Added correct decision procedure

git-svn-id: svn+ssh://idea.nguyen.vg/svn/sxsi/trunk/xpathcomp@407 3cdefd35-fc62-479d-8e8d-bae585ffb9ca

diff --git a/ata.ml b/ata.ml
index 42bf24e..eb4f394 100644 (file)
--- a/ata.ml
+++ b/ata.ml
@@ -512,11 +512,13 @@ END
       let mk_fun f s = D_IGNORE_(register_funname f s,f)
       let mk_app_fun f arg s = let g = f arg in 
        D_IGNORE_(register_funname g ((get_funname f) ^ " " ^ s), g) 
+      let mk_app_fun2 f arg1 arg2 s = let g = f arg1 arg2 in 
+       D_IGNORE_(register_funname g ((get_funname f) ^ " " ^ s), g) 
 
       let string_of_ts tags = (Ptset.Int.fold (fun t a -> a ^ " " ^ (Tag.to_string t) ) tags "{")^ " }"
 
 
-
+(*
       module Algebra =
        struct
          type jump = [ `LONG | `CLOSE | `NIL ]
@@ -616,6 +618,139 @@ END
          (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 
@@ -726,14 +861,16 @@ END
                      slist (Formlistlist.nil,SList.nil,SList.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 tree tag in
+                 let tags_child,tags_below,tags_siblings,tags_after = Tree.tags tree tag in
+                 let d_f = Algebra.decide a tags_child tags_below (StateSet.union ca da) true in
+                 let d_n = Algebra.decide a tags_siblings tags_after (StateSet.union sa fa) false in
 (*               let _ = Printf.eprintf "Tags below %s are : \n" (Tag.to_string tag) in
                  let _ = Ptset.Int.iter (fun i -> Printf.eprintf "%s " (Tag.to_string i)) tags_below in
                  let _ = Printf.eprintf "\n%!" in *)
-                 let tags_below = Ptset.Int.remove tag tags_below in
-                 let f_kind,first = choose_jump_down tree tags_below ca da a
+(*               let tags_below = Ptset.Int.remove tag tags_below in *)
+                 let f_kind,first = choose_jump_down tree d_f
                  and n_kind,next = if noright then (`NIL, fun _ _ -> Tree.nil )
-                 else choose_jump_next tree tags_after sa fa a in
+                 else choose_jump_next tree d_n in
                  let empty_res = null_result in
                   let cont =
                     match f_kind,n_kind with

diff --git a/finiteCofinite.ml b/finiteCofinite.ml
index 58f0730..907b604 100644 (file)
--- a/finiteCofinite.ml
+++ b/finiteCofinite.ml
@@ -41,6 +41,8 @@ sig
   val equal : t -> t -> bool
   val positive : t -> set
   val negative : t -> set
+  val inj_positive : set -> t
+  val inj_negative : set -> t
 end
 
 module Make (E : Sigs.Set) : S with type elt = E.elt and type set = E.t =
@@ -192,5 +194,7 @@ struct
       | CoFinite x -> x
       | _ -> E.empty
 
+  let inj_positive t = Finite t
+  let inj_negative t = CoFinite t
 end
 

diff --git a/finiteCofinite.mli b/finiteCofinite.mli
index 7f98130..72b1aec 100644 (file)
--- a/finiteCofinite.mli
+++ b/finiteCofinite.mli
@@ -35,6 +35,8 @@ module type S =
     val equal : t -> t -> bool
     val positive : t -> set
     val negative : t -> set
+    val inj_positive : set -> t
+    val inj_negative : set -> t
   end
 
 module Make :  functor (E : Sigs.Set) -> S with type elt = E.elt and type set = E.t