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

4 files changed, 56 insertions, 52 deletions

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