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 let pp c t =
  38   (*
  39   let t =
  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
  43   in
  44     ApplyTransformation.txt_of_cic_term ~map_unicode_to_tex:false
  45       max_int [] c t
  46   *)
  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
  50 ;;
  51 let pp_goal context x =
  52   if x == fake_goal then "" else pp context x
  53 ;;
  54 let pp_candidate context x = pp context x
  55
  56 let sublist start len l =
  57   let rec aux pos len = function
  58     | [] when pos < start -> aux (pos+1) len []
  59     | [] when len > 0 ->
  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 *) -> []
  65   in
  66   aux 0 len l
  67 ;;
  68
  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? *)
  71   let button =
  72     GButton.button
  73       ~label:(pp_candidate context c(* ^ " - " ^ string_of_int id*))
  74       ()
  75   in
  76   button#misc#set_size_request ~height ();
  77   if active then
  78     button#misc#set_sensitive false;
  79   let text =
  80     "Follow computation of "^pp_candidate context c^" on "^pp_goal context g
  81   in
  82   tooltip#set_tip ~text (button :> GObj.widget);
  83   ignore(button#connect#clicked
  84     (fun _ -> HLog.warn (string_of_int id); Auto.give_hint id));
  85   button
  86 ;;
  87 let cell_of_goal height win_width context goal =
  88   GMisc.label
  89     ~markup:(pp_goal context goal) ~xalign:0.0
  90     ~width:(min (win_width * 60 / 100) 500)
  91     ~line_wrap:false
  92     ~ellipsize:`END
  93     ~height
  94     ()
  95 ;;
  96 let cell_of_row_header height n k id =
  97   GMisc.label
  98     ~markup:("<span stretch=\"ultracondensed\">" ^ string_of_int n ^ "<sub>(" ^
  99              string_of_int id ^ "|" ^ string_of_int k ^ ")</sub></span>")
 100     ~line_wrap:true ~justify:`LEFT ~height ~width:80 ()
 101 ;;
 102 let cell_of_candidates height grey context goal cads =
 103   let hbox = GPack.hbox () in
 104   match cads with
 105   | [] -> hbox
 106   | (id,c)::tl ->
 107       hbox#pack
 108         (cell_of_candidate height ~active:grey
 109           context goal id c :> GObj.widget);
 110       List.iter
 111         (fun (id,c) ->
 112         hbox#pack (cell_of_candidate height context goal id c :> GObj.widget)) tl;
 113         hbox
 114 ;;
 115
 116 let elems_to_rows height context win_width (table : GPack.table) (or_list) =
 117   let height = height / (List.length or_list) in
 118   let _ =
 119    List.fold_left
 120     (fun position (goal_id, goal, grey, depth, candidates) ->
 121       table#attach ~left:0 ~top:position
 122         (cell_of_row_header height (position + !start)
 123           depth goal_id :> GObj.widget);
 124       table#attach ~left:1 ~top:position ~fill:`BOTH
 125         (cell_of_goal height win_width context goal :> GObj.widget);
 126       table#attach ~left:2 ~top:position
 127         (cell_of_candidates height grey context goal candidates :> GObj.widget);
 128       position+1)
 129     0 or_list
 130   in
 131   ()
 132 ;;
 133
 134 let old_displayed_status = ref [];;
 135 let old_size = ref 0;;
 136
 137 let fill_win (win : MatitaGeneratedGui.autoWin) cb =
 138   let init = Unix.gettimeofday () in
 139     try
 140       let (status : status) = cb () in
 141       let win_size = win#toplevel#misc#allocation.Gtk.width in
 142       let ctx, or_list, and_list, last_moves = status in
 143       let displayed_status =
 144         sublist !start !len
 145           (or_list @ (List.map (fun (id,x,d) -> id,x,false,d,[]) and_list))
 146       in
 147       if displayed_status <> !old_displayed_status || !old_size <> win_size then
 148         begin
 149           old_displayed_status := displayed_status;
 150           old_size := win_size;
 151           win#labelLAST#set_text
 152             (String.concat ";" (List.map (pp_candidate ctx) last_moves));
 153           List.iter win#table#remove win#table#children;
 154           let height = win#viewportAREA#misc#allocation.Gtk.height in
 155           elems_to_rows height ctx win_size win#table displayed_status;
 156           Printf.eprintf
 157             "REDRAW COST: %2.1f\n%!" (Unix.gettimeofday () -.  init);
 158         end
 159     with exn -> prerr_endline (Printexc.to_string exn); ()
 160 ;;
 161
 162 let auto_dialog elems =
 163   let win = new MatitaGeneratedGui.autoWin () in
 164   let width = Gdk.Screen.width () in
 165   let height = Gdk.Screen.height () in
 166   let main_w = width * 70 / 100 in
 167   let main_h = height * 60 / 100 in
 168   win#toplevel#resize ~width:main_w ~height:main_h;
 169   win#check_widgets ();
 170   win#table#set_columns 3;
 171   win#table#set_col_spacings 6;
 172   win#table#set_row_spacings 4;
 173   ignore(win#buttonUP#connect#clicked
 174     (fun _ -> start := max 0 (!start -1); fill_win win elems));
 175   ignore(win#buttonDOWN#connect#clicked
 176     (fun _ -> incr start; fill_win win elems));
 177   ignore(win#buttonCLOSE#connect#clicked
 178     (fun _ ->
 179       Auto.pause false;
 180       Auto.step ();
 181       win#toplevel#destroy ();
 182       GMain.Main.quit ()));
 183   let redraw_callback _ = fill_win win elems;true in
 184   let redraw = GMain.Timeout.add ~ms:400 ~callback:redraw_callback in
 185   ignore(win#buttonPAUSE#connect#clicked
 186     (fun _ ->
 187       Auto.pause true;
 188       win#buttonPLAY#misc#set_sensitive true;
 189       win#buttonPAUSE#misc#set_sensitive false;));
 190   ignore(win#buttonPLAY#connect#clicked
 191     (fun _ ->
 192       Auto.pause false;
 193       Auto.step ();
 194       win#buttonPLAY#misc#set_sensitive false;
 195       win#buttonPAUSE#misc#set_sensitive true;));
 196   ignore(win#buttonNEXT#connect#clicked
 197     (fun _ -> Auto.step ()));
 198   Auto.pause true;
 199   win#buttonPLAY#misc#set_sensitive true;
 200   win#buttonPAUSE#misc#set_sensitive false;
 201   fill_win win elems;
 202   win#toplevel#show ();
 203   GtkThread.main ();
 204   GMain.Timeout.remove redraw;
 205 ;;
 206