iris.sty 15.5 KB
Newer Older
1 2 3
\NeedsTeXFormat{LaTeX2e}[1999/12/01]
\ProvidesPackage{iris}

Ralf Jung's avatar
Ralf Jung committed
4
\RequirePackage{faktor}
5 6
\RequirePackage{tikz}
\RequirePackage{scalerel}
7 8 9 10
\RequirePackage{array}
\RequirePackage{dashbox}
\RequirePackage{tensor}
\RequirePackage{xparse}
11
\RequirePackage{xifthen}
12 13
\RequirePackage{mathtools}

14 15 16 17 18
\usetikzlibrary{shapes}
\usetikzlibrary{arrows}
\usetikzlibrary{calc}
\usetikzlibrary{arrows.meta}

19 20 21 22 23 24 25 26 27 28

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% FONTS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\textdom}[1]{\textit{#1}} % for domains/sets/types
\newcommand{\textproj}[1]{\textsc{#1}} % for projections/fields
\newcommand{\textlog}[1]{\textsf{\upshape #1}} % for mathematical/logic-level identifiers (make sure we do not inherit italic shape from the environment)


29 30 31 32
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% MATH SYMBOLS & NOTATION & IDENTIFIERS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

33 34
\newcommand{\nat}{\mathbb{N}}

35
\DeclareMathOperator*{\Sep}{\scalerel*{\ast}{\sum}}
Ralf Jung's avatar
Ralf Jung committed
36 37
\newcommand*{\disj}[1][]{\mathrel{\#_{#1}}}
\newcommand\pord{\sqsubseteq}
Ralf Jung's avatar
Ralf Jung committed
38 39 40

\makeatletter%
\@ifundefined{dplus}{%
41
\newcommand\dplus{\mathbin{+\kern-1.0ex+}}
Ralf Jung's avatar
Ralf Jung committed
42 43
}{}
\makeatother%
44
\newcommand\fmap{\mathrel{\langle\$\rangle}}
Ralf Jung's avatar
Ralf Jung committed
45

46 47 48
\newcommand{\upclose}{\mathord{\uparrow}}
\newcommand{\ALT}{\ |\ }

49
\newcommand{\spac}{\hskip 0.2em plus 0.1em} % a space
50 51 52 53 54 55 56

\def\All #1.{\forall #1.\spac}%
\def\Exists #1.{\exists #1.\spac}%
\def\Ret #1.{#1.\spac}%

\newcommand{\any}{{\rule[-.2ex]{1ex}{.4pt}}}%

57
% For some reason \paragraph gives the weirdest errors ("missing \item").
58
\newcommand{\judgment}[2][]{\bigskip\noindent\textit{#1}\hspace{\stretch{1}}\fbox{$#2$}\nopagebreak}
59 60

\newcommand{\pfn}{\rightharpoonup}
61
\newcommand\fpfn{\xrightharpoonup{\smash{\raisebox{-.3ex}{\ensuremath{\scriptstyle\kern-0.25ex\textlog{fin}\kern-0.1ex}}}}}
Ralf Jung's avatar
Ralf Jung committed
62
\newcommand{\la}{\leftarrow}
63 64 65
\newcommand{\ra}{\rightarrow}
\newcommand{\Ra}{\Rightarrow}
\newcommand{\Lra}{\Leftrightarrow}
66 67 68
\newcommand\monra[1][]{\xrightarrow{\smash{\raisebox{-.3ex}{\ensuremath{\scriptstyle\kern-0.15ex\textlog{mon}_{#1}\kern-0.05ex}}}}}
\newcommand\monnra{\xrightarrow{\smash{\raisebox{-.3ex}{\ensuremath{\scriptstyle\kern-0.15ex\textlog{mon,ne}\kern-0.05ex}}}}}
\newcommand\nfn{\xrightarrow{\smash{\raisebox{-.3ex}{\ensuremath{\scriptstyle\kern-0.15ex\textlog{ne}\kern-0.05ex}}}}}
69
\newcommand{\eqdef}{\triangleq}
Ralf Jung's avatar
Ralf Jung committed
70 71
\newcommand{\bnfdef}{\vcentcolon\vcentcolon=}

Ralf Jung's avatar
Ralf Jung committed
72 73
\newcommand{\maybe}[1]{#1^?}

74 75
\newcommand*\setComp[2]{\left\{#1\spac\middle|\spac#2\right\}}
\newcommand*\set[1]{\left\{#1\right\}}
76
\newcommand*\record[1]{\left\{\spac#1\spac\right\}}
Ralf Jung's avatar
Ralf Jung committed
77
\newcommand*\recordComp[2]{\left\{\spac#1\spac\middle|\spac#2\spac\right\}}
78 79 80 81 82 83 84

\newenvironment{inbox}[1][]{
  \begin{array}[#1]{@{}l@{}}
}{
  \end{array}
}

85 86 87 88
\newcommand{\op}{\textlog{op}}
\newcommand{\dom}{\textlog{dom}}
\newcommand{\cod}{\textlog{cod}}
\renewcommand{\lim}{\textlog{lim}}
Ralf Jung's avatar
Ralf Jung committed
89
\renewcommand{\min}{\textlog{min}}
90 91

\newcommand{\Chains}{\textdom{Chains}}
92 93 94

\newcommand{\pset}[1]{\wp(#1)} % Powerset
\newcommand{\psetdown}[1]{\wp^\downarrow(#1)}
95
\newcommand{\finpset}[1]{\wp^\textlog{fin}(#1)}
Ralf Jung's avatar
Ralf Jung committed
96
\newcommand{\pmultiset}[1]{\wp^{+}(#1)}
97
\newcommand{\finpmultiset}[1]{\wp^{\textlog{fin},+}(#1)}
98 99 100

\newcommand{\Func}{F} % functor

101 102
\newcommand{\subst}[3]{{#1}[{#3} / {#2}]}

103 104 105 106
\newcommand{\mapelem}[2]{#1\mathop{\la}#2}
\newcommand{\mapinsert}[3]{#3\!\left[\mapelem{#1}{#2}\right]}
\newcommand{\mapdelete}[2]{#2\setminus\set{#1}}
\newcommand{\mapsingleton}[2]{\mapinsert{#1}{#2}{\,}}
Ralf Jung's avatar
Ralf Jung committed
107 108 109 110
\newcommand{\mapinsertComp}[4]
  {\mapinsert{#1}{#2 \spac\middle|\spac #3}{#4}}
\newcommand{\mapComp}[3]
  {\mapinsertComp{#1}{#2}{#3}{}}
111 112 113

\newcommand{\nil}{\epsilon}

Robbert Krebbers's avatar
Robbert Krebbers committed
114 115 116
% displaced dot
\newcommand{\dispdot}[2][.2ex]{\dot{\raisebox{0pt}[\dimexpr\height+#1][\depth]{$#2$}}}% \dispdot[<displace>]{<stuff>}

117 118 119 120 121 122 123 124
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% MODEL-SPECIFIC SYMBOLS & NOTATION & IDENTIFIERS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\wIso}{\xi}

\newcommand{\rs}{r}
\newcommand{\rsB}{s}
Ralf Jung's avatar
Ralf Jung committed
125
\newcommand{\rss}{R}
126 127 128 129 130 131

\newcommand{\pres}{\pi}
\newcommand{\wld}{w}
\newcommand{\ghostRes}{g}

%% Various pieces of syntax
Ralf Jung's avatar
Ralf Jung committed
132 133
\newcommand{\wsat}[3]{#1 \models_{#2} #3}
\newcommand{\wsatpre}{\textdom{pre-wsat}}
134 135 136 137

\newcommand{\wtt}[2]{#1 : #2} % well-typed term

\newcommand{\nequiv}[1]{\ensuremath{\mathrel{\stackrel{#1}{=}}}}
138
\newcommand{\nincl}[1]{\ensuremath{\mathrel{\stackrel{#1}{\subseteq}}}}
139 140 141 142
\newcommand{\notnequiv}[1]{\ensuremath{\mathrel{\stackrel{#1}{\neq}}}}
\newcommand{\nequivset}[2]{\ensuremath{\mathrel{\stackrel{#1}{=}_{#2}}}}
\newcommand{\nequivB}[1]{\ensuremath{\mathrel{\stackrel{#1}{\equiv}}}}
\newcommand{\latert}{\mathord{\blacktriangleright}}
Ralf Jung's avatar
Ralf Jung committed
143
\newcommand{\latertinj}{\textlog{next}}
144 145 146 147 148 149 150 151

\newcommand{\Sem}[1]{\llbracket #1 \rrbracket}

\newcommand{\sembox}[1]{\hfill \normalfont \mbox{\fbox{\(#1\)}}}
\newcommand{\typedsection}[2]{\subsubsection*{\rm\em #1 \sembox{#2}}}


%% Some commonly used identifiers
Ralf Jung's avatar
Ralf Jung committed
152
\newcommand{\SProp}{\textdom{SProp}}
153
\newcommand{\UPred}{\textdom{UPred}}
Ralf Jung's avatar
Ralf Jung committed
154 155
\newcommand{\mProp}{\textdom{Prop}} % meta-level prop
\newcommand{\iProp}{\textdom{iProp}}
Ralf Jung's avatar
Ralf Jung committed
156
\newcommand{\iPreProp}{\textdom{iPreProp}}
Ralf Jung's avatar
Ralf Jung committed
157
\newcommand{\Wld}{\textdom{Wld}}
Ralf Jung's avatar
Ralf Jung committed
158
\newcommand{\Res}{\textdom{Res}}
159

160 161 162
% List
\newcommand{\List}{\ensuremath{\textdom{List}}}

163 164 165 166
\newcommand{\ofe}{T}
\newcommand{\ofeB}{U}
\newcommand{\cofe}{\ofe}
\newcommand{\cofeB}{\ofeB}
167 168
\newcommand{\OFEs}{\mathbf{OFE}} % category of OFEs
\newcommand{\COFEs}{\mathbf{COFE}} % category of COFEs
169
\newcommand{\iFunc}{\Sigma}
Ralf Jung's avatar
Ralf Jung committed
170
\newcommand{\fix}{\textdom{fix}}
171 172 173 174 175 176

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% CMRA (RESOURCE ALGEBRA) SYMBOLS & NOTATION & IDENTIFIERS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\monoid}{M}
Ralf Jung's avatar
Ralf Jung committed
177
\newcommand{\mval}{\mathcal{V}}
Ralf Jung's avatar
Ralf Jung committed
178
\newcommand{\mvalFull}{\overline{\mathcal{V}}}
179 180 181 182 183 184 185

\newcommand{\melt}{a}
\newcommand{\meltB}{b}
\newcommand{\meltC}{c}
\newcommand{\melts}{A}
\newcommand{\meltsB}{B}

186
\newcommand{\f}{\textlog{f}} % used as subscript, for "frame"
Ralf Jung's avatar
Ralf Jung committed
187

188
\newcommand{\munit}{\varepsilon}
Ralf Jung's avatar
Ralf Jung committed
189
\newcommand{\mcore}[1]{{\mid}#1{\mid}} % using "|" here makes LaTeX diverge. WTF.
Ralf Jung's avatar
Ralf Jung committed
190
\newcommand{\bigmcore}[1]{{\big|}#1{\big|}} % using "|" here makes LaTeX diverge. WTF.
Ralf Jung's avatar
Ralf Jung committed
191
\newcommand{\mnocore}{\bot}
192
\newcommand{\mtimes}{\mathbin{\cdot}}
193
\newcommand{\mundef}{\lightning}
194

195
\newcommand{\exclusive}{\textlog{exclusive}}
Ralf Jung's avatar
Ralf Jung committed
196

197
\newcommand{\mupd}{\rightsquigarrow}
198
\newcommand{\lupd}{\rightsquigarrow_{\textlog{L}}}
Ralf Jung's avatar
Ralf Jung committed
199 200 201 202 203 204 205
\newcommand{\mincl}[1][]{%
  \ensuremath{\mathrel{\vbox{\offinterlineskip\ialign{%
    \hfil##\hfil\cr
    \ensuremath{\scriptstyle #1}\cr
    \noalign{\kern-0.25ex}
    $\preccurlyeq$\cr
}}}}}
206

207
\newcommand{\CMRAs}{\mathbf{Camera}} % category of Cameras/CMRAs
208 209 210 211 212 213 214 215 216 217 218 219 220 221

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% LOGIC SYMBOLS & NOTATION & IDENTIFIERS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\Sig}{\mathcal{S}}
\newcommand{\SigType}{\mathcal{T}}
\newcommand{\SigFn}{\mathcal{F}}
\newcommand{\SigAx}{\mathcal{A}}
\newcommand{\sigtype}{T}
\newcommand{\sigfn}{F}
\newcommand{\sigax}{A}

\newcommand{\type}{\tau}
222
\newcommand{\typeB}{\sigma}
223 224 225 226 227 228 229 230

\newcommand{\var}{x}
\newcommand{\varB}{y}
\newcommand{\varC}{z}

\newcommand{\term}{t}
\newcommand{\termB}{u}

Robbert Krebbers's avatar
Robbert Krebbers committed
231
\newcommand{\venv}{\rho}
232 233 234 235 236 237 238
\newcommand{\vctx}{\Gamma}
\newcommand{\pfctx}{\Theta}

\newcommand{\prop}{P}
\newcommand{\propB}{Q}
\newcommand{\propC}{R}

239 240 241 242 243 244 245
% pure propositions
\newcommand{\pprop}{\phi}
\newcommand{\ppropB}{\psi}

\newcommand{\pred}{\varPhi}
\newcommand{\predB}{\Psi}
\newcommand{\predC}{\Zeta}
246 247 248 249 250 251

\newcommand{\gname}{\gamma}
\newcommand{\iname}{\iota}

\newcommand{\mask}{\mathcal{E}}
\newcommand{\namesp}{\mathcal{N}}
Ralf Jung's avatar
Ralf Jung committed
252
\newcommand{\namecl}[1]{{#1^{\kern0.2ex\uparrow}}}
253

Ralf Jung's avatar
Ralf Jung committed
254 255
\newcommand{\fixp}{\mathit{fix}}

256
%% various pieces of Syntax
257 258
\def\MU #1.{\mu #1.\spac}%
\def\Lam #1.{\lambda #1.\spac}%
259 260

\newcommand{\proves}{\vdash}
Ralf Jung's avatar
Ralf Jung committed
261
\newcommand{\provesIff}{\mathrel{\dashv\vdash}}
262

263 264
\newcommand{\wand}{\mathrel{-\!\!\ast}}
\newcommand{\wandIff}{\mathrel{\ast\!\!{-}\!\!\ast}}
265 266

% oh my... I have to wrap the "-" in a \mathrm, otherwise all hell breaks lose...
267
\newcommand{\fmapsto}[1][]{\xmapsto{\smash{\raisebox{-.15ex}{\ensuremath{\scriptstyle #1}}}}}
268 269 270
\newcommand{\gmapsto}{\hookrightarrow}%
\newcommand{\fgmapsto}[1][\mathrm{-}]{\xhookrightarrow{#1}}%

Ralf Jung's avatar
Ralf Jung committed
271 272
\NewDocumentCommand\wpre{O{} m O{} m}%
  {\textlog{wp}^{#1}_{#3}\spac#2\spac{\left\{#4\right\}}}
273

Robbert Krebbers's avatar
Robbert Krebbers committed
274 275
\newcommand{\stateinterp}{S}

Ralf Jung's avatar
Ralf Jung committed
276 277 278 279
\newcommand\stuckness{s}
\newcommand\NotStuck{\textlog{NotStuck}}
\newcommand\MaybeStuck{\textlog{Stuck}}

Ralf Jung's avatar
Ralf Jung committed
280 281
\newcommand{\later}{\mathop{{\triangleright}}}
\newcommand*{\lateropt}[1]{\mathop{{\later}^{#1}}}
282
\newcommand{\always}{\mathop{\boxempty}}
Ralf Jung's avatar
Ralf Jung committed
283
\newcommand{\plainly}{\mathop{\blacksquare}}
284
\newcommand{\pers}{\mathop{\boxdot}}
285 286 287 288 289 290 291 292

%% Invariants and Ghost ownership
% PDS: Was 0pt inner, 2pt outer.
% \boxedassert [tikzoptions] contents [name]
\tikzstyle{boxedassert_border} = [sharp corners,line width=0.2pt]
\NewDocumentCommand \boxedassert {O{} m o}{%
	\tikz[baseline=(m.base)]{
		%	  \node[rectangle, draw,inner sep=0.8pt,anchor=base,#1] (m) {${#2}\mathstrut$};
293
		\node[rectangle,inner sep=0.8pt,outer sep=0.2pt,anchor=base] (m) {${\,#2\,}\mathstrut$};
294 295 296 297
		\draw[#1,boxedassert_border] ($(m.south west) + (0,0.65pt)$) rectangle ($(m.north east) + (0, 0.7pt)$);
	}\IfNoValueF{#3}{^{\,#3}}%
}
\newcommand*{\knowInv}[2]{\boxedassert{#2}[#1]}
Ralf Jung's avatar
Ralf Jung committed
298
\newcommand*{\invM}[2]{\textlog{Inv}^{#1}\left(#2\right)}
299
\newcommand*{\ownGhost}[2]{\boxedassert[densely dashed]{#2}[#1]}
Ralf Jung's avatar
Ralf Jung committed
300
\newcommand*{\ownM}[1]{\textlog{Own}\left(#1\right)}
Ralf Jung's avatar
Ralf Jung committed
301
\newcommand*{\ownPhys}[1]{\textlog{Phy}(#1)}
302 303 304 305 306 307 308 309 310 311 312

%% View Shifts
\NewDocumentCommand \vsGen {O{} m O{}}%
  {\mathrel{%
    \ifthenelse{\equal{#3}{}}{%
      % Just one mask, or none
      {#2}_{#1}%
    }{%
      % Two masks
      \tensor*[^{#1}]{#2}{^{#3}}
    }%
313
  }}%
314
\NewDocumentCommand \vs {O{} O{}} {\vsGen[#1]{\Rrightarrow}[#2]}
Robbert Krebbers's avatar
Robbert Krebbers committed
315
\NewDocumentCommand \bvs {O{} O{}} {\vsGen[#1]{\dispdot[0.02ex]{\Rrightarrow}}[#2]}
316
\NewDocumentCommand \vsL {O{} O{}} {\vsGen[#1]{\Lleftarrow}[#2]}
317
\NewDocumentCommand \vsE {O{} O{}} %
318
  {\vsGen[#1]{\Lleftarrow\!\!\!\Rrightarrow}[#2]}
319
\NewDocumentCommand \pvs {O{} O{}} {\mathord{\vsGen[#1]{{\mid\kern-0.5ex\Rrightarrow\kern-0.25ex}}[#2]\kern0.2ex}}
320

321
\newcommand\vsWand{{\displaystyle\equiv\kern-1.6ex-\kern-1.5ex\smash{\scalerel*{\vphantom-\ast}{\sum}}\kern-0.2ex}}
Ralf Jung's avatar
Ralf Jung committed
322 323
\NewDocumentCommand \vsW {O{} O{}} {\vsGen[#1]{\vsWand}[#2]}

324 325 326
\newcommand\vsWandStep{{\displaystyle\raisebox{0.106ex}{\scaleobj{0.82}{\later}}\kern-1.65ex\equiv\kern-1.6ex-\kern-1.5ex\smash{\scalerel*{\vphantom-\ast}{\sum}}\kern-0.2ex}}
\NewDocumentCommand \vsWS {O{} O{}} {\vsGen[#1]{\vsWandStep}[#2]}

327
% for now, the update modality looks like a pvs without masks.
Robbert Krebbers's avatar
Robbert Krebbers committed
328
\NewDocumentCommand \upd {} {\mathop{\dispdot[-0.2ex]{\mid\kern-0.4ex\Rrightarrow\kern-0.25ex}}}
329

330
\NewDocumentCommand\Acc{O{} O{} m m}{#3 \mathrel{~\vsGen[#1]{\propto}[#2]~} #4}
331

332 333

%% Hoare Triples
334 335 336

% needs extra {...} for some weird reason
\newcommand{\curlybracket}[1]{{\left\{#1\right\}}}
337 338 339 340 341

\NewDocumentCommand \hoare {m m m O{}}{
	\curlybracket{#1}\spac #2 \spac \curlybracket{#3}_{#4}%
}

342 343 344 345 346
% \hoareV[t] pre c post [mask]
\NewDocumentCommand \hoareV {O{c} m m m O{}}{
		{\begin{aligned}[#1]
		&\curlybracket{#2} \\
		&\quad{#3} \\
347
		&\curlybracket{#4}_{#5}
348 349 350 351 352
		\end{aligned}}%
}
% \hoareHV[t] pre c post [mask]
\NewDocumentCommand \hoareHV {O{c} m m m O{}}{
	{\begin{aligned}[#1]
353 354 355 356 357 358 359 360 361
	&\curlybracket{#2} \spac {#3} \\
	&\curlybracket{#4}_{#5}
	\end{aligned}}%
}
% \hoareVH[t] pre c post [mask]
\NewDocumentCommand \hoareVH {O{c} m m m O{}}{
	{\begin{aligned}[#1]
	&\curlybracket{#2} \\
        & {#3}\spac \curlybracket{#4}_{#5}
362 363 364 365 366
	\end{aligned}}%
}


%% Some commonly used identifiers
Ralf Jung's avatar
Ralf Jung committed
367
\newcommand{\inhabited}[1]{\textlog{inhabited}(#1)}
368
\newcommand{\infinite}{\textlog{infinite}}
369
\newcommand{\timeless}[1]{\textlog{timeless}(#1)}
370
\newcommand{\persistent}[1]{\textlog{persistent}(#1)}
371

372 373 374
\newcommand\InvName{\textdom{InvName}}
\newcommand\GName{\textdom{GName}}

375 376
\newcommand{\Prop}{\textdom{iProp}}
\newcommand{\Pred}{\textdom{Pred}}
377 378 379

\newcommand{\TRUE}{\textlog{True}}
\newcommand{\FALSE}{\textlog{False}}
380
\newcommand{\EMP}{\textlog{Emp}}
381 382

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Ralf Jung's avatar
Ralf Jung committed
383
% GENERIC LANGUAGE SYNTAX AND SEMANTICS
384 385 386 387 388
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\expr}{e}
\newcommand{\val}{v}
\newcommand{\valB}{w}
\newcommand{\state}{\sigma}
389 390 391 392
\newcommand{\step}[1][]{\xrightarrow{{#1}}_{\textlog{t}}}
\newcommand{\hstep}[1][]{\xrightarrow{{#1}}_{\textlog{h}}}
\newcommand{\tpstep}[1][]{\xrightarrow{{#1}}_{\textlog{tp}}}
\newcommand{\tpsteps}[1][]{\xrightarrow{{#1}}\mathrel{\vphantom{\to}^{*}_{\textlog{tp}}}}
393
\newcommand{\lctx}{K}
394
\newcommand{\Lctx}{\textdom{Ctx}}
Ralf Jung's avatar
Ralf Jung committed
395 396
\newcommand{\obs}{\kappa}

Ralf Jung's avatar
Ralf Jung committed
397 398 399 400 401 402 403
\newcommand{\State}{\kern-0.05em\textdom{State}}
\newcommand{\Val}{\kern-0.2em\textdom{Val}}
\newcommand{\Loc}{\kern-0.05em\textdom{Loc}}
\newcommand{\Expr}{\kern-0.05em\textdom{Expr}}
\newcommand{\Var}{\kern-0.2em\textdom{Var}}
\newcommand{\Obs}{\kern-0.1em\textdom{Obs}}
\newcommand{\ThreadPool}{\kern-0.05em\textdom{ThreadPool}}
404

405 406 407 408 409
\newcommand{\toval}{\textlog{expr\any to\any val}}
\newcommand{\ofval}{\textlog{val\any to\any expr}}
\newcommand{\atomic}{\textlog{atomic}}
\newcommand{\stronglyAtomic}{\textlog{strongly\any{}atomic}}
\newcommand{\red}{\textlog{red}}
410 411 412 413 414 415
\newcommand{\Lang}{\Lambda}

\newcommand{\tpool}{T}

\newcommand{\cfg}[2]{{#1};{#2}}

416
\def\fillctx#1[#2]{#1 {[}\, #2\,{]} }
417

418 419 420 421
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% STANDARD DERIVED CONSTRUCTIONS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Ralf Jung's avatar
Ralf Jung committed
422 423 424
\newcommand{\unittt}{()}
\newcommand{\unit}{1}

425
% Agreement
426
\newcommand{\agm}{\ensuremath{\textdom{Ag}}}
Ralf Jung's avatar
Ralf Jung committed
427
\newcommand{\aginj}{\textlog{ag}}
428 429

% Fraction
430
\newcommand{\fracm}{\ensuremath{\textdom{Frac}}}
Ralf Jung's avatar
Ralf Jung committed
431
\newcommand{\fracinj}{\textlog{frac}}
432 433

% Exclusive
434
\newcommand{\exm}{\ensuremath{\textdom{Ex}}}
Ralf Jung's avatar
Ralf Jung committed
435
\newcommand{\exinj}{\textlog{ex}}
436 437

% Auth
438 439 440 441
\newcommand{\authm}{\textdom{Auth}}
\newcommand{\authinj}{\textlog{auth}}
\newcommand{\authfull}{\mathord{\bullet}}
\newcommand{\authfrag}{\mathord{\circ}}
442 443 444 445

\newcommand{\AuthInv}{\textsf{AuthInv}}
\newcommand{\Auth}{\textsf{Auth}}

Ralf Jung's avatar
Ralf Jung committed
446
% Sum
447
\newcommand{\csumm}{\mathrel{+_{\!\mundef}}}
Ralf Jung's avatar
Ralf Jung committed
448 449 450
\newcommand{\cinl}{\textsf{inl}}
\newcommand{\cinr}{\textsf{inr}}

Ralf Jung's avatar
Ralf Jung committed
451
% STSs
452
\newcommand{\STSCtx}{\textlog{StsCtx}}
453
\newcommand{\STSInv}{\textlog{StsInv}}
454
\newcommand{\STSSt}{\textlog{StsSt}}
455 456 457
\newcommand{\STSclsd}{\textlog{closed}}
\newcommand{\STSauth}{\textlog{auth}}
\newcommand{\STSfrag}{\textlog{frag}}
458 459 460
\newcommand{\STSS}{\mathcal{S}} % states
\newcommand{\STST}{\mathcal{T}} % tokens
\newcommand{\STSL}{\mathcal{L}} % labels
461
\newcommand{\stsstep}{\ra}
462
\newcommand{\ststrans}{\ra^{*}}%	the relation relevant to the STS rules
463 464
\newcommand{\stsfstep}[1]{\xrightarrow{#1}}
\newcommand{\stsftrans}[1]{\stsfstep{#1}^{*}}
465
\newcommand{\stsinterp}{\varphi}
466

467 468
\tikzstyle{sts_state} = [rectangle, rounded corners, draw, minimum size=1.2cm, align=center]
\tikzstyle{sts_arrows} = [->,arrows={->[scale=1.5]},every node/.style={font=\sffamily\small}]
469 470

%% Stored Propositions
471
\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}}
472

Ralf Jung's avatar
Ralf Jung committed
473 474
%% Cancellable invariants
\newcommand\CInv[3]{\textlog{CInv}^{#1,#2}(#3)}
475
\newcommand*\CInvTok[2]{{[}\textlog{CInv}:#1{]}_{#2}}
Ralf Jung's avatar
Ralf Jung committed
476

Ralf Jung's avatar
Ralf Jung committed
477
%% Non-atomic invariants
478 479
\newcommand*\pid{p}
\newcommand\NaInv[3]{\textlog{NaInv}^{#1.#2}(#3)}
Ralf Jung's avatar
Ralf Jung committed
480

481 482
\newcommand*\NaTok[1]{{[}\textlog{NaInv}:#1{]}}
\newcommand*\NaTokE[2]{{[}\textlog{NaInv}:#1.#2{]}}
Ralf Jung's avatar
Ralf Jung committed
483

Ralf Jung's avatar
Ralf Jung committed
484
%% Boxes
485 486
\newcommand*\sname{\iota}
\newcommand*\BoxState{\textdom{BoxState}}
Ralf Jung's avatar
Ralf Jung committed
487 488 489 490 491
\newcommand*\BoxFull{\textlog{full}}
\newcommand*\BoxEmp{\textlog{empty}}
\newcommand*\BoxSlice[3]{\textlog{BoxSlice}(#1, #2, #3)}
\newcommand*\ABox[3]{\textlog{Box}(#1, #2, #3)}

492
\endinput
493