-type t = {
- id : int;
- mutable states : Ptset.t;
- init : Ptset.t;
- mutable final : Ptset.t;
- universal : Ptset.t;
- phi : (state,(TagSet.t*(bool*formula*predicate)) list) Hashtbl.t;
- delta : (state*Tag.t, (bool*formula*predicate)) Hashtbl.t;
-(* delta : (state,(bool*formula*predicate) TagMap.t) Hashtbl.t; *)
- sigma : (bool*formula*(predicate list*predicate list)*bool) HTagSet.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