Suite picking numeral notation

Ceci est une suite à numeral notation in custom entries, cherchant à
raffiner la compatibilité entre entrées. C'est mélangé avec le "pick"
précédent, et c'est en chantier.

4 files changed, 78 insertions, 84 deletions

diff --git a/parsing/notgram_ops.ml b/parsing/notgram_ops.ml
index 5c220abeda..5c79ec2eba 100644
--- a/parsing/notgram_ops.ml
+++ b/parsing/notgram_ops.ml
@@ -13,22 +13,7 @@ open CErrors
 open Util
 open Notation
 open Notation_gram
-
-(* Uninterpreted notation levels *)
-
-let notation_level_map = Summary.ref ~name:"notation_level_map" NotationMap.empty
-
-let declare_notation_level ?(onlyprint=false) ntn level =
-  try
-    let (level,onlyprint) = NotationMap.find ntn !notation_level_map in
-    if not onlyprint then anomaly (str "Notation " ++ pr_notation ntn ++ str " is already assigned a level.")
-  with Not_found ->
-  notation_level_map := NotationMap.add ntn (level,onlyprint) !notation_level_map
-
-let level_of_notation ?(onlyprint=false) ntn =
-  let (level,onlyprint') = NotationMap.find ntn !notation_level_map in
-  if onlyprint' && not onlyprint then raise Not_found;
-  level
+open Constrexpr
 
 (**********************************************************************)
 (* Equality *)
@@ -40,34 +25,61 @@ let parenRelation_eq t1 t2 = match t1, t2 with
 | Prec l1, Prec l2 -> Int.equal l1 l2
 | _ -> 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 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
-| ETString, ETString -> true
+let constr_entry_key_compatible v1 v2 = match v1, v2 with
+| (ETGlobal | ETBigint | ETString), (ETGlobal | ETBigint | ETString) -> true
+| (ETIdent | ETBigint | ETString), ETIdent -> true
+| ETIdent, (ETBigint | ETString) -> 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
+| ETConstr (s1,bko1,_lev1), ETConstr (s2,bko2,_lev2) ->
+   notation_entry_eq s1 s2 && Option.equal (=) bko1 bko2
 | ETPattern (b1,n1), ETPattern (b2,n2) -> b1 = b2 && Option.equal Int.equal n1 n2
 | (ETIdent | ETGlobal | ETBigint | ETString | ETBinder _ | ETConstr _ | ETPattern _), _ -> false
 
-let level_eq_gen strict (s1, l1, t1, u1) (s2, l2, t2, u2) =
+let level_compatible (s1, l1, t1, u1) (s2, l2, t2, u2) =
   let tolerability_eq (i1, r1) (i2, r2) = Int.equal i1 i2 && parenRelation_eq r1 r2 in
-  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 tolerability_eq t1 t2
-  && List.equal (constr_entry_key_eq prod_eq) u1 u2
+  && List.equal constr_entry_key_compatible u1 u2
 
-let level_eq = level_eq_gen false
+(* Uninterpreted notation levels *)
+
+let pr_arg_level from (lev,typ) =
+  let pplev = function
+  | (n,L) when Int.equal n from -> str "at next level"
+  | (n,E) -> str "at level " ++ int n
+  | (n,L) -> str "at level below " ++ int n
+  | (n,Prec m) when Int.equal m n -> str "at level " ++ int n
+  | (n,_) -> str "Unknown level" in
+  Ppvernac.pr_set_entry_type (fun _ -> (*TO CHECK*) mt()) typ ++
+  (match typ with
+   | ETConstr _ | ETPattern _ -> spc () ++ pplev lev
+   | _ -> mt ())
+
+let pr_level ntn (from,fromlevel,args,typs) =
+  (match from with InConstrEntry -> mt () | InCustomEntry s -> str "in " ++ str s ++ spc()) ++
+  str "at level " ++ int fromlevel ++ spc () ++ str "with arguments" ++ spc() ++
+  prlist_with_sep pr_comma (pr_arg_level fromlevel) (List.combine args typs)
+
+let error_incompatible_level ntn oldprec prec =
+  user_err
+    (str "Notation " ++ pr_notation ntn ++ str " is already defined" ++ spc() ++
+    pr_level ntn oldprec ++
+    spc() ++ str "while it is now required to be" ++ spc() ++
+    pr_level ntn prec ++ str ".")
+
+let notation_level_map = Summary.ref ~name:"notation_level_map" NotationMap.empty
+
+let declare_notation_level ?(onlyprint=false) ntn prec =
+  let oldprecs =
+    try
+      let oldprecs = NotationMap.find ntn !notation_level_map in
+      let f (old,onlyprint) = not onlyprint && not (level_compatible prec old) in
+      match List.filter f oldprecs with
+      | (oldprec,_)::_ -> error_incompatible_level ntn oldprec prec
+      | [] -> oldprecs
+    with Not_found -> [] in
+  notation_level_map := NotationMap.add ntn ((prec,onlyprint)::oldprecs) !notation_level_map
+
+let level_of_notation ?(onlyprint=false) ntn =
+  let (level,onlyprint') = NotationMap.find ntn !notation_level_map in
+  if onlyprint' && not onlyprint then raise Not_found;
+  level
diff --git a/parsing/notgram_ops.mli b/parsing/notgram_ops.mli
index c31f4505e7..3185db8f26 100644
--- a/parsing/notgram_ops.mli
+++ b/parsing/notgram_ops.mli
@@ -12,7 +12,7 @@
 open Constrexpr
 open Notation_gram
 
-val level_eq : level -> level -> bool
+val level_compatible : level -> level -> bool
 
 (** {6 Declare and test the level of a (possibly uninterpreted) notation } *)
 
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 4ab800c9ba..dbfa939230 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -25,6 +25,20 @@ Check [ << # 0 >> ].
 Notation "n" := n%nat (in custom myconstr at level 0, n bigint).
 Check [ 2 + 3 ].
 
+Module A1.
+  (* This is compatible with bigint *)
+  Notation "x" := x (in custom myconstr at level 0, x ident).
+  (* This is incompatible with ident *)
+  Fail Notation "x" := x (in custom myconstr at level 0, x global).
+End A1.
+
+Module A2.
+  (* This is compatible with bigint *)
+  Notation "x" := x (in custom myconstr at level 0, x global).
+  (* This is compatible with bigint and global *)
+  Notation "x" := x (in custom myconstr at level 0, x string).
+End A2.
+
 End A.
 
 Module B.
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index d39ee60c25..c9ad71c2e8 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -744,30 +744,6 @@ let recompute_assoc typs = let open Gramlib.Gramext in
 (**************************************************************************)
 (* Registration of syntax extensions (parsing/printing, no interpretation)*)
 
-let pr_arg_level from (lev,typ) =
-  let pplev = function
-  | (n,L) when Int.equal n from -> str "at next level"
-  | (n,E) -> str "at level " ++ int n
-  | (n,L) -> str "at level below " ++ int n
-  | (n,Prec m) when Int.equal m n -> str "at level " ++ int n
-  | (n,_) -> str "Unknown level" in
-  Ppvernac.pr_set_entry_type (fun _ -> (*TO CHECK*) mt()) typ ++
-  (match typ with
-   | ETConstr _ | ETPattern _ -> spc () ++ pplev lev
-   | _ -> mt ())
-
-let pr_level ntn (from,fromlevel,args,typs) =
-  (match from with InConstrEntry -> mt () | InCustomEntry s -> str "in " ++ str s ++ spc()) ++
-  str "at level " ++ int fromlevel ++ spc () ++ str "with arguments" ++ spc() ++
-  prlist_with_sep pr_comma (pr_arg_level fromlevel) (List.combine args typs)
-
-let error_incompatible_level ntn oldprec prec =
-  user_err
-    (str "Notation " ++ pr_notation ntn ++ str " is already defined" ++ spc() ++
-    pr_level ntn oldprec ++
-    spc() ++ str "while it is now required to be" ++ spc() ++
-    pr_level ntn prec ++ str ".")
-
 let error_parsing_incompatible_level ntn ntn' oldprec prec =
   user_err
     (str "Notation " ++ pr_notation ntn ++ str " relies on a parsing rule for " ++ pr_notation ntn' ++ spc() ++
@@ -792,27 +768,21 @@ let check_and_extend_constr_grammar ntn rule =
     if notation_eq ntn ntn_for_grammar then raise Not_found;
     let prec = rule.notgram_level in
     let oldprec = Notgram_ops.level_of_notation ntn_for_grammar in
-    if not (Notgram_ops.level_eq prec oldprec) then error_parsing_incompatible_level ntn ntn_for_grammar oldprec prec;
-  with Not_found ->
+    if not (Notgram_ops.level_compatible prec oldprec) then error_parsing_incompatible_level ntn ntn_for_grammar oldprec prec;
+  with NoSyntaxRule ->
     Egramcoq.extend_constr_grammar rule
 
 let cache_one_syntax_extension se =
   let ntn = se.synext_notation in
   let prec = se.synext_level in
   let onlyprint = se.synext_notgram.notgram_onlyprinting in
-  try
-    let oldprec = Notgram_ops.level_of_notation ~onlyprint ntn in
-    if not (Notgram_ops.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec;
-  with Not_found ->
-    begin
-      (* Reserve the notation level *)
-      Notgram_ops.declare_notation_level ntn prec ~onlyprint;
-      (* Declare the parsing rule *)
-      if not onlyprint then List.iter (check_and_extend_constr_grammar ntn) se.synext_notgram.notgram_rules;
-      (* Declare the notation rule *)
-      declare_notation_rule ntn
-        ~extra:se.synext_extra (se.synext_unparsing, let (_,lev,_,_) = prec in lev) se.synext_notgram
-    end
+  (* Reserve the notation level *)
+  Notgram_ops.declare_notation_level ntn prec ~onlyprint;
+  (* Declare the parsing rule *)
+  if not onlyprint then List.iter (check_and_extend_constr_grammar ntn) se.synext_notgram.notgram_rules;
+  (* Declare the notation rule *)
+  declare_notation_rule ntn
+    ~extra:se.synext_extra (se.synext_unparsing, let (_,lev,_,_) = prec in lev) se.synext_notgram
 
 let cache_syntax_extension (_, (_, sy)) =
   cache_one_syntax_extension sy
@@ -1182,7 +1152,7 @@ let find_precedence custom lev etyps symbols onlyprint =
 
 let check_curly_brackets_notation_exists () =
   try let _ = Notgram_ops.level_of_notation (InConstrEntrySomeLevel,"{ _ }") in ()
-  with Not_found ->
+  with NoSyntaxRule ->
     user_err Pp.(str "Notations involving patterns of the form \"{ _ }\" are treated \n\
 specially and require that the notation \"{ _ }\" is already reserved.")
 
@@ -1421,8 +1391,6 @@ let with_syntax_protection f x =
 (**********************************************************************)
 (* Recovering existing syntax                                         *)
 
-exception NoSyntaxRule
-
 let recover_notation_syntax ntn =
   try
     let prec = Notgram_ops.level_of_notation ~onlyprint:true ntn (* Be as little restrictive as possible *) in
@@ -1435,7 +1403,7 @@ let recover_notation_syntax ntn =
       synext_unparsing = pp_rule;
       synext_extra = pp_extra_rules;
     }
-  with Not_found ->
+  with Not_found | NoSyntaxRule ->
     raise NoSyntaxRule
 
 let recover_squash_syntax sy =