From 407e154baa44609dea9f6f1ade746e24d60e2513 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 9 Aug 2017 14:00:26 +0200
Subject: Rephrasing ETBinderList with a self-documenting and
 invariant-carrying argument.

---
 parsing/egramcoq.ml | 19 +++++++++----------
 1 file changed, 9 insertions(+), 10 deletions(-)

(limited to 'parsing')

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index ea6266dd44..16124c26c3 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -232,8 +232,8 @@ type (_, _) entry =
 | TTBinder : ('self, local_binder_expr list) entry
 | TTConstr : prod_info * 'r target -> ('r, 'r) entry
 | TTConstrList : prod_info * Tok.t list * 'r target -> ('r, 'r list) entry
-| TTBinderListT : ('self, local_binder_expr list) entry
-| TTBinderListF : Tok.t list -> ('self, local_binder_expr list list) entry
+| TTOpenBinderList : ('self, local_binder_expr list) entry
+| TTClosedBinderList : Tok.t list -> ('self, local_binder_expr list list) entry
 
 type _ any_entry = TTAny : ('s, 'r) entry -> 's any_entry
 
@@ -289,11 +289,11 @@ let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) symbol = fun as
   Alist1 (symbol_of_target typ' assoc from forpat)
 | TTConstrList (typ', tkl, forpat) ->
   Alist1sep (symbol_of_target typ' assoc from forpat, make_sep_rules tkl)
-| TTBinderListF [] -> Alist1 (Aentry Constr.binder)
-| TTBinderListF tkl -> Alist1sep (Aentry Constr.binder, make_sep_rules tkl)
+| TTClosedBinderList [] -> Alist1 (Aentry Constr.binder)
+| TTClosedBinderList tkl -> Alist1sep (Aentry Constr.binder, make_sep_rules tkl)
 | TTName -> Aentry Prim.name
 | TTBinder -> Aentry Constr.binder
-| TTBinderListT -> Aentry Constr.open_binders
+| TTOpenBinderList -> Aentry Constr.open_binders
 | TTBigint -> Aentry Prim.bigint
 | TTReference -> Aentry Constr.global
 
@@ -307,9 +307,8 @@ let interp_entry forpat e = match e with
 | ETPattern -> assert false (** not used *)
 | ETOther _ -> assert false (** not used *)
 | ETConstrList (p, tkl) -> TTAny (TTConstrList (p, tkl, forpat))
-| ETBinderList (true, []) -> TTAny TTBinderListT
-| ETBinderList (true, _) -> assert false
-| ETBinderList (false, tkl) -> TTAny (TTBinderListF tkl)
+| ETBinderList ETBinderOpen -> TTAny TTOpenBinderList
+| ETBinderList (ETBinderClosed tkl) -> TTAny (TTClosedBinderList tkl)
 
 let constr_expr_of_name (loc,na) = CAst.make ?loc @@ match na with
   | Anonymous -> CHole (None,Misctypes.IntroAnonymous,None)
@@ -336,8 +335,8 @@ match e with
   | ForPattern -> push_constr subst (cases_pattern_expr_of_name v)
   end
 | TTBinder -> { subst with binders = (v, true) :: subst.binders }
-| TTBinderListT -> { subst with binders = (v, true) :: subst.binders }
-| TTBinderListF _ -> { subst with binders = (List.flatten v, false) :: subst.binders }
+| TTOpenBinderList -> { subst with binders = (v, true) :: subst.binders }
+| TTClosedBinderList _ -> { subst with binders = (List.flatten v, false) :: subst.binders }
 | TTBigint ->
   begin match forpat with
   | ForConstr ->  push_constr subst (CAst.make @@ CPrim (Numeral (v,true)))
-- 
cgit v1.2.3


From 351e9acd3aa11a751129f5956fe991fc4d0bf0b8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 11 Aug 2017 19:24:50 +0200
Subject: Introducing an intermediary type "constr_prod_entry_key" for grammar
 productions.

This type describes the grammar non-terminal. It typically contains
ETConstrList (now renamed ETProdConstrList) but not ETBinder. It is
the type for metasyntax.ml and egramcoq.ml to communicate together.

The type constr_prod_entry_key with ETConstr, ETBinder, is now used
only in metasyntax.ml. This allows to get rid of some "assert false"
in uselessly matching over ETConstrList in metasyntax.ml and of some
"assert false" in uselessly matching over ETBinder in egramcoq.ml.

Also exporting less of extend.mli in API.
---
 parsing/egramcoq.ml | 23 +++++++++--------------
 1 file changed, 9 insertions(+), 14 deletions(-)

(limited to 'parsing')

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 16124c26c3..3c4f408f86 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -229,7 +229,6 @@ type (_, _) entry =
 | TTName : ('self, Name.t Loc.located) entry
 | TTReference : ('self, reference) entry
 | TTBigint : ('self, Constrexpr.raw_natural_number) entry
-| TTBinder : ('self, local_binder_expr list) entry
 | TTConstr : prod_info * 'r target -> ('r, 'r) entry
 | TTConstrList : prod_info * Tok.t list * 'r target -> ('r, 'r list) entry
 | TTOpenBinderList : ('self, local_binder_expr list) entry
@@ -292,23 +291,20 @@ let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) symbol = fun as
 | TTClosedBinderList [] -> Alist1 (Aentry Constr.binder)
 | TTClosedBinderList tkl -> Alist1sep (Aentry Constr.binder, make_sep_rules tkl)
 | TTName -> Aentry Prim.name
-| TTBinder -> Aentry Constr.binder
 | TTOpenBinderList -> Aentry Constr.open_binders
 | TTBigint -> Aentry Prim.bigint
 | TTReference -> Aentry Constr.global
 
 let interp_entry forpat e = match e with
-| ETName -> TTAny TTName
-| ETReference -> TTAny TTReference
-| ETBigint -> TTAny TTBigint
-| ETBinder true -> anomaly (Pp.str "Should occur only as part of BinderList.")
-| ETBinder false  -> TTAny TTBinder
-| ETConstr p -> TTAny (TTConstr (p, forpat))
-| ETPattern -> assert false (** not used *)
-| ETOther _ -> assert false (** not used *)
-| ETConstrList (p, tkl) -> TTAny (TTConstrList (p, tkl, forpat))
-| ETBinderList ETBinderOpen -> TTAny TTOpenBinderList
-| ETBinderList (ETBinderClosed tkl) -> TTAny (TTClosedBinderList tkl)
+| ETProdName -> TTAny TTName
+| ETProdReference -> TTAny TTReference
+| ETProdBigint -> TTAny TTBigint
+| ETProdConstr p -> TTAny (TTConstr (p, forpat))
+| ETProdPattern -> assert false (** not used *)
+| ETProdOther _ -> assert false (** not used *)
+| ETProdConstrList (p, tkl) -> TTAny (TTConstrList (p, tkl, forpat))
+| ETProdBinderList ETBinderOpen -> TTAny TTOpenBinderList
+| ETProdBinderList (ETBinderClosed tkl) -> TTAny (TTClosedBinderList tkl)
 
 let constr_expr_of_name (loc,na) = CAst.make ?loc @@ match na with
   | Anonymous -> CHole (None,Misctypes.IntroAnonymous,None)
@@ -334,7 +330,6 @@ match e with
   | ForConstr -> push_constr subst (constr_expr_of_name v)
   | ForPattern -> push_constr subst (cases_pattern_expr_of_name v)
   end
-| TTBinder -> { subst with binders = (v, true) :: subst.binders }
 | TTOpenBinderList -> { subst with binders = (v, true) :: subst.binders }
 | TTClosedBinderList _ -> { subst with binders = (List.flatten v, false) :: subst.binders }
 | TTBigint ->
-- 
cgit v1.2.3


From 00c3248a80253eb28a3779e8640101d8c83ab5d2 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 11 Aug 2017 20:55:23 +0200
Subject: Renaming binders into binderlists in egramcoq.ml.

---
 parsing/egramcoq.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'parsing')

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 3c4f408f86..4fd84eac50 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -317,7 +317,7 @@ let cases_pattern_expr_of_name (loc,na) = CAst.make ?loc @@ match na with
 type 'r env = {
   constrs : 'r list;
   constrlists : 'r list list;
-  binders : (local_binder_expr list * bool) list;
+  binderlists : (local_binder_expr list * bool) list;
 }
 
 let push_constr subst v = { subst with constrs = v :: subst.constrs }
@@ -330,8 +330,8 @@ match e with
   | ForConstr -> push_constr subst (constr_expr_of_name v)
   | ForPattern -> push_constr subst (cases_pattern_expr_of_name v)
   end
-| TTOpenBinderList -> { subst with binders = (v, true) :: subst.binders }
-| TTClosedBinderList _ -> { subst with binders = (List.flatten v, false) :: subst.binders }
+| TTOpenBinderList -> { subst with binderlists = (v, true) :: subst.binderlists }
+| TTClosedBinderList _ -> { subst with binderlists = (List.flatten v, false) :: subst.binderlists }
 | TTBigint ->
   begin match forpat with
   | ForConstr ->  push_constr subst (CAst.make @@ CPrim (Numeral (v,true)))
@@ -431,10 +431,10 @@ let rec pure_sublevels : type a b c. int option -> (a, b, c) rule -> int list =
 
 let make_act : type r. r target -> _ -> r gen_eval = function
 | ForConstr -> fun notation loc env ->
-  let env = (env.constrs, env.constrlists, List.map fst env.binders) in
+  let env = (env.constrs, env.constrlists, List.map fst env.binderlists) in
   CAst.make ~loc @@ CNotation (notation , env)
 | ForPattern -> fun notation loc env ->
-  let invalid = List.exists (fun (_, b) -> not b) env.binders in
+  let invalid = List.exists (fun (_, b) -> not b) env.binderlists in
   let () = if invalid then Constrexpr_ops.error_invalid_pattern_notation ~loc () in
   let env = (env.constrs, env.constrlists) in
   CAst.make ~loc @@ CPatNotation (notation, env, [])
@@ -451,7 +451,7 @@ let extend_constr state forpat ng =
     let needed_levels, state = register_empty_levels state isforpat pure_sublevels in
     let (pos,p4assoc,name,reinit), state = find_position state isforpat assoc level in
     let empty_rules = List.map (prepare_empty_levels isforpat) needed_levels in
-    let empty = { constrs = []; constrlists = []; binders = [] } in
+    let empty = { constrs = []; constrlists = []; binderlists = [] } in
     let act = ty_eval r (make_act forpat ng.notgram_notation) empty in
     let rule = (name, p4assoc, [Rule (symbs, act)]) in
     let r = ExtendRule (entry, reinit, (pos, [rule])) in
-- 
cgit v1.2.3


From 398358618bb3eabfe822b79c669703c1c33b67e6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 15 Aug 2017 18:32:02 +0200
Subject: Adding patterns in the category of binders for notations.

For instance, the following is now possible:

  Check {(x,y)|x+y=0}.

Some questions remains. Maybe, by consistency, the notation should be
"{'(x,y)|x+y=0}"...
---
 parsing/g_constr.ml4 | 12 +-----------
 1 file changed, 1 insertion(+), 11 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index db68a75e09..4c55f3ec65 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -387,17 +387,7 @@ GEXTEND Gram
     | "10" LEFTA
       [ p = pattern; "as"; id = ident ->
         CAst.make ~loc:!@loc @@ CPatAlias (p, id)
-      | p = pattern; lp = LIST1 NEXT ->
-        (let open CAst in match p with
-	  | { v = CPatAtom (Some r) } -> CAst.make ~loc:!@loc @@ CPatCstr (r, None, lp)
-	  | { v = CPatCstr (r, None, l2); loc } ->
-                 CErrors.user_err ?loc ~hdr:"compound_pattern"
-                 (Pp.str "Nested applications not supported.")
-	  | { v = CPatCstr (r, l1, l2) }  -> CAst.make ~loc:!@loc @@ CPatCstr (r, l1 , l2@lp)
-	  | { v = CPatNotation (n, s, l) } -> CAst.make ~loc:!@loc @@ CPatNotation (n , s, l@lp)
-          | _ -> CErrors.user_err
-                 ?loc:(cases_pattern_expr_loc p) ~hdr:"compound_pattern"
-                 (Pp.str "Such pattern cannot have arguments."))
+      | p = pattern; lp = LIST1 NEXT -> mkAppPattern ~loc:!@loc p lp
       | "@"; r = Prim.reference; lp = LIST0 NEXT ->
         CAst.make ~loc:!@loc @@ CPatCstr (r, Some lp, []) ]
     | "1" LEFTA
-- 
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.
---
 parsing/egramcoq.ml  | 30 ++++++++++++++++--------------
 parsing/g_constr.ml4 |  8 ++++----
 parsing/g_vernac.ml4 |  2 ++
 3 files changed, 22 insertions(+), 18 deletions(-)

(limited to 'parsing')

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 4fd84eac50..a3d2571549 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -231,6 +231,7 @@ type (_, _) entry =
 | TTBigint : ('self, Constrexpr.raw_natural_number) entry
 | TTConstr : prod_info * 'r target -> ('r, 'r) entry
 | TTConstrList : prod_info * Tok.t list * 'r target -> ('r, 'r list) entry
+| TTPattern : int -> ('self, cases_pattern_expr) entry
 | TTOpenBinderList : ('self, local_binder_expr list) entry
 | TTClosedBinderList : Tok.t list -> ('self, local_binder_expr list list) entry
 
@@ -288,6 +289,7 @@ let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) symbol = fun as
   Alist1 (symbol_of_target typ' assoc from forpat)
 | TTConstrList (typ', tkl, forpat) ->
   Alist1sep (symbol_of_target typ' assoc from forpat, make_sep_rules tkl)
+| TTPattern p -> Aentryl (Constr.pattern, p)
 | TTClosedBinderList [] -> Alist1 (Aentry Constr.binder)
 | TTClosedBinderList tkl -> Alist1sep (Aentry Constr.binder, make_sep_rules tkl)
 | TTName -> Aentry Prim.name
@@ -300,16 +302,12 @@ let interp_entry forpat e = match e with
 | ETProdReference -> TTAny TTReference
 | ETProdBigint -> TTAny TTBigint
 | ETProdConstr p -> TTAny (TTConstr (p, forpat))
-| ETProdPattern -> assert false (** not used *)
+| ETProdPattern p -> TTAny (TTPattern p)
 | ETProdOther _ -> assert false (** not used *)
 | ETProdConstrList (p, tkl) -> TTAny (TTConstrList (p, tkl, forpat))
 | ETProdBinderList ETBinderOpen -> TTAny TTOpenBinderList
 | ETProdBinderList (ETBinderClosed tkl) -> TTAny (TTClosedBinderList tkl)
 
-let constr_expr_of_name (loc,na) = CAst.make ?loc @@ match na with
-  | Anonymous -> CHole (None,Misctypes.IntroAnonymous,None)
-  | Name id   -> CRef (Ident (Loc.tag ?loc id), None)
-
 let cases_pattern_expr_of_name (loc,na) = CAst.make ?loc @@ match na with
   | Anonymous -> CPatAtom None
   | Name id   -> CPatAtom (Some (Ident (Loc.tag ?loc id)))
@@ -317,7 +315,8 @@ let cases_pattern_expr_of_name (loc,na) = CAst.make ?loc @@ match na with
 type 'r env = {
   constrs : 'r list;
   constrlists : 'r list list;
-  binderlists : (local_binder_expr list * bool) list;
+  binders : cases_pattern_expr list;
+  binderlists : local_binder_expr list list;
 }
 
 let push_constr subst v = { subst with constrs = v :: subst.constrs }
@@ -327,11 +326,16 @@ match e with
 | TTConstr _ -> push_constr subst v
 | TTName ->
   begin match forpat with
-  | ForConstr -> push_constr subst (constr_expr_of_name v)
+  | ForConstr -> { subst with binders = cases_pattern_expr_of_name v :: subst.binders }
   | ForPattern -> push_constr subst (cases_pattern_expr_of_name v)
   end
-| TTOpenBinderList -> { subst with binderlists = (v, true) :: subst.binderlists }
-| TTClosedBinderList _ -> { subst with binderlists = (List.flatten v, false) :: subst.binderlists }
+| TTPattern _ ->
+  begin match forpat with
+  | ForConstr -> { subst with binders = v :: subst.binders }
+  | ForPattern -> push_constr subst v
+  end
+| TTOpenBinderList -> { subst with binderlists = v :: subst.binderlists }
+| TTClosedBinderList _ -> { subst with binderlists = List.flatten v :: subst.binderlists }
 | TTBigint ->
   begin match forpat with
   | ForConstr ->  push_constr subst (CAst.make @@ CPrim (Numeral (v,true)))
@@ -431,11 +435,9 @@ let rec pure_sublevels : type a b c. int option -> (a, b, c) rule -> int list =
 
 let make_act : type r. r target -> _ -> r gen_eval = function
 | ForConstr -> fun notation loc env ->
-  let env = (env.constrs, env.constrlists, List.map fst env.binderlists) in
-  CAst.make ~loc @@ CNotation (notation , env)
+  let env = (env.constrs, env.constrlists, env.binders, env.binderlists) in
+  CAst.make ~loc @@ CNotation (notation, env)
 | ForPattern -> fun notation loc env ->
-  let invalid = List.exists (fun (_, b) -> not b) env.binderlists in
-  let () = if invalid then Constrexpr_ops.error_invalid_pattern_notation ~loc () in
   let env = (env.constrs, env.constrlists) in
   CAst.make ~loc @@ CPatNotation (notation, env, [])
 
@@ -451,7 +453,7 @@ let extend_constr state forpat ng =
     let needed_levels, state = register_empty_levels state isforpat pure_sublevels in
     let (pos,p4assoc,name,reinit), state = find_position state isforpat assoc level in
     let empty_rules = List.map (prepare_empty_levels isforpat) needed_levels in
-    let empty = { constrs = []; constrlists = []; binderlists = [] } in
+    let empty = { constrs = []; constrlists = []; binders = []; binderlists = [] } in
     let act = ty_eval r (make_act forpat ng.notgram_notation) empty in
     let rule = (name, p4assoc, [Rule (symbs, act)]) in
     let r = ExtendRule (entry, reinit, (pos, [rule])) in
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 4c55f3ec65..c2ce003f13 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -120,7 +120,7 @@ let name_colon =
               | _ -> err ())
         | _ -> err ())
 
-let aliasvar = function { CAst.loc = loc; CAst.v = CPatAlias (_, id) } -> Some (loc,Name id) | _ -> None
+let aliasvar = function { CAst.v = CPatAlias (_, na) } -> Some na | _ -> None
 
 GEXTEND Gram
   GLOBAL: binder_constr lconstr constr operconstr universe_level sort sort_family
@@ -216,7 +216,7 @@ GEXTEND Gram
       | "("; c = operconstr LEVEL "200"; ")" ->
           (match c.CAst.v with
             | CPrim (Numeral (n,true)) ->
-                CAst.make ~loc:(!@loc) @@ CNotation("( _ )",([c],[],[]))
+                CAst.make ~loc:(!@loc) @@ CNotation("( _ )",([c],[],[],[]))
             | _ -> c)
       | "{|"; c = record_declaration; "|}" -> c
       | "`{"; c = operconstr LEVEL "200"; "}" ->
@@ -385,8 +385,8 @@ GEXTEND Gram
     | "99" RIGHTA [ ]
     | "90" RIGHTA [ ]
     | "10" LEFTA
-      [ p = pattern; "as"; id = ident ->
-        CAst.make ~loc:!@loc @@ CPatAlias (p, id)
+      [ p = pattern; "as"; na = name ->
+        CAst.make ~loc:!@loc @@ CPatAlias (p, na)
       | p = pattern; lp = LIST1 NEXT -> mkAppPattern ~loc:!@loc p lp
       | "@"; r = Prim.reference; lp = LIST0 NEXT ->
         CAst.make ~loc:!@loc @@ CPatCstr (r, Some lp, []) ]
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index d42b5f622c..6ef0b4fa88 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -1181,6 +1181,8 @@ GEXTEND Gram
     [ [ IDENT "ident" -> ETName | IDENT "global" -> ETReference
       | IDENT "bigint" -> ETBigint
       | IDENT "binder" -> ETBinder true
+      | IDENT "pattern" -> ETPattern 0
+      | IDENT "pattern"; "at"; IDENT "level"; n = natural -> ETPattern n
       | IDENT "closed"; IDENT "binder" -> ETBinder false
     ] ]
   ;
-- 
cgit v1.2.3


From 69822345c198aa6bf51354f6b84c7fd5d401bc9c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 23 Aug 2017 20:32:15 +0200
Subject: Moving Metasyntax.register_grammar to Pcoq for usability in Egramcoq.

Renaming it register_grammars_by_name.
---
 parsing/pcoq.ml  | 12 ++++++++++++
 parsing/pcoq.mli |  7 +++++++
 2 files changed, 19 insertions(+)

(limited to 'parsing')

diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 54e7949aea..ddb26d7717 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -638,3 +638,15 @@ let () =
   Grammar.register0 wit_constr (Constr.constr);
   Grammar.register0 wit_red_expr (Vernac_.red_expr);
   ()
+
+(** Registering extra grammar *)
+
+type any_entry = AnyEntry : 'a Gram.entry -> any_entry
+
+let grammar_names : any_entry list String.Map.t ref = ref String.Map.empty
+
+let register_grammars_by_name name grams =
+  grammar_names := String.Map.add name grams !grammar_names
+
+let find_grammars_by_name name =
+  String.Map.find name !grammar_names
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 75378d2c66..accb51366b 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -315,3 +315,10 @@ val (!@) : Ploc.t -> Loc.t
 
 type frozen_t
 val parser_summary_tag : frozen_t Summary.Dyn.tag
+
+(** Registering grammars by name *)
+
+type any_entry = AnyEntry : 'a Gram.entry -> any_entry
+
+val register_grammars_by_name : string -> any_entry list -> unit
+val find_grammars_by_name : string -> any_entry list
-- 
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
---
 parsing/g_vernac.ml4 | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 6ef0b4fa88..009c1c19a6 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -1181,8 +1181,8 @@ GEXTEND Gram
     [ [ IDENT "ident" -> ETName | IDENT "global" -> ETReference
       | IDENT "bigint" -> ETBigint
       | IDENT "binder" -> ETBinder true
-      | IDENT "pattern" -> ETPattern 0
-      | IDENT "pattern"; "at"; IDENT "level"; n = natural -> ETPattern n
+      | IDENT "pattern" -> ETPattern None
+      | IDENT "pattern"; "at"; IDENT "level"; n = natural -> ETPattern (Some n)
       | IDENT "closed"; IDENT "binder" -> ETBinder false
     ] ]
   ;
-- 
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}.
---
 parsing/g_vernac.ml4 | 16 ++++++++++++++--
 1 file changed, 14 insertions(+), 2 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 009c1c19a6..cca1b29898 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -1174,6 +1174,7 @@ GEXTEND Gram
       | x = IDENT; ","; l = LIST1 [id = IDENT -> id ] SEP ","; "at";
         lev = level -> SetItemLevel (x::l,lev)
       | x = IDENT; "at"; lev = level -> SetItemLevel ([x],lev)
+      | x = IDENT; "at"; lev = level; b = constr_as_binder_kind -> SetItemLevelAsBinder ([x],b,lev)
       | x = IDENT; typ = syntax_extension_type -> SetEntryType (x,typ)
     ] ]
   ;
@@ -1181,9 +1182,20 @@ GEXTEND Gram
     [ [ IDENT "ident" -> ETName | IDENT "global" -> ETReference
       | IDENT "bigint" -> ETBigint
       | IDENT "binder" -> ETBinder true
-      | IDENT "pattern" -> ETPattern None
-      | IDENT "pattern"; "at"; IDENT "level"; n = natural -> ETPattern (Some n)
+      | IDENT "constr"; n = OPT at_level; b = constr_as_binder_kind -> ETConstrAsBinder (b,n)
+      | IDENT "pattern" -> ETPattern (false,None)
+      | IDENT "pattern"; "at"; IDENT "level"; n = natural -> ETPattern (false,Some n)
+      | IDENT "strict"; IDENT "pattern" -> ETPattern (true,None)
+      | IDENT "strict"; IDENT "pattern"; "at"; IDENT "level"; n = natural -> ETPattern (true,Some n)
       | IDENT "closed"; IDENT "binder" -> ETBinder false
     ] ]
   ;
+  at_level:
+    [ [ "at"; n = level -> n ] ]
+  ;
+  constr_as_binder_kind:
+    [ [ "as"; IDENT "ident" -> AsIdent
+      | "as"; IDENT "pattern" -> AsIdentOrPattern
+      | "as"; IDENT "strict"; IDENT "pattern" -> AsStrictPattern ] ]
+  ;
 END
-- 
cgit v1.2.3


From 0c4eea2553d5b3b70d0b5baaf92781a544de83bd Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 23 Nov 2017 13:30:36 +0100
Subject: Change default for notations with variables bound to both terms and
 binders.

For compatibility, the default is to parse as ident and not as pattern.
---
 parsing/g_vernac.ml4 | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'parsing')

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index cca1b29898..d90fd3eb70 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -1174,7 +1174,8 @@ GEXTEND Gram
       | x = IDENT; ","; l = LIST1 [id = IDENT -> id ] SEP ","; "at";
         lev = level -> SetItemLevel (x::l,lev)
       | x = IDENT; "at"; lev = level -> SetItemLevel ([x],lev)
-      | x = IDENT; "at"; lev = level; b = constr_as_binder_kind -> SetItemLevelAsBinder ([x],b,lev)
+      | x = IDENT; "at"; lev = level; b = constr_as_binder_kind -> SetItemLevelAsBinder ([x],b,Some lev)
+      | x = IDENT; b = constr_as_binder_kind -> SetItemLevelAsBinder ([x],b,None)
       | x = IDENT; typ = syntax_extension_type -> SetEntryType (x,typ)
     ] ]
   ;
-- 
cgit v1.2.3


From 0af54860172efe1aa5da419b81e4cb34348320ee Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 23 Nov 2017 13:42:41 +0100
Subject: Trying a hack to support {'pat|P} without breaking compatibility.

Concretely, we bypass the following limitation: The notation
"{ ' pat | P }" broke the parsing of expressions of the form
"{ forall x, P } + { Q }". Indeed the latter works thanks to a
tolerance of Camlp5 in parsing "forall x, P" at level 200 while the
rule asks to actually parse the interior of "{ ... }" at level 99 (the
reason for 99 is to be below the rule for "M : T" which is at level
100, so that "{ x : A | P }" does not see "x : A" as a cast). Adding
an extra "'"; pat = pattern in parallel to c = constr LEVEL "99" broke
the tolerance for constr at level 200.

We fix this by adding an ad hoc rule for "{ binder_constr }" in the
native grammar (g_constr.ml4).

Actually, this is inconsistent with having a rule for "{ constr at level 99 }"
in Notations.v. We should have both rules in Notations.v or both rules
hard-wired in the native grammar. But I still don't know what is the best
decision to take, so leaving as it at the current time.

Advantages of hard-wiring both rules in g_constr.ml4: a bit simpler in
metasyntax.ml (no need to ensure that the rule exist). Disadvantages:
if one wants a different initial state without the business needing
the "{ }" for sumbool, sumor, sig, sigT, one still have the rules
there.

Advantages of having them in Notations.v: more modular, we can change
the initial state. Disadvantages: one would need a new kind of
modifier, something like "x at level 99 || binder_constr", with all
the difficulty to find a nice, intuitive, name for "binder_constr",
and the difficulty of understanding if there is a generality to this
"||" disjunction operator, and whether it should be documented or not.
---
 parsing/g_constr.ml4 | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'parsing')

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index c2ce003f13..9f12db649b 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -219,6 +219,8 @@ GEXTEND Gram
                 CAst.make ~loc:(!@loc) @@ CNotation("( _ )",([c],[],[],[]))
             | _ -> c)
       | "{|"; c = record_declaration; "|}" -> c
+      | "{"; c = binder_constr ; "}" ->
+          CAst.make ~loc:(!@loc) @@ CNotation(("{ _ }"),([c],[],[],[]))
       | "`{"; c = operconstr LEVEL "200"; "}" ->
 	  CAst.make ~loc:(!@loc) @@ CGeneralization (Implicit, None, c)
       | "`("; c = operconstr LEVEL "200"; ")" ->
-- 
cgit v1.2.3