Matching with a RefinedDiscrTree

We use a very simple unification algorithm. For all star/metavariable patterns in the RefinedDiscrTree and in the target, we store the assignment, and when it is assigned again, we check that it is the same assignment.

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

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

partial def Lean.Meta.RefinedDiscrTree.GetUnify.skipEntries {α : Type} (t : Trie α) (skipped : Array Key) : ℕ → Lean.Meta.RefinedDiscrTree.GetUnify.M✝ (Array Key × Trie α)

Return the possible Trie α that match with n metavariable.

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

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

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

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

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

Return the possible Trie α that match with e.

@[specialize #[]]

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

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

def Lean.Meta.RefinedDiscrTree.getMatchWithScore {α : Type} (d : RefinedDiscrTree α) (e : Expr) (unify : Bool) (allowRootStar : Bool := false) : MetaM (Array (Array α × ℕ))

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

def Lean.Meta.RefinedDiscrTree.getMatchWithScoreWithExtra {α : Type} (d : RefinedDiscrTree α) (e : Expr) (unify : Bool) (allowRootStar : Bool := false) : MetaM (Array (Array α × ℕ × ℕ))

Similar to getMatchWithScore, but also returns matches with prefixes of e. We store the score, followed by the number of ignored arguments.

partial def Lean.Meta.RefinedDiscrTree.getMatchWithScoreWithExtra.go {α : Type} (d : RefinedDiscrTree α) (unify : Bool) (allowRootStar : Bool := false) (e : Expr) (numIgnored : ℕ) : MetaM (Array (Array α × ℕ × ℕ))

go