Sanitize the representation of formula

[tatoo.git] / src / ata.mli

diff --git a/src/ata.mli b/src/ata.mli
index d65fabb..e4f0ffd 100644 (file)
--- a/src/ata.mli
+++ b/src/ata.mli
@@ -13,28 +13,27 @@
 (*                                                                     *)
 (***********************************************************************)
 
-type predicate =
-    First_child
-  | Next_sibling
-  | Parent
-  | Previous_sibling
-  | Stay
-  | Is_first_child
-  | Is_next_sibling
-  | Is of Tree.NodeKind.t
-  | Has_first_child
-  | Has_next_sibling
+type move = [ `First_child
+            | `Next_sibling
+            | `Parent
+            | `Previous_sibling
+            | `Stay ]
+
+type predicate = Move of move * State.t
+                 | Is_first_child
+                 | Is_next_sibling
+                 | Is of Tree.NodeKind.t
+                 | Has_first_child
+                 | Has_next_sibling
 
 val is_move : predicate -> bool
 
-type atom = predicate * bool * State.t
+module Atom : Boolean.ATOM with type data = predicate
 
-module Atom : Formula.ATOM with type data = atom
-
-module SFormula :
+module Formula :
   sig
-    include module type of Formula.Make(Atom)
-    val mk_atom : predicate -> bool -> State.t -> t
+    include module type of Boolean.Make(Atom)
+    val mk_atom : predicate -> t
     val mk_kind : Tree.NodeKind.t -> t
     val has_first_child : t
     val has_next_sibling : t
@@ -54,7 +53,7 @@ module SFormula :
 
 
 module Transition : Hcons.S with
-            type data = State.t * QNameSet.t * SFormula.t
+            type data = State.t * QNameSet.t * Formula.t
 
 module TransList : sig
   include Hlist.S with type elt = Transition.t
@@ -79,7 +78,7 @@ type t = private {
   id : Uid.t;
   mutable states : StateSet.t;
   mutable selection_states: StateSet.t;
-  transitions: (State.t, (QNameSet.t*SFormula.t) list) Hashtbl.t;
+  transitions: (State.t, (QNameSet.t*Formula.t) list) Hashtbl.t;
   mutable cache2 : TransList.t Cache.N2.t;
   mutable cache4 : Config.t Cache.N4.t;
 }
@@ -94,7 +93,7 @@ val get_trans : t -> QNameSet.elt -> StateSet.t -> TransList.t
 
 val eval_trans : t -> Config.t -> Config.t -> Config.t -> Config.t -> Config.t
 
-val add_trans : t -> State.t -> QNameSet.t -> SFormula.t -> unit
+val add_trans : t -> State.t -> QNameSet.t -> Formula.t -> unit
 val print : Format.formatter -> t -> unit
 val complete_transitions : t -> unit
 val cleanup_states : t -> unit