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

INCLUDE "utils.ml"


(* Hash Consign modules *)

module type Oracle_fixpoint =
sig
  type t = StateSet.t*StateSet.t*StateSet.t*((StateSet.elt*Formula.t) list)*QName.t
  val equal : t -> t -> bool
  val hash : t -> int
end

type dStateS = StateSet.t*StateSet.t
module type Run_fixpoint =
sig
  type t = dStateS*dStateS*dStateS*(State.t*Formula.t) list*QName.t
  val equal : t -> t -> bool
  val hash : t -> int
end
    
module Oracle_fixpoint : Oracle_fixpoint = struct
  type t =
      StateSet.t*StateSet.t*StateSet.t*((StateSet.elt*Formula.t) list)*QName.t
  let equal (s,l,r,list,t) (s',l',r',list',t') = StateSet.equal s s' &&
    StateSet.equal l l' && StateSet.equal r r' && QName.equal t t'
  let hash (s,l,r,list,t) =
    HASHINT4(StateSet.hash s, StateSet.hash l, StateSet.hash r, QName.hash t)
end
  
let dequal (x,y) (x',y') = StateSet.equal x x' && StateSet.equal y y'
let dhash (x,y) = HASHINT2(StateSet.hash x, StateSet.hash y)
module Run_fixpoint : Run_fixpoint = struct
  type t = dStateS*dStateS*dStateS*(State.t*Formula.t) list*QName.t
  let equal (s,l,r,list,t) (s',l',r',list',t') = dequal s s' &&
    dequal l l' && dequal r r' && QName.equal t t'
  let hash (s,l,r,list,t) =
    HASHINT4(dhash s, dhash l, dhash r, QName.hash t)
end