From 4950a69874524dd6d79ca6a83b0c36d6dd1a3e45 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 9 May 2016 14:36:36 +0200 Subject: Removing dead code in Compat. --- parsing/compat.ml4 | 71 ++---------------------------------------------------- parsing/pcoq.ml | 21 +++++++++++++--- parsing/pcoq.mli | 5 ++++ 3 files changed, 24 insertions(+), 73 deletions(-) (limited to 'parsing') diff --git a/parsing/compat.ml4 b/parsing/compat.ml4 index 310a44149a..2b67693d28 100644 --- a/parsing/compat.ml4 +++ b/parsing/compat.ml4 @@ -21,17 +21,11 @@ end exception Exc_located = Ploc.Exc IFDEF CAMLP5_6_00 THEN -let ploc_make_loc fname lnb pos bpep = Ploc.make_loc fname lnb pos bpep "" let ploc_file_name = Ploc.file_name ELSE -let ploc_make_loc fname lnb pos bpep = Ploc.make lnb pos bpep let ploc_file_name _ = "" END -let of_coqloc loc = - let (fname, lnb, pos, bp, ep) = Loc.represent loc in - ploc_make_loc fname lnb pos (bp,ep) - let to_coqloc loc = Loc.create (ploc_file_name loc) (Ploc.line_nb loc) (Ploc.bol_pos loc) (Ploc.first_pos loc, Ploc.last_pos loc) @@ -44,10 +38,6 @@ module CompatLoc = Camlp4.PreCast.Loc exception Exc_located = CompatLoc.Exc_located -let of_coqloc loc = - let (fname, lnb, pos, bp, ep) = Loc.represent loc in - CompatLoc.of_tuple (fname, 0, 0, bp, 0, 0, ep, false) - let to_coqloc loc = Loc.create (CompatLoc.file_name loc) (CompatLoc.start_line loc) (CompatLoc.start_bol loc) (CompatLoc.start_off loc, CompatLoc.stop_off loc) @@ -65,6 +55,7 @@ IFDEF CAMLP5 THEN module PcamlSig = struct end module Token = Token +module CompatGramext = struct include Gramext type assoc = g_assoc end ELSE @@ -73,68 +64,10 @@ module Ast = Camlp4.PreCast.Ast module Pcaml = Camlp4.PreCast.Syntax module MLast = Ast module Token = struct exception Error of string end +module CompatGramext = Camlp4.Sig.Grammar END - -(** Grammar auxiliary types *) - -IFDEF CAMLP5 THEN - -let to_coq_assoc = function -| Gramext.RightA -> Extend.RightA -| Gramext.LeftA -> Extend.LeftA -| Gramext.NonA -> Extend.NonA - -let of_coq_assoc = function -| Extend.RightA -> Gramext.RightA -| Extend.LeftA -> Gramext.LeftA -| Extend.NonA -> Gramext.NonA - -let of_coq_position = function -| Extend.First -> Gramext.First -| Extend.Last -> Gramext.Last -| Extend.Before s -> Gramext.Before s -| Extend.After s -> Gramext.After s -| Extend.Level s -> Gramext.Level s - -let to_coq_position = function -| Gramext.First -> Extend.First -| Gramext.Last -> Extend.Last -| Gramext.Before s -> Extend.Before s -| Gramext.After s -> Extend.After s -| Gramext.Level s -> Extend.Level s -| Gramext.Like _ -> assert false (** dont use it, not in camlp4 *) - -ELSE - -let to_coq_assoc = function -| PcamlSig.Grammar.RightA -> Extend.RightA -| PcamlSig.Grammar.LeftA -> Extend.LeftA -| PcamlSig.Grammar.NonA -> Extend.NonA - -let of_coq_assoc = function -| Extend.RightA -> PcamlSig.Grammar.RightA -| Extend.LeftA -> PcamlSig.Grammar.LeftA -| Extend.NonA -> PcamlSig.Grammar.NonA - -let of_coq_position = function -| Extend.First -> PcamlSig.Grammar.First -| Extend.Last -> PcamlSig.Grammar.Last -| Extend.Before s -> PcamlSig.Grammar.Before s -| Extend.After s -> PcamlSig.Grammar.After s -| Extend.Level s -> PcamlSig.Grammar.Level s - -let to_coq_position = function -| PcamlSig.Grammar.First -> Extend.First -| PcamlSig.Grammar.Last -> Extend.Last -| PcamlSig.Grammar.Before s -> Extend.Before s -| PcamlSig.Grammar.After s -> Extend.After s -| PcamlSig.Grammar.Level s -> Extend.Level s - -END - - (** Signature of CLexer *) IFDEF CAMLP5 THEN diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 6dcf76da8c..8c82725893 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -19,6 +19,18 @@ module G = GrammarMake (CLexer) let warning_verbose = Compat.warning_verbose +let of_coq_assoc = function +| Extend.RightA -> CompatGramext.RightA +| Extend.LeftA -> CompatGramext.LeftA +| Extend.NonA -> CompatGramext.NonA + +let of_coq_position = function +| Extend.First -> CompatGramext.First +| Extend.Last -> CompatGramext.Last +| Extend.Before s -> CompatGramext.Before s +| Extend.After s -> CompatGramext.After s +| Extend.Level s -> CompatGramext.Level s + module Symbols = GramextMake(G) let gram_token_of_token = Symbols.stoken @@ -86,8 +98,10 @@ let grammar_delete e reinit (pos,rls) = (List.rev rls); match reinit with | Some (a,ext) -> - let lev = match Option.map Compat.to_coq_position pos with - | Some (Level n) -> n + let a = of_coq_assoc a in + let ext = of_coq_position ext in + let lev = match pos with + | Some (CompatGramext.Level n) -> n | _ -> assert false in maybe_uncurry (G.extend e) (Some ext, [Some lev,Some a,[]]) @@ -135,8 +149,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 -> - let f (a,b) = (of_coq_assoc a, of_coq_position b) in - grammar_delete g (Option.map f reinit) ext; + grammar_delete g reinit ext; camlp4_state := t; remove_grammars (n-1) | ByEXTEND (undo,redo)::t -> diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index d320520015..8c3c299ade 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -288,3 +288,8 @@ val register_empty_levels : bool -> int list -> val remove_levels : int -> unit val level_of_snterml : Gram.symbol -> int + +(** TODO: remove me *) + +val of_coq_position : Extend.gram_position -> Compat.CompatGramext.position +val of_coq_assoc : Extend.gram_assoc -> Compat.CompatGramext.assoc -- cgit v1.2.3 From 9891f2321f13861e3f48ddb28abcd5a77be30791 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 9 May 2016 15:48:11 +0200 Subject: Hardening the obsolete unsafe_grammar_statement API. --- parsing/egramcoq.ml | 3 +-- parsing/pcoq.ml | 17 +++++++++++--- parsing/pcoq.mli | 65 +++++++++++++++++++++++++++-------------------------- 3 files changed, 48 insertions(+), 37 deletions(-) (limited to 'parsing') diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index eff666c9c4..c0a6e5906c 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -189,8 +189,7 @@ let extend_constr (entry,level) (n,assoc) mkact forpat rules = 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; - unsafe_grammar_extend entry reinit (Option.map of_coq_position pos, - [(name, Option.map of_coq_assoc p4assoc, [symbs, mkact pt])]); + unsafe_grammar_extend entry reinit (pos, [(name, p4assoc, [symbs, mkact pt])]); nb_decls) 0 rules type notation_grammar = { diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 8c82725893..70bcf1def3 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -135,7 +135,18 @@ module Gram = (** This extension command is used by the Grammar constr *) -let unsafe_grammar_extend e reinit ext = +type unsafe_single_extend_statment = + string option * + gram_assoc option * + Gram.production_rule list + +type unsafe_extend_statment = + gram_position option * + unsafe_single_extend_statment list + +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 @@ -706,10 +717,10 @@ 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) + (lvl, 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) + (pos, List.map of_coq_single_extend_statement st) let grammar_extend e reinit ext = let ext = of_coq_extend_statement ext in diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 8c3c299ade..3723504149 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -96,28 +96,11 @@ module Gram : Compat.GrammarSig *) -val gram_token_of_token : Tok.t -> Gram.symbol -val gram_token_of_string : string -> Gram.symbol - -(** The superclass of all grammar entries *) -type grammar_object +(** {5 Grammar extension API} *) (** Type of reinitialization data *) type gram_reinit = gram_assoc * gram_position -(** General entry keys *) - -(** This intermediate abstract representation of entries can - both be reified into mlexpr for the ML extensions and - dynamically interpreted as entries for the Coq level extensions -*) - -(** Add one extension at some camlp4 position of some camlp4 entry *) -val unsafe_grammar_extend : - grammar_object Gram.entry -> - gram_reinit option (** for reinitialization if ever needed *) -> - Gram.extend_statment -> unit - val grammar_extend : 'a Gram.entry -> gram_reinit option (** for reinitialization if ever needed *) -> @@ -251,17 +234,6 @@ val main_entry : (Loc.t * vernac_expr) option Gram.entry val get_command_entry : unit -> vernac_expr Gram.entry val set_command_entry : vernac_expr Gram.entry -> unit -(** Mapping formal entries into concrete ones *) - -(** Binding constr entry keys to entries and symbols *) - -val interp_constr_entry_key : bool (** true for cases_pattern *) -> - int -> grammar_object Gram.entry * int option - -val symbol_of_constr_prod_entry_key : gram_assoc option -> - constr_entry_key -> bool -> constr_prod_entry_key -> - Gram.symbol - val name_of_entry : 'a Gram.entry -> 'a Entry.t val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option @@ -287,9 +259,38 @@ val register_empty_levels : bool -> int list -> val remove_levels : int -> unit +(** {5 Unsafe grammar extension API} + +For compatibility purpose only. Do not use in newly written code. + +*) + +val gram_token_of_token : Tok.t -> Gram.symbol +val gram_token_of_string : string -> Gram.symbol val level_of_snterml : Gram.symbol -> int -(** TODO: remove me *) +(** The superclass of all grammar entries *) +type grammar_object + +(** Binding constr entry keys to entries and symbols *) + +val interp_constr_entry_key : bool (** true for cases_pattern *) -> + int -> grammar_object Gram.entry * int option + +val symbol_of_constr_prod_entry_key : gram_assoc option -> + constr_entry_key -> bool -> constr_prod_entry_key -> + Gram.symbol -val of_coq_position : Extend.gram_position -> Compat.CompatGramext.position -val of_coq_assoc : Extend.gram_assoc -> Compat.CompatGramext.assoc +type unsafe_single_extend_statment = + string option * + gram_assoc option * + Gram.production_rule list + +type unsafe_extend_statment = + gram_position option * + unsafe_single_extend_statment list + +val unsafe_grammar_extend : + grammar_object Gram.entry -> + gram_reinit option (** for reinitialization if ever needed *) -> + unsafe_extend_statment -> unit -- cgit v1.2.3 From 6150d15647afc739329019f7e9de595187ecc282 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 9 May 2016 16:08:50 +0200 Subject: Removing the Entry module now that rules need not be marshalled. --- parsing/entry.ml | 30 ------------------------------ parsing/entry.mli | 23 ----------------------- parsing/parsing.mllib | 1 - parsing/pcoq.ml | 13 ------------- parsing/pcoq.mli | 5 +---- 5 files changed, 1 insertion(+), 71 deletions(-) delete mode 100644 parsing/entry.ml delete mode 100644 parsing/entry.mli (limited to 'parsing') diff --git a/parsing/entry.ml b/parsing/entry.ml deleted file mode 100644 index b7c6c23fa6..0000000000 --- a/parsing/entry.ml +++ /dev/null @@ -1,30 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 'a t -(** Create an entry. They should be synchronized with the entries defined in - {!Pcoq}. *) - -(** {5 Meta-programming} *) - -val repr : 'a t -> string -val unsafe_of_name : string -> 'a t diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib index b052b6ee6d..0e1c79c91b 100644 --- a/parsing/parsing.mllib +++ b/parsing/parsing.mllib @@ -1,7 +1,6 @@ Tok Compat CLexer -Entry Pcoq Egramml Egramcoq diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 70bcf1def3..a7f7ad7bca 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -215,18 +215,9 @@ let get_univ u = (** A table associating grammar to entries *) let gtable : Obj.t Gram.entry String.Map.t ref = ref String.Map.empty -let get_grammar (e : 'a Entry.t) : 'a Gram.entry = - Obj.magic (String.Map.find (Entry.repr e) !gtable) - -let set_grammar (e : 'a Entry.t) (g : 'a Gram.entry) = - assert (not (String.Map.mem (Entry.repr e) !gtable)); - gtable := String.Map.add (Entry.repr e) (Obj.magic g) !gtable - let new_entry u s = let ename = u ^ ":" ^ s in - let entry = Entry.create ename in let e = Gram.entry_create ename in - let () = set_grammar entry e in e let make_gen_entry u s = new_entry u s @@ -689,10 +680,8 @@ let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> _ = function | Aself -> Symbols.sself | Anext -> Symbols.snext | Aentry e -> - let e = get_grammar e in Symbols.snterm (Gram.Entry.obj (weaken_entry e)) | Aentryl (e, n) -> - let e = get_grammar e in Symbols.snterml (Gram.Entry.obj (weaken_entry e), string_of_int n) | Arules rs -> Gram.srules' (symbol_of_rules rs [] (fun x -> I0 x)) @@ -726,8 +715,6 @@ let grammar_extend e reinit ext = let ext = of_coq_extend_statement ext in unsafe_grammar_extend e reinit ext -let name_of_entry e = Entry.unsafe_of_name (Gram.Entry.name e) - let list_entry_names () = [] let epsilon_value f e = diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 3723504149..70eb211067 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -19,7 +19,7 @@ open Genredexpr (** The parser of Coq *) -module Gram : Compat.GrammarSig +module Gram : module type of Compat.GrammarMake(CLexer) (** The parser of Coq is built from three kinds of rule declarations: @@ -128,7 +128,6 @@ val uconstr : gram_universe val utactic : gram_universe val uvernac : gram_universe -val set_grammar : 'a Entry.t -> 'a Gram.entry -> unit val register_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry -> unit val genarg_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry @@ -234,8 +233,6 @@ val main_entry : (Loc.t * vernac_expr) option Gram.entry val get_command_entry : unit -> vernac_expr Gram.entry val set_command_entry : vernac_expr Gram.entry -> unit -val name_of_entry : 'a Gram.entry -> 'a Entry.t - val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option (** Binding general entry keys to symbols *) -- cgit v1.2.3 From 53724bbcce87da0b1a9a71da4e5334d7a893ba49 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 9 May 2016 19:12:24 +0200 Subject: Purer implementation of empty level registering in Pcoq. --- parsing/egramcoq.ml | 21 ++++++++++-------- parsing/pcoq.ml | 64 ++++++++++++++++++++++++++++++++--------------------- parsing/pcoq.mli | 11 +++++---- 3 files changed, 56 insertions(+), 40 deletions(-) (limited to 'parsing') diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index c0a6e5906c..78b9185fbf 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -182,15 +182,18 @@ let pure_sublevels level symbs = List.map_filter filter symbs let extend_constr (entry,level) (n,assoc) mkact forpat rules = - List.fold_left (fun nb pt -> - 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 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; - unsafe_grammar_extend entry reinit (pos, [(name, p4assoc, [symbs, mkact pt])]); - nb_decls) 0 rules + let fold nb pt = + 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 pos,p4assoc,name,reinit = find_position forpat assoc level in + let nb_decls = List.length needed_levels + 1 in + let () = List.iter (prepare_empty_levels forpat) needed_levels in + let rule = (name, p4assoc, [symbs, mkact pt]) in + let () = unsafe_grammar_extend entry reinit (pos, [rule]) in + nb_decls + in + List.fold_left fold 0 rules type notation_grammar = { notgram_level : int; diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index a7f7ad7bca..42eb8724af 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -423,9 +423,6 @@ let default_pattern_levels = 1,Extend.LeftA,false; 0,Extend.RightA,false] -let level_stack = - ref [(default_levels, default_pattern_levels)] - (* At a same level, LeftA takes precedence over RightA and NoneA *) (* In case, several associativity exists for a level, we make two levels, *) (* first LeftA, then RightA and NoneA together *) @@ -453,12 +450,10 @@ let create_pos = function | None -> Extend.First | Some lev -> Extend.After (constr_level lev) -let find_position_gen forpat ensure assoc lev = - let ccurrent,pcurrent as current = List.hd !level_stack in +let find_position_gen current ensure assoc lev = match lev with | None -> - level_stack := current :: !level_stack; - None, None, None, None + current, (None, None, None, None) | Some n -> let after = ref None in let init = ref None in @@ -475,25 +470,24 @@ let find_position_gen forpat ensure assoc lev = | l -> after := q; (n,create_assoc assoc,ensure)::l in try - let updated = - if forpat then (ccurrent, add_level None pcurrent) - else (add_level None ccurrent, pcurrent) in - level_stack := updated:: !level_stack; + let updated = add_level None current in let assoc = create_assoc assoc in begin match !init with | None -> (* Create the entry *) - Some (create_pos !after), Some assoc, Some (constr_level n), None + updated, (Some (create_pos !after), Some assoc, Some (constr_level n), None) | _ -> (* The reinit flag has been updated *) - Some (Extend.Level (constr_level n)), None, None, !init + updated, (Some (Extend.Level (constr_level n)), None, None, !init) end with (* Nothing has changed *) Exit -> - level_stack := current :: !level_stack; (* Just inherit the existing associativity and name (None) *) - Some (Extend.Level (constr_level n)), None, None, None + current, (Some (Extend.Level (constr_level n)), None, None, None) + +let level_stack = + ref [(default_levels, default_pattern_levels)] let remove_levels n = level_stack := List.skipn n !level_stack @@ -502,23 +496,43 @@ let rec list_mem_assoc_triple x = function | [] -> false | (a,b,c) :: l -> Int.equal a x || list_mem_assoc_triple x l +type gram_level = + gram_position option * gram_assoc option * string option * + (** for reinitialization: *) gram_reinit option + +let top = function +| [] -> assert false +| h :: _ -> h + let register_empty_levels forpat levels = - let filter n = - try - let levels = (if forpat then snd else fst) (List.hd !level_stack) in - if not (list_mem_assoc_triple n levels) then - Some (find_position_gen forpat true None (Some n)) - else None - with Failure _ -> None + let rec filter accu = function + | [] -> ([], accu) + | n :: rem -> + let rem, accu = filter accu rem in + let (clev, plev) = top accu in + let levels = if forpat then plev else clev in + if not (list_mem_assoc_triple n levels) then + let nlev, ans = find_position_gen levels true None (Some n) in + let nlev = if forpat then (clev, nlev) else (nlev, plev) in + ans :: rem, nlev :: accu + else rem, accu in - List.map_filter filter levels + let ans, accu = filter !level_stack levels in + let () = level_stack := accu in + ans let find_position forpat assoc level = - find_position_gen forpat false assoc level + let (clev, plev) = top !level_stack in + let levels = if forpat then plev else clev in + let nlev, ans = find_position_gen levels false assoc level in + let nlev = if forpat then (clev, nlev) else (nlev, plev) in + level_stack := nlev :: !level_stack; + ans (* Synchronise the stack of level updates *) let synchronize_level_positions () = - let _ = find_position true None None in () + let lev = top !level_stack in + level_stack := lev :: !level_stack (**********************************************************************) (* Binding constr entry keys to entries *) diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 70eb211067..8d653a179b 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -242,17 +242,16 @@ val list_entry_names : unit -> (string * argument_type) list (** Registering/resetting the level of a constr entry *) +type gram_level = + gram_position option * gram_assoc option * string option * gram_reinit option + val find_position : bool (** true if for creation in pattern entry; false if in constr entry *) -> - Extend.gram_assoc option -> int option -> - Extend.gram_position option * Extend.gram_assoc option * string option * - (** for reinitialization: *) gram_reinit option + Extend.gram_assoc option -> int option -> gram_level val synchronize_level_positions : unit -> unit -val register_empty_levels : bool -> int list -> - (Extend.gram_position option * Extend.gram_assoc option * - string option * gram_reinit option) list +val register_empty_levels : bool -> int list -> gram_level list val remove_levels : int -> unit -- cgit v1.2.3 From 946a3d4a800ae1f459cb67cc15c9e6ec44fb3f94 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 10 May 2016 08:56:15 +0200 Subject: Simpler data structure for Arules token. --- parsing/pcoq.ml | 25 +++++++++---------------- 1 file changed, 9 insertions(+), 16 deletions(-) (limited to 'parsing') diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 42eb8724af..b06362dc38 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -675,12 +675,9 @@ let rec symbol_of_constr_prod_entry_key assoc from forpat typ = (** Binding general entry keys to symbol *) -let tuplify l = - List.fold_left (fun accu x -> Obj.repr (x, accu)) (Obj.repr ()) l - -let rec adj : type a b c. (a, b, Loc.t -> Loc.t * c) adj -> _ = function -| Adj0 -> Obj.magic (fun accu f loc -> f (Obj.repr (to_coqloc loc, tuplify accu))) -| AdjS e -> Obj.magic (fun accu f x -> adj e (x :: accu) f) +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 @@ -697,25 +694,21 @@ let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> _ = function 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' (symbol_of_rules rs [] (fun x -> I0 x)) + | 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 -| Rule0 -> fun accu _ -> accu -| RuleS (r, e, rs) -> fun accu f -> - let symb = symbol_of_rule r [] in - let act = adj e [] f in - symbol_of_rules rs ((symb, act) :: accu) (fun x -> IS (f x)) +| 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 level_of_snterml e = int_of_string (Symbols.snterml_level e) -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 of_coq_production_rule : type a. a Extend.production_rule -> _ = function | Rule (toks, act) -> (symbol_of_rule toks [], of_coq_action toks act) -- cgit v1.2.3 From 61f79019be6082c3ebabd503c322fb2edb05a99a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 10 May 2016 11:11:39 +0200 Subject: AlistNsep token now accepts an arbitrary separator. --- parsing/pcoq.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'parsing') diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index b06362dc38..2790063e67 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -683,10 +683,10 @@ 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, gram_token_of_string 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, gram_token_of_string 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 -- cgit v1.2.3 From 810afe7c16ca2d18ac7fb39b1d3bd1a3db1c1331 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 10 May 2016 09:59:41 +0200 Subject: Type-safe constr notations. This removes the last call to unsafe_grammar_extend, so that all handwritten grammar extensions are now type-safe. Grammars defined by CAMLPX EXTEND are still using the unsafe interface, but as they insert explicit casts they are deemed safe. --- parsing/egramcoq.ml | 413 +++++++++++++++++++++++++++++++++++----------------- parsing/pcoq.ml | 156 -------------------- parsing/pcoq.mli | 36 ----- 3 files changed, 281 insertions(+), 324 deletions(-) (limited to 'parsing') diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 78b9185fbf..6286dab5a5 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Compat open Errors open Util open Pcoq @@ -43,6 +42,159 @@ open Names (**********************************************************************) (** Declare Notations grammar rules *) +(**********************************************************************) +(* Binding constr entry keys to entries *) + +(* Camlp4 levels do not treat NonA: use RightA with a NEXT on the left *) +let camlp4_assoc = function + | Some NonA | Some RightA -> RightA + | None | Some LeftA -> LeftA + +let assoc_eq al ar = match al, ar with +| NonA, NonA +| RightA, RightA +| LeftA, LeftA -> true +| _, _ -> false + +(* [adjust_level assoc from prod] where [assoc] and [from] are the name + and associativity of the level where to add the rule; the meaning of + the result is + + None = SELF + Some None = NEXT + Some (Some (n,cur)) = constr LEVEL n + s.t. if [cur] is set then [n] is the same as the [from] level *) +let adjust_level assoc from = function +(* Associativity is None means force the level *) + | (NumLevel n,BorderProd (_,None)) -> Some (Some (n,true)) +(* Compute production name on the right side *) + (* If NonA or LeftA on the right-hand side, set to NEXT *) + | (NumLevel n,BorderProd (Right,Some (NonA|LeftA))) -> + Some None + (* If RightA on the right-hand side, set to the explicit (current) level *) + | (NumLevel n,BorderProd (Right,Some RightA)) -> + Some (Some (n,true)) +(* Compute production name on the left side *) + (* If NonA on the left-hand side, adopt the current assoc ?? *) + | (NumLevel n,BorderProd (Left,Some NonA)) -> None + (* If the expected assoc is the current one, set to SELF *) + | (NumLevel n,BorderProd (Left,Some a)) when assoc_eq a (camlp4_assoc assoc) -> + None + (* Otherwise, force the level, n or n-1, according to expected assoc *) + | (NumLevel n,BorderProd (Left,Some a)) -> + begin match a with + | LeftA -> Some (Some (n, true)) + | _ -> Some None + end + (* None means NEXT *) + | (NextLevel,_) -> Some None +(* Compute production name elsewhere *) + | (NumLevel n,InternalProd) -> + if from = n + 1 then Some None else Some (Some (n, Int.equal n from)) + +type _ target = +| ForConstr : constr_expr target +| ForPattern : cases_pattern_expr target + +type prod_info = production_level * production_position + +type (_, _) entry = +| TTName : ('self, Name.t Loc.located) entry +| TTReference : ('self, reference) entry +| TTBigint : ('self, Bigint.bigint) entry +| TTBinder : bool -> ('self, local_binder list) entry +| TTConstr : prod_info * 'r target -> ('r, 'r) entry +| TTPattern : ('self, cases_pattern_expr) entry +| TTConstrList : prod_info * Tok.t list * 'r target -> ('r, 'r list) entry +| TTBinderListT : ('self, local_binder list) entry +| TTBinderListF : Tok.t list -> ('self, local_binder list list) entry + +type _ any_entry = TTAny : ('s, 'r) entry -> 's any_entry + +(* This computes the name of the level where to add a new rule *) +let interp_constr_entry_key : type r. r target -> int -> r Gram.entry * int option = + fun forpat level -> match forpat with + | ForConstr -> + if level = 200 then Constr.binder_constr, None + else Constr.operconstr, Some level + | ForPattern -> Constr.pattern, Some level + +let compute_entry : type s r. (s, r) entry -> r Gram.entry = function +| TTConstr (_, ForConstr) -> Constr.operconstr +| TTConstr (_, ForPattern) -> Constr.pattern +| TTName -> Prim.name +| TTBinder true -> anomaly (Pp.str "Should occur only as part of BinderList") +| TTBinder false -> Constr.binder +| TTBinderListT -> Constr.open_binders +| TTBinderListF _ -> anomaly (Pp.str "List of entries cannot be registered.") +| TTBigint -> Prim.bigint +| TTReference -> Constr.global +| TTPattern -> Constr.pattern +| TTConstrList _ -> anomaly (Pp.str "List of entries cannot be registered.") + +let is_self from e = match e with +| (NumLevel n, BorderProd (Right, _ (* Some(NonA|LeftA) *))) -> false +| (NumLevel n, BorderProd (Left, _)) -> Int.equal from n +| _ -> false + +let is_binder_level from e = match e with +| (NumLevel 200, (BorderProd (Right, _) | InternalProd)) -> from = 200 +| _ -> false + +let make_sep_rules tkl = + let rec mkrule : Tok.t list -> unit rules = function + | [] -> Rules ({ norec_rule = Stop }, ignore) + | tkn :: rem -> + let Rules ({ norec_rule = r }, f) = mkrule rem in + let r = { norec_rule = Next (r, Atoken tkn) } in + Rules (r, fun _ -> f) + in + let r = mkrule (List.rev tkl) in + Arules [r] + +let rec symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) symbol = fun assoc from typ -> match typ with +| TTConstr (p, forpat) -> + if is_binder_level from p then match forpat with + | ForConstr -> Aentryl (Constr.operconstr, 200) + | ForPattern -> Aentryl (Constr.pattern, 200) + else if is_self from p then Aself + else + let g = compute_entry (TTConstr (p, forpat)) in + let lev = adjust_level assoc from p in + begin match lev with + | None -> Aentry g + | Some None -> Anext + | Some (Some (lev, cur)) -> Aentryl (g, lev) + end +| TTConstrList (typ', [], forpat) -> + let symb = symbol_of_entry assoc from (TTConstr (typ', forpat)) in + Alist1 symb +| TTConstrList (typ', tkl, forpat) -> + let symb = symbol_of_entry assoc from (TTConstr (typ', forpat)) in + Alist1sep (symb, make_sep_rules tkl) +| TTBinderListF [] -> + let symb = symbol_of_entry assoc from (TTBinder false) in + Alist1 (symb) +| TTBinderListF tkl -> + let symb = symbol_of_entry assoc from (TTBinder false) in + Alist1sep (symb, make_sep_rules tkl) +| _ -> + let g = compute_entry typ in + Aentry g + +let interp_entry forpat e = match e with +| ETName -> TTAny TTName +| ETReference -> TTAny TTReference +| ETBigint -> TTAny TTBigint +| ETBinder b -> TTAny (TTBinder b) +| ETConstr p -> TTAny (TTConstr (p, forpat)) +| ETPattern -> TTAny TTPattern +| ETOther _ -> assert false (** not used *) +| ETConstrList (p, tkl) -> TTAny (TTConstrList (p, tkl, forpat)) +| ETBinderList (true, []) -> TTAny TTBinderListT +| ETBinderList (true, _) -> assert false +| ETBinderList (false, tkl) -> TTAny (TTBinderListF tkl) + let constr_expr_of_name (loc,na) = match na with | Anonymous -> CHole (loc,None,Misctypes.IntroAnonymous,None) | Name id -> CRef (Ident (loc,id), None) @@ -58,139 +210,138 @@ type grammar_constr_prod_item = (* tells action rule to make a list of the n previous parsed items; concat with last parsed list if true *) -let make_constr_action - (f : Loc.t -> constr_notation_substitution -> constr_expr) pil = - let rec make (constrs,constrlists,binders as fullsubst) = function - | [] -> - Gram.action (fun (loc:CompatLoc.t) -> f (!@loc) fullsubst) - | (GramConstrTerminal _ | GramConstrNonTerminal (_,None)) :: tl -> - (* parse a non-binding item *) - Gram.action (fun _ -> make fullsubst tl) - | GramConstrNonTerminal (typ, Some _) :: tl -> - (* parse a binding non-terminal *) - (match typ with - | (ETConstr _| ETOther _) -> - Gram.action (fun (v:constr_expr) -> - make (v :: constrs, constrlists, binders) tl) - | ETReference -> - Gram.action (fun (v:reference) -> - make (CRef (v,None) :: constrs, constrlists, binders) tl) - | ETName -> - Gram.action (fun (na:Loc.t * Name.t) -> - make (constr_expr_of_name na :: constrs, constrlists, binders) tl) - | ETBigint -> - Gram.action (fun (v:Bigint.bigint) -> - make (CPrim(Loc.ghost,Numeral v) :: constrs, constrlists, binders) tl) - | ETConstrList (_,n) -> - Gram.action (fun (v:constr_expr list) -> - make (constrs, v::constrlists, binders) tl) - | ETBinder _ | ETBinderList (true,_) -> - Gram.action (fun (v:local_binder list) -> - make (constrs, constrlists, v::binders) tl) - | ETBinderList (false,_) -> - Gram.action (fun (v:local_binder list list) -> - make (constrs, constrlists, List.flatten v::binders) tl) - | ETPattern -> - failwith "Unexpected entry of type cases pattern") - | GramConstrListMark (n,b) :: tl -> - (* Rebuild expansions of ConstrList *) - let heads,constrs = List.chop n constrs in - let constrlists = - if b then (heads@List.hd constrlists)::List.tl constrlists - else heads::constrlists - in make (constrs, constrlists, binders) tl - in - make ([],[],[]) (List.rev pil) - -let check_cases_pattern_env loc (env,envlist,hasbinders) = - if hasbinders then Topconstr.error_invalid_pattern_notation loc - else (env,envlist) - -let make_cases_pattern_action - (f : Loc.t -> cases_pattern_notation_substitution -> cases_pattern_expr) pil = - let rec make (env,envlist,hasbinders as fullenv) = function - | [] -> - Gram.action - (fun (loc:CompatLoc.t) -> - let loc = !@loc in - f loc (check_cases_pattern_env loc fullenv)) - | (GramConstrTerminal _ | GramConstrNonTerminal (_,None)) :: tl -> - (* parse a non-binding item *) - Gram.action (fun _ -> make fullenv tl) - | GramConstrNonTerminal (typ, Some _) :: tl -> - (* parse a binding non-terminal *) - (match typ with - | ETConstr _ -> (* pattern non-terminal *) - Gram.action (fun (v:cases_pattern_expr) -> - make (v::env, envlist, hasbinders) tl) - | ETReference -> - Gram.action (fun (v:reference) -> - make (CPatAtom (Loc.ghost,Some v) :: env, envlist, hasbinders) tl) - | ETName -> - Gram.action (fun (na:Loc.t * Name.t) -> - make (cases_pattern_expr_of_name na :: env, envlist, hasbinders) tl) - | ETBigint -> - Gram.action (fun (v:Bigint.bigint) -> - make (CPatPrim (Loc.ghost,Numeral v) :: env, envlist, hasbinders) tl) - | ETConstrList (_,_) -> - Gram.action (fun (vl:cases_pattern_expr list) -> - make (env, vl :: envlist, hasbinders) tl) - | ETBinder _ | ETBinderList (true,_) -> - Gram.action (fun (v:local_binder list) -> - make (env, envlist, hasbinders) tl) - | ETBinderList (false,_) -> - Gram.action (fun (v:local_binder list list) -> - make (env, envlist, true) tl) - | (ETPattern | ETOther _) -> - anomaly (Pp.str "Unexpected entry of type cases pattern or other")) - | GramConstrListMark (n,b) :: tl -> - (* Rebuild expansions of ConstrList *) - let heads,env = List.chop n env in - if b then - make (env,(heads@List.hd envlist)::List.tl envlist,hasbinders) tl - else - make (env,heads::envlist,hasbinders) tl +type 'r env = { + constrs : 'r list; + constrlists : 'r list list; + binders : (local_binder list * bool) list; +} + +let push_constr subst v = { subst with constrs = v :: subst.constrs } + +let push_item : type s r. s target -> (s, r) entry -> s env -> r -> s env = fun forpat e subst v -> +match e with +| TTConstr _ -> push_constr subst v +| TTName -> + begin match forpat with + | ForConstr -> push_constr subst (constr_expr_of_name v) + | ForPattern -> push_constr subst (cases_pattern_expr_of_name v) + end +| TTBinder _ -> { subst with binders = (v, true) :: subst.binders } +| TTBinderListT -> { subst with binders = (v, true) :: subst.binders } +| TTBinderListF _ -> { subst with binders = (List.flatten v, false) :: subst.binders } +| TTBigint -> + begin match forpat with + | ForConstr -> push_constr subst (CPrim (Loc.ghost, Numeral v)) + | ForPattern -> push_constr subst (CPatPrim (Loc.ghost, Numeral v)) + end +| TTReference -> + begin match forpat with + | ForConstr -> push_constr subst (CRef (v, None)) + | ForPattern -> push_constr subst (CPatAtom (Loc.ghost, Some v)) + end +| TTPattern -> anomaly (Pp.str "Unexpected entry of type cases pattern or other") +| TTConstrList _ -> { subst with constrlists = v :: subst.constrlists } + +type (_, _) ty_symbol = +| TyTerm : Tok.t -> ('s, string) ty_symbol +| TyNonTerm : 's target * ('s, 'a) entry * ('s, 'a) symbol * bool -> ('s, 'a) ty_symbol + +type ('self, _, 'r) ty_rule = +| TyStop : ('self, 'r, 'r) ty_rule +| TyNext : ('self, 'a, 'r) ty_rule * ('self, 'b) ty_symbol -> ('self, 'b -> 'a, 'r) ty_rule +| TyMark : int * bool * ('self, 'a, 'r) ty_rule -> ('self, 'a, 'r) ty_rule + +type 'r gen_eval = Loc.t -> 'r env -> 'r + +let rec ty_eval : type s a. (s, a, Loc.t -> s) ty_rule -> s gen_eval -> s env -> a = function +| TyStop -> + fun f env loc -> f loc env +| TyNext (rem, TyTerm _) -> + fun f env _ -> ty_eval rem f env +| TyNext (rem, TyNonTerm (_, _, _, false)) -> + fun f env _ -> ty_eval rem f env +| TyNext (rem, TyNonTerm (forpat, e, _, true)) -> + fun f env v -> + ty_eval rem f (push_item forpat e env v) +| TyMark (n, b, rem) -> + fun f env -> + let heads, constrs = List.chop n env.constrs in + let constrlists = + if b then (heads @ List.hd env.constrlists) :: List.tl env.constrlists + else heads :: env.constrlists + in + ty_eval rem f { env with constrs; constrlists; } + +let rec ty_erase : type s a r. (s, a, r) ty_rule -> (s, a, r) Extend.rule = function +| TyStop -> Stop +| TyMark (_, _, r) -> ty_erase r +| TyNext (rem, TyTerm tok) -> Next (ty_erase rem, Atoken tok) +| TyNext (rem, TyNonTerm (_, _, s, _)) -> Next (ty_erase rem, s) + +type ('self, 'r) any_ty_rule = +| AnyTyRule : ('self, 'act, Loc.t -> 'r) ty_rule -> ('self, 'r) any_ty_rule + +let make_ty_rule assoc from forpat prods = + let rec make_ty_rule = function + | [] -> AnyTyRule TyStop + | GramConstrTerminal tok :: rem -> + let AnyTyRule r = make_ty_rule rem in + AnyTyRule (TyNext (r, TyTerm tok)) + | GramConstrNonTerminal (e, var) :: rem -> + let AnyTyRule r = make_ty_rule rem in + let TTAny e = interp_entry forpat e in + let s = symbol_of_entry assoc from e in + let bind = match var with None -> false | Some _ -> true in + AnyTyRule (TyNext (r, TyNonTerm (forpat, e, s, bind))) + | GramConstrListMark (n, b) :: rem -> + let AnyTyRule r = make_ty_rule rem in + AnyTyRule (TyMark (n, b, r)) in - make ([],[],false) (List.rev pil) - -let rec make_constr_prod_item assoc from forpat = function - | GramConstrTerminal tok :: l -> - gram_token_of_token tok :: make_constr_prod_item assoc from forpat l - | GramConstrNonTerminal (nt, ovar) :: l -> - symbol_of_constr_prod_entry_key assoc from forpat nt - :: make_constr_prod_item assoc from forpat l - | GramConstrListMark _ :: l -> - make_constr_prod_item assoc from forpat l - | [] -> - [] + make_ty_rule (List.rev prods) + +let target_to_bool : type r. r target -> bool = function +| ForConstr -> false +| ForPattern -> true let prepare_empty_levels forpat (pos,p4assoc,name,reinit) = 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 = - try - let i = level_of_snterml s in - begin match level with - | Some j when Int.equal i j -> None - | _ -> Some i - end - with Failure _ -> None - in - List.map_filter filter symbs - -let extend_constr (entry,level) (n,assoc) mkact forpat rules = +let rec pure_sublevels : type a b c. int option -> (a, b, c) rule -> int list = fun level r -> match r with +| Stop -> [] +| Next (rem, Aentryl (_, i)) -> + let rem = pure_sublevels level rem in + begin match level with + | Some j when Int.equal i j -> rem + | _ -> i :: rem + end +| Next (rem, _) -> pure_sublevels level rem + +let make_act : type r. r target -> _ -> r gen_eval = function +| ForConstr -> fun notation loc env -> + let env = (env.constrs, env.constrlists, List.map fst env.binders) in + CNotation (loc, notation , env) +| ForPattern -> fun notation loc env -> + let invalid = List.exists (fun (_, b) -> not b) env.binders in + let () = if invalid then Topconstr.error_invalid_pattern_notation loc in + let env = (env.constrs, env.constrlists) in + CPatNotation (loc, notation, env, []) + +let extend_constr (entry,level) (n,assoc) forpat notation rules = let fold nb pt = - let symbs = make_constr_prod_item assoc n forpat pt in + let AnyTyRule r = make_ty_rule assoc n forpat pt in + let symbs = ty_erase r in let pure_sublevels = pure_sublevels level symbs in - let needed_levels = register_empty_levels forpat pure_sublevels in - let pos,p4assoc,name,reinit = find_position forpat assoc level in + let isforpat = target_to_bool forpat in + let needed_levels = register_empty_levels isforpat pure_sublevels in + let pos,p4assoc,name,reinit = find_position isforpat assoc level in let nb_decls = List.length needed_levels + 1 in - let () = List.iter (prepare_empty_levels forpat) needed_levels in - let rule = (name, p4assoc, [symbs, mkact pt]) in - let () = unsafe_grammar_extend entry reinit (pos, [rule]) in + let () = List.iter (prepare_empty_levels isforpat) needed_levels in + let empty = { constrs = []; constrlists = []; binders = [] } in + let act = ty_eval r (make_act forpat notation) empty in + let rule = (name, p4assoc, [Rule (symbs, act)]) in + let () = grammar_extend entry reinit (pos, [rule]) in nb_decls in List.fold_left fold 0 rules @@ -205,17 +356,15 @@ type notation_grammar = { let extend_constr_constr_notation ng = let level = ng.notgram_level in - let mkact loc env = CNotation (loc, ng.notgram_notation, env) in - let e = interp_constr_entry_key false level in - let ext = (ETConstr (level, ()), ng.notgram_assoc) in - extend_constr e ext (make_constr_action mkact) false ng.notgram_prods + let e = interp_constr_entry_key ForConstr level in + let ext = (level, ng.notgram_assoc) in + extend_constr e ext ForConstr ng.notgram_notation ng.notgram_prods let extend_constr_pat_notation ng = let level = ng.notgram_level in - let mkact loc env = CPatNotation (loc, ng.notgram_notation, env, []) in - let e = interp_constr_entry_key true level in - let ext = ETConstr (level, ()), ng.notgram_assoc in - extend_constr e ext (make_cases_pattern_action mkact) true ng.notgram_prods + let e = interp_constr_entry_key ForPattern level in + let ext = (level, ng.notgram_assoc) in + extend_constr e ext ForPattern ng.notgram_notation ng.notgram_prods let extend_constr_notation (_, ng) = (* Add the notation in constr *) diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 2790063e67..8fa5da4bd9 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -33,9 +33,6 @@ let of_coq_position = function module Symbols = GramextMake(G) -let gram_token_of_token = Symbols.stoken -let gram_token_of_string s = gram_token_of_token (CLexer.terminal s) - let camlp4_verbosity silent f x = let a = !warning_verbose in warning_verbose := silent; @@ -135,15 +132,6 @@ module Gram = (** This extension command is used by the Grammar constr *) -type unsafe_single_extend_statment = - string option * - gram_assoc option * - Gram.production_rule list - -type unsafe_extend_statment = - gram_position option * - unsafe_single_extend_statment list - 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 @@ -212,9 +200,6 @@ let get_univ u = if Hashtbl.mem utables u then u else raise Not_found -(** A table associating grammar to entries *) -let gtable : Obj.t Gram.entry String.Map.t ref = ref String.Map.empty - let new_entry u s = let ename = u ^ ":" ^ s in let e = Gram.entry_create ename in @@ -534,145 +519,6 @@ let synchronize_level_positions () = let lev = top !level_stack in level_stack := lev :: !level_stack -(**********************************************************************) -(* Binding constr entry keys to entries *) - -(* Camlp4 levels do not treat NonA: use RightA with a NEXT on the left *) -let camlp4_assoc = function - | Some Extend.NonA | Some Extend.RightA -> Extend.RightA - | None | Some Extend.LeftA -> Extend.LeftA - -let assoc_eq al ar = match al, ar with -| Extend.NonA, Extend.NonA -| Extend.RightA, Extend.RightA -| Extend.LeftA, Extend.LeftA -> true -| _, _ -> false - -(* [adjust_level assoc from prod] where [assoc] and [from] are the name - and associativity of the level where to add the rule; the meaning of - the result is - - None = SELF - Some None = NEXT - Some (Some (n,cur)) = constr LEVEL n - s.t. if [cur] is set then [n] is the same as the [from] level *) -let adjust_level assoc from = function -(* Associativity is None means force the level *) - | (NumLevel n,BorderProd (_,None)) -> Some (Some (n,true)) -(* Compute production name on the right side *) - (* If NonA or LeftA on the right-hand side, set to NEXT *) - | (NumLevel n,BorderProd (Right,Some (Extend.NonA|Extend.LeftA))) -> - Some None - (* If RightA on the right-hand side, set to the explicit (current) level *) - | (NumLevel n,BorderProd (Right,Some Extend.RightA)) -> - Some (Some (n,true)) -(* Compute production name on the left side *) - (* If NonA on the left-hand side, adopt the current assoc ?? *) - | (NumLevel n,BorderProd (Left,Some Extend.NonA)) -> None - (* If the expected assoc is the current one, set to SELF *) - | (NumLevel n,BorderProd (Left,Some a)) when assoc_eq a (camlp4_assoc assoc) -> - None - (* Otherwise, force the level, n or n-1, according to expected assoc *) - | (NumLevel n,BorderProd (Left,Some a)) -> - begin match a with - | Extend.LeftA -> Some (Some (n, true)) - | _ -> Some None - end - (* None means NEXT *) - | (NextLevel,_) -> Some None -(* Compute production name elsewhere *) - | (NumLevel n,InternalProd) -> - match from with - | ETConstr (p,()) when Int.equal p (n + 1) -> Some None - | ETConstr (p,()) -> Some (Some (n, Int.equal n p)) - | _ -> Some (Some (n,false)) - -let compute_entry adjust forpat = function - | ETConstr (n,q) -> - (if forpat then weaken_entry Constr.pattern - else weaken_entry Constr.operconstr), - adjust (n,q), false - | ETName -> weaken_entry Prim.name, None, false - | ETBinder true -> anomaly (Pp.str "Should occur only as part of BinderList") - | ETBinder false -> weaken_entry Constr.binder, None, false - | ETBinderList (true,tkl) -> - let () = match tkl with [] -> () | _ -> assert false in - weaken_entry Constr.open_binders, None, false - | ETBinderList (false,_) -> anomaly (Pp.str "List of entries cannot be registered.") - | ETBigint -> weaken_entry Prim.bigint, None, false - | ETReference -> weaken_entry Constr.global, None, false - | ETPattern -> weaken_entry Constr.pattern, None, false - | ETConstrList _ -> anomaly (Pp.str "List of entries cannot be registered.") - | ETOther (u,n) -> assert false - -(* This computes the name of the level where to add a new rule *) -let interp_constr_entry_key forpat level = - if level = 200 && not forpat then weaken_entry Constr.binder_constr, None - else if forpat then weaken_entry Constr.pattern, Some level - else weaken_entry Constr.operconstr, Some level - -(* This computes the name to give to a production knowing the name and - associativity of the level where it must be added *) -let interp_constr_prod_entry_key ass from forpat en = - compute_entry (adjust_level ass from) forpat en - -(**********************************************************************) -(* Binding constr entry keys to symbols *) - -let is_self from e = - match from, e with - ETConstr(n,()), ETConstr(NumLevel n', - BorderProd(Right, _ (* Some(NonA|LeftA) *))) -> false - | ETConstr(n,()), ETConstr(NumLevel n',BorderProd(Left,_)) -> Int.equal n n' - | (ETName,ETName | ETReference, ETReference | ETBigint,ETBigint - | ETPattern, ETPattern) -> true - | ETOther(s1,s2), ETOther(s1',s2') -> - String.equal s1 s1' && String.equal s2 s2' - | _ -> false - -let is_binder_level from e = - match from, e with - ETConstr(200,()), - ETConstr(NumLevel 200,(BorderProd(Right,_)|InternalProd)) -> true - | _ -> false - -let make_sep_rules tkl = - Gram.srules' - [List.map gram_token_of_token tkl, - List.fold_right (fun _ v -> Gram.action (fun _ -> v)) tkl - (Gram.action (fun loc -> ()))] - -let rec symbol_of_constr_prod_entry_key assoc from forpat typ = - if is_binder_level from typ then - if forpat then - Symbols.snterml (Gram.Entry.obj Constr.pattern,"200") - else - Symbols.snterml (Gram.Entry.obj Constr.operconstr,"200") - else if is_self from typ then - Symbols.sself - else - match typ with - | ETConstrList (typ',[]) -> - Symbols.slist1 (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ')) - | ETConstrList (typ',tkl) -> - Symbols.slist1sep - (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'), - make_sep_rules tkl) - | ETBinderList (false,[]) -> - Symbols.slist1 - (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false)) - | ETBinderList (false,tkl) -> - Symbols.slist1sep - (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false), - make_sep_rules tkl) - - | _ -> - match interp_constr_prod_entry_key assoc from forpat typ with - | (eobj,None,_) -> Symbols.snterm (Gram.Entry.obj eobj) - | (eobj,Some None,_) -> Symbols.snext - | (eobj,Some (Some (lev,cur)),_) -> - Symbols.snterml (Gram.Entry.obj eobj,constr_level lev) - (** 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 @@ -707,8 +553,6 @@ and symbol_of_rules : type a. a Extend.rules -> _ = function let act = of_coq_action r.norec_rule act in (symb, act) -let level_of_snterml e = int_of_string (Symbols.snterml_level e) - let of_coq_production_rule : type a. a Extend.production_rule -> _ = function | Rule (toks, act) -> (symbol_of_rule toks [], of_coq_action toks act) diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 8d653a179b..84f72ac55c 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -254,39 +254,3 @@ val synchronize_level_positions : unit -> unit val register_empty_levels : bool -> int list -> gram_level list val remove_levels : int -> unit - -(** {5 Unsafe grammar extension API} - -For compatibility purpose only. Do not use in newly written code. - -*) - -val gram_token_of_token : Tok.t -> Gram.symbol -val gram_token_of_string : string -> Gram.symbol -val level_of_snterml : Gram.symbol -> int - -(** The superclass of all grammar entries *) -type grammar_object - -(** Binding constr entry keys to entries and symbols *) - -val interp_constr_entry_key : bool (** true for cases_pattern *) -> - int -> grammar_object Gram.entry * int option - -val symbol_of_constr_prod_entry_key : gram_assoc option -> - constr_entry_key -> bool -> constr_prod_entry_key -> - Gram.symbol - -type unsafe_single_extend_statment = - string option * - gram_assoc option * - Gram.production_rule list - -type unsafe_extend_statment = - gram_position option * - unsafe_single_extend_statment list - -val unsafe_grammar_extend : - grammar_object Gram.entry -> - gram_reinit option (** for reinitialization if ever needed *) -> - unsafe_extend_statment -> unit -- cgit v1.2.3 From b82512946a2818e13397b9f1a128fcafe4a78ba5 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 10 May 2016 19:19:10 +0200 Subject: Further tidying of the constr extension code. --- parsing/egramcoq.ml | 101 ++++++++++++++++++++-------------------------------- 1 file changed, 39 insertions(+), 62 deletions(-) (limited to 'parsing') diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 6286dab5a5..4c038db65c 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -102,9 +102,8 @@ type (_, _) entry = | TTName : ('self, Name.t Loc.located) entry | TTReference : ('self, reference) entry | TTBigint : ('self, Bigint.bigint) entry -| TTBinder : bool -> ('self, local_binder list) entry +| TTBinder : ('self, local_binder list) entry | TTConstr : prod_info * 'r target -> ('r, 'r) entry -| TTPattern : ('self, cases_pattern_expr) entry | TTConstrList : prod_info * Tok.t list * 'r target -> ('r, 'r list) entry | TTBinderListT : ('self, local_binder list) entry | TTBinderListF : Tok.t list -> ('self, local_binder list list) entry @@ -119,18 +118,9 @@ let interp_constr_entry_key : type r. r target -> int -> r Gram.entry * int opti else Constr.operconstr, Some level | ForPattern -> Constr.pattern, Some level -let compute_entry : type s r. (s, r) entry -> r Gram.entry = function -| TTConstr (_, ForConstr) -> Constr.operconstr -| TTConstr (_, ForPattern) -> Constr.pattern -| TTName -> Prim.name -| TTBinder true -> anomaly (Pp.str "Should occur only as part of BinderList") -| TTBinder false -> Constr.binder -| TTBinderListT -> Constr.open_binders -| TTBinderListF _ -> anomaly (Pp.str "List of entries cannot be registered.") -| TTBigint -> Prim.bigint -| TTReference -> Constr.global -| TTPattern -> Constr.pattern -| TTConstrList _ -> anomaly (Pp.str "List of entries cannot be registered.") +let target_entry : type s. s target -> s Gram.entry = function +| ForConstr -> Constr.operconstr +| ForPattern -> Constr.pattern let is_self from e = match e with | (NumLevel n, BorderProd (Right, _ (* Some(NonA|LeftA) *))) -> false @@ -152,43 +142,40 @@ let make_sep_rules tkl = let r = mkrule (List.rev tkl) in Arules [r] -let rec symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) symbol = fun assoc from typ -> match typ with -| TTConstr (p, forpat) -> - if is_binder_level from p then match forpat with - | ForConstr -> Aentryl (Constr.operconstr, 200) - | ForPattern -> Aentryl (Constr.pattern, 200) +let symbol_of_target : type s. _ -> _ -> _ -> s target -> (s, s) symbol = fun p assoc from forpat -> + if is_binder_level from p then Aentryl (target_entry forpat, 200) else if is_self from p then Aself else - let g = compute_entry (TTConstr (p, forpat)) in + let g = target_entry forpat in let lev = adjust_level assoc from p in begin match lev with | None -> Aentry g | Some None -> Anext | Some (Some (lev, cur)) -> Aentryl (g, lev) end + +let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) symbol = fun assoc from typ -> match typ with +| TTConstr (p, forpat) -> symbol_of_target p assoc from forpat | TTConstrList (typ', [], forpat) -> - let symb = symbol_of_entry assoc from (TTConstr (typ', forpat)) in - Alist1 symb + Alist1 (symbol_of_target typ' assoc from forpat) | TTConstrList (typ', tkl, forpat) -> - let symb = symbol_of_entry assoc from (TTConstr (typ', forpat)) in - Alist1sep (symb, make_sep_rules tkl) -| TTBinderListF [] -> - let symb = symbol_of_entry assoc from (TTBinder false) in - Alist1 (symb) -| TTBinderListF tkl -> - let symb = symbol_of_entry assoc from (TTBinder false) in - Alist1sep (symb, make_sep_rules tkl) -| _ -> - let g = compute_entry typ in - Aentry g + Alist1sep (symbol_of_target typ' assoc from forpat, make_sep_rules tkl) +| TTBinderListF [] -> Alist1 (Aentry Constr.binder) +| TTBinderListF tkl -> Alist1sep (Aentry Constr.binder, make_sep_rules tkl) +| TTName -> Aentry Prim.name +| TTBinder -> Aentry Constr.binder +| TTBinderListT -> Aentry Constr.open_binders +| TTBigint -> Aentry Prim.bigint +| TTReference -> Aentry Constr.global let interp_entry forpat e = match e with | ETName -> TTAny TTName | ETReference -> TTAny TTReference | ETBigint -> TTAny TTBigint -| ETBinder b -> TTAny (TTBinder b) +| ETBinder true -> anomaly (Pp.str "Should occur only as part of BinderList") +| ETBinder false -> TTAny TTBinder | ETConstr p -> TTAny (TTConstr (p, forpat)) -| ETPattern -> TTAny TTPattern +| ETPattern -> assert false (** not used *) | ETOther _ -> assert false (** not used *) | ETConstrList (p, tkl) -> TTAny (TTConstrList (p, tkl, forpat)) | ETBinderList (true, []) -> TTAny TTBinderListT @@ -226,7 +213,7 @@ match e with | ForConstr -> push_constr subst (constr_expr_of_name v) | ForPattern -> push_constr subst (cases_pattern_expr_of_name v) end -| TTBinder _ -> { subst with binders = (v, true) :: subst.binders } +| TTBinder -> { subst with binders = (v, true) :: subst.binders } | TTBinderListT -> { subst with binders = (v, true) :: subst.binders } | TTBinderListF _ -> { subst with binders = (List.flatten v, false) :: subst.binders } | TTBigint -> @@ -239,7 +226,6 @@ match e with | ForConstr -> push_constr subst (CRef (v, None)) | ForPattern -> push_constr subst (CPatAtom (Loc.ghost, Some v)) end -| TTPattern -> anomaly (Pp.str "Unexpected entry of type cases pattern or other") | TTConstrList _ -> { subst with constrlists = v :: subst.constrlists } type (_, _) ty_symbol = @@ -328,7 +314,18 @@ let make_act : type r. r target -> _ -> r gen_eval = function let env = (env.constrs, env.constrlists) in CPatNotation (loc, notation, env, []) -let extend_constr (entry,level) (n,assoc) forpat notation rules = +type notation_grammar = { + notgram_level : int; + notgram_assoc : gram_assoc option; + notgram_notation : notation; + notgram_prods : grammar_constr_prod_item list list; + notgram_typs : notation_var_internalization_type list; +} + +let extend_constr forpat ng = + let n = ng.notgram_level in + let assoc = ng.notgram_assoc in + let (entry, level) = interp_constr_entry_key forpat n in let fold nb pt = let AnyTyRule r = make_ty_rule assoc n forpat pt in let symbs = ty_erase r in @@ -339,38 +336,18 @@ let extend_constr (entry,level) (n,assoc) forpat notation rules = let nb_decls = List.length needed_levels + 1 in let () = List.iter (prepare_empty_levels isforpat) needed_levels in let empty = { constrs = []; constrlists = []; binders = [] } in - let act = ty_eval r (make_act forpat notation) empty in + let act = ty_eval r (make_act forpat ng.notgram_notation) empty in let rule = (name, p4assoc, [Rule (symbs, act)]) in let () = grammar_extend entry reinit (pos, [rule]) in nb_decls in - List.fold_left fold 0 rules - -type notation_grammar = { - notgram_level : int; - notgram_assoc : gram_assoc option; - notgram_notation : notation; - notgram_prods : grammar_constr_prod_item list list; - notgram_typs : notation_var_internalization_type list; -} - -let extend_constr_constr_notation ng = - let level = ng.notgram_level in - let e = interp_constr_entry_key ForConstr level in - let ext = (level, ng.notgram_assoc) in - extend_constr e ext ForConstr ng.notgram_notation ng.notgram_prods - -let extend_constr_pat_notation ng = - let level = ng.notgram_level in - let e = interp_constr_entry_key ForPattern level in - let ext = (level, ng.notgram_assoc) in - extend_constr e ext ForPattern ng.notgram_notation ng.notgram_prods + List.fold_left fold 0 ng.notgram_prods let extend_constr_notation (_, ng) = (* Add the notation in constr *) - let nb = extend_constr_constr_notation ng in + let nb = extend_constr ForConstr ng in (* Add the notation in cases_pattern *) - let nb' = extend_constr_pat_notation ng in + let nb' = extend_constr ForPattern ng in nb + nb' module GrammarCommand = Dyn.Make(struct end) -- cgit v1.2.3 From bc3981687cd363820e35e5a2bd037d50e213f524 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 10 May 2016 19:42:39 +0200 Subject: Overlooked use of Gram instead of G module in Pcoq. This was probably wreaking havoc in tricky undo-redo scenarii. --- parsing/pcoq.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'parsing') diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 8fa5da4bd9..305cd4f80f 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -572,7 +572,7 @@ 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 let entry = G.entry_create "epsilon" in - let () = maybe_uncurry (Gram.extend entry) ext in + let () = maybe_uncurry (G.extend entry) ext in try Some (parse_string entry "") with _ -> None (** Registering grammar of generic arguments *) -- cgit v1.2.3 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 ++++++++++++++++++++++--------------------------------- parsing/pcoq.mli | 5 --- 2 files changed, 52 insertions(+), 86 deletions(-) (limited to 'parsing') diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 305cd4f80f..631c5325dc 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 diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 84f72ac55c..72edab8f2f 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -235,11 +235,6 @@ val set_command_entry : vernac_expr Gram.entry -> unit val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option -(** Binding general entry keys to symbols *) - -(** Recover the list of all known tactic notation entries. *) -val list_entry_names : unit -> (string * argument_type) list - (** Registering/resetting the level of a constr entry *) type gram_level = -- cgit v1.2.3 From 17da4a6805622ab3b5e46b0c3ffef57e4b7ded4c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 11 May 2016 10:30:49 +0200 Subject: Moving the grammar summary to Pcoq. --- parsing/egramcoq.ml | 81 ++++------------------------------------------------ parsing/egramcoq.mli | 16 ----------- parsing/pcoq.ml | 74 +++++++++++++++++++++++++++++++++++++++++++++++ parsing/pcoq.mli | 24 ++++++++++++---- 4 files changed, 99 insertions(+), 96 deletions(-) (limited to 'parsing') diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 4c038db65c..9cfd534b0c 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -350,85 +350,16 @@ let extend_constr_notation (_, ng) = let nb' = extend_constr ForPattern ng in nb + nb' -module GrammarCommand = Dyn.Make(struct end) -module GrammarInterp = struct type 'a t = 'a -> int end -module GrammarInterpMap = GrammarCommand.Map(GrammarInterp) - -let grammar_interp = ref GrammarInterpMap.empty - -let (grammar_state : (int * GrammarCommand.t) list ref) = ref [] - -type 'a grammar_command = 'a GrammarCommand.tag - -let create_grammar_command name interp : _ grammar_command = - let obj = GrammarCommand.create name in - let () = grammar_interp := GrammarInterpMap.add obj interp !grammar_interp in - obj - -let extend_grammar tag g = - let nb = GrammarInterpMap.find tag !grammar_interp g in - grammar_state := (nb, GrammarCommand.Dyn (tag, g)) :: !grammar_state - -let extend_dyn_grammar (GrammarCommand.Dyn (tag, g)) = extend_grammar tag g - -let constr_grammar : (Notation.level * notation_grammar) GrammarCommand.tag = +let constr_grammar : (Notation.level * notation_grammar) grammar_command = create_grammar_command "Notation" extend_constr_notation -let extend_constr_grammar pr ntn = extend_grammar constr_grammar (pr, ntn) +let extend_constr_grammar pr ntn = extend_grammar_command constr_grammar (pr, ntn) let recover_constr_grammar ntn prec = - let filter (_, gram) : notation_grammar option = match gram with - | GrammarCommand.Dyn (tag, obj) -> - match GrammarCommand.eq tag constr_grammar with - | None -> None - | Some Refl -> - let (prec', ng) = obj in - if Notation.level_eq prec prec' && String.equal ntn ng.notgram_notation then Some ng - else None + let filter (prec', ng) = + if Notation.level_eq prec prec' && String.equal ntn ng.notgram_notation then Some ng + else None in - match List.map_filter filter !grammar_state with + match List.map_filter filter (recover_grammar_command constr_grammar) with | [x] -> x | _ -> assert false - -(* Summary functions: the state of the lexer is included in that of the parser. - Because the grammar affects the set of keywords when adding or removing - grammar rules. *) -type frozen_t = (int * GrammarCommand.t) list * CLexer.frozen_t - -let freeze _ : frozen_t = (!grammar_state, CLexer.freeze ()) - -(* We compare the current state of the grammar and the state to unfreeze, - by computing the longest common suffixes *) -let factorize_grams l1 l2 = - if l1 == l2 then ([], [], l1) else List.share_tails l1 l2 - -let number_of_entries gcl = - List.fold_left (fun n (p,_) -> n + p) 0 gcl - -let unfreeze (grams, lex) = - let (undo, redo, common) = factorize_grams !grammar_state grams in - let n = number_of_entries undo in - remove_grammars n; - remove_levels n; - grammar_state := common; - CLexer.unfreeze lex; - List.iter extend_dyn_grammar (List.rev_map snd redo) - -(** No need to provide an init function : the grammar state is - statically available, and already empty initially, while - the lexer state should not be resetted, since it contains - keywords declared in g_*.ml4 *) - -let _ = - Summary.declare_summary "GRAMMAR_LEXER" - { Summary.freeze_function = freeze; - Summary.unfreeze_function = unfreeze; - Summary.init_function = Summary.nop } - -let with_grammar_rule_protection f x = - let fs = freeze false in - try let a = f x in unfreeze fs; a - with reraise -> - let reraise = Errors.push reraise in - let () = unfreeze fs in - iraise reraise diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli index 6ec1066260..1fe06a29df 100644 --- a/parsing/egramcoq.mli +++ b/parsing/egramcoq.mli @@ -36,20 +36,6 @@ type notation_grammar = { notgram_typs : notation_var_internalization_type list; } -(** {5 Extending the parser with Summary-synchronized commands} *) - -type 'a grammar_command -(** Type of synchronized parsing extensions. The ['a] type should be - marshallable. *) - -val create_grammar_command : string -> ('a -> int) -> 'a grammar_command -(** Create a new grammar-modifying command with the given name. The function - should modify the parser state and return the number of grammar extensions - performed. *) - -val extend_grammar : 'a grammar_command -> 'a -> unit -(** Extend the grammar of Coq with the given data. *) - (** {5 Adding notations} *) val extend_constr_grammar : Notation.level -> notation_grammar -> unit @@ -58,5 +44,3 @@ val extend_constr_grammar : Notation.level -> notation_grammar -> unit val recover_constr_grammar : notation -> Notation.level -> notation_grammar (** For a declared grammar, returns the rule + the ordered entry types of variables in the rule (for use in the interpretation) *) - -val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 631c5325dc..de57feb7f3 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -546,6 +546,80 @@ let epsilon_value f e = let () = maybe_uncurry (G.extend entry) ext in try Some (parse_string entry "") with _ -> None +(** Synchronized grammar extensions *) + +module GrammarCommand = Dyn.Make(struct end) +module GrammarInterp = struct type 'a t = 'a -> int end +module GrammarInterpMap = GrammarCommand.Map(GrammarInterp) + +let grammar_interp = ref GrammarInterpMap.empty + +let (grammar_state : (int * GrammarCommand.t) list ref) = ref [] + +type 'a grammar_command = 'a GrammarCommand.tag + +let create_grammar_command name interp : _ grammar_command = + let obj = GrammarCommand.create name in + let () = grammar_interp := GrammarInterpMap.add obj interp !grammar_interp in + obj + +let extend_grammar_command tag g = + let nb = GrammarInterpMap.find tag !grammar_interp g in + grammar_state := (nb, GrammarCommand.Dyn (tag, g)) :: !grammar_state + +let recover_grammar_command (type a) (tag : a grammar_command) : a list = + let filter : _ -> a option = fun (_, GrammarCommand.Dyn (tag', v)) -> + match GrammarCommand.eq tag tag' with + | None -> None + | Some Refl -> Some v + in + List.map_filter filter !grammar_state + +let extend_dyn_grammar (GrammarCommand.Dyn (tag, g)) = extend_grammar_command tag g + +(* Summary functions: the state of the lexer is included in that of the parser. + Because the grammar affects the set of keywords when adding or removing + grammar rules. *) +type frozen_t = (int * GrammarCommand.t) list * CLexer.frozen_t + +let freeze _ : frozen_t = (!grammar_state, CLexer.freeze ()) + +(* We compare the current state of the grammar and the state to unfreeze, + by computing the longest common suffixes *) +let factorize_grams l1 l2 = + if l1 == l2 then ([], [], l1) else List.share_tails l1 l2 + +let number_of_entries gcl = + List.fold_left (fun n (p,_) -> n + p) 0 gcl + +let unfreeze (grams, lex) = + let (undo, redo, common) = factorize_grams !grammar_state grams in + let n = number_of_entries undo in + remove_grammars n; + remove_levels n; + grammar_state := common; + CLexer.unfreeze lex; + List.iter extend_dyn_grammar (List.rev_map snd redo) + +(** No need to provide an init function : the grammar state is + statically available, and already empty initially, while + the lexer state should not be resetted, since it contains + keywords declared in g_*.ml4 *) + +let _ = + Summary.declare_summary "GRAMMAR_LEXER" + { Summary.freeze_function = freeze; + Summary.unfreeze_function = unfreeze; + Summary.init_function = Summary.nop } + +let with_grammar_rule_protection f x = + let fs = freeze false in + try let a = f x in unfreeze fs; a + with reraise -> + let reraise = Errors.push reraise in + let () = unfreeze fs in + iraise reraise + (** Registering grammar of generic arguments *) let () = diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 72edab8f2f..1021ef4844 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -106,9 +106,6 @@ val grammar_extend : gram_reinit option (** for reinitialization if ever needed *) -> 'a Extend.extend_statment -> unit -(** Remove the last n extensions *) -val remove_grammars : int -> unit - (** Temporary activate camlp4 verbosity *) val camlp4_verbosity : bool -> ('a -> unit) -> 'a -> unit @@ -235,6 +232,25 @@ val set_command_entry : vernac_expr Gram.entry -> unit val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option +(** {5 Extending the parser with Summary-synchronized commands} *) + +type 'a grammar_command +(** Type of synchronized parsing extensions. The ['a] type should be + marshallable. *) + +val create_grammar_command : string -> ('a -> int) -> 'a grammar_command +(** Create a new grammar-modifying command with the given name. The function + should modify the parser state and return the number of grammar extensions + performed. *) + +val extend_grammar_command : 'a grammar_command -> 'a -> unit +(** Extend the grammar of Coq with the given data. *) + +val recover_grammar_command : 'a grammar_command -> 'a list +(** Recover the current stack of grammar extensions. *) + +val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b + (** Registering/resetting the level of a constr entry *) type gram_level = @@ -247,5 +263,3 @@ val find_position : val synchronize_level_positions : unit -> unit val register_empty_levels : bool -> int list -> gram_level list - -val remove_levels : int -> unit -- cgit v1.2.3 From df2d71323081f8a395881ffc0e1793e429abc3bb Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 11 May 2016 11:28:04 +0200 Subject: Turning the grammar extend command API into a state-passing one. --- parsing/egramcoq.ml | 4 ++-- parsing/pcoq.ml | 33 +++++++++++++++++++++------------ parsing/pcoq.mli | 7 ++++++- 3 files changed, 29 insertions(+), 15 deletions(-) (limited to 'parsing') diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 9cfd534b0c..72cb14badd 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -343,12 +343,12 @@ let extend_constr forpat ng = in List.fold_left fold 0 ng.notgram_prods -let extend_constr_notation (_, ng) = +let extend_constr_notation (_, ng) state = (* Add the notation in constr *) let nb = extend_constr ForConstr ng in (* Add the notation in cases_pattern *) let nb' = extend_constr ForPattern ng in - nb + nb' + (nb + nb', state) let constr_grammar : (Notation.level * notation_grammar) grammar_command = create_grammar_command "Notation" extend_constr_notation diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index de57feb7f3..efb52dc233 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -548,13 +548,17 @@ let epsilon_value f e = (** Synchronized grammar extensions *) +module GramState = Store.Make(struct end) + +type 'a grammar_extension = 'a -> GramState.t -> int * GramState.t + module GrammarCommand = Dyn.Make(struct end) -module GrammarInterp = struct type 'a t = 'a -> int end +module GrammarInterp = struct type 'a t = 'a grammar_extension end module GrammarInterpMap = GrammarCommand.Map(GrammarInterp) let grammar_interp = ref GrammarInterpMap.empty -let (grammar_state : (int * GrammarCommand.t) list ref) = ref [] +let (grammar_stack : (int * GrammarCommand.t * GramState.t) list ref) = ref [] type 'a grammar_command = 'a GrammarCommand.tag @@ -564,25 +568,30 @@ let create_grammar_command name interp : _ grammar_command = obj let extend_grammar_command tag g = - let nb = GrammarInterpMap.find tag !grammar_interp g in - grammar_state := (nb, GrammarCommand.Dyn (tag, g)) :: !grammar_state + let modify = GrammarInterpMap.find tag !grammar_interp in + let grammar_state = match !grammar_stack with + | [] -> GramState.empty + | (_, _, st) :: _ -> st + in + let (nb, st) = modify g grammar_state in + grammar_stack := (nb, GrammarCommand.Dyn (tag, g), st) :: !grammar_stack let recover_grammar_command (type a) (tag : a grammar_command) : a list = - let filter : _ -> a option = fun (_, GrammarCommand.Dyn (tag', v)) -> + let filter : _ -> a option = fun (_, GrammarCommand.Dyn (tag', v), _) -> match GrammarCommand.eq tag tag' with | None -> None | Some Refl -> Some v in - List.map_filter filter !grammar_state + List.map_filter filter !grammar_stack let extend_dyn_grammar (GrammarCommand.Dyn (tag, g)) = extend_grammar_command tag g (* Summary functions: the state of the lexer is included in that of the parser. Because the grammar affects the set of keywords when adding or removing grammar rules. *) -type frozen_t = (int * GrammarCommand.t) list * CLexer.frozen_t +type frozen_t = (int * GrammarCommand.t * GramState.t) list * CLexer.frozen_t -let freeze _ : frozen_t = (!grammar_state, CLexer.freeze ()) +let freeze _ : frozen_t = (!grammar_stack, CLexer.freeze ()) (* We compare the current state of the grammar and the state to unfreeze, by computing the longest common suffixes *) @@ -590,16 +599,16 @@ let factorize_grams l1 l2 = if l1 == l2 then ([], [], l1) else List.share_tails l1 l2 let number_of_entries gcl = - List.fold_left (fun n (p,_) -> n + p) 0 gcl + List.fold_left (fun n (p,_,_) -> n + p) 0 gcl let unfreeze (grams, lex) = - let (undo, redo, common) = factorize_grams !grammar_state grams in + let (undo, redo, common) = factorize_grams !grammar_stack grams in let n = number_of_entries undo in remove_grammars n; remove_levels n; - grammar_state := common; + grammar_stack := common; CLexer.unfreeze lex; - List.iter extend_dyn_grammar (List.rev_map snd redo) + List.iter extend_dyn_grammar (List.rev_map pi2 redo) (** No need to provide an init function : the grammar state is statically available, and already empty initially, while diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 1021ef4844..98fc471332 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -234,11 +234,16 @@ val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option (** {5 Extending the parser with Summary-synchronized commands} *) +module GramState : Store.S +(** Auxilliary state of the grammar. Any added data must be marshallable. *) + type 'a grammar_command (** Type of synchronized parsing extensions. The ['a] type should be marshallable. *) -val create_grammar_command : string -> ('a -> int) -> 'a grammar_command +type 'a grammar_extension = 'a -> GramState.t -> int * GramState.t + +val create_grammar_command : string -> 'a grammar_extension -> 'a grammar_command (** Create a new grammar-modifying command with the given name. The function should modify the parser state and return the number of grammar extensions performed. *) -- cgit v1.2.3 From 85753a0bdb6183604a78232c4c32fd15f7a21a2a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 11 May 2016 13:25:02 +0200 Subject: Moving the constr empty entry registering to the state-based API. --- parsing/egramcoq.ml | 153 +++++++++++++++++++++++++++++++++++++++++++++++++--- parsing/pcoq.ml | 146 ------------------------------------------------- parsing/pcoq.mli | 13 ----- 3 files changed, 145 insertions(+), 167 deletions(-) (limited to 'parsing') diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 72cb14badd..8af324d71b 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -15,6 +15,136 @@ open Notation_term open Libnames open Names +(**********************************************************************) +(* This determines (depending on the associativity of the current + level and on the expected associativity) if a reference to constr_n is + a reference to the current level (to be translated into "SELF" on the + left border and into "constr LEVEL n" elsewhere), to the level below + (to be translated into "NEXT") or to an below wrt associativity (to be + translated in camlp4 into "constr" without level) or to another level + (to be translated into "constr LEVEL n") + + The boolean is true if the entry was existing _and_ empty; this to + circumvent a weakness of camlp4/camlp5 whose undo mechanism is not the + converse of the extension mechanism *) + +let constr_level = string_of_int + +let default_levels = + [200,Extend.RightA,false; + 100,Extend.RightA,false; + 99,Extend.RightA,true; + 10,Extend.RightA,false; + 9,Extend.RightA,false; + 8,Extend.RightA,true; + 1,Extend.LeftA,false; + 0,Extend.RightA,false] + +let default_pattern_levels = + [200,Extend.RightA,true; + 100,Extend.RightA,false; + 99,Extend.RightA,true; + 11,Extend.LeftA,false; + 10,Extend.RightA,false; + 1,Extend.LeftA,false; + 0,Extend.RightA,false] + +let default_constr_levels = (default_levels, default_pattern_levels) + +(* At a same level, LeftA takes precedence over RightA and NoneA *) +(* In case, several associativity exists for a level, we make two levels, *) +(* first LeftA, then RightA and NoneA together *) + +let admissible_assoc = function + | Extend.LeftA, Some (Extend.RightA | Extend.NonA) -> false + | Extend.RightA, Some Extend.LeftA -> false + | _ -> true + +let create_assoc = function + | None -> Extend.RightA + | Some a -> a + +let error_level_assoc p current expected = + let open Pp in + let pr_assoc = function + | Extend.LeftA -> str "left" + | Extend.RightA -> str "right" + | Extend.NonA -> str "non" in + errorlabstrm "" + (str "Level " ++ int p ++ str " is already declared " ++ + pr_assoc current ++ str " associative while it is now expected to be " ++ + pr_assoc expected ++ str " associative.") + +let create_pos = function + | None -> Extend.First + | Some lev -> Extend.After (constr_level lev) + +type gram_level = + gram_position option * gram_assoc option * string option * + (** for reinitialization: *) gram_reinit option + +let find_position_gen current ensure assoc lev = + match lev with + | None -> + current, (None, None, None, None) + | Some n -> + let after = ref None in + let init = ref None in + let rec add_level q = function + | (p,_,_ as pa)::l when p > n -> pa :: add_level (Some p) l + | (p,a,reinit)::l when Int.equal p n -> + if reinit then + let a' = create_assoc assoc in + (init := Some (a',create_pos q); (p,a',false)::l) + else if admissible_assoc (a,assoc) then + raise Exit + else + error_level_assoc p a (Option.get assoc) + | l -> after := q; (n,create_assoc assoc,ensure)::l + in + try + let updated = add_level None current in + let assoc = create_assoc assoc in + begin match !init with + | None -> + (* Create the entry *) + updated, (Some (create_pos !after), Some assoc, Some (constr_level n), None) + | _ -> + (* The reinit flag has been updated *) + updated, (Some (Extend.Level (constr_level n)), None, None, !init) + end + with + (* Nothing has changed *) + Exit -> + (* Just inherit the existing associativity and name (None) *) + current, (Some (Extend.Level (constr_level n)), None, None, None) + +let rec list_mem_assoc_triple x = function + | [] -> false + | (a,b,c) :: l -> Int.equal a x || list_mem_assoc_triple x l + +let register_empty_levels accu forpat levels = + let rec filter accu = function + | [] -> ([], accu) + | n :: rem -> + let rem, accu = filter accu rem in + let (clev, plev) = accu in + let levels = if forpat then plev else clev in + if not (list_mem_assoc_triple n levels) then + let nlev, ans = find_position_gen levels true None (Some n) in + let nlev = if forpat then (clev, nlev) else (nlev, plev) in + ans :: rem, nlev + else rem, accu + in + filter accu levels + +let find_position accu forpat assoc level = + let (clev, plev) = accu in + let levels = if forpat then plev else clev in + let nlev, ans = find_position_gen levels false assoc level in + let nlev = if forpat then (clev, nlev) else (nlev, plev) in + (ans, nlev) + (**************************************************************************) (* * --- Note on the mapping of grammar productions to camlp4 actions --- @@ -322,32 +452,39 @@ type notation_grammar = { notgram_typs : notation_var_internalization_type list; } -let extend_constr forpat ng = +let extend_constr state forpat ng = let n = ng.notgram_level in let assoc = ng.notgram_assoc in let (entry, level) = interp_constr_entry_key forpat n in - let fold nb pt = + let fold (nb, state) pt = let AnyTyRule r = make_ty_rule assoc n forpat pt in let symbs = ty_erase r in let pure_sublevels = pure_sublevels level symbs in let isforpat = target_to_bool forpat in - let needed_levels = register_empty_levels isforpat pure_sublevels in - let pos,p4assoc,name,reinit = find_position isforpat assoc level in + let needed_levels, state = register_empty_levels state isforpat pure_sublevels in + let (pos,p4assoc,name,reinit), state = find_position state isforpat assoc level in let nb_decls = List.length needed_levels + 1 in let () = List.iter (prepare_empty_levels isforpat) needed_levels in let empty = { constrs = []; constrlists = []; binders = [] } in let act = ty_eval r (make_act forpat ng.notgram_notation) empty in let rule = (name, p4assoc, [Rule (symbs, act)]) in let () = grammar_extend entry reinit (pos, [rule]) in - nb_decls + (nb + nb_decls, state) in - List.fold_left fold 0 ng.notgram_prods + List.fold_left fold (0, state) ng.notgram_prods + +let constr_levels = GramState.field () let extend_constr_notation (_, ng) state = + let levels = match GramState.get state constr_levels with + | None -> default_constr_levels + | Some lev -> lev + in (* Add the notation in constr *) - let nb = extend_constr ForConstr ng in + let (nb, levels) = extend_constr levels ForConstr ng in (* Add the notation in cases_pattern *) - let nb' = extend_constr ForPattern ng in + let (nb', levels) = extend_constr levels ForPattern ng in + let state = GramState.set state constr_levels levels in (nb + nb', state) let constr_grammar : (Notation.level * notation_grammar) grammar_command = diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index efb52dc233..1cc7b6c540 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -394,151 +394,6 @@ let main_entry = Vernac_.main_entry let set_command_entry e = Vernac_.command_entry_ref := e let get_command_entry () = !Vernac_.command_entry_ref -(**********************************************************************) -(* This determines (depending on the associativity of the current - level and on the expected associativity) if a reference to constr_n is - a reference to the current level (to be translated into "SELF" on the - left border and into "constr LEVEL n" elsewhere), to the level below - (to be translated into "NEXT") or to an below wrt associativity (to be - translated in camlp4 into "constr" without level) or to another level - (to be translated into "constr LEVEL n") - - The boolean is true if the entry was existing _and_ empty; this to - circumvent a weakness of camlp4/camlp5 whose undo mechanism is not the - converse of the extension mechanism *) - -let constr_level = string_of_int - -let default_levels = - [200,Extend.RightA,false; - 100,Extend.RightA,false; - 99,Extend.RightA,true; - 10,Extend.RightA,false; - 9,Extend.RightA,false; - 8,Extend.RightA,true; - 1,Extend.LeftA,false; - 0,Extend.RightA,false] - -let default_pattern_levels = - [200,Extend.RightA,true; - 100,Extend.RightA,false; - 99,Extend.RightA,true; - 11,Extend.LeftA,false; - 10,Extend.RightA,false; - 1,Extend.LeftA,false; - 0,Extend.RightA,false] - -(* At a same level, LeftA takes precedence over RightA and NoneA *) -(* In case, several associativity exists for a level, we make two levels, *) -(* first LeftA, then RightA and NoneA together *) - -let admissible_assoc = function - | Extend.LeftA, Some (Extend.RightA | Extend.NonA) -> false - | Extend.RightA, Some Extend.LeftA -> false - | _ -> true - -let create_assoc = function - | None -> Extend.RightA - | Some a -> a - -let error_level_assoc p current expected = - let pr_assoc = function - | Extend.LeftA -> str "left" - | Extend.RightA -> str "right" - | Extend.NonA -> str "non" in - errorlabstrm "" - (str "Level " ++ int p ++ str " is already declared " ++ - pr_assoc current ++ str " associative while it is now expected to be " ++ - pr_assoc expected ++ str " associative.") - -let create_pos = function - | None -> Extend.First - | Some lev -> Extend.After (constr_level lev) - -let find_position_gen current ensure assoc lev = - match lev with - | None -> - current, (None, None, None, None) - | Some n -> - let after = ref None in - let init = ref None in - let rec add_level q = function - | (p,_,_ as pa)::l when p > n -> pa :: add_level (Some p) l - | (p,a,reinit)::l when Int.equal p n -> - if reinit then - let a' = create_assoc assoc in - (init := Some (a',create_pos q); (p,a',false)::l) - else if admissible_assoc (a,assoc) then - raise Exit - else - error_level_assoc p a (Option.get assoc) - | l -> after := q; (n,create_assoc assoc,ensure)::l - in - try - let updated = add_level None current in - let assoc = create_assoc assoc in - begin match !init with - | None -> - (* Create the entry *) - updated, (Some (create_pos !after), Some assoc, Some (constr_level n), None) - | _ -> - (* The reinit flag has been updated *) - updated, (Some (Extend.Level (constr_level n)), None, None, !init) - end - with - (* Nothing has changed *) - Exit -> - (* Just inherit the existing associativity and name (None) *) - current, (Some (Extend.Level (constr_level n)), None, None, None) - -let level_stack = - ref [(default_levels, default_pattern_levels)] - -let remove_levels n = - level_stack := List.skipn n !level_stack - -let rec list_mem_assoc_triple x = function - | [] -> false - | (a,b,c) :: l -> Int.equal a x || list_mem_assoc_triple x l - -type gram_level = - gram_position option * gram_assoc option * string option * - (** for reinitialization: *) gram_reinit option - -let top = function -| [] -> assert false -| h :: _ -> h - -let register_empty_levels forpat levels = - let rec filter accu = function - | [] -> ([], accu) - | n :: rem -> - let rem, accu = filter accu rem in - let (clev, plev) = top accu in - let levels = if forpat then plev else clev in - if not (list_mem_assoc_triple n levels) then - let nlev, ans = find_position_gen levels true None (Some n) in - let nlev = if forpat then (clev, nlev) else (nlev, plev) in - ans :: rem, nlev :: accu - else rem, accu - in - let ans, accu = filter !level_stack levels in - let () = level_stack := accu in - ans - -let find_position forpat assoc level = - let (clev, plev) = top !level_stack in - let levels = if forpat then plev else clev in - let nlev, ans = find_position_gen levels false assoc level in - let nlev = if forpat then (clev, nlev) else (nlev, plev) in - level_stack := nlev :: !level_stack; - ans - -(* Synchronise the stack of level updates *) -let synchronize_level_positions () = - let lev = top !level_stack in - level_stack := lev :: !level_stack - 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 @@ -605,7 +460,6 @@ let unfreeze (grams, lex) = let (undo, redo, common) = factorize_grams !grammar_stack grams in let n = number_of_entries undo in remove_grammars n; - remove_levels n; grammar_stack := common; CLexer.unfreeze lex; List.iter extend_dyn_grammar (List.rev_map pi2 redo) diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 98fc471332..1d076e2950 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -255,16 +255,3 @@ val recover_grammar_command : 'a grammar_command -> 'a list (** Recover the current stack of grammar extensions. *) val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b - -(** Registering/resetting the level of a constr entry *) - -type gram_level = - gram_position option * gram_assoc option * string option * gram_reinit option - -val find_position : - bool (** true if for creation in pattern entry; false if in constr entry *) -> - Extend.gram_assoc option -> int option -> gram_level - -val synchronize_level_positions : unit -> unit - -val register_empty_levels : bool -> int list -> gram_level list -- cgit v1.2.3 From 16d0e6f7cfc453944874cc1665a0eb4db8ded354 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 11 May 2016 15:33:47 +0200 Subject: Making the grammar command extend API purely functional. Instead of leaving the responsibility of extending the grammar to the caller, we ask for a list of extensions in the return value of the function. --- parsing/egramcoq.ml | 20 ++++++++++---------- parsing/pcoq.ml | 19 +++++++++++-------- parsing/pcoq.mli | 14 ++++++++++---- 3 files changed, 31 insertions(+), 22 deletions(-) (limited to 'parsing') diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 8af324d71b..21a9afa293 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -421,8 +421,8 @@ let target_to_bool : type r. r target -> bool = function let prepare_empty_levels forpat (pos,p4assoc,name,reinit) = let empty = (pos, [(name, p4assoc, [])]) in - if forpat then grammar_extend Constr.pattern reinit empty - else grammar_extend Constr.operconstr reinit empty + if forpat then ExtendRule (Constr.pattern, reinit, empty) + else ExtendRule (Constr.operconstr, reinit, empty) let rec pure_sublevels : type a b c. int option -> (a, b, c) rule -> int list = fun level r -> match r with | Stop -> [] @@ -456,7 +456,7 @@ let extend_constr state forpat ng = let n = ng.notgram_level in let assoc = ng.notgram_assoc in let (entry, level) = interp_constr_entry_key forpat n in - let fold (nb, state) pt = + let fold (accu, state) pt = let AnyTyRule r = make_ty_rule assoc n forpat pt in let symbs = ty_erase r in let pure_sublevels = pure_sublevels level symbs in @@ -464,14 +464,14 @@ let extend_constr state forpat ng = let needed_levels, state = register_empty_levels state isforpat pure_sublevels in let (pos,p4assoc,name,reinit), state = find_position state isforpat assoc level in let nb_decls = List.length needed_levels + 1 in - let () = List.iter (prepare_empty_levels isforpat) needed_levels in + let empty_rules = List.map (prepare_empty_levels isforpat) needed_levels in let empty = { constrs = []; constrlists = []; binders = [] } in let act = ty_eval r (make_act forpat ng.notgram_notation) empty in let rule = (name, p4assoc, [Rule (symbs, act)]) in - let () = grammar_extend entry reinit (pos, [rule]) in - (nb + nb_decls, state) + let r = ExtendRule (entry, reinit, (pos, [rule])) in + (accu @ empty_rules @ [r], state) in - List.fold_left fold (0, state) ng.notgram_prods + List.fold_left fold ([], state) ng.notgram_prods let constr_levels = GramState.field () @@ -481,11 +481,11 @@ let extend_constr_notation (_, ng) state = | Some lev -> lev in (* Add the notation in constr *) - let (nb, levels) = extend_constr levels ForConstr ng in + let (r, levels) = extend_constr levels ForConstr ng in (* Add the notation in cases_pattern *) - let (nb', levels) = extend_constr levels ForPattern ng in + let (r', levels) = extend_constr levels ForPattern ng in let state = GramState.set state constr_levels levels in - (nb + nb', state) + (r @ r', state) let constr_grammar : (Notation.level * notation_grammar) grammar_command = create_grammar_command "Notation" extend_constr_notation diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 1cc7b6c540..ae56c4723b 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -98,11 +98,11 @@ let of_coq_extend_statement (pos, st) = (** Type of reinitialization data *) type gram_reinit = gram_assoc * gram_position +type extend_rule = +| ExtendRule : 'a G.entry * gram_reinit option * 'a extend_statment -> extend_rule + type ext_kind = - | ByGrammar : - 'a G.entry - * gram_reinit option (** for reinitialization if ever needed *) - * 'a Extend.extend_statment -> ext_kind + | ByGrammar of extend_rule | ByEXTEND of (unit -> unit) * (unit -> unit) (** The list of extensions *) @@ -110,7 +110,7 @@ type ext_kind = let camlp4_state = ref [] let grammar_extend e reinit ext = - camlp4_state := ByGrammar (e,reinit,ext) :: !camlp4_state; + camlp4_state := ByGrammar (ExtendRule (e, reinit, ext)) :: !camlp4_state; let ext = of_coq_extend_statement ext in camlp4_verbose (maybe_uncurry (G.extend e)) ext @@ -167,7 +167,7 @@ let rec remove_grammars n = if n>0 then (match !camlp4_state with | [] -> anomaly ~label:"Pcoq.remove_grammars" (Pp.str "too many rules to remove") - | ByGrammar(g,reinit,ext)::t -> + | ByGrammar (ExtendRule (g, reinit, ext)) :: t -> grammar_delete g reinit (of_coq_extend_statement ext); camlp4_state := t; remove_grammars (n-1) @@ -405,7 +405,7 @@ let epsilon_value f e = module GramState = Store.Make(struct end) -type 'a grammar_extension = 'a -> GramState.t -> int * GramState.t +type 'a grammar_extension = 'a -> GramState.t -> extend_rule list * GramState.t module GrammarCommand = Dyn.Make(struct end) module GrammarInterp = struct type 'a t = 'a grammar_extension end @@ -428,7 +428,10 @@ let extend_grammar_command tag g = | [] -> GramState.empty | (_, _, st) :: _ -> st in - let (nb, st) = modify g grammar_state in + let (rules, st) = modify g grammar_state in + let iter (ExtendRule (e, reinit, ext)) = grammar_extend e reinit ext in + let () = List.iter iter rules in + let nb = List.length rules in grammar_stack := (nb, GrammarCommand.Dyn (tag, g), st) :: !grammar_stack let recover_grammar_command (type a) (tag : a grammar_command) : a list = diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 1d076e2950..ed82607dd2 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -241,12 +241,18 @@ type 'a grammar_command (** Type of synchronized parsing extensions. The ['a] type should be marshallable. *) -type 'a grammar_extension = 'a -> GramState.t -> int * GramState.t +type extend_rule = +| ExtendRule : 'a Gram.entry * gram_reinit option * 'a extend_statment -> extend_rule + +type 'a grammar_extension = 'a -> GramState.t -> extend_rule list * GramState.t +(** Grammar extension entry point. Given some ['a] and a current grammar state, + such a function must produce the list of grammar extensions that will be + applied in the same order and kept synchronized w.r.t. the summary, together + with a new state. It should be pure. *) val create_grammar_command : string -> 'a grammar_extension -> 'a grammar_command -(** Create a new grammar-modifying command with the given name. The function - should modify the parser state and return the number of grammar extensions - performed. *) +(** Create a new grammar-modifying command with the given name. The extension + function is called to generate the rules for a given data. *) val extend_grammar_command : 'a grammar_command -> 'a -> unit (** Extend the grammar of Coq with the given data. *) -- cgit v1.2.3 From 9acfdfd9b7d1cae34b97a4c06c52c4646e15589b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 11 May 2016 18:57:53 +0200 Subject: The grammar_extend function now registers unsynchronized extensions. This made little sense, as all the uses of this function were actually called from toplevel ML modules. This was at best useless, and at worst a source of bugs when loading plugins and messing with backtracking. --- parsing/pcoq.ml | 20 ++++++++++++++------ parsing/pcoq.mli | 23 ++++++++++++----------- 2 files changed, 26 insertions(+), 17 deletions(-) (limited to 'parsing') diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index ae56c4723b..efb89cd6e1 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -109,11 +109,6 @@ type ext_kind = let camlp4_state = ref [] -let grammar_extend e reinit ext = - camlp4_state := ByGrammar (ExtendRule (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) = @@ -132,6 +127,19 @@ let grammar_delete e reinit (pos,rls) = maybe_uncurry (G.extend e) (Some ext, [Some lev,Some a,[]]) | None -> () +(** Extension *) + +let grammar_extend e reinit ext = + let ext = of_coq_extend_statement ext in + let undo () = grammar_delete e reinit ext in + let redo () = camlp4_verbose (maybe_uncurry (G.extend e)) ext in + camlp4_state := ByEXTEND (undo, redo) :: !camlp4_state; + redo () + +let grammar_extend_sync e reinit ext = + camlp4_state := ByGrammar (ExtendRule (e, reinit, ext)) :: !camlp4_state; + camlp4_verbose (maybe_uncurry (G.extend e)) (of_coq_extend_statement ext) + (** The apparent parser of Coq; encapsulate G to keep track of the extensions. *) @@ -429,7 +437,7 @@ let extend_grammar_command tag g = | (_, _, st) :: _ -> st in let (rules, st) = modify g grammar_state in - let iter (ExtendRule (e, reinit, ext)) = grammar_extend e reinit ext in + let iter (ExtendRule (e, reinit, ext)) = grammar_extend_sync e reinit ext in let () = List.iter iter rules in let nb = List.length rules in grammar_stack := (nb, GrammarCommand.Dyn (tag, g), st) :: !grammar_stack diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index ed82607dd2..319ca256e1 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -96,16 +96,6 @@ module Gram : module type of Compat.GrammarMake(CLexer) *) -(** {5 Grammar extension API} *) - -(** Type of reinitialization data *) -type gram_reinit = gram_assoc * gram_position - -val grammar_extend : - 'a Gram.entry -> - gram_reinit option (** for reinitialization if ever needed *) -> - 'a Extend.extend_statment -> unit - (** Temporary activate camlp4 verbosity *) val camlp4_verbosity : bool -> ('a -> unit) -> 'a -> unit @@ -232,7 +222,18 @@ val set_command_entry : vernac_expr Gram.entry -> unit val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option -(** {5 Extending the parser with Summary-synchronized commands} *) +(** {5 Extending the parser without synchronization} *) + +type gram_reinit = gram_assoc * gram_position +(** Type of reinitialization data *) + +val grammar_extend : 'a Gram.entry -> gram_reinit option -> + 'a Extend.extend_statment -> unit +(** Extend the grammar of Coq, without synchronizing it with the bactracking + mechanism. This means that grammar extensions defined this way will survive + an undo. *) + +(** {5 Extending the parser with summary-synchronized commands} *) module GramState : Store.S (** Auxilliary state of the grammar. Any added data must be marshallable. *) -- cgit v1.2.3