diff options
author | Karl Berry <karl@freefriends.org> | 2006-07-10 21:24:34 +0000 |
---|---|---|
committer | Karl Berry <karl@freefriends.org> | 2006-07-10 21:24:34 +0000 |
commit | ac151dac1f876a711cd50b4127c3c5aa8e837556 (patch) | |
tree | 622db4347270a735b6aefdf88f1b6954526665a1 /Master/texmf-dist/tex | |
parent | a9018e6c8e9ffc9fdf4f881ab4726e90c01508d9 (diff) |
remove vdm package, since license is unstated, author apparently uncontactable, ancient stuff anyway
git-svn-id: svn://tug.org/texlive/trunk@1808 c570f23f-e606-0410-a88d-b1316a301751
Diffstat (limited to 'Master/texmf-dist/tex')
-rw-r--r-- | Master/texmf-dist/tex/latex/vdm/vdm.sty | 1185 |
1 files changed, 0 insertions, 1185 deletions
diff --git a/Master/texmf-dist/tex/latex/vdm/vdm.sty b/Master/texmf-dist/tex/latex/vdm/vdm.sty deleted file mode 100644 index 8ff0260c04a..00000000000 --- a/Master/texmf-dist/tex/latex/vdm/vdm.sty +++ /dev/null @@ -1,1185 +0,0 @@ -%%% ==================================================================== -%%% @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 -% |