Datatypes, typed

A declared datatype is used at a Lean index. Give a Lean type a ToTyp instance naming the datatype, declare the datatype in the scope (Srt.datatype, Solver.declareDatatype), and Term Lst is a term like any other:

structure Lst where private mk ::
instance : ToTyp Lst := ⟨.datatype "Lst"⟩

-- in `Env`, once `Lst := nil | cons (head : Int) (tail : Lst)` is declared
let cons ← Datatype.ctor Lst "cons"      -- `Ctor Lst`
let nil ← Datatype.ctor Lst "nil"
let head ← cons.field Int "head"         -- `Field Lst Int`
let l ← cons.apply2 (← Term.mkInt 1) (← nil.apply)
let h ← head.get l                       -- `Term Int`

Which constructors a datatype has, and the sorts of their fields, are facts about its declaration: Datatype.ctor and Ctor.field look a name up and check the sorts once, and the Ctor α or Field α β they answer carries the index from there on.

@[reducible, inline]

abbrev Cvc.Typed.Datatype.Args [Ω] : Type 1

The constructor arguments of one application, each carrying its own index.

Equations

• Cvc.Typed.Datatype.Args = List ((β : Type) × Cvc.ToTyp β × Cvc.Typed.Term β)

@[reducible, inline]

abbrev Cvc.Typed.Datatype.Args.nil [Ω] : Args

No arguments.

Equations

• Cvc.Typed.Datatype.Args.nil = []

@[reducible, inline]

abbrev Cvc.Typed.Datatype.Args.cons [Ω] {β : Type} [ToTyp β] (arg : Term β) (rest : Args) : Args

Adds an argument in front of the ones collected so far: .cons a (.cons b .nil) is a, b.

Equations

• Cvc.Typed.Datatype.Args.cons arg rest = ⟨β, (inferInstance, arg)⟩ :: rest

def Cvc.Typed.Datatype.Args.toUntyped [Ω] (args : Args) : Untyped.Terms

The sort-erased terms, in field order.

Equations

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

@[reducible, inline]

abbrev Cvc.Typed.Datatype.Args.erase [Ω] (args : Args) : Untyped.Terms

The sort-erased terms, in field order.

Equations

• @Cvc.Typed.Datatype.Args.erase = @Cvc.Typed.Datatype.Args.toUntyped

structure Cvc.Typed.Datatype.Ctor [Ω] (α : Type) : Type

A datatype constructor, at the index of the datatype it builds.

• ctor : Cvc.Datatype.Ctor
• term : Cvc.Untyped.Term
• tester : Cvc.Untyped.Term

structure Cvc.Typed.Datatype.Field [Ω] (α β : Type) : Type

One field of a datatype constructor, at the datatype's index and the field's.

The typed counterpart of the selector Cvc.Datatype.Selector, which reflects a field sort-erased.

• sel : Cvc.Datatype.Selector
• term : Cvc.Untyped.Term
• updater : Cvc.Untyped.Term

def Cvc.Typed.Datatype.reflect [Ω] (α : Type) [ToTyp α] : Env Datatype

The datatype the index names, reflected.

Fails if nothing has been declared under that name in this scope.

Equations

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

def Cvc.Typed.Datatype.ctor [Ω] (α : Type) [ToTyp α] (name : String) : Env (Ctor α)

The constructor of the given name.

Equations

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

def Cvc.Typed.Datatype.Ctor.toUntyped [Ω] {α : Type} (c : Ctor α) : Cvc.Datatype.Ctor

The sort-erased constructor it reflects, for free.

Equations

• c.toUntyped = Cvc.Typed.Datatype.Ctor.ctor✝ c

@[reducible, inline]

abbrev Cvc.Typed.Datatype.Ctor.erase [Ω] {α : Type} (c : Ctor α) : Cvc.Datatype.Ctor

The sort-erased constructor it reflects, for free.

Equations

• c.erase = c.toUntyped

def Cvc.Datatype.Ctor.toTypedAs [Ω] (α : Type) [ToTyp α] (c : Ctor) : Env (Typed.Datatype.Ctor α)

Types a reflected constructor at the datatype α, checking that α is what it builds.

The reflection counterpart of Datatype.ctor, which looks a constructor up by name. A constructor of a parametric datatype read off the uninstantiated declaration builds the parametric sort, not an instance of it, and is refused. toTyped infers α from the expected type; typeCheckAs and typeCheck are the same two functions under the names that say what they do.

Equations

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

def Cvc.Datatype.Ctor.toTyped [Ω] {α : Type} [ToTyp α] (c : Ctor) : Env (Typed.Datatype.Ctor α)

Types a reflected constructor at the datatype α, checking that α is what it builds.

The reflection counterpart of Datatype.ctor, which looks a constructor up by name. A constructor of a parametric datatype read off the uninstantiated declaration builds the parametric sort, not an instance of it, and is refused. toTyped infers α from the expected type; typeCheckAs and typeCheck are the same two functions under the names that say what they do.

Equations

• c.toTyped = Cvc.Datatype.Ctor.toTypedAs α c

@[reducible, inline]

abbrev Cvc.Datatype.Ctor.typeCheckAs [Ω] (α : Type) [ToTyp α] (c : Ctor) : Env (Typed.Datatype.Ctor α)

Types a reflected constructor at the datatype α, checking that α is what it builds.

The reflection counterpart of Datatype.ctor, which looks a constructor up by name. A constructor of a parametric datatype read off the uninstantiated declaration builds the parametric sort, not an instance of it, and is refused. toTyped infers α from the expected type; typeCheckAs and typeCheck are the same two functions under the names that say what they do.

Equations

• @Cvc.Datatype.Ctor.typeCheckAs = @Cvc.Datatype.Ctor.toTypedAs

@[reducible, inline]

abbrev Cvc.Datatype.Ctor.typeCheck [Ω] {α : Type} [ToTyp α] (c : Ctor) : Env (Typed.Datatype.Ctor α)

Types a reflected constructor at the datatype α, checking that α is what it builds.

The reflection counterpart of Datatype.ctor, which looks a constructor up by name. A constructor of a parametric datatype read off the uninstantiated declaration builds the parametric sort, not an instance of it, and is refused. toTyped infers α from the expected type; typeCheckAs and typeCheck are the same two functions under the names that say what they do.

Equations

• @Cvc.Datatype.Ctor.typeCheck = @Cvc.Datatype.Ctor.toTyped

def Cvc.Typed.Datatype.Ctor.getName {α : Type} [Ω] (c : Ctor α) : Res String

The constructor's name.

Equations

• c.getName = (Cvc.Typed.Datatype.Ctor.ctor✝ c).getName

def Cvc.Typed.Datatype.Ctor.countFields {α : Type} [Ω] (c : Ctor α) : Nat

How many fields the constructor takes.

Equations

• c.countFields = (Cvc.Typed.Datatype.Ctor.ctor✝ c).countSelectors

def Cvc.Typed.Datatype.Ctor.fieldSorts {α : Type} [Ω] (c : Ctor α) : Env Srts

The sorts of the constructor's fields, in order.

Equations

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

def Cvc.Typed.Datatype.Ctor.apply {α : Type} [Ω] (c : Ctor α) (args : Args := Args.nil) : Env (Term α)

Applies the constructor, failing unless its arguments' number and sorts are its fields'.

Equations

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

def Cvc.Typed.Datatype.Ctor.apply1 {α : Type} [Ω] (c : Ctor α) {β₁ : Type} [ToTyp β₁] (fst : Term β₁) : Env (Term α)

Applies the constructor, failing unless its arguments' number and sorts are its fields'.

Equations

• c.apply1 fst = c.apply (Cvc.Typed.Datatype.Args.cons fst Cvc.Typed.Datatype.Args.nil)

def Cvc.Typed.Datatype.Ctor.apply2 {α : Type} [Ω] (c : Ctor α) {β₁ β₂ : Type} [ToTyp β₁] [ToTyp β₂] (fst : Term β₁) (snd : Term β₂) : Env (Term α)

Applies the constructor, failing unless its arguments' number and sorts are its fields'.

Equations

• c.apply2 fst snd = c.apply (Cvc.Typed.Datatype.Args.cons fst (Cvc.Typed.Datatype.Args.cons snd Cvc.Typed.Datatype.Args.nil))

def Cvc.Typed.Datatype.Ctor.apply3 {α : Type} [Ω] (c : Ctor α) {β₁ β₂ β₃ : Type} [ToTyp β₁] [ToTyp β₂] [ToTyp β₃] (fst : Term β₁) (snd : Term β₂) (thd : Term β₃) : Env (Term α)

Applies the constructor, failing unless its arguments' number and sorts are its fields'.

Equations

• c.apply3 fst snd thd = c.apply (Cvc.Typed.Datatype.Args.cons fst (Cvc.Typed.Datatype.Args.cons snd (Cvc.Typed.Datatype.Args.cons thd Cvc.Typed.Datatype.Args.nil)))

def Cvc.Typed.Datatype.Ctor.is {α : Type} [Ω] (c : Ctor α) (t : Term α) : Env (Term Bool)

Whether a value was built by this constructor.

Equations

• c.is t = (Cvc.Typed.Datatype.Ctor.tester✝ c).applyTester t.erase

def Cvc.Typed.Datatype.Ctor.field {α : Type} [Ω] (c : Ctor α) (β : Type) [ToTyp β] (name : String) : Env (Field α β)

The field of the given name, at the Lean type β of its sort, failing if the sorts differ.

Equations

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

Matching

A match picks a body by the constructor its scrutinee was built with: Term.mkMatch takes the scrutinee and an array of Case α β, whose bodies all have the index β. Ctor.case binds the constructor's fields to bound variables, pushed in field order as for Solver.defineFun, and checks their sorts. Every constructor needs a case, unless a Datatype.caseAny catches the rest; cvc5 checks that.

structure Cvc.Typed.Datatype.Case [Ω] (α β : Type) : Type

One case of a match on a Term α, producing a Term β.

• term : Cvc.Untyped.Term

def Cvc.Typed.Datatype.Case.toUntyped [Ω] {α β : Type} (c : Case α β) : Untyped.Term

The sort-erased case term it wraps, for free, as the sort-erased Term.mkMatch takes one.

There is no way back: a sort-erased case is an ordinary Term, with no type of its own to hang a conversion on.

Equations

• c.toUntyped = Cvc.Typed.Datatype.Case.term✝ c

@[reducible, inline]

abbrev Cvc.Typed.Datatype.Case.erase [Ω] {α β : Type} (c : Case α β) : Untyped.Term

The sort-erased case term it wraps, for free, as the sort-erased Term.mkMatch takes one.

There is no way back: a sort-erased case is an ordinary Term, with no type of its own to hang a conversion on.

Equations

• c.erase = c.toUntyped

def Cvc.Typed.Datatype.Ctor.checkArity {α : Type} [Ω] (c : Ctor α) (count : Nat) : Env Unit

Fails unless the constructor takes exactly count fields.

Equations

• c.checkArity count = (Cvc.Typed.Datatype.Ctor.ctor✝ c).checkArity count

def Cvc.Typed.Datatype.Ctor.mkBVarAt {α : Type} [Ω] (c : Ctor α) (idx : Nat) (name : String) : Env Untyped.BVar

A fresh sort-erased bound variable at the sort of the constructor's field at idx.

Untyped.BVar.typeCheck puts an index on it.

Equations

• c.mkBVarAt idx name = (Cvc.Typed.Datatype.Ctor.ctor✝ c).mkBVarAt idx name

def Cvc.Typed.Datatype.Ctor.caseErased {α : Type} [Ω] (c : Ctor α) {β : Type} (vars : Untyped.BVars) (body : Term β) : Env (Case α β)

case, with the fields bound to sort-erased variables (from mkBVarAt).

Equations

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

def Cvc.Typed.Datatype.Ctor.case {α : Type} [Ω] (c : Ctor α) {β : Type} (args : BVars := []) (body : Term β) : Env (Case α β)

The case taken when the scrutinee was built by this constructor.

args binds the constructor's fields, in field order, and body may mention them. Fails unless their number and sorts are the fields'.

Equations

• c.case args body = c.caseErased args.erase body

def Cvc.Typed.Datatype.Ctor.case0 {α : Type} [Ω] (c : Ctor α) {β : Type} (body : Term β) : Env (Case α β)

The case taken when the scrutinee was built by this constructor, which takes no field.

Equations

• c.case0 body = c.case [] body

def Cvc.Typed.Datatype.Ctor.case1 {α : Type} [Ω] (c : Ctor α) {β₁ β : Type} [ToTyp β₁] (fst : BVar β₁) (body : Term β) : Env (Case α β)

The case taken when the scrutinee was built by this constructor.

args binds the constructor's fields, in field order, and body may mention them. Fails unless their number and sorts are the fields'.

Equations

• c.case1 fst body = c.case (Cvc.Typed.BVars.push fst []) body

def Cvc.Typed.Datatype.Ctor.case2 {α : Type} [Ω] (c : Ctor α) {β₁ β₂ β : Type} [ToTyp β₁] [ToTyp β₂] (fst : BVar β₁) (snd : BVar β₂) (body : Term β) : Env (Case α β)

The case taken when the scrutinee was built by this constructor.

args binds the constructor's fields, in field order, and body may mention them. Fails unless their number and sorts are the fields'.

Equations

• c.case2 fst snd body = c.case (Cvc.Typed.BVars.push snd (Cvc.Typed.BVars.push fst [])) body

def Cvc.Typed.Datatype.Ctor.case3 {α : Type} [Ω] (c : Ctor α) {β₁ β₂ β₃ β : Type} [ToTyp β₁] [ToTyp β₂] [ToTyp β₃] (fst : BVar β₁) (snd : BVar β₂) (thd : BVar β₃) (body : Term β) : Env (Case α β)

The case taken when the scrutinee was built by this constructor.

args binds the constructor's fields, in field order, and body may mention them. Fails unless their number and sorts are the fields'.

Equations

• c.case3 fst snd thd body = c.case (Cvc.Typed.BVars.push thd (Cvc.Typed.BVars.push snd (Cvc.Typed.BVars.push fst []))) body

def Cvc.Typed.Datatype.caseAny [Ω] {α β : Type} [ToTyp α] (v : BVar α) (body : Term β) : Env (Case α β)

The case taken when no earlier one was.

v stands for the scrutinee itself, so body may mention it. A match needs one of these unless its cases already cover every constructor.

Equations

• Cvc.Typed.Datatype.caseAny v body = do let __do_lift ← Cvc.Untyped.Term.matchBindCase (Cvc.Typed.BVars.push v []).erase v.toTerm.erase body.erase pure { term := __do_lift }

def Cvc.Typed.Term.ctorOf [Ω] {α : Type} [ToTyp α] (_scrutinee : Term α) (name : String) : Env (Datatype.Ctor α)

Datatype.ctor at the datatype of a term's index: the constructor of the given name.

Equations

• _scrutinee.ctorOf name = Cvc.Typed.Datatype.ctor α name

def Cvc.Typed.Term.mkMatch [Ω] {α β : Type} (scrutinee : Term α) (cases : Array (Datatype.Case α β)) (_h : 0 < cases.size := by (try grind) <;> fail "failed to prove there is at least one case") : Env (Term β)

The body of whichever case matches the scrutinee.

Fails unless every constructor of α has a case, or one of them is a Datatype.caseAny.

Equations

• scrutinee.mkMatch cases _h = scrutinee.erase.mkMatch (Array.map Cvc.Typed.Datatype.Case.term✝ cases) ⋯

def Cvc.Typed.Datatype.Field.toUntyped {α β : Type} [Ω] (sel : Field α β) : Datatype.Selector

The sort-erased selector it was built from, for free.

Equations

• sel.toUntyped = Cvc.Typed.Datatype.Field.sel✝ sel

@[reducible, inline]

abbrev Cvc.Typed.Datatype.Field.erase {α β : Type} [Ω] (sel : Field α β) : Datatype.Selector

The sort-erased selector it was built from, for free.

Equations

• sel.erase = sel.toUntyped

def Cvc.Typed.Datatype.Field.get {α β : Type} [Ω] (sel : Field α β) (t : Term α) : Env (Term β)

Reads the field out of a value.

Undefined where the value was not built by the selector's own constructor, which is what Ctor.is is for.

Equations

• sel.get t = (Cvc.Typed.Datatype.Field.term✝ sel).applySelector t.erase

def Cvc.Typed.Datatype.Field.update {α β : Type} [Ω] (sel : Field α β) (t : Term α) (v : Term β) : Env (Term α)

The value with this field replaced.

Equations

• sel.update t v = (Cvc.Typed.Datatype.Field.updater✝ sel).applyUpdater t.erase v.erase

def Cvc.Datatype.Selector.toTypedAs [Ω] (α β : Type) [ToTyp α] [ToTyp β] (sel : Selector) : Env (Typed.Datatype.Field α β)

Types a reflected selector at the datatype α and the field β, checking both sorts.

The reflection counterpart of Datatype.Ctor.field, which looks a selector up by name. toTyped infers α and β from the expected type; typeCheckAs and typeCheck are the same two functions under the names that say what they do.

Equations

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

def Cvc.Datatype.Selector.toTyped [Ω] {α β : Type} [ToTyp α] [ToTyp β] (sel : Selector) : Env (Typed.Datatype.Field α β)

Types a reflected selector at the datatype α and the field β, checking both sorts.

The reflection counterpart of Datatype.Ctor.field, which looks a selector up by name. toTyped infers α and β from the expected type; typeCheckAs and typeCheck are the same two functions under the names that say what they do.

Equations

• sel.toTyped = Cvc.Datatype.Selector.toTypedAs α β sel

@[reducible, inline]

abbrev Cvc.Datatype.Selector.typeCheckAs [Ω] (α β : Type) [ToTyp α] [ToTyp β] (sel : Selector) : Env (Typed.Datatype.Field α β)

Types a reflected selector at the datatype α and the field β, checking both sorts.

The reflection counterpart of Datatype.Ctor.field, which looks a selector up by name. toTyped infers α and β from the expected type; typeCheckAs and typeCheck are the same two functions under the names that say what they do.

Equations

• @Cvc.Datatype.Selector.typeCheckAs = @Cvc.Datatype.Selector.toTypedAs

@[reducible, inline]

abbrev Cvc.Datatype.Selector.typeCheck [Ω] {α β : Type} [ToTyp α] [ToTyp β] (sel : Selector) : Env (Typed.Datatype.Field α β)

Types a reflected selector at the datatype α and the field β, checking both sorts.

The reflection counterpart of Datatype.Ctor.field, which looks a selector up by name. toTyped infers α and β from the expected type; typeCheckAs and typeCheck are the same two functions under the names that say what they do.

Equations

• @Cvc.Datatype.Selector.typeCheck = @Cvc.Datatype.Selector.toTyped

Viewing a datatype operation

Generic over every datatype: constructors and fields come back by name, and the kids' sorts as a list of Typs that matching refines. Records, tuples and nullables are datatypes to cvc5, so this covers them too; Term.recordFields?, Term.pairComponents? and Term.nullableCases? take them apart at a known index instead.

inductive Cvc.Typed.View.Datatype.Fields [Ω] : List Typ → Type

A constructor's arguments, each a Term σ.Denote at its sort σ, in order.

Empty for a constant constructor such as nil.

• nil [Ω] : Fields []

  No argument.

• cons [Ω] {τs : List Typ} {τ : Typ} (t : Term τ.Denote) (rest : Fields τs) : Fields (τ :: τs)

  One more argument, in front of the others.

def Cvc.Typed.View.Datatype.Fields.toStrings [Ω] {doms : List Typ} : Fields doms → List String

The arguments as cvc5 prints them.

Equations

• Cvc.Typed.View.Datatype.Fields.nil.toStrings = []
• (Cvc.Typed.View.Datatype.Fields.cons t rest).toStrings = toString t :: rest.toStrings

inductive Cvc.Typed.View.Datatype [Ω] : Typ → Type

A datatype operation of sort τ, taken apart one level.

• construct [Ω] {τ : Typ} (ctor : String) (doms : List Typ) (args : Fields doms) : View.Datatype τ

  A constructor applied to its arguments, none for a constant constructor.

• selectField [Ω] {τ : Typ} (field : String) (σ : Typ) (arg : Term σ.Denote) : View.Datatype τ

  A field read off arg, a term of the datatype sort σ.

• updateField [Ω] {τ : Typ} (field : String) (σ : Typ) (arg : Term τ.Denote) (value : Term σ.Denote) : View.Datatype τ

  arg with its field replaced by value, a term of sort σ.

• testCtor [Ω] (ctor : String) (σ : Typ) (arg : Term σ.Denote) : View.Datatype Typ.bool

  Whether arg, of the datatype sort σ, was built by the constructor ctor.

def Cvc.Typed.View.Datatype.of [Ω] (τ : Typ) (t : Term τ.Denote) : Env (Option (View.Datatype τ))

Takes a datatype operation of sort τ apart one level, none for any other term.

Also none when a kid's sort is one no Typ describes.

Equations

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

smt! match

smt! match l with
  | cons h t => h * 2
  | nil => 0

A bare identifier in a pattern is a constructor; _ alone is the catch-all. A field's index is inferred from its uses in the body; a nested match's scrutinee needs an ascription, | cons h (t : Lst) => match t with ….

def Cvc.Typed.Ext.expandMatchAltT (layer : Ext.Layer) (scrutId : Lean.Ident) (alt : Lean.Syntax) : Lean.MacroM (Lean.TSyntax `term)

Expands one alternative of a typed match into a term building that case.

Equations

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