aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/blaster_window.ml
blob: 400eb1025da2263e313ffad5afee0f17a590bd57 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* $Id$ *)

open Gobject.Data
open Ideutils

exception Stop
exception Done

module MyMap = Map.Make (struct type t = string let compare = compare end)

class blaster_window (n:int) = 
  let window = GWindow.window 
		 ~allow_grow:true ~allow_shrink:true 
		 ~width:320 ~height:200
		 ~title:"Blaster Window" ~show:false ()
  in
  let box1 = GPack.vbox ~packing:window#add () in
  let sw = GBin.scrolled_window ~packing:(box1#pack ~expand:true ~fill:true) () in

  let cols = new GTree.column_list in
  let argument = cols#add string in
  let tactic = cols#add string in
  let status = cols#add boolean in
  let nb_goals = cols#add string in
  
  let model = GTree.tree_store cols in
  let new_arg s =
    let row = model#append () in
    model#set ~row ~column:argument s;
    row
  in
  let new_tac arg s =  
    let row = model#append ~parent:arg () in
    model#set ~row ~column:tactic s;
    model#set ~row ~column:status false;
    model#set ~row ~column:nb_goals "?";
    row
  in
  let view = GTree.view ~model ~packing:sw#add () in
  let _ = view#selection#set_mode `SINGLE in
  let _ = view#set_rules_hint true in

  let col = GTree.view_column ~title:"Argument" ()
	      ~renderer:(GTree.cell_renderer_text [], ["text",argument]) in
  let _ = view#append_column col in
  let col = GTree.view_column ~title:"Tactics" ()
	      ~renderer:(GTree.cell_renderer_text [], ["text",tactic]) in
  let _ = view#append_column col in
  let col = GTree.view_column ~title:"Status" ()
	      ~renderer:(GTree.cell_renderer_toggle [], ["active",status]) in
  let _ = view#append_column col in
  let col = GTree.view_column ~title:"Delta Goal" ()
	      ~renderer:(GTree.cell_renderer_text [], ["text",nb_goals]) in
  let _ = view#append_column col in 

  let _ = GMisc.separator `HORIZONTAL ~packing:box1#pack () in
  
  let box2 = GPack.vbox ~spacing: 10 ~border_width: 10 ~packing: box1#pack () 
  in
  let button_stop = GButton.button ~label: "Stop" ~packing: box2#add () in
  let _ = button_stop#connect#clicked ~callback: window#misc#hide in

object(self)
  val window = window
  val roots = Hashtbl.create 17
  val mutable tbl = MyMap.empty 
  val blaster_lock = Mutex.create () 
  method lock = blaster_lock 
  val blaster_killed = Condition.create () 
  method blaster_killed = blaster_killed
  method window = window
  method set root name (compute:unit -> Coq.tried_tactic) (on_click:unit -> unit) = 
    let root_iter = 
      try Hashtbl.find roots root 
      with Not_found -> 
	let nr = new_arg root in
	  Hashtbl.add roots root nr;
	  nr
    in
    let nt = new_tac root_iter name in
    let old_val = try MyMap.find root tbl with Not_found -> MyMap.empty in
      tbl <- MyMap.add root (MyMap.add name (nt,compute,on_click) old_val) tbl

  method clear () = 
    model#clear ();      
    tbl <- MyMap.empty;
    Hashtbl.clear roots;
    
  method blaster () = 
    view#expand_all ();
    try MyMap.iter 
      (fun root_name l ->
	 try 
	   MyMap.iter 
	     (fun name (nt,compute,on_click) ->  
		match compute () with 
		  | Coq.Interrupted -> 
		      prerr_endline "Interrupted";
		      raise Stop
		  | Coq.Failed -> 
		      prerr_endline "Failed";
		      ignore (model#remove nt)
			(*	       model#set ~row:nt ~column:status false;
				       model#set ~row:nt ~column:nb_goals "N/A"
			*)
		  | Coq.Success n -> 
		      prerr_endline "Success";
		      model#set ~row:nt ~column:status true;
		      model#set ~row:nt ~column:nb_goals (string_of_int n);
		      if n= -1 then raise Done 
	     )
	     l
	 with Done -> ())
      tbl;
      Condition.signal blaster_killed;
      prerr_endline "End of blaster";
    with Stop ->
      Condition.signal blaster_killed;
      prerr_endline "End of blaster (stopped !)";

  initializer 
    ignore (window#event#connect#delete (fun _ -> window#misc#hide(); true));
    ignore (view#selection#connect#after#changed ~callback:
	      begin fun () ->
		prerr_endline "selection changed";
		List.iter 
		  (fun path ->let pt = GtkTree.TreePath.to_string path in
		     let it = model#get_iter path in
		     prerr_endline (string_of_bool (model#iter_is_valid it));
		     let name = model#get 
				  ~row:(if String.length pt >1 then begin
					  ignore (GtkTree.TreePath.up path);
					  model#get_iter path
					end else it
				       ) 
				  ~column:argument in
		     let tactic = model#get ~row:it ~column:tactic in
		     prerr_endline ("Got name: "^name);
		     let success = model#get ~row:it ~column:status in
		     if success then try 
		       prerr_endline "Got success";
		       let _,_,f = MyMap.find tactic (MyMap.find name tbl) in
		       f ();
		       (* window#misc#hide () *)
		     with _ -> ()
		  )
		  view#selection#get_selected_rows
	      end);

(* needs lablgtk2 update    ignore (view#connect#after#row_activated
   (fun path vcol ->
   prerr_endline "Activated";
   );
*)
end

let blaster_window = ref None

let main n = blaster_window := Some (new blaster_window n)

let present_blaster_window () = match !blaster_window with 
  | None -> failwith "No blaster window."
  | Some c -> c#window#misc#show (* present*) (); c


let blaster_window () = match !blaster_window with 
  | None -> failwith "No blaster window."
  | Some c -> c