let int (x : bool) : int = Obj.magic x
let kint (x : Tree.NodeKind.t) : int = Obj.magic x
- let summary tree node parent fc ns =
+ let summary tree node is_first is_next fc ns =
(int (ns != T.nil)) lor
((int (fc != T.nil)) lsl 1) lor
- ((int (node == T.next_sibling tree parent)) lsl 2) lor
- ((int (node == T.first_child tree parent)) lsl 3) lor
+ ((int is_next) lsl 2) lor
+ ((int is_first) lsl 3) lor
((kint (T.kind tree node)) lsl 4)
let has_next_sibling summary : bool = Obj.magic (summary land 1)
let is_first_child summary : bool = Obj.magic ((summary lsr 3) land 1)
let kind summary : Tree.NodeKind.t = Obj.magic (summary lsr 4)
+ let dummy_set = StateSet.singleton State.dummy
+ let dummy_trans_list =
+ Ata.(TransList.cons
+ (Transition.make (State.dummy, QNameSet.empty, Formula.false_))
+ TransList.nil)
+
+ module Run =
+ struct
+ open Bigarray
+ type t = {
+ mutable pass : int;
+ auto : Ata.t;
+ trans_cache : Ata.TransList.t Cache.N2.t;
+ td_cache : StateSet.t Cache.N6.t;
+ bu_cache : StateSet.t Cache.N6.t;
+ mark_cache : (StateSet.t*StateSet.t*StateSet.t) Cache.N4.t;
+ }
+
+ let create a =
+ {
+ pass = 0;
+ auto = a;
+ trans_cache = Cache.N2.create dummy_trans_list;
+ td_cache = Cache.N6.create dummy_set;
+ bu_cache = Cache.N6.create dummy_set;
+ mark_cache = Cache.N4.create (dummy_set,dummy_set,dummy_set);
+ }
+ end
+
let eval_form phi node_summary f_set n_set p_set s_set =
let rec loop phi =
in
loop s_set
- let dummy_set = StateSet.singleton State.dummy
- let count = ref 0
- let total = ref 0
- let () = at_exit (fun () -> Format.eprintf "Cache miss: %i/%i\n%!" !count !total)
-
- let eval_trans auto cache set tag node_summary f_set n_set p_set s_set =
- incr total;
+ let get_trans run tag set =
let i = (tag.QName.id :> int) in
- let j = node_summary in
+ let j = (set.StateSet.id :> int) in
+ let res = Cache.N2.find run.Run.trans_cache i j in
+ if res == dummy_trans_list then begin
+ let res = Ata.get_trans run.Run.auto tag set in
+ Cache.N2.add run.Run.trans_cache i j res;
+ res
+ end
+ else
+ res
+
+ let eval_trans run cache set tag node_summary f_set n_set p_set s_set =
+ let i = node_summary in
+ let j = (tag.QName.id :> int) in
let k = (f_set.StateSet.id :> int) in
let l = (n_set.StateSet.id :> int) in
let m = (p_set.StateSet.id :> int) in
let n = (s_set.StateSet.id :> int) in
let res = Cache.N6.find cache i j k l m n in
if res == dummy_set then begin
- incr count;
- let trans_list = Ata.get_trans auto tag set in
+ let trans_list = get_trans run tag set in
let res = eval_trans trans_list node_summary f_set n_set p_set s_set in
Cache.N6.add cache i j k l m n res;
res
end
else res
+ let auto_run run tree prev_nodes td_states bu_states exit_states _i =
+ let exit_id = (exit_states.StateSet.id :> int) in
+ let empty_sets = StateSet.(empty,empty,empty) in
+
+ let mark_node front res node set f_set n_set =
+ let i = (set.StateSet.id :> int) in
+ let j = (f_set.StateSet.id :> int) in
+ let k = (n_set.StateSet.id :> int) in
+ let (mstates, _, _) as block =
+ Cache.N4.find run.Run.mark_cache exit_id i j k
+ in
- let auto_run auto tree prev_nodes td_states bu_states exit_states _i =
- if false then
- Format.eprintf "Doing a td (with states: %a) and a bu (with states: %a), exit states are: %a @\n@."
- StateSet.print td_states
- StateSet.print bu_states
- StateSet.print exit_states;
- let td_cache = Cache.N6.create dummy_set in
- let bu_cache = Cache.N6.create dummy_set in
- let rec loop res node parent parent_set =
+ let mstates, ll, rr =
+ if mstates == dummy_set then begin
+ let r1 = StateSet.inter set exit_states in
+ let r2 = StateSet.inter f_set exit_states in
+ let r3 = StateSet.inter n_set exit_states in
+ let r = r1,r2,r3 in
+ Cache.N4.add run.Run.mark_cache exit_id i j k r;
+ r
+ end
+ else block
+ in
+ if mstates != StateSet.empty then
+ let block = mstates, ll, rr, node in
+ if front then Sequence.push_front block res
+ else Sequence.push_back block res
+ in
+ let rec loop res node is_first is_next parent_set =
if node == T.nil then StateSet.empty else begin
let set,lset,rset =
if Sequence.is_empty prev_nodes then
- StateSet.(empty,empty,empty)
+ empty_sets
else
let set,lset,rset, node' = Sequence.peek prev_nodes in
if node == node' then begin
set,lset,rset
end
else
- StateSet.(empty,empty,empty)
+ empty_sets
in
let tag = T.tag tree node in
let first_child = T.first_child tree node in
let next_sibling = T.next_sibling tree node in
- let node_summary = summary tree node parent first_child next_sibling in
-
+ let node_summary =
+ summary tree node is_first is_next first_child next_sibling
+ in
let status1 =
- eval_trans auto td_cache td_states tag node_summary lset rset parent_set set
+ eval_trans run run.Run.td_cache td_states tag node_summary lset rset parent_set set
in
- let fcs = loop res first_child node status1 in
+ let fcs = loop res first_child true false status1 in
let rres = Sequence.create () in
- let nss = loop rres next_sibling node status1 in
+ let nss = loop rres next_sibling false true status1 in
+ if bu_states == StateSet.empty then (* tail call *) begin
+ mark_node true res node status1 fcs StateSet.empty;
+ Sequence.append res rres;
+ status1
+ end else begin
- let status2 =
- eval_trans auto bu_cache bu_states tag node_summary fcs nss parent_set status1
- in
- let mstates = StateSet.inter status2 exit_states in
- if false then begin
- Format.eprintf "On node %i (tag : %a) status0 = %a, status1 = %a, fcs = %a, nss = %a, par = %a, status2 = %a, mstates = %a@\n@."
- (T.preorder tree node)
- QName.print tag
- StateSet.print set
- StateSet.print status1
- StateSet.print fcs
- StateSet.print nss
- StateSet.print parent_set
- StateSet.print status2
- StateSet.print mstates;
+ let status2 =
+ eval_trans run run.Run.bu_cache bu_states tag node_summary fcs nss parent_set status1
+ in
+ if status2 != StateSet.empty then
+ mark_node true res node status2 fcs nss;
+ Sequence.append res rres;
+ status2
end;
- if mstates != StateSet.empty then
- Sequence.push_front (mstates,
- StateSet.inter exit_states fcs,
- StateSet.inter exit_states nss, node) res;
- Sequence.append res rres;
- status2
end
in
let res = Sequence.create () in
- ignore (loop res (T.root tree) T.nil StateSet.empty);
- if false then Format.eprintf "Finished pass: %i @\n-----------------------@\n@." _i;
+ ignore (loop res (T.root tree) false false StateSet.empty);
res
Sequence.iter (fun n -> Sequence.push_back (start, StateSet.empty, StateSet.empty, n) res) l;
res
+let time f arg msg =
+ let t1 = Unix.gettimeofday () in
+ let r = f arg in
+ let t2 = Unix.gettimeofday () in
+ let time = (t2 -. t1) *. 1000. in
+ Logger.msg `STATS "%s: %fms" msg time;
+ r
+
let main_eval auto tree nodes =
let s_nodes = prepare_run auto nodes in
-
let ranked_states = Ata.get_states_by_rank auto in
let acc = ref s_nodes in
let max_rank = Ata.get_max_rank auto in
+ let run = Run.create auto in
for i = 0 to max_rank do
let open Ata in
let { td; bu; exit } = ranked_states.(i) in
- acc := auto_run auto tree !acc td bu exit i;
- if false then begin
- Format.eprintf "Intermediate result is: @\n";
- Sequence.iter (fun (s,_,_, n) ->
- Format.eprintf "{%a, %i (%a)} "
- StateSet.print s
- (T.preorder tree n)
- QName.print (T.tag tree n)) !acc;
- Format.eprintf "@\n@.";
- end
-
+ run.Run.pass <- i;
+ acc := auto_run run tree !acc td bu exit i;
done;
!acc
+
let eval auto tree nodes =
let res = main_eval auto tree nodes in
let r = Sequence.create () in
Sequence.iter (fun (_,_,_, n) -> Sequence.push_back n r) res;
r
+
let full_eval auto tree nodes =
let res = main_eval auto tree nodes in
let dummy = Sequence.create () in
projects / tatoo.git / commitdiff