From f442efebd8354b233827e4991a80d27082c772e1 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 24 Jul 2017 20:04:46 +0200
Subject: A little reorganization of notations + a fix to #5608.

- Formerly, notations such as "{ A } + { B }" were typically split
  into "{ _ }" and "_ + _". We keep the split only for parsing, which
  is where it is really needed, but not anymore for interpretation,
  nor printing.
- As a consequence, one notation string can give rise to several
  grammar entries, but still only one printing entry.
- As another consequence, "{ A } + { B }" and "A + { B }" must be
  reserved to be used, which is after all the natural expectation,
  even if the sublevels are constrained.
- We also now keep the information "is ident", "is binder" in the
  "key" characterizing the level of a notation.
---
 interp/constrextern.ml | 36 +-----------------------------------
 interp/notation.ml     | 11 +++++++++--
 interp/notation.mli    |  2 +-
 3 files changed, 11 insertions(+), 38 deletions(-)

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 54861ae4cc..e85415bed3 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -320,38 +320,6 @@ let drop_implicits_in_patt cst nb_expl args =
        let imps = List.skipn_at_least nb_expl (select_stronger_impargs impl_st) in
        impls_fit [] (imps,args)
 
-let has_curly_brackets ntn =
-  String.length ntn >= 6 && (String.is_sub "{ _ } " ntn 0 ||
-    String.is_sub " { _ }" ntn (String.length ntn - 6) ||
-    String.string_contains ~where:ntn ~what:" { _ } ")
-
-let rec wildcards ntn n =
-  if Int.equal n (String.length ntn) then []
-  else let l = spaces ntn (n+1) in if ntn.[n] == '_' then n::l else l
-and spaces ntn n =
-  if Int.equal n (String.length ntn) then []
-  else if ntn.[n] == ' ' then wildcards ntn (n+1) else spaces ntn (n+1)
-
-let expand_curly_brackets loc mknot ntn l =
-  let ntn' = ref ntn in
-  let rec expand_ntn i =
-    function
-    | [] -> []
-    | a::l ->
-        let a' =
-          let p = List.nth (wildcards !ntn' 0) i - 2 in
-          if p>=0 && p+5 <= String.length !ntn' && String.is_sub "{ _ }" !ntn' p
-          then begin
-            ntn' :=
-              String.sub !ntn' 0 p ^ "_" ^
-              String.sub !ntn' (p+5) (String.length !ntn' -p-5);
-            mknot (loc,"{ _ }",[a]) end
-          else a in
-        a' :: expand_ntn (i+1) l in
-  let l = expand_ntn 0 l in
-  (* side effect *)
-  mknot (loc,!ntn',l)
-
 let destPrim = function { CAst.v = CPrim t } -> Some t | _ -> None
 let destPatPrim = function { CAst.v = CPatPrim t } -> Some t | _ -> None
 
@@ -367,9 +335,7 @@ let is_zero s =
   in aux 0
 
 let make_notation_gen loc ntn mknot mkprim destprim l =
-  if has_curly_brackets ntn
-  then expand_curly_brackets loc mknot ntn l
-  else match ntn,List.map destprim l with
+  match ntn,List.map destprim l with
     (* Special case to avoid writing "- 3" for e.g. (Z.opp 3) *)
     | "- _", [Some (Numeral (p,true))] when not (is_zero p) ->
         mknot (loc,ntn,([mknot (loc,"( _ )",l)]))
diff --git a/interp/notation.ml b/interp/notation.ml
index c07a009438..c7bf0e36bf 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -41,7 +41,7 @@ open Context.Named.Declaration
 (**********************************************************************)
 (* Scope of symbols *)
 
-type level = precedence * tolerability list
+type level = precedence * tolerability list * notation_var_internalization_type list
 type delimiters = string
 type notation_location = (DirPath.t * DirPath.t) * string
 
@@ -83,11 +83,18 @@ let parenRelation_eq t1 t2 = match t1, t2 with
 | Prec l1, Prec l2 -> Int.equal l1 l2
 | _ -> false
 
-let level_eq (l1, t1) (l2, t2) =
+let notation_var_internalization_type_eq v1 v2 = match v1, v2 with
+| NtnInternTypeConstr, NtnInternTypeConstr -> true
+| NtnInternTypeBinder, NtnInternTypeBinder -> true
+| NtnInternTypeIdent, NtnInternTypeIdent -> true
+| (NtnInternTypeConstr | NtnInternTypeBinder | NtnInternTypeIdent), _ -> false
+
+let level_eq (l1, t1, u1) (l2, t2, u2) =
   let tolerability_eq (i1, r1) (i2, r2) =
     Int.equal i1 i2 && parenRelation_eq r1 r2
   in
   Int.equal l1 l2 && List.equal tolerability_eq t1 t2
+  && List.equal notation_var_internalization_type_eq u1 u2
 
 let declare_scope scope =
   try let _ = String.Map.find scope !scope_map in ()
diff --git a/interp/notation.mli b/interp/notation.mli
index e63ad10cde..5f6bfa35f0 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -21,7 +21,7 @@ open Ppextend
 (** A scope is a set of interpreters for symbols + optional
    interpreter and printers for integers + optional delimiters *)
 
-type level = precedence * tolerability list
+type level = precedence * tolerability list * notation_var_internalization_type list
 type delimiters = string
 type scope
 type scopes (** = [scope_name list] *)
-- 
cgit v1.2.3


From 5db048b7f9cb5d13e44d87a1007ff042eef25fb5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 24 Jul 2017 21:01:23 +0200
Subject: A new step of restructuration of notations.

This allows to issue a more appropriate message when a notation with a
{ } cannot be defined because of an incompatible level. E.g.:

Notation "{ A } + B" := (sumbool A B) (at level 20).
---
 interp/notation.ml  |  1 -
 interp/notation.mli |  1 -
 interp/ppextend.ml  |  9 +--------
 interp/ppextend.mli | 10 ++--------
 4 files changed, 3 insertions(+), 18 deletions(-)

(limited to 'interp')

diff --git a/interp/notation.ml b/interp/notation.ml
index c7bf0e36bf..c373faf680 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -41,7 +41,6 @@ open Context.Named.Declaration
 (**********************************************************************)
 (* Scope of symbols *)
 
-type level = precedence * tolerability list * notation_var_internalization_type list
 type delimiters = string
 type notation_location = (DirPath.t * DirPath.t) * string
 
diff --git a/interp/notation.mli b/interp/notation.mli
index 5f6bfa35f0..f9f247fe10 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -21,7 +21,6 @@ open Ppextend
 (** A scope is a set of interpreters for symbols + optional
    interpreter and printers for integers + optional delimiters *)
 
-type level = precedence * tolerability list * notation_var_internalization_type list
 type delimiters = string
 type scope
 type scopes (** = [scope_name list] *)
diff --git a/interp/ppextend.ml b/interp/ppextend.ml
index 2bbe87bbca..3ebc9b71d2 100644
--- a/interp/ppextend.ml
+++ b/interp/ppextend.ml
@@ -7,17 +7,10 @@
 (************************************************************************)
 
 open Pp
+open Notation_term
 
 (*s Pretty-print. *)
 
-(* Dealing with precedences *)
-
-type precedence = int
-
-type parenRelation = L | E | Any | Prec of precedence
-
-type tolerability = precedence * parenRelation
-
 type ppbox =
   | PpHB of int
   | PpHOVB of int
diff --git a/interp/ppextend.mli b/interp/ppextend.mli
index a347a5c7b7..6ff5a42728 100644
--- a/interp/ppextend.mli
+++ b/interp/ppextend.mli
@@ -6,15 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** {6 Pretty-print. } *)
-
-(** Dealing with precedences *)
-
-type precedence = int
+open Notation_term
 
-type parenRelation = L | E | Any | Prec of precedence
-
-type tolerability = precedence * parenRelation
+(** {6 Pretty-print. } *)
 
 type ppbox =
   | PpHB of int
-- 
cgit v1.2.3