X-Git-Url: http://git.nguyen.vg/gitweb/?a=blobdiff_plain;f=ata.mli;h=3af690737540090d6d2b684ac7a0bafbb9a3ce89;hb=df5fdb22632be887ecd9f5c46a014e7e970148a2;hp=4ec2f59224c570773264b9ebe7989c2b0532d950;hpb=6131f2f9e380543197c9fa253325bbc84749e6e8;p=SXSI%2Fxpathcomp.git diff --git a/ata.mli b/ata.mli index 4ec2f59..3af6907 100644 --- a/ata.mli +++ b/ata.mli @@ -1,78 +1,118 @@ -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 +type jump_kind = [ `CONTAINS of string | `NOTHING | `TAG of Tag.t ] +module State : +sig + include Sigs.T with type t = int + val make : unit -> t end +type merge_conf = NO | ONLY1 | ONLY2 | ONLY12 | MARK | MARK1 | MARK2 | MARK12 +module StateSet : + sig + include Ptset.S with type elt = int + val print : Format.formatter -> t -> unit + end -type state = int -val mk_state : unit -> state +module Formula : + sig + type 'a expr = + False + | True + | Or of 'a * 'a + | And of 'a * 'a + | Atom of ([ `LLeft | `Left | `RRight | `Right ] * bool * State.t) -type formula_expr = - False - | True - | Or of formula * formula - | And of formula * formula - | Atom of ([ `Left | `Right | `LLeft | `RRight ] * bool * state) -and formula = { fid : int; fkey : int; pos : formula_expr; neg : formula; st : (Ptset.t*Ptset.t*Ptset.t)*(Ptset.t*Ptset.t*Ptset.t); size: int;} -val true_ : formula -val false_ : formula -val atom_ : [`Left | `Right | `LLeft | `RRight ] -> bool -> state -> formula -val and_ : formula -> formula -> formula -val or_ : formula -> formula -> formula -val not_ : formula -> formula -(*val equal_form : formula -> formula -> bool *) -val pr_frm : Format.formatter -> formula -> unit + type t + val hash : t -> int + val uid : t -> Uid.t + val equal : t -> t -> bool + val expr : t -> t expr + val st : + t -> + (StateSet.t * StateSet.t * StateSet.t) * + (StateSet.t * StateSet.t * StateSet.t) + val size : t -> int + val print : Format.formatter -> t -> unit + val is_true : t -> bool + val is_false : t -> bool + val true_ : t + val false_ : t + val atom_ : + [ `LLeft | `Left | `RRight | `Right ] -> + bool -> StateSet.elt -> t + val not_ : t -> t + val or_ : t -> t -> t + val and_ : t -> t -> t + module Infix : sig + val ( +| ) : t -> t -> t + val ( *& ) : t -> t -> t + val ( *+ ) : + [ `LLeft | `Left | `RRight | `Right ] -> StateSet.elt -> t + val ( *- ) : + [ `LLeft | `Left | `RRight | `Right ] -> StateSet.elt -> t + end + end +module Transition : + sig + type node = State.t * TagSet.t * bool * Formula.t * bool + type data = node + type t + val make : data -> t + val node : t -> data + val hash : t -> int + val uid : t -> Uid.t + val equal : t -> t -> bool + module Infix : sig + val ( ?< ) : State.t -> State.t + val ( >< ) : State.t -> TagSet.t * bool -> State.t*(TagSet.t*bool*bool) + val ( ><@ ) : State.t -> TagSet.t * bool -> State.t*(TagSet.t*bool*bool) + val ( >=> ) : State.t * (TagSet.t*bool*bool) -> Formula.t -> (State.t*TagSet.t*t) + end + val print : Format.formatter -> t -> unit + end +module Formlist : Hlist.S with type elt = Transition.t -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 : StateSet.t; + init : StateSet.t; + starstate : StateSet.t option; + trans : (State.t, (TagSet.t * Transition.t) list) Hashtbl.t; + query_string : string; } -val dump : Format.formatter -> t -> unit - -module Transitions : sig -type t = state*TagSet.t*bool*formula*bool -(* Doing this avoid the parenthesis *) -val ( ?< ) : state -> state -val ( >< ) : state -> TagSet.t*bool -> state*(TagSet.t*bool*bool) -val ( ><@ ) : state -> TagSet.t*bool -> state*(TagSet.t*bool*bool) -val ( >=> ) : state*(TagSet.t*bool*bool) -> formula -> t -val ( +| ) : formula -> formula -> formula -val ( *& ) : formula -> formula -> formula -val ( ** ) : [`Left | `Right | `LLeft | `RRight ] -> state -> formula +val dump : Format.formatter -> 'a t -> unit -end -type transition = Transitions.t -val equal_trans : transition -> transition -> bool +module type ResultSet = + sig + type t + type elt = [`Tree] Tree.node + val empty : t + val cons : elt -> t -> t + val concat : t -> t -> t + val iter : (elt -> unit) -> t -> unit + val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a + val map : (elt -> elt) -> t -> t + val length : t -> int + val merge : merge_conf -> elt -> t -> t -> t + val mk_quick_tag_loop : (elt -> elt -> 'a*t array) -> 'a -> int -> Tree.t -> Tag.t -> (elt -> elt -> 'a*t array) + val mk_quick_star_loop : (elt -> elt -> 'a*t array) -> 'a -> int -> Tree.t -> (elt -> elt -> 'a*t array) + end +module IdSet : ResultSet +module GResult (Doc : sig val doc : Tree.t end) : ResultSet +val top_down_count : 'a t -> Tree.t -> int +val top_down_count1 : 'a t -> Tree.t -> int +val top_down : 'a t -> Tree.t -> IdSet.t +val top_down1 : 'a t -> Tree.t -> IdSet.t -(*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 bottom_up_count : + 'a t -> Tree.t -> [> `CONTAINS of 'b | `TAG of Tag.t ] -> int +val bottom_up : + 'a t -> Tree.t -> [> `CONTAINS of 'b | `TAG of Tag.t ] -> IdSet.t +module Test (Doc : sig val doc : Tree.t end ) : +sig + module Results : ResultSet + val top_down : 'a t -> Tree.t -> Results.t + val top_down1 : 'a t -> Tree.t -> Results.t +end