A notation cleanup suggested in coq#17117: using records in place of …

…tuples.

See comment at coq#17117 (comment).

interp/constrexpr.mli

@@ -45,10 +45,17 @@ type entry_relative_level = LevelLt of entry_level | LevelLe of entry_level | Le
 type notation_entry = InConstrEntry | InCustomEntry of string
 
 (* A notation entry with the level where the notation lives *)
-type notation_entry_level = notation_entry * entry_level
+type notation_entry_level = {
+  notation_entry : notation_entry;
+  notation_level : entry_level;
+}
 
 (* Notation subentries, to be associated to the variables of the notation *)
-type notation_entry_relative_level = notation_entry * (entry_relative_level * side option)
+type notation_entry_relative_level = {
+  notation_subentry : notation_entry;
+  notation_relative_level : entry_relative_level;
+  notation_position : side option;
+}
 
 type notation_key = string
 

interp/constrextern.ml

@@ -219,9 +219,11 @@ let rec fill_arg_scopes args subscopes (entry,(_,scopes) as all) =
   | a :: args, [] ->
     (a, (entry, ([], scopes))) :: fill_arg_scopes args [] all
 
-let update_with_subscope ((entry,(lev,side)),(scopt,scl)) scopes =
+let update_with_subscope (entry,(scopt,scl)) scopes =
+  let {notation_subentry = entry; notation_relative_level = lev; notation_position = side} = entry in
   let lev = if !print_parentheses && side <> None then LevelLe 0 (* min level *) else lev in
-  ((entry,(lev,side)),(scopt,scl@scopes))
+  let subentry' = {notation_subentry = entry; notation_relative_level = lev; notation_position = side} in
+  (subentry',(scopt,scl@scopes))
 
 (**********************************************************************)
 (* mapping patterns to cases_pattern_expr                                *)
@@ -334,12 +336,12 @@ let extern_record_pattern cstrsp args =
   with
     Not_found | No_match | Exit -> None
 
- (* Better to use extern_glob_constr composed with injection/retraction ?? *)
+(* Better to use extern_glob_constr composed with injection/retraction ?? *)
 let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
   try
     if !Flags.in_debugger || !Flags.raw_print || !print_raw_literal then raise No_match;
     let (na,p,key) = uninterp_prim_token_cases_pattern pat scopes in
-    match availability_of_entry_coercion custom (InConstrEntry,0) with
+    match availability_of_entry_coercion custom constr_lowest_level with
       | None -> raise No_match
       | Some coercion ->
         let loc = cases_pattern_loc pat in
@@ -356,10 +358,10 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
     | PatVar (Name id) when entry_has_global custom || entry_has_ident custom ->
       CAst.make ?loc (CPatAtom (Some (qualid_of_ident ?loc id)))
     | pat ->
-    match availability_of_entry_coercion custom (InConstrEntry,0) with
+    match availability_of_entry_coercion custom constr_lowest_level with
     | None -> raise No_match
     | Some coercion ->
-      let allscopes = ((InConstrEntry,(LevelSome,None)),scopes) in
+      let allscopes = (constr_some_level,scopes) in
       let pat = match pat with
         | PatVar (Name id) -> CAst.make ?loc (CPatAtom (Some (qualid_of_ident ?loc id)))
         | PatVar (Anonymous) -> CAst.make ?loc (CPatAtom None)
@@ -389,7 +391,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(no_implicit,nb_to_drop
   match rule with
     | NotationRule (_,ntn as specific_ntn) ->
       begin
-        let entry = (fst ntn, pi2 (Notation.level_of_notation ntn)) in
+        let entry = fst (Notation.level_of_notation ntn) in
         match availability_of_entry_coercion custom entry with
         | None -> raise No_match
         | Some coercion ->
@@ -425,7 +427,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(no_implicit,nb_to_drop
                  (make_pat_notation ?loc specific_ntn (l,ll) l2') key)
       end
     | AbbrevRule kn ->
-      match availability_of_entry_coercion custom (InConstrEntry, 0) with
+      match availability_of_entry_coercion custom constr_lowest_level with
       | None -> raise No_match
       | Some coercion ->
       let qid = Nametab.shortest_qualid_of_abbreviation ?loc vars kn in
@@ -493,7 +495,7 @@ let extern_ind_pattern_in_scope (custom,scopes as allscopes) vars ind args =
            |None           -> CAst.make @@ CPatCstr (c, Some args, [])
 
 let extern_cases_pattern vars p =
-  extern_cases_pattern_in_scope ((InConstrEntry,(LevelSome (*??*),None)),([],[])) vars p
+  extern_cases_pattern_in_scope (constr_some_level,([],[])) vars p
 
 (**********************************************************************)
 (* Externalising applications *)
@@ -749,7 +751,7 @@ let same_binder_type ty nal c =
 let extern_possible_prim_token (custom,scopes) r =
    if !print_raw_literal then raise No_match;
    let (n,key) = uninterp_prim_token r scopes in
-   match availability_of_entry_coercion custom (InConstrEntry,0) with
+   match availability_of_entry_coercion custom constr_lowest_level with
    | None -> raise No_match
    | Some coercion ->
       insert_entry_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key)
@@ -889,11 +891,11 @@ let rec extern inctx ?impargs scopes vars r =
 
   | c ->
 
-  match availability_of_entry_coercion (fst scopes) (InConstrEntry,0) with
+  match availability_of_entry_coercion (fst scopes) constr_lowest_level with
   | None -> raise No_match
   | Some coercion ->
 
-  let scopes = ((InConstrEntry,(LevelSome (*??*),None)), snd scopes) in
+  let scopes = (constr_some_level, snd scopes) in
   let c = match c with
 
   (* The remaining cases are only for the constr entry *)
@@ -1222,7 +1224,7 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules =
         (* Try availability of interpretation ... *)
         match keyrule with
           | NotationRule (_,ntn as specific_ntn) ->
-            let entry = (fst ntn, pi2 (Notation.level_of_notation ntn)) in
+            let entry = fst (Notation.level_of_notation ntn) in
              (match availability_of_entry_coercion custom entry with
              | None -> raise No_match
              | Some coercion ->
@@ -1275,7 +1277,7 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules =
               let args = extern_args (extern true) (vars,uvars) args in
               let c = CAst.make ?loc @@ extern_applied_abbreviation inctx nallargs argsimpls (a,cf) l args in
               if isCRef_no_univ c.CAst.v && entry_has_global custom then c
-             else match availability_of_entry_coercion custom (InConstrEntry,0) with
+             else match availability_of_entry_coercion custom constr_lowest_level with
              | None -> raise No_match
              | Some coercion -> insert_entry_coercion coercion c
       with
@@ -1294,10 +1296,10 @@ and extern_applied_proj inctx scopes vars (cst,us) params c extraargs =
   extern_projection inctx (f,us) nparams args imps
 
 let extern_glob_constr vars c =
-  extern false ((InConstrEntry,(LevelSome,None)),([],[])) vars c
+  extern false (constr_some_level,([],[])) vars c
 
 let extern_glob_type ?impargs vars c =
-  extern_typ ?impargs ((InConstrEntry,(LevelSome,None)),([],[])) vars c
+  extern_typ ?impargs (constr_some_level,([],[])) vars c
 
 (******************************************************************)
 (* Main translation function from constr -> constr_expr *)
@@ -1306,7 +1308,7 @@ let extern_constr ?(inctx=false) ?scope env sigma t =
   let r = Detyping.detype Detyping.Later Id.Set.empty env sigma t in
   let vars = extern_env env sigma in
   let scope = Option.cata (fun x -> [x]) [] scope in
-  extern inctx ((InConstrEntry,(LevelSome,None)),(scope,[])) vars r
+  extern inctx (constr_some_level,(scope,[])) vars r
 
 let extern_constr_in_scope ?inctx scope env sigma t =
   extern_constr ?inctx ~scope env sigma t
@@ -1332,7 +1334,7 @@ let extern_closed_glob ?(goal_concl_style=false) ?(inctx=false) ?scope env sigma
   in
   let vars = extern_env env sigma in
   let scope = Option.cata (fun x -> [x]) [] scope in
-  extern inctx ((InConstrEntry,(LevelSome,None)),(scope,[])) vars r
+  extern inctx (constr_some_level,(scope,[])) vars r
 
 (******************************************************************)
 (* Main translation function from pattern -> constr_expr *)
@@ -1474,7 +1476,7 @@ and glob_of_pat_under_context avoid env sigma (nas, pat) =
   (Array.rev_of_list nas, pat)
 
 let extern_constr_pattern env sigma pat =
-  extern true ((InConstrEntry,(LevelSome,None)),([],[]))
+  extern true (constr_some_level,([],[]))
     (* XXX no vars? *)
     (Id.Set.empty, Evd.universe_binders sigma)
     (glob_of_pat Id.Set.empty env sigma pat)
@@ -1483,4 +1485,4 @@ let extern_rel_context where env sigma sign =
   let a = detype_rel_context Detyping.Later where Id.Set.empty (names_of_rel_context env,env) sigma sign in
   let vars = extern_env env sigma in
   let a = List.map (extended_glob_local_binder_of_decl) a in
-  pi3 (extern_local_binder ((InConstrEntry,(LevelSome,None)),([],[])) vars a)
+  pi3 (extern_local_binder (constr_some_level,([],[])) vars a)

interp/notation.ml

@@ -1543,21 +1543,27 @@ let sublevel_ord lev lev' =
   | LevelLt n, LevelLe n' -> n < n'
   | LevelLe n, LevelLt n' -> n <= n'-1
 
-let is_coercion (e1,n1) (e2,(n2,_)) =
+let is_coercion
+    { notation_entry = e1; notation_level = n1 }
+    { notation_subentry = e2; notation_relative_level = n2 } =
   not (notation_entry_eq e1 e2) ||
   match n2 with
   | LevelLt n2 | LevelLe n2 -> n1 < n2
   | LevelSome -> true (* unless n2 is the entry top level but we shall know it only dynamically *)
 
-let included (e1,n1) (e2,(n2,_)) =
+let included
+    { notation_entry = e1; notation_level = n1 }
+    { notation_subentry = e2; notation_relative_level = n2 } =
   notation_entry_eq e1 e2 && entry_relative_level_le n1 n2
 
 let rec search nfrom nto = function
   | [] -> raise Not_found
   | ((pfrom,pto),coe)::l ->
     if entry_relative_level_le pfrom nfrom && entry_relative_level_le nto pto then coe else search nfrom nto l
 
-let availability_of_entry_coercion (entry,(sublev,_) as entry_sublev) (entry',lev' as entry_lev) =
+let availability_of_entry_coercion
+    ({ notation_subentry = entry; notation_relative_level = sublev } as entry_sublev)
+    ({ notation_entry = entry'; notation_level = lev' } as entry_lev) =
   if included entry_lev entry_sublev then
     (* [entry] is by default included in [relative_entry] *)
     Some []
@@ -1578,21 +1584,23 @@ let rec insert_coercion_path path = function
       else path'::insert_coercion_path path paths
 
 let declare_entry_coercion ntn entry_level entry_relative_level' =
-  let entry, lev = entry_level in
-  let entry', (sublev',_) = entry_relative_level' in
+  let { notation_entry = entry; notation_level = lev } = entry_level in
+  let { notation_subentry = entry'; notation_relative_level = sublev' } = entry_relative_level' in
   (* Transitive closure *)
   let toaddleft =
     EntryCoercionMap.fold (fun (entry'',entry''') paths l ->
         List.fold_right (fun ((lev'',sublev'''),path) l ->
-        if included entry_level (entry''',(sublev''',None)) &&
-           not (included (entry'',lev'') entry_relative_level')
+            if included entry_level
+                { notation_subentry = entry'''; notation_relative_level = sublev'''; notation_position = None } &&
+               not (included { notation_entry = entry''; notation_level = lev'' } entry_relative_level')
         then ((entry'',entry'),((lev'',sublev'),path@[ntn]))::l else l) paths l)
       !entry_coercion_map [] in
   let toaddright =
     EntryCoercionMap.fold (fun (entry'',entry''') paths l ->
         List.fold_right (fun ((lev'',sublev'''),path) l ->
-        if included (entry'',lev'') entry_relative_level' &&
-           not (included entry_level (entry''',(sublev''',None)))
+        if included { notation_entry = entry''; notation_level = lev'' } entry_relative_level' &&
+           not (included entry_level
+                  { notation_subentry = entry'''; notation_relative_level = sublev'''; notation_position = None })
         then ((entry,entry'''),((lev,sublev'''),path@[ntn]))::l else l) paths l)
       !entry_coercion_map [] in
   entry_coercion_map :=
@@ -1615,9 +1623,10 @@ let declare_custom_entry_has_global s n =
   with Not_found ->
     entry_has_global_map := String.Map.add s n !entry_has_global_map
 
-let entry_has_global = function
-  | InConstrEntry, _ -> true
-  | InCustomEntry s, (n,_) ->
+let entry_has_global { notation_subentry = entry; notation_relative_level = n } =
+  match entry with
+  | InConstrEntry -> true
+  | InCustomEntry s ->
      try entry_relative_level_le (String.Map.find s !entry_has_global_map) n with Not_found -> false
 
 let entry_has_ident_map = ref String.Map.empty
@@ -1630,9 +1639,10 @@ let declare_custom_entry_has_ident s n =
   with Not_found ->
     entry_has_ident_map := String.Map.add s n !entry_has_ident_map
 
-let entry_has_ident = function
-  | InConstrEntry, _ -> true
-  | InCustomEntry s, (n,_) ->
+let entry_has_ident { notation_subentry = entry; notation_relative_level = n } =
+  match entry with
+  | InConstrEntry -> true
+  | InCustomEntry s ->
      try entry_relative_level_le (String.Map.find s !entry_has_ident_map) n with Not_found -> false
 
 type entry_coercion_kind =
@@ -2002,7 +2012,7 @@ let is_numeral_in_constr (entry,symbs) =
 let level_of_notation ntn =
   if is_numeral_in_constr (decompose_notation_key ntn) then
     (* A primitive notation *)
-    (fst ntn, 0, []) (* TODO: string notations*)
+    ({ notation_entry = fst ntn; notation_level = 0}, []) (* TODO: string notations*)
   else
     NotationMap.find ntn !notation_level_map
 

interp/notation_ops.ml

@@ -21,6 +21,14 @@ open Glob_ops
 open Mod_subst
 open Notation_term
 
+(** Constr default entry *)
+
+let constr_lowest_level =
+  Constrexpr.{notation_entry = InConstrEntry; notation_level = 0}
+
+let constr_some_level =
+  Constrexpr.{notation_subentry = InConstrEntry; notation_relative_level = LevelSome; notation_position = None}
+
 (**********************************************************************)
 (* Utilities                                                          *)
 
@@ -1309,11 +1317,9 @@ let remove_sigma x (terms,termlists,binders,binderlists) =
 let remove_bindinglist_sigma x (terms,termlists,binders,binderlists) =
   (terms,termlists,binders,Id.List.remove_assoc x binderlists)
 
-let default_constr_entry_relative_level = Constrexpr.(InConstrEntry,(LevelSome,None))
-
-let add_ldots_var metas = (ldots_var,((default_constr_entry_relative_level,([],[])),NtnTypeConstr))::metas
+let add_ldots_var metas = (ldots_var,((constr_some_level,([],[])),NtnTypeConstr))::metas
 
-let add_meta_bindinglist x metas = (x,((default_constr_entry_relative_level,([],[])),NtnTypeBinderList (*arbitrary:*) NtnBinderParsedAsBinder))::metas
+let add_meta_bindinglist x metas = (x,((constr_some_level,([],[])),NtnTypeBinderList (*arbitrary:*) NtnBinderParsedAsBinder))::metas
 
 (* This tells if letins in the middle of binders should be included in
    the sequence of binders *)
@@ -1359,7 +1365,7 @@ let match_binderlist match_iter_fun match_termin_fun alp metas sigma rest x y it
   let alp,sigma = bind_bindinglist_env alp sigma x bl in
   match_termin_fun alp metas sigma rest termin
 
-let add_meta_term x metas = (x,((default_constr_entry_relative_level,([],[])),NtnTypeConstr))::metas (* Should reuse the scope of the partner of x! *)
+let add_meta_term x metas = (x,((constr_some_level,([],[])),NtnTypeConstr))::metas (* Should reuse the scope of the partner of x! *)
 
 let match_termlist match_fun alp metas sigma rest x y iter termin revert =
   let rec aux alp sigma acc rest =

interp/notation_ops.mli

@@ -12,6 +12,14 @@ open Names
 open Notation_term
 open Glob_term
 
+(** Constr default entries *)
+
+(* Equivalent to an entry "in constr at level 0"; used for coercion to constr *)
+val constr_lowest_level : Constrexpr.notation_entry_level
+
+(* Equivalent to "x constr" in a subentry, at highest level *)
+val constr_some_level : Constrexpr.notation_entry_relative_level
+
 (** {5 Utilities about [notation_constr]} *)
 
 val eq_notation_constr : Id.t list * Id.t list -> notation_constr -> notation_constr -> bool

interp/notationextern.ml

@@ -36,10 +36,14 @@ let notation_entry_eq s1 s2 = match (s1,s2) with
   | InCustomEntry s1, InCustomEntry s2 -> String.equal s1 s2
   | (InConstrEntry | InCustomEntry _), _ -> false
 
-let notation_entry_level_eq (e1,n1) (e2,n2) =
+let notation_entry_level_eq
+    { notation_entry = e1; notation_level = n1 }
+    { notation_entry = e2; notation_level = n2 } =
   notation_entry_eq e1 e2 && Int.equal n1 n2
 
-let notation_entry_relative_level_eq (e1,(n1,s1)) (e2,(n2,s2)) =
+let notation_entry_relative_level_eq
+    { notation_subentry = e1; notation_relative_level = n1; notation_position = s1 }
+    { notation_subentry = e2; notation_relative_level = n2; notation_position = s2 } =
   notation_entry_eq e1 e2 && entry_relative_level_eq n1 n2 && s1 = s2
 
 let notation_eq (from1,ntn1) (from2,ntn2) =
@@ -77,13 +81,12 @@ let interpretation_eq (vars1, t1 as x1) (vars2, t2 as x2) =
   List.equal var_attributes_eq vars1 vars2 &&
   Notation_ops.eq_notation_constr (List.map fst vars1, List.map fst vars2) t1 t2
 
-type level = notation_entry * entry_level * entry_relative_level list
-  (* first argument is InCustomEntry s for custom entries *)
+type level = notation_entry_level * entry_relative_level list
 
-let level_eq (s1, l1, t1) (s2, l2, t2) =
+let level_eq ({ notation_entry = s1; notation_level = l1}, t1) ({ notation_entry = s2; notation_level = l2}, t2) =
   notation_entry_eq s1 s2 && Int.equal l1 l2 && List.equal entry_relative_level_eq t1 t2
 
-(* Uninterpretation tables *)
+(** Uninterpretation tables *)
 
 type 'a interp_rule_gen =
   | NotationRule of Constrexpr.specific_notation

interp/notationextern.mli

@@ -30,8 +30,8 @@ val interpretation_eq : interpretation -> interpretation -> bool
 val notation_entry_level_eq : notation_entry_level -> notation_entry_level -> bool
 (** Equality on [notation_entry_level]. *)
 
-type level = notation_entry * entry_level * entry_relative_level list
-  (* first argument is InCustomEntry s for custom entries *)
+type level = notation_entry_level * entry_relative_level list
+(** The "signature" of a rule: its level together with the levels of its subentries *)
 
 val level_eq : level -> level -> bool
 (** Equality on [level]. *)