rules: Attempt at merge/accum parameterised transformationevm

1 files changed, 43 insertions, 23 deletions

diff --git a/rules/rules.tex b/rules/rules.tex
index 0aec7dc..dfdd366 100644
--- a/rules/rules.tex
+++ b/rules/rules.tex
@@ -64,16 +64,19 @@
 
 \begin{document}
 
-\begin{align*}
-  &\sigma, \tau \coloneqqq
-    \tUnit
-    \mid \sigma \times \tau
-    \mid \sigma \uplus \tau
-    \mid \R
-    \mid \Z
-    \textcolor{gray}{{} \mid \tArray\ \tau} \\
-  &C \coloneqqq \{ \overline{x = t} \} \\
-  &\begin{array}{@{}l@{\;}r@{\;}l@{}}
+\[ \begin{array}{@{}c@{\qquad}c@{}}
+  \begin{array}{@{}l@{}}
+    \sigma, \tau \coloneqqq
+      \tUnit
+      \mid \sigma \times \tau
+      \mid \sigma \uplus \tau
+      \mid \R
+      \mid \Z
+      \textcolor{gray}{{} \mid \tArray\ \tau} \\
+    C \coloneqqq \{ \overline{x = t} \}
+  \end{array}
+  &
+  \begin{array}{@{}l@{\;}r@{\;}l@{}}
     s,t &\coloneqqq& x \mid \tlet\ C\ \tin\ t \\
     &\mid& \tunit \\
     &\mid& \ttup{s, t} \mid \tfst\ t \mid \tsnd\ t \\
@@ -81,22 +84,24 @@
     &\mid& c \mid \op{t_1,\ldots,t_n} \\
     &\textcolor{gray}{\mid}& \textcolor{gray}{\textit{array stuff}} \\
   \end{array}
-\end{align*}
+\end{array} \]
+
 \begin{gather*}
-  \fbox{$D_1[\tau]$} \\
   D_1[\tUnit] = \tUnit \qquad
   D_1[\sigma \times \tau] = D_1[\sigma] \times D_1[\tau] \qquad
   D_1[\sigma \uplus \tau] = D_1[\sigma] \uplus D_1[\tau] \\
   D_1[\R] = \R \qquad
   D_1[\Z] = \Z \qquad
-  D_1[\tArray\ \tau] = \tArray\ D_1[\tau] \\[0.5em]
-  \fbox{$D_2[\tau]$} \\
+  D_1[\tArray\ \tau] = \tArray\ D_1[\tau]
+  \\[0.5em]
   D_2[\tUnit] = \tUnit \qquad
   D_2[\sigma \times \tau] = D_2[\sigma] \times D_2[\tau] \qquad
   D_2[\sigma \uplus \tau] = D_2[\sigma] \luplus D_2[\tau] \\
   D_2[\R] = \R \qquad
   D_2[\Z] = \tUnit \qquad
   D_2[\tArray\ \tau] = \tArray\ D_2[\tau]
+  \\[0.5em]
+  \TupBinds[\{x_1 = t_1, \ldots, x_n = t_n\}] = \ttup{x_1, \ttup{x_2, \ldots \ttup{x_{n-1}, x_n}\ldots}}
 \end{gather*}
 
 \begin{gather*}
@@ -123,7 +128,7 @@
     &= (\epsilon, \tunit, \evm{return}\ \tunit)
   \\
   \DD\Gamma[\ttup{s,t}]
-    &= (\Dc\Gamma[s] \app \Dc\Gamma[t], \ttup{\Dp\Gamma[s], \Dp\Gamma[t]}, \tdo\ \tlet\ \ttup{d_1,d_2} = d\ \tin\ \Dd\Gamma{d_1}[s]; \Dd\Gamma{d_2}[t])
+    &= (\Dc\Gamma[s] \app \Dc\Gamma[t], \ttup{\Dp\Gamma[s], \Dp\Gamma[t]}, \tlet\ \ttup{d_1,d_2} = d\ \tin\ \tdo\ \Dd\Gamma{d_1}[s]; \Dd\Gamma{d_2}[t])
   \\
   \DD\Gamma[\tfst\ t]
     &= (\Dc\Gamma[t], \tfst\ \Dp\Gamma[t], \Dd\Gamma{\ttup{d, \linzero}}[t])
@@ -131,19 +136,19 @@
   \DD\Gamma[\tinl\ t]
     &= (\Dc\Gamma[t], \tinl\ \Dp\Gamma[t], \Dd\Gamma{(\mathbf{lcastl}\ d)}[t])
   \\
-  \DD\Gamma[\multiline{\tcase{s : \sigma \uplus \tau}\ \{ \\ \quad\hphantom{\mid {}} \tinl\ x \to t_1 \\ \quad \mid \tinr\ y \to t_2 \}]}
+  \DD\Gamma[\multiline{\tcase{s : \sigma \uplus \tau} \\ \quad\mathrlap{\{}\hphantom{\mid {}} \tinl\ x \to t_1 \\ \quad \mid \tinr\ y \to t_2 \}]}
     &= (\multiline{
           \Dc\Gamma[s] \app \{z = \Dp\Gamma[s]\} \app {} \\
-          \ttup{v, \mathit{tape}} = \multiline{
-            \tcase z\ \{ \\
-            \quad \hphantom{\mid {}} \tinl\ x \to \tlet\ \Dc\Gamma[t_1]\ \tin\ \ttup{\Dp\Gamma[t_1], \tinl\ (\TupBinds[\Dc\Gamma[t_1]])} \\
-            \quad \mid \tinr\ y \to \tlet\ \Dc\Gamma[t_2]\ \tin\ \ttup{\Dp\Gamma[t_2], \tinr\ (\TupBinds[\Dc\Gamma[t_2]])} \}
+          \{\ttup{v, \mathit{tape}} = \multiline{
+            \tcase z \\
+            \quad \mathrlap{\{}\hphantom{\mid {}} \tinl\ x \to \tlet\ \Dc\Gamma[t_1]\ \tin\ \ttup{\Dp\Gamma[t_1], \tinl\ (\TupBinds[\Dc\Gamma[t_1]])} \\
+            \quad \mid \tinr\ y \to \tlet\ \Dc\Gamma[t_2]\ \tin\ \ttup{\Dp\Gamma[t_2], \tinr\ (\TupBinds[\Dc\Gamma[t_2]])} \}\}
           } \\
           \precomma v \\
           \precomma \tdo\ \multiline{
             \mathit{dz'} \leftarrow \multiline{
-              \tcase{\mathit{tape}}\ \{ \\
-              \quad \hphantom{\mid {}} \tinl\ (\TupBinds[\Dc\Gamma[t_1]]) \to \tdo\ \multiline{
+              \tcase{\mathit{tape}} \\
+              \quad \mathrlap{\{}\hphantom{\mid {}} \tinl\ (\TupBinds[\Dc\Gamma[t_1]]) \to \tdo\ \multiline{
                 \ttup{\tunit, \mathit{dz}} \leftarrow \evm{scope}_{D_2[\Gamma],D_2[\sigma]}\ (\Dd\Gamma d[t_1]) \\
                 \evm{return}\ (\mathbf{linl}\ \mathit{dz})
               } \\
@@ -152,7 +157,7 @@
                 \evm{return}\ (\mathbf{linr}\ \mathit{dz}) \}
               }
             } \\
-            \Dd\Gamma{dz'}[s]
+            \Dd\Gamma{dz'}[s])
           }
        }
   \\
@@ -167,4 +172,19 @@
        }
 \end{align*}
 
+\newpage
+
+\newcommand\Tup{\mathrm{Tup}}
+\[
+  \Tup[x_1 : \tau_1, \ldots, x_n : \tau_n] = \tau_1 \times (\tau_2 \times \cdots (\tau_{n-1} \times \tau_n)\cdots)
+\]
+%
+\begin{gather*}
+  \Gamma \vdash t : \tau
+    \;\;\leadsto\;\; 
+    D_1[\Gamma] \vdash \tlet\ \Dc\Gamma[t]\ \tin\ \ttup{\Dp\Gamma[t], \lambda d.\ \Dd{\Gamma_M,\Gamma_A} d[t]} : D_1[\tau] \times (D_2[\tau] \lto \tEVM\ D_2[\Gamma_A]\ (\Tup[D_2[D^M_{\Gamma_M}[t]]])) \\
+  \DD\Gamma[t] \coloneqq (\Dc\Gamma[t], \Dp\Gamma[t], D^M_{\Gamma_M}[t], \Dd\Gamma d[t])
+\end{gather*}
+
+
 \end{document}