module Make (T : Tree.S) =
struct
- let eval_form phi tree node fcs nss pars selfs =
+ let int (x : bool) : int = Obj.magic x
+ let kint (x : Tree.NodeKind.t) : int = Obj.magic x
+ let summary tree node is_first is_next fc ns =
+ (int (ns != T.nil)) lor
+ ((int (fc != T.nil)) lsl 1) 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 has_first_child summary : bool = Obj.magic ((summary lsr 1) land 1)
+ let is_next_sibling summary : bool = Obj.magic ((summary lsr 2) 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 =
let open Boolean in
match Ata.Formula.expr phi with
| And (phi1, phi2) -> loop phi1 && loop phi2
| Atom (a, b) -> b == Ata.(
match Atom.node a with
- Is_first_child -> let par = T.parent tree node in
- (T.first_child tree par) == node
- | Is_next_sibling -> let par = T.parent tree node in
- (T.next_sibling tree par) == node
- | Is k -> k == T.kind tree node
- | Has_first_child -> T.nil != T.first_child tree node
- | Has_next_sibling -> T.nil != T.next_sibling tree node
+ Is_first_child -> is_first_child node_summary
+ | Is_next_sibling -> is_next_sibling node_summary
+ | Is k -> k == kind node_summary
+ | Has_first_child -> has_first_child node_summary
+ | Has_next_sibling -> has_next_sibling node_summary
| Move (m, q) ->
let set =
match m with
- `First_child -> fcs
- | `Next_sibling -> nss
+ `First_child -> f_set
+ | `Next_sibling -> n_set
| `Parent
- | `Previous_sibling -> pars
- | `Stay -> selfs
+ | `Previous_sibling -> p_set
+ | `Stay -> s_set
in
StateSet.mem q set
)
loop phi
- let eval_trans_aux trans tree node fcs nss pars selfs =
+ let eval_trans_aux trans_list node_summary f_set n_set p_set s_set =
let open Ata in
TransList.fold (fun trs acc ->
let q, _ , phi = Transition.node trs in
- let res = eval_form phi tree node fcs nss pars selfs in
- if false then begin
- Format.eprintf "Formula %a evaluates to %b with context: (fcs=%a, nss=%a, pars=%a, olds=%a) @\n@."
- Formula.print phi res
- StateSet.print fcs
- StateSet.print nss
- StateSet.print pars
- StateSet.print selfs
- end;
- if res then
+ if eval_form phi node_summary f_set n_set p_set s_set then
StateSet.add q acc
else
- acc) trans selfs
-
- let eval_trans trans tree node fcs nss pars sstates =
- let rec loop olds =
-
- let news = eval_trans_aux trans tree node fcs nss pars olds in
- if false then begin
- Format.eprintf "Saturating formula: olds=%a, news=%a@\n@."
- StateSet.print olds
- StateSet.print news
- end;
- if news == olds then olds else
- loop news
+ acc) trans_list s_set
+
+ let eval_trans trans_list node_summary f_set n_set p_set s_set =
+ let rec loop old_s =
+
+ let new_s =
+ eval_trans_aux trans_list node_summary f_set n_set p_set old_s
+ in
+ if new_s == old_s then old_s else loop new_s
in
- let r = loop sstates in
- if false then begin
- Format.eprintf "Evaluating transitions (fcs=%a, nss=%a, pars=%a, olds=%a):@\n\t%a@."
- StateSet.print fcs
- StateSet.print nss
- StateSet.print pars
- StateSet.print sstates
- (Ata.TransList.print ~sep:"\n\t") trans;
- Format.eprintf "Got %a@\n@." StateSet.print r;
- end;
- r
+ loop s_set
+
+ let get_trans run tag set =
+ let i = (tag.QName.id :> int) 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
+ 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 rec loop res node parset =
+ 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 td_trans = Ata.get_trans auto tag td_states in
- let status1 = eval_trans td_trans tree node lset rset parset set in
- let fcs = loop res (T.first_child tree node) status1 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 is_first is_next first_child next_sibling
+ in
+ let status1 =
+ eval_trans run run.Run.td_cache td_states tag node_summary lset rset parent_set set
+ in
+ let fcs = loop res first_child true false status1 in
let rres = Sequence.create () in
- let nss = loop rres (T.next_sibling tree node) status1 in
- let bu_trans = Ata.get_trans auto tag bu_states in
- let status2 = eval_trans bu_trans tree node fcs nss parset 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 parset
- StateSet.print status2
- StateSet.print mstates;
+ 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 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) 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 / blobdiff