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

5 files changed, 24 insertions, 15 deletions

diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index fe0959ddb..7c20ff18e 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 18b1ccd3b..b1eabdd98 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 7393a0d58..d01fb1e9a 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 2e725b46c..70151cef1 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 03061d8bd..d99af6a33 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