refined core

1 files changed, 196 insertions, 0 deletions

diff --git a/cmds.tex b/cmds.tex
new file mode 100644
index 0000000..b7f3534
--- /dev/null
+++ b/cmds.tex
@@ -0,0 +1,196 @@
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%							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}}}