From: Kim Nguyễn <kn@lri.fr>
Date: Fri, 26 Oct 2012 15:44:25 +0000 (+0200)
Subject: Merge branch 'master' of ssh://git.nguyen.vg/tatoo
X-Git-Tag: v0.1~198
X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=commitdiff_plain;h=cb29d45b3a79233581292a2ef172151b1ff489cb;hp=e2dce9a8858c17d907ddecc34cd939905a73f0cc

Merge branch 'master' of ssh://git.nguyen.vg/tatoo
---

diff --git a/HACKING b/HACKING
index 12ca0e5..5ddab53 100644
--- a/HACKING
+++ b/HACKING
@@ -1,4 +1,5 @@
-To build:
+Building instructions
+---------------------
 
 ocamlbuild src/test.native
 
diff --git a/src/finiteCofinite.ml b/src/finiteCofinite.ml
index 1c8e6ef..d3d0f13 100644
--- a/src/finiteCofinite.ml
+++ b/src/finiteCofinite.ml
@@ -14,14 +14,10 @@
 (***********************************************************************)
 INCLUDE "utils.ml"
 
-module type S =
-  sig
-    include Sigs.FiniteCofiniteSet
-    include Hcons.S with type t := t
-  end
+include Sigs.FINITECOFINITE
 
 module type HConsBuilder =
-  functor (H : Sigs.HashedType) -> Hcons.S with type data = H.t
+  functor (H : Sigs.AUX.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 =
@@ -137,44 +133,46 @@ struct
     in
       first_cofinite E.empty l
 
+  let exn = Sigs.FINITECOFINITE.InfiniteSet
+
   let fold f t a = match t.node with
     | Finite s -> E.fold f s a
-    | CoFinite _ -> raise Sigs.InfiniteSet
+    | CoFinite _ -> raise exn
 
   let iter f t = match t.node with
     | Finite t -> E.iter f t
-    | CoFinite _ -> raise Sigs.InfiniteSet
+    | CoFinite _ -> raise exn
 
   let for_all f t = match t.node with
     | Finite s -> E.for_all f s
-    | CoFinite _ -> raise Sigs.InfiniteSet
+    | CoFinite _ -> raise exn
 
   let exists f t = match t.node with
     | Finite s -> E.exists f s
-    | CoFinite _ -> raise Sigs.InfiniteSet
+    | CoFinite _ -> raise exn
 
   let filter f t = match t.node with
     | Finite s -> finite (E.filter f s)
-    | CoFinite _ -> raise Sigs.InfiniteSet
+    | 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 Sigs.InfiniteSet
+    | CoFinite _ -> raise exn
 
   let cardinal t = match t.node with
     | Finite s -> E.cardinal s
-    | CoFinite _ -> raise Sigs.InfiniteSet
+    | CoFinite _ -> raise exn
 
   let elements t = match t.node with
     | Finite s -> E.elements s
-    | CoFinite _ -> raise Sigs.InfiniteSet
+    | 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
-    | _ -> raise Sigs.InfiniteSet
+    | _ -> raise exn
 
   let is_singleton t = match t.node with
     | Finite s -> E.is_singleton s
@@ -191,15 +189,15 @@ struct
       let s1, b, s2 = E.split x s in
       finite s1, b, finite s2
 
-    | _ -> raise Sigs.InfiniteSet
+    | _ -> raise exn
 
   let min_elt s = match s.node with
     | Finite s -> E.min_elt s
-    | _ -> raise Sigs.InfiniteSet
+    | _ -> raise exn
 
   let max_elt s = match s.node with
     | Finite s -> E.min_elt s
-    | _ -> raise Sigs.InfiniteSet
+    | _ -> raise exn
 
   let positive t =
     match t.node with
diff --git a/src/finiteCofinite.mli b/src/finiteCofinite.mli
index 198e6e2..9b036c4 100644
--- a/src/finiteCofinite.mli
+++ b/src/finiteCofinite.mli
@@ -16,11 +16,8 @@
 (** Implementation of hashconsed finite or cofinite sets.
 *)
 
-module type S =
-sig
-  include Sigs.FiniteCofiniteSet
-  include Hcons.S with type t := t
-end
+include module type of Sigs.FINITECOFINITE
+
 (** Output signature of the {!FiniteCofinite.Make} and
     {!FiniteCofinite.Weak} functors.*)
 
diff --git a/src/formula.ml b/src/formula.ml
index f7eae85..1dd0f14 100644
--- a/src/formula.ml
+++ b/src/formula.ml
@@ -15,18 +15,18 @@
 INCLUDE "utils.ml"
 
 open Format
-type move = [ `Left | `Right ]
-type 'hcons expr =
-  | False | True
-  | Or of 'hcons * 'hcons
-  | And of 'hcons * 'hcons
-  | Atom of (move * bool * State.t)
+type move = [ `Left | `Right | `Epsilon | `Up1 | `Up2 ]
+type 'formula expr =
+  | False
+  | True
+  | Or of 'formula * 'formula
+  | And of 'formula * 'formula
+  | Move of (move * bool * State.t)
+  | Label of QNameSet.t
 
 type 'hcons node = {
   pos : 'hcons expr;
   mutable neg : 'hcons;
-  st : StateSet.t * StateSet.t;
-  size: int; (* Todo check if this is needed *)
 }
 
 external hash_const_variant : [> ] -> int = "%identity"
@@ -37,12 +37,13 @@ module rec Node : Hcons.S
   and Data : Hashtbl.HashedType  with type t = Node.t node =
   struct
     type t =  Node.t node
-    let equal x y = x.size == y.size &&
+    let equal x y = (*x.size == y.size &&*)
       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(d1, p1, s1), Atom(d2 ,p2 ,s2) -> d1 == d2 && p1 == p2 && s1 == s2
+      | Move(d1, p1, s1), Move(d2 ,p2 ,s2) -> d1 == d2 && p1 == p2 && s1 == s2
+      | Label s1, Label s2 -> s1 == s2
       | _ -> false
 
     let hash f =
@@ -54,7 +55,8 @@ module rec Node : Hcons.S
       | And (f1, f2) ->
         HASHINT3(PRIME3, Uid.to_int f1.Node.id, Uid.to_int f2.Node.id)
 
-      | Atom(d, p, s) -> HASHINT4(PRIME5, hash_const_variant d,vb p,s)
+      | Move(d, p, s) -> HASHINT4(PRIME5, hash_const_variant d,vb p,s)
+      | Label s -> HASHINT2(PRIME7, Uid.to_int s.QNameSet.id)
   end
 
 type t = Node.t
@@ -62,13 +64,14 @@ let hash x = x.Node.key
 let uid x = x.Node.id
 let equal = Node.equal
 let expr f = f.Node.node.pos
-let st f = f.Node.node.st
-let size f = f.Node.node.size
+(*let st f = f.Node.node.st*)
+(*let size f = f.Node.node.size*)
 let compare f1 f2 = compare f1.Node.id  f2.Node.id
 let prio f =
   match expr f with
     | True | False -> 10
-    | Atom _ -> 8
+    | Move _ -> 8
+    | Label _ -> 7
     | And _ -> 6
     | Or _ -> 1
 
@@ -85,7 +88,8 @@ let rec print ?(parent=false) ppf f =
       (print ppf f1);
       fprintf ppf " %s " Pretty.vee;
       (print ppf f2);
-    | Atom(dir, b, s) ->
+    | Label s -> fprintf ppf "%a" QNameSet.print s
+    | Move(dir, b, s) ->
       let _ = flush_str_formatter() in
       let fmt = str_formatter in
         let a_str, d_str =
diff --git a/src/formula.mli b/src/formula.mli
index 46cbe65..9b2659f 100644
--- a/src/formula.mli
+++ b/src/formula.mli
@@ -18,17 +18,19 @@
 type move = [ `Left |`Right ]
 (** Direction for automata predicates *)
 
-type 'hcons expr =
-    False
-    | True
-    | Or of 'hcons * 'hcons
-    | And of 'hcons * 'hcons
-    | Atom of (move * bool * State.t)
-
-(** Partial internal representation of a formula,
+type 'formula expr =
+  | False
+  | True
+  | Or of 'formula * 'formula
+  | And of 'formula * 'formula
+  | Move of (move * bool * State.t)
+  | Label of QNameSet.t
+
+(** View of the internal representation of a formula,
     used for pattern matching *)
 
 type t
+
 (** Abstract type representing hashconsed formulae *)
 
 val hash : t -> int
@@ -43,8 +45,9 @@ val equal : t -> t -> bool
 val expr : t -> t expr
 (** Equality over formulae *)
 
-val st : t -> StateSet.t * StateSet.t
+(*val st : t -> StateSet.t * StateSet.t
 (** states occuring left and right, positively or negatively *)
+*)
 
 val compare : t -> t -> int
 (** Comparison of formulae *)
diff --git a/src/hcons.ml b/src/hcons.ml
index d421d03..a820e08 100644
--- a/src/hcons.ml
+++ b/src/hcons.ml
@@ -13,45 +13,23 @@
 (*                                                                     *)
 (***********************************************************************)
 
-module type Abstract =
-  sig
-    type data
-    type t
-    val make : data -> t
-    val node : t -> data
-    val hash : t -> int
-    val uid : t -> Uid.t
-    val equal : t -> t -> bool
-    val init : unit -> unit
-  end
-
-type 'a node = { id   : Uid.t;
-                 key  : int;
-                 node : 'a }
-module type S =
-sig
-  type data
-  type t = private { id   : Uid.t;
-                     key  : int;
-                     node : data }
-  include Abstract with type data := data and type t := t
-end
+include Sigs.HCONS
 
 module type TableBuilder =
   functor
-    (H : Sigs.HashedType) ->
-      Sigs.HashSet with type data = H.t
+    (H : Sigs.AUX.HashedType) ->
+      Sigs.AUX.HashSet with type data = H.t
 
-module Builder (TB : TableBuilder) (H : Sigs.HashedType) =
+module Builder (TB : TableBuilder) (H : Sigs.AUX.HashedType) =
 struct
   type data = H.t
   type t = { id   : Uid.t;
-             key  : int;
+             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.key
+  let hash t = t.hash
   let equal t1 t2 = t1 == t2
   module HN =
   struct
@@ -68,7 +46,7 @@ struct
     uid_make := Uid.make_maker ()
 
   let make x =
-    let cell = { id = Uid.dummy; key = H.hash x; node = x } in
+    let cell = { id = Uid.dummy; hash = H.hash x; node = x } in
     try
       T.find pool cell
     with
@@ -88,9 +66,14 @@ struct
   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 equal x y = x == y
+
   let init () = ()
 end
diff --git a/src/hcons.mli b/src/hcons.mli
index af5618e..6b11bce 100644
--- a/src/hcons.mli
+++ b/src/hcons.mli
@@ -15,59 +15,18 @@
 
 (** Implementation of generic hashconsing. *)
 
-module type Abstract =
-  sig
-    type data
-      (** The type of the data to be hashconsed *)
-
-    type t
-      (** The type of hashconsed data *)
-
-    val make : data -> t
-      (** [make v] internalizes the value [v], making it an hashconsed
-          value.
-      *)
-
-    val node : t -> data
-      (** [node h] extract the original data from its hashconsed value
-      *)
-
-    val hash : t -> int
-      (** [hash h] returns a hash of [h], such that for every [h1] and
-          [h2], [equal h1 h2] implies [hash h1 = hash h2].
-      *)
-
-    val uid : t -> Uid.t
-      (** [uid h] returns a unique identifier *)
-    val equal : t -> t -> bool
-      (** Equality between hashconsed values. Equivalent to [==] *)
-
-    val init : unit -> unit
-      (** Initializes the internal storage. Any previously hashconsed
-          element is discarded. *)
-
-  end
-(** Abstract signature of a module implementing an hashconsed datatype *)
-
-module type S =
-sig
-  type data
-  type t = private { id   : Uid.t;
-                     key  : int;
-                     node : data }
-  include Abstract with type data := data and type t := t
-end
+include module type of Sigs.HCONS
 
 (** Output signature of the functor {!Hcons.Make} *)
 
-module Make (H : Sigs.HashedType) : S with type data = H.t
+module Make (H : Sigs.AUX.HashedType) : S with type data = H.t
 (** Functor building an implementation of hashconsed values for a given
     implementation of {!Sigs.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 : Sigs.HashedType) : S with type data = H.t
+module Weak (H : Sigs.AUX.HashedType) : S with type data = H.t
 (** Functor building an implementation of hashconsed values for a given
     implementation of {!Sigs.HashedType}. Hashconsed values have a
     weak semantics: they may be reclaimed as soon as no external
diff --git a/src/ptset.ml b/src/ptset.ml
index 9576993..774b9fc 100644
--- a/src/ptset.ml
+++ b/src/ptset.ml
@@ -1,5 +1,4 @@
-(* Original file : *)
-
+(* Original file: *)
 (***********************************************************************)
 (*                                                                     *)
 (*  Copyright (C) Jean-Christophe Filliatre                            *)
@@ -16,21 +15,17 @@
 (***********************************************************************)
 
 (* Modified by Kim Nguyen *)
-(* The Patricia trees are themselves deeply hashconsed. The module
-   provides a Make (and Weak) functor to build hashconsed patricia
-   trees whose elements are Abstract hashconsed values. This allows
-   to build sets of integers without boxing them in an hacons structure
+(* 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"
 
-module type S =
-  sig
-    include Sigs.Set
-    include Hcons.S with type t := t
-  end
+include Sigs.PTSET
 
 module type HConsBuilder =
-  functor (H : Sigs.HashedType) -> Hcons.S with type data = H.t
+  functor (H : Sigs.AUX.HashedType) -> Hcons.S with type data = H.t
 
 module Builder (HCB : HConsBuilder) (H : Hcons.Abstract) :
   S with type elt = H.t =
@@ -43,22 +38,22 @@ struct
     | Branch of int * int * 'a * 'a
 
   module rec Node : Hcons.S with type data = Data.t = HCB(Data)
-  and Data : Sigs.HashedType with type t = Node.t set =
+                            and Data : Sigs.AUX.HashedType with type t = Node.t set =
   struct
     type t =  Node.t set
     let equal x y =
       match x,y with
-        Empty,Empty -> true
+      | 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)
+      | Branch(b1,i1,l1,r1), Branch(b2,i2,l2,r2) ->
+          b1 == b2 && i1 == i2 && (Node.equal l1 l2) && (Node.equal r1 r2)
 
       | _ -> false
 
     let hash = function
-      | Empty -> 0
-      | Leaf i -> HASHINT2 (PRIME1, Uid.to_int (H.uid i))
-      | Branch (b,i,l,r) ->
+    | 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
 
@@ -72,13 +67,13 @@ struct
 
   let leaf k = Node.make (Leaf k)
 
-  (* To enforce the invariant that a branch contains two non empty
-     sub-trees *)
+                            (* 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 ************)
+                            (******** from here on, only use the smart constructors ************)
 
   let zero_bit k m = (k land m) == 0
 
@@ -86,33 +81,33 @@ struct
 
   let is_singleton n =
     match Node.node n with Leaf _ -> true
-      | _ -> false
+    | _ -> 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
+    | 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
+  | 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
+  | 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
+    | Empty -> acc
+    | Leaf k -> k :: acc
+    | Branch (_,_,l,r) -> elements_aux (elements_aux acc r) l
     in
-      elements_aux [] s
+    elements_aux [] s
 
   let mask k m  = (k lor (m-1)) land (lnot m)
 
@@ -121,20 +116,20 @@ struct
     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
+    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"
-*)
+                            (*
+                              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)
+        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)))
 
@@ -147,47 +142,47 @@ struct
   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
+    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);
+    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)  ->
+    | 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)
+        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
+        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) ->
+    | 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)
+        if zero_bit kid m then
+        branch_ne p m (rmv t0) t1
         else
-          n
+        branch_ne p m t0 (rmv t1)
+        else
+        n
     in
     rmv t
 
-  (* should run in O(1) thanks to Hash consing *)
+                            (* should run in O(1) thanks to Hash consing *)
 
   let equal a b = Node.equal a b
 
@@ -198,170 +193,170 @@ struct
     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) ->
+    | 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)
+        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)
+        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)
+        if zero_bit p n then
+        branch_ne q n (merge s t0) t1
         else
-          (* The prefixes disagree. *)
-          join p s q t
+        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) ->
+    | 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
+        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
+        if zero_bit p1 m2 then
+        subset l1 l2 && subset r1 l2
+        else
+        subset l1 r2 && subset r1 r2
         else
-          false
+        false
 
 
   let union s1 s2 = merge s1 s2
-    (* Todo replace with e Memo Module *)
+                            (* 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) ->
+    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)
+        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
+        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)
+        inter s1 (if zero_bit p1 m2 then l2 else r2)
         else
-          empty
+        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) ->
+    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)
+        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)
+        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
+        if zero_bit p1 m2 then diff s1 l2 else diff s1 r2
         else
-          s1
+        s1
 
 
-(*s All the following operations ([cardinal], [iter], [fold], [for_all],
+  (*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
+  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
+  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
+  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
+  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
+  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
+  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
+  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
+    in
+    part (empty, empty) s
 
-let rec choose n = match Node.node n with
+  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
+  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
+        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
+        else if m1 > m2 && match_prefix p1 p2 m2 then
         intersect s1 (if zero_bit p1 m2 then l2 else r2)
-      else
+        else
         false
 
 
-let from_list l = List.fold_left (fun acc e -> add e acc) empty l
+  let from_list l = List.fold_left (fun acc e -> add e acc) empty l
 
 
 end
@@ -371,11 +366,11 @@ 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
+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
index df38255..28e00d1 100644
--- a/src/ptset.mli
+++ b/src/ptset.mli
@@ -13,12 +13,8 @@
 (*                                                                     *)
 (***********************************************************************)
 
-module type S =
-  sig
-    include Sigs.Set
-    include Hcons.S with type t := t
-  end
-(** Output signature of the {!Ptset.Make} and {!Ptset.Weak} functors. *)
+
+include module type of Sigs.PTSET
 
 module Make (H : Hcons.Abstract) : S with type elt = H.t
 (** Builds an implementation of hashconsed sets of hashconsed elements.
@@ -30,5 +26,5 @@ module Weak (H : Hcons.Abstract) : S with type elt = H.t
     with weak internal storage. See {!Hcons.Weak}.
 *)
 
-module PosInt : Sigs.Set with type elt = int
+module PosInt : S with type elt = int
 (** Implementation of hashconsed sets of positive integers *)
diff --git a/src/qName.mli b/src/qName.mli
index 36bf022..fa448bc 100644
--- a/src/qName.mli
+++ b/src/qName.mli
@@ -15,8 +15,8 @@
 
 (** Implementation of qualified names as hashconsed strings *)
 
-include Hcons.S with type data = string
-include Sigs.Printable with type t := t
+include Sigs.HCONS.S with type data = string
+include Sigs.AUX.Printable with type t := t
 
 
 val of_string : string -> t
diff --git a/src/sigs.ml b/src/sigs.ml
index 3664d4e..dc98baf 100644
--- a/src/sigs.ml
+++ b/src/sigs.ml
@@ -13,114 +13,190 @@
 (*                                                                     *)
 (***********************************************************************)
 
-(** Various generic signatures *)
-
-module type HashedType =
-sig
-  type t
-  val hash : t -> int
-    (** [hash v] returns an integer in the range
-        [ 0 - 2^30-1 ]
-    *)
-  val equal : t -> t -> bool
-    (** Equality *)
-end
-(** Type equipped with an equality and hash function.
-    If [equal a b] then [(hash a) = (hash b)]
+(** This module contains all the signatures of the project, to avoid
+    code duplication. Each toplevel module (HCONS, PTSET, ...)
+    corresponds to an existing module in the project. The AUX modules
+    regroups common auxiliary signatures.
 *)
 
 
-module type OrderedType =
-sig
-  type t
-  val compare : t -> t -> int
-    (** 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].
+(** The [AUX] module regroups the definitions of common interfaces *)
+module  AUX =
+struct
+
+  (** 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 ]
     *)
-end
-(** Type equiped with a total ordering *)
+    val hash : t -> int
 
-module type Printable =
-sig
-  type t
-  val print : Format.formatter -> t -> unit
-end
-  (** Type equiped with a pretty-printer *)
+    (** 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
+
+  (** Type equiped with a pretty-printer *)
+  module type Printable =
+  sig
+    type t
+    val print : Format.formatter -> t -> unit
+  end
 
-module type Type =
-sig
-  type t
-  include HashedType with type t := t
-  include OrderedType with type t := t
-end
   (** Type with both total ordering and hashing functions.
       All modules of that type must enforce than:
       [equal a b] if and only if [compare a b = 0]
   *)
+  module type Type =
+  sig
+    type t
+    include HashedType with type t := t
+    include OrderedType with type t := t
+  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
 
-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
+  (** 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
 end
-(** Signature of a simple HashSet 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
+
+module  HCONS =
+struct
+  (** 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
+  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
+
+end
+
+
+module PTSET =
+struct
+  module type S =
+  sig
+    include HCONS.S
+    include AUX.Set with type t := t
+  end
 end
 
-exception InfiniteSet
-
-module type FiniteCofiniteSet =
-sig
-  include Set
-  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
+module FINITECOFINITE =
+struct
+  exception InfiniteSet
+  module type S =
+  sig
+    include HCONS.S
+    include AUX.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
 end
diff --git a/src/state.mli b/src/state.mli
index ef54518..8c126be 100644
--- a/src/state.mli
+++ b/src/state.mli
@@ -15,7 +15,7 @@
 
 (** Implementation of states *)
 
-include Sigs.Type with type t = int
+include Sigs.AUX.Type with type t = int
 
 val make : unit -> t
 (** Generate a fresh state *)
diff --git a/src/utils.ml b/src/utils.ml
index 2c3772d..1224f2a 100644
--- a/src/utils.ml
+++ b/src/utils.ml
@@ -17,9 +17,8 @@
 *)
 INCLUDE "utils.ml"
 
-
 module HashSet (H : Hashtbl.HashedType) :
-  Sigs.HashSet with type data = H.t =
+  Sigs.AUX.HashSet with type data = H.t =
 struct
   module T = Hashtbl.Make(H)
   type data = H.t
@@ -33,8 +32,8 @@ struct
   let mem = T.mem
 end
 
-module Pair (X : Sigs.Type) (Y : Sigs.Type) :
-  Sigs.Type with type t = X.t * Y.t =
+module Pair (X : Sigs.AUX.Type) (Y : Sigs.AUX.Type) :
+  Sigs.AUX.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)