typing: put typing rules in figures

typing/lambdaCalculus.tex

@@ -0,0 +1,56 @@
+\begin{mathpar}
+  \inferrule{ }{\Gamma; x:\tau \vdash x:\tau}(Var)
+
+  \and
+  \inferrule{ }{\Gamma \vdash c:\mathcal{B}(c)}(Const)
+
+  \and
+  \inferrule{%
+    \Gamma \vdash e_1 : \tau_1 \\ \Gamma \vdash e_2 : \tau_2 \\
+    \tau_1 \subtype \zero \rightarrow \one \\
+    \tau_2 \subtype \dom(\tau_1)
+  }{%
+    \Gamma \vdash e_1 e_2 : \tau_1 \tau_2
+  }
+  (App)
+
+  \and
+  \inferrule{%
+    \forall i \in \discrete{1}{n}, \\
+      \Gamma; \ofTypeP{p}{\sigma_i} \vdash e: \tau_i \\
+  }{%
+    \lambda \left(p:{\bigvee\limits_{i=1}^n\σ}\right).e :
+      \bigwedge\limits_{i=1}^n \left(\σ \rightarrow \τ\right)
+  }
+  (Abs)
+
+  \and
+  \inferrule{%
+    \Gamma \vdash e : \tau \\
+      \Γ; x : \τ \wedge t \vdash e_1 : \sigma_1 \\
+      \Γ; x : \τ \wedge \lnot t \vdash e_2 : \sigma_2
+  }{%
+    \Gamma \vdash ((x := e \in t) ? e_1 : e_2) : \sigma_1 \vee \sigma_2
+  }
+  (Tcase)
+
+  \and
+  \inferrule{%
+    \forall i \in \discrete{1}{n}, \Γ \vdash e_i : \τ_i \\
+      \Γ; x_1 : \τ_1; \ldots; x_n : \τ_n \vdash e : \τ
+  }{%
+    \Gamma \vdash \text{let } x_1 = e_1; \ldots{}; x_n = e_n
+      \text{ in } e : \τ
+  }
+  (Let)
+
+  \and
+  \inferrule{%
+    \forall i \in \discrete{0}{n},
+      \Γ; x_1 : \τ_1; \ldots; x_n : \τ_n \vdash e_i : \τ_i
+  }{%
+    \Gamma \vdash \text{let rec } x_1 : \τ_1 = e_1; \ldots{}; x_n : \τ_n = e_n
+      \text{ in } e_0 : \τ_0
+  }
+  (LetRec)
+\end{mathpar}

typing/recordTypingRules.tex

@@ -1,51 +1,53 @@
-\inferrule{%
-  \Γ \vdash e' : \τ \\
+\begin{mathpar}
+  \inferrule{%
+    \Γ \vdash e' : \τ \\
   \Γ \vdash e : \bigvee\limits_{i=1}^n s_i
-}{%
-  \Γ \vdash \left\{ e = e'; \right\} :
+  }{%
+    \Γ \vdash \left\{ e = e'; \right\} :
   \bigvee\limits_{i=1}^n \left\{ s_i: \τ \right\}
-}
-\irlabel{RFinite}
-\and
-\inferrule{%
-  \Γ \vdash e' : \τ \\
+  }
+  \irlabel{RFinite}
+  \and
+  \inferrule{%
+    \Γ \vdash e' : \τ \\
   \Γ \vdash e : \σ \\
   \σ \subtype \ty{string}
-}{%
-  \Γ \vdash \left\{ e = e'; \right\} :
+  }{%
+    \Γ \vdash \left\{ e = e'; \right\} :
   \left\{ \_: \τ \vee \undef \right\}
-}
-\irlabel{RInfinite}
-\and
-\inferrule{%
-  \Γ \vdash e_1 : \tau \\ \Γ \vdash e_2 : \σ \\
+  }
+  \irlabel{RInfinite}
+  \and
+  \inferrule{%
+    \Γ \vdash e_1 : \tau \\ \Γ \vdash e_2 : \σ \\
   \tau \subtype \onerec{} \\
   \sigma \subtype \onerec{} \\
   \dom_\undef(\tau) \wedge \dom_\undef(\sigma) = \varnothing
-}{%
-  \Γ \vdash e_1 \orthplus e_2 : \tau \orthplus \sigma
-}
-\irlabel{ROrthMerge}
-\and
-\inferrule{%
-  \Γ \vdash e_1 : \tau \\ \Γ \vdash e_2 : \σ \\
+  }{%
+    \Γ \vdash e_1 \orthplus e_2 : \tau \orthplus \sigma
+  }
+  \irlabel{ROrthMerge}
+  \and
+  \inferrule{%
+    \Γ \vdash e_1 : \tau \\ \Γ \vdash e_2 : \σ \\
   \tau \subtype \onerec{} \\
   \sigma \subtype \onerec{}
-}{%
-  \Γ \vdash e_1 + e_2 : \tau + \sigma
-}
-\irlabel{RMerge}
-\and
-\inferrule{%
-  \Γ \vdash e_1 : \τ \\ \Γ \vdash e_2 : \bigvee\limits_{i=1}^n s_i
-}{%
-  \Γ \vdash e_1 . e_2 : \left( \bigvee\limits_{i=1}^n \τ(s_i) \right) \backslash \undef
-}
-\irlabel{RAccessFinite}
-\and
-\inferrule{%
-  \Γ \vdash e_1 : \τ \\ \Γ \vdash e_2 : \σ \\ \σ \subtype \ty{string}
-}{%
-  \Γ \vdash e_1 . e_2 : \left( \deff(\τ) \vee \bigvee\limits_{s \in \dom(\τ)} \τ(s) \right) \backslash \undef
-}
-\irlabel{RAccessInfinite}
+  }{%
+    \Γ \vdash e_1 + e_2 : \tau + \sigma
+  }
+  \irlabel{RMerge}
+  \and
+  \inferrule{%
+    \Γ \vdash e_1 : \τ \\ \Γ \vdash e_2 : \bigvee\limits_{i=1}^n s_i
+  }{%
+    \Γ \vdash e_1 . e_2 : \left( \bigvee\limits_{i=1}^n \τ(s_i) \right) \backslash \undef
+  }
+  \irlabel{RAccessFinite}
+  \and
+  \inferrule{%
+    \Γ \vdash e_1 : \τ \\ \Γ \vdash e_2 : \σ \\ \σ \subtype \ty{string}
+  }{%
+    \Γ \vdash e_1 . e_2 : \left( \deff(\τ) \vee \bigvee\limits_{s \in \dom(\τ)} \τ(s) \right) \backslash \undef
+  }
+  \irlabel{RAccessInfinite}
+\end{mathpar}

typing/type-system.tex

@@ -1,64 +1,15 @@
-\subsection{$\lambda\&$-calculus}
-\begin{mathpar}
-  \inferrule{ }{\Gamma; x:\tau \vdash x:\tau}(Var)
+The typing rules are given by the figures~\pref{typing::lambda-calculus},~\pref{typing::records} and~\pref{typing::operators}.
 
-  \and
-  \inferrule{ }{\Gamma \vdash c:\mathcal{B}(c)}(Const)
+\begin{figure}
+  \input{typing/lambdaCalculus}
+  \caption{Typing rules for the $\λ\&-calculus$\label{typing::lambda-calculus}}
+\end{figure}
+\begin{figure}
+    \input{typing/recordTypingRules}
+  \caption{Typing rules for records\label{typing::records}}
+\end{figure}
 
-  \and
-  \inferrule{%
-    \Gamma \vdash e_1 : \tau_1 \\ \Gamma \vdash e_2 : \tau_2 \\
-    \tau_1 \subtype \zero \rightarrow \one \\
-    \tau_2 \subtype \dom(\tau_1)
-  }{%
-    \Gamma \vdash e_1 e_2 : \tau_1 \tau_2
-  }
-  (App)
-
-  \and
-  \inferrule{%
-    \forall i \in \discrete{1}{n}, \\
-      \Gamma; \ofTypeP{p}{\sigma_i} \vdash e: \tau_i \\
-  }{%
-    \lambda \left(p:{\bigvee\limits_{i=1}^n\σ}\right).e :
-      \bigwedge\limits_{i=1}^n \left(\σ \rightarrow \τ\right)
-  }
-  (Abs)
-
-  \and
-  \inferrule{%
-    \Gamma \vdash e : \tau \\
-      \Γ; x : \τ \wedge t \vdash e_1 : \sigma_1 \\
-      \Γ; x : \τ \wedge \lnot t \vdash e_2 : \sigma_2
-  }{%
-    \Gamma \vdash ((x := e \in t) ? e_1 : e_2) : \sigma_1 \vee \sigma_2
-  }
-  (Tcase)
-
-  \and
-  \inferrule{%
-    \forall i \in \discrete{1}{n}, \Γ \vdash e_i : \τ_i \\
-      \Γ; x_1 : \τ_1; \ldots; x_n : \τ_n \vdash e : \τ
-  }{%
-    \Gamma \vdash \text{let } x_1 = e_1; \ldots{}; x_n = e_n
-    \text{ in } e : \τ
-  }
-  (Let)
-
-  \and
-  \inferrule{%
-    \forall i \in \discrete{0}{n},
-      \Γ; x_1 : \τ_1; \ldots; x_n : \τ_n \vdash e_i : \τ_i
-  }{%
-    \Gamma \vdash \text{let rec } x_1 : \τ_1 = e_1; \ldots{}; x_n : \τ_n = e_n
-    \text{ in } e_0 : \τ_0
-  }
-  (LetRec)
-\end{mathpar}
-\subsection{Records}
-\begin{mathpar}
-   \input{typing/recordTypingRules}
-\end{mathpar}
-
-\subsection{Other builtin operators}
-\todo{add rules for operators}
+\begin{figure}
+  \todo{add rules for operators}
+  \caption{Typing rules for builtins operators\label{typing::operators}}
+\end{figure}