EXTEND macros use their own internal representations.

4 files changed, 60 insertions, 37 deletions

diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index a38f57cdc..f9f3ee988 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -8,10 +8,8 @@
 
 (*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 >>
@@ -25,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$ >>
@@ -79,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 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 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<
@@ -114,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 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 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
diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4
index 56deb61f3..682188732 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 Extend.user_symbol * string
+| ExtNonTerminal of user_symbol * string
 
 let mlexpr_of_list f l =
   List.fold_right
@@ -48,14 +63,14 @@ 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 (e = "tactic");
     if l = 5 then <:expr< Extend.Aentry (Pcoq.name_of_entry Pcoq.Tactic.binder_tactic) >>
@@ -63,10 +78,10 @@ let rec mlexpr_of_prod_entry_key f = function
 
 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 c84e9d140..7d4cc0200 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 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 51c382b3b..bbd3d8a62 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -68,7 +68,7 @@ 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