diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/envars.ml | 6 | ||||
| -rw-r--r-- | lib/explore.ml | 18 | ||||
| -rw-r--r-- | lib/explore.mli | 2 | ||||
| -rw-r--r-- | lib/pp.ml4 | 19 | ||||
| -rw-r--r-- | lib/pp.mli | 3 | ||||
| -rw-r--r-- | lib/util.ml | 25 | ||||
| -rw-r--r-- | lib/util.mli | 6 | ||||
| -rw-r--r-- | lib/xml_parser.mli | 2 |
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 @@ -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 () @@ -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.} } *) |