A new step of restructuration of notations.

This allows to issue a more appropriate message when a notation with a
{ } cannot be defined because of an incompatible level. E.g.:

Notation "{ A } + B" := (sumbool A B) (at level 20).

17 files changed, 79 insertions, 76 deletions

diff --git a/API/API.ml b/API/API.ml
index 1d7a4a4f4..c4bcef6f6 100644
--- a/API/API.ml
+++ b/API/API.ml
@@ -169,7 +169,6 @@ module Stdarg = Stdarg
 module Genintern = Genintern
 module Constrexpr_ops = Constrexpr_ops
 module Notation_ops = Notation_ops
-module Ppextend = Ppextend
 module Notation = Notation
 module Dumpglob = Dumpglob
 (* module Syntax_def *)
diff --git a/API/API.mli b/API/API.mli
index 5804a82f6..6a7b2fc9a 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -3184,6 +3184,10 @@ sig
                        | NCast of notation_constr * notation_constr Misctypes.cast_type
   type interpretation = (Names.Id.t * (subscopes * notation_var_instance_type)) list *
     notation_constr
+  type precedence = int
+  type parenRelation =
+    | L | E | Any | Prec of precedence
+  type tolerability = precedence * parenRelation
 end
 
 module Tactypes :
@@ -4179,16 +4183,6 @@ sig
                                                     'a -> Notation_term.notation_constr -> Glob_term.glob_constr
 end
 
-module Ppextend :
-sig
-
-  type precedence = int
-  type parenRelation =
-    | L | E | Any | Prec of precedence
-  type tolerability = precedence * parenRelation
-
-end
-
 module Notation :
 sig
   type cases_pattern_status = bool
@@ -4880,7 +4874,7 @@ sig
   val pr_with_comments : ?loc:Loc.t -> Pp.t -> Pp.t
   val pr_lident : Names.Id.t Loc.located -> Pp.t
   val pr_lname : Names.Name.t Loc.located -> Pp.t
-  val prec_less : int -> int * Ppextend.parenRelation -> bool
+  val prec_less : int -> int * Notation_term.parenRelation -> bool
   val pr_constr_expr : Constrexpr.constr_expr -> Pp.t
   val pr_lconstr_expr : Constrexpr.constr_expr -> Pp.t
   val pr_constr_pattern_expr : Constrexpr.constr_pattern_expr -> Pp.t
diff --git a/interp/notation.ml b/interp/notation.ml
index c7bf0e36b..c373faf68 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -41,7 +41,6 @@ open Context.Named.Declaration
 (**********************************************************************)
 (* Scope of symbols *)
 
-type level = precedence * tolerability list * notation_var_internalization_type list
 type delimiters = string
 type notation_location = (DirPath.t * DirPath.t) * string
 
diff --git a/interp/notation.mli b/interp/notation.mli
index 5f6bfa35f..f9f247fe1 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -21,7 +21,6 @@ open Ppextend
 (** A scope is a set of interpreters for symbols + optional
    interpreter and printers for integers + optional delimiters *)
 
-type level = precedence * tolerability list * notation_var_internalization_type list
 type delimiters = string
 type scope
 type scopes (** = [scope_name list] *)
diff --git a/interp/ppextend.ml b/interp/ppextend.ml
index 2bbe87bbc..3ebc9b71d 100644
--- a/interp/ppextend.ml
+++ b/interp/ppextend.ml
@@ -7,17 +7,10 @@
 (************************************************************************)
 
 open Pp
+open Notation_term
 
 (*s Pretty-print. *)
 
-(* Dealing with precedences *)
-
-type precedence = int
-
-type parenRelation = L | E | Any | Prec of precedence
-
-type tolerability = precedence * parenRelation
-
 type ppbox =
   | PpHB of int
   | PpHOVB of int
diff --git a/interp/ppextend.mli b/interp/ppextend.mli
index a347a5c7b..6ff5a4272 100644
--- a/interp/ppextend.mli
+++ b/interp/ppextend.mli
@@ -6,15 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** {6 Pretty-print. } *)
-
-(** Dealing with precedences *)
-
-type precedence = int
+open Notation_term
 
-type parenRelation = L | E | Any | Prec of precedence
-
-type tolerability = precedence * parenRelation
+(** {6 Pretty-print. } *)
 
 type ppbox =
   | PpHB of int
diff --git a/intf/notation_term.ml b/intf/notation_term.ml
index 084a1042c..c342da3dc 100644
--- a/intf/notation_term.ml
+++ b/intf/notation_term.ml
@@ -88,12 +88,24 @@ type grammar_constr_prod_item =
        concat with last parsed list when true; additionally release
        the p last items as if they were parsed autonomously *)
 
+(** Dealing with precedences *)
+
+type precedence = int
+type parenRelation = L | E | Any | Prec of precedence
+type tolerability = precedence * parenRelation
+
+type level = precedence * tolerability list * notation_var_internalization_type list
+
+(** Grammar rules for a notation *)
+
 type one_notation_grammar = {
-  notgram_level : int;
+  notgram_level : level;
   notgram_assoc : Extend.gram_assoc option;
   notgram_notation : Constrexpr.notation;
   notgram_prods : grammar_constr_prod_item list list;
-  notgram_typs : notation_var_internalization_type list;
 }
 
-type notation_grammar = (* onlyprinting *) bool * one_notation_grammar list
+type notation_grammar = {
+  notgram_onlyprinting : bool;
+  notgram_rules : one_notation_grammar list
+}
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 1b38a013c..870137ca1 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -443,7 +443,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 n = ng.notgram_level in
+  let n,_,_ = ng.notgram_level in
   let assoc = ng.notgram_assoc in
   let (entry, level) = interp_constr_entry_key forpat n in
   let fold (accu, state) pt =
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index 609795133..89feea8dc 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -249,7 +249,7 @@ END
 let pr_by_arg_tac _prc _prlc prtac opt_c =
   match opt_c with
     | None -> mt ()
-    | Some t -> hov 2 (str "by" ++ spc () ++ prtac (3,Ppextend.E) t)
+    | Some t -> hov 2 (str "by" ++ spc () ++ prtac (3,Notation_term.E) t)
 
 ARGUMENT EXTEND by_arg_tac
   TYPED AS tactic_opt
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index b06f35ddc..00668ddc7 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -64,7 +64,7 @@ val wit_by_arg_tac :
   Geninterp.Val.t option) Genarg.genarg_type
 
 val pr_by_arg_tac : 
-  (int * Ppextend.parenRelation -> raw_tactic_expr -> Pp.t) ->
+  (int * Notation_term.parenRelation -> raw_tactic_expr -> Pp.t) ->
   raw_tactic_expr option -> Pp.t
 
 val test_lpar_id_colon : unit Pcoq.Gram.entry
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 140cc3344..cb7d9b9c0 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -18,7 +18,7 @@ open Geninterp
 open Stdarg
 open Tacarg
 open Libnames
-open Ppextend
+open Notation_term
 open Misctypes
 open Locus
 open Decl_kinds
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 0bf9bc7f6..1f6ebaf44 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -16,7 +16,7 @@ open Misctypes
 open Environ
 open Constrexpr
 open Tacexpr
-open Ppextend
+open Notation_term
 
 type 'a grammar_tactic_prod_item_expr =
 | TacTerm of string
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index ce23bb2b3..db1981228 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -62,7 +62,7 @@ DECLARE PLUGIN "ssreflect_plugin"
  * we thus save the lexer to restore it at the end of the file *)
 let frozen_lexer = CLexer.get_keyword_state () ;;
 
-let tacltop = (5,Ppextend.E)
+let tacltop = (5,Notation_term.E)
 
 let pr_ssrtacarg _ _ prt = prt tacltop
 ARGUMENT EXTEND ssrtacarg TYPED AS tactic PRINTED BY pr_ssrtacarg
diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli
index 88beeaa71..f9dc345e1 100644
--- a/plugins/ssr/ssrparser.mli
+++ b/plugins/ssr/ssrparser.mli
@@ -10,11 +10,11 @@
 
 val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry
 val wit_ssrtacarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type
-val pr_ssrtacarg : 'a -> 'b -> (int * Ppextend.parenRelation -> 'c) -> 'c
+val pr_ssrtacarg : 'a -> 'b -> (Notation_term.tolerability -> 'c) -> 'c
 
 val ssrtclarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry
 val wit_ssrtclarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type
-val pr_ssrtclarg : 'a -> 'b -> (int * Ppextend.parenRelation -> 'c -> 'd) -> 'c -> 'd
+val pr_ssrtclarg : 'a -> 'b -> (Notation_term.tolerability -> 'c -> 'd) -> 'c -> 'd
 
 val add_genarg : string -> ('a -> Pp.t) -> 'a Genarg.uniform_genarg_type
 
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index ee03bc900..4a103cdd2 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -15,6 +15,7 @@ open Nameops
 open Libnames
 open Pputils
 open Ppextend
+open Notation_term
 open Constrexpr
 open Constrexpr_ops
 open Decl_kinds
@@ -737,7 +738,7 @@ let tag_var = tag Tag.variable
     pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t
   }
 
-  type precedence =  Ppextend.precedence * Ppextend.parenRelation
+  type precedence =  Notation_term.precedence * Notation_term.parenRelation
   let modular_constr_pr = pr
   let rec fix rf x = rf (fix rf) x
   let pr = fix modular_constr_pr mt
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index 833503485..7546c748d 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -15,6 +15,7 @@ open Libnames
 open Constrexpr
 open Names
 open Misctypes
+open Notation_term
 
 val extract_lam_binders :
   constr_expr -> local_binder_expr list * constr_expr
@@ -24,7 +25,7 @@ val split_fix :
   int -> constr_expr -> constr_expr ->
   local_binder_expr list *  constr_expr * constr_expr
 
-val prec_less : int -> int * Ppextend.parenRelation -> bool
+val prec_less : precedence -> tolerability -> bool
 
 val pr_tight_coma : unit -> Pp.t
 
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index a98cff384..38c418ae0 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -705,8 +705,16 @@ let error_incompatible_level ntn oldprec prec =
     spc() ++ str "while it is now required to be" ++ spc() ++
     pr_level ntn prec ++ str ".")
 
+let error_parsing_incompatible_level ntn ntn' oldprec prec =
+  user_err
+    (str "Notation " ++ str ntn ++ str " relies on a parsing rule for " ++ str ntn' ++ spc() ++
+    str " which is already defined" ++ spc() ++
+    pr_level ntn oldprec ++
+    spc() ++ str "while it is now required to be" ++ spc() ++
+    pr_level ntn prec ++ str ".")
+
 type syntax_extension = {
-  synext_level : Notation.level;
+  synext_level : Notation_term.level;
   synext_notation : notation;
   synext_notgram : notation_grammar;
   synext_unparsing : unparsing list;
@@ -720,19 +728,29 @@ let is_active_compat = function
 
 type syntax_extension_obj = locality_flag * syntax_extension
 
+let check_and_extend_constr_grammar ntn rule =
+  try
+    let ntn_for_grammar = rule.notgram_notation in
+    if String.equal ntn ntn_for_grammar then raise Not_found;
+    let prec = rule.notgram_level in
+    let oldprec = Notation.level_of_notation ntn_for_grammar in
+    if not (Notation.level_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 onlyprint = fst se.synext_notgram in
+  let onlyprint = se.synext_notgram.notgram_onlyprinting in
   try
     let oldprec = Notation.level_of_notation ntn in
-    if not (Notation.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec
+    if not (Notation.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec;
   with Not_found ->
     if is_active_compat se.synext_compat then begin
       (* Reserve the notation level *)
       Notation.declare_notation_level ntn prec;
       (* Declare the parsing rule *)
-      if not onlyprint then List.iter Egramcoq.extend_constr_grammar (snd se.synext_notgram);
+      if not onlyprint then List.iter (check_and_extend_constr_grammar ntn) se.synext_notgram.notgram_rules;
       (* Declare the notation rule *)
       Notation.declare_notation_rule ntn
         ~extra:se.synext_extra (se.synext_unparsing, pi1 prec) se.synext_notgram
@@ -747,7 +765,7 @@ let subst_printing_rule subst x = x
 
 let subst_syntax_extension (subst, (local, sy)) =
   (local, { sy with
-    synext_notgram = (fst sy.synext_notgram, List.map (subst_parsing_rule subst) (snd sy.synext_notgram));
+    synext_notgram = { sy.synext_notgram with notgram_rules = List.map (subst_parsing_rule subst) sy.synext_notgram.notgram_rules };
     synext_unparsing = subst_printing_rule subst sy.synext_unparsing;
   })
 
@@ -1045,6 +1063,8 @@ let remove_curly_brackets l =
 
 module SynData = struct
 
+  type subentry_types = (Id.t * (production_level, production_position) constr_entry_key_gen) list
+
   (* XXX: Document *)
   type syn_data = {
 
@@ -1067,14 +1087,11 @@ module SynData = struct
     intern_typs   : notation_var_internalization_type list;
 
     (* Notation data for parsing *)
-
-    level         : int;
-    pa_syntax_data : (Id.t * (production_level, production_position) constr_entry_key_gen) list * (* typs    *)
-                     symbol list;                                                                 (* symbols *)
-    pp_syntax_data : (Id.t * (production_level, production_position) constr_entry_key_gen) list * (* typs    *)
-                      symbol list;                                                                (* symbols *)
+    level         : level;
+    pa_syntax_data : subentry_types * symbol list;
+    pp_syntax_data : subentry_types * symbol list;
     not_data      : notation *                   (* notation *)
-                    (int * parenRelation) list * (* precedence *)
+                    level *                      (* level, precedence, types *)
                     bool;                        (* needs_squash *)
   }
 
@@ -1124,7 +1141,7 @@ let compute_syntax_data df modifiers =
   let i_typs = set_internalization_type sy_typs in
   let pa_sy_data = (sy_typs_for_grammar,symbols_for_grammar) in
   let pp_sy_data = (sy_typs,symbols) in
-  let sy_fulldata = (ntn_for_grammar,prec,need_squash) in
+  let sy_fulldata = (ntn_for_grammar,(n,prec_for_grammar,i_typs),need_squash) in
   let df' = ((Lib.library_dp(),Lib.current_dirpath true),df) in
   let i_data = ntn_for_interp, df' in
 
@@ -1143,7 +1160,7 @@ let compute_syntax_data df modifiers =
     mainvars;
     intern_typs = i_typs;
 
-    level  = n;
+    level  = (n,prec,i_typs);
     pa_syntax_data = pa_sy_data;
     pp_syntax_data = pp_sy_data;
     not_data    = sy_fulldata;
@@ -1228,7 +1245,7 @@ let with_syntax_protection f x =
 
 exception NoSyntaxRule
 
-let recover_syntax ntn =
+let recover_notation_syntax ntn =
   try
     let prec = Notation.level_of_notation ntn in
     let pp_rule,_ = Notation.find_notation_printing_rule ntn in
@@ -1245,18 +1262,13 @@ let recover_syntax ntn =
     raise NoSyntaxRule
 
 let recover_squash_syntax sy =
-  let sq = recover_syntax "{ _ }" in
-  sy :: snd (sq.synext_notgram)
-
-let recover_notation_syntax ntn =
-  let sy = recover_syntax ntn in
-  let onlyprint,_ = sy.synext_notgram in
-  pi3 sy.synext_level, sy, onlyprint
+  let sq = recover_notation_syntax "{ _ }" in
+  sy :: sq.synext_notgram.notgram_rules
 
 (**********************************************************************)
 (* Main entry point for building parsing and printing rules           *)
 
-let make_pa_rule i_typs level (typs,symbols) ntn need_squash =
+let make_pa_rule level (typs,symbols) ntn need_squash =
   let assoc = recompute_assoc typs in
   let prod = make_production typs symbols in
   let sy = {
@@ -1264,7 +1276,6 @@ let make_pa_rule i_typs level (typs,symbols) ntn need_squash =
     notgram_assoc = assoc;
     notgram_notation = ntn;
     notgram_prods = prod;
-    notgram_typs = i_typs;
   } in
   (* By construction, the rule for "{ _ }" is declared, but we need to
      redeclare it because the file where it is declared needs not be open
@@ -1278,12 +1289,12 @@ 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, need_squash = sd.not_data in
-  let pa_rule = make_pa_rule sd.intern_typs sd.level sd.pa_syntax_data ntn_for_grammar need_squash in
-  let pp_rule = make_pp_rule sd.level sd.pp_syntax_data sd.format in {
-    synext_level    = (sd.level, prec, sd.intern_typs);
+  let ntn_for_grammar, prec_for_grammar, need_squash = sd.not_data 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 (pi1 sd.level) sd.pp_syntax_data sd.format in {
+    synext_level    = sd.level;
     synext_notation = fst sd.info;
-    synext_notgram  = (sd.only_printing,pa_rule);
+    synext_notgram  = { notgram_onlyprinting = sd.only_printing; notgram_rules = pa_rule };
     synext_unparsing = pp_rule;
     synext_extra  = sd.extra;
     synext_compat = sd.compat;
@@ -1332,11 +1343,11 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env)
   let (recvars,mainvars,symbs) = analyze_notation_tokens ~onlyprint dfs in
   (* Recover types of variables and pa/pp rules; redeclare them if needed *)
   let i_typs, onlyprint = if not (is_numeral symbs) then begin
-    let i_typs,sy_rules,onlyprint' = recover_notation_syntax (make_notation_key symbs) in
-    let () = Lib.add_anonymous_leaf (inSyntaxExtension (local,sy_rules)) in
+    let sy = recover_notation_syntax (make_notation_key symbs) in
+    let () = Lib.add_anonymous_leaf (inSyntaxExtension (local,sy)) in
     (** If the only printing flag has been explicitly requested, put it back *)
-    let onlyprint = onlyprint || onlyprint' in
-    i_typs, onlyprint
+    let onlyprint = onlyprint || sy.synext_notgram.notgram_onlyprinting in
+    pi3 sy.synext_level, onlyprint
   end else [], false in
   (* Declare interpretation *)
   let path = (Lib.library_dp(), Lib.current_dirpath true) in