% $Id: cil.sty,v 1.15 2002/04/05 02:03:50 fturbak Exp $

\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{cil}[1998/10/28 CIL language macros]

\RequirePackage{jbw-math}

% Evaluate sexp on next line in Emacs for outline minor mode with this file.
% (progn(outline-minor-mode 1)(setq outline-regexp "%%%+ "))

% 2/15/99 Lyn: TeX Version 3.1415 (C version 6.1) complains
% that \mathbf is only allowed in math mode
% 
% \newcommand{\kwd}[1]{\mathbf{#1}}
\newcommand{\kwd}[1]{\ensuremath{\mathbf{#1}}}

%%% Additional Symbols %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\DeclareMathSymbol\rightsquigarrow{\mathrel}{AMSa}{"20}
\newcommand{\longtwoheadrightarrow}{\relbar\joinrel\twoheadrightarrow}
 
%%% Language Names %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\lang}{\ensuremath{\lambda^{\mathrm{CIL}}}}
\let\langExp=\lang % ``Exp'' == ``explicit''
\newcommand{\langUnt}{\ensuremath{\lang_{\mathrm{ut}}}} % Untyped language 
\newcommand{\langUnl}{\ensuremath{\lang_{\mathrm{ul}}}} % Unlabelled language 
\newcommand{\langImp}{\ensuremath{\lang_{\mathrm{i}}}}  % Implicitly typed language 
% Synonyms for above 
\newcommand{\langUntyped}{\langUnt} % Untyped language 
\newcommand{\langUnlabelled}{\langUnl} % Unlabelled language 
\newcommand{\langImplicit}{\langImp}  % Implicitly typed language 
\newcommand{\langUnknown}{\ensuremath{\lang_{\mathrm{X}}}}
\newcommand{\langDLO}{\ensuremath{\lang_{\mathrm{DLO}}}}
\newcommand{\langDLS}{\ensuremath{\lang_{\mathrm{DLS}}}}
 
%%% Reduction %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\ReduceOneStepByRedex}[4]%
  {{{#2}\ReduceOneStepByRedexSym{#1}{#4}{#3}}}
\newcommand{\ReduceOneStep}[3]{\ensuremath{{#2}\ReduceOneStepSym{#1}{#3}}}
\newcommand{\ReduceManyStep}[3]{\ensuremath{{#2}\ReduceManyStepSym{#1}{#3}}}
\newcommand{\ReduceToNF}[3]{\ensuremath{{#2}\ReduceToNFSym{#1}{#3}}}
\newcommand{\RedexPair}[3]{\ensuremath{{#2}\RedexPairSym{#1}{#3}}}
\newcommand{\IsInNF}[2]{\ensuremath{\text{$#1$-\textup{nf}}\Parens{#2}}}

\newcommand{\ReduceOneStepSym}[1]{\ensuremath{\longrightarrow_{#1}}}
\newcommand{\ReduceOneStepByRedexSym}[2]{\myxrightarrow{#2}_{#1}}
\newcommand{\ReduceManyStepSym}[1]{\ensuremath{\longtwoheadrightarrow_{#1}}}
\newcommand{\ReduceToNFSym}[1]%
  %{\ensuremath{\longrightarrow_{\text{$#1$-\textup{nf}}}}}
  {\ensuremath{\myxrightarrow{\mathrm{nf}}_{#1}}}
\newcommand{\RedexPairSym}[1]{\ensuremath{\rightsquigarrow_{#1}}}
\newcommand{\ReductionContextSet}[1]{\ensuremath{\mathbf{C}_{#1}}}
\newcommand{\EvaluationContextSet}[1]{\ensuremath{\mathbf{E}_{#1}}}

\newcommand{\MainRel}{\ensuremath{\mathrm r}}
\newcommand{\CompRel}{\ensuremath{\mathrm c}}
\newcommand{\TypeAnnSimpRel}{\ensuremath{\mathrm t}}
%\newcommand{\UntCompRel}{\ensuremath{\hat{c}}}
\newcommand{\UntCompRel}{\ensuremath{\mathrm{ut}}}
\newcommand{\UntEvalRel}{\ensuremath{\hat{\mathrm e}}}
\newcommand{\TypedEvalRel}{\ensuremath{\mathrm e}}
\newcommand{\EvaluationRelation}{\ensuremath{\mathrm{e}}}
\newcommand{\UnlMainRel}{\ensuremath{\tilde{r}}}
\newcommand{\UnlCompRel}{\ensuremath{\tilde{c}}}
\newcommand{\UnlTypeAnnSimpRel}{\ensuremath{\tilde{t}}}

%%% Sets of Pieces of Syntax of Terms/Contexts %%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\ConstantSet}{\ensuremath{\mathbf{Constant}}}
\newcommand{\TermVarSet}{\ensuremath{\mathbf{Variable}}}

\newcommand{\ContextSet}{\ensuremath{\mathbf{Context}}}
\newcommand{\TermSet}{\ensuremath{\mathbf{Term}}}
\newcommand{\ValueSet}{\ensuremath{\mathbf{Value}}}
\newcommand{\ParContextSet}{\ensuremath{\mathbf{ParallelContext}}}
\newcommand{\LabelSet}{\ensuremath{\mathbf{Label}}}
 
\newcommand{\BaseTypeSet}{\ensuremath{\mathbf{BaseType}}}
\newcommand{\TypeVarSet}{\ensuremath{\mathbf{TypeVariable}}}
\newcommand{\OpenTypeSet}{\ensuremath{\mathbf{OpenType}}}
\newcommand{\TypeSet}{\ensuremath{\mathbf{Type}}}

% Untyped Language 
\newcommand{\UntContextSet}{\ensuremath{\mathbf{UntContext}}}
\newcommand{\UntTermSet}{\ensuremath{\mathbf{UntTerm}}}
\newcommand{\UntValueSet}{\ensuremath{\mathbf{UntValue}}}
%\newcommand{\UntEvalContextSet}{\ensuremath{\mathbf{UntEvalContext}}}

\newcommand{\Unt}[1]{\ensuremath{\hat{#1}}}
\newcommand{\UntTerm}[1]{\Unt{#1}}
\newcommand{\UntTermSub}[2]{\ensuremath{\Unt{#1}_{#2}}}

% Unlabelled language
\newcommand{\UnlOpenTypeSet}{\ensuremath{\mathbf{UnlOpenType}}}
\newcommand{\UnlTypeSet}{\ensuremath{\mathbf{UnlType}}}
\newcommand{\UnlContextSet}{\ensuremath{\mathbf{UnlContext}}}
\newcommand{\UnlTermSet}{\ensuremath{\mathbf{UnlTerm}}}
\newcommand{\UnlValueSet}{\ensuremath{\mathbf{UnlValue}}}
%\newcommand{\UnlEvalContextSet}{\ensuremath{\mathbf{UnlEvalContext}}}
\newcommand{\UnlParContextSet}{\ensuremath{\mathbf{UnlParallelContext}}}

\newcommand{\Unl}[1]{\ensuremath{\tilde{#1}}}
\newcommand{\UnlType}[1]{\Unl{#1}}
\newcommand{\UnlTypeSub}[2]{\ensuremath{\Unl{#1}_{#2}}}
\newcommand{\UnlTerm}[1]{\ensuremath{\Unl{#1}}}
\newcommand{\UnlTermSub}[2]{\ensuremath{\Unl{#1}_{#2}}}
\newcommand{\UnlEnv}[1]{\ensuremath{\Unl{#1}}}
\newcommand{\UnlEnvSub}[2]{\ensuremath{\Unl{#1}_{#2}}}

%%% Constants and Variables %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\BaseType}{\ensuremath{o}}
\newcommand{\ConstTypeSym}{\ensuremath{\mathrm{ConstType}}}
\newcommand*{\ConstType}[1]{\ensuremath{\ConstTypeSym\Parens{#1}}}
\newcommand{\Int}{\ensuremath{\mathrm{int}}}
\newcommand{\Bool}{\ensuremath{\mathrm{bool}}}
\newcommand{\Real}{\ensuremath{\mathrm{real}}}
\newcommand{\Word}{\ensuremath{\mathrm{word}}}
\newcommand{\Char}{\ensuremath{\mathrm{char}}}
\newcommand{\Unit}{\ensuremath{\mathrm{unit}}}
\newcommand{\Var}[2]{{#1}^{#2}}
 
%%% Functions and Applications %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\RequirePackage{jbw-arrow}

% Labelled versions
\newcommand*{\LabArrowType}[4]{{#1}\mathbin{\myxrightarrow[#4]{#3}}{#2}}
\let\LabArrow=\LabArrowType
\newcommand{\LabAbs}[5]{\lambda^{#4}_{#5}{\Var{#1}{#2}}.\;{#3}}
\newcommand{\LabApp}[4]{{#1}\;@^{#3}_{#4}\;{#2}}

\newcommand{\LabLam}[2]{\lambda^{#1}_{#2}}
\newcommand{\LabAsp}[2]{@^{#1}_{#2}}

% Unlabelled versions
\newcommand{\ArrowType}[2]{{#1}\mathbin{\to}{#2}}
\newcommand{\Abs}[3]{\lambda{#1}^{#2}.\;{#3}}
\newcommand{\App}[2]{{#1}\;@\;{#2}}

% Untyped versions
\newcommand{\UntAbs}[2]{\lambda{#1}.{#2}}
\newcommand{\UntApp}[2]{\App{#1}{#2}}
 
% Labelled and Marked versions
\newcommand{\MarkedLabAbs}[5]{\bar\lambda{}^{#4}_{#5}{\Var{#1}{#2}}.{#3}}
\newcommand{\MarkedLabApp}[4]{{#1}\;\bar@{}^{#3}_{#4}\;{#2}}

%%% Term and Type Recursion (mu) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\UntTermRecurse}[2]{\ensuremath{\kwd{rec}\ {#1}.{#2}}}
\newcommand{\TermRecurse}[3]{\ensuremath{\kwd{rec}\ {#1}^{#2}.{#3}}}
\newcommand{\TypeRecurse}[2]{\ensuremath{\mu{#1}.{#2}}}
 
%%% Tuple-like Type and Term Syntax %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Auto-resizing versions of the type constructors.
\def\delwedge{%
  % 1: big operator
  % 25E: family 2, char 5E
  % 356: family 3, char 56
  \delimiter"125E356 } 
\def\delvee{%
  % 1: big operator
  % 25F: family 2, char 5F
  % 357: family 3, char 57
  \delimiter"125F357 }

% Need to find larger char codes for + and \times.
%\delcode`+="02B000
%\def\times{\delimiter"1202000 }

\newif\iftesting
\testingfalse

\newcommand{\ResizePrefixOpAux}[4]%
  % TYPE: (box-->mlist)-->mlist-->style-->*-->mlist
  % arg1: a function to compute the prefix.
  %       takes one argument: a box whose height should be used to adjust
  %       the height of the prefix.
  % arg2: stuff to form a math list -- placed after prefix.
  % arg3: a math style command.
  %       arg2 should be typeset in this style.
  % arg4: a dummy argument.
{%
  \setbox0=\hbox{$#3#2$}
  \setbox1=\hbox{}%
\iftesting
  \ht1=\ht0%
  \dp1=\dp0%
  #1{\copy1}\box0%
\else
  \dimen0=\ht0%
  \advance\dimen0 by -2pt%
  \ht1=\dimen0
  \dimen0=\dp0%
  \advance\dimen0 by -2pt%
  \dp1=\dimen0%
  %\dimen0=\fontdimen22\textfont2%
  %\vrule height\ht1 width3pt depth-\dimen0%
  %\vrule height\dimen0 width3pt depth\dp1%
  %\vrule height\fontdimen11\textfont3 width 1pt depth0pt%
  #1{\copy1}\box0%
\fi
}
\newcommand{\ResizePrefixOp}[2]% TYPE: (box-->mlist)-->mlist-->mlist
  % arg1: a function to compute the prefix.
  %       takes one argument: an empty box -- height used to resize the prefix.
  % arg2: stuff to form a math list -- placed after the prefix.
{%
  \mathpalette{\ResizePrefixOpAux{#1}{#2}}{}%
}
\newcommand{\ResizingPrefixBuild}[3]%
  % TYPE: delim-->(mlist-->mlist)-->box-->mlist
  % arg1: resizable prefix char (must have \delcode).
  % arg2: a function to compute the prefix.
  %       takes one argument: a math list with the resized prefix char.
  % arg3: an empty box whose height is used to resize the prefix char.
{%
  #2{\left#1#3\right.\kern-\nulldelimiterspace}%
  \mkern-0.5\thinmuskip
}
\newcommand{\XXXResizingPrefixBuild}[3]%
{%
  %\tracingon
  #2{\XXXResizePrefix
       25,20,17,14,12,11,10,9,8,7,6,5,0,;%
       {#1}{#3}}%
}
\def\XXXResizePrefix#1,#2;#3#4{%
  % TYPE: (list size)-->delim-->box-->mlist
  % arg1 and arg2 are the head and tail of the list.
  % arg3: a command name defined by \mathchardef.
  % arg4: an empty box whose height is used to find a version of arg3 of
  %       the right height.
  {%
    \ifnum#1=0\relax
      % We've reached the end of list, so barf and die.
      \diediedie
    \else
      \setbox2=\hbox{%
                 %\tracingoff
                 \fontsize{#1}{\f@baselineskip}\selectfont
                 $\mathop{#3}{}$%
               }%
      \setbox3=#4%
      \dimen0=\ht2%
      \advance\dimen0 by \dp2%
      \dimen1=\ht3%
      \advance\dimen1 by \dp3%
      %\showthe\dimen0
      %\showthe\dimen1
      \relax
      \ifdim\dimen0>\dimen1\relax
        \let\XYZZY=\relax
        \xdef\XYZZY{%
          \noexpand\XXXResizePrefix#2;{#3}{#4}}%
        \aftergroup\XYZZY
      \else
        \copy2%
      \fi
    \fi
  }%
}
%
\newcommand{\NonResizingPrefixBuild}[2]%
  % arg1: stuff to form a math list (the prefix).
  % arg2: a dummy argument.
  % TYPE: mlist-->*-->mlist
  {\mathord{#1}}
\newcommand{\CompactRangePrefixBuild}[4]%
  % TYPE: mlist-->mlist-->mlist-->mlist-->mlist
  {\mathop{#4}\nolimits_{{#1}={#2}}^{#3}}
\newcommand{\RangeOverSetPrefixBuild}[3]%
  % TYPE: mlist-->mlist-->mlist-->mlist
  {\mathop{#3}\nolimits_{{#1}\in{#2}}}
\newcommand{\RangeOverSequencePrefixBuild}[3]%
  % TYPE: mlist-->mlist-->mlist-->mlist
  {\mathop{#3}\nolimits_{{#1}\text{ \textup{in} }{#2}}}
\newcommand{\ResizingCompactRangePrefix}[4]
  % TYPE: delim-->mlist-->mlist-->mlist-->box-->mlist
{%
  \ResizingPrefixBuild{#1}% delim
                      {\CompactRangePrefixBuild{#2}{#3}{#4}}% mlist-->mlist
}
\newcommand{\ResizingRangeOverSetPrefix}[3]
  % TYPE: delim-->mlist-->mlist-->box-->mlist
{%
  \ResizingPrefixBuild{#1}% delim
                      {\RangeOverSetPrefixBuild{#2}{#3}}% mlist-->mlist
}
\newcommand{\ResizingRangeOverSequencePrefix}[3]
  % TYPE: delim-->mlist-->mlist-->box-->mlist
{%
  \ResizingPrefixBuild{#1}% delim
                      {\RangeOverSequencePrefixBuild{#2}{#3}}% mlist-->mlist
}

\newcommand{\ConBody}[3]% TYPE: delim-->delim-->mlist-->mlist
  % arg1: left delimiter character.
  % arg2: right delimiter character.
  % arg3: stuff to form a math list.
  {\left#1{#3}\right#2}
\newcommand{\ConType}[2]% TYPE: (box-->mlist)-->mlist-->mlist
  {\ResizePrefixOp% (box-->mlist)-->mlist-->mlist
     {#1}{\ConBody[]{#2}}}
\newcommand{\ConTerm}[2]% TYPE: (box-->mlist)-->mlist-->mlist
  {\ResizePrefixOp% (box-->mlist)-->mlist-->mlist
     {#1}{\ConBody(){#2}}}
\newcommand{\ResizingConThingRangeOverSet}[6]
  % TYPE: delim-->delim-->delim-->mlist-->mlist-->mlist-->mlist
  %       tycon   paren   paren   bound    set    body
  {\ResizePrefixOp% (box-->mlist)-->mlist-->mlist
     {\ResizingRangeOverSetPrefix% TYPE: delim-->mlist-->mlist-->box-->mlist
        {#1}{#4}{#5}}% box-->mlist
     {\ConBody#2#3{#6}}}
\newcommand{\ResizingConThingRangeOverSequence}[6]
  % TYPE: delim-->delim-->delim-->mlist-->mlist-->mlist-->mlist
  %       tycon   paren   paren   bound    set    body
  {\ResizePrefixOp% (box-->mlist)-->mlist-->mlist
     {\ResizingRangeOverSequencePrefix%TYPE:delim-->mlist-->mlist-->box-->mlist
        {#1}{#4}{#5}}% box-->mlist
     {\ConBody#2#3{#6}}}
\newcommand{\ResizingConThingCompactRange}[7]
  % TYPE: delim-->delim-->delim-->mlist-->mlist-->mlist-->mlist-->mlist
  %       tycon   paren   paren   bound   lower   upper   body
  {\ResizePrefixOp% (box-->mlist)-->mlist-->mlist
     {\ResizingCompactRangePrefix{#1}{#4}{#5}{#6}}% box-->mlist
     {\ConBody{#2}{#3}{#7}}}
 
%%% Notation Shared Among Product/Intersection/Sum/Union Types %%%%%%%

\newcommand{\Constructor}{Q}
\newcommand{\QPfx}{\NonResizingPrefixBuild{\Constructor}}
\newcommand{\QType}[1]{\ConType{\QPfx}{#1}}

% These two probably shouldn't be used:
\newcommand{\ConstructedType}[2]{\ConType{\NonResizingPrefixBuild{#1}}{#2}}
\newcommand{\ConstructedTypeRange}[5] % Arg #5 is higher-order
           {\ConstructedType{#1}{\IndexedRange{#3}{#4}{#5}}}
 
%%% Product and Intersection Types %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\Productor}{P}
\newcommand{\PPfx}{\NonResizingPrefixBuild{\Productor}}
\newcommand{\PType}[1]{\ConType{\PPfx}{#1}}
\newcommand{\PTerm}[1]{\ConTerm{\PPfx}{#1}}

\newcommand{\IntPfx}% TYPE: box-->mlist
  {\ResizingPrefixBuild% delim-->(mlist-->mlist)-->box-->mlist
     {\delwedge}
     {}% The identity!
  }
\newcommand{\IntType}[1]{\ConType{\IntPfx}{#1}}
\newcommand{\IntTypeCompactRange}[4]% TYPE: mlist*4-->mlist
  {\ResizingConThingCompactRange{\delwedge}{[}{]}{#1}{#2}{#3}{#4}}
\newcommand{\IntTypeRangeOverSet}[3]% TYPE: mlist*3-->mlist
  {\ResizingConThingRangeOverSet{\delwedge}{[}{]}{#1}{#2}{#3}}
\newcommand{\IntTypeRangeOverSequence}[3]% TYPE: mlist*3-->mlist
  {\ResizingConThingRangeOverSequence{\delwedge}{[}{]}{#1}{#2}{#3}}

\newcommand{\IntTerm}[1]{\ConTerm{\IntPfx}{#1}}
\newcommand{\IntTermCompactRange}[4]% TYPE: mlist*4-->mlist
  {\ResizingConThingCompactRange{\delwedge}{(}{)}{#1}{#2}{#3}{#4}}

\newcommand{\ProdPfx}% TYPE: box-->mlist
{%
  \iftesting
    \def\ProdPfxAux{%
      \XXXResizingPrefixBuild% delim-->(mlist-->mlist)-->box-->mlist
        {\times}%
        {}}%
  \else
    \def\ProdPfxAux{%
      \NonResizingPrefixBuild{\times}}%
  \fi
  \ProdPfxAux
}
\newcommand{\ProdType}[1]{\ConType{\ProdPfx}{#1}}
\newcommand{\ProdTerm}[1]{\ConTerm{\ProdPfx}{#1}}

\newcommand{\Proj}[3]{\pi^{#1}_{#2}\,{#3}}
\newcommand{\ProjP}[2]{\Proj{\Productor}{#1}{#2}}
\newcommand{\ProjProd}[2]{\Proj{\times}{#1}{#2}}
\newcommand{\ProjInt}[2]{\Proj{\wedge}{#1}{#2}}
\newcommand{\ProjSym}[2]{\pi^{#1}_{#2}}
\newcommand*{\ProjPSym}[1]{\ProjSym{\Productor}{#1}}
\newcommand*{\ProjIntSym}[1]{\ProjSym{\wedge}{#1}}
\newcommand*{\ProjProdSym}[1]{\ProjSym{\times}{#1}}
 
% Marked versions
\newcommand{\MarkedIntPfx}{\NonResizingPrefixBuild{\bar\wedge}}%
\newcommand{\MarkedIntTerm}[1]{\ConTerm{\MarkedIntPfx}{#1}}
\newcommand{\MarkedProjInt}[2]{\bar{\pi^\wedge}_{#1}\,{#2}}

%%% Sum and Union Types %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\Sumor}{S}
\newcommand{\SPfx}{\NonResizingPrefixBuild{\Sumor}}
\newcommand{\SType}[1]{\ConType{\SPfx}{#1}}

\newcommand{\UnionPfx}% TYPE: box-->mlist
  {\ResizingPrefixBuild% delim-->(mlist-->mlist)-->box-->mlist
     {\delvee}
     {}% The identity!
  }
\newcommand{\UnionType}[1]{\ConType{\UnionPfx}{#1}}
\newcommand{\UnionTypeCompactRange}[4]% TYPE: mlist*4-->mlist
  {\ResizingConThingCompactRange{\delvee}{[}{]}{#1}{#2}{#3}{#4}}
\newcommand{\UnionTypeRangeOverSet}[3]% TYPE: mlist*3-->mlist
  {\ResizingConThingRangeOverSet{\delvee}{[}{]}{#1}{#2}{#3}}
\newcommand{\UnionTypeRangeOverSequence}[3]% TYPE: mlist*3-->mlist
  {\ResizingConThingRangeOverSequence{\delvee}{[}{]}{#1}{#2}{#3}}

\newcommand{\SumPfx}{\NonResizingPrefixBuild{+}}
\newcommand{\SumType}[1]{\ConType{\SumPfx}{#1}}

\newcommand*{\In}[4]{\left(\kwd{in}^{#1}_{#2}\;#4\right)^{#3}}
\newcommand*{\UntIn}[2]{\kwd{in}^+_{#1}{#2}}
\newcommand*{\InSym}[2]{\kwd{in}^{#1}_{#2}}
\newcommand*{\InUnionSym}[1]{\kwd{in}^{\vee}_{#1}}
\newcommand*{\InSumSym}[1]{\kwd{in}^{+}_{#1}}
\newcommand*{\InSSym}[1]{\kwd{in}^{\Sumor}_{#1}}
\newcommand{\InUnion}[3]{\In{\vee}{#1}{#2}{#3}}
\newcommand{\InSum}[3]{\In{+}{#1}{#2}{#3}}
\newcommand{\InS}[3]{\In{\Sumor}{#1}{#2}{#3}}
\newcommand{\CaseClause}[2]{{#1}\Rightarrow{#2}}
\newcommand{\CaseClauseSub}[1]{\CaseClause{\Tausub{#1}}{\Msub{#1}}}
\newcommand{\GenCaseClauseSub}[3]{\CaseClause{#1_{#3}}{#2_{#3}}}
\newcommand{\Case}[4]{\kwd{case}^{#1}\,{#2}\;\kwd{bind}\;{#3}\;\kwd{in}\;{#4}}
\newcommand{\CaseUnion}[3]{\Case{\vee}{#1}{#2}{#3}}
\newcommand{\CaseSum}[3]{\Case{+}{#1}{#2}{#3}}
\newcommand{\CaseS}[3]{\Case{\Sumor}{#1}{#2}{#3}}
\newcommand{\CaseClauseSubErased}[1]
           {\TypeErasure{\Msub{#1}}}
\newcommand{\CaseSym}[1]{\ensuremath{\kwd{case}^{#1}}}
\newcommand{\CaseUnionSym}{\CaseSym{\vee}}
\newcommand{\CaseSumSym}{\CaseSym{+}}
\newcommand{\CaseSSym}{\CaseSym{\Sumor}}
 
% Marked versions
\newcommand*{\MarkedCase}[4]%
  {\bar\kwd{case}^{#1}\,{#2}\;\kwd{bind}\;{#3}\;\kwd{in}\;{#4}}
\newcommand*{\MarkedCaseUnion}[3]{\MarkedCase{\vee}{#1}{#2}{#3}}
\newcommand*{\MarkedIn}[4]{\left(\bar\kwd{in}^{#1}_{#2}\;#4\right)^{#3}}
\newcommand*{\MarkedInUnion}[3]{\MarkedIn{\vee}{#1}{#2}{#3}}

%%% Flow-Label Subtyping %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\Coerce}[3]{\ensuremath{\kwd{coerce}\left({#1},{#2}\right)#3}}
\newcommand{\SubtypeSym}{\ensuremath{\leq}}
\newcommand{\Subtype}[2]{\ensuremath{{#1}\SubtypeSym{#2}}}
\newcommand{\NotSubtypeSym}{\ensuremath{\nleq}}
\newcommand{\NotSubtype}[2]{\ensuremath{{#1}\NotSubtypeSym{#2}}}

%%% Syntactic Sugar %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Records (syntactic sugar for products)
% (not currently in use)

\newcommand{\RecordLabel}[1]{l_{#1}}
\newcommand{\RecordFieldType}[2]{{#1}:{#2}}
\newcommand{\RecordType}[1]{\left\{{#1}\right\}}
\newcommand{\RecordTypeRange}[5] % Args #4 & #5 are higher-order
                                 % Arg #1 (index variable) is ignored here
           {\RecordType{\Range{\RecordFieldType{#4{#2}}{#5{#2}}}
                              {\RecordFieldType{#4{#3}}{#5{#3}}}}}
\newcommand{\RecordField}[2]{{#1}={#2}}
\newcommand{\Record}[1]{\left\{{#1}\right\}}
\newcommand{\RecordSelector}[1]{\#{#1}}
 
% let and letrec (syntactic sugar for beta-redex and mu)

\newcommand{\UntLet}[3]{\kwd{let}\ {#1}={#2}\ \kwd{in}\ {#3}}
\let\Let=\UntLet
\newcommand*{\TypLet}[4]{\kwd{let}\ \Var{#1}{#2}={#3}\ \kwd{in}\ {#4}}
\newcommand{\LetRec}[3]{\kwd{letrec}\ {#1}={#2}\ \kwd{in}\ {#3}}

% if-then-else (syntactic sugar for sum/case)

\newcommand{\UnitTypeSugar}{\ProdType{\ }}
\newcommand{\UnitValueSugar}{\Prod{\,}}

\newcommand{\If}[3]{\kwd{if}~{#1}~\kwd{then}~{#2}~\kwd{else}~{#3}}
\newcommand{\True}{\ensuremath{\mathrm{true}}}
\newcommand{\False}{\ensuremath{\mathrm{false}}}
\newcommand{\truth}{\ensuremath{\mathrm{true}}}
\newcommand{\falsity}{\ensuremath{\mathrm{false}}}

%%% General Term/Type Notation %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand*{\Subst}[3]{\ensuremath{{#3}\Bracks{{#2}{:}{=}{#1}}}}
\newcommand*{\SubstForIn}[3]{\Subst{#1}{#2}{#3}}

% \newcommand{\OccursInNotEqSym}{\lhd}
\newcommand{\OccursInNotEqSym}{\vartriangleleft}
\newcommand{\OccursInNotEq}[2]{{#1}\OccursInNotEqSym{#2}}
% \newcommand{\OccursInOrEqSym}{\unlhd}
\newcommand{\OccursInOrEqSym}{\trianglelefteq}
\newcommand{\OccursInOrEq}[2]{{#1}\OccursInOrEqSym{#2}}

\newcommand{\NeitherOccursInNorEqSym}{\mathrel{\ntrianglelefteq}}
\newcommand{\NeitherOccursInNorEq}[2]{{#1}\NeitherOccursInNorEqSym{#2}}

\newcommand{\SubtermNotEqSym}{\OccursInNotEqSym}
\newcommand{\SubtermNotEq}[2]{\OccursInNotEq{#1}{#2}}
\newcommand{\SubtermOrEqSym}{\OccursInOrEqSym}
\newcommand{\SubtermOrEq}[2]{\OccursInOrEq{#1}{#2}}
\newcommand{\NotSubtermOrEqSym}{\NeitherOccursInNorEqSym}
\newcommand{\NotSubtermOrEq}[2]{\NeitherOccursInNorEq{#1}{#2}}

\newcommand{\SameTerm}[2]{{#1}\equiv{#2}}
\newcommand{\SameTermSym}{\equiv}
\newcommand{\NotSameTerm}[2]{{#1}\not\equiv{#2}}
\newcommand{\NotSameTermSym}{\nequiv}

\newcommand{\TypeErasure}[1]{\ensuremath{\left\vert{#1}\right\vert}}
\newcommand{\LabelErasure}[1]{\ensuremath{\left\langle{#1}\right\rangle}}

\newcommand{\LabelInsertion}[1]{\ensuremath{\left\lceil{#1}\right\rceil}}
\newcommand{\UnitLabel}{\ensuremath{\bullet}} % Distinguished label
\newcommand{\UnitLabelSet}{\ensuremath{\Set{\UnitLabel}}} % Distinguished source label set

\newcommand*{\FreeVars}[1]{\ensuremath{\mathrm{FV}\Parens{#1}}}
\newcommand*{\FreeTypeVars}[1]{\FreeVars{#1}}
 
%%% Systems of Rules and Derivations in these Systems %%%%%%%%%%%%%%%%

\newcommand{\TypeRuleConst}{\RuleLabel{const}}
\newcommand{\TypeRuleVar}{\RuleLabel{var}}
\newcommand{\TypeRuleArrowIntro}{\RuleLabel{$\rightarrow$ intro}}
\newcommand{\TypeRuleArrowElim}{\RuleLabel{$\rightarrow$ elim}}
\newcommand{\TypeRuleProdIntro}{\RuleLabel{$\times$ intro}}
\newcommand{\TypeRuleInterIntro}{\RuleLabel{$\wedge$ intro}}
\newcommand{\TypeRuleProdElim}{\RuleLabel{$\times{,}\wedge$ elim}}
\newcommand{\TypeRuleSumIntro}{\RuleLabel{$+{,}\vee$ intro}}
\newcommand{\TypeRuleSumElim}{\RuleLabel{$+$ elim}}
\newcommand{\TypeRuleUnionIntro}{\RuleLabel{$\vee$ intro}}
\newcommand{\TypeRuleUnionElim}{\RuleLabel{$\vee$ elim}}
\newcommand{\TypeRuleCoerce}{\RuleLabel{coerce}}
% \newcommand{\TypeRuleTermRecurse}{\RuleLabel{recurse}}
% Lyn changed ``recurse'' to ``rec'' because there is no word ``recurse''
% (it's ``recur''). Also, ``rec'' is shorter. 
\newcommand{\TypeRuleTermRecurse}{\RuleLabel{rec}}
\newcommand{\TypeRuleLet}{\RuleLabel{let}}

\newcommand{\TypeEnvExtend}[3]{{#1},{#2}{:}\mkern 1mu{#3}}
\newcommand{\RuleLabel}[1]{\ensuremath{\Parens{\text{#1}}}}

%%% Definitions for Uniqueness of typings theorem %%%%%%%%%%%%%%%%%%%%

\newcommand{\EnvPlus}{\ensuremath{\oplus}}
\newcommand{\EnvMinus}{\ensuremath{\ominus}}
\newcommand{\EnvironSym}{\ensuremath{\mathrm{Env}}}
\newcommand*{\Environ}[1]{\ensuremath{\EnvironSym\Parens{#1}}}
\newcommand{\TypSym}{\ensuremath{\mathrm{Typ}}}
\newcommand{\Typ}[1]{\ensuremath{\TypSym\Parens{#1}}}
 
%%% Pieces of a Fixed Term in SDL Form %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\newcommand{\fv}[2]{\ensuremath{\mathrm{fv}\Parens{{#1},{#2}}}}
\newcommand{\numfv}[2]{\ensuremath{\mathrm{\#fv}\Parens{{#1},{#2}}}}
\newcommand{\fvi}[3]{\ensuremath{\mathrm{fv}_{#1}\Parens{{#2},{#3}}}}
\newcommand{\bv}[2]{\ensuremath{\mathrm{bv}\Parens{#1,#2}}}
\newcommand{\body}[2]{\ensuremath{\mathrm{body}\Parens{#1,#2}}}

\newcommand{\varname}[1]{\ensuremath{\mathrm{name}\Parens{#1}}}
\newcommand{\vartype}[1]{\ensuremath{\mathrm{type}\Parens{#1}}}

\newcommand{\inlinedinqSym}{\ensuremath{\mathrm{inlinedin?}}}
\newcommand*{\inlinedinq}[3]%
  {\ensuremath{\inlinedinqSym\Parens{{#1},{#2},{#3}}}}
\newcommand{\inliningatdepthSym}{\ensuremath{\mathrm{inliningatdepth?}}}
\newcommand*{\inliningatdepth}[4]%
  {\ensuremath{\inliningatdepthSym\Parens{{#1},{#2},{#3},{#4}}}}

%%% Source/Sink Flow Paths and Flow Path Sets %%%%%%%%%%%%%%%%%%%%%%%%

% Commonly used flows
\newcommand{\flowstackaux}[2]{{\ifx#1\displaystyle\textstyle\fi#2}}
\newcommand{\flowstack}[2]{\mathpalette\flowstackaux{{}^{#1}_{#2}}}
\newcommand{\phipsi}{\flowstack{\phi}{\psi}}
\newcommand{\lpsi}{\flowstack{l}{\psi}}
\newcommand{\phik}{\flowstack{\phi}{k}}
\newcommand{\lk}{\flowstack{l}{k}}
\newcommand{\lkp}{\flowstack{l'}{k'}}
\newcommand*{\lki}[1]{\flowstack{l_{#1}}{k_{#1}}}

%%% Name macros %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% name of the CIL compiler intermediate langauge
\newcommand{\cil}{CIL \ }
\newcommand{\cilfull}{Church \ intermediate \ language \ }
% name of the CIL compiler
\newcommand{\cilc}{CILc \ }
\newcommand{\cilcfull}{\cil \ compiler \ }
\newcommand{\cilcfullSML}{\cilcfull \ for \ Standard \ ML \ }
 
%%% Emacs File-Local Variables %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Local variables:
% outline-regexp: "%%%+ "
% end:
