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 {ProofList} from "./AEG/ProofList";
 
 /**
  * Interface for an object describing Sheet of Assertion
@@ -38,8 +39,8 @@ interface atomObj {
  * @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 | AEGTree[]) {
+    const data = JSON.stringify(saveData, null, "\t");
 
     const writable = await handle.createWritable();
     await writable.write(data);
@@ -48,35 +49,63 @@ 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 {
+export function loadFile(
+    mode: "Draw" | "Proof",
+    fileData: string | ArrayBuffer | null
+): AEGTree | 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;
+        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: AEGTree[] = [];
+            data.forEach((tree: object) => {
+                const childData: (atomObj | cutObj)[] = (tree as sheetObj).internalSheet
+                    .internalChildren;
+                arr.push(toTree(childData));
+            });
+
+            return arr;
+        }
     }
 
     return null;
 }
 
+/**
+ * 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)[] = [];
+
+    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;
+}
+
 /**
  * Function that parses a Cut Object into a valid CutNode
  * @param data The Cut Object to be parsed

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
      */
     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;
     }

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

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;
     }
 
@@ -282,6 +314,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

src/AEG/ProofList.ts

@@ -0,0 +1,104 @@
+import {AEGTree} from "./AEGTree";
+import {ProofNode} from "./ProofNode";
+
+export class ProofList {
+    private internalHead: ProofNode = new ProofNode(new AEGTree());
+
+    public ProofList(node: ProofNode) {
+        this.internalHead = node;
+    }
+
+    public get head(): ProofNode {
+        return this.internalHead;
+    }
+
+    public set head(node: ProofNode) {
+        this.insertAtFirst(node);
+    }
+
+    public insertAtFirst(node: ProofNode) {
+        //If the head and the node to be inserted in first are both empty sheets, skip the head by
+        //setting the next of the node to be inserted as the next of head
+        //This is to avoid having 2 consecutive empty sheets
+        if (this.internalHead.tree.sheet.isEmptySheet() && node.tree.sheet.isEmptySheet()) {
+            node.next = this.internalHead.next;
+        } else {
+            this.internalHead.previous = node;
+            node.next = this.internalHead;
+            this.internalHead = node;
+        }
+    }
+
+    public insertAtEnd(node: ProofNode) {
+        const lastNode = this.getLastNode(this.internalHead);
+        //If the head and the node to be inserted at end are both empty sheets, skip the node by
+        //setting the next of the last node as the next of the node to be inserted
+        //This is to avoid having 2 consecutive empty sheets
+        if (lastNode.tree.sheet.isEmptySheet() && node.tree.sheet.isEmptySheet()) {
+            lastNode.next = node.next;
+        } else {
+            lastNode.next = node;
+            node.previous = lastNode;
+        }
+    }
+
+    public getLastNode(currentNode: ProofNode): ProofNode {
+        //If currentNode.next exists, recurse the function on currentNode.next to keep traversing
+        //the list. Otherwise, return currentNode -> if it has no next, it is the last node of list
+        if (currentNode.next === null) {
+            return currentNode;
+        } else {
+            return this.getLastNode(currentNode.next);
+        }
+    }
+
+    public deleteNode(node: ProofNode) {
+        if (node.previous === null) {
+            //If the node has no previous, it was the head node
+            //Set the head at the next of the node to be deleted
+            //If there was no next, initialize the head as a new proof node
+            this.internalHead = node.next ?? new ProofNode(new AEGTree());
+        } else {
+            //Set the next of the node before this node to the node after this node
+            node.previous.next = node.next;
+        }
+    }
+
+    /**
+     * Convert our proof list into an ordered array
+     * @returns An array of AEG Trees, in order of the proof
+     */
+    public toArray(): AEGTree[] {
+        const arr: AEGTree[] = [];
+        arr.push(this.head.tree);
+
+        if (this.head.next === null) {
+            return arr;
+        } else {
+            let nextNode: ProofNode | null = this.head.next;
+            do {
+                arr.push(nextNode.tree);
+                nextNode = nextNode.next;
+            } while (nextNode !== null);
+            return arr;
+        }
+    }
+
+    /**
+     * Builds a proof list from a given array of AEG Trees
+     * @param arr The array of AEG Trees in order, which will be used to construct our proof list
+     */
+    public rebuildFromArray(arr: AEGTree[] | null) {
+        if (arr !== null && arr.length !== 0) {
+            //Reset the proof list so that new list can be build
+            this.internalHead.tree = new AEGTree();
+            this.head.next = null;
+
+            let node: ProofNode;
+            arr.forEach(tree => {
+                node = new ProofNode(tree);
+                this.insertAtEnd(node);
+            });
+        }
+    }
+}

src/AEG/ProofNode.ts

@@ -0,0 +1,77 @@
+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;
+
+    /**
+     * The AEG Tree representing the previous state of the proof
+     */
+    public next: ProofNode | null = null;
+
+    /**
+     * The AEG Tree representing the next state of the proof
+     */
+    public previous: ProofNode | null = null;
+
+    /**
+     * 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 next (OPTIONAL) The AEG at the next state of the proof
+     * @param prev (OPTIONAL) The AEG at the previous state of the proof
+     */
+    public constructor(tree?: AEGTree, next?: ProofNode, prev?: ProofNode) {
+        this.tree = new AEGTree(tree?.sheet);
+        this.next = next ?? null;
+        this.previous = prev ?? null;
+    }
+
+    // /**
+    //  * Accessor that returns the AEG at the current state of the proof
+    //  */
+    // public get tree(): AEGTree | null {
+    //     return this.internalTree;
+    // }
+
+    // /**
+    //  * Modifier to set the AEG at the current state of the proof
+    //  */
+    // public set tree(tree: AEGTree | null) {
+    //     this.internalTree = tree;
+    // }
+
+    // /**
+    //  * Accessor that returns the AEG at the next state of the proof
+    //  */
+    // public get nextTree(): AEGTree | null {
+    //     return this.internalNextTree;
+    // }
+
+    // /**
+    //  * Modifier to set the AEG at the current state of the proof
+    //  */
+    // public set nextTree(tree: AEGTree | null) {
+    //     this.internalNextTree = tree;
+    // }
+
+    // /**
+    //  * Accessor that returns the AEG at the previous state of the proof
+    //  */
+    // public get previousTree(): AEGTree | null {
+    //     return this.internalPreviousTree;
+    // }
+
+    // /**
+    //  * Modifier to set the AEG at the current state of the proof
+    //  */
+    // public set previousTree(tree: AEGTree | null) {
+    //     this.internalPreviousTree = tree;
+    // }
+}