From: Kim Nguyễn Date: Thu, 4 Apr 2013 19:16:44 +0000 (+0200) Subject: Merge branch 'master' of ssh://git.nguyen.vg/tatoo X-Git-Tag: v0.1~105 X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=commitdiff_plain;h=974dacbf4f625bfd8ea83db69d6b346050141fea Merge branch 'master' of ssh://git.nguyen.vg/tatoo * 'master' of ssh://git.nguyen.vg/tatoo: Flatten the sources, only leave the XPath module packed. Fix the build script. --- 974dacbf4f625bfd8ea83db69d6b346050141fea diff --cc src/ata.ml index 0000000,08a4308..c01cd50 mode 000000,100644..100644 --- a/src/ata.ml +++ b/src/ata.ml @@@ -1,0 -1,474 +1,492 @@@ + (***********************************************************************) + (* *) + (* 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: ++ Time-stamp: + *) + + INCLUDE "utils.ml" + open Format + + type predicate = | First_child + | Next_sibling + | Parent + | Previous_sibling + | Stay + | Is_first_child + | Is_next_sibling + | Is of (Tree.NodeKind.t) + | Has_first_child + | Has_next_sibling + + let is_move p = match p with + | First_child | Next_sibling + | Parent | Previous_sibling | Stay -> true + | _ -> false + + + type atom = predicate * bool * State.t + + module Atom : (Formula.ATOM with type data = atom) = + struct + + module Node = + struct + type t = atom + let equal n1 n2 = n1 = n2 + let hash n = Hashtbl.hash n + end + + include Hcons.Make(Node) + + let print ppf a = + let p, b, q = a.node in + if not b then fprintf ppf "%s" Pretty.lnot; + match p with + | First_child -> fprintf ppf "FC(%a)" State.print q + | Next_sibling -> fprintf ppf "NS(%a)" State.print q + | Parent -> fprintf ppf "FC%s(%a)" Pretty.inverse State.print q + | Previous_sibling -> fprintf ppf "NS%s(%a)" Pretty.inverse State.print q + | Stay -> fprintf ppf "%s(%a)" Pretty.epsilon State.print q + | Is_first_child -> fprintf ppf "FC%s?" Pretty.inverse + | Is_next_sibling -> fprintf ppf "NS%s?" Pretty.inverse + | Is k -> fprintf ppf "is-%a?" Tree.NodeKind.print k + | Has_first_child -> fprintf ppf "FC?" + | Has_next_sibling -> fprintf ppf "NS?" + + let neg a = + let p, b, q = a.node in + make (p, not b, q) + + + end + + module SFormula = + struct + include Formula.Make(Atom) + open Tree.NodeKind + let mk_atom a b c = atom_ (Atom.make (a,b,c)) + let mk_kind k = mk_atom (Is k) true State.dummy + let has_first_child = + (mk_atom Has_first_child true State.dummy) + + let has_next_sibling = + (mk_atom Has_next_sibling true State.dummy) + + let is_first_child = + (mk_atom Is_first_child true State.dummy) + + let is_next_sibling = + (mk_atom Is_next_sibling true State.dummy) + + let is_attribute = + (mk_atom (Is Attribute) true State.dummy) + + let is_element = + (mk_atom (Is Element) true State.dummy) + + let is_processing_instruction = + (mk_atom (Is ProcessingInstruction) true State.dummy) + + let is_comment = + (mk_atom (Is Comment) true State.dummy) + + let first_child q = + and_ + (mk_atom First_child true q) + has_first_child + + let next_sibling q = + and_ + (mk_atom Next_sibling true q) + has_next_sibling + + let parent q = + and_ + (mk_atom Parent true q) + is_first_child + + let previous_sibling q = + and_ + (mk_atom Previous_sibling true q) + is_next_sibling + + let stay q = + (mk_atom Stay true q) + + let get_states phi = + fold (fun phi acc -> + match expr phi with + | Formula.Atom a -> let _, _, q = Atom.node a in + if q != State.dummy then StateSet.add q acc else acc + | _ -> acc + ) phi StateSet.empty + + end + + + module Transition = Hcons.Make (struct + type t = State.t * QNameSet.t * SFormula.t + let equal (a, b, c) (d, e, f) = + a == d && b == e && c == f + let hash (a, b, c) = + 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 -> ?sep:string -> t -> unit + end = + struct + include Hlist.Make(Transition) + let print ppf ?(sep="\n") l = + iter (fun t -> + let q, lab, f = Transition.node t in + fprintf ppf "%a, %a -> %a%s" State.print q QNameSet.print lab SFormula.print f sep) l + 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; + 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 create s ss = ++ let auto = { id = next (); ++ states = s; ++ selection_states = ss; ++ transitions = Hashtbl.create 17; ++ cache2 = Cache.N2.create dummy2; ++ cache6 = Cache.N6.create dummy6; ++ } ++ in ++ at_exit (fun () -> ++ let n6 = ref 0 in ++ let n2 = ref 0 in ++ Cache.N2.iteri (fun _ _ _ b -> if b then incr n2) auto.cache2; ++ Cache.N6.iteri (fun _ _ _ _ _ _ _ b -> if b then incr n6) auto.cache6; ++ Format.eprintf "INFO: automaton %i, cache2: %i entries, cache6: %i entries\n%!" ++ (auto.id :> int) !n2 !n6; ++ let c2l, c2u = Cache.N2.stats auto.cache2 in ++ let c6l, c6u = Cache.N6.stats auto.cache6 in ++ Format.eprintf "INFO: cache2: length: %i, used: %i, occupation: %f\n%!" c2l c2u (float c2u /. float c2l); ++ Format.eprintf "INFO: cache6: length: %i, used: %i, occupation: %f\n%!" c6l c6u (float c6u /. float c6l) ++ ++ ); ++ auto + + 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 + List.fold_left (fun acc1 (labs, phi) -> + if QNameSet.mem tag labs then TransList.cons (Transition.make (q, labs, phi)) acc1 else acc1) acc0 trs + 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.True | Formula.False -> phi + | Formula.Atom a -> - let p, b, q = Atom.node a in - let pos = ++ let p, b, q = Atom.node a in begin + 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 ++ | First_child -> ++ if b == StateSet.mem q fcs then SFormula.true_ else phi ++ | Next_sibling -> ++ if b == StateSet.mem q nss then SFormula.true_ else phi ++ | Parent | Previous_sibling -> ++ if b == StateSet.mem q ps then SFormula.true_ else phi ++ | Stay -> ++ if b == StateSet.mem q ss then SFormula.true_ else phi ++ | Is_first_child -> SFormula.of_bool (b == is_left) ++ | Is_next_sibling -> SFormula.of_bool (b == is_right) ++ | Is k -> SFormula.of_bool (b == (k == kind)) ++ | Has_first_child -> SFormula.of_bool (b == has_left) ++ | Has_next_sibling -> SFormula.of_bool (b == has_right) ++ end ++ | Formula.And(phi1, phi2) -> SFormula.and_ (loop phi1) (loop phi2) ++ | Formula.Or (phi1, phi2) -> SFormula.or_ (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 ++ let n = 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 - ++ 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 i = (ltrs.TransList.id :> int) ++ and j = (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 ++ let q, lab, 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 ++ let new_phi = ++ eval_form ++ phi fcs nss ps accs ++ is_left is_right has_left has_right kind ++ in ++ if SFormula.is_true new_phi then + (acct, StateSet.add q accs) ++ else if SFormula.is_false new_phi then ++ (acct, accs) + else - (TransList.cons trs acct, accs) ++ let new_tr = Transition.make (q, lab, new_phi) in ++ (TransList.cons new_tr 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 + *) + + let add_trans a q s f = + let trs = try Hashtbl.find a.transitions q with Not_found -> [] in + let cup, ntrs = + List.fold_left (fun (acup, atrs) (labs, phi) -> + let lab1 = QNameSet.inter labs s in + let lab2 = QNameSet.diff labs s in + let tr1 = + if QNameSet.is_empty lab1 then [] + else [ (lab1, SFormula.or_ phi f) ] + in + let tr2 = + if QNameSet.is_empty lab2 then [] + else [ (lab2, SFormula.or_ phi f) ] + in + (QNameSet.union acup labs, tr1@ tr2 @ atrs) + ) (QNameSet.empty, []) trs + in + let rem = QNameSet.diff s cup in + let ntrs = if QNameSet.is_empty rem then ntrs + else (rem, f) :: ntrs + in + Hashtbl.replace a.transitions q ntrs + + let _pr_buff = Buffer.create 50 + let _str_fmt = formatter_of_buffer _pr_buff + let _flush_str_fmt () = pp_print_flush _str_fmt (); + let s = Buffer.contents _pr_buff in + Buffer.clear _pr_buff; s + + let print fmt a = + fprintf fmt + "\nInternal UID: %i@\n\ + States: %a@\n\ + Selection states: %a@\n\ + Alternating transitions:@\n" + (a.id :> int) + StateSet.print a.states + StateSet.print a.selection_states; + let trs = + Hashtbl.fold + (fun q t acc -> List.fold_left (fun acc (s , f) -> (q,s,f)::acc) acc t) + a.transitions + [] + in + let sorted_trs = List.stable_sort (fun (q1, s1, _) (q2, s2, _) -> + let c = State.compare q1 q2 in - (if c == 0 then QNameSet.compare s1 s2 else c)) + trs + in + let _ = _flush_str_fmt () in + let strs_strings, max_pre, max_all = List.fold_left (fun (accl, accp, acca) (q, s, f) -> + let s1 = State.print _str_fmt q; _flush_str_fmt () in + let s2 = QNameSet.print _str_fmt s; _flush_str_fmt () in + let s3 = SFormula.print _str_fmt f; _flush_str_fmt () in + let pre = Pretty.length s1 + Pretty.length s2 in + let all = Pretty.length s3 in + ( (q, s1, s2, s3) :: accl, max accp pre, max acca all) + ) ([], 0, 0) sorted_trs + in + let line = Pretty.line (max_all + max_pre + 6) in + let prev_q = ref State.dummy in + List.iter (fun (q, s1, s2, s3) -> + if !prev_q != q && !prev_q != State.dummy then fprintf fmt " %s\n%!" line; + prev_q := q; + fprintf fmt " %s, %s" s1 s2; + fprintf fmt "%s" (Pretty.padding (max_pre - Pretty.length s1 - Pretty.length s2)); + fprintf fmt " %s %s@\n%!" Pretty.right_arrow s3; + ) strs_strings; + fprintf fmt " %s\n%!" line + + (* + [complete transitions a] ensures that for each state q + and each symbols s in the alphabet, a transition q, s exists. + (adding q, s -> F when necessary). + *) + + let complete_transitions a = + StateSet.iter (fun q -> + let qtrans = Hashtbl.find a.transitions q in + let rem = + List.fold_left (fun rem (labels, _) -> + QNameSet.diff rem labels) QNameSet.any qtrans + in + let nqtrans = + if QNameSet.is_empty rem then qtrans + else + (rem, SFormula.false_) :: qtrans + in + Hashtbl.replace a.transitions q nqtrans + ) a.states + + let cleanup_states a = + let memo = ref StateSet.empty in + let rec loop q = + if not (StateSet.mem q !memo) then begin + memo := StateSet.add q !memo; + let trs = try Hashtbl.find a.transitions q with Not_found -> [] in + List.iter (fun (_, phi) -> + StateSet.iter loop (SFormula.get_states phi)) trs + end + in + StateSet.iter loop a.selection_states; + let unused = StateSet.diff a.states !memo in + eprintf "Unused states %a\n%!" StateSet.print unused; + StateSet.iter (fun q -> Hashtbl.remove a.transitions q) unused; + a.states <- !memo + + (* [normalize_negations a] removes negative atoms in the formula + complementing the sub-automaton in the negative states. + [TODO check the meaning of negative upward arrows] + *) + + let normalize_negations auto = + eprintf "Automaton before normalize_trans:\n"; + print err_formatter auto; + eprintf "--------------------\n%!"; + + let memo_state = Hashtbl.create 17 in + let todo = Queue.create () in + let rec flip b f = + match SFormula.expr f with + Formula.True | Formula.False -> if b then f else SFormula.not_ f + | Formula.Or(f1, f2) -> (if b then SFormula.or_ else SFormula.and_)(flip b f1) (flip b f2) + | Formula.And(f1, f2) -> (if b then SFormula.and_ else SFormula.or_)(flip b f1) (flip b f2) + | Formula.Atom(a) -> begin + let l, b', q = Atom.node a in + if q == State.dummy then if b then f else SFormula.not_ f + else + if b == b' then begin + (* a appears positively, either no negation or double negation *) + if not (Hashtbl.mem memo_state (q,b)) then Queue.add (q,true) todo; + SFormula.atom_ (Atom.make (l, true, q)) + end else begin + (* need to reverse the atom + either we have a positive state deep below a negation + or we have a negative state in a positive formula + b' = sign of the state + b = sign of the enclosing formula + *) + let not_q = + try + (* does the inverted state of q exist ? *) + Hashtbl.find memo_state (q, false) + with + Not_found -> + (* create a new state and add it to the todo queue *) + let nq = State.make () in + auto.states <- StateSet.add nq auto.states; + Hashtbl.add memo_state (q, false) nq; + Queue.add (q, false) todo; nq + in + SFormula.atom_ (Atom.make (l, true, not_q)) + end + end + in + (* states that are not reachable from a selection stat are not interesting *) + StateSet.iter (fun q -> Queue.add (q, true) todo) auto.selection_states; + + while not (Queue.is_empty todo) do + let (q, b) as key = Queue.pop todo in + let q' = + try + Hashtbl.find memo_state key + with + Not_found -> + let nq = if b then q else + let nq = State.make () in + auto.states <- StateSet.add nq auto.states; + nq + in + Hashtbl.add memo_state key nq; nq + in + let trans = Hashtbl.find auto.transitions q in + let trans' = List.map (fun (lab, f) -> lab, flip b f) trans in + Hashtbl.replace auto.transitions q' trans'; + done; + cleanup_states auto + + diff --cc src/cache.ml index 0000000,abd999e..f9b7457 mode 000000,100644..100644 --- a/src/cache.ml +++ b/src/cache.ml @@@ -1,0 -1,253 +1,323 @@@ + (***********************************************************************) + (* *) + (* 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: ++ Time-stamp: + *) + -let realloc l old_size new_size dummy = - let l' = Array.create new_size dummy in - for i = 0 to (min old_size new_size) - 1 do - Array.unsafe_set l' i (Array.unsafe_get l i); - done; - l' - + module N1 = + struct - type 'a t = { mutable line : 'a array; - dummy : 'a; - mutable offset : int; - } - let create a = { ++ type 'a t = { ++ mutable line : 'a array; ++ dummy : 'a; ++ mutable offset : int; ++ level : int; ++ } ++ type 'a index = int -> 'a ++ let level a = a.level ++ let create_with_level level a = { + line = Array.create 0 a; + dummy = a; + offset = ~-1; - ++ level = level; + } - - let print fmt a = - Format.fprintf fmt "{ offset=%i;\n dummy=_;line=%a \n}\n%!" - a.offset - (Pretty.print_array ~sep:", " (fun fmt x -> - if x==a.dummy then - Format.fprintf fmt "%s" "D" - else - Format.fprintf fmt "%s" "E")) a.line ++ let create a = create_with_level 1 a + + let add a i v = + if a.offset == ~-1 then a.offset <- i; + let offset = a.offset in + let len = Array.length a.line in + if i >= offset && i < offset + len then + a.line.(i - offset) <- v + else + if i < offset then begin (* bottom resize *) + let pad = offset - i in + let nlen = len + pad in - let narray = Array.create nlen a.dummy in ++ let narray = Array.create nlen a.dummy in + for j = 0 to len - 1 do + narray.(j+pad) <- a.line.(j) + done; + a.offset <- i; + a.line <- narray; + narray.(0) <- v; + end else begin (* top resize *) + (* preventively allocate the space for the following elements *) + let nlen = ((i - offset + 1) lsl 1) + 1 in + let narray = Array.create nlen a.dummy in + for j = 0 to len - 1 do + narray.(j) <- a.line.(j); + done; + narray.(i - offset) <- v; + a.line <- narray + end + + let find a i = + let idx = i - a.offset in + let len = Array.length a.line in + if idx >= 0 && idx < len then + Array.unsafe_get a.line idx + else a.dummy + + let dummy a = a.dummy + + let iteri f a = + let line = a.line in + if a.offset == ~-1 then () else + for i = 0 to Array.length line - 1 do + let v = line.(i) in + f (i+a.offset) v (v==a.dummy) + done + - ++ let stats a = ++ let d = dummy a in ++ let len = Array.length a.line in ++ let used = Array.fold_left (fun acc i -> ++ if i != d then acc+1 else acc) 0 a.line ++ in ++ len, used + end + + module N2 = + struct + type 'a t = 'a N1.t N1.t - let create a = - let dummy1 = N1.create a in - N1.create dummy1 ++ let create_with_level level a = ++ let dummy1 = N1.create_with_level (level+1) a in ++ N1.create_with_level level dummy1 ++ ++ let create a = create_with_level 1 a + + let add a i j v = + let line = N1.find a i in - if line == a.N1.dummy then - let nline = N1.create line.N1.dummy in ++ if line == N1.dummy a then ++ let nline = N1.create_with_level (a.N1.level+1) (N1.dummy line) in + N1.add a i nline; + N1.add nline j v + else + N1.add line j v + + + let find a i j = + let v = N1.find a i in + if v == a.N1.dummy then v.N1.dummy + else N1.find v j + + + let dummy c = c.N1.dummy.N1.dummy + + let iteri f a = + let line = a.N1.line in + if a.N1.offset == ~-1 then () else + for i = 0 to Array.length line - 1 do + N1.iteri (f i) line.(i) + done + ++ let stats a = ++ let d = a.N1.dummy in ++ let len, used = ++ Array.fold_left (fun ((alen,aused) as acc) i -> ++ if i != d then ++ let l, u = N1.stats i in ++ (alen+l, aused+u) ++ else ++ acc) (0, 0) a.N1.line ++ in ++ len, used + + end + + module N3 = + struct + type 'a t = 'a N2.t N1.t + - let create a = - let dummy2 = N2.create a in - N1.create dummy2 ++ let create_with_level level a = ++ let dummy2 = N2.create_with_level (level+1) a in ++ N1.create_with_level (level) dummy2 ++ ++ let create a = create_with_level 1 a ++ + + let add a i j k v = + let line = N1.find a i in + if line == a.N1.dummy then - let nline = N1.create line.N1.dummy in ++ let nline = N2.create_with_level (a.N1.level+1) (N2.dummy line) in + N1.add a i nline; + N2.add nline j k v + else + N2.add line j k v + + let find a i j k = + let v = N1.find a i in + if v == a.N1.dummy then N2.dummy v + else N2.find v j k + + + let dummy a = N2.dummy a.N1.dummy + let iteri f a = + let line = a.N1.line in + if a.N1.offset == ~-1 then () else + for i = 0 to Array.length line - 1 do + N2.iteri (f i) line.(i) + done + ++ let stats a = ++ let d = a.N1.dummy in ++ let len, used = ++ Array.fold_left (fun ((alen,aused) as acc) i -> ++ if i != d then ++ let l, u = N2.stats i in ++ (alen+l, aused+u) ++ else ++ acc) (0, 0) a.N1.line ++ in ++ len, used ++ + end + + module N4 = + struct + type 'a t = 'a N3.t N1.t + - let create a = - let dummy3 = N3.create a in - N1.create dummy3 ++ let create_with_level level a = ++ let dummy3 = N3.create_with_level (level+1) a in ++ N1.create_with_level (level) dummy3 ++ ++ let create a = create_with_level 1 a ++ + + let add a i j k l v = + let line = N1.find a i in + if line == N1.dummy a then - let nline = N3.create (N3.dummy line) in ++ let nline = N3.create_with_level (a.N1.level+1) (N3.dummy line) in + N1.add a i nline; + N3.add nline j k l v + else + N3.add line j k l v + + let find a i j k l = + let v = N1.find a i in + if v == (N1.dummy a) then N3.dummy v + else N3.find v j k l + + + let dummy a = N3.dummy (N1.dummy a) + let iteri f a = + N1.iteri (fun i v _ -> + N3.iteri (fun j k l v2 b -> f i j k l v2 b) v ) a + ++ let stats a = ++ let d = a.N1.dummy in ++ let len, used = ++ Array.fold_left (fun ((alen,aused) as acc) i -> ++ if i != d then ++ let l, u = N3.stats i in ++ (alen+l, aused+u) ++ else ++ acc) (0, 0) a.N1.line ++ in ++ len, used ++ + end + + module N5 = + struct + type 'a t = 'a N4.t N1.t + - let create a = - let dummy4 = N4.create a in - N1.create dummy4 ++ ++ let create_with_level level a = ++ let dummy4 = N4.create_with_level (level+1) a in ++ N1.create_with_level level dummy4 ++ ++ let create a = create_with_level 1 a + + let add a i j k l m v = + let line = N1.find a i in + if line == (N1.dummy a) then - let nline = N4.create (N4.dummy line) in ++ let nline = N4.create_with_level (a.N1.level+1) (N4.dummy line) in + N1.add a i nline; + N4.add nline j k l m v + else + N4.add line j k l m v + + let find a i j k l m = + let v = N1.find a i in + if v == (N1.dummy a) then N4.dummy v + else N4.find v j k l m + + + let dummy a = N4.dummy (N1.dummy a) + let iteri f a = + N1.iteri (fun i v _ -> + N4.iteri (fun j k l m v2 b -> f i j k l m v2 b) v + ) a ++ ++ ++ let stats a = ++ let d = a.N1.dummy in ++ let len, used = ++ Array.fold_left (fun ((alen,aused) as acc) i -> ++ if i != d then ++ let l, u = N4.stats i in ++ (alen+l, aused+u) ++ else ++ acc) (0, 0) a.N1.line ++ in ++ len, used ++ + end + + module N6 = + struct + type 'a t = 'a N5.t N1.t + - let create a = - let dummy5 = N5.create a in - N1.create dummy5 ++ let create_with_level level a = ++ let dummy5 = N5.create_with_level (level+1) a in ++ N1.create_with_level (level) dummy5 ++ ++ let create a = create_with_level 1 a + + let add a i j k l m n v = + let line = N1.find a i in + if line == N1.dummy a then - let nline = N5.create (N5.dummy line) in ++ let nline = N5.create_with_level (a.N1.level+1) (N5.dummy line) in + N1.add a i nline; + N5.add nline j k l m n v + else + N5.add line j k l m n v + + let find a i j k l m n = + let v = N1.find a i in + if v == N1.dummy a then N5.dummy v + else N5.find v j k l m n + + + let dummy a = N5.dummy (N1.dummy a) + let iteri f a = + N1.iteri (fun i v _ -> + N5.iteri (fun j k l m n v2 b -> f i j k l m n v2 b) v + ) a ++ ++ let stats a = ++ let d = a.N1.dummy in ++ let len, used = ++ Array.fold_left (fun ((alen,aused) as acc) i -> ++ if i != d then ++ let l, u = N5.stats i in ++ (alen+l, aused+u) ++ else ++ acc) (0, 0) a.N1.line ++ in ++ len, used ++ + end diff --cc src/cache.mli index 0000000,1211935..5827f6c mode 000000,100644..100644 --- a/src/cache.mli +++ b/src/cache.mli @@@ -1,0 -1,81 +1,87 @@@ + (***********************************************************************) + (* *) + (* 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: ++ Time-stamp: + *) + + (** N-dimentional caches *) + + module N1 : + sig + + type 'a t + val create : 'a -> 'a t + val find : 'a t -> int -> 'a + val add : 'a t -> int -> 'a -> unit + val dummy : 'a t -> 'a + val iteri : (int -> 'a -> bool -> unit) -> 'a t -> unit ++ val stats : 'a t -> int*int + end + + module N2: + sig + type 'a t + val create : 'a -> 'a t + val find : 'a t -> int -> int -> 'a + val add : 'a t -> int -> int -> 'a -> unit + val dummy : 'a t -> 'a + val iteri : (int -> int -> 'a -> bool -> unit) -> 'a t -> unit ++ val stats : 'a t -> int*int + end + + module N3 : + sig + type 'a t + val create : 'a -> 'a t + val find : 'a t -> int -> int -> int -> 'a + val add : 'a t -> int -> int -> int -> 'a -> unit + val dummy : 'a t -> 'a + val iteri : (int -> int -> int -> 'a -> bool -> unit) -> 'a t -> unit ++ val stats : 'a t -> int*int + end + + module N4 : + sig + type 'a t + val create : 'a -> 'a t + val find : 'a t -> int -> int -> int -> int -> 'a + val add : 'a t -> int -> int -> int -> int -> 'a -> unit + val dummy : 'a t -> 'a + val iteri : (int -> int -> int -> int -> 'a -> bool -> unit) -> 'a t -> unit ++ val stats : 'a t -> int*int + end + + module N5 : + sig + type 'a t + val create : 'a -> 'a t + val find : 'a t -> int -> int -> int -> int -> int -> 'a + val add : 'a t -> int -> int -> int -> int -> int -> 'a -> unit + val dummy : 'a t -> 'a + val iteri : (int -> int -> int -> int -> int -> 'a -> bool -> unit) -> 'a t -> unit ++ val stats : 'a t -> int*int + end + + module N6 : + sig + type 'a t + val create : 'a -> 'a t + val find : 'a t -> int -> int -> int -> int -> int -> int -> 'a + val add : 'a t -> int -> int -> int -> int -> int -> int -> 'a -> unit + val dummy : 'a t -> 'a + val iteri : (int -> int -> int -> int -> int -> int -> 'a -> bool -> unit) -> 'a t -> unit ++ val stats : 'a t -> int*int + end diff --cc src/eval.ml index 0000000,206debe..76d9153 mode 000000,100644..100644 --- a/src/eval.ml +++ b/src/eval.ml @@@ -1,0 -1,131 +1,138 @@@ + (***********************************************************************) + (* *) + (* 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: ++ Time-stamp: + *) + + INCLUDE "utils.ml" + open Format + + module Make (T : Tree.S) : + sig + val eval : Ata.t -> T.t -> T.node -> T.node list + end + = struct + + + IFDEF HTMLTRACE + THEN + DEFINE TRACE(e) = (e) + ELSE + DEFINE TRACE(e) = () + END + + + + type cache = StateSet.t Cache.N1.t + let get c t n = Cache.N1.find c (T.preorder t n) + + let set c t n v = Cache.N1.add c (T.preorder t n) v + + + let top_down_run auto tree node cache _i = + let redo = ref false in + let rec loop node = + if node != T.nil then begin + let parent = T.parent tree node in + let fc = T.first_child tree node in + let ns = T.next_sibling tree node in + let tag = T.tag tree node in + let states0 = get cache tree node 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 ~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 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 = + 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 ~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 = + 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 ~sep:"
") trans2) + in + if states2 != states1 then set cache tree node states2; + let () = loop ns in + let _trans3, states3 = + 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 ~sep:"
") _trans3) + in + if states3 != states2 then set cache tree node states3; - if states0 != states3 && (not !redo) then redo := true ++ (*if states0 != states3 && (not !redo) then redo := true *) ++ if (not !redo) ++ && not (Ata.TransList.nil == _trans3) ++ && (states1 != states3) ++ && not (StateSet.intersect states3 auto.Ata.selection_states) ++ then redo := true + end + in + loop node; + !redo + + let get_results auto tree node cache = + let rec loop node acc = + if node == T.nil then acc + else + let acc0 = loop (T.next_sibling tree node) acc in + let acc1 = loop (T.first_child tree node) acc0 in + + if StateSet.intersect (get cache tree node) auto.Ata.selection_states then + node::acc1 + else + acc1 + in + loop node [] + + let eval auto tree node = + let cache = Cache.N1.create StateSet.empty in + let redo = ref true in + let iter = ref 0 in + Ata.reset auto; + while !redo do ++ redo := false; + redo := top_down_run auto tree node cache !iter; + incr iter; + done; ++ at_exit (fun () -> eprintf "INFO: %i iterations\n" !iter); + let r = get_results auto tree node cache in + TRACE(Html.gen_trace (module T : Tree.Sig.S with type t = T.t) (tree)); + r + + end diff --cc src/hcons.ml index 0000000,3fc3e71..cc7327a mode 000000,100644..100644 --- a/src/hcons.ml +++ b/src/hcons.ml @@@ -1,0 -1,84 +1,84 @@@ + (***********************************************************************) + (* *) + (* TAToo *) + (* *) + (* Kim Nguyen, LRI UMR8623 *) + (* Université Paris-Sud & CNRS *) + (* *) + (* Copyright 2010-2012 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: ++ Time-stamp: + *) + + include Hcons_sig + + module type TableBuilder = + functor + (H : Common_sig.HashedType) -> + Common_sig.HashSet with type data = H.t + + module Builder (TB : TableBuilder) (H : Common_sig.HashedType) = + struct + type data = H.t + type t = { id : Uid.t; + hash : int; + node : data } + let uid_make = ref (Uid.make_maker()) + let node t = t.node + let uid t = t.id + let hash t = t.hash + let equal t1 t2 = t1 == t2 + module HN = + struct + type _t = t + type t = _t + let hash = hash + let equal x y = x == y || H.equal x.node y.node + end + module T = TB(HN) + + let pool = T.create 101 + let init () = + T.clear pool; + uid_make := Uid.make_maker () + let dummy x = { id = Uid.dummy; hash = H.hash x; node = x } + + let make x = - let cell = { id = Uid.dummy; hash = H.hash x; node = x } in ++ let cell = dummy x in + try + T.find pool cell + with + | Not_found -> + let cell = { cell with id = !uid_make(); } in + T.add pool cell; + cell + end + + module Make = Builder (Misc.HashSet) + module Weak = Builder (Weak.Make) + + module PosInt = + struct + type data = int + type t = int + let make v = + if v < 0 then raise (Invalid_argument "Hcons.PosInt.make") + else v + + let node v = v + + let hash v = v + + let uid v = Uid.of_int v + let dummy _ = ~-1 + let equal x y = x == y + + let init () = () + end