From b98314cdc0420c72f2521f3c084ecccc574cf74d Mon Sep 17 00:00:00 2001 From: pimjager Date: Thu, 9 Jun 2016 16:21:23 +0200 Subject: [PATCH] Working sem part of report --- deliverables/report/intro.tex | 2 +- deliverables/report/report.tex | 7 ++++-- deliverables/report/sem.tex | 39 ++++++++++++++++++++++++++++++++++ 3 files changed, 45 insertions(+), 3 deletions(-) diff --git a/deliverables/report/intro.tex b/deliverables/report/intro.tex index c333738..86e78d6 100644 --- a/deliverables/report/intro.tex +++ b/deliverables/report/intro.tex @@ -3,7 +3,7 @@ \SPLC{} is a program written in the purely functional lazy programming language Clean\footnote{\url{http://clean.cs.ru.nl/Clean}}. \SPLC{} has a standardized UNIX like command line interface and functions as a filter in a way that it -processes standard input in standard output. Default command line argument such +processes standard input to standard output. Default command line argument such as \texttt{--version} and \texttt{--help} provide the expected output. To illustrate all the command line interface options the output of \texttt{spl --help} is given in Listing~\ref{lst:splchelp}. diff --git a/deliverables/report/report.tex b/deliverables/report/report.tex index 5131eb0..ff25cb7 100644 --- a/deliverables/report/report.tex +++ b/deliverables/report/report.tex @@ -17,8 +17,11 @@ } \newcommand{\SPLC}{\texttt{SPLC}} -\newcommand{\SPL}{\texttt{SPLC}} -\newcommand{\SSM}{\texttt{SPLC}} +\newcommand{\SPL}{\texttt{SPL}} +\newcommand{\SSM}{\texttt{SSM}} +\def\AST/{\texttt{AST}} + +\let\tt\texttt \begin{document} \maketitle diff --git a/deliverables/report/sem.tex b/deliverables/report/sem.tex index c6003b4..66fda2c 100644 --- a/deliverables/report/sem.tex +++ b/deliverables/report/sem.tex @@ -14,3 +14,42 @@ %A concise but precise description of how the work was divided amongst the %members of %the team. + +The semantic analysis phase asses if a -grammatically correct- program is also +semantically correct and decorates the program with extra information it +finds during this checking. The input of the semantic analysis is an \AST/ of +the +parsed program, its output is either a semantically correct and completely typed +\AST/ plus the environment in which it was typed (for debug purposes), or it is +an error describing the problem with the \AST/. + +During this analysis \SPLC checks four properties of the program: +\begin{enumerate} + \item That no functions are declared with the same name + \item That \tt{main} is of type \tt{(-> Void)} + \item That the program includes a main function + \item That the program is correctly typed +\end{enumerate} +The first three steps are simple sanity checks which are coded in slightly over +two dozen lines of Clean code. The last step is a Hindley Milner type inference +algorithm, which is a magnitude more complex. This last step also decorates the +\AST/ with inferred type information. + +\subsection{Sanity checks} +The sanity checks are defined as simple recursive functions over the function +declarations in the AST. We will very shortly describe them here. + +\begin{description} + \item [No duplicate functions] This function checks that the program does + not contain top level functions sharing the same name. Formally: + $ \forall f \in \textrm{functions} \ldotp \neg + \exists g \in \textrm{functions} \setminus \{f\} \ldotp + f.\textrm{name} = g.\textrm{name}$ + \item [\tt{main} should have type \tt{->Void}] Our semantics of \SPL{} + require the main function to take no arguments and to not return a + value. Formally: $\forall f \in \textrm{functions} \ldotp + f.\textrm{name} = \textrm{'main'} \Rightarrow + \textit{typeof}\textrm{(main)} = \rightarrow\textrm{Void} $ + \item [The program should have a main function] $\exists f \in + \textrm{functions} \ldotp f.\textrm{name} = \textrm{'main'}$ +\end{description} \ No newline at end of file -- 2.20.1