K3-Reference.sty

\usepackage{ifthen}
\usepackage{todonotes}

\setlength{\marginparwidth}{4.1cm}

\definecolor{shyam}{HTML}{F50CAB}
\newcommand{\sn}[2]{\todo[caption=#1,size=\small,color=shyam!50]{#2}}

% Translation Contexts.
\newcommand{\intI}[1]{\llbracket\,#1\,\rrbracket_I}

\newcommand{\intC}[2]{\llbracket\,#2\,\rrbracket_{C}^{#1}}
\newcommand{\intE}[2]{\llbracket\,#2\,\rrbracket_{E}^{#1}}
\newcommand{\intV}[2]{\llbracket\,#2\,\rrbracket_{V}^{#1}}

\newcommand{\intCI}[1]{\llbracket\,#1\,\rrbracket_{C}^{I}}
\newcommand{\intEI}[1]{\llbracket\,#1\,\rrbracket_{E}^{I}}
\newcommand{\intVI}[1]{\llbracket\,#1\,\rrbracket_{V}^{I}}
\newcommand{\intCD}[1]{\llbracket\,#1\,\rrbracket_{C}^{\delta}}
\newcommand{\intED}[1]{\llbracket\,#1\,\rrbracket_{E}^{\delta}}

\newcommand{\eqI}[3]{\intI{#1} &\longrightarrow #2 \ifthenelse{\equal{#3}{}}{}{\\\notag& \text{#3}}}
\newcommand{\eqC}[3]{\intC{#1} &\longrightarrow #2 \ifthenelse{\equal{#3}{}}{}{\\\notag& \text{#3}}}

\newcommand{\with}{\Big/}

% General-purpose token macro.
\newcommand{\tk}[1]{\ensuremath{\mathinner{\texttt{#1}}}}

% Grammar-Terminal definition macro.
\newcommand{\defgt}[2][]{%
    \ifthenelse{\equal{#1}{}}{\defgt[#2]{#2}}{%
        \expandafter\newcommand\expandafter{\csname gt#2\endcsname}{\mathinner{\texttt{#1}}}%
    }%
}

% Grammar Terminals


% Punctuation
\defgt[(]{LP}
\defgt[)]{RP}
\defgt[\texttt{\char`\{}]{LB}
\defgt[\texttt{\char`\}}]{RB}
\defgt[,]{Comma}
\defgt[.]{Dot}
\defgt[;]{Semi}
\defgt[:]{Colon}
\defgt[<]{LA}
\defgt[>]{RA}
\defgt[@]{At}
\defgt[?]{Qt}
\defgt[*]{Star}
\defgt[\&]{Amp}
\defgt["]{DQuote}
\defgt[']{SQuote}

% Operators
\defgt[+]{Plus}
\defgt[-]{Minus}
\defgt[*]{Times}
\defgt[/]{DividedBy}
\defgt[==]{Eq}
\defgt[!=]{Neq}
\defgt[<]{LT}
\defgt[>]{GT}
\defgt[<=]{LE}
\defgt[>=]{GE}
\defgt[++]{Concat}
\defgt[=]{Assign}
\defgt[=]{Is}
\defgt[->]{Arrow}

% Keywords
\defgt[let]{Let}
\defgt[in]{In}

\defgt[Some]{Some}
\defgt[None]{None}

\defgt[if]{If}
\defgt[then]{Then}
\defgt[else]{Else}

\defgt[ind]{Ind}

\defgt[immut]{Immut}
\defgt[mut]{Mut}

\defgt[case]{Case}
\defgt[of]{Of}

\defgt[bind]{Bind}
\defgt[as]{As}

\defgt[trigger]{Trigger}
\defgt[declare]{Declare}
\defgt[annotation]{Annotation}
\defgt[provides]{Provides}
\defgt[requires]{Requires}
\defgt[lifted]{Lifted}
\defgt[given]{Given}
\defgt[type]{Type}

\defgt[collection]{Collection}
\defgt[named]{Named}

% Types
\defgt[bool]{Bool}
\defgt[byte]{Byte}
\defgt[double]{Double}
\defgt[int]{Int}
\defgt[real]{Real}
\defgt[string]{String}

\defgt[return]{Return}
\defgt[null]{Null}

\defgt[composite]{Composite}

\defgt[new]{New}

\newcommand{\ccall}[3]{%
    \ensuremath{\texttt{#1}\ifthenelse{\equal{#2}{}}{}{\texttt{<}#2\texttt{>}}\texttt{(}#3\texttt{)}}
}

\newcommand{\rw}[1]{\vdash_{#1}}
\newcommand{\rwI}{\rw{I}}
\newcommand{\rwD}{\rw{\delta}}

% Function definition macros
\newcommand{\ConstructComposite}[1]{\textsc{Construct-Composite}(\ensuremath{\mathit{#1}})}
\newcommand{\ConstructRecord}[1]{\textsc{Construct-Record}(\ensuremath{\mathit{#1}})}
\newcommand{\Fresh}[1]{\textsc{Fresh($#1$)}}
\newcommand{\Decl}[3]{\Omega_{#1} \; #2 \ifthenelse{\equal{#3}{}}{}{\gtAssign #3}}