+ if (hastext1||hastextn) then f_text (* jumping to text nodes doesn't work really well *)
+ else if (Ptset.is_empty tags1) && (Ptset.is_empty tagsn) then f_nil
+ else if (Ptset.is_empty tagsn) then
+ if (Ptset.is_singleton tags1) then f_t1 (Ptset.choose tags1) (* TaggedChild/Sibling *)
+ else f_s1 tags1 (* SelectChild/Sibling *)
+ else if (Ptset.is_empty tags1) then
+ if (Ptset.is_singleton tagsn) then f_tn (Ptset.choose tagsn) (* TaggedDesc/Following *)
+ else f_sn tagsn (* SelectDesc/Following *)
+ else f_notext
+
+ let choose_jump_down a b c d =
+ choose_jump a b c d
+ (Tree.mk_nil)
+ (Tree.text_below)
+ (*fun x -> let i,j = Tree.doc_ids x in
+ let res = Tree.text_below x in
+ Printf.printf "Calling text_below %s (tag=%s), docids= (%i,%i), res=%s\n"
+ (Tree.dump_node x) (Tag.to_string (Tree.tag x)) i j (Tree.dump_node res);
+ res*)
+ (fun _ -> Tree.node_child ) (* !! no tagged_child in Tree.ml *)
+ (fun _ -> Tree.node_child ) (* !! no select_child in Tree.ml *)
+ (Tree.tagged_desc)
+ (fun _ -> Tree.node_child ) (* !! no select_desc *)
+ (Tree.node_child)
+
+ let choose_jump_next a b c d =
+ choose_jump a b c d
+ (fun t _ -> Tree.mk_nil t)
+ (Tree.text_next)
+ (*fun x y -> let i,j = Tree.doc_ids x in
+ let res = Tree.text_next x y in
+ Printf.printf "Calling text_next %s (tag=%s) ctx=%s, docids= (%i,%i), res=%s\n"
+ (Tree.dump_node x) (Tag.to_string (Tree.tag x)) (Tree.dump_node y) i j (Tree.dump_node res);
+ res*)
+
+ (fun _ -> Tree.node_sibling_ctx) (* !! no tagged_sibling in Tree.ml *)
+ (fun _ -> Tree.node_sibling_ctx) (* !! no select_child in Tree.ml *)
+ (Tree.tagged_foll_below)
+ (fun _ -> Tree.node_sibling_ctx) (* !! no select_foll *)
+ (Tree.node_sibling_ctx)
+
+
+ let get_trans slist tag a t =
+ try
+ Hashtbl.find td_trans (tag,hpl slist)
+ with
+ | Not_found ->
+ let fl_list,llist,rlist,ca,da,sa,fa =
+ fold_pl
+ (fun set _ (fll_acc,lllacc,rllacc,ca,da,sa,fa) -> (* For each set *)
+ let fl,ll,rr,ca,da,sa,fa =
+ Ptset.fold
+ (fun q acc ->
+ fst (
+ List.fold_left
+ (fun (((fl_acc,ll_acc,rl_acc,c_acc,d_acc,s_acc,f_acc),h_acc) as acc)
+ (ts,(m,f,_)) ->
+ if (TagSet.mem tag ts)
+ then
+ let (child,desc,below),(sibl,foll,after) = f.st in
+ ((Formlist.cons q f h_acc m fl_acc,
+ Ptset.union ll_acc below,
+ Ptset.union rl_acc after,
+ Ptset.union child c_acc,
+ Ptset.union desc d_acc,
+ Ptset.union sibl s_acc,
+ Ptset.union foll f_acc),
+ HASHINT3(h_acc,f.fid,HASHINT2(q,vb m)))
+ else acc ) (acc,0) (
+ try Hashtbl.find a.phi q
+ with
+ Not_found -> Printf.eprintf "Looking for state %i, doesn't exist!!!\n%!"
+ q;[]
+ ))
+
+ ) set (Formlist.nil,Ptset.empty,Ptset.empty,ca,da,sa,fa)
+ in fl::fll_acc, cons ll lllacc, cons rr rllacc,ca,da,sa,fa)
+ slist ([],Nil,Nil,Ptset.empty,Ptset.empty,Ptset.empty,Ptset.empty)
+ in
+ (* Logic to chose the first and next function *)
+ let tags_below,tags_after = Tree.tags t tag in
+ let first = choose_jump_down tags_below ca da a
+ and next = choose_jump_next tags_after sa fa a in
+ let v = (fl_list,llist,rlist,first,next) in
+ Hashtbl.add td_trans (tag, hpl slist) v; v
+
+ let merge rb rb1 rb2 mark t res1 res2 =
+ if rb
+ then
+ let res1 = if rb1 then res1 else RS.empty
+ and res2 = if rb2 then res2 else RS.empty
+ in
+ if mark then RS.cons t (RS.concat res1 res2)
+ else RS.concat res1 res2
+ else RS.empty
+
+ let top_down ?(noright=false) a t slist ctx slot_size =
+ let pempty = empty_size slot_size in
+ let eval_fold2_slist fll sl1 sl2 res1 res2 t =
+ let res = Array.copy res1 in
+ let rec fold l1 l2 fll i aq = match l1,l2,fll with
+ | Cons(s1,_,ll1), Cons(s2, _ ,ll2),fl::fll ->
+ let r',rb,rb1,rb2,mark = eval_formlist s1 s2 fl in
+ let _ = res.(i) <- merge rb rb1 rb2 mark t res1.(i) res2.(i)
+ in
+ fold ll1 ll2 fll (i+1) (cons r' aq)
+ | Nil, Nil,[] -> aq,res
+ | _ -> assert false
+ in
+ fold sl1 sl2 fll 0 Nil
+ in
+ let null_result() = (pempty,Array.make slot_size RS.empty) in
+ let rec loop t slist ctx =
+ if Tree.is_nil t then null_result()
+ else
+ let tag = Tree.tag t in
+ let fl_list,llist,rlist,first,next = get_trans slist tag a t in
+ let sl1,res1 = loop (first t) llist t in
+ let sl2,res2 = if noright then null_result()
+ else loop (next t ctx) rlist ctx in
+ eval_fold2_slist fl_list sl1 sl2 res1 res2 t
+ in
+ let loop_no_right t slist ctx =
+ if Tree.is_nil t then null_result()
+ else
+ let tag = Tree.tag t in
+ let fl_list,llist,rlist,first,next = get_trans slist tag a t in
+ let sl1,res1 = loop (first t) llist t in
+ let sl2,res2 = null_result() in
+ eval_fold2_slist fl_list sl1 sl2 res1 res2 t
+ in
+ (if noright then loop_no_right else loop) t slist ctx
+
+ let run_top_down a t =
+ let init = cons a.init Nil in
+ let _,res = top_down a t init t 1
+ in res.(0)
+ ;;
+
+ module Configuration =
+ struct
+ module Ptss = Set.Make(Ptset)
+ module IMap = Map.Make(Ptset)
+ type t = { hash : int;
+ sets : Ptss.t;
+ results : RS.t IMap.t }
+ let empty = { hash = 0;
+ sets = Ptss.empty;
+ results = IMap.empty;
+ }
+ let is_empty c = Ptss.is_empty c.sets
+ let add c s r =
+ if Ptss.mem s c.sets then
+ { c with results = IMap.add s (RS.concat r (IMap.find s c.results)) c.results}
+ else
+ { hash = HASHINT2(c.hash,Ptset.hash s);
+ sets = Ptss.add s c.sets;
+ results = IMap.add s r c.results
+ }
+
+ let pr fmt c = Format.fprintf fmt "{";
+ Ptss.iter (fun s -> pr_st fmt (Ptset.elements s);
+ Format.fprintf fmt " ") c.sets;
+ Format.fprintf fmt "}\n%!";
+ IMap.iter (fun k d ->
+ pr_st fmt (Ptset.elements k);
+ Format.fprintf fmt "-> %i\n" (RS.length d)) c.results;
+ Format.fprintf fmt "\n%!"
+
+ let merge c1 c2 =
+ let acc1 = IMap.fold (fun s r acc ->
+ IMap.add s
+ (try
+ RS.concat r (IMap.find s acc)
+ with
+ | Not_found -> r) acc) c1.results IMap.empty
+ in
+ let imap =
+ IMap.fold (fun s r acc ->
+ IMap.add s
+ (try
+ RS.concat r (IMap.find s acc)
+ with
+ | Not_found -> r) acc) c2.results acc1
+ in
+ let h,s =
+ Ptss.fold
+ (fun s (ah,ass) -> (HASHINT2(ah,Ptset.hash s),
+ Ptss.add s ass))
+ (Ptss.union c1.sets c2.sets) (0,Ptss.empty)
+ in
+ { hash = h;
+ sets =s;
+ results = imap }
+
+ end
+ let fmt = Format.err_formatter
+ let pr x = Format.fprintf fmt x
+ let h_fold = Hashtbl.create 511
+
+ let fold_f_conf t slist fl_list conf dir=
+ let rec loop sl fl acc =
+ match sl,fl with
+ |Nil,[] -> acc
+ | Cons(s,hs,sll), formlist::fll ->
+ let r',rb,rb1,rb2,mark =
+ try
+ Hashtbl.find h_fold (hs,Formlist.hash formlist,dir)
+ with
+ Not_found -> let res =
+ if dir then eval_formlist ~memo:false s Ptset.empty formlist
+ else eval_formlist ~memo:false Ptset.empty s formlist
+ in (Hashtbl.add h_fold (hs,Formlist.hash formlist,dir) res;res)
+ in(*
+ let _ = pr "Evaluating on set (%s) with tree %s=%s"
+ (if dir then "left" else "right")
+ (Tag.to_string (Tree.tag t))
+ (Tree.dump_node t) ;
+ pr_st fmt (Ptset.elements s);
+ pr ", formualae (with hash %i): \n" (Formlist.hash formlist);
+ Formlist.pr fmt formlist;
+ pr "result is ";
+ pr_st fmt (Ptset.elements r');
+ pr " %b %b %b %b \n%!" rb rb1 rb2 mark ;
+ in *)
+ if rb && ((dir&&rb1)|| ((not dir) && rb2))
+ then
+ let acc =
+ let old_r =
+ try Configuration.IMap.find s conf.Configuration.results
+ with Not_found -> RS.empty
+ in
+ Configuration.add acc r' (if mark then RS.cons t old_r else old_r)
+ in
+ loop sll fll acc
+ else loop sll fll acc
+ | _ -> assert false
+ in
+ loop slist fl_list Configuration.empty
+
+ let h_trans = Hashtbl.create 4096
+
+ let get_up_trans slist ptag a tree =
+ let key = (HASHINT2(hpl slist,Tag.hash ptag)) in
+ try
+ Hashtbl.find h_trans key
+ with
+ | Not_found ->
+ let f_list,_ =
+ Hashtbl.fold (fun q l acc ->
+ List.fold_left (fun (fl_acc,h_acc) (ts,(m,f,_)) ->
+ if TagSet.mem ptag ts
+ then (Formlist.cons q f h_acc m fl_acc,
+ HASHINT3(h_acc,f.fid,q))
+ else (fl_acc,h_acc))
+ acc l)
+ a.phi (Formlist.nil,0)
+ in
+ let res = fold_pl (fun _ _ acc -> f_list::acc) slist []
+ in
+ (Hashtbl.add h_trans key res;res)
+
+
+ let rec bottom_up a tree conf next jump_fun root dotd init accu =
+ if (not dotd) && (Configuration.is_empty conf ) then
+ (* let _ = pr "Returning early from %s, with accu %i, next is %s\n%!"
+ (Tree.dump_node tree) (Obj.magic accu) (Tree.dump_node next)
+ in *)
+ accu,conf,next
+ else
+(* let _ =
+ pr "Going bottom up for tree with tag %s configuration is"
+ (if Tree.is_nil tree then "###" else Tag.to_string (Tree.tag tree));
+ Configuration.pr fmt conf
+ in *)
+ let below_right = Tree.is_below_right tree next in
+(* let _ = Format.fprintf Format.err_formatter "below_right %s %s = %b\n%!"
+ (Tree.dump_node tree) (Tree.dump_node next) below_right
+ in *)
+ let accu,rightconf,next_of_next =
+ if below_right then (* jump to the next *)
+(* let _ = pr "Jumping to %s\n%!" (Tree.dump_node next) in *)
+ bottom_up a next conf (jump_fun next) jump_fun (Tree.next_sibling tree) true init accu
+ else accu,Configuration.empty,next
+ in
+(* let _ = if below_right then pr "Returning from jump to next\n" in *)
+ let sub =
+ if dotd then
+ if below_right then (* only recurse on the left subtree *)
+ (* let _ = pr "Topdown on subtree\n%!" in *)
+ prepare_topdown a tree true
+ else
+(* let _ = pr "Topdown on whole tree\n%!" in *)
+ prepare_topdown a tree false
+ else conf
+ in
+ let conf,next =
+ (Configuration.merge rightconf sub, next_of_next)
+ in
+ if Tree.equal tree root then
+(* let _ = pr "Stopping at root, configuration after topdown is:" ;
+ Configuration.pr fmt conf;
+ pr "\n%!"
+ in *) accu,conf,next
+ else
+ let parent = Tree.binary_parent tree in
+ let ptag = Tree.tag parent in
+ let dir = Tree.is_left tree in
+ let slist = Configuration.Ptss.fold (fun e a -> cons e a) conf.Configuration.sets Nil in
+ let fl_list = get_up_trans slist ptag a parent in
+ let slist = rev_pl (slist) in
+(* let _ = pr "Current conf is : %i " (Tree.id tree);
+ Configuration.pr fmt conf;
+ pr "\n"
+ in *)
+ let newconf = fold_f_conf parent slist fl_list conf dir in
+(* let _ = pr "New conf before pruning is (dir=%b):" dir;
+ Configuration.pr fmt newconf ;
+ pr "accu is %i\n" (RS.length accu);
+ in *)
+ let accu,newconf = Configuration.IMap.fold (fun s res (ar,nc) ->
+ if Ptset.intersect s init then
+ ( RS.concat res ar ,nc)
+ else (ar,Configuration.add nc s res))
+ (newconf.Configuration.results) (accu,Configuration.empty)
+ in
+(* let _ = pr "New conf after pruning is (dir=%b):" dir;
+ Configuration.pr fmt newconf ;
+ pr "accu is %i\n" (RS.length accu);
+ in *)
+ bottom_up a parent newconf next jump_fun root false init accu
+
+ and prepare_topdown a t noright =
+(* pr "Going top down on tree with tag %s\n%!"
+ (if Tree.is_nil t then "###" else (Tag.to_string(Tree.tag t))); *)
+ let r = cons a.states Nil in
+ let set,res = top_down (~noright:noright) a t r t 1 in
+ let set = match set with
+ | Cons(x,_,Nil) ->x
+ | _ -> assert false
+ in
+(* pr "Result of topdown run is %!";
+ pr_st fmt (Ptset.elements set);
+ pr ", number is %i\n%!" (RS.length res.(0)); *)
+ Configuration.add Configuration.empty set res.(0)
+
+
+
+ let run_bottom_up_contains a t =
+ let trlist = Hashtbl.find a.phi (Ptset.choose a.init)
+ in
+ let init = List.fold_left
+ (fun acc (_,(_,f,_)) ->
+ Ptset.union acc (let (_,_,l) = fst (f.st) in l))
+ Ptset.empty trlist
+ in
+ let tree1 = Tree.text_below t in
+ let jump_fun = fun tree -> Tree.text_next tree t in
+ let tree2 = jump_fun tree1 in
+ let rec loop tree next acc =
+(* let _ = pr "\n_________________________\nNew iteration\n" in *)
+(* let _ = pr "Jumping to %s\n%!" (Tree.dump_node tree) in *)
+ let acc,conf,next_of_next = bottom_up a tree
+ Configuration.empty next jump_fun (Tree.root tree) true init acc
+ in
+ (* let _ = pr "End of first iteration, conf is:\n%!";
+ Configuration.pr fmt conf
+ in *)
+ let acc = Configuration.IMap.fold
+ ( fun s res acc -> if Ptset.intersect init s
+ then RS.concat res acc else acc) conf.Configuration.results acc
+ in
+ if Tree.is_nil next_of_next (*|| Tree.equal next next_of_next *)then
+ acc
+ else loop next_of_next (jump_fun next_of_next) acc
+ in
+ loop tree1 tree2 RS.empty
+
+
+
+
+
+
+
+
+
+
+
+
+
+ end
+
+ let top_down_count a t = let module RI = Run(Integer) in Integer.length (RI.run_top_down a t)
+ let top_down a t = let module RI = Run(IdSet) in (RI.run_top_down a t)
+ let bottom_up_count_contains a t = let module RI = Run(Integer) in Integer.length (RI.run_bottom_up_contains a t)
+ let bottom_up_count a t = failwith "not implemented"
+