src/runtime.ml

   1 INCLUDE "debug.ml"
   2 INCLUDE "log.ml"
   3 INCLUDE "utils.ml"
   4
   5 open Format
   6 open Ata
   7 module type S = sig
   8   type result_set
   9   val top_down_run : Ata.t -> Tree.t -> Tree.node -> result_set
  10   val bottom_up_run : Ata.t -> Tree.t -> Compile.text_query * string -> result_set
  11   val naive_top_down_run : Ata.t -> Tree.t -> Tree.node -> result_set
  12   val twopass_top_down_run : Ata.t -> Tree.t -> Tree.node -> result_set
  13 end
  14
  15 module Make (U : ResJIT.S) : S with type result_set = U.NS.t =
  16   struct
  17
  18     type result_set = U.NS.t;;
  19
  20     let eval_form auto s1 s2 f =
  21       let rec loop f =
  22         match Formula.expr f with
  23           | Formula.False | Formula.True | Formula.Pred _ -> f, []
  24           | Formula.Atom(`Left, b, q) ->
  25               Formula.of_bool (b == (StateSet.mem q s1)),
  26               if b && StateSet.mem q auto.topdown_marking_states then [ResJIT.LEFT q] else []
  27           | Formula.Atom (`Right, b, q) ->
  28               Formula.of_bool(b == (StateSet.mem q s2)),
  29               if b && StateSet.mem q auto.topdown_marking_states then [ResJIT.RIGHT q] else []
  30           | Formula.Atom (`Epsilon, _, _) -> assert false
  31
  32           | Formula.Or(f1, f2) ->
  33               let b1, i1 = loop f1 in
  34               let b2, i2 = loop f2 in
  35               Formula.or_pred b1 b2, i1 @ i2
  36           | Formula.And(f1, f2) ->
  37               let b1, i1 = loop f1 in
  38               let b2, i2 = loop f2 in
  39               Formula.and_pred b1 b2, i1 @ i2
  40       in
  41       loop f
  42
  43
  44     let eval_trans auto s1 s2 trans =
  45       LOG(__ "top-down-run" 3 "Evaluating transition list:@\n%a" Translist.print trans);
  46       Translist.fold
  47         (fun t ((a_st, a_op, a_todo) as acc)->
  48            let q, _, m, f = Transition.node t in
  49            let form, ops = eval_form auto s1 s2 f in
  50            match Formula.expr form with
  51              | Formula.True ->
  52                StateSet.add q a_st,
  53                (q, (if m then (ResJIT.SELF() :: ops) else ops)):: a_op,
  54                a_todo
  55              | Formula.False -> acc
  56              | Formula.Pred p -> a_st, a_op,
  57                (p.Tree.Predicate.node, q, [(q,(if m then (ResJIT.SELF() :: ops) else ops))]) :: a_todo
  58              | _ -> assert false
  59         ) trans (StateSet.empty, [], [])
  60
  61
  62
  63     module L3JIT =
  64       struct
  65
  66         type opcode = (t -> t -> t -> Tree.t -> Tree.node -> StateSet.t * t)
  67
  68         type t = opcode Cache.Lvl3.t
  69
  70         let dummy _ _ _ _ _ = failwith "Uninitialized L3JIT"
  71
  72
  73         let show_stats a =
  74           let count = ref 0 in
  75           Cache.Lvl3.iteri (fun _ _ _ _ b -> if not b then incr count) a;
  76           Logger.print err_formatter "@?L3JIT: %i used entries@\n@?" !count
  77         let create () =
  78           let v = Cache.Lvl3.create 1024 dummy in
  79           if !Config.verbose then at_exit (fun () -> show_stats v);
  80           v
  81
  82         let find t tlist s1 s2 =
  83           Cache.Lvl3.find t
  84             (Uid.to_int s2.StateSet.Node.id)
  85             (Uid.to_int s1.StateSet.Node.id)
  86             (Uid.to_int tlist.Translist.Node.id)
  87
  88         let add t tlist s1 s2 v =
  89           Cache.Lvl3.add t
  90             (Uid.to_int s2.StateSet.Node.id)
  91             (Uid.to_int s1.StateSet.Node.id)
  92             (Uid.to_int tlist.Translist.Node.id)
  93             v
  94
  95         let compile auto trl s1 s2 =
  96           let orig_s1, orig_s2 =
  97             Translist.fold (fun t (a1, a2) ->
  98                           let _, _, _, f = Transition.node t in
  99                           let fs1, fs2 = Formula.st f in
 100                             (StateSet.union a1 fs1, StateSet.union a2 fs2)
 101                        ) trl (StateSet.empty, StateSet.empty)
 102           in
 103           let ns1 = StateSet.inter s1 orig_s1
 104           and ns2 = StateSet.inter s2 orig_s2 in
 105           let res, ops, todo = eval_trans auto ns1 ns2 trl in
 106           let code, not_marking = ResJIT.compile ops in
 107           let todo_code, todo_notmarking =
 108             List.fold_left (fun (l, b) (p, q, o) -> let c, b' = ResJIT.compile o in
 109                                          (p, q, c)::l, b && b')
 110               ([], not_marking) todo
 111           in
 112           let opcode = res, code, todo_notmarking, todo_code in
 113           opcode
 114
 115         let choose_slot empty sl1 sl2 =
 116           if sl1 != empty then sl1
 117           else if sl2 != empty then sl2
 118           else Array.copy empty
 119
 120         let gen_code auto tlist s1 s2 =
 121           let res, code, not_marking, todo_code = compile auto tlist s1 s2 in
 122           let f =
 123             if todo_code == [] then begin
 124               if not_marking then begin fun empty_slot sl1 sl2 _ node ->
 125                 if sl1 == empty_slot && sl2 == empty_slot then res, empty_slot
 126                 else
 127                   let sl = choose_slot empty_slot sl1 sl2 in
 128                   U.exec sl sl1 sl2 node code;
 129                   res, sl
 130               end else (* marking *) begin fun empty_slot sl1 sl2 _ node ->
 131                 let sl = choose_slot empty_slot sl1 sl2 in
 132                 U.exec sl sl1 sl2 node code;
 133                 res, sl
 134               end
 135             end else (* todo_code *) begin fun empty_slot sl1 sl2 tree node ->
 136               let sl = choose_slot empty_slot sl1 sl2 in
 137               LOG( __ "bottom-up" 3 "Has todo code\n");
 138               U.exec sl sl1 sl2 node code;
 139               List.fold_left
 140                 (fun ares (p, q, code) ->
 141                   if !p tree node then begin
 142                     if code != ResJIT.Nil then U.exec sl sl1 sl2 node code;
 143                     StateSet.add q ares
 144                   end
 145                   else ares) res todo_code, sl
 146             end
 147           in
 148           f
 149
 150         let cache_apply cache auto tlist s1 s2 =
 151           let f = gen_code auto tlist s1 s2 in
 152           LOG(__ "top-down-run" 2 "Inserting: %i, %a, %a\n%!"
 153             (Uid.to_int tlist.Translist.Node.id) StateSet.print s1 StateSet.print s2);
 154           if not !Config.no_cache then add cache tlist s1 s2 f;
 155           f
 156       end
 157
 158 DEFINE LOOP (t, states, ctx) = (
 159   let _t = t in
 160   LOG(__ "top-down-run" 3
 161         "Entering node %i with loop (tag %s, context %i) with states %a"
 162         (Node.to_int _t)
 163         (Tag.to_string (Tree.tag tree _t))
 164         (Node.to_int (ctx))
 165         (StateSet.print) (states));
 166   if _t == Tree.nil then nil_res
 167   else
 168     let tag = Tree.tag tree _t in
 169       l2jit_dispatch
 170         _t tag (states) (ctx) (L2JIT.find cache2 tag (states))
 171 )
 172
 173 DEFINE LOOP_TAG (t, states, tag, ctx) = (
 174   let _t = (t) in (* to avoid duplicating expression t *)
 175   LOG(__ "top-down-run" 3
 176         "Entering node %i with loop_tag (tag %s, context %i) with states %a"
 177           (Node.to_int _t)
 178           (Tag.to_string (tag))
 179           (Node.to_int (ctx))
 180           (StateSet.print) (states));
 181   if _t == Tree.nil then nil_res
 182   else
 183     l2jit_dispatch
 184       _t (tag) (states) (ctx) (L2JIT.find cache2 (tag) (states)))
 185
 186
 187     let top_down_run auto tree root states ctx =
 188       let res_len = StateSet.max_elt auto.states + 1 in
 189       let empty_slot = Array.create res_len U.NS.empty in
 190       let nil_res = auto.bottom_states, empty_slot in
 191
 192       let mark_subtree s subtree =
 193         if subtree != U.NS.empty then
 194           let r = Array.copy empty_slot in
 195           r.(auto.last) <- subtree;
 196           s, r
 197         else
 198           s, empty_slot
 199       in
 200       let cache3 = L3JIT.create () in
 201       let l3jit_dispatch trl s1 s2 t sl1 sl2 =
 202         let f = L3JIT.find cache3 trl s1 s2 in
 203         if f == L3JIT.dummy then (L3JIT.cache_apply cache3 auto trl s1 s2) empty_slot sl1 sl2 tree t
 204         else f empty_slot sl1 sl2 tree t
 205       in
 206       let cache2 = L2JIT.create () in
 207       let rec loop t states ctx =
 208         if t == Tree.nil then nil_res
 209         else
 210           let tag = Tree.tag tree t in
 211           l2jit_dispatch
 212             t tag (states) (ctx) (L2JIT.find cache2 tag (states))
 213       and loop_tag t states ctx tag =
 214         if t == Tree.nil then nil_res
 215         else
 216           l2jit_dispatch
 217             t (tag) (states) (ctx) (L2JIT.find cache2 (tag) (states))
 218
 219       and l2jit_dispatch t tag states ctx opcode =
 220         match opcode with
 221           | L2JIT.RETURN () -> nil_res
 222           | L2JIT.LEFT (tr_list, instr) ->
 223               let res1, slot1 =
 224                 l2jit_dispatch_instr t (Tree.closing tree t) instr
 225               in
 226               l3jit_dispatch tr_list res1 auto.bottom_states t slot1 empty_slot
 227
 228           | L2JIT.RIGHT (tr_list, instr) ->
 229             let res2, slot2 =
 230               l2jit_dispatch_instr t ctx instr
 231             in
 232             l3jit_dispatch tr_list auto.bottom_states res2 t empty_slot slot2
 233
 234           | L2JIT.BOTH (tr_list, instr1, instr2) ->
 235               let res1, slot1 =
 236                 l2jit_dispatch_instr t (Tree.closing tree t) instr1
 237               in
 238               let res2, slot2 =
 239                 l2jit_dispatch_instr t ctx instr2
 240               in
 241                 l3jit_dispatch tr_list res1 res2 t slot1 slot2
 242           | L2JIT.CACHE () ->
 243             LOG(__ "top-down-run" 3
 244                   "Top-down cache miss for configuration %s %a"
 245                   (Tag.to_string tag) StateSet.print states);
 246             l2jit_dispatch t tag states ctx
 247               (L2JIT.compile cache2 auto tree tag states)
 248
 249     and l2jit_dispatch_instr t ctx instr =
 250         LOG(__ "top-down-run" 3 "Dispatching instr: %a on node %i (context=%i)"
 251               L2JIT.print_jump instr (Node.to_int t) (Node.to_int ctx));
 252         match instr with
 253         | L2JIT.NOP _ -> nil_res
 254         | L2JIT.FIRST_CHILD s -> loop (Tree.first_child tree t) s ctx
 255         | L2JIT.NEXT_SIBLING s -> loop (Tree.next_sibling tree t) s ctx
 256
 257         | L2JIT.FIRST_ELEMENT s -> loop (Tree.first_element tree t) s ctx
 258         | L2JIT.NEXT_ELEMENT s -> loop (Tree.next_element tree t) s ctx
 259
 260         | L2JIT.TAGGED_DESCENDANT (s, tag) ->
 261           loop_tag (Tree.tagged_descendant tree t tag) s ctx tag
 262
 263         | L2JIT.TAGGED_FOLLOWING (s, tag) ->
 264           loop_tag (Tree.tagged_following_before tree t tag ctx) s ctx  tag
 265
 266         | L2JIT.SELECT_DESCENDANT (s, _, us) ->
 267           loop (Tree.select_descendant tree t us) s ctx
 268
 269         | L2JIT.SELECT_FOLLOWING (s, pt, us) ->
 270           loop (Tree.select_following_before tree t us ctx) s ctx
 271
 272         | L2JIT.TAGGED_CHILD (s, tag) ->
 273           loop_tag (Tree.tagged_child tree t tag) s ctx tag
 274
 275         | L2JIT.TAGGED_SIBLING (s, tag) ->
 276           loop_tag (Tree.tagged_sibling tree t tag) s ctx tag
 277
 278         | L2JIT.SELECT_CHILD (s, _, us) ->
 279           loop (Tree.select_child tree t us) s ctx
 280
 281         | L2JIT.SELECT_SIBLING (s, _, us) ->
 282           loop (Tree.select_sibling tree t us) s ctx
 283
 284         | L2JIT.TAGGED_SUBTREE(s, tag) ->
 285           mark_subtree s (U.NS.subtree_tags tree t tag)
 286
 287         | L2JIT.ELEMENT_SUBTREE(s) ->
 288           mark_subtree s (U.NS.subtree_elements tree t)
 289       in
 290       let r = loop root states ctx in
 291       r
 292
 293     let full_top_down_run auto states tree root =
 294       top_down_run auto tree root states (Tree.closing tree root)
 295
 296     let top_down_run auto tree root =
 297       Ata.init ();
 298       L2JIT.init();
 299       let res, slot = full_top_down_run auto auto.init tree root in
 300       slot.(StateSet.min_elt auto.topdown_marking_states)
 301
 302
 303     (*** Bottom-up evaluation function **)
 304
 305     let eval_trans auto tree parent res1 res2 = assert false
 306
 307     let rec uniq = function
 308       | ([] | [ _ ]) as l -> l
 309       | e1 :: ((e2 :: ll) as l) -> if e1 == e2 then uniq l
 310         else e1 :: e2 :: (uniq ll);;
 311
 312 DEFINE BOTTOM_UP_NEXT(node, rest, stop) =
 313       (let ___fs = Tree.first_child tree node in
 314        let ___res1 =
 315          if ___fs == Tree.nil then nil_res
 316          else full_top_down_run auto states tree ___fs
 317        in
 318        move_up node ___res1 true rest stop)
 319
 320
 321     let bottom_up_run auto tree (query, pat) =
 322       let array = time ~msg:"Timing text query" (Tree.full_text_query query tree) pat in
 323       let leaves = Array.to_list array in
 324       let states = auto.states in
 325       let res_len = (StateSet.max_elt states) + 1 in
 326       let empty_slot = Array.create res_len U.NS.empty in
 327       let nil_res = auto.bottom_states, empty_slot in
 328       let cache = Cache.Lvl3.create 0 L3JIT.dummy in
 329       let rec move_up node res is_left rest stop =
 330         LOG(__ "bottom-up" 2 "move_up: node %i is_left %b stop %i\n"
 331               (Node.to_int node) is_left (Node.to_int stop));
 332         if node == stop then res, rest
 333         else
 334           (*let prev_sibling = Tree.prev_sibling tree node in *)
 335           let is_left' = Tree.is_first_child tree node (*prev_sibling == Tree.nil*) in
 336           (*TODO: unsound in case of following-sibling moves
 337             should replace the else by previous_sibling and walk up the sequence of
 338             right child moves *)
 339           let parent = if is_left' then Tree.parent tree node else
 340               let p = Tree.first_child tree (Tree.parent tree node) in
 341               if p < stop then stop else p
 342           in
 343           let (s1, sl1), (s2, sl2), rest' =
 344             if is_left then match rest with
 345                 [] -> res, nil_res, rest
 346               | next :: rest' ->
 347                 if Tree.is_right_descendant tree node next
 348                 then
 349                   let res2, rest' = (*bottom_up_next*) BOTTOM_UP_NEXT(next, rest', node) in
 350                   res, res2, rest'
 351                 else res, nil_res, rest
 352             else
 353               nil_res, res, rest
 354           in
 355           let tag = Tree.tag tree node in
 356           let id1 = Uid.to_int s1.StateSet.Node.id in
 357           let id2 = Uid.to_int s2.StateSet.Node.id in
 358           let code =
 359             let code = Cache.Lvl3.find cache id2 id1 tag in
 360             if code == L3JIT.dummy  then
 361               let trl =
 362                 StateSet.fold
 363                   (fun q acc ->
 364                     List.fold_left (fun acc' (labels, tr) ->
 365                       if TagSet.mem tag labels
 366                       then Translist.cons tr acc' else acc')
 367                       acc
 368                       (Hashtbl.find auto.trans q)
 369                   )
 370                   states
 371                   Translist.nil
 372               in
 373               LOG( __ "bottom-up" 3 "Transition list for %s, %a, %a is %a\n"
 374                      (Tag.to_string tag)
 375                      StateSet.print s1
 376                      StateSet.print s2
 377                      Translist.print trl
 378               );
 379               let code = L3JIT.gen_code auto trl s1 s2 in
 380               Cache.Lvl3.add cache id2 id1 tag code; code
 381             else code
 382           in
 383           let res' = code empty_slot sl1 sl2 tree node in
 384           move_up parent res' is_left' rest' stop
 385       in
 386       let loop_leaves l =
 387         match l with
 388           [] -> nil_res
 389         | node :: ll ->
 390           let res, lll = BOTTOM_UP_NEXT( (*bottom_up_next*) node, ll, Tree.nil) in
 391           if lll <> [] then
 392             Logger.print err_formatter "WARNING: Leftover nodes: %i\n" (List.length lll);
 393           res
 394       in
 395     let _, slot = loop_leaves leaves in
 396     slot.(StateSet.min_elt auto.topdown_marking_states)
 397
 398
 399
 400     (* Slow reference top-down implementation *)
 401     let naive_top_down auto tree root states ctx =
 402       let res_len = StateSet.max_elt auto.states + 1 in
 403       let empty_slot = Array.create res_len U.NS.empty in
 404       let nil_res = auto.bottom_states, empty_slot in
 405       let cache3 = L3JIT.create () in
 406       let l3jit_dispatch trl s1 s2 t sl1 sl2 =
 407         let f = L3JIT.find cache3 trl s1 s2 in
 408         if f == L3JIT.dummy then (L3JIT.cache_apply cache3 auto trl s1 s2) empty_slot sl1 sl2 tree t
 409         else f empty_slot sl1 sl2 tree t
 410       in
 411       let dummy = Translist.nil, StateSet.singleton State.dummy, StateSet.singleton State.dummy in
 412       let cache2 = Cache.Lvl2.create 512 dummy in
 413       let rec loop t states ctx =
 414         if states == StateSet.empty then nil_res
 415         else if t == Tree.nil then (*StateSet.inter states auto.bottom_states, empty_slot *) nil_res
 416         else
 417           let tag = Tree.tag tree t in
 418
 419           let trans, lstates, rstates =
 420             let c = Cache.Lvl2.find cache2 (Uid.to_int states.StateSet.Node.id) tag in
 421             if c == dummy then
 422               let c = Ata.get_trans auto states tag in
 423               Cache.Lvl2.add cache2 (Uid.to_int states.StateSet.Node.id) tag c;
 424               c
 425             else c
 426           in
 427           let s1, res1 = loop (Tree.first_child tree t) lstates ctx
 428           and s2, res2 = loop (Tree.next_sibling tree t) rstates ctx in
 429           l3jit_dispatch trans s1 s2 t res1 res2
 430       in
 431       loop root states ctx
 432
 433
 434
 435
 436     let naive_top_down_run auto tree root =
 437       let res, slot = naive_top_down auto tree root auto.init (Tree.closing tree root) in
 438       slot.(StateSet.min_elt auto.topdown_marking_states)
 439
 440
 441
 442     let eval_form auto s1 s2 f =
 443       let rec loop f =
 444         match Formula.expr f with
 445           | Formula.False | Formula.True | Formula.Pred _ -> f
 446           | Formula.Atom(`Left, b, q) ->
 447               Formula.of_bool (b == (StateSet.mem q s1))
 448           | Formula.Atom (`Right, b, q) ->
 449               Formula.of_bool(b == (StateSet.mem q s2))
 450           | Formula.Atom (`Epsilon, _, _) -> assert false
 451
 452           | Formula.Or(f1, f2) ->
 453               let b1 = loop f1 in
 454               let b2 = loop f2 in
 455               Formula.or_pred b1 b2
 456           | Formula.And(f1, f2) ->
 457               let b1 = loop f1 in
 458               let b2 = loop f2 in
 459               Formula.and_pred b1 b2
 460       in
 461       loop f
 462
 463     let eval_trans auto s1 s2 trans =
 464       Translist.fold
 465         (fun t ((a_st, mark) as acc)->
 466            let q, _, m, f = Transition.node t in
 467            let form = eval_form auto s1 s2 f in
 468            match Formula.expr form with
 469              | Formula.True -> StateSet.add q a_st, mark || m
 470              | Formula.False -> acc
 471              | _ -> assert false
 472         ) trans (StateSet.empty, false)
 473
 474
 475     let set a i v =
 476       LOG(__ "twopass" 2 "Setting node %i to state %a\n%!"
 477         i StateSet.print v);
 478       a.(i) <- v
 479
 480     let twopass_top_down states_array auto tree root states ctx =
 481       let dummy3 = StateSet.singleton State.dummy in
 482       let cache3 = Cache.Lvl3.create 512  dummy3 in
 483       let dummy2 = Translist.nil, StateSet.singleton State.dummy, StateSet.singleton State.dummy in
 484       let cache2 = Cache.Lvl2.create 512 dummy2 in
 485       let attributes = TagSet.inj_positive (Tree.attribute_tags tree) in
 486       let rec loop t states ctx =
 487         if t == Tree.nil then auto.bottom_states
 488         else if states == StateSet.empty then
 489           let () = set states_array (Node.to_int t) auto.bottom_states in
 490           auto.bottom_states
 491         else
 492           let tag = Tree.tag tree t in
 493           LOG(__ "twopass" 2 "Traversing node %i (tag %s) in states %a\n%!" (Node.to_int t) (Tag.to_string tag)
 494           StateSet.print states
 495           );
 496           let trans, lstates, rstates =
 497             let c = Cache.Lvl2.find cache2 (Uid.to_int states.StateSet.Node.id) tag in
 498             if c == dummy2 then
 499               let c = Ata.get_trans ~attributes:attributes auto states tag in
 500               Cache.Lvl2.add cache2 (Uid.to_int states.StateSet.Node.id) tag c;
 501               c
 502             else c
 503           in
 504           LOG(__ "twopass" 2 "\nTransitions are:\n%!");
 505           LOG(__ "twopass" 2"\nTransitions are:\n%a\n%!"
 506             Translist.print trans
 507           );
 508           let s1 = loop (Tree.first_child tree t) lstates ctx
 509           and s2 = loop (Tree.next_sibling tree t) rstates ctx in
 510           let st =
 511             let c = Cache.Lvl3.find cache3
 512               (Uid.to_int s1.StateSet.Node.id)
 513               (Uid.to_int s2.StateSet.Node.id)
 514               (Uid.to_int trans.Translist.Node.id)
 515             in
 516             if c == dummy3 then
 517               let c, _ = eval_trans auto s1 s2 trans in
 518               Cache.Lvl3.add cache3
 519                 (Uid.to_int s1.StateSet.Node.id)
 520                 (Uid.to_int s2.StateSet.Node.id)
 521                 (Uid.to_int trans.Translist.Node.id) c;c
 522             else c
 523           in
 524           set states_array (Node.to_int t) st;
 525           st
 526       in
 527       loop root states ctx, (dummy2, cache2)
 528
 529
 530     type action = Nop | Mark | Dummy
 531
 532     let twopass_top_down_scan states_array (dummy2, cache2) auto tree root states ctx =
 533       let attributes = TagSet.inj_positive (Tree.attribute_tags tree) in
 534       let cache3 = Cache.Lvl3.create 512  Dummy in
 535       let rec loop t states acc =
 536         if states == StateSet.empty || t = Tree.nil then acc
 537         else
 538           let tag = Tree.tag tree t in
 539           let trans, _, _ =
 540           let c = Cache.Lvl2.find cache2 (Uid.to_int states.StateSet.Node.id) tag in
 541             if c == dummy2 then
 542               let c = Ata.get_trans  ~attributes:attributes auto states tag in
 543               Cache.Lvl2.add cache2 (Uid.to_int states.StateSet.Node.id) tag c;
 544               c
 545             else c
 546           in
 547           let fs = Tree.first_child tree t in
 548           let ns = Tree.next_sibling tree t in
 549           let s1 = if fs != Tree.nil then states_array.(Node.to_int fs) else auto.bottom_states
 550           and s2 = if ns != Tree.nil then states_array.(Node.to_int ns) else auto.bottom_states
 551           in
 552           let mark =
 553             let c = Cache.Lvl3.find cache3
 554               (Uid.to_int s1.StateSet.Node.id)
 555               (Uid.to_int s2.StateSet.Node.id)
 556               (Uid.to_int trans.Translist.Node.id)
 557             in
 558             if c == Dummy then
 559               let _, c = eval_trans auto s1 s2 trans in
 560               let c = if c then Mark else Nop in
 561                Cache.Lvl3.add cache3
 562                  (Uid.to_int s1.StateSet.Node.id)
 563                  (Uid.to_int s2.StateSet.Node.id)
 564                  (Uid.to_int trans.Translist.Node.id) c;c
 565             else c
 566           in
 567           LOG(__ "twopass" 2 "Evaluating node %i (tag %s).\n%!States=%a\n%!"
 568             (Node.to_int t)
 569             (Tag.to_string tag)
 570             StateSet.print states
 571           );
 572           LOG(__ "twopass" 2 "Translist=%a\nLeft=%a\nRight=%a\nMark=%s\n\n%!"
 573             Translist.print trans
 574             StateSet.print s1
 575             StateSet.print s2
 576             (match mark with
 577               Dummy -> "Dummy"
 578             | Mark -> "Mark"
 579             | Nop -> "Nop"));
 580           if mark == Mark then
 581             loop ns s2 (loop fs s1 (U.NS.snoc acc t))
 582           else
 583             loop ns s2 (loop fs s1 acc)
 584       in
 585       loop root states U.NS.empty
 586
 587     let twopass_top_down_run auto tree root =
 588       let len = Node.to_int (Tree.closing tree root) + 1 in
 589       LOG(__ "twopass" 2 "Creating array of size: %i\n%!" len);
 590       let states_array = Array.make len StateSet.empty in
 591       let _, cache =
 592         twopass_top_down states_array auto tree root auto.init Tree.nil
 593       in
 594       twopass_top_down_scan states_array cache auto tree root auto.init Tree.nil
 595
 596
 597
 598
 599
 600
 601
 602
 603
 604
 605   end