Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg

10 files changed, 326 insertions, 109 deletions

diff --git a/lib/envars.ml b/lib/envars.ml
new file mode 100644
index 00000000..5887adcd
--- /dev/null
+++ b/lib/envars.ml
@@ -0,0 +1,84 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* This file gathers environment variables needed by Coq to run (such
+   as coqlib) *)
+
+let coqbin () = 
+  if !Flags.boot || Coq_config.local
+  then Filename.concat Coq_config.coqsrc "bin"
+  else System.canonical_path_name (Filename.dirname Sys.executable_name)
+
+let guess_coqlib () = 
+  let file = "states/initial.coq" in
+    if Sys.file_exists (Filename.concat Coq_config.coqlib file) 
+    then Coq_config.coqlib
+    else 
+      let coqbin = System.canonical_path_name (Filename.dirname Sys.executable_name) in
+      let prefix = Filename.dirname coqbin in
+      let coqlib = if Coq_config.local then prefix else 
+	List.fold_left Filename.concat prefix ["lib";"coq"] in
+	if Sys.file_exists (Filename.concat coqlib file) then coqlib else
+	  Util.error "cannot guess a path for Coq libraries; please use -coqlib option"
+	  
+let coqlib () = 
+  if !Flags.coqlib_spec then !Flags.coqlib else
+    (if !Flags.boot then Coq_config.coqsrc else guess_coqlib ())
+
+let path_to_list p =
+  let sep = if Sys.os_type = "Win32" then ';' else ':' in
+    Util.split_string_at sep p 
+
+let rec which l f =
+  match l with
+    | [] -> raise Not_found
+    | p :: tl -> 
+	if Sys.file_exists (Filename.concat p f) 
+	then p 
+	else which tl f
+ 
+let guess_camlbin () = 
+  let path = try Sys.getenv "PATH" with _ -> raise Not_found in 
+  let lpath = path_to_list path in
+    which lpath "ocamlc"
+
+let guess_camlp4bin () = 
+  let path = try Sys.getenv "PATH" with _ -> raise Not_found in 
+  let lpath = path_to_list path in
+    which lpath Coq_config.camlp4
+
+let camlbin () = 
+  if !Flags.camlbin_spec then !Flags.camlbin else
+    if !Flags.boot then Coq_config.camlbin else
+      try guess_camlbin () with _ -> Coq_config.camlbin
+
+let camllib () = 
+  if !Flags.boot
+  then Coq_config.camllib
+  else 
+    let camlbin = camlbin () in 
+    let com = (Filename.concat camlbin "ocamlc") ^ " -where" in
+    let _,res = System.run_command (fun x -> x) (fun _ -> ()) com in
+    Util.strip res
+
+(* TODO : essayer aussi camlbin *)
+let camlp4bin () = 
+  if !Flags.camlp4bin_spec then !Flags.camlp4bin else
+    if !Flags.boot then Coq_config.camlp4bin else
+      try guess_camlp4bin () with _ -> Coq_config.camlp4bin
+
+let camlp4lib () = 
+  if !Flags.boot
+  then Coq_config.camlp4lib
+  else 
+    let camlp4bin = camlp4bin () in 
+    let com = (Filename.concat camlp4bin Coq_config.camlp4) ^ " -where" in
+    let _,res = System.run_command (fun x -> x) (fun _ -> ()) com in
+    Util.strip res
+
+    
diff --git a/lib/envars.mli b/lib/envars.mli
new file mode 100644
index 00000000..62d0cb61
--- /dev/null
+++ b/lib/envars.mli
@@ -0,0 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+val coqlib : unit -> string
+val coqbin : unit -> string
+
+val camlbin : unit -> string
+val camlp4bin : unit -> string
+val camllib : unit -> string
+val camlp4lib : unit -> string
diff --git a/lib/flags.ml b/lib/flags.ml
index 16ae0c64..928912e6 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -6,13 +6,18 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: flags.ml 11309 2008-08-06 10:30:35Z herbelin $ i*)
+(*i $Id: flags.ml 11801 2009-01-18 20:11:41Z herbelin $ i*)
 
 let with_option o f x =
   let old = !o in o:=true;
   try let r = f x in o := old; r
   with e -> o := old; raise e
 
+let without_option o f x =
+  let old = !o in o:=false;
+  try let r = f x in o := old; r
+  with e -> o := old; raise e
+
 let boot = ref false
 
 let batch_mode = ref false
@@ -33,13 +38,10 @@ let raw_print = ref false
 let unicode_syntax = ref false
 
 (* Translate *)
-let translate = ref false
-let make_translate f = translate := f
-let do_translate () = !translate
-let translate_file = ref false
-
-(* True only when interning from pp*new.ml *)
-let translate_syntax = ref false
+let beautify = ref false
+let make_beautify f = beautify := f
+let do_beautify () = !beautify
+let beautify_file = ref false
 
 (* Silent / Verbose *)
 let silent = ref false
@@ -47,16 +49,8 @@ let make_silent flag = silent := flag; ()
 let is_silent () = !silent
 let is_verbose () = not !silent
 
-let silently f x =
-  let oldsilent = !silent in
-  try 
-    silent := true;
-    let rslt = f x in
-    silent := oldsilent; 
-    rslt
-  with e -> begin
-    silent := oldsilent; raise e
-  end
+let silently f x = with_option silent f x
+let verbosely f x = without_option silent f x
 
 let if_silent f x = if !silent then f x
 let if_verbose f x = if not !silent then f x
@@ -82,33 +76,13 @@ let unsafe_set = ref Stringset.empty
 let add_unsafe s = unsafe_set := Stringset.add s !unsafe_set
 let is_unsafe s = Stringset.mem s !unsafe_set
 
-(* Dump of globalization (to be used by coqdoc) *)
-
-let dump = ref false
-let dump_file = ref ""
-let dump_into_file f = dump := true; dump_file := f
-
-let dump_buffer = Buffer.create 8192
-
-let dump_string = Buffer.add_string dump_buffer
-
-let dump_it () = 
-  if !dump then begin
-    let mode = [Open_wronly; Open_append; Open_creat] in
-    let c = open_out_gen mode 0o666 !dump_file in
-    output_string c (Buffer.contents dump_buffer);
-    close_out c
-  end
-
-let _ = at_exit dump_it
-
-(* Flags.for the virtual machine *)
+(* Flags for the virtual machine *)
 
 let boxed_definitions = ref true
 let set_boxed_definitions b = boxed_definitions := b
 let boxed_definitions _ = !boxed_definitions 
  
-(* Flags.for external tools *)
+(* Flags for external tools *)
 
 let subst_command_placeholder s t =
   let buff = Buffer.create (String.length s + String.length t) in
@@ -127,3 +101,16 @@ let browser_cmd_fmt =
   Sys.getenv coq_netscape_remote_var
  with
   Not_found -> Coq_config.browser
+
+(* Options for changing coqlib *)
+let coqlib_spec = ref false
+let coqlib = ref Coq_config.coqlib
+
+(* Options for changing camlbin (used by coqmktop) *)
+let camlbin_spec = ref false
+let camlbin = ref Coq_config.camlbin
+
+(* Options for changing camlp4bin (used by coqmktop) *)
+let camlp4bin_spec = ref false
+let camlp4bin = ref Coq_config.camlp4bin
+
diff --git a/lib/flags.mli b/lib/flags.mli
index 1fcae990..c5903285 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: flags.mli 10921 2008-05-12 12:27:25Z msozeau $ i*)
+(*i $Id: flags.mli 11801 2009-01-18 20:11:41Z herbelin $ i*)
 
 (* Global options of the system. *)
 
@@ -29,16 +29,16 @@ val raw_print : bool ref
 
 val unicode_syntax : bool ref
 
-val translate : bool ref
-val make_translate : bool -> unit
-val do_translate : unit -> bool
-val translate_file : bool ref
-val translate_syntax : bool ref
+val beautify : bool ref
+val make_beautify : bool -> unit
+val do_beautify : unit -> bool
+val beautify_file : bool ref
 
 val make_silent : bool -> unit
 val is_silent : unit -> bool
 val is_verbose : unit -> bool
 val silently : ('a -> 'b) -> 'a -> 'b
+val verbosely : ('a -> 'b) -> 'a -> 'b
 val if_silent : ('a -> unit) -> 'a -> unit
 val if_verbose : ('a -> unit) -> 'a -> unit
 
@@ -47,9 +47,13 @@ val if_warn : ('a -> unit) -> 'a -> unit
 
 val hash_cons_proofs : bool ref
 
-(* Temporary activate an option ('c must be an atomic type) *)
+(* Temporary activate an option (to activate option [o] on [f x y z],
+   use [with_option o (f x y) z]) *)
 val with_option : bool ref -> ('a -> 'b) -> 'a -> 'b
 
+(* Temporary deactivate an option *)
+val without_option : bool ref -> ('a -> 'b) -> 'a -> 'b
+
 (* If [None], no limit *)
 val set_print_hyps_limit : int option -> unit
 val print_hyps_limit : unit -> int option
@@ -57,12 +61,6 @@ val print_hyps_limit : unit -> int option
 val add_unsafe : string -> unit
 val is_unsafe : string -> bool
 
-(* Dump of globalization (to be used by coqdoc) *)
-
-val dump : bool ref
-val dump_into_file : string -> unit
-val dump_string : string -> unit
-
 (* Options for the virtual machine *)
 
 val set_boxed_definitions : bool -> unit
@@ -75,3 +73,13 @@ val browser_cmd_fmt : string
  
 (* Substitute %s in the first chain by the second chain *)
 val subst_command_placeholder : string -> string -> string
+
+(* Options for specifying where coq librairies reside *)
+val coqlib_spec : bool ref
+val coqlib : string ref
+
+(* Options for specifying where OCaml binaries reside *)
+val camlbin_spec : bool ref
+val camlbin : string ref
+val camlp4bin_spec : bool ref
+val camlp4bin : string ref
diff --git a/lib/option.ml b/lib/option.ml
index 34749b8c..85efdd44 100644
--- a/lib/option.ml
+++ b/lib/option.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: option.ml 10739 2008-04-01 14:45:20Z herbelin $ i*)
+(*i $Id: option.ml 11576 2008-11-10 19:13:15Z msozeau $ i*)
 
 (** Module implementing basic combinators for OCaml option type.
    It tries follow closely the style of OCaml standard library.
@@ -97,6 +97,10 @@ let fold_right f x a =
   | Some y -> f y a
   | _ -> a
 
+(** [cata f a x] is [a] if [x] is [None] and [f y] if [x] is [Some y]. *)
+let cata f a = function
+  | Some c -> f c
+  | None -> a
 
 (** {6 More Specific operations} ***)
 
diff --git a/lib/option.mli b/lib/option.mli
index d9c18d88..6fa89098 100644
--- a/lib/option.mli
+++ b/lib/option.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: option.mli 10739 2008-04-01 14:45:20Z herbelin $ *)
+(* $Id: option.mli 11576 2008-11-10 19:13:15Z msozeau $ *)
 
 (** Module implementing basic combinators for OCaml option type.
    It tries follow closely the style of OCaml standard library.
@@ -66,6 +66,8 @@ val fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b option -> 'c option -> 'a
 (** [fold_right f x a] is [f y a] if [x] is [Some y], and [a] otherwise. *)
 val fold_right : ('a -> 'b -> 'b) -> 'a option -> 'b -> 'b
 
+(** [cata e f x] is [e] if [x] is [None] and [f a] if [x] is [Some a] *)
+val cata : ('a -> 'b) -> 'b -> 'a option -> 'b
 
 (** {6 More Specific Operations} ***)
 
diff --git a/lib/system.ml b/lib/system.ml
index 22eb52ee..65826c81 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: system.ml 11209 2008-07-05 10:17:49Z herbelin $ *)
+(* $Id: system.ml 11801 2009-01-18 20:11:41Z herbelin $ *)
 
 open Pp
 open Util
@@ -63,6 +63,34 @@ type load_path = physical_path list
 let physical_path_of_string s = s
 let string_of_physical_path p = p
 
+(* Hints to partially detects if two paths refer to the same repertory *)
+let rec remove_path_dot p = 
+  let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *)
+  let n = String.length curdir in
+  if String.length p > n && String.sub p 0 n = curdir then
+    remove_path_dot (String.sub p n (String.length p - n))
+  else
+    p
+
+let strip_path p =
+  let cwd = Filename.concat (Sys.getcwd ()) "" in (* Unix: "`pwd`/" *)
+  let n = String.length cwd in
+  if String.length p > n && String.sub p 0 n = cwd then
+    remove_path_dot (String.sub p n (String.length p - n))
+  else
+    remove_path_dot p
+
+let canonical_path_name p =
+  let current = Sys.getcwd () in
+  try 
+    Sys.chdir p;
+    let p' = Sys.getcwd () in
+    Sys.chdir current;
+    p'
+  with Sys_error _ ->
+    (* We give up to find a canonical name and just simplify it... *)
+    strip_path p
+
 (* All subdirectories, recursively *)
 
 let exists_dir dir =
@@ -100,7 +128,7 @@ let all_subdirs ~unix_path:root =
   if exists_dir root then traverse root [];
   List.rev !l
 
-let where_in_path warn path filename =
+let where_in_path ?(warn=true) path filename =
   let rec search = function
     | lpe :: rem ->
 	let f = Filename.concat lpe filename in
@@ -116,25 +144,26 @@ let where_in_path warn path filename =
 	    msg_warning
 	      (str filename ++ str " has been found in" ++ spc () ++
 	       hov 0 (str "[ " ++
-	         hv 0 (prlist_with_sep pr_semicolon (fun (lpe,_) -> str lpe) l)
+	         hv 0 (prlist_with_sep (fun () -> str " " ++ pr_semicolon())
+		   (fun (lpe,_) -> str lpe) l)
 	         ++ str " ];") ++ fnl () ++
 	       str "loading " ++ str f);
 	  (lpe, f) in
   check_and_warn (search path)
 
-let find_file_in_path paths filename =
+let find_file_in_path ?(warn=true) paths filename =
   if not (Filename.is_implicit filename) then
     let root = Filename.dirname filename in
     root, filename
   else 
-    try where_in_path true paths filename
+    try where_in_path ~warn paths filename
     with Not_found ->
       errorlabstrm "System.find_file_in_path"
 	(hov 0 (str "Can't find file" ++ spc () ++ str filename ++ spc () ++ 
 		str "on loadpath"))
 
 let is_in_path lpath filename =
-  try ignore (where_in_path false lpath filename); true
+  try ignore (where_in_path ~warn:false lpath filename); true
   with Not_found -> false
 
 let make_suffix name suffix =
@@ -172,7 +201,7 @@ let raw_extern_intern magic suffix =
   in 
   (extern_state,intern_state)
 
-let extern_intern magic suffix =
+let extern_intern ?(warn=true) magic suffix =
   let (raw_extern,raw_intern) = raw_extern_intern magic suffix in
   let extern_state name val_0 = 
     try
@@ -185,7 +214,7 @@ let extern_intern magic suffix =
     with Sys_error s -> error ("System error: " ^ s)
   and intern_state paths name = 
     try
-      let _,filename = find_file_in_path paths (make_suffix name suffix) in
+      let _,filename = find_file_in_path ~warn paths (make_suffix name suffix) in
       let channel = raw_intern filename in
       let v = marshal_in channel in
       close_in channel; 
diff --git a/lib/system.mli b/lib/system.mli
index eb83cbf8..ba5aa408 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: system.mli 11209 2008-07-05 10:17:49Z herbelin $ i*)
+(*i $Id: system.mli 11801 2009-01-18 20:11:41Z herbelin $ i*)
 
 (*s Files and load paths. Load path entries remember the original root
     given by the user. For efficiency, we keep the full path (field
@@ -16,11 +16,13 @@
 type physical_path = string
 type load_path = physical_path list
 
+val canonical_path_name : string -> string
+
 val exclude_search_in_dirname : string -> unit
 
 val all_subdirs : unix_path:string -> (physical_path * string list) list
 val is_in_path : load_path -> string -> bool
-val where_in_path : bool -> load_path -> string -> physical_path * string
+val where_in_path : ?warn:bool -> load_path -> string -> physical_path * string
 
 val physical_path_of_string : string -> physical_path
 val string_of_physical_path : physical_path -> string
@@ -34,7 +36,8 @@ val home : string
 
 val exists_dir : string -> bool
 
-val find_file_in_path : load_path -> string -> physical_path * string
+val find_file_in_path :
+  ?warn:bool -> load_path -> string -> physical_path * string
 
 (*s Generic input and output functions, parameterized by a magic number
   and a suffix. The intern functions raise the exception [Bad_magic_number]
@@ -48,8 +51,8 @@ exception Bad_magic_number of string
 val raw_extern_intern : int -> string -> 
   (string -> string * out_channel) * (string -> in_channel)
 
-val extern_intern : 
-  int -> string -> (string -> 'a -> unit) * (load_path -> string -> 'a)
+val extern_intern : ?warn:bool -> int -> string -> 
+  (string -> 'a -> unit) * (load_path -> string -> 'a)
 
 (*s Sending/receiving once with external executable *)
 
diff --git a/lib/util.ml b/lib/util.ml
index a19cc65b..a73a5558 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id: util.ml 11350 2008-09-02 15:37:49Z barras $ *)
+(* $Id: util.ml 11845 2009-01-22 18:55:08Z letouzey $ *)
 
 open Pp
 
@@ -59,6 +59,9 @@ let is_letter c = (c >= 'a' && c <= 'z') or (c >= 'A' && c <= 'Z')
 let is_digit c = (c >= '0' && c <= '9')
 let is_ident_tail c =
   is_letter c or is_digit c or c = '\'' or c = '_'
+let is_blank = function
+  | ' ' | '\r' | '\t' | '\n' -> true
+  | _ -> false
 
 (* Strings *)
 
@@ -73,6 +76,21 @@ let explode s =
 
 let implode sl = String.concat "" sl
 
+let strip s =
+  let n = String.length s in
+  let rec lstrip_rec i =
+    if i < n && is_blank s.[i] then
+      lstrip_rec (i+1)
+    else i
+  in
+  let rec rstrip_rec i =
+    if i >= 0 && is_blank s.[i] then
+      rstrip_rec (i-1)
+    else i
+  in
+  let a = lstrip_rec 0 and b = rstrip_rec (n-1) in
+  String.sub s a (b-a+1)
+
 (* substring searching... *)
 
 (* gdzie = where, co = what *)
@@ -83,6 +101,9 @@ let rec is_sub gdzie gl gi co cl ci =
    (is_sub gdzie gl (gi+1) co cl (ci+1)))
 
 let rec raw_str_index i gdzie l c co cl = 
+  (* First adapt to ocaml 3.11 new semantics of index_from *)
+  if (i+cl > l) then raise Not_found;
+  (* Then proceed as in ocaml < 3.11 *)
   let i' = String.index_from gdzie i c in
     if (i'+cl <= l) && (is_sub gdzie l i' co cl 0) then i' else
       raw_str_index (i'+1) gdzie l c co cl
@@ -106,19 +127,23 @@ let ordinal n =
 
 (* string parsing *)
 
-let parse_loadpath s =
+let split_string_at c s =
   let len = String.length s in
-  let rec decoupe_dirs n =
+  let rec split n =
     try  
-      let pos = String.index_from s n '/' in
-      if pos = n then
-	invalid_arg "parse_loadpath: find an empty dir in loadpath";
+      let pos = String.index_from s n c in
       let dir = String.sub s n (pos-n) in
-      dir :: (decoupe_dirs (succ pos))
+      dir :: split (succ pos)
     with
       | Not_found -> [String.sub s n (len-n)]
   in
-  if len = 0 then [] else decoupe_dirs 0
+  if len = 0 then [] else split 0
+
+let parse_loadpath s =
+  let l = split_string_at '/' s in
+  if List.mem "" l then
+    invalid_arg "parse_loadpath: find an empty dir in loadpath";
+  l
 
 module Stringset = Set.Make(struct type t = string let compare = compare end)
 
@@ -239,6 +264,8 @@ let classify_unicode unicode =
     end
     | _ ->
     begin match unicode with
+    (* utf-8 CJC Symbols and Punctuation  *)
+    | x when 0x3008 <= x & x <= 0x3020 -> UnicodeSymbol
     (* utf-8 Hiragana U3040-309F and Katakana U30A0-30FF *)
     | x when 0x3040 <= x & x <= 0x30FF -> UnicodeLetter
     (* utf-8 Unified CJK Ideographs U4E00-9FA5 *)
@@ -304,27 +331,40 @@ let next_utf8 s i =
 
 (* Check the well-formedness of an identifier *)
 
-let check_ident s =
+let check_initial handle j n s =
+  match classify_unicode n with
+  | UnicodeLetter -> ()
+  | _ ->
+      let c = String.sub s 0 j in
+      handle ("Invalid character '"^c^"' at beginning of identifier \""^s^"\".")
+
+let check_trailing handle i j n s =
+  match classify_unicode n with
+  | UnicodeLetter | UnicodeIdentPart -> ()
+  | _ ->
+      let c = String.sub s i j in
+      handle ("Invalid character '"^c^"' in identifier \""^s^"\".")
+
+let check_ident_gen handle s =
   let i = ref 0 in
   if s <> ".." then try
     let j, n = next_utf8 s 0 in
-    match classify_unicode n with
-    | UnicodeLetter ->
-	i := !i + j;
-	begin try
-	  while true do
-	    let j, n = next_utf8 s !i in
-	    match classify_unicode n with
-	    | UnicodeLetter | UnicodeIdentPart -> i := !i + j
-	    | _ -> error
-		("invalid character "^(String.sub s !i j)^" in identifier "^s)
-	  done
-	with End_of_input -> () end
-    | _ -> error (s^": an identifier should start with a letter")
+    check_initial handle j n s;
+    i := !i + j;
+    try
+      while true do
+	let j, n = next_utf8 s !i in
+	check_trailing handle !i j n s;
+	i := !i + j
+      done
+    with End_of_input -> ()
   with 
-  | End_of_input -> error "The empty string is not an identifier"
-  | UnsupportedUtf8 -> error (s^": unsupported character in utf8 sequence")
-  | Invalid_argument _ -> error (s^": invalid utf8 sequence")
+  | End_of_input -> error "The empty string is not an identifier."
+  | UnsupportedUtf8 -> error (s^": unsupported character in utf8 sequence.")
+  | Invalid_argument _ -> error (s^": invalid utf8 sequence.")
+
+let check_ident_soft = check_ident_gen warning
+let check_ident = check_ident_gen error
 
 let lowercase_unicode s unicode =
     match unicode land 0x1F000 with
@@ -626,6 +666,10 @@ let rec list_remove_first a = function
   | b::l -> b::list_remove_first a l
   | [] -> raise Not_found
 
+let rec list_remove_assoc_in_triple x = function
+  | [] -> []
+  | (y,_,_ as z)::l -> if x = y then l else z::list_remove_assoc_in_triple x l
+
 let list_add_set x l = if List.mem x l then l else x::l
 
 let list_eq_set l1 l2 =
@@ -726,13 +770,21 @@ let list_subset l1 l2 =
   in 
   look l1
 
-let list_splitby p = 
-  let rec splitby_loop x y = 
+let list_split_at p = 
+  let rec split_at_loop x y = 
     match y with 
       | []      -> ([],[])
-      | (a::l)  -> if (p a) then (x,y) else (splitby_loop (x@[a]) l)
+      | (a::l)  -> if (p a) then (List.rev x,y) else split_at_loop (a::x) l
+  in 
+  split_at_loop []
+
+let list_split_by p = 
+  let rec split_loop = function
+  | []      -> ([],[])
+  | (a::l)  ->
+      let (l1,l2) = split_loop l in if (p a) then (a::l1,l2) else (l1,a::l2)
   in 
-  splitby_loop []
+  split_loop
 
 let rec list_split3 = function
   | [] -> ([], [], [])
@@ -859,6 +911,20 @@ let list_cartesians op init ll =
 
 let list_combinations l = list_cartesians (fun x l -> x::l) [] l
 
+(* Keep only those products that do not return None *)
+
+let rec list_cartesian_filter op l1 l2 = 
+  list_map_append (fun x -> list_map_filter (op x) l2) l1
+
+(* Keep only those products that do not return None *)
+
+let rec list_cartesians_filter op init ll = 
+  List.fold_right (list_cartesian_filter op) ll [init]
+
+(* Drop the last element of a list *)
+
+let rec list_drop_last = function [] -> assert false | hd :: [] -> [] | hd :: tl -> hd :: list_drop_last tl
+
 (* Arrays *)
 
 let array_exists f v = 
@@ -902,6 +968,10 @@ let array_for_all4 f v1 v2 v3 v4 =
   lv1 = Array.length v4 &&
     allrec (pred lv1) 
 
+let array_for_all_i f i v = 
+  let rec allrec i n = n = Array.length v || f i v.(n) && allrec (i+1) (n+1) in 
+  allrec i 0
+
 let array_hd v = 
   match Array.length v with
     | 0 -> failwith "array_hd"
@@ -1117,15 +1187,15 @@ let array_fold_map2' f v1 v2 e =
   (v',!e')
 
 let array_distinct v =
+  let visited = Hashtbl.create 23 in
   try
-    for i=0 to Array.length v-1 do
-      for j=i+1 to Array.length v-1 do
-	if v.(i)=v.(j) then raise Exit
-      done
-    done;
+    Array.iter
+      (fun x ->
+        if Hashtbl.mem visited x then raise Exit
+        else Hashtbl.add visited x x)
+      v;
     true
-  with Exit ->
-    false
+  with Exit -> false
 
 let array_union_map f a acc =
   Array.fold_left
@@ -1209,11 +1279,13 @@ let rec prlist elem l = match l with
   | h::t -> Stream.lapp (fun () -> elem h) (prlist elem t)
 
 (* unlike all other functions below, [prlist] works lazily.
-   if a strict behavior is needed, use [prlist_strict] instead. *)
+   if a strict behavior is needed, use [prlist_strict] instead.
+   evaluation is done from left to right. *)
 
 let rec prlist_strict elem l = match l with 
   | []   -> mt ()
-  | h::t -> (elem h)++(prlist_strict elem t)
+  | h::t ->
+      let e = elem h in let r = prlist_strict elem t in e++r
 
 (* [prlist_with_sep sep pr [a ; ... ; c]] outputs
    [pr a ++ sep() ++ ... ++ sep() ++ pr c] *)
@@ -1275,7 +1347,7 @@ let prvect_with_sep sep elem v =
 let prvect elem v = prvect_with_sep mt elem v
 
 let pr_located pr (loc,x) =
-  if Flags.do_translate() && loc<>dummy_loc then
+  if Flags.do_beautify() && loc<>dummy_loc then
     let (b,e) = unloc loc in
     comment b ++ pr x ++ comment e
   else pr x
diff --git a/lib/util.mli b/lib/util.mli
index 99ad3c03..3cd934e7 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(*i $Id: util.mli 11309 2008-08-06 10:30:35Z herbelin $ i*)
+(*i $Id: util.mli 11769 2009-01-08 17:59:22Z glondu $ i*)
 
 (*i*)
 open Pp
@@ -68,15 +68,18 @@ val pi3 : 'a * 'b * 'c -> 'c
 val is_letter : char -> bool
 val is_digit : char -> bool
 val is_ident_tail : char -> bool
+val is_blank : char -> bool
 
 (*s Strings. *)
 
 val explode : string -> string list
 val implode : string list -> string
+val strip : string -> string
 val string_index_from : string -> int -> string -> int
 val string_string_contains : where:string -> what:string -> bool
 val plural : int -> string -> string
 val ordinal : int -> string
+val split_string_at : char -> string -> string list
 
 val parse_loadpath : string -> string list
 
@@ -89,6 +92,7 @@ exception UnsupportedUtf8
 
 val classify_unicode : int -> utf8_status
 val check_ident : string -> unit
+val check_ident_soft : string -> unit
 val lowercase_first_char_utf8 : string -> string
 
 (*s Lists. *)
@@ -137,6 +141,7 @@ val list_for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool
 val list_except : 'a -> 'a list -> 'a list
 val list_remove : 'a -> 'a list -> 'a list
 val list_remove_first : 'a -> 'a list -> 'a list
+val list_remove_assoc_in_triple : 'a -> ('a * 'b * 'c) list -> ('a * 'b * 'c) list
 val list_for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
 val list_sep_last : 'a list -> 'a * 'a list
 val list_try_find_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b
@@ -145,7 +150,8 @@ val list_uniquize : 'a list -> 'a list
 (* merges two sorted lists and preserves the uniqueness property: *)
 val list_merge_uniq : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list
 val list_subset : 'a list -> 'a list -> bool
-val list_splitby : ('a -> bool) -> 'a list -> 'a list * 'a list
+val list_split_at : ('a -> bool) -> 'a list -> 'a list * 'a list
+val list_split_by : ('a -> bool) -> 'a list -> 'a list * 'a list
 val list_split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list
 val list_partition_by : ('a -> 'a -> bool) -> 'a list -> 'a list list
 val list_firstn : int -> 'a list -> 'a list
@@ -155,6 +161,7 @@ val list_skipn : int -> 'a list -> 'a list
 val list_addn : int -> 'a -> 'a list -> 'a list
 val list_prefix_of : 'a list -> 'a list -> bool
 val list_drop_prefix : 'a list -> 'a list -> 'a list
+val list_drop_last : 'a list -> 'a list
 (* [map_append f [x1; ...; xn]] returns [(f x1)@(f x2)@...@(f xn)] *)
 val list_map_append : ('a -> 'b list) -> 'a list -> 'b list
 val list_join_map : ('a -> 'b list) -> 'a list -> 'b list
@@ -175,6 +182,11 @@ val list_cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
 val list_cartesians : ('a -> 'b -> 'b) -> 'b -> 'a list list -> 'b list
 (* list_combinations [[a;b];[c;d]] returns [[a;c];[a;d];[b;c];[b;d]] *)
 val list_combinations : 'a list list -> 'a list list
+(* Keep only those products that do not return None *)
+val list_cartesian_filter :
+  ('a -> 'b -> 'c option) -> 'a list -> 'b list -> 'c list
+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
 
@@ -187,6 +199,7 @@ val array_for_all3 : ('a -> 'b -> 'c -> bool) ->
   'a array -> 'b array -> 'c array -> bool
 val array_for_all4 : ('a -> 'b -> 'c -> 'd -> bool) ->
   'a array -> 'b array -> 'c array -> 'd array -> bool
+val array_for_all_i : (int -> 'a -> bool) -> int -> 'a array -> bool
 val array_hd : 'a array -> 'a
 val array_tl : 'a array -> 'a array
 val array_last : 'a array -> 'a