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 * (Cic.term * (int * Cic.term) list) list * Cic.term list *
  29   Cic.term list
  30 let fake_goal = Cic.Implicit None;;
  31 let fake_candidates = [];;
  32
  33 let start = ref 0;;
  34 let len = ref 10;;
  35
  36 let pp c t =
  37   let names = List.map (function None -> None | Some (n,_) -> Some n) c in
  38   let t =
  39     ProofEngineReduction.replace
  40       ~equality:(fun a b -> match b with Cic.Meta _ -> true | _ -> false)
  41       ~what:[Cic.Rel 1] ~with_what:[Cic.Implicit None] ~where:t
  42   in
  43   CicPp.pp t names
  44 ;;
  45 let pp_goal context x =
  46   if x == fake_goal then "" else pp context x
  47 ;;
  48 let pp_candidate context x = pp context x
  49
  50 let sublist start len l =
  51   let rec aux pos len = function
  52     | [] when pos < start -> aux (pos+1) len []
  53     | [] when len > 0 -> (fake_goal, fake_candidates) :: aux (pos+1) (len-1) []
  54     | [] (* when len <= 0 *) -> []
  55     | he::tl when pos < start -> aux (pos+1) len tl
  56     | he::tl when pos >= start && len > 0 -> he::aux (pos+1) (len-1) tl
  57     | he::tl (* when pos >= start && len <= 0 *) -> []
  58   in
  59   aux 0 len l
  60 ;;
  61
  62 let cell_of_candidate context ?(active=false) g id c =
  63   let tooltip = GData.tooltips () in (* should be only one isn't it? *)
  64   let button =
  65     GButton.button
  66       ~label:(pp_candidate context c(* ^ " - " ^ string_of_int id*)) ()
  67   in
  68   if active then
  69     button#misc#set_sensitive false;
  70   let text =
  71     "Follow computation of "^pp_candidate context c^" on "^pp_goal context g
  72   in
  73   tooltip#set_tip ~text (button :> GObj.widget);
  74   ignore(button#connect#clicked
  75     (fun _ -> HLog.warn (string_of_int id); Auto.give_hint id));
  76   button
  77 ;;
  78 let cell_of_goal win_width context goal =
  79   GMisc.label ~text:(pp_goal context goal) ~xalign:0.0 ()
  80 ;;
  81 let cell_of_int n =
  82   GMisc.label ~text:(string_of_int n)
  83     ~line_wrap:true ~justify:`RIGHT ()
  84 ;;
  85 let cell_of_candidates context goal cads =
  86   let hbox = GPack.hbox () in
  87   match cads with
  88   | [] -> hbox
  89   | (id,c)::tl ->
  90       hbox#pack
  91         (cell_of_candidate ~active:true context goal id c :> GObj.widget);
  92       List.iter
  93         (fun (id,c) ->
  94         hbox#pack (cell_of_candidate context goal id c :> GObj.widget)) tl;
  95         hbox
  96 ;;
  97
  98 let elems_to_rows context win_width (table : GPack.table) (or_list) =
  99   let _ =
 100    List.fold_left
 101     (fun position (goal, candidates) ->
 102       table#attach ~left:0 ~top:position
 103         (cell_of_int (position + !start) :> GObj.widget);
 104       table#attach ~left:1 ~top:position ~expand:`BOTH ~fill:`BOTH
 105         (cell_of_goal win_width context goal :> GObj.widget);
 106       table#attach ~left:2 ~top:position
 107         (cell_of_candidates context goal candidates :> GObj.widget);
 108       position+1)
 109     0 or_list
 110   in
 111   ()
 112 ;;
 113
 114 let old_displayed_status = ref ([]);;
 115 let old_size = ref 0;;
 116
 117 let fill_win (win : MatitaGeneratedGui.autoWin) cb =
 118   let init = Unix.gettimeofday () in
 119     try
 120       let (status : status) = cb () in
 121       let win_size = win#toplevel#misc#allocation.Gtk.width in
 122       let ctx, or_list, and_list, last_moves = status in
 123       let displayed_status =
 124         sublist !start !len (or_list @ (List.map (fun x -> x,[]) and_list))
 125       in
 126       if displayed_status <> !old_displayed_status || !old_size <> win_size then
 127         begin
 128           old_displayed_status := displayed_status;
 129           old_size := win_size;
 130           win#labelLAST#set_text
 131             (String.concat ";" (List.map (pp_candidate ctx) last_moves));
 132           List.iter win#table#remove win#table#children;
 133           elems_to_rows ctx win_size win#table displayed_status;
 134           Printf.eprintf
 135             "REDRAW COST: %2.1f\n%!" (Unix.gettimeofday () -.  init);
 136         end
 137     with exn -> prerr_endline (Printexc.to_string exn); ()
 138 ;;
 139
 140 let auto_dialog elems =
 141   let win = new MatitaGeneratedGui.autoWin () in
 142   win#check_widgets ();
 143   win#table#set_columns 3;
 144   win#table#set_col_spacings 6;
 145   win#table#set_row_spacings 4;
 146   ignore(win#buttonUP#connect#clicked
 147     (fun _ -> start := max 0 (!start -1); fill_win win elems));
 148   ignore(win#buttonDOWN#connect#clicked
 149     (fun _ -> incr start; fill_win win elems));
 150   ignore(win#buttonCLOSE#connect#clicked
 151     (fun _ -> win#toplevel#destroy ();GMain.Main.quit ()));
 152   let redraw_callback _ = fill_win win elems;true in
 153   let redraw = GMain.Timeout.add ~ms:400 ~callback:redraw_callback in
 154   ignore(win#buttonPAUSE#connect#clicked
 155     (fun _ -> Auto.pause true));
 156   ignore(win#buttonPLAY#connect#clicked
 157     (fun _ -> Auto.pause false;Auto.step ()));
 158   ignore(win#buttonNEXT#connect#clicked
 159     (fun _ -> Auto.step ()));
 160   fill_win win elems;
 161   win#toplevel#show ();
 162   GtkThread.main ();
 163   GMain.Timeout.remove redraw;
 164 ;;
 165