More spec

doc/spec/03.01.lexical_structure.tex

@@ -1,4 +1,5 @@
 \section{Lexical Structure}
+\label{sec:lexical_structure}
 
 The character set for the language is \textsc{ASCII}, case-sensitive. In the following lexical description we will use
 the GNU Regexp syntax~\cite{GNULib} in lexical definitions.
@@ -26,7 +27,7 @@ Additionally, two kinds of comments are recognized:
 
 There is a number of specific cases which have to be considered explicitly.
 
-First, block comments can be properly nested. Then, the occurencies of comment symbols inside string literals (see below) do not
+First, block comments can be properly nested. Then, the occurencies of comment symbols inside string literals (see below) are not
 considered as comments.
 
 End-of-line comment encountered \emph{outside} of a block comment escapes block comment symbols:
@@ -92,7 +93,7 @@ There is a predefined set of built-in infix operators (see~\ref{binary_expressio
 an end-used can define custom infix operators (see~\ref{custom_infix}). Note, sometimes 
 additional whitespaces are required to disambiguate infix operator applications. For example, if a
 custom infix operator "\lstinline|+-|" is defined, then the expression "\lstinline|a +- b|" can no longer be
-considered as "\lstinline|a +(-b)|". Note also that a custom operator "\lstinline|--|" can not be
+considered as "\lstinline|a +(-b)|". Note also that a custom operator containing "\lstinline|--|" can not be
 defined due to lexical conventions.
 
 \subsection{Delimiters}
@@ -105,6 +106,6 @@ The following symbols are treated as delimiters:
 \end{lstlisting}
 
 Despite custom infix operators can coincide with delimiters "\lstinline|#|" and "\lstinline|->|" they can
-never clash as both these delimiters can not be encountered in expressions.
+never clash as neither of these delimiters can be encountered in expressions in infix operator position.
 
 

doc/spec/03.02.compilation_units.tex

@@ -10,12 +10,13 @@
 \end{figure}
 
 \section{Compilation Units}
+\label{sec:compilation_units}
 
 Compilation unit is a minimal structure recognized by a parser. An application can contain multiple units, compiled separatedly.
 In order to use other units they have to be imported. In particular, the standard library is comprized of a number of precompiled units,
 which can be imported by an end-user application.
 
-The concrete syntax for compilation unit is show on Fig.~\ref{compilation_unit}. Besides optional imports a unit must contain
+The concrete syntax for compilation unit is shown on 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~\ref{separate_compilation}).
 

doc/spec/03.03.scope_expressions.tex

@@ -16,6 +16,7 @@
 \end{figure}
 
 \section{Scope Expressions}
+\label{sec:scope_expressions}
 
 Scope expressions provide a mean to put expressions is a scoped context. The definitions in scoped expressions comprise of function definitions and
 variable definitions (see Fig.~\ref{scope_expression}). For example:

doc/spec/03.04.expressions.tex

@@ -41,5 +41,83 @@
 \section{Expressions}
 \label{sec:expressions}
 
-Expressions 
+The syntax definition for expressions is shown on Fig.~\ref{expressions}. The top-level construct is \emph{sequential composition}, expressed
+using right-associative conective "\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.
+
+Apart from assignment and list constructor all other built-in infix operators operate on signed integers; in conjunction and disjunction
+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 ``$e$ is a reference''. The result of assignment operator coincides with its right operand, thus
+
+\begin{lstlisting}
+    x := y := 3
+\end{lstlisting}
+
+assigns 3 to both "\lstinline|x|" and "\lstinline|y|".
+
+There are four 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 the value;
+\item built-in primitive "\lstinline|.length|", returning the length of boxed value.
+\end{itemize}
+
+Multiple postfixes are allowed, for example
+
+\begin{lstlisting}
+    x () [3] (1, 2, 3) . string
+    x . string [4]
+    x . length . string
+    x . string . length
+\end{lstlisting}
+
+The basic form of expression is \nonterm{primary}.
+
+Some other examples with comments:
+
+\begin{tabular}{ll}
+  "\lstinline|x !! y && z + 3|" & is equivalent to "\lstinline|x !! (y && (z + 3))|"\\
+  "\lstinline|x == y < 4|"      & invalid \\
+  "\lstinline|x [y := 8] := 6|" & is equivalent to "\lstinline|y := 8; x [8] := 6|"\\
+  "\lstinline|(write (3); x) := (write (4); z)|" & is equivalent to "\lstinline|write (3); write (4); x := z|"
+\end{tabular}
+
+
+\begin{figure}
+  \begin{tabular}{c|l|l}
+    infix operator(s) & description & associativity \\
+    \hline
+    \lstinline|:=|                                                                                & assignment                         & right-associative \\
+    \lstinline|:|                                                                                 & list constructor                   & right-associative \\
+    \lstinline|!!|                                                                                & disjunction                        & left-associative  \\
+    \lstinline|&&|                                                                                & conjunction                        & left-associative  \\
+    \lstinline|==|, \lstinline|!=|,  \lstinline|<=|, \lstinline|<|, \lstinline|>=|, \lstinline|>| & integer comparisons                & non-associative   \\
+    \lstinline|+|, \lstinline|-|                                                                  & addition, subtraction              & left-associative  \\
+    \lstinline|*|, \lstinline|/|, \lstinline|%|                                                   & multiplication, quotent, remainder & left-associative
+  \end{tabular}
+\caption{The precedence and associativity of built-in infix operators}
+\label{builtin_infixes}
+\end{figure}
+
+\begin{figure}
+  \newcommand{\Ref}[1]{\mathcal{R}\,({#1})}
+  \renewcommand{\arraystretch}{4}
+  \[
+    \begin{array}{cc}
+      \Ref{x},\,x\;\mbox{is a variable}&\dfrac{\Ref{e}}{\Ref{\lstinline|$e$ [$\dots$]|}}\\
+      \dfrac{\Ref{e_i}}{\Ref{\mbox{\lstinline|if $\dots$ then $\;e_1\;$ else $\;e_2\;$ fi|}}} & \dfrac{\Ref{e_i}}{\Ref{\mbox{\lstinline|case $\dots$ of $\;\dots\;$ -> $\;e_1\;\dots\;\dots\;$ -> $\;e_k\;$ esac|}}}\\
+      \multicolumn{2}{c}{\dfrac{\Ref{e}}{\Ref{\lstinline|$\dots\;$;$\;e$|}}}
+    \end{array}
+  \]
+  \caption{Reference inference system}
+  \label{reference_inference}
+\end{figure}
+
 

doc/spec/03.concrete_syntax.tex

@@ -1,4 +1,5 @@
 \chapter{Concrete Syntax}
+\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:
@@ -14,7 +15,7 @@ syntactic description we will use extended Backus-Naur form with the following c
 \item a colon ``$:$'' separates a nonterminal being defined from its definition.
 \end{itemize}
 
-In the description below we will take an in-line code samples in blockquotes "..." which are not considered as a
+In the description below we will take in-line code samples in blockquotes "..." which are not considered as a
 part of concrete syntax.
 
 \input{03.01.lexical_structure}

doc/spec/04.driver_options.tex

@@ -0,0 +1 @@
+\chapter{Driver Options and Separate Compilation}

doc/spec/05.standard_library.tex

@@ -0,0 +1 @@
+\chapter{Standard Library}

doc/spec/spec.tex

@@ -127,5 +127,10 @@ language=alm
 \input{01.introduction}
 \input{02.abstract_syntax_and_semantics}
 \input{03.concrete_syntax}
+\input{04.driver_options}
+\input{05.standard_library}
+
+\bibliographystyle{plainurl}
+\bibliography{spec}
 
 \end{document}