pl-syntax.sty

\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{pl-syntax}[2024/12/13 1.5.0 PL Syntax Macros]
\DeclareOption{abt}{
    \NewDocumentCommand{\Abt}{}{\A@bt}
    \NewDocumentCommand{\Abs}{}{\A@bs}
    \NewDocumentCommand{\Opn}{}{\O@pn}
    \ProvideDocumentCommand{\kw}{}{\@kw}
    \ProvideDocumentCommand{\sep}{}{\@sep}
    \ProvideDocumentCommand{\empMap}{}{\emp@map}
    \ProvideDocumentCommand{\singMap}{}{\sing@map}
    \ProvideDocumentCommand{\finMap}{}{\fin@map}
    \ProvideDocumentCommand{\extMap}{}{\ext@map}
}
\DeclareOption{sf}{
    \ProvideDocumentCommand{\@kw}{m}{\textsf{#1}}
}
\DeclareOption{sc}{
    \ProvideDocumentCommand{\@kw}{m}{\textsc{#1}}
}
\DeclareOption{pfpl}{
    \ProvideDocumentCommand{\param@bracks}{m}{[#1]}
    \ProvideDocumentCommand{\minor@bracks}{m}{\{#1\}}
    \ProvideDocumentCommand{\major@bracks}{m}{(#1)}
}
\DeclareOption{nosyn}{
    \NewDocumentCommand{\no@syn}{}{}
}
\DeclareOption*{\PackageWarning{pl-syntax}{Unrecognized option `\CurrentOption'.}}
\ProcessOptions\relax

\RequirePackage{xifthen,scalerel,bbm}
\ifdefined\bigplus\else\DeclareMathOperator*{\bigplus}{\scalerel*{+}{\sum}}\fi
\ifdefined\bigtimes\else\DeclareMathOperator*{\bigtimes}{\scalerel*{\times}{\prod}}\fi

\makeatletter

\ProvideDocumentCommand{\param@bracks}{m}{\langle #1\rangle}
\ProvideDocumentCommand{\minor@bracks}{m}{[#1]}
\ProvideDocumentCommand{\major@bracks}{m}{(#1)}
\ProvideDocumentCommand{\@kw}{m}{\texttt{#1}}
\NewDocumentCommand{\@sep}{s}{\IfBooleanTF{#1}{\mathbin}{\mathord}{\@kw{;}}}

\NewDocumentCommand{\emp@map}{}{\emptyset}
\NewDocumentCommand{\sing@map}{m m}{#1\hookrightarrow #2}
\NewDocumentCommand{\fin@map}{m m m}{\sing@map{#2}{#3_#2}\mid #2\in #1}
\NewDocumentCommand{\ext@map}{s m m m}{\IfBooleanF{#1}{#2,\,}\sing@map{#3}{#4}{\IfBooleanT{#1}{\,, #2}}}

% starred for math name, non-starred for verbatim name, optional index
\NewDocumentCommand{\O@pn}{s m}{\mathop{\IfBooleanTF{#1}{#2}{\textnormal{\@kw{#2}}}}\nolimits}
% choose between concrete and abstract operation name
\NewDocumentCommand{\Opn@}{m m m}{\IfBooleanTF{#1}{\O@pn*{#2}}{\O@pn{#3}}}

% abstractor of symbols in <>'s and variables in ()'s in an abs
\NewDocumentCommand{\A@bs}{d<> d() m}{\IfValueT{#1}{#1\mathord{.}}\IfValueT{#2}{#2\mathord{.}} #3}
% abstract binding tree with operator, parameter, minor, and major arguments
% starred form omits the minor arguments, a cheap form of concrete syntax
% omitted minor and major arguments are dropped entirely from output
\ProvideDocumentCommand{\A@bt}{s m d<> o d()}{#2\IfValueT{#3}{\param@bracks{#3}}\IfBooleanTF{#1}{}{\IfValueT{#4}{\minor@bracks{#4}}}\IfValueT{#5}{\major@bracks{#5}}}

% choose starred form of \A@bt according to boolean argument
\NewDocumentCommand{\Abt@}{m m}{\IfBooleanTF{#1}{\A@bt*{#2}}{\A@bt{#2}}}

% pre- or post-fix substitution notation
\ProvideDocumentCommand{\Sub}{s m m m}{\IfBooleanTF{#1}{#4[#2/#3]}{[#2/#3]#4}}
% substitution maps
\ProvideDocumentCommand{\empSub}{}{\emp@map}
\ProvideDocumentCommand{\extSub}{s m m m}{\IfBooleanTF{#1}{\ext@map*{#2}{#3}{#4}}{\ext@map{#2}{#3}{#4}}}
% apply a substitution to an abt, \gamma^\ast(a), or \hat{\gamma}(a)
\ProvideDocumentCommand{\appSub}{s m}{\IfBooleanTF{#1}{{#2}^{\ast}}{\widehat{#2}}}

\ifdefined\no@syn\else

%%% consecutive optional arguments are problematic, because when one is omitted, which one is it?

%%% variable arguments should be in parentheses, and hence optional.
%%% the option could default to \_, and omitted in concrete form.

% product types
% nullary
\NewDocumentCommand{\unitTy}{s}{\Abt@{#1}{\Opn@{#1}{1}{unit}}}
\NewDocumentCommand{\unitEx}{s}{\Abt@{#1}{\Opn@{#1}{\langle\rangle}{null}}}
\NewDocumentCommand{\check@Cst}{m m}{\O@pn{check}\,#1\,\{\,#2\,\}}
\NewDocumentCommand{\check@Abt}{m m m}{\A@bt{\O@pn{check}}[#1](#2\@sep #3)}
\NewDocumentCommand{\checkEx}{s O{\rho} m m}{\IfBooleanTF{#1}{\check@Cst{#3}{#4}}{\check@Abt{#2}{#3}{#4}}}
% binary
\NewDocumentCommand{\prod@Abt}{m m}{\A@bt{\O@pn{prod}}(#1\@sep#2)}
\NewDocumentCommand{\prod@Cst}{m m}{#1\times #2}
\NewDocumentCommand{\prodTy}{s m m}{\IfBooleanTF{#1}{\prod@Cst{#2}{#3}}{\prod@Abt{#2}{#3}}}
\NewDocumentCommand{\pair@Abt}{m m m m}{\A@bt{\O@pn{pair}}[#1\@sep #2](#3\@sep #4)}
\NewDocumentCommand{\pair@Cst}{m m}{\langle #1, #2\rangle}
\NewDocumentCommand{\pairEx}{s O{\tau_1} O{\tau_2} m m}{\IfBooleanTF{#1}{\pair@Cst{#4}{#5}}{\pair@Abt{#2}{#3}{#4}{#5}}}
\NewDocumentCommand{\proj@Abt}{m m m m}{\A@bt{\O@pn{proj}}<#1>[#2\@sep #3](#4)}
\NewDocumentCommand{\proj@Cst}{m m}{#2\cdot #1}
\NewDocumentCommand{\projEx}{s r<> O{\tau_1} O{\tau_2} m}{\IfBooleanTF{#1}{\proj@Cst{#2}{#5}}{\proj@Abt{#2}{#3}{#4}{#5}}}
% n-ary
\NewDocumentCommand{\vprod@Abt}{m m m}{\A@bt{\O@pn{vprod}}<#1>({#3}_{#1})}
\NewDocumentCommand{\vprod@Cst}{m m m}{\bigtimes_{#2\in #1}(\sing@map{#2}{{#3}_{#2}})}
\NewDocumentCommand{\vprodTy}{s r<> r<> m}{\IfBooleanTF{#1}{\vprod@Cst{#2}{#3}{#4}}{\vprod@Abt{#2}{#3}{#4}}}
\NewDocumentCommand{\vtuple@Abt}{m m m m}{\A@bt{\O@pn{vtuple}}<#1>[{#3}_{#1}]({#4}_{#1})}
\NewDocumentCommand{\vtuple@Cst}{m m m}{\langle \fin@map{#1}{#2}{#3} \rangle}
\NewDocumentCommand{\vtupleEx}{s r<> r<> O{\tau} m}{\IfBooleanTF{#1}{\vtuple@Cst{#2}{#3}{#5}}{\vtuple@Abt{#2}{#3}{#4}{#5}}}
\NewDocumentCommand{\vproj@Abt}{m m m m}{\A@bt{\O@pn{vproj}}<#1\@sep #2>[{#3}_{#1}](#4)}
\NewDocumentCommand{\vproj@Cst}{m m}{#2\cdot #1}
\NewDocumentCommand{\vprojEx}{s r<> r<> O{\tau} m}{\IfBooleanTF{#1}{\vproj@Cst{#3}{#5}}{\vproj@Abt{#2}{#3}{#4}{#5}}}

% sum types
% nullary
\NewDocumentCommand{\voidTy}{s}{\Abt@{#1}{\Opn@{#1}{0}{void}}}
\NewDocumentCommand{\absurdEx}{s O{\rho} m}{\Abt@{#1}{\O@pn{absurd}}[#2](#3)}
% binary
\NewDocumentCommand{\sum@Abt}{d<> m m}{\IfValueTF{#1}{\A@bt{\O@pn{sum}}<#1>(#2\@sep #3)}{\A@bt{\O@pn{sum}}(#2\@sep  #3)}}
\NewDocumentCommand{\sum@Cst}{D<>{} m m}{#2+_{#1}#3}
\NewDocumentCommand{\sumTy}{s d<> m m}{\IfBooleanTF{#1}{\IfValueTF{#2}{\sum@Cst<#2>}{\sum@Cst}{#3}{#4}}{\IfValueTF{#2}{\sum@Abt<#2>}{\sum@Abt}{#3}{#4}}}
\NewDocumentCommand{\inj@Abt}{r<> m m m}{\A@bt{\O@pn{inj}}<#1>[#2\@sep #3](#4)}
\NewDocumentCommand{\inj@Cst}{r<> m}{#1\cdot #2}
\NewDocumentCommand{\injEx}{s r<> O{\tau_1} O{\tau_2} m}{\IfBooleanTF{#1}{\inj@Cst<#2>{#5}}{\inj@Abt<#2>{#3}{#4}{#5}}}
% explicit cases
\NewDocumentCommand{\xcase@Abt}{m m m m m m m m}{\A@bt{\O@pn{case}}[#1\@sep #2\@sep #3](#4\@sep \A@bs(#5){#6}\@sep \A@bs(#7){#8})}
\NewDocumentCommand{\xcase@Cst}{m m m m m}{\O@pn{case}\,#1\,\{\,\A@bs(#2){#3} \mid \A@bs(#4){#5} \,\}}
\NewDocumentCommand{\xcaseEx}{s O{\tau_1} O{\tau_2} O{\rho} m m m m m}{\IfBooleanTF{#1}{\xcase@Cst{#5}{#6}{#7}{#8}{#9}}{\xcase@Abt{#2}{#3}{#4}{#5}{#6}{#7}{#8}{#9}}}
% generated cases
\NewDocumentCommand{\caseEx}{s O{\tau} O{\rho} m m m}{\IfBooleanTF{#1}{\xcase@Cst{#4}{#5_1}{#6_1}{#5_2}{#6_2}}{\xcase@Abt{{#2}_1}{{#2}_2}{#3}{#4}{#5_1}{#6_1}{#5_2}{#6_2}}}
% n-ary
\NewDocumentCommand{\vsum@Abt}{m m m}{\A@bt{\O@pn{vsum}}<#1>({#3}_{#1})}
\NewDocumentCommand{\vsum@Cst}{m m m}{\bigplus_{#2\in #1}(\sing@map{#2}{{#3}_{#2}})}
\NewDocumentCommand{\vsumTy}{s r<> r<> m}{\IfBooleanTF{#1}{\vsum@Cst{#2}{#3}{#4}}{\vsum@Abt{#2}{#3}{#4}}}
\NewDocumentCommand{\vinj@Abt}{m m m m}{\A@bt{\O@pn{vinj}}<#1\@sep #2>[#3_{#1}](#4)}
\NewDocumentCommand{\vinj@Cst}{m m}{#1\cdot #2}
\NewDocumentCommand{\vinjEx}{s r<> r<> O{\tau} m}{\IfBooleanTF{#1}{\vinj@Cst{#3}{#5}}{\vinj@Abt{#2}{#3}{#4}{#5}}}
\NewDocumentCommand{\vcase@Abt}{m m m m m m m}{\A@bt{\O@pn{vcase}}<#1>[{#3}_{#1}\@sep #4](#5\@sep \A@bs(#6){#7}_{#1})}
\NewDocumentCommand{\vcase@Cst}{m m m m m}{\O@pn{vcase}\, #3\,\{\,\fin@map{#1}{#2}{\A@bs(#4){#5}}\,\}}
\NewDocumentCommand{\vcaseEx}{s r<> r<> O{\tau} O{\rho} m m m}{\IfBooleanTF{#1}{\vcase@Cst{#2}{#3}{#6}{#7}{#8}}{\vcase@Abt{#2}{#3}{#4}{#5}{#6}{#7}{#8}}}

% booleans, sum of one and one.
\NewDocumentCommand{\boolTy}{s}{\Abt@{#1}{\Opn@{#1}{2}{bool}}}
\NewDocumentCommand{\trueEx}{s}{\A@bt{\O@pn{true}}}
\NewDocumentCommand{\falseEx}{s}{\A@bt{\O@pn{false}}}
\NewDocumentCommand{\ifEx}{s O{\rho} m m m}{\Abt@{#1}{\O@pn{if}}[#2](#3\@sep  #4\@sep  #5)}

% options
\NewDocumentCommand{\optTy}{s m}{\IfBooleanTF{#1}{#2\,\O@pn{opt}}{\A@bt{\O@pn{opt}}(#2)}}
\NewDocumentCommand{\nothingEx}{s}{\A@bt{\O@pn{Nothing}}}
\NewDocumentCommand{\justEx}{s m}{\A@bt{\O@pn{Just}}(#2)}

% inductive type
\NewDocumentCommand{\indTy}{s m m}{\A@bt{\O@pn{ind}}(\A@bs(#2){#3})}
\NewDocumentCommand{\inEx}{s O{t} O{\tau} m}{\Abt@{#1}{\O@pn{in}}[\A@bs(#2){#3}](#4)}
\NewDocumentCommand{\recEx}{s O{t} O{\tau} O{\rho} m m m}{\Abt@{#1}{\O@pn{rec}}[\A@bs(#2){#3}\@sep #4](#5\@sep \A@bs(#6){#7})}

% list type
\NewDocumentCommand{\listTy}{s m}{\IfBooleanTF{#1}{#2\,\O@pn{list}}{\A@bt{\O@pn{list}}(#2)}}
\NewDocumentCommand{\nilEx}{s O{\tau}}{\Abt@{#1}{\O@pn{nil}}[#2]}
\NewDocumentCommand{\consEx}{s O{\tau} m m}{\Abt@{#1}{\O@pn{cons}}[#2](#3\@sep #4)}
\NewDocumentCommand{\listrec@Abt}{m m m m m m}{\A@bt{\O@pn{listrec}}[#1](#2\@sep #3\@sep \A@bs(#4,#5){#6})}
\NewDocumentCommand{\listrec@Cst}{m m m m m}{\O@pn{listrec}\,#1\,\{\,#2\mid\A@bs(#3,#4){#5}\}}
\NewDocumentCommand{\listrecEx}{s O{\rho} m m m m m}{\IfBooleanTF{#1}{\listrec@Cst{#3}{#4}{#5}{#6}{#7}}{\listrec@Abt{#2}{#3}{#4}{#5}{#6}{#7}}}
\NewDocumentCommand{\listcase@Abt}{m m m m m m}{\A@bt{\O@pn{listcase}}[#1](#2\@sep #3\@sep \A@bs(#4,#5){#6})}
\NewDocumentCommand{\listcase@Cst}{m m m m m}{\O@pn{listcase}\,#1\,\{\,#2\mid\A@bs(#3,#4){#5}\}}
\NewDocumentCommand{\listcaseEx}{s O{\rho} m m m m m}{\IfBooleanTF{#1}{\listcase@Cst{#3}{#4}{#5}{#6}{#7}}{\listcase@Abt{#2}{#3}{#4}{#5}{#6}{#7}}}

% nat type
\NewDocumentCommand{\natTy}{s}{\A@bt{\O@pn{nat}}}
\NewDocumentCommand{\zeroEx}{s}{\A@bt{\O@pn{zero}}}
\NewDocumentCommand{\succEx}{s m}{\A@bt{\O@pn{succ}}(#2)}
\NewDocumentCommand{\natit@Abt}{m m m m m}{\A@bt{\O@pn{natit}}[#1](#2\@sep #3\@sep \A@bs(#4){#5})}
\NewDocumentCommand{\natit@Cst}{m m m m}{\O@pn{natit}\,#1\,\{\,#2\mid\A@bs(#3){#4}\}}
\NewDocumentCommand{\natitEx}{s O{\rho} m m m m}{\IfBooleanTF{#1}{\natit@Cst{#3}{#4}{#5}{#6}}{\natit@Abt{#2}{#3}{#4}{#5}{#6}}}
\NewDocumentCommand{\ifz@Abt}{m m m m m}{\A@bt{\O@pn{ifz}}[#1](#2\@sep #3\@sep \A@bs(#4){#5})}
\NewDocumentCommand{\ifz@Cst}{m m m m}{\O@pn{ifz}\,#1\,\{\,#2\mid\A@bs(#3){#4}\}}
\NewDocumentCommand{\ifzEx}{s O{\rho} m m m m}{\IfBooleanTF{#1}{\ifz@Cst{#3}{#4}{#5}{#6}}{\ifz@Abt{#2}{#3}{#4}{#5}{#6}}}
\NewDocumentCommand{\natrec@Cst}{m m m m m}{\O@pn{natrec}\,#1\,\{\,#2\mid \A@bs(#3,#4){#5} \,\}}
\NewDocumentCommand{\natrec@Abt}{m m m m m m}{\A@bt{\O@pn{natrec}}[#1](#2\@sep #3\@sep \A@bs(#4,#5){#6})}
\NewDocumentCommand{\natrecEx}{s O{\rho} m m m m m}{\IfBooleanTF{#1}{\natrec@Cst{#3}{#4}{#5}{#6}{#7}}{\natrec@Abt{#2}{#3}{#4}{#5}{#6}{#7}}}

% coinductive type
\NewDocumentCommand{\coiTy}{s m m}{\A@bt{\O@pn{coi}}(\A@bs(#2){#3})}
\NewDocumentCommand{\outEx}{s O{t} O{\tau} m}{\Abt@{#1}{\O@pn{out}}[\A@bs(#2){#3}](#4)}
\NewDocumentCommand{\genEx}{s O{t} O{\tau} O{\sigma} m m m}{\Abt@{#1}{\O@pn{gen}}[\A@bs(#2){#3}\@sep #4](#5\@sep \A@bs(#6){#7})}

% conat
\NewDocumentCommand{\conatTy}{s}{\A@bt{\O@pn{conat}}}

% stream
\NewDocumentCommand{\streamTy}{s m}{\IfBooleanTF{#1}{#2\,\O@pn{stream}}{\A@bt{\O@pn{stream}}(#2)}}

% yes/no answer type
\NewDocumentCommand{\ansTy}{s}{\A@bt{\O@pn{ans}}}
\NewDocumentCommand{\yesEx}{s}{\A@bt{\O@pn{yes}}}
\NewDocumentCommand{\noEx}{s}{\A@bt{\O@pn{no}}}

% continuation type
\NewDocumentCommand{\contTy}{s m}{\IfBooleanTF{#1}{#2\,\@kw{cont}}{\A@bt{\O@pn{cont}}(#2)}}
\NewDocumentCommand{\contEx}{s O{\tau} m}{\Abt@{#1}{\O@pn{cont}}[#2](#3)}
\NewDocumentCommand{\letccEx}{s O{\tau} m m}{\Abt@{#1}{\O@pn{letcc}}[#2](\A@bs(#3){#4})}
\NewDocumentCommand{\throwEx}{s O{\tau} O{\rho} m m}{\Abt@{#1}{\O@pn{throw}}[#2\@sep #3](#4\@sep #5)}
\NewDocumentCommand{\letccCmd}{s O{\tau} m m}{\Abt@{#1}{\O@pn{letcc}}[#2](\A@bs(#3){#4})}
\NewDocumentCommand{\throwCmd}{s O{\rho} m m}{\Abt@{#1}{\O@pn{throw}}[#2](#3\@sep #4)}
% stacks
\NewDocumentCommand{\frmSlot}{s}{\A@bt{\O@pn*{\mathord{-}}}}
\NewDocumentCommand{\empStk}{s O{\tau}}{\Abt@{#1}{\Opn@{#1}{\bullet}{emp}}[#2]}
\NewDocumentCommand{\extStk}{s O{\tau_1} O{\tau_2} m m}{\IfBooleanTF{#1}{#4\mathbin{\circ} #5}{\A@bt{\O@pn{ext}}[#2\@sep #3](#4\@sep #5)}}

% total function type
\NewDocumentCommand{\arr@Abt}{m m}{\A@bt{\O@pn{fun}}(#1\@sep #2)}
\NewDocumentCommand{\arr@Cst}{m m}{#1\to #2}
\NewDocumentCommand{\arrTy}{s m m}{\IfBooleanTF{#1}{\arr@Cst{#2}{#3}}{\arr@Abt{#2}{#3}}}
\NewDocumentCommand{\funTy}{s m m}{\IfBooleanTF{#1}{\arr@Cst{#2}{#3}}{\arr@Abt{#2}{#3}}}
\NewDocumentCommand{\lamEx}{s O{\tau_1} O{\tau_2} m m}{\Abt@{#1}{\Opn@{#1}{\lambda}{lam}}[#2\@sep #3](\A@bs(#4){#5})}
\NewDocumentCommand{\appEx}{s O{\tau_1} O{\tau_2} m m}{\Abt@{#1}{\O@pn{ap}}[#2\@sep #3](#4\@sep #5)}

% universal and existential types
\NewDocumentCommand{\allTy}{s m m}{\Abt@{#1}{\Opn@{#1}{\forall}{all}}(\A@bs(#2){#3})}
\NewDocumentCommand{\tlamEx}{s m O{\tau} m}{\Abt@{#1}{\Opn@{#1}{\Lambda}{tlam}}(\A@bs(#2){#4})}
\NewDocumentCommand{\tapEx}{s O{t} O{\tau} m m}{\Abt@{#1}{\O@pn{tap}}[\A@bs(#2){#3}](#4\@sep #5)}

\NewDocumentCommand{\someTy}{s m m}{\Abt@{#1}{\Opn@{#1}{\exists}{some}}(\A@bs(#2){#3})}
\NewDocumentCommand{\packEx}{s O{t} O{\tau} m m}{\Abt@{#1}{\O@pn{pack}}[\A@bs(#2){#3}](#4\@sep  #5)}
\NewDocumentCommand{\openEx}{s O{t} O{\tau} O{\rho} m m m m}{\Abt@{#1}{\O@pn{open}}[\A@bs(#2){#3}\@sep #4](#5\@sep \A@bs(#6,#7){#8})}

% partial function type with recursive lambda, shares application form with total
\NewDocumentCommand{\parr@Abt}{m m}{\A@bt{\O@pn{parr}}(#1\@sep  #2)}
\NewDocumentCommand{\parr@Cst}{m m}{#1\mathbin{\rightharpoonup} #2}
\NewDocumentCommand{\parrTy}{s m m}{\IfBooleanTF{#1}{\parr@Cst{#2}{#3}}{\parr@Abt{#2}{#3}}}
\NewDocumentCommand{\funEx}{s O{\tau_1} O{\tau_2} m m m}{\Abt@{#1}{\O@pn{fun}}[#2\@sep #3](\A@bs(#4,#5){#6})}
\NewDocumentCommand{\papEx}{s O{\tau_1} O{\tau_2} m m}{\Abt@{#1}{\O@pn{ap}}[#2\@sep #3](#4\@sep #5)}
\NewDocumentCommand{\fixEx}{s O{\tau} m m}{\Abt@{#1}{\O@pn{fix}}[#2](\A@bs(#3){#4})}

% suspensions
\NewDocumentCommand{\suspTy}{s m}{\IfBooleanTF{#1}{#2\,\@kw{susp}}{\A@bt{\O@pn{susp}}(#2)}}
\NewDocumentCommand{\suspEx}{s O{\tau} m}{\Abt@{#1}{\O@pn{susp}}[#2](#3)}
\NewDocumentCommand{\forceEx}{s O{\tau} m}{\Abt@{#1}{\O@pn{force}}[#2](#3)}

% generic computations
\NewDocumentCommand{\compTy}{s m}{\IfBooleanTF{#1}{#2\,\@kw{comp}}{\Abt@{#1}{\O@pn{comp}}(#2)}}
\NewDocumentCommand{\compEx}{s m}{\Abt@{#1}{\O@pn{comp}}(#2)}
\NewDocumentCommand{\retEx}{s O{\tau} m}{\Abt@{#1}{\O@pn{ret}}[#2](#3)}
\NewDocumentCommand{\bndEx}{s O{\tau} m m m}{\Abt@{#1}{\O@pn{bind}}[#2](#3\@sep \A@bs(#4){#5})}

% recursive type
\NewDocumentCommand{\recTy}{s m m}{\A@bt{\O@pn{rec}}(\A@bs(#2){#3})}
\NewDocumentCommand{\foldEx}{s O{t} O{\tau} m}{\Abt@{#1}{\O@pn{fold}}[\A@bs(#2){#3}](#4)}
\NewDocumentCommand{\unfoldEx}{s O{t} O{\tau} m}{\Abt@{#1}{\O@pn{unfold}}[\A@bs(#2){#3}](#4)}

% self-reference
\NewDocumentCommand{\selfTy}{s m}{\IfBooleanTF{#1}{#2\,\@kw{self}}{\A@bt{\O@pn{self}}(#2)}}
\NewDocumentCommand{\unrollEx}{s O{\tau} m}{\Abt@{#1}{\O@pn{unroll}}[#2](#3)}
\NewDocumentCommand{\selfEx}{s O{\tau} m m}{\Abt@{#1}{\O@pn{self}}[#2](\A@bs(#3){#4})}

% untyped
\NewDocumentCommand{\ulamEx}{s m m}{\Abt@{#1}{\Opn@{#1}{\lambda}{lam}}(\A@bs(#2){#3})}
\NewDocumentCommand{\uapEx}{s m m}{\IfBooleanTF{#1}{#2(#3)}{\A@bt{\O@pn{app}}(#2\@sep #3)}}
\NewDocumentCommand{\uIEx}{s}{\A@bt{\O@pn{I}}}
\NewDocumentCommand{\uKEx}{s}{\A@bt{\O@pn{K}}}
\NewDocumentCommand{\uSEx}{s}{\A@bt{\O@pn{S}}}
\NewDocumentCommand{\uBEx}{s}{\A@bt{\O@pn{B}}}

% symbols

\NewDocumentCommand{\newCmd}{s O{\tau} m m}{\IfBooleanTF{#1}{\@kw{new}\,#3\mathbin{\sim}#2\mathbin{\@kw{in}} #4}{\A@bt{\O@pn{new}}[#2](\A@bs<#3>{#4})}}

\NewDocumentCommand{\symTy}{s m}{\IfBooleanTF{#1}{#2\,\@kw{sym}}{\A@bt{\O@pn{sym}}(#2)}}
\NewDocumentCommand{\quoteEx}{s r<>}{\IfBooleanTF{#1}{\@kw{'}#2}{\A@bt{\O@pn{quote}}<#2>}}
\NewDocumentCommand{\ifisCmd}{s r<> O{t} O{\rho} m m m}{\IfBooleanTF{#1}{\A@bt*}{\A@bt}{\O@pn{is}}<#2>[\A@bs(#3){#4}](#5\@sep #6\@sep #7)}
\NewDocumentCommand{\ifeqCmd}{s O{t} O{\rho} m m m m}{\IfBooleanTF{#1}{\A@bt*}{\A@bt}{\O@pn{eq}}[\A@bs(#2){#3}](#4\@sep #5\@sep #6\@sep #7)}
\NewDocumentCommand{\newsymCmd}{s O{\tau}}{\A@bt{\O@pn{gensym}}[#2]}

% dynamic classification
\NewDocumentCommand{\newclsCmd}{s O{\tau}}{\A@bt{\O@pn{newcls}}[#2]}
\NewDocumentCommand{\clsfdTy}{s}{\Abt{\Opn{clsfd}}}
\NewDocumentCommand{\clsinEx}{s r<> m}{\Abt{\Opn{in}}<#2>(#3)}
\NewDocumentCommand{\clsoutEx}{s r<> m}{\Abt{\Opn{out}}<#2>(#3)}
\NewDocumentCommand{\clsrefTy}{s m}{\IfBooleanTF{#1}{#2\,\kw{cls}}{\Abt{\Opn{cls}}(#2)}}
\NewDocumentCommand{\clsrefEx}{s m}{\IfBooleanTF{#1}{\kw{\&}\,#2}{\Abt{\Opn{cls}}(#2)}}
\NewDocumentCommand{\clsinrefEx}{s m m}{\Abt{\Opn{clsfy}}(#2\@sep* #3)}
\NewDocumentCommand{\clsoutrefEx}{s m m}{\Abt{\Opn{declsfy}}(#2\@sep* #3)}

% commands
\NewDocumentCommand{\cmdTy}{s m}{\IfBooleanTF{#1}{#2\,\O@pn{cmd}}{\A@bt{\O@pn{cmd}}(#2)}}
\NewDocumentCommand{\cmdEx}{s O{\tau} m}{\Abt@{#1}{\O@pn{cmd}}[#2](#3)}

\NewDocumentCommand{\retCmd}{s O{\rho} m}{\Abt@{#1}{\O@pn{ret}}[#2](#3)}
\NewDocumentCommand{\raiseCmd}{s O{\rho} m}{\Abt@{#1}{\O@pn{raise}}[#2](#3)}

\NewDocumentCommand{\bnd@Abt}{m m m m m}{\A@bt{\O@pn{bnd}}[#1\@sep  #2](#3\@sep \A@bs(#4){#5})}
\NewDocumentCommand{\bnd@Cst}{m m m}{\O@pn{bnd}\,#2\mathbin{\leftarrow}#1\@sep* #3}
% \NewDocumentCommand{\bnd@Cst}{m m m}{\A@bt{\O@pn{bnd}}(#1\@sep \A@bs(#2){#3})}
\NewDocumentCommand{\bndCmd}{s O{\tau} m O{\rho} m m}{\IfBooleanTF{#1}{\bnd@Cst{#3}{#5}{#6}}{\bnd@Abt{#2}{#4}{#3}{#5}{#6}}}

\NewDocumentCommand{\retunitCmd}{s}{\O@pn{ret}}
\NewDocumentCommand{\doCmd}{s o m}{\Abt@{#1}{\O@pn{do}}[#2](#3)}
\NewDocumentCommand{\seq@Abt}{m O{\_} m}{\A@bt{\O@pn{seq}}(#1\@sep \A@bs(#2){#3})}
\NewDocumentCommand{\seq@Cst}{m o m}{\IfValueT{#2}{#2\mathbin{\leftarrow}}#1\@sep* #3}
\NewDocumentCommand{\seqCmd}{s m o m}{\IfBooleanTF{#1}{\seq@Cst{#2}[#3]{#4}}{\seq@Abt{#2}[#3]{#4}}}

\NewDocumentCommand{\ifCmd}{s O{\rho} m m m}{\IfBooleanTF{#1}{\ifEx*{#3}{#4}{#5}}{\ifEx[#2]{#3}{#4}{#5}}}

\NewDocumentCommand{\bndow@Abt}{m m m m m m}{\A@bt{\O@pn{bndow}}[#1](#2\@sep \A@bs(#3){#4}\@sep \A@bs(#5){#6})}
\NewDocumentCommand{\bndow@Cst}{m m m m m}{\O@pn{bnd}\,#2\mathbin{\leftarrow}#1\@sep* #3\mathbin{\@kw{ow}}#4\mathbin{\rightarrow}\,#5}
\NewDocumentCommand{\bndowCmd}{s O{\rho} m m m m m}{\IfBooleanTF{#1}{\bndow@Cst{#3}{#4}{#5}{#6}{#7}}{\bndow@Abt{#2}{#3}{#4}{#5}{#6}{#7}}}

\NewDocumentCommand{\dcl@Abt}{m m m m}{\A@bt{\O@pn{dcl}}[#1\@sep  #2](#3\@sep  #4)}
\NewDocumentCommand{\dcl@Cst}{m m m}{\O@pn{dcl}\,#2\mathbin{\@kw{:=}}#1\,\@kw{in}\,#3}
\NewDocumentCommand{\dclCmd}{s O{\tau} m O{\rho} r<> m}{\IfBooleanTF{#1}{\dcl@Cst{#3}{#5}{#6}}{\dcl@Abt{#2}{#4}{#3}{\A@bs<#5>{#6}}}}

% reference types
\NewDocumentCommand{\refTy}{s m}{\IfBooleanTF{#1}{#2\,\O@pn{ref}}{\A@bt{\O@pn{ref}}(#2)}}
\NewDocumentCommand{\ref@Abt}{m}{\A@bt{\O@pn{ref}}<#1>}
\NewDocumentCommand{\ref@Cst}{m}{\texttt{\&}\,#1}
\NewDocumentCommand{\refEx}{s r<>}{\IfBooleanTF{#1}{\ref@Cst{#2}}{\ref@Abt{#2}}}

\NewDocumentCommand{\get@Abt}{m}{\A@bt{\O@pn{get}}<#1>}
\NewDocumentCommand{\get@Cst}{m}{\O@pn{!}{#1}}
\NewDocumentCommand{\getCmd}{s r<>}{\IfBooleanTF{#1}{\get@Cst{#2}}{\get@Abt{#2}}}

\NewDocumentCommand{\getref@Abt}{m m}{\A@bt{\O@pn{getref}}[#1](#2)}
\NewDocumentCommand{\getref@Cst}{m}{\@kw{*}#1}
\NewDocumentCommand{\getrefCmd}{s O{\tau} m}{\IfBooleanTF{#1}{\getref@Cst{#3}}{\getref@Abt{#2}{#3}}}

\NewDocumentCommand{\set@Abt}{m m}{\A@bt{\O@pn{set}}<#1>(#2)}
\NewDocumentCommand{\set@Cst}{m m}{#1\mathbin{\@kw{:=}}#2}
\NewDocumentCommand{\setCmd}{s r<> m}{\IfBooleanTF{#1}{\set@Cst{#2}{#3}}{\set@Abt{#2}{#3}}}

\NewDocumentCommand{\setref@Abt}{m m m}{\A@bt{\O@pn{setref}}[#1](#2\@sep  #3)}
\NewDocumentCommand{\setref@Cst}{m m}{#1\mathbin{\@kw{*{=}}} #2}
\NewDocumentCommand{\setrefCmd}{s O{\tau} m m}{\IfBooleanTF{#1}{\setref@Cst{#3}{#4}}{\setref@Abt{#2}{#3}{#4}}}

\NewDocumentCommand{\newrefCmd}{s O{\tau} m}{\IfBooleanTF{#1}{\@kw{newref}(#3)}{\A@bt{\O@pn{newref}}[#2](#3)}}

\NewDocumentCommand{\preincCmd}{s r<>}{\IfBooleanTF{#1}{\@kw{++}#2}{\A@bt{\O@pn{inc}}<#2>}}
\NewDocumentCommand{\postincCmd}{s r<>}{\IfBooleanTF{#1}{#2\@kw{++}}{\A@bt{\O@pn{cni}}<#2>}}
\NewDocumentCommand{\predecCmd}{s r<>}{\IfBooleanTF{#1}{\@kw{{-}{-}}#2}{\A@bt{\O@pn{dec}}<#2>}}
\NewDocumentCommand{\postdecCmd}{s r<>}{\IfBooleanTF{#1}{#2\@kw{{-}{-}}}{\A@bt{\O@pn{ced}}<#2>}}

% effect handlers
% \NewDocumentCommand{\doCmd}{s r<> d() o}{\IfBooleanTF{#1}{\@kw{do}\,#2\IfValueT{#3}{(#3)}\IfValueT{#4}{(#4)}}{\A@bt{\O@pn{do}}<#2>(#3)\IfValueT{#4}{(#4)}}}
% \NewDocumentCommand{\hdl@Cst}{r<> m m m m m m}{\@kw{hdl}\,#2\,\{\,\@kw{ret}(#3)\mathbin{\hookrightarrow} #4\mathrel{|}#1(#5,#6) \mathbin{\hookrightarrow}#7\,\}}
% \NewDocumentCommand{\hdl@Abt}{r<> m m m m m m m}{\A@bt{\O@pn{hdl}}<#1>[#2](#3\@sep \A@bs(#4){#5} \@sep \A@bs(#6,#7){#8})}
% \NewDocumentCommand{\hdlCmd}{s r<> O{\tau} m m m m m m}{\IfBooleanTF{#1}{\hdl@Cst<#2>{#4}{#5}{#6}{#7}{#8}{#9}}{\hdl@Abt<#2>{#3}{#4}{#5}{#6}{#7}{#8}{#9}}}

% module types
\NewDocumentCommand{\univSg}{s}{\A@bt{\O@pn{Type}}}
\NewDocumentCommand{\typSg}{s}{\univSg}
\NewDocumentCommand{\valSg}{s m}{\A@bt{\O@pn{Val}}(#2)}

\NewDocumentCommand{\comp@Abt}{m}{\A@bt{\O@pn{Comp}}(#1)}
\NewDocumentCommand{\comp@Cst}{m}{\A@bt{\O@pn{Comp}}(#1)}
\NewDocumentCommand{\compSg}{s m}{\IfBooleanTF{#1}{\comp@Cst{#2}}{\comp@Abt{#2}}}

\NewDocumentCommand{\staticLock}{s}{\Abt@{#1}{\O@pn{st}}}
\NewDocumentCommand{\starEx}{s}{\ast}
\NewDocumentCommand{\starMd}{s}{\star}
\NewDocumentCommand{\ext@Abt}{m m}{\A@bt{\O@pn{Ext}}(#1\@sep  #2)}
\NewDocumentCommand{\ext@Cst}{m m}{\{#1\mid \staticLock\hookrightarrow #2\}}
\NewDocumentCommand{\extSg}{s m m}{\IfBooleanTF{#1}{\ext@Cst{#2}{#3}}{\ext@Abt{#2}{#3}}}
\NewDocumentCommand{\isMd}{s o o m}{\Abt@{#1}{\O@pn{is}}[#2\@sep #3](#4)}
\NewDocumentCommand{\asMd}{s o o m}{\Abt@{#1}{\O@pn{as}}[#2\@sep #3](#4)}

% \NewDocumentCommand{\sig@Abt}{m m m}{\A@bt{\O@pn{Sig}}(#1\@sep \A@bs(#2){#3})}
% \NewDocumentCommand{\sig@Cst}{m m m}{#2{\mathbin{:}}#1\times #3}
% \NewDocumentCommand{\sigSg}{s m m m}{\IfBooleanTF{#1}{\sig@Cst{#2}{#3}{#4}}{\sig@Abt{#2}{#3}{#4}}}
% \NewDocumentCommand{\sigTy}{s m o m}{\IfBooleanTF{#1}{\IfNoValueTF{#3}{\prodTy*{#2}{#4}}{\sig@Cst{#2}{#3}{#4}}}{\IfNoValueTF{#3}{\sig@Abt{#2}{\_}{#4}}{\sig@Abt{#2}{#3}{#4}}}}

\NewDocumentCommand{\unitSg}{s}{\IfBooleanTF{#1}{1}{\O@pn{Unit}}}
\NewDocumentCommand{\unitMd}{s}{\IfBooleanTF{#1}{\O@pn*{\langle\rangle}}{\O@pn{triv}}}

\NewDocumentCommand{\sigSg@Abt}{m O{\_} m}{\A@bt{\O@pn{Sig}}(#1\@sep\A@bs(#2){#3})}
\NewDocumentCommand{\sigSg@Cst}{m o m}{\IfValueT{#2}{#2\mathbin{:}}#1\times #3}
\NewDocumentCommand{\sigSg}{s m o m}{\IfBooleanTF{#1}{\sigSg@Cst{#2}[#3]{#4}}{\sigSg@Abt{#2}[#3]{#4}}}
\NewDocumentCommand{\sigTy}{s m o m}{\IfBooleanTF{#1}{\sigSg@Cst{#2}[#3]{#4}}{\sigSg@Abt{#2}[#3]{#4}}}
\NewDocumentCommand{\strSg@Abt}{m O{\_} m}{\A@bt{\O@pn{Str}}(#1\@sep\A@bs(#2){#3})}
\NewDocumentCommand{\strSg@Cst}{m o m}{\IfValueT{#2}{#2\mathbin{:}}#1\times #3}
\NewDocumentCommand{\strSg}{s m o m}{\IfBooleanTF{#1}{\strSg@Cst{#2}[#3]{#4}}{\strSg@Abt{#2}[#3]{#4}}}

\NewDocumentCommand{\strMd@Abt}{m m m m m}{\A@bt{\O@pn{str}}[#1\@sep\A@bs(#2){#3}](#4\@sep #5)}
\NewDocumentCommand{\strMd@Cst}{m m}{\A@bt{\O@pn{str}}(#1\@sep #2)}
\NewDocumentCommand{\strMd}{s o O{\_} o m m}{\IfBooleanTF{#1}{\strMd@Cst{#5}{#6}}{\strMd@Abt{#2}{#3}{#4}{#5}{#6}}}
\NewDocumentCommand{\projMd}{s r<> o O{\_} o m}{\IfBooleanTF{#1}{#6\cdot\@kw{#2}}{\A@bt{\O@pn{proj}}<#2>[#3\@sep \A@bs(#4){#5}](#6)}}

% \NewDocumentCommand{\pi@Abt}{m m m}{\A@bt{\O@pn{Pi}}(#1\@sep \A@bs(#2){#3})}
% \NewDocumentCommand{\pi@Cst}{m m m}{#2{\mathbin{:}}#1\to #3}
% \NewDocumentCommand{\piSg}{s m m m}{\IfBooleanTF{#1}{\pi@Cst{#2}{#3}{#4}}{\pi@Abt{#2}{#3}{#4}}}
% \NewDocumentCommand{\piTy}{s m o m}{\IfBooleanTF{#1}{\IfNoValueTF{#3}{\funTy*{#2}{#4}}{\pi@Cst{#2}{#3}{#4}}}{\IfNoValueTF{#3}{\pi@Abt{#2}{\_}{#4}}{\pi@Abt{#2}{#3}{#4}}}}

\NewDocumentCommand{\piSg@Abt}{m O{\_} m}{\A@bt{\O@pn{Pi}}(#1\@sep\A@bs(#2){#3})}
\NewDocumentCommand{\piSg@Cst}{m o m}{\IfValueT{#2}{#2\mathbin{:}}#1\to #3}
\NewDocumentCommand{\piSg}{s m o m}{\IfBooleanTF{#1}{\piSg@Cst{#2}[#3]{#4}}{\piSg@Abt{#2}[#3]{#4}}}
\NewDocumentCommand{\piTy}{s m o m}{\IfBooleanTF{#1}{\piSg@Cst{#2}[#3]{#4}}{\piSg@Abt{#2}[#3]{#4}}}
\NewDocumentCommand{\funSg@Abt}{m O{\_} m}{\A@bt{\O@pn{Fun}}(#1\@sep\A@bs(#2){#3})}
\NewDocumentCommand{\funSg@Cst}{m o m}{\IfValueT{#2}{#2\mathbin{:}}#1\to #3}
\NewDocumentCommand{\funSg}{s m o m}{\IfBooleanTF{#1}{\funSg@Cst{#2}[#3]{#4}}{\funSg@Abt{#2}[#3]{#4}}}
\NewDocumentCommand{\gfunSg@Abt}{m O{\_} m}{\A@bt{\O@pn{Fun}}(#1\@sep\A@bs(#2){#3})}
\NewDocumentCommand{\gfunSg@Cst}{m o m}{\IfValueT{#2}{#2\mathbin{:}}#1\pto #3}
\NewDocumentCommand{\gfunSg}{s m o m}{\IfBooleanTF{#1}{\gfunSg@Cst{#2}[#3]{#4}}{\gfunSg@Abt{#2}[#3]{#4}}}

\NewDocumentCommand{\funMd@Abt}{m m m m}{\A@bt{\O@pn{fun}}[#1\@sep \A@bs(#2){#3}](\A@bs(#2){#4})}
\NewDocumentCommand{\funMd@Cst}{m m m}{\O@pn{fun}(\Abs(#2){#3})}  % no type label?
\NewDocumentCommand{\funMd}{s m m o m}{\IfBooleanTF{#1}{\funMd@Cst{#2}{#3}{#5}}{\funMd@Abt{#2}{#3}{#4}{#5}}}
\NewDocumentCommand{\instMd@Abt}{m m m m m}{\A@bt{\O@pn{app}}[#1\@sep \A@bs(#2){#3}](#4\@sep #5)}
\NewDocumentCommand{\instMd@Cst}{m m}{\O@pn{app}(#1\@sep #2)}
\NewDocumentCommand{\instMd}{s o o o m m}{\IfBooleanTF{#1}{\instMd@Cst{#5}{#6}}{\instMd@Abt{#2}{#3}{#4}{#5}{#6}}}

% cbpv / polarization
\NewDocumentCommand{\freeTy}{s m}{\Abt@{#1}{\Opn@{#1}{\downarrow}{F}}(#2)}
\NewDocumentCommand{\freeEx}{s o m}{\Abt@{#1}{\O@pn{ret}}[#2](#3)}
\NewDocumentCommand{\fletEx}{s o o m m m}{\IfBooleanTF{#1}{\@kw{bind}\,#5\leftarrow #4\@sep* #6}{\Abt@{#1}{\O@pn{bind}}[#2\@sep #3](#4\@sep \A@bs(#5){#6})}}
\NewDocumentCommand{\thunkTy}{s m}{\Abt@{#1}{\Opn@{#1}{\uparrow}{U}}(#2)}
\NewDocumentCommand{\thunkEx}{s o m}{\Abt@{#1}{\O@pn{susp}}[#2](#3)}
%\NewDocumentCommand{\recthunkEx}{s d<> o m m}{\Abt@{#1}{\O@pn{susp}}<#2>[#3](\Abs(#4){#5})}
\NewDocumentCommand{\recthunkEx}{s d<> o m m}{\IfBooleanTF{#1}{\O@pn{susp}\IfValueT{#2}{^{(#2)}}(\Abs(#4){#5})}{\A@bt{\O@pn{susp}}<#2>[#3](\Abs(#4){#5})}}
%\NewDocumentCommand{\forceEx}{s o m}{\Abt@{#1}{\O@pn{force}}[#2](#3)}
% copower needs linearity, not suitable for cbpv.
\NewDocumentCommand{\copTy}{s m m}{\IfBooleanTF{#1}{#2\mathbin{\ltimes} #3}{\Abt@{#1}{\O@pn{copow}}(#2\@sep #3)}}
\NewDocumentCommand{\coppair@Abt}{m m m m}{\A@bt{\O@pn{copow}}[#1\@sep #2](#3\@sep #4)}
\NewDocumentCommand{\coppair@Cst}{m m}{#1\mathbin{\ltimes} #2}
\NewDocumentCommand{\copEx}{s o o m m}{\IfBooleanTF{#1}{\coppair@Cst{#4}{#5}}{\coppair@Abt{#2}{#3}{#4}{#5}}}
\NewDocumentCommand{\cosplitEx}{s o o o m m m m}{\IfBooleanTF{#1}{\@kw{cosplit}\,#5\,\{\,\A@bs(#6,#7){#8}\,\}}{\A@bt{\O@pn{cosplit}}[#2\@sep #3\@sep #4](#5\@sep \A@bs(#6,#7){#8})}}

% eager product
\NewDocumentCommand{\tensorTy}{s m m}{\IfBooleanTF{#1}{{#2}\otimes{#3}}{\A@bt{\O@pn{tens}}(#2\@sep #3)}}
\NewDocumentCommand{\tensorEx}{s O{\tau_1} O{\tau_2} m m}{\IfBooleanTF{#1}{{#4}\otimes{#5}}{\A@bt{\O@pn{with}}[#2\@sep  #3](#4\@sep  #5)}}
\NewDocumentCommand{\splitEx}{s O{\tau_1} O{\tau_2} O{\rho} m m m m}{\IfBooleanTF{#1}{\@kw{split}\,{#5}\,\{\,\A@bs(#6,#7){#8}\,\}}{\A@bt{\O@pn{split}}[#2\@sep #3\@sep #4](#5\@sep \A@bs(#6,#7){#8})}}

% lazy, not memoized, product
\NewDocumentCommand{\bothTy}{s m m}{\IfBooleanTF{#1}{#2\mathbin{\&} #3}{\A@bt{\O@pn{both}}(#2\@sep #3)}}
\NewDocumentCommand{\bothEx}{s m m}{\IfBooleanTF{#1}{#2\mathbin{\&} #3}{\A@bt{\O@pn{both}}(#2\@sep #3)}}
\NewDocumentCommand{\parEx}{s m m m m}{\A@bt{\O@pn{par}}(#2\@sep \A@bs(#3,#4){#5})}
\NewDocumentCommand{\topTy}{s}{\A@bt{\O@pn*{\top}}}
\NewDocumentCommand{\topEx}{s}{\A@bt{\O@pn*{\star}}}
\NewDocumentCommand{\chckEx}{s O{\rho} m m}{\IfBooleanTF{#1}{\@kw{split}\,#3\,\{#4\}}{\A@bt{\O@pn{check}}[#2](#3\@sep #4)}}

% processes
\NewDocumentCommand{\unitPr}{s}{\Abt@{#1}{\Opn@{#1}{1}{one}}}
\NewDocumentCommand{\parPr}{s m m}{\IfBooleanTF{#1}{#2 \otimes #3}{\A@bt{\O@pn{par}}(#2\@sep #3)}}
\NewDocumentCommand{\nullPr}{s}{\Abt@{#1}{\Opn@{#1}{0}{null}}}
\NewDocumentCommand{\choosePr}{s m m}{\IfBooleanTF{#1}{#2\oplus #3}{\A@bt{\O@pn{or}}(#2\@sep #3)}}
%\NewDocumentCommand{\quePr}{s m m}{\Abt@{#1}{\Opn@{#1}{?}{que}}<#2>(#3)}
%\NewDocumentCommand{\sigPr}{s m m}{\Abt@{#1}{\Opn@{#1}{!}{sig}}<#2>(#3)}
\NewDocumentCommand{\sigPr}{s m m}{\IfBooleanTF{#1}{\mathop{!}#2\,(#3)}{\A@bt{\O@pn{sig}}<#2>(#3)}}
\NewDocumentCommand{\quePr}{s m m}{\IfBooleanTF{#1}{\mathop{?}#2\,(#3)}{\A@bt{\O@pn{que}}<#2>(#3)}}
% \NewDocumentCommand{\rcvPr}{s m m m}{\Abt@{#1}{\Opn@{#1}{?}{rcv}}<#2>(\A@bs(#3){#4})}
%\NewDocumentCommand{\sndPr}{s m m m}{\Abt@{#1}{\Opn@{#1}{!}{snd}}<#2>(#3\@sep #4)}
\NewDocumentCommand{\rcvPr}{s m m m}{\IfBooleanTF{#1}{\mathop{?}#2\,(\A@bs(#3){#4})}{\A@bt{\O@pn{rcv}}<#2>(\A@bs(#3){#4})}}
\NewDocumentCommand{\sndPr}{s m m m}{\IfBooleanTF{#1}{\mathop{!}#2\,(#3\@sep #4)}{\A@bt{\O@pn{snd}}<#2>(#3\@sep #4)}}
\NewDocumentCommand{\asndPr}{s m m}{\IfBooleanTF{#1}{\mathop{!}#2\,(#3)}{\A@bt{\O@pn{asnd}}<#2>(#3)}}
%\NewDocumentCommand{\asndPr}{s m m}{\Abt@{#1}{\Opn@{#1}{!}{asnd}}<#2>(#3)}
\NewDocumentCommand{\syncPr}{s m}{\Abt@{#1}{\O@pn{sync}}(#2)}
\NewDocumentCommand{\newPr}{s O{\tau} m m}{\Abt@{#1}{\Opn@{#1}{\nu}{new}}[#2](\A@bs(#3){#4})}
\NewDocumentCommand{\runPr}{s r<> m}{\A@bt{\O@pn{run}}<#2>(#3)}

% actions
\NewDocumentCommand{\silAc}{s}{\Abt@{#1}{\Opn@{#1}{\epsilon}{sil}}}
\NewDocumentCommand{\sigAc}{s m}{\IfBooleanTF{#1}{#2\O@pn*{!}}{\A@bt{\O@pn{sig}}<#2>}}
\NewDocumentCommand{\queAc}{s m}{\IfBooleanTF{#1}{#2\O@pn*{?}}{\A@bt{\O@pn{que}}<#2>}}
\NewDocumentCommand{\sndAc}{s m m}{\IfBooleanTF{#1}{#2\O@pn*{!}#3}{\A@bt{\O@pn{snd}}<#2>(#3)}}
\NewDocumentCommand{\rcvAc}{s m m}{\IfBooleanTF{#1}{#2\O@pn*{?}#3}{\A@bt{\O@pn{rcv}}<#2>(#3)}}
\NewDocumentCommand{\anyAc}{s m}{\IfBooleanTF{#1}{#2\O@pn*{?}}{\A@bt{\O@pn{any}}(#2)}}
\NewDocumentCommand{\emitAc}{s m}{\IfBooleanTF{#1}{#2\O@pn*{!}}{\A@bt{\O@pn{emit}}(#2)}}

% concurrent algol
\NewDocumentCommand{\nullEv}{s}{\Abt@{#1}{\Opn@{#1}{0}{null}}}
\NewDocumentCommand{\orEv}{s O{\tau} m m}{\IfBooleanTF{#1}{#3\oplus #4}{\A@bt{\O@pn{or}}[#2](#3\@sep #4)}}
\NewDocumentCommand{\rcvEv}{s r<>}{\Abt@{#1}{\O@pn{rcv}}<#2>}
\NewDocumentCommand{\sndEv}{s r<> m}{\Abt@{#1}{\O@pn{snd}}<#2>(#3)}
\NewDocumentCommand{\wrapEv}{s O{\tau} m m m}{\A@bt{\O@pn{wrap}}[#2](#3\@sep\Abs(#4){#5})}
\NewDocumentCommand{\emitCmd}{s O{\tau} m}{\A@bt{\O@pn{emit}}\IfBooleanF{#1}{[#2]}(#3)}
\NewDocumentCommand{\accCmd}{s O{\tau}}{\A@bt{\O@pn{acc}}\IfBooleanF{#1}{[#2]}}
\NewDocumentCommand{\syncCmd}{s O{\tau} m}{\A@bt{\O@pn{sync}}\IfBooleanF{#1}{[#2]}(#3)}
\NewDocumentCommand{\spawnCmd}{s O{\tau} m}{\A@bt{\O@pn{spawn}}\IfBooleanF{#1}{[#2]}(#3)}
\NewDocumentCommand{\newchCmd}{s m}{\IfBooleanTF{#1}{\O@pn{newch}_{#2}}{\A@bt{\O@pn{newch}}[#2]}}
\NewDocumentCommand{\sndCmd}{s r<> m}{\A@bt{\O@pn{send}}<#2>(#3)}
\NewDocumentCommand{\rcvCmd}{s r<> m m}{\A@bt{\O@pn{recv}}<#2>(\A@bs(#3){#4})}

% propositions
\NewDocumentCommand{\trueProp}{s}{\Abt@{#1}{\Opn@{#1}{\top}{truth}}}
\NewDocumentCommand{\trueIPf}{s}{\Abt@{#1}{\Opn@{#1}{\top\@kw{I}}{truthI}}}

\NewDocumentCommand{\andProp}{s m m}{\IfBooleanTF{#1}{#2\wedge #3}{\A@bt{\O@pn{and}}(#2\@sep #3)}}
\NewDocumentCommand{\andIPf}{s o o m m}{\Abt@{#1}{\Opn@{#1}{\wedge\@kw{I}}{andI}}[#2\@sep #3](#4\@sep #5)}
\NewDocumentCommand{\andEPf}{s o o r<> m}{\Abt@{#1}{\Opn@{#1}{\wedge\@kw{E}}{andE}}<#4>[#2\@sep #3](#5)}

\NewDocumentCommand{\falseProp}{s}{\Abt@{#1}{\Opn@{#1}{\bot}{falsity}}}
\NewDocumentCommand{\falseIPf}{s o m}{\Abt@{#1}{\Opn@{#1}{\bot\@kw{I}}{falseI}}[#2](#3)}  % for use when contradiction is a judgment
\NewDocumentCommand{\falseEPf}{s o m}{\Abt@{#1}{\Opn@{#1}{\bot\@kw{E}}{falseE}}[#2](#3)}

\NewDocumentCommand{\orProp}{s m m}{\IfBooleanTF{#1}{#2\vee #3}{\A@bt{\O@pn{or}}(#2\@sep #3)}}
\NewDocumentCommand{\orIPf}{s o o r<> m}{\Abt@{#1}{\Opn@{#1}{\vee\@kw{I}}{orI}}<#4>[#2\@sep #3](#5)}
\NewDocumentCommand{\orEPf}{s o o o m m m m m}{\Abt@{#1}{\Opn@{#1}{\vee\@kw{E}}{orE}}[#2\@sep #3\@sep #4](#5\@sep \A@bs(#6){#7}\@sep \A@bs(#8){#9})}

\NewDocumentCommand{\impProp}{s m m}{\IfBooleanTF{#1}{#2\supset #3}{\A@bt{\O@pn{imp}}(#2\@sep #3)}}
\NewDocumentCommand{\impIPf}{s o o m m}{\Abt@{#1}{\Opn@{#1}{\mathord{\supset}\@kw{I}}{impI}}[#2\@sep #3](\A@bs(#4){#5})}
\NewDocumentCommand{\impEPf}{s o o m m}{\Abt@{#1}{\Opn@{#1}{\mathord{\supset}\@kw{E}}{impE}}[#2\@sep #3](#4\@sep #5)}

\NewDocumentCommand{\notProp}{s m}{\IfBooleanTF{#1}{\neg #2}{\A@bt{\O@pn{not}}(#2)}}
\NewDocumentCommand{\notIPf}{s o m m}{\Abt@{#1}{\Opn@{#1}{\neg\@kw{I}}{notI}}[#2](\A@bs(#3){#4})}
\NewDocumentCommand{\notEPf}{s o m m}{\Abt@{#1}{\Opn@{#1}{\neg\@kw{E}}{notE}}[#2](#3\@sep #4)}

% kinds and constructors
\NewDocumentCommand{\unitKd}{s}{\IfBooleanTF{#1}{\mathbbm{1}}{\A@bt{\O@pn{One}}}}
\NewDocumentCommand{\unitCn}{s}{\IfBooleanTF{#1}{\unitEx*}{\A@bt{\O@pn{triv}}}}
\NewDocumentCommand{\tyKd}{s}{\IfBooleanTF{#1}{\mathbbm{T}}{\A@bt{\O@pn{Ty}}}}
\NewDocumentCommand{\unittyCn}{s}{\O@pn{unit}}
\NewDocumentCommand{\nattyCn}{s}{\O@pn{nat}}
\NewDocumentCommand{\prodtyCn}{s}{\O@pn*{\times}}
\NewDocumentCommand{\arrtyCn}{s}{\O@pn*{\to}}
\NewDocumentCommand{\funKd}{s m o m}{\IfBooleanTF{#1}{\IfValueT{#3}{#3\mathbin{:}}#2\Rightarrow #4}{\A@bt{\O@pn{Fun}}(#2\@sep \IfValueT{#3}{\A@bs(#3)}{#4})}}
\NewDocumentCommand{\lamCn}{s o o o m m}{\Abt@{#1}{\Opn@{#1}{\lambda}{lam}}[#2;\A@bs(#3){#4}](\A@bs(#5){#6})}
\NewDocumentCommand{\appCn}{s o o o m m}{\IfBooleanTF{#1}{#5(#6)}{\A@bt{\O@pn{ap}}[#2\@sep \Abs(#3){#4}](#5\@sep #6)}}
\NewDocumentCommand{\prodKd}{s m o m}{\IfBooleanTF{#1}{\IfValueT{#3}{#3\mathbin{:}}#2\mathbin{\#} #4}{\A@bt{\O@pn{Prod}}(#2\@sep \IfValueT{#3}{\A@bs(#3)}{#4})}}
\NewDocumentCommand{\pairCn}{s o o o m m}{\IfBooleanTF{#1}{\langle #5\@sep #6\rangle}{\A@bt{\O@pn{pair}}[#2\@sep \Abs(#3){#4}](#5\@sep #6)}}
\NewDocumentCommand{\projCn}{s d<> o o o m}{\IfBooleanTF{#1}{#6\cdot #2}{\A@bt{\O@pn{proj}}<#2>[#3\@sep \Abs(#4){#5}](#6)}}

\NewDocumentCommand{\singtyKd}{s m}{\IfBooleanTF{#1}{\mathop{\mathbbm{S}}(#2)}{\A@bt{\O@pn{Eqv}}(#2)}}
\NewDocumentCommand{\eqvtyCn}{s m}{\Abt@{#1}{\O@pn{eqv}}(#2)}
\NewDocumentCommand{\thustyCn}{s m}{\Abt@{#1}{\O@pn{thus}}(#2)}

\NewDocumentCommand{\allkdTy}{s O{\tyKd*} m m}{\A@bt{\Opn@{#1}{\forall}{all}}[#2](\A@bs(#3){#4})}
\NewDocumentCommand{\kLamEx}{s O{\tyKd*} m m}{\A@bt{\Opn@{#1}{\Lambda}{Lam}}[#2](\A@bs(#3){#4})}
\NewDocumentCommand{\kAppEx}{s o o o m m}{\IfBooleanTF{#1}{#5\,[#6]}{\Abt@{#1}{\O@pn{Ap}}[#2\@sep \A@bs(#3){#4}](#5\@sep #6)}}

\NewDocumentCommand{\somekdTy}{s O{\tyKd*} m m}{\A@bt{\Opn@{#1}{\exists}{some}}[#2](\A@bs(#3){#4})}
\NewDocumentCommand{\kpackEx}{s o o o m m}{\Abt@{#1}{\O@pn{pack}}[#2\@sep \A@bs(#3){#4}](#5\@sep #6)}
\NewDocumentCommand{\kopenEx}{s o o o m m m m}{\Abt@{#1}{\O@pn{open}}[#2\@sep \A@bs(#3){#4}](#5\@sep\A@bs(#6,#7){#8})}

\fi % no@syn

\makeatother