Moving the last parts of the Ltac engine to hightactics.

11 files changed, 41 insertions, 27 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 761c41da6..fc6ff03b4 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -140,8 +140,6 @@ si après Intros la conclusion matche le pattern.
 
 (* conclPattern doit échouer avec error car il est rattraper par tclFIRST *)
 
-let (forward_interp_tactic, extern_interp) = Hook.make ()
-
 let conclPattern concl pat tac =
   let constr_bindings env sigma =
     match pat with
@@ -156,7 +154,13 @@ let conclPattern concl pat tac =
      let env = Proofview.Goal.env gl in
      let sigma = Tacmach.New.project gl in
        constr_bindings env sigma >>= fun constr_bindings ->
-     Hook.get forward_interp_tactic constr_bindings tac
+     let open Genarg in
+     let open Geninterp in
+     let inj c = Val.Dyn (val_tag (topwit Constrarg.wit_constr), c) in
+     let fold id c accu = Id.Map.add id (inj c) accu in
+     let lfun = Id.Map.fold fold constr_bindings Id.Map.empty in
+     let ist = { lfun; extra = TacStore.empty } in
+     Ftactic.run (Geninterp.generic_interp ist tac) (fun _ -> Proofview.tclUNIT ())
   end }
 
 (***********************************************************)
diff --git a/tactics/auto.mli b/tactics/auto.mli
index cd2de99be..8c4f35904 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -13,9 +13,6 @@ open Pattern
 open Decl_kinds
 open Hints
 
-val extern_interp :
-  (patvar_map -> Tacexpr.glob_tactic_expr -> unit Proofview.tactic) Hook.t
-
 (** Auto and related automation tactics *)
 
 val priority : ('a * full_hint) list -> ('a * full_hint) list
@@ -35,7 +32,7 @@ val unify_resolve : polymorphic -> Unification.unify_flags -> (raw_hint * clause
    [Pattern.somatches], then replace [?1] [?2] metavars in tacast by the
    right values to build a tactic *)
 
-val conclPattern : constr -> constr_pattern option -> Tacexpr.glob_tactic_expr -> unit Proofview.tactic
+val conclPattern : constr -> constr_pattern option -> Genarg.glob_generic_argument -> unit Proofview.tactic
 
 (** The Auto tactic *)
 
diff --git a/tactics/hightactics.mllib b/tactics/hightactics.mllib
index 468b938b6..7987d774d 100644
--- a/tactics/hightactics.mllib
+++ b/tactics/hightactics.mllib
@@ -1,3 +1,6 @@
+Tacsubst
+Tacenv
+Tactic_debug
 Tacintern
 Tacentries
 Tacinterp
diff --git a/tactics/hints.ml b/tactics/hints.ml
index e5abad686..b2104ba43 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -76,7 +76,7 @@ type 'a hint_ast =
   | Give_exact of 'a
   | Res_pf_THEN_trivial_fail of 'a (* Hint Immediate *)
   | Unfold_nth of evaluable_global_reference       (* Hint Unfold *)
-  | Extern     of glob_tactic_expr       (* Hint Extern *)
+  | Extern     of Genarg.glob_generic_argument (* Hint Extern *)
 
 type hints_path_atom = 
   | PathHints of global_reference list
@@ -749,6 +749,7 @@ let make_unfold eref =
      code = with_uid (Unfold_nth eref) })
 
 let make_extern pri pat tacast =
+  let tacast = Genarg.in_gen (Genarg.glbwit Constrarg.wit_ltac) tacast in
   let hdconstr = Option.map try_head_pattern pat in
   (hdconstr,
    { pri = pri;
@@ -900,7 +901,7 @@ let subst_autohint (subst, obj) =
           let ref' = subst_evaluable_reference subst ref in
           if ref==ref' then data.code.obj else Unfold_nth ref'
       | Extern tac ->
-	  let tac' = Tacsubst.subst_tactic subst tac in
+	  let tac' = Genintern.generic_substitute subst tac in
 	  if tac==tac' then data.code.obj else Extern tac'
     in
     let name' = subst_path_atom subst data.name in
@@ -1219,7 +1220,7 @@ let pr_hint h = match h.obj with
           env
         with e when Errors.noncritical e -> Global.env ()
       in
-      (str "(*external*) " ++ Pptactic.pr_glob_tactic env tac)
+      (str "(*external*) " ++ Pptactic.pr_glb_generic env tac)
 
 let pr_id_hint (id, v) =
   (pr_hint v.code ++ str"(level " ++ int v.pri ++ str", id " ++ int id ++ str ")" ++ spc ())
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 3e08060f8..df9d79212 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -33,7 +33,7 @@ type 'a hint_ast =
   | Give_exact of 'a
   | Res_pf_THEN_trivial_fail of 'a (* Hint Immediate *)
   | Unfold_nth of evaluable_global_reference       (* Hint Unfold *)
-  | Extern     of Tacexpr.glob_tactic_expr       (* Hint Extern *)
+  | Extern     of Genarg.glob_generic_argument       (* Hint Extern *)
 
 type hint
 type raw_hint = constr * types * Univ.universe_context_set
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 89dc843cb..a75805b4f 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -795,6 +795,7 @@ let () =
   Genintern.register_intern0 wit_ident intern_ident';
   Genintern.register_intern0 wit_var (lift intern_hyp);
   Genintern.register_intern0 wit_tactic (lift intern_tactic_or_tacarg);
+  Genintern.register_intern0 wit_ltac (lift intern_tactic_or_tacarg);
   Genintern.register_intern0 wit_sort (fun ist s -> (ist, s));
   Genintern.register_intern0 wit_quant_hyp (lift intern_quantified_hypothesis);
   Genintern.register_intern0 wit_constr (fun ist c -> (ist,intern_constr ist c));
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 6bf0e2aa7..4506f8159 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -365,7 +365,7 @@ let debugging_exception_step ist signal_anomaly e pp =
     if signal_anomaly then explain_logic_error
     else explain_logic_error_no_anomaly in
   debugging_step ist (fun () ->
-    pp() ++ spc() ++ str "raised the exception" ++ fnl() ++ !explain_exc e)
+    pp() ++ spc() ++ str "raised the exception" ++ fnl() ++ explain_exc e)
 
 let error_ltac_variable loc id env v s =
    user_err_loc (loc, "", str "Ltac variable " ++ pr_id id ++
@@ -2144,6 +2144,10 @@ let () =
   Geninterp.register_interp0 wit_tactic interp
 
 let () =
+  let interp ist tac = interp_tactic ist tac >>= fun () -> Ftactic.return () in
+  Geninterp.register_interp0 wit_ltac interp
+
+let () =
   Geninterp.register_interp0 wit_uconstr (fun ist c -> Ftactic.nf_enter { enter = begin fun gl ->
     Ftactic.return (interp_uconstr ist (Proofview.Goal.env gl) c)
   end })
@@ -2175,12 +2179,6 @@ let _ =
   in
   Hook.set Pretyping.genarg_interp_hook eval
 
-let _ = Hook.set Auto.extern_interp
-  (fun l ->
-    let lfun = Id.Map.map (fun c -> Value.of_constr c) l in
-    let ist = { (default_ist ()) with lfun; } in
-    interp_tactic ist)
-
 (** Used in tactic extension **)
 
 let dummy_id = Id.of_string "_"
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 55941c1ca..4059877b7 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -299,6 +299,7 @@ let () =
   Genintern.register_subst0 wit_var (fun _ v -> v);
   Genintern.register_subst0 wit_intro_pattern (fun _ v -> v);
   Genintern.register_subst0 wit_tactic subst_tactic;
+  Genintern.register_subst0 wit_ltac subst_tactic;
   Genintern.register_subst0 wit_constr subst_glob_constr;
   Genintern.register_subst0 wit_sort (fun _ v -> v);
   Genintern.register_subst0 wit_clause_dft_concl (fun _ v -> v);
diff --git a/tactics/tactic_debug.ml b/tactics/tactic_debug.ml
index e991eb86d..d661f9677 100644
--- a/tactics/tactic_debug.ml
+++ b/tactics/tactic_debug.ml
@@ -14,6 +14,7 @@ open Termops
 open Nameops
 open Proofview.Notations
 
+
 let (ltac_trace_info : ltac_trace Exninfo.t) = Exninfo.make ()
 
 let prtac x =
@@ -34,9 +35,11 @@ type debug_info =
   | DebugOff
 
 (* An exception handler *)
-let explain_logic_error = ref (fun e -> mt())
+let explain_logic_error e =
+  Errors.print (fst (Cerrors.process_vernac_interp_error (e, Exninfo.null)))
 
-let explain_logic_error_no_anomaly = ref (fun e -> mt())
+let explain_logic_error_no_anomaly e =
+  Errors.print_no_report (fst (Cerrors.process_vernac_interp_error (e, Exninfo.null)))
 
 let msg_tac_debug s = Proofview.NonLogical.print_debug (s++fnl())
 let msg_tac_notice s = Proofview.NonLogical.print_notice (s++fnl())
@@ -202,7 +205,7 @@ let debug_prompt lev tac f =
         (Proofview.tclLIFT begin
           (skip:=0) >> (skipped:=0) >>
             if Logic.catchable_exception reraise then
-              msg_tac_debug (str "Level " ++ int lev ++ str ": " ++ Pervasives.(!) explain_logic_error reraise)
+              msg_tac_debug (str "Level " ++ int lev ++ str ": " ++ explain_logic_error reraise)
             else return ()
         end)
         (Proofview.tclZERO ~info reraise)
@@ -304,7 +307,7 @@ let db_logic_failure debug err =
   is_debug debug >>= fun db ->
   if db then
   begin
-    msg_tac_debug (Pervasives.(!) explain_logic_error err) >>
+    msg_tac_debug (explain_logic_error err) >>
     msg_tac_debug (str "This rule has failed due to a logic error!" ++ fnl() ++
            str "Let us try the next one...")
   end
@@ -398,3 +401,12 @@ let extract_ltac_trace trace eloc =
         | [] -> Loc.ghost in
         aux trace in
     None, best_loc
+
+let get_ltac_trace (_, info) =
+  let ltac_trace = Exninfo.get info ltac_trace_info in
+  let loc = Option.default Loc.ghost (Loc.get_loc info) in
+  match ltac_trace with
+  | None -> None
+  | Some trace -> Some (extract_ltac_trace trace loc)
+
+let () = Cerrors.register_additional_error_info get_ltac_trace
diff --git a/tactics/tactic_debug.mli b/tactics/tactic_debug.mli
index 523398e75..520fb41ef 100644
--- a/tactics/tactic_debug.mli
+++ b/tactics/tactic_debug.mli
@@ -61,13 +61,13 @@ val db_matching_failure : debug_info -> unit Proofview.NonLogical.t
 val db_eval_failure : debug_info -> Pp.std_ppcmds -> unit Proofview.NonLogical.t
 
 (** An exception handler *)
-val explain_logic_error: (exn -> Pp.std_ppcmds) ref
+val explain_logic_error: exn -> Pp.std_ppcmds
 
 (** For use in the Ltac debugger: some exception that are usually
    consider anomalies are acceptable because they are caught later in
    the process that is being debugged.  One should not require
    from users that they report these anomalies. *)
-val explain_logic_error_no_anomaly : (exn -> Pp.std_ppcmds) ref
+val explain_logic_error_no_anomaly : exn -> Pp.std_ppcmds
 
 (** Prints a logic failure message for a rule *)
 val db_logic_failure : debug_info -> exn -> unit Proofview.NonLogical.t
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index b495a885f..cb327e52c 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -14,11 +14,8 @@ Equality
 Contradiction
 Inv
 Leminv
-Tacsubst
 Taccoerce
-Tacenv
 Hints
 Auto
 Tactic_matching
-Tactic_debug
 Term_dnet