(***********************************************************************)
(*                                                                     *)
(*                               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 *)

exception Oracle_fail
exception Over_max_fail
exception Max_fail

(* 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
    let tfnode = Tree.first_child tree tnode
    and tnnode = Tree.next_sibling tree tnode in
    begin
      bu_oracle asta run tree tfnode;
      bu_oracle asta run tree tnnode;
      let (fnode,nnode) =
        (Tree.preorder tree tfnode, Tree.preorder tree tnnode) in
      let q_rec n =
        try NodeHash.find run n
        with Not_found -> (StateSet.empty,StateSet.empty) in
      let (_,qf),(_,qn) = q_rec fnode,q_rec nnode in
      let lab = Tree.tag tree tnode in
      let _,list_tr = Asta.transitions_lab asta lab in (* only take reco. *)
      let result_set = ref StateSet.empty in
      let rec result = function
        | [] -> ()
        | (q,form) :: tl ->
          if Formula.eval_form (qf,qn) form
          then begin
            result_set := (StateSet.add q (!result_set));
            result tl; end
          else result tl in
      result list_tr;
      NodeHash.add run node (StateSet.empty, !result_set)
    (* Do not remove elt in Hahs (the old one would appear) *)
    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