Implements the #strata_gen command, which reads a dialect definition and generates Lean inductive types, toAst, and ofAst functions for each category used by the dialect.

Category Classification

The generator classifies Init categories into several sets that control how code is generated:

• declaredCategories — Primitive Init categories (e.g., Init.Num, Init.Ident) that map directly to existing Lean types (e.g., Nat, String). No inductive type is generated for these; they appear as-is in constructor fields.

• forbiddenCategories — Internal machinery categories (e.g., Init.BindingType, StrataDDL.Binding) that dialects must not reference in generated code. An error is reported if a dialect operation uses one.

• abstractCategories — The abstract extension points Init.Expr, Init.Type, and Init.TypeP. Init-defined operators for these are ignored; instead they are populated via fn/type declarations and augmented with builtin constructors (see makeBuiltinCtors). Non-Init dialects are prevented from adding operators to these categories by the check in addDecl.

• reservedCategories — Category names that would shadow Lean keywords (currently just "Type"). These are prefixed with the dialect name in generated identifiers.

def StrataDDM.strataGenCmd : Lean.ParserDescr

#strata_gen ident generates an AST for the dialect ident.

This includes functions for converting from the standard AST to the generated AST and back.

Equations

• StrataDDM.strataGenCmd = Lean.ParserDescr.node `StrataDDM.strataGenCmd 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#strata_gen") (Lean.ParserDescr.const `ident))

def StrataDDM.genAstImpl : Lean.Elab.Command.CommandElab

Equations

• One or more equations did not get rendered due to their size.