X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Fata.mli;h=1f8e8637ee6a1b1487bab295d9d7118b2487d4e9;hp=aa28abff5cd55bae2d5b4071db7474a80c9ad478;hb=e3ad6d6f098809af95ddaf8b1e9bc4ec5cb7b0f4;hpb=021fdd8af4067ec57cdbf5c2dbc903252cbd4707

diff --git a/src/ata.mli b/src/ata.mli
index aa28abf..1f8e863 100644
--- a/src/ata.mli
+++ b/src/ata.mli
@@ -21,22 +21,42 @@ type move = [ `First_child
             | `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 for_all2 : (t -> 'a -> 'b -> bool) -> 'a table -> 'b table -> bool
+    val exists : (t -> 'a -> bool) -> 'a table -> bool
+  end
+
 (** Type of moves an automaton can perform *)
 
 type predicate =
-    Move of move * State.t  (** In the [move] direction, the automaton must be in the given state *)
-  | Is_first_child          (** True iff the node is the first child of its parent *)
-  | Is_next_sibling         (** True iff the node is the next sibling of its parent *)
+    Move of move * State.t  (** In the [move] direction,
+                                the automaton must be in the given state *)
+  | Is_first_child          (** True iff
+                                the node is the first child of its parent *)
+  | Is_next_sibling         (** True iff
+                                the node is the next sibling of its parent *)
   | Is of Tree.NodeKind.t   (** True iff the node is of the given kind *)
   | Has_first_child         (** True iff the node has a first child *)
   | Has_next_sibling        (** True iff the node has a next sibling *)
-(** Type of the predicates that can occur in the Boolean formulae that are in the transitions of the automaton *)
+(** Type of the predicates that can occur in the Boolean formulae that
+    are in the transitions of the automaton *)
 
 module Atom : sig
   include Hcons.S with type data = predicate
-  include Common_sig.Printable with type t:= t
+  include Common_sig.Printable with type t := t
 end
-(** Module representing atoms of Boolean formulae, which are simply hashconsed [predicate]s *)
+(** Module representing atoms of Boolean formulae, which are simply
+    hashconsed [predicate]s *)
 
 module Formula :
   sig
@@ -46,25 +66,29 @@ module Formula :
     val parent : State.t -> t
     val previous_sibling : State.t -> t
     val stay : State.t -> t
-      (** [first_child], [next_sibling], [parent], [previous_sibling], [stay] create a formula which consists only
-          of the corresponding [move] atom. *)
+    (** [first_child], [next_sibling], [parent], [previous_sibling],
+        [stay] create a formula which consists only of the
+        corresponding [move] atom. *)
     val is_first_child : t
     val is_next_sibling : t
     val has_first_child : t
     val has_next_sibling : t
-      (** [is_first_child], [is_next_sibling], [has_first_child], [has_next_sibling] are constant formulae which consist
-          only of the corresponding atom
-      *)
+    (** [is_first_child], [is_next_sibling], [has_first_child],
+        [has_next_sibling] are constant formulae which consist only
+        of the corresponding atom *)
     val is : Tree.NodeKind.t -> t
       (** [is k] creates a formula that tests the kind of the current node *)
     val is_attribute : t
     val is_element : t
     val is_processing_instruction : t
     val is_comment : t
-      (** [is_attribute], [is_element], [is_processing_instruction], [is_comment] are constant formulae that tests a
-          particular kind *)
+    (** [is_attribute], [is_element], [is_processing_instruction],
+        [is_comment] are constant formulae that tests a particular
+        kind *)
     val get_states : t -> StateSet.t
-      (** [get_state f] retrieves all the states occuring in [move] predicates in [f] *)
+    (** [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 *)
 
@@ -72,12 +96,13 @@ module Transition : sig
   include Hcons.S with type data = State.t * QNameSet.t * Formula.t
   val print : Format.formatter -> t -> unit
 end
-(** A [Transition.t] is a hashconsed triple of the state, the set of labels and the formula *)
+(** A [Transition.t] is a hashconsed triple of the state, the set of
+    labels and the formula *)
 
 
 module TransList : sig
   include Hlist.S with type elt = Transition.t
-  val print : Format.formatter -> ?sep:string -> t -> unit
+  val print : ?sep:string -> Format.formatter  -> t -> unit
 end
 (** Hashconsed lists of transitions, with a printing facility *)
 
@@ -97,6 +122,15 @@ val get_starting_states : t -> StateSet.t
 val get_selecting_states : t -> StateSet.t
 (** return the set of selecting states of the automaton *)
 
+val get_states_by_rank : t -> StateSet.t array
+(** return an array of states ordered by ranks.
+*)
+
+val get_max_rank : t -> int
+(** return the maximal rank of a state in the automaton, that is the
+    maximum number of runs needed to fuly evaluate the automaton.
+*)
+
 val get_trans : t -> QNameSet.elt -> StateSet.t -> TransList.t
 (** [get_trans auto l q] returns the list of transitions taken by [auto]
     for label [l] in state [q]. Takes time proportional to the number of
@@ -107,6 +141,10 @@ val get_form : t -> QNameSet.elt -> State.t -> Formula.t
 (** [get_form auto l q] returns a single formula for label [l] in state [q].
     Takes time proportional to the number of transitions in the automaton.
  *)
+val state_prerequisites : move -> t -> State.t -> StateSet.t
+(** [state_prerequisites m auto q] returns the set of all states q' such
+    that [q', _ -> phi] and [m(q)] is in phi
+*)
 
 val print : Format.formatter -> t -> unit
 (** Pretty printing of the automaton *)
@@ -126,6 +164,26 @@ val merge : t -> t -> t
     in parallel
 *)
 
+val union : t -> t -> t
+(** [union a a'] creates a new automaton [a''] that selects node
+    selected by either [a] or [a']
+*)
+
+val inter : t -> t -> t
+(** [inter a a'] creates a new automaton [a''] that selects node
+    selected by both [a] and [a']
+*)
+
+val neg : t -> t
+(** [neg a] creates a new automaton [a'] that selects the nodes not
+    selected by [a]
+*)
+
+val diff : t -> t -> t
+(** [diff a a'] creates a new automaton [a''] that select nodes selected
+    by [a] but not selected by [a']
+*)
+
 module Builder :
 sig
   type auto = t
@@ -147,9 +205,9 @@ sig
     (** Add a transition to the automaton *)
 
   val finalize : t  -> auto
-    (** Finalize the automaton and return it. Clean-up unused states (states that
-        do not occur in any transitions and remove instantes of negative [move] atoms
-        by creating fresh states that accept the complement of the negated state.
-    *)
+(** Finalize the automaton and return it. Clean-up unused states
+    (states that do not occur in any transitions and remove
+    instances of negative [move] atoms by creating fresh states
+    that accept the complement of the negated state.  *)
 end
   (** Builder facility for the automaton *)