Parser Implementation Notes

This page documents where the ANTLR4 grammar (modules/parser/src/main/antlr4/Spec.g4) diverges from the EBNF specification and the reasoning behind each deviation.

Keyword-as-identifier problem

The EBNF assumes identifiers and keywords are context-free: output in output.url is just an identifier.

ANTLR4's lexer is context-independent. Once output is defined as the OUTPUT keyword token, it is always lexed as OUTPUT, never as LOWER_IDENT. This means Resolve.http_header "Location" = output.url fails because the parser sees OUTPUT where it expects an expression identifier.

The fix is a lowerIdent parser rule that accepts LOWER_IDENT and all keywords that may appear in identifier positions:

lowerIdent
    : LOWER_IDENT
    | INPUT | OUTPUT | FIELD | STATE
    | ONE | LONE | SET_MULT
    | VIA | WHEN | WHERE | WITH | EXTENDS
    | REQUIRES | ENSURES
    | ENTITY | OPERATION | TRANSITION | INVARIANT | FACT
    | CONVENTIONS | FUNCTION | PREDICATE | TYPE | ENUM | IMPORT
    | SERVICE
    ;

This rule is used everywhere the EBNF says LOWER_IDENT: field declarations, parameter names, state fields, convention properties, expression identifiers, quantifier bindings, let/lambda variable names, and field access (.field).

The cost is that every keyword becomes a valid identifier, which is overly permissive at the grammar level. Semantic analysis (a later phase) should reject nonsensical uses like naming a field service.

set multiplicity vs Set[T] type

In the EBNF, set (lowercase) is a multiplicity keyword and Set (uppercase) is the parameterized collection type. The EBNF treats them as separate tokens implicitly.

In ANTLR4, the SET keyword is defined as 'Set' (uppercase S). Lowercase set in Int -> set String gets lexed as LOWER_IDENT, which doesn't match the multiplicity rule.

The fix is a separate lexer token SET_MULT: 'set' for the lowercase multiplicity, distinct from SET: 'Set' for the type constructor. The multiplicity rule uses SET_MULT:

multiplicity: ONE | LONE | SOME | SET_MULT ;

Newline handling in requires/ensures

The EBNF spec writes expr_list = expr { NEWLINE expr }: newlines are significant separators between top-level expressions in requires: and ensures: blocks.

In the ANTLR4 implementation, all whitespace (including newlines) goes to channel(HIDDEN). The blocks use expr+ instead of newline-delimited lists.

This works because expressions in this DSL are self-delimiting; there is no juxtaposition or implicit application operator. After parsing one complete expression, the next token is either:

• A binary operator (and, +, =, etc.) -> continues the current expression
• An identifier, keyword, or prefix operator (#, -, not, all, etc.) -> starts a new expression

Since two expressions side-by-side without an operator between them cannot form a valid larger expression, ANTLR4's greedy expr+ naturally splits them at the right boundaries.

For example:

ensures:
  code not in pre(store)         <- expr 1: comparison
  store' = pre(store) + {code -> url}   <- expr 2: equality

After pre(store), the next token store is an identifier with no infix operator preceding it, so the parser terminates expr 1 and starts expr 2.

The risk: if the DSL ever adds a juxtaposition operator (e.g., implicit function application), this approach breaks. The fallback would be reintroducing a NEWLINE token on a separate channel and using it as an explicit separator.

Regex literals vs division operator

The EBNF spec defines both REGEX_LIT (/pattern/) and division (/). This creates a classic lexer ambiguity: a / b / c could be tokenized as division or as a regex literal.

The fix is a lexer predicate that restricts REGEX_LIT to match only immediately after the MATCHES keyword. All other / tokens are lexed as SLASH (division).

The lexer tracks the most recent non-hidden token type via an overridden nextToken():

@lexer::members {
private lastNonWsType: number = -1;

public override nextToken(): antlr.Token {
    const token = super.nextToken();
    if (token.channel === 0) {
        this.lastNonWsType = token.type;
    }
    return token;
}
}

REGEX_LIT
    : {this.lastNonWsType === SpecLexer.MATCHES}? '/' ~[/\r\n]+ '/'
    ;

This means value matches /^[a-z]+$/ correctly lexes the regex, while a / b / c produces three tokens: a SLASH b SLASH c.

Error listener wiring

ANTLR's default listeners print to stderr and don't fail the parse. We collect parse errors into List[ParseError] and surface them as VerifyError.Parse by overriding BaseErrorListener on both the lexer and the parser, after first removing the defaults:

val listener: BaseErrorListener = new BaseErrorListener:
  override def syntaxError(
      recognizer: Recognizer[?, ?],
      offendingSymbol: Any,
      line: Int,
      column: Int,
      msg: String,
      e: RecognitionException
  ): Unit =
    errors += ParseError(line, column, msg)

lexer.removeErrorListeners()
parser.removeErrorListeners()
lexer.addErrorListener(listener)
parser.addErrorListener(listener)

The Scala 3 wildcard Recognizer[?, ?] matches the Java runtime's Recognizer<?, ?> raw generic; offendingSymbol: Any covers the Object parameter that may be a Token (parser) or null (lexer). See modules/parser/src/main/scala/specrest/parser/Parse.scala.

Grammar compilation

Parser generation is driven by the sbt-antlr4 plugin: placing the grammar at modules/parser/src/main/antlr4/Spec.g4 is enough. sbt parser/compile generates Java lexer / parser / visitor classes into src_managed/main/antlr4/specrest/parser/generated/ at the package configured in build.sbt:

Antlr4 / antlr4Version     := "4.13.2"
Antlr4 / antlr4PackageName := Some("specrest.parser.generated")
Antlr4 / antlr4GenVisitor  := true

No hand-run CLI is needed; the generated Java sources are invisible to developers and refreshed automatically whenever Spec.g4 changes.

Expression precedence strategy

The EBNF approach uses 10+ separate named rules (or_expr, and_expr, not_expr, etc.) forming a precedence chain.

The ANTLR4 approach uses a single left-recursive expr rule with labeled alternatives. ANTLR4 assigns implicit precedence by alternative order: the first alternative binds tightest (highest precedence), the last binds loosest. The alternatives are ordered accordingly:

Alternative order in grammar (first = tightest):
1. postfix (', ., [], ())
2. with (record update)
3. unary prefix (#, -, ^)
4. multiplicative (*, /)
5. additive (+, -)
6. set operations (union, intersect, minus)
7. comparisons (=, !=, <, >, <=, >=, in, not in, subset, matches)
8. not (unary)
9. and
10. or
11. implies, iff
12. primaries (literals, identifiers, quantifiers, not left-recursive, no precedence)

The two top-level structural rules render as:

Regenerate the SVGs with node docs/scripts/build-railroad.mjs whenever the grammar changes.

An early mistake: the first version of the grammar had the order inverted (or first, postfix last). This produced correct parse acceptance (all tests passed) but incorrect parse trees: a + b * c would have been parsed as (a + b) * c. The review caught this because the tests only asserted zero errors, not tree structure.

This is more concise than the EBNF chain and uses ANTLR4's native left-recursion elimination.

some disambiguation

The ambiguity is some(expr) (Option wrapper) vs some x in S | P (existential quantifier).

The EBNF uses separate rules some_wrap_expr and quantifier_expr.

In ANTLR4, the someWrapExpr sub-rule and the quantifierExpr sub-rule are both referenced from the expr rule's primary alternatives. ANTLR4's ALL(*) adaptive prediction resolves the ambiguity by lookahead:

• some ( -> matches someWrapExpr: SOME LPAREN expr RPAREN
• some identifier in -> matches quantifierExpr with SOME as the quantifier

No semantic predicates are needed; the syntactic structure is sufficient.