Type-safe Egramml.grammar_prod_item.

3 files changed, 35 insertions, 13 deletions

diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index cfabd2688..1fe66b367 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -52,7 +52,15 @@ let make_globwit loc arg = <:expr< Genarg.glbwit $make_wit loc arg$ >>
 let make_topwit loc arg = <:expr< Genarg.topwit $make_wit loc arg$ >>
 
 let has_extraarg l =
-  List.exists (function GramNonTerminal(_,ExtraArgType _,_,_) -> true | _ -> false) l
+  let check = function
+  | GramNonTerminal(_, t, _, _) ->
+    begin match Genarg.unquote t with
+    | ExtraArgType _ -> true
+    | _ -> false
+    end
+  | _ -> false
+  in
+  List.exists check l
 
 let rec is_possibly_empty : type s a. (s, a) entry_key -> bool = function
 | Aopt _ -> true
@@ -74,12 +82,15 @@ let rec get_empty_entry : type s a. (s, a) entry_key -> _ = function
 
 let statically_known_possibly_empty s (prods,_) =
   List.for_all (function
-    | GramNonTerminal(_,ExtraArgType s',_,_) ->
+    | GramNonTerminal(_,t,e,_) ->
+      begin match Genarg.unquote t with
+      | ExtraArgType s' ->
         (* For ExtraArg we don't know (we'll have to test dynamically) *)
         (* unless it is a recursive call *)
         s <> s'
-    | GramNonTerminal(_,_,e,_) ->
+      | _ ->
         is_possibly_empty e
+      end
     | GramTerminal _ ->
         (* This consumes a token for sure *) false)
       prods
@@ -93,7 +104,11 @@ let possibly_empty_subentries loc (prods,act) =
     | [] -> <:expr< let loc = $default_loc$ in let _ = loc in $act$ >>
     | GramNonTerminal(_,_,e,p) :: tl when is_possibly_empty e ->
         bind_name p (get_empty_entry e) (aux tl)
-    | GramNonTerminal(_,(ExtraArgType _ as t),_,p) :: tl ->
+    | GramNonTerminal(_,t,_,p) :: tl ->
+        let t = match Genarg.unquote t with
+        | ExtraArgType _ as t -> t
+        | _ -> assert false
+        in
         (* We check at runtime if extraarg s parses "epsilon" *)
         let s = match p with None -> "_" | Some id -> Names.Id.to_string id in
         <:expr< let $lid:s$ = match Genarg.default_empty_value $make_wit loc t$ with
@@ -129,6 +144,7 @@ let make_act loc act pil =
   let rec make = function
     | [] -> <:expr< Pcoq.Gram.action (fun loc -> ($act$ : 'a)) >>
     | GramNonTerminal (_,t,_,Some p) :: tl ->
+        let t = Genarg.unquote t in
 	let p = Names.Id.to_string p in
 	<:expr<
           Pcoq.Gram.action
@@ -290,10 +306,10 @@ EXTEND
   genarg:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
         let EntryName (t, g) = interp_entry_name false TgAny e "" in
-	GramNonTerminal (!@loc, Genarg.unquote t, g, Some (Names.Id.of_string s))
+	GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s))
       | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
         let EntryName (t, g) = interp_entry_name false TgAny e sep in
-	GramNonTerminal (!@loc, Genarg.unquote t, g, Some (Names.Id.of_string s))
+	GramNonTerminal (!@loc, 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 8c2a45bae..df2209606 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -39,13 +39,14 @@ let rec make_when loc = function
       let p = Names.Id.to_string p in
       let l = make_when loc l in
       let loc = CompatLoc.merge loc' loc in
-      let t = mlexpr_of_argtype loc' t in
+      let t = mlexpr_of_argtype loc' (Genarg.unquote 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$ >>
   | GramNonTerminal(loc,t,_,Some p)::l ->
+      let t = Genarg.unquote t in
       let loc = of_coqloc loc in
       let p = Names.Id.to_string p in
       let loc = CompatLoc.merge loc (MLast.loc_of_expr e) in
@@ -58,7 +59,7 @@ let rec make_let raw e = function
 
 let rec extract_signature = function
   | [] -> []
-  | GramNonTerminal (_,t,_,_) :: l -> t :: extract_signature l
+  | GramNonTerminal (_,t,_,_) :: l -> Genarg.unquote t :: extract_signature l
   | _::l -> extract_signature l
 
 
@@ -83,6 +84,7 @@ let make_fun_clauses loc s l =
 let rec make_args = function
   | [] -> <:expr< [] >>
   | GramNonTerminal(loc,t,_,Some p)::l ->
+      let t = Genarg.unquote t in
       let loc = of_coqloc loc in
       let p = Names.Id.to_string p in
       <:expr< [ Genarg.in_gen $make_topwit loc t$ $lid:p$ :: $make_args l$ ] >>
@@ -97,7 +99,8 @@ let make_prod_item = function
   | GramTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >>
   | GramNonTerminal (loc,nt,g,sopt) ->
       let loc = of_coqloc loc in
-      <:expr< Egramml.GramNonTerminal $default_loc$ $mlexpr_of_argtype loc nt$
+      let nt = Genarg.unquote nt in
+      <:expr< Egramml.GramNonTerminal $default_loc$ $make_rawwit loc nt$
       $mlexpr_of_prod_entry_key g$ $mlexpr_of_option mlexpr_of_ident sopt$ >>
 
 let mlexpr_of_clause cl =
@@ -109,6 +112,7 @@ let rec make_tags loc = function
       let loc' = of_coqloc loc' in
       let l = make_tags loc l in
       let loc = CompatLoc.merge loc' loc in
+      let t = Genarg.unquote t in
       let t = mlexpr_of_argtype loc' t in
       <:expr< [ $t$ :: $l$ ] >>
   | _::l -> make_tags loc l
@@ -124,6 +128,7 @@ let make_printing_rule r = mlexpr_of_list make_one_printing_rule r
 
 let make_empty_check = function
 | GramNonTerminal(_, t, e, _)->
+  let t = Genarg.unquote t in
   let is_extra = match t with ExtraArgType _ -> true | _ -> false in
   if is_possibly_empty e || is_extra then
     (* This possibly parses epsilon *)
@@ -262,10 +267,10 @@ EXTEND
   tacargs:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
         let EntryName (t, g) = interp_entry_name false TgAny e "" in
-        GramNonTerminal (!@loc, Genarg.unquote t, g, Some (Names.Id.of_string s))
+        GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s))
       | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
         let EntryName (t, g) = interp_entry_name false TgAny e sep in
-        GramNonTerminal (!@loc, Genarg.unquote t, g, Some (Names.Id.of_string s))
+        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.");
         GramTerminal s
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4
index 5d4309aba..54638556d 100644
--- a/grammar/vernacextend.ml4
+++ b/grammar/vernacextend.ml4
@@ -35,6 +35,7 @@ type rule = {
 let rec make_let e = function
   | [] -> e
   | GramNonTerminal(loc,t,_,Some p)::l ->
+      let t = Genarg.unquote t in
       let loc = of_coqloc loc in
       let p = Names.Id.to_string p in
       let loc = CompatLoc.merge loc (MLast.loc_of_expr e) in
@@ -182,10 +183,10 @@ EXTEND
   args:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
         let EntryName (t, g) = interp_entry_name false TgAny e "" in
-        GramNonTerminal (!@loc, Genarg.unquote t, g, Some (Names.Id.of_string s))
+        GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s))
       | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
         let EntryName (t, g) = interp_entry_name false TgAny e sep in
-        GramNonTerminal (!@loc, Genarg.unquote t, g, Some (Names.Id.of_string s))
+        GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s))
       | s = STRING ->
         GramTerminal s
     ] ]