Put the move type of automata in a Move module and add auxiliary function to create...

[tatoo.git] / src / ata.mli

diff --git a/src/ata.mli b/src/ata.mli
index 00070d4..650673e 100644 (file)
--- a/src/ata.mli
+++ b/src/ata.mli
@@ -21,6 +21,20 @@ type move = [ `First_child
             | `Parent
             | `Previous_sibling
             | `Stay ]
             | `Parent
             | `Previous_sibling
             | `Stay ]

+
+module Move :
+  sig
+    type t = move
+    type 'a table
+    val create_table : 'a -> 'a table
+    val get : 'a table -> t -> 'a
+    val set : 'a table -> t -> 'a -> unit
+    val iter : (t -> 'a -> unit) -> 'a table -> unit
+    val fold : (t -> 'a -> 'b -> 'b) -> 'a table -> 'b -> 'b
+    val for_all : (t -> 'a -> bool) -> 'a table -> bool
+    val exists : (t -> 'a -> bool) -> 'a table -> bool
+  end
+

 (** Type of moves an automaton can perform *)
 
 type predicate =
 (** Type of moves an automaton can perform *)
 
 type predicate =


@@ -65,6 +79,7 @@ module Formula :
           particular kind *)
     val get_states : t -> StateSet.t
       (** [get_state f] retrieves all the states occuring in [move] predicates in [f] *)
           particular kind *)
     val get_states : t -> StateSet.t
       (** [get_state f] retrieves all the states occuring in [move] predicates in [f] *)

+    val get_states_by_move : t -> StateSet.t Move.table

   end
 (** Modules representing the Boolean formulae used in transitions *)
 
   end
 (** Modules representing the Boolean formulae used in transitions *)