X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Fformula.mli;h=52e38b7a731ec8a34c76e9d47a22af10562a0e97;hp=e83bca138884c37917f40b528cfca3efdf7106b6;hb=974dacbf4f625bfd8ea83db69d6b346050141fea;hpb=d9c0e4863807eaf472e875a4bad35cfefe985c95

diff --git a/src/formula.mli b/src/formula.mli
index e83bca1..52e38b7 100644
--- a/src/formula.mli
+++ b/src/formula.mli
@@ -14,30 +14,28 @@
 (***********************************************************************)
 
 (*
-  Time-stamp: <Last modified on 2013-02-05 16:11:43 CET by Kim Nguyen>
+  Time-stamp: <Last modified on 2013-04-04 18:41:24 CEST by Kim Nguyen>
 *)
 
-module type PREDICATE =
+module type ATOM =
 sig
   type t
-  type ctx
-  val eval : ctx -> t -> bool
   val neg : t -> t
   include Hcons.Abstract with type t := t
-  include Sigs.AUX.Printable with type t := t
+  include Common_sig.Printable with type t := t
 end
 
-type ('formula,'pred) expr =
+type ('formula,'atom) expr =
   | False
   | True
   | Or of 'formula * 'formula
   | And of 'formula * 'formula
-  | Atom of 'pred
+  | Atom of 'atom
 
 (** View of the internal representation of a formula,
     used for pattern matching *)
 
-module Make(P : PREDICATE) :
+module Make(P : ATOM) :
 sig
   type t
 
@@ -53,7 +51,7 @@ sig
   (** Equality over formulae *)
 
   val expr : t -> (t,P.t) expr
-  (** Equality over formulae *)
+  (** Return a view of the formulae *)
 
   val compare : t -> t -> int
   (** Comparison of formulae *)
@@ -77,15 +75,16 @@ sig
   (** [atom_ dir b q] creates a down_left or down_right atom for state
       [q]. The atom is positive if [b == true].
   *)
-    
+
   val not_ : t -> t
   val or_ : t -> t -> t
   val and_ : t -> t -> t
   (** Boolean connective *)
-    
+
   val of_bool : bool -> t
   (** Convert an ocaml Boolean value to a formula *)
-    
-  val eval : P.ctx -> t -> bool
-    (** Evaluate a formula given a context for atomic predicates *)
+
+  val fold : (t -> 'a -> 'a) -> t -> 'a -> 'a
+  (** [fold f phi acc] folds [f] over the formula structure *)
+
 end