09a5b34931
This PR adjusts the experimental module system to make `private` the default visibility modifier in `module`s, introducing `public` as a new modifier instead. `public section` can be used to revert the default for an entire section, though this is more intended to ease gradual adoption of the new semantics such as in `Init` (and soon `Std`) where they should be replaced by a future decl-by-decl re-review of visibilities.
94 lines
3.2 KiB
Text
94 lines
3.2 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
|
||
-/
|
||
module
|
||
|
||
prelude
|
||
public import Init.Tactics
|
||
public import Init.NotationExtra
|
||
|
||
public section
|
||
|
||
/-!
|
||
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" optConfig rwRuleSeq (location)? : tactic
|
||
macro_rules
|
||
| `(tactic| rw_mod_cast $cfg:optConfig [$rules,*] $[$loc]?) => do
|
||
let tacs ← rules.getElems.mapM fun rule =>
|
||
`(tactic| (norm_cast at *; rw $cfg [$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
|