Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2

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.}
         }
  *)