-
Notifications
You must be signed in to change notification settings - Fork 350
/
Location.lean
72 lines (65 loc) · 2.66 KB
/
Location.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
60
61
62
63
64
65
66
67
68
69
70
71
72
/-
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Lean.Elab.Tactic.Basic
import Lean.Elab.Tactic.ElabTerm
namespace Lean.Elab.Tactic
/-- Denotes a set of locations where a tactic should be applied for the main goal. See also `withLocation`. -/
inductive Location where
/-- Apply the tactic everywhere. -/
| wildcard
/-- `hypotheses` are hypothesis names in the main goal that the tactic should be applied to.
If `type` is true, then the tactic should also be applied to the target type. -/
| targets (hypotheses : Array Syntax) (type : Bool)
/-
Recall that
```
syntax locationWildcard := "*"
syntax locationHyp := (colGt term:max)+ ("⊢" <|> "|-")?
syntax location := withPosition("at " locationWildcard <|> locationHyp)
```
-/
def expandLocation (stx : Syntax) : Location :=
let arg := stx[1]
if arg.getKind == ``Parser.Tactic.locationWildcard then
Location.wildcard
else
Location.targets arg[0].getArgs (!arg[1].isNone)
def expandOptLocation (stx : Syntax) : Location :=
if stx.isNone then
Location.targets #[] true
else
expandLocation stx[0]
open Meta
/--
Runs the given `atLocal` and `atTarget` methods on each of the locations selected by the given `loc`.
* If `loc` is a list of locations, runs at each specified hypothesis (and finally the goal if `⊢` is included),
and fails if any of the tactic applications fail.
* If `loc` is `*`, runs at the target first and then the hypotheses in reverse order.
If `atTarget` closes the main goal, `withLocation` does not run `atLocal`.
If all tactic applications fail, `withLocation` with call `failed` with the main goal mvar.
-/
def withLocation (loc : Location) (atLocal : FVarId → TacticM Unit) (atTarget : TacticM Unit) (failed : MVarId → TacticM Unit) : TacticM Unit := do
match loc with
| Location.targets hyps type =>
hyps.forM fun hyp => withMainContext do
let fvarId ← getFVarId hyp
atLocal fvarId
if type then
withMainContext atTarget
| Location.wildcard =>
let worked ← tryTactic <| withMainContext <| atTarget
let g ← try getMainGoal catch _ => return () -- atTarget closed the goal
g.withContext do
let mut worked := worked
-- We must traverse backwards because the given `atLocal` may use the revert/intro idiom
for fvarId in (← getLCtx).getFVarIds.reverse do
if (← fvarId.getDecl).isImplementationDetail then
continue
worked := worked || (← tryTactic <| withMainContext <| atLocal fvarId)
unless worked do
failed (← getMainGoal)
end Lean.Elab.Tactic