Fix grammar compilation errors and latent build breakers

- Restructure conditionals into a condExpr precedence level and exception
  handling into a postfix rule, removing the mutual left recursion through
  expr/atomExpr (ANTLR error 119)
- Rewrite pattern as patternAtom (COMMA patternAtom)*, removing left
  recursion with an empty-matchable tail (ANTLR error 148)
- Drop the LAMBDA token fully shadowed by LAMBDA_VAR (warning 184)
- Give \Rightarrow to EXPORT only; IMPLIES keeps \implies (warning 184)
- Remove @header package declaration that duplicated the -package argument
  and made the generated parser uncompilable
- Point the ANTLR source set at src/main/antlr4 so Gradle actually finds
  the grammar
- Treat ANTLR warnings as errors (-Werror)
- Record decisions in DECISIONS.md
This commit is contained in:
developtheweb 2026-07-09 02:44:14 -04:00
parent 590762cad3
commit 5230273ab1
3 changed files with 59 additions and 20 deletions

13
DECISIONS.md Normal file
View file

@ -0,0 +1,13 @@
# Design decisions
One line per decision, with the rejected alternatives named. Governing
principles, in order: One Right Answer, the Fatima test, minimal churn
against the existing examples.
- **Conditionals are guarded alternatives** `(condition ⟹ result) | fallback`, wired in as a `condExpr` precedence level; rejected: C-style ternary `cond ? a : b` (programmer convention, fails the Fatima test), standalone left-recursive `conditional` rule (ANTLR error 119).
- **Exception handling is a postfix operator** `expr ↴ { … }`; rejected: standalone `exceptionHandler` rule reachable from `atomExpr` (mutual left recursion, ANTLR error 119).
- **λ has one token, `LAMBDA_VAR`**, used both as a variable and to open a lambda; rejected: separate `LAMBDA` token (identical alternatives, fully shadowed, ANTLR warning 184).
- **`\implies` maps to ⟹ and `\Rightarrow` maps to ⇒** — one escape, one glyph; rejected: `\Rightarrow` as an alias of ⟹ (shadowed EXPORT's escape, ANTLR warning 184).
- **The Java package for generated code comes from `-package` in build.gradle only**; rejected: `@header` package declaration in the grammar (combined with `-package` it generates a duplicate `package` statement that does not compile).
- **ANTLR warnings fail the build** (`-Werror` in build.gradle); rejected: warnings as advisory output (they hid the shadowed-token bugs).
- **The choice-type rule is `⟨ expr ⟩`** with the interior `|` consumed by `condExpr`; rejected: explicit `⟨ expr | expr ⟩` (the interior expr already consumes the bar, making the explicit BAR unreachable).

View file

@ -20,7 +20,8 @@ dependencies {
generateGrammarSource {
maxHeapSize = "64m"
arguments += ["-visitor", "-listener", "-package", "com.mpl.parser"]
// -Werror: any ANTLR warning (e.g. 184, token shadowing) fails the build
arguments += ["-visitor", "-listener", "-Werror", "-package", "com.mpl.parser"]
outputDirectory = file("${project.buildDir}/generated-src/antlr/main/com/mpl/parser")
}
@ -28,6 +29,11 @@ compileJava.dependsOn generateGrammarSource
sourceSets {
main {
antlr {
// The Gradle ANTLR plugin defaults to src/main/antlr; the grammar
// lives in src/main/antlr4 (Maven layout).
srcDirs = ['src/main/antlr4']
}
java {
srcDirs += "${project.buildDir}/generated-src/antlr/main"
}

View file

@ -1,8 +1,7 @@
grammar MPL;
@header {
package com.mpl.parser;
}
// The Java package comes from the '-package com.mpl.parser' argument in
// build.gradle. An @header package declaration here would duplicate it.
// ============================================================================
// PARSER RULES
@ -31,7 +30,15 @@ parallelExpr
;
assignExpr
: impliesExpr (LEFTARROW assignExpr)? // Level 0: Assignment (right-assoc)
: condExpr (LEFTARROW assignExpr)? // Level 0: Assignment (right-assoc)
;
// Guarded alternatives: (condition ⟹ result) | fallback
// This is the canonical conditional form. It lives in the precedence chain
// (below assignment, above implication) instead of being a left-recursive
// standalone rule, which previously caused ANTLR error(119).
condExpr
: impliesExpr (BAR impliesExpr)*
;
impliesExpr
@ -67,13 +74,28 @@ composeExpr
;
unaryExpr
: prefixOp* appExpr // Level 8: Prefix operators
: prefixOp* postfixExpr // Level 8: Prefix operators
;
prefixOp
: RAISE | TRACE | QUERY | BREAK | DELAY
;
// Exception handling is a postfix construct: expr ↴ { ↯name ⇒ handler }
// Formerly a standalone rule reachable from atomExpr, which cycled back into
// expr and caused ANTLR error(119) (mutual left recursion).
postfixExpr
: appExpr handlerSuffix*
;
handlerSuffix
: HANDLE LBRACE handlerClause+ RBRACE
;
handlerClause
: RAISE IDENTIFIER EXPORT expr
;
appExpr
: atomExpr atomExpr* // Level 9: Function application
;
@ -84,7 +106,6 @@ atomExpr
| block
| lambda
| forall
| conditional
| choiceType
| atomicSection
| raiiScope
@ -93,7 +114,6 @@ atomExpr
| periodicTask
| moduleDecl
| pathLiteral
| exceptionHandler
;
primary
@ -127,19 +147,16 @@ block
;
lambda
: LAMBDA pattern (IN expr)? COLON expr
: LAMBDA_VAR pattern (IN expr)? COLON expr
;
forall
: FORALL pattern IN expr COLON expr
;
conditional
: expr BAR expr // Simple conditional
;
// The | inside ⟨a|b⟩ is consumed by condExpr, so the rule needs no explicit BAR.
choiceType
: LANGLE expr BAR expr RANGLE
: LANGLE expr RANGLE
;
atomicSection
@ -170,15 +187,15 @@ pathLiteral
: PATH STRING
;
exceptionHandler
: expr HANDLE LBRACE (RAISE IDENTIFIER EXPORT expr)+ RBRACE
// Rewritten from the left-recursive, empty-tail form that caused error(148).
pattern
: patternAtom (COMMA patternAtom)*
;
pattern
patternAtom
: IDENTIFIER
| greekVar
| UNDERSCORE
| pattern (COMMA pattern)*
;
list
@ -244,7 +261,9 @@ BOOL : '𝔹' | '\\bool' | '\\B' ;
SEMICOLON : ';' ;
PARALLEL : '‖' | '\\parallel' ;
LEFTARROW : '←' | '\\leftarrow' | '\\gets' ;
IMPLIES : '⟹' | '\\implies' | '\\Rightarrow' ;
// '\Rightarrow' belongs to EXPORT (⇒); giving it to IMPLIES too fully
// shadowed EXPORT's escape (ANTLR warning 184).
IMPLIES : '⟹' | '\\implies' ;
OR : '' | '\\or' | '\\vee' ;
AND : '∧' | '\\and' | '\\wedge' ;
EQ : '=' ;
@ -270,7 +289,8 @@ BREAK : '⧈' | '\\break' ;
DELAY : '⏲' | '\\delay' ;
// Special operators
LAMBDA : 'λ' | '\\lambda' | '\\lam' ;
// (LAMBDA was fully shadowed by LAMBDA_VAR — warning 184; LAMBDA_VAR is the
// single λ token and the lambda parser rule uses it.)
FORALL : '∀' | '\\forall' ;
EXISTS : '∃' | '\\exists' ;
DEFINITION : '≜' | '\\coloneq' ;