BussproofsMethods.js 11 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243
  1. "use strict";
  2. var __createBinding = (this && this.__createBinding) || (Object.create ? (function(o, m, k, k2) {
  3. if (k2 === undefined) k2 = k;
  4. var desc = Object.getOwnPropertyDescriptor(m, k);
  5. if (!desc || ("get" in desc ? !m.__esModule : desc.writable || desc.configurable)) {
  6. desc = { enumerable: true, get: function() { return m[k]; } };
  7. }
  8. Object.defineProperty(o, k2, desc);
  9. }) : (function(o, m, k, k2) {
  10. if (k2 === undefined) k2 = k;
  11. o[k2] = m[k];
  12. }));
  13. var __setModuleDefault = (this && this.__setModuleDefault) || (Object.create ? (function(o, v) {
  14. Object.defineProperty(o, "default", { enumerable: true, value: v });
  15. }) : function(o, v) {
  16. o["default"] = v;
  17. });
  18. var __importStar = (this && this.__importStar) || function (mod) {
  19. if (mod && mod.__esModule) return mod;
  20. var result = {};
  21. if (mod != null) for (var k in mod) if (k !== "default" && Object.prototype.hasOwnProperty.call(mod, k)) __createBinding(result, mod, k);
  22. __setModuleDefault(result, mod);
  23. return result;
  24. };
  25. var __read = (this && this.__read) || function (o, n) {
  26. var m = typeof Symbol === "function" && o[Symbol.iterator];
  27. if (!m) return o;
  28. var i = m.call(o), r, ar = [], e;
  29. try {
  30. while ((n === void 0 || n-- > 0) && !(r = i.next()).done) ar.push(r.value);
  31. }
  32. catch (error) { e = { error: error }; }
  33. finally {
  34. try {
  35. if (r && !r.done && (m = i["return"])) m.call(i);
  36. }
  37. finally { if (e) throw e.error; }
  38. }
  39. return ar;
  40. };
  41. var __spreadArray = (this && this.__spreadArray) || function (to, from, pack) {
  42. if (pack || arguments.length === 2) for (var i = 0, l = from.length, ar; i < l; i++) {
  43. if (ar || !(i in from)) {
  44. if (!ar) ar = Array.prototype.slice.call(from, 0, i);
  45. ar[i] = from[i];
  46. }
  47. }
  48. return to.concat(ar || Array.prototype.slice.call(from));
  49. };
  50. var __importDefault = (this && this.__importDefault) || function (mod) {
  51. return (mod && mod.__esModule) ? mod : { "default": mod };
  52. };
  53. Object.defineProperty(exports, "__esModule", { value: true });
  54. var TexError_js_1 = __importDefault(require("../TexError.js"));
  55. var TexParser_js_1 = __importDefault(require("../TexParser.js"));
  56. var ParseUtil_js_1 = __importDefault(require("../ParseUtil.js"));
  57. var BussproofsUtil = __importStar(require("./BussproofsUtil.js"));
  58. var BussproofsMethods = {};
  59. BussproofsMethods.Prooftree = function (parser, begin) {
  60. parser.Push(begin);
  61. var newItem = parser.itemFactory.create('proofTree').
  62. setProperties({ name: begin.getName(),
  63. line: 'solid', currentLine: 'solid', rootAtTop: false });
  64. return newItem;
  65. };
  66. BussproofsMethods.Axiom = function (parser, name) {
  67. var top = parser.stack.Top();
  68. if (top.kind !== 'proofTree') {
  69. throw new TexError_js_1.default('IllegalProofCommand', 'Proof commands only allowed in prooftree environment.');
  70. }
  71. var content = paddedContent(parser, parser.GetArgument(name));
  72. BussproofsUtil.setProperty(content, 'axiom', true);
  73. top.Push(content);
  74. };
  75. var paddedContent = function (parser, content) {
  76. var nodes = ParseUtil_js_1.default.internalMath(parser, ParseUtil_js_1.default.trimSpaces(content), 0);
  77. if (!nodes[0].childNodes[0].childNodes.length) {
  78. return parser.create('node', 'mrow', []);
  79. }
  80. var lpad = parser.create('node', 'mspace', [], { width: '.5ex' });
  81. var rpad = parser.create('node', 'mspace', [], { width: '.5ex' });
  82. return parser.create('node', 'mrow', __spreadArray(__spreadArray([lpad], __read(nodes), false), [rpad], false));
  83. };
  84. BussproofsMethods.Inference = function (parser, name, n) {
  85. var top = parser.stack.Top();
  86. if (top.kind !== 'proofTree') {
  87. throw new TexError_js_1.default('IllegalProofCommand', 'Proof commands only allowed in prooftree environment.');
  88. }
  89. if (top.Size() < n) {
  90. throw new TexError_js_1.default('BadProofTree', 'Proof tree badly specified.');
  91. }
  92. var rootAtTop = top.getProperty('rootAtTop');
  93. var childCount = (n === 1 && !top.Peek()[0].childNodes.length) ? 0 : n;
  94. var children = [];
  95. do {
  96. if (children.length) {
  97. children.unshift(parser.create('node', 'mtd', [], {}));
  98. }
  99. children.unshift(parser.create('node', 'mtd', [top.Pop()], { 'rowalign': (rootAtTop ? 'top' : 'bottom') }));
  100. n--;
  101. } while (n > 0);
  102. var row = parser.create('node', 'mtr', children, {});
  103. var table = parser.create('node', 'mtable', [row], { framespacing: '0 0' });
  104. var conclusion = paddedContent(parser, parser.GetArgument(name));
  105. var style = top.getProperty('currentLine');
  106. if (style !== top.getProperty('line')) {
  107. top.setProperty('currentLine', top.getProperty('line'));
  108. }
  109. var rule = createRule(parser, table, [conclusion], top.getProperty('left'), top.getProperty('right'), style, rootAtTop);
  110. top.setProperty('left', null);
  111. top.setProperty('right', null);
  112. BussproofsUtil.setProperty(rule, 'inference', childCount);
  113. parser.configuration.addNode('inference', rule);
  114. top.Push(rule);
  115. };
  116. function createRule(parser, premise, conclusions, left, right, style, rootAtTop) {
  117. var upper = parser.create('node', 'mtr', [parser.create('node', 'mtd', [premise], {})], {});
  118. var lower = parser.create('node', 'mtr', [parser.create('node', 'mtd', conclusions, {})], {});
  119. var rule = parser.create('node', 'mtable', rootAtTop ? [lower, upper] : [upper, lower], { align: 'top 2', rowlines: style, framespacing: '0 0' });
  120. BussproofsUtil.setProperty(rule, 'inferenceRule', rootAtTop ? 'up' : 'down');
  121. var leftLabel, rightLabel;
  122. if (left) {
  123. leftLabel = parser.create('node', 'mpadded', [left], { height: '+.5em', width: '+.5em', voffset: '-.15em' });
  124. BussproofsUtil.setProperty(leftLabel, 'prooflabel', 'left');
  125. }
  126. if (right) {
  127. rightLabel = parser.create('node', 'mpadded', [right], { height: '+.5em', width: '+.5em', voffset: '-.15em' });
  128. BussproofsUtil.setProperty(rightLabel, 'prooflabel', 'right');
  129. }
  130. var children, label;
  131. if (left && right) {
  132. children = [leftLabel, rule, rightLabel];
  133. label = 'both';
  134. }
  135. else if (left) {
  136. children = [leftLabel, rule];
  137. label = 'left';
  138. }
  139. else if (right) {
  140. children = [rule, rightLabel];
  141. label = 'right';
  142. }
  143. else {
  144. return rule;
  145. }
  146. rule = parser.create('node', 'mrow', children);
  147. BussproofsUtil.setProperty(rule, 'labelledRule', label);
  148. return rule;
  149. }
  150. BussproofsMethods.Label = function (parser, name, side) {
  151. var top = parser.stack.Top();
  152. if (top.kind !== 'proofTree') {
  153. throw new TexError_js_1.default('IllegalProofCommand', 'Proof commands only allowed in prooftree environment.');
  154. }
  155. var content = ParseUtil_js_1.default.internalMath(parser, parser.GetArgument(name), 0);
  156. var label = (content.length > 1) ?
  157. parser.create('node', 'mrow', content, {}) : content[0];
  158. top.setProperty(side, label);
  159. };
  160. BussproofsMethods.SetLine = function (parser, _name, style, always) {
  161. var top = parser.stack.Top();
  162. if (top.kind !== 'proofTree') {
  163. throw new TexError_js_1.default('IllegalProofCommand', 'Proof commands only allowed in prooftree environment.');
  164. }
  165. top.setProperty('currentLine', style);
  166. if (always) {
  167. top.setProperty('line', style);
  168. }
  169. };
  170. BussproofsMethods.RootAtTop = function (parser, _name, where) {
  171. var top = parser.stack.Top();
  172. if (top.kind !== 'proofTree') {
  173. throw new TexError_js_1.default('IllegalProofCommand', 'Proof commands only allowed in prooftree environment.');
  174. }
  175. top.setProperty('rootAtTop', where);
  176. };
  177. BussproofsMethods.AxiomF = function (parser, name) {
  178. var top = parser.stack.Top();
  179. if (top.kind !== 'proofTree') {
  180. throw new TexError_js_1.default('IllegalProofCommand', 'Proof commands only allowed in prooftree environment.');
  181. }
  182. var line = parseFCenterLine(parser, name);
  183. BussproofsUtil.setProperty(line, 'axiom', true);
  184. top.Push(line);
  185. };
  186. function parseFCenterLine(parser, name) {
  187. var dollar = parser.GetNext();
  188. if (dollar !== '$') {
  189. throw new TexError_js_1.default('IllegalUseOfCommand', 'Use of %1 does not match it\'s definition.', name);
  190. }
  191. parser.i++;
  192. var axiom = parser.GetUpTo(name, '$');
  193. if (axiom.indexOf('\\fCenter') === -1) {
  194. throw new TexError_js_1.default('IllegalUseOfCommand', 'Missing \\fCenter in %1.', name);
  195. }
  196. var _a = __read(axiom.split('\\fCenter'), 2), prem = _a[0], conc = _a[1];
  197. var premise = (new TexParser_js_1.default(prem, parser.stack.env, parser.configuration)).mml();
  198. var conclusion = (new TexParser_js_1.default(conc, parser.stack.env, parser.configuration)).mml();
  199. var fcenter = (new TexParser_js_1.default('\\fCenter', parser.stack.env, parser.configuration)).mml();
  200. var left = parser.create('node', 'mtd', [premise], {});
  201. var middle = parser.create('node', 'mtd', [fcenter], {});
  202. var right = parser.create('node', 'mtd', [conclusion], {});
  203. var row = parser.create('node', 'mtr', [left, middle, right], {});
  204. var table = parser.create('node', 'mtable', [row], { columnspacing: '.5ex', columnalign: 'center 2' });
  205. BussproofsUtil.setProperty(table, 'sequent', true);
  206. parser.configuration.addNode('sequent', row);
  207. return table;
  208. }
  209. BussproofsMethods.FCenter = function (_parser, _name) { };
  210. BussproofsMethods.InferenceF = function (parser, name, n) {
  211. var top = parser.stack.Top();
  212. if (top.kind !== 'proofTree') {
  213. throw new TexError_js_1.default('IllegalProofCommand', 'Proof commands only allowed in prooftree environment.');
  214. }
  215. if (top.Size() < n) {
  216. throw new TexError_js_1.default('BadProofTree', 'Proof tree badly specified.');
  217. }
  218. var rootAtTop = top.getProperty('rootAtTop');
  219. var childCount = (n === 1 && !top.Peek()[0].childNodes.length) ? 0 : n;
  220. var children = [];
  221. do {
  222. if (children.length) {
  223. children.unshift(parser.create('node', 'mtd', [], {}));
  224. }
  225. children.unshift(parser.create('node', 'mtd', [top.Pop()], { 'rowalign': (rootAtTop ? 'top' : 'bottom') }));
  226. n--;
  227. } while (n > 0);
  228. var row = parser.create('node', 'mtr', children, {});
  229. var table = parser.create('node', 'mtable', [row], { framespacing: '0 0' });
  230. var conclusion = parseFCenterLine(parser, name);
  231. var style = top.getProperty('currentLine');
  232. if (style !== top.getProperty('line')) {
  233. top.setProperty('currentLine', top.getProperty('line'));
  234. }
  235. var rule = createRule(parser, table, [conclusion], top.getProperty('left'), top.getProperty('right'), style, rootAtTop);
  236. top.setProperty('left', null);
  237. top.setProperty('right', null);
  238. BussproofsUtil.setProperty(rule, 'inference', childCount);
  239. parser.configuration.addNode('inference', rule);
  240. top.Push(rule);
  241. };
  242. exports.default = BussproofsMethods;
  243. //# sourceMappingURL=BussproofsMethods.js.map