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

[tatoo.git] / src / formula.mli

diff --git a/src/formula.mli b/src/formula.mli
index 46cbe65..9b2659f 100644 (file)
--- 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 *)