path: root/macros/latex/contrib/vdm/vdm.sty

%%% ====================================================================
%%%  @LaTeX-style-file{
%%%     author          = "Mario Wolczko",
%%%     version         = "4.00",
%%%     date            = "14 October 1994",
%%%     filename        = "vdm.sty",
%%%     address         = "FORMERLY AT
%%%                        Dept of Computer Science
%%%                        The University of Manchester
%%%                        Oxford Road
%%%                        Manchester M13 9PL
%%%                        UK",
%%%     codetable       = "ISO/ASCII",
%%%     keywords        = "LaTeX, VDM specification language",
%%%     supported       = "yes",
%%%     docstring       = "LaTeX macros for typesetting VDM
%%%                        specifications.
%%%                        NOTE
%%%                        Mario no longer works at Manchester
%%%                        This is a minimal update to LaTeX2e
%%%                        By David Carlisle",
%%%  }
%%% ====================================================================
%
%       BSI VDM documentstyle option for LaTeX
%
%       M. Wolczko
%
%
% Dept. of Computer Science   Internet:      mario@cs.man.ac.uk
% The University              uucp:    mcsun!uknet!man.cs!mario
% Manchester M13 9PL          JANET:         mario@uk.ac.man.cs
% U.K.                        Tel: +44-61-275 6146  (FAX: 6236)
%
% Version for LaTeX2e by David Carlisle.
% Just constructed by removing all the old font wierdness.
% Not tested at all!
%
%
%----------------------------------------------------------------
%
%       Installation-dependent features
%


\newif\ifams@ 

\ams@true

\ifams@
 \RequirePackage{amsfonts}
\fi

%----------------------------------------------------------------
%
%       The vdm environment
%
% record whether we were in horizontal mode when entering...
\newif\ifhm@

\def\vdm{\ifhmode\hm@true\else\hm@false\fi
  \@changeMathmodeCatcodes\@postUnderPenalty10000\relax}

% after an \end{vdm} the next paragraph is not indented unless a \par
% comes first (if we entered in horizontal mode).  This is a bit of a
% kludge!
\def\endvdm{\ifhm@\else
  \global\let\par=\@undonoindent
  \global\everypar={{\setbox0=\lastbox}\global\everypar={}%
                        \global\let\par=\@@par}%
  \fi}

\def\@undonoindent{\global\everypar={}\global\let\par=\@@par\@@par}

%-----------------------------------------------------------------
%
%       Controlling line and page breaks
%
% Text within the vdm environment is essentially mathematical in
% nature, so requires special care.  Whenever outer vertical mode is
% entered, the \@beginVerticalVDM command should be used.  This sets
% up \leftskip, \rightskip, \baselineskip, \lineskip and
% \lineskiplimit to conform with the overall style.
%
% When entering unrestricted horizontal mode, the \@beginHorizontalVDM
% command should be used.  This sets up:
%       \leftskip and \rightskip to 0,
%       \\ to do line breaking
%       ragged right line breaking, with special penalties, and
%       enters math mode.
% \@endHorizontalVDM should be called when leaving unrestricted
% horizontal mode.

\def\@beginVerticalVDM{\@changeMargins\@changeBaselineskip}

\def\@beginHorizontalVDM{\@restoreLineSeparator
  \@restoreMargins\@raggedRight\noindent$\strut\relax}
\def\@endHorizontalVDM{\relax\strut$}

% \VDMindent is used for \leftskip within VDM, \VDMrindent for
% \rightskip, \VDMbaselineskip for \baselineskip
\newdimen\VDMindent \VDMindent=\parindent
\newdimen\VDMrindent \VDMrindent=\parindent
\def\VDMbaselineskip{\baselineskip}

\def\@changeMargins{\leftskip=\VDMindent \rightskip=\VDMrindent}
\def\@restoreMargins{\advance\hsize by-\leftskip
  \advance\hsize by-\rightskip
  \leftskip=0pt \rightskip=0pt}
\def\@changeBaselineskip{\baselineskip=\VDMbaselineskip
  \lineskip=0pt \lineskiplimit=0pt
  % need to alter the size of struts, too
  \setbox\strutbox\hbox{\vrule height.7\baselineskip
      depth.3\baselineskip width\z@}}

% these are used in externals, records and cases
\def\@changeLineSeparator{\let\\=\cr} % for usr within \halign
\def\@restoreLineSeparator{\let\\=\newline}

\def\@raggedRight{\rightskip=0pt plus 1fil
  \hyphenpenalty=-100 \linepenalty=200
  \binoppenalty=10000 \relpenalty=10000 \pretolerance=-1}

% ------------------------------------------------------------------------

%       Font and Character Changes

% make a-zA-Z use the \it family within math mode, and ~ mean \hook.
% Digits 0-9 remain as normal.
\everymath=\expandafter{\the\everymath\vdm@it
        \@changeMathmodeCatcodes}%
\everydisplay=\expandafter{\the\everydisplay\vdm@it
        \@changeMathmodeCatcodes}%

\def\vdm@it{\@fontswitch\it\mathit}

\mathcode`\0="0030
\mathcode`\1="0031
\mathcode`\2="0032
\mathcode`\3="0033
\mathcode`\4="0034
\mathcode`\5="0035
\mathcode`\6="0036
\mathcode`\7="0037
\mathcode`\8="0038
\mathcode`\9="0039

\mathchardef\Gamma="0000
\mathchardef\Delta="0001
\mathchardef\Theta="0002
\mathchardef\Lambda="0003
\mathchardef\Xi="0004
\mathchardef\Pi="0005
\mathchardef\Sigma="0006
\mathchardef\Upsilon="0007
\mathchardef\Phi="0008
\mathchardef\Psi="0009
\mathchardef\Omega="000A

% If the user really wants the normal codes, she can call \defaultMathcodes
%\def\defaultMathcodes{\let\vdm@it\relax}
\def\defaultMathcodes{\let\vdm@it\relax}


% remember the original mathcode of minus sign
\edef\@minuscode{\the\mathcode`\-}

\def\mathminus{\mathcode`\-=\@minuscode }
\def\textminus{\mathcode`\-="002D }
% by default, use text minus
%\textminus

% make a : into punctuation, a - into a letter, and | mean \mid
 % NFSS-change
 % \mathcode`\-="042D changed to \mathcode`\-="002D as we can not rely on
 % \itfam being fam 4.
 \def\@changeOtherMathcodes{\mathcode`\:="603A \textminus
  \mathcode`\|="326A \mathchardef\Or="325F }% this is a rel to get 5mu spacing
 \def\relbar{\mathrel{\smash\minus}}% redefine because mathcode of -
                                    % has changed


% alternative underscore
\def\@VDMunderscore{\leavevmode
  \kern.06em\vbox{\hrule\@height .2ex\@width .3em}\penalty\@postUnderPenalty
  \hskip 0.1em}

% Allow line breaks after an underscore, but not in vdm mode (see
% \vdm).  This is so long identifiers can be broken when run
% into paragraphs.
\newcount\@postUnderPenalty \@postUnderPenalty=200

% now require some catcode trickery to enable us to change _ when we want to
{\catcode`\_=\active 
 \gdef\@changeGlobalCatcodes{% make _ a normal char
        \catcode`\_=\active \let_=\@VDMunderscore}
 \gdef\@changeMathmodeCatcodes{%
        % make ~ mean \hook, " do text, @ mean subscript
        \let~=\hook
        \catcode`\@=8
        \mathcode`\"="8000 }
        \uccode`\~=`\"%
 \gdef\underscoreoff{% make _ a normal char
        \catcode`\_=\active \let_=\@VDMunderscore}
 \gdef\underscoreon{% restore underscore to usual meaning
        \catcode`\_=8}
\uppercase{\gdef~}#1"{\nfss@text{\rm #1}}}

%----------------------------------------------------------------
%
%       Keywords
%
\ifx\fmtname\@fmtname
        \def\keywordFontBeginSequence{\sf}%     user-definable
\else\ifx\fmtname\@psfmtname
        \def\keywordFontBeginSequence{\sf}% Helvetica is OK
\else
        \def\keywordFontBeginSequence{\bf}% good for SliTeX
\fi\fi

\def\kw#1{\hbox{\keywordFontBeginSequence #1\/}}

\def\makeNewKeyword#1#2{% use \newcommand for extra checks
        \newcommand{#1}{\hbox{\keywordFontBeginSequence #2\/}}}

\makeNewKeyword{\nil}{nil}
\makeNewKeyword{\True}{true}
\makeNewKeyword{\true}{true}
\makeNewKeyword{\False}{false}
\makeNewKeyword{\false}{false}
\makeNewKeyword{\rem}{ rem }

\def\where{\par\moveright\VDMindent\hbox{\keywordFontBeginSequence where\/}}

%----------------------------------------------------------------
%
%       monadic operator creation
%
\def\newMonadicOperator#1#2{\newcommand{#1}{\kw{#2\kern.16667em}\nobreak}}

%----------------------------------------------------------------
%
%       primitive numeric types
%
% use the AMS fonts for these if possible

\ifams@
  \DeclareMathSymbol{\Bool} {\mathord}{AMSb}{"42}   % Booleans
  \DeclareMathSymbol{\Nat}  {\mathord}{AMSb}{"4E}   % Natural numbers
  \def\Nati{\Nat_1}             % Positive natural numbers
  \DeclareMathSymbol{\Int}  {\mathord}{AMSb}{"5A}   % Integers
  \DeclareMathSymbol{\Real} {\mathord}{AMSb}{"52}   % Reals
  \DeclareMathSymbol{\Rat}  {\mathord}{AMSb}{"51}   % Rationals
\else
  \def\Bool{\nfss@text{\bfseries B\/}}
  \def\Nat{\nfss@text{\bfseries N\/}}
  \def\Nati{\hbox{$\nfss@text{\bfseries N}_1$}}
  \def\Int{\nfss@text{\bfseries Z\/}}
  \def\Real{\nfss@text{\bfseries R\/}}
  \def\Rat{\nfss@text{\bfseries Q\/}}
\fi
\let\Natone=\Nati % just for an alternative

%----------------------------------------------------------------
%
%       Operations
%
% The op environment.  Within op you can specify args,
% result, etc. which are gathered into registers, and output when the
% op env. ends.
%
% The optional argument is the operation name

% shorthand for an operation on its own: the vdmop env.
\def\vdmop{\vdm\op} \def\endvdmop{\endop\endvdm}

% registers constructed within an op environment
\newtoks\@operationName
\newbox\@operationNameBox
\newif\ifArgumentListEncountered@
\newtoks\@argumentListTokens
\newtoks\@resultNameAndTypeTokens
\newbox\@externalsBox
\newbox\@preConditionBox
\newbox\@postConditionBox
\newbox\@errConditionBox

\def\op{% clear temporaries, deal with optional arg
        \setbox\@operationNameBox=\hbox{}%
        \@argumentListTokens={}\ArgumentListEncountered@false
        \@resultNameAndTypeTokens={}%
        \setbox\@externalsBox=\box\voidb@x
        \setbox\@preConditionBox=\box\voidb@x
        \setbox\@postConditionBox=\box\voidb@x
        \par\preOperationHook
        \vskip\preOperationSkip
        \@beginVerticalVDM
        \@ifnextchar [{\@opname}{}}

% breaking parameters
\newcount\preOperationPenalty \preOperationPenalty=0
\newcount\preExternalPenalty \preExternalPenalty=2000
\newcount\prePreConditionPenalty \prePreConditionPenalty=800
\newcount\prePostConditionPenalty \prePostConditionPenalty=500
\newcount\preErrConditionPenalty \preErrConditionPenalty=500
\newcount\postOperationPenalty \postOperationPenalty=-500

% gaps between bits of operations
\newskip\preOperationSkip \preOperationSkip=2ex plus 0.5ex minus 0.2ex
\newskip\postOperationSkip \postOperationSkip=2ex plus 0.5ex minus 0.2ex
\newskip\postHeaderSkip \postHeaderSkip=.5ex plus .2ex minus .2ex
\newskip\postExternalsSkip \postExternalsSkip=.5ex plus .2ex minus .2ex
\newskip\postPreConditionSkip \postPreConditionSkip=.5ex plus .2ex minus .2ex
\newskip\preErrConditionSkip \preErrConditionSkip=.5ex plus .2ex minus .2ex

\def\endop{% make up operation
        % IMPORTANT---don't remove the vskips in this macro
        % if you don't want one, set it to 0pt
        \vskip 0pt
        \@setOperationHeader
        \betweenHeaderAndExternalsHook
        \vskip\postHeaderSkip
        \ifvoid\@externalsBox
              \betweenExternalsAndPreConditionHook
        \else \moveright\VDMindent\box\@externalsBox
              \betweenExternalsAndPreConditionHook
              \vskip\postExternalsSkip
        \fi
        \ifvoid\@preConditionBox
              \betweenPreAndPostConditionHook
        \else \moveright\VDMindent\box\@preConditionBox
              \betweenPreAndPostConditionHook
              \vskip\postPreConditionSkip
        \fi
        \ifvoid\@postConditionBox
              \betweenPostAndErrHook
        \else \moveright\VDMindent\box\@postConditionBox
              \betweenPostAndErrConditionHook
        \fi
        \ifvoid\@errConditionBox
        \else \vskip\preErrConditionSkip
              \moveright\VDMindent\box\@errConditionBox
        \fi
        \postOperationHook
        \vskip\postOperationSkip}

% hooks for user-defined expansion
% TeX is in outer vertical mode when these are called.
% ALWAYS leave TeX in vertical mode after these macros have been called
\def\preOperationHook{\penalty\preOperationPenalty }
\def\betweenHeaderAndExternalsHook{\penalty\preExternalPenalty }
\def\betweenExternalsAndPreConditionHook{\penalty\prePreConditionPenalty }
\def\betweenPreAndPostConditionHook{\penalty\prePostConditionPenalty }
\def\betweenPostAndErrConditionHook{\penalty\preErrConditionPenalty }
\def\postOperationHook{\penalty\postOperationPenalty }

% combine the operation name, argument list and result
\def\@setOperationHeader{%
        \moveright\VDMindent\vtop{%
                \ifArgumentListEncountered@
                        \setbox\@operationNameBox=%
                                \hbox{\unhbox\@operationNameBox$($}\fi
                \hangindent=\wd\@operationNameBox \hangafter=1
                \noindent\kern-.05em\box\@operationNameBox
                \@beginHorizontalVDM
                \ifArgumentListEncountered@\the\@argumentListTokens)\fi
                \ \the\@resultNameAndTypeTokens
                \@endHorizontalVDM}}

% set the operation name
% \opname{name-of-operation}
\def\opname#1{\@opname[#1]}
\def\@opname[#1]{\@operationName={#1}%
  \global\setbox\@operationNameBox=\hbox{$\relax#1$\ }}

% set up the argument list
% \args{ argument \\ argument \\ argument... } where \\ forces a line break
% This is also used in the fn environment
\def\args{\global\ArgumentListEncountered@true \global\@argumentListTokens=}

% result name and type
\def\res{\global\@resultNameAndTypeTokens=}

% externals list
%
% An external list could be either very long or very short, so we provide
% two forms.  One is the short \ext{..} command, the other is the externals
% environment.
% Externals are always separated by \\
%

% we have to mess a little to get the catcode of : right
\def\ext{\bgroup\@makeColonActive\@ext}
\def\@ext#1{\externals#1\endexternals\egroup}

\def\externals{\global\setbox\@externalsBox=%
        \@beginIndentedPara{\hsize}{ext }{\@setUpExternals}}
\def\endexternals{\@endIndentedPara{\@endAlignment}}

\def\@setUpExternals{\@makeColonActive\@changeLineSeparator\@beginAlignment}

% more catcode trickery for :
{\catcode`\:=\active
 \gdef\@makeColonActive{\catcode`\:=\active \let:=&}}

% the \expandafters are necessary because TeX doesn't expand
% \halign specs when scanning for # and &
\def\@beginAlignment{\expandafter\halign\expandafter\bgroup
        \the\@extAlign\strut\enspace&:\enspace$##$\hfil\cr}
\def\@endAlignment{\crcr\egroup}

% the user can decide on the exact alignment of the field names
\newtoks\@extAlign
\def\leftExternals{\@extAlign={$##$\hfil}}
\def\rightExternals{\@extAlign={\hfil$##$}}
\leftExternals

\makeNewKeyword{\Rd}{rd } \makeNewKeyword{\Wr}{wr }

% pre-condition, post-condition and err-condition
%
% once again we provide short forms \pre, \post, \err and environments
% precond, postcond and errcond
\def\pre#1{\precond#1\endprecond}
\def\precond{\global\setbox\@preConditionBox=%
        \@beginMathIndentedPara{\hsize}{pre }}
\def\endprecond{\@endMathIndentedPara}

\def\post#1{\postcond#1\endpostcond}
\def\postcond{\global\setbox\@postConditionBox=%
        \@beginMathIndentedPara{\hsize}{post }}
\def\endpostcond{\@endMathIndentedPara}

\def\err#1{\errcond#1\enderrcond}
\def\errcond{\global\setbox\@errConditionBox=%
        \@beginMathIndentedPara{\hsize}{errs }}
\def\enderrcond{\@endMathIndentedPara}


%----------------------------------------------------------------
%
%       Box man\oe uvres
%
% Here's where all the tricky box manipulation commands go
%
% \@beginIndentedPara begins construction of a \hbox of width #1
% which contains keyword #2 to the left of a para in a vtop.
% #3 is evaluated within the inner vtop.
% endIndentedPara closes the box off; its arg. is evaluated just
% before closing the box.
%
\def\@beginIndentedPara#1#2#3{\hbox to #1\bgroup \setbox0=\kw{#2}%
        \copy0 \strut \vtop\bgroup \advance\hsize by -\wd0 #3}
\def\@endIndentedPara#1{\strut#1\egroup\hss\egroup}

% \@beginMathIndentedPara places the para in vdm mode
\def\@beginMathIndentedPara#1#2{\@beginIndentedPara{#1}{#2}%
        {\@beginHorizontalVDM}}
\def\@endMathIndentedPara{\@endIndentedPara{\@endHorizontalVDM}}

% \@belowAndIndent#1#2 places #2 in a vbox below and to the right of #1
\def\@belowAndIndent#1#2{#1\hfil\break
        \@beginMathIndentedPara{\hsize}{\qquad}#2\@endMathIndentedPara}

% \@mathIndentedPara does the whole thing
\def\@mathIndentedPara#1#2#3{\@beginMathIndentedPara{#1}{#2}#3%
        \@endMathIndentedPara}
%----------------------------------------------------------------
%
%       Constructions
%
% Here are all the standard constructions.
% The only tricky one is \cases.
% Those that construct a box must be made to make that box of 0 width,
% and force a line break immediately afterwards.

% \If mm-exp \Then mm-exp \Else mm-exp \Fi
% multi-line indented if-then-else
%
\def\If#1\Then#2\Else#3\Fi{\vtop{%
        \@mathIndentedPara{0pt}{if }{#1}%
        \@mathIndentedPara{0pt}{then }{#2}%
        \@mathIndentedPara{0pt}{else }{#3}}}

% \SIf mm-exp \Then mm-exp \Else mm-exp \Fi
% single line if-then-else
\def\SIf#1\Then#2\Else#3\Fi{\hbox to 0pt{\vtop{\@beginHorizontalVDM
        \kw{if }\nobreak#1\penalty0\hskip 0.5em
        \kw{then }\nobreak#2\penalty-100\hskip 0.5em % break here OK
        \kw{else }\nobreak#3\@endHorizontalVDM}\hss}}

% \Let mm-exp \In mm-exp2
% multi-line let..in ; mm-exp2 is `curried'
\def\Let#1\In{\vtop{%
        \@mathIndentedPara{0pt}{let }{#1\hskip 0.5em\kw{in}}}\hfil\break}

% \SLet mm-exp \In mm-exp
% single-line let..in
\def\SLet#1\In#2{\hbox to 0pt{\vtop{\@beginHorizontalVDM
        \kw{let }\nobreak#1\hskip 0.5em
        \kw{in }\penalty-100 #2\@endHorizontalVDM}\hss}}

% multi-line cases
%
% \Cases{ selecting-mm-exp }
% from-case1 & to-case1 \\
% from-case2 & to-case2 \\
%           ...
% from-casen & to-casen
% \Otherwise{ mm-exp }
% \Endcases[optional text for the rest of the line]

\newif\ifOtherwiseEncountered@
\newtoks\@OtherwiseTokens

\def\Cases#1{\hbox to 0pt\bgroup \vtop\bgroup
                \@mathIndentedPara{\hsize}{cases }{\strut
                        #1\hskip 0.5em\strut\kw{of}}%
                \bgroup % we might be in a nested case, so we have to
                        % save the \Otherwise bits we might lose
                \OtherwiseEncountered@false \@changeLineSeparator
                \@beginCasesAlignment}

% the user can decide on the exact alignment
\newtoks\@casesDef
\def\leftCases{\@casesDef={$##$\hfil}}
\def\rightCases{\@casesDef={\hfil$##$}}
\rightCases

% the \expandafters are necessary because TeX doesn't expand
% \halign specs when scanning for # and &
\def\@beginCasesAlignment{\expandafter\halign\expandafter\bgroup
        \the\@casesDef&$\,\rightarrow##$\hfil\cr}

\def\Otherwise{\global\OtherwiseEncountered@true \global\@OtherwiseTokens=}
\let\Others=\Otherwise

\def\Endcases{\@endCasesAlignment \@setOtherwise \egroup \@setEndcases}
\def\@endCasesAlignment{\crcr\egroup}
\def\@setOtherwise{\ifOtherwiseEncountered@ % have an otherwise clause
        \@mathIndentedPara{\hsize}{others }{%
                \strut\the\@OtherwiseTokens\strut}
        \fi}

% must test for the optional arg to follow the end
\def\@setEndcases{\noindent
        \strut\kw{end}\@ifnextchar [{\@unbracket}{\@finalCaseEnd}}
\def\@unbracket[#1]{$#1$\@finalCaseEnd}
\def\@finalCaseEnd{\egroup\hss\egroup}%\hfil\break

%----------------------------------------------------------------
%
%       special symbols

% defined as
\def\DEF{\raise.5ex
        \hbox{\footnotesize\underline{$\mathchar"3234$}}}% a \triangle


% cross product
\let\x=\times

%       logical connectives
%
\def\Iff{\penalty-50\mskip 7mu plus 2mu minus 2mu
        \Leftrightarrow\mskip 7mu plus 2mu minus 2mu}
\let\iff=\Iff
\def\Implies{\penalty-35\mskip 6mu plus 2mu minus 1mu \Rightarrow
        \mskip 6mu plus 2mu minus 1mu}
\let\implies=\Implies
% see changeOtherMathcodes for \Or
\let\And=\land
\let\@and=\and
\def\and{\ifmmode\And\else\@and\fi}
%  use \neg for logical not, or
\def\Not{\neg\,}

%       quantification
%

\DeclareMathSymbol{\Exists}   {\mathord}{symbols}{"39}
\DeclareMathSymbol{\Forall}   {\mathord}{symbols}{"38}
\DeclareMathSymbol{\suchthat} {\mathbin}{symbols}{"01}

\def\exists{\@ifstar{\@splitExists}{\@normalExists}}
\ifams@
  \DeclareMathSymbol{\@nexists} {\mathop}{AMSb}{"40}
               % crossed out existential quantifier
\else
  \def\@nexists{\hbox to 0pt{\raise0.15ex\hbox{/}\hss}\Exists}
\fi
\def\nexists{\@ifstar{\@splitNExists}{\@normalNExists}}
\def\forall{\@ifstar{\@splitForall}{\@normalForall}}
\def\unique{\@ifstar{\@splitUnique}{\@normalUnique}}
\def\uniqueval{\@ifstar{\@splitUniqueval}{\@normalUniqueval}}

\def\@normalExists#1#2{{\Exists#1}\suchthat #2}
\def\@normalNExists#1#2{{\@nexists#1}\suchthat #2}
\def\@normalForall#1#2{{\Forall#1}\suchthat #2}
\def\@normalUnique#1#2{{\Exists!\,#1}\suchthat #2}
\def\@normalUniqueval#1#2{{\iota\,#1}\suchthat #2}

\def\@splitExists#1{\@belowAndIndent{\Exists#1\suchthat}}
\def\@splitNExists#1{\@belowAndIndent{\@nexists#1\suchthat}}
\def\@splitForall#1{\@belowAndIndent{\Forall#1\suchthat}}
\def\@splitUnique#1{\@belowAndIndent{\Exists!\,#1\suchthat}}
\def\@splitUniqueval#1{\@belowAndIndent{\iota\,#1\suchthat}}
%
%       sequents
%
\let\Tstlp=\vdash
%
\def\sequent{\@ifstar{\@splitSequent}{\@normalSequent}}
\def\@normalSequent#1#2{{#1}\:\Tstlp\: #2}
\def\@splitSequent#1{\@belowAndIndent{#1\;\Tstlp}}

%
%       strachey brackets
%
% (see TeXbook, p.437)
\def\term#1{[\mkern-\thinmuskip[#1\relax]\mkern-\thinmuskip]}

%       function composition
%
\let\compf=\circ

%----------------------------------------------------------------
%
%       function environment
%
% This environment is similar to the op environment, but is used for
% function definition.
%
% The mandatory first parameter is the name of the function, the
% second is the argument list.
%
% The *-form simply doesn't force the parentheses round the argument list

\def\fn{\parens@true\@beginVDMfunction}
\@namedef{fn*}{\parens@false\@beginVDMfunction}
\@namedef{endfn*}{\endfn}

% short form
\def\vdmfn{\vdm\parens@true \@beginVDMfunction}
\def\endvdmfn{\endfn\endvdm}
\@namedef{vdmfn*}{\vdm\parens@false \@beginVDMfunction}
\@namedef{endvdmfn*}{\endfn\endvdm}

% registers used within the fn environment
\newtoks\@fnName
\newbox\@fnNameBox
\newif\ifsignatureEncountered@
\newtoks\@signatureTokens
\newbox\@fnDefnBox
\newif\ifparens@

\def\@beginVDMfunction#1#2{%
        \@fnName={#1}%
        \setbox\@fnNameBox=\hbox{$#1$}%
        \setbox\@preConditionBox=\box\voidb@x % for people who want to do
        \setbox\@postConditionBox=\box\voidb@x% implicit defns
        \@signatureTokens={}\signatureEncountered@false
        \ifparens@
                \@argumentListTokens={(#2)}%
        \else
                \@argumentListTokens={#2}%
        \fi
        \par\preFunctionHook
        \vskip\preFunctionSkip
        \@beginVerticalVDM
        \@beginFnDefn}

% read in a signature
\def\signature{\global\signatureEncountered@true \global\@signatureTokens=}

\def\@beginFnDefn{\global\setbox\@fnDefnBox=\vtop\bgroup
        \hangindent=2em \hangafter=1 \@beginHorizontalVDM
        \advance\hsize by-2em % this fools vboxes within the
        % function body about the hanging indent...yuk.
        % If you change the size of the indent, change the
        % corresponding line in \endfn.
        \copy\@fnNameBox \the\@argumentListTokens
        \quad\DEF\penalty-100\quad }

\newskip\preFunctionSkip \preFunctionSkip=2ex plus .5ex minus .2ex
\newskip\postFunctionSkip \postFunctionSkip=2ex plus .5ex minus .2ex
\newskip\betweenSignatureAndBodySkip
\betweenSignatureAndBodySkip=1.2ex plus .3ex minus .2ex
\newskip\betweenFunctionAndPreSkip
\betweenFunctionAndPreSkip=1.2ex plus .3ex minus .2ex

\def\endfn{%
        \advance\hsize by 2em% matches the dirty \advance in \@beginFnDefn
        \@endHorizontalVDM
        \egroup  % this ends the vtop we started in \@beginFnDefn
        \ifsignatureEncountered@
                \setbox0=\hbox{\unhbox\@fnNameBox$\;\mathpunct:\,$}%
                \dimen255=\wd0 \noindent \box0
                \vtop{\advance\hsize by-\dimen255 \@beginHorizontalVDM
                        \the\@signatureTokens \@endHorizontalVDM}\par
                \betweenSignatureAndBodyHook
                \vskip\betweenSignatureAndBodySkip
        \fi
        \moveright\VDMindent\box\@fnDefnBox\,
        \ifvoid\@preConditionBox
              \betweenPreAndPostConditionHook
              \vskip\postFunctionSkip
        \else \betweenFunctionAndPreHook
              \vskip\betweenFunctionAndPreSkip
              \moveright\VDMindent\box\@preConditionBox
              \betweenPreAndPostConditionHook
              \vskip\postPreConditionSkip
        \fi
        \ifvoid\@postConditionBox
              \postFunctionHook
        \else \moveright\VDMindent\box\@postConditionBox
              \postFunctionHook
              \vskip\postOperationSkip
        \fi}

\newcount\preFunctionPenalty \preFunctionPenalty=0
\newcount\betweenSignatureAndBodyPenalty
 \betweenSignatureAndBodyPenalty=10000
\newcount\betweenFunctionAndPrePenalty \betweenFunctionAndPrePenalty=1000
\newcount\postFunctionPenalty \postFunctionPenalty=-500

% These are called in outer vertical mode---they must also exit in this mode
\def\preFunctionHook{\penalty\preFunctionPenalty }
\def\betweenSignatureAndBodyHook{\penalty\betweenSignatureAndBodyPenalty }
\def\betweenFunctionAndPreHook{\penalty\betweenFunctionAndPrePenalty }
\def\postFunctionHook{\penalty\postFunctionPenalty }

%       other function-related things
%

% function arrow
\def\to{\penalty-100\rightarrow}

% explicit lamdba function
\def\LambdaFn{\@ifstar{\@splitLambdaFn}{\@normalLambdaFn}}
\def\@normalLambdaFn#1#2{{\lambda#1}\suchthat#2}
\def\@splitLambdaFn#1#2{% place body in a separate box below and to the right
        {\lambda#1}\suchthat\hfil\break
        \@mathIndentedPara{\hsize}{\qquad}{#2}}

%----------------------------------------------------------------
%
%       Optional fields
%
\def\Opt#1{\big[#1\big]}


%----------------------------------------------------------------
%
%       Sets

% new set type
\def\setof#1{#1-\kw{set}}

% set enumeration
\def\set#1{\{#1\}}

% empty set
\def\emptyset{\{\,\}}

% usual LaTeX operators apply: \in \notin \subset \subseteq
\let\inter=\cap \let\intersection=\inter
\let\Inter=\bigcap \let\Intersection=\Inter
\let\union=\cup
\let\Union=\bigcup

\mathchardef\minus="2200

\def\diff{\minus} \let\difference=\diff

\newMonadicOperator{\card}{card}
\newMonadicOperator{\Min}{min}
\newMonadicOperator{\Max}{max}
\newMonadicOperator{\abs}{abs}

%----------------------------------------------------------------
%
%       Map type

% new map type
\def\mapof#1#2{#1\buildrel m\over\longrightarrow#2}

% one-one map
\def\mapinto#1#2{#1\buildrel m\over\longleftrightarrow#2}

% map enumeration
\def\map#1{\{#1\}}

% empty map
\def\emptymap{\{\,\}}

%       map operators
%
% use \mapsto for |->
% overwrite
\def\owr{\dagger}

\let\dres=\lhd
\let\rres=\rhd


% domain subtraction
\def\dsub{\mathbin{\hbox{$\rlap{$\mathord\minus$}\mkern-1.5mu
        \lower.1ex\hbox{$\dres$}$}}}

% range subtraction
\def\rsub{\mathbin{\hbox{$\rlap{$\mathord\minus$}\mkern-1.5mu
        \lower.1ex\hbox{$\rres$}$}}}

\newMonadicOperator{\dom}{dom}
\newMonadicOperator{\rng}{rng}
\newMonadicOperator{\merge}{merge}

%----------------------------------------------------------------
%
%       Sequences
%

% new type
\def\seqof#1{#1^*}

% non-empty sequence
\def\neseqof#1{#1^+}

% enumeration
\def\seq#1{[#1]}

% empty sequence
\def\emptyseq{[\,]}

\newMonadicOperator{\len}{len}
\newMonadicOperator{\hd}{hd}
\newMonadicOperator{\tl}{tl}
\newMonadicOperator{\elems}{elems}
\newMonadicOperator{\inds}{inds}
\def\cons#1{\kw{cons}\nobreak(#1)}

% sequence concatenation

\DeclareMathSymbol{\@sc@nc} {\mathbin}{AMSb}{"79}

\ifams@
  \def\sconc{\mathbin{\hbox{\raise1ex\hbox{$\@sc@nc$}}}}
\else
  % this is truly yukky
  \def\sconc{\mathbin{\hbox{\raise1ex\hbox{$\frown$}\kern-0.47em
        \raise0.2ex\hbox{\it\char"12}}}}
\fi

% distributed concatenation
\newMonadicOperator{\Conc}{dconc}

%----------------------------------------------------------------
%
%       type equation
%
\newtoks\@typeName
\def\type#1#2{{\@typeName{#1} \preTypeHook \vskip\preTypeSkip
        \@beginVerticalVDM
        \moveright\VDMindent\vtop{\@beginHorizontalVDM #1=#2%
                \@endHorizontalVDM}
        \postTypeHook \vskip\postTypeSkip}}

% restricted type (has invariant)
\def\rtype#1#2#3{{\@typeName{#1} \preTypeHook \vskip\preTypeSkip
        \@beginVerticalVDM
        \moveright\VDMindent\vtop{\@beginHorizontalVDM #1=#2%
                \@endHorizontalVDM}
        \vskip\betweenTypeAndInvSkip
        \moveright\VDMindent\@mathIndentedPara{\hsize}{inv }{#3}%
        \postTypeHook \vskip\postTypeSkip}}

% initialised type
\def\ritype#1#2#3#4{{\@typeName{#1} \preTypeHook \vskip\preTypeSkip
        \@beginVerticalVDM
        \moveright\VDMindent\vtop{\@beginHorizontalVDM #1=#2%
                \@endHorizontalVDM}
        \vskip\betweenTypeAndInvSkip
        \moveright\VDMindent\@mathIndentedPara{\hsize}{inv }{#3}%
        \vskip\betweenInvAndInitSkip
        \moveright\VDMindent\@mathIndentedPara{\hsize}{init }{#4}%
        \postTypeHook \vskip\postTypeSkip}}

\def\preTypeHook{} \def\postTypeHook{}
\newskip\preTypeSkip \preTypeSkip=1.2ex plus .5ex minus .3ex
\newskip\postTypeSkip \postTypeSkip=1.2ex plus .5ex minus .3ex
\newskip\betweenTypeAndInvSkip
  \betweenTypeAndInvSkip=.5ex plus .3ex minus .2ex
\newskip\betweenInvAndInitSkip
  \betweenInvAndInitSkip=.5ex plus .3ex minus .2ex

%----------------------------------------------------------------
%
%       Composite Objects
%

% literal composition; we have a compose and a composite env.

% single line compose
\@namedef{composite*}#1{\kw{compose }$\relax#1\relax$\kw{ of }$\relax}
\@namedef{endcomposite*}{\relax$\kw{ end}}

% multiple line version
\def\composite#1{\bgroup\vskip\preCompositeSkip
    \@beginVerticalVDM
    \moveright\VDMindent\vtop\bgroup
        \@beginHorizontalVDM
        \kw{compose }#1\kw{ of}%
        \@endHorizontalVDM
        \@makeColonActive\@changeLineSeparator
        \expandafter\halign\expandafter\bgroup\expandafter\qquad
                \the\@recordAlign\strut\enspace&:\enspace$##$\hfil\cr}
\def\endcomposite{\crcr\egroup % closes \halign
        \kw{end}\egroup % ends the \vtop
        \vskip\postCompositeSkip\egroup}

\def\scompose#1#2{\@nameuse{composite*}{#1}{#2}\@nameuse{endcomposite*}}

\newskip\preCompositeSkip \preCompositeSkip=1.2ex plus .5ex minus .3ex
\newskip\postCompositeSkip \postCompositeSkip=1.2ex plus .5ex minus .3ex

% record composites; likewise we have a short and a long form
\newtoks\@recordName

\def\record#1{%
  \InvEncountered@false \InitEncountered@false
  \@invTokens={}\@initTokens={}
  \@recordName{#1}
  \par\preRecordHook
  \vskip\preRecordSkip
  \@beginVerticalVDM
  \moveright\VDMindent\hbox\bgroup
          \setbox0=\hbox{$#1$\enspace::\enspace}%
          \@makeColonActive\@changeLineSeparator
          \advance\hsize by-\wd0 \box0
          \@restoreMargins
          %
          % the \expandafters are necessary because TeX doesn't expand
          % \halign specs when scanning for # and &
          \vtop\bgroup\expandafter\halign\expandafter\bgroup
                  \the\@recordAlign\strut\enspace&:\enspace$##$\hfil\cr}

\def\endrecord{\crcr\egroup% closes halign
        \egroup% closes vtop
        \egroup% closes hbox
  \ifInvEncountered@
        \betweenRecordAndInvHook
        \vskip\betweenRecordAndInvSkip
        \moveright\VDMindent\@mathIndentedPara{\hsize}{inv }{%
                \the\@invTokens}
  \fi
  \ifInitEncountered@
        \betweenInvAndInitHook
        \vskip\betweenInvAndInitSkip
        \moveright\VDMindent\@mathIndentedPara{\hsize}{init }{%
                \the\@initTokens}
  \fi
  \par\postRecordHook
  \vskip\postRecordSkip}

\def\inv{\global\InvEncountered@true \global\@invTokens=}
\def\init{\global\InitEncountered@true \global\@initTokens=}

\newif\ifInvEncountered@
\newif\ifInitEncountered@
\newtoks\@invTokens
\newtoks\@initTokens
\def\betweenRecordAndInvHook{}
\def\betweenInvAndInitHook{}
\newskip\betweenRecordAndInvSkip
  \betweenRecordAndInvSkip=0.5ex plus 0.2ex minus 0.1ex
\newskip\betweenInvAndInitSkip
  \betweenInvAndInitSkip=0.5ex plus 0.2ex minus 0.1ex

% the user can decide on the exact alignment of the field names
\newtoks\@recordAlign
\def\leftRecord{\@recordAlign={$##$\hfil}}
\def\rightRecord{\@recordAlign={\hfil$##$}}
\rightRecord

% more catcode trickery
\def\defrecord{\bgroup\@makeColonActive\@defrecord}
\def\@defrecord#1#2{\record{#1}#2\endrecord\egroup}

\newskip\preRecordSkip \preRecordSkip=.75ex plus .3ex minus .2ex
\newskip\postRecordSkip \postRecordSkip=.75ex plus .3ex minus .2ex
\newcount\preRecordPenalty \preRecordPenalty=0
\newcount\postRecordPenalty \postRecordPenalty=-100
\def\preRecordHook{\penalty\preRecordPenalty }
\def\postRecordHook{\penalty\postRecordPenalty }

% \chg: mu function on composites
\def\chg#1#2#3{\mu(#1,#2\mapsto#3)}

%----------------------------------------------------------------
%
%       Hooks
%
% hooked identifiers --- these are taken from the TeXbook, p.357, 359
\def\leftharpoonupfill{$\m@th \mathord\leftharpoonup \mkern-6mu
  \cleaders\hbox{$\mkern-2mu \mathord\minus \mkern-2mu$}\hfill
  \mkern-6mu \mathord\minus$}  % p.357, \leftarrowfill

\def\overleftharpoonup#1{{%
  \boxmaxdepth=\maxdimen % this fixes Lamport's figures, but isn't necessary
                         % for versions after 15 Dec 87
  \vbox{\ialign{##\crcr % p.359, \overleftarrow
    \leftharpoonupfill\crcr\noalign{\kern-\p@\nointerlineskip}
    $\hfil\displaystyle{#1}\hfil$\crcr}}}}

\let\hook=\overleftharpoonup  % c'est simple comme bonjour

%-----------------------------------------------------------------
%
%       General formula environment, a bit like \[ \] but is
%       indented to \VDMindent and will take \\
%
%
\def\form#1{\formula #1\endformula}

\def\formula{\par\preFormulaHook
        \vskip\preFormulaSkip
        \@beginVerticalVDM
        \bgroup
        \moveright\VDMindent\vtop\bgroup\@beginHorizontalVDM}
\def\endformula{\@endHorizontalVDM\egroup % ends the vtop
        \egroup % ends the overall group
        \par\postFormulaHook
        \vskip\postFormulaSkip}

\newskip\preFormulaSkip \preFormulaSkip=1.2ex plus .5ex minus .3ex
\newskip\postFormulaSkip \postFormulaSkip=1.2ex plus .5ex minus .3ex
\newcount\preFormulaPenalty \preFormulaPenalty=0
\newcount\postFormulaPenalty \postFormulaPenalty=-100
\def\preFormulaHook{\penalty\preFormulaPenalty }
\def\postFormulaHook{\penalty\postFormulaPenalty }

%----------------------------------------------------------------
%
%       Formula within a box, when width is unknown
%
%       equivalent to \parbox[t]{\hsize}{\@beginHorizontalVDM
%               ...\@endHorizontalVDM}
%
\def\formbox{\vtop\bgroup\@beginHorizontalVDM}
\def\endformbox{\strut\@endHorizontalVDM\egroup}

%----------------------------------------------------------------
%
%       special font for constants
%
\def\constantFont{\sc}
\def\const#1{\hbox{\constantFont{#1}\/}}

%----------------------------------------------------------------
%
%       line break and indent
%
\def\T#1{\\\hbox to #1em{}}

%----------------------------------------------------------------
%
%       line break and push line after to RHS
%
\def\R{\\\hspace*{\fill}}

%----------------------------------------------------------------
%
%       Proofs
%
% a proof environment for typesetting proofs in the "natural
% deduction" style.

\newdimen\ProofIndent \ProofIndent=\VDMindent
\newdimen\ProofNumberWidth \ProofNumberWidth=\parindent

\def\proof{\par\preProofHook
        \vskip\preProofSkip
        \let\&=\@proofLine
        \moveright\ProofIndent\vtop\bgroup
                \@indentLevel=1
                \advance\linewidth by-\ProofIndent
                \begin{tabbing}%
                \hbox to\ProofNumberWidth{}\=\kill}     % template line
\def\endproof{\end{tabbing}\advance\linewidth by\ProofIndent
        \egroup % ends the \vtop
        \par\postProofHook
        \vskip\postProofSkip}

\newskip\preProofSkip \preProofSkip=1.2ex plus .5ex minus .3ex
\newskip\postProofSkip \postProofSkip=1.2ex plus .5ex minus .3ex

\newcount\preProofPenalty \preProofPenalty=-100
\newcount\postProofPenalty \postProofPenalty=0
\def\preProofHook{\penalty\preProofPenalty }
\def\postProofHook{\penalty\postProofPenalty }

\def\From{\@indentProof\kw{from }\=%
        \global\advance\@indentLevel by 1
        \@enterMathMode}
\def\Infer{\global\advance\@indentLevel by-1
        \@indentProof\kw{infer }\@enterMathMode}
\def\@proofLine{\@indentProof\@enterMathMode}
\def\by{\`}

\newcount\@indentLevel
\newcount\@indentCount
\def\@indentProof{% do \>, \@indentLevel times
        \global\@indentCount=\@indentLevel
        \@gloop \>\global\advance\@indentCount by-1
        \ifnum\@indentCount>0
        \repeat}

% need special loop macros that works in across boxes
\def\@gloop#1\repeat{\gdef\@body{#1}\@giterate}
\def\@giterate{\@body \global\let\@gloopNext=\@giterate
        \else \global\let\@gloopNext=\relax \fi \@gloopNext}

% this enters math mode and sets the LaTeX macros \@stopfield up
% to exit math mode
\def\@enterMathMode{\def\@stopfield{$\egroup}$}

%----------------------------------------------------------------
\def\VDMauthor{M.Wolczko,
CS Dept.,
Univ. of Manchester, UK.
mario@cs.man.ac.uk
uknet!man.cs!mario}

\def\VDMversion{vdm3.0}

\typeout{BSI VDM style option <9 Jun 1992>}
%----------------------------------------------------------------
%
%       Global changes
%
% All things that have to be invoked before the user's stuff appears
% should go here.
%
% by default the math spacing and changes to @ and _ apply everywhere
\@changeOtherMathcodes \@changeGlobalCatcodes
%
%-------------------the end--------------------------------------
\endinput
%
%       Summary of penalties
%
%       Penalties in vertical mode
%
% \preOperationPenalty          before an op begins
% \preExternalPenalty           between the header and externals of an op
% \prePreConditionPenalty       before the precondition
% \prePostConditionPenalty      before the postcondition
% \postOperationPenalty         at the end of an op
%
% \preFunctionPenalty           before a fn begins
% \betweenSignatureAndBodyPenalty -guess
% \postFunctionPenalty          after a fn ends
%
% \preRecordPenalty             before a record
% \postRecordPenalty            after a record
%
%       etc for formula, proof
%
%       Penalties in horizontal mode in boxes
%
% \linepenalty                  101             \@raggedRight
% `if mm-exp ^ then..'          0               \SIf
% `if ... then mm-exp ^ else'   -100            \SIf
% `let mm-exp in ^ ...'         -100            \SLet
% `map mm-exp ^ to ...'         -50             \map
% ^\iff                         -50             \iff
% ^\implies                     -35             \implies
% func(args) \DEF^              -100            \begin{fn}
% \binoppenalty                 10000
% \relpenalty                   10000
% \hyphenpenalty                -100            \suchthat
% ^\to                          -100            \to
% _^                            100             \@VDMunderscore
%