diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/cLexer.ml | 65 | ||||
| -rw-r--r-- | parsing/extend.ml | 21 | ||||
| -rw-r--r-- | parsing/notation_gram.ml | 2 | ||||
| -rw-r--r-- | parsing/pcoq.ml | 100 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 14 | ||||
| -rw-r--r-- | parsing/tok.mli | 1 |
6 files changed, 64 insertions, 139 deletions
diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml index d81ee475b5..c2b7fa117d 100644 --- a/parsing/cLexer.ml +++ b/parsing/cLexer.ml @@ -13,28 +13,6 @@ open Util open Tok open Gramlib -(** Location utilities *) -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 from_coqloc fname line_nb bol_pos bp ep = - Ploc.make_loc (ploc_file_of_coq_file fname) line_nb bol_pos (bp, ep) "" - -let to_coqloc loc = - { Loc.fname = coq_file_of_ploc_file (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 - (* Dictionaries: trees annotated with string options, each node being a map from chars to dictionaries (the subtrees). A trie, in other words. *) @@ -128,18 +106,22 @@ module Error = struct end open Error -let err loc str = Loc.raise ~loc:(to_coqloc loc) (Error.E str) +let err loc str = Loc.raise ~loc (Error.E str) let bad_token str = raise (Error.E (Bad_token str)) (* Update a loc without allocating an intermediate pair *) let set_loc_pos loc bp ep = - Ploc.sub loc (bp - Ploc.first_pos loc) (ep - bp) + Ploc.sub loc (bp - loc.Loc.bp) (ep - bp) (* Increase line number by 1 and update position of beginning of line *) let bump_loc_line loc bol_pos = - Ploc.make_loc (Ploc.file_name loc) (Ploc.line_nb loc + 1) bol_pos - (Ploc.first_pos loc, Ploc.last_pos loc) (Ploc.comment loc) + Loc.{ loc with + line_nb = loc.line_nb + 1; + line_nb_last = loc.line_nb + 1; + bol_pos; + bol_pos_last = bol_pos; + } (* Same as [bump_loc_line], but for the last line in location *) (* For an obscure reason, camlp5 does not give an easy way to set line_nb_stop, @@ -147,19 +129,25 @@ let bump_loc_line loc bol_pos = (* Warning: [bump_loc_line_last] changes the end position. You may need to call [set_loc_pos] to fix it. *) let bump_loc_line_last loc bol_pos = - let loc' = - Ploc.make_loc (Ploc.file_name loc) (Ploc.line_nb_last loc + 1) bol_pos - (Ploc.first_pos loc + 1, Ploc.last_pos loc + 1) (Ploc.comment loc) - in - Ploc.encl loc loc' + let open Loc in + let loc' = { loc with + line_nb = loc.line_nb_last + 1; + line_nb_last = loc.line_nb_last + 1; + bol_pos; + bol_pos_last = bol_pos; + bp = loc.bp + 1; + ep = loc.ep + 1; + } in + Loc.merge loc loc' (* For some reason, the [Ploc.after] function of Camlp5 does not update line numbers, so we define our own function that does it. *) let after loc = - let line_nb = Ploc.line_nb_last loc in - let bol_pos = Ploc.bol_pos_last loc in - Ploc.make_loc (Ploc.file_name loc) line_nb bol_pos - (Ploc.last_pos loc, Ploc.last_pos loc) (Ploc.comment loc) + Loc.{ loc with + line_nb = loc.line_nb_last; + bol_pos = loc.bol_pos_last; + bp = loc.ep; + } (** Lexer conventions on tokens *) @@ -324,7 +312,7 @@ let rec ident_tail loc len s = match Stream.peek s with | Utf8Token (st, n) when Unicode.is_unknown st -> let id = get_buff len in let u = String.concat "" (List.map (String.make 1) (Stream.npeek n s)) in - warn_unrecognized_unicode ~loc:!@loc (u,id); len + warn_unrecognized_unicode ~loc (u,id); len | _ -> len let rec number len s = match Stream.peek s with @@ -368,7 +356,7 @@ let rec string loc ~comm_level bp len s = match Stream.peek s with Stream.junk s; let () = match comm_level with | Some 0 -> - warn_comment_terminator_in_string ~loc:!@loc () + warn_comment_terminator_in_string ~loc () | _ -> () in let comm_level = Option.map pred comm_level in @@ -757,7 +745,7 @@ let token_text = function let func cs = let loct = loct_create () in - let cur_loc = ref (from_coqloc !current_file 1 0 0 0) in + let cur_loc = ref (Loc.create !current_file 1 0 0 0) in let ts = Stream.from (fun i -> @@ -775,7 +763,6 @@ let lexer = { | _ -> ()); Plexing.tok_removing = (fun _ -> ()); Plexing.tok_match = Tok.match_pattern; - Plexing.tok_comm = None; Plexing.tok_text = token_text } (** Terminal symbols interpretation *) diff --git a/parsing/extend.ml b/parsing/extend.ml index 5caeab535a..9b5537d7f6 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -14,17 +14,8 @@ type 'a entry = 'a Gramlib.Grammar.GMake(CLexer).Entry.e type side = Left | Right -type gram_assoc = NonA | RightA | LeftA - -type gram_position = - | First - | Last - | Before of string - | After of string - | Level of string - type production_position = - | BorderProd of side * gram_assoc option + | BorderProd of side * Gramlib.Gramext.g_assoc option | InternalProd type production_level = @@ -115,12 +106,12 @@ type 'a production_rule = type 'a single_extend_statement = string option * - (** Level *) - gram_assoc option * - (** Associativity *) + (* Level *) + Gramlib.Gramext.g_assoc option * + (* Associativity *) 'a production_rule list - (** Symbol list with the interpretation function *) + (* Symbol list with the interpretation function *) type 'a extend_statement = - gram_position option * + Gramlib.Gramext.position option * 'a single_extend_statement list diff --git a/parsing/notation_gram.ml b/parsing/notation_gram.ml index d8c08803b6..fc5feba58b 100644 --- a/parsing/notation_gram.ml +++ b/parsing/notation_gram.ml @@ -32,7 +32,7 @@ type grammar_constr_prod_item = type one_notation_grammar = { notgram_level : level; - notgram_assoc : Extend.gram_assoc option; + notgram_assoc : Gramlib.Gramext.g_assoc option; notgram_notation : Constrexpr.notation; notgram_prods : grammar_constr_prod_item list list; } diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 170df6ad09..923147ba2e 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -14,31 +14,6 @@ open Extend open Genarg open Gramlib -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; - 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 @@ -82,7 +57,6 @@ module type S = end *) - type 'a entry = 'a Entry.e type coq_parsable val coq_parsable : ?file:Loc.source -> char Stream.t -> coq_parsable @@ -91,12 +65,10 @@ module type S = val comment_state : coq_parsable -> ((int * int) * string) list -end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct +end with type 'a Entry.e = 'a Extend.entry = struct include Grammar.GMake(CLexer) - type 'a entry = 'a Entry.e - type coq_parsable = parsable * CLexer.lexer_state ref let coq_parsable ?(file=Loc.ToplevelInput) c = @@ -117,7 +89,7 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct 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 + let loc = match loc' with None -> loc | Some loc -> loc in Loc.raise ~loc e let comment_state (p,state) = @@ -146,20 +118,6 @@ struct end -let warning_verbose = Gramext.warning_verbose - -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 - module Symbols : sig val stoken : Tok.t -> ('s, string) G.ty_symbol val slist0sep : ('s, 'a) G.ty_symbol -> ('s, 'b) G.ty_symbol -> ('s, 'a list) G.ty_symbol @@ -184,12 +142,6 @@ end = struct let slist1sep x y = G.s_list1sep x y false end -let camlp5_verbosity silent f x = - let a = !warning_verbose in - warning_verbose := silent; - f x; - warning_verbose := a - (** Grammar extensions *) (** NB: [extend_statement = @@ -218,10 +170,12 @@ let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> (s, a) G.ty_symbol | Anext -> G.s_next | Aentry e -> G.s_nterm e | Aentryl (e, n) -> G.s_nterml e n -| Arules rs -> G.s_rules (List.map symbol_of_rules rs) +| Arules rs -> + let warning msg = Feedback.msg_warning Pp.(str msg) in + G.s_rules ~warning:(Some warning) (List.map symbol_of_rules rs) -and symbol_of_rule : type s a r. (s, a, Loc.t -> r) Extend.rule -> (s, a, Ploc.t -> r) casted_rule = function -| Stop -> Casted (G.r_stop, fun act loc -> act (!@loc)) +and symbol_of_rule : type s a r. (s, a, Loc.t -> r) Extend.rule -> (s, a, Loc.t -> r) casted_rule = function +| Stop -> Casted (G.r_stop, fun act loc -> act loc) | Next (r, s) -> let Casted (r, cast) = symbol_of_rule r in Casted (G.r_next r (symbol_of_prod_entry_key s), (fun act x -> cast (act x))) @@ -232,7 +186,7 @@ and symbol_of_rules : type a. a Extend.rules -> a G.ty_production = function G.production (symb, cast act) (** FIXME: This is a hack around a deficient camlp5 API *) -type 'a any_production = AnyProduction : ('a, 'f, Ploc.t -> 'a) G.ty_rule * 'f -> 'a any_production +type 'a any_production = AnyProduction : ('a, 'f, Loc.t -> 'a) G.ty_rule * 'f -> 'a any_production let of_coq_production_rule : type a. a Extend.production_rule -> a any_production = function | Rule (toks, act) -> @@ -240,10 +194,10 @@ let of_coq_production_rule : type a. a Extend.production_rule -> a any_productio AnyProduction (symb, cast 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 fix_extend_statement (pos, st) = let fix_single_extend_statement (lvl, assoc, rules) = @@ -253,19 +207,19 @@ let fix_extend_statement (pos, st) = (pos, List.map fix_single_extend_statement st) (** Type of reinitialization data *) -type gram_reinit = gram_assoc * gram_position +type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position type extend_rule = -| ExtendRule : 'a G.entry * gram_reinit option * 'a extend_statement -> extend_rule +| ExtendRule : 'a G.Entry.e * 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 EntryData = struct type _ t = Ex : 'b G.Entry.e 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 + | ByEntry : ('a * 'b) EntryCommand.tag * string * 'b G.Entry.e -> ext_kind (** The list of extensions *) @@ -282,13 +236,12 @@ let grammar_delete e reinit (pos,rls) = (List.rev rls); match reinit with | Some (a,ext) -> - let a = of_coq_assoc a in - let ext = of_coq_position ext in let lev = match pos with | Some (Gramext.Level n) -> n | _ -> assert false in - (G.safe_extend e) (Some ext) [Some lev,Some a,[]] + let warning msg = Feedback.msg_warning Pp.(str msg) in + (G.safe_extend ~warning:(Some warning) e) (Some ext) [Some lev,Some a,[]] | None -> () (** Extension *) @@ -296,15 +249,15 @@ 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 ext = fix_extend_statement ext in - let redo () = camlp5_verbosity false (uncurry (G.safe_extend e)) ext in + let pos, ext = fix_extend_statement ext in + let redo () = G.safe_extend ~warning:None e pos ext in camlp5_state := ByEXTEND (undo, redo) :: !camlp5_state; redo () let grammar_extend_sync e reinit ext = camlp5_state := ByGrammar (ExtendRule (e, reinit, ext)) :: !camlp5_state; - let ext = fix_extend_statement (of_coq_extend_statement ext) in - camlp5_verbosity false (uncurry (G.safe_extend e)) ext + let pos, ext = fix_extend_statement (of_coq_extend_statement ext) in + G.safe_extend ~warning:None e pos ext (** The apparent parser of Coq; encapsulate G to keep track of the extensions. *) @@ -352,14 +305,16 @@ let eoi_entry en = let e = Entry.create ((Gram.Entry.name en) ^ "_eoi") in let symbs = G.r_next (G.r_next G.r_stop (G.s_nterm en)) (Symbols.stoken Tok.EOI) in let act = fun _ x loc -> x in - Gram.safe_extend e None (make_rule [G.production (symbs, act)]); + let warning msg = Feedback.msg_warning Pp.(str msg) in + Gram.safe_extend ~warning:(Some warning) e None (make_rule [G.production (symbs, act)]); e let map_entry f en = let e = Entry.create ((Gram.Entry.name en) ^ "_map") in let symbs = G.r_next G.r_stop (G.s_nterm en) in let act = fun x loc -> f x in - Gram.safe_extend e None (make_rule [G.production (symbs, act)]); + let warning msg = Feedback.msg_warning Pp.(str msg) in + Gram.safe_extend ~warning:(Some warning) e None (make_rule [G.production (symbs, act)]); e (* Parse a string, does NOT check if the entire string was read @@ -489,7 +444,8 @@ let epsilon_value f e = let r = G.production (G.r_next G.r_stop (symbol_of_prod_entry_key e), (fun x _ -> f x)) in let ext = [None, None, [r]] in let entry = Gram.entry_create "epsilon" in - let () = G.safe_extend entry None ext in + let warning msg = Feedback.msg_warning Pp.(str msg) in + let () = G.safe_extend ~warning:(Some warning) entry None ext in try Some (parse_string entry "") with _ -> None (** Synchronized grammar extensions *) @@ -542,7 +498,7 @@ let extend_grammar_command tag g = let nb = List.length rules in grammar_stack := (GramExt (nb, GrammarCommand.Dyn (tag, g)), st) :: !grammar_stack -let extend_entry_command (type a) (type b) (tag : (a, b) entry_command) (g : a) : b Gram.entry list = +let extend_entry_command (type a) (type b) (tag : (a, b) entry_command) (g : a) : b Gram.Entry.e list = let EntryInterp.Ex modify = EntryInterpMap.find tag !entry_interp in let grammar_state = match !grammar_stack with | [] -> GramState.empty @@ -574,7 +530,7 @@ let extend_dyn_grammar (e, _) = match e with (** Registering extra grammar *) -type any_entry = AnyEntry : 'a Gram.entry -> any_entry +type any_entry = AnyEntry : 'a Gram.Entry.e -> any_entry let grammar_names : any_entry list String.Map.t ref = ref String.Map.empty diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index e64c614149..352857d4cd 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -13,7 +13,6 @@ open Extend open Genarg open Constrexpr open Libnames -open Gramlib (** The parser of Coq *) @@ -26,7 +25,7 @@ sig end module Entry : sig - type 'a t = 'a Grammar.GMake(CLexer).Entry.e + type 'a t = 'a Extend.entry val create : string -> 'a t val parse : 'a t -> Parsable.t -> 'a val print : Format.formatter -> 'a t -> unit @@ -110,10 +109,6 @@ end *) -(** Temporarily activate camlp5 verbosity *) - -val camlp5_verbosity : bool -> ('a -> unit) -> 'a -> unit - (** Parse a string *) val parse_string : 'a Entry.t -> string -> 'a @@ -202,7 +197,7 @@ val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option (** {5 Extending the parser without synchronization} *) -type gram_reinit = gram_assoc * gram_position +type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position (** Type of reinitialization data *) val grammar_extend : 'a Entry.t -> gram_reinit option -> @@ -265,11 +260,6 @@ val find_custom_entry : ('a, 'b) entry_command -> string -> 'b Entry.t val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b -(** Location Utils *) -val of_coqloc : Loc.t -> Ploc.t -val to_coqloc : Ploc.t -> Loc.t -val (!@) : Ploc.t -> Loc.t - type frozen_t val parser_summary_tag : frozen_t Summary.Dyn.tag diff --git a/parsing/tok.mli b/parsing/tok.mli index 9b8c008555..55fcd33272 100644 --- a/parsing/tok.mli +++ b/parsing/tok.mli @@ -27,6 +27,7 @@ val to_string : t -> string (* Needed to fit Camlp5 signature *) val print : Format.formatter -> t -> unit val match_keyword : string -> t -> bool + (** for camlp5 *) val of_pattern : string*string -> t val to_pattern : t -> string*string |