Split Egrammar into Egramml and Egramcoq

 Two gains:
 - no Summary in Grammar.cma
 - get rid of the hack concerning error_invalid_pattern_notation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15386 85f007b7-540e-0410-9357-904b9bb8a0f7

10 files changed, 127 insertions, 107 deletions

diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index b6fd95a81..5a64580d2 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -10,7 +10,7 @@
 
 open Genarg
 open Q_util
-open Egrammar
+open Egramml
 open Pcoq
 open Compat
 
diff --git a/parsing/egrammar.ml b/parsing/egramcoq.ml
index b0c705400..ee8ec009d 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egramcoq.ml
@@ -17,10 +17,10 @@ open Constrexpr
 open Notation_term
 open Genarg
 open Libnames
-open Nameops
 open Tacexpr
 open Names
 open Vernacexpr
+open Egramml
 
 (**************************************************************************)
 (*
@@ -61,7 +61,7 @@ type grammar_constr_prod_item =
   | GramConstrTerminal of Tok.t
   | GramConstrNonTerminal of constr_prod_entry_key * identifier option
   | GramConstrListMark of int * bool
-    (* tells action rule to make a list of the n previous parsed items; 
+    (* tells action rule to make a list of the n previous parsed items;
        concat with last parsed list if true *)
 
 let make_constr_action
@@ -108,12 +108,8 @@ let make_constr_action
   in
   make ([],[],[]) (List.rev pil)
 
-(* TODO: factorize the error message with error_invalid_pattern_notaition
-   without introducing useless dependencies *)
-
 let check_cases_pattern_env loc (env,envlist,hasbinders) =
-  if hasbinders then
-    Errors.user_err_loc (loc,"",str "Invalid notation for pattern.")
+  if hasbinders then Topconstr.error_invalid_pattern_notation loc
   else (env,envlist)
 
 let make_cases_pattern_action
@@ -209,60 +205,6 @@ let extend_constr_notation (n,assoc,ntn,rules) =
   nb+nb'
 
 (**********************************************************************)
-(** Making generic actions in type generic_argument                   *)
-
-let make_generic_action
-  (f:loc -> ('b * raw_generic_argument) list -> 'a) pil =
-  let rec make env = function
-    | [] ->
-	Gram.action (fun loc -> f loc env)
-    | None :: tl -> (* parse a non-binding item *)
-        Gram.action (fun _ -> make env tl)
-    | Some (p, t) :: tl -> (* non-terminal *)
-        Gram.action (fun v -> make ((p,in_generic t v) :: env) tl) in
-  make [] (List.rev pil)
-
-let make_rule univ f g pt =
-  let (symbs,ntl) = List.split (List.map g pt) in
-  let act = make_generic_action f ntl in
-  (symbs, act)
-
-(**********************************************************************)
-(** Grammar extensions declared at ML level                           *)
-
-type grammar_prod_item =
-  | GramTerminal of string
-  | GramNonTerminal of
-      loc * argument_type * prod_entry_key * identifier option
-
-let make_prod_item = function
-  | GramTerminal s -> (gram_token_of_string s, None)
-  | GramNonTerminal (_,t,e,po) ->
-      (symbol_of_prod_entry_key e, Option.map (fun p -> (p,t)) po)
-
-(* Tactic grammar extensions *)
-
-let extend_tactic_grammar s gl =
-  let univ = get_univ "tactic" in
-  let mkact loc l = Tacexpr.TacExtend (loc,s,List.map snd l) in
-  let rules = List.map (make_rule univ mkact make_prod_item) gl in
-  maybe_uncurry (Gram.extend Tactic.simple_tactic)
-    (None,[(None, None, List.rev rules)])
-
-(* Vernac grammar extensions *)
-
-let vernac_exts = ref []
-let get_extend_vernac_grammars () = !vernac_exts
-
-let extend_vernac_command_grammar s nt gl =
-  let nt = Option.default Vernac_.command nt in
-  vernac_exts := (s,gl) :: !vernac_exts;
-  let univ = get_univ "vernac" in
-  let mkact loc l = VernacExtend (s,List.map snd l) in
-  let rules = List.map (make_rule univ mkact make_prod_item) gl in
-  maybe_uncurry (Gram.extend nt) (None,[(None, None, List.rev rules)])
-
-(**********************************************************************)
 (** Grammar declaration for Tactic Notation (Coq level)               *)
 
 let get_tactic_entry n =
@@ -280,7 +222,6 @@ let get_tactic_entry n =
 let head_is_ident = function GramTerminal _::_ -> true | _ -> false
 
 let add_tactic_entry (key,lev,prods,tac) =
-  let univ = get_univ "tactic" in
   let entry, pos = get_tactic_entry lev in
   let rules =
     if lev = 0 then begin
@@ -288,12 +229,12 @@ let add_tactic_entry (key,lev,prods,tac) =
 	error "Notation for simple tactic must start with an identifier.";
       let mkact s tac loc l =
 	(TacAlias(loc,s,l,tac):raw_atomic_tactic_expr) in
-      make_rule univ (mkact key tac) make_prod_item prods
+      make_rule (mkact key tac) prods
     end
     else
       let mkact s tac loc l =
 	(TacAtom(loc,TacAlias(loc,s,l,tac)):raw_tactic_expr) in
-      make_rule univ (mkact key tac) make_prod_item prods in
+      make_rule (mkact key tac) prods in
   synchronize_level_positions ();
   grammar_extend entry None (pos,[(None, None, List.rev [rules])]);
   1
diff --git a/parsing/egrammar.mli b/parsing/egramcoq.mli
index 108f39eaa..263519591 100644
--- a/parsing/egrammar.mli
+++ b/parsing/egramcoq.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Compat
-open Errors
 open Pp
 open Names
 open Constrexpr
@@ -16,14 +15,13 @@ open Pcoq
 open Extend
 open Vernacexpr
 open Ppextend
-open Glob_term
 open Genarg
-open Mod_subst
+open Egramml
 
-(** Mapping of grammar productions to camlp4 actions
-    Used for Coq-level Notation and Tactic Notation,
-    and for ML-level tactic and vernac extensions
- *)
+(** Mapping of grammar productions to camlp4 actions *)
+
+(** This is the part specific to Coq-level Notation and Tactic Notation.
+    For the ML-level tactic and vernac extensions, see Egramml. *)
 
 (** For constr notations *)
 
@@ -31,19 +29,12 @@ type grammar_constr_prod_item =
   | GramConstrTerminal of Tok.t
   | GramConstrNonTerminal of constr_prod_entry_key * identifier option
   | GramConstrListMark of int * bool
-    (* tells action rule to make a list of the n previous parsed items; 
+    (* tells action rule to make a list of the n previous parsed items;
        concat with last parsed list if true *)
 
 type notation_grammar =
     int * gram_assoc option * notation * grammar_constr_prod_item list list
 
-(** For tactic and vernac notations *)
-
-type grammar_prod_item =
-  | GramTerminal of string
-  | GramNonTerminal of loc * argument_type *
-      prod_entry_key * identifier option
-
 (** Adding notations *)
 
 type all_grammar_command =
@@ -59,15 +50,6 @@ type all_grammar_command =
 
 val extend_grammar : all_grammar_command -> unit
 
-val extend_tactic_grammar :
-  string -> grammar_prod_item list list -> unit
-
-val extend_vernac_command_grammar :
-  string -> vernac_expr Gram.entry option -> grammar_prod_item list list -> unit
-
-val get_extend_vernac_grammars :
- unit -> (string * grammar_prod_item list list) list
-
 (** For a declared grammar, returns the rule + the ordered entry types
     of variables in the rule (for use in the interpretation) *)
 val recover_notation_grammar :
diff --git a/parsing/egramml.ml b/parsing/egramml.ml
new file mode 100644
index 000000000..62e7ae2bb
--- /dev/null
+++ b/parsing/egramml.ml
@@ -0,0 +1,67 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Compat
+open Names
+open Pcoq
+open Genarg
+open Tacexpr
+open Vernacexpr
+
+(** Making generic actions in type generic_argument *)
+
+let make_generic_action
+  (f:loc -> ('b * raw_generic_argument) list -> 'a) pil =
+  let rec make env = function
+    | [] ->
+	Gram.action (fun loc -> f loc env)
+    | None :: tl -> (* parse a non-binding item *)
+        Gram.action (fun _ -> make env tl)
+    | Some (p, t) :: tl -> (* non-terminal *)
+        Gram.action (fun v -> make ((p,in_generic t v) :: env) tl) in
+  make [] (List.rev pil)
+
+let make_rule_gen mkproditem mkact pt =
+  let (symbs,ntl) = List.split (List.map mkproditem pt) in
+  let act = make_generic_action mkact ntl in
+  (symbs, act)
+
+(** Grammar extensions declared at ML level *)
+
+type grammar_prod_item =
+  | GramTerminal of string
+  | GramNonTerminal of
+      loc * argument_type * prod_entry_key * identifier option
+
+let make_prod_item = function
+  | GramTerminal s -> (gram_token_of_string s, None)
+  | GramNonTerminal (_,t,e,po) ->
+      (symbol_of_prod_entry_key e, Option.map (fun p -> (p,t)) po)
+
+let make_rule mkact = make_rule_gen make_prod_item mkact
+
+(** Tactic grammar extensions *)
+
+let extend_tactic_grammar s gl =
+  let mkact loc l = Tacexpr.TacExtend (loc,s,List.map snd l) in
+  let rules = List.map (make_rule mkact) gl in
+  maybe_uncurry (Gram.extend Tactic.simple_tactic)
+    (None,[(None, None, List.rev rules)])
+
+(** Vernac grammar extensions *)
+
+let vernac_exts = ref []
+let get_extend_vernac_grammars () = !vernac_exts
+
+let extend_vernac_command_grammar s nt gl =
+  let nt = Option.default Vernac_.command nt in
+  vernac_exts := (s,gl) :: !vernac_exts;
+  let mkact loc l = VernacExtend (s,List.map snd l) in
+  let rules = List.map (make_rule mkact) gl in
+  maybe_uncurry (Gram.extend nt) (None,[(None, None, List.rev rules)])
diff --git a/parsing/egramml.mli b/parsing/egramml.mli
new file mode 100644
index 000000000..350e75f90
--- /dev/null
+++ b/parsing/egramml.mli
@@ -0,0 +1,33 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Mapping of grammar productions to camlp4 actions. *)
+
+(** This is the part specific to ML-level tactic and vernac extensions.
+    For the Coq-level Notation and Tactic Notation, see Egramcoq. *)
+
+type grammar_prod_item =
+  | GramTerminal of string
+  | GramNonTerminal of Pp.loc * Genarg.argument_type *
+      Pcoq.prod_entry_key * Names.identifier option
+
+val extend_tactic_grammar :
+  string -> grammar_prod_item list list -> unit
+
+val extend_vernac_command_grammar :
+  string -> Vernacexpr.vernac_expr Pcoq.Gram.entry option ->
+    grammar_prod_item list list -> unit
+
+val get_extend_vernac_grammars :
+  unit -> (string * grammar_prod_item list list) list
+
+(** Utility function reused in Egramcoq : *)
+
+val make_rule :
+  (Pp.loc -> (Names.identifier * Tacexpr.raw_generic_argument) list -> 'b) ->
+  grammar_prod_item list -> Pcoq.Gram.symbol list * Pcoq.Gram.action
diff --git a/parsing/grammar.mllib b/parsing/grammar.mllib
index c99ae47d0..313676c96 100644
--- a/parsing/grammar.mllib
+++ b/parsing/grammar.mllib
@@ -1,6 +1,5 @@
 Coq_config
 
-Profile
 Pp_control
 Compat
 Flags
@@ -10,16 +9,13 @@ Unicodetable
 Errors
 Util
 Bigint
-Dyn
 Hashcons
 Predicate
 Option
 
 Names
 Libnames
-Summary
 Genarg
-Ppextend
 Tok
 Lexer
 Extend
@@ -28,7 +24,7 @@ Pcoq
 Q_util
 Q_coqast
 
-Egrammar
+Egramml
 Argextend
 Tacextend
 Vernacextend
diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib
index 84a08d549..8414ec766 100644
--- a/parsing/parsing.mllib
+++ b/parsing/parsing.mllib
@@ -1,7 +1,8 @@
 Extend
 Extrawit
 Pcoq
-Egrammar
+Egramml
+Egramcoq
 G_xml
 Ppconstr
 Printer
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index ec164a7e3..1f8d7cb83 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -77,7 +77,7 @@ let pr_raw_tactic tac = pr_raw_tactic (Global.env()) tac
 
 let rec extract_signature = function
   | [] -> []
-  | Egrammar.GramNonTerminal (_,t,_,_) :: l -> t :: extract_signature l
+  | Egramml.GramNonTerminal (_,t,_,_) :: l -> t :: extract_signature l
   | _::l -> extract_signature l
 
 let rec match_vernac_rule tys = function
@@ -942,19 +942,19 @@ and pr_extend s cl =
     try pr_gen (Global.env()) a
     with Failure _ -> str ("<error in "^s^">") in
   try
-    let rls = List.assoc s (Egrammar.get_extend_vernac_grammars()) in
+    let rls = List.assoc s (Egramml.get_extend_vernac_grammars()) in
     let rl = match_vernac_rule (List.map Genarg.genarg_tag cl) rls in
     let start,rl,cl =
       match rl with
-      | Egrammar.GramTerminal s :: rl -> str s, rl, cl
-      | Egrammar.GramNonTerminal _ :: rl -> pr_arg (List.hd cl), rl, List.tl cl
+      | Egramml.GramTerminal s :: rl -> str s, rl, cl
+      | Egramml.GramNonTerminal _ :: rl -> pr_arg (List.hd cl), rl, List.tl cl
       | [] -> anomaly "Empty entry" in
     let (pp,_) =
       List.fold_left
         (fun (strm,args) pi ->
           let pp,args = match pi with
-          | Egrammar.GramNonTerminal _ -> (pr_arg (List.hd args), List.tl args)
-          | Egrammar.GramTerminal s -> (str s, args) in
+          | Egramml.GramNonTerminal _ -> (pr_arg (List.hd args), List.tl args)
+          | Egramml.GramTerminal s -> (str s, args) in
           (strm ++ spc() ++ pp), args)
         (start,cl) rl in
     hov 1 pp
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index c7a646ac4..ec0784c52 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -16,7 +16,7 @@ open Q_coqast
 open Argextend
 open Pcoq
 open Extrawit
-open Egrammar
+open Egramml
 open Compat
 
 let rec make_patt = function
@@ -95,9 +95,9 @@ let mlexpr_terminals_of_grammar_tactic_prod_item_expr = function
   | GramNonTerminal (loc,nt,_,sopt) -> <:expr< None >>
 
 let make_prod_item = function
-  | GramTerminal s -> <:expr< Egrammar.GramTerminal $str:s$ >>
+  | GramTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >>
   | GramNonTerminal (loc,nt,g,sopt) ->
-      <:expr< Egrammar.GramNonTerminal $default_loc$ $mlexpr_of_argtype loc nt$
+      <:expr< Egramml.GramNonTerminal $default_loc$ $mlexpr_of_argtype loc nt$
       $mlexpr_of_prod_entry_key g$ $mlexpr_of_option mlexpr_of_ident sopt$ >>
 
 let mlexpr_of_clause =
@@ -190,7 +190,7 @@ let declare_tactic loc s cl =
            | None -> () ])
           $atomic_tactics$
       with e -> Pp.pp (Errors.print e);
-      Egrammar.extend_tactic_grammar $se$ $gl$;
+      Egramml.extend_tactic_grammar $se$ $gl$;
       List.iter Pptactic.declare_extra_tactic_pprule $pp$; } >>
     ])
 
diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4
index 7553aef4a..94135d121 100644
--- a/parsing/vernacextend.ml4
+++ b/parsing/vernacextend.ml4
@@ -16,7 +16,7 @@ open Q_coqast
 open Argextend
 open Tacextend
 open Pcoq
-open Egrammar
+open Egramml
 open Compat
 
 let rec make_let e = function
@@ -56,7 +56,7 @@ let declare_command loc s nt cl =
     [ <:str_item< do {
 	try Vernacinterp.vinterp_add $mlexpr_of_string s$ $funcl$
 	with e -> Pp.pp (Errors.print e);
-	Egrammar.extend_vernac_command_grammar $mlexpr_of_string s$ $nt$ $gl$
+	Egramml.extend_vernac_command_grammar $mlexpr_of_string s$ $nt$ $gl$
       } >> ]
 
 open Pcaml