fix nog meer boxen en referenties

[cc1516.git] / deliverables / report / sem.tex

diff --git a/deliverables/report/sem.tex b/deliverables/report/sem.tex
index cfb7cfb..9aa5af9 100644 (file)
--- a/deliverables/report/sem.tex
+++ b/deliverables/report/sem.tex
@@ -36,10 +36,7 @@ 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=SPLCode]
+\begin{lstlisting}[label={lst:lambdaLift},caption={\SPLC{} types},language=SPLCode]
 main() {
        var x = \a b -> a + b;
 }
@@ -186,19 +183,21 @@ and accumulating the resulting types, substitutions, etc.
                }
 \end{equation}
 
-\begin{equation} \label{eq:inferAppN}
-       \infer[AppN]
-               {\Gamma \vdash \textit{id}(e^*).\textit{fs}^* \Rightarrow
-                       ((\Gamma^\star, \star, \tau^r,
-                               \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
+\begin{equation}\label{eq:inferAppN}
+       \resizebox{\linewidth}{!}{%
+               \infer[AppN]
+                       {\Gamma \vdash \textit{id}(e^*).\textit{fs}^* \Rightarrow
+                               ((\Gamma^\star, \star, \tau^r,
+                                       \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}
@@ -235,15 +234,17 @@ 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
-                       (\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
+       \resizebox{\linewidth}{!}{%
+               \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}