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

diff --git a/src/formula.mli b/src/formula.mli
index 46cbe65..04b3662 100644
--- a/src/formula.mli
+++ b/src/formula.mli
@@ -15,20 +15,22 @@
 
 (** 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
 
-(** 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 +45,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 *)
 
@@ -79,14 +79,3 @@ val and_ : t -> t -> t
 
 val of_bool : bool -> t
 (** Convert an ocaml Boolean value to a formula *)
-
-module Infix : sig
-  val ( +| ) : t -> t -> t
-  val ( *& ) : t -> t -> t
-  val ( *+ ) : move -> StateSet.elt -> t
-  val ( *- ) : move -> StateSet.elt -> t
-end
-(** Module to facilitate infix notations of formulae.
-    Just [open Formla.Infix] and write:
-    [let f = `Left *+ q1 +| `Right *+ q2 in ...]
-*)