3a6ebd88bb
Small tactics used in the implementation of `ext`. --------- Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
66 lines
2.3 KiB
Text
66 lines
2.3 KiB
Text
/-
|
||
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) =>
|
||
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) =>
|
||
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)
|
||
|
||
end Lean.Parser.Tactic
|