From: pimjager Date: Tue, 14 Jun 2016 07:47:21 +0000 (+0200) Subject: sdfsdf X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=05f56c65ccbd8b1f402461e0505e9dadaffbb786;p=cc1516.git sdfsdf --- diff --git a/deliverables/report/infRules.tex b/deliverables/report/infRules.tex new file mode 100644 index 0000000..e69de29 diff --git a/deliverables/report/report.tex b/deliverables/report/report.tex index e8deb22..36446e8 100644 --- 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 --- 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