From e2e23a52655fbd04a1cc659e64fb520d97d7f9db Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 10 Jul 2018 13:04:17 +0200 Subject: 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. --- plugins/ltac/tacinterp.ml | 35 +++++++++++++++++++++++++---------- plugins/ltac/tacinterp.mli | 1 + plugins/setoid_ring/newring.ml | 19 ++----------------- 3 files changed, 28 insertions(+), 27 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 *) 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 -- cgit v1.2.3