sdfsdf

diff --git a/deliverables/report/infRules.tex b/deliverables/report/infRules.tex
new file mode 100644 (file)
index 0000000..e69de29

diff --git a/deliverables/report/report.tex b/deliverables/report/report.tex
index e8deb22..36446e8 100644 (file)
--- a/deliverables/report/report.tex
+++ b/deliverables/report/report.tex
@@ -24,6 +24,7 @@
 \newcommand{\Yard}{\textsc{Yard}}
 \newcommand{\AST}{\emph{AST}}
 \newcommand{\ADT}{\emph{ADT}}
+\newcommand{\Clean}{\emph{Clean}}
 
 \let\tt\texttt
 
@@ -55,4 +56,8 @@
        firstline=6,
        lastline=42]{../../AST.dcl}
 
+\newpage
+\subsection{Inference rules} \label{sec:infRules}
+\input{infRules.tex}
+
 \end{document}

diff --git a/deliverables/report/sem.tex b/deliverables/report/sem.tex
index 6b49e68..fde8f01 100644 (file)
--- a/deliverables/report/sem.tex
+++ b/deliverables/report/sem.tex
@@ -30,31 +30,35 @@ During this analysis \SPLC{} checks four properties of the program:
        \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 AST transformation for lambdas
        \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
+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}
+\subsection{AST transformation for lambdas}
+
+% \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}
 
 \subsection{Type inference}
 \SPLC{} features a Hindley-Milner type inference algorithm based on the
@@ -66,7 +70,7 @@ essence the program is typed as nested \tt{let .. in ..} statements.
 \subsubsection{Types}
 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 is Higher order functions, this is described
+attention. \SPLC{}s extension is higher order functions, this is described
 in more detail in Section~\ref{sec:ext}. These require a change to the
 type system, which we will already describe here.
 
@@ -83,7 +87,7 @@ type then in itself can be a function.
 \begin{lstlisting}[
        label={lst:types},
        caption={SPLC types},
-       language=clean]
+       language=Clean]
 :: Type 
        = TupleType (Type, Type)        -- (t1, t2)
        | ListType type                         -- [t]
@@ -93,7 +97,7 @@ type then in itself can be a function.
        | CharType
     | VoidType
        | FuncType Type                         -- (-> t)
-    | (->>) infixl 7 Type Type         -- (t1 -> t2)
+    | (\->>) infixl 7 Type Type        -- (t1 -> t2)
 \end{lstlisting}
 
 \subsubsection{Environment}
@@ -138,11 +142,14 @@ yielded type is the type returned by a return statement if one is present, or
 Void otherwise.
 
 In the Clean implementation the new Gamma in the result of an inference is
-hidden in the Typing Monad. 
+carried through the Typing Monad. 
 
 Below we will show the inference rules for expressions and statements. In these
 lowercase Greek letters are always fresh type variables. 
 
+Section~\ref{sec:infRules} shows all typing inference rules. Below we will show
+a few to express the basics and show some interesting cases. 
+
 \paragraph{Op2 expressions}
 Equation~\ref{eq:inferOp2} shows the inference rule for op2 expressions. 
 \textit{op2type} is a function which takes an operator and returns the