% Mathpartir --- Math Paragraph for Typesetting Inference Rules+ −
%+ −
% Copyright (C) 2001, 2002, 2003 Didier Rémy+ −
%+ −
% Author : Didier Remy + −
% Version : 1.1.1+ −
% Bug Reports : to author+ −
% Web Site : http://pauillac.inria.fr/~remy/latex/+ −
% + −
% WhizzyTeX is free software; you can redistribute it and/or modify+ −
% it under the terms of the GNU General Public License as published by+ −
% the Free Software Foundation; either version 2, or (at your option)+ −
% any later version.+ −
% + −
% Mathpartir is distributed in the hope that it will be useful,+ −
% but WITHOUT ANY WARRANTY; without even the implied warranty of+ −
% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the+ −
% GNU General Public License for more details + −
% (http://pauillac.inria.fr/~remy/license/GPL).+ −
%+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
% File mathpartir.sty (LaTeX macros)+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
+ −
\NeedsTeXFormat{LaTeX2e}+ −
\ProvidesPackage{mathpartir}+ −
[2003/07/10 version 1.1.1 Math Paragraph for Typesetting 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 inferrule+ −
\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+ −
% \inferrule [label]{[premisses}{conclusions}+ −
% or+ −
% \inferrule* [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+ −
% left put a left label [Val]+ −
% Left put a left label [Val], ignoring its width + −
% right put a right label [Val]+ −
% Right put a right label [Val], ignoring its width+ −
% leftskip skip negative space on the left-hand side+ −
% rightskip skip negative space on the right-hand side+ −
% 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 leftskip must preceed left and Left and+ −
% rightskip must follow Right or right; vdots must come last + −
% or be only followed by rightskip. + −
% + −
+ −
\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+ −