Datatypes, sort-erased

A datatype sort is declared, in three steps: a constructor declaration collects its selectors, a datatype declaration collects its constructors, and Srt.datatype turns that into a sort. Once the sort exists, Srt.getDatatype reflects it back as a Datatype whose constructors and selectors carry the terms that build and take apart its values.

A declared sort is fresh, never nominal. Declaring the same datatype twice gives two different sorts that print identically, and cvc5 rejects any term mixing them:

Subexpressions must have the same type: Type 1: Pair, Type 2: Pair

So Srt.datatype, Srt.datatypes and Solver.declareDatatype record each datatype's name in the scope, and refuse a name already taken; Srt.ofName finds the sort again by its name.

A record sort is the exception: cvc5 builds the same record sort from the same fields, so it is not declared. Records are still datatypes underneath, and Cvc.Untyped.Theory.Record builds on what is here.

Recursion goes through addSelectorSelf for a datatype referring to itself, and addSelectorUnresolved with Srt.datatypes for a mutually recursive group.

Declaring

def Cvc.Datatype.Ctor.Decl.mk [Ω] (name : String) : Env Decl

Create a datatype constructor declaration.

• name The name of the datatype constructor.

Equations

• Cvc.Datatype.Ctor.Decl.mk name = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkDatatypeConstructorDecl name

def Cvc.Datatype.Ctor.Decl.addSelector [Ω] (d : Decl) (name : String) (srt : Srt) : Env Decl

Adds a selector named name, of codomain sort srt.

Equations

• d.addSelector name srt = Cvc.runUnsafe'✝ ((Cvc.Datatype.Ctor.Decl.toUnsafe✝ d).addSelector name (Cvc.Srt.toUnsafe✝ srt))

def Cvc.Datatype.Ctor.Decl.addSelectorSelf [Ω] (d : Decl) (name : String) : Env Decl

Adds a selector whose codomain is the datatype being declared.

Equations

• d.addSelectorSelf name = Cvc.runUnsafe'✝ ((Cvc.Datatype.Ctor.Decl.toUnsafe✝ d).addSelectorSelf name)

def Cvc.Datatype.Ctor.Decl.addSelectorUnresolved [Ω] (d : Decl) (name unresDatatypeName : String) : Env Decl

Adds a selector whose codomain is another datatype of the same mutually recursive group.

Equations

• d.addSelectorUnresolved name unresDatatypeName = Cvc.runUnsafe'✝ ((Cvc.Datatype.Ctor.Decl.toUnsafe✝ d).addSelectorUnresolved name unresDatatypeName)

def Cvc.Datatype.Decl.mk [Ω] (name : String) (params : Srts := #[]) (isCoDatatype : Bool := false) : Env Decl

Create a datatype declaration.

• name The name of the datatype.
• params A list of sort parameters.
• isCoDatatype True if a codatatype is to be constructed.

Equations

• Cvc.Datatype.Decl.mk name params isCoDatatype = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkDatatypeDecl name params isCoDatatype

def Cvc.Datatype.Decl.addCtor [Ω] (d : Decl) (ctor : Ctor.Decl) : Env Decl

Add datatype constructor declaration.

• ctor The datatype constructor declaration to add.

Equations

• d.addCtor ctor = Cvc.runUnsafe'✝ ((Cvc.Datatype.Decl.toUnsafe✝ d).addConstructor (Cvc.Datatype.Ctor.Decl.toUnsafe✝ ctor))

def Cvc.Datatype.Decl.countCtors [Ω] (d : Decl) : Nat

Get the number of constructors for this datatype declaration.

Equations

• d.countCtors = (Cvc.Datatype.Decl.toUnsafe✝ d).getNumConstructors

def Cvc.Datatype.Decl.isParametric [Ω] (d : Decl) : Bool

Determine if this datatype declaration is parametric.

Warning: this function is experimental and may change in future versions.

Equations

• d.isParametric = (Cvc.Datatype.Decl.toUnsafe✝ d).isParametric

def Cvc.Datatype.Decl.getName [Ω] (d : Decl) : Res String

Get the name of this datatype declaration.

Equations

• d.getName = liftM (Cvc.Datatype.Decl.toUnsafe✝ d).getName

def Cvc.Datatype.Decl.isResolved [Ω] (d : Decl) : Env Bool

Determine if this datatype declaration is resolved (has already been used to declare a datatype).

Equations

• d.isResolved = Cvc.runUnsafe'✝ (Cvc.Datatype.Decl.toUnsafe✝ d).isResolved

def Cvc.Untyped.Solver.declareDatatype [Ω] (s : Solver) (symbol : String) (ctors : Array Datatype.Ctor.Decl) : Env Srt

Declares a datatype sort from its constructors.

The short path: no parameters and no mutual recursion. Srt.datatype is the general one.

Equations

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

Reflecting

Srt.getDatatype is the way in, from a sort that Srt.isDatatype holds of.

def Cvc.Datatype.Selector.getName [Ω] (s : Selector) : Res String

Get the name of this datatype selector.

Equations

• s.getName = liftM (Cvc.Datatype.Selector.toUnsafe✝ s).getName

def Cvc.Datatype.Selector.getTerm [Ω] (s : Selector) : Env Untyped.Term

The selector term, the first argument of an applySelector.

Equations

• s.getTerm = Cvc.runUnsafe'✝ (Cvc.Datatype.Selector.toUnsafe✝ s).getTerm

def Cvc.Datatype.Selector.getUpdaterTerm [Ω] (s : Selector) : Env Untyped.Term

The updater term, the first argument of an applyUpdater.

Equations

• s.getUpdaterTerm = Cvc.runUnsafe'✝ (Cvc.Datatype.Selector.toUnsafe✝ s).getUpdaterTerm

def Cvc.Datatype.Selector.getCodomainSort [Ω] (s : Selector) : Env Srt

Get the codomain sort of this selector.

Equations

• s.getCodomainSort = Cvc.runUnsafe'✝ (Cvc.Datatype.Selector.toUnsafe✝ s).getCodomainSort

def Cvc.Datatype.Ctor.getName [Ω] (c : Ctor) : Res String

Get the name of this datatype constructor.

Equations

• c.getName = liftM (Cvc.Datatype.Ctor.toUnsafe✝ c).getName

def Cvc.Datatype.Ctor.getTerm [Ω] (c : Ctor) : Env Untyped.Term

The constructor term, the first argument of an applyCtor.

Equations

• c.getTerm = Cvc.runUnsafe'✝ (Cvc.Datatype.Ctor.toUnsafe✝ c).getTerm

def Cvc.Datatype.Ctor.getInstantiatedTerm [Ω] (c : Ctor) (retSort : Srt) : Env Untyped.Term

The constructor term of a parametric datatype, at the given instance of it.

Equations

• c.getInstantiatedTerm retSort = Cvc.runUnsafe'✝ ((Cvc.Datatype.Ctor.toUnsafe✝ c).getInstantiatedTerm (Cvc.Srt.toUnsafe✝ retSort))

def Cvc.Datatype.Ctor.getTesterTerm [Ω] (c : Ctor) : Env Untyped.Term

The tester term, the first argument of an applyTester.

Equations

• c.getTesterTerm = Cvc.runUnsafe'✝ (Cvc.Datatype.Ctor.toUnsafe✝ c).getTesterTerm

def Cvc.Datatype.Ctor.countSelectors [Ω] (c : Ctor) : Nat

The number of selectors of this datatype constructor.

Equations

• c.countSelectors = (Cvc.Datatype.Ctor.toUnsafe✝ c).getNumSelectors

def Cvc.Datatype.Ctor.getSelector [Ω] (c : Ctor) (name : String) : Env Selector

Get the datatype selector with the given name.

This is a linear search through the selectors, so in case of multiple, similarly-named selectors, the first is returned.

• name The name of the datatype selector.

Equations

• c.getSelector name = Cvc.runUnsafe'✝ ((Cvc.Datatype.Ctor.toUnsafe✝ c).getSelector name)

def Cvc.Datatype.Ctor.getSelectorAt [Ω] (c : Ctor) (idx : Fin c.countSelectors) : Selector

The datatype selector at index idx.

Equations

• c.getSelectorAt idx = (Cvc.Datatype.Ctor.toUnsafe✝ c).getSelectorAt idx

@[instance_reducible]

instance Cvc.Datatype.Ctor.instGetElemNatSelectorLtCountSelectors [Ω] : GetElem Ctor Nat Selector fun (c : Ctor) (idx : Nat) => idx < c.countSelectors

Equations

• Cvc.Datatype.Ctor.instGetElemNatSelectorLtCountSelectors = { getElem := Cvc.Datatype.Ctor.instGetElemNatSelectorLtCountSelectors._aux_1 }

@[instance_reducible]

instance Cvc.Datatype.Ctor.instForInSelectorOfMonad [Ω] {m : Type u_1 → Type u_2} [Monad m] : ForIn m Ctor Selector

Equations

• Cvc.Datatype.Ctor.instForInSelectorOfMonad = { forIn := @Cvc.Datatype.Ctor.instForInSelectorOfMonad._aux_1 inst✝¹ m inst✝ }

def Cvc.Datatype.getName [Ω] (dt : Datatype) : Res String

Get the name of this datatype.

Equations

• dt.getName = liftM (Cvc.Datatype.toUnsafe✝ dt).getName

def Cvc.Datatype.getCtorNamed [Ω] (dt : Datatype) (name : String) : Env Ctor

Get the datatype constructor with the given name.

This is a linear search through the constructors, so in case of multiple, similarly-named constructors, the first is returned.

• name The name of the datatype constructor.

Equations

• dt.getCtorNamed name = Cvc.runUnsafe'✝ ((Cvc.Datatype.toUnsafe✝ dt).getConstructor name)

def Cvc.Datatype.countCtors [Ω] (dt : Datatype) : Nat

Get the number of constructors of this datatype.

Equations

• dt.countCtors = (Cvc.Datatype.toUnsafe✝ dt).getNumConstructors

def Cvc.Datatype.getCtorAt [Ω] (dt : Datatype) (idx : Fin dt.countCtors) : Ctor

Get the datatype constructor at a given index.

• idx The index of the datatype constructor to return.

Equations

• dt.getCtorAt idx = (Cvc.Datatype.toUnsafe✝ dt).getConstructorAt idx

def Cvc.Datatype.getCtorAt? [Ω] (dt : Datatype) (idx : Nat) : Option Ctor

The constructor at index idx, none if there is none.

Equations

• dt.getCtorAt? idx = if h : idx < dt.countCtors then some (dt.getCtorAt ⟨idx, h⟩) else none

def Cvc.Datatype.getCtor [Ω] (dt : Datatype) (idx : Nat) : Res Ctor

The constructor at index idx, failing if there is none.

Equations

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

@[instance_reducible]

instance Cvc.Datatype.instGetElemNatCtorLtCountCtors [Ω] : GetElem Datatype Nat Ctor fun (dt : Datatype) (idx : Nat) => idx < dt.countCtors

Equations

• Cvc.Datatype.instGetElemNatCtorLtCountCtors = { getElem := Cvc.Datatype.instGetElemNatCtorLtCountCtors._aux_1 }

@[instance_reducible]

instance Cvc.Datatype.instForInCtorOfMonad [Ω] {m : Type u_1 → Type u_2} [Monad m] : ForIn m Datatype Ctor

Equations

• Cvc.Datatype.instForInCtorOfMonad = { forIn := @Cvc.Datatype.instForInCtorOfMonad._aux_1 inst✝¹ m inst✝ }

def Cvc.Datatype.getSelector [Ω] (dt : Datatype) (name : String) : Env Selector

Looks a selector up by name, across every constructor.

Equations

• dt.getSelector name = Cvc.runUnsafe'✝ ((Cvc.Datatype.toUnsafe✝ dt).getSelector name)

def Cvc.Datatype.getParameters [Ω] (dt : Datatype) : Env Srts

The sort parameters of this datatype, failing unless it is parametric.

Equations

• dt.getParameters = Cvc.runUnsafe'✝ (Cvc.Datatype.toUnsafe✝ dt).getParameters

def Cvc.Datatype.isParametric [Ω] (dt : Datatype) : Bool

Determine if this datatype is parametric.

Warning: this function is experimental and may change in future versions.

Equations

• dt.isParametric = (Cvc.Datatype.toUnsafe✝ dt).isParametric

def Cvc.Datatype.isCoDatatype [Ω] (dt : Datatype) : Bool

Determine if this datatype corresponds to a co-datatype.

Equations

• dt.isCoDatatype = (Cvc.Datatype.toUnsafe✝ dt).isCodatatype

def Cvc.Datatype.isTuple [Ω] (dt : Datatype) : Bool

Determine if this datatype corresponds to a tuple.

Equations

• dt.isTuple = (Cvc.Datatype.toUnsafe✝ dt).isTuple

def Cvc.Datatype.isRecord [Ω] (dt : Datatype) : Bool

Determine if this datatype corresponds to a record.

Warning: this function is experimental and may change in future versions.

Equations

• dt.isRecord = (Cvc.Datatype.toUnsafe✝ dt).isRecord

def Cvc.Datatype.isFinite [Ω] (dt : Datatype) : Res Bool

Determine if this datatype is finite.

Equations

• dt.isFinite = liftM (Cvc.Datatype.toUnsafe✝ dt).isFinite

def Cvc.Datatype.isWellFounded [Ω] (dt : Datatype) : Bool

Whether this datatype is well-founded.

A datatype that is not a codatatype is well-founded when it has a value of finite size.

Equations

• dt.isWellFounded = (Cvc.Datatype.toUnsafe✝ dt).isWellFounded

Building and taking apart values

Each of these takes the relevant term off a Ctor or Selector as its first argument, which is how cvc5 spells datatype application.

def Cvc.Untyped.Term.applyCtor [Ω] (ctor : Term) (args : Terms := #[]) : Env Term

Applies a constructor to its arguments.

Equations

• ctor.applyCtor args = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.APPLY_CONSTRUCTOR (#[ctor] ++ args)

def Cvc.Untyped.Term.applySelector [Ω] (sel dt : Term) : Env Term

Reads a field out of a datatype value.

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

Equations

• sel.applySelector dt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.APPLY_SELECTOR #[sel, dt]

def Cvc.Untyped.Term.applyTester [Ω] (tester dt : Term) : Env Term

Whether a datatype value was built by a given constructor.

Equations

• tester.applyTester dt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.APPLY_TESTER #[tester, dt]

def Cvc.Untyped.Term.applyUpdater [Ω] (updater dt newValue : Term) : Env Term

The datatype value with one field replaced.

Equations

• updater.applyUpdater dt newValue = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.APPLY_UPDATER #[updater, dt, newValue]

@[reducible, inline]

abbrev Cvc.Datatype.Ctor.apply [Ω] (ctor : Ctor) (args : Untyped.Terms := #[]) : Env Untyped.Term

Applies a constructor to its arguments.

Equations

• ctor.apply args = do let __do_lift ← ctor.getTerm __do_lift.applyCtor args

@[reducible, inline]

abbrev Cvc.Datatype.Selector.apply [Ω] (sel : Selector) (dt : Untyped.Term) : Env Untyped.Term

Reads a field out of a datatype value.

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

Equations

• sel.apply dt = do let __do_lift ← sel.getTerm __do_lift.applySelector dt

@[reducible, inline]

abbrev Cvc.Datatype.Selector.applyUpdate [Ω] (sel : Selector) (dt newValue : Untyped.Term) : Env Untyped.Term

The datatype value with one field replaced.

Equations

• sel.applyUpdate dt newValue = do let __do_lift ← sel.getUpdaterTerm __do_lift.applyUpdater dt newValue

Matching

A match term picks a body by the constructor its scrutinee was built with. Each case pairs a pattern with the body to use when it applies, and mkMatch collects them. A case binds its constructor's fields to bound variables (Term.mkBVar).

cvc5 checks that the cases cover every constructor, unless one of them is a catch-all, and that all of the bodies have the same sort.

Cases are tried in order, so a catch-all placed before another case shadows it — the same reading Lean's own match has. cvc5 accepts a catch-all in any position, including as the only case.

ctorOf, checkArity and mkBVarAt find a constructor by name and bind its fields, which is what smt! match expands to; hand-written matches can use them too.

def Cvc.Untyped.Term.ctorOf [Ω] (t : Term) (name : String) : Env Datatype.Ctor

The constructor of the given name, of the datatype this term's sort denotes.

Equations

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

def Cvc.Datatype.Ctor.checkArity [Ω] (c : Ctor) (count : Nat) : Env Unit

Fails unless the constructor takes exactly count fields, naming the constructor.

Equations

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

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

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

Equations

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

def Cvc.Untyped.Term.matchCase [Ω] (pattern body : Term) : Env Term

A match case for a constructor taking no field.

pattern is that constructor applied to nothing. A constructor that does take fields needs matchBindCase, which binds them.

Equations

• pattern.matchCase body = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.MATCH_CASE #[pattern, body]

def Cvc.Untyped.Term.matchBindCase [Ω] (bvars : BVars) (pattern body : Term) : Env Term

A match case binding the variables its pattern mentions.

pattern is either a constructor applied to exactly bvars, or a single bound variable — which makes the case a catch-all, matching whatever the earlier cases left over. body is free to mention the bound variables.

Equations

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

def Cvc.Untyped.Term.mkMatch [Ω] (scrutinee : Term) (cases : Terms) (_h : 0 < Array.size cases := by (try grind) <;> fail "failed to prove there is at least one case") : Env Term

The body of whichever case matches the scrutinee.

Every case must come from matchCase or matchBindCase, and the resulting term has the sort the bodies share.

Equations

• scrutinee.mkMatch cases _h = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.MATCH (#[scrutinee] ++ cases)

The view of a datatype operation

Written by hand, and generic over every datatype: which constructors and fields a datatype has is a fact about its declaration, so they come back by name. Records, tuples and nullables are datatypes to cvc5 too, so this covers them, a record's fields and a tuple's components being selectors like any other — a record's constructor answers the name cvc5 gives it, __cvc5_record_….

inductive Cvc.Untyped.View.Datatype [Ω] : Type

A datatype operation, taken apart one level, sort-erased.

• construct [Ω] (ctor : String) (args : Terms) : View.Datatype

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

• selectField [Ω] (field : String) (arg : Term) : View.Datatype

  A field read off a datatype term.

• updateField [Ω] (field : String) (arg value : Term) : View.Datatype

  arg with its field replaced by value.

• testCtor [Ω] (ctor : String) (arg : Term) : View.Datatype

  Whether arg was built by the constructor ctor.

def Cvc.Untyped.View.Datatype.of? [Ω] (t : Term) : Option View.Datatype

Takes a term apart one level, if it is a datatype operation.

Equations

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

smt! match

match … with | ctor x y => … | _ => … over a datatype, binding each constructor's fields without the writer having to make bound variables.

The catch-all is spelled _ and nothing else: a bare identifier is always a constructor name, so | nil => … means the constructor. The body of a catch-all can mention the scrutinee directly.

def Lean.Parser.Category.smtPatArg : Category

One variable bound by a pattern, optionally at a stated sort.

Equations

• Lean.Parser.Category.smtPatArg = { }

def Cvc.smtPatArg.quot : Lean.ParserDescr

Equations

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

def Cvc.smtPatArg : Lean.ParserDescr

A variable whose sort is inferred.

Equations

• Cvc.smtPatArg = Lean.ParserDescr.node `Cvc.smtPatArg 1022 (Lean.ParserDescr.const `ident)

def Cvc.smtPatArgOf : Lean.ParserDescr

A variable at a stated sort, (x : Lst); typed layer only, refused sort-erased.

Equations

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

def Lean.Parser.Category.smtMatchAlt : Category

One alternative of a match.

Equations

• Lean.Parser.Category.smtMatchAlt = { }

def Cvc.smtMatchAlt.quot : Lean.ParserDescr

Equations

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

def Cvc.smtAlt : Lean.ParserDescr

An alternative matching one constructor, binding one variable per field.

Equations

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

def Cvc.smtAltAny : Lean.ParserDescr

The catch-all alternative, taken when no earlier one matches.

Equations

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

def Cvc.smtMatch : Lean.ParserDescr

Matches a datatype term against its constructors.

Equations

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

def Cvc.Ext.patBinderName (arg : Lean.Syntax) : Lean.Name

The name a pattern variable binds.

Equations

• Cvc.Ext.patBinderName arg = if (arg.getKind == `Cvc.smtPatArgOf) = true then arg[1].getId else arg[0].getId

partial def Cvc.Ext.occursIn (name : Lean.Name) : Lean.Syntax → Bool

Whether an identifier is referenced anywhere in a piece of syntax.

Used on a match body, before it is expanded, to tell whether a variable the pattern binds is mentioned at all — which in the typed layer is what decides whether its index can be inferred.

Binders shadow, so this stops at one: a nested alternative or let that rebinds the name is talking about a different variable, and descending into its body would report an occurrence that is not one.

def Cvc.Ext.patArgs (args : Array Lean.Syntax) : Lean.MacroM (Array (Lean.Ident × Option (Lean.TSyntax `term)))

Parses a pattern's variables into their binders and their sort ascriptions, where given.

Equations

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

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

Expands one alternative of a sort-erased match into a term building that case.

The body sees each variable the pattern binds, under the name the writer gave it, as a term. A variable is made at its field's declared sort, so a sort ascription is refused.

Equations

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