%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%							COMMANDS						  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%	TODO annotations
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\MP}[1]{\todo[color=blue!30]{MP TODO: #1}}
\newcommand{\MPin}[1]{\todo[color=blue!30,inline]{MP TODO: #1}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%	Math formatting
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% some shortcuts
\newcommand{\mi}[1]{\ensuremath{\mathit{#1}}}
\newcommand{\mr}[1]{\ensuremath{\mathrm{#1}}}
\newcommand{\mt}[1]{\ensuremath{\texttt{#1}}}
\newcommand{\mtt}[1]{\ensuremath{\mathtt{#1}}}
\newcommand{\mf}[1]{\ensuremath{\mathbf{#1}}}
\newcommand{\mk}[1]{\ensuremath{\mathfrak{#1}}}
\newcommand{\mc}[1]{\ensuremath{\mathcal{#1}}}
\newcommand{\ms}[1]{\ensuremath{\mathsf{#1}}}
\newcommand{\mb}[1]{\ensuremath{\mathbb{#1}}}
\newcommand{\msc}[1]{\ensuremath{\mathscr{#1}}}

\DeclareMathOperator\mydefsym{\ensuremath{\iangleq}}
\newcommand{\bnfdef}[0]{\ensuremath{\mathrel{::=}}}
\newcommand{\isdef}[0]{\ensuremath{\mathrel{\overset{\makebox[0pt]{\mbox{\normalfont\tiny\sffamily def}}}{=}}}}

% http://tex.stackexchange.com/questions/5502/how-to-get-a-mid-binary-relation-that-grows
\newcommand{\relmiddle}[1]{\mathrel{}\middle#1\mathrel{}}
\newcommand{\myset}[2]{\ensuremath{\left\{#1 ~\relmiddle|~ #2\right\}}}

\newcommand{\divr}[0]{\ensuremath{\!\!\Uparrow}\xspace}
\newcommand{\term}[0]{\ensuremath{\!\!\Downarrow}\xspace}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%	Compiler 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\genlang}[2]{\ensuremath{\lambda^{#1}_{#2}}}
\newcommand{\genlangF}[2]{\ensuremath{F^{#1}_{#2}}}

\newcommand{\ulc}[0]{\bl{\genlang{u}{}}}
\newcommand{\stlc}[0]{\src{\genlang{\tau}{}}}
\newcommand{\sysf}[0]{\oth{\genlangF{\forall}{}}}

\newcommand{\funname}[1]{\mtt{#1}}
\newcommand{\fun}[2]{\ensuremath{{\bl{\funname{#1}\left(#2\right)}}}\xspace}
\newcommand{\dom}[1]{\fun{dom}{#1}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%	Language shortcuts
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\ctx}[0]{\ensuremath{\mk{C}}}
\newcommand{\ctxh}[1]{\ctx\hole{#1}}
\newcommand{\hole}[1]{\ensuremath{\left[#1\right]}}
\newcommand{\evalctx}[0]{\ensuremath{\mb{E}}}

\newcommand{\srce}[0]{\src{\emptyset}\xspace}
\newcommand{\trge}[0]{\trgb{\emptyset}\xspace}
\newcommand{\come}[0]{\com{\emptyset}\xspace}
\newcommand{\othe}[0]{\oth{\emptyset}\xspace}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%	Language formatting
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\neutcol}[0]{black}
\newcommand{\stlccol}[0]{RoyalBlue}
\newcommand{\ulccol}[0]{RedOrange}
\newcommand{\commoncol}[0]{black}    % CarnationPink
\newcommand{\othercol}[0]{CarnationPink}

\newcommand{\col}[2]{\ensuremath{{\color{#1}{#2}}}}

\newcommand{\src}[1]{\ms{\col{\stlccol}{#1}}}
\newcommand{\trgb}[1]{\ensuremath{\bm{\col{\ulccol }{#1}}}}
\newcommand{\trg}[1]{{\mf{\col{\ulccol }{#1}}}}
\newcommand{\oth}[1]{\mi{\col{\othercol }{#1}}}
% MARCO: \bm is notorious to break things around. it's there only to make bold math letters. we can remove it if necessary.
% it is currently removed -- the paretheses are still there though -- as it did go beyond its scope, i did not know how to remove it (\mr did nont work)
% it was affecting stuff inside the compilation brackets, making source stuff bold ... 
%if we know of a solution, we can add \bm at the beginning here and the bold-removal command in the core of \compgen
\newcommand{\bl}[1]{\col{\neutcol }{#1}}
\newcommand{\com}[1]{\mi{\col{\commoncol }{#1}}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%	Type rules
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcounter{typerule}
\crefname{typerule}{rule}{rules}

\newcommand{\typeruleInt}[5]{%									    % #1 is the title, #2 is the hypotheses. #3 is the thesis, #4 is the label for referencing
	\def\thetyperule{#1}%
	\refstepcounter{typerule}%
	\label{tr:#4}%
  \ensuremath{\begin{array}{c}#5 \inference{#2}{#3}\end{array}} 
}
\newcommand{\typerule}[4]{%									        % #1 is the title, #2 is the hypotheses. #3 is the thesis, #4 is the label for referencing
  \typeruleInt{#1}{#2}{#3}{#4}{\textsf{\scriptsize ({#1})} \\      }
}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%	Contextual equivalence
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\DeclareMathOperator\niff{\ensuremath{\nLeftrightarrow}}
\DeclareMathOperator\nsimeq{\ensuremath{\mathrel{\not\simeq}}}

\DeclareMathOperator\ceq{\ensuremath{\mathrel{\simeq_{\mi{ctx}}}}}
\DeclareMathOperator\nceq{\mathrel{\nsimeq_{\mi{ctx}}}}

\DeclareMathOperator\ceqs{\src{\ceq}}
\DeclareMathOperator\ceqt{\trgb{\ceq}}
\DeclareMathOperator\ceqo{\oth{\ceq}}

\DeclareMathOperator\nceqs{\src{\nceq}}
\DeclareMathOperator\nceqt{\trgb{\nceq}}
\DeclareMathOperator\nceqo{\oth{\nceq}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Missing envs
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\theoremstyle{definition}
\newtheorem{assumption}{Assumption}
\newtheorem{notation}{Notation}
\newtheorem{definition}{Definition}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{property}{Property}
\newtheorem{example}{Example}
\newtheorem{informal}{Informal definition}
\newtheorem{corollary}{Corollary}

\Crefname{corollary}{Corollary}{Corollaries}
\Crefname{informal}{Definition}{Definition}
\Crefname{assumption}{Assumption}{Assumptions}
\crefname{assumption}{Assumption}{Assumptions}
\Crefname{property}{Property}{Properties}
\crefname{property}{Property}{Properties}
\Crefname{lstlisting}{Listing}{Listings}
\Crefname{problem}{Problem}{Problems}
\Crefname{equation}{Rule}{Rules}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Lambda 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\DeclareMathOperator\op{\ensuremath{\oplus}}

\newcommand{\lam}[2]{\ensuremath{\lambda #1\ldotp #2}}
\newcommand{\pair}[1]{\ensuremath{\left\langle#1\right\rangle}}
\newcommand{\projone}[1]{\ensuremath{#1.1}}
\newcommand{\projtwo}[1]{\ensuremath{#1.2}}
\newcommand{\caseof}[3]{\ensuremath{{case}~#1~{of}~\inl{x_1}\mapsto #2\mid\inr{x_2}\mapsto #3}}
\newcommand{\inl}[1]{\ensuremath{{inl}~#1}}
\newcommand{\inr}[1]{\ensuremath{{inr}~#1}}
\newcommand{\fold}[1]{\ensuremath{{fold}_{#1}}}
\newcommand{\unfold}[1]{\ensuremath{{unfold}_{#1}}}
\newcommand{\Lam}[2]{\ensuremath{\Lambda #1\ldotp #2}}
\newcommand{\tapp}[2]{\ensuremath{#1 \hole{#2}}}
\newcommand{\pack}[3]{\ensuremath{{pack}~\pair{#1,#2}~{as}~#3}}
\newcommand{\unpack}[4]{\ensuremath{{unpack}~#1~{as}~\pair{#2,#3}~{in}~#4}}

\newcommand{\type}[3]{\ensuremath{ \left\{#1:#2\relmiddle|#3 \right\}}}

\newcommand{\matgen}[2]{\ensuremath{\mu #1\ldotp#2}}
\newcommand{\mat}[0]{\matgen{\alpha}{\tau}}
\newcommand{\fatgen}[2]{\ensuremath{\forall #1\ldotp#2}}
\newcommand{\fat}[0]{\fatgen{\alpha}{\tau}}
\newcommand{\eatgen}[2]{\ensuremath{\exists #1\ldotp#2}}
\newcommand{\eat}[0]{\eatgen{\alpha}{\tau}}
% \newcommand{\fatgent}[2]{\ensuremath{\trgb{\forall} #1\ldotp#2}}
% \newcommand{\fatt}[0]{\fatgent{\alpt}{\tat}}
% \newcommand{\eatgent}[2]{\ensuremath{\trgb{\exists} #1\ldotp#2}}
% \newcommand{\eatt}[0]{\eatgent{\alpt}{\tat}}

\newcommand{\fail}[0]{\mi{fail}}

\newcommand{\redgen}[1]{\ensuremath{ \hookrightarrow^{#1} }}
\newcommand{\nredgen}[1]{\ensuremath{\not\hookrightarrow^{#1}}}
\DeclareMathOperator\red{\redgen{}}

\newcommand{\nred}[0]{\nredgen{}}
\newcommand{\redstar}[0]{\redgen{*}}

\newcommand{\bigredgen}[1]{\ensuremath{ \Downarrow^{#1} }}
\newcommand{\nbigredgen}[1]{\ensuremath{\not\Downarrow^{#1}}}
\DeclareMathOperator\bigs{\bigredgen{}}

\newcommand{\credgen}[1]{\ensuremath{ \leadsto^{#1} }}
\newcommand{\ncredgen}[1]{\ensuremath{\not\leadsto^{#1}}}
\DeclareMathOperator\cred{\credgen{}}
\DeclareMathOperator\credp{\credgen{p}}

\newcommand{\subst}[2]{\ensuremath{\bl{\left[#1\relmiddle/#2\right]}}} %replace 1 in place of 2
\newcommand{\subs}[2]{\subst{\src{#1}}{\src{#2}}}
\newcommand{\subt}[2]{\subst{\trg{#1}}{\trg{#2}}}
\newcommand{\subo}[2]{\subst{\oth{#1}}{\oth{#2}}}