RefinedDiscrTree discrimination tree with refined indexing

We define discrimination trees for the purpose of unifying local expressions with library results.

This implementation is based on the DiscrTree in Lean. I document here what is not in the original.

• The constructor Key.star now takes a Nat identifier as an argument. For example, the library pattern a+a is encoded as [⟨Hadd.hadd, 6⟩, *0, *0, *0, *1, *2, *2]. *0 corresponds to the type of a, *1 to the Hadd instance, and *2 to a. This means that it will only match an expression x+y if x is definitionally equal to y.

• The constructor Key.opaque has been introduced in order to index existential variables in lemmas like Nat.exists_prime_and_dvd {n : ℕ} (hn : n ≠ 1) : ∃ p, Prime p ∧ p ∣ n, where the part Prime p gets the pattern [⟨Nat.Prime, 1⟩, ◾]. (◾ represents Key.opaque)

• The constructors Key.lam, Key.forall and Key.bvar have been introduced in order to allow for patterns under binders. For example, this allows for more specific matching with the left hand side of Finset.sum_range_id (n : ℕ) : ∑ i in range n, i = n * (n - 1) / 2, which is indexed by [⟨Finset.sum, 5⟩, ⟨Nat, 0⟩, ⟨Nat, 0⟩, *0, ⟨Finset.Range, 1⟩, *1, λ, ⟨#0, 0⟩]

• We keep track of the matching score of a unification. This score represent the number of keys that had to be the same for the unification to succeed. For example, matching (1 + 2) + 3 with add_comm gives a score of 3, since the pattern of commutativity is [⟨Hadd.hadd, 6⟩, *0, *0, *0, *1, *2, *3], so matching ⟨Hadd.hadd, 6⟩ gives 1 point, and matching *0 two times after its first appearance gives another 2 points. Similarly, matching it with add_assoc gives a score of 7.

  TODO?: the third type parameter of Hadd.hadd is an outparam, so its matching should not be counted in the score.

• Patterns that have the potential to be η-reduced are put into the RefinedDiscrTree under all possible reduced key sequences. This is for terms of the form fun x => f (?m x₁ .. xₙ), where ?m is a metavariable, and for some i, xᵢ = x. For example, the pattern Continuous fun y => Real.exp (f y)]) is indexed by [⟨Continuous, 5⟩, *0, ⟨Real, 0⟩, *1, *2, λ, ⟨Real.exp⟩, *3] and by [⟨Continuous, 5⟩, *0, ⟨Real, 0⟩, *1, *2, ⟨Real.exp⟩] so that it also comes up if you search with Continuous Real.exp. Similarly, Continuous fun x => f x + g x is indexed by [⟨Continuous, 1⟩, λ, ⟨Hadd.hadd, 6⟩, *0, *0, *0, *1, *2, *3] and by [⟨Continuous, 1⟩, ⟨Hadd.hadd, 5⟩, *0, *0, *0, *1, *2].

inductive Mathlib.Meta.FunProp.RefinedDiscrTree.Key : Type

Discrimination tree key.

• star: Nat → Mathlib.Meta.FunProp.RefinedDiscrTree.Key

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

• opaque: Mathlib.Meta.FunProp.RefinedDiscrTree.Key

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

• const: Lean.Name → Nat → Mathlib.Meta.FunProp.RefinedDiscrTree.Key

  A constant. It stores a Name and an arity.

• fvar: Lean.FVarId → Nat → Mathlib.Meta.FunProp.RefinedDiscrTree.Key

  A free variable. It stores a FVarId and an arity.

• bvar: Nat → Nat → Mathlib.Meta.FunProp.RefinedDiscrTree.Key

  A bound variable, from either a .lam or a .forall. It stores an index and an arity.

• lit: Lean.Literal → Mathlib.Meta.FunProp.RefinedDiscrTree.Key

  A literal.

• sort: Mathlib.Meta.FunProp.RefinedDiscrTree.Key

  A sort. Universe levels are ignored.

• lam: Mathlib.Meta.FunProp.RefinedDiscrTree.Key

  A lambda function.

• forall: Mathlib.Meta.FunProp.RefinedDiscrTree.Key

  A dependent arrow.

• proj: Lean.Name → Nat → Nat → Mathlib.Meta.FunProp.RefinedDiscrTree.Key

  A projection. It takes the constructor name, the projection index and the arity.

instance Mathlib.Meta.FunProp.RefinedDiscrTree.instInhabitedKey : Inhabited Mathlib.Meta.FunProp.RefinedDiscrTree.Key

Equations

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

instance Mathlib.Meta.FunProp.RefinedDiscrTree.instBEqKey : BEq Mathlib.Meta.FunProp.RefinedDiscrTree.Key

Equations

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

instance Mathlib.Meta.FunProp.RefinedDiscrTree.instReprKey : Repr Mathlib.Meta.FunProp.RefinedDiscrTree.Key

Equations

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

instance Mathlib.Meta.FunProp.RefinedDiscrTree.instHashableKey : Hashable Mathlib.Meta.FunProp.RefinedDiscrTree.Key

Equations

• Mathlib.Meta.FunProp.RefinedDiscrTree.instHashableKey = { hash := Mathlib.Meta.FunProp.RefinedDiscrTree.Key.hash }

def Mathlib.Meta.FunProp.RefinedDiscrTree.Key.ctorIdx : Mathlib.Meta.FunProp.RefinedDiscrTree.Key → Nat

Constructor index as a help 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

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

instance Mathlib.Meta.FunProp.RefinedDiscrTree.instLTKey : LT Mathlib.Meta.FunProp.RefinedDiscrTree.Key

Equations

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

instance Mathlib.Meta.FunProp.RefinedDiscrTree.instDecidableLtKeyInstLTKey (a : Mathlib.Meta.FunProp.RefinedDiscrTree.Key) (b : Mathlib.Meta.FunProp.RefinedDiscrTree.Key) : Decidable (a < b)

Equations

• Mathlib.Meta.FunProp.RefinedDiscrTree.instDecidableLtKeyInstLTKey a b = inferInstanceAs (Decidable (Mathlib.Meta.FunProp.RefinedDiscrTree.Key.lt a b = true))

instance Mathlib.Meta.FunProp.RefinedDiscrTree.instToFormatKey : Lean.ToFormat Mathlib.Meta.FunProp.RefinedDiscrTree.Key

Equations

• Mathlib.Meta.FunProp.RefinedDiscrTree.instToFormatKey = { format := Mathlib.Meta.FunProp.RefinedDiscrTree.Key.format }

def Mathlib.Meta.FunProp.RefinedDiscrTree.Key.arity : Mathlib.Meta.FunProp.RefinedDiscrTree.Key → Nat

Return the number of arguments that the Key takes.

Equations

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

inductive Mathlib.Meta.FunProp.RefinedDiscrTree.Trie (α : Type) : Type

Discrimination tree trie. See RefinedDiscrTree.

• node: {α : Type} → Array (Mathlib.Meta.FunProp.RefinedDiscrTree.Key × Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α) → Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α

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

• path: {α : Type} → Array Mathlib.Meta.FunProp.RefinedDiscrTree.Key → Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α → Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α

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

• values: {α : Type} → Array α → Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α

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

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

Equations

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

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

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

Equations

• Mathlib.Meta.FunProp.RefinedDiscrTree.Trie.mkPath keys child = if Array.isEmpty keys = true then child else Mathlib.Meta.FunProp.RefinedDiscrTree.Trie.path keys child

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

Trie constructor for a single value.

Equations

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

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

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

Equations

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

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

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

Equations

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

def Mathlib.Meta.FunProp.RefinedDiscrTree.Trie.children! {α : Type} : Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α → Array (Mathlib.Meta.FunProp.RefinedDiscrTree.Key × Mathlib.Meta.FunProp.RefinedDiscrTree.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.

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

Equations

• Mathlib.Meta.FunProp.RefinedDiscrTree.instToFormatTrie = { format := Mathlib.Meta.FunProp.RefinedDiscrTree.Trie.format }

structure Mathlib.Meta.FunProp.RefinedDiscrTree (α : Type) : Type

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

• root : Lean.PersistentHashMap Mathlib.Meta.FunProp.RefinedDiscrTree.Key (Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α)

  The underlying PersistentHashMap of a RefinedDiscrTree.

instance Mathlib.Meta.FunProp.RefinedDiscrTree.instInhabitedRefinedDiscrTree : {a : Type} → Inhabited (Mathlib.Meta.FunProp.RefinedDiscrTree a)

Equations

• Mathlib.Meta.FunProp.RefinedDiscrTree.instInhabitedRefinedDiscrTree = { default := { root := default } }

instance Mathlib.Meta.FunProp.RefinedDiscrTree.instToFormatRefinedDiscrTree {α : Type} [Lean.ToFormat α] : Lean.ToFormat (Mathlib.Meta.FunProp.RefinedDiscrTree α)

Equations

• Mathlib.Meta.FunProp.RefinedDiscrTree.instToFormatRefinedDiscrTree = { format := Mathlib.Meta.FunProp.RefinedDiscrTree.RefinedDiscrTree.format }

inductive Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr : Type

DTExpr is a simplified form of Expr. It is intermediate step in converting from Expr to Array Key.

• star: Option Lean.MVarId → Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr

  A metavariable.

• opaque: Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr

  An opaque variable.

• const: Lean.Name → Array Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr → Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr

  A constant.

• fvar: Lean.FVarId → Array Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr → Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr

  A free variable.

• bvar: Nat → Array Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr → Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr

  A bound variable.

• lit: Lean.Literal → Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr

  A literal.

• sort: Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr

  A sort.

• lam: Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr → Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr

  A lambda function.

• forall: Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr → Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr → Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr

  A dependent arrow.

• proj: Lean.Name → Nat → Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr → Array Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr → Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr

  A projection.

instance Mathlib.Meta.FunProp.RefinedDiscrTree.instInhabitedDTExpr : Inhabited Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr

Equations

• Mathlib.Meta.FunProp.RefinedDiscrTree.instInhabitedDTExpr = { default := Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr.star default }

instance Mathlib.Meta.FunProp.RefinedDiscrTree.instBEqDTExpr : BEq Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr

Equations

• Mathlib.Meta.FunProp.RefinedDiscrTree.instBEqDTExpr = { beq := Mathlib.Meta.FunProp.RefinedDiscrTree.beqDTExpr✝ }

instance Mathlib.Meta.FunProp.RefinedDiscrTree.instToFormatDTExpr : Lean.ToFormat Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr

Equations

• Mathlib.Meta.FunProp.RefinedDiscrTree.instToFormatDTExpr = { format := Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr.format }

partial def Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr.size : Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr → Nat

Return the size of the DTExpr. This is used for calculating the matching score when two expressions are equal. The score is not incremented at a lambda, which is so that the expressions ∀ x, p[x] and ∃ x, p[x] get the same size.

def Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr.flatten (e : Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr) (initCapacity : optParam Nat 16) : Array Mathlib.Meta.FunProp.RefinedDiscrTree.Key

Given a DTExpr, return the linearized encoding in terms of Key, which is used for RefinedDiscrTree indexing.

Equations

• Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr.flatten e initCapacity = StateT.run' (Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr.flattenAux (Array.mkEmpty initCapacity) e) { stars := #[] }

partial def Mathlib.Meta.FunProp.RefinedDiscrTree.reduce (e : Lean.Expr) (config : Lean.Meta.WhnfCoreConfig) : Lean.MetaM Lean.Expr

Reduction procedure for the RefinedDiscrTree indexing.

def Mathlib.Meta.FunProp.RefinedDiscrTree.isStar : Lean.Expr → Bool

Check whether the expression is represented by Key.star.

Equations

• Mathlib.Meta.FunProp.RefinedDiscrTree.isStar (Lean.Expr.mvar mvarId) = true
• Mathlib.Meta.FunProp.RefinedDiscrTree.isStar (Lean.Expr.app f arg) = Mathlib.Meta.FunProp.RefinedDiscrTree.isStar f
• Mathlib.Meta.FunProp.RefinedDiscrTree.isStar x = false

def Mathlib.Meta.FunProp.RefinedDiscrTree.isStarWithArg (arg : Lean.Expr) : Lean.Expr → Bool

Check whether the expression is represented by Key.star and has arg as an argument.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Meta.FunProp.RefinedDiscrTree.isStarWithArg arg x = false

def Mathlib.Meta.FunProp.RefinedDiscrTree.starEtaExpanded : Lean.Expr → Nat → Option Lean.Expr

If e is of the form (fun x₀ ... xₙ => b y₀ ... yₙ), where each yᵢ has a metavariable head with xᵢ as an argument, then return some b. Otherwise, return none.

Equations

• Mathlib.Meta.FunProp.RefinedDiscrTree.starEtaExpanded (Lean.Expr.lam binderName binderType b binderInfo) x = Mathlib.Meta.FunProp.RefinedDiscrTree.starEtaExpanded b (x + 1)
• Mathlib.Meta.FunProp.RefinedDiscrTree.starEtaExpanded x✝ x = Mathlib.Meta.FunProp.RefinedDiscrTree.starEtaExpandedBody x✝ x 0

def Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr.hasLooseBVars (e : Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr) : Bool

Return true if e contains a loose bound variable.

Equations

• Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr.hasLooseBVars e = Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr.hasLooseBVarsAux 0 e

instance Mathlib.Meta.FunProp.RefinedDiscrTree.MkDTExpr.instMonadCacheExprDTExprM : Lean.MonadCache Lean.Expr Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr Mathlib.Meta.FunProp.RefinedDiscrTree.MkDTExpr.M

Equations

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

partial def Mathlib.Meta.FunProp.RefinedDiscrTree.MkDTExpr.introEtaBVars {α : Type} [Inhabited α] (e : Lean.Expr) (b : Lean.Expr) (k : Lean.Expr → Mathlib.Meta.FunProp.RefinedDiscrTree.MkDTExpr.M α) : Mathlib.Meta.FunProp.RefinedDiscrTree.MkDTExpr.M α

If e is of the form (fun x₁ ... xₙ => b y₁ ... yₙ), then introduce variables for x₁, ..., xₙ, instantiate these in b, and run k on b.

partial def Mathlib.Meta.FunProp.RefinedDiscrTree.MkDTExpr.mkDTExprAux (root : Bool) (e : Lean.Expr) : ReaderT Mathlib.Meta.FunProp.RefinedDiscrTree.MkDTExpr.Context Lean.MetaM Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr

Return the encoding of e as a DTExpr. If root = false, then e is a strict sub expression of the original expression.

partial def Mathlib.Meta.FunProp.RefinedDiscrTree.MkDTExpr.mkDTExprAux.mkDTExprBinder (domain : Lean.Expr) (e : Lean.Expr) : ReaderT Mathlib.Meta.FunProp.RefinedDiscrTree.MkDTExpr.Context Lean.MetaM Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr

Introduce a bound variable of type domain to the context, instantiate it in e, and then return all encodings of e as a DTExpr

partial def Mathlib.Meta.FunProp.RefinedDiscrTree.MkDTExpr.mkDTExprsAux (root : Bool) (e : Lean.Expr) : Mathlib.Meta.FunProp.RefinedDiscrTree.MkDTExpr.M Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr

Return all encodings of e as a DTExpr, taking possible η-reductions into account. If root = false, then e is a strict sub expression of the original expression.

partial def Mathlib.Meta.FunProp.RefinedDiscrTree.MkDTExpr.mkDTExprsAux.mkDTExprsBinder (domain : Lean.Expr) (e : Lean.Expr) : Mathlib.Meta.FunProp.RefinedDiscrTree.MkDTExpr.M Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr

Introduce a bound variable of type domain to the context, instantiate it in e, and then return all encodings of e as a DTExpr

def Mathlib.Meta.FunProp.RefinedDiscrTree.mkDTExpr (e : Lean.Expr) (config : optParam Lean.Meta.WhnfCoreConfig { iota := true, beta := true, proj := Lean.Meta.ProjReductionKind.yesWithDelta, zeta := true }) (fvarInContext : optParam (Lean.FVarId → Bool) fun (x : Lean.FVarId) => false) : Lean.MetaM Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr

Return the encoding of e as a DTExpr. The argument fvarInContext allows you to specify which free variables in e will still be in the context when the RefinedDiscrTree is being used for lookup. It should return true only if the RefinedDiscrTree is build and used locally.

Equations

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

def Mathlib.Meta.FunProp.RefinedDiscrTree.mkDTExprs (e : Lean.Expr) (config : optParam Lean.Meta.WhnfCoreConfig { iota := true, beta := true, proj := Lean.Meta.ProjReductionKind.yesWithDelta, zeta := true }) (fvarInContext : optParam (Lean.FVarId → Bool) fun (x : Lean.FVarId) => false) : Lean.MetaM (List Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr)

Similar to mkDTExpr. Return all encodings of e as a DTExpr, taking possible η-reductions into account.

Equations

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

def Mathlib.Meta.FunProp.RefinedDiscrTree.mkPath (e : Lean.Expr) (config : optParam Lean.Meta.WhnfCoreConfig { iota := true, beta := true, proj := Lean.Meta.ProjReductionKind.yesWithDelta, zeta := true }) : Lean.MetaM (Array Mathlib.Meta.FunProp.RefinedDiscrTree.Key)

Make discr tree path for expression e.

Equations

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

partial def Mathlib.Meta.FunProp.RefinedDiscrTree.insertInTrie {α : Type} [BEq α] (keys : Array Mathlib.Meta.FunProp.RefinedDiscrTree.Key) (v : α) (i : Nat) : Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α → Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α

Insert the value v at index keys : Array Key in a Trie.

def Mathlib.Meta.FunProp.RefinedDiscrTree.insertInRefinedDiscrTree {α : Type} [BEq α] (d : Mathlib.Meta.FunProp.RefinedDiscrTree α) (keys : Array Mathlib.Meta.FunProp.RefinedDiscrTree.Key) (v : α) : Mathlib.Meta.FunProp.RefinedDiscrTree α

Insert the value v at index keys : Array Key in a RefinedDiscrTree.

Equations

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

def Mathlib.Meta.FunProp.RefinedDiscrTree.insertDTExpr {α : Type} [BEq α] (d : Mathlib.Meta.FunProp.RefinedDiscrTree α) (e : Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr) (v : α) : Mathlib.Meta.FunProp.RefinedDiscrTree α

Insert the value v at index e : DTExpr in a RefinedDiscrTree.

Equations

• Mathlib.Meta.FunProp.RefinedDiscrTree.insertDTExpr d e v = Mathlib.Meta.FunProp.RefinedDiscrTree.insertInRefinedDiscrTree d (Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr.flatten e) v

def Mathlib.Meta.FunProp.RefinedDiscrTree.insert {α : Type} [BEq α] (d : Mathlib.Meta.FunProp.RefinedDiscrTree α) (e : Lean.Expr) (v : α) (config : optParam Lean.Meta.WhnfCoreConfig { iota := true, beta := true, proj := Lean.Meta.ProjReductionKind.yesWithDelta, zeta := true }) (fvarInContext : optParam (Lean.FVarId → Bool) fun (x : Lean.FVarId) => false) : Lean.MetaM (Mathlib.Meta.FunProp.RefinedDiscrTree α)

Insert the value v at index e : Expr in a RefinedDiscrTree. The argument fvarInContext allows you to specify which free variables in e will still be in the context when the RefinedDiscrTree is being used for lookup. It should return true only if the RefinedDiscrTree is build and used locally.

Equations

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

def Mathlib.Meta.FunProp.RefinedDiscrTree.GetUnify.findKey {α : Type} (children : Array (Mathlib.Meta.FunProp.RefinedDiscrTree.Key × Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α)) (k : Mathlib.Meta.FunProp.RefinedDiscrTree.Key) : Option (Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α)

If k is a key in children, return the corresponding Trie α. Otherwise return none.

Equations

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

partial def Mathlib.Meta.FunProp.RefinedDiscrTree.GetUnify.skipEntries {α : Type} (t : Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α) (skipped : Array Mathlib.Meta.FunProp.RefinedDiscrTree.Key) : Nat → Mathlib.Meta.FunProp.RefinedDiscrTree.GetUnify.M (Array Mathlib.Meta.FunProp.RefinedDiscrTree.Key × Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α)

Return the possible Trie α that match with n metavariable.

def Mathlib.Meta.FunProp.RefinedDiscrTree.GetUnify.matchTargetStar {α : Type} (mvarId? : Option Lean.MVarId) (t : Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α) : Mathlib.Meta.FunProp.RefinedDiscrTree.GetUnify.M (Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α)

Return the possible Trie α that match with anything. We add 1 to the matching score when the key equals .opaque, since this pattern is "harder" to match with.

Equations

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

def Mathlib.Meta.FunProp.RefinedDiscrTree.GetUnify.matchTreeStars {α : Type} (e : Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr) (t : Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α) : Mathlib.Meta.FunProp.RefinedDiscrTree.GetUnify.M (Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α)

Return the possible Trie α that come from a Key.star, while keeping track of the Key.star assignments.

Equations

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

partial def Mathlib.Meta.FunProp.RefinedDiscrTree.GetUnify.matchExpr {α : Type} (e : Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr) (t : Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α) : Mathlib.Meta.FunProp.RefinedDiscrTree.GetUnify.M (Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α)

Return the possible Trie α that match with e.

partial def Mathlib.Meta.FunProp.RefinedDiscrTree.GetUnify.exactMatch {α : Type} (e : Mathlib.Meta.FunProp.RefinedDiscrTree.DTExpr) (find? : Mathlib.Meta.FunProp.RefinedDiscrTree.Key → Option (Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α)) : Mathlib.Meta.FunProp.RefinedDiscrTree.GetUnify.M (Mathlib.Meta.FunProp.RefinedDiscrTree.GetUnify.M (Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α) ⊕ Option Lean.MVarId)

If the head of e is not a metavariable, return the possible Trie α that exactly match with e.

def Mathlib.Meta.FunProp.RefinedDiscrTree.getMatchWithScore {α : Type} (d : Mathlib.Meta.FunProp.RefinedDiscrTree α) (e : Lean.Expr) (unify : Bool) (config : Lean.Meta.WhnfCoreConfig) (allowRootStar : optParam Bool false) : Lean.MetaM (Array (Array α × Nat))

Return the results from the RefinedDiscrTree that match the given expression, together with their matching scores, in decreasing order of score.

Each entry of type Array α × Nat corresponds to one pattern.

If unify := false, then metavariables in e are treated as opaque variables. This is for when you don't want the matched keys to instantiate metavariables in e.

If allowRootStar := false, then we don't allow e or the matched key in d to be a star pattern.

Equations

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

partial def Mathlib.Meta.FunProp.RefinedDiscrTree.Trie.mapArraysM {α : Type} {m : Type → Type} [Monad m] {β : Type} (t : Mathlib.Meta.FunProp.RefinedDiscrTree.Trie α) (f : Array α → m (Array β)) : m (Mathlib.Meta.FunProp.RefinedDiscrTree.Trie β)

Apply a monadic function to the array of values at each node in a RefinedDiscrTree.

def Mathlib.Meta.FunProp.RefinedDiscrTree.mapArraysM {α : Type} {m : Type → Type} [Monad m] {β : Type} (d : Mathlib.Meta.FunProp.RefinedDiscrTree α) (f : Array α → m (Array β)) : m (Mathlib.Meta.FunProp.RefinedDiscrTree β)

Apply a monadic function to the array of values at each node in a RefinedDiscrTree.

Equations

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

def Mathlib.Meta.FunProp.RefinedDiscrTree.mapArrays {α : Type} {β : Type} (d : Mathlib.Meta.FunProp.RefinedDiscrTree α) (f : Array α → Array β) : Mathlib.Meta.FunProp.RefinedDiscrTree β

Apply a function to the array of values at each node in a RefinedDiscrTree.

Equations

• Mathlib.Meta.FunProp.RefinedDiscrTree.mapArrays d f = Mathlib.Meta.FunProp.RefinedDiscrTree.mapArraysM d f