diff options
| -rw-r--r-- | plugins/ltac/tacentries.ml | 105 | ||||
| -rw-r--r-- | plugins/ltac/tacentries.mli | 19 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 14 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.mli | 1 |
4 files changed, 136 insertions, 3 deletions
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 9910796d9c..e6c59f446d 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -683,6 +683,111 @@ let tactic_extend plugin_name tacname ~level ?deprecation sign = Tacenv.register_ml_tactic ml_tactic_name @@ Array.of_list (List.map eval sign); Mltop.declare_cache_obj obj plugin_name +type (_, 'a) ml_ty_sig = +| MLTyNil : ('a, 'a) ml_ty_sig +| MLTyArg : ('r, 'a) ml_ty_sig -> (Geninterp.Val.t -> 'r, 'a) ml_ty_sig + +let rec ml_sig_len : type r a. (r, a) ml_ty_sig -> int = function +| MLTyNil -> 0 +| MLTyArg sign -> 1 + ml_sig_len sign + +let rec cast_ml : type r a. (r, a) ml_ty_sig -> r -> Geninterp.Val.t list -> a = + fun sign f -> + match sign with + | MLTyNil -> + begin function + | [] -> f + | _ :: _ -> CErrors.anomaly (str "Arity mismatch") + end + | MLTyArg sign -> + function + | [] -> CErrors.anomaly (str "Arity mismatch") + | arg :: args -> cast_ml sign (f arg) args + +let ml_tactic_extend ~plugin ~name ~local ?deprecation sign tac = + let open Tacexpr in + let tac args _ = cast_ml sign tac args in + let ml_tactic_name = { mltac_tactic = name; mltac_plugin = plugin } in + let ml = { mltac_name = ml_tactic_name; mltac_index = 0 } in + let len = ml_sig_len sign in + let args = List.init len (fun i -> Id.of_string (Printf.sprintf "arg%i" i)) in + let vars = List.map (fun id -> Name id) args in + let args = List.map (fun id -> Reference (Locus.ArgVar (CAst.make id))) args in + let body = Tacexpr.TacFun (vars, Tacexpr.TacML (CAst.make (ml, args))) in + let id = Names.Id.of_string name in + let obj () = Tacenv.register_ltac true local id body ?deprecation in + let () = Tacenv.register_ml_tactic ml_tactic_name [|tac|] in + Mltop.declare_cache_obj obj plugin + +module MLName = +struct + open Tacexpr + type t = ml_tactic_name + let compare tac1 tac2 = + let c = String.compare tac1.mltac_tactic tac2.mltac_tactic in + if c = 0 then String.compare tac1.mltac_plugin tac2.mltac_plugin + else c +end + +module MLTacMap = Map.Make(MLName) + +let ml_table : (Geninterp.Val.t list -> Geninterp.Val.t Ftactic.t) MLTacMap.t ref = ref MLTacMap.empty + +type ml_ltac_val = { + tacval_tac : Tacexpr.ml_tactic_name; + tacval_var : Id.t list; +} + +let in_tacval = +(* This is a hack to emulate value-returning ML-implemented tactics in Ltac. + We use a dummy generic argument to work around the limitations of the Ltac + runtime. Indeed, the TacML node needs to return unit values, since it is + considered a "tactic" in the runtime. Changing it to allow arbitrary values + would require to toggle this status, and thus to make it a "value" node. + This would in turn create too much backwards incompatibility. Instead, we + piggy back on the TacGeneric node, which by construction is used to return + values. + + The trick is to represent a n-ary application of a ML function as a generic + argument. We store in the node the name of the tactic and its arity, while + giving canonical names to the bound variables of the closure. This trick is + already performed in several external developments for specific calls, we + make it here generic. The argument should not be used for other purposes, so + we only export the registering functions. + *) + let wit : (Empty.t, ml_ltac_val, Geninterp.Val.t) Genarg.genarg_type = + Genarg.create_arg "ltac:val" + in + (* No need to internalize this ever *) + let intern_fun _ e = Empty.abort e in + let subst_fun s v = v in + let () = Genintern.register_intern0 wit intern_fun in + let () = Genintern.register_subst0 wit subst_fun in + (* No need to register a value tag for it via register_val0 since we will + never access this genarg directly. *) + let interp_fun ist tac = + let args = List.map (fun id -> Id.Map.get id ist.Geninterp.lfun) tac.tacval_var in + let tac = MLTacMap.get tac.tacval_tac !ml_table in + tac args + in + let () = Geninterp.register_interp0 wit interp_fun in + (fun v -> Genarg.in_gen (Genarg.Glbwit wit) v) + + +let ml_val_tactic_extend ~plugin ~name ~local ?deprecation sign tac = + let open Tacexpr in + let tac args = cast_ml sign tac args in + let ml_tactic_name = { mltac_tactic = name; mltac_plugin = plugin } in + let len = ml_sig_len sign in + let vars = List.init len (fun i -> Id.of_string (Printf.sprintf "arg%i" i)) in + let body = TacGeneric (in_tacval { tacval_tac = ml_tactic_name; tacval_var = vars }) in + let vars = List.map (fun id -> Name id) vars in + let body = Tacexpr.TacFun (vars, Tacexpr.TacArg (CAst.make body)) in + let id = Names.Id.of_string name in + let obj () = Tacenv.register_ltac true local id body ?deprecation in + let () = assert (not @@ MLTacMap.mem ml_tactic_name !ml_table) in + let () = ml_table := MLTacMap.add ml_tactic_name tac !ml_table in + Mltop.declare_cache_obj obj plugin (** ARGUMENT EXTEND *) diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index ce38431a18..6ee3ce091b 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -69,6 +69,25 @@ val print_ltacs : unit -> unit val print_located_tactic : Libnames.qualid -> unit (** Display the absolute name of a tactic. *) +(** {5 Low-level registering of tactics} *) + +type (_, 'a) ml_ty_sig = +| MLTyNil : ('a, 'a) ml_ty_sig +| MLTyArg : ('r, 'a) ml_ty_sig -> (Geninterp.Val.t -> 'r, 'a) ml_ty_sig + +val ml_tactic_extend : plugin:string -> name:string -> local:locality_flag -> + ?deprecation:Deprecation.t -> ('r, unit Proofview.tactic) ml_ty_sig -> 'r -> unit +(** Helper function to define directly an Ltac function in OCaml without any + associated parsing rule nor further shenanigans. The Ltac function will be + defined as [name] in the Coq file that loads the ML plugin where this + function is called. It will have the arity given by the [ml_ty_sig] + argument. *) + +val ml_val_tactic_extend : plugin:string -> name:string -> local:locality_flag -> + ?deprecation:Deprecation.t -> ('r, Geninterp.Val.t Ftactic.t) ml_ty_sig -> 'r -> unit +(** Same as {!ml_tactic_extend} but the function can return an argument + instead. *) + (** {5 TACTIC EXTEND} *) type _ ty_sig = 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 *) |