Basic Definitions for RefinedDiscrTree

Definitions

inductive Lean.Meta.RefinedDiscrTree.Key : Type

Discrimination tree key.

• star : Nat → Key

  A metavariable. This key matches with anything. It stores an index.

• opaque : Key

  An opaque variable. This key only matches with itself or Key.star.

• const : Name → Nat → Key

  A constant. It stores the name and the arity.

• fvar : FVarId → Nat → Key

  A free variable. It stores the FVarId and the arity.

• bvar : Nat → Nat → Key

  A bound variable, from a lambda or forall binder. It stores the De Bruijn index and the arity.

• lit : Literal → Key

  A literal.

• sort : Key

  A sort. Universe levels are ignored.

• lam : Key

  A lambda function.

• forall : Key

  A dependent arrow.

• proj : Name → Nat → Nat → Key

  A projection. It stores the structure name, the projection index and the arity.

instance Lean.Meta.RefinedDiscrTree.instInhabitedKey : Inhabited Key

Equations

• Lean.Meta.RefinedDiscrTree.instInhabitedKey = { default := Lean.Meta.RefinedDiscrTree.Key.star default }

instance Lean.Meta.RefinedDiscrTree.instBEqKey : BEq Key

Equations

• Lean.Meta.RefinedDiscrTree.instBEqKey = { beq := Lean.Meta.RefinedDiscrTree.beqKey✝ }

instance Lean.Meta.RefinedDiscrTree.instReprKey : Repr Key

Equations

• Lean.Meta.RefinedDiscrTree.instReprKey = { reprPrec := Lean.Meta.RefinedDiscrTree.reprKey✝ }

instance Lean.Meta.RefinedDiscrTree.instHashableKey : Hashable Key

Equations

• Lean.Meta.RefinedDiscrTree.instHashableKey = { hash := Lean.Meta.RefinedDiscrTree.Key.hash✝ }

def Lean.Meta.RefinedDiscrTree.Key.ctorIdx : Key → Nat

Constructor index used for ordering Key. Note that the index of the star pattern is 0, so that when looking up in a Trie, we can look at the start of the sorted array for all .star patterns.

Equations

• (Lean.Meta.RefinedDiscrTree.Key.star a).ctorIdx = 0
• Lean.Meta.RefinedDiscrTree.Key.opaque.ctorIdx = 1
• (Lean.Meta.RefinedDiscrTree.Key.const a a_1).ctorIdx = 2
• (Lean.Meta.RefinedDiscrTree.Key.fvar a a_1).ctorIdx = 3
• (Lean.Meta.RefinedDiscrTree.Key.bvar a a_1).ctorIdx = 4
• (Lean.Meta.RefinedDiscrTree.Key.lit a).ctorIdx = 5
• Lean.Meta.RefinedDiscrTree.Key.sort.ctorIdx = 6
• Lean.Meta.RefinedDiscrTree.Key.lam.ctorIdx = 7
• Lean.Meta.RefinedDiscrTree.Key.forall.ctorIdx = 8
• (Lean.Meta.RefinedDiscrTree.Key.proj a a_1 a_2).ctorIdx = 9

instance Lean.Meta.RefinedDiscrTree.instLTKey : LT Key

Equations

• Lean.Meta.RefinedDiscrTree.instLTKey = { lt := fun (a b : Lean.Meta.RefinedDiscrTree.Key) => Lean.Meta.RefinedDiscrTree.Key.lt✝ a b = true }

instance Lean.Meta.RefinedDiscrTree.instDecidableLtKey (a b : Key) : Decidable (a < b)

Equations

• Lean.Meta.RefinedDiscrTree.instDecidableLtKey a b = inferInstanceAs (Decidable (Lean.Meta.RefinedDiscrTree.Key.lt✝ a b = true))

instance Lean.Meta.RefinedDiscrTree.instToFormatKey : ToFormat Key

Equations

• Lean.Meta.RefinedDiscrTree.instToFormatKey = { format := Lean.Meta.RefinedDiscrTree.Key.format✝ }

def Lean.Meta.RefinedDiscrTree.Key.arity : Key → Nat

Return the number of arguments that the Key takes.

Equations

• (Lean.Meta.RefinedDiscrTree.Key.const a a_1).arity = a_1
• (Lean.Meta.RefinedDiscrTree.Key.fvar a a_1).arity = a_1
• (Lean.Meta.RefinedDiscrTree.Key.bvar a a_1).arity = a_1
• Lean.Meta.RefinedDiscrTree.Key.lam.arity = 1
• Lean.Meta.RefinedDiscrTree.Key.forall.arity = 2
• (Lean.Meta.RefinedDiscrTree.Key.proj a a_1 a_2).arity = 1 + a_2
• x✝.arity = 0

inductive Lean.Meta.RefinedDiscrTree.Trie (α : Type) : Type

Discrimination tree trie. See RefinedDiscrTree.

• node {α : Type} (children : Array (Key × Trie α)) : Trie α

  Map from Key to Trie. Children is an Array of size at least 2, sorted in increasing order using Key.lt.

• path {α : Type} (keys : Array Key) (child : Trie α) : Trie α

  Sequence of nodes with only one child. keys is an Array of size at least 1.

• values {α : Type} (vs : Array α) : Trie α

  Leaf of the Trie. values is an Array of size at least 1.

instance Lean.Meta.RefinedDiscrTree.instInhabitedTrie {α : Type} : Inhabited (Trie α)

Equations

• Lean.Meta.RefinedDiscrTree.instInhabitedTrie = { default := Lean.Meta.RefinedDiscrTree.Trie.node #[] }

def Lean.Meta.RefinedDiscrTree.Trie.mkPath {α : Type} (keys : Array Key) (child : Trie α) : Trie α

Trie.path constructor that only inserts the path if it is non-empty.

Equations

• Lean.Meta.RefinedDiscrTree.Trie.mkPath keys child = if keys.isEmpty = true then child else Lean.Meta.RefinedDiscrTree.Trie.path keys child

def Lean.Meta.RefinedDiscrTree.Trie.singleton {α : Type} (keys : Array Key) (value : α) (i : Nat) : Trie α

Trie constructor for a single value, taking the keys starting at index i.

Equations

• Lean.Meta.RefinedDiscrTree.Trie.singleton keys value i = Lean.Meta.RefinedDiscrTree.Trie.mkPath (let a := keys; ↑(a.toSubarray i)) (Lean.Meta.RefinedDiscrTree.Trie.values #[value])

def Lean.Meta.RefinedDiscrTree.Trie.mkNode2 {α : Type} (k1 : Key) (t1 : Trie α) (k2 : Key) (t2 : Trie α) : Trie α

Trie.node constructor for combining two Key, Trie α pairs.

Equations

• Lean.Meta.RefinedDiscrTree.Trie.mkNode2 k1 t1 k2 t2 = if k1 < k2 then Lean.Meta.RefinedDiscrTree.Trie.node #[(k1, t1), (k2, t2)] else Lean.Meta.RefinedDiscrTree.Trie.node #[(k2, t2), (k1, t1)]

def Lean.Meta.RefinedDiscrTree.Trie.values! {α : Type} : Trie α → Array α

Return the values from a Trie α, assuming that it is a leaf

Equations

• (Lean.Meta.RefinedDiscrTree.Trie.values vs).values! = vs
• x✝.values! = panicWithPosWithDecl "Mathlib.Lean.Meta.RefinedDiscrTree.Basic" "Lean.Meta.RefinedDiscrTree.Trie.values!" 139 9 "expected .values constructor"

def Lean.Meta.RefinedDiscrTree.Trie.children! {α : Type} : Trie α → Array (Key × Trie α)

Return the children of a Trie α, assuming that it is not a leaf. The result is sorted by the Key's

Equations

• One or more equations did not get rendered due to their size.
• (Lean.Meta.RefinedDiscrTree.Trie.node cs).children! = cs
• (Lean.Meta.RefinedDiscrTree.Trie.path ks c).children! = #[(ks[0]!, Lean.Meta.RefinedDiscrTree.Trie.mkPath (let a := ks; ↑(a.toSubarray 1)) c)]

instance Lean.Meta.RefinedDiscrTree.instToFormatTrie {α : Type} [ToFormat α] : ToFormat (Trie α)

Equations

• Lean.Meta.RefinedDiscrTree.instToFormatTrie = { format := Lean.Meta.RefinedDiscrTree.Trie.format✝ }

structure Lean.Meta.RefinedDiscrTree (α : Type) : Type

Discrimination tree. It is an index from expressions to values of type α.

• root : PersistentHashMap Key (Trie α)

  The underlying PersistentHashMap of a RefinedDiscrTree.

instance Lean.Meta.RefinedDiscrTree.instInhabited {α : Type} : Inhabited (RefinedDiscrTree α)

Equations

• Lean.Meta.RefinedDiscrTree.instInhabited = { default := { } }

instance Lean.Meta.RefinedDiscrTree.instToFormat {α : Type} [ToFormat α] : ToFormat (RefinedDiscrTree α)

Equations

• Lean.Meta.RefinedDiscrTree.instToFormat = { format := Lean.Meta.RefinedDiscrTree.format✝ }