diff --git a/docs/assets/prooftree.js b/docs/assets/prooftree.js index da98fa6..73f6f86 100644 --- a/docs/assets/prooftree.js +++ b/docs/assets/prooftree.js @@ -4,41 +4,47 @@ const p = "bussproofs-html__", x = { paddingAxiomConclusion: 20, marginLabelLeft: 10, styleOnLoad: null -}, $ = (t) => ({ - marginPremises: t.marginPremises ?? x.marginPremises, - paddingAxiomConclusion: t.paddingAxiomConclusion ?? x.paddingAxiomConclusion, - marginLabelLeft: t.marginLabelLeft ?? x.marginLabelLeft, - styleOnLoad: t.styleOnLoad ?? x.styleOnLoad -}), B = (t) => `div.${p}proof-tree{width:max-content;margin:20px auto}div.${p}sequent{width:auto;text-align:center}div.${p}premises{width:auto;display:flex;flex-direction:row;gap:${t.marginPremises}px;align-items:flex-end}div.${p}horizontal-rule{width:100%;border-bottom:1.3px solid;position:relative}div.${p}horizontal-rule>.${p}right-label{position:absolute;height:auto;top:-50%;right:0;-webkit-transform:translateY(-50%);transform:translateY(-50%)}`, X = (t = x) => { +}, T = (t, e) => t === void 0 ? e : t, v = (t) => ({ + marginPremises: T(t.marginPremises, x.marginPremises), + paddingAxiomConclusion: T( + t.paddingAxiomConclusion, + x.paddingAxiomConclusion + ), + marginLabelLeft: T( + t.marginLabelLeft, + x.marginLabelLeft + ), + styleOnLoad: T(t.styleOnLoad, x.styleOnLoad) +}), B = (t) => `div.${p}proof-tree{width:max-content;margin:20px auto}div.${p}sequent{width:auto;text-align:center}div.${p}premises{width:auto;display:flex;flex-direction:row;gap:${t.marginPremises}px;align-items:flex-end}div.${p}horizontal-rule{width:100%;border-bottom:1.3px solid;position:relative}div.${p}horizontal-rule>.${p}right-label{position:absolute;height:auto;top:-50%;right:0;-webkit-transform:translateY(-50%);transform:translateY(-50%)}`, _ = (t = x) => { console.log(`renderProofTreesOnLoad(${JSON.stringify(t)})`), document.addEventListener("DOMContentLoaded", () => { - v(t); + I(t); }); -}, v = (t = x) => { +}, I = (t = x) => { console.log(`renderProofTrees(${JSON.stringify(t)})`); - const e = $(t), n = document.createElement("style"); + const e = v(t), n = document.createElement("style"); n.innerHTML = B(e), document.head.appendChild(n), Array.from( document.body.getElementsByTagName("P") ).filter( (o) => o.innerHTML.includes("\\begin{prooftree}") - ).forEach((o) => P(o, e)); -}, P = (t, e) => { + ).forEach((o) => V(o, e)); +}, V = (t, e) => { try { - const n = I(t); + const n = z(t); if (!n) throw new Error("cannot find fragment"); - const r = S(n); + const r = H(n); if (!r) throw new Error("error: cannot recognise latex command"); - const s = H(r); + const s = M(r); if (!s) throw new Error("error: cannot construct proof tree"); n == null || n.nodeList.slice(1).forEach((u) => { var i; return (i = u.parentNode) == null ? void 0 : i.removeChild(u); }); - const o = M(s); - t.insertBefore(n == null ? void 0 : n.beforeTextNode, n == null ? void 0 : n.nodeList[0]), t.insertBefore(o, n == null ? void 0 : n.nodeList[0]), t.insertBefore(n == null ? void 0 : n.afterTextNode, n == null ? void 0 : n.nodeList[0]), t.removeChild(n == null ? void 0 : n.nodeList[0]), e.styleOnLoad === null ? window.addEventListener("load", () => N(e, o), !1) : setTimeout(() => N(e, o), e.styleOnLoad), t.innerHTML.includes("\\begin{prooftree}") && P(t, e); + const o = R(s); + t.insertBefore(n == null ? void 0 : n.beforeTextNode, n == null ? void 0 : n.nodeList[0]), t.insertBefore(o, n == null ? void 0 : n.nodeList[0]), t.insertBefore(n == null ? void 0 : n.afterTextNode, n == null ? void 0 : n.nodeList[0]), t.removeChild(n == null ? void 0 : n.nodeList[0]), e.styleOnLoad === null ? window.addEventListener("load", () => P(e, o), !1) : setTimeout(() => P(e, o), e.styleOnLoad), t.innerHTML.includes("\\begin{prooftree}") && V(t, e); } catch (n) { console.error(n); } -}, C = (t, e) => { +}, N = (t, e) => { let n = -1, r = -1; for (let a = 0; a < e.length; a++) if (e[a].nodeType === Node.TEXT_NODE) { @@ -51,12 +57,12 @@ const p = "bussproofs-html__", x = { if (n === -1) return null; const s = e[r].nodeValue, o = s.slice(0, n), u = s.slice(n + t.length), i = document.createTextNode(o), f = document.createTextNode(u); return [r, i, f]; -}, I = (t) => { - const e = Array.from(t.childNodes), n = C("\\begin{prooftree}", e); +}, z = (t) => { + const e = Array.from(t.childNodes), n = N("\\begin{prooftree}", e); if (n === null) return null; const [r, s, o] = n, u = e.slice(r), i = [...u]; i.splice(0, 1, o); - const f = C("\\end{prooftree}", i); + const f = N("\\end{prooftree}", i); if (f === null) return null; const [a, l, m] = f, d = u.slice(0, a + 1), h = i; h.splice( @@ -73,16 +79,16 @@ const p = "bussproofs-html__", x = { beforeTextNode: s, afterTextNode: m }; -}, z = (t) => { +}, S = (t) => { t[0].nodeValue = t[0].nodeValue.trimStart(); -}, V = (t) => { +}, E = (t) => { const e = t[0].nodeValue.indexOf(` `); if (e !== -1) return t[0].nodeValue = t[0].nodeValue.substring(e + 1), !0; for (t.shift(); t.length > 0; ) if (t[0].nodeType !== Node.TEXT_NODE) t.shift(); - else return V(t); + else return E(t); return !1; }, c = (t, e) => { const n = t[0].nodeValue, r = n.indexOf("}"); @@ -95,14 +101,14 @@ const p = "bussproofs-html__", x = { else return c(t, e); return null; } -}, S = (t) => { +}, H = (t) => { const e = t.prtrNodeList; let n = [], r = 100; - for (; e.length > 0 && r-- > 0 && (z(e), e.length !== 0); ) { + for (; e.length > 0 && r-- > 0 && (S(e), e.length !== 0); ) { if (e[0].nodeType !== Node.TEXT_NODE) return null; const s = e[0].nodeValue; if (s.startsWith("%")) { - if (e[0].nodeValue = s.substring(1), !V(e)) return null; + if (e[0].nodeValue = s.substring(1), !E(e)) return null; } else if (s.startsWith("\\AXC{")) { e[0].nodeValue = s.substring(5); const o = c(e, []); @@ -159,14 +165,14 @@ const p = "bussproofs-html__", x = { return console.error("error: unrecognised charactor", e[0].nodeValue), null; } return n; -}, T = (t, e, n) => { +}, w = (t, e, n) => { const r = t[0]; if (!r) return null; let s = []; r.type === "RightLabel" && (t.shift(), s = r.body); const o = []; for (let u = 0; u < n; u++) { - const i = E(t); + const i = A(t); if (!i) return null; o.push(i); } @@ -176,40 +182,40 @@ const p = "bussproofs-html__", x = { rightLabel: s, conclusion: e }; -}, E = (t) => { +}, A = (t) => { const e = t.shift(); if (!e) return null; switch (e.type) { case "AXC": return { type: "Axiom", axiom: e.body }; case "UIC": - return T(t, e.body, 1); + return w(t, e.body, 1); case "BIC": - return T(t, e.body, 2); + return w(t, e.body, 2); case "TIC": - return T(t, e.body, 3); + return w(t, e.body, 3); case "QuaternaryInfC": - return T(t, e.body, 4); + return w(t, e.body, 4); } return null; -}, H = (t) => { - const e = E(t.reverse()); +}, M = (t) => { + const e = A(t.reverse()); return t.length > 0 ? null : e; }, y = (t, e) => { const n = document.createElement("div"); return n.classList.add(p + t), (t === "axiom" || t === "right-label" || t === "conclusion") && (n.style.width = "max-content"), e.forEach((r) => n.appendChild(r)), n; -}, A = (t) => { +}, W = (t) => { switch (t.type) { case "Axiom": return y("axiom", t.axiom); case "Sequent": return y("sequent", [ - y("premises", t.premises.map(A)), + y("premises", t.premises.map(W)), y("horizontal-rule", [y("right-label", t.rightLabel)]), y("conclusion", t.conclusion) ]); } -}, M = (t) => y("proof-tree", [A(t)]), R = (t) => t.reduce((e, n) => e + n, 0), W = (t) => { +}, R = (t) => y("proof-tree", [W(t)]), q = (t) => t.reduce((e, n) => e + n, 0), O = (t) => { switch (t.type) { case "PSAxiom": { t.node.style.width = `${t.prtrStyleAux.w}px`; @@ -217,11 +223,11 @@ const p = "bussproofs-html__", x = { } case "PSSequent": { const e = t.prtrStyleAux; - t.node.style.width = `${e.w}px`, t.nodePremises.style.marginLeft = `${e.mlp}px`, t.nodeHR.style.width = `${e.whr}px`, t.nodeHR.style.marginLeft = `${e.mlhr}px`, t.nodeHR.style.marginRight = `${e.mrhr}px`, t.nodeLabel.style.right = `-${e.widthL}px`, t.nodeConclusion.style.width = `${e.widthC}px`, t.nodeConclusion.style.marginLeft = `${e.mlc}px`, t.premises.forEach(W); + t.node.style.width = `${e.w}px`, t.nodePremises.style.marginLeft = `${e.mlp}px`, t.nodeHR.style.width = `${e.whr}px`, t.nodeHR.style.marginLeft = `${e.mlhr}px`, t.nodeHR.style.marginRight = `${e.mrhr}px`, t.nodeLabel.style.right = `-${e.widthL}px`, t.nodeConclusion.style.width = `${e.widthC}px`, t.nodeConclusion.style.marginLeft = `${e.mlc}px`, t.premises.forEach(O); return; } } -}, O = (t) => (e) => { +}, $ = (t) => (e) => { if (e.classList.contains(p + "axiom")) { const n = e.offsetWidth + 1 + t.paddingAxiomConclusion * 2; return { @@ -240,9 +246,9 @@ const p = "bussproofs-html__", x = { node: e }; } else if (e.classList.contains(p + "sequent")) { - const n = e.children[0], r = e.children[1], s = r.children[0], o = e.children[2], u = Array.prototype.slice.apply(n.children), i = o.children[0] ? o.children[0].offsetWidth + 1 + t.paddingAxiomConclusion * 2 : o.offsetWidth + 1 + t.paddingAxiomConclusion * 2, f = s.offsetWidth + t.marginLabelLeft, a = u.map(O(t)), l = a.map((d) => d.prtrStyleAux); + const n = e.children[0], r = e.children[1], s = r.children[0], o = e.children[2], u = Array.prototype.slice.apply(n.children), i = o.children[0] ? o.children[0].offsetWidth + 1 + t.paddingAxiomConclusion * 2 : o.offsetWidth + 1 + t.paddingAxiomConclusion * 2, f = s.offsetWidth + t.marginLabelLeft, a = u.map($(t)), l = a.map((d) => d.prtrStyleAux); u.length === 0 && console.error("error: empty premises", u); - const m = R(l.map((d) => d.w)) + t.marginPremises * (l.length - 1) - l[0].mlc - l[l.length - 1].mrc; + const m = q(l.map((d) => d.w)) + t.marginPremises * (l.length - 1) - l[0].mlc - l[l.length - 1].mrc; if (m > i) { const d = m, h = l[0].mlc, L = h + (m - i) / 2, b = Math.max(l[l.length - 1].mrc, f), g = b + (m - i) / 2; return { @@ -269,10 +275,10 @@ const p = "bussproofs-html__", x = { const d = i, h = Math.max(l[0].mlc - (i - m) / 2, 0), L = Math.max((i - m) / 2 - l[0].mlc, 0), b = h, g = Math.max( l[l.length - 1].mrc - (i - m) / 2, f - ), w = g; + ), C = g; return { type: "PSSequent", - prtrStyleAux: { w: d + h + g, whr: d, mlc: b, mrc: w, mlhr: h, mrhr: g, widthC: i, widthL: f, mlp: L }, + prtrStyleAux: { w: d + h + g, whr: d, mlc: b, mrc: C, mlhr: h, mrhr: g, widthC: i, widthL: f, mlp: L }, premises: a, node: e, nodePremises: n, @@ -283,11 +289,11 @@ const p = "bussproofs-html__", x = { } } else throw new Error("error"); -}, N = (t, e) => { - const n = O(t)(e.children[0]); - W(n); +}, P = (t, e) => { + const n = $(t)(e.children[0]); + O(n); }; export { - v as renderProofTrees, - X as renderProofTreesOnLoad + I as renderProofTrees, + _ as renderProofTreesOnLoad }; diff --git a/proof-tree/package.json b/proof-tree/package.json index 4e3e7ab..1959e6d 100644 --- a/proof-tree/package.json +++ b/proof-tree/package.json @@ -5,7 +5,7 @@ "type": "module", "scripts": { "dev": "vite", - "build": "tsc && vite build", + "build": "tsc --project tsconfig.json && vite build", "preview": "vite preview", "test": "jest" }, diff --git a/proof-tree/src/lib/prooftree/index.js b/proof-tree/src/lib/prooftree/index.js new file mode 100644 index 0000000..f58cde9 --- /dev/null +++ b/proof-tree/src/lib/prooftree/index.js @@ -0,0 +1,492 @@ +// import "./prooftree.css"; +console.log("ProofTree v0.0.1"); +const BH = "bussproofs-html__"; +const defaultConfig = { + marginPremises: 20, + paddingAxiomConclusion: 20, + marginLabelLeft: 10, + styleOnLoad: null, +}; +const initConfig = (configP) => { + var _a, _b, _c, _d; + return ({ + marginPremises: (_a = configP.marginPremises) !== null && _a !== void 0 ? _a : defaultConfig.marginPremises, + paddingAxiomConclusion: (_b = configP.paddingAxiomConclusion) !== null && _b !== void 0 ? _b : defaultConfig.paddingAxiomConclusion, + marginLabelLeft: (_c = configP.marginLabelLeft) !== null && _c !== void 0 ? _c : defaultConfig.marginLabelLeft, + styleOnLoad: (_d = configP.styleOnLoad) !== null && _d !== void 0 ? _d : defaultConfig.styleOnLoad, + }); +}; +const style = (cfg) => `div.${BH}proof-tree{width:max-content;margin:20px auto}div.${BH}sequent{width:auto;text-align:center}div.${BH}premises{width:auto;display:flex;flex-direction:row;gap:${cfg.marginPremises}px;align-items:flex-end}div.${BH}horizontal-rule{width:100%;border-bottom:1.3px solid;position:relative}div.${BH}horizontal-rule>.${BH}right-label{position:absolute;height:auto;top:-50%;right:0;-webkit-transform:translateY(-50%);transform:translateY(-50%)}`; +// Render proof trees on DOMContentLoaded. +export const renderProofTreesOnLoad = (configP = defaultConfig) => { + console.log(`renderProofTreesOnLoad(${JSON.stringify(configP)})`); + document.addEventListener("DOMContentLoaded", () => { + renderProofTrees(configP); + }); +}; +// Render proof trees. +export const renderProofTrees = (configP = defaultConfig) => { + console.log(`renderProofTrees(${JSON.stringify(configP)})`); + const config = initConfig(configP); + const styleElem = document.createElement("style"); + styleElem.innerHTML = style(config); + document.head.appendChild(styleElem); + const nodeArray = Array.from(document.body.getElementsByTagName("P")); + const nodes = nodeArray.filter((node) => node.innerHTML.includes("\\begin{prooftree}")); + nodes.forEach((node) => renderProofTree(node, config)); +}; +const renderProofTree = (node, config) => { + try { + const prtrFragment = getPrtrFragment(node); + if (!prtrFragment) + throw new Error("cannot find fragment"); + const ltxCommands = createLtxCommands(prtrFragment); + if (!ltxCommands) + throw new Error("error: cannot recognise latex command"); + const proofTree = parseProofTree(ltxCommands); + if (!proofTree) + throw new Error("error: cannot construct proof tree"); + prtrFragment === null || prtrFragment === void 0 ? void 0 : prtrFragment.nodeList.slice(1).forEach((node) => { var _a; return (_a = node.parentNode) === null || _a === void 0 ? void 0 : _a.removeChild(node); }); + const elem = createPrtrDom(proofTree); + node.insertBefore(prtrFragment === null || prtrFragment === void 0 ? void 0 : prtrFragment.beforeTextNode, prtrFragment === null || prtrFragment === void 0 ? void 0 : prtrFragment.nodeList[0]); + node.insertBefore(elem, prtrFragment === null || prtrFragment === void 0 ? void 0 : prtrFragment.nodeList[0]); + node.insertBefore(prtrFragment === null || prtrFragment === void 0 ? void 0 : prtrFragment.afterTextNode, prtrFragment === null || prtrFragment === void 0 ? void 0 : prtrFragment.nodeList[0]); + node.removeChild(prtrFragment === null || prtrFragment === void 0 ? void 0 : prtrFragment.nodeList[0]); + if (config.styleOnLoad === null) { + window.addEventListener("load", () => applyStyles(config, elem), false); + } + else { + setTimeout(() => applyStyles(config, elem), config.styleOnLoad); + } + if (node.innerHTML.includes("\\begin{prooftree}")) { + renderProofTree(node, config); + } + } + catch (e) { + console.error(e); + } +}; +const searchBeginEnd = (delimeter, nodes) => { + let jiBeginPT = -1; + let iBeginPT = -1; + for (let i = 0; i < nodes.length; i++) { + if (nodes[i].nodeType === Node.TEXT_NODE) { + const j = nodes[i].nodeValue.indexOf(delimeter); + if (j !== -1) { + iBeginPT = i; + jiBeginPT = j; + break; + } + } + } + if (jiBeginPT === -1) + return null; + const text = nodes[iBeginPT].nodeValue; + const beforeText = text.slice(0, jiBeginPT); + const afterBeginPTText = text.slice(jiBeginPT + delimeter.length); + const beforeTextNode = document.createTextNode(beforeText); + const afterBeginPTTextNode = document.createTextNode(afterBeginPTText); + return [iBeginPT, beforeTextNode, afterBeginPTTextNode]; +}; +const getPrtrFragment = (parentNode) => { + const nodes = Array.from(parentNode.childNodes); + const resultBegin = searchBeginEnd("\\begin{prooftree}", nodes); + if (resultBegin === null) + return null; + const [iBeginPT, beforeTextNode, afterBeginPTTextNode] = resultBegin; + const nodeList = nodes.slice(iBeginPT); + const prtrNodeList = [...nodeList]; + prtrNodeList.splice(0, 1, afterBeginPTTextNode); + const resultEnd = searchBeginEnd("\\end{prooftree}", prtrNodeList); + if (resultEnd === null) + return null; + const [iEndPT, beforeEndPTTextNode, afterTextNode] = resultEnd; + const nodeList2 = nodeList.slice(0, iEndPT + 1); + const prtrNodeList2 = prtrNodeList; + prtrNodeList2.splice(iEndPT, prtrNodeList.length - iEndPT, beforeEndPTTextNode); + const prtrNodeList3 = prtrNodeList2.filter((node) => node.nodeType !== Node.COMMENT_NODE); + const result3 = { + nodeList: nodeList2, + prtrNodeList: prtrNodeList3, + beforeTextNode: beforeTextNode, + afterTextNode: afterTextNode, + }; + return result3; +}; +const consumeSpaces = (nodes) => { + nodes[0].nodeValue = nodes[0].nodeValue.trimStart(); +}; +// もし true を返すなら，必ずテキストノードが先頭に来る． +const consumeComments = (nodes) => { + const i = nodes[0].nodeValue.indexOf("\n"); + if (i !== -1) { + nodes[0].nodeValue = nodes[0].nodeValue.substring(i + 1); + return true; + } + else { + nodes.shift(); + while (nodes.length > 0) { + if (nodes[0].nodeType !== Node.TEXT_NODE) + nodes.shift(); + else + return consumeComments(nodes); + } + return false; + } +}; +// もし true を返すなら，必ずテキストノードが先頭に来る． +const consumeLtxCommand = (nodes, acc) => { + const text = nodes[0].nodeValue; + const i = text.indexOf("}"); + if (i !== -1) { + const finalTextNode = document.createTextNode(text.slice(0, i)); + nodes[0].nodeValue = text.substring(i + 1); + acc.push(finalTextNode); + return acc; + } + else { + acc.push(nodes.shift()); + while (nodes.length > 0) { + if (nodes[0].nodeType !== Node.TEXT_NODE) + acc.push(nodes.shift()); + else + return consumeLtxCommand(nodes, acc); + } + return null; + } +}; +const createLtxCommands = (prtrFragment) => { + const nodes = prtrFragment.prtrNodeList; + let ltxCommands = []; + let i = 100; // A safeguard to prevent infinite loop (unnecessory) + while (nodes.length > 0 && i-- > 0) { + consumeSpaces(nodes); + if (nodes.length === 0) + break; + if (nodes[0].nodeType !== Node.TEXT_NODE) + return null; // unreachable. + const text = nodes[0].nodeValue; + if (text.startsWith("%")) { + nodes[0].nodeValue = text.substring(1); + if (!consumeComments(nodes)) + return null; + } + else if (text.startsWith("\\AXC{")) { + nodes[0].nodeValue = text.substring("\\AXC{".length); + const body = consumeLtxCommand(nodes, []); + if (body === null) + return null; + ltxCommands.push({ type: "AXC", body: body }); + } + else if (text.startsWith("\\UIC{")) { + nodes[0].nodeValue = text.substring("\\UIC{".length); + const body = consumeLtxCommand(nodes, []); + if (body === null) + return null; + ltxCommands.push({ type: "UIC", body: body }); + } + else if (text.startsWith("\\BIC{")) { + nodes[0].nodeValue = text.substring("\\BIC{".length); + const body = consumeLtxCommand(nodes, []); + if (body === null) + return null; + ltxCommands.push({ type: "BIC", body: body }); + } + else if (text.startsWith("\\TIC{")) { + nodes[0].nodeValue = text.substring("\\TIC{".length); + const body = consumeLtxCommand(nodes, []); + if (body === null) + return null; + ltxCommands.push({ type: "TIC", body: body }); + } + else if (text.startsWith("\\QuaternaryInfC{")) { + nodes[0].nodeValue = text.substring("\\QuaternaryInfC{".length); + const body = consumeLtxCommand(nodes, []); + if (body === null) + return null; + ltxCommands.push({ type: "QuaternaryInfC", body: body }); + } + else if (text.startsWith("\\RightLabel{")) { + nodes[0].nodeValue = text.substring("\\RightLabel{".length); + const body = consumeLtxCommand(nodes, []); + if (body === null) + return null; + ltxCommands.push({ type: "RightLabel", body: body }); + } + else if (text.startsWith("\\normalsize{")) { + nodes[0].nodeValue = text.substring("\\normalsize{".length); + const body = consumeLtxCommand(nodes, []); + if (body === null) + return null; + } + else if (text.startsWith("\\normalsize")) { + nodes[0].nodeValue = text.substring("\\normalsize".length); + } + else if (text.startsWith("\\small{")) { + nodes[0].nodeValue = text.substring("\\small{".length); + const body = consumeLtxCommand(nodes, []); + if (body === null) + return null; + } + else if (text.startsWith("\\small")) { + nodes[0].nodeValue = text.substring("\\small".length); + } + else if (text.startsWith("\\footnotesize{")) { + nodes[0].nodeValue = text.substring("\\footnotesize{".length); + const body = consumeLtxCommand(nodes, []); + if (body === null) + return null; + } + else if (text.startsWith("\\footnotesize")) { + nodes[0].nodeValue = text.substring("\\footnotesize".length); + } + else if (text.startsWith("\\scriptsize{")) { + nodes[0].nodeValue = text.substring("\\scriptsize{".length); + const body = consumeLtxCommand(nodes, []); + if (body === null) + return null; + } + else if (text.startsWith("\\scriptsize")) { + nodes[0].nodeValue = text.substring("\\scriptsize".length); + } + else if (text.startsWith("\\tiny{")) { + nodes[0].nodeValue = text.substring("\\tiny{".length); + const body = consumeLtxCommand(nodes, []); + if (body === null) + return null; + } + else if (text.startsWith("\\tiny")) { + nodes[0].nodeValue = text.substring("\\tiny".length); + } + else if (nodes[0].nodeValue.length === 0) { + // console.log("no more chars"); + // succeed + nodes.shift(); + } + else { + console.error("error: unrecognised charactor", nodes[0].nodeValue); + return null; + } + } + return ltxCommands; +}; +const parseHelper = (ltxCommands, conclusion, degree) => { + const nextLtxCommand = ltxCommands[0]; + if (!nextLtxCommand) + return null; + let rightLabel = []; + if (nextLtxCommand.type === "RightLabel") { + ltxCommands.shift(); + rightLabel = nextLtxCommand.body; + } + const premises = []; + for (let i = 0; i < degree; i++) { + const premise = parseProofTreeHelper(ltxCommands); + if (!premise) + return null; + premises.push(premise); + } + return { + type: "Sequent", + premises: premises.reverse(), + rightLabel: rightLabel, + conclusion: conclusion, + }; +}; +const parseProofTreeHelper = (ltxCommands) => { + const ltxCommand = ltxCommands.shift(); + if (!ltxCommand) + return null; + switch (ltxCommand.type) { + case "AXC": { + return { type: "Axiom", axiom: ltxCommand.body }; + } + case "UIC": { + return parseHelper(ltxCommands, ltxCommand.body, 1); + } + case "BIC": { + return parseHelper(ltxCommands, ltxCommand.body, 2); + } + case "TIC": { + return parseHelper(ltxCommands, ltxCommand.body, 3); + } + case "QuaternaryInfC": { + return parseHelper(ltxCommands, ltxCommand.body, 4); + } + } + return null; +}; +const parseProofTree = (ltxCommands) => { + const result = parseProofTreeHelper(ltxCommands.reverse()); + if (ltxCommands.length > 0) + return null; + else + return result; +}; +const div = (label, children) => { + const newDiv = document.createElement("div"); + newDiv.classList.add(BH + label); + if (label === "axiom" || label === "right-label" || label === "conclusion") { + newDiv.style.width = "max-content"; + } + children.forEach((node) => newDiv.appendChild(node)); + return newDiv; +}; +const createPrtrDomHelper = (prtrDom) => { + switch (prtrDom.type) { + case "Axiom": { + return div("axiom", prtrDom.axiom); + } + case "Sequent": { + return div("sequent", [ + div("premises", prtrDom.premises.map(createPrtrDomHelper)), + div("horizontal-rule", [div("right-label", prtrDom.rightLabel)]), + div("conclusion", prtrDom.conclusion), + ]); + } + } +}; +const createPrtrDom = (prtrDom) => div("proof-tree", [createPrtrDomHelper(prtrDom)]); +const sum = (nums) => nums.reduce((acc, x) => acc + x, 0); +const applyStylesToPrtr = (prtrStyle) => { + switch (prtrStyle.type) { + case "PSAxiom": { + prtrStyle.node.style.width = `${prtrStyle.prtrStyleAux.w}px`; + return; + } + case "PSSequent": { + const d = prtrStyle.prtrStyleAux; + prtrStyle.node.style.width = `${d.w}px`; + prtrStyle.nodePremises.style.marginLeft = `${d.mlp}px`; + prtrStyle.nodeHR.style.width = `${d.whr}px`; + prtrStyle.nodeHR.style.marginLeft = `${d.mlhr}px`; + prtrStyle.nodeHR.style.marginRight = `${d.mrhr}px`; + prtrStyle.nodeLabel.style.right = `-${d.widthL}px`; + prtrStyle.nodeConclusion.style.width = `${d.widthC}px`; + prtrStyle.nodeConclusion.style.marginLeft = `${d.mlc}px`; + prtrStyle.premises.forEach(applyStylesToPrtr); + return; + } + } +}; +const getPrtrStyle = (config) => (node) => { + if (node.classList.contains(BH + "axiom")) { + const width = node.offsetWidth + 1 + config.paddingAxiomConclusion * 2; + // console.log("axiom", width); + const prtrStyleAux = { + w: width, + whr: width, + mlc: 0, + mrc: 0, + mlhr: 0, + mrhr: 0, + widthC: width, + widthL: 0, + mlp: 0, + }; + const prtrStyle = { + type: "PSAxiom", + prtrStyleAux: prtrStyleAux, + node: node, + }; + return prtrStyle; + } + else if (node.classList.contains(BH + "sequent")) { + const nodePremises = node.children[0]; + const nodeHR = node.children[1]; + const nodeLabel = nodeHR.children[0]; + const nodeConclusion = node.children[2]; + const premises = Array.prototype.slice.apply(nodePremises.children); + const widthC = nodeConclusion.children[0] + ? nodeConclusion.children[0].offsetWidth + + 1 + + config.paddingAxiomConclusion * 2 + : nodeConclusion.offsetWidth + 1 + config.paddingAxiomConclusion * 2; + // console.log("widthC", widthC); + const widthL = nodeLabel.offsetWidth + config.marginLabelLeft; + const pss = premises.map(getPrtrStyle(config)); + const ps = pss.map((p) => p.prtrStyleAux); + if (premises.length === 0) { + console.error("error: empty premises", premises); + } + // $wpc(D) \triangleq + // \sum_{i}^{n} w(P_i) + margin \times (n - 1) - mlc(P_1) - mrc(P_n)$ + const wpc = sum(ps.map((pi) => pi.w)) + + config.marginPremises * (ps.length - 1) - + ps[0].mlc - + ps[ps.length - 1].mrc; + // console.log("wpc", wpc); + // $wpc(D) > width(C)$ + if (wpc > widthC) { + // $whr(D) \triangleq wpc(D)$ + const whr = wpc; + // $mlhr(D) \triangleq mlc(P_1)$ + const mlhr = ps[0].mlc; + // $mlc(D) \triangleq mlhr(D) + \dfrac{wpc(D) - width(C)}{2}$ + const mlc = mlhr + (wpc - widthC) / 2; + // console.log("mlc", mlc); + // $mrhr(D) \triangleq \max(mrc(P_n), width(L))$ + const mrhr = Math.max(ps[ps.length - 1].mrc, widthL); + // $mrc(D) \triangleq mrhr(D) + \dfrac{wpc(D) - width(C)}{2}$ + const mrc = mrhr + (wpc - widthC) / 2; + // $w(D) \triangleq whr(D) + mrhr(D) + mrhr(D)$ + const w = whr + mlhr + mrhr; + return { + type: "PSSequent", + prtrStyleAux: { + w, + whr, + mlc, + mrc, + mlhr, + mrhr, + widthC, + widthL, + mlp: 0, + }, + premises: pss, + node, + nodePremises, + nodeHR, + nodeLabel, + nodeConclusion, + }; + } + else { + // $wpc(D) < width(C)$ + // $whr(D) \triangleq width(C)$ + const whr = widthC; + // $mlhr(D) \triangleq mlc(P_1) - \dfrac{width(C) - wpc(D)}{2}$ + const mlhr = Math.max(ps[0].mlc - (widthC - wpc) / 2, 0); + // console.log("mlhr", mlhr); + const mlp = Math.max((widthC - wpc) / 2 - ps[0].mlc, 0); + // $mlc(D) \triangleq mlhr(D)$ + const mlc = mlhr; + // console.log("mlc", mlc); + // $mrhr(D) \triangleq + // \max(mrc(P_n) - \dfrac{width(C) - wpc(D)}{2}, width(L))$ + const mrhr = Math.max(ps[ps.length - 1].mrc - (widthC - wpc) / 2, widthL); + // $mrc(D) \triangleq mrhr(D)$ + const mrc = mrhr; + // $w(D) \triangleq whr(D) + mrhr(D) + mrhr(D)$ + const w = whr + mlhr + mrhr; + return { + type: "PSSequent", + prtrStyleAux: { w, whr, mlc, mrc, mlhr, mrhr, widthC, widthL, mlp }, + premises: pss, + node, + nodePremises, + nodeHR, + nodeLabel, + nodeConclusion, + }; + } + } + else { + throw new Error("error"); + } +}; +const applyStyles = (config, pt) => { + const prtrStyle = getPrtrStyle(config)(pt.children[0]); + applyStylesToPrtr(prtrStyle); +}; diff --git a/proof-tree/src/lib/prooftree/index.ts b/proof-tree/src/lib/prooftree/index.ts index 85c2db2..818f340 100644 --- a/proof-tree/src/lib/prooftree/index.ts +++ b/proof-tree/src/lib/prooftree/index.ts @@ -25,12 +25,19 @@ const defaultConfig: config = { styleOnLoad: null, }; +const maybe = (x: undefined | T, def: T): T => (x === undefined ? def : x); + const initConfig = (configP: configP) => ({ - marginPremises: configP.marginPremises ?? defaultConfig.marginPremises, - paddingAxiomConclusion: - configP.paddingAxiomConclusion ?? defaultConfig.paddingAxiomConclusion, - marginLabelLeft: configP.marginLabelLeft ?? defaultConfig.marginLabelLeft, - styleOnLoad: configP.styleOnLoad ?? defaultConfig.styleOnLoad, + marginPremises: maybe(configP.marginPremises, defaultConfig.marginPremises), + paddingAxiomConclusion: maybe( + configP.paddingAxiomConclusion, + defaultConfig.paddingAxiomConclusion + ), + marginLabelLeft: maybe( + configP.marginLabelLeft, + defaultConfig.marginLabelLeft + ), + styleOnLoad: maybe(configP.styleOnLoad, defaultConfig.styleOnLoad), }); const style = (cfg: config) => diff --git a/proof-tree/src/main.js b/proof-tree/src/main.js new file mode 100644 index 0000000..ad8de2a --- /dev/null +++ b/proof-tree/src/main.js @@ -0,0 +1,11 @@ +import "./style.css"; +import { renderProofTrees } from "./lib/prooftree"; +document.addEventListener("DOMContentLoaded", function () { + renderProofTrees(); +}); +// renderProofTreesOnLoad({ +// marginPremises: 100, +// paddingAxiomConclusion: 0, +// marginLabelLeft: 0, +// styleOnLoad: 100, +// }); diff --git a/proof-tree/tsconfig.json b/proof-tree/tsconfig.json index b48aac1..0e8c6ea 100644 --- a/proof-tree/tsconfig.json +++ b/proof-tree/tsconfig.json @@ -1,10 +1,10 @@ { "compilerOptions": { - "target": "ES2015", + "target": "es2015", "useDefineForClassFields": true, "module": "ESNext", "lib": [ - "ES2015", + "es2015", "DOM", "DOM.Iterable" ],