Skip to content

Commit 8625199

Browse files
kovzolkovzol
authored
Merge pull request #65 from khush3e/master
 Core Engine Cleanup, Locale-Invariant Rule Selection, and UI Error Surfacing
2 parents 1721113 + bd46f86 commit 8625199

26 files changed

Lines changed: 487 additions & 187 deletions

‎.gitignore‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -22,3 +22,7 @@ doc/aris/*.html
2222
doc/aris.info
2323
doc/stamp-vti
2424
doc/version.texi
25+
26+
# Personal editor config
27+
.vscode/
28+
.DS_Store

‎qt/DrawerTools.qml‎

Lines changed: 5 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -66,7 +66,6 @@ ToolBar {
6666
if (Qt.platform.os === "wasm") {
6767
isExtFile = true
6868
cConnector.wasmOpenProof(theData, theGoals)
69-
computePremise = true
7069
} else
7170
fileDialogID.open()
7271

@@ -296,23 +295,23 @@ ToolBar {
296295

297296
MenuItem {
298297
text: "English"
299-
onTriggered: settings.setLanguage("en")
298+
onTriggered: { settings.setLanguage("en"); appPrefs.language = "en" }
300299
}
301300
MenuItem {
302301
text: "العربية"
303-
onTriggered: settings.setLanguage("ar")
302+
onTriggered: { settings.setLanguage("ar"); appPrefs.language = "ar" }
304303
}
305304
MenuItem {
306305
text: "Deutsch"
307-
onTriggered: settings.setLanguage("de")
306+
onTriggered: { settings.setLanguage("de"); appPrefs.language = "de" }
308307
}
309308
MenuItem {
310309
text: "Français"
311-
onTriggered: settings.setLanguage("fr")
310+
onTriggered: { settings.setLanguage("fr"); appPrefs.language = "fr" }
312311
}
313312
MenuItem {
314313
text: "Magyar"
315-
onTriggered: settings.setLanguage("hu")
314+
onTriggered: { settings.setLanguage("hu"); appPrefs.language = "hu" }
316315
}
317316
}
318317
}

‎qt/GoalLine.qml‎

Lines changed: 11 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -92,7 +92,12 @@ RowLayout {
9292
}
9393
}
9494

95-
onEditingFinished: model.text = text
95+
onTextEdited: fileModified = true
96+
97+
onEditingFinished: {
98+
if (model.text !== text) fileModified = true
99+
model.text = text
100+
}
96101
}
97102

98103
Button {
@@ -115,6 +120,7 @@ RowLayout {
115120
text: "Add Goal"
116121
onTriggered: {
117122
theGoals.insertgLine(index + 1, -2, false, "")
123+
fileModified = true
118124
}
119125
}
120126

@@ -123,8 +129,11 @@ RowLayout {
123129
onTriggered: {
124130
if (goalDataID.rowCount() > 1) {
125131
theGoals.removegLineAt(index)
126-
} else
132+
fileModified = true
133+
} else {
127134
console.log("Invalid Operation: Cannot remove all Lines")
135+
cConnector.evalText = "⚠ " + qsTr("Invalid Operation: At least one goal line must remain.")
136+
}
128137
}
129138
}
130139
}

‎qt/ProofArea.qml‎

Lines changed: 95 additions & 54 deletions
Original file line numberDiff line numberDiff line change
@@ -54,14 +54,14 @@ Item {
5454
proofModel.updateLines()
5555
proofModel.updateRefs(myIdx, false)
5656

57-
// After removal the boundary shifts to premiseCount - 1.
58-
var insertAt = proofModel.premiseCount - 1
57+
// After removal, recomputePremiseCount has already fired and premiseCount
58+
// is now P-1. The insert boundary (first conclusion slot) is exactly premiseCount.
59+
var insertAt = proofModel.premiseCount
5960
theData.insertLine(insertAt, insertAt + 1, pText, "choose",
6061
pSub, pSubSt, pSubEnd, pInd, [-1])
6162
proofModel.updateLines()
6263
proofModel.updateRefs(insertAt, true)
6364
listView.currentIndex = insertAt
64-
proofModel.premiseCount = proofModel.premiseCount - 1
6565

6666
fileModified = true
6767
cConnector.evalText = "Evaluate Proof"
@@ -83,20 +83,41 @@ Item {
8383
proofModel.updateLines()
8484
proofModel.updateRefs(insertAt2, true)
8585
listView.currentIndex = insertAt2
86-
proofModel.premiseCount = proofModel.premiseCount + 1
8786

8887
fileModified = true
8988
cConnector.evalText = "Evaluate Proof"
9089
proofModel.clearErrors()
9190
}
9291

93-
property var combo2: [
94-
[qsTr("Modus Ponens"), qsTr("Addition"), qsTr("Simplification"), qsTr("Conjunction"), qsTr("Hypothetical Syllogism"), qsTr("Disjunctive Syllogism"), qsTr("Excluded middle"), qsTr("Constructive Dilemma"), qsTr("XOR Introduction"), qsTr("XOR Elimination")],
95-
[qsTr("Implication"), qsTr("DeMorgan"), qsTr("Association"), qsTr("Commutativity"), qsTr("Idempotence"), qsTr("Distribution"), qsTr("Equivalence"), qsTr("Double Negation"), qsTr("Exportation"), qsTr("Subsumption"), qsTr("Contrapositive")],
96-
[qsTr("Universal Generalization"), qsTr("Universal Instantiation"), qsTr("Existential Generalization"), qsTr("Existential Instantiation"), qsTr("Bound Variable Substitution"), qsTr("Null Quantifier"), qsTr("Prenex"), qsTr("Identity"), qsTr("Free Variable Substitution")],
97-
[qsTr("Lemma"), qsTr("Subproof"), qsTr("Sequence"), qsTr("Induction")],
98-
[qsTr("Identity "), qsTr("Negation"), qsTr("Dominance"), qsTr("Symbol Negation")]
99-
]
92+
property var chooseCategories: getChooseCategories()
93+
property var combo2: getCombo2()
94+
95+
function getChooseCategories() {
96+
return [qsTr("Inference"), qsTr("Equivalence"), qsTr("Predicate"), qsTr("Miscellaneous"), qsTr("Boolean")]
97+
}
98+
99+
function getCombo2() {
100+
return [
101+
[qsTr("Modus Ponens"), qsTr("Addition"), qsTr("Simplification"), qsTr("Conjunction"), qsTr("Hypothetical Syllogism"), qsTr("Disjunctive Syllogism"), qsTr("Excluded middle"), qsTr("Constructive Dilemma"), qsTr("XOR Introduction"), qsTr("XOR Elimination")],
102+
[qsTr("Implication"), qsTr("DeMorgan"), qsTr("Association"), qsTr("Commutativity"), qsTr("Idempotence"), qsTr("Distribution"), qsTr("Equivalence"), qsTr("Double Negation"), qsTr("Exportation"), qsTr("Subsumption"), qsTr("Contrapositive")],
103+
[qsTr("Universal Generalization"), qsTr("Universal Instantiation"), qsTr("Existential Generalization"), qsTr("Existential Instantiation"), qsTr("Bound Variable Substitution"), qsTr("Null Quantifier"), qsTr("Prenex"), qsTr("Identity"), qsTr("Free Variable Substitution")],
104+
[qsTr("Lemma"), qsTr("Subproof"), qsTr("Sequence"), qsTr("Induction")],
105+
[qsTr("Identity "), qsTr("Negation"), qsTr("Dominance"), qsTr("Symbol Negation")]
106+
]
107+
}
108+
109+
function refreshTranslations() {
110+
chooseCategories = getChooseCategories()
111+
combo2 = getCombo2()
112+
}
113+
114+
Connections {
115+
target: settings
116+
function onLanguageChanged() {
117+
refreshTranslations()
118+
}
119+
}
120+
100121
anchors.fill: parent
101122

102123
Shortcut {
@@ -196,7 +217,6 @@ Item {
196217
proofModel.updateLines()
197218
proofModel.updateRefs(insertIndex, true)
198219
listView.currentIndex = insertIndex
199-
proofModel.premiseCount = proofModel.premiseCount + 1
200220
fileModified = true
201221
cConnector.evalText = "Evaluate Proof"
202222
proofModel.clearErrors()
@@ -233,16 +253,13 @@ Item {
233253
var myType = proofModel.data(proofModel.index(myIdx, 0), 258)
234254

235255
if (listView.count > 1) {
236-
if (myType === "premise")
237-
proofModel.premiseCount = proofModel.premiseCount - 1
238256
theData.removeLineAt(myIdx)
239257
proofModel.updateLines()
240258
proofModel.updateRefs(myIdx, false)
241259
listView.currentIndex = Math.min(myIdx, listView.count - 1)
242260
} else {
243261
theData.removeLineAt(0)
244262
theData.insertLine(0, 1, "", "premise", false, false, false, 0, [-1])
245-
proofModel.premiseCount = 1
246263
proofModel.updateLines()
247264
listView.currentIndex = 0
248265
}
@@ -405,6 +422,11 @@ Item {
405422
property int indexx: model.index
406423
property bool vis: type === "premise" || type === "subproof"
407424
|| type === "sf"
425+
// These delegate-level ints mirror the ProofModel roles.
426+
// They must live here (not inside a ComboBox) because inside a ComboBox,
427+
// `model` refers to the combo's own string-array model, NOT the row data.
428+
property int savedRuleCategory: model.ruleCategory
429+
property int savedRuleIndex: model.ruleIndex
408430
property string textFieldColor: {
409431
if (rootProofArea.selectedIndices.includes(indexx)) {
410432
return darkMode ? "#5C469C" : "#E6E6FA"
@@ -423,6 +445,18 @@ Item {
423445
listView.currentIndex = temp
424446
}
425447

448+
// Restore stored integer role values when language change resets combobox models.
449+
Connections {
450+
target: settings
451+
function onLanguageChanged() {
452+
if (outerColumn.savedRuleCategory >= 0)
453+
chooseID.currentIndex = outerColumn.savedRuleCategory
454+
if (outerColumn.savedRuleIndex >= 0)
455+
conclusionRuleID.currentIndex = outerColumn.savedRuleIndex
456+
}
457+
}
458+
459+
426460
RowLayout {
427461
id: root_delegate
428462
spacing: scaledSpacing
@@ -452,24 +486,28 @@ Item {
452486

453487
// Add this button's line to the current line's references
454488
onClicked: {
455-
if (listView.currentIndex <= index)
489+
if (listView.currentIndex <= index) {
456490
console.log("Invalid Operation : Can only reference to smaller line numbers")
457-
else if (proofModel.data(proofModel.index(
491+
cConnector.evalText = "⚠ " + qsTr("Invalid Operation: A proof line can only reference earlier line numbers.")
492+
} else if (proofModel.data(proofModel.index(
458493
listView.currentIndex, 0),
459-
257) === "premise")
494+
257) === "premise") {
460495
console.log("Invalid Operation: Current Line is a premise")
461-
else if (proofModel.data(proofModel.index(
496+
cConnector.evalText = "⚠ " + qsTr("Invalid Operation: Cannot assign inference rules or references to a premise.")
497+
} else if (proofModel.data(proofModel.index(
462498
listView.currentIndex, 0),
463-
260) === true)
499+
260) === true) {
464500
//|| proofModel.data(proofModel.index(listView.currentIndex,0),261) === true)
465501
console.log("Invalid Operation: Subproof beginning")
466-
else if (proofModel.data(
502+
cConnector.evalText = "⚠ " + qsTr("Invalid Operation: Cannot modify or reference the start line of a subproof directly.")
503+
} else if (proofModel.data(
467504
proofModel.index(listView.currentIndex, 0),
468505
262) < model.ind && proofModel.data(
469506
proofModel.index(listView.currentIndex, 0),
470-
261) === false)
507+
261) === false) {
471508
console.log("Invalid Operation: Invalid reference to subproof")
472-
else {
509+
cConnector.evalText = "⚠ " + qsTr("Invalid Operation: Cannot reference lines across closed subproof boundaries.")
510+
} else {
473511
cConnector.evalText = "Evaluate Proof"
474512
proofModel.clearErrors()
475513
var array = Array.from(proofModel.data(
@@ -482,6 +520,7 @@ Item {
482520
proofModel.setData(proofModel.index(
483521
listView.currentIndex,
484522
0), array, 263)
523+
fileModified = true
485524
refreshTextFieldColor()
486525
return
487526
}
@@ -490,6 +529,7 @@ Item {
490529
proofModel.setData(proofModel.index(
491530
listView.currentIndex, 0),
492531
array, 263)
532+
fileModified = true
493533
refreshTextFieldColor()
494534
}
495535
}
@@ -636,6 +676,8 @@ Item {
636676
}
637677
}
638678

679+
onTextEdited: fileModified = true
680+
639681
// Save Text inside Model
640682
onEditingFinished: {
641683
if (model.lText !== text) {
@@ -715,26 +757,16 @@ Item {
715757
onActivated: {
716758
editCombos = true
717759
proofModel.setData(proofModel.index(indexx, 0),
718-
conclusionRuleID.currentText, 258)
760+
currentIndex, 265) // RuleCategoryRole
761+
fileModified = true
719762
asteriskID.visible = false
720763
}
721764

722-
model: [qsTr("Inference"), qsTr("Equivalence"), qsTr("Predicate"), qsTr("Miscellaneous"), qsTr("Boolean")]
765+
model: chooseCategories
723766

724-
Component.onCompleted: {
725-
if (!editCombos) {
726-
if (combo2[0].includes(type))
727-
currentIndex = 0
728-
else if (combo2[1].includes(type))
729-
currentIndex = 1
730-
else if (combo2[2].includes(type))
731-
currentIndex = 2
732-
else if (combo2[3].includes(type))
733-
currentIndex = 3
734-
else
735-
currentIndex = 4
736-
}
737-
}
767+
// Use delegate-level savedRuleCategory (not `model.ruleCategory` here,
768+
// because inside a ComboBox `model` shadows the row data).
769+
currentIndex: outerColumn.savedRuleCategory >= 0 ? outerColumn.savedRuleCategory : currentIndex
738770
}
739771

740772
// Second ComboBox to select rule
@@ -775,17 +807,34 @@ Item {
775807
onActivated: {
776808
editCombos = true
777809
proofModel.setData(proofModel.index(indexx, 0),
778-
currentText, 258)
810+
chooseID.currentIndex, 265) // RuleCategoryRole
811+
// Write the rule index integer (locale-invariant).
812+
proofModel.setData(proofModel.index(indexx, 0),
813+
currentIndex, 266) // RuleIndexRole
814+
fileModified = true
779815
asteriskID.visible = false
780816
}
781817

782-
onModelChanged: {
783-
if (!editCombos) {
784-
currentIndex = model.indexOf(type)
785-
}
818+
// DO NOT use a declarative `currentIndex:` binding here.
819+
// When chooseID.currentIndex changes, combo2[cat] changes,
820+
// which causes QML to reset currentIndex internally — destroying
821+
// any declarative binding. Instead we use onModelChanged to
822+
// re-apply the saved ruleIndex after the model swap settles.
823+
model: combo2[chooseID.currentIndex]
824+
825+
Component.onCompleted: {
826+
// `model` here is the combo's string array — use outerColumn.savedRuleIndex.
827+
if (outerColumn.savedRuleIndex >= 0)
828+
currentIndex = outerColumn.savedRuleIndex
786829
}
787830

788-
model: combo2[chooseID.currentIndex]
831+
onModelChanged: {
832+
// Fires when chooseID.currentIndex changes (during load or user action).
833+
if (!editCombos && outerColumn.savedRuleIndex >= 0)
834+
currentIndex = outerColumn.savedRuleIndex // restore on load
835+
else if (editCombos)
836+
currentIndex = 0 // user picked a new category → start at rule 0
837+
}
789838
}
790839

791840
// Display Asterisk next to ComboBox if rule not chosen
@@ -841,6 +890,7 @@ Item {
841890
proofModel.setData(proofModel.index(
842891
listView.currentIndex,
843892
0), ar, 263)
893+
fileModified = true
844894
cConnector.evalText = "Evaluate Proof"
845895
proofModel.clearErrors()
846896
}
@@ -869,10 +919,6 @@ Item {
869919
}
870920

871921
onClicked: {
872-
if (computePremise) {
873-
proofModel.recomputePremiseCount()
874-
computePremise = false
875-
}
876922
optionsID.open()
877923
}
878924

@@ -904,7 +950,6 @@ Item {
904950
listView.currentIndex = insertIndex
905951
cConnector.evalText = "Evaluate Proof"
906952
proofModel.clearErrors()
907-
proofModel.premiseCount = proofModel.premiseCount + 1
908953
}
909954
}
910955
Action {
@@ -1000,17 +1045,13 @@ Item {
10001045
proofModel.clearErrors()
10011046

10021047
if (listView.count > 1) {
1003-
if (type === "premise")
1004-
proofModel.premiseCount = proofModel.premiseCount - 1
1005-
10061048
var i = index
10071049
theData.removeLineAt(index)
10081050
proofModel.updateLines()
10091051
proofModel.updateRefs(i, false)
10101052
} else {
10111053
theData.removeLineAt(0)
10121054
theData.insertLine(0, 1, "", "premise", false, false, false, 0, [-1])
1013-
proofModel.premiseCount = 1
10141055
proofModel.updateLines()
10151056
listView.currentIndex = 0
10161057
console.log("Goal 3: Last line reset to prevent blank screen crash.")

0 commit comments

Comments
 (0)