- in eval f
-
-
-
- let fstate_pool = Hashtbl.create 11
-
- let merge_pred a b = match a,b with
- | Some(f1), Some(f2) -> Some(fun x -> f1 x || f2 x)
- | None,None -> None
- | None,Some(_) -> b
- | Some(_),None -> a
-
- let acc_pred p l1 l2 = match p with
- | `Left _ -> p::l1,l2
- | `Right _ -> l1,p::l2
- | _ -> l1,l2
-
-
- let merge_trans t a tag q acc =
- List.fold_left (fun (accf,accm,acchtrue) (ts,(m,f,pred)) ->
- if TagSet.mem tag ts
- then
- let tmpf,hastrue =
- if is_true f then
- let newfinal =
- try Hashtbl.find fstate_pool f.fid with
- | Not_found -> let s = mk_state() in
- a.states <- Ptset.add s a.states;
- a.final <- Ptset.add s a.final;
- Hashtbl.add fstate_pool f.fid s;s
- in
- (atom_ `Left true newfinal),true
- else f,false in
- (or_ tmpf accf,accm||m,acchtrue||hastrue)
- else (accf,accm,acchtrue)
- ) acc (Hashtbl.find a.phi q)
-
-
- let get_trans t a tag r =
- try
- let mark,f,predl,has_true =
- HTagSet.find a.sigma (r,tag)
- in f.st,f,mark,has_true,r
- with
- Not_found ->
- let f,mark,has_true,accq =
- Ptset.fold (fun q (accf,accm,acchtrue,accq) ->
- let naccf,naccm,nacctrue =
- merge_trans t a tag q (accf,accm,acchtrue )
- in
- if is_false naccf then (naccf,naccm,nacctrue,accq)
- else (naccf,naccm,nacctrue,Ptset.add q accq)
- )
- 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 check_pred l t = true (*l = [] ||
- List.exists (function p ->
- match p with
- `Left f | `Right f -> f t
- | _ -> assert false) l
- *)
-
+ let choose_jump_down a b c d =
+ choose_jump a b c d
+ (mk_fun (Tree.mk_nil) "Tree.mk_nil")
+ (mk_fun (Tree.text_below) "Tree.text_below")
+ (mk_fun (fun _ -> Tree.node_child) "[TaggedChild]Tree.node_child") (* !! no tagged_child in Tree.ml *)
+ (mk_fun (fun _ -> Tree.node_child) "[SelectChild]Tree.node_child") (* !! no select_child in Tree.ml *)
+ (mk_fun (Tree.tagged_desc) "Tree.tagged_desc")
+ (mk_fun (fun _ -> Tree.node_child ) "[SelectDesc]Tree.node_child") (* !! no select_desc *)
+ (mk_fun (Tree.node_child) "Tree.node_child")
+
+ let choose_jump_next a b c d =
+ choose_jump a b c d
+ (mk_fun (fun t _ -> Tree.mk_nil t) "Tree.mk_nil2")
+ (mk_fun (Tree.text_next) "Tree.text_next")
+ (mk_fun (fun _ -> Tree.node_sibling_ctx) "[TaggedSibling]Tree.node_sibling_ctx")(* !! no tagged_sibling in Tree.ml *)
+ (mk_fun (fun _ -> Tree.node_sibling_ctx) "[SelectSibling]Tree.node_sibling_ctx")(* !! no select_sibling in Tree.ml *)
+ (mk_fun (Tree.tagged_foll_below) "Tree.tagged_foll_below")
+ (mk_fun (fun _ -> Tree.node_sibling_ctx) "[SelectFoll]Tree.node_sibling_ctx")(* !! no select_foll *)
+ (mk_fun (Tree.node_sibling_ctx) "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 =
+ StateSet.fold
+ (fun q acc ->
+ List.fold_left
+ (fun ((fl_acc,ll_acc,rl_acc,c_acc,d_acc,s_acc,f_acc) as acc)
+ (ts,t) ->
+ if (TagSet.mem tag ts)
+ then
+ let _,_,f,_ = Transition.node t in
+ let (child,desc,below),(sibl,foll,after) = Formula.st f in
+ (Formlist.add t fl_acc,
+ StateSet.union ll_acc below,
+ StateSet.union rl_acc after,
+ StateSet.union child c_acc,
+ StateSet.union desc d_acc,
+ StateSet.union sibl s_acc,
+ StateSet.union foll f_acc)
+ else acc ) acc (
+ try Hashtbl.find a.trans q
+ with
+ Not_found -> Printf.eprintf "Looking for state %i, doesn't exist!!!\n%!"
+ q;[]
+ )
+
+ ) set (Formlist.empty,StateSet.empty,StateSet.empty,ca,da,sa,fa)
+ in fl::fll_acc, cons ll lllacc, cons rr rllacc,ca,da,sa,fa)
+ slist ([],Nil,Nil,StateSet.empty,StateSet.empty,StateSet.empty,StateSet.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 = loop (next t ctx) rlist ctx in
+ let res = eval_fold2_slist fl_list sl1 sl2 res1 res2 t
+ in
+ D_IGNORE_(
+ register_trace t (slist,(fst res),sl1,sl2,fl_list,first,next,ctx),
+ res)
+ 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
+ let res = eval_fold2_slist fl_list sl1 sl2 res1 res2 t
+ in
+ D_IGNORE_(
+ register_trace t (slist,(fst res),sl1,sl2,fl_list,first,next,ctx),
+ res)
+ in
+ (if noright then loop_no_right else loop) t slist ctx
+