macros.tex

%%
%% Defined-as equality
%%
\newcommand{\defas}[0]{\mathrel{\overset{\makebox[0pt]{\mbox{\normalfont\tiny\text{def}}}}{=}}}
\newcommand{\defnas}[0]{\mathrel{:=}}
\newcommand{\simdefas}[0]{\mathrel{\overset{\makebox[0pt]{\mbox{\normalfont\tiny\text{def}}}}{\simeq}}}
\newcommand{\adef}[0]{\mathrel{\overset{\makebox[0pt]{\mbox{\normalfont\tiny{\text{$\alpha$-def}}}}}{\simeq}}}

%%
%% Some useful maths abbreviations
%%
\newcommand{\C}{\ensuremath{\mathbb{C}}}
\newcommand{\N}{\ensuremath{\mathbb{N}}}
\newcommand{\R}{\ensuremath{\mathbb{R}}}
\newcommand{\Z}{\ensuremath{\mathbb{Z}}}
\newcommand{\B}{\ensuremath{\mathbb{B}}}
\newcommand{\BB}[1]{\ensuremath{\mathbf{#1}}}
\newcommand{\CC}{\keyw{ctrl}}
% \newcommand{\Delim}[1]{\ensuremath{\langle\!\!\mkern-1.5mu\langle#1\rangle\!\!\mkern-1.5mu\rangle}}
\newcommand{\Delim}[1]{\ensuremath{\keyw{del}.#1}}
\newcommand{\sembr}[1]{\ensuremath{\llbracket #1 \rrbracket}}
\newcommand{\BigO}{\ensuremath{\mathcal{O}}}
\newcommand{\SC}{\ensuremath{\mathsf{S}}}
\newcommand{\ST}{\ensuremath{\mathsf{T}}}
\newcommand{\ar}{\ensuremath{\mathsf{ar}}}
\newcommand{\Tm}{\ensuremath{\mathsf{Tm}}}
\newcommand{\Ty}{\ensuremath{\mathsf{Ty}}}

%%
%% Partiality
%%
\newcommand{\pto}[0]{\ensuremath{\rightharpoonup}}

%%
%% Operation arrows
%%
\newcommand{\opto}[0]{\ensuremath{\twoheadrightarrow}}

%%
%% Calculi names.
%%
\newcommand{\Links}{Links\xspace}
\newcommand{\CoreLinks}{\ensuremath{\mathsf{CoreLinks}}\xspace}
\newcommand{\BCalc}{\ensuremath{\lambda_{\mathsf{b}}}\xspace}
\newcommand{\BCalcRec}{\ensuremath{\lambda_{\mathsf{b}+\mathsf{rec}}}\xspace}
\newcommand{\HCalc}{\ensuremath{\lambda_{\mathsf{h}}}\xspace}
\newcommand{\SCalc}{\ensuremath{\lambda_{\mathsf{h^\dagger}}}\xspace}
\newcommand{\HSCalc}{\ensuremath{\lambda_{\mathsf{h^\delta}}}\xspace}
\newcommand{\EffCalc}{\ensuremath{\lambda_{\mathsf{eff}}}\xspace}
\newcommand{\UCalc}{\ensuremath{\lambda_{\mathsf{u}}}\xspace}
\newcommand{\param}{\ensuremath{\ddagger}}
\newcommand{\HPCalc}{\ensuremath{\lambda_{\mathsf{h^\param}}}\xspace}
\newcommand{\HPCF}{\ensuremath{\lambda^\rightarrow_{\mathsf{h}}}\xspace}
\newcommand{\BPCF}{\ensuremath{\lambda^\rightarrow_{\mathsf{b}}}\xspace}

%%
%% Calculi terms and types type-setting.
%%
\newcommand{\revto}{\ensuremath{\leftarrow}}

\newcommand{\dec}[1]{\mathsf{#1}}
\newcommand{\keyw}[1]{\mathbf{#1}}
\newcommand{\Handle}{\keyw{handle}}
\newcommand{\ParamHandle}{\Handle^\param}
\newcommand{\ShallowHandle}{\ensuremath{\keyw{handle}^\dagger}}
\newcommand{\With}{\keyw{with}}
\newcommand{\Let}{\keyw{let}}
\newcommand{\Rec}{\keyw{rec}}
\newcommand{\In}{\keyw{in}}
\newcommand{\Do}{\keyw{do}}
\newcommand{\Return}{\keyw{return}}
\newcommand{\Val}{\keyw{val}}
\newcommand{\Case}{\keyw{case}}
\newcommand{\If}{\keyw{if}}
\newcommand{\Then}{\keyw{then}}
\newcommand{\Else}{\keyw{else}}
\newcommand{\Absurd}{\keyw{absurd}}
\newcommand{\Record}[1]{\ensuremath{\langle #1 \rangle}}
\newcommand{\Op}[1]{\ensuremath{\langle\!\!\langle #1 \rangle\!\!\rangle}}
%\newcommand{\Op}[1]{\ensuremath{\{#1\}}}
\newcommand{\OpCase}[3]{\Op{#1~#2 \opto #3}}
\newcommand{\ExnCase}[2]{\Op{#1~#2}}
\newcommand{\Unit}{\Record{}}
\newcommand{\Inl}{\keyw{inl}}
\newcommand{\Inr}{\keyw{inr}}
\newcommand{\Thunk}{\lambda \Unit.}
\newcommand{\PCFRef}{\dec{Ref}}
\newcommand{\refv}{\keyw{ref}}

\newcommand{\Pre}[1]{\mathsf{Pre}(#1)}
\newcommand{\Abs}{\mathsf{Abs}}
\newcommand{\Presence}{\mathsf{Presence}}
\newcommand{\Row}{\mathsf{Row}}
\newcommand{\Type}{\mathsf{Type}}
\newcommand{\Ground}{\mathsf{ground}}

\newcommand{\Comp}{\mathsf{Comp}}
\newcommand{\Effect}{\mathsf{Effect}}
\newcommand{\Handler}{\mathsf{Handler}}

\newcommand{\ZeroType}{0}
\newcommand{\UnitType}{1}
\newcommand{\One}{1}
\newcommand{\Int}{\mathsf{Int}}
\newcommand{\Float}{\mathsf{Float}}
\newcommand{\Bool}{\mathsf{Bool}}
\newcommand{\List}{\mathsf{List}}
\newcommand{\Nat}{\mathsf{Nat}}
\newcommand{\Choose}{\dec{Choose}}
\newcommand{\Count}{\dec{count}}
\newcommand{\GenericSearch}{\dec{genericSearch}}
\newcommand{\Predicate}{\dec{Predicate}}
\newcommand{\Point}{\dec{Point}}
\newcommand{\Branch}{\dec{Branch}}
\newcommand{\Get}{\dec{Get}}
\newcommand{\Put}{\dec{Put}}
\newcommand{\Zero}{\dec{Zero}}
\newcommand{\Fail}{\dec{Fail}}
\newcommand{\Read}{\dec{Read}}
\newcommand{\Write}{\dec{Write}}
\newcommand{\Char}{\dec{Char}}
\newcommand{\String}{\dec{String}}

\newcommand{\True}{\mathsf{true}}
\newcommand{\False}{\mathsf{false}}

\newcommand{\eff}{!}
\newcommand{\typ}[2]{#1 \vdash #2}
\newcommand{\typv}[2]{#1 \vdash #2}
\newcommand{\typc}[3]{#1 \vdash #2 \eff #3}
\newcommand{\Harrow}{\Rightarrow}

\newcommand{\FTV}{\ensuremath{\mathrm{FTV}}}
\newcommand{\FV}{\ensuremath{\mathrm{FV}}}

\newcommand{\reducesto}[0]{\ensuremath{\leadsto}}
\newcommand{\areducesto}{\ensuremath{\reducesto_{\textrm{a}}}}
\newcommand{\stepsto}[0]{\ensuremath{\longrightarrow}}
\newcommand{\Stepsto}{\Longrightarrow}
\newcommand{\EC}{\ensuremath{\mathcal{E}}}

\newcommand{\BL}{\ensuremath{\mathsf{BL}}}

\newcommand{\dom}{\ensuremath{\mathsf{dom}}}

\newcommand{\Res}{\keyw{res}}

\newcommand{\Cong}{\mathrm{cong}}

\newcommand{\AlgTheory}{\ensuremath{\mathcal{T}}}

%% Handler projections.
\newcommand{\mret}{\mathrm{ret}}
\newcommand{\mops}{\mathrm{ops}}
\newcommand{\hret}{H^{\mret}}
\newcommand{\hval}{\hret}
\newcommand{\hops}{H^{\mops}}
%\newcommand{\hex}{H^{\mathrm{ex}}}
\newcommand{\hell}{H^{\ell}}
\newcommand{\gell}{\theta^{\ell}}

\newcommand{\depth}{\delta}

\newcommand{\alertbox}[2]{{\par\noindent\small\color{red} \framebox{\parbox{\dimexpr\linewidth-2\fboxsep-2\fboxrule}{\textbf{#1:} #2}}}}
\newcommand{\todo}[1]{\alertbox{TODO}{#1}}
\newcommand{\dhil}[1]{\alertbox{Daniel}{#1}}

%%
%% Labels
%%
\newcommand{\slab}[1]{\ensuremath{\mathsf{#1}}}
\newcommand{\rulelabel}[2]{\ensuremath{\mathsf{#1\textrm{-}#2}}}
\newcommand{\klab}[1]{\rulelabel{K}{#1}}
\newcommand{\semlab}[1]{\rulelabel{S}{#1}}
\newcommand{\usemlab}[1]{\rulelabel{U}{#1}}
\newcommand{\tylab}[1]{\rulelabel{T}{#1}}
\newcommand{\mlab}[1]{\rulelabel{M}{#1}}
\newcommand{\siglab}[1]{\rulelabel{Sig}{#1}}
\newcommand{\rowlab}[1]{\rulelabel{R}{#1}}

%%
%% Syntactic categories.
%%
\newcommand{\CatName}[1]{\textrm{#1}}
\newcommand{\CompCat}{\CatName{Comp}}
\newcommand{\UCompCat}{\CatName{UComp}}
\newcommand{\UValCat}{\CatName{UVal}}
\newcommand{\SCompCat}{\CatName{SComp}}
\newcommand{\SValCat}{\CatName{SVal}}
\newcommand{\SPatCat}{\CatName{SPat}}
\newcommand{\ValCat}{\CatName{Val}}
\newcommand{\VarCat}{\CatName{Var}}
\newcommand{\ValTypeCat}{\CatName{VType}}
\newcommand{\CompTypeCat}{\CatName{CType}}
\newcommand{\HandlerTypeCat}{\CatName{HType}}
\newcommand{\PresenceCat}{\CatName{Presence}}
\newcommand{\TypeCat}{\CatName{Type}}
\newcommand{\TyVarCat}{\CatName{TVar}}
\newcommand{\KindCat}{\CatName{Kind}}
\newcommand{\RowCat}{\CatName{Row}}
\newcommand{\EffectCat}{\CatName{Effect}}
\newcommand{\TermCat}{\CatName{Term}}
\newcommand{\LabelCat}{\CatName{Label}}
\newcommand{\TyEnvCat}{\CatName{TyEnv}}
\newcommand{\KindEnvCat}{\CatName{KindEnv}}
\newcommand{\EvalCat}{\CatName{Cont}}
\newcommand{\UEvalCat}{\CatName{UCont}}
\newcommand{\HandlerCat}{\CatName{HDef}}
\newcommand{\MConfCat}{\CatName{Conf}}
\newcommand{\MEnvCat}{\CatName{Env}}
\newcommand{\MValCat}{\CatName{Mval}}
\newcommand{\MGContCat}{\CatName{GenCont}}
\newcommand{\MGFrameCat}{\CatName{GenFrame}}
\newcommand{\MPContCat}{\CatName{PureCont}}
\newcommand{\MPFrameCat}{\CatName{PureFrame}}
\newcommand{\MHCloCat}{\CatName{HClo}}

%%
%% Lindley's array stuff.
%%
\newcommand{\ba}{\begin{array}}
\newcommand{\ea}{\end{array}}

\newcommand{\bl}{\ba[t]{@{}l@{}}}
\newcommand{\el}{\ea}


%%
%% Lindley's syntax, reductions, equations, and derivation environments.
%%
\newenvironment{syntax}{\[\ba{@{}l@{\quad}r@{~}c@{~}l@{}}}{\ea\]\ignorespacesafterend}
\newenvironment{reductions}{\[\ba{@{}l@{\qquad}@{}r@{~~}c@{~~}l@{}}}{\ea\]\ignorespacesafterend}

\newenvironment{eqs}{\ba{@{}r@{~}c@{~}l@{}}}{\ea}
\newenvironment{equations}{\[\ba{@{}r@{~}c@{~}l@{}}}{\ea\]\ignorespacesafterend}
\newcommand\numberthis{\addtocounter{equation}{1}\tag{$\ast$\theequation}} % Numbering equations
\newenvironment{derivation}{\begin{displaymath}\ba{@{}r@{~}l@{}}}{\ea\end{displaymath}\ignorespacesafterend}
\newcommand{\reason}[1]{\quad (\text{#1})}


\newenvironment{smathpar}{\vspace{-3ex}\small\begin{mathpar}}{\end{mathpar}\normalsize\ignorespacesafterend}

%%
%% Lists
%%
\newcommand{\nil}{\ensuremath{[]}}
\newcommand{\cons}{\ensuremath{::}}

\newcommand{\concat}{\mathbin{+\!\!+}}
\newcommand{\revconcat}{\mathbin{\widehat{\concat}}}
\newcommand{\snoc}[2]{\ensuremath{#1 \concat [#2]}}

%%
%% CPS notation
%%
% static / dynamic stuff
\newcommand{\scol}[1]{{\color{blue}#1}}
\newcommand{\dcol}[1]{{\color{red}#1}}

\newcommand{\static}[1]{\scol{\overline{#1}}}
\newcommand{\dynamic}[1]{\dcol{\underline{#1}}}
\newcommand{\nary}[1]{\overline{#1}}

\newcommand{\slam}{\static{\lambda}}
\newcommand{\dlam}{\dynamic{\lambda}}
\newcommand{\sapp}{\mathbin{\static{@}}}
\newcommand{\dapp}{\mathbin{\dynamic{@}}}

\newcommand{\reify}{\mathord{\downarrow}}
\newcommand{\reflect}{\mathord{\uparrow}}

\newcommand{\scons}{\mathbin{\static{\cons}}}
\newcommand{\dcons}{\mathbin{\dynamic{\cons}}}

\newcommand{\snil}{\static{\nil}}
\newcommand{\dnil}{\dynamic{\nil}}

\newcommand{\sRecord}[1]{\static{\langle}#1\static{\rangle}}
\newcommand{\dRecord}[1]{\dynamic{\langle}#1\dynamic{\rangle}}

\newcommand{\sQ}{\mathcal{Q}}
\newcommand{\sV}{\mathcal{V}}
\newcommand{\sW}{\mathcal{W}}

\newcommand{\sM}{\mathcal{M}}
\renewcommand{\snil}{\reflect \dnil}

\newcommand{\cps}[1]{\ensuremath{\llbracket #1 \rrbracket}}
\newcommand{\pcps}[1]{\top\cps{#1}}

\newcommand{\hforward}{M_{\textrm{forward}}}
\newcommand{\hid}{V_{\textrm{id}}}

% continuation application
\newcommand{\kapp}{\keyw{app}}

%%% Continuation names
%%% The following set of macros are a bit more consistent with those
%%% currently used by the abstract machine, and don't use the plural
%%% convention of functional programming.

% dynamic
\newcommand{\dlf}{f}    % let frames
\newcommand{\dlk}{fs}   % let continuations
\newcommand{\dhf}{q}    % handler frames
\newcommand{\dhk}{ks}    % handler continuations
\newcommand{\dhkr}{rs}  % reverse handler continuations
\newcommand{\dLet}{\dynamic{\Let}}
\newcommand{\dIn}{\dynamic{\In}}

% static
\newcommand{\slf}{\phi}    % let frames
\newcommand{\slk}{\sigma}  % let continuations
\newcommand{\shf}{\theta}  % handler frames
\newcommand{\shk}{\kappa}  % handler continuations
\newcommand{\sLet}{\static{\Let}}
\newcommand{\sIn}{\static{\In}}
% \newcommand{\sk}{\kappa}
% \newcommand{\sks}{\mathit{\kappa s}}
\newcommand{\sks}{\kappa}
% \newcommand{\sh}{\eta}
\newcommand{\sk}{\theta}
\newcommand{\sh}{\chi}
\newcommand{\sx}{\varepsilon}

\newcommand{\sP}{\mathcal{P}}
\newcommand{\VS}{VS}
\newcommand{\Vmap}{\keyw{vmap}}
\newcommand{\Vmapsnd}{\keyw{vmapsnd}}
\newcommand{\Fun}{\keyw{fun}}

% Canonical variables for handler components
\newcommand{\vhret}{h^{\mret}}
\newcommand{\vhops}{h^{\mops}}
\newcommand{\sv}{\chi}
\newcommand{\svhret}{\sv^{\mret}}
\newcommand{\svhops}{\sv^{\mops}}

% \newcommand{\dk}{\dRecord{fs,\dRecord{\vhret,\vhops}}}
\newcommand{\dk}{k}

%
\renewcommand{\hid}{V_{\mops}}
\newcommand{\kid}{V_\mathrm{id}}
\newcommand{\rid}{V_{\mret}}

% Examples
\newcommand{\Pipe}{\dec{pipe}}
\newcommand{\Copipe}{\dec{copipe}}
\newcommand{\Ones}{\dec{ones}}
\newcommand{\Yield}{\dec{Yield}}
\newcommand{\Await}{\dec{Await}}
\newcommand{\AddTwo}{\ensuremath{\dec{add}_2}}
\newcommand{\Option}{\dec{Option}}
\newcommand{\Some}{\dec{Some}}
\newcommand{\None}{\dec{None}}
\newcommand{\Toss}{\dec{Toss}}
\newcommand{\toss}{\dec{toss}}
\newcommand{\Heads}{\dec{Heads}}
\newcommand{\Tails}{\dec{Tails}}
\newcommand{\Exn}{\dec{Exn}}
\newcommand{\fail}{\dec{fail}}
\newcommand{\optionalise}{\dec{optionalise}}
\newcommand{\bind}{\ensuremath{\gg\!=}}
\newcommand{\return}{\dec{Return}}
\newcommand{\faild}{\dec{withDefault}}
\newcommand{\Free}{\dec{Free}}
\newcommand{\FreeState}{\dec{FreeState}}
\newcommand{\OpF}{\dec{Op}}
\newcommand{\DoF}{\dec{do}}
\newcommand{\getF}{\dec{get}}
\newcommand{\putF}{\dec{put}}
\newcommand{\fmap}{\dec{fmap}}
\newcommand{\toggle}{\dec{toggle}}
\newcommand{\incrEven}{\dec{incrEven}}
\newcommand{\even}{\dec{even}}

% Abstract machine
\newcommand{\cek}[1]{\ensuremath{\langle #1 \rangle}}
% Environments
\newcommand{\env}{\ensuremath{\gamma}}
% restrict an environment
\newcommand{\res}{\backslash}

% abstract machine translations
\newcommand{\val}[2]{\llbracket #1 \rrbracket #2}
\newcommand{\inv}[1]{\llparenthesis #1 \rrparenthesis}

% configurations
\newcommand{\conf}{\mathcal{C}}

% effect sugar
\newcommand{\inward}[1]{\mathcal{I}\sembr{#1}}
\newcommand{\outward}[1]{\mathcal{O}\sembr{#1}}
\newcommand{\xcomp}[1]{\outward{#1}}
\newcommand{\xval}[1]{\outward{#1}}
\newcommand{\xpre}[1]{\outward{#1}}
\newcommand{\xrow}[1]{\outward{#1}}
\newcommand{\xeff}[1]{\outward{#1}}
\newcommand{\pcomp}[1]{\inward{#1}}
\newcommand{\pval}[1]{\inward{#1}}
\newcommand{\ppre}[1]{\inward{#1}}
\newcommand{\prow}[1]{\inward{#1}}
\newcommand{\peff}[1]{\inward{#1}}
\newcommand{\eamb}{\ensuremath{E_{\mathsf{amb}}}}
\newcommand{\trval}[1]{\mathcal{T}\sembr{#1}}

% UNIX example
\newcommand{\UNIX}{UNIX}
\newcommand{\OSname}[0]{Tiny UNIX}
\newcommand{\exit}{\dec{exit}}
\newcommand{\Exit}{\dec{Exit}}
\newcommand{\Status}{\dec{Status}}
\newcommand{\status}{\dec{status}}
\newcommand{\basicIO}{\dec{basicIO}}
\newcommand{\Putc}{\dec{Putc}}
\newcommand{\putc}{\dec{putc}}
\newcommand{\UFile}{\dec{File}}
\newcommand{\UFD}{\dec{FileDescr}}
\newcommand{\fwrite}{\dec{fwrite}}
\newcommand{\iter}{\dec{iter}}
\newcommand{\map}{\dec{map}}
\newcommand{\stdout}{\dec{stdout}}
\newcommand{\IO}{\dec{IO}}
\newcommand{\BIO}{\dec{BIO}}
\newcommand{\Alice}{\dec{Alice}}
\newcommand{\Bob}{\dec{Bob}}
\newcommand{\Root}{\dec{Root}}
\newcommand{\User}{\dec{User}}
\newcommand{\environment}{\dec{env}}
\newcommand{\EnvE}{\dec{Session}}
\newcommand{\Ask}{\dec{Ask}}
\newcommand{\whoami}{\dec{whoami}}
\newcommand{\Su}{\dec{Su}}
\newcommand{\su}{\dec{su}}
\newcommand{\sessionmgr}{\dec{sessionmgr}}
\newcommand{\echo}{\dec{echo}}
\newcommand{\strlit}[1]{\texttt{"#1"}}
\newcommand{\nondet}{\dec{nondet}}
\newcommand{\Fork}{\dec{Fork}}
\newcommand{\fork}{\dec{fork}}
\newcommand{\Interrupt}{\dec{Interrupt}}
\newcommand{\interrupt}{\dec{interrupt}}
\newcommand{\Pstate}{\dec{Pstate}}
\newcommand{\Done}{\dec{Done}}
\newcommand{\Suspended}{\dec{Paused}}
\newcommand{\slice}{\dec{slice}}
\newcommand{\reifyP}{\dec{reifyProcess}}
\newcommand{\timeshare}{\dec{timeshare}}
\newcommand{\runNext}{\dec{runNext}}
\newcommand{\concatMap}{\dec{concatMap}}
\newcommand{\State}{\dec{State}}
\newcommand{\runState}{\dec{runState}}
\newcommand{\Uget}{\dec{get}}
\newcommand{\Uput}{\dec{put}}
\newcommand{\nl}{\textbackslash{}n}
\newcommand{\quoteRitchie}{\dec{ritchie}}
\newcommand{\quoteHamlet}{\dec{hamlet}}
\newcommand{\Proc}{\dec{Proc}}
\newcommand{\schedule}{\dec{schedule}}
\newcommand{\fsname}{BSFS}
\newcommand{\FileSystem}{\dec{FileSystem}}
\newcommand{\Directory}{\dec{Directory}}
\newcommand{\DataRegion}{\dec{DataRegion}}
\newcommand{\INode}{\dec{INode}}
\newcommand{\IList}{\dec{IList}}
\newcommand{\fileRW}{\dec{fileRW}}
\newcommand{\fileAlloc}{\dec{fileCO}}
\newcommand{\URead}{\dec{Read}}
\newcommand{\UWrite}{\dec{Write}}
\newcommand{\UCreate}{\dec{Create}}
\newcommand{\UOpen}{\dec{Open}}
\newcommand{\fread}{\dec{fread}}
\newcommand{\fcreate}{\dec{fcreate}}
\newcommand{\Ucreate}{\dec{create}}
\newcommand{\redirect}{\texttt{>}}
\newcommand{\fopen}{\dec{fopen}}
\newcommand{\lookup}{\dec{lookup}}
\newcommand{\modify}{\dec{modify}}
\newcommand{\fileIO}{\dec{fileIO}}
\newcommand{\ULink}{\dec{Link}}
\newcommand{\UUnlink}{\dec{Unlink}}
\newcommand{\flink}{\dec{flink}}
\newcommand{\funlink}{\dec{funlink}}
\newcommand{\remove}{\dec{remove}}
\newcommand{\FileLU}{\dec{FileLU}}
\newcommand{\fileLU}{\dec{fileLU}}
\newcommand{\FileIO}{\dec{FileIO}}
\newcommand{\FileRW}{\dec{FileRW}}
\newcommand{\FileCO}{\dec{FileCO}}
\newcommand{\cat}{\dec{cat}}
\newcommand{\head}{\dec{head}}
\newcommand{\grep}{\dec{grep}}
\newcommand{\match}{\dec{match}}
\newcommand{\wc}{\dec{wc}}
\newcommand{\forever}{\dec{forever}}
\newcommand{\textnil}{\textbackslash{}0}
\newcommand{\charlit}[1]{\texttt{'#1'}}
\newcommand{\where}{\keyw{where}}
\newcommand{\intToString}{\dec{intToString}}
\newcommand{\freq}{\dec{freq}}
\newcommand{\paste}{\dec{paste}}
\newcommand{\sed}{\dec{sed}}
\newcommand{\printTable}{\dec{renderTable}}
\newcommand{\timesharee}{\dec{timeshare2}}
\newcommand{\Co}{\dec{Co}}
\newcommand{\UFork}{\dec{UFork}}
\newcommand{\ufork}{\dec{ufork}}
\newcommand{\Wait}{\dec{Wait}}
\newcommand{\scheduler}{\dec{scheduler}}
\newcommand{\Sstate}{\dec{Sstate}}
\newcommand{\Ready}{\dec{Ready}}
\newcommand{\Blocked}{\dec{Blocked}}
\newcommand{\init}{\dec{init}}
\newcommand{\Reader}{\dec{Reader}}
\newcommand{\Other}{\dec{Other}}

%%
%% Some control operators
%%
\newcommand{\Cupto}{\keyw{cupto}}
\newcommand{\Set}{\keyw{set}}
\newcommand{\newPrompt}{\keyw{newPrompt}}
\newcommand{\Callcc}{\keyw{callcc}}
\newcommand{\Callcomc}{\ensuremath{\keyw{callcomp}}}
\newcommand{\textCallcomc}{callcomp}
\newcommand{\Throw}{\keyw{throw}}
\newcommand{\Continue}{\keyw{resume}}
\newcommand{\Catch}{\keyw{catch}}
\newcommand{\Catchcont}{\keyw{catchcont}}
\newcommand{\Control}{\keyw{control}}
\newcommand{\Prompt}{\#}
\newcommand{\Controlz}{\ensuremath{\keyw{control_0}}}
\newcommand{\Spawn}{\keyw{spawn}}
\newcommand{\Promptz}{\ensuremath{\#_0}}
\newcommand{\Escape}{\keyw{escape}}
\newcommand{\shift}{\keyw{shift}}
\newcommand{\shiftz}{\ensuremath{\keyw{shift_0}}}
\newcommand{\CCpp}{\ensuremath{+\CC+}}
\newcommand{\CCpm}{\ensuremath{+\CC-}}
\newcommand{\CCmp}{\ensuremath{-\CC+}}
\newcommand{\CCmm}{\ensuremath{-\CC-}}
\def\sigh#1{%
\pmb{\left\langle\vphantom{#1}\right.}%
#1%
\pmb{\left.\vphantom{#1}\right\rangle}}
\newcommand{\llambda}{\ensuremath{\pmb{\lambda}}}
\newcommand{\reset}[1]{\pmb{\langle} #1 \pmb{\rangle}}
\newcommand{\resetz}[1]{\pmb{\langle} #1 \pmb{\rangle}_0}
\newcommand{\dollarz}[2]{\ensuremath{\reset{#2 \mid #1}}}
\newcommand{\dollarzh}[2]{\ensuremath{#1\,\$_0#2}}
\newcommand{\fcontrol}{\keyw{fcontrol}}
\newcommand{\fprompt}{\%}
\newcommand{\splitter}{\keyw{splitter}}
\newcommand{\abort}{\keyw{abort}}
\newcommand{\calldc}{\keyw{calldc}}
\newcommand{\J}{\keyw{J}}
\newcommand{\JI}{\keyw{J}\,\keyw{I}}
\newcommand{\FelleisenC}{\ensuremath{\keyw{C}}}
\newcommand{\FelleisenF}{\ensuremath{\keyw{F}}}
\newcommand{\cont}{\keyw{cont}}
\newcommand{\Cont}{\dec{Cont}}
\newcommand{\Algol}{Algol~60}
\newcommand{\qq}[1]{\ensuremath{\ulcorner #1 \urcorner}}
\newcommand{\prompttype}{\dec{Prompt}}
\newcommand{\async}{\keyw{async}}
\newcommand{\await}{\keyw{await}}

% Language macros
\newcommand{\Frank}{Frank}
\newcommand{\SML}{SML}
\newcommand{\SMLNJ}{\SML{}/NJ}
\newcommand{\OCaml}{OCaml}


%%
%% Asymptotic improvement macros
%%
\newcommand{\LLL}{\ensuremath{\mathcal L}}
\newcommand{\naive}{naïve\xspace}
\newcommand{\naively}{naïvely\xspace}
\newcommand{\Naive}{Naïve\xspace}
\newcommand{\sem}[1]{\ensuremath{\pi_{#1}}}
\newcommand{\Iff}{\Leftrightarrow}
\newcommand{\Implies}{\Rightarrow}
\newcommand{\BCalcS}{\ensuremath{\lambda_{\textrm{\normalfont s}}\xspace}}
\newcommand{\BCalcE}{\ensuremath{\lambda_{\textrm{\normalfont e}}\xspace}}
\newcommand{\BCalcSE}{\ensuremath{\lambda_{\textrm{\normalfont se}}\xspace}}
\newcommand{\BSPCF}{\ensuremath{\lambda^\rightarrow_{\textrm{\normalfont s}}\xspace}}
\newcommand{\BEPCF}{\ensuremath{\lambda^\rightarrow_{\textrm{\normalfont e}}\xspace}}
\newcommand{\BSEPCF}{\ensuremath{\lambda^\rightarrow_{\textrm{\normalfont se}}\xspace}}
\newcommand{\IfZero}{\keyw{ifzero}}
\newcommand{\Superpoint}{\lambda\_.\Do\;\Branch~\Unit}
\newcommand{\ECount}{\dec{effcount}}
\newcommand{\Countprog}{K}
\newcommand{\Plus}{\mathsf{Plus}}
\newcommand{\Minus}{\mathsf{Minus}}
\newcommand{\Eq}{\mathsf{Eq}}
\newcommand{\BList}{\mathbb{B}^\ast}

\newcommand{\CtxCat}{\CatName{Ctx}}
\newcommand{\PureCont}{\mathsf{PureCont}}

\newcommand{\Addr}{\mathsf{Addr}}
\newcommand{\Lab}{\mathsf{Lab}}
\newcommand{\Env}{\mathsf{Env}}

\newcommand{\Time}{\dec{DTIME}}
\newcommand{\query}{\mathord{?}}
\newcommand{\ans}{\mathord{!}}
\newcommand{\labs}{\mathsf{labs}}
\newcommand{\steps}{\mathsf{steps}}

\newcommand{\tree}{\tau}
\newcommand{\tl}{\labs(\tree)}
\newcommand{\ts}{\steps(\tree)}
\newcommand{\T}[1]{\ensuremath{\mathcal{T}_{#1}}}
\newcommand{\Config}{\dec{Config}}
\newcommand{\cekl}{\langle}
\newcommand{\cekr}{\rangle}

\newcommand{\const}[1]{\ulcorner #1 \urcorner}
\newcommand{\HC}{\ensuremath{\mathcal{H}}}

\newcommand{\tr}{\mathcal{T}}
\newcommand{\tru}{\mathcal{U}}
\newcommand{\Tree}{\dec{Tree}}
\newcommand{\TimedTree}{\dec{TimedTree}}
\newcommand{\denotep}[1]{\ensuremath{\mathbb{P}\llbracket #1 \rrbracket}}

\newcommand\ttTwoTree{
\begin{tikzpicture}[->,>=stealth',level/.style={sibling distance = 4cm/##1,
  level distance = 2.0cm}]
\node (root) [opnode] {Branch}
  child { node [opnode] {Branch}
    child { node [leaf] {$\True$}
      edge from parent node[above left] {$\True$}
    }
    child { node [leaf] {$\True$}
      edge from parent node[above right] {$\False$}
    }
    edge from parent node[above left] {$\True$}
  }
  child { node [opnode] {Branch}
    child { node [leaf] {$\True$}
      edge from parent node[above left] {$\True$}
    }
    child { node [leaf] {$\True$}
      edge from parent node[above right] {$\False$}
    }
    edge from parent node[above right] {$\False$}
  }
;
\end{tikzpicture}}


\newcommand{\tossTree}{
  \begin{tikzpicture}[->,>=stealth',level/.style={sibling distance = 2.5cm/##1,
      level distance = 1.0cm}]
\node (root) [opnode] {$\dec{Branch}$}
  child { node [leaf] {$\dec{Heads}$}
    edge from parent node[above left] {$\True$}
  }
  child { node [leaf] {$\dec{Tails}$}
    edge from parent node[above right] {$\False$}
  }
;
\end{tikzpicture}}

\newenvironment{twoeqs}{\ba[t]{@{}r@{~}c@{~}l@{~}c@{~}r@{~}c@{~}l@{}}}{\ea}

\newcommand{\compTreeEx}{
  \begin{tikzpicture}[->,>=stealth',level/.style={sibling distance = 2.0cm/##1,
      level distance = 2.0cm}]
\node (root) [opnode] {$\getF$}
    child { node [yshift=15] {$\dots$}
    edge from parent {}
    }
    child { node [opnode] {$\putF$}
      child { node {$\True$}
         edge from parent node[left] {$\Unit$}
      }
    edge from parent node[yshift=5,left] {$-2$}
    }
    child { node [opnode] {$\putF$}
      child { node {$\False$}
         edge from parent node[left] {$\Unit$}
      }
    edge from parent node[yshift=2,left] {$-1$}
    }
    child { node [opnode] {$\putF$}
      child { node {$\True$}
         edge from parent node[left] {$\Unit$}
      }
    edge from parent node[left] {$0$}
    }
    child { node [opnode] {$\putF$}
      child { node {$\False$}
         edge from parent node[right] {$\Unit$}
      }
    edge from parent node[yshift=2,right] {$1$}
    }
    child { node [opnode] {$\putF$}
      child { node {$\True$}
         edge from parent node[right] {$\Unit$}
      }
    edge from parent node[yshift=5,right] {$2$}
    }
    child { node [yshift=15] {$\dots$}
    edge from parent {}
    }
;
\end{tikzpicture}}

\newcommand{\smath}[1]{\ensuremath{{\scriptstyle #1}}}

\newcommand{\InfiniteModel}{%
\begin{tikzpicture}[->,>=stealth',level/.style={sibling distance = 3.0cm/##1,
    level distance = 1.0cm}]
\node (root) [draw=none] { }
  child { node [opnode] {$\smath{\query 0}$}
    child { node [opnode] {$\smath{\query 0}$}
      child { node [draw=none,rotate=165] {$\vdots$}
        edge from parent node { }
      }
      child { node[leaf] {$\smath{\ans\False}$}
        edge from parent node { }
      }
      edge from parent node { }
    }
    child { node [leaf] {$\smath{\ans\False}$}
      edge from parent node { }
    }
    edge from parent node { }
  }
;
\end{tikzpicture}}
%
\newcommand{\ShortConjModel}{%
\begin{tikzpicture}[->,>=stealth',level/.style={sibling distance = 3.5cm/##1,
    level distance = 1.0cm}]
\node (root) [draw=none] { }
  child { node [opnode] {$\smath{\query 0}$}
    child { node [opnode] {$\smath{\query 0}$}
      child { node [treenode] {$\smath{\ans\True}$}
        edge from parent node { }
      }
      child { node[treenode] {$\smath{\ans\False}$}
        edge from parent node { }
      }
      edge from parent node { }
    }
    child { node [treenode] {$\smath{\ans\False}$}
      edge from parent node { }
    }
    edge from parent node { }
  }
;
\end{tikzpicture}}
%

\newcommand{\TTTwoModel}{%
\begin{tikzpicture}[->,>=stealth',level/.style={sibling distance = 8cm/##1,
    level distance = 1.5cm}]
\node (root) [draw=none] { }
  child { node [opnode] {$\smath{\query 0}$}
    child { node [opnode] {$\smath{\query 1}$}
      child { node [leaf] {$\smath{\ans\True}$}
        edge from parent node { }
      }
      child { node[leaf] {$\smath{\ans\True}$}
        edge from parent node { }
      }
      edge from parent node { }
    }
    child { node [opnode] {$\smath{\query 1}$}
      child { node [leaf] {$\smath{\ans\True}$}
        edge from parent node { }
      }
      child { node[leaf] {$\smath{\ans\True}$}
        edge from parent node { }
      }
      edge from parent node { }
    }
    edge from parent node { }
  }
;
\end{tikzpicture}}
%
\newcommand{\XORTwoModel}{%
\begin{tikzpicture}[->,>=stealth',level/.style={sibling distance = 5.5cm/##1,
    level distance = 1cm}]
\node (root) [draw=none] { }
  child { node [opnode] {$\smath{\query 0}$}
    child { node [opnode] {$\smath{\query 1}$}
      child { node [treenode] {$\smath{\ans\False}$}
        edge from parent node { }
      }
      child { node[treenode] {$\smath{\ans\True}$}
        edge from parent node { }
      }
      edge from parent node { }
    }
    child { node [opnode] {$\smath{\query 1}$}
      child { node [treenode] {$\smath{\ans\True}$}
        edge from parent node { }
      }
      child { node[treenode] {$\smath{\ans\False}$}
        edge from parent node { }
      }
      edge from parent node { }
    }
    edge from parent node { }
  }
;
\end{tikzpicture}}
%
\newcommand{\SXORTwoModel}{%
\begin{tikzpicture}[->,>=stealth',level/.style={sibling distance = 2.5cm/##1,
    level distance = 1cm}]
\node (root) [opnode] {$\smath{\query 0}$}
    child { node [opnode] {$\smath{\query 1}$}
      child { node [treenode] {$\smath{\ans\False}$}
        edge from parent node { }
      }
      child { node[treenode] {$\smath{\ans\True}$}
        edge from parent node { }
      }
      edge from parent node { }
    }
    child { node [opnode] {$\smath{\query 1}$}
      child { node [treenode] {$\smath{\ans\True}$}
        edge from parent node { }
      }
      child { node[treenode] {$\smath{\ans\False}$}
        edge from parent node { }
      }
      edge from parent node { }
    }
;
\end{tikzpicture}}
%
\newcommand{\TTZeroModel}{%
  \begin{tikzpicture}[->,>=stealth',level/.style={sibling distance = 1cm/##1,
    level distance = 1cm}]
  \node (root) [draw=none] { }
  child { node [treenode] {$\smath{\ans\True}$}
    edge from parent node { }
  }
;
\end{tikzpicture}}%