1 (* Copyright (C) 2003, HELM Team.
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.
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.
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.
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,
23 * For details, see the HELM World-Wide-Web page,
24 * http://cs.unibo.it/helm/.
28 Cic.context * (int * Cic.term * bool * int * (int * Cic.term) list) list *
29 (int * Cic.term * int) list *
31 let fake_goal = Cic.Implicit None;;
32 let fake_candidates = [];;
40 ProofEngineReduction.replace
41 ~equality:(fun a b -> match b with Cic.Meta _ -> true | _ -> false)
42 ~what:[Cic.Rel 1] ~with_what:[Cic.Implicit None] ~where:t
44 ApplyTransformation.txt_of_cic_term ~map_unicode_to_tex:false
47 let names = List.map (function None -> None | Some (x,_) -> Some x) c in
48 let txt_t = CicPp.pp t names in
49 Pcre.replace ~pat:"\\?(\\d+)\\[[^]]*\\]" ~templ:"?<sub>$1</sub>" txt_t
51 let pp_goal context x =
52 if x == fake_goal then "" else pp context x
54 let pp_candidate context x = pp context x
56 let sublist start len l =
57 let rec aux pos len = function
58 | [] when pos < start -> aux (pos+1) len []
60 (0,fake_goal, false, 0, fake_candidates) :: aux (pos+1) (len-1) []
61 | [] (* when len <= 0 *) -> []
62 | he::tl when pos < start -> aux (pos+1) len tl
63 | he::tl when pos >= start && len > 0 -> he::aux (pos+1) (len-1) tl
64 | he::tl (* when pos >= start && len <= 0 *) -> []
69 let cell_of_candidate height context ?(active=false) g id c =
70 let tooltip = GData.tooltips () in (* should be only one isn't it? *)
73 ~label:(pp_candidate context c(* ^ " - " ^ string_of_int id*))
76 button#misc#set_size_request ~height ();
78 button#misc#set_sensitive false;
80 "Follow computation of "^pp_candidate context c^" on "^pp_goal context g
82 tooltip#set_tip ~text (button :> GObj.widget);
83 ignore(button#connect#clicked
85 let menu = GMenu.menu () in
86 let follow = GMenu.menu_item ~label:"Follow" () in
87 let prune = GMenu.menu_item ~label:"Prune" () in
88 ignore (follow#connect#activate
89 (fun _ -> HLog.warn (string_of_int id); Auto.give_hint id));
90 ignore (prune#connect#activate
91 (fun _ -> HLog.warn (string_of_int id); Auto.give_prune_hint id));
94 menu#popup 0 (GtkMain.Main.get_current_event_time ())));
97 let cell_of_goal height win_width context goal =
99 ~markup:(pp_goal context goal) ~xalign:0.0
100 ~width:(min (win_width * 60 / 100) 500)
106 let cell_of_row_header height n k id =
108 ~markup:("<span stretch=\"ultracondensed\">" ^ string_of_int n ^ "<sub>(" ^
109 string_of_int id ^ "|" ^ string_of_int k ^ ")</sub></span>")
110 ~line_wrap:true ~justify:`LEFT ~height ~width:80 ()
112 let cell_of_candidates height grey context goal cads =
113 let hbox = GPack.hbox () in
118 (cell_of_candidate height ~active:grey
119 context goal id c :> GObj.widget);
122 hbox#pack (cell_of_candidate height context goal id c :> GObj.widget)) tl;
126 let elems_to_rows height context win_width (table : GPack.table) (or_list) =
127 let height = height / ((List.length or_list) + 1) in
130 (fun position (goal_id, goal, grey, depth, candidates) ->
131 table#attach ~left:0 ~top:position
132 (cell_of_row_header height (position + !start)
133 depth goal_id :> GObj.widget);
134 table#attach ~left:1 ~top:position ~fill:`BOTH
135 (cell_of_goal height win_width context goal :> GObj.widget);
136 table#attach ~left:2 ~top:position
137 (cell_of_candidates height grey context goal candidates :> GObj.widget);
144 let old_displayed_status = ref [];;
145 let old_size = ref 0;;
147 let fill_win (win : MatitaGeneratedGui.autoWin) cb =
148 let init = Unix.gettimeofday () in
150 let (status : status) = cb () in
151 let win_size = win#toplevel#misc#allocation.Gtk.width in
152 let ctx, or_list, and_list, last_moves = status in
153 let displayed_status =
155 (or_list @ (List.map (fun (id,x,d) -> id,x,false,d,[]) and_list))
157 if displayed_status <> !old_displayed_status || !old_size <> win_size then
159 old_displayed_status := displayed_status;
160 old_size := win_size;
161 win#labelLAST#set_text
162 (String.concat ";" (List.map (pp_candidate ctx) last_moves));
163 List.iter win#table#remove win#table#children;
164 let height = win#viewportAREA#misc#allocation.Gtk.height in
165 elems_to_rows height ctx win_size win#table displayed_status;
167 "REDRAW COST: %2.1f\n%!" (Unix.gettimeofday () -. init);
169 with exn -> prerr_endline (Printexc.to_string exn); ()
172 let auto_dialog elems =
173 let win = new MatitaGeneratedGui.autoWin () in
174 let width = Gdk.Screen.width () in
175 let height = Gdk.Screen.height () in
176 let main_w = width * 70 / 100 in
177 let main_h = height * 60 / 100 in
178 win#toplevel#resize ~width:main_w ~height:main_h;
179 win#check_widgets ();
180 win#table#set_columns 3;
181 win#table#set_col_spacings 6;
182 win#table#set_row_spacings 4;
183 ignore(win#buttonUP#connect#clicked
184 (fun _ -> start := max 0 (!start -1); fill_win win elems));
185 ignore(win#buttonDOWN#connect#clicked
186 (fun _ -> incr start; fill_win win elems));
187 ignore(win#buttonCLOSE#connect#clicked
191 win#toplevel#destroy ();
192 GMain.Main.quit ()));
193 ignore(win#toplevel#event#connect#delete
197 win#toplevel#destroy ();
198 GMain.Main.quit ();true));
199 let redraw_callback _ = fill_win win elems;true in
200 let redraw = GMain.Timeout.add ~ms:400 ~callback:redraw_callback in
201 ignore(win#buttonPAUSE#connect#clicked
204 win#buttonPLAY#misc#set_sensitive true;
205 win#buttonPAUSE#misc#set_sensitive false;));
206 ignore(win#buttonPLAY#connect#clicked
210 win#buttonPLAY#misc#set_sensitive false;
211 win#buttonPAUSE#misc#set_sensitive true;));
212 ignore(win#buttonNEXT#connect#clicked
213 (fun _ -> Auto.step ()));
215 win#buttonPLAY#misc#set_sensitive true;
216 win#buttonPAUSE#misc#set_sensitive false;
218 win#toplevel#show ();
220 GMain.Timeout.remove redraw;