summaryrefslogtreecommitdiff
path: root/macros/latex/contrib/semantic/semantic.dtx
diff options
context:
space:
mode:
authorNorbert Preining <norbert@preining.info>2019-09-02 13:46:59 +0900
committerNorbert Preining <norbert@preining.info>2019-09-02 13:46:59 +0900
commite0c6872cf40896c7be36b11dcc744620f10adf1d (patch)
tree60335e10d2f4354b0674ec22d7b53f0f8abee672 /macros/latex/contrib/semantic/semantic.dtx
Initial commit
Diffstat (limited to 'macros/latex/contrib/semantic/semantic.dtx')
-rw-r--r--macros/latex/contrib/semantic/semantic.dtx2881
1 files changed, 2881 insertions, 0 deletions
diff --git a/macros/latex/contrib/semantic/semantic.dtx b/macros/latex/contrib/semantic/semantic.dtx
new file mode 100644
index 0000000000..fb5aab6453
--- /dev/null
+++ b/macros/latex/contrib/semantic/semantic.dtx
@@ -0,0 +1,2881 @@
+% \RCS$Revision: 1.11 $
+% \RCS$Date: 2003/10/28 13:45:57 $
+%
+%\iffalse metacomment
+%
+%%
+%% semantic.dtx (c)1995--2002 Peter Møller Neergaard and
+%% Arne John Glenstrup
+%%
+%
+% This program may be distributed and/or modified under the
+% conditions of the LaTeX Project Public License, either version 1.2
+% of this license or (at your option) any later version.
+% The latest version of this license is in
+% http://www.latex-project.org/lppl.txt
+% and version 1.2 or later is part of all distributions of LaTeX
+% version 1999/12/01 or later.
+%
+% This program consists of the files semantic.dtx and semantic.ins
+%
+% This file is the source code containing the package.
+%
+% You install the package by running tex on semantic.ins, i.e.,
+%
+% tex semantic.ins
+%
+%\fi
+% \DeleteShortVerb{\|}
+% \CheckSum{1918}
+% \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{\"}
+%
+% \title{The \semantic\ package\thanks
+% {This file has version \semanticVersionPrint\ and is dated
+% \semanticDate. It is CVS revision \RCSRevision, dated \RCSDate.}\thanks{Michael John Downes of AMS provided a patch to
+% make the \semantic compatible with \texttt{amsmath} v.2.01.}}
+% \author{Peter M{\o}ller Neergaard^^A
+% \thanks{\texttt{turtle}@\texttt{turtle@linearity.org},
+% \texttt{http://linearity.org/turtle}} \\
+% Arne John Glenstrup^^A
+% \thanks{\texttt{panic}@\texttt{diku.dk},
+% \texttt{http://www.diku.dk/\lower0.7ex\hbox{\~{}}panic}}}
+% \maketitle
+%
+% \begin{abstract}
+% The aim of this package is to help people doing programming
+% languages using \LaTeX. The package provides commands that
+% facilitates the use of the notation of semantics and compilation
+% in your documents. It provides an easy way to define new
+% ligatures, \eg making "=>" a short hand for \cmd{\RightArrow}. It
+% fascilitates the drawing of inference rules and allows you to draw
+% T-diagrams in the "picture" environment. It supports writing
+% extracts of computer languages in a uniform way. It comes with a
+% predefined set of shorthand suiting most people.
+% \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 facilitating the writing
+% of notation of programming languages and compilation. To use it, the
+% file "semantic.sty" should be placed so that \LaTeX\ can find
+% it.
+%
+% The \semantic\ package consists of several parts, which can be used
+% independently. The different parts are
+%
+% \begin{description}
+% \item[Ligatures] providing an easy way to define ligatures for often used
+% symbols like $\Rightarrow$ and $\vdash$.
+% \item[Inference Rules] fascilitating the presentation of inference rules and
+% derivations using inference rules.
+% \item[T-diagrams] providing T-diagrams as an extension the "picture"
+% environment.
+% \item[Reserved word\footnote{A better name is highly needed.}] fascilitating
+% getting a uniform appearance of langugage constructions.
+% \item[Short hands] for often used symbols.
+% \end{description}
+%
+% In the following we describe the use of the various parts of
+% \semantic and the installation. We also give a short introduction to the
+% two files "semantic.dtx" and "semantic.ins".
+%
+% This package is---like most other computer-programs---provided with
+% several bugs, insuffiencies and inconsistencies. They should be regarded
+% as features of the package. To increase the excitement of using the package
+% these features appear in unpredictable places. If they
+% however get too annoying and seriously reduce your satisfaction with
+% \semantic, please notify us. You could also drop us a note if you
+% would like to be informed when \semantic\ is updated.
+%
+% \ifmulticols
+% \end{multicols}
+% \fi
+%
+% \iffalse^^A At the moment no bugs are known
+% \ifmulticols
+% \begin{multicols}{2}[\section*{Known Bugs}
+% \fi
+% \begin{columnItemize}
+% \end{columnItemize}
+%
+% \ifmulticols
+% \end{multicols}
+% \fi
+% \fi
+%
+% \section{Loading}
+%
+% There is two ways of loading the \semantic\ package. You can either load
+% it with all the parts, or to save time and space, you can load, only the
+% parts you will use.
+%
+% In the first case you just include
+% \begin{code}
+% \cmd{\usepackage}\marg{semantic}
+% \end{code}
+% in your document preamble.
+%
+% In the other case you include
+% \begin{code}
+% \cmd{usepackage}\oarg{parts}\marg{semantic}
+% \end{code}
+% in your document preamble. \meta{parts} is a comma
+% separated list of the parts you wants to include. The possibilities
+% are: "ligature", "inference", "tdiagram", "reserved", and
+% "shorthand". The different parts are described in detail below.
+%
+% \section{Math Ligatures}
+% \subsection{Defining New Math Ligatures}
+% \label{sec:DefiningNewMathLigatures}
+%
+% \DescribeMacro{\mathlig} When the package is loaded, you can define new
+% ligatures for use in the math environments by using the
+% \cmd{\mathlig}\marg{character sequence}\marg{ligature commands}
+% command. \meta{character sequence} is a sequence of
+% \DeleteShortVerb{\"}\DeleteShortVerb{\|}^^A
+% characters\footnote{There are some restrictions on the characters you can
+% use. This should be described here but isn't; basically you should stick
+% to using the characters
+% \texttt{\frenchspacing ` " ' \~{}
+% ! ? @ * ( ) [ ] < > - + = | : ; . , / 0\ldots 9}, and certainly this
+% should suffice for any sane person.}^^A
+% \MakeShortVerb{\"}
+% that must be entered in the source file to achieve the effect of the
+% \meta{ligature command}. If for example you write
+% `"\mathlig{-><-}{\rightarrow\leftarrow}"', subsequently typing `"$-><-$"'
+% will produce $\rightarrow\leftarrow$.
+%
+% \subsection{Turning Math Ligatures On and Off}
+% \label{sec:TurningMathLigaturesOnAndOff}
+%
+% \DescribeMacro{\mathligson}\DescribeMacro{\mathligsoff} By default, math
+% ligatures are in effect when the \package{mathligs} package is loaded,
+% but this can be turned off and on by using the commands \cmd{\mathligsoff} and
+% \cmd{\mathligson}. Thus, typing `"$-><-$" \cmd{\mathligsoff} "$-><-$"
+% \cmd{\mathligson} "$-><-$"'
+% will produce $\rightarrow\leftarrow$ $-{}>{}<{}-$ $\rightarrow\leftarrow$.
+%
+% \subsection{Protecting Fragile Math Commands}
+% \label{sec:ProtectingFragileMathCommands}
+%
+% \DescribeMacro{\mathligprotect} Unfortunately, some macros used in math
+% mode will break when using
+% \package{mathligs}, so they need to be turned into protected macros with the
+% declaration \cmd{\mathligprotect}\marg{macro}. \emph{NOTE:} This
+% declaration only needs to be issued once, best in the preamble.
+%
+%
+% \section{Inference Rules}
+%
+% \DescribeMacro{\inference}
+% \DescribeMacro{\inference*}
+% Inference rules like
+% {\def\predicatebegin#1|-#2=>#3\predicateend{$#1 \vdash \texttt{#2} \Rightarrow #3$}
+% \[
+% \inference[It(1) :]{\rho|-$E$=>\textsc{False}}
+% {\rho|-while $E$ do $s$=>\rho }
+% \quad\quad
+% \inference*[It(2) :]{\rho|-$E$=>\textsc{True} & \rho|-$s$=>\rho' \\
+% \rho'|-while $E$ do $s$=>\rho''}^^A
+% {\rho|-while $E$ do $s$=>\rho''}
+% \]}
+% and
+% \[
+% \inference[$->*_1$]{p,\mathrm{M} ->* p',\mathrm{M'} \\
+% p',\mathrm{M'} -> p'',\mathrm{M''}}
+% {p,\mathrm{M} ->* p'',\mathrm{M''}} \;\;\;\;
+% \inference[$->*_2$]{}{p,\mathrm{M} ->* p,\mathrm{M}}
+% \]
+% are easily set using \cmd{\inference} and \cmd{\inference*}. The syntax is
+% \begin{code}
+% \cmd{\inference}\oarg{name}"{"\meta{line$_1$}" \\ \cmd{\lttdots} \\ "\meta{line$_n$}"}"\marg{conclusion}
+% \end{code}
+% and
+% \begin{code}
+% \cmd{\inference}"*"\oarg{name}"{"\meta{line$_1$}" \\ \cmd{\lttdots} \\ "\meta{line$_n$}"}"\marg{conclusion}
+% \end{code}
+% where $n \geq 0$ so that you can also type axioms. When using
+% \cmd{\inference} the bar will be as wide as the conclusion and the premise,
+% whichever is widest; while \cmd{\inference*} only will make the
+% bar as wide as the conclusion (It(2) above). The
+% optional names are typeset on the side of the inferences that they appear.
+%
+% Each line consists of premises seperated by "&":
+% \begin{code}
+% \meta{premise$_1$}"&\cmd{\lttdots}&"\meta{premise$_m$}
+% \end{code}
+% Note that $m$ can also be zero, which is used when typing axioms. Each
+% premise and the conclusion are by default set in math mode (\see however
+% \pageref{ref:changePredicateBegin}).
+%
+% The rules are set so that the line flushes 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. One may also set the rules in a table as shown
+% below:
+%
+% \begin{tabular}{ll}
+% Transitive (1): &
+% \inference{p,\mathrm{M} ->* p',\mathrm{M}' \\
+% p',\mathrm{M'} -> p'',\mathrm{M''}}
+% {p,\mathrm{M} ->* p'',\mathrm{M''}} \\
+% Transitive (2): &
+% \inference{}{p,\mathrm{M} ->* p,\mathrm{M}}
+% \end{tabular}
+%
+% An inference rule can be nested within another rule without problems,
+% like in:
+% \[
+% \inference[$->*_1$]{
+% \inference[$->*_1$]{
+% \inference[$->*_2$]{}
+% {p,\mathrm{M} ->* p,\mathrm{M}} &
+% p,\mathrm{M} ->* p',\mathrm{M'}}
+% {p,\mathrm{M} ->* p',\mathrm{M'}} &
+% p',\mathrm{M'} -> p'',\mathrm{M''}}
+% {p,\mathrm{M} ->* p'',\mathrm{M''}}
+% \]
+%
+% \subsection{Controlling the Appearance}
+% \DescribeMacro{\setpremisesend}
+% \DescribeMacro{\setpremisesspace}
+% \DescribeMacro{\setnamespace}
+% The appearance of the inferences rules can be partly 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
+% \cmd{\setnamespace}\marg{length}, \cmd{\setpremisesend}\marg{length} and
+% \cmd{\setpremisesspace}\marg{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" and $\frac{1}{2}$"em" for "namespace".
+% Note that the lengths \emph{cannot} be altered using the ordinary
+% \LaTeX-commands \cmd{\setlength} and \cmd{\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.
+%
+% {\small ^^A This description is only for TeXnichians and it it therefore
+% ^^A written in a smaller font.
+% \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}, we have
+% used double exclamation marks to indicate that you do not need 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 from top to bottom, the leaves get bigger
+% and the names get further from the line below.
+%
+% \subsection{Formatting the Entries}
+% \parmark
+% \DescribeMacro{\predicate}
+% To set up a single predicate (a premise or conclusion) the single-argument
+% command \cmd{\predicate} is used. This allows a finer control of the
+% formatting. As an example, all premises and conclusions can be set in
+% mathematics mode by the command:
+% \begin{code}
+% "\renewcommand{\prediate}[1]{$ #1 $}"
+% \end{code}
+%
+% \parmark
+% \semantic\ uses \cmd{\predicate} on a premise only when the premise does not
+% contain a nested \cmd{\inference}.\footnote{What \semantic\ precisely does is
+% to append the tokens \cs{inference} \cs{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
+% \cs{inference}. When this is found the following token is examened,
+% and if it is \cs{end}, \semantic\ concludes that the premise does not
+% contain a nested inference rule} So even if the declaration above has been
+% given, \cmd{\inference} is \emph{never} be executed in math mode. Neither is
+% it used on the premises if you write:
+% \begin{code}
+% "\inference{\inference"\lttdots"}{"\lttdots"}"
+% \end{code}
+%
+% \parmark
+% \DescribeMacro{\predicatebegin}
+% \DescribeMacro{\predicateend}
+% \label{ref:changePredicateBegin}
+% The default definition of \cmd{\predicate} is "\predicatebegin #1\predicateend",
+% where \cmd{\predicatebegin} and \cmd{\predicateend} are defined to `"$"'. In this
+% way the premises and conlusions are set in math
+%
+% \parmark
+% The motivation for introducing \cmd{\predicatebegin} and \cmd{\predicateend}
+% was, however, to use \TeX's pattern matching on macro arguments to do even
+% more sophisticated formatting by redefining \cmd{\predicatebegin}.
+% \label{pattern matching}
+% If for example, \emph{every} \textsl{expression} is to be evaluated in an
+% \textsl{environment} giving a \textsl{value}, and you would like to set
+% \emph{all} the \textsl{environment's} \textsl{values} in mathematics and the
+% \textsl{expressions} in \texttt{typewriter}-font, then this could be
+% facilitated 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 "ligatures" option \emph{has not} been used
+% above. }
+% ^^A TeXnichian mode OFF
+%
+% \section{T-diagrams}
+%
+% \DescribeMacro\compiler
+% \DescribeMacro\interpreter
+% \DescribeMacro\program
+% \DescribeMacro\machine
+% To draw T-diagrams describing the result of using one or more
+% compilers, interpreters etc., \semantic\ has commands for the diagram:
+% \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}
+% These commands should only be used in a "picture" environement and are
+% \begin{code}
+% \cmd{\program}"{"\meta{program}","\meta{implementation language}"}" \\
+% \cmd{\interpreter}"{"\meta{source}","\meta{implemenation language}"}" \\
+% \cmd{\compiler}"{"\meta{source}","\meta{machine}","\meta{target}"}" \\
+% \cmd{\machine}\marg{machine}
+% \end{code}
+% The arguments can be a either a string describing the language (please do
+% not begin the string with a macro name), or one of the four commands.
+% However, combinations taht make no sense---like implementing an
+% interpreter on a program---are excluded, yielding an error message like:
+% \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 use 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 T- diagrams can easily be
+% drawn. The hole construction should be placed using af \cmd{\put} command,
+% where the \emph{reference point} is the center of the bottom of the figure
+% corresponding to the outermost command. An example (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. The figure
+% \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 \cmd{\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, \emph{ie} the
+% second example could also be written (with a change of the parameters of
+% \cmd{\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 is often easier to start in
+% the middle, since this is where you get the least levels of nesting.
+%
+% Even though most situations may be handled by means of nesting, it is in
+% some rare cases adequate to use different
+% language symbols on the two sides of the line of touch.
+% When \emph{eg} describing bootstrappring the poor U-code
+% implementation can be symbolized by \texttt{U$^{-}$}, indicating that the
+% poor implementation is still executed on a \texttt{U}-machine. This can
+% be done by providing the symbol-command
+% with an optional argument immediately after the command name. Thus
+% the bootstrapping
+% \begin{center}
+% \begin{picture}(230,100)(-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}
+%
+% For calculating the dimensions of the "picture"-environment, one needs the
+% dimensions of the individual figures. In units of
+% \cmd{\unitlength} they are the following:
+%
+% \ifmulticols
+% \begin{multicols}{2}
+% \fi \noindent
+% compiler: 80*40 \\
+% interpreter: 20*40 \\
+% machine: 20*17.1 \\
+% program: 20*40
+% \ifmulticols
+% \end{multicols}
+% \fi
+%
+% \section{Reserved Words}
+% \label{sec:Reserved Words}
+%
+% ^^A \tracingmacros=1 \tracingonline=1
+% \reservestyle{\command}{\mathbf} \command{let,in}
+% \reservestyle{\punctuation}{\mathtt} \punctuation{=}
+% \tracingmacros=0
+%
+% When describing computer languages, one often wants to typeset commands in
+% one style, expressions in another style, and punctuation characters in
+% yet another style, for instance
+% \[
+% \<let> \; x \;\<=>\; e \;\<in>\; e
+% \]
+%
+% \DescribeMacro{\reservestyle}
+% The \semantic\ package supports this by allowing you to reserve a certain
+% \emph{style} for certain language constructs. The fundamental command is
+% \begin{code}
+% \cmd{\reservestyle}\marg{\cs{stylename}}\marg{formatting}
+% \end{code}
+% \cmd{\reservestyle} reserves \cs{\meta{stylename}} as the macro to define
+% the language constructs. The language constructs will be set using
+% \meta{formatting}.
+%
+% The reserved macro \cs{\meta{stylename}} should be given a comma
+% separated list of words to reserve. For instance to reserve the words
+% $\<let>$ and $\<in>$ as
+% commands, which all are set using a bold font, you can put
+% \begin{code}
+% "\reservestyle{\command}{\textbf}" \\
+% "\command{let,in}"
+% \end{code}
+% in the preamble of your document. Note that there must not any
+% superfloues space in the comma separated list.
+% Thus for instance \verb*+\command{let , in}+
+% would reserve $\setcommand{let\ExplicitSpace}$ resp.\
+% $\setcommand{\ExplicitSpace in}$ instead of $\<let>$ resp. $\<in>$!
+% You can of course reserve several styles
+% and reserve several words within each of the styles.
+%
+% \DescribeMacro{\<}
+% To refer to a \emph{reserved word} in the text you use the command
+% "\<"\meta{reserved word}">", \eg "\<let>". If you have reserved several
+% styles, \semantic will find the style that was used to reserve
+% \meta{reserved word} and use the appropriate formatting commands.
+%
+% The "\<"$\cdots$">" can be used in both plain text and in math mode. You
+% should, however, decide in the preamble if a given style should be used in
+% math mode or in plain text, as the formatting commands will be different.
+%
+% \DescribeMacro{\set\protect\meta{style}}
+% If you only want to type a reserved word a single time, it can seem tedious
+% first to reserve the word and then refer to it once using "\<"$\cdots$">".
+% Instead you can use the command \cs{set\meta{style}} that is defined for each
+% style you reserve.
+%
+% \subsection{Bells and Whistles: Spacing in Math Mode}
+%
+% In many situations it seems best to use \emph{reserved words} in math
+% mode---after all you get typesetting of expressions for free. The drawback
+% is that it becomes more difficult to get the space correct. One can of
+% course allways insert the space by hand, \eg "$\<let>\; x=e \;\<in>\; e'$",
+% However, this soon becomes tedious and \semantic have several ways to try to
+% work around this.
+%
+% The first option is to provide \cmd{\reservestyle} with an optional spacing
+% command, \eg \cmd{\mathinner}. For instance
+% \begin{code}
+% "\reservestyle[\mathinner]{\command}{\mathbf}"
+% \end{code}
+% will force all \emph{commands} to be typeset with spacing of math inner
+% symbols.
+%
+% You can also provide an optional space command to each reservation of
+% words. For instance
+% \begin{code}
+% "\command[\mathrel]{in}"
+% \end{code}
+% will make $\<in>$ use the spacing of the relational symbols. The space
+% command is applied to all the words in the reservation. Thus if you would
+% like $\<in>$ and $\<let>$ to have different space commands, you must
+% specify them in two different \cmd{\command}.
+%
+% The drawback of using the math spacing is that in the rare cases where you
+% use the reserved words in super- or subscripts, most of the spacing will
+% disappear. This can be avoided by defining the replacement text to be the
+% word plus a space, \eg "\;in\;". For this end a reservation of a word can
+% be followed by an explicit replacement text in brackets, \eg
+% \begin{code}
+% "\command{let[let\;], in[\;in\;]}"
+% \end{code}
+% The formatting of \cmd{\command} (with the setting above: \cmd{\mathbf}) will still
+% be used so it is only necessary to provide the replacement text. Note
+% that each word in the reservation can have its own optional replacement
+% text.
+%
+% The drawback of this method is, that the you also get the space, if you use
+% the reserved word ``out of context'', for instance refering to the
+% $\;\<in>\;$-token! In these cases you can cancel the space by hand using
+% "\!".
+%
+% This option is also usefull, if you want to typeset the same word in two
+% different styles. If you for instance sometimes want `let' to be typeset
+% as a command and sometimes as data, you can define
+% \begin{code}
+% "\command{let}" \\
+% "\data{Let[let]}"
+% \end{code}
+% Then "\<let>" will typeset the word `let' as a command, while "\<Let>" will
+% typeset it as data. Note that in both cases the word appears in
+% lower case.
+%
+% Unfortunately there is no way to get the right spacing everytime, so you
+% will have to choose which of the two methods serves you the best.
+%
+% \section{Often Needed Short Hands}
+%
+% Within the field of semantics there are a tradition for using some special.
+% symbols. These are provided as default as short hand in the \semantic\
+% package. Most of the following symbols are defined as ligatures, and
+% hence the "ligature" option is always implied when the "shorthand" option
+% is provided.
+%
+% \makeatletter
+% \subsection{The Meaning of: \@bblb\ and \@bbrb}
+% \marginpar{\raggedleft\strut\@bblb}
+% \marginpar{\raggedleft\strut\@bbrb}
+%
+% The symbols for denoting the meaning of an expression,
+% \@bblb\ and \@bbrb\ are provided as short
+% hands in math with the ligatures "|[" and "|]".
+% \makeatother
+%
+% \subsection{Often Needed Symbols}
+%
+% The following ligatures are defined for often needed symbols
+%
+% \begin{tabular}[c]{cl@{\qquad\qquad}cl}
+% $\vdash$ & "|-" & $\mathligsoff\models$ & "|=" \\
+% $<->$ & "<->" & $<=>$ & "<=>" \\
+% $->$ & "->" & $-->$ & "-->" \\
+% $=>$ & "=>" & $==>$ & "==>" \\
+% $<-$ & "<-" & $<--$ & "<--" \\
+% $<=$ & "<=" & $<==$ & "<==" \\
+% \end{tabular}
+%
+% All the single directed arrows also comes in a starred and plussed form, \eg\
+% "*<=" gives $*<=$ and "-->+" gives $-->+$.
+%
+% \DescribeMacro{\eval}
+% \DescribeMacro{\comp}
+% To support writing denotational, semantics the commands \cmd{\comp} and \cmd{\eval}
+% are provided to describe the evaluation of programs respectively
+% expressions. They have the same syntax:
+% \cmd{\comp}\marg{command}\marg{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 \cmd{\comp} or
+% \cmd{\eval}, respectively. As an example a denotational rule for a
+% sequencing 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 evaluation symbol in itself. This is done by
+% \cmd{\compsymbol} or \cmd{\evalsymbol}, respectively. 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 \cmd{\exe}, which has the syntax
+% \cmd{\exe}\marg{program}\oarg{machine}\marg{data}. The third Futumara projection
+% $\mathtt{cogen} = \exe{spec}{spec.spec}$ can be written
+% "$\mathtt{cogen} = \exe{spec}{spec.spec}$". As an alternative, you
+% can also give the machine \texttt{L} explicit:
+% \begin{code}
+% "$\mathtt{cogen} = \exe{spec}[L]{spec.spec}$"
+% \end{code}
+% This will result in:
+% $\mathtt{cogen} = \exe{spec}[L]{spec.spec}$
+%
+% \section{Some Notes about the Files}
+%
+% \semantic\ is distributed in two files, "semantic.dtx" and
+% "semantic.ins". Of these two files, "semantic.dtx" is the most
+% important, as it contains all the essentials---users guide, code and
+% documentation of the code. "semantic.ins" is used only to guide
+% \package{docstrip} in generating "semantic.sty" from "semantic.dtx".
+%
+% {\makeatletter To get \@bblb\ and \@bbrb, used in \cmd{\comp}, \cmd{\eval} and \cmd{\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 two sharps. However, we recommend
+% that you get \package{bbold} from your nearest CTAN-archive.
+% \makeatother}
+%
+% In addition to the users guide, you can also get the fully documented code.
+% You need this, however, if you want to see how the macros are implemented
+% the macros or if you want to change some part of the package. You should
+% start by editing "semantic.dtx" and remove the percentage signs from the
+% four lines starting at Line~\ref{lin:AlsoImplementation}
+% \begin{verbatim}
+% % \AlsoImplementation
+% % \EnableCrossrefs
+% % \CodelineIndex
+% % \RecordChanges
+% \end{verbatim}
+% After saving the changes, 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}
+% After another run of \LaTeX, then the documentation is ready for printing.
+%
+% \medskip
+% \parmark[\copyright]^^A
+% At last the boring formal stuff: The package is protected by the The
+% \LaTeX\ Project Public License (lppl). You are encouraged to copy, use, delete
+% etc.\ the package ("semantic.dtx" and "semantic.ins") as much as
+% your heart, but if you modify the code (even locally), you should
+% change the name to avoid confusion. Under all circumstances, the
+% package is still: {\small \copyright 1995--2000 Peter Møller Neergaard
+% and Arne John Glenstrup.}
+%
+% \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 Add a grammar option if needed.
+% \item If at all possible, add a check for the existence of "manfnt.tfm".
+% \item Use \cmd{\hrule} and \cmd{\vrule} instead of \cmd{\line} (cf.\ \package{Epic}) as
+% much as possible to build the translation diagrams , since this will
+% improve performance.
+% \item Develop example macros that set an example and give the source text
+% for the example.
+% \item Analyze my use of registers to see if I can reduce the
+% number of permanently reserved registers.
+% \end{columnItemize}
+%
+% \ifmulticols
+% \end{multicols}
+% \fi
+%
+% \subsection{Stub for Users Guide and Documentation}
+%
+% First comes a little hack that makes \LaTeX\ think it is loading the
+% package \texttt{semantic.sty}. In this way, the commands in the package can
+% be for printing the documentation:
+% \begin{macrocode}
+%<*documentation>
+\makeatletter \def\@currname{semantic} \def\@currext{sty}
+%</documentation>
+% \end{macrocode}
+% \cmd{\@currname} and \cmd{\@currext} are internal \LaTeX-macros containg the name
+% and extension of the package currently being loaded. The code is
+% encapsulated in "<*documentation>"\lttdots"</documentation>". Thus it is
+% not included in the style file, when the package is installed.
+%
+% \changes{2.0}{1995/05/24}{Added code for loader of different package options}
+%
+% \subsection{Package Identification and Option Loading}
+%
+% The package code starts by identifying the file as a \LaTeXe\ package:
+% \begin{macrocode}
+%<*general>
+\NeedsTeXFormat{LaTeX2e}
+% \end{macrocode}
+% \begin{macro}{\semanticVersion}
+% \begin{macro}{\semanticDate}
+% Constants definining the package release.
+% \begin{macrocode}
+\newcommand{\semanticVersion}{2.0(epsilon)}
+\newcommand{\semanticDate}{2003/10/28}
+% \end{macrocode}
+% \changes{2.0$\delta$}{2002/07/11}{Added.}
+% \end{macro}^^A \semanticDate
+% \changes{2.0$\delta$}{2002/07/11}{Added.}
+% \end{macro}^^A \semanticVersion
+% \begin{macrocode}
+\ProvidesPackage{semantic}
+ [\semanticDate\space v\semanticVersion\space]
+\typeout{Semantic Package v\semanticVersion\space [\semanticDate]}
+\typeout{CVSId: $Id: semantic.dtx,v 1.11 2003/10/28 13:45:57 turtle Exp $}
+%</general>
+% \end{macrocode}
+% \changes{2.0$\delta$}{2002/07/11}{Using \cs{typeout} to print (now) extended information to user.}
+%
+% \subsubsection{Avoid Naming Conflicts}
+%
+% The following code is used to test that all names used by the
+% \semantic-package are not used by other packages.
+%
+% \begin{macro}{\@semanticNotDefinable}
+% \changes{2.0$\alpha$}{1996/05/18}{Added redefinition of
+% \cs{@notdefinable} during package loading}
+% This replaces the internal \LaTeX\ command \cmd{\@notdefinable}, which is
+% used to issue an error message when a command cannot be defined, during
+% loading of \semantic. The name of the command that could not be defined
+% is saved by \LaTeX\ in \cmd{\reserved@a}.
+% \begin{macrocode}
+%<*general>
+\newcounter{@@conflict}
+\newcommand{\@semanticNotDefinable}{%
+ \typeout{Command \@backslashchar\reserved@a\space already defined}
+ \stepcounter{@@conflict}}
+\newcommand{\@oldNotDefinable}{}
+\let\@oldNotDefinable=\@notdefinable
+\let\@notdefinable=\@semanticNotDefinable
+% \end{macrocode}
+% The macro types the name of the confliction macro to the user and then
+% marks that there has been a conflict by increasing the numbers of
+% conflicts encountered. \cmd{\@notdefinable} is an internal \LaTeX\
+% command used to write an error message when a command cannot be
+% defined. It is temporarily saved for later restoring.
+% \end{macro}
+%
+% \begin{macro}{\TestForConflict}
+% \changes{2.0$\alpha$}{1996/05/18}{Added macro for testing for conlict
+% instead of using \cs{newcommand}}
+% \cmd{\@testconflict} takes a list of macros (separated by comma) and testes
+% that they are all undefined. If one of them is not undefined an error
+% message will be issued. The syntax is choosen like \cmd{\DoNotIndex} from
+% \package{ltxdoc}.
+% \begin{macrocode}
+\newcommand{\TestForConflict}{}
+\def\TestForConflict#1{\sem@test #1,,}
+% \end{macrocode}
+% The macro initialises the testing and then uses \cmd{\@test} to test the
+% indiviual commands in the list.
+% \end{macro}
+%
+% \begin{macro}{\sem@test}
+% This is the command for doing the test of a single macro
+% \begin{macrocode}
+\newcommand{\sem@test}{}
+\newcommand{\sem@tmp}{}
+\newcommand{\@@next}{}
+\def\sem@test#1,{%
+ \def\sem@tmp{#1}%
+ \ifx \sem@tmp\empty \let\@@next=\relax \else
+ \@ifdefinable{#1}{} \let\@@next=\sem@test \fi
+ \@@next}
+%</general>
+% \end{macrocode}
+% The macro takes a single argument. If its not empty, \ie\ the list has
+% not been read to the end, the internal \LaTeX\ command \cmd{\@ifdefinable}
+% is used to test if the command can be defined (\see\
+% \cite[p.~192]{LaTeXbook}).
+%
+% To avoid to many unclosed "\if" the macro is made tail recursive by
+% saving the next macro in \cmd{\@@next}.
+% \changes{2.0$\delta$}{2002/06/19}{Renamed \cs{@temp} \cs{sem@tmp}.}
+% \end{macro}
+%
+% \subsubsection{Hack for the documentation}
+%
+% The following is a hack inserted to make the processing of the
+% documentation, skip all the options loading and just incorporate the
+% package code.
+% \begin{macrocode}
+%<*documentation>
+\iftrue\iffalse
+%</documentation>
+% \end{macrocode}
+% The "\iftrue" matches the "\fi" in the bottom of the code, while the
+% "\iffalse" is skipping the code controlling loading of the options.
+%
+% \subsubsection{Loading of Options}
+%
+% The code to load the different options is defined. By ``erasing'' the
+% definitions after loading the parts, the code ensures that no part is
+% loaded more than once.
+% \begin{macrocode}
+%<*general>
+\TestForConflict{\@inputLigature,\@inputInference,\@inputTdiagram}
+\TestForConflict{\@inputReservedWords,\@inputShorthand}
+\TestForConflict{\@ddInput,\sem@nticsLoader,\lo@d}
+\def\@inputLigature{\input{ligature.sty}\message{ math mode ligatures,}%
+ \let\@inputLigature\relax}
+\def\@inputInference{\input{infernce.sty}\message{ inference rules,}%
+ \let\@inputInference\relax}
+\def\@inputTdiagram{\input{tdiagram.sty}\message{ T diagrams,}%
+ \let\@inputTdiagram\relax}
+\def\@inputReservedWords{\input{reserved.sty}\message{ reserved words,}%
+ \let\@inputReservedWords\relax}
+\def\@inputShorthand{\input{shrthand.sty}\message{ short hands,}%
+ \let\@inputShorthand\relax}
+% \end{macrocode}
+% Token register~1 is used for keeping the commands to load the package.
+% An empty register will mark that all options should be loaded:
+% \begin{macrocode}
+\toks1={}
+% \end{macrocode}
+% \begin{macro}{\@ddInput}
+% \cmd{\@ddInput} adds its argument to the list of commands used for loading:
+% \begin{macrocode}
+\newcommand{\@ddInput}[1]{%
+ \toks1=\expandafter{\the\toks1\noexpand#1}}
+% \end{macrocode}
+% The \cmd{\expandafter} makes \cmd{\the} expand the tokens register~0 one level,
+% thus listing all the loading instructions.
+% \end{macro}
+%
+% Each option add the code to load the option to token register~0.
+% \begin{macrocode}
+\DeclareOption{ligature}{\@ddInput\@inputLigature}
+\DeclareOption{inference}{\@ddInput\@inputInference}
+\DeclareOption{tdiagram}{\@ddInput\@inputTdiagram}
+\DeclareOption{reserved}{\@ddInput\@inputReservedWords}
+\DeclareOption{shorthand}{\@ddInput\@inputLigature
+ \@ddInput\@inputShorthand}
+% \end{macrocode}
+%
+% The options are processed
+% \begin{macrocode}
+\ProcessOptions*
+% \end{macrocode}
+%
+% and the specified options are loaded (if no options are specifieed, then
+% all options are loaded)
+% \begin{macrocode}
+\typeout{Loading features: }
+\def\sem@nticsLoader{}
+\edef\lo@d{\the\toks1}
+\ifx\lo@d\empty
+ \@inputLigature
+ \@inputInference
+ \@inputTdiagram
+ \@inputReservedWords
+ \@inputShorthand
+\else
+ \lo@d
+\fi
+\typeout{and general definitions.^^J}
+% \end{macrocode}
+% \cmd{\sem@nticsLoader} is flag used for testing in the options file to check
+% that the files are loaeded from the package.
+%
+% After loading the options the name space is cleaned up.
+% \begin{macrocode}
+\let\@ddInput\relax
+\let\@inputInference\relax
+\let\@inputLigature\relax
+\let\@inputTdiagram\relax
+\let\@inputReservedWords\relax
+\let\@inputShorthand\relax
+\let\sem@nticsLoader\realx
+\let\lo@d\relax
+%</general>
+% \end{macrocode}
+%
+% \subsubsection{Options' Test that They Are Loaded by \semantic}
+%
+% \label{page:testForSemanticsLoader}
+% The following does a test in all the options files to see whether they are
+% loaded from the \semantic\ package. If not, no commands are defined. See
+% also the bottom of the code part, where the mathcing "\fi" is provided.
+% \begin{macrocode}
+%<*allOptions>
+\expandafter\ifx\csname sem@nticsLoader\endcsname\relax
+% \end{macrocode}
+% A feature of \cmd{\csname}\meta{name}\cmd{\endcsname} is that the command
+% sequence would be taken to be \cmd{\relax} if \cs{\meta{name}} is not
+% defined.
+% \begin{macrocode}
+ \PackageError{semantic}{%
+ This file should not be loaded directly}
+ {%
+ This file is an option of the semantic package. It should not be
+ loaded directly\MessageBreak
+ but by using \protect\usepackage{semantic} in your document
+ preamble.\MessageBreak
+ No commands are defined.\MessageBreak
+ Type <return> to proceed.
+ }%
+\else
+%</allOptions>
+% \end{macrocode}
+% This is the end of the part, which should not be processed when processing
+% the documentation
+% \begin{macrocode}
+%<*documentation>
+\fi\fi
+%</documentation>
+% \end{macrocode}
+%
+% \subsubsection{Auxiliary Macros}
+%
+% \begin{macrocode}
+%<*general>
+\TestForConflict{\@dropnext,\@ifnext,\@ifn,\@ifNextMacro,\@ifnMacro}
+\TestForConflict{\@@maxwidth,\@@pLineBox,\if@@Nested,\@@cBox}
+\TestForConflict{\if@@moreLines,\@@pBox}
+% \end{macrocode}
+%
+% \begin{macro}{\@ifnext}
+% This macro compares the next token with a given token (\#1), and if they
+% are identical,
+% the first choice (\#2) is expanded, else the second choice(\#3).
+% This is a loan of \cmd{\@ifnextchar} from the \LaTeXe-base and it therefore
+% uses the interal variables \cmd{\reserved@a}\lttdots\cmd{\reserved@d}. The only
+% change from \cmd{\@ifnextchar} is that spaces are not ignoree. This is
+% appropriate for defining
+% the ligatures (eg.\ I do not want \verb*"- >" to be converted to
+% $\rightarrow$).
+% \begin{macrocode}
+\def\@ifnext#1#2#3{%
+ \let\reserved@e=#1\def\reserved@a{#2}\def\reserved@b{#3}\futurelet%
+ \reserved@c\@ifn}
+\def\@ifn{%
+ \ifx \reserved@c \reserved@e\let\reserved@d\reserved@a\else%
+ \let\reserved@d\reserved@b\fi \reserved@d}
+% \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\@ifNextMacro}
+% This macro examines the next token, and if it is a macro, the first
+% option (\#1) is executed, else the second option (\#2). Like
+% \cmd{\@ifnext}, the code is mainly ``borrowed'' from the \LaTeX-source.
+% \begin{macrocode}
+\def\@ifNextMacro#1#2{%
+ \def\reserved@a{#1}\def\reserved@b{#2}%
+ \futurelet\reserved@c\@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 of whether it is a macro, is done in \cmd{\@ifnMacro} by comparing the
+% catcodes of the token and a macro, \cmd{\@ifnMacro} (any other
+% macro could have been used as well). The \cmd{\noexpand} secures that I compare
+% the token and not its expansion. If \emph{eg} \cmd{\@noexpand} were left out and
+% the token were a macro, then it would be expanded and the first token in
+% the macro be compared to the first token in \cmd{\@ifnMacro}.
+% \end{macro}
+%
+% \begin{macro}{\@dropnext}
+% This macro processes the next token and ignores its successor
+% (it is not processed at all).
+% \begin{macrocode}
+\newcommand{\@dropnext}[2]{#1}
+%</general>
+% \end{macrocode}
+% \end{macro}
+%
+% \subsubsection{Testing for Name Conflict During Loading}
+%
+% At the end of the loading it is tested if an error has occurred. In that
+% case an error message is issued. Then the testing commands is disabled.
+%
+% \medskip\noindent But first yet another documentation hack$\ldots$
+% \begin{macrocode}
+%<*documentation>
+\iffalse
+%</documentation>
+%<*general>
+\ifnum \value{@@conflict} > 0
+ \PackageError{Semantic}
+ {The \the@@conflict\space command(s) listed above have been
+ redefined.\MessageBreak
+ Please report this to turtle@bu.edu}
+ {Some of the commands defined in semantic was already defined %
+ and has\MessageBreak now be redefined. There is a risk that %
+ these commands will be used\MessageBreak by other packages %
+ leading to spurious errors.\MessageBreak
+ \space\space Type <return> and cross your fingers%
+}\fi
+\let\@notdefinable=\@oldNotDefinable
+\let\@semanticNotDefinable=\relax
+\let\@oldNotDefinable=\relax
+\let\TestForConflict=\relax
+\let\@endmark=\relax
+\let\sem@test=\relax
+%</general>
+% \end{macrocode}
+%
+% \medskip\noindent The end of yet another documentation hack
+% \begin{macrocode}
+%<*documentation>
+\fi
+%</documentation>
+% \end{macrocode}
+%
+% \subsection{Math Ligatures}
+%
+% \begin{macrocode}
+%<*ligature>
+\TestForConflict{\@addligto,\@addligtofollowlist,\@def@ligstep}
+\TestForConflict{\@@trymathlig,\@defactive,\@defligstep}
+\TestForConflict{\@definemathlig,\@domathligfirsts,\@domathligfollows}
+\TestForConflict{\@exitmathlig,\@firstmathligs,\@ifactive,\@ifcharacter}
+\TestForConflict{\@ifinlist,\@lastvalidmathlig,\@mathliglink}
+\TestForConflict{\@mathligredefactive,\@mathligsoff,\@mathligson}
+\TestForConflict{\@seentoks,\@setupfirstligchar,\@try@mathlig}
+\TestForConflict{\@trymathlig,\if@mathligon,\mathlig,\mathligprotect}
+\TestForConflict{\mathligsoff,\mathligson,\@startmathlig,\@pushedtoks}
+% \end{macrocode}
+%
+% \subsubsection{User Interface}
+% \label{sec:UserInterface}
+%
+% \begin{macro}{\if@mathligon}
+% First we define a new "\if" flag that indicates whether the user has
+% requested math ligatures to be active or not:
+% \begin{macrocode}
+\newif\if@mathligon
+% \end{macrocode}
+% \end{macro}
+% \begin{macro}{\mathlig}
+% Now, for the definition of \cmd{\mathlig}\marg{character
+% sequence}\marg{ligature commands}, we first add the ligature
+% character sequence $c_1c_2\cdots c_n$ to the internal ligature
+% character lists, and then
+% we set up the macros "\@mathlig"$c_1c_2\cdots$ by calling
+% \cmd{\@defligstep}:
+% \begin{macrocode}
+\DeclareRobustCommand\mathlig[1]{\@addligtolists#1\@@
+ \if@mathligon\mathligson\fi
+ \@setupfirstligchar#1\@@
+ \@defligstep{}#1\@@}
+% \end{macrocode}
+% \changes{2.0$\beta$}{2000/08/02}{Corrected typo in \cs{mathligson}.}
+% \end{macro}
+% \DescribeMacro{\@mathligson}\DescribeMacro{\@mathligsoff}
+% We define macros \cmd{\@mathligson} and \cmd{\@mathligsoff} for turning math
+% ligatures on and off internally without changing the status of the
+% "\if@mathligon" flag:
+% \begin{macrocode}
+\def\@mathligson{\if@mathligon\mathligson\fi}
+\def\@mathligsoff{\if@mathligon\mathligsoff\@mathligontrue\fi}
+% \end{macrocode}
+% \begin{macro}{\mathligprotect}
+% \cmd{\mathligprotect}\marg{command} defines \meta{command} to be a macro
+% expanding into \cmd{\@mathligsoff}\emph{expansion
+% of}\meta{command}\cmd{\@mathligson}:
+% \begin{macrocode}
+\DeclareRobustCommand\mathligprotect[1]{\expandafter
+ \def\expandafter#1\expandafter{%
+ \expandafter\@mathligsoff#1\@mathligson}}
+% \end{macrocode}
+% \end{macro}
+% \begin{macro}{\mathligson}
+% \cmd{\mathligson} changes the math code of all the characters that can occur
+% as the first character of a ligature character sequence to be active, and
+% sets the "\if@mathligon" flag:
+% \begin{macrocode}
+\DeclareRobustCommand\mathligson{\def\do##1##2##3{\mathcode`##1="8000}%
+ \@domathligfirsts\@mathligontrue}
+% \end{macrocode}
+% and turn on math ligatures automatically.
+% \begin{macrocode}
+\AtBeginDocument{\mathligson}
+% \end{macrocode}
+% \changes{2.0$\beta$}{2000/08/02}{Ligature turned on when ligatures are loaded (moved from \texttt{shorthand} option).}
+% \end{macro}
+% \begin{macro}{\mathligsoff}
+% \cmd{\mathligsoff} does the reverse actions: resetting math codes to their
+% values as recorded at ligature definition time (stored in the
+% \cmd{\@domathligfirsts} data structure).
+% \begin{macrocode}
+\DeclareRobustCommand\mathligsoff{\def\do##1##2##3{\mathcode`##1=##2}%
+ \@domathligfirsts\@mathligonfalse}
+% \end{macrocode}
+% \end{macro}
+%
+% \subsubsection{Utilities}
+% \label{sec:Utilities}
+%
+% \DescribeMacro{\@mathliglink} \cmd{\@mathliglink} is a dummy macro that
+% should never be expanded, so we issue an error if it is:
+% \begin{macrocode}
+\edef\@mathliglink{Error: \noexpand\verb|\string\@mathliglink| expanded}
+% \end{macrocode}
+% \DescribeMacro{\@ifcharacter}\DescribeMacro{\@ifactive}
+% \cmd{\@ifcharacter}\meta{character}\marg{truebranch}\marg{falsebranch}
+% is used to test whether \meta{character} is in fact a character and chooses the
+% appropriate branch. \cmd{\@ifactive} is analogous.
+% \begin{macrocode}
+{\catcode`\A=11\catcode`\1=12\catcode`\~=13 % Letter, Other and Active
+\gdef\@ifcharacter#1{\ifcat A\noexpand#1\let\next\@firstoftwo
+ \else\ifcat 1\noexpand#1\let\next\@firstoftwo
+ \else\ifcat \noexpand~\noexpand#1\let\next\@firstoftwo
+ \else\let\next\@secondoftwo\fi\fi\fi\next}%
+\gdef\@ifactive#1{\ifcat \noexpand~\noexpand#1\let\next\@firstoftwo
+ \else\let\next\@secondoftwo\fi\next}}
+% \end{macrocode}
+%
+% \subsubsection{Data Structures}
+% \label{sec:DataStructures}
+%
+% For each math ligature character sequence $c_1c_2\cdots c_n$ the macros
+% "\@mathlig"$c_1$, "\@mathlig"$c_1c_2$, \ldots, "\@mathlig"$c_1c_2\cdots
+% c_n$ are defined, and "\@mathlig"$c_1c_2\cdots c_n$ expands to the
+% commands that typeset the ligature. For $1<i<n$, if $c_1c_2\cdots c_i$ is
+% not also a ligature character sequence, it is defined as the (dummy)
+% macro \cmd{\@mathliglink}\DescribeMacro{\@mathliglink}.
+%
+% E.g.: if `"-><-"' has been defined to typeset as
+% "\rightarrow\leftarrow" and `"-->"' has been defined to typeset as
+% \cmd{\longrightarrow}, the following macros will be defined:
+% \begin{center}
+% \begin{tabular}{ll}
+% \textbf{Macro} & \textbf{is defined as} \\
+% "\@mathlig-" & "-" \\
+% "\@mathlig--" & \cmd{\@mathliglink} \\
+% "\@mathlig-->" & \cmd{\longrightarrow} \\
+% "\@mathlig->" & \cmd{\@mathliglink} \\
+% "\@mathlig-><" & \cmd{\@mathliglink} \\
+% "\@mathlig-><-" & "\rightarrow\leftarrow" \\
+% \end{tabular}
+% \end{center}
+% As it can be seen, "\@mathlig"$c$ expands to $c$, so that the original
+% meaning of a single character $c$ can be used.
+%
+% The macro \cmd{\@domathligfirsts}\DescribeMacro{\@domathligfirsts} holds a
+% list of characters, which occur as a
+% first character in a ligature character sequence, with their
+% "mathcode"s and "catcode"s as defined when the ligature is defined. E.g.:
+% if ligatures have been defined for `"-><-"' and `"<--"', then
+% \cmd{\@domathligfirsts} will expand into a token sequence containing the
+% sequence
+% \begin{center}
+% "\do \-{8704}{12}\do \<{12604}{12}"
+% \end{center}
+% Thus, defining command "\do#1#2#3{"\emph{manipulate character}"#1}" and
+% executing \cmd{\@domathligfirsts} manipulates all the first characters of
+% ligature character sequences.
+%
+% The macro \cmd{\@domathligfollows}\DescribeMacro{\@domathligfollows} is
+% analogous for characters that occur after the first character in a
+% ligature character sequence. \cmd{\@makemathligsactive} and
+% \cmd{\@makemathligsnormal} change the catcodes of these characters.
+% \begin{macrocode}
+\def\@domathligfollows{}\def\@domathligfirsts{}
+\def\@makemathligsactive{\mathligson
+ \def\do##1##2##3{\catcode`##1=12}\@domathligfollows}
+\def\@makemathligsnormal{\mathligsoff
+ \def\do##1##2##3{\catcode`##1=##3}\@domathligfollows}
+% \end{macrocode}
+% \begin{macro}{\@ifinlist}
+% \cmd{\@ifinlist}\marg{character/mathcode/catcode list}\discretionary{}{}{}^^A
+% \marg{character}\discretionary{}{}{}^^A
+% \marg{true\-branch}\discretionary{}{}{}^^A
+% \marg{false\-branch}
+% checks whether \meta{character} is in \meta{character/mathcode/catcode
+% list} and chooses the appropriate branch.
+% \begin{macrocode}
+\def\@ifinlist#1#2{\@tempswafalse
+ \def\do##1##2##3{\ifnum`##1=`#2\relax\@tempswatrue\fi}#1%
+ \if@tempswa\let\next\@firstoftwo\else\let\next\@secondoftwo\fi\next}
+% \end{macrocode}
+% \end{macro}
+%
+% \subsubsection{Setting up the Data Structures}
+% \label{sec:SettingUpTheDataStructures}
+%
+% \begin{macro}{\@addligto}
+% \cmd{\@addligto}\marg{character/mathcode/catcode
+% list}\marg{character} inserts (replaces) or adds the "mathcode"
+% and "catcode" information into the \meta{character/mathcode/catcode
+% list}:
+% \begin{macrocode}
+\def\@addligto#1#2{%
+ \@ifinlist#1#2{\def\do##1##2##3{\noexpand\do\noexpand##1%
+ \ifnum`##1=`#2 {\the\mathcode`#2}{\the\catcode`#2}%
+ \else{##2}{##3}\fi}%
+ \edef#1{#1}}%
+ {\def\do##1##2##3{\noexpand\do\noexpand##1%
+ \ifnum`##1=`#2 {\the\mathcode`#2}{\the\catcode`#2}%
+ \else{##2}{##3}\fi}%
+ \edef#1{#1\do#2{\the\mathcode`#2}{\the\catcode`#2}}}}
+% \end{macrocode}
+% \end{macro}
+% \begin{macro}{\@addligtolists}
+% \begin{macro}{\@addligtofollowlist}
+% \errorcontextlines=10
+% \cmd{\@addligtolists}\marg{$c_1c_2\cdots{}c_n$} adds $c_1$ to the
+% \cmd{\@domathligfirsts} list and the remaining to the \cmd{\@domathligfollows}
+% list by only eating the first character and passing the remaining to
+% \cmd{\@addligtofollowlist}:
+% \begin{macrocode}
+\def\@addligtolists#1{\expandafter\@addligto
+ \expandafter\@domathligfirsts
+ \csname\string#1\endcsname\@addligtofollowlist}
+\def\@addligtofollowlist#1{\ifx#1\@@\let\next\relax\else
+ \def\next{\expandafter\@addligto
+ \expandafter\@domathligfollows
+ \csname\string#1\endcsname
+ \@addligtofollowlist}\fi\next}
+% \end{macrocode}
+% \end{macro}
+% \end{macro}
+% \begin{macro}{\@defligstep}
+% \begin{macro}{\@def@ligstep}
+% \cmd{\@defligstep}\marg{$c_1\cdots{}c_{i-1}$}\marg{$c_i$} defines one
+% step in the parsing of a ligature character sequence: the
+% "\@mathlig"$c_1\cdots c_i$ macro. The (possibly active) characters are
+% turned into letters by applying \cmd{\string} until the end of the sequence
+% is reached:
+% \begin{macrocode}
+\def\@defligstep#1#2{\def\@tempa##1{\ifx##1\endcsname
+ \expandafter\endcsname\else
+ \string##1\expandafter\@tempa\fi}%
+ \expandafter\@def@ligstep\csname @mathlig\@tempa#1#2\endcsname{#1#2}}
+% \end{macrocode}
+% when the end of ALL the characters of the sequence (i.e.{} $c_1c_2\cdots
+% c_n$) is reached---signalled by the \cmd{\@@} control
+% sequence inserted by \cmd{\mathlig}---\cmd{\@def@ligstep} can define the macro
+% "\@mathlig"$c_1c_2\cdots
+% c_n$ (note that the following tokens in the input stream are the ones
+% following the first parameter of a \cmd{\mathlig} command). Otherwise, the
+% process is repeated by calling \cmd{\@defligstep} again.
+% \begin{macrocode}
+\def\@def@ligstep#1#2#3{%
+ \ifx#3\@@
+ \def\next{\def#1}%
+ \else
+ \ifx#1\relax
+ \def\next{\let#1\@mathliglink\@defligstep{#2}#3}%
+ \else
+ \def\next{\@defligstep{#2}#3}%
+ \fi
+ \fi\next}
+% \end{macrocode}
+% \end{macro}
+% \end{macro}
+% \begin{macro}{\@setupfirstligchar}
+% The first character, $c$, of a ligature sequence must receive special
+% treatment: if it is already active, we must redefine it to check whether
+% it is used inside or outside of math. When inside, it should expand to
+% \cmd{\@startmathlig}$c$\SpecialUsageIndex{\@startmathlig}.
+% \begin{macrocode}
+\def\@setupfirstligchar#1#2\@@{%
+ \@ifactive{#1}{%
+ \expandafter\expandafter\expandafter\@mathligredefactive
+ \expandafter\string\expandafter#1\expandafter{#1}{#1}}%
+% \end{macrocode}
+% If on the other hand it is not active, we must define \emph{its active
+% variant} to expand to \cmd{\@startmathlig}$c$. This cannot be done directly,
+% as we cannot change the "catcode"s of characters once they've been read,
+% so we call \cmd{\@defactive}:
+% \begin{macrocode}
+ {\@defactive#1{\@startmathlig #1}\@namedef{@mathlig#1}{#1}}}
+% \end{macrocode}
+% \end{macro}
+% \begin{macro}{\@mathligredefactive}
+% The use of \cmd{\@mathligredefactive} is tricky: the macro needs three
+% versions of the character to be defined: an active (for defining), a
+% letter (for \cmd{\@namedef}ining) and an expanded version (for wrapping the
+% math mode check stuff around). thus it must be called by
+% \cmd{\@mathligredefactive}\marg{letter}\marg{expansion}\marg{active
+% character}.
+% \begin{macrocode}
+\def\@mathligredefactive#1#2#3{%
+ \def#3{{}\ifmmode\def\next{\@startmathlig#1}\else
+ \def\next{#2}\fi\next}%
+ \@namedef{@mathlig#1}{#2}}
+% \end{macrocode}
+% \end{macro}
+% \begin{macro}{\@defactive}
+% \begin{macro}{\@definemathlig}
+% The only way we can get an active version of a character $c$ is by
+% storing a list of possible characters, each with catcode 13
+% (active). Actually, what we do is to have a list of macros,
+% \cmd{\@definemathlig}$c$\marg{expansion text} that will define the
+% active character $c$ to expand to \meta{expansion text}.
+% \begin{macrocode}
+\def\@defactive#1{\@ifundefined{@definemathlig\string#1}%
+ {\@latex@error{Illegal first character in math ligature}
+ {You can only use \@firstmathligs\space as the first^^J
+ character of a math ligature}}%
+ {\csname @definemathlig\string#1\endcsname}}
+
+{\def\@firstmathligs{}\def\do#1{\catcode`#1=\active
+ \expandafter\gdef\expandafter\@firstmathligs
+ \expandafter{\@firstmathligs\space\string#1}\next}
+ \def\next#1{\expandafter\gdef\csname
+ @definemathlig\string#1\endcsname{\def#1}}
+% \end{macrocode}
+% Well, this is the list of characters I found it reasonable to expect as
+% first characters of a ligature sequence. Characters like "$" "&" "^" "_"
+% "#" "\" and "%" don't really make sense. All these characters are put
+% into a comma separated list,
+% \cmd{\@firstmathligs}\DescribeMacro{\@firstmathligs}.
+% \begin{macrocode}
+ \do{"}"\do{@}@\do{/}/\do{(}(\do{)})\do{[}[\do{]}]\do{=}=
+ \do{?}?\do{!}!\do{`}`\do{'}'\do{|}|\do{~}~\do{<}<\do{>}>
+ \do{+}+\do{-}-\do{*}*\do{.}.\do{,},\do{:}:\do{;};}
+% \end{macrocode}
+% \end{macro}
+% \end{macro}
+%
+% \subsubsection{Parser Algorithm}
+% \label{sec:ParserAlgorithm}
+%
+% During parsing,
+% \begin{itemize}
+% \item \DescribeMacro{\@seentoks}\cmd{\@seentoks} holds the characters seen
+% so far.
+% \item \DescribeMacro{\@lastvalidmathlig}\cmd{\@lastvalidmathlig} holds the
+% macro corresponding to the longest
+% valid math ligature character sequence seen so far
+% \item \DescribeMacro{\@pushedtoks}\cmd{\@pushedtoks} holds the remaining
+% characters seen that are not a
+% part of the valid ligature character sequence
+% \end{itemize}
+% \begin{macrocode}
+\newtoks\@pushedtoks
+\newtoks\@seentoks
+% \end{macrocode}
+%
+% The overall algorithm is as follows:
+%
+% \begin{itemize}
+% \item [1] Let $i=1$. A character $c_i$ in \cmd{\@domathligfirsts} triggers
+% the following steps:
+% \item [2]
+% \begin{tabbing}
+% \cmd{\@seentoks} := [ ] \\
+% \cmd{\@lastvalidmathlig} := \{\} \\
+% \cmd{\@pushedtoks} := [ ]
+% \end{tabbing}
+% \item [3]
+% \begin{tabbing}\qquad\=\qquad\=\qquad\=\kill
+% if the macro \cmd{\@mathlig}$c_1c_2\cdots c_i$ is defined then \\
+% \>if \cmd{\@mathlig}$c_1c_2\cdots c_i$ is a \cmd{\@mathliglink} then \\
+% \>\>\cmd{\@pushedtoks} := \cmd{\@pushedtoks} ++ [$c_i$] \\
+% \>else \\
+% \>\>\cmd{\@lastvalidmathlig} := \cmd{\@mathlig}$c_1c_2\cdots c_i$ \\
+% \>\>\cmd{\@pushedtoks} := [ ] \\
+% \>\cmd{\@seentoks} := \cmd{\@seentoks} ++ [$c_i$] \\
+% else \\
+% \>disable ligatures \\
+% \>expand \cmd{\@lastvalidmathlig} \\
+% \>enable ligatures \\
+% \>put the \cmd{\@pushedtoks} and $c_i$ on the input stream \\
+% \>go to 1
+% \end{tabbing}
+% \item [4] Let $i=i+1$; read next character $c_i$ and go to 3.
+% \end{itemize}
+% \begin{macro}{\@startmathlig}
+% \begin{macro}{\@trymathlig}
+% \begin{macro}{\@@trymathlig}
+% \begin{macro}{\@try@mathlig}
+% \begin{macro}{\@exitmathlig}
+% All this is accomplished by the following macros, starting with
+% \cmd{\@startmathlig}:
+% \begin{macrocode}
+\def\@startmathlig{\def\@lastvalidmathlig{}\@pushedtoks{}%
+ \@seentoks{}\@trymathlig}
+\def\@trymathlig{\futurelet\next\@@trymathlig}
+\def\@@trymathlig{\@ifcharacter\next{\@try@mathlig}{\@exitmathlig{}}}
+\def\@exitmathlig#1{%
+ \expandafter\@makemathligsnormal\@lastvalidmathlig\mathligson
+ \the\@pushedtoks#1}
+\def\@try@mathlig#1{%\typeout{char: #1 catcode: \the\catcode`#1
+%^^A \space pushed:\the\@pushedtoks
+%^^A \space seen:\the\@seentoks
+%^^A \space last\meaning\@lastvalidmathlig}%
+ \@ifundefined{@mathlig\the\@seentoks#1}{\@exitmathlig{#1}}%
+ {\expandafter\ifx
+ \csname @mathlig\the\@seentoks#1\endcsname
+ \@mathliglink
+ \expandafter\@pushedtoks
+ \expandafter=\expandafter{\the\@pushedtoks#1}%
+ \else
+ \expandafter\let\expandafter\@lastvalidmathlig
+ \csname @mathlig\the\@seentoks#1\endcsname
+ \@pushedtoks={}%
+ \fi
+ \expandafter\@seentoks\expandafter=\expandafter%
+ {\the\@seentoks#1}\@makemathligsactive\obeyspaces\@trymathlig}}
+% \end{macrocode}
+% \end{macro}
+% \end{macro}
+% \end{macro}
+% \end{macro}
+% \end{macro}
+%
+% \subsubsection{Compatibility with \texttt{amsmath} package}
+%
+% \begin{macro}{\patch@newmcodes@}
+% The \texttt{amsmath} package by AMS uses some non-alphanumeric
+% characters to produce for instance extended arrows. Consequently
+% the \cmd{\newmcodes@} in \texttt{amsopn.sty} (2.01) fails with an error message if
+% the hyphen character has mathcode \"8000. So we in provide a patch
+% (suggested by Michael John Downes of AMS<).
+% \begin{macrocode}
+\edef\patch@newmcodes@{%
+ \mathcode\number`\'=39
+ \mathcode\number`\*=42
+ \mathcode\number`\.=\string "613A
+ \mathchardef\noexpand\std@minus=\the\mathcode`\-\relax
+ \mathcode\number`\-=45
+ \mathcode\number`\/=47
+ \mathcode\number`\:=\string "603A\relax
+}
+\AtBeginDocument{\let\newmcodes@=\patch@newmcodes@}
+%</ligature>
+% \end{macrocode}
+% \changes{2.0$\epsilon$}{2002/06/13}{Provided patch to make \semantic compatible with \texttt{amsmath} v. 2.01}
+% \end{macro}
+%
+% \subsubsection{ToDo}
+% \label{sec:ToDo}
+%
+% \begin{itemize}
+% \item Make removing of math ligatures possible (tricky!)
+% \item Make it possible to define a single char as a ligature
+% (redefinition)
+% \item Check the use of \cmd{\@makemathligsactive}: is it possible to
+% replace it by \cmd{\mathligson}?
+% \end{itemize}
+%
+% \subsection{Inference Rules}
+%
+% \begin{macrocode}
+%<*inference>
+\TestForConflict{\@@tempa,\@@tempb,\@adjustPremises,\@inference}
+\TestForConflict{\@inferenceBack,\@inferenceFront,\@inferenceOrPremis}
+\TestForConflict{\@premises,\@processInference,\@processPremiseLine}
+\TestForConflict{\@setLengths,\inference,\predicate,\predicatebegin}
+\TestForConflict{\predicateend,\setnamespace,\setpremisesend}
+\TestForConflict{\setpremisesspace,\@makeLength,\@@space}
+\TestForConflict{\@@aLineBox,\if@@shortDivider}
+% \end{macrocode}
+% \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 \cs{@setLengths}}
+% First I define two auxiliary macros to facilitate 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 have to be evaluated before the setting of every rule. As
+% there are only a few lengths, it could been have been simpler and less
+% general, but I found it inspiring to work out a general solution.
+%
+% \cmd{\@makelength}\marg{users name}\marg{internal name}\marg{default
+% value}\marg{stretch} does all the definitions associated with
+% making a new length: defines a new length \cs{@@\meta{internal name}}, makes
+% a command to evaluate it (with the current choice of font)
+% \cs{@set\meta{internal name}} and makes the users command to change the
+% length \cs{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 should be set wider than its natural width.
+%
+% The macro \cmd{\@setLengths} is used to evaluate all the lengths. When a new
+% length is made using \cmd{\@makelength}, the name of its evaluation macro,
+% \cs{@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 \cmd{\@makelength} builds the name of the length in
+% \cmd{\@@tempa} and the macro to evaluate it in \cmd{\@@tempb}---this requires some
+% playing with \cmd{\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 is, in fact, 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
+% \cmd{\@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, \cmd{\baselineskip}, \cmd{\lineskip} and
+% \cmd{\lineskiplimit}, to zero it is necessary to set them in \cmd{\@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 \cs{name\-space}}^^A
+% This is followed by the definition of some auxiliary internal registers:
+% \label{space setting}
+% \begin{macrocode}
+\@makeLength{premisesspace}{pSpace}{1.5em}{plus 1fil}
+\@makeLength{premisesend}{pEnd}{.75em}{plus 0.5fil}
+\@makeLength{namespace}{nSpace}{.5em}{}
+%</inference>
+% \end{macrocode}
+% \end{macro}
+% \end{macro}
+% \end{macro}
+%
+% Then comes some auxiliary internal registers
+% \changes{1.1$\delta$}{1995/12/01}{Introduced \cs{@@space} for use in comparisons}
+% \begin{macrocode}
+%<*general>
+\newdimen\@@maxwidth
+\newbox\@@pLineBox
+\newbox\@@cBox
+\newbox\@@pBox
+\newif\if@@moreLines
+%</general>
+%<*inference>
+\newbox\@@aLineBox
+\newif\if@@shortDivider
+\newcommand{\@@space}{ }
+% \end{macrocode}
+% \begin{tabular}{lp{9.4cm}}
+% \cmd{\@@maxwidth} & The largest width of a premise/ \\
+% \cmd{\@@cBox} & Holds the conclusion when it has been built \\
+% \cmd{\@@pBox} & The premises is built in this register \\
+% \cmd{\@@pLineBox} & Used to build a single line of the premise \\
+% \cmd{\@@aLineBox} & Contains the line to be adjusted \\
+% \cmd{\@@moreLines} & Flag telling if there is more lines of premises to process \\
+% \cmd{\@@moreLines} & Flag telling the divider should only be the length of
+% the conclusion \\
+% \cmd{\@@space} & Macro with a single space---used for comparison.
+% \end{tabular}
+%
+% \begin{macro}{\predicate}
+% \begin{macro}{\predicatebegin}
+% \changes{1.0}{1995/10/18}{Changed the name to avoid conflict with \LaTeX}
+% \changes{2.0}{1998/06/05}{Changed the default setting to "$" such that
+% the premises are set in math mode.}
+% \begin{macro}{\predicateend}
+% \changes{1.0}{1995/10/18}{Changed the name to avoid conflict with \LaTeX}
+% \changes{2.0}{1998/06/05}{Changed the default setting to "$" such that
+% the premises are set in math mode.}
+% \cmd{\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}
+%
+% \subsection{Typesetting Inference Rules}
+%
+% These macros typesets inference rules. The macros are used nested,
+% which means that \TeX{}'s stack is used extensively. In
+% particular, these put a heavy burden on the paramter stack. To
+% circumvent this the macros are splitted such that each macro only
+% parses one argument at a time. Then only the arguments
+% containing the premise are saved. It is still worth considering
+% ways to remove more nesting of macros with arguments, for
+% instance one could probaply test if the following token was a
+% begin group and then redefine the meaning of~"&" and~"\\". The
+% drawback is that it then might be necessary to use active
+% characters.
+%
+% \begin{macro}{\inference}
+% \changes{1.0}{1995/18/10}{Changed some names due to a conflict with \LaTeX's \cs{rule}}
+% \changes{1.01}{1995/11/07}{Inserted a space in front of the name using \cs{name\-space}}
+% \changes{1.1}{1995/11/15}{Removed \cs{@pInference}}
+% \changes{2.0}{1998/05/20}{Added check for starred version}
+% This is the entry macro. It starts the parameter parsig by testing
+% for the starred version; this is stored in the value of
+% "\if@@shortDivider". It starts a group that the full inference
+% with names is saved in.
+% \begin{macrocode}
+\def\inference{%
+ \@@shortDividerfalse
+ \expandafter\hbox\bgroup
+ \@ifstar{\@@shortDividertrue\@inferenceFront}%
+ \@inferenceFront
+}
+% \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\@inferenceFront}
+% This macro testes for an optional argument to the left of the
+% inference.
+% \begin{macrocode}
+\def\@inferenceFront{%
+ \@ifnextchar[%
+ {\@inferenceFrontName}%
+ {\@inferenceMiddle}%
+}
+% \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\@inferenceFrontName}
+% This maacro typesets an optional argument with the apropriate
+% space and then passes control to the typesetting of the inference
+% \begin{macrocode}
+\def\@inferenceFrontName[#1]{%
+ \setbox3=\hbox{\footnotesize #1}%
+ \ifdim \wd3 > \z@
+ \unhbox3%
+ \hskip\@@nSpace
+ \fi
+ \@inferenceMiddle
+}
+% \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\@inferenceMiddle}
+% It typesets the premises in the box~\cmd{\@@pBox}.
+% \begin{macrocode}
+\long\def\@inferenceMiddle#1{%
+ \@setLengths%
+% \end{macrocode}
+% Initialises the length parameters according to the current font
+% size.
+% \begin{macrocode}
+ \setbox\@@pBox=
+ \vbox{%
+ \@premises{#1}%
+ \unvbox\@@pBox
+ }%
+% \end{macrocode}
+% This typesets the premises. It is necessary to have the
+% typesetting in its own group to prevent interferring with a
+% premise being typeset on the outer levels. We therefore typeset
+% the premises inside a group and moves them one level out by
+% \cmd{\unvbox} inside a~\cmd{\vbox}.
+% \begin{macrocode}
+ \@inferenceBack
+}
+% \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\@inferenceBack}
+% This macro typesets the conclusion, sets up the premises on top of
+% the conclusion and tests for an additional argument.
+% \begin{macrocode}
+\long\def\@inferenceBack#1{%
+ \setbox\@@cBox=%
+ \hbox{\hskip\@@pEnd \predicate{\ignorespaces#1}\unskip\hskip\@@pEnd}%
+% \end{macrocode}
+% Typeset the conclusion in its own box. In this way we are able to
+% compare the lengths of the two.
+% \begin{macrocode}
+ \setbox1=\hbox{$ $}%
+% \end{macrocode}
+% We then ensure that we have the right math fonts loaded by changing
+% to math mode.
+% \begin{macrocode}
+ \setbox\@@pBox=\vtop{\unvbox\@@pBox
+ \vskip 4\fontdimen8\textfont3}%
+ \setbox\@@cBox=\vbox{\vskip 4\fontdimen8\textfont3%
+ \box\@@cBox}%
+% \end{macrocode}
+% Add the space corresponding to a fraction bar in a display below
+% the premises and above the conclusion.
+% \begin{macrocode}
+ \if@@shortDivider
+% \end{macrocode}
+% If the user want a short divider, we typeset the premises and the
+% conclusion in a box with the width of the biggest of the two, but
+% ensures that the divider only gets the width of the
+% conclusion. Anyway, this is not really what we want. We should
+% somehow know the length of the previous premise, but I have not
+% worked out the algorithm yet.
+% \begin{macrocode}
+ \ifdim\wd\@@pBox >\wd\@@cBox%
+ \dimen1=\wd\@@pBox%
+ \else%
+ \dimen1=\wd\@@cBox%
+ \fi%
+ \dimen0=\wd\@@cBox%
+ \hbox to \dimen1{%
+ \hss
+ $\frac{\hbox to \dimen0{\hss\box\@@pBox\hss}}%
+ {\box\@@cBox}$%
+ \hss
+ }%
+ \else
+% \end{macrocode}
+% If plain style, we simply typeset the premise on top of the
+% conclusion.
+% \begin{macrocode}
+ $\frac{\box\@@pBox}%
+ {\box\@@cBox}$%
+ \fi
+ \@ifnextchar[%
+ {\@inferenceBackName}%{}%
+ {\egroup}
+}
+% \end{macrocode}
+% We end the typesetting by testing for an optional argument. If
+% this is not provided we simply ends the group started by
+% \cmd{\inference}.
+% \end{macro}
+%
+% \begin{macro}{\@inferenceBackName}
+% Here we typeset an additional argument
+% \begin{macrocode}
+\def\@inferenceBackName[#1]{%
+ \setbox3=\hbox{\footnotesize #1}%
+ \ifdim \wd3 > \z@
+ \hskip\@@nSpace
+ \unhbox3%
+ \fi
+% \end{macrocode}
+% and end the group started by \cmd{\inference}.
+% \begin{macrocode}
+ \egroup
+}
+% \end{macrocode}
+% \end{macro}
+%
+% \subsubsection{Processing of Premises}
+%
+% Then comes the code that processes a list of premises and set them in
+% \cmd{\@@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 belive this to be faster than actually reading
+% one token at a time using \TeX\ primitives.
+%
+% \begin{macro}{\@premises}
+% \changes{1.1}{1995/11/25}{Initially set \cs{@max\-width} equal to the width of the conclusion}
+% \changes{1.1$\gamma$}{1995/11/12}{Changed \cs{@premises} so the
+% premises can extend over several lines}
+% This initialises the processing of the list of premises line by line. A
+% line is recognised in \cmd{\@processPremises}, which does the processing by
+% matching on its terminating "\\". Since there is not a "\\" after the last
+% premise, I insert \verb*"\\ \end" as an end marker after the list of
+% premises. In this way, \cmd{\@processPremises} can assume that every line is
+% followed by "\\", and if this is followed by \cmd{\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---are two narrow premises on one line
+% and a broad one on another line. it would look strange if the distance between
+% the two premises were 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 \cmd{\@@maxwidth} so that \cmd{\@adjustPremises} adjusts
+% all lines to it. By initially setting \cmd{\@@maxwidth} to the width of the
+% conclusion, no line will become 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}
+% This macro adjusts the lines of premises to \cmd{\@@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 \cmd{\@@pBox} in reverse order. They are taken from
+% \cmd{\@@pBox} one by one by emptying (\cmd{\unvbox}) \cmd{\@@pBox}, setting
+% \cmd{\@@aLineBox} to the last box in the vertical list just emptied and putting
+% the rest back in \cmd{\@@pBox}. I do not expect this to be as bas as it sounds,
+% because presumably the \cmd{\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 \cmd{\vbox} so the contents of \cmd{\@@aLineBox} can be
+% added to the list being build simply using "\hbox to "\lttdots\ (doing the
+% adjusting simultaneousnessly). Being inside a \cmd{\vbox} has the additional
+% advantage that \TeX\ is in internal vertical mode so that there
+% is added lineskip automaticly in accordance with \cmd{\baselineskip} etc.\
+% (cf.~\cite[80]{texbook}). As the macro is in no sense recursive, it is no
+% problem changing \cmd{\@aLineBox} globally.
+% \end{macro}
+%
+% \begin{macro}{\@processPremises}\mbox{}^^A
+% \changes{1.1$\beta$}{1995/11/21}{Fixed bug that made an empty premise sometimes contain \cs{pSpace}}
+% \changes{1.1$\beta$}{1995/11/21}{Moved the processing of spaces to \cs{@inferenceOrPremis}}
+% \begin{macrocode}
+\def\@processPremises#1\\#2\end{%
+% \end{macrocode}
+% This pattern splits the list of premises into the first
+% line (\#1---possibly empty) and the following lines
+% (\#2---possibly containing no lines).
+% \begin{macrocode}
+ \setbox\@@pLineBox=\hbox{}%
+ \@processPremiseLine #1&\end%
+ \setbox\@@pLineBox=\hbox{\unhbox\@@pLineBox \unskip}%
+% \end{macrocode}
+% The first line is typesetted in \cmd{\@@pLineBox} and additional space
+% is removed. We use \cmd{\@processPremiseLine} that like
+% \cmd{\@processPremises} gets "&\end" added so that it recognizes the
+% end of line. After the line has been set
+% \begin{macrocode}
+ \ifdim \wd\@@pLineBox > \z@ %
+% \end{macrocode}
+% If the premise is not empty, we add it to \cmd{\@@pBox}, that when finished
+% will contain the lines (in reverse order---cf.~\cmd{\@adjustPremises}), and if
+% necessary \cmd{\@@maxwidth} is increased.
+% \begin{macrocode}
+ \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 %
+% \end{macrocode}
+% If there are more lines we process them.
+% \begin{macrocode}
+ \def\sem@tmp{#2}%
+ \ifx \sem@tmp\empty \else %
+ \@ReturnAfterFi{%
+ \@processPremises #2\end %
+ }%
+% \end{macrocode}
+% \cmd{\@ReturnAfterFi} is a trick due to Heiko Oberdik to ensure that we
+% get a tail recursive macro.
+% \begin{macrocode}
+ \fi%
+}
+% \end{macrocode}
+% \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}
+\def\@processPremiseLine#1&#2\end{%
+% \end{macrocode}
+% This pattern splits the line into the first premise (\#1---possibly
+% empty) and the following premises (\#2---possibly none).
+% \begin{macrocode}
+ \def\sem@tmp{#1}%
+ \ifx \sem@tmp\empty \else%
+ \ifx \sem@tmp\@@space \else%
+ \setbox\@@pLineBox=%
+ \hbox{\unhbox\@@pLineBox%
+ \@inferenceOrPremis #1\inference\end%
+ \hskip\@@pSpace}%
+ \fi%
+ \fi%
+% \end{macrocode}
+% 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), it is typesetted using
+% \cmd{\@inferenceOrPremis}, and an appropriate 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 \cmd{\@processPremises}.
+% \begin{macrocode}
+ \def\sem@tmp{#2}%
+ \ifx \sem@tmp\empty \else%
+ \@ReturnAfterFi{%
+ \@processPremiseLine#2\end%
+ }%
+ \fi%
+}
+% \end{macrocode}
+% If there are any premises in the
+% \emph{following premises} we use \cmd{\@processPremisesLine}
+% tail recursively.
+% \end{macro}
+%
+% \begin{macro}{\@inferenceOrPremis}
+% "@inferenceOrPremis" decides wether there is a nested \cmd{\@inference} in a
+% premise.
+% \begin{macrocode}
+\def\@inferenceOrPremis#1\inference{%
+ \@ifnext \end
+ {\@dropnext{\predicate{\ignorespaces #1}\unskip}}%
+ {\@processInference #1\inference}%
+}
+% \end{macrocode}
+% The calling macro appends the argument with "\inference \end". We
+% then test whether \cmd{\inference} followd by the token~\cmd{\end}. If
+% this is the case, we conclude that premise did not originally
+% contain a nesting (\emph{ie} \cmd{\inference}). In this case,
+% the \cmd{\end}-token is removed and the premise is set using
+% \cmd{\predicate}. Otherwise, \cmd{\inference}
+% \cmd{\end} is removed and the inference rule is set---all this is done by
+% \cmd{\@processInference}.
+% \end{macro}
+%
+% \begin{macro}{\@processInference}
+% Remove \cmd{\inference} \cmd{\end} from the testing for a nested
+% appearance of an inference rule. Typesets the inference and
+% adjust its vertical placement such that the baseline of its
+% conclusion match the baseline of a plain premise.
+% \begin{macrocode}
+\def\@processInference#1\inference\end{%
+ \ignorespaces #1%
+% \end{macrocode}
+% Typesets the inference rule and returns the full inference rule in
+% a box.
+% \begin{macrocode}
+ \setbox3=\lastbox
+ \dimen3=\dp3
+ \advance\dimen3 by -\fontdimen22\textfont2
+ \advance\dimen3 by \fontdimen8\textfont3
+ \expandafter\raise\dimen3\box3%
+% \end{macrocode}
+% We take the previously type setted inference rule and lifts it by
+% its depth modulo the extra depth that it has got from be lowered
+% by a fraction.
+% \begin{macrocode}
+}
+% \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\@ReturnAfterFi}
+% This is a small macro due to Heiko Oberdik. It ensure that we get
+% a tail recursive function even inside an "\if"-construction.
+% \begin{macrocode}
+\long\def\@ReturnAfterFi#1\fi{\fi#1}
+% \end{macrocode}
+% It finds the commands up till the enclosing "\fi", closes the "\if"
+% and executes the commands.
+% \end{macro}
+%
+% \begin{macrocode}
+%</inference>
+% \end{macrocode}
+%
+% \subsubsection{ToDo}
+%
+% \begin{itemize}
+% \item Find a way to made the conclusion bar as wide as the
+% conclusion of the premises (tricky).
+% \item Get it to work correctly with amsmath and mathbbol
+% \end{itemize}
+%
+% \subsection{T-diagrams}
+%
+% \begin{macrocode}
+%<*Tdiagram>
+\TestForConflict{\@getSymbol,\@interpreter,\@parseArg,\@program}
+\TestForConflict{\@putSymbol,\@saveBeforeSymbolMacro,\compiler}
+\TestForConflict{\interpreter,\machine,\program,\@compiler}
+%</Tdiagram>
+% \end{macrocode}
+% First some auxilary registers are reserved:
+% \begin{macrocode}
+%<*general>
+\newif\if@@Nested \@@Nestedfalse
+%</general>
+%<*Tdiagram>
+\newif\if@@Left
+\newif\if@@Up
+\newcount\@@xShift
+\newcount\@@yShift
+\newtoks\@@symbol
+\newtoks\@@tempSymbol
+% \end{macrocode}
+% \begin{tabular}{lp{9.2cm}}
+% \cmd{\@@Nested} & Flag telling if the current diagram is nested within another \\
+% \cmd{\@@Left} & Flag telling that a nested diagram should be drawn to the
+% left---if not set, the nested diagram is drawn to the right \\
+% \cmd{\@@Right} & Flag telling that a nested diagram should be drawn above
+% the current one---if not set, the diagram is drawn below
+% the current one \\
+% \cmd{\@@xShift} & Horizontal shift from the local origin to the starting
+% position in units of \cmd{\unitlength}. \\
+% \cmd{\@@yShift} & Vertical shift from the local origin to the starting
+% position in units of \cmd{\unitlength} \\
+% \cmd{\@@Symbol} & The current machine symbol (i.e.\ the letter designating
+% the programme/machine) \\
+% \cmd{\@@tempSymbol} & Used as temporary storage for different symbols
+% \end{tabular}
+%
+% When \LaTeX's \cmd{\put} command is invoked, it raises a \cmd{\hbox} to
+% the given offset, giving it height zero, and puts a \cmd{\hss} in the end
+% so that it will end up with zero width too. It expands the "picture" command
+% given in "{"\lttdots"}" just before the \cmd{\hss}, so they can be drawn
+% from a local origin (given as coordinates to \cmd{\put}). The
+% diagram commands are adapted to this scheme. Thus they are all constructed
+% according to a common 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
+% \emph{not} nested, the bottom should be centered around the position
+% given by \cmd{\put}. If the diagram is nested, the bottom should
+% be at the current vertical position, if the diagram is to 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 \cmd{\hbox} is shifted to the given offset using \cmd{\hskip} and
+% \cmd{\raise}. Inside the box the frame of the diagram is drawn first.
+% This is done using the \cmd{\put}, \cmd{\line} and other
+% "picture" commands. This relies on the way the
+% "picture" commands are construtced. It is admittely a little
+% bad style to use the commands in a 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, to
+% which the position and orientation (\emph{ie} up and left) of a
+% possible nested diagram, and the coordinates for the symbol in the
+% current diagram are given. The macro will examine the argument, and if it
+% consists of letters, it is considered a language symbol and is
+% set in the appropriate place. If itis a macro, however, the nested diagram
+% will be drawn, returning the language symbol using the global register
+% \cmd{\@@symbol}, which afterwards is set inside the diagram.
+%
+% \item If the diagram is nested, it is finally ensure, that \cmd{\@@symbol}
+% is set globally accordingly to the orientation. Thus it returns
+% the symbol to the ``calling'' diagram.
+% \end{itemize}
+%
+% Most of the translation diagrams are coded with a small stup, that
+% packs the arguments (that are separated by commas) followed by an \cmd{\end},
+% 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 a little code that reports errors if the
+% command is used wrongly, is incorporated.
+% \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 a little code that reports errors if the
+% command is used wrongly, is incorporated.
+% \end{macro}
+%
+% \begin{macro}{\@parseArg}
+% \begin{macro}{\@getSymbol}
+% \begin{macro}{\@doSymbolMacro}
+% \begin{macro}{\@saveBeforeSymbolMacro}
+% These macros parse a single argument. As there is some testing of
+% the following token, it is splitted into four macros, the main one being
+% \cmd{\@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 (\cmd{\@doSymbolMacro}) or some
+% text string ("@\getSymbol"), and then passing the parameters on to the
+% appropriate macro.
+% \begin{macrocode}
+\def\@parseArg(#1)(#2){%
+ \@ifNextMacro{\@doSymbolMacro(#1)(#2)}{\@getSymbol(#2)}}
+% \end{macrocode}
+% \cmd{\@getSymbol} is used when the argument is ``plain'' text. It simply
+% passes the parameters to \cmd{\@putSymbol}, which does the setting up.
+% \begin{macrocode}
+\def\@getSymbol(#1)#2\end{\@putSymbol[#2]{#1}}
+% \end{macrocode}
+% \cmd{\@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 \cmd{\@@symbol} using \cmd{\@saveBeforeSymbolMacro} and \cmd{\@@tempSymbol}.
+% Then the macro is expanded.
+% \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}
+% This is an auxiliary macro that sets as default set the text of register
+% \cmd{\@@symbol} on the given position. If, however, a parameter is given,
+% \cmd{\@@symbol} is set to this parameter before \cmd{\@@symbol} is set. The
+% macro is used by all the diagrams to set the symbols when they have
+% been determined.
+% \begin{macrocode}
+\newcommand{\@putSymbol}[2][\the\@@symbol]{%
+ \global\@@symbol=\expandafter{#1}%
+ \put(#2){\makebox(20,20){\texttt{\the\@@symbol}}}}
+%</Tdiagram>
+% \end{macrocode}
+% \end{macro}
+%
+% \MakeShortVerb{\|} ^^A Usefull as " is used by the grammar
+% \subsection{Reserved words}
+%
+% \begin{macrocode}
+%<*reservedWords>
+\TestForConflict{\reservestyle,\@reservestyle,\setreserved,\<}
+\TestForConflict{\@parseDefineReserved,\@xparseDefineReserved}
+\TestForConflict{\@defineReserved,\@xdefineReserved}
+% \end{macrocode}
+%
+% \begin{macro}{\reservestyle}
+% \changes{2.0$\alpha$}{1996/05/18}{Added commands for setting reserved
+% words: \cs{reservestyle} and \cs{<}}
+% \cmd{\reservestyle} defines the typesetting style for a class of reserved
+% words by defining a command for defining reserved words
+% from this class
+% \begin{macrocode}
+\newcommand{\reservestyle}[3][]{
+ \newcommand{#2}{\@parseDefineReserved{#1}{#3}}
+% \end{macrocode}
+% \cmd{\reservestyle} takes an optional command to control the spacing, \eg
+% \cmd{\mathinner}, a command \cs{\meta{name}} and a formatting
+% macro. The commandname is defined to call an internal parsing function,
+% \cmd{\@parseDefineReserved} which will reserve the concrete words.
+% \begin{macrocode}
+ \expandafter\expandafter\expandafter\def
+ \expandafter\csname set\expandafter\@gobble\string#2\endcsname##1%
+ {#1{#3{##1}}}}
+% \end{macrocode}
+% Defines the command \cs{set\meta{name}} as a shortcut to get the
+% specified style. For an explanation of the expansion of
+% \cs{set\meta{name}}, see the definition of "@xdefineReserved" on
+% p.~\pageref{page:styleExpansion}.
+% \end{macro} ^^A \reservestyle
+%
+% \begin{macro}{\@parseDefineReserved}^^A
+% \begin{macro}{\@xparseDefineReserved}^^A
+% \cmd{\@parseDefineReserved} parses the parameters and set up the following
+% two internal registers, which are used when defining each word.
+% \begin{macrocode}
+\newtoks\@@spacing
+\newtoks\@@formating
+\def\@parseDefineReserved#1#2{%
+ \@ifnextchar[{\@xparseDefineReserved{#2}}%
+ {\@xparseDefineReserved{#2}[#1]}}
+% \end{macrocode}
+% If no spacing command is provided to the definition, the default ("#1")
+% for the style is used.
+% \begin{macrocode}
+\def\@xparseDefineReserved#1[#2]#3{%
+ \@@formating{#1}%
+ \@@spacing{#2}%
+ \expandafter\@defineReserved#3,\end
+}
+% \end{macrocode}
+% The formatting and the spacing information is saved and then the
+% comma separated list of words to be reserved are processed. The
+% sequence ",\end" gives and end marker.
+% \end{macro} ^^A \@parseDefineReserved
+% \end{macro} ^^A \@xparseDefineReserved
+%
+% \begin{macro}{\@defineReserved}^^A
+% \begin{macro}{\@xdefineReserved}
+% The two commands define a reserved word: \cmd{\@defineReserved} testes if
+% it is the last argument and makes it possible for \cmd{\@xdefineReserved} to
+% test if an alternative text is provided. \cmd{\@xdefineReserved} also
+% defines the reserved word.
+% \begin{macrocode}
+\def\@defineReserved#1,{%
+ \@ifnextchar\end
+% \end{macrocode}
+% Testes if this is the last word (\cmd{\end} is following the comma) to
+% decide if another iteration should be done after defining the word in
+% "#1".
+% \begin{macrocode}
+ {\@xdefineReserved #1[]\END\@gobble}%
+% \end{macrocode}
+% If is was the last then remove the endmarker \cmd{\end}.
+% \begin{macrocode}
+ {\@xdefineReserved#1[]\END\@defineReserved}}
+% \end{macrocode}
+% "[]" is inserted to ensure \cmd{\@xdefineReserved} that all
+% definitions have a pair of and \cmd{\END} makes it possible to remove an
+% extra set of brackets, if there was already a pair of brackets in "#1".
+% \begin{macrocode}
+\def\@xdefineReserved#1[#2]#3\END{%
+ \def\reserved@a{#2}%
+ \ifx \reserved@a\empty \toks0{#1}\else \toks0{#2} \fi
+% \end{macrocode}
+% If the optional text is empty the word is used as text (saved in token
+% register 0).
+% \begin{macrocode}
+ \expandafter\edef\csname\expandafter<#1>\endcsname
+ {\the\@@formating{\the\@@spacing{\the\toks0}}}}
+% \end{macrocode}
+% \label{page:styleExpansion}
+% This defines the reserved word given in "#1" to the text given in
+% "#2". Saving "#2" in token register 0 is done to avoid having \cmd{\edef}
+% expanding any commands in the text (\see \cite[p.~216]{texbook}).
+%
+% The reserved words are saved as macros with the names enclosed in angle
+% brackets. They can thus only be expanded using
+% \cmd{\csname}\lttdots\cmd{\endcsname}. The typesetting ("{#1{#3}}") is done
+% inside a group so it is possible to use style changing commands like
+% \cmd{\scriptstyle} (though it would admittedly be strange). By enclosing
+% the text "#2" in brackets one argument commands like \cmd{\textbf} are also
+% possible.
+%
+% Be aware that the use of \cmd{\def} to
+% define the command, allows redefinition of a already reserved words an
+% even other macros.
+% \end{macro} ^^A \@xdefineReserved
+% \end{macro} ^^A \@DefineReserved
+%
+% \begin{macro}{\setreserved}
+% \begin{macro}{\<}
+% \cmd{\setreserved} is a command for internal use (however provided for the
+% user if necessary to avoid conflict on "\<") to typeset a reserved word.
+% \cmd{\setreserved} is used by "\<",
+% the command to typeset reserved words, and the argument is thus
+% delimited by a ">" (the use being \cs{<\meta{name}>}).
+% \begin{macrocode}
+\def\setreserved#1>{%
+ \expandafter\let\expandafter\reserved@a\csname<#1>\endcsname
+ \@ifundefined{reserved@a}{\PackageError{Semantic}
+ {``#1'' is not defined as a reserved word}%
+ {Before referring to a name as a reserved word, it %
+ should be defined\MessageBreak using an appropriate style
+ definer. A style definer is defined \MessageBreak
+ using \protect\reservestyle.\MessageBreak%
+ Type <return> to proceed --- nothing will be set.}}%
+ {\reserved@a}}
+\let\<=\setreserved
+%</reservedWords>
+% \end{macrocode}
+% Typesetting of the reserved word is done by expanding the macro defined
+% for the name. The macro name is first build in the internal \LaTeX\
+% register \cmd{\reserved@a} so it can be tested if the name is defined.
+% \end{macro}
+% \end{macro}
+%
+% \subsection{The Short Hands Part}
+% \changes{2.0}{1998/05/24}{Made the short hand options part}
+% At last come all the commands for symbols facilitating the notation of
+% semantics. They are all fairly simple, taking some arguments and setting
+% them in an pproriate font intermixed with some filling symbols.
+%
+% \subsubsection{The Symbols \@bblb and \@bbrb}
+% \begin{macro}{\@bblb}
+% \begin{macro}{\@bbrb}
+% \begin{macro}{\@mbblb}
+% \begin{macro}{\@mbbrb}
+% \changes{1.0}{1995/10/20}{I have defined ``fake''-black\-board\-bold for
+% the benefit of people who do not have \package{bbold}}
+% \changes{1.2$\alpha$}{1996/01/31}{Changed the names}
+% \changes{1.2$\alpha$}{1996/01/31}{Added permanent use of document main font}
+% \makeatletter\changes{2.0}{1998/05/24}{Moved to the new "shorthand" options part and made ligatures for $\@bblb$ and $\@bbrb$.}\makeatother
+% \changes{2.0}{1998/05/24}{Introduced the math mode commands \cs{@mbblb} and \cs{@mbbrb}.}
+% \makeatletter
+% If \package{bbold}, is installed it is used to make \@bblb\ og \@bbrb.
+% Otherwise two brackets are drawn together. To make this transparent to the
+% rest of the package, two commands \cmd{\@bblb} (\textbf{b}lackboard
+% \textbf{b}old \textbf{l}eft \textbf{b}racket) and \cmd{\bbrb}
+% (\textbf{b}lackboard \textbf{b}old \textbf{r}ight \textbf{b}racket) are
+% defined , which in both cases gives \@bblb\ or \@bbrb, respectively.
+% \begin{macrocode}
+%<*shorthand>
+\IfFileExists{DONOTUSEmathbbol.sty}{%
+ \RequirePackage{mathbbol}
+ \newcommand{\@bblb}{\textbb{[}}
+ \newcommand{\@bbrb}{\textbb{]}}
+ \newcommand{\@mbblb}{\mathopen{\mbox{\textbb{[}}}}
+ \newcommand{\@mbbrb}{\mathclose{\mbox{\textbb{]}}}}
+}
+{ \newcommand{\@bblb}{\textnormal{[\kern-.15em[}}
+ \newcommand{\@bbrb}{\textnormal{]\kern-.15em]}}
+ \newcommand{\@mbblb}{\mathopen{[\mkern-2.67mu[}}
+ \newcommand{\@mbbrb}{\mathclose{]\mkern-2.67mu]}}
+}
+% \end{macrocode}
+% \makeatother
+% \end{macro}
+% \end{macro}
+% \end{macro}
+% \end{macro}
+%
+% \subsubsection{Short Hands for the Often Needed Symbols}
+%
+% This defines the often needed symbols. Note that by specifying the option
+% "shorthand" math ligatures are automatically loaded.
+% \begin{macrocode}
+\mathlig{|-}{\vdash}
+\mathlig{|=}{\models}
+\mathlig{->}{\rightarrow}
+\mathlig{->*}{\mathrel{\rightarrow^*}}
+\mathlig{->+}{\mathrel{\rightarrow^+}}
+\mathlig{-->}{\longrightarrow}
+\mathlig{-->*}{\mathrel{\longrightarrow^*}}
+\mathlig{-->+}{\mathrel{\longrightarrow^+}}
+\mathlig{=>}{\Rightarrow}
+\mathlig{=>*}{\mathrel{\Rightarrow^*}}
+\mathlig{=>+}{\mathrel{\Rightarrow^+}}
+\mathlig{==>}{\Longrightarrow}
+\mathlig{==>*}{\mathrel{\Longrightarrow^*}}
+\mathlig{==>+}{\mathrel{\Longrightarrow^+}}
+\mathlig{<-}{\leftarrow}
+\mathlig{*<-}{\mathrel{{}^*\mkern-1mu\mathord\leftarrow}}
+\mathlig{+<-}{\mathrel{{}^+\mkern-1mu\mathord\leftarrow}}
+\mathlig{<--}{\longleftarrow}
+\mathlig{*<--}{\mathrel{{}^*\mkern-1mu\mathord{\longleftarrow}}}
+\mathlig{+<--}{\mathrel{{}^+\mkern-1mu\mathord{\longleftarrow}}}
+\mathlig{<=}{\Leftarrow}
+\mathlig{*<=}{\mathrel{{}^*\mkern-1mu\mathord\Leftarrow}}
+\mathlig{+<=}{\mathrel{{}^+\mkern-1mu\mathord\Leftarrow}}
+\mathlig{<==}{\Longleftarrow}
+\mathlig{*<==}{\mathrel{{}^*\mkern-1mu\mathord{\Longleftarrow}}}
+\mathlig{+<==}{\mathrel{{}^+\mkern-1mu\mathord{\Longleftarrow}}}
+\mathlig{<->}{\longleftrightarrow}
+\mathlig{<=>}{\Longleftrightarrow}
+\mathlig{|[}{\@mbblb}
+\mathlig{|]}{\@mbbrb}
+% \end{macrocode}
+%
+% \subsubsection{Denotational Semantics}
+% I have given a lot of thoughts to the problem of choosing a good syntax.
+% The most essential requirement was that syntax should be consistent and
+% simple/intuitive, close to that used in \emph{Introduction to the Semantics
+% of Programming Languages}. To a semantics person, the most natural way to get
+% \eval{\lttdots}{x} would probably be "\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 decisively, one cannot make an analogoues syntax for
+% \cmd{\evalsymbol} since it is undecidable whether it is followed by a
+% symbol: Does \emph{eg} "\evalsymbol test" mean ``\evalsymbol[t]est'' or
+% ``\evalsymbol test''? This makes it necessary to use brackets in connection
+% with \cmd{\evalsymbol} and in order to have a consistent syntax, I have made
+% the same decission for \cmd{\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'' based on the decided syntax}
+% \begin{macrocode}
+\newcommand{\evalsymbol}[1][]{\ensuremath{\mathcal{E}^{#1}}}
+\newcommand{\compsymbol}[1][]{\ensuremath{\mathcal{C}^{#1}}}
+% \end{macrocode}
+% These lines define commands that take an 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
+% just special cases of the other commands (with the decided
+% syntax). Furthermore the names were translated from danish into english}
+% \changes{1.2$\alpha$}{1996/01/30}{Made a brand new definition to avoid an
+% error when using \cs{comp} and \cs{eval} with 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)}$}}
+%</shorthand>
+% \end{macrocode}
+% The command \cmd{\exe} is a stub that checks if the second argument begins
+% with an optional sharp by looking at the token following the first
+% argument. If a bracket is not provided, an empty second argument is
+% added before the control is given to \cmd{\@exe}, which does the setting.
+% There is no place to do an expedient linebreak, so everything is
+% encapsulated in a \cmd{\mbox}.
+% \end{macro}
+%
+% \subsection{End of All Options Files}
+%
+% All the options files are ended with the following code to match the test
+% whether the file is loaded from the semantics package
+% (\emph{see}~\pageref{page:testForSemanticsLoader}):
+% \begin{macrocode}
+%<*allOptions>
+\fi
+%</allOptions>
+% \end{macrocode}
+%
+% \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 document header at the bottom, and introduced a hack making \LaTeX\ think it is loading \texttt{semantic.sty} when processing \texttt{semantic.dtx}}
+%
+% The document preamble and the code to generate code is placed at the end,
+% so that the documentation may be printed before \semantic\ is installed.
+% For 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[latin1]{inputenc}
+% \end{macrocode}
+% We test whether multiple columns are supported (the package is
+% loaded by \package{ltxdoc}):
+% \begin{macrocode}
+\newif\ifmulticols
+\IfFileExists{multicol.sty}{\multicolstrue}{}
+% \end{macrocode}
+% We make a command \cmd{\command} for the dangerous bend sign (used in the
+% \TeX-book). If the font "manfnt.tfm" is not installed on your
+% system, you should turn the second line, \cmd{\dangertrue} into a
+% comment:
+% \begin{macrocode}
+\newif\ifdanger
+\dangertrue
+\DeclareFontFamily{U}{manual}{}
+\DeclareFontShape{U}{manual}{m}{n}{<-> manfnt }{}
+\newcommand{\danger}
+ {{\fontencoding{U}\fontfamily{manual}\selectfont\symbol{127}}}
+% \end{macrocode}
+% We define some abbreviations used in the text,
+% \begin{macrocode}
+\usepackage{xspace}
+\newcommand{\ie}{\emph{ie}\xspace}
+\newcommand{\eg}{\emph{eg}\xspace}
+\newcommand{\see}{\emph{see}\xspace}
+\newcommand{\semantic}{\texttt{semantic}\xspace}
+\newcommand{\lttdots}{\ensuremath{\mathtt{\ldots}}}
+\newcommand{\ExplicitSpace}{\texttt{\char'040}}
+% \end{macrocode}
+% a command for typesetting the names of other packages.
+% \begin{macrocode}
+\newcommand{\package}[1]{\textsf{#1}}
+% \end{macrocode}
+% and a command for printing CVS tags.
+% \begin{macrocode}
+\def\RCS$#1: #2 ${\@namedef{RCS#1}{#2}}
+% \end{macrocode}
+% \changes{2.0(delta)}{2002/06/19}{Included the RCS revision in the file information}
+%
+% We make a command \cmd{\labelnextline} for labelling the following line
+% \begin{macrocode}
+\newcommand{\labelnextline}[1]{{%
+ \count8\inputlineno \advance\count8\@ne
+ \@bsphack
+ \protected@write\@auxout{}%
+ {\string\newlabel{#1}{{\the\count8}{\thepage}}}%
+ \@esphack}}
+% \end{macrocode}
+% We then define that the default is to typeset only the manual so we
+% can live without cross references.
+% \begin{macrocode}
+\OnlyDescription
+\DisableCrossrefs
+% \end{macrocode}
+% You can change this behaviour by uncommenting line two to five
+% below. That will include the implementation and also add
+% crossreferences, an index of the command usage and definitions, and
+% the change history.
+% \begin{macrocode}
+\labelnextline{lin:AlsoImplementation}
+ % \AlsoImplementation
+ % \EnableCrossrefs
+ % \CodelineIndex
+ % \RecordChanges
+% \end{macrocode}
+% We define the command \cmd{\semanticVersionPrint} containing the commands to
+% to typeset the version number with neatly formatting of the Greek letter.
+% \begin{macrocode}
+\makeatletter
+{\def\ver#1(#2)#3\relax{%
+ \def\tc{#1}%
+ \def\td{#2}%
+ \ifx\td\empty
+ \else \edef\td{$\csname #2\endcsname$}\fi}%
+ \expandafter\ver\semanticVersion()\relax
+ \xdef\semanticVersionPrint{\tc\td}}
+% \end{macrocode}
+% (\cmd{\tc} and \cmd{\td} are use similarly in \LaTeX's \cmd{\GetInfo}.)
+% \changes{2.0\delta}{2002/07/12}{Deleted \cs{GetInfo}.}
+% \changes{2.0\delta}{2002/07/12}{Introduced \cs{semanticVersionPrint} to give a formatted version number.}
+% We define a command \cmd{\parmark}\oarg{mark} which starts a
+% paragraph with \meta{mark} to the left of the paragraph. This is to
+% put dangerous bends around certain paragraphs. If \meta{mark} is
+% not given, the default set with \cmd{\setparagraphmark} is used.
+% \begin{macrocode}
+\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 to\z@{\box0 \vss}\hfill}}}
+% \end{macrocode}
+% We make an environment for typesetting small pieces of code
+% \begin{macrocode}
+\newenvironment{code}
+ {\begin{verse}\small}
+ {\end{verse}}
+% \end{macrocode}
+% and a variant of the "itemize" environment to be used inside
+% columns (we choose smaller values of the indentation).
+% \begin{macrocode}
+\newenvironment{columnItemize}%
+ {\begin{list}%
+ {$\bullet$}%
+ {\settowidth{\labelwidth}{$\bullet$}%
+ \setlength{\leftmargin}{5mm}%
+ \setlength{\labelsep}{\leftmargin}%
+ \addtolength{\labelsep}{-\labelwidth}}}%
+ {\end{list}}
+% \end{macrocode}
+% Finally, we print a (hopefully) comforting message to the user
+% \begin{macrocode}
+\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 2725)}
+\typeout{\@spaces\@spaces \protect\dangertrue}
+\typeout{}
+\typeout{There will be some overfull and underfull boxes, %
+ and some moved marginpars.}
+\typeout{Do not bother!!!}
+\typeout{}
+\makeatother
+% \end{macrocode}
+% before we finally starts typesetting the manual.
+% \begin{macrocode}
+\begin{document}
+ \DocInput{semantic.dtx}
+\end{document}
+%</documentation>
+% \end{macrocode}
+%
+% \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
+% \bibitem{LaTeXbook}
+% \textsc{L. Lamport} \emph{\LaTeX\ : a Document preparation system}, 1994, Addison-Wesley
+% \end{thebibliography}
+%
+% \Finale\PrintIndex \sloppy \PrintChanges
+\endinput
+