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) list) list *
  29   (int * Cic.term * int) list *
  30   Cic.term 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   (Pcre.replace ~pat:"<" ~templ:"&lt;"
  53    (Pcre.replace ~pat:">" ~templ:"&gt;"
  54     (ApplyTransformation.txt_of_cic_term ~map_unicode_to_tex:false
  55       max_int [] c t)))^
  56   (if size > 0 then "</span>" else "")
  57 ;;
  58 let pp_goal context x =
  59   if x == fake_goal then "" else pp context x
  60 ;;
  61 let pp_candidate context x = pp context x
  62 let pp_candidate_tip context x = pp ~size:0 context x
  63 let pp_candidate_type context x =
  64   try
  65     let ty, _ =
  66       CicTypeChecker.type_of_aux' [] ~subst:[]
  67        context x CicUniv.oblivion_ugraph
  68     in
  69       pp ~size:0 context ty
  70   with CicUtil.Meta_not_found _ ->  pp ~size:0 context x
  71 ;;
  72
  73 let sublist start len l =
  74   let rec aux pos len = function
  75     | [] when pos < start -> aux (pos+1) len []
  76     | [] when len > 0 ->
  77           (0,fake_goal, false, 0, fake_candidates) :: aux (pos+1) (len-1) []
  78     | [] (* when len <= 0 *) -> []
  79     | he::tl when pos < start -> aux (pos+1) len tl
  80     | he::tl when pos >= start && len > 0 -> he::aux (pos+1) (len-1) tl
  81     | he::tl (* when pos >= start && len <= 0 *) -> []
  82   in
  83   aux 0 len l
  84 ;;
  85
  86 let cell_of_candidate height context ?(active=false) g id c =
  87   let tooltip = GData.tooltips () in (* should be only one isn't it? *)
  88   let button = GButton.button () in
  89   let l = GMisc.label ~markup:(pp_candidate context c) () in
  90   button#add l#coerce;
  91   button#misc#set_size_request ~height ();
  92   if active then
  93     button#misc#set_sensitive false;
  94   let text =
  95     "Follow/Prune computation of\n"^pp_candidate_tip context c^": "^
  96     pp_candidate_type context c
  97   in
  98   tooltip#set_tip ~text (button :> GObj.widget);
  99   ignore(button#connect#clicked
 100     (fun _ ->
 101       let menu = GMenu.menu () in
 102       let follow = GMenu.menu_item ~label:"Follow" () in
 103       let prune = GMenu.menu_item ~label:"Prune" () in
 104       ignore (follow#connect#activate
 105         (fun _ -> HLog.warn (string_of_int id); Auto.give_hint id));
 106       ignore (prune#connect#activate
 107         (fun _ -> HLog.warn (string_of_int id); Auto.give_prune_hint id));
 108       menu#append follow;
 109       menu#append prune;
 110       menu#popup 0 (GtkMain.Main.get_current_event_time ())));
 111   button
 112 ;;
 113 let cell_of_goal height win_width context goal =
 114   GMisc.label
 115     ~markup:(pp_goal context goal) ~xalign:0.0
 116     ~width:(min (win_width * 30 / 100) 500)
 117     ~line_wrap:false
 118     ~ellipsize:`END
 119     ~height
 120     ()
 121 ;;
 122 let cell_of_row_header height n k id =
 123   GMisc.label
 124     ~markup:("<span stretch=\"ultracondensed\">" ^ string_of_int n ^ "<sub>(" ^
 125              string_of_int id ^ "|" ^ string_of_int k ^ ")</sub></span>")
 126     ~line_wrap:true ~justify:`LEFT ~height ~width:80 ()
 127 ;;
 128 let cell_of_candidates height grey context goal cads =
 129   let hbox = GPack.hbox () in
 130   match cads with
 131   | [] -> hbox
 132   | (id,c)::tl ->
 133       hbox#pack
 134         (cell_of_candidate height ~active:grey
 135           context goal id c :> GObj.widget);
 136       List.iter
 137         (fun (id,c) ->
 138         hbox#pack (cell_of_candidate height context goal id c :> GObj.widget)) tl;
 139         hbox
 140 ;;
 141
 142 let elems_to_rows height context win_width (table : GPack.table) (or_list) =
 143   let height = height / ((List.length or_list) + 1) in
 144   let _ =
 145    List.fold_left
 146     (fun position (goal_id, goal, grey, depth, candidates) ->
 147       table#attach ~left:0 ~top:position
 148         (cell_of_row_header height (position + !start)
 149           depth goal_id :> GObj.widget);
 150       table#attach ~left:1 ~top:position ~fill:`BOTH
 151         (cell_of_goal height win_width context goal :> GObj.widget);
 152       table#attach ~left:2 ~top:position
 153         (cell_of_candidates height grey context goal candidates :> GObj.widget);
 154       position+1)
 155     0 or_list
 156   in
 157   ()
 158 ;;
 159
 160 let old_displayed_status = ref [];;
 161 let old_size = ref 0;;
 162
 163 let fill_win (win : MatitaGeneratedGui.autoWin) cb =
 164   let init = Unix.gettimeofday () in
 165     try
 166       let (status : status) = cb () in
 167       let win_size = win#toplevel#misc#allocation.Gtk.width in
 168       let ctx, or_list, and_list, last_moves = status in
 169       let displayed_status =
 170         sublist !start !len
 171           (or_list @ (List.map (fun (id,x,d) -> id,x,false,d,[]) and_list))
 172       in
 173       if displayed_status <> !old_displayed_status || !old_size <> win_size then
 174         begin
 175           old_displayed_status := displayed_status;
 176           old_size := win_size;
 177 (*
 178           win#labelLAST#set_text
 179             (String.concat ";" (List.map (pp_candidate ctx) last_moves));
 180 *)
 181           List.iter win#table#remove win#table#children;
 182           let height = win#viewportAREA#misc#allocation.Gtk.height in
 183           elems_to_rows height ctx win_size win#table displayed_status;
 184           Printf.eprintf
 185             "REDRAW COST: %2.1f\n%!" (Unix.gettimeofday () -.  init);
 186         end
 187     with exn -> prerr_endline (Printexc.to_string exn); ()
 188 ;;
 189
 190 let auto_dialog elems =
 191   let win = new MatitaGeneratedGui.autoWin () in
 192   let width = Gdk.Screen.width () in
 193   let height = Gdk.Screen.height () in
 194   let main_w = width * 70 / 100 in
 195   let main_h = height * 60 / 100 in
 196   win#toplevel#resize ~width:main_w ~height:main_h;
 197   win#check_widgets ();
 198   win#table#set_columns 3;
 199   win#table#set_col_spacings 6;
 200   win#table#set_row_spacings 4;
 201   ignore(win#buttonUP#connect#clicked
 202     (fun _ -> start := max 0 (!start -1); fill_win win elems));
 203   ignore(win#buttonDOWN#connect#clicked
 204     (fun _ -> incr start; fill_win win elems));
 205   ignore(win#buttonCLOSE#connect#clicked
 206     (fun _ ->
 207       Auto.pause false;
 208       Auto.step ();
 209       win#toplevel#destroy ();
 210       GMain.Main.quit ()));
 211   ignore(win#toplevel#event#connect#delete
 212     (fun _ ->
 213       Auto.pause false;
 214       Auto.step ();
 215       win#toplevel#destroy ();
 216       GMain.Main.quit ();true));
 217   let redraw_callback _ = fill_win win elems;true in
 218   let redraw = GMain.Timeout.add ~ms:400 ~callback:redraw_callback in
 219   ignore(win#buttonPAUSE#connect#clicked
 220     (fun _ ->
 221       Auto.pause true;
 222       win#buttonPLAY#misc#set_sensitive true;
 223       win#buttonPAUSE#misc#set_sensitive false;));
 224   ignore(win#buttonPLAY#connect#clicked
 225     (fun _ ->
 226       Auto.pause false;
 227       Auto.step ();
 228       win#buttonPLAY#misc#set_sensitive false;
 229       win#buttonPAUSE#misc#set_sensitive true;));
 230   ignore(win#buttonNEXT#connect#clicked
 231     (fun _ -> Auto.step ()));
 232   Auto.pause true;
 233   win#buttonPLAY#misc#set_sensitive true;
 234   win#buttonPAUSE#misc#set_sensitive false;
 235   fill_win win elems;
 236   win#toplevel#show ();
 237   GtkThread.main ();
 238   GMain.Timeout.remove redraw;
 239 ;;
 240