(***********************************************************************)
(*
- Time-stamp: <Last modified on 2013-02-07 10:03:26 CET by Kim Nguyen>
+ Time-stamp: <Last modified on 2013-03-09 11:16:45 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 Utils.Hcons.Abstract with type t := t
- include Utils.Sigs.AUX.Printable with type t := t
+ include Utils.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
(** 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 *)
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