ctx application

xnning · Dec 11, 2017 · b3082c7 · b3082c7
1 parent 1667348
commit b3082c7
Show file tree

Hide file tree

Showing 3 changed files with 18 additions and 11 deletions.
diff --git a/doc/unify/main.tex b/doc/unify/main.tex
@@ -90,6 +90,7 @@
 \bibliographystyle{ACM-Reference-Format}
 \citestyle{acmauthoryear}
 
+\usepackage{multirow}
 
 \begin{document}
 

diff --git a/doc/unify/paper_utility.tex b/doc/unify/paper_utility.tex
@@ -187,7 +187,7 @@
 \newcommand{\byapp}{\vdash}
 \newcommand{\bywt}{\vDash}
 \newcommand{\toctx}{\dashv \ctxl}
-\newcommand{\toctxo}{\dashv \tctx}
+\newcommand{\toctxo}{\dashv \lctx}
 \newcommand{\toctxr}{\dashv \ctxr}
 \newcommand{\dpreinf}[1][]{\dctx {#1} \byinf}
 \newcommand{\dprechk}[1][]{\dctx {#1} \bychk}
@@ -236,7 +236,7 @@
 \newcommand{\erase}[1]{|{#1}|}
 \newcommand{\etaeq}{\rightsquigarrow_{\eta id}}
 
-\newcommand{\applye}[2]{[{#1}] #2}
+\newcommand{\applye}[2]{\llbracket{#1}\rrbracket #2}
 \newcommand{\glb}{\rightsquigarrow}
 
 

diff --git a/doc/unify/sections/rules.tex b/doc/unify/sections/rules.tex
@@ -42,15 +42,21 @@ \section{Algorithm}
 \end{mathpar}
 
 \begin{figure}[t]
-    \begin{tabular}{llp{3cm}lll}
-        $\applye \tctx x $ & = & $x$ \\
-        $\applye \tctx \star $ & = & $\star$ \\
-        $\applye \tctx {e_1 ~ e_2} $ & = & ${\applye \tctx {e_1}} ~ {\applye \tctx {e_2}}$ \\
-        $\applye \tctx {\erlam x e} $ & = & $\erlam x {\applye \tctx e}$ \\
-        $\applye \tctx {\blam x A e} $ & = & $\blam x {\applye \tctx A} {\applye \tctx e}$ \\
-        $\applye \tctx {\bpi x A B} $ & = & $\bpi x {\applye \tctx A} {\applye \tctx B}$ \\
-        $\applye {\tctx[\genA[\sctx_2]]} {(\genA[\sctx_1])} $ & = & $\genA[\sctx_1] $ \\
-        $\applye {\tctx[\genA[\sctx_2] = e]} {(\genA[\sctx_1])} $ & = & $\applye \tctx {(e \subst {\sctx_2} {\sctx_1})} $ \\
+    \begin{tabular}{lll}
+      \multicolumn{3}{l}{Meta Context Application on terms}\\
+        $\applye \lctx x $ & = & $x$ \\
+        $\applye \lctx \star $ & = & $\star$ \\
+        $\applye \lctx {e_1 ~ e_2} $ & = & ${\applye \lctx {e_1}} ~ {\applye \lctx {e_2}}$ \\
+        $\applye \lctx {\erlam x e} $ & = & $\erlam x {\applye \lctx e}$ \\
+        $\applye \lctx {\blam x A e} $ & = & $\blam x {\applye \lctx A} {\applye \lctx e}$ \\
+        $\applye \lctx {\bpi x A B} $ & = & $\bpi x {\applye \lctx A} {\applye \lctx B}$ \\
+        $\applye {\lctx[\genA[\sctx]]} {(\genA[\sigma])} $ & = & $\genA[\sigma'] $ \\
+           & & where $\sigma' = \applye {\lctx[\genA[\sctx]]} \sigma$\\
+        $\applye {\lctx[\genA[\sctx] = e]} {(\genA[\sigma])} $ & = & ${(e \subst {\sctx} {\sigma'})} $ \\
+           & & where $\sigma' = \applye {\lctx[\genA[\sctx] = e]} \sigma$\\
+      \multicolumn{3}{l}{Meta Context Application on suspended substitution}\\
+        $\applye \lctx {\cdot} $ & = & $\cdot$ \\
+        $\applye \lctx {(\sigma, e)} $ & = & $\applye \lctx \sigma, \applye \lctx e$ \\
     \end{tabular}
     \caption{Meta Context Application}
     \label{figure:erasure}