Generating a symbols structure

structure.symbols writes the boilerplate a Symbols instance needs. A user states the symbols they want and the Lean type each denotes:

structure.symbols MySymbols where
  /-- Whether the thing is on. -/
  isOn : Bool
  count : Int

and what is generated is the structure the Symbols class actually wants — parameterized by the Wrap, with every field wrapped in it — plus one alias per Symbols.Sig type (Idents, Terms, Values, …), the idents naming each symbol, and the instance:

structure MySymbols (W : Symbols.Wrap) where
  isOn : W Bool
  count : W Int

A symbol's name is its field's name, as a string. declare, getValues and findCex are generic over the Sig, so nothing beyond the instance is needed for them.

This module holds what both layers share. Each layer declares its own scoped spelling of the command, so open Cvc.Untyped selects the sort-erased one exactly as it selects smt!.

def Cvc.Ext.symbolsReserved : Array Lean.Name

Names generated or reached beside a symbols structure other than its aliases, which a symbol therefore cannot be called.

Equations

• Cvc.Ext.symbolsReserved = #[`idents, `mapM, `foldM, `declare, `declareIn, `getValues, `findCex, `TermTrace, `ValueTrace, `ValueTermTrace]

def Cvc.Ext.symbolsTraceAliases : Array (Lean.Name × Bool)

The traces of Cvc.{Untyped,Typed}.Extra.Sys, aliased beside a symbols structure where that module is imported, each with whether it takes the scope.

Equations

• Cvc.Ext.symbolsTraceAliases = #[(`TermTrace, true), (`ValueTrace, false), (`ValueTermTrace, true)]

def Cvc.Ext.symbolsSharedAliases : Array (Lean.Name × Bool)

The aliases of Symbols.Sig both layers generate beside a symbols structure, with the same parameters in both, each with whether it takes the scope. A layer's own aliases are its extras.

Equations

• Cvc.Ext.symbolsSharedAliases = #[(`Idents, false), (`Values, false), (`ValuesAt, false), (`Terms, true), (`TermsAt, true), (`BVars, true), (`ValueTerms, true), (`ValueTermsAt, true)]

def Cvc.Ext.foldChain {m : Type → Type} [Monad m] [Lean.MonadQuotation m] (fields : Array Lean.Name) : m (Lean.TSyntax `term)

The body of a generated foldM syms acc f: f acc syms.a >>= fun acc => f acc syms.b >>= …, over the given fields in order.

Equations

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

def Cvc.Ext.mkSymbolsStructure (doc? : Option Lean.Syntax) (id w wrap : Lean.Syntax) (binders : Array Lean.Syntax) : Lean.Syntax

structure <id> (<w> : <wrap>) where <binders>, with doc? as its doc comment.

Equations

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

def Cvc.Ext.wrapSymbolsField (w : Lean.Ident) (field : Lean.TSyntax `Lean.Parser.Command.structSimpleBinder) : Lean.Elab.Command.CommandElabM Lean.Syntax

One field, rebuilt with its type wrapped in w.

Everything the writer wrote — the doc comment, the name, the source position — is carried over untouched; only the type is replaced, by w applied to it.

Equations

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

def Cvc.Ext.elabSymbols (root : Lean.Name) (extras : Array (Lean.Name × Bool)) (doc? : Option (Lean.TSyntax `Lean.Parser.Command.docComment)) (id : Lean.Ident) (fields : Array (Lean.TSyntax `Lean.Parser.Command.structSimpleBinder)) : Lean.Elab.Command.CommandElabM Unit

Emits a symbols structure and everything generated beside it.

root is the layer's namespace, and extras the aliases only that layer has, beside the shared symbolsSharedAliases, each with whether it takes the scope. Every alias is Symbols.Sig.<name> applied to the structure, so its own parameters — a sort, a depth — stay those of the definition.

Equations

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