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.

1 files changed, 22 insertions, 18 deletions

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