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 : ℕ) : 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 : ℕ) : Key

  A constant. It stores the name and the arity.

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

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

• bvar (deBruijnIndex nargs : ℕ) : 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 : ℕ) : Key

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

@[implicit_reducible]

instance Lean.Meta.RefinedDiscrTree.instInhabitedKey : Inhabited Key

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

@[implicit_reducible]

instance Lean.Meta.RefinedDiscrTree.instBEqKey : BEq Key

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

def Lean.Meta.RefinedDiscrTree.Key.hash : Key → UInt64

Compute the hash of a RefinedDiscrTree.Key.

Note: at the root, .const is the most common key, and it is very uncommon to get the same constant name with a different arity. So for performance, we just use hash name to hash .const name _.

@[implicit_reducible]

instance Lean.Meta.RefinedDiscrTree.instHashableKey : Hashable Key

def Lean.Meta.RefinedDiscrTree.Key.format : Key → Format

Format a RefinedDiscrTree.Key.

@[implicit_reducible]

instance Lean.Meta.RefinedDiscrTree.instToFormatKey : ToFormat Key

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

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

Get the next key.

partial def Lean.Meta.RefinedDiscrTree.keysAsPattern.mkApp (keys : Array Key) (f : MessageData) (nargs : ℕ) (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.

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

Return the number of arguments that the Key takes.

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.

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.

def Lean.Meta.RefinedDiscrTree.StackEntry.format : StackEntry → Format

Format a RefinedDiscrTree.StackEntry.

@[implicit_reducible]

instance Lean.Meta.RefinedDiscrTree.instToFormatStackEntry : ToFormat StackEntry

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

@[implicit_reducible]

instance Lean.Meta.RefinedDiscrTree.instInhabitedLazyEntry : Inhabited LazyEntry

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

Creates a LazyEntry using the current metavariable context.

def Lean.Meta.RefinedDiscrTree.LazyEntry.format (entry : LazyEntry) : Format

Format a RefinedDiscrTree.LazyEntry.

@[implicit_reducible]

instance Lean.Meta.RefinedDiscrTree.instToFormatLazyEntry : ToFormat LazyEntry

@[reducible, inline]

abbrev Lean.Meta.RefinedDiscrTree.TrieIndex : Type

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

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 ℕ 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.

• )

@[implicit_reducible]

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

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.

@[implicit_reducible]

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

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

def Lean.Meta.RefinedDiscrTree.format {α : Type} [ToFormat α] (tree : RefinedDiscrTree α) : Format

Format a RefinedDiscrTree as a flowchart.

• Non-terminal nodes are of the form {key} =>, followed by all of the following nodes, indented with 2 more spaces.
• Terminal nodes have either "entries", containing the return values, or "pending entries", for nodes that have not been evaluated/expanded.

For example:

Discrimination tree flowchart:
⟨HMul.hMul, 6⟩ =>
  ⟨Int, 0⟩ =>
    ⟨Int, 0⟩ =>
      * =>
        * =>
          *0 =>
            *0 =>
              pending entries: #[mul_self]
            *1 =>
              entries: #[mul_comm]
            ⟨Neg.neg, 3⟩ =>
              ⟨Int, 0⟩ =>
                * =>
                  *1 =>
                    entries: #[mul_neg]
            1 =>
              pending entries: #[mul_one]
          ⟨Neg.neg, 3⟩ =>
            pending entries: #[neg_mul]
          1 =>
            *0 =>
              entries: #[one_mul]

partial def Lean.Meta.RefinedDiscrTree.format.go {α : Type} [ToFormat α] (tree : RefinedDiscrTree α) (trie : TrieIndex) : Format

Auxiliary function for RefinedDiscrTree.format.

@[implicit_reducible]

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