From 1d0eb5d4d6fea88abc29798ee2004b2e27e952c6 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 8 Mar 2017 03:22:22 +0100 Subject: [camlpX] Remove camlp4 compat layer. We remove the camlp4 compatibility layer, and try to clean up most structures. `parsing/compat` is gone. We added some documentation to the lexer/parser interfaces that are often obscured by module includes. --- parsing/pcoq.ml | 228 +++++++++++++++++++++++++++++++++++++++++++++++++------- 1 file changed, 200 insertions(+), 28 deletions(-) (limited to 'parsing/pcoq.ml') diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index b8405ca8c..92d249e53 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -7,31 +7,203 @@ (************************************************************************) open Pp -open Compat open CErrors open Util open Extend open Genarg +let curry f x y = f (x, y) +let uncurry f (x,y) = f x y + +(** Location Utils *) +let to_coqloc loc = + { Loc.fname = Ploc.file_name loc; + Loc.line_nb = Ploc.line_nb loc; + Loc.bol_pos = Ploc.bol_pos loc; + Loc.bp = Ploc.first_pos loc; + Loc.ep = Ploc.last_pos loc; + Loc.line_nb_last = Ploc.line_nb_last loc; + Loc.bol_pos_last = Ploc.bol_pos_last loc; } + +let (!@) = to_coqloc + (** The parser of Coq *) +module G : sig + + include Grammar.S with type te = Tok.t + +(* where Grammar.S + +module type S = + sig + type te = 'x; + type parsable = 'x; + value parsable : Stream.t char -> parsable; + value tokens : string -> list (string * int); + value glexer : Plexing.lexer te; + value set_algorithm : parse_algorithm -> unit; + module Entry : + sig + type e 'a = 'y; + value create : string -> e 'a; + value parse : e 'a -> parsable -> 'a; + value parse_token : e 'a -> Stream.t te -> 'a; + value name : e 'a -> string; + value of_parser : string -> (Stream.t te -> 'a) -> e 'a; + value print : Format.formatter -> e 'a -> unit; + external obj : e 'a -> Gramext.g_entry te = "%identity"; + end + ; + module Unsafe : + sig + value gram_reinit : Plexing.lexer te -> unit; + value clear_entry : Entry.e 'a -> unit; + end + ; + value extend : + Entry.e 'a -> option Gramext.position -> + list + (option string * option Gramext.g_assoc * + list (list (Gramext.g_symbol te) * Gramext.g_action)) -> + unit; + value delete_rule : Entry.e 'a -> list (Gramext.g_symbol te) -> unit; + end + *) + + type 'a entry = 'a Entry.e + 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:string -> 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 with_parsable : coq_parsable -> ('a -> 'b) -> 'a -> 'b + 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) + + type 'a entry = 'a Entry.e + 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 c = + let state = ref (CLexer.init_lexer_state file) in + CLexer.set_lexer_state !state; + let a = parsable c in + state := CLexer.release_lexer_state (); + (a,state) + + let action = Gramext.action + let entry_create = Entry.create + + let entry_parse e (p,state) = + CLexer.set_lexer_state !state; + try + let c = Entry.parse e p in + state := CLexer.release_lexer_state (); + c + with Ploc.Exc (loc,e) -> + CLexer.drop_lexer_state (); + let loc' = Loc.get_loc (Exninfo.info e) in + let loc = match loc' with None -> to_coqloc loc | Some loc -> loc in + Loc.raise ~loc e + + let with_parsable (p,state) f x = + CLexer.set_lexer_state !state; + try + let a = f x in + state := CLexer.release_lexer_state (); + a + with e -> + CLexer.drop_lexer_state (); + raise e + + 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 G = GrammarMake (CLexer) -let warning_verbose = Compat.warning_verbose +let warning_verbose = Gramext.warning_verbose let of_coq_assoc = function -| Extend.RightA -> CompatGramext.RightA -| Extend.LeftA -> CompatGramext.LeftA -| Extend.NonA -> CompatGramext.NonA +| Extend.RightA -> Gramext.RightA +| Extend.LeftA -> Gramext.LeftA +| Extend.NonA -> Gramext.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 +| 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 + +module Symbols : sig + val stoken : Tok.t -> G.symbol + val sself : G.symbol + val snext : G.symbol + val slist0 : G.symbol -> G.symbol + val slist0sep : G.symbol * G.symbol -> G.symbol + val slist1 : G.symbol -> G.symbol + val slist1sep : G.symbol * G.symbol -> G.symbol + val sopt : G.symbol -> G.symbol + val snterml : G.internal_entry * string -> G.symbol + val snterm : G.internal_entry -> G.symbol + val snterml_level : G.symbol -> string +end = struct + + let stoken tok = + let pattern = match tok with + | Tok.KEYWORD s -> "", s + | Tok.IDENT s -> "IDENT", s + | Tok.PATTERNIDENT s -> "PATTERNIDENT", s + | Tok.FIELD s -> "FIELD", s + | Tok.INT s -> "INT", s + | Tok.STRING s -> "STRING", s + | Tok.LEFTQMARK -> "LEFTQMARK", "" + | Tok.BULLET s -> "BULLET", s + | Tok.EOI -> "EOI", "" + in + Gramext.Stoken pattern + + let slist0sep (x, y) = Gramext.Slist0sep (x, y, false) + let slist1sep (x, y) = Gramext.Slist1sep (x, y, false) + + let snterml (x, y) = Gramext.Snterml (x, y) + let snterm x = Gramext.Snterm x + let sself = Gramext.Sself + let snext = Gramext.Snext + let slist0 x = Gramext.Slist0 x + let slist1 x = Gramext.Slist1 x + let sopt x = Gramext.Sopt x -module Symbols = GramextMake(G) + let snterml_level = function + | Gramext.Snterml (_, l) -> l + | _ -> failwith "snterml_level" + +end let camlp4_verbosity silent f x = let a = !warning_verbose in @@ -55,7 +227,7 @@ let camlp4_verbose f x = camlp4_verbosity (Flags.is_verbose ()) f x (** 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)) +| Stop -> fun f -> G.action (fun loc -> f (!@ 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 @@ -121,10 +293,10 @@ let grammar_delete e reinit (pos,rls) = let a = of_coq_assoc a in let ext = of_coq_position ext in let lev = match pos with - | Some (CompatGramext.Level n) -> n + | Some (Gramext.Level n) -> n | _ -> assert false in - maybe_uncurry (G.extend e) (Some ext, [Some lev,Some a,[]]) + (G.extend e) (Some ext) [Some lev,Some a,[]] | None -> () (** Extension *) @@ -132,13 +304,13 @@ let grammar_delete e reinit (pos,rls) = 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_verbosity false (maybe_uncurry (G.extend e)) ext in + let redo () = camlp4_verbosity false (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_verbosity false (maybe_uncurry (G.extend e)) (of_coq_extend_statement ext) + camlp4_verbosity false (uncurry (G.extend e)) (of_coq_extend_statement ext) (** The apparent parser of Coq; encapsulate G to keep track of the extensions. *) @@ -147,13 +319,13 @@ module Gram = struct include G let extend e = - maybe_curry + curry (fun ext -> camlp4_state := (ByEXTEND ((fun () -> grammar_delete e None ext), - (fun () -> maybe_uncurry (G.extend e) ext))) + (fun () -> uncurry (G.extend e) ext))) :: !camlp4_state; - maybe_uncurry (G.extend e) ext) + uncurry (G.extend e) ext) let delete_rule e pil = (* spiwack: if you use load an ML module which contains GDELETE_RULE in a section, God kills a kitty. As it would corrupt remove_grammars. @@ -194,14 +366,14 @@ let eoi_entry en = let e = Gram.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 - maybe_uncurry (Gram.extend e) (None, make_rule [symbs, act]); + 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 symbs = [Symbols.snterm (Gram.Entry.obj en)] in let act = Gram.action (fun x loc -> f x) in - maybe_uncurry (Gram.extend e) (None, make_rule [symbs, act]); + uncurry (Gram.extend e) (None, make_rule [symbs, act]); e (* Parse a string, does NOT check if the entire string was read @@ -345,13 +517,13 @@ module Vernac_ = let noedit_mode = gec_vernac "noedit_command" let () = - let act_vernac = Gram.action (fun v loc -> Some (!@loc, v)) in + 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) ], act_vernac ); ] in - maybe_uncurry (Gram.extend main_entry) (None, make_rule rule) + uncurry (Gram.extend main_entry) (None, make_rule rule) let command_entry_ref = ref noedit_mode let command_entry = @@ -369,7 +541,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 (G.extend entry) ext in + let () = uncurry (G.extend entry) ext in try Some (parse_string entry "") with _ -> None (** Synchronized grammar extensions *) @@ -418,9 +590,9 @@ let extend_dyn_grammar (GrammarCommand.Dyn (tag, g)) = extend_grammar_command ta (* 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.frozen_t +type frozen_t = (int * GrammarCommand.t * GramState.t) list * CLexer.keyword_state -let freeze _ : frozen_t = (!grammar_stack, CLexer.freeze ()) +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 *) @@ -435,7 +607,7 @@ let unfreeze (grams, lex) = let n = number_of_entries undo in remove_grammars n; grammar_stack := common; - CLexer.unfreeze lex; + CLexer.set_keyword_state lex; List.iter extend_dyn_grammar (List.rev_map pi2 redo) (** No need to provide an init function : the grammar state is -- cgit v1.2.3