UniTO/tesi/mathpartir.sty
2024-10-29 09:11:05 +01:00

469 lines
16 KiB
TeX
Executable file

%%
%% 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, 2020 by Didier Remy <didier.remy(at)inria(dot)fr>
%%
%% 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 <http://www.gnu.org/licenses/>.
%%
\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{mathpartir}
[2020/02/15 version 1.4.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
%% 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
\def \MathparBeginhook {}
\def \MathparEndhook {}
\let \MathparCentering \centering
\newenvironment{mathpar}[1][]
{$$
\MathparBeginhook
%% We save \lineskip parameters so that the user can restore them
%% inside math \MathparNormalpar
\mpr@savepar
%% We define the shape of the paragrah
\parskip 0em \hsize \linewidth \MathparCentering
\vbox \bgroup \mpr@prebindings \mpr@paroptions #1\ifmmode $\else
\noindent $\displaystyle\fi
\MathparBindings}
{\MathparEndhook \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 {}
\let \mpr@vbox \vbox
\def \mpr@htovlist {%
\setbox \mpr@hlist
\hbox {\strut
\ifmpr@center \hskip -0.5\wd\mpr@hlist\fi
\unhbox \mpr@hlist}%
\setbox \mpr@vlist
\mpr@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
\def \@test {#3}\ifx \empty \@test
\PackageWarning {mathpartir}
{\string\inferrule\space empty arguments substituted}{}%
\setbox0 \mpr@fraction {?}{?}%
\else
\setbox0 \hbox {$\vcenter {\mpr@hovbox{B}{#3}}$}%
\fi
\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}}
%% Version for Hoare triples
\def \triple@hlinebox{\noalign{\setbox0\hbox {}\dp0 0.1ex\ht0 0.1ex\box0}}
\def \triple@hline {\triple@hlinebox\hline\triple@hlinebox}
\newcommand{\triplerule}[4][]
{\bgroup
\ifnum \linewidth<\hsize \hsize \linewidth\fi
\mpr@rulelineskip
\let \and \qquad
\let \hva \mpr@hva
\setbox0 \hbox {\begin{array}[b]{@{}c@{}}
\mpr@hovbox{T}{#2}\cr\triple@hline
\mpr@hovbox{T}{#3}\cr\triple@hline
\let \mpr@vbox \vtop \ht0 0em
\setbox0 \strut \@tempdima \ht0
\setbox0 \mpr@hovbox{B}{#4}\advance \@tempdima by -\ht0
\setbox0 \hbox{\raise \@tempdima \box0}\box0
\end{array}}%
\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}
%% 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'.