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 xmldump_observer _ _ =  print_endline proof#toString in
  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 (*
  93   ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events
  94     xmldump_observer);
  95 *)
  96   proof#notify;
  97   set_proof (Some proof)
  98
  99 let quit () = (* quit program, asking for confirmation if needed *)
 100   if not (has_proof ()) ||
 101     (ask_confirmation ~gui
 102       ~msg:("Proof in progress, are you sure you want to quit?") ())
 103   then
 104     GMain.Main.quit ()
 105
 106 let abort_proof () =
 107   if has_proof () then begin
 108     set_proof None;
 109     sequents_viewer#reset
 110   end
 111
 112 let proof_handler =
 113   { MatitaTypes.get_proof = get_proof;
 114     MatitaTypes.abort_proof = abort_proof;
 115     MatitaTypes.set_proof = set_proof;
 116     MatitaTypes.has_proof = has_proof;
 117     MatitaTypes.new_proof = new_proof;
 118     MatitaTypes.quit = quit;
 119   }
 120
 121 let interpreter =
 122   let console = gui#console in
 123   new MatitaInterpreter.interpreter ~disambiguator ~proof_handler ~console ()
 124
 125   (** prompt the user for the textual input of a term and disambiguate it *)
 126 let ask_term ?(title = "term input") ?(msg = "insert term") () =
 127   match gui#askText ~title ~msg () with
 128   | Some t ->
 129       let (_, _, term) = disambiguator#disambiguateTerm (Stream.of_string t) in
 130       Some term
 131   | None -> None
 132
 133 (** {2 Script window handling} *)
 134
 135 let script_forward _ =
 136   let buf = gui#script#scriptTextView#buffer in
 137   let locked_iter = buf#get_iter_at_mark (`NAME "locked") in
 138   interpreter#evalPhrase
 139     (buf#get_text ~start:locked_iter ~stop:buf#end_iter ());
 140   gui#lockScript (locked_iter#offset + interpreter#endOffset)
 141
 142 let script_jump _ =
 143   let buf = gui#script#scriptTextView#buffer in
 144   let locked_iter = buf#get_iter_at_mark (`NAME "locked") in
 145   let cursor_iter = buf#get_iter_at_mark (`NAME "insert") in
 146   let raw_text = buf#get_text ~start:locked_iter ~stop:cursor_iter () in
 147   let len = String.length raw_text in
 148   let rec parse offset =
 149     if offset < len then begin
 150       interpreter#evalPhrase ~transparent:true
 151         (String.sub raw_text offset (len - offset));
 152       let new_offset = interpreter#endOffset + offset in
 153       gui#lockScript (new_offset + locked_iter#offset);
 154       parse new_offset
 155     end
 156   in
 157   try
 158     parse 0
 159   with CicTextualParser2.Parse_error _ -> ()
 160
 161 let script_back _ = not_implemented "script_back"
 162
 163 let load_script fname =
 164   gui#script#scriptTextView#buffer#set_text (input_file fname);
 165   gui#script#scriptWin#show ();
 166   gui#main#showScriptMenuItem#set_active true
 167
 168 (** {2 GUI callbacks} *)
 169
 170 let _ =
 171   gui#setQuitCallback quit;
 172   gui#setPhraseCallback interpreter#evalPhrase;
 173   gui#main#debugMenu#misc#hide ();
 174   ignore (gui#main#newProofMenuItem#connect#activate (fun _ ->
 175    if has_proof () &&
 176       not (ask_confirmation ~gui
 177         ~msg:("Proof in progress, are you sure you want to start a new one?")
 178         ())
 179     then
 180       ()  (* abort new proof process *)
 181     else
 182       let input = ask_text ~gui ~msg:"Insert proof goal" ~multiline:true () in
 183       let (env, metasenv, expr) =
 184         disambiguator#disambiguateTerm (Stream.of_string input)
 185       in
 186       let proof = MatitaProof.proof ~typ:expr ~metasenv () in
 187       new_proof proof));
 188   ignore (gui#main#openMenuItem#connect#activate (fun _ ->
 189     match gui#chooseFile () with
 190     | None -> ()
 191     | Some f when is_proof_script f -> load_script f
 192     | Some f ->
 193         gui#console#echo_error (sprintf
 194           "Don't know what to do with file: %s\nUnrecognized file format."
 195           f)));
 196   ignore (gui#script#scriptWinForwardButton#connect#clicked script_forward);
 197   ignore (gui#script#scriptWinBackButton#connect#clicked script_back);
 198   ignore (gui#script#scriptWinJumpButton#connect#clicked script_jump);
 199   let tac_w_term name tac _ =
 200     match ask_term ~title:name ~msg:("term for " ^ name) () with
 201     | Some term -> (get_proof ())#apply_tactic (tac ~term)
 202     | None -> ()
 203   in
 204   let tac _ tac _ = (get_proof ())#apply_tactic tac in
 205   let tbar = gui#toolbar in
 206   ignore (tbar#introsButton#connect#clicked (tac "intros" (Tactics.intros ())));
 207   ignore (tbar#applyButton#connect#clicked (tac_w_term "apply" Tactics.apply));
 208   ignore (tbar#exactButton#connect#clicked (tac_w_term "exact" Tactics.exact));
 209   ignore (tbar#elimButton#connect#clicked (tac_w_term "elim"
 210     Tactics.elim_intros_simpl));
 211   ignore (tbar#elimTypeButton#connect#clicked (tac_w_term "elim type"
 212     Tactics.elim_type));
 213   ignore (tbar#splitButton#connect#clicked (tac "split" Tactics.split));
 214   ignore (tbar#leftButton#connect#clicked (tac "left" Tactics.left));
 215   ignore (tbar#rightButton#connect#clicked (tac "right" Tactics.right));
 216   ignore (tbar#existsButton#connect#clicked (tac "exists" Tactics.exists));
 217   ignore (tbar#reflexivityButton#connect#clicked (tac "reflexivity"
 218     Tactics.reflexivity));
 219   ignore (tbar#symmetryButton#connect#clicked (tac "symmetry"
 220     Tactics.symmetry));
 221   ignore (tbar#transitivityButton#connect#clicked (tac_w_term "transitivity"
 222     Tactics.transitivity));
 223   ignore (tbar#assumptionButton#connect#clicked (tac "assumption"
 224     Tactics.assumption));
 225   ignore (tbar#cutButton#connect#clicked (tac_w_term "cut"
 226     (Tactics.cut ?mk_fresh_name_callback:None)));
 227   ignore (tbar#autoButton#connect#clicked (tac "auto" (Tactics.auto ~dbd)))
 228
 229   (** <DEBUGGING> *)
 230
 231 let save_dom =
 232   let domImpl = lazy (Gdome.domImplementation ()) in
 233   fun ~doc ~dest ->
 234     ignore
 235       ((Lazy.force domImpl)#saveDocumentToFile ~doc ~name:dest ~indent:true ())
 236
 237 let _ =
 238   if BuildTimeConf.debug then begin
 239     gui#main#debugMenu#misc#show ();
 240     let addDebugItem ~label callback =
 241       let item =
 242         GMenu.menu_item ~packing:gui#main#debugMenu_menu#append ~label ()
 243       in
 244       ignore (item#connect#activate callback)
 245     in
 246     addDebugItem "interactive user uri choice" (fun _ ->
 247       try
 248         let uris =
 249           interactive_user_uri_choice ~gui ~selection_mode:`MULTIPLE
 250             ~msg:"messaggio" ~nonvars_button:true
 251             ["cic:/uno.con"; "cic:/due.var"; "cic:/tre.con"; "cic:/quattro.con";
 252             "cic:/cinque.var"]
 253         in
 254         List.iter prerr_endline uris
 255       with MatitaGtkMisc.Cancel -> MatitaTypes.error "no choice");
 256     addDebugItem "toggle auto disambiguation" (fun _ ->
 257       Helm_registry.set_bool "matita.auto_disambiguation"
 258         (not (Helm_registry.get_bool "matita.auto_disambiguation")));
 259     addDebugItem "mono line text input" (fun _ ->
 260       prerr_endline (ask_text ~gui ~title:"title" ~msg:"message" ()));
 261     addDebugItem "multi line text input" (fun _ ->
 262       prerr_endline
 263         (ask_text ~gui ~title:"title" ~multiline:true ~msg:"message" ()));
 264     addDebugItem "dump proof status to stdout" (fun _ ->
 265       print_endline ((get_proof ())#toString));
 266   end
 267
 268   (** </DEBUGGING> *)
 269
 270 let _ =
 271   (try
 272     load_script Sys.argv.(1)
 273   with Invalid_argument _ -> ());
 274   GtkThread.main ()
 275