Pcoq.prod_entry_key now uses a GADT to statically enforce typedness.

10 files changed, 81 insertions, 68 deletions

diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index fe0959ddbc..7c20ff18e9 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -54,15 +54,22 @@ let make_topwit loc arg = <:expr< Genarg.topwit $make_wit loc arg$ >>
 let has_extraarg =
   List.exists (function GramNonTerminal(_,ExtraArgType _,_,_) -> true | _ -> false)
 
-let rec is_possibly_empty = function
-| Aopt _ | Alist0 _ | Alist0sep _ | Amodifiers _ -> true
-| Alist1 t | Alist1sep (t, _) -> is_possibly_empty t
+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
 | _ -> false
 
-let rec get_empty_entry = function
+let rec get_empty_entry : type s a. (s, a) entry_key -> _ = function
 | Aopt _ -> <:expr< None >>
-| Alist0 _ | Alist0sep _ | Amodifiers _ -> <:expr< [] >>
-| Alist1 t | Alist1sep (t, _) -> <:expr< [$get_empty_entry t$] >>
+| Alist0 _ -> <:expr< [] >>
+| Alist0sep _ -> <:expr< [] >>
+| Amodifiers _ -> <:expr< [] >>
+| Alist1 t -> <:expr< [$get_empty_entry t$] >>
+| Alist1sep (t, _) -> <:expr< [$get_empty_entry t$] >>
 | _ -> assert false
 
 let statically_known_possibly_empty s (prods,_) =
@@ -272,7 +279,9 @@ EXTEND
       [ e = argtype; LIDENT "list" -> ListArgType e
       | e = argtype; LIDENT "option" -> OptArgType e ]
     | "0"
-      [ e = LIDENT -> fst (interp_entry_name false None e "")
+      [ e = LIDENT ->
+        let EntryName (t, _) = interp_entry_name false None e "" in
+        t
       | "("; e = argtype; ")" -> e ] ]
   ;
   argrule:
@@ -280,10 +289,10 @@ EXTEND
   ;
   genarg:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
-        let t, g = interp_entry_name false None e "" in
+        let EntryName (t, g) = interp_entry_name false None e "" in
 	GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s))
       | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
-        let t, g = interp_entry_name false None e sep in
+        let EntryName (t, g) = interp_entry_name false None e sep in
 	GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s))
       | s = STRING ->
 	  if String.length s > 0 && Util.is_letter s.[0] then
diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4
index 18b1ccd3be..b1eabdd98b 100644
--- a/grammar/q_util.ml4
+++ b/grammar/q_util.ml4
@@ -49,7 +49,7 @@ let mlexpr_of_option f = function
   | None -> <:expr< None >>
   | Some e -> <:expr< Some $f e$ >>
 
-let rec mlexpr_of_prod_entry_key = function
+let rec mlexpr_of_prod_entry_key : type s a. (s, a) Pcoq.entry_key -> _ = function
   | 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$ >>
diff --git a/grammar/q_util.mli b/grammar/q_util.mli
index 7393a0d588..d01fb1e9a0 100644
--- a/grammar/q_util.mli
+++ b/grammar/q_util.mli
@@ -30,4 +30,4 @@ val mlexpr_of_string : string -> MLast.expr
 
 val mlexpr_of_option : ('a -> MLast.expr) -> 'a option -> MLast.expr
 
-val mlexpr_of_prod_entry_key : Pcoq.prod_entry_key -> MLast.expr
+val mlexpr_of_prod_entry_key : ('self, 'a) Pcoq.entry_key -> MLast.expr
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index 2e725b46c3..70151cef1b 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -257,10 +257,10 @@ EXTEND
   ;
   tacargs:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
-        let t, g = interp_entry_name false None e "" in
+        let EntryName (t, g) = interp_entry_name false None e "" in
         GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s))
       | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
-        let t, g = interp_entry_name false None e sep in
+        let EntryName (t, g) = interp_entry_name false None e sep in
         GramNonTerminal (!@loc, 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.");
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4
index 03061d8bde..d99af6a33d 100644
--- a/grammar/vernacextend.ml4
+++ b/grammar/vernacextend.ml4
@@ -181,10 +181,10 @@ EXTEND
   ;
   args:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
-        let t, g = interp_entry_name false None e "" in
+        let EntryName (t, g) = interp_entry_name false None e "" in
         GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s))
       | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
-        let t, g = interp_entry_name false None e sep in
+        let EntryName (t, g) = interp_entry_name false None e sep in
         GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s))
       | s = STRING ->
         GramTerminal s
diff --git a/parsing/egramml.ml b/parsing/egramml.ml
index 8fe03b3632..8f07087085 100644
--- a/parsing/egramml.ml
+++ b/parsing/egramml.ml
@@ -30,8 +30,8 @@ let make_generic_action
 
 type grammar_prod_item =
   | GramTerminal of string
-  | GramNonTerminal of
-      Loc.t * argument_type * prod_entry_key * Id.t option
+  | GramNonTerminal :
+      Loc.t * argument_type * ('s, 'a) entry_key * Id.t option -> grammar_prod_item
 
 let make_prod_item = function
   | GramTerminal s -> (gram_token_of_string s, None)
diff --git a/parsing/egramml.mli b/parsing/egramml.mli
index 9ebb5b83b5..60ec6a05a8 100644
--- a/parsing/egramml.mli
+++ b/parsing/egramml.mli
@@ -13,8 +13,8 @@
 
 type grammar_prod_item =
   | GramTerminal of string
-  | GramNonTerminal of Loc.t * Genarg.argument_type *
-      Pcoq.prod_entry_key * Names.Id.t option
+  | GramNonTerminal : Loc.t * Genarg.argument_type *
+      ('s, 'a) Pcoq.entry_key * Names.Id.t option -> grammar_prod_item
 
 val extend_vernac_command_grammar :
   Vernacexpr.extend_name -> Vernacexpr.vernac_expr Pcoq.Gram.entry option ->
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 48dc1372ce..63662a9561 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -36,26 +36,6 @@ let camlp4_verbosity silent f x =
 let camlp4_verbose f x = camlp4_verbosity (Flags.is_verbose ()) f x
 
 
-(** General entry keys *)
-
-(** This intermediate abstract representation of entries can
-   both be reified into mlexpr for the ML extensions and
-   dynamically interpreted as entries for the Coq level extensions
-*)
-
-type prod_entry_key =
-  | Alist1 of prod_entry_key
-  | Alist1sep of prod_entry_key * string
-  | Alist0 of prod_entry_key
-  | Alist0sep of prod_entry_key * string
-  | Aopt of prod_entry_key
-  | Amodifiers of prod_entry_key
-  | Aself
-  | Anext
-  | Atactic of int
-  | Agram of string
-  | Aentry of string * string
-
 (** [grammar_object] is the superclass of all grammar entries *)
 
 module type Gramobj =
@@ -80,6 +60,28 @@ let type_of_typed_entry (t,e) = t
 let object_of_typed_entry (t,e) = e
 let weaken_entry x = Gramobj.weaken_entry x
 
+(** General entry keys *)
+
+(** This intermediate abstract representation of entries can
+   both be reified into mlexpr for the ML extensions and
+   dynamically interpreted as entries for the Coq level extensions
+*)
+
+type ('self, _) entry_key =
+| Alist1 : ('self, 'a) entry_key -> ('self, 'a list) entry_key
+| Alist1sep : ('self, 'a) entry_key * string -> ('self, 'a list) entry_key
+| Alist0 : ('self, 'a) entry_key -> ('self, 'a list) entry_key
+| Alist0sep : ('self, 'a) entry_key * string -> ('self, 'a list) entry_key
+| Aopt : ('self, 'a) entry_key -> ('self, 'a option) entry_key
+| Amodifiers : ('self, 'a) entry_key -> ('self, 'a list) entry_key
+| Aself : ('self, 'self) entry_key
+| Anext : ('self, 'self) entry_key
+| Atactic : int -> ('self, Tacexpr.raw_tactic_expr) entry_key
+| Agram : string -> ('self, 'a) entry_key
+| Aentry : string * string -> ('self, 'a) entry_key
+
+type entry_name = EntryName : entry_type * ('self, 'a) entry_key -> entry_name
+
 module type Gramtypes =
 sig
   val inGramObj : 'a raw_abstract_argument_type -> 'a G.entry -> typed_entry
@@ -689,7 +691,7 @@ let rec symbol_of_constr_prod_entry_key assoc from forpat typ =
 
 (** Binding general entry keys to symbol *)
 
-let rec symbol_of_prod_entry_key = function
+let rec symbol_of_prod_entry_key : type s a. (s, a) entry_key -> _ = function
   | Alist1 s -> Symbols.slist1 (symbol_of_prod_entry_key s)
   | Alist1sep (s,sep) ->
       Symbols.slist1sep (symbol_of_prod_entry_key s, gram_token_of_string sep)
@@ -756,24 +758,24 @@ let type_of_entry u s =
 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 t, g = interp_entry_name static up_level (String.sub s 3 (l-8)) "" in
-    ListArgType t, Alist1 g
+    let EntryName (t, g) = interp_entry_name static up_level (String.sub s 3 (l-8)) "" in
+    EntryName (ListArgType t, Alist1 g)
   else if l > 12 && coincide s "ne_" 0 &&
                    coincide s "_list_sep" (l-9) then
-    let t, g = interp_entry_name static up_level (String.sub s 3 (l-12)) "" in
-    ListArgType t, Alist1sep (g,sep)
+    let EntryName (t, g) = interp_entry_name static up_level (String.sub s 3 (l-12)) "" in
+    EntryName (ListArgType t, Alist1sep (g,sep))
   else if l > 5 && coincide s "_list" (l-5) then
-    let t, g = interp_entry_name static up_level (String.sub s 0 (l-5)) "" in
-    ListArgType t, Alist0 g
+    let EntryName (t, g) = interp_entry_name static up_level (String.sub s 0 (l-5)) "" in
+    EntryName (ListArgType t, Alist0 g)
   else if l > 9 && coincide s "_list_sep" (l-9) then
-    let t, g = interp_entry_name static up_level (String.sub s 0 (l-9)) "" in
-    ListArgType t, Alist0sep (g,sep)
+    let EntryName (t, g) = interp_entry_name static up_level (String.sub s 0 (l-9)) "" in
+    EntryName (ListArgType t, Alist0sep (g,sep))
   else if l > 4 && coincide s "_opt" (l-4) then
-    let t, g = interp_entry_name static up_level (String.sub s 0 (l-4)) "" in
-    OptArgType t, Aopt g
+    let EntryName (t, g) = interp_entry_name static up_level (String.sub s 0 (l-4)) "" in
+    EntryName (OptArgType t, Aopt g)
   else if l > 5 && coincide s "_mods" (l-5) then
-    let t, g = interp_entry_name static up_level (String.sub s 0 (l-1)) "" in
-    ListArgType t, Amodifiers g
+    let EntryName (t, g) = interp_entry_name static up_level (String.sub s 0 (l-1)) "" in
+    EntryName (ListArgType t, Amodifiers g)
   else
     let s = match s with "hyp" -> "var" | _ -> s in
     let check_lvl n = match up_level with
@@ -805,7 +807,7 @@ let rec interp_entry_name static up_level s sep =
       match t with
 	| Some t -> t
 	| None -> ExtraArgType s in
-    t, se
+    EntryName (t, se)
 
 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 6e9cf263f2..cdffbcba50 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -264,28 +264,30 @@ val symbol_of_constr_prod_entry_key : gram_assoc option ->
    dynamically interpreted as entries for the Coq level extensions
 *)
 
-type prod_entry_key =
-  | Alist1 of prod_entry_key
-  | Alist1sep of prod_entry_key * string
-  | Alist0 of prod_entry_key
-  | Alist0sep of prod_entry_key * string
-  | Aopt of prod_entry_key
-  | Amodifiers of prod_entry_key
-  | Aself
-  | Anext
-  | Atactic of int
-  | Agram of string
-  | Aentry of string * string
+type ('self, _) entry_key =
+| Alist1 : ('self, 'a) entry_key -> ('self, 'a list) entry_key
+| Alist1sep : ('self, 'a) entry_key * string -> ('self, 'a list) entry_key
+| Alist0 : ('self, 'a) entry_key -> ('self, 'a list) entry_key
+| Alist0sep : ('self, 'a) entry_key * string -> ('self, 'a list) entry_key
+| Aopt : ('self, 'a) entry_key -> ('self, 'a option) entry_key
+| Amodifiers : ('self, 'a) entry_key -> ('self, 'a list) entry_key
+| Aself : ('self, 'self) entry_key
+| Anext : ('self, 'self) entry_key
+| Atactic : int -> ('self, raw_tactic_expr) entry_key
+| Agram : string -> ('self, 'a) entry_key
+| Aentry : string * string -> ('self, 'a) entry_key
 
 (** Binding general entry keys to symbols *)
 
 val symbol_of_prod_entry_key :
-  prod_entry_key -> Gram.symbol
+  ('self, 'a) entry_key -> Gram.symbol
+
+type entry_name = EntryName : entry_type * ('self, 'a) entry_key -> entry_name
 
 (** Interpret entry names of the form "ne_constr_list" as entry keys   *)
 
 val interp_entry_name : bool (** true to fail on unknown entry *) ->
-  int option -> string -> string -> entry_type * prod_entry_key
+  int option -> string -> string -> 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 9864182a07..780a8f111c 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -49,7 +49,7 @@ let interp_prod_item lev = function
   | TacTerm s -> GramTerminal s
   | TacNonTerm (loc, nt, po) ->
       let sep = match po with Some (_,sep) -> sep | _ -> "" in
-      let (etyp, e) = interp_entry_name true (Some lev) nt sep in
+      let EntryName (etyp, e) = interp_entry_name true (Some lev) nt sep in
       GramNonTerminal (loc, etyp, e, Option.map fst po)
 
 let make_terminal_status = function