small fix eval

diff --git a/deliverables/report/sem.tex b/deliverables/report/sem.tex
index 9aa5af9..67d74db 100644 (file)
--- a/deliverables/report/sem.tex
+++ b/deliverables/report/sem.tex
@@ -6,8 +6,8 @@ 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{} applies one \AST{} transformation and checks four
-properties of the program:
+During this analysis \SPLC{} applies two transformation and checks four
+properties of the \AST{}:
 \begin{enumerate}
        \item That no functions are declared with the same name
        \item That \tt{main} is of type \tt{(-> Void)}
@@ -61,7 +61,8 @@ assembly code for different types and thus need not to be specified.
 
 \subsection{Type inference}
 \SPLC{} features a \emph{Hindley-Milner} type inference algorithm based on the
-algorithm presented in the slides. It supports full polymorphism and can infer
+algorithm presented in the slides. \SPLC{} supports full polymorphism and can 
+infer
 omitted types. It does not support multiple recursion and all functions and
 identifiers need to be declared before they can be used. In essence the program
 is typed as nested \tt{let .. in ..} statements.
@@ -71,7 +72,7 @@ Listing~\ref{lst:types} shows the \ADT{} representing types in \SPLC{}. Most of
 these are self explanatory, however typing of functions requires some special
 attention. \SPLC{}s extension of higher order functions requires that the type
 system can distinguish if an
-expression represents a type $a$ or a functions which takes no input and returns
+expression represents a type $a$ or a function which takes no input and returns
 a value of type $a$ (we write: $\rightarrow a$). The latter is represented by
 the \CI{FuncType}.
 
@@ -109,7 +110,7 @@ unified in the \tt{Typing} monad, which is defined as \CI{Typing a :== StateT
 infinite list of fresh \tt{TVars}, which are just an alias of \tt{String}.
 
 \subsubsection{Substitution and Unification}
-In \SPLC{} substitutions are defined as map from type variables to concrete
+In \SPLC{} substitutions are defined as map from type variables to
 types. Composing of substitutions is then simply taking the union of two
 substitutions and substituting the first substitution over the types in the
 second substitution. We write $\star$ for a substitution and $\star_0$ for the
@@ -123,7 +124,7 @@ trivially promoting unification to the contained types, or checking directly if
 the types to be unified are equal.
 
 \begin{equation} \label{eq:unifyId}
-       \infer{\alpha \unif \tau = [tv \mapsto \tau]}
+       \infer{\alpha \unif \tau = [\alpha \mapsto \tau]}
                        {\alpha \notin ftv(\tau)}
 \end{equation}
 
@@ -195,7 +196,7 @@ and accumulating the resulting types, substitutions, etc.
                        &(\texttt{fold } (\rightarrow) \texttt{ } \alpha \texttt{ } \tau^*)
                                \unif \tau^e = \star_2
                        &\star = \star_2 \cdot \star_1
-                       &\texttt{fold apfs } \tau \textit{ fs}^* = \tau^e
+                       &\texttt{fold apfs } \tau^e \textit{ fs}^* = \tau^r
                }
        }
 \end{equation}