automaton.ml

   1 (******************************************************************************)
   2 (*  SXSI : XPath evaluator                                                    *)
   3 (*  Kim Nguyen (Kim.Nguyen@nicta.com.au)                                      *)
   4 (*  Copyright NICTA 2008                                                      *)
   5 (*  Distributed under the terms of the LGPL (see LICENCE)                     *)
   6 (******************************************************************************)
   7 INCLUDE "debug.ml";;
   8
   9 module State =
  10 struct
  11   type t = int
  12   let mk = let i = ref ~-1 in fun () -> incr i;!i
  13   let compare p q = p - q
  14   let equal p q = p==q
  15   let hash p = p
  16   let print fmt p = Format.fprintf fmt "<%.6i>" p
  17 end
  18
  19 module ISet : Set.S with type elt = int=
  20 struct
  21   let max = Sys.word_size - 2
  22   type t = int
  23   type elt = int
  24
  25   let empty = 0
  26   let full = -1
  27   let is_empty x = x == 0
  28   let mem e s = ((1 lsl e) land s) != 0
  29   let add e s = (1 lsl e) lor s
  30   let singleton e = (1 lsl e)
  31   let union = (lor)
  32   let inter = (land)
  33   let diff a b = a land (lnot b)
  34   let remove e s = (lnot (1 lsl e) land s)
  35   let compare = (-)
  36   let equal = (==)
  37   let subset a b = a land (lnot b) == 0
  38   let cardinal s =
  39     let rec loop n s =
  40       if s == 0 then n else loop (succ n) (s - (s land (-s)))
  41     in
  42   loop 0 s
  43 (* inverse of bit i = 1 lsl i i.e. tib i = log_2(i) *)
  44 let log2 = Array.create 255 0
  45 let () = for i = 0 to 7 do log2.(1 lsl i) <- i done
  46
  47 (* assumption: x is a power of 2 *)
  48 let tib32 x =
  49   if x land 0xFFFF == 0 then
  50     let x = x lsr 16 in
  51     if x land 0xFF == 0 then 24 + log2.(x lsr 8) else 16 + log2.(x)
  52   else
  53     if x land 0xFF == 0 then 8 + log2.(x lsr 8) else log2.(x)
  54
  55 let ffffffff = (0xffff lsl 16) lor 0xffff
  56 let tib64 x =
  57   if x land ffffffff == 0 then 32 + tib32 (x lsr 32) else tib32 x
  58
  59 let tib =
  60   match Sys.word_size with 32 -> tib32 | 64 -> tib64 | _ -> assert false
  61
  62 let min_elt s =
  63   if s == 0 then raise Not_found;
  64   tib (s land (-s))
  65
  66 let choose = min_elt
  67
  68 (* TODO: improve? *)
  69 let max_elt s =
  70   if s == 0 then raise Not_found;
  71   let rec loop i =
  72     if s land i != 0 then tib i
  73     else if i = 1 then raise Not_found else loop (i lsr 1)
  74   in
  75   loop min_int
  76
  77 let rec elements s =
  78   if s == 0 then [] else let i = s land (-s) in tib i :: elements (s - i)
  79
  80 let rec iter f s =
  81   if s != 0 then let i = s land (-s) in f (tib i); iter f (s - i)
  82
  83 let rec fold f s acc =
  84   if s == 0 then acc else let i = s land (-s) in fold f (s - i) (f (tib i) acc)
  85
  86 let rec for_all p s =
  87   s == 0 || let i = s land (-s) in p (tib i) && for_all p (s - i)
  88
  89 let rec exists p s =
  90   s != 0 && let i = s land (-s) in p (tib i) || exists p (s - i)
  91
  92 let rec filter p s =
  93   if s == 0 then
  94     0
  95   else
  96     let i = s land (-s) in
  97     let s = filter p (s - i) in
  98     if p (tib i) then s + i else s
  99
 100 let rec partition p s =
 101    if s == 0 then
 102     0, 0
 103   else
 104     let i = s land (-s) in
 105     let st,sf = partition p (s - i) in
 106     if p (tib i) then st + i, sf else st, sf + i
 107
 108 let split i s =
 109   let bi = 1 lsl i in
 110   s land (bi - 1), s land bi != 0, s land (-1 lsl (i+1))
 111
 112
 113 end
 114 (* module SSet = Set.Make(State)*)
 115 module SSet = ISet
 116
 117 module Transition =
 118 struct
 119
 120   type t = Label of State.t * TagSet.Xml.t * State.t * State.t
 121            | External of State.t * (Tree.Binary.t -> bool)*State.t * State.t
 122
 123   let source = function Label(s,_,_,_) | External(s,_,_,_) -> s
 124   let dest1 = function Label(_,_,d,_) | External(_,_,d,_) -> d
 125   let dest2 = function Label(_,_,_,d) | External(_,_,_,d) -> d
 126
 127   let compatible t1 t2 =
 128     State.equal (source t1) (source t2)
 129     && State.equal (dest1 t1) (dest1 t2)
 130     && State.equal (dest2 t1) (dest2 t2)
 131
 132   let check t1 t2 =
 133     if not (compatible t1 t2)
 134     then failwith "Incompatible transitions"
 135
 136   let cup t1 t2 =
 137     check t1 t2;
 138     match (t1,t2) with
 139       | Label(s,ts,d1,d2), Label(_,ts',_,_) -> Label(s,TagSet.Xml.cup ts ts',d1,d2)
 140       | External(s,f,d1,d2), External(_,f',_,_) -> External(s,(fun x -> (f x)||(f' x)),d1,d2)
 141       | Label(s,ts,d1,d2), External(_,f,_,_)
 142       | External(_,f,_,_), Label(s,ts,d1,d2) ->  External(s,(fun x -> (TagSet.Xml.mem (Tree.Binary.tag x) ts)||f x),d1,d2)
 143
 144   let cap t1 t2 =
 145     check t1 t2;
 146     match (t1,t2) with
 147       | Label(s,ts,d1,d2), Label(_,ts',_,_) -> Label(s,TagSet.Xml.cap ts ts',d1,d2)
 148       | External(s,f,d1,d2), External(_,f',_,_) -> External(s,(fun x -> (f x)&&(f' x)),d1,d2)
 149       | Label(s,ts,d1,d2), External(_,f,_,_)
 150       | External(_,f,_,_), Label(s,ts,d1,d2) -> External(s,(fun x -> (TagSet.Xml.mem (Tree.Binary.tag x) ts)&& f x),d1,d2)
 151
 152   let neg = function
 153     | Label(s,ts,d1,d2) -> Label(s,TagSet.Xml.neg ts,d1,d2)
 154     | External(s,f,d1,d2) -> External(s,(fun x -> not(f x)), d1 ,d2)
 155
 156
 157   let can_take t = function
 158     | Label(_,ts,_,_)  -> TagSet.Xml.mem (Tree.Binary.tag t) ts
 159     | External(_,f,_,_) -> f t
 160
 161   (* Hashtbl indexed by source State *)
 162   module HT = Hashtbl.Make(State)
 163
 164
 165
 166   type hashtbl = { label : (TagSet.Xml.t*State.t*State.t) HT.t;
 167                    extern : ((Tree.Binary.t-> bool)*State.t*State.t) HT.t;
 168                  }
 169
 170
 171   let empty () = { label = HT.create 17;
 172                    extern = HT.create 17;
 173                  }
 174
 175   let clear h = HT.clear h.label; HT.clear h.extern
 176
 177   let add h = function
 178     | Label(s,t,d1,d2) -> HT.add h.label s (t,d1,d2)
 179     | External(s,f,d1,d2) -> HT.add h.extern s (f,d1,d2)
 180
 181   let find_all ?(accu=[]) ?(pred_label=fun _ _ _ _ -> true) ?(pred_extern= fun _ _ _ _ -> true) h q =
 182     List.fold_left
 183       (fun acc (t,d1,d2) ->
 184          if pred_label q t d1 d2
 185          then Label(q,t,d1,d2) :: acc
 186          else acc)
 187      (List.fold_left
 188          (fun acc (f,d1,d2) ->
 189             if pred_extern q f d1 d2
 190             then External(q,f,d1,d2) :: acc
 191             else acc)
 192          accu
 193          (HT.find_all h.extern q))
 194       (HT.find_all h.label q)
 195
 196   let find_all_dest q h =
 197     HT.fold (fun source (t,q1,q2) acc ->
 198                if  (State.equal q1 q || State.equal q2 q)
 199                then Label(source,t,q1,q2)::acc
 200                else acc) h.label
 201       (HT.fold (fun source (t,q1,q2) acc ->
 202                   if (State.equal q1 q || State.equal q2 q)
 203                   then External(source,t,q1,q2)::acc
 204                   else acc) h.extern [])
 205
 206
 207   let fold_state f_lab f_ext h q acc =
 208     List.fold_left
 209       (fun acc (t,d1,d2) ->
 210          f_lab acc q t d1 d2)
 211       (List.fold_left
 212          (fun acc (f,d1,d2) ->
 213             f_ext acc q f d1 d2)
 214          acc
 215          (HT.find_all h.extern q))
 216       (HT.find_all h.label q)
 217
 218
 219 end
 220 module BST = Set.Make(Tree.Binary)
 221
 222 type t = { initial : SSet.t;
 223            final : SSet.t;
 224            transitions : Transition.hashtbl;
 225            marking : SSet.t;
 226            ignore : SSet.t;
 227            mutable result : BST.t;
 228            (* Statistics *)
 229            mutable numbt : int;
 230            mutable max_states : int;
 231            }
 232
 233 let mk () = { initial = SSet.empty;
 234              final = SSet.empty;
 235              transitions = Transition.empty();
 236              marking = SSet.empty;
 237              ignore = SSet.empty;
 238              result = BST.empty;
 239              numbt = 0;
 240              max_states = 0
 241            };;
 242
 243   let print_tags fmt l =
 244     let l =
 245       if TagSet.Xml.is_finite l then l
 246       else (Format.fprintf fmt "* \\ "; TagSet.Xml.neg l )
 247     in
 248       Format.fprintf fmt "{ ";
 249       ignore(TagSet.Xml.fold (fun t first ->
 250                                 if not first
 251                                 then Format.fprintf fmt " ,";
 252                                 Tag.print fmt t; false) l true);
 253       Format.fprintf fmt "}"
 254
 255   let dump fmt auto =
 256     Format.fprintf fmt "----------------- Automaton dump -------------------\n";
 257     Format.fprintf fmt "Initial states: ";
 258     SSet.iter (fun s -> State.print fmt s;
 259                             Format.fprintf fmt " ") auto.initial;
 260     Format.fprintf fmt "\n";
 261     Format.fprintf fmt "Final states:   ";
 262     SSet.iter (fun s -> State.print fmt s;
 263                             Format.fprintf fmt " ") auto.final;
 264     Format.fprintf fmt "\n";
 265     Format.fprintf fmt "Marking states: ";
 266     SSet.iter (fun s -> State.print fmt s;
 267                             Format.fprintf fmt " ") auto.marking;
 268     Format.fprintf fmt "\n";
 269     Format.fprintf fmt "Ignore states:  ";
 270     SSet.iter (fun s -> State.print fmt s;
 271                             Format.fprintf fmt " ") auto.ignore;
 272     Format.fprintf fmt "\n";
 273     Format.fprintf fmt "Transitions:\n";
 274     Transition.HT.iter (fun source (l,dest1,dest2) ->
 275                           State.print fmt source;
 276                           Format.fprintf fmt "-> ";
 277                           print_tags fmt l;
 278                           Format.fprintf fmt "(";
 279                           State.print fmt dest1;
 280                           Format.fprintf fmt " ,";
 281                           State.print fmt dest2;
 282                           Format.fprintf fmt ")\n") auto.transitions.Transition.label;
 283     Format.fprintf fmt "----------------------------------------------------\n"
 284
 285
 286
 287 module BottomUp =
 288 struct
 289
 290   exception Fail
 291
 292   let pr_states fmt st = SSet.iter (fun s -> State.print fmt s;
 293                                                  Format.fprintf fmt " ") st
 294
 295   let err = Format.err_formatter
 296   let filter_map_rev filt map l =
 297     let rec loop ((accuf,accum) as accu) = function
 298       | [] -> accu
 299       | t::r -> loop (if filt t  then (t::accuf,SSet.add (map t) accum)
 300                       else accu) r
 301     in
 302       loop ([],SSet.empty) l
 303
 304   let mem s x =  SSet.mem x s
 305
 306
 307   let rec accepting_among ?(strings=None)auto t r =
 308     if SSet.is_empty r then r else
 309       match strings with
 310         | Some valid_strings when (Tree.Binary.DocIdSet.for_all (fun i ->
 311                                                                    not (Tree.Binary.string_below t i)) valid_strings )
 312             -> SSet.empty
 313         | _ -> (
 314
 315     let to_ignore = SSet.inter auto.ignore r in
 316     let r = SSet.diff r to_ignore
 317     in
 318     let res =
 319       match Tree.Binary.descr t with
 320         | Tree.Binary.Nil -> SSet.inter r auto.final
 321         | Tree.Binary.String id -> (
 322             match strings with
 323               | None -> SSet.inter r auto.final
 324               | Some valid_strings when (Tree.Binary.DocIdSet.mem id valid_strings)
 325                   -> SSet.inter r auto.final
 326               | _ -> SSet.empty
 327           )
 328         | Tree.Binary.Node(_) ->
 329             let t1 = Tree.Binary.left t
 330             and t2 = Tree.Binary.right t
 331             in
 332             let transitions =
 333               SSet.fold
 334               ( fun q accu ->
 335                  Transition.fold_state
 336                    (fun acc q t d1 d2 -> Transition.Label(q,t,d1,d2) :: acc)
 337                    (fun acc q t d1 d2 -> Transition.External(q,t,d1,d2) :: acc)
 338                    auto.transitions q accu) r []
 339             in
 340             let transitions,r1 =
 341               filter_map_rev
 342                 (Transition.can_take t)
 343                 Transition.dest1 transitions
 344             in
 345             let s1 = accepting_among auto t1 r1
 346             in
 347             let transitions,r2 =
 348               filter_map_rev
 349                 (fun x->SSet.mem (Transition.dest1 x) s1)
 350                 Transition.dest2 transitions
 351             in
 352             let s2 = accepting_among auto t2 r2
 353             in
 354             let _,s = filter_map_rev
 355               (fun x -> SSet.mem (Transition.dest2 x) s2)
 356               (Transition.source) transitions
 357             in
 358               if SSet.is_empty s then s
 359               else
 360                 (if SSet.exists (mem auto.marking) s1 || SSet.exists (mem auto.marking) s2
 361                  then auto.result <- BST.add t auto.result;s)
 362     in SSet.union to_ignore res)
 363
 364
 365   let accept ?(strings=None) auto t =
 366     auto.result <- BST.empty;
 367     if SSet.is_empty (accepting_among ~strings:strings auto t auto.initial)
 368     then false
 369     else true
 370 end
 371
 372 module TopDown = struct
 373   let rec accept_at auto t q =
 374     if SSet.mem q auto.ignore then true
 375     else
 376       match Tree.Binary.descr t with
 377         | Tree.Binary.Nil | Tree.Binary.String _ -> SSet.mem q auto.final
 378         | Tree.Binary.Node(_) ->
 379             let tag = Tree.Binary.tag t
 380             and t1 = Tree.Binary.left t
 381             and t2 = Tree.Binary.right t
 382             in
 383             let transitions =
 384               Transition.find_all
 385                 ~pred_label:(fun _ ts _ _ -> TagSet.Xml.mem tag ts)
 386                 ~pred_extern:(fun _ f _ _ -> f t)
 387                 auto.transitions q
 388             in
 389             let rec iter_trans res = function
 390                 [] -> res
 391               | (Transition.Label(_,_,q1,q2) | Transition.External (_,_,q1,q2))::r ->
 392                   let _ = auto.numbt <- succ auto.numbt in
 393                   if (accept_at auto  t1 q1) && (accept_at auto t2 q2)
 394                   then
 395                     begin
 396                       if (SSet.mem q1 auto.marking)||(SSet.mem q2 auto.marking)
 397                       then
 398                         begin
 399                           auto.result <- BST.add t auto.result;
 400                         end;
 401                       iter_trans true r
 402                     end
 403                   else
 404                     iter_trans res r
 405             in iter_trans false transitions
 406
 407
 408
 409
 410   let accept auto t =
 411     auto.numbt <- -1;
 412     SSet.exists (fun q ->
 413                    P(auto.numbt <- succ auto.numbt);
 414                    auto.result <- BST.empty;
 415                    accept_at auto t q)  auto.initial
 416
 417
 418   let rec run_in auto t states =
 419     if SSet.is_empty states then ()
 420     else
 421     match Tree.Binary.descr t with
 422       | Tree.Binary.Nil | Tree.Binary.String _ -> ()
 423       | Tree.Binary.Node(_) ->
 424           let tag = Tree.Binary.tag t
 425           and t1 = Tree.Binary.left t
 426           and t2 = Tree.Binary.right t
 427           in
 428           P(let i = SSet.cardinal states in
 429               if i > auto.max_states then auto.max_states <- i);
 430           let s1,s2 =
 431             SSet.fold
 432               (fun q acc ->
 433                  if SSet.mem q auto.ignore then acc
 434                  else
 435                    Transition.fold_state
 436                      (fun (ss1,ss2) _ ts d1 d2 ->
 437                         if TagSet.Xml.mem tag ts
 438                         then
 439                           (SSet.add d1 ss1,
 440                            SSet.add d2 ss2)
 441                         else (ss1,ss2))
 442                      (fun (ss1,ss2) _ f d1 d2 ->
 443                         if f t
 444                         then
 445                           (SSet.add d1 ss1,
 446                            SSet.add d2 ss2)
 447                           else (ss1,ss2)) auto.transitions q acc ) states (SSet.empty,SSet.empty)
 448           in
 449             if SSet.is_empty (SSet.inter auto.marking (SSet.union s1 s2))
 450             then ()
 451             else auto.result <- BST.add t auto.result;
 452             run_in auto t1 s1;
 453             run_in auto t2 s2
 454
 455
 456   let run auto t =
 457     auto.result <- BST.empty;
 458     P(auto.numbt <- 0);
 459
 460       run_in auto t auto.initial
 461
 462 end
 463