From 09058e990c86555c9c9211f00639901bbd386730 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Kim=20Nguy=E1=BB=85n?= Date: Fri, 15 Mar 2013 17:31:59 +0100 Subject: [PATCH] Code refactoring: - move the caching tables inside the automaton object - add an interface for the ata module - make the automaton record type private --- src/auto/ata.ml | 148 +++++++++++++++++++++++++++++++++++++------ src/auto/ata.mli | 93 +++++++++++++++++++++++++++ src/auto/eval.ml | 140 +++++++--------------------------------- src/xpath/compile.ml | 6 +- 4 files changed, 246 insertions(+), 141 deletions(-) create mode 100644 src/auto/ata.mli diff --git a/src/auto/ata.ml b/src/auto/ata.ml index 1015513..af729da 100644 --- a/src/auto/ata.ml +++ b/src/auto/ata.ml @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) INCLUDE "utils.ml" @@ -137,21 +137,6 @@ struct end -type t = { - id : Uid.t; - mutable states : StateSet.t; - mutable selection_states: StateSet.t; - transitions: (State.t, (QNameSet.t*SFormula.t) list) Hashtbl.t; -} - -let next = Uid.make_maker () - -let create () = { id = next (); - states = StateSet.empty; - selection_states = StateSet.empty; - transitions = Hashtbl.create 17; - } - module Transition = Hcons.Make (struct type t = State.t * QNameSet.t * SFormula.t @@ -161,19 +146,52 @@ module Transition = Hcons.Make (struct HASHINT4 (PRIME1, a, ((QNameSet.uid b) :> int), ((SFormula.uid c) :> int)) end) + module TransList : sig include Hlist.S with type elt = Transition.t - val print : Format.formatter -> t -> unit + val print : Format.formatter -> ?sep:string -> t -> unit end = struct include Hlist.Make(Transition) - let print ppf l = + let print ppf ?(sep="\n") l = iter (fun t -> let q, lab, f = Transition.node t in - fprintf ppf "%a, %a -> %a
" State.print q QNameSet.print lab SFormula.print f) l + fprintf ppf "%a, %a -> %a%s" State.print q QNameSet.print lab SFormula.print f sep) l end -let get_trans a states tag = + +type t = { + id : Uid.t; + mutable states : StateSet.t; + mutable selection_states: StateSet.t; + transitions: (State.t, (QNameSet.t*SFormula.t) list) Hashtbl.t; + mutable cache2 : TransList.t Cache.N2.t; + mutable cache6 : (TransList.t*StateSet.t) Cache.N6.t; +} + +let next = Uid.make_maker () + +let dummy2 = TransList.cons + (Transition.make (State.dummy,QNameSet.empty, SFormula.false_)) + TransList.nil + +let dummy6 = (dummy2, StateSet.empty) + + +let create s ss = { id = next (); + states = s; + selection_states = ss; + transitions = Hashtbl.create 17; + cache2 = Cache.N2.create dummy2; + cache6 = Cache.N6.create dummy6; + } + +let reset a = + a.cache2 <- Cache.N2.create dummy2; + a.cache6 <- Cache.N6.create dummy6 + + +let get_trans_aux a tag states = StateSet.fold (fun q acc0 -> try let trs = Hashtbl.find a.transitions q in @@ -182,6 +200,96 @@ let get_trans a states tag = with Not_found -> acc0 ) states TransList.nil + +let get_trans a tag states = + let trs = + Cache.N2.find a.cache2 + (tag.QName.id :> int) (states.StateSet.id :> int) + in + if trs == dummy2 then + let trs = get_trans_aux a tag states in + (Cache.N2.add + a.cache2 + (tag.QName.id :> int) + (states.StateSet.id :> int) trs; trs) + else trs + + + +let eval_form phi fcs nss ps ss is_left is_right has_left has_right kind = + let rec loop phi = + begin match SFormula.expr phi with + Formula.True -> true + | Formula.False -> false + | Formula.Atom a -> + let p, b, q = Atom.node a in + let pos = + match p with + | First_child -> StateSet.mem q fcs + | Next_sibling -> StateSet.mem q nss + | Parent | Previous_sibling -> StateSet.mem q ps + | Stay -> StateSet.mem q ss + | Is_first_child -> is_left + | Is_next_sibling -> is_right + | Is k -> k == kind + | Has_first_child -> has_left + | Has_next_sibling -> has_right + in + if is_move p && (not b) then + eprintf "Warning: Invalid negative atom %a" Atom.print a; + b == pos + | Formula.And(phi1, phi2) -> loop phi1 && loop phi2 + | Formula.Or (phi1, phi2) -> loop phi1 || loop phi2 + end + in + loop phi + +let int_of_conf is_left is_right has_left has_right kind = + ((Obj.magic kind) lsl 4) lor + ((Obj.magic is_left) lsl 3) lor + ((Obj.magic is_right) lsl 2) lor + ((Obj.magic has_left) lsl 1) lor + (Obj.magic has_right) + +let eval_trans auto ltrs fcs nss ps ss is_left is_right has_left has_right kind = + let i = int_of_conf is_left is_right has_left has_right kind + and k = (fcs.StateSet.id :> int) + and l = (nss.StateSet.id :> int) + and m = (ps.StateSet.id :> int) + in + + let rec loop ltrs ss = + let j = (ltrs.TransList.id :> int) + and n = (ss.StateSet.id :> int) in + let (new_ltrs, new_ss) as res = + let res = Cache.N6.find auto.cache6 i j k l m n in + if res == dummy6 then + let res = + TransList.fold (fun trs (acct, accs) -> + let q, _, phi = Transition.node trs in + if StateSet.mem q accs then (acct, accs) else + if eval_form + phi fcs nss ps accs + is_left is_right has_left has_right kind + then + (acct, StateSet.add q accs) + else + (TransList.cons trs acct, accs) + ) ltrs (TransList.nil, ss) + in + Cache.N6.add auto.cache6 i j k l m n res; res + else + res + in + if new_ss == ss then res else + loop new_ltrs new_ss + in + loop ltrs ss + + + + + (* [add_trans a q labels f] adds a transition [(q,labels) -> f] to the automaton [a] but ensures that transitions remains pairwise disjoint diff --git a/src/auto/ata.mli b/src/auto/ata.mli new file mode 100644 index 0000000..0ca6e55 --- /dev/null +++ b/src/auto/ata.mli @@ -0,0 +1,93 @@ +(***********************************************************************) +(* *) +(* TAToo *) +(* *) +(* Kim Nguyen, LRI UMR8623 *) +(* Université Paris-Sud & CNRS *) +(* *) +(* Copyright 2010-2013 Université Paris-Sud and Centre National de la *) +(* Recherche Scientifique. All rights reserved. This file is *) +(* distributed under the terms of the GNU Lesser General Public *) +(* License, with the special exception on linking described in file *) +(* ../LICENSE. *) +(* *) +(***********************************************************************) + +(* + Time-stamp: +*) + +type predicate = + First_child + | Next_sibling + | Parent + | Previous_sibling + | Stay + | Is_first_child + | Is_next_sibling + | Is of Tree.Common.NodeKind.t + | Has_first_child + | Has_next_sibling + +val is_move : predicate -> bool + +type atom = predicate * bool * State.t + +module Atom : Formula.ATOM with type data = atom + +module SFormula : + sig + include module type of Formula.Make(Atom) + val mk_atom : predicate -> bool -> State.t -> t + val mk_kind : Tree.Common.NodeKind.t -> t + val has_first_child : t + val has_next_sibling : t + val is_first_child : t + val is_next_sibling : t + val is_attribute : t + val is_element : t + val is_processing_instruction : t + val is_comment : t + val first_child : State.t -> t + val next_sibling : State.t -> t + val parent : State.t -> t + val previous_sibling : State.t -> t + val stay : State.t -> t + val get_states : t -> StateSet.t + end + + +module Transition : Utils.Hcons.S with + type data = State.t * Utils.QNameSet.t * SFormula.t + +module TransList : sig + include Utils.Hlist.S with type elt = Transition.t + val print : Format.formatter -> ?sep:string -> t -> unit +end + + +type t = private { + id : Utils.Uid.t; + mutable states : StateSet.t; + mutable selection_states: StateSet.t; + transitions: (State.t, (Utils.QNameSet.t*SFormula.t) list) Hashtbl.t; + mutable cache2 : TransList.t Utils.Cache.N2.t; + mutable cache6 : (TransList.t*StateSet.t) Utils.Cache.N6.t; +} + + + +val create : StateSet.t -> StateSet.t -> t +val reset : t -> unit +val get_trans : t -> Utils.QNameSet.elt -> StateSet.t -> TransList.t + +val eval_trans : t -> TransList.t + -> StateSet.t -> StateSet.t -> StateSet.t -> StateSet.t + -> bool -> bool -> bool -> bool -> Tree.Common.NodeKind.t + -> TransList.t*StateSet.t + +val add_trans : t -> State.t -> Utils.QNameSet.t -> SFormula.t -> unit +val print : Format.formatter -> t -> unit +val complete_transitions : t -> unit +val cleanup_states : t -> unit +val normalize_negations : t -> unit diff --git a/src/auto/eval.ml b/src/auto/eval.ml index 3192773..4a27fa5 100644 --- a/src/auto/eval.ml +++ b/src/auto/eval.ml @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) INCLUDE "utils.ml" @@ -42,81 +42,8 @@ END let set c t n v = Cache.N1.add c (T.preorder t n) v - module Info = struct - type t = { is_left : bool; - is_right : bool; - has_left : bool; - has_right : bool; - kind : Tree.Common.NodeKind.t; - } - let equal a b = a = b - let hash a = Hashtbl.hash a - end - - module NodeInfo = Hcons.Make(Info) - - let eval_form phi node_info fcs nss ps ss = - let open NodeInfo in - let open Info in - let rec loop phi = - begin match Ata.SFormula.expr phi with - Formula.True -> true - | Formula.False -> false - | Formula.Atom a -> - let p, b, q = Ata.Atom.node a in - let pos = - let open Ata in - match p with - | First_child -> StateSet.mem q fcs - | Next_sibling -> StateSet.mem q nss - | Parent | Previous_sibling -> StateSet.mem q ps - | Stay -> StateSet.mem q ss - | Is_first_child -> node_info.node.is_left - | Is_next_sibling -> node_info.node.is_right - | Is k -> k == node_info.node.kind - | Has_first_child -> node_info.node.has_left - | Has_next_sibling -> node_info.node.has_right - in - if Ata.is_move p && (not b) then - eprintf "Warning: Invalid negative atom %a" Ata.Atom.print a; - b == pos - | Formula.And(phi1, phi2) -> loop phi1 && loop phi2 - | Formula.Or (phi1, phi2) -> loop phi1 || loop phi2 - end - in - loop phi - - let eval_trans cache ltrs node_info fcs nss ps ss = - let j = (node_info.NodeInfo.id :> int) - and k = (fcs.StateSet.id :> int) - and l = (nss.StateSet.id :> int) - and m = (ps.StateSet.id :> int) in - let rec loop ltrs ss = - let i = (ltrs.Ata.TransList.id :> int) - and n = (ss.StateSet.id :> int) in - let (new_ltrs, new_ss) as res = - let res = Cache.N6.find cache i j k l m n in - if res == Cache.N6.dummy cache then - let res = - Ata.TransList.fold (fun trs (acct, accs) -> - let q, _, phi = Ata.Transition.node trs in - if StateSet.mem q accs then (acct, accs) else - if eval_form phi node_info fcs nss ps accs then - (acct, StateSet.add q accs) - else - (Ata.TransList.cons trs acct, accs) - ) ltrs (Ata.TransList.nil, ss) - in - Cache.N6.add cache i j k l m n res; res - else - res - in - if new_ss == ss then res else - loop new_ltrs new_ss - in - loop ltrs ss - let top_down_run auto tree node cache trans_cache2 trans_cache6 _i = + let top_down_run auto tree node cache _i = let redo = ref false in let rec loop node = if node != T.nil then begin @@ -125,55 +52,48 @@ END let ns = T.next_sibling tree node in let tag = T.tag tree node in let states0 = get cache tree node in - let trans0 = - let trs = - Cache.N2.find trans_cache2 - (tag.QName.id :> int) (auto.Ata.states.StateSet.id :> int) - in - if trs == Cache.N2.dummy trans_cache2 then - let trs = Ata.get_trans auto auto.Ata.states tag in - (Cache.N2.add - trans_cache2 - (tag.QName.id :> int) - (auto.Ata.states.StateSet.id :> int) trs; trs) - else trs - in + let trans0 = Ata.get_trans auto tag auto.Ata.states in let () = TRACE(Html.trace (T.preorder tree node) _i "Pre States: %a
Pre Trans: %a
" - StateSet.print states0 Ata.TransList.print trans0) + StateSet.print states0 (Ata.TransList.print ~sep:"
") trans0) in let ps = get cache tree parent in let fcs = get cache tree fc in let nss = get cache tree ns in - let node_info = NodeInfo.make - (Info.({ is_left = node == T.first_child tree parent; - is_right = node == T.next_sibling tree parent; - has_left = fc != T.nil; - has_right = ns != T.nil; - kind = T.kind tree node })) + let is_left = node == T.first_child tree parent + and is_right = node == T.next_sibling tree parent + and has_left = fc != T.nil + and has_right = ns != T.nil + and kind = T.kind tree node in let trans1, states1 = - eval_trans trans_cache6 trans0 node_info fcs nss ps states0 + Ata.eval_trans auto trans0 + fcs nss ps states0 + is_left is_right has_left has_right kind in let () = - TRACE(Html.trace (T.preorder tree node) _i "TD States: %a
TD Trans: %a
" StateSet.print states1 Ata.TransList.print trans1) + TRACE(Html.trace (T.preorder tree node) _i "TD States: %a
TD Trans: %a
" StateSet.print states1 (Ata.TransList.print ~sep:"
") trans1) in if states1 != states0 then set cache tree node states1; let () = loop fc in let fcs1 = get cache tree fc in let trans2, states2 = - eval_trans trans_cache6 trans1 node_info fcs1 nss ps states1 + Ata.eval_trans auto trans1 + fcs1 nss ps states1 + is_left is_right has_left has_right kind in let () = - TRACE(Html.trace (T.preorder tree node) _i "Left BU States: %a
Left BU Trans: %a
" StateSet.print states2 Ata.TransList.print trans2) + TRACE(Html.trace (T.preorder tree node) _i "Left BU States: %a
Left BU Trans: %a
" StateSet.print states2 (Ata.TransList.print ~sep:"
") trans2) in if states2 != states1 then set cache tree node states2; let () = loop ns in let _trans3, states3 = - eval_trans trans_cache6 trans2 node_info fcs1 (get cache tree ns) ps states2 + Ata.eval_trans auto trans2 + fcs1 (get cache tree ns) ps states2 + is_left is_right has_left has_right kind in let () = - TRACE(Html.trace (T.preorder tree node) _i "Right BU States: %a
Right BU Trans: %a
" StateSet.print states3 Ata.TransList.print _trans3) + TRACE(Html.trace (T.preorder tree node) _i "Right BU States: %a
Right BU Trans: %a
" StateSet.print states3 (Ata.TransList.print ~sep:"
") _trans3) in if states3 != states2 then set cache tree node states3; if states0 != states3 && (not !redo) then redo := true @@ -200,23 +120,9 @@ END let cache = Cache.N1.create StateSet.empty in let redo = ref true in let iter = ref 0 in - let dummy2 = Ata.TransList.cons - (Ata.Transition.make (State.dummy,QNameSet.empty, Ata.SFormula.false_)) - Ata.TransList.nil - in - let dummy6 = (dummy2, StateSet.empty) in - let trans_cache6 = Cache.N6.create dummy6 in - let trans_cache2 = Cache.N2.create dummy2 in - let () = at_exit (fun () -> - let num_phi = ref 0 in - let num_trans = ref 0 in - Cache.N6.iteri (fun _ _ _ _ _ _ _ b -> if not b then incr num_phi) trans_cache6; - Cache.N2.iteri (fun _ _ _ b -> if not b then incr num_trans) trans_cache2; - Format.eprintf "PROFILE:materialized %i transitions and %i configurations\n@." !num_trans !num_phi - ) - in + Ata.reset auto; while !redo do - redo := top_down_run auto tree node cache trans_cache2 trans_cache6 !iter; + redo := top_down_run auto tree node cache !iter; incr iter; done; let r = get_results auto tree node cache in diff --git a/src/xpath/compile.ml b/src/xpath/compile.ml index 2588432..0038506 100644 --- a/src/xpath/compile.ml +++ b/src/xpath/compile.ml @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) open Ast @@ -235,9 +235,7 @@ let path p = in (StateSet.add ms ams), natrs, nasts) (StateSet.empty, [], StateSet.empty) p in - let a = Ata.create () in - a.Ata.states <- states; - a.Ata.selection_states <- mstates; + let a = Ata.create states mstates in List.iter (fun (q, l) -> List.iter (fun (lab, phi) -> Ata.add_trans a q lab phi -- 2.17.1