helm/matita/matita.ml

   1 (* Copyright (C) 2004, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26 open Printf
  27
  28 open MatitaGtkMisc
  29 open MatitaTypes
  30 open MatitaMisc
  31
  32 (** {2 Internal status} *)
  33
  34 let (get_proof, set_proof, has_proof) =
  35   let (current_proof: MatitaTypes.proof option ref) = ref None in
  36   ((fun () -> (* get_proof *)
  37     match !current_proof with
  38     | Some proof -> proof
  39     | None -> failwith "No current proof"),
  40    (fun proof ->  (* set_proof *)
  41       current_proof := proof),
  42    (fun () -> (* has_proof *)
  43       !current_proof <> None))
  44
  45 (** {2 Initialization} *)
  46
  47 let _ =
  48   Helm_registry.load_from "matita.conf.xml";
  49   GtkMain.Rc.add_default_file BuildTimeConf.gtkrc;
  50   GMain.Main.init ()
  51 let parserr = new MatitaDisambiguator.parserr ()
  52 let dbd =
  53   Mysql.quick_connect
  54     ~host:(Helm_registry.get "db.host")
  55     ~user:(Helm_registry.get "db.user")
  56     ~database:(Helm_registry.get "db.database")
  57     ()
  58 let gui = MatitaGui.instance ()
  59 let disambiguator =
  60   new MatitaDisambiguator.disambiguator ~parserr ~dbd
  61     ~chooseUris:(interactive_user_uri_choice ~gui)
  62     ~chooseInterp:(interactive_interp_choice ~gui)
  63     ()
  64 let proof_viewer = MatitaMathView.proof_viewer_instance ()
  65 let sequent_viewer = MatitaMathView.sequent_viewer ~show:true ()
  66 let sequents_viewer =
  67   let set_goal goal =
  68     if not (has_proof ()) then assert false;
  69     (get_proof ())#set_goal goal
  70   in
  71   MatitaMathView.sequents_viewer ~notebook:gui#main#sequentsNotebook
  72     ~sequent_viewer ~set_goal ()
  73
  74 let new_proof (proof: MatitaTypes.proof) =
  75   let proof_observer _ (status, ()) =
  76     let ((uri_opt, _, _, _), _) = status in
  77     proof_viewer#load_proof status;
  78   in
  79   let sequents_observer _ (((_, metasenv, _, _), goal_opt), ()) =
  80     sequents_viewer#reset;
  81     (match goal_opt with
  82     | None -> ()
  83     | Some goal ->
  84         sequents_viewer#load_sequents metasenv;
  85         sequents_viewer#goto_sequent goal)
  86   in
  87   ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events
  88     sequents_observer);
  89   ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events
  90     proof_observer);
  91   proof#notify;
  92   set_proof (Some proof)
  93
  94 let quit () = (* quit program, asking for confirmation if needed *)
  95   if not (has_proof ()) ||
  96     (ask_confirmation ~gui
  97       ~msg:("Proof in progress, are you sure you want to quit?") ())
  98   then
  99     GMain.Main.quit ()
 100
 101 let abort_proof () =
 102   if has_proof () then begin
 103     set_proof None;
 104     sequents_viewer#reset
 105   end
 106
 107 let proof_handler =
 108   { MatitaTypes.get_proof = get_proof;
 109     MatitaTypes.abort_proof = abort_proof;
 110     MatitaTypes.set_proof = set_proof;
 111     MatitaTypes.has_proof = has_proof;
 112     MatitaTypes.new_proof = new_proof;
 113     MatitaTypes.quit = quit;
 114   }
 115
 116 let interpreter =
 117   let console = gui#console in
 118   new MatitaInterpreter.interpreter
 119     ~disambiguator ~proof_handler ~console ~dbd ()
 120
 121 (** {2 Script window handling} *)
 122
 123 let script_forward _ =
 124   let buf = gui#script#scriptTextView#buffer in
 125   let locked_iter = buf#get_iter_at_mark (`NAME "locked") in
 126   if
 127     interpreter#evalPhrase
 128       (buf#get_text ~start:locked_iter ~stop:buf#end_iter ());
 129   then
 130     gui#lockScript (locked_iter#offset + interpreter#endOffset)
 131
 132 let script_jump _ =
 133   let buf = gui#script#scriptTextView#buffer in
 134   let locked_iter = buf#get_iter_at_mark (`NAME "locked") in
 135   let cursor_iter = buf#get_iter_at_mark (`NAME "insert") in
 136   let raw_text = buf#get_text ~start:locked_iter ~stop:cursor_iter () in
 137   let len = String.length raw_text in
 138   let rec parse offset =
 139     if offset < len then begin
 140       if
 141         interpreter#evalPhrase (String.sub raw_text offset (len - offset))
 142       then begin
 143         let new_offset = interpreter#endOffset + offset in
 144         gui#lockScript (new_offset + locked_iter#offset);
 145         parse new_offset
 146       end else
 147         raise Exit
 148     end
 149   in
 150   try
 151     parse 0
 152   with Exit -> ()
 153
 154 let script_back _ = not_implemented "script_back"
 155
 156 let load_script fname =
 157   gui#script#scriptTextView#buffer#set_text (input_file fname);
 158   gui#script#scriptWin#show ();
 159   gui#main#showScriptMenuItem#set_active true
 160
 161 (** {2 GUI callbacks} *)
 162
 163 let _ =
 164   gui#setQuitCallback quit;
 165   gui#setPhraseCallback interpreter#evalPhrase;
 166   gui#main#debugMenu#misc#hide ();
 167   ignore (gui#main#newProofMenuItem#connect#activate (fun _ ->
 168     gui#console#clear ();
 169     gui#console#show ~msg:"theorem " ()));
 170   ignore (gui#main#openMenuItem#connect#activate (fun _ ->
 171     match gui#chooseFile () with
 172     | None -> ()
 173     | Some f when is_proof_script f -> load_script f
 174     | Some f ->
 175         gui#console#echo_error (sprintf
 176           "Don't know what to do with file: %s\nUnrecognized file format."
 177           f)));
 178   connect_button gui#script#scriptWinForwardButton script_forward;
 179   connect_button gui#script#scriptWinBackButton script_back;
 180   connect_button gui#script#scriptWinJumpButton script_jump;
 181   let module A = TacticAst in
 182   let hole = CicAst.UserInput in
 183   let tac ast _ = ignore (interpreter#evalAst (A.Tactic ast)) in
 184   let tac_w_term ast _ =
 185     gui#console#clear ();
 186     gui#console#show ~msg:(TacticAstPp.pp_tactic ast) ();
 187     gui#main#mainWin#present ()
 188   in
 189   let tbar = gui#toolbar in
 190   connect_button tbar#introsButton (tac (A.Intros (None, [])));
 191   connect_button tbar#applyButton (tac_w_term (A.Apply hole));
 192   connect_button tbar#exactButton (tac_w_term (A.Exact hole));
 193   connect_button tbar#elimButton (tac_w_term (A.Elim (hole, None)));
 194   connect_button tbar#elimTypeButton (tac_w_term (A.ElimType hole));
 195   connect_button tbar#splitButton (tac A.Split);
 196   connect_button tbar#leftButton (tac A.Left);
 197   connect_button tbar#rightButton (tac A.Right);
 198   connect_button tbar#existsButton (tac A.Exists);
 199   connect_button tbar#reflexivityButton (tac A.Reflexivity);
 200   connect_button tbar#symmetryButton (tac A.Symmetry);
 201   connect_button tbar#transitivityButton (tac_w_term (A.Transitivity hole));
 202
 203 (*   connect_button tbar#simplifyButton FINQUI; *)
 204
 205   connect_button tbar#assumptionButton (tac A.Assumption);
 206   connect_button tbar#cutButton (tac_w_term (A.Cut hole));
 207   connect_button tbar#autoButton (tac A.Auto)
 208
 209   (** <DEBUGGING> *)
 210
 211 let _ =
 212   if BuildTimeConf.debug then begin
 213     gui#main#debugMenu#misc#show ();
 214     let addDebugItem ~label callback =
 215       let item =
 216         GMenu.menu_item ~packing:gui#main#debugMenu_menu#append ~label ()
 217       in
 218       ignore (item#connect#activate callback)
 219     in
 220     addDebugItem "toggle auto disambiguation" (fun _ ->
 221       Helm_registry.set_bool "matita.auto_disambiguation"
 222         (not (Helm_registry.get_bool "matita.auto_disambiguation")));
 223     addDebugItem "dump proof status to stdout" (fun _ ->
 224       print_endline ((get_proof ())#toString));
 225     addDebugItem "print selected terms" (fun () ->
 226       let i = ref 0 in
 227       List.iter
 228         (fun t -> incr i; debug_print (sprintf "%d: %s" !i (CicPp.ppterm t)))
 229         sequent_viewer#get_selected_terms)
 230   end
 231
 232   (** </DEBUGGING> *)
 233
 234 let _ =
 235   (try
 236     load_script Sys.argv.(1)
 237   with Invalid_argument _ -> ());
 238   GtkThread.main ()
 239