- 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)
+ 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 is_final_marking a s =
+ List.exists (fun (_,t) -> let _,_,m,f,_ = Transition.node t in m&& (Formula.is_true 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
+ (`MANY(ll),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
+ (`MANY(cl),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