From f329e1e63eb29958c4cc0d7bddfdb84a754351d2 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 19 Mar 2016 17:55:15 +0100 Subject: Do not keep the argument type in ExtNonTerminal. --- grammar/argextend.ml4 | 10 +++++----- grammar/q_util.ml4 | 2 +- grammar/q_util.mli | 2 +- grammar/tacextend.ml4 | 16 +++++++++------- grammar/vernacextend.ml4 | 9 +++++---- 5 files changed, 21 insertions(+), 18 deletions(-) (limited to 'grammar') diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index 801229bcb..a38f57cdc 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -32,14 +32,14 @@ let make_topwit loc arg = <:expr< Genarg.topwit $make_wit loc arg$ >> let make_act loc act pil = let rec make = function | [] -> <:expr< (fun loc -> $act$) >> - | ExtNonTerminal (_, _, p) :: tl -> <:expr< (fun $lid:p$ -> $make tl$) >> + | ExtNonTerminal (_, p) :: tl -> <:expr< (fun $lid:p$ -> $make tl$) >> | ExtTerminal _ :: tl -> <:expr< (fun _ -> $make tl$) >> in make (List.rev pil) let make_prod_item = function | ExtTerminal s -> <:expr< Extend.Atoken (Lexer.terminal $mlexpr_of_string s$) >> - | ExtNonTerminal (_, g, _) -> + | ExtNonTerminal (g, _) -> let base s = <:expr< Pcoq.name_of_entry $lid:s$ >> in mlexpr_of_prod_entry_key base g @@ -55,7 +55,7 @@ let is_ident x = function | _ -> false let make_extend loc s cl wit = match cl with -| [[ExtNonTerminal (_, Uentry e, id)], act] when is_ident id act -> +| [[ExtNonTerminal (Uentry e, id)], act] when is_ident id act -> (** Special handling of identity arguments by not redeclaring an entry *) <:str_item< value $lid:s$ = @@ -223,10 +223,10 @@ EXTEND genarg: [ [ e = LIDENT; "("; s = LIDENT; ")" -> let e = parse_user_entry e "" in - ExtNonTerminal (type_of_user_symbol e, e, s) + ExtNonTerminal (e, s) | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> let e = parse_user_entry e sep in - ExtNonTerminal (type_of_user_symbol e, e, s) + ExtNonTerminal (e, s) | s = STRING -> ExtTerminal s ] ] ; diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4 index bde1e7651..56deb61f3 100644 --- a/grammar/q_util.ml4 +++ b/grammar/q_util.ml4 @@ -13,7 +13,7 @@ open Compat type extend_token = | ExtTerminal of string -| ExtNonTerminal of Genarg.argument_type * Extend.user_symbol * string +| ExtNonTerminal of Extend.user_symbol * string let mlexpr_of_list f l = List.fold_right diff --git a/grammar/q_util.mli b/grammar/q_util.mli index 5f292baf3..c84e9d140 100644 --- a/grammar/q_util.mli +++ b/grammar/q_util.mli @@ -10,7 +10,7 @@ open Compat (* necessary for camlp4 *) type extend_token = | ExtTerminal of string -| ExtNonTerminal of Genarg.argument_type * Extend.user_symbol * string +| ExtNonTerminal of Extend.user_symbol * string val mlexpr_of_list : ('a -> MLast.expr) -> 'a list -> MLast.expr diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index a34b880ae..51c382b3b 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -20,13 +20,14 @@ let plugin_name = <:expr< __coq_plugin_name >> let rec make_patt = function | [] -> <:patt< [] >> - | ExtNonTerminal (_, _, p) :: l -> + | ExtNonTerminal (_, p) :: l -> <:patt< [ $lid:p$ :: $make_patt l$ ] >> | _::l -> make_patt l let rec make_let raw e = function | [] -> <:expr< fun $lid:"ist"$ -> $e$ >> - | ExtNonTerminal (t, _, p) :: l -> + | ExtNonTerminal (g, p) :: l -> + let t = type_of_user_symbol g in let loc = MLast.loc_of_expr e in let e = make_let raw e l in let v = @@ -46,7 +47,8 @@ let make_fun_clauses loc s l = let make_prod_item = function | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >> - | ExtNonTerminal (nt, g, id) -> + | ExtNonTerminal (g, id) -> + let nt = type_of_user_symbol g in let base s = <:expr< Pcoq.name_of_entry (Pcoq.genarg_grammar $mk_extraarg loc s$) >> in <:expr< Egramml.GramNonTerminal $default_loc$ $make_rawwit loc nt$ $mlexpr_of_prod_entry_key base g$ >> @@ -66,11 +68,11 @@ let make_printing_rule r = mlexpr_of_list make_one_printing_rule r (** Special treatment of constr entries *) let is_constr_gram = function | ExtTerminal _ -> false -| ExtNonTerminal (_, Extend.Uentry "constr", _) -> true +| ExtNonTerminal (Extend.Uentry "constr", _) -> true | _ -> false let make_var = function - | ExtNonTerminal (_, _, p) -> Some p + | ExtNonTerminal (_, p) -> Some p | _ -> assert false let declare_tactic loc s c cl = match cl with @@ -158,10 +160,10 @@ EXTEND tacargs: [ [ e = LIDENT; "("; s = LIDENT; ")" -> let e = parse_user_entry e "" in - ExtNonTerminal (type_of_user_symbol e, e, s) + ExtNonTerminal (e, s) | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> let e = parse_user_entry e sep in - ExtNonTerminal (type_of_user_symbol e, e, s) + ExtNonTerminal (e, s) | s = STRING -> let () = if s = "" then failwith "Empty terminal." in ExtTerminal s diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4 index 40e327c37..aedaead71 100644 --- a/grammar/vernacextend.ml4 +++ b/grammar/vernacextend.ml4 @@ -30,7 +30,8 @@ type rule = { let rec make_let e = function | [] -> e - | ExtNonTerminal (t, _, p) :: l -> + | ExtNonTerminal (g, p) :: l -> + let t = type_of_user_symbol g in let loc = MLast.loc_of_expr e in let e = make_let e l in <:expr< let $lid:p$ = Genarg.out_gen $make_rawwit loc t$ $lid:p$ in $e$ >> @@ -44,7 +45,7 @@ let make_clause { r_patt = pt; r_branch = e; } = (* To avoid warnings *) let mk_ignore c pt = let fold accu = function - | ExtNonTerminal (_, _, p) -> p :: accu + | ExtNonTerminal (_, p) -> p :: accu | _ -> accu in let names = List.fold_left fold [] pt in @@ -179,10 +180,10 @@ EXTEND args: [ [ e = LIDENT; "("; s = LIDENT; ")" -> let e = parse_user_entry e "" in - ExtNonTerminal (type_of_user_symbol e, e, s) + ExtNonTerminal (e, s) | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> let e = parse_user_entry e sep in - ExtNonTerminal (type_of_user_symbol e, e, s) + ExtNonTerminal (e, s) | s = STRING -> ExtTerminal s ] ] -- cgit v1.2.3