Merge branch 'ralf/triples' into 'master'

fix triple issues with revert, and add logatom triples

See merge request iris/iris!801

tex/iris.sty

@@ -332,24 +332,8 @@
 
 %% Hoare Triples
 
-\newcommand*{\hoaresizebox}[1]{%
-  \hbox{$\mathsurround=0pt{#1}\mathstrut$}}
-\newcommand*{\hoarescalebox}[2]{%
-  \hbox{\scalerel*[1ex]{#1}{#2}}}
-\newcommand{\triple}[5]{%
-  \setbox0=\hoaresizebox{{#3}{#5}}%
-  \setbox1=\hoarescalebox{#1}{\copy0}%
-  \setbox2=\hoarescalebox{#2}{\copy0}%
-  \copy1{#3}\copy2%
-  \; #4 \;%
-  \copy1{#5}\copy2}
-
-\newcommand{\irisbracketgen}[4][]{%
-  \setbox0=\hbox{$\mathsurround=0pt{#1}{#4}\mathstrut$}%
-  \scalerel*[1ex]{#2}{\copy0}%
-  {#4}%
-  \scalerel*[1ex]{#3}{\copy0}}
-\newcommand{\curlybracket}[2][]{\irisbracketgen[{#1}]\{\}{#2}}
+% needs extra {...} for some weird reason
+\newcommand{\curlybracket}[1]{{\left\{#1\right\}}}
 
 \NewDocumentCommand \hoare {m m m O{}}{
 	\curlybracket{#1}\spac #2 \spac \curlybracket{#3}_{#4}%
@@ -378,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

+\documentclass[10pt]{article}
+\usepackage{lmodern}
+\usepackage[T1]{fontenc}
+\usepackage[utf8]{inputenc}
+
+\input{setup}
+
+
+\title{The Iris TeX Test Document}
+\begin{document}
+\maketitle
+
+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}}}
+\newcommand{\mapstoLftd}{\mapsto_d^{\mathrm{lftd}}}
+
+\begin{align*}
+  \hoareV{ \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*}
+\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}