Promoted spec to 1.10

This commit is contained in:
Dmitry Boulytchev 2021-02-01 09:52:28 +03:00
parent f1430a1cdf
commit 7c7ef67e1d
11 changed files with 86 additions and 87 deletions

Binary file not shown.

View file

@ -21,8 +21,8 @@ The following characters are treated as whitespaces:
Additionally, two kinds of comments are recognized:
\begin{itemize}
\item end-of-line comment "\texttt{--}" escapes the rest of the line, including itself;
\item block comment "\texttt{(*} ... \texttt{*)}" escapes all the text between
\item the end-of-line comment "\texttt{--}" escapes the rest of the line, including itself;
\item the block comment "\texttt{(*} ... \texttt{*)}" escapes all the text between
"\texttt{(*}" and "\texttt{*)}".
\end{itemize}
@ -76,11 +76,10 @@ two-character abbreviations "\textbackslash t" and "\textbackslash n" are recogn
The following identifiers are reserved for keywords:
\begin{lstlisting}
after array at before boxed case do elif else
esac eta false fi for fun if import infix
infixl infixr lazy length local od of public repeat
return sexp skip string string syntax then true unboxed
until when while
after array at before box case do elif else
esac eta false fi for fun if import infix
infixl infixr lazy od of public sexp skip str
syntax then true val var while
\end{lstlisting}
\subsection{Infix Operators}

View file

@ -18,7 +18,7 @@ Compilation unit is a minimal structure recognized by the parser. An application
In order to use other units they have to be imported. In particular, the standard library is comprised of a number of precompiled units,
which can be imported by an end-user application.
The concrete syntax for compilation unit is shown on Fig.~\ref{compilation_unit}. Besides optional imports a unit must contain
The concrete syntax for compilation unit is shown in Fig.~\ref{compilation_unit}. Besides optional imports a unit must contain
a \nonterm{scopeExpression}, which may contain some definitions and computations. Note, a unit can not be empty. The computations described in
a unit are performed at unit initialization time (see Chapter~\ref{sec:driver}).
a unit are performed at the unit initialization time (see Chapter~\ref{sec:driver}).

View file

@ -5,7 +5,7 @@
\defterm{definition} & : & \nonterm{variableDefinition}&\alt\\
& & \nonterm{functionDefinition}&\alt\\
& & \nonterm{infixDefinition}&\\
\defterm{variableDefinition} & : & (\s\term{local}\alt\term{public}\s)\s\nonterm{variableDefinitionSequence}\s\term{;}&\\
\defterm{variableDefinition} & : & (\s\term{var}\alt\term{public}\s)\s\nonterm{variableDefinitionSequence}\s\term{;}&\\
\defterm{variableDefinitionSequence} & : & \nonterm{variableDefinitionItem}\s(\s\term{,}\s\nonterm{variableDefinitionItem}\s)^\star&\\
\defterm{variableDefinitionItem} & : & \token{LIDENT}\s[\s\term{=}\s\nonterm{basicExpression}\s]&\\
\defterm{functionDefinition} & : & [\s\term{public}\s]\s\term{fun}\s\token{LIDENT}\s\term{(}\s\nonterm{functionArguments}\s\term{)}&\\
@ -25,7 +25,7 @@ Scope expressions provide a mean to put expressions is a scoped context. The def
variable definitions (see Fig.~\ref{scope_expression}). For example:
\begin{lstlisting}
local x, y, z; -- variable definitions
var x, y, z; -- variable definitions
fun id (x) {x} -- function definition
\end{lstlisting}
@ -33,50 +33,50 @@ variable definitions (see Fig.~\ref{scope_expression}). For example:
As scope expressions are expressions, they can be nested:
\begin{lstlisting}
local x;
var x;
{ -- nested scope begins here
local y;
( -- nested scope begins here
var y;
skip
} -- nested scope ends here
) -- nested scope ends here
\end{lstlisting}
The definitions on the top-level of compilation unit can be tagged as ``\lstinline|public|'', in which case they are exported and become visible by
other units which import the given one. Nested scopes can not contain public definitions.
other units which import a given one. Nested scopes can not contain public definitions.
The nesting relation has the shape of a tree, and in a concrete node of the tree all definitions in all enclosing scopes are visible:
\begin{lstlisting}
local x;
var x;
{local y;
{local z;
(var y;
(var z;
skip -- x, y, and z are visible here
};
{local t;
);
(var t;
skip -- x, y, and t are visible here
};
);
skip -- x and y are visible here
};
);
skip -- only x is visible here
\end{lstlisting}
Multiple definitions of the same name in the same scope are prohibited:
\begin{lstlisting}
local x;
var x;
fun x () {0} -- error
\end{lstlisting}
However, a definition is a nested scope can override a definition in an enclosing one:
\begin{lstlisting}
local x;
var x;
{
(
fun x () {0} -- ok
skip -- here x is associated with the function
};
);
skip -- here x is associated with the variable
\end{lstlisting}
@ -85,15 +85,15 @@ A function can freely use all visible definitions; in particular, functions defi
same scope can be mutually recursive:
\begin{lstlisting}
local x;
var x;
fun f () {0}
{
(
fun g () {f () + h () + y} -- ok
fun h () {g () + x} -- ok
local y;
var y;
skip
};
);
skip
\end{lstlisting}
@ -103,7 +103,7 @@ technically it is possible to have forward references in the initialization expr
behavior is undefined. For example:
\begin{lstlisting}
local x = y + 2; -- undefined, as y is not yet initialized at this point
local y = x + 2;
var x = y + 2; -- undefined, as y is not yet initialized at this point
var y = x + 2;
skip
\end{lstlisting}

View file

@ -1,11 +1,11 @@
\section{Expressions}
\label{sec:expressions}
The syntax definition for expressions is shown on Fig.~\ref{expressions}. The top-level construct is \emph{sequential composition}, expressed
The syntax definition for expressions is shown in Fig.~\ref{expressions}. The top-level construct is \emph{sequential composition}, expressed
using right-associative connective "\term{;}". The basic blocks of sequential composition have the form of \nonterm{binaryExpression}, which is
a composition of infix operators and operands. The description above is given in a highly ambiguous form as it does not specify explicitly the
precedence and associativity of infix operators. The precedences and associativity of predefined built-in infix operators are shown
on Fig.~\ref{builtin_infixes} with the precedence level increasing top-to-bottom.
in Fig.~\ref{builtin_infixes} with the precedence level increasing top-to-bottom.
\begin{figure}[h]
\begin{tabular}{c|l|l}
@ -27,7 +27,7 @@ Apart from assignment and list constructor all other built-in infix operators op
any non-zero value is treated as truth and zero as falsity, and the result respects this convention.
The assignment operator is unique among all others in the sense that it requires its left operand to designate a \emph{reference}. This
property is syntactically ensured using an inference system shown on Fig.~\ref{reference_inference}; here $\mathcal{R}\,(e)$ designates the
property is syntactically ensured using an inference system shown in Fig.~\ref{reference_inference}; here $\mathcal{R}\,(e)$ designates the
property ``$e$ is a reference''. The result of assignment operator coincides with its right operand, thus
\begin{lstlisting}
@ -52,15 +52,15 @@ assigns 3 to both "\lstinline|x|" and "\lstinline|y|".
\subsection{Postfix Expressions}
There are four postfix forms of expressions:
There are two postfix forms of expressions:
\begin{itemize}
\item function call, designated as postfix form "\lstinline|($arg_1, \dots, arg_k$)|";
\item array element selection, designated as "\lstinline|[$index$]|";
\item built-in primitive "\lstinline|.string|", returning the string representation of a value;
\item built-in primitive "\lstinline|.length|", returning the length of a boxed value.
\item array element selection, designated as "\lstinline|[$index$]|".
\end{itemize}
Also, see postfix ``dot'' notation (Section~\ref{sec:dot-notation}).
Multiple postfixes are allowed, for example
\begin{lstlisting}
@ -71,10 +71,10 @@ Multiple postfixes are allowed, for example
\end{lstlisting}
The basic form of expression is \nonterm{primary}. The simplest form of primary is an identifier or constant. Keywords \lstinline|true| and \lstinline|false|
designate integer constants 1 and 0 respectively, character constant is implicitly converted into its ASCII code. String constants designate arrays
designate integer constants 1 and 0 respectively, character constant is implicitly converted into its \textsc{ASCII} code. String constants designate arrays
of one-byte characters. Infix constants allow to reference a functional value associated with corresponding infix operator (however, a value associated with
builtin assignment operator "\lstinline|:=|" can not be taken), and functional constant (\emph{lambda-expression})
designates an anonymous functional value in the form of closure.
designates an anonymous functional value in the form of a closure.
\begin{figure}[h]
\[
@ -88,8 +88,6 @@ designates an anonymous functional value in the form of closure.
\defterm{postfixExpression} & : & \nonterm{primary}&\alt\\
& & \nonterm{postfixExpression}\s\term{(}\s[\s\nonterm{expression}\s(\s\term{,}\s\nonterm{expression}\s)^\star\s]\s\term{)}&\alt\\
& & \nonterm{postfixExpression}\s\term{[}\s\nonterm{expression}\s\term{]}&\alt\\
& & \nonterm{postfixExpression}\s\term{.}\s\term{length}&\alt\\
& & \nonterm{postfixExpression}\s\term{.}\s\term{string}&\\
\defterm{primary} & : & \token{DECIMAL}&\alt\\
& & \token{STRING}&\alt\\
& & \token{CHAR}&\alt\\
@ -99,17 +97,15 @@ designates an anonymous functional value in the form of closure.
& & \term{infix}\s\token{INFIX}&\alt\\
& & \term{fun}\s\term{(}\s\nonterm{functionArguments}\s\term{)}\s\nonterm{functionBody}&\alt\\
& & \term{skip}&\alt\\
& & \term{return}\s[\s\nonterm{basicExpression}\s]&\alt\\
& & \term{\{}\s\nonterm{scopeExpression}\s\term{\}}&\alt\\
& & \term{(}\s\nonterm{scopeExpression}\s\term{)}&\alt\\
& & \nonterm{listExpression}&\alt\\
& & \nonterm{arrayExpression}&\alt\\
& & \nonterm{S-expression}&\alt\\
& & \nonterm{ifExpression}&\alt\\
& & \nonterm{whileExpression}&\alt\\
& & \nonterm{repeatExpression}&\alt\\
& & \nonterm{whileDoExpression}&\alt\\
& & \nonterm{doWhileExpression}&\alt\\
& & \nonterm{forExpression}&\alt\\
& & \nonterm{caseExpression}&\alt\\
& & \term{(}\s\nonterm{expression}\s\term{)}&
& & \nonterm{caseExpression}&
\end{array}
\]
\caption{Expression concrete syntax}
@ -117,10 +113,9 @@ designates an anonymous functional value in the form of closure.
\end{figure}
\FloatBarrier
\subsection{\texttt{skip} and \texttt{return} Expressions}
\subsection{\texttt{skip} Expression}
Expression \lstinline|skip| can be used to designate a no-value when no action is needed (for example, in the body of unit which contains only declarations).
\lstinline|return| expression can be used to immediately complete the execution of current function call; optional return value can be specified.
\subsection{Arrays, Lists, and S-expressions}
@ -136,9 +131,7 @@ Expression \lstinline|skip| can be used to designate a no-value when no action i
\label{composite_expressions}
\end{figure}
There are three forms of expressions to specify composite values: arrays, lists and S-expressions (see Fig.~\ref{composite_expressions}). Note, it is impossible
to specify one-element list as "\lstinline|{$e$}|" since it is treated as scope expression. Instead, the form "\lstinline|$e$:{}|" can be used; alternatively, a standard
unit "\lstinline|List|" (see~Section~\ref{sec:std:list}) defines function "\lstinline|singleton|" which serves for the same purpose.
There are three forms of expressions to specify composite values: arrays, lists and S-expressions (see Fig.~\ref{composite_expressions}).
\subsection{Conditional Expressions}
@ -182,9 +175,9 @@ is equivalent to a nested form
\begin{figure}[t]
\[
\begin{array}{rcl}
\defterm{whileExpression} & : & \term{while}\s\nonterm{expression}\s\term{do}\s\nonterm{scopeExpression}\s\term{od}\\
\defterm{repeatExpression} & : & \term{repeat}\s\nonterm{scopeExpression}\s\term{until}\s\nonterm{basicExpression}\\
\defterm{forExpression} & : & \term{for}\s\nonterm{expression}\s\term{,}\s\nonterm{expression}\s\term{,}\s\nonterm{expression}\\
\defterm{whileDoExpression} & : & \term{while}\s\nonterm{expression}\s\term{do}\s\nonterm{scopeExpression}\s\term{od}\\
\defterm{doWhileExpression} & : & \term{do}\s\nonterm{scopeExpression}\s\term{while}\s\nonterm{expression}\s\term{od}\\
\defterm{forExpression} & : & \term{for}\s\nonterm{scopeExpression}\s\term{,}\s\nonterm{expression}\s\term{,}\s\nonterm{expression}\\
& & \term{do}\nonterm{scopeExpresssion}\s\term{od}
\end{array}
\]
@ -192,21 +185,21 @@ is equivalent to a nested form
\label{loop_expression}
\end{figure}
There are three forms of loop expressions~--- "\lstinline|while|", "\lstinline|repeat|", and "\lstinline|for|", among which "\lstinline|while|" is the
basic one (see Fig.~\ref{loop_expression}). In "\lstinline|while|" expression the evaluation of the body is repeated as long as the evaluation of condition provides
a non-zero value. The condition is evaluated before the body on each iteration of the loop, and the body is evaluated in the context of
condition evaluation results.
There are three forms of loop expressions~--- "\lstinline|while$\dots$do$\dots$od|", "\lstinline|do$\dots$while$\dots$od|", and "\lstinline|for$\dots$|", among
which "\lstinline|while$\dots$do$\dots$od|" is the basic one (see Fig.~\ref{loop_expression}). In "\lstinline|while$\dots$do$\dots$od|" expression the evaluation
of the body is repeated as long as the evaluation of condition provides a non-zero value. The condition is evaluated before the body on each iteration of the loop,
and the body is evaluated in the context of condition evaluation results.
The construct "\lstinline|repeat $\;e\;$ until $\;c$|" is derived and operationally equivalent to
The construct "\lstinline|do $\;e\;$ while $\;c\;$ od|" is derived and operationally equivalent to
\begin{lstlisting}
$e\;$; while $\;c\;$ == 0 do $\;e\;$ od
$e\;$; while $\;c\;$ do $\;e\;$ od
\end{lstlisting}
However, the top-level local declarations in the body of "\lstinline|repeat|"-loop are visible in the condition expression:
However, the top-level local declarations in the body of "\lstinline|do$\dots$while$\dots$od|"-loop are visible in the condition expression:
\begin{lstlisting}
repeat local x = read () until x
do var x = read () while x od
\end{lstlisting}
@ -219,7 +212,7 @@ The construct "\lstinline|for $\;i\;$, $\;c\;$, $\;s\;$ do $\;e\;$ od|" is also
However, the top-level local definitions of the the first expression ("$i$") are visible in the rest of the construct:
\begin{lstlisting}
for local i; i := 0, i < 10, i := i + 1 do write (i) od
for var i; i := 0, i < 10, i := i + 1 do write (i) od
\end{lstlisting}
\subsection{Pattern Matching}
@ -239,9 +232,9 @@ However, the top-level local definitions of the the first expression ("$i$") are
& & \token{CHAR} & \alt \\
& & \term{true} & \alt \\
& & \term{false} & \alt \\
& & \term{\#}\s\term{boxed} & \alt \\
& & \term{\#}\s\term{unboxed} & \alt \\
& & \term{\#}\s\term{string} & \alt \\
& & \term{\#}\s\term{box} & \alt \\
& & \term{\#}\s\term{val} & \alt \\
& & \term{\#}\s\term{str} & \alt \\
& & \term{\#}\s\term{array} & \alt \\
& & \term{\#}\s\term{sexp} & \alt \\
& & \term{\#}\s\term{fun} & \alt \\
@ -277,8 +270,8 @@ The semantics of patterns is as follows:
\item a "\lstinline|$x$@$p$|"-pattern matches what pattern $p$ matches, and additionally binds the
matched value to the identifier $x$;
\item constant patterns match corresponding constants;
\item six "\lstinline|#|"-patterns match values of corresponding shapes (boxed, unboxed, string, array, S-expression or
closure) regardless their content;
\item six "\lstinline|#|"-patterns match values of corresponding shapes (reference values (\lstinline|box|), primitive values (\lstinline|val|),
strings (\lstinline|str|), arrays, S-expressions or closures (\lstinline|fun|)) regardless their content;
\item round brackets can be used for grouping.
\end{itemize}

View file

@ -2,7 +2,7 @@
\label{sec:concrete_syntax}
In this chapter we describe the concrete syntax of the language as it is recognized by the parser. In the
syntactic description we will use extended Backus-Naur form with the following conventions:
syntactic description we will use the extended Backus-Naur form with the following conventions:
\begin{itemize}
\item nonterminals are presented in \nonterm{italics};
@ -16,7 +16,7 @@ syntactic description we will use extended Backus-Naur form with the following c
\end{itemize}
In the description below we will take in-line code samples in blockquotes "..." which are not considered as a
part of concrete syntax.
part of the concrete syntax.
\input{03.01.lexical_structure}
\input{03.02.compilation_units}

View file

@ -16,10 +16,11 @@ redefinition of builtin infix operators:
\begin{itemize}
\item redefinitions of builtin infix operators can not be exported;
\item the assignment operator "\lstinline|:=|" can not be redefined;
\item infix definitions can not be mutually recursive.
\item infix definitions can not be mutually recursive (but this can be worked around by
definining infix synonyms for mutually-recursive functions).
\end{itemize}
The syntax for infix operator definition is shown on Fig.~\ref{custom_infix_construct}; a custom infix definition must specify exactly two arguments.
The syntax for infix operator definition is shown in Fig.~\ref{custom_infix_construct}; a custom infix definition must specify exactly two arguments.
An associativity and precedence level has to be assigned to each custom infix operator. A precedence level is assigned by specifying at which
position, relative to other known infix operators, the operator being defined is inserted. Three kinds of specifications are allowed: at given level,
immediately before or immediately after. For example, "\lstinline|at +|" means that the operator is assigned exactly the same
@ -27,7 +28,7 @@ level of precedence as "\lstinline|+|"; "\lstinline|after +|" creates a new prec
"\lstinline|+|" (but \emph{before} that for "\lstinline|*|"), and "\lstinline|before *|" has exactly the same effect (provided
there were no insertions of precedence levels between those for "\lstinline|+|" and "\lstinline|*|").
When begin inserted at existing precedence level, an infix operator inherits the associativity from that level; hence, only "\lstinline|infix|"
When being inserted at an existing precedence level, an infix operator inherits the associativity from that level; hence, only "\lstinline|infix|"
keyword can be used for such definitions. When a new level is created, an associativity for this level has to be additionally specified
by using corresponding keyword ("\lstinline|infix|" for non-associative levels, "\lstinline|infixr|"~--- for levels with right
associativity, and "\lstinline|infixl|"~--- for levels with left associativity).
@ -94,6 +95,7 @@ where $e$~--- a $\nonterm{basicExpression}$~--- is converted into
where "$x$"~--- a fresh variable which does not occur free in "$e$".
\section{Dot Notation}
\label{sec:dot-notation}
A function call
@ -134,7 +136,7 @@ where $x_i$~--- fresh variables, not free in $e$.
\section{Syntax Definitions}
Syntax definition extension represents an alternative simplified syntax for parsers written using standard unit \lstinline|Ostap| (see Section~\ref{sec:ostap}).
The syntax for syntax definition expressions is shown on Fig.~\ref{syntax_expressions}.
The syntax for syntax definition expressions is shown in Fig.~\ref{syntax_expressions}.
\begin{figure}[h]
\[

View file

@ -15,6 +15,11 @@ The following declarations are accessible:
\descr{\lstinline|fun assert (n, s, ...)|}{Asserts that \lstinline|n| is non-zero; otherwise raises \lstinline|failure| with
a corresponding error message.}
\descr{\lstinline|fun string (x)|}{Converts \lstinline|x| into its string representation.}
\descr{\lstinline|fun length (x)|}{Returns the number of immediate subvalues for a reference value \lstinline|x|; in particular, for
strings and arrays returns their lengths.}
\descr{\lstinline|fun stringInt (s)|}{Converts a string representation of a signed decimal number into integer.}
\descr{\lstinline|fun read ()|}{Reads an integer value from the standard input, printing a prompt "\lstinline|>|".}
@ -124,7 +129,7 @@ Random data structures generation functions.
\descr{\lstinline|fun randomInt ()|}{Generates a random representable integer value.}
\descr{\lstinline|fun randomString (len)|}{Generates a random string of printable ASCII characters of given length.}
\descr{\lstinline|fun randomString (len)|}{Generates a random string of printable \textsc{ASCII} characters of given length.}
\descr{\lstinline|fun randomArray (f, n)|}{Generates a random array of \emph{deep} size \lstinline|n|. The length of the array is chosen randomly, and \lstinline|f| is intended to be an element-generating function which takes the size of the element as an argument.}
@ -322,9 +327,7 @@ The unit provides primitives for lazy evaluation.
\section{Unit \texttt{List}}
\label{sec:std:list}
The unit provides some list-manipulation functions. None of the functions mutate their arguments.
\descr{\lstinline|fun singleton (x)|}{Returns a one-element list with the value "\lstinline|x|" as its head.}
The unit provides some list-manipulation functions.
\descr{\lstinline|fun size (l)|}{Returns the length of the list.}

View file

@ -86,8 +86,8 @@
\newcommand{\descr}[2]{\smallskip{#1}\begin{itemize}[noitemsep,topsep=0pt]\item[]{#2}\end{itemize}}
\lstdefinelanguage{lama}{
keywords={skip,if,then,else,elif,fi,while,do,od,repeat,until,for,fun,local,public,import,length,
string,case,of,esac,when,boxed,unboxed,string,sexp,array,infix,infixl,infixr,at,before,after,true,false,eta,lazy,syntax},
keywords={skip,if,then,else,elif,fi,while,do,od,for,fun,public,import,
box,val, var,case,of,esac,when,box,str,sexp,array,infix,infixl,infixr,at,before,after,true,false,eta,lazy,syntax},
sensitive=true,
basicstyle=\small,
%commentstyle=\scriptsize\rmfamily,
@ -145,6 +145,8 @@ language=lama
{\huge\bfseries \lama Language Specification}\\[0.4cm] % Title of your document
{\textsc{Version 1.10}}
\HRule\\[1.5cm]
%------------------------------------------------

View file

@ -1254,7 +1254,7 @@ let run_parser cmd =
"while"; "do"; "od";
"for";
"fun"; "var"; "public"; "external"; "import";
"case"; "of"; "esac"; "when";
"case"; "of"; "esac";
"box"; "val"; "str"; "sexp"; "array";
"infix"; "infixl"; "infixr"; "at"; "before"; "after";
"true"; "false"; "lazy"; "eta"; "syntax"]

View file

@ -1 +1 @@
let version = "Version 1.10, 216e71625, Sun Jan 31 22:25:31 2021 +0300"
let version = "Version 1.10, f1430a1cd, Sun Jan 31 22:57:12 2021 +0300"