summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/envars.ml6
-rw-r--r--lib/explore.ml18
-rw-r--r--lib/explore.mli2
-rw-r--r--lib/pp.ml419
-rw-r--r--lib/pp.mli3
-rw-r--r--lib/util.ml25
-rw-r--r--lib/util.mli6
-rw-r--r--lib/xml_parser.mli2
8 files changed, 57 insertions, 24 deletions
diff --git a/lib/envars.ml b/lib/envars.ml
index e5c93803..17cfa122 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -62,10 +62,10 @@ let xdg_config_home =
"coq"
let xdg_data_dirs =
- try
+ (try
List.map (fun dir -> Filename.concat dir "coq") (path_to_list (Sys.getenv "XDG_DATA_DIRS"))
- with Not_found -> "/usr/local/share/coq" :: "/usr/share/coq"
- :: (match Coq_config.datadir with |None -> [] |Some datadir -> [datadir])
+ with Not_found -> ["/usr/local/share/coq";"/usr/share/coq"])
+ @ (match Coq_config.datadir with |None -> [] |Some datadir -> [datadir])
let xdg_dirs =
let dirs = xdg_data_home :: xdg_data_dirs
diff --git a/lib/explore.ml b/lib/explore.ml
index 407bf1e9..e353c907 100644
--- a/lib/explore.ml
+++ b/lib/explore.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Format
+open Pp
(*s Definition of a search problem. *)
@@ -14,20 +14,20 @@ module type SearchProblem = sig
type state
val branching : state -> state list
val success : state -> bool
- val pp : state -> unit
+ val pp : state -> std_ppcmds
end
module Make = functor(S : SearchProblem) -> struct
type position = int list
- let pp_position p =
+ let msg_with_position p pp =
let rec pp_rec = function
- | [] -> ()
- | [i] -> printf "%d" i
- | i :: l -> pp_rec l; printf ".%d" i
+ | [] -> mt ()
+ | [i] -> int i
+ | i :: l -> pp_rec l ++ str "." ++ int i
in
- open_hbox (); pp_rec p; close_box ()
+ msg_debug (h 0 (pp_rec p) ++ pp)
(*s Depth first search. *)
@@ -40,7 +40,7 @@ module Make = functor(S : SearchProblem) -> struct
let debug_depth_first s =
let rec explore p s =
- pp_position p; S.pp s;
+ msg_with_position p (S.pp s);
if S.success s then s else explore_many 1 p (S.branching s)
and explore_many i p = function
| [] -> raise Not_found
@@ -83,7 +83,7 @@ module Make = functor(S : SearchProblem) -> struct
explore q
| s :: l ->
let ps = i::p in
- pp_position ps; S.pp s;
+ msg_with_position ps (S.pp s);
if S.success s then s else enqueue (succ i) p (push (ps,s) q) l
in
enqueue 1 [] empty [s]
diff --git a/lib/explore.mli b/lib/explore.mli
index e64459f1..a292fd83 100644
--- a/lib/explore.mli
+++ b/lib/explore.mli
@@ -27,7 +27,7 @@ module type SearchProblem = sig
val success : state -> bool
- val pp : state -> unit
+ val pp : state -> Pp.std_ppcmds
end
diff --git a/lib/pp.ml4 b/lib/pp.ml4
index c602b403..ab172c44 100644
--- a/lib/pp.ml4
+++ b/lib/pp.ml4
@@ -274,17 +274,15 @@ let pp_dirs ft =
(* pretty print on stdout and stderr *)
(* Special chars for emacs, to detect warnings inside goal output *)
-let emacs_warning_start_string = String.make 1 (Char.chr 254)
-let emacs_warning_end_string = String.make 1 (Char.chr 255)
+let emacs_quote_start = String.make 1 (Char.chr 254)
+let emacs_quote_end = String.make 1 (Char.chr 255)
-let warnstart() =
- if not !print_emacs then mt() else str emacs_warning_start_string
+let emacs_quote strm =
+ if !print_emacs then
+ [< str emacs_quote_start; hov 0 strm; str emacs_quote_end >]
+ else hov 0 strm
-let warnend() =
- if not !print_emacs then mt() else str emacs_warning_end_string
-
-let warnbody strm =
- [< warnstart() ; hov 0 (str "Warning: " ++ strm) ; warnend() >]
+let warnbody strm = emacs_quote (str "Warning: " ++ strm)
(* pretty printing functions WITHOUT FLUSH *)
let pp_with ft strm =
@@ -333,6 +331,9 @@ let msgerr x = msg_with !err_ft x
let msgerrnl x = msgnl_with !err_ft x
let msg_warning x = msg_warning_with !err_ft x
+(* Same specific display in emacs as warning, but without the "Warning:" *)
+let msg_debug x = msgnl (emacs_quote x)
+
let string_of_ppcmds c =
msg_with Format.str_formatter c;
Format.flush_str_formatter ()
diff --git a/lib/pp.mli b/lib/pp.mli
index 7070e3f5..1b923d4a 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -113,4 +113,7 @@ val msgerr : std_ppcmds -> unit
val msgerrnl : std_ppcmds -> unit
val msg_warning : std_ppcmds -> unit
+(** Same specific display in emacs as warning, but without the "Warning:" **)
+val msg_debug : std_ppcmds -> unit
+
val string_of_ppcmds : std_ppcmds -> string
diff --git a/lib/util.ml b/lib/util.ml
index 287dd371..4f14b83a 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -499,6 +499,9 @@ let list_map4 f l1 l2 l3 l4 =
in
map (l1,l2,l3,l4)
+let list_map_to_array f l =
+ Array.of_list (List.map f l)
+
let rec list_smartfilter f l = match l with
[] -> l
| h::tl ->
@@ -708,6 +711,12 @@ let list_map_filter_i f =
match f i x with None -> l' | Some y -> y::l'
in aux 0
+let list_filter_along f filter l =
+ snd (list_filter2 (fun b c -> f b) (filter,l))
+
+let list_filter_with filter l =
+ list_filter_along (fun x -> x) filter l
+
let list_subset l1 l2 =
let t2 = Hashtbl.create 151 in
List.iter (fun x -> Hashtbl.add t2 x ()) l2;
@@ -741,7 +750,7 @@ let list_split_when p =
split_when_loop []
(* [list_split_by p l] splits [l] into two lists [(l1,l2)] such that elements of
- [l1] satisfy [p] and elements of [l2] do not *)
+ [l1] satisfy [p] and elements of [l2] do not; order is preserved *)
let list_split_by p =
let rec split_by_loop = function
| [] -> ([],[])
@@ -900,6 +909,14 @@ let rec list_cartesians_filter op init ll =
let rec list_drop_last = function [] -> assert false | hd :: [] -> [] | hd :: tl -> hd :: list_drop_last tl
+(* Factorize lists of pairs according to the left argument *)
+let rec list_factorize_left = function
+ | (a,b)::l ->
+ let al,l' = list_split_by (fun (a',b) -> a=a') l in
+ (a,(b::List.map snd al)) :: list_factorize_left l'
+ | [] ->
+ []
+
(* Arrays *)
let array_compare item_cmp v1 v2 =
@@ -1217,6 +1234,12 @@ let array_rev_to_list a =
if i >= Array.length a then res else tolist (i+1) (a.(i) :: res) in
tolist 0 []
+let array_filter_along f filter v =
+ Array.of_list (list_filter_along f filter (Array.to_list v))
+
+let array_filter_with filter v =
+ Array.of_list (list_filter_with filter (Array.to_list v))
+
(* Stream *)
let stream_nth n st =
diff --git a/lib/util.mli b/lib/util.mli
index 1fec2295..a0a28970 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -135,6 +135,8 @@ val list_duplicates : 'a list -> 'a list
val list_filter2 : ('a -> 'b -> bool) -> 'a list * 'b list -> 'a list * 'b list
val list_map_filter : ('a -> 'b option) -> 'a list -> 'b list
val list_map_filter_i : (int -> 'a -> 'b option) -> 'a list -> 'b list
+val list_filter_with : bool list -> 'a list -> 'a list
+val list_filter_along : ('a -> bool) -> 'a list -> 'b list -> 'b list
(** [list_smartmap f [a1...an] = List.map f [a1...an]] but if for all i
[ f ai == ai], then [list_smartmap f l==l] *)
@@ -147,6 +149,7 @@ val list_map3 :
('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
val list_map4 :
('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list
+val list_map_to_array : ('a -> 'b) -> 'a list -> 'b array
val list_filter_i :
(int -> 'a -> bool) -> 'a list -> 'a list
@@ -239,6 +242,7 @@ val list_cartesians_filter :
('a -> 'b -> 'b option) -> 'b -> 'a list list -> 'b list
val list_union_map : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
+val list_factorize_left : ('a * 'b) list -> ('a * 'b list) list
(** {6 Arrays. } *)
@@ -291,6 +295,8 @@ val array_fold_map2' :
val array_distinct : 'a array -> bool
val array_union_map : ('a -> 'b -> 'b) -> 'a array -> 'b -> 'b
val array_rev_to_list : 'a array -> 'a list
+val array_filter_along : ('a -> bool) -> 'a list -> 'b array -> 'b array
+val array_filter_with : bool list -> 'a array -> 'a array
(** {6 Streams. } *)
diff --git a/lib/xml_parser.mli b/lib/xml_parser.mli
index a3e8aa4a..e3e7ac4d 100644
--- a/lib/xml_parser.mli
+++ b/lib/xml_parser.mli
@@ -42,7 +42,7 @@ type t
and the {!Xml.error_pos} can be used to retreive the document
location where the error occured at.}
{li {!Xml.File_not_found} is raised when and error occured while
- opening a file with the {!Xml.parse_file} function.
+ opening a file with the {!Xml.parse_file} function.}
}
*)