aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--grammar/argextend.ml42
-rw-r--r--ltac/extraargs.ml44
-rw-r--r--ltac/tacentries.ml228
-rw-r--r--ltac/tacentries.mli8
-rw-r--r--parsing/egramcoq.ml153
-rw-r--r--parsing/egramcoq.mli33
-rw-r--r--parsing/pcoq.ml110
-rw-r--r--parsing/pcoq.mli8
-rw-r--r--test-suite/bugs/closed/1850.v4
9 files changed, 283 insertions, 267 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index f9f3ee988e..adfbd8cfde 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -140,7 +140,7 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
<:str_item< do {
Pptactic.declare_extra_genarg_pprule
$wit$ $lid:rawpr$ $lid:globpr$ $lid:pr$;
- Egramcoq.create_ltac_quotation $se$
+ Tacentries.create_ltac_quotation $se$
(fun (loc, v) -> Tacexpr.TacGeneric (Genarg.in_gen (Genarg.rawwit $wit$) v))
($lid:s$, None)
} >> ]
diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4
index d33ec91f9d..4d3507cbc4 100644
--- a/ltac/extraargs.ml4
+++ b/ltac/extraargs.ml4
@@ -25,7 +25,7 @@ open Locus
let create_generic_quotation name e wit =
let inject (loc, v) = Tacexpr.TacGeneric (Genarg.in_gen (Genarg.rawwit wit) v) in
- Egramcoq.create_ltac_quotation name inject (e, None)
+ Tacentries.create_ltac_quotation name inject (e, None)
let () = create_generic_quotation "integer" Pcoq.Prim.integer Stdarg.wit_int
let () = create_generic_quotation "string" Pcoq.Prim.string Stdarg.wit_string
@@ -38,7 +38,7 @@ let () = create_generic_quotation "ipattern" Pcoq.Tactic.simple_intropattern Con
let () = create_generic_quotation "open_constr" Pcoq.Constr.lconstr Constrarg.wit_open_constr
let () =
let inject (loc, v) = Tacexpr.Tacexp v in
- Egramcoq.create_ltac_quotation "ltac" inject (Pcoq.Tactic.tactic_expr, Some 5)
+ Tacentries.create_ltac_quotation "ltac" inject (Pcoq.Tactic.tactic_expr, Some 5)
(* Rewriting orientation *)
diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml
index 711cd8d9d0..99c2213e19 100644
--- a/ltac/tacentries.ml
+++ b/ltac/tacentries.ml
@@ -11,6 +11,7 @@ open Errors
open Util
open Names
open Libobject
+open Genarg
open Pcoq
open Egramml
open Egramcoq
@@ -19,6 +20,196 @@ open Libnames
open Nameops
(**********************************************************************)
+(* Interpret entry names of the form "ne_constr_list" as entry keys *)
+
+let coincide s pat off =
+ let len = String.length pat in
+ let break = ref true in
+ let i = ref 0 in
+ while !break && !i < len do
+ let c = Char.code s.[off + !i] in
+ let d = Char.code pat.[!i] in
+ break := Int.equal c d;
+ incr i
+ done;
+ !break
+
+let atactic n =
+ let open Extend in
+ if n = 5 then Aentry (name_of_entry Tactic.binder_tactic)
+ else Aentryl (name_of_entry Tactic.tactic_expr, n)
+
+type entry_name = EntryName :
+ 'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, 'a) Extend.symbol -> entry_name
+
+let try_get_entry u s =
+ let open Extend in
+ (** Order the effects: get_entry can raise Not_found *)
+ let TypedEntry (typ, e) = get_entry u s in
+ EntryName (typ, Aentry (name_of_entry e))
+
+(** Quite ad-hoc *)
+let get_tacentry n m =
+ let open Extend in
+ let check_lvl n =
+ Int.equal m n
+ && not (Int.equal m 5) (* Because tactic5 is at binder_tactic *)
+ && not (Int.equal m 0) (* Because tactic0 is at simple_tactic *)
+ in
+ if check_lvl n then EntryName (rawwit Constrarg.wit_tactic, Aself)
+ else if check_lvl (n + 1) then EntryName (rawwit Constrarg.wit_tactic, Anext)
+ else EntryName (rawwit Constrarg.wit_tactic, atactic n)
+
+let rec parse_user_entry s sep =
+ let open Extend in
+ let l = String.length s in
+ if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then
+ let entry = parse_user_entry (String.sub s 3 (l-8)) "" in
+ Ulist1 entry
+ else if l > 12 && coincide s "ne_" 0 &&
+ coincide s "_list_sep" (l-9) then
+ let entry = parse_user_entry (String.sub s 3 (l-12)) "" in
+ Ulist1sep (entry, sep)
+ else if l > 5 && coincide s "_list" (l-5) then
+ let entry = parse_user_entry (String.sub s 0 (l-5)) "" in
+ Ulist0 entry
+ else if l > 9 && coincide s "_list_sep" (l-9) then
+ let entry = parse_user_entry (String.sub s 0 (l-9)) "" in
+ Ulist0sep (entry, sep)
+ else if l > 4 && coincide s "_opt" (l-4) then
+ let entry = parse_user_entry (String.sub s 0 (l-4)) "" in
+ Uopt entry
+ else if l > 5 && coincide s "_mods" (l-5) then
+ let entry = parse_user_entry (String.sub s 0 (l-1)) "" in
+ Umodifiers entry
+ else if Int.equal l 7 && coincide s "tactic" 0 && '5' >= s.[6] && s.[6] >= '0' then
+ let n = Char.code s.[6] - 48 in
+ Uentryl ("tactic", n)
+ else
+ let s = match s with "hyp" -> "var" | _ -> s in
+ Uentry s
+
+let arg_list = function Rawwit t -> Rawwit (ListArg t)
+let arg_opt = function Rawwit t -> Rawwit (OptArg t)
+
+let interp_entry_name up_level s sep =
+ let open Extend in
+ let rec eval = function
+ | Ulist1 e ->
+ let EntryName (t, g) = eval e in
+ EntryName (arg_list t, Alist1 g)
+ | Ulist1sep (e, sep) ->
+ let EntryName (t, g) = eval e in
+ EntryName (arg_list t, Alist1sep (g, sep))
+ | Ulist0 e ->
+ let EntryName (t, g) = eval e in
+ EntryName (arg_list t, Alist0 g)
+ | Ulist0sep (e, sep) ->
+ let EntryName (t, g) = eval e in
+ EntryName (arg_list t, Alist0sep (g, sep))
+ | Uopt e ->
+ let EntryName (t, g) = eval e in
+ EntryName (arg_opt t, Aopt g)
+ | Umodifiers e ->
+ let EntryName (t, g) = eval e in
+ EntryName (arg_list t, Amodifiers g)
+ | Uentry s ->
+ begin
+ try try_get_entry uprim s with Not_found ->
+ try try_get_entry uconstr s with Not_found ->
+ try try_get_entry utactic s with Not_found ->
+ error ("Unknown entry "^s^".")
+ end
+ | Uentryl (s, n) ->
+ (** FIXME: do better someday *)
+ assert (String.equal s "tactic");
+ get_tacentry n up_level
+ in
+ eval (parse_user_entry s sep)
+
+(**********************************************************************)
+(** Grammar declaration for Tactic Notation (Coq level) *)
+
+let get_tactic_entry n =
+ if Int.equal n 0 then
+ Tactic.simple_tactic, None
+ else if Int.equal n 5 then
+ Tactic.binder_tactic, None
+ else if 1<=n && n<5 then
+ Tactic.tactic_expr, Some (Extend.Level (string_of_int n))
+ else
+ error ("Invalid Tactic Notation level: "^(string_of_int n)^".")
+
+(**********************************************************************)
+(** State of the grammar extensions *)
+
+type tactic_grammar = {
+ tacgram_level : int;
+ tacgram_prods : Tacexpr.raw_tactic_expr grammar_prod_item list;
+}
+
+(** ML Tactic grammar extensions *)
+
+let add_ml_tactic_entry (name, prods) =
+ let entry = Tactic.simple_tactic in
+ let mkact i loc l : Tacexpr.raw_tactic_expr =
+ let open Tacexpr in
+ let entry = { mltac_name = name; mltac_index = i } in
+ 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 ();
+ grammar_extend entry None (None, [(None, None, List.rev rules)]);
+ 1
+
+(* Declaration of the tactic grammar rule *)
+
+let head_is_ident tg = match tg.tacgram_prods with
+| GramTerminal _::_ -> true
+| _ -> false
+
+(** Tactic grammar extensions *)
+
+let add_tactic_entry (kn, tg) =
+ let open Tacexpr in
+ let entry, pos = get_tactic_entry tg.tacgram_level in
+ let mkact loc l =
+ let filter = function
+ | GramTerminal _ -> None
+ | GramNonTerminal (_, t, _) -> Some (Genarg.unquote t)
+ in
+ let types = List.map_filter filter tg.tacgram_prods in
+ let map 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
+ Tacexp (Genarg.out_gen wit arg)
+ else
+ 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."
+ in
+ let rules = make_rule mkact tg.tacgram_prods in
+ synchronize_level_positions ();
+ grammar_extend entry None (pos, [(None, None, List.rev [rules])]);
+ 1
+
+let tactic_grammar =
+ create_grammar_command "TacticGrammar" add_tactic_entry
+
+let ml_tactic_grammar =
+ create_grammar_command "MLTacticGrammar" add_ml_tactic_entry
+
+let extend_tactic_grammar kn ntn = extend_grammar tactic_grammar (kn, ntn)
+let extend_ml_tactic_grammar n ntn = extend_grammar ml_tactic_grammar (n, ntn)
+
+(**********************************************************************)
(* Tactic Notation *)
let interp_prod_item lev = function
@@ -63,13 +254,13 @@ let cache_tactic_notation (_, tobj) =
let key = tobj.tacobj_key in
let () = check_key key in
Tacenv.register_alias key tobj.tacobj_body;
- Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram;
+ extend_tactic_grammar key tobj.tacobj_tacgram;
Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp
let open_tactic_notation i (_, tobj) =
let key = tobj.tacobj_key in
if Int.equal i 1 && not tobj.tacobj_local then
- Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram
+ extend_tactic_grammar key tobj.tacobj_tacgram
let load_tactic_notation i (_, tobj) =
let key = tobj.tacobj_key in
@@ -78,7 +269,7 @@ let load_tactic_notation i (_, tobj) =
Tacenv.register_alias key tobj.tacobj_body;
Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp;
if Int.equal i 1 && not tobj.tacobj_local then
- Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram
+ extend_tactic_grammar key tobj.tacobj_tacgram
let subst_tactic_notation (subst, tobj) =
let (ids, body) = tobj.tacobj_body in
@@ -188,6 +379,37 @@ let add_ml_tactic_notation name prods =
Lib.add_anonymous_leaf (inMLTacticGrammar obj);
extend_atomic_tactic name prods
+(**********************************************************************)
+(** Ltac quotations *)
+
+let ltac_quotations = ref String.Set.empty
+
+let create_ltac_quotation name cast (e, l) =
+ let open Extend in
+ let () =
+ if String.Set.mem name !ltac_quotations then
+ failwith ("Ltac quotation " ^ name ^ " already registered")
+ in
+ let () = ltac_quotations := String.Set.add name !ltac_quotations in
+ let entry = match l with
+ | None -> Aentry (name_of_entry e)
+ | Some l -> Aentryl (name_of_entry e, l)
+ in
+(* let level = Some "1" in *)
+ let level = None in
+ let assoc = None in
+ let rule =
+ Next (Next (Next (Next (Next (Stop,
+ Atoken (Lexer.terminal name)),
+ Atoken (Lexer.terminal ":")),
+ Atoken (Lexer.terminal "(")),
+ entry),
+ Atoken (Lexer.terminal ")"))
+ in
+ let action _ v _ _ _ loc = cast (loc, v) in
+ let gram = (level, assoc, [Rule (rule, action)]) in
+ Pcoq.grammar_extend Tactic.tactic_arg None (None, [gram])
+
(** Command *)
diff --git a/ltac/tacentries.mli b/ltac/tacentries.mli
index 3cf0bc5cc9..b60d8f478e 100644
--- a/ltac/tacentries.mli
+++ b/ltac/tacentries.mli
@@ -19,3 +19,11 @@ val add_ml_tactic_notation : ml_tactic_name ->
Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list list -> unit
val register_ltac : bool -> Vernacexpr.tacdef_body list -> unit
+
+(** {5 Adding tactic quotations} *)
+
+val create_ltac_quotation : string ->
+ ('grm Loc.located -> raw_tactic_arg) -> ('grm Pcoq.Gram.entry * int option) -> unit
+(** [create_ltac_quotation name f e] adds a quotation rule to Ltac, that is,
+ Ltac grammar now accepts arguments of the form ["name" ":" "(" <e> ")"], and
+ generates an argument using [f] on the entry parsed by [e]. *)
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 8c4930806e..f0c12ab8ef 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -217,115 +217,48 @@ let extend_constr_pat_notation ng =
let ext = ETConstr (level, ()), ng.notgram_assoc in
extend_constr e ext (make_cases_pattern_action mkact) true ng.notgram_prods
-let extend_constr_notation ng =
+let extend_constr_notation (_, ng) =
(* Add the notation in constr *)
let nb = extend_constr_constr_notation ng in
(* Add the notation in cases_pattern *)
let nb' = extend_constr_pat_notation ng in
nb + nb'
-(**********************************************************************)
-(** Grammar declaration for Tactic Notation (Coq level) *)
-
-let get_tactic_entry n =
- if Int.equal n 0 then
- Tactic.simple_tactic, None
- else if Int.equal n 5 then
- Tactic.binder_tactic, None
- else if 1<=n && n<5 then
- Tactic.tactic_expr, Some (Extend.Level (string_of_int n))
- else
- error ("Invalid Tactic Notation level: "^(string_of_int n)^".")
+module GrammarCommand = Dyn.Make(struct end)
+module GrammarInterp = struct type 'a t = 'a -> int end
+module GrammarInterpMap = GrammarCommand.Map(GrammarInterp)
-(**********************************************************************)
-(** State of the grammar extensions *)
+let grammar_interp = ref GrammarInterpMap.empty
-type tactic_grammar = {
- tacgram_level : int;
- tacgram_prods : Tacexpr.raw_tactic_expr grammar_prod_item list;
-}
+let (grammar_state : (int * GrammarCommand.t) list ref) = ref []
-type all_grammar_command =
- | Notation of Notation.level * notation_grammar
- | TacticGrammar of KerName.t * tactic_grammar
- | MLTacticGrammar of ml_tactic_name * Tacexpr.raw_tactic_expr grammar_prod_item list list
+type 'a grammar_command = 'a GrammarCommand.tag
-(** ML Tactic grammar extensions *)
+let create_grammar_command name interp : _ grammar_command =
+ let obj = GrammarCommand.create name in
+ let () = grammar_interp := GrammarInterpMap.add obj interp !grammar_interp in
+ obj
-let add_ml_tactic_entry name prods =
- let entry = Tactic.simple_tactic in
- let mkact i loc l : raw_tactic_expr =
- let open Tacexpr in
- let entry = { mltac_name = name; mltac_index = i } in
- 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 ();
- grammar_extend entry None (None, [(None, None, List.rev rules)]);
- 1
-
-(* Declaration of the tactic grammar rule *)
-
-let head_is_ident tg = match tg.tacgram_prods with
-| GramTerminal _::_ -> true
-| _ -> false
-
-(** Tactic grammar extensions *)
-
-let add_tactic_entry kn tg =
- let entry, pos = get_tactic_entry tg.tacgram_level in
- let mkact loc l =
- let filter = function
- | GramTerminal _ -> None
- | GramNonTerminal (_, t, _) -> Some (Genarg.unquote t)
- in
- let types = List.map_filter filter tg.tacgram_prods in
- let map 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
- Tacexp (Genarg.out_gen wit arg)
- else
- 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."
- in
- let rules = make_rule mkact tg.tacgram_prods in
- synchronize_level_positions ();
- grammar_extend entry None (pos, [(None, None, List.rev [rules])]);
- 1
-
-let (grammar_state : (int * all_grammar_command) list ref) = ref []
-
-let extend_grammar gram =
- let nb = match gram with
- | Notation (_,a) -> extend_constr_notation a
- | TacticGrammar (kn, g) -> add_tactic_entry kn g
- | MLTacticGrammar (name, pr) -> add_ml_tactic_entry name pr
- in
- grammar_state := (nb,gram) :: !grammar_state
+let extend_grammar tag g =
+ let nb = GrammarInterpMap.find tag !grammar_interp g in
+ grammar_state := (nb, GrammarCommand.Dyn (tag, g)) :: !grammar_state
-let extend_constr_grammar pr ntn =
- extend_grammar (Notation (pr, ntn))
+let extend_dyn_grammar (GrammarCommand.Dyn (tag, g)) = extend_grammar tag g
-let extend_tactic_grammar kn ntn =
- extend_grammar (TacticGrammar (kn, ntn))
+let constr_grammar : (Notation.level * notation_grammar) GrammarCommand.tag =
+ create_grammar_command "Notation" extend_constr_notation
-let extend_ml_tactic_grammar name ntn =
- extend_grammar (MLTacticGrammar (name, ntn))
+let extend_constr_grammar pr ntn = extend_grammar constr_grammar (pr, ntn)
let recover_constr_grammar ntn prec =
- let filter = function
- | _, Notation (prec', ng) when
- Notation.level_eq prec prec' &&
- String.equal ntn ng.notgram_notation -> Some ng
- | _ -> None
+ let filter (_, gram) : notation_grammar option = match gram with
+ | GrammarCommand.Dyn (tag, obj) ->
+ match GrammarCommand.eq tag constr_grammar with
+ | None -> None
+ | Some Refl ->
+ let (prec', ng) = obj in
+ if Notation.level_eq prec prec' && String.equal ntn ng.notgram_notation then Some ng
+ else None
in
match List.map_filter filter !grammar_state with
| [x] -> x
@@ -334,7 +267,7 @@ let recover_constr_grammar ntn prec =
(* Summary functions: the state of the lexer is included in that of the parser.
Because the grammar affects the set of keywords when adding or removing
grammar rules. *)
-type frozen_t = (int * all_grammar_command) list * Lexer.frozen_t
+type frozen_t = (int * GrammarCommand.t) list * Lexer.frozen_t
let freeze _ : frozen_t = (!grammar_state, Lexer.freeze ())
@@ -353,7 +286,7 @@ let unfreeze (grams, lex) =
remove_levels n;
grammar_state := common;
Lexer.unfreeze lex;
- List.iter extend_grammar (List.rev_map snd redo)
+ List.iter extend_dyn_grammar (List.rev_map snd redo)
(** No need to provide an init function : the grammar state is
statically available, and already empty initially, while
@@ -373,33 +306,3 @@ let with_grammar_rule_protection f x =
let reraise = Errors.push reraise in
let () = unfreeze fs in
iraise reraise
-
-(**********************************************************************)
-(** Ltac quotations *)
-
-let ltac_quotations = ref String.Set.empty
-
-let create_ltac_quotation name cast (e, l) =
- let () =
- if String.Set.mem name !ltac_quotations then
- failwith ("Ltac quotation " ^ name ^ " already registered")
- in
- let () = ltac_quotations := String.Set.add name !ltac_quotations in
- let entry = match l with
- | None -> Aentry (name_of_entry e)
- | Some l -> Aentryl (name_of_entry e, l)
- in
-(* let level = Some "1" in *)
- let level = None in
- let assoc = None in
- let rule =
- Next (Next (Next (Next (Next (Stop,
- Atoken (Lexer.terminal name)),
- Atoken (Lexer.terminal ":")),
- Atoken (Lexer.terminal "(")),
- entry),
- Atoken (Lexer.terminal ")"))
- in
- let action _ v _ _ _ loc = cast (loc, v) in
- let gram = (level, assoc, [Rule (rule, action)]) in
- Pcoq.grammar_extend Tactic.tactic_arg None (None, [gram])
diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli
index 23eaa64eec..6ec1066260 100644
--- a/parsing/egramcoq.mli
+++ b/parsing/egramcoq.mli
@@ -36,34 +36,27 @@ type notation_grammar = {
notgram_typs : notation_var_internalization_type list;
}
-type tactic_grammar = {
- tacgram_level : int;
- tacgram_prods : Tacexpr.raw_tactic_expr grammar_prod_item list;
-}
+(** {5 Extending the parser with Summary-synchronized commands} *)
+
+type 'a grammar_command
+(** Type of synchronized parsing extensions. The ['a] type should be
+ marshallable. *)
+
+val create_grammar_command : string -> ('a -> int) -> 'a grammar_command
+(** Create a new grammar-modifying command with the given name. The function
+ should modify the parser state and return the number of grammar extensions
+ performed. *)
+
+val extend_grammar : 'a grammar_command -> 'a -> unit
+(** Extend the grammar of Coq with the given data. *)
(** {5 Adding notations} *)
val extend_constr_grammar : Notation.level -> notation_grammar -> unit
(** Add a term notation rule to the parsing system. *)
-val extend_tactic_grammar : KerName.t -> tactic_grammar -> unit
-(** Add a tactic notation rule to the parsing system. This produces a TacAlias
- tactic with the provided kernel name. *)
-
-val extend_ml_tactic_grammar : Tacexpr.ml_tactic_name -> Tacexpr.raw_tactic_expr grammar_prod_item list list -> unit
-(** Add a ML tactic notation rule to the parsing system. This produces a
- TacML tactic with the provided string as name. *)
-
val recover_constr_grammar : notation -> Notation.level -> notation_grammar
(** For a declared grammar, returns the rule + the ordered entry types
of variables in the rule (for use in the interpretation) *)
val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b
-
-(** {5 Adding tactic quotations} *)
-
-val create_ltac_quotation : string ->
- ('grm Loc.located -> Tacexpr.raw_tactic_arg) -> ('grm Gram.entry * int option) -> unit
-(** [create_ltac_quotation name f e] adds a quotation rule to Ltac, that is,
- Ltac grammar now accepts arguments of the form ["name" ":" "(" <e> ")"], and
- generates an argument using [f] on the entry parsed by [e]. *)
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 207b43064c..75144addb2 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -57,16 +57,6 @@ type typed_entry = TypedEntry : 'a raw_abstract_argument_type * 'a G.entry -> ty
let object_of_typed_entry (TypedEntry (_, e)) = Gramobj.weaken_entry e
let weaken_entry x = Gramobj.weaken_entry x
-(** General entry keys *)
-
-(** This intermediate abstract representation of entries can
- both be reified into mlexpr for the ML extensions and
- dynamically interpreted as entries for the Coq level extensions
-*)
-
-type entry_name = EntryName :
- 'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, 'a) symbol -> entry_name
-
(** Grammar extensions *)
(** NB: [extend_statment =
@@ -740,108 +730,8 @@ let grammar_extend e reinit ext =
let ext = of_coq_extend_statement ext in
unsafe_grammar_extend e reinit ext
-(**********************************************************************)
-(* Interpret entry names of the form "ne_constr_list" as entry keys *)
-
-let coincide s pat off =
- let len = String.length pat in
- let break = ref true in
- let i = ref 0 in
- while !break && !i < len do
- let c = Char.code s.[off + !i] in
- let d = Char.code pat.[!i] in
- break := Int.equal c d;
- incr i
- done;
- !break
-
let name_of_entry e = Entry.unsafe_of_name (Gram.Entry.name e)
-let atactic n =
- if n = 5 then Aentry (name_of_entry Tactic.binder_tactic)
- else Aentryl (name_of_entry Tactic.tactic_expr, n)
-
-let try_get_entry u s =
- (** Order the effects: get_entry can raise Not_found *)
- let TypedEntry (typ, e) = get_entry u s in
- EntryName (typ, Aentry (name_of_entry e))
-
-(** Quite ad-hoc *)
-let get_tacentry n m =
- let check_lvl n =
- Int.equal m n
- && not (Int.equal m 5) (* Because tactic5 is at binder_tactic *)
- && not (Int.equal m 0) (* Because tactic0 is at simple_tactic *)
- in
- if check_lvl n then EntryName (rawwit wit_tactic, Aself)
- else if check_lvl (n + 1) then EntryName (rawwit wit_tactic, Anext)
- else EntryName (rawwit wit_tactic, atactic n)
-
-let rec parse_user_entry s sep =
- let l = String.length s in
- if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then
- let entry = parse_user_entry (String.sub s 3 (l-8)) "" in
- Ulist1 entry
- else if l > 12 && coincide s "ne_" 0 &&
- coincide s "_list_sep" (l-9) then
- let entry = parse_user_entry (String.sub s 3 (l-12)) "" in
- Ulist1sep (entry, sep)
- else if l > 5 && coincide s "_list" (l-5) then
- let entry = parse_user_entry (String.sub s 0 (l-5)) "" in
- Ulist0 entry
- else if l > 9 && coincide s "_list_sep" (l-9) then
- let entry = parse_user_entry (String.sub s 0 (l-9)) "" in
- Ulist0sep (entry, sep)
- else if l > 4 && coincide s "_opt" (l-4) then
- let entry = parse_user_entry (String.sub s 0 (l-4)) "" in
- Uopt entry
- else if l > 5 && coincide s "_mods" (l-5) then
- let entry = parse_user_entry (String.sub s 0 (l-1)) "" in
- Umodifiers entry
- else if Int.equal l 7 && coincide s "tactic" 0 && '5' >= s.[6] && s.[6] >= '0' then
- let n = Char.code s.[6] - 48 in
- Uentryl ("tactic", n)
- else
- let s = match s with "hyp" -> "var" | _ -> s in
- Uentry s
-
-let arg_list = function Rawwit t -> Rawwit (ListArg t)
-let arg_opt = function Rawwit t -> Rawwit (OptArg t)
-
-let rec interp_entry_name up_level s sep =
- let rec eval = function
- | Ulist1 e ->
- let EntryName (t, g) = eval e in
- EntryName (arg_list t, Alist1 g)
- | Ulist1sep (e, sep) ->
- let EntryName (t, g) = eval e in
- EntryName (arg_list t, Alist1sep (g, sep))
- | Ulist0 e ->
- let EntryName (t, g) = eval e in
- EntryName (arg_list t, Alist0 g)
- | Ulist0sep (e, sep) ->
- let EntryName (t, g) = eval e in
- EntryName (arg_list t, Alist0sep (g, sep))
- | Uopt e ->
- let EntryName (t, g) = eval e in
- EntryName (arg_opt t, Aopt g)
- | Umodifiers e ->
- let EntryName (t, g) = eval e in
- EntryName (arg_list t, Amodifiers g)
- | Uentry s ->
- begin
- try try_get_entry uprim s with Not_found ->
- try try_get_entry uconstr s with Not_found ->
- try try_get_entry utactic s with Not_found ->
- error ("Unknown entry "^s^".")
- end
- | Uentryl (s, n) ->
- (** FIXME: do better someday *)
- assert (String.equal s "tactic");
- get_tacentry n up_level
- in
- eval (parse_user_entry s sep)
-
let list_entry_names () =
let add_entry key (TypedEntry (entry, _)) accu = (key, unquote entry) :: accu in
let ans = Hashtbl.fold add_entry (get_utable uprim) [] in
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 35973a4d72..afe8889096 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -268,13 +268,9 @@ val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option
(** Binding general entry keys to symbols *)
-type entry_name = EntryName :
- 'a raw_abstract_argument_type * (raw_tactic_expr, 'a) Extend.symbol -> entry_name
+type typed_entry = TypedEntry : 'a raw_abstract_argument_type * 'a Gram.entry -> typed_entry
-(** [interp_entry_name lev n sep] returns the entry corresponding to the name
- [n] of the form "ne_constr_list" in a tactic entry of level [lev] with
- separator [sep]. *)
-val interp_entry_name : int -> string -> string -> entry_name
+val get_entry : gram_universe -> string -> typed_entry
(** Recover the list of all known tactic notation entries. *)
val list_entry_names : unit -> (string * argument_type) list
diff --git a/test-suite/bugs/closed/1850.v b/test-suite/bugs/closed/1850.v
new file mode 100644
index 0000000000..26b48093b7
--- /dev/null
+++ b/test-suite/bugs/closed/1850.v
@@ -0,0 +1,4 @@
+Parameter P : Type -> Type -> Type.
+Notation "e |= t --> v" := (P e t v) (at level 100, t at level 54).
+Fail Check (nat |= nat --> nat).
+
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-17 23:19:47 +0000