Type up some of the rules in LaTeX

2 files changed, 174 insertions, 0 deletions

diff --git a/rules/.gitignore b/rules/.gitignore
new file mode 100644
index 0000000..ef5f7e5
--- /dev/null
+++ b/rules/.gitignore
@@ -0,0 +1,4 @@
+*.aux
+*.log
+*.out
+*.pdf
diff --git a/rules/rules.tex b/rules/rules.tex
new file mode 100644
index 0000000..0aec7dc
--- /dev/null
+++ b/rules/rules.tex
@@ -0,0 +1,170 @@
+\documentclass[11pt,a4paper]{article}
+\usepackage[margin=2.5cm]{geometry}
+\usepackage[utf8]{inputenc}
+\usepackage[T1]{fontenc}
+\usepackage[british]{babel}
+\usepackage{microtype}
+\usepackage{amsmath}
+\usepackage{amsfonts}
+\usepackage{amssymb}
+\usepackage{mathtools}
+\usepackage{hyperref}
+% \usepackage{parskip}
+% \usepackage{graphicx}
+% \usepackage{xifthen}
+% \usepackage{wasysym}
+% \usepackage{verbatim}
+% \usepackage{changepage}
+\usepackage{xcolor}
+
+% fonts
+\usepackage{libertine}
+\usepackage[varqu]{zi4}
+\usepackage[libertine]{newtxmath}
+
+\let\oldepsilon\epsilon \let\epsilon\varepsilon \let\varepsilon\oldepsilon
+\let\oldphi\phi \let\phi\varphi \let\varphi\oldphi
+\let\oldemptyset\emptyset \let\emptyset\varnothing \let\varnothing\oldemptyset
+
+\newcommand\coloneqqq{\mathbin{\raisebox{0.04em}{::}\hspace{-0.25em}=}}
+
+\newcommand\multiline[1]{\begin{array}[t]{@{}l@{}} #1 \end{array}}
+\newcommand\precomma{\mathllap{,\mkern1mu}}
+
+\newcommand\R{\mathbb R}
+\newcommand\Z{\mathbb Z}
+\newcommand\tArray{\mathrm{Array}}
+\newcommand\tEVM{\mathrm{EVM}}
+\newcommand\tUnit{\mathbf{1}}
+\newcommand\ttup[1]{\langle #1 \rangle}
+\newcommand\tunit{\ttup{}}
+\newcommand\tfst{\mathrm{fst}}
+\newcommand\tsnd{\mathrm{snd}}
+\newcommand\op[1]{\mathit{op}(#1)}
+\newcommand\tlet{\mathbf{let}}
+\newcommand\tin{\mathbf{in}}
+\newcommand\tinl{\mathrm{inl}}
+\newcommand\tinr{\mathrm{inr}}
+\newcommand\tcase[1]{\mathbf{case}\ #1\ \mathbf{of}}
+\newcommand\tdo{\mathbf{do}}
+\newcommand\lto{\multimap}
+\newcommand\app{\mathbin{{+}\mkern-4mu{+}}}
+\newcommand\evm[1]{\underline{\vphantom{\mathbf{b}}\smash{\mathbf{#1}}}}
+
+\newcommand\luplus{\mathbin{\underline{\uplus}}}
+\newcommand\linzero{\underline{\mathbf0}}
+
+\newcommand\Dc[1]{D^0_{#1}}
+\newcommand\Dp[1]{D^1_{#1}}
+\newcommand\Dd[2]{D^2_{#1,#2}}
+\newcommand\DD[1]{\bar D_{#1}}
+
+\newcommand\TupBinds{\mathrm{TupBinds}}
+
+
+\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@{}}
+    s,t &\coloneqqq& x \mid \tlet\ C\ \tin\ t \\
+    &\mid& \tunit \\
+    &\mid& \ttup{s, t} \mid \tfst\ t \mid \tsnd\ t \\
+    &\mid& \tinl\ t \mid \tinr\ t \mid \tcase{s}\ \{ \ldots \} \\
+    &\mid& c \mid \op{t_1,\ldots,t_n} \\
+    &\textcolor{gray}{\mid}& \textcolor{gray}{\textit{array stuff}} \\
+  \end{array}
+\end{align*}
+\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_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]
+\end{gather*}
+
+\begin{gather*}
+  \Gamma \vdash t : \tau
+    \;\;\leadsto\;\; 
+    D_1[\Gamma] \vdash \tlet\ \Dc\Gamma[t]\ \tin\ \ttup{\Dp\Gamma[t], \lambda d.\ \Dd\Gamma d[t]} : D_1[\tau] \times (D_2[\tau] \lto \tEVM\ D_2[\Gamma]\ \tUnit) \\
+  \DD\Gamma[t] \coloneqq (\Dc\Gamma[t], \Dp\Gamma[t], \Dd\Gamma d[t])
+\end{gather*}
+%
+\begin{align*}
+  \DD\Gamma[x : \tau]
+    &= (\epsilon, x : D_2[\tau], \evm{one}_{x : D_2[\tau] \in D_2[\Gamma]}\ d)
+  \\
+  \DD\Gamma[\tlet\ x : \tau = s\ \tin\ t]
+    &= (\multiline{
+          \Dc\Gamma[s] \app \{x = \Dp\Gamma[t]\} \app \Dc\Gamma[t] \\
+          \precomma \Dp\Gamma[t] \\
+          \precomma \tdo\ \multiline{
+            \ttup{\tunit, \mathit{dx}} \leftarrow \evm{scope}_{D_2[\Gamma],D_2[\tau]}\ (\Dd\Gamma d[t]) \\
+            \Dd\Gamma{\mathit{dx}}[s])
+       }}
+  \\
+  \DD\Gamma[\tunit]
+    &= (\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])
+  \\
+  \DD\Gamma[\tfst\ t]
+    &= (\Dc\Gamma[t], \tfst\ \Dp\Gamma[t], \Dd\Gamma{\ttup{d, \linzero}}[t])
+  \\
+  \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 \}]}
+    &= (\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]])} \}
+          } \\
+          \precomma v \\
+          \precomma \tdo\ \multiline{
+            \mathit{dz'} \leftarrow \multiline{
+              \tcase{\mathit{tape}}\ \{ \\
+              \quad \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})
+              } \\
+              \quad \mid \tinr\ (\TupBinds[\Dc\Gamma[t_2]]) \to \tdo\ \multiline{
+                \ttup{\tunit, \mathit{dz}} \leftarrow \evm{scope}_{D_2[\Gamma],D_2[\tau]}\ (\Dd\Gamma d[t_2]) \\
+                \evm{return}\ (\mathbf{linr}\ \mathit{dz}) \}
+              }
+            } \\
+            \Dd\Gamma{dz'}[s]
+          }
+       }
+  \\
+  \DD\Gamma[c]
+    &= (\epsilon, c, \evm{return}\ \tunit)
+  \\
+  \DD\Gamma[\op{t_1,\ldots,t_n}]
+    &= (\multiline{
+          \Dc\Gamma[t_1] \app \cdots \app \Dc\Gamma[t_n] \app \{x_1 = \Dp\Gamma[t_1], \ldots, x_n = \Dp\Gamma[t_n]\} \\
+          \precomma \op{x_1, \ldots, x_n} \\
+          \precomma \tlet\ \ttup{d_1, \ldots, d_n} = D\mathit{op}^\top(x_1,\ldots,x_n; d)\ \tin\ \tdo\ \Dd\Gamma{d_1}[t_1]; \ldots; \Dd\Gamma{d_n}[t_n])
+       }
+\end{align*}
+
+\end{document}