Fix #11121: Simultaneous definition of term and notation in custom grammar

5 files changed, 30 insertions, 67 deletions

diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index c19dd00b38..429e740403 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -165,11 +165,11 @@ GRAMMAR EXTEND Gram
              collapse -(3) into the numeral -3. *)
           (match c.CAst.v with
             | CPrim (Numeral (NumTok.SPlus,n)) ->
-                CAst.make ~loc @@ CNotation(None,(InConstrEntrySomeLevel,"( _ )"),([c],[],[],[]))
+                CAst.make ~loc @@ CNotation(None,(InConstrEntry,"( _ )"),([c],[],[],[]))
             | _ -> c) }
       | "{|"; c = record_declaration; bar_cbrace -> { c }
       | "{"; c = binder_constr ; "}" ->
-        { CAst.make ~loc @@ CNotation(None,(InConstrEntrySomeLevel,"{ _ }"),([c],[],[],[])) }
+        { CAst.make ~loc @@ CNotation(None,(InConstrEntry,"{ _ }"),([c],[],[],[])) }
       | "`{"; c = operconstr LEVEL "200"; "}" ->
         { CAst.make ~loc @@ CGeneralization (MaxImplicit, None, c) }
       | "`("; c = operconstr LEVEL "200"; ")" ->
@@ -346,7 +346,7 @@ GRAMMAR EXTEND Gram
              collapse -(3) into the numeral -3. *)
           match p.CAst.v with
           | CPatPrim (Numeral (NumTok.SPlus,n)) ->
-              CAst.make ~loc @@ CPatNotation(None,(InConstrEntrySomeLevel,"( _ )"),([p],[]),[])
+              CAst.make ~loc @@ CPatNotation(None,(InConstrEntry,"( _ )"),([p],[]),[])
           | _ -> p }
       | "("; p = pattern LEVEL "200"; "|" ; pl = LIST1 pattern LEVEL "200" SEP "|"; ")" ->
         { CAst.make ~loc @@ CPatOr (p::pl) }
diff --git a/parsing/notation_gram.ml b/parsing/notation_gram.ml
index 7940931dfc..045f497070 100644
--- a/parsing/notation_gram.ml
+++ b/parsing/notation_gram.ml
@@ -9,13 +9,6 @@
 (************************************************************************)
 
 open Names
-open Extend
-open Constrexpr
-
-(** Dealing with precedences *)
-
-type level = notation_entry * entry_level * entry_relative_level list * constr_entry_key list
-  (* first argument is InCustomEntry s for custom entries *)
 
 type grammar_constr_prod_item =
   | GramConstrTerminal of string Tok.p
@@ -28,10 +21,11 @@ type grammar_constr_prod_item =
 (** Grammar rules for a notation *)
 
 type one_notation_grammar = {
-  notgram_level : level;
+  notgram_level : Notation.level;
   notgram_assoc : Gramlib.Gramext.g_assoc option;
   notgram_notation : Constrexpr.notation;
   notgram_prods : grammar_constr_prod_item list list;
+  notgram_typs : Extend.constr_entry_key list;
 }
 
 type notation_grammar = one_notation_grammar list
diff --git a/parsing/notgram_ops.ml b/parsing/notgram_ops.ml
index 1d18e7dcfa..74ced431c9 100644
--- a/parsing/notgram_ops.ml
+++ b/parsing/notgram_ops.ml
@@ -12,63 +12,33 @@ open Pp
 open CErrors
 open Util
 open Notation
-open Constrexpr
 
-(* Register the level of notation for parsing and printing
+(* Register the grammar of notation for parsing and printing
    (also register the parsing rule if not onlyprinting) *)
 
-let notation_level_map = Summary.ref ~name:"notation_level_map" NotationMap.empty
+let notation_grammar_map = Summary.ref ~name:"notation_grammar_map" NotationMap.empty
 
-let declare_notation_level ntn parsing_rule level =
+let declare_notation_grammar ntn rule =
   try
-    let _ = NotationMap.find ntn !notation_level_map in
-    anomaly (str "Notation " ++ pr_notation ntn ++ str " is already assigned a level.")
+    let _ = NotationMap.find ntn !notation_grammar_map in
+    anomaly (str "Notation " ++ pr_notation ntn ++ str " is already assigned a grammar.")
   with Not_found ->
-  notation_level_map := NotationMap.add ntn (parsing_rule,level) !notation_level_map
+  notation_grammar_map := NotationMap.add ntn rule !notation_grammar_map
 
-let level_of_notation ntn =
-  NotationMap.find ntn !notation_level_map
+let grammar_of_notation ntn =
+  NotationMap.find ntn !notation_grammar_map
 
-let get_defined_notations () =
-  NotationSet.elements @@ NotationMap.domain !notation_level_map
-
-(**********************************************************************)
-(* Equality *)
-
-open Extend
-
-let entry_relative_level_eq t1 t2 = match t1, t2 with
-| LevelLt n1, LevelLt n2 -> Int.equal n1 n2
-| LevelLe n1, LevelLe n2 -> Int.equal n1 n2
-| LevelSome, LevelSome -> true
-| (LevelLt _ | LevelLe _ | LevelSome), _ -> false
-
-let production_position_eq pp1 pp2 = match (pp1,pp2) with
-| BorderProd (side1,assoc1), BorderProd (side2,assoc2) -> side1 = side2 && assoc1 = assoc2
-| InternalProd, InternalProd -> true
-| (BorderProd _ | InternalProd), _ -> false
+let notation_subentries_map = Summary.ref ~name:"notation_subentries_map" NotationMap.empty
 
-let production_level_eq l1 l2 = match (l1,l2) with
-| NextLevel, NextLevel -> true
-| NumLevel n1, NumLevel n2 -> Int.equal n1 n2
-| DefaultLevel, DefaultLevel -> true
-| (NextLevel | NumLevel _ | DefaultLevel), _ -> false
-
-let constr_entry_key_eq eq v1 v2 = match v1, v2 with
-| ETIdent, ETIdent -> true
-| ETGlobal, ETGlobal -> true
-| ETBigint, ETBigint -> true
-| ETBinder b1, ETBinder b2 -> b1 == b2
-| ETConstr (s1,bko1,lev1), ETConstr (s2,bko2,lev2) ->
-   notation_entry_eq s1 s2 && eq lev1 lev2 && Option.equal (=) bko1 bko2
-| ETPattern (b1,n1), ETPattern (b2,n2) -> b1 = b2 && Option.equal Int.equal n1 n2
-| (ETIdent | ETGlobal | ETBigint | ETBinder _ | ETConstr _ | ETPattern _), _ -> false
+let declare_notation_subentries ntn entries =
+  try
+    let _ = NotationMap.find ntn !notation_grammar_map in
+    anomaly (str "Notation " ++ pr_notation ntn ++ str " is already assigned a grammar.")
+  with Not_found ->
+  notation_subentries_map := NotationMap.add ntn entries !notation_subentries_map
 
-let level_eq_gen strict (s1, l1, t1, u1) (s2, l2, t2, u2) =
-  let prod_eq (l1,pp1) (l2,pp2) =
-    not strict ||
-    (production_level_eq l1 l2 && production_position_eq pp1 pp2) in
-  notation_entry_eq s1 s2 && Int.equal l1 l2 && List.equal entry_relative_level_eq t1 t2
-  && List.equal (constr_entry_key_eq prod_eq) u1 u2
+let subentries_of_notation ntn =
+  NotationMap.find ntn !notation_subentries_map
 
-let level_eq = level_eq_gen false
+let get_defined_notations () =
+  NotationSet.elements @@ NotationMap.domain !notation_grammar_map
diff --git a/parsing/notgram_ops.mli b/parsing/notgram_ops.mli
index dd1375a1f1..15b8717705 100644
--- a/parsing/notgram_ops.mli
+++ b/parsing/notgram_ops.mli
@@ -12,14 +12,14 @@
 open Constrexpr
 open Notation_gram
 
-val level_eq : level -> level -> bool
-val entry_relative_level_eq : entry_relative_level -> entry_relative_level -> bool
+(** {6 Declare the parsing rules and entries of a (possibly uninterpreted) notation } *)
 
-(** {6 Declare and test the level of a (possibly uninterpreted) notation } *)
-
-val declare_notation_level : notation -> notation_grammar option -> level -> unit
-val level_of_notation : notation -> notation_grammar option * level
+val declare_notation_grammar : notation -> notation_grammar -> unit
+val grammar_of_notation : notation -> notation_grammar
   (** raise [Not_found] if not declared *)
 
+val declare_notation_subentries : notation -> Extend.constr_entry_key list -> unit
+val subentries_of_notation : notation -> Extend.constr_entry_key list
+
 (** Returns notations with defined parsing/printing rules *)
 val get_defined_notations : unit -> notation list
diff --git a/parsing/ppextend.ml b/parsing/ppextend.ml
index b888614ecb..fe6e8360c1 100644
--- a/parsing/ppextend.ml
+++ b/parsing/ppextend.ml
@@ -13,7 +13,6 @@ open Pp
 open CErrors
 open Notation
 open Constrexpr
-open Notgram_ops
 
 (*s Pretty-print. *)