Spec: Rewrite lambdas to simpler semantics instead.

docs/language/dartLangSpec.tex

 \documentclass{article}
 \usepackage{epsfig}
 \usepackage{color}
 \usepackage{dart}
 \usepackage{bnf}
 \usepackage{hyperref}
 \usepackage{lmodern}
 \newcommand{\code}[1]{{\sf #1}}
 \title{Dart Programming Language  Specification  \\
 {4th edition draft}\\
@@ skipping 910 matching lines @@
 It is a compile-time error if a class has an instance member and a static member  with the same name.
 % It is a compile-time error if a generic (\ref{generics}) class declares a member with the same name as one of its type parameters.
 
 \commentary{Here are simple examples, that illustrate the difference between ``has a member'' and ``declares a member''. For example, \code{B} {\em declares} one member named \code{f}, but {\em has} two such members. The rules of inheritance determine what members a class has.
 }
 
 \begin{dartCode}
 \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 \{
   int i = 1; //  getter i and setter i= override versions from A
   \STATIC{} j; // compile-time error: static getter \& setter conflict with
   //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}
 
 \LMHash{}
 It is a compile time error if a class $C$ declares a member with the same name as $C$. It is a compile time error if a generic class declares a type variable with the same name as the class or any of its members or constructors.
 
 \subsection{Instance Methods}
 \LMLabel{instanceMethods}
 
 \LMHash{}
@@ skipping 2870 matching lines @@
 \LMHash{}
 An ordinary method invocation can be {\em conditional} or {\em unconditional}.
 
 \LMHash{}
 Evaluation of a {\em conditional ordinary method invocation} $e$ of the form
 
 \LMHash{}
 $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})$.
 
 \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})$.
 
 \LMHash{}
@@ skipping 86 matching lines @@
 {\bf cascadeSection:}
       `{\escapegrammar ..}' (cascadeSelector arguments*) (assignableSelector arguments*)* (assignmentOperator expressionWithoutCascade)?
       .
 
 {\bf cascadeSelector:}`['  expression `]';
       identifier
       .
 \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}.
 }
 
 \subsubsection{Super Invocation}
 \LMLabel{superInvocation}
 
 \LMHash{}
 A super method invocation $i$ has the form
 
@@ skipping 70 matching lines @@
 
 
 \commentary{Closures derived from members via closurization are colloquially known as tear-offs}
 
 Property extraction can be either {\em conditional} or {\em unconditional}.
 
 \rationale {
 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$.
 
 \LMHash{}
 Unconditional property extraction takes several syntactic forms: $e.m$ (\ref{getterAccessAndMethodExtraction}), $\SUPER.m$ (\ref{superGetterAccessAndMethodClosurization}), $e\#m$ (\ref{generalClosurization}), $\NEW{}$ $T\#m$ (\ref{namedConstructorExtraction}), $\NEW{}$ $T\#$ (\ref{anonymousConstructorExtraction}) and $\SUPER\#m$ (\ref{generalSuperPropertyExtraction}), where $e$ is an expression, $m$ is an identifier optionally followed by an equal sign and $T$ is a type.
 
 \subsubsection{Getter Access and Method Extraction}
 \LMLabel{getterAccessAndMethodExtraction}
 
 \LMHash{}
@@ skipping 423 matching lines @@
 \LMHash{}
 Otherwise, the assignment is equivalent to the assignment \code{ \THIS{}.$v$ = $e$}.
 
 \LMHash{}
 In checked mode, it is a dynamic type error if $o$ is not \NULL{} and the interface of the class of $o$ is not a subtype of the actual type (\ref{actualTypeOfADeclaration}) of $v$.
 
 \LMHash{}
 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:
 
 \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$.
 
 \LMHash{}
 If the setter lookup has failed, then a new instance $im$  of the predefined class  \code{Invocation}  is created, such that :
 \begin{itemize}
 \item  \code{im.isSetter} evaluates to \code{\TRUE{}}.
@@ skipping 67 matching lines @@
 
 \LMHash{}
 It is a static type warning if the static type of $e$ may not be assigned to the static type of the formal parameter of the setter $v=$.   The static type of the expression $\SUPER.v$ \code{=} $e$ is the static type of $e$.
 
 
 
 
 
 
 \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.
 
 \LMHash{}
 It is a static warning if an assignment of the form $v = e$ occurs inside a top level or static function (be it function, method, getter, or setter) or variable initializer and there is neither a local variable declaration with name $v$  nor setter declaration with name $v=$ in the lexical scope enclosing the assignment.
 
 \LMHash{}
 It is a compile-time error to invoke any of the setters of class \cd{Object} on a prefix object (\ref{imports}) or on a constant type literal that is  immediately followed by the token `.'.
 
 
 
 \subsubsection{Compound Assignment}
 \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{}
 A compound assignment of the form $C?.v$  {\em ??=} $e_2$ is equivalent to the expression $C.v$ {\em ??=} $e$.
 
 \LMHash{}
 The static type of a compound assignment of the form $v$ {\em ??=} $e$ is the least upper bound of the static type of $v$ and the static type of $e$.  Exactly the same static warnings that would be caused by $v = e$ are also generated in the case of $v$ {\em ??=} $e$.
 
 
 \LMHash{}
 The static type of a compound assignment of the form  $C.v$ {\em ??=} $e$  is the least upper bound of the static type of $C.v$ and the static type of $e$.  Exactly the same static warnings that would be caused by $C.v = e$ are also generated in the case of $C.v$ {\em ??=} $e$.
 
 \LMHash{}
 The static type of a compound assignment of the form $e_1.v$  {\em ??=} $e_2$ is the least upper bound of the static type of $e_1.v$ and the static type of $e_2$. Let $T$ be the static type of $e_1$ and let $z$ be a fresh variable of type $T$. Exactly the same static warnings that would be caused by $z.v = e_2$ are also generated in the case of $e_1.v$  {\em ??=} $e_2$.
 
 \LMHash{}
 The static type of a compound assignment of the form $e_1[e_2]$  {\em ??=} $e_3$  is the least upper bound of the static type of $e_1[e_2]$ and the static type of $e_3$. Exactly the same static warnings that would be caused by $e_1[e_2] = e_3$ are also generated in the case of $e_1[e_2]$  {\em ??=} $e_3$.
 
 \LMHash{}
 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
 $C.v$ $op = e_2$.
 
 \begin{grammar}
 {\bf compoundAssignmentOperator:}`*=';
       `/=';
       `\~{}/=';
       `\%=';
@@ skipping 47 matching lines @@
 
  \LMHash{}
  An {\em if-null expression}evaluates an expression and if the result is \NULL, evaluates another.
 
 \begin{grammar}
 {\bf ifNullExpression:}
   logicalOrExpression (`??' logicalOrExpression)*
 \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}
 \LMLabel{logicalBooleanExpressions}
 
 \LMHash{}
 The logical boolean expressions combine boolean objects using the boolean conjunction and disjunction operators.
 
 \begin{grammar}
 {\bf logicalOrExpression:}
@@ skipping 350 matching lines @@
 {\bf incrementOperator:}`++';
       `-{}-'
     .
 
  \end{grammar}
 
 \LMHash{}
  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$.
 
 
 \rationale{The above ensures that if $v$ is a field, the getter gets called exactly once. Likewise in the cases below.
 }
 
 \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:
 
-\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: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$.
+
 
 \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$.
 
 
 \subsection{ Assignable Expressions}
 \LMLabel{assignableExpressions}
 
 \LMHash{}
 Assignable expressions are expressions that can appear on the left hand side of an assignment.
@@ skipping 250 matching lines @@
 \LMHash{}
  Evaluation of the cast expression \code{$e$ \AS{} $T$} proceeds as follows:
 
 \LMHash{}
 The expression $e$ is evaluated to a value $v$. Then, if $T$ is a malformed or deferred type (\ref{staticTypes}), a dynamic error occurs. Otherwise, if the interface of the class of $v$ is a subtype of $T$, the cast expression evaluates to $v$. Otherwise, if $v$ is \NULL{}, the cast expression evaluates to $v$.
 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}
 
  \begin{grammar}
 {\bf statements:}
       statement*
     .
 
 
@@ skipping 116 matching lines @@
  \end{grammar}
 
 \LMHash{}
 A function declaration statement of one of the forms $id$ $signature$ $\{ statements \}$ or $T$ $id$ $signature$ $\{ statements \}$ causes a new function named $id$ to be added to the innermost enclosing scope. It is a compile-time error to reference a local function before its declaration.
 
 
 \commentary{ This implies that local functions can be directly recursive, but not mutually recursive. Consider these examples:
 }
 
 \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
   g1(x) $=>$ h(x, 1); // error: h is not declared yet
   h(x, n) $=>$ x $>$ 1? h(x-1, n*x): n; // again, recursion is fine
   g2(x) $=>$ h(x, 1); // legal
 
   p1(x) $=>$ q(x,x); // illegal
   q1(a, b)$ =>$ a $>$ 0 ? p1(a-1): b; // fine
 
@@ skipping 572 matching lines @@
 \begin{itemize}
 \item
  if there is a dynamically enclosing error handler $g$ defined by a \FINALLY{} clause in $m$, control is transferred to $g$.
  \item
 Otherwise $m$ terminates.
 \end{itemize}
 
 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:
 
 \LMHash{}
 Let $x$ be the current exception and let $t$ be the active stack trace. Then the current exception and the active stack trace both become undefined. The statement $s$ is executed. Then, if $x$ is defined,  it is rethrown as if by a rethrow statement (\ref{rethrow}) enclosed in a \CATCH{} clause of the form \code{\CATCH{} ($v_x$, $v_t$)} where $v_x$ and $v_t$ are fresh variables bound to $x$ and $t$ respectively.
 
 
 \LMHash{}
 Execution of a try statement of the form \code{\TRY{} $s_1$ $on-catch_1 \ldots on-catch_n$ \FINALLY{} $s_f$;}  proceeds as follows:
@@ skipping 1736 matching lines @@
 
 The invariant that each normative paragraph is associated with a line
 containing the text \LMHash{} should be maintained.  Extra occurrences
 of \LMHash{} can be added if needed, e.g., in order to make
 individual \item{}s in itemized lists addressable.  Each \LM.. command
 must occur on a separate line.  \LMHash{} must occur immediately
 before the associated paragraph, and \LMLabel must occur immediately
 after the associated \section{}, \subsection{} etc.
 
 ----------------------------------------------------------------------