projects
/
tatoo.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
temp commit.
[tatoo.git]
/
src
/
formula.mli
diff --git
a/src/formula.mli
b/src/formula.mli
index
9b2659f
..
52e38b7
100644
(file)
--- a/
src/formula.mli
+++ b/
src/formula.mli
@@
-13,83
+13,78
@@
(* *)
(***********************************************************************)
(* *)
(***********************************************************************)
-(** Implementation of hashconsed Boolean formulae *)
+(*
+ Time-stamp: <Last modified on 2013-04-04 18:41:24 CEST by Kim Nguyen>
+*)
-type move = [ `Left |`Right ]
-(** Direction for automata predicates *)
+module type ATOM =
+sig
+ type t
+ val neg : t -> t
+ include Hcons.Abstract with type t := t
+ include Common_sig.Printable with type t := t
+end
-type
'formula
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
- | Move of (move * bool * State.t)
- | Label of QNameSet.t
+ | 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 *)
-type t
-
-(** Abstract type representing hashconsed formulae *)
+module Make(P : ATOM) :
+sig
+ type t
-val hash : t -> int
-(** Hash function for formulae *)
+ (** Abstract type representing hashconsed formulae *)
-
val uid : t -> Uid.
t
-
(** Returns a unique ID
for formulae *)
+
val hash : t -> in
t
+
(** Hash function
for formulae *)
-val equal : t -> t -> bool
-
(** Equality ove
r formulae *)
+ val uid : t -> Uid.t
+
(** Returns a unique ID fo
r formulae *)
-val expr : t -> t expr
-(** Equality over formulae *)
+ val equal : t -> t -> bool
+
(** Equality over formulae *)
-(*val st : t -> StateSet.t * StateSet.t
-(** states occuring left and right, positively or negatively *)
-*)
+ val expr : t -> (t,P.t) expr
+ (** Return a view of the formulae *)
-val compare : t -> t -> int
-(** Comparison of formulae *)
+
val compare : t -> t -> int
+
(** Comparison of formulae *)
-
val size : t -> in
t
-
(** Syntactic size of the formula
*)
+
val print : Format.formatter -> t -> uni
t
+
(** Pretty printer
*)
-val print : Format.formatter -> t -> unit
-
(** Pretty printer
*)
+ val is_true : t -> bool
+
(** [is_true f] tests whether the formula is the atom True
*)
-
val is_tru
e : t -> bool
-
(** [is_true f] tests whether the formula is the atom Tru
e *)
+
val is_fals
e : t -> bool
+
(** [is_false f] tests whether the formula is the atom Fals
e *)
-val is_false : t -> bool
-
(** [is_false f] tests whether the formula is the atom Fals
e *)
+ val true_ : t
+
(** Atom Tru
e *)
-
val tru
e_ : t
-
(** Atom Tru
e *)
+
val fals
e_ : t
+
(** Atom Fals
e *)
-val false_ : t
-(** Atom False *)
+ val atom_ : P.t -> t
+ (** [atom_ dir b q] creates a down_left or down_right atom for state
+ [q]. The atom is positive if [b == true].
+ *)
-
val atom_ : move -> bool -> StateSet.el
t -> t
-(** [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 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 of_bool : bool -> t
-
(** Convert an ocaml Boolean value to a formula
*)
+ val fold : (t -> 'a -> 'a) -> t -> 'a -> 'a
+
(** [fold f phi acc] folds [f] over the formula structure
*)
-module Infix : sig
- val ( +| ) : t -> t -> t
- val ( *& ) : t -> t -> t
- val ( *+ ) : move -> StateSet.elt -> t
- val ( *- ) : move -> StateSet.elt -> t
end
end
-(** Module to facilitate infix notations of formulae.
- Just [open Formla.Infix] and write:
- [let f = `Left *+ q1 +| `Right *+ q2 in ...]
-*)