Generating views

A view takes a term apart one level: its operator, as a constructor, and its kids. Each theory has its own view, generated from its specification beside its constructors — or, for what no specification describes, written by hand and registered — and def.term_view V gathers the views of every theory the current module imports into one inductive.

• gen_untyped_view% from <Spec module> generates a theory's sort-erased view, an inductive with one constructor per operator, and its viewer of?, then registers it.
• register_untyped_view% <View> [ctor KIND, …] registers a hand-written one.
• def.untyped_term_view V — def.term_view V under open Cvc.Untyped — generates the aggregate V: the leaves, a variant of<Theory> per registered view, a catch-all other, one @[match_pattern] abbreviation per operator so that a pattern can skip the theory, a viewer V.of, and a TermView instance.

Which theories def.term_view gathers is decided by the registry, which holds exactly the views of the modules imported: importing a theory is what makes its operators visible.

Like Cvc.Gen.Term, this module imports neither layer: every name the generated code mentions is built with mkIdent, fully qualified.

The registry

structure Cvc.UntypedView : Type

A registered sort-erased view.

• theory : Lean.Name

  The theory, Arith: the aggregate's variant holding the view is ofArith.

• view : Lean.Name

  The view's inductive.

• ctors : Array (Lean.Name × Lean.Name)

  Each constructor, and the kind it owns.

• skipped : Array (Lean.Name × String)

  The specification's entries the view has no constructor for, and why.

@[instance_reducible]

instance Cvc.instInhabitedUntypedView : Inhabited UntypedView

Equations

• Cvc.instInhabitedUntypedView = { default := Cvc.instInhabitedUntypedView.default }

opaque Cvc.untypedViewExt : Lean.SimplePersistentEnvExtension UntypedView (Array UntypedView)

The registered sort-erased views, imported ones included.

def Cvc.untypedViews {m : Type → Type} [Monad m] [Lean.MonadEnv m] : m (Array UntypedView)

Every registered sort-erased view.

Equations

• Cvc.untypedViews = do let __do_lift ← Lean.getEnv pure (Cvc.untypedViewExt.getState __do_lift)

Emitted names

Built with mkIdent and spliced, never written in a quotation: a name written there resolves against this module's environment, which imports neither layer.

def Cvc.viewTermId : Lean.Ident

Cvc.Untyped.Term.

Equations

• Cvc.viewTermId = Lean.mkIdent `Cvc.Untyped.Term

def Cvc.viewKidsId : Lean.Ident

Cvc.Untyped.Kids.

Equations

• Cvc.viewKidsId = Lean.mkIdent `Cvc.Untyped.Kids

def Cvc.viewKidsOfId : Lean.Ident

Cvc.Untyped.Kids.of?.

Equations

• Cvc.viewKidsOfId = Lean.mkIdent `Cvc.Untyped.Kids.of?

def Cvc.viewGetKidsId : Lean.Ident

Cvc.Untyped.Term.getKids.

Equations

• Cvc.viewGetKidsId = Lean.mkIdent `Cvc.Untyped.Term.getKids

def Cvc.viewGetKindId : Lean.Ident

Cvc.Untyped.Term.getKind?.

Equations

• Cvc.viewGetKindId = Lean.mkIdent `Cvc.Untyped.Term.getKind?

def Cvc.viewIndexAtId : Lean.Ident

Cvc.Untyped.Term.indexAt?.

Equations

• Cvc.viewIndexAtId = Lean.mkIdent `Cvc.Untyped.Term.indexAt?

def Cvc.viewGetSymbolId : Lean.Ident

Cvc.Untyped.Term.getSymbol.

Equations

• Cvc.viewGetSymbolId = Lean.mkIdent `Cvc.Untyped.Term.getSymbol

def Cvc.viewBVarId : Lean.Ident

Cvc.Untyped.BVar.

Equations

• Cvc.viewBVarId = Lean.mkIdent `Cvc.Untyped.BVar

def Cvc.viewAsBVarId : Lean.Ident

Cvc.Untyped.Term.asBVar.

Equations

• Cvc.viewAsBVarId = Lean.mkIdent `Cvc.Untyped.Term.asBVar

def Cvc.viewTermViewId : Lean.Ident

Cvc.Untyped.TermView.

Equations

• Cvc.viewTermViewId = Lean.mkIdent `Cvc.Untyped.TermView

def Cvc.viewKindId (k : Lean.Name) : Lean.Ident

cvc5.Kind.<k>.

Equations

• Cvc.viewKindId k = Lean.mkIdent (`cvc5.Kind ++ k)

def Cvc.viewValueKinds : Array Lean.Name

The kinds of values: the leaves own them, so no view does.

Equations

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

def Cvc.viewDoc (s : String) : Lean.TSyntax `Lean.Parser.Command.docComment

A docstring node.

Equations

• Cvc.viewDoc s = Lean.mkNode `Lean.Parser.Command.docComment #[Lean.mkAtom "/--", Lean.mkAtom (s ++ " -/")]

def Cvc.viewCtorDoc (spec : OpSpec) (nary : Bool) : String

A view constructor's docstring: its entry's, plus where the operands are when nary.

Equations

• Cvc.viewCtorDoc spec nary = if nary = true then spec.doc ++ "\n\n`kids` holds every operand, two or more." else spec.doc

A theory's sort-erased view

@[reducible, inline]

abbrev Cvc.ViewCtor : Type

A view's constructor, and its viewer's alternative.

Equations

• Cvc.ViewCtor = (Lean.TSyntax `Lean.Parser.Command.ctor × Lean.TSyntax `Lean.Parser.Term.matchAlt)

def Cvc.genUntypedCtor (spec : OpSpec) (view : Lean.Name) : Lean.MacroM (Except String ViewCtor)

One entry's constructor in its theory's view, and the viewer's alternative for it.

Equations

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

def Cvc.genUntypedViewStx : Lean.ParserDescr

Generates and registers a theory's sort-erased view from its specification module.

Equations

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

def Cvc.elabGenUntypedView : Lean.Elab.Command.CommandElab

Equations

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

def Cvc.registerUntypedViewStx : Lean.ParserDescr

Registers a hand-written sort-erased view: its inductive, and each constructor with the kind it owns. The theory is the inductive's last component.

Equations

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

def Cvc.elabRegisterUntypedView : Lean.Elab.Command.CommandElab

Equations

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

def Cvc.untypedViewsStx : Lean.ParserDescr

Lists the registered sort-erased views: each theory, how many operators it takes apart, and the specification entries it has no constructor for.

Equations

• Cvc.untypedViewsStx = Lean.ParserDescr.node `Cvc.untypedViewsStx 1024 (Lean.ParserDescr.symbol "#untyped_views")

def Cvc.elabUntypedViews : Lean.Elab.Command.CommandElab

Equations

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

The sort-erased aggregate

def Cvc.theoryVariant (theory : Lean.Name) : Lean.Name

The aggregate's variant holding a theory's view: ofArith, which no operator's name can clash with.

Equations

• Cvc.theoryVariant theory = Lean.Name.mkSimple (toString "of" ++ toString theory)

def Cvc.untypedTermViewStx : Lean.ParserDescr

Generates the sort-erased aggregate V from every registered view.

Equations

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

def Cvc.elabUntypedTermView : Lean.Elab.Command.CommandElab

Equations

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

def Cvc.Untyped.«commandDef.term_view_» : Lean.ParserDescr

Declares V, a sort-erased term taken apart one level, over every theory imported.

V.of t takes t apart; a match on it names operators directly (.add kids, .ite c a b), the leaves .value, .symbol and .bvar, or .other for a term no imported theory takes apart. Needs variable [Ω] in scope.

Equations

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