From f8710e19b6d4a357cd87b884721e749643ce56e9 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 23 May 2022 13:08:34 +0200
Subject: [PATCH] add logically atomic triples
---
tex/iris.sty | 24 ++++++++++++++++++++++++
tex/test.tex | 16 ++++++++++++++++
2 files changed, 40 insertions(+)
diff --git a/tex/iris.sty b/tex/iris.sty
index 7d29b2905..fc371567b 100644
--- a/tex/iris.sty
+++ b/tex/iris.sty
@@ -362,6 +362,30 @@
\end{aligned}}%
}
+%% Logical atomicity
+%Limit bracket width to 2ex
+\newcommand{\anglebracket}[1]{{\scaleleftright[2ex]{\langle}{#1}{\rangle}}}
+
+\NewDocumentCommand \ahoare {m m m O{}}{
+ \anglebracket{#1}\spac #2 \spac \anglebracket{#3}_{#4}%
+}
+
+\NewDocumentCommand \ahoareV {O{c} m m m O{}}{
+ {\begin{aligned}[#1]
+ &\anglebracket{#2} \\
+ &\quad{#3} \\
+ &{\anglebracket{#4}}_{#5}
+ \end{aligned}}%
+}
+
+\NewDocumentCommand \ahoareHV {O{c} m m m O{}}{
+ {\begin{aligned}[#1]
+ &\anglebracket{#2}\; {#3} \\
+ &{\anglebracket{#4}}_{#5}
+ \end{aligned}}%
+}
+
+
%% Some commonly used identifiers
\newcommand{\inhabited}[1]{\textlog{inhabited}(#1)}
diff --git a/tex/test.tex b/tex/test.tex
index 256e13e20..faa3727e3 100644
--- a/tex/test.tex
+++ b/tex/test.tex
@@ -12,6 +12,12 @@
Here we put a bunch of uses of the macros in \texttt{iris.sty} that we can visually test to ensure they still work when those macros are changed.
+\begin{mathpar}
+{ \hoare{P}{\expr}{Q} }
+
+{ \ahoare{P}{\expr}{Q} }
+\end{mathpar}
+
{
\newcommand{\mapstoDisk}{\mapsto_d}
\newcommand{\mapstoOp}{\mapsto_{\mathit{op}}}
@@ -27,6 +33,16 @@ Here we put a bunch of uses of the macros in \texttt{iris.sty} that we can visua
{\left( \Sep_{(a,o) \in m} a \mapstoDisk o \right) \lor
\left( \Sep_{(a,o') \in m'} a \mapstoDisk o' \right) }
\end{align*}
+\begin{align*}
+ \ahoareV{ \begin{aligned}
+ &\dom(m) = \dom(m') * {} \\
+ &\left( \Sep_{(a,o) \in m} a \mapstoLftd o \right) * %
+ \left( \Sep_{(a,o') \in m'} a \mapstoOp o' \right)
+ \end{aligned}} %
+ {\mathit{op}.\texttt{Commit}()}%
+ {\left( \Sep_{(a,o) \in m} a \mapstoDisk o \right) \lor
+ \left( \Sep_{(a,o') \in m'} a \mapstoDisk o' \right) }
+\end{align*}
}
\end{document}
--
GitLab