Lean4
/-- Given an expression, generate a matcher for it.
The `boundFVars` hash map records which state variables certain fvars correspond to.
The `localFVars` hash map records which local variable the matcher should use for an exact
expression match.
If it succeeds generating a matcher, returns
1. a list of keys that should be used for the `delab` attribute
when defining the elaborator
2. a `Term` that represents a `Matcher` for the given expression `e`. -/
partial def exprToMatcher (boundFVars : Std.HashMap FVarId Name) (localFVars : Std.HashMap FVarId Term) (e : Expr) :
OptionT TermElabM (List DelabKey × Term) := do
match e with
| .mvar .. =>
return ([], ← `(pure))
| .const n _ =>
return ([.app n 0], ← ``(matchExpr (Expr.isConstOf · $(quote n))))
| .sort u =>
/-
We should try being more accurate here.
Prop / Type / Type _ / Sort _ is at least an OK approximation.
We mimic the core Sort delaborator `Lean.PrettyPrinter.Delaborator.delabSort`.
-/
let matcher ←
if u.isZero then
``(matchExpr Expr.isProp)
else if e.isType0 then
``(matchExpr Expr.isType0)
else if u.dec.isSome then
``(matchExpr isType')
else
``(matchExpr Expr.isSort)
return ([.other `sort], matcher)
| .fvar fvarId =>
if let some n := boundFVars[fvarId]? then
-- This fvar is a pattern variable.
return ([], ← ``(matchVar $(quote n)))
else if let some s := localFVars[fvarId]? then
-- This fvar is bound by a lambda or forall expression in the pattern itself
return ([], ← ``(matchExpr (· == $s)))
else
let n ← fvarId.getUserName
if n.hasMacroScopes then
-- Match by just the type; this is likely an unnamed instance for example
let (_, m) ← exprToMatcher boundFVars localFVars (← instantiateMVars (← inferType e))
return ([.other `fvar], ← ``(matchTypeOf $m))
else
-- This is an fvar from a `variable`. Match by name and type.
let (_, m) ← exprToMatcher boundFVars localFVars (← instantiateMVars (← inferType e))
return ([.other `fvar], ← ``(matchFVar $(quote n) $m))
| .app .. =>
e.withApp fun f args => do
let (keys, matchF) ←
if let .const n _ := f then
pure ([.app n args.size], ← ``(matchExpr (Expr.isConstOf · $(quote n))))
else
let (_, matchF) ← exprToMatcher boundFVars localFVars f
pure ([.app none args.size], matchF)
let mut fty ← inferType f
let mut matcher := matchF
for arg in args do
fty ← whnf fty
guard fty.isForall
let bi := fty.bindingInfo!
fty := fty.bindingBody!.instantiate1 arg
if bi.isInstImplicit then
-- Assumption: elaborated instances are canonical, so no need to match.
-- The type of the instance is already accounted for by the previous arguments
-- and the type of `f`.
matcher ← ``(matchApp $matcher pure)
else
let (_, matchArg) ← exprToMatcher boundFVars localFVars arg
matcher ← ``(matchApp $matcher $matchArg)
return (keys, matcher)
| .lit (.natVal n) =>
return ([.other `lit], ← ``(natLitMatcher $(quote n)))
| .forallE n t b bi =>
let (_, matchDom) ← exprToMatcher boundFVars localFVars t
withLocalDecl n bi t fun arg =>
withFreshMacroScope
(do
let n' ← `(n)
let body := b.instantiate1 arg
let localFVars' := localFVars.insert arg.fvarId! n'
let (_, matchBody) ← exprToMatcher boundFVars localFVars' body
return ([.other `forallE], ← ``(matchForall $matchDom (fun $n' => $matchBody))))
| .lam n t b bi =>
let (_, matchDom) ← exprToMatcher boundFVars localFVars t
withLocalDecl n bi t fun arg =>
withFreshMacroScope
(do
let n' ← `(n)
let body := b.instantiate1 arg
let localFVars' := localFVars.insert arg.fvarId! n'
let (_, matchBody) ← exprToMatcher boundFVars localFVars' body
return ([.other `lam], ← ``(matchLambda $matchDom (fun $n' => $matchBody))))
| _ =>
trace[notation3]"can't generate matcher for {e}"
failure
