% LaTeX Macros for math 

\message{mymath.sty; Mitchell Wand Wed Jan  3 12:47:34 2001}

\RequirePackage{alltt}
\RequirePackage{xspace}
\RequirePackage{psfig}
\RequirePackage{epsf}

%%%%%%%%%%%%%%%% Fonts: for compatibility with eopl.sty  %%%%%%%%%%%%%%%%

%%% Most of these should be obsolete.

\def\f#1{\hbox{\tt #1}}
\def\ff{\tt}                    % may need fancier defs from eopl.sty
\def\breakf{\tt}                % can be the same if no \hbox on \f.

\def\ttbox#1{\hbox{\tt #1}}

%%%%%%%%%%%%%%%% obsolescent and deprecated commands %%%%%%%%%%%%%%%%

\def\eqalign#1{{\def\cr{\\}\begin{array}{r@{{}}l}#1\end{array}}}

% '~' is used as a tie in text and to separate parts of terms in math mode
\def~{\relax\ifmmode \mskip\thinmuskip \else \penalty10000 \ \fi}
% This is now deprecated. mw Thu Aug 13 15:39:21 1998

% deprecated, should use \ensuremath instead
% \def\forcemath#1{\relax\ifmmode #1 \else $#1$ \fi}

%%%%%%%%%%%%%%%% characters %%%%%%%%%%%%%%%%


\def\til{{\tt\char'176}}  % \tt tilde
\def\bs{{\tt\char'134}} % \tt backslashes

\def\hash{{\tt\char'043}} % \tt hash
\def\hasht{{\tt \hash t}}
\def\hashf{{\tt \hash f}}

\def\lbr{{\tt \char'173}} % \tt braces
\def\rbr{{\tt \char'175}}

%%%%%%%%%%%%%%%% Math Mode %%%%%%%%%%%%%%%%

% Like \ensuremath, only better
\newcommand{\ma}[1]{\ensuremath{#1}\xspace}

% use \mdef for 0-arg macros that are smart enough to go into mathmode without
% your telling them to.

\def\mdef#1#2{\def#1{\ma{#2}}}

%% these should be generated by a single abstraction
\def\rmop#1{\ma{\mathop{\hbox{\rm #1\/}}\nolimits}}
\def\itop#1{\ma{\mathop{\hbox{\it #1\/}}\nolimits}}
\def\ttop#1{\ma{\mathop{\hbox{\tt #1\/}}\nolimits}}

%% as should these
\def\itord#1{\ma{\mathord{\hbox{\it #1\/}}}}
\def\rmord#1{\ma{\mathord{\hbox{\rm #1\/}}}}
\def\ttord#1{\ma{\mathord{\hbox{\tt #1\/}}}}


\mdef\car{\rmop{car}}
\mdef\cdr{\rmop{cdr}}
\mdef\cons{\rmop{cons}}
\mdef\a{\alpha}
\mdef\b{\beta}
\mdef\g{\gamma}
\mdef\r{\rho}
\mdef\l{\lambda}
\mdef\G{\Gamma}
\mdef\s{\sigma}

\def\setof#1{\ensuremath{\{#1\}}}

\def\semfcn#1#2{\mathop{#1}\nolimits\lbrack\!\lbrack{#2}\rbrack\!\rbrack}

%%%%%%%%%%%%%%%% Grammars %%%%%%%%%%%%%%%%

% From eopl.sty

% basic components:

% nonterminal names default to roman, even in theorems.
\def\nt#1{\hbox{$\langle\hbox{\rm #1\/}\rangle$}}
\def\term#1{\hbox{\tt #1}}      % I usually put \, before and after the hbox.
\def\lparen{\term{(}}
\def\rparen{\term{)}}
\def\alt{~~\vert~~}

% Kleene star, plus

\def\st#1{\ensuremath{\{#1\}^*}}
\def\pl#1{\ensuremath{\{#1\}^+}}
\def\seplist#1#2{\ensuremath{\{#1\}^{*({#2})}}}
\def\pst#1{\term(\st{#1}\term)}


%% There will be exactly one grammar environment, it will be called
%% grammar, and it will behave like gramalign: it will automatically generate
%% a ::= for each entry.

%% It will normally live inside
%% displaymath.  It has 3 fields:  lll .  The 3th field is for commentary.
%% Alas, Latex does not have a good way of automatically switching modes on a
%% per-field basis, so you'll have to put in $...$ around text-mode stuff,or
%% $|...|$ around tt-mode stuff.

\newenvironment{grammar}{\begin{array}{l@{{}::={}}l@{\quad}l}}{\end{array}}


% rhs for multiline production:  This is like a little array that can be used
% for a production that spans multiple lines, as in:
%
% &\multilineproduction{
%         \term{simpleclass}\ \nt{varlist}\ \nt{varlist}\ \nt{methdecls}\
%                 \nt{exp} \\  
%         \quad $|new-simpleclass (c-vars i-vars methdecls init-exp)|$ } \\
%% but see \production, below, for preferred entry point

\def\multilineproduction#1{\multicolumn{2}{@{}l}{\begin{array}[t]{@{}l}#1\end{array}}}

%%  Just say \asyntax{foo (bar baz)}
%% the raisebox parameter determines how much extra space there will
%% be after the production.  You can fiddle with 
\def\asyntax#1{\quad\vphantom{\raisebox{-8pt}{\mathstrut}}\relax
               \setlength{\fboxsep}{1.9pt}\relax    % default is 3.0pt
               \setlength{\fboxrule}{0.20pt}\relax  % default is 0.4pt
               \fbox{\f{#1}}} 

% this will take care of most productions with abstract syntax
% example:
% \production{\nt{expression}}{\nt{number}}{lit (datum)} \\
% the first argument can be empty.
\def\production#1#2#3{{#1} &\multilineproduction{\f{#2} \\ \asyntax{#3}}}
% for simple productions, no abstract syntax
\def\simpleproduction#1#2{{#1} & \f{#2}}



%% for compatibility
\newcommand\gramalign[1]{\begin{grammar}#1\end{grammar}}


%%%% Example:

% $$
% \begin{grammar}
% \production{\nt{program}}{\nt{expression}}{a-program (exp)}\\
% \production{\nt{expression}}{\nt{number}}{lit-exp (datum)} \\
% \production{}{true}{true-exp}\\
% \production{}{false}{false-exp}\\
% \production{}{\nt{identifier}}{var-exp (id)}\\
% \production{}{\nt{primitive} (\seplist{\nt{expression}}{\term,})}
%              {primapp-exp (prim rands)}\\
% \production{}
%         {if \nt{expression} then \nt{expression} else \nt{expression}}
%         {if-exp (test-exp true-exp false-exp)} \\
% \production{}{proc (\seplist{\nt{identifier}}{\term,}) \nt{expression}}
%                         {proc-exp (ids body)}\\
% \production{}{(\nt{expression} \st{\nt{expression}})}{app-exp (rator rands)}\\
% \nt{primitive} &\term+ \alt \term- \alt \f* \alt \term{add1} \alt
% \term{sub1} \alt \f{zero?}
% \end{grammar}
% $$



%%%%%%%%%%%%%%%% Domains %%%%%%%%%%%%%%%%

\def\newdom#1#2{\mdef#1{\mathop{\hbox{{#2}}}\nolimits\xspace}}
\newdom\expval{Expressed Value}
\newdom\denval{Denoted Value}
\newdom\num{Number}
\newdom\proc{Procedure}
\newdom\primproc{Primitive Procedure}
\newdom\closure{Closure}
\newdom\cell{Cell}
\newdom\location{Ref}
\newdom\bool{Bool}
\newdom\procval{ProcVal}
\newdom\Ans{Ans}
\newdom\comp{Comp}


%%%%%%%%%%%%%%%% Misc %%%%%%%%%%%%%%%%

% for comments (Note \par)
\def\cmt#1\par{$\lbrack\!\lbrack$ #1 $\rbrack\!\rbrack$\par}


\def\eqalign#1{{\def\cr{\\}\begin{array}{r@{{}}l}#1\end{array}}}

%% for representation
\def\uc#1{{\lceil {#1} \rceil}}

\def\diagram#1{\centerline{\epsffile{\diagramdirectory/#1}}}

%% for subscripts in alltt
\def\sub#1{\ensuremath{{}_{#1}}}

%%%%%%%%%%%%%%%% Operational Semantics %%%%%%%%%%%%%%%%

%%% judgements and stuff

\def\Rj#1#2#3{\ma{{\mit #1}\vdash{#2}\Rightarrow{#3}}}

\def\Dj#1#2#3{\ma{{#1}\vdash{#2}\Downarrow{#3}}}

\def\Dji#1#2#3{\ma{{\mit #1}\vdash{#2}\Downarrow{#3}}}

\def\ej#1#2#3{\Dj{#1}{\f{#2}}{\f{#3}}}

\def\primj#1#2#3{\Dj{\rmop{primapp}}{\f{(#1,#2)}}{\f{#3}}}

\def\append{\mathbin{@}}

\mdef\alt{~~\vert~~}

% Sample use of rules, etc.  Note the use of macros for whatever
% syntax will appear in the judgements.

% \def\rj#1{\Rj{\hbox{\rm #1}}}
% \def\rjs{\rj{subtree}}

% \def\atree{\ttop{a-tree}}
% \def\rednode#1#2{(\ttop{red-node}\ #1\ #2)}
% \def\leaf#1{(\ttop{a-leaf}\ #1)}

% $$\rj{subtree}{(s, 0)}{s'}
% \over
% \rj{tree}{(\atree\ s)}{(\atree\ s')}
% $$

% $${}
% \over
% \rj{subtree}{((\ttop{leaf}\ d), n)}{(\ttop{leaf} n)}
% $$

% $$
% \rjs{(s_1, n+1)}{s_1'}  \qquad \rjs{(s_2, n+1)}{s_2'}
% \over
% \rjs{((\ttop{red-node}\ s_1\ s_2),n)}{(\ttop{red-node}\ s_1'\ s_2')}
% $$

% $$
% \rjs{(s_1, n)}{s_1'} \dots
% \over
% \rjs{(\ttop{blue-node} (s_1 \dots), n)}{(\ttop{blue-node} (s_1' \dots))}
% $$

%%%% Another example:

% $$
% \begin{array}l
%   \ej{\r}{$e_1$}{$v_1$}\\ \vdots\\ \ej{\r}{$e_n$}{$v_n$} \\
%   \primj{$p$}{$(v_1, \dots, v_n)$}{$w$}
% \end{array}
% \over
% \ej{\r}{(prim-app $p$ $(e_1, \dots, e_n)$)}{$w$}
% $$