Export a function to apply toplevel tactic values in Tacinterp.

This is a function that keeps beeing asked or reimplemented. It doesn't hurt
adding it to the Ltac API.

2 files changed, 26 insertions, 10 deletions

diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index d9ac96d89..6d94e3f86 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -141,16 +141,6 @@ let extract_trace ist = match TacStore.get ist.extra f_trace with
 | None -> []
 | Some l -> l
 
-module Value = struct
-
-  include Taccoerce.Value
-
-  let of_closure ist tac =
-    let closure = VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], tac) in
-    of_tacvalue closure
-
-end
-
 let print_top_val env v = Pptactic.pr_value Pptactic.ltop v
 
 let catching_error call_trace fail (e, info) =
@@ -1860,6 +1850,31 @@ let eval_tactic_ist ist t =
   Proofview.tclLIFT db_initialize <*>
   interp_tactic ist t
 
+(** FFI *)
+
+module Value = struct
+
+  include Taccoerce.Value
+
+  let of_closure ist tac =
+    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 fold arg (i, vars, lfun) =
+      let id = Id.of_string ("x" ^ string_of_int i) in
+      let x = Reference (ArgVar CAst.(make id)) in
+      (succ i, x :: vars, Id.Map.add id arg lfun)
+    in
+    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(Loc.tag @@ TacCall (Loc.tag (ArgVar CAst.(make @@ Id.of_string "F"),args))) in
+    eval_tactic_ist ist tac
+
+end
+
 (* globalization + interpretation *)
 
 
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index fd2d96bd6..f9883e444 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -28,6 +28,7 @@ sig
   val to_list : t -> t list option
   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
 end
 
 (** Values for interpretation *)