-
Notifications
You must be signed in to change notification settings - Fork 329
/
Rewrite.lean
59 lines (53 loc) · 2.42 KB
/
Rewrite.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
/-
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Meta.Tactic.Rewrite
import Lean.Meta.Tactic.Replace
import Lean.Elab.Tactic.Basic
import Lean.Elab.Tactic.ElabTerm
import Lean.Elab.Tactic.Location
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 ← rewrite (← getMainGoal) (← getMainTarget) e symm (config := config)
let mvarId' ← replaceTargetEq (← getMainGoal) 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 ← getLocalDecl fvarId
let rwResult ← rewrite (← getMainGoal) localDecl.type e symm (config := config)
let replaceResult ← replaceLocalDecl (← getMainGoal) 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]
let rules := rwRulesSeqStx[1].getArgs
let rbrak := rwRulesSeqStx[2]
-- show initial state up to (incl.) `[`
withTacticInfoContext (mkNullNode #[token, lbrak]) (pure ())
let numRules := (rules.size + 1) / 2
for i in [:numRules] do
let rule := rules[i * 2]
let sep := rules.getD (i * 2 + 1) Syntax.missing
-- show rule state up to (incl.) next `,`
withTacticInfoContext (mkNullNode #[rule, sep]) do
-- show errors on rule
withRef rule do
let symm := !rule[0].isNone
let term := rule[1]
x symm term
declare_config_elab elabRewriteConfig Rewrite.Config
@[builtinTactic Lean.Parser.Tactic.rewriteSeq] def evalRewriteSeq : Tactic := fun stx => do
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")
end Lean.Elab.Tactic