-
Notifications
You must be signed in to change notification settings - Fork 345
/
TacticsExtra.lean
90 lines (80 loc) · 3.15 KB
/
TacticsExtra.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
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
/-
Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Mario Carneiro
-/
prelude
import Init.Tactics
import Init.NotationExtra
/-!
Extra tactics and implementation for some tactics defined at `Init/Tactic.lean`
-/
namespace Lean.Parser.Tactic
private def expandIfThenElse
(ifTk thenTk elseTk pos neg : Syntax)
(mkIf : Term → Term → MacroM Term) : MacroM (TSyntax `tactic) := do
let mkCase tk holeOrTacticSeq mkName : MacroM (Term × Array (TSyntax `tactic)) := do
if holeOrTacticSeq.isOfKind `Lean.Parser.Term.syntheticHole then
pure (⟨holeOrTacticSeq⟩, #[])
else if holeOrTacticSeq.isOfKind `Lean.Parser.Term.hole then
pure (← mkName, #[])
else
let hole ← withFreshMacroScope mkName
let holeId := hole.raw[1]
let case ← (open TSyntax.Compat in `(tactic|
case $holeId:ident =>%$tk
-- annotate `then/else` with state after `case`
with_annotate_state $tk skip
$holeOrTacticSeq))
pure (hole, #[case])
let (posHole, posCase) ← mkCase thenTk pos `(?pos)
let (negHole, negCase) ← mkCase elseTk neg `(?neg)
`(tactic| ((open Classical in refine%$ifTk $(← mkIf posHole negHole)); $[$(posCase ++ negCase)]*))
macro_rules
| `(tactic| if%$tk $h : $c then%$ttk $pos else%$etk $neg) =>
-- Limit ref variability for incrementality; see Note [Incremental Macros]
withRef tk do
expandIfThenElse tk ttk etk pos neg fun pos neg => `(if $h : $c then $pos else $neg)
macro_rules
| `(tactic| if%$tk $c then%$ttk $pos else%$etk $neg) =>
-- Limit ref variability for incrementality; see Note [Incremental Macros]
withRef tk do
expandIfThenElse tk ttk etk pos neg fun pos neg => `(if h : $c then $pos else $neg)
/--
`iterate n tac` runs `tac` exactly `n` times.
`iterate tac` runs `tac` repeatedly until failure.
`iterate`'s argument is a tactic sequence,
so multiple tactics can be run using `iterate n (tac₁; tac₂; ⋯)` or
```lean
iterate n
tac₁
tac₂
⋯
```
-/
syntax "iterate" (ppSpace num)? ppSpace tacticSeq : tactic
macro_rules
| `(tactic| iterate $seq:tacticSeq) =>
`(tactic| try ($seq:tacticSeq); iterate $seq:tacticSeq)
| `(tactic| iterate $n $seq:tacticSeq) =>
match n.1.toNat with
| 0 => `(tactic| skip)
| n+1 => `(tactic| ($seq:tacticSeq); iterate $(quote n) $seq:tacticSeq)
/--
Rewrites with the given rules, normalizing casts prior to each step.
-/
syntax "rw_mod_cast" (config)? rwRuleSeq (location)? : tactic
macro_rules
| `(tactic| rw_mod_cast $[$config]? [$rules,*] $[$loc]?) => do
let tacs ← rules.getElems.mapM fun rule =>
`(tactic| (norm_cast at *; rw $[$config]? [$rule] $[$loc]?))
`(tactic| ($[$tacs]*))
/--
Normalize casts in the goal and the given expression, then close the goal with `exact`.
-/
macro "exact_mod_cast " e:term : tactic => `(tactic| exact mod_cast ($e : _))
/--
Normalize casts in the goal and the given expression, then `apply` the expression to the goal.
-/
macro "apply_mod_cast " e:term : tactic => `(tactic| apply mod_cast ($e : _))
end Lean.Parser.Tactic