(**************************************************************************)
(*                                                                        *)
(*  This file is part of the Concurrency Plugin for Frama-C               *)
(*                                                                        *)
(*  Copyright (C) 2013                                                    *)
(*    Adelard LLP                                                         *)
(*    CINIF (Control and Instrumentation Nuclear Industry Forum)          *)
(*                                                                        *)
(*  You can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 3.                                                *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version v3                  *)
(*  for more details (enclosed in the file ./LGPLv3).                     *)
(*                                                                        *)
(**************************************************************************)
open Concurguiglobs
open Cil_datatype 
open Cil_types
(**
 * A form to show variable accesses locations.
*)
class vAccWindow mainui =
object(slf) 
  val mutable access_display = (None : GWindow.window option)
 
  val m_mainui = mainui
  val mutable m_acc_tree_columns = ([] : string GTree.column list)
  val mutable m_acc_tree = (None : GTree.list_store option)
  val mutable m_acc_adjust = (None : GData.adjustment option)
 
  (*Populates the tree view with the current 
    functions to be displayed.*)
  method private populate_tree 
    (pa_tree : GTree.list_store) 
    (columns_list :  string GTree.column list) 
    (pa_adjust : GData.adjustment) =
    begin
      match columns_list with
	  col0::col1::col2::col3::col4::_ ->
	    begin
	      let add_acc_to_tree nn (ep, i, f, b) = 
		let fname = match f with
		    Some(f) -> Kernel_function.get_name f
		  | None -> "(global)"
		in
		let iter = pa_tree#append () in
		pa_tree#set ~row:iter ~column:col0 (Kernel_function.get_name ep);
		pa_tree#set ~row:iter ~column:col1 (if b then "Write" else "Read");
		pa_tree#set ~row:iter ~column:col2 (Pretty_utils.to_string Printer.pp_location (Kinstr.loc i));
		pa_tree#set ~row:iter ~column:col3 fname;
		pa_tree#set ~row:iter ~column:col4 (string_of_int nn);
		nn+1;
	      in
	      pa_tree#clear ();
	      ignore (List.fold_left add_acc_to_tree 0 (AccessForList.get ()));
	      pa_adjust#set_bounds ~upper:(float_of_int (List.length (AccessForList.get ()))) ()
	    end
	| _ -> ()
    end
       
  method private create_acc_display () = 
    begin
      access_display <- Some(GWindow.window ~title:"Current variable RoW"()); 
      ignore((get_option access_display)#connect#destroy ( fun () -> access_display <- None));
      
      let v_box = GPack.vbox ~packing:(get_option access_display)#add () in
      let h2_box = GPack.hbox ~packing:v_box#add () in
      let acc_tree_columns = new GTree.column_list in
      let acc_tree_column0 = acc_tree_columns#add Gobject.Data.string in 
      let acc_tree_column1 = acc_tree_columns#add Gobject.Data.string in 
      let acc_tree_column2 = acc_tree_columns#add Gobject.Data.string in 
      let acc_tree_column3 = acc_tree_columns#add Gobject.Data.string in 
      let acc_tree_column4 = acc_tree_columns#add Gobject.Data.string in 
      let acc_tree = GTree.list_store acc_tree_columns in
      let acc_view = GTree.view ~model:acc_tree ~height:360 ~packing:h2_box#pack () in
      
      acc_view#selection#set_mode `SINGLE;
      
      let acc_col0 = GTree.view_column 
	~title: "From" 
	~renderer: (GTree.cell_renderer_text [], [("text", acc_tree_column0)]) ()
      in
      let acc_col1 = GTree.view_column 
	~title: "R/W" 
	~renderer: (GTree.cell_renderer_text [], [("text", acc_tree_column1)]) ()
      in
      let acc_col2 = GTree.view_column 
	~title: "Location" 
	~renderer: (GTree.cell_renderer_text [], [("text", acc_tree_column2)]) ()
      in
      let acc_col3 = GTree.view_column 
	~title: "Function" 
	~renderer: (GTree.cell_renderer_text [], [("text", acc_tree_column3)]) ()
      in
      let acc_col4 = GTree.view_column 
	~title: "ID" 
	~renderer: (GTree.cell_renderer_text [], [("text", acc_tree_column4)]) ()
      in
      
      ignore (acc_view#append_column acc_col0);
      ignore (acc_view#append_column acc_col1);
      ignore (acc_view#append_column acc_col2);
      ignore (acc_view#append_column acc_col3);
      ignore (acc_view#append_column acc_col4);
      
      
      let acc_adjust = GData.adjustment () in 
      (*create a scroll bar*)
      ignore(GRange.scrollbar `VERTICAL ~adjustment:acc_adjust ~packing:h2_box#pack ());
      
      acc_view#set_vadjustment acc_adjust;
      
      m_acc_tree <- Some(acc_tree);
      m_acc_tree_columns <- [acc_tree_column0;
			     acc_tree_column1;
			     acc_tree_column2;
			     acc_tree_column3;
			     acc_tree_column4];
      m_acc_adjust <- Some(acc_adjust);
	      
      (*Selects a row as var of interest *)
      let select_kloc () =
	let selected_rows = acc_view#selection#get_selected_rows in
	if (List.length selected_rows) > 0 then
	  let model = acc_view#model in
	  let lid = int_of_string (get_t_row model acc_tree_column4 (List.hd selected_rows)) in
	  
	  let (_, b, _, _) = List.nth (AccessForList.get ()) lid in
	  match b with
	      Kstmt(st) -> (CurrentKinstr.set b; m_mainui#view_stmt st; m_mainui#rehighlight ();)
	    | Kglobal -> ()
	else 
	  ()
      in
      ignore(acc_view#connect#cursor_changed select_kloc); 
      
      slf#populate_tree acc_tree m_acc_tree_columns acc_adjust;
      (get_option access_display)#show ()
    end
      
  method show_acc () =
    begin
      match access_display with 
	  Some(e) ->
	    ignore(e#present ())
	| None -> 
	  slf#create_acc_display ()
    end
	
  method refresh () = 
    begin
      match (access_display, m_acc_tree , m_acc_adjust) with 
	  (Some(_), Some(b), Some(c)) ->
	    slf#populate_tree b m_acc_tree_columns c; 
	| _ -> ()
    end
end