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{\Yard}{\textsc{Yard}}
 \newcommand{\AST}{\emph{AST}}
 \newcommand{\ADT}{\emph{ADT}}

+\newcommand{\Clean}{\emph{Clean}}

 
 \let\tt\texttt
 
 
 \let\tt\texttt
 


@@ -55,4 +56,8 @@
        firstline=6,
        lastline=42]{../../AST.dcl}
 
        firstline=6,
        lastline=42]{../../AST.dcl}
 

+\newpage
+\subsection{Inference rules} \label{sec:infRules}
+\input{infRules.tex}
+

 \end{document}
 \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 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 
        \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. 
 
 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
 
 \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
 \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.
 
 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},
 \begin{lstlisting}[
        label={lst:types},
        caption={SPLC types},

-       language=clean]
+       language=Clean]

 :: Type 
        = TupleType (Type, Type)        -- (t1, t2)
        | ListType type                         -- [t]
 :: 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)
        | CharType
     | VoidType
        | FuncType Type                         -- (-> t)

-    | (->>) infixl 7 Type Type         -- (t1 -> t2)
+    | (\->>) infixl 7 Type Type        -- (t1 -> t2)

 \end{lstlisting}
 
 \subsubsection{Environment}
 \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
 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. 
 
 
 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 
 \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