Clarifying the logic of levels in custom and constr entry rules (reopening of #13025)

dev/ci/user-overlays/17117-master+fix-printing-custom-no-level.sh

@@ -0,0 +1,2 @@
+overlay elpi https://github.com/herbelin/coq-elpi coq-master+adapt-coq-pr13025-fix-custom-entry-no-level-printing 17117 master+fix-printing-custom-no-level
+overlay serapi https://github.com/herbelin/coq-serapi main+adapt-coq-pr17117-renamings 17117 master+fix-printing-custom-no-level

dev/doc/changes.md

@@ -144,6 +144,15 @@ deprecation warning tells what to do.
   defined level with the provided rules. Note that this differs from FIRST,
   which creates a new level and prepends it to the list of levels of the entry.
 
+### Notations:
+
+- The type `notation_entry_level` has been split into two: the name
+  `notation_entry_level` still exists and is used to characterize the
+  level and custom entry name (if any) where a grammar rule lives; the
+  new `notation_subentry_level` is to characterize the level (possibly
+  none) and custom entry name associated to the variables (=
+  non-terminal subentries) of the grammar rule.
+
 ## Changes between Coq 8.12 and Coq 8.13
 
 ### Code formatting

doc/changelog/03-notations/17117-master+fix-printing-custom-no-level.rst

@@ -0,0 +1,4 @@
+- **Added:**
+  Support for :flag:`Printing Parentheses` in custom notations
+  (`#17117 <https://github.com/coq/coq/pull/17117>`_, by Hugo
+  Herbelin).

interp/constrexpr.mli

@@ -37,11 +37,19 @@ type name_decl = lname * universe_decl_expr option
 
 type notation_with_optional_scope = LastLonelyNotation | NotationInScope of string
 
+type side = Left | Right
 type entry_level = int
 type entry_relative_level = LevelLt of entry_level | LevelLe of entry_level | LevelSome
 
+(* The entry in which a notation is declared *)
 type notation_entry = InConstrEntry | InCustomEntry of string
-type notation_entry_level = InConstrEntrySomeLevel | InCustomEntryLevel of string * entry_level
+
+(* A notation entry with the level where the notation lives *)
+type notation_entry_level = notation_entry * 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_key = string
 
 (* A notation associated to a given parsing rule *)

interp/constrexpr_ops.ml

@@ -15,7 +15,7 @@ open Nameops
 open Libnames
 open Namegen
 open Glob_term
-open Notation
+open Notationextern
 open Constrexpr
 
 (***********)

interp/constrextern.ml

@@ -221,6 +221,10 @@ 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 lev = if !print_parentheses && side <> None then LevelLe 0 (* min level *) else lev in
+  ((entry,(lev,side)),(scopt,scl@scopes))
+
 (**********************************************************************)
 (* mapping patterns to cases_pattern_expr                                *)
 
@@ -337,7 +341,7 @@ 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 InConstrEntrySomeLevel with
+    match availability_of_entry_coercion custom (InConstrEntry,0) with
       | None -> raise No_match
       | Some coercion ->
         let loc = cases_pattern_loc pat in
@@ -354,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 InConstrEntrySomeLevel with
+    match availability_of_entry_coercion custom (InConstrEntry,0) with
     | None -> raise No_match
     | Some coercion ->
-      let allscopes = (InConstrEntrySomeLevel,scopes) in
+      let allscopes = ((InConstrEntry,(LevelSome,None)),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)
@@ -383,17 +387,12 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
       insert_pat_coercion coercion pat
 
 and apply_notation_to_pattern ?loc gr ((subst,substlist),(no_implicit,nb_to_drop,more_args))
-    (custom, (tmp_scope, scopes) as allscopes) vars =
-  function
+    (custom, (tmp_scope, scopes) as allscopes) vars rule =
+  match rule with
     | NotationRule (_,ntn as specific_ntn) ->
       begin
-        let notation_entry_level = match (fst ntn) with
-          | InConstrEntry -> InConstrEntrySomeLevel
-          | InCustomEntry s ->
-            let (_,level,_) = Notation.level_of_notation ntn in
-            InCustomEntryLevel (s, level)
-        in
-        match availability_of_entry_coercion custom notation_entry_level with
+        let entry = (fst ntn, pi2 (Notation.level_of_notation ntn)) in
+        match availability_of_entry_coercion custom entry with
         | None -> raise No_match
         | Some coercion ->
         match availability_of_notation specific_ntn (tmp_scope,scopes) with
@@ -403,13 +402,14 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(no_implicit,nb_to_drop
           | Some (scopt,key) ->
             let scopes' = Option.List.cons scopt scopes in
             let l =
-              List.map (fun (c,(subentry,(scopt,scl))) ->
-                extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes')) vars c)
+              List.map (fun (c,subscope) ->
+                let scopes = update_with_subscope subscope scopes' in
+                extern_cases_pattern_in_scope scopes vars c)
                 subst in
             let ll =
-              List.map (fun (c,(subentry,(scopt,scl))) ->
-                let subscope = (subentry,(scopt,scl@scopes')) in
-                List.map (extern_cases_pattern_in_scope subscope vars) c)
+              List.map (fun (c,subscope) ->
+                let scopes = update_with_subscope subscope scopes' in
+                List.map (extern_cases_pattern_in_scope scopes vars) c)
                 substlist in
             let subscopes = find_arguments_scope gr in
             let more_args_scopes = try List.skipn nb_to_drop subscopes with Failure _ -> [] in
@@ -427,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 InConstrEntrySomeLevel with
+      match availability_of_entry_coercion custom (InConstrEntry, 0) with
       | None -> raise No_match
       | Some coercion ->
       let qid = Nametab.shortest_qualid_of_abbreviation ?loc vars kn in
@@ -495,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 (InConstrEntrySomeLevel,([],[])) vars p
+  extern_cases_pattern_in_scope ((InConstrEntry,(LevelSome (*??*),None)),([],[])) vars p
 
 (**********************************************************************)
 (* Externalising applications *)
@@ -751,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 InConstrEntrySomeLevel with
+   match availability_of_entry_coercion custom (InConstrEntry,0) with
    | None -> raise No_match
    | Some coercion ->
       insert_entry_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key)
@@ -891,11 +891,11 @@ let rec extern inctx ?impargs scopes vars r =
 
   | c ->
 
-  match availability_of_entry_coercion (fst scopes) InConstrEntrySomeLevel with
+  match availability_of_entry_coercion (fst scopes) (InConstrEntry,0) with
   | None -> raise No_match
   | Some coercion ->
 
-  let scopes = (InConstrEntrySomeLevel, snd scopes) in
+  let scopes = ((InConstrEntry,(LevelSome (*??*),None)), snd scopes) in
   let c = match c with
 
   (* The remaining cases are only for the constr entry *)
@@ -1224,13 +1224,8 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules =
         (* Try availability of interpretation ... *)
         match keyrule with
           | NotationRule (_,ntn as specific_ntn) ->
-            let notation_entry_level = match (fst ntn) with
-              | InConstrEntry -> InConstrEntrySomeLevel
-              | InCustomEntry s ->
-                let (_,level,_) = Notation.level_of_notation ntn in
-                InCustomEntryLevel (s, level)
-             in
-             (match availability_of_entry_coercion custom notation_entry_level with
+            let entry = (fst ntn, pi2 (Notation.level_of_notation ntn)) in
+             (match availability_of_entry_coercion custom entry with
              | None -> raise No_match
              | Some coercion ->
                match availability_of_notation specific_ntn scopes with
@@ -1240,28 +1235,29 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules =
               | Some (scopt,key) ->
                   let scopes' = Option.List.cons scopt (snd scopes) in
                   let l =
-                    List.map (fun ((vars,c),(subentry,(scopt,scl))) ->
-                      extern (* assuming no overloading: *) true
-                        (subentry,(scopt,scl@scopes')) (vars,uvars) c)
+                    List.map (fun ((vars,c),subscope) ->
+                      let scopes = update_with_subscope subscope scopes' in
+                      extern (* assuming no overloading: *) true scopes (vars,uvars) c)
                       terms
                   in
                   let ll =
-                    List.map (fun ((vars,l),(subentry,(scopt,scl))) ->
-                      List.map (extern true (subentry,(scopt,scl@scopes')) (vars,uvars)) l)
+                    List.map (fun ((vars,l),subscope) ->
+                      let scopes = update_with_subscope subscope scopes' in
+                      List.map (extern true scopes (vars,uvars)) l)
                       termlists
                   in
                   let bl =
-                    List.map (fun ((vars,bl),(subentry,(scopt,scl))) ->
+                    List.map (fun ((vars,bl),subscope) ->
+                      let scopes = update_with_subscope subscope scopes' in
                         (mkCPatOr (List.map
-                                     (extern_cases_pattern_in_scope
-                                        (subentry,(scopt,scl@scopes')) vars)
-                                     bl)),
+                                     (extern_cases_pattern_in_scope scopes vars) bl)),
                         Explicit)
                       binders
                   in
                   let bll =
-                    List.map (fun ((vars,bl),(subentry,(scopt,scl))) ->
-                      pi3 (extern_local_binder (subentry,(scopt,scl@scopes')) (vars,uvars) bl))
+                    List.map (fun ((vars,bl),subscope) ->
+                      let scopes = update_with_subscope subscope scopes' in
+                      pi3 (extern_local_binder scopes (vars,uvars) bl))
                       binderlists
                   in
                   let c = make_notation loc specific_ntn (l,ll,bl,bll) in
@@ -1281,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 InConstrEntrySomeLevel with
+             else match availability_of_entry_coercion custom (InConstrEntry,0) with
              | None -> raise No_match
              | Some coercion -> insert_entry_coercion coercion c
       with
@@ -1300,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 (InConstrEntrySomeLevel,([],[])) vars c
+  extern false ((InConstrEntry,(LevelSome,None)),([],[])) vars c
 
 let extern_glob_type ?impargs vars c =
-  extern_typ ?impargs (InConstrEntrySomeLevel,([],[])) vars c
+  extern_typ ?impargs ((InConstrEntry,(LevelSome,None)),([],[])) vars c
 
 (******************************************************************)
 (* Main translation function from constr -> constr_expr *)
@@ -1312,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 (InConstrEntrySomeLevel,(scope,[])) vars r
+  extern inctx ((InConstrEntry,(LevelSome,None)),(scope,[])) vars r
 
 let extern_constr_in_scope ?inctx scope env sigma t =
   extern_constr ?inctx ~scope env sigma t
@@ -1338,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 (InConstrEntrySomeLevel,(scope,[])) vars r
+  extern inctx ((InConstrEntry,(LevelSome,None)),(scope,[])) vars r
 
 (******************************************************************)
 (* Main translation function from pattern -> constr_expr *)
@@ -1480,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 (InConstrEntrySomeLevel,([],[]))
+  extern true ((InConstrEntry,(LevelSome,None)),([],[]))
     (* XXX no vars? *)
     (Id.Set.empty, Evd.universe_binders sigma)
     (glob_of_pat Id.Set.empty env sigma pat)
@@ -1489,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 (InConstrEntrySomeLevel,([],[])) vars a)
+  pi3 (extern_local_binder ((InConstrEntry,(LevelSome,None)),([],[])) vars a)