Finer type for Pcoq.interp_entry_name.

6 files changed, 60 insertions, 48 deletions

diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index 51949e8aa..cfabd2688 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -280,8 +280,8 @@ EXTEND
       | e = argtype; LIDENT "option" -> OptArgType e ]
     | "0"
       [ e = LIDENT ->
-        let EntryName (t, _) = interp_entry_name false None e "" in
-        t
+        let EntryName (t, _) = interp_entry_name false TgAny e "" in
+        Genarg.unquote t
       | "("; e = argtype; ")" -> e ] ]
   ;
   argrule:
@@ -289,11 +289,11 @@ EXTEND
   ;
   genarg:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
-        let EntryName (t, g) = interp_entry_name false None e "" in
-	GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s))
+        let EntryName (t, g) = interp_entry_name false TgAny e "" in
+	GramNonTerminal (!@loc, Genarg.unquote t, g, Some (Names.Id.of_string s))
       | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
-        let EntryName (t, g) = interp_entry_name false None e sep in
-	GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s))
+        let EntryName (t, g) = interp_entry_name false TgAny e sep in
+	GramNonTerminal (!@loc, Genarg.unquote t, g, Some (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/tacextend.ml4 b/grammar/tacextend.ml4
index 2c9a73a37..8c2a45bae 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -261,11 +261,11 @@ EXTEND
   ;
   tacargs:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
-        let EntryName (t, g) = interp_entry_name false None e "" in
-        GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s))
+        let EntryName (t, g) = interp_entry_name false TgAny e "" in
+        GramNonTerminal (!@loc, Genarg.unquote t, g, Some (Names.Id.of_string s))
       | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
-        let EntryName (t, g) = interp_entry_name false None e sep in
-        GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s))
+        let EntryName (t, g) = interp_entry_name false TgAny e sep in
+        GramNonTerminal (!@loc, Genarg.unquote t, g, Some (Names.Id.of_string s))
       | s = STRING ->
 	if String.is_empty s then Errors.user_err_loc (!@loc,"",Pp.str "Empty terminal.");
         GramTerminal s
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4
index f0fde2bf8..5d4309aba 100644
--- a/grammar/vernacextend.ml4
+++ b/grammar/vernacextend.ml4
@@ -181,11 +181,11 @@ EXTEND
   ;
   args:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
-        let EntryName (t, g) = interp_entry_name false None e "" in
-        GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s))
+        let EntryName (t, g) = interp_entry_name false TgAny e "" in
+        GramNonTerminal (!@loc, Genarg.unquote t, g, Some (Names.Id.of_string s))
       | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
-        let EntryName (t, g) = interp_entry_name false None e sep in
-        GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s))
+        let EntryName (t, g) = interp_entry_name false TgAny e sep in
+        GramNonTerminal (!@loc, Genarg.unquote t, g, Some (Names.Id.of_string s))
       | s = STRING ->
         GramTerminal s
     ] ]
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 2227f7e9c..4bb1fd0a4 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -80,7 +80,8 @@ type ('self, 'a) entry_key = ('self, 'a) Extend.symbol =
 | Aentry : 'a Entry.t -> ('self, 'a) entry_key
 | Aentryl : 'a Entry.t * int -> ('self, 'a) entry_key
 
-type 's entry_name = EntryName : entry_type * ('s, 'a) entry_key -> 's entry_name
+type 's entry_name = EntryName :
+  'a raw_abstract_argument_type * ('s, 'a) entry_key -> 's entry_name
 
 module type Gramtypes =
 sig
@@ -789,51 +790,64 @@ let atactic n =
   if n = 5 then Aentry (name_of_entry Tactic.binder_tactic)
   else Aentryl (name_of_entry Tactic.tactic_expr, n)
 
+let unsafe_of_genarg : argument_type -> 'a raw_abstract_argument_type =
+  (** FIXME *)
+  Obj.magic
+
 let try_get_entry u s =
   (** Order the effects: type_of_entry can raise Not_found *)
   let typ = type_of_entry u s in
-  Some typ, Aentry (Entry.unsafe_of_name (Entry.univ_name u, s))
+  let typ = unsafe_of_genarg typ in
+  EntryName (typ, Aentry (Entry.unsafe_of_name (Entry.univ_name u, s)))
+
+let wit_list : 'a raw_abstract_argument_type -> 'a list raw_abstract_argument_type =
+  fun t -> unsafe_of_genarg (ListArgType (unquote t))
+
+let wit_opt : 'a raw_abstract_argument_type -> 'a option raw_abstract_argument_type =
+  fun t -> unsafe_of_genarg (OptArgType (unquote t))
+
+type _ target =
+| TgAny : 's target
+| TgTactic : int -> Tacexpr.raw_tactic_expr target
+
+(** Quite ad-hoc *)
+let get_tacentry (type s) (n : int) (t : s target) : s entry_name = match t with
+| TgAny -> EntryName (rawwit wit_tactic, atactic n)
+| TgTactic m ->
+  let check_lvl n =
+    Int.equal m n
+    && not (Int.equal m 5) (* Because tactic5 is at binder_tactic *)
+    && not (Int.equal m 0) (* Because tactic0 is at simple_tactic *)
+  in
+  if check_lvl n then EntryName (rawwit wit_tactic, Aself)
+  else if check_lvl (n + 1) then EntryName (rawwit wit_tactic, Anext)
+  else EntryName (rawwit wit_tactic, atactic n)
 
 let rec interp_entry_name static up_level s sep =
   let l = String.length s in
   if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then
     let EntryName (t, g) = interp_entry_name static up_level (String.sub s 3 (l-8)) "" in
-    EntryName (ListArgType t, Alist1 g)
+    EntryName (wit_list t, Alist1 g)
   else if l > 12 && coincide s "ne_" 0 &&
                    coincide s "_list_sep" (l-9) then
     let EntryName (t, g) = interp_entry_name static up_level (String.sub s 3 (l-12)) "" in
-    EntryName (ListArgType t, Alist1sep (g,sep))
+    EntryName (wit_list t, Alist1sep (g,sep))
   else if l > 5 && coincide s "_list" (l-5) then
     let EntryName (t, g) = interp_entry_name static up_level (String.sub s 0 (l-5)) "" in
-    EntryName (ListArgType t, Alist0 g)
+    EntryName (wit_list t, Alist0 g)
   else if l > 9 && coincide s "_list_sep" (l-9) then
     let EntryName (t, g) = interp_entry_name static up_level (String.sub s 0 (l-9)) "" in
-    EntryName (ListArgType t, Alist0sep (g,sep))
+    EntryName (wit_list t, Alist0sep (g,sep))
   else if l > 4 && coincide s "_opt" (l-4) then
     let EntryName (t, g) = interp_entry_name static up_level (String.sub s 0 (l-4)) "" in
-    EntryName (OptArgType t, Aopt g)
+    EntryName (wit_opt t, Aopt g)
   else if l > 5 && coincide s "_mods" (l-5) then
     let EntryName (t, g) = interp_entry_name static up_level (String.sub s 0 (l-1)) "" in
-    EntryName (ListArgType t, Amodifiers g)
+    EntryName (wit_list t, Amodifiers g)
   else
     let s = match s with "hyp" -> "var" | _ -> s in
-    let check_lvl n = match up_level with
-    | None -> false
-    | Some m -> Int.equal m n
-                && not (Int.equal m 5) (* Because tactic5 is at binder_tactic *)
-                && not (Int.equal m 0) (* Because tactic0 is at simple_tactic *)
-    in
-    let t, se =
       match tactic_level s with
-      | Some n ->
-        (** Quite ad-hoc *)
-        let t = unquote (rawwit wit_tactic) in
-        let se =
-          if check_lvl n then Aself
-          else if check_lvl (n + 1) then Anext
-          else atactic n
-        in
-        (Some t, se)
+      | Some n -> get_tacentry n up_level
       | None ->
       try try_get_entry uprim s with Not_found ->
       try try_get_entry uconstr s with Not_found ->
@@ -841,12 +855,7 @@ let rec interp_entry_name static up_level s sep =
 	if static then
 	  error ("Unknown entry "^s^".")
 	else
-	  None, Aentry (Entry.dynamic s) in
-    let t =
-      match t with
-	| Some t -> t
-	| None -> ExtraArgType s in
-    EntryName (t, se)
+	  EntryName (unsafe_of_genarg (ExtraArgType s), Aentry (Entry.dynamic s))
 
 let list_entry_names () =
   let add_entry key (entry, _) accu = (key, entry) :: accu in
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 8a1bc884a..69b25879b 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -285,12 +285,15 @@ val name_of_entry : 'a Gram.entry -> 'a Entry.t
 val symbol_of_prod_entry_key :
   ('self, 'a) entry_key -> Gram.symbol
 
-type 's entry_name = EntryName : entry_type * ('s, 'a) entry_key -> 's entry_name
+type 's entry_name = EntryName :
+  'a raw_abstract_argument_type * ('s, 'a) entry_key -> 's entry_name
 
 (** Interpret entry names of the form "ne_constr_list" as entry keys   *)
 
+type _ target = TgAny : 's target | TgTactic : int -> raw_tactic_expr target
+
 val interp_entry_name : bool (** true to fail on unknown entry *) ->
-  int option -> string -> string -> 's entry_name
+  's target -> string -> string -> 's entry_name
 
 (** Recover the list of all known tactic notation entries. *)
 val list_entry_names : unit -> (string * entry_type) list
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index ca263e6cb..94b7fe5bc 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -49,8 +49,8 @@ let interp_prod_item lev = function
   | TacTerm s -> GramTerminal s
   | TacNonTerm (loc, nt, po) ->
       let sep = match po with Some (_,sep) -> sep | _ -> "" in
-      let EntryName (etyp, e) = interp_entry_name true (Some lev) nt sep in
-      GramNonTerminal (loc, etyp, e, Option.map fst po)
+      let EntryName (etyp, e) = interp_entry_name true (TgTactic lev) nt sep in
+      GramNonTerminal (loc, Genarg.unquote etyp, e, Option.map fst po)
 
 let make_terminal_status = function
   | GramTerminal s -> Some s