From: pimjager <pim@pimjager.nl>
Date: Thu, 9 Jun 2016 14:21:23 +0000 (+0200)
Subject: Working sem part of report
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=b98314cdc0420c72f2521f3c084ecccc574cf74d;p=cc1516.git

Working sem part of report
---

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