Skip to content
Snippets Groups Projects
Commit a42da19c authored by Jenny Zhang's avatar Jenny Zhang
Browse files

added linkSequentNode functions and tests. added isSequentNode,...

added linkSequentNode functions and tests. added isSequentNode, generateProofTreeHTML for the proof tree rendering
parent 848a3322
No related branches found
No related tags found
No related merge requests found
// Define sequentNode constructor function // Define sequentNode constructor function
function sequentNode(value, left, right) { // top is a list of string, for children nodes
this.value = value; // bottom is a string, for the current node
this.left = left; function sequentNode(bottom, rule = "", tops=[]) {
this.right = right; 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 // Define isSequentNode function to check if an object is an instance of sequentNode
function isSequentNode(obj) { function isSequentNode(obj) {
return obj instanceof sequentNode && return obj instanceof sequentNode &&
'value' in obj && typeof obj.rule === 'string' &&
'left' in obj && typeof obj.bottom === 'string' &&
'right' in obj; 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 // Define linkSequentNode function to link a new node to an existing node, prioritizing the left side
...@@ -23,18 +52,19 @@ function linkSequentNode(existingNode, newNode) { ...@@ -23,18 +52,19 @@ function linkSequentNode(existingNode, newNode) {
} }
// Prioritize linking to the left // Prioritize linking to the left
if (!existingNode.left) { if (existingNode.tops.length < 2) {
existingNode.left = newNode; existingNode.tops.push(newNode);
} else if (!existingNode.right) {
existingNode.right = newNode;
} else { } else {
// If both left and right nodes are occupied, recursively try to link to the left child node throw new Error('Addition failed, this node is already full');
linkSequentNode(existingNode.left, newNode);
} }
return existingNode;
} }
module.exports = { module.exports = {
sequentNode, sequentNode,
isSequentNode, isSequentNode,
linkSequentNode linkSequentNode,
generateProofTreeHTML,
addRule
}; };
\ No newline at end of file
const { parse } = require("../../src/utils/parser.js"); const { parse } = require("../../src/utils/parser.js");
const ast = require('../../src/utils/expAst.js/index.js'); const ast = require('../../src/utils/expAst.js');
// isNode test // isExpNode test
test('isNode could work correctly for node', () => { test('isNode could work correctly for node', () => {
const input = ast.Symbol("symbol", "A", null, null); const input = ast.Symbol("symbol", "A", null, null);
const output = ast.isNode(input); const output = ast.isExpNode(input);
expect(output).toEqual(true); expect(output).toEqual(true);
}); });
......
const { sequentNode, linkSequentNode } = require("../../src/utils/sequentAst.js");
// linkSequentNode test
test('linkSequentNode could work correctly for node', () => {
const inputA = new sequentNode("A");
const inputB = new sequentNode("B");
const output = linkSequentNode(inputA, inputB);
const expected = new sequentNode("A", "", [inputB]);
expect(output).toEqual(expected);
});
test('linkSequentNode could work correctly for node', () => {
const inputA = new sequentNode("A");
const inputB = new sequentNode("B");
const output = linkSequentNode(inputA, inputB);
const output1 = linkSequentNode(output, inputB);
expect(output1).toEqual(new sequentNode("A", "", [inputB, inputB]));
});
test('linkSequentNode could report error when adding nodes on a full node', () => {
const inputA = new sequentNode("A");
const inputB = new sequentNode("B");
const output = linkSequentNode(inputA, inputB);
const output1 = linkSequentNode(output, inputB);
expect(() => linkSequentNode(output1, inputB)).toThrow('Addition failed, this node is already full');
});
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment