From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- parsing/pcoq.ml | 299 +++++++++++++++++++++++++++++++------------------------- 1 file changed, 165 insertions(+), 134 deletions(-) (limited to 'parsing/pcoq.ml') diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 258c4bb1..eb3e6338 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -17,9 +17,17 @@ let curry f x y = f (x, y) let uncurry f (x,y) = f x y (** Location Utils *) +let ploc_file_of_coq_file = function +| Loc.ToplevelInput -> "" +| Loc.InFile f -> f + let coq_file_of_ploc_file s = if s = "" then Loc.ToplevelInput else Loc.InFile s +let of_coqloc loc = + let open Loc in + Ploc.make_loc (ploc_file_of_coq_file loc.fname) loc.line_nb loc.bol_pos (loc.bp, loc.ep) "" + let to_coqloc loc = { Loc.fname = coq_file_of_ploc_file (Ploc.file_name loc); Loc.line_nb = Ploc.line_nb loc; @@ -78,24 +86,15 @@ module type S = type internal_entry = Tok.t Gramext.g_entry type symbol = Tok.t Gramext.g_symbol type action = Gramext.g_action - type production_rule = symbol list * action - type single_extend_statment = - string option * Gramext.g_assoc option * production_rule list - type extend_statment = - Gramext.position option * single_extend_statment list type coq_parsable - val parsable : ?file:Loc.source -> char Stream.t -> coq_parsable + val coq_parsable : ?file:Loc.source -> char Stream.t -> coq_parsable val action : 'a -> action val entry_create : string -> 'a entry val entry_parse : 'a entry -> coq_parsable -> 'a - val entry_print : Format.formatter -> 'a entry -> unit val comment_state : coq_parsable -> ((int * int) * string) list - val srules' : production_rule list -> symbol - val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a - end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct include Grammar.GMake(CLexer) @@ -104,15 +103,10 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct type internal_entry = Tok.t Gramext.g_entry type symbol = Tok.t Gramext.g_symbol type action = Gramext.g_action - type production_rule = symbol list * action - type single_extend_statment = - string option * Gramext.g_assoc option * production_rule list - type extend_statment = - Gramext.position option * single_extend_statment list type coq_parsable = parsable * CLexer.lexer_state ref - let parsable ?(file=Loc.ToplevelInput) c = + let coq_parsable ?(file=Loc.ToplevelInput) c = let state = ref (CLexer.init_lexer_state file) in CLexer.set_lexer_state !state; let a = parsable c in @@ -137,14 +131,25 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct let comment_state (p,state) = CLexer.get_comment_state !state - let entry_print ft x = Entry.print ft x - - (* Not used *) - let srules' = Gramext.srules - let parse_tokens_after_filter = Entry.parse_token +end +module Parsable = +struct + type t = G.coq_parsable + let make = G.coq_parsable + let comment_state = G.comment_state end +module Entry = +struct + + type 'a t = 'a Grammar.GMake(CLexer).Entry.e + + let create = G.Entry.create + let parse = G.entry_parse + let print = G.Entry.print + +end let warning_verbose = Gramext.warning_verbose @@ -208,9 +213,9 @@ let camlp5_verbosity silent f x = (** Grammar extensions *) -(** NB: [extend_statment = - gram_position option * single_extend_statment list] - and [single_extend_statment = +(** NB: [extend_statement = + gram_position option * single_extend_statement list] + and [single_extend_statement = string option * gram_assoc option * production_rule list] and [production_rule = symbol list * action] @@ -237,9 +242,9 @@ let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> _ = function | Aentry e -> Symbols.snterm (G.Entry.obj e) | Aentryl (e, n) -> - Symbols.snterml (G.Entry.obj e, string_of_int n) + Symbols.snterml (G.Entry.obj e, n) | Arules rs -> - G.srules' (List.map symbol_of_rules rs) + Gramext.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 @@ -264,16 +269,23 @@ let of_coq_extend_statement (pos, st) = type gram_reinit = gram_assoc * gram_position type extend_rule = -| ExtendRule : 'a G.entry * gram_reinit option * 'a extend_statment -> extend_rule +| ExtendRule : 'a G.entry * gram_reinit option * 'a extend_statement -> extend_rule + +module EntryCommand = Dyn.Make () +module EntryData = struct type _ t = Ex : 'b G.entry String.Map.t -> ('a * 'b) t end +module EntryDataMap = EntryCommand.Map(EntryData) type ext_kind = | ByGrammar of extend_rule | ByEXTEND of (unit -> unit) * (unit -> unit) + | ByEntry : ('a * 'b) EntryCommand.tag * string * 'b G.entry -> ext_kind (** The list of extensions *) let camlp5_state = ref [] +let camlp5_entries = ref EntryDataMap.empty + (** Deletion *) let grammar_delete e reinit (pos,rls) = @@ -329,6 +341,7 @@ module Gram = I'm not entirely sure it makes sense, but at least it would be more correct. *) G.delete_rule e pil + let gram_extend e ext = grammar_extend e None ext end (** Remove extensions @@ -338,7 +351,7 @@ module Gram = let rec remove_grammars n = if n>0 then - (match !camlp5_state with + match !camlp5_state with | [] -> anomaly ~label:"Pcoq.remove_grammars" (Pp.str "too many rules to remove.") | ByGrammar (ExtendRule (g, reinit, ext)) :: t -> grammar_delete g reinit (of_coq_extend_statement ext); @@ -349,21 +362,31 @@ let rec remove_grammars n = camlp5_state := t; remove_grammars n; redo(); - camlp5_state := ByEXTEND (undo,redo) :: !camlp5_state) + camlp5_state := ByEXTEND (undo,redo) :: !camlp5_state + | ByEntry (tag, name, e) :: t -> + G.Unsafe.clear_entry e; + camlp5_state := t; + let EntryData.Ex entries = + try EntryDataMap.find tag !camlp5_entries + with Not_found -> EntryData.Ex String.Map.empty + in + let entries = String.Map.remove name entries in + camlp5_entries := EntryDataMap.add tag (EntryData.Ex entries) !camlp5_entries; + remove_grammars (n - 1) let make_rule r = [None, None, r] (** An entry that checks we reached the end of the input. *) let eoi_entry en = - let e = Gram.entry_create ((Gram.Entry.name en) ^ "_eoi") in + let e = Entry.create ((Gram.Entry.name en) ^ "_eoi") in let symbs = [Symbols.snterm (Gram.Entry.obj en); Symbols.stoken Tok.EOI] in let act = Gram.action (fun _ x loc -> x) in uncurry (Gram.extend e) (None, make_rule [symbs, act]); e let map_entry f en = - let e = Gram.entry_create ((Gram.Entry.name en) ^ "_map") in + let e = Entry.create ((Gram.Entry.name en) ^ "_map") in let symbs = [Symbols.snterm (Gram.Entry.obj en)] in let act = Gram.action (fun x loc -> f x) in uncurry (Gram.extend e) (None, make_rule [symbs, act]); @@ -373,7 +396,7 @@ let map_entry f en = (use eoi_entry) *) let parse_string f x = - let strm = Stream.of_string x in Gram.entry_parse f (Gram.parsable strm) + let strm = Stream.of_string x in Gram.entry_parse f (Gram.coq_parsable strm) type gram_universe = string @@ -387,7 +410,6 @@ let create_universe u = let uprim = create_universe "prim" let uconstr = create_universe "constr" let utactic = create_universe "tactic" -let uvernac = create_universe "vernac" let get_univ u = if Hashtbl.mem utables u then u @@ -395,14 +417,14 @@ let get_univ u = let new_entry u s = let ename = u ^ ":" ^ s in - let e = Gram.entry_create ename in + let e = Entry.create ename in e let make_gen_entry u s = new_entry u s module GrammarObj = struct - type ('r, _, _) obj = 'r Gram.entry + type ('r, _, _) obj = 'r Entry.t let name = "grammar" let default _ = None end @@ -412,7 +434,7 @@ module Grammar = Register(GrammarObj) let register_grammar = Grammar.register0 let genarg_grammar = Grammar.obj -let create_generic_entry (type a) u s (etyp : a raw_abstract_argument_type) : a Gram.entry = +let create_generic_entry (type a) u s (etyp : a raw_abstract_argument_type) : a Entry.t = let e = new_entry u s in let Rawwit t = etyp in let () = Grammar.register0 t e in @@ -424,38 +446,38 @@ module Prim = struct let gec_gen n = make_gen_entry uprim n - (* Entries that can be referred via the string -> Gram.entry table *) + (* Entries that can be referred via the string -> Entry.t table *) (* Typically for tactic or vernac extensions *) let preident = gec_gen "preident" let ident = gec_gen "ident" let natural = gec_gen "natural" let integer = gec_gen "integer" - let bigint = Gram.entry_create "Prim.bigint" + let bigint = Entry.create "Prim.bigint" let string = gec_gen "string" - let lstring = Gram.entry_create "Prim.lstring" + let lstring = Entry.create "Prim.lstring" let reference = make_gen_entry uprim "reference" - let by_notation = Gram.entry_create "by_notation" - let smart_global = Gram.entry_create "smart_global" + let by_notation = Entry.create "by_notation" + let smart_global = Entry.create "smart_global" (* parsed like ident but interpreted as a term *) let var = gec_gen "var" - let name = Gram.entry_create "Prim.name" - let identref = Gram.entry_create "Prim.identref" - let univ_decl = Gram.entry_create "Prim.univ_decl" - let ident_decl = Gram.entry_create "Prim.ident_decl" - let pattern_ident = Gram.entry_create "pattern_ident" - let pattern_identref = Gram.entry_create "pattern_identref" + let name = Entry.create "Prim.name" + let identref = Entry.create "Prim.identref" + let univ_decl = Entry.create "Prim.univ_decl" + let ident_decl = Entry.create "Prim.ident_decl" + let pattern_ident = Entry.create "pattern_ident" + let pattern_identref = Entry.create "pattern_identref" (* A synonym of ident - maybe ident will be located one day *) - let base_ident = Gram.entry_create "Prim.base_ident" + let base_ident = Entry.create "Prim.base_ident" - let qualid = Gram.entry_create "Prim.qualid" - let fullyqualid = Gram.entry_create "Prim.fullyqualid" - let dirpath = Gram.entry_create "Prim.dirpath" + let qualid = Entry.create "Prim.qualid" + let fullyqualid = Entry.create "Prim.fullyqualid" + let dirpath = Entry.create "Prim.dirpath" - let ne_string = Gram.entry_create "Prim.ne_string" - let ne_lstring = Gram.entry_create "Prim.ne_lstring" + let ne_string = Entry.create "Prim.ne_string" + let ne_lstring = Entry.create "Prim.ne_lstring" end @@ -463,7 +485,7 @@ module Constr = struct let gec_constr = make_gen_entry uconstr - (* Entries that can be referred via the string -> Gram.entry table *) + (* Entries that can be referred via the string -> Entry.t table *) let constr = gec_constr "constr" let operconstr = gec_constr "operconstr" let constr_eoi = eoi_entry constr @@ -474,67 +496,29 @@ module Constr = let universe_level = make_gen_entry uconstr "universe_level" let sort = make_gen_entry uconstr "sort" let sort_family = make_gen_entry uconstr "sort_family" - let pattern = Gram.entry_create "constr:pattern" + let pattern = Entry.create "constr:pattern" let constr_pattern = gec_constr "constr_pattern" let lconstr_pattern = gec_constr "lconstr_pattern" - let closed_binder = Gram.entry_create "constr:closed_binder" - let binder = Gram.entry_create "constr:binder" - let binders = Gram.entry_create "constr:binders" - let open_binders = Gram.entry_create "constr:open_binders" - let binders_fixannot = Gram.entry_create "constr:binders_fixannot" - let typeclass_constraint = Gram.entry_create "constr:typeclass_constraint" - let record_declaration = Gram.entry_create "constr:record_declaration" - let appl_arg = Gram.entry_create "constr:appl_arg" + let closed_binder = Entry.create "constr:closed_binder" + let binder = Entry.create "constr:binder" + let binders = Entry.create "constr:binders" + let open_binders = Entry.create "constr:open_binders" + let binders_fixannot = Entry.create "constr:binders_fixannot" + let typeclass_constraint = Entry.create "constr:typeclass_constraint" + let record_declaration = Entry.create "constr:record_declaration" + let appl_arg = Entry.create "constr:appl_arg" end module Module = struct - let module_expr = Gram.entry_create "module_expr" - let module_type = Gram.entry_create "module_type" + let module_expr = Entry.create "module_expr" + let module_type = Entry.create "module_type" end -module Vernac_ = - struct - let gec_vernac s = Gram.entry_create ("vernac:" ^ s) - - (* The different kinds of vernacular commands *) - let gallina = gec_vernac "gallina" - let gallina_ext = gec_vernac "gallina_ext" - let command = gec_vernac "command" - let syntax = gec_vernac "syntax_command" - let vernac_control = gec_vernac "Vernac.vernac_control" - let rec_definition = gec_vernac "Vernac.rec_definition" - let red_expr = make_gen_entry utactic "red_expr" - let hint_info = gec_vernac "hint_info" - (* Main vernac entry *) - let main_entry = Gram.entry_create "vernac" - let noedit_mode = gec_vernac "noedit_command" - - let () = - let act_vernac = Gram.action (fun v loc -> Some (to_coqloc loc, v)) in - let act_eoi = Gram.action (fun _ loc -> None) in - let rule = [ - ([ Symbols.stoken Tok.EOI ], act_eoi); - ([ Symbols.snterm (Gram.Entry.obj vernac_control) ], act_vernac ); - ] in - uncurry (Gram.extend main_entry) (None, make_rule rule) - - let command_entry_ref = ref noedit_mode - let command_entry = - Gram.Entry.of_parser "command_entry" - (fun strm -> Gram.parse_tokens_after_filter !command_entry_ref strm) - - end - -let main_entry = Vernac_.main_entry - -let set_command_entry e = Vernac_.command_entry_ref := e -let get_command_entry () = !Vernac_.command_entry_ref - 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 entry = Gram.entry_create "epsilon" in let () = uncurry (G.extend entry) ext in try Some (parse_string entry "") with _ -> None @@ -550,59 +534,119 @@ module GrammarInterpMap = GrammarCommand.Map(GrammarInterp) let grammar_interp = ref GrammarInterpMap.empty -let (grammar_stack : (int * GrammarCommand.t * GramState.t) list ref) = ref [] +type ('a, 'b) entry_extension = 'a -> GramState.t -> string list * GramState.t + +module EntryInterp = struct type _ t = Ex : ('a, 'b) entry_extension -> ('a * 'b) t end +module EntryInterpMap = EntryCommand.Map(EntryInterp) + +let entry_interp = ref EntryInterpMap.empty + +type grammar_entry = +| GramExt of int * GrammarCommand.t +| EntryExt : int * ('a * 'b) EntryCommand.tag * 'a -> grammar_entry + +let (grammar_stack : (grammar_entry * GramState.t) list ref) = ref [] type 'a grammar_command = 'a GrammarCommand.tag +type ('a, 'b) entry_command = ('a * 'b) EntryCommand.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 create_entry_command name (interp : ('a, 'b) entry_extension) : ('a, 'b) entry_command = + let obj = EntryCommand.create name in + let () = entry_interp := EntryInterpMap.add obj (EntryInterp.Ex interp) !entry_interp in + obj + let extend_grammar_command tag g = let modify = GrammarInterpMap.find tag !grammar_interp in let grammar_state = match !grammar_stack with | [] -> GramState.empty - | (_, _, st) :: _ -> st + | (_, st) :: _ -> st in let (rules, st) = modify g grammar_state 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 + grammar_stack := (GramExt (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), _) -> - match GrammarCommand.eq tag tag' with - | None -> None - | Some Refl -> Some v +let extend_entry_command (type a) (type b) (tag : (a, b) entry_command) (g : a) : b Gram.entry list = + let EntryInterp.Ex modify = EntryInterpMap.find tag !entry_interp in + let grammar_state = match !grammar_stack with + | [] -> GramState.empty + | (_, st) :: _ -> st + in + let (names, st) = modify g grammar_state in + let entries = List.map (fun name -> Gram.entry_create name) names in + let iter name e = + camlp5_state := ByEntry (tag, name, e) :: !camlp5_state; + let EntryData.Ex old = + try EntryDataMap.find tag !camlp5_entries + with Not_found -> EntryData.Ex String.Map.empty + in + let entries = String.Map.add name e old in + camlp5_entries := EntryDataMap.add tag (EntryData.Ex entries) !camlp5_entries in - List.map_filter filter !grammar_stack + let () = List.iter2 iter names entries in + let nb = List.length entries in + let () = grammar_stack := (EntryExt (nb, tag, g), st) :: !grammar_stack in + entries + +let find_custom_entry tag name = + let EntryData.Ex map = EntryDataMap.find tag !camlp5_entries in + String.Map.find name map + +let extend_dyn_grammar (e, _) = match e with +| GramExt (_, (GrammarCommand.Dyn (tag, g))) -> extend_grammar_command tag g +| EntryExt (_, tag, g) -> ignore (extend_entry_command tag g) + +(** Registering extra grammar *) -let extend_dyn_grammar (GrammarCommand.Dyn (tag, g)) = extend_grammar_command tag g +type any_entry = AnyEntry : 'a Gram.entry -> any_entry + +let grammar_names : any_entry list String.Map.t ref = ref String.Map.empty -(* Summary functions: the state of the lexer is included in that of the parser. +let register_grammars_by_name name grams = + grammar_names := String.Map.add name grams !grammar_names + +let find_grammars_by_name name = + try String.Map.find name !grammar_names + with Not_found -> + let fold (EntryDataMap.Any (tag, EntryData.Ex map)) accu = + try AnyEntry (String.Map.find name map) :: accu + with Not_found -> accu + in + EntryDataMap.fold fold !camlp5_entries [] + +(** 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 * GramState.t) list * CLexer.keyword_state +type frozen_t = + (grammar_entry * GramState.t) list * + CLexer.keyword_state -let freeze _ : frozen_t = (!grammar_stack, CLexer.get_keyword_state ()) +let freeze _ : frozen_t = + (!grammar_stack, CLexer.get_keyword_state ()) (* 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 rec number_of_entries accu = function +| [] -> accu +| ((GramExt (p, _) | EntryExt (p, _, _)), _) :: rem -> + number_of_entries (p + accu) rem let unfreeze (grams, lex) = let (undo, redo, common) = factorize_grams !grammar_stack grams in - let n = number_of_entries undo in + let n = number_of_entries 0 undo in remove_grammars n; grammar_stack := common; CLexer.set_keyword_state lex; - List.iter extend_dyn_grammar (List.rev_map pi2 redo) + List.iter extend_dyn_grammar (List.rev redo) (** No need to provide an init function : the grammar state is statically available, and already empty initially, while @@ -635,17 +679,4 @@ let () = Grammar.register0 wit_ref (Prim.reference); Grammar.register0 wit_sort_family (Constr.sort_family); Grammar.register0 wit_constr (Constr.constr); - Grammar.register0 wit_red_expr (Vernac_.red_expr); () - -(** Registering extra grammar *) - -type any_entry = AnyEntry : 'a Gram.entry -> any_entry - -let grammar_names : any_entry list String.Map.t ref = ref String.Map.empty - -let register_grammars_by_name name grams = - grammar_names := String.Map.add name grams !grammar_names - -let find_grammars_by_name name = - String.Map.find name !grammar_names -- cgit v1.2.3