From 2f6abf61ff39e16a7df18143b08c264541b7f806 Mon Sep 17 00:00:00 2001 From: konard Date: Fri, 13 Feb 2026 23:55:53 +0100 Subject: [PATCH 1/5] Initial commit with task details Adding .gitkeep for PR creation (created with --gitkeep-file flag). This file will be removed when the task is complete. Issue: https://github.com/netkeep80/aprover/issues/56 --- .gitkeep | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.gitkeep b/.gitkeep index 92a1936..7023912 100644 --- a/.gitkeep +++ b/.gitkeep @@ -3,4 +3,5 @@ # Branch: issue-41-4a8c5ae3f3bc # Timestamp: 2026-02-13T19:06:21.093Z # This file was created with --gitkeep-file flag -# It will be removed when the task is complete \ No newline at end of file +# It will be removed when the task is complete +# Updated: 2026-02-13T22:55:53.421Z \ No newline at end of file From edf98569b7975d879724421cbcd9dbf1c803c78c Mon Sep 17 00:00:00 2001 From: konard Date: Sat, 14 Feb 2026 00:08:09 +0100 Subject: [PATCH 2/5] feat: Make terminating periods optional in formal notation Remove the requirement for periods (.) at the end of formulas. Periods, commas, and newlines can now be used as optional separators between statements, but are not required. Changes: - Parser: Made DOT and COMMA tokens optional separators in parseStatement() - Updated grammar documentation to reflect optional separators - Updated all example .mtl files to remove terminating periods - Updated documentation in formal-notation.md and specification-v0.1.md - Updated tests to reflect new behavior Fixes #56 Co-Authored-By: Claude Sonnet 4.5 --- docs/mts/formal-notation.md | 72 ++++++++++++++++---------------- docs/mts/specification-v0.1.md | 2 +- examples/basic.mtl | 40 +++++++++--------- examples/test-issue-48-error.mtl | 16 +++---- examples/test-issue-48.mtl | 16 +++---- src/core/parser.ts | 21 ++++++++-- tests/unit/parser.test.ts | 40 +++++++++++++----- 7 files changed, 120 insertions(+), 87 deletions(-) diff --git a/docs/mts/formal-notation.md b/docs/mts/formal-notation.md index 2795fec..c1f2efc 100644 --- a/docs/mts/formal-notation.md +++ b/docs/mts/formal-notation.md @@ -46,7 +46,7 @@ ```ebnf File = { Stmt } ; -Stmt = Expr , "." ; +Stmt = Expr , [ "." | "," ] ; (* separators are optional *) Expr = DefExpr | EqExpr | NeqExpr | Term ; @@ -100,9 +100,9 @@ Ctx = "[" , AbitSeq , "]" ; У тебя явно зафиксированы: ориентированность, единственность, порождение равенства, guarded recursion. ```mts -(s : F) != (F : s). -(s : F) : (s = F). -{ s : F, s : G } : (F = G). +(s : F) != (F : s) +(s : F) : (s = F) +{ s : F, s : G } : (F = G) ``` > Заметь: это ровно твой тезис “`:` и `=` — разные онтологические категории, но `:` порождает `=`”. @@ -112,20 +112,20 @@ Ctx = "[" , AbitSeq , "]" ; Ты формулируешь её как “равенство сложных сводится к равенству компонентов” и даёшь схемы через `{…}`. ```mts -((a -> b) = (c -> d)) : { a = c, b = d }. -{ a = c, b = d } : ((a -> b) = (c -> d)). +((a -> b) = (c -> d)) : { a = c, b = d } +{ a = c, b = d } : ((a -> b) = (c -> d)) -(♂a = ♂b) : (a = b). -(a = b) : (♂a = ♂b). +(♂a = ♂b) : (a = b) +(a = b) : (♂a = ♂b) -(a♀ = b♀) : (a = b). -(a = b) : (a♀ = b♀). +(a♀ = b♀) : (a = b) +(a = b) : (a♀ = b♀) -(¬a = ¬b) : (a = b). -(a = b) : (¬a = ¬b). +(¬a = ¬b) : (a = b) +(a = b) : (¬a = ¬b) -(!a = !b) : (a = b). -(a = b) : (!a = !b). +(!a = !b) : (a = b) +(a = b) : (!a = !b) ``` ### 3.3 Кванторы форм: `∞`, `♂`, `♀`, `->` @@ -134,20 +134,20 @@ Ctx = "[" , AbitSeq , "]" ; “Фундаментальная теорема” про `r -> v : (r -> v)` тоже есть. ```mts -∞ : (∞ -> ∞). +∞ : (∞ -> ∞) -♂x : (♂x -> x). -x♀ : (x -> x♀). +♂x : (♂x -> x) +x♀ : (x -> x♀) -(r -> v) : (r -> v). +(r -> v) : (r -> v) ``` А “уникальность” акорня ты формулируешь как эквивалентность `x = (x -> x)` и `x = ∞`. Без введения отдельного `⇔` даём как две направленные аксиомы через `:`: ```mts -(x = (x -> x)) : (x = ∞). -(x = ∞) : (x = (x -> x)). +(x = (x -> x)) : (x = ∞) +(x = ∞) : (x = (x -> x)) ``` ### 3.4 Инверсия направления `¬` (замена твоего `-`) @@ -157,14 +157,14 @@ x♀ : (x -> x♀). Чтобы не повторить внутреннюю несогласованность “и просто переворот, и совместимость”, фиксирую **одну когерентную схему**: инверсия переворачивает связь и рекурсивно применяется к компонентам (контравариантно): ```mts -¬(a -> b) : (¬b -> ¬a). -¬(a !-> b) : (¬b !-> ¬a). +¬(a -> b) : (¬b -> ¬a) +¬(a !-> b) : (¬b !-> ¬a) -¬(♂x) : (x♀). -¬(x♀) : (♂x). -¬∞ : ∞. +¬(♂x) : (x♀) +¬(x♀) : (♂x) +¬∞ : ∞ -¬¬x = x. +¬¬x = x ``` ### 3.5 Несвязь `!->` и смысловая дуальность `!`, `0/1` @@ -175,23 +175,23 @@ x♀ : (x -> x♀). Делаем `!->` определением “негации связи”: ```mts -!(a -> b) : (a !-> b). -!(a !-> b) : (a -> b). +!(a -> b) : (a !-> b) +!(a !-> b) : (a -> b) -!!x = x. +!!x = x ``` Определяем `1` как “единицу смысла” (у тебя это `♂∞ -> ∞♀`). ```mts -1 : (♂∞ -> ∞♀). +1 : (♂∞ -> ∞♀) ``` А `0` задаём как дуал `1` через `!` (и тем самым выполняем твои пункты 4–5): ```mts -!1 : 0. -!0 : 1. +!1 : 0 +!0 : 1 ``` (Отсюда, через “(s:F) : (s = F)” + симметрию равенства в ядре прувера, получатся привычные записи `0 = !1`, `1 = !0`.) @@ -203,8 +203,8 @@ x♀ : (x -> x♀). Фиксируем новую пару: ```mts -[ : (♂∞ -> ∞). -] : (∞ -> ∞♀). +[ : (♂∞ -> ∞) +] : (∞ -> ∞♀) ``` ### 3.7 Акс. левоассоциативности цепочек @@ -212,8 +212,8 @@ x♀ : (x -> x♀). У тебя это отдельный “онтологический принцип группировки”. ```mts -(a -> b -> c) = ((a -> b) -> c). -(a -> (b -> c)) != ((a -> b) -> c). +(a -> b -> c) = ((a -> b) -> c) +(a -> (b -> c)) != ((a -> b) -> c) ``` --- diff --git a/docs/mts/specification-v0.1.md b/docs/mts/specification-v0.1.md index f70d3c8..a0f4ea0 100644 --- a/docs/mts/specification-v0.1.md +++ b/docs/mts/specification-v0.1.md @@ -67,7 +67,7 @@ EBNF: File ::= { Stmt } ; -Stmt ::= Expr "." ; +Stmt ::= Expr [ "." | "," ] ; // separators are optional Expr ::= DefExpr | EqExpr diff --git a/examples/basic.mtl b/examples/basic.mtl index 3cd4ac6..dbd756d 100644 --- a/examples/basic.mtl +++ b/examples/basic.mtl @@ -8,10 +8,10 @@ // ======================================== // Тождественность акорня самому себе -∞ = ∞. +∞ = ∞ // Акорень равен связи с самим собой -∞ = ∞ -> ∞. +∞ = ∞ -> ∞ // ======================================== // А5. Самозамыкание начала @@ -19,10 +19,10 @@ // ======================================== // Мужской оператор определяет самозамыкание начала -♂v = ♂v -> v. +♂v = ♂v -> v // Вложенность мужского оператора -♂♂v = ♂♂v -> ♂v. +♂♂v = ♂♂v -> ♂v // ======================================== // А6. Самозамыкание конца @@ -30,10 +30,10 @@ // ======================================== // Женский оператор определяет самозамыкание конца -r♀ = r -> r♀. +r♀ = r -> r♀ // Вложенность женского оператора -r♀♀ = r♀ -> r♀♀. +r♀♀ = r♀ -> r♀♀ // ======================================== // А7. Аксиома инверсии @@ -42,14 +42,14 @@ r♀♀ = r♀ -> r♀♀. // ======================================== // Инверсия мужского оператора -!♂x = x♀. +!♂x = x♀ // Инверсия женского оператора -!x♀ = ♂x. +!x♀ = ♂x // Инверсия акорня -!♂∞ = ∞♀. -!∞♀ = ♂∞. +!♂∞ = ∞♀ +!∞♀ = ♂∞ // ======================================== // А11. Левоассоциативность связи @@ -57,10 +57,10 @@ r♀♀ = r♀ -> r♀♀. // ======================================== // Цепочка связей левоассоциативна -a -> b -> c = (a -> b) -> c. +a -> b -> c = (a -> b) -> c // Более длинная цепочка -a -> b -> c -> d = ((a -> b) -> c) -> d. +a -> b -> c -> d = ((a -> b) -> c) -> d // ======================================== // Степенной оператор @@ -68,31 +68,31 @@ a -> b -> c -> d = ((a -> b) -> c) -> d. // ======================================== // a^2 = (a -> a) -a^2 = a -> a. +a^2 = a -> a // a^3 = ((a -> a) -> a) -a^3 = (a -> a) -> a. +a^3 = (a -> a) -> a // a^4 = (((a -> a) -> a) -> a) -a^4 = ((a -> a) -> a) -> a. +a^4 = ((a -> a) -> a) -> a // ======================================== // Комбинированные выражения // ======================================== // Применение ♂ к ∞ -♂∞ = ♂∞ -> ∞. +♂∞ = ♂∞ -> ∞ // Применение ♀ к ∞ -∞♀ = ∞ -> ∞♀. +∞♀ = ∞ -> ∞♀ // Комбинация ♂ и ♀ -♂∞♀ = (♂∞)♀. +♂∞♀ = (♂∞)♀ // ======================================== // Неравенства // ======================================== // Различные выражения не равны -♂∞♀ != ∞. -♂∞ != ∞♀. +♂∞♀ != ∞ +♂∞ != ∞♀ diff --git a/examples/test-issue-48-error.mtl b/examples/test-issue-48-error.mtl index af3405e..36d81e3 100644 --- a/examples/test-issue-48-error.mtl +++ b/examples/test-issue-48-error.mtl @@ -2,21 +2,21 @@ // Примеры аксиом и формул // А4. Смысл (акорень): ∞ : (∞ -> ∞) -∞ = ∞ -> ∞. +∞ = ∞ -> ∞ // А5. Самозамыкание начала: ♂x : (♂x -> x) -♂v = ♂v -> v. +♂v = ♂v -> v // А6. Самозамыкание конца: x♀ : (x -> x♀) -r♀ = r -> r♀. +r♀ = r -> r♀ // А7. Инверсия -!♂x = x♀. -!x♀ = ♂x.) // тут некорректная закрывающая скобка +!♂x = x♀ +!x♀ = ♂x) // тут некорректная закрывающая скобка // А11. Левоассоциативность -a -> b -> c = (a -> b) -> c. +a -> b -> c = (a -> b) -> c // Степени -a^2 = a -> a. -a^3 = (a -> a) -> a. +a^2 = a -> a +a^3 = (a -> a) -> a diff --git a/examples/test-issue-48.mtl b/examples/test-issue-48.mtl index 6a238dc..685ade6 100644 --- a/examples/test-issue-48.mtl +++ b/examples/test-issue-48.mtl @@ -2,21 +2,21 @@ // Пример из issue #48 с ошибкой парсинга // А4. Смысл (акорень): ∞ : (∞ -> ∞) -∞ = ∞ -> ∞. +∞ = ∞ -> ∞ // А5. Самозамыкание начала: ♂x : (♂x -> x) -♂v = ♂v -> v. +♂v = ♂v -> v // А6. Самозамыкание конца: x♀ : (x -> x♀) -r♀ = r -> r♀. +r♀ = r -> r♀ // А7. Инверсия -!♂x = x♀. -!x♀ = ♂x.) // тут некорректная закрывающая скобка +!♂x = x♀ +!x♀ = ♂x) // тут некорректная закрывающая скобка // А11. Левоассоциативность -a -> b -> c = (a -> b) -> c. +a -> b -> c = (a -> b) -> c // Степени -a^2 = a -> a. -a^3 = (a -> a) -> a. +a^2 = a -> a +a^3 = (a -> a) -> a diff --git a/src/core/parser.ts b/src/core/parser.ts index 5f7e212..1cfadd1 100644 --- a/src/core/parser.ts +++ b/src/core/parser.ts @@ -4,7 +4,7 @@ * * Grammar (simplified): * File ::= { Stmt } - * Stmt ::= Expr "." + * Stmt ::= Expr [ "." | "," ] // separators are optional * Expr ::= DefExpr | EqExpr | NeqExpr | Term * DefExpr ::= Term ":" Term * EqExpr ::= Term "=" Term @@ -164,15 +164,28 @@ export class Parser { } } - /** Parse statement: Expr "." */ + /** Parse statement: Expr ["." | "," | newline] + * Periods, commas, and newlines are optional separators between statements. + * They are consumed if present but not required. + */ private parseStatement(): Statement { const expr = this.parseExpr() - const dot = this.expect('DOT') + + // Optional separator: consume period or comma if present + // Newlines are already consumed by whitespace skipping in lexer + if (this.checkAny('DOT', 'COMMA')) { + const separator = this.advance() + return { + type: 'Statement', + expr, + loc: this.mergeLoc(expr.loc!, separator.loc), + } + } return { type: 'Statement', expr, - loc: this.mergeLoc(expr.loc!, dot.loc), + loc: expr.loc!, } } diff --git a/tests/unit/parser.test.ts b/tests/unit/parser.test.ts index 67e2e0a..cd65188 100644 --- a/tests/unit/parser.test.ts +++ b/tests/unit/parser.test.ts @@ -180,12 +180,36 @@ describe('Parser', () => { }) describe('File parsing', () => { - it('should parse multiple statements', () => { + it('should parse multiple statements with periods', () => { const file = parse('a = b. c = d.') expect(file.type).toBe('File') expect(file.statements.length).toBe(2) }) + it('should parse multiple statements with commas', () => { + const file = parse('a = b, c = d') + expect(file.type).toBe('File') + expect(file.statements.length).toBe(2) + }) + + it('should parse multiple statements with newlines', () => { + const file = parse('a = b\nc = d') + expect(file.type).toBe('File') + expect(file.statements.length).toBe(2) + }) + + it('should parse multiple statements without separators', () => { + const file = parse('a = b\nc = d\ne = f') + expect(file.type).toBe('File') + expect(file.statements.length).toBe(3) + }) + + it('should parse mixed separators', () => { + const file = parse('a = b.\nc = d,\ne = f') + expect(file.type).toBe('File') + expect(file.statements.length).toBe(3) + }) + it('should parse empty file', () => { const file = parse('') expect(file.statements.length).toBe(0) @@ -193,10 +217,6 @@ describe('Parser', () => { }) describe('Error handling', () => { - it('should throw on missing dot', () => { - expect(() => parse('a = b')).toThrow(ParseError) - }) - it('should throw on unexpected token', () => { expect(() => parseExpr(')')).toThrow(ParseError) }) @@ -212,9 +232,9 @@ e = f) const result = parseWithRecovery(input) - // Should have parsed first two statements successfully + // Should have parsed three statements successfully (e = f is valid without period) expect(result.file).not.toBeNull() - expect(result.file?.statements.length).toBe(2) + expect(result.file?.statements.length).toBe(3) // Should have error information expect(result.error).not.toBeNull() @@ -283,10 +303,10 @@ c = d. const result = parseWithRecovery(input) - // Should have parsed first statement - expect(result.file?.statements.length).toBe(1) + // Should have parsed two statements (a = b and c = d are valid) + expect(result.file?.statements.length).toBe(2) - // Error should be on line 2 + // Error should be on line 2 (the ').' part) expect(result.errorLocation?.start.line).toBe(2) expect(result.error?.message).toContain('RPAREN') }) From 38853acb1495bf45af4ef1b0eb18637fd4941964 Mon Sep 17 00:00:00 2001 From: konard Date: Sat, 14 Feb 2026 00:09:55 +0100 Subject: [PATCH 3/5] Revert "Initial commit with task details" This reverts commit 2f6abf61ff39e16a7df18143b08c264541b7f806. --- .gitkeep | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/.gitkeep b/.gitkeep index 7023912..92a1936 100644 --- a/.gitkeep +++ b/.gitkeep @@ -3,5 +3,4 @@ # Branch: issue-41-4a8c5ae3f3bc # Timestamp: 2026-02-13T19:06:21.093Z # This file was created with --gitkeep-file flag -# It will be removed when the task is complete -# Updated: 2026-02-13T22:55:53.421Z \ No newline at end of file +# It will be removed when the task is complete \ No newline at end of file From d15f619831ff4695b5214760882e04b2a1d10dce Mon Sep 17 00:00:00 2001 From: konard Date: Sat, 14 Feb 2026 00:18:19 +0100 Subject: [PATCH 4/5] feat: Remove period support from parser - only allow commas and newlines Based on feedback from netkeep80, periods should not be supported at all as separators. Only commas and newlines should work as statement separators. Changes: - Updated parser to remove DOT token support in parseStatement() - Updated parseExpr() helper to not append period - Updated EBNF grammar in formal-notation.md and specification-v0.1.md - Updated all test cases to remove periods - All 255 tests pass successfully Addresses feedback in PR #57 Co-Authored-By: Claude Sonnet 4.5 --- docs/mts/formal-notation.md | 2 +- docs/mts/specification-v0.1.md | 2 +- experiments/test-error-location.ts | 7 ++++- src/core/parser.ts | 15 ++++----- tests/integration/mtl_formulas.test.ts | 12 ++++---- tests/unit/parser.test.ts | 42 +++++++++++--------------- 6 files changed, 40 insertions(+), 40 deletions(-) diff --git a/docs/mts/formal-notation.md b/docs/mts/formal-notation.md index c1f2efc..394457d 100644 --- a/docs/mts/formal-notation.md +++ b/docs/mts/formal-notation.md @@ -46,7 +46,7 @@ ```ebnf File = { Stmt } ; -Stmt = Expr , [ "." | "," ] ; (* separators are optional *) +Stmt = Expr , [ "," ] ; (* comma separator is optional *) Expr = DefExpr | EqExpr | NeqExpr | Term ; diff --git a/docs/mts/specification-v0.1.md b/docs/mts/specification-v0.1.md index a0f4ea0..eab652c 100644 --- a/docs/mts/specification-v0.1.md +++ b/docs/mts/specification-v0.1.md @@ -67,7 +67,7 @@ EBNF: File ::= { Stmt } ; -Stmt ::= Expr [ "." | "," ] ; // separators are optional +Stmt ::= Expr [ "," ] ; // comma separator is optional Expr ::= DefExpr | EqExpr diff --git a/experiments/test-error-location.ts b/experiments/test-error-location.ts index 4f177a9..3b3f768 100644 --- a/experiments/test-error-location.ts +++ b/experiments/test-error-location.ts @@ -33,7 +33,12 @@ if (result.errorLocation) { console.log('\nError context:') console.log('Line', errorLine + 1, ':', lines[errorLine]) - console.log('Error at column', errorCol, '-> character:', JSON.stringify(lines[errorLine][errorCol])) + console.log( + 'Error at column', + errorCol, + '-> character:', + JSON.stringify(lines[errorLine][errorCol]) + ) // Show visual pointer const pointer = ' '.repeat(errorCol) + '^' diff --git a/src/core/parser.ts b/src/core/parser.ts index 1cfadd1..e03b8df 100644 --- a/src/core/parser.ts +++ b/src/core/parser.ts @@ -4,7 +4,7 @@ * * Grammar (simplified): * File ::= { Stmt } - * Stmt ::= Expr [ "." | "," ] // separators are optional + * Stmt ::= Expr [ "," ] // comma separator is optional * Expr ::= DefExpr | EqExpr | NeqExpr | Term * DefExpr ::= Term ":" Term * EqExpr ::= Term "=" Term @@ -164,16 +164,17 @@ export class Parser { } } - /** Parse statement: Expr ["." | "," | newline] - * Periods, commas, and newlines are optional separators between statements. + /** Parse statement: Expr ["," | newline] + * Commas and newlines are optional separators between statements. * They are consumed if present but not required. + * Periods (.) are NOT supported as separators. */ private parseStatement(): Statement { const expr = this.parseExpr() - // Optional separator: consume period or comma if present + // Optional separator: consume comma if present // Newlines are already consumed by whitespace skipping in lexer - if (this.checkAny('DOT', 'COMMA')) { + if (this.check('COMMA')) { const separator = this.advance() return { type: 'Statement', @@ -443,9 +444,9 @@ export function parseWithRecovery(input: string): ParseResult { return parser.parseFileWithRecovery() } -/** Parse single expression (without trailing dot) */ +/** Parse single expression */ export function parseExpr(input: string): ASTNode { - const lexer = new Lexer(input + '.') + const lexer = new Lexer(input) const tokens = lexer.tokenize() const parser = new Parser(tokens) const file = parser.parseFile() diff --git a/tests/integration/mtl_formulas.test.ts b/tests/integration/mtl_formulas.test.ts index e8130c3..e259342 100644 --- a/tests/integration/mtl_formulas.test.ts +++ b/tests/integration/mtl_formulas.test.ts @@ -21,7 +21,7 @@ import { createProverState, verify } from '../../src/core/prover' * Parse and verify a single formula string */ function verifyFormula(formula: string): { success: boolean; message: string } { - const file = parse(formula + '.') + const file = parse(formula) const state = createProverState() const stmt = file.statements[0] const normalized = normalize(stmt.expr) @@ -179,10 +179,10 @@ describe('Integration: mtl_formulas.mtc', () => { describe('Integration: Full pipeline test', () => { it('should process multiple statements', () => { const input = ` - ∞ = ∞ -> ∞. - ♂v = ♂v -> v. - r♀ = r -> r♀. - !♂x = x♀. + ∞ = ∞ -> ∞ + ♂v = ♂v -> v + r♀ = r -> r♀ + !♂x = x♀ ` const file = parse(input) expect(file.statements).toHaveLength(4) @@ -197,7 +197,7 @@ describe('Integration: Full pipeline test', () => { it('should normalize and verify power expressions correctly', () => { // Power expansion should work with normalizer - const input = 'a^5.' + const input = 'a^5' const file = parse(input) const stmt = file.statements[0] const normalized = normalize(stmt.expr) diff --git a/tests/unit/parser.test.ts b/tests/unit/parser.test.ts index cd65188..8581eab 100644 --- a/tests/unit/parser.test.ts +++ b/tests/unit/parser.test.ts @@ -180,12 +180,6 @@ describe('Parser', () => { }) describe('File parsing', () => { - it('should parse multiple statements with periods', () => { - const file = parse('a = b. c = d.') - expect(file.type).toBe('File') - expect(file.statements.length).toBe(2) - }) - it('should parse multiple statements with commas', () => { const file = parse('a = b, c = d') expect(file.type).toBe('File') @@ -204,8 +198,8 @@ describe('Parser', () => { expect(file.statements.length).toBe(3) }) - it('should parse mixed separators', () => { - const file = parse('a = b.\nc = d,\ne = f') + it('should parse mixed separators (commas and newlines)', () => { + const file = parse('a = b\nc = d,\ne = f') expect(file.type).toBe('File') expect(file.statements.length).toBe(3) }) @@ -225,14 +219,14 @@ describe('Parser', () => { describe('Partial parsing with error recovery', () => { it('should return partial AST when error occurs after valid statements', () => { const input = ` -a = b. -c = d. +a = b +c = d e = f) `.trim() const result = parseWithRecovery(input) - // Should have parsed three statements successfully (e = f is valid without period) + // Should have parsed three statements successfully (e = f is valid) expect(result.file).not.toBeNull() expect(result.file?.statements.length).toBe(3) @@ -245,7 +239,7 @@ e = f) it('should return null file when error occurs on first statement', () => { const input = ` ) -a = b. +a = b `.trim() const result = parseWithRecovery(input) @@ -260,22 +254,22 @@ a = b. it('should handle error from issue #48 example', () => { const input = ` -∞ = ∞ -> ∞. -♂v = ♂v -> v. -r♀ = r -> r♀. -!♂x = x♀. -!x♀ = ♂x.) -a -> b -> c = (a -> b) -> c. +∞ = ∞ -> ∞ +♂v = ♂v -> v +r♀ = r -> r♀ +!♂x = x♀ +!x♀ = ♂x) +a -> b -> c = (a -> b) -> c `.trim() const result = parseWithRecovery(input) - // Line 5 is "!x♀ = ♂x.)" which parses as "!x♀ = ♂x." followed by stray ")" + // Line 5 is "!x♀ = ♂x)" which parses as "!x♀ = ♂x" followed by stray ")" // So 5 valid statements should be parsed (lines 1-5) expect(result.file).not.toBeNull() expect(result.file?.statements.length).toBe(5) - // Should have error on the closing paren after the dot + // Should have error on the closing paren expect(result.error).not.toBeNull() expect(result.error?.message).toContain('RPAREN') expect(result.errorLocation?.start.line).toBe(5) @@ -283,8 +277,8 @@ a -> b -> c = (a -> b) -> c. it('should return no error when parsing is fully successful', () => { const input = ` -a = b. -c = d. +a = b +c = d `.trim() const result = parseWithRecovery(input) @@ -299,14 +293,14 @@ c = d. }) it('should provide correct error location', () => { - const input = 'a = b.\nc = d).' + const input = 'a = b\nc = d)' const result = parseWithRecovery(input) // Should have parsed two statements (a = b and c = d are valid) expect(result.file?.statements.length).toBe(2) - // Error should be on line 2 (the ').' part) + // Error should be on line 2 (the ')' part) expect(result.errorLocation?.start.line).toBe(2) expect(result.error?.message).toContain('RPAREN') }) From 51e7730fc8cb00ebc849da86208616e012dbde09 Mon Sep 17 00:00:00 2001 From: konard Date: Sat, 14 Feb 2026 00:21:52 +0100 Subject: [PATCH 5/5] fix: Update E2E tests to remove period separators Updated all E2E tests to use newlines instead of periods as statement separators, consistent with the new parser behavior. Co-Authored-By: Claude Sonnet 4.5 --- tests/e2e/editor.spec.ts | 70 ++++++++++++++++++++-------------------- 1 file changed, 35 insertions(+), 35 deletions(-) diff --git a/tests/e2e/editor.spec.ts b/tests/e2e/editor.spec.ts index 8b525a1..2bacd9f 100644 --- a/tests/e2e/editor.spec.ts +++ b/tests/e2e/editor.spec.ts @@ -44,7 +44,7 @@ test.describe('aprover Web Interface', () => { const editor = page.locator('.code-input') // Clear editor and enter a simple valid formula - await editor.fill('∞ = ∞.') + await editor.fill('∞ = ∞') // Wait for results to update await expect(page.locator('.result-item')).toHaveCount(1) @@ -53,7 +53,7 @@ test.describe('aprover Web Interface', () => { test('should show success indicator for valid equality', async ({ page }) => { const editor = page.locator('.code-input') - await editor.fill('a = a.') + await editor.fill('a = a') const resultItem = page.locator('.result-item') await expect(resultItem).toHaveClass(/success/) @@ -64,7 +64,7 @@ test.describe('aprover Web Interface', () => { const editor = page.locator('.code-input') // Using different structures that cannot be unified: // ♂∞ (male of infinity) cannot equal ∞♀ (female of infinity) - await editor.fill('♂∞ = ∞♀.') + await editor.fill('♂∞ = ∞♀') const resultItem = page.locator('.result-item') await expect(resultItem).toHaveClass(/failure/) @@ -80,7 +80,7 @@ test.describe('aprover Web Interface', () => { test('should verify infinity axiom (А4)', async ({ page }) => { const editor = page.locator('.code-input') - await editor.fill('∞ = ∞ -> ∞.') + await editor.fill('∞ = ∞ -> ∞') await expect(page.locator('.result-item.success')).toBeVisible() await expect(page.locator('.result-status')).toHaveText('✓') @@ -88,28 +88,28 @@ test.describe('aprover Web Interface', () => { test('should verify male self-closing axiom (А5)', async ({ page }) => { const editor = page.locator('.code-input') - await editor.fill('♂v = ♂v -> v.') + await editor.fill('♂v = ♂v -> v') await expect(page.locator('.result-item.success')).toBeVisible() }) test('should verify female self-closing axiom (А6)', async ({ page }) => { const editor = page.locator('.code-input') - await editor.fill('r♀ = r -> r♀.') + await editor.fill('r♀ = r -> r♀') await expect(page.locator('.result-item.success')).toBeVisible() }) test('should verify inversion axiom (А7)', async ({ page }) => { const editor = page.locator('.code-input') - await editor.fill('!♂x = x♀.') + await editor.fill('!♂x = x♀') await expect(page.locator('.result-item.success')).toBeVisible() }) test('should verify power expansion', async ({ page }) => { const editor = page.locator('.code-input') - await editor.fill('a^2 = a -> a.') + await editor.fill('a^2 = a -> a') await expect(page.locator('.result-item.success')).toBeVisible() }) @@ -117,9 +117,9 @@ test.describe('aprover Web Interface', () => { test('should verify multiple formulas', async ({ page }) => { const editor = page.locator('.code-input') await editor.fill(` -∞ = ∞ -> ∞. -♂v = ♂v -> v. -r♀ = r -> r♀. +∞ = ∞ -> ∞ +♂v = ♂v -> v +r♀ = r -> r♀ `) const results = page.locator('.result-item') @@ -132,14 +132,14 @@ r♀ = r -> r♀. test('should verify inequality', async ({ page }) => { const editor = page.locator('.code-input') - await editor.fill('♂∞ != ∞♀.') + await editor.fill('♂∞ != ∞♀') await expect(page.locator('.result-item.success')).toBeVisible() }) test('should handle left associativity (А11)', async ({ page }) => { const editor = page.locator('.code-input') - await editor.fill('a -> b -> c = (a -> b) -> c.') + await editor.fill('a -> b -> c = (a -> b) -> c') await expect(page.locator('.result-item.success')).toBeVisible() }) @@ -182,7 +182,7 @@ r♀ = r -> r♀. test('should collapse all AST nodes', async ({ page }) => { // Enter a formula to generate AST const editor = page.locator('.code-input') - await editor.fill('a -> b.') + await editor.fill('a -> b') // Wait for AST to render await expect(page.locator('.tree-root')).toBeVisible() @@ -203,7 +203,7 @@ r♀ = r -> r♀. test('should expand all AST nodes after collapse', async ({ page }) => { // Enter a formula to generate AST const editor = page.locator('.code-input') - await editor.fill('a -> b.') + await editor.fill('a -> b') // Wait for AST to render await expect(page.locator('.tree-root')).toBeVisible() @@ -222,7 +222,7 @@ r♀ = r -> r♀. test('should display node location in AST tree', async ({ page }) => { // Enter a simple formula const editor = page.locator('.code-input') - await editor.fill('a = a.') + await editor.fill('a = a') // Wait for AST to render await expect(page.locator('.tree-root')).toBeVisible() @@ -235,7 +235,7 @@ r♀ = r -> r♀. test('should highlight source code when hovering AST node', async ({ page }) => { // Enter a simple formula const editor = page.locator('.code-input') - await editor.fill('a = a.') + await editor.fill('a = a') // Wait for AST to render await expect(page.locator('.tree-root')).toBeVisible() @@ -254,7 +254,7 @@ r♀ = r -> r♀. test('should remove highlight when mouse leaves AST node', async ({ page }) => { // Enter a simple formula const editor = page.locator('.code-input') - await editor.fill('a = a.') + await editor.fill('a = a') // Wait for AST to render await expect(page.locator('.tree-root')).toBeVisible() @@ -277,7 +277,7 @@ r♀ = r -> r♀. test('should toggle individual AST nodes', async ({ page }) => { // Enter a formula with nested structure const editor = page.locator('.code-input') - await editor.fill('a -> b.') + await editor.fill('a -> b') // Wait for AST to render with children visible await expect(page.locator('.tree-root')).toBeVisible() @@ -413,7 +413,7 @@ r♀ = r -> r♀. test('should enable export buttons when results exist', async ({ page }) => { const editor = page.locator('.code-input') - await editor.fill('a = a.') + await editor.fill('a = a') // Wait for verification to complete await expect(page.locator('.result-item')).toBeVisible() @@ -493,7 +493,7 @@ r♀ = r -> r♀. test.describe('Enhanced Prover Features', () => { test('should display applied axioms badges', async ({ page }) => { const editor = page.locator('.code-input') - await editor.fill('∞ = ∞ -> ∞.') + await editor.fill('∞ = ∞ -> ∞') // Wait for results await expect(page.locator('.result-item.success')).toBeVisible() @@ -505,7 +505,7 @@ r♀ = r -> r♀. test('should show axiom badges with correct labels', async ({ page }) => { const editor = page.locator('.code-input') - await editor.fill('∞ = ∞ -> ∞.') + await editor.fill('∞ = ∞ -> ∞') await expect(page.locator('.result-item.success')).toBeVisible() @@ -516,7 +516,7 @@ r♀ = r -> r♀. test('should show expand toggle for results with details', async ({ page }) => { const editor = page.locator('.code-input') - await editor.fill('♂v = ♂v -> v.') + await editor.fill('♂v = ♂v -> v') await expect(page.locator('.result-item.success')).toBeVisible() @@ -526,7 +526,7 @@ r♀ = r -> r♀. test('should expand proof steps on click', async ({ page }) => { const editor = page.locator('.code-input') - await editor.fill('∞ = ∞ -> ∞.') + await editor.fill('∞ = ∞ -> ∞') await expect(page.locator('.result-item.success')).toBeVisible() @@ -540,7 +540,7 @@ r♀ = r -> r♀. test('should display proof step index numbers', async ({ page }) => { const editor = page.locator('.code-input') - await editor.fill('a = a.') + await editor.fill('a = a') await expect(page.locator('.result-item.success')).toBeVisible() @@ -554,7 +554,7 @@ r♀ = r -> r♀. test('should display proof step actions', async ({ page }) => { const editor = page.locator('.code-input') - await editor.fill('a = a.') + await editor.fill('a = a') await expect(page.locator('.result-item.success')).toBeVisible() @@ -567,7 +567,7 @@ r♀ = r -> r♀. test('should collapse proof steps on second click', async ({ page }) => { const editor = page.locator('.code-input') - await editor.fill('a = a.') + await editor.fill('a = a') await expect(page.locator('.result-item.success')).toBeVisible() @@ -583,7 +583,7 @@ r♀ = r -> r♀. test('should display hints for failed verification', async ({ page }) => { const editor = page.locator('.code-input') // This should fail: male and female are dual but not equal - await editor.fill('♂∞ = ∞♀.') + await editor.fill('♂∞ = ∞♀') await expect(page.locator('.result-item.failure')).toBeVisible() @@ -594,7 +594,7 @@ r♀ = r -> r♀. test('should display hint icons', async ({ page }) => { const editor = page.locator('.code-input') - await editor.fill('♂∞ = ∞♀.') + await editor.fill('♂∞ = ∞♀') await expect(page.locator('.result-item.failure')).toBeVisible() @@ -604,7 +604,7 @@ r♀ = r -> r♀. test('should display related axiom in hints when applicable', async ({ page }) => { const editor = page.locator('.code-input') - await editor.fill('♂∞ = ∞♀.') + await editor.fill('♂∞ = ∞♀') await expect(page.locator('.result-item.failure')).toBeVisible() @@ -615,7 +615,7 @@ r♀ = r -> r♀. test('should show A5 axiom for male self-closing', async ({ page }) => { const editor = page.locator('.code-input') - await editor.fill('♂v = ♂v -> v.') + await editor.fill('♂v = ♂v -> v') await expect(page.locator('.result-item.success')).toBeVisible() @@ -625,7 +625,7 @@ r♀ = r -> r♀. test('should show A6 axiom for female self-closing', async ({ page }) => { const editor = page.locator('.code-input') - await editor.fill('r♀ = r -> r♀.') + await editor.fill('r♀ = r -> r♀') await expect(page.locator('.result-item.success')).toBeVisible() @@ -635,7 +635,7 @@ r♀ = r -> r♀. test('should show A1 axiom for structural equality', async ({ page }) => { const editor = page.locator('.code-input') - await editor.fill('a = a.') + await editor.fill('a = a') await expect(page.locator('.result-item.success')).toBeVisible() @@ -645,7 +645,7 @@ r♀ = r -> r♀. test('should show axiom tooltip on hover', async ({ page }) => { const editor = page.locator('.code-input') - await editor.fill('∞ = ∞ -> ∞.') + await editor.fill('∞ = ∞ -> ∞') await expect(page.locator('.result-item.success')).toBeVisible() @@ -658,7 +658,7 @@ r♀ = r -> r♀. test('should display axioms label', async ({ page }) => { const editor = page.locator('.code-input') - await editor.fill('a = a.') + await editor.fill('a = a') await expect(page.locator('.result-item.success')).toBeVisible()