ata.ml

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