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