Moving the Tauto tactic to proper Ltac.

This gets rid of brittle code written in ML files through Ltac quotations, and
reduces the dependance of Coq to such a feature. This also fixes the particular
instance of bug #2800, although the underlying issue is still there.

2 files changed, 40 insertions, 209 deletions

diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 5485f344b3..e0427ae89a 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -14,6 +14,7 @@ open Names
 open Pp
 open Genarg
 open Stdarg
+open Misctypes
 open Tacexpr
 open Tacinterp
 open Tactics
@@ -90,6 +91,7 @@ let _ =
 
 (** Base tactics *)
 
+let loc = Loc.ghost
 let idtac = Proofview.tclUNIT ()
 let fail = Proofview.tclINDEPENDENT (tclFAIL 0 (Pp.mt ()))
 
@@ -112,38 +114,9 @@ let split = Tactics.split_with_bindings false [Misctypes.NoBindings]
 
 (** Test *)
 
-let make_lfun l =
-  let fold accu (id, v) = Id.Map.add (Id.of_string id) v accu in
-  List.fold_left fold Id.Map.empty l
-
-let register_tauto_tactic tac name =
-  let name = { mltac_plugin = "tauto"; mltac_tactic = name; } in
-  let entry = { mltac_name = name; mltac_index = 0 } in
-  Tacenv.register_ml_tactic name [| tac |];
-  TacML (Loc.ghost, entry, [])
-
-let tacticIn_ist tac name =
-  let tac _ ist =
-    let avoid = Option.default [] (TacStore.get ist.extra f_avoid_ids) in
-    let debug = Option.default Tactic_debug.DebugOff (TacStore.get ist.extra f_debug) in
-    let (tac, ist) = tac ist in
-    interp_tac_gen ist.lfun avoid debug tac
-  in
-  register_tauto_tactic tac name
-
-let tacticIn tac name =
-  tacticIn_ist (fun ist -> tac ist, ist) name
-
-let push_ist ist args =
-  let fold accu (id, arg) = Id.Map.add (Id.of_string id) arg accu in
-  let lfun = List.fold_left fold ist.lfun args in
-  { ist with lfun = lfun }
-
 let is_empty _ ist =
   if is_empty_type (assoc_var "X1" ist) then idtac else fail
 
-let t_is_empty = register_tauto_tactic is_empty "is_empty"
-
 (* Strictly speaking, this exceeds the propositional fragment as it
    matches also equality types (and solves them if a reflexivity) *)
 let is_unit_or_eq _ ist =
@@ -151,16 +124,6 @@ let is_unit_or_eq _ ist =
   let test = if flags.strict_unit then is_unit_type else is_unit_or_eq_type in
   if test (assoc_var "X1" ist) then idtac else fail
 
-let t_is_unit_or_eq = register_tauto_tactic is_unit_or_eq "is_unit_or_eq"
-
-let is_record t =
-  let (hdapp,args) = decompose_app t in
-    match (kind_of_term hdapp) with
-      | Ind (ind,u) ->
-          let (mib,mip) = Global.lookup_inductive ind in
-	    mib.Declarations.mind_record <> None
-      | _ -> false
-
 let bugged_is_binary t =
   isApp t &&
   let (hdapp,args) = decompose_app t in
@@ -182,8 +145,6 @@ let is_conj _ ist =
     then idtac
     else fail
 
-let t_is_conj = register_tauto_tactic is_conj "is_conj"
-
 let flatten_contravariant_conj _ ist =
   let flags = assoc_flags ist in
   let typ = assoc_var "X1" ist in
@@ -200,18 +161,8 @@ let flatten_contravariant_conj _ ist =
     tclTHENLIST [assert_ ~by newtyp; clear (destVar hyp)]
   | _ -> fail
 
-let t_flatten_contravariant_conj =
-  register_tauto_tactic flatten_contravariant_conj "flatten_contravariant_conj"
-
 (** Dealing with disjunction *)
 
-let constructor i =
-  let name = { Tacexpr.mltac_plugin = "coretactics"; mltac_tactic = "constructor" } in
-  (** Take care of the index: this is the second entry in constructor. *)
-  let name = { Tacexpr.mltac_name = name; mltac_index = 1 } in
-  let i = in_gen (rawwit Constrarg.wit_int_or_var) (Misctypes.ArgArg i) in
-  Tacexpr.TacML (Loc.ghost, name, [TacGeneric i])
-
 let is_disj _ ist =
   let flags = assoc_flags ist in
   let t = assoc_var "X1" ist in
@@ -222,8 +173,6 @@ let is_disj _ ist =
   then idtac
   else fail
 
-let t_is_disj = register_tauto_tactic is_disj "is_disj"
-
 let flatten_contravariant_disj _ ist =
   let flags = assoc_flags ist in
   let typ = assoc_var "X1" ist in
@@ -245,159 +194,30 @@ let flatten_contravariant_disj _ ist =
       tclTHEN (tclTHENLIST tacs) tac0
   | _ -> fail
 
-let t_flatten_contravariant_disj =
-  register_tauto_tactic flatten_contravariant_disj "flatten_contravariant_disj"
-
-(** Main tactic *)
-
-let not_dep_intros ist =
-  <:tactic<
-  repeat match goal with
-  | |- (forall (_: ?X1), ?X2) => intro
-  | |- (Coq.Init.Logic.not _) => unfold Coq.Init.Logic.not at 1; intro
-  end >>
-
-let t_not_dep_intros = tacticIn not_dep_intros "not_dep_intros"
-
-let axioms ist =
-  let c1 = constructor 1 in
-    <:tactic<
-    match reverse goal with
-      | |- ?X1 => $t_is_unit_or_eq; $c1
-      | _:?X1 |- _ => $t_is_empty; elimtype X1; assumption
-      | _:?X1 |- ?X1 => assumption
-    end >>
-
-let t_axioms = tacticIn axioms "axioms"
-
-let simplif ist =
-  let c1 = constructor 1 in
-  <:tactic<
-    $t_not_dep_intros;
-    repeat
-       (match reverse goal with
-        | id: ?X1 |- _ => $t_is_conj; elim id; do 2 intro; clear id
-        | id: (Coq.Init.Logic.iff _ _) |- _ => elim id; do 2 intro; clear id
-        | id: (Coq.Init.Logic.not _) |- _ => red in id
-        | id: ?X1 |- _ => $t_is_disj; elim id; intro; clear id
-        | id0: (forall (_: ?X1), ?X2), id1: ?X1|- _ =>
-	    (* generalize (id0 id1); intro; clear id0 does not work
-	       (see Marco Maggiesi's bug PR#301)
-	    so we instead use Assert and exact. *)
-	    assert X2; [exact (id0 id1) | clear id0]
-        | id: forall (_ : ?X1), ?X2|- _ =>
-          $t_is_unit_or_eq; cut X2;
-	    [ intro; clear id
-	    | (* id : forall (_: ?X1), ?X2 |- ?X2 *)
-	      cut X1; [exact id| $c1; fail]
-	    ]
-        | id: forall (_ : ?X1), ?X2|- _ =>
-          $t_flatten_contravariant_conj
-	  (* moved from "id:(?A/\?B)->?X2|-" to "?A->?B->?X2|-" *)
-        | id: forall (_: Coq.Init.Logic.iff ?X1 ?X2), ?X3|- _ =>
-          assert (forall (_: forall _:X1, X2), forall (_: forall _: X2, X1), X3)
-	    by (do 2 intro; apply id; split; assumption);
-            clear id
-        | id: forall (_:?X1), ?X2|- _ =>
-          $t_flatten_contravariant_disj
-	  (* moved from "id:(?A\/?B)->?X2|-" to "?A->?X2,?B->?X2|-" *)
-        | |- ?X1 => $t_is_conj; split
-        | |- (Coq.Init.Logic.iff _ _) => split
-        | |- (Coq.Init.Logic.not _) => red
-        end;
-        $t_not_dep_intros) >>
-
-let t_simplif = tacticIn simplif "simplif"
-
-let tauto_intuit flags t_reduce solver =
-  let flags = Genarg.Val.Dyn (Genarg.val_tag (topwit wit_tauto_flags), flags) in
-  let lfun = make_lfun [("t_solver", solver); ("tauto_flags", flags)] in
-  let ist = { default_ist () with lfun = lfun; } in
-  let vars = [Id.of_string "t_solver"] in
-  (vars, ist, <:tactic<
-   let rec t_tauto_intuit :=
-   ($t_simplif;$t_axioms
-   || match reverse goal with
-      | id:forall(_: forall (_: ?X1), ?X2), ?X3|- _ =>
-	  cut X3;
-	    [ intro; clear id; t_tauto_intuit
-	    | cut (forall (_: X1), X2);
-		[ exact id
-		| generalize (fun y:X2 => id (fun x:X1 => y)); intro; clear id;
-		  solve [ t_tauto_intuit ]]]
-      | id:forall (_:not ?X1), ?X3|- _ =>
-	  cut X3;
-	    [ intro; clear id; t_tauto_intuit
-	    | cut (not X1); [ exact id | clear id; intro; solve [t_tauto_intuit ]]]
-      | |- ?X1 =>
-          $t_is_disj; solve [left;t_tauto_intuit | right;t_tauto_intuit]
-      end
-    ||
-    (* NB: [|- _ -> _] matches any product *)
-    match goal with | |- forall (_ : _),  _ => intro; t_tauto_intuit
-    |  |- _  => $t_reduce;t_solver
-    end
-    ||
-    t_solver
-   ) in t_tauto_intuit >>)
-
-let reduction_not_iff _ist =
-  match !negation_unfolding, unfold_iff () with
+let reduction_not_iff _ ist =
+  let avoid = Option.default [] (TacStore.get ist.extra f_avoid_ids) in
+  let debug = Option.default Tactic_debug.DebugOff (TacStore.get ist.extra f_debug) in
+  let tac = match !negation_unfolding, unfold_iff () with
     | true, true -> <:tactic< unfold Coq.Init.Logic.not, Coq.Init.Logic.iff in * >>
     | true, false -> <:tactic< unfold Coq.Init.Logic.not in * >>
     | false, true -> <:tactic< unfold Coq.Init.Logic.iff in * >>
     | false, false -> <:tactic< idtac >>
-
-let t_reduction_not_iff = tacticIn reduction_not_iff "reduction_not_iff"
-
-let intuition_gen ist flags tac =
-  Proofview.Goal.enter { enter = begin fun gl ->
-  let env = Proofview.Goal.env gl in
-  let vars, ist, intuition = tauto_intuit flags t_reduction_not_iff tac in
-  let glb_intuition = Tacintern.glob_tactic_env vars env intuition in
-  eval_tactic_ist ist glb_intuition
-  end }
-
-let tauto_intuitionistic flags =
-  let fail = Value.of_closure (default_ist ()) <:tactic<fail>> in
-  Proofview.tclORELSE
-    (intuition_gen (default_ist ()) flags fail)
-    begin function (e, info) -> match e with
-      | Refiner.FailError _ | UserError _ ->
-          Tacticals.New.tclZEROMSG (str "tauto failed.")
-      | e -> Proofview.tclZERO ~info e
-    end
+  in
+  interp_tac_gen ist.lfun avoid debug tac
 
 let coq_nnpp_path =
   let dir = List.map Id.of_string ["Classical_Prop";"Logic";"Coq"] in
   Libnames.make_path (DirPath.make dir) (Id.of_string "NNPP")
 
-let tauto_classical flags nnpp =
-  Proofview.tclORELSE
-    (Tacticals.New.tclTHEN (apply nnpp) (tauto_intuitionistic flags))
-    begin function (e, info) -> match e with
-      | UserError _ -> Tacticals.New.tclZEROMSG (str "Classical tauto failed.")
-      | e -> Proofview.tclZERO ~info e
-    end
-
-let tauto_gen flags =
-  (* spiwack: I use [tclBIND (tclUNIT ())] as a way to delay the effect
-     (in [constr_of_global]) to the application of the tactic. *)
+let apply_nnpp _ ist =
   Proofview.tclBIND
     (Proofview.tclUNIT ())
     begin fun () -> try
       let nnpp = Universes.constr_of_global (Nametab.global_of_path coq_nnpp_path) in
-    (* try intuitionistic version first to avoid an axiom if possible *)
-      Tacticals.New.tclORELSE (tauto_intuitionistic flags) (tauto_classical flags nnpp)
-    with Not_found ->
-      tauto_intuitionistic flags
+      apply nnpp
+    with Not_found -> tclFAIL 0 (Pp.mt ())
     end
 
-let default_intuition_tac =
-  let tac _ _ = Auto.h_auto None [] None in
-  let tac = register_tauto_tactic tac "auto_with" in
-  Value.of_closure (default_ist ()) tac
-
 (* This is the uniform mode dealing with ->, not, iff and types isomorphic to
    /\ and *, \/ and +, False and Empty_set, True and unit, _and_ eq-like types.
    For the moment not and iff are still always unfolded. *)
@@ -427,23 +247,34 @@ let tauto_power_flags = {
   strict_unit = false
 }
 
-let tauto = tauto_gen tauto_uniform_unit_flags
-let dtauto = tauto_gen tauto_power_flags
-
-TACTIC EXTEND tauto
-| [ "tauto" ] -> [ tauto ]
-END
-
-TACTIC EXTEND dtauto
-| [ "dtauto" ] -> [ dtauto ]
+let with_flags flags ist tac =
+  let f = (loc, Id.of_string "f") in
+  let x = (loc, Id.of_string "x") in
+  let arg = Val.Dyn (val_tag (topwit wit_tauto_flags), flags) in
+  let ist = { ist with lfun = Id.Map.add (snd f) tac (Id.Map.add (snd x) arg ist.lfun) } in
+  eval_tactic_ist ist (TacArg (loc, TacCall (loc, ArgVar f, [Reference (ArgVar x)])))
+
+TACTIC EXTEND with_flags
+| [ "with_uniform_flags" tactic(tac) ] -> [ with_flags tauto_uniform_unit_flags ist tac ]
+| [ "with_legacy_flags" tactic(tac) ] -> [ with_flags tauto_legacy_flags ist tac ]
+| [ "with_power_flags" tactic(tac) ] -> [ with_flags tauto_power_flags ist tac ]
 END
 
-TACTIC EXTEND intuition
-| [ "intuition" ] -> [ intuition_gen ist tauto_uniform_unit_flags default_intuition_tac ]
-| [ "intuition" tactic(t) ] -> [ intuition_gen ist tauto_uniform_unit_flags t ]
-END
-
-TACTIC EXTEND dintuition
-| [ "dintuition" ] -> [ intuition_gen ist tauto_power_flags default_intuition_tac ]
-| [ "dintuition" tactic(t) ] -> [ intuition_gen ist tauto_power_flags t ]
-END
+let register_tauto_tactic_ tac name0 args =
+  let ids = List.map (fun id -> Id.of_string id) args in
+  let ids = List.map (fun id -> Some id) ids in
+  let name = { mltac_plugin = "tauto"; mltac_tactic = name0 ^ "_"; } in
+  let entry = { mltac_name = name; mltac_index = 0 } in
+  let () = Tacenv.register_ml_tactic name [| tac |] in
+  let tac = TacFun (ids, TacML (loc, entry, [])) in
+  let obj () = Tacenv.register_ltac true true (Id.of_string name0) tac in
+  Mltop.declare_cache_obj obj "tauto"
+
+let () = register_tauto_tactic_ is_empty "is_empty" ["tauto_flags"; "X1"]
+let () = register_tauto_tactic_ is_unit_or_eq "is_unit_or_eq" ["tauto_flags"; "X1"]
+let () = register_tauto_tactic_ is_disj "is_disj" ["tauto_flags"; "X1"]
+let () = register_tauto_tactic_ is_conj "is_conj" ["tauto_flags"; "X1"]
+let () = register_tauto_tactic_ flatten_contravariant_disj "flatten_contravariant_disj" ["tauto_flags"; "X1"; "X2"; "id"]
+let () = register_tauto_tactic_ flatten_contravariant_conj "flatten_contravariant_conj" ["tauto_flags"; "X1"; "X2"; "id"]
+let () = register_tauto_tactic_ apply_nnpp "apply_nnpp" []
+let () = register_tauto_tactic_ reduction_not_iff "reduction_not_iff" []
diff --git a/tactics/tauto.mli b/tactics/tauto.mli
new file mode 100644
index 0000000000..e69de29bb2
--- /dev/null
+++ b/tactics/tauto.mli