diff --git a/src/Init/Conv.lean b/src/Init/Conv.lean index 17d2c3a69d..5365b63ea8 100644 --- a/src/Init/Conv.lean +++ b/src/Init/Conv.lean @@ -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) diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean index c7dc097478..41121ab15f 100644 --- a/src/Init/Meta.lean +++ b/src/Init/Meta.lean @@ -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 diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 8bd0260fbe..b04961361a 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -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 /-- diff --git a/src/Init/TacticsExtra.lean b/src/Init/TacticsExtra.lean index 221bf99f3d..425f9a619f 100644 --- a/src/Init/TacticsExtra.lean +++ b/src/Init/TacticsExtra.lean @@ -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]*)) /-- diff --git a/src/Lean/Elab/Tactic/Config.lean b/src/Lean/Elab/Tactic/Config.lean index 6d1d89d2e5..160b8cb092 100644 --- a/src/Lean/Elab/Tactic/Config.lean +++ b/src/Lean/Elab/Tactic/Config.lean @@ -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 diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean index fdfff857dd..4a8b27d7f7 100644 --- a/src/Lean/Elab/Tactic/Simp.lean +++ b/src/Lean/Elab/Tactic/Simp.lean @@ -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 diff --git a/src/Lean/Elab/Tactic/SimpTrace.lean b/src/Lean/Elab/Tactic/SimpTrace.lean index 3342fc35dd..2bc4f649fc 100644 --- a/src/Lean/Elab/Tactic/SimpTrace.lean +++ b/src/Lean/Elab/Tactic/SimpTrace.lean @@ -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) diff --git a/src/Lean/Elab/Tactic/Simpa.lean b/src/Lean/Elab/Tactic/Simpa.lean index b74883da30..a3a70f49fd 100644 --- a/src/Lean/Elab/Tactic/Simpa.lean +++ b/src/Lean/Elab/Tactic/Simpa.lean @@ -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 diff --git a/src/Lean/Elab/Tactic/SolveByElim.lean b/src/Lean/Elab/Tactic/SolveByElim.lean index 18d9468729..d8aeec7678 100644 --- a/src/Lean/Elab/Tactic/SolveByElim.lean +++ b/src/Lean/Elab/Tactic/SolveByElim.lean @@ -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 diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index 0699845ba4..658ab0874e 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -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);