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

perf: reject rewrites that produce same expr

Browse source
This commit is contained in:
Leonardo de Moura 2021-03-03 19:59:27 -08:00
parent e841f16738
commit 152a84c468
1 changed files with 8 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/Lean/Meta/Tactic/Simp/Rewrite.lean
View file

@ -84,14 +84,20 @@ where
if ← hasAssignableMVar proof then
return none
let rhs ← instantiateMVars (← getRHS lemma.kind type)
if e == rhs then
return none
if lemma.perm && !Expr.lt rhs e then
trace[Meta.Tactic.simp.unify]! "{lemma}, perm rejected {e} ==> {rhs}"
trace[Meta.Tactic.simp.rewrite]! "{lemma}, perm rejected {e} ==> {rhs}"
return none
let proof ← finalizeProof lemma.kind proof
trace[Meta.Tactic.simp.rewrite]! "{lemma}, {e} ==> {rhs}"
return some { expr := rhs, proof? := proof }
else
trace[Meta.Tactic.simp.unify]! "{lemma}, failed to unify {lhs} with {e}"
unless lhs.isMVar do
-- We do not report unification failures when `lhs` is a metavariable
-- Example: `x = ()`
-- TODO: reconsider if we want lemmas such as `(x : Unit) → x = ()`
trace[Meta.Tactic.simp.unify]! "{lemma}, failed to unify {lhs} with {e}"
return none
def rewriteCtorEq? (e : Expr) : MetaM (Option Result) := withReducibleAndInstances do