From f4b94d7cc2cb05611b462ba278e4f12f7a7a5e5e Mon Sep 17 00:00:00 2001
From: Tom Smeding <t.j.smeding@uu.nl>
Date: Thu, 29 Aug 2024 17:46:15 +0200
Subject: rules: Attempt at merge/accum parameterised transformation
---
rules/rules.tex | 66 +++++++++++++++++++++++++++++++++++++--------------------
1 file changed, 43 insertions(+), 23 deletions(-)
(limited to 'rules/rules.tex')
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}
--
cgit v1.2.3-70-g09d2