aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2018-07-20 11:33:40 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2018-07-20 11:33:40 +0200
commitd8cd9ba6d56d32eb8aa383bca9198a18517e82d3 (patch)
treedc6670607c7831c5a6b80da427b1f299ffd0f2df /plugins/ltac
parent2de309b65b379a3c496752aa25f1cfc177644222 (diff)
parente2e23a52655fbd04a1cc659e64fb520d97d7f9db (diff)
Merge PR #8037: Export a function to apply toplevel tactic values in Tacinterp.
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/tacinterp.ml35
-rw-r--r--plugins/ltac/tacinterp.mli1
2 files changed, 26 insertions, 10 deletions
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 77b5b06d4..a0446bd6a 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 *)