Refactor the code to have a unique place for signature definition.

[tatoo.git] / src / formula.ml

diff --git a/src/formula.ml b/src/formula.ml
index f7eae85..1dd0f14 100644 (file)
--- 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 =