From 5fe60b5b3e57f0ef8ca2da5da5fd6c8c10eef9fe Mon Sep 17 00:00:00 2001
From: pimjager <pim@pimjager.nl>
Date: Thu, 9 Jun 2016 18:40:23 +0200
Subject: [PATCH] report type checking wip

---
 deliverables/report/proof.sty  | 259 +++++++++++++++++++++++++++++++++
 deliverables/report/report.tex |   1 +
 deliverables/report/sem.tex    |  74 +++++++++-
 3 files changed, 332 insertions(+), 2 deletions(-)
 create mode 100644 deliverables/report/proof.sty

diff --git a/deliverables/report/proof.sty b/deliverables/report/proof.sty
new file mode 100644
index 0000000..63403a7
--- /dev/null
+++ b/deliverables/report/proof.sty
@@ -0,0 +1,259 @@
+%   proof.sty   (Proof Figure Macros)
+%
+%   version 3.1 (for both LaTeX 2.09 and LaTeX 2e)
+%   Nov 24, 2005
+%   Copyright (C) 1990 -- 2005, Makoto Tatsuta (tatsuta@nii.ac.jp)
+% 
+% This program is free software; you can redistribute it or modify
+% it under the terms of the GNU General Public License as published by
+% the Free Software Foundation; either versions 1, or (at your option)
+% any later version.
+% 
+% This program is distributed in the hope that it will be useful
+% but WITHOUT ANY WARRANTY; without even the implied warranty of
+% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+% GNU General Public License for more details.
+%
+%   Usage:
+%       In \documentstyle, specify an optional style `proof', say,
+%           \documentstyle[proof]{article}.
+%
+%   The following macros are available:
+%
+%   In all the following macros, all the arguments such as
+%   <Lowers> and <Uppers> are processed in math mode.
+%
+%   \infer<Lower><Uppers>
+%       draws an inference.
+%
+%       Use & in <Uppers> to delimit upper formulae.
+%       <Uppers> consists more than 0 formulae.
+%
+%       \infer returns \hbox{ ... } or \vbox{ ... } and
+%       sets \@LeftOffset and \@RightOffset globally.
+%
+%   \infer[<Label>]<Lower><Uppers>
+%       draws an inference labeled with <Label>.
+%
+%   \infer*<Lower><Uppers>
+%       draws a many step deduction.
+%
+%   \infer*[<Label>]<Lower><Uppers>
+%       draws a many step deduction labeled with <Label>.
+%
+%   \infer=<Lower><Uppers>
+%       draws a double-ruled deduction.
+%
+%   \infer=[<Label>]<Lower><Uppers>
+%       draws a double-ruled deduction labeled with <Label>.
+%
+%   \deduce<Lower><Uppers>
+%       draws an inference without a rule.
+%
+%   \deduce[<Proof>]<Lower><Uppers>
+%       draws a many step deduction with a proof name.
+%
+%   Example:
+%       If you want to write
+%                       B C
+%              -----
+%              A     D
+%             ----------
+%             E
+%   use
+%       \infer{E}{
+%           A
+%           &
+%           \infer{D}{B & C}
+%       }
+%
+
+%   Style Parameters
+
+\newdimen\inferLineSkip     \inferLineSkip=2pt
+\newdimen\inferLabelSkip    \inferLabelSkip=5pt
+\def\inferTabSkip{\quad}
+
+%   Variables
+
+\newdimen\@LeftOffset   % global
+\newdimen\@RightOffset  % global
+\newdimen\@SavedLeftOffset  % safe from users
+
+\newdimen\UpperWidth
+\newdimen\LowerWidth
+\newdimen\LowerHeight
+\newdimen\UpperLeftOffset
+\newdimen\UpperRightOffset
+\newdimen\UpperCenter
+\newdimen\LowerCenter
+\newdimen\UpperAdjust
+\newdimen\RuleAdjust
+\newdimen\LowerAdjust
+\newdimen\RuleWidth
+\newdimen\HLabelAdjust
+\newdimen\VLabelAdjust
+\newdimen\WidthAdjust
+
+\newbox\@UpperPart
+\newbox\@LowerPart
+\newbox\@LabelPart
+\newbox\ResultBox
+
+%   Flags
+
+\newif\if@inferRule % whether \@infer draws a rule.
+\newif\if@DoubleRule    % whether \@infer draws doulbe rules.
+\newif\if@ReturnLeftOffset  % whether \@infer returns \@LeftOffset.
+
+%   Special Fonts
+
+\def\DeduceSym{\vtop{\baselineskip4\p@ \lineskiplimit\z@
+    \vbox{\hbox{.}\hbox{.}\hbox{.}}\hbox{.}}}
+
+%   Macros
+
+% Renaming @ifnextchar and @ifnch of LaTeX2e to @IFnextchar and @IFnch.
+
+\def\@IFnextchar#1#2#3{%
+  \let\reserved@e=#1\def\reserved@a{#2}\def\reserved@b{#3}\futurelet
+    \reserved@c\@IFnch}
+\def\@IFnch{\ifx \reserved@c \@sptoken \let\reserved@d\@xifnch
+      \else \ifx \reserved@c \reserved@e\let\reserved@d\reserved@a\else
+          \let\reserved@d\reserved@b\fi
+      \fi \reserved@d}
+
+\def\@ifEmpty#1#2#3{\def\@tempa{\@empty}\def\@tempb{#1}\relax
+    \ifx \@tempa \@tempb #2\else #3\fi }
+
+\def\infer{\@IFnextchar *{\@inferSteps}{\relax
+    \@IFnextchar ={\@inferDoubleRule}{\@inferOneStep}}}
+
+\def\@inferOneStep{\@inferRuletrue \@DoubleRulefalse
+    \@IFnextchar [{\@infer}{\@infer[\@empty]}}
+
+\def\@inferDoubleRule={\@inferRuletrue \@DoubleRuletrue
+    \@IFnextchar [{\@infer}{\@infer[\@empty]}}
+
+\def\@inferSteps*{\@IFnextchar [{\@@inferSteps}{\@@inferSteps[\@empty]}}
+
+\def\@@inferSteps[#1]{\@deduce{#1}[\DeduceSym]}
+
+\def\deduce{\@IFnextchar [{\@deduce{\@empty}}
+    {\@inferRulefalse \@infer[\@empty]}}
+
+%   \@deduce<Proof Label>[<Proof>]<Lower><Uppers>
+
+\def\@deduce#1[#2]#3#4{\@inferRulefalse
+    \@infer[\@empty]{#3}{\@infer[{#1}]{#2}{#4}}}
+
+%   \@infer[<Label>]<Lower><Uppers>
+%       If \@inferRuletrue, it draws a rule and <Label> is right to
+%       a rule. In this case, if \@DoubleRuletrue, it draws
+%       double rules.
+%
+%       Otherwise, draws no rule and <Label> is right to <Lower>.
+
+\def\@infer[#1]#2#3{\relax
+% Get parameters
+    \if@ReturnLeftOffset \else \@SavedLeftOffset=\@LeftOffset \fi
+    \setbox\@LabelPart=\hbox{$#1$}\relax
+    \setbox\@LowerPart=\hbox{$#2$}\relax
+%
+    \global\@LeftOffset=0pt
+    \setbox\@UpperPart=\vbox{\tabskip=0pt \halign{\relax
+        \global\@RightOffset=0pt \@ReturnLeftOffsettrue $##$&&
+        \inferTabSkip
+        \global\@RightOffset=0pt \@ReturnLeftOffsetfalse $##$\cr
+        #3\cr}}\relax
+    \UpperLeftOffset=\@LeftOffset
+    \UpperRightOffset=\@RightOffset
+% Calculate Adjustments
+    \LowerWidth=\wd\@LowerPart
+    \LowerHeight=\ht\@LowerPart
+    \LowerCenter=0.5\LowerWidth
+%
+    \UpperWidth=\wd\@UpperPart \advance\UpperWidth by -\UpperLeftOffset
+    \advance\UpperWidth by -\UpperRightOffset
+    \UpperCenter=\UpperLeftOffset
+    \advance\UpperCenter by 0.5\UpperWidth
+%
+    \ifdim \UpperWidth > \LowerWidth
+        % \UpperCenter > \LowerCenter
+    \UpperAdjust=0pt
+    \RuleAdjust=\UpperLeftOffset
+    \LowerAdjust=\UpperCenter \advance\LowerAdjust by -\LowerCenter
+    \RuleWidth=\UpperWidth
+    \global\@LeftOffset=\LowerAdjust
+%
+    \else   % \UpperWidth <= \LowerWidth
+    \ifdim \UpperCenter > \LowerCenter
+%
+    \UpperAdjust=0pt
+    \RuleAdjust=\UpperCenter \advance\RuleAdjust by -\LowerCenter
+    \LowerAdjust=\RuleAdjust
+    \RuleWidth=\LowerWidth
+    \global\@LeftOffset=\LowerAdjust
+%
+    \else   % \UpperWidth <= \LowerWidth
+        % \UpperCenter <= \LowerCenter
+%
+    \UpperAdjust=\LowerCenter \advance\UpperAdjust by -\UpperCenter
+    \RuleAdjust=0pt
+    \LowerAdjust=0pt
+    \RuleWidth=\LowerWidth
+    \global\@LeftOffset=0pt
+%
+    \fi\fi
+% Make a box
+    \if@inferRule
+%
+    \setbox\ResultBox=\vbox{
+        \moveright \UpperAdjust \box\@UpperPart
+        \nointerlineskip \kern\inferLineSkip
+        \if@DoubleRule
+        \moveright \RuleAdjust \vbox{\hrule width\RuleWidth
+            \kern 1pt\hrule width\RuleWidth}\relax
+        \else
+        \moveright \RuleAdjust \vbox{\hrule width\RuleWidth}\relax
+        \fi
+        \nointerlineskip \kern\inferLineSkip
+        \moveright \LowerAdjust \box\@LowerPart }\relax
+%
+    \@ifEmpty{#1}{}{\relax
+%
+    \HLabelAdjust=\wd\ResultBox \advance\HLabelAdjust by -\RuleAdjust
+    \advance\HLabelAdjust by -\RuleWidth
+    \WidthAdjust=\HLabelAdjust
+    \advance\WidthAdjust by -\inferLabelSkip
+    \advance\WidthAdjust by -\wd\@LabelPart
+    \ifdim \WidthAdjust < 0pt \WidthAdjust=0pt \fi
+%
+    \VLabelAdjust=\dp\@LabelPart
+    \advance\VLabelAdjust by -\ht\@LabelPart
+    \VLabelAdjust=0.5\VLabelAdjust  \advance\VLabelAdjust by \LowerHeight
+    \advance\VLabelAdjust by \inferLineSkip
+%
+    \setbox\ResultBox=\hbox{\box\ResultBox
+        \kern -\HLabelAdjust \kern\inferLabelSkip
+        \raise\VLabelAdjust \box\@LabelPart \kern\WidthAdjust}\relax
+%
+    }\relax % end @ifEmpty
+%
+    \else % \@inferRulefalse
+%
+    \setbox\ResultBox=\vbox{
+        \moveright \UpperAdjust \box\@UpperPart
+        \nointerlineskip \kern\inferLineSkip
+        \moveright \LowerAdjust \hbox{\unhbox\@LowerPart
+            \@ifEmpty{#1}{}{\relax
+            \kern\inferLabelSkip \unhbox\@LabelPart}}}\relax
+    \fi
+%
+    \global\@RightOffset=\wd\ResultBox
+    \global\advance\@RightOffset by -\@LeftOffset
+    \global\advance\@RightOffset by -\LowerWidth
+    \if@ReturnLeftOffset \else \global\@LeftOffset=\@SavedLeftOffset \fi
+%
+    \box\ResultBox
+}
\ No newline at end of file
diff --git a/deliverables/report/report.tex b/deliverables/report/report.tex
index ff25cb7..efd98e0 100644
--- a/deliverables/report/report.tex
+++ b/deliverables/report/report.tex
@@ -5,6 +5,7 @@
 \usepackage{spl}
 \usepackage{hyperref}
 \usepackage[a4paper]{geometry}
+\usepackage{proof}
 
 \title{Compiler Construction: SPL Compiler}
 \author{Pim Jager\and Mart Lubbers}
diff --git a/deliverables/report/sem.tex b/deliverables/report/sem.tex
index 66fda2c..20512cd 100644
--- a/deliverables/report/sem.tex
+++ b/deliverables/report/sem.tex
@@ -23,7 +23,7 @@ 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:
+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)}
@@ -52,4 +52,74 @@ declarations in the AST. We will very shortly describe them here.
 			\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
+\end{description}
+
+\subsection{Type inference}
+\SPLC{} features a Hindley-Milner type inference algorithm based on the
+algorithm presented in the slides. It 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. 
+
+\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
+in more detail in Section~\ref{sec:ext}. These require a change to the
+type system, which we will already describe here.
+
+Higher order functions require that the type system can distinguish if an 
+expression represents a type $a$ or a functions which takes no input and returns
+a value of type $a$ (we write: $\rightarrow a$). The latter is represented by 
+the \CI{FuncType}. 
+
+Another important difference with standard \SPL{} is that \SPLC{} supports 
+currying of functions, functions are not typed with a list of argument types
+and a return type, but with just a single argument and return type. This return
+type then in itself can be a function. 
+
+\begin{lstlisting}[
+	label={lst:types},
+	caption={SPLC types},
+	language=clean]
+:: Type 
+	= TupleType (Type, Type) 	-- (t1, t2)
+	| ListType type 			-- [t]
+	| IdType TVar  				-- polymorphic type
+	| IntType 
+	| BoolType
+	| CharType
+    | VoidType
+	| FuncType Type 			-- (-> t)
+    | (->>) infixl 7 Type Type 	-- (t1 -> t2)
+\end{lstlisting}
+
+\subsubsection{Environment}
+As all stages of \SPLC{}, the type inference is programmed in Clean. It takes an
+AST and produces either a fully typed AST, or an error if the provided AST 
+contains type errors. The Program is typed in an environment $\Gamma : id 
+\rightarrow \tau$ which maps identifiers of functions or variables to types. 
+
+In Clean the type inference functions run in the \tt{Typing} monad, which is
+defined as \CI{Typing a :== StateT (Gamma, [TVar]) (Either SemError) a}. The 
+carried list of \tt{TVar} is an 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
+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.
+
+Unification ($\cup$) takes two types and either provides a substitution which
+could
+unify them, or an error of the types are not unifiable. The interesting case
+of unification is when trying to unify an type variable with a more 
+specialised type. Equation~\ref{eq:unifyId} shows this. All other cases 
+are trivially promoting unification to the contained types, or checking directly
+if the types to be unified are equal.
+
+\begin{equation} \label{eq:unifyId}
+	\infer{tv \cup \tau \Rightarrow [tv \mapsto \tau]}
+			{tv \notin ftv(\tau)}
+\end{equation}
\ No newline at end of file
-- 
2.20.1