Initial revision

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2 85f007b7-540e-0410-9357-904b9bb8a0f7

8 files changed, 795 insertions, 0 deletions

diff --git a/lib/hashcons.ml b/lib/hashcons.ml
new file mode 100644
index 0000000000..301643dbae
--- /dev/null
+++ b/lib/hashcons.ml
@@ -0,0 +1,244 @@
+(****************************************************************************)
+(*                 The Calculus of Inductive Constructions                  *)
+(*                                                                          *)
+(*                                Projet Coq                                *)
+(*                                                                          *)
+(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
+(*              Rocquencourt         Orsay          Lyon                    *)
+(*                                                                          *)
+(*                                 Coq V6.3                                 *)
+(*                               July 1st 1999                              *)
+(*                                                                          *)
+(****************************************************************************)
+(*                               hashcons.ml                                *)
+(****************************************************************************)
+(* Hash consing of datastructures *)
+
+(*
+open Pp;;
+let acces = ref 0;;
+let comparaison = ref 0;;
+let succes = ref 0;;
+let accesstr = ref 0;;
+let comparaisonstr = ref 0;;
+let successtr = ref 0;;
+*)let stat() = ();;
+(*
+  mSGNL [< 'sTR"acces="; 'iNT !acces; 'sPC;
+           'sTR"comp="; 'iNT !comparaison; 'sPC;
+           'sTR"succes="; 'iNT !succes; 'sPC >];
+  comparaison:=0;
+  acces:=0;
+  succes:=0;
+  mSGNL [< 'sTR"String:"; 'sPC;
+           'sTR"acces="; 'iNT !accesstr; 'sPC;
+           'sTR"comp="; 'iNT !comparaisonstr; 'sPC;
+           'sTR"succes="; 'iNT !successtr; 'sPC >];
+  comparaisonstr:=0;
+  accesstr:=0;
+  successtr:=0
+;;
+*)
+
+
+(* The generic hash-consing functions (does not use Obj) *)
+
+(* [t] is the type of object to hash-cons
+ * [u] is the type of hash-cons functions for the sub-structures
+ *   of objects of type t (u usually has the form (t1->t1)*(t2->t2)*...).
+ * [hash_sub u x] is a function that hash-cons the sub-structures of x using
+ *   the hash-consing functions u provides.
+ * [equal] is a comparison function. It is allowed to use physical equality
+ *   on the sub-terms hash-consed by the hash_sub function.
+ * [hash] is the hash function given to the Hashtbl.Make function 
+ *
+ * Note that this module type coerces to the argument of Hashtbl.Make.
+ *)
+module type Comp =
+  sig
+    type t
+    type u
+    val hash_sub :  u -> t -> t
+    val equal : t -> t -> bool
+    val hash : t -> int
+  end
+
+(* The output is a function f such that
+ * [f ()] has the side-effect of creating (internally) a hash-table of the
+ *   hash-consed objects. The result is a function taking the sub-hashcons
+ *   functions and an object, and hashcons it. It does not really make sense
+ *   to call f() with different sub-hcons functions. That's why we use the
+ *   wrappers simple_hcons, recursive_hcons, ... The latter just take as
+ *   argument the sub-hcons functions (the tables are created at that moment),
+ *   and returns the hcons function for t.
+ *)
+module type S =
+  sig
+    type t
+    type u
+    val f : unit -> (u -> t -> t)
+  end
+
+
+module Make(X:Comp) =
+  struct
+    type t = X.t
+    type u = X.u
+
+    (* We create the type of hashtables for t, with our comparison fun.
+     * An invariant is that the table never contains two entries equals
+     * w.r.t (=), although the equality on keys is X.equal. This is
+     * granted since we hcons the subterms before looking up in the table.
+     *)
+    module Htbl = Hashtbl.Make(
+      struct type t=X.t
+             type u=X.u
+             let hash=X.hash
+             let equal x1 x2 = (*incr comparaison;*) X.equal x1 x2
+      end)
+
+    (* The table is created when () is applied.
+     * Hashconsing is then very simple:
+     *  1- hashcons the subterms using hash_sub and u
+     *  2- look up in the table, if we do not get a hit, we add it
+     *)
+    let f () =
+      let tab = Htbl.create 97 in
+        (fun u x ->
+           let y = X.hash_sub u x in
+            (* incr acces;*)
+             try let r = Htbl.find tab y in(* incr succes;*) r
+             with Not_found -> Htbl.add tab y y; y)
+  end;;
+
+(* A few usefull wrappers:
+ * takes as argument the function f above and build a function of type
+ * u -> t -> t that creates a fresh table each time it is applied to the
+ * sub-hcons functions. *)
+
+(* For non-recursive types it is quite easy. *)
+let simple_hcons h u = h () u;;
+
+(* For a recursive type T, we write the module of sig Comp with u equals
+ * to (T -> T) * u0
+ * The first component will be used to hash-cons the recursive subterms
+ * The second one to hashcons the other sub-structures.
+ * We just have to take the fixpoint of h
+ *)
+let recursive_hcons h u =
+  let hc = h () in
+  let rec hrec x = hc (hrec,u) x in
+    hrec
+;;
+
+(* If the structure may contain loops, use this one. *)
+let recursive_loop_hcons h u =
+  let hc = h () in
+  let rec hrec visited x =
+    if List.memq x visited then x
+    else hc (hrec (x::visited),u) x
+  in hrec []
+;;
+
+(* For 2 mutually recursive types *)
+let recursive2_hcons h1 h2 u1 u2 =
+  let hc1 = h1 () in
+  let hc2 = h2 () in
+  let rec hrec1 x = hc1 (hrec1,hrec2,u1) x
+  and hrec2 x = hc2 (hrec1,hrec2,u2) x
+  in (hrec1,hrec2)
+;;
+
+
+
+
+(* A set of global hashcons functions *)
+let hashcons_resets = ref [];;
+let init() = List.iter (fun f -> f()) !hashcons_resets;;
+
+(* [register_hcons h u] registers the hcons function h, result of the above
+ *   wrappers. It returns another hcons function that always uses the same
+ *   table, which can be reinitialized by init()
+ *)
+let register_hcons h u =
+  let hf = ref (h u) in
+  let reset() = hf := h u in
+    hashcons_resets := reset :: !hashcons_resets;
+    (fun x -> !hf x)
+;;
+
+
+
+(* Basic hashcons modules for string and obj. Integers do not need be
+   hashconsed.  *)
+
+(* string *)
+module Hstring = Make(
+  struct
+    type t = string
+    type u = unit
+    let hash_sub () s =(* incr accesstr;*) s
+    let equal s1 s2 =(* incr comparaisonstr;
+      if*) s1=s2(* then (incr successtr; true) else false*)
+    let hash = Hashtbl.hash
+  end);;
+
+(* Obj.t *)
+exception NotEq;;
+
+(* From CAMLLIB/caml/mlvalues.h *)
+let no_scan_tag = 251;;
+let tuple_p obj = Obj.is_block obj & (Obj.tag obj < no_scan_tag);;
+
+let comp_obj o1 o2 =
+  if tuple_p o1 & tuple_p o2 then
+    let n1 = Obj.size o1 and n2 = Obj.size o2 in
+      if n1=n2 then
+        try
+          for i = 0 to pred n1 do
+            if not (Obj.field o1 i == Obj.field o2 i) then raise NotEq
+          done; true
+        with NotEq -> false
+      else false
+  else o1=o2
+;;
+
+let hash_obj hrec o = 
+  begin
+    if tuple_p o then
+      let n = Obj.size o in
+        for i = 0 to pred n do
+          Obj.set_field o i (hrec (Obj.field o i))
+        done
+  end;
+  o
+;;
+
+module Hobj = Make(
+  struct
+    type t = Obj.t
+    type u = (Obj.t -> Obj.t) * unit
+    let hash_sub (hrec,_) = hash_obj hrec
+    let equal = comp_obj
+    let hash = Hashtbl.hash
+  end);;
+
+
+
+(* Hashconsing functions for string and obj. Always use the same
+ * global tables. The latter can be reinitialized with init()
+ *)
+(* string : string -> string *)
+(* obj : Obj.t -> Obj.t *)
+let string = register_hcons (simple_hcons Hstring.f) ();;
+let obj = register_hcons (recursive_hcons Hobj.f) ();;
+
+(* The unsafe polymorphic hashconsing function *)
+let magic_hash (c: 'a) =
+  init();
+  let r = obj (Obj.repr c) in
+    init();
+    (Obj.magic r : 'a)
+;;
+
+(* $Id$ *)
diff --git a/lib/hashcons.mli b/lib/hashcons.mli
new file mode 100644
index 0000000000..76a8fba4e8
--- /dev/null
+++ b/lib/hashcons.mli
@@ -0,0 +1,60 @@
+(****************************************************************************)
+(*                 The Calculus of Inductive Constructions                  *)
+(*                                                                          *)
+(*                                Projet Coq                                *)
+(*                                                                          *)
+(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
+(*              Rocquencourt         Orsay          Lyon                    *)
+(*                                                                          *)
+(*                                 Coq V6.3                                 *)
+(*                               July 1st 1999                              *)
+(*                                                                          *)
+(****************************************************************************)
+(*                               hashcons.mli                               *)
+(****************************************************************************)
+val stat: unit->unit
+
+
+module type Comp =
+  sig
+    type t
+    type u
+    val hash_sub :  u -> t -> t
+    val equal : t -> t -> bool
+    val hash : t -> int
+  end
+
+module type S =
+  sig
+    type t
+    type u
+    val f : unit -> (u -> t -> t)
+  end
+
+module Make(X:Comp): (S with type t = X.t and type u = X.u)
+
+val simple_hcons : (unit -> 'u -> 't -> 't) -> ('u -> 't -> 't)
+val recursive_hcons : (unit -> ('t -> 't) * 'u -> 't -> 't) -> ('u -> 't -> 't)
+val recursive_loop_hcons :
+    (unit -> ('t -> 't) * 'u -> 't -> 't) -> ('u -> 't -> 't)
+val recursive2_hcons :
+  (unit -> ('t1 -> 't1) * ('t2 -> 't2) * 'u1 -> 't1 -> 't1) ->
+    (unit -> ('t1 -> 't1) * ('t2 -> 't2) * 'u2 -> 't2 -> 't2) ->
+      'u1 -> 'u2 -> ('t1 -> 't1) * ('t2 -> 't2)
+
+
+(* Declaring and reinitializing global hash-consing functions *)
+val init : unit -> unit
+val register_hcons : ('u -> 't -> 't) -> ('u -> 't -> 't)
+
+
+module Hstring : (S with type t = string and type u = unit)
+module Hobj : (S with type t = Obj.t and type u = (Obj.t -> Obj.t) * unit)
+
+val string : string -> string
+val obj : Obj.t -> Obj.t
+
+val magic_hash : 'a -> 'a
+
+(* $Id$ *)
+
diff --git a/lib/pp.ml b/lib/pp.ml
new file mode 100644
index 0000000000..0588970bcf
--- /dev/null
+++ b/lib/pp.ml
@@ -0,0 +1,175 @@
+
+(* $Id$ *)
+
+open Pp_control
+
+(* The different kinds of blocks are: 
+   \begin{description}
+   \item[hbox:] Horizontal block no line breaking;
+   \item[vbox:] Vertical block each break leads to a new line;
+   \item[hvbox:] Horizontal-vertical block: same as vbox, except if
+      this block is small enough to fit on a single line
+   \item[hovbox:] Horizontal or Vertical block: breaks lead to new line
+      only when necessary to print the content of the block
+   \item[tbox:] Tabulation block: go to tabulation marks and no line breaking
+      (except if no mark yet on the reste of the line)
+   \end{description}
+ *)
+   
+type block_type =
+  | Pp_hbox of int
+  | Pp_vbox of int
+  | Pp_hvbox of int
+  | Pp_hovbox of int
+  | Pp_tbox
+
+type 'a ppcmd_token =
+  | Ppcmd_print of 'a
+  | Ppcmd_box of block_type * ('a ppcmd_token Stream.t)
+  | Ppcmd_print_break of int * int
+  | Ppcmd_set_tab
+  | Ppcmd_print_tbreak of int * int
+  | Ppcmd_white_space of int
+  | Ppcmd_force_newline
+  | Ppcmd_print_if_broken
+  | Ppcmd_open_box of block_type
+  | Ppcmd_close_box
+  | Ppcmd_close_tbox
+
+type 'a ppdir_token =
+  | Ppdir_ppcmds of 'a ppcmd_token Stream.t
+  | Ppdir_print_newline
+  | Ppdir_print_flush
+
+type std_ppcmds = (int*string) ppcmd_token Stream.t
+type 'a ppdirs = 'a ppdir_token Stream.t
+
+
+(* formatting commands *)
+let sTR s = Ppcmd_print (String.length s,s)
+let sTRas (i,s) = Ppcmd_print (i,s)
+let bRK (a,b) = Ppcmd_print_break (a,b)
+let tBRK (a,b) = Ppcmd_print_tbreak (a,b)
+let tAB = Ppcmd_set_tab
+let fNL = Ppcmd_force_newline
+let pifB = Ppcmd_print_if_broken
+let wS n = Ppcmd_white_space n
+
+(* derived commands *)
+let sPC = Ppcmd_print_break (1,0)
+let cUT = Ppcmd_print_break (0,0)
+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)
+let qSTRING s = sTR ("\""^(String.escaped s)^"\"")
+let qS = qSTRING
+
+(* boxing commands *)
+let h n s = [< 'Ppcmd_box(Pp_hbox n,s) >]
+let v n s = [< 'Ppcmd_box(Pp_vbox n,s) >]
+let hV n s = [< 'Ppcmd_box(Pp_hvbox n,s) >]
+let hOV n s = [< 'Ppcmd_box(Pp_hovbox n,s) >]
+let t s = [< 'Ppcmd_box(Pp_tbox,s) >]
+
+(* Opening and closing of boxes *)
+let hB n = Ppcmd_open_box(Pp_hbox n)
+let vB n = Ppcmd_open_box(Pp_vbox n)
+let hVB n = Ppcmd_open_box(Pp_hvbox n)
+let hOVB n = Ppcmd_open_box(Pp_hovbox n)
+let tB = Ppcmd_open_box Pp_tbox
+let cLOSE = Ppcmd_close_box
+let tCLOSE = Ppcmd_close_tbox
+
+
+(* pretty printing functions *)
+let pp_dirs ft = 
+  let maxbox = (get_gp ft).max_depth in
+  let pp_open_box = function
+    | Pp_hbox n   -> Format.pp_open_hbox ft ()
+    | Pp_vbox n   -> Format.pp_open_vbox ft n
+    | Pp_hvbox n  -> Format.pp_open_hvbox ft n
+    | Pp_hovbox n -> Format.pp_open_hovbox ft n
+    | Pp_tbox     -> Format.pp_open_tbox ft () 
+  in
+  let rec pp_cmd = function
+    | Ppcmd_print(n,s)        -> Format.pp_print_as ft n s
+    | Ppcmd_box(bty,ss)       -> (* Prevent evaluation of the stream! *)
+        pp_open_box bty ;
+        if not (Format.over_max_boxes ()) then Stream.iter pp_cmd ss;
+        Format.pp_close_box ft ()
+    | Ppcmd_open_box bty      -> pp_open_box bty
+    | Ppcmd_close_box         -> Format.pp_close_box ft ()
+    | Ppcmd_close_tbox        -> Format.pp_close_tbox ft ()
+    | Ppcmd_white_space n     -> Format.pp_print_break ft n 0
+    | Ppcmd_print_break(m,n)  -> Format.pp_print_break ft m n
+    | Ppcmd_set_tab           -> Format.pp_set_tab ft ()
+    | Ppcmd_print_tbreak(m,n) -> Format.pp_print_tbreak ft m n
+    | Ppcmd_force_newline     -> Format.pp_force_newline ft ()
+    | Ppcmd_print_if_broken   -> Format.pp_print_if_newline ft () 
+  in
+  let pp_dir = function
+    | Ppdir_ppcmds cmdstream -> Stream.iter pp_cmd cmdstream
+    | Ppdir_print_newline    -> Format.pp_print_newline ft ()
+    | Ppdir_print_flush      -> Format.pp_print_flush ft () 
+  in
+  fun dirstream ->
+    try  
+      Stream.iter pp_dir dirstream
+    with 
+      | e -> Format.pp_print_flush ft () ; raise e
+
+
+(* pretty print on stdout and stderr *)
+
+let pp_std_dirs = pp_dirs std_ft
+let pp_err_dirs = pp_dirs err_ft
+
+let pPCMDS x = Ppdir_ppcmds x
+
+(* pretty printing functions WITHOUT FLUSH *)
+let pP_with ft strm =
+  pp_dirs ft [< 'pPCMDS strm >]
+
+let pPNL_with ft strm =
+  pp_dirs ft [< 'pPCMDS [< strm ; 'Ppcmd_force_newline >] >]
+
+let warning_with ft string =
+  pPNL_with ft [< 'sTR"Warning: " ; 'sTR string >]
+
+let wARN_with ft pps =
+  pPNL_with ft [< 'sTR"Warning: " ; pps >]
+
+let pp_flush_with ft =
+  Format.pp_print_flush ft
+
+
+(* pretty printing functions WITH FLUSH *)
+let mSG_with ft strm =
+  pp_dirs ft [< 'pPCMDS strm ; 'Ppdir_print_flush >]
+
+let mSGNL_with ft strm =
+  pp_dirs ft [< 'pPCMDS strm ; 'Ppdir_print_newline >]
+
+let wARNING_with ft strm=
+  pp_dirs ft [<'pPCMDS ([<'sTR "Warning: "; strm>]); 'Ppdir_print_newline>]
+
+
+(* pretty printing functions WITHOUT FLUSH *)
+let pP        = pP_with std_ft
+let pPNL      = pPNL_with std_ft
+let pPERR     = pP_with err_ft
+let pPERRNL   = pPNL_with err_ft
+let message s = pPNL [< 'sTR s >]
+let warning   = warning_with std_ft
+let wARN      = wARN_with std_ft
+let pp_flush  = Format.pp_print_flush std_ft
+let flush_all() = flush stderr; flush stdout; pp_flush()
+
+(* pretty printing functions WITH FLUSH *)
+let mSG = mSG_with std_ft
+let mSGNL = mSGNL_with std_ft
+let mSGERR = mSG_with err_ft
+let mSGERRNL = mSGNL_with err_ft
+let wARNING = wARNING_with std_ft
+
diff --git a/lib/pp.mli b/lib/pp.mli
new file mode 100644
index 0000000000..72bbde1b92
--- /dev/null
+++ b/lib/pp.mli
@@ -0,0 +1,79 @@
+
+(* $Id$ *)
+
+open Pp_control
+
+type 'a ppcmd_token
+
+type std_ppcmds = (int*string) ppcmd_token Stream.t
+
+(* formatting commands *)
+val sTR  : string -> (int*string) ppcmd_token (* string *)
+val sTRas : int * string -> (int*string) ppcmd_token
+                                              (* string with length *)
+val bRK  : int * int -> 'a ppcmd_token        (* break *)
+val tBRK : int * int -> 'a ppcmd_token        (* go to tabulation *)
+val tAB  : 'a ppcmd_token                     (* set tabulation *)
+val fNL  : 'a ppcmd_token                     (* force newline *)
+val pifB : 'a ppcmd_token                     (* print if broken *)
+val wS   : int -> 'a ppcmd_token              (* white space *)
+
+(* derived commands *)
+val sPC     : 'a ppcmd_token                        (* space *)
+val cUT     : 'a ppcmd_token                        (* cut *)
+val aLIGN   : 'a ppcmd_token                        (* go to tab *)
+val iNT     : int -> (int*string) ppcmd_token       (* int *)
+val rEAL    : float -> (int * string) ppcmd_token   (* real *)
+val bOOL    : bool -> (int * string) ppcmd_token    (* bool *)
+val qSTRING : string -> (int * string) ppcmd_token  (* quoted string *)
+val qS      : string -> (int * string) ppcmd_token  (*   "       "   *)
+
+(* boxing commands *)
+val h   : int -> std_ppcmds -> std_ppcmds (* H box   *) 
+val v   : int -> std_ppcmds -> std_ppcmds (* V box   *)
+val hV  : int -> std_ppcmds -> std_ppcmds (* HV box  *)  
+val hOV : int -> std_ppcmds -> std_ppcmds (* HOV box *)
+val t   : std_ppcmds -> std_ppcmds        (* TAB box *)
+
+(* Opening and closing of boxes *)
+val hB    : int -> 'a ppcmd_token  (* open hbox *)
+val vB    : int -> 'a ppcmd_token  (* open vbox *)
+val hVB   : int -> 'a ppcmd_token  (* open hvbox *)
+val hOVB  : int -> 'a ppcmd_token  (* open hovbox *)
+val tB    : 'a ppcmd_token         (* open tbox *)
+val cLOSE : 'a ppcmd_token         (* close box *)
+val tCLOSE: 'a ppcmd_token         (* close tbox *)
+
+
+(* pretty printing functions WITHOUT FLUSH *)
+val pP_with       : Format.formatter -> std_ppcmds -> unit
+val pPNL_with     : Format.formatter -> std_ppcmds -> unit
+val warning_with  : Format.formatter -> string -> unit
+val wARN_with     : Format.formatter -> std_ppcmds -> unit
+val pp_flush_with : Format.formatter -> unit -> unit
+
+(* pretty printing functions WITH FLUSH *)
+val mSG_with      : Format.formatter -> std_ppcmds -> unit
+val mSGNL_with    : Format.formatter -> std_ppcmds -> unit
+
+
+(* These are instances of the previous ones on std_ft and err_ft *)
+
+(* pretty printing functions WITHOUT FLUSH on stdout and stderr *)
+val pP       : std_ppcmds -> unit
+val pPNL     : std_ppcmds -> unit
+val pPERR    : std_ppcmds -> unit
+val pPERRNL  : std_ppcmds -> unit
+val message  : string -> unit       (* = pPNL *)
+val warning  : string -> unit
+val wARN     : std_ppcmds -> unit
+val pp_flush : unit -> unit
+val flush_all: unit -> unit
+
+(* pretty printing functions WITH FLUSH on stdout and stderr *)
+val mSG      : std_ppcmds -> unit
+val mSGNL    : std_ppcmds -> unit
+val mSGERR   : std_ppcmds -> unit
+val mSGERRNL : std_ppcmds -> unit
+val wARNING  : std_ppcmds -> unit
+
diff --git a/lib/pp_control.ml b/lib/pp_control.ml
new file mode 100644
index 0000000000..3eb10e6dde
--- /dev/null
+++ b/lib/pp_control.ml
@@ -0,0 +1,93 @@
+
+(* $Id$ *)
+
+(* Parameters of pretty-printing *)
+
+type pp_global_params = {
+  margin : int;
+  max_indent : int;
+  max_depth : int;
+  ellipsis : string }
+
+(* Default parameters of pretty-printing *)
+
+let dflt_gp = { 
+  margin     = 72;
+  max_indent = 62;
+  max_depth  = 50;
+  ellipsis   = "." }
+
+(* A deeper pretty-printer to print proof scripts *)
+
+let deep_gp = { 
+  margin     = 72;
+  max_indent = 62;
+  max_depth  = 10000;
+  ellipsis   = "." }
+
+(* set_gp : Format.formatter -> pp_global_params -> unit
+ * set the parameters of a formatter *)
+
+let set_gp ft gp = 
+  Format.pp_set_margin ft gp.margin ;
+  Format.pp_set_max_indent ft gp.max_indent ;
+  Format.pp_set_max_boxes ft gp.max_depth ;
+  Format.pp_set_ellipsis_text ft gp.ellipsis
+
+let set_dflt_gp ft = set_gp ft dflt_gp 
+
+let get_gp ft =
+  { margin = Format.pp_get_margin ft ();
+    max_indent = Format.pp_get_max_indent ft ();
+    max_depth = Format.pp_get_max_boxes ft ();
+    ellipsis = Format.pp_get_ellipsis_text ft () }
+
+
+(* Output functions of pretty-printing *)
+
+type 'a pp_formatter_params = {
+  fp_output : out_channel ;
+  fp_output_function : string -> int -> int -> unit ;
+  fp_flush_function : unit -> unit }
+				
+(* Output functions for stdout and stderr *)
+
+let std_fp = {
+  fp_output = stdout ;
+  fp_output_function = output stdout;
+  fp_flush_function = (fun () -> flush stdout) }
+
+let err_fp = {
+  fp_output = stderr ;
+  fp_output_function = output stderr;
+  fp_flush_function = (fun () -> flush stderr) }
+
+(* with_fp : 'a pp_formatter_params -> Format.formatter 
+ * returns of formatter for given formatter functions *)
+
+let with_fp fp =
+  let ft = Format.make_formatter fp.fp_output_function fp.fp_flush_function in
+  Format.pp_set_formatter_out_channel ft fp.fp_output;
+  ft
+
+(* Output on a channel ch *)
+
+let with_output_to ch =
+  let ft = with_fp { fp_output = ch ;
+      	             fp_output_function = (output ch) ;
+	             fp_flush_function = (fun () -> flush ch) } in
+  set_dflt_gp ft; 
+  ft
+
+let std_ft = Format.std_formatter
+let _ = set_dflt_gp std_ft
+
+let err_ft = with_output_to stderr
+
+let deep_ft = with_output_to stdout
+let _ = set_gp deep_ft deep_gp
+
+(* For parametrization through vernacular *)
+let set_depth_boxes v  = Format.pp_set_max_boxes std_ft v
+let get_depth_boxes () = Format.pp_get_max_boxes std_ft ()
+
diff --git a/lib/pp_control.mli b/lib/pp_control.mli
new file mode 100644
index 0000000000..03a1487bf1
--- /dev/null
+++ b/lib/pp_control.mli
@@ -0,0 +1,38 @@
+
+(* $Id$ *)
+
+(* Parameters of pretty-printing *)
+
+type pp_global_params = { 
+  margin : int;
+  max_indent : int;
+  max_depth : int;
+  ellipsis : string }
+
+val dflt_gp : pp_global_params                (* default parameters *)
+val deep_gp : pp_global_params                (* with depth = 10000 *)
+val set_gp : Format.formatter -> pp_global_params -> unit
+val set_dflt_gp : Format.formatter -> unit
+val get_gp : Format.formatter -> pp_global_params
+
+
+(* Output functions of pretty-printing *)
+
+type 'a pp_formatter_params ={ 
+  fp_output : out_channel ;
+  fp_output_function : string -> int -> int -> unit ;
+  fp_flush_function : unit -> unit }
+
+val std_fp : (int*string) pp_formatter_params (* output functions for stdout *)
+val err_fp : (int*string) pp_formatter_params (* output functions for stderr *)
+
+val with_fp : 'a pp_formatter_params -> Format.formatter
+val with_output_to : out_channel -> Format.formatter
+
+val std_ft : Format.formatter  (* the formatter on stdout *)
+val err_ft : Format.formatter  (* the formatter on stderr *)
+val deep_ft : Format.formatter (* a deep formatter on stdout (depth=10000) *)
+
+(* For parametrization through vernacular *)
+val set_depth_boxes : int -> unit
+val get_depth_boxes : unit -> int
diff --git a/lib/util.ml b/lib/util.ml
new file mode 100644
index 0000000000..f04b2cf4b9
--- /dev/null
+++ b/lib/util.ml
@@ -0,0 +1,81 @@
+
+(* $Id$ *)
+
+open Pp
+
+(* Strings *)
+
+let explode s = 
+  let rec explode_rec n =
+    if n >= String.length s then
+      []
+    else 
+      String.make 1 (String.get s n) :: explode_rec (succ n)
+  in 
+  explode_rec 0
+
+let implode sl =
+  let len = List.fold_left (fun a b -> a + (String.length b)) 0 sl in
+  let dest = String.create len in
+  let _ = List.fold_left 
+	    (fun start src ->
+	       let src_len = String.length src in
+	       String.blit src 0 dest start src_len;
+	       start + src_len)
+	    0 sl 
+  in
+  dest
+
+let parse_section_path s =
+  let len = String.length s in
+  let rec decoupe_dirs n =
+    try
+      let pos = String.index_from s n '#' in
+      let dir = String.sub s n (pos-n) in
+      let dirs,n' = decoupe_dirs (succ pos) in
+      dir::dirs,n'
+    with
+      | Not_found -> [],n
+  in
+  let decoupe_kind n =
+    try
+      let pos = String.index_from s n '.' in
+      String.sub s n (pos-n), String.sub s (succ pos) (pred (len-pos))
+    with
+      | Not_found -> invalid_arg "parse_section_path"
+  in
+  if len = 0 || String.get s 0 <> '#' then
+    invalid_arg "parse_section_path"
+  else
+    let dirs,n = decoupe_dirs 1 in
+    let id,k = decoupe_kind n in
+    dirs,id,k
+
+(* Pretty-printing *)
+  
+let pr_spc () = [< 'sPC >];;
+let pr_fnl () = [< 'fNL >];;
+let pr_int n = [< 'iNT n >];;
+let pr_str s = [< 'sTR s >];;
+let pr_coma () = [< 'sTR","; 'sPC >];;
+
+let rec prlist elem l = match l with 
+  | []   -> [< >]
+  | h::t -> let e = elem h and r = prlist elem t in [< e; r >]
+
+let rec prlist_with_sep sep elem l = match l with
+  | []   -> [< >]
+  | [h]  -> elem h
+  | h::t ->
+      let e = elem h and s = sep() and r = prlist_with_sep sep elem t in
+      [< e; s; r >]
+      
+let prvect_with_sep sep elem v =
+  let rec pr n =
+    if n = 0 then 
+      elem v.(0)
+    else 
+      let r = pr (n-1) and s = sep() and e = elem v.(n) in 
+      [< r; s; e >]
+  in
+  if Array.length v = 0 then [< >] else pr (Array.length v - 1)
diff --git a/lib/util.mli b/lib/util.mli
new file mode 100644
index 0000000000..25b419be83
--- /dev/null
+++ b/lib/util.mli
@@ -0,0 +1,25 @@
+
+(* $Id$ *)
+
+open Pp
+
+(* Strings *)
+
+val explode : string -> string list
+val implode : string list -> string
+
+val parse_section_path : string -> string list * string * string
+
+(* Pretty-printing *)
+
+val pr_spc : unit -> std_ppcmds
+val pr_fnl : unit -> std_ppcmds
+val pr_int : int -> std_ppcmds
+val pr_str : string -> std_ppcmds
+val pr_coma : unit -> std_ppcmds
+
+val prlist : ('a -> 'b Stream.t) -> 'a list -> 'b Stream.t
+val prlist_with_sep :
+   (unit -> 'a Stream.t) -> ('b -> 'a Stream.t) -> 'b list -> 'a Stream.t
+val prvect_with_sep :
+   (unit -> 'a Stream.t) -> ('b -> 'a Stream.t) -> 'b array -> 'a Stream.t