[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.

7 files changed, 259 insertions, 6 deletions

diff --git a/parsing/extend.ml b/parsing/extend.ml
index 734b859f6..f2af594ef 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -31,11 +31,6 @@ type production_level =
   | NextLevel
   | NumLevel of int
 
-type constr_as_binder_kind =
-  | AsIdent
-  | AsIdentOrPattern
-  | AsStrictPattern
-
 (** User-level types used to tell how to parse or interpret of the non-terminal *)
 
 type 'a constr_entry_key_gen =
@@ -44,7 +39,7 @@ type 'a constr_entry_key_gen =
   | ETBigint
   | ETBinder of bool  (* open list of binders if true, closed list of binders otherwise *)
   | ETConstr of 'a
-  | ETConstrAsBinder of constr_as_binder_kind * 'a
+  | ETConstrAsBinder of Notation_term.constr_as_binder_kind * 'a
   | ETPattern of bool * int option (* true = strict pattern, i.e. not a single variable *)
   | ETOther of string * string
 
diff --git a/parsing/notation_gram.ml b/parsing/notation_gram.ml
new file mode 100644
index 000000000..346350641
--- /dev/null
+++ b/parsing/notation_gram.ml
@@ -0,0 +1,42 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Names
+open Extend
+
+(** Dealing with precedences *)
+
+type precedence = int
+type parenRelation = L | E | Any | Prec of precedence
+type tolerability = precedence * parenRelation
+
+type level = precedence * tolerability list * constr_entry_key list
+
+type grammar_constr_prod_item =
+  | GramConstrTerminal of Tok.t
+  | GramConstrNonTerminal of Extend.constr_prod_entry_key * Id.t option
+  | GramConstrListMark of int * bool * int
+    (* tells action rule to make a list of the n previous parsed items;
+       concat with last parsed list when true; additionally release
+       the p last items as if they were parsed autonomously *)
+
+(** Grammar rules for a notation *)
+
+type one_notation_grammar = {
+  notgram_level : level;
+  notgram_assoc : Extend.gram_assoc option;
+  notgram_notation : Constrexpr.notation;
+  notgram_prods : grammar_constr_prod_item list list;
+}
+
+type notation_grammar = {
+  notgram_onlyprinting : bool;
+  notgram_rules : one_notation_grammar list
+}
diff --git a/parsing/notgram_ops.ml b/parsing/notgram_ops.ml
new file mode 100644
index 000000000..071e6db20
--- /dev/null
+++ b/parsing/notgram_ops.ml
@@ -0,0 +1,65 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Pp
+open CErrors
+open Util
+open Extend
+open Notation_gram
+
+(* Uninterpreted notation levels *)
+
+let notation_level_map = Summary.ref ~name:"notation_level_map" String.Map.empty
+
+let declare_notation_level ?(onlyprint=false) ntn level =
+  if String.Map.mem ntn !notation_level_map then
+    anomaly (str "Notation " ++ str ntn ++ str " is already assigned a level.");
+  notation_level_map := String.Map.add ntn (level,onlyprint) !notation_level_map
+
+let level_of_notation ?(onlyprint=false) ntn =
+  let (level,onlyprint') = String.Map.find ntn !notation_level_map in
+  if onlyprint' && not onlyprint then raise Not_found;
+  level
+
+(**********************************************************************)
+(* Operations on scopes *)
+
+let parenRelation_eq t1 t2 = match t1, t2 with
+| L, L | E, E | Any, Any -> true
+| Prec l1, Prec l2 -> Int.equal l1 l2
+| _ -> false
+
+let production_level_eq l1 l2 = true (* (l1 = l2) *)
+
+let production_position_eq pp1 pp2 = true (* pp1 = pp2 *) (* match pp1, pp2 with
+| NextLevel, NextLevel -> true
+| NumLevel n1, NumLevel n2 -> Int.equal n1 n2
+| (NextLevel | NumLevel _), _ -> false *)
+
+let constr_entry_key_eq eq v1 v2 = match v1, v2 with
+| ETName, ETName -> true
+| ETReference, ETReference -> true
+| ETBigint, ETBigint -> true
+| ETBinder b1, ETBinder b2 -> b1 == b2
+| ETConstr lev1, ETConstr lev2 -> eq lev1 lev2
+| ETConstrAsBinder (bk1,lev1), ETConstrAsBinder (bk2,lev2) -> eq lev1 lev2 && bk1 = bk2
+| ETPattern (b1,n1), ETPattern (b2,n2) -> b1 = b2 && Option.equal Int.equal n1 n2
+| ETOther (s1,s1'), ETOther (s2,s2') -> String.equal s1 s2 && String.equal s1' s2'
+| (ETName | ETReference | ETBigint | ETBinder _ | ETConstr _ | ETPattern _ | ETOther _ | ETConstrAsBinder _), _ -> false
+
+let level_eq_gen strict (l1, t1, u1) (l2, t2, u2) =
+  let tolerability_eq (i1, r1) (i2, r2) = Int.equal i1 i2 && parenRelation_eq r1 r2 in
+  let prod_eq (l1,pp1) (l2,pp2) =
+    if strict then production_level_eq l1 l2 && production_position_eq pp1 pp2
+    else production_level_eq l1 l2 in
+  Int.equal l1 l2 && List.equal tolerability_eq t1 t2
+  && List.equal (constr_entry_key_eq prod_eq) u1 u2
+
+let level_eq = level_eq_gen false
diff --git a/parsing/notgram_ops.mli b/parsing/notgram_ops.mli
new file mode 100644
index 000000000..f427a607b
--- /dev/null
+++ b/parsing/notgram_ops.mli
@@ -0,0 +1,20 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* Merge with metasyntax? *)
+open Constrexpr
+open Notation_gram
+
+val level_eq : level -> level -> bool
+
+(** {6 Declare and test the level of a (possibly uninterpreted) notation } *)
+
+val declare_notation_level : ?onlyprint:bool -> notation -> level -> unit
+val level_of_notation : ?onlyprint:bool -> notation -> level (** raise [Not_found] if no level or not respecting onlyprint *)
diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib
index da4a0421b..2154f2f88 100644
--- a/parsing/parsing.mllib
+++ b/parsing/parsing.mllib
@@ -1,6 +1,9 @@
 Tok
 CLexer
 Extend
+Notation_gram
+Ppextend
+Notgram_ops
 Pcoq
 G_constr
 G_prim
diff --git a/parsing/ppextend.ml b/parsing/ppextend.ml
new file mode 100644
index 000000000..d2b50fa83
--- /dev/null
+++ b/parsing/ppextend.ml
@@ -0,0 +1,76 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Util
+open Pp
+open CErrors
+open Notation_gram
+
+(*s Pretty-print. *)
+
+type ppbox =
+  | PpHB of int
+  | PpHOVB of int
+  | PpHVB of int
+  | PpVB of int
+
+type ppcut =
+  | PpBrk of int * int
+  | PpFnl
+
+let ppcmd_of_box = function
+  | PpHB n -> h n
+  | PpHOVB n -> hov n
+  | PpHVB n -> hv n
+  | PpVB n -> v n
+
+let ppcmd_of_cut = function
+  | PpFnl -> fnl ()
+  | PpBrk(n1,n2) -> brk(n1,n2)
+
+type unparsing =
+  | UnpMetaVar of int * parenRelation
+  | UnpBinderMetaVar of int * parenRelation
+  | UnpListMetaVar of int * parenRelation * unparsing list
+  | UnpBinderListMetaVar of int * bool * unparsing list
+  | UnpTerminal of string
+  | UnpBox of ppbox * unparsing Loc.located list
+  | UnpCut of ppcut
+
+type unparsing_rule = unparsing list * precedence
+type extra_unparsing_rules = (string * string) list
+(* Concrete syntax for symbolic-extension table *)
+let notation_rules =
+  Summary.ref ~name:"notation-rules" (String.Map.empty : (unparsing_rule * extra_unparsing_rules * notation_grammar) String.Map.t)
+
+let declare_notation_rule ntn ~extra unpl gram =
+  notation_rules := String.Map.add ntn (unpl,extra,gram) !notation_rules
+
+let find_notation_printing_rule ntn =
+  try pi1 (String.Map.find ntn !notation_rules)
+  with Not_found -> anomaly (str "No printing rule found for " ++ str ntn ++ str ".")
+let find_notation_extra_printing_rules ntn =
+  try pi2 (String.Map.find ntn !notation_rules)
+  with Not_found -> []
+let find_notation_parsing_rules ntn =
+  try pi3 (String.Map.find ntn !notation_rules)
+  with Not_found -> anomaly (str "No parsing rule found for " ++ str ntn ++ str ".")
+
+let get_defined_notations () =
+  String.Set.elements @@ String.Map.domain !notation_rules
+
+let add_notation_extra_printing_rule ntn k v =
+  try
+    notation_rules :=
+      let p, pp, gr = String.Map.find ntn !notation_rules in
+      String.Map.add ntn (p, (k,v) :: pp, gr) !notation_rules
+  with Not_found ->
+    user_err ~hdr:"add_notation_extra_printing_rule"
+      (str "No such Notation.")
diff --git a/parsing/ppextend.mli b/parsing/ppextend.mli
new file mode 100644
index 000000000..9f61e121a
--- /dev/null
+++ b/parsing/ppextend.mli
@@ -0,0 +1,52 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Constrexpr
+open Notation_gram
+
+(** {6 Pretty-print. } *)
+
+type ppbox =
+  | PpHB of int
+  | PpHOVB of int
+  | PpHVB of int
+  | PpVB of int
+
+type ppcut =
+  | PpBrk of int * int
+  | PpFnl
+
+val ppcmd_of_box : ppbox -> Pp.t -> Pp.t
+
+val ppcmd_of_cut : ppcut -> Pp.t
+
+(** {6 Printing rules for notations} *)
+
+(** Declare and look for the printing rule for symbolic notations *)
+type unparsing =
+  | UnpMetaVar of int * parenRelation
+  | UnpBinderMetaVar of int * parenRelation
+  | UnpListMetaVar of int * parenRelation * unparsing list
+  | UnpBinderListMetaVar of int * bool * unparsing list
+  | UnpTerminal of string
+  | UnpBox of ppbox * unparsing Loc.located list
+  | UnpCut of ppcut
+
+type unparsing_rule = unparsing list * precedence
+type extra_unparsing_rules = (string * string) list
+
+val declare_notation_rule : notation -> extra:extra_unparsing_rules -> unparsing_rule -> notation_grammar -> unit
+val find_notation_printing_rule : notation -> unparsing_rule
+val find_notation_extra_printing_rules : notation -> extra_unparsing_rules
+val find_notation_parsing_rules : notation -> notation_grammar
+val add_notation_extra_printing_rule : notation -> string -> string -> unit
+
+(** Returns notations with defined parsing/printing rules *)
+val get_defined_notations : unit -> notation list