From 8dc969d054bd3d70ef869fbd2262e75235af9172 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 21 May 2022 11:45:43 +0200
Subject: [PATCH] remove MatchCore macro, and add sugar for match with binders
---
tex/heaplang.sty | 1 -
tex/heaplang.tex | 14 ++++++++++----
2 files changed, 10 insertions(+), 5 deletions(-)
diff --git a/tex/heaplang.sty b/tex/heaplang.sty
index 4cf01cd5a..df6afc2ea 100644
--- a/tex/heaplang.sty
+++ b/tex/heaplang.sty
@@ -44,7 +44,6 @@
\def\NewProph{\langkw{newproph}}
\def\ResolveWith#1at#2to#3{\langkw{resolve}\spac\langkw{with}\spac#1\spac\langkw{at}\spac#2\spac\langkw{to}\spac#3}
\def\Resolve#1to#2{\langkw{resolve}\spac#1\spac\langkw{to}\spac#2}
-\def\MatchCore#1with#2|#3end{\langkw{match}\spac#1\spac\langkw{with}\spac#2\mid#3\spac\langkw{end}}
\def\Match#1with#2=>#3|#4=>#5end{\langkw{match}\spac#1\spac\langkw{with}\spac#2\Ra#3\mid#4\Ra#5\spac\langkw{end}}
\def\MatchML#1with#2=>#3|#4=>#5end#6{{\arraycolsep=1.4pt\begin{array}[t]{rll}%
\multicolumn{3}{l}{\langkw{match}\spac#1\spac\langkw{with}}\\%
diff --git a/tex/heaplang.tex b/tex/heaplang.tex
index 95b1961b5..0498d8222 100644
--- a/tex/heaplang.tex
+++ b/tex/heaplang.tex
@@ -37,7 +37,7 @@ The grammar of HeapLang, and in particular its set \Expr{} of \emph{expressions}
{}\\ &
\Inl(\expr)_\exprForm \mid
\Inr(\expr)_\exprForm \mid
- \MatchCore \expr with \expr_1 | \expr_2 end \mid
+ \Match \expr with \Inl => \expr_1 | \Inr => \expr_2 end \mid
{}\\ &
\Alloc(\expr_1,\expr_2) \mid
\Free(\expr) \mid
@@ -55,6 +55,10 @@ The grammar of HeapLang, and in particular its set \Expr{} of \emph{expressions}
\end{align*}
(Note that \langkw{match} contains a literal $|$ that is not part of the BNF but part of HeapLang syntax.)
+To simplify the formalization, the only binders occur in \langkw{rec}.
+\langkw{match} has a closure in each arm which will be applied to the value of the left/right variant, respectively.
+(See the syntactic sugar defined later.)
+
Recursive abstractions, pairs, and the injections exist both as a value form and an expression form.
The expression forms will reduce to the value form once all their arguments are values.
Conceptually, one can think of that as corresponding to ``boxing'' that most functional language implementations do.
@@ -93,7 +97,7 @@ The HeapLang operational semantics is defined via the use of \emph{evaluation co
{}\\ &
\Inl(\lctx) \mid
\Inr(\lctx) \mid
- \MatchCore \lctx with \expr_1 | \expr_2 end \mid
+ \Match \lctx with \Inl => \expr_1 | \Inr => \expr_2 end \mid
{}\\ &
\Alloc(\expr, \lctx) \mid
\Alloc(\lctx, \val) \mid
@@ -175,9 +179,9 @@ The intention of this is to forbid directly comparing large values such as pairs
(\val_1, \state, \nil) \\
(\Snd((\val_1, \val_2)_\valForm), \state) \hstep[\nil]{}&
(\val_2, \state, \nil) \\
-(\MatchCore \Inl(\val)_\valForm with \expr_1 | \expr_2 end, \state) \hstep[\nil]{}&
+(\Match \Inl(\val)_\valForm with \Inl => \expr_1 | \Inr => \expr_2 end, \state) \hstep[\nil]{}&
(\expr_1(\val), \state, \nil) \\
-(\MatchCore \Inr(\val)_\valForm with \expr_1 | \expr_2 end, \state) \hstep[\nil]{}&
+(\Match \Inr(\val)_\valForm with \Inl => \expr_1 | \Inr => \expr_2 end, \state) \hstep[\nil]{}&
(\expr_2(\val), \state, \nil)
\end{align*}
\caption{HeapLang pure and boxed reduction rules. \\ \small
@@ -272,6 +276,8 @@ We recover many of the common language operations as syntactic sugar.
\Skip \eqdef{}& \TT; \TT \\
\expr_1 \mathop{\&\&} \expr_2 \eqdef{}& \If \expr_1 then \expr_2 \Else \False \\
\expr_1 \mathop{||} \expr_2 \eqdef{}& \If \expr_1 then \True \Else \expr_2 \\
+ \Match \expr with \Inl(\lvar) => \expr_1 | \Inr(\lvarB) => \expr_2 end \eqdef {}&
+ \Match \expr with \Inl => \Lam\lvar. \expr_1 | \Inr => \Lam\lvarB. \expr_2 end \\
\Ref(\expr) \eqdef{}& \Alloc(1,\expr) \\
\CAS(\expr_1, \expr_2, \expr_3) \eqdef{}& \Snd(\CmpXchg(\expr_1, \expr_2, \expr_3)) \\
\Resolve \expr_1 to \expr_2 \eqdef{}& \ResolveWith \Skip at \expr_1 to \expr_2
--
GitLab