From af7e9fd126e1460815820130558bf1f890b83291 Mon Sep 17 00:00:00 2001 From: Jack Rutland Date: Sat, 27 Aug 2022 15:49:47 -0400 Subject: [PATCH] README and proof utils Updated readme and has some proof util changes --- README.md | 165 ++++--- client/src/components/Paper/scripts/Atomic.js | 2 +- client/src/components/Paper/scripts/Cut.js | 2 +- client/src/components/Paper/scripts/Sheet.js | 3 +- client/src/index.css | 205 ++------- client/src/util/proof-util.js | 414 ++++++++++++++++++ 6 files changed, 558 insertions(+), 233 deletions(-) create mode 100644 client/src/util/proof-util.js diff --git a/README.md b/README.md index cb60cbb..6769606 100644 --- a/README.md +++ b/README.md @@ -1,73 +1,92 @@ -# Getting Started with Create React App - -This project was bootstrapped with [Create React App](https://github.com/facebook/create-react-app). - -## Available Scripts - -In the project directory, you can run: - -### `npm start` - -Runs the app in the development mode.\ -Open [http://localhost:3000](http://localhost:3000) to view it in the browser. - -The page will reload if you make edits.\ -You will also see any lint errors in the console. - -### `npm test` - -Launches the test runner in the interactive watch mode.\ -See the section about [running tests](https://facebook.github.io/create-react-app/docs/running-tests) for more information. - -### `npm run build` - -Builds the app for production to the `build` folder.\ -It correctly bundles React in production mode and optimizes the build for the best performance. - -The build is minified and the filenames include the hashes.\ -Your app is ready to be deployed! - -See the section about [deployment](https://facebook.github.io/create-react-app/docs/deployment) for more information. - -### `npm run eject` - -**Note: this is a one-way operation. Once you `eject`, you can’t go back!** - -If you aren’t satisfied with the build tool and configuration choices, you can `eject` at any time. This command will remove the single build dependency from your project. - -Instead, it will copy all the configuration files and the transitive dependencies (webpack, Babel, ESLint, etc) right into your project so you have full control over them. All of the commands except `eject` will still work, but they will point to the copied scripts so you can tweak them. At this point you’re on your own. - -You don’t have to ever use `eject`. The curated feature set is suitable for small and middle deployments, and you shouldn’t feel obligated to use this feature. However we understand that this tool wouldn’t be useful if you couldn’t customize it when you are ready for it. - -## Learn More - -You can learn more in the [Create React App documentation](https://facebook.github.io/create-react-app/docs/getting-started). - -To learn React, check out the [React documentation](https://reactjs.org/). - -### Code Splitting - -This section has moved here: [https://facebook.github.io/create-react-app/docs/code-splitting](https://facebook.github.io/create-react-app/docs/code-splitting) - -### Analyzing the Bundle Size - -This section has moved here: [https://facebook.github.io/create-react-app/docs/analyzing-the-bundle-size](https://facebook.github.io/create-react-app/docs/analyzing-the-bundle-size) - -### Making a Progressive Web App - -This section has moved here: [https://facebook.github.io/create-react-app/docs/making-a-progressive-web-app](https://facebook.github.io/create-react-app/docs/making-a-progressive-web-app) - -### Advanced Configuration - -This section has moved here: [https://facebook.github.io/create-react-app/docs/advanced-configuration](https://facebook.github.io/create-react-app/docs/advanced-configuration) - -### Deployment - -This section has moved here: [https://facebook.github.io/create-react-app/docs/deployment](https://facebook.github.io/create-react-app/docs/deployment) - -### `npm run build` fails to minify - -This section has moved here: [https://facebook.github.io/create-react-app/docs/troubleshooting#npm-run-build-fails-to-minify](https://facebook.github.io/create-react-app/docs/troubleshooting#npm-run-build-fails-to-minify) - - -# existential-graphs +
+ +
+
+ GPL 3.0 License +
+ A tool for diagrammatic notation of logical expressions +
+
+ +Existential Graphs is a web app that enables the manipulation of logical expressions using a visual notation. It was created by [Dr. Bram van Heuveln](https://science.rpi.edu/itws/faculty/bram-van-heuveln), whose goal for this project is to provide another unique approach to solving logical expressions to students. + +
+ +## If you would like to access Existential Graphs, the live website can be found [here](https://eg.bram-hub.com/). +> Note: Existential Graphs is currently under development. As such the live website will not always be in sync with what is here in the repository. Currently, the live website is on a functionally complete version, however a rehaul of the website should end up going live in the near future. + +## Table of Contents +- [If you would like to access Existential Graphs, the live website can be found here.](#if-you-would-like-to-access-existential-graphs-the--live-website-can-be-found-here) +- [Table of Contents](#table-of-contents) +- [Background](#background) +- [Use Cases](#use-cases) + - [Guided Proof Mode](#guided-proof-mode) + - [Unguided Proof Mode](#unguided-proof-mode) +- [For Educators](#for-educators) +- [For Students](#for-students) +- [Development](#development) +- [License](#license) + +## Background +Dr. van Heuveln has taught logic courses on a frequent basis for the past 15 years, and noted that a good number of students struggle with the systems of modern formal logic that were developed in the late 1800's and early 1900's, and that have been universally used in logic courses since. These traditional systems use abstract linear symbol strings such as `(P & Q) -> (R v S)`, and deploy even more abstract rules such as & Elim to infer new symbol strings from old ones, thus engaging the user in logical reasoning. + +This project brings about the idea that there are unique ways to view logical expressions, as well as teach students about logic. + +The idea at the core of Existential Graphs, graphical logic, was first written about in 1882 by Charles Sanders Peirce. While it is interesting and in many cases helpful to analyze logical expressions with a graphical system, it is largely infeasible due to physical constraints. The only way to use existential graphs so far has been on paper or a whiteboard, where you are limited by space, and have to redraw the whole logical expression every step, or lose your previous steps. The Existential Graphs web application is one of the first, if not the first, publicly available systems to use graphical logic. + +## Use Cases +The Existential Graphs web application can be used by philosophers, educators, and students alike. The experience can be very beginner friendly in the guided mode, or act more as a sandbox in the unguided proof mode. + + + +### Guided Proof Mode +Guided Proof Mode is intended mainly for beginners to existential graphs. In this mode, you are given a pallet of operations that are available in existential graphs which you are allowed to use to manipulate the graph. You are not allowed to make incorrect proof steps, which makes this a safe space to learn the basics of existential graphs. + +### Unguided Proof Mode +Unguided Proof Mode is the main mode intended for Existential Graphs. In this mode, you can directly operate on the graph and define what proof step you took. This allows for users to make logically invalid steps, which is great for students who are beyond a beginner level. This mode also has proof validation, which will tell you which steps you took were logically valid, as well as the steps that you took that were logically invalid. + +## For Educators +As an educator, you are able to create a "Problem". A problem is simply a graph with an initial state and a goal state. With this problem, you are able to send it to your students and have them solve it. Their goal is to get from the initial state to the goal state, using only valid logical operations. Existential Graphs can check the validity of these steps, making grading easy for educators. + +## For Students +As a student, you are able to upload problem files that you have received from your professor. When you open the problem file, you will see an initial state and a goal state. Your objective is to take the initial state graph, and manipulate it using logical steps until you reach the goal state. As you work with the graph, your steps will create branches, so don't worry about losing your progress if you want to explore a different route. + +Additionally, if you are interested in computer science and programming, please consider contributing to Existential Graphs! Not only would it be a great way to practice logical reasoning, but it is also a great way to dip your toes into open source software and contributing to open source projects. + +## Development +To work on and run this project, you will need to have Node.js installed. + +You will have to run two terminals : + +In the first terminal : +``` +cd server +npm i +npm run start +``` +In the second terminal : +``` +cd client +npm i +npm run start +``` +Now everything should be up and running for you to work on Existential Graphs! +## License +Existential Graphs is licensed under the GPL-3.0 license, which can be viewed [here](LICENSE). +``` +Existential Graphs: A Unique Approach to Formal Logic +Copyright (C) 2022, the Existential Graphs Developers + +This program is free software: you can redistribute it and/or modify +it under the terms of the GNU General Public License as published by +the Free Software Foundation, either version 3 of the License, or +(at your option) any later version. + +This program is distributed in the hope that it will be useful, +but WITHOUT ANY WARRANTY; without even the implied warranty of +MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +GNU General Public License for more details. + +You should have received a copy of the GNU General Public License +along with this program. If not, see . + ``` \ No newline at end of file diff --git a/client/src/components/Paper/scripts/Atomic.js b/client/src/components/Paper/scripts/Atomic.js index 407d9e6..287b847 100644 --- a/client/src/components/Paper/scripts/Atomic.js +++ b/client/src/components/Paper/scripts/Atomic.js @@ -100,7 +100,7 @@ export default class Atomic extends joint.dia.Element { destroy() { this.remove(); - this.sheet.paper.handleDeleteCell(); + //this.sheet.paper.handleDeleteCell(); } obliterate() { diff --git a/client/src/components/Paper/scripts/Cut.js b/client/src/components/Paper/scripts/Cut.js index 8ee6870..487beb4 100644 --- a/client/src/components/Paper/scripts/Cut.js +++ b/client/src/components/Paper/scripts/Cut.js @@ -140,7 +140,7 @@ export default class Cut extends joint.dia.Element { this.sheet.handleCollisions(parent); } - this.sheet.paper.handleDeleteCell(); + //this.sheet.paper.handleDeleteCell(); } //Destroys itself and all decendants obliterate() { diff --git a/client/src/components/Paper/scripts/Sheet.js b/client/src/components/Paper/scripts/Sheet.js index 8ee48b4..62f1bda 100644 --- a/client/src/components/Paper/scripts/Sheet.js +++ b/client/src/components/Paper/scripts/Sheet.js @@ -62,7 +62,8 @@ export default class Sheet { // the diagram (parent / child structure (embedding)) to reflect what the user // sees on the paper let cellbbox = cell.getBoundingBox(); - + + console.log(this); let potential_parents = this.findPotentialParents(cellbbox); let parent = findSmallestCell(potential_parents); diff --git a/client/src/index.css b/client/src/index.css index 122b81d..5d8cc73 100644 --- a/client/src/index.css +++ b/client/src/index.css @@ -569,18 +569,6 @@ video { right: 0px; } -.top-1\/2 { - top: 50%; -} - -.right-20 { - right: 5rem; -} - -.right-1 { - right: 0.25rem; -} - .z-10 { z-index: 10; } @@ -601,6 +589,10 @@ video { margin-right: 5rem; } +.mt-10 { + margin-top: 2.5rem; +} + .mr-5 { margin-right: 1.25rem; } @@ -609,10 +601,6 @@ video { margin-right: 1rem; } -.mt-10 { - margin-top: 2.5rem; -} - .inline-block { display: inline-block; } @@ -638,10 +626,6 @@ video { height: 2.5rem; } -.h-3\/4 { - height: 75%; -} - .h-5\/6 { height: 83.333333%; } @@ -658,45 +642,24 @@ video { width: 2.5rem; } -.w-1\/4 { - width: 25%; -} - -.w-56 { - width: 14rem; -} - -.w-32 { - width: 8rem; -} - -.w-max { - width: -webkit-max-content; - width: max-content; -} - -.w-3\/4 { - width: 75%; +.w-4\/5 { + width: 80%; } -.w-5\/6 { - width: 83.333333%; +.w-2\/5 { + width: 40%; } .w-11\/12 { width: 91.666667%; } -.w-1\/2 { - width: 50%; -} - -.w-2\/5 { - width: 40%; +.w-56 { + width: 14rem; } -.w-4\/5 { - width: 80%; +.w-32 { + width: 8rem; } .origin-top-right { @@ -760,10 +723,6 @@ video { justify-content: space-around; } -.justify-evenly { - justify-content: space-evenly; -} - .gap-4 { gap: 1rem; } @@ -779,10 +738,6 @@ video { border-color: rgb(243 244 246 / var(--tw-divide-opacity)); } -.place-self-center { - place-self: center; -} - .self-center { align-self: center; } @@ -791,24 +746,16 @@ video { justify-self: center; } -.rounded-full { - border-radius: 9999px; -} - -.rounded-md { - border-radius: 0.375rem; -} - .rounded-lg { border-radius: 0.5rem; } -.border-2 { - border-width: 2px; +.rounded-md { + border-radius: 0.375rem; } -.border-b-4 { - border-bottom-width: 4px; +.rounded-full { + border-radius: 9999px; } .border-b-2 { @@ -838,11 +785,6 @@ video { background-color: transparent; } -.bg-slate-400 { - --tw-bg-opacity: 1; - background-color: rgb(148 163 184 / var(--tw-bg-opacity)); -} - .bg-blue-500 { --tw-bg-opacity: 1; background-color: rgb(59 130 246 / var(--tw-bg-opacity)); @@ -853,19 +795,17 @@ video { background-color: rgb(22 163 74 / var(--tw-bg-opacity)); } -.bg-slate-600 { +.bg-slate-400 { --tw-bg-opacity: 1; - background-color: rgb(71 85 105 / var(--tw-bg-opacity)); + background-color: rgb(148 163 184 / var(--tw-bg-opacity)); } -.bg-slate-700 { - --tw-bg-opacity: 1; - background-color: rgb(51 65 85 / var(--tw-bg-opacity)); +.p-5 { + padding: 1.25rem; } -.bg-blue-400 { - --tw-bg-opacity: 1; - background-color: rgb(96 165 250 / var(--tw-bg-opacity)); +.p-4 { + padding: 1rem; } .p-2 { @@ -876,14 +816,6 @@ video { padding: 0.25rem; } -.p-5 { - padding: 1.25rem; -} - -.p-4 { - padding: 1rem; -} - .px-2 { padding-left: 0.5rem; padding-right: 0.5rem; @@ -894,11 +826,6 @@ video { padding-bottom: 0.25rem; } -.px-1 { - padding-left: 0.25rem; - padding-right: 0.25rem; -} - .py-4 { padding-top: 1rem; padding-bottom: 1rem; @@ -909,9 +836,9 @@ video { padding-right: 1.5rem; } -.py-10 { - padding-top: 2.5rem; - padding-bottom: 2.5rem; +.px-1 { + padding-left: 0.25rem; + padding-right: 0.25rem; } .pt-2 { @@ -947,14 +874,9 @@ video { line-height: 1.75rem; } -.text-3xl { - font-size: 1.875rem; - line-height: 2.25rem; -} - -.text-lg { - font-size: 1.125rem; - line-height: 1.75rem; +.text-2xl { + font-size: 1.5rem; + line-height: 2rem; } .text-5xl { @@ -972,9 +894,9 @@ video { line-height: 1.5rem; } -.text-2xl { - font-size: 1.5rem; - line-height: 2rem; +.text-3xl { + font-size: 1.875rem; + line-height: 2.25rem; } .font-medium { @@ -1007,14 +929,9 @@ video { color: rgb(255 255 255 / var(--tw-text-opacity)); } -.text-blue-600 { - --tw-text-opacity: 1; - color: rgb(37 99 235 / var(--tw-text-opacity)); -} - -.text-blue-300 { +.text-slate-500 { --tw-text-opacity: 1; - color: rgb(147 197 253 / var(--tw-text-opacity)); + color: rgb(100 116 139 / var(--tw-text-opacity)); } .text-blue-400 { @@ -1022,11 +939,6 @@ video { color: rgb(96 165 250 / var(--tw-text-opacity)); } -.text-slate-500 { - --tw-text-opacity: 1; - color: rgb(100 116 139 / var(--tw-text-opacity)); -} - .text-blue-500 { --tw-text-opacity: 1; color: rgb(59 130 246 / var(--tw-text-opacity)); @@ -1051,6 +963,12 @@ video { box-shadow: var(--tw-ring-offset-shadow, 0 0 #0000), var(--tw-ring-shadow, 0 0 #0000), var(--tw-shadow); } +.shadow-md { + --tw-shadow: 0 4px 6px -1px rgb(0 0 0 / 0.1), 0 2px 4px -2px rgb(0 0 0 / 0.1); + --tw-shadow-colored: 0 4px 6px -1px var(--tw-shadow-color), 0 2px 4px -2px var(--tw-shadow-color); + box-shadow: var(--tw-ring-offset-shadow, 0 0 #0000), var(--tw-ring-shadow, 0 0 #0000), var(--tw-shadow); +} + .shadow { --tw-shadow: 0 1px 3px 0 rgb(0 0 0 / 0.1), 0 1px 2px -1px rgb(0 0 0 / 0.1); --tw-shadow-colored: 0 1px 3px 0 var(--tw-shadow-color), 0 1px 2px -1px var(--tw-shadow-color); @@ -1063,22 +981,11 @@ video { box-shadow: var(--tw-ring-offset-shadow, 0 0 #0000), var(--tw-ring-shadow, 0 0 #0000), var(--tw-shadow); } -.shadow-md { - --tw-shadow: 0 4px 6px -1px rgb(0 0 0 / 0.1), 0 2px 4px -2px rgb(0 0 0 / 0.1); - --tw-shadow-colored: 0 4px 6px -1px var(--tw-shadow-color), 0 2px 4px -2px var(--tw-shadow-color); - box-shadow: var(--tw-ring-offset-shadow, 0 0 #0000), var(--tw-ring-shadow, 0 0 #0000), var(--tw-shadow); -} - .shadow-slate-500 { --tw-shadow-color: #64748b; --tw-shadow: var(--tw-shadow-colored); } -.shadow-black { - --tw-shadow-color: #000; - --tw-shadow: var(--tw-shadow-colored); -} - .shadow-slate-600 { --tw-shadow-color: #475569; --tw-shadow: var(--tw-shadow-colored); @@ -1118,6 +1025,10 @@ video { transition-duration: 150ms; } +.duration-500 { + transition-duration: 500ms; +} + .duration-100 { transition-duration: 100ms; } @@ -1126,14 +1037,6 @@ video { transition-duration: 75ms; } -.duration-300 { - transition-duration: 300ms; -} - -.duration-500 { - transition-duration: 500ms; -} - .ease-out { transition-timing-function: cubic-bezier(0, 0, 0.2, 1); } @@ -1205,17 +1108,6 @@ html, body, #root, .app { outline-offset: 2px; } -.focus\:ring-0:focus { - --tw-ring-offset-shadow: var(--tw-ring-inset) 0 0 0 var(--tw-ring-offset-width) var(--tw-ring-offset-color); - --tw-ring-shadow: var(--tw-ring-inset) 0 0 0 calc(0px + var(--tw-ring-offset-width)) var(--tw-ring-color); - box-shadow: var(--tw-ring-offset-shadow), var(--tw-ring-shadow), var(--tw-shadow, 0 0 #0000); -} - -.active\:bg-slate-500:active { - --tw-bg-opacity: 1; - background-color: rgb(100 116 139 / var(--tw-bg-opacity)); -} - .active\:bg-blue-600:active { --tw-bg-opacity: 1; background-color: rgb(37 99 235 / var(--tw-bg-opacity)); @@ -1226,18 +1118,17 @@ html, body, #root, .app { background-color: rgb(21 128 61 / var(--tw-bg-opacity)); } +.active\:bg-slate-500:active { + --tw-bg-opacity: 1; + background-color: rgb(100 116 139 / var(--tw-bg-opacity)); +} + .active\:shadow-none:active { --tw-shadow: 0 0 #0000; --tw-shadow-colored: 0 0 #0000; box-shadow: var(--tw-ring-offset-shadow, 0 0 #0000), var(--tw-ring-shadow, 0 0 #0000), var(--tw-shadow); } -.active\:ring-0:active { - --tw-ring-offset-shadow: var(--tw-ring-inset) 0 0 0 var(--tw-ring-offset-width) var(--tw-ring-offset-color); - --tw-ring-shadow: var(--tw-ring-inset) 0 0 0 calc(0px + var(--tw-ring-offset-width)) var(--tw-ring-color); - box-shadow: var(--tw-ring-offset-shadow), var(--tw-ring-shadow), var(--tw-shadow, 0 0 #0000); -} - @media (prefers-color-scheme: dark) { .dark\:bg-slate-700 { --tw-bg-opacity: 1; diff --git a/client/src/util/proof-util.js b/client/src/util/proof-util.js new file mode 100644 index 0000000..d1e10aa --- /dev/null +++ b/client/src/util/proof-util.js @@ -0,0 +1,414 @@ +/** + * proof-util.js + * + * @summary Provides utilities for existential graphs proofs + */ + + + +/******************************************************************** + * Guided Mode * + * Proof Actions * + *******************************************************************/ +export const inferenceInsertion = function(sheet, model, mousePosition) { + console.log('ARGS', arguments); + if(model.__proto__.constructor.name === "Cut" && (model.attributes.level) % 2 === 0) return; + console.log('opening modal...') + const paper = sheet.paper; + paper.props.handleOpenModal(mousePosition, model); +} + +export const inferenceErasure = function(sheet, model) { + console.log(model.attributes.attrs.level) + if(model.attributes.attrs.level % 2 === 0) { + const children = model.getEmbeddedCells({deep: true}); + const parent = sheet.graph.getCell(model.attributes.parent); + + model.destroy(); + for (let i = 0; i < children.length; i++){ + children[i].destroy(); + } + + if(parent) { + sheet.handleCollisions(parent); + } + } +} + +export const insertDoubleCut = function(sheet, model, mousePosition={}) { + let position = {}; + let size = {} + if (!model && mousePosition) { + position = mousePosition; + size = { width: 80, height: 80 } + } + else if (model){ + position = model.get('position'); + size = { width: model.attr('rect/width'), height: model.attr('rect/height') } + } + else { + throw new Error('Bad arguments'); + } + const multipliers = [0.8, 0.25]; + let new_cuts = [] + for(let i = 0; i < multipliers.length; i++) { + new_cuts.push(sheet.addCut({ + position: { + x: position.x - (size.width * multipliers[i]/2), + y: position.y - (size.height * multipliers[i]/2) + }, + attrs: { + rect: { + width: size.width * (1 + multipliers[i]), + height: size.height * (1 + multipliers[i]) + } + } + }, false)); + } + new_cuts[0].embed(new_cuts[1]) + sheet.colorByLevel(new_cuts[0]) + let selected_premise = sheet.paper.selected_premise; + if (selected_premise && selected_premise.attributes.type === "dia.Element.Cut") { + selected_premise.embed(new_cuts[0]); + sheet.colorByLevel(selected_premise) + sheet.pack(selected_premise) + } + sheet.handleCollisions(new_cuts[0]) +} + +export const deleteDoubleCut = function(sheet, model) { + console.log("MODEL: ", model); + const graph = sheet.graph; + if(model.__proto__.constructor.name === "Cut" && model.attributes.embeds?.length === 1 && + graph.getCell(model.attributes.embeds[0]).__proto__.constructor.name === "Cut") { + const children = graph.getCell(model.attributes.embeds[0]).attributes.embeds; + graph.getCell(model.attributes.embeds[0]).destroy(); + model.destroy(); + if(model.attributes.parent) { + sheet.handleCollisions(graph.getCell(model.attributes.parent)); + } + else { + children?.forEach(element => { + if(graph.getCell(element).__proto__.constructor.name === "Cut") { + sheet.handleCollisions(graph.getCell(element)) + } + }); + } + } +} + +export const iteration = function(sheet, model) { + return iterationend.bind(null, model); +} + +const iterationend = function(model, sheet, model_clone, mousePosition={}) { + let subgraph = sheet.graph.cloneSubgraph([model], {deep: true}); + let sub_id = sheet.addSubgraph(subgraph, mousePosition, model_clone); + + subgraph = sheet.graph.getCell(sub_id); + if(!legalIteration(sheet,model,subgraph)) { + obliterate(sheet, subgraph); + } +} + +export const deiteration = function(sheet, model) { + const model_id = model.id; + + let ancestor = model; + while(ancestor.attributes.parent) { + // Iterate up to parent + ancestor = sheet.graph.getCell(ancestor.attributes.parent); + + // Parent must be of type cut, however we check for redundancy + if(ancestor.__proto__.constructor.name !== "Cut") { + console.error("Parent is of type " + ancestor.__proto__.constructor.name + ". Expected Cut. Contact administrator." ); + return; + } + + // Now, recursivly check all premises in the cut and look for a matching subgraph + let children = ancestor.attributes.embeds + + children?.forEach(element => { + let child = sheet.graph.getCell(element); + //Check if premise text is the same and if premise id is dissimilar + if(child.id !== model_id && + matchingModel(sheet, model, child)) { + // Remove desired element and return + obliterate(sheet, model); + return; + } + }); + } + + // Finally, check sheet of assertion becuase of Joey's "Multi-tree" theory... + + let all_models = sheet.graph.attributes.cells.models; + + all_models?.forEach(element => { + let child = sheet.graph.getCell(element); + if(child?.attributes.attrs.level === 0 && + child?.id !== model_id && + matchingModel(sheet, model,child)) { + // Remove desired element and return + obliterate(sheet, model); + return; + } + }); +} + + +/******************************************************************** + * All Modes * + * Graph Validation * + *******************************************************************/ + + +/** + * Returns if two subgraphs match. + * @param {Sheet} sheet - The sheet the two subgraphs are contained by. + * @param {Cell} model_one - The root cell of the first subgraph. + * @param {Cell} model_two - The root cell of the second subgraph. + * @returns {Boolean} - If the two subgraphs match. + */ +function matchingModel(sheet, model_one, model_two) { + + // If comparing premise to a cut, return false + if(model_one.__proto__.constructor.name !== model_two.__proto__.constructor.name) return false; + + // If comparing a premise to a premise, return based on text + if (model_one.__proto__.constructor.name === "Premise") { + return model_one.attributes.attrs.text.text === model_two.attributes.attrs.text.text; + } + + // If comparing a cut, return based on a match to all children + if(model_one.__proto__.constructor.name === "Cut") { + + // Get the children of each cut + let model_one_children = [...(model_one.attributes.embeds || [])]; + let model_two_children = [...(model_two.attributes.embeds || [])]; + + // If both embeds dont exist + if(!model_one_children && !model_two_children) return true; + + // If dissimilar sizes, return false + if(model_one_children.length !== model_two_children.length) return false; + + // Match children until children array are of size zero, or all options are exaughsted + // Runtime : O(n^2) where n = number of children per model. + // To attempt optimization, search for "Graph Isomorphism Problem" + outer: + while(model_one_children.length > 0) { + let child = sheet.graph.getCell(model_one_children[0]); + + // Iterate through all children of model_two and compare to child + for (let i = 0; i < model_two_children.length; i++) { + if(matchingModel(sheet, child, sheet.graph.getCell(model_two_children[i]))) { + // Remove the elements from the arrays + model_one_children.shift() // Removes the first index + model_two_children.splice(i, 1) // Removes index i + continue outer; + } + } + // If you get here, it didn't match :( + return false; + } + // If you get here, it matched! Congrats! :) + return true; + } + // If comparing something other than a premise or cut, contact an administatior + console.error("Can not compare models of type " + model_one.__proto__.constructor.name + ". Contact administrator"); + return false; +} + +/** + * Returns if two subgraphs match. + * @param {Sheet} sheet_one - The sheet the the first subgraph is contained by. + * @param {Sheet} sheet_two - The sheet the the second subgraph is contained by. + * @param {Cell} model_one - The root cell of the first subgraph. + * @param {Cell} model_two - The root cell of the second subgraph. + * @returns {Boolean} - If the two subgraphs match. + */ + function crossMatchingModel(sheet_one, sheet_two, model_one, model_two) { + + // If comparing premise to a cut, return false + if(model_one.__proto__.constructor.name !== model_two.__proto__.constructor.name) return false; + + // If comparing a premise to a premise, return based on text + if (model_one.__proto__.constructor.name === "Premise") { + return model_one.attributes.attrs.text.text === model_two.attributes.attrs.text.text; + } + + // If comparing a cut, return based on a match to all children + if(model_one.__proto__.constructor.name === "Cut") { + + // Get the children of each cut + let model_one_children = [...(model_one.attributes.embeds || [])]; + let model_two_children = [...(model_two.attributes.embeds || [])]; + + // If both embeds dont exist + if(!model_one_children && !model_two_children) return true; + + // If dissimilar sizes, return false + if(model_one_children.length !== model_two_children.length) return false; + + // Match children until children array are of size zero, or all options are exaughsted + // Runtime : O(n^2) where n = number of children per model. + // To attempt optimization, search for "Graph Isomorphism Problem" + outer: + while(model_one_children.length > 0) { + let child = sheet_one.graph.getCell(model_one_children[0]); + + // Iterate through all children of model_two and compare to child + for (let i = 0; i < model_two_children.length; i++) { + if(crossMatchingModel(sheet_one, sheet_two, child, sheet_two.graph.getCell(model_two_children[i]))) { + // Remove the elements from the arrays + model_one_children.shift() // Removes the first index + model_two_children.splice(i, 1) // Removes index i + continue outer; + } + } + // If you get here, it didn't match :( + return false; + } + // If you get here, it matched! Congrats! :) + return true; + } + // If comparing something other than a premise or cut, contact an administatior + console.error("Can not compare models of type " + model_one.__proto__.constructor.name + ". Contact administrator"); + return false; +} + +/** + * Destroys the root and all decendants. + * @param {Sheet} sheet - The sheet the subgraph is contained by. + * @param {Cell} model - Root of subgraph to be destroyed. + */ +function obliterate(sheet, model) { + // If premise or empty cell + if(model.__proto__.constructor.name === "Premise" || model.attributes.embeds?.length === 0) { + model.destroy(); + console.log('ballse'); + return; + } + + // If non-empty cell, destroy all children + let children = model.attributes.embeds; + children.forEach(child => {obliterate(sheet, sheet.graph.getCell(child))}); + // Then destroy self + model.destroy(); + + + +} + +/** + * Returns if a iteration is legal + * @param {Sheet} sheet - The sheet the subgraphs are contained by. + * @param {Cell} model - The origin subgraph. + * @param {Cell} model_clone - The clone of the origin subgraph + * @returns {Boolean} - If the iteration is legal. + */ +function legalIteration(sheet, model, model_clone) { + // First, confirm the two models are the same. + if(!matchingModel(sheet, model,model_clone)) { + console.error("Model discrepency when detecting legality of iteration."); + return false; + } + // If the first model is on the sheet of assertion return true + if(model.attributes.attrs.level === 0) { return true; } + + // If the clone is on a lower level than the origin, return false + if(model.attributes.attrs.level > model_clone.attributes.attrs.level) { return false; } + + // Add all sibling cuts to a list (all children of parent, remove self) + let search = [...sheet.graph.getCell(model.attributes.parent).attributes.embeds]; + search.splice(search.indexOf(model.id, 1)); + + //Iterativly search + + while(search.length > 0) { + let current = search.shift(); + // Check if it is clone + if( current === model_clone.id) { + return true; + } + // If it is a cut, add all children + if(sheet.graph.getCell(current).__proto__.constructor.name === "Cut") { + sheet.graph.getCell(current).attributes.embeds?.forEach( element => { + search.push(element); + }); + } + } + + // If you get here, it's illegal! >:o + return false; +} + +/** + * Gets the root elements of the sheet + * @param {Sheet} graph + * @returns {Array} - ID's to all root elements of the sheet. + */ +function getRootElements(graph) { + + let roots = []; + + graph.attributes.cells.models.forEach( (model) => { + if(model.attributes.attrs.level === 0) { + roots.push(model); + } + } ); + + return roots; +} + +/** + * Finds (graph_final) - (graph_init ∩ graph_final) + * That is anything that has been added to the graph + * @param {Sheet} graph_init + * @param {Sheet} graph_final + */ +function getDifference(graph_init, graph_final) { + + let difference = {} + + let roots_init = getRootElements(graph_init); + let roots_final = getRootElements(graph_final); + + for( let i = roots_init.length - 1; i >= 0; i--) {: + for( let j = roots_final.length - 1; j >= 0; j--) { + if( crossMatchingModel(graph_init, graph_final, graph_init.graph.getCell(roots_init[i]), graph_final.graph.getCell(roots_final[j])) ) { + roots_init.splice(i, 1); + roots_final.splice(j, 1); + break; + } + } + } + + +} +/******************************************************************** + * Freeform Mode * + * Step Validation * + *******************************************************************/ + +export const proof = { + 'INSERTION' : 1, + 'ERASURE' : 2, + 'INSERT_DOUBLE_CUT' : 3, + 'DELETE_DOUBLE_CUT' : 4, + 'ITERATION' : 5, + 'DEITERATION' : 6, +} + +/** + * Verifies if a proof step is valid. + * + * @param {Sheet} graph_init - The initial state of the graph. + * @param {Sheet} graph_final - The final state of the graph. + * @param {Number} proof_step - The id for the proof step type. + * @returns {Boolean} - If the step is valid. + */ +function verify_step(graph_init, graph_final, proof_step) { + +} \ No newline at end of file