aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/extraargs.mlg54
-rw-r--r--plugins/ltac/extraargs.mli4
-rw-r--r--plugins/ltac/extratactics.mlg8
-rw-r--r--plugins/ltac/g_ltac.mlg2
-rw-r--r--plugins/ltac/pptactic.ml2
-rw-r--r--plugins/ltac/rewrite.ml12
-rw-r--r--plugins/ltac/taccoerce.ml7
-rw-r--r--plugins/ltac/tacentries.ml105
-rw-r--r--plugins/ltac/tacentries.mli19
-rw-r--r--plugins/ltac/tacintern.ml7
-rw-r--r--plugins/ltac/tacinterp.ml15
-rw-r--r--plugins/ltac/tacinterp.mli1
-rw-r--r--plugins/ltac/tacsubst.ml1
13 files changed, 227 insertions, 10 deletions
diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg
index c4731e5c34..eb53fd45d0 100644
--- a/plugins/ltac/extraargs.mlg
+++ b/plugins/ltac/extraargs.mlg
@@ -31,6 +31,8 @@ let create_generic_quotation name e wit =
let () = create_generic_quotation "integer" Pcoq.Prim.integer Stdarg.wit_int
let () = create_generic_quotation "string" Pcoq.Prim.string Stdarg.wit_string
+let () = create_generic_quotation "smart_global" Pcoq.Prim.smart_global Stdarg.wit_smart_global
+
let () = create_generic_quotation "ident" Pcoq.Prim.ident Stdarg.wit_ident
let () = create_generic_quotation "reference" Pcoq.Prim.reference Stdarg.wit_ref
let () = create_generic_quotation "uconstr" Pcoq.Constr.lconstr Stdarg.wit_uconstr
@@ -342,3 +344,55 @@ let pr_lpar_id_colon _ _ _ _ = mt ()
ARGUMENT EXTEND test_lpar_id_colon TYPED AS unit PRINTED BY { pr_lpar_id_colon }
| [ local_test_lpar_id_colon(x) ] -> { () }
END
+
+{
+
+(* Work around a limitation of the macro system *)
+let strategy_level0 = Pcoq.Prim.strategy_level
+
+let pr_strategy _ _ _ v = Conv_oracle.pr_level v
+
+}
+
+ARGUMENT EXTEND strategy_level PRINTED BY { pr_strategy }
+| [ strategy_level0(n) ] -> { n }
+END
+
+{
+
+let intern_strategy ist v = match v with
+| ArgVar id -> ArgVar (Tacintern.intern_hyp ist id)
+| ArgArg v -> ArgArg v
+
+let subst_strategy _ v = v
+
+let interp_strategy ist gl = function
+| ArgArg n -> gl.Evd.sigma, n
+| ArgVar { CAst.v = id; CAst.loc } ->
+ let v =
+ try Id.Map.find id ist.lfun
+ with Not_found ->
+ CErrors.user_err ?loc
+ (str "Unbound variable " ++ Id.print id ++ str".")
+ in
+ let v =
+ try Tacinterp.Value.cast (Genarg.topwit wit_strategy_level) v
+ with CErrors.UserError _ -> Taccoerce.error_ltac_variable ?loc id None v "a strategy_level"
+ in
+ gl.Evd.sigma, v
+
+let pr_loc_strategy _ _ _ v = Pputils.pr_or_var Conv_oracle.pr_level v
+
+}
+
+ARGUMENT EXTEND strategy_level_or_var
+ TYPED AS strategy_level
+ PRINTED BY { pr_strategy }
+ INTERPRETED BY { interp_strategy }
+ GLOBALIZED BY { intern_strategy }
+ SUBSTITUTED BY { subst_strategy }
+ RAW_PRINTED BY { pr_loc_strategy }
+ GLOB_PRINTED BY { pr_loc_strategy }
+| [ strategy_level(n) ] -> { ArgArg n }
+| [ identref(id) ] -> { ArgVar id }
+END
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index fbdb7c0032..e52bf55f71 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -78,3 +78,7 @@ val wit_in_clause :
(lident Locus.clause_expr,
lident Locus.clause_expr,
Id.t Locus.clause_expr) Genarg.genarg_type
+
+val wit_strategy_level : Conv_oracle.level Genarg.uniform_genarg_type
+
+val wit_strategy_level_or_var : (Conv_oracle.level Locus.or_var, Conv_oracle.level Locus.or_var, Conv_oracle.level) Genarg.genarg_type
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 0bad3cbe5b..ffb597d4cb 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -1119,3 +1119,11 @@ let tclOPTIMIZE_HEAP =
TACTIC EXTEND optimize_heap
| [ "optimize_heap" ] -> { tclOPTIMIZE_HEAP }
END
+
+(** Tactic analogous to [Strategy] vernacular *)
+
+TACTIC EXTEND with_strategy
+| [ "with_strategy" strategy_level_or_var(v) "[" ne_smart_global_list(q) "]" tactic3(tac) ] -> {
+ with_set_strategy [(v, q)] (Tacinterp.tactic_of_value ist tac)
+}
+END
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 5baa23b3e9..aef5f645f4 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -342,7 +342,7 @@ GRAMMAR EXTEND Gram
hint:
[ [ IDENT "Extern"; n = natural; c = OPT Constr.constr_pattern ; "=>";
tac = Pltac.tactic ->
- { ComHints.HintsExtern (n,c, in_tac tac) } ] ]
+ { Vernacexpr.HintsExtern (n,c, in_tac tac) } ] ]
;
operconstr: LEVEL "0"
[ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" ->
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 09f1fc371a..d74e981c6d 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -1325,6 +1325,8 @@ let () =
register_basic_print0 wit_int_or_var (pr_or_var int) (pr_or_var int) int;
register_basic_print0 wit_ref
pr_qualid (pr_or_var (pr_located pr_global)) pr_global;
+ register_basic_print0 wit_smart_global
+ (pr_or_by_notation pr_qualid) (pr_or_var (pr_located pr_global)) pr_global;
register_basic_print0 wit_ident pr_id pr_id pr_id;
register_basic_print0 wit_var pr_lident pr_lident pr_id;
register_print0 wit_intropattern pr_raw_intro_pattern pr_glob_intro_pattern pr_intro_pattern_env [@warning "-3"];
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 3834b21a14..3b8fb48eb0 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1894,10 +1894,10 @@ let declare_projection name instance_id r =
in it_mkProd_or_LetIn ccl ctx
in
let types = Some (it_mkProd_or_LetIn typ ctx) in
- let kind, opaque, scope = Decls.(IsDefinition Definition), false, DeclareDef.Global Declare.ImportDefaultBehavior in
+ let kind, opaque, scope = Decls.(IsDefinition Definition), false, Declare.Global Declare.ImportDefaultBehavior in
let impargs, udecl = [], UState.default_univ_decl in
let _r : GlobRef.t =
- DeclareDef.declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ~poly ~types ~body sigma
+ Declare.declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ~poly ~types ~body sigma
in ()
let build_morphism_signature env sigma m =
@@ -1961,10 +1961,10 @@ let add_morphism_as_parameter atts m n : unit =
let env = Global.env () in
let evd = Evd.from_env env in
let poly = atts.polymorphic in
- let kind, opaque, scope = Decls.(IsAssumption Logical), false, DeclareDef.Global Declare.ImportDefaultBehavior in
+ let kind, opaque, scope = Decls.(IsAssumption Logical), false, Declare.Global Declare.ImportDefaultBehavior in
let impargs, udecl = [], UState.default_univ_decl in
let evd, types = build_morphism_signature env evd m in
- let evd, pe = DeclareDef.prepare_parameter ~poly ~udecl ~types evd in
+ let evd, pe = Declare.prepare_parameter ~poly ~udecl ~types evd in
let cst = Declare.declare_constant ~name:instance_id ~kind (Declare.ParameterEntry pe) in
let cst = GlobRef.ConstRef cst in
Classes.add_instance
@@ -1981,7 +1981,7 @@ let add_morphism_interactive atts m n : Lemmas.t =
let poly = atts.polymorphic in
let kind = Decls.(IsDefinition Instance) in
let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
- let hook { DeclareDef.Hook.S.dref; _ } = dref |> function
+ let hook { Declare.Hook.S.dref; _ } = dref |> function
| GlobRef.ConstRef cst ->
Classes.add_instance (Classes.mk_instance
(PropGlobal.proper_class env evd) Hints.empty_hint_info
@@ -1989,7 +1989,7 @@ let add_morphism_interactive atts m n : Lemmas.t =
declare_projection n instance_id (GlobRef.ConstRef cst)
| _ -> assert false
in
- let hook = DeclareDef.Hook.make hook in
+ let hook = Declare.Hook.make hook in
let info = Lemmas.Info.make ~hook ~kind () in
Flags.silently
(fun () ->
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 04d85ed390..91d26519b8 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -293,6 +293,13 @@ let coerce_to_evaluable_ref env sigma v =
| VarRef var -> EvalVarRef var
| ConstRef c -> EvalConstRef c
| IndRef _ | ConstructRef _ -> fail ()
+ else if has_type v (topwit wit_smart_global) then
+ let open GlobRef in
+ let r = out_gen (topwit wit_smart_global) v in
+ match r with
+ | VarRef var -> EvalVarRef var
+ | ConstRef c -> EvalConstRef c
+ | IndRef _ | ConstructRef _ -> fail ()
else
match Value.to_constr v with
| Some c when isConst sigma c -> EvalConstRef (fst (destConst sigma c))
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/tacintern.ml b/plugins/ltac/tacintern.ml
index 597c3fdaac..929fd5e132 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -305,6 +305,12 @@ let intern_evaluable_reference_or_by_notation ist = function
(Notation.interp_notation_as_global_reference ?loc
GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc)
+let intern_smart_global ist = function
+ | {v=AN r} -> intern_global_reference ist r
+ | {v=ByNotation (ntn,sc);loc} ->
+ ArgArg (loc, (Notation.interp_notation_as_global_reference ?loc
+ GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc))
+
(* Globalize a reduction expression *)
let intern_evaluable ist r =
let f ist r =
@@ -813,6 +819,7 @@ let intern_ltac ist tac =
let () =
Genintern.register_intern0 wit_int_or_var (lift intern_int_or_var);
+ Genintern.register_intern0 wit_smart_global (lift intern_smart_global);
Genintern.register_intern0 wit_ref (lift intern_global_reference);
Genintern.register_intern0 wit_pre_ident (fun ist c -> (ist,c));
Genintern.register_intern0 wit_ident intern_ident';
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index a8bb97c774..5ae0b2efd7 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 *)
@@ -2014,6 +2022,7 @@ let interp_pre_ident ist env sigma s =
let () =
register_interp0 wit_int_or_var (fun ist n -> Ftactic.return (interp_int_or_var ist n));
+ register_interp0 wit_smart_global (lift interp_reference);
register_interp0 wit_ref (lift interp_reference);
register_interp0 wit_pre_ident (lift interp_pre_ident);
register_interp0 wit_ident (lift interp_ident);
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 *)
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index 600c30b403..ed298b7e66 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -280,6 +280,7 @@ and subst_genarg subst (GenArg (Glbwit wit, x)) =
let () =
Genintern.register_subst0 wit_int_or_var (fun _ v -> v);
Genintern.register_subst0 wit_ref subst_global_reference;
+ Genintern.register_subst0 wit_smart_global subst_global_reference;
Genintern.register_subst0 wit_pre_ident (fun _ v -> v);
Genintern.register_subst0 wit_ident (fun _ v -> v);
Genintern.register_subst0 wit_var (fun _ v -> v);
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 19:05:32 +0000