Matching with a RefinedDiscrTree

This file defines the matching procedure for the RefinedDiscrTree.

The main definitions are

• The structure MatchResult, which contains the match results, ordered by matching score.
• The (private) function evalNode which evaluates a node of the RefinedDiscrTree
• The (private) function getMatchLoop, which is the main function that computes the matches. It implements the non-deterministic computation by keeping a stack of PartialMatches, and repeatedly processing the most recent one.
• The matching function getMatch that also returns an updated RefinedDiscrTree

To find the matches, we first encode the expression as a List Key. Then using this, we find all matches with the tree. When unify == true, we also allow metavariables in the target expression to be assigned.

We use a simple unification algorithm. For all star/metavariable patterns in the RefinedDiscrTree (and in the target if unify == true), we store the assignment, and when it is attempted to be assigned again, we check that it is the same assignment.

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

A match result contains the results from matching a term against patterns in the discrimination tree.

• elts : Std.TreeMap Nat (Array (Array α)) compare

  The elements in the match result.

  The Nat in the tree map represents the score of the results. The elements are arrays of arrays, where each sub-array corresponds to one discr tree pattern.

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

Equations

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

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

Equations

• Lean.Meta.RefinedDiscrTree.instInhabitedMatchResult.default = { elts := default }

def Lean.Meta.RefinedDiscrTree.MatchResult.toArray {α : Type} (mr : MatchResult α) : Array α

Convert a MatchResult into a Array, with better matches at the start of the array.

Equations

• mr.toArray = Std.TreeMap.foldr (fun (x : Nat) (a : Array (Array α)) (r : Array α) => Array.foldl (fun (x1 x2 : Array α) => x1 ++ x2) r a) #[] mr.elts

def Lean.Meta.RefinedDiscrTree.MatchResult.flatten {α : Type} (mr : MatchResult α) : Array (Array α)

Convert a MatchResult into an Array of Arrays. Each Array corresponds to one pattern. The better matching patterns are at the start of the outer array. For each inner array, the entries are ordered in the order they were inserted.

Equations

• mr.flatten = Std.TreeMap.foldr (fun (x : Nat) (arr cand : Array (Array α)) => cand ++ arr) #[] mr.elts

def Lean.Meta.RefinedDiscrTree.instInhabitedPartialMatch.default : Lean.Meta.RefinedDiscrTree.PartialMatch✝

Equations

• Lean.Meta.RefinedDiscrTree.instInhabitedPartialMatch.default = { keys := default, score := default, trie := default, treeStars := default }

instance Lean.Meta.RefinedDiscrTree.instInhabitedPartialMatch : Inhabited Lean.Meta.RefinedDiscrTree.PartialMatch✝

Equations

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

def Lean.Meta.RefinedDiscrTree.getMatch {α : Type} (d : RefinedDiscrTree α) (e : Expr) (unify matchRootStar : Bool) : MetaM (Except Exception (MatchResult α) × RefinedDiscrTree α)

Find values that match e in d.

• If unify == true then metavariables in e can be assigned.
• If matchRootStar == true then we allow metavariables at the root to unify. Set this to false to avoid getting excessively many results.

Note: to preserve the reference to d, getMatch will never throw an error, and instead it returns an Except Exception (MatchResult α).

Equations

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