Lean4
/-- 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 α)`.
-/
def getMatch (d : RefinedDiscrTree α) (e : Expr) (unify matchRootStar : Bool) :
MetaM (Except Exception (MatchResult α) × RefinedDiscrTree α) := do
withReducible do
runTreeM d
(do
let (key, keys) ← encodeExpr e (labelledStars := false)
let pMatch : PartialMatch := { keys, score := 0, trie := default }
if key == .star then
if matchRootStar then
if unify then
matchEverything d.root
else
matchTreeRootStar d.root
else
return { }
else
let todo := matchKey key d.root pMatch #[]
if matchRootStar then
getMatchLoop todo (← matchTreeRootStar d.root) unify
else
getMatchLoop todo { } unify)
