From dcc638cf4072979834f404894cbedc653542374f Mon Sep 17 00:00:00 2001 From: =?utf8?q?Kim=20Nguy=E1=BB=85n?= Date: Wed, 18 Apr 2012 13:43:32 +0200 Subject: [PATCH] Misc. rewrites: - cosmetic changes tab -> whitespaces - more logging --- src/ata.ml | 171 ++++---- src/ata.mli | 2 + src/compile.ml | 7 +- src/runtime.ml | 1087 ++++++++++++++++++++++++------------------------ 4 files changed, 639 insertions(+), 628 deletions(-) diff --git a/src/ata.ml b/src/ata.ml index 3c27ae8..ae633d3 100644 --- a/src/ata.ml +++ b/src/ata.ml @@ -81,18 +81,24 @@ let print_kind fmt k = end; fprintf fmt "%!" +let pr_trans fmt (ts, (l, r, m)) = + Format.fprintf fmt "%a %s %a %a" + TagSet.print ts + (if m then Pretty.double_right_arrow else Pretty.right_arrow) + StateSet.print l + StateSet.print r let compute_jump auto tree states l marking = let rel_trans, skip_trans = List.fold_left (fun (acc_rel, acc_skip) ((ts, (l,r,marking)) as tr) -> - if not marking && - ((l == states && r == states) - || (l == StateSet.empty && states == r) - || (l == states && r = StateSet.empty) - || (l == StateSet.empty && r = StateSet.empty)) - then (acc_rel, tr::acc_skip) - else (tr::acc_rel, acc_skip)) + if not marking && + ((l == states && r == states) + || (l == StateSet.empty && states == r) + || (l == states && r = StateSet.empty) + || (l == StateSet.empty && r = StateSet.empty)) + then (acc_rel, tr::acc_skip) + else (tr::acc_rel, acc_skip)) ([],[]) l in let rel_labels = List.fold_left @@ -105,24 +111,30 @@ let compute_jump auto tree states l marking = else match skip_trans with [ (_, (l, r, _) ) ] when l == r && l == states -> - begin - match rel_trans with - | [ (_, (l, r, m) ) ] - when (rel_labels == (Tree.element_tags tree) || - Ptset.Int.is_singleton rel_labels) - && (StateSet.diff l auto.true_states) == states && m - -> CAPTURE_MANY(rel_labels) - | _ -> - JUMP_MANY(rel_labels) - end + begin + match rel_trans with + | [ (_, (l, r, m) ) ] + when (rel_labels == (Tree.element_tags tree) || + Ptset.Int.is_singleton rel_labels) + && (StateSet.diff l auto.true_states) == states && m + -> CAPTURE_MANY(rel_labels) + | _ -> + JUMP_MANY(rel_labels) + end | [ (_, (l, r, _) ) ] when l == StateSet.empty -> JUMP_ONE(rel_labels) | _ -> if Ptset.Int.mem Tag.pcdata rel_labels then begin - LOG(__ "top-down-approx" 3 "Computed rel_labels: %a@\n" - TagSet.print (TagSet.inj_positive rel_labels)); - NODE + LOG(__ "top-down-approx" 3 "Computed rel_labels: %a" + TagSet.print (TagSet.inj_positive rel_labels)); + LOG(__ "top-down-approx" 3 "skip_trans:@\n%a" + (Pretty.pp_print_list ~sep:Format.pp_force_newline pr_trans) + skip_trans); + LOG(__ "top-down-approx" 3 "rel_trans:@\n%a" + (Pretty.pp_print_list ~sep:Format.pp_force_newline pr_trans) + rel_trans); + NODE end else STAR module Cache = Hashtbl.Make(StateSet) @@ -171,33 +183,33 @@ let top_down_approx auto states tree = | Not_found -> let trs = (* Collect all (ts, (l, r, m)) where - ts is a tagset, l and r are left and right set of states - m is marking flag + ts is a tagset, l and r are left and right set of states + m is marking flag *) fold_trans_of_states auto - (fun acc_tr (ts, tr) -> - let pos = - if ts == TagSet.star then Tree.element_tags tree - else if ts == TagSet.any then Tree.node_tags tree - else TagSet.positive ts - in - let _, _, m, f = Transition.node tr in - let ls, rs = Formula.st f in - if Ptset.Int.is_empty pos then acc_tr - else - (TagSet.inj_positive pos, (ls, rs, m))::acc_tr - ) - states - [] + (fun acc_tr (ts, tr) -> + let pos = + if ts == TagSet.star then Tree.element_tags tree + else if ts == TagSet.any then Tree.node_tags tree + else TagSet.positive ts + in + let _, _, m, f = Transition.node tr in + let ls, rs = Formula.st f in + if Ptset.Int.is_empty pos then acc_tr + else + (TagSet.inj_positive pos, (ls, rs, m))::acc_tr + ) + states + [] in (* for all labels in the tree compute which transition is taken *) let all_trs = Ptset.Int.fold (fun tag acc -> - List.fold_left (fun acc' (ts, rhs) -> - if TagSet.mem tag ts then - (TagSet.singleton tag, rhs)::acc' - else acc') acc trs) - (Tree.node_tags tree) [] + List.fold_left (fun acc' (ts, rhs) -> + if TagSet.mem tag ts then + (TagSet.singleton tag, rhs)::acc' + else acc') acc trs) + (Tree.node_tags tree) [] in (* merge together states that have common labels *) let uniq_states_trs = @@ -206,48 +218,48 @@ let top_down_approx auto states tree = (* merge together labels that have common states *) let td_approx = merge_trans by_states merge_labels - (List.sort by_states uniq_states_trs) + (List.sort by_states uniq_states_trs) in LOG( let is_pairwise_disjoint l = - List.for_all (fun ((ts, _) as tr) -> - List.for_all (fun ((ts', _) as tr') -> - (ts == ts' && (by_states tr tr' == 0)) || - TagSet.is_empty (TagSet.cap ts ts')) l) l + List.for_all (fun ((ts, _) as tr) -> + List.for_all (fun ((ts', _) as tr') -> + (ts == ts' && (by_states tr tr' == 0)) || + TagSet.is_empty (TagSet.cap ts ts')) l) l in let is_complete l = TagSet.positive - (List.fold_left (fun acc (ts, _) -> TagSet.cup acc ts) - TagSet.empty l) - == - (Tree.node_tags tree) + (List.fold_left (fun acc (ts, _) -> TagSet.cup acc ts) + TagSet.empty l) + == + (Tree.node_tags tree) in let pr_td_approx fmt td_approx = - List.iter (fun (ts,(l,r, m)) -> - let ts = if TagSet.cardinal ts >10 - then TagSet.diff TagSet.any - (TagSet.diff - (TagSet.inj_positive (Tree.node_tags tree)) - ts) - else ts - in - fprintf fmt "%a, %a, %b -> %a, %a@\n" - StateSet.print states - TagSet.print ts - m - StateSet.print l - StateSet.print r - ) td_approx; - fprintf fmt "\n%!" + List.iter (fun (ts,(l,r, m)) -> + let ts = if TagSet.cardinal ts >10 + then TagSet.diff TagSet.any + (TagSet.diff + (TagSet.inj_positive (Tree.node_tags tree)) + ts) + else ts + in + fprintf fmt "%a, %a, %b -> %a, %a@\n" + StateSet.print states + TagSet.print ts + m + StateSet.print l + StateSet.print r + ) td_approx; + fprintf fmt "\n%!" in __ "top-down-approx" 2 " pairwise-disjoint:%b, complete:%b:@\n%a" - (is_pairwise_disjoint td_approx) - (is_complete td_approx) - pr_td_approx td_approx + (is_pairwise_disjoint td_approx) + (is_complete td_approx) + pr_td_approx td_approx ); let jump = compute_jump - auto tree states td_approx - (List.exists (fun (_,(_,_,b)) -> b) td_approx) + auto tree states td_approx + (List.exists (fun (_,(_,_,b)) -> b) td_approx) in Cache.add cache states jump; jump @@ -260,17 +272,16 @@ let get_trans ?(attributes=TagSet.empty) auto states tag = in let b = TagSet.mem tag ts in let () = LOG(__ "transition" 3 "tag=<%s>, %s: %a7C" - (Tag.to_string tag) - (if b then " taking" else "not taking") - Transition.print tr) + (Tag.to_string tag) + (if b then " taking" else "not taking") + Transition.print tr) in if b then - let _, _, _, f = Transition.node tr in - let l, r = Formula.st f in - (Translist.cons tr tr_acc, - StateSet.union l l_acc, - StateSet.union r r_acc) + let _, _, _, f = Transition.node tr in + let l, r = Formula.st f in + (Translist.cons tr tr_acc, + StateSet.union l l_acc, + StateSet.union r r_acc) else acc) acc (Hashtbl.find auto.trans q)) states (Translist.nil, StateSet.empty, StateSet.empty) - diff --git a/src/ata.mli b/src/ata.mli index 9fa9d67..74966b1 100644 --- a/src/ata.mli +++ b/src/ata.mli @@ -21,6 +21,8 @@ type jump_kind = | JUMP_MANY of Ptset.Int.t | CAPTURE_MANY of Ptset.Int.t +val print_kind : Format.formatter -> jump_kind -> unit + val top_down_approx : t -> StateSet.t -> Tree.t -> jump_kind val init : unit -> unit diff --git a/src/compile.ml b/src/compile.ml index e60ede6..296f665 100644 --- a/src/compile.ml +++ b/src/compile.ml @@ -65,10 +65,9 @@ let rec compile_step toplevel (axis, test, _) state cont conf last = let loop = loopfun (`Left *+ state) (`Right *+ state) in let phi = mk_phi toplevel cont loop in ( [ (Transition.make (state, test, marking, phi)); - (Transition.make (state, TagSet.any, false, loop)); - (*(Transition.make (state, TagSet.any, false, `Right *+ state)) *) - ], - (`Left *+ state)) + (Transition.make (state, TagSet.any, false, loop)); + ], + (`Left *+ state)) | _ -> assert false in diff --git a/src/runtime.ml b/src/runtime.ml index 3082f50..2285116 100644 --- a/src/runtime.ml +++ b/src/runtime.ml @@ -20,24 +20,24 @@ module Make (U : ResJIT.S) : S with type result_set = U.NS.t = let eval_form auto s1 s2 f = let rec loop f = - match Formula.expr f with - | Formula.False | Formula.True | Formula.Pred _ -> f, [] - | Formula.Atom(`Left, b, q) -> - Formula.of_bool (b == (StateSet.mem q s1)), - if b && StateSet.mem q auto.topdown_marking_states then [ResJIT.LEFT q] else [] - | Formula.Atom (`Right, b, q) -> - Formula.of_bool(b == (StateSet.mem q s2)), - if b && StateSet.mem q auto.topdown_marking_states then [ResJIT.RIGHT q] else [] - | Formula.Atom (`Epsilon, _, _) -> assert false - - | Formula.Or(f1, f2) -> - let b1, i1 = loop f1 in - let b2, i2 = loop f2 in - Formula.or_pred b1 b2, i1 @ i2 - | Formula.And(f1, f2) -> - let b1, i1 = loop f1 in - let b2, i2 = loop f2 in - Formula.and_pred b1 b2, i1 @ i2 + match Formula.expr f with + | Formula.False | Formula.True | Formula.Pred _ -> f, [] + | Formula.Atom(`Left, b, q) -> + Formula.of_bool (b == (StateSet.mem q s1)), + if b && StateSet.mem q auto.topdown_marking_states then [ResJIT.LEFT q] else [] + | Formula.Atom (`Right, b, q) -> + Formula.of_bool(b == (StateSet.mem q s2)), + if b && StateSet.mem q auto.topdown_marking_states then [ResJIT.RIGHT q] else [] + | Formula.Atom (`Epsilon, _, _) -> assert false + + | Formula.Or(f1, f2) -> + let b1, i1 = loop f1 in + let b2, i2 = loop f2 in + Formula.or_pred b1 b2, i1 @ i2 + | Formula.And(f1, f2) -> + let b1, i1 = loop f1 in + let b2, i2 = loop f2 in + Formula.and_pred b1 b2, i1 @ i2 in loop f @@ -45,131 +45,131 @@ module Make (U : ResJIT.S) : S with type result_set = U.NS.t = let eval_trans auto s1 s2 trans = LOG(__ "top-down-run" 3 "Evaluating transition list:@\n%a" Translist.print trans); Translist.fold - (fun t ((a_st, a_op, a_todo) as acc)-> - let q, _, m, f = Transition.node t in - let form, ops = eval_form auto s1 s2 f in - match Formula.expr form with - | Formula.True -> - StateSet.add q a_st, - (q, (if m then (ResJIT.SELF() :: ops) else ops)):: a_op, - a_todo - | Formula.False -> acc - | Formula.Pred p -> a_st, a_op, - (p.Tree.Predicate.node, q, [(q,(if m then (ResJIT.SELF() :: ops) else ops))]) :: a_todo - | _ -> assert false - ) trans (StateSet.empty, [], []) + (fun t ((a_st, a_op, a_todo) as acc)-> + let q, _, m, f = Transition.node t in + let form, ops = eval_form auto s1 s2 f in + match Formula.expr form with + | Formula.True -> + StateSet.add q a_st, + (q, (if m then (ResJIT.SELF() :: ops) else ops)):: a_op, + a_todo + | Formula.False -> acc + | Formula.Pred p -> a_st, a_op, + (p.Tree.Predicate.node, q, [(q,(if m then (ResJIT.SELF() :: ops) else ops))]) :: a_todo + | _ -> assert false + ) trans (StateSet.empty, [], []) module L3JIT = struct - type opcode = (t -> t -> t -> Tree.t -> Tree.node -> StateSet.t * t) - - type t = opcode Cache.Lvl3.t - - let dummy _ _ _ _ _ = failwith "Uninitialized L3JIT" - - - let show_stats a = - let count = ref 0 in - Cache.Lvl3.iteri (fun _ _ _ _ b -> if not b then incr count) a; - Logger.print err_formatter "@?L3JIT: %i used entries@\n@?" !count - let create () = - let v = Cache.Lvl3.create 1024 dummy in - if !Options.verbose then at_exit (fun () -> show_stats v); - v - - let find t tlist s1 s2 = - Cache.Lvl3.find t - (Uid.to_int s2.StateSet.Node.id) - (Uid.to_int s1.StateSet.Node.id) - (Uid.to_int tlist.Translist.Node.id) - - let add t tlist s1 s2 v = - Cache.Lvl3.add t - (Uid.to_int s2.StateSet.Node.id) - (Uid.to_int s1.StateSet.Node.id) - (Uid.to_int tlist.Translist.Node.id) - v - - let compile auto trl s1 s2 = - let orig_s1, orig_s2 = - Translist.fold (fun t (a1, a2) -> - let _, _, _, f = Transition.node t in - let fs1, fs2 = Formula.st f in - (StateSet.union a1 fs1, StateSet.union a2 fs2) - ) trl (StateSet.empty, StateSet.empty) - in - let ns1 = StateSet.inter s1 orig_s1 - and ns2 = StateSet.inter s2 orig_s2 in - let res, ops, todo = eval_trans auto ns1 ns2 trl in - let code, not_marking = ResJIT.compile ops in - let todo_code, todo_notmarking = - List.fold_left (fun (l, b) (p, q, o) -> let c, b' = ResJIT.compile o in - (p, q, c)::l, b && b') - ([], not_marking) todo - in - let opcode = res, code, todo_notmarking, todo_code in - opcode - - let gen_code auto tlist s1 s2 = - let res, code, not_marking, todo_code = compile auto tlist s1 s2 in - let f = - if todo_code == [] then - if not_marking then begin fun empty_slot sl1 sl2 _ node -> - let slot1_empty = sl1 == empty_slot - and slot2_empty = sl2 == empty_slot in - if slot1_empty && slot2_empty then res,sl2 - else - let sl = - if slot2_empty then - if slot1_empty then - Array.copy empty_slot - else sl1 - else sl2 - in - U.exec sl sl1 sl2 node code; - res, sl - end - else (* marking *) begin fun empty_slot sl1 sl2 _ node -> - let sl = - if sl2 == empty_slot then - if sl1 == empty_slot then - Array.copy empty_slot - else sl1 - else sl2 - in - U.exec sl sl1 sl2 node code; - res, sl - end - else (* todo != [] *) - begin fun empty_slot sl1 sl2 tree node -> - let sl = - if sl2 == empty_slot then - if sl1 == empty_slot then - Array.copy empty_slot - else sl1 - else sl2 - in - U.exec sl sl1 sl2 node code; - List.fold_left - (fun ares (p, q, code) -> - if !p tree node then begin - if code != ResJIT.Nil then U.exec sl sl1 sl2 node code; - StateSet.add q ares - end - else ares) res todo_code, sl - - end - in - f - - let cache_apply cache auto tlist s1 s2 = - let f = gen_code auto tlist s1 s2 in - LOG(__ "grammar" 2 "Inserting: %i, %a, %a\n%!" - (Uid.to_int tlist.Translist.Node.id) StateSet.print s1 StateSet.print s2); - add cache tlist s1 s2 f; f + type opcode = (t -> t -> t -> Tree.t -> Tree.node -> StateSet.t * t) + + type t = opcode Cache.Lvl3.t + + let dummy _ _ _ _ _ = failwith "Uninitialized L3JIT" + + + let show_stats a = + let count = ref 0 in + Cache.Lvl3.iteri (fun _ _ _ _ b -> if not b then incr count) a; + Logger.print err_formatter "@?L3JIT: %i used entries@\n@?" !count + let create () = + let v = Cache.Lvl3.create 1024 dummy in + if !Options.verbose then at_exit (fun () -> show_stats v); + v + + let find t tlist s1 s2 = + Cache.Lvl3.find t + (Uid.to_int s2.StateSet.Node.id) + (Uid.to_int s1.StateSet.Node.id) + (Uid.to_int tlist.Translist.Node.id) + + let add t tlist s1 s2 v = + Cache.Lvl3.add t + (Uid.to_int s2.StateSet.Node.id) + (Uid.to_int s1.StateSet.Node.id) + (Uid.to_int tlist.Translist.Node.id) + v + + let compile auto trl s1 s2 = + let orig_s1, orig_s2 = + Translist.fold (fun t (a1, a2) -> + let _, _, _, f = Transition.node t in + let fs1, fs2 = Formula.st f in + (StateSet.union a1 fs1, StateSet.union a2 fs2) + ) trl (StateSet.empty, StateSet.empty) + in + let ns1 = StateSet.inter s1 orig_s1 + and ns2 = StateSet.inter s2 orig_s2 in + let res, ops, todo = eval_trans auto ns1 ns2 trl in + let code, not_marking = ResJIT.compile ops in + let todo_code, todo_notmarking = + List.fold_left (fun (l, b) (p, q, o) -> let c, b' = ResJIT.compile o in + (p, q, c)::l, b && b') + ([], not_marking) todo + in + let opcode = res, code, todo_notmarking, todo_code in + opcode + + let gen_code auto tlist s1 s2 = + let res, code, not_marking, todo_code = compile auto tlist s1 s2 in + let f = + if todo_code == [] then + if not_marking then begin fun empty_slot sl1 sl2 _ node -> + let slot1_empty = sl1 == empty_slot + and slot2_empty = sl2 == empty_slot in + if slot1_empty && slot2_empty then res,sl2 + else + let sl = + if slot2_empty then + if slot1_empty then + Array.copy empty_slot + else sl1 + else sl2 + in + U.exec sl sl1 sl2 node code; + res, sl + end + else (* marking *) begin fun empty_slot sl1 sl2 _ node -> + let sl = + if sl2 == empty_slot then + if sl1 == empty_slot then + Array.copy empty_slot + else sl1 + else sl2 + in + U.exec sl sl1 sl2 node code; + res, sl + end + else (* todo != [] *) + begin fun empty_slot sl1 sl2 tree node -> + let sl = + if sl2 == empty_slot then + if sl1 == empty_slot then + Array.copy empty_slot + else sl1 + else sl2 + in + U.exec sl sl1 sl2 node code; + List.fold_left + (fun ares (p, q, code) -> + if !p tree node then begin + if code != ResJIT.Nil then U.exec sl sl1 sl2 node code; + StateSet.add q ares + end + else ares) res todo_code, sl + + end + in + f + + let cache_apply cache auto tlist s1 s2 = + let f = gen_code auto tlist s1 s2 in + LOG(__ "grammar" 2 "Inserting: %i, %a, %a\n%!" + (Uid.to_int tlist.Translist.Node.id) StateSet.print s1 StateSet.print s2); + add cache tlist s1 s2 f; f end DEFINE LOOP (t, states, ctx) = ( @@ -190,11 +190,11 @@ DEFINE LOOP (t, states, ctx) = ( DEFINE LOOP_TAG (t, states, tag, ctx) = ( let _t = (t) in (* to avoid duplicating expression t *) LOG(__ "top-down-run" 3 - "Entering node %i with loop_tag (tag %s, context %i) with states %a" - (Node.to_int _t) - (Tag.to_string (tag)) - (Node.to_int (ctx)) - (StateSet.print) (states)); + "Entering node %i with loop_tag (tag %s, context %i) with states %a" + (Node.to_int _t) + (Tag.to_string (tag)) + (Node.to_int (ctx)) + (StateSet.print) (states)); if _t == Tree.nil then nil_res else l2jit_dispatch @@ -207,93 +207,93 @@ DEFINE LOOP_TAG (t, states, tag, ctx) = ( let nil_res = auto.bottom_states, empty_slot in let cache3 = L3JIT.create () in let mark_subtree = - fun s subtree -> if subtree != U.NS.empty then - let r = Array.copy empty_slot in - r.(auto.last) <- subtree; - s,r - else - s,empty_slot + fun s subtree -> if subtree != U.NS.empty then + let r = Array.copy empty_slot in + r.(auto.last) <- subtree; + s,r + else + s,empty_slot in let l3jit_dispatch trl s1 s2 t sl1 sl2 = - let f = L3JIT.find cache3 trl s1 s2 in - if f == L3JIT.dummy then (L3JIT.cache_apply cache3 auto trl s1 s2) empty_slot sl1 sl2 tree t - else f empty_slot sl1 sl2 tree t + let f = L3JIT.find cache3 trl s1 s2 in + if f == L3JIT.dummy then (L3JIT.cache_apply cache3 auto trl s1 s2) empty_slot sl1 sl2 tree t + else f empty_slot sl1 sl2 tree t in let cache2 = L2JIT.create () in let rec l2jit_dispatch t tag states ctx opcode = - match opcode with - | L2JIT.RETURN -> nil_res - | L2JIT.CACHE -> - LOG(__ "top-down-run" 3 - "Top-down cache miss for configuration %s %a" - (Tag.to_string tag) StateSet.print states); - let opcode = L2JIT.compile cache2 auto tree tag states in - l2jit_dispatch t tag states ctx opcode - - | L2JIT.LEFT (tr_list, instr) -> - let res1, slot1 = - l2jit_dispatch_instr t (Tree.closing tree t) instr - in - l3jit_dispatch tr_list res1 auto.bottom_states t slot1 empty_slot - - | L2JIT.RIGHT (tr_list, instr) -> - let res2, slot2 = - l2jit_dispatch_instr t ctx instr - in - l3jit_dispatch tr_list auto.bottom_states res2 t empty_slot slot2 - - | L2JIT.BOTH (tr_list, instr1, instr2) -> - let res1, slot1 = - l2jit_dispatch_instr t (Tree.closing tree t) instr1 - in - let res2, slot2 = - l2jit_dispatch_instr t ctx instr2 - in - l3jit_dispatch tr_list res1 res2 t slot1 slot2 + match opcode with + | L2JIT.RETURN -> nil_res + | L2JIT.CACHE -> + LOG(__ "top-down-run" 3 + "Top-down cache miss for configuration %s %a" + (Tag.to_string tag) StateSet.print states); + let opcode = L2JIT.compile cache2 auto tree tag states in + l2jit_dispatch t tag states ctx opcode + + | L2JIT.LEFT (tr_list, instr) -> + let res1, slot1 = + l2jit_dispatch_instr t (Tree.closing tree t) instr + in + l3jit_dispatch tr_list res1 auto.bottom_states t slot1 empty_slot + + | L2JIT.RIGHT (tr_list, instr) -> + let res2, slot2 = + l2jit_dispatch_instr t ctx instr + in + l3jit_dispatch tr_list auto.bottom_states res2 t empty_slot slot2 + + | L2JIT.BOTH (tr_list, instr1, instr2) -> + let res2, slot2 = + l2jit_dispatch_instr t ctx instr2 + in + let res1, slot1 = + l2jit_dispatch_instr t (Tree.closing tree t) instr1 + in + l3jit_dispatch tr_list res1 res2 t slot1 slot2 and l2jit_dispatch_instr t ctx instr = let () = LOG(__ "top-down-run" 3 "Dispatching instr: %a on node %i (context=%i)" L2JIT.print_jump instr (Node.to_int t) (Node.to_int ctx)) in - match instr with - | L2JIT.NOP () -> nil_res - | L2JIT.FIRST_CHILD s -> LOOP ((Tree.first_child tree t), s, ctx) - | L2JIT.NEXT_SIBLING s -> LOOP ((Tree.next_sibling tree t), s, ctx) + match instr with + | L2JIT.NOP () -> nil_res + | L2JIT.FIRST_CHILD s -> LOOP ((Tree.first_child tree t), s, ctx) + | L2JIT.NEXT_SIBLING s -> LOOP ((Tree.next_sibling tree t), s, ctx) - | L2JIT.FIRST_ELEMENT s -> LOOP ((Tree.first_element tree t), s, ctx) - | L2JIT.NEXT_ELEMENT s -> LOOP ((Tree.next_element tree t), s, ctx) + | L2JIT.FIRST_ELEMENT s -> LOOP ((Tree.first_element tree t), s, ctx) + | L2JIT.NEXT_ELEMENT s -> LOOP ((Tree.next_element tree t), s, ctx) - | L2JIT.TAGGED_DESCENDANT (s, tag) -> - LOOP_TAG ((Tree.tagged_descendant tree t tag), s, tag, ctx) + | L2JIT.TAGGED_DESCENDANT (s, tag) -> + LOOP_TAG ((Tree.tagged_descendant tree t tag), s, tag, ctx) - | L2JIT.TAGGED_FOLLOWING (s, tag) -> - LOOP_TAG((Tree.tagged_following_before tree t tag ctx), s, tag, ctx) + | L2JIT.TAGGED_FOLLOWING (s, tag) -> + LOOP_TAG((Tree.tagged_following_before tree t tag ctx), s, tag, ctx) - | L2JIT.SELECT_DESCENDANT (s, _, us) -> - LOOP((Tree.select_descendant tree t us), s, ctx) + | L2JIT.SELECT_DESCENDANT (s, _, us) -> + LOOP((Tree.select_descendant tree t us), s, ctx) - | L2JIT.SELECT_FOLLOWING (s, pt, us) -> - LOOP ((Tree.select_following_before tree t us ctx), s, ctx) + | L2JIT.SELECT_FOLLOWING (s, pt, us) -> + LOOP ((Tree.select_following_before tree t us ctx), s, ctx) - | L2JIT.TAGGED_CHILD (s, tag) -> - LOOP_TAG((Tree.tagged_child tree t tag), s, tag, ctx) + | L2JIT.TAGGED_CHILD (s, tag) -> + LOOP_TAG((Tree.tagged_child tree t tag), s, tag, ctx) - | L2JIT.TAGGED_SIBLING (s, tag) -> - LOOP_TAG((Tree.tagged_sibling tree t tag), s, tag, ctx) + | L2JIT.TAGGED_SIBLING (s, tag) -> + LOOP_TAG((Tree.tagged_sibling tree t tag), s, tag, ctx) - | L2JIT.SELECT_CHILD (s, _, us) -> - LOOP ((Tree.select_child tree t us), s, ctx) + | L2JIT.SELECT_CHILD (s, _, us) -> + LOOP ((Tree.select_child tree t us), s, ctx) - | L2JIT.SELECT_SIBLING (s, _, us) -> - LOOP ((Tree.select_sibling tree t us), s, ctx) + | L2JIT.SELECT_SIBLING (s, _, us) -> + LOOP ((Tree.select_sibling tree t us), s, ctx) - | L2JIT.TAGGED_SUBTREE(s, tag) -> - mark_subtree s (U.NS.subtree_tags tree t tag) + | L2JIT.TAGGED_SUBTREE(s, tag) -> + mark_subtree s (U.NS.subtree_tags tree t tag) - | L2JIT.ELEMENT_SUBTREE(s) -> - mark_subtree s (U.NS.subtree_elements tree t) + | L2JIT.ELEMENT_SUBTREE(s) -> + mark_subtree s (U.NS.subtree_elements tree t) in let r = LOOP (root, states, ctx) in (*L3JIT.stats err_formatter cache3; *) @@ -317,13 +317,13 @@ DEFINE LOOP_TAG (t, states, tag, ctx) = ( let rec uniq = function | ([] | [ _ ]) as l -> l | e1 :: ((e2 :: ll) as l) -> if e1 == e2 then uniq l - else e1 :: e2 :: (uniq ll);; + else e1 :: e2 :: (uniq ll);; DEFINE BOTTOM_UP_NEXT(node, rest, stop) = (let ___fs = Tree.first_child tree node in let ___res1 = - if ___fs == Tree.nil then nil_res - else full_top_down_run auto states tree ___fs + if ___fs == Tree.nil then nil_res + else full_top_down_run auto states tree ___fs in move_up node ___res1 true rest stop) @@ -337,62 +337,62 @@ DEFINE BOTTOM_UP_NEXT(node, rest, stop) = let nil_res = auto.bottom_states, empty_slot in let cache = Cache.Lvl3.create 0 L3JIT.dummy in let rec move_up node res is_left rest stop = - if node == stop then res, rest - else - (*let prev_sibling = Tree.prev_sibling tree node in *) - let is_left' = Tree.is_first_child tree node (*prev_sibling == Tree.nil*) in - (*TODO: unsound in case of following-sibling moves - should replace the else by previous_sibling and walk up the sequence of - right child moves *) - let parent = if is_left' then Tree.parent tree node else - let p = Tree.first_child tree (Tree.parent tree node) in - if p < stop then stop else p - in - let (s1, sl1), (s2, sl2), rest' = - if is_left then match rest with - [] -> res, nil_res, rest - | next :: rest' -> - if Tree.is_right_descendant tree node next - then - let res2, rest' = (*bottom_up_next*) BOTTOM_UP_NEXT(next, rest', node) in - res, res2, rest' - else res, nil_res, rest - else - nil_res, res, rest - in - let tag = Tree.tag tree node in - let id1 = Uid.to_int s1.StateSet.Node.id in - let id2 = Uid.to_int s2.StateSet.Node.id in - let code = - let code = Cache.Lvl3.find cache id2 id1 tag in - if code == L3JIT.dummy then - let trl = - StateSet.fold - (fun q acc -> - List.fold_left (fun acc' (labels, tr) -> - if TagSet.mem tag labels - then Translist.cons tr acc' else acc') - acc - (Hashtbl.find auto.trans q) - ) - states - Translist.nil - in - let code = L3JIT.gen_code auto trl s1 s2 in - Cache.Lvl3.add cache id2 id1 tag code; code - else code - in - let res' = code empty_slot sl1 sl2 tree node in - move_up parent res' is_left' rest' stop + if node == stop then res, rest + else + (*let prev_sibling = Tree.prev_sibling tree node in *) + let is_left' = Tree.is_first_child tree node (*prev_sibling == Tree.nil*) in + (*TODO: unsound in case of following-sibling moves + should replace the else by previous_sibling and walk up the sequence of + right child moves *) + let parent = if is_left' then Tree.parent tree node else + let p = Tree.first_child tree (Tree.parent tree node) in + if p < stop then stop else p + in + let (s1, sl1), (s2, sl2), rest' = + if is_left then match rest with + [] -> res, nil_res, rest + | next :: rest' -> + if Tree.is_right_descendant tree node next + then + let res2, rest' = (*bottom_up_next*) BOTTOM_UP_NEXT(next, rest', node) in + res, res2, rest' + else res, nil_res, rest + else + nil_res, res, rest + in + let tag = Tree.tag tree node in + let id1 = Uid.to_int s1.StateSet.Node.id in + let id2 = Uid.to_int s2.StateSet.Node.id in + let code = + let code = Cache.Lvl3.find cache id2 id1 tag in + if code == L3JIT.dummy then + let trl = + StateSet.fold + (fun q acc -> + List.fold_left (fun acc' (labels, tr) -> + if TagSet.mem tag labels + then Translist.cons tr acc' else acc') + acc + (Hashtbl.find auto.trans q) + ) + states + Translist.nil + in + let code = L3JIT.gen_code auto trl s1 s2 in + Cache.Lvl3.add cache id2 id1 tag code; code + else code + in + let res' = code empty_slot sl1 sl2 tree node in + move_up parent res' is_left' rest' stop in let loop_leaves l = - match l with - [] -> nil_res - | node :: ll -> - let res, lll = BOTTOM_UP_NEXT( (*bottom_up_next*) node, ll, Tree.nil) in - if lll <> [] then - Logger.print err_formatter "WARNING: Leftover nodes: %i\n" (List.length lll); - res + match l with + [] -> nil_res + | node :: ll -> + let res, lll = BOTTOM_UP_NEXT( (*bottom_up_next*) node, ll, Tree.nil) in + if lll <> [] then + Logger.print err_formatter "WARNING: Leftover nodes: %i\n" (List.length lll); + res in let _, slot = loop_leaves leaves in slot.(StateSet.min_elt auto.topdown_marking_states) @@ -403,9 +403,9 @@ let get_trans g auto tag states = List.fold_left (fun ((lstates, rstates, tacc) as acc) (ts, trs) -> if TagSet.mem (Tag.translate tag) ts then - if not (TagSet.mem Tag.attribute ts) && Grammar2.is_attribute g tag - then acc - else + if not (TagSet.mem Tag.attribute ts) && Grammar2.is_attribute g tag + then acc + else let _, _, _, phi = Transition.node trs in let l, r = Formula.st phi in (StateSet.union l lstates, @@ -440,27 +440,27 @@ let dispatch_param1 conf id2 y0 y1 = module K_up = struct type t = Grammar2.n_symbol * StateSet.t * StateSet.t * StateSet.t let hash (a,b,c,d) = - HASHINT4 (Node.to_int a, - Uid.to_int b.StateSet.Node.id, - Uid.to_int c.StateSet.Node.id, - Uid.to_int d.StateSet.Node.id) + HASHINT4 (Node.to_int a, + Uid.to_int b.StateSet.Node.id, + Uid.to_int c.StateSet.Node.id, + Uid.to_int d.StateSet.Node.id) let equal (a1, b1, c1, d1) (a2, b2, c2, d2) = - a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 + a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 end module DCache = struct - include Hashtbl.Make(K_down) - let dummy = StateSet.singleton State.dummy - let notfound l = l.(0) == dummy && l.(1) == dummy - let find h k = - try - find h k - with - Not_found -> - let a = [| dummy; dummy |] in - add h k a; - a + include Hashtbl.Make(K_down) + let dummy = StateSet.singleton State.dummy + let notfound l = l.(0) == dummy && l.(1) == dummy + let find h k = + try + find h k + with + Not_found -> + let a = [| dummy; dummy |] in + add h k a; + a end module UCache = Hashtbl.Make(K_up) type result = { @@ -472,16 +472,16 @@ let dispatch_param1 conf id2 y0 y1 = } let mk_empty e = { in0 = StateSet.empty; - in1 = StateSet.empty; - out0 = e; - out1 = e; - main = e + in1 = StateSet.empty; + out0 = e; + out1 = e; + main = e } let mk_nil s v = { - mk_empty (s,v) with - out0 = StateSet.empty,v; - out1 = StateSet.empty,v; + mk_empty (s,v) with + out0 = StateSet.empty,v; + out1 = StateSet.empty,v; } let grammar_run auto g () = @@ -497,140 +497,140 @@ let dispatch_param1 conf id2 y0 y1 = let preorder_counter = ref 0 in let term_array = [| StateSet.empty; StateSet.empty |] in let get_trans tag states = - let c = Cache.Lvl2.find cache2 tag (Uid.to_int states.StateSet.Node.id) in - if c == dummy2 then - let c = get_trans g auto tag states in - begin - Cache.Lvl2.add cache2 tag (Uid.to_int states.StateSet.Node.id) c; - c - end - else c + let c = Cache.Lvl2.find cache2 tag (Uid.to_int states.StateSet.Node.id) in + if c == dummy2 then + let c = get_trans g auto tag states in + begin + Cache.Lvl2.add cache2 tag (Uid.to_int states.StateSet.Node.id) c; + c + end + else c in let lambda = ref 0 in let rec start_loop idx states = - LOG(__ "grammar" 2 "Node %i\n%!" (Node.to_int idx)); - if states == dummy_set then nil_res else - if idx < Node.null then nil_res - else begin - let symbol = Grammar2.start_tag g idx in - let fc = Grammar2.start_first_child g idx in - let ns = Grammar2.start_next_sibling g fc in - if Grammar2.is_terminal g symbol then - let t = Grammar2.terminal symbol in - terminal_loop t states (Grammar2.Leaf (~-1,0,term_array, fc)) (Grammar2.Leaf (~-1,1,term_array, ns)) - else - let nt = Grammar2.non_terminal symbol in - incr lambda; - let lmbd = !lambda in - let y0 = (Grammar2.Leaf (lmbd,0, term_array, fc)) - and y1 = (Grammar2.Leaf (lmbd,1, term_array, ns)) in - rule_loop nt states y0 y1 - end + LOG(__ "grammar" 2 "Node %i\n%!" (Node.to_int idx)); + if states == dummy_set then nil_res else + if idx < Node.null then nil_res + else begin + let symbol = Grammar2.start_tag g idx in + let fc = Grammar2.start_first_child g idx in + let ns = Grammar2.start_next_sibling g fc in + if Grammar2.is_terminal g symbol then + let t = Grammar2.terminal symbol in + terminal_loop t states (Grammar2.Leaf (~-1,0,term_array, fc)) (Grammar2.Leaf (~-1,1,term_array, ns)) + else + let nt = Grammar2.non_terminal symbol in + incr lambda; + let lmbd = !lambda in + let y0 = (Grammar2.Leaf (lmbd,0, term_array, fc)) + and y1 = (Grammar2.Leaf (lmbd,1, term_array, ns)) in + rule_loop nt states y0 y1 + end and rule_loop (t : Grammar2.n_symbol) states y0 y1 = - if t = Node.nil || states == dummy_set then nil_res else - let () = incr rule_counter in - if !rule_counter land 65535 == 0 then begin Gc.minor() end; -(* let k = (t, states) in*) -(* let pstates = DCache.find dcache k in - let notfound = DCache.notfound pstates in *) - let rhs = Grammar2.get_rule g t in - let id1 = Grammar2.get_id1 rhs in - let id2 = Grammar2.get_id2 rhs in - let conf = Grammar2.get_conf rhs in -(* if notfound then*) - let ny0 = dispatch_param0 conf id2 y0 y1 in - let ny1 = dispatch_param1 conf id2 y0 y1 in - let res = dispatch_loop id1 states ny0 ny1 in -(* pstates.(0) <- res.in0; - pstates.(1) <- res.in1; *) - res (* - UCache.add ucache (t, states, fst res.out0, fst res.out1) - res.main; - let h = Hashtbl.create 7 in - for i = 0 to res_len - 1 do - Hashtbl.add h (0, i) (snd res.out0).(i); - Hashtbl.add h (1, i) (snd res.out1).(i); - done; - { res with - main = ((fst res.main), (U.close h (snd res.main))); - } *) + if t = Node.nil || states == dummy_set then nil_res else + let () = incr rule_counter in + if !rule_counter land 65535 == 0 then begin Gc.minor() end; +(* let k = (t, states) in*) +(* let pstates = DCache.find dcache k in + let notfound = DCache.notfound pstates in *) + let rhs = Grammar2.get_rule g t in + let id1 = Grammar2.get_id1 rhs in + let id2 = Grammar2.get_id2 rhs in + let conf = Grammar2.get_conf rhs in +(* if notfound then*) + let ny0 = dispatch_param0 conf id2 y0 y1 in + let ny1 = dispatch_param1 conf id2 y0 y1 in + let res = dispatch_loop id1 states ny0 ny1 in +(* pstates.(0) <- res.in0; + pstates.(1) <- res.in1; *) + res (* + UCache.add ucache (t, states, fst res.out0, fst res.out1) + res.main; + let h = Hashtbl.create 7 in + for i = 0 to res_len - 1 do + Hashtbl.add h (0, i) (snd res.out0).(i); + Hashtbl.add h (1, i) (snd res.out1).(i); + done; + { res with + main = ((fst res.main), (U.close h (snd res.main))); + } *) (* - else - let res0 = partial_loop y0 pstates.(0) in - let res1 = partial_loop y1 pstates.(1) in - let k2 = (t, states, fst res0.main, fst res1.main) in - let s, r = - try - UCache.find ucache k2 - with - Not_found -> - let ores0 = { res0 with main = fst res0.main, U.var 0 (snd res0.main) } - and ores1 = { res1 with main = fst res1.main, U.var 1 (snd res1.main) } - in - let res = dispatch_loop id1 states (Grammar2.Cache (0,ores0)) (Grammar2.Cache (1, ores1)) in - UCache.add ucache k2 res.main; - res.main - in - let h = Hashtbl.create 7 in - for i = 0 to res_len - 1 do - Hashtbl.add h (0, i) (snd res0.main).(i); - Hashtbl.add h (1, i) (snd res1.main).(i); - done; - { in0 = pstates.(0); - in1 = pstates.(1); - out0 = res0.main; - out1 = res1.main; - main = s, U.close h r; - } + else + let res0 = partial_loop y0 pstates.(0) in + let res1 = partial_loop y1 pstates.(1) in + let k2 = (t, states, fst res0.main, fst res1.main) in + let s, r = + try + UCache.find ucache k2 + with + Not_found -> + let ores0 = { res0 with main = fst res0.main, U.var 0 (snd res0.main) } + and ores1 = { res1 with main = fst res1.main, U.var 1 (snd res1.main) } + in + let res = dispatch_loop id1 states (Grammar2.Cache (0,ores0)) (Grammar2.Cache (1, ores1)) in + UCache.add ucache k2 res.main; + res.main + in + let h = Hashtbl.create 7 in + for i = 0 to res_len - 1 do + Hashtbl.add h (0, i) (snd res0.main).(i); + Hashtbl.add h (1, i) (snd res1.main).(i); + done; + { in0 = pstates.(0); + in1 = pstates.(1); + out0 = res0.main; + out1 = res1.main; + main = s, U.close h r; + } *) and dispatch_loop id1 states ny0 ny1 = - if Grammar2.is_non_terminal g id1 then - rule_loop (Grammar2.non_terminal id1) states ny0 ny1 - else - terminal_loop (Grammar2.terminal id1) states ny0 ny1 + if Grammar2.is_non_terminal g id1 then + rule_loop (Grammar2.non_terminal id1) states ny0 ny1 + else + terminal_loop (Grammar2.terminal id1) states ny0 ny1 and terminal_loop (symbol : Grammar2.t_symbol) states y0 y1 = - if symbol == Grammar2.nil_symbol || symbol = Node.nil || states == dummy_set then nil_res else begin - let tag = Grammar2.tag symbol in - let lst, rst, trans = get_trans tag states in - let res0 = partial_loop y0 lst in - let res1 = partial_loop y1 rst in - let s1, slot1 = res0.main - and s2, slot2 = res1.main in - let opcode = L3JIT.find cache3 trans s1 s2 in - let node = Node.of_int !preorder_counter in - incr preorder_counter; - let res = - if opcode == L3JIT.dummy then - (L3JIT.cache_apply cache3 auto trans s1 s2) empty_slot slot1 slot2 (Obj.magic ()) node - else - opcode empty_slot slot1 slot2 (Obj.magic()) (node) - in - { in0 = lst; - in1 = rst; - out0 = res0.main; - out1 = res1.main; - main = res } - end + if symbol == Grammar2.nil_symbol || symbol = Node.nil || states == dummy_set then nil_res else begin + let tag = Grammar2.tag symbol in + let lst, rst, trans = get_trans tag states in + let res0 = partial_loop y0 lst in + let res1 = partial_loop y1 rst in + let s1, slot1 = res0.main + and s2, slot2 = res1.main in + let opcode = L3JIT.find cache3 trans s1 s2 in + let node = Node.of_int !preorder_counter in + incr preorder_counter; + let res = + if opcode == L3JIT.dummy then + (L3JIT.cache_apply cache3 auto trans s1 s2) empty_slot slot1 slot2 (Obj.magic ()) node + else + opcode empty_slot slot1 slot2 (Obj.magic()) (node) + in + { in0 = lst; + in1 = rst; + out0 = res0.main; + out1 = res1.main; + main = res } + end and partial_loop l states = - if l == dummy_leaf then nil_res else - match l with - | Grammar2.Cache (_, r) -> r - | Grammar2.Leaf (_,_, _, id) -> start_loop id states - | Grammar2.Node0 id -> - if (Grammar2.terminal id) == Grammar2.nil_symbol then nil_res - else - rule_loop (Grammar2.non_terminal id) states dummy_leaf dummy_leaf - - | Grammar2.Node1 (id, y0) -> - rule_loop (Grammar2.non_terminal id) states y0 dummy_leaf - | Grammar2.Node2 (id, y0, y1) -> - if Grammar2.is_terminal g id then - terminal_loop (Grammar2.terminal id) states y0 y1 - else - rule_loop (Grammar2.non_terminal id) states y0 y1 + if l == dummy_leaf then nil_res else + match l with + | Grammar2.Cache (_, r) -> r + | Grammar2.Leaf (_,_, _, id) -> start_loop id states + | Grammar2.Node0 id -> + if (Grammar2.terminal id) == Grammar2.nil_symbol then nil_res + else + rule_loop (Grammar2.non_terminal id) states dummy_leaf dummy_leaf + + | Grammar2.Node1 (id, y0) -> + rule_loop (Grammar2.non_terminal id) states y0 dummy_leaf + | Grammar2.Node2 (id, y0, y1) -> + if Grammar2.is_terminal g id then + terminal_loop (Grammar2.terminal id) states y0 y1 + else + rule_loop (Grammar2.non_terminal id) states y0 y1 in let (_, slot) = (start_loop (Node.null) auto.init).main in @@ -645,29 +645,29 @@ let dispatch_param1 conf id2 y0 y1 = let nil_res = auto.bottom_states, empty_slot in let cache3 = L3JIT.create () in let l3jit_dispatch trl s1 s2 t sl1 sl2 = - let f = L3JIT.find cache3 trl s1 s2 in - if f == L3JIT.dummy then (L3JIT.cache_apply cache3 auto trl s1 s2) empty_slot sl1 sl2 tree t - else f empty_slot sl1 sl2 tree t + let f = L3JIT.find cache3 trl s1 s2 in + if f == L3JIT.dummy then (L3JIT.cache_apply cache3 auto trl s1 s2) empty_slot sl1 sl2 tree t + else f empty_slot sl1 sl2 tree t in let dummy = Translist.nil, StateSet.singleton State.dummy, StateSet.singleton State.dummy in let cache2 = Cache.Lvl2.create 512 dummy in let rec loop t states ctx = - if states == StateSet.empty then nil_res - else if t == Tree.nil then (*StateSet.inter states auto.bottom_states, empty_slot *) nil_res - else - let tag = Tree.tag tree t in - - let trans, lstates, rstates = - let c = Cache.Lvl2.find cache2 (Uid.to_int states.StateSet.Node.id) tag in - if c == dummy then - let c = Ata.get_trans auto states tag in - Cache.Lvl2.add cache2 (Uid.to_int states.StateSet.Node.id) tag c; - c - else c - in - let s1, res1 = loop (Tree.first_child tree t) lstates ctx - and s2, res2 = loop (Tree.next_sibling tree t) rstates ctx in - l3jit_dispatch trans s1 s2 t res1 res2 + if states == StateSet.empty then nil_res + else if t == Tree.nil then (*StateSet.inter states auto.bottom_states, empty_slot *) nil_res + else + let tag = Tree.tag tree t in + + let trans, lstates, rstates = + let c = Cache.Lvl2.find cache2 (Uid.to_int states.StateSet.Node.id) tag in + if c == dummy then + let c = Ata.get_trans auto states tag in + Cache.Lvl2.add cache2 (Uid.to_int states.StateSet.Node.id) tag c; + c + else c + in + let s1, res1 = loop (Tree.first_child tree t) lstates ctx + and s2, res2 = loop (Tree.next_sibling tree t) rstates ctx in + l3jit_dispatch trans s1 s2 t res1 res2 in loop root states ctx @@ -682,40 +682,40 @@ let dispatch_param1 conf id2 y0 y1 = let eval_form auto s1 s2 f = let rec loop f = - match Formula.expr f with - | Formula.False | Formula.True | Formula.Pred _ -> f - | Formula.Atom(`Left, b, q) -> - Formula.of_bool (b == (StateSet.mem q s1)) - | Formula.Atom (`Right, b, q) -> - Formula.of_bool(b == (StateSet.mem q s2)) - | Formula.Atom (`Epsilon, _, _) -> assert false - - | Formula.Or(f1, f2) -> - let b1 = loop f1 in - let b2 = loop f2 in - Formula.or_pred b1 b2 - | Formula.And(f1, f2) -> - let b1 = loop f1 in - let b2 = loop f2 in - Formula.and_pred b1 b2 + match Formula.expr f with + | Formula.False | Formula.True | Formula.Pred _ -> f + | Formula.Atom(`Left, b, q) -> + Formula.of_bool (b == (StateSet.mem q s1)) + | Formula.Atom (`Right, b, q) -> + Formula.of_bool(b == (StateSet.mem q s2)) + | Formula.Atom (`Epsilon, _, _) -> assert false + + | Formula.Or(f1, f2) -> + let b1 = loop f1 in + let b2 = loop f2 in + Formula.or_pred b1 b2 + | Formula.And(f1, f2) -> + let b1 = loop f1 in + let b2 = loop f2 in + Formula.and_pred b1 b2 in loop f let eval_trans auto s1 s2 trans = Translist.fold - (fun t ((a_st, mark) as acc)-> - let q, _, m, f = Transition.node t in - let form = eval_form auto s1 s2 f in - match Formula.expr form with - | Formula.True -> StateSet.add q a_st, mark || m - | Formula.False -> acc - | _ -> assert false - ) trans (StateSet.empty, false) + (fun t ((a_st, mark) as acc)-> + let q, _, m, f = Transition.node t in + let form = eval_form auto s1 s2 f in + match Formula.expr form with + | Formula.True -> StateSet.add q a_st, mark || m + | Formula.False -> acc + | _ -> assert false + ) trans (StateSet.empty, false) let set a i v = LOG(__ "twopass" 2 "Setting node %i to state %a\n%!" - i StateSet.print v); + i StateSet.print v); a.(i) <- v let twopass_top_down states_array auto tree root states ctx = @@ -725,45 +725,45 @@ let dispatch_param1 conf id2 y0 y1 = let cache2 = Cache.Lvl2.create 512 dummy2 in let attributes = TagSet.inj_positive (Tree.attribute_tags tree) in let rec loop t states ctx = - if t == Tree.nil then auto.bottom_states - else if states == StateSet.empty then - let () = set states_array (Node.to_int t) auto.bottom_states in - auto.bottom_states - else - let tag = Tree.tag tree t in - LOG(__ "twopass" 2 "Traversing node %i (tag %s) in states %a\n%!" (Node.to_int t) (Tag.to_string tag) - StateSet.print states - ); - let trans, lstates, rstates = - let c = Cache.Lvl2.find cache2 (Uid.to_int states.StateSet.Node.id) tag in - if c == dummy2 then - let c = Ata.get_trans ~attributes:attributes auto states tag in - Cache.Lvl2.add cache2 (Uid.to_int states.StateSet.Node.id) tag c; - c - else c - in - LOG(__ "twopass" 2 "\nTransitions are:\n%!"); - LOG(__ "twopass" 2"\nTransitions are:\n%a\n%!" - Translist.print trans - ); - let s1 = loop (Tree.first_child tree t) lstates ctx - and s2 = loop (Tree.next_sibling tree t) rstates ctx in - let st = - let c = Cache.Lvl3.find cache3 - (Uid.to_int s1.StateSet.Node.id) - (Uid.to_int s2.StateSet.Node.id) - (Uid.to_int trans.Translist.Node.id) - in - if c == dummy3 then - let c, _ = eval_trans auto s1 s2 trans in - Cache.Lvl3.add cache3 - (Uid.to_int s1.StateSet.Node.id) - (Uid.to_int s2.StateSet.Node.id) - (Uid.to_int trans.Translist.Node.id) c;c - else c - in - set states_array (Node.to_int t) st; - st + if t == Tree.nil then auto.bottom_states + else if states == StateSet.empty then + let () = set states_array (Node.to_int t) auto.bottom_states in + auto.bottom_states + else + let tag = Tree.tag tree t in + LOG(__ "twopass" 2 "Traversing node %i (tag %s) in states %a\n%!" (Node.to_int t) (Tag.to_string tag) + StateSet.print states + ); + let trans, lstates, rstates = + let c = Cache.Lvl2.find cache2 (Uid.to_int states.StateSet.Node.id) tag in + if c == dummy2 then + let c = Ata.get_trans ~attributes:attributes auto states tag in + Cache.Lvl2.add cache2 (Uid.to_int states.StateSet.Node.id) tag c; + c + else c + in + LOG(__ "twopass" 2 "\nTransitions are:\n%!"); + LOG(__ "twopass" 2"\nTransitions are:\n%a\n%!" + Translist.print trans + ); + let s1 = loop (Tree.first_child tree t) lstates ctx + and s2 = loop (Tree.next_sibling tree t) rstates ctx in + let st = + let c = Cache.Lvl3.find cache3 + (Uid.to_int s1.StateSet.Node.id) + (Uid.to_int s2.StateSet.Node.id) + (Uid.to_int trans.Translist.Node.id) + in + if c == dummy3 then + let c, _ = eval_trans auto s1 s2 trans in + Cache.Lvl3.add cache3 + (Uid.to_int s1.StateSet.Node.id) + (Uid.to_int s2.StateSet.Node.id) + (Uid.to_int trans.Translist.Node.id) c;c + else c + in + set states_array (Node.to_int t) st; + st in loop root states ctx, (dummy2, cache2) @@ -774,54 +774,54 @@ let dispatch_param1 conf id2 y0 y1 = let attributes = TagSet.inj_positive (Tree.attribute_tags tree) in let cache3 = Cache.Lvl3.create 512 Dummy in let rec loop t states acc = - if states == StateSet.empty || t = Tree.nil then acc - else - let tag = Tree.tag tree t in - let trans, _, _ = - let c = Cache.Lvl2.find cache2 (Uid.to_int states.StateSet.Node.id) tag in - if c == dummy2 then - let c = Ata.get_trans ~attributes:attributes auto states tag in - Cache.Lvl2.add cache2 (Uid.to_int states.StateSet.Node.id) tag c; - c - else c - in - let fs = Tree.first_child tree t in - let ns = Tree.next_sibling tree t in - let s1 = if fs != Tree.nil then states_array.(Node.to_int fs) else auto.bottom_states - and s2 = if ns != Tree.nil then states_array.(Node.to_int ns) else auto.bottom_states - in - let mark = - let c = Cache.Lvl3.find cache3 - (Uid.to_int s1.StateSet.Node.id) - (Uid.to_int s2.StateSet.Node.id) - (Uid.to_int trans.Translist.Node.id) - in - if c == Dummy then - let _, c = eval_trans auto s1 s2 trans in - let c = if c then Mark else Nop in - Cache.Lvl3.add cache3 - (Uid.to_int s1.StateSet.Node.id) - (Uid.to_int s2.StateSet.Node.id) - (Uid.to_int trans.Translist.Node.id) c;c - else c - in - LOG(__ "twopass" 2 "Evaluating node %i (tag %s).\n%!States=%a\n%!" - (Node.to_int t) - (Tag.to_string tag) - StateSet.print states - ); - LOG(__ "twopass" 2 "Translist=%a\nLeft=%a\nRight=%a\nMark=%s\n\n%!" - Translist.print trans - StateSet.print s1 - StateSet.print s2 - (match mark with - Dummy -> "Dummy" - | Mark -> "Mark" - | Nop -> "Nop")); - if mark == Mark then - loop ns s2 (loop fs s1 (U.NS.snoc acc t)) - else - loop ns s2 (loop fs s1 acc) + if states == StateSet.empty || t = Tree.nil then acc + else + let tag = Tree.tag tree t in + let trans, _, _ = + let c = Cache.Lvl2.find cache2 (Uid.to_int states.StateSet.Node.id) tag in + if c == dummy2 then + let c = Ata.get_trans ~attributes:attributes auto states tag in + Cache.Lvl2.add cache2 (Uid.to_int states.StateSet.Node.id) tag c; + c + else c + in + let fs = Tree.first_child tree t in + let ns = Tree.next_sibling tree t in + let s1 = if fs != Tree.nil then states_array.(Node.to_int fs) else auto.bottom_states + and s2 = if ns != Tree.nil then states_array.(Node.to_int ns) else auto.bottom_states + in + let mark = + let c = Cache.Lvl3.find cache3 + (Uid.to_int s1.StateSet.Node.id) + (Uid.to_int s2.StateSet.Node.id) + (Uid.to_int trans.Translist.Node.id) + in + if c == Dummy then + let _, c = eval_trans auto s1 s2 trans in + let c = if c then Mark else Nop in + Cache.Lvl3.add cache3 + (Uid.to_int s1.StateSet.Node.id) + (Uid.to_int s2.StateSet.Node.id) + (Uid.to_int trans.Translist.Node.id) c;c + else c + in + LOG(__ "twopass" 2 "Evaluating node %i (tag %s).\n%!States=%a\n%!" + (Node.to_int t) + (Tag.to_string tag) + StateSet.print states + ); + LOG(__ "twopass" 2 "Translist=%a\nLeft=%a\nRight=%a\nMark=%s\n\n%!" + Translist.print trans + StateSet.print s1 + StateSet.print s2 + (match mark with + Dummy -> "Dummy" + | Mark -> "Mark" + | Nop -> "Nop")); + if mark == Mark then + loop ns s2 (loop fs s1 (U.NS.snoc acc t)) + else + loop ns s2 (loop fs s1 acc) in loop root states U.NS.empty @@ -830,7 +830,7 @@ let dispatch_param1 conf id2 y0 y1 = LOG(__ "twopass" 2 "Creating array of size: %i\n%!" len); let states_array = Array.make len StateSet.empty in let _, cache = - twopass_top_down states_array auto tree root auto.init Tree.nil + twopass_top_down states_array auto tree root auto.init Tree.nil in twopass_top_down_scan states_array cache auto tree root auto.init Tree.nil @@ -844,4 +844,3 @@ let dispatch_param1 conf id2 y0 y1 = end - -- 2.17.1