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

(* utils.ml-> INCLUDE "utils.ml" HASHINT2 () *)

type state = State.t

type label = QNameSet.t
  
type formula = Formula.t

module Transition = 
struct
  type t = state * label * formula

  let compare (st,la,f) (st',la',f') =
    let x_1 = State.compare st st' in
    if x_1 != 0 then x_1
    else let x_2 = QNameSet.compare la la' in
	 if x_2 != 0 then x_2
	 else Formula.compare f f'
  let st (st,la,f) = st
  let la (st,la,f) = la
  let fo (st,la,f) = f
  let print fmt (st,la,f) =
    Format.fprintf fmt "%a ----%s---> %a"
      State.print st
      (QNameSet.to_string la)
      Formula.print f
end

module  SetT = 
struct
  include Set.Make(Transition)
end

type transition = Transition.t

type t = {
  mutable quer : StateSet.t;
  mutable reco : StateSet.t;
  mutable selec : StateSet.t;
  mutable bottom : StateSet.t;
  mutable top : StateSet.t;
  mutable trans_q : SetT.t;
  mutable trans_r : SetT.t;
}

exception Not_found_transition
exception Transition_not_injective
  
let transition asta st lab =
  let filter (s,l,f) =
    (State.compare s st = 0) && (QNameSet.compare l lab = 0) in
  let tr_set = (SetT.elements (SetT.filter filter asta.trans_q)) @
    (SetT.elements (SetT.filter filter asta.trans_r))
  in
  match tr_set with
    | [] -> raise Not_found_transition
    | x::y::z -> raise Transition_not_injective
    | [l] -> Transition.fo l

let transitions asta st =
  let filter (s,l,f) = State.compare s st = 0 in
  let rec remove_states = function
    | [] -> []
    | (s,l,f) :: tl -> (l,f) :: (remove_states tl) in
  (remove_states (SetT.elements (SetT.filter filter asta.trans_q)),
   (remove_states (SetT.elements (SetT.filter filter asta.trans_r))))

let transitions_lab asta lab = 
  let filter (s,l,f) = QNameSet.mem lab l in
    let rec remove_lab = function
      | [] -> []
      | (s,l,f) :: tl -> (s,f) :: (remove_lab tl) in
    (remove_lab (SetT.elements (SetT.filter filter asta.trans_q)),
     (remove_lab (SetT.elements (SetT.filter filter asta.trans_r))))

let empty = {
  quer = StateSet.empty;
  reco = StateSet.empty;
  selec = StateSet.empty;
  bottom = StateSet.empty;
  top = StateSet.empty;
  trans_q = SetT.empty;
  trans_r = SetT.empty
}

let any_label = QNameSet.complement (QNameSet.empty)

let new_state () = State.make()

let add_tr ast tr flag =
  if flag
  then ast.trans_q <- (SetT.add tr (ast.trans_q))
  else ast.trans_r <- (SetT.add tr (ast.trans_r))

let add_quer ast st = ast.quer <- (StateSet.add st (ast.quer))

let add_reco ast st = ast.reco <- (StateSet.add st (ast.reco))

let add_selec ast st = ast.selec <- (StateSet.add st (ast.selec))

let add_bot ast st = ast.bottom <- (StateSet.add st (ast.bottom))

let add_top ast st = ast.top <- (StateSet.add st (ast.top))

let init_top ast  = ast.top <- (StateSet.empty)

let top_states ast = StateSet.elements ast.top

let top_states_s ast = ast.top

let bot_states_s ast = ast.bottom

let selec_states ast = ast.selec

let print fmt asta =
  let print_box fmt flag = 
    let pp = Format.fprintf fmt in
    pp "@[<v 0># Query states: %a@ @]"
      StateSet.print asta.quer;
    pp "@[<v 0># Recognizing states: %a@ @]"
      StateSet.print asta.reco;
    pp "@[<v 0># Selecting states: %a@ @]"
      StateSet.print asta.selec;
    pp "@[<v 0># Bottom states: %a@ @]"
      StateSet.print asta.bottom;
    pp "@[<v 0># Top states: %a@ @]"
      StateSet.print asta.top;
    let print_list_tr fmt z =
      if SetT.is_empty z 
      then Format.fprintf fmt "ø"
      else
	SetT.iter (fun x -> Format.fprintf fmt "|  %a  @ "  Transition.print x) z in
    let print_box_list fmt trans =
      Format.fprintf fmt "  @[<hov 0>%a @]" print_list_tr trans in
    Format.fprintf fmt "@[<v 0># Queries transitions:@ %a@ @]"
      print_box_list asta.trans_q;
    Format.fprintf fmt "@[<v 0># Recognizing transitions:@ %a@]"
      print_box_list asta.trans_r in
  Format.fprintf fmt "@[<v 1>##### ASTA #####@. %a@ @]@." print_box 0

let to_file out asta = ()