Skip to content

AGENTS.md — how to modify this module

Invariants, conventions and change recipes for contributors — and for AI coding assistants, which load this file automatically when editing the module. Largely derived from the source and verified against it.

Mirrored from subprojects/common/grammar/AGENTS.md — edit it there, not here.

common/grammar — notes for editing this module

Gradle module: :theta-grammar. Kotlin + ANTLR (grammars in src/main/antlr/: CommonTokens.g4, Type.g4, Expr.g4, Stmt.g4, Declarations.g4).

What this module is: the parser for core's own toString() output. Core exprs/stmts/types print in lisp style (Utils.lispStringBuilder); this module parses that text back into core objects — verified round-trip in ExprTest/StmtTest (assertEquals(serialized, expr.toString()), then re-parse).

Of the repo's three text stacks for core objects, this is the machine round-trip one: core/dsl (CoreDslManager) is for human-written models, core/parser is legacy Lisp with no production consumers, and this module is what xcfa uses to restore exprs/stmts from text.

Invariants

  1. The grammar must track core's toString() exactly. A new expr class (or a changed OPERATOR_LABEL) in core silently breaks the round-trip until Expr.g4 + ExprParser.kt's ExprCreatorVisitor learn it — there is no compile-time coupling. The round-trip tests are the only guard; extend them with every grammar change.
  2. Expr.g4 is full-fidelity (~45 rules: quantifiers, ite, arrays, bv, fp, deref, func lits). Stmt.g4 is not: skip/assign/memAssign/havoc/assume + ;-separated stmtList only — no composite stmts (Sequence/NonDet/Loop/If/Ort as objects; xcfa doesn't need them since XCFA edges carry label lists).
  3. Parsing is scope-dependent: wrappers take a Scope (SimpleScope) mapping names → Decl symbols, and instantiate against an Env — same Decl-identity rules as everywhere (names don't resurrect decls; the scope must hold the original instances).
  4. ANTLR generated sources land under build/ at build time — edit only the .g4 files; parser/visitor base classes regenerate.

Change recipes

  • Core gained a new expr/type: add the rule to the .g4, a visit... override in the matching *CreatorVisitor (Expr/Type/Stmt Parser.kt), and a round-trip test case. Check the label matches core's OPERATOR_LABEL verbatim.

Files

  • dsl/ — ExpressionWrapper/StatementWrapper/TypeWrapper (lazy: hold text + scope, instantiate(env) parses), SimpleScope, Utils.kt (textWithWS, ThrowingErrorListener — parse errors throw instead of printing).

Consumers: xcfa/xcfa (Dsl.kt, XcfaLabel.kt). (c-frontend/btor2-frontend declare the dep but don't use it — see possible-issues.md.)