Sem fixed
authorpimjager <pim@pimjager.nl>
Tue, 14 Jun 2016 21:36:02 +0000 (23:36 +0200)
committerpimjager <pim@pimjager.nl>
Tue, 14 Jun 2016 21:36:02 +0000 (23:36 +0200)
deliverables/report/infRules.tex
deliverables/report/report.tex
deliverables/report/sem.tex
deliverables/report/todo.txt

index e69de29..a6594d9 100644 (file)
@@ -0,0 +1,125 @@
+\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 
+corresponding function type, i.e. $\textit{op2type}(\&\&) = Bool \rightarrow
+Bool \rightarrow Bool$. 
+
+\begin{equation} \label{eq:inferOp2}
+       \infer[Op2]
+               {\Gamma \vdash e_1 \oplus e_2 \Rightarrow 
+                       (\Gamma^{\star}, \star, \alpha^\star, (e_1' \oplus e_2')^\star)}
+               {\Gamma \vdash e_1 \Rightarrow (\Gamma^{\star_1},\star_1, \tau_1, e_1') 
+               &\Gamma^{\star_1} \vdash e_2 \Rightarrow (\Gamma^{\star_2},
+                       \star_2, \tau_2, e_2') 
+               &(\tau_1 \rightarrow \tau_2 \rightarrow \alpha) \unif
+                       \textit{op2type}(\oplus) = \star_3
+               &\star = \star_3 \cdot \star_2 \cdot \star_1
+               }
+\end{equation}
+
+\paragraph{Op1 expressions}
+\begin{equation} \label{eq:inferOp1}
+       \infer[Op1]
+               {\Gamma \vdash \ominus e \Rightarrow 
+                       (\Gamma^{\star}, \star, \alpha^\star, (\ominus e')^\star)}
+               {\Gamma \vdash e \Rightarrow (\star_1, \tau, e_1') 
+               &(\tau \rightarrow \alpha) \unif
+                       \textit{op1type}(\ominus) = \star_2
+               &\star = \star_2 \cdot \star_1
+               }
+\end{equation}
+
+\paragraph{Tuples}
+\begin{equation} \label{eq:tuples}
+       \infer[Tuple]
+               {\Gamma \vdash (e_1, e_2) \Rightarrow 
+                       (\Gamma^{\star}, \star, (\tau_1, \tau_2)^\star, 
+                               (e_1', e_2')^\star)}
+               {\Gamma \vdash e_1 \Rightarrow (\Gamma^{\star_1},\star_1, \tau_1, e_1') 
+               &\Gamma^{\star_1} \vdash e_2 \Rightarrow (\Gamma^{\star_2},
+                       \star_2, \tau_2, e_2') 
+               &\star = \star_3 \cdot \star_2 \cdot \star_1
+               }
+\end{equation}
+
+\paragraph{Literals}
+
+\begin{equation}
+       \infer[Int]{\Gamma \vdash n \Rightarrow (\Gamma, \star_0, Int, n)}{}
+\end{equation}
+
+\begin{equation}
+       \infer[Bool]{\Gamma \vdash b \Rightarrow (\Gamma, \star_0, Bool, b)}{}
+\end{equation}
+
+\begin{equation}
+       \infer[Char]{\Gamma \vdash c \Rightarrow (\Gamma, \star_0, Char, c)}{}
+\end{equation}
+
+\begin{equation}
+       \infer[\emptyset]
+               {\Gamma \vdash [] \Rightarrow (\Gamma, \star_0, \alpha, [])}{}
+\end{equation}
+
+\paragraph{If statements}
+\begin{equation}
+       \infer[If]
+               {\Gamma \vdash \underline{\textrm{if }} e 
+                       \underline{\textrm{ then }} s_1 
+                       \underline{\textrm{ else }} s_2
+                       \Rightarrow
+                       (\Gamma^\star, \star, \tau_e^\star, \underline{\textrm{if }} e' 
+                       \underline{\textrm{ then }} s_1' 
+                       \underline{\textrm{ else }} s_2')
+               }
+               {\Gamma \vdash e \Rightarrow (\Gamma^{\star_1}, \star_1, \tau_1, e')
+               &\tau_1 \unif \textrm{Bool} = \star_2
+               &\Gamma^{\star_2\cdot \star_1} \vdash s_1 \Rightarrow 
+                       (\Gamma^{\star_3}, \star_3, \tau_t, s_1')
+               &\Gamma^{\star_3} \vdash s_2 \Rightarrow 
+                       (\Gamma^{\star_4}, \star_4, \tau_e, s_2')
+               &\tau_t \unif \tau_e = \star_5
+               }
+\end{equation}
+
+\paragraph{While statements}
+\begin{equation}
+       \infer[While]
+               {\Gamma \vdash \underline{\textrm{while }} e \textrm{ } s 
+                       \Rightarrow
+                       (\Gamma^\star, \star, \tau_s^\star, 
+                               \underline{\textrm{while }} e' \textrm{ } s_1')
+               }
+               {\Gamma \vdash e \Rightarrow (\Gamma^{\star_1}, \star_1, \tau_1, e')
+               &\tau_1 \unif \textrm{Bool} = \star_2
+               &\Gamma^{\star_2\cdot \star_1} \vdash s \Rightarrow 
+                       (\Gamma^{\star_3}, \star_3, \tau_t, s')
+               &\star = \star_3 \cdot \star_2 \cdot \star_1
+               }
+\end{equation}
+
+\paragraph{Function Statements}
+\begin{equation} \label{eq:inferStmtApp0}
+       \infer[Stmt App 0]
+               {\Gamma \vdash \textit{id}().\textit{fs}^* \Rightarrow
+                       ((\Gamma^\star, \star, \textrm{Void}, 
+                               \textit{id}().\textit{fs}^*)}
+               {\Gamma(id) = \lfloor \tau^e \rfloor
+               &\texttt{fold apfs } \tau \textit{ fs}^* = \tau^r
+               }
+\end{equation}
+
+\begin{equation} \label{eq:inferAppN}
+       \infer[Stmt AppN]
+               {\Gamma \vdash \textit{id}(e^*).\textit{fs}^* \Rightarrow
+                       ((\Gamma^\star, \star, \textrm{Void}, 
+                               \textit{id}({e^*}').\textit{fs}^*)}
+               {\Gamma(id) = \lfloor \tau^e \rfloor
+               &\Gamma \vdash e^* \Rightarrow 
+                       (\Gamma^{\star_1}, \star_1, \tau^*, {e^*}')
+               &(\texttt{fold } (\rightarrow) \texttt{ } \alpha \texttt{ } \tau^*) 
+                       \unif \tau^e = \star_2
+               &\star = \star_2 \cdot \star_1
+               &\texttt{fold apfs } \tau \textit{ fs}^* = \tau^e
+               }
+\end{equation}
\ No newline at end of file
index 7a8d361..2b7b772 100644 (file)
@@ -6,6 +6,7 @@
 \usepackage{hyperref}
 \usepackage[a4paper]{geometry}
 \usepackage{proof}
+\usepackage{lscape}
 
 \title{Compiler Construction: SPL Compiler}
 \author{Pim Jager\and Mart Lubbers}
@@ -57,7 +58,9 @@
        lastline=42]{../../AST.dcl}
 
 \newpage
+\begin{landscape}
 \subsection{Inference rules} \label{sec:infRules}
 \input{infRules.tex}
+\end{landscape}
 
 \end{document}
index f63a32e..9fc3dee 100644 (file)
@@ -69,6 +69,36 @@ algorithm, which is a magnitude more complex. This last step also decorates the
 \AST{} with inferred type information. 
 
 \subsection{AST transformation for lambdas}
+Before checking the semantic correctness of the program one small \AST{} 
+transformations needs to be done. Currently this transformation is build into 
+the semantic analysis phase, however, it would be more in place as a separate 
+compiler phase, and if more transformations are needed in the future these will
+be placed in a separate phase.
+
+The implementation of lambdas in \SPLC{} is implemented through a clever trick.
+All \tt{LambdaExpressions} in the \AST{} are lifted to actual functions. This
+transformation is illustrated in Listing~\ref{lst:lambdaLift}. This 
+has the advantage that, with our support for higher order functions, lambda 
+functions do not require any special attention after this transformation. One 
+downside is that in the current implementation lambdas can not access variables
+in the scope in which they are declared. This could be solved by adding all 
+free variables in the lambda expression as parameters to the lifted function.
+
+\begin{lstlisting}[
+       label={lst:lambdaLift},
+       caption={SPLC types},
+       language=Clean]
+main() {
+       var x = \a b -> a + b;
+}
+--is transformed to:
+2lambda_12(a, b) {
+       return a + b;
+}
+main() {
+       var x = 2lambda_12;
+}
+\end{lstlisting}
 
 % \subsection{Sanity checks}
 % The sanity checks are defined as simple recursive functions over the function
@@ -179,50 +209,6 @@ 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 
-corresponding function type, i.e. $\textit{op2type}(\&\&) = Bool \rightarrow
-Bool \rightarrow Bool$. 
-
-\begin{equation} \label{eq:inferOp2}
-       \infer[Op2]
-               {\Gamma \vdash e_1 \oplus e_2 \Rightarrow 
-                       (\Gamma^{\star}, \star, \alpha^\star, (e_1' \oplus e_2')^\star)}
-               {\Gamma \vdash e_1 \Rightarrow (\Gamma^{\star_1},\star_1, \tau_1, e_1') 
-               &\Gamma^{\star_1} \vdash e_2 \Rightarrow (\Gamma^{\star_2},
-                       \star_2, \tau_2, e_2') 
-               &(\tau_1 \rightarrow \tau_2 \rightarrow \alpha) \unif
-                       \textit{op2type}(\oplus) = \star_3
-               &\star = \star_3 \cdot \star_2 \cdot \star_1
-               }
-\end{equation}
-
-\paragraph{Op1 expressions}
-\begin{equation} \label{eq:inferOp1}
-       \infer[Op1]
-               {\Gamma \vdash \ominus e \Rightarrow 
-                       (\Gamma^{\star}, \star, \alpha^\star, (\ominus e')^\star)}
-               {\Gamma \vdash e \Rightarrow (\star_1, \tau, e_1') 
-               &(\tau \rightarrow \alpha) \unif
-                       \textit{op1type}(\ominus) = \star_2
-               &\star = \star_2 \cdot \star_1
-               }
-\end{equation}
-
-\paragraph{Tuples}
-\begin{equation} \label{eq:tuples}
-       \infer[Tuple]
-               {\Gamma \vdash (e_1, e_2) \Rightarrow 
-                       (\Gamma^{\star}, \star, (\tau_1, \tau_2)^\star, 
-                               (e_1', e_2')^\star)}
-               {\Gamma \vdash e_1 \Rightarrow (\Gamma^{\star_1},\star_1, \tau_1, e_1') 
-               &\Gamma^{\star_1} \vdash e_2 \Rightarrow (\Gamma^{\star_2},
-                       \star_2, \tau_2, e_2') 
-               &\star = \star_3 \cdot \star_2 \cdot \star_1
-               }
-\end{equation}
-
 \paragraph{Variables}
 Inferring variable requires a bit of care. First of all the variable has to
 be present in $\Gamma$, secondly field selectors need to be respected. To apply
@@ -277,68 +263,39 @@ and accumulating the resulting types, substitutions, etc.
                }
 \end{equation}
 
-\paragraph{Literals}
-The types of literals -Ints, Bools, Chars and empty lists- are trivially 
-determined and are shown below. 
-
-\begin{equation}
-       \infer[Int]{\Gamma \vdash n \Rightarrow (\Gamma, \star_0, Int, n)}{}
-\end{equation}
-
-\begin{equation}
-       \infer[Bool]{\Gamma \vdash b \Rightarrow (\Gamma, \star_0, Bool, b)}{}
-\end{equation}
-
-\begin{equation}
-       \infer[Char]{\Gamma \vdash c \Rightarrow (\Gamma, \star_0, Char, c)}{}
-\end{equation}
+\paragraph{Return statements}
+Statements are typed with the type they return. The base case for this is 
+trivially a return statement. An empty return statement is of type \tt{Void} 
+and other return statements are typed with the type or their expression.
 
-\begin{equation}
-       \infer[\emptyset]
-               {\Gamma \vdash [] \Rightarrow (\Gamma, \star_0, \alpha, [])}{}
-\end{equation}
+When checking combinations of statements, e.g. if-then-else statements, it is
+checked that all branches return the same type, then the
+type of the combination is set to this type.
 
-\paragraph{If statements}
-balbal de if en else mzelfed type, jwz statements hebben he tupen wat ze
-returnen.
 \begin{equation}
-       \infer[If]
-               {\Gamma \vdash \underline{\textrm{if }} e 
-                       \underline{\textrm{ then }} s_1 
-                       \underline{\textrm{ else }} s_2
-                       \Rightarrow
-                       (\Gamma^\star, \star, \tau_e^\star, \underline{\textrm{if }} e' 
-                       \underline{\textrm{ then }} s_1' 
-                       \underline{\textrm{ else }} s_2')
-               }
-               {\Gamma \vdash e \Rightarrow (\Gamma^{\star_1}, \star_1, \tau_1, e')
-               &\tau_1 \unif \textrm{Bool} = \star_2
-               &\Gamma^{\star_2\cdot \star_1} \vdash s_1 \Rightarrow 
-                       (\Gamma^{\star_3}, \star_3, \tau_t, s_1')
-               &\Gamma^{\star_3} \vdash s_2 \Rightarrow 
-                       (\Gamma^{\star_4}, \star_4, \tau_e, s_2')
-               &\tau_t \unif \tau_e = \star_5
+       \infer[Return \emptyset]
+               {\Gamma \vdash \underline{\textrm{return}} \Rightarrow
+                       (\Gamma, \star_0, \textrm{Void}, \underline{\textrm{return}})
                }
+               {}
 \end{equation}
 
-\paragraph{While statements}
 \begin{equation}
-       \infer[While]
-               {\Gamma \vdash \underline{\textrm{while }} e \textrm{ } s 
-                       \Rightarrow
-                       (\Gamma^\star, \star, \tau_s^\star, 
-                               \underline{\textrm{while }} e' \textrm{ } s_1')
-               }
-               {\Gamma \vdash e \Rightarrow (\Gamma^{\star_1}, \star_1, \tau_1, e')
-               &\tau_1 \unif \textrm{Bool} = \star_2
-               &\Gamma^{\star_2\cdot \star_1} \vdash s \Rightarrow 
-                       (\Gamma^{\star_3}, \star_3, \tau_t, s')
-               &\star = \star_3 \cdot \star_2 \cdot \star_1
+       \infer[Return]
+               {\Gamma \vdash \underline{\textrm{return }} e \Rightarrow
+                       (\Gamma^\star, \star, \tau, \underline{\textrm{return }} e')
                }
+               {\Gamma \vdash e \Rightarrow (\Gamma^\star, \star, \tau, e')}
 \end{equation}
 
 \paragraph{Assignment statement}
-blabla unapfs, en extenden van Gamma
+When assigning a new value to a variable this variable needs to be present in
+Gamma and its type needs to unify with the type of the expression. 
+
+One thing that needs to be taken care of when assigning are the field selectors.
+\tt{unapfs} is a function which takes a type and a fieldselector and returns the
+type of the variable needed to assign to that fieldselector, i.e. \CI{unapfs 
+a FieldHd = ListType a}
 \begin{equation}
        \infer[Ass]
                {\Gamma \vdash \textit{id.fs}^* \underline{=} e \Rightarrow
@@ -352,51 +309,3 @@ blabla unapfs, en extenden van Gamma
                &\star = \star_2 \cdot \star_1
                }
 \end{equation}
-
-\paragraph{Function Statements}
-Blabl, praktisch gelijk aan function call, behalve dat ze altijd Void als
-type hebben.
-
-\begin{equation} \label{eq:inferStmtApp0}
-       \infer[Stmt App 0]
-               {\Gamma \vdash \textit{id}().\textit{fs}^* \Rightarrow
-                       ((\Gamma^\star, \star, \textrm{Void}, 
-                               \textit{id}().\textit{fs}^*)}
-               {\Gamma(id) = \lfloor \tau^e \rfloor
-               &\texttt{fold apfs } \tau \textit{ fs}^* = \tau^r
-               }
-\end{equation}
-
-\begin{equation} \label{eq:inferAppN}
-       \infer[Stmt AppN]
-               {\Gamma \vdash \textit{id}(e^*).\textit{fs}^* \Rightarrow
-                       ((\Gamma^\star, \star, \textrm{Void}, 
-                               \textit{id}({e^*}').\textit{fs}^*)}
-               {\Gamma(id) = \lfloor \tau^e \rfloor
-               &\Gamma \vdash e^* \Rightarrow 
-                       (\Gamma^{\star_1}, \star_1, \tau^*, {e^*}')
-               &(\texttt{fold } (\rightarrow) \texttt{ } \alpha \texttt{ } \tau^*) 
-                       \unif \tau^e = \star_2
-               &\star = \star_2 \cdot \star_1
-               &\texttt{fold apfs } \tau \textit{ fs}^* = \tau^e
-               }
-\end{equation}
-
-\paragraph{Return statements}
-blabla, verschil tussen wel en niet iets returnen
-
-\begin{equation}
-       \infer[Return \emptyset]
-               {\Gamma \vdash \underline{\textrm{return}} \Rightarrow
-                       (\Gamma, \star_0, \textrm{Void}, \underline{\textrm{return}})
-               }
-               {}
-\end{equation}
-
-\begin{equation}
-       \infer[Return]
-               {\Gamma \vdash \underline{\textrm{return }} e \Rightarrow
-                       (\Gamma^\star, \star, \tau, \underline{\textrm{return }} e')
-               }
-               {\Gamma \vdash e \Rightarrow (\Gamma^\star, \star, \tau, e')}
-\end{equation}
index c16bfe3..a0e5b5c 100644 (file)
@@ -1,5 +1,5 @@
 pim parse: Uitleggen over YARD
-pim sem: sem opschonen appendix, die pagina landscape(package: lscape, \begin{lscape})
+VINK pim sem: sem opschonen appendix, die pagina landscape(package: lscape, \begin{lscape})
 pim gen: abi en generation
 mart gen: higher order functions
 pim eval: doen