(* *)
(******************************************************************************)
+open Printf;;
+
+(* DEBUGGING *)
+
+let debug_print =
+ let debug = true in
+ fun s -> prerr_endline (sprintf "DEBUG: %s" s)
+;;
(* GLOBAL CONSTANTS *)
let expr =
let term =
term_of_cic_textual_parser_uri
- (Misc.cic_textual_parser_uri_of_string uri)
+ (MQueryMisc.cic_textual_parser_uri_of_string uri)
in
(Cic.Cast (term, CicTypeChecker.type_of_aux' [] [] term))
in
end));
window#set_position `CENTER ;
window#show () ;
- GMain.Main.main () ;
+ GtkThread.main ();
if !chosen then
if !use_only_constants then
List.filter
(function () -> chosen := Some notebook#current_page ; window#destroy ())) ;
window#set_position `CENTER ;
window#show () ;
- GMain.Main.main () ;
+ GtkThread.main ();
match !chosen with
None -> raise NoChoice
| Some n -> n
| _ -> raise OpenConjecturesStillThere
;;
-let save () =
+ (** save an unfinished proof on the filesystem *)
+let save_unfinished_proof () =
let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
- match !ProofEngine.proof with
- None -> assert false
- | Some (uri, metasenv, bo, ty) ->
- let currentproof =
- (*CSC: Wrong: [] is just plainly wrong *)
- Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[])
- in
- let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
- Cic2acic.acic_object_of_cic_object currentproof
- in
- let xml, bodyxml =
- match
- Cic2Xml.print_object uri ~ids_to_inner_sorts
- ~ask_dtd_to_the_getter:true acurrentproof
- with
- xml,Some bodyxml -> xml,bodyxml
- | _,None -> assert false
- in
- Xml.pp ~quiet:true xml (Some prooffiletype) ;
- output_html outputhtml
- ("<h1 color=\"Green\">Current proof type saved to " ^
- prooffiletype ^ "</h1>") ;
- Xml.pp ~quiet:true bodyxml (Some prooffile) ;
- output_html outputhtml
- ("<h1 color=\"Green\">Current proof body saved to " ^
- prooffile ^ "</h1>")
+ let (xml, bodyxml) = ProofEngine.get_current_status_as_xml () in
+ Xml.pp ~quiet:true xml (Some prooffiletype) ;
+ output_html outputhtml
+ ("<h1 color=\"Green\">Current proof type saved to " ^
+ prooffiletype ^ "</h1>") ;
+ Xml.pp ~quiet:true bodyxml (Some prooffile) ;
+ output_html outputhtml
+ ("<h1 color=\"Green\">Current proof body saved to " ^
+ prooffile ^ "</h1>")
;;
(* Used to typecheck the loaded proofs *)
let module U = UriManager in
List.map
(function uri ->
- match Misc.cic_textual_parser_uri_of_string uri with
+ match MQueryMisc.cic_textual_parser_uri_of_string uri with
CicTextualParser0.IndTyUri (uri,typeno) -> (uri,typeno,[])
| _ -> assert false)
(interactive_user_uri_choice
raise (InvokeTactics.RefreshSequentException e)
with Not_found -> prerr_endline ("Offending sequent " ^ string_of_int metano ^ " unknown."); raise (InvokeTactics.RefreshSequentException e)
-
+let __notify_hbugs = ref None;;
module InvokeTacticsCallbacks =
struct
let sequent_viewer () = (rendering_window ())#notebook#proofw
let decompose_uris_choice_callback = decompose_uris_choice_callback
let mk_fresh_name_callback = mk_fresh_name_callback
let output_html msg = output_html (outputhtml ()) msg
+ let notify_hbugs () =
+ match !__notify_hbugs with
+ | Some f -> f ()
+ | None -> assert false
end
;;
+module InvokeTactics' = InvokeTactics.Make (InvokeTacticsCallbacks);;
+module Hbugs' = Hbugs.Make (InvokeTactics');;
+__notify_hbugs := Some Hbugs'.notify;;
-module InvokeTactics' = InvokeTactics.Make(InvokeTacticsCallbacks);;
-
-
-let load () =
+ (** load an unfinished proof from filesystem *)
+let load_unfinished_proof () =
let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
let notebook = (rendering_window ())#notebook in
output_html outputhtml
("<h1 color=\"Green\">Current proof body loaded from " ^
prooffile ^ "</h1>") ;
- !save_set_sensitive true
+ !save_set_sensitive true;
+ Hbugs'.notify ()
| _ -> assert false
with
InvokeTactics.RefreshSequentException e ->
(string_of_cic_textual_parser_uri uri)
) dom))) ;
window#show () ;
- GMain.Main.main () ;
+ GtkThread.main ();
if !chosen then
let dom,resolve_id =
let inputtext = input#get_chars 0 input#length in
let n' = Str.search_forward regexpr inputtext n in
let id = Str.matched_group 2 inputtext in
let uri =
- Misc.cic_textual_parser_uri_of_string
+ MQueryMisc.cic_textual_parser_uri_of_string
("cic:" ^ (Str.matched_group 5 inputtext))
in
let dom,resolve_id = aux (n' + 1) in
let scrolled_window =
GBin.scrolled_window ~border_width:10 ~packing:window#add () in
let mmlwidget =
- GMathViewAux.single_selection_math_view ~packing:scrolled_window#add ~width:600 ~height:400 () in
+ GMathViewAux.single_selection_math_view
+ ~packing:scrolled_window#add ~width:600 ~height:400 ()
+ in
let _ = window#event#connect#delete (fun _ -> window#misc#hide () ; true ) in
let href = Gdome.domString "href" in
let show_in_show_window_obj uri obj =
let uris =
List.map
(function uri,_ ->
- Misc.wrong_xpointer_format_from_wrong_xpointer_format' uri)
+ MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri)
result in
let html =
(" <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>")
locate_input#delete_text 0 (String.length id)
)) ;
window#show () ;
- GMain.Main.main () ;
+ GtkThread.main ();
match !uri with
None -> raise NoChoice
| Some uri -> UriManager.uri_of_string ("cic:" ^ uri)
end
;;
+module Disambiguate' = Disambiguate.Make(Callbacks);;
+
module TermEditor' = TermEditor.Make(Callbacks);;
(* OTHER FUNCTIONS *)
("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
)) ;
window2#show () ;
- GMain.Main.main () ;
+ GtkThread.main ();
let okb_pressed = !chosen in
chosen := false ;
if (not okb_pressed) then
phase1 () ;
(* No more phases left or Abort pressed *)
window#show () ;
- GMain.Main.main () ;
+ GtkThread.main ();
window#destroy () ;
if !chosen then
try
("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
)) ;
window#show () ;
- GMain.Main.main () ;
+ GtkThread.main ();
if !chosen then
try
let metasenv,expr = !get_metasenv_and_term () in
!save_set_sensitive true ;
inputt#reset ;
ProofEngine.intros ~mk_fresh_name_callback () ;
+ Hbugs'.notify ();
refresh_goals notebook ;
refresh_proof output
with
(fun ~row ~column ~event ->
let (uristr,_) = List.nth results row in
match
- Misc.cic_textual_parser_uri_of_string
- (Misc.wrong_xpointer_format_from_wrong_xpointer_format'
+ MQueryMisc.cic_textual_parser_uri_of_string
+ (MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format'
uristr)
with
CicTextualParser0.ConUri uri
(okb#connect#clicked (function () -> chosen := true ; window#destroy ()));
window#set_position `CENTER ;
window#show () ;
- GMain.Main.main () ;
+ GtkThread.main ();
if !chosen then
let chosen_must_rel =
List.map
ignore (input#insert_text text ~pos:0))) ;
window#set_position `CENTER ;
window#show () ;
- GMain.Main.main () ;
+ GtkThread.main ();
match !chosen with
None -> ()
| Some q ->
(function () -> chosen := Some notebook#current_page ; window#destroy ())) ;
window#set_position `CENTER ;
window#show () ;
- GMain.Main.main () ;
+ GtkThread.main ();
match !chosen with
None -> raise NoChoice
| Some n ->
let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
try
- let metasenv =
+ let proof =
match !ProofEngine.proof with
None -> assert false
- | Some (_,metasenv,_,_) -> metasenv
+ | Some proof -> proof
in
match !ProofEngine.goal with
- None -> ()
+ | None -> ()
| Some metano ->
- let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in
- let list_of_must,only = MQueryLevels.out_restr metasenv ey ty in
- let must = choose_must list_of_must only in
- let torigth_restriction (u,b) =
- let p =
- if b then
- "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion"
- else
- "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion"
- in
- (u,p,None)
- in
- let rigth_must = List.map torigth_restriction must in
- let rigth_only = Some (List.map torigth_restriction only) in
- let result =
- MQueryGenerator.searchPattern
- (rigth_must,[],[]) (rigth_only,None,None) in
- let uris =
- List.map
- (function uri,_ ->
- Misc.wrong_xpointer_format_from_wrong_xpointer_format' uri
- ) result in
- let html =
- " <h1>Backward Query: </h1>" ^
- " <pre>" ^ get_last_query result ^ "</pre>"
- in
- output_html outputhtml html ;
- let uris',exc =
- let rec filter_out =
- function
- [] -> [],""
- | uri::tl ->
- let tl',exc = filter_out tl in
- try
- if
- ProofEngine.can_apply
- (term_of_cic_textual_parser_uri
- (Misc.cic_textual_parser_uri_of_string uri))
- then
- uri::tl',exc
- else
- tl',exc
- with
- e ->
- let exc' =
- "<h1 color=\"red\"> ^ Exception raised trying to apply " ^
- uri ^ ": " ^ Printexc.to_string e ^ " </h1>" ^ exc
- in
- tl',exc'
- in
- filter_out uris
- in
- let html' =
- " <h1>Objects that can actually be applied: </h1> " ^
- String.concat "<br>" uris' ^ exc ^
- " <h1>Number of false matches: " ^
- string_of_int (List.length uris - List.length uris') ^ "</h1>" ^
- " <h1>Number of good matches: " ^
- string_of_int (List.length uris') ^ "</h1>"
- in
- output_html outputhtml html' ;
- let uri' =
- user_uri_choice ~title:"Ambiguous input."
- ~msg:
- "Many lemmas can be successfully applied. Please, choose one:"
- uris'
- in
- inputt#set_term uri' ;
- InvokeTactics'.apply ()
+ let uris' =
+ TacticChaser.searchPattern
+ ~output_html:(output_html outputhtml) ~choose_must ()
+ ~status:(proof, metano)
+ in
+ let uri' =
+ user_uri_choice ~title:"Ambiguous input."
+ ~msg: "Many lemmas can be successfully applied. Please, choose one:"
+ uris'
+ in
+ inputt#set_term uri' ;
+ InvokeTactics'.apply ()
with
e ->
output_html outputhtml
class scratch_window =
let window =
- GWindow.window ~title:"MathML viewer" ~border_width:2 () in
+ GWindow.window
+ ~title:"MathML viewer"
+ ~border_width:2 () in
let vbox =
GPack.vbox ~packing:window#add () in
let hbox =
class rendering_window output (notebook : notebook) =
let scratch_window = new scratch_window in
let window =
- GWindow.window ~title:"MathML viewer" ~border_width:0
- ~allow_shrink:false () in
+ GWindow.window
+ ~title:"gTopLevel - Helm's Proof Assistant"
+ ~border_width:0 ~allow_shrink:false () in
let vbox_for_menu = GPack.vbox ~packing:window#add () in
(* menus *)
let handle_box = GBin.handle_box ~border_width:2
ignore (factory1#add_separator ()) ;
ignore
(factory1#add_item "Load Unfinished Proof..." ~key:GdkKeysyms._L
- ~callback:load) ;
+ ~callback:load_unfinished_proof) ;
let save_menu_item =
- factory1#add_item "Save Unfinished Proof" ~key:GdkKeysyms._S ~callback:save
+ factory1#add_item "Save Unfinished Proof" ~key:GdkKeysyms._S
+ ~callback:save_unfinished_proof
in
ignore
(save_set_sensitive := function b -> save_menu_item#misc#set_sensitive b);
~callback:(check scratch_window) in
let _ = check_menu_item#misc#set_sensitive false in
(* search menu *)
- let settings_menu = factory0#add_submenu "Search" in
- let factory4 = new GMenu.factory settings_menu ~accel_group in
+ let search_menu = factory0#add_submenu "Search" in
+ let factory4 = new GMenu.factory search_menu ~accel_group in
let _ =
factory4#add_item "Locate..." ~key:GdkKeysyms._T
~callback:locate in
let insert_query_item =
factory4#add_item "Insert Query (Experts Only)..." ~key:GdkKeysyms._U
~callback:insertQuery in
+ (* hbugs menu *)
+ let hbugs_menu = factory0#add_submenu "HBugs" in
+ let factory6 = new GMenu.factory hbugs_menu ~accel_group in
+ let toggle_hbugs_menu_item =
+ factory6#add_check_item
+ ~active:false ~key:GdkKeysyms._F5 ~callback:Hbugs'.toggle "HBugs enabled"
+ in
(* settings menu *)
let settings_menu = factory0#add_submenu "Settings" in
let factory3 = new GMenu.factory settings_menu ~accel_group in
let rendering_window' = new rendering_window output notebook in
set_rendering_window rendering_window' ;
rendering_window'#show () ;
- GMain.Main.main ()
+(* Hbugs'.toggle true; *)
+ GtkThread.main ()
;;
-let _ =
+let main () =
if !usedb then
begin
Mqint.set_database Mqint.postgres_db ;
ignore (GtkMain.Main.init ()) ;
initialize_everything () ;
if !usedb then Mqint.close ();
+ prerr_endline "FOO";
+ Hbugs'.quit ()
;;
+
+try
+ Sys.catch_break true;
+ main ();
+with Sys.Break -> () (* exit nicely, invoking at_exit functions *)
+
projects / helm.git / commitdiff