From 2b833683ccd4bc1c17316d0e7c6fcd5fec2c4b16 Mon Sep 17 00:00:00 2001 From: AnushaTiwari5 Date: Fri, 10 Nov 2023 15:30:44 -0500 Subject: [PATCH 01/17] intial stages of proof history; committing before merging master --- src/AEG/AEGTree.ts | 14 +++++++- src/AEG/AtomNode.ts | 13 ++++++++ src/AEG/CutNode.ts | 34 +++++++++++++++++++- src/AEG/ProofNode.ts | 76 ++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 135 insertions(+), 2 deletions(-) create mode 100644 src/AEG/ProofNode.ts diff --git a/src/AEG/AEGTree.ts b/src/AEG/AEGTree.ts index 9ca523fd..2a73a500 100644 --- a/src/AEG/AEGTree.ts +++ b/src/AEG/AEGTree.ts @@ -13,8 +13,20 @@ import {shapesOverlap, shapesIntersect} from "./AEGUtils"; export class AEGTree { private internalSheet: CutNode; + /** + * 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) { - this.internalSheet = sheet ?? new CutNode(null); + 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); + } } public get sheet(): CutNode { diff --git a/src/AEG/AtomNode.ts b/src/AEG/AtomNode.ts index c3918d2a..881092b4 100644 --- a/src/AEG/AtomNode.ts +++ b/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 diff --git a/src/AEG/CutNode.ts b/src/AEG/CutNode.ts index ce925a9e..ac92f6bb 100644 --- a/src/AEG/CutNode.ts +++ b/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; } diff --git a/src/AEG/ProofNode.ts b/src/AEG/ProofNode.ts new file mode 100644 index 00000000..b51f79c2 --- /dev/null +++ b/src/AEG/ProofNode.ts @@ -0,0 +1,76 @@ +import {AEGTree} from "./AEGTree"; + +/** + * The structure representing a single node of the proof + * @author Anusha Tiwari + */ +export class ProofList { + /** + * The AEG Tree representing the current state of the proof + */ + private internalTree: AEGTree | null; + + /** + * The AEG Tree representing the previous state of the proof + */ + private internalNextTree: AEGTree | null; + + /** + * The AEG Tree representing the next state of the proof + */ + private internalPreviousTree: AEGTree | 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 + * @param nextTree (OPTIONAL) The AEG at the next state of the proof + * @param prevTree (OPTIONAL) The AEG at the previous state of the proof + */ + public constructor(tree: AEGTree, rule?: string, nextTree?: AEGTree, prevTree?: AEGTree) { + this.internalTree = tree ?? null; + this.internalNextTree = nextTree ?? null; + this.internalPreviousTree = prevTree ?? 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; + } +} From 7d877142a3b692843d3b9a7f1766a56d45fb7995 Mon Sep 17 00:00:00 2001 From: AnushaTiwari5 Date: Sun, 12 Nov 2023 18:25:51 -0500 Subject: [PATCH 02/17] proof history building --- src/AEG-IO.ts | 5 +- src/AEG/ProofList.ts | 63 ++++++++++++++++ src/AEG/ProofNode.ts | 95 +++++++++++++------------ src/DrawModes/ToProofMode.ts | 14 ++-- src/ProofTools/DoubleCutDeletionTool.ts | 1 + src/ToggleModes.ts | 29 ++++++-- src/index.ts | 28 ++++++-- src/treeContext.ts | 8 ++- 8 files changed, 179 insertions(+), 64 deletions(-) create mode 100644 src/AEG/ProofList.ts diff --git a/src/AEG-IO.ts b/src/AEG-IO.ts index 54a7e0c5..6fcb0424 100644 --- a/src/AEG-IO.ts +++ b/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 | ProofList) { + const data = JSON.stringify(saveData, null, "\t"); const writable = await handle.createWritable(); await writable.write(data); diff --git a/src/AEG/ProofList.ts b/src/AEG/ProofList.ts new file mode 100644 index 00000000..5f68bb76 --- /dev/null +++ b/src/AEG/ProofList.ts @@ -0,0 +1,63 @@ +//import {AEGTree} from "./AEGTree"; +import {ProofNode} from "./ProofNode"; + +export class ProofList { + private internalHead: ProofNode | null = null; + + public get head(): ProofNode | null { + return this.internalHead; + } + + public set head(node: ProofNode) { + this.insertAtFirst(node); + } + + public ProofList(node?: ProofNode) { + this.internalHead = node ?? null; + } + + public insertAtFirst(node: ProofNode) { + if (this.internalHead === null) { + this.internalHead = node; + } else { + this.internalHead.previous = node; + node.next = this.internalHead; + this.internalHead = node; + } + } + + public insertAtEnd(node: ProofNode) { + if (this.internalHead === null) { + this.internalHead = node; + } else { + const lastNode = this.getLastNode(this.internalHead); + 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 + return currentNode.next ? this.getLastNode(currentNode.next) : currentNode; + } + + 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 + this.internalHead = node.next; + } else { + //Set the next of the node before this node to the node after this node + node.previous.next = node.next; + } + } + + /* public toArray(): AEGTree[] { + const arr: AEGTree = []; //ERROR: Type 'never[]' is missing the following properties from type 'AEGTree': internalSheet, sheet, verify, verifyAEG, and 7 more + if (this.head === null) { + return arr; + } + + } */ +} diff --git a/src/AEG/ProofNode.ts b/src/AEG/ProofNode.ts index b51f79c2..dd588b16 100644 --- a/src/AEG/ProofNode.ts +++ b/src/AEG/ProofNode.ts @@ -4,73 +4,74 @@ import {AEGTree} from "./AEGTree"; * The structure representing a single node of the proof * @author Anusha Tiwari */ -export class ProofList { +export class ProofNode { /** * The AEG Tree representing the current state of the proof */ - private internalTree: AEGTree | null; + public tree: AEGTree; /** * The AEG Tree representing the previous state of the proof */ - private internalNextTree: AEGTree | null; + public next: ProofNode | null = null; /** * The AEG Tree representing the next state of the proof */ - private internalPreviousTree: AEGTree | null; + 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 - * @param nextTree (OPTIONAL) The AEG at the next state of the proof - * @param prevTree (OPTIONAL) The AEG at the previous 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, rule?: string, nextTree?: AEGTree, prevTree?: AEGTree) { - this.internalTree = tree ?? null; - this.internalNextTree = nextTree ?? null; - this.internalPreviousTree = prevTree ?? null; + public constructor(tree?: AEGTree, next?: ProofNode, prev?: ProofNode) { + this.tree = tree ?? new AEGTree(); + 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; - } + // /** + // * 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; - } + // /** + // * 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; - } + // /** + // * 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; - } + // /** + // * 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; - } + // /** + // * 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; - } + // /** + // * Modifier to set the AEG at the current state of the proof + // */ + // public set previousTree(tree: AEGTree | null) { + // this.internalPreviousTree = tree; + // } } diff --git a/src/DrawModes/ToProofMode.ts b/src/DrawModes/ToProofMode.ts index eda43936..c5b6dad3 100644 --- a/src/DrawModes/ToProofMode.ts +++ b/src/DrawModes/ToProofMode.ts @@ -28,20 +28,24 @@ let legalNode: boolean; * @param event The MouseDown event while in copy to proof mode */ export function toProofMouseDown(event: MouseEvent) { + //Reset our selectForProof tree to a blank AEG so that a new graph can be selected treeContext.selectForProof.sheet = new AEGTree().sheet; + selectPoint = new Point(event.x, event.y); selectedNode = treeContext.tree.getLowestNode(selectPoint); + const tempTree = new AEGTree(treeContext.tree.sheet); + if (selectedNode !== null) { legalNode = true; //Temporarily remove the selected part of the tree and highlight selected part only - if (selectedNode !== treeContext.tree.sheet) { - const tempParent = treeContext.tree.getLowestParent(selectPoint); + if (selectedNode !== tempTree.sheet) { + const tempParent = tempTree.getLowestParent(selectPoint); if (tempParent !== null) { tempParent.remove(selectPoint); } - redrawTree(treeContext.tree); + redrawTree(tempTree); } else { //If the entire tree is selected, clear the canvas and redraw entire tree in legalColor. cleanCanvas(); @@ -54,10 +58,10 @@ export function toProofMouseDown(event: MouseEvent) { highlightNode(selectedNode, legalColor()); } - //Add the selected part back into the tree + /* //Add the selected part back into the tree if (selectedNode !== treeContext.tree.sheet) { treeContext.tree.insert(selectedNode); - } + } */ } } diff --git a/src/ProofTools/DoubleCutDeletionTool.ts b/src/ProofTools/DoubleCutDeletionTool.ts index a1a537ac..b699027d 100644 --- a/src/ProofTools/DoubleCutDeletionTool.ts +++ b/src/ProofTools/DoubleCutDeletionTool.ts @@ -10,6 +10,7 @@ import {drawCut, redrawTree} from "../DrawModes/DrawUtils"; import {treeContext} from "../treeContext"; import {illegalColor} from "../Themes"; import {offset} from "../DrawModes/DragMode"; +import {ProofNode} from "../AEG/ProofNode"; //The node selected with the user mouse down. let currentNode: CutNode | AtomNode | null = null; diff --git a/src/ToggleModes.ts b/src/ToggleModes.ts index 89dd11b6..0128534f 100644 --- a/src/ToggleModes.ts +++ b/src/ToggleModes.ts @@ -5,6 +5,7 @@ */ import {loadFile} from "./AEG-IO"; import {AEGTree} from "./AEG/AEGTree"; +import {ProofNode} from "./AEG/ProofNode"; import {redrawTree} from "./DrawModes/DrawUtils"; // import {setMode} from "./index"; // import {selectedNode} from "./DrawModes/ToProofMode"; @@ -46,6 +47,7 @@ export function toggleHandler(): void { throw Error("invalid cached AEG"); } treeContext.toolState = drawCachedTool; + redrawTree(treeContext.tree); } else { //Display the buttons for Proof Mode drawButtons.style.display = "none"; @@ -57,22 +59,28 @@ export function toggleHandler(): void { //Load in our saved proof structure and tool state const loadedProof = loadFile(proofCachedAEG); + let proofTree: AEGTree; if (loadedProof !== null) { - treeContext.tree.sheet = loadedProof.sheet; + proofTree = new AEGTree(loadedProof.sheet); + //treeContext.tree.sheet = loadedProof.sheet; + //If the user selected something to be copied over from draw mode, //insert it into our existing proof structure for (let i = 0; i < treeContext.selectForProof.sheet.children.length; i++) { const child = treeContext.selectForProof.sheet.children[i]; try { - treeContext.tree.insert(child); + proofTree.insert(child); } catch (error) { console.log("Could not insert " + child); } } + + treeContext.proofHistory.insertAtEnd(new ProofNode(proofTree)); } else { //If there is no saved proof and the user selected something to be copied over from //draw mode, make that our proof structure - treeContext.tree.sheet = treeContext.selectForProof.sheet; + proofTree = new AEGTree(treeContext.selectForProof.sheet); + treeContext.proofHistory.insertAtEnd(new ProofNode(proofTree)); } //Reset the state of our tools @@ -80,6 +88,19 @@ export function toggleHandler(): void { //The selected node has been loaded in. //Reset it to avoid accidentally reloading it next time. treeContext.selectForProof.sheet = new AEGTree().sheet; + + if (treeContext.proofHistory.head !== null) { + const currentProof = treeContext.proofHistory.getLastNode( + treeContext.proofHistory.head + ).tree; + + if (currentProof !== null) { + redrawTree(currentProof); + } + } else { + treeContext.proofHistory.head = new ProofNode(new AEGTree()); + redrawTree(treeContext.proofHistory.head.tree); + } } - redrawTree(treeContext.tree); + // redrawTree(treeContext.tree); } diff --git a/src/index.ts b/src/index.ts index bbc8d1cd..e0f13687 100644 --- a/src/index.ts +++ b/src/index.ts @@ -74,6 +74,7 @@ import { doubleCutDeletionMouseOut, } from "./ProofTools/DoubleCutDeletionTool"; import {toggleHandler} from "./ToggleModes"; +import {ProofList} from "./AEG/ProofList"; //Setting up Canvas const canvas: HTMLCanvasElement = document.getElementById("canvas"); @@ -175,6 +176,12 @@ export function setMode(state: Tool) { cutTools.style.display = "none"; atomTools.style.display = "none"; + if (state <= 10) { + treeContext.modeState = "Draw"; + } else { + treeContext.modeState = "Proof"; + } + switch (treeContext.toolState) { case Tool.atomMode: atomTools.style.display = "block"; @@ -192,11 +199,22 @@ export function setMode(state: Tool) { * Calls the function to save the file. */ async function saveMode() { + let name: string; + let data: AEGTree | ProofList; + + if (treeContext.modeState === "Draw") { + name = "AEG Tree"; + data = treeContext.tree; + } else { + name = "Proof History"; + data = treeContext.proofHistory; + } + + //Slow Download if ("showSaveFilePicker" in window) { - //Slow Download const saveHandle = await window.showSaveFilePicker({ excludeAcceptAllOption: true, - suggestedName: "AEG Tree", + suggestedName: name, startIn: "downloads", types: [ { @@ -207,12 +225,12 @@ async function saveMode() { }, ], }); - saveFile(saveHandle, treeContext.tree); + saveFile(saveHandle, data); } else { //Quick Download const f = document.createElement("a"); - f.href = JSON.stringify(treeContext.tree, null, "\t"); - f.download = "AEGTree.json"; + f.href = JSON.stringify(data, null, "\t"); + f.download = name + ".json"; f.click(); } } diff --git a/src/treeContext.ts b/src/treeContext.ts index 07e8cd7f..21605f69 100644 --- a/src/treeContext.ts +++ b/src/treeContext.ts @@ -1,4 +1,5 @@ import {AEGTree} from "./AEG/AEGTree"; +import {ProofList} from "./AEG/ProofList"; // import {Tool} from "./index"; /** @@ -29,10 +30,15 @@ export class treeContext { //The current tree on the the canvas, needs to be redrawn upon any updates. public static tree: AEGTree = new AEGTree(); + //A history of the proof constructed + public static proofHistory: ProofList = new ProofList(); + //The node selected on draw mode which will copy over when we toggle to proof mode. public static selectForProof: AEGTree = new AEGTree(); //Used to determine the current mode the program is in. - //Modified via setState public static toolState: Tool = Tool.none; + + //An indicator of the mode that we are currently on + public static modeState: "Draw" | "Proof" = "Draw"; } From 4817dff02256cdd63b73df92e5e0d9b6485e1a2d Mon Sep 17 00:00:00 2001 From: AnushaTiwari5 Date: Sun, 12 Nov 2023 20:18:27 -0500 Subject: [PATCH 03/17] fixed bugs --- src/ProofTools/DoubleCutDeletionTool.ts | 2 +- src/ProofTools/ErasureTool.ts | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/ProofTools/DoubleCutDeletionTool.ts b/src/ProofTools/DoubleCutDeletionTool.ts index af685ce2..1e2ef4d6 100644 --- a/src/ProofTools/DoubleCutDeletionTool.ts +++ b/src/ProofTools/DoubleCutDeletionTool.ts @@ -92,7 +92,7 @@ function isDoubleCut(currentCut: CutNode): Boolean { return ( currentCut.children.length === 1 && currentCut.children[0] instanceof CutNode && - currentNode !== treeContext.tree.sheet + currentNode !== currentProofTree.sheet ); } diff --git a/src/ProofTools/ErasureTool.ts b/src/ProofTools/ErasureTool.ts index 027ea528..82dfb0d3 100644 --- a/src/ProofTools/ErasureTool.ts +++ b/src/ProofTools/ErasureTool.ts @@ -88,9 +88,9 @@ export function erasureMouseOut() { function isLegal() { //If the node is not the tree, is not null, and is even it is legal if ( - currentNode !== treeContext.tree.sheet && + currentNode !== currentProofTree.sheet && currentNode !== null && - treeContext.tree.getLevel(currentNode) % 2 === 0 + currentProofTree.getLevel(currentNode) % 2 === 0 ) { legalNode = true; highlightChildren(currentNode, illegalColor()); From df052e8c57391352e6a171cd2f26589bacd29570 Mon Sep 17 00:00:00 2001 From: AnushaTiwari5 Date: Sun, 12 Nov 2023 21:48:06 -0500 Subject: [PATCH 04/17] Proof working --- src/AEG-IO.ts | 70 +++++++++++++++++++++++++++++++------------- src/AEG/CutNode.ts | 4 +++ src/AEG/ProofList.ts | 54 ++++++++++++++++++++++++++++------ src/ToggleModes.ts | 39 +++++++++++++----------- src/index.ts | 16 +++++----- 5 files changed, 129 insertions(+), 54 deletions(-) diff --git a/src/AEG-IO.ts b/src/AEG-IO.ts index 6fcb0424..cbad5ef0 100644 --- a/src/AEG-IO.ts +++ b/src/AEG-IO.ts @@ -39,7 +39,7 @@ 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, saveData: AEGTree | ProofList) { +export async function saveFile(handle: FileSystemFileHandle, saveData: AEGTree | AEGTree[]) { const data = JSON.stringify(saveData, null, "\t"); const writable = await handle.createWritable(); @@ -49,35 +49,63 @@ export async function saveFile(handle: FileSystemFileHandle, saveData: 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 diff --git a/src/AEG/CutNode.ts b/src/AEG/CutNode.ts index dccff8c4..27d4c5d4 100644 --- a/src/AEG/CutNode.ts +++ b/src/AEG/CutNode.ts @@ -314,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 diff --git a/src/AEG/ProofList.ts b/src/AEG/ProofList.ts index 8ffdbac3..390c90ae 100644 --- a/src/AEG/ProofList.ts +++ b/src/AEG/ProofList.ts @@ -17,8 +17,11 @@ export class ProofList { } public insertAtFirst(node: ProofNode) { - if (this.internalHead === null) { - this.internalHead = node; + //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; @@ -27,10 +30,13 @@ export class ProofList { } public insertAtEnd(node: ProofNode) { - if (this.internalHead === null) { - this.internalHead = node; + 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 { - const lastNode = this.getLastNode(this.internalHead); lastNode.next = node; node.previous = lastNode; } @@ -58,11 +64,41 @@ export class ProofList { } } - /* public toArray(): AEGTree[] { - const arr: AEGTree = []; //ERROR: Type 'never[]' is missing the following properties from type 'AEGTree': internalSheet, sheet, verify, verifyAEG, and 7 more - if (this.head === null) { + /** + * 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); + }); + } + } } diff --git a/src/ToggleModes.ts b/src/ToggleModes.ts index 1f5a8e32..e81bf63f 100644 --- a/src/ToggleModes.ts +++ b/src/ToggleModes.ts @@ -34,13 +34,14 @@ export function toggleHandler(): void { //Display the buttons for Draw Mode drawButtons.style.display = "block"; proofButtons.style.display = "none"; + treeContext.modeState = "Draw"; //cache the proof tree and tool state so that we can load it back in when we toggle again - proofCachedAEG = JSON.stringify(treeContext.tree); + proofCachedAEG = JSON.stringify(treeContext.proofHistory.toArray()); proofCachedTool = treeContext.toolState; //Load in our saved draw tree and tool state - const loadedAEG = loadFile(drawCachedAEG); + const loadedAEG = loadFile(treeContext.modeState, drawCachedAEG) as AEGTree | null; if (loadedAEG !== null) { treeContext.tree.sheet = loadedAEG.sheet; } else { @@ -52,34 +53,39 @@ export function toggleHandler(): void { //Display the buttons for Proof Mode drawButtons.style.display = "none"; proofButtons.style.display = "block"; + treeContext.modeState = "Proof"; //cache the draw tree and tool state so that we can load it back in when we toggle again drawCachedAEG = JSON.stringify(treeContext.tree); drawCachedTool = treeContext.toolState; //Load in our saved proof structure and tool state - const loadedProof = loadFile(proofCachedAEG); - let proofTree: AEGTree; + const loadedProof = loadFile(treeContext.modeState, proofCachedAEG) as AEGTree[] | null; if (loadedProof !== null) { - proofTree = new AEGTree(loadedProof.sheet); - //treeContext.tree.sheet = loadedProof.sheet; + treeContext.proofHistory.rebuildFromArray(loadedProof); + //Construct the next tree from the last tree in the proof + const nextTree = new AEGTree( + treeContext.proofHistory.getLastNode(treeContext.proofHistory.head).tree.sheet + ); //If the user selected something to be copied over from draw mode, - //insert it into our existing proof structure - for (let i = 0; i < treeContext.selectForProof.sheet.children.length; i++) { - const child = treeContext.selectForProof.sheet.children[i]; - try { - proofTree.insert(child); - } catch (error) { - console.log("Could not insert " + child); + //insert it into the next tree + if (treeContext.selectForProof.sheet.children.length > 0) { + for (let i = 0; i < treeContext.selectForProof.sheet.children.length; i++) { + const child = treeContext.selectForProof.sheet.children[i]; + try { + nextTree.insert(child); + } catch (error) { + console.log("Could not insert " + child); + } } - } - treeContext.proofHistory.insertAtEnd(new ProofNode(proofTree)); + treeContext.proofHistory.insertAtEnd(new ProofNode(nextTree)); + } } else { //If there is no saved proof and the user selected something to be copied over from //draw mode, make that our proof structure - proofTree = new AEGTree(treeContext.selectForProof.sheet); + const proofTree = new AEGTree(treeContext.selectForProof.sheet); treeContext.proofHistory.insertAtEnd(new ProofNode(proofTree)); } @@ -91,5 +97,4 @@ export function toggleHandler(): void { redrawProof(); } - // redrawTree(treeContext.tree); } diff --git a/src/index.ts b/src/index.ts index a5251a43..14d86e62 100644 --- a/src/index.ts +++ b/src/index.ts @@ -16,7 +16,7 @@ import { atomMouseOut, } from "./DrawModes/AtomTool"; import {saveFile, loadFile} from "./AEG-IO"; -import {redrawTree} from "./DrawModes/DrawUtils"; +import {redrawProof, redrawTree} from "./DrawModes/DrawUtils"; import {dragMosueOut, dragMouseDown, dragMouseMove} from "./DrawModes/DragTool"; import { moveSingleMouseDown, @@ -80,7 +80,6 @@ import { erasureMouseOut, } from "./ProofTools/ErasureTool"; import {toggleHandler} from "./ToggleModes"; -import {ProofList} from "./AEG/ProofList"; import { resizeMouseDown, @@ -217,14 +216,14 @@ export function setTool(state: Tool) { */ async function saveMode() { let name: string; - let data: AEGTree | ProofList; + let data: AEGTree | AEGTree[]; if (treeContext.modeState === "Draw") { name = "AEG Tree"; data = treeContext.tree; } else { name = "Proof History"; - data = treeContext.proofHistory; + data = treeContext.proofHistory.toArray(); } //Slow Download @@ -274,10 +273,13 @@ async function loadMode() { const reader = new FileReader(); reader.addEventListener("load", () => { const aegData = reader.result; - const loadData = loadFile(aegData); - if (loadData instanceof AEGTree) { - treeContext.tree = loadData; + const loadData = loadFile(treeContext.modeState, aegData); + if (treeContext.modeState === "Draw") { + treeContext.tree = loadData as AEGTree; redrawTree(treeContext.tree); + } else if (treeContext.modeState === "Proof") { + treeContext.proofHistory.rebuildFromArray(loadData as AEGTree[]); + redrawProof(); } //TODO: else popup error }); From e91963f8ad91a46f0f927ac605dc36c2ff754972 Mon Sep 17 00:00:00 2001 From: AnushaTiwari5 Date: Tue, 14 Nov 2023 23:05:43 -0500 Subject: [PATCH 05/17] new proof structure using ts array --- src/AEG-IO.ts | 20 +++-- src/AEG/ProofNode.ts | 60 +------------ src/DrawModes/DrawUtils.ts | 25 ++++-- .../{ToProofMode.ts => copyFromDraw.ts} | 84 ++++++++----------- src/ProofTools/DoubleCutDeletionTool.ts | 6 +- src/ProofTools/DoubleCutInsertionTool.ts | 8 +- src/ProofTools/ErasureTool.ts | 6 +- src/ToggleModes.ts | 12 +-- src/index.ts | 15 ++-- src/treeContext.ts | 6 +- 10 files changed, 100 insertions(+), 142 deletions(-) rename src/DrawModes/{ToProofMode.ts => copyFromDraw.ts} (73%) diff --git a/src/AEG-IO.ts b/src/AEG-IO.ts index cbad5ef0..56733fdc 100644 --- a/src/AEG-IO.ts +++ b/src/AEG-IO.ts @@ -3,7 +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"; +import {ProofNode} from "./AEG/ProofNode"; /** * Interface for an object describing Sheet of Assertion @@ -34,12 +34,17 @@ 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, saveData: AEGTree | AEGTree[]) { +export async function saveFile(handle: FileSystemFileHandle, saveData: AEGTree | ProofNode[]) { const data = JSON.stringify(saveData, null, "\t"); const writable = await handle.createWritable(); @@ -59,7 +64,7 @@ export async function saveFile(handle: FileSystemFileHandle, saveData: AEGTree | export function loadFile( mode: "Draw" | "Proof", fileData: string | ArrayBuffer | null -): AEGTree | AEGTree[] | null { +): AEGTree | ProofNode[] | null { if (typeof fileData === "string") { const data = JSON.parse(fileData); @@ -69,11 +74,10 @@ export function loadFile( 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)); + const arr: ProofNode[] = []; + data.forEach((node: nodeObj) => { + const childData: (atomObj | cutObj)[] = node.tree.internalSheet.internalChildren; + arr.push(new ProofNode(toTree(childData), node.appliedRule)); }); return arr; diff --git a/src/AEG/ProofNode.ts b/src/AEG/ProofNode.ts index e57091bb..cf235f63 100644 --- a/src/AEG/ProofNode.ts +++ b/src/AEG/ProofNode.ts @@ -10,68 +10,16 @@ export class ProofNode { */ 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; + 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 next (OPTIONAL) The AEG at the next state of the proof - * @param prev (OPTIONAL) The AEG at the previous state of the proof + * @param rule The inference rule applied to get to this stage of the proof. */ - public constructor(tree?: AEGTree, next?: ProofNode, prev?: ProofNode) { + public constructor(tree?: AEGTree, rule?: string) { + this.appliedRule = rule ?? ""; 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; - // } } diff --git a/src/DrawModes/DrawUtils.ts b/src/DrawModes/DrawUtils.ts index 33d655a3..563bdf76 100644 --- a/src/DrawModes/DrawUtils.ts +++ b/src/DrawModes/DrawUtils.ts @@ -11,7 +11,6 @@ import {treeContext} from "../treeContext"; import {offset} from "./DragTool"; import {placedColor} from "../Themes"; import {AEGTree} from "../AEG/AEGTree"; -import {ProofNode} from "../AEG/ProofNode"; //Setting up Canvas const canvas: HTMLCanvasElement = document.getElementById("canvas"); @@ -148,10 +147,26 @@ function redrawAtom(incomingNode: AtomNode) { export function redrawProof() { //If this is the first step taken in the proof, //set the current tree as the head of the proof history - if (treeContext.proofHistory.head === null) { - treeContext.proofHistory.head = new ProofNode(treeContext.tree); + let tree: AEGTree; + if (treeContext.proofHistory.length === 0) { + tree = new AEGTree(); + } else { + tree = treeContext.proofHistory[treeContext.proofHistory.length - 1].tree; } - //Get the last step in the history and draw its tree - redrawTree(treeContext.proofHistory.getLastNode(treeContext.proofHistory.head).tree); + redrawTree(tree); +} + +/** + * Helper function to highlight the specific selected node + */ +export function highlightNode(child: AtomNode | CutNode, color: string) { + if (child instanceof AtomNode) { + drawAtom(child, color, true); + } else if (child instanceof CutNode) { + drawCut(child, color); + for (let i = 0; i < child.children.length; i++) { + highlightNode(child.children[i], color); + } + } } diff --git a/src/DrawModes/ToProofMode.ts b/src/DrawModes/copyFromDraw.ts similarity index 73% rename from src/DrawModes/ToProofMode.ts rename to src/DrawModes/copyFromDraw.ts index 1b56ea58..64d4ab5f 100644 --- a/src/DrawModes/ToProofMode.ts +++ b/src/DrawModes/copyFromDraw.ts @@ -7,13 +7,13 @@ import {Point} from "../AEG/Point"; import {AtomNode} from "../AEG/AtomNode"; import {CutNode} from "../AEG/CutNode"; import {treeContext} from "../treeContext"; -// import {offset} from "./DragMode"; -import {drawAtom, drawCut, cleanCanvas, redrawTree} from "./DrawUtils"; +import {offset} from "./DragTool"; +import {drawAtom, drawCut, cleanCanvas, redrawTree, highlightNode} from "./DrawUtils"; import {legalColor} from "../Themes"; import {AEGTree} from "../AEG/AEGTree"; //The initial point the user pressed down. -let selectPoint: Point; +let startingPoint: Point; //The current node and its children we will be moving. let selectedNode: CutNode | AtomNode | null = null; @@ -21,6 +21,9 @@ let selectedNode: CutNode | AtomNode | null = null; //Whether or not the node is allowed to be selected. let legalNode: boolean; +//A deep copy of the global tree +const tempTree = new AEGTree(treeContext.tree.sheet); + /** * Handles the MouseDown event while in copy to proof mode. * Gets the lowest node on the tree at the point identified by the MouseDown event. @@ -31,48 +34,23 @@ export function toProofMouseDown(event: MouseEvent) { //Reset our selectForProof tree to a blank AEG so that a new graph can be selected treeContext.selectForProof.sheet = new AEGTree().sheet; - selectPoint = new Point(event.x, event.y); - selectedNode = treeContext.tree.getLowestNode(selectPoint); - - const tempTree = new AEGTree(treeContext.tree.sheet); - - if (selectedNode !== null) { - legalNode = true; - - //Temporarily remove the selected part of the tree and highlight selected part only - if (selectedNode !== tempTree.sheet) { - const tempParent = tempTree.getLowestParent(selectPoint); - if (tempParent !== null) { - tempParent.remove(selectPoint); - } - redrawTree(tempTree); - } else { - //If the entire tree is selected, clear the canvas and redraw entire tree in legalColor. - cleanCanvas(); - } - - //Highlight the selected part by redrawing in legalColor - if (selectedNode instanceof AtomNode) { - drawAtom(selectedNode, legalColor(), true); - } else { - highlightNode(selectedNode, legalColor()); - } + startingPoint = new Point(event.x - offset.x, event.y - offset.y); + selectedNode = treeContext.tree.getLowestNode(startingPoint); - /* //Add the selected part back into the tree - if (selectedNode !== treeContext.tree.sheet) { - treeContext.tree.insert(selectedNode); - } */ - } + isLegal(); } /** * Handles the MouseMove event while in copy to proof mode. * Currently MouseMove does not allow for node selection. (Can be changed as per team review) */ -export function toProofMouseMove() { - selectedNode = null; - legalNode = false; +export function toProofMouseMove(event: MouseEvent) { redrawTree(treeContext.tree); + + const movePoint: Point = new Point(event.x - offset.x, event.y - offset.y); + selectedNode = treeContext.tree.getLowestNode(movePoint); + + isLegal(); } /** @@ -104,16 +82,28 @@ export function toProofMouseOut() { redrawTree(treeContext.tree); } -/** - * Helper function to highlight the specific selected node - */ -function highlightNode(child: AtomNode | CutNode, color: string) { - if (child instanceof AtomNode) { - drawAtom(child, color, true); - } else if (child instanceof CutNode) { - drawCut(child, color); - for (let i = 0; i < child.children.length; i++) { - highlightNode(child.children[i], color); +function isLegal() { + if (selectedNode !== null) { + legalNode = true; + + //Temporarily remove the selected part of the tree and highlight selected part only + //NEED TREE EQUALITY DONE TO COMPARE DEEP COPY + if (selectedNode !== tempTree.sheet) { + const tempParent = tempTree.getLowestParent(startingPoint); + if (tempParent !== null) { + tempParent.remove(startingPoint); + } + redrawTree(tempTree); + } else { + //If the entire tree is selected, clear the canvas and redraw entire tree in legalColor. + cleanCanvas(); + } + + //Highlight the selected part by redrawing in legalColor + if (selectedNode instanceof AtomNode) { + drawAtom(selectedNode, legalColor(), true); + } else { + highlightNode(selectedNode, legalColor()); } } } diff --git a/src/ProofTools/DoubleCutDeletionTool.ts b/src/ProofTools/DoubleCutDeletionTool.ts index 1e2ef4d6..bdff5ebc 100644 --- a/src/ProofTools/DoubleCutDeletionTool.ts +++ b/src/ProofTools/DoubleCutDeletionTool.ts @@ -28,7 +28,7 @@ let currentProofTree: AEGTree; */ export function doubleCutDeletionMouseDown(event: MouseEvent) { const currentPoint: Point = new Point(event.x - offset.x, event.y - offset.y); - currentProofTree = treeContext.proofHistory.getLastNode(treeContext.proofHistory.head).tree; + currentProofTree = treeContext.proofHistory[treeContext.proofHistory.length - 1].tree; currentNode = currentProofTree.getLowestNode(currentPoint); isLegal(); @@ -55,7 +55,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); + const nextProof = new ProofNode(currentProofTree, "Double Cut Deletion"); const currentPoint: Point = new Point(event.x - offset.x, event.y - offset.y); if (legalNode && currentNode instanceof CutNode) { @@ -68,7 +68,7 @@ export function doubleCutDeletionMouseUp(event: MouseEvent) { nextProof.tree.insert(lowerCut.children[i]); } } - treeContext.proofHistory.insertAtEnd(nextProof); + treeContext.proofHistory.push(nextProof); } redrawProof(); diff --git a/src/ProofTools/DoubleCutInsertionTool.ts b/src/ProofTools/DoubleCutInsertionTool.ts index bd6ec7ff..293b9edc 100644 --- a/src/ProofTools/DoubleCutInsertionTool.ts +++ b/src/ProofTools/DoubleCutInsertionTool.ts @@ -31,7 +31,7 @@ let currentProofTree: AEGTree; */ export function doubleCutInsertionMouseDown(event: MouseEvent) { startingPoint = new Point(event.clientX - offset.x, event.clientY - offset.y); - currentProofTree = treeContext.proofHistory.getLastNode(treeContext.proofHistory.head).tree; + currentProofTree = treeContext.proofHistory[treeContext.proofHistory.length - 1].tree; wasOut = false; } @@ -73,14 +73,14 @@ export function doubleCutInsertionMouseMove(event: MouseEvent) { */ export function doubleCutInsertionMouseUp(event: MouseEvent) { const currentPoint: Point = new Point(event.clientX - offset.x, event.clientY - offset.y); - currentProofTree = treeContext.proofHistory.getLastNode(treeContext.proofHistory.head).tree; + currentProofTree = treeContext.proofHistory[treeContext.proofHistory.length - 1].tree; const largeCut: CutNode = new CutNode(createEllipse(startingPoint, currentPoint)); const smallCut: CutNode = new CutNode(calcSmallEllipse(largeCut.ellipse)); //Stores the tree of the previous proof so that we can perform double cut actions without //altering that tree - const nextProof = new ProofNode(currentProofTree); + const nextProof = new ProofNode(currentProofTree, "Double Cut Insertion"); 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 +93,7 @@ export function doubleCutInsertionMouseUp(event: MouseEvent) { if (legal) { nextProof.tree.insert(largeCut); nextProof.tree.insert(smallCut); - treeContext.proofHistory.insertAtEnd(nextProof); + treeContext.proofHistory.push(nextProof); } } redrawProof(); diff --git a/src/ProofTools/ErasureTool.ts b/src/ProofTools/ErasureTool.ts index 82dfb0d3..4a1e4fe4 100644 --- a/src/ProofTools/ErasureTool.ts +++ b/src/ProofTools/ErasureTool.ts @@ -29,7 +29,7 @@ let currentProofTree: AEGTree; */ export function erasureMouseDown(event: MouseEvent) { const currentPoint: Point = new Point(event.x - offset.x, event.y - offset.y); - currentProofTree = treeContext.proofHistory.getLastNode(treeContext.proofHistory.head).tree; + currentProofTree = treeContext.proofHistory[treeContext.proofHistory.length - 1].tree; currentNode = currentProofTree.getLowestNode(currentPoint); isLegal(); @@ -57,7 +57,7 @@ export function erasureMouseUp(event: MouseEvent) { if (legalNode) { //Stores the tree of the previous proof so that we can perform double cut actions without //altering that tree - const nextProof = new ProofNode(currentProofTree); + const nextProof = new ProofNode(currentProofTree, "Erasure"); const currentPoint: Point = new Point(event.x - offset.x, event.y - offset.y); const currentParent = nextProof.tree.getLowestParent(currentPoint); @@ -65,7 +65,7 @@ export function erasureMouseUp(event: MouseEvent) { currentParent.remove(currentPoint); } - treeContext.proofHistory.insertAtEnd(nextProof); + treeContext.proofHistory.push(nextProof); redrawProof(); } diff --git a/src/ToggleModes.ts b/src/ToggleModes.ts index e81bf63f..ac949345 100644 --- a/src/ToggleModes.ts +++ b/src/ToggleModes.ts @@ -37,7 +37,7 @@ export function toggleHandler(): void { treeContext.modeState = "Draw"; //cache the proof tree and tool state so that we can load it back in when we toggle again - proofCachedAEG = JSON.stringify(treeContext.proofHistory.toArray()); + proofCachedAEG = JSON.stringify(treeContext.proofHistory); proofCachedTool = treeContext.toolState; //Load in our saved draw tree and tool state @@ -60,12 +60,12 @@ export function toggleHandler(): void { drawCachedTool = treeContext.toolState; //Load in our saved proof structure and tool state - const loadedProof = loadFile(treeContext.modeState, proofCachedAEG) as AEGTree[] | null; + const loadedProof = loadFile(treeContext.modeState, proofCachedAEG) as ProofNode[] | null; if (loadedProof !== null) { - treeContext.proofHistory.rebuildFromArray(loadedProof); + treeContext.proofHistory = loadedProof; //Construct the next tree from the last tree in the proof const nextTree = new AEGTree( - treeContext.proofHistory.getLastNode(treeContext.proofHistory.head).tree.sheet + treeContext.proofHistory[treeContext.proofHistory.length - 1].tree.sheet ); //If the user selected something to be copied over from draw mode, @@ -80,13 +80,13 @@ export function toggleHandler(): void { } } - treeContext.proofHistory.insertAtEnd(new ProofNode(nextTree)); + treeContext.proofHistory.push(new ProofNode(nextTree)); } } else { //If there is no saved proof and the user selected something to be copied over from //draw mode, make that our proof structure const proofTree = new AEGTree(treeContext.selectForProof.sheet); - treeContext.proofHistory.insertAtEnd(new ProofNode(proofTree)); + treeContext.proofHistory.push(new ProofNode(proofTree)); } //Reset the state of our tools diff --git a/src/index.ts b/src/index.ts index 14d86e62..f7573c4f 100644 --- a/src/index.ts +++ b/src/index.ts @@ -60,7 +60,7 @@ import { toProofMouseMove, toProofMouseUp, toProofMouseOut, -} from "./DrawModes/ToProofMode"; +} from "./DrawModes/copyFromDraw"; import { doubleCutInsertionMouseDown, doubleCutInsertionMouseMove, @@ -87,6 +87,7 @@ import { resizeMouseUp, resizeMouseOut, } from "./DrawModes/ResizeTool"; +import {ProofNode} from "./AEG/ProofNode"; //Setting up Canvas const canvas: HTMLCanvasElement = document.getElementById("canvas"); @@ -216,14 +217,14 @@ export function setTool(state: Tool) { */ async function saveMode() { let name: string; - let data: AEGTree | AEGTree[]; + let data: AEGTree | ProofNode[]; if (treeContext.modeState === "Draw") { name = "AEG Tree"; data = treeContext.tree; } else { name = "Proof History"; - data = treeContext.proofHistory.toArray(); + data = treeContext.proofHistory; } //Slow Download @@ -274,11 +275,11 @@ async function loadMode() { reader.addEventListener("load", () => { const aegData = reader.result; const loadData = loadFile(treeContext.modeState, aegData); - if (treeContext.modeState === "Draw") { + if (loadData !== null && treeContext.modeState === "Draw") { treeContext.tree = loadData as AEGTree; redrawTree(treeContext.tree); - } else if (treeContext.modeState === "Proof") { - treeContext.proofHistory.rebuildFromArray(loadData as AEGTree[]); + } else if (loadData !== null && treeContext.modeState === "Proof") { + treeContext.proofHistory = loadData as ProofNode[]; redrawProof(); } //TODO: else popup error @@ -395,7 +396,7 @@ function mouseMoveHandler(event: MouseEvent) { resizeMouseMove(event); break; case Tool.toProofMode: - toProofMouseMove(); + toProofMouseMove(event); break; case Tool.doubleCutInsertionTool: doubleCutInsertionMouseMove(event); diff --git a/src/treeContext.ts b/src/treeContext.ts index c0052a65..c3b943b3 100644 --- a/src/treeContext.ts +++ b/src/treeContext.ts @@ -1,5 +1,5 @@ import {AEGTree} from "./AEG/AEGTree"; -import {ProofList} from "./AEG/ProofList"; +import {ProofNode} from "./AEG/ProofNode"; // import {Tool} from "./index"; /** @@ -32,8 +32,8 @@ export class treeContext { //The current tree on the the canvas, needs to be redrawn upon any updates. public static tree: AEGTree = new AEGTree(); - //A history of the proof constructed - public static proofHistory: ProofList = new ProofList(); + //The proof being constructed + public static proofHistory: ProofNode[] = []; //The node selected on draw mode which will copy over when we toggle to proof mode. public static selectForProof: AEGTree = new AEGTree(); From 4478a8ec24410ba4b9b69ecd259dfeddd770c3fb Mon Sep 17 00:00:00 2001 From: AnushaTiwari5 Date: Thu, 16 Nov 2023 19:53:23 -0500 Subject: [PATCH 06/17] mouse move selection, displays selected graph --- src/AEG/CutNode.ts | 2 +- src/DrawModes/DrawUtils.ts | 5 +++- src/DrawModes/copyFromDraw.ts | 53 ++++++++++++++++++++++++----------- src/ToggleModes.ts | 5 ++++ src/index.html | 8 +++++- src/index.ts | 42 +++++++++++++++++---------- src/treeContext.ts | 2 +- 7 files changed, 82 insertions(+), 35 deletions(-) diff --git a/src/AEG/CutNode.ts b/src/AEG/CutNode.ts index 27d4c5d4..18e79492 100644 --- a/src/AEG/CutNode.ts +++ b/src/AEG/CutNode.ts @@ -305,7 +305,7 @@ export class CutNode { if (this.internalEllipse === null) { str = "Sheet of Assertion of the AEG Tree"; } else { - str = "A cut node with boundary box of " + this.internalEllipse.toString(); + str = "A cut node with " + this.internalEllipse.toString(); } if (this.internalChildren.length > 0) { diff --git a/src/DrawModes/DrawUtils.ts b/src/DrawModes/DrawUtils.ts index 563bdf76..5140a798 100644 --- a/src/DrawModes/DrawUtils.ts +++ b/src/DrawModes/DrawUtils.ts @@ -23,6 +23,7 @@ ctx.font = "35pt arial"; //Tree string displayed on webpage const cutDisplay = document.getElementById("graphString"); +const proofString = document.getElementById("proofString"); //HTML bounding box check const atomCheckBox = document.getElementById("atomBox"); @@ -154,7 +155,9 @@ export function redrawProof() { tree = treeContext.proofHistory[treeContext.proofHistory.length - 1].tree; } - redrawTree(tree); + cleanCanvas(); + proofString.innerHTML = tree.toString(); + redrawCut(tree.sheet); } /** diff --git a/src/DrawModes/copyFromDraw.ts b/src/DrawModes/copyFromDraw.ts index 64d4ab5f..b7505266 100644 --- a/src/DrawModes/copyFromDraw.ts +++ b/src/DrawModes/copyFromDraw.ts @@ -8,12 +8,12 @@ import {AtomNode} from "../AEG/AtomNode"; import {CutNode} from "../AEG/CutNode"; import {treeContext} from "../treeContext"; import {offset} from "./DragTool"; -import {drawAtom, drawCut, cleanCanvas, redrawTree, highlightNode} from "./DrawUtils"; +import {drawAtom, cleanCanvas, redrawTree, highlightNode} from "./DrawUtils"; import {legalColor} from "../Themes"; import {AEGTree} from "../AEG/AEGTree"; //The initial point the user pressed down. -let startingPoint: Point; +let currentPoint: Point; //The current node and its children we will be moving. let selectedNode: CutNode | AtomNode | null = null; @@ -22,20 +22,22 @@ let selectedNode: CutNode | AtomNode | null = null; let legalNode: boolean; //A deep copy of the global tree -const tempTree = new AEGTree(treeContext.tree.sheet); +let tempTree: AEGTree; +const selectString = document.getElementById("selectionString"); /** * Handles the MouseDown event while in copy to proof mode. * Gets the lowest node on the tree at the point identified by the MouseDown event. * If it is a legal selection, highlights the node. * @param event The MouseDown event while in copy to proof mode */ -export function toProofMouseDown(event: MouseEvent) { +export function copyFromDrawMouseDown(event: MouseEvent) { + tempTree = new AEGTree(treeContext.tree.sheet); //Reset our selectForProof tree to a blank AEG so that a new graph can be selected - treeContext.selectForProof.sheet = new AEGTree().sheet; + treeContext.selectForProof = new AEGTree(); - startingPoint = new Point(event.x - offset.x, event.y - offset.y); - selectedNode = treeContext.tree.getLowestNode(startingPoint); + currentPoint = new Point(event.x - offset.x, event.y - offset.y); + selectedNode = treeContext.tree.getLowestNode(currentPoint); isLegal(); } @@ -44,11 +46,11 @@ export function toProofMouseDown(event: MouseEvent) { * Handles the MouseMove event while in copy to proof mode. * Currently MouseMove does not allow for node selection. (Can be changed as per team review) */ -export function toProofMouseMove(event: MouseEvent) { +export function copyFromDrawMouseMove(event: MouseEvent) { redrawTree(treeContext.tree); - const movePoint: Point = new Point(event.x - offset.x, event.y - offset.y); - selectedNode = treeContext.tree.getLowestNode(movePoint); + currentPoint = new Point(event.x - offset.x, event.y - offset.y); + selectedNode = treeContext.tree.getLowestNode(currentPoint); isLegal(); } @@ -57,7 +59,7 @@ export function toProofMouseMove(event: MouseEvent) { * Handles the MouseUp event while in copy to proof mode. * MouseUp displays an alert stating that a legal node has been selected */ -export function toProofMouseUp() { +export function copyFromDrawMouseUp() { if (legalNode) { //If the selected node is the tree, insert its children so we do not insert another tree. if (selectedNode instanceof CutNode && selectedNode.ellipse === null) { @@ -67,6 +69,9 @@ export function toProofMouseUp() { } else { treeContext.selectForProof.insert(selectedNode!); } + /* if (selectedNode !== null) { + treeContext.selectForProof.insert(selectedNode); + } */ redrawTree(treeContext.tree); alert("Graph selected, you may now toggle to proof mode"); } @@ -76,26 +81,35 @@ export function toProofMouseUp() { * Handles the MouseOut event of when the mouse moves outside the canvas while in copy to proof mode. * On MouseOut, the selection is cancelled. */ -export function toProofMouseOut() { +export function copyFromDrawMouseOut() { selectedNode = null; legalNode = false; redrawTree(treeContext.tree); } function isLegal() { + const tree = new AEGTree(); + let removed = false; + if (selectedNode !== null) { + tree.insert(selectedNode); + legalNode = true; + const tempParent = tempTree.getLowestParent(currentPoint); //Temporarily remove the selected part of the tree and highlight selected part only //NEED TREE EQUALITY DONE TO COMPARE DEEP COPY - if (selectedNode !== tempTree.sheet) { - const tempParent = tempTree.getLowestParent(startingPoint); + if ( + selectedNode instanceof AtomNode || + (selectedNode instanceof CutNode && selectedNode.ellipse !== null) + ) { if (tempParent !== null) { - tempParent.remove(startingPoint); + tempParent.remove(currentPoint); + removed = true; } redrawTree(tempTree); } else { - //If the entire tree is selected, clear the canvas and redraw entire tree in legalColor. + //If the sheet is selected, clear the canvas so that entire tree is highlighted cleanly cleanCanvas(); } @@ -105,5 +119,12 @@ function isLegal() { } else { highlightNode(selectedNode, legalColor()); } + + if (removed) { + tempTree.insert(selectedNode); + } + } else { + legalNode = false; } + selectString.innerHTML = tree.toString(); } diff --git a/src/ToggleModes.ts b/src/ToggleModes.ts index ac949345..21917060 100644 --- a/src/ToggleModes.ts +++ b/src/ToggleModes.ts @@ -7,6 +7,7 @@ import {loadFile} from "./AEG-IO"; import {AEGTree} from "./AEG/AEGTree"; import {ProofNode} from "./AEG/ProofNode"; import {redrawProof, redrawTree} from "./DrawModes/DrawUtils"; +import {treeString, proofString} from "."; // import {setMode} from "./index"; // import {selectedNode} from "./DrawModes/ToProofMode"; import {Tool, treeContext} from "./treeContext"; @@ -33,7 +34,9 @@ export function toggleHandler(): void { if (drawMode) { //Display the buttons for Draw Mode drawButtons.style.display = "block"; + treeString.style.display = "block"; proofButtons.style.display = "none"; + proofString.style.display = "none"; treeContext.modeState = "Draw"; //cache the proof tree and tool state so that we can load it back in when we toggle again @@ -52,7 +55,9 @@ export function toggleHandler(): void { } else { //Display the buttons for Proof Mode drawButtons.style.display = "none"; + treeString.style.display = "none"; proofButtons.style.display = "block"; + proofString.style.display = "block"; treeContext.modeState = "Proof"; //cache the draw tree and tool state so that we can load it back in when we toggle again diff --git a/src/index.html b/src/index.html index 84fe6f88..6426e1b5 100644 --- a/src/index.html +++ b/src/index.html @@ -76,7 +76,7 @@ - @@ -129,6 +129,7 @@

+

@@ -178,6 +179,11 @@
+
+

Selected subgraph:

+

+
+
diff --git a/src/index.ts b/src/index.ts index f7573c4f..5fa98bea 100644 --- a/src/index.ts +++ b/src/index.ts @@ -56,10 +56,10 @@ import { deleteMultiMouseUp, } from "./DrawModes/DeleteMultiTool"; import { - toProofMouseDown, - toProofMouseMove, - toProofMouseUp, - toProofMouseOut, + copyFromDrawMouseDown, + copyFromDrawMouseMove, + copyFromDrawMouseUp, + copyFromDrawMouseOut, } from "./DrawModes/copyFromDraw"; import { doubleCutInsertionMouseDown, @@ -103,6 +103,10 @@ ctx.font = "35pt arial"; //Global State const cutTools = document.getElementById("cutTools"); const atomTools = document.getElementById("atomTools"); +export const treeString = document.getElementById("graphString"); +export const proofString = document.getElementById("proofString"); +const selectionDisplay = document.getElementById("toProofTools"); + window.addEventListener("keydown", keyDownHandler); canvas.addEventListener("mousedown", mouseDownHandler); canvas.addEventListener("mousemove", mouseMoveHandler); @@ -128,7 +132,7 @@ window.copySingleTool = Tool.copySingleTool; window.copyMultiTool = Tool.copyMultiTool; window.deleteSingleTool = Tool.deleteSingleTool; window.deleteMultiTool = Tool.deleteMultiTool; -window.toProofMode = Tool.toProofMode; +window.copyFromDrawTool = Tool.copyFromDrawTool; window.doubleCutInsertionTool = Tool.doubleCutInsertionTool; window.resizeTool = Tool.resizeTool; window.doubleCutDeletionTool = Tool.doubleCutDeletionTool; @@ -150,7 +154,7 @@ declare global { copyMultiTool: Tool; deleteSingleTool: Tool; deleteMultiTool: Tool; - toProofMode: Tool; + copyFromDrawTool: Tool; resizeTool: Tool; doubleCutInsertionTool: Tool; doubleCutDeletionTool: Tool; @@ -192,11 +196,16 @@ export function setTool(state: Tool) { treeContext.toolState = state; cutTools.style.display = "none"; atomTools.style.display = "none"; + treeString.style.display = "none"; + proofString.style.display = "none"; + selectionDisplay.style.display = "none"; - if (state <= 10) { + if (state <= 11) { treeContext.modeState = "Draw"; + treeString.style.display = "block"; } else { treeContext.modeState = "Proof"; + proofString.style.display = "block"; } switch (treeContext.toolState) { @@ -206,6 +215,9 @@ export function setTool(state: Tool) { case Tool.cutTool: cutTools.style.display = "block"; break; + case Tool.copyFromDrawTool: + selectionDisplay.style.display = "block"; + break; case Tool.doubleCutInsertionTool: cutTools.style.display = "block"; break; @@ -340,8 +352,8 @@ function mouseDownHandler(event: MouseEvent) { case Tool.resizeTool: resizeMouseDown(event); break; - case Tool.toProofMode: - toProofMouseDown(event); + case Tool.copyFromDrawTool: + copyFromDrawMouseDown(event); break; case Tool.doubleCutInsertionTool: doubleCutInsertionMouseDown(event); @@ -395,8 +407,8 @@ function mouseMoveHandler(event: MouseEvent) { case Tool.resizeTool: resizeMouseMove(event); break; - case Tool.toProofMode: - toProofMouseMove(event); + case Tool.copyFromDrawTool: + copyFromDrawMouseMove(event); break; case Tool.doubleCutInsertionTool: doubleCutInsertionMouseMove(event); @@ -447,8 +459,8 @@ function mouseUpHandler(event: MouseEvent) { case Tool.resizeTool: resizeMouseUp(event); break; - case Tool.toProofMode: - toProofMouseUp(); + case Tool.copyFromDrawTool: + copyFromDrawMouseUp(); break; case Tool.doubleCutInsertionTool: doubleCutInsertionMouseUp(event); @@ -501,8 +513,8 @@ function mouseOutHandler() { case Tool.resizeTool: resizeMouseOut(); break; - case Tool.toProofMode: - toProofMouseOut(); + case Tool.copyFromDrawTool: + copyFromDrawMouseOut(); break; case Tool.doubleCutInsertionTool: doubleCutInsertionMouseOut(); diff --git a/src/treeContext.ts b/src/treeContext.ts index c3b943b3..c77b192b 100644 --- a/src/treeContext.ts +++ b/src/treeContext.ts @@ -22,7 +22,7 @@ export enum Tool { deleteSingleTool, deleteMultiTool, resizeTool, - toProofMode, + copyFromDrawTool, doubleCutInsertionTool, doubleCutDeletionTool, erasureTool, From ff76ee0ffe4445616cf8c470870dc415d62cfa8c Mon Sep 17 00:00:00 2001 From: AnushaTiwari5 Date: Fri, 17 Nov 2023 12:49:25 -0500 Subject: [PATCH 07/17] equality works --- src/AEG/AEGTree.ts | 12 +++ src/AEG/AtomNode.ts | 10 ++ src/AEG/CutNode.ts | 53 +++++++++++ src/DrawModes/CopyMultiTool.ts | 4 +- src/DrawModes/EditModeUtils.ts | 9 +- src/DrawModes/MoveMultiTool.ts | 4 +- src/DrawModes/copyFromDraw.ts | 1 + src/ProofTools/ErasureTool.ts | 2 +- src/ProofTools/InsertionTools.ts | 156 +++++++++++++++++++++++++++++++ src/ToggleModes.ts | 8 +- src/index.html | 8 +- src/index.ts | 20 ++++ src/treeContext.ts | 9 ++ 13 files changed, 279 insertions(+), 17 deletions(-) create mode 100644 src/ProofTools/InsertionTools.ts diff --git a/src/AEG/AEGTree.ts b/src/AEG/AEGTree.ts index 16d70f14..3aa544b2 100644 --- a/src/AEG/AEGTree.ts +++ b/src/AEG/AEGTree.ts @@ -214,6 +214,18 @@ export class AEGTree { } } + public isEqualTo(otherTree: AEGTree): boolean { + //For 2 trees to be equal, they must have the same number of children + if (this.sheet.children.length === otherTree.sheet.children.length) { + if (this.sheet.children.length === 0) { + //Both trees are empty trees => they are equal + return true; + } + return this.sheet.isEqualTo(otherTree.sheet); + } + return false; + } + /** * Method that returns a string representation of the AEG Tree * @returns The structure formed by the cuts and atoms in this AEG Tree diff --git a/src/AEG/AtomNode.ts b/src/AEG/AtomNode.ts index 881092b4..8b8d3b47 100644 --- a/src/AEG/AtomNode.ts +++ b/src/AEG/AtomNode.ts @@ -163,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; + } } diff --git a/src/AEG/CutNode.ts b/src/AEG/CutNode.ts index 18e79492..0cac48ff 100644 --- a/src/AEG/CutNode.ts +++ b/src/AEG/CutNode.ts @@ -344,4 +344,57 @@ export class CutNode { } return formulaString; } + + /** + * Method that checks if a cut node is equal to another cut node + * The are equal if they represent the same graph + * @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; + } } diff --git a/src/DrawModes/CopyMultiTool.ts b/src/DrawModes/CopyMultiTool.ts index 5e5bbdf3..35d9437a 100644 --- a/src/DrawModes/CopyMultiTool.ts +++ b/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) { diff --git a/src/DrawModes/EditModeUtils.ts b/src/DrawModes/EditModeUtils.ts index 173a28b4..dfe5d4a2 100644 --- a/src/DrawModes/EditModeUtils.ts +++ b/src/DrawModes/EditModeUtils.ts @@ -10,6 +10,7 @@ import {treeContext} from "../treeContext"; import {offset} from "./DragTool"; import {Ellipse} from "../AEG/Ellipse"; import {drawCut, drawAtom} from "./DrawUtils"; +import {AEGTree} from "../AEG/AEGTree"; /** * Checks the validity of the incoming node and all of its children. If the child is a cut node uses @@ -19,10 +20,10 @@ import {drawCut, drawAtom} from "./DrawUtils"; * @param change The difference between the original position and the new position * @returns If all nodes are in a valid position returns true, if any node is not returns false */ -export function validateChildren(incomingNode: CutNode, change: Point): boolean { +export function validateChildren(tree: AEGTree, incomingNode: CutNode, change: Point): boolean { if (incomingNode.ellipse !== null) { const tempCut: CutNode = alterCut(incomingNode, change); - if (!treeContext.tree.canInsert(tempCut)) { + if (!tree.canInsert(tempCut)) { return false; } } @@ -31,7 +32,7 @@ export function validateChildren(incomingNode: CutNode, change: Point): boolean if ( incomingNode.children[i] instanceof CutNode && (incomingNode.children[i] as CutNode).ellipse !== null && - !validateChildren(incomingNode.children[i] as CutNode, change) + !validateChildren(tree, incomingNode.children[i] as CutNode, change) ) { //If any of this node's children are in an invalid location return false for all of them. return false; @@ -39,7 +40,7 @@ export function validateChildren(incomingNode: CutNode, change: Point): boolean let tempAtom = incomingNode.children[i] as AtomNode; tempAtom = alterAtom(tempAtom, change); - if (!treeContext.tree.canInsert(tempAtom)) { + if (!tree.canInsert(tempAtom)) { return false; } } diff --git a/src/DrawModes/MoveMultiTool.ts b/src/DrawModes/MoveMultiTool.ts index 3a78bd4e..0c95cbd0 100644 --- a/src/DrawModes/MoveMultiTool.ts +++ b/src/DrawModes/MoveMultiTool.ts @@ -55,7 +55,7 @@ export function moveMultiMouseMove(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); @@ -82,7 +82,7 @@ export function moveMultiMouseUp(event: MouseEvent) { ); if (currentNode instanceof CutNode) { - if (validateChildren(currentNode, moveDifference)) { + if (validateChildren(treeContext.tree, currentNode, moveDifference)) { insertChildren(currentNode, moveDifference); } else { treeContext.tree.insert(currentNode); diff --git a/src/DrawModes/copyFromDraw.ts b/src/DrawModes/copyFromDraw.ts index b7505266..00921179 100644 --- a/src/DrawModes/copyFromDraw.ts +++ b/src/DrawModes/copyFromDraw.ts @@ -33,6 +33,7 @@ const selectString = document.getElementById("selectionStr */ export function copyFromDrawMouseDown(event: MouseEvent) { tempTree = new AEGTree(treeContext.tree.sheet); + treeContext.tree.isEqualTo(tempTree); //Reset our selectForProof tree to a blank AEG so that a new graph can be selected treeContext.selectForProof = new AEGTree(); diff --git a/src/ProofTools/ErasureTool.ts b/src/ProofTools/ErasureTool.ts index 4a1e4fe4..3a405dc9 100644 --- a/src/ProofTools/ErasureTool.ts +++ b/src/ProofTools/ErasureTool.ts @@ -29,7 +29,7 @@ let currentProofTree: AEGTree; */ export function erasureMouseDown(event: MouseEvent) { const currentPoint: Point = new Point(event.x - offset.x, event.y - offset.y); - currentProofTree = treeContext.proofHistory[treeContext.proofHistory.length - 1].tree; + currentProofTree = treeContext.getLastProofStep().tree; currentNode = currentProofTree.getLowestNode(currentPoint); isLegal(); diff --git a/src/ProofTools/InsertionTools.ts b/src/ProofTools/InsertionTools.ts new file mode 100644 index 00000000..b75956ac --- /dev/null +++ b/src/ProofTools/InsertionTools.ts @@ -0,0 +1,156 @@ +/** + * File containing multi node movement event handlers. + * @author Dawn Moore + */ + +import {Point} from "../AEG/Point"; +import {AtomNode} from "../AEG/AtomNode"; +import {CutNode} from "../AEG/CutNode"; +import {treeContext} from "../treeContext"; +import {offset} from "../DrawModes/DragTool"; +import {drawAtom, redrawTree} from "../DrawModes/DrawUtils"; +import {legalColor, illegalColor} from "../Themes"; +import {validateChildren, drawAltered, insertChildren, alterAtom} from "../DrawModes/EditModeUtils"; +import {AEGTree} from "../AEG/AEGTree"; +import {ProofNode} from "../AEG/ProofNode"; + +//The initial point the user pressed down. +let startingPoint: Point; + +//The selected subgraph that we will be placing +let currentGraph: (CutNode | AtomNode)[] | null; + +//The parent identified the position where we are trying to insert the incoming node +let currentParent: CutNode | null; + +//The tree that we are trying to insert the graph into +let currentTree: AEGTree; + +//Whether or not the node is allowed to be inserted (not the sheet). +let legalNode: boolean; + +//Whether or not applying this rule will result in the creation of a new node for our proof +let newNode: 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); + currentGraph = treeContext.selectForProof.sheet.children; + startingPoint = new Point(event.x - offset.x, event.y - offset.y); + + if (currentGraph.length > 0) { + if (treeContext.proofHistory.length > 1) { + currentParent = currentTree.getLowestParent(startingPoint); + + //According to rule of insertion, we can only insert on odd levels -> check to + //ensure that the new point where we are pasting is on an odd level + if (currentParent !== null && currentTree.getLevel(currentParent) % 2 === 1) { + legalNode = true; + newNode = true; + + if (currentGraph instanceof CutNode) { + const color = validateChildren(currentTree, currentGraph, startingPoint) + ? legalColor() + : illegalColor(); + drawAltered(currentGraph, color, startingPoint); + } else if (currentGraph instanceof AtomNode) { + const tempAtom: AtomNode = alterAtom(currentGraph, startingPoint); + const color = treeContext.tree.canInsert(tempAtom) + ? legalColor() + : illegalColor(); + drawAtom(tempAtom, color, true); + } + } else { + //If not on odd level, it is an illegal insertion. Highlight as such to signify + if (currentGraph instanceof CutNode) { + drawAltered(currentGraph, illegalColor(), startingPoint); + } else if (currentGraph instanceof AtomNode) { + const tempAtom: AtomNode = alterAtom(currentGraph, startingPoint); + drawAtom(tempAtom, illegalColor(), true); + } + } + } else { + if (currentTree.sheet.isEmptySheet()) { + legalNode = true; + newNode = false; + } else { + legalNode = false; + } + } + } else { + legalNode = false; + } +} + +export function insertionMouseMove(event: MouseEvent) { + if (legalNode) { + const moveDifference: Point = new Point( + event.x - startingPoint.x, + event.y - startingPoint.y + ); + + redrawTree(currentTree); + currentParent = currentTree.getLowestParent(moveDifference); + + if (currentParent !== null && currentTree.getLevel(currentParent) % 2 === 1) { + if (currentGraph instanceof CutNode) { + const color = validateChildren(currentTree, currentGraph, startingPoint) + ? legalColor() + : illegalColor(); + drawAltered(currentGraph, color, startingPoint); + } else if (currentGraph instanceof AtomNode) { + const tempAtom: AtomNode = alterAtom(currentGraph, startingPoint); + const color = treeContext.tree.canInsert(tempAtom) ? legalColor() : illegalColor(); + drawAtom(tempAtom, color, true); + } + } else { + if (currentGraph instanceof CutNode) { + drawAltered(currentGraph, illegalColor(), startingPoint); + } else if (currentGraph instanceof AtomNode) { + const tempAtom: AtomNode = alterAtom(currentGraph, startingPoint); + drawAtom(tempAtom, illegalColor(), true); + } + } + } +} + +export function insertionMouseUp(event: MouseEvent) { + if (legalNode) { + const moveDifference: Point = new Point( + event.x - startingPoint.x, + event.y - startingPoint.y + ); + + currentParent = currentTree.getLowestParent(moveDifference); + + if (currentParent !== null && currentTree.getLevel(currentParent) % 2 === 1) { + if (currentGraph instanceof CutNode) { + if (validateChildren(currentTree, currentGraph, moveDifference)) { + insertChildren(currentGraph, moveDifference); + } + } else if (currentGraph instanceof AtomNode) { + const tempAtom: AtomNode = alterAtom(currentGraph, moveDifference); + + if (currentTree.canInsert(tempAtom)) { + currentTree.insert(tempAtom); + } + } + } + + if (newNode) { + treeContext.proofHistory.push(new ProofNode(currentTree, "Insertion")); + } else { + treeContext.getLastProofStep().tree = currentTree; + treeContext.getLastProofStep().appliedRule = "Insertion"; + } + } + redrawTree(currentTree); + legalNode = false; +} + +export function insertionMouseOut() { + legalNode = false; + newNode = false; + redrawTree(treeContext.getLastProofStep().tree); +} diff --git a/src/ToggleModes.ts b/src/ToggleModes.ts index 21917060..8dd65a38 100644 --- a/src/ToggleModes.ts +++ b/src/ToggleModes.ts @@ -68,7 +68,7 @@ export function toggleHandler(): void { const loadedProof = loadFile(treeContext.modeState, proofCachedAEG) as ProofNode[] | null; if (loadedProof !== null) { treeContext.proofHistory = loadedProof; - //Construct the next tree from the last tree in the proof + /* //Construct the next tree from the last tree in the proof const nextTree = new AEGTree( treeContext.proofHistory[treeContext.proofHistory.length - 1].tree.sheet ); @@ -86,12 +86,12 @@ export function toggleHandler(): void { } treeContext.proofHistory.push(new ProofNode(nextTree)); - } + } */ } else { - //If there is no saved proof and the user selected something to be copied over from + /* //If there is no saved proof and the user selected something to be copied over from //draw mode, make that our proof structure const proofTree = new AEGTree(treeContext.selectForProof.sheet); - treeContext.proofHistory.push(new ProofNode(proofTree)); + treeContext.proofHistory.push(new ProofNode(proofTree)); */ } //Reset the state of our tools diff --git a/src/index.html b/src/index.html index 6426e1b5..2e5b863f 100644 --- a/src/index.html +++ b/src/index.html @@ -76,7 +76,7 @@ - @@ -86,8 +86,8 @@ -
@@ -107,7 +107,7 @@
- -
diff --git a/src/index.ts b/src/index.ts index 07e9fc73..eca94075 100644 --- a/src/index.ts +++ b/src/index.ts @@ -94,6 +94,12 @@ import { resizeMouseOut, } from "./DrawModes/ResizeTool"; import {ProofNode} from "./AEG/ProofNode"; +import { + pasteInProofMouseDown, + pasteInProofMouseMove, + pasteInProofMouseOut, + pasteInProofMouseUp, +} from "./ProofTools/pasteInProof"; //Setting up Canvas const canvas: HTMLCanvasElement = document.getElementById("canvas"); @@ -139,6 +145,7 @@ window.copyMultiTool = Tool.copyMultiTool; window.deleteSingleTool = Tool.deleteSingleTool; window.deleteMultiTool = Tool.deleteMultiTool; window.copyFromDrawTool = Tool.copyFromDrawTool; +window.pasteInProofTool = Tool.pasteInProofTool; window.doubleCutInsertionTool = Tool.doubleCutInsertionTool; window.resizeTool = Tool.resizeTool; window.doubleCutDeletionTool = Tool.doubleCutDeletionTool; @@ -162,6 +169,7 @@ declare global { deleteSingleTool: Tool; deleteMultiTool: Tool; copyFromDrawTool: Tool; + pasteInProofTool: Tool; resizeTool: Tool; doubleCutInsertionTool: Tool; doubleCutDeletionTool: Tool; @@ -363,6 +371,9 @@ function mouseDownHandler(event: MouseEvent) { case Tool.copyFromDrawTool: copyFromDrawMouseDown(event); break; + case Tool.pasteInProofTool: + pasteInProofMouseDown(); + break; case Tool.doubleCutInsertionTool: doubleCutInsertionMouseDown(event); break; @@ -421,6 +432,9 @@ function mouseMoveHandler(event: MouseEvent) { case Tool.copyFromDrawTool: copyFromDrawMouseMove(event); break; + case Tool.pasteInProofTool: + pasteInProofMouseMove(); + break; case Tool.doubleCutInsertionTool: doubleCutInsertionMouseMove(event); break; @@ -476,6 +490,9 @@ function mouseUpHandler(event: MouseEvent) { case Tool.copyFromDrawTool: copyFromDrawMouseUp(); break; + case Tool.pasteInProofTool: + pasteInProofMouseUp(); + break; case Tool.doubleCutInsertionTool: doubleCutInsertionMouseUp(event); break; @@ -533,6 +550,9 @@ function mouseOutHandler() { case Tool.copyFromDrawTool: copyFromDrawMouseOut(); break; + case Tool.pasteInProofTool: + pasteInProofMouseOut(); + break; case Tool.doubleCutInsertionTool: doubleCutInsertionMouseOut(); break; diff --git a/src/treeContext.ts b/src/treeContext.ts index ccc37c98..1faee24b 100644 --- a/src/treeContext.ts +++ b/src/treeContext.ts @@ -23,6 +23,7 @@ export enum Tool { deleteMultiTool, resizeTool, copyFromDrawTool, + pasteInProofTool, doubleCutInsertionTool, doubleCutDeletionTool, insertionTool, @@ -47,7 +48,7 @@ export class treeContext { public static getLastProofStep(): ProofNode { if (treeContext.proofHistory.length === 0) { - treeContext.proofHistory.push(new ProofNode(new AEGTree())); + return new ProofNode(new AEGTree()); } return treeContext.proofHistory[treeContext.proofHistory.length - 1]; From a1013804b4c90e6efb14e97b5aabec3fc6ff834b Mon Sep 17 00:00:00 2001 From: AnushaTiwari5 Date: Wed, 22 Nov 2023 18:13:43 -0500 Subject: [PATCH 11/17] non movement based indicator fix --- src/index.ts | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/index.ts b/src/index.ts index eca94075..5794f6f7 100644 --- a/src/index.ts +++ b/src/index.ts @@ -196,11 +196,11 @@ function setHighlight(event: string, id: string) { } //Active mode button stays pressed down until another mode button is clicked -const modeButtons = document.querySelectorAll(".modeButton"); -modeButtons.forEach(button => { +const toolButtons = document.querySelectorAll(".toolButton"); +toolButtons.forEach(button => { button.addEventListener("click", () => { - button.classList.toggle("modeButtonPressed"); - modeButtons.forEach(otherButton => { + button.classList.add("modeButtonPressed"); + toolButtons.forEach(otherButton => { if (otherButton !== button) { otherButton.classList.remove("modeButtonPressed"); } From 4e4e77c92a781ba6c4ee68a4d53636f174152198 Mon Sep 17 00:00:00 2001 From: AnushaTiwari5 Date: Wed, 22 Nov 2023 18:21:36 -0500 Subject: [PATCH 12/17] non movement indicator fix --- src/index.ts | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/index.ts b/src/index.ts index 5794f6f7..cfec939c 100644 --- a/src/index.ts +++ b/src/index.ts @@ -199,10 +199,10 @@ function setHighlight(event: string, id: string) { const toolButtons = document.querySelectorAll(".toolButton"); toolButtons.forEach(button => { button.addEventListener("click", () => { - button.classList.add("modeButtonPressed"); + button.classList.add("toolButtonPressed"); toolButtons.forEach(otherButton => { if (otherButton !== button) { - otherButton.classList.remove("modeButtonPressed"); + otherButton.classList.remove("toolButtonPressed"); } }); }); From 51575bad924715c5050e1fb4cf9b1ab033013383 Mon Sep 17 00:00:00 2001 From: AnushaTiwari5 Date: Wed, 22 Nov 2023 18:58:27 -0500 Subject: [PATCH 13/17] insertion done --- src/AEG/AEGTree.ts | 18 +++ src/ProofTools/InsertionTools.ts | 247 ++++++++++++++++++------------- 2 files changed, 165 insertions(+), 100 deletions(-) diff --git a/src/AEG/AEGTree.ts b/src/AEG/AEGTree.ts index bd7386f3..03f0c81e 100644 --- a/src/AEG/AEGTree.ts +++ b/src/AEG/AEGTree.ts @@ -146,6 +146,24 @@ export class AEGTree { return this.internalSheet.getLowestParent(incomingPoint); } + public getParent(incomingNode: CutNode | AtomNode): CutNode | null { + if (!this.internalSheet.containsNode(incomingNode)) { + return null; + } + + let corner: Point | null = null; + if (incomingNode instanceof CutNode && incomingNode.ellipse !== null) { + corner = incomingNode.ellipse.boundingBox.startVertex; + } else if (incomingNode instanceof AtomNode) { + corner = incomingNode.calcRect().startVertex; + } + + if (corner !== null) { + return this.internalSheet.getLowestParent(corner); + } + return null; + } + /** * Finds the depth of the node within the tree. * @param incomingNode The node to be searched for diff --git a/src/ProofTools/InsertionTools.ts b/src/ProofTools/InsertionTools.ts index f26386d0..d5152da4 100644 --- a/src/ProofTools/InsertionTools.ts +++ b/src/ProofTools/InsertionTools.ts @@ -1,6 +1,6 @@ /** - * File containing multi node movement event handlers. - * @author Dawn Moore + * File containing insertion node movement event handlers. + * @author Anusha Tiwari */ import {Point} from "../AEG/Point"; @@ -8,150 +8,197 @@ import {AtomNode} from "../AEG/AtomNode"; import {CutNode} from "../AEG/CutNode"; import {treeContext} from "../treeContext"; import {offset} from "../DrawModes/DragTool"; -import {drawAtom, redrawTree} from "../DrawModes/DrawUtils"; +import {redrawProof} from "../DrawModes/DrawUtils"; import {legalColor, illegalColor} from "../Themes"; -import {validateChildren, drawAltered, insertChildren, alterAtom} from "../DrawModes/EditModeUtils"; +import { + validateChildren, + drawAltered, + insertChildren, + alterAtom, + alterCut, +} from "../DrawModes/EditModeUtils"; import {AEGTree} from "../AEG/AEGTree"; import {ProofNode} from "../AEG/ProofNode"; -//The initial point the user pressed down. -let startingPoint: Point; - //The selected subgraph that we will be placing -let currentGraph: (CutNode | AtomNode)[] | null; +let currentGraphs: (CutNode | AtomNode)[]; //The parent identified the position where we are trying to insert the incoming node -let currentParent: CutNode | null; +let currentParent: CutNode | AtomNode | null; //The tree that we are trying to insert the graph into let currentTree: AEGTree; -//Whether or not the node is allowed to be inserted (not the sheet). -let legalNode: boolean; +//Whether or not the node is allowed to be inserted in that place. +let legalPlace: boolean; -//Whether or not applying this rule will result in the creation of a new node for our proof -let newNode: boolean; +//Whether or not the node being placed is a legal node +let legalNode: boolean; export function insertionMouseDown(event: MouseEvent) { - console.log("selected: " + treeContext.selectForProof.toString()); //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); - currentGraph = treeContext.selectForProof.sheet.children; - startingPoint = new Point(event.x - offset.x, event.y - offset.y); - - if (currentGraph.length > 0) { - if (treeContext.proofHistory.length > 1) { - currentParent = currentTree.getLowestParent(startingPoint); - - //According to rule of insertion, we can only insert on odd levels -> check to - //ensure that the new point where we are pasting is on an odd level - if (currentParent !== null && currentTree.getLevel(currentParent) % 2 === 1) { - legalNode = true; - newNode = true; - - if (currentGraph instanceof CutNode) { - const color = validateChildren(currentTree, currentGraph, startingPoint) - ? legalColor() - : illegalColor(); - drawAltered(currentGraph, color, startingPoint); - } else if (currentGraph instanceof AtomNode) { - const tempAtom: AtomNode = alterAtom(currentGraph, startingPoint); - const color = treeContext.tree.canInsert(tempAtom) + currentGraphs = 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 && currentGraphs.length === 1) { + //As long as there are graphs to be placed, they are legal nodes + legalNode = true; + + //The change in the original position of the node vs the new position we are placing it on + const newPoint = calculatePoint(event, currentGraphs[0]); + + //Get node we have clicked to insert within. If the node is an atom node, get its parent cut + currentParent = + currentTree.getLowestNode(startingPoint) instanceof AtomNode + ? currentTree.getLowestParent(startingPoint) + : currentTree.getLowestNode(startingPoint); + + if (newPoint) { + //Create a temporary node with the altered values of the location we are placing it on + const newNode = + currentGraphs[0] instanceof AtomNode + ? alterAtom(currentGraphs[0], newPoint) + : alterCut(currentGraphs[0], newPoint); + + //If the node being placed is not contained within the parent node at the given position, + //get the parent of that node. Repeat this until we find the actual parent that contains + //the new node + while (currentParent !== null && !(currentParent as CutNode).containsNode(newNode)) { + currentParent = currentTree.getParent(currentParent); + } + //According to rule of insertion, we can insert 1 graph at a time only on odd levels -> + //check to ensure that the new point where we are pasting is on an odd level. + //For the placement to be an odd level, its parent must be on an even level + if ( + currentParent !== null && + currentParent instanceof CutNode && + currentParent.ellipse !== null && + currentTree.getLevel(currentParent) % 2 === 0 + ) { + //Check if the node can be placed at that position, and draw it accordingly + let color = ""; + if (currentGraphs[0] instanceof CutNode) { + color = validateChildren(currentTree, currentGraphs[0], newPoint) ? legalColor() : illegalColor(); - drawAtom(tempAtom, color, true); - } - } else { - //If not on odd level, it is an illegal insertion. Highlight as such to signify - if (currentGraph instanceof CutNode) { - drawAltered(currentGraph, illegalColor(), startingPoint); - } else if (currentGraph instanceof AtomNode) { - const tempAtom: AtomNode = alterAtom(currentGraph, startingPoint); - drawAtom(tempAtom, illegalColor(), true); + } else if (currentGraphs[0] instanceof AtomNode) { + const tempAtom: AtomNode = alterAtom(currentGraphs[0], newPoint); + color = currentTree.canInsert(tempAtom) ? legalColor() : illegalColor(); } - } - } else { - if (currentTree.sheet.isEmptySheet()) { - legalNode = true; - newNode = false; + legalPlace = color === legalColor() ? true : false; + drawAltered(currentGraphs[0], color, newPoint); } else { - legalNode = false; + legalPlace = false; + drawAltered(currentGraphs[0], illegalColor(), newPoint); } } } else { + legalPlace = false; legalNode = false; } } export function insertionMouseMove(event: MouseEvent) { if (legalNode) { - const moveDifference: Point = new Point( - event.x - startingPoint.x, - event.y - startingPoint.y - ); + const movePoint: Point = new Point(event.x - offset.x, event.y - offset.y); + + redrawProof(); + + if (treeContext.proofHistory.length > 0 && currentGraphs.length === 1) { + const newPoint = calculatePoint(event, currentGraphs[0]); + currentParent = + currentTree.getLowestNode(movePoint) instanceof AtomNode + ? currentTree.getLowestParent(movePoint) + : currentTree.getLowestNode(movePoint); + + if (newPoint) { + const newNode = + currentGraphs[0] instanceof AtomNode + ? alterAtom(currentGraphs[0], newPoint) + : alterCut(currentGraphs[0], newPoint); + + while ( + currentParent !== null && + !(currentParent as CutNode).containsNode(newNode) + ) { + currentParent = currentTree.getParent(currentParent); + } - redrawTree(currentTree); - currentParent = currentTree.getLowestParent(moveDifference); - - if (currentParent !== null && currentTree.getLevel(currentParent) % 2 === 1) { - if (currentGraph instanceof CutNode) { - const color = validateChildren(currentTree, currentGraph, startingPoint) - ? legalColor() - : illegalColor(); - drawAltered(currentGraph, color, startingPoint); - } else if (currentGraph instanceof AtomNode) { - const tempAtom: AtomNode = alterAtom(currentGraph, startingPoint); - const color = treeContext.tree.canInsert(tempAtom) ? legalColor() : illegalColor(); - drawAtom(tempAtom, color, true); + if ( + currentParent !== null && + currentParent instanceof CutNode && + currentParent.ellipse !== null && + currentTree.getLevel(currentParent) % 2 === 0 + ) { + let color = ""; + if (currentGraphs[0] instanceof CutNode) { + color = validateChildren(currentTree, currentGraphs[0], newPoint) + ? legalColor() + : illegalColor(); + } else if (currentGraphs[0] instanceof AtomNode) { + const tempAtom: AtomNode = alterAtom(currentGraphs[0], newPoint); + color = currentTree.canInsert(tempAtom) ? legalColor() : illegalColor(); + } + + legalPlace = color === legalColor() ? true : false; + drawAltered(currentGraphs[0], color, newPoint); + } else { + legalPlace = false; + drawAltered(currentGraphs[0], illegalColor(), newPoint); + } } } else { - if (currentGraph instanceof CutNode) { - drawAltered(currentGraph, illegalColor(), startingPoint); - } else if (currentGraph instanceof AtomNode) { - const tempAtom: AtomNode = alterAtom(currentGraph, startingPoint); - drawAtom(tempAtom, illegalColor(), true); - } + legalPlace = false; } } } export function insertionMouseUp(event: MouseEvent) { - if (legalNode) { - const moveDifference: Point = new Point( - event.x - startingPoint.x, - event.y - startingPoint.y - ); - - currentParent = currentTree.getLowestParent(moveDifference); - - if (currentParent !== null && currentTree.getLevel(currentParent) % 2 === 1) { - if (currentGraph instanceof CutNode) { - if (validateChildren(currentTree, currentGraph, moveDifference)) { - insertChildren(currentGraph, moveDifference); - } - } else if (currentGraph instanceof AtomNode) { - const tempAtom: AtomNode = alterAtom(currentGraph, moveDifference); - - if (currentTree.canInsert(tempAtom)) { + //If it is a legal node and is being placed at a legal position, insert it into the tree + if (legalNode && legalPlace) { + if (treeContext.proofHistory.length > 0 && currentGraphs.length === 1) { + //Calculate the point where the node has to be placed + const newPoint = calculatePoint(event, currentGraphs[0]); + + //Insert the node, and its children if it has any + if (newPoint) { + if (currentGraphs[0] instanceof CutNode) { + insertChildren(currentGraphs[0], newPoint, currentTree); + } else if (currentGraphs[0] instanceof AtomNode) { + const tempAtom: AtomNode = alterAtom(currentGraphs[0], newPoint); 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")); } } - - if (newNode) { - treeContext.proofHistory.push(new ProofNode(currentTree, "Insertion")); - } else { - treeContext.getLastProofStep().tree = currentTree; - treeContext.getLastProofStep().appliedRule = "Insertion"; - } } - redrawTree(currentTree); + redrawProof(); legalNode = false; } export function insertionMouseOut() { legalNode = false; - newNode = false; - redrawTree(treeContext.getLastProofStep().tree); + redrawProof(); +} + +/** + * Calculates the difference between the original position of the node in the draw canvas and the + * new position we are placing it on the proof canvas + * @param event The mouse event that identifies our new position + * @param graph The node we are trying to place + * @returns The difference between the original position and the new position + */ +function calculatePoint(event: MouseEvent, node: CutNode | AtomNode): Point | undefined { + if (node instanceof CutNode && node.ellipse !== null) { + return new Point( + event.x - node.ellipse.center.x - offset.x, + event.y - node.ellipse.center.y - offset.y + ); + } else if (node instanceof AtomNode) { + return new Point(event.x - node.origin.x - offset.x, event.y - node.origin.y - offset.y); + } } From 2b7aef993e0b16de2b63f617286a7be13eb13949 Mon Sep 17 00:00:00 2001 From: AnushaTiwari5 Date: Wed, 22 Nov 2023 19:00:39 -0500 Subject: [PATCH 14/17] insertion done? --- src/ProofTools/InsertionTools.ts | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/ProofTools/InsertionTools.ts b/src/ProofTools/InsertionTools.ts index d5152da4..a8d22f59 100644 --- a/src/ProofTools/InsertionTools.ts +++ b/src/ProofTools/InsertionTools.ts @@ -201,4 +201,6 @@ function calculatePoint(event: MouseEvent, node: CutNode | AtomNode): Point | un } else if (node instanceof AtomNode) { return new Point(event.x - node.origin.x - offset.x, event.y - node.origin.y - offset.y); } + + return undefined; } From a4f86f87f540442373530be98fc3a9c46de76f86 Mon Sep 17 00:00:00 2001 From: AnushaTiwari5 Date: Fri, 24 Nov 2023 11:47:13 -0500 Subject: [PATCH 15/17] modified proof tools to account for restructuring, insertion no longer adopts nodes, proof file name has -> --- src/ProofTools/DoubleCutDeletionTool.ts | 2 +- src/ProofTools/DoubleCutInsertionTool.ts | 4 +- src/ProofTools/ErasureTool.ts | 2 +- src/ProofTools/InsertionTools.ts | 178 ++++++++++++++++------- src/index.ts | 6 +- 5 files changed, 133 insertions(+), 59 deletions(-) diff --git a/src/ProofTools/DoubleCutDeletionTool.ts b/src/ProofTools/DoubleCutDeletionTool.ts index bdff5ebc..db32dffe 100644 --- a/src/ProofTools/DoubleCutDeletionTool.ts +++ b/src/ProofTools/DoubleCutDeletionTool.ts @@ -28,7 +28,7 @@ let currentProofTree: AEGTree; */ export function doubleCutDeletionMouseDown(event: MouseEvent) { const currentPoint: Point = new Point(event.x - offset.x, event.y - offset.y); - currentProofTree = treeContext.proofHistory[treeContext.proofHistory.length - 1].tree; + currentProofTree = new AEGTree(treeContext.getLastProofStep().tree.sheet); currentNode = currentProofTree.getLowestNode(currentPoint); isLegal(); diff --git a/src/ProofTools/DoubleCutInsertionTool.ts b/src/ProofTools/DoubleCutInsertionTool.ts index 293b9edc..04b4b25f 100644 --- a/src/ProofTools/DoubleCutInsertionTool.ts +++ b/src/ProofTools/DoubleCutInsertionTool.ts @@ -31,7 +31,7 @@ let currentProofTree: AEGTree; */ export function doubleCutInsertionMouseDown(event: MouseEvent) { startingPoint = new Point(event.clientX - offset.x, event.clientY - offset.y); - currentProofTree = treeContext.proofHistory[treeContext.proofHistory.length - 1].tree; + currentProofTree = new AEGTree(treeContext.getLastProofStep().tree.sheet); wasOut = false; } @@ -73,7 +73,7 @@ export function doubleCutInsertionMouseMove(event: MouseEvent) { */ export function doubleCutInsertionMouseUp(event: MouseEvent) { const currentPoint: Point = new Point(event.clientX - offset.x, event.clientY - offset.y); - currentProofTree = treeContext.proofHistory[treeContext.proofHistory.length - 1].tree; + currentProofTree = new AEGTree(treeContext.getLastProofStep().tree.sheet); const largeCut: CutNode = new CutNode(createEllipse(startingPoint, currentPoint)); const smallCut: CutNode = new CutNode(calcSmallEllipse(largeCut.ellipse)); diff --git a/src/ProofTools/ErasureTool.ts b/src/ProofTools/ErasureTool.ts index 3a405dc9..0c2390cf 100644 --- a/src/ProofTools/ErasureTool.ts +++ b/src/ProofTools/ErasureTool.ts @@ -29,7 +29,7 @@ let currentProofTree: AEGTree; */ export function erasureMouseDown(event: MouseEvent) { const currentPoint: Point = new Point(event.x - offset.x, event.y - offset.y); - currentProofTree = treeContext.getLastProofStep().tree; + currentProofTree = new AEGTree(treeContext.getLastProofStep().tree.sheet); currentNode = currentProofTree.getLowestNode(currentPoint); isLegal(); diff --git a/src/ProofTools/InsertionTools.ts b/src/ProofTools/InsertionTools.ts index a8d22f59..88d05a44 100644 --- a/src/ProofTools/InsertionTools.ts +++ b/src/ProofTools/InsertionTools.ts @@ -57,47 +57,78 @@ export function insertionMouseDown(event: MouseEvent) { : currentTree.getLowestNode(startingPoint); if (newPoint) { - //Create a temporary node with the altered values of the location we are placing it on + //Create a temporary node with the altered values of the new node at the location we + //are placing it on const newNode = currentGraphs[0] instanceof AtomNode ? alterAtom(currentGraphs[0], newPoint) : alterCut(currentGraphs[0], newPoint); //If the node being placed is not contained within the parent node at the given position, - //get the parent of that node. Repeat this until we find the actual parent that contains - //the new node - while (currentParent !== null && !(currentParent as CutNode).containsNode(newNode)) { - currentParent = currentTree.getParent(currentParent); - } - //According to rule of insertion, we can insert 1 graph at a time only on odd levels -> - //check to ensure that the new point where we are pasting is on an odd level. - //For the placement to be an odd level, its parent must be on an even level - if ( - currentParent !== null && - currentParent instanceof CutNode && - currentParent.ellipse !== null && - currentTree.getLevel(currentParent) % 2 === 0 - ) { - //Check if the node can be placed at that position, and draw it accordingly - let color = ""; - if (currentGraphs[0] instanceof CutNode) { - color = validateChildren(currentTree, currentGraphs[0], newPoint) - ? legalColor() - : illegalColor(); - } else if (currentGraphs[0] instanceof AtomNode) { - const tempAtom: AtomNode = alterAtom(currentGraphs[0], newPoint); - color = currentTree.canInsert(tempAtom) ? legalColor() : illegalColor(); - } - legalPlace = color === legalColor() ? true : false; - drawAltered(currentGraphs[0], color, newPoint); - } else { + //it is being placed in a position which will result in adoption of nodes. This is + //considered illegal -> mark it as such + if (currentParent !== null && !(currentParent as CutNode).containsNode(newNode)) { legalPlace = false; drawAltered(currentGraphs[0], illegalColor(), newPoint); + } else { + //According to rule of insertion, we can insert 1 graph at a time only on odd levels. + //Check to ensure that the new point where we are pasting is on an odd level (for + //the placement to be an odd level, its parent must be on an even level). + if ( + currentParent !== null && + currentParent instanceof CutNode && + currentParent.ellipse !== null && + currentTree.getLevel(currentParent) % 2 === 0 + ) { + //Insertion also does not allow for adoption of nodes, so check to make sure we are + //not adopting any children of the node we are being placed in + if (newNode instanceof CutNode) { + for (let i = 0; i < currentParent.children.length; i++) { + if (newNode.containsNode(currentParent.children[i])) { + legalPlace = false; + break; + } + + //The new node does not contain any of the children of the node it is + //being placed in - this is a legal placement + if (i === currentParent.children.length - 1) { + legalPlace = true; + } + } + } else { + //An atom node cannot contain any other nodes. This node is being placed + //at the right level + legalPlace = true; + } + + if (legalPlace) { + //We have confirmed that the node can be placed at this level without + //adopting any existing nodes. However, we still need to check for any + //collisions within this level + let color = ""; + if (currentGraphs[0] instanceof CutNode) { + color = validateChildren(currentTree, currentGraphs[0], newPoint) + ? legalColor() + : illegalColor(); + } else if (currentGraphs[0] instanceof AtomNode) { + const tempAtom: AtomNode = alterAtom(currentGraphs[0], newPoint); + color = currentTree.canInsert(tempAtom) ? legalColor() : illegalColor(); + } + legalPlace = color === legalColor() ? true : false; + drawAltered(currentGraphs[0], color, newPoint); + } else { + drawAltered(currentGraphs[0], illegalColor(), newPoint); + } + } else { + legalPlace = false; + drawAltered(currentGraphs[0], illegalColor(), newPoint); + } } } } else { legalPlace = false; legalNode = false; + drawAltered(currentGraphs[0], illegalColor(), startingPoint); } } @@ -105,49 +136,88 @@ export function insertionMouseMove(event: MouseEvent) { if (legalNode) { const movePoint: Point = new Point(event.x - offset.x, event.y - offset.y); + //Reset the canvas by redrawing our current proof structure redrawProof(); if (treeContext.proofHistory.length > 0 && currentGraphs.length === 1) { const newPoint = calculatePoint(event, currentGraphs[0]); + + //Get node we have clicked to insert within. If the node is an atom node, get its parent currentParent = currentTree.getLowestNode(movePoint) instanceof AtomNode ? currentTree.getLowestParent(movePoint) : currentTree.getLowestNode(movePoint); + //Create a temporary node with the altered values of the new node at the location we + //are placing it on if (newPoint) { const newNode = currentGraphs[0] instanceof AtomNode ? alterAtom(currentGraphs[0], newPoint) : alterCut(currentGraphs[0], newPoint); - while ( - currentParent !== null && - !(currentParent as CutNode).containsNode(newNode) - ) { - currentParent = currentTree.getParent(currentParent); - } - - if ( - currentParent !== null && - currentParent instanceof CutNode && - currentParent.ellipse !== null && - currentTree.getLevel(currentParent) % 2 === 0 - ) { - let color = ""; - if (currentGraphs[0] instanceof CutNode) { - color = validateChildren(currentTree, currentGraphs[0], newPoint) - ? legalColor() - : illegalColor(); - } else if (currentGraphs[0] instanceof AtomNode) { - const tempAtom: AtomNode = alterAtom(currentGraphs[0], newPoint); - color = currentTree.canInsert(tempAtom) ? legalColor() : illegalColor(); - } - - legalPlace = color === legalColor() ? true : false; - drawAltered(currentGraphs[0], color, newPoint); - } else { + //If the node being placed is not contained within the parent node at the given + //position, it is being placed in a position which will result in adoption of nodes. + //This is considered illegal -> mark it as such + if (currentParent !== null && !(currentParent as CutNode).containsNode(newNode)) { legalPlace = false; drawAltered(currentGraphs[0], illegalColor(), newPoint); + } else { + //According to rule of insertion, we can insert 1 graph at a time only on odd + //levels. Check to ensure that the new point where we are pasting is on an odd + //level (for the placement to be an odd level, its parent must be on an even + //level). + if ( + currentParent !== null && + currentParent instanceof CutNode && + currentParent.ellipse !== null && + currentTree.getLevel(currentParent) % 2 === 0 + ) { + //Insertion also does not allow for adoption of nodes, so check to make + //sure we are not adopting any children of the node we are being placed in + if (newNode instanceof CutNode) { + for (let i = 0; i < currentParent.children.length; i++) { + if (newNode.containsNode(currentParent.children[i])) { + legalPlace = false; + break; + } + + //The new node does not contain any of the children of the node it is + //being placed in - this is a legal placement + if (i === currentParent.children.length - 1) { + legalPlace = true; + } + } + } else { + //An atom node cannot contain any other nodes. This node is being placed + //at the right level + legalPlace = true; + } + + if (legalPlace) { + //We have confirmed that the node can be placed at this level without + //adopting any existing nodes. However, we still need to check for any + //collisions within this level + let color = ""; + if (currentGraphs[0] instanceof CutNode) { + color = validateChildren(currentTree, currentGraphs[0], newPoint) + ? legalColor() + : illegalColor(); + } else if (currentGraphs[0] instanceof AtomNode) { + const tempAtom: AtomNode = alterAtom(currentGraphs[0], newPoint); + color = currentTree.canInsert(tempAtom) + ? legalColor() + : illegalColor(); + } + legalPlace = color === legalColor() ? true : false; + drawAltered(currentGraphs[0], color, newPoint); + } else { + drawAltered(currentGraphs[0], illegalColor(), newPoint); + } + } else { + legalPlace = false; + drawAltered(currentGraphs[0], illegalColor(), newPoint); + } } } } else { diff --git a/src/index.ts b/src/index.ts index cfec939c..697dd3b2 100644 --- a/src/index.ts +++ b/src/index.ts @@ -251,7 +251,11 @@ async function saveMode() { name = "AEG Tree"; data = treeContext.tree; } else { - name = "Proof History"; + name = + treeContext.proofHistory[0].tree.toString() + + // " - " + + "\u2192" + + treeContext.getLastProofStep().tree.toString(); data = treeContext.proofHistory; } From f9dab12d5e3a3ba8b56c9eb28f6b1d7f2b6cdeab Mon Sep 17 00:00:00 2001 From: AnushaTiwari5 Date: Fri, 24 Nov 2023 23:07:57 -0500 Subject: [PATCH 16/17] resolved changes as requested on code review --- src/AEG-IO.ts | 46 +++---- src/AEG/AEGTree.ts | 29 +--- src/DrawModes/EditModeUtils.ts | 18 ++- src/ProofTools/InsertionTools.ts | 224 ++++++++++++++----------------- src/ToggleModes.ts | 38 ++---- src/index.ts | 19 +-- 6 files changed, 161 insertions(+), 213 deletions(-) diff --git a/src/AEG-IO.ts b/src/AEG-IO.ts index 56733fdc..0f2b5715 100644 --- a/src/AEG-IO.ts +++ b/src/AEG-IO.ts @@ -61,30 +61,24 @@ export async function saveFile(handle: FileSystemFileHandle, saveData: AEGTree | * This can be used to build the proof list * Returns null if an error occurred */ -export function loadFile( - mode: "Draw" | "Proof", - fileData: string | ArrayBuffer | null -): AEGTree | ProofNode[] | null { - if (typeof fileData === "string") { - 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[] = []; - data.forEach((node: nodeObj) => { - const childData: (atomObj | cutObj)[] = node.tree.internalSheet.internalChildren; - arr.push(new ProofNode(toTree(childData), node.appliedRule)); - }); - - return arr; +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 null; + return arr; + } } /** @@ -96,7 +90,7 @@ function toTree(childData: (atomObj | cutObj)[]): AEGTree { const tree: AEGTree = new AEGTree(); const children: (AtomNode | CutNode)[] = []; - childData.forEach(child => { + for (const child of childData) { if (Object.prototype.hasOwnProperty.call(child, "internalEllipse")) { //make cut children.push(toCut(child as cutObj)); @@ -104,7 +98,7 @@ function toTree(childData: (atomObj | cutObj)[]): AEGTree { //Make atom children.push(toAtom(child as atomObj)); } - }); + } tree.sheet.children = children; return tree; @@ -124,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); } diff --git a/src/AEG/AEGTree.ts b/src/AEG/AEGTree.ts index 03f0c81e..7e3f95c7 100644 --- a/src/AEG/AEGTree.ts +++ b/src/AEG/AEGTree.ts @@ -146,24 +146,6 @@ export class AEGTree { return this.internalSheet.getLowestParent(incomingPoint); } - public getParent(incomingNode: CutNode | AtomNode): CutNode | null { - if (!this.internalSheet.containsNode(incomingNode)) { - return null; - } - - let corner: Point | null = null; - if (incomingNode instanceof CutNode && incomingNode.ellipse !== null) { - corner = incomingNode.ellipse.boundingBox.startVertex; - } else if (incomingNode instanceof AtomNode) { - corner = incomingNode.calcRect().startVertex; - } - - if (corner !== null) { - return this.internalSheet.getLowestParent(corner); - } - return null; - } - /** * Finds the depth of the node within the tree. * @param incomingNode The node to be searched for @@ -246,15 +228,8 @@ export class AEGTree { * @returns True, if the trees are equal. Else, false */ public isEqualTo(otherTree: AEGTree): boolean { - //For 2 trees to be equal, they must have the same number of children - if (this.sheet.children.length === otherTree.sheet.children.length) { - if (this.sheet.children.length === 0) { - //Both trees are empty trees => they are equal - return true; - } - return this.sheet.isEqualTo(otherTree.sheet); - } - return false; + //For 2 trees to be equal, their sheet of assertion must be equal + return this.sheet.isEqualTo(otherTree.sheet); } /** diff --git a/src/DrawModes/EditModeUtils.ts b/src/DrawModes/EditModeUtils.ts index 755470eb..d67c905b 100644 --- a/src/DrawModes/EditModeUtils.ts +++ b/src/DrawModes/EditModeUtils.ts @@ -98,6 +98,20 @@ export function insertChildren(incomingNode: CutNode | AtomNode, change: Point, } } +/** + * Takes a node object and alters it accordingly based on the type of node + * @param node The node to be altered + * @param difference The difference on how far the node should move + * @returns The new altered version of the node + */ +export function alterNode(node: AtomNode | CutNode, difference: Point) { + if (node instanceof AtomNode) { + return alterAtom(node, difference); + } + + return alterCut(node as CutNode, difference); +} + /** * Takes a cut object and changes the center point of the ellipse by the difference. * If the cut does not have an ellipse throws and error. @@ -125,8 +139,8 @@ export function alterCut(originalCut: CutNode, difference: Point): CutNode { /** * Takes an atom object and changes the origin point by the difference. * @param originalAtom The Atom to be altered - * @param difference The difference on how far the center should move - * @returns The new altered version of the cut + * @param difference The difference on how far the atom should move + * @returns The new altered version of the atom */ export function alterAtom(originalAtom: AtomNode, difference: Point) { return new AtomNode( diff --git a/src/ProofTools/InsertionTools.ts b/src/ProofTools/InsertionTools.ts index 88d05a44..e2f34aa1 100644 --- a/src/ProofTools/InsertionTools.ts +++ b/src/ProofTools/InsertionTools.ts @@ -10,18 +10,12 @@ import {treeContext} from "../treeContext"; import {offset} from "../DrawModes/DragTool"; import {redrawProof} from "../DrawModes/DrawUtils"; import {legalColor, illegalColor} from "../Themes"; -import { - validateChildren, - drawAltered, - insertChildren, - alterAtom, - alterCut, -} from "../DrawModes/EditModeUtils"; +import {validateChildren, drawAltered, insertChildren, alterNode} from "../DrawModes/EditModeUtils"; import {AEGTree} from "../AEG/AEGTree"; import {ProofNode} from "../AEG/ProofNode"; //The selected subgraph that we will be placing -let currentGraphs: (CutNode | AtomNode)[]; +let currentNode: CutNode | AtomNode; //The parent identified the position where we are trying to insert the incoming node let currentParent: CutNode | AtomNode | null; @@ -39,37 +33,34 @@ 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); - currentGraphs = treeContext.selectForProof.sheet.children; + 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 && currentGraphs.length === 1) { + if (treeContext.proofHistory.length > 0 && selectedNodes.length === 1) { //As long as there are graphs to be placed, they are legal nodes legalNode = true; + currentNode = selectedNodes[0]; //The change in the original position of the node vs the new position we are placing it on - const newPoint = calculatePoint(event, currentGraphs[0]); + const newPoint = calculatePoint(event, currentNode); //Get node we have clicked to insert within. If the node is an atom node, get its parent cut - currentParent = - currentTree.getLowestNode(startingPoint) instanceof AtomNode - ? currentTree.getLowestParent(startingPoint) - : currentTree.getLowestNode(startingPoint); + const tempNode = currentTree.getLowestNode(startingPoint); + const tempParent = currentTree.getLowestParent(startingPoint); + currentParent = tempNode instanceof AtomNode ? tempParent : tempNode; if (newPoint) { //Create a temporary node with the altered values of the new node at the location we //are placing it on - const newNode = - currentGraphs[0] instanceof AtomNode - ? alterAtom(currentGraphs[0], newPoint) - : alterCut(currentGraphs[0], newPoint); + const newNode = alterNode(currentNode, newPoint); //If the node being placed is not contained within the parent node at the given position, //it is being placed in a position which will result in adoption of nodes. This is //considered illegal -> mark it as such if (currentParent !== null && !(currentParent as CutNode).containsNode(newNode)) { legalPlace = false; - drawAltered(currentGraphs[0], illegalColor(), newPoint); + drawAltered(currentNode, illegalColor(), newPoint); } else { //According to rule of insertion, we can insert 1 graph at a time only on odd levels. //Check to ensure that the new point where we are pasting is on an odd level (for @@ -83,17 +74,14 @@ export function insertionMouseDown(event: MouseEvent) { //Insertion also does not allow for adoption of nodes, so check to make sure we are //not adopting any children of the node we are being placed in if (newNode instanceof CutNode) { + legalPlace = true; for (let i = 0; i < currentParent.children.length; i++) { + //The new node contains a child of the node it is being placed in - this + //is an illegal placement, as it would result in adoption if (newNode.containsNode(currentParent.children[i])) { legalPlace = false; break; } - - //The new node does not contain any of the children of the node it is - //being placed in - this is a legal placement - if (i === currentParent.children.length - 1) { - legalPlace = true; - } } } else { //An atom node cannot contain any other nodes. This node is being placed @@ -106,29 +94,33 @@ export function insertionMouseDown(event: MouseEvent) { //adopting any existing nodes. However, we still need to check for any //collisions within this level let color = ""; - if (currentGraphs[0] instanceof CutNode) { - color = validateChildren(currentTree, currentGraphs[0], newPoint) - ? legalColor() - : illegalColor(); - } else if (currentGraphs[0] instanceof AtomNode) { - const tempAtom: AtomNode = alterAtom(currentGraphs[0], newPoint); - color = currentTree.canInsert(tempAtom) ? legalColor() : illegalColor(); + if (currentNode instanceof CutNode) { + const legalChildren = validateChildren( + currentTree, + currentNode, + newPoint + ); + color = legalChildren ? legalColor() : illegalColor(); + } else if (currentNode instanceof AtomNode) { + const tempAtom: AtomNode = alterNode(currentNode, newPoint) as AtomNode; + const canInsert = currentTree.canInsert(tempAtom); + color = canInsert ? legalColor() : illegalColor(); } legalPlace = color === legalColor() ? true : false; - drawAltered(currentGraphs[0], color, newPoint); + drawAltered(currentNode, color, newPoint); } else { - drawAltered(currentGraphs[0], illegalColor(), newPoint); + drawAltered(currentNode, illegalColor(), newPoint); } } else { legalPlace = false; - drawAltered(currentGraphs[0], illegalColor(), newPoint); + drawAltered(currentNode, illegalColor(), newPoint); } } } } else { legalPlace = false; legalNode = false; - drawAltered(currentGraphs[0], illegalColor(), startingPoint); + drawAltered(currentNode, illegalColor(), startingPoint); } } @@ -138,112 +130,102 @@ export function insertionMouseMove(event: MouseEvent) { //Reset the canvas by redrawing our current proof structure redrawProof(); + const newPoint = calculatePoint(event, currentNode); - if (treeContext.proofHistory.length > 0 && currentGraphs.length === 1) { - const newPoint = calculatePoint(event, currentGraphs[0]); - - //Get node we have clicked to insert within. If the node is an atom node, get its parent - currentParent = - currentTree.getLowestNode(movePoint) instanceof AtomNode - ? currentTree.getLowestParent(movePoint) - : currentTree.getLowestNode(movePoint); + //Get node we have clicked to insert within. If the node is an atom node, get its parent + const tempNode = currentTree.getLowestNode(movePoint); + const tempParent = currentTree.getLowestParent(movePoint); + currentParent = tempNode instanceof AtomNode ? tempParent : tempNode; + if (newPoint) { //Create a temporary node with the altered values of the new node at the location we //are placing it on - if (newPoint) { - const newNode = - currentGraphs[0] instanceof AtomNode - ? alterAtom(currentGraphs[0], newPoint) - : alterCut(currentGraphs[0], newPoint); + const newNode = alterNode(currentNode, newPoint); - //If the node being placed is not contained within the parent node at the given - //position, it is being placed in a position which will result in adoption of nodes. - //This is considered illegal -> mark it as such - if (currentParent !== null && !(currentParent as CutNode).containsNode(newNode)) { - legalPlace = false; - drawAltered(currentGraphs[0], illegalColor(), newPoint); - } else { - //According to rule of insertion, we can insert 1 graph at a time only on odd - //levels. Check to ensure that the new point where we are pasting is on an odd - //level (for the placement to be an odd level, its parent must be on an even - //level). - if ( - currentParent !== null && - currentParent instanceof CutNode && - currentParent.ellipse !== null && - currentTree.getLevel(currentParent) % 2 === 0 - ) { - //Insertion also does not allow for adoption of nodes, so check to make - //sure we are not adopting any children of the node we are being placed in - if (newNode instanceof CutNode) { - for (let i = 0; i < currentParent.children.length; i++) { - if (newNode.containsNode(currentParent.children[i])) { - legalPlace = false; - break; - } - - //The new node does not contain any of the children of the node it is - //being placed in - this is a legal placement - if (i === currentParent.children.length - 1) { - legalPlace = true; - } + //If the node being placed is not contained within the parent node at the given + //position, it is being placed in a position which will result in adoption of nodes. + //This is considered illegal -> mark it as such + if (currentParent !== null && !(currentParent as CutNode).containsNode(newNode)) { + legalPlace = false; + drawAltered(currentNode, illegalColor(), newPoint); + } else { + //According to rule of insertion, we can insert 1 graph at a time only on odd + //levels. Check to ensure that the new point where we are pasting is on an odd + //level (for the placement to be an odd level, its parent must be on an even + //level). + if ( + currentParent !== null && + currentParent instanceof CutNode && + currentParent.ellipse !== null && + currentTree.getLevel(currentParent) % 2 === 0 + ) { + //Insertion also does not allow for adoption of nodes, so check to make + //sure we are not adopting any children of the node we are being placed in + if (newNode instanceof CutNode) { + legalPlace = true; + for (let i = 0; i < currentParent.children.length; i++) { + //The new node contains a child of the node it is being placed in - this + //is an illegal placement, as it would result in adoption + if (newNode.containsNode(currentParent.children[i])) { + legalPlace = false; + break; } - } else { - //An atom node cannot contain any other nodes. This node is being placed - //at the right level - legalPlace = true; } + } else { + //An atom node cannot contain any other nodes. This node is being placed + //at the right level + legalPlace = true; + } - if (legalPlace) { - //We have confirmed that the node can be placed at this level without - //adopting any existing nodes. However, we still need to check for any - //collisions within this level - let color = ""; - if (currentGraphs[0] instanceof CutNode) { - color = validateChildren(currentTree, currentGraphs[0], newPoint) - ? legalColor() - : illegalColor(); - } else if (currentGraphs[0] instanceof AtomNode) { - const tempAtom: AtomNode = alterAtom(currentGraphs[0], newPoint); - color = currentTree.canInsert(tempAtom) - ? legalColor() - : illegalColor(); - } - legalPlace = color === legalColor() ? true : false; - drawAltered(currentGraphs[0], color, newPoint); - } else { - drawAltered(currentGraphs[0], illegalColor(), newPoint); + if (legalPlace) { + //We have confirmed that the node can be placed at this level without + //adopting any existing nodes. However, we still need to check for any + //collisions within this level + let color = ""; + if (currentNode instanceof CutNode) { + const legalChildren = validateChildren( + currentTree, + currentNode, + newPoint + ); + color = legalChildren ? legalColor() : illegalColor(); + } else if (currentNode instanceof AtomNode) { + const tempAtom: AtomNode = alterNode(currentNode, newPoint) as AtomNode; + const canInsert = currentTree.canInsert(tempAtom); + color = canInsert ? legalColor() : illegalColor(); } + legalPlace = color === legalColor() ? true : false; + drawAltered(currentNode, color, newPoint); } else { - legalPlace = false; - drawAltered(currentGraphs[0], illegalColor(), newPoint); + drawAltered(currentNode, illegalColor(), newPoint); } + } else { + legalPlace = false; + drawAltered(currentNode, illegalColor(), newPoint); } } - } else { - legalPlace = false; } + } else { + legalPlace = false; } } export function insertionMouseUp(event: MouseEvent) { //If it is a legal node and is being placed at a legal position, insert it into the tree if (legalNode && legalPlace) { - if (treeContext.proofHistory.length > 0 && currentGraphs.length === 1) { - //Calculate the point where the node has to be placed - const newPoint = calculatePoint(event, currentGraphs[0]); + //Calculate the point where the node has to be placed + const newPoint = calculatePoint(event, currentNode); - //Insert the node, and its children if it has any - if (newPoint) { - if (currentGraphs[0] instanceof CutNode) { - insertChildren(currentGraphs[0], newPoint, currentTree); - } else if (currentGraphs[0] instanceof AtomNode) { - const tempAtom: AtomNode = alterAtom(currentGraphs[0], newPoint); - 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")); + //Insert the node, and its children if it has any + if (newPoint) { + if (currentNode instanceof CutNode) { + insertChildren(currentNode, newPoint, currentTree); + } else if (currentNode instanceof AtomNode) { + const tempAtom: AtomNode = alterNode(currentNode, newPoint) as AtomNode; + 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")); } } redrawProof(); diff --git a/src/ToggleModes.ts b/src/ToggleModes.ts index b1b184c9..3e898263 100644 --- a/src/ToggleModes.ts +++ b/src/ToggleModes.ts @@ -42,7 +42,10 @@ export function toggleHandler(): void { proofCachedTool = treeContext.toolState; //Load in our saved draw tree and tool state - const loadedAEG = loadFile(treeContext.modeState, drawCachedAEG) as AEGTree | null; + let loadedAEG: AEGTree | null = null; + if (drawCachedAEG !== null) { + loadedAEG = loadFile(treeContext.modeState, drawCachedAEG) as AEGTree | null; + } if (loadedAEG !== null) { treeContext.tree.sheet = loadedAEG.sheet; } else { @@ -63,38 +66,15 @@ export function toggleHandler(): void { drawCachedTool = treeContext.toolState; //Load in our saved proof structure and tool state - const loadedProof = loadFile(treeContext.modeState, proofCachedAEG) as ProofNode[] | null; + let loadedProof: ProofNode[] | null = null; + if (proofCachedAEG !== null) { + loadedProof = loadFile(treeContext.modeState, proofCachedAEG) as ProofNode[] | null; + } if (loadedProof !== null) { treeContext.proofHistory = loadedProof; - /* //Construct the next tree from the last tree in the proof - const nextTree = new AEGTree( - treeContext.proofHistory[treeContext.proofHistory.length - 1].tree.sheet - ); - - //If the user selected something to be copied over from draw mode, - //insert it into the next tree - if (treeContext.selectForProof.sheet.children.length > 0) { - for (let i = 0; i < treeContext.selectForProof.sheet.children.length; i++) { - const child = treeContext.selectForProof.sheet.children[i]; - try { - nextTree.insert(child); - } catch (error) { - console.log("Could not insert " + child); - } - } - - treeContext.proofHistory.push(new ProofNode(nextTree)); - } */ - } /* else { - //If there is no saved proof and the user selected something to be copied over from - //draw mode, make that our proof structure - const proofTree = new AEGTree(treeContext.selectForProof.sheet); - treeContext.proofHistory.push(new ProofNode(proofTree)); - } */ - + } //Reset the state of our tools treeContext.toolState = proofCachedTool; - redrawProof(); } } diff --git a/src/index.ts b/src/index.ts index 697dd3b2..80f4bb1d 100644 --- a/src/index.ts +++ b/src/index.ts @@ -306,15 +306,18 @@ async function loadMode() { const reader = new FileReader(); reader.addEventListener("load", () => { const aegData = reader.result; - const loadData = loadFile(treeContext.modeState, aegData); - if (loadData !== null && treeContext.modeState === "Draw") { - treeContext.tree = loadData as AEGTree; - redrawTree(treeContext.tree); - } else if (loadData !== null && treeContext.modeState === "Proof") { - treeContext.proofHistory = loadData as ProofNode[]; - redrawProof(); + if (typeof aegData === "string") { + const loadData = loadFile(treeContext.modeState, aegData); + if (treeContext.modeState === "Draw") { + treeContext.tree = loadData as AEGTree; + redrawTree(treeContext.tree); + } else if (treeContext.modeState === "Proof") { + treeContext.proofHistory = loadData as ProofNode[]; + redrawProof(); + } + } else { + throw Error("Loading failed because reading the file was unsuccessful"); } - //TODO: else popup error }); reader.readAsText(file); } From 63a207b00686b68dc8ea5886fae3f47849d2913d Mon Sep 17 00:00:00 2001 From: AnushaTiwari5 Date: Fri, 24 Nov 2023 23:30:38 -0500 Subject: [PATCH 17/17] updated iteration to match proof structure --- src/ProofTools/IterationTool.ts | 35 ++++++++++++++++++++++----------- 1 file changed, 23 insertions(+), 12 deletions(-) diff --git a/src/ProofTools/IterationTool.ts b/src/ProofTools/IterationTool.ts index f5c7f06f..fc314a0b 100644 --- a/src/ProofTools/IterationTool.ts +++ b/src/ProofTools/IterationTool.ts @@ -9,7 +9,7 @@ import {AtomNode} from "../AEG/AtomNode"; import {CutNode} from "../AEG/CutNode"; import {treeContext} from "../treeContext"; import {offset} from "../DrawModes/DragTool"; -import {drawAtom, redrawTree} from "../DrawModes/DrawUtils"; +import {drawAtom, redrawProof} from "../DrawModes/DrawUtils"; import {legalColor, illegalColor} from "../Themes"; import { validateChildren, @@ -18,6 +18,8 @@ import { alterAtom, alterCut, } from "../DrawModes/EditModeUtils"; +import {AEGTree} from "../AEG/AEGTree"; +import {ProofNode} from "../AEG/ProofNode"; //The initial point the user pressed down. let startingPoint: Point; @@ -31,18 +33,25 @@ let currentParent: CutNode | null = null; //Whether or not the node is allowed to be moved (not the sheet). let legalNode: boolean; +//The tree of the current proof step +let currentProofTree: AEGTree; + /** * Sets the starting point for future use as well as obtaining the lowest node containing this point. * Also obtains the parent of this lowest point for future use as well. * @param event The mouse down event while using the iteration tool */ 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); startingPoint = new Point(event.x - offset.x, event.y - offset.y); - currentNode = treeContext.tree.getLowestNode(startingPoint); - currentParent = treeContext.tree.getLowestParent(startingPoint); + currentNode = currentProofTree.getLowestNode(startingPoint); + currentParent = currentProofTree.getLowestParent(startingPoint); //So long as we have obtained a node that isn't the sheet we are allowed to select this. - legalNode = currentNode !== treeContext.tree.sheet && currentNode !== null; + legalNode = currentNode !== currentProofTree.sheet && currentNode !== null; } /** @@ -58,7 +67,7 @@ export function iterationMouseMove(event: MouseEvent) { event.y - startingPoint.y ); - redrawTree(treeContext.tree); + redrawProof(); const currentPoint = new Point(event.x - offset.x, event.y - offset.y); const color = isLegal(moveDifference, currentPoint) ? legalColor() : illegalColor(); if (currentNode instanceof CutNode) { @@ -84,14 +93,16 @@ export function iterationMouseUp(event: MouseEvent) { if (isLegal(moveDifference, new Point(event.x - offset.x, event.y - offset.y))) { if (currentNode instanceof CutNode) { - insertChildren(currentNode, moveDifference); + insertChildren(currentNode, moveDifference, currentProofTree); } else if (currentNode instanceof AtomNode) { const tempAtom: AtomNode = alterAtom(currentNode, moveDifference); - treeContext.tree.insert(tempAtom); + 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")); } } - redrawTree(treeContext.tree); + redrawProof(); legalNode = false; } @@ -100,7 +111,7 @@ export function iterationMouseUp(event: MouseEvent) { */ export function iterationMouseOut() { legalNode = false; - redrawTree(treeContext.tree); + redrawProof(); } /** @@ -119,14 +130,14 @@ function isLegal(moveDifference: Point, currentPoint: Point): boolean { //If the currentNode is a cut, then it is legal if it and all if it's children can be placed //legally, and if the node we have selected can not be inserted over something else. ((currentNode instanceof CutNode && - validateChildren(currentNode, moveDifference) && + validateChildren(currentProofTree, currentNode, moveDifference) && insertChildless( - treeContext.tree.sheet, + currentProofTree.sheet, alterCut(currentNode, moveDifference).ellipse! )) || //AtomNodes are legal if they can be inserted in their current location. (currentNode instanceof AtomNode && - treeContext.tree.canInsert(alterAtom(currentNode, moveDifference)))) + currentProofTree.canInsert(alterAtom(currentNode, moveDifference)))) ); }