X-Git-Url: http://git.nguyen.vg/gitweb/?a=blobdiff_plain;f=src%2Fformula.mli;h=78edcfcb0b7e8350dcf4967eb88e78c1a5870fa2;hb=9b75e9a2074c357fc2c823156451209d2a4cef8b;hp=46cbe6508c5219513329ebc404be212edaa77d98;hpb=cba2938d929fd5119b1491686ddc224d5af618c6;p=tatoo.git

diff --git a/src/formula.mli b/src/formula.mli
index 46cbe65..78edcfc 100644
--- a/src/formula.mli
+++ b/src/formula.mli
@@ -15,20 +15,23 @@
 
 (** Implementation of hashconsed Boolean formulae *)
 
-type move = [ `Left |`Right ]
+type move = [ `Left | `Right | `Epsilon | `Up1 | `Up2 ]
+
 (** Direction for automata predicates *)
 
-type 'hcons expr =
-    False
-    | True
-    | Or of 'hcons * 'hcons
-    | And of 'hcons * 'hcons
-    | Atom of (move * bool * State.t)
+type 'formula expr =
+  | False
+  | True
+  | Or of 'formula * 'formula
+  | And of 'formula * 'formula
+  | Move of (move * bool * State.t)
+  | Label of QNameSet.t
 
-(** Partial internal representation of a formula,
+(** View of the internal representation of a formula,
     used for pattern matching *)
 
 type t
+
 (** Abstract type representing hashconsed formulae *)
 
 val hash : t -> int
@@ -43,15 +46,13 @@ 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 *)
 
-val size : t -> int
-(** Syntactic size of the formula *)
-
 val print : Format.formatter -> t -> unit
 (** Pretty printer *)