aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/genarg.ml42
-rw-r--r--interp/genarg.mli6
-rw-r--r--parsing/argextend.ml471
-rw-r--r--parsing/extrawit.ml12
-rw-r--r--parsing/tacextend.ml445
-rw-r--r--plugins/decl_mode/g_decl_mode.ml42
-rw-r--r--plugins/firstorder/g_ground.ml42
-rw-r--r--plugins/funind/g_indfun.ml42
-rw-r--r--tactics/extraargs.ml48
-rw-r--r--tactics/extraargs.mli2
-rw-r--r--tactics/rewrite.ml46
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2732.v19
-rw-r--r--toplevel/g_obligations.ml42
13 files changed, 168 insertions, 51 deletions
diff --git a/interp/genarg.ml b/interp/genarg.ml
index b4f87d96b3..0d640640b3 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -64,23 +64,10 @@ type 'a with_ebindings = 'a * open_constr bindings
type 'a generic_argument = argument_type * Obj.t
-let dyntab = ref ([] : string list)
-
type rlevel
type glevel
type tlevel
-type ('a,'b) abstract_argument_type = argument_type
-
-let create_arg s =
- if List.mem s !dyntab then
- anomaly ("Genarg.create: already declared generic argument " ^ s);
- dyntab := s :: !dyntab;
- let t = ExtraArgType s in
- (t,t,t)
-
-let exists_argtype s = List.mem s !dyntab
-
type intro_pattern_expr =
| IntroOrAndPattern of or_and_intro_pattern_expr
| IntroWildcard
@@ -260,3 +247,32 @@ let unquote x = x
type an_arg_of_this_type = Obj.t
let in_generic t x = (t, Obj.repr x)
+
+let dyntab = ref ([] : (string * glevel generic_argument option) list)
+
+type ('a,'b) abstract_argument_type = argument_type
+
+let create_arg v s =
+ if List.mem_assoc s !dyntab then
+ anomaly ("Genarg.create: already declared generic argument " ^ s);
+ let t = ExtraArgType s in
+ dyntab := (s,Option.map (in_gen t) v) :: !dyntab;
+ (t,t,t)
+
+let exists_argtype s = List.mem_assoc s !dyntab
+
+let default_empty_argtype_value s = List.assoc s !dyntab
+
+let default_empty_value t =
+ let rec aux = function
+ | List0ArgType _ -> Some (in_gen t [])
+ | OptArgType _ -> Some (in_gen t None)
+ | PairArgType(t1,t2) ->
+ (match aux t1, aux t2 with
+ | Some (_,v1), Some (_,v2) -> Some (in_gen t (v1,v2))
+ | _ -> None)
+ | ExtraArgType s -> default_empty_argtype_value s
+ | _ -> None in
+ match aux t with
+ | Some v -> Some (out_gen t v)
+ | None -> None
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 9c47c691a9..43cd73aedb 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -257,7 +257,8 @@ val app_pair :
(** create a new generic type of argument: force to associate
unique ML types at each of the three levels *)
-val create_arg : string ->
+val create_arg : 'globa option ->
+ string ->
('a,tlevel) abstract_argument_type
* ('globa,glevel) abstract_argument_type
* ('rawa,rlevel) abstract_argument_type
@@ -299,7 +300,6 @@ val in_gen :
val out_gen :
('a,'co) abstract_argument_type -> 'co generic_argument -> 'a
-
(** [in_generic] is used in combination with camlp4 [Gramext.action] magic
[in_generic: !l:type, !a:argument_type -> |a|_l -> 'l generic_argument]
@@ -313,3 +313,5 @@ type an_arg_of_this_type
val in_generic :
argument_type -> an_arg_of_this_type -> 'co generic_argument
+
+val default_empty_value : ('a,glevel) abstract_argument_type -> 'a option
diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index 788e664e29..d890be142b 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -107,6 +107,72 @@ let rec make_wit loc = function
value wit = $lid:"wit_"^s$;
end in WIT.wit >>
+let possibly_empty_subentries prods =
+ try
+ Some (List.fold_right (fun e l -> match e with
+ | GramNonTerminal(_,(List0ArgType _| OptArgType _),_,_) ->
+ (* This parses epsilon *) l
+ | GramNonTerminal(_,ExtraArgType s,_,_) ->
+ (* This parses epsilon if s parses it *) s::l
+ | GramTerminal _ | GramNonTerminal(_,_,_,_) ->
+ (* This does not parse epsilon *)
+ (* Not meaningful to have Pair in prods nor to have empty *)
+ (* entries in Lst1 productions *)
+ raise Exit) prods [])
+ with Exit -> None
+
+let has_extraarg =
+ List.exists (function GramNonTerminal(_,ExtraArgType _,_,_) -> true | _ -> false)
+
+let statically_known_possibly_empty (prods,_) =
+ List.for_all (function
+ | GramNonTerminal(_,(OptArgType _|List0ArgType _|ExtraArgType _),_,_) ->
+ (* Opt and List0 parses the empty string and for ExtraArg we don't know *)
+ (* (we'll have to test dynamically *)
+ true
+ | _ ->
+ (* This consumes a token for sure *) false)
+ prods
+
+let possibly_empty_subentries loc (prods,act) =
+ let bind_name p v e = match p with
+ | None -> e
+ | Some id ->
+ let s = Names.string_of_id id in <:expr< let $lid:s$ = $v$ in $e$ >> in
+ let rec aux = function
+ | [] -> <:expr< $act$ >>
+ | GramNonTerminal(_,OptArgType _,_,p) :: tl ->
+ bind_name p <:expr< None >> (aux tl)
+ | GramNonTerminal(_,List0ArgType _,_,p) :: tl ->
+ bind_name p <:expr< [] >> (aux tl)
+ | GramNonTerminal(_,(ExtraArgType _ as t),_,p) :: tl ->
+ (* We check at runtime if extraarg s parses "epsilon" *)
+ let s = match p with None -> "_" | Some id -> Names.string_of_id id in
+ <:expr< let $lid:s$ = match Genarg.default_empty_value $make_globwit loc t$ with
+ [ None -> raise Exit
+ | Some v -> v ] in $aux tl$ >>
+ | _ -> assert false (* already filtered out *) in
+ if has_extraarg prods then
+ (* Needs a dynamic check *)
+ (true, <:expr< try Some $aux prods$ with Exit -> None >>)
+ else
+ (* Static optimisation *)
+ (false, aux prods)
+
+let make_possibly_empty_subentries loc cl =
+ let cl = List.filter statically_known_possibly_empty cl in
+ if cl = [] then
+ <:expr< None >>
+ else
+ let rec aux = function
+ | (true, e) :: l ->
+ <:expr< match $e$ with [ Some v -> Some v | None -> $aux l$ ] >>
+ | (false, e) :: _ ->
+ <:expr< Some $e$ >>
+ | [] ->
+ <:expr< None >> in
+ aux (List.map (possibly_empty_subentries loc) cl)
+
let make_act loc act pil =
let rec make = function
| [] -> <:expr< Pcoq.Gram.action (fun loc -> ($act$ : 'a)) >>
@@ -160,10 +226,11 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
let rawwit = <:expr< $lid:"rawwit_"^s$ >> in
let globwit = <:expr< $lid:"globwit_"^s$ >> in
let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in
+ let default_value = <:expr< $make_possibly_empty_subentries loc cl$ >> in
declare_str_items loc
[ <:str_item<
value ($lid:"wit_"^s$, $lid:"globwit_"^s$, $lid:"rawwit_"^s$) =
- Genarg.create_arg $se$ >>;
+ Genarg.create_arg $default_value$ $se$>>;
<:str_item<
value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$ >>;
<:str_item< do {
@@ -195,7 +262,7 @@ let declare_vernac_argument loc s pr cl =
[ <:str_item<
value (($lid:"wit_"^s$:Genarg.abstract_argument_type unit Genarg.tlevel),
($lid:"globwit_"^s$:Genarg.abstract_argument_type unit Genarg.glevel),
- $lid:"rawwit_"^s$) = Genarg.create_arg $se$ >>;
+ $lid:"rawwit_"^s$) = Genarg.create_arg None $se$ >>;
<:str_item<
value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$ >>;
<:str_item< do {
diff --git a/parsing/extrawit.ml b/parsing/extrawit.ml
index cc5b58ee70..a660f910e0 100644
--- a/parsing/extrawit.ml
+++ b/parsing/extrawit.ml
@@ -16,12 +16,12 @@ open Genarg
let tactic_main_level = 5
-let (wit_tactic0,globwit_tactic0,rawwit_tactic0) = create_arg "tactic0"
-let (wit_tactic1,globwit_tactic1,rawwit_tactic1) = create_arg "tactic1"
-let (wit_tactic2,globwit_tactic2,rawwit_tactic2) = create_arg "tactic2"
-let (wit_tactic3,globwit_tactic3,rawwit_tactic3) = create_arg "tactic3"
-let (wit_tactic4,globwit_tactic4,rawwit_tactic4) = create_arg "tactic4"
-let (wit_tactic5,globwit_tactic5,rawwit_tactic5) = create_arg "tactic5"
+let (wit_tactic0,globwit_tactic0,rawwit_tactic0) = create_arg None "tactic0"
+let (wit_tactic1,globwit_tactic1,rawwit_tactic1) = create_arg None "tactic1"
+let (wit_tactic2,globwit_tactic2,rawwit_tactic2) = create_arg None "tactic2"
+let (wit_tactic3,globwit_tactic3,rawwit_tactic3) = create_arg None "tactic3"
+let (wit_tactic4,globwit_tactic4,rawwit_tactic4) = create_arg None "tactic4"
+let (wit_tactic5,globwit_tactic5,rawwit_tactic5) = create_arg None "tactic5"
let wit_tactic = function
| 0 -> wit_tactic0
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index 838c771c6b..b7364efc13 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -120,19 +120,27 @@ let make_one_printing_rule se (pt,e) =
let make_printing_rule se = mlexpr_of_list (make_one_printing_rule se)
-let rec contains_epsilon = function
- | List0ArgType _ -> true
- | List1ArgType t -> contains_epsilon t
- | OptArgType _ -> true
- | PairArgType(t1,t2) -> contains_epsilon t1 && contains_epsilon t2
- | ExtraArgType("hintbases") -> true
- | _ -> false
-let is_atomic = function
- | GramTerminal s :: l when
- List.for_all (function
- GramTerminal _ -> false
- | GramNonTerminal(_,t,_,_) -> contains_epsilon t) l
- -> [s]
+let possibly_empty_subentries loc s prods =
+ try
+ let l = List.map (function
+ | GramNonTerminal(_,(List0ArgType _|OptArgType _|ExtraArgType _ as t),_,_)->
+ (* This possibly parses epsilon *)
+ let globwit = make_globwit loc t in
+ <:expr< match Genarg.default_empty_value $globwit$ with
+ [ None -> failwith ""
+ | Some v -> Genarg.in_gen $globwit$ v ] >>
+ | GramTerminal _ | GramNonTerminal(_,_,_,_) ->
+ (* This does not parse epsilon (this Exit is static time) *)
+ raise Exit) prods in
+ if has_extraarg prods then
+ [s, <:expr< try Some $mlexpr_of_list (fun x -> x) l$
+ with Failure "" -> None >>]
+ else
+ [s, <:expr< Some $mlexpr_of_list (fun x -> x) l$ >>]
+ with Exit -> []
+
+let possibly_atomic loc = function
+ | GramTerminal s :: l -> possibly_empty_subentries loc s l
| _ -> []
let declare_tactic loc s cl =
@@ -152,17 +160,20 @@ let declare_tactic loc s cl =
in
let hidden = if List.length cl = 1 then List.map hide_tac cl else [] in
let atomic_tactics =
- mlexpr_of_list mlexpr_of_string
- (List.flatten (List.map (fun (al,_) -> is_atomic al) cl)) in
+ mlexpr_of_list (mlexpr_of_pair mlexpr_of_string (fun x -> x))
+ (List.flatten (List.map (fun (al,_) -> possibly_atomic loc al) cl)) in
declare_str_items loc
(hidden @
[ <:str_item< do {
try
let _=Tacinterp.add_tactic $se$ $make_fun_clauses loc s cl$ in
List.iter
- (fun s -> Tacinterp.add_primitive_tactic s
+ (fun (s,l) -> match l with
+ [ Some l ->
+ Tacinterp.add_primitive_tactic s
(Tacexpr.TacAtom($default_loc$,
- Tacexpr.TacExtend($default_loc$,s,[]))))
+ Tacexpr.TacExtend($default_loc$,$se$,l)))
+ | None -> () ])
$atomic_tactics$
with e -> Pp.pp (Errors.print e);
Egrammar.extend_tactic_grammar $se$ $gl$;
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 88e62e46df..b5a2ac82eb 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -103,7 +103,7 @@ let proof_instr = Gram.entry_create "proofmode:instr"
(* [Genarg.create_arg] creates a new embedding into Genarg. *)
let (wit_proof_instr,globwit_proof_instr,rawwit_proof_instr) =
- Genarg.create_arg "proof_instr"
+ Genarg.create_arg None "proof_instr"
let _ = Tacinterp.add_interp_genarg "proof_instr"
begin
begin fun e x -> (* declares the globalisation function *)
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index f5b16e43fe..48bb87214a 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -134,8 +134,6 @@ TACTIC EXTEND firstorder
| [ "firstorder" tactic_opt(t) firstorder_using(l)
"with" ne_preident_list(l') ] ->
[ gen_ground_tac true (Option.map eval_tactic t) l l' ]
-| [ "firstorder" tactic_opt(t) ] ->
- [ gen_ground_tac true (Option.map eval_tactic t) [] [] ]
END
TACTIC EXTEND gintuition
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index f330f9ff92..e8fec0dd84 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -154,7 +154,7 @@ type 'a function_rec_definition_loc_argtype = ((Vernacexpr.fixpoint_expr * Verna
let (wit_function_rec_definition_loc : Genarg.tlevel function_rec_definition_loc_argtype),
(globwit_function_rec_definition_loc : Genarg.glevel function_rec_definition_loc_argtype),
(rawwit_function_rec_definition_loc : Genarg.rlevel function_rec_definition_loc_argtype) =
- Genarg.create_arg "function_rec_definition_loc"
+ Genarg.create_arg None "function_rec_definition_loc"
VERNAC COMMAND EXTEND Function
["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")] ->
[
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index 0496d758b0..72e18ab140 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -287,13 +287,13 @@ let glob_in_arg_hyp_to_clause = gen_in_arg_hyp_to_clause (fun x -> x)
(* spiwack argument for the commands of the retroknowledge *)
let (wit_r_nat_field, globwit_r_nat_field, rawwit_r_nat_field) =
- Genarg.create_arg "r_nat_field"
+ Genarg.create_arg None "r_nat_field"
let (wit_r_n_field, globwit_r_n_field, rawwit_r_n_field) =
- Genarg.create_arg "r_n_field"
+ Genarg.create_arg None "r_n_field"
let (wit_r_int31_field, globwit_r_int31_field, rawwit_r_int31_field) =
- Genarg.create_arg "r_int31_field"
+ Genarg.create_arg None "r_int31_field"
let (wit_r_field, globwit_r_field, rawwit_r_field) =
- Genarg.create_arg "r_field"
+ Genarg.create_arg None "r_field"
(* spiwack: the print functions are incomplete, but I don't know what they are
used for *)
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index a682af04f8..35344c99c2 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -15,6 +15,7 @@ open Termops
open Glob_term
val rawwit_orient : bool raw_abstract_argument_type
+val globwit_orient : bool glob_abstract_argument_type
val wit_orient : bool typed_abstract_argument_type
val orient : bool Pcoq.Gram.entry
val pr_orient : bool -> Pp.std_ppcmds
@@ -39,6 +40,7 @@ val hloc : loc_place Pcoq.Gram.entry
val pr_hloc : loc_place -> Pp.std_ppcmds
val in_arg_hyp: (Names.identifier Pp.located list option * bool) Pcoq.Gram.entry
+val globwit_in_arg_hyp : (Names.identifier Pp.located list option * bool) glob_abstract_argument_type
val rawwit_in_arg_hyp : (Names.identifier Pp.located list option * bool) raw_abstract_argument_type
val wit_in_arg_hyp : (Names.identifier list option * bool) typed_abstract_argument_type
val raw_in_arg_hyp_to_clause : (Names.identifier Pp.located list option * bool) -> Tacticals.clause
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index b8bd166b9b..ba95038187 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1366,7 +1366,7 @@ ARGUMENT EXTEND glob_constr_with_bindings
END
let _ =
- (Genarg.create_arg "strategy" :
+ (Genarg.create_arg None "strategy" :
((strategy, Genarg.tlevel) Genarg.abstract_argument_type *
(strategy, Genarg.glevel) Genarg.abstract_argument_type *
(strategy, Genarg.rlevel) Genarg.abstract_argument_type))
@@ -1426,6 +1426,8 @@ let clsubstitute o c =
| Some id when is_tac id -> tclIDTAC
| _ -> cl_rewrite_clause c o all_occurrences cl)
+open Extraargs
+
TACTIC EXTEND substitute
| [ "substitute" orient(o) glob_constr_with_bindings(c) ] -> [ clsubstitute o c ]
END
@@ -1537,7 +1539,7 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans =
type 'a binders_argtype = (local_binder list, 'a) Genarg.abstract_argument_type
let _, _, rawwit_binders =
- (Genarg.create_arg "binders" :
+ (Genarg.create_arg None "binders" :
Genarg.tlevel binders_argtype *
Genarg.glevel binders_argtype *
Genarg.rlevel binders_argtype)
diff --git a/test-suite/bugs/closed/shouldsucceed/2732.v b/test-suite/bugs/closed/shouldsucceed/2732.v
new file mode 100644
index 0000000000..f22a8cccc5
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2732.v
@@ -0,0 +1,19 @@
+(* Check correct behavior of add_primitive_tactic in TACEXTEND *)
+
+(* Added also the case of eauto and congruence *)
+
+Ltac thus H := solve [H].
+
+Lemma test: forall n : nat, n <= n.
+Proof.
+ intro.
+ thus firstorder.
+ Undo.
+ thus eauto.
+Qed.
+
+Lemma test2: false = true -> False.
+Proof.
+ intro.
+ thus congruence.
+Qed.
diff --git a/toplevel/g_obligations.ml4 b/toplevel/g_obligations.ml4
index 7d155ab41a..9840814b1f 100644
--- a/toplevel/g_obligations.ml4
+++ b/toplevel/g_obligations.ml4
@@ -61,7 +61,7 @@ type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_a
let (wit_withtac : Genarg.tlevel withtac_argtype),
(globwit_withtac : Genarg.glevel withtac_argtype),
(rawwit_withtac : Genarg.rlevel withtac_argtype) =
- Genarg.create_arg "withtac"
+ Genarg.create_arg None "withtac"
open Obligations
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-29 14:32:39 +0000