Add a bullet symbol.

[tatoo.git] / src / formula.mli

diff --git a/src/formula.mli b/src/formula.mli
index e83bca1..f69a40d 100644 (file)
--- a/src/formula.mli
+++ b/src/formula.mli
@@ -13,31 +13,25 @@
 (*                                                                     *)
 (***********************************************************************)
 
-(*
-  Time-stamp: <Last modified on 2013-02-05 16:11:43 CET 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 +47,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 +71,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