diff --git a/tex/iris.sty b/tex/iris.sty index 9dbdc4842415d52eac6fffad1ee03b63e6ffafad..fc371567ba378b616c7fb4e6f82daf74846ffccf 100644 --- a/tex/iris.sty +++ b/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)} diff --git a/tex/test.tex b/tex/test.tex new file mode 100644 index 0000000000000000000000000000000000000000..faa3727e31cb6d6c12cac9bf411b9cee07911dcd --- /dev/null +++ b/tex/test.tex @@ -0,0 +1,48 @@ +\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}