ata.ml

   1 (* Todo refactor and remove this alias *)
   2 INCLUDE "debug.ml"
   3 module Tree = Tree.Binary
   4
   5
   6 let gen_id =
   7   let id = ref (-1) in
   8     fun () -> incr id;!id
   9
  10
  11 module State = struct
  12
  13   type t = int
  14   let mk = gen_id
  15
  16 end
  17 let mk_state = State.mk
  18
  19 type state = State.t
  20
  21 type predicate = [ `Left of (Tree.t -> bool) | `Right of (Tree.t -> bool) |
  22                        `True
  23                  ]
  24
  25 let eval_pred t =
  26   function `True -> true
  27     | `Left f | `Right f -> f t
  28
  29 type formula_expr =
  30   | False | True
  31   | Or of formula * formula
  32   | And of formula * formula
  33   | Atom of ([ `Left | `Right  | `LLeft | `RRight  ]*bool*state)
  34 and formula = { fid: int;
  35                 fkey : int;
  36                 pos : formula_expr;
  37                 neg : formula;
  38                 st : (Ptset.t*Ptset.t)*(Ptset.t*Ptset.t);
  39                 size: int;
  40               }
  41
  42 external hash_const_variant : [> ] -> int = "%identity"
  43 external int_bool : bool -> int = "%identity"
  44
  45 let hash_node_form t = match t with
  46   | False -> 0
  47   | True -> 1
  48   | And(f1,f2) -> (2+17*f1.fkey + 37*f2.fkey) land max_int
  49   | Or(f1,f2) -> (3+101*f1.fkey + 253*f2.fkey) land max_int
  50   | Atom(v,b,s) -> ((hash_const_variant v) + (3846*(int_bool b) +257) + (s lsl 13 - s)) land max_int
  51
  52
  53 module FormNode =
  54 struct
  55   type t = formula
  56
  57   let hash t = t.fkey
  58   let equal f1 f2 =
  59     if f1.fid == f2.fid || f1.fkey == f2.fkey || f1.pos == f2.pos then true
  60     else
  61     match f1.pos,f2.pos with
  62       | False,False | True,True -> true
  63       | Atom(d1,b1,s1), Atom(d2,b2,s2) when (b1==b2) &&  (s1==s2) && (d1 = d2) -> true
  64       | Or(g1,g2),Or(h1,h2)
  65       | And(g1,g2),And(h1,h2)  -> g1.fid == h1.fid && g2.fid == h2.fid
  66       | _ -> false
  67
  68 end
  69 module WH = Weak.Make(FormNode)
  70
  71 let f_pool = WH.create 107
  72
  73 let empty_pair = Ptset.empty,Ptset.empty
  74 let empty_quad = empty_pair,empty_pair
  75
  76 let true_,false_ =
  77   let rec t = { fid = 1; pos = True; fkey=1; neg = f ; st = empty_quad; size =1; }
  78   and f = { fid = 0; pos = False; fkey=0; neg = t; st = empty_quad; size = 1; }
  79   in
  80     WH.add f_pool f;
  81     WH.add f_pool t;
  82     t,f
  83
  84 let is_true f = f.fid == 1
  85 let is_false f = f.fid == 0
  86
  87
  88 let cons pos neg s1 s2 size1 size2 =
  89   let rec pnode =
  90     { fid = gen_id ();
  91       fkey = hash_node_form pos;
  92       pos = pos;
  93       neg = nnode;
  94       st = s1;
  95       size = size1;}
  96   and nnode = {
  97     fid = gen_id ();
  98     pos = neg;
  99     fkey = hash_node_form neg;
 100     neg = pnode;
 101     st = s2;
 102     size = size2;
 103   }
 104   in
 105     (WH.merge f_pool pnode),(WH.merge f_pool nnode)
 106
 107 let atom_  d p s =
 108   let si = Ptset.singleton s in
 109   let ss = match d with
 110     | `Left -> (si,Ptset.empty),empty_pair
 111     | `Right -> empty_pair,(si,Ptset.empty)
 112     | `LLeft -> (Ptset.empty,si),empty_pair
 113     | `RRight -> empty_pair,(Ptset.empty,si)
 114   in fst (cons (Atom(d,p,s)) (Atom(d,not p,s)) ss ss 1 1)
 115
 116 let union_quad  ((l1,ll1),(r1,rr1))  ((l2,ll2),(r2,rr2)) =
 117   (Ptset.union l1 l2 ,Ptset.union ll1 ll2),
 118   (Ptset.union r1 r2 ,Ptset.union rr1 rr2)
 119
 120 let merge_states f1 f2 =
 121   let sp =
 122     union_quad f1.st f2.st
 123   and sn =
 124     union_quad f1.neg.st f2.neg.st
 125   in
 126     sp,sn
 127
 128 let full_or_ f1 f2 =
 129   let f1,f2 = if f1.fid < f2.fid then f2,f1 else f1,f2 in
 130   let sp,sn = merge_states f1 f2 in
 131   let psize = f1.size + f2.size in
 132   let nsize = f1.neg.size + f2.neg.size in
 133     fst (cons (Or(f1,f2)) (And(f1.neg,f2.neg)) sp sn psize nsize )
 134
 135 let or_ f1 f2 =
 136   let f1,f2 = if f1.fid < f2.fid then f2,f1 else f1,f2 in
 137   if is_true f1 || is_true f2 then true_
 138   else if is_false f1 && is_false f2 then false_
 139   else if is_false f1 then f2
 140   else if is_false f2 then f1
 141   else
 142     let psize = f1.size + f2.size in
 143     let nsize = f1.neg.size + f2.neg.size in
 144     let sp,sn = merge_states f1 f2 in
 145       fst (cons (Or(f1,f2)) (And(f1.neg,f2.neg)) sp sn psize nsize)
 146
 147
 148
 149 let and_ f1 f2 =
 150   let f1,f2 = if f1.fid < f2.fid then f2,f1 else f1,f2 in
 151   if is_true f1 && is_true f2 then true_
 152   else if is_false f1 || is_false f2 then false_
 153   else if is_true f1 then f2
 154   else if is_true f2 then f1
 155   else
 156     let psize = f1.size + f2.size in
 157     let nsize = f1.neg.size + f2.neg.size in
 158     let sp,sn = merge_states f1 f2 in
 159       fst (cons (And(f1,f2)) (Or(f1.neg,f2.neg)) sp sn psize nsize)
 160
 161
 162 let not_ f = f.neg
 163
 164
 165 module HTagSetKey =
 166 struct
 167   type t = Ptset.t*Tag.t
 168   let int_hash key = key lsl 31 lor (key lsl 8)
 169   let equal (s1,s2) (t1,t2) =  (s2 == t2) &&  Ptset.equal s1 t1
 170   let hash (s,t) = int_hash (Ptset.hash s) lxor ( int_hash (Tag.hash t))
 171 end
 172 module HTagSet = Hashtbl.Make(HTagSetKey)
 173
 174 type t = {
 175     id : int;
 176     mutable states : Ptset.t;
 177     init : Ptset.t;
 178     mutable final : Ptset.t;
 179     universal : Ptset.t;
 180     (* Transitions of the Alternating automaton *)
 181     phi : (state,(TagSet.t*(bool*formula*predicate)) list) Hashtbl.t;
 182     delta : (state*Tag.t, (bool*formula*predicate)) Hashtbl.t;
 183 (*    delta : (state,(bool*formula*predicate) TagMap.t) Hashtbl.t; *)
 184     sigma : (bool*formula*(predicate list*predicate list)*bool) HTagSet.t;
 185   }
 186
 187   module Pair (X : Set.OrderedType) (Y : Set.OrderedType) =
 188   struct
 189     type t = X.t*Y.t
 190     let compare (x1,y1) (x2,y2) =
 191       let r = X.compare x1 x2 in
 192         if r == 0 then Y.compare y1 y2
 193         else r
 194   end
 195
 196   module PL = Set.Make (Pair (Ptset) (Ptset))
 197
 198
 199       let pr_st ppf l = Format.fprintf ppf "{";
 200     begin
 201       match l with
 202         |       [] -> ()
 203         | [s] -> Format.fprintf ppf " %i" s
 204         | p::r -> Format.fprintf ppf " %i" p;
 205             List.iter (fun i -> Format.fprintf ppf "; %i" i) r
 206     end;
 207     Format.fprintf ppf " }"
 208   let rec pr_frm ppf f = match f.pos with
 209     | True -> Format.fprintf ppf "⊤"
 210     | False -> Format.fprintf ppf "⊥"
 211     | And(f1,f2) ->
 212         Format.fprintf ppf "(";
 213         (pr_frm ppf f1);
 214         Format.fprintf ppf ") ∧ (";
 215         (pr_frm ppf f2);
 216         Format.fprintf ppf ")"
 217     | Or(f1,f2) ->
 218         (pr_frm ppf f1);
 219         Format.fprintf ppf " ∨ ";
 220         (pr_frm ppf f2);
 221     | Atom(dir,b,s) -> Format.fprintf ppf "%s%s[%i]"
 222         (if b then "" else "¬")
 223         (match  dir with
 224            | `Left ->  "↓₁"
 225            | `Right -> "↓₂"
 226            | `LLeft ->  "⇓₁"
 227            | `RRight -> "⇓₂") s
 228
 229   let dnf_hash = Hashtbl.create 17
 230
 231   let rec dnf_aux f = match f.pos with
 232     | False -> PL.empty
 233     | True -> PL.singleton (Ptset.empty,Ptset.empty)
 234     | Atom((`Left|`LLeft),_,s) -> PL.singleton (Ptset.singleton s,Ptset.empty)
 235     | Atom((`Right|`RRight),_,s) -> PL.singleton (Ptset.empty,Ptset.singleton s)
 236     | Or(f1,f2) -> PL.union (dnf f1) (dnf f2)
 237     | And(f1,f2) ->
 238           let pl1 = dnf f1
 239           and pl2 = dnf f2
 240           in
 241             PL.fold (fun (s1,s2) acc ->
 242                        PL.fold ( fun (s1', s2') acc' ->
 243                                    (PL.add
 244                                       ((Ptset.union s1 s1'),
 245                                        (Ptset.union s2 s2')) acc') )
 246                           pl2 acc )
 247               pl1 PL.empty
 248
 249
 250   and dnf f =
 251     try
 252       Hashtbl.find dnf_hash f.fid
 253     with
 254         Not_found ->
 255           let d = dnf_aux f in
 256             Hashtbl.add dnf_hash f.fid d;d
 257
 258
 259   let can_top_down f =
 260     let nf = dnf f in
 261       if (PL.cardinal nf > 3)then None
 262       else match PL.elements nf with
 263         | [(s1,s2); (t1,t2); (u1,u2)] when
 264             Ptset.is_empty s1 && Ptset.is_empty s2 && Ptset.is_empty t1 && Ptset.is_empty u2
 265               -> Some(true,t2,u1)
 266         | [(t1,t2); (u1,u2)] when Ptset.is_empty t1 && Ptset.is_empty u2
 267             -> Some(false,t2,u1)
 268         | _ -> None
 269
 270
 271   let equal_form f1 f2 =
 272     (f1.fid == f2.fid) || (FormNode.equal f1 f2) || (PL.equal (dnf f1) (dnf f2))
 273
 274   let dump ppf a =
 275     Format.fprintf ppf "Automaton (%i) :\n" a.id;
 276     Format.fprintf ppf "States : "; pr_st ppf (Ptset.elements a.states);
 277     Format.fprintf ppf "\nInitial states : "; pr_st ppf (Ptset.elements a.init);
 278     Format.fprintf ppf "\nFinal states : "; pr_st ppf (Ptset.elements a.final);
 279     Format.fprintf ppf "\nUniversal states : "; pr_st ppf (Ptset.elements a.universal);
 280     Format.fprintf ppf "\nAlternating transitions :\n------------------------------\n";
 281     let l = Hashtbl.fold (fun k t acc ->
 282                             (List.map (fun (t,(m,f,p)) -> (t,k),(m,f,p)) t)@ acc) a.phi [] in
 283     let l = List.sort (fun ((tsx,x),_) ((tsy,y),_) -> if x-y == 0 then TagSet.compare tsx tsy else x-y) l in
 284     List.iter (fun ((ts,q),(b,f,_)) ->
 285
 286                     let s =
 287                       if TagSet.is_finite ts
 288                       then "{" ^ (TagSet.fold (fun t a -> a ^ " '" ^ (Tag.to_string t)^"'") ts "") ^" }"
 289                       else let cts = TagSet.neg ts in
 290                         if TagSet.is_empty cts then "*" else
 291                           (TagSet.fold (fun t a -> a ^ " " ^ (Tag.to_string t)) cts "*\\{"
 292                           )^ "}"
 293                     in
 294                       Format.fprintf ppf "(%s,%i) %s " s q (if b then "=>" else "->");
 295                       pr_frm ppf f;
 296                       Format.fprintf ppf "\n")l;
 297
 298     Format.fprintf ppf "NFA transitions :\n------------------------------\n";
 299     HTagSet.iter (fun (qs,t) (b,f,_,_) ->
 300                     pr_st ppf (Ptset.elements qs);
 301                     Format.fprintf ppf ",%s  %s " (Tag.to_string t) (if b then "=>" else "->");
 302                     pr_frm ppf f;
 303                     Format.fprintf ppf "(fid=%i) left=" f.fid;
 304                     let (l,ll),(r,rr) = f.st in
 305                       pr_st ppf (Ptset.elements l);
 306                       Format.fprintf ppf ", ";
 307                       pr_st ppf (Ptset.elements ll);
 308                       Format.fprintf ppf ", right=";
 309                       pr_st ppf (Ptset.elements r);
 310                       Format.fprintf ppf ", ";
 311                       pr_st ppf (Ptset.elements rr);
 312                       Format.fprintf ppf "\n";
 313                  ) a.sigma;
 314     Format.fprintf ppf "=======================================\n"
 315
 316   module Transitions = struct
 317     type t = state*TagSet.t*bool*formula*predicate
 318     let ( ?< ) x = x
 319     let ( >< ) state (l,b) = state,(l,b,`True)
 320     let ( ><@ ) state (l,b,p) = state,(l,b,p)
 321     let ( >=> ) (state,(label,mark,pred)) form = (state,label,mark,form,pred)
 322     let ( +| ) f1 f2 = or_ f1 f2
 323     let ( *& ) f1 f2 = and_ f1 f2
 324     let ( ** ) d s = atom_ d true s
 325
 326
 327   end
 328   type transition = Transitions.t
 329
 330   let equal_trans (q1,t1,m1,f1,_) (q2,t2,m2,f2,_) =
 331     (q1 == q2) && (TagSet.equal t1 t2) && (m1 == m2) && (equal_form f1 f2)
 332
 333   module TS =
 334   struct
 335     type node = Nil | Cons of Tree.t * node | Concat of node*node
 336     and t = { node : node; size : int }
 337     let node n s = { node=n; size = s }
 338
 339     let empty = node Nil 0
 340
 341     let cons e t = node (Cons(e,t.node)) (t.size+1)
 342     let concat t1 t2 = node (Concat (t1.node,t2.node)) (t1.size+t2.size)
 343     let append = cons
 344 (*    let append e t = node (Concat(t.node,Cons(e,Nil))) (t.size+1) *)
 345
 346     let to_list_rev t =
 347       let rec aux acc l rest =
 348         match l with
 349           | Nil -> begin
 350               match rest with
 351                 | Nil -> acc
 352                 | Cons(e,t) -> aux (e::acc) t Nil
 353                 | Concat(t1,t2) -> aux acc t1 t2
 354             end
 355           | Cons(e,r) -> aux (e::acc) r rest
 356           | Concat(t1,t2) -> aux acc t1 (Concat(t2,rest))
 357       in
 358     aux [] t.node Nil
 359
 360     let length = function { size = s } -> s
 361
 362     let iter f { node = n } =
 363       let rec loop = function
 364         | Nil -> ()
 365         | Cons(e,n) -> let _ = f e in loop n
 366         | Concat(n1,n2) -> let _ = loop n1 in loop n2
 367       in loop n
 368
 369     let rev_iter f { node = n } =
 370       let rec loop = function
 371         | Nil -> ()
 372         | Cons(e,n) -> let _ = loop n in f e
 373         | Concat(n1,n2) -> let _ = loop n2 in loop n1
 374       in loop n
 375
 376
 377     let find f { node = n } =
 378       let rec loop = function
 379         | Nil -> raise Not_found
 380         | Cons(e,n) -> if f e then e else loop n
 381         | Concat(n1,n2) -> try
 382             loop n1
 383           with
 384             | Not_found -> loop n2
 385       in
 386         loop n
 387
 388   end
 389 (*
 390   module BottomUpJumpNew = struct
 391
 392 *)
 393     module HFEval = Hashtbl.Make(
 394       struct
 395         type t = int*Ptset.t*Ptset.t
 396         let equal (a,b,c) (d,e,f) =
 397           a==d && (Ptset.equal b e) && (Ptset.equal c f)
 398         let hash (a,b,c) =
 399           a+17*(Ptset.hash b) + 31*(Ptset.hash c)
 400       end)
 401
 402     let hfeval = HFEval.create 4097
 403
 404
 405     let eval_form_bool f s1 s2 =
 406       let rec eval f = match f.pos with
 407         | Atom((`Left|`LLeft),b,q) -> if b == (Ptset.mem q s1) then (true,true,false) else false,false,false
 408         | Atom((`Right|`RRight),b,q) -> if b == (Ptset.mem q s2) then (true,false,true) else false,false,false
 409             (* test some inlining *)
 410         | True -> true,true,true
 411         | False -> false,false,false
 412         | _ ->
 413             try
 414                HFEval.find hfeval (f.fid,s1,s2)
 415             with
 416               | Not_found -> let r =
 417                   match f.pos with
 418                     | Or(f1,f2) ->
 419                         let b1,rl1,rr1 = eval f1
 420                         in
 421                           if b1 && rl1 && rr1 then (true,true,true)
 422                           else
 423                             let b2,rl2,rr2 = eval f2
 424                             in
 425                             let rl1,rr1 = if b1 then rl1,rr1 else false,false
 426                             and rl2,rr2 = if b2 then rl2,rr2 else false,false
 427                             in (b1 || b2, rl1||rl2,rr1||rr2)
 428                     | And(f1,f2) ->
 429                         let b1,rl1,rr1 = eval f1 in
 430                           if b1 && rl1 && rr1 then (true,true,true)
 431                           else if b1
 432                           then let b2,rl2,rr2 = eval f2 in
 433                             if b2 then (true,rl1||rl2,rr1||rr2)
 434                             else (false,false,false)
 435                           else (false,false,false)
 436                     | _ -> assert false
 437                 in
 438                   HFEval.add hfeval (f.fid,s1,s2) r;
 439                   r
 440       in eval f
 441
 442
 443     let fstate_pool = Hashtbl.create 11
 444
 445     let merge_pred a b = match a,b with
 446       | Some(f1), Some(f2) -> Some(fun x -> f1 x || f2 x)
 447       | None,None -> None
 448       | None,Some(_) -> b
 449       | Some(_),None -> a
 450
 451     let acc_pred p l1 l2 = match p with
 452       | `Left _ -> p::l1,l2
 453       | `Right _ -> l1,p::l2
 454       | _ -> l1,l2
 455
 456
 457     let merge_trans t a tag q acc =
 458       List.fold_left (fun (accf,accm,acchtrue) (ts,(m,f,pred)) ->
 459                         if TagSet.mem tag ts
 460                         then
 461                           let tmpf,hastrue =
 462                             if is_true f then
 463                               let newfinal =
 464                                 try Hashtbl.find fstate_pool f.fid with
 465                                   | Not_found -> let s = mk_state() in
 466                                       a.states <- Ptset.add s a.states;
 467                                       a.final <- Ptset.add s a.final;
 468                                       Hashtbl.add fstate_pool f.fid s;s
 469                               in
 470                                 (atom_ `Left true newfinal),true
 471                             else f,false in
 472                             (or_ tmpf accf,accm||m,acchtrue||hastrue)
 473                         else (accf,accm,acchtrue)
 474                      ) acc (try Hashtbl.find a.phi q with Not_found -> [])
 475
 476     let get_trans t a tag r =
 477       try
 478         let mark,f,predl,has_true =
 479           HTagSet.find a.sigma (r,tag)
 480         in f.st,f,mark,has_true,r
 481       with
 482           Not_found ->
 483             let f,mark,has_true,accq =
 484               Ptset.fold (fun q (accf,accm,acchtrue,accq) ->
 485                             let naccf,naccm,nacctrue =
 486                               merge_trans t a tag q (accf,accm,acchtrue )
 487                             in
 488                               if is_false naccf then (naccf,naccm,nacctrue,accq)
 489                               else (naccf,naccm,nacctrue,Ptset.add q accq)
 490                          )
 491                 r (false_,false,false,Ptset.empty)
 492             in
 493               HTagSet.add a.sigma (accq,tag) (mark,f,([],[]),has_true);
 494               f.st,f,mark,has_true,accq
 495
 496     let h_union = Hashtbl.create 4097
 497
 498     let pt_cup s1 s2 =
 499       let h = (Ptset.hash s1,Ptset.hash s2) in
 500       try
 501         Hashtbl.find h_union h
 502       with
 503         | Not_found -> let s = Ptset.union s1 s2
 504           in
 505             Hashtbl.add h_union h s;s
 506
 507
 508
 509     let tags_of_state a q = Hashtbl.fold
 510       (fun p l acc ->
 511          if p == q then
 512            List.fold_left
 513              (fun acc (ts,_) ->
 514                 pt_cup (TagSet.positive ts) acc) acc l
 515          else acc) a.phi Ptset.empty
 516
 517     let h_tags_states = Hashtbl.create 4096
 518
 519
 520
 521
 522     let tags a qs =
 523       try
 524         Hashtbl.find h_tags_states (Ptset.hash qs)
 525       with
 526         | Not_found ->
 527             let l = Ptset.fold (fun q acc -> pt_cup acc (tags_of_state a q)) qs Ptset.empty
 528             in
 529                 Hashtbl.add h_tags_states (Ptset.hash qs) l;l
 530
 531     let time cpt acc f x =
 532       let t1 = Unix.gettimeofday () in
 533       let r = f x in
 534       let t2 = Unix.gettimeofday () in
 535       let t = (1000. *.(t2 -. t1)) in
 536         acc:=!acc+.t;
 537         incr cpt;
 538         r
 539
 540
 541     let h_time = Hashtbl.create 4096
 542     let calls = ref 0
 543
 544     let rtime s f x =
 545
 546       let cpt,atime =
 547         try
 548           Hashtbl.find h_time s
 549         with
 550           | _ -> (ref 0, ref 0.)
 551       in
 552       let r = time cpt atime f x
 553       in
 554         Hashtbl.replace h_time s (cpt,atime);
 555         r
 556
 557     let rec accepting_among_time a t r ctx =
 558       incr calls;
 559       let orig = r in
 560       let rest = Ptset.inter r a.final in
 561       let r = Ptset.diff r rest in
 562         if Ptset.is_empty r then rest,TS.empty else
 563           if Tree.is_node t
 564           then
 565             let among,result,form =
 566               let ((ls,lls),(rs,rrs)),formula,mark,has_true,r' =
 567                 let tag = rtime "Tree.tag" Tree.tag t in
 568                 rtime "get_trans" (get_trans t a tag) r
 569               in
 570               let tl = rtime "tags" (tags a) ls
 571               and tr = rtime "tags" (tags a) rs
 572               and tll = rtime "tags" (tags a) lls
 573               and trr = rtime "tags" (tags a) rrs
 574               in
 575               let first =
 576                 if Ptset.mem Tag.pcdata (pt_cup tl tll)
 577                 then
 578                    rtime "Tree.text_below" (Tree.text_below) t
 579                 else
 580                   let etl = Ptset.is_empty tl
 581                   and etll = Ptset.is_empty tll
 582                   in
 583                     if etl && etll
 584                     then Tree.mk_nil t
 585                     else
 586                       if etl then  rtime "Tree.tagged_desc_only" (Tree.tagged_desc_only t) tll
 587                       else if etll then  rtime "Tree.first_child" (Tree.first_child) t
 588                       else (* add child only *)
 589                         rtime  "Tree.tagged_below" (Tree.tagged_below t tl) tll
 590               and next =
 591                 if Ptset.mem Tag.pcdata (pt_cup tr trr)
 592                 then
 593                   rtime "Tree.text_next" (Tree.text_next t) ctx
 594                 else
 595                   let etr = Ptset.is_empty tr
 596                   and etrr = Ptset.is_empty trr
 597                   in
 598                     if etr && etrr
 599                     then Tree.mk_nil t
 600                     else
 601                       if etr then rtime "Tree.tagged_foll_only" (Tree.tagged_foll_only t trr) ctx
 602                       else if etrr then rtime "Tree.next_sibling" (Tree.next_sibling) t
 603                       else (* add ns only *)
 604                         rtime "Tree.tagged_next" (Tree.tagged_next t tr trr) ctx
 605
 606               in
 607               let s1,res1 = accepting_among_time a first (pt_cup ls lls) t
 608               and s2,res2 =  accepting_among_time a next (pt_cup rs rrs) ctx
 609               in
 610               let rb,rb1,rb2 = rtime "eval_form_bool" (eval_form_bool formula s1) s2 in
 611                 if rb
 612                 then
 613                   let res1 = if rb1 then res1 else TS.empty
 614                   and res2 = if rb2 then res2 else TS.empty
 615                   in r', rtime "TS.concat" (TS.concat res2) (if mark then rtime "TS.append" (TS.append t) res1 else res1),formula
 616                 else Ptset.empty,TS.empty,formula
 617
 618             in
 619
 620                 among,result
 621
 622           else orig,TS.empty
 623
 624
 625     let run_time a t =
 626       let st,res = accepting_among_time a t a.init t in
 627       let _ = Printf.eprintf "\n Timings\n";
 628         let total_time = Hashtbl.fold (fun fname ({ contents=cpt }, {contents=atime}) (total_time) ->
 629                                          Printf.eprintf "%s\t %i calls, %f ms accumulated time, %f ms mean time\n"
 630                                            fname cpt atime (atime /. (float_of_int cpt));
 631                                          total_time +. atime ) h_time 0.
 632         in
 633           Printf.eprintf "total calls %i, total monitored time %f ms\n%!" !calls total_time
 634       in
 635       if Ptset.is_empty (st) then TS.empty else res
 636
 637
 638
 639     let rec accepting_among a t r ctx =
 640       let orig = r in
 641       let rest = Ptset.inter r a.final in
 642       let r = Ptset.diff r rest in
 643         if Ptset.is_empty r then rest,TS.empty else
 644           if Tree.is_node t
 645           then
 646             let among,result,form =
 647               let ((ls,lls),(rs,rrs)),formula,mark,has_true,r' =
 648                 let tag =  Tree.tag t in
 649                   get_trans t a tag r
 650               in
 651               let tl = tags a ls
 652               and tr = tags a rs
 653               and tll = tags a lls
 654               and trr = tags a rrs
 655               in
 656               let first =
 657                 if Ptset.mem Tag.pcdata (pt_cup tl tll)
 658                 then
 659                    Tree.text_below t
 660                 else
 661                   let etl = Ptset.is_empty tl
 662                   and etll = Ptset.is_empty tll
 663                   in
 664                     if etl && etll
 665                     then Tree.mk_nil t
 666                     else
 667                       if etl then Tree.tagged_desc_only t tll
 668                       else if etll then  Tree.first_child t
 669                       else (* add child only *)
 670                         Tree.tagged_below t tl tll
 671               and next =
 672                 if Ptset.mem Tag.pcdata (pt_cup tr trr)
 673                 then
 674                   Tree.text_next t ctx
 675                 else
 676                   let etr = Ptset.is_empty tr
 677                   and etrr = Ptset.is_empty trr
 678                   in
 679                     if etr && etrr
 680                     then Tree.mk_nil t
 681                     else
 682                       if etr then Tree.tagged_foll_only t trr ctx
 683                       else if etrr then Tree.next_sibling t
 684                       else (* add ns only *)
 685                         Tree.tagged_next t tr trr ctx
 686
 687               in
 688               let s1,res1 = accepting_among a first (pt_cup ls lls) t
 689               and s2,res2 =  accepting_among a next (pt_cup rs rrs) ctx
 690               in
 691               let rb,rb1,rb2 = eval_form_bool formula s1 s2 in
 692                 if rb
 693                 then
 694                   let res1 = if rb1 then res1 else TS.empty
 695                   and res2 = if rb2 then res2 else TS.empty
 696                   in r', TS.concat res2 (if mark then TS.append t res1 else res1),formula
 697                 else Ptset.empty,TS.empty,formula
 698
 699             in
 700                 among,result
 701
 702           else orig,TS.empty
 703
 704
 705     let run a t =
 706       let st,res = accepting_among a t a.init t in
 707         if Ptset.is_empty (st) then TS.empty else res
 708
 709     let rec accepting_among_count a t r ctx =
 710       let orig = r in
 711       let rest = Ptset.inter r a.final in
 712       let r = Ptset.diff r rest in
 713         if Ptset.is_empty r then rest,0 else
 714           if Tree.is_node t
 715           then
 716             let ((ls,lls),(rs,rrs)),formula,mark,has_true,r' =
 717               let tag =  Tree.tag t in
 718                 get_trans t a tag r
 719             in
 720             let tl = tags a ls
 721             and tr = tags a rs
 722             and tll = tags a lls
 723             and trr = tags a rrs
 724             in
 725             let first =
 726               if Ptset.mem Tag.pcdata (pt_cup tl tll)
 727               then
 728                 Tree.text_below t
 729               else
 730                 let etl = Ptset.is_empty tl
 731                 and etll = Ptset.is_empty tll
 732                 in
 733                   if etl && etll
 734                   then Tree.mk_nil t
 735                   else
 736                     if etl then Tree.tagged_desc_only t tll
 737                     else if etll then  Tree.first_child t
 738                     else (* add child only *)
 739                       Tree.tagged_below t tl tll
 740             and next =
 741               if Ptset.mem Tag.pcdata (pt_cup tr trr)
 742               then
 743                 Tree.text_next t ctx
 744               else
 745                 let etr = Ptset.is_empty tr
 746                 and etrr = Ptset.is_empty trr
 747                 in
 748                     if etr && etrr
 749                     then Tree.mk_nil t
 750                     else
 751                       if etr then Tree.tagged_foll_only t trr ctx
 752                       else if etrr then Tree.next_sibling t
 753                       else (* add ns only *)
 754                         Tree.tagged_next t tr trr ctx
 755
 756             in
 757             let s1,res1 = accepting_among_count a first (pt_cup ls lls) t
 758             and s2,res2 =  accepting_among_count a next (pt_cup rs rrs) ctx
 759             in
 760             let rb,rb1,rb2 = eval_form_bool formula s1 s2 in
 761                 if rb
 762                 then
 763                   let res1 = if rb1 then res1 else 0
 764                   and res2 = if rb2 then res2 else 0
 765                   in r', res2 + (if mark then  1 + res1 else res1)
 766                 else Ptset.empty,0
 767
 768
 769
 770           else orig,0
 771
 772
 773     let run_count a t =
 774       let st,res = accepting_among_count a t a.init t in
 775         if Ptset.is_empty (st) then 0 else res
 776
 777
 778
 779
 780
 781 (*
 782   end
 783 *)