// Define sequentNode constructor function // top is a list of string, for children nodes // bottom is a string, for the current node function sequentNode(bottom, rule = "", tops=[]) { this.rule = rule; this.bottom = bottom; this.tops = tops; } function addRule(node, rule) { node.rule = rule; } function generateProofTreeHTML(node) { if (!node) return ''; // Generate the HTML for the current node let html = '<div class="node">'; if (node.rule) { html += '<div class="tops">'; // Recursively process prerequisite nodes node.tops.forEach(childNode => { html += generateProofTreeHTML(childNode); }); html += '</div>'; html += `<div class="bar"><div class="rule">\\(${node.rule}\\)</div></div>`; } html += `<div class="bottom"><span class="math">\\(${node.bottom}\\)</span></div>`; html += '</div>'; return html; } // Define isSequentNode function to check if an object is an instance of sequentNode function isSequentNode(obj) { return obj instanceof sequentNode && typeof obj.rule === 'string' && typeof obj.bottom === 'string' && Array.isArray(obj.tops) && obj.tops.every(top => top instanceof sequentNode); } // Define linkSequentNode function to link a new node to an existing node, prioritizing the left side function linkSequentNode(existingNode, newNode) { if (!isSequentNode(existingNode)) { throw new Error('Existing node must be a sequentNode'); } if (!isSequentNode(newNode)) { throw new Error('New node must be a sequentNode'); } // Prioritize linking to the left if (existingNode.tops.length < 2) { existingNode.tops.push(newNode); } else { throw new Error('Addition failed, this node is already full'); } return existingNode; } module.exports = { sequentNode, isSequentNode, linkSequentNode, generateProofTreeHTML, addRule };