Update rules.tex

1 files changed, 34 insertions, 2 deletions

diff --git a/rules/rules.tex b/rules/rules.tex
index dfdd366..ee1d54b 100644
--- a/rules/rules.tex
+++ b/rules/rules.tex
@@ -64,6 +64,8 @@
 
 \begin{document}
 
+\section*{Original triple CHAD}
+
 \[ \begin{array}{@{}c@{\qquad}c@{}}
   \begin{array}{@{}l@{}}
     \sigma, \tau \coloneqqq
@@ -174,16 +176,46 @@
 
 \newpage
 
+\section*{With accumulators and selective merge envs}
+
 \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)
 \]
 %
+\renewcommand\DD[2]{\bar D_{#1,#2}}%
+\newcommand\Dzero[1]{D^0_{#1}}%
+\newcommand\Dsave[1]{D^{0\mathrm{S}}_{#1}}%
+\renewcommand\Dp[1]{D^1_{#1}}%
+\newcommand\Dmerge[1]{D^M_{#1}}%
+\renewcommand\Dd[3]{D^2_{#1,#2,#3}}%
+\newcommand\Dac{D_{2\mathrm{Ac}}}%
 \begin{gather*}
+  \DD{\Gamma_M}{\Gamma_A}\,t = (\Dzero\Gamma\,t, \Dsave\Gamma\,t, \Dp\Gamma\,t, \Dmerge{\Gamma_M}\,t, \Dd{\Gamma_M}{\Gamma_A}{d}\,t) \qquad(\Gamma \coloneqq \Gamma_M \cup \Gamma_A) \\
+  \Dac[x_1 : \tau_1, \ldots, x_n : \tau_n] \coloneqq x_1 : \mathrm{Accum}\ \tau_1, \ldots, x_n : \mathrm{Accum}\ \tau_n \\
   \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])
+    \left\{ \begin{array}{ll}
+      \Dzero\Gamma\,t & \text{list of bindings in $D_1\,\Gamma$} \\
+      \Dsave\Gamma\,t & \text{subset of $\Dzero\Gamma\,t$ (``save list'')} \\
+      \Dp\Gamma\,t & D_1\,\Gamma, \Dzero\Gamma\,t \vdash \Dp\Gamma\,t : D_1\,\tau \\
+      \Dmerge{\Gamma_M}\,t & \text{subset of $\Gamma_M$} \\
+      \Dd{\Gamma_M}{\Gamma_A}{d}\,t & \Dac\,\Gamma_A, \Dsave\Gamma\,t, d : D_2\,\tau \vdash \Dd{\Gamma_M}{\Gamma_A}{d} : \Tup[D_2[\Dmerge{\Gamma_M}\,t]]
+        \qquad\text{(accumulation effect)}
+    \end{array} \right. \\
+  \text{Top-level: } D_1\,\Gamma, \Dac\,{\Gamma_A} \vdash \mathbf{let}\ \Dzero\Gamma\,t\ \mathbf{in}\ \ttup{\Dp\Gamma\,t, \lambda d.\ \Dd{\Gamma_M}{\Gamma_A}{d}\,t} : D_1\,\tau \times (D_2\,\tau \lto \Tup[D_2\,\Gamma_M])
+\end{gather*}
+Accumulation effect:
+\begin{gather*}
+  \frac{\Gamma \vdash t_1 : D_2\,\tau
+        \quad \Gamma, \mathrm{Accum}\ \tau \vdash t_2 : \alpha}
+       {\Gamma \vdash \underline{\mathrm{with}}\ t_1\ t_2 : \alpha \times D_2\,\tau}
+  \qquad
+  \frac{\tau_1 \overset{p}{\rightsquigarrow} \tau_2, \tau_{\mathrm{idx}}
+        \quad \Gamma \vdash t_1 : \tau_{\mathrm{idx}}
+        \quad \Gamma \vdash t_2 : D_2\,\tau_2
+        \quad \Gamma \vdash t_2 : \mathrm{Accum}\ \tau_1}
+       {\Gamma \vdash \underline{\mathrm{accum}}_p\ t_1\ t_2\ t_3 : \tUnit}
 \end{gather*}