(* *)
(******************************************************************************)
+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
(* MISC FUNCTIONS *)
(* CSC: IMPERATIVE AND NOT VERY CLEAN, TO GET THE LAST ISSUED QUERY *)
+(* FG : THIS FUNCTION IS BECOMING A REAL NONSENSE *)
let get_last_query =
let query = ref "" in
+ let out s = query := ! query ^ s in
MQueryGenerator.set_confirm_query
- (function q -> query := MQueryUtil.text_of_query q ; true) ;
- function result -> !query ^ " <h1>Result:</h1> " ^ MQueryUtil.text_of_result result "<br>"
+ (function q ->
+ query := ""; MQueryUtil.text_of_query out q ""; true);
+ function result ->
+ out (!query ^ " <h1>Result:</h1> "); MQueryUtil.text_of_result out result "<br>";
+ !query
;;
let
(* CALLBACKS *)
-(*
-ignore(domImpl#saveDocumentToFile ~doc:sequent_doc
- ~name:"/home/galata/miohelm/guruguru1" ~indent:true ()) ;
-*)
-
exception OpenConjecturesStillThere;;
exception WrongProof;;
| _ -> 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 ->
let uri =
match resolve_id v with
None -> assert false
- | Some uri -> uri
+ | Some (CicTextualParser0.Uri uri) -> uri
+ | Some (CicTextualParser0.Term _)
+ | Some CicTextualParser0.Implicit -> assert false
in
- "alias " ^ v ^ " " ^
- (string_of_cic_textual_parser_uri uri)
+ "alias " ^
+ (match v with
+ CicTextualParser0.Id id -> id
+ | CicTextualParser0.Symbol (descr,_) ->
+ (* CSC: To be implemented *)
+ assert false
+ )^ " " ^ (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 rec aux n =
try
let n' = Str.search_forward regexpr inputtext n in
- let id = Str.matched_group 2 inputtext in
+ let id = CicTextualParser0.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
dom,resolve_id
else
id::dom,
- (function id' -> if id = id' then Some uri else resolve_id id')
+ (function id' ->
+ if id = id' then
+ Some (CicTextualParser0.Uri uri)
+ else resolve_id id')
with
Not_found -> TermEditor.empty_id_to_uris
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 obj = CicEnvironment.get_obj uri in
show_in_show_window_obj uri obj
in
- let show_in_show_window_callback mmlwidget (n : Gdome.element) _ =
- if n#hasAttributeNS ~namespaceURI:xlinkns ~localName:href then
- let uri =
- (n#getAttributeNS ~namespaceURI:xlinkns ~localName:href)#to_string
- in
- show_in_show_window_uri (UriManager.uri_of_string uri)
- else
- ignore (mmlwidget#action_toggle n)
+ let show_in_show_window_callback mmlwidget (n : Gdome.element option) _ =
+ match n with
+ None -> ()
+ | Some n' ->
+ if n'#hasAttributeNS ~namespaceURI:xlinkns ~localName:href then
+ let uri =
+ (n'#getAttributeNS ~namespaceURI:xlinkns ~localName:href)#to_string
+ in
+ show_in_show_window_uri (UriManager.uri_of_string uri)
+ else
+ ignore (mmlwidget#action_toggle n')
in
let _ =
mmlwidget#connect#click (show_in_show_window_callback mmlwidget)
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)
(* A WIDGET TO ENTER CIC TERMS *)
+module ChosenTermEditor = TexTermEditor;;
+module ChosenTextualParser0 = TexCicTextualParser0;;
+(*
+module ChosenTermEditor = TermEditor;;
+module ChosenTextualParser0 = CicTextualParser0;;
+*)
+
module Callbacks =
struct
+ let get_metasenv () = !ChosenTextualParser0.metasenv
+ let set_metasenv metasenv = ChosenTextualParser0.metasenv := metasenv
+
let output_html msg = output_html (outputhtml ()) msg;;
let interactive_user_uri_choice =
fun ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id ->
end
;;
-module TermEditor' = TermEditor.Make(Callbacks);;
+module TexTermEditor' = ChosenTermEditor.Make(Callbacks);;
(* OTHER FUNCTIONS *)
GBin.scrolled_window ~border_width:5
~packing:(vbox#pack ~expand:true ~padding:0) () in
let newinputt =
- TermEditor'.term_editor
+ TexTermEditor'.term_editor
~width:400 ~height:20 ~packing:scrolled_window#add
~share_id_to_uris_with:inputt ()
~isnotempty_callback:
GBin.scrolled_window ~border_width:5
~packing:(vbox#pack ~expand:true ~padding:0) () in
let newinputt =
- TermEditor'.term_editor
+ TexTermEditor'.term_editor
~width:400 ~height:20 ~packing:scrolled_window#add
~share_id_to_uris_with:inputt ()
~isnotempty_callback:
("<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
~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
(* moved here to have visibility of the ok button *)
let newinputt =
- TermEditor'.term_editor ~width:400 ~height:100 ~packing:scrolled_window#add
+ TexTermEditor'.term_editor ~width:400 ~height:100 ~packing:scrolled_window#add
~share_id_to_uris_with:inputt ()
~isnotempty_callback:
(function b ->
("<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 =
let replaceb =
GButton.button ~label:"Replace"
~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
+ let injectionb =
+ GButton.button ~label:"Injection"
+ ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
+ let discriminateb =
+ GButton.button ~label:"Discriminate"
+ ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
(* Zack: spostare in una toolbar
let generalizeb =
GButton.button ~label:"Generalize"
ignore(introsb#connect#clicked InvokeTactics'.intros) ;
ignore(decomposeb#connect#clicked InvokeTactics'.decompose) ;
ignore(searchpatternb#connect#clicked searchPattern) ;
+ ignore(injectionb#connect#clicked InvokeTactics'.injection) ;
+ ignore(discriminateb#connect#clicked InvokeTactics'.discriminate) ;
(* Zack: spostare in una toolbar
ignore(whdb#connect#clicked whd) ;
ignore(reduceb#connect#clicked reduce) ;
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
factory4#add_item "Show..." ~key:GdkKeysyms._H ~callback:show
in
let insert_query_item =
- factory4#add_item "Insert Query (Experts Only)..." ~key:GdkKeysyms._U
+ factory4#add_item "Insert Query (Experts Only)..." ~key:GdkKeysyms._Y
~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
GBin.scrolled_window ~border_width:5
~packing:frame#add () in
let inputt =
- TermEditor'.term_editor
+ TexTermEditor'.term_editor
~width:400 ~height:100 ~packing:scrolled_window1#add ()
~isnotempty_callback:
(function b ->
let notebook = new notebook in
let rendering_window' = new rendering_window output notebook in
set_rendering_window rendering_window' ;
- rendering_window'#show () ;
- GMain.Main.main ()
+ let print_error_as_html prefix msg =
+ output_html (outputhtml ())
+ ("<h1 color=\"red\">" ^ prefix ^ msg ^ "</h1>")
+ in
+ Gdome_xslt.setErrorCallback (Some (print_error_as_html "XSLT Error: "));
+ Gdome_xslt.setDebugCallback
+ (Some (print_error_as_html "XSLT Debug Message: "));
+ rendering_window'#show () ;
+(* 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 / blobdiff