feat(tactic/tidy): add tidy? syntax for reporting a tactic script

Author: kim-em

docs/tactics.md

@@ -487,18 +487,19 @@ same type, or the type `α → β → tactic γ → tactic γ` or
 In particular, `tidy` uses the `chain` tactic to repeatedly apply a list of tactics to
 the goal and recursively on new goals, until no tactic makes further progress.
 
-`tidy` can report the tactic script it found using `tidy { trace_result := tt }`. As an example
+`tidy` can report the tactic script it found using `tidy?`. As an example
 ```lean
 example : ∀ x : unit, x = unit.star :=
 begin
-  tidy {trace_result:=tt} -- Prints the trace message: "intros x, exact dec_trivial"
+  tidy? -- Prints the trace message: "intros x, exact dec_trivial"
 end
 ```
 
 The default list of tactics can be found by looking up the definition of
 [`default_tidy_tactics`](https://github.com/leanprover/mathlib/blob/master/tactic/tidy.lean).
 
-This list can be overriden using `tidy { tactics :=  ... }`. (The list must be a list of `tactic string`.)
+This list can be overriden using `tidy { tactics :=  ... }`. (The list must be a list of
+`tactic string`, so that `tidy?` can report a usable tactic script.)
 
 ## linarith
 

src/tactic/tidy.lean

@@ -21,7 +21,7 @@ meta def name_to_tactic (n : name) : tactic string :=
 do d ← get_decl n,
    e ← mk_const n,
    let t := d.type,
-   if (t =ₐ `(tactic unit)) then 
+   if (t =ₐ `(tactic unit)) then
      (eval_expr (tactic unit) e) >>= (λ t, t >> pure n.to_string)
    else if (t =ₐ `(tactic string)) then
      (eval_expr (tactic string) e) >>= (λ t, t)
@@ -40,7 +40,7 @@ do ng ← num_goals,
    else "ext1"
 
 meta def default_tactics : list (tactic string) :=
-[ reflexivity                                 >> pure "refl", 
+[ reflexivity                                 >> pure "refl",
   `[exact dec_trivial]                        >> pure "exact dec_trivial",
   propositional_goal >> assumption            >> pure "assumption",
   ext1_wrapper,
@@ -49,7 +49,7 @@ meta def default_tactics : list (tactic string) :=
   `[apply_auto_param]                         >> pure "apply_auto_param",
   `[dsimp at *]                               >> pure "dsimp at *",
   `[simp at *]                                >> pure "simp at *",
-  fsplit                                      >> pure "fsplit", 
+  fsplit                                      >> pure "fsplit",
   injections_and_clear                        >> pure "injections_and_clear",
   propositional_goal >> (`[solve_by_elim])    >> pure "solve_by_elim",
   `[unfold_aux]                               >> pure "unfold_aux",
@@ -74,11 +74,14 @@ end tidy
 meta def tidy (cfg : tidy.cfg := {}) := tactic.tidy.core cfg >> skip
 
 namespace interactive
-meta def tidy (cfg : tidy.cfg := {}) := tactic.tidy cfg
+open lean.parser interactive
+
+meta def tidy (trace : parse $ optional (tk "?")) (cfg : tidy.cfg := {}) :=
+tactic.tidy { trace_result := trace.is_some, ..cfg }
 end interactive
 
 @[hole_command] meta def tidy_hole_cmd : hole_command :=
-{ name := "tidy", 
+{ name := "tidy",
   descr := "Use `tidy` to complete the goal.",
   action := λ _, do script ← tidy.core, return [("begin " ++ (", ".intercalate script) ++ " end", "by tidy")] }
 

test/tidy.lean

@@ -10,22 +10,22 @@ namespace tidy.test
 
 meta def interactive_simp := `[simp]
 
-def tidy_test_0 : ∀ x : unit, x = unit.star := 
+def tidy_test_0 : ∀ x : unit, x = unit.star :=
 begin
   success_if_fail { chain [ interactive_simp ] },
   intro1,
   induction x,
   refl
 end
-def tidy_test_1 (a : string): ∀ x : unit, x = unit.star := 
+def tidy_test_1 (a : string): ∀ x : unit, x = unit.star :=
 begin
   tidy -- intros x, exact dec_trivial
 end
 
 structure A :=
 (z : ℕ)
 
-structure B := 
+structure B :=
 (a : A)
 (aa : a.z = 0)
 
@@ -41,14 +41,14 @@ structure D :=
 
 open tactic
 
-def d : D := 
+def d : D :=
 begin
-  tidy, 
+  tidy,
   -- /- obviously says -/ fsplit, work_on_goal 0 { fsplit, work_on_goal 0 { fsplit }, work_on_goal 1 { refl } }, work_on_goal 0 { fsplit, work_on_goal 0 { fsplit }, work_on_goal 1 { fsplit, work_on_goal 0 { fsplit }, work_on_goal 1 { refl } }, work_on_goal 1 { refl } }, refl
 end.
 
 def f : unit → unit → unit := by tidy -- intros a a_1, cases a_1, cases a, fsplit
 
 def g (P Q : Prop) (p : P) (h : P ↔ Q) : Q := by tidy
 
-end tidy.test
+end tidy.test