improvements...
[SXSI/xpathcomp.git] / ata.ml
diff --git a/ata.ml b/ata.ml
index bba3203..bb38863 100644 (file)
--- a/ata.ml
+++ b/ata.ml
@@ -1,6 +1,7 @@
 INCLUDE "debug.ml"
 INCLUDE "utils.ml"
 
+type jump_kind = [ `TAG of Tag.t | `CONTAINS of string | `NOTHING ]
 let cpt_trans = ref 0
 let miss_trans = ref 0
 let cpt_eval = ref 0
@@ -398,8 +399,8 @@ type 'a t = {
            let b,b1,b2 = eval_form_bool f s1 s2 in
            let r = if b then (Ptset.add q s, b, b1'||b1,b2'||b2,mark||amark)
            else s,b',b1',b2',amark
-           in
-(*           Format.fprintf Format.err_formatter "\nEvaluating formula (%i) %i %s" h q (if mark then "=>" else "->");
+           in(*
+             Format.fprintf Format.err_formatter "\nEvaluating formula (%i) %i %s" h q (if mark then "=>" else "->");
              pr_frm (Format.err_formatter) f;
              Format.fprintf Format.err_formatter " in context ";
              pr_st Format.err_formatter (Ptset.elements s1);
@@ -438,467 +439,7 @@ type 'a t = {
     let r_ignore _ x = x
       
     let set_get_tag r t = r := (fun _ -> t)
-      (*
-
-       let merge_trans t a tag q acc = 
-       List.fold_left (fun (accf,acchash,idx) (ts,(m,f,pred)) ->
-       if TagSet.mem tag ts 
-       then
-       let acchash = HASHINT3(acchash,f.fid,q) in
-       (Cons(q,f,acchash,idx,m,accf),acchash,idx+1)
-       else (accf,acchash,idx)
-       ) acc (try Hashtbl.find a.phi q with Not_found -> [])
-
-       
-
-    let cast_cont :'b -> ('a t -> Tree.t -> Tree.t -> Ptset.t*'a) = 
-      Obj.magic 
-
-    let get_trans conti t a tag r = 
-      try      
-         Hashtbl.find a.sigma (HASHINT2(Ptset.hash r,Tag.hash tag))
-      with
-         Not_found -> 
-           let fl,_,accq,_ = 
-             Ptset.fold (fun q (accf,acchash,accq,aidx) ->
-                           let naccf,acchash,naidx =
-                             merge_trans t a tag q (accf,acchash,aidx )
-                           in
-                             (naccf,acchash,Ptset.add q accq,naidx)
-                        )
-               r (Nil,17,Ptset.empty,0)
-           in 
-           let (ls,lls,llls),(rs,rrs,rrrs) = 
-            form_list_fold_left (fun ((a1,b1,c1),(a2,b2,c2)) _ f _ _ _ ->
-                                   let (x1,y1,z1),(x2,y2,z2) = f.st in
-                                     ((Ptset.union x1 a1),(Ptset.union y1 b1),(Ptset.union c1 z1)),
-                                   ((Ptset.union x2 a2),(Ptset.union y2 b2),(Ptset.union c2 z2)))
-              ((Ptset.empty,Ptset.empty,Ptset.empty),
-               (Ptset.empty,Ptset.empty,Ptset.empty))
-               fl 
-           in
-           let tb,ta = 
-             Tree.tags t tag 
-           in 
-           let tl,htlt,lfin = inter_text tb (tags a ls)
-           and tll,htllt,llfin = inter_text tb (tags a lls)
-           and tr,htrt,rfin = inter_text ta (tags a rs)
-           and trr,htrrt,rrfin = inter_text ta  (tags a rrs)
-           in
-           let get_tag = ref Tree.tag in
-           let first,flabel =
-             if (llfin && lfin) then (* no stars *)
-               (if htlt || htllt then (Tree.text_below, "#text_below")
-                else
-                  let etl = Ptset.is_empty tl
-                  and etll = Ptset.is_empty tll
-                  in
-                    if (etl && etll)
-                        then (Tree.mk_nil, "#mk_nil")
-                        else
-                          if etl then 
-                            if Ptset.is_singleton tll 
-                            then begin
-                              set_get_tag get_tag (Ptset.choose tll);
-                              (Tree.tagged_desc (Ptset.choose tll), "#tagged_desc")
-                            end
-                            else (Tree.select_desc_only tll, "#select_desc_only")
-                          else if etll then (Tree.node_child,"#node_child")
-                          else (Tree.select_below tl tll,"#select_below"))
-                 else (* stars or node() *)
-                   if htlt||htllt then (Tree.first_child,"#first_child")
-                   else (Tree.node_child,"#node_child")
-           and next,nlabel =
-             if (rrfin && rfin) then (* no stars *)
-               ( if htrt || htrrt
-                 then (Tree.text_next, "#text_next")
-                   else
-                     let etr = Ptset.is_empty tr
-                     and etrr = Ptset.is_empty trr
-                     in
-                       if etr && etrr 
-                       then (mk_nil_ctx, "#mk_nil_ctx")
-                       else
-                         if etr then
-                           if Ptset.is_singleton trr 
-                           then begin
-                             set_get_tag get_tag (Ptset.choose trr);
-                             (Tree.tagged_foll_below (Ptset.choose trr),"#tagged_foll_below")
-                           end
-                           else (Tree.select_foll_only trr,"#select_foll_only")
-                         else if etrr then (Tree.node_sibling_ctx,"#node_sibling_ctx")
-                         else  
-                           (Tree.select_next tr trr,"#select_next") )
-
-                 else if htrt || htrrt then (Tree.next_sibling_ctx,"#next_sibling_ctx")
-                 else (Tree.node_sibling_ctx,"#node_sibling_ctx")
-           in
-           let cont = let flist = fl in
-             fun a t res ctx -> 
-               let s1,res1 = conti a (first t) llls res t
-               and s2,res2 = conti a (next t ctx) rrrs res ctx in
-               let r',rb,rb1,rb2,mark,idxl = eval_formlist s1 s2 flist
-               in      
-                 r',(vb rb)*((vb mark)  + (vb rb1)*res1 + (vb rb2)*res2)         
-           in
-             Hashtbl.add a.sigma (HASHINT2(Ptset.hash r,Tag.hash tag)) (cast_cont cont);
-             (cast_cont cont)
-               
-       
-(*
-    let rec accepting_among a t r ctx =           
-      if Tree.is_nil t || Ptset.is_empty r then Ptset.empty,0,TS.Nil else 
-       let dispatch,mark,flist,llls,rrrs =
-         get_trans (fun _ _ _ _ -> failwith "toto") t a (Tree.tag t) r
-       in
-       let s1,n1,res1 = accepting_among a (dispatch.first t) llls t in
-       let s2,n2,res2 = accepting_among a (dispatch.next t ctx) rrrs ctx in
-       let r',rb,rb1,rb2 = eval_formlist s1 s2 flist in
-         r',(vb rb)*((vb mark) + (vb rb1)* n1 + (vb rb2)*n2),if rb then 
-           dispatch.consres t res1 res2 rb1 rb2
-         else TS.Nil *)
-
-    let run a t = assert false (*
-      let st,n,res = accepting_among a t a.init t in
-        if Ptset.is_empty (st) then TS.empty,0 else res,n *)
-    let rec accepting_among_count_no_star  a t r ctx  =
-      if Tree.is_nil t then Ptset.empty,0 else 
-       (get_trans (accepting_among_count_no_star) t a (Tree.tag t) r)
-         a t ctx
-           
-(*
-    let rec accepting_among_count_star a t n =     
-       if Tree.is_nil t then n else 
-         if (Tree.tag t == Tag.attribute) 
-         then accepting_among_count_star a (Tree.node_sibling t) n
-         else accepting_among_count_star a (Tree.node_sibling t) 
-           (accepting_among_count_star a (Tree.node_child t) (1+n))
-
-    let rec accepting_among_count_may_star starstate a t r ctx =
-      if r == starstate then starstate,(accepting_among_count_star a t 0)
-      else
-       if Tree.is_nil t||Ptset.is_empty r then Ptset.empty,0 else 
-         let dispatch,mark,flist,llls,rrrs =
-           get_trans (fun _ _ _ _ -> failwith "toto") t a (Tree.tag t) r
-         in    
-         let s1,res1 = accepting_among_count_may_star starstate a (dispatch.first t) llls t
-         and s2,res2 = accepting_among_count_may_star starstate a (dispatch.next t ctx) rrrs ctx
-         in
-         let r',rb,rb1,rb2 = eval_formlist s1 s2 flist
-         in    
-           r',(vb rb)*((vb mark) + (vb rb1)*res1 + (vb rb2)*res2)      
-       
-*)
-    let run_count a t = 
-      
-      let st,res = match a.starstate with 
-       | None -> accepting_among_count_no_star  a t a.init t 
-       | Some s -> assert false (*accepting_among_count_may_star s a t a.init t  *)
-      in
-        if Ptset.is_empty (st) then 0 else  res
-
-         
-    let run_time _ _ = failwith "blah"
-         
-
-    module RealBottomUp = struct
-
-      (* decrease number of arguments *) 
-      let ton t = if Tree.is_nil t then "##"
-      else Tag.to_string (Tree.tag t)
-      ;;
-      let ion t = Tree.dump_node t
-      let memo = Hashtbl.create 4097
-      let rlist = ref []
-
-       let cpt = ref 0;;
-      let rec run a t res r root rinit next targettag r0 first tomark =
-       incr cpt;
-       let res = (vb tomark) + res in
-       let newr,newres = if first then
-         accepting_among_count_no_star  a t r t 
-       else r, res
-       in      
-       let r,res = if Ptset.is_empty newr then r,0 else newr,newres in   
-         if Tree.equal t root then 
-           if Ptset.intersect r rinit then (r,res,next) 
-           else (Ptset.empty,0,next)
-         else
-         let tag = Tree.tag t in
-         let parent = Tree.binary_parent t in
-         let parent_tag = Tree.tag parent in
-         let left = Tree.is_left t in
-         let r',mark =
-             try Hashtbl.find memo (r,parent_tag,left) with
-               | Not_found ->
-                   let pair = 
-                     Hashtbl.fold 
-                       (fun q l acc -> 
-                          List.fold_left 
-                            (fun (aq,am) (ts,(mark,form,_)) ->
-                               if TagSet.mem parent_tag ts then
-                                 let (value,_,_) = if left then
-                                   eval_form_bool form r Ptset.empty
-                                 else
-                                   eval_form_bool form Ptset.empty r
-                                 in
-(*                               let _ = if value then begin
-                                   Format.fprintf Format.err_formatter "Can take transition (%i,%s)%s%!"
-                                     q (Tag.to_string parent_tag) 
-                                     (if mark then "=>" else "->");
-                                   pr_frm Format.err_formatter form;
-                                   Format.fprintf Format.err_formatter "%! %s(" (if left then "left" else "right");
-                                   pr_st Format.err_formatter (Ptset.elements r);
-                                   Format.fprintf Format.err_formatter ")\n%!" end;
-                             in *)
-                                   if value then (Ptset.add q aq, mark||am) 
-                                   else (aq,am)
-                               else (aq,am))
-                            acc l                              
-                       ) a.phi (Ptset.empty,false)
-                   in Hashtbl.add memo (r,parent_tag,left) pair;pair
-         in
-           if Ptset.is_empty r' then Ptset.empty,0,next
-           else
-           if Tree.is_below_right t next then
-             let rn,resn,nextofnext = run a next 0 r0 t r (Tree.tagged_next next targettag) targettag r0 true false
-             in
-             let rn,resn = if Ptset.is_empty rn then Ptset.empty,0 else rn,resn in
-               run a (parent) (resn+res) r' root rinit nextofnext targettag r0 false false
-           else
-             run a (parent) (res) r' root rinit next targettag r0 false (mark&&left)
-                           
-               
-               
-      let accept_count a t tag initset =
-       let tree1 = Tree.tagged_lowest t tag in
-       let tree2 = Tree.tagged_next tree1 tag in
-         let c,b,_ =run a tree1 0 initset t a.init tree2 tag initset true false
-         in Printf.eprintf "%i\n%!" !cpt;
-           if Ptset.is_empty c then 0 else b
-                           
-    end *)
-(*
-    module RealBottomUp2 = struct
-      module Formlist = 
-      struct
-       type t = formlist
-       let nil : t = Nil
-       let cons q f i m l = Cons(q,f,i,m,l)
-       let hash = function Nil -> 0 | Cons(_,_,i,_,_) -> max_int land i
-       let pr fmt l = 
-         let rec loop = function
-           | Nil -> ()
-           | Cons(q,f,_,m,l) ->
-               Format.fprintf fmt "%i %s" q (if m then "=>" else "->");
-               pr_frm fmt f;
-               Format.fprintf fmt "\n%!";
-               loop l
-         in
-           loop l
-      end
-
-      type ptset_list = Nil | Cons of Ptset.t*int*ptset_list
-      let hpl l = match l with
-       | Nil -> 0
-       | Cons (_,i,_) -> i 
 
-      let cons s l = Cons (s,(Ptset.hash s) + 65599 * (hpl l), l)
-         
-      let rec empty_size n = 
-       if n == 0 then Nil
-       else cons Ptset.empty (empty_size (n-1))
-       
-      let fold_pl f l acc = 
-       let rec loop l acc = match l with
-           Nil -> acc
-         | Cons(s,h,pl) -> loop pl (f s h acc)
-       in
-         loop l acc
-      let map_pl f l = 
-       let rec loop =
-         function Nil -> Nil 
-           | Cons(s,h,ll) -> cons (f s) (loop ll) 
-       in loop l
-
-      let rev_pl l = 
-       let rec loop acc l = match l with 
-         | Nil -> acc
-         | Cons(s,_,ll) -> loop (cons s acc) ll
-       in
-         loop Nil l
-
-      let rev_map_pl f l  = 
-       let rec loop acc l = 
-         match l with 
-           | Nil -> acc
-           | Cons(s,_,ll) -> loop (cons (f s) acc) ll
-       in
-         loop Nil l
-
-      let merge_int _ rb rb1 rb2 mark _ res1 res2 =
-       if rb then (vb mark) + ((vb rb1)*res1) + ((vb rb2)*res2)
-       else 0
-
-      let td_trans = Hashtbl.create 4096 
-       
-      let choose_jump tagset qtags1 qtagsn a f_nil f_text f_t1 f_s1 f_tn f_sn f_notext =
-       let tags1,hastext1,fin1 = inter_text tagset (tags a qtags1) in
-       let tagsn,hastextn,finn = inter_text tagset (tags a qtagsn) in
-(*       Format.fprintf Format.err_formatter "Tags below states ";
-         pr_st Format.err_formatter (Ptset.elements qtags1);
-         Format.fprintf Format.err_formatter " are { ";
-         Ptset.iter (fun t -> Format.fprintf Format.err_formatter "%s " (Tag.to_string t)) tags1;
-         Format.fprintf Format.err_formatter "}, %b,%b\n%!" hastext1 fin1;
-
-         Format.fprintf Format.err_formatter "Tags below states ";
-         pr_st Format.err_formatter (Ptset.elements qtagsn);
-         Format.fprintf Format.err_formatter " are { ";
-         Ptset.iter (fun t -> Format.fprintf Format.err_formatter "%s " (Tag.to_string t)) tagsn;
-         Format.fprintf Format.err_formatter "}, %b,%b\n%!" hastextn finn;
-*)
-         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 _ -> 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 _ -> 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)
-         
-      module type RS = sig
-       type t
-       type elt
-       val empty : t
-       val cons : elt -> t -> t
-       val concat : t -> t -> t
-      end
-       
-                                   
-      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 top_down ?(noright=false) a merge null 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 null rb rb1 rb2 mark t res1.(i) res2.(i) 
-               in
-(*             let _ = Format.fprintf Format.err_formatter "(%b,%b,%b,%b) Result was %i %i, now %i\n%!"
-                 rb rb1 rb2 mark (Obj.magic res1.(i))  (Obj.magic res2.(i)) (Obj.magic res.(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 rec loop  t slist ctx = 
-         if Tree.is_nil t then (pempty,Array.make slot_size null)
-         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 (pempty,Array.make slot_size null) 
-           else loop (next t ctx) rlist ctx in
-           eval_fold2_slist fl_list sl1 sl2 res1 res2 t            
-       in
-         loop t slist ctx
-
-       let run_top_down_count a t =
-         let init = cons a.init Nil in
-         let _,res = top_down a (fun _ rb rb1 rb2 mark t res1 res2 ->
-                                   (vb rb)*( (vb mark) + (vb rb1)*res1 + (vb rb2)*res2))
-           0 t init t 1
-         in res.(0)
-       ;;
-
-       let run_top_down a t =
-         let init = cons a.init Nil in
-         let _,res = 
-           top_down a (fun null rb rb1 rb2 mark t res1 res2 ->
-                        if rb then
-                          TS.concat 
-                            (TS.concat (if mark then TS.Sing(t) else null)
-                               (if rb1 then res1 else null))
-                              (if rb2 then res2 else null)
-                        else null)
-             TS.Nil t init t 1
-         in res.(0)
-       ;;
-
-
-    end
-*)
     module type ResultSet = 
     sig
       type t
@@ -938,7 +479,6 @@ type 'a t = {
       let concat t1 t2 = { node = Concat(t1.node,t2.node); length = t1.length+t2.length }
       let append e t = { node = Concat(t.node,Cons(e,Nil)); length = t.length+1 } 
        
-       
       let fold f l acc = 
        let rec loop acc t = match t with
          | Nil -> acc
@@ -970,6 +510,8 @@ type 'a t = {
 
     module Run (RS : ResultSet) =
     struct
+      let fmt = Format.err_formatter
+      let pr x = Format.fprintf fmt x
       module Formlist = 
       struct
        type t = formlist
@@ -1010,6 +552,11 @@ type 'a t = {
          function Nil -> Nil 
            | Cons(s,h,ll) -> cons (f s) (loop ll) 
        in loop l
+      let iter_pl f l = 
+       let rec loop =
+         function Nil -> ()
+           | Cons(s,h,ll) ->  (f s);(loop ll) 
+       in loop l
 
       let rev_pl l = 
        let rec loop acc l = match l with 
@@ -1104,6 +651,7 @@ type 'a t = {
                                     if (TagSet.mem tag ts)
                                     then 
                                       let (child,desc,below),(sibl,foll,after) = f.st in
+                                      let h_acc = HASHINT3(h_acc,f.fid,HASHINT2(q,vb m)) in
                                         ((Formlist.cons q f h_acc m fl_acc,
                                           Ptset.union ll_acc below,
                                           Ptset.union rl_acc after,
@@ -1111,7 +659,7 @@ type 'a t = {
                                           Ptset.union desc d_acc,
                                           Ptset.union sibl s_acc,
                                           Ptset.union foll f_acc),
-                                         HASHINT3(h_acc,f.fid,HASHINT2(q,vb m)))
+                                         h_acc)                                 
                                   else acc ) (acc,0) (
                                  try Hashtbl.find a.phi q 
                                  with
@@ -1147,6 +695,13 @@ type 'a t = {
          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 _ = pr "Evaluation context : "; pr_st fmt (Ptset.elements s1);
+                 pr_st fmt (Ptset.elements s2);
+                 pr "Formlist (%i) : " (Formlist.hash fl);
+                 Formlist.pr fmt fl;
+                 pr "Results : "; pr_st fmt (Ptset.elements r');
+                 pr ", %b %b %b %b\n%!" rb rb1 rb2 mark
+               in *)
                let _ = res.(i) <- merge rb rb1 rb2 mark t res1.(i) res2.(i) 
                in                
                  fold ll1 ll2 fll (i+1) (cons r' aq)
@@ -1157,14 +712,25 @@ type 'a t = {
        in
        let null_result() = (pempty,Array.make slot_size RS.empty) in
        let rec loop t slist ctx = 
+         let (a,b) = 
          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 _ = pr "For tag %s,node %s, returning formulae list: \n%!"
+             (Tag.to_string tag) (Tree.dump_node t);
+             List.iter (fun f -> Formlist.pr fmt f;pr "\n%!") fl_list
+           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
+           let sl2,res2 = loop (next t ctx) rlist ctx in
              eval_fold2_slist fl_list sl1 sl2 res1 res2 t          
+         in 
+(*       let _ = pr "Inside topdown call: tree was %s, tag = %s" (Tree.dump_node t) (if Tree.is_nil t then "###" 
+                                                                                     else Tag.to_string (Tree.tag t));
+           iter_pl (fun s -> (pr_st fmt (Ptset.elements s))) a;
+           Array.iter (fun i -> pr "%i" (RS.length i)) b;
+           pr "\n%!"; in*) (a,b)
+           
        in
        let loop_no_right t slist ctx =
          if Tree.is_nil t then null_result()
@@ -1240,8 +806,7 @@ type 'a t = {
                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= 
@@ -1296,8 +861,10 @@ type 'a t = {
            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))
+                                             then
+                                               let h_acc = HASHINT3(h_acc,f.fid,HASHINT2(q,vb m)) in
+                                                 (Formlist.cons q f h_acc m fl_acc,
+                                                  h_acc)
                                              else (fl_acc,h_acc))
                              acc l)
              a.phi (Formlist.nil,0)
@@ -1306,37 +873,38 @@ type 'a t = {
          in
            (Hashtbl.add h_trans key res;res) 
                      
-
+             
+       let h_tdconf = Hashtbl.create 511 
        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
+(*                 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 _ =   
+(*         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));
+           (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 =         
+           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  *)
+(*           let _ = pr "Jumping to %s tag %s\n%!" (Tree.dump_node next) (Tag.to_string (Tree.tag 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 _ = if below_right then pr "Returning from jump to next = %s\n" (Tree.dump_node next)in   *)
          let sub =
            if dotd then
              if below_right then (* only recurse on the left subtree *)
-       (*      let _ = pr "Topdown on subtree\n%!" in     *)
+(*             let _ = pr "Topdown on left subtree\n%!" in      *)
                prepare_topdown a tree true
              else 
-(*             let _ = pr "Topdown on whole tree\n%!" in   *)
+(*             let _ = pr "Topdown on whole tree\n%!" in *)
                prepare_topdown a tree false
            else conf
          in
@@ -1344,10 +912,10 @@ type 'a t = {
            (Configuration.merge rightconf sub, next_of_next)
          in
            if Tree.equal tree root then 
-(*           let _ = pr "Stopping at root, configuration after topdown is:" ;
+(*             let _ = pr "Stopping at root, configuration after topdown is:" ;
                Configuration.pr fmt conf;
                pr "\n%!"               
-             in  *) accu,conf,next 
+             in *)  accu,conf,next 
            else              
          let parent = Tree.binary_parent tree in
          let ptag = Tree.tag parent in
@@ -1355,7 +923,7 @@ type 'a t = {
          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);
+(*       let _ = pr "Current conf is : %s " (Tree.dump_node tree); 
            Configuration.pr fmt conf;
            pr "\n" 
          in *)
@@ -1377,9 +945,25 @@ type 'a t = {
            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 tag = Tree.tag t in
+(*       pr "Going top down on tree with tag %s = %s "  
+           (if Tree.is_nil t then "###" else (Tag.to_string(Tree.tag t))) (Tree.dump_node t); *)
+         let r = 
+           try
+             Hashtbl.find h_tdconf tag
+           with
+             | Not_found -> 
+                 let res = Hashtbl.fold (fun q l acc -> 
+                                           if List.exists (fun (ts,_) -> TagSet.mem tag ts) l
+                                           then Ptset.add q acc
+                                           else acc) a.phi Ptset.empty
+                 in Hashtbl.add h_tdconf tag res;res
+         in 
+(*       let _ = pr ", among ";
+           pr_st fmt (Ptset.elements r);
+           pr "\n%!";
+         in *)
+         let r = cons r Nil in
          let set,res = top_down (~noright:noright) a t r t 1 in
          let set = match set with
            | Cons(x,_,Nil) ->x
@@ -1392,7 +976,7 @@ type 'a t = {
 
 
 
-       let run_bottom_up_contains a t =
+       let run_bottom_up a t k =
          let trlist = Hashtbl.find a.phi (Ptset.choose a.init)
          in
          let init = List.fold_left 
@@ -1400,12 +984,18 @@ type 'a t = {
               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 tree1,jump_fun =
+           match k with
+             | `TAG (tag) -> 
+                 (*Tree.tagged_lowest t tag, fun tree -> Tree.tagged_next tree tag*)
+                 (Tree.tagged_desc tag t, fun tree -> Tree.tagged_foll_below tag tree t)
+             | `CONTAINS(_) -> (Tree.text_below t,fun tree -> Tree.text_next tree t)
+             | _ -> assert false
+         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 _ = 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 
@@ -1423,21 +1013,10 @@ type 'a t = {
          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"
+    let bottom_up_count a t k = let module RI = Run(Integer) in Integer.length (RI.run_bottom_up a t k)
+