diff options
Diffstat (limited to 'lib/loc.ml')
| -rw-r--r-- | lib/loc.ml | 59 |
1 files changed, 38 insertions, 21 deletions
@@ -1,15 +1,21 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* 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,16 +29,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 ghost = { - fname = ""; line_nb = -1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0; - bp = 0; ep = 0; } - -let is_ghost loc = loc.ep = 0 +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; @@ -51,26 +56,38 @@ let merge loc1 loc2 = bp = loc2.bp; ep = loc1.ep; } else loc2 +let merge_opt l1 l2 = match l1, l2 with + | None, None -> None + | Some l , None -> Some l + | None, Some l -> Some l + | Some l1, Some l2 -> Some (merge l1 l2) + +let finer l1 l2 = match l1, l2 with + | None, _ -> false + | Some l , None -> true + | Some l1, Some l2 -> l1.fname = l2.fname && merge l1 l2 = l2 + let unloc loc = (loc.bp, loc.ep) -let dummy_loc = ghost -let join_loc = merge +let shift_loc kb kp loc = { loc with bp = loc.bp + kb ; ep = loc.ep + kp } (** Located type *) +type 'a located = t option * 'a -type 'a located = t * 'a -let located_fold_left f x (_,a) = f x a -let located_iter2 f (_,a) (_,b) = f a b -let down_located f (_,a) = f a +let tag ?loc x = loc, x +let map f (l,x) = (l, f x) (** Exceptions *) let location : t Exninfo.t = Exninfo.make () let add_loc e loc = Exninfo.add e location loc - let get_loc e = Exninfo.get e location -let raise loc e = - let info = Exninfo.add Exninfo.null location loc in - Exninfo.iraise (e, info) +let raise ?loc e = + match loc with + | None -> raise e + | Some loc -> + let info = Exninfo.add Exninfo.null location loc in + Exninfo.iraise (e, info) + |