diff --git a/testsuite/tests/input/tex/Bussproofs.test.ts b/testsuite/tests/input/tex/Bussproofs.test.ts
index dafa66cf4..5b3ba9e69 100644
--- a/testsuite/tests/input/tex/Bussproofs.test.ts
+++ b/testsuite/tests/input/tex/Bussproofs.test.ts
@@ -2,6 +2,7 @@ import { afterAll, beforeEach, describe, expect, it } from '@jest/globals';
import { getTokens, setupTexWithOutput, tex2mml } from '#helpers';
import '#js/input/tex/bussproofs/BussproofsConfiguration';
import '#js/input/tex/ams/AmsConfiguration';
+import '#js/input/tex/newcommand/NewcommandConfiguration';
beforeEach(() => setupTexWithOutput(['base', 'ams', 'bussproofs']));
@@ -213,4 +214,184 @@ describe('BussproofsRegProofs', () => {
/**********************************************************************************/
+describe('BussproofsSequents', () => {
+ beforeEach(() =>
+ setupTexWithOutput(['base', 'ams', 'newcommand', 'bussproofs'])
+ );
+
+ it('Sequent Axiom Only', () => {
+ expect(
+ tex2mml(
+ '\\def\\fCenter{\\vdash}\\begin{prooftree}\\Axiom$A \\fCenter B$\\end{prooftree}'
+ )
+ ).toMatchSnapshot();
+ });
+
+ it('Sequent Axiom Display Proof No Space', () => {
+ expect(tex2mml('\\Axiom$A\\fCenterA$\\DisplayProof')).toMatchSnapshot();
+ });
+
+ it('Sequent Unary', () => {
+ expect(
+ tex2mml(
+ '\\def\\fCenter{\\vdash}\\begin{prooftree}\\Axiom$A,B \\fCenter C$\\UnaryInf$A \\fCenter B,C$\\end{prooftree}'
+ )
+ ).toMatchSnapshot();
+ });
+
+ it('Sequent Unary Chain', () => {
+ expect(
+ tex2mml(
+ '\\def\\fCenter{\\vdash}\\begin{prooftree}\\Axiom$A,B,Q,R \\fCenter C$\\UnaryInf$A \\fCenter B,C$\\UnaryInf$\\fCenter A,B,C,D,E$\\end{prooftree}'
+ )
+ ).toMatchSnapshot();
+ });
+
+ it('Sequent Unary Chain Labelled', () => {
+ expect(
+ tex2mml(
+ '\\def\\fCenter{\\vdash}\\begin{prooftree}\\Axiom$A,B,Q,R \\fCenter C$\\RightLabel{X}\\UnaryInf$A \\fCenter B,C$\\RightLabel{Y}\\UnaryInf$\\fCenter A,B,C$\\end{prooftree}'
+ )
+ ).toMatchSnapshot();
+ });
+
+ it('Sequent Unary Chain Plain Line', () => {
+ expect(
+ tex2mml(
+ '\\def\\fCenter{\\vdash}\\begin{prooftree}\\Axiom$A,B \\fCenter C$\\UnaryInfC{intermediate}\\UnaryInf$A \\fCenter B,C,D,E$\\end{prooftree}'
+ )
+ ).toMatchSnapshot();
+ });
+
+ it('Sequent Unary Chain Binary Top', () => {
+ expect(
+ tex2mml(
+ '\\def\\fCenter{\\vdash}\\begin{prooftree}\\AxiomC{$P$}\\AxiomC{$Q$}\\BinaryInf$A,B,Q,R \\fCenter C$\\UnaryInf$A \\fCenter B,C$\\UnaryInf$\\fCenter A,B,C$\\end{prooftree}'
+ )
+ ).toMatchSnapshot();
+ });
+
+ it('Sequent Binary', () => {
+ expect(
+ tex2mml(
+ '\\def\\fCenter{\\vdash}\\begin{prooftree}\\Axiom$\\fCenter A$\\Axiom$B \\fCenter C,D$\\UnaryInf$B,X,Y,Z \\fCenter C$\\BinaryInf$A,B \\fCenter C$\\end{prooftree}'
+ )
+ ).toMatchSnapshot();
+ });
+
+ it('Sequent Root At Top', () => {
+ expect(
+ tex2mml(
+ '\\def\\fCenter{\\vdash}\\begin{prooftree}\\rootAtTop\\Axiom$A,B,Q,R \\fCenter C$\\UnaryInf$A \\fCenter B,C$\\UnaryInf$\\fCenter A,B,C$\\end{prooftree}'
+ )
+ ).toMatchSnapshot();
+ });
+
+ it('Sequent Widest At Bottom', () => {
+ expect(
+ tex2mml(
+ '\\def\\fCenter{\\vdash}\\begin{prooftree}\\Axiom$A \\fCenter B$\\UnaryInf$A,B \\fCenter C$\\UnaryInf$A,B,C,D \\fCenter E$\\UnaryInf$A,B,C,D,E,F \\fCenter G$\\end{prooftree}'
+ )
+ ).toMatchSnapshot();
+ });
+
+ it('Sequent Display Proof Chain', () => {
+ expect(
+ tex2mml(
+ '\\def\\fCenter{\\vdash}\\Axiom$A,B,Q \\fCenter C$\\UnaryInf$A \\fCenter B,C$\\UnaryInf$\\fCenter A,B,C$\\DP'
+ )
+ ).toMatchSnapshot();
+ });
+
+ it('Sequent Abbreviations', () => {
+ expect(
+ tex2mml(
+ '\\def\\fCenter{\\vdash}\\AX$A \\fCenter B$\\AX$C \\fCenter D$\\BI$E \\fCenter F$\\DP'
+ )
+ ).toMatchSnapshot();
+ });
+});
+
+/**********************************************************************************/
+
+describe('BussproofsCommands', () => {
+ it('Display Proof', () => {
+ expect(tex2mml('\\AxiomC{A}\\UnaryInfC{B}\\DisplayProof')).toMatchSnapshot();
+ });
+
+ it('Display Proof Inline', () => {
+ expect(tex2mml('X = \\AxiomC{A}\\UnaryInfC{B}\\DP')).toMatchSnapshot();
+ });
+
+ it('Enable Abbreviations', () => {
+ expect(
+ tex2mml('\\EnableBpAbbreviations\\AXC{A}\\AXC{B}\\AXC{C}\\TIC{D}\\DP')
+ ).toMatchSnapshot();
+ });
+
+ it('Quaternary Abbreviation', () => {
+ expect(
+ tex2mml('\\AXC{A}\\AXC{B}\\AXC{C}\\AXC{D}\\QIC{E}\\DP')
+ ).toMatchSnapshot();
+ });
+
+ it('Quinary Abbreviation', () => {
+ expect(
+ tex2mml('\\AXC{A}\\AXC{B}\\AXC{C}\\AXC{D}\\AXC{E}\\QuIC{F}\\DP')
+ ).toMatchSnapshot();
+ });
+
+ it('Kern Hyps', () => {
+ expect(
+ tex2mml(
+ '\\begin{prooftree}\\AxiomC{A}\\AxiomC{B}\\kernHyps{1em}\\BinaryInfC{C}\\end{prooftree}'
+ )
+ ).toMatchSnapshot();
+ });
+
+ it('Insert Between Hyps', () => {
+ expect(
+ tex2mml(
+ '\\begin{prooftree}\\AxiomC{A}\\AxiomC{B}\\insertBetweenHyps{\\hskip 2em}\\BinaryInfC{C}\\end{prooftree}'
+ )
+ ).toMatchSnapshot();
+ });
+
+ it('Dotted Line', () => {
+ expect(
+ tex2mml(
+ '\\begin{prooftree}\\AxiomC{A}\\dottedLine\\UnaryInfC{B}\\end{prooftree}'
+ )
+ ).toMatchSnapshot();
+ });
+
+ it('Double Line', () => {
+ expect(
+ tex2mml(
+ '\\begin{prooftree}\\AxiomC{A}\\doubleLine\\UnaryInfC{B}\\end{prooftree}'
+ )
+ ).toMatchSnapshot();
+ });
+
+ it('Bottom Align Proof', () => {
+ expect(
+ tex2mml('\\bottomAlignProof\\AxiomC{A}\\UnaryInfC{B}\\DP')
+ ).toMatchSnapshot();
+ });
+
+ it('Center Align Proof', () => {
+ expect(
+ tex2mml('\\centerAlignProof\\AxiomC{A}\\UnaryInfC{B}\\DP')
+ ).toMatchSnapshot();
+ });
+
+ it('Normal Align Proof', () => {
+ expect(
+ tex2mml('\\normalAlignProof\\AxiomC{A}\\UnaryInfC{B}\\DP')
+ ).toMatchSnapshot();
+ });
+});
+
+/**********************************************************************************/
+
afterAll(() => getTokens('bussproofs'));
diff --git a/testsuite/tests/input/tex/__snapshots__/Bussproofs.test.ts.snap b/testsuite/tests/input/tex/__snapshots__/Bussproofs.test.ts.snap
index 78e77a56a..f37b175ff 100644
--- a/testsuite/tests/input/tex/__snapshots__/Bussproofs.test.ts.snap
+++ b/testsuite/tests/input/tex/__snapshots__/Bussproofs.test.ts.snap
@@ -1,8 +1,8 @@
// Jest Snapshot v1, https://goo.gl/fbAQLP
-exports[`BussproofsRegInf Binary Inference 1`] = `
-""
+`;
+
+exports[`BussproofsCommands Center Align Proof 1`] = `
+""
`;
-exports[`BussproofsRegInf Binary Inference Abbr 1`] = `
-""
`;
diff --git a/ts/input/tex/bussproofs/BussproofsItems.ts b/ts/input/tex/bussproofs/BussproofsItems.ts
index a9a4f51ad..c45ac334a 100644
--- a/ts/input/tex/bussproofs/BussproofsItems.ts
+++ b/ts/input/tex/bussproofs/BussproofsItems.ts
@@ -22,6 +22,7 @@
*/
import TexError from '../TexError.js';
+import NodeUtil from '../NodeUtil.js';
import { BaseItem, CheckType, StackItem } from '../StackItem.js';
import { MmlNode } from '../../../core/MmlTree/MmlNode.js';
import Stack from '../Stack.js';
@@ -61,6 +62,13 @@ export class ProofTreeItem extends BaseItem {
return [[this.factory.create('mml', node), item], true];
}
if (item.isKind('stop')) {
+ if (this.getProperty('implicit')) {
+ throw new TexError(
+ 'MissingDisplayProof',
+ 'Missing %1 to display the proof tree.',
+ '\\DisplayProof'
+ );
+ }
throw new TexError('EnvMissingEnd', 'Missing \\end{%1}', this.getName());
}
this.innerStack.Push(item);
@@ -72,6 +80,7 @@ export class ProofTreeItem extends BaseItem {
*/
public toMml() {
const tree = super.toMml();
+ this.alignProof(tree);
const start = this.innerStack.Top();
if (start.isKind('start') && !start.Size()) {
return tree;
@@ -80,4 +89,33 @@ export class ProofTreeItem extends BaseItem {
const prefix = this.innerStack.Top().toMml();
return this.create('node', 'mrow', [prefix, tree], {});
}
+
+ /**
+ * Adjusts the vertical alignment of the finished proof tree with respect
+ * to the baseline, as requested by \bottomAlignProof or \centerAlignProof.
+ *
+ * @param {MmlNode} tree The proof tree.
+ */
+ protected alignProof(tree: MmlNode) {
+ const align = this.getProperty('proofAlign') as string;
+ if (!align || align === 'normal') {
+ return;
+ }
+ const table = NodeUtil.isType(tree, 'mtable')
+ ? tree
+ : (tree.childNodes.find((node) =>
+ NodeUtil.isType(node as MmlNode, 'mtable')
+ ) as MmlNode);
+ if (!table) {
+ return;
+ }
+ NodeUtil.setAttribute(
+ table,
+ 'align',
+ align === 'center'
+ ? 'center'
+ : // Align the baseline with that of the conclusion row.
+ `baseline ${this.getProperty('rootAtTop') ? 1 : 2}`
+ );
+ }
}
diff --git a/ts/input/tex/bussproofs/BussproofsMappings.ts b/ts/input/tex/bussproofs/BussproofsMappings.ts
index 586257654..4c5bd07e7 100644
--- a/ts/input/tex/bussproofs/BussproofsMappings.ts
+++ b/ts/input/tex/bussproofs/BussproofsMappings.ts
@@ -37,29 +37,44 @@ new CommandMap('Bussproofs-macros', {
QuinaryInfC: [BussproofsMethods.Inference, 5],
RightLabel: [BussproofsMethods.Label, 'right'],
LeftLabel: [BussproofsMethods.Label, 'left'],
- // Abbreviations are automatically enabled
+ DisplayProof: BussproofsMethods.DisplayProof,
+
+ // Abbreviations are automatically enabled, so this is a no-op.
+ EnableBpAbbreviations: BussproofsMethods.EnableAbbreviations,
+ AX: BussproofsMethods.AxiomF,
AXC: BussproofsMethods.Axiom,
+ UI: [BussproofsMethods.InferenceF, 1],
UIC: [BussproofsMethods.Inference, 1],
+ BI: [BussproofsMethods.InferenceF, 2],
BIC: [BussproofsMethods.Inference, 2],
+ TI: [BussproofsMethods.InferenceF, 3],
TIC: [BussproofsMethods.Inference, 3],
+ QI: [BussproofsMethods.InferenceF, 4],
+ QIC: [BussproofsMethods.Inference, 4],
+ QuI: [BussproofsMethods.InferenceF, 5],
+ QuIC: [BussproofsMethods.Inference, 5],
RL: [BussproofsMethods.Label, 'right'],
LL: [BussproofsMethods.Label, 'left'],
+ DP: BussproofsMethods.DisplayProof,
+
+ kernHyps: BussproofsMethods.KernHyps,
+ insertBetweenHyps: BussproofsMethods.BetweenHyps,
noLine: [BussproofsMethods.SetLine, 'none', false],
singleLine: [BussproofsMethods.SetLine, 'solid', false],
solidLine: [BussproofsMethods.SetLine, 'solid', false],
dashedLine: [BussproofsMethods.SetLine, 'dashed', false],
- // Not yet implemented in CSS!
- // doubleLine: [BussproofsMethods.SetLine, 'double', false],
- // dottedLine: [BussproofsMethods.SetLine, 'dotted', false],
+ dottedLine: [BussproofsMethods.SetLine, 'dotted', false],
+ // Double lines are not yet implemented in the SVG output jax!
+ doubleLine: [BussproofsMethods.SetLine, 'double', false],
alwaysNoLine: [BussproofsMethods.SetLine, 'none', true],
alwaysSingleLine: [BussproofsMethods.SetLine, 'solid', true],
alwaysSolidLine: [BussproofsMethods.SetLine, 'solid', true],
alwaysDashedLine: [BussproofsMethods.SetLine, 'dashed', true],
- // Not yet implemented in CSS!
- // alwaysDoubleLine: [BussproofsMethods.SetLine, 'double', true],
- // alwaysDottedLine: [BussproofsMethods.SetLine, 'dotted', true],
+ alwaysDottedLine: [BussproofsMethods.SetLine, 'dotted', true],
+ // Double lines are not yet implemented in the SVG output jax!
+ alwaysDoubleLine: [BussproofsMethods.SetLine, 'double', true],
rootAtTop: [BussproofsMethods.RootAtTop, true],
alwaysRootAtTop: [BussproofsMethods.RootAtTop, true],
@@ -68,6 +83,10 @@ new CommandMap('Bussproofs-macros', {
alwaysRootAtBottom: [BussproofsMethods.RootAtTop, false],
// TODO: always commands should be persistent.
+ bottomAlignProof: [BussproofsMethods.AlignProof, 'bottom'],
+ centerAlignProof: [BussproofsMethods.AlignProof, 'center'],
+ normalAlignProof: [BussproofsMethods.AlignProof, 'normal'],
+
fCenter: BussproofsMethods.FCenter,
Axiom: BussproofsMethods.AxiomF,
UnaryInf: [BussproofsMethods.InferenceF, 1],
diff --git a/ts/input/tex/bussproofs/BussproofsMethods.ts b/ts/input/tex/bussproofs/BussproofsMethods.ts
index d3f5803b2..7d6544108 100644
--- a/ts/input/tex/bussproofs/BussproofsMethods.ts
+++ b/ts/input/tex/bussproofs/BussproofsMethods.ts
@@ -48,6 +48,30 @@ function paddedContent(parser: TexParser, content: string): MmlNode {
return parser.create('node', 'mrow', [lpad, ...nodes, rpad]);
}
+/**
+ * Gets the current proof tree stack item. If the parser is not currently
+ * inside a prooftree environment, an implicit proof tree is started, which
+ * has to be terminated with a \DisplayProof command (as in the original
+ * plain TeX version of the package, where proof commands can occur anywhere
+ * in the text).
+ *
+ * @param {TexParser} parser The calling parser.
+ * @returns {StackItem} The (possibly newly created) proof tree item.
+ */
+function getProofTree(parser: TexParser): StackItem {
+ let top = parser.stack.Top();
+ if (top.kind !== 'proofTree') {
+ top = parser.itemFactory.create('proofTree').setProperties({
+ line: 'solid',
+ currentLine: 'solid',
+ rootAtTop: false,
+ implicit: true,
+ });
+ parser.Push(top);
+ }
+ return top;
+}
+
/**
* Creates a ND style inference rule.
*
@@ -182,6 +206,91 @@ function parseFCenterLine(parser: TexParser, name: string): MmlNode {
return table;
}
+/**
+ * Builds an inference rule from the topmost n elements of the proof tree.
+ * This implements the joint functionality of the InfC (plain conclusion) and
+ * Inf (sequent conclusion with \fCenter) commands of any arity.
+ *
+ * @param {TexParser} parser The current parser.
+ * @param {string} name The name of the calling command.
+ * @param {number} n Number of premises for this inference rule.
+ * @param {boolean} sequent True if the conclusion is a sequent line
+ * containing \fCenter.
+ */
+function doInference(
+ parser: TexParser,
+ name: string,
+ n: number,
+ sequent: boolean
+) {
+ const top = getProofTree(parser);
+ if (top.Size() < n) {
+ throw new TexError('BadProofTree', 'Proof tree badly specified.');
+ }
+ const rootAtTop = top.getProperty('rootAtTop') as boolean;
+ const childCount = n === 1 && !top.Peek()[0].childNodes.length ? 0 : n;
+ const hypSep = top.getProperty('hypSep') as string;
+ const children: MmlNode[] = [];
+ do {
+ if (children.length) {
+ // The separating column, possibly containing the material given by
+ // \insertBetweenHyps, which is parsed anew for each separator.
+ const sep = hypSep
+ ? [new TexParser(hypSep, parser.stack.env, parser.configuration).mml()]
+ : [];
+ children.unshift(parser.create('node', 'mtd', sep, {}));
+ }
+ children.unshift(
+ parser.create('node', 'mtd', [top.Pop()], {
+ rowalign: rootAtTop ? 'top' : 'bottom',
+ })
+ );
+ n--;
+ } while (n > 0);
+ const hypKern = top.getProperty('hypKern') as string;
+ if (hypKern) {
+ // \kernHyps: slide the block of hypotheses to the right (or left for
+ // negative values) by prepending a space to the first premise.
+ const mspace = parser.create('node', 'mspace', [], { width: hypKern });
+ const mrow = children[0].childNodes[0] as MmlNode;
+ mspace.parent = mrow;
+ mrow.childNodes.unshift(mspace);
+ }
+ const row = parser.create('node', 'mtr', children, {});
+ const table = parser.create(
+ 'node',
+ 'mtable',
+ [row],
+ hypSep
+ ? // The hypothesis separation replaces the default column spacing.
+ { framespacing: '0 0', columnspacing: '0em' }
+ : { framespacing: '0 0' }
+ );
+ const conclusion = sequent
+ ? parseFCenterLine(parser, name) // TODO: Padding
+ : paddedContent(parser, parser.GetArgument(name));
+ const style = top.getProperty('currentLine') as string;
+ if (style !== top.getProperty('line')) {
+ top.setProperty('currentLine', top.getProperty('line'));
+ }
+ const rule = createRule(
+ parser,
+ table,
+ [conclusion],
+ top.getProperty('left') as MmlNode,
+ top.getProperty('right') as MmlNode,
+ style,
+ rootAtTop
+ );
+ top.setProperty('left', null);
+ top.setProperty('right', null);
+ top.setProperty('hypKern', null);
+ top.setProperty('hypSep', null);
+ BussproofsUtil.setProperty(rule, 'inference', childCount);
+ parser.configuration.addNode('inference', rule);
+ top.Push(rule);
+}
+
// Namespace
const BussproofsMethods: { [key: string]: ParseMethod } = {
/**
@@ -213,14 +322,7 @@ const BussproofsMethods: { [key: string]: ParseMethod } = {
* @param {string} name The name of the command.
*/
Axiom(parser: TexParser, name: string) {
- const top = parser.stack.Top();
- // TODO: Label error
- if (top.kind !== 'proofTree') {
- throw new TexError(
- 'IllegalProofCommand',
- 'Proof commands only allowed in prooftree environment.'
- );
- }
+ const top = getProofTree(parser);
const content = paddedContent(parser, parser.GetArgument(name));
BussproofsUtil.setProperty(content, 'axiom', true);
top.Push(content);
@@ -234,53 +336,7 @@ const BussproofsMethods: { [key: string]: ParseMethod } = {
* @param {number} n Number of premises for this inference rule.
*/
Inference(parser: TexParser, name: string, n: number) {
- const top = parser.stack.Top();
- if (top.kind !== 'proofTree') {
- throw new TexError(
- 'IllegalProofCommand',
- 'Proof commands only allowed in prooftree environment.'
- );
- }
- if (top.Size() < n) {
- throw new TexError('BadProofTree', 'Proof tree badly specified.');
- }
- const rootAtTop = top.getProperty('rootAtTop') as boolean;
- const childCount = n === 1 && !top.Peek()[0].childNodes.length ? 0 : n;
- const children: MmlNode[] = [];
- do {
- if (children.length) {
- children.unshift(parser.create('node', 'mtd', [], {}));
- }
- children.unshift(
- parser.create('node', 'mtd', [top.Pop()], {
- rowalign: rootAtTop ? 'top' : 'bottom',
- })
- );
- n--;
- } while (n > 0);
- const row = parser.create('node', 'mtr', children, {});
- const table = parser.create('node', 'mtable', [row], {
- framespacing: '0 0',
- });
- const conclusion = paddedContent(parser, parser.GetArgument(name));
- const style = top.getProperty('currentLine') as string;
- if (style !== top.getProperty('line')) {
- top.setProperty('currentLine', top.getProperty('line'));
- }
- const rule = createRule(
- parser,
- table,
- [conclusion],
- top.getProperty('left') as MmlNode,
- top.getProperty('right') as MmlNode,
- style,
- rootAtTop
- );
- top.setProperty('left', null);
- top.setProperty('right', null);
- BussproofsUtil.setProperty(rule, 'inference', childCount);
- parser.configuration.addNode('inference', rule);
- top.Push(rule);
+ doInference(parser, name, n, false);
},
/**
@@ -291,14 +347,7 @@ const BussproofsMethods: { [key: string]: ParseMethod } = {
* @param {string} side The side of the label.
*/
Label(parser: TexParser, name: string, side: string) {
- const top = parser.stack.Top();
- // Label error
- if (top.kind !== 'proofTree') {
- throw new TexError(
- 'IllegalProofCommand',
- 'Proof commands only allowed in prooftree environment.'
- );
- }
+ const top = getProofTree(parser);
const content = ParseUtil.internalMath(parser, parser.GetArgument(name), 0);
const label =
content.length > 1
@@ -316,14 +365,7 @@ const BussproofsMethods: { [key: string]: ParseMethod } = {
* @param {boolean} always Set as permanent style.
*/
SetLine(parser: TexParser, _name: string, style: string, always: boolean) {
- const top = parser.stack.Top();
- // Label error
- if (top.kind !== 'proofTree') {
- throw new TexError(
- 'IllegalProofCommand',
- 'Proof commands only allowed in prooftree environment.'
- );
- }
+ const top = getProofTree(parser);
top.setProperty('currentLine', style);
if (always) {
top.setProperty('line', style);
@@ -338,13 +380,7 @@ const BussproofsMethods: { [key: string]: ParseMethod } = {
* @param {string} where If true root is at top, otherwise at bottom.
*/
RootAtTop(parser: TexParser, _name: string, where: boolean) {
- const top = parser.stack.Top();
- if (top.kind !== 'proofTree') {
- throw new TexError(
- 'IllegalProofCommand',
- 'Proof commands only allowed in prooftree environment.'
- );
- }
+ const top = getProofTree(parser);
top.setProperty('rootAtTop', where);
},
@@ -355,13 +391,7 @@ const BussproofsMethods: { [key: string]: ParseMethod } = {
* @param {string} name The name of the command.
*/
AxiomF(parser: TexParser, name: string) {
- const top = parser.stack.Top();
- if (top.kind !== 'proofTree') {
- throw new TexError(
- 'IllegalProofCommand',
- 'Proof commands only allowed in prooftree environment.'
- );
- }
+ const top = getProofTree(parser);
const line = parseFCenterLine(parser, name);
BussproofsUtil.setProperty(line, 'axiom', true);
top.Push(line);
@@ -383,54 +413,80 @@ const BussproofsMethods: { [key: string]: ParseMethod } = {
* @param {number} n Number of premises for this inference rule.
*/
InferenceF(parser: TexParser, name: string, n: number) {
+ doInference(parser, name, n, true);
+ },
+
+ /**
+ * Implements the DisplayProof command that terminates and displays a
+ * proof tree given outside of a prooftree environment. Inside the
+ * environment the command is redundant, as the display is provided by the
+ * end of the environment.
+ *
+ * @param {TexParser} parser The current parser.
+ * @param {string} _name The name of the command.
+ */
+ DisplayProof(parser: TexParser, _name: string) {
const top = parser.stack.Top();
if (top.kind !== 'proofTree') {
- throw new TexError(
- 'IllegalProofCommand',
- 'Proof commands only allowed in prooftree environment.'
- );
+ throw new TexError('BadProofTree', 'Proof tree badly specified.');
}
- if (top.Size() < n) {
+ if (!top.getProperty('implicit')) {
+ return;
+ }
+ if (top.Size() !== 1) {
throw new TexError('BadProofTree', 'Proof tree badly specified.');
}
- const rootAtTop = top.getProperty('rootAtTop') as boolean;
- const childCount = n === 1 && !top.Peek()[0].childNodes.length ? 0 : n;
- const children: MmlNode[] = [];
- do {
- if (children.length) {
- children.unshift(parser.create('node', 'mtd', [], {}));
- }
- children.unshift(
- parser.create('node', 'mtd', [top.Pop()], {
- rowalign: rootAtTop ? 'top' : 'bottom',
- })
- );
- n--;
- } while (n > 0);
- const row = parser.create('node', 'mtr', children, {});
- const table = parser.create('node', 'mtable', [row], {
- framespacing: '0 0',
- });
+ const node = top.toMml();
+ BussproofsUtil.setProperty(node, 'proof', true);
+ parser.stack.Pop();
+ parser.Push(node);
+ },
- const conclusion = parseFCenterLine(parser, name); // TODO: Padding
- const style = top.getProperty('currentLine') as string;
- if (style !== top.getProperty('line')) {
- top.setProperty('currentLine', top.getProperty('line'));
- }
- const rule = createRule(
- parser,
- table,
- [conclusion],
- top.getProperty('left') as MmlNode,
- top.getProperty('right') as MmlNode,
- style,
- rootAtTop
- );
- top.setProperty('left', null);
- top.setProperty('right', null);
- BussproofsUtil.setProperty(rule, 'inference', childCount);
- parser.configuration.addNode('inference', rule);
- top.Push(rule);
+ /**
+ * Implements the EnableBpAbbreviations command. The abbreviated commands
+ * are always enabled in this implementation, so this is a no-op.
+ *
+ * @param {TexParser} _parser The current parser.
+ * @param {string} _name The name of the command.
+ */
+ EnableAbbreviations(_parser: TexParser, _name: string) {},
+
+ /**
+ * Implements the kernHyps command that slides the block of hypotheses of
+ * the next inference to the right by the given dimension (negative values
+ * slide to the left).
+ *
+ * @param {TexParser} parser The current parser.
+ * @param {string} name The name of the command.
+ */
+ KernHyps(parser: TexParser, name: string) {
+ const top = getProofTree(parser);
+ top.setProperty('hypKern', parser.GetDimen(name));
+ },
+
+ /**
+ * Implements the insertBetweenHyps command that provides the material
+ * separating the hypotheses of the next inference.
+ *
+ * @param {TexParser} parser The current parser.
+ * @param {string} name The name of the command.
+ */
+ BetweenHyps(parser: TexParser, name: string) {
+ const top = getProofTree(parser);
+ top.setProperty('hypSep', parser.GetArgument(name));
+ },
+
+ /**
+ * Implements the proof alignment commands that determine the vertical
+ * position of the proof tree with respect to the baseline.
+ *
+ * @param {TexParser} parser The current parser.
+ * @param {string} _name The name of the command.
+ * @param {string} align The alignment: 'bottom', 'center' or 'normal'.
+ */
+ AlignProof(parser: TexParser, _name: string, align: string) {
+ const top = getProofTree(parser);
+ top.setProperty('proofAlign', align);
},
};
diff --git a/ts/input/tex/bussproofs/BussproofsUtil.ts b/ts/input/tex/bussproofs/BussproofsUtil.ts
index 701460b16..8d96cfcc7 100644
--- a/ts/input/tex/bussproofs/BussproofsUtil.ts
+++ b/ts/input/tex/bussproofs/BussproofsUtil.ts
@@ -328,7 +328,8 @@ const adjustSequents = function (config: ParseOptions) {
}
const collect = [];
let inf = getParentInf(seq);
- if (getProperty(inf, 'inference') !== 1) {
+ // An axiom-only proof has no parent inference rule.
+ if (!inf || getProperty(inf, 'inference') !== 1) {
continue;
}
collect.push(seq);
@@ -338,14 +339,17 @@ const adjustSequents = function (config: ParseOptions) {
const premise = firstPremise(
getPremises(inf, getProperty(inf, 'inferenceRule') as string)
);
- const sequent = getProperty(premise, 'inferenceRule')
- ? // If the first premise is an inference rule, check the conclusions for a sequent.
- getConclusion(
- premise,
- getProperty(premise, 'inferenceRule') as string
- )
- : // Otherwise it is a hyp and we have to check the formula itself.
- premise;
+ // If the premise is an inference rule (possibly with labels), we have
+ // to check its conclusion for a sequent. Otherwise it is a hyp and we
+ // have to check the formula itself.
+ const rule = getProperty(premise, 'inferenceRule')
+ ? premise
+ : getProperty(premise, 'labelledRule')
+ ? getRule(premise)
+ : null;
+ const sequent = rule
+ ? getConclusion(rule, getProperty(rule, 'inferenceRule') as string)
+ : premise;
if (getProperty(sequent, 'sequent')) {
seq = sequent.childNodes[0];
collect.push(seq);
@@ -353,7 +357,9 @@ const adjustSequents = function (config: ParseOptions) {
}
inf = premise;
}
- adjustSequentPairwise(config, collect);
+ if (collect.length > 1) {
+ alignSequents(config, collect);
+ }
}
};
@@ -387,73 +393,38 @@ const addSequentSpace = function (
};
/**
- * Adjusts the sequent positioning for a list of inference rules by pairwise
- * adjusting the width of formulas in sequents. I.e.,
+ * Aligns the fCenter elements of a chain of sequents by padding the
+ * antecedent and succedent of each sequent to the maximal width occurring in
+ * the chain. As all sequent lines are centered within the proof tree, equal
+ * widths on both sides align the fCenter positions vertically. I.e.,
* A,B |- C
* ------------
* A |- B,C
*
* will be adjusted to
*
- * A, B |- C
+ * A,B |- C__
* ----------------
- * A |- B,C
+ * __A |- B,C
*
* @param {ParseOptions} config Parser configuration options.
* @param {MmlNode[]} sequents The list of sequents.
*/
-const adjustSequentPairwise = function (
- config: ParseOptions,
- sequents: MmlNode[]
-) {
- let top = sequents.pop();
- while (sequents.length) {
- const bottom = sequents.pop();
- const [left, right] = compareSequents(top, bottom);
- if (getProperty(top.parent, 'axiom')) {
- addSequentSpace(
- config,
- left < 0 ? top : bottom,
- 0,
- 'left',
- Math.abs(left)
- );
- addSequentSpace(
- config,
- right < 0 ? top : bottom,
- 2,
- 'right',
- Math.abs(right)
- );
+const alignSequents = function (config: ParseOptions, sequents: MmlNode[]) {
+ const lefts = sequents.map((seq) => getBBox(seq.childNodes[0] as MmlNode));
+ const rights = sequents.map((seq) => getBBox(seq.childNodes[2] as MmlNode));
+ const maxLeft = Math.max(...lefts);
+ const maxRight = Math.max(...rights);
+ for (let i = 0; i < sequents.length; i++) {
+ if (lefts[i] < maxLeft) {
+ addSequentSpace(config, sequents[i], 0, 'left', maxLeft - lefts[i]);
+ }
+ if (rights[i] < maxRight) {
+ addSequentSpace(config, sequents[i], 2, 'right', maxRight - rights[i]);
}
- top = bottom;
}
};
-/**
- * Compares the top and bottom sequent of a inference rule
- * Top: A |- B
- * ----------
- * Bottom: C |- D
- *
- * @param {MmlNode} top Top sequent.
- * @param {MmlNode} bottom Bottom sequent.
- * @returns {[number, number]} The delta for left and right side of the sequents.
- */
-const compareSequents = function (
- top: MmlNode,
- bottom: MmlNode
-): [number, number] {
- const tr = getBBox(top.childNodes[2]);
- const br = getBBox(bottom.childNodes[2]);
- const tl = getBBox(top.childNodes[0]);
- const bl = getBBox(bottom.childNodes[0]);
- // Deltas
- const dl = tl - bl;
- const dr = tr - br;
- return [dl, dr];
-};
-
// For every inference rule we adjust the width of ruler by subtracting and
// adding suitable spaces around the rule. The algorithm in detail.
//