X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Fformula.mli;h=f69a40d7e164e6c143621a3e548c32030f689edb;hp=9b2659f310575a5f1cb0b5b967c57057b3fcb472;hb=9a127b83fbb1171ebd36e6f42780093412a5e91a;hpb=f5d90fb688bc1a9b29815fc33c369856e6c51a67

diff --git a/src/formula.mli b/src/formula.mli
index 9b2659f..f69a40d 100644
--- a/src/formula.mli
+++ b/src/formula.mli
@@ -13,83 +13,74 @@
 (*                                                                     *)
 (***********************************************************************)
 
-(** Implementation of hashconsed Boolean formulae *)
-
-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
-  | 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 *)
 
-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 -> int
+  (** Hash function for formulae *)
 
-val equal : t -> t -> bool
-(** Equality over formulae *)
+  val uid : t -> Uid.t
+  (** Returns a unique ID for 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 -> int
-(** Syntactic size of the formula *)
+  val print : Format.formatter -> t -> unit
+  (** 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_true : t -> bool
-(** [is_true f] tests whether the formula is the atom True *)
+  val is_false : t -> bool
+  (** [is_false f] tests whether the formula is the atom False *)
 
-val is_false : t -> bool
-(** [is_false f] tests whether the formula is the atom False *)
+  val true_ : t
+  (** Atom True *)
 
-val true_ : t
-(** Atom True *)
+  val false_ : t
+  (** Atom False *)
 
-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.elt -> 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
-(** Module to facilitate infix notations of formulae.
-    Just [open Formla.Infix] and write:
-    [let f = `Left *+ q1 +| `Right *+ q2 in ...]
-*)