From: Kim Nguyễn <kn@lri.fr>
Date: Thu, 4 Apr 2013 16:48:43 +0000 (+0200)
Subject: Flatten the sources, only leave the XPath module packed.
X-Git-Tag: v0.1~105^2
X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=commitdiff_plain;h=b00bff88c7902e828804c06b7f9dc55222fdc84e

Flatten the sources, only leave the XPath module packed.
---

diff --git a/_tags b/_tags
index f500328..347e39c 100644
--- a/_tags
+++ b/_tags
@@ -16,14 +16,6 @@ true:    inline(1000), unsafe(true)
 <src/xpath/*.cmx>:  for-pack(Xpath)
 <src/xpath>:        include
 
-<src/utils/*.cmx>:  for-pack(Utils)
-<src/utils>: include
-
-<src/tree/*.cmx>:   for-pack(Tree)
-<src/tree>: include
-
-<src/auto/*.cmx>:   for-pack(Auto)
-<src/auto>: include
 <src>: include
 
 #Enable warning for all but generated files:
diff --git a/src/ata.ml b/src/ata.ml
new file mode 100644
index 0000000..08a4308
--- /dev/null
+++ b/src/ata.ml
@@ -0,0 +1,474 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                               TAToo                                 *)
+(*                                                                     *)
+(*                     Kim Nguyen, LRI UMR8623                         *)
+(*                   Université Paris-Sud & CNRS                       *)
+(*                                                                     *)
+(*  Copyright 2010-2013 Université Paris-Sud and Centre National de la *)
+(*  Recherche Scientifique. All rights reserved.  This file is         *)
+(*  distributed under the terms of the GNU Lesser General Public       *)
+(*  License, with the special exception on linking described in file   *)
+(*  ../LICENSE.                                                        *)
+(*                                                                     *)
+(***********************************************************************)
+
+(*
+  Time-stamp: <Last modified on 2013-04-04 18:46:50 CEST by Kim Nguyen>
+*)
+
+INCLUDE "utils.ml"
+open Format
+
+type predicate = | First_child
+                 | Next_sibling
+                 | Parent
+                 | Previous_sibling
+                 | Stay
+                 | Is_first_child
+                 | Is_next_sibling
+                 | Is of (Tree.NodeKind.t)
+                 | Has_first_child
+                 | Has_next_sibling
+
+let is_move p = match p with
+| First_child | Next_sibling
+| Parent | Previous_sibling | Stay -> true
+| _ -> false
+
+
+type atom = predicate * bool * State.t
+
+module Atom : (Formula.ATOM with type data = atom) =
+struct
+
+  module Node =
+  struct
+    type t = atom
+    let equal n1 n2 = n1 = n2
+    let hash n = Hashtbl.hash n
+  end
+
+  include Hcons.Make(Node)
+
+  let print ppf a =
+    let p, b, q = a.node in
+    if not b then fprintf ppf "%s" Pretty.lnot;
+    match p with
+    | First_child -> fprintf ppf "FC(%a)" State.print q
+    | Next_sibling -> fprintf ppf "NS(%a)" State.print q
+    | Parent -> fprintf ppf "FC%s(%a)" Pretty.inverse State.print q
+    | Previous_sibling -> fprintf ppf "NS%s(%a)" Pretty.inverse State.print q
+    | Stay -> fprintf ppf "%s(%a)" Pretty.epsilon State.print q
+    | Is_first_child -> fprintf ppf "FC%s?" Pretty.inverse
+    | Is_next_sibling -> fprintf ppf "NS%s?" Pretty.inverse
+    | Is k -> fprintf ppf "is-%a?" Tree.NodeKind.print k
+    | Has_first_child -> fprintf ppf "FC?"
+    | Has_next_sibling -> fprintf ppf "NS?"
+
+  let neg a =
+    let p, b, q = a.node in
+    make (p, not b, q)
+
+
+end
+
+module SFormula =
+struct
+  include Formula.Make(Atom)
+  open Tree.NodeKind
+  let mk_atom a b c = atom_ (Atom.make (a,b,c))
+  let mk_kind k = mk_atom (Is k) true State.dummy
+  let has_first_child =
+    (mk_atom Has_first_child true State.dummy)
+
+  let has_next_sibling =
+    (mk_atom Has_next_sibling true State.dummy)
+
+  let is_first_child =
+    (mk_atom Is_first_child true State.dummy)
+
+  let is_next_sibling =
+    (mk_atom Is_next_sibling true State.dummy)
+
+  let is_attribute =
+    (mk_atom (Is Attribute) true State.dummy)
+
+  let is_element =
+    (mk_atom (Is Element) true State.dummy)
+
+  let is_processing_instruction =
+    (mk_atom (Is ProcessingInstruction) true State.dummy)
+
+  let is_comment =
+    (mk_atom (Is Comment) true State.dummy)
+
+  let first_child q =
+  and_
+    (mk_atom First_child true q)
+    has_first_child
+
+  let next_sibling q =
+  and_
+    (mk_atom Next_sibling true q)
+    has_next_sibling
+
+  let parent q =
+  and_
+    (mk_atom Parent true q)
+    is_first_child
+
+  let previous_sibling q =
+  and_
+    (mk_atom Previous_sibling true q)
+    is_next_sibling
+
+  let stay q =
+    (mk_atom Stay true q)
+
+  let get_states phi =
+    fold (fun phi acc ->
+      match expr phi with
+      | Formula.Atom a -> let _, _, q = Atom.node a in
+                          if q != State.dummy then StateSet.add q acc else acc
+      | _ -> acc
+    ) phi StateSet.empty
+
+end
+
+
+module Transition = Hcons.Make (struct
+  type t = State.t * QNameSet.t * SFormula.t
+  let equal (a, b, c) (d, e, f) =
+    a == d && b == e && c == f
+  let hash (a, b, c) =
+    HASHINT4 (PRIME1, a, ((QNameSet.uid b) :> int), ((SFormula.uid c) :> int))
+end)
+
+
+module TransList : sig
+  include Hlist.S with type elt = Transition.t
+  val print : Format.formatter -> ?sep:string -> t -> unit
+end =
+  struct
+    include Hlist.Make(Transition)
+    let print ppf ?(sep="\n") l =
+      iter (fun t ->
+        let q, lab, f = Transition.node t in
+        fprintf ppf "%a, %a -> %a%s" State.print q QNameSet.print lab SFormula.print f sep) l
+  end
+
+
+type t = {
+  id : Uid.t;
+  mutable states : StateSet.t;
+  mutable selection_states: StateSet.t;
+  transitions: (State.t, (QNameSet.t*SFormula.t) list) Hashtbl.t;
+  mutable cache2 : TransList.t Cache.N2.t;
+  mutable cache6 : (TransList.t*StateSet.t) Cache.N6.t;
+}
+
+let next = Uid.make_maker ()
+
+let dummy2 = TransList.cons
+  (Transition.make (State.dummy,QNameSet.empty, SFormula.false_))
+  TransList.nil
+
+let dummy6 = (dummy2, StateSet.empty)
+
+
+let create s ss = { id = next ();
+                  states = s;
+                  selection_states = ss;
+                  transitions = Hashtbl.create 17;
+                  cache2 = Cache.N2.create dummy2;
+                  cache6 = Cache.N6.create dummy6;
+ }
+
+let reset a =
+  a.cache2 <- Cache.N2.create dummy2;
+  a.cache6 <- Cache.N6.create dummy6
+
+
+let get_trans_aux a tag states =
+  StateSet.fold (fun q acc0 ->
+    try
+      let trs = Hashtbl.find a.transitions q in
+      List.fold_left (fun acc1 (labs, phi) ->
+        if QNameSet.mem tag labs then TransList.cons (Transition.make (q, labs, phi)) acc1 else acc1) acc0 trs
+    with Not_found -> acc0
+  ) states TransList.nil
+
+
+let get_trans a tag states =
+  let trs =
+    Cache.N2.find a.cache2
+      (tag.QName.id :> int) (states.StateSet.id :> int)
+  in
+  if trs == dummy2 then
+    let trs = get_trans_aux a tag states in
+    (Cache.N2.add
+       a.cache2
+       (tag.QName.id :> int)
+       (states.StateSet.id :> int) trs; trs)
+  else trs
+
+
+
+let eval_form phi fcs nss ps ss is_left is_right has_left has_right kind =
+  let rec loop phi =
+    begin match SFormula.expr phi with
+      Formula.True -> true
+    | Formula.False -> false
+    | Formula.Atom a ->
+        let p, b, q = Atom.node a in
+        let pos =
+          match p with
+          | First_child -> StateSet.mem q fcs
+          | Next_sibling ->  StateSet.mem q nss
+          | Parent | Previous_sibling -> StateSet.mem q ps
+          | Stay -> StateSet.mem q ss
+          | Is_first_child -> is_left
+          | Is_next_sibling -> is_right
+          | Is k -> k == kind
+          | Has_first_child -> has_left
+          | Has_next_sibling -> has_right
+        in
+        if is_move p && (not b) then
+          eprintf "Warning: Invalid negative atom %a" Atom.print a;
+        b == pos
+    | Formula.And(phi1, phi2) -> loop phi1 && loop phi2
+    | Formula.Or (phi1, phi2) -> loop phi1 || loop phi2
+    end
+  in
+  loop phi
+
+let int_of_conf is_left is_right has_left has_right kind =
+  ((Obj.magic kind) lsl 4) lor
+    ((Obj.magic is_left) lsl 3) lor
+    ((Obj.magic is_right) lsl 2) lor
+    ((Obj.magic has_left) lsl 1) lor
+    (Obj.magic has_right)
+
+let eval_trans auto ltrs fcs nss ps ss is_left is_right has_left has_right kind =
+  let i = int_of_conf is_left is_right has_left has_right kind
+  and k = (fcs.StateSet.id :> int)
+  and l = (nss.StateSet.id :> int)
+  and m = (ps.StateSet.id :> int)
+  in
+
+  let rec loop ltrs ss =
+    let j = (ltrs.TransList.id :> int)
+    and n = (ss.StateSet.id :> int) in
+    let (new_ltrs, new_ss) as res =
+      let res = Cache.N6.find auto.cache6 i j k l m n in
+      if res == dummy6 then
+        let res =
+          TransList.fold (fun trs (acct, accs) ->
+            let q, _, phi = Transition.node trs in
+            if StateSet.mem q accs then (acct, accs) else
+              if eval_form
+                phi fcs nss ps accs
+                is_left is_right has_left has_right kind
+              then
+                (acct, StateSet.add q accs)
+              else
+                (TransList.cons trs acct, accs)
+          ) ltrs (TransList.nil, ss)
+        in
+        Cache.N6.add auto.cache6 i j k l m n res; res
+      else
+        res
+    in
+    if new_ss == ss then res else
+      loop new_ltrs new_ss
+  in
+  loop ltrs ss
+
+
+
+
+
+(*
+  [add_trans a q labels f] adds a transition [(q,labels) -> f] to the
+  automaton [a] but ensures that transitions remains pairwise disjoint
+*)
+
+let add_trans a q s f =
+  let trs = try Hashtbl.find a.transitions q with Not_found -> [] in
+  let cup, ntrs =
+    List.fold_left (fun (acup, atrs) (labs, phi) ->
+      let lab1 = QNameSet.inter labs s in
+      let lab2 = QNameSet.diff labs s in
+      let tr1 =
+        if QNameSet.is_empty lab1 then []
+        else [ (lab1, SFormula.or_ phi f) ]
+      in
+      let tr2 =
+        if QNameSet.is_empty lab2 then []
+        else [ (lab2, SFormula.or_ phi f) ]
+      in
+      (QNameSet.union acup labs, tr1@ tr2 @ atrs)
+    ) (QNameSet.empty, []) trs
+  in
+  let rem = QNameSet.diff s cup in
+  let ntrs = if QNameSet.is_empty rem then ntrs
+    else (rem, f) :: ntrs
+  in
+  Hashtbl.replace a.transitions q ntrs
+
+let _pr_buff = Buffer.create 50
+let _str_fmt = formatter_of_buffer _pr_buff
+let _flush_str_fmt () = pp_print_flush _str_fmt ();
+  let s = Buffer.contents _pr_buff in
+  Buffer.clear _pr_buff; s
+
+let print fmt a =
+  fprintf fmt
+    "\nInternal UID: %i@\n\
+     States: %a@\n\
+     Selection states: %a@\n\
+     Alternating transitions:@\n"
+    (a.id :> int)
+    StateSet.print a.states
+    StateSet.print a.selection_states;
+  let trs =
+    Hashtbl.fold
+      (fun q t acc -> List.fold_left (fun acc (s , f) -> (q,s,f)::acc) acc t)
+      a.transitions
+      []
+  in
+  let sorted_trs = List.stable_sort (fun (q1, s1, _) (q2, s2, _) ->
+    let c = State.compare q1 q2 in - (if c == 0 then QNameSet.compare s1 s2 else c))
+    trs
+  in
+  let _ = _flush_str_fmt () in
+  let strs_strings, max_pre, max_all = List.fold_left (fun (accl, accp, acca) (q, s, f) ->
+    let s1 = State.print _str_fmt q; _flush_str_fmt () in
+    let s2 = QNameSet.print _str_fmt s;  _flush_str_fmt () in
+    let s3 = SFormula.print _str_fmt f;  _flush_str_fmt () in
+    let pre = Pretty.length s1 + Pretty.length s2 in
+    let all = Pretty.length s3 in
+    ( (q, s1, s2, s3) :: accl, max accp pre, max acca all)
+  ) ([], 0, 0) sorted_trs
+  in
+  let line = Pretty.line (max_all + max_pre + 6) in
+  let prev_q = ref State.dummy in
+  List.iter (fun (q, s1, s2, s3) ->
+    if !prev_q != q && !prev_q != State.dummy then fprintf fmt " %s\n%!"  line;
+    prev_q := q;
+    fprintf fmt " %s, %s" s1 s2;
+    fprintf fmt "%s" (Pretty.padding (max_pre - Pretty.length s1 - Pretty.length s2));
+    fprintf fmt " %s  %s@\n%!" Pretty.right_arrow s3;
+  ) strs_strings;
+  fprintf fmt " %s\n%!" line
+
+(*
+  [complete transitions a] ensures that for each state q
+  and each symbols s in the alphabet, a transition q, s exists.
+  (adding q, s -> F when necessary).
+*)
+
+let complete_transitions a =
+  StateSet.iter (fun q ->
+    let qtrans = Hashtbl.find a.transitions q in
+    let rem =
+      List.fold_left (fun rem (labels, _) ->
+        QNameSet.diff rem labels) QNameSet.any qtrans
+    in
+    let nqtrans =
+      if QNameSet.is_empty rem then qtrans
+      else
+        (rem, SFormula.false_) :: qtrans
+    in
+    Hashtbl.replace a.transitions q nqtrans
+  ) a.states
+
+let cleanup_states a =
+  let memo = ref StateSet.empty in
+  let rec loop q =
+    if not (StateSet.mem q !memo) then begin
+      memo := StateSet.add q !memo;
+      let trs = try Hashtbl.find a.transitions q with Not_found -> [] in
+      List.iter (fun (_, phi) ->
+        StateSet.iter loop (SFormula.get_states phi)) trs
+    end
+  in
+  StateSet.iter loop a.selection_states;
+  let unused = StateSet.diff a.states !memo in
+  eprintf "Unused states %a\n%!" StateSet.print unused;
+  StateSet.iter (fun q -> Hashtbl.remove a.transitions q) unused;
+  a.states <- !memo
+
+(* [normalize_negations a] removes negative atoms in the formula
+   complementing the sub-automaton in the negative states.
+   [TODO check the meaning of negative upward arrows]
+*)
+
+let normalize_negations auto =
+  eprintf "Automaton before normalize_trans:\n";
+  print err_formatter auto;
+  eprintf "--------------------\n%!";
+
+  let memo_state = Hashtbl.create 17 in
+  let todo = Queue.create () in
+  let rec flip b f =
+    match SFormula.expr f with
+      Formula.True | Formula.False -> if b then f else SFormula.not_ f
+    | Formula.Or(f1, f2) -> (if b then SFormula.or_ else SFormula.and_)(flip b f1) (flip b f2)
+    | Formula.And(f1, f2) -> (if b then SFormula.and_ else SFormula.or_)(flip b f1) (flip b f2)
+    | Formula.Atom(a) -> begin
+      let l, b', q = Atom.node a in
+      if q == State.dummy then if b then f else SFormula.not_ f
+      else
+        if b == b' then begin
+        (* a appears positively, either no negation or double negation *)
+          if not (Hashtbl.mem memo_state (q,b)) then Queue.add (q,true) todo;
+          SFormula.atom_ (Atom.make (l, true, q))
+        end else begin
+        (* need to reverse the atom
+           either we have a positive state deep below a negation
+           or we have a negative state in a positive formula
+           b' = sign of the state
+           b = sign of the enclosing formula
+        *)
+        let not_q =
+          try
+            (* does the inverted state of q exist ? *)
+            Hashtbl.find memo_state (q, false)
+          with
+            Not_found ->
+              (* create a new state and add it to the todo queue *)
+              let nq = State.make () in
+              auto.states <- StateSet.add nq auto.states;
+              Hashtbl.add memo_state (q, false) nq;
+              Queue.add (q, false) todo; nq
+        in
+        SFormula.atom_ (Atom.make (l, true, not_q))
+      end
+    end
+  in
+  (* states that are not reachable from a selection stat are not interesting *)
+  StateSet.iter (fun q -> Queue.add (q, true) todo) auto.selection_states;
+
+  while not (Queue.is_empty todo) do
+    let (q, b) as key = Queue.pop todo in
+    let q' =
+      try
+        Hashtbl.find memo_state key
+      with
+        Not_found ->
+          let nq = if b then q else
+              let nq = State.make () in
+              auto.states <- StateSet.add nq auto.states;
+              nq
+          in
+          Hashtbl.add memo_state key nq; nq
+    in
+    let trans = Hashtbl.find auto.transitions q in
+    let trans' = List.map (fun (lab, f) -> lab, flip b f) trans in
+    Hashtbl.replace auto.transitions q' trans';
+  done;
+  cleanup_states auto
+
+
diff --git a/src/ata.mli b/src/ata.mli
new file mode 100644
index 0000000..bb94a7c
--- /dev/null
+++ b/src/ata.mli
@@ -0,0 +1,93 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                               TAToo                                 *)
+(*                                                                     *)
+(*                     Kim Nguyen, LRI UMR8623                         *)
+(*                   Université Paris-Sud & CNRS                       *)
+(*                                                                     *)
+(*  Copyright 2010-2013 Université Paris-Sud and Centre National de la *)
+(*  Recherche Scientifique. All rights reserved.  This file is         *)
+(*  distributed under the terms of the GNU Lesser General Public       *)
+(*  License, with the special exception on linking described in file   *)
+(*  ../LICENSE.                                                        *)
+(*                                                                     *)
+(***********************************************************************)
+
+(*
+  Time-stamp: <Last modified on 2013-04-04 18:42:38 CEST by Kim Nguyen>
+*)
+
+type predicate =
+    First_child
+  | Next_sibling
+  | Parent
+  | Previous_sibling
+  | Stay
+  | Is_first_child
+  | Is_next_sibling
+  | Is of Tree.NodeKind.t
+  | Has_first_child
+  | Has_next_sibling
+
+val is_move : predicate -> bool
+
+type atom = predicate * bool * State.t
+
+module Atom : Formula.ATOM with type data = atom
+
+module SFormula :
+  sig
+    include module type of Formula.Make(Atom)
+    val mk_atom : predicate -> bool -> State.t -> t
+    val mk_kind : Tree.NodeKind.t -> t
+    val has_first_child : t
+    val has_next_sibling : t
+    val is_first_child : t
+    val is_next_sibling : t
+    val is_attribute : t
+    val is_element : t
+    val is_processing_instruction : t
+    val is_comment : t
+    val first_child : State.t -> t
+    val next_sibling : State.t -> t
+    val parent : State.t -> t
+    val previous_sibling : State.t -> t
+    val stay : State.t -> t
+    val get_states : t -> StateSet.t
+  end
+
+
+module Transition : Hcons.S with
+            type data = State.t * QNameSet.t * SFormula.t
+
+module TransList : sig
+  include Hlist.S with type elt = Transition.t
+  val print : Format.formatter -> ?sep:string -> t -> unit
+end
+
+
+type t = private {
+  id : Uid.t;
+  mutable states : StateSet.t;
+  mutable selection_states: StateSet.t;
+  transitions: (State.t, (QNameSet.t*SFormula.t) list) Hashtbl.t;
+  mutable cache2 : TransList.t Cache.N2.t;
+  mutable cache6 : (TransList.t*StateSet.t) Cache.N6.t;
+}
+
+
+
+val create : StateSet.t -> StateSet.t -> t
+val reset : t -> unit
+val get_trans : t -> QNameSet.elt -> StateSet.t -> TransList.t
+
+val eval_trans : t -> TransList.t
+  -> StateSet.t -> StateSet.t -> StateSet.t -> StateSet.t
+  -> bool -> bool -> bool -> bool -> Tree.NodeKind.t
+  -> TransList.t*StateSet.t
+
+val add_trans : t -> State.t -> QNameSet.t -> SFormula.t -> unit
+val print : Format.formatter -> t -> unit
+val complete_transitions : t -> unit
+val cleanup_states : t -> unit
+val normalize_negations : t -> unit
diff --git a/src/auto.mlpack b/src/auto.mlpack
deleted file mode 100644
index 3ec7d78..0000000
--- a/src/auto.mlpack
+++ /dev/null
@@ -1,6 +0,0 @@
-auto/Ata
-auto/Formula
-auto/Eval
-auto/State
-auto/StateSet
-auto/Html
diff --git a/src/auto/ata.ml b/src/auto/ata.ml
deleted file mode 100644
index af729da..0000000
--- a/src/auto/ata.ml
+++ /dev/null
@@ -1,475 +0,0 @@
-(***********************************************************************)
-(*                                                                     *)
-(*                               TAToo                                 *)
-(*                                                                     *)
-(*                     Kim Nguyen, LRI UMR8623                         *)
-(*                   Université Paris-Sud & CNRS                       *)
-(*                                                                     *)
-(*  Copyright 2010-2013 Université Paris-Sud and Centre National de la *)
-(*  Recherche Scientifique. All rights reserved.  This file is         *)
-(*  distributed under the terms of the GNU Lesser General Public       *)
-(*  License, with the special exception on linking described in file   *)
-(*  ../LICENSE.                                                        *)
-(*                                                                     *)
-(***********************************************************************)
-
-(*
-  Time-stamp: <Last modified on 2013-03-15 18:18:11 CET by Kim Nguyen>
-*)
-
-INCLUDE "utils.ml"
-open Format
-open Utils
-
-type predicate = | First_child
-                 | Next_sibling
-                 | Parent
-                 | Previous_sibling
-                 | Stay
-                 | Is_first_child
-                 | Is_next_sibling
-                 | Is of (Tree.Common.NodeKind.t)
-                 | Has_first_child
-                 | Has_next_sibling
-
-let is_move p = match p with
-| First_child | Next_sibling
-| Parent | Previous_sibling | Stay -> true
-| _ -> false
-
-
-type atom = predicate * bool * State.t
-
-module Atom : (Formula.ATOM with type data = atom) =
-struct
-
-  module Node =
-  struct
-    type t = atom
-    let equal n1 n2 = n1 = n2
-    let hash n = Hashtbl.hash n
-  end
-
-  include Hcons.Make(Node)
-
-  let print ppf a =
-    let p, b, q = a.node in
-    if not b then fprintf ppf "%s" Pretty.lnot;
-    match p with
-    | First_child -> fprintf ppf "FC(%a)" State.print q
-    | Next_sibling -> fprintf ppf "NS(%a)" State.print q
-    | Parent -> fprintf ppf "FC%s(%a)" Pretty.inverse State.print q
-    | Previous_sibling -> fprintf ppf "NS%s(%a)" Pretty.inverse State.print q
-    | Stay -> fprintf ppf "%s(%a)" Pretty.epsilon State.print q
-    | Is_first_child -> fprintf ppf "FC%s?" Pretty.inverse
-    | Is_next_sibling -> fprintf ppf "NS%s?" Pretty.inverse
-    | Is k -> fprintf ppf "is-%a?" Tree.Common.NodeKind.print k
-    | Has_first_child -> fprintf ppf "FC?"
-    | Has_next_sibling -> fprintf ppf "NS?"
-
-  let neg a =
-    let p, b, q = a.node in
-    make (p, not b, q)
-
-
-end
-
-module SFormula =
-struct
-  include Formula.Make(Atom)
-  open Tree.Common.NodeKind
-  let mk_atom a b c = atom_ (Atom.make (a,b,c))
-  let mk_kind k = mk_atom (Is k) true State.dummy
-  let has_first_child =
-    (mk_atom Has_first_child true State.dummy)
-
-  let has_next_sibling =
-    (mk_atom Has_next_sibling true State.dummy)
-
-  let is_first_child =
-    (mk_atom Is_first_child true State.dummy)
-
-  let is_next_sibling =
-    (mk_atom Is_next_sibling true State.dummy)
-
-  let is_attribute =
-    (mk_atom (Is Attribute) true State.dummy)
-
-  let is_element =
-    (mk_atom (Is Element) true State.dummy)
-
-  let is_processing_instruction =
-    (mk_atom (Is ProcessingInstruction) true State.dummy)
-
-  let is_comment =
-    (mk_atom (Is Comment) true State.dummy)
-
-  let first_child q =
-  and_
-    (mk_atom First_child true q)
-    has_first_child
-
-  let next_sibling q =
-  and_
-    (mk_atom Next_sibling true q)
-    has_next_sibling
-
-  let parent q =
-  and_
-    (mk_atom Parent true q)
-    is_first_child
-
-  let previous_sibling q =
-  and_
-    (mk_atom Previous_sibling true q)
-    is_next_sibling
-
-  let stay q =
-    (mk_atom Stay true q)
-
-  let get_states phi =
-    fold (fun phi acc ->
-      match expr phi with
-      | Formula.Atom a -> let _, _, q = Atom.node a in
-                          if q != State.dummy then StateSet.add q acc else acc
-      | _ -> acc
-    ) phi StateSet.empty
-
-end
-
-
-module Transition = Hcons.Make (struct
-  type t = State.t * QNameSet.t * SFormula.t
-  let equal (a, b, c) (d, e, f) =
-    a == d && b == e && c == f
-  let hash (a, b, c) =
-    HASHINT4 (PRIME1, a, ((QNameSet.uid b) :> int), ((SFormula.uid c) :> int))
-end)
-
-
-module TransList : sig
-  include Hlist.S with type elt = Transition.t
-  val print : Format.formatter -> ?sep:string -> t -> unit
-end =
-  struct
-    include Hlist.Make(Transition)
-    let print ppf ?(sep="\n") l =
-      iter (fun t ->
-        let q, lab, f = Transition.node t in
-        fprintf ppf "%a, %a -> %a%s" State.print q QNameSet.print lab SFormula.print f sep) l
-  end
-
-
-type t = {
-  id : Uid.t;
-  mutable states : StateSet.t;
-  mutable selection_states: StateSet.t;
-  transitions: (State.t, (QNameSet.t*SFormula.t) list) Hashtbl.t;
-  mutable cache2 : TransList.t Cache.N2.t;
-  mutable cache6 : (TransList.t*StateSet.t) Cache.N6.t;
-}
-
-let next = Uid.make_maker ()
-
-let dummy2 = TransList.cons
-  (Transition.make (State.dummy,QNameSet.empty, SFormula.false_))
-  TransList.nil
-
-let dummy6 = (dummy2, StateSet.empty)
-
-
-let create s ss = { id = next ();
-                  states = s;
-                  selection_states = ss;
-                  transitions = Hashtbl.create 17;
-                  cache2 = Cache.N2.create dummy2;
-                  cache6 = Cache.N6.create dummy6;
- }
-
-let reset a =
-  a.cache2 <- Cache.N2.create dummy2;
-  a.cache6 <- Cache.N6.create dummy6
-
-
-let get_trans_aux a tag states =
-  StateSet.fold (fun q acc0 ->
-    try
-      let trs = Hashtbl.find a.transitions q in
-      List.fold_left (fun acc1 (labs, phi) ->
-        if QNameSet.mem tag labs then TransList.cons (Transition.make (q, labs, phi)) acc1 else acc1) acc0 trs
-    with Not_found -> acc0
-  ) states TransList.nil
-
-
-let get_trans a tag states =
-  let trs =
-    Cache.N2.find a.cache2
-      (tag.QName.id :> int) (states.StateSet.id :> int)
-  in
-  if trs == dummy2 then
-    let trs = get_trans_aux a tag states in
-    (Cache.N2.add
-       a.cache2
-       (tag.QName.id :> int)
-       (states.StateSet.id :> int) trs; trs)
-  else trs
-
-
-
-let eval_form phi fcs nss ps ss is_left is_right has_left has_right kind =
-  let rec loop phi =
-    begin match SFormula.expr phi with
-      Formula.True -> true
-    | Formula.False -> false
-    | Formula.Atom a ->
-        let p, b, q = Atom.node a in
-        let pos =
-          match p with
-          | First_child -> StateSet.mem q fcs
-          | Next_sibling ->  StateSet.mem q nss
-          | Parent | Previous_sibling -> StateSet.mem q ps
-          | Stay -> StateSet.mem q ss
-          | Is_first_child -> is_left
-          | Is_next_sibling -> is_right
-          | Is k -> k == kind
-          | Has_first_child -> has_left
-          | Has_next_sibling -> has_right
-        in
-        if is_move p && (not b) then
-          eprintf "Warning: Invalid negative atom %a" Atom.print a;
-        b == pos
-    | Formula.And(phi1, phi2) -> loop phi1 && loop phi2
-    | Formula.Or (phi1, phi2) -> loop phi1 || loop phi2
-    end
-  in
-  loop phi
-
-let int_of_conf is_left is_right has_left has_right kind =
-  ((Obj.magic kind) lsl 4) lor
-    ((Obj.magic is_left) lsl 3) lor
-    ((Obj.magic is_right) lsl 2) lor
-    ((Obj.magic has_left) lsl 1) lor
-    (Obj.magic has_right)
-
-let eval_trans auto ltrs fcs nss ps ss is_left is_right has_left has_right kind =
-  let i = int_of_conf is_left is_right has_left has_right kind
-  and k = (fcs.StateSet.id :> int)
-  and l = (nss.StateSet.id :> int)
-  and m = (ps.StateSet.id :> int)
-  in
-
-  let rec loop ltrs ss =
-    let j = (ltrs.TransList.id :> int)
-    and n = (ss.StateSet.id :> int) in
-    let (new_ltrs, new_ss) as res =
-      let res = Cache.N6.find auto.cache6 i j k l m n in
-      if res == dummy6 then
-        let res =
-          TransList.fold (fun trs (acct, accs) ->
-            let q, _, phi = Transition.node trs in
-            if StateSet.mem q accs then (acct, accs) else
-              if eval_form
-                phi fcs nss ps accs
-                is_left is_right has_left has_right kind
-              then
-                (acct, StateSet.add q accs)
-              else
-                (TransList.cons trs acct, accs)
-          ) ltrs (TransList.nil, ss)
-        in
-        Cache.N6.add auto.cache6 i j k l m n res; res
-      else
-        res
-    in
-    if new_ss == ss then res else
-      loop new_ltrs new_ss
-  in
-  loop ltrs ss
-
-
-
-
-
-(*
-  [add_trans a q labels f] adds a transition [(q,labels) -> f] to the
-  automaton [a] but ensures that transitions remains pairwise disjoint
-*)
-
-let add_trans a q s f =
-  let trs = try Hashtbl.find a.transitions q with Not_found -> [] in
-  let cup, ntrs =
-    List.fold_left (fun (acup, atrs) (labs, phi) ->
-      let lab1 = QNameSet.inter labs s in
-      let lab2 = QNameSet.diff labs s in
-      let tr1 =
-        if QNameSet.is_empty lab1 then []
-        else [ (lab1, SFormula.or_ phi f) ]
-      in
-      let tr2 =
-        if QNameSet.is_empty lab2 then []
-        else [ (lab2, SFormula.or_ phi f) ]
-      in
-      (QNameSet.union acup labs, tr1@ tr2 @ atrs)
-    ) (QNameSet.empty, []) trs
-  in
-  let rem = QNameSet.diff s cup in
-  let ntrs = if QNameSet.is_empty rem then ntrs
-    else (rem, f) :: ntrs
-  in
-  Hashtbl.replace a.transitions q ntrs
-
-let _pr_buff = Buffer.create 50
-let _str_fmt = formatter_of_buffer _pr_buff
-let _flush_str_fmt () = pp_print_flush _str_fmt ();
-  let s = Buffer.contents _pr_buff in
-  Buffer.clear _pr_buff; s
-
-let print fmt a =
-  fprintf fmt
-    "\nInternal UID: %i@\n\
-     States: %a@\n\
-     Selection states: %a@\n\
-     Alternating transitions:@\n"
-    (a.id :> int)
-    StateSet.print a.states
-    StateSet.print a.selection_states;
-  let trs =
-    Hashtbl.fold
-      (fun q t acc -> List.fold_left (fun acc (s , f) -> (q,s,f)::acc) acc t)
-      a.transitions
-      []
-  in
-  let sorted_trs = List.stable_sort (fun (q1, s1, _) (q2, s2, _) ->
-    let c = State.compare q1 q2 in - (if c == 0 then QNameSet.compare s1 s2 else c))
-    trs
-  in
-  let _ = _flush_str_fmt () in
-  let strs_strings, max_pre, max_all = List.fold_left (fun (accl, accp, acca) (q, s, f) ->
-    let s1 = State.print _str_fmt q; _flush_str_fmt () in
-    let s2 = QNameSet.print _str_fmt s;  _flush_str_fmt () in
-    let s3 = SFormula.print _str_fmt f;  _flush_str_fmt () in
-    let pre = Pretty.length s1 + Pretty.length s2 in
-    let all = Pretty.length s3 in
-    ( (q, s1, s2, s3) :: accl, max accp pre, max acca all)
-  ) ([], 0, 0) sorted_trs
-  in
-  let line = Pretty.line (max_all + max_pre + 6) in
-  let prev_q = ref State.dummy in
-  List.iter (fun (q, s1, s2, s3) ->
-    if !prev_q != q && !prev_q != State.dummy then fprintf fmt " %s\n%!"  line;
-    prev_q := q;
-    fprintf fmt " %s, %s" s1 s2;
-    fprintf fmt "%s" (Pretty.padding (max_pre - Pretty.length s1 - Pretty.length s2));
-    fprintf fmt " %s  %s@\n%!" Pretty.right_arrow s3;
-  ) strs_strings;
-  fprintf fmt " %s\n%!" line
-
-(*
-  [complete transitions a] ensures that for each state q
-  and each symbols s in the alphabet, a transition q, s exists.
-  (adding q, s -> F when necessary).
-*)
-
-let complete_transitions a =
-  StateSet.iter (fun q ->
-    let qtrans = Hashtbl.find a.transitions q in
-    let rem =
-      List.fold_left (fun rem (labels, _) ->
-        QNameSet.diff rem labels) QNameSet.any qtrans
-    in
-    let nqtrans =
-      if QNameSet.is_empty rem then qtrans
-      else
-        (rem, SFormula.false_) :: qtrans
-    in
-    Hashtbl.replace a.transitions q nqtrans
-  ) a.states
-
-let cleanup_states a =
-  let memo = ref StateSet.empty in
-  let rec loop q =
-    if not (StateSet.mem q !memo) then begin
-      memo := StateSet.add q !memo;
-      let trs = try Hashtbl.find a.transitions q with Not_found -> [] in
-      List.iter (fun (_, phi) ->
-        StateSet.iter loop (SFormula.get_states phi)) trs
-    end
-  in
-  StateSet.iter loop a.selection_states;
-  let unused = StateSet.diff a.states !memo in
-  eprintf "Unused states %a\n%!" StateSet.print unused;
-  StateSet.iter (fun q -> Hashtbl.remove a.transitions q) unused;
-  a.states <- !memo
-
-(* [normalize_negations a] removes negative atoms in the formula
-   complementing the sub-automaton in the negative states.
-   [TODO check the meaning of negative upward arrows]
-*)
-
-let normalize_negations auto =
-  eprintf "Automaton before normalize_trans:\n";
-  print err_formatter auto;
-  eprintf "--------------------\n%!";
-
-  let memo_state = Hashtbl.create 17 in
-  let todo = Queue.create () in
-  let rec flip b f =
-    match SFormula.expr f with
-      Formula.True | Formula.False -> if b then f else SFormula.not_ f
-    | Formula.Or(f1, f2) -> (if b then SFormula.or_ else SFormula.and_)(flip b f1) (flip b f2)
-    | Formula.And(f1, f2) -> (if b then SFormula.and_ else SFormula.or_)(flip b f1) (flip b f2)
-    | Formula.Atom(a) -> begin
-      let l, b', q = Atom.node a in
-      if q == State.dummy then if b then f else SFormula.not_ f
-      else
-        if b == b' then begin
-        (* a appears positively, either no negation or double negation *)
-          if not (Hashtbl.mem memo_state (q,b)) then Queue.add (q,true) todo;
-          SFormula.atom_ (Atom.make (l, true, q))
-        end else begin
-        (* need to reverse the atom
-           either we have a positive state deep below a negation
-           or we have a negative state in a positive formula
-           b' = sign of the state
-           b = sign of the enclosing formula
-        *)
-        let not_q =
-          try
-            (* does the inverted state of q exist ? *)
-            Hashtbl.find memo_state (q, false)
-          with
-            Not_found ->
-              (* create a new state and add it to the todo queue *)
-              let nq = State.make () in
-              auto.states <- StateSet.add nq auto.states;
-              Hashtbl.add memo_state (q, false) nq;
-              Queue.add (q, false) todo; nq
-        in
-        SFormula.atom_ (Atom.make (l, true, not_q))
-      end
-    end
-  in
-  (* states that are not reachable from a selection stat are not interesting *)
-  StateSet.iter (fun q -> Queue.add (q, true) todo) auto.selection_states;
-
-  while not (Queue.is_empty todo) do
-    let (q, b) as key = Queue.pop todo in
-    let q' =
-      try
-        Hashtbl.find memo_state key
-      with
-        Not_found ->
-          let nq = if b then q else
-              let nq = State.make () in
-              auto.states <- StateSet.add nq auto.states;
-              nq
-          in
-          Hashtbl.add memo_state key nq; nq
-    in
-    let trans = Hashtbl.find auto.transitions q in
-    let trans' = List.map (fun (lab, f) -> lab, flip b f) trans in
-    Hashtbl.replace auto.transitions q' trans';
-  done;
-  cleanup_states auto
-
-
diff --git a/src/auto/ata.mli b/src/auto/ata.mli
deleted file mode 100644
index 0ca6e55..0000000
--- a/src/auto/ata.mli
+++ /dev/null
@@ -1,93 +0,0 @@
-(***********************************************************************)
-(*                                                                     *)
-(*                               TAToo                                 *)
-(*                                                                     *)
-(*                     Kim Nguyen, LRI UMR8623                         *)
-(*                   Université Paris-Sud & CNRS                       *)
-(*                                                                     *)
-(*  Copyright 2010-2013 Université Paris-Sud and Centre National de la *)
-(*  Recherche Scientifique. All rights reserved.  This file is         *)
-(*  distributed under the terms of the GNU Lesser General Public       *)
-(*  License, with the special exception on linking described in file   *)
-(*  ../LICENSE.                                                        *)
-(*                                                                     *)
-(***********************************************************************)
-
-(*
-  Time-stamp: <Last modified on 2013-03-15 18:18:23 CET by Kim Nguyen>
-*)
-
-type predicate =
-    First_child
-  | Next_sibling
-  | Parent
-  | Previous_sibling
-  | Stay
-  | Is_first_child
-  | Is_next_sibling
-  | Is of Tree.Common.NodeKind.t
-  | Has_first_child
-  | Has_next_sibling
-
-val is_move : predicate -> bool
-
-type atom = predicate * bool * State.t
-
-module Atom : Formula.ATOM with type data = atom
-
-module SFormula :
-  sig
-    include module type of Formula.Make(Atom)
-    val mk_atom : predicate -> bool -> State.t -> t
-    val mk_kind : Tree.Common.NodeKind.t -> t
-    val has_first_child : t
-    val has_next_sibling : t
-    val is_first_child : t
-    val is_next_sibling : t
-    val is_attribute : t
-    val is_element : t
-    val is_processing_instruction : t
-    val is_comment : t
-    val first_child : State.t -> t
-    val next_sibling : State.t -> t
-    val parent : State.t -> t
-    val previous_sibling : State.t -> t
-    val stay : State.t -> t
-    val get_states : t -> StateSet.t
-  end
-
-
-module Transition : Utils.Hcons.S with
-            type data = State.t * Utils.QNameSet.t * SFormula.t
-
-module TransList : sig
-  include Utils.Hlist.S with type elt = Transition.t
-  val print : Format.formatter -> ?sep:string -> t -> unit
-end
-
-
-type t = private {
-  id : Utils.Uid.t;
-  mutable states : StateSet.t;
-  mutable selection_states: StateSet.t;
-  transitions: (State.t, (Utils.QNameSet.t*SFormula.t) list) Hashtbl.t;
-  mutable cache2 : TransList.t Utils.Cache.N2.t;
-  mutable cache6 : (TransList.t*StateSet.t) Utils.Cache.N6.t;
-}
-
-
-
-val create : StateSet.t -> StateSet.t -> t
-val reset : t -> unit
-val get_trans : t -> Utils.QNameSet.elt -> StateSet.t -> TransList.t
-
-val eval_trans : t -> TransList.t
-  -> StateSet.t -> StateSet.t -> StateSet.t -> StateSet.t
-  -> bool -> bool -> bool -> bool -> Tree.Common.NodeKind.t
-  -> TransList.t*StateSet.t
-
-val add_trans : t -> State.t -> Utils.QNameSet.t -> SFormula.t -> unit
-val print : Format.formatter -> t -> unit
-val complete_transitions : t -> unit
-val cleanup_states : t -> unit
-val normalize_negations : t -> unit
diff --git a/src/auto/eval.ml b/src/auto/eval.ml
deleted file mode 100644
index 4a27fa5..0000000
--- a/src/auto/eval.ml
+++ /dev/null
@@ -1,132 +0,0 @@
-(***********************************************************************)
-(*                                                                     *)
-(*                               TAToo                                 *)
-(*                                                                     *)
-(*                     Kim Nguyen, LRI UMR8623                         *)
-(*                   Université Paris-Sud & CNRS                       *)
-(*                                                                     *)
-(*  Copyright 2010-2013 Université Paris-Sud and Centre National de la *)
-(*  Recherche Scientifique. All rights reserved.  This file is         *)
-(*  distributed under the terms of the GNU Lesser General Public       *)
-(*  License, with the special exception on linking described in file   *)
-(*  ../LICENSE.                                                        *)
-(*                                                                     *)
-(***********************************************************************)
-
-(*
-  Time-stamp: <Last modified on 2013-03-15 18:32:22 CET by Kim Nguyen>
-*)
-
-INCLUDE "utils.ml"
-open Format
-open Utils
-
-module Make (T : Tree.Sig.S) :
-  sig
-    val eval : Ata.t -> T.t -> T.node -> T.node list
-  end
- = struct
-
-
-IFDEF HTMLTRACE
-  THEN
-DEFINE TRACE(e) = (e)
-  ELSE
-DEFINE TRACE(e) = ()
-END
-
-
-
-  type cache = StateSet.t Cache.N1.t
-  let get c t n = Cache.N1.find c (T.preorder t n)
-
-  let set c t n v = Cache.N1.add c (T.preorder t n) v
-
-
-  let top_down_run auto tree node cache _i =
-    let redo = ref false in
-    let rec loop node =
-      if node != T.nil then begin
-        let parent = T.parent tree node in
-        let fc = T.first_child tree node in
-        let ns = T.next_sibling tree node in
-        let tag = T.tag tree node in
-        let states0 = get cache tree node in
-        let trans0 = Ata.get_trans auto tag auto.Ata.states in
-        let () =
-          TRACE(Html.trace (T.preorder tree node) _i "Pre States: %a<br/>Pre Trans: %a<br/>"
-                  StateSet.print states0 (Ata.TransList.print ~sep:"<br/>") trans0)
-        in
-        let ps = get cache tree parent in
-        let fcs = get cache tree fc in
-        let nss = get cache tree ns in
-        let is_left = node == T.first_child tree parent
-        and is_right = node == T.next_sibling tree parent
-        and has_left = fc != T.nil
-        and has_right = ns != T.nil
-        and kind = T.kind tree node
-        in
-        let trans1, states1 =
-          Ata.eval_trans auto trans0
-            fcs nss ps states0
-            is_left is_right has_left has_right kind
-        in
-        let () =
-          TRACE(Html.trace (T.preorder tree node) _i "TD States: %a<br/>TD Trans: %a<br/>" StateSet.print states1 (Ata.TransList.print ~sep:"<br/>") trans1)
-        in
-        if states1 != states0 then set cache tree node states1;
-        let () = loop fc in
-        let fcs1 = get cache tree fc in
-        let trans2, states2 =
-          Ata.eval_trans auto trans1
-            fcs1 nss ps states1
-            is_left is_right has_left has_right kind
-        in
-        let () =
-          TRACE(Html.trace (T.preorder tree node) _i "Left BU States: %a<br/>Left BU Trans: %a<br/>" StateSet.print states2 (Ata.TransList.print ~sep:"<br/>") trans2)
-        in
-        if states2 != states1 then set cache tree node states2;
-        let () = loop ns in
-        let _trans3, states3 =
-          Ata.eval_trans auto trans2
-            fcs1 (get cache tree ns) ps states2
-            is_left is_right has_left has_right kind
-        in
-        let () =
-          TRACE(Html.trace (T.preorder tree node) _i "Right BU States: %a<br/>Right BU Trans: %a<br/>" StateSet.print states3 (Ata.TransList.print ~sep:"<br/>") _trans3)
-        in
-        if states3 != states2 then set cache tree node states3;
-        if states0 != states3 && (not !redo) then redo := true
-      end
-    in
-    loop node;
-    !redo
-
-  let get_results auto tree node cache =
-    let rec loop node acc =
-      if node == T.nil then acc
-      else
-        let acc0 = loop (T.next_sibling tree node) acc in
-        let acc1 = loop (T.first_child tree node) acc0 in
-
-        if StateSet.intersect (get cache tree node) auto.Ata.selection_states then
-          node::acc1
-        else
-          acc1
-    in
-    loop node []
-
-  let eval auto tree node =
-    let cache = Cache.N1.create StateSet.empty in
-    let redo = ref true in
-    let iter = ref 0 in
-    Ata.reset auto;
-    while !redo do
-      redo := top_down_run auto tree node cache !iter;
-      incr iter;
-    done;
-    let r = get_results auto tree node cache in
-    TRACE(Html.gen_trace (module T : Tree.Sig.S with type t = T.t) (tree));
-    r
-
-end
diff --git a/src/auto/formula.ml b/src/auto/formula.ml
deleted file mode 100644
index 097114e..0000000
--- a/src/auto/formula.ml
+++ /dev/null
@@ -1,182 +0,0 @@
-(***********************************************************************)
-(*                                                                     *)
-(*                               TAToo                                 *)
-(*                                                                     *)
-(*                     Kim Nguyen, LRI UMR8623                         *)
-(*                   Université Paris-Sud & CNRS                       *)
-(*                                                                     *)
-(*  Copyright 2010-2013 Université Paris-Sud and Centre National de la *)
-(*  Recherche Scientifique. All rights reserved.  This file is         *)
-(*  distributed under the terms of the GNU Lesser General Public       *)
-(*  License, with the special exception on linking described in file   *)
-(*  ../LICENSE.                                                        *)
-(*                                                                     *)
-(***********************************************************************)
-
-(*
-  Time-stamp: <Last modified on 2013-03-09 11:16:29 CET by Kim Nguyen>
-*)
-
-INCLUDE "utils.ml"
-
-open Format
-open Utils
-
-(*
-
-(** Implementation of hashconsed Boolean formulae *)
-
-*)
-module type ATOM =
-sig
-  type t
-  val neg : t -> t
-  include Hcons.Abstract with type t := t
-  include Common_sig.Printable with type t := t
-end
-
-type ('formula,'atom) expr =
-  | False
-  | True
-  | Or of 'formula * 'formula
-  | And of 'formula * 'formula
-  | Atom of 'atom
-
-module Make (P: ATOM) =
-struct
-
-
-  type 'hcons node = {
-    pos : ('hcons,P.t) expr;
-    mutable neg : 'hcons;
-  }
-
-  external hash_const_variant : [> ] -> int = "%identity"
-  external vb : bool -> int = "%identity"
-
-  module rec Node : Hcons.S
-    with type data = Data.t = Hcons.Make (Data)
-    and Data : Common_sig.HashedType  with type t = Node.t node =
-  struct
-    type t =  Node.t node
-    let equal x y =
-      match x.pos, y.pos with
-      | a,b when a == b -> true
-      | Or(xf1, xf2), Or(yf1, yf2)
-      | And(xf1, xf2), And(yf1,yf2)  -> xf1 == yf1 && xf2 == yf2
-      | Atom(p1), Atom(p2) -> p1 == p2
-      | _ -> false
-
-    let hash f =
-      match f.pos with
-      | False -> 0
-      | True -> 1
-      | Or (f1, f2) ->
-          HASHINT3 (PRIME1, Uid.to_int f1.Node.id, Uid.to_int f2.Node.id)
-      | And (f1, f2) ->
-          HASHINT3(PRIME3, Uid.to_int f1.Node.id, Uid.to_int f2.Node.id)
-      | Atom(p) -> HASHINT2(PRIME5, Uid.to_int (P.uid p))
-  end
-
-    type t = Node.t
-    let hash x = x.Node.hash
-    let uid x = x.Node.id
-    let equal = Node.equal
-    let expr f = f.Node.node.pos
-
-    let compare f1 f2 = compare f1.Node.id  f2.Node.id
-    let prio f =
-      match expr f with
-      | True | False -> 10
-      | Atom _ -> 8
-      | And _ -> 6
-      | Or _ -> 1
-
-    let rec print ?(parent=false) ppf f =
-      if parent then fprintf ppf "(";
-      let _ = match expr f with
-      | True -> fprintf ppf "%s" Pretty.top
-      | False -> fprintf ppf "%s" Pretty.bottom
-      | And(f1,f2) ->
-          print ~parent:(prio f > prio f1) ppf f1;
-          fprintf ppf " %s "  Pretty.wedge;
-          print ~parent:(prio f > prio f2) ppf f2;
-      | Or(f1,f2) ->
-          (print ppf f1);
-          fprintf ppf " %s " Pretty.vee;
-          (print ppf f2);
-      | Atom(p) -> fprintf ppf "%a" P.print p
-(*          let _ = flush_str_formatter() in
-          let fmt = str_formatter in
-          let a_str, d_str =
-          match  dir with
-          | `Left ->  Pretty.down_arrow, Pretty.subscript 1
-          | `Right -> Pretty.down_arrow, Pretty.subscript 2
-          | `Epsilon -> Pretty.epsilon, ""
-          | `Up1 -> Pretty.up_arrow, Pretty.subscript 1
-          | `Up2 -> Pretty.up_arrow, Pretty.subscript 2
-        in
-        fprintf fmt "%s%s" a_str d_str;
-        State.print fmt s;
-        let str = flush_str_formatter() in
-        if b then fprintf ppf "%s" str
-        else Pretty.pp_overline ppf str *)
-  in
-    if parent then fprintf ppf ")"
-
-let print ppf f =  print ~parent:false ppf f
-
-let is_true f = (expr f) == True
-let is_false f = (expr f) == False
-
-
-let cons pos neg =
-  let nnode = Node.make { pos = neg; neg = Obj.magic 0 } in
-  let pnode = Node.make { pos = pos; neg = nnode } in
-    (Node.node nnode).neg <- pnode; (* works because the neg field isn't taken into
-                                       account for hashing ! *)
-    pnode,nnode
-
-
-let true_,false_ = cons True False
-
-let atom_ p = fst (cons (Atom(p)) (Atom(P.neg p)))
-
-let not_ f = f.Node.node.neg
-
-let order f1 f2 = if uid f1 < uid f2 then f2,f1 else f1,f2
-
-let or_ f1 f2 =
-  (* Tautologies: x|x, x|not(x) *)
-
-  if equal f1 f2 then f1
-  else if equal f1 (not_ f2) then true_
-
-  (* simplification *)
-  else if is_true f1 || is_true f2 then true_
-  else if is_false f1 && is_false f2 then false_
-  else if is_false f1 then f2
-  else if is_false f2 then f1
-
-  (* commutativity of | *)
-  else
-    let f1, f2 = order f1 f2 in
-      fst (cons (Or(f1,f2)) (And(not_ f1, not_ f2)))
-
-
-let and_ f1 f2 =
-  not_ (or_ (not_ f1) (not_ f2))
-
-
-let of_bool = function true -> true_ | false -> false_
-
-let fold f phi acc =
-  let rec loop phi acc =
-    match expr phi with
-    | And (phi1, phi2) | Or(phi1, phi2)  ->
-        loop phi2 (loop phi1 (f phi acc))
-    | _ -> f phi acc
-  in
-  loop phi acc
-
-end
diff --git a/src/auto/formula.mli b/src/auto/formula.mli
deleted file mode 100644
index d708c2d..0000000
--- a/src/auto/formula.mli
+++ /dev/null
@@ -1,90 +0,0 @@
-(***********************************************************************)
-(*                                                                     *)
-(*                               TAToo                                 *)
-(*                                                                     *)
-(*                     Kim Nguyen, LRI UMR8623                         *)
-(*                   Université Paris-Sud & CNRS                       *)
-(*                                                                     *)
-(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(*  Recherche Scientifique. All rights reserved.  This file is         *)
-(*  distributed under the terms of the GNU Lesser General Public       *)
-(*  License, with the special exception on linking described in file   *)
-(*  ../LICENSE.                                                        *)
-(*                                                                     *)
-(***********************************************************************)
-
-(*
-  Time-stamp: <Last modified on 2013-03-09 11:16:45 CET by Kim Nguyen>
-*)
-
-module type ATOM =
-sig
-  type t
-  val neg : t -> t
-  include Utils.Hcons.Abstract with type t := t
-  include Utils.Common_sig.Printable with type t := t
-end
-
-type ('formula,'atom) expr =
-  | False
-  | True
-  | Or of 'formula * 'formula
-  | And of 'formula * 'formula
-  | Atom of 'atom
-
-(** View of the internal representation of a formula,
-    used for pattern matching *)
-
-module Make(P : ATOM) :
-sig
-  type t
-
-  (** Abstract type representing hashconsed formulae *)
-
-  val hash : t -> int
-  (** Hash function for formulae *)
-
-  val uid : t -> Utils.Uid.t
-  (** Returns a unique ID for formulae *)
-
-  val equal : t -> t -> bool
-  (** Equality over formulae *)
-
-  val expr : t -> (t,P.t) expr
-  (** Return a view of the formulae *)
-
-  val compare : t -> t -> int
-  (** Comparison of formulae *)
-
-  val print : Format.formatter -> t -> unit
-  (** Pretty printer *)
-
-  val is_true : t -> bool
-  (** [is_true f] tests whether the formula is the atom True *)
-
-  val is_false : t -> bool
-  (** [is_false f] tests whether the formula is the atom False *)
-
-  val true_ : t
-  (** Atom True *)
-
-  val false_ : t
-  (** Atom False *)
-
-  val atom_ : P.t -> t
-  (** [atom_ dir b q] creates a down_left or down_right atom for state
-      [q]. The atom is positive if [b == true].
-  *)
-
-  val not_ : t -> t
-  val or_ : t -> t -> t
-  val and_ : t -> t -> t
-  (** Boolean connective *)
-
-  val of_bool : bool -> t
-  (** Convert an ocaml Boolean value to a formula *)
-
-  val fold : (t -> 'a -> 'a) -> t -> 'a -> 'a
-  (** [fold f phi acc] folds [f] over the formula structure *)
-
-end
diff --git a/src/auto/html.ml b/src/auto/html.ml
deleted file mode 100644
index 6c45c93..0000000
--- a/src/auto/html.ml
+++ /dev/null
@@ -1,92 +0,0 @@
-open Format
-module M = Map.Make(struct type t = int let compare = compare end)
-
-let info = Hashtbl.create 2017
-
-
-let add_info (nodeid:int) (i:int) s =
-  let m = try Hashtbl.find info nodeid with Not_found -> M.empty in
-  let old_s = try M.find i m with Not_found -> "" in
-  let s' = old_s ^ s in
-  let m' = M.add i s' m in
-  Hashtbl.replace info nodeid m'
-
-let buff = Buffer.create 20
-let fmt = formatter_of_buffer buff
-
-let trace nodeid i =
-  let () = pp_print_flush fmt ();
-    Buffer.clear buff
-  in
-  kfprintf (fun fmt ->
-    pp_print_flush fmt ();
-    let s = Buffer.contents buff in
-    add_info nodeid i s) fmt
-
-
-let gen_trace (type s)  = (); fun t tree ->
-  let module T = (val (t) : Tree.Sig.S with type t = s) in
-  let rec loop odot ohtml node parent =
-    if node == T.nil then () else begin
-      let s_node = "node" ^ (string_of_int (T.preorder tree node)) in
-      fprintf odot "%s[ id=\"%s\" label=\"%s\"];\n"
-        s_node s_node (Utils.QName.to_string (T.tag tree node));
-      let m =
-        try
-          Hashtbl.find info (T.preorder tree node)
-        with Not_found -> M.empty
-      in
-      fprintf ohtml "data['%s'] = new Array();\n" s_node;
-      M.iter
-        (fun i s -> fprintf ohtml "data['%s'][%i] = '%s';\n" s_node i s)
-        m;
-      if parent != T.nil then
-        fprintf odot "node%i -> %s;\n"
-          (T.preorder tree parent) s_node;
-      loop odot ohtml (T.first_child tree node) node;
-      loop odot ohtml (T.next_sibling tree node) parent
-    end
-  in
-  ignore (Sys.command "mkdir -p tests/trace");
-  let odot_ = open_out "tests/trace/trace.dot" in
-  let ohtml_ = open_out "tests/trace/trace.html" in
-  let odot = formatter_of_out_channel odot_ in
-  let ohtml = formatter_of_out_channel ohtml_ in
-  fprintf odot "digraph G {\n node[shape=box, style=filled, fillcolor=white];splines=false;";
-  fprintf ohtml "<html>\
-<head><title></title>
-<link rel='stylesheet' type='text/css' href='trace.css' />\
-<meta http-equiv='content-type' content='text/html;charset=utf-8'/>\
-</head>\
-<body>\
-<div id='data' > </div>\
-<script type='text/javascript'>";
-  loop odot ohtml (T.root tree) (T.nil);
-  fprintf odot "\n}\n%!";
-  pp_print_flush odot ();
-  close_out odot_;
-  ignore (Sys.command "dot -o tests/trace/trace.svg -Tsvg tests/trace/trace.dot");
-  ignore (Sys.command "./tools/add_onclick.sh tests/trace/trace.svg > tests/trace/trace2.svg");
-  fprintf ohtml "var activate = function (id) {\
-  var d = document.getElementById('data');
-  var msg = '';
-  for (i=0; i < data[id].length; i++)
-     msg += ('<p>' + i + ':') + data[id][i] + '</p>\\n';
-  d.innerHTML = msg;
-  return;
-  };\n";
-
-  fprintf ohtml "</script>\n<div id='svg'>\n";
-  let fi = open_in "tests/trace/trace2.svg" in
-  try
-    while true do
-      let s = input_line fi in
-      fprintf ohtml "%s\n" s;
-    done
-  with
-    End_of_file ->
-      fprintf ohtml "</div></body></html>\n%!";
-      pp_print_flush ohtml ();
-      close_out ohtml_;
-      close_in fi
-
diff --git a/src/auto/html.mli b/src/auto/html.mli
deleted file mode 100644
index 0a7d8dd..0000000
--- a/src/auto/html.mli
+++ /dev/null
@@ -1,2 +0,0 @@
-val trace : int -> int -> ('a, Format.formatter, unit, unit) format4 -> 'a
-val gen_trace : (module Tree.Sig.S with type t = 'a) -> 'a -> unit
diff --git a/src/auto/state.ml b/src/auto/state.ml
deleted file mode 100644
index 83ad4b4..0000000
--- a/src/auto/state.ml
+++ /dev/null
@@ -1,41 +0,0 @@
-(***********************************************************************)
-(*                                                                     *)
-(*                               TAToo                                 *)
-(*                                                                     *)
-(*                     Kim Nguyen, LRI UMR8623                         *)
-(*                   Université Paris-Sud & CNRS                       *)
-(*                                                                     *)
-(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(*  Recherche Scientifique. All rights reserved.  This file is         *)
-(*  distributed under the terms of the GNU Lesser General Public       *)
-(*  License, with the special exception on linking described in file   *)
-(*  ../LICENSE.                                                        *)
-(*                                                                     *)
-(***********************************************************************)
-
-(*
-  Time-stamp: <Last modified on 2013-02-07 10:03:52 CET by Kim Nguyen>
-*)
-
-open Format
-open Utils
-
-type t = int
-let make =
-  let id = ref ~-1 in
-    fun () -> incr id; !id
-
-let compare = (-)
-
-let equal = (==)
-
-external hash : t -> int =  "%identity"
-
-let print fmt x = fprintf fmt "q%a" Pretty.pp_subscript x
-
-let dump fmt x = print fmt x
-
-let check x =
-  if x < 0 then failwith (Printf.sprintf "State: Assertion %i < 0 failed" x)
-
-let dummy = max_int
diff --git a/src/auto/state.mli b/src/auto/state.mli
deleted file mode 100644
index 89d67cd..0000000
--- a/src/auto/state.mli
+++ /dev/null
@@ -1,31 +0,0 @@
-(***********************************************************************)
-(*                                                                     *)
-(*                               TAToo                                 *)
-(*                                                                     *)
-(*                     Kim Nguyen, LRI UMR8623                         *)
-(*                   Université Paris-Sud & CNRS                       *)
-(*                                                                     *)
-(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(*  Recherche Scientifique. All rights reserved.  This file is         *)
-(*  distributed under the terms of the GNU Lesser General Public       *)
-(*  License, with the special exception on linking described in file   *)
-(*  ../LICENSE.                                                        *)
-(*                                                                     *)
-(***********************************************************************)
-
-(*
-  Time-stamp: <Last modified on 2013-03-04 23:02:21 CET by Kim Nguyen>
-*)
-
-(** Implementation of states *)
-
-include Common_sig.Type with type t = int
-
-val make : unit -> t
-(** Generate a fresh state *)
-
-val dummy : t
-(** Dummy state that can never be returned by [make ()] *)
-
-val print : Format.formatter -> t -> unit
-(** Pretty printer *)
diff --git a/src/auto/stateSet.ml b/src/auto/stateSet.ml
deleted file mode 100644
index e99cd5e..0000000
--- a/src/auto/stateSet.ml
+++ /dev/null
@@ -1,27 +0,0 @@
-(***********************************************************************)
-(*                                                                     *)
-(*                               TAToo                                 *)
-(*                                                                     *)
-(*                     Kim Nguyen, LRI UMR8623                         *)
-(*                   Université Paris-Sud & CNRS                       *)
-(*                                                                     *)
-(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(*  Recherche Scientifique. All rights reserved.  This file is         *)
-(*  distributed under the terms of the GNU Lesser General Public       *)
-(*  License, with the special exception on linking described in file   *)
-(*  ../LICENSE.                                                        *)
-(*                                                                     *)
-(***********************************************************************)
-
-(*
-  Time-stamp: <Last modified on 2013-02-07 09:57:17 CET by Kim Nguyen>
-*)
-
-open Format
-open Utils
-
-include Ptset.Make (Hcons.PosInt)
-
-let print ppf s =
-  fprintf ppf "{ %a }"
-    (Pretty.print_list ~sep:" " (State.print)) (elements s)
diff --git a/src/auto/stateSet.mli b/src/auto/stateSet.mli
deleted file mode 100644
index 96b5b6d..0000000
--- a/src/auto/stateSet.mli
+++ /dev/null
@@ -1,24 +0,0 @@
-(***********************************************************************)
-(*                                                                     *)
-(*                               TAToo                                 *)
-(*                                                                     *)
-(*                     Kim Nguyen, LRI UMR8623                         *)
-(*                   Université Paris-Sud & CNRS                       *)
-(*                                                                     *)
-(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(*  Recherche Scientifique. All rights reserved.  This file is         *)
-(*  distributed under the terms of the GNU Lesser General Public       *)
-(*  License, with the special exception on linking described in file   *)
-(*  ../LICENSE.                                                        *)
-(*                                                                     *)
-(***********************************************************************)
-
-(*
-  Time-stamp: <Last modified on 2013-02-07 09:57:11 CET by Kim Nguyen>
-*)
-
-(** Implementation of sets of states *)
-include Utils.Ptset.S with type elt = int
-
-val print : Format.formatter -> t -> unit
-(** Pretty printer *)
diff --git a/src/cache.ml b/src/cache.ml
new file mode 100644
index 0000000..abd999e
--- /dev/null
+++ b/src/cache.ml
@@ -0,0 +1,253 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                               TAToo                                 *)
+(*                                                                     *)
+(*                     Kim Nguyen, LRI UMR8623                         *)
+(*                   Université Paris-Sud & CNRS                       *)
+(*                                                                     *)
+(*  Copyright 2010-2013 Université Paris-Sud and Centre National de la *)
+(*  Recherche Scientifique. All rights reserved.  This file is         *)
+(*  distributed under the terms of the GNU Lesser General Public       *)
+(*  License, with the special exception on linking described in file   *)
+(*  ../LICENSE.                                                        *)
+(*                                                                     *)
+(***********************************************************************)
+
+(*
+  Time-stamp: <Last modified on 2013-03-14 14:50:18 CET by Kim Nguyen>
+*)
+
+let realloc l old_size new_size dummy =
+  let l' = Array.create new_size dummy in
+  for i = 0 to (min old_size new_size) - 1 do
+    Array.unsafe_set l' i  (Array.unsafe_get l i);
+  done;
+  l'
+
+module N1 =
+struct
+  type 'a t = { mutable line : 'a array;
+		dummy : 'a;
+		mutable offset : int;
+	      }
+  let create a = {
+    line = Array.create 0 a;
+    dummy = a;
+    offset = ~-1;
+
+  }
+
+  let print fmt a =
+    Format.fprintf fmt "{ offset=%i;\n dummy=_;line=%a \n}\n%!"
+      a.offset
+      (Pretty.print_array ~sep:", " (fun fmt x ->
+	if x==a.dummy then
+	  Format.fprintf fmt "%s" "D"
+	else
+	  Format.fprintf fmt "%s" "E")) a.line
+
+  let add a i v =
+    if a.offset == ~-1 then a.offset <- i;
+    let offset = a.offset in
+    let len = Array.length a.line in
+    if i >= offset && i < offset + len then
+      a.line.(i - offset) <- v
+    else
+      if i < offset then begin (* bottom resize *)
+	let pad = offset - i in
+	let nlen = len + pad in
+	let narray = Array.create nlen a.dummy in
+	for j = 0 to len - 1 do
+	  narray.(j+pad) <- a.line.(j)
+	done;
+	a.offset <- i;
+	a.line <- narray;
+	narray.(0) <- v;
+      end else begin (* top resize *)
+	(* preventively allocate the space for the following elements *)
+	let nlen = ((i - offset + 1) lsl 1) + 1 in
+	let narray = Array.create nlen a.dummy in
+	for j = 0 to len - 1 do
+	  narray.(j) <- a.line.(j);
+	done;
+	narray.(i - offset) <- v;
+	a.line <- narray
+      end
+
+  let find a i =
+    let idx = i - a.offset in
+    let len = Array.length a.line in
+    if idx >= 0 && idx < len then
+      Array.unsafe_get a.line idx
+    else a.dummy
+
+  let dummy a = a.dummy
+
+  let iteri f a =
+    let line = a.line in
+    if a.offset == ~-1 then () else
+      for i = 0 to Array.length line - 1 do
+	let v = line.(i) in
+	  f (i+a.offset) v (v==a.dummy)
+      done
+
+
+end
+
+module N2 =
+struct
+  type 'a t = 'a N1.t N1.t
+  let create a =
+    let dummy1 = N1.create a in
+    N1.create dummy1
+
+  let add a i j v =
+    let line = N1.find a i in
+    if line == a.N1.dummy then
+      let nline = N1.create line.N1.dummy in
+      N1.add a i nline;
+      N1.add nline j v
+    else
+      N1.add line j v
+
+
+  let find a i j =
+    let v = N1.find a i in
+    if v == a.N1.dummy then v.N1.dummy
+    else N1.find v j
+
+
+  let dummy c = c.N1.dummy.N1.dummy
+
+  let iteri f a =
+    let line = a.N1.line in
+    if a.N1.offset == ~-1 then () else
+      for i = 0 to Array.length line - 1 do
+	N1.iteri (f i) line.(i)
+      done
+
+
+end
+
+module N3 =
+struct
+  type 'a t = 'a N2.t N1.t
+
+  let create a =
+    let dummy2 = N2.create a in
+    N1.create dummy2
+
+  let add a i j k v =
+    let line = N1.find a i in
+    if line == a.N1.dummy then
+      let nline =  N1.create line.N1.dummy in
+      N1.add a i nline;
+      N2.add nline j k v
+    else
+      N2.add line j k v
+
+  let find a i j k =
+    let v = N1.find a i in
+    if v == a.N1.dummy then N2.dummy v
+    else N2.find v j k
+
+
+  let dummy a = N2.dummy a.N1.dummy
+  let iteri f a =
+    let line = a.N1.line in
+    if a.N1.offset == ~-1 then () else
+      for i = 0 to Array.length line - 1 do
+	N2.iteri (f i) line.(i)
+      done
+
+end
+
+module N4 =
+struct
+  type 'a t = 'a N3.t N1.t
+
+  let create a =
+  let dummy3 = N3.create a in
+  N1.create dummy3
+
+  let add a i j k l v =
+    let line = N1.find a i in
+    if line == N1.dummy a then
+      let nline =  N3.create (N3.dummy line) in
+      N1.add a i nline;
+      N3.add nline j k l v
+    else
+      N3.add line j k l v
+
+  let find a i j k l =
+    let v = N1.find a i in
+    if v == (N1.dummy a) then N3.dummy v
+    else N3.find v j k l
+
+
+  let dummy a = N3.dummy (N1.dummy a)
+  let iteri f a =
+    N1.iteri (fun i v _ ->
+      N3.iteri (fun j k l v2 b -> f i j k l v2 b) v ) a
+
+end
+
+module N5 =
+struct
+  type 'a t = 'a N4.t N1.t
+
+  let create a =
+    let dummy4 = N4.create a in
+    N1.create dummy4
+
+  let add a i j k l m v =
+    let line = N1.find a i in
+    if line == (N1.dummy a) then
+      let nline =  N4.create (N4.dummy line) in
+      N1.add a i nline;
+      N4.add nline j k l m v
+    else
+      N4.add line j k l m v
+
+  let find a i j k l m =
+    let v = N1.find a i in
+    if v == (N1.dummy a) then N4.dummy v
+    else N4.find v j k l m
+
+
+  let dummy a = N4.dummy (N1.dummy a)
+  let iteri f a =
+    N1.iteri (fun i v _ ->
+      N4.iteri (fun j k l m v2 b -> f i j k l m v2 b) v
+    ) a
+end
+
+module N6 =
+struct
+  type 'a t = 'a N5.t N1.t
+
+  let create a =
+    let dummy5 = N5.create a in
+    N1.create dummy5
+
+  let add a i j k l m n v =
+    let line = N1.find a i in
+    if line == N1.dummy a then
+      let nline =  N5.create (N5.dummy line) in
+      N1.add a i nline;
+      N5.add nline j k l m n v
+    else
+      N5.add line j k l m n v
+
+  let find a i j k l m n =
+    let v = N1.find a i in
+    if v == N1.dummy a then N5.dummy v
+    else N5.find v j k l m n
+
+
+  let dummy a = N5.dummy (N1.dummy a)
+  let iteri f a =
+    N1.iteri (fun i v _  ->
+      N5.iteri (fun j k l m n v2 b -> f i j k l m n v2 b) v
+    ) a
+end
diff --git a/src/cache.mli b/src/cache.mli
new file mode 100644
index 0000000..1211935
--- /dev/null
+++ b/src/cache.mli
@@ -0,0 +1,81 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                               TAToo                                 *)
+(*                                                                     *)
+(*                     Kim Nguyen, LRI UMR8623                         *)
+(*                   Université Paris-Sud & CNRS                       *)
+(*                                                                     *)
+(*  Copyright 2010-2013 Université Paris-Sud and Centre National de la *)
+(*  Recherche Scientifique. All rights reserved.  This file is         *)
+(*  distributed under the terms of the GNU Lesser General Public       *)
+(*  License, with the special exception on linking described in file   *)
+(*  ../LICENSE.                                                        *)
+(*                                                                     *)
+(***********************************************************************)
+
+(*
+  Time-stamp: <Last modified on 2013-03-14 13:42:53 CET by Kim Nguyen>
+*)
+
+(** N-dimentional caches *)
+
+module N1 :
+sig
+
+  type 'a t
+  val create : 'a -> 'a t
+  val find : 'a t -> int -> 'a
+  val add : 'a t -> int -> 'a -> unit
+  val dummy : 'a t -> 'a
+  val iteri : (int -> 'a -> bool -> unit) -> 'a t -> unit
+end
+
+module N2:
+sig
+    type 'a t
+    val create : 'a -> 'a t
+    val find : 'a t -> int -> int -> 'a
+    val add : 'a t -> int -> int -> 'a -> unit
+    val dummy : 'a t -> 'a
+    val iteri : (int -> int -> 'a -> bool -> unit) -> 'a t -> unit
+end
+
+module N3 :
+  sig
+    type 'a t
+    val create : 'a -> 'a t
+    val find : 'a t -> int -> int -> int -> 'a
+    val add : 'a t -> int -> int -> int -> 'a -> unit
+    val dummy : 'a t -> 'a
+    val iteri : (int -> int -> int -> 'a -> bool -> unit) -> 'a t -> unit
+  end
+
+module N4 :
+  sig
+    type 'a t
+    val create : 'a -> 'a t
+    val find : 'a t -> int -> int -> int -> int -> 'a
+    val add : 'a t -> int -> int -> int -> int -> 'a -> unit
+    val dummy : 'a t -> 'a
+    val iteri : (int -> int -> int -> int -> 'a -> bool -> unit) -> 'a t -> unit
+  end
+
+module N5 :
+  sig
+    type 'a t
+    val create : 'a -> 'a t
+    val find : 'a t -> int -> int -> int -> int -> int -> 'a
+    val add : 'a t -> int -> int -> int -> int -> int -> 'a -> unit
+    val dummy : 'a t -> 'a
+    val iteri : (int -> int -> int -> int -> int -> 'a -> bool -> unit) -> 'a t -> unit
+  end
+
+module N6 :
+  sig
+    type 'a t
+    val create : 'a -> 'a t
+    val find : 'a t -> int -> int -> int -> int -> int -> int -> 'a
+    val add : 'a t -> int -> int -> int -> int -> int -> int -> 'a -> unit
+    val dummy : 'a t -> 'a
+    val iteri : (int -> int -> int -> int -> int -> int -> 'a -> bool -> unit) -> 'a t -> unit
+  end
diff --git a/src/common_sig.ml b/src/common_sig.ml
new file mode 100644
index 0000000..37437e4
--- /dev/null
+++ b/src/common_sig.ml
@@ -0,0 +1,108 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                               TAToo                                 *)
+(*                                                                     *)
+(*                     Kim Nguyen, LRI UMR8623                         *)
+(*                   Université Paris-Sud & CNRS                       *)
+(*                                                                     *)
+(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(*  Recherche Scientifique. All rights reserved.  This file is         *)
+(*  distributed under the terms of the GNU Lesser General Public       *)
+(*  License, with the special exception on linking described in file   *)
+(*  ../LICENSE.                                                        *)
+(*                                                                     *)
+(***********************************************************************)
+
+(*
+  Time-stamp: <Last modified on 2013-03-04 23:01:55 CET by Kim Nguyen>
+*)
+
+(** Type equipped with an equality and hash function.
+    If [equal a b] then [(hash a) = (hash b)]
+*)
+module type HashedType =
+sig
+  type t
+
+    (** [hash v] returns an integer in the range [ 0 - 2^30-1 ]
+    *)
+  val hash : t -> int
+
+    (** Equality *)
+  val equal : t -> t -> bool
+
+end
+
+(** Type equiped with a total ordering *)
+module type OrderedType =
+sig
+  type t
+
+    (** Total ordering on values of type [t].  [compare a b] returns a
+        negative number if [a] is strictly smaller than [b], a positive
+        number if [a] is strictly greater than [b] and 0 if [a] is equal
+        to [b].  *)
+  val compare : t -> t -> int
+end
+
+module type Type =
+sig
+  type t
+  include HashedType with type t := t
+  include OrderedType with type t := t
+end
+
+(** Type equiped with a pretty-printer *)
+module type Printable =
+sig
+  type t
+  val print : Format.formatter -> t -> unit
+end
+
+(** Signature of a simple HashSet module *)
+module type HashSet =
+sig
+  type data
+  type t
+  val create : int -> t
+  val add : t -> data -> unit
+  val remove : t -> data -> unit
+  val find : t -> data -> data
+  val find_all : t -> data -> data list
+  val clear : t -> unit
+  val mem : t -> data -> bool
+end
+
+  (** Signature of simple Set module *)
+module type Set =
+sig
+  type elt
+  type t
+  val empty : t
+  val is_empty : t -> bool
+  val mem : elt -> t -> bool
+  val add : elt -> t -> t
+  val singleton : elt -> t
+  val remove : elt -> t -> t
+  val union : t -> t -> t
+  val inter : t -> t -> t
+  val diff : t -> t -> t
+  val compare : t -> t -> int
+  val equal : t -> t -> bool
+  val subset : t -> t -> bool
+  val iter : (elt -> unit) -> t -> unit
+  val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
+  val for_all : (elt -> bool) -> t -> bool
+  val exists : (elt -> bool) -> t -> bool
+  val filter : (elt -> bool) -> t -> t
+  val partition : (elt -> bool) -> t -> t * t
+  val cardinal : t -> int
+  val elements : t -> elt list
+  val min_elt : t -> elt
+  val max_elt : t -> elt
+  val choose : t -> elt
+  val split : elt -> t -> t * bool * t
+  val intersect : t -> t -> bool
+  val is_singleton : t -> bool
+  val from_list : elt list -> t
+end
diff --git a/src/eval.ml b/src/eval.ml
new file mode 100644
index 0000000..206debe
--- /dev/null
+++ b/src/eval.ml
@@ -0,0 +1,131 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                               TAToo                                 *)
+(*                                                                     *)
+(*                     Kim Nguyen, LRI UMR8623                         *)
+(*                   Université Paris-Sud & CNRS                       *)
+(*                                                                     *)
+(*  Copyright 2010-2013 Université Paris-Sud and Centre National de la *)
+(*  Recherche Scientifique. All rights reserved.  This file is         *)
+(*  distributed under the terms of the GNU Lesser General Public       *)
+(*  License, with the special exception on linking described in file   *)
+(*  ../LICENSE.                                                        *)
+(*                                                                     *)
+(***********************************************************************)
+
+(*
+  Time-stamp: <Last modified on 2013-04-04 18:45:19 CEST by Kim Nguyen>
+*)
+
+INCLUDE "utils.ml"
+open Format
+
+module Make (T : Tree.S) :
+  sig
+    val eval : Ata.t -> T.t -> T.node -> T.node list
+  end
+ = struct
+
+
+IFDEF HTMLTRACE
+  THEN
+DEFINE TRACE(e) = (e)
+  ELSE
+DEFINE TRACE(e) = ()
+END
+
+
+
+  type cache = StateSet.t Cache.N1.t
+  let get c t n = Cache.N1.find c (T.preorder t n)
+
+  let set c t n v = Cache.N1.add c (T.preorder t n) v
+
+
+  let top_down_run auto tree node cache _i =
+    let redo = ref false in
+    let rec loop node =
+      if node != T.nil then begin
+        let parent = T.parent tree node in
+        let fc = T.first_child tree node in
+        let ns = T.next_sibling tree node in
+        let tag = T.tag tree node in
+        let states0 = get cache tree node in
+        let trans0 = Ata.get_trans auto tag auto.Ata.states in
+        let () =
+          TRACE(Html.trace (T.preorder tree node) _i "Pre States: %a<br/>Pre Trans: %a<br/>"
+                  StateSet.print states0 (Ata.TransList.print ~sep:"<br/>") trans0)
+        in
+        let ps = get cache tree parent in
+        let fcs = get cache tree fc in
+        let nss = get cache tree ns in
+        let is_left = node == T.first_child tree parent
+        and is_right = node == T.next_sibling tree parent
+        and has_left = fc != T.nil
+        and has_right = ns != T.nil
+        and kind = T.kind tree node
+        in
+        let trans1, states1 =
+          Ata.eval_trans auto trans0
+            fcs nss ps states0
+            is_left is_right has_left has_right kind
+        in
+        let () =
+          TRACE(Html.trace (T.preorder tree node) _i "TD States: %a<br/>TD Trans: %a<br/>" StateSet.print states1 (Ata.TransList.print ~sep:"<br/>") trans1)
+        in
+        if states1 != states0 then set cache tree node states1;
+        let () = loop fc in
+        let fcs1 = get cache tree fc in
+        let trans2, states2 =
+          Ata.eval_trans auto trans1
+            fcs1 nss ps states1
+            is_left is_right has_left has_right kind
+        in
+        let () =
+          TRACE(Html.trace (T.preorder tree node) _i "Left BU States: %a<br/>Left BU Trans: %a<br/>" StateSet.print states2 (Ata.TransList.print ~sep:"<br/>") trans2)
+        in
+        if states2 != states1 then set cache tree node states2;
+        let () = loop ns in
+        let _trans3, states3 =
+          Ata.eval_trans auto trans2
+            fcs1 (get cache tree ns) ps states2
+            is_left is_right has_left has_right kind
+        in
+        let () =
+          TRACE(Html.trace (T.preorder tree node) _i "Right BU States: %a<br/>Right BU Trans: %a<br/>" StateSet.print states3 (Ata.TransList.print ~sep:"<br/>") _trans3)
+        in
+        if states3 != states2 then set cache tree node states3;
+        if states0 != states3 && (not !redo) then redo := true
+      end
+    in
+    loop node;
+    !redo
+
+  let get_results auto tree node cache =
+    let rec loop node acc =
+      if node == T.nil then acc
+      else
+        let acc0 = loop (T.next_sibling tree node) acc in
+        let acc1 = loop (T.first_child tree node) acc0 in
+
+        if StateSet.intersect (get cache tree node) auto.Ata.selection_states then
+          node::acc1
+        else
+          acc1
+    in
+    loop node []
+
+  let eval auto tree node =
+    let cache = Cache.N1.create StateSet.empty in
+    let redo = ref true in
+    let iter = ref 0 in
+    Ata.reset auto;
+    while !redo do
+      redo := top_down_run auto tree node cache !iter;
+      incr iter;
+    done;
+    let r = get_results auto tree node cache in
+    TRACE(Html.gen_trace (module T : Tree.Sig.S with type t = T.t) (tree));
+    r
+
+end
diff --git a/src/finiteCofinite.ml b/src/finiteCofinite.ml
new file mode 100644
index 0000000..2bfe70c
--- /dev/null
+++ b/src/finiteCofinite.ml
@@ -0,0 +1,221 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                               TAToo                                 *)
+(*                                                                     *)
+(*                     Kim Nguyen, LRI UMR8623                         *)
+(*                   Université Paris-Sud & CNRS                       *)
+(*                                                                     *)
+(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(*  Recherche Scientifique. All rights reserved.  This file is         *)
+(*  distributed under the terms of the GNU Lesser General Public       *)
+(*  License, with the special exception on linking described in file   *)
+(*  ../LICENSE.                                                        *)
+(*                                                                     *)
+(***********************************************************************)
+
+(*
+  Time-stamp: <Last modified on 2013-03-05 01:50:21 CET by Kim Nguyen>
+*)
+
+INCLUDE "utils.ml"
+
+include FiniteCofinite_sig
+
+module type HConsBuilder =
+  functor (H : Common_sig.HashedType) -> Hcons.S with type data = H.t
+
+module Builder (HCB : HConsBuilder) (E : Ptset.S) :
+  S with type elt = E.elt and type set = E.t =
+struct
+  type elt = E.elt
+  type node = Finite of E.t | CoFinite of E.t
+  type set = E.t
+  module Node = HCB(struct
+    type t = node
+    let equal a b =
+      match a, b with
+        Finite s1, Finite s2
+      | CoFinite s1, CoFinite s2 -> E.equal s1 s2
+      | (Finite _| CoFinite _), _ -> false
+
+    let hash = function
+      | Finite s -> HASHINT2 (PRIME1, E.hash s)
+      | CoFinite s -> HASHINT2 (PRIME3, E.hash s)
+  end)
+  include Node
+  let empty = make (Finite E.empty)
+  let any = make (CoFinite E.empty)
+  let finite x = make (Finite x)
+  let cofinite x = make (CoFinite x)
+
+  let is_empty t =  match t.node with
+    | Finite s -> E.is_empty s
+    | CoFinite _  -> false
+
+  let is_any t = match t.node with
+    | CoFinite s -> E.is_empty s
+    | Finite _  -> false
+
+  let is_finite t = match t.node with
+    | Finite _ -> true
+    | CoFinite _ -> false
+
+  let kind t = match t.node with
+    | Finite _ -> `Finite
+    | CoFinite _  -> `Cofinite
+
+  let mem x t = match t.node with
+    | Finite s -> E.mem x s
+    | CoFinite s -> not (E.mem x s)
+
+  let singleton x = finite (E.singleton x)
+
+  let add e t = match t.node with
+    | Finite s -> finite (E.add e s)
+    | CoFinite s -> cofinite (E.remove e s)
+
+  let remove e t = match t.node with
+    | Finite s -> finite (E.remove e s)
+    | CoFinite s -> cofinite (E.add e s)
+
+  let union s t = match s.node, t.node with
+    | Finite s, Finite t -> finite (E.union s t)
+    | CoFinite s, CoFinite t -> cofinite ( E.inter s t)
+    | Finite s, CoFinite t -> cofinite (E.diff t s)
+    | CoFinite s, Finite t-> cofinite (E.diff s t)
+
+  let inter s t = match s.node, t.node with
+    | Finite s, Finite t -> finite (E.inter s t)
+    | CoFinite s, CoFinite t -> cofinite (E.union s t)
+    | Finite s, CoFinite t -> finite (E.diff s t)
+    | CoFinite s, Finite t-> finite (E.diff t s)
+
+  let diff s t = match s.node, t.node with
+    | Finite s, Finite t -> finite (E.diff s t)
+    | Finite s, CoFinite t -> finite(E.inter s t)
+    | CoFinite s, Finite t -> cofinite(E.union t s)
+    | CoFinite s, CoFinite t -> finite (E.diff t s)
+
+  let complement t = match t.node with
+    | Finite s -> cofinite s
+    | CoFinite s -> finite s
+
+  let compare s t = match s.node, t.node with
+    | Finite s , Finite t -> E.compare s t
+    | CoFinite s , CoFinite t -> E.compare t s
+    | Finite _, CoFinite _ -> -1
+    | CoFinite _, Finite _ -> 1
+
+  let subset s t = match s.node, t.node with
+    | Finite s , Finite t -> E.subset s t
+    | CoFinite s , CoFinite t -> E.subset t s
+    | Finite s, CoFinite t -> E.is_empty (E.inter s t)
+    | CoFinite _, Finite _ -> false
+
+  (* given a  list l of type t list,
+     returns two sets (f,c) where :
+     - f is the union of all the finite sets of l
+     - c is the union of all the cofinite sets of l
+     - f and c are disjoint
+     Invariant : cup f c = List.fold_left cup empty l
+     We treat the CoFinite part explicitely :
+  *)
+
+  let kind_split l =
+
+    let rec next_finite_cofinite facc cacc = function
+      | [] -> finite facc, cofinite (E.diff cacc facc)
+      | { node = Finite s; _ } ::r ->
+        next_finite_cofinite (E.union s facc) cacc r
+      | { node = CoFinite _ ; _ } ::r when E.is_empty cacc ->
+        next_finite_cofinite facc cacc r
+      | { node = CoFinite s; _ } ::r ->
+        next_finite_cofinite facc (E.inter cacc s) r
+    in
+    let rec first_cofinite facc = function
+      | [] -> empty,empty
+      | { node = Finite s ; _ } :: r-> first_cofinite (E.union s facc) r
+      | { node = CoFinite s ; _ } :: r -> next_finite_cofinite facc s r
+    in
+      first_cofinite E.empty l
+
+  let exn = FiniteCofinite_sig.InfiniteSet
+
+  let fold f t a = match t.node with
+    | Finite s -> E.fold f s a
+    | CoFinite _ -> raise exn
+
+  let iter f t = match t.node with
+    | Finite t -> E.iter f t
+    | CoFinite _ -> raise exn
+
+  let for_all f t = match t.node with
+    | Finite s -> E.for_all f s
+    | CoFinite _ -> raise exn
+
+  let exists f t = match t.node with
+    | Finite s -> E.exists f s
+    | CoFinite _ -> raise exn
+
+  let filter f t = match t.node with
+    | Finite s -> finite (E.filter f s)
+    | CoFinite _ -> raise exn
+
+  let partition f t = match t.node with
+    | Finite s -> let a,b = E.partition f s in finite a,finite b
+    | CoFinite _ -> raise exn
+
+  let cardinal t = match t.node with
+    | Finite s -> E.cardinal s
+    | CoFinite _ -> raise exn
+
+  let elements t = match t.node with
+    | Finite s -> E.elements s
+    | CoFinite _ -> raise exn
+
+  let from_list l =
+    finite (List.fold_left (fun x a -> E.add a x ) E.empty l)
+
+  let choose t = match t.node with
+      Finite s -> E.choose s
+    | CoFinite _ -> raise exn
+
+  let is_singleton t = match t.node with
+    | Finite s -> E.is_singleton s
+    | CoFinite _ -> false
+
+  let intersect s t = match s.node, t.node with
+    | Finite s, Finite t -> E.intersect s t
+    | CoFinite s, Finite t -> not (E.subset t s)
+    | Finite s, CoFinite t -> not (E.subset s t)
+    | CoFinite _ , CoFinite _ -> true
+
+  let split x s = match s.node with
+    | Finite s ->
+      let s1, b, s2 = E.split x s in
+      finite s1, b, finite s2
+
+    | CoFinite _ -> raise exn
+
+  let min_elt s = match s.node with
+    | Finite s -> E.min_elt s
+    | CoFinite _ -> raise exn
+
+  let max_elt s = match s.node with
+    | Finite s -> E.min_elt s
+    | CoFinite _ -> raise exn
+
+  let positive t = match t.node with
+      | Finite x -> x
+      | CoFinite _ -> E.empty
+
+  let negative t = match t.node with
+      | CoFinite x -> x
+      | Finite _ -> E.empty
+
+  let inj_positive t = finite t
+  let inj_negative t = cofinite t
+end
+
+module Make = Builder(Hcons.Make)
+module Weak = Builder(Hcons.Weak)
diff --git a/src/finiteCofinite.mli b/src/finiteCofinite.mli
new file mode 100644
index 0000000..cd92cda
--- /dev/null
+++ b/src/finiteCofinite.mli
@@ -0,0 +1,36 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                               TAToo                                 *)
+(*                                                                     *)
+(*                     Kim Nguyen, LRI UMR8623                         *)
+(*                   Université Paris-Sud & CNRS                       *)
+(*                                                                     *)
+(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(*  Recherche Scientifique. All rights reserved.  This file is         *)
+(*  distributed under the terms of the GNU Lesser General Public       *)
+(*  License, with the special exception on linking described in file   *)
+(*  ../LICENSE.                                                        *)
+(*                                                                     *)
+(***********************************************************************)
+
+(*
+  Time-stamp: <Last modified on 2013-03-04 22:44:50 CET by Kim Nguyen>
+*)
+
+(** Implementation of hashconsed finite or cofinite sets.
+*)
+
+include module type of FiniteCofinite_sig
+
+(** Output signature of the {!FiniteCofinite.Make} and
+    {!FiniteCofinite.Weak} functors.*)
+
+module Make (E : Ptset.S) : S with type elt = E.elt and type set = E.t
+(** Builds an implementation of hashconsed sets of hashconsed elements.
+    See {!Hcons.Make}.
+*)
+
+module Weak (E : Ptset.S) : S with type elt = E.elt and type set = E.t
+(** Builds an implementation of hashconsed sets of hashconsed elements
+    with weak internal storage. See {!Hcons.Weak}.
+*)
diff --git a/src/finiteCofinite_sig.ml b/src/finiteCofinite_sig.ml
new file mode 100644
index 0000000..da17049
--- /dev/null
+++ b/src/finiteCofinite_sig.ml
@@ -0,0 +1,36 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                               TAToo                                 *)
+(*                                                                     *)
+(*                     Kim Nguyen, LRI UMR8623                         *)
+(*                   Université Paris-Sud & CNRS                       *)
+(*                                                                     *)
+(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(*  Recherche Scientifique. All rights reserved.  This file is         *)
+(*  distributed under the terms of the GNU Lesser General Public       *)
+(*  License, with the special exception on linking described in file   *)
+(*  ../LICENSE.                                                        *)
+(*                                                                     *)
+(***********************************************************************)
+
+(*
+  Time-stamp: <Last modified on 2013-03-04 22:44:15 CET by Kim Nguyen>
+*)
+
+exception InfiniteSet
+module type S =
+sig
+  include Hcons.S
+  include Common_sig.Set with type t := t
+  type set
+  val any : t
+  val is_any : t -> bool
+  val is_finite : t -> bool
+  val kind : t -> [ `Finite | `Cofinite ]
+  val complement : t -> t
+  val kind_split : t list -> t * t
+  val positive : t -> set
+  val negative : t -> set
+  val inj_positive : set -> t
+  val inj_negative : set -> t
+end
diff --git a/src/formula.ml b/src/formula.ml
new file mode 100644
index 0000000..7d37e5b
--- /dev/null
+++ b/src/formula.ml
@@ -0,0 +1,181 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                               TAToo                                 *)
+(*                                                                     *)
+(*                     Kim Nguyen, LRI UMR8623                         *)
+(*                   Université Paris-Sud & CNRS                       *)
+(*                                                                     *)
+(*  Copyright 2010-2013 Université Paris-Sud and Centre National de la *)
+(*  Recherche Scientifique. All rights reserved.  This file is         *)
+(*  distributed under the terms of the GNU Lesser General Public       *)
+(*  License, with the special exception on linking described in file   *)
+(*  ../LICENSE.                                                        *)
+(*                                                                     *)
+(***********************************************************************)
+
+(*
+  Time-stamp: <Last modified on 2013-04-04 18:46:09 CEST by Kim Nguyen>
+*)
+
+INCLUDE "utils.ml"
+
+open Format
+
+(*
+
+(** Implementation of hashconsed Boolean formulae *)
+
+*)
+module type ATOM =
+sig
+  type t
+  val neg : t -> t
+  include Hcons.Abstract with type t := t
+  include Common_sig.Printable with type t := t
+end
+
+type ('formula,'atom) expr =
+  | False
+  | True
+  | Or of 'formula * 'formula
+  | And of 'formula * 'formula
+  | Atom of 'atom
+
+module Make (P: ATOM) =
+struct
+
+
+  type 'hcons node = {
+    pos : ('hcons,P.t) expr;
+    mutable neg : 'hcons;
+  }
+
+  external hash_const_variant : [> ] -> int = "%identity"
+  external vb : bool -> int = "%identity"
+
+  module rec Node : Hcons.S
+    with type data = Data.t = Hcons.Make (Data)
+    and Data : Common_sig.HashedType  with type t = Node.t node =
+  struct
+    type t =  Node.t node
+    let equal x y =
+      match x.pos, y.pos with
+      | a,b when a == b -> true
+      | Or(xf1, xf2), Or(yf1, yf2)
+      | And(xf1, xf2), And(yf1,yf2)  -> xf1 == yf1 && xf2 == yf2
+      | Atom(p1), Atom(p2) -> p1 == p2
+      | _ -> false
+
+    let hash f =
+      match f.pos with
+      | False -> 0
+      | True -> 1
+      | Or (f1, f2) ->
+          HASHINT3 (PRIME1, Uid.to_int f1.Node.id, Uid.to_int f2.Node.id)
+      | And (f1, f2) ->
+          HASHINT3(PRIME3, Uid.to_int f1.Node.id, Uid.to_int f2.Node.id)
+      | Atom(p) -> HASHINT2(PRIME5, Uid.to_int (P.uid p))
+  end
+
+    type t = Node.t
+    let hash x = x.Node.hash
+    let uid x = x.Node.id
+    let equal = Node.equal
+    let expr f = f.Node.node.pos
+
+    let compare f1 f2 = compare f1.Node.id  f2.Node.id
+    let prio f =
+      match expr f with
+      | True | False -> 10
+      | Atom _ -> 8
+      | And _ -> 6
+      | Or _ -> 1
+
+    let rec print ?(parent=false) ppf f =
+      if parent then fprintf ppf "(";
+      let _ = match expr f with
+      | True -> fprintf ppf "%s" Pretty.top
+      | False -> fprintf ppf "%s" Pretty.bottom
+      | And(f1,f2) ->
+          print ~parent:(prio f > prio f1) ppf f1;
+          fprintf ppf " %s "  Pretty.wedge;
+          print ~parent:(prio f > prio f2) ppf f2;
+      | Or(f1,f2) ->
+          (print ppf f1);
+          fprintf ppf " %s " Pretty.vee;
+          (print ppf f2);
+      | Atom(p) -> fprintf ppf "%a" P.print p
+(*          let _ = flush_str_formatter() in
+          let fmt = str_formatter in
+          let a_str, d_str =
+          match  dir with
+          | `Left ->  Pretty.down_arrow, Pretty.subscript 1
+          | `Right -> Pretty.down_arrow, Pretty.subscript 2
+          | `Epsilon -> Pretty.epsilon, ""
+          | `Up1 -> Pretty.up_arrow, Pretty.subscript 1
+          | `Up2 -> Pretty.up_arrow, Pretty.subscript 2
+        in
+        fprintf fmt "%s%s" a_str d_str;
+        State.print fmt s;
+        let str = flush_str_formatter() in
+        if b then fprintf ppf "%s" str
+        else Pretty.pp_overline ppf str *)
+  in
+    if parent then fprintf ppf ")"
+
+let print ppf f =  print ~parent:false ppf f
+
+let is_true f = (expr f) == True
+let is_false f = (expr f) == False
+
+
+let cons pos neg =
+  let nnode = Node.make { pos = neg; neg = Obj.magic 0 } in
+  let pnode = Node.make { pos = pos; neg = nnode } in
+    (Node.node nnode).neg <- pnode; (* works because the neg field isn't taken into
+                                       account for hashing ! *)
+    pnode,nnode
+
+
+let true_,false_ = cons True False
+
+let atom_ p = fst (cons (Atom(p)) (Atom(P.neg p)))
+
+let not_ f = f.Node.node.neg
+
+let order f1 f2 = if uid f1 < uid f2 then f2,f1 else f1,f2
+
+let or_ f1 f2 =
+  (* Tautologies: x|x, x|not(x) *)
+
+  if equal f1 f2 then f1
+  else if equal f1 (not_ f2) then true_
+
+  (* simplification *)
+  else if is_true f1 || is_true f2 then true_
+  else if is_false f1 && is_false f2 then false_
+  else if is_false f1 then f2
+  else if is_false f2 then f1
+
+  (* commutativity of | *)
+  else
+    let f1, f2 = order f1 f2 in
+      fst (cons (Or(f1,f2)) (And(not_ f1, not_ f2)))
+
+
+let and_ f1 f2 =
+  not_ (or_ (not_ f1) (not_ f2))
+
+
+let of_bool = function true -> true_ | false -> false_
+
+let fold f phi acc =
+  let rec loop phi acc =
+    match expr phi with
+    | And (phi1, phi2) | Or(phi1, phi2)  ->
+        loop phi2 (loop phi1 (f phi acc))
+    | _ -> f phi acc
+  in
+  loop phi acc
+
+end
diff --git a/src/formula.mli b/src/formula.mli
new file mode 100644
index 0000000..52e38b7
--- /dev/null
+++ b/src/formula.mli
@@ -0,0 +1,90 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                               TAToo                                 *)
+(*                                                                     *)
+(*                     Kim Nguyen, LRI UMR8623                         *)
+(*                   Université Paris-Sud & CNRS                       *)
+(*                                                                     *)
+(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(*  Recherche Scientifique. All rights reserved.  This file is         *)
+(*  distributed under the terms of the GNU Lesser General Public       *)
+(*  License, with the special exception on linking described in file   *)
+(*  ../LICENSE.                                                        *)
+(*                                                                     *)
+(***********************************************************************)
+
+(*
+  Time-stamp: <Last modified on 2013-04-04 18:41:24 CEST by Kim Nguyen>
+*)
+
+module type ATOM =
+sig
+  type t
+  val neg : t -> t
+  include Hcons.Abstract with type t := t
+  include Common_sig.Printable with type t := t
+end
+
+type ('formula,'atom) expr =
+  | False
+  | True
+  | Or of 'formula * 'formula
+  | And of 'formula * 'formula
+  | Atom of 'atom
+
+(** View of the internal representation of a formula,
+    used for pattern matching *)
+
+module Make(P : ATOM) :
+sig
+  type t
+
+  (** Abstract type representing hashconsed formulae *)
+
+  val hash : t -> int
+  (** Hash function for formulae *)
+
+  val uid : t -> Uid.t
+  (** Returns a unique ID for formulae *)
+
+  val equal : t -> t -> bool
+  (** Equality over formulae *)
+
+  val expr : t -> (t,P.t) expr
+  (** Return a view of the formulae *)
+
+  val compare : t -> t -> int
+  (** Comparison of formulae *)
+
+  val print : Format.formatter -> t -> unit
+  (** Pretty printer *)
+
+  val is_true : t -> bool
+  (** [is_true f] tests whether the formula is the atom True *)
+
+  val is_false : t -> bool
+  (** [is_false f] tests whether the formula is the atom False *)
+
+  val true_ : t
+  (** Atom True *)
+
+  val false_ : t
+  (** Atom False *)
+
+  val atom_ : P.t -> t
+  (** [atom_ dir b q] creates a down_left or down_right atom for state
+      [q]. The atom is positive if [b == true].
+  *)
+
+  val not_ : t -> t
+  val or_ : t -> t -> t
+  val and_ : t -> t -> t
+  (** Boolean connective *)
+
+  val of_bool : bool -> t
+  (** Convert an ocaml Boolean value to a formula *)
+
+  val fold : (t -> 'a -> 'a) -> t -> 'a -> 'a
+  (** [fold f phi acc] folds [f] over the formula structure *)
+
+end
diff --git a/src/hcons.ml b/src/hcons.ml
new file mode 100644
index 0000000..3fc3e71
--- /dev/null
+++ b/src/hcons.ml
@@ -0,0 +1,84 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                               TAToo                                 *)
+(*                                                                     *)
+(*                     Kim Nguyen, LRI UMR8623                         *)
+(*                   Université Paris-Sud & CNRS                       *)
+(*                                                                     *)
+(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(*  Recherche Scientifique. All rights reserved.  This file is         *)
+(*  distributed under the terms of the GNU Lesser General Public       *)
+(*  License, with the special exception on linking described in file   *)
+(*  ../LICENSE.                                                        *)
+(*                                                                     *)
+(***********************************************************************)
+
+(*
+  Time-stamp: <Last modified on 2013-03-04 22:39:39 CET by Kim Nguyen>
+*)
+
+include Hcons_sig
+
+module type TableBuilder =
+  functor
+    (H : Common_sig.HashedType) ->
+      Common_sig.HashSet with type data = H.t
+
+module Builder (TB : TableBuilder) (H : Common_sig.HashedType) =
+struct
+  type data = H.t
+  type t = { id   : Uid.t;
+             hash : int;
+             node : data }
+  let uid_make = ref (Uid.make_maker())
+  let node t = t.node
+  let uid t = t.id
+  let hash t = t.hash
+  let equal t1 t2 = t1 == t2
+  module HN =
+  struct
+    type _t = t
+    type t = _t
+    let hash = hash
+    let equal x y = x == y || H.equal x.node y.node
+  end
+  module T = TB(HN)
+
+  let pool = T.create 101
+  let init () =
+    T.clear pool;
+    uid_make := Uid.make_maker ()
+  let dummy x = { id = Uid.dummy; hash = H.hash x; node = x }
+
+  let make x =
+    let cell = { id = Uid.dummy; hash = H.hash x; node = x } in
+    try
+      T.find pool cell
+    with
+    | Not_found ->
+      let cell = { cell with id = !uid_make(); } in
+      T.add pool cell;
+      cell
+end
+
+module Make = Builder (Misc.HashSet)
+module Weak = Builder (Weak.Make)
+
+module PosInt =
+struct
+  type data = int
+  type t = int
+  let make v =
+    if v < 0 then raise (Invalid_argument "Hcons.PosInt.make")
+    else v
+
+  let node v = v
+
+  let hash v = v
+
+  let uid v = Uid.of_int v
+  let dummy _ = ~-1
+  let equal x y = x == y
+
+  let init () = ()
+end
diff --git a/src/hcons.mli b/src/hcons.mli
new file mode 100644
index 0000000..b4049a0
--- /dev/null
+++ b/src/hcons.mli
@@ -0,0 +1,45 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                               TAToo                                 *)
+(*                                                                     *)
+(*                     Kim Nguyen, LRI UMR8623                         *)
+(*                   Université Paris-Sud & CNRS                       *)
+(*                                                                     *)
+(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(*  Recherche Scientifique. All rights reserved.  This file is         *)
+(*  distributed under the terms of the GNU Lesser General Public       *)
+(*  License, with the special exception on linking described in file   *)
+(*  ../LICENSE.                                                        *)
+(*                                                                     *)
+(***********************************************************************)
+
+(*
+  Time-stamp: <Last modified on 2013-03-04 23:05:14 CET by Kim Nguyen>
+*)
+
+(** Implementation of generic hashconsing. *)
+
+include module type of Hcons_sig
+
+(** Output signature of the functor {!Hcons.Make} *)
+
+module Make (H : Common_sig.HashedType) : S with type data = H.t
+(** Functor building an implementation of hashconsed values for a given
+    implementation of {!Common_sig.HashedType}. Hashconsed values are
+    persistent: the are kept in memory even if no external reference
+    remain. Calling [init()] explicitely will reclaim the space.
+*)
+
+module Weak (H : Common_sig.HashedType) : S with type data = H.t
+(** Functor building an implementation of hashconsed values for a given
+    implementation of {!Common_sig.HashedType}. Hashconsed values have a
+    weak semantics: they may be reclaimed as soon as no external
+    reference to them exists. The space may still be reclaimed
+    explicitely by calling [init].
+*)
+
+module PosInt : Abstract with type data = int and type t = int
+(** Compact implementation of hashconsed positive integer that
+    avoids boxing. [PosInt.make v] raises [Invalid_argument] if
+    [ v < 0 ]
+*)
diff --git a/src/hcons_sig.ml b/src/hcons_sig.ml
new file mode 100644
index 0000000..599819c
--- /dev/null
+++ b/src/hcons_sig.ml
@@ -0,0 +1,68 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                               TAToo                                 *)
+(*                                                                     *)
+(*                     Kim Nguyen, LRI UMR8623                         *)
+(*                   Université Paris-Sud & CNRS                       *)
+(*                                                                     *)
+(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(*  Recherche Scientifique. All rights reserved.  This file is         *)
+(*  distributed under the terms of the GNU Lesser General Public       *)
+(*  License, with the special exception on linking described in file   *)
+(*  ../LICENSE.                                                        *)
+(*                                                                     *)
+(***********************************************************************)
+
+(*
+  Time-stamp: <Last modified on 2013-03-04 22:36:31 CET by Kim Nguyen>
+*)
+
+  (** Abstract signature of a module implementing an hashconsed datatype *)
+module type Abstract =
+sig
+
+    (** The type of the data to be hash-consed *)
+  type data
+
+    (** The type of hashconsed data *)
+  type t
+
+    (** [make v] internalizes the value [v], making it an hashconsed
+        value.
+    *)
+  val make : data -> t
+
+    (** [node h] extract the original data from its hashconsed value
+    *)
+  val node : t -> data
+
+    (** [hash h] returns a hash of [h], such that for every [h1] and
+        [h2], [equal h1 h2] implies [hash h1 = hash h2].
+    *)
+  val hash : t -> int
+
+    (** [uid h] returns a unique identifier *)
+  val uid : t -> Uid.t
+
+    (** Equality between hashconsed values. Equivalent to [==] *)
+  val equal : t -> t -> bool
+
+    (** Initializes the internal storage. Any previously hashconsed
+        element is discarded. *)
+  val init : unit -> unit
+
+    (** Create a dummy (non-hashconsed) node with a boggus identifer
+        and hash *)
+  val dummy : data -> t
+end
+
+
+  (** Concrete signature of a module implementing an hashconsed datatype *)
+module type S =
+sig
+  type data
+  type t = private { id   : Uid.t;
+                     hash : int;
+                     node : data }
+  include Abstract with type data := data and type t := t
+end
diff --git a/src/hlist.ml b/src/hlist.ml
new file mode 100644
index 0000000..3ffb8fc
--- /dev/null
+++ b/src/hlist.ml
@@ -0,0 +1,82 @@
+INCLUDE "utils.ml"
+
+include Hlist_sig
+
+module type HConsBuilder =
+  functor (H : Common_sig.HashedType) -> Hcons.S with type data = H.t
+
+module Builder (HCB : HConsBuilder) (H : Hcons.Abstract) :
+  S with type elt = H.t =
+struct
+  type elt = H.t
+
+  module rec Node : Hcons.S with type data = Data.t = HCB(Data)
+                            and Data : Common_sig.HashedType with type t = (elt, Node.t) node =
+  struct
+    type t = (elt, Node.t) node
+    let equal x y =
+      match x,y with
+      | Nil, Nil -> true
+      | Cons(e1, l1), Cons(e2, l2) -> e1 == e2 && l1 == l2
+      | _ -> false
+
+    let hash = function
+    | Nil -> 0
+    | Cons(e, l) -> HASHINT3 (PRIME1, Uid.to_int (H.uid e), Uid.to_int (Node.uid l))
+  end
+
+  include Node
+
+  let nil = make Nil
+
+  let rec sorted_cons e l =
+    match l.Node.node with
+      |	Nil -> Node.make (Cons(e, l))
+      | Cons (x, ll) ->
+	  if H.uid e < H.uid x
+	  then Node.make (Cons(e, l))
+	  else Node.make (Cons(x, sorted_cons e ll))
+
+  let cons e l =
+    Node.make(Cons(e, l))
+
+  let cons ?(sorted=true) e l =
+    if sorted then sorted_cons e l else cons e l
+
+  let hd = function { Node.node = Cons(e, _); _ } -> e | _ -> failwith "hd"
+  let tl = function { Node.node = Cons(_, l); _ } -> l | _ -> failwith "tl"
+
+  let fold f l acc =
+    let rec loop acc l = match l.Node.node with
+      | Nil -> acc
+      | Cons (a, aa) -> loop (f a acc) aa
+    in
+      loop acc l
+
+  let map f l  =
+    let rec loop l = match l.Node.node with
+      | Nil -> nil
+      | Cons(a, aa) -> cons (f a) (loop aa)
+    in
+      loop l
+
+  let iter f l =
+    let rec loop l = match l.Node.node with
+      | Nil -> ()
+      | Cons(a,aa) ->  (f a);(loop aa)
+    in
+      loop l
+
+  let rev l = fold cons l nil
+  let rev_map f l = fold (fun x acc -> cons (f x) acc) l nil
+  let length l = fold (fun _ c -> c+1) l 0
+  let rec mem e l =
+    match l.Node.node with
+      | Nil -> false
+      | Cons (x, ll) -> x == e || mem e ll
+
+end
+
+module Make = Builder(Hcons.Make)
+module Weak = Builder(Hcons.Weak)
+
diff --git a/src/hlist.mli b/src/hlist.mli
new file mode 100644
index 0000000..80204d2
--- /dev/null
+++ b/src/hlist.mli
@@ -0,0 +1,30 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                               TAToo                                 *)
+(*                                                                     *)
+(*                     Kim Nguyen, LRI UMR8623                         *)
+(*                   Université Paris-Sud & CNRS                       *)
+(*                                                                     *)
+(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(*  Recherche Scientifique. All rights reserved.  This file is         *)
+(*  distributed under the terms of the GNU Lesser General Public       *)
+(*  License, with the special exception on linking described in file   *)
+(*  ../LICENSE.                                                        *)
+(*                                                                     *)
+(***********************************************************************)
+
+(*
+  Time-stamp: <Last modified on 2013-03-13 18:30:59 CET by Kim Nguyen>
+*)
+
+include module type of Hlist_sig
+
+module Make (H : Hcons.Abstract) : S with type elt = H.t
+(** Builds an implementation of hashconsed lists of hashconsed elements.
+    See {!Hcons.Make}.
+*)
+
+module Weak (H : Hcons.Abstract) : S with type elt = H.t
+(** Builds an implementation of hashconsed lists of hashconsed elements
+    with weak internal storage. See {!Hcons.Weak}.
+*)
diff --git a/src/hlist_sig.ml b/src/hlist_sig.ml
new file mode 100644
index 0000000..227768c
--- /dev/null
+++ b/src/hlist_sig.ml
@@ -0,0 +1,35 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                               TAToo                                 *)
+(*                                                                     *)
+(*                     Kim Nguyen, LRI UMR8623                         *)
+(*                   Université Paris-Sud & CNRS                       *)
+(*                                                                     *)
+(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(*  Recherche Scientifique. All rights reserved.  This file is         *)
+(*  distributed under the terms of the GNU Lesser General Public       *)
+(*  License, with the special exception on linking described in file   *)
+(*  ../LICENSE.                                                        *)
+(*                                                                     *)
+(***********************************************************************)
+
+(*
+  Time-stamp: <Last modified on 2013-03-13 18:21:28 CET by Kim Nguyen>
+*)
+type ('a,'b) node = Nil | Cons of ('a * 'b)
+
+module type S = sig
+  type elt
+  include Hcons.S
+  val nil : t
+  val cons : ?sorted:bool -> elt -> t -> t
+  val hd : t -> elt
+  val tl : t -> t
+  val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
+  val map : (elt -> elt) -> t -> t
+  val iter : (elt -> 'a) -> t -> unit
+  val rev : t -> t
+  val rev_map : (elt -> elt) -> t -> t
+  val length : t -> int
+  val mem : elt -> t -> bool
+end
diff --git a/src/html.ml b/src/html.ml
new file mode 100644
index 0000000..6c45c93
--- /dev/null
+++ b/src/html.ml
@@ -0,0 +1,92 @@
+open Format
+module M = Map.Make(struct type t = int let compare = compare end)
+
+let info = Hashtbl.create 2017
+
+
+let add_info (nodeid:int) (i:int) s =
+  let m = try Hashtbl.find info nodeid with Not_found -> M.empty in
+  let old_s = try M.find i m with Not_found -> "" in
+  let s' = old_s ^ s in
+  let m' = M.add i s' m in
+  Hashtbl.replace info nodeid m'
+
+let buff = Buffer.create 20
+let fmt = formatter_of_buffer buff
+
+let trace nodeid i =
+  let () = pp_print_flush fmt ();
+    Buffer.clear buff
+  in
+  kfprintf (fun fmt ->
+    pp_print_flush fmt ();
+    let s = Buffer.contents buff in
+    add_info nodeid i s) fmt
+
+
+let gen_trace (type s)  = (); fun t tree ->
+  let module T = (val (t) : Tree.Sig.S with type t = s) in
+  let rec loop odot ohtml node parent =
+    if node == T.nil then () else begin
+      let s_node = "node" ^ (string_of_int (T.preorder tree node)) in
+      fprintf odot "%s[ id=\"%s\" label=\"%s\"];\n"
+        s_node s_node (Utils.QName.to_string (T.tag tree node));
+      let m =
+        try
+          Hashtbl.find info (T.preorder tree node)
+        with Not_found -> M.empty
+      in
+      fprintf ohtml "data['%s'] = new Array();\n" s_node;
+      M.iter
+        (fun i s -> fprintf ohtml "data['%s'][%i] = '%s';\n" s_node i s)
+        m;
+      if parent != T.nil then
+        fprintf odot "node%i -> %s;\n"
+          (T.preorder tree parent) s_node;
+      loop odot ohtml (T.first_child tree node) node;
+      loop odot ohtml (T.next_sibling tree node) parent
+    end
+  in
+  ignore (Sys.command "mkdir -p tests/trace");
+  let odot_ = open_out "tests/trace/trace.dot" in
+  let ohtml_ = open_out "tests/trace/trace.html" in
+  let odot = formatter_of_out_channel odot_ in
+  let ohtml = formatter_of_out_channel ohtml_ in
+  fprintf odot "digraph G {\n node[shape=box, style=filled, fillcolor=white];splines=false;";
+  fprintf ohtml "<html>\
+<head><title></title>
+<link rel='stylesheet' type='text/css' href='trace.css' />\
+<meta http-equiv='content-type' content='text/html;charset=utf-8'/>\
+</head>\
+<body>\
+<div id='data' > </div>\
+<script type='text/javascript'>";
+  loop odot ohtml (T.root tree) (T.nil);
+  fprintf odot "\n}\n%!";
+  pp_print_flush odot ();
+  close_out odot_;
+  ignore (Sys.command "dot -o tests/trace/trace.svg -Tsvg tests/trace/trace.dot");
+  ignore (Sys.command "./tools/add_onclick.sh tests/trace/trace.svg > tests/trace/trace2.svg");
+  fprintf ohtml "var activate = function (id) {\
+  var d = document.getElementById('data');
+  var msg = '';
+  for (i=0; i < data[id].length; i++)
+     msg += ('<p>' + i + ':') + data[id][i] + '</p>\\n';
+  d.innerHTML = msg;
+  return;
+  };\n";
+
+  fprintf ohtml "</script>\n<div id='svg'>\n";
+  let fi = open_in "tests/trace/trace2.svg" in
+  try
+    while true do
+      let s = input_line fi in
+      fprintf ohtml "%s\n" s;
+    done
+  with
+    End_of_file ->
+      fprintf ohtml "</div></body></html>\n%!";
+      pp_print_flush ohtml ();
+      close_out ohtml_;
+      close_in fi
+
diff --git a/src/html.mli b/src/html.mli
new file mode 100644
index 0000000..0a7d8dd
--- /dev/null
+++ b/src/html.mli
@@ -0,0 +1,2 @@
+val trace : int -> int -> ('a, Format.formatter, unit, unit) format4 -> 'a
+val gen_trace : (module Tree.Sig.S with type t = 'a) -> 'a -> unit
diff --git a/src/misc.ml b/src/misc.ml
new file mode 100644
index 0000000..f8156b0
--- /dev/null
+++ b/src/misc.ml
@@ -0,0 +1,51 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                               TAToo                                 *)
+(*                                                                     *)
+(*                     Kim Nguyen, LRI UMR8623                         *)
+(*                   Université Paris-Sud & CNRS                       *)
+(*                                                                     *)
+(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(*  Recherche Scientifique. All rights reserved.  This file is         *)
+(*  distributed under the terms of the GNU Lesser General Public       *)
+(*  License, with the special exception on linking described in file   *)
+(*  ../LICENSE.                                                        *)
+(*                                                                     *)
+(***********************************************************************)
+
+(*
+  Time-stamp: <Last modified on 2013-03-04 23:00:19 CET by Kim Nguyen>
+*)
+
+(** Various generic signatures and generic module and functor definitions
+*)
+INCLUDE "utils.ml"
+
+module HashSet (H : Hashtbl.HashedType) :
+  Common_sig.HashSet with type data = H.t =
+struct
+  module T = Hashtbl.Make(H)
+  type data = H.t
+  type t = data T.t
+  let create = T.create
+  let add h v = T.add h v v
+  let find = T.find
+  let remove = T.remove
+  let find_all = T.find_all
+  let clear = T.clear
+  let mem = T.mem
+end
+
+module Pair (X : Common_sig.Type) (Y : Common_sig.Type) :
+  Common_sig.Type with type t = X.t * Y.t =
+struct
+  type t = X.t * Y.t
+  let hash (x, y) = HASHINT2(X.hash x, Y.hash y)
+  let compare (x1, y1) (x2, y2) =
+    let r = X.compare x1 x2 in
+    if r != 0 then r else Y.compare y1 y2
+  let equal p1 p2 =
+    p1 == p2 ||
+      let x1, y1 = p1
+      and x2, y2 = p2 in X.equal x1 x2 && Y.equal y1 y2
+end
diff --git a/src/naive_tree.ml b/src/naive_tree.ml
new file mode 100644
index 0000000..b7c0be6
--- /dev/null
+++ b/src/naive_tree.ml
@@ -0,0 +1,313 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                               TAToo                                 *)
+(*                                                                     *)
+(*                     Kim Nguyen, LRI UMR8623                         *)
+(*                   Université Paris-Sud & CNRS                       *)
+(*                                                                     *)
+(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(*  Recherche Scientifique. All rights reserved.  This file is         *)
+(*  distributed under the terms of the GNU Lesser General Public       *)
+(*  License, with the special exception on linking described in file   *)
+(*  ../LICENSE.                                                        *)
+(*                                                                     *)
+(***********************************************************************)
+
+(*
+  Time-stamp: <Last modified on 2013-04-04 18:47:30 CEST by Kim Nguyen>
+*)
+
+type node = {
+  tag : QName.t;
+  preorder : int;
+  mutable kind : Tree.NodeKind.t;
+  mutable data : string;
+  mutable first_child : node;
+  mutable next_sibling : node;
+  mutable parent: node;
+}
+
+
+
+let rec nil = {
+  tag = QName.nil;
+  kind = Tree.NodeKind.Element;
+  preorder = -1;
+  data = "";
+  first_child = nil;
+  next_sibling = nil;
+  parent = nil;
+}
+
+let dummy_tag = QName.of_string "#dummy"
+let rec dummy = {
+  tag = dummy_tag;
+  kind = Tree.NodeKind.Element;
+  preorder = -1;
+  data = "";
+  first_child = dummy;
+  next_sibling = dummy;
+  parent = dummy;
+}
+
+
+type t = {
+  root : node;
+  size : int;
+  (* TODO add other intersting stuff *)
+}
+
+
+
+module Parser =
+struct
+
+  type context = {
+    mutable stack : node list;
+    text_buffer : Buffer.t;
+    mutable current_preorder : int;
+  }
+
+  let print_node_ptr fmt n =
+    Format.fprintf fmt "<%s>"
+      (if n == nil then "NIL" else
+        if n == dummy then "DUMMY" else
+          "NODE " ^  string_of_int n.preorder)
+
+  let debug_node fmt node =
+    Format.fprintf fmt "{ tag=%s; preorder=%i; data=%S; first_child=%a; next_sibling=%a; parent=%a }"
+      (QName.to_string node.tag)
+      node.preorder
+      node.data
+      print_node_ptr node.first_child
+      print_node_ptr node.next_sibling
+      print_node_ptr node.parent
+
+
+  let debug_ctx fmt ctx =
+    Format.fprintf fmt "Current context: { preorder = %i\n; stack = \n%a\n }\n-------------\n"
+      ctx.current_preorder
+      (Pretty.print_list ~sep:";\n" debug_node) ctx.stack
+
+
+  let push n ctx = ctx.stack <- n :: ctx.stack
+  let pop ctx =
+    match ctx.stack with
+      [] -> failwith "XML parse error"
+    | e :: l -> ctx.stack <- l; e
+
+  let top ctx = match ctx.stack with
+    | [] -> failwith "XML parse error"
+    | e :: _ -> e
+
+  let next ctx =
+    let i = ctx.current_preorder in
+    ctx.current_preorder <- 1 + i;
+    i
+
+  let is_left n = n.next_sibling == dummy
+
+
+  let text_string = QName.to_string QName.text
+  let comment_string = QName.to_string QName.comment
+
+
+  let rec start_element_handler parser_ ctx tag attr_list =
+    do_text parser_ ctx;
+    let parent = top ctx in
+    let n = { tag = QName.of_string tag;
+              kind = Tree.NodeKind.Element;
+              preorder = next ctx;
+              data = "";
+              first_child = dummy;
+              next_sibling = dummy;
+              parent = parent;
+            }
+    in
+    if parent.first_child == dummy then parent.first_child <- n
+    else parent.next_sibling <- n;
+    push n ctx;
+    List.iter (do_attribute parser_ ctx) attr_list
+
+  and do_attribute parser_ ctx (att, value) =
+    let att_tag = QName.to_string (QName.attribute (QName.of_string att)) in
+    start_element_handler parser_ ctx att_tag [];
+    let n = top ctx in
+    n.data <- value;
+    n.kind <- Tree.NodeKind.Attribute;
+    end_element_handler parser_ ctx att_tag
+
+  and consume_closing ctx n =
+    if n.next_sibling != dummy then
+      let _ = pop ctx in consume_closing ctx (top ctx)
+
+  and end_element_handler parser_ ctx _ =
+    do_text parser_ ctx;
+    let node = top ctx in
+    if node.first_child == dummy then node.first_child <- nil
+    else begin
+      node.next_sibling <- nil;
+      consume_closing ctx node
+    end
+
+  and do_text parser_ ctx =
+    if Buffer.length ctx.text_buffer != 0 then
+      let s = Buffer.contents ctx.text_buffer in
+      Buffer.clear  ctx.text_buffer;
+      start_element_handler parser_ ctx text_string [];
+      let node = top ctx in
+      node.data <- s;
+      node.kind <- Tree.NodeKind.Text;
+      end_element_handler parser_ ctx text_string
+
+  and comment_handler parser_ ctx s =
+    do_text parser_ ctx;
+    start_element_handler parser_ ctx comment_string [];
+    let node = top ctx in
+    node.data <- s;
+    node.kind <- Tree.NodeKind.Comment;
+    end_element_handler parser_ ctx comment_string
+
+  and processing_instruction_handler parser_ ctx tag data =
+    do_text parser_ ctx;
+    let pi = QName.to_string
+      (QName.processing_instruction (QName.of_string tag))
+    in
+    start_element_handler parser_ ctx pi [];
+    let node = top ctx in
+    node.data <- data;
+    node.kind <- Tree.NodeKind.ProcessingInstruction;
+    end_element_handler parser_ ctx pi
+
+
+  let character_data_handler _parser ctx text =
+    Buffer.add_string ctx.text_buffer text
+
+  let create_parser () =
+    let ctx = { text_buffer = Buffer.create 512;
+                current_preorder = 0;
+                stack = [] } in
+    let psr = Expat.parser_create ~encoding:None in
+    Expat.set_start_element_handler psr (start_element_handler psr ctx);
+    Expat.set_end_element_handler psr (end_element_handler psr ctx);
+    Expat.set_character_data_handler
+      psr (character_data_handler psr ctx);
+    Expat.set_comment_handler psr (comment_handler psr ctx);
+    Expat.set_processing_instruction_handler psr
+      (processing_instruction_handler psr ctx);
+    push { tag = QName.document;
+           preorder = next ctx;
+           kind = Tree.NodeKind.Document;
+           data = "";
+           first_child = dummy;
+           next_sibling = dummy;
+           parent = nil;
+         } ctx;
+    (psr,
+     fun () ->
+       let node = top ctx in
+       node.next_sibling <- nil;
+       consume_closing ctx node;
+       match ctx.stack with
+         [ root ] ->
+           root.next_sibling <- nil;
+           { root = root;
+             size = ctx.current_preorder
+           }
+       | _ -> raise (Expat.Expat_error Expat.UNCLOSED_TOKEN)
+    )
+
+
+  let parse_string s =
+    let parser_, finalize = create_parser () in
+    Expat.parse parser_ s;
+    finalize ()
+
+  let parse_file fd =
+    let buffer = String.create 4096 in
+    let parser_, finalize = create_parser () in
+    let rec loop () =
+      let read = input fd buffer 0 4096 in
+      if read != 0 then
+        let () = Expat.parse_sub parser_ buffer 0 read in
+        loop ()
+    in loop (); finalize ()
+
+end
+
+
+let load_xml_file = Parser.parse_file
+let load_xml_string = Parser.parse_string
+
+let output_escape_string out s =
+  for i = 0 to String.length s - 1 do
+    match s.[i] with
+    | '<' -> output_string out "&lt;"
+    | '>' -> output_string out "&gt;"
+    | '&' -> output_string out "&amp;"
+    | '"' -> output_string out "&quot;"
+    | '\'' -> output_string out "&apos;"
+    | c -> output_char out c
+  done
+
+
+let rec print_attributes ?(sep=true) out tree_ node =
+  if (node.kind == Tree.NodeKind.Attribute) then
+    let tag = QName.to_string (QName.remove_prefix node.tag) in
+    if sep then output_char out ' ';
+    output_string out tag;
+    output_string out "=\"";
+    output_escape_string out node.data;
+    output_char out '\"';
+    print_attributes out tree_ node.next_sibling
+  else
+    node
+
+let rec print_xml out tree_ node =
+  if node != nil then
+  let () =
+    let open Tree.NodeKind in
+    match node.kind with
+    | Node -> ()
+    | Text -> output_escape_string out node.data
+    | Element | Document ->
+        let tag = QName.to_string node.tag in
+        output_char out '<';
+        output_string out tag;
+        let fchild = print_attributes out tree_ node.first_child in
+        if fchild == nil then output_string out "/>"
+        else begin
+          output_char out '>';
+          print_xml out tree_ fchild;
+          output_string out "</";
+          output_string out tag;
+          output_char out '>'
+        end
+    | Attribute -> ignore (print_attributes ~sep:false out tree_ node)
+    | Comment ->
+        output_string out "<!--";
+        output_string out node.data;
+        output_string out "-->"
+    | ProcessingInstruction ->
+        output_string out "<?";
+        output_string out (QName.to_string (QName.remove_prefix node.tag));
+        output_char out ' ';
+        output_string out node.data;
+        output_string out "?>"
+  in
+  print_xml out tree_ node.next_sibling
+
+let print_xml out tree_ node =
+  let nnode =  { node with next_sibling = nil } in print_xml out tree_ nnode
+
+let root t = t.root
+let size t = t.size
+let first_child _ n = n.first_child
+let next_sibling _ n = n.next_sibling
+let parent _ n = n.parent
+let tag _ n = n.tag
+let data _ n = n.data
+let kind _ n = n.kind
+let preorder _ n = n.preorder
+
+let print_node fmt n = Parser.debug_node fmt n
diff --git a/src/naive_tree.mli b/src/naive_tree.mli
new file mode 100644
index 0000000..2a11164
--- /dev/null
+++ b/src/naive_tree.mli
@@ -0,0 +1,20 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                               TAToo                                 *)
+(*                                                                     *)
+(*                     Kim Nguyen, LRI UMR8623                         *)
+(*                   Université Paris-Sud & CNRS                       *)
+(*                                                                     *)
+(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(*  Recherche Scientifique. All rights reserved.  This file is         *)
+(*  distributed under the terms of the GNU Lesser General Public       *)
+(*  License, with the special exception on linking described in file   *)
+(*  ../LICENSE.                                                        *)
+(*                                                                     *)
+(***********************************************************************)
+
+(*
+  Time-stamp: <Last modified on 2013-04-04 18:44:39 CEST by Kim Nguyen>
+*)
+
+include Tree.S
diff --git a/src/pretty.ml b/src/pretty.ml
new file mode 100644
index 0000000..1927216
--- /dev/null
+++ b/src/pretty.ml
@@ -0,0 +1,151 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                               TAToo                                 *)
+(*                                                                     *)
+(*                     Kim Nguyen, LRI UMR8623                         *)
+(*                   Université Paris-Sud & CNRS                       *)
+(*                                                                     *)
+(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(*  Recherche Scientifique. All rights reserved.  This file is         *)
+(*  distributed under the terms of the GNU Lesser General Public       *)
+(*  License, with the special exception on linking described in file   *)
+(*  ../LICENSE.                                                        *)
+(*                                                                     *)
+(***********************************************************************)
+
+(*
+  Time-stamp: <Last modified on 2013-03-09 10:41:21 CET by Kim Nguyen>
+*)
+
+open Format
+
+exception InvalidUtf8Codepoint of int
+
+let subscripts = "₀₁₂₃₄₅₆₇₈₉"
+let superscripts = "⁰¹²³⁴⁵⁶⁷⁸⁹"
+
+let char_length c =
+  let code = Char.code c in
+    if code <= 0x7f then 1
+    else if 0xc2 <= code && code <= 0xdf then 2
+    else if 0xe0 <= code && code <= 0xef then 3
+    else if 0xf0 <= code && code <= 0xf4 then 4
+    else raise (InvalidUtf8Codepoint code)
+
+
+let next_char s i len =
+  let n = i + char_length s.[i] in
+    if n >= len then -1 else n
+
+let str_len s =
+  let len = String.length s in
+  let rec loop i acc =
+    if i == -1 then acc
+    else loop (next_char s i len) (acc+1)
+  in
+    loop 0 0
+
+let length = str_len
+
+let get_char s i =
+  let len = String.length s in
+  let rec loop j count =
+    if count == i then String.sub s j (char_length s.[j])
+    else loop (next_char s j len) (count+1)
+  in
+    loop 0 0
+
+
+let format_number digits i =
+  let s = string_of_int i in
+  let len = String.length s in
+  let buf = Buffer.create (len*4) in
+    for i = 0 to len - 1 do
+      let d = Char.code s.[i] - Char.code '0' in
+	Buffer.add_string buf (get_char digits d)
+    done;
+    Buffer.contents buf
+
+let rev_explode s =
+  let len = str_len s in
+  let rec loop i acc =
+      if i >= len then acc
+      else
+	loop (i+1) ((get_char s i) :: acc)
+  in
+      loop 0 []
+
+
+let explode s = List.rev (rev_explode s)
+
+let combine_all comp s =
+  let l = rev_explode s in
+  String.concat "" (List.fold_left (fun acc e -> comp::e::acc) [] l)
+
+
+let subscript = format_number subscripts
+let superscript = format_number superscripts
+let down_arrow = "↓"
+let up_arrow = "↑"
+let right_arrow = "→"
+let left_arrow =  "←"
+let epsilon = "ϵ"
+let big_sigma = "∑"
+let cap = "∩"
+let cup = "∪"
+let lnot = "¬"
+let wedge = "∧"
+let vee = "∨"
+let top = "⊤"
+let bottom = "⊥"
+let dummy = "☠"
+let inverse = "⁻¹"
+let double_right_arrow = "⇒"
+let combining_overbar = "\204\133"
+let combining_underbar = "\204\178"
+let combining_stroke = "\204\182"
+let combining_vertical_line = "\226\131\146"
+
+
+let overline s = combine_all combining_overbar s
+let underline s = combine_all combining_underbar s
+let strike s = combine_all combining_stroke s
+
+let padding i = String.make i ' '
+let line i = String.make i '_'
+
+
+
+
+let ppf f fmt s =
+  pp_print_string fmt (f s)
+
+let pp_overline = ppf overline
+let pp_underline = ppf underline
+let pp_strike = ppf strike
+let pp_subscript = ppf subscript
+let pp_superscript = ppf superscript
+let dummy_printer _ () = ()
+
+let pp_print_list ?(sep=dummy_printer) printer fmt l =
+  match l with
+    [] -> ()
+  | [ e ] -> printer fmt e
+  | e :: es -> printer fmt e; List.iter
+    (fun x ->
+      sep fmt ();
+      fprintf fmt "%a" printer x) es
+
+let pp_print_array ?(sep=dummy_printer) printer fmt a =
+  pp_print_list ~sep:sep printer fmt (Array.to_list a)
+
+let print_list ?(sep=" ") printer fmt l =
+  let sep_printer fmt () =
+    pp_print_string fmt sep
+  in
+  pp_print_list ~sep:sep_printer printer fmt l
+
+let print_array ?(sep=" ") printer fmt a =
+  print_list ~sep:sep printer fmt (Array.to_list a)
+
+
diff --git a/src/pretty.mli b/src/pretty.mli
new file mode 100644
index 0000000..9064f8a
--- /dev/null
+++ b/src/pretty.mli
@@ -0,0 +1,57 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                               TAToo                                 *)
+(*                                                                     *)
+(*                     Kim Nguyen, LRI UMR8623                         *)
+(*                   Université Paris-Sud & CNRS                       *)
+(*                                                                     *)
+(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(*  Recherche Scientifique. All rights reserved.  This file is         *)
+(*  distributed under the terms of the GNU Lesser General Public       *)
+(*  License, with the special exception on linking described in file   *)
+(*  ../LICENSE.                                                        *)
+(*                                                                     *)
+(***********************************************************************)
+
+(*
+  Time-stamp: <Last modified on 2013-03-09 10:41:32 CET by Kim Nguyen>
+*)
+
+exception InvalidUtf8Codepoint of int
+
+val subscript : int -> string
+val superscript : int -> string
+val down_arrow : string
+val up_arrow : string
+val right_arrow : string
+val left_arrow : string
+val epsilon : string
+val big_sigma : string
+val cap : string
+val cup : string
+val lnot : string
+val wedge : string
+val vee : string
+val top : string
+val bottom : string
+val dummy : string
+val inverse : string
+val double_right_arrow : string
+val overline : string -> string
+val underline : string -> string
+val strike : string -> string
+val padding : int -> string
+val line : int -> string
+val length : string -> int
+val pp_overline : Format.formatter -> string -> unit
+val pp_underline : Format.formatter -> string -> unit
+val pp_strike : Format.formatter -> string -> unit
+val pp_subscript : Format.formatter -> int -> unit
+val pp_superscript : Format.formatter -> int -> unit
+
+val pp_print_list :
+  ?sep:(Format.formatter -> unit -> unit) -> (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a list -> unit
+val pp_print_array :
+  ?sep:(Format.formatter -> unit -> unit) -> (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a array -> unit
+val print_list : ?sep:string -> (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a list -> unit
+val print_array : ?sep:string -> (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a array -> unit
diff --git a/src/ptset.ml b/src/ptset.ml
new file mode 100644
index 0000000..f9bbd03
--- /dev/null
+++ b/src/ptset.ml
@@ -0,0 +1,381 @@
+(* Original file: *)
+(***********************************************************************)
+(*                                                                     *)
+(*  Copyright (C) Jean-Christophe Filliatre                            *)
+(*                                                                     *)
+(*  This software is free software; you can redistribute it and/or     *)
+(*  modify it under the terms of the GNU Library General Public        *)
+(*  License version 2.1, with the special exception on linking         *)
+(*  described in file http://www.lri.fr/~filliatr/ftp/ocaml/ds/LICENSE *)
+(*                                                                     *)
+(*  This software is distributed in the hope that it will be useful,   *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.               *)
+(*                                                                     *)
+(***********************************************************************)
+
+(*
+  Time-stamp: <Last modified on 2013-03-10 18:18:54 CET by Kim Nguyen>
+*)
+
+(* Modified by Kim Nguyen *)
+(* The Patricia trees are themselves deeply hash-consed. The module
+   provides a Make (and Weak) functor to build hash-consed patricia
+   trees whose elements are Abstract hash-consed values.
+*)
+
+INCLUDE "utils.ml"
+
+include Ptset_sig
+
+module type HConsBuilder =
+  functor (H : Common_sig.HashedType) -> Hcons.S with type data = H.t
+
+module Builder (HCB : HConsBuilder) (H : Hcons.Abstract) :
+  S with type elt = H.t =
+struct
+  type elt = H.t
+
+  type 'a set =
+    | Empty
+    | Leaf of elt
+    | Branch of int * int * 'a * 'a
+
+  module rec Node : Hcons.S with type data = Data.t = HCB(Data)
+                            and Data : Common_sig.HashedType with type t = Node.t set =
+  struct
+    type t =  Node.t set
+    let equal x y =
+      match x,y with
+      | Empty,Empty -> true
+      | Leaf k1, Leaf k2 ->  k1 == k2
+      | Branch(b1,i1,l1,r1), Branch(b2,i2,l2,r2) ->
+          b1 == b2 && i1 == i2 && (Node.equal l1 l2) && (Node.equal r1 r2)
+
+      | (Empty|Leaf _|Branch _), _  -> false
+
+    let hash = function
+    | Empty -> 0
+    | Leaf i -> HASHINT2 (PRIME1, Uid.to_int (H.uid i))
+    | Branch (b,i,l,r) ->
+        HASHINT4(b, i, Uid.to_int l.Node.id, Uid.to_int r.Node.id)
+  end
+
+  include Node
+
+  let empty = Node.make Empty
+
+  let is_empty s = (Node.node s) == Empty
+
+  let branch p m l r = Node.make (Branch(p,m,l,r))
+
+  let leaf k = Node.make (Leaf k)
+
+                            (* To enforce the invariant that a branch contains two non empty
+                               sub-trees *)
+  let branch_ne p m t0 t1 =
+    if (is_empty t0) then t1
+    else if is_empty t1 then t0 else branch p m t0 t1
+
+                            (******** from here on, only use the smart constructors ************)
+
+  let zero_bit k m = (k land m) == 0
+
+  let singleton k = leaf k
+
+  let is_singleton n =
+    match Node.node n with
+      | Leaf _ -> true
+      | Branch _ | Empty -> false
+
+  let mem (k:elt) n =
+    let kid = Uid.to_int (H.uid k) in
+    let rec loop n = match Node.node n with
+    | Empty -> false
+    | Leaf j ->  k == j
+    | Branch (p, _, l, r) -> if kid <= p then loop l else loop r
+    in loop n
+
+  let rec min_elt n = match Node.node n with
+  | Empty -> raise Not_found
+  | Leaf k -> k
+  | Branch (_,_,s,_) -> min_elt s
+
+  let rec max_elt n = match Node.node n with
+  | Empty -> raise Not_found
+  | Leaf k -> k
+  | Branch (_,_,_,t) -> max_elt t
+
+  let elements s =
+    let rec elements_aux acc n = match Node.node n with
+    | Empty -> acc
+    | Leaf k -> k :: acc
+    | Branch (_,_,l,r) -> elements_aux (elements_aux acc r) l
+    in
+    elements_aux [] s
+
+  let mask k m  = (k lor (m-1)) land (lnot m)
+
+  let naive_highest_bit x =
+    assert (x < 256);
+    let rec loop i =
+      if i = 0 then 1 else if x lsr i = 1 then 1 lsl i else loop (i-1)
+    in
+    loop 7
+
+  let hbit = Array.init 256 naive_highest_bit
+  (*
+    external clz : int -> int = "caml_clz" "noalloc"
+    external leading_bit : int -> int = "caml_leading_bit" "noalloc"
+  *)
+  let highest_bit x =
+    try
+      let n = (x) lsr 24 in
+      if n != 0 then  hbit.(n) lsl 24
+      else let n = (x) lsr 16 in if n != 0 then hbit.(n) lsl 16
+        else let n = (x) lsr 8 in if n != 0 then hbit.(n) lsl 8
+          else hbit.(x)
+    with
+      _ -> raise (Invalid_argument ("highest_bit " ^ (string_of_int x)))
+
+  let highest_bit64 x =
+    let n = x lsr 32 in if n != 0 then highest_bit n lsl 32
+      else highest_bit x
+
+  let branching_bit p0 p1 = highest_bit64 (p0 lxor p1)
+
+  let join p0 t0 p1 t1 =
+    let m = branching_bit p0 p1  in
+    let msk = mask p0 m in
+    if zero_bit p0 m then
+    branch_ne msk m t0 t1
+    else
+    branch_ne msk m t1 t0
+
+  let match_prefix k p m = (mask k m) == p
+
+  let add k t =
+    let kid = Uid.to_int (H.uid k) in
+    assert (kid >=0);
+    let rec ins n = match Node.node n with
+    | Empty -> leaf k
+    | Leaf j ->  if j == k then n else join kid (leaf k) (Uid.to_int (H.uid j)) n
+    | Branch (p,m,t0,t1)  ->
+        if match_prefix kid p m then
+        if zero_bit kid m then
+        branch_ne p m (ins t0) t1
+        else
+        branch_ne p m t0 (ins t1)
+        else
+        join kid (leaf k)  p n
+    in
+    ins t
+
+  let remove k t =
+    let kid = Uid.to_int(H.uid k) in
+    let rec rmv n = match Node.node n with
+    | Empty -> empty
+    | Leaf j  -> if  k == j then empty else n
+    | Branch (p,m,t0,t1) ->
+        if match_prefix kid p m then
+        if zero_bit kid m then
+        branch_ne p m (rmv t0) t1
+        else
+        branch_ne p m t0 (rmv t1)
+        else
+        n
+    in
+    rmv t
+
+  (* should run in O(1) thanks to hash consing *)
+
+  let equal a b = Node.equal a b
+
+  let compare a b = (Uid.to_int (Node.uid a)) - (Uid.to_int (Node.uid b))
+
+  let rec merge s t =
+    if equal s t (* This is cheap thanks to hash-consing *)
+    then s
+    else
+    match Node.node s, Node.node t with
+    | Empty, _  -> t
+    | _, Empty  -> s
+    | Leaf k, _ -> add k t
+    | _, Leaf k -> add k s
+    | Branch (p,m,s0,s1), Branch (q,n,t0,t1) ->
+        if m == n && match_prefix q p m then
+        branch p  m  (merge s0 t0) (merge s1 t1)
+        else if m > n && match_prefix q p m then
+        if zero_bit q m then
+        branch_ne p m (merge s0 t) s1
+        else
+        branch_ne p m s0 (merge s1 t)
+        else if m < n && match_prefix p q n then
+        if zero_bit p n then
+        branch_ne q n (merge s t0) t1
+        else
+        branch_ne q n t0 (merge s t1)
+        else
+                                  (* The prefixes disagree. *)
+        join p s q t
+
+
+
+
+  let rec subset s1 s2 = (equal s1 s2) ||
+    match (Node.node s1,Node.node s2) with
+    | Empty, _ -> true
+    | _, Empty -> false
+    | Leaf k1, _ -> mem k1 s2
+    | Branch _, Leaf _ -> false
+    | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
+        if m1 == m2 && p1 == p2 then
+        subset l1 l2 && subset r1 r2
+        else if m1 < m2 && match_prefix p1 p2 m2 then
+        if zero_bit p1 m2 then
+        subset l1 l2 && subset r1 l2
+        else
+        subset l1 r2 && subset r1 r2
+        else
+        false
+
+
+  let union s1 s2 = merge s1 s2
+                            (* Todo replace with e Memo Module *)
+
+  let rec inter s1 s2 =
+    if equal s1 s2
+    then s1
+    else
+    match (Node.node s1,Node.node s2) with
+    | Empty, _ -> empty
+    | _, Empty -> empty
+    | Leaf k1, _ -> if mem k1 s2 then s1 else empty
+    | _, Leaf k2 -> if mem k2 s1 then s2 else empty
+    | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
+        if m1 == m2 && p1 == p2 then
+        merge (inter l1 l2)  (inter r1 r2)
+        else if m1 > m2 && match_prefix p2 p1 m1 then
+        inter (if zero_bit p2 m1 then l1 else r1) s2
+        else if m1 < m2 && match_prefix p1 p2 m2 then
+        inter s1 (if zero_bit p1 m2 then l2 else r2)
+        else
+        empty
+
+  let rec diff s1 s2 =
+    if equal s1 s2
+    then empty
+    else
+    match (Node.node s1,Node.node s2) with
+    | Empty, _ -> empty
+    | _, Empty -> s1
+    | Leaf k1, _ -> if mem k1 s2 then empty else s1
+    | _, Leaf k2 -> remove k2 s1
+    | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
+        if m1 == m2 && p1 == p2 then
+        merge (diff l1 l2) (diff r1 r2)
+        else if m1 > m2 && match_prefix p2 p1 m1 then
+        if zero_bit p2 m1 then
+        merge (diff l1 s2) r1
+        else
+        merge l1 (diff r1 s2)
+        else if m1 < m2 && match_prefix p1 p2 m2 then
+        if zero_bit p1 m2 then diff s1 l2 else diff s1 r2
+        else
+        s1
+
+
+  (*s All the following operations ([cardinal], [iter], [fold], [for_all],
+    [exists], [filter], [partition], [choose], [elements]) are
+    implemented as for any other kind of binary trees. *)
+
+  let rec cardinal n = match Node.node n with
+  | Empty -> 0
+  | Leaf _ -> 1
+  | Branch (_,_,t0,t1) -> cardinal t0 + cardinal t1
+
+  let rec iter f n = match Node.node n with
+  | Empty -> ()
+  | Leaf k -> f k
+  | Branch (_,_,t0,t1) -> iter f t0; iter f t1
+
+  let rec fold f s accu = match Node.node s with
+  | Empty -> accu
+  | Leaf k -> f k accu
+  | Branch (_,_,t0,t1) -> fold f t0 (fold f t1 accu)
+
+
+  let rec for_all p n = match Node.node n with
+  | Empty -> true
+  | Leaf k -> p k
+  | Branch (_,_,t0,t1) -> for_all p t0 && for_all p t1
+
+  let rec exists p n = match Node.node n with
+  | Empty -> false
+  | Leaf k -> p k
+  | Branch (_,_,t0,t1) -> exists p t0 || exists p t1
+
+  let rec filter pr n = match Node.node n with
+  | Empty -> empty
+  | Leaf k -> if pr k then n else empty
+  | Branch (p,m,t0,t1) -> branch_ne p m (filter pr t0) (filter pr t1)
+
+  let partition p s =
+    let rec part (t,f as acc) n = match Node.node n with
+    | Empty -> acc
+    | Leaf k -> if p k then (add k t, f) else (t, add k f)
+    | Branch (_,_,t0,t1) -> part (part acc t0) t1
+    in
+    part (empty, empty) s
+
+  let rec choose n = match Node.node n with
+  | Empty -> raise Not_found
+  | Leaf k -> k
+  | Branch (_, _,t0,_) -> choose t0   (* we know that [t0] is non-empty *)
+
+
+  let split x s =
+    let coll k (l, b, r) =
+      if k < x then add k l, b, r
+      else if k > x then l, b, add k r
+      else l, true, r
+    in
+    fold coll s (empty, false, empty)
+
+  (*s Additional functions w.r.t to [Set.S]. *)
+
+  let rec intersect s1 s2 = (equal s1 s2) ||
+    match (Node.node s1,Node.node s2) with
+    | Empty, _ -> false
+    | _, Empty -> false
+    | Leaf k1, _ -> mem k1 s2
+    | _, Leaf k2 -> mem k2 s1
+    | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
+        if m1 == m2 && p1 == p2 then
+        intersect l1 l2 || intersect r1 r2
+        else if m1 > m2 && match_prefix p2 p1 m1 then
+        intersect (if zero_bit p2 m1 then l1 else r1) s2
+        else if m1 < m2 && match_prefix p1 p2 m2 then
+        intersect s1 (if zero_bit p1 m2 then l2 else r2)
+        else
+        false
+
+
+  let from_list l = List.fold_left (fun acc e -> add e acc) empty l
+
+
+end
+
+module Make = Builder(Hcons.Make)
+module Weak = Builder(Hcons.Weak)
+
+module PosInt
+  =
+struct
+  include Make(Hcons.PosInt)
+  let print ppf s =
+    Format.pp_print_string ppf "{ ";
+    iter (fun i -> Format.fprintf ppf "%i " i) s;
+    Format.pp_print_string ppf "}";
+    Format.pp_print_flush ppf ()
+end
diff --git a/src/ptset.mli b/src/ptset.mli
new file mode 100644
index 0000000..f4f53f7
--- /dev/null
+++ b/src/ptset.mli
@@ -0,0 +1,33 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                               TAToo                                 *)
+(*                                                                     *)
+(*                     Kim Nguyen, LRI UMR8623                         *)
+(*                   Université Paris-Sud & CNRS                       *)
+(*                                                                     *)
+(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(*  Recherche Scientifique. All rights reserved.  This file is         *)
+(*  distributed under the terms of the GNU Lesser General Public       *)
+(*  License, with the special exception on linking described in file   *)
+(*  ../LICENSE.                                                        *)
+(*                                                                     *)
+(***********************************************************************)
+
+(*
+  Time-stamp: <Last modified on 2013-03-04 22:42:37 CET by Kim Nguyen>
+*)
+
+include module type of Ptset_sig
+
+module Make (H : Hcons.Abstract) : S with type elt = H.t
+(** Builds an implementation of hashconsed sets of hashconsed elements.
+    See {!Hcons.Make}.
+*)
+
+module Weak (H : Hcons.Abstract) : S with type elt = H.t
+(** Builds an implementation of hashconsed sets of hashconsed elements
+    with weak internal storage. See {!Hcons.Weak}.
+*)
+
+module PosInt : S with type elt = int
+(** Implementation of hashconsed sets of positive integers *)
diff --git a/src/ptset_sig.ml b/src/ptset_sig.ml
new file mode 100644
index 0000000..f37f6ba
--- /dev/null
+++ b/src/ptset_sig.ml
@@ -0,0 +1,24 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                               TAToo                                 *)
+(*                                                                     *)
+(*                     Kim Nguyen, LRI UMR8623                         *)
+(*                   Université Paris-Sud & CNRS                       *)
+(*                                                                     *)
+(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(*  Recherche Scientifique. All rights reserved.  This file is         *)
+(*  distributed under the terms of the GNU Lesser General Public       *)
+(*  License, with the special exception on linking described in file   *)
+(*  ../LICENSE.                                                        *)
+(*                                                                     *)
+(***********************************************************************)
+
+(*
+  Time-stamp: <Last modified on 2013-03-04 23:32:36 CET by Kim Nguyen>
+*)
+
+module type S =
+sig
+  include Hcons.S
+  include Common_sig.Set with type t := t
+end
diff --git a/src/qName.ml b/src/qName.ml
new file mode 100644
index 0000000..4a3aac4
--- /dev/null
+++ b/src/qName.ml
@@ -0,0 +1,47 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                               TAToo                                 *)
+(*                                                                     *)
+(*                     Kim Nguyen, LRI UMR8623                         *)
+(*                   Université Paris-Sud & CNRS                       *)
+(*                                                                     *)
+(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(*  Recherche Scientifique. All rights reserved.  This file is         *)
+(*  distributed under the terms of the GNU Lesser General Public       *)
+(*  License, with the special exception on linking described in file   *)
+(*  ../LICENSE.                                                        *)
+(*                                                                     *)
+(***********************************************************************)
+
+(*
+  Time-stamp: <Last modified on 2013-03-10 23:05:56 CET by Kim Nguyen>
+*)
+
+include Hcons.Make (struct
+  include String
+  let hash s = Hashtbl.hash s
+  let equal s1 s2 = s1 = s2
+end)
+
+let print pp s = Format.fprintf pp "%s" s.node
+
+let of_string = make
+let to_string = node
+
+let document = of_string "#document"
+let text = of_string "#text"
+let comment = of_string "#comment"
+let nil = of_string "#"
+
+let attribute t = of_string ( "@" ^ (to_string t))
+let processing_instruction t = of_string ( "?" ^ (to_string t))
+
+let remove_prefix t =
+  let s = to_string t in
+  let lens = String.length s in
+  if lens == 0 then t
+  else
+    if s.[0] == '@' || s.[0] == '?' then
+      of_string (String.sub s 1 (lens-1))
+    else
+      t
diff --git a/src/qName.mli b/src/qName.mli
new file mode 100644
index 0000000..978ba3c
--- /dev/null
+++ b/src/qName.mli
@@ -0,0 +1,70 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                               TAToo                                 *)
+(*                                                                     *)
+(*                     Kim Nguyen, LRI UMR8623                         *)
+(*                   Université Paris-Sud & CNRS                       *)
+(*                                                                     *)
+(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(*  Recherche Scientifique. All rights reserved.  This file is         *)
+(*  distributed under the terms of the GNU Lesser General Public       *)
+(*  License, with the special exception on linking described in file   *)
+(*  ../LICENSE.                                                        *)
+(*                                                                     *)
+(***********************************************************************)
+
+(*
+  Time-stamp: <Last modified on 2013-03-10 23:02:12 CET by Kim Nguyen>
+*)
+
+(** Implementation of qualified names as hashconsed strings *)
+
+include Hcons.S with type data = string
+include Common_sig.Printable with type t := t
+
+
+val of_string : string -> t
+(** Utility function, equivalent to [make] *)
+
+val to_string : t -> string
+(** Utility function, equivalent to [node] *)
+
+
+(** Special constants, that denote the QName of nodes that are not
+    elements (using the nodeValue property of DOM for such nodes.
+*)
+
+val document : t
+(** Represents the QName of a document node. Equivalent to
+    [of_string "#document"]
+*)
+
+val text : t
+(** Represents the QName of a text node. Equivalent to
+    [of_string "#text"]
+*)
+
+val comment : t
+(** Represents the QName of a comment node. Equivalent to
+    [of_string "#comment"]
+*)
+
+val nil : t
+(** Represents the QName of a nil node. Equivalent to
+    [of_string "#"]
+*)
+
+val attribute : t -> t
+(** Adds a prefix character (@) to distinguish the name
+    from an element name
+*)
+
+val processing_instruction : t -> t
+(** Adds a prefix character (?) to distinguish the name
+    from an element name
+*)
+
+val remove_prefix : t -> t
+(** Removes the prefix of the qname given as argument. Does not
+    do anything if there is no prefix.
+*)
diff --git a/src/qNameSet.ml b/src/qNameSet.ml
new file mode 100644
index 0000000..d895ff3
--- /dev/null
+++ b/src/qNameSet.ml
@@ -0,0 +1,49 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                               TAToo                                 *)
+(*                                                                     *)
+(*                     Kim Nguyen, LRI UMR8623                         *)
+(*                   Université Paris-Sud & CNRS                       *)
+(*                                                                     *)
+(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(*  Recherche Scientifique. All rights reserved.  This file is         *)
+(*  distributed under the terms of the GNU Lesser General Public       *)
+(*  License, with the special exception on linking described in file   *)
+(*  ../LICENSE.                                                        *)
+(*                                                                     *)
+(***********************************************************************)
+
+(*
+  Time-stamp: <Last modified on 2013-03-09 17:54:35 CET by Kim Nguyen>
+*)
+
+include FiniteCofinite.Make(Ptset.Make(QName))
+
+let print_finite fmt e conv =
+  Format.fprintf fmt "{";
+  Pretty.print_list ~sep:"," QName.print fmt (conv e);
+  Format.fprintf fmt "}"
+
+let printer fmt e test conv inv is_any =
+  if test e then print_finite fmt e conv
+  else
+    let () = Format.fprintf fmt "%s" Pretty.big_sigma in
+    if not (is_any e) then begin Format.fprintf fmt "-";print_finite fmt (inv e) conv end
+
+let print fmt e = printer fmt e is_finite elements complement is_any
+
+let specials = [ QName.document; QName.text; QName.text ]
+let notstar = from_list specials
+let star = diff any notstar
+let node = any
+let text = singleton QName.text
+
+module Weak =
+struct
+  include FiniteCofinite.Weak(Ptset.Weak(QName))
+  let print fmt e =  printer fmt e is_finite elements complement is_any
+  let notstar = from_list specials
+  let star = diff any notstar
+  let node = any
+  let text = singleton QName.text
+end
diff --git a/src/qNameSet.mli b/src/qNameSet.mli
new file mode 100644
index 0000000..132d834
--- /dev/null
+++ b/src/qNameSet.mli
@@ -0,0 +1,36 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                               TAToo                                 *)
+(*                                                                     *)
+(*                     Kim Nguyen, LRI UMR8623                         *)
+(*                   Université Paris-Sud & CNRS                       *)
+(*                                                                     *)
+(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(*  Recherche Scientifique. All rights reserved.  This file is         *)
+(*  distributed under the terms of the GNU Lesser General Public       *)
+(*  License, with the special exception on linking described in file   *)
+(*  ../LICENSE.                                                        *)
+(*                                                                     *)
+(***********************************************************************)
+
+(*
+  Time-stamp: <Last modified on 2013-03-09 17:53:53 CET by Kim Nguyen>
+*)
+
+(** Implementation of sets of Qualified Names that can be finite
+    or cofinite *)
+
+include FiniteCofinite.S with type elt = QName.t
+include Common_sig.Printable with type t := t
+val star : t
+val text : t
+val node : t
+
+module Weak :
+sig
+  include FiniteCofinite.S with type elt = QName.t
+  include Common_sig.Printable with type t := t
+  val star : t
+  val text : t
+  val node : t
+end
diff --git a/src/state.ml b/src/state.ml
new file mode 100644
index 0000000..bb7a063
--- /dev/null
+++ b/src/state.ml
@@ -0,0 +1,40 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                               TAToo                                 *)
+(*                                                                     *)
+(*                     Kim Nguyen, LRI UMR8623                         *)
+(*                   Université Paris-Sud & CNRS                       *)
+(*                                                                     *)
+(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(*  Recherche Scientifique. All rights reserved.  This file is         *)
+(*  distributed under the terms of the GNU Lesser General Public       *)
+(*  License, with the special exception on linking described in file   *)
+(*  ../LICENSE.                                                        *)
+(*                                                                     *)
+(***********************************************************************)
+
+(*
+  Time-stamp: <Last modified on 2013-04-04 18:45:59 CEST by Kim Nguyen>
+*)
+
+open Format
+
+type t = int
+let make =
+  let id = ref ~-1 in
+    fun () -> incr id; !id
+
+let compare = (-)
+
+let equal = (==)
+
+external hash : t -> int =  "%identity"
+
+let print fmt x = fprintf fmt "q%a" Pretty.pp_subscript x
+
+let dump fmt x = print fmt x
+
+let check x =
+  if x < 0 then failwith (Printf.sprintf "State: Assertion %i < 0 failed" x)
+
+let dummy = max_int
diff --git a/src/state.mli b/src/state.mli
new file mode 100644
index 0000000..89d67cd
--- /dev/null
+++ b/src/state.mli
@@ -0,0 +1,31 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                               TAToo                                 *)
+(*                                                                     *)
+(*                     Kim Nguyen, LRI UMR8623                         *)
+(*                   Université Paris-Sud & CNRS                       *)
+(*                                                                     *)
+(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(*  Recherche Scientifique. All rights reserved.  This file is         *)
+(*  distributed under the terms of the GNU Lesser General Public       *)
+(*  License, with the special exception on linking described in file   *)
+(*  ../LICENSE.                                                        *)
+(*                                                                     *)
+(***********************************************************************)
+
+(*
+  Time-stamp: <Last modified on 2013-03-04 23:02:21 CET by Kim Nguyen>
+*)
+
+(** Implementation of states *)
+
+include Common_sig.Type with type t = int
+
+val make : unit -> t
+(** Generate a fresh state *)
+
+val dummy : t
+(** Dummy state that can never be returned by [make ()] *)
+
+val print : Format.formatter -> t -> unit
+(** Pretty printer *)
diff --git a/src/stateSet.ml b/src/stateSet.ml
new file mode 100644
index 0000000..2fec234
--- /dev/null
+++ b/src/stateSet.ml
@@ -0,0 +1,26 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                               TAToo                                 *)
+(*                                                                     *)
+(*                     Kim Nguyen, LRI UMR8623                         *)
+(*                   Université Paris-Sud & CNRS                       *)
+(*                                                                     *)
+(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(*  Recherche Scientifique. All rights reserved.  This file is         *)
+(*  distributed under the terms of the GNU Lesser General Public       *)
+(*  License, with the special exception on linking described in file   *)
+(*  ../LICENSE.                                                        *)
+(*                                                                     *)
+(***********************************************************************)
+
+(*
+  Time-stamp: <Last modified on 2013-04-04 18:46:16 CEST by Kim Nguyen>
+*)
+
+open Format
+
+include Ptset.Make (Hcons.PosInt)
+
+let print ppf s =
+  fprintf ppf "{ %a }"
+    (Pretty.print_list ~sep:" " (State.print)) (elements s)
diff --git a/src/stateSet.mli b/src/stateSet.mli
new file mode 100644
index 0000000..1a9c237
--- /dev/null
+++ b/src/stateSet.mli
@@ -0,0 +1,24 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                               TAToo                                 *)
+(*                                                                     *)
+(*                     Kim Nguyen, LRI UMR8623                         *)
+(*                   Université Paris-Sud & CNRS                       *)
+(*                                                                     *)
+(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(*  Recherche Scientifique. All rights reserved.  This file is         *)
+(*  distributed under the terms of the GNU Lesser General Public       *)
+(*  License, with the special exception on linking described in file   *)
+(*  ../LICENSE.                                                        *)
+(*                                                                     *)
+(***********************************************************************)
+
+(*
+  Time-stamp: <Last modified on 2013-04-04 18:41:31 CEST by Kim Nguyen>
+*)
+
+(** Implementation of sets of states *)
+include Ptset.S with type elt = int
+
+val print : Format.formatter -> t -> unit
+(** Pretty printer *)
diff --git a/src/tatoo.ml b/src/tatoo.ml
index d6a1986..1b8c17d 100644
--- a/src/tatoo.ml
+++ b/src/tatoo.ml
@@ -14,12 +14,12 @@
 (***********************************************************************)
 
 (*
-  Time-stamp: <Last modified on 2013-03-13 21:29:17 CET by Kim Nguyen>
+  Time-stamp: <Last modified on 2013-04-04 18:45:43 CEST by Kim Nguyen>
 *)
 
 let doc =
   let fd = open_in Sys.argv.(1) in
-  let d = Tree.Naive.load_xml_file fd in
+  let d = Naive_tree.load_xml_file fd in
   close_in fd; d
 
 
@@ -34,16 +34,16 @@ open Format
 
 let () =
   fprintf err_formatter "Query: %a\n%!" Xpath.Ast.print_path query;
-  fprintf err_formatter "Automata: %a\n%!" Auto.Ata.print auto;
+  fprintf err_formatter "Automata: %a\n%!" Ata.print auto;
   fprintf err_formatter "Evaluating automaton:\n%!";
-  let module Naive = Auto.Eval.Make(Tree.Naive) in
+  let module Naive = Eval.Make(Naive_tree) in
   let t1 = Unix.gettimeofday() in
-  let results = Naive.eval auto doc (Tree.Naive.root doc) in
+  let results = Naive.eval auto doc (Naive_tree.root doc) in
   let teval = (Unix.gettimeofday () -. t1) *. 1000. in
   let t1 = Unix.gettimeofday () in
   output_string stdout "<xml_result>\n";
   List.iter (fun n ->
-    Tree.Naive.print_xml stdout doc n;
+    Naive_tree.print_xml stdout doc n;
     output_char stdout '\n'
   ) results;
   output_string stdout "</xml_result>\n";
diff --git a/src/tree.ml b/src/tree.ml
new file mode 100644
index 0000000..9ef78ce
--- /dev/null
+++ b/src/tree.ml
@@ -0,0 +1,115 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                               TAToo                                 *)
+(*                                                                     *)
+(*                     Kim Nguyen, LRI UMR8623                         *)
+(*                   Université Paris-Sud & CNRS                       *)
+(*                                                                     *)
+(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(*  Recherche Scientifique. All rights reserved.  This file is         *)
+(*  distributed under the terms of the GNU Lesser General Public       *)
+(*  License, with the special exception on linking described in file   *)
+(*  ../LICENSE.                                                        *)
+(*                                                                     *)
+(***********************************************************************)
+
+(*
+  Time-stamp: <Last modified on 2013-04-04 18:40:39 CEST by Kim Nguyen>
+*)
+
+(** The different kind of XML nodes and utility functions *)
+
+module NodeKind =
+  struct
+    type t =
+        Document | Element | Text | Comment | Attribute | ProcessingInstruction | Node
+
+    let to_string =
+      function
+    Document -> "document"
+    | Element -> "element"
+    | Attribute -> "attribute"
+    | Text -> "text"
+    | Comment -> "comment"
+    | ProcessingInstruction -> "processing-instruction"
+    | Node -> "node"
+
+    let print ppf k = Format.fprintf ppf "%s" (to_string k)
+
+
+    let is_a k1 k2 =
+      k1 == Node || k2 == Node || k1 == k2
+end
+
+
+(** Signatures for trees *)
+
+module type S =
+sig
+  type node
+  (** The type of a tree node *)
+
+  type t
+  (** The type of trees *)
+
+  val size : t -> int
+  (** Return the number of nodes *)
+
+  val nil : node
+  (** Nil node, denoting the first/second child of a leaf or the parent of
+      the root *)
+
+  val dummy : node
+  (** Dummy node that is guaranteed to never occur in any tree *)
+
+  val load_xml_file : in_channel -> t
+  (** Takes a file descriptor and returns the XML data stored in the
+      corresponding file. Start at the current position in the file
+      descriptor (which is not necessarily the begining of file)
+  *)
+
+  val load_xml_string : string -> t
+  (** Loads XML data stored in a string *)
+
+  val print_xml : out_channel -> t -> node -> unit
+  (** Outputs the tree as an XML document on the given output_channel *)
+
+  val root : t -> node
+  (** Returns the root of the tree *)
+
+  val first_child : t -> node -> node
+  (** [first_child t n] returns the first child of node [n] in tree [t].
+      Returns [nil] if [n] is a leaf. Returns [nil] if [n == nil].
+  *)
+
+  val next_sibling : t -> node -> node
+  (** [next_sibling t n] returns the next_sibling of node [n] in tree [t].
+      Returns [nil] if [n] is the last child of a node.
+      Returns [nil] if [n == nil].
+  *)
+
+  val parent : t -> node -> node
+  (** [next_sibling t n] returns the parent of node [n] in tree [t].
+      Returns [nil] if [n] is the root of the tree.
+      Returns [nil] if [n == nil].
+  *)
+
+  val tag : t -> node -> QName.t
+  (** Returns the label of a given node *)
+
+  val data : t -> node -> string
+  (** Returns the character data associated with a node.
+      The only node having character data are those whose label is
+      QName.text, QName.cdata_section or QName.comment
+  *)
+
+  val kind : t -> node -> NodeKind.t
+  (** Returns the kind of the given node *)
+
+  val preorder : t -> node -> int
+  (** Returns the position of a node in pre-order in the tree. The
+    root has preorder 0. [nil] has pre-order [-1].
+  *)
+
+  val print_node : Format.formatter -> node -> unit
+end
diff --git a/src/tree.mlpack b/src/tree.mlpack
deleted file mode 100644
index 6dd2e12..0000000
--- a/src/tree.mlpack
+++ /dev/null
@@ -1,3 +0,0 @@
-tree/Naive
-tree/Sig
-tree/Common
diff --git a/src/tree/common.ml b/src/tree/common.ml
deleted file mode 100644
index 099d751..0000000
--- a/src/tree/common.ml
+++ /dev/null
@@ -1,40 +0,0 @@
-(***********************************************************************)
-(*                                                                     *)
-(*                               TAToo                                 *)
-(*                                                                     *)
-(*                     Kim Nguyen, LRI UMR8623                         *)
-(*                   Université Paris-Sud & CNRS                       *)
-(*                                                                     *)
-(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(*  Recherche Scientifique. All rights reserved.  This file is         *)
-(*  distributed under the terms of the GNU Lesser General Public       *)
-(*  License, with the special exception on linking described in file   *)
-(*  ../LICENSE.                                                        *)
-(*                                                                     *)
-(***********************************************************************)
-
-(*
-  Time-stamp: <Last modified on 2013-03-11 00:11:53 CET by Kim Nguyen>
-*)
-
-module NodeKind =
-  struct
-    type t =
-        Document | Element | Text | Comment | Attribute | ProcessingInstruction
-      | Node
-
-    let to_string =
-      function
-    Document -> "document"
-    | Element -> "element"
-    | Attribute -> "attribute"
-    | Text -> "text"
-    | Comment -> "comment"
-    | ProcessingInstruction -> "processing-instruction"
-    | Node -> "node"
-    let print ppf k = Format.fprintf ppf "%s" (to_string k)
-
-
-    let is_a k1 k2 =
-      k1 == Node || k2 == Node || k1 == k2
-end
diff --git a/src/tree/naive.ml b/src/tree/naive.ml
deleted file mode 100644
index fa14d93..0000000
--- a/src/tree/naive.ml
+++ /dev/null
@@ -1,314 +0,0 @@
-(***********************************************************************)
-(*                                                                     *)
-(*                               TAToo                                 *)
-(*                                                                     *)
-(*                     Kim Nguyen, LRI UMR8623                         *)
-(*                   Université Paris-Sud & CNRS                       *)
-(*                                                                     *)
-(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(*  Recherche Scientifique. All rights reserved.  This file is         *)
-(*  distributed under the terms of the GNU Lesser General Public       *)
-(*  License, with the special exception on linking described in file   *)
-(*  ../LICENSE.                                                        *)
-(*                                                                     *)
-(***********************************************************************)
-
-(*
-  Time-stamp: <Last modified on 2013-03-13 18:47:18 CET by Kim Nguyen>
-*)
-open Utils
-
-type node = {
-  tag : QName.t;
-  preorder : int;
-  mutable kind : Common.NodeKind.t;
-  mutable data : string;
-  mutable first_child : node;
-  mutable next_sibling : node;
-  mutable parent: node;
-}
-
-
-
-let rec nil = {
-  tag = QName.nil;
-  kind = Common.NodeKind.Element;
-  preorder = -1;
-  data = "";
-  first_child = nil;
-  next_sibling = nil;
-  parent = nil;
-}
-
-let dummy_tag = QName.of_string "#dummy"
-let rec dummy = {
-  tag = dummy_tag;
-  kind = Common.NodeKind.Element;
-  preorder = -1;
-  data = "";
-  first_child = dummy;
-  next_sibling = dummy;
-  parent = dummy;
-}
-
-
-type t = {
-  root : node;
-  size : int;
-  (* TODO add other intersting stuff *)
-}
-
-
-
-module Parser =
-struct
-
-  type context = {
-    mutable stack : node list;
-    text_buffer : Buffer.t;
-    mutable current_preorder : int;
-  }
-
-  let print_node_ptr fmt n =
-    Format.fprintf fmt "<%s>"
-      (if n == nil then "NIL" else
-        if n == dummy then "DUMMY" else
-          "NODE " ^  string_of_int n.preorder)
-
-  let debug_node fmt node =
-    Format.fprintf fmt "{ tag=%s; preorder=%i; data=%S; first_child=%a; next_sibling=%a; parent=%a }"
-      (QName.to_string node.tag)
-      node.preorder
-      node.data
-      print_node_ptr node.first_child
-      print_node_ptr node.next_sibling
-      print_node_ptr node.parent
-
-
-  let debug_ctx fmt ctx =
-    Format.fprintf fmt "Current context: { preorder = %i\n; stack = \n%a\n }\n-------------\n"
-      ctx.current_preorder
-      (Pretty.print_list ~sep:";\n" debug_node) ctx.stack
-
-
-  let push n ctx = ctx.stack <- n :: ctx.stack
-  let pop ctx =
-    match ctx.stack with
-      [] -> failwith "XML parse error"
-    | e :: l -> ctx.stack <- l; e
-
-  let top ctx = match ctx.stack with
-    | [] -> failwith "XML parse error"
-    | e :: _ -> e
-
-  let next ctx =
-    let i = ctx.current_preorder in
-    ctx.current_preorder <- 1 + i;
-    i
-
-  let is_left n = n.next_sibling == dummy
-
-
-  let text_string = QName.to_string QName.text
-  let comment_string = QName.to_string QName.comment
-
-
-  let rec start_element_handler parser_ ctx tag attr_list =
-    do_text parser_ ctx;
-    let parent = top ctx in
-    let n = { tag = QName.of_string tag;
-              kind = Common.NodeKind.Element;
-              preorder = next ctx;
-              data = "";
-              first_child = dummy;
-              next_sibling = dummy;
-              parent = parent;
-            }
-    in
-    if parent.first_child == dummy then parent.first_child <- n
-    else parent.next_sibling <- n;
-    push n ctx;
-    List.iter (do_attribute parser_ ctx) attr_list
-
-  and do_attribute parser_ ctx (att, value) =
-    let att_tag = QName.to_string (QName.attribute (QName.of_string att)) in
-    start_element_handler parser_ ctx att_tag [];
-    let n = top ctx in
-    n.data <- value;
-    n.kind <- Common.NodeKind.Attribute;
-    end_element_handler parser_ ctx att_tag
-
-  and consume_closing ctx n =
-    if n.next_sibling != dummy then
-      let _ = pop ctx in consume_closing ctx (top ctx)
-
-  and end_element_handler parser_ ctx _ =
-    do_text parser_ ctx;
-    let node = top ctx in
-    if node.first_child == dummy then node.first_child <- nil
-    else begin
-      node.next_sibling <- nil;
-      consume_closing ctx node
-    end
-
-  and do_text parser_ ctx =
-    if Buffer.length ctx.text_buffer != 0 then
-      let s = Buffer.contents ctx.text_buffer in
-      Buffer.clear  ctx.text_buffer;
-      start_element_handler parser_ ctx text_string [];
-      let node = top ctx in
-      node.data <- s;
-      node.kind <- Common.NodeKind.Text;
-      end_element_handler parser_ ctx text_string
-
-  and comment_handler parser_ ctx s =
-    do_text parser_ ctx;
-    start_element_handler parser_ ctx comment_string [];
-    let node = top ctx in
-    node.data <- s;
-    node.kind <- Common.NodeKind.Comment;
-    end_element_handler parser_ ctx comment_string
-
-  and processing_instruction_handler parser_ ctx tag data =
-    do_text parser_ ctx;
-    let pi = QName.to_string
-      (QName.processing_instruction (QName.of_string tag))
-    in
-    start_element_handler parser_ ctx pi [];
-    let node = top ctx in
-    node.data <- data;
-    node.kind <- Common.NodeKind.ProcessingInstruction;
-    end_element_handler parser_ ctx pi
-
-
-  let character_data_handler _parser ctx text =
-    Buffer.add_string ctx.text_buffer text
-
-  let create_parser () =
-    let ctx = { text_buffer = Buffer.create 512;
-                current_preorder = 0;
-                stack = [] } in
-    let psr = Expat.parser_create ~encoding:None in
-    Expat.set_start_element_handler psr (start_element_handler psr ctx);
-    Expat.set_end_element_handler psr (end_element_handler psr ctx);
-    Expat.set_character_data_handler
-      psr (character_data_handler psr ctx);
-    Expat.set_comment_handler psr (comment_handler psr ctx);
-    Expat.set_processing_instruction_handler psr
-      (processing_instruction_handler psr ctx);
-    push { tag = QName.document;
-           preorder = next ctx;
-           kind = Common.NodeKind.Document;
-           data = "";
-           first_child = dummy;
-           next_sibling = dummy;
-           parent = nil;
-         } ctx;
-    (psr,
-     fun () ->
-       let node = top ctx in
-       node.next_sibling <- nil;
-       consume_closing ctx node;
-       match ctx.stack with
-         [ root ] ->
-           root.next_sibling <- nil;
-           { root = root;
-             size = ctx.current_preorder
-           }
-       | _ -> raise (Expat.Expat_error Expat.UNCLOSED_TOKEN)
-    )
-
-
-  let parse_string s =
-    let parser_, finalize = create_parser () in
-    Expat.parse parser_ s;
-    finalize ()
-
-  let parse_file fd =
-    let buffer = String.create 4096 in
-    let parser_, finalize = create_parser () in
-    let rec loop () =
-      let read = input fd buffer 0 4096 in
-      if read != 0 then
-        let () = Expat.parse_sub parser_ buffer 0 read in
-        loop ()
-    in loop (); finalize ()
-
-end
-
-
-let load_xml_file = Parser.parse_file
-let load_xml_string = Parser.parse_string
-
-let output_escape_string out s =
-  for i = 0 to String.length s - 1 do
-    match s.[i] with
-    | '<' -> output_string out "&lt;"
-    | '>' -> output_string out "&gt;"
-    | '&' -> output_string out "&amp;"
-    | '"' -> output_string out "&quot;"
-    | '\'' -> output_string out "&apos;"
-    | c -> output_char out c
-  done
-
-
-let rec print_attributes ?(sep=true) out tree_ node =
-  if (node.kind == Common.NodeKind.Attribute) then
-    let tag = QName.to_string (QName.remove_prefix node.tag) in
-    if sep then output_char out ' ';
-    output_string out tag;
-    output_string out "=\"";
-    output_escape_string out node.data;
-    output_char out '\"';
-    print_attributes out tree_ node.next_sibling
-  else
-    node
-
-let rec print_xml out tree_ node =
-  if node != nil then
-  let () =
-    let open Common.NodeKind in
-    match node.kind with
-    | Node -> ()
-    | Text -> output_escape_string out node.data
-    | Element | Document ->
-        let tag = QName.to_string node.tag in
-        output_char out '<';
-        output_string out tag;
-        let fchild = print_attributes out tree_ node.first_child in
-        if fchild == nil then output_string out "/>"
-        else begin
-          output_char out '>';
-          print_xml out tree_ fchild;
-          output_string out "</";
-          output_string out tag;
-          output_char out '>'
-        end
-    | Attribute -> ignore (print_attributes ~sep:false out tree_ node)
-    | Comment ->
-        output_string out "<!--";
-        output_string out node.data;
-        output_string out "-->"
-    | ProcessingInstruction ->
-        output_string out "<?";
-        output_string out (QName.to_string (QName.remove_prefix node.tag));
-        output_char out ' ';
-        output_string out node.data;
-        output_string out "?>"
-  in
-  print_xml out tree_ node.next_sibling
-
-let print_xml out tree_ node =
-  let nnode =  { node with next_sibling = nil } in print_xml out tree_ nnode
-
-let root t = t.root
-let size t = t.size
-let first_child _ n = n.first_child
-let next_sibling _ n = n.next_sibling
-let parent _ n = n.parent
-let tag _ n = n.tag
-let data _ n = n.data
-let kind _ n = n.kind
-let preorder _ n = n.preorder
-
-let print_node fmt n = Parser.debug_node fmt n
diff --git a/src/tree/naive.mli b/src/tree/naive.mli
deleted file mode 100644
index 5e0a52e..0000000
--- a/src/tree/naive.mli
+++ /dev/null
@@ -1,20 +0,0 @@
-(***********************************************************************)
-(*                                                                     *)
-(*                               TAToo                                 *)
-(*                                                                     *)
-(*                     Kim Nguyen, LRI UMR8623                         *)
-(*                   Université Paris-Sud & CNRS                       *)
-(*                                                                     *)
-(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(*  Recherche Scientifique. All rights reserved.  This file is         *)
-(*  distributed under the terms of the GNU Lesser General Public       *)
-(*  License, with the special exception on linking described in file   *)
-(*  ../LICENSE.                                                        *)
-(*                                                                     *)
-(***********************************************************************)
-
-(*
-  Time-stamp: <Last modified on 2013-03-05 14:08:25 CET by Kim Nguyen>
-*)
-
-include Sig.S
diff --git a/src/tree/sig.ml b/src/tree/sig.ml
deleted file mode 100644
index e2db1d1..0000000
--- a/src/tree/sig.ml
+++ /dev/null
@@ -1,90 +0,0 @@
-(***********************************************************************)
-(*                                                                     *)
-(*                               TAToo                                 *)
-(*                                                                     *)
-(*                     Kim Nguyen, LRI UMR8623                         *)
-(*                   Université Paris-Sud & CNRS                       *)
-(*                                                                     *)
-(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(*  Recherche Scientifique. All rights reserved.  This file is         *)
-(*  distributed under the terms of the GNU Lesser General Public       *)
-(*  License, with the special exception on linking described in file   *)
-(*  ../LICENSE.                                                        *)
-(*                                                                     *)
-(***********************************************************************)
-
-(*
-  Time-stamp: <Last modified on 2013-03-13 18:46:18 CET by Kim Nguyen>
-*)
-
-(** Implementation of documents as binary trees *)
-
-module type S =
-sig
-  type node
-  (** The type of a tree node *)
-
-  type t
-  (** The type of trees *)
-
-  val size : t -> int
-  (** Return the number of nodes *)
-
-  val nil : node
-  (** Nil node, denoting the first/second child of a leaf or the parent of
-      the root *)
-
-  val dummy : node
-  (** Dummy node that is guaranteed to never occur in any tree *)
-
-  val load_xml_file : in_channel -> t
-  (** Takes a file descriptor and returns the XML data stored in the
-      corresponding file. Start at the current position in the file
-      descriptor (which is not necessarily the begining of file)
-  *)
-
-  val load_xml_string : string -> t
-  (** Loads XML data stored in a string *)
-
-  val print_xml : out_channel -> t -> node -> unit
-  (** Outputs the tree as an XML document on the given output_channel *)
-
-  val root : t -> node
-  (** Returns the root of the tree *)
-
-  val first_child : t -> node -> node
-  (** [first_child t n] returns the first child of node [n] in tree [t].
-      Returns [nil] if [n] is a leaf. Returns [nil] if [n == nil].
-  *)
-
-  val next_sibling : t -> node -> node
-  (** [next_sibling t n] returns the next_sibling of node [n] in tree [t].
-      Returns [nil] if [n] is the last child of a node.
-      Returns [nil] if [n == nil].
-  *)
-
-  val parent : t -> node -> node
-  (** [next_sibling t n] returns the parent of node [n] in tree [t].
-      Returns [nil] if [n] is the root of the tree.
-      Returns [nil] if [n == nil].
-  *)
-
-  val tag : t -> node -> Utils.QName.t
-  (** Returns the label of a given node *)
-
-  val data : t -> node -> string
-  (** Returns the character data associated with a node.
-      The only node having character data are those whose label is
-      QName.text, QName.cdata_section or QName.comment
-  *)
-
-  val kind : t -> node -> Common.NodeKind.t
-  (** Returns the kind of the given node *)
-
-  val preorder : t -> node -> int
-  (** Returns the position of a node in pre-order in the tree. The
-    root has preorder 0. [nil] has pre-order [-1].
-  *)
-
-  val print_node : Format.formatter -> node -> unit
-end
diff --git a/src/uid.ml b/src/uid.ml
new file mode 100644
index 0000000..0cb9688
--- /dev/null
+++ b/src/uid.ml
@@ -0,0 +1,33 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                               TAToo                                 *)
+(*                                                                     *)
+(*                     Kim Nguyen, LRI UMR8623                         *)
+(*                   Université Paris-Sud & CNRS                       *)
+(*                                                                     *)
+(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(*  Recherche Scientifique. All rights reserved.  This file is         *)
+(*  distributed under the terms of the GNU Lesser General Public       *)
+(*  License, with the special exception on linking described in file   *)
+(*  ../LICENSE.                                                        *)
+(*                                                                     *)
+(***********************************************************************)
+
+(*
+  Time-stamp: <Last modified on 2013-01-30 19:06:39 CET by Kim Nguyen>
+*)
+
+type t = int
+
+exception Overflow
+let make_maker () =
+  let _id = ref ~-1 in
+    fun () ->
+      incr _id;
+      let i = !_id in
+      if i < 0 then raise Overflow else i
+
+let dummy = -1
+
+external to_int : t -> int = "%identity"
+external of_int : int -> t= "%identity"
diff --git a/src/uid.mli b/src/uid.mli
new file mode 100644
index 0000000..286cacc
--- /dev/null
+++ b/src/uid.mli
@@ -0,0 +1,45 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                               TAToo                                 *)
+(*                                                                     *)
+(*                     Kim Nguyen, LRI UMR8623                         *)
+(*                   Université Paris-Sud & CNRS                       *)
+(*                                                                     *)
+(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(*  Recherche Scientifique. All rights reserved.  This file is         *)
+(*  distributed under the terms of the GNU Lesser General Public       *)
+(*  License, with the special exception on linking described in file   *)
+(*  ../LICENSE.                                                        *)
+(*                                                                     *)
+(***********************************************************************)
+
+(*
+  Time-stamp: <Last modified on 2013-01-30 19:06:33 CET by Kim Nguyen>
+*)
+
+(** This modules implements unique identifiers represented by integers *)
+
+type t = private int
+(** The type of unique identifiers. *)
+
+exception Overflow
+(** Raised when the internal counters for IDs overflows. *)
+
+val make_maker : unit -> (unit -> t)
+(** Returns an uid generator.
+    [make_maker ()] returns a function that generates unique ids. Raises
+    [Overflow] if the internal counter overflows.
+*)
+
+val dummy : t
+(** A dummy identifier, guaranteed to be distinct from any value
+    returned by a generator.
+*)
+
+external to_int : t -> int = "%identity"
+(** Convert a unique id to an integer *)
+
+(**/**)
+
+external of_int : int -> t = "%identity"
+(** May break the invariant, use with caution *)
diff --git a/src/utils.mlpack b/src/utils.mlpack
deleted file mode 100644
index 755f521..0000000
--- a/src/utils.mlpack
+++ /dev/null
@@ -1,15 +0,0 @@
-utils/Cache
-utils/Common_sig
-utils/FiniteCofinite
-utils/FiniteCofinite_sig
-utils/Hcons
-utils/Hcons_sig
-utils/Hlist
-utils/Hlist_sig
-utils/Misc
-utils/Pretty
-utils/Ptset
-utils/Ptset_sig
-utils/QName
-utils/QNameSet
-utils/Uid
diff --git a/src/utils/cache.ml b/src/utils/cache.ml
deleted file mode 100644
index abd999e..0000000
--- a/src/utils/cache.ml
+++ /dev/null
@@ -1,253 +0,0 @@
-(***********************************************************************)
-(*                                                                     *)
-(*                               TAToo                                 *)
-(*                                                                     *)
-(*                     Kim Nguyen, LRI UMR8623                         *)
-(*                   Université Paris-Sud & CNRS                       *)
-(*                                                                     *)
-(*  Copyright 2010-2013 Université Paris-Sud and Centre National de la *)
-(*  Recherche Scientifique. All rights reserved.  This file is         *)
-(*  distributed under the terms of the GNU Lesser General Public       *)
-(*  License, with the special exception on linking described in file   *)
-(*  ../LICENSE.                                                        *)
-(*                                                                     *)
-(***********************************************************************)
-
-(*
-  Time-stamp: <Last modified on 2013-03-14 14:50:18 CET by Kim Nguyen>
-*)
-
-let realloc l old_size new_size dummy =
-  let l' = Array.create new_size dummy in
-  for i = 0 to (min old_size new_size) - 1 do
-    Array.unsafe_set l' i  (Array.unsafe_get l i);
-  done;
-  l'
-
-module N1 =
-struct
-  type 'a t = { mutable line : 'a array;
-		dummy : 'a;
-		mutable offset : int;
-	      }
-  let create a = {
-    line = Array.create 0 a;
-    dummy = a;
-    offset = ~-1;
-
-  }
-
-  let print fmt a =
-    Format.fprintf fmt "{ offset=%i;\n dummy=_;line=%a \n}\n%!"
-      a.offset
-      (Pretty.print_array ~sep:", " (fun fmt x ->
-	if x==a.dummy then
-	  Format.fprintf fmt "%s" "D"
-	else
-	  Format.fprintf fmt "%s" "E")) a.line
-
-  let add a i v =
-    if a.offset == ~-1 then a.offset <- i;
-    let offset = a.offset in
-    let len = Array.length a.line in
-    if i >= offset && i < offset + len then
-      a.line.(i - offset) <- v
-    else
-      if i < offset then begin (* bottom resize *)
-	let pad = offset - i in
-	let nlen = len + pad in
-	let narray = Array.create nlen a.dummy in
-	for j = 0 to len - 1 do
-	  narray.(j+pad) <- a.line.(j)
-	done;
-	a.offset <- i;
-	a.line <- narray;
-	narray.(0) <- v;
-      end else begin (* top resize *)
-	(* preventively allocate the space for the following elements *)
-	let nlen = ((i - offset + 1) lsl 1) + 1 in
-	let narray = Array.create nlen a.dummy in
-	for j = 0 to len - 1 do
-	  narray.(j) <- a.line.(j);
-	done;
-	narray.(i - offset) <- v;
-	a.line <- narray
-      end
-
-  let find a i =
-    let idx = i - a.offset in
-    let len = Array.length a.line in
-    if idx >= 0 && idx < len then
-      Array.unsafe_get a.line idx
-    else a.dummy
-
-  let dummy a = a.dummy
-
-  let iteri f a =
-    let line = a.line in
-    if a.offset == ~-1 then () else
-      for i = 0 to Array.length line - 1 do
-	let v = line.(i) in
-	  f (i+a.offset) v (v==a.dummy)
-      done
-
-
-end
-
-module N2 =
-struct
-  type 'a t = 'a N1.t N1.t
-  let create a =
-    let dummy1 = N1.create a in
-    N1.create dummy1
-
-  let add a i j v =
-    let line = N1.find a i in
-    if line == a.N1.dummy then
-      let nline = N1.create line.N1.dummy in
-      N1.add a i nline;
-      N1.add nline j v
-    else
-      N1.add line j v
-
-
-  let find a i j =
-    let v = N1.find a i in
-    if v == a.N1.dummy then v.N1.dummy
-    else N1.find v j
-
-
-  let dummy c = c.N1.dummy.N1.dummy
-
-  let iteri f a =
-    let line = a.N1.line in
-    if a.N1.offset == ~-1 then () else
-      for i = 0 to Array.length line - 1 do
-	N1.iteri (f i) line.(i)
-      done
-
-
-end
-
-module N3 =
-struct
-  type 'a t = 'a N2.t N1.t
-
-  let create a =
-    let dummy2 = N2.create a in
-    N1.create dummy2
-
-  let add a i j k v =
-    let line = N1.find a i in
-    if line == a.N1.dummy then
-      let nline =  N1.create line.N1.dummy in
-      N1.add a i nline;
-      N2.add nline j k v
-    else
-      N2.add line j k v
-
-  let find a i j k =
-    let v = N1.find a i in
-    if v == a.N1.dummy then N2.dummy v
-    else N2.find v j k
-
-
-  let dummy a = N2.dummy a.N1.dummy
-  let iteri f a =
-    let line = a.N1.line in
-    if a.N1.offset == ~-1 then () else
-      for i = 0 to Array.length line - 1 do
-	N2.iteri (f i) line.(i)
-      done
-
-end
-
-module N4 =
-struct
-  type 'a t = 'a N3.t N1.t
-
-  let create a =
-  let dummy3 = N3.create a in
-  N1.create dummy3
-
-  let add a i j k l v =
-    let line = N1.find a i in
-    if line == N1.dummy a then
-      let nline =  N3.create (N3.dummy line) in
-      N1.add a i nline;
-      N3.add nline j k l v
-    else
-      N3.add line j k l v
-
-  let find a i j k l =
-    let v = N1.find a i in
-    if v == (N1.dummy a) then N3.dummy v
-    else N3.find v j k l
-
-
-  let dummy a = N3.dummy (N1.dummy a)
-  let iteri f a =
-    N1.iteri (fun i v _ ->
-      N3.iteri (fun j k l v2 b -> f i j k l v2 b) v ) a
-
-end
-
-module N5 =
-struct
-  type 'a t = 'a N4.t N1.t
-
-  let create a =
-    let dummy4 = N4.create a in
-    N1.create dummy4
-
-  let add a i j k l m v =
-    let line = N1.find a i in
-    if line == (N1.dummy a) then
-      let nline =  N4.create (N4.dummy line) in
-      N1.add a i nline;
-      N4.add nline j k l m v
-    else
-      N4.add line j k l m v
-
-  let find a i j k l m =
-    let v = N1.find a i in
-    if v == (N1.dummy a) then N4.dummy v
-    else N4.find v j k l m
-
-
-  let dummy a = N4.dummy (N1.dummy a)
-  let iteri f a =
-    N1.iteri (fun i v _ ->
-      N4.iteri (fun j k l m v2 b -> f i j k l m v2 b) v
-    ) a
-end
-
-module N6 =
-struct
-  type 'a t = 'a N5.t N1.t
-
-  let create a =
-    let dummy5 = N5.create a in
-    N1.create dummy5
-
-  let add a i j k l m n v =
-    let line = N1.find a i in
-    if line == N1.dummy a then
-      let nline =  N5.create (N5.dummy line) in
-      N1.add a i nline;
-      N5.add nline j k l m n v
-    else
-      N5.add line j k l m n v
-
-  let find a i j k l m n =
-    let v = N1.find a i in
-    if v == N1.dummy a then N5.dummy v
-    else N5.find v j k l m n
-
-
-  let dummy a = N5.dummy (N1.dummy a)
-  let iteri f a =
-    N1.iteri (fun i v _  ->
-      N5.iteri (fun j k l m n v2 b -> f i j k l m n v2 b) v
-    ) a
-end
diff --git a/src/utils/cache.mli b/src/utils/cache.mli
deleted file mode 100644
index 1211935..0000000
--- a/src/utils/cache.mli
+++ /dev/null
@@ -1,81 +0,0 @@
-(***********************************************************************)
-(*                                                                     *)
-(*                               TAToo                                 *)
-(*                                                                     *)
-(*                     Kim Nguyen, LRI UMR8623                         *)
-(*                   Université Paris-Sud & CNRS                       *)
-(*                                                                     *)
-(*  Copyright 2010-2013 Université Paris-Sud and Centre National de la *)
-(*  Recherche Scientifique. All rights reserved.  This file is         *)
-(*  distributed under the terms of the GNU Lesser General Public       *)
-(*  License, with the special exception on linking described in file   *)
-(*  ../LICENSE.                                                        *)
-(*                                                                     *)
-(***********************************************************************)
-
-(*
-  Time-stamp: <Last modified on 2013-03-14 13:42:53 CET by Kim Nguyen>
-*)
-
-(** N-dimentional caches *)
-
-module N1 :
-sig
-
-  type 'a t
-  val create : 'a -> 'a t
-  val find : 'a t -> int -> 'a
-  val add : 'a t -> int -> 'a -> unit
-  val dummy : 'a t -> 'a
-  val iteri : (int -> 'a -> bool -> unit) -> 'a t -> unit
-end
-
-module N2:
-sig
-    type 'a t
-    val create : 'a -> 'a t
-    val find : 'a t -> int -> int -> 'a
-    val add : 'a t -> int -> int -> 'a -> unit
-    val dummy : 'a t -> 'a
-    val iteri : (int -> int -> 'a -> bool -> unit) -> 'a t -> unit
-end
-
-module N3 :
-  sig
-    type 'a t
-    val create : 'a -> 'a t
-    val find : 'a t -> int -> int -> int -> 'a
-    val add : 'a t -> int -> int -> int -> 'a -> unit
-    val dummy : 'a t -> 'a
-    val iteri : (int -> int -> int -> 'a -> bool -> unit) -> 'a t -> unit
-  end
-
-module N4 :
-  sig
-    type 'a t
-    val create : 'a -> 'a t
-    val find : 'a t -> int -> int -> int -> int -> 'a
-    val add : 'a t -> int -> int -> int -> int -> 'a -> unit
-    val dummy : 'a t -> 'a
-    val iteri : (int -> int -> int -> int -> 'a -> bool -> unit) -> 'a t -> unit
-  end
-
-module N5 :
-  sig
-    type 'a t
-    val create : 'a -> 'a t
-    val find : 'a t -> int -> int -> int -> int -> int -> 'a
-    val add : 'a t -> int -> int -> int -> int -> int -> 'a -> unit
-    val dummy : 'a t -> 'a
-    val iteri : (int -> int -> int -> int -> int -> 'a -> bool -> unit) -> 'a t -> unit
-  end
-
-module N6 :
-  sig
-    type 'a t
-    val create : 'a -> 'a t
-    val find : 'a t -> int -> int -> int -> int -> int -> int -> 'a
-    val add : 'a t -> int -> int -> int -> int -> int -> int -> 'a -> unit
-    val dummy : 'a t -> 'a
-    val iteri : (int -> int -> int -> int -> int -> int -> 'a -> bool -> unit) -> 'a t -> unit
-  end
diff --git a/src/utils/common_sig.ml b/src/utils/common_sig.ml
deleted file mode 100644
index 37437e4..0000000
--- a/src/utils/common_sig.ml
+++ /dev/null
@@ -1,108 +0,0 @@
-(***********************************************************************)
-(*                                                                     *)
-(*                               TAToo                                 *)
-(*                                                                     *)
-(*                     Kim Nguyen, LRI UMR8623                         *)
-(*                   Université Paris-Sud & CNRS                       *)
-(*                                                                     *)
-(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(*  Recherche Scientifique. All rights reserved.  This file is         *)
-(*  distributed under the terms of the GNU Lesser General Public       *)
-(*  License, with the special exception on linking described in file   *)
-(*  ../LICENSE.                                                        *)
-(*                                                                     *)
-(***********************************************************************)
-
-(*
-  Time-stamp: <Last modified on 2013-03-04 23:01:55 CET by Kim Nguyen>
-*)
-
-(** Type equipped with an equality and hash function.
-    If [equal a b] then [(hash a) = (hash b)]
-*)
-module type HashedType =
-sig
-  type t
-
-    (** [hash v] returns an integer in the range [ 0 - 2^30-1 ]
-    *)
-  val hash : t -> int
-
-    (** Equality *)
-  val equal : t -> t -> bool
-
-end
-
-(** Type equiped with a total ordering *)
-module type OrderedType =
-sig
-  type t
-
-    (** Total ordering on values of type [t].  [compare a b] returns a
-        negative number if [a] is strictly smaller than [b], a positive
-        number if [a] is strictly greater than [b] and 0 if [a] is equal
-        to [b].  *)
-  val compare : t -> t -> int
-end
-
-module type Type =
-sig
-  type t
-  include HashedType with type t := t
-  include OrderedType with type t := t
-end
-
-(** Type equiped with a pretty-printer *)
-module type Printable =
-sig
-  type t
-  val print : Format.formatter -> t -> unit
-end
-
-(** Signature of a simple HashSet module *)
-module type HashSet =
-sig
-  type data
-  type t
-  val create : int -> t
-  val add : t -> data -> unit
-  val remove : t -> data -> unit
-  val find : t -> data -> data
-  val find_all : t -> data -> data list
-  val clear : t -> unit
-  val mem : t -> data -> bool
-end
-
-  (** Signature of simple Set module *)
-module type Set =
-sig
-  type elt
-  type t
-  val empty : t
-  val is_empty : t -> bool
-  val mem : elt -> t -> bool
-  val add : elt -> t -> t
-  val singleton : elt -> t
-  val remove : elt -> t -> t
-  val union : t -> t -> t
-  val inter : t -> t -> t
-  val diff : t -> t -> t
-  val compare : t -> t -> int
-  val equal : t -> t -> bool
-  val subset : t -> t -> bool
-  val iter : (elt -> unit) -> t -> unit
-  val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
-  val for_all : (elt -> bool) -> t -> bool
-  val exists : (elt -> bool) -> t -> bool
-  val filter : (elt -> bool) -> t -> t
-  val partition : (elt -> bool) -> t -> t * t
-  val cardinal : t -> int
-  val elements : t -> elt list
-  val min_elt : t -> elt
-  val max_elt : t -> elt
-  val choose : t -> elt
-  val split : elt -> t -> t * bool * t
-  val intersect : t -> t -> bool
-  val is_singleton : t -> bool
-  val from_list : elt list -> t
-end
diff --git a/src/utils/finiteCofinite.ml b/src/utils/finiteCofinite.ml
deleted file mode 100644
index 2bfe70c..0000000
--- a/src/utils/finiteCofinite.ml
+++ /dev/null
@@ -1,221 +0,0 @@
-(***********************************************************************)
-(*                                                                     *)
-(*                               TAToo                                 *)
-(*                                                                     *)
-(*                     Kim Nguyen, LRI UMR8623                         *)
-(*                   Université Paris-Sud & CNRS                       *)
-(*                                                                     *)
-(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(*  Recherche Scientifique. All rights reserved.  This file is         *)
-(*  distributed under the terms of the GNU Lesser General Public       *)
-(*  License, with the special exception on linking described in file   *)
-(*  ../LICENSE.                                                        *)
-(*                                                                     *)
-(***********************************************************************)
-
-(*
-  Time-stamp: <Last modified on 2013-03-05 01:50:21 CET by Kim Nguyen>
-*)
-
-INCLUDE "utils.ml"
-
-include FiniteCofinite_sig
-
-module type HConsBuilder =
-  functor (H : Common_sig.HashedType) -> Hcons.S with type data = H.t
-
-module Builder (HCB : HConsBuilder) (E : Ptset.S) :
-  S with type elt = E.elt and type set = E.t =
-struct
-  type elt = E.elt
-  type node = Finite of E.t | CoFinite of E.t
-  type set = E.t
-  module Node = HCB(struct
-    type t = node
-    let equal a b =
-      match a, b with
-        Finite s1, Finite s2
-      | CoFinite s1, CoFinite s2 -> E.equal s1 s2
-      | (Finite _| CoFinite _), _ -> false
-
-    let hash = function
-      | Finite s -> HASHINT2 (PRIME1, E.hash s)
-      | CoFinite s -> HASHINT2 (PRIME3, E.hash s)
-  end)
-  include Node
-  let empty = make (Finite E.empty)
-  let any = make (CoFinite E.empty)
-  let finite x = make (Finite x)
-  let cofinite x = make (CoFinite x)
-
-  let is_empty t =  match t.node with
-    | Finite s -> E.is_empty s
-    | CoFinite _  -> false
-
-  let is_any t = match t.node with
-    | CoFinite s -> E.is_empty s
-    | Finite _  -> false
-
-  let is_finite t = match t.node with
-    | Finite _ -> true
-    | CoFinite _ -> false
-
-  let kind t = match t.node with
-    | Finite _ -> `Finite
-    | CoFinite _  -> `Cofinite
-
-  let mem x t = match t.node with
-    | Finite s -> E.mem x s
-    | CoFinite s -> not (E.mem x s)
-
-  let singleton x = finite (E.singleton x)
-
-  let add e t = match t.node with
-    | Finite s -> finite (E.add e s)
-    | CoFinite s -> cofinite (E.remove e s)
-
-  let remove e t = match t.node with
-    | Finite s -> finite (E.remove e s)
-    | CoFinite s -> cofinite (E.add e s)
-
-  let union s t = match s.node, t.node with
-    | Finite s, Finite t -> finite (E.union s t)
-    | CoFinite s, CoFinite t -> cofinite ( E.inter s t)
-    | Finite s, CoFinite t -> cofinite (E.diff t s)
-    | CoFinite s, Finite t-> cofinite (E.diff s t)
-
-  let inter s t = match s.node, t.node with
-    | Finite s, Finite t -> finite (E.inter s t)
-    | CoFinite s, CoFinite t -> cofinite (E.union s t)
-    | Finite s, CoFinite t -> finite (E.diff s t)
-    | CoFinite s, Finite t-> finite (E.diff t s)
-
-  let diff s t = match s.node, t.node with
-    | Finite s, Finite t -> finite (E.diff s t)
-    | Finite s, CoFinite t -> finite(E.inter s t)
-    | CoFinite s, Finite t -> cofinite(E.union t s)
-    | CoFinite s, CoFinite t -> finite (E.diff t s)
-
-  let complement t = match t.node with
-    | Finite s -> cofinite s
-    | CoFinite s -> finite s
-
-  let compare s t = match s.node, t.node with
-    | Finite s , Finite t -> E.compare s t
-    | CoFinite s , CoFinite t -> E.compare t s
-    | Finite _, CoFinite _ -> -1
-    | CoFinite _, Finite _ -> 1
-
-  let subset s t = match s.node, t.node with
-    | Finite s , Finite t -> E.subset s t
-    | CoFinite s , CoFinite t -> E.subset t s
-    | Finite s, CoFinite t -> E.is_empty (E.inter s t)
-    | CoFinite _, Finite _ -> false
-
-  (* given a  list l of type t list,
-     returns two sets (f,c) where :
-     - f is the union of all the finite sets of l
-     - c is the union of all the cofinite sets of l
-     - f and c are disjoint
-     Invariant : cup f c = List.fold_left cup empty l
-     We treat the CoFinite part explicitely :
-  *)
-
-  let kind_split l =
-
-    let rec next_finite_cofinite facc cacc = function
-      | [] -> finite facc, cofinite (E.diff cacc facc)
-      | { node = Finite s; _ } ::r ->
-        next_finite_cofinite (E.union s facc) cacc r
-      | { node = CoFinite _ ; _ } ::r when E.is_empty cacc ->
-        next_finite_cofinite facc cacc r
-      | { node = CoFinite s; _ } ::r ->
-        next_finite_cofinite facc (E.inter cacc s) r
-    in
-    let rec first_cofinite facc = function
-      | [] -> empty,empty
-      | { node = Finite s ; _ } :: r-> first_cofinite (E.union s facc) r
-      | { node = CoFinite s ; _ } :: r -> next_finite_cofinite facc s r
-    in
-      first_cofinite E.empty l
-
-  let exn = FiniteCofinite_sig.InfiniteSet
-
-  let fold f t a = match t.node with
-    | Finite s -> E.fold f s a
-    | CoFinite _ -> raise exn
-
-  let iter f t = match t.node with
-    | Finite t -> E.iter f t
-    | CoFinite _ -> raise exn
-
-  let for_all f t = match t.node with
-    | Finite s -> E.for_all f s
-    | CoFinite _ -> raise exn
-
-  let exists f t = match t.node with
-    | Finite s -> E.exists f s
-    | CoFinite _ -> raise exn
-
-  let filter f t = match t.node with
-    | Finite s -> finite (E.filter f s)
-    | CoFinite _ -> raise exn
-
-  let partition f t = match t.node with
-    | Finite s -> let a,b = E.partition f s in finite a,finite b
-    | CoFinite _ -> raise exn
-
-  let cardinal t = match t.node with
-    | Finite s -> E.cardinal s
-    | CoFinite _ -> raise exn
-
-  let elements t = match t.node with
-    | Finite s -> E.elements s
-    | CoFinite _ -> raise exn
-
-  let from_list l =
-    finite (List.fold_left (fun x a -> E.add a x ) E.empty l)
-
-  let choose t = match t.node with
-      Finite s -> E.choose s
-    | CoFinite _ -> raise exn
-
-  let is_singleton t = match t.node with
-    | Finite s -> E.is_singleton s
-    | CoFinite _ -> false
-
-  let intersect s t = match s.node, t.node with
-    | Finite s, Finite t -> E.intersect s t
-    | CoFinite s, Finite t -> not (E.subset t s)
-    | Finite s, CoFinite t -> not (E.subset s t)
-    | CoFinite _ , CoFinite _ -> true
-
-  let split x s = match s.node with
-    | Finite s ->
-      let s1, b, s2 = E.split x s in
-      finite s1, b, finite s2
-
-    | CoFinite _ -> raise exn
-
-  let min_elt s = match s.node with
-    | Finite s -> E.min_elt s
-    | CoFinite _ -> raise exn
-
-  let max_elt s = match s.node with
-    | Finite s -> E.min_elt s
-    | CoFinite _ -> raise exn
-
-  let positive t = match t.node with
-      | Finite x -> x
-      | CoFinite _ -> E.empty
-
-  let negative t = match t.node with
-      | CoFinite x -> x
-      | Finite _ -> E.empty
-
-  let inj_positive t = finite t
-  let inj_negative t = cofinite t
-end
-
-module Make = Builder(Hcons.Make)
-module Weak = Builder(Hcons.Weak)
diff --git a/src/utils/finiteCofinite.mli b/src/utils/finiteCofinite.mli
deleted file mode 100644
index cd92cda..0000000
--- a/src/utils/finiteCofinite.mli
+++ /dev/null
@@ -1,36 +0,0 @@
-(***********************************************************************)
-(*                                                                     *)
-(*                               TAToo                                 *)
-(*                                                                     *)
-(*                     Kim Nguyen, LRI UMR8623                         *)
-(*                   Université Paris-Sud & CNRS                       *)
-(*                                                                     *)
-(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(*  Recherche Scientifique. All rights reserved.  This file is         *)
-(*  distributed under the terms of the GNU Lesser General Public       *)
-(*  License, with the special exception on linking described in file   *)
-(*  ../LICENSE.                                                        *)
-(*                                                                     *)
-(***********************************************************************)
-
-(*
-  Time-stamp: <Last modified on 2013-03-04 22:44:50 CET by Kim Nguyen>
-*)
-
-(** Implementation of hashconsed finite or cofinite sets.
-*)
-
-include module type of FiniteCofinite_sig
-
-(** Output signature of the {!FiniteCofinite.Make} and
-    {!FiniteCofinite.Weak} functors.*)
-
-module Make (E : Ptset.S) : S with type elt = E.elt and type set = E.t
-(** Builds an implementation of hashconsed sets of hashconsed elements.
-    See {!Hcons.Make}.
-*)
-
-module Weak (E : Ptset.S) : S with type elt = E.elt and type set = E.t
-(** Builds an implementation of hashconsed sets of hashconsed elements
-    with weak internal storage. See {!Hcons.Weak}.
-*)
diff --git a/src/utils/finiteCofinite_sig.ml b/src/utils/finiteCofinite_sig.ml
deleted file mode 100644
index da17049..0000000
--- a/src/utils/finiteCofinite_sig.ml
+++ /dev/null
@@ -1,36 +0,0 @@
-(***********************************************************************)
-(*                                                                     *)
-(*                               TAToo                                 *)
-(*                                                                     *)
-(*                     Kim Nguyen, LRI UMR8623                         *)
-(*                   Université Paris-Sud & CNRS                       *)
-(*                                                                     *)
-(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(*  Recherche Scientifique. All rights reserved.  This file is         *)
-(*  distributed under the terms of the GNU Lesser General Public       *)
-(*  License, with the special exception on linking described in file   *)
-(*  ../LICENSE.                                                        *)
-(*                                                                     *)
-(***********************************************************************)
-
-(*
-  Time-stamp: <Last modified on 2013-03-04 22:44:15 CET by Kim Nguyen>
-*)
-
-exception InfiniteSet
-module type S =
-sig
-  include Hcons.S
-  include Common_sig.Set with type t := t
-  type set
-  val any : t
-  val is_any : t -> bool
-  val is_finite : t -> bool
-  val kind : t -> [ `Finite | `Cofinite ]
-  val complement : t -> t
-  val kind_split : t list -> t * t
-  val positive : t -> set
-  val negative : t -> set
-  val inj_positive : set -> t
-  val inj_negative : set -> t
-end
diff --git a/src/utils/hcons.ml b/src/utils/hcons.ml
deleted file mode 100644
index 3fc3e71..0000000
--- a/src/utils/hcons.ml
+++ /dev/null
@@ -1,84 +0,0 @@
-(***********************************************************************)
-(*                                                                     *)
-(*                               TAToo                                 *)
-(*                                                                     *)
-(*                     Kim Nguyen, LRI UMR8623                         *)
-(*                   Université Paris-Sud & CNRS                       *)
-(*                                                                     *)
-(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(*  Recherche Scientifique. All rights reserved.  This file is         *)
-(*  distributed under the terms of the GNU Lesser General Public       *)
-(*  License, with the special exception on linking described in file   *)
-(*  ../LICENSE.                                                        *)
-(*                                                                     *)
-(***********************************************************************)
-
-(*
-  Time-stamp: <Last modified on 2013-03-04 22:39:39 CET by Kim Nguyen>
-*)
-
-include Hcons_sig
-
-module type TableBuilder =
-  functor
-    (H : Common_sig.HashedType) ->
-      Common_sig.HashSet with type data = H.t
-
-module Builder (TB : TableBuilder) (H : Common_sig.HashedType) =
-struct
-  type data = H.t
-  type t = { id   : Uid.t;
-             hash : int;
-             node : data }
-  let uid_make = ref (Uid.make_maker())
-  let node t = t.node
-  let uid t = t.id
-  let hash t = t.hash
-  let equal t1 t2 = t1 == t2
-  module HN =
-  struct
-    type _t = t
-    type t = _t
-    let hash = hash
-    let equal x y = x == y || H.equal x.node y.node
-  end
-  module T = TB(HN)
-
-  let pool = T.create 101
-  let init () =
-    T.clear pool;
-    uid_make := Uid.make_maker ()
-  let dummy x = { id = Uid.dummy; hash = H.hash x; node = x }
-
-  let make x =
-    let cell = { id = Uid.dummy; hash = H.hash x; node = x } in
-    try
-      T.find pool cell
-    with
-    | Not_found ->
-      let cell = { cell with id = !uid_make(); } in
-      T.add pool cell;
-      cell
-end
-
-module Make = Builder (Misc.HashSet)
-module Weak = Builder (Weak.Make)
-
-module PosInt =
-struct
-  type data = int
-  type t = int
-  let make v =
-    if v < 0 then raise (Invalid_argument "Hcons.PosInt.make")
-    else v
-
-  let node v = v
-
-  let hash v = v
-
-  let uid v = Uid.of_int v
-  let dummy _ = ~-1
-  let equal x y = x == y
-
-  let init () = ()
-end
diff --git a/src/utils/hcons.mli b/src/utils/hcons.mli
deleted file mode 100644
index b4049a0..0000000
--- a/src/utils/hcons.mli
+++ /dev/null
@@ -1,45 +0,0 @@
-(***********************************************************************)
-(*                                                                     *)
-(*                               TAToo                                 *)
-(*                                                                     *)
-(*                     Kim Nguyen, LRI UMR8623                         *)
-(*                   Université Paris-Sud & CNRS                       *)
-(*                                                                     *)
-(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(*  Recherche Scientifique. All rights reserved.  This file is         *)
-(*  distributed under the terms of the GNU Lesser General Public       *)
-(*  License, with the special exception on linking described in file   *)
-(*  ../LICENSE.                                                        *)
-(*                                                                     *)
-(***********************************************************************)
-
-(*
-  Time-stamp: <Last modified on 2013-03-04 23:05:14 CET by Kim Nguyen>
-*)
-
-(** Implementation of generic hashconsing. *)
-
-include module type of Hcons_sig
-
-(** Output signature of the functor {!Hcons.Make} *)
-
-module Make (H : Common_sig.HashedType) : S with type data = H.t
-(** Functor building an implementation of hashconsed values for a given
-    implementation of {!Common_sig.HashedType}. Hashconsed values are
-    persistent: the are kept in memory even if no external reference
-    remain. Calling [init()] explicitely will reclaim the space.
-*)
-
-module Weak (H : Common_sig.HashedType) : S with type data = H.t
-(** Functor building an implementation of hashconsed values for a given
-    implementation of {!Common_sig.HashedType}. Hashconsed values have a
-    weak semantics: they may be reclaimed as soon as no external
-    reference to them exists. The space may still be reclaimed
-    explicitely by calling [init].
-*)
-
-module PosInt : Abstract with type data = int and type t = int
-(** Compact implementation of hashconsed positive integer that
-    avoids boxing. [PosInt.make v] raises [Invalid_argument] if
-    [ v < 0 ]
-*)
diff --git a/src/utils/hcons_sig.ml b/src/utils/hcons_sig.ml
deleted file mode 100644
index 599819c..0000000
--- a/src/utils/hcons_sig.ml
+++ /dev/null
@@ -1,68 +0,0 @@
-(***********************************************************************)
-(*                                                                     *)
-(*                               TAToo                                 *)
-(*                                                                     *)
-(*                     Kim Nguyen, LRI UMR8623                         *)
-(*                   Université Paris-Sud & CNRS                       *)
-(*                                                                     *)
-(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(*  Recherche Scientifique. All rights reserved.  This file is         *)
-(*  distributed under the terms of the GNU Lesser General Public       *)
-(*  License, with the special exception on linking described in file   *)
-(*  ../LICENSE.                                                        *)
-(*                                                                     *)
-(***********************************************************************)
-
-(*
-  Time-stamp: <Last modified on 2013-03-04 22:36:31 CET by Kim Nguyen>
-*)
-
-  (** Abstract signature of a module implementing an hashconsed datatype *)
-module type Abstract =
-sig
-
-    (** The type of the data to be hash-consed *)
-  type data
-
-    (** The type of hashconsed data *)
-  type t
-
-    (** [make v] internalizes the value [v], making it an hashconsed
-        value.
-    *)
-  val make : data -> t
-
-    (** [node h] extract the original data from its hashconsed value
-    *)
-  val node : t -> data
-
-    (** [hash h] returns a hash of [h], such that for every [h1] and
-        [h2], [equal h1 h2] implies [hash h1 = hash h2].
-    *)
-  val hash : t -> int
-
-    (** [uid h] returns a unique identifier *)
-  val uid : t -> Uid.t
-
-    (** Equality between hashconsed values. Equivalent to [==] *)
-  val equal : t -> t -> bool
-
-    (** Initializes the internal storage. Any previously hashconsed
-        element is discarded. *)
-  val init : unit -> unit
-
-    (** Create a dummy (non-hashconsed) node with a boggus identifer
-        and hash *)
-  val dummy : data -> t
-end
-
-
-  (** Concrete signature of a module implementing an hashconsed datatype *)
-module type S =
-sig
-  type data
-  type t = private { id   : Uid.t;
-                     hash : int;
-                     node : data }
-  include Abstract with type data := data and type t := t
-end
diff --git a/src/utils/hlist.ml b/src/utils/hlist.ml
deleted file mode 100644
index 3ffb8fc..0000000
--- a/src/utils/hlist.ml
+++ /dev/null
@@ -1,82 +0,0 @@
-INCLUDE "utils.ml"
-
-include Hlist_sig
-
-module type HConsBuilder =
-  functor (H : Common_sig.HashedType) -> Hcons.S with type data = H.t
-
-module Builder (HCB : HConsBuilder) (H : Hcons.Abstract) :
-  S with type elt = H.t =
-struct
-  type elt = H.t
-
-  module rec Node : Hcons.S with type data = Data.t = HCB(Data)
-                            and Data : Common_sig.HashedType with type t = (elt, Node.t) node =
-  struct
-    type t = (elt, Node.t) node
-    let equal x y =
-      match x,y with
-      | Nil, Nil -> true
-      | Cons(e1, l1), Cons(e2, l2) -> e1 == e2 && l1 == l2
-      | _ -> false
-
-    let hash = function
-    | Nil -> 0
-    | Cons(e, l) -> HASHINT3 (PRIME1, Uid.to_int (H.uid e), Uid.to_int (Node.uid l))
-  end
-
-  include Node
-
-  let nil = make Nil
-
-  let rec sorted_cons e l =
-    match l.Node.node with
-      |	Nil -> Node.make (Cons(e, l))
-      | Cons (x, ll) ->
-	  if H.uid e < H.uid x
-	  then Node.make (Cons(e, l))
-	  else Node.make (Cons(x, sorted_cons e ll))
-
-  let cons e l =
-    Node.make(Cons(e, l))
-
-  let cons ?(sorted=true) e l =
-    if sorted then sorted_cons e l else cons e l
-
-  let hd = function { Node.node = Cons(e, _); _ } -> e | _ -> failwith "hd"
-  let tl = function { Node.node = Cons(_, l); _ } -> l | _ -> failwith "tl"
-
-  let fold f l acc =
-    let rec loop acc l = match l.Node.node with
-      | Nil -> acc
-      | Cons (a, aa) -> loop (f a acc) aa
-    in
-      loop acc l
-
-  let map f l  =
-    let rec loop l = match l.Node.node with
-      | Nil -> nil
-      | Cons(a, aa) -> cons (f a) (loop aa)
-    in
-      loop l
-
-  let iter f l =
-    let rec loop l = match l.Node.node with
-      | Nil -> ()
-      | Cons(a,aa) ->  (f a);(loop aa)
-    in
-      loop l
-
-  let rev l = fold cons l nil
-  let rev_map f l = fold (fun x acc -> cons (f x) acc) l nil
-  let length l = fold (fun _ c -> c+1) l 0
-  let rec mem e l =
-    match l.Node.node with
-      | Nil -> false
-      | Cons (x, ll) -> x == e || mem e ll
-
-end
-
-module Make = Builder(Hcons.Make)
-module Weak = Builder(Hcons.Weak)
-
diff --git a/src/utils/hlist.mli b/src/utils/hlist.mli
deleted file mode 100644
index 80204d2..0000000
--- a/src/utils/hlist.mli
+++ /dev/null
@@ -1,30 +0,0 @@
-(***********************************************************************)
-(*                                                                     *)
-(*                               TAToo                                 *)
-(*                                                                     *)
-(*                     Kim Nguyen, LRI UMR8623                         *)
-(*                   Université Paris-Sud & CNRS                       *)
-(*                                                                     *)
-(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(*  Recherche Scientifique. All rights reserved.  This file is         *)
-(*  distributed under the terms of the GNU Lesser General Public       *)
-(*  License, with the special exception on linking described in file   *)
-(*  ../LICENSE.                                                        *)
-(*                                                                     *)
-(***********************************************************************)
-
-(*
-  Time-stamp: <Last modified on 2013-03-13 18:30:59 CET by Kim Nguyen>
-*)
-
-include module type of Hlist_sig
-
-module Make (H : Hcons.Abstract) : S with type elt = H.t
-(** Builds an implementation of hashconsed lists of hashconsed elements.
-    See {!Hcons.Make}.
-*)
-
-module Weak (H : Hcons.Abstract) : S with type elt = H.t
-(** Builds an implementation of hashconsed lists of hashconsed elements
-    with weak internal storage. See {!Hcons.Weak}.
-*)
diff --git a/src/utils/hlist_sig.ml b/src/utils/hlist_sig.ml
deleted file mode 100644
index 227768c..0000000
--- a/src/utils/hlist_sig.ml
+++ /dev/null
@@ -1,35 +0,0 @@
-(***********************************************************************)
-(*                                                                     *)
-(*                               TAToo                                 *)
-(*                                                                     *)
-(*                     Kim Nguyen, LRI UMR8623                         *)
-(*                   Université Paris-Sud & CNRS                       *)
-(*                                                                     *)
-(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(*  Recherche Scientifique. All rights reserved.  This file is         *)
-(*  distributed under the terms of the GNU Lesser General Public       *)
-(*  License, with the special exception on linking described in file   *)
-(*  ../LICENSE.                                                        *)
-(*                                                                     *)
-(***********************************************************************)
-
-(*
-  Time-stamp: <Last modified on 2013-03-13 18:21:28 CET by Kim Nguyen>
-*)
-type ('a,'b) node = Nil | Cons of ('a * 'b)
-
-module type S = sig
-  type elt
-  include Hcons.S
-  val nil : t
-  val cons : ?sorted:bool -> elt -> t -> t
-  val hd : t -> elt
-  val tl : t -> t
-  val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
-  val map : (elt -> elt) -> t -> t
-  val iter : (elt -> 'a) -> t -> unit
-  val rev : t -> t
-  val rev_map : (elt -> elt) -> t -> t
-  val length : t -> int
-  val mem : elt -> t -> bool
-end
diff --git a/src/utils/misc.ml b/src/utils/misc.ml
deleted file mode 100644
index f8156b0..0000000
--- a/src/utils/misc.ml
+++ /dev/null
@@ -1,51 +0,0 @@
-(***********************************************************************)
-(*                                                                     *)
-(*                               TAToo                                 *)
-(*                                                                     *)
-(*                     Kim Nguyen, LRI UMR8623                         *)
-(*                   Université Paris-Sud & CNRS                       *)
-(*                                                                     *)
-(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(*  Recherche Scientifique. All rights reserved.  This file is         *)
-(*  distributed under the terms of the GNU Lesser General Public       *)
-(*  License, with the special exception on linking described in file   *)
-(*  ../LICENSE.                                                        *)
-(*                                                                     *)
-(***********************************************************************)
-
-(*
-  Time-stamp: <Last modified on 2013-03-04 23:00:19 CET by Kim Nguyen>
-*)
-
-(** Various generic signatures and generic module and functor definitions
-*)
-INCLUDE "utils.ml"
-
-module HashSet (H : Hashtbl.HashedType) :
-  Common_sig.HashSet with type data = H.t =
-struct
-  module T = Hashtbl.Make(H)
-  type data = H.t
-  type t = data T.t
-  let create = T.create
-  let add h v = T.add h v v
-  let find = T.find
-  let remove = T.remove
-  let find_all = T.find_all
-  let clear = T.clear
-  let mem = T.mem
-end
-
-module Pair (X : Common_sig.Type) (Y : Common_sig.Type) :
-  Common_sig.Type with type t = X.t * Y.t =
-struct
-  type t = X.t * Y.t
-  let hash (x, y) = HASHINT2(X.hash x, Y.hash y)
-  let compare (x1, y1) (x2, y2) =
-    let r = X.compare x1 x2 in
-    if r != 0 then r else Y.compare y1 y2
-  let equal p1 p2 =
-    p1 == p2 ||
-      let x1, y1 = p1
-      and x2, y2 = p2 in X.equal x1 x2 && Y.equal y1 y2
-end
diff --git a/src/utils/pretty.ml b/src/utils/pretty.ml
deleted file mode 100644
index 1927216..0000000
--- a/src/utils/pretty.ml
+++ /dev/null
@@ -1,151 +0,0 @@
-(***********************************************************************)
-(*                                                                     *)
-(*                               TAToo                                 *)
-(*                                                                     *)
-(*                     Kim Nguyen, LRI UMR8623                         *)
-(*                   Université Paris-Sud & CNRS                       *)
-(*                                                                     *)
-(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(*  Recherche Scientifique. All rights reserved.  This file is         *)
-(*  distributed under the terms of the GNU Lesser General Public       *)
-(*  License, with the special exception on linking described in file   *)
-(*  ../LICENSE.                                                        *)
-(*                                                                     *)
-(***********************************************************************)
-
-(*
-  Time-stamp: <Last modified on 2013-03-09 10:41:21 CET by Kim Nguyen>
-*)
-
-open Format
-
-exception InvalidUtf8Codepoint of int
-
-let subscripts = "₀₁₂₃₄₅₆₇₈₉"
-let superscripts = "⁰¹²³⁴⁵⁶⁷⁸⁹"
-
-let char_length c =
-  let code = Char.code c in
-    if code <= 0x7f then 1
-    else if 0xc2 <= code && code <= 0xdf then 2
-    else if 0xe0 <= code && code <= 0xef then 3
-    else if 0xf0 <= code && code <= 0xf4 then 4
-    else raise (InvalidUtf8Codepoint code)
-
-
-let next_char s i len =
-  let n = i + char_length s.[i] in
-    if n >= len then -1 else n
-
-let str_len s =
-  let len = String.length s in
-  let rec loop i acc =
-    if i == -1 then acc
-    else loop (next_char s i len) (acc+1)
-  in
-    loop 0 0
-
-let length = str_len
-
-let get_char s i =
-  let len = String.length s in
-  let rec loop j count =
-    if count == i then String.sub s j (char_length s.[j])
-    else loop (next_char s j len) (count+1)
-  in
-    loop 0 0
-
-
-let format_number digits i =
-  let s = string_of_int i in
-  let len = String.length s in
-  let buf = Buffer.create (len*4) in
-    for i = 0 to len - 1 do
-      let d = Char.code s.[i] - Char.code '0' in
-	Buffer.add_string buf (get_char digits d)
-    done;
-    Buffer.contents buf
-
-let rev_explode s =
-  let len = str_len s in
-  let rec loop i acc =
-      if i >= len then acc
-      else
-	loop (i+1) ((get_char s i) :: acc)
-  in
-      loop 0 []
-
-
-let explode s = List.rev (rev_explode s)
-
-let combine_all comp s =
-  let l = rev_explode s in
-  String.concat "" (List.fold_left (fun acc e -> comp::e::acc) [] l)
-
-
-let subscript = format_number subscripts
-let superscript = format_number superscripts
-let down_arrow = "↓"
-let up_arrow = "↑"
-let right_arrow = "→"
-let left_arrow =  "←"
-let epsilon = "ϵ"
-let big_sigma = "∑"
-let cap = "∩"
-let cup = "∪"
-let lnot = "¬"
-let wedge = "∧"
-let vee = "∨"
-let top = "⊤"
-let bottom = "⊥"
-let dummy = "☠"
-let inverse = "⁻¹"
-let double_right_arrow = "⇒"
-let combining_overbar = "\204\133"
-let combining_underbar = "\204\178"
-let combining_stroke = "\204\182"
-let combining_vertical_line = "\226\131\146"
-
-
-let overline s = combine_all combining_overbar s
-let underline s = combine_all combining_underbar s
-let strike s = combine_all combining_stroke s
-
-let padding i = String.make i ' '
-let line i = String.make i '_'
-
-
-
-
-let ppf f fmt s =
-  pp_print_string fmt (f s)
-
-let pp_overline = ppf overline
-let pp_underline = ppf underline
-let pp_strike = ppf strike
-let pp_subscript = ppf subscript
-let pp_superscript = ppf superscript
-let dummy_printer _ () = ()
-
-let pp_print_list ?(sep=dummy_printer) printer fmt l =
-  match l with
-    [] -> ()
-  | [ e ] -> printer fmt e
-  | e :: es -> printer fmt e; List.iter
-    (fun x ->
-      sep fmt ();
-      fprintf fmt "%a" printer x) es
-
-let pp_print_array ?(sep=dummy_printer) printer fmt a =
-  pp_print_list ~sep:sep printer fmt (Array.to_list a)
-
-let print_list ?(sep=" ") printer fmt l =
-  let sep_printer fmt () =
-    pp_print_string fmt sep
-  in
-  pp_print_list ~sep:sep_printer printer fmt l
-
-let print_array ?(sep=" ") printer fmt a =
-  print_list ~sep:sep printer fmt (Array.to_list a)
-
-
diff --git a/src/utils/pretty.mli b/src/utils/pretty.mli
deleted file mode 100644
index 9064f8a..0000000
--- a/src/utils/pretty.mli
+++ /dev/null
@@ -1,57 +0,0 @@
-(***********************************************************************)
-(*                                                                     *)
-(*                               TAToo                                 *)
-(*                                                                     *)
-(*                     Kim Nguyen, LRI UMR8623                         *)
-(*                   Université Paris-Sud & CNRS                       *)
-(*                                                                     *)
-(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(*  Recherche Scientifique. All rights reserved.  This file is         *)
-(*  distributed under the terms of the GNU Lesser General Public       *)
-(*  License, with the special exception on linking described in file   *)
-(*  ../LICENSE.                                                        *)
-(*                                                                     *)
-(***********************************************************************)
-
-(*
-  Time-stamp: <Last modified on 2013-03-09 10:41:32 CET by Kim Nguyen>
-*)
-
-exception InvalidUtf8Codepoint of int
-
-val subscript : int -> string
-val superscript : int -> string
-val down_arrow : string
-val up_arrow : string
-val right_arrow : string
-val left_arrow : string
-val epsilon : string
-val big_sigma : string
-val cap : string
-val cup : string
-val lnot : string
-val wedge : string
-val vee : string
-val top : string
-val bottom : string
-val dummy : string
-val inverse : string
-val double_right_arrow : string
-val overline : string -> string
-val underline : string -> string
-val strike : string -> string
-val padding : int -> string
-val line : int -> string
-val length : string -> int
-val pp_overline : Format.formatter -> string -> unit
-val pp_underline : Format.formatter -> string -> unit
-val pp_strike : Format.formatter -> string -> unit
-val pp_subscript : Format.formatter -> int -> unit
-val pp_superscript : Format.formatter -> int -> unit
-
-val pp_print_list :
-  ?sep:(Format.formatter -> unit -> unit) -> (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a list -> unit
-val pp_print_array :
-  ?sep:(Format.formatter -> unit -> unit) -> (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a array -> unit
-val print_list : ?sep:string -> (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a list -> unit
-val print_array : ?sep:string -> (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a array -> unit
diff --git a/src/utils/ptset.ml b/src/utils/ptset.ml
deleted file mode 100644
index f9bbd03..0000000
--- a/src/utils/ptset.ml
+++ /dev/null
@@ -1,381 +0,0 @@
-(* Original file: *)
-(***********************************************************************)
-(*                                                                     *)
-(*  Copyright (C) Jean-Christophe Filliatre                            *)
-(*                                                                     *)
-(*  This software is free software; you can redistribute it and/or     *)
-(*  modify it under the terms of the GNU Library General Public        *)
-(*  License version 2.1, with the special exception on linking         *)
-(*  described in file http://www.lri.fr/~filliatr/ftp/ocaml/ds/LICENSE *)
-(*                                                                     *)
-(*  This software is distributed in the hope that it will be useful,   *)
-(*  but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
-(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.               *)
-(*                                                                     *)
-(***********************************************************************)
-
-(*
-  Time-stamp: <Last modified on 2013-03-10 18:18:54 CET by Kim Nguyen>
-*)
-
-(* Modified by Kim Nguyen *)
-(* The Patricia trees are themselves deeply hash-consed. The module
-   provides a Make (and Weak) functor to build hash-consed patricia
-   trees whose elements are Abstract hash-consed values.
-*)
-
-INCLUDE "utils.ml"
-
-include Ptset_sig
-
-module type HConsBuilder =
-  functor (H : Common_sig.HashedType) -> Hcons.S with type data = H.t
-
-module Builder (HCB : HConsBuilder) (H : Hcons.Abstract) :
-  S with type elt = H.t =
-struct
-  type elt = H.t
-
-  type 'a set =
-    | Empty
-    | Leaf of elt
-    | Branch of int * int * 'a * 'a
-
-  module rec Node : Hcons.S with type data = Data.t = HCB(Data)
-                            and Data : Common_sig.HashedType with type t = Node.t set =
-  struct
-    type t =  Node.t set
-    let equal x y =
-      match x,y with
-      | Empty,Empty -> true
-      | Leaf k1, Leaf k2 ->  k1 == k2
-      | Branch(b1,i1,l1,r1), Branch(b2,i2,l2,r2) ->
-          b1 == b2 && i1 == i2 && (Node.equal l1 l2) && (Node.equal r1 r2)
-
-      | (Empty|Leaf _|Branch _), _  -> false
-
-    let hash = function
-    | Empty -> 0
-    | Leaf i -> HASHINT2 (PRIME1, Uid.to_int (H.uid i))
-    | Branch (b,i,l,r) ->
-        HASHINT4(b, i, Uid.to_int l.Node.id, Uid.to_int r.Node.id)
-  end
-
-  include Node
-
-  let empty = Node.make Empty
-
-  let is_empty s = (Node.node s) == Empty
-
-  let branch p m l r = Node.make (Branch(p,m,l,r))
-
-  let leaf k = Node.make (Leaf k)
-
-                            (* To enforce the invariant that a branch contains two non empty
-                               sub-trees *)
-  let branch_ne p m t0 t1 =
-    if (is_empty t0) then t1
-    else if is_empty t1 then t0 else branch p m t0 t1
-
-                            (******** from here on, only use the smart constructors ************)
-
-  let zero_bit k m = (k land m) == 0
-
-  let singleton k = leaf k
-
-  let is_singleton n =
-    match Node.node n with
-      | Leaf _ -> true
-      | Branch _ | Empty -> false
-
-  let mem (k:elt) n =
-    let kid = Uid.to_int (H.uid k) in
-    let rec loop n = match Node.node n with
-    | Empty -> false
-    | Leaf j ->  k == j
-    | Branch (p, _, l, r) -> if kid <= p then loop l else loop r
-    in loop n
-
-  let rec min_elt n = match Node.node n with
-  | Empty -> raise Not_found
-  | Leaf k -> k
-  | Branch (_,_,s,_) -> min_elt s
-
-  let rec max_elt n = match Node.node n with
-  | Empty -> raise Not_found
-  | Leaf k -> k
-  | Branch (_,_,_,t) -> max_elt t
-
-  let elements s =
-    let rec elements_aux acc n = match Node.node n with
-    | Empty -> acc
-    | Leaf k -> k :: acc
-    | Branch (_,_,l,r) -> elements_aux (elements_aux acc r) l
-    in
-    elements_aux [] s
-
-  let mask k m  = (k lor (m-1)) land (lnot m)
-
-  let naive_highest_bit x =
-    assert (x < 256);
-    let rec loop i =
-      if i = 0 then 1 else if x lsr i = 1 then 1 lsl i else loop (i-1)
-    in
-    loop 7
-
-  let hbit = Array.init 256 naive_highest_bit
-  (*
-    external clz : int -> int = "caml_clz" "noalloc"
-    external leading_bit : int -> int = "caml_leading_bit" "noalloc"
-  *)
-  let highest_bit x =
-    try
-      let n = (x) lsr 24 in
-      if n != 0 then  hbit.(n) lsl 24
-      else let n = (x) lsr 16 in if n != 0 then hbit.(n) lsl 16
-        else let n = (x) lsr 8 in if n != 0 then hbit.(n) lsl 8
-          else hbit.(x)
-    with
-      _ -> raise (Invalid_argument ("highest_bit " ^ (string_of_int x)))
-
-  let highest_bit64 x =
-    let n = x lsr 32 in if n != 0 then highest_bit n lsl 32
-      else highest_bit x
-
-  let branching_bit p0 p1 = highest_bit64 (p0 lxor p1)
-
-  let join p0 t0 p1 t1 =
-    let m = branching_bit p0 p1  in
-    let msk = mask p0 m in
-    if zero_bit p0 m then
-    branch_ne msk m t0 t1
-    else
-    branch_ne msk m t1 t0
-
-  let match_prefix k p m = (mask k m) == p
-
-  let add k t =
-    let kid = Uid.to_int (H.uid k) in
-    assert (kid >=0);
-    let rec ins n = match Node.node n with
-    | Empty -> leaf k
-    | Leaf j ->  if j == k then n else join kid (leaf k) (Uid.to_int (H.uid j)) n
-    | Branch (p,m,t0,t1)  ->
-        if match_prefix kid p m then
-        if zero_bit kid m then
-        branch_ne p m (ins t0) t1
-        else
-        branch_ne p m t0 (ins t1)
-        else
-        join kid (leaf k)  p n
-    in
-    ins t
-
-  let remove k t =
-    let kid = Uid.to_int(H.uid k) in
-    let rec rmv n = match Node.node n with
-    | Empty -> empty
-    | Leaf j  -> if  k == j then empty else n
-    | Branch (p,m,t0,t1) ->
-        if match_prefix kid p m then
-        if zero_bit kid m then
-        branch_ne p m (rmv t0) t1
-        else
-        branch_ne p m t0 (rmv t1)
-        else
-        n
-    in
-    rmv t
-
-  (* should run in O(1) thanks to hash consing *)
-
-  let equal a b = Node.equal a b
-
-  let compare a b = (Uid.to_int (Node.uid a)) - (Uid.to_int (Node.uid b))
-
-  let rec merge s t =
-    if equal s t (* This is cheap thanks to hash-consing *)
-    then s
-    else
-    match Node.node s, Node.node t with
-    | Empty, _  -> t
-    | _, Empty  -> s
-    | Leaf k, _ -> add k t
-    | _, Leaf k -> add k s
-    | Branch (p,m,s0,s1), Branch (q,n,t0,t1) ->
-        if m == n && match_prefix q p m then
-        branch p  m  (merge s0 t0) (merge s1 t1)
-        else if m > n && match_prefix q p m then
-        if zero_bit q m then
-        branch_ne p m (merge s0 t) s1
-        else
-        branch_ne p m s0 (merge s1 t)
-        else if m < n && match_prefix p q n then
-        if zero_bit p n then
-        branch_ne q n (merge s t0) t1
-        else
-        branch_ne q n t0 (merge s t1)
-        else
-                                  (* The prefixes disagree. *)
-        join p s q t
-
-
-
-
-  let rec subset s1 s2 = (equal s1 s2) ||
-    match (Node.node s1,Node.node s2) with
-    | Empty, _ -> true
-    | _, Empty -> false
-    | Leaf k1, _ -> mem k1 s2
-    | Branch _, Leaf _ -> false
-    | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
-        if m1 == m2 && p1 == p2 then
-        subset l1 l2 && subset r1 r2
-        else if m1 < m2 && match_prefix p1 p2 m2 then
-        if zero_bit p1 m2 then
-        subset l1 l2 && subset r1 l2
-        else
-        subset l1 r2 && subset r1 r2
-        else
-        false
-
-
-  let union s1 s2 = merge s1 s2
-                            (* Todo replace with e Memo Module *)
-
-  let rec inter s1 s2 =
-    if equal s1 s2
-    then s1
-    else
-    match (Node.node s1,Node.node s2) with
-    | Empty, _ -> empty
-    | _, Empty -> empty
-    | Leaf k1, _ -> if mem k1 s2 then s1 else empty
-    | _, Leaf k2 -> if mem k2 s1 then s2 else empty
-    | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
-        if m1 == m2 && p1 == p2 then
-        merge (inter l1 l2)  (inter r1 r2)
-        else if m1 > m2 && match_prefix p2 p1 m1 then
-        inter (if zero_bit p2 m1 then l1 else r1) s2
-        else if m1 < m2 && match_prefix p1 p2 m2 then
-        inter s1 (if zero_bit p1 m2 then l2 else r2)
-        else
-        empty
-
-  let rec diff s1 s2 =
-    if equal s1 s2
-    then empty
-    else
-    match (Node.node s1,Node.node s2) with
-    | Empty, _ -> empty
-    | _, Empty -> s1
-    | Leaf k1, _ -> if mem k1 s2 then empty else s1
-    | _, Leaf k2 -> remove k2 s1
-    | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
-        if m1 == m2 && p1 == p2 then
-        merge (diff l1 l2) (diff r1 r2)
-        else if m1 > m2 && match_prefix p2 p1 m1 then
-        if zero_bit p2 m1 then
-        merge (diff l1 s2) r1
-        else
-        merge l1 (diff r1 s2)
-        else if m1 < m2 && match_prefix p1 p2 m2 then
-        if zero_bit p1 m2 then diff s1 l2 else diff s1 r2
-        else
-        s1
-
-
-  (*s All the following operations ([cardinal], [iter], [fold], [for_all],
-    [exists], [filter], [partition], [choose], [elements]) are
-    implemented as for any other kind of binary trees. *)
-
-  let rec cardinal n = match Node.node n with
-  | Empty -> 0
-  | Leaf _ -> 1
-  | Branch (_,_,t0,t1) -> cardinal t0 + cardinal t1
-
-  let rec iter f n = match Node.node n with
-  | Empty -> ()
-  | Leaf k -> f k
-  | Branch (_,_,t0,t1) -> iter f t0; iter f t1
-
-  let rec fold f s accu = match Node.node s with
-  | Empty -> accu
-  | Leaf k -> f k accu
-  | Branch (_,_,t0,t1) -> fold f t0 (fold f t1 accu)
-
-
-  let rec for_all p n = match Node.node n with
-  | Empty -> true
-  | Leaf k -> p k
-  | Branch (_,_,t0,t1) -> for_all p t0 && for_all p t1
-
-  let rec exists p n = match Node.node n with
-  | Empty -> false
-  | Leaf k -> p k
-  | Branch (_,_,t0,t1) -> exists p t0 || exists p t1
-
-  let rec filter pr n = match Node.node n with
-  | Empty -> empty
-  | Leaf k -> if pr k then n else empty
-  | Branch (p,m,t0,t1) -> branch_ne p m (filter pr t0) (filter pr t1)
-
-  let partition p s =
-    let rec part (t,f as acc) n = match Node.node n with
-    | Empty -> acc
-    | Leaf k -> if p k then (add k t, f) else (t, add k f)
-    | Branch (_,_,t0,t1) -> part (part acc t0) t1
-    in
-    part (empty, empty) s
-
-  let rec choose n = match Node.node n with
-  | Empty -> raise Not_found
-  | Leaf k -> k
-  | Branch (_, _,t0,_) -> choose t0   (* we know that [t0] is non-empty *)
-
-
-  let split x s =
-    let coll k (l, b, r) =
-      if k < x then add k l, b, r
-      else if k > x then l, b, add k r
-      else l, true, r
-    in
-    fold coll s (empty, false, empty)
-
-  (*s Additional functions w.r.t to [Set.S]. *)
-
-  let rec intersect s1 s2 = (equal s1 s2) ||
-    match (Node.node s1,Node.node s2) with
-    | Empty, _ -> false
-    | _, Empty -> false
-    | Leaf k1, _ -> mem k1 s2
-    | _, Leaf k2 -> mem k2 s1
-    | Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
-        if m1 == m2 && p1 == p2 then
-        intersect l1 l2 || intersect r1 r2
-        else if m1 > m2 && match_prefix p2 p1 m1 then
-        intersect (if zero_bit p2 m1 then l1 else r1) s2
-        else if m1 < m2 && match_prefix p1 p2 m2 then
-        intersect s1 (if zero_bit p1 m2 then l2 else r2)
-        else
-        false
-
-
-  let from_list l = List.fold_left (fun acc e -> add e acc) empty l
-
-
-end
-
-module Make = Builder(Hcons.Make)
-module Weak = Builder(Hcons.Weak)
-
-module PosInt
-  =
-struct
-  include Make(Hcons.PosInt)
-  let print ppf s =
-    Format.pp_print_string ppf "{ ";
-    iter (fun i -> Format.fprintf ppf "%i " i) s;
-    Format.pp_print_string ppf "}";
-    Format.pp_print_flush ppf ()
-end
diff --git a/src/utils/ptset.mli b/src/utils/ptset.mli
deleted file mode 100644
index f4f53f7..0000000
--- a/src/utils/ptset.mli
+++ /dev/null
@@ -1,33 +0,0 @@
-(***********************************************************************)
-(*                                                                     *)
-(*                               TAToo                                 *)
-(*                                                                     *)
-(*                     Kim Nguyen, LRI UMR8623                         *)
-(*                   Université Paris-Sud & CNRS                       *)
-(*                                                                     *)
-(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(*  Recherche Scientifique. All rights reserved.  This file is         *)
-(*  distributed under the terms of the GNU Lesser General Public       *)
-(*  License, with the special exception on linking described in file   *)
-(*  ../LICENSE.                                                        *)
-(*                                                                     *)
-(***********************************************************************)
-
-(*
-  Time-stamp: <Last modified on 2013-03-04 22:42:37 CET by Kim Nguyen>
-*)
-
-include module type of Ptset_sig
-
-module Make (H : Hcons.Abstract) : S with type elt = H.t
-(** Builds an implementation of hashconsed sets of hashconsed elements.
-    See {!Hcons.Make}.
-*)
-
-module Weak (H : Hcons.Abstract) : S with type elt = H.t
-(** Builds an implementation of hashconsed sets of hashconsed elements
-    with weak internal storage. See {!Hcons.Weak}.
-*)
-
-module PosInt : S with type elt = int
-(** Implementation of hashconsed sets of positive integers *)
diff --git a/src/utils/ptset_sig.ml b/src/utils/ptset_sig.ml
deleted file mode 100644
index f37f6ba..0000000
--- a/src/utils/ptset_sig.ml
+++ /dev/null
@@ -1,24 +0,0 @@
-(***********************************************************************)
-(*                                                                     *)
-(*                               TAToo                                 *)
-(*                                                                     *)
-(*                     Kim Nguyen, LRI UMR8623                         *)
-(*                   Université Paris-Sud & CNRS                       *)
-(*                                                                     *)
-(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(*  Recherche Scientifique. All rights reserved.  This file is         *)
-(*  distributed under the terms of the GNU Lesser General Public       *)
-(*  License, with the special exception on linking described in file   *)
-(*  ../LICENSE.                                                        *)
-(*                                                                     *)
-(***********************************************************************)
-
-(*
-  Time-stamp: <Last modified on 2013-03-04 23:32:36 CET by Kim Nguyen>
-*)
-
-module type S =
-sig
-  include Hcons.S
-  include Common_sig.Set with type t := t
-end
diff --git a/src/utils/qName.ml b/src/utils/qName.ml
deleted file mode 100644
index 4a3aac4..0000000
--- a/src/utils/qName.ml
+++ /dev/null
@@ -1,47 +0,0 @@
-(***********************************************************************)
-(*                                                                     *)
-(*                               TAToo                                 *)
-(*                                                                     *)
-(*                     Kim Nguyen, LRI UMR8623                         *)
-(*                   Université Paris-Sud & CNRS                       *)
-(*                                                                     *)
-(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(*  Recherche Scientifique. All rights reserved.  This file is         *)
-(*  distributed under the terms of the GNU Lesser General Public       *)
-(*  License, with the special exception on linking described in file   *)
-(*  ../LICENSE.                                                        *)
-(*                                                                     *)
-(***********************************************************************)
-
-(*
-  Time-stamp: <Last modified on 2013-03-10 23:05:56 CET by Kim Nguyen>
-*)
-
-include Hcons.Make (struct
-  include String
-  let hash s = Hashtbl.hash s
-  let equal s1 s2 = s1 = s2
-end)
-
-let print pp s = Format.fprintf pp "%s" s.node
-
-let of_string = make
-let to_string = node
-
-let document = of_string "#document"
-let text = of_string "#text"
-let comment = of_string "#comment"
-let nil = of_string "#"
-
-let attribute t = of_string ( "@" ^ (to_string t))
-let processing_instruction t = of_string ( "?" ^ (to_string t))
-
-let remove_prefix t =
-  let s = to_string t in
-  let lens = String.length s in
-  if lens == 0 then t
-  else
-    if s.[0] == '@' || s.[0] == '?' then
-      of_string (String.sub s 1 (lens-1))
-    else
-      t
diff --git a/src/utils/qName.mli b/src/utils/qName.mli
deleted file mode 100644
index 978ba3c..0000000
--- a/src/utils/qName.mli
+++ /dev/null
@@ -1,70 +0,0 @@
-(***********************************************************************)
-(*                                                                     *)
-(*                               TAToo                                 *)
-(*                                                                     *)
-(*                     Kim Nguyen, LRI UMR8623                         *)
-(*                   Université Paris-Sud & CNRS                       *)
-(*                                                                     *)
-(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(*  Recherche Scientifique. All rights reserved.  This file is         *)
-(*  distributed under the terms of the GNU Lesser General Public       *)
-(*  License, with the special exception on linking described in file   *)
-(*  ../LICENSE.                                                        *)
-(*                                                                     *)
-(***********************************************************************)
-
-(*
-  Time-stamp: <Last modified on 2013-03-10 23:02:12 CET by Kim Nguyen>
-*)
-
-(** Implementation of qualified names as hashconsed strings *)
-
-include Hcons.S with type data = string
-include Common_sig.Printable with type t := t
-
-
-val of_string : string -> t
-(** Utility function, equivalent to [make] *)
-
-val to_string : t -> string
-(** Utility function, equivalent to [node] *)
-
-
-(** Special constants, that denote the QName of nodes that are not
-    elements (using the nodeValue property of DOM for such nodes.
-*)
-
-val document : t
-(** Represents the QName of a document node. Equivalent to
-    [of_string "#document"]
-*)
-
-val text : t
-(** Represents the QName of a text node. Equivalent to
-    [of_string "#text"]
-*)
-
-val comment : t
-(** Represents the QName of a comment node. Equivalent to
-    [of_string "#comment"]
-*)
-
-val nil : t
-(** Represents the QName of a nil node. Equivalent to
-    [of_string "#"]
-*)
-
-val attribute : t -> t
-(** Adds a prefix character (@) to distinguish the name
-    from an element name
-*)
-
-val processing_instruction : t -> t
-(** Adds a prefix character (?) to distinguish the name
-    from an element name
-*)
-
-val remove_prefix : t -> t
-(** Removes the prefix of the qname given as argument. Does not
-    do anything if there is no prefix.
-*)
diff --git a/src/utils/qNameSet.ml b/src/utils/qNameSet.ml
deleted file mode 100644
index d895ff3..0000000
--- a/src/utils/qNameSet.ml
+++ /dev/null
@@ -1,49 +0,0 @@
-(***********************************************************************)
-(*                                                                     *)
-(*                               TAToo                                 *)
-(*                                                                     *)
-(*                     Kim Nguyen, LRI UMR8623                         *)
-(*                   Université Paris-Sud & CNRS                       *)
-(*                                                                     *)
-(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(*  Recherche Scientifique. All rights reserved.  This file is         *)
-(*  distributed under the terms of the GNU Lesser General Public       *)
-(*  License, with the special exception on linking described in file   *)
-(*  ../LICENSE.                                                        *)
-(*                                                                     *)
-(***********************************************************************)
-
-(*
-  Time-stamp: <Last modified on 2013-03-09 17:54:35 CET by Kim Nguyen>
-*)
-
-include FiniteCofinite.Make(Ptset.Make(QName))
-
-let print_finite fmt e conv =
-  Format.fprintf fmt "{";
-  Pretty.print_list ~sep:"," QName.print fmt (conv e);
-  Format.fprintf fmt "}"
-
-let printer fmt e test conv inv is_any =
-  if test e then print_finite fmt e conv
-  else
-    let () = Format.fprintf fmt "%s" Pretty.big_sigma in
-    if not (is_any e) then begin Format.fprintf fmt "-";print_finite fmt (inv e) conv end
-
-let print fmt e = printer fmt e is_finite elements complement is_any
-
-let specials = [ QName.document; QName.text; QName.text ]
-let notstar = from_list specials
-let star = diff any notstar
-let node = any
-let text = singleton QName.text
-
-module Weak =
-struct
-  include FiniteCofinite.Weak(Ptset.Weak(QName))
-  let print fmt e =  printer fmt e is_finite elements complement is_any
-  let notstar = from_list specials
-  let star = diff any notstar
-  let node = any
-  let text = singleton QName.text
-end
diff --git a/src/utils/qNameSet.mli b/src/utils/qNameSet.mli
deleted file mode 100644
index 132d834..0000000
--- a/src/utils/qNameSet.mli
+++ /dev/null
@@ -1,36 +0,0 @@
-(***********************************************************************)
-(*                                                                     *)
-(*                               TAToo                                 *)
-(*                                                                     *)
-(*                     Kim Nguyen, LRI UMR8623                         *)
-(*                   Université Paris-Sud & CNRS                       *)
-(*                                                                     *)
-(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(*  Recherche Scientifique. All rights reserved.  This file is         *)
-(*  distributed under the terms of the GNU Lesser General Public       *)
-(*  License, with the special exception on linking described in file   *)
-(*  ../LICENSE.                                                        *)
-(*                                                                     *)
-(***********************************************************************)
-
-(*
-  Time-stamp: <Last modified on 2013-03-09 17:53:53 CET by Kim Nguyen>
-*)
-
-(** Implementation of sets of Qualified Names that can be finite
-    or cofinite *)
-
-include FiniteCofinite.S with type elt = QName.t
-include Common_sig.Printable with type t := t
-val star : t
-val text : t
-val node : t
-
-module Weak :
-sig
-  include FiniteCofinite.S with type elt = QName.t
-  include Common_sig.Printable with type t := t
-  val star : t
-  val text : t
-  val node : t
-end
diff --git a/src/utils/uid.ml b/src/utils/uid.ml
deleted file mode 100644
index 0cb9688..0000000
--- a/src/utils/uid.ml
+++ /dev/null
@@ -1,33 +0,0 @@
-(***********************************************************************)
-(*                                                                     *)
-(*                               TAToo                                 *)
-(*                                                                     *)
-(*                     Kim Nguyen, LRI UMR8623                         *)
-(*                   Université Paris-Sud & CNRS                       *)
-(*                                                                     *)
-(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(*  Recherche Scientifique. All rights reserved.  This file is         *)
-(*  distributed under the terms of the GNU Lesser General Public       *)
-(*  License, with the special exception on linking described in file   *)
-(*  ../LICENSE.                                                        *)
-(*                                                                     *)
-(***********************************************************************)
-
-(*
-  Time-stamp: <Last modified on 2013-01-30 19:06:39 CET by Kim Nguyen>
-*)
-
-type t = int
-
-exception Overflow
-let make_maker () =
-  let _id = ref ~-1 in
-    fun () ->
-      incr _id;
-      let i = !_id in
-      if i < 0 then raise Overflow else i
-
-let dummy = -1
-
-external to_int : t -> int = "%identity"
-external of_int : int -> t= "%identity"
diff --git a/src/utils/uid.mli b/src/utils/uid.mli
deleted file mode 100644
index 286cacc..0000000
--- a/src/utils/uid.mli
+++ /dev/null
@@ -1,45 +0,0 @@
-(***********************************************************************)
-(*                                                                     *)
-(*                               TAToo                                 *)
-(*                                                                     *)
-(*                     Kim Nguyen, LRI UMR8623                         *)
-(*                   Université Paris-Sud & CNRS                       *)
-(*                                                                     *)
-(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
-(*  Recherche Scientifique. All rights reserved.  This file is         *)
-(*  distributed under the terms of the GNU Lesser General Public       *)
-(*  License, with the special exception on linking described in file   *)
-(*  ../LICENSE.                                                        *)
-(*                                                                     *)
-(***********************************************************************)
-
-(*
-  Time-stamp: <Last modified on 2013-01-30 19:06:33 CET by Kim Nguyen>
-*)
-
-(** This modules implements unique identifiers represented by integers *)
-
-type t = private int
-(** The type of unique identifiers. *)
-
-exception Overflow
-(** Raised when the internal counters for IDs overflows. *)
-
-val make_maker : unit -> (unit -> t)
-(** Returns an uid generator.
-    [make_maker ()] returns a function that generates unique ids. Raises
-    [Overflow] if the internal counter overflows.
-*)
-
-val dummy : t
-(** A dummy identifier, guaranteed to be distinct from any value
-    returned by a generator.
-*)
-
-external to_int : t -> int = "%identity"
-(** Convert a unique id to an integer *)
-
-(**/**)
-
-external of_int : int -> t = "%identity"
-(** May break the invariant, use with caution *)
diff --git a/src/xpath/ast.ml b/src/xpath/ast.ml
index 64c6c8d..a90a41b 100644
--- a/src/xpath/ast.ml
+++ b/src/xpath/ast.ml
@@ -14,10 +14,9 @@
 (***********************************************************************)
 
 (*
-  Time-stamp: <Last modified on 2013-03-13 10:59:20 CET by Kim Nguyen>
+  Time-stamp: <Last modified on 2013-04-04 18:43:04 CEST by Kim Nguyen>
 *)
 
-open Utils
 
 type path = single_path list
 and single_path = Absolute of step list | Relative of step list
@@ -30,7 +29,7 @@ and axis = Self | Attribute | Child
            | PrecedingSibling
            | Preceding | Following
 
-and test = QNameSet.t * Tree.Common.NodeKind.t
+and test = QNameSet.t * Tree.NodeKind.t
 
 and binop = Eq | Neq | Lt | Gt | Lte | Gte | Or | And | Add | Sub | Mult | Div | Mod
 and unop =  Neg
@@ -128,7 +127,7 @@ and print_axis fmt a = pp fmt "%s" begin
 end
 
 and print_test fmt (ts,kind) =
-  let open Tree.Common.NodeKind in
+  let open Tree.NodeKind in
     match kind with
       Text -> pp fmt "%s" "text()"
     | Element | Attribute ->
diff --git a/src/xpath/ast.mli b/src/xpath/ast.mli
index 0fc63d4..78dd7bb 100644
--- a/src/xpath/ast.mli
+++ b/src/xpath/ast.mli
@@ -14,7 +14,7 @@
 (***********************************************************************)
 
 (*
-  Time-stamp: <Last modified on 2013-03-13 10:59:27 CET by Kim Nguyen>
+  Time-stamp: <Last modified on 2013-04-04 18:41:03 CEST by Kim Nguyen>
 *)
 
 type path = single_path list
@@ -28,21 +28,21 @@ and axis = Self | Attribute | Child
            | PrecedingSibling
            | Preceding | Following
 
-and test = Utils.QNameSet.t * Tree.Common.NodeKind.t
+and test = QNameSet.t * Tree.NodeKind.t
 
 and binop = Eq | Neq | Lt | Gt | Lte | Gte | Or | And | Add | Sub | Mult | Div | Mod
 and unop =  Neg
 and expr =
   | Number of [ `Int of int | `Float of float ]
   | String of string
-  | Fun_call of Utils.QName.t * expr list
+  | Fun_call of QName.t * expr list
   | Path of path
   | Binop of expr * binop * expr
   | Unop of unop * expr
 type t = path
-val text : Utils.QNameSet.t
-val node : Utils.QNameSet.t
-val star : Utils.QNameSet.t
+val text : QNameSet.t
+val node : QNameSet.t
+val star : QNameSet.t
 val print_binop : Format.formatter -> binop -> unit
 val print_unop : Format.formatter -> unop -> unit
 val print_path : Format.formatter -> path -> unit
diff --git a/src/xpath/compile.ml b/src/xpath/compile.ml
index 0038506..e62b918 100644
--- a/src/xpath/compile.ml
+++ b/src/xpath/compile.ml
@@ -14,12 +14,10 @@
 (***********************************************************************)
 
 (*
-  Time-stamp: <Last modified on 2013-03-15 18:17:50 CET by Kim Nguyen>
+  Time-stamp: <Last modified on 2013-04-04 18:43:48 CEST by Kim Nguyen>
 *)
 
 open Ast
-open Auto
-open Utils
 
 
 let ( => ) a b = (a, b)
@@ -48,7 +46,7 @@ let root_set = QNameSet.singleton QName.document
 let compile_axis_test axis (test,kind) phi trans states =
   let q = State.make () in
   let phi = match kind with
-    Tree.Common.NodeKind.Node -> phi
+    Tree.NodeKind.Node -> phi
   | _ -> phi %% F.mk_kind kind
   in
   let phi', trans', states' =
@@ -145,7 +143,7 @@ and compile_single_path p trans states =
     match p with
     | Absolute steps ->
         (Ancestor false, (QNameSet.singleton QName.document,
-                          Tree.Common.NodeKind.Node), [])
+                          Tree.NodeKind.Node), [])
         :: steps
     | Relative steps -> steps
   in
@@ -181,7 +179,7 @@ let compile_top_level_step_list l trans states =
     | (axis, (test,kind), elist) :: ll ->
         let phi0, trans0, states0 =
           compile_axis_test (invert_axis axis)
-            (QNameSet.any, Tree.Common.NodeKind.Node)
+            (QNameSet.any, Tree.NodeKind.Node)
             phi_above trans states
         in
         (* Only select attribute nodes if the previous axis
@@ -219,7 +217,7 @@ let compile_top_level_step_list l trans states =
   let phi0, trans0, states0 =
     compile_axis_test
       Self
-      (QNameSet.singleton QName.document, Tree.Common.NodeKind.Node)
+      (QNameSet.singleton QName.document, Tree.NodeKind.Node)
       Ata.SFormula.true_
       trans
       states
diff --git a/src/xpath/compile.mli b/src/xpath/compile.mli
index 6f50f11..a326992 100644
--- a/src/xpath/compile.mli
+++ b/src/xpath/compile.mli
@@ -14,7 +14,7 @@
 (***********************************************************************)
 
 (*
-  Time-stamp: <Last modified on 2013-03-04 16:36:21 CET by Kim Nguyen>
+  Time-stamp: <Last modified on 2013-04-04 18:41:11 CEST by Kim Nguyen>
 *)
 
-val path : Ast.path -> Auto.Ata.t
+val path : Ast.path -> Ata.t
diff --git a/src/xpath/xpath_internal_parser.mly b/src/xpath/xpath_internal_parser.mly
index 9830e76..2a861aa 100644
--- a/src/xpath/xpath_internal_parser.mly
+++ b/src/xpath/xpath_internal_parser.mly
@@ -15,11 +15,11 @@
 (***********************************************************************)
 
 (*
-  Time-stamp: <Last modified on 2013-03-13 14:21:53 CET by Kim Nguyen>
+  Time-stamp: <Last modified on 2013-04-04 18:44:13 CEST by Kim Nguyen>
 *)
 
   open Ast
-  open Tree.Common
+  open Tree
 %}
 
 %token <string> TAG
@@ -103,12 +103,12 @@ step:
 axis_test:
   AXIS COLONCOLON test  { let a, (t,k) = $1, $3 in
                           match a with
-                            Attribute when Utils.QNameSet.is_finite t ->
-                              [ a, ((Utils.QNameSet.fold
+                            Attribute when QNameSet.is_finite t ->
+                              [ a, ((QNameSet.fold
                                        (fun t a ->
-                                         Utils.QNameSet.add
-                                           (Utils.QName.attribute t) a)
-                                       t Utils.QNameSet.empty), k) ]
+                                         QNameSet.add
+                                           (QName.attribute t) a)
+                                       t QNameSet.empty), k) ]
                           | Preceding|Following ->
                               [ (Descendant true, (t,k));
                                 if a == Preceding then
@@ -124,10 +124,10 @@ axis_test:
   let _ = Format.flush_str_formatter () in
   let () = Format.fprintf Format.str_formatter "%a" Ast.print_axis $1 in
   let a = Format.flush_str_formatter () in
-  [Child, (Utils.QNameSet.singleton (Utils.QName.of_string a),NodeKind.Element)]
+  [Child, (QNameSet.singleton (QName.of_string a),NodeKind.Element)]
 }
 | ATTNAME             {  [(Attribute,
-                           (Utils.QNameSet.singleton (Utils.QName.of_string $1),
+                           (QNameSet.singleton (QName.of_string $1),
                             NodeKind.Attribute))] }
 ;
 
@@ -135,16 +135,16 @@ test:
   NODE                { node, NodeKind.Node }
 | TEXT                { text, NodeKind.Text }
 | STAR                { star, NodeKind.Element }
-| COMMENT             { Utils.QNameSet.singleton(Utils.QName.comment),
+| COMMENT             { QNameSet.singleton(QName.comment),
                         NodeKind.Comment
                       }
 | PI                  { (if $1 = "" then star
-                         else Utils.QNameSet.singleton(
-                           Utils.QName.processing_instruction (
-                             Utils.QName.of_string $1)
+                         else QNameSet.singleton(
+                           QName.processing_instruction (
+                             QName.of_string $1)
                          )), NodeKind.ProcessingInstruction
                       }
-| TAG                 { Utils.QNameSet.singleton(Utils.QName.of_string $1),
+| TAG                 { QNameSet.singleton(QName.of_string $1),
                         NodeKind.Element
                       }
 ;
@@ -176,7 +176,7 @@ expr:
 | expr LTE expr             { Binop($1, Lte, $3) }
 | expr GT expr              { Binop($1, Gt, $3) }
 | expr GTE expr             { Binop($1, Gte, $3) }
-| TAG LP arg_list RP        { Fun_call(Utils.QName.of_string $1, $3) }
+| TAG LP arg_list RP        { Fun_call(QName.of_string $1, $3) }
 | LP expr RP                { $2 }
 | path                      { Path $1 }
 ;