Making the EXTEND macros almost self-contained.

7 files changed, 65 insertions, 87 deletions

diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index f26a66a12b..5bf7b65d77 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -10,10 +10,8 @@
 
 open Genarg
 open Q_util
-open Egramml
 open Compat
 open Extend
-open Pcoq
 
 let loc = CompatLoc.ghost
 let default_loc = <:expr< Loc.ghost >>
@@ -36,17 +34,10 @@ let make_rawwit loc arg = <:expr< Genarg.rawwit $make_wit loc arg$ >>
 let make_globwit loc arg = <:expr< Genarg.glbwit $make_wit loc arg$ >>
 let make_topwit loc arg = <:expr< Genarg.topwit $make_wit loc arg$ >>
 
-let has_extraarg l =
-  let check = function
-  | ExtNonTerminal(ExtraArgType _, _, _) -> true
-  | _ -> false
-  in
-  List.exists check l
-
 let make_act loc act pil =
   let rec make = function
     | [] -> <:expr< (fun loc -> $act$) >>
-    | ExtNonTerminal (t, _, p) :: tl -> <:expr< (fun $lid:p$ -> $make tl$) >>
+    | ExtNonTerminal (_, _, p) :: tl -> <:expr< (fun $lid:p$ -> $make tl$) >>
     | ExtTerminal _ :: tl ->
 	<:expr< (fun _ -> $make tl$) >> in
   make (List.rev pil)
@@ -241,10 +232,7 @@ EXTEND
       | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
         let e = parse_user_entry e sep in
         ExtNonTerminal (type_of_user_symbol e, e, s)
-      | s = STRING ->
-	  if String.length s > 0 && Util.is_letter s.[0] then
-	    Lexer.add_keyword s;
-          ExtTerminal s
+      | s = STRING -> ExtTerminal s
     ] ]
   ;
   entry_name:
diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib
index 6a265bf4a8..ae18925ead 100644
--- a/grammar/grammar.mllib
+++ b/grammar/grammar.mllib
@@ -1,46 +1,22 @@
 Coq_config
 
-Hook
-Terminal
 Hashset
 Hashcons
-CSet
 CMap
 Int
-Dyn
-HMap
 Option
 Store
 Exninfo
-Backtrace
-Pp_control
-Flags
 Loc
 CList
 CString
-Serialize
-Stateid
-Feedback
-Pp
 
-CArray
-CStack
-Util
-Ppstyle
-Errors
 Segmenttree
 Unicodetable
 Unicode
-Genarg
-
-Stdarg
-Constrarg
 
 Tok
 Compat
-Lexer
-Entry
-Pcoq
 
 Q_util
 Argextend
diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4
index c43ce15be2..4160d03c5c 100644
--- a/grammar/q_util.ml4
+++ b/grammar/q_util.ml4
@@ -67,3 +67,43 @@ let rec type_of_user_symbol = function
 | Uopt s ->
   Genarg.OptArgType (type_of_user_symbol s)
 | Uentry e | Uentryl (e, _) -> Genarg.ExtraArgType e
+
+let coincide s pat off =
+  let len = String.length pat in
+  let break = ref true in
+  let i = ref 0 in
+  while !break && !i < len do
+    let c = Char.code s.[off + !i] in
+    let d = Char.code pat.[!i] in
+    break := Int.equal c d;
+    incr i
+  done;
+  !break
+
+let rec parse_user_entry s sep =
+  let l = String.length s in
+  if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then
+    let entry = parse_user_entry (String.sub s 3 (l-8)) "" in
+    Ulist1 entry
+  else if l > 12 && coincide s "ne_" 0 &&
+                   coincide s "_list_sep" (l-9) then
+    let entry = parse_user_entry (String.sub s 3 (l-12)) "" in
+    Ulist1sep (entry, sep)
+  else if l > 5 && coincide s "_list" (l-5) then
+    let entry = parse_user_entry (String.sub s 0 (l-5)) "" in
+    Ulist0 entry
+  else if l > 9 && coincide s "_list_sep" (l-9) then
+    let entry = parse_user_entry (String.sub s 0 (l-9)) "" in
+    Ulist0sep (entry, sep)
+  else if l > 4 && coincide s "_opt" (l-4) then
+    let entry = parse_user_entry (String.sub s 0 (l-4)) "" in
+    Uopt entry
+  else if l > 5 && coincide s "_mods" (l-5) then
+    let entry = parse_user_entry (String.sub s 0 (l-1)) "" in
+    Umodifiers entry
+  else if Int.equal l 7 && coincide s "tactic" 0 && '5' >= s.[6] && s.[6] >= '0' then
+    let n = Char.code s.[6] - 48 in
+    Uentryl ("tactic", n)
+  else
+    let s = match s with "hyp" -> "var" | _ -> s in
+    Uentry s
diff --git a/grammar/q_util.mli b/grammar/q_util.mli
index 712aa8509d..5f292baf32 100644
--- a/grammar/q_util.mli
+++ b/grammar/q_util.mli
@@ -31,3 +31,5 @@ val mlexpr_of_ident : string -> MLast.expr
 val mlexpr_of_prod_entry_key : (string -> MLast.expr) -> Extend.user_symbol -> MLast.expr
 
 val type_of_user_symbol : Extend.user_symbol -> Genarg.argument_type
+
+val parse_user_entry : string -> string -> Extend.user_symbol
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index a18dfa5096..1951b8b452 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -10,14 +10,8 @@
 
 (** Implementation of the TACTIC EXTEND macro. *)
 
-open Util
-open Pp
-open Names
-open Genarg
 open Q_util
 open Argextend
-open Pcoq
-open Egramml
 open Compat
 
 let dloc = <:expr< Loc.ghost >>
@@ -39,14 +33,6 @@ let rec mlexpr_of_argtype loc = function
       <:expr< Genarg.PairArgType $t1$ $t2$ >>
   | Genarg.ExtraArgType s -> <:expr< Genarg.ExtraArgType $str:s$ >>
 
-let rec make_when loc = function
-  | [] -> <:expr< True >>
-  | ExtNonTerminal (t, _, p) :: l ->
-      let l = make_when loc l in
-      let t = mlexpr_of_argtype loc t in
-      <:expr< Genarg.argument_type_eq (Genarg.genarg_tag $lid:p$) $t$ && $l$ >>
-  | _::l -> make_when loc l
-
 let rec make_let raw e = function
   | [] -> <:expr< fun $lid:"ist"$ -> $e$ >>
   | ExtNonTerminal (t, _, p) :: l ->
@@ -64,21 +50,12 @@ let rec extract_signature = function
   | _::l -> extract_signature l
 
 
-
-let check_unicity s l =
-  let l' = List.map (fun (l,_,_) -> extract_signature l) l in
-  if not (Util.List.distinct l') then
-    Pp.msg_warning
-      (strbrk ("Two distinct rules of tactic entry "^s^" have the same "^
-      "non-terminals in the same order: put them in distinct tactic entries"))
-
 let make_clause (pt,_,e) =
   (make_patt pt,
    vala None,
    make_let false e pt)
 
 let make_fun_clauses loc s l =
-  check_unicity s l;
   let map c = Compat.make_fun loc [make_clause c] in
   mlexpr_of_list map l
 
@@ -126,7 +103,7 @@ let declare_tactic loc s c cl = match cl with
     (** Special handling of tactics without arguments: such tactics do not do
         a Proofview.Goal.nf_enter to compute their arguments. It matters for some
         whole-prof tactics like [shelve_unifiable]. *)
-    if List.is_empty rem then
+    if CList.is_empty rem then
       <:expr< fun _ $lid:"ist"$ -> $tac$ >>
     else
       let f = Compat.make_fun loc [patt, vala None, <:expr< fun $lid:"ist"$ -> $tac$ >>] in
@@ -201,7 +178,7 @@ EXTEND
         let e = parse_user_entry e sep in
         ExtNonTerminal (type_of_user_symbol e, e, s)
       | s = STRING ->
-	if String.is_empty s then Errors.user_err_loc (!@loc,"",Pp.str "Empty terminal.");
+	let () = if CString.is_empty s then failwith "Empty terminal." in
         ExtTerminal s
     ] ]
   ;
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4
index d8c8850884..453907689e 100644
--- a/grammar/vernacextend.ml4
+++ b/grammar/vernacextend.ml4
@@ -10,13 +10,9 @@
 
 (** Implementation of the VERNAC EXTEND macro. *)
 
-open Pp
-open Util
 open Q_util
 open Argextend
 open Tacextend
-open Pcoq
-open Egramml
 open Compat
 
 type rule = {
@@ -64,26 +60,26 @@ let make_clause_classifier cg s { r_patt = pt; r_class = c; } =
      (make_patt pt,
       vala None,
       <:expr< fun () -> $cg$ $str:s$ >>)
-  | None, None -> msg_warning
-      (strbrk("Vernac entry \""^s^"\" misses a classifier. "^
+  | None, None -> prerr_endline
+      (("Vernac entry \""^s^"\" misses a classifier. "^
          "A classifier is a function that returns an expression "^
-         "of type vernac_classification (see Vernacexpr). You can: ")++
-       str"- "++hov 0 (
-        strbrk("Use '... EXTEND "^s^" CLASSIFIED AS QUERY ...' if the "^
-          "new vernacular command does not alter the system state;"))++fnl()++
-       str"- "++hov 0 (
-        strbrk("Use '... EXTEND "^s^" CLASSIFIED AS SIDEFF ...' if the "^
+         "of type vernac_classification (see Vernacexpr). You can: ") ^
+       "- " ^ (
+        ("Use '... EXTEND "^s^" CLASSIFIED AS QUERY ...' if the "^
+          "new vernacular command does not alter the system state;"))^ "\n" ^
+       "- " ^ (
+        ("Use '... EXTEND "^s^" CLASSIFIED AS SIDEFF ...' if the "^
           "new vernacular command alters the system state but not the "^
-          "parser nor it starts a proof or ends one;"))++fnl()++
-       str"- "++hov 0 (
-        strbrk("Use '... EXTEND "^s^" CLASSIFIED BY f ...' to specify "^
+          "parser nor it starts a proof or ends one;"))^ "\n" ^
+       "- " ^ (
+        ("Use '... EXTEND "^s^" CLASSIFIED BY f ...' to specify "^
           "a global function f.  The function f will be called passing "^
-          "\""^s^"\" as the only argument;")) ++fnl()++
-       str"- "++hov 0 (
-        strbrk"Add a specific classifier in each clause using the syntax:"
-        ++fnl()++strbrk("'[...] => [ f ] -> [...]'. "))++fnl()++
-       strbrk("Specific classifiers have precedence over global "^
-         "classifiers. Only one classifier is called.")++fnl());
+          "\""^s^"\" as the only argument;")) ^ "\n" ^
+       "- " ^ (
+        "Add a specific classifier in each clause using the syntax:"
+        ^ "\n" ^("'[...] => [ f ] -> [...]'. "))^ "\n" ^
+       ("Specific classifiers have precedence over global "^
+         "classifiers. Only one classifier is called.") ^ "\n");
     (make_patt pt,
       vala None,
       <:expr< fun () -> (Vernacexpr.VtUnknown, Vernacexpr.VtNow) >>)
@@ -164,8 +160,7 @@ EXTEND
   rule:
     [ [ "["; s = STRING; l = LIST0 args; "]";
         d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
-      if String.is_empty s then
-        Errors.user_err_loc (!@loc,"",Pp.str"Command name is empty.");
+      let () = if CString.is_empty s then failwith "Command name is empty." in
       let b = <:expr< fun () -> $e$ >> in
       { r_head = Some s; r_patt = l; r_class = c; r_branch = b; r_depr = d; }
       | "[" ; "-" ; l = LIST1 args ; "]" ;
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 232e9aee3f..8b8b38c34b 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -724,7 +724,7 @@ let strip s =
 
 let terminal s =
   let s = strip s in
-  let () = match s with "" -> Errors.error "empty token." | _ -> () in
+  let () = match s with "" -> failwith "empty token." | _ -> () in
   if is_ident_not_keyword s then IDENT s
   else if is_number s then INT s
   else KEYWORD s