macros.tex

\usepackage[hidelinks]{hyperref}
\usepackage{amssymb}
\usepackage{amsmath}

\def\K{\mathsf}
\def\X{\mathit}
\def\F{\mathrm}

\def\subtypeof{\preccurlyeq}
\def\ESUBRESOURCE{\K{resource}}

% TODO: xref properly
\def\name{\X{name}}
\def\tyvar{\alpha}
\def\tyvarb{\beta}
\def\rtidx{\X{rtidx}}
\def\bool{\X{bool}}
\def\true{\K{true}}
\def\false{\K{false}}

\catcode`:=11
\def\core:type{\X{core{:}type}}
\def\core:typeidx{\X{core{:}typeidx}}
\def\core:funcidx{\X{core{:}funcidx}}
\def\core:memidx{\X{core{:}memidx}}
\def\core:functype{\X{core{:}functype}}
\def\core:tabletype{\X{core{:}tabletype}}
\def\core:memtype{\X{core{:}memtype}}
\def\core:globaltype{\X{core{:}globaltype}}
\def\core:import{\X{core{:}import}}
\def\core:importdesc{\X{core{:}importdesc}}
\def\core:module{\X{core{:}module}}
\def\core:IMODULE{\K{module}}
\def\core:ENAME{\K{name}}
\def\core:INAME{\K{name}}
\def\core:EDESC{\K{desc}}
\def\core:IDESC{\K{desc}}

\makeatletter

\protected\def\u{\afterassignment\@u\count255=}
\def\@u{\K{u\the\count255}}
\protected\def\i{\afterassignment\@i\count255=}
\def\@i{\K{i\the\count255}}

\def\setupPCR{\def\production@cr{\global\let\production@cr=\\}}
\def\setupSP{%
  \def\alt{\\&&\mathchar"26A&}%
  \mathcode`|="8000%
  \setupPCR%
}
\catcode`|=13
\def|{~\mathchar"26A~}
\catcode`|=12
\newenvironment{sum-productions}
{\[\setupSP\begin{array}{llcl}}
{\end{array}\]}
\newenvironment{sum-production}[1]
{\begin{sum-productions}\production{#1}}
{\end{sum-productions}}
\def\production#1{\production@cr&\hypertarget{syntax:#1}{\csname#1\endcsname}&::=&}
\newenvironment{record-productions}
{\[\setupPCR\begin{array}{llll}}
{\end{array}\]}
\newenvironment{record-production}[1]
{\begin{record-productions}\production{#1}}
{\end{record-productions}}

\def\defgrammar@#1#2#3{%
  \def\currentprefix{#1}%
  \def\currentgrammar{#2}%
  \expandafter\def\csname#2\endcsname{{\protect\hyperlink{syntax:#2}{#3}}}%
}
\def\defgrammar#1#2{\defgrammar@{#1}{#2}{\X{#2}}}
\def\defconstr@#1#2{%
  \expandafter\uppercase\expandafter{\expandafter\expandafter\expandafter\gdef\expandafter\csname\currentprefix#1}\expandafter\endcsname\expandafter{\expandafter{\expandafter\protect\expandafter\hyperlink\expandafter{\expandafter s\expandafter y\expandafter n\expandafter t\expandafter a\expandafter x\expandafter :\currentgrammar}{#2}}}%
}
\def\defconstr#1{\defconstr@{#1}{\K{#1}}}

\def\defconstrs#1{\@defconstrs#1,,\relax}
\def\@defconstrs#1,#2\relax{\defconstr{#1}\if#2,\expandafter\@firstoftwo\else\expandafter\@secondoftwo\fi{}{\@defconstrs#2\relax}}
\def\defsyntax#1#2#3{\defgrammar{#1}{#2}\defconstrs{#3}}

%%% Surface Type Syntax

\defgrammar{VT}{primvaltype}
\defconstr{bool}
\protected\def\VTS{\afterassignment\@VTS\count255=}
\def\@VTS{\hyperlink{syntax:primvaltype}{\K{s\the\count255}}}
\protected\def\VTU{\afterassignment\@VTU\count255=}
\def\@VTU{\hyperlink{syntax:primvaltype}{\K{u\the\count255}}}
\protected\def\VTFLOAT{\afterassignment\@VTFLOAT\count255=}
\def\@VTFLOAT{\hyperlink{syntax:primvaltype}{\K{float\the\count255}}}
\defconstr{char}
\defconstr{string}

\defgrammar{VT}{defvaltype}
\defconstr{prim}
\defconstr{record}
\defconstr{variant}
\defconstr{list}
\defconstr{tuple}
\defconstr{flags}
\defconstr{enum}
\defconstr{union}
\defconstr{option}
\defconstr{result}
\defconstr{own}
\defconstr{borrow}

\defgrammar{VT}{valtype}

\defgrammar{RF}{recordfield}
\defconstr{name}
\defconstr{type}

\defgrammar{VC}{variantcase}
\defconstr{name}
\defconstr{type}
\defconstr{refines}

\defgrammar{RT}{resourcetype}
\tracingmacros1
\defconstrs{rep,dtor}

\defsyntax{FT}{functype}{params,results}
\defsyntax{PL}{paramlist}{type,name}
\defsyntax{RL}{resultlist}{type,name}

\defsyntax{IT}{instancetype}{}
\defsyntax{ID}{instancedecl}{alias,type,export}
\defsyntax{ED}{externdesc}{type,func,value,instance,component}
\defconstr@{coremodule}{\K{core\_module}}
\defsyntax{TB}{typebound}{eq,subr}
\defsyntax{ED}{exportdecl}{name,desc}

\defsyntax{}{componenttype}{}
\defsyntax{CD}{componentdecl}{import}
\defsyntax{ID}{importdecl}{name,desc}

\defsyntax{}{deftype}{}

\defgrammar@{}{coredeftype}{\X{core{:}deftype}}
\defgrammar@{}{coremoduletype}{\X{core{:}moduletype}}
\defgrammar@{}{coremoduledecl}{\X{core{:}moduledecl}}
\defgrammar@{}{coreimportdecl}{\X{core{:}importdecl}}
\defgrammar@{CA}{corealias}{\X{core{:}alias}}
\defconstrs{sort,target}
\defgrammar@{CAT}{corealiastarget}{\X{core{:}aliastarget}}
\defconstrs{outer}
\defgrammar@{CED}{coreexportdecl}{\X{core{:}exportdecl}}
\defconstrs{name,desc}

%%% Surface Expression Syntax

\defsyntax{S}{sort}{core,func,value,type,component,instance}
\defgrammar@{CS}{coresort}{\X{core{:}sort}}
\defconstrs{instance,module,type,global,memory,table,func}

\defgrammar@{}{coremoduleidx}{\X{core{:}moduleidx}}
\defgrammar@{}{coreinstanceidx}{\X{core{:}instanceidx}}
\defgrammar{}{componentidx}
\defgrammar{}{instanceidx}
\defgrammar{}{funcidx}
\defgrammar@{}{corefuncidx}{\X{core{:}funcidx}}
\defgrammar{}{valueidx}
\defgrammar{}{typeidx}
\defgrammar@{}{coretypeidx}{\X{core{:}typeidx}}

\defgrammar@{CSI}{coresortidx}{\X{core{:}sortidx}}
\defconstrs{sort,idx}
\defsyntax{SI}{sortidx}{sort,idx}

\defsyntax{D}{definition}{component,instance,alias,type,canon,start,import,export}
\defconstr@{coremodule}{\K{core\_module}}
\defconstr@{coreinstance}{\K{core\_instance}}
\defconstr@{coretype}{\K{core\_type}}

\defgrammar@{CI}{coreinstance}{\X{core{:}instance}}
\defconstrs{instantiate,exports}
\defgrammar@{CIA}{coreinstantiatearg}{\X{core{:}instantiatearg}}
\defconstrs{instance,name}
\defgrammar@{CE}{coreexport}{\X{core{:}export}}
\defconstrs{def,name}

\defsyntax{}{component}{}

\defsyntax{I}{instance}{instantiate,exports}
\defsyntax{IA}{instantiatearg}{name,arg}

\defsyntax{A}{alias}{sort,target}
\defsyntax{AT}{aliastarget}{export,outer}
\defconstr@{coreexport}{\K{core\_export}}

\defsyntax{C}{canon}{lift,lower}
\defconstr@{resourcenew}{\K{resource.new}}
\defconstr@{resourcedrop}{\K{resource.drop}}
\defconstr@{resourcerep}{\K{resource.rep}}
\defsyntax{CO}{canonopt}{memory,realloc,postreturn}
\defconstr@{stringencodingUTFEIGHT}{\K{string\_encoding\_utf8}}
\defconstr@{stringencodingUTFSIXTEEN}{\K{string\_encoding\_utf16}}
\defconstr@{stringencodingLATINONEUTFSIXTEEN}{\K{string\_encoding\_latin1{+}utf16}}

\defsyntax{F}{start}{func,args}

\defsyntax{}{import}{}

\defsyntax{E}{export}{name,def,desc}

%%% Elaborated Type Syntax
\def\defesyntax#1#2#3{\defgrammar@{E#1}{e#2}{\X{#2}_e}\defconstrs{#3}}

\def\maybedead{{\rlap{$\mathsurround=0pt\dagger$}?}}

\defesyntax{VT}{valtype}{bool,char,list,record,variant,own,ref}
\protected\def\EVTS{\afterassignment\@EVTS\count255=}
\def\@EVTS{\hyperlink{syntax:evaltype}{\K{s\the\count255}}}
\protected\def\EVTU{\afterassignment\@EVTU\count255=}
\def\@EVTU{\hyperlink{syntax:evaltype}{\K{u\the\count255}}}
\protected\def\EVTFLOAT{\afterassignment\@EVTFLOAT\count255=}
\def\@EVTFLOAT{\hyperlink{syntax:evaltype}{\K{float\the\count255}}}
\defsyntax{RS}{refscope}{call}
\defgrammar@{}{evaltypead}{{\X{valtype}_e^\maybedead}}

\defesyntax{RF}{recordfield}{name,type}
\defesyntax{VC}{variantcase}{name,type,refines}

\defesyntax{RT}{resourcetype}{rep,dtor}

\defesyntax{PL}{paramlist}{name,type}
\defesyntax{RL}{resultlist}{name,type}

\defesyntax{}{functype}{}
\defesyntax{TB}{typebound}{eq,subr}

\defesyntax{}{instancetype}{}
\defsyntax{}{boundedtyvar}{}
\defesyntax{ED}{externdecl}{name,desc}
\defesyntax{EMD}{externdesc}{func,value,type,instance,component}
\defconstr@{coremodule}{\K{core\_module}}
\defgrammar@{}{einstancetypead}{{\X{instancetype}_e^\maybedead}}
\defgrammar@{}{eexterndeclad}{{\X{externdecl}_e^\maybedead}}

\defesyntax{}{componenttype}{}

\defesyntax{DT}{deftype}{resource}

\defgrammar@{}{ecoreinstancetype}{\X{core{:}instancetype}_e}
\defgrammar@{}{ecoremoduletype}{\X{core{:}moduletype}_e}
\defgrammar@{}{ecoredeftype}{\X{core{:}deftype}_e}

%%% Contexts

\defgrammar@{CTC}{coretyctx}{\Gamma_c}
\defconstrs{types,funcs,tables,mems,globals,modules,instances}
\defgrammar@{TC}{tyctx}{\Gamma}
\defconstrs{parent,core,vars,rtypes,types,components,instances,funcs,values}
\defconstr@{ob}{\K{outer\_boundary}}
\defconstr@{ld}{\K{locally\_defined}}

\defsyntax{VCC}{vcctx}{ctx,cases}
\defgrammar@{EVTP}{evaltypepos}{{\pi_v}}
\defconstrs{result,export}
\defgrammar@{EDTP}{edeftypepos}{{\pi_d}}
\defconstr@{export}{extern}

%%% Judgments


\def\vdashh!#1!{\mathrel{\hyperref[judgment:#1]{\vdash}}}
\def\leadstoh!#1!{\mathrel{\hyperref[judgment:#1]{\leadsto}}}
\def\dashvh!#1!{\mathrel{\hyperref[judgment:#1]{\dashv}}}
\def\trelh!#1!{\mathrel{\hyperref[judgment:#1]{:}}}

\def\freeVars#1{\mathop{\F{fv}}(#1)}
\def\subst{\gamma}
\def\resolveVars#1{\mathop{\F{resolve\_vars}}(#1)}
\def\length#1{\lVert#1\rVert}

\def\novalues#1{{}\mathrel{\hyperref[judgment:novalues]{\vdash^\mathsf{\mkern-20mu\neg v}}}{#1}}

%\def\EEDtoCtx#1#2#3#4{{#1} \mathrel{\hyperref[judgment:EEDtoCtx]{\oplus}} {#2} \mathrel{\hyperref[judgment:EEDtoCtx]{=}} {#4} \mathrel{\hyperref[judgment:EEDtoCtx]{@}} {#3}}
%\def\callEITvars#1{\mathop{\hyperref[judgment:EITvars]{\F{unvar\_instance}}}({#1})}
%\def\EITvars#1#2#3{\callEITvars{#1} = \exists {#2}. {#3}}

\makeatother