|
| 1 | +/- |
| 2 | +Copyright (c) 2022 Mario Carneiro. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Mario Carneiro |
| 5 | +-/ |
| 6 | +import Lean |
| 7 | +import Mathlib.Tactic.Core |
| 8 | + |
| 9 | +/-! |
| 10 | +# `simp?` and `squeeze_scope` tactics |
| 11 | +
|
| 12 | +The `simp?` tactic is a simple wrapper around the simp with trace behavior implemented in core. |
| 13 | +
|
| 14 | +The `squeeze_scope` tactic allows aggregating multiple calls to `simp` coming from the same syntax |
| 15 | +but in different branches of execution, such as in `cases x <;> simp`. |
| 16 | +The reported `simp` call covers all simp lemmas used by this syntax. |
| 17 | +-/ |
| 18 | +namespace Mathlib.Tactic |
| 19 | +open Lean Elab Parser Tactic |
| 20 | + |
| 21 | +/-- The common arguments of `simp?` and `simp?!`. -/ |
| 22 | +syntax simpTraceArgsRest := (config)? (discharger)? (&" only")? (simpArgs)? (ppSpace location)? |
| 23 | + |
| 24 | +/-- |
| 25 | +`simp?` takes the same arguments as `simp`, but reports an equivalent call to `simp only` |
| 26 | +that would be sufficient to close the goal. This is useful for reducing the size of the simp |
| 27 | +set in a local invocation to speed up processing. |
| 28 | +``` |
| 29 | +example (x : Nat) : (if True then x + 2 else 3) = x + 2 := by |
| 30 | + simp? -- prints "Try this: simp only [ite_true]" |
| 31 | +``` |
| 32 | +
|
| 33 | +This command can also be used in `simp_all` and `dsimp`. |
| 34 | +-/ |
| 35 | +syntax (name := simpTrace) "simp?" "!"? simpTraceArgsRest : tactic |
| 36 | + |
| 37 | +@[inheritDoc simpTrace] |
| 38 | +macro tk:"simp?!" rest:simpTraceArgsRest : tactic => `(tactic| simp?%$tk ! $rest) |
| 39 | + |
| 40 | +macro_rules |
| 41 | + | `(tactic| simp?%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?) => |
| 42 | + `(tactic| set_option tactic.simp.trace true in |
| 43 | + simp%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?) |
| 44 | + | `(tactic| simp?%$tk ! $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?) => |
| 45 | + `(tactic| set_option tactic.simp.trace true in |
| 46 | + simp!%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?) |
| 47 | + |
| 48 | +/-- The common arguments of `simp_all?` and `simp_all?!`. -/ |
| 49 | +syntax simpAllTraceArgsRest := (config)? (discharger)? (&" only")? (dsimpArgs)? |
| 50 | + |
| 51 | +@[inheritDoc simpTrace] |
| 52 | +syntax (name := simpAllTrace) "simp_all?" "!"? simpAllTraceArgsRest : tactic |
| 53 | + |
| 54 | +@[inheritDoc simpTrace] |
| 55 | +macro tk:"simp_all?!" rest:simpAllTraceArgsRest : tactic => `(tactic| simp_all?%$tk ! $rest) |
| 56 | + |
| 57 | +macro_rules |
| 58 | + | `(tactic| simp_all?%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]?) => |
| 59 | + `(tactic| set_option tactic.simp.trace true in |
| 60 | + simp_all%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]?) |
| 61 | + | `(tactic| simp_all?%$tk ! $(config)? $(discharger)? $[only%$o]? $[[$args,*]]?) => |
| 62 | + `(tactic| set_option tactic.simp.trace true in |
| 63 | + simp_all!%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]?) |
| 64 | + |
| 65 | +/-- The common arguments of `dsimp?` and `dsimp?!`. -/ |
| 66 | +syntax dsimpTraceArgsRest := (config)? (&" only")? (dsimpArgs)? (ppSpace location)? |
| 67 | + |
| 68 | +@[inheritDoc simpTrace] |
| 69 | +syntax (name := dsimpTrace) "dsimp?" "!"? dsimpTraceArgsRest : tactic |
| 70 | + |
| 71 | +@[inheritDoc simpTrace] |
| 72 | +macro tk:"dsimp?!" rest:dsimpTraceArgsRest : tactic => `(tactic| dsimp?%$tk ! $rest) |
| 73 | + |
| 74 | +macro_rules |
| 75 | + | `(tactic| dsimp?%$tk $(config)? $[only%$o]? $[[$args,*]]? $(loc)?) => |
| 76 | + `(tactic| set_option tactic.simp.trace true in |
| 77 | + dsimp%$tk $(config)? $[only%$o]? $[[$args,*]]? $(loc)?) |
| 78 | + | `(tactic| dsimp?%$tk ! $(config)? $[only%$o]? $[[$args,*]]? $(loc)?) => |
| 79 | + `(tactic| set_option tactic.simp.trace true in |
| 80 | + dsimp!%$tk $(config)? $[only%$o]? $[[$args,*]]? $(loc)?) |
| 81 | + |
| 82 | +/-- |
| 83 | +`squeeze_scope a => tacs` is part of the implementation of `squeeze_scope`. |
| 84 | +Inside `tacs`, invocations of `simp` wrapped with `squeeze_wrap a _ => ...` will contribute |
| 85 | +to the accounting associated to scope `a`. |
| 86 | +-/ |
| 87 | +local syntax (name := squeezeScopeIn) "squeeze_scope " ident " => " tacticSeq : tactic |
| 88 | +/-- |
| 89 | +`squeeze_wrap a x => tac` is part of the implementation of `squeeze_scope`. |
| 90 | +Here `tac` will be a `simp` or `dsimp` syntax, and `squeeze_wrap` will run the tactic |
| 91 | +and contribute the generated `usedSimps` to the `squeezeScopes[a][x]` variable. |
| 92 | +-/ |
| 93 | +local syntax (name := squeezeWrap) "squeeze_wrap " ident ident " => " tactic : tactic |
| 94 | + |
| 95 | +open TSyntax.Compat in |
| 96 | +/-- |
| 97 | +The `squeeze_scope` tactic allows aggregating multiple calls to `simp` coming from the same syntax |
| 98 | +but in different branches of execution, such as in `cases x <;> simp`. |
| 99 | +The reported `simp` call covers all simp lemmas used by this syntax. |
| 100 | +``` |
| 101 | +@[simp] def bar (z : Nat) := 1 + z |
| 102 | +@[simp] def baz (z : Nat) := 1 + z |
| 103 | +
|
| 104 | +@[simp] def foo : Nat → Nat → Nat |
| 105 | + | 0, z => bar z |
| 106 | + | _+1, z => baz z |
| 107 | +
|
| 108 | +example : foo x y = 1 + y := by |
| 109 | + cases x <;> simp? -- two printouts: |
| 110 | + -- "Try this: simp only [foo, bar]" |
| 111 | + -- "Try this: simp only [foo, baz]" |
| 112 | +
|
| 113 | +example : foo x y = 1 + y := by |
| 114 | + squeeze_scope |
| 115 | + cases x <;> simp -- only one printout: "Try this: simp only [foo, baz, bar]" |
| 116 | +``` |
| 117 | +-/ |
| 118 | +macro (name := squeezeScope) "squeeze_scope " seq:tacticSeq : tactic => do |
| 119 | + let a ← withFreshMacroScope `(a) |
| 120 | + let seq ← seq.raw.rewriteBottomUpM fun stx => |
| 121 | + match stx.getKind with |
| 122 | + | ``dsimp | ``simpAll | ``simp => do |
| 123 | + withFreshMacroScope `(tactic| squeeze_wrap $a x => $stx) |
| 124 | + | _ => pure stx |
| 125 | + `(tactic| squeeze_scope $a => $seq) |
| 126 | + |
| 127 | +open Meta |
| 128 | + |
| 129 | +/-- |
| 130 | +We implement `squeeze_scope` using a global variable that tracks all `squeeze_scope` invocations |
| 131 | +in flight. It is a map `a ↦ (x ↦ (stx, simps))` where `a` is a unique identifier for |
| 132 | +the `squeeze_scope` invocation which is shared with all contained simps, and `x` is a unique |
| 133 | +identifier for a particular piece of simp syntax (which can be called multiple times). |
| 134 | +Within that, `stx` is the simp syntax itself, and `simps` is the aggregated list of simps used |
| 135 | +so far. |
| 136 | +-/ |
| 137 | +initialize squeezeScopes : IO.Ref (NameMap (NameMap (Syntax × List Simp.UsedSimps))) ← IO.mkRef {} |
| 138 | + |
| 139 | +elab_rules : tactic |
| 140 | + | `(tactic| squeeze_scope $a => $tac) => do |
| 141 | + let a := a.getId |
| 142 | + let old ← squeezeScopes.modifyGet fun map => (map.find? a, map.insert a {}) |
| 143 | + let reset map := match old with | some old => map.insert a old | none => map.erase a |
| 144 | + let new ← try |
| 145 | + Elab.Tactic.evalTactic tac |
| 146 | + squeezeScopes.modifyGet fun map => (map.find? a, reset map) |
| 147 | + catch e => |
| 148 | + squeezeScopes.modify reset |
| 149 | + throw e |
| 150 | + if let some new := new then |
| 151 | + for (_, stx, usedSimps) in new do |
| 152 | + let usedSimps := usedSimps.foldl (fun s usedSimps => usedSimps.fold .insert s) {} |
| 153 | + Elab.Tactic.traceSimpCall stx usedSimps |
| 154 | + |
| 155 | +-- TODO: move to core |
| 156 | +/-- Implementation of `dsimp`. -/ |
| 157 | +def dsimpLocation' (ctx : Simp.Context) (loc : Location) : TacticM Simp.UsedSimps := do |
| 158 | + match loc with |
| 159 | + | Location.targets hyps simplifyTarget => |
| 160 | + withMainContext do |
| 161 | + let fvarIds ← getFVarIds hyps |
| 162 | + go fvarIds simplifyTarget |
| 163 | + | Location.wildcard => |
| 164 | + withMainContext do |
| 165 | + go (← (← getMainGoal).getNondepPropHyps) (simplifyTarget := true) |
| 166 | +where |
| 167 | + /-- Implementation of `dsimp`. -/ |
| 168 | + go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM Simp.UsedSimps := do |
| 169 | + let mvarId ← getMainGoal |
| 170 | + let (result?, usedSimps) ← |
| 171 | + dsimpGoal mvarId ctx (simplifyTarget := simplifyTarget) (fvarIdsToSimp := fvarIdsToSimp) |
| 172 | + match result? with |
| 173 | + | none => replaceMainGoal [] |
| 174 | + | some mvarId => replaceMainGoal [mvarId] |
| 175 | + pure usedSimps |
| 176 | + |
| 177 | +elab_rules : tactic |
| 178 | + | `(tactic| squeeze_wrap $a $x => $tac) => do |
| 179 | + let stx := tac.raw |
| 180 | + let usedSimps ← match stx.getKind with |
| 181 | + | ``Parser.Tactic.simp => do |
| 182 | + let { ctx, dischargeWrapper } ← withMainContext <| mkSimpContext stx (eraseLocal := false) |
| 183 | + dischargeWrapper.with fun discharge? => |
| 184 | + simpLocation ctx discharge? (expandOptLocation stx[5]) |
| 185 | + | ``Parser.Tactic.simpAll => do |
| 186 | + let { ctx, .. } ← mkSimpContext stx |
| 187 | + (eraseLocal := true) (kind := .simpAll) (ignoreStarArg := true) |
| 188 | + let (result?, usedSimps) ← simpAll (← getMainGoal) ctx |
| 189 | + match result? with |
| 190 | + | none => replaceMainGoal [] |
| 191 | + | some mvarId => replaceMainGoal [mvarId] |
| 192 | + pure usedSimps |
| 193 | + | ``Parser.Tactic.dsimp => do |
| 194 | + let { ctx, .. } ← withMainContext <| mkSimpContext stx (eraseLocal := false) (kind := .dsimp) |
| 195 | + dsimpLocation' ctx (expandOptLocation stx[5]) |
| 196 | + | _ => Elab.throwUnsupportedSyntax |
| 197 | + let a := a.getId; let x := x.getId |
| 198 | + squeezeScopes.modify fun map => Id.run do |
| 199 | + let some map1 := map.find? a | return map |
| 200 | + let newSimps := match map1.find? x with |
| 201 | + | some (stx, oldSimps) => (stx, usedSimps :: oldSimps) |
| 202 | + | none => (stx, [usedSimps]) |
| 203 | + map.insert a (map1.insert x newSimps) |
0 commit comments