max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: make sure stop conv pattern stop at first match

Browse source
This commit is contained in:
Leonardo de Moura 2021-10-10 15:00:53 -07:00
parent e8bdb66dda
commit 04fae18fe4
1 changed files with 10 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/Lean/Elab/Tactic/Conv/Pattern.lean
View file

@ -21,11 +21,17 @@ private def getContext : MetaM Simp.Context := do
config.decide := false
}
def matchPattern (pattern : AbstractMVarsResult) (e : Expr) : MetaM Bool :=
withNewMCtxDepth do
/- TODO: check whether the following is a performance bottleneck. If it is, recall that we used `AbstractMVarsResult` to make
sure we can match the pattern inside of binders. So, it is not needed in most cases. -/
let (_, _, pattern) ← openAbstractMVarsResult pattern
withReducible <| isDefEqGuarded pattern e
private def pre (pattern : AbstractMVarsResult) (found? : IO.Ref (Option Expr)) (e : Expr) : SimpM Simp.Step := do
/- TODO: check whether the following is a performance bottleneck. If it is, recall that we used `AbstractMVarsResult` to make
sure we can match the pattern inside of binders. So, it is not needed in most cases. -/
let (_, _, pattern) ← openAbstractMVarsResult pattern
if (← withReducible <| isDefEqGuarded pattern e) then
if (← found?.get).isSome then
return Simp.Step.visit { expr := e }
else if (← matchPattern pattern e) then
let (rhs, newGoal) ← mkConvGoalFor e
found?.set newGoal
return Simp.Step.done { expr := rhs, proof? := newGoal }