diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-07-20 11:33:40 +0200 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-07-20 11:33:40 +0200 |
commit | d8cd9ba6d56d32eb8aa383bca9198a18517e82d3 (patch) | |
tree | dc6670607c7831c5a6b80da427b1f299ffd0f2df /plugins/ltac | |
parent | 2de309b65b379a3c496752aa25f1cfc177644222 (diff) | |
parent | e2e23a52655fbd04a1cc659e64fb520d97d7f9db (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.ml | 35 | ||||
-rw-r--r-- | plugins/ltac/tacinterp.mli | 1 |
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 *) |