From 73c3dddc94dda003b1bb854d3b6ca9d15474e299 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 27 Oct 2015 10:28:23 +0100 Subject: Getting rid of most uses of unsafe_grammar_extend. --- parsing/egramcoq.ml | 22 +++++++++------------- parsing/egramml.ml | 27 ++------------------------- parsing/egramml.mli | 4 ++-- 3 files changed, 13 insertions(+), 40 deletions(-) diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 14fe15e89..84736f8ab 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -167,10 +167,9 @@ let rec make_constr_prod_item assoc from forpat = function [] let prepare_empty_levels forpat (pos,p4assoc,name,reinit) = - let entry = - if forpat then weaken_entry Constr.pattern - else weaken_entry Constr.operconstr in - unsafe_grammar_extend entry reinit (pos,[(name, p4assoc, [])]) + let empty = (pos, [(name, p4assoc, [])]) in + if forpat then grammar_extend Constr.pattern reinit empty + else grammar_extend Constr.operconstr reinit empty let pure_sublevels level symbs = let filter s = @@ -189,9 +188,6 @@ let extend_constr (entry,level) (n,assoc) mkact forpat rules = let symbs = make_constr_prod_item assoc n forpat pt in let pure_sublevels = pure_sublevels level symbs in let needed_levels = register_empty_levels forpat pure_sublevels in - let map_level (pos, ass1, name, ass2) = - (Option.map of_coq_position pos, Option.map of_coq_assoc ass1, name, ass2) in - let needed_levels = List.map map_level needed_levels in let pos,p4assoc,name,reinit = find_position forpat assoc level in let nb_decls = List.length needed_levels + 1 in List.iter (prepare_empty_levels forpat) needed_levels; @@ -233,11 +229,11 @@ let extend_constr_notation ng = let get_tactic_entry n = if Int.equal n 0 then - weaken_entry Tactic.simple_tactic, None + Tactic.simple_tactic, None else if Int.equal n 5 then - weaken_entry Tactic.binder_tactic, None + Tactic.binder_tactic, None else if 1<=n && n<5 then - weaken_entry Tactic.tactic_expr, Some (Extend.Level (string_of_int n)) + Tactic.tactic_expr, Some (Extend.Level (string_of_int n)) else error ("Invalid Tactic Notation level: "^(string_of_int n)^".") @@ -257,7 +253,7 @@ type all_grammar_command = (** ML Tactic grammar extensions *) let add_ml_tactic_entry name prods = - let entry = weaken_entry Tactic.simple_tactic in + let entry = Tactic.simple_tactic in let mkact i loc l : raw_tactic_expr = let open Tacexpr in let entry = { mltac_name = name; mltac_index = i } in @@ -265,7 +261,7 @@ let add_ml_tactic_entry name prods = in let rules = List.map_i (fun i p -> make_rule (mkact i) p) 0 prods in synchronize_level_positions (); - unsafe_grammar_extend entry None (None ,[(None, None, List.rev rules)]); + grammar_extend entry None (None, [(None, None, List.rev rules)]); 1 (* Declaration of the tactic grammar rule *) @@ -285,7 +281,7 @@ let add_tactic_entry kn tg = in let rules = make_rule mkact tg.tacgram_prods in synchronize_level_positions (); - unsafe_grammar_extend entry None (Option.map of_coq_position pos,[(None, None, List.rev [rules])]); + grammar_extend entry None (pos, [(None, None, List.rev [rules])]); 1 let (grammar_state : (int * all_grammar_command) list ref) = ref [] diff --git a/parsing/egramml.ml b/parsing/egramml.ml index 96c1566c4..7a66b24f3 100644 --- a/parsing/egramml.ml +++ b/parsing/egramml.ml @@ -13,19 +13,6 @@ open Pcoq open Genarg open Vernacexpr -(** Making generic actions in type generic_argument *) - -let make_generic_action - (f:Loc.t -> ('b * raw_generic_argument) list -> 'a) pil = - let rec make env = function - | [] -> - Gram.action (fun loc -> f (to_coqloc loc) env) - | None :: tl -> (* parse a non-binding item *) - Gram.action (fun _ -> make env tl) - | Some (p, t) :: tl -> (* non-terminal *) - Gram.action (fun v -> make ((p, Unsafe.inj t v) :: env) tl) in - make [] (List.rev pil) - (** Grammar extensions declared at ML level *) type 's grammar_prod_item = @@ -33,16 +20,6 @@ type 's grammar_prod_item = | GramNonTerminal : Loc.t * argument_type * ('s, 'a) entry_key * Id.t option -> 's grammar_prod_item -let make_prod_item = function - | GramTerminal s -> (gram_token_of_string s, None) - | GramNonTerminal (_,t,e,po) -> - (symbol_of_prod_entry_key e, Option.map (fun p -> (p,t)) po) - -let make_rule mkact pt = - let (symbs,ntl) = List.split (List.map make_prod_item pt) in - let act = make_generic_action mkact ntl in - (symbs, act) - type 'a ty_arg = Id.t * ('a -> raw_generic_argument) type ('self, _, 'r) ty_rule = @@ -84,7 +61,7 @@ let rec ty_eval : type s a r. (s, a, Loc.t -> s) ty_rule -> s gen_eval -> a = fu let f loc args = f loc ((id, inj x) :: args) in ty_eval rem f -let make_rule' f prod = +let make_rule f prod = let AnyTyRule ty_rule = ty_rule_of_gram (List.rev prod) in let symb = ty_erase ty_rule in let f loc l = f loc (List.rev l) in @@ -107,5 +84,5 @@ let extend_vernac_command_grammar s nt gl = let nt = Option.default Vernac_.command nt in vernac_exts := (s,gl) :: !vernac_exts; let mkact loc l = VernacExtend (s,List.map snd l) in - let rules = [make_rule' mkact gl] in + let rules = [make_rule mkact gl] in grammar_extend nt None (None, [None, None, rules]) diff --git a/parsing/egramml.mli b/parsing/egramml.mli index 182a72086..32646cfaf 100644 --- a/parsing/egramml.mli +++ b/parsing/egramml.mli @@ -27,5 +27,5 @@ val get_extend_vernac_rule : Vernacexpr.extend_name -> vernac_expr grammar_prod_ (** Utility function reused in Egramcoq : *) val make_rule : - (Loc.t -> (Names.Id.t * Genarg.raw_generic_argument) list -> 'b) -> - 's grammar_prod_item list -> Pcoq.Gram.symbol list * Pcoq.Gram.action + (Loc.t -> (Names.Id.t * Genarg.raw_generic_argument) list -> 'a) -> + 'a grammar_prod_item list -> 'a Extend.production_rule -- cgit v1.2.3