%  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