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

23 files changed, 1185 insertions, 241 deletions

diff --git a/lib/bigint.ml b/lib/bigint.ml
index 5bcceb5c..7671b0fc 100644
--- a/lib/bigint.ml
+++ b/lib/bigint.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: bigint.ml 7305 2005-08-19 19:51:02Z letouzey $ *)
+(* $Id: bigint.ml 9821 2007-05-11 17:00:58Z aspiwack $ *)
 
 (*i*)
 open Pp
@@ -350,6 +350,29 @@ let is_pos_or_zero n = is_pos_or_zero (ints_of_z n)
 
 let pr_bigint n = str (to_string n)
 
+(* spiwack: computes n^m *)
+(* The basic idea of the algorithm is that n^(2m) = (n^2)^m *)
+(* In practice the algorithm performs :
+    k*n^0 = k
+    k*n^(2m) = k*(n*n)^m
+    k*n^(2m+1) = (n*k)*(n*n)^m *)
+let pow  =
+  let rec pow_aux odd_rest n m = (* odd_rest is the k from above *)
+    if is_neg_or_zero m then
+      odd_rest
+    else
+      let (quo,rem) = div2_with_rest m in
+      pow_aux
+	((* [if m mod 2 = 1]*)
+         if rem then 
+          mult n odd_rest
+	 else
+          odd_rest )
+	(* quo = [m/2] *)
+	(mult n n) quo 
+  in
+  pow_aux one
+
 (* Testing suite *)
 
 let check () =
diff --git a/lib/bigint.mli b/lib/bigint.mli
index 7a835a49..f6d3da7b 100644
--- a/lib/bigint.mli
+++ b/lib/bigint.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: bigint.mli 6616 2005-01-21 17:18:23Z herbelin $ i*)
+(*i $Id: bigint.mli 9821 2007-05-11 17:00:58Z aspiwack $ i*)
 
 (*i*)
 open Pp
@@ -42,4 +42,6 @@ val is_pos_or_zero : bigint -> bool
 val is_neg_or_zero : bigint -> bool
 val neg : bigint -> bigint
 
+val pow : bigint -> bigint -> bigint
+
 val pr_bigint : bigint -> std_ppcmds
diff --git a/lib/bstack.ml b/lib/bstack.ml
index b86dccf9..35bbf32b 100644
--- a/lib/bstack.ml
+++ b/lib/bstack.ml
@@ -6,19 +6,27 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: bstack.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
+(* $Id: bstack.ml 10441 2008-01-15 16:37:46Z lmamane $ *)
 
 (* Queues of a given length *)
 
 open Util
 
+(* - size  is the count of elements actually in the queue
+   - depth is the the amount of elements pushed in the queue (and not popped)
+   in particular, depth >= size always and depth > size if the queue overflowed
+   (and forgot older elements)
+ *)
+
 type 'a t = {mutable pos : int;
              mutable size : int;
+             mutable depth : int;
              stack : 'a array}
 
 let create depth e =
   {pos = 0;
    size = 1;
+   depth = 1;
    stack = Array.create depth e}
 
 (*
@@ -37,14 +45,16 @@ let decr_pos bs =
 let push bs e =
   incr_pos bs;
   incr_size bs;
+  bs.depth <- bs.depth + 1;
   bs.stack.(bs.pos) <- e
 	  
 let pop bs =
   if bs.size > 1 then begin
     bs.size <- bs.size - 1; 
+    bs.depth <- bs.depth - 1;
     let oldpos = bs.pos in
     decr_pos bs;
-    (* Release the memory at oldpos, by coyping what is at new pos *)
+    (* Release the memory at oldpos, by copying what is at new pos *)
     bs.stack.(oldpos) <- bs.stack.(bs.pos)
   end
 
@@ -60,4 +70,6 @@ let app_repl bs f =
   if bs.size = 0 then error "Nothing on the stack"
   else bs.stack.(bs.pos) <- f (bs.stack.(bs.pos))
 
-let depth bs = bs.size
+let depth bs = bs.depth
+
+let size bs = bs.size
diff --git a/lib/bstack.mli b/lib/bstack.mli
index f018d155..ca2b5f02 100644
--- a/lib/bstack.mli
+++ b/lib/bstack.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: bstack.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
+(*i $Id: bstack.mli 10441 2008-01-15 16:37:46Z lmamane $ i*)
 
 (* Bounded stacks. If the depth is [None], then there is no depth limit. *)
 
@@ -19,3 +19,4 @@ val app_repl : 'a t -> ('a -> 'a) -> unit
 val pop : 'a t -> unit
 val top : 'a t -> 'a
 val depth : 'a t -> int
+val size : 'a t -> int
diff --git a/lib/compat.ml4 b/lib/compat.ml4
index 372d2be3..40cffadb 100644
--- a/lib/compat.ml4
+++ b/lib/compat.ml4
@@ -6,13 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* Compatibility file depending on ocaml version *)
+(*i camlp4use: "pa_macro.cmo" i*)
 
-(* type loc is different in 3.08 *)
+(* Compatibility file depending on ocaml version *)
 
 IFDEF OCAML309 THEN DEFINE OCAML308 END
 
-IFDEF CAMLP5 THEN
+IFDEF CAMLP5 THEN 
 module M = struct 
 type loc = Stdpp.location
 let dummy_loc = Stdpp.dummy_loc
@@ -45,7 +45,7 @@ type token = Token.t
 type lexer = Token.lexer
 let using l x = l.Token.using x
 end
-ELSE
+ELSE 
 module M = struct
 type loc = int * int
 let dummy_loc = (0,0)
@@ -63,8 +63,8 @@ END
 
 type loc = M.loc
 let dummy_loc = M.dummy_loc
-let unloc = M.unloc
 let make_loc = M.make_loc
+let unloc = M.unloc
 let join_loc = M.join_loc
 type token = M.token
 type lexer = M.lexer
diff --git a/lib/edit.ml b/lib/edit.ml
index 03420992..380abfd8 100644
--- a/lib/edit.ml
+++ b/lib/edit.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: edit.ml 6947 2005-04-20 16:18:41Z coq $ *)
+(* $Id: edit.ml 10441 2008-01-15 16:37:46Z lmamane $ *)
 
 open Pp
 open Util
@@ -80,7 +80,7 @@ let undo e n =
     | None -> invalid_arg "Edit.undo"
     | Some d ->
 	let (bs,_) = Hashtbl.find e.buf d in
-	if Bstack.depth bs = 1 & n > 0 then
+	if n >= Bstack.size bs then
 	  errorlabstrm "Edit.undo" (str"Undo stack exhausted");
         repeat n Bstack.pop bs
 
@@ -102,15 +102,16 @@ let undo_todepth e n =
 	else () (* if there is no proof in progress, then n must be zero *)
     | Some d ->
 	let (bs,_) = Hashtbl.find e.buf d in
-	if Bstack.depth bs < n then
+	let ucnt = Bstack.depth bs - n in
+	if  ucnt >= Bstack.size bs then
 	  errorlabstrm "Edit.undo_todepth" (str"Undo stack would be exhausted");
-        repeat (Bstack.depth bs - n) Bstack.pop bs
+        repeat ucnt Bstack.pop bs
 
-let create e (d,b,c,udepth) =
+let create e (d,b,c,usize) =
   if Hashtbl.mem e.buf d then
     errorlabstrm "Edit.create" 
       (str"Already editing something of that name");
-  let bs = Bstack.create udepth b in
+  let bs = Bstack.create usize b in
   Hashtbl.add e.buf d (bs,c)
 
 let delete e d =
diff --git a/lib/options.ml b/lib/flags.ml
index 53a7e9cf..de971c7c 100644
--- a/lib/options.ml
+++ b/lib/flags.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: options.ml 10105 2007-08-30 16:53:32Z herbelin $ *)
+(*i $Id: flags.ml 11077 2008-06-09 11:26:32Z herbelin $ i*)
 
 open Util
 
@@ -32,6 +32,8 @@ let dont_load_proofs = ref false
 
 let raw_print = ref false
 
+let unicode_syntax = ref false
+
 (* Translate *)
 let translate = ref false
 let make_translate f = translate := f
@@ -63,6 +65,10 @@ let if_verbose f x = if not !silent then f x
 
 let hash_cons_proofs = ref true
 
+let warn = ref true
+let make_warn flag = warn := flag;  ()
+let if_warn f x = if !warn then f x
+
 (* The number of printed hypothesis in a goal *)
 
 let print_hyps_limit = ref (None : int option)
@@ -96,29 +102,31 @@ let dump_it () =
 
 let _ = at_exit dump_it
 
-(* Options 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 
  
-(* Options for external tools *)
+(* Flags.for external tools *)
+
+let subst_command_placeholder s t =
+  let buff = Buffer.create (String.length s + String.length t) in
+  let i = ref 0 in
+  while (!i < String.length s) do
+    if s.[!i] = '%' & !i+1 < String.length s & s.[!i+1] = 's'
+    then (Buffer.add_string buff t;incr i)
+    else Buffer.add_char buff s.[!i];
+    incr i
+  done;
+  Buffer.contents buff
 
 let browser_cmd_fmt =
  try
   let coq_netscape_remote_var = "COQREMOTEBROWSER" in
-  let coq_netscape_remote = Sys.getenv coq_netscape_remote_var in
-  let i = Util.string_index_from coq_netscape_remote 0 "%s" in
-  let pre = String.sub coq_netscape_remote 0 i in
-  let post = String.sub coq_netscape_remote (i + 2)
-              (String.length coq_netscape_remote - (i + 2)) in
-   if Util.string_string_contains ~where:post ~what:"%s" then
-    error ("The environment variable \"" ^
-           coq_netscape_remote_var ^
-           "\" must contain exactly one placeholder \"%s\".")
-   else pre,post
+  Sys.getenv coq_netscape_remote_var
  with
   Not_found ->
    if Sys.os_type = "Win32"
-   then "C:\\PROGRA~1\\INTERN~1\\IEXPLORE ", ""
-   else "firefox -remote \"OpenURL(", ")\""
+   then "C:\\PROGRA~1\\INTERN~1\\IEXPLORE %s"
+   else "firefox -remote \"OpenURL(%s,new-tab)\" || firefox %s &"
diff --git a/lib/options.mli b/lib/flags.mli
index 30d585fb..1fcae990 100644
--- a/lib/options.mli
+++ b/lib/flags.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: options.mli 9191 2006-09-29 15:45:42Z courtieu $ i*)
+(*i $Id: flags.mli 10921 2008-05-12 12:27:25Z msozeau $ i*)
 
 (* Global options of the system. *)
 
@@ -27,6 +27,8 @@ val dont_load_proofs : bool ref
 
 val raw_print : bool ref
 
+val unicode_syntax : bool ref
+
 val translate : bool ref
 val make_translate : bool -> unit
 val do_translate : unit -> bool
@@ -40,6 +42,9 @@ val silently : ('a -> 'b) -> 'a -> 'b
 val if_silent : ('a -> unit) -> 'a -> unit
 val if_verbose : ('a -> unit) -> 'a -> unit
 
+val make_warn : bool -> unit
+val if_warn : ('a -> unit) -> 'a -> unit
+
 val hash_cons_proofs : bool ref
 
 (* Temporary activate an option ('c must be an atomic type) *)
@@ -65,7 +70,8 @@ val boxed_definitions : unit -> bool
 
 (* Options for external tools *)
 
-(* Returns head and tail of printf string format *)
-(* ocaml doesn't allow not applied formats *)
-val browser_cmd_fmt : string * string
+(* Returns string format for default browser to use from Coq or CoqIDE *)
+val browser_cmd_fmt : string
  
+(* Substitute %s in the first chain by the second chain *)
+val subst_command_placeholder : string -> string -> string
diff --git a/lib/gmap.ml b/lib/gmap.ml
index 884305d9..7a4cb56e 100644
--- a/lib/gmap.ml
+++ b/lib/gmap.ml
@@ -5,7 +5,7 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(* $Id: gmap.ml 7925 2006-01-24 23:20:39Z herbelin $ *)
+(* $Id: gmap.ml 10250 2007-10-23 15:02:23Z aspiwack $ *)
 
 (* Maps using the generic comparison function of ocaml. Code borrowed from
    the ocaml standard library (Copyright 1996, INRIA). *)
@@ -16,6 +16,8 @@
 
     let empty = Empty
 
+    let is_empty = function Empty -> true | _ -> false
+
     let height = function
         Empty -> 0
       | Node(_,_,_,_,h) -> h
diff --git a/lib/gmap.mli b/lib/gmap.mli
index 79958fab..5186cff4 100644
--- a/lib/gmap.mli
+++ b/lib/gmap.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: gmap.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
+(*i $Id: gmap.mli 10250 2007-10-23 15:02:23Z aspiwack $ i*)
 
 (* Maps using the generic comparison function of ocaml. Same interface as
    the module [Map] from the ocaml standard library. *)
@@ -14,6 +14,7 @@
 type ('a,'b) t
 
 val empty : ('a,'b) t
+val is_empty : ('a,'b) t -> bool
 val add : 'a -> 'b -> ('a,'b) t -> ('a,'b) t
 val find : 'a -> ('a,'b) t -> 'b
 val remove : 'a -> ('a,'b) t -> ('a,'b) t
diff --git a/lib/gset.mli b/lib/gset.mli
index 0f14368f..5c794381 100644
--- a/lib/gset.mli
+++ b/lib/gset.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: gset.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
+(*i $Id: gset.mli 10840 2008-04-23 21:29:34Z herbelin $ i*)
 
 (* Sets using the generic comparison function of ocaml. Same interface as
    the module [Set] from the ocaml standard library. *)
@@ -26,7 +26,7 @@ val compare : 'a t -> 'a t -> int
 val equal : 'a t -> 'a t -> bool
 val subset : 'a t -> 'a t -> bool
 val iter : ('a -> unit) -> 'a t -> unit
-val fold : ('a -> 'a -> 'a) -> 'a t -> 'a -> 'a
+val fold : ('a -> 'b -> 'b) -> 'a t -> 'b -> 'b
 val cardinal : 'a t -> int
 val elements : 'a t -> 'a list
 val min_elt : 'a t -> 'a
diff --git a/lib/option.ml b/lib/option.ml
new file mode 100644
index 00000000..34749b8c
--- /dev/null
+++ b/lib/option.ml
@@ -0,0 +1,165 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(*i $Id: option.ml 10739 2008-04-01 14:45:20Z herbelin $ i*)
+
+(** Module implementing basic combinators for OCaml option type.
+   It tries follow closely the style of OCaml standard library.
+
+   Actually, some operations have the same name as [List] ones:
+   they actually are similar considering ['a option] as a type
+   of lists with at most one element. *)
+
+(** [has_some x] is [true] if [x] is of the form [Some y] and [false]
+    otherwise.  *)
+let has_some = function
+  | None -> false
+  | _ -> true
+  
+exception IsNone
+
+(** [get x] returns [y] where [x] is [Some y]. It raises IsNone
+    if [x] equals [None]. *)
+let get = function
+  | Some y -> y
+  | _ -> raise IsNone
+
+(** [make x] returns [Some x]. *)
+let make x = Some x
+
+(** [init b x] returns [Some x] if [b] is [true] and [None] otherwise. *)
+let init b x =
+  if b then 
+    Some x
+  else
+    None
+    
+
+(** [flatten x] is [Some y] if [x] is [Some (Some y)] and [None] otherwise. *)
+let flatten = function
+  | Some (Some y) -> Some y
+  | _ -> None
+
+
+(** {6 "Iterators"} ***)
+
+(** [iter f x] executes [f y] if [x] equals [Some y]. It does nothing 
+    otherwise. *)
+let iter f = function
+  | Some y -> f y
+  | _ -> ()
+
+
+exception Heterogeneous
+
+(** [iter2 f x y] executes [f z w] if [x] equals [Some z] and [y] equals
+    [Some w]. It does nothing if both [x] and [y] are [None]. And raises
+    [Heterogeneous] otherwise. *)
+let iter2 f x y = 
+  match x,y with
+  | Some z, Some w -> f z w
+  | None,None -> ()
+  | _,_ -> raise Heterogeneous
+
+(** [map f x] is [None] if [x] is [None] and [Some (f y)] if [x] is [Some y]. *)
+let map f = function
+  | Some y -> Some (f y)
+  | _ -> None
+
+(** [smartmap f x] does the same as [map f x] except that it tries to share
+    some memory. *)
+let smartmap f = function
+  | Some y as x -> let y' = f y in if y' == y then x else Some y'
+  | _ -> None
+
+(** [fold_left f a x] is [f a y] if [x] is [Some y], and [a] otherwise. *)
+let fold_left f a = function
+  | Some y -> f a y
+  | _ -> a
+
+(** [fold_left2 f a x y] is [f z w] if [x] is [Some z] and [y] is [Some w].
+    It is [a] if both [x] and [y] are [None]. Otherwise it raises
+    [Heterogeneous]. *)
+let fold_left2 f a x y =
+  match x,y with
+  | Some x, Some y -> f a x y
+  | None, None -> a
+  | _ -> raise Heterogeneous
+
+(** [fold_right f x a] is [f y a] if [x] is [Some y], and [a] otherwise. *)
+let fold_right f x a = 
+  match x with
+  | Some y -> f y a
+  | _ -> a
+
+
+(** {6 More Specific operations} ***)
+
+(** [default a x] is [y] if [x] is [Some y] and [a] otherwise. *)
+let default a = function
+  | Some y -> y
+  | _ -> a
+
+(** [lift f x] is the same as [map f x]. *)
+let lift = map
+
+(** [lift_right f a x] is [Some (f a y)] if [x] is [Some y], and 
+    [None] otherwise. *)
+let lift_right f a = function
+  | Some y -> Some (f a y)
+  | _ -> None
+
+(** [lift_left f x a] is [Some (f y a)] if [x] is [Some y], and 
+    [None] otherwise. *)
+let lift_left f x a =
+  match x with
+  | Some y -> Some (f y a)
+  | _ -> None
+
+(** [lift2 f x y] is [Some (f z w)] if [x] equals [Some z] and [y] equals 
+    [Some w]. It is [None] otherwise. *)
+let lift2 f x y =
+  match x,y with
+  | Some z, Some w -> Some (f z w)
+  | _,_ -> None
+
+
+
+(** {6 Operations with Lists} *)
+
+module List =
+ struct 
+  (** [List.cons x l] equals [y::l] if [x] is [Some y] and [l] otherwise. *)
+  let cons x l =
+    match x with
+    | Some y -> y::l
+    | _ -> l
+ 
+  (** [List.flatten l] is the list of all the [y]s such that [l] contains
+      [Some y] (in the same order). *)
+  let rec flatten = function
+    | x::l -> cons x (flatten l)
+    | [] -> [] 
+end
+
+
+
+(** {6 Miscelaneous Primitives} *)
+
+module Misc =
+ struct
+  (** [Misc.compare f x y] lifts the equality predicate [f] to 
+      option types. That is, if both [x] and [y] are [None] then 
+      it returns [true], if they are bothe [Some _] then
+      [f] is called. Otherwise it returns [false]. *)
+   let compare f x y =
+     match x,y with
+     | None, None -> true
+     | Some z, Some w -> f z w
+     | _,_ -> false
+end
diff --git a/lib/option.mli b/lib/option.mli
new file mode 100644
index 00000000..d9c18d88
--- /dev/null
+++ b/lib/option.mli
@@ -0,0 +1,112 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(* $Id: option.mli 10739 2008-04-01 14:45:20Z herbelin $ *)
+
+(** Module implementing basic combinators for OCaml option type.
+   It tries follow closely the style of OCaml standard library.
+
+   Actually, some operations have the same name as [List] ones:
+   they actually are similar considering ['a option] as a type
+   of lists with at most one element. *)
+
+(** [has_some x] is [true] if [x] is of the form [Some y] and [false]
+    otherwise.  *)
+val has_some : 'a option -> bool
+  
+exception IsNone
+
+(** [get x] returns [y] where [x] is [Some y]. It raises IsNone
+    if [x] equals [None]. *)
+val get : 'a option -> 'a
+
+(** [make x] returns [Some x]. *)
+val make : 'a -> 'a option
+
+(** [init b x] returns [Some x] if [b] is [true] and [None] otherwise. *)
+val init : bool -> 'a -> 'a option
+
+(** [flatten x] is [Some y] if [x] is [Some (Some y)] and [None] otherwise. *)
+val flatten : 'a option option -> 'a option
+
+
+(** {6 "Iterators"} ***)
+
+(** [iter f x] executes [f y] if [x] equals [Some y]. It does nothing 
+    otherwise. *)
+val iter : ('a -> unit) -> 'a option -> unit
+
+exception Heterogeneous
+
+(** [iter2 f x y] executes [f z w] if [x] equals [Some z] and [y] equals
+    [Some w]. It does nothing if both [x] and [y] are [None]. And raises
+    [Heterogeneous] otherwise. *)
+val iter2 : ('a -> 'b -> unit) -> 'a option -> 'b option -> unit
+
+(** [map f x] is [None] if [x] is [None] and [Some (f y)] if [x] is [Some y]. *)
+val map : ('a -> 'b) -> 'a option -> 'b option
+
+(** [smartmap f x] does the same as [map f x] except that it tries to share
+    some memory. *)
+val smartmap : ('a -> 'a) -> 'a option -> 'a option
+
+(** [fold_left f a x] is [f a y] if [x] is [Some y], and [a] otherwise. *)
+val fold_left : ('b -> 'a -> 'b) -> 'b -> 'a option -> 'b
+
+(** [fold_left2 f a x y] is [f z w] if [x] is [Some z] and [y] is [Some w].
+    It is [a] if both [x] and [y] are [None]. Otherwise it raises
+    [Heterogeneous]. *)
+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
+
+
+(** {6 More Specific Operations} ***)
+
+(** [default a x] is [y] if [x] is [Some y] and [a] otherwise. *)
+val default : 'a -> 'a option -> 'a
+
+(** [lift] is the same as {!map}. *)
+val lift : ('a -> 'b) -> 'a option -> 'b option
+
+(** [lift_right f a x] is [Some (f a y)] if [x] is [Some y], and 
+    [None] otherwise. *)
+val lift_right : ('a -> 'b -> 'c) -> 'a -> 'b option -> 'c option
+
+(** [lift_left f x a] is [Some (f y a)] if [x] is [Some y], and 
+    [None] otherwise. *)
+val lift_left : ('a -> 'b -> 'c) -> 'a option -> 'b -> 'c option
+
+(** [lift2 f x y] is [Some (f z w)] if [x] equals [Some z] and [y] equals 
+    [Some w]. It is [None] otherwise. *)
+val lift2 : ('a -> 'b -> 'c) -> 'a option -> 'b option -> 'c option
+
+
+(** {6 Operations with Lists} *)
+
+module List : sig
+  (** [List.cons x l] equals [y::l] if [x] is [Some y] and [l] otherwise. *)
+  val cons : 'a option -> 'a list -> 'a list
+
+  (** [List.flatten l] is the list of all the [y]s such that [l] contains
+      [Some y] (in the same order). *)
+  val flatten : 'a option list -> 'a list
+end
+
+
+(** {6 Miscelaneous Primitives} *)
+
+module Misc : sig
+  (** [Misc.compare f x y] lifts the equality predicate [f] to 
+      option types. That is, if both [x] and [y] are [None] then 
+      it returns [true], if they are bothe [Some _] then
+      [f] is called. Otherwise it returns [false]. *)
+   val compare : ('a -> 'a -> bool) -> 'a option -> 'a option -> bool
+end
+
diff --git a/lib/pp.ml4 b/lib/pp.ml4
index 88efc5f2..616302ac 100644
--- a/lib/pp.ml4
+++ b/lib/pp.ml4
@@ -6,17 +6,18 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pp.ml4 8747 2006-04-27 16:00:49Z courtieu $ *)
+(* $Id: pp.ml4 10803 2008-04-16 09:30:05Z cek $ *)
 
 open Pp_control
 
 (* This should not be used outside of this file. Use
-   Options.print_emacs instead. This one is updated when reading
+   Flags.print_emacs instead. This one is updated when reading
    command line options. This was the only way to make [Pp] depend on
-   an option without creating a circularity: [Options] -> [Util] ->
-   [Pp] -> [Options] *)
+   an option without creating a circularity: [Flags. -> [Util] ->
+   [Pp] -> [Flags. *)
 let print_emacs = ref false
 let make_pp_emacs() = print_emacs:=true
+let make_pp_nonemacs() = print_emacs:=false
 
 (* The different kinds of blocks are: 
    \begin{description}
@@ -129,19 +130,17 @@ let align () = [< 'Ppcmd_print_break (0,0) >]
 let int n = str (string_of_int n)
 let real r = str (string_of_float r)
 let bool b = str (string_of_bool b)
-
-(* In new syntax only double quote char is escaped by repeating it *)
-let rec escape_string s =
-  let rec escape_at s i =
-    if i<0 then s
-    else if s.[i] == '"' then
-      let s' = String.sub s 0 i^"\""^String.sub s i (String.length s - i) in
-      escape_at s' (i-1)
-    else escape_at s (i-1) in
-  escape_at s (String.length s - 1)
-
-let qstring s = str ("\""^escape_string s^"\"")
-let qs = qstring
+let strbrk s =
+  let rec aux p n =
+    if n < String.length s then 
+      if s.[n] = ' ' then
+	if p=n then [< spc (); aux (n+1) (n+1) >]
+	else [< str (String.sub s p (n-p)); spc (); aux (n+1) (n+1) >]
+      else aux p (n+1)
+    else if p=n then [< >] else [< str (String.sub s p (n-p)) >]
+  in aux 0 0
+
+let ismt s = try let _ = Stream.empty s in true with Stream.Failure -> false
 
 (* boxing commands *)
 let h n s = [< 'Ppcmd_box(Pp_hbox n,s) >]
@@ -161,6 +160,41 @@ let tclose () = [< 'Ppcmd_close_tbox >]
 
 let (++) = Stream.iapp
 
+(* In new syntax only double quote char is escaped by repeating it *)
+let rec escape_string s =
+  let rec escape_at s i =
+    if i<0 then s
+    else if s.[i] == '"' then
+      let s' = String.sub s 0 i^"\""^String.sub s i (String.length s - i) in
+      escape_at s' (i-1)
+    else escape_at s (i-1) in
+  escape_at s (String.length s - 1)
+
+let qstring s = str ("\""^escape_string s^"\"")
+let qs = qstring
+let quote s = h 0 (str "\"" ++ s ++ str "\"")
+
+let rec xmlescape ppcmd =
+  let rec escape what withwhat (len, str) =
+    try
+      let pos = String.index str what in
+      let (tlen, tail) =
+        escape what withwhat ((len - pos - 1),
+          (String.sub str (pos + 1) (len - pos - 1)))
+      in
+      (pos + tlen + String.length withwhat, String.sub str 0 pos ^ withwhat ^ tail)
+    with Not_found -> (len, str)
+  in
+  match ppcmd with
+    | Ppcmd_print (len, str) ->
+        Ppcmd_print (escape '"' "&quot;"
+          (escape '<' "&lt;" (escape '&' "&amp;" (len, str))))
+      (* In XML we always print whole content so we can npeek the whole stream *)
+    | Ppcmd_box (x, str) -> Ppcmd_box (x, Stream.of_list
+        (List.map xmlescape (Stream.npeek max_int str)))
+    | x -> x
+
+
 (* This flag tells if the last printed comment ends with a newline, to
   avoid empty lines *)
 let com_eol = ref false
@@ -242,7 +276,7 @@ let pp_dirs ft =
 (* pretty print on stdout and stderr *)
 
 let pp_std_dirs = pp_dirs !std_ft
-let pp_err_dirs = pp_dirs err_ft
+let pp_err_dirs = pp_dirs !err_ft
 
 let ppcmds x = Ppdir_ppcmds x
 
@@ -251,11 +285,13 @@ let emacs_warning_start_string = String.make 1 (Char.chr 254)
 let emacs_warning_end_string = String.make 1 (Char.chr 255)
 
 let warnstart() = 
-  if not !print_emacs then str "" else str emacs_warning_start_string
+  if not !print_emacs then mt() else str emacs_warning_start_string
 
 let warnend() = 
-  if not !print_emacs then str "" else str emacs_warning_end_string
-  
+  if not !print_emacs then mt() else str emacs_warning_end_string
+
+let warnbody strm =
+  [< warnstart() ; hov 0 (str "Warning: " ++ strm) ; warnend() >]
 
 (* pretty printing functions WITHOUT FLUSH *)
 let pp_with ft strm =
@@ -264,15 +300,17 @@ let pp_with ft strm =
 let ppnl_with ft strm =
   pp_dirs ft [< 'Ppdir_ppcmds [< strm ; 'Ppcmd_force_newline >] >]
 
-let warning_with ft string =
-  ppnl_with ft [< warnstart() ; str "Warning: " ; str string ; warnend() >]
+let default_warn_with ft strm = ppnl_with ft (warnbody strm)
+
+let pp_warn_with = ref default_warn_with
 
-let warn_with ft pps =
-  ppnl_with ft [< warnstart() ; str "Warning: " ; pps ; warnend() >]
+let set_warning_function pp_warn = pp_warn_with := pp_warn
 
-let pp_flush_with ft =
-  Format.pp_print_flush ft
+let warn_with ft strm = !pp_warn_with ft strm
 
+let warning_with ft string = warn_with ft (str string)
+
+let pp_flush_with ft = Format.pp_print_flush ft
 
 (* pretty printing functions WITH FLUSH *)
 let msg_with ft strm =
@@ -281,25 +319,23 @@ let msg_with ft strm =
 let msgnl_with ft strm =
   pp_dirs ft [< 'Ppdir_ppcmds strm ; 'Ppdir_print_newline >]
 
-let msg_warning_with ft strm=
-  pp_dirs ft [< 'Ppdir_ppcmds [< warnstart() ; str "Warning: "; strm ; warnend() >]; 
-		'Ppdir_print_newline >]
-
+let msg_warning_with ft strm =
+  msgnl_with ft (warnbody strm)
 
 (* pretty printing functions WITHOUT FLUSH *)
-let pp        x = pp_with !std_ft x
+let pp        x = pp_with   !std_ft x
 let ppnl      x = ppnl_with !std_ft x
-let pperr     = pp_with err_ft
-let pperrnl   = ppnl_with err_ft
-let message s = ppnl (str s)
-let warning   x = warning_with err_ft x
-let warn      x = warn_with err_ft x
+let pperr     x = pp_with   !err_ft x
+let pperrnl   x = ppnl_with !err_ft x
+let message   s = ppnl      (str s)
+let warning   x = warning_with !err_ft x
+let warn      x = warn_with    !err_ft x
 let pp_flush  x = Format.pp_print_flush !std_ft x
 let flush_all() = flush stderr; flush stdout; pp_flush()
 
 (* pretty printing functions WITH FLUSH *)
 let msg x = msg_with !std_ft x
 let msgnl x = msgnl_with !std_ft x
-let msgerr = msg_with err_ft
-let msgerrnl = msgnl_with err_ft
-let msg_warning x = msg_warning_with err_ft x
+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
diff --git a/lib/pp.mli b/lib/pp.mli
index e240fd2d..85b8345d 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: pp.mli 8748 2006-04-27 16:01:26Z courtieu $ i*)
+(*i $Id: pp.mli 10803 2008-04-16 09:30:05Z cek $ i*)
 
 (*i*)
 open Pp_control
@@ -16,6 +16,7 @@ open Pp_control
    chars inserted at some places). This function should called once in
    module [Options], that's all. *)
 val make_pp_emacs:unit -> unit
+val make_pp_nonemacs:unit -> unit
 
 (* Pretty-printers. *)
 
@@ -34,6 +35,7 @@ val fnl : unit -> std_ppcmds
 val pifb : unit -> std_ppcmds
 val ws : int -> std_ppcmds
 val mt : unit -> std_ppcmds
+val ismt : std_ppcmds -> bool
 
 val comment : int -> std_ppcmds
 val comments : ((int * int) * string) list ref
@@ -52,6 +54,10 @@ val real : float -> std_ppcmds
 val bool : bool -> std_ppcmds
 val qstring : string -> std_ppcmds
 val qs : string -> std_ppcmds
+val quote : std_ppcmds -> std_ppcmds
+val strbrk : string -> std_ppcmds
+
+val xmlescape : ppcmd -> ppcmd
 
 (*s Boxing commands. *)
 
@@ -79,6 +85,8 @@ val warning_with : Format.formatter -> string -> unit
 val warn_with : Format.formatter -> std_ppcmds -> unit
 val pp_flush_with : Format.formatter -> unit -> unit
 
+val set_warning_function : (Format.formatter -> std_ppcmds -> unit) -> unit 
+
 (*s Pretty-printing functions \emph{with flush}. *)
 
 val msg_with : Format.formatter -> std_ppcmds -> unit
diff --git a/lib/pp_control.ml b/lib/pp_control.ml
index 7632d736..7aa05975 100644
--- a/lib/pp_control.ml
+++ b/lib/pp_control.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pp_control.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
+(* $Id: pp_control.ml 10917 2008-05-10 16:35:46Z herbelin $ *)
 
 (* Parameters of pretty-printing *)
 
@@ -89,10 +89,11 @@ let with_output_to ch =
 let std_ft = ref Format.std_formatter
 let _ = set_dflt_gp !std_ft
 
-let err_ft = with_output_to stderr
+let err_ft = ref Format.err_formatter
+let _ = set_gp !err_ft deep_gp
 
-let deep_ft = with_output_to stdout
-let _ = set_gp deep_ft deep_gp
+let deep_ft = ref (with_output_to stdout)
+let _ = set_gp !deep_ft deep_gp
 
 (* For parametrization through vernacular *)
 let default = Format.pp_get_max_boxes !std_ft ()
diff --git a/lib/pp_control.mli b/lib/pp_control.mli
index 7e25e561..f245d942 100644
--- a/lib/pp_control.mli
+++ b/lib/pp_control.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: pp_control.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
+(*i $Id: pp_control.mli 10917 2008-05-10 16:35:46Z herbelin $ i*)
 
 (* Parameters of pretty-printing. *)
 
@@ -37,8 +37,8 @@ val with_fp : 'a pp_formatter_params -> Format.formatter
 val with_output_to : out_channel -> Format.formatter
 
 val std_ft : Format.formatter ref
-val err_ft : Format.formatter
-val deep_ft : Format.formatter
+val err_ft : Format.formatter ref
+val deep_ft : Format.formatter ref
 
 (*s For parametrization through vernacular. *)
 
diff --git a/lib/rtree.ml b/lib/rtree.ml
index ab689be1..4742a90d 100644
--- a/lib/rtree.ml
+++ b/lib/rtree.ml
@@ -6,11 +6,15 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: rtree.ml 8648 2006-03-18 15:37:14Z herbelin $ i*)
+(*i $Id: rtree.ml 10690 2008-03-18 13:30:04Z barras $ i*)
+
+open Util
 
 
 (* Type of regular trees:
    - Param denotes tree variables (like de Bruijn indices)
+     the first int is the depth of the occurrence, and the second int
+     is the index in the array of trees introduced at that depth
    - Node denotes the usual tree node, labelled with 'a
    - Rec(j,v1..vn) introduces infinite tree. It denotes
      v(j+1) with parameters 0..n-1 replaced by
@@ -19,55 +23,87 @@
      current Rec node (as usual in de Bruijn binding system)
  *)
 type 'a t =
-    Param of int 
+    Param of int * int
   | Node of 'a * 'a t array
   | Rec of int * 'a t array
 
 (* Building trees *)
-let mk_param i = Param i
+let mk_rec_calls i = Array.init i (fun j -> Param(0,j))
 let mk_node lab sons = Node (lab, sons)
 
-(* Given a vector of n bodies, builds the n mutual recursive trees.
-   Recursive calls are made with parameters 0 to n-1. We check
-   the bodies actually build something by checking it is not
-   directly one of the parameters 0 to n-1. *)
-let mk_rec defs =
-  Array.mapi
-    (fun i d ->
-      (match d with
-          Param k when k < Array.length defs -> failwith "invalid rec call"
-        | _ -> ());
-      Rec(i,defs))
-    defs
-
 (* The usual lift operation *)
 let rec lift_rtree_rec depth n = function
-    Param i -> if i < depth then Param i else Param (i+n)
+    Param (i,j) as t -> if i < depth then t else Param (i+n,j)
   | Node (l,sons) -> Node (l,Array.map (lift_rtree_rec depth n) sons)
   | Rec(j,defs) ->
-      Rec(j, Array.map (lift_rtree_rec (depth+Array.length defs) n) defs)
+      Rec(j, Array.map (lift_rtree_rec (depth+1) n) defs)
 
 let lift n t = if n=0 then t else lift_rtree_rec 0 n t
 
 (* The usual subst operation *)
 let rec subst_rtree_rec depth sub = function
-    Param i ->
-      if i < depth then Param i
-      else if i-depth < Array.length sub then lift depth sub.(i-depth)
-      else Param (i-Array.length sub)
+    Param (i,j) as t ->
+      if i < depth then t
+      else if i-depth < Array.length sub then
+        lift depth sub.(i-depth).(j)
+      else Param (i-Array.length sub,j)
   | Node (l,sons) -> Node (l,Array.map (subst_rtree_rec depth sub) sons)
   | Rec(j,defs) ->
-      Rec(j, Array.map (subst_rtree_rec (depth+Array.length defs) sub) defs)
+      Rec(j, Array.map (subst_rtree_rec (depth+1) sub) defs)
+
+let subst_rtree sub t = subst_rtree_rec 0 [|sub|] t
+
+(* To avoid looping, we must check that every body introduces a node 
+   or a parameter *)
+let rec expand = function
+  | Rec(j,defs) ->
+      let sub = Array.init (Array.length defs) (fun i -> Rec(i,defs)) in
+      expand (subst_rtree sub defs.(j))
+  | t -> t
+
+(* Given a vector of n bodies, builds the n mutual recursive trees.
+   Recursive calls are made with parameters (0,0) to (0,n-1). We check
+   the bodies actually build something by checking it is not
+   directly one of the parameters of depth 0. Some care is taken to
+   accept definitions like  rec X=Y and Y=f(X,Y) *)
+let mk_rec defs =
+  let rec check histo d =
+    match expand d with
+        Param(0,j) when List.mem j histo -> failwith "invalid rec call"
+      | Param(0,j) -> check (j::histo) defs.(j)
+      | _ -> () in
+  Array.mapi (fun i d -> check [i] d; Rec(i,defs)) defs
+(*
+let v(i,j) = lift i (mk_rec_calls(j+1)).(j);;
+let r = (mk_rec[|(mk_rec[|v(1,0)|]).(0)|]).(0);;
+let r = mk_rec[|v(0,1);v(1,0)|];;
+the last one should be accepted
+*)
+
+(* Tree destructors, expanding loops when necessary *)
+let dest_param t = 
+  match expand t with
+      Param (i,j) -> (i,j)
+    | _ -> failwith "Rtree.dest_param"
+
+let dest_node t = 
+  match expand t with
+      Node (l,sons) -> (l,sons)
+    | _ -> failwith "Rtree.dest_node"
+
+let is_node t = 
+  match expand t with
+      Node _ -> true
+    | _ -> false
 
-let subst_rtree sub t = subst_rtree_rec 0 sub t
 
 let rec map f t = match t with
-    Param i -> Param i
+    Param(i,j) -> Param(i,j)
   | Node (a,sons) -> Node (f a, Array.map (map f) sons)
   | Rec(j,defs) -> Rec (j, Array.map (map f) defs)
 
 let rec smartmap f t = match t with
-    Param i -> t
+    Param _ -> t
   | Node (a,sons) -> 
       let a'=f a and sons' = Util.array_smartmap (map f) sons in
 	if a'==a && sons'==sons then
@@ -81,43 +117,61 @@ let rec smartmap f t = match t with
 	else
 	  Rec(j,defs')
 
-(* To avoid looping, we must check that every body introduces a node 
-   or a parameter *)
-let rec expand_rtree = function
-  | Rec(j,defs) ->
-      let sub = Array.init (Array.length defs) (fun i -> Rec(i,defs)) in
-      expand_rtree (subst_rtree sub defs.(j))
-  | t -> t
-
-(* Tree destructors, expanding loops when necessary *)
-let dest_param t = 
-  match expand_rtree t with
-      Param i -> i
-    | _ -> failwith "dest_param"
-
-let dest_node t = 
-  match expand_rtree t with
-      Node (l,sons) -> (l,sons)
-    | _ -> failwith "dest_node"
-
-(* Tests if a given tree is infinite or not. It proceeds *)
-let rec is_infinite = function
-    Param i -> i = (-1)
-  | Node(_,sons) -> Util.array_exists is_infinite sons
-  | Rec(j,defs) ->
-      let newdefs =
-        Array.mapi (fun i def -> if i=j then Param (-1) else def) defs in
-      let sub =
-        Array.init (Array.length defs)
-          (fun i -> if i=j then Param (-1) else Rec(i,newdefs)) in
-      is_infinite (subst_rtree sub defs.(j))
+(* Fixpoint operator on trees:
+   f is the body of the fixpoint. Arguments passed to f are:
+   - a boolean telling if the subtree has already been seen
+   - the current subtree
+   - a function to make recursive calls on subtrees
+ *)
+let fold f t =
+  let rec fold histo t =
+    let seen = List.mem t histo in
+    let nhisto = if not seen then t::histo else histo in
+    f seen (expand t) (fold nhisto) in
+  fold [] t
+
+
+(* Tests if a given tree is infinite, i.e. has an branch of infinte length. *)
+let is_infinite t = fold
+  (fun seen t is_inf ->
+    seen ||
+    (match t with
+        Node(_,v) -> array_exists is_inf v
+      | Param _ -> false
+      | _ -> assert false))
+  t
+
+let fold2 f t x =
+  let rec fold histo t x =
+    let seen = List.mem (t,x) histo in
+    let nhisto = if not seen then (t,x)::histo else histo in
+    f seen (expand t) x (fold nhisto) in
+  fold [] t x
+
+let compare_rtree f = fold2
+  (fun seen t1 t2 cmp ->
+    seen ||
+    let b = f t1 t2 in
+    if b < 0 then false
+    else if b > 0 then true
+    else match expand t1, expand t2 with
+        Node(_,v1), Node(_,v2) when Array.length v1 = Array.length v2 ->
+          array_for_all2 cmp v1 v2
+      | _ -> false)
+
+let eq_rtree cmp t1 t2 =
+  t1 == t2 || t1=t2 ||
+  compare_rtree
+    (fun t1 t2 ->
+      if cmp (fst(dest_node t1)) (fst(dest_node t2)) then 0
+      else (-1)) t1 t2
 
 (* Pretty-print a tree (not so pretty) *)
 open Pp
 
 let rec pp_tree prl t =
   match t with
-      Param k -> str"#"++int k
+      Param (i,j) -> str"#"++int i++str","++int j
     | Node(lab,[||]) -> hov 2 (str"("++prl lab++str")")
     | Node(lab,v) ->
         hov 2 (str"("++prl lab++str","++brk(1,0)++
diff --git a/lib/rtree.mli b/lib/rtree.mli
index 7be96652..b61e6965 100644
--- a/lib/rtree.mli
+++ b/lib/rtree.mli
@@ -6,35 +6,74 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: rtree.mli 7493 2005-11-02 22:12:16Z mohring $ i*)
+(*i $Id: rtree.mli 10690 2008-03-18 13:30:04Z barras $ i*)
 
 (* Type of regular tree with nodes labelled by values of type 'a *)
-
+(* The implementation uses de Bruijn indices, so binding capture
+   is avoided by the lift operator (see example below) *)
 type 'a t 
 
 (* Building trees *)
-(* build a recursive call *) 
-val mk_param : int -> 'a t
+
 (* build a node given a label and the vector of sons *)
 val mk_node  : 'a -> 'a t array -> 'a t
-(* build mutually dependent trees *)
+
+(* Build mutually recursive trees:
+    X_1 = f_1(X_1,..,X_n) ... X_n = f_n(X_1,..,X_n)
+   is obtained by the following pseudo-code
+   let vx = mk_rec_calls n in
+   let [|x_1;..;x_n|] =
+      mk_rec[|f_1(vx.(0),..,vx.(n-1);..;f_n(vx.(0),..,vx.(n-1))|]
+
+  First example: build  rec X = a(X,Y) and Y = b(X,Y,Y)
+  let [|vx;vy|] = mk_rec_calls 2 in
+  let [|x;y|] = mk_rec [|mk_node a [|vx;vy|]; mk_node b [|vx;vy;vy|]|]
+
+  Another example: nested recursive trees rec Y = b(rec X = a(X,Y),Y,Y)
+  let [|vy|] = mk_rec_calls 1 in
+  let [|vx|] = mk_rec_calls 1 in
+  let [|x|] = mk_rec[|mk_node a [|vx;lift 1 vy|]
+  let [|y|] = mk_rec[|mk_node b [|x;vy;vy|]|]
+  (note the lift to avoid
+ *)
+val mk_rec_calls : int -> 'a t array
 val mk_rec   : 'a t array -> 'a t array
 
 (* [lift k t] increases of [k] the free parameters of [t]. Needed
    to avoid captures when a tree appears under [mk_rec] *) 
 val lift : int -> 'a t -> 'a t
 
-val map : ('a -> 'b) -> 'a t -> 'b t
-
-(* [(smartmap f t) == t] if [(f a) ==a ] for all nodes *)
-val smartmap : ('a -> 'a) -> 'a t -> 'a t
-
+val is_node : 'a t -> bool
 (* Destructors (recursive calls are expanded) *)
-val dest_param : 'a t -> int
 val dest_node  : 'a t -> 'a * 'a t array
+(* dest_param is not needed for closed trees (i.e. with no free variable) *)
+val dest_param : 'a t -> int * int
 
 (* Tells if a tree has an infinite branch *)
 val is_infinite : 'a t -> bool
 
+(* [compare_rtree f t1 t2] compares t1 t2 (top-down).
+   f is called on each node: if the result is negative then the
+   traversal ends on false, it is is positive then deeper nodes are
+   not examined, and the traversal continues on respective siblings,
+   and if it is 0, then the traversal continues on sons, pairwise.
+   In this latter case, if the nodes do not have the same number of
+   sons, then the traversal ends on false.
+   In case of loop, the traversal is successful and it resumes on
+   siblings.
+ *)
+val compare_rtree : ('a t -> 'b t -> int) -> 'a t -> 'b t -> bool
+
+val eq_rtree : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
+
+(* Iterators *)
+
+val map : ('a -> 'b) -> 'a t -> 'b t
+(* [(smartmap f t) == t] if [(f a) ==a ] for all nodes *)
+val smartmap : ('a -> 'a) -> 'a t -> 'a t
+val fold : (bool -> 'a t -> ('a t -> 'b) -> 'b) -> 'a t -> 'b
+val fold2 :
+  (bool -> 'a t -> 'b -> ('a t -> 'b -> 'c) -> 'c) -> 'a t -> 'b -> 'c
+
 (* A rather simple minded pretty-printer *)
 val pp_tree : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds
diff --git a/lib/system.ml b/lib/system.ml
index c92e87f1..aa71ddfa 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: system.ml 9397 2006-11-21 21:50:54Z herbelin $ *)
+(* $Id: system.ml 10437 2008-01-11 14:50:44Z bertot $ *)
 
 open Pp
 open Util
@@ -98,15 +98,31 @@ let all_subdirs ~unix_path:root =
   List.rev !l
 
 let where_in_path path filename =
-  let rec search = function
+  let rec search acc = function
     | lpe :: rem ->
 	let f = Filename.concat lpe filename in
-	if Sys.file_exists f then (lpe,f) else search rem
-    | [] ->
-	raise Not_found
+	  if Sys.file_exists f 
+	  then (search ((lpe,f)::acc) rem) 
+	  else search acc rem
+    | [] -> acc in
+  let rec check_and_warn cont acc l = 
+    match l with
+      | [] -> if cont then assert false else raise Not_found
+      | [ (lpe, f) ] -> 
+	  if cont then begin
+	      warning (acc ^ (string_of_physical_path lpe) ^ " ]");
+	      warning ("Loading " ^ f)
+	    end;
+	  (lpe, f)
+      | (lpe, f) :: l' -> 
+	  if cont then
+	    check_and_warn true (acc ^ (string_of_physical_path lpe) ^ "; ") l'
+	  else
+	    check_and_warn true 
+	      (filename ^ " has been found in [ " ^ (string_of_physical_path lpe) ^ "; ") l' 
   in
-  search path
-
+    check_and_warn false "" (search [] path)
+  
 let find_file_in_path paths filename =
   if not (Filename.is_implicit filename) then
     let root = Filename.dirname filename in
@@ -199,7 +215,7 @@ let connect writefun readfun com =
   let pid = 
     let ch_to' = Unix.descr_of_in_channel ch_to_in in
     let ch_from' = Unix.descr_of_out_channel ch_from_out in
-    try Unix.create_process com [||] ch_to' ch_from' Unix.stdout
+    try Unix.create_process com [|com|] ch_to' ch_from' Unix.stdout
     with Unix.Unix_error (err,_,_) ->
       close_in ch_to_in; close_in ch_from_in; close_out ch_from_out;
       unlink tmp_from; unlink tmp_to;
diff --git a/lib/system.mli b/lib/system.mli
index a58308a8..6d535464 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 9397 2006-11-21 21:50:54Z herbelin $ i*)
+(*i $Id: system.mli 9398 2006-11-21 21:51:18Z 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
diff --git a/lib/util.ml b/lib/util.ml
index 16d73430..9fa92f94 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id: util.ml 10185 2007-10-06 18:05:13Z herbelin $ *)
+(* $Id: util.ml 11083 2008-06-09 22:08:14Z herbelin $ *)
 
 open Pp
 
@@ -26,19 +26,27 @@ type loc = Compat.loc
 let dummy_loc = Compat.dummy_loc
 let unloc = Compat.unloc
 let make_loc = Compat.make_loc
+let join_loc = Compat.join_loc
 
 (* raising located exceptions *)
 type 'a located = loc * 'a
 let anomaly_loc (loc,s,strm) = Stdpp.raise_with_loc loc (Anomaly (s,strm))
 let user_err_loc (loc,s,strm) = Stdpp.raise_with_loc loc (UserError (s,strm))
 let invalid_arg_loc (loc,s) = Stdpp.raise_with_loc loc (Invalid_argument s)
-let join_loc = Compat.join_loc
+
+let located_fold_left f x (_,a) = f x a 
+let located_iter2 f (_,a) (_,b) = f a b
 
 (* Like Exc_located, but specifies the outermost file read, the filename
    associated to the location of the error, and the error itself. *)
 
 exception Error_in_file of string * (bool * string * loc) * exn
 
+(* Mapping under pairs *)
+
+let on_fst f (a,b) = (f a,b)
+let on_snd f (a,b) = (a,f b)
+
 (* Projections from triplets *)
 
 let pi1 (a,_,_) = a
@@ -47,15 +55,8 @@ let pi3 (_,_,a) = a
 
 (* Characters *)
 
-let is_letter c =
-  (c >= 'a' && c <= 'z') or
-  (c >= 'A' && c <= 'Z') or
-  (c >= '\248' && c <= '\255') or
-  (c >= '\192' && c <= '\214') or
-  (c >= '\216' && c <= '\246')
-
+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 = '_'
 
@@ -99,6 +100,10 @@ let string_string_contains ~where ~what =
 
 let plural n s = if n>1 then s^"s" else s
 
+let ordinal n =
+  let s = match n mod 10 with 1 -> "st" | 2 -> "nd" | 3 -> "rd" | _ -> "th" in
+  string_of_int n ^ s
+
 (* string parsing *)
 
 let parse_loadpath s =
@@ -119,9 +124,329 @@ module Stringset = Set.Make(struct type t = string let compare = compare end)
 
 module Stringmap = Map.Make(struct type t = string let compare = compare end)
 
-(* Lists *)
+type utf8_status = UnicodeLetter | UnicodeIdentPart | UnicodeSymbol
+
+exception UnsupportedUtf8
+
+let classify_unicode unicode =
+    match unicode land 0x1F000 with
+    | 0x0 ->
+    begin match unicode with
+    (* utf-8 Basic Latin underscore *)
+    | x when x = 0x005F -> UnicodeLetter
+    (* utf-8 Basic Latin letters *)
+    | x when 0x0041 <= x & x <= 0x005A -> UnicodeLetter
+    | x when 0x0061 <= x & x <= 0x007A -> UnicodeLetter
+    (* utf-8 Basic Latin digits and quote *)
+    | x when 0x0030 <= x & x <= 0x0039 or x = 0x0027 -> UnicodeIdentPart
+    (* utf-8 Basic Latin symbols *)
+    | x when x <= 0x007F -> UnicodeSymbol
+    (* utf-8 Latin-1 non breaking space U00A0 *)
+    | 0x00A0 -> UnicodeLetter
+    (* utf-8 Latin-1 symbols U00A1-00BF *)
+    | x when 0x00A0 <= x & x <= 0x00BF -> UnicodeSymbol
+    (* utf-8 Latin-1 letters U00C0-00D6 *)
+    | x when 0x00C0 <= x & x <= 0x00D6 -> UnicodeLetter
+    (* utf-8 Latin-1 symbol U00D7 *)
+    | 0x00D7 -> UnicodeSymbol
+    (* utf-8 Latin-1 letters U00D8-00F6 *)
+    | x when 0x00D8 <= x & x <= 0x00F6 -> UnicodeLetter
+    (* utf-8 Latin-1 symbol U00F7 *)
+    | 0x00F7 -> UnicodeSymbol
+    (* utf-8 Latin-1 letters U00F8-00FF *)
+    | x when 0x00F8 <= x & x <= 0x00FF -> UnicodeLetter
+    (* utf-8 Latin Extended A U0100-017F and Latin Extended B U0180-U0241 *)
+    | x when 0x0100 <= x & x <= 0x0241 -> UnicodeLetter
+    (* utf-8 Phonetic letters U0250-02AF *)
+    | x when 0x0250 <= x & x <= 0x02AF -> UnicodeLetter
+    (* utf-8 what do to with diacritics U0300-U036F ? *)
+    (* utf-8 Greek letters U0380-03FF *)
+    | x when 0x0380 <= x & x <= 0x03FF -> UnicodeLetter
+    (* utf-8 Cyrillic letters U0400-0481 *)
+    | x when 0x0400 <= x & x <= 0x0481 -> UnicodeLetter
+    (* utf-8 Cyrillic symbol U0482 *)
+    | 0x0482 -> UnicodeSymbol
+    (* utf-8 what do to with diacritics U0483-U0489 \ U0487 ? *)
+    (* utf-8 Cyrillic letters U048A-U4F9 (Warning: 04CF) *)
+    | x when 0x048A <= x & x <= 0x04F9 -> UnicodeLetter
+    (* utf-8 Cyrillic supplement letters U0500-U050F *)
+    | x when 0x0500 <= x & x <= 0x050F -> UnicodeLetter
+    (* utf-8 Hebrew letters U05D0-05EA *)
+    | x when 0x05D0 <= x & x <= 0x05EA -> UnicodeLetter
+    (* utf-8 Arabic letters U0621-064A *)
+    | x when 0x0621 <= x & x <= 0x064A -> UnicodeLetter
+    (* utf-8 Arabic supplement letters U0750-076D *)
+    | x when 0x0750 <= x & x <= 0x076D -> UnicodeLetter
+    | _ -> raise UnsupportedUtf8
+    end
+    | 0x1000 ->
+    begin match unicode with
+    (* utf-8 Georgian U10A0-10FF (has holes) *)
+    | x when 0x10A0 <= x & x <= 0x10FF -> UnicodeLetter
+    (* utf-8 Hangul Jamo U1100-11FF (has holes) *)
+    | x when 0x1100 <= x & x <= 0x11FF -> UnicodeLetter
+    (* utf-8 Latin additional letters U1E00-1E9B and U1EA0-1EF9 *)
+    | x when 0x1E00 <= x & x <= 0x1E9B -> UnicodeLetter
+    | x when 0x1EA0 <= x & x <= 0x1EF9 -> UnicodeLetter
+    | _ -> raise UnsupportedUtf8
+    end
+    | 0x2000 ->
+    begin match unicode with
+    (* utf-8 general punctuation U2080-2089 *)
+    (* Hyphens *)
+    | x when 0x2010 <= x & x <= 0x2011 -> UnicodeLetter 
+    (* Dashes and other symbols *)
+    | x when 0x2012 <= x & x <= 0x2027 -> UnicodeSymbol
+    (* Per mille and per ten thousand signs *)
+    | x when 0x2030 <= x & x <= 0x2031 -> UnicodeSymbol
+    (* Prime letters *)
+    | x when 0x2032 <= x & x <= 0x2034 or x = 0x2057 -> UnicodeIdentPart
+    (* Miscellaneous punctuation *)
+    | x when 0x2039 <= x & x <= 0x2056 -> UnicodeSymbol
+    | x when 0x2058 <= x & x <= 0x205E -> UnicodeSymbol
+    (* Invisible mathematical operators *)
+    | x when 0x2061 <= x & x <= 0x2063 -> UnicodeSymbol
+    (* utf-8 superscript U2070-207C *) 
+    | x when 0x2070 <= x & x <= 0x207C -> UnicodeSymbol
+    (* utf-8 subscript U2080-2089 *) 
+    | x when 0x2080 <= x & x <= 0x2089 -> UnicodeIdentPart
+    (* utf-8 letter-like U2100-214F *)
+    | x when 0x2100 <= x & x <= 0x214F -> UnicodeLetter
+    (* utf-8 number-forms U2153-2183 *)
+    | x when 0x2153 <= x & x <= 0x2183 -> UnicodeSymbol
+    (* utf-8 arrows A U2190-21FF *)
+    (* utf-8 mathematical operators U2200-22FF *)
+    (* utf-8 miscellaneous technical U2300-23FF *)
+    | x when 0x2190 <= x & x <= 0x23FF -> UnicodeSymbol
+    (* utf-8 box drawing U2500-257F has ceiling, etc. *)
+    (* utf-8 block elements U2580-259F *)
+    (* utf-8 geom. shapes U25A0-25FF (has triangles, losange, etc) *)
+    (* utf-8 miscellaneous symbols U2600-26FF *)
+    | x when 0x2500 <= x & x <= 0x26FF -> UnicodeSymbol
+    (* utf-8 arrows B U2900-297F *)
+    | x when 0x2900 <= x & x <= 0x297F -> UnicodeSymbol
+    (* utf-8 mathematical operators U2A00-2AFF *)
+    | x when 0x2A00 <= x & x <= 0x2AFF -> UnicodeSymbol
+    (* utf-8 bold symbols U2768-U2775 *)
+    | x when 0x2768 <= x & x <= 0x2775 -> UnicodeSymbol
+    (* utf-8 arrows and brackets U27E0-U27FF *)
+    | x when 0x27E0 <= x & x <= 0x27FF -> UnicodeSymbol
+    (* utf-8 brackets, braces and parentheses *)
+    | x when 0x2980 <= x & x <= 0x299F -> UnicodeSymbol
+    (* utf-8 miscellaneous including double-plus U29F0-U29FF *)
+    | x when 0x29F0 <= x & x <= 0x29FF -> UnicodeSymbol
+    | _ -> raise UnsupportedUtf8
+    end
+    | _ ->
+    begin match unicode with
+    (* utf-8 Hiragana U3040-309F and Katakana U30A0-30FF *)
+    | x when 0x3040 <= x & x <= 0x30FF -> UnicodeLetter
+    (* utf-8 Unified CJK Ideographs U4E00-9FA5 *)
+    | x when 0x4E00 <= x & x <= 0x9FA5 -> UnicodeLetter
+    (* utf-8 Hangul syllables UAC00-D7AF *)
+    | x when 0xAC00 <= x & x <= 0xD7AF -> UnicodeLetter
+    (* utf-8 Gothic U10330-1034A *)
+    | x when 0x10330 <= x & x <= 0x1034A -> UnicodeLetter
+    (* utf-8 Math Alphanumeric Symbols U1D400-1D7FF (letters) (has holes) *)
+    | x when 0x1D400 <= x & x <= 0x1D7CB -> UnicodeLetter
+    (* utf-8 Math Alphanumeric Symbols U1D400-1D7FF (digits) *)
+    | x when 0x1D7CE <= x & x <= 0x1D7FF -> UnicodeIdentPart
+    | _ -> raise UnsupportedUtf8
+    end
 
-let list_add_set x l = if List.mem x l then l else x::l
+exception End_of_input
+
+let utf8_of_unicode n =
+  if n < 128 then 
+    String.make 1 (Char.chr n)
+  else if n < 2048 then
+    let s = String.make 2 (Char.chr (128 + n mod 64)) in
+    begin
+      s.[0] <- Char.chr (192 + n / 64);
+      s
+    end
+  else if n < 65536 then
+    let s = String.make 3 (Char.chr (128 + n mod 64)) in
+    begin 
+      s.[1] <- Char.chr (128 + (n / 64) mod 64);
+      s.[0] <- Char.chr (224 + n / 4096); 
+      s
+    end
+  else
+    let s = String.make 4 (Char.chr (128 + n mod 64)) in
+    begin 
+      s.[2] <- Char.chr (128 + (n / 64) mod 64);
+      s.[1] <- Char.chr (128 + (n / 4096) mod 64);
+      s.[0] <- Char.chr (240 + n / 262144);
+      s 
+    end
+
+let next_utf8 s i =
+  let err () = invalid_arg "utf8" in
+  let l = String.length s - i in
+  if l = 0 then raise End_of_input
+  else let a = Char.code s.[i] in if a <= 0x7F then
+    1, a
+  else if a land 0x40 = 0 or l = 1 then err ()
+  else let b = Char.code s.[i+1] in if b land 0xC0 <> 0x80 then err ()
+  else if a land 0x20 = 0 then
+    2, (a land 0x1F) lsl 6 + (b land 0x3F)
+  else if l = 2 then err ()
+  else let c = Char.code s.[i+2] in if c land 0xC0 <> 0x80 then err ()
+  else if a land 0x10 = 0 then
+    3, (a land 0x0F) lsl 12 + (b land 0x3F) lsl 6 + (c land 0x3F)
+  else if l = 3 then err ()
+  else let d = Char.code s.[i+3] in if d land 0xC0 <> 0x80 then err ()
+  else if a land 0x08 = 0 then
+    4, (a land 0x07) lsl 18 + (b land 0x3F) lsl 12 +
+       (c land 0x3F) lsl 6 + (d land 0x3F)
+  else err ()
+
+(* Check the well-formedness of an identifier *)
+
+let check_ident 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")
+  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")
+
+let lowercase_unicode s unicode =
+    match unicode land 0x1F000 with
+    | 0x0 ->
+    begin match unicode with
+    (* utf-8 Basic Latin underscore *)
+    | x when x = 0x005F -> x
+    (* utf-8 Basic Latin letters *)
+    | x when 0x0041 <= x & x <= 0x005A -> x + 32
+    | x when 0x0061 <= x & x <= 0x007A -> x
+    (* utf-8 Latin-1 non breaking space U00A0 *)
+    | 0x00A0 as x -> x
+    (* utf-8 Latin-1 letters U00C0-00D6 *)
+    | x when 0x00C0 <= x & x <= 0x00D6 -> x + 32
+    (* utf-8 Latin-1 letters U00D8-00F6 *)
+    | x when 0x00D8 <= x & x <= 0x00DE -> x + 32
+    | x when 0x00E0 <= x & x <= 0x00F6 -> x
+    (* utf-8 Latin-1 letters U00F8-00FF *)
+    | x when 0x00F8 <= x & x <= 0x00FF -> x
+    (* utf-8 Latin Extended A U0100-017F and Latin Extended B U0180-U0241 *)
+    | x when 0x0100 <= x & x <= 0x017F ->
+	if x mod 2 = 1 then x else x + 1
+    | x when 0x0180 <= x & x <= 0x0241 ->
+	warning ("Unable to decide which lowercase letter to map to "^s); x
+    (* utf-8 Phonetic letters U0250-02AF *)
+    | x when 0x0250 <= x & x <= 0x02AF -> x
+    (* utf-8 what do to with diacritics U0300-U036F ? *)
+    (* utf-8 Greek letters U0380-03FF *)
+    | x when 0x0380 <= x & x <= 0x0385 -> x
+    | 0x0386 -> 0x03AC
+    | x when 0x0388 <= x & x <= 0x038A -> x + 37
+    | 0x038C -> 0x03CC
+    | x when 0x038E <= x & x <= 0x038F -> x + 63
+    | x when 0x0390 <= x & x <= 0x03AB & x <> 0x03A2 -> x + 32
+    (* utf-8 Greek lowercase letters U03B0-03CE *)	
+    | x when 0x03AC <= x & x <= 0x03CE -> x
+    | x when 0x03CF <= x & x <= 0x03FF ->
+	warning ("Unable to decide which lowercase letter to map to "^s); x
+    (* utf-8 Cyrillic letters U0400-0481 *)
+    | x when 0x0400 <= x & x <= 0x040F -> x + 80
+    | x when 0x0410 <= x & x <= 0x042F -> x + 32
+    | x when 0x0430 <= x & x <= 0x045F -> x 
+    | x when 0x0460 <= x & x <= 0x0481 ->
+	if x mod 2 = 1 then x else x + 1
+    (* utf-8 Cyrillic letters U048A-U4F9 (Warning: 04CF) *)
+    | x when 0x048A <= x & x <= 0x04F9 & x <> 0x04CF -> 
+	if x mod 2 = 1 then x else x + 1
+    (* utf-8 Cyrillic supplement letters U0500-U050F *)
+    | x when 0x0500 <= x & x <= 0x050F ->
+	if x mod 2 = 1 then x else x + 1
+    (* utf-8 Hebrew letters U05D0-05EA *)
+    | x when 0x05D0 <= x & x <= 0x05EA -> x
+    (* utf-8 Arabic letters U0621-064A *)
+    | x when 0x0621 <= x & x <= 0x064A -> x
+    (* utf-8 Arabic supplement letters U0750-076D *)
+    | x when 0x0750 <= x & x <= 0x076D -> x
+    | _ -> raise UnsupportedUtf8
+    end
+    | 0x1000 ->
+    begin match unicode with
+    (* utf-8 Georgian U10A0-10FF (has holes) *)
+    | x when 0x10A0 <= x & x <= 0x10FF -> x
+    (* utf-8 Hangul Jamo U1100-11FF (has holes) *)
+    | x when 0x1100 <= x & x <= 0x11FF -> x
+    (* utf-8 Latin additional letters U1E00-1E9B and U1EA0-1EF9 *)
+    | x when 0x1E00 <= x & x <= 0x1E95 ->
+	if x mod 2 = 1 then x else x + 1
+    | x when 0x1E96 <= x & x <= 0x1E9B -> x
+    | x when 0x1EA0 <= x & x <= 0x1EF9 ->
+	if x mod 2 = 1 then x else x + 1
+    | _ -> raise UnsupportedUtf8
+    end
+    | 0x2000 ->
+    begin match unicode with
+    (* utf-8 general punctuation U2080-2089 *)
+    (* Hyphens *)
+    | x when 0x2010 <= x & x <= 0x2011 -> x
+    (* utf-8 letter-like U2100-214F *)
+    | 0x2102 (* double-struck C *) -> Char.code 'x'
+    | 0x2115 (* double-struck N *) -> Char.code 'n'
+    | 0x2119 (* double-struck P *) -> Char.code 'x'
+    | 0x211A (* double-struck Q *) -> Char.code 'x'
+    | 0x211D (* double-struck R *) -> Char.code 'r'
+    | 0x2124 (* double-struck Z *) -> Char.code 'x'
+    | x when 0x2100 <= x & x <= 0x214F ->
+	warning ("Unable to decide which lowercase letter to map to "^s); x
+    | _ -> raise UnsupportedUtf8
+    end
+    | _ ->
+    begin match unicode with
+    (* utf-8 Hiragana U3040-309F and Katakana U30A0-30FF *)
+    | x when 0x3040 <= x & x <= 0x30FF -> x
+    (* utf-8 Unified CJK Ideographs U4E00-9FA5 *)
+    | x when 0x4E00 <= x & x <= 0x9FA5 -> x
+    (* utf-8 Hangul syllables UAC00-D7AF *)
+    | x when 0xAC00 <= x & x <= 0xD7AF -> x
+    (* utf-8 Gothic U10330-1034A *)
+    | x when 0x10330 <= x & x <= 0x1034A -> x
+    (* utf-8 Math Alphanumeric Symbols U1D400-1D7FF (letters) (has holes) *)
+    | x when 0x1D6A8 <= x & x <= 0x1D7C9 ->
+        let a = (x - 0x1D6A8) mod 58 in
+        if a <= 16 or (18 <= a & a <= 24)
+        then x + 26 (* all but nabla and theta symbol *)
+        else x
+    | x when 0x1D538 <= x & x <= 0x1D56B ->
+        (* Use ordinary lowercase in both small and capital double-struck *)
+        (x - 0x1D538) mod 26 + Char.code 'a'
+    | x when 0x1D468 <= x & x <= 0x1D6A3 -> (* General case *)
+        if (x - 0x1D400 / 26) mod 2 = 0 then x + 26 else x
+    | x when 0x1D400 <= x & x <= 0x1D7CB -> (* fallback *)
+        x
+    (* utf-8 Math Alphanumeric Symbols U1D400-1D7FF (digits) *)
+    | x when 0x1D7CE <= x & x <= 0x1D7FF -> x
+    | _ -> raise UnsupportedUtf8
+    end
+
+let lowercase_first_char_utf8 s =
+  assert (s <> "");
+  let j, n = next_utf8 s 0 in
+  utf8_of_unicode (lowercase_unicode (String.sub s 0 j) n)
+
+(* Lists *)
 
 let list_intersect l1 l2 = 
   List.filter (fun x -> List.mem x l2) l1
@@ -160,6 +485,11 @@ let list_tabulate f len =
   in 
   tabrec 0
 
+let rec list_make n v =
+  if n = 0 then []
+  else if n < 0 then invalid_arg "list_make"
+  else v::list_make (n-1) v
+
 let list_assign l n e = 
   let rec assrec stk = function
     | ((h::t), 0) -> List.rev_append stk (e::t)
@@ -205,6 +535,14 @@ let list_map3 f l1 l2 l3 =
   in 
   map (l1,l2,l3)
 
+let list_map4 f l1 l2 l3 l4 =
+  let rec map = function
+    | ([], [], [], []) -> []
+    | ((h1::t1), (h2::t2), (h3::t3), (h4::t4)) -> let v = f h1 h2 h3 h4 in v::map (t1,t2,t3,t4)
+    | (_, _, _, _) -> invalid_arg "map4"
+  in 
+  map (l1,l2,l3,l4)
+
 let list_index x = 
   let rec index_x n = function
     | y::l -> if x = y then n else index_x (succ n) l
@@ -212,6 +550,8 @@ let list_index x =
   in 
   index_x 1
 
+let list_index0 x l = list_index x l - 1 
+
 let list_unique_index x = 
   let rec index_x n = function
     | y::l -> 
@@ -222,6 +562,13 @@ let list_unique_index x =
     | [] -> raise Not_found 
   in index_x 1
 
+let list_fold_right_i f i l =
+  let rec it_list_f i l a = match l with
+    | [] -> a
+    | b::l -> f (i-1) b (it_list_f (i-1) l a)
+  in 
+  it_list_f (List.length l + i) l
+
 let list_fold_left_i f = 
   let rec it_list_f i a = function
     | [] -> a 
@@ -247,6 +594,14 @@ let rec list_fold_right_and_left f l hd =
     | a::l -> let hd = aux (a::tl) l in f hd a tl
    in aux [] l
 
+let list_iter3 f l1 l2 l3 =
+  let rec iter = function
+    | ([], [], []) -> ()
+    | ((h1::t1), (h2::t2), (h3::t3)) -> f h1 h2 h3; iter (t1,t2,t3)
+    | (_, _, _) -> invalid_arg "map3"
+  in 
+  iter (l1,l2,l3)
+
 let list_iter_i f l = list_fold_left_i (fun i _ x -> f i x) 0 () l
 
 let list_for_all_i p = 
@@ -265,6 +620,8 @@ let rec list_remove_first a = function
   | b::l -> b::list_remove_first a l
   | [] -> raise Not_found
 
+let list_add_set x l = if List.mem x l then l else x::l
+
 let list_eq_set l1 l2 =
   let rec aux l1 = function
   | [] -> l1 = []
@@ -300,14 +657,46 @@ let list_try_find f =
   try_find_f
 
 let list_uniquize l =
+  let visited = Hashtbl.create 23 in
   let rec aux acc = function
-  | [] -> List.rev acc
-  | h::t -> if List.mem h acc then aux acc t else aux (h::acc) t
+    | h::t -> if Hashtbl.mem visited h then aux acc t else
+	  begin
+	    Hashtbl.add visited h h;
+	    aux (h::acc) t
+	  end
+    | [] -> List.rev acc
   in aux [] l
 
-let rec list_distinct = function
-  | h::t -> (not (List.mem h t)) && list_distinct t
-  | _ -> true
+let rec list_distinct l = 
+  let visited = Hashtbl.create 23 in
+  let rec loop = function
+    | h::t ->
+	if Hashtbl.mem visited h then false
+	else 
+	  begin
+	    Hashtbl.add visited h h;
+	    loop t
+	  end
+    | [] -> true
+  in loop l
+
+let rec list_merge_uniq cmp l1 l2 =
+  match l1, l2 with
+  | [], l2 -> l2
+  | l1, [] -> l1
+  | h1 :: t1, h2 :: t2 ->
+      let c = cmp h1 h2 in 
+      if c = 0 
+      then h1 :: list_merge_uniq cmp t1 t2
+      else if c <= 0 
+      then h1 :: list_merge_uniq cmp t1 l2
+      else h2 :: list_merge_uniq cmp l1 t2
+
+let rec list_duplicates = function
+  | [] -> []
+  | x::l ->
+      let l' = list_duplicates l in
+      if List.mem x l then list_add_set x l' else l'
 
 let rec list_filter2 f = function
   | [], [] as p -> p
@@ -316,6 +705,12 @@ let rec list_filter2 f = function
       if f d l then d::dp', l::lp' else p
   | _ -> invalid_arg "list_filter2"
 
+let rec list_map_filter f = function
+  | [] -> []
+  | x::l ->
+      let l' = list_map_filter f l in
+      match f x with None -> l' | Some y -> y::l'
+
 let list_subset l1 l2 =
   let t2 = Hashtbl.create 151 in
   List.iter (fun x -> Hashtbl.add t2 x ()) l2;
@@ -338,6 +733,14 @@ let rec list_split3 = function
   | (x,y,z)::l ->
       let (rx, ry, rz) = list_split3 l in (x::rx, y::ry, z::rz)
 
+let rec list_insert_in_class f a = function
+  | [] -> [[a]]
+  | (b::_ as l)::classes when f a b -> (a::l)::classes
+  | l::classes -> l :: list_insert_in_class f a classes
+
+let list_partition_by f l =
+  List.fold_right (list_insert_in_class f) l []
+
 let list_firstn n l =
   let rec aux acc = function
     | (0, l) -> List.rev acc
@@ -363,6 +766,9 @@ let rec list_skipn n l = match n,l with
   | _, [] -> failwith "list_fromn"
   | n, _::l -> list_skipn (pred n) l
 
+let rec list_addn n x l = 
+  if n = 0 then l else x :: (list_addn (pred n) x l)
+
 let list_prefix_of prefl l = 
   let rec prefrec = function
     | (h1::t1, h2::t2) -> h1 = h2 && prefrec (t1,t2)
@@ -384,6 +790,7 @@ let list_drop_prefix p l =
       | None -> l
 
 let list_map_append f l = List.flatten (List.map f l)
+let list_join_map = list_map_append   (* Alias *)
 
 let list_map_append2 f l1 l2 = List.flatten (List.map2 f l1 l2)
 
@@ -394,8 +801,6 @@ let list_share_tails l1 l2 =
   in 
   shr_rev [] (List.rev l1, List.rev l2)
 
-let list_join_map f l = List.flatten (List.map f l)
-
 let rec list_fold_map f e = function
   |  []  -> (e,[])
   |  h::t ->
@@ -419,6 +824,35 @@ let list_fold_map' f l e =
 
 let list_map_assoc f = List.map (fun (x,a) -> (x,f a))
 
+(* Specification:
+   - =p= is set equality (double inclusion)
+   - f such that \forall l acc, (f l acc) =p= append (f l []) acc
+   - let g = fun x -> f x [] in
+   - union_map f l acc =p= append (flatten (map g l)) acc
+ *)
+let list_union_map f l acc =
+  List.fold_left
+    (fun x y -> f y x)
+    acc
+    l
+
+(* A generic cartesian product: for any operator (**), 
+   [list_cartesian (**) [x1;x2] [y1;y2] = [x1**y1; x1**y2; x2**y1; x2**y1]], 
+   and so on if there are more elements in the lists. *)
+
+let rec list_cartesian op l1 l2 = 
+  list_map_append (fun x -> List.map (op x) l2) l1
+
+(* [list_cartesians] is an n-ary cartesian product: it iterates 
+   [list_cartesian] over a list of lists.  *)
+
+let list_cartesians op init ll = 
+  List.fold_right (list_cartesian op) ll [init]
+
+(* list_combinations [[a;b];[c;d]] gives [[a;c];[a;d];[b;c];[b;d]] *)
+
+let list_combinations l = list_cartesians (fun x l -> x::l) [] l
+
 (* Arrays *)
 
 let array_exists f v = 
@@ -645,6 +1079,11 @@ let array_map_left_pair f a g b =
     r, s
   end
 
+let array_iter2 f v1 v2 =
+  let n = Array.length v1 in
+  if Array.length v2 <> n then invalid_arg "array_iter2"
+  else for i = 0 to n - 1 do f v1.(i) v2.(i) done
+
 let pure_functional = false
 
 let array_fold_map' f v e =
@@ -659,6 +1098,11 @@ else
   let v' = Array.map (fun x -> let (y,e) = f x !e' in e' := e; y) v in
   (v',!e')
 
+let array_fold_map f e v =
+  let e' = ref e in
+  let v' = Array.map (fun x -> let (e,y) = f !e' x in e' := e; y) v in
+  (!e',v')
+
 let array_fold_map2' f v1 v2 e =
   let e' = ref e in
   let v' = 
@@ -677,6 +1121,12 @@ let array_distinct v =
   with Exit ->
     false
 
+let array_union_map f a acc =
+  Array.fold_left
+    (fun x y -> f y x)
+    acc
+    a
+
 (* Matrices *)
 
 let matrix_transpose mat =
@@ -723,44 +1173,6 @@ let interval n m =
   in 
   interval_n ([],m)
 
-let in_some x = Some x
-
-let out_some = function
-  | Some x -> x
-  | None -> failwith "out_some"
-
-let option_map f = function
-  | None -> None
-  | Some x -> Some (f x)
-
-let option_cons a l = match a with
-  | Some x -> x::l
-  | None -> l
-
-let option_fold_left2 f e a b = match (a,b) with
-  | Some x, Some y -> f e x y
-  | _ -> e
-
-let option_fold_left f e a = match a with
-  | Some x -> f e x
-  | _ -> e
-
-let option_fold_right f a e = match a with
-  | Some x -> f x e
-  | _ -> e
-
-let option_compare f a b = match (a,b) with
-  | None, None -> true
-  | Some a', Some b' -> f a' b'
-  | _ -> failwith "option_compare"
-
-let option_iter f = function
-  | None -> ()
-  | Some x -> f x
-
-let option_smartmap f a = match a with
-  | None -> a
-  | Some x -> let x' = f x in if x'==x then a else Some x'
 
 let map_succeed f = 
   let rec map_f = function 
@@ -780,15 +1192,21 @@ let pr_semicolon () = str ";" ++ spc ()
 let pr_bar () = str "|" ++ spc ()
 let pr_arg pr x = spc () ++ pr x
 let pr_opt pr = function None -> mt () | Some x -> pr_arg pr x
+let pr_opt_no_spc pr = function None -> mt () | Some x -> pr x
 
-let pr_ord n =
-  let suff = match n mod 10 with 1 -> "st" | 2 -> "nd" | _ -> "th" in
-  int n ++ str suff
+let nth n = str (ordinal n)
 
 let rec prlist elem l = match l with 
   | []   -> mt ()
   | 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. *)
+
+let rec prlist_strict elem l = match l with 
+  | []   -> mt ()
+  | h::t -> (elem h)++(prlist_strict elem t)
+
 let rec prlist_with_sep sep elem l = match l with
   | []   -> mt ()
   | [h]  -> elem h
@@ -821,6 +1239,8 @@ let prvect_with_sep sep elem v =
   let n = Array.length v in
   if n = 0 then mt () else pr (n - 1)
 
+let prvect elem v = prvect_with_sep mt elem v
+
 let surround p = hov 1 (str"(" ++ p ++ str")")
 
 (*s Size of ocaml values. *)
diff --git a/lib/util.mli b/lib/util.mli
index cc44a677..7807bbbd 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 9766 2007-04-13 13:26:28Z herbelin $ i*)
+(*i $Id: util.mli 11083 2008-06-09 22:08:14Z herbelin $ i*)
 
 (*i*)
 open Pp
@@ -43,6 +43,8 @@ val anomaly_loc : loc * string * std_ppcmds -> 'a
 val user_err_loc : loc * string * std_ppcmds -> 'a
 val invalid_arg_loc : loc * string -> 'a
 val join_loc : loc -> loc -> loc
+val located_fold_left : ('a -> 'b -> 'a) -> 'a -> 'b located -> 'a
+val located_iter2 : ('a -> 'b -> unit) -> 'a located -> 'b located -> unit
 
 (* Like [Exc_located], but specifies the outermost file read, the
    input buffer associated to the location of the error (or the module name
@@ -50,6 +52,11 @@ val join_loc : loc -> loc -> loc
 
 exception Error_in_file of string * (bool * string * loc) * exn
 
+(* Mapping under pairs *)
+
+val on_fst : ('a -> 'b) -> 'a * 'c -> 'b * 'c
+val on_snd : ('a -> 'b) -> 'c * 'a -> 'c * 'b
+
 (*s Projections from triplets *)
 
 val pi1 : 'a * 'b * 'c -> 'a
@@ -69,12 +76,21 @@ val implode : string list -> 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 parse_loadpath : string -> string list
 
 module Stringset : Set.S with type elt = string
 module Stringmap : Map.S with type key = string
 
+type utf8_status = UnicodeLetter | UnicodeIdentPart | UnicodeSymbol
+
+exception UnsupportedUtf8
+
+val classify_unicode : int -> utf8_status
+val check_ident : string -> unit
+val lowercase_first_char_utf8 : string -> string
+
 (*s Lists. *)
 
 val list_add_set : 'a -> 'a list -> 'a list
@@ -87,10 +103,12 @@ val list_subtractq : 'a list -> 'a list -> 'a list
 val list_chop : int -> 'a list -> 'a list * 'a list
 (* [list_tabulate f n] builds [[f 0; ...; f (n-1)]] *)
 val list_tabulate : (int -> 'a) -> int -> 'a list
+val list_make : int -> 'a -> 'a list
 val list_assign : 'a list -> int -> 'a -> 'a list
 val list_distinct : 'a list -> bool
+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
 (* [list_smartmap f [a1...an] = List.map f [a1...an]] but if for all i
    [ f ai == ai], then [list_smartmap f l==l] *)
 val list_smartmap : ('a -> 'a) -> 'a list -> 'a list
@@ -100,10 +118,17 @@ val list_map2_i :
   (int -> 'a -> 'b -> 'c) -> int -> 'a list -> 'b list -> 'c list
 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
+(* [list_index] returns the 1st index of an element in a list (counting from 1) *)
 val list_index : 'a -> 'a list -> int
 (* [list_unique_index x l] returns [Not_found] if [x] doesn't occur exactly once *)
 val list_unique_index : 'a -> 'a list -> int 
+(* [list_index0] behaves as [list_index] except that it starts counting at 0 *)
+val list_index0 : 'a -> 'a list -> int
+val list_iter3 : ('a -> 'b -> 'c -> unit) -> 'a list -> 'b list -> 'c list -> unit
 val list_iter_i :  (int -> 'a -> unit) -> 'a list -> unit
+val list_fold_right_i :  (int -> 'a -> 'b -> 'b) -> int -> 'a list -> 'b -> 'b
 val list_fold_left_i :  (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a
 val list_fold_right_and_left :
     ('a -> 'b -> 'b list -> 'a) -> 'b list -> 'a -> 'a
@@ -116,26 +141,41 @@ val list_sep_last : 'a list -> 'a * 'a list
 val list_try_find_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b
 val list_try_find : ('a -> 'b) -> 'a list -> 'b
 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_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
 val list_last : 'a list -> 'a
 val list_lastn : int -> 'a list -> 'a list
 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
 (* [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
 (* raises [Invalid_argument] if the two lists don't have the same length *)
 val list_map_append2 : ('a -> 'b -> 'c list) -> 'a list -> 'b list -> 'c list
 val list_share_tails : 'a list -> 'a list -> 'a list * 'a list * 'a list
-val list_join_map : ('a -> 'b list) -> 'a list -> 'b list
 (* [list_fold_map f e_0 [l_1...l_n] = e_n,[k_1...k_n]]
    where [(e_i,k_i)=f e_{i-1} l_i] *)
 val list_fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list
 val list_fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a
 val list_map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list
+(* A generic cartesian product: for any operator (**), 
+   [list_cartesian (**) [x1;x2] [y1;y2] = [x1**y1; x1**y2; x2**y1; x2**y1]], 
+   and so on if there are more elements in the lists. *)
+val list_cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
+(* [list_cartesians] is an n-ary cartesian product: it iterates 
+   [list_cartesian] over a list of lists.  *)
+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
+
+val list_union_map : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
 
 (*s Arrays. *)
 
@@ -174,10 +214,13 @@ val array_map3 :
 val array_map_left : ('a -> 'b) -> 'a array -> 'b array
 val array_map_left_pair : ('a -> 'b) -> 'a array -> ('c -> 'd) -> 'c array ->
   'b array * 'd array
+val array_iter2 : ('a -> 'b -> unit) -> 'a array -> 'b array -> unit
 val array_fold_map' : ('a -> 'c -> 'b * 'c) -> 'a array -> 'c -> 'b array * 'c
+val array_fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b array -> 'a * 'c array
 val array_fold_map2' :
   ('a -> 'b -> 'c -> 'd * 'c) -> 'a array -> 'b array -> 'c -> 'd array * 'c
 val array_distinct : 'a array -> bool
+val array_union_map : ('a -> 'b -> 'b) -> 'a array -> 'b -> 'b
 
 (*s Matrices *)
 
@@ -205,17 +248,6 @@ val intmap_inv : 'a Intmap.t -> 'a -> int list
 
 val interval : int -> int -> int list
 
-val in_some : 'a -> 'a option
-val out_some : 'a option -> 'a
-val option_map : ('a -> 'b) -> 'a option -> 'b option
-val option_cons : 'a option -> 'a list -> 'a list
-val option_fold_right : ('a -> 'b -> 'b) -> 'a option -> 'b -> 'b
-val option_fold_left : ('a -> 'b -> 'a) -> 'a -> 'b option -> 'a
-val option_fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b option ->
-  'c option -> 'a
-val option_iter : ('a -> unit) -> 'a option -> unit
-val option_compare : ('a -> 'b -> bool) -> 'a option -> 'b option -> bool 
-val option_smartmap : ('a -> 'a) -> 'a option -> 'a option
 
 (* In [map_succeed f l] an element [a] is removed if [f a] raises *)
 (* [Failure _] otherwise behaves as [List.map f l] *)
@@ -231,14 +263,19 @@ val pr_str : string -> std_ppcmds
 val pr_coma : unit -> std_ppcmds
 val pr_semicolon : unit -> std_ppcmds
 val pr_bar : unit -> std_ppcmds
-val pr_ord : int -> std_ppcmds
 val pr_arg : ('a -> std_ppcmds) -> 'a -> std_ppcmds
 val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds
+val pr_opt_no_spc : ('a -> std_ppcmds) -> 'a option -> std_ppcmds
+val nth : int -> std_ppcmds
 
 val prlist : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
-val prvecti : (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds
+(* unlike all other functions below, [prlist] works lazily.
+   if a strict behavior is needed, use [prlist_strict] instead. *)
+val prlist_strict :  ('a -> std_ppcmds) -> 'a list -> std_ppcmds
 val prlist_with_sep :
    (unit -> std_ppcmds) -> ('b -> std_ppcmds) -> 'b list -> std_ppcmds
+val prvect : ('a -> std_ppcmds) -> 'a array -> std_ppcmds
+val prvecti : (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds
 val prvect_with_sep :
    (unit -> std_ppcmds) -> ('b -> std_ppcmds) -> 'b array -> std_ppcmds
 val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds