aboutsummaryrefslogtreecommitdiffhomepage
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
parent2de309b65b379a3c496752aa25f1cfc177644222 (diff)
parente2e23a52655fbd04a1cc659e64fb520d97d7f9db (diff)
Merge PR #8037: Export a function to apply toplevel tactic values in Tacinterp.
-rw-r--r--plugins/ltac/tacinterp.ml35
-rw-r--r--plugins/ltac/tacinterp.mli1
-rw-r--r--plugins/setoid_ring/newring.ml19
3 files changed, 28 insertions, 27 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 *)
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 8e0ca877a..a736eec5e 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -161,21 +161,6 @@ let decl_constant na univs c =
let ltac_call tac (args:glob_tactic_arg list) =
TacArg(Loc.tag @@ TacCall (Loc.tag (ArgArg(Loc.tag @@ Lazy.force tac),args)))
-(* Calling a locally bound tactic *)
-let ltac_lcall tac args =
- TacArg(Loc.tag @@ TacCall (Loc.tag (ArgVar CAst.(make @@ Id.of_string tac),args)))
-
-let ltac_apply (f : Value.t) (args: Tacinterp.Value.t 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 = { (Tacinterp.default_ist ()) with Tacinterp.lfun = lfun; } in
- Tacinterp.eval_tactic_ist ist (ltac_lcall "F" args)
-
let dummy_goal env sigma =
let (gl,_,sigma) =
Goal.V82.mk_goal sigma (named_context_val env) EConstr.mkProp Evd.Store.empty in
@@ -765,7 +750,7 @@ let ring_lookup (f : Value.t) lH rl t =
let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.ring_carrier) rl) in
let lH = carg (make_hyp_list env evdref lH) in
let ring = ltac_ring_structure e in
- Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (ring@[lH;rl]))
+ Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (ring@[lH;rl]))
with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
end
@@ -1051,6 +1036,6 @@ let field_lookup (f : Value.t) lH rl t =
let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.field_carrier) rl) in
let lH = carg (make_hyp_list env evdref lH) in
let field = ltac_field_structure e in
- Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (field@[lH;rl]))
+ Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (field@[lH;rl]))
with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
end