%%%%%%%%  Copyright 1990 J. C. Bradfield
%%%%%%%%  This file may be freely distributed and modified
% Version 2.1 dated 12/02/90
%  permit \ProofTreespace to be assigned between the consequents
%  of a ii rule (not yet a iii rule) to have local effect
% Version 2.0 dated 05/02/90
%  annotated rules added. \ProofTreerulestrut added.
%  \tree no longer unboxes (this should have gone with the silly
%  format). Add \ProofTreedopremise.
% Version 1.0 dated 31/01/90
% macros for proof trees
% Usage: \tree{TREE} where TREE ::= \PTaxiom{TEXT} |
% \PTirule{TEXT}{TREE} | \PTiirule{TEXT}{TREE}{TREE}
% | \PTiiirule{TEXT}{TREE}{TREE}{TREE}
% Also \aPTirule{ANNOTATION}{TEXT}{TREE} etc., where the annotation
% appears to the right of the rule.
% Spaces, but nothing else, are permitted between arguments.

% Parameters: \ProofTreespace is the space between conclusions
% \ProofTreeannotspace is the space between rule and annotation (0pt)
% (default 1em) ; \ProofTreebias is an integer from 0 (left) to 
% 100 (right) (default 50) determining the centring of trees; 
% \ProofTreeovershoot (0.1em) is the amount lines overhang text
% \ProofTreestrut and \ProofTreerulestrut are struts put in each
% premise and rule respectively. Default to 10.5pt+4.5pt and 0pt+0pt
% \ProofTreedopremise is a one argument macro that can be used to 
%  transform premise: each premise has this applied to it before being
%  typeset.
% to skip by \ProofTreebias and 100 -\ProofTreebias fil
\newcount\ProofTreebias \ProofTreebias=50
\newdimen\ProofTreeovershoot \ProofTreeovershoot=0.1em % amount by which
						     % rule overhangs
						     % text
\newdimen\ProofTreeannotspace \ProofTreeannotspace=0pt
\def\ProofTreestrut{\vrule depth 4.5pt height 10.5pt width 0pt }
\def\ProofTreerulestrut{\vrule depth 0pt height 0pt width 0pt }
\newbox\ProofTree\newskip\ProofTreespace\ProofTreespace=1em
\newdimen\ProofTreea\newdimen\ProofTreeb\newdimen\ProofTreec
\def\ProofTreedopremise#1{#1}
\def\PTirule{\aPTirule{\hskip-\ProofTreeannotspace}}
\def\PTiirule{\aPTiirule{\hskip-\ProofTreeannotspace}}
\def\PTiiirule{\aPTiiirule{\hskip-\ProofTreeannotspace}}
% utilities
%% swallow spaces until left brace then execute arg, swallowing the
%% brace itself
\def\gobblebrace#1{%
\def\gobblearg{#1}%
\afterassignment\agobblebrace\let\gobblething= }

\def\agobblebrace{%
\ifx\gobblething\ProofTreespace % local spacing required
\let\next=\setskip
\else
\ifcat\bgroup\noexpand\gobblething
\let\next=\gobblearg
\else
\ifcat\space\noexpand\gobblething
\let\next=\bgobblebrace
\else
\def\next{\errmessage
{I was expecting optional spaces followed by a left
brace!}}%
\fi\fi\fi\next}
\def\bgobblebrace{\afterassignment\agobblebrace\let\gobblething=}
\def\setskip{\afterassignment\bgobblebrace\skip255}

% two conclusion rule. sets \box\ProofTree to a box  in the format used internally

\def\doannot#1{\setbox0=\vbox to 0pt{\vss\hbox{#1}\vss}}
%\def\doannot#1{\setbox0=\hbox{\hskip\ProofTreeannotspace$\smash{\vcenter{\hbox{$\hbox{#1}$}}}$}}
\def\aPTiirule#1#2{%
\begingroup
% \box0 holds the annotation.
% box 1 and 2 will hold the subtrees,
% dimen 1,2,3 and 4,5,6 the abc.
%type set the premise first so that recursive descent numbers the
% nodes correctly
% and the annotation.
% Annotation should be a box of zero height and depth, with 
% the math axis on the ref point.
\doannot{#1}
\setbox7=\hbox{\ProofTreestrut\ProofTreedopremise{#2}}\setbox8=\copy7
%set the conclusions
\gobblebrace{\bgroup\aftergroup\aPTiirulepartb}}

\def\aPTiirulepartb{%
\setbox1=\box\ProofTree
\dimen1=\ProofTreea \dimen2=\ProofTreeb \dimen3=\ProofTreec
\skip255=\ProofTreespace % save default
\gobblebrace{\bgroup\aftergroup\aPTiirulepartc}}

\def\aPTiirulepartc{%
% set local space
\ProofTreespace=\skip255
\setbox2=\box\ProofTree
\dimen4=\ProofTreea \dimen5=\ProofTreeb \dimen6=\ProofTreec
%
\dimen0=\wd1
\advance\dimen0 -\dimen1
\advance\dimen0 -\dimen2
\advance\dimen0 \ProofTreespace
\advance\dimen0 \dimen4
\advance\dimen0 \dimen5
\advance\dimen0 \dimen6
% that's the width of the rule if the premise is short: recall we have
% the premise in box7
% is the premise shorter than the rule so far?
\ifnum\wd7 <\dimen0
% OK, so premise is shorter--set \dimen9 to offset of rule wrt box
\dimen9=\dimen1
\advance\dimen9 \dimen2
\global\ProofTreea=\dimen9
% calculate offset of premise wrt rule
\ProofTreeb=\dimen0
\advance\ProofTreeb -\wd7
\divide\ProofTreeb 100
\multiply\ProofTreeb \ProofTreebias
\global\ProofTreeb=\ProofTreeb
% now rebox premise to size of rule
\setbox7=\hbox to\dimen0{\hskip\ProofTreeb\box7\hfil}
\else % premise is longer than rule
% calculate excess of premise over rule
\advance\dimen0 -\wd7
% reduce the offset of the rule wrt box by the excess
% adjusted by bias
\divide\dimen0 100 \multiply\dimen0 \ProofTreebias
\dimen9=\dimen1
\advance\dimen9 \dimen2
\advance\dimen9 \dimen0
%if \dimen 9 is negative, then
%as far as the outside world is concerned, the offset of the rule wrt
%box is zero (cos now our premise delimits the box!)--so see a bit later
\global\ProofTreea=\dimen9
% and no offset for premise wrt rule
\dimen0=\wd7
\global\ProofTreeb=0pt
\fi
% if the offset of the rule wrt box is negative, move the whole
% shebang right by that amount
\ifnum\dimen9 <0
\dimen8=-\dimen9
\global\ProofTreea=0pt
\else
\dimen8=0pt
\fi
\global\ProofTreec=\wd8
% and return result
\global\setbox\ProofTree=\vtop{\offinterlineskip\halign
{\hskip\dimen8 ##\cr
\hskip\dimen9\box7\hfil\cr
\ProofTreerulestrut\hskip\dimen9\hskip-\ProofTreeovershoot\advance\dimen0 2\ProofTreeovershoot
\vrule width\dimen0 depth0pt height 0.4pt\hskip\ProofTreeannotspace\box0\hskip-\ProofTreeovershoot
\hfil\cr
\box1\hskip\ProofTreespace\box2\hfil\cr}}%
\endgroup}%

\def\PTaxiom#1{\global\setbox\ProofTree=\vtop{\hbox{\ProofTreestrut\ProofTreedopremise{#1}}}%
\global\ProofTreea=0pt\global\ProofTreeb=0pt\global\ProofTreec=\wd\ProofTree
}

\def\aPTirule#1#2{
\begingroup
\doannot{#1}
\setbox7=\hbox{\ProofTreestrut\ProofTreedopremise{#2}}\setbox8=\copy7
\gobblebrace{\bgroup\aftergroup\aPTirulepartb}}
\def\aPTirulepartb{%
% Box 1 contains the subtree
% Dimen 1,2,3 contain ProofTreea,b,c
\setbox1=\box\ProofTree
\dimen1=\ProofTreea \dimen2=\ProofTreeb \dimen3=\ProofTreec
%
\dimen0=\dimen3 % width of rule
\ifnum\wd7 <\dimen0
% premise shorter than rule
% offset of rule wrt box
\dimen9=\dimen1
\advance\dimen9 \dimen2
\global\ProofTreea=\dimen9
% offset of premise wrt rule
\ProofTreeb=\dimen0
\advance\ProofTreeb -\wd7
\divide\ProofTreeb 100
\multiply\ProofTreeb \ProofTreebias
\global\ProofTreeb=\ProofTreeb
% now rebox premise to size of rule
\setbox7=\hbox to\dimen0{\hskip\ProofTreeb\box7\hfil}
\else
% of rule wrt box
% calculate excess of premise over rule
\advance\dimen0 -\wd7
% reduce the offset of the rule wrt box by the excess
% adjusted by bias
\divide\dimen0 100 \multiply\dimen0 \ProofTreebias
\dimen9=\dimen1
\advance\dimen9 \dimen2
\advance\dimen9 \dimen0
\global\ProofTreea=\dimen9
% and no offset for premise wrt rule
\dimen0=\wd7
\global\ProofTreeb=0pt
\fi
% if the offset of the rule wrt box is negative, move the whole
% Shebang right by that amount
\ifnum\dimen9 <0
\dimen8=-\dimen9
\global\ProofTreea=0pt
\else
\dimen8=0pt
\fi
\global\ProofTreec=\wd8 % width of premise
\global\setbox\ProofTree=\vtop{\offinterlineskip\halign
{\hskip\dimen8 ##\cr
\hskip\dimen9\box7\hfil\cr
\ProofTreerulestrut\hskip\dimen9\hskip-\ProofTreeovershoot\advance\dimen0 2\ProofTreeovershoot
\vrule width\dimen0 depth0pt height 0.4pt \hskip\ProofTreeannotspace\box0\hskip-\ProofTreeovershoot
\hfil\cr\box1\hfil\cr}}%
\endgroup}%

% and a three conclusion rule
\def\aPTiiirule#1#2{%
\begingroup
% same assignment as for iirule, plus box3 as the middle conclusion
\doannot{#1}
\setbox7=\hbox{\ProofTreestrut\ProofTreedopremise{#2}}\setbox8=\copy7
\gobblebrace{\bgroup\aftergroup\aPTiiirulepartb}}

\def\aPTiiirulepartb{%
\setbox1=\box\ProofTree
\dimen1=\ProofTreea \dimen2=\ProofTreeb \dimen3=\ProofTreec
\gobblebrace{\bgroup\aftergroup\aPTiiirulepartc}}

\def\aPTiiirulepartc{%
\setbox3=\box\ProofTree
\gobblebrace{\bgroup\aftergroup\aPTiiirulepartd}}

\def\aPTiiirulepartd{%
\setbox2=\box\ProofTree
\dimen4=\ProofTreea \dimen5=\ProofTreeb \dimen6=\ProofTreec
\dimen0=\wd1
\advance\dimen0 -\dimen1
\advance\dimen0 -\dimen2
\advance\dimen0 \ProofTreespace
\advance\dimen0 \wd3
\advance\dimen0 \ProofTreespace
\advance\dimen0 \dimen4
\advance\dimen0 \dimen5
\advance\dimen0 \dimen6
% that's the width of the rule if the premise is short: recall we have
% the premise in box7
% is the premise shorter than the rule so far?
\ifnum\wd7 <\dimen0
% OK, so premise is shorter--set \dimen9 to offset of rule wrt box
\dimen9=\dimen1
\advance\dimen9 \dimen2
\global\ProofTreea=\dimen9
% calculate offset of premise wrt rule
\ProofTreeb=\dimen0
\advance\ProofTreeb -\wd7
\divide\ProofTreeb 100
\multiply\ProofTreeb \ProofTreebias
\global\ProofTreeb=\ProofTreeb
% now rebox premise to size of rule
\setbox7=\hbox to\dimen0{\hskip\ProofTreeb\box7\hfil}%
\else % premise is longer than rule
% calculate excess of premise over rule
\advance\dimen0 -\wd7
% reduce the offset of the rule wrt box by the excess
% adjusted by bias
\divide\dimen0 100 \multiply\dimen0 \ProofTreebias
\dimen9=\dimen1
\advance\dimen9 \dimen2
\advance\dimen9 \dimen0
%if \dimen 9 is negative, then
%as far as the outside world is concerned, the offset of the rule wrt
%box is zero (cos now our premise delimits the box!)--so see a bit later
\global\ProofTreea=\dimen9
% and no offset for premise wrt rule
\dimen0=\wd7
\global\ProofTreeb=0pt
\fi
% if the offset of the rule wrt box is negative, move the whole
% shebang right by that amount
\ifnum\dimen9 <0
\dimen8=-\dimen9
\global\ProofTreea=0pt
\else
\dimen8=0pt
\fi
% and return result
\global\ProofTreec=\wd8
\global\setbox\ProofTree=\vtop{\offinterlineskip\halign
{\hskip\dimen8 ##\cr
\hskip\dimen9\copy7\hfil\cr
\ProofTreerulestrut\hskip\dimen9\hskip-\ProofTreeovershoot\advance\dimen0 2\ProofTreeovershoot
\vrule width\dimen0 depth0pt height 0.4pt \hskip\ProofTreeannotspace\box0\hskip-\ProofTreeovershoot
\hfil\cr
\box1\hskip\ProofTreespace\box3\hskip\ProofTreespace\box2\hfil\cr}}%
\endgroup}%




\def\tree{%
\gobblebrace{\bgroup\aftergroup\treepartb}}
\def\treepartb{%
\box\ProofTree
}

%%%% remainder is for testing
%%%
%%%\def\test{
%%%\tree{
%%%\PTirule{another very long premise}
%%%{\PTirule{cond}
%%%{\PTaxiom{and a long one}}}}
%%%
%%%\tree{
%%%\PTiirule{a very long premise indeed}
%%% {\PTaxiom{one}}
%%% {\PTaxiom{two}}}
%%%
%%%\tree{
%%%\PTiirule{one}
%%% {\PTaxiom{two}}
%%% {\PTaxiom{three}}}
%%%
%%%
%%%\tree{
%%%\PTiirule{main conc}
%%% {\PTiirule{sub}
%%%  {\PTiirule{onea}
%%%   {\PTaxiom{oneb}}
%%%   {\PTaxiom{onec}}}
%%%  {\PTaxiom{two}}}
%%% {\PTirule{three}
%%% {\PTiirule{four}
%%%  {\PTaxiom{four}}
%%%  {\PTaxiom{five}}}\ProofTreespace=0pt}}
%%%}
%%%
%%%\ProofTreebias=0\test\vfill\eject
%%%\ProofTreebias=25\test\vfill\eject
%%%\ProofTreebias=50\test\vfill\eject
%%%\ProofTreebias=75\test\vfill\eject
%%%\ProofTreebias=100\test\vfill\eject
%%%
%%%% test of 3-concl rule
%%%
%%%\tree{\tracingcommands=1
%%%\PTiiirule{This premise}
%%%{\PTiirule{has}
%%% {\PTaxiom{with}}
%%% {\PTaxiom{two}}}
%%%{\PTirule{three}
%%% {\PTaxiom{(one)}}}
%%%{\PTirule{conclusions}
%%% {\PTaxiom{subtrees}}}}
%%%\vfill\eject
%%%\ProofTreebias=0
%%%\tree{\PTiirule{one}{\PTaxiom{two}}{\PTaxiom{three}}}
%%%
%%%\tree{\PTiiirule{one}{\PTaxiom{two}}{\PTaxiom{three}}{\PTaxiom{four}}}
%%%
%%%\ProofTreebias=100
%%%\tree{\PTiirule{one}{\PTaxiom{two}}{\PTaxiom{three}}}
%%%\showboxbreadth=100 \showboxdepth=100
%%%\tree{\PTiiirule{one}{\PTaxiom{two}}{\PTaxiom{three}}{\PTaxiom{four}}
%%%\showbox\ProofTree}
%%%
%%%
%%%
%%%
%%%\bye
%%%% test of annotated rules
%%%\tree{
%%%\aPTiiirule{Annot}{premise}
%%%{\aPTirule{Another}{first}{\PTaxiom{bottom}}}
%%%{\aPTiirule{2nd}{second}
%%% {\PTaxiom{third}}
%%% {\aPTirule{again}{fourth}{\PTaxiom{}}}}
%%%{\PTaxiom{fifth}}}
%%%
%%%\bye
