diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-06 11:41:33 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-09-14 13:31:27 +0200 |
commit | 7f816f00fed5ee7c7e94bd5f02a88880cdfa96aa (patch) | |
tree | 3c0d25c6cb26b5425ec5bc38ed9707c87a8d7e52 | |
parent | a86bdf0cae05e46d5f0516f29254aeb72bf08de7 (diff) |
Using an algebraic type for distinguishing toplevel input from location in file.
-rw-r--r-- | API/API.mli | 2 | ||||
-rw-r--r-- | lib/loc.ml | 13 | ||||
-rw-r--r-- | lib/loc.mli | 8 | ||||
-rw-r--r-- | parsing/cLexer.ml4 | 29 | ||||
-rw-r--r-- | parsing/cLexer.mli | 2 | ||||
-rw-r--r-- | parsing/pcoq.ml | 9 | ||||
-rw-r--r-- | parsing/pcoq.mli | 2 | ||||
-rw-r--r-- | toplevel/coqloop.ml | 6 | ||||
-rw-r--r-- | toplevel/vernac.ml | 2 | ||||
-rw-r--r-- | vernac/topfmt.ml | 5 | ||||
-rw-r--r-- | vernac/vernacentries.ml | 2 |
11 files changed, 51 insertions, 29 deletions
diff --git a/API/API.mli b/API/API.mli index 8b0bef48c..a3701621e 100644 --- a/API/API.mli +++ b/API/API.mli @@ -4703,7 +4703,7 @@ sig type coq_parsable - val parsable : ?file:string -> char Stream.t -> coq_parsable + val 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 diff --git a/lib/loc.ml b/lib/loc.ml index 9f036d90f..06da13d44 100644 --- a/lib/loc.ml +++ b/lib/loc.ml @@ -8,8 +8,12 @@ (* Locations management *) +type source = + | InFile of string + | ToplevelInput + type t = { - fname : string; (** filename *) + fname : source; (** filename or toplevel input *) line_nb : int; (** start line number *) bol_pos : int; (** position of the beginning of start line *) line_nb_last : int; (** end line number *) @@ -23,10 +27,15 @@ let create fname line_nb bol_pos bp ep = { line_nb_last = line_nb; bol_pos_last = bol_pos; bp = bp; ep = ep; } let make_loc (bp, ep) = { - fname = ""; line_nb = -1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0; + fname = ToplevelInput; line_nb = -1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0; bp = bp; ep = ep; } +let mergeable loc1 loc2 = + loc1.fname = loc2.fname + let merge loc1 loc2 = + if not (mergeable loc1 loc2) then + failwith "Trying to merge unmergeable locations."; if loc1.bp < loc2.bp then if loc1.ep < loc2.ep then { fname = loc1.fname; diff --git a/lib/loc.mli b/lib/loc.mli index 1fbaae836..d4061e044 100644 --- a/lib/loc.mli +++ b/lib/loc.mli @@ -8,8 +8,12 @@ (** {5 Basic types} *) +type source = + | InFile of string + | ToplevelInput + type t = { - fname : string; (** filename *) + fname : source; (** filename or toplevel input *) line_nb : int; (** start line number *) bol_pos : int; (** position of the beginning of start line *) line_nb_last : int; (** end line number *) @@ -22,7 +26,7 @@ type t = { (** This is inherited from CAMPL4/5. *) -val create : string -> int -> int -> int -> int -> t +val create : source -> int -> int -> int -> int -> t (** Create a location from a filename, a line number, a position of the beginning of the line, a start and end position *) diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 index 636027f9b..9c9189ffe 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml4 @@ -10,8 +10,19 @@ open Pp open Util open Tok +(** 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 = Ploc.file_name 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; @@ -118,14 +129,6 @@ let err loc str = Loc.raise ~loc:(to_coqloc loc) (Error.E str) let bad_token str = raise (Error.E (Bad_token str)) -(** Location utilities *) -let file_loc_of_file = function -| None -> "" -| Some f -> f - -let make_loc fname line_nb bol_pos bp ep = - Ploc.make_loc (file_loc_of_file fname) line_nb bol_pos (bp, ep) "" - (* 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) @@ -369,7 +372,7 @@ let rec string loc ~comm_level bp len = parser err loc Unterminated_string (* To associate locations to a file name *) -let current_file = ref None +let current_file = ref Loc.ToplevelInput (* Utilities for comments in beautify *) let comment_begin = ref None @@ -392,7 +395,7 @@ let rec split_comments comacc acc pos = function let extract_comments pos = split_comments [] [] pos !comments (* The state of the lexer visible from outside *) -type lexer_state = int option * string * bool * ((int * int) * string) list * string option +type lexer_state = int option * string * bool * ((int * int) * string) list * Loc.source let init_lexer_state f = (None,"",true,[],f) let set_lexer_state (o,s,b,c,f) = @@ -404,7 +407,7 @@ let set_lexer_state (o,s,b,c,f) = let release_lexer_state () = (!comment_begin, Buffer.contents current_comment, !between_commands, !comments, !current_file) let drop_lexer_state () = - set_lexer_state (init_lexer_state None) + set_lexer_state (init_lexer_state Loc.ToplevelInput) let real_push_char c = Buffer.add_char current_comment c @@ -672,7 +675,7 @@ let token_text = function let func cs = let loct = loct_create () in - let cur_loc = ref (make_loc !current_file 1 0 0 0) in + let cur_loc = ref (from_coqloc !current_file 1 0 0 0) in let ts = Stream.from (fun i -> diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli index 77d652b18..d3ef19873 100644 --- a/parsing/cLexer.mli +++ b/parsing/cLexer.mli @@ -49,7 +49,7 @@ end (* Mainly for comments state, etc... *) type lexer_state -val init_lexer_state : string option -> lexer_state +val init_lexer_state : Loc.source -> lexer_state val set_lexer_state : lexer_state -> unit val release_lexer_state : unit -> lexer_state val drop_lexer_state : unit -> unit diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 81f02bf95..0a4411233 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -15,8 +15,11 @@ let curry f x y = f (x, y) let uncurry f (x,y) = f x y (** Location Utils *) +let coq_file_of_ploc_file s = + if s = "" then Loc.ToplevelInput else Loc.InFile s + let to_coqloc loc = - { Loc.fname = Ploc.file_name 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; @@ -80,7 +83,7 @@ module type S = Gramext.position option * single_extend_statment list type coq_parsable - val parsable : ?file:string -> char Stream.t -> coq_parsable + val 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 @@ -104,7 +107,7 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct Gramext.position option * single_extend_statment list type coq_parsable = parsable * CLexer.lexer_state ref - let parsable ?file c = + let parsable ?(file=Loc.ToplevelInput) c = let state = ref (CLexer.init_lexer_state file) in CLexer.set_lexer_state !state; let a = parsable c in diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 445818e13..ecb0ddd4f 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -73,7 +73,7 @@ module type S = type coq_parsable - val parsable : ?file:string -> char Stream.t -> coq_parsable + val 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 diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index d76703d98..444bf8a8f 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -155,14 +155,16 @@ let error_info_for_buffer ?loc buf = let fname = loc.Loc.fname in let hl, loc = (* We are in the toplevel *) - if CString.equal fname "" then + match fname with + | Loc.ToplevelInput -> let nloc = adjust_loc_buf buf loc in if valid_buffer_loc buf loc then (fnl () ++ print_highlight_location buf nloc, nloc) (* in the toplevel, but not a valid buffer *) else (mt (), nloc) (* we are in batch mode, don't adjust location *) - else (mt (), loc) + | Loc.InFile _ -> + (mt (), loc) in Topfmt.pr_loc loc ++ hl ) loc diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index bfab44770..1602f9c68 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -182,7 +182,7 @@ and load_vernac verbosely sid file = if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout in let in_chan = open_utf8_file_in file in let in_echo = if verbosely then Some (open_utf8_file_in file) else None in - let in_pa = Pcoq.Gram.parsable ~file (Stream.of_channel in_chan) in + let in_pa = Pcoq.Gram.parsable ~file:(Loc.InFile file) (Stream.of_channel in_chan) in let rsid = ref sid in try (* we go out of the following infinite loop when a End_of_input is diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index e7b14309d..6a10eb43a 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -292,10 +292,11 @@ let emacs_logger = gen_logger Emacs.quote_info Emacs.quote_warning (* This is specific to the toplevel *) let pr_loc loc = let fname = loc.Loc.fname in - if CString.equal fname "" then + match fname with + | Loc.ToplevelInput -> Loc.(str"Toplevel input, characters " ++ int loc.bp ++ str"-" ++ int loc.ep ++ str":") - else + | Loc.InFile fname -> Loc.(str"File " ++ str "\"" ++ str fname ++ str "\"" ++ str", line " ++ int loc.line_nb ++ str", characters " ++ int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos) ++ diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index d2ba9eb1c..22306ac5b 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1902,7 +1902,7 @@ let vernac_load interp fname = let input = let longfname = Loadpath.locate_file fname in let in_chan = open_utf8_file_in longfname in - Pcoq.Gram.parsable ~file:longfname (Stream.of_channel in_chan) in + Pcoq.Gram.parsable ~file:(Loc.InFile longfname) (Stream.of_channel in_chan) in try while true do interp (snd (parse_sentence input)) done with End_of_input -> () |