228 save and load proofs as the history of aegs

src/AEG-IO.ts

@@ -3,6 +3,7 @@ import {AtomNode} from "./AEG/AtomNode";
 import {CutNode} from "./AEG/CutNode";
 import {Ellipse} from "./AEG/Ellipse";
 import {Point} from "./AEG/Point";
+import {ProofNode} from "./AEG/ProofNode";
 
 /**
  * Interface for an object describing Sheet of Assertion
@@ -33,13 +34,18 @@ interface atomObj {
     internalOrigin: {x: number; y: number};
 }
 
+interface nodeObj {
+    tree: sheetObj;
+    appliedRule: string;
+}
+
 /**
  * Function that creates and saves a file containing the given AEG data
  * @param handle The handler for the save file picker
  * @param aegData Serialized JSON string containing the AEG data
  */
-export async function saveFile(handle: FileSystemFileHandle, aegData: AEGTree) {
-    const data = JSON.stringify(aegData, null, "\t");
+export async function saveFile(handle: FileSystemFileHandle, saveData: AEGTree | ProofNode[]) {
+    const data = JSON.stringify(saveData, null, "\t");
 
     const writable = await handle.createWritable();
     await writable.write(data);
@@ -48,33 +54,54 @@ export async function saveFile(handle: FileSystemFileHandle, aegData: AEGTree) {
 
 /**
  * Function that takes in data read from a file and converts it into a valid AEG representation.
+ * @param mode The mode we are in (Draw mode or proof mode)
  * @param fileData The data read from a file.
- * @returns An AEG representation of the data.
+ * @returns If in draw mode, returns an AEG representation of the data.
+ * If in proof mode, constructs an array of AEGs read from the file.
+ * This can be used to build the proof list
  * Returns null if an error occurred
  */
-export function loadFile(fileData: string | ArrayBuffer | null): AEGTree | null {
-    if (typeof fileData === "string") {
-        const data: sheetObj = JSON.parse(fileData);
-        const childData: (atomObj | cutObj)[] = data.internalSheet.internalChildren;
-
-        const tree: AEGTree = new AEGTree();
-        const children: (AtomNode | CutNode)[] = [];
-
-        childData.forEach(child => {
-            if (Object.prototype.hasOwnProperty.call(child, "internalEllipse")) {
-                //make cut
-                children.push(toCut(child as cutObj));
-            } else {
-                //Make atom
-                children.push(toAtom(child as atomObj));
-            }
-        });
-
-        tree.sheet.children = children;
-        return tree;
+export function loadFile(mode: "Draw" | "Proof", fileData: string): AEGTree | ProofNode[] {
+    const data = JSON.parse(fileData);
+
+    if (mode === "Draw") {
+        const childData: (atomObj | cutObj)[] = (data as sheetObj).internalSheet.internalChildren;
+        return toTree(childData);
+    } else {
+        //Construct the tree at every step of the proof and store them in an array
+        const arr: ProofNode[] = [];
+
+        let node: nodeObj;
+        for (node of data) {
+            const childData: (atomObj | cutObj)[] = node.tree.internalSheet.internalChildren;
+            arr.push(new ProofNode(toTree(childData), node.appliedRule));
+        }
+
+        return arr;
+    }
+}
+
+/**
+ * Constructs an AEG from the array of JSON objects parsed from our file data.
+ * @param childData The array of objects which should be filled in as children of the tree.
+ * @returns An AEG Tree representation of our data.
+ */
+function toTree(childData: (atomObj | cutObj)[]): AEGTree {
+    const tree: AEGTree = new AEGTree();
+    const children: (AtomNode | CutNode)[] = [];
+
+    for (const child of childData) {
+        if (Object.prototype.hasOwnProperty.call(child, "internalEllipse")) {
+            //make cut
+            children.push(toCut(child as cutObj));
+        } else {
+            //Make atom
+            children.push(toAtom(child as atomObj));
+        }
     }
 
-    return null;
+    tree.sheet.children = children;
+    return tree;
 }
 
 /**
@@ -91,13 +118,13 @@ function toCut(data: cutObj): CutNode {
 
     const children: (AtomNode | CutNode)[] = [];
 
-    data.internalChildren.forEach(child => {
+    for (const child of data.internalChildren) {
         if ("internalEllipse" in child) {
             children.push(toCut(child));
         } else {
             children.push(toAtom(child));
         }
-    });
+    }
 
     return new CutNode(ellipse, children);
 }

src/AEG/AEGTree.ts

@@ -17,24 +17,21 @@ export class AEGTree {
     private internalSheet: CutNode;
 
     /**
-     * Method to construct a new AEG Tree.
-     * @param sheet If an existing sheet is passed, deep copy it to construct a new AEG Tree
+     * Constructs the sheet of assertion of the AEG tree
+     * @param sheet (OPTIONAL) An existing cut node which is to be used to construct the sheet of
+     * assertion of this AEG Tree. If given, creates a new tree with a deep copy of this node.
      */
     public constructor(sheet?: CutNode) {
-        //If we are constructing a new tree from a given sheet, deep copy the sheet and its children
-        //to ensure an entirely new tree is constructed.
-        this.internalSheet = new CutNode(null);
-        if (sheet instanceof CutNode) {
-            // this.internalSheet = new CutNode(sheet.ellipse);
-            if (sheet.children.length > 0) {
-                this.internalSheet.children = [...sheet.children];
-            }
+        if (sheet !== undefined) {
+            //If an existing cut node is passed, make a deep copy of it to copy over any children
+            this.internalSheet = sheet.copy();
+            //Ellipse of the sheet of assertion should be null
+            this.internalSheet.ellipse = null;
+        } else {
+            this.internalSheet = new CutNode(null);
         }
     }
 
-    /**
-     * Accessor to get the sheet of the AEG Tree
-     */
     public get sheet(): CutNode {
         return this.internalSheet;
     }
@@ -224,6 +221,17 @@ export class AEGTree {
         }
     }
 
+    /**
+     * Method that checks if an AEG Tree is equal to another AEG Tree. Trees are equal if they have
+     * the same children, irrespective of the ordering of nodes within a level
+     * @param otherTree The tree we want to check for equality with
+     * @returns True, if the trees are equal. Else, false
+     */
+    public isEqualTo(otherTree: AEGTree): boolean {
+        //For 2 trees to be equal, their sheet of assertion must be equal
+        return this.sheet.isEqualTo(otherTree.sheet);
+    }
+
     /**
      * Method that returns a string representation of the AEG Tree
      * @returns The structure formed by the cuts and atoms in this AEG Tree

src/AEG/AtomNode.ts

@@ -54,6 +54,19 @@ export class AtomNode {
         this.internalHeight = height;
     }
 
+    /**
+     * Creates a deep copy of this AtomNode
+     * @returns A new AtomNode, which is a deep copy of this node
+     */
+    public copy(): AtomNode {
+        return new AtomNode(
+            this.internalIdentifier,
+            new Point(this.internalOrigin.x, this.internalOrigin.y),
+            this.internalWidth,
+            this.internalHeight
+        );
+    }
+
     /**
      * Accessor to get the width of this Atom Node.
      * @returns The width of this Atom Node
@@ -150,4 +163,14 @@ export class AtomNode {
             this.internalHeight
         );
     }
+
+    /**
+     * Method that checks if an atom node is equal to another atom node. The are equal if they
+     * represent the same proposition.
+     * @param otherAtom The other atom node we are checking against for equality
+     * @returns True, if they are equal (the same). Else, false
+     */
+    public isEqualTo(otherAtom: AtomNode): boolean {
+        return this.identifier === otherAtom.identifier;
+    }
 }

src/AEG/CutNode.ts

@@ -32,6 +32,38 @@ export class CutNode {
         this.internalChildren = childList ?? [];
     }
 
+    /**
+     * Creates a deep copy of this CutNode
+     * @returns A new CutNode, which is a deep copy of this node
+     */
+    public copy(): CutNode {
+        let newEllipse: Ellipse | null;
+        const newChildren: (AtomNode | CutNode)[] = [];
+        if (this.ellipse !== null) {
+            newEllipse = new Ellipse(
+                new Point(this.ellipse.center.x, this.ellipse.center.y),
+                this.ellipse.radiusX,
+                this.ellipse.radiusY
+            );
+        } else {
+            newEllipse = null;
+        }
+
+        // Copy all the nested children individually
+        if (this.children.length > 0) {
+            for (let i = 0; i < this.children.length; i++) {
+                const newChild = this.children[i];
+                if (newChild instanceof AtomNode) {
+                    newChildren.push((newChild as AtomNode).copy());
+                } else {
+                    newChildren.push((newChild as CutNode).copy());
+                }
+            }
+        }
+
+        return new CutNode(newEllipse, newChildren);
+    }
+
     /**
      * Accessor to get the bounding ellipse of the Cut Node.
      * @returns The bounding ellipse of this Cut Node
@@ -44,7 +76,7 @@ export class CutNode {
     /**
      * Modifier to set the bounding ellipse of this Cut Node
      */
-    public set ellipse(ellipse: Ellipse) {
+    public set ellipse(ellipse: Ellipse | null) {
         this.internalEllipse = ellipse;
     }
 
@@ -289,6 +321,10 @@ export class CutNode {
         return str;
     }
 
+    public isEmptySheet(): boolean {
+        return this.internalEllipse === null && this.internalChildren.length === 0;
+    }
+
     /**
      * Constructs a string representation of an AEGTree or a subtree.
      * () - cut
@@ -315,4 +351,57 @@ export class CutNode {
         }
         return formulaString;
     }
+
+    /**
+     * Method that checks if a cut node is equal to another cut node. The are equal if they have
+     * the same children, irrespective of the ordering of nodes within a level
+     * @param otherCut The other cut node we are checking against for equality
+     * @returns True, if they are equal (the same). Else, false
+     */
+    public isEqualTo(otherCut: CutNode): boolean {
+        //For 2 cuts to be equal, they must have the same number of children
+        if (this.children.length === otherCut.children.length) {
+            if (this.children.length === 0) {
+                //If they do not have children, they are empty cuts
+                //Empty cuts are always equal
+                return true;
+            }
+            //If they have the same number of children, they should be the same children
+            //Make a deep copy and get the list of children of each cut
+            const thisChildren = this.copy().children;
+            const otherChildren = otherCut.copy().children;
+
+            //Iterate through the children of a cut and see if the other cut has the same child
+            //If they have the same child, remove it from the lists and continue
+            //If a child is not present in both, they are not equal
+            for (let i = 0; i < thisChildren.length; i++) {
+                for (let j = 0; j < otherChildren.length; j++) {
+                    if (
+                        (thisChildren[i] instanceof AtomNode &&
+                            otherChildren[j] instanceof AtomNode &&
+                            (thisChildren[i] as AtomNode).isEqualTo(
+                                otherChildren[j] as AtomNode
+                            )) ||
+                        (thisChildren[i] instanceof CutNode &&
+                            otherChildren[j] instanceof CutNode &&
+                            (thisChildren[i] as CutNode).isEqualTo(otherChildren[j] as CutNode))
+                    ) {
+                        thisChildren.splice(i, 1);
+                        otherChildren.splice(j, 1);
+                        i--;
+                        break;
+                    }
+
+                    if (j === otherChildren.length - 1) {
+                        //Checked all children but a match was not found. The nodes are not equal
+                        return false;
+                    }
+                }
+            }
+            //Check if all the children have been matched and returned
+            return thisChildren.length === 0 && otherChildren.length === 0;
+        }
+
+        return false;
+    }
 }

src/AEG/ProofNode.ts

@@ -0,0 +1,25 @@
+import {AEGTree} from "./AEGTree";
+
+/**
+ * The structure representing a single node of the proof
+ * @author Anusha Tiwari
+ */
+export class ProofNode {
+    /**
+     * The AEG Tree representing the current state of the proof
+     */
+    public tree: AEGTree;
+
+    public appliedRule: string;
+
+    /**
+     * Construct a proof node by providing the AEG Tree at the current state of the proof
+     * @param tree The AEG at the current state of the proof.
+     * If not defined, an empty AEG tree will be set constructed.
+     * @param rule The inference rule applied to get to this stage of the proof.
+     */
+    public constructor(tree?: AEGTree, rule?: string) {
+        this.appliedRule = rule ?? "";
+        this.tree = new AEGTree(tree?.sheet);
+    }
+}

src/DrawModes/CopyMultiTool.ts

@@ -52,7 +52,7 @@ export function copyMultiMouseMove(event: MouseEvent) {
 
         redrawTree(treeContext.tree);
         if (currentNode instanceof CutNode) {
-            const color = validateChildren(currentNode, moveDifference)
+            const color = validateChildren(treeContext.tree, currentNode, moveDifference)
                 ? legalColor()
                 : illegalColor();
             drawAltered(currentNode, color, moveDifference);
@@ -79,7 +79,7 @@ export function copyMultiMouseUp(event: MouseEvent) {
         );
 
         if (currentNode instanceof CutNode) {
-            if (validateChildren(currentNode, moveDifference)) {
+            if (validateChildren(treeContext.tree, currentNode, moveDifference)) {
                 insertChildren(currentNode, moveDifference);
             }
         } else if (currentNode instanceof AtomNode) {