From: pimjager Date: Tue, 14 Jun 2016 21:36:02 +0000 (+0200) Subject: Sem fixed X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=e002c0637c6ba05183b19a9c4175d3f18ab7490d;p=cc1516.git Sem fixed --- diff --git a/deliverables/report/infRules.tex b/deliverables/report/infRules.tex index e69de29..a6594d9 100644 --- a/deliverables/report/infRules.tex +++ b/deliverables/report/infRules.tex @@ -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 diff --git a/deliverables/report/report.tex b/deliverables/report/report.tex index 7a8d361..2b7b772 100644 --- a/deliverables/report/report.tex +++ b/deliverables/report/report.tex @@ -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} diff --git a/deliverables/report/sem.tex b/deliverables/report/sem.tex index f63a32e..9fc3dee 100644 --- a/deliverables/report/sem.tex +++ b/deliverables/report/sem.tex @@ -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} diff --git a/deliverables/report/todo.txt b/deliverables/report/todo.txt index c16bfe3..a0e5b5c 100644 --- a/deliverables/report/todo.txt +++ b/deliverables/report/todo.txt @@ -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