Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: better support for partial applications in the E-matching procedure #6654

Merged
merged 1 commit into from
Jan 15, 2025
Merged

feat: better support for partial applications in the E-matching procedure #6654

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 12 additions & 2 deletions src/Lean/Meta/Tactic/Grind/EMatch.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -129,6 +129,16 @@ private partial def matchArgs? (c : Choice) (p : Expr) (e : Expr) : OptionT Goal
let c ← matchArg? c pArg eArg
matchArgs? c p.appFn! e.appFn!

/-- Similar to `matchArgs?` but if `p` has fewer arguments than `e`, we match `p` with a prefix of `e`. -/
private partial def matchArgsPrefix? (c : Choice) (p : Expr) (e : Expr) : OptionT GoalM Choice := do
let pn := p.getAppNumArgs
let en := e.getAppNumArgs
guard (pn <= en)
if pn == en then
matchArgs? c p e
else
matchArgs? c p (e.getAppPrefix pn)

/--
Matches pattern `p` with term `e` with respect to choice `c`.
We traverse the equivalence class of `e` looking for applications compatible with `p`.
Expand Down Expand Up @@ -194,7 +204,7 @@ private def processContinue (c : Choice) (p : Expr) : M Unit := do
let n ← getENode app
if n.generation < maxGeneration
&& (n.heqProofs || n.isCongrRoot) then
if let some c ← matchArgs? c p app |>.run then
if let some c ← matchArgsPrefix? c p app |>.run then
let gen := n.generation
let c := { c with gen := Nat.max gen c.gen }
modify fun s => { s with choiceStack := c :: s.choiceStack }
Expand Down Expand Up @@ -300,7 +310,7 @@ private def main (p : Expr) (cnstrs : List Cnstr) : M Unit := do
if (n.heqProofs || n.isCongrRoot) &&
(!useMT || n.mt == gmt) then
withInitApp app do
if let some c ← matchArgs? { cnstrs, assignment, gen := n.generation } p app |>.run then
if let some c ← matchArgsPrefix? { cnstrs, assignment, gen := n.generation } p app |>.run then
modify fun s => { s with choiceStack := [c] }
processChoices

Expand Down
2 changes: 1 addition & 1 deletion src/Lean/Meta/Tactic/Grind/PP.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -101,7 +101,7 @@ private def ppEqcs (goal : Goal) : MetaM (Array MessageData) := do
return result

private def ppEMatchTheorem (thm : EMatchTheorem) : MetaM MessageData := do
let m := m!"{← thm.origin.pp}\n{← inferType thm.proof}\npatterns: {thm.patterns.map ppPattern}"
let m := m!"{← thm.origin.pp}:\n{← inferType thm.proof}\npatterns: {thm.patterns.map ppPattern}"
return .trace { cls := `thm } m #[]

private def ppActiveTheorems (goal : Goal) : MetaM MessageData := do
Expand Down
Loading