st/lama_byterun
1
0
Fork 0
mirror of https://github.com/ProgramSnail/Lama.git synced 2025-12-05 22:38:44 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Abstract layer in spec started

Browse source
This commit is contained in:
Dmitry Boulytchev 2021-02-10 00:56:28 +03:00
parent 59f78fe38a
commit ec655ea22d
12 changed files with 456 additions and 91 deletions
Download patch file Download diff file Expand all files Collapse all files

13
spec/01.01.general_characteristics.tex
View file

@ -1,13 +0,0 @@
\section{General Characteristic of the Language}
\begin{itemize}
\item procedural with first-class functions~--- functions can be passed as arguments, placed in data structures,
returned and constructed at runtime via closures mechanism;
\item with lexical static scoping;
\item strict~--- all arguments of function application are evaluated before function's body;
\item imperative~--- variables can be re-assigned, function calls can have side effects;
\item untyped~--- no static type checking is performed;
\item supports S-expressions and pattern-matching;
\item supports user-defined infix operators, including those defined in local scopes;
\item with automatic memory management (garbage collection).
\end{itemize}

50
spec/01.02.notation.tex
View file

@ -1,50 +0,0 @@
\section{Notation}
Pairs and tuples:
\[
\inbr{\bullet,\,\bullet,\,\dots}
\]
Lists of elements of kind $X$:
\[
X^*
\]
Deconstructing lists into sublists:
\[
h\circ t
\]
This applies also to lists of length 1. Empty list is denoted
\[
\epsilon
\]
For a mapping $f : X\to Y$ we use the following definition:
\[
f [x\gets y] = \lambda\,z\,.\,
\left\{
\begin{array}{rcl}
y &,& x = z \\
f\;x &,& x\neq z
\end{array}
\right.
\]
Empty mapping (undefined everywhere) is denoted $\Lambda$, the domain of a mapping $f$~--- $\dom{f}$, and we abbreviate
\[
\Lambda[x_1\gets y_1][x_2\gets y_2]\dots[x_k\gets y_k]
\]
as
\[
[x_1\gets y_1,\,x_2\gets y_2,\,\dots,\,x_k\gets y_k]
\]

20
spec/01.03.values.tex
View file

@ -1,20 +0,0 @@
\section{Names, Values and States}
\begin{table}[t]
\begin{tabular}{cccl}
denotation & instances & definition & comments \\
\hline
$\mathscr X$ & $x,\,y,\,z,\,\dots$ & & variables \\
$\mathscr T$ & $\llang{C},\,\llang{D},\,\dots$ & & tags (constructors) \\
$\Sigma$ & $\sigma$ & $\mathscr X\to\mathscr V$ & bindings (a partial map from variables to values) \\
$\Sigma_{\mathscr X}$ & $\inbr{\sigma,\,S}$ & $2^{\mathscr X}\times\Sigma$ & local scope (a set of variable and bindings) \\
$St$ & $\inbr{\sigma_g,\,ss}$ & $\Sigma\times\Sigma^*_{\mathscr X}$ & state (global bindings and a stack of local scopes) \\
$\mathscr L$ & $l$ & & locations \\
$M$ & $\mu$ & $\mathscr L\to\mathscr C$ & abstract memory (a partial map from locations to composite values) \\
$\mathscr V$ & $v$ & $\mathbb Z\uplus \mathscr L$ & values (integer values or locations) \\
$\mathscr C$ & & $Arr\uplus Sexp \uplus Clo$ & composite values (arrays, S-expressions or closures) \\
$Arr$ & & $\mathbb N\times (\mathbb N\to\mathscr V)$ & arrays (length and element function) \\
$Sexp$ & & $\mathscr T \times Arr$ & S-expressions (tag and array of subvalues) \\
$Clo$ & & $\mathscr X \times \Sigma^*_{\mathscr X}$ & closures (function name and a stack of local scopes)
\end{tabular}
\end{table}

4
spec/01.introduction.tex
View file

@ -33,7 +33,3 @@ standard library, written in \lama itself. The native code compiler uses \textsc
In addition, a source-level reference interpreter is implemented as well as a compiler to a small
stack machine. The stack machine code can in turn be either interpreted on a stack machine interpreter, or
used as an intermediate representation by the native code compiler.
%\input{01.01.general_characteristics}
%\input{01.02.notation}
%\input{01.03.values}

37
spec/02.01.categories.tex Normal file
View file

@ -0,0 +1,37 @@
\begin{table}[t]
\begin{tabular}{cccl}
notation & instances & definition & comments \\[1mm]
\hline\\
$\inbr{\bullet,\,\bullet,\,\dots}$ & & & pairs and tuples\\[1mm]
$X^\bot$ & & & $X\cup\{\bot\}$\\[1mm]
$X^*$ & & & lists of elements of $X$\\[1mm]
$\mathscr X$ & $x,\,y,\,z,\,\dots$ & & variables \\[1mm]
$\mathscr E$ & & & expressions \\[1mm]
$\mathscr T$ & $\con{C},\,\con{D},\,\dots$ & & tags (constructors) \\[1mm]
$\Sigma$ & $\sigma$ & $\mathscr X\to\mathscr V$ & bindings (a partial map from\\
& & & variables to values) \\[1mm]
$\Sigma_{\mathscr X}$ & $\inbr{S,\,\sigma}$ & $2^{\mathscr X}\times\Sigma$ & local scopes (sets of variables\\
& & & and their bindings) \\[1mm]
$St$ & $\inbr{\sigma_g,\,ss}$ & $\Sigma\times\Sigma^*_{\mathscr X}$ & states (global bindings and stacks\\
& & & of local scopes) \\[1mm]
$\mathcal W$ & $w$ & & worlds\\[1mm]
$\mathcal L$ & $l$ & & locations \\[1mm]
$\mathcal M$ & $\mu$ & $\mathcal L\to\mathcal C$ & abstract memory (a partial map from\\
& & & locations to composite values) \\[1mm]
$\mathcal C$ & $c$ & $St\times\mathcal{M}\times\mathcal{W}$ & configurations (state, memory and world)\\[2mm]
$\mathcal P$ & & $\mathbb Z^\bot\uplus$ & primitive values (integer or default\\
& & $\primi{ref}{\mathscr{X}}\uplus$ & value, references to variables or\\
& & $\primi{elemRef}{\mathcal L\;\mathbb N}$ & array elements)\\[2mm]
$\mathcal F$ & & $\mathscr X^*\times\mathscr E \times \mathbb N$ & function values (argument names, body,\\
& & & nesting level)\\[1mm]
$\mathcal V$ & $v$ & $\mathcal P\uplus \mathcal L$ & values (primitive values or locations) \\[1mm]
$\mathcal C$ & & $Arr\uplus Sexp \uplus Clo$ & composite values (arrays, S-expressions, \\
& & & or closures) \\[1mm]
$Arr$ & & $\mathbb N\times (\mathbb N\to\mathcal V)$ & arrays (length and element function) \\[1mm]
$Sexp$ & & $\mathscr T \times Arr$ & S-expressions (tag and array of subvalues) \\[1mm]
$Clo$ & & $\mathscr X^* \times\mathscr E\times\Sigma^*_{\mathscr X}$ & closures (argument names, function body\\
& & & and a stack of local scopes)
\end{tabular}
\caption{Basic Categories}
\label{categories}
\end{table}

78
spec/02.02.abstract_syntax.tex Normal file
View file

@ -0,0 +1,78 @@
\section{Abstract Syntax}
Abstract syntax defines the shapes of \emph{abstract syntax trees} (AST). We give the formation rules in a \emph{mixfix} form to
reflect the concrete syntax (presented in Section~\ref{sec:concrete_syntax}); however, the intended meaning is \emph{prefix},
thus the formation rule for, for example, conditional expression
\[
\mbox{\llang{if $\;\mathscr E\;$ then $\;\mathscr E\;$ else $\;\mathscr E$}}
\]
defines the following AST fragment:
\[
\mbox{\llang{if$\,(\mathscr E,\,\mathscr E,\,\mathscr E)$}}
\]
The root syntactic category for the language is \emph{compilation unit} $\mathscr U$, which is an expression in a contexts of
a group of top-level \emph{definitions} $\mathscr D$:
\[
\begin{array}{rcll}
\mathscr S & :: & \mathscr D^*\quad \mathscr E & \mbox{--- scope expression}\\
\mathscr D & :: & \mbox{\lstinline|var $\;\mathscr X$|} & \mbox{--- local variable definition} \\
& & \mbox{\lstinline|fun $\;\mathscr X\;$ ($\mathscr X^*$) \{$\;\mathscr S\;$\}|} & \mbox{--- function definition}\\
\mathscr U & :: & \mathscr S & \mbox{--- compilation unit}
\end{array}
\]
The core syntactic category for the language is \emph{expressions} $\mathscr E$. The following kinds of
expressions are distinguished:
\[
\begin{array}{rcll}
\mathscr E & :: & \mathscr X & \mbox{--- variable} \\
& & \mathbb N & \mbox{--- constant} \\
& & \lstinline|{ $\mathscr S\;$ }| & \mbox{--- nested scope} \\
& & \mathscr E \otimes \mathscr E & \mbox{--- binary expression} \\
& & \mathscr E\;\lstinline|($\mathscr E^*$)| & \mbox{--- call} \\
& & \llang{fun ($\mathscr X^*$) \{$\mathscr S$\}} & \mbox{--- lambda expression} \\
& & \llang{[$\mathscr E^*$]} & \mbox{--- array} \\
& & \llang{$\mathscr E\;$ [$\mathscr E$]} & \mbox{--- array element} \\
& & \llang{$\mathscr T\;$ ($\mathscr E^*$)} & \mbox{--- S-expression} \\
& & \mathscr E \;\mbox{\lstinline|:=|} \;\mathscr E & \mbox{--- assignment} \\
& & \mathscr E \mbox{\lstinline|;|}\; \mathscr E & \mbox{--- sequential expression} \\
& & \llang{if $\;\mathscr E\;$ then $\;\mathscr E\;$ else $\;\mathscr E$} & \mbox{--- conditional expression} \\
& & \llang{while $\;\mathscr E\;$ do $\;\mathscr E$} & \mbox{--- loop expression} \\
& & \llang{case $\;\mathscr E\;$ ($\mathscr P$ -> $\mathscr E$)$^+$} & \mbox{--- pattern matching} \\
& & \mbox{\lstinline|skip|} & \mbox{--- empty expression} \\
& & \bot & \mbox{--- default value} \\
& & \llang{ref ($\mathscr X$)} & \mbox{--- reference to variable} \\
& & \llang{elemRef ($\mathscr E$,$\;\mathscr E$)} & \mbox{--- reference to array element} \\
& & \llang{ignore ($\mathscr E$)} & \mbox{--- ignore expression}
\end{array}
\]
Note, in the formation rule for binary expressions the symbol ``$\otimes$'' is left undefined. The actual assortment of
binary operators is given in Section~\ref{sec:expressions}.
The last four kinds of expressions (``$\bot$'', \llang{ref}, \llang{elemRef} and \llang{ignore}) are \emph{internal} in the sense that
they are not represented explicitly in the concrete syntax; instead, they are \emph{inferred} using the attribute system described
in Section~\ref{sec:wellformedness}.
The last category is \emph{patterns} $\mathscr P$. Patterns are used in \lstinline|case|-expressions to match the values against:
\[
\begin{array}{rcll}
\mathscr P & :: & \_ & \mbox{--- wildcard} \\
& & \mathbb N & \mbox{--- constant} \\
& & \llang{[$\mathcal P^*$]} & \mbox{--- array}\\
& & \llang{$\mathcal T\;$($\mathcal P^*$)} & \mbox{--- S-expression}\\
& & \llang{array} & \mbox{--- array type}\\
& & \llang{sexp} & \mbox{--- S-expression type}\\
& & \llang{fun} & \mbox{--- closure type}\\
& & \llang{val} & \mbox{--- value type}\\
& & \llang{box} & \mbox{--- reference type}
\end{array}
\]

224
spec/02.03.operational_semantics.tex Normal file
View file

@ -0,0 +1,224 @@
\section{Operational Semantics}
The semantics for the language is given in the form of a \emph{big-step} operational semantics with the
main transition relation being
\[
\setarrow{\xRightarrow}
\trans{c}{e}{\inbr{c^\prime,\,v}}
\]
for some \emph{configurations} $c, c^\prime$, some expression $e$ and some value $v$. Besides this main relation a few supplementary are
used to handle the semantics of other syntactic categories.
\subsection{States, Worlds and Configurations}
A configuration is a triple of a \emph{state}, a \emph{memory}, and a \emph{world}. A world is an abstract entity to accomodate side-effects
potentially performed as the execution of a program proceeds, and a memory is a patrial function which maps \emph{locations} to
\emph{composite values} (arrays, S-expressions, and closures).
A state is a pair
\[
\inbr{\sigma_g,\,ss}
\]
of a \emph{global} binding and a stack (list) of local scopes, each of which is a pair
\[
\inbr{S,\,\sigma}
\]
where $S$ is a set of variable names and $\sigma$ is local bindings. For states we define two primitives to read a variable
value in a state
\[
\begin{array}{rcl}
\inbr{\sigma_g,\,\epsilon}\,x & = &\sigma_g\,x\\[2mm]
\inbr{\sigma_g,\,\inbr{S,\,\sigma}\circ ss}\,x & = & \left\{\begin{array}{rcl}
\sigma\,x &,& x\in S\\
\inbr{\sigma_g,\,ss}\,x &,&x\not\in S
\end{array}
\right.
\end{array}
\]
and to reassign a variable to another value:
\[
\begin{array}{rcl}
\inbr{\sigma_g,\,\epsilon}\,[x\gets v] & = &\inbr{\sigma_g\,[x\gets v],\,\epsilon}\\[2mm]
\inbr{\sigma_g,\,\inbr{S,\,\sigma}\circ ss}\,[x\gets v] & = & \left\{\begin{array}{rcl}
\inbr{\sigma_g,\,\inbr{S,\,\sigma\,[x\gets v]}\circ ss} &,& x\in S\\[1mm]
\inbr{\sigma^\prime_g,\,\inbr{S,\,\sigma}\circ ss^\prime}\,x &,&x\not\in S\\
& &\inbr{\sigma^\prime_g,\,ss^\prime}=\inbr{\sigma_g,\,ss}\,[x\gets v]
\end{array}
\right.
\end{array}
\]
\subsection{Expressions}
To give the semantics for the expressions we introduce a supplementary transition ``$\xRightarrow{}^*$'', which described a left-to-right computation
of the \emph{list} of expressions and results, correspondingly, in a final configuration and a \emph{list} of values:
\setarrow{\xRightarrow}
\setsubarrow{\hskip-0,3em^*\hskip0.3em}
\[
\trans{c}{\epsilon}{\inbr{c,\,\epsilon}}\ruleno{Expr$^*_\epsilon$}
\]
\[
\trule{{\setsubarrow{}\trans{c}{e}{\inbr{c^\prime,\,v}}}\qquad\trans{c^\prime}{\omega}{\inbr{c^{\prime\prime},\,\psi}}}
{\trans{c}{e\circ\omega}{\inbr{c^{\prime\prime},\,v\circ\psi}}}\ruleno{Expr$^*$}
\]
Operational semantics for core expressions is given in Fig.~\ref{semantics:core}. Note, the semantics of binary expressions is
given in terms of a primitive ``$\oplus$'', which is left undefined. The concrete semantics of binary operators is
given in Section~\ref{sec:expressions}.
\begin{figure}[t]
\setsubarrow{}
\[
\trans{c}{z}{\inbr{c,\,z}}\ruleno{Const}
\]
\[
\trans{\inbr{s,\,m,\,w}}{x}{\inbr{\inbr{s,\,m,\,w},\,s\,x}}\ruleno{Var}
\]
\[
\trans{c}{\llang{ref $\;x$}}{\inbr{c,\,\primi{ref}{x}}}\ruleno{Ref}
\]
\[
\trule{\setsubarrow{\hskip-0,3em^*\hskip0.3em}\trans{c}{l\circ r}{\inbr{c^\prime,\,w\circ v}}}
{\trans{c}{l\oplus r}{\inbr{c^\prime,\,w\otimes v}}}\ruleno{Binop}
\]\vskip1mm
\[
\trans{c}{\llang{skip}}{\inbr{c,\,\bot}}\ruleno{Skip}
\]
\[
\trule{\setsubarrow{\hskip-0,3em^*\hskip0.3em}\trans{c}{l\circ r}{\inbr{\inbr{s,\,m,\,w},\,[\primi{ref}{x}]\circ[v]}}}
{\trans{c}{\llang{$l\;$ := $\;r$}}{\inbr{\inbr{s\,[x\gets v],\,m,\,w},\,v}}}\ruleno{Assign}
\]\vskip1mm
\[
\trule{\trans{c_1}{S_1}{\inbr{c^\prime,\,v}}\qquad \trans{c^\prime}{S_2}{c_2}}
{\trans{c_1}{S_1\llang{;}\;S_2}{c_2}}\ruleno{Seq}
\]\vskip1mm
\[
\trule{\trans{c}{e}{\inbr{c^\prime,\,n}}\qquad n\ne 0\qquad \trans{c^\prime}{S_1}{c^{\prime\prime}}}
{\trans{c}{\llang{if $\ \ e\ \ $ then $\ \ S_1\ \ $ else $\ \ S_2\ \ $}}{c^{\prime\prime}}}
\ruleno{If-True}
\]\vskip1mm
\[
\trule{\trans{c}{e}{\inbr{c^\prime,\,0}}\qquad \trans{c^\prime}{S_2}{c^{\prime\prime}}}
{\trans{c}{\llang{if $\ \ e\ \ $ then $\ \ S_1\ \ $ else $\ \ S_2\ \ $}}{c^{\prime\prime}}}
\ruleno{If-False}
\]\vskip1mm
\[
\trule{\trans{c}{e}{\inbr{c^\prime,\,n}}\quad n\ne 0\quad\trans{c^\prime}{S}{\inbr{c^{\prime\prime},\,v}}\quad\trans{c^{\prime\prime}}{\llang{while $\ \ e\ \ $ do $\ \ S\ \ $}}{c^{\prime\prime\prime}}}
{\trans{c}{\llang{while $\ \ e\ \ $ do $\ \ S\ \ $}}{c^{\prime\prime\prime}}}
\ruleno{While-True}
\]\vskip1mm
\[
\trule{\trans{c}{e}{\inbr{c^\prime,\,0}}}
{\trans{c}{\llang{while $\ \ e\ \ $ do $\ \ S\ \ $}}{\inbr{c^\prime,\,\bot}}}
\ruleno{While-False}
\]
\caption{Big-step Operational Semantics for Core Expressions}
\label{semantics:core}
\end{figure}
\subsubsection{Arrays and S-expressions}
Arrays and S-expressions allow to manipulate \emph{composite valuues} which are kept in \emph{memory}. A memory is a partial function $m$
which maps \emph{locations} into composite values. Locations are abstractions of real-world memory addresses; the set of locations
is considered to be linearly ordered. We define the following primitive
\[
\primi{new}\,m\,v=\inbr{l,\,m\,[l\gets v]}\mbox{ where }l=min\{l\in\mathcal{L}\mid m\,(l)\mbox{ undefined}\}
\]
which takes a memory $m$ and a composite value $v$ and returns a \emph{new} location $l$ (previously unoccupied) and a new \emph{memory} which
associates $l$ with $v$ and preserves other associations intact.
Arrays are represented as pairs
\[
\inbr{n,\,f}
\]
where $n\in\mathbb N$ is a lengths and $f : \mathbb{N}\to\mathcal{V}$~--- element function which maps indices into values. It is assumed, that
$\primi{dom}{f}=[0\dots n-1]$.
S-expressions are represented as pairs
\[
\inbr{t,\,s}
\]
where $t$ is a \emph{tag} and $s$ is an array of subexpressions. The semantics of arrays and subexpressions is given in Fig.~\ref{semantics:arrays}.
\begin{figure}
\setsubarrow{}
\[
\trule{\setsubarrow{\hskip-0,3em^*\hskip0.3em}
\begin{array}{c}
\trans{c}{e_1\circ\dots\circ e_k}{\inbr{\inbr{s,\,m,\,w}, v_1\circ\dots\circ v_k}}\\[2mm]
\inbr{l,\,m^\prime}=\primi{new}{m\,\inbr{k-1,\,i\mapsto v_{i+1}}}
\end{array}
}
{\trans{c}{\llang{[$e_1,\dots,e_k$]}}{\inbr{\inbr{s,\,m^\prime,\,w},\,l}}}\ruleno{Array}
\]\\[2mm]
\[
\trule{\setsubarrow{\hskip-0,3em^*\hskip0.3em}
\begin{array}{c}
\trans{c}{e_1\circ\dots\circ e_k}{\inbr{\inbr{s,\,m,\,w}, v_1\circ\dots\circ v_k}}\\[2mm]
\inbr{l,\,m^\prime}=\primi{new}{m\,\inbr{t,\,\inbr{k-1,\,i\mapsto v_{i+1}}}}
\end{array}
}
{\trans{c}{\llang{$t\,$($e_1,\dots,e_k$)}}{\inbr{\inbr{s,\,m^\prime,\,w},\,l}}}\ruleno{Sexp}
\]\\[2mm]
\[
\trule{\setsubarrow{\hskip-0,3em^*\hskip0.3em}
\begin{array}{c}
\trans{c}{e_1\circ e_2}{\inbr{\inbr{s,\,m,\,w},\,l\circ i}}\\[2mm]
l\in\mathcal{L}\\
m\,(l)=\inbr{k,\,f}\mbox{ or }m\,(l)=\inbr{t,\,\inbr{k, f}}\\
i\in[0\dots k-1]
\end{array}
}
{\trans{c}{\llang{$e_1\,$[$e_2$]}}{\inbr{\inbr{s,\,m,\,w},\,f\,(i)}}}\ruleno{Elem}
\]\\[2mm]
\[
\trule{\setsubarrow{\hskip-0,3em^*\hskip0.3em}
\begin{array}{c}
\trans{c}{e_1\circ e_2}{\inbr{\inbr{s,\,m,\,w},\,l\circ i}}\\[2mm]
l\in\mathcal{L}\\
m\,(l)=\inbr{k,\,f}\mbox{ or }m\,(l)=\inbr{t,\,\inbr{k, f}}\\
i\in[0\dots k-1]
\end{array}
}
{\trans{c}{\llang{elemRef ($e_1$,$\ \ e_2$)}}{\inbr{\inbr{s,\,m,\,w},\,\primi{elemRef}{l\;i}}}}\ruleno{ElemRef}
\]\\[2mm]
\[
\trule{\setsubarrow{\hskip-0,3em^*\hskip0.3em}
\begin{array}{c}
\trans{c}{l\circ r}{\inbr{\inbr{s,\,m,\,w},\,[\primi{elemRef}{l\;i}]\circ[v]}}\\[2mm]
m^\prime=\left\{\begin{array}{rcl}
m\,[l\gets\inbr{k,\,f\,[i\gets v]}] &,&m\,(l)=\inbr{k,\,f}\\
m\,[l\gets\inbr{t,\,\inbr{k,\,f\,[i\gets v]}}] &,&m\,(l)=\inbr{t,\,\inbr{k,\,f}}
\end{array}
\right.
\end{array}
}
{\trans{c}{\llang{$l\;$ := $\;r$}}{\inbr{\inbr{s,\,m,\,w},\,v}}}\ruleno{AssignElem}
\]
\caption{Big-step Operational Semantics for Arrays and S-expressions}
\label{semantics:arrays}
\end{figure}
\subsubsection{Pattern Matching}
\subsubsection{Declarations}
\subsubsection{Functions and Closures}

46
spec/02.04.wellformedness.tex Normal file
View file

@ -0,0 +1,46 @@
\section{Well-formed Expressions}
\label{sec:wellformedness}
{
\newcommand{\Ref}{\primi{Ref}{}}
\newcommand{\Val}{\primi{Val}{}}
\newcommand{\Void}{\primi{Void}{}}
\newcommand{\Weak}{\primi{Weak}{}}
\renewcommand{\withenv}[2]{{#2}\,:\,{#1}}
\begin{comment}
\withenv{\Ref}{\llang{ref $\;x$}} & \withenv{\Val}{x}& \withenv{\Void}{\llang{ignore $\;x$}} & x \in \mathscr X\\
& \withenv{\Val}{z}& \withenv{\Void}{\llang{ignore $\;z$}} & z \in \mathbb N \\
& \trule{\withenv{\Val}{l},\quad\withenv{\Val}{r}}
{\withenv{\Val}{l\oplus r}} &
\trule{\withenv{\Val}{l},\quad\withenv{\Val}{r}}
{\withenv{\Void}{\llang{ignore $\;l\oplus r$}}} & \\
& & \withenv{\Void}{\llang{skip}} & \\
& \trule{\withenv{\Ref}{l},\quad\withenv{\Val}{r}}
{\withenv{\Val}{\llang{$l\;$ := $\; r$}}} &
\trule{\withenv{\Ref}{l},\quad\withenv{\Val}{r}}
{\withenv{\Void}{\llang{ignore ($l\;$ := $\; r$})}} & \\
& & \withenv{\Void}{\llang{read ($x$)}} & \\
& & \trule{\withenv{\Val}{e}}{\withenv{\Void}{\llang{write ($e$)}}} & \\[2mm]
\trule{\withenv{\Void}{s_1},\quad\withenv{a}{s_2}}{\withenv{a}{\llang{$s_1\;$;$\;s_2$}}}&
\trule{\withenv{\Val}{e},\quad\withenv{a}{s_1},\quad\withenv{a}{s_2}}{\withenv{a}{\llang{if $\;e\;$ then $\;s_1\;$ else $\;s_2$}}}&
\trule{\withenv{\Val}{e},\quad\withenv{\Void}{s}}{\withenv{\Void}{\llang{while $\;e\;$ do $\;s$}}}& \\[2mm]
& \trule{\withenv{\Val}{e},\quad\withenv{\Void}{s}}{\withenv{\Void}{\llang{repeat $\;s\;$ until $\;e$}}} & &
\end{comment}
\renewcommand{\arraystretch}{3}
\[
\begin{array}{cc}
\trule{x \in \mathscr X}{\withenv{\Weak}{x}} & \trule{z \in \mathbb N }{\withenv{\Weak}{z}}\\
\trule{\withenv{\Val}{l},\quad\withenv{\Val}{r}}
{\withenv{\Weak}{l\oplus r}} & \withenv{\Weak}{\llang{skip; $\;\bot$}} \\
\trule{\withenv{\Ref}{l},\quad\withenv{\Val}{r}}
{\withenv{\Weak}{\llang{$l\;$ := $\; r$}}} & \withenv{\Weak}{\llang{read ($x$); $\;\bot$}} \\
\trule{\withenv{\Val}{e}}{\withenv{\Weak}{\llang{write ($e$); $\;\bot$}}} & \trule{\withenv{\Val}{e},\quad\withenv{\Void}{s}}{\withenv{\Weak}{\llang{while $\;e\;$ do $\;s\;$ od; $\;\bot$}}} \\
\trule{\withenv{\Val}{e},\quad\withenv{\Void}{s}}{\withenv{\Weak}{\llang{(repeat $\;s\;$ until $\;e$); $\;\bot$ }}} &
\end{array}
\]
}

47
spec/02.abstract_syntax_and_semantics.tex
View file

@ -1 +1,48 @@
\chapter{Abstract Syntax and Semantics}
In this section we present abstract syntax and semantics of \lama. The syntax is given in the form of \emph{abstract syntax tree} (AST) format,
and the semantics~--- in the form of a \emph{big-step operational semantics}. In addition we present a part of static semantics of the language
in the form of \emph{attribute system}, which can be considered as a form of simplictic type system. Only the core constructs of the languge
are considered here.
Basic syntactic and semantic categories and their brief descriptions are given in Tab.~\ref{categories}. Apart from those, we will use the
following notations: for a mapping $f : X\to Y$ we use the following definition:
\[
f [x\gets y] = \lambda\,z\,.\,
\left\{
\begin{array}{rcl}
y &,& x = z \\
f\;x &,& x\neq z
\end{array}
\right.
\]
Empty mapping (undefined everywhere) is denoted $\Lambda$, the domain of a mapping $f$~--- $\primi{dom}{f}$, and we abbreviate
\[
\Lambda[x_1\gets y_1][x_2\gets y_2]\dots[x_k\gets y_k]
\]
as
\[
[x_1\gets y_1,\,x_2\gets y_2,\,\dots,\,x_k\gets y_k]
\]
For lists, we use notation $h\circ t$ for decomposition lists into heads and tails, $\epsilon$~--- for empty lists,
$|l|$~--- for list length and
\[
l[i:j]\qquad l[:n]\qquad l[n:]
\]
for taking sublists from $i$-th to $j$-th elements, $n$-last and $n$-first elements respectively; the numbering
of elements is left-to-right, starting from $0$. We also will enclose elements of lists which have a
composite structure in square brackets ``$[\dots]$'' to separate them properly.
\input{02.01.categories}
\FloatBarrier
\input{02.02.abstract_syntax}
\input{02.03.operational_semantics}
%\input{02.04.wellformedness}

26
spec/lama-spec.tex
View file

@ -1,5 +1,8 @@
\documentclass{book}
\newcommand\hmmax{0}
\newcommand\bmmax{0}
\usepackage{amssymb, amsmath}
\usepackage{alltt}
\usepackage{pslatex}
@ -42,12 +45,12 @@
\def\subarrow{}
\newcommand{\setsubarrow}[1]{\def\subarrow{#1}}
\newcommand{\trule}[2]{\frac{#1}{#2}}
\newcommand{\trule}[2]{\dfrac{#1}{#2}}
\newcommand{\crule}[3]{\frac{#1}{#2},\;{#3}}
\newcommand{\withenv}[2]{{#1}\vdash{#2}}
\newcommand{\trans}[3]{{#1}\transarrow{\padding{\textstyle #2}\padding}\subarrow{#3}}
\newcommand{\trans}[3]{{#1}\transarrow{\padding{\textstyle #2}\padding}{\subarrow}{#3}}
\newcommand{\ctrans}[4]{{#1}\transarrow{\padding#2\padding}\subarrow{#3},\;{#4}}
\newcommand{\llang}[1]{\mbox{\lstinline[mathescape]|#1|}}
\newcommand{\llang}[1]{\mbox{\lstinline[language=abslama,mathescape]|#1|}}
\newcommand{\pair}[2]{\inbr{{#1}\mid{#2}}}
\newcommand{\inbr}[1]{\left<{#1}\right>}
\newcommand{\highlight}[1]{\color{red}{#1}}
@ -71,6 +74,7 @@
\renewcommand{\emptyset}{\varnothing}
\newcommand{\dom}[1]{\mathtt{dom}\;{#1}}
\newcommand{\primi}[2]{\mathbf{#1}\;{#2}}
\newcommand{\con}[1]{\mathbf{#1}}
\newcommand{\lama}{$\lambda\kern -.1667em\lower -.5ex\hbox{$a$}\kern -.1000em\lower .2ex\hbox{$\mathcal M$}\kern -.1000em\lower -.5ex\hbox{$a$}$\xspace}
%\newcommand{\sial}{S\textit{\lower -.5ex\hbox{I}\kern -.1667em\lower .5ex\hbox {A}}\kern -.125emL\@\xspace}
\definecolor{light-gray}{gray}{0.90}
@ -85,6 +89,22 @@
\newcommand{\descr}[2]{\smallskip{#1}\begin{itemize}[noitemsep,topsep=0pt]\item[]{#2}\end{itemize}}
\lstdefinelanguage{abslama}{
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,ref,ignore,elemRef},
sensitive=true,
basicstyle=\small,
%commentstyle=\scriptsize\rmfamily,
keywordstyle=\ttfamily\bfseries,
identifierstyle=\ttfamily,
basewidth={0.5em,0.5em},
columns=fixed,
fontadjust=true,
literate={->}{{$\to$}}3,
morecomment=[s][\ttfamily]{(*}{*)},
morecomment=[l][\ttfamily]{--}
}
\lstdefinelanguage{lama}{
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},