BussproofsUtil.js 12 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329
  1. "use strict";
  2. var __read = (this && this.__read) || function (o, n) {
  3. var m = typeof Symbol === "function" && o[Symbol.iterator];
  4. if (!m) return o;
  5. var i = m.call(o), r, ar = [], e;
  6. try {
  7. while ((n === void 0 || n-- > 0) && !(r = i.next()).done) ar.push(r.value);
  8. }
  9. catch (error) { e = { error: error }; }
  10. finally {
  11. try {
  12. if (r && !r.done && (m = i["return"])) m.call(i);
  13. }
  14. finally { if (e) throw e.error; }
  15. }
  16. return ar;
  17. };
  18. var __values = (this && this.__values) || function(o) {
  19. var s = typeof Symbol === "function" && Symbol.iterator, m = s && o[s], i = 0;
  20. if (m) return m.call(o);
  21. if (o && typeof o.length === "number") return {
  22. next: function () {
  23. if (o && i >= o.length) o = void 0;
  24. return { value: o && o[i++], done: !o };
  25. }
  26. };
  27. throw new TypeError(s ? "Object is not iterable." : "Symbol.iterator is not defined.");
  28. };
  29. var __importDefault = (this && this.__importDefault) || function (mod) {
  30. return (mod && mod.__esModule) ? mod : { "default": mod };
  31. };
  32. var _a;
  33. Object.defineProperty(exports, "__esModule", { value: true });
  34. exports.clearDocument = exports.saveDocument = exports.makeBsprAttributes = exports.removeProperty = exports.getProperty = exports.setProperty = exports.balanceRules = void 0;
  35. var NodeUtil_js_1 = __importDefault(require("../NodeUtil.js"));
  36. var ParseUtil_js_1 = __importDefault(require("../ParseUtil.js"));
  37. var doc = null;
  38. var item = null;
  39. var getBBox = function (node) {
  40. item.root = node;
  41. var width = doc.outputJax.getBBox(item, doc).w;
  42. return width;
  43. };
  44. var getRule = function (node) {
  45. var i = 0;
  46. while (node && !NodeUtil_js_1.default.isType(node, 'mtable')) {
  47. if (NodeUtil_js_1.default.isType(node, 'text')) {
  48. return null;
  49. }
  50. if (NodeUtil_js_1.default.isType(node, 'mrow')) {
  51. node = node.childNodes[0];
  52. i = 0;
  53. continue;
  54. }
  55. node = node.parent.childNodes[i];
  56. i++;
  57. }
  58. return node;
  59. };
  60. var getPremises = function (rule, direction) {
  61. return rule.childNodes[direction === 'up' ? 1 : 0].childNodes[0].
  62. childNodes[0].childNodes[0].childNodes[0];
  63. };
  64. var getPremise = function (premises, n) {
  65. return premises.childNodes[n].childNodes[0].childNodes[0];
  66. };
  67. var firstPremise = function (premises) {
  68. return getPremise(premises, 0);
  69. };
  70. var lastPremise = function (premises) {
  71. return getPremise(premises, premises.childNodes.length - 1);
  72. };
  73. var getConclusion = function (rule, direction) {
  74. return rule.childNodes[direction === 'up' ? 0 : 1].childNodes[0].childNodes[0].childNodes[0];
  75. };
  76. var getColumn = function (inf) {
  77. while (inf && !NodeUtil_js_1.default.isType(inf, 'mtd')) {
  78. inf = inf.parent;
  79. }
  80. return inf;
  81. };
  82. var nextSibling = function (inf) {
  83. return inf.parent.childNodes[inf.parent.childNodes.indexOf(inf) + 1];
  84. };
  85. var previousSibling = function (inf) {
  86. return inf.parent.childNodes[inf.parent.childNodes.indexOf(inf) - 1];
  87. };
  88. var getParentInf = function (inf) {
  89. while (inf && (0, exports.getProperty)(inf, 'inference') == null) {
  90. inf = inf.parent;
  91. }
  92. return inf;
  93. };
  94. var getSpaces = function (inf, rule, right) {
  95. if (right === void 0) { right = false; }
  96. var result = 0;
  97. if (inf === rule) {
  98. return result;
  99. }
  100. if (inf !== rule.parent) {
  101. var children_1 = inf.childNodes;
  102. var index_1 = right ? children_1.length - 1 : 0;
  103. if (NodeUtil_js_1.default.isType(children_1[index_1], 'mspace')) {
  104. result += getBBox(children_1[index_1]);
  105. }
  106. inf = rule.parent;
  107. }
  108. if (inf === rule) {
  109. return result;
  110. }
  111. var children = inf.childNodes;
  112. var index = right ? children.length - 1 : 0;
  113. if (children[index] !== rule) {
  114. result += getBBox(children[index]);
  115. }
  116. return result;
  117. };
  118. var adjustValue = function (inf, right) {
  119. if (right === void 0) { right = false; }
  120. var rule = getRule(inf);
  121. var conc = getConclusion(rule, (0, exports.getProperty)(rule, 'inferenceRule'));
  122. var w = getSpaces(inf, rule, right);
  123. var x = getBBox(rule);
  124. var y = getBBox(conc);
  125. return w + ((x - y) / 2);
  126. };
  127. var addSpace = function (config, inf, space, right) {
  128. if (right === void 0) { right = false; }
  129. if ((0, exports.getProperty)(inf, 'inferenceRule') ||
  130. (0, exports.getProperty)(inf, 'labelledRule')) {
  131. var mrow = config.nodeFactory.create('node', 'mrow');
  132. inf.parent.replaceChild(mrow, inf);
  133. mrow.setChildren([inf]);
  134. moveProperties(inf, mrow);
  135. inf = mrow;
  136. }
  137. var index = right ? inf.childNodes.length - 1 : 0;
  138. var mspace = inf.childNodes[index];
  139. if (NodeUtil_js_1.default.isType(mspace, 'mspace')) {
  140. NodeUtil_js_1.default.setAttribute(mspace, 'width', ParseUtil_js_1.default.Em(ParseUtil_js_1.default.dimen2em(NodeUtil_js_1.default.getAttribute(mspace, 'width')) + space));
  141. return;
  142. }
  143. mspace = config.nodeFactory.create('node', 'mspace', [], { width: ParseUtil_js_1.default.Em(space) });
  144. if (right) {
  145. inf.appendChild(mspace);
  146. return;
  147. }
  148. mspace.parent = inf;
  149. inf.childNodes.unshift(mspace);
  150. };
  151. var moveProperties = function (src, dest) {
  152. var props = ['inference', 'proof', 'maxAdjust', 'labelledRule'];
  153. props.forEach(function (x) {
  154. var value = (0, exports.getProperty)(src, x);
  155. if (value != null) {
  156. (0, exports.setProperty)(dest, x, value);
  157. (0, exports.removeProperty)(src, x);
  158. }
  159. });
  160. };
  161. var adjustSequents = function (config) {
  162. var sequents = config.nodeLists['sequent'];
  163. if (!sequents) {
  164. return;
  165. }
  166. for (var i = sequents.length - 1, seq = void 0; seq = sequents[i]; i--) {
  167. if ((0, exports.getProperty)(seq, 'sequentProcessed')) {
  168. (0, exports.removeProperty)(seq, 'sequentProcessed');
  169. continue;
  170. }
  171. var collect = [];
  172. var inf = getParentInf(seq);
  173. if ((0, exports.getProperty)(inf, 'inference') !== 1) {
  174. continue;
  175. }
  176. collect.push(seq);
  177. while ((0, exports.getProperty)(inf, 'inference') === 1) {
  178. inf = getRule(inf);
  179. var premise = firstPremise(getPremises(inf, (0, exports.getProperty)(inf, 'inferenceRule')));
  180. var sequent = ((0, exports.getProperty)(premise, 'inferenceRule')) ?
  181. getConclusion(premise, (0, exports.getProperty)(premise, 'inferenceRule')) :
  182. premise;
  183. if ((0, exports.getProperty)(sequent, 'sequent')) {
  184. seq = sequent.childNodes[0];
  185. collect.push(seq);
  186. (0, exports.setProperty)(seq, 'sequentProcessed', true);
  187. }
  188. inf = premise;
  189. }
  190. adjustSequentPairwise(config, collect);
  191. }
  192. };
  193. var addSequentSpace = function (config, sequent, position, direction, width) {
  194. var mspace = config.nodeFactory.create('node', 'mspace', [], { width: ParseUtil_js_1.default.Em(width) });
  195. if (direction === 'left') {
  196. var row = sequent.childNodes[position].childNodes[0];
  197. mspace.parent = row;
  198. row.childNodes.unshift(mspace);
  199. }
  200. else {
  201. sequent.childNodes[position].appendChild(mspace);
  202. }
  203. (0, exports.setProperty)(sequent.parent, 'sequentAdjust_' + direction, width);
  204. };
  205. var adjustSequentPairwise = function (config, sequents) {
  206. var top = sequents.pop();
  207. while (sequents.length) {
  208. var bottom = sequents.pop();
  209. var _a = __read(compareSequents(top, bottom), 2), left = _a[0], right = _a[1];
  210. if ((0, exports.getProperty)(top.parent, 'axiom')) {
  211. addSequentSpace(config, left < 0 ? top : bottom, 0, 'left', Math.abs(left));
  212. addSequentSpace(config, right < 0 ? top : bottom, 2, 'right', Math.abs(right));
  213. }
  214. top = bottom;
  215. }
  216. };
  217. var compareSequents = function (top, bottom) {
  218. var tr = getBBox(top.childNodes[2]);
  219. var br = getBBox(bottom.childNodes[2]);
  220. var tl = getBBox(top.childNodes[0]);
  221. var bl = getBBox(bottom.childNodes[0]);
  222. var dl = tl - bl;
  223. var dr = tr - br;
  224. return [dl, dr];
  225. };
  226. var balanceRules = function (arg) {
  227. var e_1, _a;
  228. item = new arg.document.options.MathItem('', null, arg.math.display);
  229. var config = arg.data;
  230. adjustSequents(config);
  231. var inferences = config.nodeLists['inference'] || [];
  232. try {
  233. for (var inferences_1 = __values(inferences), inferences_1_1 = inferences_1.next(); !inferences_1_1.done; inferences_1_1 = inferences_1.next()) {
  234. var inf = inferences_1_1.value;
  235. var isProof = (0, exports.getProperty)(inf, 'proof');
  236. var rule = getRule(inf);
  237. var premises = getPremises(rule, (0, exports.getProperty)(rule, 'inferenceRule'));
  238. var premiseF = firstPremise(premises);
  239. if ((0, exports.getProperty)(premiseF, 'inference')) {
  240. var adjust_1 = adjustValue(premiseF);
  241. if (adjust_1) {
  242. addSpace(config, premiseF, -adjust_1);
  243. var w_1 = getSpaces(inf, rule, false);
  244. addSpace(config, inf, adjust_1 - w_1);
  245. }
  246. }
  247. var premiseL = lastPremise(premises);
  248. if ((0, exports.getProperty)(premiseL, 'inference') == null) {
  249. continue;
  250. }
  251. var adjust = adjustValue(premiseL, true);
  252. addSpace(config, premiseL, -adjust, true);
  253. var w = getSpaces(inf, rule, true);
  254. var maxAdjust = (0, exports.getProperty)(inf, 'maxAdjust');
  255. if (maxAdjust != null) {
  256. adjust = Math.max(adjust, maxAdjust);
  257. }
  258. var column = void 0;
  259. if (isProof || !(column = getColumn(inf))) {
  260. addSpace(config, (0, exports.getProperty)(inf, 'proof') ? inf : inf.parent, adjust - w, true);
  261. continue;
  262. }
  263. var sibling = nextSibling(column);
  264. if (sibling) {
  265. var pos = config.nodeFactory.create('node', 'mspace', [], { width: adjust - w + 'em' });
  266. sibling.appendChild(pos);
  267. inf.removeProperty('maxAdjust');
  268. continue;
  269. }
  270. var parentRule = getParentInf(column);
  271. if (!parentRule) {
  272. continue;
  273. }
  274. adjust = (0, exports.getProperty)(parentRule, 'maxAdjust') ?
  275. Math.max((0, exports.getProperty)(parentRule, 'maxAdjust'), adjust) : adjust;
  276. (0, exports.setProperty)(parentRule, 'maxAdjust', adjust);
  277. }
  278. }
  279. catch (e_1_1) { e_1 = { error: e_1_1 }; }
  280. finally {
  281. try {
  282. if (inferences_1_1 && !inferences_1_1.done && (_a = inferences_1.return)) _a.call(inferences_1);
  283. }
  284. finally { if (e_1) throw e_1.error; }
  285. }
  286. };
  287. exports.balanceRules = balanceRules;
  288. var property_prefix = 'bspr_';
  289. var blacklistedProperties = (_a = {},
  290. _a[property_prefix + 'maxAdjust'] = true,
  291. _a);
  292. var setProperty = function (node, property, value) {
  293. NodeUtil_js_1.default.setProperty(node, property_prefix + property, value);
  294. };
  295. exports.setProperty = setProperty;
  296. var getProperty = function (node, property) {
  297. return NodeUtil_js_1.default.getProperty(node, property_prefix + property);
  298. };
  299. exports.getProperty = getProperty;
  300. var removeProperty = function (node, property) {
  301. node.removeProperty(property_prefix + property);
  302. };
  303. exports.removeProperty = removeProperty;
  304. var makeBsprAttributes = function (arg) {
  305. arg.data.root.walkTree(function (mml, _data) {
  306. var attr = [];
  307. mml.getPropertyNames().forEach(function (x) {
  308. if (!blacklistedProperties[x] && x.match(RegExp('^' + property_prefix))) {
  309. attr.push(x + ':' + mml.getProperty(x));
  310. }
  311. });
  312. if (attr.length) {
  313. NodeUtil_js_1.default.setAttribute(mml, 'semantics', attr.join(';'));
  314. }
  315. });
  316. };
  317. exports.makeBsprAttributes = makeBsprAttributes;
  318. var saveDocument = function (arg) {
  319. doc = arg.document;
  320. if (!('getBBox' in doc.outputJax)) {
  321. throw Error('The bussproofs extension requires an output jax with a getBBox() method');
  322. }
  323. };
  324. exports.saveDocument = saveDocument;
  325. var clearDocument = function (_arg) {
  326. doc = null;
  327. };
  328. exports.clearDocument = clearDocument;
  329. //# sourceMappingURL=BussproofsUtil.js.map