diff --git a/package-lock.json b/package-lock.json index 355a633..5cb0392 100644 --- a/package-lock.json +++ b/package-lock.json @@ -5880,9 +5880,9 @@ } }, "elliptic": { - "version": "6.5.2", - "resolved": "https://registry.npmjs.org/elliptic/-/elliptic-6.5.2.tgz", - "integrity": "sha512-f4x70okzZbIQl/NSRLkI/+tteV/9WqL98zx+SQ69KbXxmVrmjwsNUPn/gYJJ0sHvEak24cZgHIPegRePAtA/xw==", + "version": "6.5.3", + "resolved": "https://registry.npmjs.org/elliptic/-/elliptic-6.5.3.tgz", + "integrity": "sha512-IMqzv5wNQf+E6aHeIqATs0tOLeOTwj1QKbRcS3jBbYkl5oLAserA8yJTT7/VyHUYG91PRmPyeQDObKLPpeS4dw==", "requires": { "bn.js": "^4.4.0", "brorand": "^1.0.1", @@ -6686,9 +6686,9 @@ "integrity": "sha1-Qa4u62XvpiJorr/qg6x9eSmbCIc=" }, "eventemitter3": { - "version": "4.0.0", - "resolved": "https://registry.npmjs.org/eventemitter3/-/eventemitter3-4.0.0.tgz", - "integrity": "sha512-qerSRB0p+UDEssxTtm6EDKcE7W4OaoisfIMl4CngyEhjpYglocpNg6UEqCvemdGhosAsg4sO2dXJOdyBifPGCg==" + "version": "4.0.7", + "resolved": "https://registry.npmjs.org/eventemitter3/-/eventemitter3-4.0.7.tgz", + "integrity": "sha512-8guHBZCwKnFhYdHr2ysuRWErTwhoN2X8XELRlrRwpmfeY2jjuUN4taQMsULKUVo1K4DvZl+0pgfyoysHxvmvEw==" }, "events": { "version": "3.1.0", @@ -7162,11 +7162,6 @@ "bser": "2.1.1" } }, - "figgy-pudding": { - "version": "3.5.2", - "resolved": "https://registry.npmjs.org/figgy-pudding/-/figgy-pudding-3.5.2.tgz", - "integrity": "sha512-0btnI/H8f2pavGMN8w40mlSKOfTK2SVJmBfBeVIj3kNw0swwgzyRq0d5TJVOwodFmtvpPeWPN/MCcfuWF0Ezbw==" - }, "figures": { "version": "3.2.0", "resolved": "https://registry.npmjs.org/figures/-/figures-3.2.0.tgz", @@ -7354,22 +7349,9 @@ } }, "follow-redirects": { - "version": "1.11.0", - "resolved": "https://registry.npmjs.org/follow-redirects/-/follow-redirects-1.11.0.tgz", - "integrity": "sha512-KZm0V+ll8PfBrKwMzdo5D13b1bur9Iq9Zd/RMmAoQQcl2PxxFml8cxXPaaPYVbV0RjNjq1CU7zIzAOqtUPudmA==", - "requires": { - "debug": "^3.0.0" - }, - "dependencies": { - "debug": { - "version": "3.2.6", - "resolved": "https://registry.npmjs.org/debug/-/debug-3.2.6.tgz", - "integrity": "sha512-mel+jf7nrtEl5Pn1Qx46zARXKDpBbvzezse7p7LqINmdoIk8PYP5SySaxEmYv6TZ0JyEKA1hsCId6DIhgITtWQ==", - "requires": { - "ms": "^2.1.1" - } - } - } + "version": "1.13.0", + "resolved": "https://registry.npmjs.org/follow-redirects/-/follow-redirects-1.13.0.tgz", + "integrity": "sha512-aq6gF1BEKje4a9i9+5jimNFIpq4Q1WiwBToeRK5NvZBd/TRsmW8BsJfOEGkr76TbOyPVD3OVDN910EcUNtRYEA==" }, "for-in": { "version": "1.0.2", @@ -8093,9 +8075,9 @@ } }, "http-proxy": { - "version": "1.18.0", - "resolved": "https://registry.npmjs.org/http-proxy/-/http-proxy-1.18.0.tgz", - "integrity": "sha512-84I2iJM/n1d4Hdgc6y2+qY5mDaz2PUVjlg9znE9byl+q0uC3DeByqBGReQu5tpLK0TAqTIXScRUV+dg7+bUPpQ==", + "version": "1.18.1", + "resolved": "https://registry.npmjs.org/http-proxy/-/http-proxy-1.18.1.tgz", + "integrity": "sha512-7mz/721AbnJwIVbnaSv1Cz3Am0ZLT/UBwkC92VlxhXv/k/BBQfM2fXElQNC27BVGr0uwUpplYPQM9LnaBMR5NQ==", "requires": { "eventemitter3": "^4.0.0", "follow-redirects": "^1.0.0", @@ -12343,23 +12325,6 @@ "yallist": "^4.0.0" } }, - "mississippi": { - "version": "3.0.0", - "resolved": "https://registry.npmjs.org/mississippi/-/mississippi-3.0.0.tgz", - "integrity": "sha512-x471SsVjUtBRtcvd4BzKE9kFC+/2TeWgKCgw0bZcw1b9l2X3QX5vCWgF+KaZaYm87Ss//rHnWryupDrgLvmSkA==", - "requires": { - "concat-stream": "^1.5.0", - "duplexify": "^3.4.2", - "end-of-stream": "^1.1.0", - "flush-write-stream": "^1.0.0", - "from2": "^2.1.0", - "parallel-transform": "^1.1.0", - "pump": "^3.0.0", - "pumpify": "^1.3.3", - "stream-each": "^1.1.0", - "through2": "^2.0.0" - } - }, "mixin-deep": { "version": "1.3.2", "resolved": "https://registry.npmjs.org/mixin-deep/-/mixin-deep-1.3.2.tgz", @@ -12377,29 +12342,6 @@ "minimist": "^1.2.5" } }, - "move-concurrently": { - "version": "1.0.1", - "resolved": "https://registry.npmjs.org/move-concurrently/-/move-concurrently-1.0.1.tgz", - "integrity": "sha1-viwAX9oy4LKa8fBdfEszIUxwH5I=", - "requires": { - "aproba": "^1.1.1", - "copy-concurrently": "^1.0.0", - "fs-write-stream-atomic": "^1.0.8", - "mkdirp": "^0.5.1", - "rimraf": "^2.5.4", - "run-queue": "^1.0.3" - }, - "dependencies": { - "rimraf": { - "version": "2.7.1", - "resolved": "https://registry.npmjs.org/rimraf/-/rimraf-2.7.1.tgz", - "integrity": "sha512-uWjbaKIK3T1OSVptzX7Nl6PvQ3qAGtKEtVRjRuazjfL3Bx5eI409VZSqgND+4UNnmzLVdPj9FqFJNPqBZFve4w==", - "requires": { - "glob": "^7.1.3" - } - } - } - }, "ms": { "version": "2.1.2", "resolved": "https://registry.npmjs.org/ms/-/ms-2.1.2.tgz", @@ -12500,9 +12442,9 @@ } }, "node-forge": { - "version": "0.9.0", - "resolved": "https://registry.npmjs.org/node-forge/-/node-forge-0.9.0.tgz", - "integrity": "sha512-7ASaDa3pD+lJ3WvXFsxekJQelBKRpne+GOVbLbtHYdd7pFspyeuJHnWfLplGf3SwKGbfs/aYl5V/JCIaHVUKKQ==" + "version": "0.10.0", + "resolved": "https://registry.npmjs.org/node-forge/-/node-forge-0.10.0.tgz", + "integrity": "sha512-PPmu8eEeG9saEUvI97fm4OYxXVB6bFvyNTyiUOBichBpFG8A1Ljw3bY62+5oOjDEMHRnd0Y7HQ+x7uzxOzC6JA==" }, "node-gyp": { "version": "3.8.0", @@ -14921,6 +14863,14 @@ "prop-types": "^15.7.2" } }, + "react-switch": { + "version": "5.0.1", + "resolved": "https://registry.npmjs.org/react-switch/-/react-switch-5.0.1.tgz", + "integrity": "sha512-Pa5kvqRfX85QUCK1Jv0rxyeElbC3aNpCP5hV0LoJpU/Y6kydf0t4kRriQ6ZYA4kxWwAYk/cH51T4/sPzV9mCgQ==", + "requires": { + "prop-types": "^15.6.2" + } + }, "react-transition-group": { "version": "1.2.1", "resolved": "https://registry.yarnpkg.com/react-transition-group/-/react-transition-group-1.2.1.tgz", @@ -15816,11 +15766,11 @@ "integrity": "sha1-Yl2GWPhlr0Psliv8N2o3NZpJlMo=" }, "selfsigned": { - "version": "1.10.7", - "resolved": "https://registry.npmjs.org/selfsigned/-/selfsigned-1.10.7.tgz", - "integrity": "sha512-8M3wBCzeWIJnQfl43IKwOmC4H/RAp50S8DF60znzjW5GVqTcSe2vWclt7hmYVPkKPlHWOu5EaWOMZ2Y6W8ZXTA==", + "version": "1.10.8", + "resolved": "https://registry.npmjs.org/selfsigned/-/selfsigned-1.10.8.tgz", + "integrity": "sha512-2P4PtieJeEwVgTU9QEcwIRDQ/mXJLX8/+I3ur+Pg16nS8oNbrGxEso9NyYWy8NAmXiNl4dlAp5MwoNeCWzON4w==", "requires": { - "node-forge": "0.9.0" + "node-forge": "^0.10.0" } }, "semver": { @@ -18514,6 +18464,43 @@ "ssri": "^6.0.1", "unique-filename": "^1.1.1", "y18n": "^4.0.0" + }, + "dependencies": { + "figgy-pudding": { + "version": "3.5.2", + "resolved": "https://registry.npmjs.org/figgy-pudding/-/figgy-pudding-3.5.2.tgz", + "integrity": "sha512-0btnI/H8f2pavGMN8w40mlSKOfTK2SVJmBfBeVIj3kNw0swwgzyRq0d5TJVOwodFmtvpPeWPN/MCcfuWF0Ezbw==" + }, + "mississippi": { + "version": "3.0.0", + "resolved": "https://registry.npmjs.org/mississippi/-/mississippi-3.0.0.tgz", + "integrity": "sha512-x471SsVjUtBRtcvd4BzKE9kFC+/2TeWgKCgw0bZcw1b9l2X3QX5vCWgF+KaZaYm87Ss//rHnWryupDrgLvmSkA==", + "requires": { + "concat-stream": "^1.5.0", + "duplexify": "^3.4.2", + "end-of-stream": "^1.1.0", + "flush-write-stream": "^1.0.0", + "from2": "^2.1.0", + "parallel-transform": "^1.1.0", + "pump": "^3.0.0", + "pumpify": "^1.3.3", + "stream-each": "^1.1.0", + "through2": "^2.0.0" + } + }, + "move-concurrently": { + "version": "1.0.1", + "resolved": "https://registry.npmjs.org/move-concurrently/-/move-concurrently-1.0.1.tgz", + "integrity": "sha1-viwAX9oy4LKa8fBdfEszIUxwH5I=", + "requires": { + "aproba": "^1.1.1", + "copy-concurrently": "^1.0.0", + "fs-write-stream-atomic": "^1.0.8", + "mkdirp": "^0.5.1", + "rimraf": "^2.5.4", + "run-queue": "^1.0.3" + } + } } }, "chownr": { @@ -18626,9 +18613,12 @@ } }, "serialize-javascript": { - "version": "2.1.2", - "resolved": "https://registry.npmjs.org/serialize-javascript/-/serialize-javascript-2.1.2.tgz", - "integrity": "sha512-rs9OggEUF0V4jUSecXazOYsLfu7OGK2qIn3c7IPBiffz32XniEp/TX9Xmc9LQfK2nQ2QKHvZ2oygKUGU0lG4jQ==" + "version": "4.0.0", + "resolved": "https://registry.npmjs.org/serialize-javascript/-/serialize-javascript-4.0.0.tgz", + "integrity": "sha512-GaNA54380uFefWghODBWEGisLZFj00nS5ACs6yHa9nLqlLpVLO8ChDGeKRjZnV4Nh4n0Qi7nhYZD/9fCPzEqkw==", + "requires": { + "randombytes": "^2.1.0" + } }, "ssri": { "version": "6.0.1", @@ -18636,22 +18626,39 @@ "integrity": "sha512-3Wge10hNcT1Kur4PDFwEieXSCMCJs/7WvSACcrMYrNp+b8kDL1/0wJch5Ni2WrtwEa2IO8OsVfeKIciKCDx/QA==", "requires": { "figgy-pudding": "^3.5.1" + }, + "dependencies": { + "figgy-pudding": { + "version": "3.5.2", + "resolved": "https://registry.npmjs.org/figgy-pudding/-/figgy-pudding-3.5.2.tgz", + "integrity": "sha512-0btnI/H8f2pavGMN8w40mlSKOfTK2SVJmBfBeVIj3kNw0swwgzyRq0d5TJVOwodFmtvpPeWPN/MCcfuWF0Ezbw==" + } } }, "terser-webpack-plugin": { - "version": "1.4.3", - "resolved": "https://registry.npmjs.org/terser-webpack-plugin/-/terser-webpack-plugin-1.4.3.tgz", - "integrity": "sha512-QMxecFz/gHQwteWwSo5nTc6UaICqN1bMedC5sMtUc7y3Ha3Q8y6ZO0iCR8pq4RJC8Hjf0FEPEHZqcMB/+DFCrA==", + "version": "1.4.5", + "resolved": "https://registry.npmjs.org/terser-webpack-plugin/-/terser-webpack-plugin-1.4.5.tgz", + "integrity": "sha512-04Rfe496lN8EYruwi6oPQkG0vo8C+HT49X687FZnpPF0qMAIHONI6HEXYPKDOE8e5HjXTyKfqRd/agHtH0kOtw==", "requires": { "cacache": "^12.0.2", "find-cache-dir": "^2.1.0", "is-wsl": "^1.1.0", "schema-utils": "^1.0.0", - "serialize-javascript": "^2.1.2", + "serialize-javascript": "^4.0.0", "source-map": "^0.6.1", "terser": "^4.1.2", "webpack-sources": "^1.4.0", "worker-farm": "^1.7.0" + }, + "dependencies": { + "worker-farm": { + "version": "1.7.0", + "resolved": "https://registry.npmjs.org/worker-farm/-/worker-farm-1.7.0.tgz", + "integrity": "sha512-rvw3QTZc8lAxyVrqcSGVm5yP/IJ2UcB3U0graE3LCFoZ0Yn2x4EoVSqJKdB/T5M+FLcRPjz4TDacRf3OCfNUzw==", + "requires": { + "errno": "~0.1.7" + } + } } }, "to-regex-range": { @@ -19750,14 +19757,6 @@ "workbox-core": "^5.1.4" } }, - "worker-farm": { - "version": "1.7.0", - "resolved": "https://registry.npmjs.org/worker-farm/-/worker-farm-1.7.0.tgz", - "integrity": "sha512-rvw3QTZc8lAxyVrqcSGVm5yP/IJ2UcB3U0graE3LCFoZ0Yn2x4EoVSqJKdB/T5M+FLcRPjz4TDacRf3OCfNUzw==", - "requires": { - "errno": "~0.1.7" - } - }, "worker-rpc": { "version": "0.1.1", "resolved": "https://registry.npmjs.org/worker-rpc/-/worker-rpc-0.1.1.tgz", diff --git a/package.json b/package.json index d6dbadb..16e4c1a 100644 --- a/package.json +++ b/package.json @@ -20,6 +20,7 @@ "react-scripts": "^4.0.0", "react-sizeme": "^2.6.12", "react-svg": "^11.0.18", + "react-switch": "^5.0.1", "react-transition-group": "1.x" }, "scripts": { diff --git a/src/App.js b/src/App.js index fd21ba4..ae4c60d 100644 --- a/src/App.js +++ b/src/App.js @@ -14,11 +14,13 @@ class App extends React.Component { this.openCanvas = this.openCanvas.bind(this); this.saveProof = this.saveProof.bind(this); this.getRecents = this.getRecents.bind(this); + this.setStyle = this.setStyle.bind(this); this.introWindow = React.createRef(); this.state = { initialCSS: 'initial', canvasOpen: false, popupOpen: false, + fitchStyle: true, filename: '', proof: { premises: [], @@ -103,6 +105,10 @@ class App extends React.Component { this.setState({ popupOpen: true }) } + setStyle(bool) { + this.setState({ fitchStyle: bool }); + } + render() { if (this.state.canvasOpen) { return ( @@ -137,7 +143,9 @@ class App extends React.Component { + setupFunc={this.setupProof} + setStyle={this.setStyle} + proofStyle={this.state.fitchStyle} /> ); } diff --git a/src/converters.js b/src/converters.js index 710f7e9..c6aac8f 100644 --- a/src/converters.js +++ b/src/converters.js @@ -55,6 +55,55 @@ const convertToTeX = (formula) => { else return "" } +const wrapVarsTeX = (formula) => { + if (typeof formula === 'string' || formula instanceof String) { + function consume(c) { + if (formula.length > 0 && c === formula[0]) { + formula = formula.substring(1); + return true; + } + return false; + } + + function parseId() { + let str = "{" + while (formula.length > 0 + && formula[0] !== '(' + && formula[0] !== ')') { + + str += formula[0] + consume(formula[0]) + } + return str + "}"; + } + + function parseExpression() { + let str = "" + while (true) { + if (consume('(')) { + str += "(" + let newExpr = parseExpression() + str += newExpr + if (newExpr === "") + str += "{}" + if (!consume(')')) + return null; + str += ")" + } else if (formula[0] !== ")") { + str += parseId() + } else break; + if (formula.length === 0) { + break; + } + } + return str; + } + + return parseExpression(); + } + else return null +} + /** * @param {string} statement * @return {int} counts the number of unary operators in the given input. @@ -169,7 +218,7 @@ const convertToArray = (formula) => { else return null } -console.log(convertToArray('((({P}(({Q}({R})))))({T}))({T}){P}')) +console.log(wrapVarsTeX('(((P((Q(R)))))(T))(T)P')) /** * Export all converters @@ -178,5 +227,6 @@ export { convertToTeX, convertToEG, convertToArray, + wrapVarsTeX, verifySentence } \ No newline at end of file diff --git a/src/intro/CreateNew.js b/src/intro/CreateNew.js index a9fa6b7..c0de8a7 100644 --- a/src/intro/CreateNew.js +++ b/src/intro/CreateNew.js @@ -1,6 +1,6 @@ import React from 'react'; import verify from '../verifySentence'; -import { convertToTeX, convertToEG } from '../converters'; +import { convertToTeX, convertToEG, wrapVarsTeX } from '../converters'; // KATEX import 'katex/dist/katex.min.css'; import TeX from '@matejmazur/react-katex'; @@ -55,15 +55,13 @@ class CreateNew extends React.Component { } create() { - console.log("Creating...") - console.log("Verification concluded " + this.verify()) + let { useFitchNotation } = this.props; if (this.verify()) { let { premises, conclusion } = this.state; for (let i in premises) { - premises[i] = convertToEG(premises[i]) - console.log(premises[i]) + premises[i] = useFitchNotation ? convertToEG(premises[i]) : wrapVarsTeX(premises[i]) } - conclusion = convertToEG(conclusion) + conclusion = useFitchNotation ? convertToEG(conclusion) : wrapVarsTeX(conclusion) this.props.setupFunc(this.filename.current.value, { premises, conclusion, steps: [] }) } } @@ -72,7 +70,11 @@ class CreateNew extends React.Component { let tex, eg if (verify(formula)) { tex = convertToTeX(formula); - eg = convertToEG(formula); + if (this.props.useFitchNotation) + eg = convertToEG(formula); + else { + eg = convertToEG(formula); + } } let closeBtn = {tex && } - + {this.props.useFitchNotation && {eg && } - + } { closeBtn } ); @@ -119,14 +121,17 @@ class CreateNew extends React.Component { Formula - TeX notationEG notation + {this.props.useFitchNotation && TeX notation} + EG notation + {premises.map((formula,i) => this.getFormulaCell(formula, i))} this.setState({ premises: premises.concat(['']) }) }> Add New Premise - + {this.props.useFitchNotation && } + diff --git a/src/intro/IntroWindow.js b/src/intro/IntroWindow.js index ab6a416..f753128 100644 --- a/src/intro/IntroWindow.js +++ b/src/intro/IntroWindow.js @@ -1,6 +1,7 @@ import React from 'react'; import CreateNew from './CreateNew'; import { ReactSVG } from 'react-svg'; +import Switch from "react-switch"; import './intro.scss'; const IntroContent = ({ recentDocs }) => ( @@ -81,18 +82,35 @@ class IntroWindow extends React.Component { render() { const { createShown, floatingWindowCSS } = this.state; + const swi = ( + +
+ +
+ Fitch-Style Notation + + ); return (
{!createShown && } - {createShown && } + {createShown && + } {!createShown && (
- - + + + {swi}
)} {createShown && ( @@ -106,6 +124,7 @@ class IntroWindow extends React.Component { + {swi}
)} diff --git a/src/intro/intro.scss b/src/intro/intro.scss index 21488be..b1c538f 100644 --- a/src/intro/intro.scss +++ b/src/intro/intro.scss @@ -26,6 +26,7 @@ flex-direction: row-reverse; padding: 6px; padding-right: 20px; + align-items: center; .svg { display: inline-block; padding-right: 10px;