From: pimjager <pim@pimjager.nl>
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