%  Mathpartir --- Math Paragraph for Typesetting Inference Rules

 %

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

 %

 %  Author         : Didier Remy 

 %  Version        : 1.2.0

 %  Bug Reports    : to author

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

 % 

 %  Mathpartir 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}

     [2005/12/20 version 1.2.0 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

 }

 \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}

 %% Part III -- Type inference rules

 \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@item #1{$\displaystyle #1$}

 \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 T 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{\mpr@item {##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

   }{}

 %% The default

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

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

 \let \mpr@fraction \mpr@@fraction

 %% A generic solution to arrow

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

      \def \mpr@tail{#1}%

      \def \mpr@body{#2}%

      \def \mpr@head{#3}%

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

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

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

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

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

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

      \dimen0=\wd0\box0

      \box0 \hskip -\dimen0\relax

      \hbox to \dimen0 {$%

        \mathrel{\mpr@tail}\joinrel

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

      $}}}

 %% Old stuff should be removed in next version

 \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

      \let \mpr@over \@@over

      \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. 

 %  

 %% Keys that make sence in all kinds of rules

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

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

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

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

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

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

 \newbox \mpr@right

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

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

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

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

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

 \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 \TirNameStyle #1{\small \textsc{#1}}

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

 \let \TirName \tir@name

 \let \DefTirName \TirName

 \let \RefTirName \TirName

 %%% Other Exports

 % \let \listcons \mpr@cons

 % \let \listsnoc \mpr@snoc

 % \let \listhead \mpr@head

 % \let \listmake \mpr@makelist

 \endinput