Opaque implementation of auto tactics.

We provide an eliminator ensuring that the AST will be used to build a tactic,
so that we can stuff arbitrary things inside. An escape function is also provided
for backward compatibility.

6 files changed, 46 insertions, 34 deletions

diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 2f7f21e41..7d034db55 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -209,7 +209,7 @@ open Hints
 let extend_with_auto_hints l seq gl=
   let seqref=ref seq in
   let f p_a_t =
-    match p_a_t.code with
+    match repr_auto_tactic p_a_t.code with
 	Res_pf (c,_) | Give_exact (c,_)
       | Res_pf_THEN_trivial_fail (c,_) ->
 	  (try
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 45052685d..46274f832 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -359,8 +359,7 @@ and my_find_search_delta db_list local_db hdc concl =
       	(local_db::db_list)
 
 and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly})) =
-  let tactic = 
-    match t with
+  let tactic = function
     | Res_pf (c,cl) -> unify_resolve_gen poly flags (c,cl)
     | ERes_pf _ -> Proofview.V82.tactic (fun gl -> error "eres_pf")
     | Give_exact (c, cl)  -> exact poly (c, cl)
@@ -378,7 +377,7 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly}))
     | Extern tacast -> 
       conclPattern concl p tacast
   in
-  tclLOG dbg (fun () -> pr_autotactic t) tactic
+  tclLOG dbg (fun () -> pr_autotactic t) (run_auto_tactic t tactic)
 
 and trivial_resolve dbg mod_delta db_list local_db cl =
   try
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 98266a4b6..e11458c04 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -221,20 +221,19 @@ and e_my_find_search db_list local_db hdc complete sigma concl =
   in
   let tac_of_hint =
     fun (flags, {pri = b; pat = p; poly = poly; code = t; name = name}) ->
-      let tac =
-	match t with
-	  | Res_pf (term,cl) -> with_prods nprods poly (term,cl) (unify_resolve poly flags)
-	  | ERes_pf (term,cl) -> with_prods nprods poly (term,cl) (unify_e_resolve poly flags)
-	  | Give_exact c -> e_give_exact flags poly c
-	  | Res_pf_THEN_trivial_fail (term,cl) ->
-              tclTHEN (with_prods nprods poly (term,cl) (unify_e_resolve poly flags))
-	        (if complete then tclIDTAC else e_trivial_fail_db db_list local_db)
-	  | Unfold_nth c -> tclWEAK_PROGRESS (unfold_in_concl [AllOccurrences,c])
-	  | Extern tacast ->
-	    Proofview.V82.of_tactic (conclPattern concl p tacast)
+      let tac = function
+      | Res_pf (term,cl) -> Proofview.V82.tactic (with_prods nprods poly (term,cl) (unify_resolve poly flags))
+      | ERes_pf (term,cl) -> Proofview.V82.tactic (with_prods nprods poly (term,cl) (unify_e_resolve poly flags))
+      | Give_exact c -> Proofview.V82.tactic (e_give_exact flags poly c)
+      | Res_pf_THEN_trivial_fail (term,cl) ->
+          Proofview.V82.tactic (tclTHEN (with_prods nprods poly (term,cl) (unify_e_resolve poly flags))
+            (if complete then tclIDTAC else e_trivial_fail_db db_list local_db))
+      | Unfold_nth c -> Proofview.V82.tactic (tclWEAK_PROGRESS (unfold_in_concl [AllOccurrences,c]))
+      | Extern tacast -> conclPattern concl p tacast
       in
+      let tac = Proofview.V82.of_tactic (run_auto_tactic t tac) in
       let tac = if complete then tclCOMPLETE tac else tac in
-	match t with
+	match repr_auto_tactic t with
 	| Extern _ -> (tac,b,true, name, lazy (pr_autotactic t))
 	| _ ->
 (* 	  let tac gl = with_pattern (pf_env gl) (project gl) flags p concl tac gl in *)
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 7af43e606..27c3569da 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -162,18 +162,18 @@ and e_my_find_search db_list local_db hdc concl =
   let tac_of_hint =
     fun (st, {pri = b; pat = p; code = t; poly = poly}) ->
       (b,
-       let tac =
-	 match t with
-	   | Res_pf (term,cl) -> Proofview.V82.of_tactic (unify_resolve poly st (term,cl))
-	   | ERes_pf (term,cl) -> unify_e_resolve poly st (term,cl)
-	   | Give_exact (c,cl) -> e_exact poly st (c,cl)
-	   | Res_pf_THEN_trivial_fail (term,cl) ->
-               tclTHEN (unify_e_resolve poly st (term,cl))
-		 (e_trivial_fail_db db_list local_db)
-	   | Unfold_nth c -> reduce (Unfold [AllOccurrences,c]) onConcl
-	   | Extern tacast -> Proofview.V82.of_tactic (conclPattern concl p tacast)
+        let tac = function
+        | Res_pf (term,cl) -> unify_resolve poly st (term,cl)
+        | ERes_pf (term,cl) -> Proofview.V82.tactic (unify_e_resolve poly st (term,cl))
+        | Give_exact (c,cl) -> Proofview.V82.tactic (e_exact poly st (c,cl))
+        | Res_pf_THEN_trivial_fail (term,cl) ->
+          Proofview.V82.tactic (tclTHEN (unify_e_resolve poly st (term,cl))
+            (e_trivial_fail_db db_list local_db))
+        | Unfold_nth c -> Proofview.V82.tactic (reduce (Unfold [AllOccurrences,c]) onConcl)
+        | Extern tacast -> conclPattern concl p tacast
        in
-       (tac,lazy (pr_autotactic t)))
+       let tac = Proofview.V82.of_tactic (run_auto_tactic t tac) in
+       (tac, lazy (pr_autotactic t)))
   in
   List.map tac_of_hint hintl
 
diff --git a/tactics/hints.ml b/tactics/hints.ml
index bbd66dfd4..cf1754e38 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -68,7 +68,7 @@ let decompose_app_bound t =
 (*           The Type of Constructions Autotactic Hints                 *)
 (************************************************************************)
 
-type 'a auto_tactic =
+type 'a auto_tactic_ast =
   | Res_pf     of 'a (* Hint Apply *)
   | ERes_pf    of 'a (* Hint EApply *)
   | Give_exact of 'a
@@ -92,18 +92,23 @@ type hint_term =
   | IsGlobRef of global_reference
   | IsConstr of constr * Univ.universe_context_set
 
+type 'a auto_tactic = 'a auto_tactic_ast
+
 type 'a gen_auto_tactic = {
   pri  : int;            (* A number lower is higher priority *)
   poly  : polymorphic;    (** Is the hint polymorpic and hence should be refreshed at each application *)
   pat  : constr_pattern option; (* A pattern for the concl of the Goal *)
   name  : hints_path_atom; (* A potential name to refer to the hint *) 
-  code : 'a auto_tactic     (* the tactic to apply when the concl matches pat *)
+  code : 'a     (* the tactic to apply when the concl matches pat *)
 }
 
-type pri_auto_tactic = (constr * clausenv) gen_auto_tactic
+type pri_auto_tactic = (constr * clausenv) auto_tactic gen_auto_tactic
 
 type hint_entry = global_reference option * 
-  (constr * types * Univ.universe_context_set) gen_auto_tactic
+  (constr * types * Univ.universe_context_set) auto_tactic_ast gen_auto_tactic
+
+let run_auto_tactic tac k = k tac
+let repr_auto_tactic tac = tac
 
 let eq_hints_path_atom p1 p2 = match p1, p2 with
 | PathHints gr1, PathHints gr2 -> List.equal eq_gr gr1 gr2
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 9a781c722..958cca1c3 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -28,7 +28,7 @@ val decompose_app_bound : constr -> global_reference * constr array
 
 (** Pre-created hint databases *)
 
-type 'a auto_tactic =
+type 'a auto_tactic_ast =
   | Res_pf     of 'a (* Hint Apply *)
   | ERes_pf    of 'a (* Hint EApply *)
   | Give_exact of 'a
@@ -36,6 +36,8 @@ type 'a auto_tactic =
   | Unfold_nth of evaluable_global_reference       (* Hint Unfold *)
   | Extern     of Tacexpr.glob_tactic_expr       (* Hint Extern *)
 
+type 'a auto_tactic
+
 type hints_path_atom = 
   | PathHints of global_reference list
   | PathAny
@@ -45,10 +47,10 @@ type 'a gen_auto_tactic = private {
   poly  : polymorphic;    (** Is the hint polymorpic and hence should be refreshed at each application *)
   pat   : constr_pattern option; (** A pattern for the concl of the Goal *)
   name  : hints_path_atom; (** A potential name to refer to the hint *) 
-  code  : 'a auto_tactic; (** the tactic to apply when the concl matches pat *)
+  code  : 'a; (** the tactic to apply when the concl matches pat *)
 }
 
-type pri_auto_tactic = (constr * clausenv) gen_auto_tactic
+type pri_auto_tactic = (constr * clausenv) auto_tactic gen_auto_tactic
 
 type search_entry
 
@@ -195,6 +197,13 @@ val make_extern :
   int -> constr_pattern option -> Tacexpr.glob_tactic_expr
       -> hint_entry
 
+val run_auto_tactic : 'a auto_tactic ->
+  ('a auto_tactic_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic
+
+(** This function is for backward compatibility only, not to use in newly
+    written code. *)
+val repr_auto_tactic : 'a auto_tactic -> 'a auto_tactic_ast
+
 val extern_intern_tac :
   (patvar list -> Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_expr) Hook.t