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, 34 insertions, 11 deletions

diff --git a/interp/notation.mli b/interp/notation.mli
index b177b7f1e0..c921606484 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -17,6 +17,21 @@ open Notation_term
 
 (** Notations *)
 
+val pr_notation : notation -> Pp.t
+(** Printing *)
+
+val notation_entry_eq : notation_entry -> notation_entry -> bool
+(** Equality on [notation_entry]. *)
+
+val notation_entry_level_eq : notation_entry_level -> notation_entry_level -> bool
+(** Equality on [notation_entry_level]. *)
+
+val notation_eq : notation -> notation -> bool
+(** Equality on [notation]. *)
+
+module NotationSet : Set.S with type elt = notation
+module NotationMap : CMap.ExtS with type key = notation and module Set := NotationSet
+
 (** {6 Scopes } *)
 (** A scope is a set of interpreters for symbols + optional
    interpreter and printers for integers + optional delimiters *)
@@ -25,8 +40,6 @@ type delimiters = string
 type scope
 type scopes (** = [scope_name list] *)
 
-type local_scopes = tmp_scope_name option * scope_name list
-
 val declare_scope : scope_name -> unit
 
 val current_scopes : unit -> scopes
@@ -84,11 +97,11 @@ val declare_string_interpreter : scope_name -> required_module ->
 (** Return the [term]/[cases_pattern] bound to a primitive token in a
    given scope context*)
 
-val interp_prim_token : ?loc:Loc.t -> prim_token -> local_scopes ->
+val interp_prim_token : ?loc:Loc.t -> prim_token -> subscopes ->
   glob_constr * (notation_location * scope_name option)
 (* This function returns a glob_const representing a pattern *)
 val interp_prim_token_cases_pattern_expr : ?loc:Loc.t -> (GlobRef.t -> unit) -> prim_token ->
-  local_scopes -> glob_constr * (notation_location * scope_name option)
+  subscopes -> glob_constr * (notation_location * scope_name option)
 
 (** Return the primitive token associated to a [term]/[cases_pattern];
    raise [No_match] if no such token *)
@@ -101,7 +114,7 @@ val uninterp_prim_token_ind_pattern :
  inductive -> cases_pattern list -> scope_name * prim_token
 
 val availability_of_prim_token :
-  prim_token -> scope_name -> local_scopes -> delimiters option option
+  prim_token -> scope_name -> subscopes -> delimiters option option
 
 (** {6 Declare and interpret back and forth a notation } *)
 
@@ -116,7 +129,7 @@ val declare_notation_interpretation : notation -> scope_name option ->
 val declare_uninterpretation : interp_rule -> interpretation -> unit
 
 (** Return the interpretation bound to a notation *)
-val interp_notation : ?loc:Loc.t -> notation -> local_scopes ->
+val interp_notation : ?loc:Loc.t -> notation -> subscopes ->
       interpretation * (notation_location * scope_name option)
 
 type notation_rule = interp_rule * interpretation * int option
@@ -129,13 +142,13 @@ val uninterp_ind_pattern_notations : inductive -> notation_rule list
 (** Test if a notation is available in the scopes 
    context [scopes]; if available, the result is not None; the first 
    argument is itself not None if a delimiters is needed *)
-val availability_of_notation : scope_name option * notation -> local_scopes ->
+val availability_of_notation : scope_name option * notation -> subscopes ->
   (scope_name option * delimiters option) option
 
 (** {6 Miscellaneous} *)
 
 val interp_notation_as_global_reference : ?loc:Loc.t -> (GlobRef.t -> bool) ->
-      notation -> delimiters option -> GlobRef.t
+      notation_key -> delimiters option -> GlobRef.t
 
 (** Checks for already existing notations *)
 val exists_notation_in_scope : scope_name option -> notation ->
@@ -177,8 +190,8 @@ type symbol =
 val symbol_eq : symbol -> symbol -> bool
 
 (** Make/decompose a notation of the form "_ U _" *)
-val make_notation_key : symbol list -> notation
-val decompose_notation_key : notation -> symbol list
+val make_notation_key : notation_entry_level -> symbol list -> notation
+val decompose_notation_key : notation -> notation_entry_level * symbol list
 
 (** Decompose a notation of the form "a 'U' b" *)
 val decompose_raw_notation : string -> symbol list
@@ -187,11 +200,21 @@ val decompose_raw_notation : string -> symbol list
 val pr_scope_class : scope_class -> Pp.t
 val pr_scope : (glob_constr -> Pp.t) -> scope_name -> Pp.t
 val pr_scopes : (glob_constr -> Pp.t) -> Pp.t
-val locate_notation : (glob_constr -> Pp.t) -> notation ->
+val locate_notation : (glob_constr -> Pp.t) -> notation_key ->
       scope_name option -> Pp.t
 
 val pr_visibility: (glob_constr -> Pp.t) -> scope_name option -> Pp.t
 
+type entry_coercion = notation list
+val declare_entry_coercion : notation -> notation_entry_level -> unit
+val availability_of_entry_coercion : notation_entry_level -> notation_entry_level -> entry_coercion option
+
+val declare_custom_entry_has_global : string -> int -> unit
+val declare_custom_entry_has_ident : string -> int -> unit
+
+val entry_has_global : notation_entry_level -> bool
+val entry_has_ident : notation_entry_level -> bool
+
 (** Rem: printing rules for primitive token are canonical *)
 
 val with_notation_protection : ('a -> 'b) -> 'a -> 'b