src/run.ml

   1 (***********************************************************************)
   2 (*                                                                     *)
   3 (*                               TAToo                                 *)
   4 (*                                                                     *)
   5 (*                     Kim Nguyen, LRI UMR8623                         *)
   6 (*                   Université Paris-Sud & CNRS                       *)
   7 (*                                                                     *)
   8 (*  Copyright 2010-2013 Université Paris-Sud and Centre National de la *)
   9 (*  Recherche Scientifique. All rights reserved.  This file is         *)
  10 (*  distributed under the terms of the GNU Lesser General Public       *)
  11 (*  License, with the special exception on linking described in file   *)
  12 (*  ../LICENSE.                                                        *)
  13 (*                                                                     *)
  14 (***********************************************************************)
  15
  16 INCLUDE "utils.ml"
  17 INCLUDE "debug.ml"
  18
  19
  20 module Make (T : Tree.S) =
  21 struct
  22
  23   let int (x : bool) : int = Obj.magic x
  24   let kint (x : Tree.NodeKind.t) : int = Obj.magic x
  25   let summary tree node parent fc ns =
  26     (int (ns != T.nil)) lor
  27       ((int (fc != T.nil)) lsl 1) lor
  28       ((int (node == T.next_sibling tree parent)) lsl 2) lor
  29       ((int (node == T.first_child tree parent)) lsl 3) lor
  30       ((kint (T.kind tree node)) lsl 4)
  31
  32   let has_next_sibling summary : bool = Obj.magic (summary land 1)
  33   let has_first_child summary : bool = Obj.magic ((summary lsr 1) land 1)
  34   let is_next_sibling summary : bool = Obj.magic ((summary lsr 2) land 1)
  35   let is_first_child summary : bool = Obj.magic ((summary lsr 3) land 1)
  36   let kind summary : Tree.NodeKind.t  = Obj.magic (summary lsr 4)
  37
  38
  39   let eval_form phi node_summary f_set n_set p_set s_set =
  40     let rec loop phi =
  41       let open Boolean in
  42       match Ata.Formula.expr phi with
  43         False -> false
  44       | True -> true
  45       | Or (phi1, phi2) -> loop phi1 || loop phi2
  46       | And (phi1, phi2) -> loop phi1 && loop phi2
  47       | Atom (a, b) -> b == Ata.(
  48         match Atom.node a with
  49           Is_first_child -> is_first_child node_summary
  50         | Is_next_sibling -> is_next_sibling node_summary
  51         | Is k -> k == kind node_summary
  52         | Has_first_child -> has_first_child node_summary
  53         | Has_next_sibling -> has_next_sibling node_summary
  54         | Move (m, q) ->
  55           let set =
  56             match m with
  57               `First_child -> f_set
  58             | `Next_sibling -> n_set
  59             | `Parent
  60             | `Previous_sibling -> p_set
  61             | `Stay -> s_set
  62           in
  63           StateSet.mem q set
  64       )
  65     in
  66     loop phi
  67
  68
  69   let eval_trans_aux trans_list node_summary f_set n_set p_set s_set =
  70     let open Ata in
  71     TransList.fold (fun trs acc ->
  72       let q, _ , phi = Transition.node trs in
  73       if eval_form phi node_summary f_set n_set p_set s_set then
  74         StateSet.add q acc
  75       else
  76         acc) trans_list s_set
  77
  78   let eval_trans trans_list node_summary f_set n_set p_set s_set =
  79     let rec loop old_s =
  80
  81       let new_s =
  82         eval_trans_aux trans_list node_summary f_set n_set p_set old_s
  83       in
  84       if new_s == old_s then old_s else loop new_s
  85     in
  86     loop s_set
  87
  88   let dummy_set = StateSet.singleton State.dummy
  89   let count = ref 0
  90   let total = ref 0
  91   let () = at_exit (fun () -> Format.eprintf "Cache miss: %i/%i\n%!" !count !total)
  92
  93   let eval_trans auto cache set tag node_summary f_set n_set p_set s_set =
  94     incr total;
  95     let i = (tag.QName.id :> int) in
  96     let j = node_summary in
  97     let k = (f_set.StateSet.id :> int) in
  98     let l = (n_set.StateSet.id :> int) in
  99     let m = (p_set.StateSet.id :> int) in
 100     let n = (s_set.StateSet.id :> int) in
 101     let res = Cache.N6.find cache i j k l m n in
 102     if res == dummy_set then begin
 103       incr count;
 104       let trans_list = Ata.get_trans auto tag set in
 105       let res = eval_trans trans_list node_summary f_set n_set p_set s_set in
 106       Cache.N6.add cache i j k l m n res;
 107       res
 108     end
 109     else res
 110
 111
 112   let auto_run auto tree prev_nodes td_states bu_states exit_states _i =
 113     if false then
 114       Format.eprintf "Doing a td (with states: %a) and a bu (with states: %a), exit states are: %a @\n@."
 115         StateSet.print td_states
 116         StateSet.print bu_states
 117         StateSet.print exit_states;
 118     let td_cache = Cache.N6.create dummy_set in
 119     let bu_cache = Cache.N6.create dummy_set in
 120     let rec loop res node parent parent_set =
 121       if node == T.nil then StateSet.empty else begin
 122         let set,lset,rset =
 123         if Sequence.is_empty prev_nodes then
 124           StateSet.(empty,empty,empty)
 125         else
 126           let set,lset,rset, node' = Sequence.peek prev_nodes in
 127           if node == node' then begin
 128             ignore (Sequence.pop prev_nodes);
 129             set,lset,rset
 130           end
 131           else
 132             StateSet.(empty,empty,empty)
 133         in
 134         let tag = T.tag tree node in
 135         let first_child = T.first_child tree node in
 136         let next_sibling = T.next_sibling tree node in
 137         let node_summary = summary tree node parent first_child next_sibling in
 138
 139         let status1 =
 140           eval_trans auto td_cache td_states tag node_summary lset rset parent_set set
 141         in
 142         let fcs = loop res first_child node status1 in
 143         let rres = Sequence.create () in
 144         let nss = loop rres next_sibling node status1 in
 145
 146         let status2 =
 147           eval_trans auto bu_cache bu_states tag node_summary fcs nss parent_set status1
 148         in
 149         let mstates = StateSet.inter status2 exit_states in
 150         if false then begin
 151         Format.eprintf "On node %i (tag : %a) status0 = %a, status1 = %a, fcs = %a, nss = %a, par = %a, status2 = %a, mstates = %a@\n@."
 152           (T.preorder tree node)
 153           QName.print tag
 154           StateSet.print set
 155           StateSet.print status1
 156           StateSet.print fcs
 157           StateSet.print nss
 158           StateSet.print parent_set
 159           StateSet.print status2
 160           StateSet.print mstates;
 161         end;
 162         if mstates != StateSet.empty then
 163           Sequence.push_front (mstates,
 164                                StateSet.inter exit_states fcs,
 165                                StateSet.inter exit_states nss, node) res;
 166         Sequence.append res rres;
 167         status2
 168       end
 169     in
 170     let res = Sequence.create () in
 171     ignore (loop res (T.root tree) T.nil StateSet.empty);
 172     if false then Format.eprintf "Finished pass: %i @\n-----------------------@\n@." _i;
 173     res
 174
 175
 176
 177   let prepare_run auto l =
 178     let res = Sequence.create () in
 179     let start = Ata.get_starting_states auto in
 180     Sequence.iter (fun n -> Sequence.push_back (start, StateSet.empty, StateSet.empty, n) res) l;
 181     res
 182
 183
 184   let main_eval auto tree nodes =
 185     let s_nodes = prepare_run auto nodes in
 186
 187     let ranked_states = Ata.get_states_by_rank auto in
 188     let acc = ref s_nodes in
 189     let max_rank = Ata.get_max_rank auto in
 190     for i = 0 to max_rank do
 191       let open Ata in
 192       let { td; bu; exit } = ranked_states.(i) in
 193       acc := auto_run auto tree !acc td bu exit i;
 194       if false then begin
 195         Format.eprintf "Intermediate result is: @\n";
 196         Sequence.iter (fun (s,_,_, n) ->
 197           Format.eprintf "{%a, %i (%a)}  "
 198             StateSet.print s
 199             (T.preorder tree n)
 200             QName.print (T.tag tree n)) !acc;
 201         Format.eprintf "@\n@.";
 202       end
 203
 204     done;
 205     !acc
 206
 207   let eval auto tree nodes =
 208     let res = main_eval auto tree nodes in
 209     let r = Sequence.create () in
 210     Sequence.iter (fun (_,_,_, n) -> Sequence.push_back n r) res;
 211     r
 212
 213   let full_eval auto tree nodes =
 214     let res = main_eval auto tree nodes in
 215     let dummy = Sequence.create () in
 216     let cache = Cache.N1.create dummy in
 217     Sequence.iter (fun (set, _, _, n) ->
 218       StateSet.iter (fun q ->
 219         let qres = Cache.N1.find cache q in
 220         let qres =
 221           if qres == dummy then begin
 222             let s = Sequence.create () in
 223             Cache.N1.add cache q s;
 224             s
 225           end
 226           else qres
 227         in
 228         Sequence.push_back n qres) set )
 229       res;
 230     let l = StateSet.fold (fun q acc ->
 231       let res = Cache.N1.find cache q in
 232       (q, res) :: acc) (Ata.get_selecting_states auto) []
 233     in
 234     List.rev l
 235
 236 end