From: Stefano Zacchiroli Date: Thu, 20 Feb 2003 17:27:11 +0000 (+0000) Subject: - added HBugs support X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=c205359e224034e2024947fc4cd1801d37b7c824 - added HBugs support - switched to multi threaded implementation - fixed references from Misc to MQueryMisc module - moved search pattern apply in ../ocaml/tactics/tacticChaser.ml* --- diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index bdf78b28f..82cabae04 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -33,6 +33,14 @@ (* *) (******************************************************************************) +open Printf;; + +(* DEBUGGING *) + +let debug_print = + let debug = true in + fun s -> prerr_endline (sprintf "DEBUG: %s" s) +;; (* GLOBAL CONSTANTS *) @@ -194,7 +202,7 @@ let check_window outputhtml uris = 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 @@ -312,7 +320,7 @@ let end)); window#set_position `CENTER ; window#show () ; - GMain.Main.main () ; + GtkThread.main (); if !chosen then if !use_only_constants then List.filter @@ -373,7 +381,7 @@ let interactive_interpretation_choice interpretations = (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 @@ -504,34 +512,18 @@ let qed () = | _ -> 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 - ("

Current proof type saved to " ^ - prooffiletype ^ "

") ; - Xml.pp ~quiet:true bodyxml (Some prooffile) ; - output_html outputhtml - ("

Current proof body saved to " ^ - prooffile ^ "

") + let (xml, bodyxml) = ProofEngine.get_current_status_as_xml () in + Xml.pp ~quiet:true xml (Some prooffiletype) ; + output_html outputhtml + ("

Current proof type saved to " ^ + prooffiletype ^ "

") ; + Xml.pp ~quiet:true bodyxml (Some prooffile) ; + output_html outputhtml + ("

Current proof body saved to " ^ + prooffile ^ "

") ;; (* Used to typecheck the loaded proofs *) @@ -552,7 +544,7 @@ let decompose_uris_choice_callback uris = 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 @@ -660,7 +652,7 @@ let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in 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 @@ -678,13 +670,18 @@ module InvokeTacticsCallbacks = 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 @@ -714,7 +711,8 @@ let load () = output_html outputhtml ("

Current proof body loaded from " ^ prooffile ^ "

") ; - !save_set_sensitive true + !save_set_sensitive true; + Hbugs'.notify () | _ -> assert false with InvokeTactics.RefreshSequentException e -> @@ -772,7 +770,7 @@ let edit_aliases () = (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 @@ -791,7 +789,7 @@ let edit_aliases () = 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 @@ -888,7 +886,9 @@ let 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 = @@ -955,7 +955,7 @@ let locate_callback id = 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 = ("

Locate Query: 

" ^ get_last_query result ^ "
") @@ -1067,7 +1067,7 @@ let input_or_locate_uri ~title = 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) @@ -1089,6 +1089,8 @@ module Callbacks = end ;; +module Disambiguate' = Disambiguate.Make(Callbacks);; + module TermEditor' = TermEditor.Make(Callbacks);; (* OTHER FUNCTIONS *) @@ -1398,7 +1400,7 @@ let new_inductive () = ("

" ^ Printexc.to_string e ^ "

") ; )) ; window2#show () ; - GMain.Main.main () ; + GtkThread.main (); let okb_pressed = !chosen in chosen := false ; if (not okb_pressed) then @@ -1412,7 +1414,7 @@ let new_inductive () = phase1 () ; (* No more phases left or Abort pressed *) window#show () ; - GMain.Main.main () ; + GtkThread.main (); window#destroy () ; if !chosen then try @@ -1534,7 +1536,7 @@ let new_proof () = ("

" ^ Printexc.to_string e ^ "

") ; )) ; window#show () ; - GMain.Main.main () ; + GtkThread.main (); if !chosen then try let metasenv,expr = !get_metasenv_and_term () in @@ -1547,6 +1549,7 @@ let new_proof () = !save_set_sensitive true ; inputt#reset ; ProofEngine.intros ~mk_fresh_name_callback () ; + Hbugs'.notify (); refresh_goals notebook ; refresh_proof output with @@ -1680,8 +1683,8 @@ let show_query_results results = (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 @@ -1872,7 +1875,7 @@ let refine_constraints (must_obj,must_rel,must_sort) = (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 @@ -1967,7 +1970,7 @@ let insertQuery () = ignore (input#insert_text text ~pos:0))) ; window#set_position `CENTER ; window#show () ; - GMain.Main.main () ; + GtkThread.main (); match !chosen with None -> () | Some q -> @@ -2095,7 +2098,7 @@ let choose_must list_of_must only = (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 -> @@ -2110,83 +2113,26 @@ let searchPattern () = 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 = - "

Backward Query:

" ^ - " 
" ^ get_last_query result ^ "
" - 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' = - "

^ Exception raised trying to apply " ^ - uri ^ ": " ^ Printexc.to_string e ^ "

" ^ exc - in - tl',exc' - in - filter_out uris - in - let html' = - "

Objects that can actually be applied:

" ^ - String.concat "
" uris' ^ exc ^ - "

Number of false matches: " ^ - string_of_int (List.length uris - List.length uris') ^ "

" ^ - "

Number of good matches: " ^ - string_of_int (List.length uris') ^ "

" - 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 @@ -2342,7 +2288,9 @@ end;; 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 = @@ -2686,8 +2634,9 @@ end 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 @@ -2717,9 +2666,10 @@ class rendering_window output (notebook : notebook) = 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); @@ -2762,8 +2712,8 @@ class rendering_window output (notebook : notebook) = ~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 @@ -2777,6 +2727,13 @@ class rendering_window output (notebook : notebook) = 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 @@ -2863,10 +2820,11 @@ let initialize_everything () = 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 ; @@ -2875,4 +2833,12 @@ let _ = 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 *) +