Notations: renaming an internal data structure (level -> signature).

This is to emphasize that this is more general than just a level.

Should not change semantics.

parsing/notation_gram.ml

@@ -14,7 +14,8 @@ open Constrexpr
 
 (** Dealing with precedences *)
 
-type level = notation_entry * entry_level * entry_relative_level list * constr_entry_key list
+type notation_signature =
+  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 =
@@ -28,7 +29,7 @@ type grammar_constr_prod_item =
 (** Grammar rules for a notation *)
 
 type one_notation_grammar = {
-  notgram_level : level;
+  notgram_signature : notation_signature;
   notgram_assoc : Gramlib.Gramext.g_assoc option;
   notgram_notation : Constrexpr.notation;
   notgram_prods : grammar_constr_prod_item list list;

parsing/notgram_ops.ml

@@ -16,17 +16,17 @@ open Constrexpr
 
 (* Uninterpreted notation levels *)
 
-let notation_level_map = Summary.ref ~name:"notation_level_map" NotationMap.empty
+let notation_signature_map = Summary.ref ~name:"notation_signature_map" NotationMap.empty
 
-let declare_notation_level ?(onlyprint=false) ntn level =
+let declare_notation_signature ?(onlyprint=false) ntn level =
   try
-    let (level,onlyprint) = NotationMap.find ntn !notation_level_map in
+    let (level,onlyprint) = NotationMap.find ntn !notation_signature_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
+  notation_signature_map := NotationMap.add ntn (level,onlyprint) !notation_signature_map
 
-let level_of_notation ?(onlyprint=false) ntn =
-  let (level,onlyprint') = NotationMap.find ntn !notation_level_map in
+let signature_of_notation ?(onlyprint=false) ntn =
+  let (level,onlyprint') = NotationMap.find ntn !notation_signature_map in
   if onlyprint' && not onlyprint then raise Not_found;
   level
 
@@ -61,11 +61,11 @@ let constr_entry_key_eq eq v1 v2 = match v1, v2 with
 | ETPattern (b1,n1), ETPattern (b2,n2) -> b1 = b2 && Option.equal Int.equal n1 n2
 | (ETIdent | ETGlobal | ETBigint | ETBinder _ | ETConstr _ | ETPattern _), _ -> false
 
-let level_eq_gen strict (s1, l1, t1, u1) (s2, l2, t2, u2) =
+let notation_signature_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 level_eq = level_eq_gen false
+let notation_signature_eq = notation_signature_eq_gen false

parsing/notgram_ops.mli

@@ -12,9 +12,9 @@
 open Constrexpr
 open Notation_gram
 
-val level_eq : level -> level -> bool
+val notation_signature_eq : notation_signature -> notation_signature -> bool
 
 (** {6 Declare and test the level of a (possibly uninterpreted) notation } *)
 
-val declare_notation_level : ?onlyprint:bool -> notation -> level -> unit
-val level_of_notation : ?onlyprint:bool -> notation -> level (** raise [Not_found] if no level or not respecting onlyprint *)
+val declare_notation_signature : ?onlyprint:bool -> notation -> notation_signature -> unit
+val signature_of_notation : ?onlyprint:bool -> notation -> notation_signature (** raise [Not_found] if no level or not respecting onlyprint *)

vernac/egramcoq.ml

@@ -529,7 +529,7 @@ let make_act : type r. r target -> _ -> r gen_eval = function
   CAst.make ~loc @@ CPatNotation (notation, env, [])
 
 let extend_constr state forpat ng =
-  let custom,n,_,_ = ng.notgram_level in
+  let custom,n,_,_ = ng.notgram_signature in
   let assoc = ng.notgram_assoc in
   let (entry, level) = interp_constr_entry_key custom forpat n in
   let fold (accu, state) pt =

vernac/metasyntax.ml

@@ -719,28 +719,28 @@ let pr_arg_level from (lev,typ) =
   | LevelSome -> mt () in
   Ppvernac.pr_set_entry_type (fun _ -> (*TO CHECK*) mt()) typ ++ pplev lev
 
-let pr_level ntn (from,fromlevel,args,typs) =
+let pr_level_signature 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 =
+let error_incompatible_level ntn old_ntn_sign ntn_sign =
   user_err
     (str "Notation " ++ pr_notation ntn ++ str " is already defined" ++ spc() ++
-    pr_level ntn oldprec ++
+    pr_level_signature ntn old_ntn_sign ++
     spc() ++ str "while it is now required to be" ++ spc() ++
-    pr_level ntn prec ++ str ".")
+    pr_level_signature ntn ntn_sign ++ str ".")
 
-let error_parsing_incompatible_level ntn ntn' oldprec prec =
+let error_parsing_incompatible_level ntn ntn' old_ntn_sign ntn_sign =
   user_err
     (str "Notation " ++ pr_notation ntn ++ str " relies on a parsing rule for " ++ pr_notation ntn' ++ spc() ++
     str " which is already defined" ++ spc() ++
-    pr_level ntn oldprec ++
+    pr_level_signature ntn old_ntn_sign ++
     spc() ++ str "while it is now required to be" ++ spc() ++
-    pr_level ntn prec ++ str ".")
+    pr_level_signature ntn ntn_sign ++ str ".")
 
 type syntax_extension = {
-  synext_level : Notation_gram.level;
+  synext_signature : notation_signature;
   synext_notation : notation;
   synext_notgram : notation_grammar;
   synext_unparsing : unparsing list;
@@ -753,28 +753,28 @@ let check_and_extend_constr_grammar ntn rule =
   try
     let ntn_for_grammar = rule.notgram_notation in
     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;
+    let prec = rule.notgram_signature in
+    let oldprec = Notgram_ops.signature_of_notation ntn_for_grammar in
+    if not (Notgram_ops.notation_signature_eq prec oldprec) then error_parsing_incompatible_level ntn ntn_for_grammar oldprec prec;
   with Not_found ->
     Egramcoq.extend_constr_grammar rule
 
 let cache_one_syntax_extension se =
   let ntn = se.synext_notation in
-  let prec = se.synext_level in
+  let ntn_sign = se.synext_signature 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;
+    let old_ntn_sign = Notgram_ops.signature_of_notation ~onlyprint ntn in
+    if not (Notgram_ops.notation_signature_eq ntn_sign old_ntn_sign) then error_incompatible_level ntn old_ntn_sign ntn_sign;
   with Not_found ->
     begin
       (* Reserve the notation level *)
-      Notgram_ops.declare_notation_level ntn prec ~onlyprint;
+      Notgram_ops.declare_notation_signature ntn ntn_sign ~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
+        ~extra:se.synext_extra (se.synext_unparsing, let (_,lev,_,_) = ntn_sign in lev) se.synext_notgram
     end
 
 let cache_syntax_extension (_, (_, sy)) =
@@ -1145,7 +1145,7 @@ let find_precedence custom lev etyps symbols onlyprint =
       [],Option.get lev
 
 let check_curly_brackets_notation_exists () =
-  try let _ = Notgram_ops.level_of_notation (InConstrEntrySomeLevel,"{ _ }") in ()
+  try let _ = Notgram_ops.signature_of_notation (InConstrEntrySomeLevel,"{ _ }") in ()
   with Not_found ->
     user_err Pp.(str "Notations involving patterns of the form \"{ _ }\" are treated \n\
 specially and require that the notation \"{ _ }\" is already reserved.")
@@ -1199,11 +1199,11 @@ module SynData = struct
     intern_typs   : notation_var_internalization_type list;
 
     (* Notation data for parsing *)
-    level         : level;
+    ntn_sign       : notation_signature;
     pa_syntax_data : subentry_types * symbol list;
     pp_syntax_data : subentry_types * symbol list;
     not_data      : notation *                   (* notation *)
-                    level *                      (* level, precedence, types *)
+                    notation_signature *         (* level, precedence, types *)
                     bool;                        (* needs_squash *)
   }
 
@@ -1283,7 +1283,7 @@ let compute_syntax_data ~local deprecation df modifiers =
     mainvars;
     intern_typs = i_typs;
 
-    level  = (mods.custom,n,prec,List.map snd sy_typs);
+    ntn_sign  = (mods.custom,n,prec,List.map snd sy_typs);
     pa_syntax_data = pa_sy_data;
     pp_syntax_data = pp_sy_data;
     not_data    = sy_fulldata;
@@ -1387,11 +1387,11 @@ 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
+    let ntn_sign = Notgram_ops.signature_of_notation ~onlyprint:true ntn (* Be as little restrictive as possible *) in
     let pp_rule,_ = find_notation_printing_rule ntn in
     let pp_extra_rules = find_notation_extra_printing_rules ntn in
     let pa_rule = find_notation_parsing_rules ntn in
-    { synext_level = prec;
+    { synext_signature = ntn_sign;
       synext_notation = ntn;
       synext_notgram = pa_rule;
       synext_unparsing = pp_rule;
@@ -1407,11 +1407,11 @@ let recover_squash_syntax sy =
 (**********************************************************************)
 (* Main entry point for building parsing and printing rules           *)
 
-let make_pa_rule level (typs,symbols) ntn need_squash =
+let make_pa_rule ntn_sign (typs,symbols) ntn need_squash =
   let assoc = recompute_assoc typs in
   let prod = make_production typs symbols in
   let sy = {
-    notgram_level = level;
+    notgram_signature = ntn_sign;
     notgram_assoc = assoc;
     notgram_notation = ntn;
     notgram_prods = prod;
@@ -1436,10 +1436,10 @@ let make_pp_rule level (typs,symbols) fmt =
 (* let make_syntax_rules i_typs (ntn,prec,need_squash) sy_data fmt extra onlyprint compat = *)
 let make_syntax_rules (sd : SynData.syn_data) = let open SynData in
   let ntn_for_grammar, prec_for_grammar, need_squash = sd.not_data in
-  let custom,level,_,_ = sd.level in
+  let custom,level,_,_ = sd.ntn_sign in
   let pa_rule = make_pa_rule prec_for_grammar sd.pa_syntax_data ntn_for_grammar need_squash in
   let pp_rule = make_pp_rule level sd.pp_syntax_data sd.format in {
-    synext_level    = sd.level;
+    synext_signature = sd.ntn_sign;
     synext_notation = fst sd.info;
     synext_notgram  = { notgram_onlyprinting = sd.only_printing; notgram_rules = pa_rule };
     synext_unparsing = pp_rule;
@@ -1467,7 +1467,7 @@ let add_notation_in_scope ~local deprecation df env c mods scope =
   let (acvars, ac, reversibility) = interp_notation_constr env nenv c in
   let interp = make_interpretation_vars sd.recvars acvars (fst sd.pa_syntax_data) in
   let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in
-  let onlyparse,coe = printability (Some sd.level) sd.only_parsing reversibility ac in
+  let onlyparse,coe = printability (Some sd.ntn_sign) sd.only_parsing reversibility ac in
   let notation = {
     notobj_local = local;
     notobj_scope = scope;
@@ -1493,8 +1493,8 @@ let add_notation_interpretation_core ~local df env ?(impls=empty_internalization
     let () = Lib.add_anonymous_leaf (inSyntaxExtension (local,sy)) in
     (* If the only printing flag has been explicitly requested, put it back *)
     let onlyprint = onlyprint || sy.synext_notgram.notgram_onlyprinting in
-    let _,_,_,typs = sy.synext_level in
-    Some sy.synext_level, typs, onlyprint
+    let _,_,_,typs = sy.synext_signature in
+    Some sy.synext_signature, typs, onlyprint
   end else None, [], false in
   (* Declare interpretation *)
   let path = (Lib.library_dp(), Lib.current_dirpath true) in