(***********************************************************************)
(*                                                                     *)
(*                               TAToo                                 *)
(*                                                                     *)
(*                   Lucca Hirschi, 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.                                                        *)
(*                                                                     *)
(***********************************************************************)

module Node  =
struct
  type t = int
  let hash n = n
  let compare n1 n2 = n1 - n2
  let equal n1 n2 = n1 = n2
end
  
module NodeHash = Hashtbl.Make (Node)
  
type t = (StateSet.t*StateSet.t) NodeHash.t
(** Map from node to query and recognizing states *)
(* Note that we do not consider the nil nodes *)

(* Build the Oracle *)
let rec bu_oracle asta run tree tnode =
  let init_set node =
    let set = (StateSet.empty,StateSet.empty) in
    NodeHash.add run node set
  and node = Tree.preorder tree tnode in
  if (Tree.is_leaf tree tnode)
  then
    if not (tnode == Tree.nil)
    then
      init_set node
    else ()
  else
    begin
      bu_oracle asta run tree (Tree.first_child tree tnode);
      bu_oracle asta run tree (Tree.next_sibling tree tnode);
      ();
    end

(* Build the over-approx. of the maximal run *)
let rec bu_over_max asta run tree node =
  ()

(* Build the maximal run *)
let rec tp_max asta run tree node =
  ()

let compute tree asta =
  let size_tree = 10000 in              (* todo *)
  let map = NodeHash.create size_tree in
  bu_oracle asta map tree (Tree.root tree);
  bu_over_max asta map tree (Tree.root tree);
  tp_max asta map tree (Tree.root tree);
  map

let print fmt run =
  let print_d_set fmt (s_1,s_2) = 
    Format.fprintf fmt "@[<hov 0>(%a,@ %a)@]"
      StateSet.print s_1 StateSet.print s_2 in
  let print_map fmt run = 
    let pp = Format.fprintf fmt in
    if NodeHash.length run = 0
    then Format.fprintf fmt "ø"
    else
      NodeHash.iter (fun cle set -> pp "|  %i-->%a  @ " cle print_d_set set)
        run in
  let print_box fmt run =
    let pp = Format.fprintf fmt in
    pp "@[<hov 0>@.  # Mapping:@.   @[<hov 0>%a@]@]"
      print_map run
  in
  Format.fprintf fmt "@[<hov 0>##### RUN #####@, %a@]@." print_box run