From: pimjager Date: Mon, 13 Jun 2016 20:23:53 +0000 (+0200) Subject: Added inferenece formulas, need some explaination and formatting X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=939fd9d78dea9ca768753028ef3f5d0f8bba629b;p=cc1516.git Added inferenece formulas, need some explaination and formatting --- diff --git a/deliverables/report/sem.tex b/deliverables/report/sem.tex index 3687777..6b49e68 100644 --- a/deliverables/report/sem.tex +++ b/deliverables/report/sem.tex @@ -261,3 +261,106 @@ determined and are shown below. \infer[\emptyset] {\Gamma \vdash [] \Rightarrow (\Gamma, \star_0, \alpha, [])}{} \end{equation} + +\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 + } +\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{Assignment statement} +blabla unapfs, en extenden van Gamma +\begin{equation} + \infer[Ass] + {\Gamma \vdash \textit{id.fs}^* \underline{=} e \Rightarrow + (\Gamma^\star.k:\tau_r^\star, \star, \textrm{Void}, + \textit{id.fs}^* \underline{=} e') + } + {\Gamma(\textit{id}) = \lfloor \tau_e \rfloor + &\Gamma \vdash e \Rightarrow (\Gamma^{\star_1}, \star_1, \tau_g, e') + &\texttt{fold unapfs } \tau_g \textit{reverse fs} = \tau^r + &\tau_e \unif \tau_g = \star_2 + &\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} \ No newline at end of file