+\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
\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
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
}
\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
&\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}
repositories / cc1516.git / commitdiff