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

perf: dont repeatedly elab term in rw at multiple locations #2317

Browse source
This commit is contained in:
Alex J Best 2023-07-24 17:47:52 +02:00 • committed by GitHub
parent 3b6bc4a87d
commit 808bb9b579
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 15 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

32
src/Lean/Elab/Tactic/Rewrite.lean
View file

@ -11,20 +11,16 @@ import Lean.Elab.Tactic.Config
namespace Lean.Elab.Tactic
open Meta
def rewriteTarget (stx : Syntax) (symm : Bool) (config : Rewrite.Config) : TacticM Unit := do
Term.withSynthesize <| withMainContext do
let e ← elabTerm stx none true
let r ← (← getMainGoal).rewrite (← getMainTarget) e symm (config := config)
let mvarId' ← (← getMainGoal).replaceTargetEq r.eNew r.eqProof
replaceMainGoal (mvarId' :: r.mvarIds)
def rewriteTarget (e : Expr) (symm : Bool) (config : Rewrite.Config) : TacticM Unit := do
let r ← (← getMainGoal).rewrite (← getMainTarget) e symm (config := config)
let mvarId' ← (← getMainGoal).replaceTargetEq r.eNew r.eqProof
replaceMainGoal (mvarId' :: r.mvarIds)
def rewriteLocalDecl (stx : Syntax) (symm : Bool) (fvarId : FVarId) (config : Rewrite.Config) : TacticM Unit := do
Term.withSynthesize <| withMainContext do
let e ← elabTerm stx none true
let localDecl ← fvarId.getDecl
let rwResult ← (← getMainGoal).rewrite localDecl.type e symm (config := config)
let replaceResult ← (← getMainGoal).replaceLocalDecl fvarId rwResult.eNew rwResult.eqProof
replaceMainGoal (replaceResult.mvarId :: rwResult.mvarIds)
def rewriteLocalDecl (e : Expr) (symm : Bool) (fvarId : FVarId) (config : Rewrite.Config) : TacticM Unit := do
let localDecl ← fvarId.getDecl
let rwResult ← (← getMainGoal).rewrite localDecl.type e symm (config := config)
let replaceResult ← (← getMainGoal).replaceLocalDecl fvarId rwResult.eNew rwResult.eqProof
replaceMainGoal (replaceResult.mvarId :: rwResult.mvarIds)
def withRWRulesSeq (token : Syntax) (rwRulesSeqStx : Syntax) (x : (symm : Bool) → (term : Syntax) → TacticM Unit) : TacticM Unit := do
let lbrak := rwRulesSeqStx[0]
@ -62,9 +58,11 @@ declare_config_elab elabRewriteConfig Rewrite.Config
let cfg ← elabRewriteConfig stx[1]
let loc := expandOptLocation stx[3]
withRWRulesSeq stx[0] stx[2] fun symm term => do
withLocation loc
(rewriteLocalDecl term symm · cfg)
(rewriteTarget term symm cfg)
(throwTacticEx `rewrite · "did not find instance of the pattern in the current goal")
Term.withSynthesize <| withMainContext do
let e ← elabTerm term none true
withLocation loc
(rewriteLocalDecl e symm · cfg)
(rewriteTarget e symm cfg)
(throwTacticEx `rewrite · "did not find instance of the pattern in the current goal")
end Lean.Elab.Tactic