From 1676ce1c594e5f00dbc121d279a977aa0fc16d95 Mon Sep 17 00:00:00 2001 From: saksham Date: Sat, 11 Nov 2023 19:29:19 +0530 Subject: [PATCH] fix: use `premiseCount` to improve premise and conclusion insertion --- qt/DrawerTools.qml | 98 ++++++------- qt/GoalLine.qml | 90 +++++------- qt/KeyButton.qml | 12 +- qt/KeyGroup.qml | 61 ++++---- qt/ProofArea.qml | 354 +++++++++++++++++++++++---------------------- qt/main.qml | 214 +++++++++++++-------------- 6 files changed, 412 insertions(+), 417 deletions(-) diff --git a/qt/DrawerTools.qml b/qt/DrawerTools.qml index f58f271..aa27c48 100644 --- a/qt/DrawerTools.qml +++ b/qt/DrawerTools.qml @@ -1,3 +1,4 @@ + /* Drawer ToolBar Custom QML Type. Copyright (C) 2023 Saksham Attri. @@ -20,7 +21,7 @@ import QtQuick.Controls 2.5 import QtQuick.Layouts 1.3 import QtQuick.Dialogs -ToolBar{ +ToolBar { anchors.fill: parent @@ -30,39 +31,39 @@ ToolBar{ button: darkMode ? "#5C469C" : "white" } - ColumnLayout{ + ColumnLayout { - ToolButton{ + ToolButton { text: qsTr("New") icon.source: "assets/new.png" onClicked: { if (Qt.platform.os === "wasm") - Qt.openUrlExternally("https://matek.hu/zoltan/aris/"); + Qt.openUrlExternally("https://matek.hu/zoltan/aris/") else - auxConnector.newWindow(); + auxConnector.newWindow() } } - ToolButton{ + ToolButton { text: qsTr("Open") icon.source: "assets/folder.png" onClicked: { - cConnector.evalText = "Evaluate Proof"; + cConnector.evalText = "Evaluate Proof" - if (Qt.platform.os === "wasm"){ - isExtFile = true; - cConnector.wasmOpenProof(theData,theGoals); - } - else - fileDialogID.open(); + if (Qt.platform.os === "wasm") { + isExtFile = true + cConnector.wasmOpenProof(theData, theGoals) + computePremise = true + } else + fileDialogID.open() - menuOptions.close(); + menuOptions.close() } } - ToolButton{ + ToolButton { text: qsTr("Save") icon.source: "assets/save.png" visible: !(Qt.platform.os === "wasm") @@ -70,37 +71,36 @@ ToolBar{ onClicked: { if (fileExists) - cConnector.saveProof(filename,theData,theGoals); + cConnector.saveProof(filename, theData, theGoals) else - saveAsID.open(); + saveAsID.open() - menuOptions.close(); + menuOptions.close() } - } - ToolButton{ + ToolButton { text: qsTr("Save As") icon.source: "assets/saveas.png" onClicked: { if (Qt.platform.os === "wasm") - cConnector.wasmSaveProof(theData,theGoals); + cConnector.wasmSaveProof(theData, theGoals) else - saveAsID.open(); + saveAsID.open() - menuOptions.close(); + menuOptions.close() } } - ToolButton{ + ToolButton { text: qsTr("Export To LaTeX") icon.source: "assets/export.png" onClicked: { if (Qt.platform.os === "wasm") - auxConnector.wasmLatex(theData,cConnector); + auxConnector.wasmLatex(theData, cConnector) else latexID.open() @@ -108,11 +108,11 @@ ToolBar{ } } - ToolSeparator{ + ToolSeparator { orientation: Qt.Horizontal } - ToolButton{ + ToolButton { text: qsTr("Toggle Goals") icon.source: "assets/goal.png" @@ -122,63 +122,61 @@ ToolBar{ } } - ToolButton{ + ToolButton { text: qsTr("Toggle Dark Mode") icon.source: "assets/boolean.png" - onClicked: darkMode = !darkMode; - + onClicked: darkMode = !darkMode } - ToolButton{ + ToolButton { text: qsTr("Import Proof") icon.source: "assets/import.png" onClicked: { - cConnector.evalText = "Evaluate Proof"; - if (Qt.platform.os === "wasm"){ - isExtFile = true; - auxConnector.wasmImportProof(theData,cConnector,proofModel) - } - else + cConnector.evalText = "Evaluate Proof" + if (Qt.platform.os === "wasm") { + isExtFile = true + auxConnector.wasmImportProof(theData, cConnector, + proofModel) + computePremise = true + } else { importID.open() + } - menuOptions.close(); + menuOptions.close() } } - ToolSeparator{ + ToolSeparator { orientation: Qt.Horizontal } - ToolButton{ + ToolButton { text: qsTr("Font") icon.source: "assets/font.png" visible: !(Qt.platform.os === "wasm") onClicked: fontDialogID.open() - } - ToolSeparator{ + ToolSeparator { visible: !(Qt.platform.os === "wasm") orientation: Qt.Horizontal } - ToolButton{ + ToolButton { text: qsTr("Help") icon.source: "assets/help.png" - onClicked: Qt.openUrlExternally("https://www.gnu.org/software/aris/manual/aris.pdf") - + onClicked: Qt.openUrlExternally( + "https://www.gnu.org/software/aris/manual/aris.pdf") } - ToolButton{ + ToolButton { text: qsTr("About") icon.source: "assets/about.png" - onClicked: Qt.openUrlExternally("https://www.gnu.org/software/aris/") - + onClicked: Qt.openUrlExternally( + "https://www.gnu.org/software/aris/") } - } - } diff --git a/qt/GoalLine.qml b/qt/GoalLine.qml index f27ca60..527c8b4 100644 --- a/qt/GoalLine.qml +++ b/qt/GoalLine.qml @@ -1,3 +1,4 @@ + /* Goal Line Custom QML Type. Copyright (C) 2023 Saksham Attri. @@ -20,16 +21,18 @@ import QtQuick.Layouts 1.3 import QtQuick.Controls 2.5 import goal.model 1.0 +RowLayout { -RowLayout{ - - property string toolTipText: (resNumID.color === Qt.color("green"))? "Goal was met at line " + line : ((resNumID.color === Qt.color("blue")) ? "Goal was met at line "+ line+"\n\t but the proof has errors": ((resNumID.color === Qt.color("red"))?"Goal was not met": "Not yet evaluated")) //aaaaaaaaaaaaaaaaaaaaaaaaaaa + property string toolTipText: (resNumID.color === Qt.color( + "green")) ? "Goal was met at line " + + line : ((resNumID.color === Qt.color( + "blue")) ? "Goal was met at line " + line + "\n\t but the proof has errors" : ((resNumID.color === Qt.color("red")) ? "Goal was not met" : "Not yet evaluated")) //aaaaaaaaaaaaaaaaaaaaaaaaaaa spacing: 10 - width: (parent)? parent.width: 0 + width: (parent) ? parent.width : 0 Layout.fillWidth: true - Label{ + Label { id: goalLineNumID height: goalTextID @@ -38,32 +41,30 @@ RowLayout{ ToolTip.visible: toolTipText ? moID.containsMouse : false ToolTip.text: toolTipText - MouseArea{ + MouseArea { id: moID anchors.fill: parent hoverEnabled: true - onClicked: console.log(line); + onClicked: console.log(line) } - Text{ + Text { id: resNumID anchors.centerIn: parent font.italic: true - text: (line > 0) ? line: ((line === -3)? "X" : "?") - color: (text === "?")? (darkMode?"yellow":"brown"): ((text === "X") ? "red": ((model.valid)? "green": "blue")) - + text: (line > 0) ? line : ((line === -3) ? "X" : "?") + color: (text === "?") ? (darkMode ? "yellow" : "brown") : ((text === "X") ? "red" : ((model.valid) ? "green" : "blue")) } - } - TextField{ + TextField { id: goalTextID height: font.pointSize + 10 width: 200 Layout.fillWidth: true - background: Rectangle{ - color: darkMode?"#332940":"lightgrey" + background: Rectangle { + color: darkMode ? "#332940" : "lightgrey" } text: model.text @@ -73,70 +74,59 @@ RowLayout{ // Implementing Keyboard Macros onTextChanged: { - if (goalTextID.length >= 2){ - const last_two = text.slice(cursorPosition-2,cursorPosition) - if (last_two.includes('/\\')){ - goalTextID.remove(cursorPosition-2, cursorPosition) - goalTextID.insert(cursorPosition,"\u2227") - } - else if (last_two.includes('\\/')){ - goalTextID.remove(cursorPosition-2, cursorPosition) - goalTextID.insert(cursorPosition,"\u2228") - } - else if (last_two.includes('->')){ - goalTextID.remove(cursorPosition-2, cursorPosition) - goalTextID.insert(cursorPosition,"\u2192") - } - else if (last_two.includes('<'+"\u2192")){ - goalTextID.remove(cursorPosition-2, cursorPosition) - goalTextID.insert(cursorPosition,"\u2194") + if (goalTextID.length >= 2) { + const last_two = text.slice(cursorPosition - 2, cursorPosition) + if (last_two.includes('/\\')) { + goalTextID.remove(cursorPosition - 2, cursorPosition) + goalTextID.insert(cursorPosition, "\u2227") + } else if (last_two.includes('\\/')) { + goalTextID.remove(cursorPosition - 2, cursorPosition) + goalTextID.insert(cursorPosition, "\u2228") + } else if (last_two.includes('->')) { + goalTextID.remove(cursorPosition - 2, cursorPosition) + goalTextID.insert(cursorPosition, "\u2192") + } else if (last_two.includes('<' + "\u2192")) { + goalTextID.remove(cursorPosition - 2, cursorPosition) + goalTextID.insert(cursorPosition, "\u2194") } - } - } onEditingFinished: model.text = text - } - Button{ + Button { id: goalPlusID height: goalTextID.height onClicked: goalOptionsID.open() - Text{ + Text { anchors.centerIn: parent text: "+ / \u2013" - color: darkMode? "white": "black" + color: darkMode ? "white" : "black" } - Menu{ + Menu { id: goalOptionsID - Action{ + Action { text: "Add Goal" onTriggered: { - theGoals.insertgLine(index + 1,-2,false,""); + theGoals.insertgLine(index + 1, -2, false, "") } } - Action{ + Action { text: "Remove Goal" onTriggered: { - if (goalDataID.rowCount() > 1){ - theGoals.removegLineAt(index); - } - else + if (goalDataID.rowCount() > 1) { + theGoals.removegLineAt(index) + } else console.log("Invalid Operation: Cannot remove all Lines") } } - - } - } } - diff --git a/qt/KeyButton.qml b/qt/KeyButton.qml index a2e91d8..d818cdf 100644 --- a/qt/KeyButton.qml +++ b/qt/KeyButton.qml @@ -1,3 +1,4 @@ + /* Buttons associated with on-screen keyboard. Copyright (C) 2023 Saksham Attri. @@ -18,7 +19,7 @@ import QtQuick 2.15 import QtQuick.Controls 2.5 -ToolButton{ +ToolButton { property string txt: "Symbol" @@ -28,21 +29,18 @@ ToolButton{ ToolTip.visible: hovered ToolTip.text: "Operation Name" - focusPolicy: Qt.NoFocus // Text is passed to focused TextArea, so the button musn't steal focus + focusPolicy: Qt.NoFocus // Text is passed to focused TextArea, so the button musn't steal focus onClicked: { if (isTextField(activeFocusItem)) activeFocusItem.insert(activeFocusItem.cursorPosition, txt) - } - Text{ + Text { text: txt font: thefont - color: darkMode? "#BB86FC" : "black" + color: darkMode ? "#BB86FC" : "black" anchors.centerIn: parent fontSizeMode: Text.HorizontalFit } - } - diff --git a/qt/KeyGroup.qml b/qt/KeyGroup.qml index acf2877..ece9acf 100644 --- a/qt/KeyGroup.qml +++ b/qt/KeyGroup.qml @@ -1,3 +1,4 @@ + /* Container for the on-screen keyboard buttons. Copyright (C) 2023 Saksham Attri. @@ -18,131 +19,121 @@ import QtQuick 2.15 import QtQuick.Controls 2.5 -ToolBar{ +ToolBar { spacing: 5 - background: Rectangle{ + background: Rectangle { anchors.fill: parent - color: darkMode? "#121212":"white" + color: darkMode ? "#121212" : "white" } - Column{ + Column { id: keyColID - KeyButton{ + KeyButton { id: conjunctionButton - txt: "\u2227" ToolTip.text: "Conjunction" } - KeyButton{ + KeyButton { id: disjunctionButton - txt: "\u2228" ToolTip.text: "Disjunction" } - KeyButton{ + KeyButton { id: negationButton - txt: "\u00ac" ToolTip.text: "Negation" } - KeyButton{ + KeyButton { id: implicationButton - txt: "\u2192" ToolTip.text: "Implication" } - KeyButton{ + KeyButton { id: biconditionalButton txt: "\u2194" ToolTip.text: "Bi-conditional" } - KeyButton{ + KeyButton { id: forAllButton txt: "\u2200" ToolTip.text: "For all" } - KeyButton{ + KeyButton { id: thereExistsButton - txt: "\u2203" ToolTip.text: "There exists" } - KeyButton{ + KeyButton { id: tautologyButton - txt: "\u22a4" ToolTip.text: "Tautology" } - KeyButton{ + KeyButton { id: contradictionButton - txt: "\u22a5" ToolTip.text: "Contradiction" } - KeyButton{ + KeyButton { id: belongsToButton - txt: "\u2208" ToolTip.text: "Belongs To" } - KeyButton{ + KeyButton { id: nullButton - - txt: "\u2205" ToolTip.text: "Null" } - ToolSeparator{ + ToolSeparator { orientation: Qt.Horizontal } // Evaluate Proof Button - - ToolButton{ + ToolButton { id: evalButton icon { source: "assets/eval.png" - height: (Qt.platform.os === "wasm") ? nullButton.height/1.5 : nullButton.height/2 - width: (Qt.platform.os === "wasm") ? nullButton.width/1.5 : nullButton.width/2 + height: (Qt.platform.os === "wasm") ? nullButton.height + / 1.5 : nullButton.height / 2 + width: (Qt.platform.os === "wasm") ? nullButton.width / 1.5 : nullButton.width / 2 } hoverEnabled: true ToolTip.visible: hovered ToolTip.text: cConnector.evalText - background: Rectangle{ + background: Rectangle { id: runButtonID - color: (cConnector.evalText === "Evaluate Proof")? (darkMode?"#BB86FC":"white"): (cConnector.evalText === "Correct!")? (darkMode?"springgreen":"green"): "red" + color: (cConnector.evalText === "Evaluate Proof") ? (darkMode ? "#BB86FC" : "white") : (cConnector.evalText === "Correct!") ? (darkMode ? "springgreen" : "green") : "red" radius: 5 } onClicked: { - cConnector.evalProof(theData,theGoals); - goalDataID.evalGoals(theGoals,cConnector); - animationID.start(); + cConnector.evalProof(theData, theGoals) + goalDataID.evalGoals(theGoals, cConnector) + animationID.start() } SequentialAnimation { diff --git a/qt/ProofArea.qml b/qt/ProofArea.qml index adbdf8c..006ea5f 100644 --- a/qt/ProofArea.qml +++ b/qt/ProofArea.qml @@ -1,3 +1,4 @@ + /* The proof area containing textfields, labels, rule combo boxes etc. Copyright (C) 2023 Saksham Attri. @@ -22,26 +23,20 @@ import proof.model 1.0 Item { - property var combo2: [ - ["Modus Ponens", "Addition", "Simplification", "Conjunction", "Hypothetical Syllogism", "Disjunctive Syllogism", "Excluded middle", "Constructive Dilemma"], - ["Implication", "DeMorgan", "Association", "Commutativity", "Idempotence","Distribution","Equivalence","Double Negation", "Exportation", "Subsumption"], - ["Universal Generalization", "Universal Instantiation", "Existential Generalization", "Existential Instantiation", "Bound Variable Substitution", "Null Quantifier", "Prenex", "Identity", "Free Variable Substitution"], - ["Lemma","Subproof","Sequence","Induction"], - ["Identity ","Negation","Dominance","Symbol Negation"] - ] + property var combo2: [["Modus Ponens", "Addition", "Simplification", "Conjunction", "Hypothetical Syllogism", "Disjunctive Syllogism", "Excluded middle", "Constructive Dilemma"], ["Implication", "DeMorgan", "Association", "Commutativity", "Idempotence", "Distribution", "Equivalence", "Double Negation", "Exportation", "Subsumption"], ["Universal Generalization", "Universal Instantiation", "Existential Generalization", "Existential Instantiation", "Bound Variable Substitution", "Null Quantifier", "Prenex", "Identity", "Free Variable Substitution"], ["Lemma", "Subproof", "Sequence", "Induction"], ["Identity ", "Negation", "Dominance", "Symbol Negation"]] anchors.fill: parent - ColumnLayout{ + ColumnLayout { id: proofAreaID - anchors{ + anchors { fill: parent leftMargin: keyboardID.width + 20 topMargin: 20 rightMargin: 20 } - ListView{ + ListView { id: listView model: proofModel @@ -53,176 +48,189 @@ Item { Layout.fillWidth: true Layout.fillHeight: true spacing: 10 - ScrollBar.vertical: ScrollBar{} + ScrollBar.vertical: ScrollBar {} onCurrentItemChanged: { if (currentItem) currentItem.children[1].forceActiveFocus() } - - } - } - Component{ + Component { id: proofLineID - - RowLayout{ + RowLayout { id: root_delegate - property bool editCombos: (!isExtFile || type === "choose"); - property var arr: model.refs; - property string type: model.type; - property int indexx: model.index; - property bool vis: type === "premise" || type === "subproof" || type === "sf"; - property string textFieldColor: (listView.currentIndex !== -1)?(proofModel.data(proofModel.index(listView.currentIndex,0),263).includes(model.line) ? (darkMode?"brown":"yellow") : (darkMode ? "#1F1A24":"white")):(darkMode?"#332940":"lightgrey"); + property bool editCombos: (!isExtFile || type === "choose") + property var arr: model.refs + property string type: model.type + property int indexx: model.index + property bool vis: type === "premise" || type === "subproof" + || type === "sf" + property string textFieldColor: (listView.currentIndex + !== -1) ? (proofModel.data( + proofModel.index( + listView.currentIndex, + 0), + 263).includes( + model.line) ? (darkMode ? "brown" : "yellow") : (darkMode ? "#1F1A24" : "white")) : (darkMode ? "#332940" : "lightgrey") // Function to refresh the line color after selecting/de-selecting references - function refreshTextFieldColor(){ - var temp = listView.currentIndex; - listView.currentIndex = -1; - listView.currentIndex = temp; + function refreshTextFieldColor() { + var temp = listView.currentIndex + listView.currentIndex = -1 + listView.currentIndex = temp } spacing: 10 - width: (parent)? parent.width: 0 + width: (parent) ? parent.width : 0 Layout.fillWidth: true // Line Number Button - Button{ + Button { id: lineNumberID height: theTextID.height width: height palette { - button: darkMode? "#1F1A24" : "white" + button: darkMode ? "#1F1A24" : "white" } - Text{ + Text { anchors.centerIn: parent font.italic: true text: model.line color: theTextID.color } - // Add this button's line to the current line's references onClicked: { if (listView.currentIndex <= index) - console.log("Invalid Operation : Can only reference to smaller line numbers"); - else if (proofModel.data(proofModel.index(listView.currentIndex,0),257) === "premise") - console.log("Invalid Operation: Current Line is a premise"); - else if (proofModel.data(proofModel.index(listView.currentIndex,0),260) === true )//|| proofModel.data(proofModel.index(listView.currentIndex,0),261) === true) - console.log("Invalid Operation: Subproof beginning"); - else if (proofModel.data(proofModel.index(listView.currentIndex,0),262) < model.ind && proofModel.data(proofModel.index(listView.currentIndex,0),261) === false) - console.log("Invalid Operation: Invalid reference to subproof"); - else{ - cConnector.evalText = "Evaluate Proof"; - var array = Array.from(proofModel.data(proofModel.index(listView.currentIndex,0),263)); - for(var i = 0; i < array.length; i++){ - if (array[i] === model.line){ - array.splice(i,1); - proofModel.setData(proofModel.index(listView.currentIndex,0),array,263); - refreshTextFieldColor(); - return; + console.log("Invalid Operation : Can only reference to smaller line numbers") + else if (proofModel.data(proofModel.index( + listView.currentIndex, 0), + 257) === "premise") + console.log("Invalid Operation: Current Line is a premise") + else if (proofModel.data(proofModel.index( + listView.currentIndex, 0), + 260) === true) + //|| proofModel.data(proofModel.index(listView.currentIndex,0),261) === true) + console.log("Invalid Operation: Subproof beginning") + else if (proofModel.data( + proofModel.index(listView.currentIndex, 0), + 262) < model.ind && proofModel.data( + proofModel.index(listView.currentIndex, 0), + 261) === false) + console.log("Invalid Operation: Invalid reference to subproof") + else { + cConnector.evalText = "Evaluate Proof" + var array = Array.from(proofModel.data( + proofModel.index( + listView.currentIndex, + 0), 263)) + for (var i = 0; i < array.length; i++) { + if (array[i] === model.line) { + array.splice(i, 1) + proofModel.setData(proofModel.index( + listView.currentIndex, + 0), array, 263) + refreshTextFieldColor() + return } } - array.push(model.line); - proofModel.setData(proofModel.index(listView.currentIndex,0),array,263); - refreshTextFieldColor(); + array.push(model.line) + proofModel.setData(proofModel.index( + listView.currentIndex, 0), + array, 263) + refreshTextFieldColor() } } } // The Typing Area - TextField{ + TextField { id: theTextID - color: darkMode? "white": "black" + color: darkMode ? "white" : "black" height: font.pointSize + 10 Layout.leftMargin: model.ind Layout.fillWidth: true - background: Rectangle{ + background: Rectangle { id: backRectID border.width: 1 - border.color: ((cConnector.evalText).includes("Error in line "+(indexx+1)+" -") && cConnector.evalText !== "Evaluate Proof")? "red" : (cConnector.evalText === "Evaluate Proof") ? ( darkMode ? "white":"black") : "springgreen" + border.color: ((cConnector.evalText).includes( + "Error in line " + (indexx + 1) + " -") + && cConnector.evalText !== "Evaluate Proof") ? "red" : (cConnector.evalText === "Evaluate Proof") ? (darkMode ? "white" : "black") : "springgreen" color: textFieldColor } //placeholderText: indexx === 0 ? qsTr("Start Typing here..."): "" text: model.lText - MouseArea{ + MouseArea { anchors.fill: parent //propagateComposedEvents: true onClicked: { - listView.currentIndex = index; - parent.forceActiveFocus(); - parent.cursorPosition = parent.positionAt(mouseX, mouseY); + listView.currentIndex = index + parent.forceActiveFocus() + parent.cursorPosition = parent.positionAt(mouseX, + mouseY) } } // Click the +/- button on pressing Enter onAccepted: plusID.clicked() - // Implementation for Keyboard Macros onTextChanged: { - // TODO: Improve implementation later - if (theTextID.length >= 2){ - const last_two = text.slice(cursorPosition-2,cursorPosition) - if (last_two.includes('/\\')){ - theTextID.remove(cursorPosition-2, cursorPosition) - theTextID.insert(cursorPosition,"\u2227") - } - else if (last_two.includes('\\/')){ - theTextID.remove(cursorPosition-2, cursorPosition) - theTextID.insert(cursorPosition,"\u2228") - } - else if (last_two.includes('->')){ - theTextID.remove(cursorPosition-2, cursorPosition) - theTextID.insert(cursorPosition,"\u2192") - } - else if (last_two.includes('<'+"\u2192")){ - theTextID.remove(cursorPosition-2, cursorPosition) - theTextID.insert(cursorPosition,"\u2194") + // TODO: Improve implementation later + if (theTextID.length >= 2) { + const last_two = text.slice(cursorPosition - 2, + cursorPosition) + if (last_two.includes('/\\')) { + theTextID.remove(cursorPosition - 2, cursorPosition) + theTextID.insert(cursorPosition, "\u2227") + } else if (last_two.includes('\\/')) { + theTextID.remove(cursorPosition - 2, cursorPosition) + theTextID.insert(cursorPosition, "\u2228") + } else if (last_two.includes('->')) { + theTextID.remove(cursorPosition - 2, cursorPosition) + theTextID.insert(cursorPosition, "\u2192") + } else if (last_two.includes('<' + "\u2192")) { + theTextID.remove(cursorPosition - 2, cursorPosition) + theTextID.insert(cursorPosition, "\u2194") } - } } // Save Text inside Model - onEditingFinished: model.lText = text; - + onEditingFinished: model.lText = text } // Label for premise, subproofs - Label{ + Label { id: ruleID height: theTextID.height width: 50 visible: vis - Text{ + Text { anchors.centerIn: parent font.italic: true text: model.type color: darkMode ? "white" : "black" opacity: darkMode ? 0.87 : 1 } - - - } // First ComboBox to select rule - ComboBox{ + ComboBox { id: chooseID palette { @@ -231,38 +239,36 @@ Item { window: darkMode ? "#CF6679" : "white" } - - visible: !vis height: theTextID.height onActivated: { - editCombos = true; - proofModel.setData(proofModel.index(indexx,0),conclusionRuleID.currentText,258) - asteriskID.visible = false; + editCombos = true + proofModel.setData(proofModel.index(indexx, 0), + conclusionRuleID.currentText, 258) + asteriskID.visible = false } - model:["Inference", "Equivalence", "Predicate", "Miscellaneous", "Boolean"] + model: ["Inference", "Equivalence", "Predicate", "Miscellaneous", "Boolean"] Component.onCompleted: { - if (!editCombos){ + if (!editCombos) { if (combo2[0].includes(type)) - currentIndex = 0; + currentIndex = 0 else if (combo2[1].includes(type)) - currentIndex = 1; + currentIndex = 1 else if (combo2[2].includes(type)) - currentIndex = 2; + currentIndex = 2 else if (combo2[3].includes(type)) - currentIndex = 3; + currentIndex = 3 else - currentIndex = 4; + currentIndex = 4 } } - } // Second ComboBox to select rule - ComboBox{ + ComboBox { id: conclusionRuleID palette { @@ -280,24 +286,23 @@ Item { ToolTip.text: currentText onActivated: { - editCombos = true; - proofModel.setData(proofModel.index(indexx,0),currentText,258) - asteriskID.visible = false; + editCombos = true + proofModel.setData(proofModel.index(indexx, 0), + currentText, 258) + asteriskID.visible = false } onModelChanged: { - if (!editCombos){ - currentIndex = model.indexOf(type); + if (!editCombos) { + currentIndex = model.indexOf(type) } } - model: combo2[chooseID.currentIndex] - + model: combo2[chooseID.currentIndex] } - // Display Asterisk next to ComboBox if rule not chosen - Label{ + Label { id: asteriskID property string toolTipText: "Rule Not Chosen" @@ -312,159 +317,168 @@ Item { ToolTip.visible: toolTipText ? mID.containsMouse : false ToolTip.text: toolTipText - MouseArea{ + MouseArea { id: mID anchors.fill: parent hoverEnabled: true } } - // Row of references - Row{ + Row { id: refID - Repeater{ + Repeater { id: repID model: arr onModelChanged: { - root_delegate.refreshTextFieldColor(); + root_delegate.refreshTextFieldColor() } - Button{ - visible: (modelData === -1)? false: true + Button { + visible: (modelData === -1) ? false : true palette { - button: darkMode? "#1F1A24" : "white" + button: darkMode ? "#1F1A24" : "white" } onClicked: { var ar = Array.from(arr) - ar.splice(index,1) - var ok = parent.parent.parent; - proofModel.setData(proofModel.index(listView.currentIndex,0),ar,263); - cConnector.evalText = "Evaluate Proof"; + ar.splice(index, 1) + var ok = parent.parent.parent + proofModel.setData(proofModel.index( + listView.currentIndex, + 0), ar, 263) + cConnector.evalText = "Evaluate Proof" } - Text{ + Text { anchors.centerIn: parent font.italic: true text: modelData - color: darkMode?"white":"black" + color: darkMode ? "white" : "black" } - } - - } - } - // The +/- Button - Button{ + Button { id: plusID height: theTextID.height palette { - button: darkMode? "#1F1A24" : "white" + button: darkMode ? "#1F1A24" : "white" } onClicked: { + if (computePremise) { + computePremiseCount(listView) + computePremise = false + } optionsID.open() } - Text{ + Text { anchors.centerIn: parent text: "+ / \u2013" color: theTextID.color } - Menu{ + Menu { id: optionsID palette { - base: darkMode? "#1F1A24" : "white" - text: darkMode? "white" : "black" + base: darkMode ? "#1F1A24" : "white" + text: darkMode ? "white" : "black" } - Action{ + Action { text: "Add Premise" onTriggered: { - theData.insertLine(0,1,"","premise",false,false,false,0,[-1]) - proofModel.updateLines(); - proofModel.updateRefs(0,true); - listView.currentIndex = 0; - cConnector.evalText = "Evaluate Proof"; + var insertIndex = (index < premiseCount) ? index + 1 : premiseCount + theData.insertLine(insertIndex, insertIndex + 1, + "", "premise", false, false, + false, 0, [-1]) + proofModel.updateLines() + proofModel.updateRefs(insertIndex, true) + listView.currentIndex = insertIndex + cConnector.evalText = "Evaluate Proof" + premiseCount = premiseCount + 1 } } - Action{ + Action { text: "Add Conclusion" + enabled: index + 1 >= premiseCount + onTriggered: { - theData.insertLine(index + 1,index+2,"","choose",model.sub,false,false,model.ind,[-1]); - proofModel.updateLines(); - proofModel.updateRefs(index+1,true); - listView.currentIndex = index + 1; - cConnector.evalText = "Evaluate Proof"; + theData.insertLine(index + 1, index + 2, "", + "choose", model.sub, false, + false, model.ind, [-1]) + proofModel.updateLines() + proofModel.updateRefs(index + 1, true) + listView.currentIndex = index + 1 + cConnector.evalText = "Evaluate Proof" } } - Action{ + Action { text: "Start Subproof" - onTriggered:{ - theData.insertLine(index + 1,index+2,"","sf",true,true,false,model.ind + 20,[-1]); - proofModel.updateLines(); - proofModel.updateRefs(index+1,true); - listView.currentIndex = index + 1; - cConnector.evalText = "Evaluate Proof"; + onTriggered: { + theData.insertLine(index + 1, index + 2, "", "sf", + true, true, false, + model.ind + 20, [-1]) + proofModel.updateLines() + proofModel.updateRefs(index + 1, true) + listView.currentIndex = index + 1 + cConnector.evalText = "Evaluate Proof" } } - Action{ + Action { text: "End Subproof" enabled: model.sub onTriggered: { - theData.insertLine(index + 1,index+2,"","subproof",(model.ind >= 20)? true: false,false,true,model.ind -20,[-1]); - proofModel.updateLines(); - proofModel.updateRefs(index+1,true); - listView.currentIndex = index + 1; - cConnector.evalText = "Evaluate Proof"; - + theData.insertLine( + index + 1, index + 2, "", "subproof", + (model.ind >= 20) ? true : false, + false, true, model.ind - 20, [-1]) + proofModel.updateLines() + proofModel.updateRefs(index + 1, true) + listView.currentIndex = index + 1 + cConnector.evalText = "Evaluate Proof" } } - Action{ + Action { text: "Remove this Line" enabled: (index !== 0) onTriggered: { - var i = index; + var i = index theData.removeLineAt(index) proofModel.updateLines() - proofModel.updateRefs(i,false); - cConnector.evalText = "Evaluate Proof"; - + proofModel.updateRefs(i, false) + cConnector.evalText = "Evaluate Proof" } } } } - } } // Background to highlight current line - Component{ + Component { id: highlightID - Rectangle{ + Rectangle { width: (parent) ? parent.width : 0 color: darkMode ? "#3700B3" : "lightblue" radius: 10 } } - } diff --git a/qt/main.qml b/qt/main.qml index 841a1a4..f19908a 100644 --- a/qt/main.qml +++ b/qt/main.qml @@ -1,3 +1,4 @@ + /* The main window. Copyright (C) 2023 Saksham Attri. @@ -27,49 +28,64 @@ ApplicationWindow { id: rootID property font thefont: rootID.font - property bool isExtFile: false // If the file is opened from an external file + property bool isExtFile: false // If the file is opened from an external file property bool darkMode: false property string filename: "Untitled" property bool fileExists: isExtFile -// property bool closing: false + property int premiseCount: 1 + property bool computePremise: false // set to true if Open or Import Proof are used + // property bool closing: false + + // Function to compute premiseCount, used when opening new file + function computePremiseCount(item) { + premiseCount = 0 + for (var child in item.contentItem.children) { + if (item.contentItem.children[child].type === "premise") + premiseCount++ + // else if (item.contentItem.children[child].type !== "undefined") + // break + } + } // Function to check if the item is a TextField QML Type - function isTextField(item){ + function isTextField(item) { return item instanceof TextField } width: 1200 height: 700 visible: true - title: qsTr(filename.slice(filename.lastIndexOf("/")+ 1) + " | " + "GNU Aris") + title: qsTr(filename.slice(filename.lastIndexOf( + "/") + 1) + " | " + "GNU Aris") font: thefont - color: darkMode ? "#121212": "white" + color: darkMode ? "#121212" : "white" // Footer to display error messages - footer: Label{ + footer: Label { height: statusID.implicitHeight - visible: !(cConnector.evalText === "Correct!" || cConnector.evalText === "Evaluate Proof") + visible: !(cConnector.evalText === "Correct!" + || cConnector.evalText === "Evaluate Proof") - Text{ + Text { id: statusID text: cConnector.evalText color: darkMode ? "#CF6679" : "red" } } -// onClosing: function(close){ -// close.accepted = closing; -// onTriggered: if(!closing) exitMessageID.open(); -// } + // onClosing: function(close){ + // close.accepted = closing; + // onTriggered: if(!closing) exitMessageID.open(); + // } // Burger Button - Button{ + Button { id: burgerMenu height: keyboardID.width width: keyboardID.width - palette{ - button: darkMode? "#121212": "white" + palette { + button: darkMode ? "#121212" : "white" } hoverEnabled: true @@ -78,41 +94,38 @@ ApplicationWindow { onClicked: menuOptions.open() - - Text{ + Text { anchors.centerIn: parent - color: darkMode? "#BB86FC": "black" + color: darkMode ? "#BB86FC" : "black" text: "\u2630" minimumPointSize: 20 } - } // On-Screen Keyboard - Frame{ + Frame { id: keyboardID anchors.verticalCenter: parent.verticalCenter - KeyGroup{} + KeyGroup {} } // Drawer associated with the Burger Button - Drawer{ + Drawer { id: menuOptions width: drawerToolBar.implicitWidth height: rootID.height interactive: true - DrawerTools{ + DrawerTools { id: drawerToolBar } } // Dialogs associated with the DrawerTools - - FileDialog{ + FileDialog { id: fileDialogID title: "Choose the proof file" @@ -121,14 +134,14 @@ ApplicationWindow { fileMode: FileDialog.OpenFile defaultSuffix: "tle" onAccepted: { - cConnector.openProof(selectedFile,theData,theGoals); - filename = selectedFile; - isExtFile = true; + cConnector.openProof(selectedFile, theData, theGoals) + filename = selectedFile + isExtFile = true + computePremise = true } - } - FileDialog{ + FileDialog { id: saveAsID nameFilters: ["Aris files (*.tle)"] @@ -136,25 +149,23 @@ ApplicationWindow { fileMode: FileDialog.SaveFile defaultSuffix: "tle" onAccepted: { - cConnector.saveProof(selectedFile,theData,theGoals); - filename = selectedFile; - fileExists = true; + cConnector.saveProof(selectedFile, theData, theGoals) + filename = selectedFile + fileExists = true } - } - FileDialog{ + FileDialog { id: latexID nameFilters: ["Latex files (*.tex)"] title: "Save As" fileMode: FileDialog.SaveFile defaultSuffix: "tex" - onAccepted: auxConnector.latex(selectedFile,theData,cConnector) - + onAccepted: auxConnector.latex(selectedFile, theData, cConnector) } - FileDialog{ + FileDialog { id: importID nameFilters: ["Aris files (*.tle)"] @@ -162,118 +173,111 @@ ApplicationWindow { fileMode: FileDialog.OpenFile defaultSuffix: "tle" onAccepted: { - isExtFile = true; - auxConnector.importProof(selectedFile,theData,cConnector,proofModel); + isExtFile = true + computePremise = true + auxConnector.importProof(selectedFile, theData, cConnector, + proofModel) } } - FontDialog{ + FontDialog { id: fontDialogID title: "Choose Font" - onAccepted: thefont = currentFont; - + onAccepted: thefont = currentFont } - Dialog{ + Dialog { id: goalDialogID title: "Goals" - width: parent.width/2 - height: parent.height/2 - x: (parent.width - width)/2 - y: (parent.height - height)/2 + width: parent.width / 2 + height: parent.height / 2 + x: (parent.width - width) / 2 + y: (parent.height - height) / 2 - background: Rectangle{ + background: Rectangle { anchors.fill: parent - color: darkMode? "#1F1B24": "white" - opacity: 1//0.6 + color: darkMode ? "#1F1B24" : "white" + opacity: 1 //0.6 border.width: 2 } palette { - button: darkMode? "#1F1A24" : "white" - buttonText: darkMode? "white": "black" - text: darkMode? "white": "black" - window: darkMode? "#1F1B24": "white" + button: darkMode ? "#1F1A24" : "white" + buttonText: darkMode ? "white" : "black" + text: darkMode ? "white" : "black" + window: darkMode ? "#1F1B24" : "white" } parent: Overlay.overlay focus: true //modal: true - closePolicy: Popup.CloseOnEscape // To allow keyboard access + closePolicy: Popup.CloseOnEscape // To allow keyboard access standardButtons: Dialog.Ok - ColumnLayout{ + ColumnLayout { id: goalAreaID anchors.fill: parent - ListView{ + ListView { model: goalDataID - delegate: GoalLine{} + delegate: GoalLine {} Layout.fillWidth: true Layout.fillHeight: true spacing: 10 - ScrollBar.vertical: ScrollBar{} + ScrollBar.vertical: ScrollBar {} } - } - } // Message Dialog when Closing App -// Dialog{ -// id: exitMessageID - -// title: "The document was modified" -// x: (parent.width - width)/2 -// y: (parent.height - height)/2 - - -// parent: Overlay.overlay -// focus: true -// modal: true -// closePolicy: Popup.CloseOnEscape - -// standardButtons: MessageDialog.Save | MessageDialog.Discard -// onAccepted: { -// if (Qt.platform.os === "wasm") -// cConnector.wasmSaveProof(theData,theGoals); -// else -// saveAsID.open(); - -// closing = true; -// } -// onDiscarded: { -// closing = true; -// rootID.close(); -// } - -// Text{ -// text: "Do you want to save the file" -// } - -// } - - GoalModel{ + // Dialog{ + // id: exitMessageID + + // title: "The document was modified" + // x: (parent.width - width)/2 + // y: (parent.height - height)/2 + + // parent: Overlay.overlay + // focus: true + // modal: true + // closePolicy: Popup.CloseOnEscape + + // standardButtons: MessageDialog.Save | MessageDialog.Discard + // onAccepted: { + // if (Qt.platform.os === "wasm") + // cConnector.wasmSaveProof(theData,theGoals); + // else + // saveAsID.open(); + + // closing = true; + // } + // onDiscarded: { + // closing = true; + // rootID.close(); + // } + + // Text{ + // text: "Do you want to save the file" + // } + + // } + GoalModel { id: goalDataID glines: theGoals } - ProofModel{ + ProofModel { id: proofModel lines: theData } - ProofArea{} - -} - -// TODO: -// 1) Implement premiseIndex to keep track of latest premise and enter any new premise after it -// 2) Dark Mode for Drawer -// 3) Closing App on Desktop + ProofArea { + id: proofID + } +} // TODO:// 1) Dark Mode for Drawer// 2) Closing App on Desktop