%\iffalse metacomment
%  (c)1995--1996 Peter M›ller Neergaard
%  This files must be distributed, installed and used freely. You especially
%  welcome to get inspiration (if possible) from the source code.
%
%  Install by running tex with "semantic.ins".  
% 
%  To get the documentation run latex twice on this file and then print the 
%  file semantic.dvi.
%
%  This file is distributed in the hope that it will be useful,
%  but WITHOUT ANY WARRANTY; without even the implied warranty of
%  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. 
%\fi
% \CheckSum{1040}
% \CharacterTable
%  {Upper-case    \A\B\C\D\E\F\G\H\I\J\K\L\M\N\O\P\Q\R\S\T\U\V\W\X\Y\Z
%   Lower-case    \a\b\c\d\e\f\g\h\i\j\k\l\m\n\o\p\q\r\s\t\u\v\w\x\y\z
%   Digits        \0\1\2\3\4\5\6\7\8\9
%   Exclamation   \!     Double quote  \"     Hash (number) \#
%   Dollar        \$     Percent       \%     Ampersand     \&
%   Acute accent  \'     Left paren    \(     Right paren   \)
%   Asterisk      \*     Plus          \+     Comma         \,
%   Minus         \-     Point         \.     Solidus       \/
%   Colon         \:     Semicolon     \;     Less than     \<
%   Equals        \=     Greater than  \>     Question mark \?
%   Commercial at \@     Left bracket  \[     Backslash     \\
%   Right bracket \]     Circumflex    \^     Underscore    \_
%   Grave accent  \`     Left brace    \{     Vertical bar  \|
%   Right brace   \}     Tilde         \~}
%
% ^^A I do not want the LaTeX-commands in the index
% ^^A This is borrowed from the standard package ``doc.dtx'' 
% \DoNotIndex{\@,\@@par,\@beginparpenalty,\@empty}
% \DoNotIndex{\@flushglue,\@gobble,\@input}
% \DoNotIndex{\@makefnmark,\@makeother,\@maketitle}
% \DoNotIndex{\@namedef,\@ne,\@spaces,\@tempa}
% \DoNotIndex{\@tempb,\@tempswafalse,\@tempswatrue}
% \DoNotIndex{\@thanks,\@thefnmark,\@topnum}
% \DoNotIndex{\@@,\@elt,\@forloop,\@fortmp,\@gtempa,\@totalleftmargin}
% \DoNotIndex{\",\/,\@ifundefined,\@nil,\@verbatim,\@vobeyspaces}
% \DoNotIndex{\|,\~,\ ,\active,\advance,\aftergroup,\begingroup,\bgroup}
% \DoNotIndex{\mathcal,\csname,\def,\documentstyle,\dospecials,\edef}
% \DoNotIndex{\egroup}
% \DoNotIndex{\else,\endcsname,\endgroup,\endinput,\endtrivlist}
% \DoNotIndex{\expandafter,\fi,\fnsymbol,\futurelet,\gdef,\global}
% \DoNotIndex{\hbox,\hss,\if,\if@inlabel,\if@tempswa,\if@twocolumn}
% \DoNotIndex{\ifcase}
% \DoNotIndex{\ifcat,\iffalse,\ifx,\ignorespaces,\index,\input,\item}
% \DoNotIndex{\jobname,\kern,\leavevmode,\leftskip,\let,\llap,\lower}
% \DoNotIndex{\m@ne,\next,\newpage,\nobreak,\noexpand,\nonfrenchspacing}
% \DoNotIndex{\obeylines,\or,\protect,\raggedleft,\rightskip,\rm,\sc}
% \DoNotIndex{\setbox,\setcounter,\small,\space,\string,\strut}
% \DoNotIndex{\strutbox}
% \DoNotIndex{\thefootnote,\thispagestyle,\topmargin,\trivlist,\tt}
% \DoNotIndex{\twocolumn,\typeout,\vss,\vtop,\xdef,\z@}
% \DoNotIndex{\,,\@bsphack,\@esphack,\@noligs,\@vobeyspaces,\@xverbatim}
% \DoNotIndex{\`,\catcode,\end,\escapechar,\frenchspacing,\glossary}
% \DoNotIndex{\hangindent,\hfil,\hfill,\hskip,\hspace,\ht,\it,\langle}
% \DoNotIndex{\leaders,\long,\makelabel,\marginpar,\markboth,\mathcode}
% \DoNotIndex{\mathsurround,\mbox,\newcount,\newdimen,\newskip}
% \DoNotIndex{\nopagebreak}
% \DoNotIndex{\parfillskip,\parindent,\parskip,\penalty,\raise,\rangle}
% \DoNotIndex{\section,\setlength,\TeX,\topsep,\underline,\unskip,\verb}
% \DoNotIndex{\vskip,\vspace,\widetilde,\\,\%,\@date,\@defpar}
% \DoNotIndex{\[,\{,\},\]}
% \DoNotIndex{\count@,\ifnum,\loop,\today,\uppercase,\uccode}
% \DoNotIndex{\baselineskip,\begin,\tw@}
% \DoNotIndex{\a,\b,\c,\d,\e,\f,\g,\h,\i,\j,\k,\l,\m,\n,\o,\p,\q}
% \DoNotIndex{\r,\s,\t,\u,\v,\w,\x,\y,\z,\A,\B,\C,\D,\E,\F,\G,\H}
% \DoNotIndex{\I,\J,\K,\L,\M,\N,\O,\P,\Q,\R,\S,\T,\U,\V,\W,\X,\Y,\Z}
% \DoNotIndex{\1,\2,\3,\4,\5,\6,\7,\8,\9,\0}
% \DoNotIndex{\!,\#,\$,\&,\',\(,\),\+,\.,\:,\;,\<,\=,\>,\?,\_}
% \DoNotIndex{\discretionary,\immediate,\makeatletter,\makeatother}
% \DoNotIndex{\meaning,\newenvironment,\par,\relax,\renewenvironment}
% \DoNotIndex{\repeat,\scriptsize,\selectfont,\the,\undefined}
% \DoNotIndex{\arabic,\do,\makeindex,\null,\number,\show,\write,\@ehc}
% \DoNotIndex{\@author,\@ehc,\@ifstar,\@sanitize,\@title,\everypar}
% \DoNotIndex{\if@minipage,\if@restonecol,\ifeof,\ifmmode}
% \DoNotIndex{\lccode,\newtoks,\onecolumn,\openin,\p@,\SelfDocumenting}
% \DoNotIndex{\settowidth,\@resetonecoltrue,\@resetonecolfalse,\bf}
% \DoNotIndex{\clearpage,\closein,\lowercase,\@inlabelfalse}
% \DoNotIndex{\selectfont,\mathcode,\newmathalphabet,\rmdefault}
% \DoNotIndex{\bfdefault}
%
% ^^A I also exclude the commands used to generate the index
% \DoNotIndex{\CodelineIndex,\DeleteShortVerb,\DisableCrossrefs}
% \DoNotIndex{\EnableCrossrefs,\OnlyDescription,\RecordChanges}
%
% \MakeShortVerb{\"}
%
% \GetInfo{semantic.sty}
% \title{The \semantic-package\thanks
%  {This file has version \fileversion\ and is dated \filedate}}
% \author{Peter M›ller Neergaard \\ 
%   \texttt{turtle}@\texttt{diku.dk} \quad \texttt{http://www.diku.dk/students/turtle}}
%
% \maketitle
%
% \begin{abstract}
%   This package provides commands that eases the notation of semantics and
%   compilers in your documents. The notation implemented is primarily that
%   used in \emph{Introduction to the Semantics for Programming Languages}
%   teached at the Department of Computer Science at the University of
%   Copenhagen in fall '95.
% \end{abstract}
%
% ^^A Table of contents in two columns --- borrowed from the standard 
% ^^A package of ``doc.dtx''
% \ifmulticols
%   \addtocontents{toc}{\protect\begin{multicols}{2}}
% \fi
%
% {\parskip 0pt                ^^A We have to reset \parskip (bug in \LaTeX)
% \sloppy
% \tableofcontents
% }
%
% \ifmulticols
%   \begin{multicols}{2}[\noindent \medskip \rule{\textwidth}{.3pt}]
% \fi
% 
% \noindent
% \semantic\ is a \LaTeXe-package easying the writing of notation of
% semantics and compilers. To use it the file \texttt{semantic.sty} should be
% placed, so that \LaTeX\ can find it. In your document preamble you should
% include "\usepackage{semantic}"
% 
% In the following I will describe the use of the different parts of
% \semantic: symbols, inference rules and translation diagrams. There is also a
% section describing the installation and giving a short introduction to the
% two files \texttt{semantic.dtx} and \texttt{semantic.ins}.
% 
% Like most other computer-programs, I have provided this package with
% several bugs, insuffiencies and inconsistencies. These should be regarded
% as features of the package. To increase the excitement of using the package
% these features appear in---even to me---unpredictable places. If they 
% however get to annoying and seriously reduce your satisfaction with 
% \semantic\ then please notify me. You could also drop me a note, if you 
% would like to be informed, when I update \semantic.
% 
% In continuation of this I will espcially draw your attention to two
% troublesome areas: the syntax and the documentation. When laying down the
% syntax I have tried to satisfy to contrary considerations: to use the
% well-known \LaTeX-syntax and to give a syntax, that is easy typed and read.
% This has lead to some compromises, which most probaply satisfy neither. And
% being dane and therefore not native english-speaking it is even harder than
% normal to express clearly in the documentation, what my intention was. Any
% feedback would therefore be greatly appreciated. 
% 
% A last---and compulsary---part is a special thanks to Jesper Groth
% L›hr, who has been $\beta$-tester of several versions leading
% to many improvements. 
% ^^A and Kai Neeg†rd, who read and commented the documentation.
% 
% \ifmulticols
%   \end{multicols}
% \fi
%
% \iffalse^^A At the moment I do not know of any bugs
%   \ifmulticols
%     \begin{multicols}{2}[\section*{Known Bugs}
%   \fi
%   \begin{columnItemize} 
%   \end{columnItemize}
%
%   \ifmulticols
%     \end{multicols}
%   \fi
% \fi
% 
% \section{Symbols}
% 
% \DescribeMacro{\eval} 
% \DescribeMacro{\comp} 
% To support writing denotational semantics the commands "\comp" and "\eval"
% are provided to describe the evaluation of programs respectively
% expressions. They have the same syntax:
% "\comp{"\meta{command}"}{"\meta{environment}"}", which yields
% \comp{\meta{command}}{\meta{environment}}.  If you need to describe more
% than one kind of evaluations, e.g.\ both \evalsymbol\ and \evalsymbol[*],
% you can provide an optional argument immediately after "\comp" respectively
% "\eval". As an example a denotational rule for a sequenciliasing of two
% commands
% \[
% \comp{C1 ; C2}{d} = \mathtt{d'} \quad \texttt{if $\comp{C1}{d} = \mathtt{d''}$ and $\comp{C2}{d''} = \mathtt{d'}$}
% \]
% can be typed
% \begin{code}
%   "\["\\
%   "  \comp{C1 ; C2}{d} = \mathtt{d'} \quad "\\
%   "   \texttt{if $\comp{C1}{d} = \mathtt{d''}$ and"\\
%   "              $\comp{C2}{d''} = \mathtt{d'}$}"\\
%   "\]"
% \end{code}
% 
% \DescribeMacro{\evalsymbol}
% \DescribeMacro{\compsymbol}
% As shown above you can get the evaluationsymbol in it self. This is done by
% "\compsymbol" respectively "\evalsymbol". These commands can also be
% supplied with an optional argument, e.g.\ "\evalsymbol[*]" to get
% \evalsymbol[*].
% 
% \DescribeMacro{\exe} 
% The result of executing a program on a machine with som data can be
% described using "\exe", which has the syntax
% "\exe{"\meta{program}"}["\meta{machine}"]{"\meta{data}"}", where the
% \meta{machine} as indicated is optional. The third Futumara projection
% $\mathtt{cogen} = \exe{spec}{spec.spec}$ can using the "\exe"-command be
% written "$\mathtt{cogen} = \exe{spec}{spec.spec}$". Or you can give an
% explicit machine \texttt{L}: "$\mathtt{cogen} = \exe{spec}[L]{spec.spec}$"
% and you will then get
%   $\mathtt{cogen} = \exe{spec}[L]{spec.spec}$
% 
% \DescribeEnv{inferencesymbols}
% \begin{inferencesymbols}
%   When writing inference rules, proofs etc.\ the symbols |-, |=, -> and =>
%   are often used extensively. Normally they are only available in mathematics
%   ("$"\lttdots"$") and you therefore need to key in lengthy and cumbersome
%   commands. In the "inferencesymbol"-environment ("\begin{inferencesymbols}"
%   \lttdots\ "\end{inferencesymbols}") these symbols are provided as
%   ``ligatures'' of "|-", "|=", "->" and "=>", which is available in both
%   mathematics and text. By typing a "*" or "+" after "->" or "=>" you get the
%   ``starred'' and ``plussed'' versions: ->*, =>*, ->+ and =>+.
%         
%   In the "inferencesymbols"-environment the vast majority of \LaTeX-commands
%   works normally. It is however not possible to ensure, that the symbols "|",
%   "-" and "=" works 100\% like outside the environment\footnote{Inside the
%     environment "|", "-" and "=" are defined as macros. These macros examens
%     the next character and if it is "-" or "=", ">" and ">" respectively, the
%     command for the ligature, e.g.\ "\$"\CSname{vdash}"\$" for
%     \texttt{{|}-} is returned. Otherwise the characters from outside the
%     environment is returned (both the character and catcode).},
%   and for instance "\cline{"\lttdots"-"\lttdots"}" cannot be used in this
%   environment (it however works if it is part of a command defined
%   \emph{outside} the environment).
% \end{inferencesymbols}
%
% \section{Inference Rules}
% 
% \DescribeMacro{\inference}
% Inference rules like
% {\def\predicatebegin#1|-#2=>#3\predicateend{$#1 \vdash \texttt{#2} \Rightarrow #3$}
%   \[
%   \textrm{It(1) : }
%     \inference{\rho|-$E$=>\textsc{True} & \rho|-$s$=>\rho' \\
%                \rho'|-while $E$ do $s$=>\rho''}^^A
%     {\rho|-while $E$ do $s$=>\rho''}
% \;\;\;\;
%   \textrm{It(2) : }
%     \inference{\rho|-$E$=>\textsc{False}}
%     {\rho|-while $E$ do $s$=>\rho } 
% \]}
% and
% \begin{inferencesymbols}
% \[
%   \inference[$->*_1$]{$p$,M ->* $p'$,M$'$ \\ $p'$,M$'$ -> $p''$,M$''$}{$p$,M ->* $p''$,M$''$} \;\;\;\;
%   \inference[$->*_2$]{}{$p$,M ->* $p$,M}
% \]
% \end{inferencesymbols}
% are easily set using "\inference". The syntax is 
% \begin{code}
%   "\inference["\meta{name}"]{"\meta{line$_1$}" \\ "\lttdots" \\ "\meta{line$_n$}"}{"\meta{conclusion}"}" 
% \end{code}
% where $n \geq 0$ so you also can type axioms. Each line consits of premises
% seperated by "&":
% \begin{code}
%   \meta{premise$_1$}"&"\lttdots"&"\meta{premise$_m$}
% \end{code}
% Note that $m$ can also be zero which is used when typing axioms. The 
% optional name is set to the right of the inference.
% 
% The rules is set so the line flush with the center of small letters in the
% surrounding text. In this way secondary conditions or names (like the first
% example above) can be written in the surrounding text. It also makes it
% possible to set the rules in a table like shown here with the last example:
%
% \begin{inferencesymbols}
%   \begin{tabular}{ll}
%     Transitive (1): & 
%      \inference{$p$,M ->* $p'$,M$'$ \\ $p'$,M$'$ -> $p''$,M$''$}{$p$,M ->* $p''$,M$''$} \\
%     Transitive (2): &
%      \inference{}{$p$,M ->* $p$,M}
%   \end{tabular}
%
% An inference rule can unproblematicly be nested within another, like:
% \[
%   \inference[$->*_1$]{
%     \inference[$->*_1$]{
%       \inference[$->*_2$]{}
%       {$p$,M ->* $p$,M} & 
%       $p$,M ->* $p'$,M$'$}
%     {$p$,M ->* $p'$,M$'$} & 
%     $p'$,M' -> $p''$,M$''$}
%   {$p$,M ->* $p''$,M$''$}
% \]
% \end{inferencesymbols}
%
% \DescribeMacro{\setpremisesend}
% \DescribeMacro{\setpremisesspace}
% \DescribeMacro{\setnamespace}
% The appearance of the inferences rules can partly be controlled by the
% following lengths:
% {\makeatletter
%  \setnamespace{3em}
%  \setpremisesend{2em}
%  \setpremisesspace{4em}
%  \[
%   \inference[^^A
%     \llap{\raisebox{0.1em}{$\overbrace{\hskip\@@nSpace}^{\makebox[0pt]{\footnotesize namespace}}$}}^^A
%     name
%   ]{^^A
%     \llap{$\overbrace{\hskip\@@pEnd}^{\makebox[0pt]{\footnotesize premisesend}}$}^^A
%     premise &
%     \llap{$\overbrace{\hskip\@@pSpace}^{\makebox[0pt]{\footnotesize premisesSpace}}$}^^A
%     premise
%   }{
%     conclusion
%   }
%  \]
%  \makeatother^^A
% }^^A
% The lengths are changed using the three commands
% "\setnamespace{"\meta{length}"}", "\setpremisesend{"\meta{length}"}" og
% "\setpremisesspace{"\meta{length}"}". \meta{length} can be given in both
% absolute units like "pt" and "cm" and in relative units like "em" and "ex".
% The default values are: 1$\frac{1}{2}$"em" for "premisesspace",
% $\frac{3}{4}$"em" for "premisesend" og $\frac{1}{2}$"em" for "namespace".
% Note that the lengths \emph{cannot} be altered using the ordinary
% \LaTeX-commands "\setlength" and "\addtolength".
%  
% Besides that the appearance of inference rules is like fractions in math:
% Among other things the premises will \emph{normally} be at same height
% above the baseline and there is a minimum distance from the line to the
% bottom of the premises. The information to set the rules like fraction is
% taken from the current math font.
%
% {\small ^^A This description is only for TeXnichians and it it therefore
%         ^^A written in a smaller fotn.
% \ifdanger \setparagraphmark{\small\danger} ^^A The dangorous bend is 
%                                            ^^A designed to span two lines
%    \parmark
% \else 
%   \setparagraphmark{\bfseries !!}\parmark\footnote{As your installation
%     lacks the ``dangerous bend'' used in \emph{The \TeX-book}, I have 
%     used double exclamation marks to mark, that you do not have to 
%     understand the following paragraphs to use \semantic.}^^A
% \fi
% Fetching the font information from the math font and the evaluation (in
% case they are defined in relative units) of the lengths mentioned above is
% done just before the individual rule is set. This is demonstrated by the
% following construction (which admittedly is not very useful):
%
% \smallskip
% {\hfill
%   \Large^^A
%    \inference[Large]{\normalsize^^A
%      \inference[normalsize]{\footnotesize^^A
%       \inference[footnotesize]{\tiny^^A
%         \inference[tiny]{}{Conclusion}}
%        {Conclusion}}
%      {Conclusion}}
%    {Conclusion}\hfill}
% \smallskip\linebreak
% Note that as going from the top to the bottom, the eaves are getting bigger
% and the names come farer from the line below.
% 
% \parmark
% \DescribeMacro{\predicate} 
% To set up a single predicate (a premise or conclusion) the singleargument
% command "\predicate" is used. This allows a finer control of the
% formatting. As an example alle premises and conclusions can be set in
% mathematics mode by the command:
% \begin{code}
%   "\renewcommand{\prediate}[1]{$ #1 $}"
% \end{code}
%
% \parmark
% \semantic\ only uses "\predicate" on a premise, when it does not
% contain a nested "\inference".\footnote{What \semantic\ precisely does is
%   to append the tokens \CSname{inference} \CSname{end} to the code of a
%   premise, when it has isolated it. \semantic\ then uses \TeX's pattern
%   matching to search this new list of tokens for an appearance of the token
%   \CSname{inference}. When this is found the following token is examened,
%   and if it is \CSname{end}, \semantic\ concludes that the premise does not
%   contain a nested inference rule} So though the declaration above has been
% given, "\inference" would \emph{never} be executed in math mode, nor if you
% wrote:
% \begin{code}
%   "\inference{\inference"\lttdots"}{"\lttdots"}"
% \end{code}
% 
% \parmark
% \DescribeMacro{\predicatebegin} 
% \DescribeMacro{\predicateend} 
% The default definition of "\predicate" is "\predicatebegin #1\predicateend",
% where "\predicatebegin" and "\predicateend" is defined to be empty. The
% setting of premises and conlusions in math could therefore also be
% obtained by
% \begin{code}
%   "\renewcommand{\predicatebegin}{$}" \\
%   "\renewcommand{\predicateend}{$}"
% \end{code}
%
% \parmark 
% My motivation however for introducing "\predicatebegin" and "\predicateend"
% was to use \TeX's patternmatching on macro arguments to do even more
% sophisticated formatting by redefining "\predicatebegin". \label{pattern matching}
% If for example \emph{every} \textsl{expression} is to be evaluated in a
% \textsl{environment} giving a \textsl{value}, and you would like to set
% \emph{all} the \textsl{environments} \textsl{values} in mathematics and the
% \textsl{expressions} in \texttt{typewriter}-font, then this could be eased
% by the definition:
% \begin{code}
%   "\def\predicatebegin#1|-#2=>#3#4\predicateend{%" \\
%   "  $#1 \vdash$\texttt{#2}$\stackrel{#3}{\Rightarrow}_S #4$}"
% \end{code}\hangindent=0pt
% Then the inference (borrowed from \textsc{M. Hennessy}, \emph{The 
% Semantics of Programming Languages})
% {\def\predicatebegin#1|-#2=>#3#4\predicateend{$#1 \vdash$\texttt{#2}$\stackrel{#3}{\Rightarrow}_S #4$}
% \[
%   \inference[TlR]{D |- $s$ =>{v} s' & D |- $s$ =>{v'} s''}
%     {D |- Tl($s$) =>{v'} s''}
% \]}^^A
% can be accomplished by
% \begin{code}
%   "\inference[TlR]{D |- $s$ =>{v} s' & D |- $s$ =>{v'} s''}" \\
%   "  {D |- Tl($s$) =>{v'} s''}"
% \end{code}
% Please note that the "inferencesymbols"-environment \emph{has not} been
% used above. 
% } ^^A TeXnichian mod OFF
%
% \section{Translation Diagrams}
%
% \DescribeMacro\compiler
% \DescribeMacro\interpreter
% \DescribeMacro\program
% \DescribeMacro\machine
% To draw translation diagrams describing the result of using one or more
% compilers, interpreters etc., \semantic\ has commands for the diagrams:
% \begin{center}
%   \begin{picture}(280,40)
%     \put(10,0) {\program{P,L}}
%     \put(70,0){\interpreter{S,L}}
%     \put(160,0){\compiler{S,M,T}}
%     \put(250,11.45){\machine{M}}
%   \end{picture}
% \end{center}
% The commands should only be used in a "picture"-environemnt and are
% respectively
% \begin{code}
%   "\program{"\meta{program}","\meta{implementation language}"}" \\
%   "\interpreter{"\meta{source}","\meta{implemenation language}"}" \\
%   "\compiler{"\meta{source}","\meta{machine}","\meta{target}"}" \\
%   "\machine{"\meta{machine}"}"
% \end{code}
% The arguments can be a either a string describing the language (please do
% not use a macro at the start of the string) or one of the four commands.
% However the combinations giving no meaning are excluded---like implementing
% a interpreter on a program, which yield the errormessage:
% \begin{code}
% \begin{verbatim}
% ! Package semantic Error: A program cannot be at the bottom .
% 
% See the semantic package documentation for explanation.
% Type  H <return>  for immediate help.
%  ...                                      
% \end{verbatim}
% \end{code}
% 
% When you are using a command as an argument \semantic\ will copy the
% language from the nested command and automaticly place the two figures in
% proportion to each other. In this way big translation diagrams can easily be
% drawn. The hole construction should be placed using af "\put" command,
% where the \emph{reference point} is the center of the bottom of the figure
% corresponding to the outermost command. I think a few examples (with the
% reference point marked by
% \raisebox{.5ex}[0pt][0pt]{\begin{picture}(6,0)(-3,0)\put(0,0){\circle*{3}}\end{picture}})
% will clarify some of these point:
% \begin{center}
%   \begin{picture}(220,75)(0,-35)
%      \put(10,0){\interpreter{S,L'}}
%      \put(10,0){\circle*{3}}
%      \put(110,0){\program{P,\compiler{C,\machine{M},\program{P,M}}}}
%      \put(110,0){\circle*{3}}
%   \end{picture}
% \end{center}
% is obtained by the commands
% \begin{code}
%   "\begin{picture}(220,75)(0,-35)" \\
%   " \put(10,0){\interpreter{S,L'}}" \\
%   " \put(110,0){\program{P,\compiler{C,\machine{M},\program{P,M}}}}" \\
%   "\end{picture}"
% \end{code}
% Note from the second example, that when "\compiler" is used as
% ``implementation language''-argument it is by convention attributed to the
% right of the figure. It is also worth mentioning that there is no strict
% demand on which command you should choose as the outermost, ie.\ the 
% second example could also be written (with a change in the coordinates to 
% "\put" due to the new reference point) as
% \begin{code}
%   "\put(160,-20){\compiler{\program{P,C},\machine{M},\program{P,M}}}"
% \end{code}
% starting off in the middle instead of using a
% ``left-to-right''-approach---in fact it will often be easiest to start in
% the middle as this gives the least nesting making it easier to end the
% arguments at the right position.
% 
% Though using nesting it is in some rare cases adequate to use different
% language symbols on the two sides of the line of touch.
% E.g.\ when describing bootstrappring the poor U-code
% implementation can be symbolized by \texttt{U$^-$}, which still is executed
% on a \texttt{U}-machine. This can be done by providing the symbol-command
% with an optional argument immediately after the commandname. In this way
% the bootstrapping:
% \begin{center}
%   \begin{picture}(230,80)(-90,-20)
%     \put(0,0){\compiler{\compiler{ML,ML,U},\machine[U$^-$]{U},\compiler{\compiler{ML,ML,U},\machine[U$^-$]{U},\compiler{ML,U,U}}}}
%   \end{picture}
% \end{center}
% is typed 
% \begin{code}
%  "\compiler{\compiler{ML,ML,U},\machine[U$^-$]{U},\compiler{"\\
%  "     \compiler{ML,ML,U},\machine[U$^-$]{U},\compiler{ML,U,U}}}"
% \end{code}
%
% When calculating the dimensions of the "picture"-environment it is
% good to know the dimensions of the figures, which is given in units of
% "\unitlength":
%
% \ifmulticols
%   \begin{multicols}{2}
% \fi \noindent
%   compiler: 80*40 \\
%   interpreter: 20*40 \\
%   machine: 20*17.1 \\
%   program: 20*40
% \ifmulticols
%   \end{multicols}
% \fi
%
% \section{Some Notes about the Files}
% 
% \semantic\ is distributed in the two files "semantic.dtx" and
% "semantic.ins".  "semantic.dtx" is the most important as it contains all
% the essentials---users guide, code and documentation of the code---while
% "semantic.ins" is used only to guide \package{docstrip} in generating
% "semantic.sty" from "semantic.dtx".
% 
% {\makeatletter To get \@bblb\ and \@bbrb\ used in "\comp", "\eval" and "\exe"
%   \semantic\ tries to load the package \package{bbold} written by 
%   \textsc{A. Jeffrey}. If this is not installed on your system, the symbols
%   are simulated by drawing together to sharps. I will however recommend 
%   that you get \package{bbold} from your nearest CTAN-archive. 
% \makeatother}
% 
% In addition to the users guide you kan also get the fully documented code.
% You will however only need this if you will sneak in how I implemented the
% macros or change some part of the package. You should start by editing
% "semantic.dtx" and make the two lines (near line 1545)
% \begin{code}
%   "\OnlyDescription    % Make to a comment to get the documentation"\\
%   "\DisableCrossrefs   % Remove comment if the index is ready or if"\\
% \end{code}
% in to a comment and remove "%" from the begining of the two next lines:
% \begin{code}
%   "%\CodelineIndex      % Make a index of the command usage"\\
%   "%\RecordChanges      % Make the changes history"
% \end{code}
% Then you should run \LaTeX\ twice on the edited file to get a correct table
% of contents. Then you generate the index and change history using
% "makeindex":
% \begin{code}
%   "makeindex -s gind.ist semantic" \\
%   "makeindex -s gglo.ist -o semantic.gls semantic.glo"
% \end{code}
% And at last the documentation is ready for printing after another run of
% \LaTeX.
% 
% "semantic.dtx" is designed to be used with \package{doc} and
% \package{docstrip}. It therefore consists of the packagecode but most of all
% of a lot of comments contaning the users guide and the documentation of the
% code. When \TeX\ is runned on "semantic.ins", \package{doc} is used to
% remove all these comments and the result is written in the package-file
% "semantic.sty". When you make the users guide by running \LaTeX\ on
% "semantic.dtx", \LaTeX\ first skips about 650 lines of comments (containing
% the source of the users guide) before it gets to the lines normally making
% up the package-file. Then follows 850 lines of intermixed comments and code
% defining the commands in the package. At last \LaTeX\ comes to a line
% "\documentclass{ltxdoc}" (\package{ltxdoc} is \LaTeXe's standard class for
% documenting). After a couple of packagesloading and some command definition
% it reaches "\begin{document}" and "\docinput{semantic.dtx}". This makes
% \LaTeX's reading over "semantic.dtx" once more but this time skipping the
% \%-chars in the first column.
% 
% \medskip
% \parmark[\copyright]^^A
% At last the borrowing formal stuff: You a encouraged to copy, use, delete
% etc.\ the package ("semantic.dtx" and "semantic.ins") as much as your heart
% desires as long as you pass it on in complete (ie.\ not only "semantic.sty").
% You are welcome to sneak in the code and get inspiration (A little warning
% however: this is my first bunch of real \TeX-code!).  You should just
% remember: {\small \copyright 1995--1996 Peter M{\o}ller Neergaard}
% 
% \StopEventually{
%  \ifmulticols
%    \addtocontents{toc}{\protect\end{multicols}}
%  \fi
% }
%
% \section{Documentation of the Package Code}
%
% \ifmulticols
%   \begin{multicols}{2}[\subsection{To Be Done (in Priority)}]
% \else
%   \subsection{To Be Done (in Priority)}
% \fi
% \changes{1.0}{1995/10/18}{Introduced a list of things to be done}
% \begin{columnItemize}
% \item If at all possible add a check for the existence of "manfnt.tfm".
% \item Use \LaTeX's "\mbox", "\parbox" etc.\ instead of \TeX's "\hbox",
%   "\vbox" (cf.\ \cite{packagesguide}). This requires that I find out what
%   the \LaTeX-``translation'' of "\unhbox" is.
% \item Use "\hrule" and "\vrule" instead of "\line" (cf.\ \package{Epic}) as
%   much as possible to build the translationdiagrams as this will improve
%   performance.
% \item Develop example-macro thats sets an example and gives the source text
%   for the example.
% \item Run over my command defininitions and use "\newcommand" instead of
%   "\newcommand"\lttdots"\def", whenever the first is sufficient, ie.\ 
%   whenever I do not use, that \TeX's gives a better pattern matching on
%   arguments than \LaTeX.
% \item Analyze my use of registers to see if I can reduce the
%   number of permantly reserved registers.
% \item Study the way \package{Babel} defines its additional ligatures and if
%   appropriate change my definition in "inferencesymbols".
% \end{columnItemize}
% 
% \ifmulticols
%   \end{multicols}
% \fi
%
% \subsection{Stub for Users Guide and Documentation}
%
% First comes a little hack, that makes \LaTeX\ thinks it is loading the
% package \texttt{semantic.sty}.  In this way the commands in the package can
% be used when printing the documentation.
%    \begin{macrocode}
%<*documentation>
\makeatletter 
\def\@currname{semantic}
\def\@currext{sty} 
%</documentation>
%    \end{macrocode}
% "\@currname" and "\@currext" is internal \LaTeX-macros containg the name
% and extension of the package currently being loaded.  The code is
% encapsulated in "<*documentation>"\lttdots"</documentation>" so that it is
% not included in the style-file, when installing the package.
%
% \subsection{Package Identification}
% The package-code starts by identifying the file as a \LaTeXe-package.
%    \begin{macrocode}
\NeedsTeXFormat{LaTeX2e} 
\ProvidesPackage{semantic}
  [1996/01/31 v1.2(alpha) Symbols for semantics]
%    \end{macrocode}
%
% \subsection{Auxiliary Macros}
%
% \begin{macro}{\@bblb}
% \begin{macro}{\@bbrb}
% \changes{1.0}{1995/10/20}{I have defined ``fake''-black\-board\-bold considering people without \package{bbold}}
% \changes{1.2$\alpha$}{1996/01/31}{Changed the names}
% \changes{1.2$\alpha$}{1996/01/31}{Added fixed use of document main font}
% \makeatletter
% If \package{bbold} is installed I use it to make \@bblb\ og \@bbrb,
% otherwise two brackets are drawn together. To make this transparent to the
% rest of the package I define two commands "\@bblb" (\textbf{b}lackboard
% \textbf{b}old \textbf{l}eft \textbf{b}racket) and "\bbrb"
% (\textbf{b}lackboard \textbf{b}old \textbf{r}ight \textbf{b}racket), which
% in both cases gives \@bblb\ respectively \@bbrb.
%    \begin{macrocode}
\IfFileExists{bbold.sty}{%
  \RequirePackage{bbold} 
  \newcommand{\@bblb}{\textbb{[}}
  \newcommand{\@bbrb}{\textbb{]}}} 
{ \newcommand{\@bblb}{\textnormal{[\kern-.15em[}}
  \newcommand{\@bbrb}{\textnormal{]\kern-.15em]}}}
%    \end{macrocode}
% \makeatother
% \end{macro}
% \end{macro}
%%
% \begin{macro}{\@ifnext}
%   Compares the next token with a given token (\#1) and if they are identical
%   the first choice (\#2) is expanded and otherwise the second choice(\#3).
%   This is loan of "\@ifnextchar" from the \LaTeXe-base and it is therefore
%   using the interal variables "\reserved@a"\lttdots"\reserved@d". The only
%   change is that spaces are not ignored, which is appropriate when defining
%   the ligatures (eg.\ I do not want \verb*"- >" to be converted to 
%   $\rightarrow$).
%    \begin{macrocode}
\newcommand{\@ifnext}[3]{}
\def\@ifnext#1#2#3{%
  \let\reserved@e=#1\def\reserved@a{#2}\def\reserved@b{#3}\futurelet%
  \reserved@c\@ifn} 
\newcommand{\@ifn}{}
\def\@ifn{%
      \ifx \reserved@c \reserved@e\let\reserved@d\reserved@a\else%
          \let\reserved@d\reserved@b\fi \reserved@d}
%    \end{macrocode}
%   Here as in the following I first define empty expansions with \LaTeX's
%   "\newcommand" before I give the real definition with \TeX's "\def", when I
%   need to use \TeX's pattern mathcing on arguments. In this way name conflict
%   with other packages should produce warnings if they also behaves rightly
%   (but they dont !).
% \end{macro}
%
% \begin{macro}{\@ifNextMacro}
%   This macro examens the next token and if it a macro, the first
%   option (\#1) is exectued and if not the other option (\#2). Like
%   "\@ifnext" the code is mainly ``borrowed'' from the \LaTeX-source.
%    \begin{macrocode}
\newcommand{\@ifNextMacro}[2]{}
\def\@ifNextMacro#1#2{%
  \def\reserved@a{#1}\def\reserved@b{#2}%
    \futurelet\reserved@c\@ifnMacro} 
\newcommand{\@ifnMacro}{}
\def\@ifnMacro{%
  \ifcat\noexpand\reserved@c\noexpand\@ifnMacro 
    \let\reserved@d\reserved@a
  \else \let\reserved@d\reserved@b\fi \reserved@d}
%    \end{macrocode}
%   The test wether it is a macro is done in "\@ifnMacro" by comparing the 
%   catcodes of the token and a macro, "\@ifnMacro" (any other
%   macro could have been used as well). The "\noexpand" secures that I compare 
%   the token and not its expansion, eg.\ if "\@noexpand" were left out and 
%   the token was a macro, then it would be expanded and the first token in 
%   the macro be compared to the first token i "\@ifnMacro".
% \end{macro}
%
% \begin{macro}{\@dropnext}
%   Takes the two following token and processes the first and ignores the
%   second (so it is not processed at all). Is implemented by simple pattern
%   mathcing where the second token is read but not used.
%    \begin{macrocode}
\newcommand{\@dropnext}[2]{#1}
%    \end{macrocode}
%  \end{macro}
%
% \subsection{Different Semantic notation}
% 
% Then comes all the commands for symbols eaysing the notation of semantics.
% They are all fairly simple taking some arguments and set them in an 
% approriate font intermixed with some filling symbols.
% 
% \subsubsection{Denotational Semantics}
% I have given a lot of thoughts to decide on a good syntax.
% The most essential requirements was that syntax was consistent and
% simple/intuitive close to that used in \emph{Introduction to the Semantics
%   of Programming Languages}. In the eyes of a semanticer the most evident
% would probaply be to write "\eval["\lttdots"]x" to get \eval{\lttdots}{x}
% and indeed "\eval**["\lttdots"]x" rather than "\eval[**]{"\lttdots"}{x}".
% This is however a departure from the standard syntax of \LaTeX. And even
% more decissive, is that there cannot be made a analogoues syntax for
% "\evalsymbol" as it is undecidable whether it is followed by a
% symbol---does "\evalsymbol test" mean ``\evalsymbol[t]est'' or
% ``\evalsymbol test''? This makes it necessary to use brackets in connection
% with "\evalsymbol" and to have consistent syntax I have made the same
% decission for "\eval".
%\begin{macro}{\evalsymbol}
%\begin{macro}{\compsymbol}\mbox{}
% \changes{1.0}{1995/10/18}{Settled on a syntax and described my considerations} 
% \changes{1.0}{1995/10/18}{Made som ``cleanup'' with offspring in the decided syntax}
%    \begin{macrocode}
\newcommand{\evalsymbol}[1][]{\ensuremath{\mathcal{E}^{#1}}}
\newcommand{\compsymbol}[1][]{\ensuremath{\mathcal{C}^{#1}}}
%    \end{macrocode}
%   The definition gives a command taking a optional argument. If this argument
%   is \emph{not} present the default value given in the second pair of
%   brackets is used ie.\ nothing.
% \end{macro}
% \end{macro}
%
%\begin{macro}{\eval}
%\begin{macro}{\comp}\mbox{}
% \changes{1.0}{1995/10/18}{Erased several previous commands as they were only a special cases of the other commands with the decided syntax. Besides that the names have been translated from danish to english}
% \changes{1.2$\alpha$}{1996/01/30}{Made a brand new definition to avoid an error when using \CSname{comp} and \CSname{eval} displaymath}
%    \begin{macrocode} 
\newcommand{\eval}[3][]%
  {\mbox{$\mathcal{E}^{#1}$\@bblb \texttt{#2}\@bbrb}\ensuremath{\mathtt{#3}}}
\newcommand{\comp}[3][]%
  {\mbox{$\mathcal{C}^{#1}$\@bblb \texttt{#2}\@bbrb}\ensuremath{\mathtt{#3}}}
%    \end{macrocode}
%  This definition should allow a linebreak after the last bracket
% \end{macro}
% \end{macro}
%
% \begin{macro}{\exe} \mbox{}
% \changes{1.0}{1995/10/18}{Translated the name to english}
%    \begin{macrocode}
\newcommand{\@exe}[3]{}
\newcommand{\exe}[1]{\@ifnextchar[{\@exe{#1}}{\@exe{#1}[]}}
\def\@exe#1[#2]#3{%
  \mbox{\@bblb\texttt{#1}\@bbrb$^\mathtt{#2}\mathtt{(#3)}$}}
%    \end{macrocode}
%   The command "\exe" is a stub that checks if the second argument is lead off
%   with an optional sharp by looking at the token following the first
%   argument. If there is not provided a bracket an empty second argument is
%   added before the control is given to "\@exe", which does the setting.
%   There is no place to do an expedient linebreak so everything is
%   encapsulated in a "\mbox".
% \end{macro}
%
% \subsubsection{Inference Symbols}
%
% \DeleteShortVerb\|  ^^A "|" is used in inferencesymbols and cannot therefroe
%                     ^^A be used as a verbatim character
% \begin{macro}{inferencesymbols}
% \changes{1.1}{1995/11/25}{Changed from a command to an environment}
%   \changes{1.1$\delta$}{1995/12/01}{Added $\protect\models$ ("|=") as a ligature} 
%   The invorking of the environment is parted in two: an initialising part and
%   a declaring macro, "\@doinferencesymbolsDef". The initialising save the
%   current ``values'' of "|", "=" and "-" and changes their catcodes
%   to \emph{active} so there can be used as commands. As ``--'' and ``---''
%   will have to be redefined they are also saved---in macros, however, as
%   "\let" can handle only one token. The macro defining the expansion of the
%   characters inside the environment had to be split out as it should be
%   parsed with the changed catcode-values---otherwise the characters
%   would not be recognised as commands as \TeX\ matches both character
%   values and catcodes when looking for an expansion. The definition of
%   this macro is therefore enclosed in a group, where the catcodes are
%   changed and is defined with "\gdef" to be known outside the group.
%    \begin{macrocode}
\newenvironment{inferencesymbols}{%
 \let\@@streg=|%  
 \let\@@lig==%    
 \let\@@minus=-%
 \def\@@enstreg{--}%
 \def\@@emstreg{---}%
 \catcode`\|=\active %
 \catcode`==\active  %
 \catcode`-\active%
 \@doinferencesymbolsDef}{}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\@doinferencesymbolsDef}
% \changes{1.0}{1995/10/19}{Added \texttt{{-}-} and \texttt{-{-}-} as ligatures as they are not defined on active tokens}
% \begin{inferencesymbols}
%   In this macro the relevant ligatures is defined: "|-" (|-), "|=" (|=),
%   (|-), "->" (->), "->*" (->*), "->+" (->+), "=>" (=>), "=>*" (=>*) og "=>+"
%   (=>+).  "--" (--) and "---" (---) is also redefined as they are not
%   naturally ligatures on active characters. All the macros a made using the
%   same scheme: The next token is examened and if it has the ``right'' value
%   it is ignored and the two tokens are replaced with the ``ligature''. If it
%   is not a ligature, ie.\ the 2nd token is ``wrong'', then the original
%   definition of the token saved above is inserted. This scheme will work in
%   most cases only failing, when the tokens ``activated'' is used as a
%   pattern to a macro definition (like in
%   "\cline{"\lttdots\textbf{\texttt{-}}\lttdots"}"). When dealing with the
%   three tokens ligature the processing of "*" and "+" is done in
%   "\@starOrPlus", when the arrow is recognised.
% \end{inferencesymbols}
%    \begin{macrocode}
\newcommand{\@doinferencesymbolsDef}{}
{\catcode`\|=\active %
 \catcode`==\active  %
 \catcode`-\active%   
 \gdef\@doinferencesymbolsDef{%
   \def|{\@ifnext -{\@dropnext{\ensuremath{\vdash}}}%
        {\@ifnext ={\@dropnext{\ensuremath{\models}}}{\@@streg}}}%
   \def={\@ifnext >{\@dropnext{\@starOrPlus{\Rightarrow}}}{\@@lig}}%
   \def-{\@ifnext >{\@dropnext{\@starOrPlus{\rightarrow}}}%
        {\@ifnext -{\@dropnext{\@ifnext -{\@dropnext{\@@emstreg}}%
                                                    {\@@enstreg}}}%
                                                    {\@@minus}}}}}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\@starOrPlus}
% \changes{1.0}{1995/18/10}{Introduced the optional $^+$- or $^*$-version}
%   The definition of "\@starOrPlus" is much like the commands above---the next
%   token is examined to decide wether to append a $*$ or $+$ on the arrow.
%    \begin{macrocode}
\newcommand{\@starOrPlus}[1]{%
  \@ifnext *{\@dropnext{\ensuremath{#1^*}}}{%
  \@ifnext +{\@dropnext{\ensuremath{#1^+}}}{\ensuremath{#1}}}}
%    \end{macrocode}
% \end{macro}
% \MakeShortVerb\|
%
% \subsection{Translation Diagrams}
% First som auxilary registers are reserved:
%    \begin{macrocode}
\newif\if@@Nested \@@Nestedfalse 
\newif\if@@Left 
\newif\if@@Up
\newcount\@@xShift 
\newcount\@@yShift 
\newtoks\@@symbol
\newtoks\@@tempSymbol
%    \end{macrocode}
% \begin{tabular}{lp{9.2cm}}
%   "\@@Nested" & Flag telling if the current diagram is nested within another \\
%   "\@@Left"   & Flag telling that a nested diagram should be drawn to the
%                 left --- if not set a nested diagram will be drawn right \\
%   "\@@Right"  & Flag telling that a nested diagram should be drawn above 
%                 the current---if not set it will be drawn below \\
%   "\@@xShift" & Horinzontal shift from the locally origin to the starting
%                  position in units of "\unitlength" \\
%   "\@@yShift" & The corresponding shift in the vertical direction \\
%   "\@@Symbol" & The current machine symbol (i.e.\ the letter designating the programme/machine) \\
%   "\@@tempSymbol" & Used as temporary storage for different symbols 
% \end{tabular}
% 
% When \LaTeX's "\put"-command is invoked it raises a "\hbox" to
% the given offset, giving it height zero and puts a "\hss" in the end,
% so it will end up with zero width too. It expands the "picture"-command
% given in "{"\lttdots"}" just before the "\hss", so they can be drawn
% from a locally origin (the one given as coordinates to "\put"). The
% diagram-commands is adapted to this scheme, so they are all constructed
% after the same scheme:
% \begin{itemize}
% \item The offset (x in "count1" and y in "count2") from the local
%   origin to the starting position is calculated: If the diagram is
%   not \emph{nested} the bottom should be centered around the position
%   given by "\put". If the diagram  is nested, the bottom should
%   be, at the current vertical position, if the diagram should be drawn
%   \emph{upwards}. Conversely the top should be at the current vertical
%   position, if the diagram is to be drawn \emph{downwards}. If the
%   diagram should go to the \emph{left}, the right side should be at
%   the current horizontal position and conversely.
% \item A "\hbox" is shifted to the given offset using "\hskip" and
%   "\raise". Inside the box is first drawn the frame of the diagram.
%   This is done using the "\put", "\line" and other
%   "picture"-commands. This relies on the way the
%   "picture"-commands are construtced. It is admittely a little
%   wrong using the commands in non-documented ways, but it takes up a
%   little less memory and I would like later to implement most of the
%   commands using rules, which would be faster.
% 
% \item The parameters are parsed. This is done in a specialized macro,
%   which is given the position and orientation (i.e.\ up and left) of a
%   possible nested diagram and the coordinates for the symbol in the
%   current diagram.  The macro will examen the argument, and if it
%   consist of letters, this will be considered the language symbol and be
%   set in the appropriate place. If it however is a macro, the nested diagram
%   will be drawn, returning the language symbol using the global register
%   "\@@symbol", which afterwards is set inside the diagram.
% 
% \item If the diagram is nested, it at last ensures, that "\@@symbol"
%   is set globally accordingly to the orientation. This way it returns
%   the symbol to the ``calling'' diagram.
% \end{itemize}
% 
% Most of the translation diagrams is coded with a little stump, that
% packs the arguments (that is separated with commaes) with an "\end"
% after, so that \TeX's pattern matching can separate them.
% 
% \begin{macro}{\compiler}
% \begin{macro}{\@compiler}\mbox{}
% \changes{1.2$\alpha$}{1996/27/01}{Rewritten to fit with a "picture"-environment and nesting of diagrams}
%    \begin{macrocode}
\newcommand{\compiler}[1]{\@compiler#1\end}
\def\@compiler#1,#2,#3\end{%
  \if@@Nested %
    \if@@Up %
    \@@yShift=40 \if@@Left \@@xShift=-50 \else \@@xShift=-30 \fi
    \else%
      \@@yShift=20 \@@xShift =0 %
    \fi%
  \else%
    \@@yShift=40 \@@xShift=-40%
    \fi
  \hskip\@@xShift\unitlength\raise \@@yShift\unitlength\hbox{%
    \put(0,0){\line(1,0){80}}%
    \put(0,-20){\line(1,0){30}}%
    \put(50,-20){\line(1,0){30}}%
    \put(30,-40){\line(1,0){20}}%
    \put(0,0){\line(0,-1){20}}%
    \put(80,0){\line(0,-1){20}}%
    \put(30,-20){\line(0,-1){20}}%
    \put(50,-20){\line(0,-1){20}}%
    \put(30,-20){\makebox(20,20){$\rightarrow$}} %
   {\@@Uptrue \@@Lefttrue \@parseArg(0,-20)(5,-20)#1\end}%
   \if@@Up \else \@@tempSymbol=\expandafter{\the\@@symbol}\fi
   {\@@Uptrue \@@Leftfalse \@parseArg(80,-20)(55,-20)#3\end}%
   {\@@Upfalse \@@Lefttrue \@parseArg(50,-40)(30,-40)#2\end}%
   \if@@Up \@@tempSymbol=\expandafter{\the\@@symbol}\fi
    \if@@Nested \global\@@symbol=\expandafter{\the\@@tempSymbol} \fi%
  }%
}
%    \end{macrocode}
% \end{macro} 
% \end{macro} 
%
% \begin{macro}{\interpreter}
% \begin{macro}{\@interpreter}\mbox{}
% \changes{1.0}{1995/18/10}{Translated command names from danish to english}
% \changes{1.2$\alpha$}{1996/27/01}{Rewritten to fit with a "picture"-environment and nesting of diagrams}
%    \begin{macrocode}
\newcommand{\interpreter}[1]{\@interpreter#1\end}
\def\@interpreter#1,#2\end{%
  \if@@Nested %
    \if@@Up %
    \@@yShift=40 \if@@Left \@@xShift=0 \else \@@xShift=20 \fi
    \else%
      \@@yShift=0 \@@xShift =0 %
    \fi%
  \else%
    \@@yShift=40 \@@xShift=10%
    \fi
  \hskip\@@xShift\unitlength\raise \@@yShift\unitlength\hbox{%
    \put(0,0){\line(-1,0){20}}%
    \put(0,-40){\line(-1,0){20}}%
    \put(0,0){\line(0,-1){40}}%
    \put(-20,0){\line(0,-1){40}}%
   {\@@Uptrue \@@Lefttrue \@parseArg(0,0)(-20,-20)#1\end}%
   \if@@Up \else \@@tempSymbol=\expandafter{\the\@@symbol}\fi
   {\@@Upfalse \@@Lefttrue \@parseArg(0,-40)(-20,-40)#2\end}%
   \if@@Up \@@tempSymbol=\expandafter{\the\@@symbol}\fi
    \if@@Nested \global\@@symbol=\expandafter{\the\@@tempSymbol} \fi%
  }%
}
%    \end{macrocode}
% \end{macro} 
% \end{macro} 
% 
% \begin{macro}{\program}
% \begin{macro}{\@program}\mbox{}
% \changes{1.2$\alpha$}{1996/27/01}{Command added}
%    \begin{macrocode}
\newcommand{\program}[1]{\@program#1\end}
\def\@program#1,#2\end{%
  \if@@Nested %
    \if@@Up %
    \@@yShift=0 \if@@Left \@@xShift=0 \else \@@xShift=20 \fi
    \else%
      \PackageError{semantic}{%
        A program cannot be at the bottom}
        {%
          You have tried to use a \protect\program\space as the
          bottom\MessageBreak parameter to \protect\compiler,
          \protect\interpreter\space or \protect\program.\MessageBreak
         Type <return> to proceed --- Output can be distorted.}%
    \fi%
  \else%
    \@@yShift=0 \@@xShift=10%
    \fi
  \hskip\@@xShift\unitlength\raise \@@yShift\unitlength\hbox{%
    \put(0,0){\line(-1,0){20}}%
    \put(0,0){\line(0,1){30}}%
    \put(-20,0){\line(0,1){30}}%
    \put(-10,30){\oval(20,20)[t]}%
    \@putSymbol[#1]{-20,20}%
   {\@@Upfalse \@@Lefttrue \@parseArg(0,0)(-20,0)#2\end}%
  }%
}
%    \end{macrocode}
% Note that there is incorporated a little code to report errors, if the
% command is used wrongly.
% \end{macro} 
% \end{macro} 
% 
% \begin{macro}{\machine}\mbox{}
% \changes{1.2$\alpha$}{1996/27/01}{Command added}
%    \begin{macrocode}
\newcommand{\machine}[1]{%
  \if@@Nested %
    \if@@Up %
      \PackageError{semantic}{%
        A machine cannot be at the top}
        {%
          You have tried to use a \protect\machine\space as a
          top\MessageBreak parameter to \protect\compiler or
          \protect\interpreter.\MessageBreak
         Type <return> to proceed --- Output can be distorted.}%
       \else \@@yShift=0 \@@xShift=0
    \fi%
  \else%
    \@@yShift=20 \@@xShift=10%
    \fi
  \hskip\@@xShift\unitlength\raise \@@yShift\unitlength\hbox{%
    \put(0,0){\line(-1,0){20}} \put(-20,0){\line(3,-5){10}}
    \put(0,0){\line(-3,-5){10}}%
   {\@@Uptrue \@@Lefttrue \@parseArg(0,0)(-20,-15)#1\end}%
  }%
}
%    \end{macrocode}
% Note that there is incorporated a little code to report errors, if the
% command is used wrongly.
% \end{macro} 
%
%
% \begin{macro}{\@parseArg}
% \begin{macro}{\@getSymbol}
% \begin{macro}{\@doSymbolMacro}
% \begin{macro}{\@saveBeforeSymbolMacro}
%   These macros parse a single argument. As there is some testign of
%   the following token, it is splitted in four macros, the main being
%   "\@parseArg". It is given the offset to a possibly nested diagram and the
%   position of the symbol within the current diagram. All it does is
%   testing wether the argument is a command ("\@doSymbolMacro") or some
%   text string ("@\getSymbol"), and then passes the parameters on to the
%   approriate macro.
%    \begin{macrocode}
\def\@parseArg(#1)(#2){%
  \@ifNextMacro{\@doSymbolMacro(#1)(#2)}{\@getSymbol(#2)}}
%    \end{macrocode}
%   "\@getSymbol" is used when the argument is ``plain'' text. It simply
%   passes the parameters to "\@putSymbol", which does the setting up.
%    \begin{macrocode}
\def\@getSymbol(#1)#2\end{\@putSymbol[#2]{#1}}
%    \end{macrocode}
%   "\@doSymbolMacro" is used, when the argument has been identified as a
%   macro. It tests if there is an optional argument, which is then saved
%   in "\@@symbol" using "\@saveBeforeSymbolMacro" and "\@@tempSymbol".
%   Then the macro is exandened.
%    \begin{macrocode}
\def\@doSymbolMacro(#1)(#2)#3{%
  \@ifnextchar[{\@saveBeforeSymbolMacro(#1)(#2)#3}%
               {\@symbolMacro(#1)(#2)#3}}
%    \end{macrocode}
%    \begin{macrocode}
\def\@saveBeforeSymbolMacro(#1)(#2)#3[#4]#5\end{%
  \@@tempSymbol={#4}%
  \@@Nestedtrue\put(#1){#3#5}%
  \@putSymbol[\the\@@tempSymbol]{#2}}
%    \end{macrocode}
%    \begin{macrocode}
\def\@symbolMacro(#1)(#2)#3\end{%
  \@@Nestedtrue\put(#1){#3}%
  \@putSymbol{#2}}
%    \end{macrocode}
% \end{macro}
% \end{macro}
% \end{macro}
% \end{macro}
%
% \begin{macro}{\@putSymbol}
%   A auxiliary macro that as default set the text of register
%   "\@@symbol" on the given position. If however a parameter is given,
%   "\@@symbol" is set to this parameter before "\@@symbol" is set. The
%   macro is used by all the diagrams to set the symbols, when the has
%   been determined.
%    \begin{macrocode}
\newcommand{\@putSymbol}[2][\the\@@symbol]{%
  \global\@@symbol=\expandafter{#1}%
  \put(#2){\makebox(20,20){\texttt{\the\@@symbol}}}}
%    \end{macrocode}
% \end{macro}
% 
% \subsection{Inference Rules}
%
% \begin{macro}{\@makeLength}
%   \changes{1.1}{1995/11/12}{Redefined the lengths commands, so that the lengths are evaluated each time}^^A
% \begin{macro}{\@setLengths}
% \changes{1.1$\beta$}{1995/11/21}{Added setting of parameters for line skipping in \CSname{@setLengths}}
%   First I define two auxiliary macros to ease the use of the lengths
%   controlling the appearance of an inference rule.  My overall aim is to
%   allow the use of relative units ("em" and "ex"). To accomplish this the
%   lengths would have to be evaluated before the setting of every rule. As
%   their is only a few lengths could been have been simpler and less
%   general, but I found it inspiring working out a general solution.
%
%   "\@makelength{"\meta{users name}"}{"\meta{internal name}"}{"\meta{default
%       value}"}{"\meta{stretch}"}" does all the definitions associated with
%   making a new length: defines a new length "\@@"\meta{internal name}, makes
%   a command to evaluate it (with the current choice of font)
%   "\@set"\meta{internal name} and makes the users command to change the
%   length "\set"\meta{users name}.  \meta{default value} is---of course---the
%   normal value used for the length while \meta{stretch} is the stretch
%   parameter in case the premise shall be set wider than its natural width.
%
%   The macro "\@setLengths" is used to evaluate all the lengths. When a new
%   length is made using "\@makelength" the name of its evaluation macro,
%   "\@set"\meta{internal name}, is added. 
%    \begin{macrocode}
\newtoks\@@tempa 
\newtoks\@@tempb 
\newcommand{\@makeLength}[4]{
  \@@tempa=\expandafter{\csname @@#2\endcsname}
  \@@tempb=\expandafter{\csname @set#2\endcsname} %
  \expandafter \newlength \the\@@tempa 
  \expandafter \newcommand \the\@@tempb {} 
  \expandafter \newcommand \csname set#1\endcsname[1]{}
  \expandafter \xdef \csname set#1\endcsname##1%
    {{\dimen0=##1}%
      \noexpand\renewcommand{\the\@@tempb}{%
        \noexpand\setlength{\the \@@tempa}{##1 #4}}%
    }%
  \csname set#1\endcsname{#3}
  \@@tempa=\expandafter{\@setLengths} %
  \edef\@setLengths{\the\@@tempa \the\@@tempb} %
  }

\newcommand{\@setLengths}{%
  \setlength{\baselineskip}{1.166em}%
  \setlength{\lineskip}{1pt}%
  \setlength{\lineskiplimit}{1pt}}
%    \end{macrocode}
%   The first lines in "\@makelength" builds the name of the length in
%   "\@@tempa" and the macro to evaluate it in "\@@tempb"---this requires some
%   playing with "\csname"---and declares the corresponding length and command.
%   Then the users command is builded: It contains a test "{\dimen0 = #1}" to
%   ensure that the given parameter in fact is a length and then it redefines
%   the evaluating command, so that the length is the length provided by the
%   user and a possibly stretch, which is defined below and cannot be altered
%   by the user. At last the evaluating command is added to
%   "\@setLengths"---the inspiration to this code I got from
%   \cite[378]{texbook}.
%
%   The distance between the lines of premises is set by \TeX\ using its normal
%   lineskipping algorithm. As some environments, e.g.\ "tabular", sets all the
%   lineskipping  parameters, "\baselineskip", "\lineskip" and 
%   "\lineskiplimit", to zero it is necessary to set them in "\@setLengths".
% \end{macro}
% \end{macro}
%
% \begin{macro}{\setpremisesspace}
%   \changes{1.0}{1995/10/18}{Changed from 10"pt" to 15"pt"}^^A
%   \changes{1.2$\alpha$}{1996/01/31}{Changed to 1.5"em"}
% \begin{macro}{\setpremisesend}
%   \changes{1.2$\alpha$}{1996/01/31}{Changed to .75"em"}
% \begin{macro}{\setnamespace}
%   \changes{1.01}{1995/11/07}{Introduced \CSname{name\-space}}^^A
%   Then comes the real definition of the users command to set the length: 
%   \label{space setting}
%    \begin{macrocode}
\@makeLength{premisesspace}{pSpace}{1.5em}{plus 1fil}
\@makeLength{premisesend}{pEnd}{.75em}{plus 0.5fil}
\@makeLength{namespace}{nSpace}{.5em}{}
%    \end{macrocode}
% \end{macro}
% \end{macro}
% \end{macro}
%
% Then comes some auxiliary internal registers
% \changes{1.1$\delta$}{1995/12/01}{Introduced \CSname{@@space} to use in comparisions}
%    \begin{macrocode}
\newdimen\@@maxwidth 
\newbox\@@cBox 
\newbox\@@pBox 
\newbox\@@pLineBox
\newbox\@@aLineBox 
\newif\if@@Nested 
\newif\if@@moreLines
\newcommand{\@@space}{}
\def\@@space{ }
%    \end{macrocode}
% \begin{tabular}{lp{9.4cm}}
%   "\@@maxwidth" & The largest width of a premise \\
%   "\@@cBox" & Holds the conclusion when it has been builded \\
%   "\@@pBox" & The premises is builded in this register  \\
%   "\@@pLineBox" & Used to build a single line of the premiseses \\
%   "\@@aLineBox" & Contains the line to be adjusted  \\
%   "\@@moreLines" & Flag telling if there is more lines of premises to process \\
%   "\@@space" & Macro with a single space---used for comparision
% \end{tabular}
%     
% "\@@Nested" defined above under the ``Translation Diagrams'' is also
% used as a flag for nesting, when drawing inference rules.
%
% \begin{macro}{\predicate}
% \begin{macro}{\predicatebegin}
% \begin{macro}{\predicateend}
% \changes{1.0}{1995/18/10}{Changed the names to avoid conflict with \LaTeX}
%   "\predicate" controls the setting of a single predicate cf.\ 
%   p.~\pageref{pattern matching}.
%    \begin{macrocode}
\newcommand{\predicate}[1]{\predicatebegin #1\predicateend}
\newcommand{\predicatebegin}{}
\newcommand{\predicateend}{}
%    \end{macrocode}
% \end{macro}
% \end{macro}
% \end{macro}
%
% \begin{macro}{\inference}
% \changes{1.0}{1995/18/10}{Changed some names due to a conflict with \LaTeX's \CSname{rule}}
% \changes{1.01}{1995/11/07}{Inserted a space in front of the name using \CSname{name\-space}}
% \changes{1.1}{1995/11/15}{Removed \CSname{@pInference}}
%   This is the central macro. It first examens if there is an optional name of
%   the inference rule. This can be recognized by being encapsulated in
%   brackets. If this is not given an empty argument is added ie.\ 
%   "[]", before the control is passed to "\@inference".
%    \begin{macrocode}
\newcommand{\inference}{}
\def\inference{\@ifnextchar[{\@inference}{\@inference[]}} 
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\@inference}
%   \changes{1.01}{1995/11/07}{Introduced a lowering of the inference so that the central line flushes with a possibly colon in the surronding text}
%   \changes{1.01}{1995/11/07}{Removed \CSname{strut} from the conclusion}
%   \changes{1.01}{1995/11/07}{Changed the formula for calculating the placement of name to incorporate the above}
%   \changes{1.1$\gamma$}{1995/11/12}{Added \CSname{@setLengths} in accordance with the changed length setting}
%   \changes{1.1$\beta$}{1995/11/21}{Added a test for vertical mode on the outermost level, where an extra box is needed}
%   \changes{1.1}{1995/11/25}{Placed the processing of the conclusion before the processing of premises so the premises can be made least the same width as the conclusion}
%   In this macro the inference rule is builded. It starts by evaluating the
%   different lengths, then the conclusion is set in "\@@cBox" (a possibly
%   space is removed---cf.\ the description in "@procesPremisesLine") so its
%   width is known when---as the next thing---the premises is set in "\@@pBox".
%   Before processing the premises there is tested for nesting. If the current
%   rule is not nested it is marked with "\@@NestedTrue" that a possibly 
%   "\inference" in its premises is in fact nested.
%   
%   After setting the conclusion and premieses the distance between the
%   premises, the line and the conclusion is calculated, so the appearance of
%   the rule is like a fraction (see below for a elaboration of the formulas).
%   The width of the inference is found as the maximum of the width of the
%   premises respectively the conclusion. If present the name is added to the
%   right and if this rule is on the outermost level it is lowered so the rule
%   flushes the center of a colon in the surrounding text ($\frac{1}{2}$"ex").
%    \begin{macrocode}
\newcommand{\@inference}[3]{}
\long\def\@inference[#1]#2#3{{%
  \@setLengths%
  \setbox\@@cBox=%
   \hbox{\hskip\@@pEnd \predicate{\ignorespaces#3}\unskip\hskip\@@pEnd}%
  \if@@Nested \@premises{#2}%
  \else \@@Nestedtrue \@premises{#2}\@@Nestedfalse \fi%
  \setbox3=\hbox{\footnotesize #1}%
  \setbox1=\hbox{$ $}%
  \dimen4=3\fontdimen8\textfont3% Minimum distance from the rule
  \dimen1=\fontdimen8\textfont2\advance\dimen1 by-\fontdimen22\textfont2%
    \advance\dimen1 by-.5\fontdimen8\textfont3%
    \advance\dimen1 by-\dp\@@pBox%
  \ifdim \dimen1<\dimen4 \dimen1=\dimen4\fi%
  \dimen2=\fontdimen22\textfont2\advance\dimen2 by\fontdimen11\textfont2%
    \advance\dimen2 by-.5\fontdimen8\textfont3%
    \advance\dimen2 by-\ht\@@cBox%
  \ifdim \dimen2<\dimen4\dimen2=\dimen4\fi%
  \dimen3=-.425ex\advance\dimen3 by .5\fontdimen8\textfont3%
    \advance\dimen3 by\ht\@@cBox\advance\dimen3 by\dimen2%
  \dimen4=\ht\@@cBox \advance\dimen4 by\dimen2%
    \advance\dimen4 by .5\fontdimen8\textfont3%
    \advance \dimen4 by-\fontdimen22\textfont2%
  \ifdim\wd\@@pBox >\wd\@@cBox% 
    \dimen0=\wd\@@pBox% 
  \else%
    \dimen0=\wd\@@cBox%
  \fi%
  \setbox1=\hbox{\vbox{%
    \unvbox\@@pBox%
    \vskip\dimen1%
    \hrule width\dimen0 height\fontdimen8\textfont3%
    \vskip\dimen2%
    \hbox to\dimen0{\unhbox\@@cBox}% 
    }}%
  \ifdim \wd3 > 0pt%
    \setbox1=\hbox{\unhbox1 \hskip\@@nSpace \raise\dimen3\box3}%
  \fi%
  \if@@Nested \box1 \else %
    \ifvmode \hbox{\lower\dimen4\box1}%
    \else \lower\dimen4\box1 \fi%
  \fi%
}}
%    \end{macrocode} 
%   To calculate the different distances some parameters from the math fonts is
%   used. It is therefore necessary to do a shift to math mode 
%   (\verb*"\hbox{$ $}") to get NFSS to load the current math font. The four
%   parameters used are:
%
%    \begin{tabular}{cl}
%      $\delta_{8,3}$  & rule thickness \\
%      $\delta_{8,2}$  & raising above the baseline of a numerator \\
%      $\delta_{11,2}$ & lowering below baseline of a denominator \\
%      $\delta_{22,2}$ & the rule's distance above baseline 
%    \end{tabular}
%
%    From this the different baselines etc.\ can be found:
%
%    \begin{tabular}{cll}
%      $t$        & rule thickness                & $\delta_{8,3}$ \\
%      $b_r$      & vertical center of the rule   & $\delta_{22,2}+\delta_{11,2}$ \\
%      $b_p$      & baseline for the premises     & $\delta_{8,2}+\delta_{11,2}$ \\
%      $b_n$      & baseline for a name           & $g_s - \frac{1}{2}\mathtt{ex}$ \\
%      $d_{\min}$ & minimumdistance from the rule & $3\delta_{8,3}$
%    \end{tabular}
%
%    and this gives the different distances used when setting the inference
%    rule:
%
%    \smallskip
%    \begin{tabular}{lll}
%      dimen 1 & distance between the premises and rule \\
%              &  $ b_p - b_r - \frac{1}{2}t - \mathrm{depth}_\mathrm{premises} = $\\
%              &  $\delta_{8,2}-\delta_{22,2}-\frac{1}{2}\delta_{8,3} - \mathrm{depth}_\mathrm{premises}$ \\ \hline            
%      dimen 2 & distance between the conclusion and the rule \\
%              &  $ b_r - \frac{1}{2}t - \mathrm{height}_\mathrm{conclusion} = $\\
%              &  $\delta_{8,2}+\delta_{22,2}-\frac{1}{2}\delta_{8,3}-\mathrm{height}_\mathrm{conclusion}$ \\ \hline
%      dimen 3 & the raising of the name \\
%              &  $ -85\% \cdot \frac{1}{2} \mathtt{ex} +\frac{1}{2}\delta_{8,3} + \mathrm{height}_\mathrm{conclusion} + \mathrm{dimen}_2$ \\ \hline
%      dimen 4 & Lowering to give the rule the right height above the baseline \\
%              &  $ \mathrm{height}_\mathrm{conclusion}+\mathrm{dimen}_2 + \delta_{8,3} - \delta_{22,2} $
%    \end{tabular}
%    \smallskip
%
%    \noindent
%    If "\dimen 1" or "\dimen 2" becomes lower than 
%    $d_{\min}$ its value is set to $d_{\min}$.
%    
%   After these acrobatic mathematical excercises the inference rule can be
%   set. First the inference is set in "\box 1". If a name is supplied 
%   it is added to the box. On the most level (ie.\ if "\if@@Nested" is 
%   false) the box should be lower. If \TeX\ is in vertical mode
%   "\lower" cannot be used, so in this case the inference is encapsulated in 
%   a "\hbox".
% \end{macro}
%
% \subsubsection{Processing of Premises}
%
% Then comes the code that processes a list of premises and set them in
% "\@@pBox". I do a lot of gambots adding and deleting extra tokens so that
% \TeX's pattern mathcing on macro arguments can be used to find nestings,
% linebreaks etc.\ as I assume this to be faster than actually reading 
% one token a time using \TeX\ primitives.
%
% \begin{macro}{\@premises}
%   \changes{1.1}{1995/11/25}{Initially set \CSname{@max\-width} equal to the width of the conclusion}
% \changes{1.1$\gamma$}{1995/11/12}{Changed \CSname{@premises} so the premises can be over several lines}
%   This initialises the processing of the list of premises line by line. A
%   line is recognised in "\@processPremises", which does the processing by
%   matching on its following "\\". As there is not a "\\" after the last
%   premise I insert \verb*"\\ \end" as an end marker after the list of
%   premises. In this way "\@processPremises" can assume that every line is
%   followed by "\\" and if this is followed by "\end", it has reached the
%   end.
%    \begin{macrocode}
\newcommand{\@premises}[1]{%
  \setbox\@@pBox=\vbox{}%
  \dimen\@@maxwidth=\wd\@@cBox%
  \@processPremises #1\\\end%
  \@adjustPremises%
}
%    \end{macrocode}
%   In cases where there---as an example---is two narrow premises on one line
%   and a wide on another line it would look strange if the distance between
%   the two premises where fixed. I therefore add som strechable glue
%   between the premises and at the end (with half the strechability) 
%   cf.~p.~\pageref{space setting}. To accomplish this I need to know the 
%   width of the widest line, but this can only be found while processing
%   the premises. It is saved in "\@@maxwidth" so "\@adjustPremises" adjust 
%   all line to it. By initially setting "\@@maxwidth" to the width of the
%   conclusion no lines will be narrower than the conclusion. And due to the
%   glue, the premises will appear centered if the conclusion is wider than the
%   premises.
% \end{macro}
%
% \begin{macro}{\@adjustPremises}
%   The adjusting of the lines of premises to "\@@maxwidth":
%    \begin{macrocode}
\newcommand{\@adjustPremises}{%
  \setbox\@@pBox=\vbox{%
    \@@moreLinestrue %
    \loop %
      \setbox\@@pBox=\vbox{%
        \unvbox\@@pBox %
        \global\setbox\@@aLineBox=\lastbox %
      }%
      \ifvoid\@@aLineBox %
        \@@moreLinesfalse %
      \else %
        \hbox to \dimen\@@maxwidth{\unhbox\@@aLineBox}%
      \fi % 
    \if@@moreLines\repeat%
  }%
}
%    \end{macrocode}
%   The lines set are put in "\@@pBox" in reverse order. They are taken from
%   "\@@pBox" one by one by emptying ("\unvbox") "\@@pBox", setting
%   "\@@aLineBox" to the last box in the vertical list just emptied and putting
%   the rest back in "\@@pBox". I do not expect this to be as bas as it sounds,
%   because presumably the "\unvbox" is not a actual copying but only some
%   pointer operation, which can be done in constant time (cf.\ the hints on
%   \cite[120]{texbook}).
%   
%   All this is done inside a "\vbox" so the contents of "\@@aLineBox" can be
%   added to the list being build simply using "\hbox to "\lttdots\ (doing the
%   adjusting simultaneousnessly). Being inside a "\vbox" has the additional
%   advantage that \TeX\ is in internal vertical mode so there
%   automaticly is added lineskip in accordance with "\baselineskip" etc.\ 
%   (cf.~\cite[80]{texbook}). As the macro in no sense is recursive there is no
%   problem in globally changing "\@aLineBox"
% \end{macro}
% 
% \begin{macro}{\@processPremises}\mbox{}^^A
% \changes{1.1$\beta$}{1995/11/21}{Fixed bug that made an empty premise sometimes contain \CSname{pSpace}}
% \changes{1.1$\beta$}{1995/11/21}{Moved the processing of spaces to \CSname{@inferenceOrPremis}}
%    \begin{macrocode}
\newcommand{\@processPremises}[2]{}
\def\@processPremises#1\\#2\end{%
  \setbox\@@pLineBox=\hbox{}%
  \@processPremiseLine #1&\end%
  \setbox\@@pLineBox=\hbox{\unhbox\@@pLineBox \unskip}%
  \ifdim \wd\@@pLineBox > 0pt %
    \setbox\@@pLineBox=%
      \hbox{\hskip\@@pEnd \unhbox\@@pLineBox \hskip\@@pEnd}%
    \ifdim \wd\@@pLineBox > \dimen\@@maxwidth %
      \dimen\@@maxwidth=\wd\@@pLineBox %
    \fi %
    \setbox\@@pBox=\vbox{\box\@@pLineBox\unvbox\@@pBox}%
  \fi %
  \def\@temp{#2}%
  \ifx \@temp\empty \else %
    \@processPremises #2\end %
  \fi%
}
%    \end{macrocode}
%   The pattern splits the list of premises into the first
%   line (\#1---possibly empty an empty) and the following lines
%   (\#2---possibly containing no lines). The first line is set in
%   "\@@pLineBox" using "\@processPremiseLine" which like "\@processPremises"
%   gets "&\end" added so it recognize the end of line. After the line has been
%   set its width is examened and if, it is not zero \semantic\ concludes that
%   the premise is not empty and adds it to "\@@pBox", which when finished
%   shall contain the lines (in reverse order---cf.~"\@adjustPremises"), and if
%   necessary "\@@maxwidth" is increased. At last it is examened wether the
%   \emph{following the lines} is not-empty, ie.\ there is more lines to
%   process, and if that is the case they are processed.
% \end{macro}
%
% \begin{macro}{\@processPremiseLine}\mbox{}^^A
% \changes{1.1$\delta$}{1995/12/01}{Fixed bug that axioms could not be handled using pattern matching}
%    \begin{macrocode}
\newcommand{\@processPremiseLine}[2]{}
\def\@processPremiseLine#1&#2\end{%
  \def\@temp{#1}%
  \ifx \@temp\empty \else%
    \ifx \@temp\@@space \else%
    \setbox\@@pLineBox=%
      \hbox{\unhbox\@@pLineBox%
            \@inferenceOrPremis #1\inference\end%
            \hskip\@@pSpace}%
    \fi%
  \fi%
  \def\@temp{#2}%
  \ifx \@temp\empty \else%
    \@processPremiseLine#2\end%
  \fi%
}
%    \end{macrocode}
%   The pattern splits the line into the first premise (\#1---possibly
%   empty) and the following premises (\#2---possibly none). It is then
%   tested if the first premise is non-empty, which in this context means that
%   it is neither empty nor a space (\verb*+& &+ should be regarded as an 
%   empty premise. If it in fact contains a premise it is set using
%   "\@inferenceOrPremis" and an approriate spacing to the next premise is
%   added. Note that this space is also added after the last premise but then
%   removed again, when \LaTeX\ has returned to "\@processPremises".
      
%   After processing the first line it is tested if there are any premises in the
%   \emph{following premises} and in that case "\@processPremisesLine" is used
%   tail recursively.
% \end{macro}
%
% \begin{macro}{\@inferenceOrPremis}
% \begin{macro}{\@processInference}
%   "@inferenceOrPremis" decides wether there is a nested "\@inference" in a
%   premise. It is done using the scheme as above, where the premise is
%   appended with "\inference \end". There is then matched on "\inference" and
%   if it followed by "\end" it is concluded that premise did not original
%   contain a nesting (ie.\ "\inference"). In this case the "\end"-token is
%   removed and the premise is set using "\predicate". Otherwise "\inference"
%   "\end" is removed and the inference rule is set---all this done by
%   "\@processInference".
%    \begin{macrocode}
\newcommand{\@inferenceOrPremis}[1]{}
\def\@inferenceOrPremis#1\inference{%
  \@ifnext \end {\@dropnext{\predicate{\ignorespaces #1}\unskip}}%
  {\@processInference #1\inference}} 
\newcommand{\@processInference}[1]{}
\def\@processInference#1\inference\end{\ignorespaces #1\unskip}
%    \end{macrocode}
%   It is natural to make spaces around \& when keying in the document,
%   which---if not removed---would give rise to (superfluous) spaces around the
%   premise in addition to the space added by "\@infenceOrPremis". Spaces
%   preceding the premise is removed using the primitive "\ignorespaces" and
%   spaces following is first set and then removed using "\unskip". When nested
%   this is not done until "\@processInference" as the rule would be changed
%   with a "\unskip" immediately after "inference" ("\inference{"\lttdots"}"
%   would become "\inference \unskip {"\lttdots"}").
% \end{macro}
% \end{macro}
%
% \subsection{Preamble of Users Guide and Documentation}
% \changes{1.0}{1995/10/16}{Made "semantic.sty" into a ".dtx"-file with a stub for generating the users guide and documentation}
% \changes{1.0}{1995/10/16}{Added control that the requested files is in fact  installed}
% \changes{1.2$\alpha$}{1996/01/28}{Put the documentheader at the bottom and introduced a hack making \LaTeX\ thinks it is loading \texttt{semantic.sty} when processing \texttt{semantic.dtx}}
%
% The documentpreamble and the code to generate code is placed last so that
% the documentation could be printed without \semantic\ being yet installed.
% To the use of \package{docstrip} the code is marked as conditional
%   code, so that it is not included in "semantic.sty" when installing the
% package.
%    \begin{macrocode}
%<*documentation>
\documentclass{ltxdoc} 
\usepackage[cp850]{inputenc} 
\usepackage[T1]{fontenc}
 % Checks if the package for multiple columns is installed and if that 
 % is the case, then load it. Borrowed from the standard package \
 % ``doc.dtx'' 
\newif\ifmulticols 
\IfFileExists{multicol.sty}{\multicolstrue}{}

\newif\ifdanger
\dangertrue       % Make this line into a comment, if the manual font
                  % ``manfnt.tfm'' is not installed on your system
\DeclareFontFamily{U}{manual}{} 
\DeclareFontShape{U}{manual}{m}{n}{<->  manfnt }{} 

\newcommand{\danger}
  {{\fontencoding{U}\fontfamily{manual}\selectfont\symbol{127}}}

\OnlyDescription    % Make to a comment to get the documentation
\DisableCrossrefs   % Remove comment if the index is ready or if you
                    % do not wish the index (e.g. when only printing
                    % the users guide)
%\CodelineIndex      % Make a index of the command usage
%\RecordChanges      % Make the changes history

\makeatletter

\newcommand{\semantic}{\texttt{semantic}}
\newcommand{\lttdots}{\ensuremath{\mathtt{\ldots}}}
\newcommand{\CSname}[1]{\texttt{\protect\bslash#1}}
\newcommand{\package}[1]{\textsf{#1}}

\def\GetInfo#1{%
  \def\filename{#1}%
  {\def\ver##1(##2)##3\relax{%
     \def\tc{##1}%
     \def\td{##2}%
     \ifx \td\empty %
     \else %
      \edef\td{$\csname ##2\endcsname$}%
     \fi}%
   \def\tb##1 v##2 ##3\end{%
   \gdef\filedate{##1}%
     \ver ##2()\relax%
     \xdef\fileversion{\tc\expandafter\noexpand\td}%
    \gdef\fileinfo{##3}}%
  \edef\ta{\csname ver@#1\endcsname}%
  \expandafter\tb\ta\end\relax}}

\newtoks\p@rm@rk 
\newcommand{\setparagraphmark}[1]{\p@rm@rk={#1}}
\newcommand{\parmark}[1][\the\p@rm@rk]{%
  \setbox0=\hbox{\huge #1}%
  \clubpenalty=10000%
  \noindent\hangindent=\wd0 \hangafter=-2%
  \llap{\raise.35em\hbox{\vbox to0pt{\box0 \vss}\hfill}}}

\newenvironment{code}
  {\begin{verse}\small}
  {\end{verse}}

\newenvironment{columnItemize}%
  {\begin{list}%
    {$\bullet$}%
    {\settowidth{\labelwidth}{$\bullet$}%
     \setlength{\leftmargin}{5mm}%
     \setlength{\labelsep}{\leftmargin}%
     \addtolength{\labelsep}{-\labelwidth}}}%
  {\end{list}}

\typeout{}
\typeout{NOTE: If LaTeX complains}
\typeout{\@spaces\@spaces Font U/manual/m/n/9 manfnt at 9.0 not loadable: ...}
\typeout{\@spaces\space\space then comment out the line (around 1600)}
\typeout{\@spaces\@spaces \protect\dangertrue}
\typeout{}
\typeout{There will be a 1 overfull box and 8 moved marginpars}
\typeout{Do not bother!!!}
\typeout{}

\makeatother

\begin{document}
   \DocInput{semantic.dtx}
\end{document}
%</documentation>
%    \end{macrocode}
% The preamble contains the normal choosing of codetables etc., it checks if
% the requested non-standard package can be found, it defines some
% commands (described below) for the use of the documentation and types out
% some ``relaxing'' messages to the users. I do not know
% any way to check if a named font is on the system---"\IfFileExist" cannot
% be used as it searches the path in---say---"TEXINPUT" while the fonts are
% searched using the path "TFMINPUT".
% 
% The commands defined are:
% \begin{description}
% \item[\CSname{ifmulticols}] conditional ensuring that \TeX\ branches over
%   parts setting up multiple columns, when this is not provided.
% \item[\CSname{ifdanger}] conditional that tells whether the dangerous bend
%   sign from \emph{The \TeX-book} is available. The manualfont ("manfnt")
%   is declared to NFSS and the command "\danger" is defined anyway. It will
%   however only be used and therefore tried loaded if "\ifdanger" is true.
% \item[\CSname{semantic}] gives the package-symbol (name in a typewriter-font)
% \item[\CSname{lttdots}] gives ellipsis in a typewriter-font
% \item[\CSname{CSname}] typeset a commandname when it is not possible using 
%   the standard notation, |"|\lttdots|"|, from \package{ltxdoc} (eg.\ in
%   headers). Intentionally given a name close to \TeX's "\csname".
% \item[\CSname{package}] sets the name of \LaTeX-package.
% \item[\CSname{GetInfo}] defines the commands "\fileversion", "\filedate"
%   and "\fileinfo" with information about \semantic\ as provided in
%   "\providespackage". It is mainly borrowed from a command with the same
%   name in \package{ltxdoc} but has been changed to type the additional
%   greek letter in the package version provided in parenthesis.
% \item[\CSname{parmark} and \CSname{setparagraphmark}] is used to set a
% given symbol in front of a paragraph. "\setparagraphmark" defines the
% symbol to be used by "\parmark" if no argument is given explicit.
% \item[\texttt{code}] Environment for displaying examples in the Users Guide.
% \item[\texttt{columnitemize}] Makes an itemizing where the bullet is not
%   idented, which would make the text too narrow when using columns.
% \end{description}
%
% \begin{thebibliography}{1}
%   \bibitem{texbook}    
%     \textsc{D.E.~Knuth} \emph{The \TeX-book}, 1994, Addison-Wesley
%^^A   \bibitem{companinon} 
%^^A     \textsc{M.~Goosens, F.~Mittelbach, and A.~Samarin} \emph{The \LaTeX{} Companion}, 1994, Addison-Wesley
%   \bibitem{packagesguide}
%     \textsc{The \LaTeX3 Project} \emph{\LaTeXe\ for class and packages writers}, 10 June 1995
% \end{thebibliography}
%
% \Finale \PrintIndex \sloppy \PrintChanges
\endinput