Adding support for custom entries in notations.

- New command "Declare Custom Entry bar".
- Entries can have levels.
- Printing is done using a notion of coercion between grammar
  entries. This typically corresponds to rules of the form
  'Notation "[ x ]" := x (x custom myconstr).' but also
  'Notation "{ x }" := x (in custom myconstr, x constr).'.
- Rules declaring idents such as 'Notation "x" := x (in custom myconstr, x ident).'
  are natively recognized.
- Rules declaring globals such as 'Notation "x" := x (in custom myconstr, x global).'
  are natively recognized.

Incidentally merging ETConstr and ETConstrAsBinder.

Noticed in passing that parsing binder as custom was not done as in
constr.

Probably some fine-tuning still to do (priority of notations,
interactions between scopes and entries, ...). To be tested live
further.

8 files changed, 70 insertions, 43 deletions

diff --git a/parsing/extend.ml b/parsing/extend.ml
index f57e32c884..a3e27f9cf5 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -38,10 +38,8 @@ type 'a constr_entry_key_gen =
   | ETReference
   | ETBigint
   | ETBinder of bool  (* open list of binders if true, closed list of binders otherwise *)
-  | ETConstr of 'a
-  | ETConstrAsBinder of Notation_term.constr_as_binder_kind * 'a
+  | ETConstr of Constrexpr.notation_entry * Notation_term.constr_as_binder_kind option * 'a
   | ETPattern of bool * int option (* true = strict pattern, i.e. not a single variable *)
-  | ETOther of string * string
 
 (** Entries level (left-hand side of grammar rules) *)
 
@@ -63,9 +61,8 @@ type constr_prod_entry_key =
   | ETProdName            (* Parsed as a name (ident or _) *)
   | ETProdReference       (* Parsed as a global reference *)
   | ETProdBigint          (* Parsed as an (unbounded) integer *)
-  | ETProdConstr of (production_level * production_position) (* Parsed as constr or pattern *)
+  | ETProdConstr of Constrexpr.notation_entry * (production_level * production_position) (* Parsed as constr or pattern, or a subentry of those *)
   | ETProdPattern of int  (* Parsed as pattern as a binder (as subpart of a constr) *)
-  | ETProdOther of string * string (* Intended for embedding custom entries in constr or pattern *)
   | ETProdConstrList of (production_level * production_position) * Tok.t list (* Parsed as non-empty list of constr *)
   | ETProdBinderList of binder_entry_kind  (* Parsed as non-empty list of local binders *)
 
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index b2913d5d4f..49e1cd7ec9 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -225,11 +225,11 @@ GRAMMAR EXTEND Gram
       | "("; c = operconstr LEVEL "200"; ")" ->
         { (match c.CAst.v with
             | CPrim (Numeral (n,true)) ->
-                CAst.make ~loc @@ CNotation("( _ )",([c],[],[],[]))
+                CAst.make ~loc @@ CNotation((InConstrEntrySomeLevel,"( _ )"),([c],[],[],[]))
             | _ -> c) }
       | "{|"; c = record_declaration; "|}" -> { c }
       | "{"; c = binder_constr ; "}" ->
-          { CAst.make ~loc @@ CNotation(("{ _ }"),([c],[],[],[])) }
+          { CAst.make ~loc @@ CNotation((InConstrEntrySomeLevel,"{ _ }"),([c],[],[],[])) }
       | "`{"; c = operconstr LEVEL "200"; "}" ->
 	  { CAst.make ~loc @@ CGeneralization (Implicit, None, c) }
       | "`("; c = operconstr LEVEL "200"; ")" ->
@@ -411,13 +411,13 @@ GRAMMAR EXTEND Gram
       | "("; p = pattern LEVEL "200"; ")" ->
           { (match p.CAst.v with
             | CPatPrim (Numeral (n,true)) ->
-                 CAst.make ~loc @@ CPatNotation("( _ )",([p],[]),[])
+                 CAst.make ~loc @@ CPatNotation((InConstrEntrySomeLevel,"( _ )"),([p],[]),[])
             | _ -> p) }
       | "("; p = pattern LEVEL "200"; ":"; ty = lconstr; ")" ->
           { let p =
             match p with
             | { CAst.v = CPatPrim (Numeral (n,true)) } ->
-                 CAst.make ~loc @@ CPatNotation("( _ )",([p],[]),[])
+                 CAst.make ~loc @@ CPatNotation((InConstrEntrySomeLevel,"( _ )"),([p],[]),[])
             | _ -> p
           in
 	  CAst.make ~loc @@ CPatCast (p, ty) }
diff --git a/parsing/notation_gram.ml b/parsing/notation_gram.ml
index 346350641f..d8c08803b6 100644
--- a/parsing/notation_gram.ml
+++ b/parsing/notation_gram.ml
@@ -17,7 +17,8 @@ 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 level = Constrexpr.notation_entry * precedence * tolerability list * constr_entry_key list
+  (* first argument is InCustomEntry s for custom entries *)
 
 type grammar_constr_prod_item =
   | GramConstrTerminal of Tok.t
diff --git a/parsing/notgram_ops.ml b/parsing/notgram_ops.ml
index 071e6db205..125ea01681 100644
--- a/parsing/notgram_ops.ml
+++ b/parsing/notgram_ops.ml
@@ -11,55 +11,59 @@
 open Pp
 open CErrors
 open Util
-open Extend
+open Notation
 open Notation_gram
 
 (* Uninterpreted notation levels *)
 
-let notation_level_map = Summary.ref ~name:"notation_level_map" String.Map.empty
+let notation_level_map = Summary.ref ~name:"notation_level_map" NotationMap.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
+  if NotationMap.mem ntn !notation_level_map then
+    anomaly (str "Notation " ++ pr_notation ntn ++ str " is already assigned a level.");
+  notation_level_map := NotationMap.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
+  let (level,onlyprint') = NotationMap.find ntn !notation_level_map in
   if onlyprint' && not onlyprint then raise Not_found;
   level
 
 (**********************************************************************)
-(* Operations on scopes *)
+(* Equality *)
+
+open Extend
 
 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 = match (pp1,pp2) with
+| BorderProd (side1,assoc1), BorderProd (side2,assoc2) -> side1 = side2 && assoc1 = assoc2
+| InternalProd, InternalProd -> true
+| (BorderProd _ | InternalProd), _ -> false
 
-let production_position_eq pp1 pp2 = true (* pp1 = pp2 *) (* match pp1, pp2 with
+let production_level_eq l1 l2 = match (l1,l2) with
 | NextLevel, NextLevel -> true
 | NumLevel n1, NumLevel n2 -> Int.equal n1 n2
-| (NextLevel | NumLevel _), _ -> false *)
+| (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
+| ETConstr (s1,bko1,lev1), ETConstr (s2,bko2,lev2) ->
+   notation_entry_eq s1 s2 && eq lev1 lev2 && Option.equal (=) bko1 bko2
 | 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
+| (ETName | ETReference | ETBigint | ETBinder _ | ETConstr _ | ETPattern _), _ -> false
 
-let level_eq_gen strict (l1, t1, u1) (l2, t2, u2) =
+let level_eq_gen strict (s1, l1, t1, u1) (s2, 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
+    not strict ||
+    (production_level_eq l1 l2 && production_position_eq pp1 pp2) in
+  notation_entry_eq s1 s2 && 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/pcoq.ml b/parsing/pcoq.ml
index 9d2f73eeb8..8455992f20 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -560,15 +560,34 @@ let register_grammars_by_name name grams =
 let find_grammars_by_name name =
   String.Map.find name !grammar_names
 
+(** Custom entries *)
+
+let custom_entries = ref String.Map.empty
+
+let create_custom_entries s =
+  let sc = "constr:"^s in
+  let sp = "pattern:"^s in
+  let c = (Gram.entry_create sc : Constrexpr.constr_expr Gram.entry) in
+  let p = (Gram.entry_create sp : Constrexpr.cases_pattern_expr Gram.entry) in
+  register_grammars_by_name s [AnyEntry c; AnyEntry p];
+  custom_entries := String.Map.add s (c,p) !custom_entries
+
+let find_custom_entries s =
+  try String.Map.find s !custom_entries
+  with Not_found -> user_err Pp.(str "Undeclared custom entry: " ++ str s ++ str ".")
+
 (** Summary functions: the state of the lexer is included in that of the parser.
    Because the grammar affects the set of keywords when adding or removing
    grammar rules. *)
 type frozen_t =
   (int * GrammarCommand.t * GramState.t) list *
   CLexer.keyword_state *
-  any_entry list String.Map.t
+  any_entry list String.Map.t *
+  (Constrexpr.constr_expr Gram.entry * Constrexpr.cases_pattern_expr Gram.entry) Util.String.Map.t
 
-let freeze _ : frozen_t = (!grammar_stack, CLexer.get_keyword_state (), !grammar_names)
+let freeze _ : frozen_t =
+  (!grammar_stack, CLexer.get_keyword_state (),
+   !grammar_names, !custom_entries)
 
 (* We compare the current state of the grammar and the state to unfreeze,
    by computing the longest common suffixes *)
@@ -578,14 +597,15 @@ let factorize_grams l1 l2 =
 let number_of_entries gcl =
   List.fold_left (fun n (p,_,_) -> n + p) 0 gcl
 
-let unfreeze (grams, lex, names) =
+let unfreeze (grams, lex, names, custom) =
   let (undo, redo, common) = factorize_grams !grammar_stack grams in
   let n = number_of_entries undo in
   remove_grammars n;
   grammar_stack := common;
   CLexer.set_keyword_state lex;
   List.iter extend_dyn_grammar (List.rev_map pi2 redo);
-  grammar_names := names
+  grammar_names := names;
+  custom_entries := custom
 
 (** No need to provide an init function : the grammar state is
     statically available, and already empty initially, while
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 029c437136..9711cd0461 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -272,3 +272,8 @@ type any_entry = AnyEntry : 'a Entry.t -> any_entry
 
 val register_grammars_by_name : string -> any_entry list -> unit
 val find_grammars_by_name : string -> any_entry list
+
+(** Create a custom entry of some name *)
+
+val create_custom_entries : string -> unit
+val find_custom_entries : string -> (Constrexpr.constr_expr Gram.entry * Constrexpr.cases_pattern_expr Gram.entry)
diff --git a/parsing/ppextend.ml b/parsing/ppextend.ml
index d2b50fa83d..e1f5e20117 100644
--- a/parsing/ppextend.ml
+++ b/parsing/ppextend.ml
@@ -11,6 +11,7 @@
 open Util
 open Pp
 open CErrors
+open Notation
 open Notation_gram
 
 (*s Pretty-print. *)
@@ -48,29 +49,29 @@ 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)
+  Summary.ref ~name:"notation-rules" (NotationMap.empty : (unparsing_rule * extra_unparsing_rules * notation_grammar) NotationMap.t)
 
 let declare_notation_rule ntn ~extra unpl gram =
-  notation_rules := String.Map.add ntn (unpl,extra,gram) !notation_rules
+  notation_rules := NotationMap.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 ".")
+  try pi1 (NotationMap.find ntn !notation_rules)
+  with Not_found -> anomaly (str "No printing rule found for " ++ pr_notation ntn ++ str ".")
 let find_notation_extra_printing_rules ntn =
-  try pi2 (String.Map.find ntn !notation_rules)
+  try pi2 (NotationMap.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 ".")
+  try pi3 (NotationMap.find ntn !notation_rules)
+  with Not_found -> anomaly (str "No parsing rule found for " ++ pr_notation ntn ++ str ".")
 
 let get_defined_notations () =
-  String.Set.elements @@ String.Map.domain !notation_rules
+  NotationSet.elements @@ NotationMap.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
+      let p, pp, gr = NotationMap.find ntn !notation_rules in
+      NotationMap.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
index 9f61e121a4..7eb5967a3e 100644
--- a/parsing/ppextend.mli
+++ b/parsing/ppextend.mli
@@ -41,7 +41,6 @@ type unparsing =
 
 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