Added containExpNode in expAsit.js in order to complement axiom rule in ndRules.js with tests

src/utils/expAst.js

@@ -15,6 +15,28 @@ function isExpNode(obj) {
         'right' in obj;
 }
 
+function containExpNode(asts, ast) {
+    for (let i = 0; i < asts.length; i++) {
+        if (toEqual(ast, asts[i])) {
+            return true;
+        }
+    }
+
+    return false;
+}
+
+function toEqual(node1, node2) {
+    if (node1.type !== node2.type) {
+        return false;
+    }
+
+    if (node1.type === 'symbol') {
+        return node1.value === node2.value;
+    }
+
+    return toEqual(node1.left, node2.left) && toEqual(node1.right, node2.right);
+}
+
 
 const precedence = {
   'imply': 1,
@@ -207,5 +229,6 @@ ast.astToString = astToString;
 ast.astToLaTeX = astToLaTeX;
 ast.astsToLateX = astsToLateX;
 ast.astsToString = astsToString;
+ast.containExpNode = containExpNode;
 
 module.exports = ast; // Export the AST module
\ No newline at end of file

src/utils/ndRules.js

@@ -173,6 +173,19 @@ function contradiction(input) {
     return [output];
 }
 
+// input list of list of ast, return list of sequents
+function axiom(input) {
+    const givens = input[0]; // list type, given list of sequent
+    const conclusion = input[1][0]; //list type of sequent
+
+    if (ast.containExpNode(givens, conclusion)) {
+        return [];
+    } else {
+        throw new Error("Invalid application for axiom rule: The list of formulas in left hand side of turnstile must contain the formula in right hand side of turnstile, to apply the imply introduction rule.");
+    }
+
+} 
+
 module.exports = {
     negationIntroduction,
     negationElimination,
@@ -184,5 +197,6 @@ module.exports = {
     orElimination,
     implyIntroduction,
     implyElimination,
-    contradiction
+    contradiction,
+    axiom
 };

tests/unit/ndRules.test.js

@@ -9,7 +9,8 @@ const { negationIntroduction,
     orElimination,
     implyIntroduction,
     implyElimination,
-    contradiction } = require('../../src/utils/ndRules');
+    contradiction,
+    axiom } = require('../../src/utils/ndRules');
 const { parse } = require("../../src/utils/parser");
 
 
@@ -218,3 +219,21 @@ test('Contradiction rule should return the correct premises', () => {
 
     expect(output).toEqual([parse("!A |- false")]);
 });
+
+
+//axiom
+test('Axiom rule should return the correct premises', () => {
+
+    const input = parse("B, A |- A");
+
+    const output = axiom(input);
+
+    expect(output).toEqual([parse("")]);
+});
+
+
+test('Axiom should throw an error for invalid application', () => {
+    const input = parse("|- !A & B");
+
+    expect(() => axiom(input)).toThrow("Invalid application for axiom rule: The list of formulas in left hand side of turnstile must contain the formula in right hand side of turnstile, to apply the imply introduction rule.");
+});
\ No newline at end of file