Merge pull request herd#1602 from herd/aslspec-phase7

[aslspec] phase7: expressions

Author: Roman-Manevich

asllib/doc/ASLFormal.tex

@@ -357,7 +357,7 @@ \subsection{Lists}
 \]
 \end{definition}
 \hypertarget{operator-listcombine}{} % DO NOT LINT
-As a shorthand, we use the notation $a \listcombine b = c$ for $\unziplist(c) = (a, b)$.
+As a shorthand, we use the notation $\listcombine{a}{b} = c$ for $\unziplist(c) = (a, b)$.
 
 \hypertarget{def-unziplistthree}{}
 \begin{definition}[Unzipping a List of Triples]
@@ -373,6 +373,8 @@ \subsection{Lists}
   \end{cases}
 \]
 \end{definition}
+\hypertarget{operator-listcombinethree}{} % DO NOT LINT
+As a shorthand, we use the notation $\listcombinethree{a}{b}{c} = d$ for $\unziplistthree(d) = (a, b, c)$.
 
 \hypertarget{def-uniquelist}{}
 \hypertarget{def-uniquep}{}
@@ -396,6 +398,16 @@ \subsection{Lists}
 \]
 \end{definition}
 
+\begin{definition}[Finding a Value in a List of Pairs]
+\hypertarget{operator-assocopt}{}
+The function
+\[
+  \assocopt{\overname{\KleeneStar{(\Identifier\times T)}}{\vli}}{\overname{\Identifier}{\id}} \aslto \Option{\overname{T}{\vv}}
+\]
+returns $\some{\vv}$ for the first pair $(\id, \vv)$ in the list of pairs $\vli$,
+or $\None$ if no such pair exists.
+\end{definition}
+
 \begin{definition}[Taking the union of a list of sets]
 The parametric function
 \hypertarget{def-unionlist}{}
@@ -409,8 +421,8 @@ \subsection{Lists}
 \end{definition}
 
 \subsection{Strings}
-\hypertarget{def-stringconcat}{}
-The function $\stringconcat : \Strings \times \Strings \rightarrow \Strings$
+\hypertarget{operator-stringconcat}{}
+The function $\concatstrings : \Strings \times \Strings \rightarrow \Strings$
 concatenates two strings.
 
 \hypertarget{def-stringofnat}{}

asllib/doc/ASLRefBET0ChangeLog.tex

@@ -23,7 +23,8 @@ \subsection{ASL-796: introduce \texttt{readonly} and \texttt{pure} keywords}
 A subprogram marked \texttt{readonly} or \texttt{pure} identifies a \readonlyterm{} or \pureterm{} subprogram respectively.
 These have the following behaviour:
 \begin{itemize}
-  \item A \readonlyterm{} subprogram does not modify global storage elements or throw exceptions, but can read global storage elements and use non-determinism ($\ARBITRARY$).
+  \item A \readonlyterm{} subprogram does not modify global storage elements or throw exceptions, but can read global storage elements
+    and use non-determinism\\ ($\ARBITRARY$).
     It can only call read-only or pure subprograms.
   \item A \pureterm{} subprogram does not read or modify global storage elements, throw exceptions, or use non-determinism. It can only call pure subprograms. It can therefore be considered read-only too.
   \item Both pure and read-only subprograms may use assertions (including asserting type conversions), or cause \dynamicerrorsterm{} (e.g.\ divide by zero, calling the \unreachablestatementterm{}, etc.).

asllib/doc/ASLmacros.tex

@@ -383,6 +383,18 @@
 \newcommand\notmember[0]{\mathrel{\not\in}} % DO NOT LINT
 \newcommand\unionlist[0]{\hyperlink{def-unionlist}{\textfunc{union\_list}}}
 \newcommand\UNIONLIST[1]{\unionlist\left({#1}\right)} % A union of a list of sets
+\newcommand\assocopt[3][H]{% DO NOT LINT
+  \ifnum\pdfstrcmp{#1}{H}=0\relax
+    \hyperlink{operator-assocopt}{\textfunc{assoc\_opt}}({#2}, {#3})
+  \else
+    \hyperlink{operator-assocopt}{\textfunc{assoc\_opt}}
+    \left(\begin{array}{l}
+    ({#2},\\
+    {#3})\\
+    \end{array}\right)
+  \fi
+}
+\newcommand\assocoptname[0]{\hyperlink{operator-assocopt}{\textfunc{assoc\_opt}}} % DO NOT LINT
 
 \newcommand\intplus[0]{\mathbin{+}} % DO NOT LINT
 \newcommand\intminus[0]{\mathbin{-}} % DO NOT LINT
@@ -403,7 +415,29 @@
 \newcommand\concat[0]{\hyperlink{operator-concat}{\mathbin{+}}}
 \newcommand\concatlist[1]{\hyperlink{operator-concatlist}{\textfunc{concat\_list}}(#1)}
 \newcommand\cons[0]{\hyperlink{operator-cons}{\mathbin{{+}{+}}}}
-\newcommand\listcombine[0]{\hyperlink{operator-listcombine}{\times}} % DO NOT LINT
+\newcommand\listcombine[3][H]{ % DO NOT LINT
+  \ifnum\pdfstrcmp{#1}{H}=0\relax
+    {#2} \mathbin{\hyperlink{operator-listcombine}{\times}} {#3} % DO NOT LINT
+  \else
+    \hyperlink{operator-listcombine}{\textfunc{list\_combine}} % DO NOT LINT
+    \left(\begin{array}{l}
+    {#2} \hyperlink{operator-listcombine}{\times}\\ % DO NOT LINT
+    {#3}\\
+    \end{array}\right)
+  \fi
+}
+\newcommand\listcombinethree[4][H]{ % DO NOT LINT
+  \ifnum\pdfstrcmp{#1}{H}=0\relax
+    {#2} \mathbin{\hyperlink{operator-listcombinethree}{\times_3}} {#3} \mathbin{\hyperlink{operator-listcombinethree}{\times_3}} {#4} % DO NOT LINT
+  \else
+    \hyperlink{operator-listcombinethree}{\textfunc{list\_combine\_3}} % DO NOT LINT
+    \left(\begin{array}{l}
+    {#2} \hyperlink{operator-listcombinethree}{\times_3}\\ % DO NOT LINT
+    {#3} \hyperlink{operator-listcombinethree}{\times_3}\\ % DO NOT LINT
+    {#4}\\
+    \end{array}\right)
+  \fi
+}
 
 \newcommand\parallelcomp[0]{\hyperlink{def-parallel}{\mathbin{\parallel}}}
 \newcommand\ordered[3]{{#1}\hyperlink{def-ordered}{\xrightarrow{#2}}{#3}}
@@ -416,6 +450,10 @@
 \newcommand\withgraph[3][H]{ {#2}(\hyperlink{operator-withgraph}{\textfunc{graph}}\mapsto{#3}) } % NO_SPECIFICATION_REQUIRED
 \newcommand\withenviron[3][H]{ {#2}(\hyperlink{def-withenviron}{\textfunc{environ}}\mapsto{#3}) } % NO_SPECIFICATION_REQUIRED
 
+\newcommand\concatstrings[0]{\hyperlink{operator-stringconcat}{\mathbin{+}}}
+\newcommand\decimaltolitname[0]{\hyperlink{operator-decimaltolit}{\textfunc{dec\_to\_lit}}} % NO_SPECIFICATION_REQUIRED
+\newcommand\decimaltolit[1]{\decimaltolitname\left(#1\right)} % NO_SPECIFICATION_REQUIRED
+
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \newcommand\overname[2]{\overbrace{#1}^{#2}}
@@ -439,7 +477,6 @@
 \newcommand\uniquelist[0]{\hyperlink{def-uniquelist}{\textfunc{unique}}}
 \newcommand\listset[0]{\hyperlink{def-listset}{\textfunc{list\_set}}}
 \newcommand\listprefix[0]{\hyperlink{def-listprefix}{\textfunc{prefix}}}
-\newcommand\stringconcat[0]{\hyperlink{def-stringconcat}{\texttt{+}}}
 \newcommand\stringofnat[0]{\hyperlink{def-stringofnat}{\texttt{string\_of\_nat}}}
 
 \newcommand\Ignore[0]{\hyperlink{def-ignore}{\underline{\;\;}}}
@@ -897,7 +934,6 @@
 \newcommand\remaxmatch[0]{\hyperlink{def-rematch}{\textfunc{re\_max\_match}}} % NO_SPECIFICATION_REQUIRED
 \newcommand\Token[0]{\hyperlink{def-token}{\mathbb{T}\mathbb{O}\mathbb{K}\mathbb{E}\mathbb{N}}}
 \newcommand\discard[0]{\hyperlink{def-discard}{\textfunc{discard}}} % NO_SPECIFICATION_REQUIRED
-\newcommand\decimaltolit[0]{\hyperlink{def-decimaltolit}{\textfunc{dec\_to\_lit}}} % NO_SPECIFICATION_REQUIRED
 \newcommand\hextolit[0]{\hyperlink{def-hextolit}{\textfunc{hex\_to\_lit}}} % NO_SPECIFICATION_REQUIRED
 \newcommand\realtolit[0]{\hyperlink{def-realtolit}{\textfunc{real\_to\_lit}}} % NO_SPECIFICATION_REQUIRED
 \newcommand\strtolit[0]{\hyperlink{def-strtolit}{\textfunc{str\_to\_lit}}} % NO_SPECIFICATION_REQUIRED
@@ -913,7 +949,7 @@
 \newcommand\Terror[0]{\hyperlink{def-terror}{\terminal{T\_ERR}}}
 \newcommand\Twhitespace[0]{\hyperlink{def-twhitespace}{\textsf{WHITE\_SPACE}}}
 \newcommand\LexSpec[0]{\hyperlink{def-lexspec}{\textsf{LexSpec}}}
-\newcommand\Lang[0]{\hyperlink{def-lang}{\textsf{Lang}}}
+\newcommand\Lang[1]{\hyperlink{def-lang}{\textsf{Lang}}\left(#1\right)}
 \newcommand\RegExp[0]{\hyperlink{def-regex}{\textsf{RegExp}}}
 \newcommand\ascii[1]{\hyperlink{def-ascii}{\textsf{ASCII}}\texttt{\{#1\}}}
 \newcommand\vnewline[0]{\hyperlink{def-newline}{\texttt{newline}}}
@@ -1144,7 +1180,6 @@
 \newcommand\Supers{\textsf{Supers}}
 \newcommand\Prosecheckisnotcollection[2]{\hyperlink{relation-checkisnotcollection}{determining}
   whether #2 is not a \collectiontypeterm{} in #1 yields $\True$\ProseOrTypeError}
-\newcommand\assocopt[0]{\hyperlink{def-assocopt}{\textfunc{assoc\_opt}}} % SPECIFICATION_DEFERRED
 \newcommand\Proseannotatesymbolicallyevaluableexpr[3]{\hyperlink{relation-annotatesymbolicallyevaluableexpr}{annotating} the
     \symbolicallyevaluableterm\ expression #2 in the static environment #1 yields #3}
 \newcommand\checkstructurelabel[0]{\hyperlink{relation-checkstructurelabel}{\textfunc{check\_structure}}} % SPECIFIED

asllib/doc/AssignableExpressions.tex

@@ -412,7 +412,7 @@ \subsection{Desugaring Assignable Expressions\label{sec:AssignableExpressionsDes
 \[
   \desugarlhsfieldstuple(\overname{\Identifier}{\id} \aslsep \overname{\KleeneStar{\Option{\Identifier}}}{\fieldopts}) \;\aslto\; \overname{\lexpr}{\vlexpr}
 \]
-transforms an assignment to a tuple of fields $\fields$ of variable $\id$ into an AST node $\vlexpr$. \\
+transforms an assignment to a tuple of fields $\fields$ of variable $\id$ into an AST node $\vlexpr$.
 
 \ExampleDef{Desugaring a left-hand side fields tuple}
 \listingref{DesugarLHSFieldsTuple} shows an example of desugaring a left-hand side fields tuple.
@@ -1359,7 +1359,7 @@ \subsection{Typing}
   \annotatelexpr(\tenv, \vleone, \vtleone) \typearrow (\vletwo, \vses) \OrTypeError\\\\
   \makeanonymous(\tenv, \vtleone) \typearrow L(\fields) \OrTypeError\\\\
   L \in \{\TException, \TRecord\}\\
-  \assocopt(\fields, \vfield) \typearrow \tyopt\\
+  \assocopt{\fields}{\vfield} \typearrow \tyopt\\
   \techeck(\tyopt \neq \None, \BadField) \typearrow \True \OrTypeError\\\\
   \tyopt \eqname \some{\vt}\\
   \checktypesat(\tenv, \vte, \vt) \typearrow \True \OrTypeError\\\\
@@ -1405,7 +1405,7 @@ \subsection{Typing}
   \annotateexpr(\tenv, \torexpr(\vleone)) \typearrow (\vtleone, \Ignore, \Ignore) \OrTypeError\\\\
   \annotatelexpr(\tenv, \vleone, \vtleone) \typearrow (\vletwo, \vses) \OrTypeError\\\\
   \makeanonymous(\tenv, \vtleone) \typearrow \TCollection(\fields) \OrTypeError\\\\
-  \assocopt(\fields, \vfield) \typearrow \tyopt\\
+  \assocopt{\fields}{\vfield} \typearrow \tyopt\\
   \techeck(\tyopt \neq \None, \BadField) \typearrow \True \OrTypeError\\\\
   \tyopt \eqname \some{\vt}\\
   \checktypesat(\tenv, \vte, \vt) \typearrow \True \OrTypeError\\\\
@@ -1582,7 +1582,7 @@ \subsection{Typing}
   \begin{itemize}
     \item $\vlefields$ is the list with prefix $\vlefieldsone$ (the elements excluding the last one) and last element $\vfield$;
     \item applying $\foldbitvectorfields$ to $\vbasefields$ and $\vlefieldsone$ in $\tenv$ yields $(\vstart, \vslicesone)$\ProseOrTypeError;
-    \item applying $\assocopt$ to $\vbasefields$ and $\vfield$ yields $\tyopt$;
+    \item applying $\assocoptname$ to $\vbasefields$ and $\vfield$ yields $\tyopt$;
     \item checking that $\tyopt$ is different to $\None$ yields $\True$\ProseTerminateAs{\BadField};
     \item view $\tyopt$ as $\some{\vtfield}$;
     \item applying $\getbitvectorconstwidth$ to $\vtfield$ in $\tenv$ yields \\$\vfieldwidth$\ProseOrTypeError;
@@ -1601,7 +1601,7 @@ \subsection{Typing}
 \begin{mathpar}
 \inferrule[non\_empty]{
   \foldbitvectorfields(\tenv, \vbasefields, \vlefieldsone) \typearrow (\vstart, \vslicesone)\OrTypeError\\\\
-  \assocopt(\vbasefields, \vfield) \typearrow \tyopt\\
+  \assocopt{\vbasefields}{\vfield} \typearrow \tyopt\\
   \techeck(\tyopt \neq \None, \BadField) \typearrow \True \OrTypeError\\\\
   \tyoptp \eqname \some{\vtfield}\\
   \getbitvectorconstwidth(\tenv, \vtfield) \typearrow \vfieldwidth \OrTypeError\\\\