aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/aux_file.ml20
-rw-r--r--lib/aux_file.mli8
-rw-r--r--lib/cAst.ml24
-rw-r--r--lib/cAst.mli22
-rw-r--r--lib/cWarnings.ml19
-rw-r--r--lib/cWarnings.mli2
-rw-r--r--lib/clib.mllib2
-rw-r--r--lib/coqProject_file.ml4215
-rw-r--r--lib/coqProject_file.mli52
-rw-r--r--lib/envars.ml31
-rw-r--r--lib/envars.mli6
-rw-r--r--lib/feedback.ml2
-rw-r--r--lib/feedback.mli2
-rw-r--r--lib/loc.ml30
-rw-r--r--lib/loc.mli34
-rw-r--r--lib/stateid.ml2
-rw-r--r--lib/stateid.mli2
17 files changed, 405 insertions, 68 deletions
diff --git a/lib/aux_file.ml b/lib/aux_file.ml
index 1b6651a55f..09a254e9d9 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..a7960fa169 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 -> unit
diff --git a/lib/cAst.ml b/lib/cAst.ml
new file mode 100644
index 0000000000..301a6bac8c
--- /dev/null
+++ b/lib/cAst.ml
@@ -0,0 +1,24 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** The ast type contains generic metadata for AST nodes. *)
+type 'a t = {
+ v : 'a;
+ loc : Loc.t option;
+}
+
+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 l =
+ let loc, v = l in
+ { v = f ?loc v ; loc }
+
+let with_val f n = f n.v
+let with_loc_val f n = f ?loc:n.loc n.v
diff --git a/lib/cAst.mli b/lib/cAst.mli
new file mode 100644
index 0000000000..700a06ce84
--- /dev/null
+++ b/lib/cAst.mli
@@ -0,0 +1,22 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** The ast type contains generic metadata for AST nodes *)
+type 'a t = private {
+ v : 'a;
+ loc : Loc.t option;
+}
+
+val make : ?loc:Loc.t -> 'a -> 'a t
+
+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 t -> 'b
+val with_loc_val : (?loc:Loc.t -> 'a -> 'b) -> 'a t -> 'b
diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml
index 71e02b3ba4..2755946abc 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 := 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/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/clib.mllib b/lib/clib.mllib
index c73ae9b904..d5c938fe54 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -18,6 +18,7 @@ IStream
Flags
Control
Loc
+CAst
CList
CString
Deque
@@ -32,3 +33,4 @@ CUnix
Envars
Aux_file
Monad
+CoqProject_file
diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4
new file mode 100644
index 0000000000..7a16605695
--- /dev/null
+++ b/lib/coqProject_file.ml4
@@ -0,0 +1,215 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+type project = {
+ project_file : string option;
+ makefile : string option;
+ install_kind : install option;
+ use_ocamlopt : bool;
+
+ v_files : string list;
+ mli_files : string list;
+ ml4_files : string list;
+ ml_files : string list;
+ mllib_files : string list;
+ mlpack_files : string list;
+
+ ml_includes : path list;
+ r_includes : (path * logic_path) list;
+ q_includes : (path * logic_path) list;
+ extra_args : string list;
+ defs : (string * string) list;
+
+ extra_targets : extra_target list;
+ subdirs : string list;
+}
+and extra_target = {
+ target : string;
+ dependencies : string;
+ phony : bool;
+ command : string;
+}
+and logic_path = string
+and path = { path : string; canonical_path : string }
+and install =
+ | NoInstall
+ | TraditionalInstall
+ | UserInstall
+
+(* TODO generate with PPX *)
+let mk_project project_file makefile install_kind use_ocamlopt = {
+ project_file;
+ makefile;
+ install_kind;
+ use_ocamlopt;
+
+ v_files = [];
+ mli_files = [];
+ ml4_files = [];
+ ml_files = [];
+ mllib_files = [];
+ mlpack_files = [];
+ extra_targets = [];
+ subdirs = [];
+ ml_includes = [];
+ r_includes = [];
+ q_includes = [];
+ extra_args = [];
+ defs = [];
+}
+
+(********************* utils ********************************************)
+
+let rec post_canonize f =
+ if Filename.basename f = Filename.current_dir_name
+ then let dir = Filename.dirname f in
+ if dir = Filename.current_dir_name then f else post_canonize dir
+ else f
+
+(* Avoid Sys.is_directory raise an exception (if the file does not exists) *)
+let is_directory f = Sys.file_exists f && Sys.is_directory f
+
+(********************* parser *******************************************)
+
+exception Parsing_error of string
+
+let rec parse_string = parser
+ | [< '' ' | '\n' | '\t' >] -> ""
+ | [< 'c; s >] -> (String.make 1 c)^(parse_string s)
+ | [< >] -> ""
+and parse_string2 = parser
+ | [< ''"' >] -> ""
+ | [< 'c; s >] -> (String.make 1 c)^(parse_string2 s)
+ | [< >] -> raise (Parsing_error "unterminated string")
+and parse_skip_comment = parser
+ | [< ''\n'; s >] -> s
+ | [< 'c; s >] -> parse_skip_comment s
+ | [< >] -> [< >]
+and parse_args = parser
+ | [< '' ' | '\n' | '\t'; s >] -> parse_args s
+ | [< ''#'; s >] -> parse_args (parse_skip_comment s)
+ | [< ''"'; str = parse_string2; s >] -> ("" ^ str) :: parse_args s
+ | [< 'c; str = parse_string; s >] -> ((String.make 1 c) ^ str) :: (parse_args s)
+ | [< >] -> []
+
+let parse f =
+ let c = open_in f in
+ let res = parse_args (Stream.of_channel c) in
+ close_in c;
+ res
+;;
+
+let process_cmd_line orig_dir proj args =
+ let orig_dir = (* avoids turning foo.v in ./foo.v *)
+ if orig_dir = "." then "" else orig_dir in
+ let error s = Feedback.msg_error (Pp.str (s^".")); exit 1 in
+ let mk_path d =
+ let p = CUnix.correct_path d orig_dir in
+ { path = CUnix.remove_path_dot (post_canonize p);
+ canonical_path = CUnix.canonical_path_name p } in
+ let rec aux proj = function
+ | [] -> proj
+ | "-impredicative-set" :: _ ->
+ error "Use \"-arg -impredicative-set\" instead of \"-impredicative-set\""
+ | "-no-install" :: _ ->
+ error "Use \"-install none\" instead of \"-no-install\""
+ | "-custom" :: _ ->
+ error "Use \"-extra[-phony] target deps command\" instead of \"-custom command deps target\""
+
+ | ("-no-opt"|"-byte") :: r -> aux { proj with use_ocamlopt = false } r
+ | ("-full"|"-opt") :: r -> aux { proj with use_ocamlopt = true } r
+ | "-install" :: d :: r ->
+ if proj.install_kind <> None then
+ Feedback.msg_warning (Pp.str "-install set more than once.");
+ let install = match d with
+ | "user" -> UserInstall
+ | "none" -> NoInstall
+ | "global" -> TraditionalInstall
+ | _ -> error ("invalid option \""^d^"\" passed to -install") in
+ aux { proj with install_kind = Some install } r
+ | "-extra" :: target :: dependencies :: command :: r ->
+ let tgt = { target; dependencies; phony = false; command } in
+ aux { proj with extra_targets = proj.extra_targets @ [tgt] } r
+ | "-extra-phony" :: target :: dependencies :: command :: r ->
+ let tgt = { target; dependencies; phony = true; command } in
+ aux { proj with extra_targets = proj.extra_targets @ [tgt] } r
+
+ | "-Q" :: d :: lp :: r ->
+ aux { proj with q_includes = proj.q_includes @ [mk_path d,lp] } r
+ | "-I" :: d :: r ->
+ aux { proj with ml_includes = proj.ml_includes @ [mk_path d] } r
+ | "-R" :: d :: lp :: r ->
+ aux { proj with r_includes = proj.r_includes @ [mk_path d,lp] } r
+
+ | "-f" :: file :: r ->
+ let file = CUnix.remove_path_dot (CUnix.correct_path file orig_dir) in
+ let () = match proj.project_file with
+ | None -> ()
+ | Some _ -> Feedback.msg_warning (Pp.str
+ "Multiple project files are deprecated.")
+ in
+ let proj = aux { proj with project_file = Some file } (parse file) in
+ aux proj r
+
+ | "-o" :: file :: r ->
+ if String.contains file '/' then
+ error "Output file must be in the current directory";
+ if proj.makefile <> None then
+ error "Option -o given more than once";
+ aux { proj with makefile = Some file } r
+ | v :: "=" :: def :: r ->
+ aux { proj with defs = proj.defs @ [v,def] } r
+ | "-arg" :: a :: r ->
+ aux { proj with extra_args = proj.extra_args @ [a] } r
+ | f :: r ->
+ let f = CUnix.correct_path f orig_dir in
+ let proj =
+ if is_directory f then { proj with subdirs = proj.subdirs @ [f] }
+ else match CUnix.get_extension f with
+ | ".v" -> { proj with v_files = proj.v_files @ [f] }
+ | ".ml" -> { proj with ml_files = proj.ml_files @ [f] }
+ | ".ml4" -> { proj with ml4_files = proj.ml4_files @ [f] }
+ | ".mli" -> { proj with mli_files = proj.mli_files @ [f] }
+ | ".mllib" -> { proj with mllib_files = proj.mllib_files @ [f] }
+ | ".mlpack" -> { proj with mlpack_files = proj.mlpack_files @ [f] }
+ | _ -> raise (Parsing_error ("Unknown option "^f)) in
+ aux proj r
+ in
+ aux proj args
+
+ (******************************* API ************************************)
+
+let cmdline_args_to_project ~curdir args =
+ process_cmd_line curdir (mk_project None None None true) args
+
+let read_project_file f =
+ process_cmd_line (Filename.dirname f)
+ (mk_project (Some f) None (Some NoInstall) true) (parse f)
+
+let rec find_project_file ~from ~projfile_name =
+ let fname = Filename.concat from projfile_name in
+ if Sys.file_exists fname then Some fname
+ else
+ let newdir = Filename.dirname from in
+ if newdir = "" || newdir = "/" then None
+ else find_project_file ~from:newdir ~projfile_name
+;;
+
+let coqtop_args_from_project
+ { ml_includes; r_includes; q_includes; extra_args }
+=
+ let map = List.map in
+ let args =
+ map (fun { canonical_path = i } -> ["-I"; i]) ml_includes @
+ map (fun ({ canonical_path = i }, l) -> ["-Q"; i; l]) q_includes @
+ map (fun ({ canonical_path = p }, l) -> ["-R"; p; l]) r_includes @
+ [extra_args] in
+ List.flatten args
+;;
+
+(* vim:set ft=ocaml: *)
diff --git a/lib/coqProject_file.mli b/lib/coqProject_file.mli
new file mode 100644
index 0000000000..8c8fc068a3
--- /dev/null
+++ b/lib/coqProject_file.mli
@@ -0,0 +1,52 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+exception Parsing_error of string
+
+type project = {
+ project_file : string option;
+ makefile : string option;
+ install_kind : install option;
+ use_ocamlopt : bool;
+
+ v_files : string list;
+ mli_files : string list;
+ ml4_files : string list;
+ ml_files : string list;
+ mllib_files : string list;
+ mlpack_files : string list;
+
+ ml_includes : path list;
+ r_includes : (path * logic_path) list;
+ q_includes : (path * logic_path) list;
+ extra_args : string list;
+ defs : (string * string) list;
+
+ (* deprecated in favor of a Makefile.local using :: rules *)
+ extra_targets : extra_target list;
+ subdirs : string list;
+
+}
+and extra_target = {
+ target : string;
+ dependencies : string;
+ phony : bool;
+ command : string;
+}
+and logic_path = string
+and path = { path : string; canonical_path : string }
+and install =
+ | NoInstall
+ | TraditionalInstall
+ | UserInstall
+
+val cmdline_args_to_project : curdir:string -> string list -> project
+val read_project_file : string -> project
+val coqtop_args_from_project : project -> string list
+val find_project_file : from:string -> projfile_name:string -> string option
+
diff --git a/lib/envars.ml b/lib/envars.ml
index 89ce528318..79516bb1bf 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -146,12 +146,8 @@ let coqpath =
let exe s = s ^ Coq_config.exec_extension
-let guess_ocamlfind () = which (user_path ()) (exe "ocamlfind")
-
let ocamlfind () =
- if !Flags.ocamlfind_spec then !Flags.ocamlfind else
- if !Flags.boot then Coq_config.ocamlfind else
- try guess_ocamlfind () / "ocamlfind" with Not_found -> Coq_config.ocamlfind
+ if !Flags.ocamlfind_spec then !Flags.ocamlfind else Coq_config.ocamlfind
(** {2 Camlp4 paths} *)
@@ -207,3 +203,28 @@ let xdg_config_dirs warn =
let xdg_dirs ~warn =
List.filter Sys.file_exists (xdg_data_dirs warn)
+
+(* Print the configuration information *)
+
+let coq_src_subdirs = [
+ "config" ; "dev" ; "lib" ; "kernel" ; "library" ;
+ "engine" ; "pretyping" ; "interp" ; "parsing" ; "proofs" ;
+ "tactics" ; "toplevel" ; "printing" ; "intf" ;
+ "grammar" ; "ide" ; "stm"; "vernac" ] @
+ Coq_config.plugins_dirs
+
+let print_config ?(prefix_var_name="") f =
+ let open Printf in
+ fprintf f "%sLOCAL=%s\n" prefix_var_name (if Coq_config.local then "1" else "0");
+ fprintf f "%sCOQLIB=%s/\n" prefix_var_name (coqlib ());
+ fprintf f "%sDOCDIR=%s/\n" prefix_var_name (docdir ());
+ fprintf f "%sOCAMLFIND=%s\n" prefix_var_name (ocamlfind ());
+ fprintf f "%sCAMLP4=%s\n" prefix_var_name Coq_config.camlp4;
+ fprintf f "%sCAMLP4O=%s\n" prefix_var_name Coq_config.camlp4o;
+ fprintf f "%sCAMLP4BIN=%s/\n" prefix_var_name (camlp4bin ());
+ fprintf f "%sCAMLP4LIB=%s\n" prefix_var_name (camlp4lib ());
+ fprintf f "%sCAMLP4OPTIONS=%s\n" prefix_var_name Coq_config.camlp4compat;
+ fprintf f "%sHASNATDYNLINK=%s\n" prefix_var_name
+ (if Coq_config.has_natdynlink then "true" else "false");
+ fprintf f "%sCOQ_SRC_SUBDIRS=%s\n" prefix_var_name (String.concat " " coq_src_subdirs)
+
diff --git a/lib/envars.mli b/lib/envars.mli
index 90a42859b9..b164e789d2 100644
--- a/lib/envars.mli
+++ b/lib/envars.mli
@@ -69,3 +69,9 @@ val xdg_data_home : (string -> unit) -> string
val xdg_config_dirs : (string -> unit) -> string list
val xdg_data_dirs : (string -> unit) -> string list
val xdg_dirs : warn : (string -> unit) -> string list
+
+(** {6 Prints the configuration information } *)
+val print_config : ?prefix_var_name:string -> out_channel -> unit
+
+(** Directories in which coq sources are found *)
+val coq_src_subdirs : string list
diff --git a/lib/feedback.ml b/lib/feedback.ml
index 0846e419b2..f6abf65120 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 e373a760cb..ee759bdfc1 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,24 +45,25 @@ let merge loc1 loc2 =
bp = loc2.bp; ep = loc1.ep; }
else loc2
-let unloc loc = (loc.bp, loc.ep)
+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 dummy_loc = ghost
-let join_loc = merge
+let unloc loc = (loc.bp, loc.ep)
(** 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 =
@@ -77,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 bb88f86428..edcf701bf2 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. *)
@@ -35,13 +32,9 @@ 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 is_ghost : t -> bool
-(** Test whether the location is meaningful *)
-
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} *)
@@ -54,18 +47,23 @@ 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 option * 'a
+val tag : ?loc:t -> 'a -> 'a located
+(** Embed a location in a type *)
+
+val map : ('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
-val located_iter2 : ('a -> 'b -> unit) -> 'a located -> 'b located -> unit
+ [@@ocaml.deprecated "use pattern matching"]
val down_located : ('a -> 'b) -> 'a located -> 'b
-(** Projects out a located object *)
+ [@@ocaml.deprecated "use pattern matching"]
-(** {5 Backward compatibility} *)
-
-val dummy_loc : t
-(** Same as [ghost] *)
+val located_iter2 : ('a -> 'b -> unit) -> 'a located -> 'b located -> unit
+ [@@ocaml.deprecated "use pattern matching"]
-val join_loc : t -> t -> t
-(** Same as [merge] *)
diff --git a/lib/stateid.ml b/lib/stateid.ml
index c153f0e808..29f020071b 100644
--- a/lib/stateid.ml
+++ b/lib/stateid.ml
@@ -40,7 +40,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
}
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 12:12:20 +0000