Fix the rewriting rules to work with tuples

assets/packages.tex

@@ -43,7 +43,7 @@ BoldItalicFont=*-BoldItalic,
 \usepackage{amsmath}
 \usepackage{amssymb}
 \usepackage{unicode-math}
-\setmathfont{GFSNeohellenicMath.otf}
+% \setmathfont{GFSNeohellenicMath.otf}
 
 % References
 \usepackage[

chapters/4_rewriting.tex

@@ -153,7 +153,7 @@ and where expressions have \mzninline{par} type.
       \alt "(" <exp> ["," <exp>]* ")"
 
     <item> ::= <param> [ "=" <exp> ]";"
-      \alt "(" <param> ["," <param>]* ")" "=" <exp> ";"
+      \alt "(" <param> ["," <param>]* ")" "=" <exp>";"
       \alt "constraint" <exp>";"
 
     <param> ::= <type-inst>":" <ident>
@@ -381,13 +381,13 @@ suitable alpha renaming.
 \begin{prooftree}
   \AxiomC{\(\ptinline{F(\(p_1, \ldots, p_k\)) = E;} \in \Prog\) where the \(p_i\)
     are fresh}
-  \noLine\
+  \noLine{}
   \UnaryInfC{\Sem{\(a_i\)}{\Prog, \Env_{i-1}} \(\Rightarrow~ \tuple{v_i,
       \Env_i'}, \ \Env_0=\Env, \Env_i=\Env_i'\cup\{p_i\mapsto v_i\sep[]\}
     \quad \forall
     1 \leq
     i \leq k\)}
-   \noLine\
+   \noLine{}
    \UnaryInfC{\Sem{E}{\Prog, \Env_k}
        \(\Rightarrow ~ \tuple{v, \Env'}\)}
   \RightLabel{(Call)}
@@ -471,12 +471,20 @@ simply the function applied to the evaluated parameters.
     (\Ctx, \Env')\)}
 \end{prooftree}
 \begin{prooftree}
- \AxiomC{\Sem{\(E\)}{\Prog, \Env} \(\Rightarrow \tuple{v, \Env'}\)}
+  \AxiomC{\Sem{\(E\)}{\Prog, \Env} \(\Rightarrow \tuple{v, \Env'}\)}
   \AxiomC{\Sem{\(\mathbf{I}\)}{\Prog, \Env' \cup\ \{x \mapsto\ v \sep\ [] \}} \(\Rightarrow (\Ctx, \Env'')\)}
   \RightLabel{(ItemTE)}
   \BinaryInfC{\Sem{\(t:x = E, \mathbf{I}\)}{\Prog, \Env} \(\Rightarrow
     (\Ctx, \Env'')\)}
 \end{prooftree}
+\begin{prooftree}
+  \AxiomC{\Sem{\(E\)}{\Prog, \Env} \(\Rightarrow \tuple{\left(v_{1}, \ldots, v_{n}\right), \Env'}\)}
+  \noLine{}
+  \UnaryInfC{\Sem{\(\mathbf{I}\)}{\Prog, \Env' \cup\ \{x_{1} \mapsto\ v_{1} \sep\ [] \} \cup\ \ldots\ \cup\ \{x_{n} \mapsto\ v_{n} \sep\ [] \}} \(\Rightarrow (\Ctx, \Env'')\)}
+  \RightLabel{(ItemTD)}
+  \UnaryInfC{\Sem{\(\left(t_{1}: x_{1}, \ldots, t_{n}: x_{n}\right) = E, \mathbf{I}\)}{\Prog, \Env} \(\Rightarrow
+    (\Ctx, \Env'')\)}
+\end{prooftree}
 \begin{prooftree}
   \AxiomC{\Sem{\(C\)}{\Prog, \Env} \(\Rightarrow \tuple{v, \Env'}\)}
   \AxiomC{\Sem{\(\mathbf{I}\)}{\Prog, \Env'} \(\Rightarrow (\Ctx, \Env'')\)}
@@ -519,6 +527,13 @@ is the base case for a list of let items.
   \AxiomC{\(c\) constant}
   \UnaryInfC{\Sem{c}{\Prog, \Env} \(\Rightarrow \tuple{c, \Env}\)}
 \end{prooftree}
+\begin{prooftree}
+  \RightLabel{(Tuple)}
+  \AxiomC{\Sem{\(E_{1}\)}{\Prog,\Env} \(\Rightarrow \tuple{v_{1}, \Env^{1}}\)}
+  \AxiomC{\ldots}
+  \AxiomC{\Sem{\(E_{n}\)}{\Prog,\Env^{n-1}} \(\Rightarrow \tuple{v_{n}, \Env^{n}}\)}
+  \TrinaryInfC{\Sem{\(\left(E_{1}, \ldots, E_{n}\right)\)}{\Prog, \Env} \(\Rightarrow \tuple{x, \{x \mapsto \left(v_{1}, \ldots, v_{n}\right) \sep [] \} \cup \Env^{n})}\)}
+\end{prooftree}
 \begin{prooftree}
   \RightLabel{(If\(_T\))}
   \AxiomC{\Sem{\(C\)}{\Prog, \Env} \(\Rightarrow\) \(\tuple{\ptinline{true}, \_}\)}

dekker_thesis.tex

@@ -1,4 +1,3 @@
-\nonstopmode{}
 \documentclass[
 paper=9in:6in,
 DIV=calc,