%% %% This is file `mathpartir.sty', %% generated with the docstrip utility. %% %% The original source files were: %% %% mathpartir.dtx (with options: `package') %% %% This is a generated file. %% %% Copyright (C) 2015 by Didier Remy %% %% This file is part of mathpartir. %% %% 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 of the License, 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. %% %% You should have received a copy of the GNU General Public License %% along with mathpartir. If not, see . %% \NeedsTeXFormat{LaTeX2e} \ProvidesPackage{mathpartir} [2016/02/24 version 1.3.2 Math Paragraph for Typesetting Inference Rules] %% Identification %% Preliminary declarations \RequirePackage {keyval} %% Options %% More declarations %% PART I: Typesetting maths in paragraphe mode %% \newdimen \mpr@tmpdim %% Dimens are a precious ressource. Uses seems to be local. \let \mpr@tmpdim \@tempdima \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 \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} \newenvironment{mathparpagebreakable}[1][] {\begingroup \par \mpr@savepar \parskip 0em \hsize \linewidth \centering \mpr@prebindings \mpr@paroptions #1% \vskip \abovedisplayskip \vskip -\lineskip% \ifmmode \else $\displaystyle\fi \MathparBindings } {\unskip \ifmmode $\fi \par\endgroup \vskip \belowdisplayskip \noindent \ignorespacesafterend} %%% 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@vskip {} \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 \ifx \mpr@vskip \empty \else \hrule height 0em depth \mpr@vskip width 0em \fi \unvbox \mpr@vlist \else \unvbox \mpr@vlist \ifx \mpr@vskip \empty \else \hrule height 0em depth \mpr@vskip width 0em \fi \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}$}} \def \mpr@@nofraction #1#2{\hbox {\advance \hsize by -0.5em $\displaystyle {#1\@@atop #2}$}} \let \mpr@fraction \mpr@@fraction %% A generic solution to arrow \def \mpr@@fractionaboveskip {0ex} \def \mpr@@fractionbelowskip {0.22ex} \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$}% \dimen0\ht3\advance\dimen0 by \dp3\relax \dimen0 0.5\dimen0\relax \advance \dimen0 by \mpr@@fractionaboveskip \setbox1=\hbox {\raise \dimen0 \box1}\relax \dimen0 -\dimen0\advance \dimen0 \mpr@@fractionaboveskip\dimen0 -\dimen0 \advance \dimen0 by \mpr@@fractionbelowskip \setbox2=\hbox {\lower \dimen0 \box2}\relax \setbox0=\hbox {$\displaystyle {\box1 \atop \box2}$}% \dimen0=\wd0\box0 \box0 \hskip -\dimen0\relax \hbox to \dimen0 {$%\color{blue} \mathrel{\mpr@tail}\joinrel \xleaders\hbox{\copy3}\hfil\joinrel\mathrel{\mpr@head}% $}}} %% Old stuff should be removed in next version \def \mpr@@nothing #1#2 {$\lower 0.01pt \mpr@@nofraction {#1}{#2}$} \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 {\DefTirName {#1}}\box0}\fi \egroup} \def \mpr@vdotfil #1{\vbox to #1{\leaders \hbox{$\cdot$} \vfil}} %% Keys that make sence in all kinds of rules \def \mprset #1{\setkeys{mprset}{#1}} \define@key {mprset}{andskip}[]{\mpr@andskip=#1} \define@key {mprset}{lineskip}[]{\lineskip=#1} \define@key {mprset}{lessskip}[]{\lineskip=0.5\lineskip} \define@key {mprset}{flushleft}[]{\mpr@centerfalse} \define@key {mprset}{center}[]{\mpr@centertrue} \define@key {mprset}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite} \define@key {mprset}{atop}[]{\let \mpr@fraction \mpr@@nofraction} \define@key {mprset}{myfraction}[]{\let \mpr@fraction #1} \define@key {mprset}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}} \define@key {mprset}{defaultfraction}[]{\let \mpr@fraction \mpr@@fraction} \define@key {mprset}{sep}{\def\mpr@sep{#1}} \define@key {mprset}{fractionaboveskip}{\def\mpr@@fractionaboveskip{#1}} \define@key {mprset}{fractionbelowskip}{\def\mpr@@fractionbelowskip{#1}} \define@key {mprset}{style}[1]{\def\TirNameStyle{#1}def} \define@key {mprset}{rightstyle}[1]{\def\RightTirNameStyle{#1}} \define@key {mprset}{leftstyle}[1]{\def\LeftTirNameStyle{#1}} \define@key {mprset}{vskip}[1]{\def \mpr@vskip{#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}{width}{\hsize #1} \define@key {mpr}{sep}{\def\mpr@sep{#1}} \define@key {mpr}{before}{#1} \define@key {mpr}{lab}{\let \DefTirName \LabTirName \def \mpr@rulename {#1}} \define@key {mpr}{Lab}{\let \DefTirName \LabTirName \def \mpr@rulename {#1}} \define@key {mpr}{style}[1]{\def\TirNameStyle{#1}def} \define@key {mpr}{rightstyle}[1]{\def\RightTirNameStyle{#1}} \define@key {mpr}{leftstyle}[1]{\def\LeftTirNameStyle{#1}} \define@key {mpr}{vskip}[1]{\def \mpr@vskip{#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 {$\LeftTirName {#1}\;$}\relax \advance \hsize by -\wd0\box0} \define@key {mpr}{Left}{\llap{$\LeftTirName {#1}\;$}} \define@key {mpr}{right} {\setbox0 \hbox {$\;\RightTirName {#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 {$\;\RightTirName {#1}$}}} \define@key {mpr}{vdots}{\def \mpr@vdots {\@@atop \mpr@vdotfil{#1}}} \define@key {mpr}{after}{\edef \mpr@after {\mpr@after #1}} \define@key {mpr}{vcenter}[]{\mpr@vcentertrue} \newif \ifmpr@vcenter \mpr@vcenterfalse \newcommand \mpr@inferstar@ [3][]{\begingroup \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$ \ifmpr@vcenter \aftergroup \mpr@vcentertrue \fi} \ifmpr@vcenter \box0 \else \setbox1 \hbox {\strut} \@tempdima \dp0 \advance \@tempdima by -\dp1 \raise \@tempdima \box0 \fi \endgroup} \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 \let \inferrule \mpr@infer \@ifundefined {infer}{\let \infer \mpr@infer}{} \def \TirNameStyle #1{\small \textsc{#1}} \def \LeftTirNameStyle #1{\TirNameStyle {#1}} \def \RightTirNameStyle #1{\TirNameStyle {#1}} \def \lefttir@name #1{\hbox {\small \LeftTirNameStyle{#1}}} \def \righttir@name #1{\hbox {\small \RightTirNameStyle{#1}}} \let \TirName \lefttir@name \let \LeftTirName \lefttir@name \let \DefTirName \lefttir@name \let \LabTirName \lefttir@name \let \RightTirName \righttir@name %%% Other Exports \endinput %% %% End of file `mathpartir.sty'.