% These macros are based on plain TeX. Use them to typeset
% calculational proofs and programs written in what Dijkstra called ``dot
% notation''. Dijkstra described the proof format in EWD 1300 and
% the programming language in ``A Discipline of Programming''.
% Don't hesitate to contact me:
% Wolfgang Helbig              helbig@lehre.ba-stuttgart.de
% Stauferstr. 22               http://wwwlehre.ba-stuttgart.de/~helbig
% 71334 Waiblingen             November 2008

% Sets and quantified operators
% The first two parameters are delimited by `: ', they provide the
% the quantifier and the range. The last parameter defines the term.
% It is delimited by `\>'. If the range is empty, the two colons will not
% be separated by space. The quantifier may be empty to give you a set.

\def\<#1: #2: #3\>{\langle #1\;:\if#2\empty\else\;#2\;\fi:\;#3\rangle}
\let\mx\uparrow % maximum
\let\mn\downarrow % minimum
\let\fa\forall % universal quantifier
\let\ex\exists % existential quantifier
\let\su\Sigma % sum
\def\nbr{\#} % number of 

% Space surrounding binary operators.
% The lower the precedence of a operator the more space should surround it.
% Plain TeX provides \qquad = 36u; \quad = 18u; \; = 5u; \> = 4u; \, = 3u;
%          \!=-3u where one u is em/18.

% logical operators (use mxx for operator xx surrounded by space)
\let\eq\equiv
\def\meq{\qquad\eq\qquad} % equivalence surrounded by 36u
\let\ff\Leftarrow % "follows from"
\def\mff{\quad\ff\quad} % "follows from" surrounded by 18u
\let\impl\Rightarrow
\def\mimpl{\quad\impl\quad} % "implies" surrounded by 18u
\let\and\land
\def\mand{\;\,\and\;\,} % "and" surrounded by 9u
%\let\or\lor
\def\mor{\;\,\lor\;\,} % "or" surrounded by by 9u

% For most arithmetic operators, we use what plain TeX provides, namely
% mathrel is surrounded by 5u space (see p. 170 in The TeXbook)
% mathbin is surrounded by 4u space
% mathpunct is followed by 3u space

% Plain TeXs classification needs some correction however.
% ``\mathcode "cfpp'' encodes class, font family and position in the font.
% Plain TeX treats '*' as a bin operator, we need it as an ordinary symbol.
\mathcode`\*="0203 % class was 2 (binary)

% Plain TeX treats ':' as a rel operator, we need it as an ordinary symbol.
\mathcode`\:="003A % class was 3 (relation)

% \div and \mod should be surrounded by very little space, since
% they have a high precedence
\def\halfthinneg{\mskip-.5\thinmuskip}
\def\div{\mathbin{\halfthinneg\hbox{\bf div}\halfthinneg}}
\def\mod{\mathbin{\halfthinneg\hbox{\bf mod}\halfthinneg}}
\def\gcd{\hbox{\bf gcd}}

% Indented formulas and proofs
% A proof is a succession of formula lines and hint lines.

% A formula line has one parameter which is deliminated by \\
% Use as `\f formula \\'
\def\f#1\\{\tabalign&&$#1$\cr} % like `\f E=mc^2\\'

% A hint line has two parameters,  a relational operator and a hint.
% Use as `\h\eq {hint why the relation holds}'
\def\h#1#2{\tabalign&$#1$&&$\{\,$#2$\,\}$\cr} % hint line
\def\heq#1{\h\eq {#1}} % Abbreviation for `\h\eq {easily seen}'

% A named formula has two parameters: The name, deliminated by
% `:' and the formula, deliminated by `\\'.
% Use as `\nf R1: formula \\'
\def\nf #1:#2\\{\tabalign$#1:$&&$#2$\cr} % like `\nf Einstein: E=mc^2\\'

% A numbered formula is similar, it typesets a parenthesized number at
% the left side, e.g., `\nrf 1 E=mc^2\\'
% Use as `\nrf 1 formula \\'
\def\nrf #1#2\\{\tabalign(#1)&&$#2$\cr} % numbered formula

% To typeset formulas, named formulas, and hints in double columns, use
% the `d'-versions that take twice as much parameters.
\def\dnf #1:#2\\#3:#4\\{\tabalign$#1:$&&$#2$&&$#3:$&&$#4$\cr} % named formula
\def\df#1\\#2\\{\tabalign&&$#1$&&&&$#2$\cr} % double formula
% Use `\dh \relax \relax = {hint}' for empty left columns
\def\dh#1#2#3#4{\tabalign&$#1$&&\condhint{#2}&&$#3$&&$\{\,$#4$\,\}$\cr}
\def\condhint#1{\ifx#1\relax\else$\{\,$#1$\,\}$\fi} % left column empty

% Here are the alignments of (double column) formulas and hint lines.
\def\+{\tabalign} % we don't want \outer\def
\def\setcols{\settabs\+\qquad&\quad&\qquad&\hskip .5\hsize\hskip-5em&
                       \qquad&\quad&\qquad&\cr}

% Macros for programs
% comments are specified as `\co {some text}'
\def\co#1{\;\{\,#1\,\}} % comment
\def\cofl#1{\{\,#1\,\}} % comment flush left

% Indententation of a program line is controlled by \& and \decind.
% \& sets the indentation of the following lines to its current position.
% \decind decrements the indentation level of the following lines
\newcount\nskips % holds number of tabstops
\def\skipn{\ifcase\nskips\def\j{&}\or\def\j{&&}\or\def\j{&&&}
      \or\def\j{&&&&}\or\def\j{&&&&&}\or\def\j{&&&&&&}\or\def\j{&&&&&&&}
      \else\def\j{}\fi\j} % skip nskips tabstops
\def\skipnmone{\global\advance\nskips by -1 \skipn\global\advance\nskips by 1}

% Set a tabstop, succeeding lines will be left aligned to the new tabstop.
\def\&{$\cleartabs&\global\advance\nskips by 1$}%

% Decrement indentation, succeeding lines will be left aligned to the tabstop 
% preceding the current one.
\def\decind{$\global\advance\nskips by -1$}

% The active character ^^M (end of line) both formats a program line and
% deliminates it. 
\def\eatfirst#1{}
\catcode`\^^M=\active %
\def\programline#1{\ifx;#1\def\next##1^^M{\+\skipnmone\hfill$;\;$&$##1$\cr^^M}%
  \else\ifx\eblock#1\def\next{\eblock}%
  \else\ifx\cofl#1\def\next##1^^M{\+\skipn$\cofl{##1}$\cr^^M}%
  \else\ifx\od#1\def\next##1^^M{\+\skipnmone\hfill$\rawod$&$##1$\decind\cr^^M}%
  \else\ifx\FI#1\def\next##1^^M{\+\skipnmone\hfill$\rawfi$&$##1$\decind\cr^^M}%
  \else\ifx\|#1\def\next##1^^M{\+\skipnmone\hfill$\rawbar\;\;$&$##1$\cr^^M}%
  \else\ifx\]#1\def\next##1^^M{\+\skipnmone\hfill$]\;$&$##1$&\decind\cr^^M}%
  \else\def\next##1^^M{\+\skipn$#1##1$\cr^^M}\fi\fi\fi\fi\fi\fi\fi\next}%
%
% Enclose a block of program lines between \bblock and \eblock.
\def\bblock{\doparskip\nskips=0\catcode`\^^M=\active \let^^M=\programline }%
\def\eblock{\catcode`\^^M=5 \setcols }%
\catcode`\^^M=5 %

% Identation is controlled automatically be some tokens as follows:

% `\[', `\do', and `\IF' set a tabstop right of them and increment
% the indent level. The corresponding closing tokens decrement the
% indent level. The `;', the `|', the \od and the \]| tokens at the
% beginning of a new line are typeset slightly left of the current
% identation level.

% Tokens in our programming language
% block
\def\[{[\;\&}
\def\nomenclature#1{\mathbin{\hbox{\bf#1}}\>}
\def\glocon{\nomenclature{glocon}}
\def\glovar{\nomenclature{glovar}}
\def\vircon{\nomenclature{vircon}}
\def\virvar{\nomenclature{virvar}}
\def\pricon{\nomenclature{pricon}}
\def\privar{\nomenclature{privar}}
\def\]{\;]\decind}
% primitive initializing statement
\def\vir{${\bf\ vir }$}
\def\array{${\bf\ array}$}
% assignment
\def\:#1{\mathord{\>\,:\!=\>\,}} % use as `\:='
% guarded command list
\def\-#1{\;\;\mathord{\rightarrow}\;\;} % use as '\->'
\def\|{\;\rawbar\;}
% if statement
\def\IF{\rawif\&}
\def\FI{\;\;\rawfi\decind}
% do statement
\def\do{\rawdo\&}
\def\od{\;\;\rawod\decind}

% internal use 
\def\rawbar{|\hskip -1.4pt]}
\def\rawdo{\hbox{\bf do}\;\;}
\def\rawod{\hbox{\bf od}\;\;}
\def\rawfi{\hbox{\bf fi}\;\;}
\def\rawif{\hbox{\bf if}\;\;}

% format definitions
\parindent=0pt
\parskip=6pt plus 2pt minus 2pt
\def\unparskip{\vskip-\parskip}
\def\doparskip{\vskip \parskip}
\def\bi{\hfil\break\hbox{\qquad}}
\setcols