%!TEX root = main.tex

\section{Syntax}

\subsection*{Identifiers}

$$
\begin{array}{@{}lrcl@{\qquad}l}
\text{(identifier)} & \x{id} &::=&
  \dots \\
\end{array}
$$


\subsection*{Types}

$$
\begin{array}{@{}lrcl@{\qquad}l}
\text{(type)} & \x{typ} &::=&
  \x{id}~\x{typ-args}
    & \text{constructor} \\&&|&
  \KK{actor}^? \K\{~\x{typ-fields}~\K\}
    & \text{object} \\&&|&
  \KK{var}^? \x{typ}~\K[~\K]
    & \text{array} \\&&|&
  \x{typ}~\K?
    & \text{option} \\&&|&
 \KK{class}^?  \x{typ-params} \x{typ} \Kto \x{typ}
    & \text{function} \\&&|&
  \KK{async}~\x{typ}
    & \text{future} \\&&|&
  \K(~( (\x{id}~\K:)^? \x{typ})\K,^\ast~\K)
    & \text{tuple} \\
[1ex]
\text{(type fields)} & \x{typ-fields} &::=&
  \KK{var}^? \x{id}~\K:~\x{typ}
    & \text{field} \\&&|&
  \x{id}~\x{typ-params}~\x{exp-params}~\K:~\x{typ}
    & \text{function field} \\&&|&
  \x{typ-fields}~\K;~\x{typ-fields}
    & \text{composition} \\
[1ex]
\text{(type parameters)} & \x{typ-params} &::=&
  (\Klt~(\x{id}~(\Ksub \x{typ})^?)\K,^\ast~\Kgt)^? \\
[1ex]
\text{(type arguments)} & \x{typ-args} &::=&
  (\Klt~\x{typ}\K,^\ast~\Kgt)^? \\
\end{array}
$$

\subsubsection*{Desugaring}

$$
\begin{array}{@{}lrcl@{}}
\text{(type)} &
\K( \dots \K, \x{id} \K: \x{typ} \K, \dots \K) &:=&
  \K( \dots \K, \x{typ} \K, \dots \K) \\
[1ex]
\text{(type field)} &
\x{id} \x{typ-params} \x{exp-params} \K: \x{typ} &:=&
  \x{id} \K: \x{typ-params} \x{exp-params} \Kto \x{typ} \\
[1ex]
\text{(type parameters)} &
\Klt \dots \K, \x{id} \K, \dots \Kgt &:=&
  \Klt \dots \K, \x{id} \Ksub \K{Any} \K, \dots \Kgt \\&
\epsilon &:=&
  \Klt \Kgt \\
\text{(type arguments)} &
\epsilon &:=&
  \Klt \Kgt \\
\end{array}
$$


\subsection*{Expressions}

$$
\begin{array}{@{}lrcl@{\qquad}l}
\text{(literal)} & \x{lit} &::=&
  \x{nat}
    & \text{natural number} \\&&|&
  \x{float}
    & \text{floating-point number} \\&&|&
  \x{char}
    & \text{unicode character} \\&&|&
  \x{text}
    & \text{unicode text string} \\
[2ex]
\text{(unary operators)} & \x{unop} &:=&
  \K{+} ~|~ \K\textendash ~|~ \K{\^{}} \\
[1ex]
%\text{(count operators)} & \x{cntop} &:=&
%  \K{++} ~|~ \K{\textendash\,\textendash} \\
%[1ex]
\text{(binary operators)} & \x{binop} &:=&
  \K{+} ~|~ \K\textendash ~|~ \K{*} ~|~ \K{/} ~|~ \K{\%} \\&&|&
  \K{\&} ~|~ \;\K\textbar\; ~|~ \K{\^{}} ~|~ \Klt\Klt ~|~ \Kgt\Kgt ~|~ \K{+}\Kgt\Kgt ~|~ \Klt\Klt\Kgt ~|~ \Klt\Kgt\Kgt \\
[1ex]
\text{(relational operators)} & \x{relop} &:=&
  \K= ~|~ \K{!=} ~|~ \Klt ~|~ \Kgt ~|~ {\Klt}{\K=} ~|~ {\Kgt}{\K=} \\
\end{array}
$$

$$
\begin{array}{@{}lrcl@{\qquad}l}
\text{(expression)} & \x{exp} &::=&
  \x{lit}
    & \text{literal} \\&&|&
  \x{id}
    & \text{variable} \\&&|&
  \x{unop}~\x{exp}
    & \text{unary operation} \\&&|&
  \x{exp}~\x{binop}~\x{exp}
    & \text{binary operation} \\&&|&
  \x{exp}~\x{relop}~\x{exp}
    & \text{relational operation} \\&&|&
  \x{exp}~\K?
    & \text{option} \\&&|&
  \K(~\x{exp}\K,^\ast~\K)
    & \text{tuple} \\&&|&
  \x{exp}~\K.~\x{nat}
    & \text{tuple projection} \\&&|&
  \KK{actor}^? \K\{~\x{exp-fields}~\K\}
    & \text{object} \\&&|&
  \x{exp}~\K.~\x{id}
    & \text{object projection} \\&&|&
  \x{exp}~\K{:=}~\K{exp}
    & \text{assignment} \\&&|&
%  \x{cntop}~\x{exp}
%    & \text{count update} \\&&|&
  \x{unop}{\!\K=}~\x{exp}
    & \text{unary update} \\&&|&
  \x{exp}~\x{binop}{\!\K=}~\x{exp}
    & \text{binary update} \\&&|&
  \K[~\void{\KK{var}^?} \x{exp}\K,^\ast~\K]
    & \text{array} \\&&|&
  \x{exp}~\K[~\x{exp}~\K]
    & \text{array indexing} \\&&|&
  \x{exp}~\x{typ-args}~\x{exp}
    & \text{function call} \\&&|&
  \KK{not}~\x{exp}
    & \text{negation} \\&&|&
  \x{exp}~\KK{and}~\x{exp}
    & \text{conjunction} \\&&|&
  \x{exp}~\KK{or}~\x{exp}
    & \text{disjunction} \\&&|&
  \KK{if}~\x{exp}~\x{exp}~(\KK{else}~\x{exp})^?
    & \text{conditional} \\&&|&
  \KK{switch}~\x{exp}~\K\{~(\KK{case}~\x{pat}~\x{exp})\K;^\ast~\K\}
    & \text{pattern match} \\&&|&
  \KK{while}~\x{exp}~\x{exp}
    & \text{guarded loop} \\&&|&
  \KK{loop}~\x{exp}~(\KK{while}~\x{exp})^?
    & \text{unconditional loop} \\&&|&
  \KK{for}~\K(~\x{pat}~\KK{in}~\x{exp}~\K)~\x{exp}
    & \text{iteration} \\&&|&
  \KK{label}~\x{id}~(\K:~\x{typ})^?~\x{exp}
    & \text{label} \\&&|&
  \KK{break}~\x{id}~\x{exp}^?
    & \text{break} \\&&|&
  \KK{continue}~\x{id}
    & \text{continue} \\&&|&
  \KK{return}~\x{exp}^?
    & \text{return} \\&&|&
  \KK{async}~\x{exp}
    & \text{future} \\&&|&
  \KK{await}~\x{exp}
    & \text{future synchronisation} \\&&|&
  \KK{assert}~\x{exp}
    & \text{assertion} \\&&|&
  \x{exp}~\KK{is}~\x{exp}
    & \text{instance check} \\&&|&
  \x{exp}~\K:~\x{typ}
    & \text{type annotatione} \\&&|&
  \x{exp}~\K;~\x{exp}
    & \text{sequence} \\&&|&
  \K\{~\x{dec}\K;^\ast~\K\}
    & \text{block} \\&&|&
  \x{dec}
    & \text{declaration} \\
[1ex]
\text{(expression fields)} & \x{exp-fields} &::=&
  \KK{private}^? \KK{var}^? \x{id}~(\K:~\x{typ})^?~\K=~\x{exp}
    & \text{field} \\&&|&
  \KK{private}^? \x{id}~\x{typ-params}~\x{exp-params}~(\K:~\x{typ})^?~\K=^?~\x{exp}
    & \text{function field} \\&&|&
  \x{exp-fields}~\K;~\x{exp-fields}
    & \text{composition} \\
[1ex]
\text{(expression parameters)} & \x{exp-params} &::=&
  \K(~(\x{id}~\K:~\x{typ})\K,^\ast~\K) \\
\end{array}
$$

\subsubsection*{Desugaring}

$$
\begin{array}{@{}lrcl@{}}
\text{(expression)} &
\K\{ \K\} &:=&
  \K\{ \K{()} \K\} \\&
\KK{if} \x{exp}_1 \x{exp}_2 &:=&
  \KK{if} \x{exp}_1 \x{exp}_2 \K{()} \\&
\KK{loop} \x{exp} &:=&
  \KK{loop} \x{exp}_1 \KK{while} \; \K{true} \\&
\KK{label} \x{id} \x{exp} &:=&
  \KK{label} \x{id} \K: \x{typ} \x{exp} \\&
\KK{label} \x{id} \KK{while} \x{exp}_1 \x{exp}_2 &:=&
  \KK{label} \x{id} \KK{while} \x{exp}_1 (\KK{label} \x{id}_{\K{continue}} \x{exp}_2) \\&
\KK{label} \x{id} \KK{loop} \x{exp}_1 \KK{while} \x{exp}_2 &:=&
  \KK{label} \x{id} \KK{loop} \, (\KK{label} \x{id}_{\K{continue}} \x{exp}_1) \, \KK{while} \x{exp}_2 \\&
\KK{label} \x{id} \KK{for} \x{id} \KK{in} \x{exp}_1 \x{exp}_2 &:=&
  \KK{label} \x{id} \KK{for} \x{id} \KK{in} \x{exp}_1 (\KK{label} \x{id}_{\K{continue}} \x{exp}_2) \\&
\KK{break} \x{id} &:=&
  \KK{break} \x{id} \K{()} \\&
\KK{continue} \x{id} &:=&
  \KK{break} \x{id}_{\K{continue}} \K{()} \\&
\KK{return} &:=&
  \KK{return} \, \K{()} \\
\end{array}
$$
$$
\begin{array}{@{}rcl@{}}
\text{(expression field)} \hfill \\
\KK{private}^? \KK{var}^? \x{id} \K: \x{typ} \K= \x{exp} &:=&
  \KK{private}^? \KK{var}^? \x{id} \K= \x{exp} \K: \x{typ} \\
\KK{private}^? \x{id} \x{typ-params} \x{exp-params} \, (\K: \x{typ})^? \K= \x{exp} &:=&
  \KK{private}^? \x{id} \K= \, \KK{func} \x{id} \x{typ-params} \x{exp-params} \, (\K: \x{typ})^? \K= \x{exp} \\
\end{array}
$$


\subsection*{Patterns}

$$
\begin{array}{@{}lrcl@{\qquad}l}
\text{(pattern)} & \x{pat} &::=&
  \K\textunderscore
    & \text{wildcard} \\&&|&
  \x{id}
    & \text{variable} \\&&|&
  \x{lit}
    & \text{literal} \\&&|&
  \x{unop}~\x{lit}
    & \text{modified literal} \\&&|&
  \x{pat}~\K?
    & \text{option} \\&&|&
  \K(~\x{pat}\K,^\ast~\K)
    & \text{tuple} \\&&|&
  \x{pat}~\K:~\x{typ}
    & \text{type annotation} \\
\end{array}
$$


\subsection*{Declarations}

$$
\begin{array}{@{}lrcl@{\qquad}l}
\text{(declarations)} & \x{dec} &::=&
  \x{exp}
    & \text{expression} \\&&|&
  \KK{let}~\x{pat}~\K=~\x{exp}
    & \text{immutable} \\&&|&
  \KK{var}~\x{id}~(\K:~\x{typ})^?~\K=~\x{exp}
    & \text{mutable} \\&&|&
  \KK{async}^?\, \KK{func}~\x{id}^? \x{typ-params}~\x{exp-params}~(\K:~\x{typ})^?~\K=^?~\x{exp}
    & \text{function} \\&&|&
  \KK{actor}^?\, \KK{class}~\x{id}^? \x{typ-params}~\x{exp-params}~\K=^?~\K\{~\x{exp-fields}~\K\}
    & \text{class} \\&&|&
  \KK{type}~\x{id}~\x{typ-params}~\K=~\x{typ}
    & \text{type} \\%&&|&
%  \x{dec}~\K;~\x{dec} 
%    & \text{sequencing} \\
\end{array}
$$

\subsubsection*{Desugaring}

$$
\begin{array}{@{}rcl@{}}
\text{(declaration)} \hfill \\
\KK{let} \x{pat} \K: \x{typ} \K= \x{exp} &:=&
  \KK{let} \x{pat} \K= \x{exp} \K: \x{typ} \\
\KK{var} \x{id} \K: \x{typ} \K= \x{exp} &:=&
  \KK{var} \x{id} \K= \x{exp} \K: \x{typ} \\
\KK{func} \x{id}^? \x{typ-params} \x{exp-params} \K= \x{exp} &:=&
  \KK{func} \x{id}^? \x{typ-params} \x{exp-params} \K: \, \K{()} \, \K= \x{exp} \\
\KK{async} \, \KK{func} \x{id}^? \x{typ-params} \x{exp-params} (\K: \x{typ})^? \K= \x{exp} &:=&
\KK{func} \x{id}^? \x{typ-params} \x{exp-params} \, (\K: \, \KK{async} \x{typ})^? \K= \, \KK{async} \x{exp} \\
\end{array}
$$


\subsection*{Programs}

$$
\begin{array}{@{}lrcl@{\qquad}l}
\text{(program)} & \x{prog} &::=&
  \x{dec}\K;^\ast
\end{array}
$$
