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 _ = MetadataDb.clean ~dbd ~owner:(Helm_registry.get "matita.owner")
  59 let gui = MatitaGui.instance ()
  60 let disambiguator =
  61   new MatitaDisambiguator.disambiguator ~parserr ~dbd
  62     ~chooseUris:(interactive_user_uri_choice ~gui)
  63     ~chooseInterp:(interactive_interp_choice ~gui)
  64     ()
  65 let proof_viewer = MatitaMathView.proof_viewer_instance ()
  66 let sequent_viewer = MatitaMathView.sequent_viewer ~show:true ()
  67 let sequents_viewer =
  68   let set_goal goal =
  69     if not (has_proof ()) then assert false;
  70     (get_proof ())#set_goal goal
  71   in
  72   MatitaMathView.sequents_viewer ~notebook:gui#main#sequentsNotebook
  73     ~sequent_viewer ~set_goal ()
  74
  75 let new_proof (proof: MatitaTypes.proof) =
  76   let proof_observer _ (status, ()) =
  77     let ((uri_opt, _, _, _), _) = status in
  78     proof_viewer#load_proof status;
  79   in
  80   let sequents_observer _ (((_, metasenv, _, _), goal_opt), ()) =
  81     sequents_viewer#reset;
  82     (match goal_opt with
  83     | None -> ()
  84     | Some goal ->
  85         sequents_viewer#load_sequents metasenv;
  86         sequents_viewer#goto_sequent goal)
  87   in
  88   ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events
  89     sequents_observer);
  90   ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events
  91     proof_observer);
  92   proof#notify;
  93   set_proof (Some proof)
  94
  95 let quit () = (* quit program, asking for confirmation if needed *)
  96   if not (has_proof ()) ||
  97     (ask_confirmation ~gui
  98       ~msg:("Proof in progress, are you sure you want to quit?") ())
  99   then
 100     GMain.Main.quit ()
 101
 102 let abort_proof () =
 103   if has_proof () then begin
 104     set_proof None;
 105     sequents_viewer#reset
 106   end
 107
 108 let proof_handler =
 109   { MatitaTypes.get_proof = get_proof;
 110     MatitaTypes.abort_proof = abort_proof;
 111     MatitaTypes.set_proof = set_proof;
 112     MatitaTypes.has_proof = has_proof;
 113     MatitaTypes.new_proof = new_proof;
 114     MatitaTypes.quit = quit;
 115   }
 116
 117 let interpreter =
 118   let console = (gui#console :> MatitaTypes.console) in
 119   new MatitaInterpreter.interpreter
 120     ~disambiguator ~proof_handler ~console ~dbd ()
 121
 122 (** {2 Script window handling} *)
 123
 124 let script_forward _ =
 125   let buf = gui#script#scriptTextView#buffer in
 126   let locked_iter = buf#get_iter_at_mark (`NAME "locked") in
 127   if
 128     interpreter#evalPhrase
 129       (buf#get_text ~start:locked_iter ~stop:buf#end_iter ());
 130   then
 131     gui#lockScript (locked_iter#offset + interpreter#endOffset)
 132
 133 let script_jump _ =
 134   let buf = gui#script#scriptTextView#buffer in
 135   let locked_iter = buf#get_iter_at_mark (`NAME "locked") in
 136   let cursor_iter = buf#get_iter_at_mark (`NAME "insert") in
 137   let raw_text = buf#get_text ~start:locked_iter ~stop:cursor_iter () in
 138   let len = String.length raw_text in
 139   let rec parse offset =
 140     if offset < len then begin
 141       if
 142         interpreter#evalPhrase (String.sub raw_text offset (len - offset))
 143       then begin
 144         let new_offset = interpreter#endOffset + offset in
 145         gui#lockScript (new_offset + locked_iter#offset);
 146         parse new_offset
 147       end else
 148         raise Exit
 149     end
 150   in
 151   try
 152     parse 0
 153   with Exit -> ()
 154
 155 let script_back _ = not_implemented "script_back"
 156
 157 let load_script fname =
 158   gui#script#scriptTextView#buffer#set_text (input_file fname);
 159   gui#script#scriptWin#show ();
 160   gui#main#showScriptMenuItem#set_active true
 161
 162 (** {2 GUI callbacks} *)
 163
 164 let _ =
 165   gui#setQuitCallback quit;
 166   gui#setPhraseCallback interpreter#evalPhrase;
 167   gui#main#debugMenu#misc#hide ();
 168   ignore (gui#main#newProofMenuItem#connect#activate (fun _ ->
 169     gui#console#clear ();
 170     gui#console#show ~msg:"theorem " ()));
 171   ignore (gui#main#openMenuItem#connect#activate (fun _ ->
 172     match gui#chooseFile () with
 173     | None -> ()
 174     | Some f when is_proof_script f -> load_script f
 175     | Some f ->
 176         gui#console#echo_error (sprintf
 177           "Don't know what to do with file: %s\nUnrecognized file format."
 178           f)));
 179   connect_button gui#script#scriptWinForwardButton script_forward;
 180   connect_button gui#script#scriptWinBackButton script_back;
 181   connect_button gui#script#scriptWinJumpButton script_jump;
 182   let module A = TacticAst in
 183   let hole = CicAst.UserInput in
 184   let tac ast _ = ignore (interpreter#evalAst (A.Tactic ast)) in
 185   let tac_w_term ast _ =
 186     gui#console#clear ();
 187     gui#console#show ~msg:(TacticAstPp.pp_tactic ast) ();
 188     gui#main#mainWin#present ()
 189   in
 190   let tbar = gui#toolbar in
 191   connect_button tbar#introsButton (tac (A.Intros (None, [])));
 192   connect_button tbar#applyButton (tac_w_term (A.Apply hole));
 193   connect_button tbar#exactButton (tac_w_term (A.Exact hole));
 194   connect_button tbar#elimButton (tac_w_term (A.Elim (hole, None)));
 195   connect_button tbar#elimTypeButton (tac_w_term (A.ElimType hole));
 196   connect_button tbar#splitButton (tac A.Split);
 197   connect_button tbar#leftButton (tac A.Left);
 198   connect_button tbar#rightButton (tac A.Right);
 199   connect_button tbar#existsButton (tac A.Exists);
 200   connect_button tbar#reflexivityButton (tac A.Reflexivity);
 201   connect_button tbar#symmetryButton (tac A.Symmetry);
 202   connect_button tbar#transitivityButton (tac_w_term (A.Transitivity hole));
 203
 204 (*   connect_button tbar#simplifyButton FINQUI; *)
 205
 206   connect_button tbar#assumptionButton (tac A.Assumption);
 207   connect_button tbar#cutButton (tac_w_term (A.Cut hole));
 208   connect_button tbar#autoButton (tac A.Auto)
 209
 210   (** <DEBUGGING> *)
 211
 212 let _ =
 213   if BuildTimeConf.debug then begin
 214     gui#main#debugMenu#misc#show ();
 215     let addDebugItem ~label callback =
 216       let item =
 217         GMenu.menu_item ~packing:gui#main#debugMenu_menu#append ~label ()
 218       in
 219       ignore (item#connect#activate callback)
 220     in
 221     addDebugItem "toggle auto disambiguation" (fun _ ->
 222       Helm_registry.set_bool "matita.auto_disambiguation"
 223         (not (Helm_registry.get_bool "matita.auto_disambiguation")));
 224     addDebugItem "dump proof status to stdout" (fun _ ->
 225       print_endline ((get_proof ())#toString));
 226     addDebugItem "dump environment to \"env.dump\"" (fun _ ->
 227       let oc = open_out "env.dump" in
 228       CicEnvironment.dump_to_channel oc;
 229       close_out oc);
 230     addDebugItem "print selected terms" (fun () ->
 231       let i = ref 0 in
 232       List.iter
 233         (fun t -> incr i; debug_print (sprintf "%d: %s" !i (CicPp.ppterm t)))
 234         sequent_viewer#get_selected_terms)
 235   end
 236
 237   (** </DEBUGGING> *)
 238
 239 let _ =
 240 (*   CicEnvironment.set_trust (fun _ -> false); *)
 241   (try
 242     load_script Sys.argv.(1)
 243   with Invalid_argument _ -> ());
 244   GtkThread.main ()
 245