(* Todo refactor and remove this alias *) INCLUDE "debug.ml" let gen_id = let id = ref (-1) in fun () -> incr id;!id module TS = struct type t = Nil | Sing of Tree.t | Cons of Tree.t*t | ConsCat of Tree.t * 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,Sing(e)) let fold f l acc = let rec loop acc = function | Nil -> acc | Sing e -> f e acc | Cons (e,t) -> loop (f e acc) t | ConsCat (e,t1,t2) -> loop (loop (f e acc) t1) t2 | 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 -> () | Sing e -> f e | Cons (e,t) -> f e; loop t | ConsCat(e,t1,t2) -> f e; loop t1; loop t2 | Concat(t1,t2) -> loop t1;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 type t = int let mk = gen_id end let mk_state = State.mk type state = 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; } external hash_const_variant : [> ] -> int = "%identity" external vb : 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*(vb b) +257) + (s lsl 13 - s)) (*land max_int *) module FormNode = struct type t = formula 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 (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; 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; t,f let is_true f = f.fid == 1 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; size = size1;} and nnode = { fid = gen_id (); pos = neg; fkey = hash_node_form neg; neg = pnode; st = s2; size = size2; } in (WH.merge f_pool pnode),(WH.merge f_pool nnode) let atom_ d p s = let si = Ptset.singleton s in let ss = match d with | `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 = union_hex f1.st f2.st and sn = 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 let psize = f1.size + f2.size in let nsize = f1.neg.size + f2.neg.size in fst (cons (Or(f1,f2)) (And(f1.neg,f2.neg)) sp sn psize nsize ) let or_ f1 f2 = let f1,f2 = if f1.fid < f2.fid then f2,f1 else f1,f2 in if is_true f1 || is_true f2 then true_ else if is_false f1 && is_false f2 then false_ else if is_false f1 then f2 else if is_false f2 then f1 else let psize = f1.size + f2.size in let nsize = f1.neg.size + f2.neg.size in let sp,sn = merge_states f1 f2 in fst (cons (Or(f1,f2)) (And(f1.neg,f2.neg)) sp sn psize nsize) let and_ f1 f2 = let f1,f2 = if f1.fid < f2.fid then f2,f1 else f1,f2 in if is_true f1 && is_true f2 then true_ else if is_false f1 || is_false f2 then false_ else if is_true f1 then f2 else if is_true f2 then f1 else let psize = f1.size + f2.size in let nsize = f1.neg.size + f2.neg.size in let sp,sn = merge_states f1 f2 in fst (cons (And(f1,f2)) (Or(f1.neg,f2.neg)) sp sn psize nsize) 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 equal (s1,s2) (t1,t2) = (s2 == t2) && Ptset.equal s1 t1 let hash = k_hash end module HTagSet = Hashtbl.Make(HTagSetKey) 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 let f_hash (h,s,t) = h * 41+((Ptset.hash s) lsl 10 ) lxor (Ptset.hash t)*4097 module HFormlistKey = struct type t = int*Ptset.t*Ptset.t let equal (h1,s1,t1) (h2,s2,t2) = h1==h2 && s1 == s2 && t1 == t2 let hash = f_hash end module HFormlist = Hashtbl.Make (HFormlistKey) 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; } module Pair (X : Set.OrderedType) (Y : Set.OrderedType) = struct type t = X.t*Y.t let compare (x1,y1) (x2,y2) = let r = X.compare x1 x2 in if r == 0 then Y.compare y1 y2 else r end module PL = Set.Make (Pair (Ptset) (Ptset)) let pr_st ppf l = Format.fprintf ppf "{"; begin match l with | [] -> () | [s] -> Format.fprintf ppf " %i" s | p::r -> Format.fprintf ppf " %i" p; List.iter (fun i -> Format.fprintf ppf "; %i" i) r end; Format.fprintf ppf " }" let rec pr_frm ppf f = match f.pos with | True -> Format.fprintf ppf "⊤" | False -> Format.fprintf ppf "⊥" | And(f1,f2) -> Format.fprintf ppf "("; (pr_frm ppf f1); Format.fprintf ppf ") ∧ ("; (pr_frm ppf f2); Format.fprintf ppf ")" | Or(f1,f2) -> (pr_frm ppf f1); Format.fprintf ppf " ∨ "; (pr_frm ppf f2); | Atom(dir,b,s) -> Format.fprintf ppf "%s%s[%i]" (if b then "" else "¬") (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|`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 Hashtbl.find dnf_hash f.fid with Not_found -> let d = dnf_aux f in Hashtbl.add dnf_hash f.fid d;d 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 let equal_form f1 f2 = (f1.fid == f2.fid) || (FormNode.equal f1 f2) || (PL.equal (dnf f1) (dnf f2)) let dump ppf a = Format.fprintf ppf "Automaton (%i) :\n" a.id; Format.fprintf ppf "States : "; pr_st ppf (Ptset.elements a.states); Format.fprintf ppf "\nInitial states : "; pr_st ppf (Ptset.elements a.init); Format.fprintf ppf "\nFinal states : "; pr_st ppf (Ptset.elements a.final); Format.fprintf ppf "\nUniversal states : "; pr_st ppf (Ptset.elements a.universal); Format.fprintf ppf "\nAlternating transitions :\n------------------------------\n"; let l = Hashtbl.fold (fun k t acc -> (List.map (fun (t,(m,f,p)) -> (t,k),(m,f,p)) t)@ acc) a.phi [] in let l = List.sort (fun ((tsx,x),_) ((tsy,y),_) -> if x-y == 0 then TagSet.compare tsx tsy else x-y) l in List.iter (fun ((ts,q),(b,f,_)) -> let s = if TagSet.is_finite 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 "*\\{" )^ "}" in Format.fprintf ppf "(%s,%i) %s " s q (if b then "=>" else "->"); pr_frm ppf f; Format.fprintf ppf "\n")l; Format.fprintf ppf "NFA transitions :\n------------------------------\n"; (* HTagSet.iter (fun (qs,t) (disp,b,_,flist,_,_) -> let (ls,lls,_),(rs,rrs,_) = List.fold_left (fun ((a1,b1,c1),(a2,b2,c2)) (_,f) -> let (x1,y1,z1),(x2,y2,z2) = f.st in ((Ptset.union x1 a1),(Ptset.union y1 b1),(Ptset.union c1 z1)), ((Ptset.union x2 a2),(Ptset.union y2 b2),(Ptset.union c2 z2))) ((Ptset.empty,Ptset.empty,Ptset.empty), (Ptset.empty,Ptset.empty,Ptset.empty)) flist in pr_st ppf (Ptset.elements qs); Format.fprintf ppf ",%s %s " (Tag.to_string t) (if b then "=>" else "->"); List.iter (fun (q,f) -> Format.fprintf ppf "\n%i," q; pr_frm ppf f) flist; Format.fprintf ppf "\nleft="; pr_st ppf (Ptset.elements ls); Format.fprintf ppf " , "; pr_st ppf (Ptset.elements lls); Format.fprintf ppf ", right="; pr_st ppf (Ptset.elements rs); Format.fprintf ppf ", "; pr_st ppf (Ptset.elements rrs); Format.fprintf ppf ", first=%s, next=%s\n\n" disp.flabel disp.nlabel; ) a.sigma; *) Format.fprintf ppf "=======================================\n%!" module Transitions = struct type t = state*TagSet.t*bool*formula*bool let ( ?< ) x = x 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 let ( ** ) d s = atom_ d true s end type transition = Transitions.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 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 (* test some inlining *) | True -> true,true,true | False -> false,false,false | _ -> try HFEval.find hfeval (f.fid,s1,s2) with | Not_found -> let r = match f.pos with | 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 | Or(f1,f2) -> let b1,rl1,rr1 = eval f1 in if b1 && rl1 && rr1 then (true,true,true) else let b2,rl2,rr2 = eval f2 in let rl1,rr1 = if b1 then rl1,rr1 else false,false and rl2,rr2 = if b2 then rl2,rr2 else false,false in (b1 || b2, rl1||rl2,rr1||rr2) | And(f1,f2) -> let b1,rl1,rr1 = eval f1 in if b1 && rl1 && rr1 then (true,true,true) else if b1 then let b2,rl2,rr2 = eval f2 in if b2 then (true,rl1||rl2,rr1||rr2) else (false,false,false) else (false,false,false) | _ -> assert false in HFEval.add hfeval (f.fid,s1,s2) r; r in eval f let h_formlist = HFormlist.create 511 let form_list_fold_left f acc fl = let rec loop acc fl = match fl with | Nil -> acc | Cons(s,frm,h,fll) -> loop (f acc s frm h) fll in loop acc fl let rec eval_formlist s1 s2 = function | Nil -> Ptset.empty,false,false,false | Cons(q,f,h,fl) -> let k = (h,s1,s2) in try HFormlist.find h_formlist k with Not_found -> let s,b',b1',b2' = eval_formlist s1 s2 fl in let b,b1,b2 = eval_form_bool f s1 s2 in let r = if b then (Ptset.add q s, b'||b, b1'||b1,b2'||b2) else s,b',b1',b2' in HFormlist.add h_formlist k r;r 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 cons_res e s1 s2 b1 b2 = if b1&&b2 then if s2 == TS.Nil && s1 == TS.Nil then TS.Sing e else if s1 == TS.Nil then TS.Cons (e,s2) else if s2 == TS.Nil then TS.Cons (e,s1) else TS.ConsCat(e,s1,s2) else if not(b1 || b2) then TS.Sing e else if b1 then if s1 == TS.Nil then TS.Sing e else TS.Cons(e,s1) else if s2 = TS.Nil then TS.Sing e else TS.Cons(e,s2) let cat_res _ s1 s2 b1 b2 = if b1&&b2 then if s1 == TS.Nil && s2 == TS.Nil then TS.Nil else if s1 == TS.Nil then s2 else if s2 == TS.Nil then s1 else TS.Concat(s1,s2) else if not(b1 || b2) then TS.Nil else if b1 then s1 else s2 let merge_trans t a tag q acc = List.fold_left (fun (accf,accm,acchtrue,acchash) (ts,(m,f,pred)) -> if TagSet.mem tag ts then let acchash = acchash+31*f.fid+42*q in (Cons(q,f,acchash,accf),accm||m,acchtrue||(is_true f),acchash) else (accf,accm,acchtrue,acchash) ) 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 get_trans t a tag r = try HTagSet.find a.sigma (r,tag) with Not_found -> let fl,mark,_,_,accq = Ptset.fold (fun q (accf,accm,acchtrue,acchash,accq) -> let naccf,naccm,nacctrue,acchash = merge_trans t a tag q (accf,accm,acchtrue,acchash ) in (* if is_false naccf then (naccf,naccm,nacctrue,accq) else *) (naccf,naccm,nacctrue,acchash,Ptset.add q accq) ) r (Nil,false,false,17,Ptset.empty) in let (ls,lls,llls),(rs,rrs,rrrs) = form_list_fold_left (fun ((a1,b1,c1),(a2,b2,c2)) _ f _ -> let (x1,y1,z1),(x2,y2,z2) = f.st in ((Ptset.union x1 a1),(Ptset.union y1 b1),(Ptset.union c1 z1)), ((Ptset.union x2 a2),(Ptset.union y2 b2),(Ptset.union c2 z2))) ((Ptset.empty,Ptset.empty,Ptset.empty), (Ptset.empty,Ptset.empty,Ptset.empty)) fl 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 _ = Format.fprintf Format.err_formatter "Tag %s, right_states " (Tag.to_string tag); pr_st Format.err_formatter (Ptset.elements rs); Format.fprintf Format.err_formatter " tags = "; Ptset.iter (fun t -> Format.fprintf Format.err_formatter "%s " (Tag.to_string t)) tr; Format.fprintf Format.err_formatter ", next_states "; pr_st Format.err_formatter (Ptset.elements rrs); Format.fprintf Format.err_formatter " tags = "; Ptset.iter (fun t -> Format.fprintf Format.err_formatter "%s " (Tag.to_string t)) trr; Format.fprintf Format.err_formatter "\n%!"; 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; consres = if mark then cons_res else cat_res } in HTagSet.add a.sigma (accq,tag) (dispatch,mark,fl,llls,rrrs); dispatch,mark,fl,llls,rrrs let rec accepting_among a t r ctx = if Tree.is_nil t || Ptset.is_empty r then Ptset.empty,0,TS.Nil else let dispatch,mark,flist,llls,rrrs = 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 r',rb,rb1,rb2 = eval_formlist s1 s2 flist in r',(vb rb)*((vb mark) + (vb rb1)* n1 + (vb rb2)*n2),if rb then dispatch.consres t res1 res2 rb1 rb2 else TS.Nil let run a t = 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 rec accepting_among_count_no_star a t r ctx = if Tree.is_nil t||Ptset.is_empty r then Ptset.empty,0 else let dispatch,mark,flist,llls,rrrs = get_trans t a (Tree.tag t) r in let s1,res1 = accepting_among_count_no_star a (dispatch.first t) llls t and s2,res2 = accepting_among_count_no_star a (dispatch.next t ctx) rrrs ctx in let r',rb,rb1,rb2 = eval_formlist s1 s2 flist in r',(vb rb)*((vb mark) + (vb rb1)*res1 + (vb rb2)*res2) let rec accepting_among_count_star a t n = if Tree.is_nil t then n else if (Tree.tag t == Tag.attribute) then accepting_among_count_star a (Tree.node_sibling t) n else accepting_among_count_star a (Tree.node_sibling t) (accepting_among_count_star a (Tree.node_child t) (1+n)) let rec accepting_among_count_may_star starstate a t r ctx = if r == starstate then starstate,(accepting_among_count_star a t 0) else if Tree.is_nil t||Ptset.is_empty r then Ptset.empty,0 else let dispatch,mark,flist,llls,rrrs = get_trans t a (Tree.tag t) r in let s1,res1 = accepting_among_count_may_star starstate a (dispatch.first t) llls t and s2,res2 = accepting_among_count_may_star starstate a (dispatch.next t ctx) rrrs ctx in let r',rb,rb1,rb2 = eval_formlist s1 s2 flist in r',(vb rb)*((vb mark) + (vb rb1)*res1 + (vb rb2)*res2) let run_count a t = let st,res = match a.starstate with | None -> accepting_among_count_no_star a t a.init t | Some s -> accepting_among_count_may_star s a t a.init t in if Ptset.is_empty (st) then 0 else res let run_time _ _ = failwith "blah" (* end *)