From 29f26d380177495a224c3b94d3309a3d23693d8f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 17 Mar 2016 11:01:32 +0100 Subject: Reducing the number of modules linked in grammar.cma. --- grammar/argextend.ml4 | 15 ++++++--------- grammar/grammar.mllib | 5 ----- grammar/q_util.ml4 | 4 ++-- grammar/q_util.mli | 4 ++-- grammar/tacextend.ml4 | 7 ++----- grammar/vernacextend.ml4 | 7 +++---- 6 files changed, 15 insertions(+), 27 deletions(-) (limited to 'grammar') diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index 65dc237bb..be4097f13 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -82,21 +82,19 @@ let statically_known_possibly_empty s (prods,_) = prods let possibly_empty_subentries loc (prods,act) = - let bind_name id v e = - let s = Names.Id.to_string id in + let bind_name s v e = <:expr< let $lid:s$ = $v$ in $e$ >> in let rec aux = function | [] -> <:expr< let loc = $default_loc$ in let _ = loc in $act$ >> - | ExtNonTerminal(_, e, id) :: tl when is_possibly_empty e -> - bind_name id (get_empty_entry e) (aux tl) - | ExtNonTerminal(t, _, id) :: tl -> + | ExtNonTerminal(_, e, s) :: tl when is_possibly_empty e -> + bind_name s (get_empty_entry e) (aux tl) + | ExtNonTerminal(t, _, s) :: tl -> let t = match t with | ExtraArgType _ as t -> t | _ -> assert false in (* We check at runtime if extraarg s parses "epsilon" *) - let s = Names.Id.to_string id in <:expr< let $lid:s$ = match Genarg.default_empty_value $make_wit loc t$ with [ None -> raise Exit | Some v -> v ] in $aux tl$ >> @@ -130,7 +128,6 @@ let make_act loc act pil = let rec make = function | [] -> <:expr< (fun loc -> $act$) >> | ExtNonTerminal (t, _, p) :: tl -> - let p = Names.Id.to_string p in <:expr< (fun $lid:p$ -> let _ = Genarg.in_gen $make_rawwit loc t$ $lid:p$ in $make tl$) @@ -312,10 +309,10 @@ EXTEND genarg: [ [ e = LIDENT; "("; s = LIDENT; ")" -> let e = parse_user_entry e "" in - ExtNonTerminal (type_of_user_symbol e, e, Names.Id.of_string s) + ExtNonTerminal (type_of_user_symbol e, e, s) | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> let e = parse_user_entry e sep in - ExtNonTerminal (type_of_user_symbol e, e, Names.Id.of_string s) + ExtNonTerminal (type_of_user_symbol e, e, s) | s = STRING -> if String.length s > 0 && Util.is_letter s.[0] then Lexer.add_keyword s; diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib index 296d32dc0..6a265bf4a 100644 --- a/grammar/grammar.mllib +++ b/grammar/grammar.mllib @@ -2,7 +2,6 @@ Coq_config Hook Terminal -Canary Hashset Hashcons CSet @@ -29,14 +28,11 @@ CStack Util Ppstyle Errors -Predicate Segmenttree Unicodetable Unicode Genarg -Names - Stdarg Constrarg @@ -47,7 +43,6 @@ Entry Pcoq Q_util -Egramml Argextend Tacextend Vernacextend diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4 index c6e2e9966..f013e323e 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 * Names.Id.t +| ExtNonTerminal of Genarg.argument_type * Extend.user_symbol * string let mlexpr_of_list f l = List.fold_right @@ -55,7 +55,7 @@ let mlexpr_of_option f = function | Some e -> <:expr< Some $f e$ >> let mlexpr_of_ident id = - <:expr< Names.Id.of_string $str:Names.Id.to_string id$ >> + <:expr< Names.Id.of_string $str:id$ >> let mlexpr_of_token = function | Tok.KEYWORD s -> <:expr< Tok.KEYWORD $mlexpr_of_string s$ >> diff --git a/grammar/q_util.mli b/grammar/q_util.mli index d0e0dab22..90fe1645f 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 * Names.Id.t +| ExtNonTerminal of Genarg.argument_type * Extend.user_symbol * string val mlexpr_of_list : ('a -> MLast.expr) -> 'a list -> MLast.expr @@ -34,7 +34,7 @@ val mlexpr_of_string : string -> MLast.expr val mlexpr_of_option : ('a -> MLast.expr) -> 'a option -> MLast.expr -val mlexpr_of_ident : Names.Id.t -> MLast.expr +val mlexpr_of_ident : string -> MLast.expr val mlexpr_of_prod_entry_key : Extend.user_symbol -> MLast.expr diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index 10afcdd21..c35fa00d2 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -27,7 +27,6 @@ let plugin_name = <:expr< __coq_plugin_name >> let rec make_patt = function | [] -> <:patt< [] >> | ExtNonTerminal (_, _, p) :: l -> - let p = Names.Id.to_string p in <:patt< [ $lid:p$ :: $make_patt l$ ] >> | _::l -> make_patt l @@ -43,7 +42,6 @@ let rec mlexpr_of_argtype loc = function let rec make_when loc = function | [] -> <:expr< True >> | ExtNonTerminal (t, _, p) :: l -> - let p = Names.Id.to_string p in let l = make_when loc l in let t = mlexpr_of_argtype loc t in <:expr< Genarg.argument_type_eq (Genarg.genarg_tag $lid:p$) $t$ && $l$ >> @@ -52,7 +50,6 @@ let rec make_when loc = function let rec make_let raw e = function | [] -> <:expr< fun $lid:"ist"$ -> $e$ >> | ExtNonTerminal (t, _, p) :: l -> - let p = Names.Id.to_string p in let loc = MLast.loc_of_expr e in let e = make_let raw e l in let v = @@ -198,10 +195,10 @@ EXTEND tacargs: [ [ e = LIDENT; "("; s = LIDENT; ")" -> let e = parse_user_entry e "" in - ExtNonTerminal (type_of_user_symbol e, e, Names.Id.of_string s) + ExtNonTerminal (type_of_user_symbol e, e, s) | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> let e = parse_user_entry e sep in - ExtNonTerminal (type_of_user_symbol e, e, Names.Id.of_string s) + ExtNonTerminal (type_of_user_symbol e, e, s) | s = STRING -> if String.is_empty s then Errors.user_err_loc (!@loc,"",Pp.str "Empty terminal."); ExtTerminal s diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4 index 57079fccd..3bb1e0907 100644 --- a/grammar/vernacextend.ml4 +++ b/grammar/vernacextend.ml4 @@ -35,7 +35,6 @@ type rule = { let rec make_let e = function | [] -> e | ExtNonTerminal (t, _, p) :: l -> - let p = Names.Id.to_string p 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$ >> @@ -49,7 +48,7 @@ let make_clause { r_patt = pt; r_branch = e; } = (* To avoid warnings *) let mk_ignore c pt = let names = CList.map_filter (function - | ExtNonTerminal (_, _, p) -> Some (Names.Id.to_string p) + | ExtNonTerminal (_, _, p) -> Some p | _ -> None) pt in let fold accu id = <:expr< let _ = $lid:id$ in $accu$ >> in let names = List.fold_left fold <:expr< () >> names in @@ -181,10 +180,10 @@ EXTEND args: [ [ e = LIDENT; "("; s = LIDENT; ")" -> let e = parse_user_entry e "" in - ExtNonTerminal (type_of_user_symbol e, e, Names.Id.of_string s) + ExtNonTerminal (type_of_user_symbol e, e, s) | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> let e = parse_user_entry e sep in - ExtNonTerminal (type_of_user_symbol e, e, Names.Id.of_string s) + ExtNonTerminal (type_of_user_symbol e, e, s) | s = STRING -> ExtTerminal s ] ] -- cgit v1.2.3