[asl][reference] work on Literals chapter and print statements

asllib/doc/ASLmacros.tex

@@ -1133,6 +1133,8 @@
 \newcommand\readvaluefrom[0]{\hyperlink{def-readvaluefrom}{\textfunc{read\_value\_from}}}
 \newcommand\writeretvals[0]{\hyperlink{def-writeretvals}{\textfunc{write\_ret\_vals}}}
 \newcommand\outputtoconsole[0]{\hyperlink{def-outputtoconsole}{\textfunc{output\_to\_console}}}
+\newcommand\literaltostring[0]{\hyperlink{def-literaltostring}{\textfunc{literal\_to\_string}}}
+\newcommand\Proseoutputtoconsole[1]{\hyperlink{def-outputtoconsole}{outputs} #1 to the console, if one exists}
 \newcommand\assignbitvectorfields[0]{\hyperlink{def-assignbitvectorfields}{\textfunc{assign\_bitvector\_fields}}}
 
 \newcommand\unoprel[0]{\hyperlink{def-unoprel}{\textfunc{unop}}}
@@ -1983,7 +1985,7 @@
 \newcommand\denv[0]{\textsf{denv}}
 \newcommand\aslsep[0]{\mathbf{,}}
 
-\newcommand\env[0]{\hyperlink{def-env}{\texttt{env}}}
+\newcommand\env[0]{\texttt{env}}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % LRM Ident info
@@ -3110,4 +3112,5 @@
 \newcommand\typedinitialvalue[0]{\texttt{typed\_initial\_value}}
 \newcommand\typede[0]{\texttt{typed\_e}}
 \newcommand\vfieldnames[0]{\texttt{field\_names}}
-\newcommand\vexpectedconstraintlength[0]{\texttt{expected\_constraint\_length}}
+\newcommand\vexpectedconstraintlength[0]{\texttt{expected\_constraint\_length}}
+\newcommand\vconsolestream[0]{\texttt{consolestream}}

asllib/doc/Literals.tex

@@ -8,8 +8,10 @@ \chapter{Literals\label{chap:Literals}}
 Rather, they are parsed as identifiers, and during type elaboration
 converted true enumeration label literal values.
 
-\section{Syntax}
+In the sequel of this reference, we often refer to literal values
+as simply literals.
 
+\section{Syntax}
 \begin{flalign*}
 \Nvalue \derives         \ & \Tintlit &\\
                         |\ & \Tboollit &\\
@@ -138,27 +140,6 @@ \subsection{Example}
 \section{Semantics}
 A literal $\vl$ can be converted to the \nativevalue\ $\nvliteral{\vl}$.
 
-\subsection{Printing}%
-\hypertarget{def-outputtoconsole}{}
-
-The following table describes how literals can be printed to a command line.
-%
-Please note that surrounding quotations mark for $\lstring(S)$ are not included
-in $S$, so they will not be printed.
-
-\begin{tabular}{rl}
-  \textbf{literal} & \textbf{prints} \\
-  \hline
-  $\lint(n)$ & $n$ in decimal format, without any leading zeros, \\
-             & preceded by a ``\texttt{-}'' sign if $n$ is negative. \\
-  $\lbool(\True)$ & ``\texttt{TRUE}'' \\
-  $\lbool(\False)$ & ``\texttt{FALSE}'' \\
-  $\lreal(q)$ & $q$ as an irreducible fraction of positive integers, \\
-              & preceded by a ``\texttt{-}'' sign when $q$ is negative, \\
-              & with the denominator omitted if it is equal to 1. \\
-  $\lbitvector(b)$ & $b$ in hexadecimal, preceded by ``\texttt{0x}'', with enough leading zeros \\
-                   & to make the number of hexadecimal digits printed equal the width \\
-                   & of $b$ divided by 4, and rounded up to the following integer. \\
-  $\lstring(S)$ & $S$. \\
-  $\llabel(s)$ & $s$. \\
-\end{tabular}
+\subsubsection{Example}
+The literal $\lint(5)$ can be used as a \nativevalue\ $\nvliteral{\lint(5)}$,
+which we will usually abbreviate as $\nvint(5)$.

asllib/doc/RuntimeEnvironment.tex

@@ -2,8 +2,9 @@ \chapter{Runtime Environment\label{chap:RuntimeEnvironment}}
 
 An ASL runtime provides run time support within a hosting environment.
 
-Examples of a hosting environment include an interactive interpreter, an interpreter running in batch mode, a
-Verilog simulator, and  Linux process (native executable).
+Examples of a hosting environment include an interactive interpreter,
+an interpreter running in batch mode,
+a Verilog simulator, and Linux process (native executable).
 
 \RequirementDef{RuntimeDefaultEntry}
 The default entry point is the \texttt{main} function, which has the signature

asllib/doc/Semantics.tex

@@ -219,9 +219,8 @@ \section{Native Values\label{sec:nativevalues}}
 \hypertarget{def-envs}{}
 \begin{definition}[Environments]
 Environments pair static environments with dynamic environments:
-$\envs = \staticenvs \times \dynamicenvs$.
+$\envs \triangleq \staticenvs \times \dynamicenvs$.
 \end{definition}
-\hypertarget{def-env}{}
 We write $\env \in \envs$ to range over environments.
 %
 From the perspective of the semantics, the static environment is immutable.

asllib/doc/Statements.tex

@@ -3288,7 +3288,9 @@ \subsection{Abstract Syntax}
   \astarrow
   \overname{\SPrint(\astversion{\vargs}, \vnewline)}{\vastnode}
 }
-\\
+\end{mathpar}
+
+\begin{mathpar}
 \inferrule{%
   \buildplist[\Nexpr](\vargs) \astarrow \astversion{\vargs} \\
   \vnewline \eqdef \True \\
@@ -3301,8 +3303,9 @@ \subsection{Abstract Syntax}
 \end{mathpar}
 
 \subsection{Typing}
-
 \TypingRuleDef{SPrint}
+\listingref{literals1} shows literals and their corresponding types in comments.
+
 \ProseParagraph
 All of the following apply:
 \begin{itemize}
@@ -3327,47 +3330,153 @@ \subsection{Typing}
 \CodeSubsection{\SPrintBegin}{\SPrintEnd}{../Typing.ml}
 
 \subsection{Semantics}
+\SemanticsRuleDef{SPrint}
+
+\subsection{Example (Printing Literals)}
+\listingref{semantics-literals} shows examples of printing various types of literals,
+followed by the output to the console resulting from running the specification.
+\ASLListing{Literals and how they are displayed}{semantics-literals}{\semanticstests/SemanticsRule.SPrint.asl}
+\begin{verbatim}
+string_number_1
+1000000
+53170898287292728730499578000
+TRUE
+FALSE
+12345678900123456789/10000000000
+hello\world
+          "here I am "
+
+0xd
+0x
+LABEL_B
+\end{verbatim}
+
+\ProseParagraph
+\OneApplies
+\begin{itemize}
+  \item \AllApplyCase{print}
+  \begin{itemize}
+    \item $\vs$ denotes a Print statement with arguments $\elist$ and newline indicator $\False$;
+    \item the evaluation of $\elist$ in $\env$ is $\Normal((\vlist, \vg), \newenv)$\ProseOrAbnormal;
+    \item \Proseoutputtoconsole{all the elements in $\elist$, without a separator,};
+    \item if $\vnewline$ is $\True$, \Proseoutputtoconsole{a newline character};
+  \end{itemize}
+
+  \item \AllApplyCase{println}
+  \begin{itemize}
+    \item $\vs$ denotes a Print statement with arguments $\elist$ and newline indicator $\True$;
+    \item the evaluation of the same statement with a newline indicator set to $\False$, that is,
+          $\SPrint(\elist, \False)$ yields the configuration $\Continuing(\vg, \envone)$\ProseOrAbnormal;
+    \item \Proseoutputtoconsole{a newline character};
+  \end{itemize}
+  \item the resulting configuration is $\Continuing(\vg, \newenv)$.
+\end{itemize}
+
+\FormallyParagraph
+\begin{mathpar}
+\inferrule[Print]{
+  \evalexprlist{\env, \elist} \evalarrow \Normal((\vlist, \vg), \env_1) \OrAbnormal\\
+  \vi\in\listrange(\vlist): \outputtoconsole(\env_\vi, \vlist[i]) \evalarrow \env_{\vi + 1} \\
+  n \eqdef \listlen{\vlist}\\
+  \newenv \eqdef \env_{n + 1}
+}{
+  \evalstmt{\env, \SPrint(\elist, \False)} \evalarrow \Continuing(\vg, \newenv)
+}
+\end{mathpar}
+
+\begin{mathpar}
+\inferrule[Println]{
+  \evalstmt{\env, \SPrint(\elist, \False)} \evalarrow \Continuing(\vg, \envone) \OrAbnormal\\\\
+  \outputtoconsole(\envone, \nvstring(\texttt{"\char`\\n"})) \evalarrow \newenv
+}{
+  \evalstmt{\env, \SPrint(\elist, \True)} \evalarrow \Continuing(\vg, \newenv)
+}
+\end{mathpar}
+\CodeSubsection{\EvalSPrintBegin}{\EvalSPrintEnd}{../Interpreter.ml}
 
-Not all ASL backends support printing to a console.
+\SemanticsRuleDef{OutputToConsole}
+Not all ASL runtimes support printing to a console (see \RequirementRef{Printing}).
 %
-Therefore, the semantics is parameterized by the function $\outputtoconsole$,
-which takes a string and communicates it to a console, where one exists.%
-\footnote{%
-  Formally, the console can be modelled by adding a string-typed component to
-  the global dybamic environment, which concatenates all strings that were sent
-  to it. For brevity, and since it is only used for print statements, we omit
-  this component from our definition of a dynamic environment.%
+Therefore, the semantics is parameterized by the function
+\hypertarget{def-outputtoconsole}{}
+\[
+\outputtoconsole(\overname{\envs}{\env} \aslsep \overname{\vals}{\vv}) \aslto
+  \overname{\envs}{\newenv}
+\]
+which takes a string and communicates it to a console, where one exists.
+
+We now explain how printing is modelled when the runtime supports a console
+and how it is modelled when the runtime does not support a console.
+
+\subsubsection{Runtime Does Not Support a Console}
+The function ignores the string value and returns the environment unchanged.
+
+\ProseParagraph
+\ProseEqdef{$\newenv$}{$\env$}.
+
+\FormallyParagraph
+\begin{mathpar}
+\inferrule[no\_console]{}{
+  \outputtoconsole(\env, \Ignore) \evalarrow \overname{\env}{\newenv}
 }
+\end{mathpar}
+
+\subsubsection{Runtime Supports a Console}
+To support a console, the definition of environments needs
+to include an extra component to capture the string of characters sent to the console:
+\[
+\envs \triangleq \staticenvs \times \dynamicenvs \times \Strings \enspace.
+\]
+We omit this component in the rest of this document to avoid clutter, and include it
+only here to explain the modeling of a console.
+
+\hypertarget{def-literaltostring}{}
+The helper function $\literaltostring : \literal \aslto \Strings$,
+which defines how a literal is represented by a string,
+is defined by the following table.
+%
+Please note that surrounding quotations mark for $\lstring(S)$ are not included
+in $\literaltostring(S)$, so they will appear in the printed string.
+
+\begin{tabular}{rl}
+\textbf{literal $\vl$} & \textbf{$\literaltostring(\vl)$} \\
+\hline
+$\lint(n)$        & $n$ in decimal format, without any leading zeros, \\
+                  & preceded by a ``\texttt{-}'' sign if $n$ is negative. \\
+$\lbool(\True)$   & \texttt{TRUE} \\
+$\lbool(\False)$  & \texttt{FALSE} \\
+$\lreal(q)$       & $q$ as an irreducible fraction of positive integers, \\
+                  & preceded by a ``\texttt{-}'' sign when $q$ is negative, \\
+                  & with the denominator omitted if it is equal to 1. \\
+$\lbitvector(b)$  & $b$ in hexadecimal, preceded by ``\texttt{0x}'', with enough leading \\
+                  & zeros to make the number of hexadecimal digits printed \\
+                  & equal to the width of $b$ divided by 4, and rounded up to \\
+                  & the following integer.\\
+$\lstring(S)$     & $S$. \\
+$\llabel(s)$      & $s$. \\
+\end{tabular}
 
 \ProseParagraph
-All of the following apply:
+\AllApply
 \begin{itemize}
-  \item $\vs$ denotes a Print statement with arguments $\elist$ and newline indicator $\vnewline$;
-  \item the evaluation of $\elist$ in $\env$ is $\Normal((\vlist, \vg), \newenv)$\ProseOrAbnormal;
-  \item \hyperlink{def-outputtoconsole}{prints} all the elements in $\elist$, without separator;
-  \item if $\vnewline$ is $\True$, prints a newline character;
-  \item $\newenv$ is $\env$.
+  \item view $\env$ as the environment consisting of the static environment $\tenv$,
+        dynamic environment $\denv$, and console string $\vconsolestream$;
+  \item view $\vv$ as a native literal for the literal $\vl$;
+  \item \Proseeqdef{$\newenv$}{the environment consisting of the static environment $\tenv$,
+        dynamic environment $\denv$, and console string
+        define as the concatenation of \\
+        $\vconsolestream$ and $\literaltostring(\vl)$}.
 \end{itemize}
 
 \FormallyParagraph
-
 \begin{mathpar}
-  \inferrule[Print]{%
-    \evalexprlist{\env, \elist} \evalarrow \Normal((\vlist, \vg), \newenv) \OrAbnormal\\
-    \vi\in\listrange(\vlist): \outputtoconsole(\vlist[i]) \\
-  }{%
-    \evalstmt{\env, \SPrint(\elist, \False)} \evalarrow \Continuing(\vg, \newenv)
-  }
-  \\
-  \inferrule[Println]{%
-    \evalexprlist{\env, \elist} \evalarrow \Normal((\vlist, \vg), \newenv) \OrAbnormal\\
-    \vi\in\listrange(\vlist): \outputtoconsole(\vlist[i]) \\
-    \outputtoconsole(\lstring(\texttt{"\char`\\n"})) \\
-  }{%
-    \evalstmt{\env, \SPrint(\elist, \True)} \evalarrow \Continuing(\vg, \newenv)
-  }
+\inferrule[console\_exists]{
+  \env \eqname (\tenv, \denv, \vconsolestream)\\
+  \newenv \eqdef (\tenv, \denv, \vconsolestream \concat \literaltostring(\vl))
+}{
+  \outputtoconsole(\env, \nvliteral{\vl}) \evalarrow (\newenv)
+}
 \end{mathpar}
-\CodeSubsection{\EvalSPrintBegin}{\EvalSPrintEnd}{../Interpreter.ml}
 
 \hypertarget{def-unreachablestatementterm}{}
 \section{The Unreachable Statement\label{sec:UnreachableStatement}}

asllib/tests/ASLSemanticsReference.t/SemanticsRule.SPrint.asl

@@ -0,0 +1,18 @@
+type MyEnum of enumeration { LABEL_A, LABEL_B, LABEL_C };
+func main () => integer
+begin
+  print("string_");
+  print("number_");
+  println(1);
+  println(1_000__000);
+  println(0xa_b_c_d_e_f__A__B__C__D__E__F__0___12345567890);
+  println(TRUE);
+  println(FALSE);
+  println(1234567890.0123456789);
+  println("hello\\world\n\t \"here I am \"");
+  print("");
+  println('11 01');
+  println('');
+  println(LABEL_B);
+  return 0;
+end;

asllib/tests/ASLSemanticsReference.t/run.t

@@ -81,6 +81,18 @@ ASL Semantics Tests:
   $ aslref SemanticsRule.SThrowSTry.asl
   aslref cannot find file "SemanticsRule.SThrowSTry.asl"
   [1]
+  $ aslref SemanticsRule.SPrint.asl
+  string_number_1
+  1000000
+  53170898287292728730499578000
+  TRUE
+  FALSE
+  12345678900123456789/10000000000
+  hello\world
+  	 "here I am "
+  0xd
+  0x
+  LABEL_B
   $ aslref SemanticsRule.Loop.asl
   $ aslref SemanticsRule.For.asl
   $ aslref SemanticsRule.Catch.asl

asllib/tests/ASLSyntaxReference.t/Lexical.Comments.asl

@@ -1,15 +1,19 @@
 // Comment example 1.
+
 // In next line, the two strings "/*" and "*/" are regular characters within the comment
 // start of comment, /* still in comment */ and still in comment which ends with newline
+
 /* line 1 of example 2, a single comment 4 lines long.
 line 2 of the comment
 // line 3 of the comment, the "//" at start of this line are just regular characters
 // line 4 of the comment, this 4 line comment ends with these two characters -->*/
+
 /* L1 Comment example 3, shows you cannot nest or mix comment styles.
 /* L2 Note the declaration of the storage FOO on L6, is outside of the comment.
 /* L3 Note the first two characters on L6 do NOT start a nested comment.
 /* L4 However, the two chars '*' and '/' following the line number L6, terminate
 /* L5 the comment started on L1.
 /* L6 */ var FOO : integer = 1; // The declaration of FOO is not within any comment */
+
 /* L7 The last two characters on line L6 have no special meaning, */
 /* L8 they are just characters within the comment that started with the "//". */