%\newcommand\pfun{\mathrel{\ooalign{\hfil$\mapstochar\mkern5mu$\hfil\cr$\to$\cr}}}
\newcommand\pfun{\rightharpoonup}
\newcommand{\Sym}{\operatorname{Sym}}

% Semantic sets
\newcommand{\sVar}   {\text{\textsf{Var}}}
\newcommand{\sExp}   {\text{\textsf{Exp}}}
\newcommand{\sHeap}  {\text{\textsf{Heap}}}
\newcommand{\sVal}   {\text{\textsf{Val}}}
\newcommand{\sValue} {\text{\textsf{Value}}}
\newcommand{\sCValue}{\text{\textsf{CValue}}}
\newcommand{\sEnv}   {\text{\textsf{Env}}}
\newcommand{\sCEnv}  {\text{\textsf{CEnv}}}
\newcommand{\sC}     {\text{\textsf{C}}}

\newcommand{\sFn}[1]{\text{\textsf{Fn}}(#1)}
\newcommand{\sFnProj}[2]{#1\,\downarrow_{\text{\textsf{Fn}}}\,#2}
\newcommand{\sB}[1]{\text{\textsf{B}}(#1)}
\newcommand{\sBProj}[3]{#1\,\downarrow_{\text{\textsf{B}}}\!(#2,#3)}
\newcommand{\sCFn}[1]{\text{\textsf{CFn}}\,(#1)}
\newcommand{\sCFnProj}[2]{#1\,\downarrow_{\text{\textsf{CFn}}}\,#2}
\newcommand{\sCB}[1]{\text{\textsf{CB}}(#1)}
\newcommand{\sCBProj}[3]{#1\,\downarrow_{\text{\textsf{CB}}}\!(#2,#3)}

\newcommand{\req}[1]{=_{#1}}

% Syntax
\newcommand{\keyword}[1]{\text{\textsf{\textbf{#1}}}}
\newcommand{\sApp}[2]{#1\;#2}
\newcommand{\sLam}[2]{\text{\textlambda} #1.\, #2}
\newcommand{\sLet}[2]{\keyword{let}~#1~\keyword{in}~#2}

\newcommand{\sITE}[3]{\ensuremath{#1 \mathop{\keyword{?}} #2 \mathop{\keyword{:}} #3}}
\newcommand{\sCon}[1]{\keyword{C}_{#1}}
\newcommand{\bT}{\keyword{t}}
\newcommand{\bF}{\keyword{f}}


% Multi argument application
\DeclareDocumentCommand\sApps{>{\SplitList{ }}m}
{%
  {\ProcessList{#1}{\sAppsItem}}%
}
\newcommand\sAppsItem[1]{#1\let\sAppsItem\sAppsItema}
\newcommand\sAppsItema[1]{\;#1}


% Semantics
\newcommand{\sred}[5]{#1 : #2 \Downarrow_{#3} #4 : #5}
% 'DOWNWARDS TRIPLE ARROW' (U+290B)
\newcommand{\ssred}[4]{#1 : #2 \mathrel{\rotatebox[origin=c]{90}{$\Lleftarrow$}} #3 : #4}
\newcommand{\sRule}[1]{\text{\rmfamily{\textsc{#1}}}}


% smallsetep semantics, stacks
\newcommand{\sest}{\mathrel{\Rightarrow^{}}}
\newcommand{\sests}{\mathrel{\Rightarrow^{\mathclap\ast}}}
\newcommand{\sestsb}{\mathrel{\Rightarrow^{\mathclap\ast}_b}}
\newcommand{\step}[2]{#1 \sest #2}
\newcommand{\steps}[2]{#1 \sests #2}
\newcommand{\fste}{\Rightarrow_\#}
\newcommand{\fstep}[2]{#1 \Rightarrow_\# #2}
\newcommand{\fsteps}[2]{#1 \ensuremath{\Rightarrow_\#^\ast} #2}

\newcommand{\emptystack}{[]}
\newcommand{\cons}[2]{#1{\cdot}#2}
\newcommand{\append}[2]{#1\cdot#2}
\renewcommand{\arg}[1]{\mathsf{\$}#1}
\newcommand{\upd}[1]{\mathsf{\#}#1}
\newcommand{\alts}[2]{(#1\mathop{\keyword{:}}#2)}

% Other functions and styles
\newcommand{\subst}[3]{#1[#2\mathop{\coloneqq}#3]}


\makeatletter
% http://tex.stackexchange.com/a/256205/15107
\newcommand*\IsExactlyOneToken[1]{%
  TT\fi
  \ifx\@empty#1\@empty
    \expandafter\@EmptyCase
  \else
    \expandafter\@IsOnlyOneToken
  \fi
  #1\@@@
}
\@ifdefinable\@IsOnlyOneToken{\def\@IsOnlyOneToken#1#2\@@@{%
  \ifx\@empty#2\@empty
}}
\@ifdefinable\@EmptyCase{\def\@EmptyCase#1\@@@{% #1 for robustness
  \iffalse % since 0 != 1
}}
\makeatother

\DeclareRobustCommand{\parensalways}[1]{
  \ifthenelse{\equal{#1}{}}{}{%
  (#1)%
  }%
}
\DeclareRobustCommand{\parens}[1]{
 \if\IsExactlyOneToken{#1}%
  \,#1%
 \else%
  \ifthenelse{\equal{#1}{}}{}{%
  (#1)%
  }%
 \fi%
}

\newcommand{\sfop}[1]{\mathsf{#1}}
\newcommand{\fv}[1]{\sfop{fv}\parens{#1}}
\newcommand{\isVal}[1]{\sfop{isVal}\parens{#1}}
\newcommand{\dom}[1]{\sfop{dom}\,#1}
\newcommand{\thunks}[1]{\sfop{thunks}\parens{#1}}
\newcommand{\nxt}[2]{\sfop{next}_{#1}\parens{#2}}
\newcommand{\paths}[1]{\sfop{paths}\parens{#1}}
\newcommand{\rec}[1]{\sfop{rec}\parens{#1}}
\newcommand{\topargs}[1]{\sfop{args}\parens{#1}}


\newcommand{\xeng}{x_1 = e_1, \ldots, x_n = e_n}
\newcommand{\xen}{x_1\mapsto e_1, \ldots, x_n\mapsto e_n}

% Longer variables names
\newcommand{\vname}[1]{\text{\textit{#1}}}

% Denotational semantics
\newcommand{\dsem}[2]{\llbracket #1 \rrbracket_{#2}}
\newcommand{\esem}[1]{\{\!\!\{#1\}\!\!\}}
\newcommand{\dsemr}[2]{\mathcal N\!\llbracket #1 \rrbracket_{#2}}
\newcommand{\esemr}[1]{\mathcal N\!\{\!\!\{#1\}\!\!\}}

\newcommand{\addon}[1]{\mathop{++_{#1}}}
\newcommand{\eqon}[1]{\mathrel{\mathord=_{\mathord|_{#1}}}}

\newcommand{\dsim}{\mathrel{\triangleleft\triangleright}}
\newcommand{\dsimheap}{\mathrel{\triangleleft\triangleright^*}}

%\newcommand{\etaeq}[1]{\mathrel{\stackrel{\eta}{=}_{#1}}}
%\newcommand{\etaeqenv}[1]{\mathrel{\stackrel{\bar\eta}{=}_{#1}}}
\newcommand{\etaeq}[1]{\mathrel{\approx_{#1}}}
\newcommand{\etaeqenv}[1]{\mathrel{\approx_{#1}}}

\newcommand{\Crestr}[2]{ #1 |_{#2}}

% Text structuring
\newcommand{\case}[1]{\par\smallskip\noindent\textbf{Case:} #1\nopagebreak\par\noindent\ignorespaces}
\newcommand{\beginright}{&\mathrel{\phantom{=}}}
\newcommand{\aexpl}[1]{&\mathrel{\phantom{=}}\left\{\text{ #1 }\right\}}

% preconditions
\newcommand{\longlineleft}[1]{&\mathrlap{#1}&&&\\}
\newcommand{\precondition}[1]{\longlineleft{#1 \implies}&&}
\newcommand{\shortprecondition}[1]{&\mathrlap{#1 \implies}&}
\newcommand{\noprecondition}{&&}

% Co-call Graphs
\newcommand{\sGraph}{\text{\textsf{Graph}}}
\newcommand{\edge}[2]{#1\text{---}#2}
\newcommand{\neighbors}[2]{N_{#1}\parensalways{#2}}

% Trace trees

\newcommand{\sTTree}{\text{\textsf{TTree}}}

\newcommand{\emptytree}{%
	\begin{tikzpicture}[grow=right, sibling distance=12, level distance=18, every node/.style={inner sep=2pt}, baseline={([yshift=-2.3pt]O)}]
	\coordinate[circle, fill, inner sep=1]
	 (O);
	\end{tikzpicture}%
}
\newcommand{\singletontree}[1]{%
	\begin{tikzpicture}[grow=right, sibling distance=12, level distance=18, every node/.style={inner sep=2pt}, baseline={([yshift=-2.3pt]O)}]
	\coordinate[circle, fill, inner sep=1]
	 (O)
	 child {
	   coordinate
	   edge from parent node[above] {#1}
	 };
	\end{tikzpicture}%
}

% Stuff from the safety chapter; to be sorted
\newcommand{\aexp}[2]{\mathcal A_{#2}\parensalways{#1}}
\newcommand{\aheap}[3]{\mathcal A_{#3}(#1,#2)}
\newcommand{\abinds}[2]{\overline{\mathcal A}_{#2}\parensalways{#1}}
\newcommand{\astack}[2]{\dot{\mathcal A}_{#2}\parensalways{#1}}
\newcommand{\trans}[2]{\mathsf T_{#2}\parensalways{#1}}
\newcommand{\transheap}[2]{\overline{\mathsf T}_{#2}\parensalways{#1}}
\newcommand{\transstack}[2]{\dot{\mathsf T}_{#2}\parensalways{#1}}
\newcommand{\transconf}[2]{\mathsf T_{#2}\parensalways{#1}}
\newcommand{\etaex}[2]{\mathcal E_{#2}\parensalways{#1}}

\newcommand{\prognosis}[2]{\mathcal C_{#2}\parensalways{#1}}
\newcommand{\cheap}[3]{\mathcal C_{#3}(#1,#2)}
\newcommand{\Card}{\mathsf{Card}}
\newcommand{\Co}{\mathbf{1}}
\newcommand{\Cm}{\mathbf{\infty}}

\newcommand{\fexp}[2]{\mathcal T_{#2}\parensalways{#1}}
\newcommand{\fbinds}[2]{\overline{\mathcal T}_{\!\!#2}\parensalways{#1}}
\newcommand{\fheap}[3]{\mathcal T_{#3}\parensalways{#1,#2}}
\newcommand{\fstack}[2]{\dot{\mathcal T}_{#2}\parensalways{#1}}

\newcommand{\ccexp}[2]{\mathcal G_{#2}\parensalways{#1}}
\newcommand{\ccheap}[3]{\mathcal G_{#3}(#1,#2)}
\newcommand{\ccbind}[4]{\mathcal G_{#3;#4}(#1\mapsto #2)}


% Obsolete and/or to sort macros

\newcommand{\letrec}{\sLet{\overline{x_i = e_i}}{e}}
\newcommand{\nonreclet}{\sLet{x = e_1}{e_2}}
\newcommand{\many}[1]{#1^\ast}
\newcommand{\restr}[2]{#1\big|_{#2}}