X-Git-Url: http://git.nguyen.vg/gitweb/?a=blobdiff_plain;f=ata.ml;h=1ba9c400d65f7462d05a213e2bf67d714a0f0fc6;hb=cea756c7adc49891004bfe455628010eb7a28bc9;hp=aec548f90dd72ea7b7d669d6b98a4c0820a3441d;hpb=5b4679e20761058f1e04c123da52631c0dd265cc;p=SXSI%2Fxpathcomp.git diff --git a/ata.ml b/ata.ml index aec548f..1ba9c40 100644 --- a/ata.ml +++ b/ata.ml @@ -1,11 +1,51 @@ (* Todo refactor and remove this alias *) INCLUDE "debug.ml" -module Tree = Tree.Binary - let gen_id = let id = ref (-1) in fun () -> incr id;!id + module TS = + struct + type t = Nil | Cons of Tree.t * t | Concat of t*t + let empty = Nil + + let cons e t = Cons(e,t) + let concat t1 t2 = Concat (t1,t2) + let append e t = Concat(t,Cons(e,Nil)) + + let fold f l acc = + let rec loop acc = function + | Nil -> acc + | Cons(e,t) -> loop (f e acc) t + | Concat(t1,t2) -> loop (loop acc t1) t2 + in + loop acc l + + let length l = fold (fun _ x -> x+1) l 0 + + + let iter f l = + let rec loop = function + | Nil -> () + | Cons(e,t) -> let _ = f e in loop t + | Concat(t1,t2) -> let _ = loop t1 in loop t2 + in loop l + + end + + + +let h_union = Hashtbl.create 4097 + +let pt_cup s1 s2 = + let h = (Ptset.hash s1)*(Ptset.hash s2) - ((Ptset.hash s2)+(Ptset.hash s1)) in + try + Hashtbl.find h_union h + with + | Not_found -> let s = Ptset.union s1 s2 + in + Hashtbl.add h_union h s;s + module State = struct @@ -17,54 +57,58 @@ let mk_state = State.mk type state = State.t -type predicate = [ `Left of (Tree.t -> bool) | `Right of (Tree.t -> bool) | - `True - ] -let eval_pred t = - function `True -> true - | `Left f | `Right f -> f t type formula_expr = | False | True | Or of formula * formula | And of formula * formula - | Atom of ([ `Left | `Right ]*bool*state) + | Atom of ([ `Left | `Right | `LLeft | `RRight ]*bool*state) and formula = { fid: int; + fkey : int; pos : formula_expr; neg : formula; - st : Ptset.t*Ptset.t; + st : (Ptset.t*Ptset.t*Ptset.t)*(Ptset.t*Ptset.t*Ptset.t); size: int; } +external hash_const_variant : [> ] -> int = "%identity" +external int_bool : bool -> int = "%identity" + +let hash_node_form t = match t with + | False -> 0 + | True -> 1 + | And(f1,f2) -> (2+17*f1.fkey + 37*f2.fkey) (*land max_int *) + | Or(f1,f2) -> (3+101*f1.fkey + 253*f2.fkey) (*land max_int *) + | Atom(v,b,s) -> ((hash_const_variant v) + (3846*(int_bool b) +257) + (s lsl 13 - s)) (*land max_int *) + module FormNode = struct type t = formula - let hash = function - | False -> 0 - | True -> 1 - | And(f1,f2) -> 2+17*f1.fid + 37*f2.fid - | Or(f1,f2) -> 3+101*f1.fid + 253*f2.fid - | Atom(d,b,s) -> 5+(if d=`Left then 11 else 19)*(if b then 23 else 31)*s - - let hash t = (hash t.pos) land max_int - + + let hash t = t.fkey let equal f1 f2 = + if f1.fid == f2.fid || f1.fkey == f2.fkey || f1.pos == f2.pos then true + else match f1.pos,f2.pos with | False,False | True,True -> true - | Atom(d1,b1,s1), Atom(d2,b2,s2) when (d1 = d2) && (b1=b2) &&(s1=s2) -> true + | Atom(d1,b1,s1), Atom(d2,b2,s2) when (b1==b2) && (s1==s2) && (d1 = d2) -> true | Or(g1,g2),Or(h1,h2) | And(g1,g2),And(h1,h2) -> g1.fid == h1.fid && g2.fid == h2.fid | _ -> false + end module WH = Weak.Make(FormNode) let f_pool = WH.create 107 +let empty_triple = Ptset.empty,Ptset.empty,Ptset.empty +let empty_hex = empty_triple,empty_triple + let true_,false_ = - let rec t = { fid = 1; pos = True; neg = f ; st = Ptset.empty,Ptset.empty; size =1; } - and f = { fid = 0; pos = False; neg = t; st = Ptset.empty,Ptset.empty; size = 1; } + let rec t = { fid = 1; pos = True; fkey=1; neg = f ; st = empty_hex; size =1; } + and f = { fid = 0; pos = False; fkey=0; neg = t; st = empty_hex; size = 1; } in WH.add f_pool f; WH.add f_pool t; @@ -77,6 +121,7 @@ let is_false f = f.fid == 0 let cons pos neg s1 s2 size1 size2 = let rec pnode = { fid = gen_id (); + fkey = hash_node_form pos; pos = pos; neg = nnode; st = s1; @@ -84,6 +129,7 @@ let cons pos neg s1 s2 size1 size2 = and nnode = { fid = gen_id (); pos = neg; + fkey = hash_node_form neg; neg = pnode; st = s2; size = size2; @@ -94,20 +140,24 @@ let cons pos neg s1 s2 size1 size2 = let atom_ d p s = let si = Ptset.singleton s in let ss = match d with - | `Left -> si,Ptset.empty - | `Right -> Ptset.empty,si + | `Left -> (si,Ptset.empty,si),empty_triple + | `Right -> empty_triple,(si,Ptset.empty,si) + | `LLeft -> (Ptset.empty,si,si),empty_triple + | `RRight -> empty_triple,(Ptset.empty,si,si) in fst (cons (Atom(d,p,s)) (Atom(d,not p,s)) ss ss 1 1) + +let union_hex ((l1,ll1,lll1),(r1,rr1,rrr1)) ((l2,ll2,lll2),(r2,rr2,rrr2)) = + (pt_cup l1 l2 ,pt_cup ll1 ll2,pt_cup lll1 lll2), + (pt_cup r1 r2 ,pt_cup rr1 rr2,pt_cup rrr1 rrr2) let merge_states f1 f2 = let sp = - Ptset.union (fst f1.st) (fst f2.st), - Ptset.union (snd f1.st) (snd f2.st) + union_hex f1.st f2.st and sn = - Ptset.union (fst f1.neg.st) (fst f2.neg.st), - Ptset.union (snd f1.neg.st) (snd f2.neg.st) + union_hex f1.neg.st f2.neg.st in sp,sn - + let full_or_ f1 f2 = let f1,f2 = if f1.fid < f2.fid then f2,f1 else f1,f2 in let sp,sn = merge_states f1 f2 in @@ -144,16 +194,181 @@ let and_ f1 f2 = let not_ f = f.neg +let k_hash (s,t) = ((Ptset.hash s)) lsl 31 lxor (Tag.hash t) module HTagSetKey = struct type t = Ptset.t*Tag.t - let int_hash key = key lsl 31 lor (key lsl 8) - let equal (s1,s2) (t1,t2) = Tag.equal s2 t2 && Ptset.equal s1 t1 - let hash (s,t) = int_hash (Ptset.hash s) lxor ( int_hash (Tag.hash t)) + let equal (s1,s2) (t1,t2) = (s2 == t2) && Ptset.equal s1 t1 + let hash = k_hash end -module HTagSet = Hashtbl.Make(HTagSetKey) +module HTagSet = +struct + type key = Ptset.t*Tag.t + let equal (s1,s2) (t1,t2) = (s2 == t2) && Ptset.equal s1 t1 + let hash (s,t) = ((Ptset.hash s)) lsl 31 lxor (Tag.hash t) + +type 'a t = + { mutable size: int; (* number of elements *) + mutable data: (key,'a) bucketlist array } (* the buckets *) + +and ('a, 'b) bucketlist = + Empty + | Cons of 'a * 'b * ('a, 'b) bucketlist + +let create initial_size = + let s = min (max 1 initial_size) Sys.max_array_length in + { size = 0; data = Array.make s Empty } + +let clear h = + for i = 0 to Array.length h.data - 1 do + h.data.(i) <- Empty + done; + h.size <- 0 + +let copy h = + { size = h.size; + data = Array.copy h.data } + +let length h = h.size + +let resize tbl = + let odata = tbl.data in + let osize = Array.length odata in + let nsize = min (2 * osize + 1) Sys.max_array_length in + if nsize <> osize then begin + let ndata = Array.create nsize Empty in + let rec insert_bucket = function + Empty -> () + | Cons(key, data, rest) -> + insert_bucket rest; (* preserve original order of elements *) + let nidx = (hash key) mod nsize in + ndata.(nidx) <- Cons(key, data, ndata.(nidx)) in + for i = 0 to osize - 1 do + insert_bucket odata.(i) + done; + tbl.data <- ndata; + end + +let add h key info = + let i = (hash key) mod (Array.length h.data) in + let bucket = Cons(key, info, h.data.(i)) in + h.data.(i) <- bucket; + h.size <- succ h.size; + if h.size > Array.length h.data lsl 1 then resize h + +let remove h key = + let rec remove_bucket = function + Empty -> + Empty + | Cons(k, i, next) -> + if equal k key + then begin h.size <- pred h.size; next end + else Cons(k, i, remove_bucket next) in + let i = (hash key) mod (Array.length h.data) in + h.data.(i) <- remove_bucket h.data.(i) + +let rec find_rec key = function + Empty -> + raise Not_found + | Cons(k, d, rest) -> + if equal key k then d else find_rec key rest + +let find h key = + match h.data.((hash key) mod (Array.length h.data)) with + Empty -> raise Not_found + | Cons(k1, d1, rest1) -> + if equal key k1 then d1 else + match rest1 with + Empty -> raise Not_found + | Cons(k2, d2, rest2) -> + if equal key k2 then d2 else + match rest2 with + Empty -> raise Not_found + | Cons(k3, d3, rest3) -> + if equal key k3 then d3 else find_rec key rest3 + +let find_all h key = + let rec find_in_bucket = function + Empty -> + [] + | Cons(k, d, rest) -> + if equal k key + then d :: find_in_bucket rest + else find_in_bucket rest in + find_in_bucket h.data.((hash key) mod (Array.length h.data)) + +let replace h key info = + let rec replace_bucket = function + Empty -> + raise Not_found + | Cons(k, i, next) -> + if equal k key + then Cons(k, info, next) + else Cons(k, i, replace_bucket next) in + let i = (hash key) mod (Array.length h.data) in + let l = h.data.(i) in + try + h.data.(i) <- replace_bucket l + with Not_found -> + h.data.(i) <- Cons(key, info, l); + h.size <- succ h.size; + if h.size > Array.length h.data lsl 1 then resize h + +let mem h key = + let rec mem_in_bucket = function + | Empty -> + false + | Cons(k, d, rest) -> + equal k key || mem_in_bucket rest in + mem_in_bucket h.data.((hash key) mod (Array.length h.data)) + +let iter f h = + let rec do_bucket = function + Empty -> + () + | Cons(k, d, rest) -> + f k d; do_bucket rest in + let d = h.data in + for i = 0 to Array.length d - 1 do + do_bucket d.(i) + done + +let fold f h init = + let rec do_bucket b accu = + match b with + Empty -> + accu + | Cons(k, d, rest) -> + do_bucket rest (f k d accu) in + let d = h.data in + let accu = ref init in + for i = 0 to Array.length d - 1 do + accu := do_bucket d.(i) !accu + done; + !accu + + +end + + + + + + + + + + + + + +type dispatch = { first : Tree.t -> Tree.t; + flabel : string; + next : Tree.t -> Tree.t -> Tree.t; + nlabel : string; + } type t = { id : int; mutable states : Ptset.t; @@ -161,11 +376,9 @@ type t = { mutable final : Ptset.t; universal : Ptset.t; (* Transitions of the Alternating automaton *) - 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; - } + phi : (state,(TagSet.t*(bool*formula*bool)) list) Hashtbl.t; + sigma : (dispatch*bool*formula) HTagSet.t; +} module Pair (X : Set.OrderedType) (Y : Set.OrderedType) = struct @@ -179,7 +392,7 @@ type t = { module PL = Set.Make (Pair (Ptset) (Ptset)) - let pr_st ppf l = Format.fprintf ppf "{"; + let pr_st ppf l = Format.fprintf ppf "{"; begin match l with | [] -> () @@ -203,48 +416,52 @@ type t = { (pr_frm ppf f2); | Atom(dir,b,s) -> Format.fprintf ppf "%s%s[%i]" (if b then "" else "¬") - (if dir = `Left then "↓₁" else "↓₂") s + (match dir with + | `Left -> "↓₁" + | `Right -> "↓₂" + | `LLeft -> "⇓₁" + | `RRight -> "⇓₂") s let dnf_hash = Hashtbl.create 17 let rec dnf_aux f = match f.pos with | False -> PL.empty | True -> PL.singleton (Ptset.empty,Ptset.empty) - | Atom(`Left,_,s) -> PL.singleton (Ptset.singleton s,Ptset.empty) - | Atom(`Right,_,s) -> PL.singleton (Ptset.empty,Ptset.singleton s) + | Atom((`Left|`LLeft),_,s) -> PL.singleton (Ptset.singleton s,Ptset.empty) + | Atom((`Right|`RRight),_,s) -> PL.singleton (Ptset.empty,Ptset.singleton s) | Or(f1,f2) -> PL.union (dnf f1) (dnf f2) | And(f1,f2) -> - let pl1 = dnf f1 - and pl2 = dnf f2 - in - PL.fold (fun (s1,s2) acc -> - PL.fold ( fun (s1', s2') acc' -> - (PL.add - ((Ptset.union s1 s1'), - (Ptset.union s2 s2')) acc') ) - pl2 acc ) - pl1 PL.empty - - - and dnf f = - try + let pl1 = dnf f1 + and pl2 = dnf f2 + in + PL.fold (fun (s1,s2) acc -> + PL.fold ( fun (s1', s2') acc' -> + (PL.add + ((Ptset.union s1 s1'), + (Ptset.union s2 s2')) acc') ) + pl2 acc ) + pl1 PL.empty + + + and dnf f = + try Hashtbl.find dnf_hash f.fid with - Not_found -> - let d = dnf_aux f in - Hashtbl.add dnf_hash f.fid d;d + Not_found -> + let d = dnf_aux f in + Hashtbl.add dnf_hash f.fid d;d - let can_top_down f = + let can_top_down f = let nf = dnf f in if (PL.cardinal nf > 3)then None else match PL.elements nf with - | [(s1,s2); (t1,t2); (u1,u2)] when - Ptset.is_empty s1 && Ptset.is_empty s2 && Ptset.is_empty t1 && Ptset.is_empty u2 - -> Some(true,t2,u1) - | [(t1,t2); (u1,u2)] when Ptset.is_empty t1 && Ptset.is_empty u2 - -> Some(false,t2,u1) - | _ -> None + | [(s1,s2); (t1,t2); (u1,u2)] when + Ptset.is_empty s1 && Ptset.is_empty s2 && Ptset.is_empty t1 && Ptset.is_empty u2 + -> Some(true,t2,u1) + | [(t1,t2); (u1,u2)] when Ptset.is_empty t1 && Ptset.is_empty u2 + -> Some(false,t2,u1) + | _ -> None let equal_form f1 f2 = @@ -264,7 +481,7 @@ type t = { let s = if TagSet.is_finite ts - then "{" ^ (TagSet.fold (fun t a -> a ^ " " ^ (Tag.to_string t)) ts "") ^"}" + then "{" ^ (TagSet.fold (fun t a -> a ^ " '" ^ (Tag.to_string t)^"'") ts "") ^" }" else let cts = TagSet.neg ts in if TagSet.is_empty cts then "*" else (TagSet.fold (fun t a -> a ^ " " ^ (Tag.to_string t)) cts "*\\{" @@ -275,23 +492,28 @@ type t = { Format.fprintf ppf "\n")l; Format.fprintf ppf "NFA transitions :\n------------------------------\n"; - HTagSet.iter (fun (qs,t) (b,f,_,_) -> + HTagSet.iter (fun (qs,t) (disp,b,f) -> pr_st ppf (Ptset.elements qs); Format.fprintf ppf ",%s %s " (Tag.to_string t) (if b then "=>" else "->"); pr_frm ppf f; Format.fprintf ppf "(fid=%i) left=" f.fid; - let l,r = f.st in pr_st ppf (Ptset.elements l); + let (l,ll,_),(r,rr,_) = f.st in + pr_st ppf (Ptset.elements l); + Format.fprintf ppf ", "; + pr_st ppf (Ptset.elements ll); Format.fprintf ppf ", right="; pr_st ppf (Ptset.elements r); - Format.fprintf ppf "\n"; + Format.fprintf ppf ", "; + pr_st ppf (Ptset.elements rr); + Format.fprintf ppf ", first=%s, next=%s\n" disp.flabel disp.nlabel; ) a.sigma; - Format.fprintf ppf "=======================================\n" + Format.fprintf ppf "=======================================\n%!" module Transitions = struct - type t = state*TagSet.t*bool*formula*predicate + type t = state*TagSet.t*bool*formula*bool let ( ?< ) x = x - let ( >< ) state (l,b) = state,(l,b,`True) - let ( ><@ ) state (l,b,p) = state,(l,b,p) + let ( >< ) state (l,b) = state,(l,b,false) + let ( ><@ ) state (l,b) = state,(l,b,true) let ( >=> ) (state,(label,mark,pred)) form = (state,label,mark,form,pred) let ( +| ) f1 f2 = or_ f1 f2 let ( *& ) f1 f2 = and_ f1 f2 @@ -303,126 +525,30 @@ type t = { let equal_trans (q1,t1,m1,f1,_) (q2,t2,m2,f2,_) = (q1 == q2) && (TagSet.equal t1 t2) && (m1 == m2) && (equal_form f1 f2) - - module TS = - struct - type node = Nil | Cons of Tree.t * node | Concat of node*node - and t = { node : node; size : int } - let node n s = { node=n; size = s } - - let empty = node Nil 0 - - let cons e t = node (Cons(e,t.node)) (t.size+1) - let concat t1 t2 = node (Concat (t1.node,t2.node)) (t1.size+t2.size) - let append e t = concat t (cons e empty) - let to_list_rev t = - let rec aux acc l rest = - match l with - | Nil -> begin - match rest with - | Nil -> acc - | Cons(e,t) -> aux (e::acc) t Nil - | Concat(t1,t2) -> aux acc t1 t2 - end - | Cons(e,r) -> aux (e::acc) r rest - | Concat(t1,t2) -> aux acc t1 (Concat(t2,rest)) - in - aux [] t.node Nil - let length = function { size = s } -> s - let iter f { node = n } = - let rec loop = function - | Nil -> () - | Cons(e,n) -> let _ = f e in loop n - | Concat(n1,n2) -> let _ = loop n1 in loop n2 - in loop n - - end - - - module BottomUpNew = struct + module HFEval = Hashtbl.Make( + struct + type t = int*Ptset.t*Ptset.t + let equal (a,b,c) (d,e,f) = + a==d && (Ptset.equal b e) && (Ptset.equal c f) + let hash (a,b,c) = + a+17*(Ptset.hash b) + 31*(Ptset.hash c) + end) + + let hfeval = HFEval.create 4097 -IFDEF DEBUG -THEN - type trace = - | TNil of Ptset.t*Ptset.t - | TNode of Ptset.t*Ptset.t*bool* (int*bool*formula) list - - let traces = Hashtbl.create 17 - let dump_trace t = - let out = open_out "debug_trace.dot" - in - let outf = Format.formatter_of_out_channel out in - - let rec aux t num = - if Tree.is_node t - then - match (try Hashtbl.find traces (Tree.id t) with Not_found -> TNil(Ptset.empty,Ptset.empty)) with - | TNode(r,s,mark,trs) -> - let numl = aux (Tree.left t) num in - let numr = aux (Tree.right t) (numl+1) in - let mynum = numr + 1 in - Format.fprintf outf "n%i [ label=\"<%s>\\nr=" mynum (Tag.to_string (Tree.tag t)); - pr_st outf (Ptset.elements r); - Format.fprintf outf "\\ns="; - pr_st outf (Ptset.elements s); - List.iter (fun (q,m,f) -> - Format.fprintf outf "\\n%i %s" q (if m then "⇨" else "→"); - pr_frm outf f ) trs; - Format.fprintf outf "\", %s shape=box ];\n" - (if mark then "color=cyan1, style=filled," else ""); - let _ = Format.fprintf outf "n%i -> n%i;\n" mynum numl in - let _ = Format.fprintf outf "n%i -> n%i;\n" mynum numr in - mynum - | TNil(r,s) -> Format.fprintf outf "n%i [ shape=box, label=\"Nil\\nr=" num; - pr_st outf (Ptset.elements r); - Format.fprintf outf "\\ns="; - pr_st outf (Ptset.elements s); - Format.fprintf outf "\"];\n";num - else - match Hashtbl.find traces (-10) with - | TNil(r,s) -> - Format.fprintf outf "n%i [ shape=box, label=\"Nil\\nr=" num; - pr_st outf (Ptset.elements r); - Format.fprintf outf "\\ns="; - pr_st outf (Ptset.elements s); - Format.fprintf outf "\"];\n"; - num - | _ -> assert false - - in - Format.fprintf outf "digraph G {\n"; - ignore(aux t 0); - Format.fprintf outf "}\n%!"; - close_out out; - ignore(Sys.command "dot -Tsvg debug_trace.dot > debug_trace.svg") -END - - - - module HFEval = Hashtbl.Make( - struct - type t = int*Ptset.t*Ptset.t - let equal (a,b,c) (d,e,f) = - a==d && (Ptset.equal b e) && (Ptset.equal c f) - let hash (a,b,c) = - a+17*(Ptset.hash b) + 31*(Ptset.hash c) - end) - - let hfeval = HFEval.create 4097 - let eval_form_bool f s1 s2 = let rec eval f = match f.pos with - | Atom(`Left,b,q) -> if b == (Ptset.mem q s1) then (true,true,false) else false,false,false - | Atom(`Right,b,q) -> if b == (Ptset.mem q s2) then (true,false,true) else false,false,false - (* test some inlining *) + (* test some inlining *) | True -> true,true,true | False -> false,false,false + | Atom((`Left|`LLeft),b,q) -> if b == (Ptset.mem q s1) then (true,true,false) else false,false,false + | Atom(_,b,q) -> if b == (Ptset.mem q s2) then (true,false,true) else false,false,false | _ -> try - HFEval.find hfeval (f.fid,s1,s2) + HFEval.find hfeval (f.fid,s1,s2) with | Not_found -> let r = match f.pos with @@ -451,55 +577,6 @@ END in eval f - module HFEvalDir = Hashtbl.Make( - struct - type t = int*Ptset.t*[`Left | `Right ] - let equal (a,b,c) (d,e,f) = - a==d && (Ptset.equal b e) && (c = f) - let hash_dir = function `Left -> 7919 - | `Right -> 3517 - - let hash (a,b,c) = - a+17*(Ptset.hash b) + 31*(hash_dir c) - end) - - let hfeval_dir = HFEvalDir.create 4097 - - - let eval_dir dir f s = - let rec eval f = match f.pos with - | Atom(d,b,q) when d = dir -> if b == (Ptset.mem q s) then true_ else false_ - | Atom(_,b,q) -> f - (* test some inlining *) - | True -> true_ - | False -> false_ - | _ -> - try - HFEvalDir.find hfeval_dir (f.fid,s,dir) - with - | Not_found -> - let r = - match f.pos with - | Or(f1,f2) -> - let f1 = eval f1 - in - if is_true f1 then true_ - else if is_false f1 then eval f2 - else or_ f1 f2 - | And(f1,f2) -> - let f1 = eval f1 in - if is_false f1 then false_ - else if is_true f1 then eval f2 - else and_ f1 f2 - | _ -> assert false - in - HFEvalDir.add hfeval_dir (f.fid,s,dir) r; - r - - in eval f - - - let fstate_pool = Hashtbl.create 11 let merge_pred a b = match a,b with @@ -513,7 +590,30 @@ END | `Right _ -> l1,p::l2 | _ -> l1,l2 + + + + let tags_of_state a q = Hashtbl.fold + (fun p l acc -> + if p == q then + List.fold_left + (fun acc (ts,(_,_,aux)) -> + if aux then acc else + TagSet.cup ts acc) acc l + else acc) a.phi TagSet.empty + + + let tags a qs = + let ts = Ptset.fold (fun q acc -> TagSet.cup acc (tags_of_state a q)) qs TagSet.empty + in + if TagSet.is_finite ts + then `Positive(TagSet.positive ts) + else `Negative(TagSet.negative ts) + + + + let merge_trans t a tag q acc = List.fold_left (fun (accf,accm,acchtrue) (ts,(m,f,pred)) -> if TagSet.mem tag ts @@ -531,18 +631,27 @@ END else f,false in (or_ tmpf accf,accm||m,acchtrue||hastrue) else (accf,accm,acchtrue) - ) acc (Hashtbl.find a.phi q) + ) acc (try Hashtbl.find a.phi q with Not_found -> []) + + let inter_text a b = + match b with + | `Positive s -> let r = Ptset.inter a s in (r,Ptset.mem Tag.pcdata r, true) + | `Negative s -> (Ptset.empty, not (Ptset.mem Tag.pcdata s), false) + + let mk_nil_ctx x _ = Tree.mk_nil x + let next_sibling_ctx x _ = Tree.next_sibling x + let r_ignore _ x = x + + - let miss = ref 0 - let call = ref 0 - let get_trans t a tag r = - try - let mark,f,predl,has_true = + let get_trans t a tag r = + try + let dispatch,mark,f = HTagSet.find a.sigma (r,tag) - in f.st,f,mark,has_true,r,predl + in f.st,dispatch,f,mark,r with - Not_found -> - let f,mark,has_true,accq = + Not_found -> + let f,mark,_,accq = Ptset.fold (fun q (accf,accm,acchtrue,accq) -> let naccf,naccm,nacctrue = merge_trans t a tag q (accf,accm,acchtrue ) @@ -552,54 +661,123 @@ END ) r (false_,false,false,Ptset.empty) in - HTagSet.add a.sigma (accq,tag) (mark,f,([],[]),has_true); - f.st,f,mark,has_true,accq,([],[]) + let (ls,lls,_),(rs,rrs,_) = f.st in + let tb,ta = + Tree.tags t tag + in + let tl,htlt,lfin = inter_text tb (tags a ls) + and tll,htllt,llfin = inter_text tb (tags a lls) + and tr,htrt,rfin = inter_text ta (tags a rs) + and trr,htrrt,rrfin = inter_text ta (tags a rrs) + in + let first,flabel = + if (llfin && lfin) then (* no stars *) + (if htlt || htllt then (Tree.text_below, "#text_below") + else + let etl = Ptset.is_empty tl + and etll = Ptset.is_empty tll + in + if (etl && etll) + then (Tree.mk_nil, "#mk_nil") + else + if etl then + if Ptset.is_singleton tll + then (Tree.tagged_desc (Ptset.choose tll), "#tagged_desc") + else (Tree.select_desc_only tll, "#select_desc_only") + else if etll then (Tree.node_child,"#node_child") + else (Tree.select_below tl tll,"#select_below")) + else (* stars or node() *) + if htlt||htllt then (Tree.first_child,"#first_child") + else (Tree.node_child,"#node_child") + and next,nlabel = + if (rrfin && rfin) then (* no stars *) + ( if htrt || htrrt + then (Tree.text_next, "#text_next") + else + let etr = Ptset.is_empty tr + and etrr = Ptset.is_empty trr + in + if etr && etrr + then (mk_nil_ctx, "#mk_nil_ctx") + else + if etr then + if Ptset.is_singleton trr + then (Tree.tagged_foll_below (Ptset.choose trr),"#tagged_foll_below") + else (Tree.select_foll_only trr,"#select_foll_only") + else if etrr then (Tree.node_sibling_ctx,"#node_sibling_ctx") + else + (Tree.select_next tr trr,"#select_next") ) + + else if htrt || htrrt then (Tree.next_sibling_ctx,"#next_sibling_ctx") + else (Tree.node_sibling_ctx,"#node_sibling_ctx") + in + let dispatch = { first = first; flabel = flabel; next = next; nlabel = nlabel} + in + HTagSet.add a.sigma (accq,tag) (dispatch,mark,f); + f.st,dispatch,f,mark,accq + let rec accepting_among a t orig ctx = + let rest = Ptset.inter orig a.universal in + let r = Ptset.diff orig rest in + if Ptset.is_empty r then rest,0,TS.empty else + if Tree.is_nil t + then orig,0,TS.empty + else + let ((_,_,llls),(_,_,rrrs)),dispatch,formula,mark,r' = + get_trans t a (Tree.tag t) r + in + let s1,n1,res1 = accepting_among a (dispatch.first t) llls t in + let s2,n2,res2 = accepting_among a (dispatch.next t ctx) rrrs ctx in + let rb,rb1,rb2 = eval_form_bool formula s1 s2 in + if rb + then + let n1,res1 = if rb1 then n1,res1 else 0,TS.empty + and n2,res2 = if rb2 then n2,res2 else 0,TS.empty + in + if mark + then r',1+n1+n2,TS.Cons(t,(TS.Concat(res1,res2))) + else r',n1+n2,TS.Concat(res1,res2) + else Ptset.empty,0,TS.empty - let check_pred l t = true (*l = [] || - List.exists (function p -> - match p with - `Left f | `Right f -> f t - | _ -> assert false) l - *) - - let rec accepting_among2 a t r acc = - let orig = r in - let rest = Ptset.inter r a.final in - let r = Ptset.diff r rest in - if Ptset.is_empty r then rest,acc else - if (not (Tree.is_node t)) + let rec accepting_among_count a t orig ctx = + let rest = Ptset.inter orig a.universal in + let r = Ptset.diff orig rest in + if Ptset.is_empty r then rest,0 else + if Tree.is_node t then - orig,acc - else - let tag = Tree.tag t in - let t1 = Tree.first_child t - and t2 = Tree.next_sibling t in - let (r1,r2),formula,mark,has_true,r,_ = get_trans t a tag r - in - let s1,res1 = accepting_among2 a t1 r1 acc + let ((_,_,llls),(_,_,rrrs)),dispatch,formula,mark,r' = + get_trans t a (Tree.tag t) r in - let formula = eval_dir `Left formula s1 in - if is_false formula then rest,acc - else - if is_true formula then (* tail call equivalent to a top down *) - accepting_among2 a t2 orig (if mark then TS.append t res1 else res1) - else - let s2,res2 = accepting_among2 a t2 r2 res1 - in - let formula = eval_dir `Right formula s2 - in - if is_false formula then rest,res1 - else - orig,(if mark then TS.append t (res2) - else res2) - - + let s1,res1 = accepting_among_count a (dispatch.first t) llls t + and s2,res2 = accepting_among_count a (dispatch.next t ctx) rrrs ctx + in + let rb,rb1,rb2 = eval_form_bool formula s1 s2 in + if rb + then + let res1 = if rb1 then res1 else 0 + and res2 = if rb2 then res2 else 0 + in r', if mark then 1+res1+res2 else res1+res2 + else Ptset.empty,0 + else orig,0 + + let run a t = - let st,res = accepting_among2 a t a.init TS.empty in - let b = Ptset.is_empty (st) in - if b then TS.empty - else - res + let st,n,res = accepting_among a t a.init t in + if Ptset.is_empty (st) then TS.empty,0 else res,n + + + + let run_count a t = + let st,res = accepting_among_count a t a.init t in + if Ptset.is_empty (st) then 0 else res + + + let run_time _ _ = failwith "blah" + + + + +(* end +*)