23004

1 
% Mathpartir  Math Paragraph for Typesetting Inference Rules


2 
%


3 
% Copyright (C) 2001, 2002, 2003, 2004, 2005 Didier Rémy


4 
%


5 
% Author : Didier Remy


6 
% Version : 1.2.0


7 
% Bug Reports : to author


8 
% Web Site : http://pauillac.inria.fr/~remy/latex/


9 
%


10 
% Mathpartir is free software; you can redistribute it and/or modify


11 
% it under the terms of the GNU General Public License as published by


12 
% the Free Software Foundation; either version 2, or (at your option)


13 
% any later version.


14 
%


15 
% Mathpartir is distributed in the hope that it will be useful,


16 
% but WITHOUT ANY WARRANTY; without even the implied warranty of


17 
% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the


18 
% GNU General Public License for more details


19 
% (http://pauillac.inria.fr/~remy/license/GPL).


20 
%


21 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


22 
% File mathpartir.sty (LaTeX macros)


23 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


24 


25 
\NeedsTeXFormat{LaTeX2e}


26 
\ProvidesPackage{mathpartir}


27 
[2005/12/20 version 1.2.0 Math Paragraph for Typesetting Inference Rules]


28 


29 
%%


30 


31 
%% Identification


32 
%% Preliminary declarations


33 


34 
\RequirePackage {keyval}


35 


36 
%% Options


37 
%% More declarations


38 


39 
%% PART I: Typesetting maths in paragraphe mode


40 


41 
\newdimen \mpr@tmpdim


42 


43 
% To ensure hevea \hva compatibility, \hva should expands to nothing


44 
% in mathpar or in inferrule


45 
\let \mpr@hva \empty


46 


47 
%% normal paragraph parametters, should rather be taken dynamically


48 
\def \mpr@savepar {%


49 
\edef \MathparNormalpar


50 
{\noexpand \lineskiplimit \the\lineskiplimit


51 
\noexpand \lineskip \the\lineskip}%


52 
}


53 


54 
\def \mpr@rulelineskip {\lineskiplimit=0.3em\lineskip=0.2em plus 0.1em}


55 
\def \mpr@lesslineskip {\lineskiplimit=0.6em\lineskip=0.5em plus 0.2em}


56 
\def \mpr@lineskip {\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em}


57 
\let \MathparLineskip \mpr@lineskip


58 
\def \mpr@paroptions {\MathparLineskip}


59 
\let \mpr@prebindings \relax


60 


61 
\newskip \mpr@andskip \mpr@andskip 2em plus 0.5fil minus 0.5em


62 


63 
\def \mpr@goodbreakand


64 
{\hskip \mpr@andskip \penalty 1000\hskip \mpr@andskip}


65 
\def \mpr@and {\hskip \mpr@andskip}


66 
\def \mpr@andcr {\penalty 50\mpr@and}


67 
\def \mpr@cr {\penalty 10000\mpr@and}


68 
\def \mpr@eqno #1{\mpr@andcr #1\hskip 0em plus 1fil \penalty 10}


69 


70 
\def \mpr@bindings {%


71 
\let \and \mpr@andcr


72 
\let \par \mpr@andcr


73 
\let \\\mpr@cr


74 
\let \eqno \mpr@eqno


75 
\let \hva \mpr@hva


76 
}


77 
\let \MathparBindings \mpr@bindings


78 


79 
% \@ifundefined {ignorespacesafterend}


80 
% {\def \ignorespacesafterend {\aftergroup \ignorespaces}


81 


82 
\newenvironment{mathpar}[1][]


83 
{$$\mpr@savepar \parskip 0em \hsize \linewidth \centering


84 
\vbox \bgroup \mpr@prebindings \mpr@paroptions #1\ifmmode $\else


85 
\noindent $\displaystyle\fi


86 
\MathparBindings}


87 
{\unskip \ifmmode $\fi\egroup $$\ignorespacesafterend}


88 


89 
% \def \math@mathpar #1{\setbox0 \hbox {$\displaystyle #1$}\ifnum


90 
% \wd0 < \hsize $$\box0$$\else \bmathpar #1\emathpar \fi}


91 


92 
%%% HOV BOXES


93 


94 
\def \mathvbox@ #1{\hbox \bgroup \mpr@normallineskip


95 
\vbox \bgroup \tabskip 0em \let \\ \cr


96 
\halign \bgroup \hfil $##$\hfil\cr #1\crcr \egroup \egroup


97 
\egroup}


98 


99 
\def \mathhvbox@ #1{\setbox0 \hbox {\let \\\qquad $#1$}\ifnum \wd0 < \hsize


100 
\box0\else \mathvbox {#1}\fi}


101 


102 


103 
%% Part II  operations on lists


104 


105 
\newtoks \mpr@lista


106 
\newtoks \mpr@listb


107 


108 
\long \def\mpr@cons #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter


109 
{#2}\edef #2{\the \mpr@lista \the \mpr@listb}}


110 


111 
\long \def\mpr@snoc #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter


112 
{#2}\edef #2{\the \mpr@listb\the\mpr@lista}}


113 


114 
\long \def \mpr@concat#1=#2\mpr@to#3{\mpr@lista \expandafter {#2}\mpr@listb


115 
\expandafter {#3}\edef #1{\the \mpr@listb\the\mpr@lista}}


116 


117 
\def \mpr@head #1\mpr@to #2{\expandafter \mpr@head@ #1\mpr@head@ #1#2}


118 
\long \def \mpr@head@ #1#2\mpr@head@ #3#4{\def #4{#1}\def#3{#2}}


119 


120 
\def \mpr@flatten #1\mpr@to #2{\expandafter \mpr@flatten@ #1\mpr@flatten@ #1#2}


121 
\long \def \mpr@flatten@ \\#1\\#2\mpr@flatten@ #3#4{\def #4{#1}\def #3{\\#2}}


122 


123 
\def \mpr@makelist #1\mpr@to #2{\def \mpr@all {#1}%


124 
\mpr@lista {\\}\mpr@listb \expandafter {\mpr@all}\edef \mpr@all {\the


125 
\mpr@lista \the \mpr@listb \the \mpr@lista}\let #2\empty


126 
\def \mpr@stripof ##1##2\mpr@stripend{\def \mpr@stripped{##2}}\loop


127 
\mpr@flatten \mpr@all \mpr@to \mpr@one


128 
\expandafter \mpr@snoc \mpr@one \mpr@to #2\expandafter \mpr@stripof


129 
\mpr@all \mpr@stripend


130 
\ifx \mpr@stripped \empty \let \mpr@isempty 0\else \let \mpr@isempty 1\fi


131 
\ifx 1\mpr@isempty


132 
\repeat


133 
}


134 


135 
\def \mpr@rev #1\mpr@to #2{\let \mpr@tmp \empty


136 
\def \\##1{\mpr@cons ##1\mpr@to \mpr@tmp}#1\let #2\mpr@tmp}


137 


138 
%% Part III  Type inference rules


139 


140 
\newif \if@premisse


141 
\newbox \mpr@hlist


142 
\newbox \mpr@vlist


143 
\newif \ifmpr@center \mpr@centertrue


144 
\def \mpr@htovlist {%


145 
\setbox \mpr@hlist


146 
\hbox {\strut


147 
\ifmpr@center \hskip 0.5\wd\mpr@hlist\fi


148 
\unhbox \mpr@hlist}%


149 
\setbox \mpr@vlist


150 
\vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist


151 
\else \unvbox \mpr@vlist \box \mpr@hlist


152 
\fi}%


153 
}


154 
% OLD version


155 
% \def \mpr@htovlist {%


156 
% \setbox \mpr@hlist


157 
% \hbox {\strut \hskip 0.5\wd\mpr@hlist \unhbox \mpr@hlist}%


158 
% \setbox \mpr@vlist


159 
% \vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist


160 
% \else \unvbox \mpr@vlist \box \mpr@hlist


161 
% \fi}%


162 
% }


163 


164 
\def \mpr@item #1{$\displaystyle #1$}


165 
\def \mpr@sep{2em}


166 
\def \mpr@blank { }


167 
\def \mpr@hovbox #1#2{\hbox


168 
\bgroup


169 
\ifx #1T\@premissetrue


170 
\else \ifx #1B\@premissefalse


171 
\else


172 
\PackageError{mathpartir}


173 
{Premisse orientation should either be T or B}


174 
{Fatal error in Package}%


175 
\fi \fi


176 
\def \@test {#2}\ifx \@test \mpr@blank\else


177 
\setbox \mpr@hlist \hbox {}%


178 
\setbox \mpr@vlist \vbox {}%


179 
\if@premisse \let \snoc \mpr@cons \else \let \snoc \mpr@snoc \fi


180 
\let \@hvlist \empty \let \@rev \empty


181 
\mpr@tmpdim 0em


182 
\expandafter \mpr@makelist #2\mpr@to \mpr@flat


183 
\if@premisse \mpr@rev \mpr@flat \mpr@to \@rev \else \let \@rev \mpr@flat \fi


184 
\def \\##1{%


185 
\def \@test {##1}\ifx \@test \empty


186 
\mpr@htovlist


187 
\mpr@tmpdim 0em %%% last bug fix not extensively checked


188 
\else


189 
\setbox0 \hbox{\mpr@item {##1}}\relax


190 
\advance \mpr@tmpdim by \wd0


191 
%\mpr@tmpdim 1.02\mpr@tmpdim


192 
\ifnum \mpr@tmpdim < \hsize


193 
\ifnum \wd\mpr@hlist > 0


194 
\if@premisse


195 
\setbox \mpr@hlist


196 
\hbox {\unhbox0 \hskip \mpr@sep \unhbox \mpr@hlist}%


197 
\else


198 
\setbox \mpr@hlist


199 
\hbox {\unhbox \mpr@hlist \hskip \mpr@sep \unhbox0}%


200 
\fi


201 
\else


202 
\setbox \mpr@hlist \hbox {\unhbox0}%


203 
\fi


204 
\else


205 
\ifnum \wd \mpr@hlist > 0


206 
\mpr@htovlist


207 
\mpr@tmpdim \wd0


208 
\fi


209 
\setbox \mpr@hlist \hbox {\unhbox0}%


210 
\fi


211 
\advance \mpr@tmpdim by \mpr@sep


212 
\fi


213 
}%


214 
\@rev


215 
\mpr@htovlist


216 
\ifmpr@center \hskip \wd\mpr@vlist\fi \box \mpr@vlist


217 
\fi


218 
\egroup


219 
}


220 


221 
%%% INFERENCE RULES


222 


223 
\@ifundefined{@@over}{%


224 
\let\@@over\over % fallback if amsmath is not loaded


225 
\let\@@overwithdelims\overwithdelims


226 
\let\@@atop\atop \let\@@atopwithdelims\atopwithdelims


227 
\let\@@above\above \let\@@abovewithdelims\abovewithdelims


228 
}{}


229 


230 
%% The default


231 


232 
\def \mpr@@fraction #1#2{\hbox {\advance \hsize by 0.5em


233 
$\displaystyle {#1\mpr@over #2}$}}


234 
\let \mpr@fraction \mpr@@fraction


235 


236 
%% A generic solution to arrow


237 


238 
\def \mpr@make@fraction #1#2#3#4#5{\hbox {%


239 
\def \mpr@tail{#1}%


240 
\def \mpr@body{#2}%


241 
\def \mpr@head{#3}%


242 
\setbox1=\hbox{$#4$}\setbox2=\hbox{$#5$}%


243 
\setbox3=\hbox{$\mkern 3mu\mpr@body\mkern 3mu$}%


244 
\setbox3=\hbox{$\mkern 3mu \mpr@body\mkern 3mu$}%


245 
\dimen0=\dp1\advance\dimen0 by \ht3\relax\dp1\dimen0\relax


246 
\dimen0=\ht2\advance\dimen0 by \dp3\relax\ht2\dimen0\relax


247 
\setbox0=\hbox {$\box1 \@@atop \box2$}%


248 
\dimen0=\wd0\box0


249 
\box0 \hskip \dimen0\relax


250 
\hbox to \dimen0 {$%


251 
\mathrel{\mpr@tail}\joinrel


252 
\xleaders\hbox{\copy3}\hfil\joinrel\mathrel{\mpr@head}%


253 
$}}}


254 


255 
%% Old stuff should be removed in next version


256 
\def \mpr@@reduce #1#2{\hbox


257 
{$\lower 0.01pt \mpr@@fraction {#1}{#2}\mkern 15mu\rightarrow$}}


258 
\def \mpr@@rewrite #1#2#3{\hbox


259 
{$\lower 0.01pt \mpr@@fraction {#2}{#3}\mkern 8mu#1$}}


260 
\def \mpr@infercenter #1{\vcenter {\mpr@hovbox{T}{#1}}}


261 


262 
\def \mpr@empty {}


263 
\def \mpr@inferrule


264 
{\bgroup


265 
\ifnum \linewidth<\hsize \hsize \linewidth\fi


266 
\mpr@rulelineskip


267 
\let \and \qquad


268 
\let \hva \mpr@hva


269 
\let \@rulename \mpr@empty


270 
\let \@rule@options \mpr@empty


271 
\let \mpr@over \@@over


272 
\mpr@inferrule@}


273 
\newcommand {\mpr@inferrule@}[3][]


274 
{\everymath={\displaystyle}%


275 
\def \@test {#2}\ifx \empty \@test


276 
\setbox0 \hbox {$\vcenter {\mpr@hovbox{B}{#3}}$}%


277 
\else


278 
\def \@test {#3}\ifx \empty \@test


279 
\setbox0 \hbox {$\vcenter {\mpr@hovbox{T}{#2}}$}%


280 
\else


281 
\setbox0 \mpr@fraction {\mpr@hovbox{T}{#2}}{\mpr@hovbox{B}{#3}}%


282 
\fi \fi


283 
\def \@test {#1}\ifx \@test\empty \box0


284 
\else \vbox


285 
%%% Suggestion de Francois pour les etiquettes longues


286 
%%% {\hbox to \wd0 {\RefTirName {#1}\hfil}\box0}\fi


287 
{\hbox {\RefTirName {#1}}\box0}\fi


288 
\egroup}


289 


290 
\def \mpr@vdotfil #1{\vbox to #1{\leaders \hbox{$\cdot$} \vfil}}


291 


292 
% They are two forms


293 
% \inferrule [label]{[premisses}{conclusions}


294 
% or


295 
% \inferrule* [options]{[premisses}{conclusions}


296 
%


297 
% Premisses and conclusions are lists of elements separated by \\


298 
% Each \\ produces a break, attempting horizontal breaks if possible,


299 
% and vertical breaks if needed.


300 
%


301 
% An empty element obtained by \\\\ produces a vertical break in all cases.


302 
%


303 
% The former rule is aligned on the fraction bar.


304 
% The optional label appears on top of the rule


305 
% The second form to be used in a derivation tree is aligned on the last


306 
% line of its conclusion


307 
%


308 
% The second form can be parameterized, using the key=val interface. The


309 
% folloiwng keys are recognized:


310 
%


311 
% width set the width of the rule to val


312 
% narrower set the width of the rule to val\hsize


313 
% before execute val at the beginning/left


314 
% lab put a label [Val] on top of the rule


315 
% lskip add negative skip on the right


316 
% left put a left label [Val]


317 
% Left put a left label [Val], ignoring its width


318 
% right put a right label [Val]


319 
% Right put a right label [Val], ignoring its width


320 
% leftskip skip negative space on the lefthand side


321 
% rightskip skip negative space on the righthand side


322 
% vdots lift the rule by val and fill vertical space with dots


323 
% after execute val at the end/right


324 
%


325 
% Note that most options must come in this order to avoid strange


326 
% typesetting (in particular leftskip must preceed left and Left and


327 
% rightskip must follow Right or right; vdots must come last


328 
% or be only followed by rightskip.


329 
%


330 


331 
%% Keys that make sence in all kinds of rules


332 
\def \mprset #1{\setkeys{mprset}{#1}}


333 
\define@key {mprset}{flushleft}[]{\mpr@centerfalse}


334 
\define@key {mprset}{center}[]{\mpr@centertrue}


335 
\define@key {mprset}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite}


336 
\define@key {mprset}{myfraction}[]{\let \mpr@fraction #1}


337 
\define@key {mprset}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}}


338 


339 
\newbox \mpr@right


340 
\define@key {mpr}{flushleft}[]{\mpr@centerfalse}


341 
\define@key {mpr}{center}[]{\mpr@centertrue}


342 
\define@key {mpr}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite}


343 
\define@key {mpr}{myfraction}[]{\let \mpr@fraction #1}


344 
\define@key {mpr}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}}


345 
\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax


346 
\advance \hsize by \wd0\box0}


347 
\define@key {mpr}{width}{\hsize #1}


348 
\define@key {mpr}{sep}{\def\mpr@sep{#1}}


349 
\define@key {mpr}{before}{#1}


350 
\define@key {mpr}{lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}


351 
\define@key {mpr}{Lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}


352 
\define@key {mpr}{narrower}{\hsize #1\hsize}


353 
\define@key {mpr}{leftskip}{\hskip #1}


354 
\define@key {mpr}{reduce}[]{\let \mpr@fraction \mpr@@reduce}


355 
\define@key {mpr}{rightskip}


356 
{\setbox \mpr@right \hbox {\unhbox \mpr@right \hskip #1}}


357 
\define@key {mpr}{LEFT}{\setbox0 \hbox {$#1$}\relax


358 
\advance \hsize by \wd0\box0}


359 
\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax


360 
\advance \hsize by \wd0\box0}


361 
\define@key {mpr}{Left}{\llap{$\TirName {#1}\;$}}


362 
\define@key {mpr}{right}


363 
{\setbox0 \hbox {$\;\TirName {#1}$}\relax \advance \hsize by \wd0


364 
\setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}


365 
\define@key {mpr}{RIGHT}


366 
{\setbox0 \hbox {$#1$}\relax \advance \hsize by \wd0


367 
\setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}


368 
\define@key {mpr}{Right}


369 
{\setbox \mpr@right \hbox {\unhbox \mpr@right \rlap {$\;\TirName {#1}$}}}


370 
\define@key {mpr}{vdots}{\def \mpr@vdots {\@@atop \mpr@vdotfil{#1}}}


371 
\define@key {mpr}{after}{\edef \mpr@after {\mpr@after #1}}


372 


373 
\newdimen \rule@dimen


374 
\newcommand \mpr@inferstar@ [3][]{\setbox0


375 
\hbox {\let \mpr@rulename \mpr@empty \let \mpr@vdots \relax


376 
\setbox \mpr@right \hbox{}%


377 
$\setkeys{mpr}{#1}%


378 
\ifx \mpr@rulename \mpr@empty \mpr@inferrule {#2}{#3}\else


379 
\mpr@inferrule [{\mpr@rulename}]{#2}{#3}\fi


380 
\box \mpr@right \mpr@vdots$}


381 
\setbox1 \hbox {\strut}


382 
\rule@dimen \dp0 \advance \rule@dimen by \dp1


383 
\raise \rule@dimen \box0}


384 


385 
\def \mpr@infer {\@ifnextchar *{\mpr@inferstar}{\mpr@inferrule}}


386 
\newcommand \mpr@err@skipargs[3][]{}


387 
\def \mpr@inferstar*{\ifmmode


388 
\let \@do \mpr@inferstar@


389 
\else


390 
\let \@do \mpr@err@skipargs


391 
\PackageError {mathpartir}


392 
{\string\inferrule* can only be used in math mode}{}%


393 
\fi \@do}


394 


395 


396 
%%% Exports


397 


398 
% Envirnonment mathpar


399 


400 
\let \inferrule \mpr@infer


401 


402 
% make a short name \infer is not already defined


403 
\@ifundefined {infer}{\let \infer \mpr@infer}{}


404 


405 
\def \TirNameStyle #1{\small \textsc{#1}}


406 
\def \tir@name #1{\hbox {\small \TirNameStyle{#1}}}


407 
\let \TirName \tir@name


408 
\let \DefTirName \TirName


409 
\let \RefTirName \TirName


410 


411 
%%% Other Exports


412 


413 
% \let \listcons \mpr@cons


414 
% \let \listsnoc \mpr@snoc


415 
% \let \listhead \mpr@head


416 
% \let \listmake \mpr@makelist


417 


418 


419 


420 


421 
\endinput
