From d4c2ed95fcfd64cdcc10e51e40be739d9f1c4a74 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 13 Aug 2017 20:05:03 +0200
Subject: Allows recursive patterns for binders to be associative on the left.

This makes treatment of recursive binders closer to the one of
recursive terms. It is unclear whether there are interesting notations
liable to use this, but this shall make easier mixing recursive
binders and recursive terms as in next commits.

Example of (artificial) notation that this commit supports:

  Notation "! x .. y # A #" :=
    (.. (A,(forall x, True)) ..,(forall y, True))
    (at level 200, x binder).
---
 interp/notation.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index 94ce2a6c8d..31f16e1a90 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -292,7 +292,7 @@ let cases_pattern_key c = match DAst.get c with
 let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
   | NApp (NRef ref,args) -> RefKey(canonical_gr ref), Some (List.length args)
   | NList (_,_,NApp (NRef ref,args),_,_)
-  | NBinderList (_,_,NApp (NRef ref,args),_) ->
+  | NBinderList (_,_,NApp (NRef ref,args),_,_) ->
       RefKey (canonical_gr ref), Some (List.length args)
   | NRef ref -> RefKey(canonical_gr ref), None
   | NApp (_,args) -> Oth, Some (List.length args)
-- 
cgit v1.2.3


From edd0d22429354a5f2c703a8c7bd1f775e2f97d9e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 12 Aug 2017 09:15:40 +0200
Subject: Adding support for parsing subterms of a notation as "pattern".

This allows in particular to define notations with 'pat style binders.

E.g.:

A non-trivial change in this commit is storing binders and patterns
separately from terms.

This is not strictly necessary but has some advantages.

However, it is relatively common to have binders also used as terms,
or binders parsed as terms. Thus, it is already relatively common to
embed binders into terms (see e.g. notation for ETA in output test
Notations3.v) or to coerce terms to idents (see e.g. the notation for
{x|P} where x is parsed as a constr).

So, it is as simple to always store idents (and eventually patterns)
as terms.
---
 interp/notation.ml | 29 +++++++++++++++++++++--------
 1 file changed, 21 insertions(+), 8 deletions(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index 31f16e1a90..e6186e08c2 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -82,18 +82,31 @@ let parenRelation_eq t1 t2 = match t1, t2 with
 | Prec l1, Prec l2 -> Int.equal l1 l2
 | _ -> false
 
-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
+open Extend
+
+let production_level_eq l1 l2 = true (* (l1 = l2) *)
+
+let production_position_eq pp1 pp2 = true (* pp1 = pp2 *) (* match pp1, pp2 with
+| NextLevel, NextLevel -> true
+| NumLevel n1, NumLevel n2 -> Int.equal n1 n2
+| (NextLevel | NumLevel _), _ -> false *)
+
+let constr_entry_key_eq v1 v2 = match v1, v2 with
+| ETName, ETName -> true
+| ETReference, ETReference -> true
+| ETBigint, ETBigint -> true
+| ETBinder b1, ETBinder b2 -> b1 == b2
+| ETConstr (n1,pp1), ETConstr (n2,pp2) -> production_level_eq n1 n2 && production_position_eq pp1 pp2
+| ETPattern n1, ETPattern n2 -> 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 _), _ -> 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
+  && List.equal constr_entry_key_eq u1 u2
 
 let declare_scope scope =
   try let _ = String.Map.find scope !scope_map in ()
@@ -611,10 +624,10 @@ let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2
 
 let ntpe_eq t1 t2 = match t1, t2 with
 | NtnTypeConstr, NtnTypeConstr -> true
-| NtnTypeOnlyBinder, NtnTypeOnlyBinder -> true
+| NtnTypeBinder b1, NtnTypeBinder b2 -> b1 = (b2:bool)
 | NtnTypeConstrList, NtnTypeConstrList -> true
 | NtnTypeBinderList, NtnTypeBinderList -> true
-| (NtnTypeConstr | NtnTypeOnlyBinder | NtnTypeConstrList | NtnTypeBinderList), _ -> false
+| (NtnTypeConstr | NtnTypeBinder _ | NtnTypeConstrList | NtnTypeBinderList), _ -> false
 
 let var_attributes_eq (_, (sc1, tp1)) (_, (sc2, tp2)) =
   pair_eq (Option.equal String.equal) (List.equal String.equal) sc1 sc2 &&
-- 
cgit v1.2.3


From 3a6b1d2c04ceeb568accbc9ddfc3fc0f14faf25b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 17 Aug 2017 12:35:56 +0200
Subject: Respecting the ident/pattern distinction in notation modifiers.

---
 interp/notation.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index e6186e08c2..e2e769d2fc 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -622,9 +622,15 @@ let availability_of_prim_token n printer_scope local_scopes =
 
 let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2
 
+let notation_binder_source_eq s1 s2 = match s1, s2 with
+   | NtnParsedAsConstr, NtnParsedAsConstr -> true
+   | NtnParsedAsIdent,  NtnParsedAsIdent -> true
+   | NtnParsedAsPattern, NtnParsedAsPattern -> true
+   | (NtnParsedAsConstr | NtnParsedAsIdent | NtnParsedAsPattern), _ -> false
+
 let ntpe_eq t1 t2 = match t1, t2 with
 | NtnTypeConstr, NtnTypeConstr -> true
-| NtnTypeBinder b1, NtnTypeBinder b2 -> b1 = (b2:bool)
+| NtnTypeBinder s1, NtnTypeBinder s2 -> notation_binder_source_eq s1 s2
 | NtnTypeConstrList, NtnTypeConstrList -> true
 | NtnTypeBinderList, NtnTypeBinderList -> true
 | (NtnTypeConstr | NtnTypeBinder _ | NtnTypeConstrList | NtnTypeBinderList), _ -> false
-- 
cgit v1.2.3


From b176959335a8cc097c254ea10b910e8ecbcde54b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 24 Aug 2017 21:14:43 +0200
Subject: More flexibility in locating or referring to a notation.

We generalize the possibility to refer to a notation not only by its
"_ U _" form but also using its "a 'U' b".

(Wish from EJGA)
---
 interp/notation.ml | 59 ++++++++++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 57 insertions(+), 2 deletions(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index e2e769d2fc..c1b66f7d61 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -945,8 +945,63 @@ let factorize_entries = function
 	  (ntn,[c],[]) l in
       (ntn,l_of_ntn)::rest
 
+type symbol_token = WhiteSpace of int | String of string
+
+let split_notation_string str =
+  let push_token beg i l =
+    if Int.equal beg i then l else
+      let s = String.sub str beg (i - beg) in
+      String s :: l
+  in
+  let push_whitespace beg i l =
+    if Int.equal beg i then l else WhiteSpace (i-beg) :: l
+  in
+  let rec loop beg i =
+    if i < String.length str then
+      if str.[i] == ' ' then
+        push_token beg i (loop_on_whitespace (i+1) (i+1))
+      else
+        loop beg (i+1)
+    else
+      push_token beg i []
+  and loop_on_whitespace beg i =
+    if i < String.length str then
+      if str.[i] != ' ' then
+        push_whitespace beg i (loop i (i+1))
+      else
+        loop_on_whitespace beg (i+1)
+    else
+      push_whitespace beg i []
+  in
+  loop 0 0
+
+let rec raw_analyze_notation_tokens = function
+  | []    -> []
+  | String ".." :: sl -> NonTerminal Notation_ops.ldots_var :: raw_analyze_notation_tokens sl
+  | String "_" :: _ -> user_err Pp.(str "_ must be quoted.")
+  | String x :: sl when Id.is_valid x ->
+      NonTerminal (Names.Id.of_string x) :: raw_analyze_notation_tokens sl
+  | String s :: sl ->
+      Terminal (String.drop_simple_quotes s) :: raw_analyze_notation_tokens sl
+  | WhiteSpace n :: sl ->
+      Break n :: raw_analyze_notation_tokens sl
+
+let decompose_raw_notation ntn = raw_analyze_notation_tokens (split_notation_string ntn)
+
+let possible_notations ntn =
+  (* We collect the possible interpretations of a notation string depending on whether it is
+    in "x 'U' y" or "_ U _" format *)
+  let toks = split_notation_string ntn in
+  if List.exists (function String "_" -> true | _ -> false) toks then
+    (* Only "_ U _" format *)
+    [ntn]
+  else
+    let ntn' = make_notation_key (raw_analyze_notation_tokens toks) in
+    if String.equal ntn ntn' then (* Only symbols *) [ntn] else [ntn;ntn']
+
 let browse_notation strict ntn map =
-  let find ntn' =
+  let ntns = possible_notations ntn in
+  let find ntn' ntn =
     if String.contains ntn ' ' then String.equal ntn ntn'
     else
       let toks = decompose_notation_key ntn' in
@@ -959,7 +1014,7 @@ let browse_notation strict ntn map =
     String.Map.fold
       (fun scope_name sc ->
 	String.Map.fold (fun ntn { not_interp  = (_, r); not_location = df } l ->
-	  if find ntn then (ntn,(scope_name,r,df))::l else l) sc.notations)
+          if List.exists (find ntn) ntns then (ntn,(scope_name,r,df))::l else l) sc.notations)
       map [] in
   List.sort (fun x y -> String.compare (fst x) (fst y)) l
 
-- 
cgit v1.2.3


From 8f93f9a2df6e17386f46f79b2a7eda4104d0a94e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 25 Nov 2017 17:09:21 +0100
Subject: Notations: A step in cleaning constr_entry_key.

- Avoid dummy use of unit
- Do not decide as early as parsing the default level for pattern
- Prepare to further extensions
---
 interp/notation.ml | 19 +++++++++++--------
 1 file changed, 11 insertions(+), 8 deletions(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index c1b66f7d61..13ff960f64 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -91,22 +91,25 @@ let production_position_eq pp1 pp2 = true (* pp1 = pp2 *) (* match pp1, pp2 with
 | NumLevel n1, NumLevel n2 -> Int.equal n1 n2
 | (NextLevel | NumLevel _), _ -> false *)
 
-let constr_entry_key_eq v1 v2 = match v1, v2 with
+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 (n1,pp1), ETConstr (n2,pp2) -> production_level_eq n1 n2 && production_position_eq pp1 pp2
-| ETPattern n1, ETPattern n2 -> Int.equal n1 n2
+| ETConstr lev1, ETConstr lev2 -> eq lev1 lev2
+| ETPattern n1, ETPattern n2 -> 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 _), _ -> 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
+let level_eq_gen strict (l1, t1, u1) (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
-  && List.equal constr_entry_key_eq u1 u2
+  && List.equal (constr_entry_key_eq prod_eq) u1 u2
+
+let level_eq = level_eq_gen false
 
 let declare_scope scope =
   try let _ = String.Map.find scope !scope_map in ()
-- 
cgit v1.2.3


From dcfd5c2c2cefcd8ae6a5b2e90fcbd98da4f1b120 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 25 Nov 2017 20:50:03 +0100
Subject: Notations: Adding modifiers to tell which kind of binder a constr can
 parse.

Concretely, we provide "constr as ident", "constr as strict pattern"
and "constr as pattern".

This tells to parse a binder as a constr, restricting to only ident or
to only a strict pattern, or to a pattern which can also be an ident.

The "strict pattern" modifier allows to restrict the use of patterns
in printing rules. This allows e.g. to select the appropriate rule for
printing between {x|P} and {'pat|P}.
---
 interp/notation.ml | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index 13ff960f64..ea7ef21b19 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -97,9 +97,10 @@ let constr_entry_key_eq eq v1 v2 = match v1, v2 with
 | ETBigint, ETBigint -> true
 | ETBinder b1, ETBinder b2 -> b1 == b2
 | ETConstr lev1, ETConstr lev2 -> eq lev1 lev2
-| ETPattern n1, ETPattern n2 -> Option.equal Int.equal n1 n2
+| ETConstrAsBinder (bk1,lev1), ETConstrAsBinder (bk2,lev2) -> eq lev1 lev2 && bk1 = bk2
+| 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 _), _ -> false
+| (ETName | ETReference | ETBigint | ETBinder _ | ETConstr _ | ETPattern _ | ETOther _ | ETConstrAsBinder _), _ -> false
 
 let level_eq_gen strict (l1, t1, u1) (l2, t2, u2) =
   let tolerability_eq (i1, r1) (i2, r2) = Int.equal i1 i2 && parenRelation_eq r1 r2 in
@@ -626,10 +627,10 @@ let availability_of_prim_token n printer_scope local_scopes =
 let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2
 
 let notation_binder_source_eq s1 s2 = match s1, s2 with
-   | NtnParsedAsConstr, NtnParsedAsConstr -> true
-   | NtnParsedAsIdent,  NtnParsedAsIdent -> true
-   | NtnParsedAsPattern, NtnParsedAsPattern -> true
-   | (NtnParsedAsConstr | NtnParsedAsIdent | NtnParsedAsPattern), _ -> false
+| NtnParsedAsIdent,  NtnParsedAsIdent -> true
+| NtnParsedAsPattern b1, NtnParsedAsPattern b2 -> b1 = b2
+| NtnBinderParsedAsConstr bk1, NtnBinderParsedAsConstr bk2 -> bk1 = bk2
+| (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnBinderParsedAsConstr _), _ -> false
 
 let ntpe_eq t1 t2 = match t1, t2 with
 | NtnTypeConstr, NtnTypeConstr -> true
-- 
cgit v1.2.3