From 4a4db77f1638290b8e39dd0f7e4c4f96249db4af Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 23 Nov 2022 13:39:43 +0100
Subject: [PATCH] heaplang.sty: avoid clash with hyperref
---
CHANGELOG.md | 16 ++++++++++++++++
tex/heaplang.sty | 5 +++--
tex/heaplang.tex | 14 +++++++-------
tex/test.tex | 2 +-
4 files changed, 27 insertions(+), 10 deletions(-)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 6dd343903..59c0c0e57 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -16,6 +16,22 @@ lemma.
intuitionistic. This means that tactics such as `iDestruct ... as "->"` will
not dispose of hypotheses to perform the rewrite.
+**LaTeX changes:**
+
+- Rename `\Alloc` to `\AllocN` and `\Ref` to `\Alloc` for better consistency
+ with the Coq names and to avoid clash with hyperref package.
+
+The following sed script helps adjust LaTeX documents to these changes:
+Note that the script is not idempotent, do not run it twice.
+```
+sed -i -E -f- *.tex <<EOF
+# Alloc & Ref
+s/\\Alloc\b/\\AllocN/g
+s/\\Ref\b/\\Alloc/g
+EOF
+```
+
+
## Iris 4.0.0 (2022-08-18)
The highlight of Iris 4.0 is the *later credits* mechanism, which provides a new
diff --git a/tex/heaplang.sty b/tex/heaplang.sty
index 388781886..a51959a9a 100644
--- a/tex/heaplang.sty
+++ b/tex/heaplang.sty
@@ -26,7 +26,6 @@
\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\Skip{\langkw{skip}}
\def\Assert{\operatorname{\langkw{assert}}}
@@ -53,12 +52,14 @@
\def\MatchS#1with#2=>#3end{
\langkw{match}\spac#1\spac\langkw{with}\spac#2\Ra#3\spac\langkw{end}}
-\newcommand\Alloc{\operatorname{\langkw{Alloc}}}
+\newcommand\AllocN{\operatorname{\langkw{AllocN}}}
+\newcommand\Alloc{\operatorname{\langkw{ref}}} % syntax rendering consistent with Coq
\newcommand\Free{\operatorname{\langkw{Free}}}
\newcommand\CAS{\operatorname{\langkw{CAS}}}
\newcommand\CmpXchg{\operatorname{\langkw{CmpXchg}}}
\newcommand\Xchg{\operatorname{\langkw{Xchg}}}
\newcommand\FAA{\operatorname{\langkw{FAA}}}
+
\newcommand\deref{\mathop{!}}
\let\gets\leftarrow
diff --git a/tex/heaplang.tex b/tex/heaplang.tex
index 32645b866..61e5ffcc6 100644
--- a/tex/heaplang.tex
+++ b/tex/heaplang.tex
@@ -39,7 +39,7 @@ The grammar of HeapLang, and in particular its set \Expr{} of \emph{expressions}
\InrE(\expr) \mid
\Match \expr with \Inl => \expr_1 | \Inr => \expr_2 end \mid
{}\\ &
- \Alloc(\expr_1,\expr_2) \mid
+ \AllocN(\expr_1,\expr_2) \mid
\Free(\expr) \mid
\deref \expr \mid
\expr_1 \gets \expr_2 \mid
@@ -66,7 +66,7 @@ We will leave away the disambiguating subscript when it is clear from the contex
All of this lets us define $\ofval$ as simply applying the value injection (the very first syntactic form of $\Expr$), which makes a lot of things in Coq much simpler.
$\toval$ is defined recursively in the obvious way.
-\langkw{Alloc} takes as first argument the number of heap cells to allocate (must be strictly positive), and as second argument the default value to use for these heap cells.
+\langkw{AllocN} takes as first argument the number of heap cells to allocate (must be strictly positive), and as second argument the default value to use for these heap cells.
This lets one allocate arrays.
$\Ptradd$ implements pointer arithmetic (the left operand must be a pointer, the right operand an integer), which is used to access array elements.
@@ -103,8 +103,8 @@ The HeapLang operational semantics is defined via the use of \emph{evaluation co
\Inr(\lctx) \mid
\Match \lctx with \Inl => \expr_1 | \Inr => \expr_2 end \mid
{}\\ &
- \Alloc(\expr, \lctx) \mid
- \Alloc(\lctx, \val) \mid
+ \AllocN(\expr, \lctx) \mid
+ \AllocN(\lctx, \val) \mid
\Free(\lctx) \mid
\deref \lctx \mid
\expr \gets \lctx \mid
@@ -198,7 +198,7 @@ The $\HLOp$ subscript indicates that this is the HeapLang operator, not the math
\newcommand\alignheader{\kern-30ex}
\begin{align*}
&\alignheader\textbf{Heap reductions} \\
-(\Alloc(z, \val), \state) \hstep[\nil]{}&
+(\AllocN(z, \val), \state) \hstep[\nil]{}&
(\loc, \mapinsert {[\loc,\loc+z)} \val {\state:\stateHeap}, \nil)
&&\text{if $z>0$ and \(\All i<z. \state.\stateHeap(\loc+i) = \bot\)} \\
(\Free(\loc), \state) \hstep[\nil]{}&
@@ -231,7 +231,7 @@ The $\HLOp$ subscript indicates that this is the HeapLang operator, not the math
\end{mathpar}
\caption{HeapLang impure reduction rules. \\ \small
Here, $\state:\stateHeap$ denotes $\sigma$ with the $\stateHeap$ field updated as indicated.
-$[\loc,\loc+z)$ in the $\Alloc$ rule indicates that we update all locations in this (left-closed, right-open) interval.}
+$[\loc,\loc+z)$ in the $\AllocN$ rule indicates that we update all locations in this (left-closed, right-open) interval.}
\label{fig:heaplang-reduction-impure}
\end{figure}
@@ -282,7 +282,7 @@ We recover many of the common language operations as syntactic sugar.
\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) \\
+ \Alloc(\expr) \eqdef{}& \AllocN(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
\end{align*}
diff --git a/tex/test.tex b/tex/test.tex
index e5fb6fce5..cdcbf73fa 100644
--- a/tex/test.tex
+++ b/tex/test.tex
@@ -58,7 +58,7 @@ Here we put a bunch of uses of the macros in \texttt{iris.sty} that we can visua
\newcommand\OScheck{\textlang{check}}
\begin{proofoutline*}
- \CODE{\Let \lvar = \Ref(\Inl(0)) in } \\
+ \CODE{\Let \lvar = \Alloc(\Inl(0)) in } \\
\RES{\lvar \mapsto \Inl(0) * \ownGhost\gname{\ospending(1)}}[\top] \quad\COMMENT{(\textsc{hoare-alloc}, \textsc{ghost-alloc})} \\
\RES{\lvar \mapsto \Inl(0) * \ownGhost\gname{\ospending(1/2)} * \ownGhost\gname{\ospending(1/2)}}[\top] \quad\COMMENT{(\textsc{ghost-op})} \\
\RES{\knowInv\namesp{I} * \ownGhost\gname{\ospending(1/2)}}[\top] \quad\COMMENT{(\textsc{inv-alloc1})} \\
--
GitLab