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 d0f62f2bbce8c323cf7d0d51e4f19cb4c584e135..dc360c0b17c4f23bf7077be8c0112bc9f13584a7 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/03 18:07:05]

The `dartCode` environment shows source code in a sans serif font (using
\sffamily), and it does a few other things to preserve white space. So the `=`
used to be in sans serif font and the `>` was in math mode (which use different
fonts, and a plethora of complex spacing rules).

I would actually expect the change from `=$>$` to `$=>$` to introduce "operator"
spacing between the two operators --- but apparently we don't get the extra
space, probably because it's classified as two operators rather than an operator
and an operand.

In any case, I can't see any difference between the sans serif `=` and the math
mode `=`, and I can't see any significant difference in the spacing either. So
I'd suggest that we avoid making changes like this because it doesn't improve
anything. I can see that there are other occurrences of `$=>$`, but the approach
where the single char `>` is in math mode seems to be the most common (a quick
estimate says 7-10 times more frequent), so this change would make things less
consistent, not more.

For a longer term solution, we are forced to put `>` in a math context in order
to get the "right angle" glyph rather than the "upside-down question mark"
glyph, but we have a lot of messy spacing due to misplaced math environments.
For example, `<` and `>` in generic class instantiations get far too much space
(e.g., `$S<U_1,  \ldots, U_m>$` in `\subsubsection{New}`).

So we would need to (1) create `\newcommand`s for each construct including all
the incantations needed in order to get the formatting right, and (2) use them
consistently. This would make it possible to fiddle with the spacing and fonts
in the definition, and consistently get the good quality formatting at each
"call site".

[Lasse Reichstein Nielsen, 2016/11/08 11:42:35]

Ack. I don't like physical formatting. I'd prefer to just write \code{literal
Dart code with $variable$}.

Is there any way we can fix \code{...} and \begin{dartCode} so we can write =>
verbatim?

Reverted for now.

 \}
 
 \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/03 18:07:06]

Just keep the old version.

[Lasse Reichstein Nielsen, 2016/11/08 11:42:35]

Done.

 \}
 \end{dartCode}
 
@@ -3828,12 +3828,15 @@ Evaluation of a {\em conditional ordinary method invocation} $e$ of the form
 $o?.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{}
-$((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)$.
+If $o$ is not a type literal, evaluate $o$ to an object $x$.
+If $x$ is the null value, $e$ evaluates to the null value.

[eernst, 2016/11/03 18:07:06]

This is confusing because the scope of the first `If` is unclear: you have to
read all the way down to `If $o$ is a type literal` to see that there is no
missing case, otherwise the obvious protest here would be "but $x$ is undefined
if $o$ is a type literal, so how is that handled?".

We could make the separation smaller (and the whole thing perhaps more smooth)
by reordering:

```
\LMHash{}
If $o$ is a type literal, $e$ is equivalent to $o.m(a_1, \ldots , a_n, x_{n+1}:
a_{n+1}, \ldots , x_{n+k}: a_{n+k})$.

\LMHash{}
Otherwise $o$ is not a type literal.
Evaluate $o$ to an object $x$. ...
```

I'm not so happy about using `$o$` for syntax and `$x$` for semantic entity
(object); in many locations `$o$` is an object and there may not be a syntactic
expression which is guaranteed to evaluate to that object (or we'd need to
invent a fresh variable, as is done in some cases, such that no side-effects can
destroy it).

Maybe we could use `$e^\prime$` for the expression that evaluates to the
receiver (rather than `$o$`), and `$o$` for the resulting object (rather than
`$x$`).

[Lasse Reichstein Nielsen, 2016/11/08 11:42:34]

changed to expression $i$ on the form $e.m(...)$ and $e$ evaluates to $o$ (also
changed the following section similarly).

+Otherwise let \code{v} be a fresh variable bound to $x$ and evaluate

[Lasse Reichstein Nielsen, 2016/10/31 07:39:25]

As discussed offline, the \code{v} should be $v$ - it's a metasyntactic
variable, not a syntactic variable. Similarly for all the other cases.

[eernst, 2016/11/03 18:07:06]

Acknowledged.

+\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})$.
+If $o$ is a type literal, $e$ 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})$.
@@ -3940,10 +3943,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..suffix} proceeds as follows:

[eernst, 2016/11/03 18:07:05]

We ought to use meta-variables here: `\code{$e$..\mbox{\em suffix}}`. The use of
`\mbox{\em suffix}` rather than a plain `suffix` in math mode is motivated by
the need to have something that is similar to math mode, but avoiding the
completely non-natural-language-ish formatting of `ff` in math mode. So we need
an unusual trick because it's unusual to have these long meta-variable names.

[Lasse Reichstein Nielsen, 2016/11/08 11:42:35]

Physical formatting :(
I added a new def so I can write \metavar{suffix}.
Maybe it should just be \var or \meta.

+
+Evaluate \code{e} to an object $o$.

[eernst, 2016/11/03 18:07:03]

`\code{e}` --> `$e$`

[Lasse Reichstein Nielsen, 2016/11/08 11:42:35]

Done.

+Let $t$ be a fresh variable bound to $o$.
+Evaluate $t.suffix$ to an object.

[eernst, 2016/11/03 18:07:06]

`$t.suffix$` --> `\code{$t$.\mbox{\em suffix}}` just to be consistent (I doubt
it looks very different ;-)

[Lasse Reichstein Nielsen, 2016/11/08 11:42:36]

Done.

+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 {\em e?..suffix}  to be equivalent to the expression \code{t == \NULL{} ? \NULL{} : t.{\em suffix}} where \code{t} is bound to the value of $e$.

[eernst, 2016/11/03 18:07:06]

might as well say `$t$ is a fresh variable bound to..` as usual.

[Lasse Reichstein Nielsen, 2016/11/08 11:42:36]

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}.
 }
@@ -4034,8 +4042,14 @@ Property extraction can be either {\em conditional} or {\em unconditional}.
 Tear-offs using the \cd{ x\#id}  syntax cannot be conditional at this time; this is inconsistent, and is likely to be addressed in the near future, perhaps via  notation such as  \cd{ x?\#id} . As indicated in section \ref{ecmaConformance}, experimentation in this area is allowed.
 }
 
-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$.
+If $e_1$ is not a type literal, evaluation of a {\em conditional property extraction expression} $e$ of the form $e_1?.id$  proceeds as follows:

[eernst, 2016/11/03 18:07:05]

I think it would be useful to reorganize this a bit: 

`Evaluation of .. proceeds as follows: If $e_1$ is a type literal, $e$ is
equivalent to $e_1.id$. Otherwise, evaluate $e_1$ to an object $o$. ..`.

The point is again that the short alternative is first, such that the list
structure is more obvious, which means that it is OK that the last alternative
is contains several sentences.

Also, I suspect that math mode '?' might be different from \sffamily '?', in
which case we should probably use `$e_1$?.$id$`

[Lasse Reichstein Nielsen, 2016/11/08 11:42:34]

Done.

+
+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$.id} to a value $r$.

[eernst, 2016/11/03 18:07:03]

`$x$.$id$`.

[Lasse Reichstein Nielsen, 2016/11/08 11:42:34]

\code{$e_1$.\metavar{id}}

Logical formatting FTW!

+Then $e$ evaluates to $r$.
+
+If $e_1$ is  a type literal, $e$ is equivalent to $e_1.m$.

[eernst, 2016/11/03 18:07:06]

(If the reorg above is performed, this line is moved up).

[Lasse Reichstein Nielsen, 2016/11/08 11:42:36]

Acknowledged.

 
 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$.
 
@@ -4479,9 +4493,17 @@ 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$}

[eernst, 2016/11/03 18:07:06]

If we keep metavariables in math mode, it should be `\code{$e_1$.$v$ = $e_2$}`.

[Lasse Reichstein Nielsen, 2016/11/08 11:42:36]

Done.

+proceeds as follows:
+
+If $e_1$ is not a type literal, 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{$o$.v = $e_2$} to an object $r$.

[eernst, 2016/11/03 18:07:04]

`\code{$o$.$v$ = $e_2$}`

[Lasse Reichstein Nielsen, 2016/11/08 11:42:35]

Done.

+Then $a$ evaluates to $r$.
+
+If $e_1$ is  a type literal, $a$ is equivalent to $e_1.v$ \code{=} $e_2$.

[eernst, 2016/11/03 18:07:04]

We could reorganize this as well, both for consistency with the previous text
and for the reasons mentioned earlier:

`If $e_1$ is a type literal, $a$ is equivalent to \code{$e_1$.$v$ = $e_2$}.

Otherwise, $e_2$ is not a type literal. Evaluate $e_1$ to ..`

[Lasse Reichstein Nielsen, 2016/11/08 11:42:35]

Done.

+
+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$.
 

[eernst, 2016/11/03 18:07:06]

It's probably difficult to tell, but `\code{$y$.$v$ = $e_2$}` would be more
consistent, and `\code{$e_1$?.$v$ = $e_2$}`.

 \LMHash{}
 Evaluation of an assignment of the form $e_1.v$ \code{=} $e_2$ proceeds as follows:
@@ -4570,10 +4592,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:
+
+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 $[]=$ on $a$ with $i$ as first argument and $v$ as second argument.

[eernst, 2016/11/03 18:07:04]

The method name is actually concrete syntax, so that would be `\code{[]=}`.

[Lasse Reichstein Nielsen, 2016/11/08 11:42:35]

Done.

+Then $e$ evaluates to $v$.
+
+The static type of the expression $e_1[e_2]$ \code{=} $e_3$ is the static type of $e_3$.

[eernst, 2016/11/03 18:07:04]

`\code{$e_1$[$e_2$] = $e_3$}` would be the consistent choice.

[Lasse Reichstein Nielsen, 2016/11/08 11:42:33]

I'm all for consistency.

 
 \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.
@@ -4590,27 +4619,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 $v$ {\em ??=} $e$

[eernst, 2016/11/03 18:07:06]

I'd say `of the form \code{$v$ ??= $e$}`.

[Lasse Reichstein Nielsen, 2016/11/08 11:42:36]

Done.

+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 $C.v$ {\em ??=} $e$, where $C$ is a type literal, proceeds as follow:

[eernst, 2016/11/03 18:07:03]

`of the form \code{$C$.$v$ ??= $e$}, ..`

[Lasse Reichstein Nielsen, 2016/11/08 11:42:34]

Done.

+
+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$,
+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 $e_1.v$ {\em ??=} $e_2$

[eernst, 2016/11/03 18:07:03]

`of the form \code{$e_1$.$v$ ??= $e_2$}`

[Lasse Reichstein Nielsen, 2016/11/08 11:42:34]

Done.

+proceeds as follows:
+
+Evaluate $e_1$ to an object $u$.
+Let \code{x} be a fresh variable not occuring in $e_2$ and bound to $u$.

[eernst, 2016/11/03 18:07:07]

`$x$`, `occuring` --> `occurring`, but it's not fresh if it occurs anywhere, so
let's just say `a fresh variable bound to $u$`.

[Lasse Reichstein Nielsen, 2016/11/08 11:42:35]

Done.

+Evalute \code{x.$v$} to an object $o$.

[eernst, 2016/11/03 18:07:04]

`\code{$x$.$v$}`

[Lasse Reichstein Nielsen, 2016/11/08 11:42:34]

Done.

+If $o$ is not the null value, $a$ evaluates to $o$.
+Otherwise evaluate \code{x.$v$ = $e_2$} to an object $r$,

[eernst, 2016/11/03 18:07:04]

`\code{$x$.$v$ = $e_2$}`

[Lasse Reichstein Nielsen, 2016/11/08 11:42:35]

Done.

+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  $e_1[e_2]$  {\em ??=} $e_3$

[eernst, 2016/11/03 18:07:05]

`\code{$e_1$[$e_2$] ??= $e_3$}`

[Lasse Reichstein Nielsen, 2016/11/08 11:42:36]

Done.

+proceeds as follows:
+
+Evaluate $e_1$ to an object $u$ and then evaluate $e_2$ to an object $i$.
+Call the $[]$ method on $u$ with argument $i$ and let $o$ be the returned value.

[eernst, 2016/11/03 18:07:04]

`\code{[]}`, add comma: `argument $i$, and let`

[Lasse Reichstein Nielsen, 2016/11/08 11:42:33]

Done.

+If $o$ is not the null value, $a$ evaluates to $o$.
+Otherwise evaluate $e_3$ to an object $v$
+and then call the $[]=$ method on $u$ with $i$ as first argument and $v$ as second argument.

[eernst, 2016/11/03 18:07:04]

`\code{[]=}`

[Lasse Reichstein Nielsen, 2016/11/08 11:42:35]

Done.

+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 $\SUPER.v$  {\em ??=} $e$

[eernst, 2016/11/03 18:07:04]

`\code{\SUPER.$v$ ??= $e$}`

[Lasse Reichstein Nielsen, 2016/11/08 11:42:35]

Done.

+proceeds as follows:
+
+Evaluate $\SUPER.v$ to an object $o$.

[eernst, 2016/11/03 18:07:06]

`\code{\SUPER.$v$}`

Ok, ok, this only changes the font of the period, but it still feels good to
follow a consistent approach. ;-) For instance, if we wish to make concrete
syntax blue then we would get it right just by adapting the definition of
\code{}, if we have been consistent.

[Lasse Reichstein Nielsen, 2016/11/08 11:42:34]

Acknowledged.

+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 $e_1?.v$  {\em ??=} $e_2$

[eernst, 2016/11/03 18:07:04]

`\code{$e_1$?.$v$ ??= $e_2$}`

[Lasse Reichstein Nielsen, 2016/11/08 11:42:35]

Done.

+proceeds as follows:
+
+Evaluate $e_1$ to an object $u$ and let \code{x} be a fresh variable bound to $u$.

[eernst, 2016/11/03 18:07:04]

`$x$`

[Lasse Reichstein Nielsen, 2016/11/08 11:42:33]

Done.

+Evaluate \code{x.$v$} to an object $o$.

[eernst, 2016/11/03 18:07:07]

`\code{$x$.$v$}`

[Lasse Reichstein Nielsen, 2016/11/08 11:42:34]

Done.

+If $o$ is not the null value then $a$ evaluates to $o$.
+Otherwise evaluate \code{x.$v$ = $e_2$} to an object $r$,

[eernst, 2016/11/03 18:07:06]

`\code{$x$.$v$ = $e_2$}`

[Lasse Reichstein Nielsen, 2016/11/08 11:42:36]

Done.

+and then $a$ evaluates to $r$.
+
 % But what about C?.v ??= e
 
 \LMHash{}
@@ -4633,11 +4702,30 @@ 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 $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$.

[eernst, 2016/11/03 18:07:06]

`\code{$v$ $op$= $e$}`, `\code{$v$ = $v$ $op$ $e$}`,
`\code{$C$.$v$ $op$= $e$}`, `\code{$C$.$v$ = $C$.$v$ $op$ $e$}`

[Lasse Reichstein Nielsen, 2016/11/08 11:42:35]

Done.

+
+Evaluation of a compound assignment $a$ of the form $e_1.v$ $op = e_2$ proceeds as follows:

[eernst, 2016/11/03 18:07:05]

`\code{$e_1$.$v$ $op$= $e_2$}`

+Evaluate $e_1$ to an object $u$ and let \code{x} be a fresh variable bound to $u$.

[eernst, 2016/11/03 18:07:06]

`$x$`

[Lasse Reichstein Nielsen, 2016/11/08 11:42:35]

Done.

+Evaluate \code{x.$v$ = x.$v$ $op$ $e_2$} to an object $r$

[eernst, 2016/11/03 18:07:06]

`\code{$x$.$v$ = $x$.$v$ $op$ $e_2$}`

[Lasse Reichstein Nielsen, 2016/11/08 11:42:34]

Done.

+and then $a$ evaluates to $r$.
+
+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 \code{a} and \code{i} be fresh variables bound to $u$ and $v$ respectively.

[eernst, 2016/11/03 18:07:05]

`$a$`, `$i$`

[Lasse Reichstein Nielsen, 2016/11/08 11:42:34]

Done.

+Evaluate \code{a[i] = a[i] $op$ $e_3$} to an object $r$,

[eernst, 2016/11/03 18:07:07]

`\code{$a$[$i$] = $a$[$i$] $op$ $e_3$}`

[Lasse Reichstein Nielsen, 2016/11/08 11:42:34]

Done.

+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/03 18:07:03]

Drop the space before `=`.

[Lasse Reichstein Nielsen, 2016/11/08 11:42:35]

Done.

+
+Evaluate $e_1$ to an object $u$ and let \code{x} be a fresh variable bound to $u$.

[eernst, 2016/11/03 18:07:05]

`$x$`

[Lasse Reichstein Nielsen, 2016/11/08 11:42:36]

Done.

+Evaluate \code{x.$v$} to an object $o$.

[eernst, 2016/11/03 18:07:05]

`\code{$x$.$v$}`

[Lasse Reichstein Nielsen, 2016/11/08 11:42:35]

Done.

+If $o$ is the null value, then $a$ evaluates to the null value.

[eernst, 2016/11/03 18:07:03]

Isn't the question whether $x$ (or $u$) is the null value, not $o$? In that case
the test should go before evaluating \code{$x$.$v$}.

$o$ is just the "before" value that we are going to use on the right hand side
of `=` to compute an "after" value which is than assigned to $x$.$v$.

[Lasse Reichstein Nielsen, 2016/11/08 11:42:34]

Done.

[Lasse Reichstein Nielsen, 2016/11/08 11:42:36]

Ack, true. I was probably still thinking of ??=.
Rewritten (and shorter).

+Otherwise let \code{y} be a fresh variable bound to $o$

[eernst, 2016/11/03 18:07:03]

`$y$`

[Lasse Reichstein Nielsen, 2016/11/08 11:42:36]

Acknowledged.

+and evaluate \code{x.$v$ = t $op$ $e_2$} to an object $r$.

[eernst, 2016/11/03 18:07:07]

`\code{$x$.$v$ = $y$ $op$ $e_2$}`

[Lasse Reichstein Nielsen, 2016/11/08 11:42:34]

Acknowledged.

+Then $a$ evaluates to $r$.
+
+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$.

[eernst, 2016/11/03 18:07:05]

`\code{$e_1$?.$v$ $op$= $e_2$}`, `\code{$e_1$.$v$ $op$ $e_2$}`, `\code{e_1$.$v$
$op$= $e_2$}`, `\code{$e_1$?.$v$ $op$= $e_2$}`.

[Lasse Reichstein Nielsen, 2016/11/08 11:42:35]

Done.

 
 \LMHash{}
 A compound assignment of the form $C?.v$ $op = e_2$ is equivalent to the expression
@@ -4705,7 +4793,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 $e_1??e_2 $

[eernst, 2016/11/03 18:07:03]

`\code{$e_1$ ?? $e_2$}`

[Lasse Reichstein Nielsen, 2016/11/08 11:42:35]

Done.

+proceeds as follows:
+
+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$.
+
+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$.
 
 
 \subsection{ Logical Boolean Expressions}
@@ -5076,7 +5172,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:
+
+Evaluate $v$ to an object $r$ and let \code{t} be a fresh variable bound to $r$.

[eernst, 2016/11/03 18:07:05]

$t$

[Lasse Reichstein Nielsen, 2016/11/08 11:42:36]

Done.

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

[eernst, 2016/11/03 18:07:04]

`\code{$v$ = $y$ + 1}`

[Lasse Reichstein Nielsen, 2016/11/08 11:42:36]

Done.

+Then $e$ evaluates to $r$.
 
 \LMHash{}
 The static type of such an expression is the static type of $v$.
@@ -5086,83 +5186,122 @@ 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$ ++}

[eernst, 2016/11/03 18:07:03]

Drop the space before `++`.

[Lasse Reichstein Nielsen, 2016/11/08 11:42:35]

Done.

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

[eernst, 2016/11/03 18:07:05]

`$y$`

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

[eernst, 2016/11/03 18:07:04]

`\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$.
 
 
 \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$++}
+proceeds as follows:
 
-\code{(x)\{\VAR{} r = x.v; x.v = r + 1; \RETURN{} r\}($e_1$)}.
+Evaluate $e_1$ to an object $u$ and let \code{x} be a fresh variable bound to $u$.

[eernst, 2016/11/03 18:07:05]

`$x$`

+Evaluate \code{x.$v$} to a value $r$ and let \code{y} be a fresh variable bound to $r$.

[eernst, 2016/11/03 18:07:07]

`\code{$x$.$v$}`, `$y$`.

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

[eernst, 2016/11/03 18:07:04]

`\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$.
 
 
 \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]$++}

[eernst, 2016/11/03 18:07:07]

`\code{$e_1$[$e_2$]++}`

+proceeds as follows:
 
-\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 \code{a} and \code{i} be fresh variables bound to $u$ and $v$ respectively.

[eernst, 2016/11/03 18:07:06]

`$a$`, `$i$`

+Evaluate \code{a[i]} to an object $r$ and let $y$ be a fresh variable bound to $r$.

[eernst, 2016/11/03 18:07:02]

`\code{$a$[$i]}`

+Evaluate \code{a[i] = y + 1}.

[eernst, 2016/11/03 18:07:03]

`\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]$.
 
 
 \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:
 
-\code{()\{\VAR{} r = $v$; $v$ = r - 1; \RETURN{} r\}()}.
+Evaluate the expression $v$ to an object $r$ and let \code{y} be a fresh variable bound to $r$.

[eernst, 2016/11/03 18:07:05]

`$y$`

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

[eernst, 2016/11/03 18:07:02]

`\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:
 
-\code{()\{\VAR{} r = $C.v$; $C.v$ = r - 1; \RETURN{} r\}()}.
+Evaluate $C.v$ to a value $r$ and let \code{y} be a fresh variable bound to $r$.

[eernst, 2016/11/03 18:07:05]

`$y$`

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

[eernst, 2016/11/03 18:07:07]

`\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$.
 
 
 \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$-{}-}

[eernst, 2016/11/03 18:07:06]

`\code{$e_1$.$v$-{}-}`

+proceeds as follows:
+
+Evaluate $e_1$ to an object $u$ and let \code{x} be a fresh variable bound to $u$.

[eernst, 2016/11/03 18:07:06]

`$x$`

+Evaluate \code{x.$v$} to a value $r$ and let \code{y} be a fresh variable bound to $r$.

[eernst, 2016/11/03 18:07:05]

`\code{$x$.$v$}`, `$y$`

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

[eernst, 2016/11/03 18:07:03]

`\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$.
 
 
 \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]$-{}-}

[eernst, 2016/11/03 18:07:03]

`\code{$e_1$[$e_2$]-{}-}`

+proceeds as follows:
 
-\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 \code{a} and \code{i} be fresh variables bound to $u$ and $v$ respectively.

[eernst, 2016/11/03 18:07:03]

`$a$`, `$i$`

+Evaluate \code{a[i]} to an object $r$ and let $y$ be a fresh variable bound to $r$.

[eernst, 2016/11/03 18:07:06]

`\code{$a$[$i$]}`

+Evaluate \code{a[i] = y - 1}.

[eernst, 2016/11/03 18:07:05]

`\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]$.
 
 \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$++}

[eernst, 2016/11/03 18:07:06]

`\code{$e_1$?.$v$++}`

+where $e_1$ is not a type literal, proceeds as follows:
 
-\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$++}
-.
+Evaluate $e_1$ to an object $u$ and let \code{x} be a fresh variable bound to $u$.

[eernst, 2016/11/03 18:07:04]

`$x$`

[Lasse Reichstein Nielsen, 2016/11/08 11:42:36]

All the above comments: done.

+Evaluate \code{u.$v$} to an object $o$.

[eernst, 2016/11/03 18:07:04]

`\code{$x$.$v$}` (if we can evaluate $u$.$v$ then there is no reason to
introduce $x$)

But I'd expect a check on $u$, and a bail out if it's null.

Checking on $o$ instead could also be useful in some cases, but in that case it
would be inconsistent to have the `?` right after `e_1`, where it usually means
"is this receiver null?". For a check on the member $v$ we could introduce
support for having the `?` elsewhere, maybe `e_1.v?++`, but I'd assume that this
wouldn't be worthwhile.

[Lasse Reichstein Nielsen, 2016/11/08 11:42:36]

ack, same bug. Fixed.

+If $o$ is the null value, then $e$ evaluates to the null value.

[eernst, 2016/11/03 18:07:07]

This test may then be moved up before computing $x$.$v$, and checking on $u$
rather than $o$.

[Lasse Reichstein Nielsen, 2016/11/08 11:42:36]

Acknowledged.

+Otherwise let $y$ be a fresh variable bound to $o$
+and evaluate \code{u.$v$ = y + 1}.

[eernst, 2016/11/03 18:07:05]

`\code{$x$.$v$ = $y$ + 1}`

[Lasse Reichstein Nielsen, 2016/11/08 11:42:35]

Rewritten to just evaluate \code{$x$.$v$++}.

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

[eernst, 2016/11/03 18:07:06]

This also motivates a test on $u$ rather than $o$: It's the type literal that
can't be null, not the static field $v$.

 
 \LMHash{}
 The static type of such an expression is the static type of $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$-{}-}

[eernst, 2016/11/03 18:07:04]

`\code{$e_1$?.$v$-{}-}`

[Lasse Reichstein Nielsen, 2016/11/08 11:42:34]

-- case fixed the same way as ++.

+where $e_1$ is not a type literal, proceeds as follows:
 
-\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$-{}-}
-.
+Evaluate $e_1$ to an object $u$ and let \code{x} be a fresh variable bound to $u$.

[eernst, 2016/11/03 18:07:04]

`$x$`

+Evaluate \code{u.$v$} to an object $o$.

[eernst, 2016/11/03 18:07:03]

`\code{$x$.$v$}`

+If $o$ is the null value, then $e$ evaluates to the null value.
+Otherwise let $y$ be a fresh variable bound to $o$
+and evaluate \code{u.$v$ = y - 1}.

[eernst, 2016/11/03 18:07:04]

`\code{$x$.$v$ = $y$ - 1}`

+Then $e$ evaluates to $o$.
+
+If $e_1$ is a type literal, $e$ is equivalent to \code{$e_1$.$v$-{}-}.
 
 \LMHash{}
 The static type of such an expression is the static type of $e_1.v$.
@@ -5433,6 +5572,46 @@ In all other cases,  a \code{CastError} is thrown.
 \LMHash{}
 The static type of a cast expression  \code{$e$ \AS{} $T$}  is $T$.
 
+\subsection{ Let}
+\LMLabel{let}
+
+\LMHash{}
+The {\em let expression} evaluates two expressions and allows the second expression to refer to the value of the first.
+
+The let expression is not expressible in the concrete grammar of the Dart language. It cannot be used in a Dart program.
+It is instead a synthetic construct used internally
+in the language specification for rewriting other expressions.
+
+\begin{grammar}
+{\bf letExpression: }
+`let' $identifier$ `=' $expression$ `in' $expression$;
+\end{grammar}
+
+A let expression $e$ on the form \code{let $v$ = $e_1$ in $e_2$}
+introduces a new scope, which is nested in the lexically enclosing scope in which the let expression is evaluated.
+The new scope introduces a final local variable $v$, and it covers only $e_2$,
+not $e_1$.
+
+The static type of $v$ is the same as the static type of $e_1$.
+
+Evaluation of $e$ proceeds as follows:
+
+First $e_1$ is evaluated to a value $o_1$.
+Then $v$ is bound to $o_1$ in the new scope,
+and $e_2$ is evaluated to a value $o_2$ in this scope.
+The evaluation of $e$ produces the value $o_2$.
+
+\commentary{
+The syntax for the let expression is abstract, so it doesn't matter that
+\code{let} is not a reserved word.
+}
+
+\commentary{
+Before introducing asynchronous functions to the Dart language, an expression on the form \code{((v) => e2)(e1)} would be equivalent to a let expression,
+and that was the rewrite used for, e.g., the logical and operator
+(\ref{logicalBooleanExpressions}).
+In an asynchronous function that rewrite is no longer correct because it moves \code{e2} into a non-synchronous function. If \code{e2} contains an await statement, the result will be an invalid expression.
+}

[eernst, 2016/11/03 18:07:07]

Wouldn't this whole section be unused at this point?

[Lasse Reichstein Nielsen, 2016/11/08 11:42:34]

Absolutely. I thought I removed it. One undo too many!

 
 \section{Statements}
 \LMLabel{statements}
@@ -5569,7 +5748,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/03 18:07:05]

Just keep `=$>$`

[Lasse Reichstein Nielsen, 2016/11/08 11:42:36]

OK, but not consistent with the following lines.
We should make a \=> macro (\arr?)

There is a macro for \> - could we just write =\> ?

 top() \{ // another top level function
   f(3); // illegal
   f(x) $=>$ x $>$ 0? x*f(x-1): 1;  // recursion is legal
@@ -6162,7 +6341,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: