diff --git a/tex/iris.sty b/tex/iris.sty index 7d29b29050623c3e325f364ef7df70af0d0fe17d..fc371567ba378b616c7fb4e6f82daf74846ffccf 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 256e13e20ecaece9321a43debf29bf7ed0c8f1b6..faa3727e31cb6d6c12cac9bf411b9cee07911dcd 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}