feat: activate new tactic configuration syntax for most tactics (#5898)
PR #5883 added a new syntax for tactic configuration, and this PR enables it in most tactics. Example: `simp +contextual`. There will be followup PRs to modify the remaining ones. Breaking change: Tactics that are macros for `simp` or other core tactics need to adapt. The easiest way is to replace `(config)?` with `optConfig` and then in the syntax quotations replace `$[$cfg]?` by `$cfg:optConfig`. For tactics that manipulate the configuration, see `erw` for an example: ```lean macro "erw" c:optConfig s:rwRuleSeq loc:(location)? : tactic => do `(tactic| rw $[$(getConfigItems c)]* (transparency := .default) $s:rwRuleSeq $(loc)?) ``` Configuration options are processed left-to-right, so this forces the `transparency` to always be `.default`.
This commit is contained in:
Kyle Miller
GitHub
parent
7730ddd1a0
commit
3b80d1eb1f
10 changed files with 108 additions and 86 deletions
|
|
@ -7,6 +7,7 @@ Notation for operators defined at Prelude.lean
|
|||
-/
|
||||
prelude
|
||||
import Init.Tactics
|
||||
import Init.Meta
|
||||
|
||||
namespace Lean.Parser.Tactic.Conv
|
||||
|
||||
|
|
@ -130,11 +131,11 @@ For example, if we are searching for `f _` in `f (f a) = f b`:
|
|||
syntax (name := pattern) "pattern " (occs)? term : conv
|
||||
|
||||
/-- `rw [thm]` rewrites the target using `thm`. See the `rw` tactic for more information. -/
|
||||
syntax (name := rewrite) "rewrite" (config)? rwRuleSeq : conv
|
||||
syntax (name := rewrite) "rewrite" optConfig rwRuleSeq : conv
|
||||
|
||||
/-- `simp [thm]` performs simplification using `thm` and marked `@[simp]` lemmas.
|
||||
See the `simp` tactic for more information. -/
|
||||
syntax (name := simp) "simp" (config)? (discharger)? (&" only")?
|
||||
syntax (name := simp) "simp" optConfig (discharger)? (&" only")?
|
||||
(" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*) "]")? : conv
|
||||
|
||||
/--
|
||||
|
|
@ -151,7 +152,7 @@ example (a : Nat): (0 + 0) = a - a := by
|
|||
rw [← Nat.sub_self a]
|
||||
```
|
||||
-/
|
||||
syntax (name := dsimp) "dsimp" (config)? (discharger)? (&" only")?
|
||||
syntax (name := dsimp) "dsimp" optConfig (discharger)? (&" only")?
|
||||
(" [" withoutPosition((simpErase <|> simpLemma),*) "]")? : conv
|
||||
|
||||
/-- `simp_match` simplifies match expressions. For example,
|
||||
|
|
@ -247,12 +248,12 @@ macro (name := failIfSuccess) tk:"fail_if_success " s:convSeq : conv =>
|
|||
|
||||
/-- `rw [rules]` applies the given list of rewrite rules to the target.
|
||||
See the `rw` tactic for more information. -/
|
||||
macro "rw" c:(config)? s:rwRuleSeq : conv => `(conv| rewrite $[$c]? $s)
|
||||
macro "rw" c:optConfig s:rwRuleSeq : conv => `(conv| rewrite $c:optConfig $s)
|
||||
|
||||
/-- `erw [rules]` is a shorthand for `rw (config := { transparency := .default }) [rules]`.
|
||||
/-- `erw [rules]` is a shorthand for `rw (transparency := .default) [rules]`.
|
||||
This does rewriting up to unfolding of regular definitions (by comparison to regular `rw`
|
||||
which only unfolds `@[reducible]` definitions). -/
|
||||
macro "erw" s:rwRuleSeq : conv => `(conv| rw (config := { transparency := .default }) $s:rwRuleSeq)
|
||||
macro "erw" c:optConfig s:rwRuleSeq : conv => `(conv| rw $[$(getConfigItems c)]* (transparency := .default) $s:rwRuleSeq)
|
||||
|
||||
/-- `args` traverses into all arguments. Synonym for `congr`. -/
|
||||
macro "args" : conv => `(conv| congr)
|
||||
|
|
|
|||
|
|
@ -1412,65 +1412,87 @@ namespace Parser
|
|||
|
||||
namespace Tactic
|
||||
|
||||
/-- `erw [rules]` is a shorthand for `rw (config := { transparency := .default }) [rules]`.
|
||||
/--
|
||||
Extracts the items from a tactic configuration,
|
||||
either a `Lean.Parser.Tactic.optConfig`, `Lean.Parser.Tactic.config`, or these wrapped in null nodes.
|
||||
-/
|
||||
partial def getConfigItems (c : Syntax) : TSyntaxArray ``configItem :=
|
||||
if c.isOfKind nullKind then
|
||||
c.getArgs.flatMap getConfigItems
|
||||
else
|
||||
match c with
|
||||
| `(optConfig| $items:configItem*) => items
|
||||
| `(config| (config := $_)) => #[⟨c⟩] -- handled by mkConfigItemViews
|
||||
| _ => #[]
|
||||
|
||||
def mkOptConfig (items : TSyntaxArray ``configItem) : TSyntax ``optConfig :=
|
||||
⟨Syntax.node1 .none ``optConfig (mkNullNode items)⟩
|
||||
|
||||
/--
|
||||
Appends two tactic configurations.
|
||||
The configurations can be `Lean.Parser.Tactic.optConfig`, `Lean.Parser.Tactic.config`,
|
||||
or these wrapped in null nodes (for example because the syntax is `(config)?`).
|
||||
-/
|
||||
def appendConfig (cfg cfg' : Syntax) : TSyntax ``optConfig :=
|
||||
mkOptConfig <| getConfigItems cfg ++ getConfigItems cfg'
|
||||
|
||||
/-- `erw [rules]` is a shorthand for `rw (transparency := .default) [rules]`.
|
||||
This does rewriting up to unfolding of regular definitions (by comparison to regular `rw`
|
||||
which only unfolds `@[reducible]` definitions). -/
|
||||
macro "erw" s:rwRuleSeq loc:(location)? : tactic =>
|
||||
`(tactic| rw (config := { transparency := .default }) $s $(loc)?)
|
||||
macro "erw" c:optConfig s:rwRuleSeq loc:(location)? : tactic => do
|
||||
`(tactic| rw $[$(getConfigItems c)]* (transparency := .default) $s:rwRuleSeq $(loc)?)
|
||||
|
||||
syntax simpAllKind := atomic(" (" &"all") " := " &"true" ")"
|
||||
syntax dsimpKind := atomic(" (" &"dsimp") " := " &"true" ")"
|
||||
|
||||
macro (name := declareSimpLikeTactic) doc?:(docComment)?
|
||||
"declare_simp_like_tactic" opt:((simpAllKind <|> dsimpKind)?)
|
||||
ppSpace tacName:ident ppSpace tacToken:str ppSpace updateCfg:term : command => do
|
||||
ppSpace tacName:ident ppSpace tacToken:str ppSpace cfg:optConfig : command => do
|
||||
let (kind, tkn, stx) ←
|
||||
if opt.raw.isNone then
|
||||
pure (← `(``simp), ← `("simp"), ← `($[$doc?:docComment]? syntax (name := $tacName) $tacToken:str (config)? (discharger)? (&" only")? (" [" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic))
|
||||
pure (← `(``simp), ← `("simp"), ← `($[$doc?:docComment]? syntax (name := $tacName) $tacToken:str optConfig (discharger)? (&" only")? (" [" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic))
|
||||
else if opt.raw[0].getKind == ``simpAllKind then
|
||||
pure (← `(``simpAll), ← `("simp_all"), ← `($[$doc?:docComment]? syntax (name := $tacName) $tacToken:str (config)? (discharger)? (&" only")? (" [" (simpErase <|> simpLemma),* "]")? : tactic))
|
||||
pure (← `(``simpAll), ← `("simp_all"), ← `($[$doc?:docComment]? syntax (name := $tacName) $tacToken:str optConfig (discharger)? (&" only")? (" [" (simpErase <|> simpLemma),* "]")? : tactic))
|
||||
else
|
||||
pure (← `(``dsimp), ← `("dsimp"), ← `($[$doc?:docComment]? syntax (name := $tacName) $tacToken:str (config)? (discharger)? (&" only")? (" [" (simpErase <|> simpLemma),* "]")? (location)? : tactic))
|
||||
pure (← `(``dsimp), ← `("dsimp"), ← `($[$doc?:docComment]? syntax (name := $tacName) $tacToken:str optConfig (discharger)? (&" only")? (" [" (simpErase <|> simpLemma),* "]")? (location)? : tactic))
|
||||
`($stx:command
|
||||
@[macro $tacName] def expandSimp : Macro := fun s => do
|
||||
let c ← match s[1][0] with
|
||||
| `(config| (config := $$c)) => `(config| (config := $updateCfg $$c))
|
||||
| _ => `(config| (config := $updateCfg {}))
|
||||
let cfg ← `(optConfig| $cfg)
|
||||
let s := s.setKind $kind
|
||||
let s := s.setArg 0 (mkAtomFrom s[0] $tkn (canonical := true))
|
||||
let s := s.setArg 1 (mkNullNode #[c])
|
||||
let s := s.setArg 1 (appendConfig s[1] cfg)
|
||||
let s := s.mkSynthetic
|
||||
return s)
|
||||
|
||||
/-- `simp!` is shorthand for `simp` with `autoUnfold := true`.
|
||||
This will rewrite with all equation lemmas, which can be used to
|
||||
partially evaluate many definitions. -/
|
||||
declare_simp_like_tactic simpAutoUnfold "simp! " fun (c : Lean.Meta.Simp.Config) => { c with autoUnfold := true }
|
||||
declare_simp_like_tactic simpAutoUnfold "simp! " (autoUnfold := true)
|
||||
|
||||
/-- `simp_arith` is shorthand for `simp` with `arith := true` and `decide := true`.
|
||||
This enables the use of normalization by linear arithmetic. -/
|
||||
declare_simp_like_tactic simpArith "simp_arith " fun (c : Lean.Meta.Simp.Config) => { c with arith := true, decide := true }
|
||||
declare_simp_like_tactic simpArith "simp_arith " (arith := true) (decide := true)
|
||||
|
||||
/-- `simp_arith!` is shorthand for `simp_arith` with `autoUnfold := true`.
|
||||
This will rewrite with all equation lemmas, which can be used to
|
||||
partially evaluate many definitions. -/
|
||||
declare_simp_like_tactic simpArithAutoUnfold "simp_arith! " fun (c : Lean.Meta.Simp.Config) => { c with arith := true, autoUnfold := true, decide := true }
|
||||
declare_simp_like_tactic simpArithAutoUnfold "simp_arith! " (arith := true) (autoUnfold := true) (decide := true)
|
||||
|
||||
/-- `simp_all!` is shorthand for `simp_all` with `autoUnfold := true`.
|
||||
This will rewrite with all equation lemmas, which can be used to
|
||||
partially evaluate many definitions. -/
|
||||
declare_simp_like_tactic (all := true) simpAllAutoUnfold "simp_all! " fun (c : Lean.Meta.Simp.ConfigCtx) => { c with autoUnfold := true }
|
||||
declare_simp_like_tactic (all := true) simpAllAutoUnfold "simp_all! " (autoUnfold := true)
|
||||
|
||||
/-- `simp_all_arith` combines the effects of `simp_all` and `simp_arith`. -/
|
||||
declare_simp_like_tactic (all := true) simpAllArith "simp_all_arith " fun (c : Lean.Meta.Simp.ConfigCtx) => { c with arith := true, decide := true }
|
||||
declare_simp_like_tactic (all := true) simpAllArith "simp_all_arith " (arith := true) (decide := true)
|
||||
|
||||
/-- `simp_all_arith!` combines the effects of `simp_all`, `simp_arith` and `simp!`. -/
|
||||
declare_simp_like_tactic (all := true) simpAllArithAutoUnfold "simp_all_arith! " fun (c : Lean.Meta.Simp.ConfigCtx) => { c with arith := true, autoUnfold := true, decide := true }
|
||||
declare_simp_like_tactic (all := true) simpAllArithAutoUnfold "simp_all_arith! " (arith := true) (autoUnfold := true) (decide := true)
|
||||
|
||||
/-- `dsimp!` is shorthand for `dsimp` with `autoUnfold := true`.
|
||||
This will rewrite with all equation lemmas, which can be used to
|
||||
partially evaluate many definitions. -/
|
||||
declare_simp_like_tactic (dsimp := true) dsimpAutoUnfold "dsimp! " fun (c : Lean.Meta.DSimp.Config) => { c with autoUnfold := true }
|
||||
declare_simp_like_tactic (dsimp := true) dsimpAutoUnfold "dsimp! " (autoUnfold := true)
|
||||
|
||||
end Tactic
|
||||
|
||||
|
|
|
|||
|
|
@ -430,12 +430,12 @@ syntax negConfigItem := "-" noWs ident
|
|||
|
||||
As a special case, `(config := ...)` sets the entire configuration.
|
||||
-/
|
||||
syntax valConfigItem := atomic("(" (ident <|> &"config")) " := " withoutPosition(term) ")"
|
||||
syntax valConfigItem := atomic(" (" notFollowedBy(&"discharger" <|> &"disch") (ident <|> &"config")) " := " withoutPosition(term) ")"
|
||||
/-- A configuration item for a tactic configuration. -/
|
||||
syntax configItem := posConfigItem <|> negConfigItem <|> valConfigItem
|
||||
|
||||
/-- Configuration options for tactics. -/
|
||||
syntax optConfig := configItem*
|
||||
syntax optConfig := (colGt configItem)*
|
||||
|
||||
/-- Optional configuration option for tactics. (Deprecated. Replace `(config)?` with `optConfig`.) -/
|
||||
syntax config := atomic(" (" &"config") " := " withoutPosition(term) ")"
|
||||
|
|
@ -503,16 +503,16 @@ restricting which later rewrites can be found.
|
|||
(Disallowed occurrences do not result in instantiation.)
|
||||
`{occs := .neg L}` allows skipping specified occurrences.
|
||||
-/
|
||||
syntax (name := rewriteSeq) "rewrite" (config)? rwRuleSeq (location)? : tactic
|
||||
syntax (name := rewriteSeq) "rewrite" optConfig rwRuleSeq (location)? : tactic
|
||||
|
||||
/--
|
||||
`rw` is like `rewrite`, but also tries to close the goal by "cheap" (reducible) `rfl` afterwards.
|
||||
-/
|
||||
macro (name := rwSeq) "rw " c:(config)? s:rwRuleSeq l:(location)? : tactic =>
|
||||
macro (name := rwSeq) "rw " c:optConfig s:rwRuleSeq l:(location)? : tactic =>
|
||||
match s with
|
||||
| `(rwRuleSeq| [$rs,*]%$rbrak) =>
|
||||
-- We show the `rfl` state on `]`
|
||||
`(tactic| (rewrite $(c)? [$rs,*] $(l)?; with_annotate_state $rbrak (try (with_reducible rfl))))
|
||||
`(tactic| (rewrite $c [$rs,*] $(l)?; with_annotate_state $rbrak (try (with_reducible rfl))))
|
||||
| _ => Macro.throwUnsupported
|
||||
|
||||
/-- `rwa` is short-hand for `rw; assumption`. -/
|
||||
|
|
@ -581,14 +581,14 @@ non-dependent hypotheses. It has many variants:
|
|||
- `simp [*] at *` simplifies target and all (propositional) hypotheses using the
|
||||
other hypotheses.
|
||||
-/
|
||||
syntax (name := simp) "simp" (config)? (discharger)? (&" only")?
|
||||
syntax (name := simp) "simp" optConfig (discharger)? (&" only")?
|
||||
(" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "]")? (location)? : tactic
|
||||
/--
|
||||
`simp_all` is a stronger version of `simp [*] at *` where the hypotheses and target
|
||||
are simplified multiple times until no simplification is applicable.
|
||||
Only non-dependent propositional hypotheses are considered.
|
||||
-/
|
||||
syntax (name := simpAll) "simp_all" (config)? (discharger)? (&" only")?
|
||||
syntax (name := simpAll) "simp_all" optConfig (discharger)? (&" only")?
|
||||
(" [" withoutPosition((simpErase <|> simpLemma),*,?) "]")? : tactic
|
||||
|
||||
/--
|
||||
|
|
@ -596,7 +596,7 @@ The `dsimp` tactic is the definitional simplifier. It is similar to `simp` but o
|
|||
applies theorems that hold by reflexivity. Thus, the result is guaranteed to be
|
||||
definitionally equal to the input.
|
||||
-/
|
||||
syntax (name := dsimp) "dsimp" (config)? (discharger)? (&" only")?
|
||||
syntax (name := dsimp) "dsimp" optConfig (discharger)? (&" only")?
|
||||
(" [" withoutPosition((simpErase <|> simpLemma),*,?) "]")? (location)? : tactic
|
||||
|
||||
/--
|
||||
|
|
@ -618,7 +618,7 @@ def dsimpArg := simpErase.binary `orelse simpLemma
|
|||
syntax dsimpArgs := " [" dsimpArg,* "]"
|
||||
|
||||
/-- The common arguments of `simp?` and `simp?!`. -/
|
||||
syntax simpTraceArgsRest := (config)? (discharger)? (&" only")? (simpArgs)? (ppSpace location)?
|
||||
syntax simpTraceArgsRest := optConfig (discharger)? (&" only")? (simpArgs)? (ppSpace location)?
|
||||
|
||||
/--
|
||||
`simp?` takes the same arguments as `simp`, but reports an equivalent call to `simp only`
|
||||
|
|
@ -637,7 +637,7 @@ syntax (name := simpTrace) "simp?" "!"? simpTraceArgsRest : tactic
|
|||
macro tk:"simp?!" rest:simpTraceArgsRest : tactic => `(tactic| simp?%$tk ! $rest)
|
||||
|
||||
/-- The common arguments of `simp_all?` and `simp_all?!`. -/
|
||||
syntax simpAllTraceArgsRest := (config)? (discharger)? (&" only")? (dsimpArgs)?
|
||||
syntax simpAllTraceArgsRest := optConfig (discharger)? (&" only")? (dsimpArgs)?
|
||||
|
||||
@[inherit_doc simpTrace]
|
||||
syntax (name := simpAllTrace) "simp_all?" "!"? simpAllTraceArgsRest : tactic
|
||||
|
|
@ -646,7 +646,7 @@ syntax (name := simpAllTrace) "simp_all?" "!"? simpAllTraceArgsRest : tactic
|
|||
macro tk:"simp_all?!" rest:simpAllTraceArgsRest : tactic => `(tactic| simp_all?%$tk ! $rest)
|
||||
|
||||
/-- The common arguments of `dsimp?` and `dsimp?!`. -/
|
||||
syntax dsimpTraceArgsRest := (config)? (&" only")? (dsimpArgs)? (ppSpace location)?
|
||||
syntax dsimpTraceArgsRest := optConfig (&" only")? (dsimpArgs)? (ppSpace location)?
|
||||
|
||||
@[inherit_doc simpTrace]
|
||||
syntax (name := dsimpTrace) "dsimp?" "!"? dsimpTraceArgsRest : tactic
|
||||
|
|
@ -655,7 +655,7 @@ syntax (name := dsimpTrace) "dsimp?" "!"? dsimpTraceArgsRest : tactic
|
|||
macro tk:"dsimp?!" rest:dsimpTraceArgsRest : tactic => `(tactic| dsimp?%$tk ! $rest)
|
||||
|
||||
/-- The arguments to the `simpa` family tactics. -/
|
||||
syntax simpaArgsRest := (config)? (discharger)? &" only "? (simpArgs)? (" using " term)?
|
||||
syntax simpaArgsRest := optConfig (discharger)? &" only "? (simpArgs)? (" using " term)?
|
||||
|
||||
/--
|
||||
This is a "finishing" tactic modification of `simp`. It has two forms.
|
||||
|
|
@ -1292,7 +1292,7 @@ example (a b : Nat)
|
|||
|
||||
See also `norm_cast`.
|
||||
-/
|
||||
syntax (name := pushCast) "push_cast" (config)? (discharger)? (&" only")?
|
||||
syntax (name := pushCast) "push_cast" optConfig (discharger)? (&" only")?
|
||||
(" [" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic
|
||||
|
||||
/--
|
||||
|
|
@ -1391,7 +1391,7 @@ You can pass a further configuration via the syntax `apply_rules (config := {...
|
|||
The options supported are the same as for `solve_by_elim` (and include all the options for `apply`).
|
||||
-/
|
||||
syntax (name := applyAssumption)
|
||||
"apply_assumption" (config)? (&" only")? (args)? (using_)? : tactic
|
||||
"apply_assumption" optConfig (&" only")? (args)? (using_)? : tactic
|
||||
|
||||
/--
|
||||
`apply_rules [l₁, l₂, ...]` tries to solve the main goal by iteratively
|
||||
|
|
@ -1416,7 +1416,7 @@ You can bound the iteration depth using the syntax `apply_rules (config := {maxD
|
|||
Unlike `solve_by_elim`, `apply_rules` does not perform backtracking, and greedily applies
|
||||
a lemma from the list until it gets stuck.
|
||||
-/
|
||||
syntax (name := applyRules) "apply_rules" (config)? (&" only")? (args)? (using_)? : tactic
|
||||
syntax (name := applyRules) "apply_rules" optConfig (&" only")? (args)? (using_)? : tactic
|
||||
end SolveByElim
|
||||
|
||||
/--
|
||||
|
|
|
|||
|
|
@ -70,11 +70,11 @@ macro_rules
|
|||
/--
|
||||
Rewrites with the given rules, normalizing casts prior to each step.
|
||||
-/
|
||||
syntax "rw_mod_cast" (config)? rwRuleSeq (location)? : tactic
|
||||
syntax "rw_mod_cast" optConfig rwRuleSeq (location)? : tactic
|
||||
macro_rules
|
||||
| `(tactic| rw_mod_cast $[$config]? [$rules,*] $[$loc]?) => do
|
||||
| `(tactic| rw_mod_cast $cfg:optConfig [$rules,*] $[$loc]?) => do
|
||||
let tacs ← rules.getElems.mapM fun rule =>
|
||||
`(tactic| (norm_cast at *; rw $[$config]? [$rule] $[$loc]?))
|
||||
`(tactic| (norm_cast at *; rw $cfg [$rule] $[$loc]?))
|
||||
`(tactic| ($[$tacs]*))
|
||||
|
||||
/--
|
||||
|
|
|
|||
|
|
@ -12,27 +12,6 @@ import Lean.Linter.MissingDocs
|
|||
namespace Lean.Elab.Tactic
|
||||
open Meta Parser.Tactic Command
|
||||
|
||||
/--
|
||||
Extracts the items from a tactic configuration,
|
||||
either a `Lean.Parser.Tactic.optConfig`, `Lean.Parser.Tactic.config`, or these wrapped in null nodes.
|
||||
-/
|
||||
private partial def getConfigItems (c : Syntax) : TSyntaxArray ``configItem :=
|
||||
if c.isOfKind nullKind then
|
||||
c.getArgs.flatMap getConfigItems
|
||||
else
|
||||
match c with
|
||||
| `(optConfig| $items:configItem*) => items
|
||||
| `(config| (config := $val)) => #[Unhygienic.run <| withRef c `(configItem| (config := $val))]
|
||||
| _ => #[]
|
||||
|
||||
/--
|
||||
Appends two tactic configurations.
|
||||
The configurations can be `Lean.Parser.Tactic.optConfig`, `Lean.Parser.Tactic.config`,
|
||||
or these wrapped in null nodes (for example because the syntax is `(config)?`).
|
||||
-/
|
||||
def appendConfig (cfg cfg' : Syntax) : TSyntax ``optConfig :=
|
||||
Unhygienic.run `(optConfig| $(getConfigItems cfg)* $(getConfigItems cfg')*)
|
||||
|
||||
private structure ConfigItemView where
|
||||
ref : Syntax
|
||||
option : Ident
|
||||
|
|
@ -47,6 +26,7 @@ private def mkConfigItemViews (c : TSyntaxArray ``configItem) : Array ConfigItem
|
|||
| `(configItem| ($option:ident := $value)) => { ref := item, option, value }
|
||||
| `(configItem| +$option) => { ref := item, option, bool := true, value := mkCIdentFrom item ``true }
|
||||
| `(configItem| -$option) => { ref := item, option, bool := true, value := mkCIdentFrom item ``false }
|
||||
| `(config| (config%$tk := $value)) => { ref := item, option := mkCIdentFrom tk `config, value := value }
|
||||
| _ => { ref := item, option := ⟨Syntax.missing⟩, value := ⟨Syntax.missing⟩ }
|
||||
|
||||
/--
|
||||
|
|
@ -83,14 +63,27 @@ private partial def expandField (structName : Name) (field : Name) : MetaM (Name
|
|||
/-- Elaborates a tactic configuration. -/
|
||||
private def elabConfig (recover : Bool) (structName : Name) (items : Array ConfigItemView) : TermElabM Expr :=
|
||||
withoutModifyingStateWithInfoAndMessages <| withLCtx {} {} <| withSaveInfoContext do
|
||||
let mut base? : Option Term := none
|
||||
let mkStructInst (source? : Option Term) (fields : TSyntaxArray ``Parser.Term.structInstField) : TermElabM Term :=
|
||||
match source? with
|
||||
| some source => `({$source with $fields* : $(mkCIdent structName)})
|
||||
| none => `({$fields* : $(mkCIdent structName)})
|
||||
let mut source? : Option Term := none
|
||||
let mut seenFields : NameSet := {}
|
||||
let mut fields : TSyntaxArray ``Parser.Term.structInstField := #[]
|
||||
for item in items do
|
||||
try
|
||||
let option := item.option.getId.eraseMacroScopes
|
||||
if option == `config then
|
||||
base? ← withRef item.value `(($item.value : $(mkCIdent structName)))
|
||||
fields := #[]
|
||||
unless fields.isEmpty do
|
||||
-- Flush fields. Even though these values will not be used, we still want to elaborate them.
|
||||
source? ← mkStructInst source? fields
|
||||
seenFields := {}
|
||||
fields := #[]
|
||||
let valSrc ← withRef item.value `(($item.value : $(mkCIdent structName)))
|
||||
if let some source := source? then
|
||||
source? ← withRef item.value `({$valSrc, $source with : $(mkCIdent structName)})
|
||||
else
|
||||
source? := valSrc
|
||||
else
|
||||
addCompletionInfo <| CompletionInfo.fieldId item.option option {} structName
|
||||
let (path, projFn) ← withRef item.option <| expandField structName option
|
||||
|
|
@ -104,14 +97,20 @@ private def elabConfig (recover : Bool) (structName : Name) (items : Array Confi
|
|||
-- Special case: `(opt := by tacs)` uses the `tacs` syntax itself
|
||||
withRef item.value <| `(Unhygienic.run `(tacticSeq| $seq))
|
||||
| value => pure value
|
||||
if seenFields.contains path then
|
||||
-- Flush fields. There is a duplicate, but we still want to elaborate both.
|
||||
source? ← mkStructInst source? fields
|
||||
seenFields := {}
|
||||
fields := #[]
|
||||
fields := fields.push <| ← `(Parser.Term.structInstField|
|
||||
$(mkCIdentFrom item.option path (canonical := true)):ident := $value)
|
||||
seenFields := seenFields.insert path
|
||||
catch ex =>
|
||||
if recover then
|
||||
logException ex
|
||||
else
|
||||
throw ex
|
||||
let stx : Term ← `({$[$base? with]? $fields*})
|
||||
let stx : Term ← mkStructInst source? fields
|
||||
let e ← Term.withSynthesize <| Term.elabTermEnsuringType stx (mkConst structName)
|
||||
instantiateMVars e
|
||||
|
||||
|
|
|
|||
|
|
@ -437,7 +437,7 @@ def withSimpDiagnostics (x : TacticM Simp.Diagnostics) : TacticM Unit := do
|
|||
Simp.reportDiag stats
|
||||
|
||||
/-
|
||||
"simp" (config)? (discharger)? (" only")? (" [" ((simpStar <|> simpErase <|> simpLemma),*,?) "]")?
|
||||
"simp" optConfig (discharger)? (" only")? (" [" ((simpStar <|> simpErase <|> simpLemma),*,?) "]")?
|
||||
(location)?
|
||||
-/
|
||||
@[builtin_tactic Lean.Parser.Tactic.simp] def evalSimp : Tactic := fun stx => withMainContext do withSimpDiagnostics do
|
||||
|
|
|
|||
|
|
@ -25,11 +25,11 @@ def mkSimpCallStx (stx : Syntax) (usedSimps : UsedSimps) : MetaM (TSyntax `tacti
|
|||
@[builtin_tactic simpTrace] def evalSimpTrace : Tactic := fun stx =>
|
||||
match stx with
|
||||
| `(tactic|
|
||||
simp?%$tk $[!%$bang]? $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?) => withMainContext do withSimpDiagnostics do
|
||||
simp?%$tk $[!%$bang]? $cfg:optConfig $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?) => withMainContext do withSimpDiagnostics do
|
||||
let stx ← if bang.isSome then
|
||||
`(tactic| simp!%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?)
|
||||
`(tactic| simp!%$tk $cfg:optConfig $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?)
|
||||
else
|
||||
`(tactic| simp%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?)
|
||||
`(tactic| simp%$tk $cfg:optConfig $[$discharger]? $[only%$o]? $[[$args,*]]? $(loc)?)
|
||||
let { ctx, simprocs, dischargeWrapper } ← mkSimpContext stx (eraseLocal := false)
|
||||
let stats ← dischargeWrapper.with fun discharge? =>
|
||||
simpLocation ctx (simprocs := simprocs) discharge? <|
|
||||
|
|
@ -41,11 +41,11 @@ def mkSimpCallStx (stx : Syntax) (usedSimps : UsedSimps) : MetaM (TSyntax `tacti
|
|||
|
||||
@[builtin_tactic simpAllTrace] def evalSimpAllTrace : Tactic := fun stx =>
|
||||
match stx with
|
||||
| `(tactic| simp_all?%$tk $[!%$bang]? $(config)? $(discharger)? $[only%$o]? $[[$args,*]]?) => withSimpDiagnostics do
|
||||
| `(tactic| simp_all?%$tk $[!%$bang]? $cfg:optConfig $(discharger)? $[only%$o]? $[[$args,*]]?) => withSimpDiagnostics do
|
||||
let stx ← if bang.isSome then
|
||||
`(tactic| simp_all!%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]?)
|
||||
`(tactic| simp_all!%$tk $cfg:optConfig $(discharger)? $[only%$o]? $[[$args,*]]?)
|
||||
else
|
||||
`(tactic| simp_all%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]?)
|
||||
`(tactic| simp_all%$tk $cfg:optConfig $(discharger)? $[only%$o]? $[[$args,*]]?)
|
||||
let { ctx, .. } ← mkSimpContext stx (eraseLocal := true)
|
||||
(kind := .simpAll) (ignoreStarArg := true)
|
||||
let (result?, stats) ← simpAll (← getMainGoal) ctx
|
||||
|
|
@ -81,11 +81,11 @@ where
|
|||
|
||||
@[builtin_tactic dsimpTrace] def evalDSimpTrace : Tactic := fun stx =>
|
||||
match stx with
|
||||
| `(tactic| dsimp?%$tk $[!%$bang]? $(config)? $[only%$o]? $[[$args,*]]? $(loc)?) => withSimpDiagnostics do
|
||||
| `(tactic| dsimp?%$tk $[!%$bang]? $cfg:optConfig $[only%$o]? $[[$args,*]]? $(loc)?) => withSimpDiagnostics do
|
||||
let stx ← if bang.isSome then
|
||||
`(tactic| dsimp!%$tk $(config)? $[only%$o]? $[[$args,*]]? $(loc)?)
|
||||
`(tactic| dsimp!%$tk $cfg:optConfig $[only%$o]? $[[$args,*]]? $(loc)?)
|
||||
else
|
||||
`(tactic| dsimp%$tk $(config)? $[only%$o]? $[[$args,*]]? $(loc)?)
|
||||
`(tactic| dsimp%$tk $cfg:optConfig $[only%$o]? $[[$args,*]]? $(loc)?)
|
||||
let { ctx, simprocs, .. } ←
|
||||
withMainContext <| mkSimpContext stx (eraseLocal := false) (kind := .dsimp)
|
||||
let stats ← dsimpLocation' ctx simprocs <| (loc.map expandLocation).getD (.targets #[] true)
|
||||
|
|
|
|||
|
|
@ -31,9 +31,9 @@ deriving instance Repr for UseImplicitLambdaResult
|
|||
|
||||
@[builtin_tactic Lean.Parser.Tactic.simpa] def evalSimpa : Tactic := fun stx => do
|
||||
match stx with
|
||||
| `(tactic| simpa%$tk $[?%$squeeze]? $[!%$unfold]? $(cfg)? $(disch)? $[only%$only]?
|
||||
| `(tactic| simpa%$tk $[?%$squeeze]? $[!%$unfold]? $cfg:optConfig $(disch)? $[only%$only]?
|
||||
$[[$args,*]]? $[using $usingArg]?) => Elab.Tactic.focus do withSimpDiagnostics do
|
||||
let stx ← `(tactic| simp $(cfg)? $(disch)? $[only%$only]? $[[$args,*]]?)
|
||||
let stx ← `(tactic| simp $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]?)
|
||||
let { ctx, simprocs, dischargeWrapper } ←
|
||||
withMainContext <| mkSimpContext stx (eraseLocal := false)
|
||||
let ctx := if unfold.isSome then { ctx with config.autoUnfold := true } else ctx
|
||||
|
|
@ -96,11 +96,11 @@ deriving instance Repr for UseImplicitLambdaResult
|
|||
g.assumption; pure stats
|
||||
if tactic.simp.trace.get (← getOptions) || squeeze.isSome then
|
||||
let stx ← match ← mkSimpOnly stx stats.usedTheorems with
|
||||
| `(tactic| simp $(cfg)? $(disch)? $[only%$only]? $[[$args,*]]?) =>
|
||||
| `(tactic| simp $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]?) =>
|
||||
if unfold.isSome then
|
||||
`(tactic| simpa! $(cfg)? $(disch)? $[only%$only]? $[[$args,*]]? $[using $usingArg]?)
|
||||
`(tactic| simpa! $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]? $[using $usingArg]?)
|
||||
else
|
||||
`(tactic| simpa $(cfg)? $(disch)? $[only%$only]? $[[$args,*]]? $[using $usingArg]?)
|
||||
`(tactic| simpa $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]? $[using $usingArg]?)
|
||||
| _ => unreachable!
|
||||
TryThis.addSuggestion tk stx (origSpan? := ← getRef)
|
||||
return stats.diag
|
||||
|
|
|
|||
|
|
@ -68,7 +68,7 @@ def processSyntax (cfg : SolveByElimConfig := {}) (only star : Bool) (add remove
|
|||
@[builtin_tactic Lean.Parser.Tactic.applyAssumption]
|
||||
def evalApplyAssumption : Tactic := fun stx =>
|
||||
match stx with
|
||||
| `(tactic| apply_assumption $[$cfg]? $[only%$o]? $[$t:args]? $[$use:using_]?) => do
|
||||
| `(tactic| apply_assumption $cfg:optConfig $[only%$o]? $[$t:args]? $[$use:using_]?) => do
|
||||
let (star, add, remove) := parseArgs t
|
||||
let use := parseUsing use
|
||||
let cfg ← elabConfig (mkOptionalNode cfg)
|
||||
|
|
@ -86,7 +86,7 @@ See `Lean.MVarId.applyRules` for a `MetaM` level analogue of this tactic.
|
|||
@[builtin_tactic Lean.Parser.Tactic.applyRules]
|
||||
def evalApplyRules : Tactic := fun stx =>
|
||||
match stx with
|
||||
| `(tactic| apply_rules $[$cfg]? $[only%$o]? $[$t:args]? $[$use:using_]?) => do
|
||||
| `(tactic| apply_rules $cfg:optConfig $[only%$o]? $[$t:args]? $[$use:using_]?) => do
|
||||
let (star, add, remove) := parseArgs t
|
||||
let use := parseUsing use
|
||||
let cfg ← elabApplyRulesConfig (mkOptionalNode cfg)
|
||||
|
|
@ -97,7 +97,7 @@ def evalApplyRules : Tactic := fun stx =>
|
|||
@[builtin_tactic Lean.Parser.Tactic.solveByElim]
|
||||
def evalSolveByElim : Tactic := fun stx =>
|
||||
match stx with
|
||||
| `(tactic| solve_by_elim $[*%$s]? $[$cfg]? $[only%$o]? $[$t:args]? $[$use:using_]?) => do
|
||||
| `(tactic| solve_by_elim $[*%$s]? $(cfg)? $[only%$o]? $[$t:args]? $[$use:using_]?) => do
|
||||
let (star, add, remove) := parseArgs t
|
||||
let use := parseUsing use
|
||||
let goals ← if s.isSome then
|
||||
|
|
|
|||
|
|
@ -8,7 +8,7 @@ options get_default_options() {
|
|||
// switch to `true` for ABI-breaking changes affecting meta code
|
||||
opts = opts.update({"interpreter", "prefer_native"}, false);
|
||||
// switch to `true` for changing built-in parsers used in quotations
|
||||
opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false);
|
||||
opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true);
|
||||
// toggling `parseQuotWithCurrentStage` may also require toggling the following option if macros/syntax
|
||||
// with custom precheck hooks were affected
|
||||
opts = opts.update({"quotPrecheck"}, true);
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue