Merge PR #982: Miscellaneous extensions of notations (including granting BZ5585)

5 files changed, 70 insertions, 48 deletions

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index ea6266dd44..a3d2571549 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -229,11 +229,11 @@ 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
-| TTBinderListT : ('self, local_binder_expr list) entry
-| TTBinderListF : Tok.t list -> ('self, local_binder_expr list 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
 
 type _ any_entry = TTAny : ('s, 'r) entry -> 's any_entry
 
@@ -289,31 +289,24 @@ 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)
+| 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
-| TTBinder -> Aentry Constr.binder
-| TTBinderListT -> Aentry Constr.open_binders
+| 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 (true, []) -> TTAny TTBinderListT
-| ETBinderList (true, _) -> assert false
-| ETBinderList (false, tkl) -> TTAny (TTBinderListF 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)
+| ETProdName -> TTAny TTName
+| ETProdReference -> TTAny TTReference
+| ETProdBigint -> TTAny TTBigint
+| ETProdConstr p -> TTAny (TTConstr (p, forpat))
+| 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 cases_pattern_expr_of_name (loc,na) = CAst.make ?loc @@ match na with
   | Anonymous -> CPatAtom None
@@ -322,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;
-  binders : (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 }
@@ -332,12 +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
-| 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 }
+| 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)))
@@ -437,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.binders) 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.binders 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, [])
 
@@ -457,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 = []; binders = [] } 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 db68a75e09..9f12db649b 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,9 +216,11 @@ 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 = binder_constr ; "}" ->
+          CAst.make ~loc:(!@loc) @@ CNotation(("{ _ }"),([c],[],[],[]))
       | "`{"; c = operconstr LEVEL "200"; "}" ->
 	  CAst.make ~loc:(!@loc) @@ CGeneralization (Implicit, None, c)
       | "`("; c = operconstr LEVEL "200"; ")" ->
@@ -385,19 +387,9 @@ GEXTEND Gram
     | "99" RIGHTA [ ]
     | "90" RIGHTA [ ]
     | "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; "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, []) ]
     | "1" LEFTA
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index d42b5f622c..d90fd3eb70 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -1174,6 +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,Some lev)
+      | x = IDENT; b = constr_as_binder_kind -> SetItemLevelAsBinder ([x],b,None)
       | x = IDENT; typ = syntax_extension_type -> SetEntryType (x,typ)
     ] ]
   ;
@@ -1181,7 +1183,20 @@ GEXTEND Gram
     [ [ IDENT "ident" -> ETName | IDENT "global" -> ETReference
       | IDENT "bigint" -> ETBigint
       | IDENT "binder" -> ETBinder true
+      | 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
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