From 8d27b12365a1d8b3f1670a055537dd3724583baf Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 30 Aug 2020 08:20:29 +0200
Subject: Notations: reworking the treatment of only-parsing and only-printing
 notations.

The (old) original model for notations was to associated both a
parsing and a printing rule to a notation.

Progressively, it become more and more common to have only parsing
notations or even multiple expressions printed with the same notation.

The new model is to attach to a given scope, string and entry at most
one either only-parsing or mixed-parsing-printing rules + an
arbitrarily many unrelated only-printing rules.

Additionally, we anticipate the ability to selectively
activate/deactivate each of those.

This allows to fix in particular #9682 but also to have
more-to-the-point warnings in case a notation overrides or partially
overrides another one.

Rules for importing are not changed (see forthcoming #12984 though).

We also improve the output of "Print Scopes" so that it adds when a
notation is only-parsing, only-printing, or deactivated, or a
combination of those.

Fixes #4738
Fixes #9682
Fixes part 2 of #12908
Fixes #13112
---
 interp/notation.mli | 24 +++++++++++++++++-------
 1 file changed, 17 insertions(+), 7 deletions(-)

(limited to 'interp/notation.mli')

diff --git a/interp/notation.mli b/interp/notation.mli
index 948831b317..d744ff41d9 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -229,12 +229,24 @@ type interp_rule =
   | NotationRule of specific_notation
   | SynDefRule of KerName.t
 
-val declare_notation_interpretation : notation -> scope_name option ->
-  interpretation -> notation_location -> onlyprint:bool ->
-  Deprecation.t option -> unit
+type notation_use =
+  | OnlyPrinting
+  | OnlyParsing
+  | ParsingAndPrinting
 
 val declare_uninterpretation : interp_rule -> interpretation -> unit
 
+type entry_coercion_kind =
+  | IsEntryCoercion of notation_entry_level
+  | IsEntryGlobal of string * int
+  | IsEntryIdent of string * int
+
+val declare_notation : notation_with_optional_scope * notation ->
+  interpretation -> notation_location -> use:notation_use ->
+  entry_coercion_kind option ->
+  Deprecation.t option -> unit
+
+
 (** Return the interpretation bound to a notation *)
 val interp_notation : ?loc:Loc.t -> notation -> subscopes ->
       interpretation * (notation_location * scope_name option)
@@ -257,16 +269,14 @@ val uninterp_ind_pattern_notations : inductive -> notation_rule list
 val availability_of_notation : specific_notation -> subscopes ->
   (scope_name option * delimiters option) option
 
+val is_printing_inactive_rule : interp_rule -> interpretation -> bool
+
 (** {6 Miscellaneous} *)
 
 (** If head is true, also allows applied global references. *)
 val interp_notation_as_global_reference : ?loc:Loc.t -> head:bool -> (GlobRef.t -> bool) ->
       notation_key -> delimiters option -> GlobRef.t
 
-(** Checks for already existing notations *)
-val exists_notation_in_scope : scope_name option -> notation ->
-      bool -> interpretation -> bool
-
 (** Declares and looks for scopes associated to arguments of a global ref *)
 val declare_arguments_scope :
   bool (** true=local *) -> GlobRef.t -> scope_name option list -> unit
-- 
cgit v1.2.3