(* $Id$ *)

(* Bertrand Jeannet. This file is released under LGPL license. *)

(** Example of use of MkFixpoint module *)

open Format

(** This file shows how to use the MkFixpoint module.

  It defines a dummy abstract domain: the domain of integer, ordered by the
  normal order, with bottom value 0, top value max_int.

  It also define a dummy fixpoint equation system.

*)

(** {2 The abstract domain} *)

module A = struct
  type t = int
  type manager = unit

  let bottom man = 0
  let canonical man x = ()
  let is_bottom man x = x=0
  let is_leq man x y = x <= y
  let join man x y = max x y
  let join_list man tx =
    List.fold_left (fun res x -> join man res x) 0 tx
  let print man fmt x = pp_print_int fmt x
end

(** {2 The equation system, modelled as an hypergraph} *)

(** First, we need to define some parameter modules for the hypergraph
structures *)

(** Set over integers *)
module SetteI = Sette.Make(struct
  type t=int
  let compare = (-)
end)

(** Hashtable over integers *)
module HashheI = Hashhe.Make(struct
  type t=int
  let equal = (==)
  let hash x = x
end)

(** Parameter module for hypergraphs *)
module T = struct
  type vertex=int
    (** type of vertices (variables in the equation system) *)
  type hedge=int
    (** type of hyperedges (functions in the equation system) *)
  let vertex_dummy =(-1)
    (** dummy value *)
  let hedge_dummy=(-1)
    (** dummy value *)
  module SetV=SetteI
    (** Set module for vertices *)
  module SetH=SetteI
    (** Set module for hyperedges *)
  module HashV=HashheI
    (** Hash module for vertices *)
  module HashH=HashheI
    (** Hash module for hyperedges *)
end

(** Creation of the hypergraph module *)
module Graph = SHGraph.Make(T)

(** {2 Instanciation of the fixpoint engine} *)

module Fixpoint = MkFixpoint.Make(Graph)

(** {2 Various functions} *)

let pp_print_unit fmt () = pp_print_string fmt "()"

let print_graph
  (manager:(int,unit) Fixpoint.manager)
  fmt
  (graph:(int,unit) Fixpoint.graph)
  =
  Fixpoint.print_graph manager fmt graph

let print_output
  (manager:(int,unit) Fixpoint.manager)
  fmt
  (output:(int,unit) Fixpoint.output)
  =
  Fixpoint.print_output manager fmt output

let essai () =
  (* Creation of the following equation graph: 
     X1 = F0(X0) U F1(X1)
     X2 = F2(X1)
  *)
  let (g:(unit,unit,unit) Graph.t) = Graph.create 10 () in
  Graph.add_vertex g 0 ();
  Graph.add_vertex g 1 ();
  Graph.add_vertex g 2 ();
  Graph.add_hedge g 0 () ~pred:[|0|] ~succ:[|1|];
  Graph.add_hedge g 1 () ~pred:[|1|] ~succ:[|1|];
  Graph.add_hedge g 2 () ~pred:[|1|] ~succ:[|2|];
  (* MANAGER *)
  let (manager:(int,unit) Fixpoint.manager) = {
    Fixpoint.bottom = begin fun vertex -> 0 end;
    Fixpoint.canonical = begin fun vertex abs -> () end;
    Fixpoint.is_bottom = begin fun vertex abs -> abs=0 end;
    Fixpoint.is_leq = begin fun vertex abs1 abs2 -> abs1<=abs2 end;
    Fixpoint.join = begin fun vertex abs1 abs2 -> max abs1 abs2 end;
    Fixpoint.join_list = begin fun vertex labs ->
      List.fold_left (fun res x -> max res x) 0 labs
    end;
    Fixpoint.widening = begin fun vertex abs1 abs2 -> 
      if abs2>abs1 then max_int else max abs1 abs2
    end;
    Fixpoint.apply= begin fun hedge tabs ->
      ((),
      if hedge=0 then 100
      else if hedge=1 then if tabs.(0)<400 then (tabs.(0)+1) else 400
      else if hedge=2 then 200
      else 0
      )
    end;
    Fixpoint.arc_init = begin fun hedge -> () end;
    Fixpoint.get_init= begin fun vertex -> if vertex=0 then max_int else 0 end;

    Fixpoint.print_abstract=pp_print_int;
    Fixpoint.print_arc=(fun fmt () -> ());
    Fixpoint.print_vertex=pp_print_int;
    Fixpoint.print_hedge=pp_print_int;

    Fixpoint.widening_first=false;
    Fixpoint.widening_start=1;
    Fixpoint.widening_freq=1;
    Fixpoint.widening_descend=2;

    Fixpoint.print_analysis=true;
    Fixpoint.print_step=true;
    Fixpoint.print_state=true;
    Fixpoint.print_postpre=true
  }
  in
  let strat = Fixpoint.strategy_default g (SetteI.singleton 0) in
  printf "strategy=%a@." (Fixpoint.print_strategy manager) strat;

  let graph = Fixpoint.init manager g (SetteI.singleton 0) in
  printf "initial graph=%a@." (print_graph manager) graph;

  Fixpoint.fixpoint manager graph strat;

  let b = Fixpoint.descend manager graph strat in
  printf "final graph=%a@." (print_graph manager) graph;

  let output = Fixpoint.output_of_graph graph in
  printf "output=%a@." (print_output manager) output;
  ()

let _ = essai ()