From f2983cec3544473b18ebc4d4e3a20b941decd196 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 10 May 2016 19:46:39 +0200 Subject: Delimiting the use of unsafe code in Pcoq. --- parsing/pcoq.ml | 133 ++++++++++++++++++++++---------------------------------- 1 file changed, 52 insertions(+), 81 deletions(-) (limited to 'parsing/pcoq.ml') diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 305cd4f80..631c5325d 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -41,26 +41,6 @@ let camlp4_verbosity silent f x = let camlp4_verbose f x = camlp4_verbosity (Flags.is_verbose ()) f x - -(** [grammar_object] is the superclass of all grammar entries *) - -module type Gramobj = -sig - type grammar_object - val weaken_entry : 'a G.entry -> grammar_object G.entry -end - -module Gramobj : Gramobj = -struct - type grammar_object = Obj.t - let weaken_entry e = Obj.magic e -end - -(** Grammar entries with associated types *) - -type grammar_object = Gramobj.grammar_object -let weaken_entry x = Gramobj.weaken_entry x - (** Grammar extensions *) (** NB: [extend_statment = @@ -72,20 +52,68 @@ let weaken_entry x = Gramobj.weaken_entry x In [single_extend_statement], first two parameters are name and assoc iff a level is created *) +(** Binding general entry keys to symbol *) + +let rec of_coq_action : type a r. (r, a, Loc.t -> r) Extend.rule -> a -> G.action = function +| Stop -> fun f -> G.action (fun loc -> f (to_coqloc loc)) +| Next (r, _) -> fun f -> G.action (fun x -> of_coq_action r (f x)) + +let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> _ = function + | Atoken t -> Symbols.stoken t + | Alist1 s -> Symbols.slist1 (symbol_of_prod_entry_key s) + | Alist1sep (s,sep) -> + Symbols.slist1sep (symbol_of_prod_entry_key s, symbol_of_prod_entry_key sep) + | Alist0 s -> Symbols.slist0 (symbol_of_prod_entry_key s) + | Alist0sep (s,sep) -> + Symbols.slist0sep (symbol_of_prod_entry_key s, symbol_of_prod_entry_key sep) + | Aopt s -> Symbols.sopt (symbol_of_prod_entry_key s) + | Aself -> Symbols.sself + | Anext -> Symbols.snext + | Aentry e -> + Symbols.snterm (G.Entry.obj e) + | Aentryl (e, n) -> + Symbols.snterml (G.Entry.obj e, string_of_int n) + | Arules rs -> + G.srules' (List.map symbol_of_rules rs) + +and symbol_of_rule : type s a r. (s, a, r) Extend.rule -> _ = function +| Stop -> fun accu -> accu +| Next (r, s) -> fun accu -> symbol_of_rule r (symbol_of_prod_entry_key s :: accu) + +and symbol_of_rules : type a. a Extend.rules -> _ = function +| Rules (r, act) -> + let symb = symbol_of_rule r.norec_rule [] in + let act = of_coq_action r.norec_rule act in + (symb, act) + +let of_coq_production_rule : type a. a Extend.production_rule -> _ = function +| Rule (toks, act) -> (symbol_of_rule toks [], of_coq_action toks act) + +let of_coq_single_extend_statement (lvl, assoc, rule) = + (lvl, Option.map of_coq_assoc assoc, List.map of_coq_production_rule rule) + +let of_coq_extend_statement (pos, st) = + (Option.map of_coq_position pos, List.map of_coq_single_extend_statement st) + (** Type of reinitialization data *) type gram_reinit = gram_assoc * gram_position type ext_kind = - | ByGrammar of - grammar_object G.entry + | ByGrammar : + 'a G.entry * gram_reinit option (** for reinitialization if ever needed *) - * G.extend_statment + * 'a Extend.extend_statment -> ext_kind | ByEXTEND of (unit -> unit) * (unit -> unit) (** The list of extensions *) let camlp4_state = ref [] +let grammar_extend e reinit ext = + camlp4_state := ByGrammar (e,reinit,ext) :: !camlp4_state; + let ext = of_coq_extend_statement ext in + camlp4_verbose (maybe_uncurry (G.extend e)) ext + (** Deletion *) let grammar_delete e reinit (pos,rls) = @@ -130,14 +158,6 @@ module Gram = G.delete_rule e pil end -(** This extension command is used by the Grammar constr *) - -let unsafe_grammar_extend e reinit (pos, st) = - let map_s (lvl, assoc, rule) = (lvl, Option.map of_coq_assoc assoc, rule) in - let ext = (Option.map of_coq_position pos, List.map map_s st) in - camlp4_state := ByGrammar (weaken_entry e,reinit,ext) :: !camlp4_state; - camlp4_verbose (maybe_uncurry (G.extend e)) ext - (** Remove extensions [n] is the number of extended entries (not the number of Grammar commands!) @@ -148,7 +168,7 @@ let rec remove_grammars n = (match !camlp4_state with | [] -> anomaly ~label:"Pcoq.remove_grammars" (Pp.str "too many rules to remove") | ByGrammar(g,reinit,ext)::t -> - grammar_delete g reinit ext; + grammar_delete g reinit (of_coq_extend_statement ext); camlp4_state := t; remove_grammars (n-1) | ByEXTEND (undo,redo)::t -> @@ -519,55 +539,6 @@ let synchronize_level_positions () = let lev = top !level_stack in level_stack := lev :: !level_stack -(** Binding general entry keys to symbol *) - -let rec of_coq_action : type a r. (r, a, Loc.t -> r) Extend.rule -> a -> Gram.action = function -| Stop -> fun f -> Gram.action (fun loc -> f (to_coqloc loc)) -| Next (r, _) -> fun f -> Gram.action (fun x -> of_coq_action r (f x)) - -let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> _ = function - | Atoken t -> Symbols.stoken t - | Alist1 s -> Symbols.slist1 (symbol_of_prod_entry_key s) - | Alist1sep (s,sep) -> - Symbols.slist1sep (symbol_of_prod_entry_key s, symbol_of_prod_entry_key sep) - | Alist0 s -> Symbols.slist0 (symbol_of_prod_entry_key s) - | Alist0sep (s,sep) -> - Symbols.slist0sep (symbol_of_prod_entry_key s, symbol_of_prod_entry_key sep) - | Aopt s -> Symbols.sopt (symbol_of_prod_entry_key s) - | Aself -> Symbols.sself - | Anext -> Symbols.snext - | Aentry e -> - Symbols.snterm (Gram.Entry.obj (weaken_entry e)) - | Aentryl (e, n) -> - Symbols.snterml (Gram.Entry.obj (weaken_entry e), string_of_int n) - | Arules rs -> - Gram.srules' (List.map symbol_of_rules rs) - -and symbol_of_rule : type s a r. (s, a, r) Extend.rule -> _ = function -| Stop -> fun accu -> accu -| Next (r, s) -> fun accu -> symbol_of_rule r (symbol_of_prod_entry_key s :: accu) - -and symbol_of_rules : type a. a Extend.rules -> _ = function -| Rules (r, act) -> - let symb = symbol_of_rule r.norec_rule [] in - let act = of_coq_action r.norec_rule act in - (symb, act) - -let of_coq_production_rule : type a. a Extend.production_rule -> _ = function -| Rule (toks, act) -> (symbol_of_rule toks [], of_coq_action toks act) - -let of_coq_single_extend_statement (lvl, assoc, rule) = - (lvl, assoc, List.map of_coq_production_rule rule) - -let of_coq_extend_statement (pos, st) = - (pos, List.map of_coq_single_extend_statement st) - -let grammar_extend e reinit ext = - let ext = of_coq_extend_statement ext in - unsafe_grammar_extend e reinit ext - -let list_entry_names () = [] - let epsilon_value f e = let r = Rule (Next (Stop, e), fun x _ -> f x) in let ext = of_coq_extend_statement (None, [None, None, [r]]) in -- cgit v1.2.3