projects
/
tatoo.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
BUG added: [68ad3227c315] following/preceding axes
[tatoo.git]
/
src
/
auto
/
formula.mli
diff --git
a/src/auto/formula.mli
b/src/auto/formula.mli
index
3cf240d
..
d708c2d
100644
(file)
--- a/
src/auto/formula.mli
+++ b/
src/auto/formula.mli
@@
-14,30
+14,28
@@
(***********************************************************************)
(*
(***********************************************************************)
(*
- Time-stamp: <Last modified on 2013-0
2-07 10:03:26
CET by Kim Nguyen>
+ Time-stamp: <Last modified on 2013-0
3-09 11:16:45
CET by Kim Nguyen>
*)
*)
-module type
PREDICATE
=
+module type
ATOM
=
sig
type t
sig
type t
- type ctx
- val eval : ctx -> t -> bool
val neg : t -> t
include Utils.Hcons.Abstract with type t := t
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
end
-type ('formula,'
pred
) expr =
+type ('formula,'
atom
) expr =
| False
| True
| Or of 'formula * 'formula
| And of 'formula * 'formula
| 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 *)
(** View of the internal representation of a formula,
used for pattern matching *)
-module Make(P :
PREDICATE
) :
+module Make(P :
ATOM
) :
sig
type t
sig
type t
@@
-53,7
+51,7
@@
sig
(** Equality over formulae *)
val expr : t -> (t,P.t) expr
(** 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 compare : t -> t -> int
(** Comparison of formulae *)
@@
-86,6
+84,7
@@
sig
val of_bool : bool -> t
(** Convert an ocaml Boolean value to a formula *)
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
end