add logically atomic triples

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)}

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}