Spec: Rewrite lambdas to simpler semantics instead.

docs/language/dartLangSpec.tex

Index: docs/language/dartLangSpec.tex
diff --git a/docs/language/dartLangSpec.tex b/docs/language/dartLangSpec.tex
index 5e009e68e58821021103639481f9a7b6f746d0a6..da2809692bb0a7788df5a71795c05f9c9901d896 100644
--- a/docs/language/dartLangSpec.tex
+++ b/docs/language/dartLangSpec.tex
@@ -928,7 +928,7 @@ It is a compile-time error if a class has an instance member and a static member
 \CLASS{} A \{
   \VAR{} i = 0;
   \VAR{} j;
-  f(x) =$>$ 3;
+  f(x) $=$> 3;

[eernst, 2016/11/09 11:35:37]

Oops, that wouldn't work! `$>$` may be needed (rather than a plain `>`) in order
to avoid getting the upside-down question mark glyph. But `$=$` should not be
needed (in a `dartCode` environment it should be a sans serif equals sign, and
there's nothing wrong with that, and it should have text spacing, not math
spacing, so `=` is still fine and `$=$` not needed).

So if this doesn't produce the upside-down question mark then line 931 does not
need to have any `$`s at all, but if it does produce that glyph then it should
contain two `$`s: `$>$`.

Similarly for all the other, similar cases.

[Lasse Reichstein Nielsen, 2016/11/09 12:31:56]

Ack, yes, that's just me not reading what the original actually wrote. It should
have been the same as the original.

 \}
 
 \CLASS{} B \EXTENDS{} A \{
@@ -937,7 +937,7 @@ It is a compile-time error if a class has an instance member and a static member
   //instance getter \& setter
 
   /* compile-time error: static method conflicts with instance method */
-  \STATIC{} f(x) =$>$ 3;
+  \STATIC{} f(x) $=$> 3;

[eernst, 2016/11/09 11:35:37]

`$>$`

[Lasse Reichstein Nielsen, 2016/11/09 12:31:56]

Acknowledged.

 \}
 \end{dartCode}
 
@@ -3821,36 +3821,41 @@ Method invocation can take several forms as specified below.
 An ordinary method invocation can be {\em conditional} or {\em unconditional}.
 
 \LMHash{}
-Evaluation of a {\em conditional ordinary method invocation} $e$ of the form
+Evaluation of a {\em conditional ordinary method invocation} $i$ of the form
 
 \LMHash{}
-$o?.m(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$
+$e?.m(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$
 
 \LMHash{}
-is equivalent to the evaluation of the expression
+proceeds as follows:
+
+\LMHash{}
+If $e$ is a type literal, $i$ is equivalent to \code{$e$.$m$($a_1$, \ldots , $a_n$, $x_{n+1}$: $a_{n+1}$, \ldots , $x_{n+k}$: $a_{n+k}$)}.
 
 \LMHash{}
-$((x) => x == \NULL ? \NULL : x.m(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k}))(o)$.
+Otherwise, evaluate $e$ to an object $o$.
+If $o$ is the null value, $i$ evaluates to the null value.
+Otherwise let $v$ be a fresh variable bound to $o$ and evaluate
+\code{$v$.$m$($a_1$, $\ldots$ , $a_n$, $x_{n+1}$: $a_{n+1}$, $\ldots$ , $x_{n+k}$: $a_{n+k}$))} to a value $r$, and then $e$ evaluates to $r$.
 
-unless $o$ is  a type literal, in which case it is equivalent to $o.m(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$.
 
 \LMHash{}
-The static type of $e$ is the same as the static type of $o.m(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$. Exactly the same static warnings that would be caused by $o.m(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$ are also generated in the case of $o?.m(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$.
+The static type of $i$ is the same as the static type of $e.m(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$. Exactly the same static warnings that would be caused by $e.m(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$ are also generated in the case of $e?.m(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$.
 
 \LMHash{}
 An {\em unconditional ordinary method invocation} $i$ has the form
 
-$o.m(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$.
+$e.m(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$.
 
 \LMHash{}
 Evaluation of an unconditional ordinary method invocation $i$ of the form
 
-$o.m(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$
+$e.m(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$
 
 proceeds as follows:
 
 \LMHash{}
-First, the expression $o$ is evaluated to a value $v_o$. Next, the argument list $(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$ is evaluated yielding actual argument objects $o_1, \ldots , o_{n+k}$. Let $f$ be the result of looking up (\ref{methodLookup}) method $m$  in $v_o$ with respect to the current library $L$.
+First, the expression $e$ is evaluated to a value $o$. Next, the argument list $(a_1, \ldots , a_n, x_{n+1}: a_{n+1}, \ldots , x_{n+k}: a_{n+k})$ is evaluated yielding actual argument objects $o_1, \ldots , o_{n+k}$. Let $f$ be the result of looking up (\ref{methodLookup}) method $m$  in $o$ with respect to the current library $L$.
 
 \LMHash{}
 Let $p_1 \ldots p_h$ be the required parameters of $f$,  let $p_1 \ldots p_m$ be the positional parameters of $f$ and let $p_{h+1}, \ldots, p_{h+l}$ be the optional parameters declared by $f$.
@@ -3860,15 +3865,15 @@ We have an argument list consisting of $n$ positional arguments and $k$ named ar
 }
 
 \LMHash{}
-If  $n < h$, or $n > m$, the method lookup has failed. Furthermore, each $x_i, n+1 \le i \le n+k$,  must have a corresponding named parameter in the set $\{p_{m+1}, \ldots, p_{h+l}\}$ or the method lookup also fails.  If $v_o$ is an instance of \code{Type} but $o$ is not a constant type literal, then if $m$ is a method that forwards (\ref{functionDeclarations}) to a static method, method lookup fails. Otherwise method lookup has succeeded.
+If  $n < h$, or $n > m$, the method lookup has failed. Furthermore, each $x_i, n+1 \le i \le n+k$,  must have a corresponding named parameter in the set $\{p_{m+1}, \ldots, p_{h+l}\}$ or the method lookup also fails.  If $o$ is an instance of \code{Type} but $e$ is not a constant type literal, then if $m$ is a method that forwards (\ref{functionDeclarations}) to a static method, method lookup fails. Otherwise method lookup has succeeded.
 
 \LMHash{}
-If the method lookup succeeded, the body of $f$ is executed with respect to the bindings that resulted from the evaluation of the argument list, and with \THIS{} bound to $v_o$. The value of $i$ is the value returned after $f$ is executed.
+If the method lookup succeeded, the body of $f$ is executed with respect to the bindings that resulted from the evaluation of the argument list, and with \THIS{} bound to $o$. The value of $i$ is the value returned after $f$ is executed.
 
 \LMHash{}
-If the method lookup has failed, then let $g$ be the result of looking up getter (\ref{getterAndSetterLookup}) $m$ in $v_o$ with respect to $L$.
-If $v_o$ is an instance of \code{Type} but $o$ is not a constant type literal, then if $g$ is a getter that forwards to a static getter, getter lookup fails.
-If the getter lookup succeeded, let $v_g$ be the value of the getter invocation $o.m$. Then the value of $i$ is the result of invoking
+If the method lookup has failed, then let $g$ be the result of looking up getter (\ref{getterAndSetterLookup}) $m$ in $o$ with respect to $L$.
+If $o$ is an instance of \code{Type} but $e$ is not a constant type literal, then if $g$ is a getter that forwards to a static getter, getter lookup fails.
+If the getter lookup succeeded, let $v_g$ be the value of the getter invocation $e.m$. Then the value of $i$ is the result of invoking
 the static method \code{Function.apply()} with arguments $v.g, [o_1, \ldots , o_n], \{\#x_{n+1}: o_{n+1}, \ldots , \#x_{n+k}: o_{n+k}\}$.
 
 \LMHash{}
@@ -3925,8 +3930,8 @@ It is a compile-time error to invoke any of the methods of class \cd{Object} on
 \LMLabel{cascadedInvocations}
 
 \LMHash{}
-A {\em cascaded method invocation} has the form {\em e..suffix}
-where $e$ is an expression and {\em suffix} is a sequence of operator, method, getter or setter invocations.
+A {\em cascaded method invocation} has the form \code{$e$..\metavar{suffix}}
+where $e$ is an expression and \metavar{suffix} is a sequence of operator, method, getter or setter invocations.
 
 \begin{grammar}
 {\bf cascadeSection:}
@@ -3939,10 +3944,15 @@ where $e$ is an expression and {\em suffix} is a sequence of operator, method, g
 \end{grammar}
 
 \LMHash{}
-A cascaded method invocation expression of the form {\em e..suffix} is equivalent to the expression \code{(t)\{t.{\em suffix}; \RETURN{} t;\}($e$)}.
+Evaluation of a cascaded method invocation expression $e$ of the form \code{$e$..\metavar{suffix}} proceeds as follows:
+
+Evaluate $e$ to an object $o$.
+Let $t$ be a fresh variable bound to $o$.
+Evaluate \code{$t$.\metavar{suffix}} to an object.
+Then $e$ evaluates to $o$.
 
 \rationale{
-With the introduction of null-aware conditional assignable expressions (\ref{assignableExpressions}), it would make sense to extend cascades with a null-aware conditional form as well. One might define {\em e?..suffix}  to be equivalent to the expression \code{(t)\{t?.{\em suffix}; \RETURN{} t;\}($e$)}.
+With the introduction of null-aware conditional assignable expressions (\ref{assignableExpressions}), it would make sense to extend cascades with a null-aware conditional form as well. One might define \code{$e$?..\metavar{suffix}} to be equivalent to the expression \code{$t$ == null ? null : $t$.\metavar{suffix}} where \code{t} is a fresh variable bound to the value of $e$.

[eernst, 2016/11/09 11:35:37]

`where $t$ is`

[Lasse Reichstein Nielsen, 2016/11/09 12:31:55]

Done.

 
 The present specification has not added such a construct, in the interests of simplicity and rapid language evolution. However, Dart implementations may experiment with such constructs, as noted in section \ref{ecmaConformance}.
 }
@@ -4029,10 +4039,22 @@ A property extraction can be either:
 
 Property extraction can be either {\em conditional} or {\em unconditional}.
 
-Evaluation of a {\em conditional property extraction expression} $e$ of the form $e_1?.id$  is equivalent to the evaluation of the expression  $((x) => x == \NULL ? \NULL : x.id)(e_1)$.
-unless $e_1$ is  a type literal, in which case it is equivalent to $e_1.m$.
+\LMHash{}
+Evaluation of a {\em conditional property extraction expression} $e$
+of the form \code{$e_1$?.\metavar{id}} proceeds as follows:
+
+\LMHash{}
+If $e_1$ is a type literal, $e$ is equivalent to $e_1.m$.

[eernst, 2016/11/09 11:35:37]

I believe it has to be `\code{$e_1$.\metavar{id}}`, not `$e_1.m$`.

[Lasse Reichstein Nielsen, 2016/11/09 12:31:56]

Done.

+
+\LMHash{}
+Otherwise evaluate $e_1$ to an object $o$.
+If $o$ is the null value, $e$ evaluates to the null value.
+Otherwise let $x$ be a fresh variable bound to $o$
+and evaluate \code{$x$.\metavar{id}} to a value $r$.
+Then $e$ evaluates to $r$.
+
 
-The static type of $e$ is the same as the static type of $e_1.id$. Let $T$ be the static type of $e_1$ and let $y$ be a fresh variable of type $T$. Exactly the same static warnings that would be caused by $y.id$ are also generated in the case of $e_1?.id$.
+The static type of $e$ is the same as the static type of \code{$e_1$.\metavar{id}}. Let $T$ be the static type of $e_1$ and let $y$ be a fresh variable of type $T$. Exactly the same static warnings that would be caused by \code{$y$.\metavar{id}} are also generated in the case of \code{$e_1$?.\metavar{id}}.
 
 \LMHash{}
 Unconditional property extraction has one of two syntactic forms: $e.m$ (\ref{getterAccessAndMethodExtraction}) or $\SUPER.m$ (\ref{superGetterAccessAndMethodClosurization}), where $e$ is an expression and $m$ is an identifier.
@@ -4163,7 +4185,7 @@ $(r_1, \ldots, r_n, [p_1 = d_1, \ldots , p_k = d_k])$\{
 \}
 \end{dartCode}
 if $f$ is named $m$ and has required parameters $r_1, \ldots, r_n$, and optional positional parameters $p_1, \ldots, p_k$ with defaults $d_1, \ldots, d_k$.
-%\end{itemize}
+\end{itemize}
 
 \LMHash{}
 Except that iff  \code{identical($o_1, o_2$)}  then \cd{$o_1.m$ == $o_2.m$}.
@@ -4263,12 +4285,24 @@ In checked mode, it is a dynamic type error if $o$ is not \NULL{} and the interf
 It is a static type warning if the static type of $e$ may not be assigned to the static type of $v$. The static type of the expression $v$ \code{=} $e$ is the static type of $e$.
 
 \LMHash{}
-Evaluation of an assignment $a$ of the form $e_1?.v$ \code{=} $e_2$ is equivalent to the evaluation of the expression $((x) => x == \NULL? \NULL: x.v = e_2)(e_1)$
- unless $e_1$ is  a type literal, in which case it is equivalent to $e_1.v$ \code{=} $e_2$.
-. The static type of $a$ is the static type of $e_2$. Let $T$ be the static type of $e_1$ and let $y$ be a fresh variable of type $T$. Exactly the same static warnings that would be caused by $y.v = e_2$ are also generated in the case of $e_1?.v$ \code{=} $e_2$.
+Evaluation of an assignment $a$ of the form \code{$e_1$?.$v$ = $e_2$}
+proceeds as follows:
+
+\LMHash
+If $e_1$ is a type literal, $a$ is equivalent to \code{$e_1$.$v$ = $e_2$}.
 
 \LMHash{}
-Evaluation of an assignment of the form $e_1.v$ \code{=} $e_2$ proceeds as follows:
+Otherwise evaluate $e_1$ to an object $o$.
+If $o$ is the null value, $a$ evaluates to the null value.
+Otherwise let $x$ be a fresh variable bound to $o$
+and evaluate \code{$x$.$v$ = $e_2$} to an object $r$.
+Then $a$ evaluates to $r$.
+
+\LMHash{}
+The static type of $a$ is the static type of $e_2$. Let $T$ be the static type of $e_1$ and let $y$ be a fresh variable of type $T$. Exactly the same static warnings that would be caused by \code{$y$.$v$ = $e_2$} are also generated in the case of \code{$e_1$?.$v$ = $e_2$}.
+
+\LMHash{}
+Evaluation of an assignment of the form \code{$e_1$.$v$ = $e_2$} proceeds as follows:
 
 \LMHash{}
 The expression $e_1$ is evaluated to an object $o_1$. Then, the expression $e_2$  is evaluated to an object $o_2$. Then, the setter $v=$ is looked up (\ref{getterAndSetterLookup}) in $o_1$ with respect to the current library.  If $o_1$ is an instance of \code{Type} but $e_1$ is not a constant type literal, then if $v=$ is a setter that forwards (\ref{functionDeclarations}) to a static setter, setter lookup fails. Otherwise, the body  of $v=$ is executed with its formal parameter bound to $o_2$ and \THIS{} bound to $o_1$.
@@ -4354,10 +4388,17 @@ It is a static type warning if the static type of $e$ may not be assigned to the
 
 
 \LMHash{}
-Evaluation of an assignment of the form $e_1[e_2]$ \code{=} $e_3$ is equivalent to the evaluation of the expression \code{(a, i, e)\{a.[]=(i, e); \RETURN{} e; \} ($e_1, e_2, e_3$)}.  The static type of the expression $e_1[e_2]$ \code{=} $e_3$ is the static type of $e_3$.
+Evaluation of an assignment $e$ of the form \code{$e_1$[$e_2$] = $e_3$}
+proceeds as follows:
+

[eernst, 2016/11/09 11:35:38]

Add a new line with `\LMHash{}` after this line.

[Lasse Reichstein Nielsen, 2016/11/09 12:31:56]

Done.

+Evaluate $e_1$ to an object $a$, then evaluate $e_2$ to an object $i$, and finally evaluate $e_3$ to an object $v$.
+Call the method \code{[]=} on $a$ with $i$ as first argument and $v$ as second argument.
+Then $e$ evaluates to $v$.
+

[eernst, 2016/11/09 11:35:37]

Add an `\LMHash{}` line.

[Lasse Reichstein Nielsen, 2016/11/09 12:31:55]

Done.

+The static type of the expression \code{$e_1$[$e_2$] = $e_3$} is the static type of $e_3$.
 
 \LMHash{}
-An assignment of the form $\SUPER[e_1]$ \code{=} $e_2$ is equivalent to the expression $\SUPER.[e_1]$ \code{=} $e_2$.  The static type of the expression $\SUPER[e_1]$ \code{=} $e_2$ is the static type of $e_2$.
+An assignment of the form \code{\SUPER[$e_1$] = $e_2$} is equivalent to the expression \code{\SUPER.[$e_1$] = $e_2$}.  The static type of the expression \code{\SUPER[$e_1$] = $e_2$} is the static type of $e_2$.
 
 
 % Should we add: It is a dynamic error if $e_1$ evaluates to an  constant list or map.
@@ -4374,27 +4415,67 @@ It is a compile-time error to invoke any of the setters of class \cd{Object} on
 \LMLabel{compoundAssignment}
 
 \LMHash{}
-Evaluation of a compound assignment of the form $v$ {\em ??=} $e$ is equivalent to the evaluation of the expression  $((x) => x == \NULL{}$ ?  $v=e : x)(v)$ where $x$ is a fresh variable that is not used in $e$.
+Evaluation of a compound assignment $a$ of the form \code{$v$ ??= $e$}
+proceeds as follows:
+
+Evaluate $v$ to an object $o$.
+If $o$ is not the null value, $a$ evaluates to $o$.
+Otherwise evaluate \code{$v$ = $e$} to a value $r$,
+and then $a$ evaluates to $r$.
 
 \LMHash{}
-Evaluation of a compound assignment of the form $C.v$ {\em ??=} $e$, where $C$ is a type literal, is equivalent to the evaluation of the expression  $((x) => x == \NULL{}$?  $C.v=e: x)(C.v)$ where $x$ is a fresh variable that is not used in $e$.
+Evaluation of a compound assignment, $a$ of the form \code{$C$.$v$ ??= $e$}, where $C$ is a type literal, proceeds as follow:
+
+Evaluate $C.v$ to an object $o$.
+If $o$ is not the null value, $a$ evaluates to $o$.
+Otherwise evaluate \code{$C.v$ = $e$} to a value $r$,

[eernst, 2016/11/09 11:35:38]

Might as well use `$C$.$v$` now that so many other locations are consistently
using this style.

[Lasse Reichstein Nielsen, 2016/11/09 12:31:56]

Done.

+and then $a$ evaluates to $r$.
 
 \commentary {
 The two rules above also apply when the variable v or the type C is prefixed.
 }
 
 \LMHash{}
-Evaluation of a compound assignment of the form $e_1.v$ {\em ??=} $e_2$ is equivalent to the evaluation of the expression  $((x) =>((y) => y == \NULL{}$ ? $ x.v = e_2: y)(x.v))(e_1)$ where $x$ and $y$ are distinct fresh variables that are not used in $e_2$.
+Evaluation of a compound assignment $a$ of the form \code{$e_1$.$v$ ??= $e_2$}
+proceeds as follows:
+

[eernst, 2016/11/09 11:35:37]

`\LMHash{}`

[Lasse Reichstein Nielsen, 2016/11/09 12:31:55]

Done.

+Evaluate $e_1$ to an object $u$.
+Let $x$ be a fresh variable bound to $u$.
+Evalute \code{$x$.$v$} to an object $o$.
+If $o$ is not the null value, $a$ evaluates to $o$.
+Otherwise evaluate \code{$x$.$v$ = $e_2$} to an object $r$,
+and then $a$ evaluates to $r$.
 
 \LMHash{}
-Evaluation of a compound assignment of the form  $e_1[e_2]$  {\em ??=} $e_3$ is equivalent to the evaluation of the expression
-$((a, i) => ((x) => x == \NULL{}$ ?  $a[i] = e_3: x)(a[i]))(e_1, e_2)$ where $x$, $a$ and $i$ are distinct fresh variables that are not used in $e_3$.
+Evaluation of a compound assignment $a$ of the form \code{$e_1$[$e_2$] ??= $e_3$}
+proceeds as follows:
+

[eernst, 2016/11/09 11:35:37]

`\LMHash{}`

[Lasse Reichstein Nielsen, 2016/11/09 12:31:56]

Done.

+Evaluate $e_1$ to an object $u$ and then evaluate $e_2$ to an object $i$.
+Call the \code{[]} method on $u$ with argument $i$, and let $o$ be the returned value.
+If $o$ is not the null value, $a$ evaluates to $o$.
+Otherwise evaluate $e_3$ to an object $v$
+and then call the \code{[]=} method on $u$ with $i$ as first argument and $v$ as second argument.
+Then $a$ evaluates to $v$.
 
 \LMHash{}
-Evaluation of a compound assignment of the form $\SUPER.v$  {\em ??=} $e$ is equivalent to the evaluation of the expression  $((x) => x == \NULL{}$ ? $\SUPER.v = e: x)(\SUPER.v)$ where $x$ is a fresh variable that is not used in $e$.
+Evaluation of a compound assignment $a$ of the form \code{\SUPER.$v$ ??= $e$}
+proceeds as follows:
+

[eernst, 2016/11/09 11:35:36]

`\LMHash{}`

[Lasse Reichstein Nielsen, 2016/11/09 12:31:56]

Done.

+Evaluate \code{\SUPER.$v$} to an object $o$.
+If $o$ is not the null value then $a$ evaluats to $o$.
+Otherwise evaluate \code{\SUPER.$v$ = $e$} to an object $r$,
+and then $a$ evaluates to $r$.
 
 \LMHash{}
-Evaluation of a compound assignment of the form $e_1?.v$  {\em ??=} $e_2$ is equivalent to the evaluation of the expression \code{((x) $=>$ x == \NULL{} ?  \NULL: $x.v ??=  e_2$)($e_1$)} where $x$ is a variable that is not used in $e_2$.
+Evaluation of a compound assignment $a$ of the form \code{$e_1$?.$v$ ??= $e_2$}
+proceeds as follows:
+

[eernst, 2016/11/09 11:35:37]

`\LMHash{}`

[Lasse Reichstein Nielsen, 2016/11/09 12:31:55]

Done.

+Evaluate $e_1$ to an object $u$ and let $x$ be a fresh variable bound to $u$.
+Evaluate \code{$x$.$v$} to an object $o$.
+If $o$ is not the null value then $a$ evaluates to $o$.
+Otherwise evaluate \code{$x$.$v$ = $e_2$} to an object $r$,
+and then $a$ evaluates to $r$.
+
 % But what about C?.v ??= e
 
 \LMHash{}
@@ -4417,11 +4498,29 @@ The static type of a compound assignment of the form $e_1[e_2]$  {\em ??=} $e_3$
 The static type of a compound assignment of the form $\SUPER.v$  {\em ??=} $e$  is the least upper bound of the static type of $\SUPER.v$ and the static type of $e$. Exactly the same static warnings that would be caused by $\SUPER.v = e$ are also generated in the case of $\SUPER.v$  {\em ??=} $e$.
 
 \LMHash{}
-For any other valid operator $op$, a compound assignment of the form $v$ $op\code{=} e$ is equivalent to $v \code{=} v$ $op$ $e$. A compound assignment of the form $C.v$ $op \code{=} e$ is equivalent to $C.v \code{=} C.v$ $op$ $e$. A compound assignment of the form $e_1.v$ $op = e_2$ is equivalent to \code{((x) $=>$ x.v = x.v $op$ $e_2$)($e_1$)} where $x$ is a variable that is not used in $e_2$. A compound assignment of the form  $e_1[e_2]$ $op\code{=} e_3$ is equivalent to
-\code{((a, i) $=>$ a[i] = a[i] $op$ $e_3$)($e_1, e_2$)} where $a$ and $i$ are a variables that are not used in $e_3$.
+For any other valid operator $op$, a compound assignment of the form \code{$v$ $op$= $e$} is equivalent to \code{$v$ = $v$ $op$ $e$}. A compound assignment of the form \code{$C$.$v$ $op$= $e$} is equivalent to \code{$C$.$v$ = $C$.$v$ $op$ $e$}.
+

[eernst, 2016/11/09 11:35:37]

`\LMHash{}`

[Lasse Reichstein Nielsen, 2016/11/09 12:31:55]

Done.

+Evaluation of a compound assignment $a$ of the form \code{$e_1$.$v$ $op$= $e_2$} proceeds as follows:
+Evaluate $e_1$ to an object $u$ and let $x$ be a fresh variable bound to $u$.
+Evaluate \code{$x$.$v$ = $x$.$v$ $op$ $e_2$} to an object $r$
+and then $a$ evaluates to $r$.
+

[eernst, 2016/11/09 11:35:38]

`\LMHash{}`

[Lasse Reichstein Nielsen, 2016/11/09 12:31:56]

Done.

+Evaluation of s compound assignment $a$ of the form \code{$e_1$[$e_2$] $op$= $e_3$} proceeds as follows:
+Evaluate $e_1$ to an object $u$ and evaluate $e_2$ to an object $v$.
+Let $a$ and $i$ be fresh variables bound to $u$ and $v$ respectively.
+Evaluate \code{$a$[$i$] = $a$[$i$] $op$ $e_3$} to an object $r$,
+and then $a$ evaluates to $r$.
 
 \LMHash{}
-Evaluation of a compound assignment of the form $e_1?.v$ $op = e_2$ is equivalent to \code{((x) $=>$ x?.v = x.v $op$ $e_2$)($e_1$)} where $x$ is a variable that is not used in $e_2$. The static type of $e_1?.v$ $op = e_2$ is the static type of $e_1.v$ $op$ $e_2$. Exactly the same static warnings that would be caused by $e_1.v$ $op = e_2$ are also generated in the case of $e_1?.v$ $op = e_2$.
+Evaluation of a compound assignment $a$ of the form \code{$e_1$?.$v$ $op$ = $e_2$} proceeds as follows:
+

[eernst, 2016/11/09 11:35:38]

`\LMHash{}`

[Lasse Reichstein Nielsen, 2016/11/09 12:31:55]

Done.

+Evaluate $e_1$ to an object $u$.
+If $u$ is the null value, then $a$ evaluates to the null value.
+Otherwise let $x$ be a fresh variable bound to $u$.
+Evaluate \code{$x$.$v$ $op$= $e_2$} to an object $r$.
+Then $a$ evaluates to $r$.
+

[eernst, 2016/11/09 11:35:37]

`\LMHash{}`

[Lasse Reichstein Nielsen, 2016/11/09 12:31:56]

Done.

+The static type of \code{$e_1$?.$v$ $op$= $e_2$} is the static type of \code{$e_1$.$v$ $op$ $e_2$}. Exactly the same static warnings that would be caused by \code{$e_1$.$v$ $op$= $e_2$} are also generated in the case of \code{$e_1$?.$v$ $op$= $e_2$}.
 
 \LMHash{}
 A compound assignment of the form $C?.v$ $op = e_2$ is equivalent to the expression
@@ -4489,7 +4588,15 @@ then the type of $v$ is known to be $T$ in $e_2$.
 \end{grammar}
 
 \LMHash{}
-Evaluation of an if-null expression $e$ of the form $e_1??e_2 $ is equivalent to the evaluation of the expression $((x) => x == \NULL? e_2: x)(e_1)$. The static type of $e$ is least upper bound (\ref{leastUpperBounds}) of the static type of $e_1$ and the static type of $e_2$.
+Evaluation of an if-null expression $e$ of the form \code{$e_1$ ?? $e_2$}
+proceeds as follows:
+

[eernst, 2016/11/09 11:35:37]

`\LMHash{}`

[Lasse Reichstein Nielsen, 2016/11/09 12:31:56]

Done.

+Evaluate $e_1$ to an object $o$.
+If $o$ is not the null value, then $e$ evaluates to $o$.
+Otherwise evaluate $e_2$ to an object $r$,
+and then $e$ evaluates to $r$.
+

[eernst, 2016/11/09 11:35:38]

`\LMHash{}`

[Lasse Reichstein Nielsen, 2016/11/09 12:31:56]

Done.

+The static type of $e$ is least upper bound (\ref{leastUpperBounds}) of the static type of $e_1$ and the static type of $e_2$.

[eernst, 2016/11/09 11:35:38]

`is least` --> `is the least`

[Lasse Reichstein Nielsen, 2016/11/09 12:31:56]

Done.

 
 
 \subsection{ Logical Boolean Expressions}
@@ -4860,7 +4967,11 @@ Postfix expressions invoke the postfix operators on objects.
  A {\em postfix expression} is either a primary expression, a function, method or getter invocation, or an invocation of a postfix operator on an expression $e$.
 
 \LMHash{}
-Execution of a postfix expression of the form \code{$v$++}, where $v$ is an identifier, is equivalent to executing \code{()\{\VAR{} r = $v$; $v$ = r + 1; \RETURN{} r\}()}.
+Evaluation of a postfix expression $e$ of the form \code{$v$++}, where $v$ is an identifier, proceeds as follows:
+

[eernst, 2016/11/09 11:35:37]

`\LMHash{}`

[Lasse Reichstein Nielsen, 2016/11/09 12:31:56]

Done.

+Evaluate $v$ to an object $r$ and let $y$ be a fresh variable bound to $r$.
+Evaluate \code{$v$ = $y$ + 1}.
+Then $e$ evaluates to $r$.
 
 \LMHash{}
 The static type of such an expression is the static type of $v$.
@@ -4870,86 +4981,130 @@ The static type of such an expression is the static type of $v$.
 }
 
 \LMHash{}
-Execution of a postfix expression of the form \code{$C.v$ ++} is equivalent to executing
+Evaluation of a postfix expression $e$ of the form \code{$C$.$v$++}
+proceeds as follows:
 

[eernst, 2016/11/09 11:35:37]

`\LMHash{}`

[Lasse Reichstein Nielsen, 2016/11/09 12:31:56]

Done.

-\code{()\{\VAR{} r = $C.v$; $C.v$ = r + 1; \RETURN{} r\}()}.
+Evaluate $C.v$ to a value $r$ and let $y$ be a fresh variable bound to $r$.

[eernst, 2016/11/09 11:35:38]

Well, `\code{$C$.$v$}` would be the strictly consistent version.

[Lasse Reichstein Nielsen, 2016/11/09 12:31:56]

Done.

+Evaluate \code{$C.v$ = $y$ + 1}.

[eernst, 2016/11/09 11:35:37]

`$C$.$v$`

[Lasse Reichstein Nielsen, 2016/11/09 12:31:56]

Done.

+Then $e$ evaluates to $r$.
 
 \LMHash{}
-The static type of such an expression is the static type of $C.v$.
+The static type of such an expression is the static type of \code{$C$.$v$}.
 
 
 \LMHash{}
-Execution of a postfix expression of the form \code{$e_1.v$++} is equivalent to executing
+Evaluating of a postfix expression $e$ of the form \code{$e_1$.$v$++}

[eernst, 2016/11/09 11:35:37]

`Evaluating` --> `Evaluation`

[Lasse Reichstein Nielsen, 2016/11/09 12:31:55]

Done.

+proceeds as follows:
 

[eernst, 2016/11/09 11:35:37]

`\LMHash{}`

[Lasse Reichstein Nielsen, 2016/11/09 12:31:55]

Done.

-\code{(x)\{\VAR{} r = x.v; x.v = r + 1; \RETURN{} r\}($e_1$)}.
+Evaluate $e_1$ to an object $u$ and let $x$ be a fresh variable bound to $u$.
+Evaluate \code{$x$.$v$} to a value $r$
+and let $y$ be a fresh variable bound to $r$.
+Evaluate \code{$x$.$v$ = $y$ + 1}.
+Then $e$ evaluates to $r$.
 
 \LMHash{}
-The static type of such an expression is the static type of $e_1.v$.
+The static type of such an expression is the static type of \code{$e_1$.$v$}.
 
 
 \LMHash{}
-Execution of a postfix expression of the form \code{$e_1[e_2]$++},  is equivalent to executing
+Evaluation of a postfix expression $e$ of the form \code{$e_1$[$e_2$]++}
+proceeds as follows:
 

[eernst, 2016/11/09 11:35:37]

`\LMHash{}`

[Lasse Reichstein Nielsen, 2016/11/09 12:31:56]

Done.

-\code{(a, i)\{\VAR{} r = a[i]; a[i] = r + 1; \RETURN{} r\}($e_1$, $e_2$)}.
+Evaluate $e_1$ to an object $u$ and $e_2$ to an object $v$.
+Let $a$ and $i$ be fresh variables bound to $u$ and $v$ respectively.
+Evaluate \code{$a$[$i$]} to an object $r$
+and let $y$ be a fresh variable bound to $r$.
+Evaluate \code{$a$[$i$] = $y$ + 1}.
+Then $e$ evaluates to $r$.
 
 \LMHash{}
-The static type of such an expression is the static type of $e_1[e_2]$.
+The static type of such an expression is the static type of \code{$e_1$[$e_2$]}.
 
 
 \LMHash{}
-Execution of a postfix expression of the form \code{$v$-{}-}, where $v$ is an identifier, is equivalent to executing
+Evaluation of a postfix expression $e$ of the form \code{$v$-{}-}, where $v$ is an identifier, proceeds as follows:
 

[eernst, 2016/11/09 11:35:38]

`\LMHash{}`

[Lasse Reichstein Nielsen, 2016/11/09 12:31:56]

Done.

-\code{()\{\VAR{} r = $v$; $v$ = r - 1; \RETURN{} r\}()}.
+Evaluate the expression $v$ to an object $r$
+and let $y$ be a fresh variable bound to $r$.
+Evaluate \code{$v$ = $y$ - 1}.
+Then $e$ evaluates to $r$.
 
 \LMHash{}
 The static type of such an expression is the static type of $v$.
 
 
 \LMHash{}
-Execution of a postfix expression of the form \code{$C.v$-{}-} is equivalent to executing
+Evaluation of a postfix expression $e$ of the form \code{$C$.$v$-{}-}
+proceeds as follows:
 

[eernst, 2016/11/09 11:35:37]

`\LMHash{}`

[Lasse Reichstein Nielsen, 2016/11/09 12:31:56]

Done.

-\code{()\{\VAR{} r = $C.v$; $C.v$ = r - 1; \RETURN{} r\}()}.
+Evaluate \code{$C$.$v$} to a value $r$
+and let $y$ be a fresh variable bound to $r$.
+Evaluate \code{$C$.$v$ = $y$ - 1}.
+Then $e$ evaluates to $r$.
 
 \LMHash{}
-The static type of such an expression is the static type of $C.v$.
+The static type of such an expression is the static type of \code{$C$.$v$}.
 
 
 \LMHash{}
-Execution of a postfix expression of the form \code{$e_1.v$-{}-} is equivalent to executing
+Evaluation of a postfix expression of the form \code{$e_1$.$v$-{}-}
+proceeds as follows:
+

[eernst, 2016/11/09 11:35:37]

`\LMHash{}`

[Lasse Reichstein Nielsen, 2016/11/09 12:31:56]

Done.

+Evaluate $e_1$ to an object $u$ and let $x$ be a fresh variable bound to $u$.
+Evaluate \code{$x$.$v$} to a value $r$
+and let $y$ be a fresh variable bound to $r$.
+Evaluate \code{$x$.$v$ = $y$ - 1}.
+Then $e$ evaluates to $r$.
 
-\code{(x)\{\VAR{} r = x.v; x.v = r - 1; \RETURN{} r\}($e_1$)}.
 
 \LMHash{}
-The static type of such an expression is the static type of $e_1.v$.
+The static type of such an expression is the static type of \code{$e_1$.$v$}.
 
 
 \LMHash{}
-Execution of a postfix expression of the form \code{$e_1[e_2]$-{}-},  is equivalent to executing
+Evaluation of a postfix expression $e$ of the form \code{$e_1$[$e_2$]-{}-}
+proceeds as follows:
 

[eernst, 2016/11/09 11:35:37]

`\LMHash{}`

[Lasse Reichstein Nielsen, 2016/11/09 12:31:55]

Done.

-\code{(a, i)\{\VAR{} r = a[i]; a[i] = r - 1; \RETURN{} r\}($e_1$, $e_2$)}.
+Evaluate $e_1$ to an object $u$ and $e_2$ to an object $v$.
+Let $a$ and $i$ be fresh variables bound to $u$ and $v$ respectively.
+Evaluate \code{$a$[$i$]} to an object $r$
+and let $y$ be a fresh variable bound to $r$.
+Evaluate \code{$a$[$i$] = $y$ - 1}.
+Then $e$ evaluates to $r$.
 
 \LMHash{}
-The static type of such an expression is the static type of $e_1[e_2]$.
+The static type of such an expression is the static type of \code{$e_1$[$e_2$]}.
 
 \LMHash{}
-Execution of a postfix expression of the form \code{$e_1?.v$++} is equivalent to executing
+Evaluation of a postfix expression $e$ of the form \code{$e_1$?.$v$++}
+where $e_1$ is not a type literal, proceeds as follows:
 

[eernst, 2016/11/09 11:35:38]

`\LMHash{}`

[Lasse Reichstein Nielsen, 2016/11/09 12:31:56]

Done.

-\code{((x) =$>$ x == \NULL? \NULL : x.v++)($e_1$)}
-unless $e_1$ is a type literal, in which case it is equivalent to \code{$e_1.v$++}
-.
+If $e_1$ is a type literal, $e$ is equivalent to \code{$e_1$.$v$++}.
+

[eernst, 2016/11/09 11:35:38]

`\LMHash{}`

[Lasse Reichstein Nielsen, 2016/11/09 12:31:56]

Done.

+Otherwise evaluate $e_1$ to an object $u$.
+if $u$ is the null value, $e$ evaluates to the null value.
+Otherwise let $x$ be a fresh variable bound to $u$.
+Evaluate \code{$x$.$v$++} to an object $o$.
+Then $e$ evaluates to $o$.
 
 \LMHash{}
-The static type of such an expression is the static type of $e_1.v$.
+The static type of such an expression is the static type of \code{$e_1$.$v$}.
 
 \LMHash{}
-Execution of a postfix expression of the form \code{$e_1?.v$-{}-} is equivalent to executing
+Evaluation of a postfix expression $e$ of the form \code{$e_1$?.$v$-{}-}
+where $e_1$ is not a type literal, proceeds as follows:
+

[eernst, 2016/11/09 11:35:37]

`\LMHash{}`

[Lasse Reichstein Nielsen, 2016/11/09 12:31:56]

Done.

+If $e_1$ is a type literal, $e$ is equivalent to \code{$e_1$.$v$-{}-}.
+

[eernst, 2016/11/09 11:35:36]

`\LMHash{}`

[Lasse Reichstein Nielsen, 2016/11/09 12:31:55]

Done.

+Otherwise evaluate $e_1$ to an object $u$.
+If $u$ is the null value, $e$ evalkuates to the null value.
+Otherwise let $x$ be a fresh variable bound to $u$.
+Evaluate \code{$x$.$v$-{}-} to an object $o$.
+Then $e$ evaluates to $o$.
 
-\code{((x) =$>$ x == \NULL? \NULL : x.v-{}-)($e_1$)}
-unless $e_1$ is a type literal, in which case it is equivalent to \code{$e_1.v$-{}-}
-.
 
 \LMHash{}
-The static type of such an expression is the static type of $e_1.v$.
+The static type of such an expression is the static type of \code{$e_1$.$v$}.
 
 
 \subsection{ Assignable Expressions}
@@ -5217,7 +5372,6 @@ In all other cases,  a \code{CastError} is thrown.
 \LMHash{}
 The static type of a cast expression  \code{$e$ \AS{} $T$}  is $T$.
 

[eernst, 2016/11/09 11:35:38]

Actually the spec is not at all as consistent as I thought when it comes to
empty lines before sectioning commands. Let's just take one step in a separate
CL, and make them all one-line-blocks: Any attempt to make the LaTeX source look
like a wysiwyg document will fail anyway, so readability is not improved much by
"big break semantically, two empty lines" or anything like that. With that,
deletion of line 5220 is fine as well.

[Lasse Reichstein Nielsen, 2016/11/09 12:31:56]

Acknowledged.

-
 \section{Statements}
 \LMLabel{statements}
 
@@ -5353,7 +5507,7 @@ A function declaration statement of one of the forms $id$ $signature$ $\{ statem
 }
 
 \begin{dartCode}
-f(x) =$>$ x++;  // a top level function
+f(x) $=$> x++;  // a top level function

[eernst, 2016/11/09 11:35:37]

Revert to `=$>$`, or just omit all `$`s if that works.

[Lasse Reichstein Nielsen, 2016/11/09 12:31:56]

Done.

 top() \{ // another top level function
   f(3); // illegal
   f(x) $=>$ x $>$ 0? x*f(x-1): 1;  // recursion is legal
@@ -5949,7 +6103,8 @@ Otherwise $m$ terminates.
 Otherwise, execution resumes at the end of the try statement.
 
 \LMHash{}
-Execution of an \ON{}-\CATCH{} clause \code{\ON{} $T$ \CATCH{} ($p_1$, $p_2$)} $s$ of a try statement $t$ proceeds as follows: The statement $s$ is executed in the dynamic scope of the exception handler defined by the finally clause of $t$. Then, the current exception and active stack trace both become undefined.
+Execution of an \ON{}-\CATCH{} clause \code{\ON{} $T$ \CATCH{} ($p_1$, $p_2$)} $s$ of a try statement $t$ proceeds as follows:
+The statement $s$ is executed in the dynamic scope of the exception handler defined by the finally clause of $t$. Then, the current exception and active stack trace both become undefined.
 
 \LMHash{}
 Execution of a \FINALLY{} clause \FINALLY{} $s$ of a try statement proceeds as follows: