[notations] Split interpretation and parsing of notations

Previously to this patch, `Notation_term` contained information about
both parsing and notation interpretation.

We split notation grammar to a file `parsing/notation_gram` as to make
`interp/` not to depend on some parsing structures such as entries.

6 files changed, 25 insertions, 24 deletions

diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 5f63d21c4..e7a308dda 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -8,14 +8,14 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open CErrors
 open Util
-open Pcoq
+open CErrors
+open Names
+open Libnames
 open Constrexpr
-open Notation_term
 open Extend
-open Libnames
-open Names
+open Notation_gram
+open Pcoq
 
 (**********************************************************************)
 (* This determines (depending on the associativity of the current
diff --git a/vernac/egramcoq.mli b/vernac/egramcoq.mli
index e15add10f..b0341e6a1 100644
--- a/vernac/egramcoq.mli
+++ b/vernac/egramcoq.mli
@@ -15,5 +15,5 @@
 
 (** {5 Adding notations} *)
 
-val extend_constr_grammar : Notation_term.one_notation_grammar -> unit
+val extend_constr_grammar : Notation_gram.one_notation_grammar -> unit
 (** Add a term notation rule to the parsing system. *)
diff --git a/vernac/g_vernac.ml4 b/vernac/g_vernac.ml4
index 0964d46ac..dd8149d0a 100644
--- a/vernac/g_vernac.ml4
+++ b/vernac/g_vernac.ml4
@@ -1148,8 +1148,8 @@ GEXTEND Gram
     [ [ "at"; n = level -> n ] ]
   ;
   constr_as_binder_kind:
-    [ [ "as"; IDENT "ident" -> AsIdent
-      | "as"; IDENT "pattern" -> AsIdentOrPattern
-      | "as"; IDENT "strict"; IDENT "pattern" -> AsStrictPattern ] ]
+    [ [ "as"; IDENT "ident" -> Notation_term.AsIdent
+      | "as"; IDENT "pattern" -> Notation_term.AsIdentOrPattern
+      | "as"; IDENT "strict"; IDENT "pattern" -> Notation_term.AsStrictPattern ] ]
   ;
 END
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index e038f54dd..2245e762f 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -15,6 +15,7 @@ open Names
 open Constrexpr
 open Constrexpr_ops
 open Notation_term
+open Notation_gram
 open Notation_ops
 open Ppextend
 open Extend
@@ -709,7 +710,7 @@ let error_parsing_incompatible_level ntn ntn' oldprec prec =
     pr_level ntn prec ++ str ".")
 
 type syntax_extension = {
-  synext_level : Notation_term.level;
+  synext_level : Notation_gram.level;
   synext_notation : notation;
   synext_notgram : notation_grammar;
   synext_unparsing : unparsing list;
@@ -728,8 +729,8 @@ let check_and_extend_constr_grammar ntn rule =
     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;
+    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;
   with Not_found ->
     Egramcoq.extend_constr_grammar rule
 
@@ -738,16 +739,16 @@ let cache_one_syntax_extension se =
   let prec = se.synext_level in
   let onlyprint = se.synext_notgram.notgram_onlyprinting in
   try
-    let oldprec = Notation.level_of_notation ~onlyprint ntn in
-    if not (Notation.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec;
+    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;
   with Not_found ->
     if is_active_compat se.synext_compat then begin
       (* Reserve the notation level *)
-      Notation.declare_notation_level ntn prec ~onlyprint;
+      Notgram_ops.declare_notation_level ntn prec ~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 *)
-      Notation.declare_notation_rule ntn
+      declare_notation_rule ntn
         ~extra:se.synext_extra (se.synext_unparsing, pi1 prec) se.synext_notgram
     end
 
@@ -1061,7 +1062,7 @@ let find_precedence lev etyps symbols onlyprint =
       [],Option.get lev
 
 let check_curly_brackets_notation_exists () =
-  try let _ = Notation.level_of_notation "{ _ }" in ()
+  try let _ = Notgram_ops.level_of_notation "{ _ }" 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.")
@@ -1274,10 +1275,10 @@ exception NoSyntaxRule
 
 let recover_notation_syntax ntn =
   try
-    let prec = Notation.level_of_notation ~onlyprint:true ntn (* Be as little restrictive as possible *) in
-    let pp_rule,_ = Notation.find_notation_printing_rule ntn in
-    let pp_extra_rules = Notation.find_notation_extra_printing_rules ntn in
-    let pa_rule = Notation.find_notation_parsing_rules ntn in
+    let prec = Notgram_ops.level_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_notation = ntn;
       synext_notgram = pa_rule;
@@ -1444,7 +1445,7 @@ let add_notation_extra_printing_rule df k v =
   let notk = 
     let _,_, symbs = analyze_notation_tokens ~onlyprint:true df in
     make_notation_key symbs in
-  Notation.add_notation_extra_printing_rule notk k v
+  add_notation_extra_printing_rule notk k v
 
 (* Infix notations *)
 
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 7e67e12cb..7aff758e9 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -102,7 +102,7 @@ open Pputils
     | NumLevel n -> keyword "at" ++ spc () ++ keyword "level" ++ spc () ++ int n
     | NextLevel -> keyword "at" ++ spc () ++ keyword "next" ++ spc () ++ keyword "level"
 
-  let pr_constr_as_binder_kind = function
+  let pr_constr_as_binder_kind = let open Notation_term in function
     | AsIdent -> keyword "as ident"
     | AsIdentOrPattern -> keyword "as pattern"
     | AsStrictPattern -> keyword "as strict pattern"
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 4ff9d105b..74355e1a7 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -207,7 +207,7 @@ type proof_expr =
 
 type syntax_modifier =
   | SetItemLevel of string list * Extend.production_level
-  | SetItemLevelAsBinder of string list * Extend.constr_as_binder_kind * Extend.production_level option
+  | SetItemLevelAsBinder of string list * Notation_term.constr_as_binder_kind * Extend.production_level option
   | SetLevel of int
   | SetAssoc of Extend.gram_assoc
   | SetEntryType of string * Extend.simple_constr_prod_entry_key