diff options
Diffstat (limited to 'Master/texmf-dist/tex/latex')
| -rw-r--r-- | Master/texmf-dist/tex/latex/bussproofs/bussproofs.sty | 909 |
1 files changed, 909 insertions, 0 deletions
diff --git a/Master/texmf-dist/tex/latex/bussproofs/bussproofs.sty b/Master/texmf-dist/tex/latex/bussproofs/bussproofs.sty new file mode 100644 index 00000000000..b5d7cc83bd5 --- /dev/null +++ b/Master/texmf-dist/tex/latex/bussproofs/bussproofs.sty @@ -0,0 +1,909 @@ +% +\def\BPmessage{Proof Tree (bussproofs) style macros. Version 1.0.} +% bussproofs.sty. Version 1.0 +% (c) 1994,1995,1996,2004,2005,2006. Copyright retained by Samuel R. Buss. +% This software may be used and distributed freely, except that +% if you make changes, you must change the file name to be different +% than bussproofs.sty to avoid compatibility problems. +% Please report comments and bugs to sbuss@ucsd.edu. +% Thanks to Felix Joachimski for making changes to let these macros +% work in plain TeX in addition to LaTeX. Nothing has been done +% to see if they work in AMSTeX. The comments below mostly +% are written for LaTeX, however. +% July 2004, version 0.7 +% - bug fix, right labels with descenders inserted too much space. +% Thanks to Peter Smith for finding this bug, +% see http://www.phil.cam.ac.uk/teaching_staff/Smith/LaTeX/ +% March 2005, version 0.8. +% Added a default definition for \fCenter at Denis Kosygin's +% suggestion. +% September 2005, version 0.9. +% Fixed some subtle spacing problems, by adding %'s to the end of +% few lines where they were inadvertantly omitted. Thanks to +% Arnold Beckmann for finding and fixing this problem. +% April 2006, version 0.9.1. Updated comments and testbp2.tex file. +% No change to the actual macros. +% June 2006, version 1.0. The first integer numbered release. +% New feature: root of proof may now be at the bottom instead of +% at just the top. Thanks to Alex Hertel for the suggestion to implement +% this. + +% A good exposition of how to use bussproofs.sty (version 0.9) has been written +% by Peter Smith and is available on the internet. +% The comments below also describe the features of bussproofs.sty, +% including user-modifiable parameters. + +% bussproofs.sty allows the construction of proof trees in the +% style of the sequent calculus and many other proof systems +% One novel feature of these macros is they support the horizontal +% alignment according to some center point specified with the +% command \fCenter. This is the style often used in sequent +% calculus proofs. +% Proofs are specified in left-to-right traversal order. +% For example a proof +% A B +% ----- +% D C +% --------- +% E +% +% if given in the order D,A,B,C,E. Each line in the proof is +% specified according to the arity of the inference which generates +% it. Thus, E would be specified with a \BinaryInf or \BinaryInfC +% command. +% +% The above proof tree could be displayed with the commands: +% +% \AxiomC{D} +% \AxiomC{A} +% \AxiomC{B} +% \BinaryInfC{C} +% \BinaryInfC{E} +% \DisplayProof +% +% Inferences in a proof may be nullary (axioms), unary, binary, or +% trinary. +% +% IMPORTANT: You must give the \DisplayProof command to make the proof +% be printed. To display a centered proof on a line by itself, +% put the proof inside \begin{center} ... \end{center}. +% +% There are two styles for specifying horizontal centering of +% lines (formulas or sequents) in a proof. One format \AxiomC{...} +% just centers the formula {...} in the usual way. The other +% format is \Axiom$...\fCenter...$. Here, the \fCenter specifies +% the center of the formula. (It is permissable for \fCenter to +% generate typeset material; in fact, I usually define it to generate +% the sequent arrow.) In unary inferences, the \fCenter +% positions will be vertically aligned in the upper and lower lines of +% the inference. Unary, Binary, Trinary inferences are specified +% with the same format as Axioms. The two styles of centering +% lines may be combined in a single proof. +% +% By using the optional \EnableBpAbbreviations command, various +% abbreviated two letter commands are enabled. This allows +% \AX and \AXC for \Axiom and \AxiomC, (resp.), +% \DP for \DisplayProof, +% \BI and \BIC for \BinaryInf and \BinaryInfC, +% \UI and \UIC for \UnaryInf and \UnaryInfC, +% \TI and \TIC for \TrinaryInf and \TrinaryInfC, +% \LL and \RL for \LeftLabel and \RightLabel. +% The enabling of these short abbreviations is OPTIONAL, since +% there is the possibility of conflicting with names from other +% macro packages. +% +% By default, the inferences have single horizontal lines (scores) +% This can be overridden using the \doubleLine, \noLine commands. +% These two commands affect only the next inference. You can make +% make a permanent override that applies to the rest of the current +% proof using \alwaysDoubleLine and \alwaysNoLine. \singleLine +% and \alwaysSingleLine work in the analogous way. +% +% The macros do their best to give good placements of for the +% parts of the proof. Several macros allow you to override the +% defaults. These are \insertBetweenHyps{...} which overrides +% the default spacing between hypotheses of Binary and Trinary +% inferences with {...}. And \kernHyps{...} specifies a distance +% to shift the whole block of hypotheses to the right (modifying +% the default center position. +% Other macros set the vertical placement of the whole proof. +% The default is to try to do a good job of placement for inferences +% included in text. Two other useful macros are: \bottomAlignProof +% which aligns the hbox output by \DisplayProof according to the base +% of the bottom line of the proof, and \centerAlignProof which +% does a precise center vertical alignment. +% +% Often, one wishes to place a label next to an inference, usually +% to specify the type of inference. These labels can be placed +% by using the commands \LeftLabel{...} and \RightLabel{...} +% immediately before the command which specifies the inference. +% For example, to generate +% +% A B +% --------- X +% C +% +% use the commands +% \AxiomC{A} +% \AxiomC{B} +% \RightLabel{X} +% \BinaryInfC{C} +% \DisplayProof +% +% The \DisplayProof command just displays the proof as a text +% item. This allows you to put proofs anywhere normal text +% might appear; for example, in a paragraph, in a table, in +% a tabbing environment, etc. When displaying a proof as inline text, +% you should write \DisplayProof{} (with curly brackets) so that +% LaTeX will not "eat" the white space following the \DisplayProof +% command. +% For displaying proofs in a centered display: Do not use the \[...\] +% construction (nor $$...$$). Instead use +% \begin{center} ... \DisplayProof\end{center}. +% Actually there is a better construction to use instead of the +% \begin{center}...\DisplayProof\end{center}. This is to +% write +% \begin{prooftree} ... \end{prooftree}. +% Note there is no \DisplayProof used for this: the +% \end{prooftree} automatically supplies the \DisplayProof +% command. +% +% Warning: Any commands that set line types or set vertical or +% horizontal alignment that are given AFTER the \DisplayProof +% command will affect the next proof, no matter how distant. + + + + +% Usages: +% ======= +% +% \Axiom$<antecedent>\fCenter<succedent>$ +% +% \AxiomC{<whole sequent or formula} +% +% Note that the use of surrounding {}'s is mandatory in \AxiomC and +% is prohibited in $\Axiom. On the other hand, the $'s are optional +% in \AxiomC and are mandatory in \Axiom. To typeset the argument +% to \AxiomC in math mode, you must use $'s (or \(...\) ). +% +% \UnaryInf$<antecendent>\fCenter<succedent>$ +% +% \UnaryInfC{<whole sequent or formula>} +% +% \BinaryInf$<antecendent>\fCenter<succedent>$ +% +% \BinaryInfC{<whole sequent or formula>} +% +% \TrinaryInf$<antecendent>\fCenter<succedent>$ +% +% \TrinaryInfC{<whole sequent or formula>} +% +% \LeftLabel{<text>} - Puts <text> as a label to the left +% of the next inference line. (Works even if +% \noLine is used too.) +% +% \RightLabel{<text>} - Puts <text> as a label to the right of the +% next inference line. (Also works with \noLine.) +% +% \DisplayProof - outputs the whole proof tree (and finishes it). +% The proof tree is output as an hbox. +% +% +% \kernHyps{<dimen>} - Slides the upper hypotheses right distance <dimen> +% (This is similar to shifting conclusion left) +% - kernHyps works with Unary, Binary and Trinary +% inferences and with centered or uncentered sequents. +% - Negative values for <dimen> are permitted. +% +% \insertBetweenHyps{...} - {...} will be inserted between the upper +% hypotheses of a Binary or Trinary Inferences. +% It is possible to use negative horizontal space +% to push them closer together (and even overlap). +% This command affects only the next inference. +% +% \doubleLine - Makes the current (ie, next) horizontal line doubled +% +% \alwaysDoubleLine - Makes lines doubled for rest of proof +% +% \singleLine - Makes the current (ie, next) line single +% +% \alwaysSingleLine - Undoes \alwaysDoubleLine or \alwaysNoLine. +% +% \noLine - Make no line at all at current (ie next) inference. +% +% \alwaysNoLine - Makes no lines for rest of proof. (Untested) +% +% \solidLine - Does solid horizontal line for current inference +% +% \dottedLine - Does dotted horizontal line for current inference +% +% \dashedLine - Does dashed horizontal line for current inference +% +% \alwaysSolidLine - Makes the indicated change in line type, permanently +% \alwaysDashedLine until end of proof or until overridden. +% \alwaysDottedLine +% +% \bottomAlignProof - Vertically align proof according to its bottom line. +% \centerAlignProof - Vertically align proof proof precisely in its center. +% \normalAlignProof - Overrides earlier bottom/center AlignProof commands. +% The default alignment will look good in most cases, +% whether the proof is displayed or is +% in-line. Other alignments may be more +% appropriate when putting proofs in tables or +% pictures, etc. For custom alignments, use +% TeX's raise commands. +% +% \rootAtTop - specifies that proofs have their root a the top. That it, +% proofs will be "upside down". +% \rootAtBottom - (default) Specifies that proofs have root at the bottom +% The \rootAtTop and \rootAtBottom commands apply *only* to the +% current proof. If you want to make them persistent, use one of +% the next two commands: +% \alwaysRootAtTop +% \alwaysRootAtBottom (default) +% + +% Optional short abbreviations for commands: +\def\EnableBpAbbreviations{% + \let\AX\Axiom + \let\AXC\AxiomC + \let\UI\UnaryInf + \let\UIC\UnaryInfC + \let\BI\BinaryInf + \let\BIC\BinaryInfC + \let\TI\TrinaryInf + \let\TIC\TrinaryInfC + \let\LL\LeftLabel + \let\RL\RightLabel + \let\DP\DisplayProof +} + +% Parameters which control the style of the proof trees. +% The user may wish to override these parameters locally or globally. +% BUT DONT CHANGE THE PARAMETERS BY CHANGING THIS FILE (to avoid +% future incompatibilities). Instead, you should change them in your +% TeX document right after including this style file in the +% header material of your LaTeX document. + +\def\ScoreOverhang{4pt} % How much underlines extend out +\def\ScoreOverhangLeft{\ScoreOverhang} +\def\ScoreOverhangRight{\ScoreOverhang} + +\def\extraVskip{2pt} % Extra space above and below lines +\def\ruleScoreFiller{\hrule} % Horizontal rule filler. +\def\dottedScoreFiller{\hbox to4pt{\hss.\hss}} +\def\dashedScoreFiller{\hbox to2.8mm{\hss\vrule width1.4mm height0.4pt depth0.0pt\hss}} +\def\defaultScoreFiller{\ruleScoreFiller} % Default horizontal filler. +\def\defaultBuildScore{\buildSingleScore} % In \singleLine mode at start. + +\def\defaultHypSeparation{\hskip.2in} % Used if \insertBetweenHyps isn't given + +\def\labelSpacing{3pt} % Horizontal space separating labels and lines + +\def\proofSkipAmount{\vskip.8ex plus.8ex minus.4ex} + % Space above and below a prooftree display. + +\def\defaultRootPosition{\buildRootBottom} +%\def\defaultRootPosition{\buildRootTop} % Makes all proofs upside down + +\ifx\fCenter\undefined +\def\fCenter{\relax} +\fi + +% +% End of user-modifiable parameters. +% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +% Here are some internal paramenters and defaults. Not really intended +% to be user-modifiable. + +\def\theHypSeparation{\defaultHypSeparation} +\def\alwaysScoreFiller{\defaultScoreFiller} % Horizontal filler. +\def\alwaysBuildScore{\defaultBuildScore} +\def\theScoreFiller{\alwaysScoreFiller} % Horizontal filler. +\def\buildScore{\alwaysBuildScore} %This command builds the score. +\def\hypKernAmt{0pt} % Initial setting for kerning the hypotheses. + +\def\defaultLeftLabel{} +\def\defaultRightLabel{} + +\def\myTrue{Y} +\def\bottomAlignFlag{N} +\def\centerAlignFlag{N} +\def\defaultRootAtBottomFlag{Y} +\def\rootAtBottomFlag{Y} + +% End of internal parameters and defaults. + +\expandafter\ifx\csname newenvironment\endcsname\relax% +% If in TeX: +\message{\BPmessage} +\def\makeatletter{\catcode`\@=11\relax} +\def\makeatother{\catcode`\@=12\relax} +\makeatletter +\def\newcount{\alloc@0\count\countdef\insc@unt} +\def\newdimen{\alloc@1\dimen\dimendef\insc@unt} +\def\newskip{\alloc@2\skip\skipdef\insc@unt} +\def\newbox{\alloc@4\box\chardef\insc@unt} +\makeatother +\else +% If in LaTeX +\typeout{\BPmessage} +\newenvironment{prooftree}% +{\begin{center}\proofSkipAmount \leavevmode}% +{\DisplayProof \proofSkipAmount \end{center} } +\fi + +\def\thecur#1{\csname#1\number\theLevel\endcsname} + +\newcount\theLevel % This counter is the height of the stack. +\global\theLevel=0 % Initialized to zero +\newcount\myMaxLevel +\global\myMaxLevel=0 +\newbox\myBoxA % Temporary storage boxes +\newbox\myBoxB +\newbox\myBoxC +\newbox\myBoxD +\newbox\myBoxLL % Boxes for the left label and the right label. +\newbox\myBoxRL +\newdimen\thisAboveSkip %Internal use: amount to skip above line +\newdimen\thisBelowSkip %Internal use: amount to skip below line +\newdimen\newScoreStart % More temporary storage. +\newdimen\newScoreEnd +\newdimen\newCenter +\newdimen\displace +\newdimen\leftLowerAmt% Amount to lower left label +\newdimen\rightLowerAmt% Amount to lower right label +\newdimen\scoreHeight% Score height +\newdimen\scoreDepth% Score Depth +\newdimen\htLbox% +\newdimen\htRbox% +\newdimen\htAbox% +\newdimen\htCbox% + +\setbox\myBoxLL=\hbox{\defaultLeftLabel}% +\setbox\myBoxRL=\hbox{\defaultRightLabel}% + +\def\allocatemore{% + \ifnum\theLevel>\myMaxLevel% + \expandafter\newbox\curBox% + \expandafter\newdimen\curScoreStart% + \expandafter\newdimen\curCenter% + \expandafter\newdimen\curScoreEnd% + \global\advance\myMaxLevel by1% + \fi% +} + +\def\prepAxiom{% + \advance\theLevel by1% + \edef\curBox{\thecur{myBox}}% + \edef\curScoreStart{\thecur{myScoreStart}}% + \edef\curCenter{\thecur{myCenter}}% + \edef\curScoreEnd{\thecur{myScoreEnd}}% + \allocatemore% +} + +\def\Axiom$#1\fCenter#2${% + % Get level and correct names set. + \prepAxiom% + % Define the boxes + \setbox\myBoxA=\hbox{$\mathord{#1}\fCenter\mathord{\relax}$}% + \setbox\myBoxB=\hbox{$#2$}% + \global\setbox\curBox=% + \hbox{\hskip\ScoreOverhangLeft\relax% + \unhcopy\myBoxA\unhcopy\myBoxB\hskip\ScoreOverhangRight\relax}% + % Set the relevant dimensions for the boxes + \global\curScoreStart=0pt \relax + \global\curScoreEnd=\wd\curBox \relax + \global\curCenter=\wd\myBoxA \relax + \global\advance \curCenter by \ScoreOverhangLeft% + \ignorespaces +} + +\def\AxiomC#1{ % Note argument not in math mode + % Get level and correct names set. + \prepAxiom% + % Define the box. + \setbox\myBoxA=\hbox{#1}% + \global\setbox\curBox =% + \hbox{\hskip\ScoreOverhangLeft\relax% + \unhcopy\myBoxA\hskip\ScoreOverhangRight\relax}% + % Set the relevant dimensions for the boxes + \global\curScoreStart=0pt \relax + \global\curScoreEnd=\wd\curBox \relax + \global\curCenter=.5\wd\curBox \relax + \global\advance \curCenter by \ScoreOverhangLeft% + \ignorespaces +} + +\def\prepUnary{% + \ifnum \theLevel<1 + \errmessage{Hypotheses missing!} + \fi% + \edef\curBox{\thecur{myBox}}% + \edef\curScoreStart{\thecur{myScoreStart}}% + \edef\curCenter{\thecur{myCenter}}% + \edef\curScoreEnd{\thecur{myScoreEnd}}% +} + +\def\UnaryInf$#1\fCenter#2${% + \prepUnary% + \buildConclusion{#1}{#2}% + \joinUnary% + \resetInferenceDefaults% + \ignorespaces% +} + +\def\UnaryInfC#1{ + \prepUnary% + \buildConclusionC{#1}% + %Align and join the curBox and the new box into one vbox. + \joinUnary% + \resetInferenceDefaults% + \ignorespaces% +} + +\def\prepBinary{% + \ifnum\theLevel<2 + \errmessage{Hypotheses missing!} + \fi% + \edef\rcurBox{\thecur{myBox}}% Set up names of right hypothesis + \edef\rcurScoreStart{\thecur{myScoreStart}}% + \edef\rcurCenter{\thecur{myCenter}}% + \edef\rcurScoreEnd{\thecur{myScoreEnd}}% + \advance\theLevel by-1% + \edef\lcurBox{\thecur{myBox}}% Set up names of left hypothesis + \edef\lcurScoreStart{\thecur{myScoreStart}}% + \edef\lcurCenter{\thecur{myCenter}}% + \edef\lcurScoreEnd{\thecur{myScoreEnd}}% +} + +\def\BinaryInf$#1\fCenter#2${% + \prepBinary% + \buildConclusion{#1}{#2}% + \joinBinary% + \resetInferenceDefaults% + \ignorespaces% +} + +\def\BinaryInfC#1{% + \prepBinary% + \buildConclusionC{#1}% + \joinBinary% + \resetInferenceDefaults% + \ignorespaces% +} + +\def\prepTrinary{% + \ifnum\theLevel<3 + \errmessage{Hypotheses missing!} + \fi% + \edef\rcurBox{\thecur{myBox}}% Set up names of right hypothesis + \edef\rcurScoreStart{\thecur{myScoreStart}}% + \edef\rcurCenter{\thecur{myCenter}}% + \edef\rcurScoreEnd{\thecur{myScoreEnd}}% + \advance\theLevel by-1% + \edef\ccurBox{\thecur{myBox}}% Set up names of center hypothesis + \edef\ccurScoreStart{\thecur{myScoreStart}}% + \edef\ccurCenter{\thecur{myCenter}}% + \edef\ccurScoreEnd{\thecur{myScoreEnd}}% + \advance\theLevel by-1% + \edef\lcurBox{\thecur{myBox}}% Set up names of left hypothesis + \edef\lcurScoreStart{\thecur{myScoreStart}}% + \edef\lcurCenter{\thecur{myCenter}}% + \edef\lcurScoreEnd{\thecur{myScoreEnd}}% +} + +\def\TrinaryInf$#1\fCenter#2${% + \prepTrinary% + \buildConclusion{#1}{#2}% + \joinTrinary% + \resetInferenceDefaults% + \ignorespaces% +} + +\def\TrinaryInfC#1{% + \prepTrinary% + \buildConclusionC{#1}% + \joinTrinary% + \resetInferenceDefaults% + \ignorespaces% +} + +\def\buildConclusion#1#2{% Build lower sequent w/ center at \fCenter position. + % Define the boxes + \setbox\myBoxA=\hbox{$\mathord{#1}\fCenter\mathord{\relax}$}% + \setbox\myBoxB=\hbox{$#2$}% + % Put them together in \myBoxC + \setbox\myBoxC =% + \hbox{\hskip\ScoreOverhangLeft\relax% + \unhcopy\myBoxA\unhcopy\myBoxB\hskip\ScoreOverhangRight\relax}% + % Calculate the center of the \myBoxC string. + \newScoreStart=0pt \relax% + \newCenter=\wd\myBoxA \relax% + \advance \newCenter by \ScoreOverhangLeft% + \newScoreEnd=\wd\myBoxC% +} + +\def\buildConclusionC#1{% Build lower sequent w/o \fCenter present. + % Define the box. + \setbox\myBoxA=\hbox{#1}% + \setbox\myBoxC =% + \hbox{\hbox{\hskip\ScoreOverhangLeft\relax% + \unhcopy\myBoxA\hskip\ScoreOverhangRight\relax}}% + % Calculate kerning to line up centers + \newScoreStart=0pt \relax% + \newCenter=.5\wd\myBoxC \relax% + \newScoreEnd=\wd\myBoxC% + \advance \newCenter by \ScoreOverhangLeft% +} + +\def\joinUnary{%Align and join \curBox and \myBoxC into a single vbox + \global\advance\curCenter by -\hypKernAmt% + \ifnum\curCenter<\newCenter% + \displace=\newCenter% + \advance \displace by -\curCenter% + \kernUpperBox% + \else% + \displace=\curCenter% + \advance \displace by -\newCenter% + \kernLowerBox% + \fi% + \ifnum \newScoreStart < \curScoreStart % + \global \curScoreStart = \newScoreStart \fi% + \ifnum \curScoreEnd < \newScoreEnd % + \global \curScoreEnd = \newScoreEnd \fi% + % Leave room for the left label. + \ifnum \curScoreStart<\wd\myBoxLL% + \global\displace = \wd\myBoxLL% + \global\advance\displace by -\curScoreStart% + \kernUpperBox% + \kernLowerBox% + \fi% + % Draw the score + \buildScore% + % Form the score and labels into a box. + \buildScoreLabels% + % Form the new box and its dimensions + \ifx\rootAtBottomFlag\myTrue% + \buildRootBottom% + \else% + \buildRootTop% + \fi% + \global \curScoreStart=\newScoreStart% + \global \curScoreEnd=\newScoreEnd% + \global \curCenter=\newCenter% +} + +\def\buildRootBottom{% + \global \setbox \curBox =% + \vbox{\box\curBox% + \vskip\thisAboveSkip \relax% + \nointerlineskip\box\myBoxD% + \vskip\thisBelowSkip \relax% + \nointerlineskip\box\myBoxC}% +} + +\def\buildRootTop{% + \global \setbox \curBox =% + \vbox{\box\myBoxC% + \vskip\thisAboveSkip \relax% + \nointerlineskip\box\myBoxD% + \vskip\thisBelowSkip \relax% + \nointerlineskip\box\curBox}% +} + +\def\kernUpperBox{% + \global\setbox\curBox =% + \hbox{\hskip\displace\box\curBox}% + \global\advance \curScoreStart by \displace% + \global\advance \curScoreEnd by \displace% + \global\advance\curCenter by \displace% +} + +\def\kernLowerBox{% + \global\setbox\myBoxC =% + \hbox{\hskip\displace\unhbox\myBoxC}% + \global\advance \newScoreStart by \displace% + \global\advance \newScoreEnd by \displace% + \global\advance\newCenter by \displace% +} + +\def\joinBinary{% Construct the binary inference into a vbox. + % Join the two hypotheses's boxes into one hbox. + \setbox\myBoxA=\hbox{\theHypSeparation}% + \lcurScoreEnd=\rcurScoreEnd% + \advance\lcurScoreEnd by\wd\lcurBox% + \advance\lcurScoreEnd by\wd\myBoxA% + \displace=\lcurScoreEnd% + \advance\displace by -\lcurScoreStart% + \lcurCenter=.5\displace% + \advance\lcurCenter by\lcurScoreStart% + \ifx\rootAtBottomFlag\myTrue% + \setbox\lcurBox=% + \hbox{\box\lcurBox\unhcopy\myBoxA\box\rcurBox}% + \else% + \htLbox = \ht\lcurBox% + \htAbox = \ht\myBoxA% + \htRbox = \ht\rcurBox% + \setbox\lcurBox=% + \hbox{\lower\htLbox\box\lcurBox% + \lower\htAbox\box\myBoxA\lower\htRbox\box\rcurBox}% + \fi% + % Adjust center of upper hypotheses according to how much + % the lower sequent is off-center. + \displace=\newCenter% + \advance\displace by -.5\newScoreStart% + \advance\displace by -.5\newScoreEnd% + \advance\lcurCenter by \displace% + %Align and join the curBox and the two hypotheses's box into one vbox. + \edef\curBox{\lcurBox}% + \edef\curScoreStart{\lcurScoreStart}% + \edef\curScoreEnd{\lcurScoreEnd}% + \edef\curCenter{\lcurCenter}% + \joinUnary% +} + +\def\joinTrinary{% Construct the trinary inference into a vbox. + % Join the three hypotheses's boxes into one hbox. + \setbox\myBoxA=\hbox{\theHypSeparation}% + \lcurScoreEnd=\rcurScoreEnd% + \advance\lcurScoreEnd by\wd\lcurBox% + \advance\lcurScoreEnd by\wd\ccurBox% + \advance\lcurScoreEnd by2\wd\myBoxA% + \displace=\lcurScoreEnd% + \advance\displace by -\lcurScoreStart% + \lcurCenter=.5\displace% + \advance\lcurCenter by\lcurScoreStart% + \ifx\rootAtBottomFlag\myTrue% + \setbox\lcurBox=% + \hbox{\box\lcurBox\unhcopy\myBoxA\box\ccurBox% + \unhcopy\myBoxA\box\rcurBox}% + \else% + \htLbox = \ht\lcurBox% + \htAbox = \ht\myBoxA% + \htCbox = \ht\ccurBox% + \htRbox = \ht\rcurBox% + \setbox\lcurBox=% + \hbox{\lower\htLbox\box\lcurBox% + \lower\htAbox\box\myBoxA\lower\htCbox\box\ccurBox% + \lower\htAbox\box\myBoxA\lower\htRbox\box\rcurBox}% + \fi% + % Adjust center of upper hypotheses according to how much + % the lower sequent is off-center. + \displace=\newCenter% + \advance\displace by -.5\newScoreStart% + \advance\displace by -.5\newScoreEnd% + \advance\lcurCenter by \displace% + %Align and join the curBox and the two hypotheses's box into one vbox. + \edef\curBox{\lcurBox}% + \edef\curScoreStart{\lcurScoreStart}% + \edef\curScoreEnd{\lcurScoreEnd}% + \edef\curCenter{\lcurCenter}% + \joinUnary% +} + +\def\DisplayProof{% + % Display (and purge) the proof tree. + % Choose the appropriate vertical alignment. + \ifnum \theLevel=1 \relax \else%x + \errmessage{Proof tree badly specified.}% + \fi% + \edef\curBox{\thecur{myBox}}% + \ifx\bottomAlignFlag\myTrue% + \displace=0pt% + \else% + \displace=.5\ht\curBox% + \ifx\centerAlignFlag\myTrue\relax + \else% + \advance\displace by -3pt% + \fi% + \fi% + \leavevmode% + \lower\displace\hbox{\copy\curBox}% + \global\theLevel=0% + \global\def\alwaysBuildScore{\defaultBuildScore}% Restore "always" + \global\def\alwaysScoreFiller{\defaultScoreFiller}% Restore "always" + \global\def\bottomAlignFlag{N}% + \global\def\centerAlignFlag{N}% + \resetRootPosition + \resetInferenceDefaults% + \ignorespaces +} + +\def\buildSingleScore{% Make an hbox with a single score. + \displace=\curScoreEnd% + \advance \displace by -\curScoreStart% + \global\setbox \myBoxD =% + \hbox to \displace{\expandafter\xleaders\theScoreFiller\hfill}% + %\global\setbox \myBoxD =% + %\hbox{\hskip\curScoreStart\relax \box\myBoxD}% +} + +\def\buildDoubleScore{% Make an hbox with a double score. + \buildSingleScore% + \global\setbox\myBoxD=% + \hbox{\hbox to0pt{\copy\myBoxD\hss}\raise2pt\copy\myBoxD}% +} + +\def\buildNoScore{% Make an hbox with no score (raise a little anyway) + \global\setbox\myBoxD=\hbox{\vbox{\vskip1pt}}% +} + +\def\doubleLine{% + \gdef\buildScore{\buildDoubleScore}% Set next score to this type + \ignorespaces +} +\def\alwaysDoubleLine{% + \gdef\alwaysBuildScore{\buildDoubleScore}% Do double for rest of proof. + \gdef\buildScore{\buildDoubleScore}% Set next score to be double + \ignorespaces +} +\def\singleLine{% + \gdef\buildScore{\buildSingleScore}% Set next score to be single + \ignorespaces +} +\def\alwaysSingleLine{% + \gdef\alwaysBuildScore{\buildSingleScore}% Do single for rest of proof. + \gdef\buildScore{\buildSingleScore}% Set next score to be single + \ignorespaces +} +\def\noLine{% + \gdef\buildScore{\buildNoScore}% Set next score to this type + \ignorespaces +} +\def\alwaysNoLine{% + \gdef\alwaysBuildScore{\buildNoScore}%Do nolines for rest of proof. + \gdef\buildScore{\buildNoScore}% Set next score to be blank + \ignorespaces +} +\def\solidLine{% + \gdef\theScoreFiller{\ruleScoreFiller}% Use solid horizontal line. + \ignorespaces +} +\def\alwaysSolidLine{% + \gdef\alwaysScoreFiller{\ruleScoreFiller}% Do solid for rest of proof + \gdef\theScoreFiller{\ruleScoreFiller}% Use solid horizontal line. + \ignorespaces +} +\def\dottedLine{% + \gdef\theScoreFiller{\dottedScoreFiller}% Use dotted horizontal line. + \ignorespaces +} +\def\alwaysDottedLine{% + \gdef\alwaysScoreFiller{\dottedScoreFiller}% Do dotted for rest of proof + \gdef\theScoreFiller{\dottedScoreFiller}% Use dotted horizontal line. + \ignorespaces +} +\def\dashedLine{% + \gdef\theScoreFiller{\dashedScoreFiller}% Use dashed horizontal line. + \ignorespaces +} +\def\alwaysDashedLine{% + \gdef\alwaysScoreFiller{\dashedScoreFiller}% Do dashed for rest of proof + \gdef\theScoreFiller{\dashedScoreFiller}% Use dashed horizontal line. + \ignorespaces +} +\def\kernHyps#1{% + \gdef\hypKernAmt{#1}% + \ignorespaces +} +\def\insertBetweenHyps#1{% + \gdef\theHypSeparation{#1}% + \ignorespaces +} + +\def\centerAlignProof{% + \def\centerAlignFlag{Y}% + \def\bottomAlignFlag{N}% + \ignorespaces +} +\def\bottomAlignProof{% + \def\centerAlignFlag{N}% + \def\bottomAlignFlag{Y}% + \ignorespaces +} +\def\normalAlignProof{% + \def\centerAlignFlag{N}% + \def\bottomAlignFlag{N}% + \ignorespaces +} + +\def\LeftLabel#1{% + \global\setbox\myBoxLL=\hbox{{#1}\hskip\labelSpacing}% + \ignorespaces +} +\def\RightLabel#1{% + \global\setbox\myBoxRL=\hbox{\hskip\labelSpacing #1}% + \ignorespaces +} + +\def\buildScoreLabels{% + \scoreHeight = \ht\myBoxD% + \scoreDepth = \dp\myBoxD% + \leftLowerAmt=\ht\myBoxLL% + \advance \leftLowerAmt by -\dp\myBoxLL% + \advance \leftLowerAmt by -\scoreHeight% + \advance \leftLowerAmt by \scoreDepth% + \leftLowerAmt=.5\leftLowerAmt% + \rightLowerAmt=\ht\myBoxRL% + \advance \rightLowerAmt by -\dp\myBoxRL% + \advance \rightLowerAmt by -\scoreHeight% + \advance \rightLowerAmt by \scoreDepth% + \rightLowerAmt=.5\rightLowerAmt% + \displace = \curScoreStart% + \advance\displace by -\wd\myBoxLL% + \global\setbox\myBoxD =% + \hbox{\hskip\displace% + \lower\leftLowerAmt\copy\myBoxLL% + \box\myBoxD% + \lower\rightLowerAmt\copy\myBoxRL}% + \global\thisAboveSkip = \ht\myBoxLL% + \global\advance \thisAboveSkip by -\leftLowerAmt% + \global\advance \thisAboveSkip by -\scoreHeight% + \ifnum \thisAboveSkip<0 % + \global\thisAboveSkip=0pt% + \fi% + \displace = \ht\myBoxRL% + \advance \displace by -\rightLowerAmt% + \advance \displace by -\scoreHeight% + \ifnum \displace<0 % + \displace=0pt% + \fi% + \ifnum \displace>\thisAboveSkip % + \global\thisAboveSkip=\displace% + \fi% + \global\thisBelowSkip = \dp\myBoxLL% + \global\advance\thisBelowSkip by \leftLowerAmt% + \global\advance\thisBelowSkip by -\scoreDepth% + \ifnum\thisBelowSkip<0 % + \global\thisBelowSkip = 0pt% + \fi% + \displace = \dp\myBoxRL% + \advance\displace by \rightLowerAmt% + \advance\displace by -\scoreDepth% + \ifnum\displace<0 % + \displace = 0pt% + \fi% + \ifnum\displace>\thisBelowSkip% + \global\thisBelowSkip = \displace% + \fi% + \global\thisAboveSkip = -\thisAboveSkip% + \global\thisBelowSkip = -\thisBelowSkip% + \global\advance\thisAboveSkip by\extraVskip% Extra space above line + \global\advance\thisBelowSkip by\extraVskip% Extra space below line +} + +\def\resetInferenceDefaults{% + \global\def\theHypSeparation{\defaultHypSeparation}% + \global\setbox\myBoxLL=\hbox{\defaultLeftLabel}% + \global\setbox\myBoxRL=\hbox{\defaultRightLabel}% + \global\def\buildScore{\alwaysBuildScore}% + \global\def\theScoreFiller{\alwaysScoreFiller}% + \gdef\hypKernAmt{0pt}% Restore to zero kerning. +} + + +\def\rootAtBottom{% + \global\def\rootAtBottomFlag{Y}% +} + +\def\rootAtTop{% + \global\def\rootAtBottomFlag{N}% +} + +\def\resetRootPosition{% + \global\edef\rootAtBottomFlag{\defaultRootAtBottomFlag} +} + +\def\alwaysRootAtBottom{% + \global\def\defaultRootAtBottomFlag{Y} + \rootAtBottom +} + +\def\alwaysRootAtTop{% + \global\def\defaultRootAtBottomFlag{N} + \rootAtTop +} + |