123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368 |
- %%
- %% This is the original source file mathpar.sty
- %%
- %% Package `mathpar' to use with LaTeX 2e
- %% Copyright Didier Remy, all rights reserved.
- \NeedsTeXFormat{LaTeX2e}
- \ProvidesPackage{mathpartir}
- [2001/23/02 v0.92 Math Paragraph for Type Inference Rules]
- %%
- %% Identification
- %% Preliminary declarations
- \RequirePackage {keyval}
- %% Options
- %% More declarations
- %% PART I: Typesetting maths in paragraphe mode
- \newdimen \mpr@tmpdim
- % To ensure hevea \hva compatibility, \hva should expands to nothing
- % in mathpar or in mathrule
- \let \mpr@hva \empty
- %% normal paragraph parametters, should rather be taken dynamically
- \def \mpr@savepar {%
- \edef \MathparNormalpar
- {\noexpand \lineskiplimit \the\lineskiplimit
- \noexpand \lineskip \the\lineskip}%
- }
- \def \mpr@rulelineskip {\lineskiplimit=0.3em\lineskip=0.2em plus 0.1em}
- \def \mpr@lesslineskip {\lineskiplimit=0.6em\lineskip=0.5em plus 0.2em}
- \def \mpr@lineskip {\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em}
- \let \MathparLineskip \mpr@lineskip
- \def \mpr@paroptions {\MathparLineskip}
- \let \mpr@prebindings \relax
- \newskip \mpr@andskip \mpr@andskip 2em plus 0.5fil minus 0.5em
- \def \mpr@goodbreakand
- {\hskip -\mpr@andskip \penalty -1000\hskip \mpr@andskip}
- \def \mpr@and {\hskip \mpr@andskip}
- \def \mpr@andcr {\penalty 50\mpr@and}
- \def \mpr@cr {\penalty -10000\mpr@and}
- \def \mpr@eqno #1{\mpr@andcr #1\hskip 0em plus -1fil \penalty 10}
- \def \mpr@bindings {%
- \let \and \mpr@andcr
- \let \par \mpr@andcr
- \let \\\mpr@cr
- \let \eqno \mpr@eqno
- \let \hva \mpr@hva
- }
- \let \MathparBindings \mpr@bindings
- % \@ifundefined {ignorespacesafterend}
- % {\def \ignorespacesafterend {\aftergroup \ignorespaces}
- \newenvironment{mathpar}[1][]
- {$$\mpr@savepar \parskip 0em \hsize \linewidth \centering
- \vbox \bgroup \mpr@prebindings \mpr@paroptions #1\ifmmode $\else
- \noindent $\displaystyle\fi
- \MathparBindings}
- {\unskip \ifmmode $\fi\egroup $$\ignorespacesafterend}
- % \def \math@mathpar #1{\setbox0 \hbox {$\displaystyle #1$}\ifnum
- % \wd0 < \hsize $$\box0$$\else \bmathpar #1\emathpar \fi}
- %%% HOV BOXES
- \def \mathvbox@ #1{\hbox \bgroup \mpr@normallineskip
- \vbox \bgroup \tabskip 0em \let \\ \cr
- \halign \bgroup \hfil $##$\hfil\cr #1\crcr \egroup \egroup
- \egroup}
- \def \mathhvbox@ #1{\setbox0 \hbox {\let \\\qquad $#1$}\ifnum \wd0 < \hsize
- \box0\else \mathvbox {#1}\fi}
- %% Part II -- operations on lists
- \newtoks \mpr@lista
- \newtoks \mpr@listb
- \long \def\mpr@cons #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
- {#2}\edef #2{\the \mpr@lista \the \mpr@listb}}
- \long \def\mpr@snoc #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
- {#2}\edef #2{\the \mpr@listb\the\mpr@lista}}
- \long \def \mpr@concat#1=#2\mpr@to#3{\mpr@lista \expandafter {#2}\mpr@listb
- \expandafter {#3}\edef #1{\the \mpr@listb\the\mpr@lista}}
- \def \mpr@head #1\mpr@to #2{\expandafter \mpr@head@ #1\mpr@head@ #1#2}
- \long \def \mpr@head@ #1#2\mpr@head@ #3#4{\def #4{#1}\def#3{#2}}
- \def \mpr@flatten #1\mpr@to #2{\expandafter \mpr@flatten@ #1\mpr@flatten@ #1#2}
- \long \def \mpr@flatten@ \\#1\\#2\mpr@flatten@ #3#4{\def #4{#1}\def #3{\\#2}}
- \def \mpr@makelist #1\mpr@to #2{\def \mpr@all {#1}%
- \mpr@lista {\\}\mpr@listb \expandafter {\mpr@all}\edef \mpr@all {\the
- \mpr@lista \the \mpr@listb \the \mpr@lista}\let #2\empty
- \def \mpr@stripof ##1##2\mpr@stripend{\def \mpr@stripped{##2}}\loop
- \mpr@flatten \mpr@all \mpr@to \mpr@one
- \expandafter \mpr@snoc \mpr@one \mpr@to #2\expandafter \mpr@stripof
- \mpr@all \mpr@stripend
- \ifx \mpr@stripped \empty \let \mpr@isempty 0\else \let \mpr@isempty 1\fi
- \ifx 1\mpr@isempty
- \repeat
- }
- %% Part III -- Type inference rules
- \def \mpr@rev #1\mpr@to #2{\let \mpr@tmp \empty
- \def \\##1{\mpr@cons ##1\mpr@to \mpr@tmp}#1\let #2\mpr@tmp}
- \newif \if@premisse
- \newbox \mpr@hlist
- \newbox \mpr@vlist
- \newif \ifmpr@center \mpr@centertrue
- \def \mpr@htovlist {%
- \setbox \mpr@hlist
- \hbox {\strut
- \ifmpr@center \hskip -0.5\wd\mpr@hlist\fi
- \unhbox \mpr@hlist}%
- \setbox \mpr@vlist
- \vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist
- \else \unvbox \mpr@vlist \box \mpr@hlist
- \fi}%
- }
- % OLD version
- % \def \mpr@htovlist {%
- % \setbox \mpr@hlist
- % \hbox {\strut \hskip -0.5\wd\mpr@hlist \unhbox \mpr@hlist}%
- % \setbox \mpr@vlist
- % \vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist
- % \else \unvbox \mpr@vlist \box \mpr@hlist
- % \fi}%
- % }
- \def \mpr@sep{2em}
- \def \mpr@blank { }
- \def \mpr@hovbox #1#2{\hbox
- \bgroup
- \ifx #1T\@premissetrue
- \else \ifx #1B\@premissefalse
- \else
- \PackageError{mathpartir}
- {Premisse orientation should either be P or B}
- {Fatal error in Package}%
- \fi \fi
- \def \@test {#2}\ifx \@test \mpr@blank\else
- \setbox \mpr@hlist \hbox {}%
- \setbox \mpr@vlist \vbox {}%
- \if@premisse \let \snoc \mpr@cons \else \let \snoc \mpr@snoc \fi
- \let \@hvlist \empty \let \@rev \empty
- \mpr@tmpdim 0em
- \expandafter \mpr@makelist #2\mpr@to \mpr@flat
- \if@premisse \mpr@rev \mpr@flat \mpr@to \@rev \else \let \@rev \mpr@flat \fi
- \def \\##1{%
- \def \@test {##1}\ifx \@test \empty
- \mpr@htovlist
- \mpr@tmpdim 0em %%% last bug fix not extensively checked
- \else
- \setbox0 \hbox{$\displaystyle {##1}$}\relax
- \advance \mpr@tmpdim by \wd0
- %\mpr@tmpdim 1.02\mpr@tmpdim
- \ifnum \mpr@tmpdim < \hsize
- \ifnum \wd\mpr@hlist > 0
- \if@premisse
- \setbox \mpr@hlist
- \hbox {\unhbox0 \hskip \mpr@sep \unhbox \mpr@hlist}%
- \else
- \setbox \mpr@hlist
- \hbox {\unhbox \mpr@hlist \hskip \mpr@sep \unhbox0}%
- \fi
- \else
- \setbox \mpr@hlist \hbox {\unhbox0}%
- \fi
- \else
- \ifnum \wd \mpr@hlist > 0
- \mpr@htovlist
- \mpr@tmpdim \wd0
- \fi
- \setbox \mpr@hlist \hbox {\unhbox0}%
- \fi
- \advance \mpr@tmpdim by \mpr@sep
- \fi
- }%
- \@rev
- \mpr@htovlist
- \ifmpr@center \hskip \wd\mpr@vlist\fi \box \mpr@vlist
- \fi
- \egroup
- }
- %%% INFERENCE RULES
- \@ifundefined{@@over}{%
- \let\@@over\over % fallback if amsmath is not loaded
- \let\@@overwithdelims\overwithdelims
- \let\@@atop\atop \let\@@atopwithdelims\atopwithdelims
- \let\@@above\above \let\@@abovewithdelims\abovewithdelims
- }{}
- \def \mpr@@fraction #1#2{\hbox {\advance \hsize by -0.5em
- $\displaystyle {#1\@@over #2}$}}
- \let \mpr@fraction \mpr@@fraction
- \def \mpr@@reduce #1#2{\hbox
- {$\lower 0.01pt \mpr@@fraction {#1}{#2}\mkern -15mu\rightarrow$}}
- \def \mpr@@rewrite #1#2#3{\hbox
- {$\lower 0.01pt \mpr@@fraction {#2}{#3}\mkern -8mu#1$}}
- \def \mpr@infercenter #1{\vcenter {\mpr@hovbox{T}{#1}}}
- \def \mpr@empty {}
- \def \mpr@inferrule
- {\bgroup
- \ifnum \linewidth<\hsize \hsize \linewidth\fi
- \mpr@rulelineskip
- \let \and \qquad
- \let \hva \mpr@hva
- \let \@rulename \mpr@empty
- \let \@rule@options \mpr@empty
- \mpr@inferrule@}
- \newcommand {\mpr@inferrule@}[3][]
- {\everymath={\displaystyle}%
- \def \@test {#2}\ifx \empty \@test
- \setbox0 \hbox {$\vcenter {\mpr@hovbox{B}{#3}}$}%
- \else
- \def \@test {#3}\ifx \empty \@test
- \setbox0 \hbox {$\vcenter {\mpr@hovbox{T}{#2}}$}%
- \else
- \setbox0 \mpr@fraction {\mpr@hovbox{T}{#2}}{\mpr@hovbox{B}{#3}}%
- \fi \fi
- \def \@test {#1}\ifx \@test\empty \box0
- \else \vbox
- %%% Suggestion de Francois pour les etiquettes longues
- %%% {\hbox to \wd0 {\RefTirName {#1}\hfil}\box0}\fi
- {\hbox {\RefTirName {#1}}\box0}\fi
- \egroup}
- \def \mpr@vdotfil #1{\vbox to #1{\leaders \hbox{$\cdot$} \vfil}}
- % They are two forms
- % \mathrule [label]{[premisses}{conclusions}
- % or
- % \mathrule* [options]{[premisses}{conclusions}
- %
- % Premisses and conclusions are lists of elements separated by \\
- % Each \\ produces a break, attempting horizontal breaks if possible,
- % and vertical breaks if needed.
- %
- % An empty element obtained by \\\\ produces a vertical break in all cases.
- %
- % The former rule is aligned on the fraction bar.
- % The optional label appears on top of the rule
- % The second form to be used in a derivation tree is aligned on the last
- % line of its conclusion
- %
- % The second form can be parameterized, using the key=val interface. The
- % folloiwng keys are recognized:
- %
- % width set the width of the rule to val
- % narrower set the width of the rule to val\hsize
- % before execute val at the beginning/left
- % lab put a label [Val] on top of the rule
- % lskip add negative skip on the right
- % llab put a left label [Val], ignoring its width
- % left put a left label [Val]
- % right put a right label [Val]
- % rlab put a right label [Val], ignoring its width
- % rskip add negative skip on the left
- % vdots lift the rule by val and fill vertical space with dots
- % after execute val at the end/right
- %
- % Note that most options must come in this order to avoid strange
- % typesetting (in particular lskip must preceed left and llab and
- % rskip must follow rlab or right; vdots must come last or be followed by
- % rskip.
- %
- \define@key {mprset}{flushleft}[]{\mpr@centerfalse}
- \define@key {mprset}{center}[]{\mpr@centertrue}
- \def \mprset #1{\setkeys{mprset}{#1}}
- \newbox \mpr@right
- \define@key {mpr}{flushleft}[]{\mpr@centerfalse}
- \define@key {mpr}{center}[]{\mpr@centertrue}
- \define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
- \advance \hsize by -\wd0\box0}
- \define@key {mpr}{width}{\hsize #1}
- \define@key {mpr}{sep}{\def\mpr@sep{#1}}
- \define@key {mpr}{before}{#1}
- \define@key {mpr}{lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}
- \define@key {mpr}{Lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}
- \define@key {mpr}{narrower}{\hsize #1\hsize}
- \define@key {mpr}{leftskip}{\hskip -#1}
- \define@key {mpr}{reduce}[]{\let \mpr@fraction \mpr@@reduce}
- \define@key {mpr}{rightskip}
- {\setbox \mpr@right \hbox {\unhbox \mpr@right \hskip -#1}}
- \define@key {mpr}{LEFT}{\setbox0 \hbox {$#1$}\relax
- \advance \hsize by -\wd0\box0}
- \define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
- \advance \hsize by -\wd0\box0}
- \define@key {mpr}{Left}{\llap{$\TirName {#1}\;$}}
- \define@key {mpr}{right}
- {\setbox0 \hbox {$\;\TirName {#1}$}\relax \advance \hsize by -\wd0
- \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
- \define@key {mpr}{RIGHT}
- {\setbox0 \hbox {$#1$}\relax \advance \hsize by -\wd0
- \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
- \define@key {mpr}{Right}
- {\setbox \mpr@right \hbox {\unhbox \mpr@right \rlap {$\;\TirName {#1}$}}}
- \define@key {mpr}{vdots}{\def \mpr@vdots {\@@atop \mpr@vdotfil{#1}}}
- \define@key {mpr}{after}{\edef \mpr@after {\mpr@after #1}}
- \newdimen \rule@dimen
- \newcommand \mpr@inferstar@ [3][]{\setbox0
- \hbox {\let \mpr@rulename \mpr@empty \let \mpr@vdots \relax
- \setbox \mpr@right \hbox{}%
- $\setkeys{mpr}{#1}%
- \ifx \mpr@rulename \mpr@empty \mpr@inferrule {#2}{#3}\else
- \mpr@inferrule [{\mpr@rulename}]{#2}{#3}\fi
- \box \mpr@right \mpr@vdots$}
- \setbox1 \hbox {\strut}
- \rule@dimen \dp0 \advance \rule@dimen by -\dp1
- \raise \rule@dimen \box0}
- \def \mpr@infer {\@ifnextchar *{\mpr@inferstar}{\mpr@inferrule}}
- \newcommand \mpr@err@skipargs[3][]{}
- \def \mpr@inferstar*{\ifmmode
- \let \@do \mpr@inferstar@
- \else
- \let \@do \mpr@err@skipargs
- \PackageError {mathpartir}
- {\string\inferrule* can only be used in math mode}{}%
- \fi \@do}
- %%% Exports
- % Envirnonment mathpar
- \let \inferrule \mpr@infer
- % make a short name \infer is not already defined
- \@ifundefined {infer}{\let \infer \mpr@infer}{}
- \def \tir@name #1{\hbox {\small \sc #1}}
- \let \TirName \tir@name
- \let \RefTirName \tir@name
- %%% Other Exports
- % \let \listcons \mpr@cons
- % \let \listsnoc \mpr@snoc
- % \let \listhead \mpr@head
- % \let \listmake \mpr@makelist
- \endinput
|