From 846b74275511bd89c2f3abe19245133050d2199c Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 12 Jan 2017 20:11:01 +0100 Subject: [constrexpr] Make patterns use Loc.located for location information This is first of a series of patches, converting `constrexpr` pattern data type from ad-hoc location handling to `Loc.located`. Along Coq, we can find two different coding styles for handling objects with location information: one style uses `'a Loc.located`, whereas other data structures directly embed `Loc.t` in their constructors. Handling all located objects uniformly would be very convenient, and would allow optimizing certain cases, in particular making located smarter when there is no location information, as it is the case for all terms coming from the kernel. `git grep 'Loc.t \*'` gives an overview of the remaining work to do. We've also added an experimental API for `located` to the `Loc` module, `Loc.tag` should be used to add locations objects, making it explicit in the code when a "located" object is created. --- lib/loc.ml | 4 ++++ lib/loc.mli | 17 ++++++++++++----- 2 files changed, 16 insertions(+), 5 deletions(-) (limited to 'lib') diff --git a/lib/loc.ml b/lib/loc.ml index e373a760cb..39f2d7dfba 100644 --- a/lib/loc.ml +++ b/lib/loc.ml @@ -59,6 +59,10 @@ let join_loc = merge (** Located type *) type 'a located = t * 'a + +let to_pair x = x +let tag ?loc x = Option.default ghost loc, x + 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 diff --git a/lib/loc.mli b/lib/loc.mli index bb88f86428..fef1d89388 100644 --- a/lib/loc.mli +++ b/lib/loc.mli @@ -18,9 +18,6 @@ type t = { ep : int; (** end position *) } -type 'a located = t * 'a -(** Embed a location in a type *) - (** {5 Location manipulation} *) (** This is inherited from CAMPL4/5. *) @@ -54,12 +51,22 @@ val get_loc : Exninfo.info -> t option val raise : ?loc:t -> exn -> 'a (** [raise loc e] is the same as [Pervasives.raise (add_loc e loc)]. *) -(** {5 Location utilities} *) +(** {5 Objects with location information } *) + +type 'a located = t * 'a +(** Embed a location in a type *) + +(** Warning, this API is experimental *) + +val to_pair : 'a located -> t * 'a +val tag : ?loc:t -> 'a -> 'a located val located_fold_left : ('a -> 'b -> 'a) -> 'a -> 'b located -> 'a +val down_located : ('a -> 'b) -> 'a located -> 'b + +(* Current not used *) val located_iter2 : ('a -> 'b -> unit) -> 'a located -> 'b located -> unit -val down_located : ('a -> 'b) -> 'a located -> 'b (** Projects out a located object *) (** {5 Backward compatibility} *) -- cgit v1.2.3 From 6d9e008ffd81bbe927e3442fb0c37269ed25b21f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 14 Jan 2017 01:27:40 +0100 Subject: [location] Use Loc.located for constr_expr. This is the second patch, which is a bit more invasive. We reasoning is similar to the previous patch. Code is not as clean as it could as we would need to convert `glob_constr` to located too, then a few parts could just map the location. --- lib/loc.ml | 5 +++++ lib/loc.mli | 5 +++++ 2 files changed, 10 insertions(+) (limited to 'lib') diff --git a/lib/loc.ml b/lib/loc.ml index 39f2d7dfba..8ae8fe25d0 100644 --- a/lib/loc.ml +++ b/lib/loc.ml @@ -63,6 +63,11 @@ type 'a located = t * 'a let to_pair x = x let tag ?loc x = Option.default ghost loc, x +let with_loc f (loc, x) = f ~loc x + +let map f (l,x) = (l, f x) +let map_with_loc f (loc, x) = (loc, f ~loc x) + 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 diff --git a/lib/loc.mli b/lib/loc.mli index fef1d89388..7fc8efaa89 100644 --- a/lib/loc.mli +++ b/lib/loc.mli @@ -61,6 +61,11 @@ type 'a located = t * 'a val to_pair : 'a located -> t * 'a val tag : ?loc:t -> 'a -> 'a located +val with_loc : (loc:t -> 'a -> 'b) -> 'a located -> 'b + +val map : ('a -> 'b) -> 'a located -> 'b located +val map_with_loc : (loc:t -> 'a -> 'b) -> 'a located -> 'b located + val located_fold_left : ('a -> 'b -> 'a) -> 'a -> 'b located -> 'a val down_located : ('a -> 'b) -> 'a located -> 'b -- cgit v1.2.3 From ad3aab9415b98a247a6cbce05752632c3c42391c Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 16 Jan 2017 13:02:55 +0100 Subject: [location] Move Glob_term.cases_pattern to located. We continue the uniformization pass. No big news here, trying to be minimally invasive. --- lib/loc.ml | 3 ++- lib/loc.mli | 1 + 2 files changed, 3 insertions(+), 1 deletion(-) (limited to 'lib') diff --git a/lib/loc.ml b/lib/loc.ml index 8ae8fe25d0..8d7432ff4b 100644 --- a/lib/loc.ml +++ b/lib/loc.ml @@ -63,7 +63,8 @@ type 'a located = t * 'a let to_pair x = x let tag ?loc x = Option.default ghost loc, x -let with_loc f (loc, x) = f ~loc x +let with_loc f (loc, x) = f ~loc x +let with_unloc f (_,x) = f x let map f (l,x) = (l, f x) let map_with_loc f (loc, x) = (loc, f ~loc x) diff --git a/lib/loc.mli b/lib/loc.mli index 7fc8efaa89..3f484bc4c3 100644 --- a/lib/loc.mli +++ b/lib/loc.mli @@ -62,6 +62,7 @@ val to_pair : 'a located -> t * 'a val tag : ?loc:t -> 'a -> 'a located val with_loc : (loc:t -> 'a -> 'b) -> 'a located -> 'b +val with_unloc : ('a -> 'b) -> 'a located -> 'b val map : ('a -> 'b) -> 'a located -> 'b located val map_with_loc : (loc:t -> 'a -> 'b) -> 'a located -> 'b located -- cgit v1.2.3 From 158f40db9482ead89befbf9bc9ad45ff8a60b75f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 17 Jan 2017 14:23:53 +0100 Subject: [location] Switch glob_constr to Loc.located --- lib/loc.ml | 1 + lib/loc.mli | 1 + 2 files changed, 2 insertions(+) (limited to 'lib') diff --git a/lib/loc.ml b/lib/loc.ml index 8d7432ff4b..2a785fac48 100644 --- a/lib/loc.ml +++ b/lib/loc.ml @@ -62,6 +62,7 @@ type 'a located = t * 'a let to_pair x = x let tag ?loc x = Option.default ghost loc, x +let obj (_,x) = x let with_loc f (loc, x) = f ~loc x let with_unloc f (_,x) = f x diff --git a/lib/loc.mli b/lib/loc.mli index 3f484bc4c3..10f63a8dd7 100644 --- a/lib/loc.mli +++ b/lib/loc.mli @@ -60,6 +60,7 @@ type 'a located = t * 'a val to_pair : 'a located -> t * 'a val tag : ?loc:t -> 'a -> 'a located +val obj : 'a located -> 'a val with_loc : (loc:t -> 'a -> 'b) -> 'a located -> 'b val with_unloc : ('a -> 'b) -> 'a located -> 'b -- cgit v1.2.3 From 30d3515546cf244837c6340b6b87c5f51e68cbf4 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 17 Jan 2017 23:40:35 +0100 Subject: [location] Remove Loc.ghost. Now it is a private field, locations are optional. --- lib/aux_file.ml | 20 +++++++++++--------- lib/aux_file.mli | 8 ++++---- lib/cWarnings.ml | 19 ++++++------------- lib/feedback.ml | 2 +- lib/feedback.mli | 2 +- lib/loc.ml | 17 ++++++++++------- lib/loc.mli | 17 +++++------------ lib/stateid.ml | 2 +- lib/stateid.mli | 2 +- 9 files changed, 40 insertions(+), 49 deletions(-) (limited to 'lib') diff --git a/lib/aux_file.ml b/lib/aux_file.ml index 1b6651a55f..fe6e873883 100644 --- a/lib/aux_file.ml +++ b/lib/aux_file.ml @@ -46,19 +46,21 @@ let contents x = x let empty_aux_file = H.empty -let get aux loc key = M.find key (H.find (Loc.unloc loc) aux) +let get ?loc aux key = M.find key (H.find (Option.cata Loc.unloc (0,0) loc) aux) -let record_in_aux_at loc key v = +let record_in_aux_at ?loc key v = Option.iter (fun oc -> - let i, j = Loc.unloc loc in - Printf.fprintf oc "%d %d %s %S\n" i j key v) - !oc + match loc with + | Some loc -> let i, j = Loc.unloc loc in + Printf.fprintf oc "%d %d %s %S\n" i j key v + | None -> Printf.fprintf oc "--- %s %S\n" key v + ) !oc -let current_loc = ref Loc.ghost +let current_loc : Loc.t option ref = ref None -let record_in_aux_set_at loc = current_loc := loc +let record_in_aux_set_at ?loc = current_loc := loc -let record_in_aux key v = record_in_aux_at !current_loc key v +let record_in_aux key v = record_in_aux_at ?loc:!current_loc key v let set h loc k v = let m = try H.find loc h with Not_found -> M.empty in @@ -91,4 +93,4 @@ let load_aux_file_for vfile = Flags.if_verbose Feedback.msg_info Pp.(str"Loading file "++str aux_fname++str": "++str s); empty_aux_file -let set h loc k v = set h (Loc.unloc loc) k v +let set ?loc h k v = set h (Option.cata Loc.unloc (0,0) loc) k v diff --git a/lib/aux_file.mli b/lib/aux_file.mli index 86e322b71d..41b7b0855d 100644 --- a/lib/aux_file.mli +++ b/lib/aux_file.mli @@ -9,9 +9,9 @@ type aux_file val load_aux_file_for : string -> aux_file -val get : aux_file -> Loc.t -> string -> string val empty_aux_file : aux_file -val set : aux_file -> Loc.t -> string -> string -> aux_file +val get : ?loc:Loc.t -> aux_file -> string -> string +val set : ?loc:Loc.t -> aux_file -> string -> string -> aux_file module H : Map.S with type key = int * int module M : Map.S with type key = string @@ -22,6 +22,6 @@ val start_aux_file : aux_file:string -> v_file:string -> unit val stop_aux_file : unit -> unit val recording : unit -> bool -val record_in_aux_at : Loc.t -> string -> string -> unit +val record_in_aux_at : ?loc:Loc.t -> string -> string -> unit val record_in_aux : string -> string -> unit -val record_in_aux_set_at : Loc.t -> unit +val record_in_aux_set_at : ?loc:Loc.t -> unit diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml index 2f569d2849..4e692af360 100644 --- a/lib/cWarnings.ml +++ b/lib/cWarnings.ml @@ -20,10 +20,10 @@ type t = { let warnings : (string, t) Hashtbl.t = Hashtbl.create 97 let categories : (string, string list) Hashtbl.t = Hashtbl.create 97 -let current_loc = ref Loc.ghost +let current_loc = ref None let flags = ref "" -let set_current_loc = (:=) current_loc +let set_current_loc loc = current_loc := Some loc let get_flags () = !flags @@ -35,29 +35,22 @@ let add_warning_in_category ~name ~category = in Hashtbl.replace categories category (name::ws) -let refine_loc = function - | None when not (Loc.is_ghost !current_loc) -> Some !current_loc - | loc -> loc - let create ~name ~category ?(default=Enabled) pp = Hashtbl.add warnings name { default; category; status = default }; add_warning_in_category ~name ~category; if default <> Disabled then add_warning_in_category ~name ~category:"default"; - fun ?loc x -> let w = Hashtbl.find warnings name in + fun ?loc x -> + let w = Hashtbl.find warnings name in + let loc = Option.append loc !current_loc in match w.status with | Disabled -> () - | AsError -> - begin match refine_loc loc with - | Some loc -> CErrors.user_err ~loc (pp x) - | None -> CErrors.user_err (pp x) - end + | AsError -> CErrors.user_err ?loc (pp x) | Enabled -> let msg = pp x ++ spc () ++ str "[" ++ str name ++ str "," ++ str category ++ str "]" in - let loc = refine_loc loc in Feedback.msg_warning ?loc msg let warn_unknown_warning = diff --git a/lib/feedback.ml b/lib/feedback.ml index df6fe3a629..3552fa4a03 100644 --- a/lib/feedback.ml +++ b/lib/feedback.ml @@ -30,7 +30,7 @@ type feedback_content = | FileDependency of string option * string | FileLoaded of string * string (* Extra metadata *) - | Custom of Loc.t * string * xml + | Custom of Loc.t option * string * xml (* Generic messages *) | Message of level * Loc.t option * Pp.std_ppcmds diff --git a/lib/feedback.mli b/lib/feedback.mli index bdd236ac78..dc104132a0 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -38,7 +38,7 @@ type feedback_content = | FileDependency of string option * string | FileLoaded of string * string (* Extra metadata *) - | Custom of Loc.t * string * xml + | Custom of Loc.t option * string * xml (* Generic messages *) | Message of level * Loc.t option * Pp.std_ppcmds diff --git a/lib/loc.ml b/lib/loc.ml index 2a785fac48..3051ca7b9d 100644 --- a/lib/loc.ml +++ b/lib/loc.ml @@ -26,12 +26,6 @@ let make_loc (bp, ep) = { fname = ""; 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 merge loc1 loc2 = if loc1.bp < loc2.bp then if loc1.ep < loc2.ep then { @@ -51,15 +45,24 @@ let merge loc1 loc2 = bp = loc2.bp; ep = loc1.ep; } else loc2 +let merge_opt l1 l2 = Option.cata (fun l1 -> merge l1 l2) l2 l1 +let opt_merge l1 l2 = Option.cata (fun l2 -> merge l1 l2) l1 l2 + let unloc loc = (loc.bp, loc.ep) -let dummy_loc = ghost let join_loc = merge (** Located type *) type 'a located = t * 'a +let is_ghost loc = loc.ep = 0 + +let ghost = { + fname = ""; line_nb = -1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0; + bp = 0; ep = 0; } + +let internal_ghost = ghost let to_pair x = x let tag ?loc x = Option.default ghost loc, x let obj (_,x) = x diff --git a/lib/loc.mli b/lib/loc.mli index 10f63a8dd7..82792613c0 100644 --- a/lib/loc.mli +++ b/lib/loc.mli @@ -32,14 +32,15 @@ val unloc : t -> int * int val make_loc : int * int -> t (** Make a location out of its start and end position *) -val ghost : t -(** Dummy location *) - +val internal_ghost : t val is_ghost : t -> bool (** Test whether the location is meaningful *) val merge : t -> t -> t +val merge_opt : t option -> t -> t +val opt_merge : t -> t option -> t + (** {5 Located exceptions} *) val add_loc : Exninfo.info -> t -> Exninfo.info @@ -71,15 +72,7 @@ val map_with_loc : (loc:t -> 'a -> 'b) -> 'a located -> 'b located val located_fold_left : ('a -> 'b -> 'a) -> 'a -> 'b located -> 'a val down_located : ('a -> 'b) -> 'a located -> 'b -(* Current not used *) +(* Currently not used *) val located_iter2 : ('a -> 'b -> unit) -> 'a located -> 'b located -> unit (** Projects out a located object *) - -(** {5 Backward compatibility} *) - -val dummy_loc : t -(** Same as [ghost] *) - -val join_loc : t -> t -> t -(** Same as [merge] *) diff --git a/lib/stateid.ml b/lib/stateid.ml index ae25735c5f..34d49685b4 100644 --- a/lib/stateid.ml +++ b/lib/stateid.ml @@ -41,7 +41,7 @@ type ('a,'b) request = { exn_info : t * t; stop : t; document : 'b; - loc : Loc.t; + loc : Loc.t option; uuid : 'a; name : string } diff --git a/lib/stateid.mli b/lib/stateid.mli index 1d87a343b3..d9e75f5840 100644 --- a/lib/stateid.mli +++ b/lib/stateid.mli @@ -34,7 +34,7 @@ type ('a,'b) request = { exn_info : t * t; stop : t; document : 'b; - loc : Loc.t; + loc : Loc.t option; uuid : 'a; name : string } -- cgit v1.2.3 From e8a6467545c2814c9418889201e8be19c0cef201 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 18 Jan 2017 15:46:23 +0100 Subject: [location] Make location optional in Loc.located This completes the Loc.ghost removal, the idea is to gear the API towards optional, but uniform, location handling. We don't print anymore in the case there is no location. This is what the test suite expects. The old printing logic for located items was a bit inconsistent as it sometimes printed and other times it printed nothing as the caller checked for `is_ghost` upstream. --- lib/cWarnings.ml | 2 +- lib/cWarnings.mli | 2 +- lib/loc.ml | 25 ++++++++++++------------- lib/loc.mli | 14 ++++++-------- 4 files changed, 20 insertions(+), 23 deletions(-) (limited to 'lib') diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml index 4e692af360..ececc6308e 100644 --- a/lib/cWarnings.ml +++ b/lib/cWarnings.ml @@ -23,7 +23,7 @@ let categories : (string, string list) Hashtbl.t = Hashtbl.create 97 let current_loc = ref None let flags = ref "" -let set_current_loc loc = current_loc := Some loc +let set_current_loc loc = current_loc := loc let get_flags () = !flags diff --git a/lib/cWarnings.mli b/lib/cWarnings.mli index 3f6cee31b7..c1fb5d6042 100644 --- a/lib/cWarnings.mli +++ b/lib/cWarnings.mli @@ -8,7 +8,7 @@ type status = Disabled | Enabled | AsError -val set_current_loc : Loc.t -> unit +val set_current_loc : Loc.t option -> unit val create : name:string -> category:string -> ?default:status -> ('a -> Pp.std_ppcmds) -> ?loc:Loc.t -> 'a -> unit diff --git a/lib/loc.ml b/lib/loc.ml index 3051ca7b9d..e02fe108d6 100644 --- a/lib/loc.ml +++ b/lib/loc.ml @@ -45,33 +45,32 @@ let merge loc1 loc2 = bp = loc2.bp; ep = loc1.ep; } else loc2 -let merge_opt l1 l2 = Option.cata (fun l1 -> merge l1 l2) l2 l1 -let opt_merge l1 l2 = Option.cata (fun l2 -> merge l1 l2) l1 l2 +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 unloc loc = (loc.bp, loc.ep) let join_loc = merge -(** Located type *) - -type 'a located = t * 'a - -let is_ghost loc = loc.ep = 0 - -let ghost = { +let internal_ghost = { fname = ""; line_nb = -1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0; bp = 0; ep = 0; } -let internal_ghost = ghost +(** Located type *) +type 'a located = t option * 'a + let to_pair x = x -let tag ?loc x = Option.default ghost loc, x +let tag ?loc x = loc, x let obj (_,x) = x -let with_loc f (loc, x) = f ~loc x +let with_loc f (loc, x) = f ?loc x let with_unloc f (_,x) = f x let map f (l,x) = (l, f x) -let map_with_loc f (loc, x) = (loc, f ~loc x) +let map_with_loc f (loc, x) = (loc, f ?loc x) let located_fold_left f x (_,a) = f x a let located_iter2 f (_,a) (_,b) = f a b diff --git a/lib/loc.mli b/lib/loc.mli index 82792613c0..6de6c584d8 100644 --- a/lib/loc.mli +++ b/lib/loc.mli @@ -33,13 +33,11 @@ val make_loc : int * int -> t (** Make a location out of its start and end position *) val internal_ghost : t -val is_ghost : t -> bool + (** Test whether the location is meaningful *) val merge : t -> t -> t - -val merge_opt : t option -> t -> t -val opt_merge : t -> t option -> t +val merge_opt : t option -> t option -> t option (** {5 Located exceptions} *) @@ -54,20 +52,20 @@ val raise : ?loc:t -> exn -> 'a (** {5 Objects with location information } *) -type 'a located = t * 'a +type 'a located = t option * 'a (** Embed a location in a type *) (** Warning, this API is experimental *) -val to_pair : 'a located -> t * 'a +val to_pair : 'a located -> t option * 'a val tag : ?loc:t -> 'a -> 'a located val obj : 'a located -> 'a -val with_loc : (loc:t -> 'a -> 'b) -> 'a located -> 'b +val with_loc : (?loc:t -> 'a -> 'b) -> 'a located -> 'b val with_unloc : ('a -> 'b) -> 'a located -> 'b val map : ('a -> 'b) -> 'a located -> 'b located -val map_with_loc : (loc:t -> 'a -> 'b) -> 'a located -> 'b located +val map_with_loc : (?loc:t -> 'a -> 'b) -> 'a located -> 'b located val located_fold_left : ('a -> 'b -> 'a) -> 'a -> 'b located -> 'a val down_located : ('a -> 'b) -> 'a located -> 'b -- cgit v1.2.3 From 9122623f2377bfe6aad0d4ea662481992e768201 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 8 Apr 2017 19:40:57 +0200 Subject: [location] Remove `Loc.internal_ghost` `internal_ghost` was an artifact to ease porting of the ml4 rules. Now that the location is optional we can finally get rid of it. --- lib/loc.ml | 4 ---- lib/loc.mli | 4 ---- 2 files changed, 8 deletions(-) (limited to 'lib') diff --git a/lib/loc.ml b/lib/loc.ml index e02fe108d6..9107dce471 100644 --- a/lib/loc.ml +++ b/lib/loc.ml @@ -55,10 +55,6 @@ let unloc loc = (loc.bp, loc.ep) let join_loc = merge -let internal_ghost = { - fname = ""; line_nb = -1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0; - bp = 0; ep = 0; } - (** Located type *) type 'a located = t option * 'a diff --git a/lib/loc.mli b/lib/loc.mli index 6de6c584d8..110920d5ad 100644 --- a/lib/loc.mli +++ b/lib/loc.mli @@ -32,10 +32,6 @@ val unloc : t -> int * int val make_loc : int * int -> t (** Make a location out of its start and end position *) -val internal_ghost : t - -(** Test whether the location is meaningful *) - val merge : t -> t -> t val merge_opt : t option -> t option -> t option -- cgit v1.2.3 From 6eb42e53ffafd9aed3c12805c6a228acccc03827 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 8 Apr 2017 20:08:01 +0200 Subject: [location] Document changes. --- lib/loc.mli | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'lib') diff --git a/lib/loc.mli b/lib/loc.mli index 110920d5ad..ec79ced5d3 100644 --- a/lib/loc.mli +++ b/lib/loc.mli @@ -51,8 +51,11 @@ val raise : ?loc:t -> exn -> 'a type 'a located = t option * 'a (** Embed a location in a type *) -(** Warning, this API is experimental *) +(* We would like in the future: + * type 'a located = private { tag: t option; obj: 'a; } + *) +(** Warning, this API is experimental *) val to_pair : 'a located -> t option * 'a val tag : ?loc:t -> 'a -> 'a located val obj : 'a located -> 'a -- cgit v1.2.3 From 054d2736c1c1b55cb7708ff0444af521cd0fe2ba Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 8 Apr 2017 23:19:35 +0200 Subject: [location] [ast] Switch Constrexpr AST to an extensible node type. Following @gasche idea, and the original intention of #402, we switch the main parsing AST of Coq from `'a Loc.located` to `'a CAst.ast` which is private and record-based. This provides significantly clearer code for the AST, and is robust wrt attributes. --- lib/cAst.ml | 24 ++++++++++++++++++++++++ lib/cAst.mli | 22 ++++++++++++++++++++++ lib/clib.mllib | 1 + 3 files changed, 47 insertions(+) create mode 100644 lib/cAst.ml create mode 100644 lib/cAst.mli (limited to 'lib') diff --git a/lib/cAst.ml b/lib/cAst.ml new file mode 100644 index 0000000000..5916c9ec12 --- /dev/null +++ b/lib/cAst.ml @@ -0,0 +1,24 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 'a -> 'a ast + +val map : ('a -> 'b) -> 'a ast -> 'b ast +val map_with_loc : (?loc:Loc.t -> 'a -> 'b) -> 'a ast -> 'b ast +val map_from_loc : (?loc:Loc.t -> 'a -> 'b) -> 'a Loc.located -> 'b ast + +val with_val : ('a -> 'b) -> 'a ast -> 'b +val with_loc_val : (?loc:Loc.t -> 'a -> 'b) -> 'a ast -> 'b diff --git a/lib/clib.mllib b/lib/clib.mllib index c73ae9b904..9eb479fcc9 100644 --- a/lib/clib.mllib +++ b/lib/clib.mllib @@ -18,6 +18,7 @@ IStream Flags Control Loc +CAst CList CString Deque -- cgit v1.2.3 From 7058b9b400e252a30c1e624cbe0de26b70356d64 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 9 Apr 2017 03:39:07 +0200 Subject: [location] Cleanup. We remove some unnecessary functions introduced before in the patch series + unused functions. --- lib/cAst.ml | 4 ++-- lib/loc.ml | 21 +++++++-------------- lib/loc.mli | 22 ++++++++-------------- 3 files changed, 17 insertions(+), 30 deletions(-) (limited to 'lib') diff --git a/lib/cAst.ml b/lib/cAst.ml index 5916c9ec12..f0a4057766 100644 --- a/lib/cAst.ml +++ b/lib/cAst.ml @@ -16,8 +16,8 @@ let make ?loc v = { v; loc } let map f n = { n with v = f n.v } let map_with_loc f n = { n with v = f ?loc:n.loc n.v } -let map_from_loc f n = - let loc, v = Loc.to_pair n in +let map_from_loc f l = + let loc, v = l in { v = f ?loc v ; loc } let with_val f n = f n.v diff --git a/lib/loc.ml b/lib/loc.ml index 9107dce471..ee759bdfc1 100644 --- a/lib/loc.ml +++ b/lib/loc.ml @@ -53,31 +53,17 @@ let merge_opt l1 l2 = match l1, l2 with let unloc loc = (loc.bp, loc.ep) -let join_loc = merge - (** Located type *) type 'a located = t option * 'a -let to_pair x = x let tag ?loc x = loc, x -let obj (_,x) = x - -let with_loc f (loc, x) = f ?loc x -let with_unloc f (_,x) = f x - let map f (l,x) = (l, f x) -let map_with_loc f (loc, x) = (loc, f ?loc x) - -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 (** 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 = @@ -86,3 +72,10 @@ let raise ?loc e = | Some loc -> let info = Exninfo.add Exninfo.null location loc in Exninfo.iraise (e, info) + +(** Deprecated *) +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 + + diff --git a/lib/loc.mli b/lib/loc.mli index ec79ced5d3..edcf701bf2 100644 --- a/lib/loc.mli +++ b/lib/loc.mli @@ -34,6 +34,7 @@ val make_loc : int * int -> t val merge : t -> t -> t val merge_opt : t option -> t option -> t option +(** Merge locations, usually generating the largest possible span *) (** {5 Located exceptions} *) @@ -49,27 +50,20 @@ val raise : ?loc:t -> exn -> 'a (** {5 Objects with location information } *) type 'a located = t option * 'a -(** Embed a location in a type *) - -(* We would like in the future: - * type 'a located = private { tag: t option; obj: 'a; } - *) -(** Warning, this API is experimental *) -val to_pair : 'a located -> t option * 'a val tag : ?loc:t -> 'a -> 'a located -val obj : 'a located -> 'a - -val with_loc : (?loc:t -> 'a -> 'b) -> 'a located -> 'b -val with_unloc : ('a -> 'b) -> 'a located -> 'b +(** Embed a location in a type *) val map : ('a -> 'b) -> 'a located -> 'b located -val map_with_loc : (?loc:t -> 'a -> 'b) -> 'a located -> 'b located +(** Modify an object carrying a location *) +(** Deprecated functions *) val located_fold_left : ('a -> 'b -> 'a) -> 'a -> 'b located -> 'a + [@@ocaml.deprecated "use pattern matching"] + val down_located : ('a -> 'b) -> 'a located -> 'b + [@@ocaml.deprecated "use pattern matching"] -(* Currently not used *) val located_iter2 : ('a -> 'b -> unit) -> 'a located -> 'b located -> unit + [@@ocaml.deprecated "use pattern matching"] -(** Projects out a located object *) -- cgit v1.2.3 From 209956322367e5a4a4c8c78c053ea9352a9a16c8 Mon Sep 17 00:00:00 2001 From: Matej Košík Date: Fri, 28 Apr 2017 14:31:14 +0200 Subject: [location] Renaming "CAst.ast" to "CAst.t" --- lib/cAst.ml | 2 +- lib/cAst.mli | 14 +++++++------- 2 files changed, 8 insertions(+), 8 deletions(-) (limited to 'lib') diff --git a/lib/cAst.ml b/lib/cAst.ml index f0a4057766..301a6bac8c 100644 --- a/lib/cAst.ml +++ b/lib/cAst.ml @@ -7,7 +7,7 @@ (************************************************************************) (** The ast type contains generic metadata for AST nodes. *) -type 'a ast = { +type 'a t = { v : 'a; loc : Loc.t option; } diff --git a/lib/cAst.mli b/lib/cAst.mli index 291536d123..700a06ce84 100644 --- a/lib/cAst.mli +++ b/lib/cAst.mli @@ -7,16 +7,16 @@ (************************************************************************) (** The ast type contains generic metadata for AST nodes *) -type 'a ast = private { +type 'a t = private { v : 'a; loc : Loc.t option; } -val make : ?loc:Loc.t -> 'a -> 'a ast +val make : ?loc:Loc.t -> 'a -> 'a t -val map : ('a -> 'b) -> 'a ast -> 'b ast -val map_with_loc : (?loc:Loc.t -> 'a -> 'b) -> 'a ast -> 'b ast -val map_from_loc : (?loc:Loc.t -> 'a -> 'b) -> 'a Loc.located -> 'b ast +val map : ('a -> 'b) -> 'a t -> 'b t +val map_with_loc : (?loc:Loc.t -> 'a -> 'b) -> 'a t -> 'b t +val map_from_loc : (?loc:Loc.t -> 'a -> 'b) -> 'a Loc.located -> 'b t -val with_val : ('a -> 'b) -> 'a ast -> 'b -val with_loc_val : (?loc:Loc.t -> 'a -> 'b) -> 'a ast -> 'b +val with_val : ('a -> 'b) -> 'a t -> 'b +val with_loc_val : (?loc:Loc.t -> 'a -> 'b) -> 'a t -> 'b -- cgit v1.2.3