284 clear proofs

src/AEG/ProofNode.ts

@@ -1,3 +1,4 @@
+import {treeContext} from "../treeContext";
 import {AEGTree} from "./AEGTree";
 
 /**
@@ -10,8 +11,16 @@ export class ProofNode {
      */
     public tree: AEGTree;
 
+    /**
+     * The proof node's action that changed the proof
+     */
     public appliedRule: string;
 
+    /**
+     * The current location of this proof node in our proof array
+     */
+    public index: number;
+
     /**
      * 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.
@@ -21,5 +30,6 @@ export class ProofNode {
     public constructor(tree?: AEGTree, rule?: string) {
         this.appliedRule = rule ?? "";
         this.tree = new AEGTree(tree?.sheet);
+        this.index = treeContext.proof.length;
     }
 }

src/DrawModes/DragTool.ts

@@ -5,7 +5,7 @@
 
 import {Point} from "../AEG/Point";
 import {treeContext} from "../treeContext";
-import {redrawTree} from "./DrawUtils";
+import {redrawProof, redrawTree} from "./DrawUtils";
 
 //Original point later points will be compared to.
 let originPoint: Point;
@@ -32,7 +32,12 @@ export function dragMouseDown(event: MouseEvent) {
 export function dragMouseMove(event: MouseEvent) {
     if (!wasOut) {
         offset = new Point(event.x - originPoint.x, event.y - originPoint.y);
-        redrawTree(treeContext.tree);
+
+        if (treeContext.modeState === "Proof") {
+            redrawProof();
+        } else {
+            redrawTree(treeContext.tree);
+        }
     }
 }
 
@@ -41,5 +46,9 @@ export function dragMouseMove(event: MouseEvent) {
  */
 export function dragMosueOut() {
     wasOut = true;
-    redrawTree(treeContext.tree);
+    if (treeContext.modeState === "Proof") {
+        redrawProof();
+    } else {
+        redrawTree(treeContext.tree);
+    }
 }

src/DrawModes/DrawUtils.ts

@@ -151,10 +151,10 @@ export function redrawProof() {
     //If this is the first step taken in the proof,
     //set the current tree as the head of the proof history
     let tree: AEGTree;
-    if (treeContext.proofHistory.length === 0) {
+    if (treeContext.proof.length === 0 || treeContext.currentProofStep === undefined) {
         tree = new AEGTree();
     } else {
-        tree = treeContext.proofHistory[treeContext.proofHistory.length - 1].tree;
+        tree = treeContext.currentProofStep.tree;
     }
 
     cleanCanvas();

src/ProofHistory.ts

@@ -0,0 +1,88 @@
+/**
+ * Creates the history bar on the left side of the screen and handles returning to a previous state.
+ * @author Dawn Moore
+ */
+
+import {treeContext} from "./treeContext";
+import {redrawProof} from "./DrawModes/DrawUtils";
+import {ProofNode} from "./AEG/ProofNode";
+
+/**
+ * Creates a button representing the proof step allowing a user to return to that step.
+ * Creates a new row, a piece of text, and a button for it.
+ * @param newStep The newest step of our proof
+ */
+export function appendStep(newStep: ProofNode) {
+    const newDiv = document.createElement("div");
+    newDiv.className = "row";
+    newDiv.id = "Row: " + treeContext.proof.length;
+
+    //Create the new button with the function stepBack calling the step it represents
+    const button = document.createElement("button");
+    button.type = "button";
+    button.id = "Step: " + treeContext.proof.length;
+    button.className = "proofNodeButton";
+    button.title = newStep.tree.toString();
+    button.onclick = function () {
+        stepBack(newStep);
+    };
+
+    //Determine which action was just taken to give the button the corresponding icon.
+    const icon = document.createElement("Text");
+    switch (newStep.appliedRule) {
+        case "Single Move":
+            icon.className = "fa fa-mouse-pointer";
+            break;
+        case "Multi Move":
+            icon.className = "fa fa-arrows";
+            break;
+        case "Resize":
+            icon.className = "fa fa-arrows-alt";
+            break;
+        case "DC Insert":
+            icon.className = "fa fa-dot-circle-o";
+            break;
+        case "DC Delete":
+            icon.className = "fa fa-times-circle";
+            break;
+        case "Insertion":
+            icon.className = "fa fa-plus";
+            break;
+        case "Erasure":
+            icon.className = "fa fa-trash";
+            break;
+        case "Iteration":
+            icon.className = "fa fa-expand";
+            break;
+        case "Deiteration":
+            icon.className = "fa fa-compress";
+            break;
+        case "Pasted":
+            icon.className = "fa fa-files-o";
+            break;
+    }
+
+    button.appendChild(icon);
+    newDiv.appendChild(button);
+    document.getElementById("proofHistoryBar")?.appendChild(newDiv);
+}
+
+/**
+ * Sets the selected step to be the current step and redraws the canvas to represent this.
+ * This will be called when a button representing a proof step is pushed.
+ * @param selectedStep The selected proof Node that will become the current step
+ */
+export function stepBack(selectedStep: ProofNode) {
+    treeContext.currentProofStep = selectedStep;
+    redrawProof();
+}
+
+/**
+ * Removes buttons related to proof steps that are no longer a part of the proof.
+ * @param stopIndex The index to stop removing buttons.
+ */
+export function deleteButtons(stopIndex: number) {
+    for (let i = treeContext.proof.length; i > stopIndex + 1; i--) {
+        document.getElementById("Row: " + i)?.remove();
+    }
+}

src/ProofTools/ClearProofTool.ts

@@ -0,0 +1,55 @@
+/**
+ * File containing clear proof tool event handlers
+ * @author Anusha Tiwari
+ */
+
+import {treeContext} from "../treeContext";
+import {cleanCanvas, highlightNode, redrawProof} from "../DrawModes/DrawUtils";
+import {AEGTree} from "../AEG/AEGTree";
+import {illegalColor} from "../Themes";
+import {deleteButtons} from "../ProofHistory";
+
+//The current tree in the proof chain
+let currentProofTree: AEGTree;
+
+//Whether or not the node can be cleared
+let legalNode: boolean;
+
+/**
+ * Handles the mouseDown event for clearProofTool
+ * Gets the tree of the current step and highlights it in the illegal color
+ */
+export function clearProofMouseDown() {
+    //Get the tree of the current step
+    currentProofTree = new AEGTree();
+    if (treeContext.currentProofStep) {
+        currentProofTree.sheet = treeContext.currentProofStep.tree.sheet.copy();
+    }
+
+    //As long as we are within the canvas, we can legally perform clear
+    legalNode = true;
+    //Clear the canvas and redraw the tree in illegal color to show that it will be deleted
+    cleanCanvas();
+    highlightNode(currentProofTree.sheet, illegalColor());
+}
+
+/**
+ * Handles the mouseOut event for clearProofTool
+ * If we are within the canvas, delete the proof history buttons and clear the proof
+ */
+export function clearProofMouseUp() {
+    if (legalNode) {
+        deleteButtons(-1);
+        treeContext.clearProof();
+        redrawProof();
+    }
+}
+
+/**
+ * Handles the mouseOut event for clearProofTool
+ * If we move out of the canvas, the proof cannot be cleared
+ */
+export function clearProofMouseOut() {
+    legalNode = false;
+    redrawProof();
+}

src/ProofTools/DeiterationTool.ts

@@ -30,7 +30,10 @@ let currentProofTree: AEGTree;
  */
 export function deiterationMouseDown(event: MouseEvent) {
     const currentPoint: Point = new Point(event.x - offset.x, event.y - offset.y);
-    currentProofTree = new AEGTree(treeContext.getLastProofStep().tree.sheet);
+    currentProofTree = new AEGTree();
+    if (treeContext.currentProofStep) {
+        currentProofTree.sheet = treeContext.currentProofStep.tree.sheet.copy();
+    }
     currentNode = currentProofTree.getLowestNode(currentPoint);
 
     setLegal();
@@ -65,7 +68,7 @@ export function deiterationMouseUp(event: MouseEvent) {
             if (currentParent instanceof CutNode) {
                 currentParent.remove(currentPoint);
             }
-            treeContext.proofHistory.push(new ProofNode(currentProofTree, "Deiteration"));
+            treeContext.pushToProof(new ProofNode(currentProofTree, "Deiteration"));
         }
     }
 

src/ProofTools/DoubleCutDeletionTool.ts

@@ -28,7 +28,10 @@ let currentProofTree: AEGTree;
  */
 export function doubleCutDeletionMouseDown(event: MouseEvent) {
     const currentPoint: Point = new Point(event.x - offset.x, event.y - offset.y);
-    currentProofTree = new AEGTree(treeContext.getLastProofStep().tree.sheet);
+    currentProofTree = new AEGTree();
+    if (treeContext.currentProofStep) {
+        currentProofTree.sheet = treeContext.currentProofStep.tree.sheet.copy();
+    }
     currentNode = currentProofTree.getLowestNode(currentPoint);
 
     isLegal();
@@ -55,7 +58,7 @@ export function doubleCutDeletionMouseMove(event: MouseEvent) {
 export function doubleCutDeletionMouseUp(event: MouseEvent) {
     //Stores the tree of the previous proof so that we can perform double cut actions without
     //altering that tree
-    const nextProof = new ProofNode(currentProofTree, "Double Cut Deletion");
+    const nextProof = new ProofNode(currentProofTree, "DC Delete");
     const currentPoint: Point = new Point(event.x - offset.x, event.y - offset.y);
 
     if (legalNode && currentNode instanceof CutNode) {
@@ -67,8 +70,8 @@ export function doubleCutDeletionMouseUp(event: MouseEvent) {
             for (let i = 0; i < lowerCut.children.length; i++) {
                 nextProof.tree.insert(lowerCut.children[i]);
             }
+            treeContext.pushToProof(nextProof);
         }
-        treeContext.proofHistory.push(nextProof);
     }
 
     redrawProof();

src/ProofTools/DoubleCutInsertionTool.ts

@@ -31,7 +31,10 @@ let currentProofTree: AEGTree;
  */
 export function doubleCutInsertionMouseDown(event: MouseEvent) {
     startingPoint = new Point(event.clientX - offset.x, event.clientY - offset.y);
-    currentProofTree = new AEGTree(treeContext.getLastProofStep().tree.sheet);
+    currentProofTree = new AEGTree();
+    if (treeContext.currentProofStep) {
+        currentProofTree.sheet = treeContext.currentProofStep.tree.sheet.copy();
+    }
     wasOut = false;
 }
 
@@ -80,7 +83,7 @@ export function doubleCutInsertionMouseUp(event: MouseEvent) {
 
     //Stores the tree of the previous proof so that we can perform double cut actions without
     //altering that tree
-    const nextProof = new ProofNode(currentProofTree, "Double Cut Insertion");
+    const nextProof = new ProofNode(currentProofTree, "DC Insert");
 
     if (!wasOut && largeCut.ellipse !== null && smallCut.ellipse !== null) {
         //If either ellipse is in an invalid position or too small it cannot be inserted
@@ -93,7 +96,7 @@ export function doubleCutInsertionMouseUp(event: MouseEvent) {
         if (legal) {
             nextProof.tree.insert(largeCut);
             nextProof.tree.insert(smallCut);
-            treeContext.proofHistory.push(nextProof);
+            treeContext.pushToProof(nextProof);
         }
     }
     redrawProof();

src/ProofTools/ErasureTool.ts

@@ -29,7 +29,10 @@ let currentProofTree: AEGTree;
  */
 export function erasureMouseDown(event: MouseEvent) {
     const currentPoint: Point = new Point(event.x - offset.x, event.y - offset.y);
-    currentProofTree = new AEGTree(treeContext.getLastProofStep().tree.sheet);
+    currentProofTree = new AEGTree();
+    if (treeContext.currentProofStep) {
+        currentProofTree.sheet = treeContext.currentProofStep.tree.sheet.copy();
+    }
     currentNode = currentProofTree.getLowestNode(currentPoint);
 
     isLegal();
@@ -65,7 +68,7 @@ export function erasureMouseUp(event: MouseEvent) {
             currentParent.remove(currentPoint);
         }
 
-        treeContext.proofHistory.push(nextProof);
+        treeContext.pushToProof(nextProof);
         redrawProof();
     }
 

src/ProofTools/InsertionTools.ts

@@ -32,12 +32,15 @@ let legalNode: boolean;
 export function insertionMouseDown(event: MouseEvent) {
     //Create a deep copy of the tree we are trying to insert the incoming node into so that we can
     //modify it as needed without affecting the actual structure
-    currentTree = new AEGTree(treeContext.getLastProofStep().tree.sheet);
+    currentTree = new AEGTree();
+    if (treeContext.currentProofStep) {
+        currentTree.sheet = treeContext.currentProofStep.tree.sheet.copy();
+    }
     const selectedNodes = treeContext.selectForProof.sheet.children;
     const startingPoint = new Point(event.x - offset.x, event.y - offset.y);
 
     //we can insert only a single subgraph at a time
-    if (treeContext.proofHistory.length > 0 && selectedNodes.length === 1) {
+    if (treeContext.proof.length > 0 && selectedNodes.length === 1) {
         //As long as there are graphs to be placed, they are legal nodes
         legalNode = true;
         currentNode = selectedNodes[0];
@@ -225,7 +228,7 @@ export function insertionMouseUp(event: MouseEvent) {
                 currentTree.insert(tempAtom);
             }
             //Insertion is a new step -> push a new node in the proof, signifying it as such
-            treeContext.proofHistory.push(new ProofNode(currentTree, "Insertion"));
+            treeContext.pushToProof(new ProofNode(currentTree, "Insertion"));
         }
     }
     redrawProof();

src/ProofTools/IterationTool.ts

@@ -45,7 +45,10 @@ export function iterationMouseDown(event: MouseEvent) {
     //Make a deep copy of the tree of our latest proof step. Our iteration actions will be performed
     //on this structure, but they should all be on a new step - we do not want to make any changes
     //on the existing step
-    currentProofTree = new AEGTree(treeContext.getLastProofStep().tree.sheet);
+    currentProofTree = new AEGTree();
+    if (treeContext.currentProofStep) {
+        currentProofTree.sheet = treeContext.currentProofStep.tree.sheet.copy();
+    }
     startingPoint = new Point(event.x - offset.x, event.y - offset.y);
     currentNode = currentProofTree.getLowestNode(startingPoint);
     currentParent = currentProofTree.getLowestParent(startingPoint);
@@ -99,7 +102,7 @@ export function iterationMouseUp(event: MouseEvent) {
                 currentProofTree.insert(tempAtom);
             }
             //Iteration is a new step -> push a new node in the proof, signifying it as such
-            treeContext.proofHistory.push(new ProofNode(currentProofTree, "Iteration"));
+            treeContext.pushToProof(new ProofNode(currentProofTree, "Iteration"));
         }
     }
     redrawProof();