ML extensions use untyped representation of user entries.

6 files changed, 102 insertions, 95 deletions

diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index cb006186a..d976ee019 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -12,6 +12,7 @@ open Genarg
 open Q_util
 open Egramml
 open Compat
+open Extend
 open Pcoq
 
 let loc = CompatLoc.ghost
@@ -42,37 +43,33 @@ let make_topwit loc arg = <:expr< Genarg.topwit $make_wit loc arg$ >>
 
 let has_extraarg l =
   let check = function
-  | ExtNonTerminal(EntryName (t, _), _) ->
-    begin match Genarg.unquote t with
-    | ExtraArgType _ -> true
-    | _ -> false
-    end
+  | ExtNonTerminal(ExtraArgType _, _, _) -> true
   | _ -> false
   in
   List.exists check l
 
-let rec is_possibly_empty : type s a. (s, a) entry_key -> bool = function
-| Aopt _ -> true
-| Alist0 _ -> true
-| Alist0sep _ -> true
-| Amodifiers _ -> true
-| Alist1 t -> is_possibly_empty t
-| Alist1sep (t, _) -> is_possibly_empty t
+let rec is_possibly_empty = function
+| Uopt _ -> true
+| Ulist0 _ -> true
+| Ulist0sep _ -> true
+| Umodifiers _ -> true
+| Ulist1 t -> is_possibly_empty t
+| Ulist1sep (t, _) -> is_possibly_empty t
 | _ -> false
 
-let rec get_empty_entry : type s a. (s, a) entry_key -> _ = function
-| Aopt _ -> <:expr< None >>
-| Alist0 _ -> <:expr< [] >>
-| Alist0sep _ -> <:expr< [] >>
-| Amodifiers _ -> <:expr< [] >>
-| Alist1 t -> <:expr< [$get_empty_entry t$] >>
-| Alist1sep (t, _) -> <:expr< [$get_empty_entry t$] >>
+let rec get_empty_entry = function
+| Uopt _ -> <:expr< None >>
+| Ulist0 _ -> <:expr< [] >>
+| Ulist0sep _ -> <:expr< [] >>
+| Umodifiers _ -> <:expr< [] >>
+| Ulist1 t -> <:expr< [$get_empty_entry t$] >>
+| Ulist1sep (t, _) -> <:expr< [$get_empty_entry t$] >>
 | _ -> assert false
 
 let statically_known_possibly_empty s (prods,_) =
   List.for_all (function
-    | ExtNonTerminal(EntryName (t, e), _) ->
-      begin match Genarg.unquote t with
+    | ExtNonTerminal(t, e, _) ->
+      begin match t with
       | ExtraArgType s' ->
         (* For ExtraArg we don't know (we'll have to test dynamically) *)
         (* unless it is a recursive call *)
@@ -91,10 +88,10 @@ let possibly_empty_subentries loc (prods,act) =
   in
   let rec aux = function
     | [] -> <:expr< let loc = $default_loc$ in let _ = loc in $act$ >>
-    | ExtNonTerminal(EntryName (_, e), id) :: tl when is_possibly_empty e ->
+    | ExtNonTerminal(_, e, id) :: tl when is_possibly_empty e ->
         bind_name id (get_empty_entry e) (aux tl)
-    | ExtNonTerminal(EntryName (t, _), id) :: tl ->
-        let t = match Genarg.unquote t with
+    | ExtNonTerminal(t, _, id) :: tl ->
+        let t = match t with
         | ExtraArgType _ as t -> t
         | _ -> assert false
         in
@@ -132,8 +129,7 @@ let make_possibly_empty_subentries loc s cl =
 let make_act loc act pil =
   let rec make = function
     | [] -> <:expr< (fun loc -> $act$) >>
-    | ExtNonTerminal (EntryName (t, _), p) :: tl ->
-        let t = Genarg.unquote t in
+    | ExtNonTerminal (t, _, p) :: tl ->
 	let p = Names.Id.to_string p in
 	<:expr<
             (fun $lid:p$ ->
@@ -145,7 +141,7 @@ let make_act loc act pil =
 
 let make_prod_item = function
   | ExtTerminal s -> <:expr< Pcoq.Atoken (Lexer.terminal $mlexpr_of_string s$) >>
-  | ExtNonTerminal (EntryName (_, g), _) -> mlexpr_of_prod_entry_key g
+  | ExtNonTerminal (_, g, _) -> mlexpr_of_prod_entry_key g
 
 let rec make_prod = function
 | [] -> <:expr< Extend.Stop >>
@@ -303,8 +299,8 @@ EXTEND
       | e = argtype; LIDENT "option" -> OptArgType e ]
     | "0"
       [ e = LIDENT ->
-        let EntryName (t, _) = interp_entry_name false TgAny e "" in
-        Genarg.unquote t
+        let e = parse_user_entry e "" in
+        type_of_user_symbol e
       | "("; e = argtype; ")" -> e ] ]
   ;
   argrule:
@@ -312,11 +308,11 @@ EXTEND
   ;
   genarg:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
-        let entry = interp_entry_name false TgAny e "" in
-        ExtNonTerminal (entry, Names.Id.of_string s)
+        let e = parse_user_entry e "" in
+        ExtNonTerminal (type_of_user_symbol e, e, Names.Id.of_string s)
       | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
-        let entry = interp_entry_name false TgAny e sep in
-        ExtNonTerminal (entry, Names.Id.of_string s)
+        let e = parse_user_entry e sep in
+        ExtNonTerminal (type_of_user_symbol e, e, Names.Id.of_string s)
       | s = STRING ->
 	  if String.length s > 0 && Util.is_letter s.[0] then
 	    Lexer.add_keyword s;
diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4
index 4c1f25941..af9de2df2 100644
--- a/grammar/q_util.ml4
+++ b/grammar/q_util.ml4
@@ -8,11 +8,12 @@
 
 (* This file defines standard combinators to build ml expressions *)
 
+open Extend
 open Compat
 
 type extend_token =
 | ExtTerminal of string
-| ExtNonTerminal of unit Pcoq.entry_name * Names.Id.t
+| ExtNonTerminal of Genarg.argument_type * Extend.user_symbol * Names.Id.t
 
 let mlexpr_of_list f l =
   List.fold_right
@@ -66,23 +67,44 @@ let mlexpr_of_token = function
 | Tok.BULLET s -> <:expr< Tok.BULLET $mlexpr_of_string s$ >>
 | Tok.EOI -> <:expr< Tok.EOI >>
 
-let rec mlexpr_of_prod_entry_key : type s a. (s, a) Pcoq.entry_key -> _ = function
-  | Pcoq.Atoken t -> <:expr< Pcoq.Atoken $mlexpr_of_token t$ >>
-  | Pcoq.Alist1 s -> <:expr< Pcoq.Alist1 $mlexpr_of_prod_entry_key s$ >>
-  | Pcoq.Alist1sep (s,sep) -> <:expr< Pcoq.Alist1sep $mlexpr_of_prod_entry_key s$ $str:sep$ >>
-  | Pcoq.Alist0 s -> <:expr< Pcoq.Alist0 $mlexpr_of_prod_entry_key s$ >>
-  | Pcoq.Alist0sep (s,sep) -> <:expr< Pcoq.Alist0sep $mlexpr_of_prod_entry_key s$ $str:sep$ >>
-  | Pcoq.Aopt s -> <:expr< Pcoq.Aopt $mlexpr_of_prod_entry_key s$ >>
-  | Pcoq.Amodifiers s -> <:expr< Pcoq.Amodifiers $mlexpr_of_prod_entry_key s$ >>
-  | Pcoq.Aself -> <:expr< Pcoq.Aself >>
-  | Pcoq.Anext -> <:expr< Pcoq.Anext >>
-  | Pcoq.Aentry e ->
-    begin match Entry.repr e with
-    | Entry.Dynamic s -> <:expr< Pcoq.Aentry (Pcoq.name_of_entry $lid:s$) >>
-    | Entry.Static (u, s) -> <:expr< Pcoq.Aentry (Entry.unsafe_of_name ($str:u$, $str:s$)) >>
-    end
-  | Pcoq.Aentryl (e, l) ->
-    begin match Entry.repr e with
-    | Entry.Dynamic s -> <:expr< Pcoq.Aentryl (Pcoq.name_of_entry $lid:s$) >>
-    | Entry.Static (u, s) -> <:expr< Pcoq.Aentryl (Entry.unsafe_of_name ($str:u$, $str:s$)) $mlexpr_of_int l$ >>
+let repr_entry e =
+  let entry u =
+    let _ = Pcoq.get_entry u e in
+    Some (Entry.univ_name u, e)
+  in
+  try entry Pcoq.uprim with Not_found ->
+  try entry Pcoq.uconstr with Not_found ->
+  try entry Pcoq.utactic with Not_found -> None
+
+let rec mlexpr_of_prod_entry_key = function
+  | Extend.Ulist1 s -> <:expr< Pcoq.Alist1 $mlexpr_of_prod_entry_key s$ >>
+  | Extend.Ulist1sep (s,sep) -> <:expr< Pcoq.Alist1sep $mlexpr_of_prod_entry_key s$ $str:sep$ >>
+  | Extend.Ulist0 s -> <:expr< Pcoq.Alist0 $mlexpr_of_prod_entry_key s$ >>
+  | Extend.Ulist0sep (s,sep) -> <:expr< Pcoq.Alist0sep $mlexpr_of_prod_entry_key s$ $str:sep$ >>
+  | Extend.Uopt s -> <:expr< Pcoq.Aopt $mlexpr_of_prod_entry_key s$ >>
+  | Extend.Umodifiers s -> <:expr< Pcoq.Amodifiers $mlexpr_of_prod_entry_key s$ >>
+  | Extend.Uentry e ->
+    begin match repr_entry e with
+    | None -> <:expr< Pcoq.Aentry (Pcoq.name_of_entry $lid:e$) >>
+    | Some (u, s) -> <:expr< Pcoq.Aentry (Entry.unsafe_of_name ($str:u$, $str:s$)) >>
     end
+  | Extend.Uentryl (e, l) ->
+    (** Keep in sync with Pcoq! *)
+    assert (CString.equal e "tactic");
+    if l = 5 then <:expr< Pcoq.Aentry (Pcoq.name_of_entry Pcoq.Tactic.binder_tactic) >>
+    else <:expr< Pcoq.Aentryl (Pcoq.name_of_entry Pcoq.Tactic.tactic_expr) $mlexpr_of_int l$ >>
+
+let type_entry u e =
+  let Pcoq.TypedEntry (t, _) = Pcoq.get_entry u e in
+  Genarg.unquote t
+
+let rec type_of_user_symbol = function
+| Ulist1 s | Ulist1sep (s, _) | Ulist0 s | Ulist0sep (s, _) | Umodifiers s ->
+  Genarg.ListArgType (type_of_user_symbol s)
+| Uopt s ->
+  Genarg.OptArgType (type_of_user_symbol s)
+| Uentry e | Uentryl (e, _) ->
+  try type_entry Pcoq.uprim e with Not_found ->
+  try type_entry Pcoq.uconstr e with Not_found ->
+  try type_entry Pcoq.utactic e with Not_found ->
+  Genarg.ExtraArgType e
diff --git a/grammar/q_util.mli b/grammar/q_util.mli
index d9359de1e..81ad42266 100644
--- a/grammar/q_util.mli
+++ b/grammar/q_util.mli
@@ -10,7 +10,7 @@ open Compat (* necessary for camlp4 *)
 
 type extend_token =
 | ExtTerminal of string
-| ExtNonTerminal of unit Pcoq.entry_name * Names.Id.t
+| ExtNonTerminal of Genarg.argument_type * Extend.user_symbol * Names.Id.t
 
 val mlexpr_of_list :  ('a -> MLast.expr) -> 'a list -> MLast.expr
 
@@ -34,4 +34,6 @@ val mlexpr_of_string : string -> MLast.expr
 
 val mlexpr_of_option : ('a -> MLast.expr) -> 'a option -> MLast.expr
 
-val mlexpr_of_prod_entry_key : ('self, 'a) Pcoq.entry_key -> MLast.expr
+val mlexpr_of_prod_entry_key : Extend.user_symbol -> MLast.expr
+
+val type_of_user_symbol : Extend.user_symbol -> Genarg.argument_type
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index a870722fd..7ae9baf72 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -27,24 +27,23 @@ let plugin_name = <:expr< __coq_plugin_name >>
 
 let rec make_patt = function
   | [] -> <:patt< [] >>
-  | ExtNonTerminal (_, p) :: l ->
+  | ExtNonTerminal (_, _, p) :: l ->
       let p = Names.Id.to_string p in
       <:patt< [ $lid:p$ :: $make_patt l$ ] >>
   | _::l -> make_patt l
 
 let rec make_when loc = function
   | [] -> <:expr< True >>
-  | ExtNonTerminal (EntryName (t, _), p) :: l ->
+  | ExtNonTerminal (t, _, p) :: l ->
       let p = Names.Id.to_string p in
       let l = make_when loc l in
-      let t = mlexpr_of_argtype loc (Genarg.unquote t) 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 (EntryName (t, _), p) :: l ->
-      let t = Genarg.unquote t in
+  | ExtNonTerminal (t, _, p) :: l ->
       let p = Names.Id.to_string p in
       let loc = MLast.loc_of_expr e in
       let e = make_let raw e l in
@@ -56,7 +55,7 @@ let rec make_let raw e = function
 
 let rec extract_signature = function
   | [] -> []
-  | ExtNonTerminal (EntryName (t, _), _) :: l -> Genarg.unquote t :: extract_signature l
+  | ExtNonTerminal (t, _, _) :: l -> t :: extract_signature l
   | _::l -> extract_signature l
 
 
@@ -78,18 +77,9 @@ let make_fun_clauses loc s l =
   let map c = Compat.make_fun loc [make_clause c] in
   mlexpr_of_list map l
 
-let rec make_args = function
-  | [] -> <:expr< [] >>
-  | ExtNonTerminal (EntryName (t, _), p) :: l ->
-      let t = Genarg.unquote t in
-      let p = Names.Id.to_string p in
-      <:expr< [ Genarg.in_gen $make_topwit loc t$ $lid:p$ :: $make_args l$ ] >>
-  | _::l -> make_args l
-
 let make_prod_item = function
   | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >>
-  | ExtNonTerminal (EntryName (nt, g), id) ->
-      let nt = Genarg.unquote nt in
+  | ExtNonTerminal (nt, g, id) ->
       <:expr< Egramml.GramNonTerminal $default_loc$ $make_rawwit loc nt$
       $mlexpr_of_prod_entry_key g$ >>
 
@@ -98,9 +88,8 @@ let mlexpr_of_clause cl =
 
 let rec make_tags loc = function
   | [] -> <:expr< [] >>
-  | ExtNonTerminal (EntryName (t, _), p) :: l ->
+  | ExtNonTerminal (t, _, p) :: l ->
       let l = make_tags loc l in
-      let t = Genarg.unquote t in
       let t = mlexpr_of_argtype loc t in
       <:expr< [ $t$ :: $l$ ] >>
   | _::l -> make_tags loc l
@@ -115,8 +104,7 @@ let make_one_printing_rule (pt,_,e) =
 let make_printing_rule r = mlexpr_of_list make_one_printing_rule r
 
 let make_empty_check = function
-| ExtNonTerminal (EntryName (t, e), _)->
-  let t = Genarg.unquote t in
+| ExtNonTerminal (t, e, _)->
   let is_extra = match t with ExtraArgType _ -> true | _ -> false in
   if is_possibly_empty e || is_extra then
     (* This possibly parses epsilon *)
@@ -153,17 +141,11 @@ let rec possibly_atomic loc = function
 (** Special treatment of constr entries *)
 let is_constr_gram = function
 | ExtTerminal _ -> false
-| ExtNonTerminal (EntryName (_, e), _) ->
-  match e with
-  | Aentry e ->
-    begin match Entry.repr e with
-    | Entry.Static ("constr", "constr") -> true
-    | _ -> false
-    end
-  | _ -> false
+| ExtNonTerminal (_, Extend.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
@@ -253,11 +235,11 @@ EXTEND
   ;
   tacargs:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
-        let entry = interp_entry_name false TgAny e "" in
-        ExtNonTerminal (entry, Names.Id.of_string s)
+        let e = parse_user_entry e "" in
+        ExtNonTerminal (type_of_user_symbol e, e, Names.Id.of_string s)
       | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
-        let entry = interp_entry_name false TgAny e sep in
-        ExtNonTerminal (entry, Names.Id.of_string s)
+        let e = parse_user_entry e sep in
+        ExtNonTerminal (type_of_user_symbol e, e, Names.Id.of_string s)
       | s = STRING ->
 	if String.is_empty s then Errors.user_err_loc (!@loc,"",Pp.str "Empty terminal.");
         ExtTerminal s
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4
index 8de59e5cd..9d78c104e 100644
--- a/grammar/vernacextend.ml4
+++ b/grammar/vernacextend.ml4
@@ -34,8 +34,7 @@ type rule = {
 
 let rec make_let e = function
   | [] -> e
-  | ExtNonTerminal (EntryName (t, _), p) :: l ->
-      let t = Genarg.unquote t in
+  | ExtNonTerminal (t, _, p) :: l ->
       let p = Names.Id.to_string p in
       let loc = MLast.loc_of_expr e in
       let e = make_let e l in
@@ -50,7 +49,7 @@ 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 (Names.Id.to_string p)
+  | ExtNonTerminal (_, _, p) -> Some (Names.Id.to_string p)
   | _ -> None) pt in
   let fold accu id = <:expr< let _ = $lid:id$ in $accu$ >> in
   let names = List.fold_left fold <:expr< () >> names in
@@ -181,11 +180,11 @@ EXTEND
   ;
   args:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
-        let entry = interp_entry_name false TgAny e "" in
-        ExtNonTerminal (entry, Names.Id.of_string s)
+        let e = parse_user_entry e "" in
+        ExtNonTerminal (type_of_user_symbol e, e, Names.Id.of_string s)
       | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
-        let entry = interp_entry_name false TgAny e sep in
-        ExtNonTerminal (entry, Names.Id.of_string s)
+        let e = parse_user_entry e sep in
+        ExtNonTerminal (type_of_user_symbol e, e, Names.Id.of_string s)
       | s = STRING ->
         ExtTerminal s
     ] ]
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 592c87919..aa2e092ad 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -153,11 +153,15 @@ type gram_universe = Entry.universe
 
 val get_univ : string -> gram_universe
 
+type typed_entry = TypedEntry : 'a raw_abstract_argument_type * 'a Gram.entry -> typed_entry
+
 val uprim : gram_universe
 val uconstr : gram_universe
 val utactic : gram_universe
 val uvernac : gram_universe
 
+val get_entry : gram_universe -> string -> typed_entry
+
 val create_generic_entry : string -> ('a, rlevel) abstract_argument_type ->
   'a Gram.entry
 
@@ -282,6 +286,8 @@ type _ target = TgAny : 's target | TgTactic : int -> raw_tactic_expr target
 val interp_entry_name : bool (** true to fail on unknown entry *) ->
   's target -> string -> string -> 's entry_name
 
+val parse_user_entry : string -> string -> user_symbol
+
 (** Recover the list of all known tactic notation entries. *)
 val list_entry_names : unit -> (string * argument_type) list