Simplifying the EXTEND macros and making them more self-contained.

7 files changed, 106 insertions, 101 deletions

diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index bebde706e4..f9f3ee988e 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -8,19 +8,12 @@
 
 (*i camlp4deps: "tools/compat5b.cmo" i*)
 
-open Genarg
 open Q_util
 open Compat
-open Extend
 
 let loc = CompatLoc.ghost
 let default_loc = <:expr< Loc.ghost >>
 
-let qualified_name loc s =
-  let path = CString.split '.' s in
-  let (name, path) = CList.sep_last path in
-  qualified_name loc path name
-
 let mk_extraarg loc s = <:expr< $lid:"wit_"^s$ >>
 
 let rec make_wit loc = function
@@ -30,6 +23,10 @@ let rec make_wit loc = function
       <:expr< Genarg.wit_pair $make_wit loc t1$ $make_wit loc t2$ >>
   | ExtraArgType s -> mk_extraarg loc s
 
+let is_self s = function
+| ExtraArgType s' -> s = s'
+| _ -> false
+
 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$ >>
@@ -37,14 +34,14 @@ let make_topwit loc arg = <:expr< Genarg.topwit $make_wit loc arg$ >>
 let make_act loc act pil =
   let rec make = function
     | [] -> <:expr< (fun loc -> $act$) >>
-    | ExtNonTerminal (_, _, 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)
 
 let make_prod_item = function
   | ExtTerminal s -> <:expr< Extend.Atoken (Lexer.terminal $mlexpr_of_string s$) >>
-  | ExtNonTerminal (_, g, _) ->
+  | ExtNonTerminal (g, _) ->
     let base s = <:expr< Pcoq.name_of_entry $lid:s$ >> in
     mlexpr_of_prod_entry_key base g
 
@@ -56,11 +53,11 @@ let make_rule loc (prods,act) =
   <:expr< Extend.Rule $make_prod (List.rev prods)$ $make_act loc act prods$ >>
 
 let is_ident x = function
-| <:expr< $lid:s$ >> -> CString.equal s x
+| <:expr< $lid:s$ >> -> (s : string) = x
 | _ -> false
 
 let make_extend loc s cl wit = match cl with
-| [[ExtNonTerminal (_, Uentry e, id)], act] when is_ident id act ->
+| [[ExtNonTerminal (Uentry e, id)], act] when is_ident id act ->
   (** Special handling of identity arguments by not redeclaring an entry *)
   <:str_item<
     value $lid:s$ =
@@ -84,30 +81,26 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
   in
   let glob = match g with
     | None ->
-      begin match rawtyp with
-      | Genarg.ExtraArgType s' when CString.equal s s' ->
+      if is_self s rawtyp then
         <:expr< fun ist v -> (ist, v) >>
-      | _ ->
+      else
         <:expr< fun ist v ->
           let ans = out_gen $make_globwit loc rawtyp$
           (Tacintern.intern_genarg ist
           (Genarg.in_gen $make_rawwit loc rawtyp$ v)) in
           (ist, ans) >>
-      end
     | Some f ->
       <:expr< fun ist v -> (ist, $lid:f$ ist v) >>
   in
   let interp = match f with
     | None ->
-      begin match globtyp with
-      | Genarg.ExtraArgType s' when CString.equal s s' ->
+      if is_self s globtyp then
         <:expr< fun ist v -> Ftactic.return v >>
-      | _ ->
+      else
 	<:expr< fun ist x ->
           Ftactic.bind
 	    (Tacinterp.interp_genarg ist (Genarg.in_gen $make_globwit loc globtyp$ x))
             (fun v -> Ftactic.return (Tacinterp.Value.cast $make_topwit loc globtyp$ v)) >>
-      end
     | Some f ->
       (** Compatibility layer, TODO: remove me *)
       <:expr<
@@ -119,23 +112,17 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
       >> in
   let subst = match h with
     | None ->
-      begin match globtyp with
-      | Genarg.ExtraArgType s' when CString.equal s s' ->
+      if is_self s globtyp then
         <:expr< fun s v -> v >>
-      | _ ->
+      else
         <:expr< fun s x ->
           out_gen $make_globwit loc globtyp$
           (Tacsubst.subst_genarg s
             (Genarg.in_gen $make_globwit loc globtyp$ x)) >>
-      end
     | Some f -> <:expr< $lid:f$>> in
   let dyn = match typ with
   | `Uniform typ ->
-    let is_new = match typ with
-    | Genarg.ExtraArgType s' when CString.equal s s' -> true
-    | _ -> false
-    in
-    if is_new then <:expr< None >>
+    if is_self s typ then <:expr< None >>
     else <:expr< Some (Genarg.val_tag $make_topwit loc typ$) >>
   | `Specialized _ -> <:expr< None >>
   in
@@ -228,10 +215,10 @@ EXTEND
   genarg:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
         let e = parse_user_entry e "" in
-        ExtNonTerminal (type_of_user_symbol e, e, s)
+        ExtNonTerminal (e, s)
       | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
         let e = parse_user_entry e sep in
-        ExtNonTerminal (type_of_user_symbol e, e, s)
+        ExtNonTerminal (e, s)
       | s = STRING -> ExtTerminal s
     ] ]
   ;
diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib
index 42fc738783..9b24c97974 100644
--- a/grammar/grammar.mllib
+++ b/grammar/grammar.mllib
@@ -1,15 +1,8 @@
 Coq_config
 
-Hashset
-Hashcons
-CMap
-Int
-Option
 Store
 Exninfo
 Loc
-CList
-CString
 
 Tok
 Compat
diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4
index d91bfd7b8d..6821887327 100644
--- a/grammar/q_util.ml4
+++ b/grammar/q_util.ml4
@@ -8,12 +8,27 @@
 
 (* This file defines standard combinators to build ml expressions *)
 
-open Extend
 open Compat
 
+type argument_type =
+| ListArgType of argument_type
+| OptArgType of argument_type
+| PairArgType of argument_type * argument_type
+| ExtraArgType of string
+
+type user_symbol =
+| Ulist1 : user_symbol -> user_symbol
+| Ulist1sep : user_symbol * string -> user_symbol
+| Ulist0 : user_symbol -> user_symbol
+| Ulist0sep : user_symbol * string -> user_symbol
+| Uopt : user_symbol -> user_symbol
+| Umodifiers : user_symbol -> user_symbol
+| Uentry : string -> user_symbol
+| Uentryl : string * int -> user_symbol
+
 type extend_token =
 | ExtTerminal of string
-| ExtNonTerminal of Genarg.argument_type * Extend.user_symbol * string
+| ExtNonTerminal of user_symbol * string
 
 let mlexpr_of_list f l =
   List.fold_right
@@ -48,25 +63,25 @@ let mlexpr_of_ident id =
   <:expr< Names.Id.of_string $str:id$ >>
 
 let rec mlexpr_of_prod_entry_key f = function
-  | Extend.Ulist1 s -> <:expr< Extend.Alist1 $mlexpr_of_prod_entry_key f s$ >>
-  | Extend.Ulist1sep (s,sep) -> <:expr< Extend.Alist1sep $mlexpr_of_prod_entry_key f s$ $str:sep$ >>
-  | Extend.Ulist0 s -> <:expr< Extend.Alist0 $mlexpr_of_prod_entry_key f s$ >>
-  | Extend.Ulist0sep (s,sep) -> <:expr< Extend.Alist0sep $mlexpr_of_prod_entry_key f s$ $str:sep$ >>
-  | Extend.Uopt s -> <:expr< Extend.Aopt $mlexpr_of_prod_entry_key f s$ >>
-  | Extend.Umodifiers s -> <:expr< Extend.Amodifiers $mlexpr_of_prod_entry_key f s$ >>
-  | Extend.Uentry e -> <:expr< Extend.Aentry $f e$ >>
-  | Extend.Uentryl (e, l) ->
+  | Ulist1 s -> <:expr< Extend.Alist1 $mlexpr_of_prod_entry_key f s$ >>
+  | Ulist1sep (s,sep) -> <:expr< Extend.Alist1sep $mlexpr_of_prod_entry_key f s$ $str:sep$ >>
+  | Ulist0 s -> <:expr< Extend.Alist0 $mlexpr_of_prod_entry_key f s$ >>
+  | Ulist0sep (s,sep) -> <:expr< Extend.Alist0sep $mlexpr_of_prod_entry_key f s$ $str:sep$ >>
+  | Uopt s -> <:expr< Extend.Aopt $mlexpr_of_prod_entry_key f s$ >>
+  | Umodifiers s -> <:expr< Extend.Amodifiers $mlexpr_of_prod_entry_key f s$ >>
+  | Uentry e -> <:expr< Extend.Aentry $f e$ >>
+  | Uentryl (e, l) ->
     (** Keep in sync with Pcoq! *)
-    assert (CString.equal e "tactic");
+    assert (e = "tactic");
     if l = 5 then <:expr< Extend.Aentry (Pcoq.name_of_entry Pcoq.Tactic.binder_tactic) >>
     else <:expr< Extend.Aentryl (Pcoq.name_of_entry Pcoq.Tactic.tactic_expr) $mlexpr_of_int l$ >>
 
 let rec type_of_user_symbol = function
 | Ulist1 s | Ulist1sep (s, _) | Ulist0 s | Ulist0sep (s, _) | Umodifiers s ->
-  Genarg.ListArgType (type_of_user_symbol s)
+  ListArgType (type_of_user_symbol s)
 | Uopt s ->
-  Genarg.OptArgType (type_of_user_symbol s)
-| Uentry e | Uentryl (e, _) -> Genarg.ExtraArgType e
+  OptArgType (type_of_user_symbol s)
+| Uentry e | Uentryl (e, _) -> ExtraArgType e
 
 let coincide s pat off =
   let len = String.length pat in
diff --git a/grammar/q_util.mli b/grammar/q_util.mli
index 5f292baf32..7d4cc0200a 100644
--- a/grammar/q_util.mli
+++ b/grammar/q_util.mli
@@ -8,9 +8,25 @@
 
 open Compat (* necessary for camlp4 *)
 
+type argument_type =
+| ListArgType of argument_type
+| OptArgType of argument_type
+| PairArgType of argument_type * argument_type
+| ExtraArgType of string
+
+type user_symbol =
+| Ulist1 : user_symbol -> user_symbol
+| Ulist1sep : user_symbol * string -> user_symbol
+| Ulist0 : user_symbol -> user_symbol
+| Ulist0sep : user_symbol * string -> user_symbol
+| Uopt : user_symbol -> user_symbol
+| Umodifiers : user_symbol -> user_symbol
+| Uentry : string -> user_symbol
+| Uentryl : string * int -> user_symbol
+
 type extend_token =
 | ExtTerminal of string
-| ExtNonTerminal of Genarg.argument_type * Extend.user_symbol * string
+| ExtNonTerminal of user_symbol * string
 
 val mlexpr_of_list :  ('a -> MLast.expr) -> 'a list -> MLast.expr
 
@@ -28,8 +44,8 @@ val mlexpr_of_option : ('a -> MLast.expr) -> 'a option -> MLast.expr
 
 val mlexpr_of_ident : string -> MLast.expr
 
-val mlexpr_of_prod_entry_key : (string -> MLast.expr) -> Extend.user_symbol -> MLast.expr
+val mlexpr_of_prod_entry_key : (string -> MLast.expr) -> user_symbol -> MLast.expr
 
-val type_of_user_symbol : Extend.user_symbol -> Genarg.argument_type
+val type_of_user_symbol : user_symbol -> argument_type
 
-val parse_user_entry : string -> string -> Extend.user_symbol
+val parse_user_entry : string -> string -> user_symbol
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index 1951b8b452..bbd3d8a62f 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -20,22 +20,14 @@ let plugin_name = <:expr< __coq_plugin_name >>
 
 let rec make_patt = function
   | [] -> <:patt< [] >>
-  | ExtNonTerminal (_, _, p) :: l ->
+  | ExtNonTerminal (_, p) :: l ->
       <:patt< [ $lid:p$ :: $make_patt l$ ] >>
   | _::l -> make_patt l
 
-let rec mlexpr_of_argtype loc = function
-  | Genarg.ListArgType t -> <:expr< Genarg.ListArgType $mlexpr_of_argtype loc t$ >>
-  | Genarg.OptArgType t -> <:expr< Genarg.OptArgType $mlexpr_of_argtype loc t$ >>
-  | Genarg.PairArgType (t1,t2) ->
-      let t1 = mlexpr_of_argtype loc t1 in
-      let t2 = mlexpr_of_argtype loc t2 in
-      <:expr< Genarg.PairArgType $t1$ $t2$ >>
-  | Genarg.ExtraArgType s -> <:expr< Genarg.ExtraArgType $str:s$ >>
-
 let rec make_let raw e = function
   | [] -> <:expr< fun $lid:"ist"$ -> $e$ >>
-  | ExtNonTerminal (t, _, p) :: l ->
+  | ExtNonTerminal (g, p) :: l ->
+      let t = type_of_user_symbol g in
       let loc = MLast.loc_of_expr e in
       let e = make_let raw e l in
       let v =
@@ -44,12 +36,6 @@ let rec make_let raw e = function
       <:expr< let $lid:p$ = $v$ in $e$ >>
   | _::l -> make_let raw e l
 
-let rec extract_signature = function
-  | [] -> []
-  | ExtNonTerminal (t, _, _) :: l -> t :: extract_signature l
-  | _::l -> extract_signature l
-
-
 let make_clause (pt,_,e) =
   (make_patt pt,
    vala None,
@@ -61,7 +47,8 @@ let make_fun_clauses loc s l =
 
 let make_prod_item = function
   | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >>
-  | ExtNonTerminal (nt, g, id) ->
+  | ExtNonTerminal (g, id) ->
+    let nt = type_of_user_symbol g in
     let base s = <:expr< Pcoq.name_of_entry (Pcoq.genarg_grammar $mk_extraarg loc s$) >> in
       <:expr< Egramml.GramNonTerminal $default_loc$ $make_rawwit loc nt$
       $mlexpr_of_prod_entry_key base g$ >>
@@ -81,11 +68,11 @@ let make_printing_rule r = mlexpr_of_list make_one_printing_rule r
 (** Special treatment of constr entries *)
 let is_constr_gram = function
 | ExtTerminal _ -> false
-| ExtNonTerminal (_, Extend.Uentry "constr", _) -> true
+| ExtNonTerminal (Uentry "constr", _) -> true
 | _ -> false
 
 let make_var = function
-  | ExtNonTerminal (_, _, p) -> Some p
+  | ExtNonTerminal (_, p) -> Some p
   | _ -> assert false
 
 let declare_tactic loc s c cl = match cl with
@@ -99,13 +86,13 @@ let declare_tactic loc s c cl = match cl with
   let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in
   let ml = <:expr< { Tacexpr.mltac_name = $se$; Tacexpr.mltac_index = 0 } >> in
   let name = mlexpr_of_string name in
-  let tac =
+  let tac = match rem 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 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
       <:expr< Tacinterp.lift_constr_tac_to_ml_tac $vars$ $f$ >>
   in
@@ -173,12 +160,12 @@ EXTEND
   tacargs:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
         let e = parse_user_entry e "" in
-        ExtNonTerminal (type_of_user_symbol e, e, s)
+        ExtNonTerminal (e, s)
       | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
         let e = parse_user_entry e sep in
-        ExtNonTerminal (type_of_user_symbol e, e, s)
+        ExtNonTerminal (e, s)
       | s = STRING ->
-	let () = if CString.is_empty s then failwith "Empty terminal." in
+	let () = if s = "" then failwith "Empty terminal." in
         ExtTerminal s
     ] ]
   ;
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4
index 453907689e..aedaead71a 100644
--- a/grammar/vernacextend.ml4
+++ b/grammar/vernacextend.ml4
@@ -30,7 +30,8 @@ type rule = {
 
 let rec make_let e = function
   | [] -> e
-  | ExtNonTerminal (t, _, p) :: l ->
+  | ExtNonTerminal (g, p) :: l ->
+      let t = type_of_user_symbol g in
       let loc = MLast.loc_of_expr e in
       let e = make_let e l in
       <:expr< let $lid:p$ = Genarg.out_gen $make_rawwit loc t$ $lid:p$ in $e$ >>
@@ -43,9 +44,11 @@ let make_clause { r_patt = pt; r_branch = e; } =
 
 (* To avoid warnings *)
 let mk_ignore c pt =
-  let names = CList.map_filter (function
-  | ExtNonTerminal (_, _, p) -> Some p
-  | _ -> None) pt in
+  let fold accu = function
+  | ExtNonTerminal (_, p) -> p :: accu
+  | _ -> accu
+  in
+  let names = List.fold_left fold [] pt in
   let fold accu id = <:expr< let _ = $lid:id$ in $accu$ >> in
   let names = List.fold_left fold <:expr< () >> names in
   <:expr< do { let _ = $names$ in $c$ } >>
@@ -99,10 +102,12 @@ let make_fun_classifiers loc s c l =
   let cl = List.map (fun x -> Compat.make_fun loc [make_clause_classifier c s x]) l in
   mlexpr_of_list (fun x -> x) cl
 
-let mlexpr_of_clause =
-  mlexpr_of_list
-    (fun { r_head = a; r_patt = b; } -> mlexpr_of_list make_prod_item
-       (Option.List.cons (Option.map (fun a -> ExtTerminal a) a) b))
+let mlexpr_of_clause cl =
+  let mkexpr { r_head = a; r_patt = b; } = match a with
+  | None -> mlexpr_of_list make_prod_item b
+  | Some a -> mlexpr_of_list make_prod_item (ExtTerminal a :: b)
+  in
+  mlexpr_of_list mkexpr cl
 
 let declare_command loc s c nt cl =
   let se = mlexpr_of_string s in
@@ -160,7 +165,7 @@ EXTEND
   rule:
     [ [ "["; s = STRING; l = LIST0 args; "]";
         d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
-      let () = if CString.is_empty s then failwith "Command name is empty." in
+      let () = if 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 ; "]" ;
@@ -175,10 +180,10 @@ EXTEND
   args:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
         let e = parse_user_entry e "" in
-        ExtNonTerminal (type_of_user_symbol e, e, s)
+        ExtNonTerminal (e, s)
       | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
         let e = parse_user_entry e sep in
-        ExtNonTerminal (type_of_user_symbol e, e, s)
+        ExtNonTerminal (e, s)
       | s = STRING ->
         ExtTerminal s
     ] ]
diff --git a/parsing/tok.ml b/parsing/tok.ml
index 6b90086155..df7e7c2a6b 100644
--- a/parsing/tok.ml
+++ b/parsing/tok.ml
@@ -8,6 +8,8 @@
 
 (** The type of token for the Coq lexer and parser *)
 
+let string_equal (s1 : string) s2 = s1 = s2
+
 type t =
   | KEYWORD of string
   | PATTERNIDENT of string
@@ -21,16 +23,16 @@ type t =
   | EOI
 
 let equal t1 t2 = match t1, t2 with
-| IDENT s1, KEYWORD s2 -> CString.equal s1 s2
-| KEYWORD s1, KEYWORD s2 -> CString.equal s1 s2
-| PATTERNIDENT s1, PATTERNIDENT s2 -> CString.equal s1 s2
-| IDENT s1, IDENT s2 -> CString.equal s1 s2
-| FIELD s1, FIELD s2 -> CString.equal s1 s2
-| INT s1, INT s2 -> CString.equal s1 s2
-| INDEX s1, INDEX s2 -> CString.equal s1 s2
-| STRING s1, STRING s2 -> CString.equal s1 s2
+| IDENT s1, KEYWORD s2 -> string_equal s1 s2
+| KEYWORD s1, KEYWORD s2 -> string_equal s1 s2
+| PATTERNIDENT s1, PATTERNIDENT s2 -> string_equal s1 s2
+| IDENT s1, IDENT s2 -> string_equal s1 s2
+| FIELD s1, FIELD s2 -> string_equal s1 s2
+| INT s1, INT s2 -> string_equal s1 s2
+| INDEX s1, INDEX s2 -> string_equal s1 s2
+| STRING s1, STRING s2 -> string_equal s1 s2
 | LEFTQMARK, LEFTQMARK -> true
-| BULLET s1, BULLET s2 -> CString.equal s1 s2
+| BULLET s1, BULLET s2 -> string_equal s1 s2
 | EOI, EOI -> true
 | _ -> false