Commit a8af5d9d authored by Robbert Krebbers's avatar Robbert Krebbers

Merge iris.sty with Iris 3.0 paper.

parent d2858676
Pipeline #2828 passed with stage
in 9 minutes and 23 seconds
...@@ -28,6 +28,8 @@ ...@@ -28,6 +28,8 @@
%% MATH SYMBOLS & NOTATION & IDENTIFIERS %% MATH SYMBOLS & NOTATION & IDENTIFIERS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\nat}{\mathbb{N}}
\DeclareMathOperator*{\Sep}{\scalerel*{\ast}{\sum}} \DeclareMathOperator*{\Sep}{\scalerel*{\ast}{\sum}}
\newcommand*{\disj}[1][]{\mathrel{\#_{#1}}} \newcommand*{\disj}[1][]{\mathrel{\#_{#1}}}
\newcommand\pord{\sqsubseteq} \newcommand\pord{\sqsubseteq}
...@@ -35,7 +37,7 @@ ...@@ -35,7 +37,7 @@
\newcommand{\upclose}{\mathord{\uparrow}} \newcommand{\upclose}{\mathord{\uparrow}}
\newcommand{\ALT}{\ |\ } \newcommand{\ALT}{\ |\ }
\newcommand{\spac}{\:} % a space \newcommand{\spac}{\,} % a space
\def\All #1.{\forall #1.\spac}% \def\All #1.{\forall #1.\spac}%
\def\Exists #1.{\exists #1.\spac}% \def\Exists #1.{\exists #1.\spac}%
...@@ -80,6 +82,12 @@ ...@@ -80,6 +82,12 @@
\newcommand{\Func}{F} % functor \newcommand{\Func}{F} % functor
\newcommand{\subst}[3]{{#1}[{#3} / {#2}]}
\newcommand{\mapinsert}[3]{#3[#1:=#2]}
\newcommand{\nil}{\epsilon}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% MODEL-SPECIFIC SYMBOLS & NOTATION & IDENTIFIERS %% MODEL-SPECIFIC SYMBOLS & NOTATION & IDENTIFIERS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
...@@ -122,6 +130,10 @@ ...@@ -122,6 +130,10 @@
\newcommand{\iPreProp}{\textdom{iPreProp}} \newcommand{\iPreProp}{\textdom{iPreProp}}
\newcommand{\Wld}{\textdom{Wld}} \newcommand{\Wld}{\textdom{Wld}}
\newcommand{\Res}{\textdom{Res}} \newcommand{\Res}{\textdom{Res}}
\newcommand{\State}{\textdom{State}}
\newcommand{\Val}{\textdom{Val}}
\newcommand{\Loc}{\textdom{Loc}}
\newcommand{\Expr}{\textdom{Expr}}
\newcommand{\cofe}{T} \newcommand{\cofe}{T}
\newcommand{\cofeB}{U} \newcommand{\cofeB}{U}
...@@ -169,6 +181,7 @@ ...@@ -169,6 +181,7 @@
\newcommand{\sigax}{A} \newcommand{\sigax}{A}
\newcommand{\type}{\tau} \newcommand{\type}{\tau}
\newcommand{\typeB}{\sigma}
\newcommand{\var}{x} \newcommand{\var}{x}
\newcommand{\varB}{y} \newcommand{\varB}{y}
...@@ -184,9 +197,13 @@ ...@@ -184,9 +197,13 @@
\newcommand{\propB}{Q} \newcommand{\propB}{Q}
\newcommand{\propC}{R} \newcommand{\propC}{R}
\newcommand{\pred}{\varphi} % pure propositions
\newcommand{\predB}{\psi} \newcommand{\pprop}{\phi}
\newcommand{\predC}{\zeta} \newcommand{\ppropB}{\psi}
\newcommand{\pred}{\varPhi}
\newcommand{\predB}{\Psi}
\newcommand{\predC}{\Zeta}
\newcommand{\gname}{\gamma} \newcommand{\gname}{\gamma}
\newcommand{\iname}{\iota} \newcommand{\iname}{\iota}
...@@ -202,18 +219,19 @@ ...@@ -202,18 +219,19 @@
\newcommand{\proves}{\vdash} \newcommand{\proves}{\vdash}
\newcommand{\provesIff}{\mathrel{\dashv\vdash}} \newcommand{\provesIff}{\mathrel{\dashv\vdash}}
\newcommand{\wand}{\;{{\mbox{---}}\!\!{*}}\;} \newcommand{\wand}{\mathrel{-\!\!*}}
% oh my... I have to wrap the "-" in a \mathrm, otherwise all hell breaks lose... % oh my... I have to wrap the "-" in a \mathrm, otherwise all hell breaks lose...
\newcommand{\fmapsto}[1][\mathrm{-}]{\xmapsto{#1}} \newcommand{\fmapsto}[1][]{\xmapsto{#1}}
\newcommand{\gmapsto}{\hookrightarrow}% \newcommand{\gmapsto}{\hookrightarrow}%
\newcommand{\fgmapsto}[1][\mathrm{-}]{\xhookrightarrow{#1}}% \newcommand{\fgmapsto}[1][\mathrm{-}]{\xhookrightarrow{#1}}%
\NewDocumentCommand\wpre{m O{} m}% \NewDocumentCommand\wpre{m O{} m}%
{\textlog{wp}_{#2}\spac#1\spac{\{#3\}}} {\textlog{wp}_{#2}\spac#1\spac{\left\{#3\right\}}}
\newcommand{\later}{\mathord{\triangleright}} \newcommand{\later}{\mathop{\triangleright}}
\newcommand{\always}{\Box{}} \newcommand{\always}{\mathop{\Box}}
\newcommand{\pure}{\mathop{\blacksquare}}
%% Invariants and Ghost ownership %% Invariants and Ghost ownership
% PDS: Was 0pt inner, 2pt outer. % PDS: Was 0pt inner, 2pt outer.
...@@ -222,7 +240,7 @@ ...@@ -222,7 +240,7 @@
\NewDocumentCommand \boxedassert {O{} m o}{% \NewDocumentCommand \boxedassert {O{} m o}{%
\tikz[baseline=(m.base)]{ \tikz[baseline=(m.base)]{
% \node[rectangle, draw,inner sep=0.8pt,anchor=base,#1] (m) {${#2}\mathstrut$}; % \node[rectangle, draw,inner sep=0.8pt,anchor=base,#1] (m) {${#2}\mathstrut$};
\node[rectangle,inner sep=0.8pt,outer sep=0.2pt,anchor=base] (m) {${#2}\mathstrut$}; \node[rectangle,inner sep=0.8pt,outer sep=0.2pt,anchor=base] (m) {${\,#2\,}\mathstrut$};
\draw[#1,boxedassert_border] ($(m.south west) + (0,0.65pt)$) rectangle ($(m.north east) + (0, 0.7pt)$); \draw[#1,boxedassert_border] ($(m.south west) + (0,0.65pt)$) rectangle ($(m.north east) + (0, 0.7pt)$);
}\IfNoValueF{#3}{^{\,#3}}% }\IfNoValueF{#3}{^{\,#3}}%
} }
...@@ -256,7 +274,7 @@ ...@@ -256,7 +274,7 @@
\NewDocumentCommand \vsW {O{} O{}} {\vsGen[#1]{\vsWand}[#2]} \NewDocumentCommand \vsW {O{} O{}} {\vsGen[#1]{\vsWand}[#2]}
% for now, the update modality looks like a pvs without masks. % for now, the update modality looks like a pvs without masks.
\NewDocumentCommand \upd {} {\mathord{\mid\kern-0.4ex\Rrightarrow\kern-0.25ex}} \NewDocumentCommand \upd {} {\mathop{\mid\kern-0.4ex\Rrightarrow\kern-0.25ex}}
%% Hoare Triples %% Hoare Triples
...@@ -269,12 +287,8 @@ ...@@ -269,12 +287,8 @@
\setbox1=\hoarescalebox{#1}{\copy0}% \setbox1=\hoarescalebox{#1}{\copy0}%
\setbox2=\hoarescalebox{#2}{\copy0}% \setbox2=\hoarescalebox{#2}{\copy0}%
\copy1{#3}\copy2% \copy1{#3}\copy2%
\;{#4}\;% \; #4 \;%
\copy1{#5}\copy2} \copy1{#5}\copy2}
\NewDocumentCommand \hoare {m m m O{}}{
\triple\{\}{#1}{#2}{#3}%
_{#4}%
}
\newcommand{\bracket}[4][]{% \newcommand{\bracket}[4][]{%
\setbox0=\hbox{$\mathsurround=0pt{#1}{#4}\mathstrut$}% \setbox0=\hbox{$\mathsurround=0pt{#1}{#4}\mathstrut$}%
...@@ -284,6 +298,11 @@ ...@@ -284,6 +298,11 @@
% \curlybracket[other] x % \curlybracket[other] x
\newcommand{\curlybracket}[2][]{\bracket[{#1}]\{\}{#2}} \newcommand{\curlybracket}[2][]{\bracket[{#1}]\{\}{#2}}
\newcommand{\anglebracket}[2][]{\bracket[{#1}]\langle\rangle{#2}} \newcommand{\anglebracket}[2][]{\bracket[{#1}]\langle\rangle{#2}}
\NewDocumentCommand \hoare {m m m O{}}{
\curlybracket{#1}\spac #2 \spac \curlybracket{#3}_{#4}%
}
% \hoareV[t] pre c post [mask] % \hoareV[t] pre c post [mask]
\NewDocumentCommand \hoareV {O{c} m m m O{}}{ \NewDocumentCommand \hoareV {O{c} m m m O{}}{
{\begin{aligned}[#1] {\begin{aligned}[#1]
...@@ -321,7 +340,10 @@ ...@@ -321,7 +340,10 @@
\newcommand{\valB}{w} \newcommand{\valB}{w}
\newcommand{\state}{\sigma} \newcommand{\state}{\sigma}
\newcommand{\step}{\ra} \newcommand{\step}{\ra}
\newcommand{\hstep}{\ra_{\mathsf{h}}}
\newcommand{\tpstep}{\ra_{\mathsf{tp}}}
\newcommand{\lctx}{K} \newcommand{\lctx}{K}
\newcommand{\Lctx}{\textdom{Ctx}}
\newcommand{\toval}{\mathrm{expr\any to\any val}} \newcommand{\toval}{\mathrm{expr\any to\any val}}
\newcommand{\ofval}{\mathrm{val\any to\any expr}} \newcommand{\ofval}{\mathrm{val\any to\any expr}}
...@@ -333,6 +355,8 @@ ...@@ -333,6 +355,8 @@
\newcommand{\cfg}[2]{{#1};{#2}} \newcommand{\cfg}[2]{{#1};{#2}}
\def\fill#1[#2]{#1 {[}\, #2\,{]} }
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% STANDARD DERIVED CONSTRUCTIONS % STANDARD DERIVED CONSTRUCTIONS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
...@@ -340,6 +364,11 @@ ...@@ -340,6 +364,11 @@
\newcommand{\unittt}{()} \newcommand{\unittt}{()}
\newcommand{\unit}{1} \newcommand{\unit}{1}
% Option
\newcommand{\option}[1]{#1^?}
\newcommand{\Some}{}
\newcommand{\None}{\textlog{None}}
% Agreement % Agreement
\newcommand{\agm}{\ensuremath{\textmon{Ag}}} \newcommand{\agm}{\ensuremath{\textmon{Ag}}}
\newcommand{\aginj}{\textlog{ag}} \newcommand{\aginj}{\textlog{ag}}
...@@ -383,12 +412,11 @@ ...@@ -383,12 +412,11 @@
\newcommand{\stsfstep}[1]{\xrightarrow{#1}} \newcommand{\stsfstep}[1]{\xrightarrow{#1}}
\newcommand{\stsftrans}[1]{\stsfstep{#1}^{*}} \newcommand{\stsftrans}[1]{\stsfstep{#1}^{*}}
\tikzstyle{sts} = [->,every node/.style={rectangle, rounded corners, draw, minimum size=1.2cm, align=center}] \tikzstyle{sts} = [->,every node/.style={rectangle, rounded corners, draw, minimum size=1.2cm, align=center}]
\tikzstyle{sts_arrows} = [arrows={->[scale=1.5]},every node/.style={font=\sffamily\small}] \tikzstyle{sts_arrows} = [arrows={->[scale=1.5]},every node/.style={font=\sffamily\small}]
%% Stored Propositions %% Stored Propositions
\newcommand{\mapstoprop}{\mathrel{\kern-0.5ex\tikz[baseline=(m)]{\node at (0,0) (m){}; \draw[line cap=round] (0,0.16) -- (0,-0.004);}\kern-1.5ex\Ra}} \newcommand{\mapstoprop}{\mathrel{\kern-0.5ex\tikz[baseline=(m)]{\node at (0,0) (m){}; \draw[line cap=round] (0,0.16) -- (0,-0.004);}\kern-1.5ex\Ra}}
\endinput \endinput
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment