Merge PR #11635: Cleanup around the tolerability structure

Reviewed-by: ejgallego

6 files changed, 27 insertions, 29 deletions

diff --git a/parsing/notation_gram.ml b/parsing/notation_gram.ml
index ffc92fa53a..427505c199 100644
--- a/parsing/notation_gram.ml
+++ b/parsing/notation_gram.ml
@@ -10,14 +10,11 @@
 
 open Names
 open Extend
+open Constrexpr
 
 (** Dealing with precedences *)
 
-type precedence = int
-type parenRelation = L | E | Any | Prec of precedence
-type tolerability = precedence * parenRelation
-
-type level = Constrexpr.notation_entry * precedence * tolerability list * constr_entry_key list
+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 =
diff --git a/parsing/notgram_ops.ml b/parsing/notgram_ops.ml
index a84d2a4cb0..b6699493bb 100644
--- a/parsing/notgram_ops.ml
+++ b/parsing/notgram_ops.ml
@@ -12,7 +12,7 @@ open Pp
 open CErrors
 open Util
 open Notation
-open Notation_gram
+open Constrexpr
 
 (* Register the level of notation for parsing and printing
    (also register the parsing rule if not onlyprinting) *)
@@ -37,10 +37,11 @@ let get_defined_notations () =
 
 open Extend
 
-let parenRelation_eq t1 t2 = match t1, t2 with
-| L, L | E, E | Any, Any -> true
-| Prec l1, Prec l2 -> Int.equal l1 l2
-| _ -> false
+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
@@ -64,11 +65,10 @@ let constr_entry_key_eq eq v1 v2 = match v1, v2 with
 | (ETIdent | ETGlobal | ETBigint | ETBinder _ | ETConstr _ | ETPattern _), _ -> false
 
 let level_eq_gen strict (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
+  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 level_eq = level_eq_gen false
diff --git a/parsing/notgram_ops.mli b/parsing/notgram_ops.mli
index 7c676fbb10..d8b7e8e4c1 100644
--- a/parsing/notgram_ops.mli
+++ b/parsing/notgram_ops.mli
@@ -13,6 +13,7 @@ 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 and test the level of a (possibly uninterpreted) notation } *)
 
diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib
index 2154f2f881..12311f9cd9 100644
--- a/parsing/parsing.mllib
+++ b/parsing/parsing.mllib
@@ -2,8 +2,8 @@ Tok
 CLexer
 Extend
 Notation_gram
-Ppextend
 Notgram_ops
+Ppextend
 Pcoq
 G_constr
 G_prim
diff --git a/parsing/ppextend.ml b/parsing/ppextend.ml
index 0277e79adb..393ab8a302 100644
--- a/parsing/ppextend.ml
+++ b/parsing/ppextend.ml
@@ -12,7 +12,8 @@ open Util
 open Pp
 open CErrors
 open Notation
-open Notation_gram
+open Constrexpr
+open Notgram_ops
 
 (*s Pretty-print. *)
 
@@ -37,22 +38,22 @@ let ppcmd_of_cut = function
   | PpBrk(n1,n2) -> brk(n1,n2)
 
 type unparsing =
-  | UnpMetaVar of int * parenRelation
-  | UnpBinderMetaVar of int * parenRelation
-  | UnpListMetaVar of int * parenRelation * unparsing list
-  | UnpBinderListMetaVar of int * bool * unparsing list
+  | UnpMetaVar of entry_relative_level
+  | UnpBinderMetaVar of entry_relative_level
+  | UnpListMetaVar of entry_relative_level * unparsing list
+  | UnpBinderListMetaVar of bool * unparsing list
   | UnpTerminal of string
   | UnpBox of ppbox * unparsing Loc.located list
   | UnpCut of ppcut
 
-type unparsing_rule = unparsing list * precedence
+type unparsing_rule = unparsing list * entry_level
 type extra_unparsing_rules = (string * string) list
 
 let rec unparsing_eq unp1 unp2 = match (unp1,unp2) with
-  | UnpMetaVar (n1,p1), UnpMetaVar (n2,p2) -> n1 = n2 && p1 = p2
-  | UnpBinderMetaVar (n1,p1), UnpBinderMetaVar (n2,p2) -> n1 = n2 && p1 = p2
-  | UnpListMetaVar (n1,p1,l1), UnpListMetaVar (n2,p2,l2) -> n1 = n2 && p1 = p2 && List.for_all2eq unparsing_eq l1 l2
-  | UnpBinderListMetaVar (n1,b1,l1), UnpBinderListMetaVar (n2,b2,l2) -> n1 = n2 && b1 = b2 && List.for_all2eq unparsing_eq l1 l2
+  | UnpMetaVar p1, UnpMetaVar p2 -> entry_relative_level_eq p1 p2
+  | UnpBinderMetaVar p1, UnpBinderMetaVar p2 -> entry_relative_level_eq p1 p2
+  | UnpListMetaVar (p1,l1), UnpListMetaVar (p2,l2) -> entry_relative_level_eq p1 p2 && List.for_all2eq unparsing_eq l1 l2
+  | UnpBinderListMetaVar (b1,l1), UnpBinderListMetaVar (b2,l2) -> b1 = b2 && List.for_all2eq unparsing_eq l1 l2
   | UnpTerminal s1, UnpTerminal s2 -> String.equal s1 s2
   | UnpBox (b1,l1), UnpBox (b2,l2) -> b1 = b2 && List.for_all2eq unparsing_eq (List.map snd l1) (List.map snd l2)
   | UnpCut p1, UnpCut p2 -> p1 = p2
diff --git a/parsing/ppextend.mli b/parsing/ppextend.mli
index 7996e7696d..346fc83f5f 100644
--- a/parsing/ppextend.mli
+++ b/parsing/ppextend.mli
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Constrexpr
-open Notation_gram
 
 (** {6 Pretty-print. } *)
 
@@ -31,15 +30,15 @@ val ppcmd_of_cut : ppcut -> Pp.t
 
 (** Declare and look for the printing rule for symbolic notations *)
 type unparsing =
-  | UnpMetaVar of int * parenRelation
-  | UnpBinderMetaVar of int * parenRelation
-  | UnpListMetaVar of int * parenRelation * unparsing list
-  | UnpBinderListMetaVar of int * bool * unparsing list
+  | UnpMetaVar of entry_relative_level
+  | UnpBinderMetaVar of entry_relative_level
+  | UnpListMetaVar of entry_relative_level * unparsing list
+  | UnpBinderListMetaVar of bool * unparsing list
   | UnpTerminal of string
   | UnpBox of ppbox * unparsing Loc.located list
   | UnpCut of ppcut
 
-type unparsing_rule = unparsing list * precedence
+type unparsing_rule = unparsing list * entry_level
 type extra_unparsing_rules = (string * string) list
 
 val unparsing_eq : unparsing -> unparsing -> bool