diff --git a/lama-spec.pdf b/lama-spec.pdf index 11d295702..32de3eb86 100644 Binary files a/lama-spec.pdf and b/lama-spec.pdf differ diff --git a/spec/01.01.general_characteristics.tex b/spec/01.01.general_characteristics.tex deleted file mode 100644 index e4000c073..000000000 --- a/spec/01.01.general_characteristics.tex +++ /dev/null @@ -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} diff --git a/spec/01.02.notation.tex b/spec/01.02.notation.tex deleted file mode 100644 index 8ae0fb166..000000000 --- a/spec/01.02.notation.tex +++ /dev/null @@ -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] -\] diff --git a/spec/01.03.values.tex b/spec/01.03.values.tex deleted file mode 100644 index c50fa1006..000000000 --- a/spec/01.03.values.tex +++ /dev/null @@ -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} diff --git a/spec/01.introduction.tex b/spec/01.introduction.tex index 99522309b..2022b01c6 100644 --- a/spec/01.introduction.tex +++ b/spec/01.introduction.tex @@ -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} diff --git a/spec/02.01.categories.tex b/spec/02.01.categories.tex new file mode 100644 index 000000000..de44ac508 --- /dev/null +++ b/spec/02.01.categories.tex @@ -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} diff --git a/spec/02.02.abstract_syntax.tex b/spec/02.02.abstract_syntax.tex new file mode 100644 index 000000000..9d4363928 --- /dev/null +++ b/spec/02.02.abstract_syntax.tex @@ -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} +\] + diff --git a/spec/02.03.operational_semantics.tex b/spec/02.03.operational_semantics.tex new file mode 100644 index 000000000..72e0ae1e5 --- /dev/null +++ b/spec/02.03.operational_semantics.tex @@ -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} + diff --git a/spec/02.04.wellformedness.tex b/spec/02.04.wellformedness.tex new file mode 100644 index 000000000..73c2444b4 --- /dev/null +++ b/spec/02.04.wellformedness.tex @@ -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} + \] + +} + diff --git a/spec/02.abstract_syntax_and_semantics.tex b/spec/02.abstract_syntax_and_semantics.tex index d8b0dbfe6..06ad09d5b 100644 --- a/spec/02.abstract_syntax_and_semantics.tex +++ b/spec/02.abstract_syntax_and_semantics.tex @@ -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} diff --git a/spec/lama-spec.tex b/spec/lama-spec.tex index 08603adb7..a88524b0c 100644 --- a/spec/lama-spec.tex +++ b/spec/lama-spec.tex @@ -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}, diff --git a/src/version.ml b/src/version.ml index d080f8174..e538131df 100644 --- a/src/version.ml +++ b/src/version.ml @@ -1 +1 @@ -let version = "Version 1.10, 7c7ef67e1, Mon Feb 1 09:52:28 2021 +0300" +let version = "Version 1.10, 59f78fe38, Mon Feb 1 10:39:12 2021 +0300"