+(*
+ module Algebra =
+ struct
+ type jump = [ `LONG | `CLOSE | `NIL ]
+ type t = jump*Ptset.Int.t
+
+ let merge_jump (j1,l1) (j2,l2) =
+ match j1,j2 with
+ | _ when j1 = j2 -> (j1,Ptset.Int.union l1 l2)
+ | _,`NIL -> j1,l1
+ | `NIL,_ -> j2,l2
+ | _,_ -> (`CLOSE, Ptset.Int.union l1 l2)
+
+ let merge_jump_list = function
+ | [] -> `NIL,Ptset.Int.empty
+ | p::r -> List.fold_left (merge_jump) p r
+
+ let labels a s =
+ Hashtbl.fold
+ (
+ fun q l acc ->
+ if (q == s)
+ then
+
+ (List.fold_left
+ (fun acc (ts,f) ->
+ let _,_,_,bur = Transition.node f in
+ if bur then acc else TagSet.cup acc ts)
+ acc l)
+ else acc ) a.trans TagSet.empty
+ exception Found
+
+ let is_rec a s access =
+ List.exists
+ (fun (_,t) -> let _,_,f,_ = Transition.node t in
+ StateSet.mem s (access f)) (Hashtbl.find a.trans s)
+
+
+ let decide a c_label l_label dir_states access =
+
+ let l = StateSet.fold
+ (fun s l ->
+ let s_rec= is_rec a s access in
+ let tlabels,jmp =
+ if s_rec then l_label,`LONG
+ else c_label,`CLOSE in
+ let slabels = TagSet.positive ((TagSet.cap (labels a s) tlabels))
+ in
+ (if Ptset.Int.is_empty slabels
+ then `NIL,Ptset.Int.empty
+ else jmp,slabels)::l) dir_states []
+ in merge_jump_list l
+
+
+
+
+
+ end
+
+
+ let choose_jump tagset qtags1 qtagsn a f_nil f_t1 f_s1 f_tn f_sn f_notext f_maytext =
+ let tags1,hastext1,fin1 = inter_text tagset (tags a qtags1) in
+ let tagsn,hastextn,finn = inter_text tagset (tags a qtagsn) in
+ (*if (hastext1||hastextn) then (`ANY,f_text) (* jumping to text nodes doesn't work really well *)
+ else*)
+ if (Ptset.Int.is_empty tags1) && (Ptset.Int.is_empty tagsn) then (`NIL,f_nil)
+ else if (Ptset.Int.is_empty tagsn) then
+ if (Ptset.Int.is_singleton tags1)
+ then (* TaggedChild/Sibling *)
+ let tag = (Ptset.Int.choose tags1) in (`TAG(tag),mk_app_fun f_t1 tag (Tag.to_string tag))
+ else (* SelectChild/Sibling *)
+ (`ANY,mk_app_fun f_s1 tags1 (string_of_ts tags1))
+ else if (Ptset.Int.is_empty tags1) then
+ if (Ptset.Int.is_singleton tagsn)
+ then (* TaggedDesc/Following *)
+ let tag = (Ptset.Int.choose tagsn) in (`TAG(tag),mk_app_fun f_tn tag (Tag.to_string tag))
+ else (* SelectDesc/Following *)
+ (`ANY,mk_app_fun f_sn tagsn (string_of_ts tagsn))
+ else if (hastext1||hastextn) then (`ANY,f_maytext)
+ else (`ANY,f_notext)
+
+ let choose_jump_down tree a b c d =
+ choose_jump a b c d
+ (mk_fun (fun _ -> Tree.nil) "Tree.mk_nil")
+ (mk_fun (Tree.tagged_child tree) "Tree.tagged_child")
+ (mk_fun (Tree.select_child tree) "Tree.select_child")
+ (mk_fun (Tree.tagged_desc tree) "Tree.tagged_desc")
+ (mk_fun (Tree.select_desc tree) "Tree.select_desc")
+ (mk_fun (Tree.first_element tree) "Tree.first_element")
+ (mk_fun (Tree.first_child tree) "Tree.first_child")
+
+ let choose_jump_next tree a b c d =
+ choose_jump a b c d
+ (mk_fun (fun _ _ -> Tree.nil) "Tree.mk_nil2")
+ (mk_fun (Tree.tagged_sibling_ctx tree) "Tree.tagged_sibling_ctx")
+ (mk_fun (Tree.select_sibling_ctx tree) "Tree.select_sibling_ctx")
+ (mk_fun (Tree.tagged_foll_ctx tree) "Tree.tagged_foll_ctx")
+ (mk_fun (Tree.select_foll_ctx tree) "Tree.select_foll_ctx")
+ (mk_fun (Tree.next_element_ctx tree) "Tree.node_element_ctx")
+ (mk_fun (Tree.next_sibling_ctx tree) "Tree.node_sibling_ctx")
+*)
+ module Algebra =
+ struct
+ type jump = [ `NIL | `ANY |`ANYNOTEXT | `JUMP ]
+ type t = jump*Ptset.Int.t*Ptset.Int.t
+ let jts = function
+ | `JUMP -> "JUMP"
+ | `NIL -> "NIL"
+ | `ANY -> "ANY"
+ | `ANYNOTEXT -> "ANYNOTEXT"
+ let merge_jump (j1,c1,l1) (j2,c2,l2) =
+ match j1,j2 with
+ | _,`NIL -> (j1,c1,l1)
+ | `NIL,_ -> (j2,c2,l2)
+ | `ANY,_ -> (`ANY,Ptset.Int.empty,Ptset.Int.empty)
+ | _,`ANY -> (`ANY,Ptset.Int.empty,Ptset.Int.empty)
+ | `ANYNOTEXT,_ ->
+ if Ptset.Int.mem Tag.pcdata (Ptset.Int.union c2 l2) then
+ (`ANY,Ptset.Int.empty,Ptset.Int.empty)
+ else
+ (`ANYNOTEXT,Ptset.Int.empty,Ptset.Int.empty)
+ | _,`ANYNOTEXT ->
+ if Ptset.Int.mem Tag.pcdata (Ptset.Int.union c1 l1) then
+ (`ANY,Ptset.Int.empty,Ptset.Int.empty)
+ else
+ (`ANYNOTEXT,Ptset.Int.empty,Ptset.Int.empty)
+ | `JUMP,`JUMP -> (`JUMP, Ptset.Int.union c1 c2,Ptset.Int.union l1 l2)
+
+ let merge_jump_list = function
+ | [] -> `NIL,Ptset.Int.empty,Ptset.Int.empty
+ | p::r ->
+ List.fold_left (merge_jump) p r
+
+ let labels a s =
+ Hashtbl.fold
+ (
+ fun q l acc ->
+ if (q == s)
+ then
+
+ (List.fold_left
+ (fun acc (ts,f) ->
+ let _,_,_,bur = Transition.node f in
+ if bur then acc else TagSet.cup acc ts)
+ acc l)
+ else acc ) a.trans TagSet.empty
+ exception Found
+
+ let is_rec a s access =
+ List.exists
+ (fun (_,t) -> let _,_,f,_ = Transition.node t in
+ StateSet.mem s ((fun (_,_,x) -> x) (access (Formula.st f)))) (Hashtbl.find a.trans s)
+
+
+ let decide a c_label l_label dir_states dir =
+
+ let l = StateSet.fold
+ (fun s l ->
+ let s_rec = is_rec a s (if dir then fst else snd) in
+ let s_rec = if dir then s_rec else
+ (* right move *)
+ is_rec a s fst
+ in
+ let s_lab = labels a s in
+ let jmp,cc,ll =
+ if (not (TagSet.is_finite s_lab)) then
+ if TagSet.mem Tag.pcdata s_lab then (`ANY,Ptset.Int.empty,Ptset.Int.empty)
+ else (`ANYNOTEXT,Ptset.Int.empty,Ptset.Int.empty)
+ else
+ if s_rec
+ then (`JUMP,Ptset.Int.empty, TagSet.positive
+ (TagSet.cap (TagSet.inj_positive l_label) s_lab))
+ else (`JUMP,TagSet.positive
+ (TagSet.cap (TagSet.inj_positive c_label) s_lab),
+ Ptset.Int.empty )
+ in
+ (if jmp != `ANY
+ && jmp != `ANYNOTEXT
+ && Ptset.Int.is_empty cc
+ && Ptset.Int.is_empty ll
+ then (`NIL,Ptset.Int.empty,Ptset.Int.empty)
+ else (jmp,cc,ll))::l) dir_states []
+ in merge_jump_list l
+
+
+ end
+
+
+
+ let choose_jump (d,cl,ll) f_nil f_t1 f_s1 f_tn f_sn f_s1n f_notext f_maytext =
+ match d with
+ | `NIL -> (`NIL,f_nil)
+ | `ANYNOTEXT -> `ANY,f_notext
+ | `ANY -> `ANY,f_maytext
+ | `JUMP ->
+ if Ptset.Int.is_empty cl then
+ if Ptset.Int.is_singleton ll then
+ let tag = Ptset.Int.choose ll in
+ (`TAG(tag),mk_app_fun f_tn tag (Tag.to_string tag))
+ else
+ (`ANY,mk_app_fun f_sn ll (string_of_ts ll))
+ else if Ptset.Int.is_empty ll then
+ if Ptset.Int.is_singleton cl then
+ let tag = Ptset.Int.choose cl in
+ (`TAG(tag),mk_app_fun f_t1 tag (Tag.to_string tag))
+ else
+ (`ANY,mk_app_fun f_s1 cl (string_of_ts cl))
+ else
+ (`ANY,mk_app_fun2 f_s1n cl ll ((string_of_ts cl) ^ " " ^ (string_of_ts ll)))
+
+ | _ -> assert false
+
+ let choose_jump_down tree d =
+ choose_jump d
+ (mk_fun (fun _ -> Tree.nil) "Tree.mk_nil")
+ (mk_fun (Tree.tagged_child tree) "Tree.tagged_child")
+ (mk_fun (Tree.select_child tree) "Tree.select_child")
+ (mk_fun (Tree.tagged_desc tree) "Tree.tagged_desc")
+ (mk_fun (Tree.select_desc tree) "Tree.select_desc")
+ (mk_fun (fun _ _ -> Tree.first_child tree) "[FIRSTCHILD]Tree.select_child_desc")
+ (mk_fun (Tree.first_element tree) "Tree.first_element")
+ (mk_fun (Tree.first_child tree) "Tree.first_child")
+
+ let choose_jump_next tree d =
+ choose_jump d
+ (mk_fun (fun _ _ -> Tree.nil) "Tree.mk_nil2")
+ (mk_fun (Tree.tagged_sibling_ctx tree) "Tree.tagged_sibling_ctx")
+ (mk_fun (Tree.select_sibling_ctx tree) "Tree.select_sibling_ctx")
+ (mk_fun (Tree.tagged_foll_ctx tree) "Tree.tagged_foll_ctx")
+ (mk_fun (Tree.select_foll_ctx tree) "Tree.select_foll_ctx")
+ (mk_fun (fun _ _ -> Tree.next_sibling_ctx tree) "[NEXTSIBLING]Tree.select_sibling_foll_ctx")
+ (mk_fun (Tree.next_element_ctx tree) "Tree.next_element_ctx")
+ (mk_fun (Tree.next_sibling_ctx tree) "Tree.node_sibling_ctx")
+
+ module SetTagKey =
+ struct
+ type t = Tag.t*SList.t
+ let equal (t1,s1) (t2,s2) = t1 == t2 && s1 == s2
+ let hash (t,s) = HASHINT2(t,s.SList.Node.id)
+ end