From 11d0abf8c8db0a389801a390d96505a7fe0c2409 Mon Sep 17 00:00:00 2001 From: Roman-Manevich Date: Thu, 6 Feb 2025 11:59:02 +0000 Subject: [PATCH] [asl][reference] work on Literals chapter and print statements --- asllib/doc/ASLmacros.tex | 7 +- asllib/doc/Literals.tex | 31 +--- asllib/doc/RuntimeEnvironment.tex | 5 +- asllib/doc/Semantics.tex | 3 +- asllib/doc/Statements.tex | 173 ++++++++++++++---- .../SemanticsRule.SPrint.asl | 18 ++ asllib/tests/ASLSemanticsReference.t/run.t | 12 ++ .../ASLSyntaxReference.t/Lexical.Comments.asl | 4 + 8 files changed, 190 insertions(+), 63 deletions(-) create mode 100644 asllib/tests/ASLSemanticsReference.t/SemanticsRule.SPrint.asl diff --git a/asllib/doc/ASLmacros.tex b/asllib/doc/ASLmacros.tex index 15bc7a95b..df38923f1 100644 --- a/asllib/doc/ASLmacros.tex +++ b/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}} \ No newline at end of file +\newcommand\vexpectedconstraintlength[0]{\texttt{expected\_constraint\_length}} +\newcommand\vconsolestream[0]{\texttt{consolestream}} diff --git a/asllib/doc/Literals.tex b/asllib/doc/Literals.tex index d567ac136..c0b60aac2 100644 --- a/asllib/doc/Literals.tex +++ b/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)$. diff --git a/asllib/doc/RuntimeEnvironment.tex b/asllib/doc/RuntimeEnvironment.tex index 653e59656..f8657f304 100644 --- a/asllib/doc/RuntimeEnvironment.tex +++ b/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 diff --git a/asllib/doc/Semantics.tex b/asllib/doc/Semantics.tex index b6a7cf6be..649c6fccc 100644 --- a/asllib/doc/Semantics.tex +++ b/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. diff --git a/asllib/doc/Statements.tex b/asllib/doc/Statements.tex index b61f9bd10..287da652b 100644 --- a/asllib/doc/Statements.tex +++ b/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}} diff --git a/asllib/tests/ASLSemanticsReference.t/SemanticsRule.SPrint.asl b/asllib/tests/ASLSemanticsReference.t/SemanticsRule.SPrint.asl new file mode 100644 index 000000000..bb74d7f1f --- /dev/null +++ b/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; diff --git a/asllib/tests/ASLSemanticsReference.t/run.t b/asllib/tests/ASLSemanticsReference.t/run.t index 46034c074..6c51fafd6 100644 --- a/asllib/tests/ASLSemanticsReference.t/run.t +++ b/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 diff --git a/asllib/tests/ASLSyntaxReference.t/Lexical.Comments.asl b/asllib/tests/ASLSyntaxReference.t/Lexical.Comments.asl index 62b828801..e5e093870 100644 --- a/asllib/tests/ASLSyntaxReference.t/Lexical.Comments.asl +++ b/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 "//". */