Notations: A step in cleaning constr_entry_key.

- Avoid dummy use of unit
- Do not decide as early as parsing the default level for pattern
- Prepare to further extensions

6 files changed, 51 insertions, 37 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index c1b66f7d6..13ff960f6 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -91,22 +91,25 @@ let production_position_eq pp1 pp2 = true (* pp1 = pp2 *) (* match pp1, pp2 with
 | NumLevel n1, NumLevel n2 -> Int.equal n1 n2
 | (NextLevel | NumLevel _), _ -> false *)
 
-let constr_entry_key_eq v1 v2 = match v1, v2 with
+let constr_entry_key_eq eq v1 v2 = match v1, v2 with
 | ETName, ETName -> true
 | ETReference, ETReference -> true
 | ETBigint, ETBigint -> true
 | ETBinder b1, ETBinder b2 -> b1 == b2
-| ETConstr (n1,pp1), ETConstr (n2,pp2) -> production_level_eq n1 n2 && production_position_eq pp1 pp2
-| ETPattern n1, ETPattern n2 -> Int.equal n1 n2
+| ETConstr lev1, ETConstr lev2 -> eq lev1 lev2
+| ETPattern n1, ETPattern n2 -> Option.equal Int.equal n1 n2
 | ETOther (s1,s1'), ETOther (s2,s2') -> String.equal s1 s2 && String.equal s1' s2'
 | (ETName | ETReference | ETBigint | ETBinder _ | ETConstr _ | ETPattern _ | ETOther _), _ -> false
 
-let level_eq (l1, t1, u1) (l2, t2, u2) =
-  let tolerability_eq (i1, r1) (i2, r2) =
-    Int.equal i1 i2 && parenRelation_eq r1 r2
-  in
+let level_eq_gen strict (l1, t1, u1) (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) =
+    if strict then production_level_eq l1 l2 && production_position_eq pp1 pp2
+    else production_level_eq l1 l2 in
   Int.equal l1 l2 && List.equal tolerability_eq t1 t2
-  && List.equal constr_entry_key_eq u1 u2
+  && List.equal (constr_entry_key_eq prod_eq) u1 u2
+
+let level_eq = level_eq_gen false
 
 let declare_scope scope =
   try let _ = String.Map.find scope !scope_map in ()
diff --git a/intf/extend.ml b/intf/extend.ml
index 5258ef56b..813ed6dc6 100644
--- a/intf/extend.ml
+++ b/intf/extend.ml
@@ -31,24 +31,24 @@ type production_level =
 
 (** User-level types used to tell how to parse or interpret of the non-terminal *)
 
-type ('lev,'pos) constr_entry_key_gen =
+type 'a constr_entry_key_gen =
   | ETName
   | ETReference
   | ETBigint
   | ETBinder of bool  (* open list of binders if true, closed list of binders otherwise *)
-  | ETConstr of ('lev * 'pos)
-  | ETPattern of int
+  | ETConstr of 'a
+  | ETPattern of int option
   | ETOther of string * string
 
 (** Entries level (left-hand side of grammar rules) *)
 
 type constr_entry_key =
-    (production_level,production_position) constr_entry_key_gen
+    (production_level * production_position) constr_entry_key_gen
 
 (** Entries used in productions, vernac side (e.g. "x bigint" or "x ident") *)
 
 type simple_constr_prod_entry_key =
-    (production_level,unit) constr_entry_key_gen
+    production_level option constr_entry_key_gen
 
 (** Entries used in productions (in right-hand-side of grammar rules), to parse non-terminals *)
 
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 6ef0b4fa8..009c1c19a 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -1181,8 +1181,8 @@ GEXTEND Gram
     [ [ IDENT "ident" -> ETName | IDENT "global" -> ETReference
       | IDENT "bigint" -> ETBigint
       | IDENT "binder" -> ETBinder true
-      | IDENT "pattern" -> ETPattern 0
-      | IDENT "pattern"; "at"; IDENT "level"; n = natural -> ETPattern n
+      | IDENT "pattern" -> ETPattern None
+      | IDENT "pattern"; "at"; IDENT "level"; n = natural -> ETPattern (Some n)
       | IDENT "closed"; IDENT "binder" -> ETBinder false
     ] ]
   ;
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index ae7364052..42329d03a 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -93,16 +93,28 @@ open Decl_kinds
   let sep = fun _ -> spc()
   let sep_v2 = fun _ -> str"," ++ spc()
 
-  let pr_set_entry_type = function
+  let pr_at_level = function
+    | NumLevel n -> keyword "at" ++ spc () ++ keyword "level" ++ spc () ++ int n
+    | NextLevel -> keyword "at" ++ spc () ++ keyword "next" ++ spc () ++ keyword "level"
+
+  let pr_set_entry_type pr = function
     | ETName -> str"ident"
     | ETReference -> str"global"
-    | ETPattern _ -> str"pattern"
-    | ETConstr _ -> str"constr"
+    | ETPattern None -> str"pattern"
+    | ETPattern (Some n) -> str"pattern" ++ spc () ++ pr_at_level (NumLevel n)
+    | ETConstr lev -> str"constr" ++ pr lev
     | ETOther (_,e) -> str e
     | ETBigint -> str "bigint"
     | ETBinder true -> str "binder"
     | ETBinder false -> str "closed binder"
 
+  let pr_at_level_opt = function
+    | None -> mt ()
+    | Some n -> spc () ++ pr_at_level n
+
+  let pr_set_simple_entry_type =
+    pr_set_entry_type pr_at_level_opt
+
   let pr_comment pr_c = function
     | CommentConstr c -> pr_c c
     | CommentString s -> qs s
@@ -359,17 +371,13 @@ open Decl_kinds
   let pr_thm_token k = keyword (Kindops.string_of_theorem_kind k)
 
   let pr_syntax_modifier = function
-    | SetItemLevel (l,NextLevel) ->
-      prlist_with_sep sep_v2 str l ++
-        spc() ++ keyword "at next level"
-    | SetItemLevel (l,NumLevel n) ->
-      prlist_with_sep sep_v2 str l ++
-        spc() ++ keyword "at level" ++ spc() ++ int n
-    | SetLevel n -> keyword "at level" ++ spc() ++ int n
+    | SetItemLevel (l,n) ->
+      prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level n
+    | SetLevel n -> pr_at_level (NumLevel n)
     | SetAssoc LeftA -> keyword "left associativity"
     | SetAssoc RightA -> keyword "right associativity"
     | SetAssoc NonA -> keyword "no associativity"
-    | SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_entry_type typ
+    | SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_simple_entry_type typ
     | SetOnlyPrinting -> keyword "only printing"
     | SetOnlyParsing -> keyword "only parsing"
     | SetCompatVersion v -> keyword("compat \"" ^ Flags.pr_version v ^ "\"")
diff --git a/printing/ppvernac.mli b/printing/ppvernac.mli
index 5e0cc8da5..603be6308 100644
--- a/printing/ppvernac.mli
+++ b/printing/ppvernac.mli
@@ -9,7 +9,7 @@
 (** This module implements pretty-printers for vernac_expr syntactic
     objects and their subcomponents. *)
 
-val pr_set_entry_type : ('a,'b) Extend.constr_entry_key_gen -> Pp.t
+val pr_set_entry_type : ('a -> Pp.t) -> 'a Extend.constr_entry_key_gen -> Pp.t
 
 (** Prints a fixpoint body *)
 val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.t
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index da8dda9c2..44a7462de 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -291,6 +291,7 @@ let precedence_of_entry_type from = function
       n, let (lp,rp) = prec_assoc a in if b == Left then lp else rp
   | ETConstr (NumLevel n,InternalProd) -> n, Prec n
   | ETConstr (NextLevel,_) -> from, L
+  | ETPattern n -> let n = match n with None -> 0 | Some n -> n in n, Prec n
   | _ -> 0, E (* ?? *)
 
 (* Some breaking examples *)
@@ -357,12 +358,13 @@ let check_open_binder isopen sl m =
       ++ strbrk "\" is allowed to occur.")
 
 let unparsing_metavar i from typs =
-  match List.nth typs (i-1) with
+  let x = List.nth typs (i-1) in
+  let prec = snd (precedence_of_entry_type from x) in
+  match x with
   | ETConstr _ | ETReference | ETBigint ->
-     let _,prec = precedence_of_entry_type from (List.nth typs (i-1)) in
      UnpMetaVar (i,prec)
-  | ETPattern n ->
-     UnpBinderMetaVar (i,Prec n)
+  | ETPattern _ ->
+     UnpBinderMetaVar (i,prec)
   | ETName ->
      UnpBinderMetaVar (i,Prec 0)
   | ETBinder isopen ->
@@ -613,7 +615,7 @@ let prod_entry_type = function
   | ETBigint -> ETProdBigint
   | ETBinder _ -> assert false (* See check_binder_type *)
   | ETConstr p -> ETProdConstr p
-  | ETPattern n -> ETProdPattern n
+  | ETPattern n -> ETProdPattern (match n with None -> 0 | Some n -> n)
   | ETOther (s,t) -> ETProdOther (s,t)
 
 let make_production etyps symbols =
@@ -676,7 +678,7 @@ let pr_arg_level from (lev,typ) =
   | (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 typ ++
+  Ppvernac.pr_set_entry_type (fun _ -> (*TO CHECK*) mt()) typ ++
   (match typ with ETConstr _ | ETPattern _ -> spc () ++ pplev lev | _ -> mt ())
 
 let pr_level ntn (from,args,typs) =
@@ -814,7 +816,7 @@ let interp_modifiers modl = let open NotationMods in
 	if Id.List.mem_assoc id acc.etyps then
 	  user_err ~hdr:"Metasyntax.interp_modifiers"
             (str s ++ str " is already assigned to an entry or constr level.");
-	let typ = ETConstr (n,()) in
+        let typ = ETConstr (Some n) in
         interp { acc with etyps = (id,typ)::acc.etyps; } (SetItemLevel (idl,n)::l)
     | SetLevel n :: l ->
 
@@ -881,11 +883,12 @@ let get_compat_version mods =
 let set_entry_type etyps (x,typ) =
   let typ = try
     match List.assoc x etyps, typ with
-      | ETConstr (n,()), (_,BorderProd (left,_)) ->
+      | ETConstr (Some n), (_,BorderProd (left,_)) ->
           ETConstr (n,BorderProd (left,None))
-      | ETConstr (n,()), (_,InternalProd) -> ETConstr (n,InternalProd)
+      | ETConstr (Some n), (_,InternalProd) -> ETConstr (n,InternalProd)
       | (ETPattern _ | ETName | ETBigint | ETOther _ |
 	 ETReference | ETBinder _ as t), _ -> t
+      | ETConstr None, _ -> ETConstr typ
     with Not_found -> ETConstr typ
   in (x,typ)
 
@@ -1060,7 +1063,7 @@ let remove_curly_brackets l =
 
 module SynData = struct
 
-  type subentry_types = (Id.t * (production_level, production_position) constr_entry_key_gen) list
+  type subentry_types = (Id.t * (production_level * production_position) constr_entry_key_gen) list
 
   (* XXX: Document *)
   type syn_data = {