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 eval_form phi tree node fcs nss pars selfs =
  24     let rec loop phi =
  25       let open Boolean in
  26       match Ata.Formula.expr phi with
  27         False -> false
  28       | True -> true
  29       | Or (phi1, phi2) -> loop phi1 || loop phi2
  30       | And (phi1, phi2) -> loop phi1 && loop phi2
  31       | Atom (a, b) -> b == Ata.(
  32         match Atom.node a with
  33           Is_first_child -> let par = T.parent tree node in
  34                            (T.first_child tree par) == node
  35         | Is_next_sibling -> let par = T.parent tree node in
  36                             (T.next_sibling tree par) == node
  37         | Is k -> k == T.kind tree node
  38         | Has_first_child -> T.nil != T.first_child tree node
  39         | Has_next_sibling -> T.nil != T.next_sibling tree node
  40         | Move (m, q) ->
  41           let set =
  42             match m with
  43               `First_child -> fcs
  44             | `Next_sibling -> nss
  45             | `Parent
  46             | `Previous_sibling -> pars
  47             | `Stay -> selfs
  48           in
  49           StateSet.mem q set
  50       )
  51     in
  52     loop phi
  53
  54
  55   let eval_trans_aux trans tree node fcs nss pars selfs =
  56     let open Ata in
  57     TransList.fold (fun trs acc ->
  58       let q, _ , phi = Transition.node trs in
  59       let res = eval_form phi tree node fcs nss pars selfs in
  60       if false then begin
  61       Format.eprintf "Formula %a evaluates to %b with context: (fcs=%a, nss=%a, pars=%a, olds=%a) @\n@."
  62         Formula.print phi res
  63         StateSet.print fcs
  64         StateSet.print nss
  65         StateSet.print pars
  66         StateSet.print selfs
  67       end;
  68       if res then
  69         StateSet.add q acc
  70       else
  71         acc) trans selfs
  72
  73   let eval_trans trans tree node fcs nss pars sstates =
  74     let rec loop olds =
  75
  76       let news = eval_trans_aux trans tree node fcs nss pars olds in
  77       if false then begin
  78         Format.eprintf "Saturating formula: olds=%a, news=%a@\n@."
  79         StateSet.print olds
  80         StateSet.print news
  81       end;
  82       if news == olds then olds else
  83         loop news
  84     in
  85     let r = loop sstates in
  86     if false then begin
  87       Format.eprintf "Evaluating transitions (fcs=%a, nss=%a, pars=%a, olds=%a):@\n\t%a@."
  88       StateSet.print fcs
  89       StateSet.print nss
  90       StateSet.print pars
  91       StateSet.print sstates
  92       (Ata.TransList.print ~sep:"\n\t") trans;
  93     Format.eprintf "Got %a@\n@." StateSet.print r;
  94     end;
  95     r
  96
  97
  98   let auto_run auto tree prev_nodes td_states bu_states exit_states _i =
  99     if false then
 100       Format.eprintf "Doing a td (with states: %a) and a bu (with states: %a), exit states are: %a @\n@."
 101         StateSet.print td_states
 102         StateSet.print bu_states
 103         StateSet.print exit_states;
 104     let rec loop res node parset =
 105       if node == T.nil then StateSet.empty else begin
 106         let set,lset,rset =
 107         if Sequence.is_empty prev_nodes then
 108           StateSet.(empty,empty,empty)
 109         else
 110           let set,lset,rset, node' = Sequence.peek prev_nodes in
 111           if node == node' then begin
 112             ignore (Sequence.pop prev_nodes);
 113             set,lset,rset
 114           end
 115           else
 116             StateSet.(empty,empty,empty)
 117         in
 118         let tag = T.tag tree node in
 119         let td_trans = Ata.get_trans auto tag td_states in
 120         let status1 = eval_trans td_trans tree node lset rset parset set in
 121         let fcs = loop res (T.first_child tree node) status1 in
 122         let rres = Sequence.create () in
 123         let nss = loop rres (T.next_sibling tree node) status1 in
 124         let bu_trans = Ata.get_trans auto tag bu_states in
 125         let status2 = eval_trans bu_trans tree node fcs nss parset status1 in
 126         let mstates = StateSet.inter status2 exit_states in
 127         if false then begin
 128         Format.eprintf "On node %i (tag : %a) status0 = %a, status1 = %a, fcs = %a, nss = %a, par = %a, status2 = %a, mstates = %a@\n@."
 129           (T.preorder tree node)
 130           QName.print tag
 131           StateSet.print set
 132           StateSet.print status1
 133           StateSet.print fcs
 134           StateSet.print nss
 135           StateSet.print parset
 136           StateSet.print status2
 137           StateSet.print mstates;
 138         end;
 139         if mstates != StateSet.empty then
 140           Sequence.push_front (mstates,
 141                                StateSet.inter exit_states fcs,
 142                                StateSet.inter exit_states nss, node) res;
 143         Sequence.append res rres;
 144         status2
 145       end
 146     in
 147     let res = Sequence.create () in
 148     ignore (loop res (T.root tree) StateSet.empty);
 149     if false then Format.eprintf "Finished pass: %i @\n-----------------------@\n@." _i;
 150     res
 151
 152
 153
 154   let prepare_run auto l =
 155     let res = Sequence.create () in
 156     let start = Ata.get_starting_states auto in
 157     Sequence.iter (fun n -> Sequence.push_back (start, StateSet.empty, StateSet.empty, n) res) l;
 158     res
 159
 160
 161   let main_eval auto tree nodes =
 162     let s_nodes = prepare_run auto nodes in
 163
 164     let ranked_states = Ata.get_states_by_rank auto in
 165     let acc = ref s_nodes in
 166     let max_rank = Ata.get_max_rank auto in
 167     for i = 0 to max_rank do
 168       let open Ata in
 169       let { td; bu; exit } = ranked_states.(i) in
 170       acc := auto_run auto tree !acc td bu exit i;
 171       if false then begin
 172         Format.eprintf "Intermediate result is: @\n";
 173         Sequence.iter (fun (s,_,_, n) ->
 174           Format.eprintf "{%a, %i (%a)}  "
 175             StateSet.print s
 176             (T.preorder tree n)
 177             QName.print (T.tag tree n)) !acc;
 178         Format.eprintf "@\n@.";
 179       end
 180
 181     done;
 182     !acc
 183
 184   let eval auto tree nodes =
 185     let res = main_eval auto tree nodes in
 186     let r = Sequence.create () in
 187     Sequence.iter (fun (_,_,_, n) -> Sequence.push_back n r) res;
 188     r
 189
 190   let full_eval auto tree nodes =
 191     let res = main_eval auto tree nodes in
 192     let dummy = Sequence.create () in
 193     let cache = Cache.N1.create dummy in
 194     Sequence.iter (fun (set, _, _, n) ->
 195       StateSet.iter (fun q ->
 196         let qres = Cache.N1.find cache q in
 197         let qres =
 198           if qres == dummy then begin
 199             let s = Sequence.create () in
 200             Cache.N1.add cache q s;
 201             s
 202           end
 203           else qres
 204         in
 205         Sequence.push_back n qres) set )
 206       res;
 207     let l = StateSet.fold (fun q acc ->
 208       let res = Cache.N1.find cache q in
 209       (q, res) :: acc) (Ata.get_selecting_states auto) []
 210     in
 211     List.rev l
 212
 213 end