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
open Wpo
module Windex = Indexer.Make(Wpo.S)
class model =
object(self)
val mutable index = Windex.empty
method reload = index <- Windex.empty
method add w = index <- Windex.add w index
method size = Windex.size index
method index w = Windex.index w index
method get k = Windex.get k index
method coerce = (self :> Wpo.t Wtable.listmodel)
end
let render_prover_result p =
let icn_stock name = [`STOCK_ID name] in
let icn_status s = [`PIXBUF(Gtk_helper.Icon.get (Gtk_helper.Icon.Feedback s))] in
let icn_na = [`PIXBUF(Gtk_helper.Icon.get Gtk_helper.Icon.Unmark)] in
let icn_none = icn_stock "" in
let icn_valid = icn_status Property_status.Feedback.Valid in
let icn_unknown = icn_status Property_status.Feedback.Unknown in
let icn_invalid = icn_status Property_status.Feedback.Invalid in
let icn_failed = icn_stock "gtk-dialog-warning" in
let icn_cut = icn_stock "gtk-cut" in
let icn_running = icn_stock "gtk-execute" in
let open VCS in
let icon_of_verdict ~smoke = function
| NoResult -> icn_none
| Valid -> if smoke then icn_invalid else icn_valid
| Invalid -> if smoke then icn_valid else icn_invalid
| Unknown -> if smoke then icn_valid else icn_unknown
| Timeout | Stepout -> if smoke then icn_valid else icn_cut
| Failed -> icn_failed
| Computing _ -> icn_running
in fun w ->
match Wpo.get_result w p , p with
| { verdict=NoResult } , Qed -> icn_na
| { verdict=NoResult } , Tactical ->
begin
match ProverScript.get w with
| `None -> icn_na
| `Script -> icn_stock "gtk-media-play"
| `Proof -> icn_stock "gtk-edit"
| `Saved -> icn_stock "gtk-file"
end
| result , _ ->
icon_of_verdict ~smoke:(Wpo.is_smoke_test w) result.verdict
class pane (gprovers:GuiConfig.provers) =
let model = new model in
let list = new Wtable.list ~headers:true ~rules:true model#coerce in
object(self)
method coerce = list#coerce
method reload = list#reload
method add wpo =
begin
model#add wpo ;
list#insert_row wpo ;
end
method size = model#size
method index = model#index
method get = model#get
method update_all = list#update_all
method update w = list#update_row w
val mutable provers : (VCS.prover * GTree.view_column) list = []
method private prover_of_column c =
let id = c#misc#get_oid in
try Some(fst(List.find (fun (_,c0) -> id = c0#misc#get_oid) provers))
with Not_found -> None
method private column_of_prover p =
try Some(snd(List.find (fun (p0,_) -> p=p0) provers))
with Not_found -> None
method private create_prover p =
begin
let title = VCS.title_of_prover p in
let column = list#add_column_pixbuf ~title [] (render_prover_result p)
in if p <> VCS.Qed then provers <- (p,column) :: provers
end
method private configure (dps:Why3.Whyconf.Sprover.t) =
begin
List.iter
(fun (vcs,column) ->
match vcs with
| VCS.Why3 p ->
column#set_visible (Why3.Whyconf.Sprover.mem p dps) ;
| _ -> ()
) provers ;
Why3.Whyconf.Sprover.iter
(fun dp ->
let prv = VCS.Why3 dp in
match self#column_of_prover prv with
| None -> self#create_prover prv
| Some _ -> ()
) dps ;
end
initializer
begin
let render w =
[`TEXT (Pretty_utils.to_string Wpo.pp_index w.po_idx)] in
ignore (list#add_column_text ~title:"Module" [] render) ;
let render w =
[`TEXT (Pretty_utils.to_string Wpo.pp_title w)] in
ignore (list#add_column_text ~title:"Goal" [] render) ;
let render w = [`TEXT (Wpo.get_model w |> WpContext.MODEL.descr)] in
ignore (list#add_column_text ~title:"Model" [] render) ;
List.iter
self#create_prover
[ VCS.Qed ; VCS.Tactical ] ;
ignore (list#add_column_empty) ;
list#set_selection_mode `MULTIPLE ;
gprovers#connect self#configure ;
self#configure gprovers#get ;
end
method private on_cell f w c = f w (self#prover_of_column c)
method on_click f = list#on_click (self#on_cell f)
method on_double_click f = list#on_double_click (self#on_cell f)
method on_right_click f = list#on_right_click (self#on_cell f)
method on_selection f = list#on_selection (fun () -> f list#count_selected)
method iter_selected = list#iter_selected
method count_selected = list#count_selected
method show w =
let col = list#view#get_column 1 in
list#set_focus w col
end