% program.sty: a LaTeX style file for typesetting algorithms.
% Copyright (C) 1991 Martin Ward
%
% This program is free software; you can redistribute it and/or modify
% it under the terms of the GNU General Public License as published by
% the Free Software Foundation.
%
% This is the "program" style option which sets up the
% program and programbox environments,
% keywords for programs and a few goodies.
% NOTE: Within the program environment:
% (1) Newlines are significant.
% (2) Each line is in math mode, so for example spaces in the input
%     file are not significant.
% (3) \\ within a line causes a linebreak in the output.
%
% We also define a "programbox" environment which typesets a program in a box.
% Useful for keeping a piece of code on one page or for typesetting small
% programs in running text.
% We also redefine \( and \) as \begin{programbox} and \end{programbox}.
% The \tab and \untab commands are defined to have no effect while outside
% a program environment, hence a single-line program can be typeset in
% maths mode without the overhead associated with programbox.

\def\@tabcommandson{% activate tabbing commands:
    % \tab sets a tab stop and adds one to the margin tab:
    \def\tab{$\=\+$}
    % Must finish current field before testing if at margin:
    \def\@finishfield{\@stopfield\@addfield\@startfield}
    % \untab removes one tab stop and moves left if at the beginning of a line:
    \def\untab{$\@finishfield\@ifatmargin\@ltab\else\relax\fi\-$}
    % \@marginspace adds an extra space unless there is no text on the line:
    \def\@marginspace{$\@finishfield$\@ifatmargin\relax\else\ \fi}
    % \rcomment{...} provides a comment flush to the right margin:
    \def\rcomment##1{$\`##1$}
    % else has the same width as then and lines up with it on right:
    \def\ELSE{\@marginspace
	     \@ifatmargin
	       \llap{\keyword{else}\ }%
	     \else \keyword{else}\ \fi}
    % Alternative else lines up with then on the left:
    % \def\ELSE{\@marginspace
    %              \@ifatmargin
    %                \llap{\rlap{\keyword{else}}\phantom{\keyword{then}}\ }%
    %              \else \keyword{else}\ \fi}
    % bar lines up on right with if or do keyword:
    \def\BAR{\@marginspace\untab
	   \@ifatmargin
	       \llap{$\barsymbol\ $}%
	   \else \barsymbol\ \fi}
    % ditto \join symbol:
    \def\join{\@marginspace
	   \@ifatmargin
	       \llap{$\sqcup\ $}%
	   \else \sqcup\ \fi}
    % and \choice:
    \def\choice{\@marginspace
	   \@ifatmargin
	       \llap{$\sqcap\ $}%
	   \else \sqcap\ \fi}
    % \EQ puts more space around symbol in program environment:
    \def\EQ{\ \equiv \ \tab}
    % \BEGIN, \REP and \ACTIONEQ make sure next statement starts on a new line
    % with one quad of indentation:
    \def\BEGIN##1{\keyword{begin}\ ##1\\\quad\tab$\kill$\@gobblecr}
    \def\REP##1{\keyword{rep}\ ##1\\\quad\tab$\kill$\@gobblecr}
    \def\ACTIONEQ{\ \equiv{}\\\quad\tab$\kill$\@gobblecr}}

\def\@tabcommandsoff{% deactivate tabbing commands:
    \let\tab=\relax
    \let\@finishfield=\relax
    \let\untab=\relax
    \let\@marginspace=\ % never at margin thus always a space
    \def\rcomment##1{\qquad\mbox{##1}}
    % else has the same width as then and lines up with it on right:
    \def\ELSE{\ \keyword{else}\ }
    % bar lines up on right with if or do keyword:
    \def\BAR{\mathrel{\>\barsymbol\>}}
    \def\join{\sqcup}
    \def\choice{\sqcap}
    \def\EQ{\equiv\tab}
    \def\ACTIONEQ{\equiv}
    \def\BEGIN{\keyword{begin}\ }
    \def\REP{\keyword{rep}\ }}

% default is tab commands deactivated:
\@tabcommandsoff

% define \normalshape if not present:
\@ifundefined{normalshape}
  {\def\normalshape{\rm}}
  {\relax}

% Underline through descenders:
\let\undertext=\underbar
%\def\undertext#1{\ifmmode\underline{\smash{\mbox{#1}}}\else
%			$\underline{\smash{\mbox{#1}}}$\fi}
% Underline below all descenders:
\def\lowundertext#1{\ifmmode\underline{\vphantom{y}\mbox{#1}}\else
			    $\underline{\vphantom{y}\mbox{#1}}$\fi}


% range dots, like \ldots but with two dots only (for 1..n etc.):
\def\rdots{\mathinner{\ldotp\ldotp}}

% Variable name style (works in any mode):
\def\variable#1{\ifmmode\mbox{\sl #1}\else\slant{#1}\fi}
% If \slant is available (from ital.sty) use it to add italic corrections
% automatically, otherwise use {\sl ...}:
\@ifundefined{slant}
  {\def\slant#1{{\sl #1}}}
  {}

% Keyword style (works in any mode):
\@ifundefined{family}
  {\def\keyword#1{\mbox{\underbar{\bf #1}}}}
  {\def\keyword#1{\mbox{\underbar%
		       {\family{cmr}\series{bx}\shape{n}\selectfont #1}}}}

% Definitions for bold subscripted symbols, eg:
%  \B1  or \B{}  or  \B{12}  or \B x  ... etc.
% We check for ' so \B', \S''' etc will work as expected.
\def\A{\boldsub{A}}
\def\B{\boldsub{B}}
\def\Q{\boldsub{Q}}
\def\R{\boldsub{R}}
\def\S{\boldsub{S}}
\def\T{\boldsub{T}}
\def\Z{\boldsub{Z}}

\newif\ifMmode \Mmodefalse

\@ifundefined{family}
  {\def\boldvar#1{{\mbox{\bf #1}}}}
  {\def\boldvar#1{{\text{\family{cmr}\series{bx}\shape{n}\selectfont #1}}}}

\@ifundefined{family}
{% No font selection:
  \def\boldsub#1{%
    \relax% to fool array and other alignments
    \ifmmode
      \Mmodetrue
    \else
      $\Mmodefalse
    \fi
   \mbox{\bf #1}%
   \@boldsub
  }
}{% With font selection:
  \def\boldsub#1{%
    \relax% to fool array and other alignments
    \ifmmode
      \Mmodetrue
    \else
      $\Mmodefalse
    \fi
    \text{\family{cmr}\series{bx}\shape{n}\selectfont #1}%
    \@boldsub
  }
}

   % Use \mathchoice (typesets all 4) if this is needed for
   % subscripts or superscripts (costs ^0.5 seconds per symbol!):
   % NB use of \text should fix this with AMSLaTeX.
   %\mathchoice{\mbox{\series{bx}\shape{n}\selectfont #1}}%
   %           {\mbox{\series{bx}\shape{n}\selectfont #1}}%
   %           {\mbox{\normalshape\bf\scriptsize #1}}%
   %           {\mbox{\normalshape\bf\tiny #1}}%

\def\@nothing{} \def\@prime{'}
\def\@boldsub#1{%
   \def\@boldsubthing{#1}% subscript
   \ifx\@boldsubthing\@nothing% empty
      \let\@boldsubnext\@boldsubfinish
   \else
      \ifx\@boldsubthing\@prime%
	 \def\@boldsubnext{»\bgroup\prime\@absorbprimes}%
      \else
	 \def\@boldsubnext{_{#1}\@boldsubfinish}\fi
   \fi
   \@boldsubnext
}


\def\@absorbprimes{\futurelet\@boldsubnext\@seeifprime}
\def\@seeifprime{%
   \ifx\@boldsubnext'%
      \def\@boldsubnext{\@getprime}%
   \else
      \def\@boldsubnext{\egroup\@boldsubfinish}%
   \fi
   \@boldsubnext
}
\def\@getprime'{\prime\@absorbprimes}
\def\@boldsubfinish{\ifMmode\else$\fi}


% The Boolean values:
\def\true{\boldvar{true}}
\def\false{\boldvar{false}}

% The simple programs:
\def\ABORT{\boldvar{abort}}
\def\SKIP{\boldvar{skip}}
\def\NULL{\boldvar{null}}

% An abbreviation:
\def\aeq{\ACTIONEQ}

% Notation for sets of the form {...|...} :
% Eg: \set{x \in N | x>0}  becomes:
% \left\{\left.\,  x \in N \:\right\origbar\: x>0 \,\right\}
% set brackets and | grow to fit the size if their contents.
% Also: \bigset{...|...} becomes:
%                        \bigl\{\, ... \mathrel{\bigm\origbar} ... \, \bigr\}
\catcode`\|=\active
\def\set#1{\@set#1\@end} % strip of the {} and pass to \@set
\def\@set#1|#2\@end{ \left\{\left.\,#1
	\:\right\origbar\:
	#2 \,\right\} }
\def\bigset#1{\@bigset#1\@end} % strip of the {} and pass to \@bigset
\def\@bigset#1|#2\@end{ \bigl\{\,  #1 \mathrel{\bigm\origbar} #2 \,\bigr\} }
\catcode`\|=12\relax

% Notation for a sequence in variable-sized angle brackets:
% \bigseq uses big size of brackets:
\def\seq#1{\left< #1 \right>}
\def\bigseq#1{\bigl< #1 \bigr>}

% Atomic Specification statement: for eg <x>/<y>.Q use: \atspec x/y. Q
% This uses "/" and "." as argument delimiters:
\def\atspec #1/#2.{\seq{#1}\!/\!\seq{#2}\!.}

% \Forall vars.formula and \Exists vars.formula:
\def\Forall#1.{\forall #1.\,}
\def\Exists#1.{\exists #1.\,}

% The keywords.

\def\IF{\keyword{if}\ \tab}
\def\THEN{\@marginspace\keyword{then}\ \tab}
% \ELSE changes depending if we are in program environment
% elsf lines up with the if:
\def\ELSF{\@marginspace\untab\untab\keyword{elsf}\ \tab}
\def\ELSIF{\@marginspace\untab\untab\keyword{elsif}\ \tab}
\def\FI{\@marginspace\untab\untab\keyword{fi}}
% \AR is the arrow for Dijkstra if and do:
\def\AR{\@marginspace\rightarrow\ \tab}
\def\DO{\keyword{do}\ \tab}
\let\@oldDO=\DO
\def\OD{\@marginspace\untab\keyword{od}}
% \WHILE and \FOR temporarily change \DO to not set a tab:
\def\WHILE{\keyword{while}\ \tab
	   \gdef\DO{\@marginspace\keyword{do}\ \global\let\DO=\@oldDO}}
\def\FOR{\keyword{for}\ \tab
	   \gdef\DO{\@marginspace\keyword{do}\ \global\let\DO=\@oldDO}}
\def\STEP{\@marginspace\keyword{step}\ }
\def\TO{\@marginspace\keyword{to}\ }
\def\EXIT{\keyword{exit}}
% Generalised expression brackets:
\def\EXP{\openexp\tab}
\def\ENDEXP{\untab\closexp}
\def\VAR{\keyword{var}\ \tab}
\def\var{\keyword{var}\ }
\def\END{\@marginspace\untab\keyword{end}}
\def\ENDREP{\@marginspace\untab\keyword{endrep}}
\def\WHERE{\@marginspace\untab\tab\keyword{where}\ }
\def\WITHIN{\@marginspace\untab\keyword{within}\ }
\def\PROC{\keyword{proc}\ \tab}
\def\ENDPROC{\fullstop}
\def\FUNCT{\keyword{funct}\ \tab}
\def\ENDFUNCT{\fullstop}
\def\JOIN{\keyword{join}\ \tab}
\def\NIOJ{\@marginspace\untab\keyword{nioj}}
\let\ENDJOIN=\NIOJ
\def\ONEOF{\keyword{oneof}\ \tab}
\def\FOENO{\@marginspace\untab\keyword{foeno}}

\def\ACTIONS{\tab\keyword{actions}\ }
\def\ENDACTIONS{\@marginspace\untab\keyword{end-actions}}
\def\ENDACTION{\fullstop}
\def\CALL{\keyword{call}\ \tab}
\def\LLAC{\untab}
\let\ENDCALL=\LLAC
\def\COMMENT#1{\keyword{comment}:\ \mbox{#1}}

% The symbols used in programs:
\def\BODY{\ \equiv \ }
\def\QE{\fullstop} % end of == definition.
\def\EQT{\ \approx\ } % program equivalence.
\def\LE{\ \le\ }      % program refinement.
\def\NOT{\neg}
% \AND and \OR relations have an extra medium space around them:
\def\AND{\mathrel{\,\wedge\,}}
\def\OR{\mathrel{\,\vee\,}}
\def\openexp{\mathopen{\mbox{\raise.15ex\hbox{$\origbar$}\kern-0.15em%
		   \raise1.3ex\hbox{--}}}}
\def\closexp{\mathclose{\mbox{\lower0.9ex\hbox{--}\kern-0.24em%
		   \raise.15ex\hbox{$\origbar$}}}}
% \fullstop ends an action, proc or funct definition:}
\def\fullstop{\untab{\bf .}}
\def\barsymbol{{\rlap{$\sqcap$}\sqcup}}
\def\sbs{\subseteq}
\def\im{\Rightarrow}
\def\union{\cup}
\def\intersect{\cap}
\def\lar{\leftarrow}
\def\rar{\rightarrow}
\def\wflt{\prec}
\def\wfle{\preccurlyeq}

% Various arrows (taken from oz.sty):
\let \rel       \leftrightarrow
\let \tfun      \rightarrow
\let \tinj      \rightarrowtail
\def \tsur      {\mathrel{\ooalign{$\tfun$\hfil\cr$\mkern4mu\tfun$}}}
\def \pfun      {\p\tfun}
\def \pinj      {\p\tinj}
\def \psur      {\p\tsur}
\def \ffun      {\f\tfun}
\def \finj      {\f\tinj}
\def \bij       {\mathrel{\ooalign{$\tinj$\hfil\cr$\mkern5mu\tfun$}}}

%% Logical exclusive or:
\def\exor{\oplus}

%% Sequence concatenation:
\def\concat{\mathrel{+\!\!\!+}}

%% bitwise operators
\def\bitand {\mathrel{\overset{\mbox{\tiny bit}}{\wedge}}}
\def\bitor  {\mathrel{\overset{\mbox{\tiny bit}}{\vee}}}
\def\bitexor{\mathrel{\overset{\mbox{\tiny bit}}{\vphantom\vee\smash\oplus}}}
\def\bitnot{{\overset{\mbox{\tiny bit}}{\vphantom\vee\neg}}}

%% add the definition of overset if not present:
\@ifundefined{overset}%
  {\def\overset#1#2{\binrel@{#2}%
     \binrel@@{\mathop{\kern\z@#2}\limits»{#1}}}
   \def\binrel@#1{\setboxz@h{\thinmuskip0mu
      \medmuskip\m@ne mu\thickmuskip\@ne mu$#1\m@th$}%
     \setbox@ne\hbox{\thinmuskip0mu\medmuskip\m@ne mu\thickmuskip
      \@ne mu${}#1{}\m@th$}%
     \setbox\tw@\hbox{\hskip\wd@ne\hskip-\wdz@}}
   \def\binrel@@#1{\ifdim\wd2<\z@\mathbin{#1}\else\ifdim\wd\tw@>\z@
     \mathrel{#1}\else{#1}\fi\fi}%
   \def\setboxz@h{\setbox\z@\hbox}%
   \def\setbox@ne{\setbox\@ne}%
   \def\wd@ne{\wd\@ne}%
   \def\wdz@{\wd\z@}%
  }{}

%% A substitute for \text:
\@ifundefined{text}{\let\text=\mbox}{}


%% Set up _ as \_ outside math mode and \sb in math mode:
\catcode`\_=\active \def_{\ifmmode\sb\else\_\fi}
\mathcode`\_="8000 % Makes _ active in math mode only.
% Now define active character _ to do a subscript operation.
%\catcode`\_=\active
%\let _ =\sb
% Now give _ the catcode that we want to be in effect for normal
% (non-math) text).  The previous definition will thus remain
% inactive until we enter a math formula.
%\catcode`\_=12 % or maybe 11?

%% This really needs sorting out:
% Set up | as a variable delimiter:
% Simple vars will have the form: |short| or |very_long_variable_name|
% The test of \@sharp checks if the | is in an array or tabular
% environment preamble - if so then | has its default value.
% Otherwise, | is a variable delimiter.
\catcode`\|=12\relax
\def\origbar{|}
\catcode`\|=\active

\def|{\ifx\@sharp\relax\origbar\else\@dovar\fi}
\def\@dovar#1#2|{#1\variable{#2}} % #1 = \fi from defn of |

% Set up ";" to add a space after it when active in math mode:
\catcode`\;=12\relax
\mathcode`\;="8000 % Makes ; active in math mode
{\catcode`\;=\active \gdef;{\semicolon\;}}
\mathchardef\semicolon="603B

% Set up ` so that ``...'' typesets the string in tt (in math mode):
\mathcode`\`="8000 % Makes ` active in math mode only.
{%\catcode`\'=\active
 \catcode`\`=\active
 \gdef`{\startstring@}
}
\def\startstring@`#1''{\text{``{\tt #1}''}}

% Set up a larger array of tabs since programs set lots of tabs.
% This section can be extended if more tabs are needed:
\newdimen\@gtempa \@firsttab=\allocationnumber
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
\newdimen\@getempa \@maxtab=\allocationnumber

% NB: can't use \pushtabns and \poptabs to reduce the need for tabs
% since \@curtab, \@curtabmar and \@nxttabmar are global variables
% which would also need to be saved and restored.

% The program environment - keeps the whole program on one page.
% This is based on the tabbing environment with each line put in math mode,
% \obeylines in force and ";" as an active character:
\def\@programcr{$\@tabcr$}

\def\program{%
    % activate tabbing commands:
    \@tabcommandson \obeycr \catcode`\;=\active %% added line
    \lineskip \z@\let\>\@rtab\let\<\@ltab\let\=\@settab
    \let\+\@tabplus\let\-\@tabminus\let\`\@tabrj\let\'\@tablab
    \let\\=\@programcr %% changed from \let\\=\tabcr
    \global\@hightab\@firsttab
    \global\@nxttabmar\@firsttab
    \dimen\@firsttab\@totalleftmargin
    \global\@tabpush0 \global\@rjfieldfalse
    \trivlist \item[]\if@minipage\else\vskip\parskip\fi
    \setbox\@tabfbox\hbox{\rlap{\indent\hskip\@totalleftmargin
      \the\everypar}}\def\@itemfudge{\box\@tabfbox}\@startline\ignorespaces
    $\@gobblecr %% added line
    }

\def\endprogram{$\@stopline\ifnum\@tabpush > 0 \@badpoptabs \fi\endtrivlist%
		%\catcode`\;=12\relax %% added line
		\restorecr \@tabcommandsoff %% added line
		%% cancel the last newline: %% added line
		\if@minipage\else\vskip-\baselineskip\fi %% added line
	       }


% - version which puts the whole program in a box.
\newenvironment{programbox}
    {\begin{minipage}[t]{\textwidth}%
     \begin{program}}%
    {\end{program}%
     \vspace{0pt}%
     \end{minipage}}

\def\({\begin{programbox}}
\def\){\end{programbox}}

%% Cases environment:
%% based on description environment with numbering:
\def\Cases{\ifnum \@enumdepth >3 \@toodeep\else
	   \advance\@enumdepth \@ne
	   \edef\@enumctr{enum\romannumeral\the\@enumdepth}%
	   \list{{\normalshape\bf Case \arabic{\@enumctr}:}}% standard label
		{\usecounter{\@enumctr}%
		 \def\makelabel##1{##1}}\fi}

\let\endCases=\endlist

%% \cases is changed by amstex.sty - don't know the syntax for their
%% environment so I change it back to the plain TeX definition:
%% Have added a line to define \\ as \cr within cases:
\def\cases#1{\left\{\,\vcenter{{\let\\=\cr\normalbaselines\m@th
    \ialign{$##\hfil$&\quad##\hfil\crcr#1\crcr}}}\right.}

%% Environment romanenumerate for lists numbered by roman numerals:
\def\romanenumerate{\begingroup
  \def\theenumi{\myroman{enumi}}%
  \def\p@enumi{(\theenumi)}%
  \def\labelenumi{(\theenumi)}%
  \enumerate}
\def\endromanenumerate{\endenumerate\endgroup}

%% A fix to get lower case Roman numerals for use as labels:
\def\myroman#1{\@myroman{\@nameuse{c@#1}}}
\def\@myroman#1{\expandafter{\romannumeral #1}}

%% \proof macro for theorems and lemmas:
\def\proof{\normalshape{\setlength{\parskip}{0pt}\par\addvspace\medskipamount
			\noindent{\bf Proof: }}\ignorespaces}

%% require the {...} for \wp and \WP
\let\oldwp=\wp % save old \wp (curly p character)
\def\wp#{\@wp}
\def\@wp#1{\text{wp}(#1)}
\def\WP#{\@WP}
\def\@WP#1{\text{WP}(#1)}

%% =df symbol:
\def\edf{\mathrel{\;=_{{}_{\text{DF}}}\;}}

%% empty set symbol: (use \varnothing if available)
\@ifundefined{varnothing}%
	     {\def\nullset{\emptyset}}%
	     {\def\nullset{\varnothing}}%

%% Powerset symbol:
%% check if \EuRoman defined - if not then use \oldwp (Large and raised):
\@ifundefined{EuRoman}%
  {\def\powerset{\raisebox{0.5ex}{\Large$\oldwp$}}}% no \EuRoman
  {\def\powerset{\raisebox{0.5ex}% Use Euler roman P
		 {\Large\family{eur}\series{m}\shape{n}\selectfont\char"7D}}}

%% old definition used \EuScript P:
%  \def\powerset{\boldsymbol{\EuScript P}}


%% Bad news, there is no \bigsqcap corresponding to \bigsqcup. Here's a
%% fake based on \sqcap (won't look quite the same unfortunately):
% \def\bigsqcap{\mathop{\mathchoice
%   {\vcenter{\hbox{\Huge $ \sqcap $}}}    % display
%   {\vcenter{\hbox{\Large $ \sqcap $}}}   % text
%   {\vcenter{\hbox{\Large $ \sqcap $}}}   % script
%   {\vcenter{\hbox{\Large $ \sqcap $}}}}} % scriptscript

%% An alternative using rules (only works at standard size)

\def\bigsqcap{\mathop{%
		\rule[-0.2ex]{.07em}{2.17ex}%
		\rule[1.8ex]{0.5em}{.17ex}%
		\rule[-0.2ex]{.07em}{2.17ex}}}

%% Two line displayed equation, eg:
%% \[  \twoline{ a_very_long_left_hand_side \\
%%                   {} = a_fairly_long_right_hand_side } \]
%% Use in displayed maths mode.
%% NB this is superseded by AMSLaTeX's multline environment.
\def\twoline#1{\def\\{\hfill\cr\hfill}% \def only last to end of display
	       \displaylines{\quad #1 \quad\cr}}
