aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--intf/tacexpr.mli4
-rw-r--r--parsing/egramcoq.ml22
-rw-r--r--plugins/setoid_ring/newring.ml6
-rw-r--r--printing/pptactic.ml43
-rw-r--r--printing/pptacticsig.mli15
-rw-r--r--tactics/tacintern.ml6
-rw-r--r--tactics/tacinterp.ml62
-rw-r--r--tactics/tacsubst.ml6
-rw-r--r--tactics/tauto.ml42
-rw-r--r--test-suite/bugs/closed/3849.v (renamed from test-suite/bugs/opened/3849.v)2
-rw-r--r--toplevel/metasyntax.ml1
11 files changed, 76 insertions, 93 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index aa1088c9ea..6d10ef9d51 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -292,9 +292,9 @@ and 'a gen_tactic_expr =
| TacFun of 'a gen_tactic_fun_ast
| TacArg of 'a gen_tactic_arg located
(* For ML extensions *)
- | TacML of Loc.t * ml_tactic_entry * 'l generic_argument list
+ | TacML of Loc.t * ml_tactic_entry * 'a gen_tactic_arg list
(* For syntax extensions *)
- | TacAlias of Loc.t * KerName.t * (Id.t * 'l generic_argument) list
+ | TacAlias of Loc.t * KerName.t * (Id.t * 'a gen_tactic_arg) list
constraint 'a = <
term:'t;
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 84736f8aba..2bc5b0f83f 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -257,7 +257,8 @@ let add_ml_tactic_entry name prods =
let mkact i loc l : raw_tactic_expr =
let open Tacexpr in
let entry = { mltac_name = name; mltac_index = i } in
- TacML (loc, entry, List.map snd l)
+ let map (_, arg) = TacGeneric arg in
+ TacML (loc, entry, List.map map l)
in
let rules = List.map_i (fun i p -> make_rule (mkact i) p) 0 prods in
synchronize_level_positions ();
@@ -274,7 +275,24 @@ let head_is_ident tg = match tg.tacgram_prods with
let add_tactic_entry kn tg =
let entry, pos = get_tactic_entry tg.tacgram_level in
- let mkact loc l = (TacAlias (loc,kn,l):raw_tactic_expr) in
+ let mkact loc l =
+ let filter = function
+ | GramTerminal _ -> None
+ | GramNonTerminal (_, t, _, None) -> None
+ | GramNonTerminal (_, t, _, Some _) -> Some (Genarg.unquote t)
+ in
+ let types = List.map_filter filter tg.tacgram_prods in
+ let map (id, arg) t =
+ (** HACK to handle especially the tactic(...) entry *)
+ let wit = Genarg.rawwit Constrarg.wit_tactic in
+ if Genarg.argument_type_eq t (Genarg.unquote wit) then
+ (id, Tacexp (Genarg.out_gen wit arg))
+ else
+ (id, TacGeneric arg)
+ in
+ let l = List.map2 map l types in
+ (TacAlias (loc,kn,l):raw_tactic_expr)
+ in
let () =
if Int.equal tg.tacgram_level 0 && not (head_is_ident tg) then
error "Notation for simple tactic must start with an identifier."
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index d596cf6fb8..88c8465b1b 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -137,8 +137,8 @@ let closed_term_ast l =
let l = List.map (fun gr -> ArgArg(Loc.ghost,gr)) l in
TacFun([Some(Id.of_string"t")],
TacML(Loc.ghost,tacname,
- [Genarg.in_gen (Genarg.glbwit Constrarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None);
- Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Constrarg.wit_ref)) l]))
+ [TacGeneric (Genarg.in_gen (Genarg.glbwit Constrarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None));
+ TacGeneric (Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Constrarg.wit_ref)) l)]))
(*
let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term"
*)
@@ -228,7 +228,7 @@ let exec_tactic env evd n f args =
(** Build the getter *)
let lid = List.init n (fun i -> Id.of_string("x"^string_of_int i)) in
let n = Genarg.in_gen (Genarg.glbwit Stdarg.wit_int) n in
- let get_res = TacML (Loc.ghost, get_res, [n]) in
+ let get_res = TacML (Loc.ghost, get_res, [TacGeneric n]) in
let getter = Tacexp (TacFun (List.map (fun id -> Some id) lid, get_res)) in
(** Evaluate the whole result *)
let gl = dummy_goal env evd in
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 6e051a1fc0..4cb7e9fb38 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -371,10 +371,11 @@ module Make
in
pr_sequence (fun x -> x) l
- let pr_extend_gen pr_gen lev { mltac_name = s; mltac_index = i } l =
+ let pr_extend_gen check pr_gen lev { mltac_name = s; mltac_index = i } l =
try
let pp_rules = Hashtbl.find prtac_tab s in
let pp = pp_rules.(i) in
+ let () = if not (List.for_all2eq check pp.pptac_args l) then raise Not_found in
let (lev', pl) = pp.pptac_prods in
let p = pr_tacarg_using_rule pr_gen (pl,l) in
if lev' > lev then surround p else p
@@ -389,28 +390,35 @@ module Make
in
str "<" ++ name ++ str ">" ++ args
- let pr_alias_gen pr_gen lev key l =
+ let pr_alias_gen check pr_gen lev key l =
try
let pp = KNmap.find key !prnotation_tab in
let (lev', pl) = pp.pptac_prods in
+ let () = if not (List.for_all2eq check pp.pptac_args l) then raise Not_found in
let p = pr_tacarg_using_rule pr_gen (pl, l) in
if lev' > lev then surround p else p
with Not_found ->
KerName.print key ++ spc() ++ pr_sequence pr_gen l ++ str" (* Generic printer *)"
+ let check_type t arg = match arg with
+ | TacGeneric arg -> argument_type_eq t (genarg_tag arg)
+ | _ -> false
+
+ let unwrap_gen f = function TacGeneric x -> f x | _ -> assert false
+
let pr_raw_extend_rec prc prlc prtac prpat =
- pr_extend_gen (pr_raw_generic_rec prc prlc prtac prpat pr_reference)
+ pr_extend_gen check_type (unwrap_gen (pr_raw_generic_rec prc prlc prtac prpat pr_reference))
let pr_glob_extend_rec prc prlc prtac prpat =
- pr_extend_gen (pr_glb_generic_rec prc prlc prtac prpat)
+ pr_extend_gen check_type (unwrap_gen (pr_glb_generic_rec prc prlc prtac prpat))
let pr_extend_rec prc prlc prtac prpat =
- pr_extend_gen (pr_top_generic_rec prc prlc prtac prpat)
+ pr_extend_gen check_type (unwrap_gen (pr_top_generic_rec prc prlc prtac prpat))
let pr_raw_alias prc prlc prtac prpat =
- pr_alias_gen (pr_raw_generic_rec prc prlc prtac prpat pr_reference)
+ pr_alias_gen check_type (unwrap_gen (pr_raw_generic_rec prc prlc prtac prpat pr_reference))
let pr_glob_alias prc prlc prtac prpat =
- pr_alias_gen (pr_glb_generic_rec prc prlc prtac prpat)
+ pr_alias_gen check_type (unwrap_gen (pr_glb_generic_rec prc prlc prtac prpat))
let pr_alias prc prlc prtac prpat =
- pr_alias_gen (pr_top_generic_rec prc prlc prtac prpat)
+ pr_alias_gen check_type (unwrap_gen (pr_top_generic_rec prc prlc prtac prpat))
(**********************************************************************)
(* The tactic printer *)
@@ -716,8 +724,8 @@ module Make
pr_reference : 'ref -> std_ppcmds;
pr_name : 'nam -> std_ppcmds;
pr_generic : 'lev generic_argument -> std_ppcmds;
- pr_extend : int -> ml_tactic_entry -> 'lev generic_argument list -> std_ppcmds;
- pr_alias : int -> KerName.t -> 'lev generic_argument list -> std_ppcmds;
+ pr_extend : int -> ml_tactic_entry -> 'a gen_tactic_arg list -> std_ppcmds;
+ pr_alias : int -> KerName.t -> 'a gen_tactic_arg list -> std_ppcmds;
}
constraint 'a = <
@@ -1352,9 +1360,18 @@ module Make
(pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env))
(pr_glob_tactic_level env) (pr_pat_and_constr_expr (pr_glob_constr_env env))
- let pr_extend env = pr_extend_rec
- (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty)
- (pr_glob_tactic_level env) pr_constr_pattern
+ let check_val_type t arg =
+ let t = Genarg.val_tag (Obj.magic t) in (** FIXME *)
+ let Val.Dyn (t', _) = arg in
+ match Genarg.Val.eq t t' with
+ | None -> false
+ | Some _ -> true
+
+ let pr_alias pr lev key args =
+ pr_alias_gen check_val_type pr lev key args
+
+ let pr_extend pr lev ml args =
+ pr_extend_gen check_val_type pr lev ml args
let pr_tactic env = pr_tactic_level env ltop
diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli
index d154e0b663..01f240f6b8 100644
--- a/printing/pptacticsig.mli
+++ b/printing/pptacticsig.mli
@@ -40,19 +40,16 @@ module type Pp = sig
val pr_top_generic : env -> tlevel generic_argument -> std_ppcmds
val pr_raw_extend: env -> int ->
- ml_tactic_entry -> raw_generic_argument list -> std_ppcmds
+ ml_tactic_entry -> raw_tactic_arg list -> std_ppcmds
val pr_glob_extend: env -> int ->
- ml_tactic_entry -> glob_generic_argument list -> std_ppcmds
+ ml_tactic_entry -> glob_tactic_arg list -> std_ppcmds
- val pr_extend : env -> int ->
- ml_tactic_entry -> typed_generic_argument list -> std_ppcmds
+ val pr_extend :
+ (Val.t -> std_ppcmds) -> int -> ml_tactic_entry -> Val.t list -> std_ppcmds
- val pr_extend_gen :
- ('a -> std_ppcmds) -> int -> ml_tactic_entry -> 'a list -> std_ppcmds
-
- val pr_alias_gen : ('a -> std_ppcmds) ->
- int -> Names.KerName.t -> 'a list -> std_ppcmds
+ val pr_alias : (Val.t -> std_ppcmds) ->
+ int -> Names.KerName.t -> Val.t list -> std_ppcmds
val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 08d2d21a3f..93d64f686d 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -656,11 +656,11 @@ and intern_tactic_seq onlytac ist = function
(* For extensions *)
| TacAlias (loc,s,l) ->
- let l = List.map (fun (id,a) -> (id,intern_genarg ist a)) l in
+ let l = List.map (fun (id,a) -> (id,intern_tacarg !strict_check false ist a)) l in
ist.ltacvars, TacAlias (loc,s,l)
| TacML (loc,opn,l) ->
let _ignore = Tacenv.interp_ml_tactic opn in
- ist.ltacvars, TacML (adjust_loc loc,opn,List.map (intern_genarg ist) l)
+ ist.ltacvars, TacML (adjust_loc loc,opn,List.map (intern_tacarg !strict_check false ist) l)
and intern_tactic_as_arg loc onlytac ist a =
match intern_tacarg !strict_check onlytac ist a with
@@ -700,7 +700,7 @@ and intern_tacarg strict onlytac ist = function
| TacNumgoals -> TacNumgoals
| Tacexp t -> Tacexp (intern_tactic onlytac ist t)
| TacGeneric arg ->
- let (_, arg) = Genintern.generic_intern ist arg in
+ let arg = intern_genarg ist arg in
TacGeneric arg
(* Reads the rules of a Match Context or a Match *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 5e5b2be243..1596406c9a 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -156,12 +156,7 @@ module Value = struct
end
-let print_top_val env arg v =
- let unpacker wit cst =
- try val_cast (topwit wit) v; mt ()
- with CastError _ -> mt ()
- in
- unpack { unpacker } arg
+let print_top_val env v = mt () (** FIXME *)
let dloc = Loc.ghost
@@ -1244,51 +1239,9 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
(* For extensions *)
| TacAlias (loc,s,l) ->
let body = Tacenv.interp_alias s in
- let rec f x = match genarg_tag x with
- | ConstrArgType
- | ListArgType ConstrArgType
- | OptArgType _ | PairArgType _ -> (** generic handler *)
- interp_genarg ist x
- | _ as tag -> (** Special treatment. TODO: use generic handler *)
- Ftactic.nf_enter begin fun gl ->
- let sigma = Tacmach.New.project gl in
- let env = Proofview.Goal.env gl in
- match tag with
- | IdentArgType ->
- Ftactic.return (value_of_ident (interp_ident ist env sigma
- (Genarg.out_gen (glbwit wit_ident) x)))
- | VarArgType ->
- Ftactic.return (Value.of_constr (mk_hyp_value ist env sigma (Genarg.out_gen (glbwit wit_var) x)))
- | ListArgType VarArgType ->
- let wit = glbwit (wit_list wit_var) in
- let ans = List.map (mk_hyp_value ist env sigma) (Genarg.out_gen wit x) in
- Ftactic.return (Value.of_list (val_tag wit_constr) ans)
- | ListArgType IdentArgType ->
- let wit = glbwit (wit_list wit_ident) in
- let mk_ident x = intro_pattern_of_ident (interp_ident ist env sigma x) in
- let ans = List.map mk_ident (Genarg.out_gen wit x) in
- Ftactic.return (Value.of_list (val_tag wit_intro_pattern) ans)
- | ListArgType t ->
- let open Ftactic in
- list_unpack { list_unpacker = fun wit l ->
- let map x = f (Genarg.in_gen (glbwit wit) x) in
- Ftactic.List.map map (glb l) >>= fun l ->
- let l = CList.map (fun x -> Value.cast (topwit wit) x) l in
- Ftactic.return (Value.of_list (val_tag wit) l)
- } x
- | ExtraArgType _ ->
- (** Special treatment of tactics *)
- if Genarg.has_type x (glbwit wit_tactic) then
- let tac = Genarg.out_gen (glbwit wit_tactic) x in
- val_interp ist tac
- else
- Geninterp.generic_interp ist x
- | _ -> assert false
- end
- in
let (>>=) = Ftactic.bind in
let interp_vars =
- Ftactic.List.map (fun (x,v) -> f v >>= fun v -> Ftactic.return (x,v)) l
+ Ftactic.List.map (fun (x,v) -> interp_tacarg ist v >>= fun v -> Ftactic.return (x,v)) l
in
let addvar (x, v) accu = Id.Map.add x v accu in
let tac l =
@@ -1302,8 +1255,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
in
let tac =
Ftactic.with_env interp_vars >>= fun (env, lr) ->
- let l = List.map2 (fun (_, g) (_, t) -> print_top_val env g t) l lr in
- let name () = Pptactic.pr_alias_gen (fun x -> x) 0 s l in
+ let name () = Pptactic.pr_alias (fun v -> print_top_val env v) 0 s (List.map snd lr) in
Proofview.Trace.name_tactic name (tac lr)
(* spiwack: this use of name_tactic is not robust to a
change of implementation of [Ftactic]. In such a situation,
@@ -1316,10 +1268,9 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
let trace = push_trace (loc,LtacMLCall tac) ist in
let ist = { ist with extra = TacStore.set ist.extra f_trace trace; } in
let tac = Tacenv.interp_ml_tactic opn in
- let args = Ftactic.List.map_right (fun a -> interp_genarg ist a) l in
+ let args = Ftactic.List.map_right (fun a -> interp_tacarg ist a) l in
let tac args =
- let l = List.map2 (print_top_val ()) l args in
- let name () = Pptactic.pr_extend_gen (fun x -> x) 0 opn l in
+ let name () = Pptactic.pr_extend (fun v -> print_top_val () v) 0 opn args in
Proofview.Trace.name_tactic name (catch_error_tac trace (tac args ist))
in
Ftactic.run args tac
@@ -1355,8 +1306,7 @@ and interp_ltac_reference loc' mustbetac ist r : Val.t Ftactic.t =
and interp_tacarg ist arg : Val.t Ftactic.t =
match arg with
- | TacGeneric arg ->
- Geninterp.generic_interp ist arg
+ | TacGeneric arg -> interp_genarg ist arg
| Reference r -> interp_ltac_reference dloc false ist r
| ConstrMayEval c ->
Ftactic.enter begin fun gl ->
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 2132e9a573..45b2d317c2 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -245,8 +245,8 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with
(* For extensions *)
| TacAlias (_,s,l) ->
let s = subst_kn subst s in
- TacAlias (dloc,s,List.map (fun (id,a) -> (id,subst_genarg subst a)) l)
- | TacML (_loc,opn,l) -> TacML (dloc,opn,List.map (subst_genarg subst) l)
+ TacAlias (dloc,s,List.map (fun (id,a) -> (id,subst_tacarg subst a)) l)
+ | TacML (_loc,opn,l) -> TacML (dloc,opn,List.map (subst_tacarg subst) l)
and subst_tactic_fun subst (var,body) = (var,subst_tactic subst body)
@@ -261,7 +261,7 @@ and subst_tacarg subst = function
| TacPretype c -> TacPretype (subst_glob_constr subst c)
| TacNumgoals -> TacNumgoals
| Tacexp t -> Tacexp (subst_tactic subst t)
- | TacGeneric arg -> TacGeneric (Genintern.generic_substitute subst arg)
+ | TacGeneric arg -> TacGeneric (subst_genarg subst arg)
(* Reads the rules of a Match Context or a Match *)
and subst_match_rule subst = function
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index d84f471163..f0805f7d08 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -210,7 +210,7 @@ let constructor i =
(** Take care of the index: this is the second entry in constructor. *)
let name = { Tacexpr.mltac_name = name; mltac_index = 1 } in
let i = in_gen (rawwit Constrarg.wit_int_or_var) (Misctypes.ArgArg i) in
- Tacexpr.TacML (Loc.ghost, name, [i])
+ Tacexpr.TacML (Loc.ghost, name, [TacGeneric i])
let is_disj _ ist =
let flags = assoc_flags ist in
diff --git a/test-suite/bugs/opened/3849.v b/test-suite/bugs/closed/3849.v
index 5290054a06..a8dc3af9cf 100644
--- a/test-suite/bugs/opened/3849.v
+++ b/test-suite/bugs/closed/3849.v
@@ -5,4 +5,4 @@ Tactic Notation "bar" hyp_list(hs) := foo hs.
Goal True.
do 5 pose proof 0 as ?n0.
foo n1 n2.
-Fail bar n3 n4.
+bar n3 n4.
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 7714cc8108..0f96c2b4af 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -171,6 +171,7 @@ let extend_atomic_tactic name entries =
| None -> ()
| Some args ->
let open Tacexpr in
+ let args = List.map (fun a -> TacGeneric a) args in
let entry = { mltac_name = name; mltac_index = i } in
let body = TacML (Loc.ghost, entry, args) in
Tacenv.register_ltac false false (Names.Id.of_string id) body
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 06:48:56 +0000