X-Git-Url: http://git.nguyen.vg/gitweb/?a=blobdiff_plain;f=src%2Fformula.mli;h=e83bca138884c37917f40b528cfca3efdf7106b6;hb=d9c0e4863807eaf472e875a4bad35cfefe985c95;hp=46cbe6508c5219513329ebc404be212edaa77d98;hpb=cba2938d929fd5119b1491686ddc224d5af618c6;p=tatoo.git

diff --git a/src/formula.mli b/src/formula.mli
index 46cbe65..e83bca1 100644
--- a/src/formula.mli
+++ b/src/formula.mli
@@ -13,80 +13,79 @@
 (*                                                                     *)
 (***********************************************************************)
 
-(** Implementation of hashconsed Boolean formulae *)
+(*
+  Time-stamp: <Last modified on 2013-02-05 16:11:43 CET by Kim Nguyen>
+*)
 
-type move = [ `Left |`Right ]
-(** Direction for automata predicates *)
+module type PREDICATE =
+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
+end
 
-type 'hcons expr =
-    False
-    | True
-    | Or of 'hcons * 'hcons
-    | And of 'hcons * 'hcons
-    | Atom of (move * bool * State.t)
+type ('formula,'pred) expr =
+  | False
+  | True
+  | Or of 'formula * 'formula
+  | And of 'formula * 'formula
+  | Atom of 'pred
 
-(** Partial internal representation of a formula,
+(** View of the internal representation of a formula,
     used for pattern matching *)
 
-type t
-(** Abstract type representing hashconsed formulae *)
-
-val hash : t -> int
-(** Hash function for formulae *)
-
-val uid : t -> Uid.t
-(** Returns a unique ID for formulae *)
+module Make(P : PREDICATE) :
+sig
+  type t
 
-val equal : t -> t -> bool
-(** Equality over formulae *)
+  (** Abstract type representing hashconsed formulae *)
 
-val expr : t -> t expr
-(** Equality over formulae *)
+  val hash : t -> int
+  (** Hash function for formulae *)
 
-val st : t -> StateSet.t * StateSet.t
-(** states occuring left and right, positively or negatively *)
+  val uid : t -> Uid.t
+  (** Returns a unique ID for formulae *)
 
-val compare : t -> t -> int
-(** Comparison of formulae *)
+  val equal : t -> t -> bool
+  (** Equality over formulae *)
 
-val size : t -> int
-(** Syntactic size of the formula *)
+  val expr : t -> (t,P.t) expr
+  (** Equality over formulae *)
 
-val print : Format.formatter -> t -> unit
-(** Pretty printer *)
+  val compare : t -> t -> int
+  (** Comparison of formulae *)
 
-val is_true : t -> bool
-(** [is_true f] tests whether the formula is the atom True *)
+  val print : Format.formatter -> t -> unit
+  (** Pretty printer *)
 
-val is_false : t -> bool
-(** [is_false f] tests whether the formula is the atom False *)
+  val is_true : t -> bool
+  (** [is_true f] tests whether the formula is the atom True *)
 
-val true_ : t
-(** Atom True *)
+  val is_false : t -> bool
+  (** [is_false f] tests whether the formula is the atom False *)
 
-val false_ : t
-(** Atom False *)
+  val true_ : t
+  (** Atom 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 false_ : t
+  (** Atom False *)
 
-val of_bool : bool -> t
-(** Convert an ocaml Boolean value to a formula *)
-
-module Infix : sig
-  val ( +| ) : t -> t -> t
-  val ( *& ) : t -> t -> t
-  val ( *+ ) : move -> StateSet.elt -> t
-  val ( *- ) : move -> StateSet.elt -> t
+  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 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 *)
 end
-(** Module to facilitate infix notations of formulae.
-    Just [open Formla.Infix] and write:
-    [let f = `Left *+ q1 +| `Right *+ q2 in ...]
-*)