%infrule.sty
%99-05-07 (from M. Hofmann)

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%                                                                   %%%
%%%        BCP's latex tricks for typesetting inference rules         %%%
%%%                                                                   %%%
%%%                         Version 1.3                               %%%
%%%                                                                   %%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%
%%% This package supports two styles of rules: named and unnamed.  
%%% Unnamed rules are centered on the page.  Named rules are set so
%%% that a series of them will have the rules centered in a vertical
%%% column taking most of the page and the labels right-justified.
%%% When a label would overlap its rule, the label is moved down.  
%%% 
%%% The width of the column of labels can be varied using a command of the
%%% form 
%%% 
%%%   \typicallabel{T-Arrow-I}
%%% 
%%% The default setting is:
%%%
%%%   \typicallabel{}
%%%
%%% In other words, the column of rules takes up the whole width of
%%% the page: rules are centered on the centerline of the text, and no
%%% extra space is left for the labels.
%%%
%%% The minimum distance between a rule and its label can be altered by a
%%% command of the form
%%% 
%%%   \setlength{\labelminsep}{0.5em}
%%% 
%%% (This is the default value.)
%%% 
%%% Examples:
%%% 
%%% An axiom with a label in the right-hand column:
%%% 
%%%   \infax[The name]{x - x = 0}
%%% 
%%% An inference rule with a name:
%%% 
%%%   \infrule[Another name]
%%%     {\mbox{false}}
%%%     {x - x = 1}
%%% 
%%% A rule with multiple premises on the same line:
%%% 
%%%   \infrule[Wide premises]
%%%     {x > 0  \andalso y > 0  \andalso z > 0}
%%%     {x + y + z > 0}
%%%   
%%% A rule with several lines of premises:
%%% 
%%%   \infrule[Long premises]
%%%     {x > 0  \\ y > 0  \\ z > 0}
%%%     {x + y + z > 0}
%%%   
%%% A rule without a name, but centered on the same vertical line as rules
%%% and axioms with names:
%%% 
%%%   \infrule[]
%%%     {x - y = 5}
%%%     {y - x = -5}
%%% 
%%% A rule without a name, centered on the page:
%%% 
%%%   \infrule
%%%     {x = 5}
%%%     {x - 1 > 0}
%%%
%%%
%%% Setting the flag \indexrulestrue causes an index entry to be 
%%% generated for each named rule.
%%%
%%% Setting the flag \suppressrulenamestrue causes the names of all rules
%%% to be left blank
%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%% The font for setting inference rule names
\newcommand{\rn}[1]{%
  \ifmmode 
    \mathchoice
      {\mbox{\sc #1}}
      {\mbox{\sc #1}}
      {\mbox{\small\sc #1}}
      {\mbox{\tiny\uppercase{#1}}}%
  \else
    {\mbox{\sc #1}}%
  \fi}

\newif\ifsuppressrulenames  
\suppressrulenamesfalse

\newif\ifbcprulessavespace
\bcprulessavespacefalse

%%% How to display a rule's name to the right of the rule
\newcommand{\inflabel}[1]{%
  \ifsuppressrulenames\else
    \def\lab{#1}%
    \ifx\lab\empty
      \relax
    \else
      (\rn{\lab})%
  \fi\fi
}

%%% Amount of extra space to add before and after a rule
\newlength{\afterruleskip}
\setlength{\afterruleskip}{\bigskipamount}

%%% Minimum distance between a rule and its label
\newlength{\labelminsep}
\setlength{\labelminsep}{0.2em}

%%% The ``typical'' width of the column of labels: labels are allowed
%%% to project further to the left if necessary; the rules will be
%%% centered in a column of width \linewidth - \labelcolwidth
\newdimen\labelcolwidth

%%% Set the label column width by providing a ``typical'' label --
%%% i.e. a label of average length
\newcommand{\typicallabel}[1]{
  \setbox \@tempboxa \hbox{\inflabel{#1}}
  \labelcolwidth \wd\@tempboxa
  }
\typicallabel{}

%%% A flag controlling generation of index entries
\newif  \ifindexrules   \indexrulesfalse

%%% Allocate some temporary registers
\newbox\labelbox
\newbox\rulebox
\newdimen\ruledim
\newdimen\labeldim

%%% Put a rule and its label on the same line if this can be done
%%% without overlapping them; otherwise, put the label on the next
%%% line.  Put a small amount of vertical space above and below.
\newcommand{\layoutruleverbose}[2]%
  {\unvbox\voidb@x  % to make sure we're in vmode
   \vspace{\afterruleskip}%

   \setbox \rulebox \hbox{$\displaystyle #2$}

   \setbox \labelbox \hbox{#1}
   \ruledim \wd \rulebox
   \labeldim \wd \labelbox

   %%% Will it all fit comfortably on one line?
   \@tempdima \linewidth
   \advance \@tempdima -\labelcolwidth
   \ifdim \@tempdima < \ruledim
     \@tempdima \ruledim
   \else
     \advance \@tempdima by \ruledim
     \divide \@tempdima by 2
   \fi
   \advance \@tempdima by \labelminsep
   \advance \@tempdima by \labeldim
   \ifdim \@tempdima < \linewidth
     % Yes, everything fits on a line
     \@tempdima \linewidth
     \advance \@tempdima -\labelcolwidth
     \hbox to \linewidth{%
       \hbox to \@tempdima{%
         \hfil
         \box\rulebox
         \hfil}%
       \hfil
       \hbox to 0pt{\hss\box\labelbox}%
     }
   \else
     % No, better put the label on the next line
     \@tempdima \linewidth
     \advance \@tempdima -\labelcolwidth
     \hbox to \linewidth{%
       \hbox to \@tempdima{%
          \hfil
          \box\rulebox
          \hfil}
       \hfil}%
     \penalty10000
     \hbox to \linewidth{%
         \hfil
         \box\labelbox}
   \fi

   \vspace{\afterruleskip}%
   \@doendpe  % use LaTeX's trick of inhibiting paragraph indent for
              % text immediately following a rule
   \ignorespaces
   }

% Alternate form, for when we need to save space
\newcommand{\layoutruleterse}[2]%
  {$\displaystyle #2$ \hspace{\labelminsep} #1
   }

%%% Select low-level layout driver based on \bcprulessavespace flag
\newcommand{\layoutrule}[2]{%
  \ifbcprulessavespace 
    \layoutruleterse{#1}{#2}
  \else
    \layoutruleverbose{#1}{#2}
  \fi   
}

%%% Commands for setting axioms and rules
\newcommand{\typesetax}[1]{
    \begin{array}{@{}c@{}}#1\end{array}}
\newcommand{\typesetrule}[2]{
    \frac{\begin{array}{@{}c@{}}#1\end{array}}
         {\begin{array}{@{}c@{}}#2\end{array}} }

%%% Indexing
\newcommand{\maybeindex}[1]{\ifindexrules\index{#1@\rn{#1}}\fi}

%%% Setting axioms, with or without names
\def\infax{\@ifnextchar[{\@infaxy}{\@infaxx}}
\def\@infaxx#1{%
  \ifbcprulessavespace $\typesetax{#1}$
  \else $$\typesetax{#1}$$
  \fi}
\def\@infaxy[#1]{\maybeindex{#1}\@infax{\inflabel{#1}}}
\def\@infax#1#2{\layoutrule{#1}{\typesetax{#2}}}

%%% Setting rules, with or without names
\def\infrule{\@ifnextchar[{\@infruley}{\@infrulex}}
\def\@infrulex#1#2{%
  \ifbcprulessavespace $\typesetrule{#1}{#2}$%
  \else $$\typesetrule{#1}{#2}$$%
  \fi}
\def\@infruley[#1]{\maybeindex{#1}\@infrule{\inflabel{#1}}}
\def\@infrule#1#2#3{\layoutrule{#1}{\typesetrule{#2}{#3}}}

%%% Miscellaneous helpful definitions
\newcommand{\andalso}{\quad\quad}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%% Commands added by mh for reverse compatibility     %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\unnamedinfax}[1]{\infax{#1}}
\newcommand{\unnamedinfrule}[2]{\infrule{#1}{#2}}

