Basic Definitions for RefinedDiscrTree

We define

• Key, the discrimination tree key
• LazyEntry, the partial, lazy computation of a sequence of Keys
• Trie, a node of the discrimination tree, which is indexed with Keys and stores an array of pending LazyEntrys
• RefinedDiscrTree, the discrimination tree itself.

inductive Lean.Meta.RefinedDiscrTree.Key : Type

Discrimination tree key.

• star : Key

  A metavariable. This key matches with anything.

• labelledStar (id : Nat) : Key

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

• opaque : Key

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

• const (declName : Name) (nargs : Nat) : Key

  A constant. It stores the name and the arity.

• fvar (fvarId : FVarId) (nargs : Nat) : Key

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

• bvar (deBruijnIndex nargs : Nat) : Key

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

• lit (v : Literal) : Key

  A literal.

• sort : Key

  A sort. Universe levels are ignored.

• lam : Key

  A lambda function.

• forall : Key

  A dependent arrow.

• proj (typeName : Name) (idx nargs : 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.instInhabitedKey.default }

def Lean.Meta.RefinedDiscrTree.instInhabitedKey.default : Key

Equations

• Lean.Meta.RefinedDiscrTree.instInhabitedKey.default = Lean.Meta.RefinedDiscrTree.Key.star

instance Lean.Meta.RefinedDiscrTree.instBEqKey : BEq Key

Equations

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

def Lean.Meta.RefinedDiscrTree.instBEqKey.beq : Key → Key → Bool

Equations

• Lean.Meta.RefinedDiscrTree.instBEqKey.beq Lean.Meta.RefinedDiscrTree.Key.star Lean.Meta.RefinedDiscrTree.Key.star = true
• Lean.Meta.RefinedDiscrTree.instBEqKey.beq (Lean.Meta.RefinedDiscrTree.Key.labelledStar a) (Lean.Meta.RefinedDiscrTree.Key.labelledStar b) = (a == b)
• Lean.Meta.RefinedDiscrTree.instBEqKey.beq Lean.Meta.RefinedDiscrTree.Key.opaque Lean.Meta.RefinedDiscrTree.Key.opaque = true
• Lean.Meta.RefinedDiscrTree.instBEqKey.beq (Lean.Meta.RefinedDiscrTree.Key.const a a_1) (Lean.Meta.RefinedDiscrTree.Key.const b b_1) = (a == b && a_1 == b_1)
• Lean.Meta.RefinedDiscrTree.instBEqKey.beq (Lean.Meta.RefinedDiscrTree.Key.fvar a a_1) (Lean.Meta.RefinedDiscrTree.Key.fvar b b_1) = (a == b && a_1 == b_1)
• Lean.Meta.RefinedDiscrTree.instBEqKey.beq (Lean.Meta.RefinedDiscrTree.Key.bvar a a_1) (Lean.Meta.RefinedDiscrTree.Key.bvar b b_1) = (a == b && a_1 == b_1)
• Lean.Meta.RefinedDiscrTree.instBEqKey.beq (Lean.Meta.RefinedDiscrTree.Key.lit a) (Lean.Meta.RefinedDiscrTree.Key.lit b) = (a == b)
• Lean.Meta.RefinedDiscrTree.instBEqKey.beq Lean.Meta.RefinedDiscrTree.Key.sort Lean.Meta.RefinedDiscrTree.Key.sort = true
• Lean.Meta.RefinedDiscrTree.instBEqKey.beq Lean.Meta.RefinedDiscrTree.Key.lam Lean.Meta.RefinedDiscrTree.Key.lam = true
• Lean.Meta.RefinedDiscrTree.instBEqKey.beq Lean.Meta.RefinedDiscrTree.Key.forall Lean.Meta.RefinedDiscrTree.Key.forall = true
• Lean.Meta.RefinedDiscrTree.instBEqKey.beq (Lean.Meta.RefinedDiscrTree.Key.proj a a_1 a_2) (Lean.Meta.RefinedDiscrTree.Key.proj b b_1 b_2) = (a == b && (a_1 == b_1 && a_2 == b_2))
• Lean.Meta.RefinedDiscrTree.instBEqKey.beq x✝¹ x✝ = false

instance Lean.Meta.RefinedDiscrTree.instHashableKey : Hashable Key

Equations

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

instance Lean.Meta.RefinedDiscrTree.instToFormatKey : ToFormat Key

Equations

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

def Lean.Meta.RefinedDiscrTree.keysAsPattern (keys : Array Key) : CoreM MessageData

Converts an entry (i.e., List Key) to the discrimination tree into MessageData that is more user-friendly.

This is a copy of Lean.Meta.DiscrTree.keysAsPattern

Equations

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

def Lean.Meta.RefinedDiscrTree.keysAsPattern.next (keys : Array Key) : StateRefT' IO.RealWorld (List Key) CoreM Key

Get the next key.

Equations

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

partial def Lean.Meta.RefinedDiscrTree.keysAsPattern.mkApp (keys : Array Key) (f : MessageData) (nargs : Nat) (paren : Bool) : StateRefT' IO.RealWorld (List Key) CoreM MessageData

Format the application f args.

partial def Lean.Meta.RefinedDiscrTree.keysAsPattern.go (keys : Array Key) (paren : Bool := true) : StateRefT' IO.RealWorld (List Key) CoreM MessageData

Format the next expression.

def Lean.Meta.RefinedDiscrTree.keysAsPattern.parenthesize (msg : MessageData) (paren : Bool) : MessageData

Add parentheses if paren == true.

Equations

• Lean.Meta.RefinedDiscrTree.keysAsPattern.parenthesize msg paren = if paren = true then msg.paren else msg.group

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

Return the number of arguments that the Key takes.

Equations

• (Lean.Meta.RefinedDiscrTree.Key.const declName nargs).arity = nargs
• (Lean.Meta.RefinedDiscrTree.Key.fvar fvarId nargs).arity = nargs
• (Lean.Meta.RefinedDiscrTree.Key.bvar deBruijnIndex nargs).arity = nargs
• Lean.Meta.RefinedDiscrTree.Key.lam.arity = 1
• Lean.Meta.RefinedDiscrTree.Key.forall.arity = 2
• (Lean.Meta.RefinedDiscrTree.Key.proj typeName idx nargs).arity = nargs + 1
• x✝.arity = 0

structure Lean.Meta.RefinedDiscrTree.ExprInfo : Type

The information for computing the keys of a subexpression.

• expr : Expr

  The expression

• bvars : List FVarId

  Variables that come from a lambda or forall binder. The list index gives the De Bruijn index.

• lctx : LocalContext

  The local context, which contains the introduced bound variables.

• localInsts : LocalInstances

  The local instances, which may contain the introduced bound variables.

• cfg : Config

  The Meta.Config used by this entry.

def Lean.Meta.RefinedDiscrTree.mkExprInfo (expr : Expr) (bvars : List FVarId) : MetaM ExprInfo

Creates an ExprInfo using the current context.

Equations

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

inductive Lean.Meta.RefinedDiscrTree.StackEntry : Type

The possible values that can appear in the stack

• star : StackEntry

  .star is an expression that will not be explicitly indexed.

• expr (info : ExprInfo) : StackEntry

  .expr is an expression that will be indexed.

instance Lean.Meta.RefinedDiscrTree.instToFormatStackEntry : ToFormat StackEntry

Equations

• Lean.Meta.RefinedDiscrTree.instToFormatStackEntry = { format := Lean.Meta.RefinedDiscrTree.StackEntry.format✝ }

structure Lean.Meta.RefinedDiscrTree.LazyEntry : Type

A LazyEntry represents a snapshot of the computation of encoding an Expr as Array Key. This is used for computing the keys one by one.

• previous : Option ExprInfo

  If an expression creates more entries in the stack, for example because it is an application, then instead of pushing to the stack greedily, we only extend the stack once we need to. So, the field previous is used to extend the stack before looking in the stack.

  For example in 10.add (20.add 30), after computing the key ⟨Nat.add, 2⟩, the stack is still empty, and previous will be 10.add (20.add 30).

• stack : List StackEntry

  The stack, used to emulate recursion. It contains the list of all expressions for which the keys still need to be computed, in that order.

  For example in 10.add (20.add 30), after computing the keys ⟨Nat.add, 2⟩ and 10, the stack will be a list of length 1 containing the expression 20.add 30.

• mctx : MetavarContext

  The metavariable context, which may contain variables appearing in this entry.

• labelledStars? : Option (Array MVarId)

  MVarIds corresponding to the .labelledStar labels. The index in the array is the label. It is none if we use .star instead of labelledStar, for example when encoding the lookup expression.

• computedKeys : List Key

  The Keys that have already been computed.

  Sometimes, more than one Key ends up being computed in one go. This happens when there are lambda binders (because it depends on the body whether the lambda key should be indexed or not). In that case the remaining Keys are stored in results.

def Lean.Meta.RefinedDiscrTree.instInhabitedLazyEntry.default : LazyEntry

Equations

• Lean.Meta.RefinedDiscrTree.instInhabitedLazyEntry.default = { previous := default, stack := default, mctx := default, labelledStars? := default, computedKeys := default }

instance Lean.Meta.RefinedDiscrTree.instInhabitedLazyEntry : Inhabited LazyEntry

Equations

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

def Lean.Meta.RefinedDiscrTree.mkInitLazyEntry (labelledStars : Bool) : MetaM LazyEntry

Creates a LazyEntry using the current metavariable context.

Equations

• Lean.Meta.RefinedDiscrTree.mkInitLazyEntry labelledStars = do let __do_lift ← Lean.getMCtx pure { mctx := __do_lift, labelledStars? := if labelledStars = true then some #[] else none }

instance Lean.Meta.RefinedDiscrTree.instToFormatLazyEntry : ToFormat LazyEntry

Equations

• Lean.Meta.RefinedDiscrTree.instToFormatLazyEntry = { format := Lean.Meta.RefinedDiscrTree.LazyEntry.format✝ }

@[reducible, inline]

abbrev Lean.Meta.RefinedDiscrTree.TrieIndex : Type

Array index of a Trie α in the tries of a RefinedDiscrTree.

Equations

• Lean.Meta.RefinedDiscrTree.TrieIndex = Nat

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

Discrimination tree trie. See RefinedDiscrTree.

A Trie will normally have exactly one of the following

• nonempty values
• nonempty stars, labelledStars and/or children
• nonempty pending But defining it as a structure that can have all at the same time turns out to be easier.

• node :: (
• values : Array α

  Return values, at a leaf

• star : Option TrieIndex

  Following Tries based on a Key.star.

• labelledStars : Std.HashMap Nat TrieIndex

  Following Tries based on a Key.labelledStar.

• children : Std.HashMap Key TrieIndex

  Following Tries based on the Key.

• pending : Array (LazyEntry × α)

  Lazy entries that still have to be evaluated.

• )

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

Equations

• Lean.Meta.RefinedDiscrTree.instInhabitedTrie = { default := { values := #[], star := none, labelledStars := ∅, children := ∅, pending := #[] } }

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

Lazy refined discrimination tree. It is an index from expressions to values of type α.

We store all of the nodes in one Array, tries, instead of using a 'normal' inductive type. This is so that we can modify the tree globally, which is very useful when evaluating lazy entries and saving the result globally.

• root : Std.HashMap Key TrieIndex

  Tries at the root based of the Key.

• tries : Array (Trie α)

  Array of trie entries. Should be owned by this trie.

def Lean.Meta.instInhabitedRefinedDiscrTree.default {a✝ : Type} : RefinedDiscrTree a✝

Equations

• Lean.Meta.instInhabitedRefinedDiscrTree.default = { root := default, tries := default }

instance Lean.Meta.instInhabitedRefinedDiscrTree {a✝ : Type} : Inhabited (RefinedDiscrTree a✝)

Equations

• Lean.Meta.instInhabitedRefinedDiscrTree = { default := Lean.Meta.instInhabitedRefinedDiscrTree.default }

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

Equations

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