CBS-LaTeX

% cbs-latex.sty

\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{cbs-latex}[2021/08/27 CBS-LaTeX package]

% This package uses sans-serif fonts for names in specifications.
% For global sans-serif fonts, use together with the cmbright package.

\RequirePackage{amsmath}
\RequirePackage{amssymb}
\RequirePackage{stmaryrd}
\RequirePackage{textcomp}
\RequirePackage[svgnames]{xcolor}
\RequirePackage{imakeid}
\RequirePackage{hyperref}
% \hypersetup{filebordercolor={White}}

% The following color names are used by the highlighting macros.
% They are set to colors defined by the svgnames option of xcolor,
% and can be reset locally in LaTeX documents.

\colorlet{Key}{Gray}
\colorlet{Name}{DarkRed}
\colorlet{SyntaxName}{DarkGreen}
\colorlet{SemanticsName}{DarkBlue}
\colorlet{PartVariable}{Black}
\colorlet{SectionNumber}{Black}
\colorlet{Language}{Black}

% The following definition of \SHADE{TEXT} produces a faint grey background
% for CBS notation in running text:
\newcommand{\SHADE}[1]{ {\setlength{\fboxsep}{0pt}\colorbox{gray!10}{$\strut#1\strut$}}}

% \KEY{text}, \STRING{text}, \ATOM{text}, \LEX{text} can be used in text or math mode.

\newcommand{\KEY}[1]{\textsf{\textsl{\STYLE{Key}{#1}}}}
\newcommand{\STRING}[1]{\textsf{``\texttt{#1}''}}
\newcommand{\ATOM}[1]{\textsf{`\texttt{#1}'}}
\newcommand{\LEX}[1]{\textsf{\STYLE{Key}{`}\texttt{#1}\STYLE{Key}{'}}}

% The following commands produce ASCII characters that are treated specially by LaTeX.

\newcommand{\HASH}{\char`\#}
\newcommand{\DOLLAR}{\char`\$}
\newcommand{\PERCENT}{\char`\%}
\newcommand{\AMPERSAND}{\char`\&}
\newcommand{\APOSTROPHE}{\char`\'}
\newcommand{\BACKSLASH}{\char`\\}
\newcommand{\CARET}{\char`\^}
\newcommand{\UNDERSCORE}{\char`\_}
\newcommand{\GRAVE}{\`{}}
\newcommand{\LEFTBRACE}{\char`\{}
\newcommand{\RIGHTBRACE}{\char`\}}
\newcommand{\TILDE}{\char`\~}

% \FUN{name} highlights the name.
% \FUNDEC{name} declares Name.name as the target of links to name.
% \FUNREF{name} links name to the target Name.name in the current file.
% \FUNHYP{url}{file}{name} links name to Name.name at url/file/file.pdf.
% Similarly for \VAR, \SYN, \SEM, and \SECT.

\newcommand{\SUB}[1]{_{\text{#1}}}

% PLAIN

\newcommand{\STYLE}[2]{\textcolor{#1}{#2}}

\newcommand{\VAR}[1]{\STYLE{PartVariable}{\textsl{#1\/}}}
\newcommand{\FUN}[1]{\STYLE{Name}{\textsf{#1}}}
\newcommand{\SYN}[1]{\STYLE{SyntaxName}{\textsf{#1}}}
\newcommand{\SEM}[1]{\STYLE{SemanticsName}{\textsf{#1}}}
\newcommand{\SECT}[1]{\STYLE{SectionNumber}{#1}}
\newcommand{\LANG}[1]{\STYLE{Language}{#1}}

% DEC

\newcommand{\DEC}[3]{\raisebox{1.2\ht\strutbox}{\hyperdef{#1}{#2}{}}#3}

\newcommand{\VARDEC}[1]{\DEC{PartVariable}{#1}{\VAR{#1}}}
\newcommand{\FUNDEC}[1]{\DEC{Name}{#1}{\FUN{#1}}}
\newcommand{\SYNDEC}[1]{\DEC{SyntaxName}{#1}{\SYN{#1}}}
\newcommand{\SEMDEC}[1]{\DEC{SemanticsName}{#1}{\SEM{#1}}}
\newcommand{\SECTDEC}[1]{\DEC{SectionNumber}{#1}{\SECT{#1}}}
% \newcommand{\LANGDEC}[1]{\DEC{Language}{#1}{\LANG{#1}}}

% REF

\newcommand{\REF}[3]{\hyperref{\jobname.pdf}{#1}{#2}{#3}}

\newcommand{\VARREF}[1]{\REF{PartVariable}{#1}{\VAR{#1}}}
\newcommand{\FUNREF}[1]{\REF{Name}{#1}{\FUN{#1}}}
\newcommand{\SYNREF}[1]{\REF{SyntaxName}{#1}{\SYN{#1}}}
\newcommand{\SEMREF}[1]{\REF{SemanticsName}{#1}{\SEM{#1}}}
\newcommand{\SECTREF}[1]{\REF{SectionNumber}{#1}{\SECT{#1}}}
% \newcommand{\LANGREF}[1]{\REF{Language}{#1}{\LANG{#1}}}

% HYP

\newcommand{\HYP}[5]{\hyperref{#1/#2/#2.pdf}{#3}{#4}{#5}}

\newcommand{\VARHYP}[3]{\HYP{#1}{#2}{PartVariable}{#3}{\VAR{#3}}}
\newcommand{\FUNHYP}[3]{\HYP{#1}{#2}{Name}{#3}{\FUN{#3}}}
\newcommand{\SYNHYP}[3]{\HYP{#1}{#2}{SyntaxName}{#3}{\SYN{#3}}}
\newcommand{\SEMHYP}[3]{\HYP{#1}{#2}{SemanticsName}{#3}{\SEM{#3}}}
\newcommand{\SECTHYP}[3]{\HYP{#1}{#2}{SectionNumber}{#3}{\SECT{#3}}}
% \newcommand{\LANGHYP}[3]{\HYP{#1}{#2}{Language}{#3}{\LANG{#3}}}

% CBS-beta/math hyperlinks

\newcommand{\CBSBETA}{https://plancomps.github.io/CBS-beta/math}

\newcommand{\VARCBS}[3]{\VARHYP{\CBSBETA/#1}{#2}{#3}}
\newcommand{\FUNCBS}[3]{\FUNHYP{\CBSBETA/#1}{#2}{#3}}
\newcommand{\SYNCBS}[3]{\SYNHYP{\CBSBETA/#1}{#2}{#3}}
\newcommand{\SEMCBS}[3]{\SEMHYP{\CBSBETA/#1}{#2}{#3}}
\newcommand{\SECTCBS}[3]{\SECTHYP{\CBSBETA/#1}{#2}{#3}}
% \newcommand{\LANGCBS}[3]{\LANGHYP{\CBSBETA/#1}{#2}{#3}}

% \hyperdef and \hyperref support both internal and external hyperlinks
% (whereas \hypertarget and \hyperlink support only internal hyperlinks)
% See https://tex.stackexchange.com/a/197244 regarding the use of \raisebox

% \LEFTPHRASE MATH \RIGHTPHRASE produces [[ MATH ]] with proper brackets:

\newcommand{\LEFTPHRASE}{\llbracket}
\newcommand{\RIGHTPHRASE}{\rrbracket}

% \LEFTGROUP MATH \RIGHTGROUP produces ( MATH ) where the parentheses are
% highlighted the same  as keywords:

\newcommand{\LEFTGROUP}{\STYLE{Key}{(}}
\newcommand{\RIGHTGROUP}{\STYLE{Key}{)}}

% MATH\PLUS produces a superscript +
% MATH\STAR produces a superscript *
% MATH\QUERY produces a superscript ?

\newcommand{\PLUS}{ {}^{\text{\scriptsize+}}}
\newcommand{\STAR}{ {}^{\raisebox{-0.5ex}{\text{\scriptsize*}}}}
\newcommand{\QUERY}{ {}^{\raisebox{-0.5ex}{\text{\scriptsize?}}}}

% \RULE{premise}{conclusion} produces
%     premise
%   ----------
%   conclusion

\newcommand{\RULE}[2]{\mkern-2.1mu\frac{\displaystyle#1}{\displaystyle#2}}
% See https://tex.stackexchange.com/questions/337328/superscripts-appear-in-various-weird-places-in-fractions

% \RULE
%   {\begin{aligned} & premise \\ & ... \end{aligned}}
%   {\begin{aligned} & conclusion ... \\ & ... \end{aligned}}
% produces an inference rule with left-aligned premises and split conclusion
%      premise
%      ...
%   --------------
%   conclusion ...
%   ...

% \TO TYPE produces => TYPE

\newcommand{\TO}{\mathop{\Rightarrow}}

% TERM \TRANS TERM produces TERM ---> TERM

\newcommand{\TRANS}{\longrightarrow}

% TERM \xrightarrow{LABEL} TERM puts the label above the long arrow