diff options
| author | Pierre-Marie Pédrot | 2020-04-09 23:29:58 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-07 00:22:11 +0200 |
| commit | c39b622a8d8b32f335ee7dfe56ad27f9db7caaee (patch) | |
| tree | 6b8bd1218e3c31d1c85dd1d89a8243f61d6157de /plugins/ltac | |
| parent | f694d42400593d7ef3ad6c2812395f941cc4f5ca (diff) | |
Export API to recover values out of Ltac application.
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 14 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.mli | 1 |
2 files changed, 12 insertions, 3 deletions
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index dda7f0742c..6debc7d9b9 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1895,8 +1895,7 @@ module Value = struct 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 apply_expr f args = 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 @@ -1905,9 +1904,18 @@ module Value = struct 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(CAst.make @@ TacCall (CAst.make (ArgVar CAst.(make @@ Id.of_string "F"),args))) in + ist, TacArg(CAst.make @@ TacCall (CAst.make (ArgVar CAst.(make @@ Id.of_string "F"),args))) + + + (** Apply toplevel tactic values *) + let apply (f : value) (args: value list) = + let ist, tac = apply_expr f args in eval_tactic_ist ist tac + let apply_val (f : value) (args: value list) = + let ist, tac = apply_expr f args in + val_interp ist tac + end (* globalization + interpretation *) diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index ce34356a37..cbb17bf0fa 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -29,6 +29,7 @@ sig 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 + val apply_val : t -> t list -> t Ftactic.t end (** Values for interpretation *) |