Fix #11121: Simultaneous definition of term and notation in custom grammar

7 files changed, 99 insertions, 39 deletions

diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index 21f682ac0e..9c4b78f4ed 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -29,10 +29,10 @@ type notation_entry_level = InConstrEntrySomeLevel | InCustomEntryLevel of strin
 type notation_key = string
 
 (* A notation associated to a given parsing rule *)
-type notation = notation_entry_level * notation_key
+type notation = notation_entry * notation_key
 
 (* A notation associated to a given interpretation *)
-type specific_notation = notation_with_optional_scope * notation
+type specific_notation = notation_with_optional_scope * (notation_entry * notation_key)
 
 type 'a or_by_notation_r =
   | AN of 'a
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 63079993c8..b087431e85 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -359,14 +359,14 @@ let make_notation_gen loc ntn mknot mkprim destprim l bl =
     (* Special case to avoid writing "- 3" for e.g. (Z.opp 3) *)
     | "- _", [Some (Numeral p)] when not (NumTok.Signed.is_zero p) ->
         assert (bl=[]);
-        mknot (loc,ntn,([mknot (loc,(InConstrEntrySomeLevel,"( _ )"),l,[])]),[])
+        mknot (loc,ntn,([mknot (loc,(InConstrEntry,"( _ )"),l,[])]),[])
     | _ ->
         match decompose_notation_key ntn, l with
-        | (InConstrEntrySomeLevel,[Terminal "-"; Terminal x]), [] ->
+        | (InConstrEntry,[Terminal "-"; Terminal x]), [] ->
            begin match NumTok.Unsigned.parse_string x with
            | Some n -> mkprim (loc, Numeral (NumTok.SMinus,n))
            | None -> mknot (loc,ntn,l,bl) end
-        | (InConstrEntrySomeLevel,[Terminal x]), [] ->
+        | (InConstrEntry,[Terminal x]), [] ->
            begin match NumTok.Unsigned.parse_string x with
            | Some n -> mkprim (loc, Numeral (NumTok.SPlus,n))
            | None -> mknot (loc,ntn,l,bl) end
@@ -486,7 +486,13 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(no_implicit,nb_to_drop
   function
     | NotationRule (_,ntn as specific_ntn) ->
       begin
-        match availability_of_entry_coercion custom (fst ntn) with
+        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
         | None -> raise No_match
         | Some coercion ->
         match availability_of_notation specific_ntn (tmp_scope,scopes) with
@@ -1260,7 +1266,13 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
         (* Try availability of interpretation ... *)
         match keyrule with
           | NotationRule (_,ntn as specific_ntn) ->
-             (match availability_of_entry_coercion custom (fst ntn) with
+            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
              | None -> raise No_match
              | Some coercion ->
                match availability_of_notation specific_ntn scopes with
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index ee041ed088..d95554de56 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -224,35 +224,35 @@ let expand_notation_string ntn n =
 (* Remark: expansion of squash at definition is done in metasyntax.ml *)
 let contract_curly_brackets ntn (l,ll,bl,bll) =
   match ntn with
-  | InCustomEntryLevel _,_ -> ntn,(l,ll,bl,bll)
-  | InConstrEntrySomeLevel, ntn ->
+  | InCustomEntry _,_ -> ntn,(l,ll,bl,bll)
+  | InConstrEntry, ntn ->
   let ntn' = ref ntn in
   let rec contract_squash n = function
     | [] -> []
-    | { CAst.v = CNotation (None,(InConstrEntrySomeLevel,"{ _ }"),([a],[],[],[])) } :: l ->
+    | { CAst.v = CNotation (None,(InConstrEntry,"{ _ }"),([a],[],[],[])) } :: l ->
         ntn' := expand_notation_string !ntn' n;
         contract_squash n (a::l)
     | a :: l ->
         a::contract_squash (n+1) l in
   let l = contract_squash 0 l in
   (* side effect; don't inline *)
-  (InConstrEntrySomeLevel,!ntn'),(l,ll,bl,bll)
+  (InConstrEntry,!ntn'),(l,ll,bl,bll)
 
 let contract_curly_brackets_pat ntn (l,ll) =
   match ntn with
-  | InCustomEntryLevel _,_ -> ntn,(l,ll)
-  | InConstrEntrySomeLevel, ntn ->
+  | InCustomEntry _,_ -> ntn,(l,ll)
+  | InConstrEntry, ntn ->
   let ntn' = ref ntn in
   let rec contract_squash n = function
     | [] -> []
-    | { CAst.v = CPatNotation (None,(InConstrEntrySomeLevel,"{ _ }"),([a],[]),[]) } :: l ->
+    | { CAst.v = CPatNotation (None,(InConstrEntry,"{ _ }"),([a],[]),[]) } :: l ->
         ntn' := expand_notation_string !ntn' n;
         contract_squash n (a::l)
     | a :: l ->
         a::contract_squash (n+1) l in
   let l = contract_squash 0 l in
   (* side effect; don't inline *)
-  (InConstrEntrySomeLevel,!ntn'),(l,ll)
+  (InConstrEntry,!ntn'),(l,ll)
 
 type intern_env = {
   ids: Names.Id.Set.t;
@@ -1688,11 +1688,11 @@ let drop_notations_pattern looked_for genv =
         (* but not scopes in expl_pl *)
         let (argscs1,_) = find_remaining_scopes expl_pl pl g in
         DAst.make ?loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, [])
-    | CPatNotation (_,(InConstrEntrySomeLevel,"- _"),([a],[]),[]) when is_non_zero_pat a ->
+    | CPatNotation (_,(InConstrEntry,"- _"),([a],[]),[]) when is_non_zero_pat a ->
       let p = match a.CAst.v with CPatPrim (Numeral (_, p)) -> p | _ -> assert false in
       let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Numeral (SMinus,p)) scopes in
       rcp_of_glob scopes pat
-    | CPatNotation (_,(InConstrEntrySomeLevel,"( _ )"),([a],[]),[]) ->
+    | CPatNotation (_,(InConstrEntry,"( _ )"),([a],[]),[]) ->
       in_pat top scopes a
     | CPatNotation (_,ntn,fullargs,extrargs) ->
       let ntn,(terms,termlists) = contract_curly_brackets_pat ntn fullargs in
@@ -2006,10 +2006,10 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
         DAst.make ?loc @@
         GLetIn (na.CAst.v, inc1, int,
           intern_restart_binders (push_name_env ntnvars (impls_term_list 1 inc1) env na) c2)
-    | CNotation (_,(InConstrEntrySomeLevel,"- _"), ([a],[],[],[])) when is_non_zero a ->
+    | CNotation (_,(InConstrEntry,"- _"), ([a],[],[],[])) when is_non_zero a ->
       let p = match a.CAst.v with CPrim (Numeral (_, p)) -> p | _ -> assert false in
        intern env (CAst.make ?loc @@ CPrim (Numeral (SMinus,p)))
-    | CNotation (_,(InConstrEntrySomeLevel,"( _ )"),([a],[],[],[])) -> intern env a
+    | CNotation (_,(InConstrEntry,"( _ )"),([a],[],[],[])) -> intern env a
     | CNotation (_,ntn,args) ->
         let c = intern_notation intern env ntnvars loc ntn args in
         let x, impl, scopes = find_appl_head_data c in
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 57ec708b07..d57c05788d 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -207,7 +207,7 @@ let cook_notation (from,df) sc =
   done;
   let df = Bytes.sub_string ntn 0 !j in
   let df_sc = match sc with Some sc -> ":" ^ sc ^ ":" ^ df | _ -> "::" ^ df in
-  let from_df_sc = match from with Constrexpr.InCustomEntryLevel (from,_) -> ":" ^ from ^ df_sc | Constrexpr.InConstrEntrySomeLevel -> ":" ^ df_sc in
+  let from_df_sc = match from with Constrexpr.InCustomEntry from -> ":" ^ from ^ df_sc | Constrexpr.InConstrEntry -> ":" ^ df_sc in
   from_df_sc
 
 let dump_notation_location posl df (((path,secpath),_),sc) =
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 3d29da025e..4016a3600e 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -92,7 +92,7 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l =
   let rec aux bdvars l c = match CAst.(c.v) with
     | CRef (qid,_) when qualid_is_ident qid ->
       found c.CAst.loc (qualid_basename qid) bdvars l
-    | CNotation (_,(InConstrEntrySomeLevel,"{ _ : _ | _ }"), ({ CAst.v = CRef (qid,_) } :: _, [], [], [])) when
+    | CNotation (_,(InConstrEntry,"{ _ : _ | _ }"), ({ CAst.v = CRef (qid,_) } :: _, [], [], [])) when
         qualid_is_ident qid && not (Id.Set.mem (qualid_basename qid) bdvars) ->
         Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add (qualid_basename qid) bdvars) l c
     | _ -> Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c
diff --git a/interp/notation.ml b/interp/notation.ml
index d4a44d9622..e282d62396 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -56,9 +56,9 @@ let notation_with_optional_scope_eq inscope1 inscope2 = match (inscope1,inscope2
  | (LastLonelyNotation | NotationInScope _), _ -> false
 
 let notation_eq (from1,ntn1) (from2,ntn2) =
-  notation_entry_level_eq from1 from2 && String.equal ntn1 ntn2
+  notation_entry_eq from1 from2 && String.equal ntn1 ntn2
 
-let pr_notation (from,ntn) = qstring ntn ++ match from with InConstrEntrySomeLevel -> mt () | InCustomEntryLevel (s,n) -> str " in custom " ++ str s
+let pr_notation (from,ntn) = qstring ntn ++ match from with InConstrEntry -> mt () | InCustomEntry s -> str " in custom " ++ str s
 
 module NotationOrd =
   struct
@@ -337,6 +337,33 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
   | NApp (_,args) -> Oth, Some (List.length args)
   | _ -> Oth, None
 
+(** Dealing with precedences *)
+
+type level = notation_entry * entry_level * entry_relative_level list
+  (* first argument is InCustomEntry s for custom entries *)
+
+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 level_eq (s1, l1, t1) (s2, l2, t2) =
+  notation_entry_eq s1 s2 && Int.equal l1 l2 && List.equal entry_relative_level_eq t1 t2
+
+let notation_level_map = Summary.ref ~name:"notation_level_map" NotationMap.empty
+
+let declare_notation_level ntn level =
+  try
+    let _ = NotationMap.find ntn !notation_level_map in
+    anomaly (str "Notation " ++ pr_notation ntn ++ str " is already assigned a level.")
+  with Not_found ->
+  notation_level_map := NotationMap.add ntn level !notation_level_map
+
+let level_of_notation ntn =
+  NotationMap.find ntn !notation_level_map
+
+
 (**********************************************************************)
 (* Interpreting numbers (not in summary because functional objects)   *)
 
@@ -1228,8 +1255,8 @@ let find_notation ntn sc =
   NotationMap.find ntn (find_scope sc).notations
 
 let notation_of_prim_token = function
-  | Constrexpr.Numeral (SPlus,n) -> InConstrEntrySomeLevel, NumTok.Unsigned.sprint n
-  | Constrexpr.Numeral (SMinus,n) -> InConstrEntrySomeLevel, "- "^NumTok.Unsigned.sprint n
+  | Constrexpr.Numeral (SPlus,n) -> InConstrEntry, NumTok.Unsigned.sprint n
+  | Constrexpr.Numeral (SMinus,n) -> InConstrEntry, "- "^NumTok.Unsigned.sprint n
   | String _ -> raise Not_found
 
 let find_prim_token check_allowed ?loc p sc =
@@ -1256,7 +1283,7 @@ let find_prim_token check_allowed ?loc p sc =
 
 let interp_prim_token_gen ?loc g p local_scopes =
   let scopes = make_current_scopes local_scopes in
-  let p_as_ntn = try notation_of_prim_token p with Not_found -> InConstrEntrySomeLevel,"" in
+  let p_as_ntn = try notation_of_prim_token p with Not_found -> InConstrEntry,"" in
   try
     let (pat,loc), sc = find_interpretation p_as_ntn (find_prim_token ?loc g p) scopes in
     pat, (loc,sc)
@@ -1336,7 +1363,8 @@ module EntryCoercionOrd =
 
 module EntryCoercionMap = Map.Make(EntryCoercionOrd)
 
-let entry_coercion_map = ref EntryCoercionMap.empty
+let entry_coercion_map : (((entry_level option * entry_level option) * entry_coercion) list EntryCoercionMap.t) ref =
+  ref EntryCoercionMap.empty
 
 let level_ord lev lev' =
   match lev, lev' with
@@ -1349,13 +1377,18 @@ let rec search nfrom nto = function
   | ((pfrom,pto),coe)::l ->
     if level_ord pfrom nfrom && level_ord nto pto then coe else search nfrom nto l
 
-let decompose_custom_entry = function
+let make_notation_entry_level entry level =
+  match entry with
+  | InConstrEntry -> InConstrEntrySomeLevel
+  | InCustomEntry s -> InCustomEntryLevel (s,level)
+
+let decompose_notation_entry_level = function
   | InConstrEntrySomeLevel -> InConstrEntry, None
   | InCustomEntryLevel (s,n) -> InCustomEntry s, Some n
 
 let availability_of_entry_coercion entry entry' =
-  let entry, lev = decompose_custom_entry entry in
-  let entry', lev' = decompose_custom_entry entry' in
+  let entry, lev = decompose_notation_entry_level entry in
+  let entry', lev' = decompose_notation_entry_level entry' in
   if notation_entry_eq entry entry' && level_ord lev' lev then Some []
   else
     try Some (search lev lev' (EntryCoercionMap.find (entry,entry') !entry_coercion_map))
@@ -1377,28 +1410,27 @@ let rec insert_coercion_path path = function
       else if shorter_path path path' then path::allpaths
       else path'::insert_coercion_path path paths
 
-let declare_entry_coercion (scope,(entry,_) as specific_ntn) entry' =
-  let entry, lev = decompose_custom_entry entry in
-  let entry', lev' = decompose_custom_entry entry' in
+let declare_entry_coercion (scope,(entry,key)) lev entry' =
+  let entry', lev' = decompose_notation_entry_level entry' in
   (* Transitive closure *)
   let toaddleft =
     EntryCoercionMap.fold (fun (entry'',entry''') paths l ->
         List.fold_right (fun ((lev'',lev'''),path) l ->
         if notation_entry_eq entry entry''' && level_ord lev lev''' &&
            not (notation_entry_eq entry' entry'')
-        then ((entry'',entry'),((lev'',lev'),path@[specific_ntn]))::l else l) paths l)
+        then ((entry'',entry'),((lev'',lev'),path@[(scope,(entry,key))]))::l else l) paths l)
       !entry_coercion_map [] in
   let toaddright =
     EntryCoercionMap.fold (fun (entry'',entry''') paths l ->
         List.fold_right (fun ((lev'',lev'''),path) l ->
         if entry' = entry'' && level_ord lev' lev'' && entry <> entry'''
-        then ((entry,entry'''),((lev,lev'''),path@[specific_ntn]))::l else l) paths l)
+        then ((entry,entry'''),((lev,lev'''),path@[(scope,(entry,key))]))::l else l) paths l)
       !entry_coercion_map [] in
   entry_coercion_map :=
     List.fold_right (fun (pair,path) ->
         let olds = try EntryCoercionMap.find pair !entry_coercion_map with Not_found -> [] in
         EntryCoercionMap.add pair (insert_coercion_path path olds))
-      (((entry,entry'),((lev,lev'),[specific_ntn]))::toaddright@toaddleft)
+      (((entry,entry'),((lev,lev'),[(scope,(entry,key))]))::toaddright@toaddleft)
       !entry_coercion_map
 
 let entry_has_global_map = ref String.Map.empty
diff --git a/interp/notation.mli b/interp/notation.mli
index e7e917463b..c39bfa6e28 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -298,8 +298,8 @@ type symbol =
 val symbol_eq : symbol -> symbol -> bool
 
 (** Make/decompose a notation of the form "_ U _" *)
-val make_notation_key : notation_entry_level -> symbol list -> notation
-val decompose_notation_key : notation -> notation_entry_level * symbol list
+val make_notation_key : notation_entry -> symbol list -> notation
+val decompose_notation_key : notation -> notation_entry * symbol list
 
 (** Decompose a notation of the form "a 'U' b" *)
 val decompose_raw_notation : string -> symbol list
@@ -313,8 +313,10 @@ val locate_notation : (glob_constr -> Pp.t) -> notation_key ->
 
 val pr_visibility: (glob_constr -> Pp.t) -> scope_name option -> Pp.t
 
+val make_notation_entry_level : notation_entry -> entry_level -> notation_entry_level
+
 type entry_coercion = (notation_with_optional_scope * notation) list
-val declare_entry_coercion : specific_notation -> notation_entry_level -> unit
+val declare_entry_coercion : specific_notation -> entry_level option -> notation_entry_level -> unit
 val availability_of_entry_coercion : notation_entry_level -> notation_entry_level -> entry_coercion option
 
 val declare_custom_entry_has_global : string -> int -> unit
@@ -323,6 +325,20 @@ val declare_custom_entry_has_ident : string -> int -> unit
 val entry_has_global : notation_entry_level -> bool
 val entry_has_ident : notation_entry_level -> bool
 
+(** Dealing with precedences *)
+
+type level = notation_entry * entry_level * entry_relative_level list
+  (* first argument is InCustomEntry s for custom entries *)
+
+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 } *)
+
+val declare_notation_level : notation -> level -> unit
+val level_of_notation : notation -> level
+  (** raise [Not_found] if not declared *)
+
 (** Rem: printing rules for primitive token are canonical *)
 
 val with_notation_protection : ('a -> 'b) -> 'a -> 'b