7 files changed, 203 insertions, 58 deletions

diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 5baa23b3e9..aef5f645f4 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -342,7 +342,7 @@ GRAMMAR EXTEND Gram
   hint:
     [ [ IDENT "Extern"; n = natural; c = OPT Constr.constr_pattern ; "=>";
         tac = Pltac.tactic ->
-        { ComHints.HintsExtern (n,c, in_tac tac) } ] ]
+        { Vernacexpr.HintsExtern (n,c, in_tac tac) } ] ]
   ;
   operconstr: LEVEL "0"
     [ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" ->
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 14fab251d0..0dbf16a821 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -25,27 +25,20 @@ let is_profiling = Flags.profile_ltac
 let set_profiling b = is_profiling := b
 let get_profiling () = !is_profiling
 
-(** LtacProf cannot yet handle backtracking into multi-success tactics.
-    To properly support this, we'd have to somehow recreate our location in the
-    call-stack, and stop/restart the intervening timers. This is tricky and
-    possibly expensive, so instead we currently just emit a warning that
-    profiling results will be off. *)
-let encountered_multi_success_backtracking = ref false
-
-let warn_profile_backtracking =
-  CWarnings.create ~name:"profile-backtracking" ~category:"ltac"
-    (fun () -> strbrk "Ltac Profiler cannot yet handle backtracking \
-       into multi-success tactics; profiling results may be wildly inaccurate.")
-
-let warn_encountered_multi_success_backtracking () =
-  if !encountered_multi_success_backtracking then
-    warn_profile_backtracking ()
-
-let encounter_multi_success_backtracking () =
-  if not !encountered_multi_success_backtracking
+let encountered_invalid_stack_no_self = ref false
+
+let warn_invalid_stack_no_self =
+  CWarnings.create ~name:"profile-invalid-stack-no-self" ~category:"ltac"
+    (fun () -> strbrk
+        "Ltac Profiler encountered an invalid stack (no self \
+         node). This can happen if you reset the profile during \
+         tactic execution.")
+
+let encounter_invalid_stack_no_self () =
+  if not !encountered_invalid_stack_no_self
   then begin
-    encountered_multi_success_backtracking := true;
-    warn_encountered_multi_success_backtracking ()
+    encountered_invalid_stack_no_self := true;
+    warn_invalid_stack_no_self ()
   end
 
 
@@ -76,8 +69,7 @@ module Local = Summary.Local
 let stack = Local.ref ~name:"LtacProf-stack" [empty_treenode root]
 
 let reset_profile_tmp () =
-  Local.(stack := [empty_treenode root]);
-  encountered_multi_success_backtracking := false
+  Local.(stack := [empty_treenode root])
 
 (* ************** XML Serialization  ********************* *)
 
@@ -218,7 +210,6 @@ let to_string ~filter ?(cutoff=0.0) node =
     cumulate tree;
     !global
   in
-  warn_encountered_multi_success_backtracking ();
   let filter s n = filter s && (all_total <= 0.0 || n /. all_total >= cutoff /. 100.0) in
   let msg =
     h 0 (str "total time: " ++ padl 11 (format_sec (all_total))) ++
@@ -296,13 +287,15 @@ let exit_tactic ~count_call start_time c =
   match Local.(!stack) with
   | [] | [_] ->
     (* oops, our stack is invalid *)
-    encounter_multi_success_backtracking ();
+    encounter_invalid_stack_no_self ();
     reset_profile_tmp ()
   | node :: (parent :: rest as full_stack) ->
     let name = string_of_call c in
     if not (String.equal name node.name) then
       (* oops, our stack is invalid *)
-      encounter_multi_success_backtracking ();
+      CErrors.anomaly
+        (Pp.strbrk "Ltac Profiler encountered an invalid stack (wrong self node) \
+                    likely due to backtracking into multi-success tactics.");
     let node = { node with
       total = node.total +. diff;
       local = node.local +. diff;
@@ -332,38 +325,56 @@ let exit_tactic ~count_call start_time c =
     (* Calls are over, we reset the stack and send back data *)
     if rest == [] && get_profiling () then begin
       assert(String.equal root parent.name);
+      encountered_invalid_stack_no_self := false;
       reset_profile_tmp ();
       feedback_results parent
     end
 
-let tclFINALLY tac (finally : unit Proofview.tactic) =
+(** [tclWRAPFINALLY before tac finally] runs [before] before each
+    entry-point of [tac] and passes the result of [before] to
+    [finally], which is then run at each exit-point of [tac],
+    regardless of whether it succeeds or fails.  Said another way, if
+    [tac] succeeds, then it behaves as [before >>= fun v -> tac >>= fun
+    ret -> finally v <*> tclUNIT ret]; otherwise, if [tac] fails with
+    [e], it behaves as [before >>= fun v -> finally v <*> tclZERO
+    e]. *)
+let rec tclWRAPFINALLY before tac finally =
+  let open Proofview in
   let open Proofview.Notations in
-  Proofview.tclIFCATCH
-    tac
-    (fun v -> finally <*> Proofview.tclUNIT v)
-    (fun (exn, info) -> finally <*> Proofview.tclZERO ~info exn)
+  before >>= fun v -> tclCASE tac >>= function
+  | Fail (e, info) -> finally v >>= fun () -> tclZERO ~info e
+  | Next (ret, tac') -> tclOR
+                          (finally v >>= fun () -> tclUNIT ret)
+                          (fun e -> tclWRAPFINALLY before (tac' e) finally)
 
 let do_profile s call_trace ?(count_call=true) tac =
   let open Proofview.Notations in
-  Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
-  if !is_profiling then
-    match call_trace, Local.(!stack) with
-      | (_, c) :: _, parent :: rest ->
-        let name = string_of_call c in
-        let node = get_child name parent in
-        Local.(stack := node :: parent :: rest);
-        Some (time ())
-      | _ :: _, [] -> assert false
-      | _ -> None
-  else None)) >>= function
-  | Some start_time ->
-    tclFINALLY
-      tac
+  (* We do an early check to [is_profiling] so that we save the
+     overhead of [tclWRAPFINALLY] when profiling is not set
+     *)
+  Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> !is_profiling)) >>= function
+  | false -> tac
+  | true ->
+    tclWRAPFINALLY
       (Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
-        (match call_trace with
-        | (_, c) :: _ -> exit_tactic ~count_call start_time c
-        | [] -> ()))))
-  | None -> tac
+           if !is_profiling then
+             match call_trace, Local.(!stack) with
+             | (_, c) :: _, parent :: rest ->
+               let name = string_of_call c in
+               let node = get_child name parent in
+               Local.(stack := node :: parent :: rest);
+               Some (time ())
+             | _ :: _, [] -> assert false
+             | _ -> None
+           else None)))
+      tac
+      (function
+        | Some start_time ->
+          (Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
+               (match call_trace with
+                | (_, c) :: _ -> exit_tactic ~count_call start_time c
+                | [] -> ()))))
+        | None -> Proofview.tclUNIT ())
 
 (* ************** Accumulation of data from workers ************************* *)
 
@@ -396,6 +407,7 @@ let _ =
     | _ -> ()))
 
 let reset_profile () =
+  encountered_invalid_stack_no_self := false;
   reset_profile_tmp ();
   data := SM.empty
 
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 3834b21a14..3b8fb48eb0 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1894,10 +1894,10 @@ let declare_projection name instance_id r =
     in it_mkProd_or_LetIn ccl ctx
   in
   let types = Some (it_mkProd_or_LetIn typ ctx) in
-  let kind, opaque, scope = Decls.(IsDefinition Definition), false, DeclareDef.Global Declare.ImportDefaultBehavior in
+  let kind, opaque, scope = Decls.(IsDefinition Definition), false, Declare.Global Declare.ImportDefaultBehavior in
   let impargs, udecl = [], UState.default_univ_decl in
   let _r : GlobRef.t =
-    DeclareDef.declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ~poly ~types ~body sigma
+    Declare.declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ~poly ~types ~body sigma
   in ()
 
 let build_morphism_signature env sigma m =
@@ -1961,10 +1961,10 @@ let add_morphism_as_parameter atts m n : unit =
   let env = Global.env () in
   let evd = Evd.from_env env in
   let poly = atts.polymorphic in
-  let kind, opaque, scope = Decls.(IsAssumption Logical), false, DeclareDef.Global Declare.ImportDefaultBehavior in
+  let kind, opaque, scope = Decls.(IsAssumption Logical), false, Declare.Global Declare.ImportDefaultBehavior in
   let impargs, udecl = [], UState.default_univ_decl in
   let evd, types = build_morphism_signature env evd m in
-  let evd, pe = DeclareDef.prepare_parameter ~poly ~udecl ~types evd in
+  let evd, pe = Declare.prepare_parameter ~poly ~udecl ~types evd in
   let cst = Declare.declare_constant ~name:instance_id ~kind (Declare.ParameterEntry pe) in
   let cst = GlobRef.ConstRef cst in
   Classes.add_instance
@@ -1981,7 +1981,7 @@ let add_morphism_interactive atts m n : Lemmas.t =
   let poly = atts.polymorphic in
   let kind = Decls.(IsDefinition Instance) in
   let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
-  let hook { DeclareDef.Hook.S.dref; _ } = dref |> function
+  let hook { Declare.Hook.S.dref; _ } = dref |> function
     | GlobRef.ConstRef cst ->
       Classes.add_instance (Classes.mk_instance
                       (PropGlobal.proper_class env evd) Hints.empty_hint_info
@@ -1989,7 +1989,7 @@ let add_morphism_interactive atts m n : Lemmas.t =
       declare_projection n instance_id (GlobRef.ConstRef cst)
     | _ -> assert false
   in
-  let hook = DeclareDef.Hook.make hook in
+  let hook = Declare.Hook.make hook in
   let info = Lemmas.Info.make ~hook ~kind () in
   Flags.silently
     (fun () ->
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 9910796d9c..e6c59f446d 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -683,6 +683,111 @@ let tactic_extend plugin_name tacname ~level ?deprecation sign =
   Tacenv.register_ml_tactic ml_tactic_name @@ Array.of_list (List.map eval sign);
   Mltop.declare_cache_obj obj plugin_name
 
+type (_, 'a) ml_ty_sig =
+| MLTyNil : ('a, 'a) ml_ty_sig
+| MLTyArg : ('r, 'a) ml_ty_sig -> (Geninterp.Val.t -> 'r, 'a) ml_ty_sig
+
+let rec ml_sig_len : type r a. (r, a) ml_ty_sig -> int = function
+| MLTyNil -> 0
+| MLTyArg sign -> 1 + ml_sig_len sign
+
+let rec cast_ml : type r a. (r, a) ml_ty_sig -> r -> Geninterp.Val.t list -> a =
+  fun sign f ->
+  match sign with
+  | MLTyNil ->
+    begin function
+    | [] -> f
+    | _ :: _ -> CErrors.anomaly (str "Arity mismatch")
+    end
+  | MLTyArg sign ->
+    function
+    | [] -> CErrors.anomaly (str "Arity mismatch")
+    | arg :: args -> cast_ml sign (f arg) args
+
+let ml_tactic_extend ~plugin ~name ~local ?deprecation sign tac =
+  let open Tacexpr in
+  let tac args _ = cast_ml sign tac args in
+  let ml_tactic_name = { mltac_tactic = name; mltac_plugin = plugin } in
+  let ml = { mltac_name = ml_tactic_name; mltac_index = 0 } in
+  let len = ml_sig_len sign in
+  let args = List.init len (fun i -> Id.of_string (Printf.sprintf "arg%i" i)) in
+  let vars = List.map (fun id -> Name id) args in
+  let args = List.map (fun id -> Reference (Locus.ArgVar (CAst.make id))) args in
+  let body = Tacexpr.TacFun (vars, Tacexpr.TacML (CAst.make (ml, args))) in
+  let id = Names.Id.of_string name in
+  let obj () = Tacenv.register_ltac true local id body ?deprecation in
+  let () = Tacenv.register_ml_tactic ml_tactic_name [|tac|] in
+  Mltop.declare_cache_obj obj plugin
+
+module MLName =
+struct
+  open Tacexpr
+  type t = ml_tactic_name
+  let compare tac1 tac2 =
+    let c = String.compare tac1.mltac_tactic tac2.mltac_tactic in
+    if c = 0 then String.compare tac1.mltac_plugin tac2.mltac_plugin
+    else c
+end
+
+module MLTacMap = Map.Make(MLName)
+
+let ml_table : (Geninterp.Val.t list -> Geninterp.Val.t Ftactic.t) MLTacMap.t ref = ref MLTacMap.empty
+
+type ml_ltac_val = {
+  tacval_tac : Tacexpr.ml_tactic_name;
+  tacval_var : Id.t list;
+}
+
+let in_tacval =
+(*  This is a hack to emulate value-returning ML-implemented tactics in Ltac.
+    We use a dummy generic argument to work around the limitations of the Ltac
+    runtime. Indeed, the TacML node needs to return unit values, since it is
+    considered a "tactic" in the runtime. Changing it to allow arbitrary values
+    would require to toggle this status, and thus to make it a "value" node.
+    This would in turn create too much backwards incompatibility. Instead, we
+    piggy back on the TacGeneric node, which by construction is used to return
+    values.
+
+    The trick is to represent a n-ary application of a ML function as a generic
+    argument. We store in the node the name of the tactic and its arity, while
+    giving canonical names to the bound variables of the closure. This trick is
+    already performed in several external developments for specific calls, we
+    make it here generic. The argument should not be used for other purposes, so
+    we only export the registering functions.
+  *)
+  let wit : (Empty.t, ml_ltac_val, Geninterp.Val.t) Genarg.genarg_type =
+    Genarg.create_arg "ltac:val"
+  in
+  (* No need to internalize this ever *)
+  let intern_fun _ e = Empty.abort e in
+  let subst_fun s v = v in
+  let () = Genintern.register_intern0 wit intern_fun in
+  let () = Genintern.register_subst0 wit subst_fun in
+  (* No need to register a value tag for it via register_val0 since we will
+     never access this genarg directly. *)
+  let interp_fun ist tac =
+    let args = List.map (fun id -> Id.Map.get id ist.Geninterp.lfun) tac.tacval_var in
+    let tac = MLTacMap.get tac.tacval_tac !ml_table in
+    tac args
+  in
+  let () = Geninterp.register_interp0 wit interp_fun in
+  (fun v -> Genarg.in_gen (Genarg.Glbwit wit) v)
+
+
+let ml_val_tactic_extend ~plugin ~name ~local ?deprecation sign tac =
+  let open Tacexpr in
+  let tac args = cast_ml sign tac args in
+  let ml_tactic_name = { mltac_tactic = name; mltac_plugin = plugin } in
+  let len = ml_sig_len sign in
+  let vars = List.init len (fun i -> Id.of_string (Printf.sprintf "arg%i" i)) in
+  let body = TacGeneric (in_tacval { tacval_tac = ml_tactic_name;  tacval_var = vars }) in
+  let vars = List.map (fun id -> Name id) vars in
+  let body = Tacexpr.TacFun (vars, Tacexpr.TacArg (CAst.make body)) in
+  let id = Names.Id.of_string name in
+  let obj () = Tacenv.register_ltac true local id body ?deprecation in
+  let () = assert (not @@ MLTacMap.mem ml_tactic_name !ml_table) in
+  let () = ml_table := MLTacMap.add ml_tactic_name tac !ml_table in
+  Mltop.declare_cache_obj obj plugin
 
 (** ARGUMENT EXTEND *)
 
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index ce38431a18..6ee3ce091b 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -69,6 +69,25 @@ val print_ltacs : unit -> unit
 val print_located_tactic : Libnames.qualid -> unit
 (** Display the absolute name of a tactic. *)
 
+(** {5 Low-level registering of tactics} *)
+
+type (_, 'a) ml_ty_sig =
+| MLTyNil : ('a, 'a) ml_ty_sig
+| MLTyArg : ('r, 'a) ml_ty_sig -> (Geninterp.Val.t -> 'r, 'a) ml_ty_sig
+
+val ml_tactic_extend : plugin:string -> name:string -> local:locality_flag ->
+  ?deprecation:Deprecation.t -> ('r, unit Proofview.tactic) ml_ty_sig -> 'r -> unit
+(** Helper function to define directly an Ltac function in OCaml without any
+    associated parsing rule nor further shenanigans. The Ltac function will be
+    defined as [name] in the Coq file that loads the ML plugin where this
+    function is called. It will have the arity given by the [ml_ty_sig]
+    argument. *)
+
+val ml_val_tactic_extend : plugin:string -> name:string -> local:locality_flag ->
+  ?deprecation:Deprecation.t -> ('r, Geninterp.Val.t Ftactic.t) ml_ty_sig -> 'r -> unit
+(** Same as {!ml_tactic_extend} but the function can return an argument
+    instead. *)
+
 (** {5 TACTIC EXTEND} *)
 
 type _ ty_sig =
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index dda7f0742c..6debc7d9b9 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1895,8 +1895,7 @@ module Value = struct
     let closure = VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], tac) in
     of_tacvalue closure
 
-  (** Apply toplevel tactic values *)
-  let apply (f : value) (args: value list) =
+  let apply_expr f args =
     let fold arg (i, vars, lfun) =
       let id = Id.of_string ("x" ^ string_of_int i) in
       let x = Reference (ArgVar CAst.(make id)) in
@@ -1905,9 +1904,18 @@ module Value = struct
     let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in
     let lfun = Id.Map.add (Id.of_string "F") f lfun in
     let ist = { (default_ist ()) with lfun = lfun; } in
-    let tac = TacArg(CAst.make @@ TacCall (CAst.make (ArgVar CAst.(make @@ Id.of_string "F"),args))) in
+    ist, TacArg(CAst.make @@ TacCall (CAst.make (ArgVar CAst.(make @@ Id.of_string "F"),args)))
+
+
+  (** Apply toplevel tactic values *)
+  let apply (f : value) (args: value list) =
+    let ist, tac = apply_expr f args in
     eval_tactic_ist ist tac
 
+  let apply_val (f : value) (args: value list) =
+    let ist, tac = apply_expr f args in
+    val_interp ist tac
+
 end
 
 (* globalization + interpretation *)
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index ce34356a37..cbb17bf0fa 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -29,6 +29,7 @@ sig
   val of_closure : Geninterp.interp_sign -> glob_tactic_expr -> t
   val cast : 'a typed_abstract_argument_type -> Geninterp.Val.t -> 'a
   val apply : t -> t list -> unit Proofview.tactic
+  val apply_val : t -> t list -> t Ftactic.t
 end
 
 (** Values for interpretation *)