-module TS : sig
- type t
- val empty : t
- val cons : Tree.t -> t -> t
- val append : Tree.t -> t -> t
- val concat : t -> t -> t
- val length : t -> int
- val iter : (Tree.t -> unit) -> t -> unit
-end
-
type state = int
val mk_state : unit -> state
module HTagSet : Hashtbl.S with type key = Ptset.t*Tag.t
-type dispatch = { first : Tree.t -> Tree.t;
- flabel : string;
- next : Tree.t -> Tree.t -> Tree.t;
- nlabel : string;
- consres : Tree.t -> TS.t -> TS.t -> bool -> bool -> TS.t;
- }
-
-type formlist = Nil | Cons of state*formula*int*formlist
-type t = {
- id : int;
- mutable states : Ptset.t;
- init : Ptset.t;
- mutable final : Ptset.t;
- universal : Ptset.t;
- starstate : Ptset.t option;
- (* Transitions of the Alternating automaton *)
- phi : (state,(TagSet.t*(bool*formula*bool)) list) Hashtbl.t;
- sigma : (dispatch*bool*formlist*Ptset.t*Ptset.t) HTagSet.t;
+type 'a t = {
+ id : int;
+ mutable states : Ptset.t;
+ init : Ptset.t;
+ mutable final : Ptset.t;
+ universal : Ptset.t;
+ starstate : Ptset.t option;
+ (* Transitions of the Alternating automaton *)
+ phi : (state,(TagSet.t*(bool*formula*bool)) list) Hashtbl.t;
+ sigma : (int,('a t -> Tree.t -> Tree.t -> Ptset.t*'a)) Hashtbl.t;
}
-val dump : Format.formatter -> t -> unit
+
+val dump : Format.formatter -> 'a t -> unit
module Transitions : sig
type t = state*TagSet.t*bool*formula*bool
val equal_trans : transition -> transition -> bool
+ module type ResultSet =
+ sig
+ type t
+ val empty : t
+ val cons : Tree.t -> t -> t
+ val concat : t -> t -> t
+ val iter : (Tree.t -> unit) -> t -> unit
+ val fold : (Tree.t -> 'a -> 'a) -> t -> 'a -> 'a
+ val map : (Tree.t -> Tree.t) -> t -> t
+ val length : t -> int
+ end
+
+ module IdSet : ResultSet
-(*module BottomUpJumpNew :
-sig *)
- val run : t -> Tree.t -> TS.t*int
- val run_count : t -> Tree.t -> int
- val run_time : t -> Tree.t -> TS.t*int
-(*end *)
+ val top_down_count : 'a t -> Tree.t -> int
+ val top_down : 'a t -> Tree.t -> IdSet.t
+ type jump_kind = [ `TAG of Tag.t | `CONTAINS of string | `NOTHING ]
+ val bottom_up_count : 'a t -> Tree.t -> jump_kind -> int