Merge branch 'heaplang-form-cleanup' into 'master'

Clean up \valForm / \exprForm

See merge request iris/iris!853

tex/heaplang.sty

@@ -23,16 +23,11 @@
 \newcommand{\stateHeap}{\textproj{heap}}
 \newcommand{\stateProphs}{\textproj{prophs}}
 
-\newcommand\exprForm{{\langkw{e}}}
-\newcommand\valForm{{\langkw{v}}}
-
 \def\Let#1=#2in{\langkw{let} \spac #1 \mathrel{=} #2 \spac \langkw{in} \spac}
 \def\If#1then{\langkw{if} \spac #1 \spac \langkw{then} \spac}
 \def\Else{\spac\langkw{else} \spac}
 \def\Ref{\operatorname{\langkw{ref}}}
 \def\Rec#1#2={\langkw{rec}\spac\operatorname{#1}#2 \mathrel{=} }
-\def\RecE#1#2={\langkw{rec}_\exprForm\spac\operatorname{#1}#2 \mathrel{=} }
-\def\RecV#1#2={\langkw{rec}_\valForm\spac\operatorname{#1}#2 \mathrel{=} }
 \def\Skip{\langkw{skip}}
 \def\Assert{\operatorname{\langkw{assert}}}
 \def\Inl{\operatorname{\langkw{inl}}}
@@ -82,3 +77,16 @@
 \newcommand\valne{\ncong}
 \newcommand\litCompareSafe{\textlog{lit\_compare\_safe}}
 \newcommand\valCompareSafe{\textlog{val\_compare\_safe}}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% VALUE AND EXPRESSION DISAMBIGUATION
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\newcommand\valForm{{\langkw{v}}}
+\def\RecV#1#2={\langkw{rec}_\valForm\spac\operatorname{#1}#2 \mathrel{=} }
+\def\InlV{\Inl_\valForm}
+\def\InrV{\Inr_\valForm}
+\newcommand\exprForm{{\langkw{e}}}
+\def\RecE#1#2={\langkw{rec}_\exprForm\spac\operatorname{#1}#2 \mathrel{=} }
+\def\InlE{\Inl_\exprForm}
+\def\InrE{\Inr_\exprForm}

tex/heaplang.tex

@@ -19,8 +19,8 @@ The grammar of HeapLang, and in particular its set \Expr{} of \emph{expressions}
   \prophid \mid {}& (z \in \integer, \loc \in \Loc, \prophid \in \ProphId) \\&
   \RecV\lvarF(\lvar)= \expr \mid
   (\val,\valB)_\valForm \mid
-  \Inl(\val)_\valForm \mid
-  \Inr(\val)_\valForm  \\
+  \InlV(\val) \mid
+  \InrV(\val)  \\
 \expr \in \Expr \bnfdef{}&
   \val \mid
   \lvar \mid
@@ -35,8 +35,8 @@ The grammar of HeapLang, and in particular its set \Expr{} of \emph{expressions}
   \Fst(\expr) \mid
   \Snd(\expr) \mid
   {}\\ &
-  \Inl(\expr)_\exprForm \mid
-  \Inr(\expr)_\exprForm \mid
+  \InlE(\expr) \mid
+  \InrE(\expr) \mid
   \Match \expr with \Inl => \expr_1 | \Inr => \expr_2 end \mid
   {}\\ &
   \Alloc(\expr_1,\expr_2) \mid
@@ -154,10 +154,10 @@ The intention of this is to forbid directly comparing large values such as pairs
   (\RecV\lvarF(\lvar)= \expr, \state, \nil) \\
 ((\val_1, \val_2)_\exprForm, \state) \hstep[\nil]{}&
   ((\val_1, \val_2)_\valForm, \state, \nil) \\
-(\Inl(\val)_\exprForm, \state) \hstep[\nil]{}&
-  (\Inl(\val)_\valForm, \state, \nil) \\
-(\Inr(\val)_\exprForm, \state) \hstep[\nil]{}&
-  (\Inr(\val)_\valForm, \state, \nil) \\
+(\InlE(\val), \state) \hstep[\nil]{}&
+  (\InlV(\val), \state, \nil) \\
+(\InrE(\val), \state) \hstep[\nil]{}&
+  (\InrV(\val), \state, \nil) \\
 &\alignheader\textbf{Pure reductions} \\
 ((\RecV\lvarF(\lvar)= \expr)(\val), \state) \hstep[\nil]{}&
   (\subst {\subst \expr \lvarF {(\Rec\lvarF(\lvar)= \expr)}} \lvar \val, \state, \nil) \\
@@ -183,9 +183,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) \\
-(\Match \Inl(\val)_\valForm with \Inl => \expr_1 | \Inr => \expr_2 end, \state) \hstep[\nil]{}&
+(\Match \InlV(\val) with \Inl => \expr_1 | \Inr => \expr_2 end, \state) \hstep[\nil]{}&
   (\expr_1(\val), \state, \nil) \\
-(\Match \Inr(\val)_\valForm with \Inl => \expr_1 | \Inr => \expr_2 end, \state) \hstep[\nil]{}&
+(\Match \InrV(\val) 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