123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243 |
- "use strict";
- var __createBinding = (this && this.__createBinding) || (Object.create ? (function(o, m, k, k2) {
- if (k2 === undefined) k2 = k;
- var desc = Object.getOwnPropertyDescriptor(m, k);
- if (!desc || ("get" in desc ? !m.__esModule : desc.writable || desc.configurable)) {
- desc = { enumerable: true, get: function() { return m[k]; } };
- }
- Object.defineProperty(o, k2, desc);
- }) : (function(o, m, k, k2) {
- if (k2 === undefined) k2 = k;
- o[k2] = m[k];
- }));
- var __setModuleDefault = (this && this.__setModuleDefault) || (Object.create ? (function(o, v) {
- Object.defineProperty(o, "default", { enumerable: true, value: v });
- }) : function(o, v) {
- o["default"] = v;
- });
- var __importStar = (this && this.__importStar) || function (mod) {
- if (mod && mod.__esModule) return mod;
- var result = {};
- if (mod != null) for (var k in mod) if (k !== "default" && Object.prototype.hasOwnProperty.call(mod, k)) __createBinding(result, mod, k);
- __setModuleDefault(result, mod);
- return result;
- };
- var __read = (this && this.__read) || function (o, n) {
- var m = typeof Symbol === "function" && o[Symbol.iterator];
- if (!m) return o;
- var i = m.call(o), r, ar = [], e;
- try {
- while ((n === void 0 || n-- > 0) && !(r = i.next()).done) ar.push(r.value);
- }
- catch (error) { e = { error: error }; }
- finally {
- try {
- if (r && !r.done && (m = i["return"])) m.call(i);
- }
- finally { if (e) throw e.error; }
- }
- return ar;
- };
- var __spreadArray = (this && this.__spreadArray) || function (to, from, pack) {
- if (pack || arguments.length === 2) for (var i = 0, l = from.length, ar; i < l; i++) {
- if (ar || !(i in from)) {
- if (!ar) ar = Array.prototype.slice.call(from, 0, i);
- ar[i] = from[i];
- }
- }
- return to.concat(ar || Array.prototype.slice.call(from));
- };
- var __importDefault = (this && this.__importDefault) || function (mod) {
- return (mod && mod.__esModule) ? mod : { "default": mod };
- };
- Object.defineProperty(exports, "__esModule", { value: true });
- var TexError_js_1 = __importDefault(require("../TexError.js"));
- var TexParser_js_1 = __importDefault(require("../TexParser.js"));
- var ParseUtil_js_1 = __importDefault(require("../ParseUtil.js"));
- var BussproofsUtil = __importStar(require("./BussproofsUtil.js"));
- var BussproofsMethods = {};
- BussproofsMethods.Prooftree = function (parser, begin) {
- parser.Push(begin);
- var newItem = parser.itemFactory.create('proofTree').
- setProperties({ name: begin.getName(),
- line: 'solid', currentLine: 'solid', rootAtTop: false });
- return newItem;
- };
- BussproofsMethods.Axiom = function (parser, name) {
- var top = parser.stack.Top();
- if (top.kind !== 'proofTree') {
- throw new TexError_js_1.default('IllegalProofCommand', 'Proof commands only allowed in prooftree environment.');
- }
- var content = paddedContent(parser, parser.GetArgument(name));
- BussproofsUtil.setProperty(content, 'axiom', true);
- top.Push(content);
- };
- var paddedContent = function (parser, content) {
- var nodes = ParseUtil_js_1.default.internalMath(parser, ParseUtil_js_1.default.trimSpaces(content), 0);
- if (!nodes[0].childNodes[0].childNodes.length) {
- return parser.create('node', 'mrow', []);
- }
- var lpad = parser.create('node', 'mspace', [], { width: '.5ex' });
- var rpad = parser.create('node', 'mspace', [], { width: '.5ex' });
- return parser.create('node', 'mrow', __spreadArray(__spreadArray([lpad], __read(nodes), false), [rpad], false));
- };
- BussproofsMethods.Inference = function (parser, name, n) {
- var top = parser.stack.Top();
- if (top.kind !== 'proofTree') {
- throw new TexError_js_1.default('IllegalProofCommand', 'Proof commands only allowed in prooftree environment.');
- }
- if (top.Size() < n) {
- throw new TexError_js_1.default('BadProofTree', 'Proof tree badly specified.');
- }
- var rootAtTop = top.getProperty('rootAtTop');
- var childCount = (n === 1 && !top.Peek()[0].childNodes.length) ? 0 : n;
- var children = [];
- 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);
- var row = parser.create('node', 'mtr', children, {});
- var table = parser.create('node', 'mtable', [row], { framespacing: '0 0' });
- var conclusion = paddedContent(parser, parser.GetArgument(name));
- var style = top.getProperty('currentLine');
- if (style !== top.getProperty('line')) {
- top.setProperty('currentLine', top.getProperty('line'));
- }
- var rule = createRule(parser, table, [conclusion], top.getProperty('left'), top.getProperty('right'), style, rootAtTop);
- top.setProperty('left', null);
- top.setProperty('right', null);
- BussproofsUtil.setProperty(rule, 'inference', childCount);
- parser.configuration.addNode('inference', rule);
- top.Push(rule);
- };
- function createRule(parser, premise, conclusions, left, right, style, rootAtTop) {
- var upper = parser.create('node', 'mtr', [parser.create('node', 'mtd', [premise], {})], {});
- var lower = parser.create('node', 'mtr', [parser.create('node', 'mtd', conclusions, {})], {});
- var rule = parser.create('node', 'mtable', rootAtTop ? [lower, upper] : [upper, lower], { align: 'top 2', rowlines: style, framespacing: '0 0' });
- BussproofsUtil.setProperty(rule, 'inferenceRule', rootAtTop ? 'up' : 'down');
- var leftLabel, rightLabel;
- if (left) {
- leftLabel = parser.create('node', 'mpadded', [left], { height: '+.5em', width: '+.5em', voffset: '-.15em' });
- BussproofsUtil.setProperty(leftLabel, 'prooflabel', 'left');
- }
- if (right) {
- rightLabel = parser.create('node', 'mpadded', [right], { height: '+.5em', width: '+.5em', voffset: '-.15em' });
- BussproofsUtil.setProperty(rightLabel, 'prooflabel', 'right');
- }
- var children, label;
- if (left && right) {
- children = [leftLabel, rule, rightLabel];
- label = 'both';
- }
- else if (left) {
- children = [leftLabel, rule];
- label = 'left';
- }
- else if (right) {
- children = [rule, rightLabel];
- label = 'right';
- }
- else {
- return rule;
- }
- rule = parser.create('node', 'mrow', children);
- BussproofsUtil.setProperty(rule, 'labelledRule', label);
- return rule;
- }
- BussproofsMethods.Label = function (parser, name, side) {
- var top = parser.stack.Top();
- if (top.kind !== 'proofTree') {
- throw new TexError_js_1.default('IllegalProofCommand', 'Proof commands only allowed in prooftree environment.');
- }
- var content = ParseUtil_js_1.default.internalMath(parser, parser.GetArgument(name), 0);
- var label = (content.length > 1) ?
- parser.create('node', 'mrow', content, {}) : content[0];
- top.setProperty(side, label);
- };
- BussproofsMethods.SetLine = function (parser, _name, style, always) {
- var top = parser.stack.Top();
- if (top.kind !== 'proofTree') {
- throw new TexError_js_1.default('IllegalProofCommand', 'Proof commands only allowed in prooftree environment.');
- }
- top.setProperty('currentLine', style);
- if (always) {
- top.setProperty('line', style);
- }
- };
- BussproofsMethods.RootAtTop = function (parser, _name, where) {
- var top = parser.stack.Top();
- if (top.kind !== 'proofTree') {
- throw new TexError_js_1.default('IllegalProofCommand', 'Proof commands only allowed in prooftree environment.');
- }
- top.setProperty('rootAtTop', where);
- };
- BussproofsMethods.AxiomF = function (parser, name) {
- var top = parser.stack.Top();
- if (top.kind !== 'proofTree') {
- throw new TexError_js_1.default('IllegalProofCommand', 'Proof commands only allowed in prooftree environment.');
- }
- var line = parseFCenterLine(parser, name);
- BussproofsUtil.setProperty(line, 'axiom', true);
- top.Push(line);
- };
- function parseFCenterLine(parser, name) {
- var dollar = parser.GetNext();
- if (dollar !== '$') {
- throw new TexError_js_1.default('IllegalUseOfCommand', 'Use of %1 does not match it\'s definition.', name);
- }
- parser.i++;
- var axiom = parser.GetUpTo(name, '$');
- if (axiom.indexOf('\\fCenter') === -1) {
- throw new TexError_js_1.default('IllegalUseOfCommand', 'Missing \\fCenter in %1.', name);
- }
- var _a = __read(axiom.split('\\fCenter'), 2), prem = _a[0], conc = _a[1];
- var premise = (new TexParser_js_1.default(prem, parser.stack.env, parser.configuration)).mml();
- var conclusion = (new TexParser_js_1.default(conc, parser.stack.env, parser.configuration)).mml();
- var fcenter = (new TexParser_js_1.default('\\fCenter', parser.stack.env, parser.configuration)).mml();
- var left = parser.create('node', 'mtd', [premise], {});
- var middle = parser.create('node', 'mtd', [fcenter], {});
- var right = parser.create('node', 'mtd', [conclusion], {});
- var row = parser.create('node', 'mtr', [left, middle, right], {});
- var table = parser.create('node', 'mtable', [row], { columnspacing: '.5ex', columnalign: 'center 2' });
- BussproofsUtil.setProperty(table, 'sequent', true);
- parser.configuration.addNode('sequent', row);
- return table;
- }
- BussproofsMethods.FCenter = function (_parser, _name) { };
- BussproofsMethods.InferenceF = function (parser, name, n) {
- var top = parser.stack.Top();
- if (top.kind !== 'proofTree') {
- throw new TexError_js_1.default('IllegalProofCommand', 'Proof commands only allowed in prooftree environment.');
- }
- if (top.Size() < n) {
- throw new TexError_js_1.default('BadProofTree', 'Proof tree badly specified.');
- }
- var rootAtTop = top.getProperty('rootAtTop');
- var childCount = (n === 1 && !top.Peek()[0].childNodes.length) ? 0 : n;
- var children = [];
- 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);
- var row = parser.create('node', 'mtr', children, {});
- var table = parser.create('node', 'mtable', [row], { framespacing: '0 0' });
- var conclusion = parseFCenterLine(parser, name);
- var style = top.getProperty('currentLine');
- if (style !== top.getProperty('line')) {
- top.setProperty('currentLine', top.getProperty('line'));
- }
- var rule = createRule(parser, table, [conclusion], top.getProperty('left'), top.getProperty('right'), style, rootAtTop);
- top.setProperty('left', null);
- top.setProperty('right', null);
- BussproofsUtil.setProperty(rule, 'inference', childCount);
- parser.configuration.addNode('inference', rule);
- top.Push(rule);
- };
- exports.default = BussproofsMethods;
- //# sourceMappingURL=BussproofsMethods.js.map
|