\SPLC{} is a program written in the purely functional lazy programming language
Clean\footnote{\url{http://clean.cs.ru.nl/Clean}}. \SPLC{} has a standardized
UNIX like command line interface and functions as a filter in a way that it
-processes standard input in standard output. Default command line argument such
+processes standard input to standard output. Default command line argument such
as \texttt{--version} and \texttt{--help} provide the expected output. To
illustrate all the command line interface options the output of \texttt{spl
--help} is given in Listing~\ref{lst:splchelp}.
--- /dev/null
+% 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
\usepackage{spl}
\usepackage{hyperref}
\usepackage[a4paper]{geometry}
+\usepackage{proof}
\title{Compiler Construction: SPL Compiler}
\author{Pim Jager\and Mart Lubbers}
}
\newcommand{\SPLC}{\texttt{SPLC}}
-\newcommand{\SPL}{\texttt{SPLC}}
-\newcommand{\SSM}{\texttt{SPLC}}
+\newcommand{\SPL}{\texttt{SPL}}
+\newcommand{\SSM}{\texttt{SSM}}
\newcommand{\Yard}{\textsc{Yard}}
+\def\AST/{\texttt{AST}}
+
+\let\tt\texttt
\begin{document}
\maketitle
%A concise but precise description of how the work was divided amongst the
%members of
%the team.
+
+The semantic analysis phase asses if a -grammatically correct- program is also
+semantically correct and decorates the program with extra information it
+finds during this checking. The input of the semantic analysis is an \AST/ of
+the
+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:
+\begin{enumerate}
+ \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 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
+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{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
--- /dev/null
+reverse (list) :: [Int] -> [Int] {
+ var accu = [];
+ while (! isEmpty (list)) {
+ accu = list . hd : accu;
+ list = list . tl;
+ }
+ return accu;
+}
+
+coPrimeWith (elem, list) :: Int -> [Int] -> Bool {
+ if (isEmpty(list)) {
+ return True;
+ } else {
+ if (elem % list.hd == 0) {
+ return False;
+ } else {
+ return coPrimeWith(elem, list.tl);
+ }
+ }
+}
+
+factorize (n) :: Int -> [Int] {
+ var primes = [];
+ var i = 2;
+ while (i < n) {
+ if (n % i == 0 && coPrimeWith(i, primes)) {
+ print("Found prime: ", i);
+ primes = i : primes;
+ }
+ i = i + 1;
+ }
+ return primes;q
+}
+
+print_list_inner (list) :: [Int] -> Void {
+ if (isEmpty(list)) {
+ return;
+ } else {
+ print(list.hd);
+ if (!isEmpty(list.tl)) {
+ print(',');
+ print(' ');
+ }
+ return print_list_inner(list.tl);
+ }
+}
+
+print_list (list) :: [Int] -> Void {
+ print('[');
+ print_list_inner(list);
+ print(']');
+ print('
+');
+ return;
+}
+
+main (){
+ //var number = 692963517;
+ var number = 12000;
+ var result = reverse(factorize(number));
+ print_list(result);
+ return;
+}
\ No newline at end of file
}
}
+giveF(){
+ return (\x->x+1);
+}
+
plus(x, y){
- return x + y;
+ return x + y;
}
main(){
var x = 5;
- var a = plus(3);
- print("3+5=", a(5));
+ var f = giveF();
+
+ var plus = \x y->x+y;
+
+ var g = map(plus, [1,2,3]);
+ var is = map(\f->f(1), g);
+
+ //print("is.hd", is.hd);
+
+ print("f(4) = ", f(4));
+
+ print("faculty of 5 is: ", foldr(\x y->x*y, 1, intList(5)));
+ print("sum of 1..5 is: ", foldr(\x y->x+y, 0, intList(5)));
+ print("sum of 0..12 but only the evens: ",
+ foldr(\x y->x+y, 0, filter(\x->x%2 == 0, intList(12))));
+
-// print("faculty of 5 is: ", foldr(\x y->x*y, 1, intList(5)));
-// print("sum of 1..5 is: ", foldr(\x y->x+y, 0, intList(5)));
-// print("sum of 0..12 but only the evens: ",
-// foldr(\x y->x+y, 0, filter(\x->x%2 == 0, intList(12))));
}
repositories / cc1516.git / commitdiff