diff --git a/src/AEG-IO.ts b/src/AEG-IO.ts index 54a7e0c5..0f2b5715 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 {ProofNode} from "./AEG/ProofNode"; /** * Interface for an object describing Sheet of Assertion @@ -33,13 +34,18 @@ interface atomObj { internalOrigin: {x: number; y: number}; } +interface nodeObj { + tree: sheetObj; + appliedRule: string; +} + /** * Function that creates and saves a file containing the given AEG data * @param handle The handler for the save file picker * @param aegData Serialized JSON string containing the AEG data */ -export async function saveFile(handle: FileSystemFileHandle, aegData: AEGTree) { - const data = JSON.stringify(aegData, null, "\t"); +export async function saveFile(handle: FileSystemFileHandle, saveData: AEGTree | ProofNode[]) { + const data = JSON.stringify(saveData, null, "\t"); const writable = await handle.createWritable(); await writable.write(data); @@ -48,33 +54,54 @@ export async function saveFile(handle: FileSystemFileHandle, aegData: AEGTree) { /** * Function that takes in data read from a file and converts it into a valid AEG representation. + * @param mode The mode we are in (Draw mode or proof mode) * @param fileData The data read from a file. - * @returns An AEG representation of the data. + * @returns If in draw mode, returns an AEG representation of the data. + * If in proof mode, constructs an array of AEGs read from the file. + * This can be used to build the proof list * Returns null if an error occurred */ -export function loadFile(fileData: string | ArrayBuffer | null): AEGTree | null { - if (typeof fileData === "string") { - const data: sheetObj = JSON.parse(fileData); - const childData: (atomObj | cutObj)[] = data.internalSheet.internalChildren; - - const tree: AEGTree = new AEGTree(); - const children: (AtomNode | CutNode)[] = []; - - childData.forEach(child => { - if (Object.prototype.hasOwnProperty.call(child, "internalEllipse")) { - //make cut - children.push(toCut(child as cutObj)); - } else { - //Make atom - children.push(toAtom(child as atomObj)); - } - }); - - tree.sheet.children = children; - return tree; +export function loadFile(mode: "Draw" | "Proof", fileData: string): AEGTree | ProofNode[] { + const data = JSON.parse(fileData); + + if (mode === "Draw") { + const childData: (atomObj | cutObj)[] = (data as sheetObj).internalSheet.internalChildren; + return toTree(childData); + } else { + //Construct the tree at every step of the proof and store them in an array + const arr: ProofNode[] = []; + + let node: nodeObj; + for (node of data) { + const childData: (atomObj | cutObj)[] = node.tree.internalSheet.internalChildren; + arr.push(new ProofNode(toTree(childData), node.appliedRule)); + } + + return arr; + } +} + +/** + * Constructs an AEG from the array of JSON objects parsed from our file data. + * @param childData The array of objects which should be filled in as children of the tree. + * @returns An AEG Tree representation of our data. + */ +function toTree(childData: (atomObj | cutObj)[]): AEGTree { + const tree: AEGTree = new AEGTree(); + const children: (AtomNode | CutNode)[] = []; + + for (const child of childData) { + if (Object.prototype.hasOwnProperty.call(child, "internalEllipse")) { + //make cut + children.push(toCut(child as cutObj)); + } else { + //Make atom + children.push(toAtom(child as atomObj)); + } } - return null; + tree.sheet.children = children; + return tree; } /** @@ -91,13 +118,13 @@ function toCut(data: cutObj): CutNode { const children: (AtomNode | CutNode)[] = []; - data.internalChildren.forEach(child => { + for (const child of data.internalChildren) { if ("internalEllipse" in child) { children.push(toCut(child)); } else { children.push(toAtom(child)); } - }); + } return new CutNode(ellipse, children); } diff --git a/src/AEG/AEGTree.ts b/src/AEG/AEGTree.ts index 38405f0e..7e3f95c7 100644 --- a/src/AEG/AEGTree.ts +++ b/src/AEG/AEGTree.ts @@ -17,24 +17,21 @@ export class AEGTree { private internalSheet: CutNode; /** - * Method to construct a new AEG Tree. - * @param sheet If an existing sheet is passed, deep copy it to construct a new AEG Tree + * Constructs the sheet of assertion of the AEG tree + * @param sheet (OPTIONAL) An existing cut node which is to be used to construct the sheet of + * assertion of this AEG Tree. If given, creates a new tree with a deep copy of this node. */ public constructor(sheet?: CutNode) { - //If we are constructing a new tree from a given sheet, deep copy the sheet and its children - //to ensure an entirely new tree is constructed. - this.internalSheet = new CutNode(null); - if (sheet instanceof CutNode) { - // this.internalSheet = new CutNode(sheet.ellipse); - if (sheet.children.length > 0) { - this.internalSheet.children = [...sheet.children]; - } + if (sheet !== undefined) { + //If an existing cut node is passed, make a deep copy of it to copy over any children + this.internalSheet = sheet.copy(); + //Ellipse of the sheet of assertion should be null + this.internalSheet.ellipse = null; + } else { + this.internalSheet = new CutNode(null); } } - /** - * Accessor to get the sheet of the AEG Tree - */ public get sheet(): CutNode { return this.internalSheet; } @@ -224,6 +221,17 @@ export class AEGTree { } } + /** + * Method that checks if an AEG Tree is equal to another AEG Tree. Trees are equal if they have + * the same children, irrespective of the ordering of nodes within a level + * @param otherTree The tree we want to check for equality with + * @returns True, if the trees are equal. Else, false + */ + public isEqualTo(otherTree: AEGTree): boolean { + //For 2 trees to be equal, their sheet of assertion must be equal + return this.sheet.isEqualTo(otherTree.sheet); + } + /** * Method that returns a string representation of the AEG Tree * @returns The structure formed by the cuts and atoms in this AEG Tree diff --git a/src/AEG/AtomNode.ts b/src/AEG/AtomNode.ts index c3918d2a..0b5a3b85 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 @@ -150,4 +163,14 @@ export class AtomNode { this.internalHeight ); } + + /** + * Method that checks if an atom node is equal to another atom node. The are equal if they + * represent the same proposition. + * @param otherAtom The other atom node we are checking against for equality + * @returns True, if they are equal (the same). Else, false + */ + public isEqualTo(otherAtom: AtomNode): boolean { + return this.identifier === otherAtom.identifier; + } } diff --git a/src/AEG/CutNode.ts b/src/AEG/CutNode.ts index 6068152e..7bb334c4 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; } @@ -289,6 +321,10 @@ export class CutNode { return str; } + public isEmptySheet(): boolean { + return this.internalEllipse === null && this.internalChildren.length === 0; + } + /** * Constructs a string representation of an AEGTree or a subtree. * () - cut @@ -315,4 +351,57 @@ export class CutNode { } return formulaString; } + + /** + * Method that checks if a cut node is equal to another cut node. The are equal if they have + * the same children, irrespective of the ordering of nodes within a level + * @param otherCut The other cut node we are checking against for equality + * @returns True, if they are equal (the same). Else, false + */ + public isEqualTo(otherCut: CutNode): boolean { + //For 2 cuts to be equal, they must have the same number of children + if (this.children.length === otherCut.children.length) { + if (this.children.length === 0) { + //If they do not have children, they are empty cuts + //Empty cuts are always equal + return true; + } + //If they have the same number of children, they should be the same children + //Make a deep copy and get the list of children of each cut + const thisChildren = this.copy().children; + const otherChildren = otherCut.copy().children; + + //Iterate through the children of a cut and see if the other cut has the same child + //If they have the same child, remove it from the lists and continue + //If a child is not present in both, they are not equal + for (let i = 0; i < thisChildren.length; i++) { + for (let j = 0; j < otherChildren.length; j++) { + if ( + (thisChildren[i] instanceof AtomNode && + otherChildren[j] instanceof AtomNode && + (thisChildren[i] as AtomNode).isEqualTo( + otherChildren[j] as AtomNode + )) || + (thisChildren[i] instanceof CutNode && + otherChildren[j] instanceof CutNode && + (thisChildren[i] as CutNode).isEqualTo(otherChildren[j] as CutNode)) + ) { + thisChildren.splice(i, 1); + otherChildren.splice(j, 1); + i--; + break; + } + + if (j === otherChildren.length - 1) { + //Checked all children but a match was not found. The nodes are not equal + return false; + } + } + } + //Check if all the children have been matched and returned + return thisChildren.length === 0 && otherChildren.length === 0; + } + + return false; + } } diff --git a/src/AEG/ProofNode.ts b/src/AEG/ProofNode.ts new file mode 100644 index 00000000..cf235f63 --- /dev/null +++ b/src/AEG/ProofNode.ts @@ -0,0 +1,25 @@ +import {AEGTree} from "./AEGTree"; + +/** + * The structure representing a single node of the proof + * @author Anusha Tiwari + */ +export class ProofNode { + /** + * The AEG Tree representing the current state of the proof + */ + public tree: AEGTree; + + public appliedRule: string; + + /** + * Construct a proof node by providing the AEG Tree at the current state of the proof + * @param tree The AEG at the current state of the proof. + * If not defined, an empty AEG tree will be set constructed. + * @param rule The inference rule applied to get to this stage of the proof. + */ + public constructor(tree?: AEGTree, rule?: string) { + this.appliedRule = rule ?? ""; + this.tree = new AEGTree(tree?.sheet); + } +} 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/DrawUtils.ts b/src/DrawModes/DrawUtils.ts index 90bcea50..9c0e7a38 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"); @@ -99,10 +100,10 @@ export function cleanCanvas() { /** * Resets the canvas and begins the recursive method of drawing the current tree. */ -export function redrawTree(tree: AEGTree) { +export function redrawTree(tree: AEGTree, color?: string) { cutDisplay.innerHTML = tree.toString(); cleanCanvas(); - redrawCut(tree.sheet); + redrawCut(tree.sheet, color); } /** @@ -111,7 +112,7 @@ export function redrawTree(tree: AEGTree) { * @param incomingNode The CutNode to be iterated through * @param offset The difference between the actual graph and the current canvas */ -function redrawCut(incomingNode: CutNode) { +function redrawCut(incomingNode: CutNode, color?: string) { for (let i = 0; incomingNode.children.length > i; i++) { if (incomingNode.children[i] instanceof AtomNode) { redrawAtom(incomingNode.children[i]); @@ -120,7 +121,7 @@ function redrawCut(incomingNode: CutNode) { } } if (incomingNode.ellipse instanceof Ellipse) { - ctx.strokeStyle = placedColor(); + ctx.strokeStyle = color ? color : placedColor(); ctx.beginPath(); ctx.ellipse( incomingNode.ellipse.center.x + offset.x, @@ -143,3 +144,32 @@ function redrawCut(incomingNode: CutNode) { export function redrawAtom(incomingNode: AtomNode) { drawAtom(incomingNode, placedColor(), false); } + +export function redrawProof() { + //If this is the first step taken in the proof, + //set the current tree as the head of the proof history + let tree: AEGTree; + if (treeContext.proofHistory.length === 0) { + tree = new AEGTree(); + } else { + tree = treeContext.proofHistory[treeContext.proofHistory.length - 1].tree; + } + + cleanCanvas(); + proofString.innerHTML = tree.toString(); + redrawCut(tree.sheet); +} + +/** + * Helper function to highlight the specific selected node + */ +export function highlightNode(child: AtomNode | CutNode, color: string) { + if (child instanceof AtomNode) { + drawAtom(child, color, false); + } 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/EditModeUtils.ts b/src/DrawModes/EditModeUtils.ts index 173a28b4..d67c905b 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; } } @@ -77,24 +78,40 @@ export function drawAltered(incomingNode: CutNode | AtomNode, color: string, cha * is a cut node that has children calls this function on each of its children. * @param incomingNode The current node to be inserted * @param change The difference between the original position and the new position + * @param tree The tree we want to insert the node in. By default, inserts in global draw tree. */ -export function insertChildren(incomingNode: CutNode | AtomNode, change: Point) { +export function insertChildren(incomingNode: CutNode | AtomNode, change: Point, tree?: AEGTree) { + const insertTree = tree ? tree : treeContext.tree; if (incomingNode instanceof CutNode && incomingNode.ellipse !== null) { const tempCut: CutNode = alterCut(incomingNode, change); - treeContext.tree.insert(tempCut); + insertTree.insert(tempCut); //If this node has any children recurses to insert them with the same distance change if (incomingNode.children.length !== 0) { for (let i = 0; i < incomingNode.children.length; i++) { - insertChildren(incomingNode.children[i], change); + insertChildren(incomingNode.children[i], change, tree); } } } else if (incomingNode instanceof AtomNode) { const tempAtom: AtomNode = alterAtom(incomingNode, change); - treeContext.tree.insert(tempAtom); + insertTree.insert(tempAtom); } } +/** + * 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. @@ -122,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/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/ToProofMode.ts b/src/DrawModes/copyFromDraw.ts similarity index 53% rename from src/DrawModes/ToProofMode.ts rename to src/DrawModes/copyFromDraw.ts index 40e9d943..5e5898b2 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, 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 currentPoint: Point; //The current node and its children we will be moving. let selectedNode: CutNode | AtomNode | null = null; @@ -21,95 +21,115 @@ 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 +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; - selectPoint = new Point(event.x, event.y); - selectedNode = treeContext.tree.getLowestNode(selectPoint); - - 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 (tempParent !== null) { - tempParent.remove(selectPoint); - } - redrawTree(treeContext.tree); - } 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()); - } + currentPoint = new Point(event.x - offset.x, event.y - offset.y); + selectedNode = treeContext.tree.getLowestNode(currentPoint); - //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; - redrawTree(treeContext.tree); +export function copyFromDrawMouseMove(event: MouseEvent) { + if (legalNode) { + redrawTree(treeContext.tree); + + currentPoint = new Point(event.x - offset.x, event.y - offset.y); + selectedNode = treeContext.tree.getLowestNode(currentPoint); + + isLegal(); + } } /** * 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() { - if (legalNode) { - //If the selected node is the tree, insert its children so we do not insert another tree. +export function copyFromDrawMouseUp() { + if (legalNode && selectedNode !== null) { + //If the selected node is the tree, insert its children only if (selectedNode instanceof CutNode && selectedNode.ellipse === null) { for (let i = 0; i < selectedNode.children.length; i++) { treeContext.selectForProof.insert(selectedNode.children[i]); } } else { - treeContext.selectForProof.insert(selectedNode!); + treeContext.selectForProof.insert(selectedNode); } + redrawTree(treeContext.tree); - alert("Graph selected, you may now toggle to proof mode"); } + + selectedNode = null; + legalNode = false; } /** * 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); } -/** - * 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() { + //A tree which will contain our selected node so that it can be displayed on the sub bar + const tree = new AEGTree(); + let removed = false; + + if (selectedNode !== null) { + legalNode = true; + + //Temporarily remove the selected part of the tree and highlight selected part only + //If the sheet has been selected, clear the canvas and redraw the entire tree + if ( + selectedNode instanceof AtomNode || + !(selectedNode as CutNode).isEqualTo(tempTree.sheet) + ) { + tree.insert(selectedNode); + const tempParent = tempTree.getLowestParent(currentPoint); + //Remove the selected node from the tree so that it can be highlighted cleanly + if (tempParent !== null) { + tempParent.remove(currentPoint); + removed = true; + } + redrawTree(tempTree); + } else { + tree.sheet = selectedNode as CutNode; + //If the sheet is selected, clear the canvas so that entire tree is highlighted cleanly + cleanCanvas(); + } + + //Highlight the selected part by redrawing in legalColor + if (selectedNode instanceof AtomNode) { + drawAtom(selectedNode, legalColor(), true); + } else { + highlightNode(selectedNode, legalColor()); + } + + //If something was removed, add it back kin + if (removed) { + tempTree.insert(selectedNode); } + } else { + legalNode = false; } + selectString.innerHTML = tree.toString(); } diff --git a/src/ProofTools/DoubleCutDeletionTool.ts b/src/ProofTools/DoubleCutDeletionTool.ts index 7c975caf..db32dffe 100644 --- a/src/ProofTools/DoubleCutDeletionTool.ts +++ b/src/ProofTools/DoubleCutDeletionTool.ts @@ -6,10 +6,12 @@ import {Point} from "../AEG/Point"; import {AtomNode} from "../AEG/AtomNode"; import {CutNode} from "../AEG/CutNode"; -import {drawCut, redrawTree} from "../DrawModes/DrawUtils"; +import {drawCut, redrawProof} from "../DrawModes/DrawUtils"; import {treeContext} from "../treeContext"; import {illegalColor} from "../Themes"; import {offset} from "../DrawModes/DragTool"; +import {ProofNode} from "../AEG/ProofNode"; +import {AEGTree} from "../AEG/AEGTree"; //The node selected with the user mouse down. let currentNode: CutNode | AtomNode | null = null; @@ -17,6 +19,8 @@ let currentNode: CutNode | AtomNode | null = null; //Whether or not the node is allowed to be moved (not the sheet). let legalNode: boolean; +let currentProofTree: AEGTree; + /** * Takes the current point and finds the lowest node containing that point. * If that node is a double cut then it is a legal node and highlights it with the illegal color. @@ -24,7 +28,8 @@ let legalNode: boolean; */ export function doubleCutDeletionMouseDown(event: MouseEvent) { const currentPoint: Point = new Point(event.x - offset.x, event.y - offset.y); - currentNode = treeContext.tree.getLowestNode(currentPoint); + currentProofTree = new AEGTree(treeContext.getLastProofStep().tree.sheet); + currentNode = currentProofTree.getLowestNode(currentPoint); isLegal(); } @@ -36,8 +41,8 @@ export function doubleCutDeletionMouseDown(event: MouseEvent) { */ export function doubleCutDeletionMouseMove(event: MouseEvent) { const currentPoint: Point = new Point(event.x - offset.x, event.y - offset.y); - currentNode = treeContext.tree.getLowestNode(currentPoint); - redrawTree(treeContext.tree); + currentNode = currentProofTree.getLowestNode(currentPoint); + redrawProof(); isLegal(); } @@ -48,19 +53,25 @@ export function doubleCutDeletionMouseMove(event: MouseEvent) { * @param event The event of a mouse up while the user is using double cut deletion */ export function doubleCutDeletionMouseUp(event: MouseEvent) { + //Stores the tree of the previous proof so that we can perform double cut actions without + //altering that tree + const nextProof = new ProofNode(currentProofTree, "Double Cut Deletion"); const currentPoint: Point = new Point(event.x - offset.x, event.y - offset.y); + if (legalNode && currentNode instanceof CutNode) { - const currentParent: CutNode | null = treeContext.tree.getLowestParent(currentPoint); + const currentParent: CutNode | null = nextProof.tree.getLowestParent(currentPoint); const lowerCut: CutNode | AtomNode | null = currentNode.children[0]; if (currentParent !== null && lowerCut instanceof CutNode) { currentParent.remove(currentPoint); for (let i = 0; i < lowerCut.children.length; i++) { - treeContext.tree.insert(lowerCut.children[i]); + nextProof.tree.insert(lowerCut.children[i]); } } + treeContext.proofHistory.push(nextProof); } - redrawTree(treeContext.tree); + + redrawProof(); } /** @@ -68,7 +79,7 @@ export function doubleCutDeletionMouseUp(event: MouseEvent) { */ export function doubleCutDeletionMouseOut() { legalNode = false; - redrawTree(treeContext.tree); + redrawProof(); } /** @@ -81,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/DoubleCutInsertionTool.ts b/src/ProofTools/DoubleCutInsertionTool.ts index 5a0cf994..04b4b25f 100644 --- a/src/ProofTools/DoubleCutInsertionTool.ts +++ b/src/ProofTools/DoubleCutInsertionTool.ts @@ -10,8 +10,10 @@ import {Ellipse} from "../AEG/Ellipse"; import {treeContext} from "../treeContext"; import {offset} from "../DrawModes/DragTool"; import {legalColor, illegalColor} from "../Themes"; -import {drawCut, redrawTree, drawGuidelines} from "../DrawModes/DrawUtils"; +import {drawCut, redrawProof, drawGuidelines} from "../DrawModes/DrawUtils"; import {ellipseLargeEnough, createEllipse} from "../DrawModes/CutTool"; +import {ProofNode} from "../AEG/ProofNode"; +import {AEGTree} from "../AEG/AEGTree"; const showRectElm: HTMLInputElement = document.getElementById("showRect"); @@ -21,12 +23,15 @@ let startingPoint: Point; //Tracks if the mouse has ever left canvas disallowing future movements. let wasOut: boolean; +let currentProofTree: AEGTree; + /** * Records the current point on the canvas. * @param event The double cut event while using the double cut insertion tool */ export function doubleCutInsertionMouseDown(event: MouseEvent) { startingPoint = new Point(event.clientX - offset.x, event.clientY - offset.y); + currentProofTree = new AEGTree(treeContext.getLastProofStep().tree.sheet); wasOut = false; } @@ -40,14 +45,14 @@ export function doubleCutInsertionMouseMove(event: MouseEvent) { const currentPoint: Point = new Point(event.clientX - offset.x, event.clientY - offset.y); const largeCut: CutNode = new CutNode(createEllipse(startingPoint, currentPoint)); const smallCut: CutNode = new CutNode(calcSmallEllipse(largeCut.ellipse)); - redrawTree(treeContext.tree); + redrawProof(); if (!wasOut && largeCut.ellipse !== null && smallCut.ellipse !== null) { //If either ellipse is in an invalid position or too small it cannot be inserted const legal = - treeContext.tree.canInsert(largeCut) && + currentProofTree.canInsert(largeCut) && ellipseLargeEnough(largeCut.ellipse) && - treeContext.tree.canInsert(smallCut) && + currentProofTree.canInsert(smallCut) && ellipseLargeEnough(smallCut.ellipse); const color = legal ? legalColor() : illegalColor(); @@ -68,23 +73,30 @@ export function doubleCutInsertionMouseMove(event: MouseEvent) { */ export function doubleCutInsertionMouseUp(event: MouseEvent) { const currentPoint: Point = new Point(event.clientX - offset.x, event.clientY - offset.y); + currentProofTree = new AEGTree(treeContext.getLastProofStep().tree.sheet); + 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, "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 const legal = - treeContext.tree.canInsert(largeCut) && + currentProofTree.canInsert(largeCut) && ellipseLargeEnough(largeCut.ellipse) && - treeContext.tree.canInsert(smallCut) && + currentProofTree.canInsert(smallCut) && ellipseLargeEnough(smallCut.ellipse); if (legal) { - treeContext.tree.insert(largeCut); - treeContext.tree.insert(smallCut); + nextProof.tree.insert(largeCut); + nextProof.tree.insert(smallCut); + treeContext.proofHistory.push(nextProof); } } - redrawTree(treeContext.tree); + redrawProof(); } /** @@ -92,7 +104,7 @@ export function doubleCutInsertionMouseUp(event: MouseEvent) { */ export function doubleCutInsertionMouseOut() { wasOut = true; - redrawTree(treeContext.tree); + redrawProof(); } /** diff --git a/src/ProofTools/ErasureTool.ts b/src/ProofTools/ErasureTool.ts index 73fc472b..0c2390cf 100644 --- a/src/ProofTools/ErasureTool.ts +++ b/src/ProofTools/ErasureTool.ts @@ -6,11 +6,13 @@ import {Point} from "../AEG/Point"; import {AtomNode} from "../AEG/AtomNode"; import {CutNode} from "../AEG/CutNode"; -import {redrawTree} from "../DrawModes/DrawUtils"; +import {redrawProof} from "../DrawModes/DrawUtils"; import {treeContext} from "../treeContext"; import {illegalColor} from "../Themes"; import {offset} from "../DrawModes/DragTool"; import {highlightChildren} from "../DrawModes/EditModeUtils"; +import {ProofNode} from "../AEG/ProofNode"; +import {AEGTree} from "../AEG/AEGTree"; //The node selected with the user mouse down. let currentNode: CutNode | AtomNode | null = null; @@ -18,6 +20,8 @@ let currentNode: CutNode | AtomNode | null = null; //Whether or not the node is allowed to be moved (not the sheet). let legalNode: boolean; +let currentProofTree: AEGTree; + /** * Captures the current location, and the node linked with that location. * Determines if it is a legal node. @@ -25,7 +29,8 @@ let legalNode: boolean; */ export function erasureMouseDown(event: MouseEvent) { const currentPoint: Point = new Point(event.x - offset.x, event.y - offset.y); - currentNode = treeContext.tree.getLowestNode(currentPoint); + currentProofTree = new AEGTree(treeContext.getLastProofStep().tree.sheet); + currentNode = currentProofTree.getLowestNode(currentPoint); isLegal(); } @@ -37,9 +42,9 @@ export function erasureMouseDown(event: MouseEvent) { */ export function erasureMouseMove(event: MouseEvent) { const currentPoint: Point = new Point(event.x - offset.x, event.y - offset.y); - currentNode = treeContext.tree.getLowestNode(currentPoint); + currentNode = currentProofTree.getLowestNode(currentPoint); - redrawTree(treeContext.tree); + redrawProof(); isLegal(); } @@ -50,12 +55,18 @@ export function erasureMouseMove(event: MouseEvent) { */ 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, "Erasure"); + const currentPoint: Point = new Point(event.x - offset.x, event.y - offset.y); - const currentParent = treeContext.tree.getLowestParent(currentPoint); + const currentParent = nextProof.tree.getLowestParent(currentPoint); if (currentParent !== null) { currentParent.remove(currentPoint); } - redrawTree(treeContext.tree); + + treeContext.proofHistory.push(nextProof); + redrawProof(); } currentNode = null; @@ -68,7 +79,7 @@ export function erasureMouseUp(event: MouseEvent) { export function erasureMouseOut() { currentNode = null; legalNode = false; - redrawTree(treeContext.tree); + redrawProof(); } /** @@ -77,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()); diff --git a/src/ProofTools/InsertionTools.ts b/src/ProofTools/InsertionTools.ts new file mode 100644 index 00000000..e2f34aa1 --- /dev/null +++ b/src/ProofTools/InsertionTools.ts @@ -0,0 +1,258 @@ +/** + * File containing insertion node movement event handlers. + * @author Anusha Tiwari + */ + +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 {redrawProof} from "../DrawModes/DrawUtils"; +import {legalColor, illegalColor} from "../Themes"; +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 currentNode: CutNode | AtomNode; + +//The parent identified the position where we are trying to insert the incoming node +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 in that place. +let legalPlace: boolean; + +//Whether or not the node being placed is a legal node +let legalNode: boolean; + +export function insertionMouseDown(event: MouseEvent) { + //Create a deep copy of the tree we are trying to insert the incoming node into so that we can + //modify it as needed without affecting the actual structure + currentTree = new AEGTree(treeContext.getLastProofStep().tree.sheet); + const selectedNodes = treeContext.selectForProof.sheet.children; + const startingPoint = new Point(event.x - offset.x, event.y - offset.y); + + //we can insert only a single subgraph at a time + if (treeContext.proofHistory.length > 0 && selectedNodes.length === 1) { + //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, currentNode); + + //Get node we have clicked to insert within. If the node is an atom node, get its parent cut + 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 = 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(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; + } + + 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 { + drawAltered(currentNode, illegalColor(), newPoint); + } + } else { + legalPlace = false; + drawAltered(currentNode, illegalColor(), newPoint); + } + } + } + } else { + legalPlace = false; + legalNode = false; + drawAltered(currentNode, illegalColor(), startingPoint); + } +} + +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(); + const newPoint = calculatePoint(event, currentNode); + + //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 + 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(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; + } + + 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 { + drawAltered(currentNode, illegalColor(), newPoint); + } + } else { + legalPlace = false; + drawAltered(currentNode, illegalColor(), newPoint); + } + } + } + } 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) { + //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 (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(); + legalNode = false; +} + +export function insertionMouseOut() { + legalNode = false; + 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); + } + + return undefined; +} 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)))) ); } diff --git a/src/ProofTools/pasteInProof.ts b/src/ProofTools/pasteInProof.ts new file mode 100644 index 00000000..f1405b09 --- /dev/null +++ b/src/ProofTools/pasteInProof.ts @@ -0,0 +1,53 @@ +/** + * File containing insertion node movement event handlers. + * @author Anusha Tiwari + */ +import {CutNode} from "../AEG/CutNode"; +import {treeContext} from "../treeContext"; +import {redrawProof} from "../DrawModes/DrawUtils"; +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 currentGraphs: CutNode; + +//The tree that we are trying to insert the graph into +let currentTree: AEGTree; + +//Whether or not applying this rule will result in the creation of a new node for our proof +let legalNode: boolean; + +export function pasteInProofMouseDown() { + currentTree = new AEGTree(treeContext.getLastProofStep().tree.sheet); + currentGraphs = treeContext.selectForProof.sheet; + + if ( + currentGraphs.children.length > 0 && + treeContext.proofHistory.length === 0 && + currentTree.sheet.isEmptySheet() + ) { + legalNode = true; + } +} + +export function pasteInProofMouseMove() { + legalNode = false; + redrawProof(); +} + +export function pasteInProofMouseUp() { + if (legalNode) { + currentTree.sheet = currentGraphs; + treeContext.proofHistory.push(new ProofNode(currentTree, "Copied from Draw Mode")); + } + legalNode = false; + redrawProof(); +} + +export function pasteInProofMouseOut() { + legalNode = false; + redrawProof(); +} diff --git a/src/ToggleModes.ts b/src/ToggleModes.ts index 89dd11b6..3e898263 100644 --- a/src/ToggleModes.ts +++ b/src/ToggleModes.ts @@ -5,9 +5,9 @@ */ import {loadFile} from "./AEG-IO"; import {AEGTree} from "./AEG/AEGTree"; -import {redrawTree} from "./DrawModes/DrawUtils"; -// import {setMode} from "./index"; -// import {selectedNode} from "./DrawModes/ToProofMode"; +import {ProofNode} from "./AEG/ProofNode"; +import {redrawProof, redrawTree} from "./DrawModes/DrawUtils"; +import {treeString, proofString} from "."; import {Tool, treeContext} from "./treeContext"; //Flag to signify the mode we are in @@ -32,54 +32,49 @@ 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 - proofCachedAEG = JSON.stringify(treeContext.tree); + proofCachedAEG = JSON.stringify(treeContext.proofHistory); proofCachedTool = treeContext.toolState; //Load in our saved draw tree and tool state - const loadedAEG = loadFile(drawCachedAEG); + 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 { throw Error("invalid cached AEG"); } treeContext.toolState = drawCachedTool; + redrawTree(treeContext.tree); } 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 drawCachedAEG = JSON.stringify(treeContext.tree); drawCachedTool = treeContext.toolState; //Load in our saved proof structure and tool state - const loadedProof = loadFile(proofCachedAEG); + let loadedProof: ProofNode[] | null = null; + if (proofCachedAEG !== null) { + loadedProof = loadFile(treeContext.modeState, proofCachedAEG) as ProofNode[] | null; + } if (loadedProof !== null) { - 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); - } catch (error) { - console.log("Could not insert " + child); - } - } - } 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; + treeContext.proofHistory = loadedProof; } - //Reset the state of our tools treeContext.toolState = proofCachedTool; - //The selected node has been loaded in. - //Reset it to avoid accidentally reloading it next time. - treeContext.selectForProof.sheet = new AEGTree().sheet; + redrawProof(); } - redrawTree(treeContext.tree); } diff --git a/src/index.html b/src/index.html index dc1410e7..be7425dc 100644 --- a/src/index.html +++ b/src/index.html @@ -76,7 +76,7 @@ - @@ -86,8 +86,8 @@ -
@@ -107,7 +107,7 @@
-