(**************************************************************************)
(*                                                                        *)
(*  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 Callgraph
open Cil_datatype
open Cil_types
open Concurrency_main

exception No_value;;

(*this might be unnecessary if we include the Option library*)
let get_option ip = 
  match ip with
      None -> raise No_value
    | Some(e) -> e;;

(** Constants used during initialisation*)
let init_varinfo = Varinfo.dummy ;; 			(*initial variable*)
let init_fundec = Kernel_function.dummy ();;		(*inital thread*)
let refresh = ref (true,true,true,false, false);; 	(*the GUI statemachine*)

(*The code's call graph*)
let cg = ref (None : callgraph option);;

(*Function to obtain a row from a Treeview model. *)
let get_t_row (model: GTree.model) col path = 
  let row = model#get_iter path in
  let name = model#get ~row ~column:col in
  name;;


(** Current variable to be passed to -var-overlap command line option*)   
module LockedVar = 
  State_builder.Ref
    (Varinfo)
    (struct
      let name = "Concurrency_gui.LockedVar"
      let dependencies = []
      let default () = init_varinfo
     end);;

(** Holds current -var-overlap output*)
module VarOverlapSet_ref = 
  State_builder.Ref (*Tried Set_ref but it did not work*)
    (Varinfo.Set)
    (struct
      let name = "Concurrency_gui. VarOverlapList"
      let dependencies = []
      let default () = Varinfo.Set.empty
     end);;

(** List of currently selected threads to intersect*)   
module SelectedThreads = 
  State_builder.List_ref
    (Kernel_function)
    (struct
      let name = "Concurrency_gui.SelectedThreads"
      let dependencies = []
     end) ;; 

(** Currently selected "main" thread to intersect*)   
module SelectedMain = 
  State_builder.Ref
    (Kernel_function)
    (struct
      let name = "Concurrency_gui.SelectedMain"
      let dependencies = []
      let default () = init_fundec
     end)  ;;

(** Holds all entry points detected*)
module AllEntryPoints = 
  State_builder.List_ref
    (Kernel_function)
    (struct
      let name = "Concurrency_gui.AllEntryPoints"
      let dependencies = []
     end);;

(** Holds entry points selected by user - we can subsume this 
* into AllEntryPoints if we use a (Kernel_function, bool) type 
* where the second argument denotes show/hide.
*)
module FilteredEntryPoints = 
  State_builder.List_ref
    (Kernel_function)
    (struct
      let name = "Concurrency_gui.FilteredEntryPoints"
      let dependencies = []
     end);;
    

module CurrentKinstr = 
  State_builder.Ref
    (Kinstr)
    (struct
      let name = "Concurrency_gui.CurrentKinstr"
      let dependencies = []
      let default () = Kglobal
     end);;

(** Holds current -access-for output*)
module AccessForList = 
  State_builder.List_ref
    (Datatype.Make
       (struct
	 include Datatype.Serializable_undefined
	 type t = Kernel_function.t * Kinstr.t * Kernel_function.t option * bool
	 let name = "Access for type"
	 (*dont know what reprs is - could be replicators??*)
	 let reprs = [(init_fundec, Kglobal, None, false)] 
	 let mem_project = Datatype.never_any_project
	end))
	(struct
	  let name = "Concurrency_gui. AccessForList"
	  let dependencies = []
	 end);;
     
(**
*  Initialises the concurrency gui
*)
let start_concurrency () =

  cg := Some(computeGraph (Ast.get()));

  let eps = computeEntryPoints (get_option !cg) in
  SelectedMain.set init_fundec;
  LockedVar.set init_varinfo;
  SelectedThreads.set [];
  
  CurrentKinstr.set Kglobal;
  
  (*Set the identified entry point functions*)
  AllEntryPoints.set eps;  
  FilteredEntryPoints.set eps;

  VarOverlapSet_ref.set Varinfo.Set.empty;
  AccessForList.set [];;

(**
*  Resets the concurrency gui without affecting the entry point lists
*)
let reset_concurrency () =
  SelectedMain.set init_fundec;
  LockedVar.set init_varinfo; 
  SelectedThreads.set []; 

  CurrentKinstr.set Kglobal;
 
  VarOverlapSet_ref.set Varinfo.Set.empty;
  AccessForList.set [];;