The Lean type a sort denotes

Typ.Denote τ is the Lean type that indexes terms of sort τ: .int denotes Int, .set .int denotes Set Int, a record its Record, a tuple its product. It is what makes a sort carried as data — a Typ field of a term's view — usable as a term's index: matching the Typ refines Term τ.Denote to Term Int, definitionally.

A sort with no better denotation denotes Sorted τ, a stand-in indexed by the sort itself: declared sorts, a container keyed on something with no order, a tuple whose last component is a tuple. A term at a stand-in is moved to a user's own index with Typed.Term.cast.

Everything here is reducible and exposed, so that a known Typ reduces both in unification and in instance resolution.

structure Cvc.Sorted (τ : Typ) : Type

The stand-in Lean type for a sort with no better denotation, indexed by the sort itself.

@[instance_reducible]

instance Cvc.instToTypSorted {τ : Typ} : ToTyp (Sorted τ)

Equations

• Cvc.instToTypSorted = { typ := τ }

@[instance_reducible]

instance Cvc.instOrdSorted {τ : Typ} : Ord (Sorted τ)

Sorted τ has exactly one value, so the constant order is the right one.

Equations

• Cvc.instOrdSorted = { compare := fun (x x_1 : Cvc.Sorted τ) => Ordering.eq }

@[reducible]

def Cvc.Typ.lastIsProd : List Typ → Bool

Whether a tuple's last component is itself a tuple.

Equations

• Cvc.Typ.lastIsProd [] = false
• Cvc.Typ.lastIsProd [Cvc.Typ.prod args] = true
• Cvc.Typ.lastIsProd [head] = false
• Cvc.Typ.lastIsProd (head :: rest) = Cvc.Typ.lastIsProd rest

@[reducible]

def Cvc.Typ.denoteWithOrd : Typ → (T : Type) × Option (Ord T)

The Lean type a sort denotes, together with its order if it has one.

Computed together because a container's denotation needs its element's order: .set .int denotes Set Int, which is only a type given Ord Int. A container whose element has no order — a set of functions — denotes Sorted τ, as do declared sorts. TotalMap and functions have no order of their own; a record or a tuple has one exactly when all its components do, lexicographically, as OrdFields and the product order give it.

Equations

• One or more equations did not get rendered due to their size.
• Cvc.Typ.bool.denoteWithOrd = ⟨Bool, some inferInstance⟩
• Cvc.Typ.int.denoteWithOrd = ⟨Int, some inferInstance⟩
• Cvc.Typ.real.denoteWithOrd = ⟨Rat, some inferInstance⟩
• Cvc.Typ.string.denoteWithOrd = ⟨String, some inferInstance⟩
• Cvc.Typ.regex.denoteWithOrd = ⟨Cvc.Regex, some inferInstance⟩
• Cvc.Typ.roundingMode.denoteWithOrd = ⟨Cvc.Float.RoundingMode, some inferInstance⟩
• (Cvc.Typ.bitVec n).denoteWithOrd = ⟨BitVec n, some inferInstance⟩
• (Cvc.Typ.float e s).denoteWithOrd = ⟨Cvc.Float e s, some inferInstance⟩
• (Cvc.Typ.finiteField n).denoteWithOrd = ⟨Cvc.FiniteField n, some inferInstance⟩
• (Cvc.Typ.seq e).denoteWithOrd = match e.denoteWithOrd with | ⟨T, some val⟩ => ⟨Array T, some inferInstance⟩ | ⟨T, none⟩ => ⟨Array T, none⟩
• e.nullable.denoteWithOrd = match e.denoteWithOrd with | ⟨T, some val⟩ => ⟨Option T, some inferInstance⟩ | ⟨T, none⟩ => ⟨Option T, none⟩
• (Cvc.Typ.record fs).denoteWithOrd = match Cvc.Typ.denoteFieldsWithOrd fs with | ⟨Fs, some val⟩ => ⟨Cvc.Record Fs, some inferInstance⟩ | ⟨Fs, none⟩ => ⟨Cvc.Record Fs, none⟩
• (Cvc.Typ.prod ts).denoteWithOrd = Cvc.Typ.denoteProdWithOrd ts
• (Cvc.Typ.set e).denoteWithOrd = match e.denoteWithOrd with | ⟨T, some val⟩ => ⟨Cvc.Set T, some inferInstance⟩ | ⟨fst, none⟩ => ⟨Cvc.Sorted (Cvc.Typ.set e), some inferInstance⟩
• (Cvc.Typ.bag e).denoteWithOrd = match e.denoteWithOrd with | ⟨T, some val⟩ => ⟨Cvc.Bag T, some inferInstance⟩ | ⟨fst, none⟩ => ⟨Cvc.Sorted (Cvc.Typ.bag e), some inferInstance⟩
• (d.function c).denoteWithOrd = ⟨d.denoteWithOrd.fst → c.denoteWithOrd.fst, none⟩
• x✝.denoteWithOrd = ⟨Cvc.Sorted x✝, some inferInstance⟩

@[reducible]

def Cvc.Typ.denoteFieldsWithOrd : List (String × Typ) → (Fs : List (String × Type)) × Option (OrdFields Fs)

A record's fields' denotations, by name, with the record's order if every field has one.

Equations

• One or more equations did not get rendered due to their size.
• Cvc.Typ.denoteFieldsWithOrd [] = ⟨[], some inferInstance⟩

@[reducible]

def Cvc.Typ.denoteProdWithOrd : List Typ → (T : Type) × Option (Ord T)

A tuple's denotation, ordered if every component is.

The right-nested product of its components' denotations, as α × β × γ indexes a three-component tuple, and OneTuple for one component. A tuple whose last component is itself a tuple has no product to denote it — the product would flatten it — and neither has the empty tuple: those are Sorted.

Equations

• One or more equations did not get rendered due to their size.
• Cvc.Typ.denoteProdWithOrd [] = ⟨Cvc.Sorted (Cvc.Typ.prod []), some inferInstance⟩
• Cvc.Typ.denoteProdWithOrd [t] = match t.denoteWithOrd with | ⟨T, some val⟩ => ⟨Cvc.OneTuple T, some inferInstance⟩ | ⟨T, none⟩ => ⟨Cvc.OneTuple T, none⟩
• Cvc.Typ.denoteProdWithOrd [a, Cvc.Typ.prod bs] = ⟨Cvc.Sorted (Cvc.Typ.prod [a, Cvc.Typ.prod bs]), some inferInstance⟩
• Cvc.Typ.denoteProdWithOrd [a, b] = match a.denoteWithOrd, b.denoteWithOrd with | ⟨A, some val⟩, ⟨B, some val_1⟩ => ⟨A × B, some inferInstance⟩ | ⟨A, snd⟩, ⟨B, snd_1⟩ => ⟨A × B, none⟩

@[reducible]

def Cvc.Typ?.denoteWithOrd : Typ? → (T : Type) × Option (Ord T)

Typ.denoteWithOrd lifted to Typ?; an abstract sort, never a term's, denotes Empty.

Equations

• (Cvc.Typ?.typ t).denoteWithOrd = t.denoteWithOrd
• x✝.denoteWithOrd = ⟨Empty, none⟩

@[reducible]

def Cvc.Typ.denoteFields (fs : List (String × Typ)) : List (String × Type)

A record's fields' denotations, by name.

Equations

• Cvc.Typ.denoteFields fs = (Cvc.Typ.denoteFieldsWithOrd fs).fst

@[reducible]

def Cvc.Typ.denoteProd (ts : List Typ) : Type

A tuple's denotation; see Typ.denoteProdWithOrd.

Equations

• Cvc.Typ.denoteProd ts = (Cvc.Typ.denoteProdWithOrd ts).fst

@[reducible]

def Cvc.Typ.Denote (τ : Typ) : Type

The Lean type a sort denotes.

It reduces on a known Typ, which is what makes matching on a view's Typ refine the kids' index: Term (Typ.Denote .int) is Term Int, and Term (Typ.Denote (.set .int)) is Term (Set Int), with the very Ord Int a user's Set Int has.

Equations

• τ.Denote = τ.denoteWithOrd.fst

@[instance_reducible]

instance Cvc.instToTypDenote (τ : Typ) : ToTyp τ.Denote

A denotation's sort is the sort it denotes.

Equations

• Cvc.instToTypDenote τ = { typ := τ }

def Cvc.Typ.arrows : List Typ → Type → Type

The function type from the denotations of doms, in order, to β.

Equations

• x✝ = x✝
• Cvc.Typ.arrows (τ :: τs) x✝ = (τ.Denote → Cvc.Typ.arrows τs x✝)

@[instance_reducible]

instance Cvc.Typ.arrowsToTyp {β : Type} [ToTyp β] (doms : List Typ) : ToTyp (arrows doms β)

A function type over denotations has the function sort they denote.

Equations

• Cvc.Typ.arrowsToTyp [] = Cvc.Typ.arrowsToTyp._aux_1
• Cvc.Typ.arrowsToTyp (τ :: τs) = { typ := (Cvc.ToTyp.typ τ.Denote).function (Cvc.Typ?.typ (Cvc.ToTyp.typ (Cvc.Typ.arrows τs β))) }

def Cvc.delabDenote : Lean.PrettyPrinter.Delaborator.Delab

Shows a denotation, or a function type over denotations, as the type it reduces to.

Typ.Denote (.set .int) shows as Set Int. A sort that does not reduce, or only part-way — one bound by an unmatched pattern — shows as τ.Denote.

Equations

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