Skip to content

USING.md — how to use this module

Cookbook for consuming this module's API from elsewhere in Theta. Largely derived from the source and verified against it, so it reads closer to code than to prose.

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

Using theta-grammar — parsing core objects from text

Counterpart of AGENTS.md. Use this module when you need to round-trip core exprs/stmts/types through text (e.g. persisting models or results). The text format is core's toString() output — you don't need a writer, expr.toString() is the writer.

implementation(project(":theta-grammar"))

// scope must hold the ORIGINAL Decl instances (Decl equality is identity!)
val symbolTable = SymbolTable()
decls.forEach { symbolTable.add(Symbol { it.name }) }   // see SimpleScope for the real pattern
val scope = SimpleScope(symbolTable)

val expr: Expr<out Type> = ExpressionWrapper(scope, exprText).instantiate(env)
val stmt: Stmt          = StatementWrapper(stmtText, scope).instantiate(env)
val type: Type          = TypeWrapper(typeText).instantiate()
  • Expr coverage is full-fidelity (quantifiers, bv/fp/arrays, deref); Stmt covers only skip/assign/memAssign/havoc/assume (+ ;-lists).
  • Parse errors throw (ThrowingErrorListener) instead of printing to stderr.
  • For human-authored model text, prefer core/dsl's CoreDslManager instead — this module's format is machine-oriented.

Reference consumers: xcfa/xcfa (Dsl.kt, XcfaLabel.kt). Round-trip examples: ExprTest.kt.