(***********************************************************************) (* *) (* 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. *) (* *) (***********************************************************************) INCLUDE "utils.ml" INCLUDE "debug.ml" module Make (T : Tree.S) = struct let eval_form phi tree node fcs nss pars selfs = let rec loop phi = let open Boolean in match Ata.Formula.expr phi with False -> false | True -> true | Or (phi1, phi2) -> loop phi1 || loop phi2 | 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 | Move (m, q) -> let set = match m with `First_child -> fcs | `Next_sibling -> nss | `Parent | `Previous_sibling -> pars | `Stay -> selfs in StateSet.mem q set ) in loop phi let eval_trans_aux trans tree node fcs nss pars selfs = 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 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 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 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 = if node == T.nil then StateSet.empty else begin let set,lset,rset = if Sequence.is_empty prev_nodes then StateSet.(empty,empty,empty) else let set,lset,rset, node' = Sequence.peek prev_nodes in if node == node' then begin ignore (Sequence.pop prev_nodes); set,lset,rset end else StateSet.(empty,empty,empty) 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 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; 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; res let prepare_run auto l = let res = Sequence.create () in let start = Ata.get_starting_states auto in Sequence.iter (fun n -> Sequence.push_back (start, StateSet.empty, StateSet.empty, n) res) l; res 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 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 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 let cache = Cache.N1.create dummy in Sequence.iter (fun (set, _, _, n) -> StateSet.iter (fun q -> let qres = Cache.N1.find cache q in let qres = if qres == dummy then begin let s = Sequence.create () in Cache.N1.add cache q s; s end else qres in Sequence.push_back n qres) set ) res; let l = StateSet.fold (fun q acc -> let res = Cache.N1.find cache q in (q, res) :: acc) (Ata.get_selecting_states auto) [] in List.rev l end