Term-constructor generators

Commands generating constructors for specification entries, either named one by one or every entry a specification module declares. They are meant to be invoked from per-theory modules, so that a user compiles only the theories and the layer they actually import.

-- in `Cvc.Untyped.Theory.BitVec`
namespace Cvc.Untyped.Term variable [Ω]
gen_untyped% from Cvc.Spec.BitVec

-- in `Cvc.Typed.Theory.BitVec`
namespace Cvc.Typed.Term open Cvc renaming Untyped.Term → T variable [Ω]
gen_typed% from Cvc.Spec.BitVec

gen_untyped% emits the sort-erased constructor, going straight to runUnsafe; gen_typed% emits the re-typed constructor, delegating to its untyped counterpart through the alias T. The alias keeps the generator independent of where the untyped constructors live.

Requirements on a generation site:

• both layers: import all Cvc.Basic.Env, since the emitted bodies use the private runUnsafe bridge;
• both layers: import all Cvc.Untyped.Core.Defs, since the term type's conversions are private;
• typed only: import all Cvc.Typed.Core.Defs, because delegation typechecks by Typed.Term α being definitionally Untyped.Term, and a plain import keeps that body opaque;
• typed only: an alias T bound to the untyped term namespace, as shown above.

Emitted names

Every name the generated code refers to is built with mkIdent rather than written literally inside a quotation. Identifiers written literally are resolved against this module's environment at quotation time, and this module deliberately imports neither layer, so such a reference would be emitted unresolved and fail at the generation site.

def Cvc.envId : Lean.Ident

Cvc.Env.

Equations

• Cvc.envId = Lean.mkIdent `Cvc.Env

def Cvc.runUnsafeId : Lean.Ident

runUnsafe, the private bridge into lean-cvc5.

Equations

• Cvc.runUnsafeId = Lean.mkIdent `runUnsafe

def Cvc.toTypId : Lean.Ident

Cvc.ToTyp.

Equations

• Cvc.toTypId = Lean.mkIdent `Cvc.ToTyp

def Cvc.untypedTermId : Lean.Ident

Cvc.Untyped.Term.

Equations

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

def Cvc.untypedTermsId : Lean.Ident

Cvc.Untyped.Terms.

Equations

• Cvc.untypedTermsId = Lean.mkIdent `Cvc.Untyped.Terms

def Cvc.typedTermId : Lean.Ident

Cvc.Typed.Term.

Equations

• Cvc.typedTermId = Lean.mkIdent `Cvc.Typed.Term

def Cvc.typedTermsId : Lean.Ident

Cvc.Typed.Terms.

Equations

• Cvc.typedTermsId = Lean.mkIdent `Cvc.Typed.Terms

def Cvc.on0Id : Lean.Ident

on0, what an N' variant answers for no term; not hygienic, so a caller can name it.

Equations

• Cvc.on0Id = Lean.mkIdent `on0

def Cvc.on1Id : Lean.Ident

on1, what an N' variant answers for one term; not hygienic, so a caller can name it.

Equations

• Cvc.on1Id = Lean.mkIdent `on1

def Cvc.srtId : Lean.Ident

Cvc.Srt.

Equations

• Cvc.srtId = Lean.mkIdent `Cvc.Srt

def Cvc.srtOfId : Lean.Ident

Cvc.Srt.of, which turns a Lean index into the sort it denotes.

Equations

• Cvc.srtOfId = Lean.mkIdent `Cvc.Srt.of

def Cvc.srtConId (id : Lean.Name) : Lean.Ident

The Cvc.Srt constructor of the given name.

Equations

• Cvc.srtConId id = Lean.mkIdent (`Cvc.Srt ++ id)

Building a sort from its element sorts

A constructor whose sort its arguments do not fix has to be handed one. It takes the sorts of its element type variables, never the sort of the term it builds — setEmpty takes the element sort, exactly as Lean's own ∅ : Set α is polymorphic in α. The sort cvc5's method wants is built from those here.

That sort is usually the result's, but not always: mkEmptySequence takes the element sort where mkEmptySet takes the set sort, which is what an entry's tmSortOf clause records.

partial def Cvc.Shape.buildSrt (ofVar : Lean.Name → Lean.MacroM (Lean.TSyntax `term)) : Shape → Lean.MacroM (Lean.TSyntax `term)

Emits an Env Srt expression building the sort a shape describes.

ofVar says where a type variable's sort comes from: a parameter for one the caller supplies, and an argument's getSort for one already fixed by an argument.

Rendering shapes as Lean types

partial def Cvc.SizeExpr.render (arityStx : Lean.TSyntax `term) : SizeExpr → Lean.MacroM (Lean.TSyntax `term)

Renders a size expression as a Nat-valued term.

partial def Cvc.Shape.render (arityStx : Lean.TSyntax `term) : Shape → Lean.MacroM (Lean.TSyntax `term)

Renders a sort shape as the Lean type indexing a Typed.Term.

Names are emitted fully qualified so that generation sites are free to sit in whichever namespace suits them. arityStx is what SizeExpr.arity renders to: a literal in a fixed-arity signature, the term array's size in an n-ary one.

Shared pieces

def Cvc.OpSpec.kindIdent (spec : OpSpec) : Lean.TSyntax `term

The cvc5.Kind constructor a specification builds its terms with.

Equations

• spec.kindIdent = { raw := (Lean.mkIdent (`cvc5 ++ `Kind ++ spec.kind)).raw }

def Cvc.OpSpec.naryId (spec : OpSpec) : Lean.Ident

Name of the n-ary variant of an operator: <id>N, or the spec's own choice.

Equations

• spec.naryId = Lean.mkIdent (spec.naryName.getD (spec.id.appendAfter "N"))

def Cvc.OpSpec.naryPrimeId (spec : OpSpec) : Lean.Ident

Name of the defaulting n-ary variant of an operator, the n-ary name primed.

Equations

• spec.naryPrimeId = Lean.mkIdent ((spec.naryName.getD (spec.id.appendAfter "N")).appendAfter "'")

def Cvc.OpSpec.naryDoc (spec : OpSpec) : String

Docstring for the N variant.

Equations

• spec.naryDoc = toString "`" ++ toString spec.id ++ toString "` over two or more terms."

def Cvc.OpSpec.primeDocOf (spec : OpSpec) (op : Lean.Name) (lifted overridable : Bool) : String

Docstring for an N' variant of op: what it answers for no term and for one.

lifted wraps the unit in some; overridable mentions the on0/on1 parameters that only the sort-erased variants take.

Equations

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

def Cvc.OpSpec.naryPrimeDoc (spec : OpSpec) (overridable : Bool) : String

Docstring for the N' variant; overridable for the sort-erased one, taking on0/on1.

Equations

• spec.naryPrimeDoc overridable = spec.primeDocOf spec.id false overridable

def Cvc.OpSpec.liftId (spec : OpSpec) : Lean.Ident

Name of the nullable-lifted operator: the operator's own, suffixed with ?.

Equations

• spec.liftId = Lean.mkIdent (spec.id.appendAfter "?")

def Cvc.OpSpec.liftNaryId (spec : OpSpec) : Lean.Ident

Name of the nullable-lifted n-ary operator.

Equations

• spec.liftNaryId = Lean.mkIdent ((Lean.TSyntax.getId spec.naryId).appendAfter "?")

def Cvc.OpSpec.liftDoc (spec : OpSpec) : String

Docstring for a lifted operator.

Equations

• spec.liftDoc = toString "`" ++ toString spec.id ++ toString "` lifted over nullables, **strictly**: `none` unless every argument is `some`."

def Cvc.OpSpec.liftNaryPrimeId (spec : OpSpec) : Lean.Ident

Name of the nullable-lifted defaulting n-ary operator.

Equations

• spec.liftNaryPrimeId = Lean.mkIdent ((Lean.TSyntax.getId spec.naryPrimeId).appendAfter "?")

def Cvc.OpSpec.liftNaryDoc (spec : OpSpec) : String

Docstring for a lifted n-ary operator.

Equations

• spec.liftNaryDoc = toString "`" ++ toString (Lean.TSyntax.getId spec.liftId) ++ toString "` over two or more terms."

def Cvc.OpSpec.liftNaryPrimeDoc (spec : OpSpec) (overridable : Bool) : String

Docstring for a lifted defaulting n-ary operator; overridable as for naryPrimeDoc.

Equations

• spec.liftNaryPrimeDoc overridable = spec.primeDocOf (Lean.TSyntax.getId spec.liftId) true overridable

def Cvc.OpSpec.unitOn1Default (spec : OpSpec) (unitTerm : Lean.TSyntax `term) : Lean.MacroM (Lean.TSyntax `term)

The default an N' variant answers for a single term, given the unit's term.

The term itself, for an operation whose result has its arguments' sort (addN' #[t] is t); the unit for a relation (equalN' #[t] is true), whose single term has the wrong sort.

Equations

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

def Cvc.arithUnitAt (type : Lean.TSyntax `term) (i : Int) : Lean.MacroM (Lean.TSyntax `term)

An integer unit as a sort-erased term at the sort of type, an arithmetic Lean type.

The sort-erased N' variants build their unit with mkInt, having no sort to go by; the typed ones know theirs, and pass the unit at it.

Equations

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

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

Creates a docComment node from a docstring.

Equations

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

def Cvc.getOpSpec (id : Lean.Ident) : Lean.Elab.Command.CommandElabM OpSpec

Looks a specification up, failing with a located error if it is not registered.

Equations

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

Untyped generation

def Cvc.genUntyped (spec : OpSpec) : Lean.MacroM (Array (Lean.TSyntax `command))

Emits the sort-erased constructors for one specification entry.

Every argument and the result erase to Untyped.Term, so the shapes play no part beyond fixing the arity: a pure operator kind infers its sort from its arguments, which op% checks.

Equations

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

Nullable lifting, sort-erased

nullable.lift applies an operator to the values inside its nullable arguments, answering none unless every one of them is some. It takes a Kind and the terms, so the lifted body is shorter than the plain one — there is no sort to build and no Op to make.

Arity is right by construction here, which it would not be if a Kind were exposed to a caller: cvc5 validates nothing, and mkNullableLift .NOT #[x, y] cheerfully builds the malformed (nullable.lift (lambda (a b) (not a b)) x y). Generating from the specification means the argument count and the n-ary form both come from the entry that already knows them.

def Cvc.genUntypedNullable (spec : OpSpec) : Lean.MacroM (Array (Lean.TSyntax `command))

Emits the sort-erased nullable-lifted constructors for one entry, if it has any.

Equations

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

def Cvc.emitUntypedNullable (spec : OpSpec) : Lean.Elab.Command.CommandElabM Unit

Emits the sort-erased lifted constructors for one entry.

Equations

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

def Cvc.genUntypedNullableStx : Lean.ParserDescr

Generates the sort-erased lifted constructors for the named entries.

Equations

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

def Cvc.genUntypedNullableFromStx : Lean.ParserDescr

Generates the sort-erased lifted constructors for every entry a module declares.

Equations

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

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

Equations

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

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

Equations

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

DSL grammar generation

The smtTerm grammar rule of an operator is emitted alongside its untyped constructor, and only there: the typed constructors delegate to the untyped ones, so a typed theory module always imports its untyped counterpart and inherits the grammar. Emitting from both layers would declare the same rule twice.

Rules are named smtOp.<shape>.<id>, which under the enclosing namespace becomes …Term.smtOp.binary.and and so on. Cvc.Ext.expandSmt dispatches on those trailing three components, so it needs no knowledge of where generation happened.

def Cvc.smtRuleId (shape id : Lean.Name) : Lean.Ident

Name of an operator's generated grammar rule, relative to the generation site's namespace.

Equations

• Cvc.smtRuleId shape id = Lean.mkIdent (`smtOp ++ shape ++ id)

def Cvc.genSmtSyntax (spec : OpSpec) : Lean.MacroM (Array (Lean.TSyntax `command))

Emits the smtTerm grammar rules for one specification entry's notation.

Equations

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

def Cvc.emitUntyped (spec : OpSpec) : Lean.Elab.Command.CommandElabM Unit

Emits the sort-erased constructors, and the DSL grammar, for one entry.

Equations

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

def Cvc.genUntypedStx : Lean.ParserDescr

Generates the sort-erased constructors for the named specification entries.

Equations

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

def Cvc.genUntypedFromStx : Lean.ParserDescr

Generates the sort-erased constructors for every entry a specification module declares.

Equations

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

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

Equations

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

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

Equations

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

Typed generation

def Cvc.typedBinders (spec : OpSpec) : Lean.MacroM (Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder))

Emits the binders a typed constructor needs: type, size, Ord and refinement classes.

A type variable carrying refinement classes also gets a ToTyp binder, since a refinement such as IsArith is stated over the variable's Typ and so takes ToTyp as an instance argument.

Equations

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

def Cvc.genTyped (spec : OpSpec) : Lean.MacroM (Array (Lean.TSyntax `command))

Emits the re-typed constructors for one specification entry, delegating to the untyped ones.

Equations

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

def Cvc.emitTyped (spec : OpSpec) : Lean.Elab.Command.CommandElabM Unit

Emits the re-typed constructors for one entry.

Equations

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

def Cvc.genTypedStx : Lean.ParserDescr

Generates the re-typed constructors for the named specification entries.

Equations

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

def Cvc.genTypedFromStx : Lean.ParserDescr

Generates the re-typed constructors for every entry a specification module declares.

Equations

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

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

Equations

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

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

Equations

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

Nullable lifting, typed

Every term argument and the result gain an Option; everything else is the plain operator's signature unchanged — type and size variables, Ord binders, and the refinement classes. The body delegates, as the plain typed constructors do.

Option (Option α) needs no special case: add? at α := Option Int would demand IsArith (Option Int), and no such instance exists.

def Cvc.genTypedNullable (spec : OpSpec) : Lean.MacroM (Array (Lean.TSyntax `command))

Emits the re-typed nullable-lifted constructors for one entry, if it has any.

Equations

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

def Cvc.emitTypedNullable (spec : OpSpec) : Lean.Elab.Command.CommandElabM Unit

Emits the re-typed lifted constructors for one entry.

Equations

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

def Cvc.genTypedNullableStx : Lean.ParserDescr

Generates the re-typed lifted constructors for the named entries.

Equations

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

def Cvc.genTypedNullableFromStx : Lean.ParserDescr

Generates the re-typed lifted constructors for every entry a module declares.

Equations

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

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

Equations

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

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

Equations

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