Compile again.

diff --git a/src/formula.ml b/src/formula.ml
index 1dd0f14..4c58e3c 100644 (file)
--- a/src/formula.ml
+++ b/src/formula.ml
@@ -60,7 +60,7 @@ module rec Node : Hcons.S
   end
 
 type t = Node.t
-let hash x = x.Node.key
+let hash x = x.Node.hash
 let uid x = x.Node.id
 let equal = Node.equal
 let expr f = f.Node.node.pos
@@ -96,6 +96,9 @@ let rec print ?(parent=false) ppf f =
           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;
@@ -111,36 +114,20 @@ let is_true f = (expr f) == True
 let is_false f = (expr f) == False
 
 
-let cons pos neg s1 s2 size1 size2 =
-  let nnode = Node.make { pos = neg; neg = (Obj.magic 0); st = s2; size = size2 } in
-  let pnode = Node.make { pos = pos; neg = nnode ; st = s1; size = size1 } in
+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 empty_pair = StateSet.empty, StateSet.empty
-let true_,false_ = cons True False empty_pair empty_pair 0 0
+let true_,false_ = cons True False
 let atom_ d p s =
-  let si = StateSet.singleton s in
-  let ss = match d with
-    | `Left -> si, StateSet.empty
-    | `Right -> StateSet.empty, si
-  in fst (cons (Atom(d,p,s)) (Atom(d,not p,s)) ss ss 1 1)
+  fst (cons (Move(d,p,s)) (Move(d,not p,s)))
 
 let not_ f = f.Node.node.neg
 
-let union_pair (l1,r1) (l2, r2) =
-  StateSet.union l1 l2,
-  StateSet.union r1 r2
-
-let merge_states f1 f2 =
-  let sp =
-    union_pair (st f1) (st f2)
-  and sn =
-    union_pair (st (not_ f1)) (st (not_ f2))
-  in
-    sp,sn
 
 let order f1 f2 = if uid f1  < uid f2 then f2,f1 else f1,f2
 
@@ -159,10 +146,7 @@ let or_ f1 f2 =
   (* commutativity of | *)
   else
     let f1, f2 = order f1 f2 in
-    let psize = (size f1) + (size f2) in
-    let nsize = (size (not_ f1)) + (size (not_ f2)) in
-    let sp, sn = merge_states f1 f2 in
-      fst (cons (Or(f1,f2)) (And(not_ f1, not_ f2)) sp sn psize nsize)
+      fst (cons (Or(f1,f2)) (And(not_ f1, not_ f2)))
 
 
 let and_ f1 f2 =

diff --git a/src/formula.mli b/src/formula.mli
index 9b2659f..78edcfc 100644 (file)
--- a/src/formula.mli
+++ b/src/formula.mli
@@ -15,7 +15,8 @@
 
 (** Implementation of hashconsed Boolean formulae *)
 
-type move = [ `Left |`Right ]
+type move = [ `Left | `Right | `Epsilon | `Up1 | `Up2 ]
+
 (** Direction for automata predicates *)
 
 type 'formula expr =
@@ -52,9 +53,6 @@ val expr : t -> t expr
 val compare : t -> t -> int
 (** Comparison of formulae *)
 
-val size : t -> int
-(** Syntactic size of the formula *)
-
 val print : Format.formatter -> t -> unit
 (** Pretty printer *)
 

diff --git a/src/pretty.ml b/src/pretty.ml
index 02c413f..bd9d410 100644 (file)
--- a/src/pretty.ml
+++ b/src/pretty.ml
@@ -86,6 +86,7 @@ let up_arrow = "↑"
 let right_arrow = "→"
 let left_arrow =  "←"
 let epsilon = "ϵ"
+let big_sigma = "∑"
 let cap = "∩"
 let cup = "∪"
 let lnot = "¬"

diff --git a/src/pretty.mli b/src/pretty.mli
index cb1b870..fb7e309 100644 (file)
--- a/src/pretty.mli
+++ b/src/pretty.mli
@@ -22,6 +22,7 @@ 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

diff --git a/src/ptset.ml b/src/ptset.ml
index 774b9fc..c4a1b33 100644 (file)
--- a/src/ptset.ml
+++ b/src/ptset.ml
@@ -119,10 +119,10 @@ struct
     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
@@ -182,14 +182,14 @@ struct
     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
 
   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 *)
+    if equal s t (* This is cheap thanks to hash-consing *)
     then s
     else
     match Node.node s, Node.node t with

diff --git a/src/qNameSet.ml b/src/qNameSet.ml
index 4035957..87c750e 100644 (file)
--- a/src/qNameSet.ml
+++ b/src/qNameSet.ml
@@ -15,4 +15,22 @@
 
 include FiniteCofinite.Make(Ptset.Make(QName))
 
-module Weak = FiniteCofinite.Weak(Ptset.Weak(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  =
+  if test e then print_finite fmt e conv
+  else begin
+    Format.fprintf fmt "%s \\ " Pretty.big_sigma;
+    print_finite fmt (inv e) conv
+  end
+
+let print fmt e = printer fmt e is_finite elements complement
+
+module Weak =
+struct
+  include FiniteCofinite.Weak(Ptset.Weak(QName))
+  let print fmt e =  printer fmt e is_finite elements complement
+end

diff --git a/src/qNameSet.mli b/src/qNameSet.mli
index 71d1478..10c3be3 100644 (file)
--- a/src/qNameSet.mli
+++ b/src/qNameSet.mli
@@ -18,5 +18,10 @@
     or cofinite *)
 
 include FiniteCofinite.S with type elt = QName.t
+include Sigs.AUX.Printable with type t := t
 
-module Weak : FiniteCofinite.S with type elt = QName.t
+module Weak  :
+  sig
+    include FiniteCofinite.S with type elt = QName.t
+    include Sigs.AUX.Printable with type t := t
+  end

diff --git a/src/sigs.ml b/src/sigs.ml
index dc98baf..9fc3e86 100644 (file)
--- a/src/sigs.ml
+++ b/src/sigs.ml
@@ -151,7 +151,6 @@ struct
     (** 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