]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/matitaAutoGui.ml
fixed, it seems the new handling of hints in some rare cases made inference stupid
[helm.git] / helm / software / matita / matitaAutoGui.ml
1 (* Copyright (C) 2003, HELM Team.
2  * 
3  * 
4  * This file is part of HELM, an Hypertextual, Electronic
5  * Library of Mathematics, developed at the Computer Science
6  * Department, University of Bologna, Italy.
7  * 
8  * HELM is free software; you can redistribute it and/or
9  * modify it under the terms of the GNU General Public License
10  * as published by the Free Software Foundation; either version 2
11  * of the License, or (at your option) any later version.
12  * 
13  * HELM is distributed in the hope that it will be useful,
14  * but WITHOUT ANY WARRANTY; without even the implied warranty of
15  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
16  * GNU General Public License for more details.
17  *
18  * You should have received a copy of the GNU General Public License
19  * along with HELM; if not, write to the Free Software
20  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
21  * MA  02111-1307, USA.
22  * 
23  * For details, see the HELM World-Wide-Web page,
24  * http://cs.unibo.it/helm/.
25  *)
26
27 type status = 
28   Cic.context * (int * Cic.term * bool * int * (int * Cic.term Lazy.t) list) list * 
29   (int * Cic.term * int) list *
30   Cic.term Lazy.t list
31 let fake_goal = Cic.Implicit None;;
32 let fake_candidates = [];;
33
34 let start = ref 0;;
35 let len = ref 10;;
36
37
38 let font_size = ref 
39   (Helm_registry.get_opt_default Helm_registry.int
40     ~default:BuildTimeConf.default_font_size "matita.font_size")
41 ;;
42
43 let set_font_size n = font_size := n;;
44
45 let pp ?(size=(!font_size)) c t =
46   let t = 
47     ProofEngineReduction.replace 
48       ~equality:(fun a b -> match b with Cic.Meta _ -> true | _ -> false) 
49       ~what:[Cic.Rel 1] ~with_what:[Cic.Implicit None] ~where:t
50   in
51   (if size > 0 then "<span font_desc=\""^string_of_int size^"\">" else "") ^
52   (MatitaGtkMisc.escape_pango_markup
53     (ApplyTransformation.txt_of_cic_term ~map_unicode_to_tex:false
54       max_int [] c t))^
55   (if size > 0 then "</span>" else "")
56 ;;
57 let pp_goal context x = 
58   if x == fake_goal then "" else pp context x
59 ;;
60 let pp_candidate context x = pp context (Lazy.force x)
61 let pp_candidate_tip context x = pp ~size:0 context (Lazy.force x)
62 let pp_candidate_type context x = 
63   try 
64     let ty, _ = 
65       CicTypeChecker.type_of_aux' [] ~subst:[] 
66        context (Lazy.force x) CicUniv.oblivion_ugraph
67     in
68       pp ~size:0 context ty
69   with CicUtil.Meta_not_found _ ->  pp ~size:0 context (Lazy.force x)
70 ;;
71
72 let sublist start len l = 
73   let rec aux pos len = function
74     | [] when pos < start -> aux (pos+1) len []
75     | [] when len > 0 -> 
76           (0,fake_goal, false, 0, fake_candidates) :: aux (pos+1) (len-1) [] 
77     | [] (* when len <= 0 *) -> []
78     | he::tl when pos < start -> aux (pos+1) len tl
79     | he::tl when pos >= start && len > 0 -> he::aux (pos+1) (len-1) tl
80     | he::tl (* when pos >= start && len <= 0 *) -> []
81   in
82   aux 0 len l
83 ;;
84
85 let cell_of_candidate height context ?(active=false) g id c = 
86   let tooltip = GData.tooltips () in (* should be only one isn't it? *)
87   let button = GButton.button () in
88   let l = GMisc.label ~markup:(pp_candidate context c) () in
89   button#add l#coerce;
90   button#misc#set_size_request ~height ();
91   if active then
92     button#misc#set_sensitive false;
93   let text = 
94     "Follow/Prune computation of\n"^pp_candidate_tip context c^": "^
95     pp_candidate_type context c
96   in
97   tooltip#set_tip ~text (button :> GObj.widget);
98   ignore(button#connect#clicked 
99     (fun _ -> 
100       let menu = GMenu.menu () in
101       let follow = GMenu.menu_item ~label:"Follow" () in
102       let prune = GMenu.menu_item ~label:"Prune" () in
103       ignore (follow#connect#activate 
104         (fun _ -> HLog.warn (string_of_int id); Auto.give_hint id));
105       ignore (prune#connect#activate 
106         (fun _ -> HLog.warn (string_of_int id); Auto.give_prune_hint id));
107       menu#append follow;
108       menu#append prune;
109       menu#popup 0 (GtkMain.Main.get_current_event_time ())));
110   button
111 ;;
112 let cell_of_goal height win_width context goal = 
113   GMisc.label 
114     ~markup:(pp_goal context goal) ~xalign:0.0 
115     ~width:(min (win_width * 30 / 100) 500) 
116     ~line_wrap:false
117     ~ellipsize:`END
118     ~height
119     ()
120 ;;
121 let cell_of_row_header height n k id = 
122   GMisc.label
123     ~markup:("<span stretch=\"ultracondensed\">" ^ string_of_int n ^ "<sub>(" ^
124              string_of_int id ^ "|" ^ string_of_int k ^ ")</sub></span>") 
125     ~line_wrap:true ~justify:`LEFT ~height ~width:80 ()
126 ;;
127 let cell_of_candidates height grey context goal cads = 
128   let hbox = GPack.hbox () in
129   match cads with
130   | [] -> hbox
131   | (id,c)::tl ->
132       hbox#pack 
133         (cell_of_candidate height ~active:grey 
134           context goal id c :> GObj.widget);
135       List.iter
136         (fun (id,c) -> 
137         hbox#pack (cell_of_candidate height context goal id c :> GObj.widget)) tl;
138         hbox
139 ;;
140
141 let elems_to_rows height context win_width (table : GPack.table) (or_list) =
142   let height = height / ((List.length or_list) + 1) in
143   let _ = 
144    List.fold_left 
145     (fun position (goal_id, goal, grey, depth, candidates) ->
146       table#attach ~left:0 ~top:position 
147         (cell_of_row_header height (position + !start) 
148           depth goal_id :> GObj.widget);
149       table#attach ~left:1 ~top:position ~fill:`BOTH
150         (cell_of_goal height win_width context goal :> GObj.widget);
151       table#attach ~left:2 ~top:position 
152         (cell_of_candidates height grey context goal candidates :> GObj.widget);
153       position+1)
154     0 or_list
155   in 
156   ()
157 ;;
158
159 let old_displayed_status = ref [];;
160 let old_size = ref 0;;
161
162 let fill_win (win : MatitaGeneratedGui.autoWin) cb =
163 (*   let init = Unix.gettimeofday () in *)
164     try 
165       let (status : status) = cb () in
166       let win_size = win#toplevel#misc#allocation.Gtk.width in
167       let ctx, or_list, and_list, last_moves = status in
168       let displayed_status = 
169         sublist !start !len 
170           (or_list @ (List.map (fun (id,x,d) -> id,x,false,d,[]) and_list)) 
171       in
172       if displayed_status <> !old_displayed_status || !old_size <> win_size then
173         begin
174           old_displayed_status := displayed_status;
175           old_size := win_size;
176 (*
177           win#labelLAST#set_text 
178             (String.concat ";" (List.map (pp_candidate ctx) last_moves));
179 *)
180           List.iter win#table#remove win#table#children;
181           let height = win#viewportAREA#misc#allocation.Gtk.height in
182           elems_to_rows height ctx win_size win#table displayed_status;
183 (*
184           Printf.eprintf 
185             "REDRAW COST: %2.1f\n%!" (Unix.gettimeofday () -.  init);
186 *)
187         end
188     with exn -> prerr_endline (Printexc.to_string exn); ()
189 ;;
190
191 let auto_dialog elems =
192   let win = new MatitaGeneratedGui.autoWin () in
193   let width = Gdk.Screen.width () in
194   let height = Gdk.Screen.height () in
195   let main_w = width * 70 / 100 in 
196   let main_h = height * 60 / 100 in
197   win#toplevel#resize ~width:main_w ~height:main_h;
198   win#check_widgets ();
199   win#table#set_columns 3;
200   win#table#set_col_spacings 6;
201   win#table#set_row_spacings 4;
202   ignore(win#buttonUP#connect#clicked 
203     (fun _ -> start := max 0 (!start -1); fill_win win elems));
204   ignore(win#buttonDOWN#connect#clicked 
205     (fun _ -> incr start; fill_win win elems));
206   ignore(win#buttonCLOSE#connect#clicked 
207     (fun _ -> 
208       Auto.pause false;
209       Auto.step ();
210       win#toplevel#destroy ();
211       GMain.Main.quit ()));
212   ignore(win#toplevel#event#connect#delete
213     (fun _ -> 
214       Auto.pause false;
215       Auto.step ();
216       win#toplevel#destroy ();
217       GMain.Main.quit ();true));
218   let redraw_callback _ = 
219     fill_win win elems;
220     true 
221   in
222   let redraw = GMain.Timeout.add ~ms:400 ~callback:redraw_callback in
223   ignore(win#buttonPAUSE#connect#clicked 
224     (fun _ -> 
225       Auto.pause true;
226       win#buttonPLAY#misc#set_sensitive true;
227       win#buttonPAUSE#misc#set_sensitive false;));
228   ignore(win#buttonPLAY#connect#clicked 
229     (fun _ -> 
230       Auto.pause false;
231       Auto.step ();
232       win#buttonPLAY#misc#set_sensitive false;
233       win#buttonPAUSE#misc#set_sensitive true;));
234   ignore(win#buttonNEXT#connect#clicked 
235     (fun _ -> Auto.step ()));
236   Auto.pause true;
237   win#buttonPLAY#misc#set_sensitive true;
238   win#buttonPAUSE#misc#set_sensitive false;  
239   fill_win win elems;
240   win#toplevel#show ();
241   GtkThread.main ();
242   GMain.Timeout.remove redraw;
243 ;;
244