diff options
Diffstat (limited to 'cmds.tex')
| -rw-r--r-- | cmds.tex | 196 |
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}}} |