X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=d3e39351c04804cf06a3c0fe8cfdbd21668fd6b7;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=7c01b4d75879b95771bbeea27b51278cdf0ad07d;hpb=2329c7fd13fb6c88f9f82ccad6b25a67c9ce7acf;p=helm.git diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 7c01b4d75..d3e39351c 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -1,4 +1,4 @@ -(* Copyright (C) 2000, HELM Team. +(* Copyright (C) 2000-2004, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -20,283 +20,2088 @@ * MA 02111-1307, USA. * * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. + * http://helm.cs.unibo.it/ *) -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 06/01/2002 *) -(* *) -(* *) -(******************************************************************************) +(*****************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 06/01/2002 *) +(* *) +(* *) +(*****************************************************************************) + +let debug_level = ref 1 +let debug_print ?(level = 1) s = if !debug_level >= level then prerr_endline s +let error s = prerr_endline ("E: " ^ s) +let warning s = prerr_endline ("W: " ^ s) + +open Printf + +module MQI = MQueryInterpreter +module MQIC = MQIConn +module MQGT = MQGTypes +module MQGU = MQGUtil +module MQG = MQueryGenerator + +(* first of all let's initialize the Helm_registry *) +let _ = + let configuration_file = "gTopLevel.conf.xml" in + if not (Sys.file_exists configuration_file) then begin + eprintf "E: Can't find configuration file '%s'\n" configuration_file; + exit 2 + end; + Helm_registry.load_from configuration_file +;; (* GLOBAL CONSTANTS *) -let helmns = Gdome.domString "http://www.cs.unibo.it/helm";; +let mqi_handle = MQIC.init_if_connected () + +let dbd = + Mysql.quick_connect + ~host:(Helm_registry.get "db.host") + ~user:(Helm_registry.get "db.user") + ~database:(Helm_registry.get "db.database") + () + +let restore_environment_on_boot = true ;; +let notify_hbugs_on_goal_change = false ;; + +let auto_disambiguation = ref true ;; + +(* GLOBAL REFERENCES (USED BY CALLBACKS) *) -let htmlheader = - "" ^ - " " +let check_term = ref (fun _ _ _ -> assert false);; + +exception RenderingWindowsNotInitialized;; + +let set_rendering_window,rendering_window = + let rendering_window_ref = ref None in + (function rw -> rendering_window_ref := Some rw), + (function () -> + match !rendering_window_ref with + None -> raise RenderingWindowsNotInitialized + | Some rw -> rw + ) ;; -let htmlfooter = - " " ^ - "" +exception SettingsWindowsNotInitialized;; + +let set_settings_window,settings_window = + let settings_window_ref = ref None in + (function rw -> settings_window_ref := Some rw), + (function () -> + match !settings_window_ref with + None -> raise SettingsWindowsNotInitialized + | Some rw -> rw + ) ;; -(* GLOBAL REFERENCES (USED BY CALLBACKS) *) +exception QedSetSensitiveNotInitialized;; +let qed_set_sensitive = + ref (function _ -> raise QedSetSensitiveNotInitialized) +;; -let htmlheader_and_content = ref htmlheader;; +exception SaveSetSensitiveNotInitialized;; +let save_set_sensitive = + ref (function _ -> raise SaveSetSensitiveNotInitialized) +;; + +(* COMMAND LINE OPTIONS *) + +let usedb = ref true -let filename4uwobo = "/public/sacerdot/prova.xml";; +let argspec = + [ + "-nodb", Arg.Clear usedb, "disable use of MathQL DB" + ] +in +Arg.parse argspec ignore "" -let current_cic_infos = ref None;; +(* UTILITY FUNCTIONS TO DISAMBIGUATE AN URI *) + +(* Check window *) + +let check_window uris = + let window = + GWindow.window + ~width:800 ~modal:true ~title:"Check" ~border_width:2 () in + let notebook = + GPack.notebook ~scrollable:true ~packing:window#add () in + window#show () ; + let render_terms = + List.map + (function uri -> + let scrolled_window = + GBin.scrolled_window ~border_width:10 + ~packing: + (notebook#append_page ~tab_label:((GMisc.label ~text:uri ())#coerce)) + () + in + lazy + (let mmlwidget = + TermViewer.sequent_viewer + ~mml_of_cic_sequent:ApplyTransformation.mml_of_cic_sequent + ~packing:scrolled_window#add ~width:400 ~height:280 () in + let expr = + let term = CicUtil.term_of_uri uri in + (Cic.Cast (term, fst(CicTypeChecker.type_of_aux' [] [] term + CicUniv.empty_ugraph ))) + in + try + mmlwidget#load_sequent [] (111,[],expr) + with + e -> + HelmLogger.log (`Error (`T (Printexc.to_string e))) + ) + ) uris + in + ignore + (notebook#connect#switch_page + (function i -> + Lazy.force (List.nth render_terms i))) +;; + +exception NoChoice;; + +let interactive_user_uri_choice + ~(selection_mode:[ `SINGLE | `MULTIPLE ]) + ?(ok="Ok") ?(enable_button_for_non_vars=false) ~title ~msg uris += + let only_constant_choices = + lazy + (List.filter + (fun uri -> not (String.sub uri (String.length uri - 4) 4 = ".var")) + uris) + in + if selection_mode <> `SINGLE && !auto_disambiguation then + Lazy.force only_constant_choices + else begin + let choices = ref [] in + let chosen = ref false in + let use_only_constants = ref false in + let window = + GWindow.dialog ~modal:true ~title ~width:600 () in + let lMessage = + GMisc.label ~text:msg + ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in + let scrolled_window = + GBin.scrolled_window ~border_width:10 + ~packing:(window#vbox#pack ~expand:true ~fill:true ~padding:5) () in + let clist = + let expected_height = 18 * List.length uris in + let height = if expected_height > 400 then 400 else expected_height in + GList.clist ~columns:1 ~packing:scrolled_window#add + ~height ~selection_mode:(selection_mode :> Gtk.Tags.selection_mode) () in + let _ = List.map (function x -> clist#append [x]) uris in + let hbox2 = + GPack.hbox ~border_width:0 + ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in + let explain_label = + GMisc.label ~text:"None of the above. Try this one:" + ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in + let manual_input = + GEdit.entry ~editable:true + ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in + let hbox = + GPack.hbox ~border_width:0 ~packing:window#action_area#add () in + let okb = + GButton.button ~label:ok + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let _ = okb#misc#set_sensitive false in + let nonvarsb = + GButton.button + ~packing: + (function w -> + if enable_button_for_non_vars then + hbox#pack ~expand:false ~fill:false ~padding:5 w) + ~label:"Try constants only" () in + let autob = + GButton.button + ~packing: + (fun w -> + if enable_button_for_non_vars then + hbox#pack ~expand:false ~fill:false ~padding:5 w) + ~label:"Auto" () in + let checkb = + GButton.button ~label:"Check" + ~packing:(hbox#pack ~padding:5) () in + let _ = checkb#misc#set_sensitive false in + let cancelb = + GButton.button ~label:"Abort" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + (* actions *) + let check_callback () = + assert (List.length !choices > 0) ; + check_window !choices + in + ignore (window#connect#destroy GMain.Main.quit) ; + ignore (cancelb#connect#clicked window#destroy) ; + ignore + (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ; + ignore + (nonvarsb#connect#clicked + (function () -> + use_only_constants := true ; + chosen := true ; + window#destroy () + )) ; + ignore (autob#connect#clicked (fun () -> + auto_disambiguation := true; + (rendering_window ())#set_auto_disambiguation true; + use_only_constants := true ; + chosen := true; + window#destroy ())); + ignore (checkb#connect#clicked check_callback) ; + ignore + (clist#connect#select_row + (fun ~row ~column ~event -> + checkb#misc#set_sensitive true ; + okb#misc#set_sensitive true ; + choices := (List.nth uris row)::!choices)) ; + ignore + (clist#connect#unselect_row + (fun ~row ~column ~event -> + choices := + List.filter (function uri -> uri != (List.nth uris row)) !choices)) ; + ignore + (manual_input#connect#changed + (fun _ -> + if manual_input#text = "" then + begin + choices := [] ; + checkb#misc#set_sensitive false ; + okb#misc#set_sensitive false ; + clist#misc#set_sensitive true + end + else + begin + choices := [manual_input#text] ; + clist#unselect_all () ; + checkb#misc#set_sensitive true ; + okb#misc#set_sensitive true ; + clist#misc#set_sensitive false + end)); + window#set_position `CENTER ; + window#show () ; + GtkThread.main (); + if !chosen then + if !use_only_constants then + Lazy.force only_constant_choices + else + if List.length !choices > 0 then !choices else raise NoChoice + else + raise NoChoice + end +;; + +let interactive_interpretation_choice interpretations = + let chosen = ref None in + let window = + GWindow.window + ~modal:true ~title:"Ambiguous well-typed input." ~border_width:2 () in + let vbox = GPack.vbox ~packing:window#add () in + let lMessage = + GMisc.label + ~text: + ("Ambiguous input since there are many well-typed interpretations." ^ + " Please, choose one of them.") + ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let notebook = + GPack.notebook ~scrollable:true + ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in + let _ = + List.map + (function interpretation -> + let clist = + let expected_height = 18 * List.length interpretation in + let height = if expected_height > 400 then 400 else expected_height in + GList.clist ~columns:2 ~packing:notebook#append_page ~height + ~titles:["id" ; "URI"] () + in + ignore + (List.map + (function (id,uri) -> + let n = clist#append [id;uri] in + clist#set_row ~selectable:false n + ) interpretation + ) ; + clist#columns_autosize () + ) interpretations in + let hbox = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let okb = + GButton.button ~label:"Ok" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let cancelb = + GButton.button ~label:"Abort" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + (* actions *) + ignore (window#connect#destroy GMain.Main.quit) ; + ignore (cancelb#connect#clicked window#destroy) ; + ignore + (okb#connect#clicked + (function () -> chosen := Some notebook#current_page ; window#destroy ())) ; + window#set_position `CENTER ; + window#show () ; + GtkThread.main (); + match !chosen with + None -> raise NoChoice + | Some n -> [n] +;; (* MISC FUNCTIONS *) -let domImpl = Gdome.domImplementation ();; +let + save_object_to_disk uri annobj ids_to_inner_sorts ids_to_inner_types pathname += + let name = + let struri = UriManager.string_of_uri uri in + let idx = (String.rindex struri '/') + 1 in + String.sub struri idx (String.length struri - idx) + in + let path = pathname ^ "/" ^ name in + let xml, bodyxml = + Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:false + annobj + in + let xmlinnertypes = + Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types + ~ask_dtd_to_the_getter:false + in + (* innertypes *) + let innertypesuri = UriManager.innertypesuri_of_uri uri in + Xml.pp ~gzip:false xmlinnertypes (Some (path ^ ".types.xml")) ; + Http_getter.register' innertypesuri + (Helm_registry.get "local_library.url" ^ + Str.replace_first (Str.regexp "^cic:") "" + (UriManager.string_of_uri innertypesuri) ^ ".xml" + ) ; + (* constant type / variable / mutual inductive types definition *) + Xml.pp ~gzip:false xml (Some (path ^ ".xml")) ; + Http_getter.register' uri + (Helm_registry.get "local_library.url" ^ + Str.replace_first (Str.regexp "^cic:") "" + (UriManager.string_of_uri uri) ^ ".xml" + ) ; + match bodyxml with + None -> () + | Some bodyxml' -> + (* constant body *) + let bodyuri = + match UriManager.bodyuri_of_uri uri with + None -> assert false + | Some bodyuri -> bodyuri + in + Xml.pp ~gzip:false bodyxml' (Some (path ^ ".body.xml")) ; + Http_getter.register' bodyuri + (Helm_registry.get "local_library.url" ^ + Str.replace_first (Str.regexp "^cic:") "" + (UriManager.string_of_uri bodyuri) ^ ".xml" + ) +;; + -let parseStyle name = - let style = - domImpl#createDocumentFromURI -(* - ~uri:("http://phd.cs.unibo.it:8081/getxslt?uri=" ^ name) ?mode:None -*) - ~uri:("styles/" ^ name) () +(* CALLBACKS *) + +exception OpenConjecturesStillThere;; +exception WrongProof;; + +let pathname_of_annuri uristring = + Helm_registry.get "local_library.dir" ^ + Str.replace_first (Str.regexp "^cic:") "" uristring +;; + +let make_dirs dirpath = + ignore (Unix.system ("mkdir -p " ^ dirpath)) +;; + +let save_obj uri obj = + let + (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts, + ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses) + = + Cic2acic.acic_object_of_cic_object ~eta_fix:false obj in - Gdome_xslt.processStylesheet style + (* let's save the theorem and register it to the getter *) + let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in + make_dirs pathname ; + save_object_to_disk uri acic ids_to_inner_sorts ids_to_inner_types + pathname +;; + +let qed () = + match ProofEngine.get_proof () with + None -> assert false + | Some (uri,[],bo,ty) -> + let uri = match uri with Some uri -> uri | _ -> assert false in + (* we want to typecheck in the ENV *) + prerr_endline "-------------> QED"; + let ty_bo,u = + CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in + let b,u1 = CicReduction.are_convertible [] ty_bo ty u in + if b then + begin + (*CSC: Wrong: [] is just plainly wrong *) + let proof = + Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[],[]) + in + let (acic,ids_to_inner_types,ids_to_inner_sorts) = + (rendering_window ())#output#load_proof proof + in + !qed_set_sensitive false ; + (* let's save the theorem and register it to the getter *) + let pathname = + pathname_of_annuri (UriManager.buri_of_uri uri) + in + let list_of_universes = + CicUnivUtils.universes_of_obj uri + (Cic.Constant ("",None,ty,[],[])) + in + let u1_clean = CicUniv.clean_ugraph u1 list_of_universes in + let u2 = CicUniv.fill_empty_nodes_with_uri u1_clean uri in + (********************************************** + TASSI: to uncomment whe universes will be ON + ***********************************************) + (* + make_dirs pathname ; + save_object_to_disk uri acic ids_to_inner_sorts + ids_to_inner_types pathname; + *) + (* save the universe graph u2 *) + (* add the object to the env *) + CicEnvironment.add_type_checked_term uri (( + Cic.Constant ((UriManager.name_of_uri uri), + (Some bo),ty,[],[])),u2); + (* FIXME: the variable list!! *) + prerr_endline "-------------> FINE"; + end + else + raise WrongProof + | _ -> raise OpenConjecturesStillThere +;; + + (** save an unfinished proof on the filesystem *) +let save_unfinished_proof () = + let (xml, bodyxml) = ProofEngine.get_current_status_as_xml () in + let proof_file_type = Helm_registry.get "gtoplevel.proof_file_type" in + let proof_file = Helm_registry.get "gtoplevel.proof_file" in + Xml.pp ~gzip:false xml (Some proof_file_type) ; + HelmLogger.log + (`Msg (`T ("Current proof type saved to " ^ proof_file_type))) ; + Xml.pp ~gzip:false bodyxml (Some proof_file) ; + HelmLogger.log + (`Msg (`T ("Current proof body saved to " ^ proof_file))) ;; -let d_c = parseStyle "drop_coercions.xsl";; -let tc1 = parseStyle "objtheorycontent.xsl";; -let hc2 = parseStyle "content_to_html.xsl";; -let l = parseStyle "link.xsl";; +(* Used to typecheck the loaded proofs *) +let typecheck_loaded_proof metasenv bo ty = + let module T = CicTypeChecker in + ignore ( + List.fold_left + (fun metasenv ((_,context,ty) as conj) -> + ignore (T.type_of_aux' metasenv context ty CicUniv.empty_ugraph) ; + metasenv @ [conj] + ) [] metasenv) ; + ignore (T.type_of_aux' metasenv [] ty CicUniv.empty_ugraph) ; + ignore (T.type_of_aux' metasenv [] bo CicUniv.empty_ugraph) +;; + +let decompose_uris_choice_callback uris = +(* N.B.: in questo passaggio perdo l'informazione su exp_named_subst !!!! *) + let module U = UriManager in + List.map + (function uri -> + match CicUtil.term_of_uri uri with + | Cic.MutInd (uri, typeno, _) -> (uri, typeno, []) + | _ -> assert false) + (interactive_user_uri_choice + ~selection_mode:`MULTIPLE ~ok:"Ok" ~enable_button_for_non_vars:false + ~title:"Decompose" ~msg:"Please, select the Inductive Types to decompose" + (List.map + (function (uri,typeno,_) -> + U.string_of_uri uri ^ "#1/" ^ string_of_int (typeno+1) + ) uris) + ) +;; -let c1 = parseStyle "rootcontent.xsl";; -let g = parseStyle "genmmlid.xsl";; -let c2 = parseStyle "annotatedpres.xsl";; +let mk_fresh_name_callback metasenv context name ~typ = + let fresh_name = + match FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ with + Cic.Name fresh_name -> fresh_name + | Cic.Anonymous -> assert false + in + match + GToolbox.input_string ~title:"Enter a fresh hypothesis name" ~text:fresh_name + ("Enter a fresh name for the hypothesis " ^ + CicPp.pp typ + (List.map (function None -> None | Some (n,_) -> Some n) context)) + with + Some fresh_name' -> Cic.Name fresh_name' + | None -> raise NoChoice +;; +let refresh_proof (output : TermViewer.proof_viewer) = + try + let uri,currentproof = + match ProofEngine.get_proof () with + None -> assert false + | Some (uri,metasenv,bo,ty) -> + ProofEngine.set_proof (Some (uri,metasenv,bo,ty)) ; + if List.length metasenv = 0 then + begin + !qed_set_sensitive true ; + Hbugs.clear () + end + else + Hbugs.notify () ; + (*CSC: Wrong: [] is just plainly wrong *) + let uri = match uri with Some uri -> uri | _ -> assert false in + (uri, + Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[],[])) + in + ignore (output#load_proof currentproof) + with + e -> + match ProofEngine.get_proof () with + None -> assert false + | Some (uri,metasenv,bo,ty) -> + debug_print ("Offending proof: " ^ + CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[],[]))); + raise (InvokeTactics.RefreshProofException e) + +let set_proof_engine_goal g = + ProofEngine.goal := g +;; + +let refresh_goals ?(empty_notebook=true) notebook = + try + match !ProofEngine.goal with + None -> + if empty_notebook then + begin + notebook#remove_all_pages ~skip_switch_page_event:false ; + notebook#set_empty_page + end + else + notebook#proofw#unload + | Some metano -> + let metasenv = + match ProofEngine.get_proof () with + None -> assert false + | Some (_,metasenv,_,_) -> metasenv + in + let currentsequent = + List.find (function (m,_,_) -> m=metano) metasenv + in + let regenerate_notebook () = + let skip_switch_page_event = + match metasenv with + (m,_,_)::_ when m = metano -> false + | _ -> true + in + notebook#remove_all_pages ~skip_switch_page_event ; + List.iter (function (m,_,_) -> notebook#add_page m) metasenv ; + in + if empty_notebook then + begin + regenerate_notebook () ; + notebook#set_current_page + ~may_skip_switch_page_event:false metano + end + else + begin + notebook#set_current_page + ~may_skip_switch_page_event:true metano ; + notebook#proofw#load_sequent metasenv currentsequent ; + end + with + e -> +let metano = + match !ProofEngine.goal with + None -> assert false + | Some m -> m +in +let metasenv = + match ProofEngine.get_proof () with + None -> assert false + | Some (_,metasenv,_,_) -> metasenv +in +try + let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in + debug_print + ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent currentsequent); + raise (InvokeTactics.RefreshSequentException e) +with Not_found -> + debug_print ("Offending sequent " ^ string_of_int metano ^ " unknown."); + raise (InvokeTactics.RefreshSequentException e) + +module InvokeTacticsCallbacks = + struct + let sequent_viewer () = (rendering_window ())#notebook#proofw + let term_editor () = (rendering_window ())#inputt + let scratch_window () = (rendering_window ())#scratch_window + + let refresh_proof () = + let output = ((rendering_window ())#output : TermViewer.proof_viewer) in + refresh_proof output + + let refresh_goals () = + let notebook = (rendering_window ())#notebook in + refresh_goals notebook + + let decompose_uris_choice_callback = decompose_uris_choice_callback + let mk_fresh_name_callback = mk_fresh_name_callback + let mqi_handle = mqi_handle + let dbd = dbd + end +;; +module InvokeTactics' = InvokeTactics.Make (InvokeTacticsCallbacks);; (* -let processorURL = "http://phd.cs.unibo.it:8080/helm/servelt/uwobo/";; -let getterURL = "http://phd.cs.unibo.it:8081/";; +(* Just to initialize the Hbugs module *) +module Ignore = Hbugs.Initialize (InvokeTactics');; +Hbugs.set_describe_hint_callback (fun hint -> + match hint with + | Hbugs_types.Use_apply_Luke term -> check_window [term] + | _ -> ()) +;; *) -let processorURL = "http://localhost:8080/helm/servelt/uwobo/";; -let getterURL = "http://localhost:8081/";; - -let mml_styles = [d_c ; c1 ; g ; c2 ; l];; -let mml_args = - ["processorURL", "'" ^ processorURL ^ "'" ; - "getterURL", "'" ^ getterURL ^ "'" ; - "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ; - "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ; - "UNICODEvsSYMBOL", "'symbol'" ; - "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ; - "encoding", "'iso-8859-1'" ; - "media-type", "'text/html'" ; - "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ; - "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ; - "naturalLanguage", "'no'" ; - "annotations", "'no'" ; - "topurl", "'http://phd.cs.unibo.it/helm'" ; - "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ] -;; - -let sequent_styles = [d_c ; c1 ; g ; c2 ; l];; -let sequent_args = - ["processorURL", "'" ^ processorURL ^ "'" ; - "getterURL", "'" ^ getterURL ^ "'" ; - "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ; - "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ; - "UNICODEvsSYMBOL", "'symbol'" ; - "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ; - "encoding", "'iso-8859-1'" ; - "media-type", "'text/html'" ; - "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ; - "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ; - "naturalLanguage", "'no'" ; - "annotations", "'no'" ; - "topurl", "'http://phd.cs.unibo.it/helm'" ; - "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ] -;; - -let parse_file filename = - let inch = open_in filename in - let rec read_lines () = - try - let line = input_line inch in - line ^ read_lines () +let dummy_uri = "/dummy.con" + + (** load an unfinished proof from filesystem *) +let load_unfinished_proof () = + let output = ((rendering_window ())#output : TermViewer.proof_viewer) in + let notebook = (rendering_window ())#notebook in + try + match + GToolbox.input_string ~title:"Load Unfinished Proof" ~text:dummy_uri + "Choose an URI:" with - End_of_file -> "" + None -> raise NoChoice + | Some uri0 -> + let uri = UriManager.uri_of_string ("cic:" ^ uri0) in + let proof_file_type = Helm_registry.get "gtoplevel.proof_file_type" in + let proof_file = Helm_registry.get "gtoplevel.proof_file" in + match CicParser.obj_of_xml proof_file_type (Some proof_file) with + Cic.CurrentProof (_,metasenv,bo,ty,_,_) -> + typecheck_loaded_proof metasenv bo ty ; + ProofEngine.set_proof (Some (Some uri, metasenv, bo, ty)); + refresh_proof output ; + set_proof_engine_goal + (match metasenv with + [] -> None + | (metano,_,_)::_ -> Some metano + ) ; + refresh_goals notebook ; + HelmLogger.log + (`Msg (`T ("Current proof type loaded from " ^ proof_file_type))); + HelmLogger.log + (`Msg (`T ("Current proof body loaded from " ^ proof_file))) ; + !save_set_sensitive true; + | _ -> assert false + with + InvokeTactics.RefreshSequentException e -> + HelmLogger.log + (`Error (`T ("Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e))) + | InvokeTactics.RefreshProofException e -> + HelmLogger.log + (`Error (`T ("Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e))) + | e -> + HelmLogger.log + (`Error (`T (Printexc.to_string e))) +;; + +let clear_aliases () = + let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in + inputt#environment := + DisambiguatingParser.EnvironmentP3.of_string + DisambiguatingParser.EnvironmentP3.empty +;; + +let edit_aliases () = + let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in + let disambiguation_env = inputt#environment in + let chosen_aliases = ref None in + let window = + GWindow.window + ~width:400 ~modal:true ~title:"Edit Aliases..." ~border_width:2 () in + let vbox = + GPack.vbox ~border_width:0 ~packing:window#add () in + let scrolled_window = + GBin.scrolled_window ~border_width:10 + ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in + let input = GText.view ~editable:true ~width:400 ~height:100 + ~packing:scrolled_window#add () in + let hbox = + GPack.hbox ~border_width:0 + ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let okb = + GButton.button ~label:"Ok" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let clearb = + GButton.button ~label:"Clear" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let cancelb = + GButton.button ~label:"Cancel" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + ignore (window#connect#destroy GMain.Main.quit) ; + ignore (cancelb#connect#clicked window#destroy) ; + ignore (clearb#connect#clicked (fun () -> + input#buffer#set_text DisambiguatingParser.EnvironmentP3.empty)) ; + ignore (okb#connect#clicked (fun () -> + chosen_aliases := Some (input#buffer#get_text ()); + window#destroy ())); + ignore + (input#buffer#insert ~iter:(input#buffer#get_iter_at_char 0) + (DisambiguatingParser.EnvironmentP3.to_string !disambiguation_env ^ "\n")); + window#show () ; + GtkThread.main (); + match !chosen_aliases with + | None -> () + | Some raw_aliases -> + let new_disambiguation_env = + (try + DisambiguatingParser.EnvironmentP3.of_string raw_aliases + with e -> + HelmLogger.log + (`Error (`T + ("Error while parsing aliases: " ^ Printexc.to_string e))); + !disambiguation_env) + in + disambiguation_env := new_disambiguation_env +;; + +let proveit () = + let module L = LogicalOperations in + let module G = Gdome in + let notebook = (rendering_window ())#notebook in + let output = (rendering_window ())#output in + try + output#make_sequent_of_selected_term ; + refresh_proof output ; + refresh_goals notebook + with + InvokeTactics.RefreshSequentException e -> + HelmLogger.log + (`Error (`T ("Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e))) + | InvokeTactics.RefreshProofException e -> + HelmLogger.log + (`Error (`T ("Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e))) + | e -> + HelmLogger.log + (`Error (`T (Printexc.to_string e))) +;; + +let focus () = + let module L = LogicalOperations in + let module G = Gdome in + let notebook = (rendering_window ())#notebook in + let output = (rendering_window ())#output in + try + output#focus_sequent_of_selected_term ; + refresh_goals notebook + with + InvokeTactics.RefreshSequentException e -> + HelmLogger.log + (`Error (`T ("Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e))) + | InvokeTactics.RefreshProofException e -> + HelmLogger.log + (`Error (`T ("Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e))) + | e -> + HelmLogger.log + (`Error (`T (Printexc.to_string e))) +;; + +exception NoPrevGoal;; +exception NoNextGoal;; + +let setgoal metano = + let module L = LogicalOperations in + let module G = Gdome in + let notebook = (rendering_window ())#notebook in + let output = (rendering_window ())#output in + let metasenv = + match ProofEngine.get_proof () with + None -> assert false + | Some (_,metasenv,_,_) -> metasenv in - read_lines () + try + refresh_goals ~empty_notebook:false notebook + with + InvokeTactics.RefreshSequentException e -> + HelmLogger.log + (`Error (`T ("Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e))) + | e -> + HelmLogger.log + (`Error (`T (Printexc.to_string e))) ;; -let applyStylesheets input styles args = - List.fold_left (fun i style -> Gdome_xslt.applyStylesheet i style args) - input styles +let + show_in_show_window_obj, show_in_show_window_uri, show_in_show_window_callback += + let window = + GWindow.window ~width:800 ~border_width:2 () 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 + 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 = + try + let mml,(_,(ids_to_terms,ids_to_father_ids,ids_to_conjectures, + ids_to_hypotheses,_,_)) = + ApplyTransformation.mml_of_cic_object obj + in + window#set_title (UriManager.string_of_uri uri) ; + window#misc#hide () ; window#show () ; + mmlwidget#load_root mml#get_documentElement ; + with + e -> + HelmLogger.log + (`Error (`T (Printexc.to_string e))) + in + let show_in_show_window_uri uri = + let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + show_in_show_window_obj uri obj + in + let show_in_show_window_callback mmlwidget ((n : Gdome.element option),_,_,_) = + match n with + None -> () + | Some n' -> + if n'#hasAttributeNS ~namespaceURI:Misc.xlink_ns ~localName:href then + let uri = + (n'#getAttributeNS ~namespaceURI:Misc.xlink_ns ~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) + in + show_in_show_window_obj, show_in_show_window_uri, + show_in_show_window_callback ;; -let mml_of_cic acic = -prerr_endline "BBB CREAZIONE" ; - let xml = - Cic2Xml.print_term (UriManager.uri_of_string "cic:/dummy.con") acic +exception NoObjectsLocated;; + +let user_uri_choice ~title ~msg uris = + let uri = + match uris with + [] -> raise NoObjectsLocated + | [uri] -> uri + | uris -> + match + interactive_user_uri_choice ~selection_mode:`SINGLE ~title ~msg uris + with + [uri] -> uri + | _ -> assert false in - Xml.pp ~quiet:true xml (Some filename4uwobo) ; -prerr_endline "BBB PARSING" ; - let input = domImpl#createDocumentFromURI ~uri:filename4uwobo () in -prerr_endline "BBB STYLESHEETS" ; - let output = applyStylesheets input mml_styles mml_args in -prerr_endline "BBB RESA" ; -ignore(domImpl#saveDocumentToFile ~doc:output ~name:"/tmp/xxxyyyzzz" ()) ; - output + String.sub uri 4 (String.length uri - 4) ;; +let locate_callback id = + let uris = MetadataQuery.locate ~dbd id in + HelmLogger.log (`Msg (`T ("Locate Query: " ^ id))) ; + HelmLogger.log (`Msg (`T "Result:")) ; + List.iter (fun uri -> HelmLogger.log (`Msg (`T uri))) uris; + user_uri_choice ~title:"Ambiguous input." + ~msg:(sprintf "Ambiguous input \"%s\". Please, choose one interpetation:" id) + uris +;; -(* CALLBACKS *) -let exact rendering_window () = - let inputt = (rendering_window#inputt : GEdit.text) in -(*CSC: Gran cut&paste da sotto... *) - let inputlen = inputt#length in - let input = inputt#get_chars 0 inputlen ^ "\n" in - let lexbuf = Lexing.from_string input in +let input_or_locate_uri ~title = + let uri = ref None in + let window = + GWindow.window + ~width:400 ~modal:true ~title ~border_width:2 () in + let vbox = GPack.vbox ~packing:window#add () in + let hbox1 = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let _ = + GMisc.label ~text:"Enter a valid URI:" ~packing:(hbox1#pack ~padding:5) () in + let manual_input = + GEdit.entry ~editable:true + ~packing:(hbox1#pack ~expand:true ~fill:true ~padding:5) () in + let checkb = + GButton.button ~label:"Check" + ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in + let _ = checkb#misc#set_sensitive false in + let hbox2 = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let _ = + GMisc.label ~text:"You can also enter an indentifier to locate:" + ~packing:(hbox2#pack ~padding:5) () in + let locate_input = + GEdit.entry ~editable:true + ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in + let locateb = + GButton.button ~label:"Locate" + ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in + let _ = locateb#misc#set_sensitive false in + let hbox3 = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let okb = + GButton.button ~label:"Ok" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let _ = okb#misc#set_sensitive false in + let cancelb = + GButton.button ~label:"Cancel" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () + in + ignore (window#connect#destroy GMain.Main.quit) ; + ignore + (cancelb#connect#clicked (function () -> uri := None ; window#destroy ())) ; + let check_callback () = + let uri = "cic:" ^ manual_input#text in try - while true do - (* Execute the actions *) - match CicTextualParser.main CicTextualLexer.token lexbuf with - None -> () - | Some expr -> - try -(*??? Ma servira' da qualche parte! - let ty = CicTypeChecker.type_of_aux' [] expr in -*) - let (acic, ids_to_terms, ids_to_father_ids) = - Cic2acic.acic_of_cic expr - in -(*CSC: chiamare la vera tattica exact qui! *) - () - with - e -> - print_endline ("? " ^ CicPp.ppterm expr) ; - raise e - done + ignore (Http_getter.resolve' (UriManager.uri_of_string uri)) ; + HelmLogger.log (`Msg (`T "OK")) ; + true with - CicTextualParser0.Eof -> - inputt#delete_text 0 inputlen -(*CSC: fare qualcosa di utile *) + Http_getter_types.Key_not_found _ -> + HelmLogger.log + (`Error (`T ("URI " ^ uri ^ + " does not correspond to any object."))) ; + false + | UriManager.IllFormedUri _ -> + HelmLogger.log + (`Error (`T ("URI " ^ uri ^ " is not well-formed."))) ; + false | e -> - print_endline ("Error: " ^ Printexc.to_string e) ; flush stdout + HelmLogger.log + (`Error (`T (Printexc.to_string e))) ; + false + in + ignore + (okb#connect#clicked + (function () -> + if check_callback () then + begin + uri := Some manual_input#text ; + window#destroy () + end + )) ; + ignore (checkb#connect#clicked (function () -> ignore (check_callback ()))) ; + ignore + (manual_input#connect#changed + (fun _ -> + if manual_input#text = "" then + begin + checkb#misc#set_sensitive false ; + okb#misc#set_sensitive false + end + else + begin + checkb#misc#set_sensitive true ; + okb#misc#set_sensitive true + end)); + ignore + (locate_input#connect#changed + (fun _ -> locateb#misc#set_sensitive (locate_input#text <> ""))) ; + ignore + (locateb#connect#clicked + (function () -> + let id = locate_input#text in + manual_input#set_text (locate_callback id) ; + locate_input#delete_text 0 (String.length id) + )) ; + window#show () ; + GtkThread.main (); + match !uri with + None -> raise NoChoice + | Some uri -> UriManager.uri_of_string ("cic:" ^ uri) ;; -let proveit rendering_window () = - let module G = Gdome in - match rendering_window#output#get_selection with - Some node -> - let xpath = - ((node : Gdome.element)#getAttributeNS - (*CSC: OCAML DIVERGE - ((element : G.element)#getAttributeNS - *) - ~namespaceURI:helmns - ~localName:(G.domString "xref"))#to_string - in - if xpath = "" then assert false (* "ERROR: No xref found!!!" *) - else - begin - match !current_cic_infos with - Some (ids_to_terms, ids_to_father_ids) -> - let id = xpath in - let sequent = - LogicalOperations.to_sequent id ids_to_terms ids_to_father_ids +exception AmbiguousInput;; + +(* A WIDGET TO ENTER CIC TERMS *) + +module DisambiguateCallbacks = + struct + let interactive_user_uri_choice = + fun ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id -> + interactive_user_uri_choice ~selection_mode ?ok + ?enable_button_for_non_vars ~title ~msg + let interactive_interpretation_choice = interactive_interpretation_choice + let input_or_locate_uri ~title ?id () = input_or_locate_uri ~title + end +;; + +module TermEditor' = ChosenTermEditor.Make (DisambiguateCallbacks);; + +(* OTHER FUNCTIONS *) + +let locate () = + let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in + try + match + GToolbox.input_string ~title:"Locate" "Enter an identifier to locate:" + with + None -> raise NoChoice + | Some input -> + let uri = locate_callback input in + inputt#set_term uri + with + e -> + HelmLogger.log + (`Error (`T (Printexc.to_string e))) +;; + + +exception UriAlreadyInUse;; +exception NotAUriToAConstant;; + +let new_inductive () = + let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in + let output = ((rendering_window ())#output : TermViewer.proof_viewer) in + let notebook = (rendering_window ())#notebook in + + let chosen = ref false in + let inductive = ref true in + let paramsno = ref 0 in + let get_uri = ref (function _ -> assert false) in + let get_base_uri = ref (function _ -> assert false) in + let get_names = ref (function _ -> assert false) in + let get_types_and_cons = ref (function _ -> assert false) in + let get_context_and_subst = ref (function _ -> assert false) in + let window = + GWindow.window + ~width:600 ~modal:true ~position:`CENTER + ~title:"New Block of Mutual (Co)Inductive Definitions" + ~border_width:2 () in + let vbox = GPack.vbox ~packing:window#add () in + let hbox = + GPack.hbox ~border_width:0 + ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let _ = + GMisc.label ~text:"Enter the URI for the new block:" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let uri_entry = + GEdit.entry ~editable:true + ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in + let hbox0 = + GPack.hbox ~border_width:0 + ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let _ = + GMisc.label + ~text: + "Enter the number of left parameters in every arity and constructor type:" + ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in + let paramsno_entry = + GEdit.entry ~editable:true ~text:"0" + ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in + let hbox1 = + GPack.hbox ~border_width:0 + ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let _ = + GMisc.label ~text:"Are the definitions inductive or coinductive?" + ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in + let inductiveb = + GButton.radio_button ~label:"Inductive" + ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in + let coinductiveb = + GButton.radio_button ~label:"Coinductive" + ~group:inductiveb#group + ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in + let hbox2 = + GPack.hbox ~border_width:0 + ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let _ = + GMisc.label ~text:"Enter the list of the names of the types:" + ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in + let names_entry = + GEdit.entry ~editable:true + ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in + let hboxn = + GPack.hbox ~border_width:0 + ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let okb = + GButton.button ~label:"> Next" + ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in + let _ = okb#misc#set_sensitive true in + let cancelb = + GButton.button ~label:"Abort" + ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in + ignore (window#connect#destroy GMain.Main.quit) ; + ignore (cancelb#connect#clicked window#destroy) ; + (* First phase *) + let rec phase1 () = + ignore + (okb#connect#clicked + (function () -> + try + let uristr = "cic:" ^ uri_entry#text in + let namesstr = names_entry#text in + let paramsno' = int_of_string (paramsno_entry#text) in + match Str.split (Str.regexp " +") namesstr with + [] -> assert false + | (he::tl) as names -> + let uri = UriManager.uri_of_string (uristr ^ "/" ^ he ^ ".ind") in + begin + try + ignore (Http_getter.resolve' uri) ; + raise UriAlreadyInUse + with Http_getter_types.Key_not_found _ -> + get_uri := (function () -> uri) ; + get_names := (function () -> names) ; + inductive := inductiveb#active ; + paramsno := paramsno' ; + phase2 () + end + with + e -> + HelmLogger.log + (`Error (`T (Printexc.to_string e))) + )) + (* Second phase *) + and phase2 () = + let type_widgets = + List.map + (function name -> + let frame = + GBin.frame ~label:name + ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in + let vbox = GPack.vbox ~packing:frame#add () in + let hbox = GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false) () in + let _ = + GMisc.label ~text:("Enter its type:") + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let scrolled_window = + GBin.scrolled_window ~border_width:5 + ~packing:(vbox#pack ~expand:true ~padding:0) () in + let newinputt = + TermEditor'.term_editor + ~dbd + ~width:400 ~height:20 ~packing:scrolled_window#add + ~share_environment_with:inputt () + ~isnotempty_callback: + (function b -> + (*non_empty_type := b ;*) + okb#misc#set_sensitive true) (*(b && uri_entry#text <> ""))*) + in + let hbox = + GPack.hbox ~border_width:0 + ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let _ = + GMisc.label ~text:("Enter the list of its constructors:") + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let cons_names_entry = + GEdit.entry ~editable:true + ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in + (newinputt,cons_names_entry) + ) (!get_names ()) + in + vbox#remove hboxn#coerce ; + let hboxn = + GPack.hbox ~border_width:0 + ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let okb = + GButton.button ~label:"> Next" + ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in + let cancelb = + GButton.button ~label:"Abort" + ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in + ignore (cancelb#connect#clicked window#destroy) ; + ignore + (okb#connect#clicked + (function () -> + try + let names = !get_names () in + let types_and_cons = + List.map2 + (fun name (newinputt,cons_names_entry) -> + let consnamesstr = cons_names_entry#text in + let cons_names = Str.split (Str.regexp " +") consnamesstr in + let metasenv,expr,ugraph = + newinputt#get_metasenv_and_term ~context:[] ~metasenv:[] + in + match metasenv with + [] -> expr,cons_names + | _ -> raise AmbiguousInput + ) names type_widgets + in + let uri = !get_uri () in + let _ = + (* Let's see if so far the definition is well-typed *) + let params = [] in + let paramsno = 0 in + (* To test if the arities of the inductive types are well *) + (* typed, we check the inductive block definition where *) + (* no constructor is given to each type. *) + let tys = + List.map2 + (fun name (ty,cons) -> (name, !inductive, ty, [])) + names types_and_cons + in + CicTypeChecker.typecheck_mutual_inductive_defs uri + (tys,params,paramsno) + in + get_context_and_subst := + (function () -> + let i = ref 0 in + List.fold_left2 + (fun (context,subst) name (ty,_) -> + let res = + (Some (Cic.Name name, Cic.Decl ty))::context, + (Cic.MutInd (uri,!i,[]))::subst + in + incr i ; res + ) ([],[]) names types_and_cons) ; + let types_and_cons' = + List.map2 + (fun name (ty,cons) -> (name, !inductive, ty, phase3 name cons)) + names types_and_cons + in + get_types_and_cons := (function () -> types_and_cons') ; + chosen := true ; + window#destroy () + with + e -> + HelmLogger.log + (`Error (`T (Printexc.to_string e))) + )) + (* Third phase *) + and phase3 name cons = + let get_cons_types = ref (function () -> assert false) in + let window2 = + GWindow.window + ~width:600 ~modal:true ~position:`CENTER + ~title:(name ^ " Constructors") + ~border_width:2 () in + let vbox = GPack.vbox ~packing:window2#add () in + let cons_type_widgets = + List.map + (function consname -> + let hbox = + GPack.hbox ~border_width:0 + ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let _ = + GMisc.label ~text:("Enter the type of " ^ consname ^ ":") + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let scrolled_window = + GBin.scrolled_window ~border_width:5 + ~packing:(vbox#pack ~expand:true ~padding:0) () in + let newinputt = + TermEditor'.term_editor + ~dbd + ~width:400 ~height:20 ~packing:scrolled_window#add + ~share_environment_with:inputt () + ~isnotempty_callback: + (function b -> + (* (*non_empty_type := b ;*) + okb#misc#set_sensitive true) (*(b && uri_entry#text <> ""))*) *)()) + in + newinputt + ) cons in + let hboxn = + GPack.hbox ~border_width:0 + ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let okb = + GButton.button ~label:"> Next" + ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in + let _ = okb#misc#set_sensitive true in + let cancelb = + GButton.button ~label:"Abort" + ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in + ignore (window2#connect#destroy GMain.Main.quit) ; + ignore (cancelb#connect#clicked window2#destroy) ; + ignore + (okb#connect#clicked + (function () -> + try + chosen := true ; + let context,subst= !get_context_and_subst () in + let cons_types = + List.map2 + (fun name inputt -> + let metasenv,expr,ugraph = + inputt#get_metasenv_and_term ~context ~metasenv:[] in - SequentPp.TextualPp.print_sequent sequent ; - let sequent_gdome = SequentPp.XmlPp.print_sequent sequent in - let sequent_doc = - Xml2Gdome.document_of_xml domImpl sequent_gdome - in - let sequent_mml = - applyStylesheets sequent_doc sequent_styles sequent_args - in - rendering_window#proofw#load_tree ~dom:sequent_mml ; -ignore(domImpl#saveDocumentToFile ~doc:sequent_doc - ~name:"/public/sacerdot/guruguru1" ~indent:true ()) ; -ignore(domImpl#saveDocumentToFile ~doc:sequent_mml - ~name:"/public/sacerdot/guruguru2" ~indent:true ()) - | None -> assert false (* "ERROR: No current term!!!" *) - end - | None -> assert false (* "ERROR: No selection!!!" *) -;; - -let output_html outputhtml msg = - htmlheader_and_content := !htmlheader_and_content ^ msg ; - outputhtml#source (!htmlheader_and_content ^ htmlfooter) -;; - -let execute rendering_window () = - let inputt = (rendering_window#inputt : GEdit.text) in - let oldinputt = (rendering_window#oldinputt : GEdit.text) in - let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in - let output = (rendering_window#output : GMathView.math_view) in - let proofw = (rendering_window#proofw : GMathView.math_view) in - let inputlen = inputt#length in - let input = inputt#get_chars 0 inputlen ^ "\n" in - (* Do something interesting *) - let lexbuf = Lexing.from_string input in - try - while true do - (* Execute the actions *) - match CicTextualParser.main CicTextualLexer.token lexbuf with - None -> () - | Some expr -> + match metasenv with + [] -> + let undebrujined_expr = + List.fold_left + (fun expr t -> CicSubstitution.subst t expr) expr subst + in + name, undebrujined_expr + | _ -> raise AmbiguousInput + ) cons cons_type_widgets + in + get_cons_types := (function () -> cons_types) ; + window2#destroy () + with + e -> + HelmLogger.log + (`Error (`T (Printexc.to_string e))) + )) ; + window2#show () ; + GtkThread.main (); + let okb_pressed = !chosen in + chosen := false ; + if (not okb_pressed) then + begin + window#destroy () ; + assert false (* The control never reaches this point *) + end + else + (!get_cons_types ()) + in + phase1 () ; + (* No more phases left or Abort pressed *) + window#show () ; + GtkThread.main (); + window#destroy () ; + if !chosen then + try + let uri = !get_uri () in +(*CSC: Da finire *) + let params = [] in + let tys = !get_types_and_cons () in + let obj = Cic.InductiveDefinition(tys,params,!paramsno,[]) in + let u = + begin + try + debug_print (CicPp.ppobj obj); + CicTypeChecker.typecheck_mutual_inductive_defs uri + (tys,params,!paramsno) CicUniv.empty_ugraph + with + e -> + debug_print "Offending mutual (co)inductive type declaration:" ; + debug_print (CicPp.ppobj obj) ; + (* I think we should fail here! *) + CicUniv.empty_ugraph + end + in + (* We already know that obj is well-typed. We need to add it to the *) + (* environment in order to compute the inner-types without having to *) + (* debrujin it or having to modify lots of other functions to avoid *) + (* asking the environment for the MUTINDs we are defining now. *) + + (* u should be cleaned before adding it to the env *) + CicEnvironment.put_inductive_definition uri (obj,u) ; + save_obj uri obj ; + (* TASSI: FIXME we should save the cleaned u here *) + show_in_show_window_obj uri obj + with + e -> + HelmLogger.log + (`Error (`T (Printexc.to_string e))) +;; + +let new_proof () = + let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in + let output = ((rendering_window ())#output : TermViewer.proof_viewer) in + let notebook = (rendering_window ())#notebook in + + let chosen = ref false in + let get_metasenv_and_term = ref (function _ -> assert false) in + let get_uri = ref (function _ -> assert false) in + let non_empty_type = ref false in + let window = + GWindow.window + ~width:600 ~modal:true ~title:"New Proof or Definition" + ~border_width:2 () in + let vbox = GPack.vbox ~packing:window#add () in + let hbox = + GPack.hbox ~border_width:0 + ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let _ = + GMisc.label ~text:"Enter the URI for the new theorem or definition:" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let uri_entry = + GEdit.entry ~editable:true + ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in + uri_entry#set_text dummy_uri; + uri_entry#select_region ~start:1 ~stop:(String.length dummy_uri); + let hbox1 = + GPack.hbox ~border_width:0 + ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let _ = + GMisc.label ~text:"Enter the theorem or definition type:" + ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in + let scrolled_window = + GBin.scrolled_window ~border_width:5 + ~packing:(vbox#pack ~expand:true ~padding:0) () in + (* the content of the scrolled_window is moved below (see comment) *) + let hbox = + GPack.hbox ~border_width:0 + ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let okb = + GButton.button ~label:"Ok" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let _ = okb#misc#set_sensitive false in + let cancelb = + GButton.button ~label:"Cancel" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + (* moved here to have visibility of the ok button *) + let newinputt = + TermEditor'.term_editor + ~dbd + ~width:400 ~height:100 ~packing:scrolled_window#add + ~share_environment_with:inputt () + ~isnotempty_callback: + (function b -> + non_empty_type := b ; + okb#misc#set_sensitive (b && uri_entry#text <> "")) + in + let _ = + newinputt#set_term inputt#get_as_string ; + inputt#reset in + let _ = + uri_entry#connect#changed + (function () -> + okb#misc#set_sensitive (!non_empty_type && uri_entry#text <> "")) + in + ignore (window#connect#destroy GMain.Main.quit) ; + ignore (cancelb#connect#clicked window#destroy) ; + ignore + (okb#connect#clicked + (function () -> + chosen := true ; + try + let metasenv,parsed,ugraph = newinputt#get_metasenv_and_term [] [] in + let uristr = "cic:" ^ uri_entry#text in + let uri = UriManager.uri_of_string uristr in + if String.sub uristr (String.length uristr - 4) 4 <> ".con" then + raise NotAUriToAConstant + else + begin try - let ty = CicTypeChecker.type_of_aux' [] expr in - let whd = CicReduction.whd expr in + ignore (Http_getter.resolve' uri) ; + raise UriAlreadyInUse + with Http_getter_types.Key_not_found _ -> + get_metasenv_and_term := (function () -> metasenv,parsed) ; + get_uri := (function () -> uri) ; + window#destroy () + end + with + e -> + HelmLogger.log + (`Error (`T (Printexc.to_string e))) + )) ; + window#show () ; + GtkThread.main (); + if !chosen then + try + let metasenv,expr = !get_metasenv_and_term () in + let _ = CicTypeChecker.type_of_aux' metasenv [] expr in + ProofEngine.set_proof + (Some (Some (!get_uri ()), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr)); + set_proof_engine_goal (Some 1) ; + refresh_goals notebook ; + refresh_proof output ; + !save_set_sensitive true ; + inputt#reset ; + ProofEngine.intros ~mk_fresh_name_callback () ; + refresh_goals notebook ; + refresh_proof output + with + InvokeTactics.RefreshSequentException e -> + HelmLogger.log + (`Error (`T ("Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e))) + | InvokeTactics.RefreshProofException e -> + HelmLogger.log + (`Error (`T ("Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e))) + | e -> + HelmLogger.log + (`Error (`T (Printexc.to_string e))) +;; - let (acic, ids_to_terms, ids_to_father_ids) = - Cic2acic.acic_of_cic expr - in - let mml = mml_of_cic acic in - output#load_tree mml ; -prerr_endline "BBB FINE RESA" ; - current_cic_infos := Some (ids_to_terms,ids_to_father_ids) ; -print_endline ("? " ^ CicPp.ppterm expr) ; -print_endline (">> " ^ CicPp.ppterm whd) ; -print_endline (": " ^ CicPp.ppterm ty) ; -flush stdout ; - with - e -> - print_endline ("? " ^ CicPp.ppterm expr) ; - raise e - done - with - CicTextualParser0.Eof -> - inputt#delete_text 0 inputlen ; - ignore(oldinputt#insert_text input oldinputt#length) ; - | e -> - print_endline ("Error: " ^ Printexc.to_string e) ; flush stdout +let check_term_in_scratch scratch_window metasenv context expr = + try + let ty,ugraph = + CicTypeChecker.type_of_aux' metasenv context expr CicUniv.empty_ugraph + in + let expr = Cic.Cast (expr,ty) in + scratch_window#show () ; + scratch_window#set_term expr ; + scratch_window#set_context context ; + scratch_window#set_metasenv metasenv ; + scratch_window#sequent_viewer#load_sequent metasenv (111,context,expr) + with + e -> + print_endline ("? " ^ CicPp.ppterm expr) ; + raise e ;; -let choose_selection - (mmlwidget : GMathView.math_view) (element : Gdome.element option) -= +let check scratch_window () = + let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in + let metasenv = + match ProofEngine.get_proof () with + None -> [] + | Some (_,metasenv,_,_) -> metasenv + in + let context = + match !ProofEngine.goal with + None -> [] + | Some metano -> + let (_,canonical_context,_) = + List.find (function (m,_,_) -> m=metano) metasenv + in + canonical_context + in + try + let metasenv',expr,ugraph = + inputt#get_metasenv_and_term context metasenv + in + check_term_in_scratch scratch_window metasenv' context expr + with + e -> + HelmLogger.log + (`Error (`T (Printexc.to_string e))) +;; + +let show () = + try + show_in_show_window_uri (input_or_locate_uri ~title:"Show") + with + e -> + HelmLogger.log + (`Error (`T (Printexc.to_string e))) +;; + +exception NotADefinition;; + +let open_ () = + let output = ((rendering_window ())#output : TermViewer.proof_viewer) in + let notebook = (rendering_window ())#notebook in + try + let uri = input_or_locate_uri ~title:"Open" in + ignore(CicTypeChecker.typecheck uri CicUniv.empty_ugraph); + (* TASSI: typecheck mette la uri nell'env... cosa fa la open_ ?*) + let metasenv,bo,ty = + match fst(CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri ) with + Cic.Constant (_,Some bo,ty,_,_) -> [],bo,ty + | Cic.CurrentProof (_,metasenv,bo,ty,_,_) -> metasenv,bo,ty + | Cic.Constant _ + | Cic.Variable _ + | Cic.InductiveDefinition _ -> raise NotADefinition + in + ProofEngine.set_proof (Some (Some uri, metasenv, bo, ty)) ; + set_proof_engine_goal None ; + refresh_goals notebook ; + refresh_proof output ; + !save_set_sensitive true + with + InvokeTactics.RefreshSequentException e -> + HelmLogger.log + (`Error (`T ("Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e))) + | InvokeTactics.RefreshProofException e -> + HelmLogger.log + (`Error (`T ("Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e))) + | e -> + HelmLogger.log + (`Error (`T (Printexc.to_string e))) +;; + +let show_query_results results = + let window = + GWindow.window + ~modal:false ~title:"Query results." ~border_width:2 () in + let vbox = GPack.vbox ~packing:window#add () in + let hbox = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let lMessage = + GMisc.label + ~text:"Click on a URI to show that object" + ~packing:hbox#add () in + let scrolled_window = + GBin.scrolled_window ~border_width:10 ~height:400 ~width:600 + ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in + let clist = GList.clist ~columns:1 ~packing:scrolled_window#add () in + ignore + (List.map + (function (uri,_) -> + let n = + clist#append [uri] + in + clist#set_row ~selectable:false n + ) results + ) ; + clist#columns_autosize () ; + ignore + (clist#connect#select_row + (fun ~row ~column ~event -> + let (uristr,_) = List.nth results row in + match CicUtil.term_of_uri uristr with + | Cic.Const (uri, _) + | Cic.Var (uri, _) + | Cic.MutInd (uri, _, _) + | Cic.MutConstruct (uri, _, _, _) -> + show_in_show_window_uri uri + | _ -> assert false + ) + ) ; + window#show () +;; + +let refine_constraints (must_obj,must_rel,must_sort) = + let chosen = ref false in + let use_only = ref false in + let window = + GWindow.window + ~modal:true ~title:"Constraints refinement." + ~width:800 ~border_width:2 () in + let vbox = GPack.vbox ~packing:window#add () in + let hbox = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let lMessage = + GMisc.label + ~text: "\"Only\" constraints can be enforced or not." + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let onlyb = + GButton.toggle_button ~label:"Enforce \"only\" constraints" + ~active:false ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () + in + ignore + (onlyb#connect#toggled (function () -> use_only := onlyb#active)) ; + (* Notebook for the constraints choice *) + let notebook = + GPack.notebook ~scrollable:true + ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in + (* Rel constraints *) + let label = + GMisc.label + ~text: "Constraints on Rels" () in + let vbox' = + GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce) + () in + let hbox = + GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in + let lMessage = + GMisc.label + ~text: "You can now specify the constraints on Rels." + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let expected_height = 25 * (List.length must_rel + 2) in + let height = if expected_height > 400 then 400 else expected_height in + let scrolled_window = + GBin.scrolled_window ~border_width:10 ~height ~width:600 + ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in + let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in + let mk_depth_button (hbox:GPack.box) d = + let mutable_ref = ref (Some d) in + let depthb = + GButton.toggle_button + ~label:("depth = " ^ string_of_int d) + ~active:true + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () + in + ignore + (depthb#connect#toggled + (function () -> + let sel_depth = if depthb#active then Some d else None in + mutable_ref := sel_depth + )) ; mutable_ref + in + let rel_constraints = + List.map + (function p -> + let hbox = + GPack.hbox + ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in + let lMessage = + GMisc.label + ~text:(MQGU.text_of_position (p:>MQGT.full_position)) + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + match p with + | `MainHypothesis None + | `MainConclusion None -> p, ref None + | `MainHypothesis (Some depth') + | `MainConclusion (Some depth') -> p, mk_depth_button hbox depth' + ) must_rel in + (* Sort constraints *) + let label = + GMisc.label + ~text: "Constraints on Sorts" () in + let vbox' = + GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce) + () in + let hbox = + GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in + let lMessage = + GMisc.label + ~text: "You can now specify the constraints on Sorts." + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let expected_height = 25 * (List.length must_sort + 2) in + let height = if expected_height > 400 then 400 else expected_height in + let scrolled_window = + GBin.scrolled_window ~border_width:10 ~height ~width:600 + ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in + let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in + let sort_constraints = + List.map + (function (p, sort) -> + let hbox = + GPack.hbox + ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in + let lMessage = + GMisc.label + ~text:(MQGU.text_of_sort sort ^ " " ^ MQGU.text_of_position (p:>MQGT.full_position)) + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + match p with + | `MainHypothesis None + | `MainConclusion None -> p, ref None, sort + | `MainHypothesis (Some depth') + | `MainConclusion (Some depth') -> p, mk_depth_button hbox depth', sort + ) must_sort in + (* Obj constraints *) + let label = + GMisc.label + ~text: "Constraints on constants" () in + let vbox' = + GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce) + () in + let hbox = + GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in + let lMessage = + GMisc.label + ~text: "You can now specify the constraints on constants." + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let expected_height = 25 * (List.length must_obj + 2) in + let height = if expected_height > 400 then 400 else expected_height in + let scrolled_window = + GBin.scrolled_window ~border_width:10 ~height ~width:600 + ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in + let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in + let obj_constraints = + List.map + (function (p, uri) -> + let hbox = + GPack.hbox + ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in + let lMessage = + GMisc.label + ~text:(uri ^ " " ^ (MQGU.text_of_position p)) + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + match p with + | `InBody + | `InHypothesis + | `InConclusion + | `MainHypothesis None + | `MainConclusion None -> p, ref None, uri + | `MainHypothesis (Some depth') + | `MainConclusion (Some depth') -> p, mk_depth_button hbox depth', uri + ) must_obj in + (* Confirm/abort buttons *) + let hbox = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let okb = + GButton.button ~label:"Ok" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let cancelb = + GButton.button ~label:"Abort" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () + in + ignore (window#connect#destroy GMain.Main.quit) ; + ignore (cancelb#connect#clicked window#destroy) ; + ignore + (okb#connect#clicked (function () -> chosen := true ; window#destroy ())); + window#set_position `CENTER ; + window#show () ; + GtkThread.main (); + if !chosen then + let chosen_must_rel = + List.map + (function (position, ref_depth) -> MQGU.set_main_position position !ref_depth) + rel_constraints + in + let chosen_must_sort = + List.map + (function (position, ref_depth, sort) -> + MQGU.set_main_position position !ref_depth,sort) + sort_constraints + in + let chosen_must_obj = + List.map + (function (position, ref_depth, uri) -> MQGU.set_full_position position !ref_depth, uri) + obj_constraints + in + (chosen_must_obj,chosen_must_rel,chosen_must_sort), + (if !use_only then +(*CSC: ???????????????????????? I assume that must and only are the same... *) + Some chosen_must_obj,Some chosen_must_rel,Some chosen_must_sort + else + None,None,None + ) + else + raise NoChoice +;; + +let completeSearchPattern () = + let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in + try + let metasenv,expr,ugraph = + inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in + let must = CGSearchPattern.get_constraints expr in + let must',only = refine_constraints must in + let query = + MQG.query_of_constraints (Some CGSearchPattern.universe) must' only + in + let results = MQI.execute mqi_handle query in + show_query_results results + with + e -> + HelmLogger.log + (`Error (`T (Printexc.to_string e))) +;; + +let insertQuery () = + try + let chosen = ref None in + let window = + GWindow.window + ~modal:true ~title:"Insert Query (Experts Only)" ~border_width:2 () in + let vbox = GPack.vbox ~packing:window#add () in + let label = + GMisc.label ~text:"Insert Query. For Experts Only." + ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let scrolled_window = + GBin.scrolled_window ~border_width:10 ~height:400 ~width:600 + ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in + let input = GText.view ~editable:true + ~packing:scrolled_window#add () in + let hbox = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let okb = + GButton.button ~label:"Ok" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let loadb = + GButton.button ~label:"Load from file..." + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let cancelb = + GButton.button ~label:"Abort" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + ignore (window#connect#destroy GMain.Main.quit) ; + ignore (cancelb#connect#clicked window#destroy) ; + ignore + (okb#connect#clicked + (function () -> + chosen := Some (input#buffer#get_text ()) ; window#destroy ())) ; + ignore + (loadb#connect#clicked + (function () -> + match + GToolbox.select_file ~title:"Select Query File" () + with + None -> () + | Some filename -> + let inch = open_in filename in + let rec read_file () = + try + let line = input_line inch in + line ^ "\n" ^ read_file () + with + End_of_file -> "" + in + let text = read_file () in + input#buffer#delete input#buffer#start_iter input#buffer#end_iter ; + ignore (input#buffer#insert text))) ; + window#set_position `CENTER ; + window#show () ; + GtkThread.main (); + match !chosen with + None -> () + | Some q -> + let results = + MQI.execute mqi_handle (MQueryUtil.query_of_text (Lexing.from_string q)) + in + show_query_results results + with + e -> + HelmLogger.log + (`Error (`T (Printexc.to_string e))) +;; + +let choose_must list_of_must only = + let chosen = ref None in + let user_constraints = ref [] in + let window = + GWindow.window + ~modal:true ~title:"Query refinement." ~border_width:2 () in + let vbox = GPack.vbox ~packing:window#add () in + let hbox = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let lMessage = + GMisc.label + ~text: + ("You can now specify the genericity of the query. " ^ + "The more generic the slower.") + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let hbox = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let lMessage = + GMisc.label + ~text: + "Suggestion: start with faster queries before moving to more generic ones." + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let notebook = + GPack.notebook ~scrollable:true + ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in + let _ = + let page = ref 0 in + let last = List.length list_of_must in + List.map + (function must -> + incr page ; + let label = + GMisc.label ~text: + (if !page = 1 then "More generic" else + if !page = last then "More precise" else " ") () in + let expected_height = 25 * (List.length must + 2) in + let height = if expected_height > 400 then 400 else expected_height in + let scrolled_window = + GBin.scrolled_window ~border_width:10 ~height ~width:600 + ~packing:(notebook#append_page ~tab_label:label#coerce) () in + let clist = + GList.clist ~columns:2 ~packing:scrolled_window#add + ~titles:["URI" ; "Position"] () + in + ignore + (List.map + (function (position, uri) -> + let n = + clist#append + [uri; MQGUtil.text_of_position position] + in + clist#set_row ~selectable:false n + ) must + ) ; + clist#columns_autosize () + ) list_of_must in + let _ = + let label = GMisc.label ~text:"User provided" () in + let vbox = + GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce) () in + let hbox = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let lMessage = + GMisc.label + ~text:"Select the constraints that must be satisfied and press OK." + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let expected_height = 25 * (List.length only + 2) in + let height = if expected_height > 400 then 400 else expected_height in + let scrolled_window = + GBin.scrolled_window ~border_width:10 ~height ~width:600 + ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in + let clist = + GList.clist ~columns:2 ~packing:scrolled_window#add + ~selection_mode:`MULTIPLE + ~titles:["URI" ; "Position"] () + in + ignore + (List.map + (function (position, uri) -> + let n = + clist#append + [uri; MQGUtil.text_of_position position] + in + clist#set_row ~selectable:true n + ) only + ) ; + clist#columns_autosize () ; + ignore + (clist#connect#select_row + (fun ~row ~column ~event -> + user_constraints := (List.nth only row)::!user_constraints)) ; + ignore + (clist#connect#unselect_row + (fun ~row ~column ~event -> + user_constraints := + List.filter + (function uri -> uri != (List.nth only row)) !user_constraints)) ; + in + let hbox = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let okb = + GButton.button ~label:"Ok" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let cancelb = + GButton.button ~label:"Abort" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + (* actions *) + ignore (window#connect#destroy GMain.Main.quit) ; + ignore (cancelb#connect#clicked window#destroy) ; + ignore + (okb#connect#clicked + (function () -> chosen := Some notebook#current_page ; window#destroy ())) ; + window#set_position `CENTER ; + window#show () ; + GtkThread.main (); + match !chosen with + None -> raise NoChoice + | Some n -> + if n = List.length list_of_must then + (* user provided constraints *) + !user_constraints + else + List.nth list_of_must n +;; + +let searchPattern () = + let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in + try + let proof = + match ProofEngine.get_proof () with + None -> assert false + | Some proof -> proof + in + match !ProofEngine.goal with + | None -> () + | Some metano -> + let uris' = List.map fst (MetadataQuery.hint ~dbd (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 -> + HelmLogger.log + (`Error (`T (Printexc.to_string e))) +;; + +let choose_selection mmlwidget (element : Gdome.element option) = let module G = Gdome in let rec aux element = if element#hasAttributeNS - ~namespaceURI:helmns + ~namespaceURI:Misc.helm_ns ~localName:(G.domString "xref") then mmlwidget#set_selection (Some element) else + try match element#get_parentNode with None -> assert false (*CSC: OCAML DIVERGES! | Some p -> aux (new G.element_of_node p) *) | Some p -> aux (new Gdome.element_of_node p) + with + GdomeInit.DOMCastException _ -> + debug_print + "******* trying to select above the document root ********" in match element with Some x -> aux x @@ -307,30 +2112,40 @@ let choose_selection (* Stuff for the widget settings *) -let export_to_postscript (output : GMathView.math_view) () = - output#export_to_postscript ~filename:"output.ps" (); +(* +let export_to_postscript output = + let lastdir = ref (Unix.getcwd ()) in + function () -> + match + GToolbox.select_file ~title:"Export to PostScript" + ~dir:lastdir ~filename:"screenshot.ps" () + with + None -> () + | Some filename -> + (output :> GMathView.math_view)#export_to_postscript + ~filename:filename (); ;; +*) -let activate_t1 (output : GMathView.math_view) button_set_anti_aliasing - button_set_kerning button_set_transparency button_export_to_postscript +(* +let activate_t1 output button_set_anti_aliasing + button_set_transparency export_to_postscript_menu_item button_t1 () = let is_set = button_t1#active in output#set_font_manager_type - (if is_set then `font_manager_t1 else `font_manager_gtk) ; + ~fm_type:(if is_set then `font_manager_t1 else `font_manager_gtk) ; if is_set then begin button_set_anti_aliasing#misc#set_sensitive true ; - button_set_kerning#misc#set_sensitive true ; button_set_transparency#misc#set_sensitive true ; - button_export_to_postscript#misc#set_sensitive true ; + export_to_postscript_menu_item#misc#set_sensitive true ; end else begin button_set_anti_aliasing#misc#set_sensitive false ; - button_set_kerning#misc#set_sensitive false ; button_set_transparency#misc#set_sensitive false ; - button_export_to_postscript#misc#set_sensitive false ; + export_to_postscript_menu_item#misc#set_sensitive false ; end ;; @@ -338,13 +2153,10 @@ let set_anti_aliasing output button_set_anti_aliasing () = output#set_anti_aliasing button_set_anti_aliasing#active ;; -let set_kerning output button_set_kerning () = - output#set_kerning button_set_kerning#active -;; - let set_transparency output button_set_transparency () = output#set_transparency button_set_transparency#active ;; +*) let changefont output font_size_spinb () = output#set_font_size font_size_spinb#value_as_int @@ -354,8 +2166,8 @@ let set_log_verbosity output log_verbosity_spinb () = output#set_log_verbosity log_verbosity_spinb#value_as_int ;; -class settings_window (output : GMathView.math_view) sw - button_export_to_postscript selection_changed_callback +class settings_window output sw + export_to_postscript_menu_item selection_changed_callback = let settings_window = GWindow.window ~title:"GtkMathView settings" () in let vbox = @@ -370,9 +2182,6 @@ class settings_window (output : GMathView.math_view) sw let button_set_anti_aliasing = GButton.toggle_button ~label:"set_anti_aliasing" ~packing:(table#attach ~left:0 ~top:1) () in - let button_set_kerning = - GButton.toggle_button ~label:"set_kerning" - ~packing:(table#attach ~left:1 ~top:1) () in let button_set_transparency = GButton.toggle_button ~label:"set_transparency" ~packing:(table#attach ~left:2 ~top:1) () in @@ -385,7 +2194,8 @@ class settings_window (output : GMathView.math_view) sw ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in let font_size_spinb = let sadj = - GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 () + GData.adjustment ~value:(float_of_int output#get_font_size) + ~lower:5.0 ~upper:50.0 ~step_incr:1.0 () in GEdit.spin_button ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in @@ -407,120 +2217,663 @@ object(self) method show = settings_window#show initializer button_set_anti_aliasing#misc#set_sensitive false ; - button_set_kerning#misc#set_sensitive false ; button_set_transparency#misc#set_sensitive false ; (* Signals connection *) + (* ignore(button_t1#connect#clicked - (activate_t1 output button_set_anti_aliasing button_set_kerning - button_set_transparency button_export_to_postscript button_t1)) ; + (activate_t1 output button_set_anti_aliasing + button_set_transparency export_to_postscript_menu_item button_t1)) ; + *) ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ; + (* ignore(button_set_anti_aliasing#connect#toggled (set_anti_aliasing output button_set_anti_aliasing)); - ignore(button_set_kerning#connect#toggled - (set_kerning output button_set_kerning)) ; ignore(button_set_transparency#connect#toggled (set_transparency output button_set_transparency)) ; + *) ignore(log_verbosity_spinb#connect#changed (set_log_verbosity output log_verbosity_spinb)) ; ignore(closeb#connect#clicked settings_window#misc#hide) end;; -(* Main windows *) +(* Scratch window *) -class rendering_window output proofw (label : GMisc.label) = +class scratch_window = let window = - GWindow.window ~title:"MathML viewer" ~border_width:2 () in - let hbox0 = - GPack.hbox ~packing:window#add () in + GWindow.window + ~title:"MathML viewer" + ~border_width:2 () in let vbox = - GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in - let _ = vbox#pack ~expand:false ~fill:false ~padding:5 label#coerce in - let scrolled_window0 = + GPack.vbox ~packing:window#add () in + let hbox = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let whdb = + GButton.button ~label:"Whd" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let reduceb = + GButton.button ~label:"Reduce" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let simplb = + GButton.button ~label:"Simpl" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let scrolled_window = GBin.scrolled_window ~border_width:10 ~packing:(vbox#pack ~expand:true ~padding:5) () in - let _ = scrolled_window0#add output#coerce in - let hbox1 = - GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let settingsb = - GButton.button ~label:"Settings" - ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in - let button_export_to_postscript = - GButton.button ~label:"export_to_postscript" - ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in - let closeb = - GButton.button ~label:"Close" - ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in - let hbox2 = - GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let proveitb = - GButton.button ~label:"Prove It" - ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in - let oldinputt = GEdit.text ~editable:false ~width:400 ~height:180 - ~packing:(vbox#pack ~padding:5) () in - let executeb = - GButton.button ~label:"Execute" - ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let inputt = GEdit.text ~editable:true ~width:400 ~height: 100 - ~packing:(vbox#pack ~padding:5) () in - let vbox1 = - GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in + let sequent_viewer = + TermViewer.sequent_viewer + ~mml_of_cic_sequent:ApplyTransformation.mml_of_cic_sequent + ~packing:(scrolled_window#add) ~width:400 ~height:280 () in +object(self) + val mutable term = Cic.Rel 1 (* dummy value *) + val mutable context = ([] : Cic.context) (* dummy value *) + val mutable metasenv = ([] : Cic.metasenv) (* dummy value *) + method sequent_viewer = sequent_viewer + method show () = window#misc#hide () ; window#show () + method term = term + method set_term t = term <- t + method context = context + method set_context t = context <- t + method metasenv = metasenv + method set_metasenv t = metasenv <- t + initializer + ignore + (sequent_viewer#connect#selection_changed (choose_selection sequent_viewer)); + ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ; + ignore(whdb#connect#clicked InvokeTactics'.whd_in_scratch) ; + ignore(reduceb#connect#clicked InvokeTactics'.reduce_in_scratch) ; + ignore(simplb#connect#clicked InvokeTactics'.simpl_in_scratch) +end;; + +let open_contextual_menu_for_selected_terms mmlwidget infos = + let button = GdkEvent.Button.button infos in + let terms_selected = List.length mmlwidget#get_selections > 0 in + if button = 3 then + begin + let time = GdkEvent.Button.time infos in + let menu = GMenu.menu () in + let f = new GMenu.factory menu in + let whd_menu_item = + f#add_item "Whd" ~key:GdkKeysyms._W ~callback:InvokeTactics'.whd in + let reduce_menu_item = + f#add_item "Reduce" ~key:GdkKeysyms._R ~callback:InvokeTactics'.reduce in + let simpl_menu_item = + f#add_item "Simpl" ~key:GdkKeysyms._S ~callback:InvokeTactics'.simpl in + let _ = f#add_separator () in + let generalize_menu_item = + f#add_item "Generalize" + ~key:GdkKeysyms._G ~callback:InvokeTactics'.generalize in + let _ = f#add_separator () in + let clear_menu_item = + f#add_item "Clear" ~key:GdkKeysyms._C ~callback:InvokeTactics'.clear in + let clearbody_menu_item = + f#add_item "ClearBody" + ~key:GdkKeysyms._B ~callback:InvokeTactics'.clearbody + in + whd_menu_item#misc#set_sensitive terms_selected ; + reduce_menu_item#misc#set_sensitive terms_selected ; + simpl_menu_item#misc#set_sensitive terms_selected ; + generalize_menu_item#misc#set_sensitive terms_selected ; + clear_menu_item#misc#set_sensitive terms_selected ; + clearbody_menu_item#misc#set_sensitive terms_selected ; + menu#popup ~button ~time + end ; + true +;; + +class page () = + let vbox1 = GPack.vbox () in +object(self) + val mutable proofw_ref = None + val mutable compute_ref = None + method proofw = + Lazy.force self#compute ; + match proofw_ref with + None -> assert false + | Some proofw -> proofw + method content = vbox1 + method compute = + match compute_ref with + None -> assert false + | Some compute -> compute + initializer + compute_ref <- + Some (lazy ( + let scrolled_window1 = + GBin.scrolled_window ~border_width:10 + ~packing:(vbox1#pack ~expand:true ~padding:5) () in + let proofw = + TermViewer.sequent_viewer + ~mml_of_cic_sequent:ApplyTransformation.mml_of_cic_sequent + ~width:400 ~height:275 ~packing:(scrolled_window1#add) () in + let _ = proofw_ref <- Some proofw in + let hbox3 = + GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in + let ringb = + GButton.button ~label:"Ring" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let fourierb = + GButton.button ~label:"Fourier" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let reflexivityb = + GButton.button ~label:"Reflexivity" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let symmetryb = + GButton.button ~label:"Symmetry" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let assumptionb = + GButton.button ~label:"Assumption" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let contradictionb = + GButton.button ~label:"Contradiction" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let autob= + GButton.button ~label:"Auto" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let hbox4 = + GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in + let existsb = + GButton.button ~label:"Exists" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let splitb = + GButton.button ~label:"Split" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let leftb = + GButton.button ~label:"Left" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let rightb = + GButton.button ~label:"Right" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let searchpatternb = + GButton.button ~label:"SearchPattern_Apply" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let hbox5 = + GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in + let exactb = + GButton.button ~label:"Exact" + ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in + let introsb = + GButton.button ~label:"Intros" + ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in + let applyb = + GButton.button ~label:"Apply" + ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in + let elimintrossimplb = + GButton.button ~label:"ElimIntrosSimpl" + ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in + let elimtypeb = + GButton.button ~label:"ElimType" + ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in + let foldwhdb = + GButton.button ~label:"Fold_whd" + ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in + let foldreduceb = + GButton.button ~label:"Fold_reduce" + ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in + let hbox6 = + GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in + let foldsimplb = + GButton.button ~label:"Fold_simpl" + ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in + let cutb = + GButton.button ~label:"Cut" + ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in + let changeb = + GButton.button ~label:"Change" + ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in + let letinb = + GButton.button ~label:"Let ... In" + ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in + let rewritesimplb = + GButton.button ~label:"RewriteSimpl ->" + ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in + let rewritebacksimplb = + GButton.button ~label:"RewriteSimpl <-" + ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in + let hbox7 = + GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in + let absurdb = + GButton.button ~label:"Absurd" + ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in + let decomposeb = + GButton.button ~label:"Decompose" + ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in + let transitivityb = + GButton.button ~label:"Transitivity" + ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in + 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" + ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in + let clearbodyb = + GButton.button ~label:"ClearBody" + ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in + let clearb = + GButton.button ~label:"Clear" + ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in + let whdb = + GButton.button ~label:"Whd" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let reduceb = + GButton.button ~label:"Reduce" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let simplb = + GButton.button ~label:"Simpl" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in +*) + + ignore(exactb#connect#clicked InvokeTactics'.exact) ; + ignore(applyb#connect#clicked InvokeTactics'.apply) ; + ignore(elimintrossimplb#connect#clicked InvokeTactics'.elimintrossimpl) ; + ignore(elimtypeb#connect#clicked InvokeTactics'.elimtype) ; + ignore(foldwhdb#connect#clicked InvokeTactics'.fold_whd) ; + ignore(foldreduceb#connect#clicked InvokeTactics'.fold_reduce) ; + ignore(foldsimplb#connect#clicked InvokeTactics'.fold_simpl) ; + ignore(cutb#connect#clicked InvokeTactics'.cut) ; + ignore(changeb#connect#clicked InvokeTactics'.change) ; + ignore(letinb#connect#clicked InvokeTactics'.letin) ; + ignore(ringb#connect#clicked InvokeTactics'.ring) ; + ignore(fourierb#connect#clicked InvokeTactics'.fourier) ; + ignore(rewritesimplb#connect#clicked InvokeTactics'.rewritesimpl) ; + ignore(rewritebacksimplb#connect#clicked InvokeTactics'.rewritebacksimpl) ; + ignore(replaceb#connect#clicked InvokeTactics'.replace) ; + ignore(reflexivityb#connect#clicked InvokeTactics'.reflexivity) ; + ignore(symmetryb#connect#clicked InvokeTactics'.symmetry) ; + ignore(transitivityb#connect#clicked InvokeTactics'.transitivity) ; + ignore(existsb#connect#clicked InvokeTactics'.exists) ; + ignore(splitb#connect#clicked InvokeTactics'.split) ; + ignore(leftb#connect#clicked InvokeTactics'.left) ; + ignore(rightb#connect#clicked InvokeTactics'.right) ; + ignore(assumptionb#connect#clicked InvokeTactics'.assumption) ; + ignore(absurdb#connect#clicked InvokeTactics'.absurd) ; + ignore(contradictionb#connect#clicked InvokeTactics'.contradiction) ; + 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) ; + ignore(autob#connect#clicked InvokeTactics'.auto) ; +(* Zack: spostare in una toolbar + ignore(whdb#connect#clicked whd) ; + ignore(reduceb#connect#clicked reduce) ; + ignore(simplb#connect#clicked simpl) ; + ignore(clearbodyb#connect#clicked clearbody) ; + ignore(clearb#connect#clicked clear) ; + ignore(generalizeb#connect#clicked generalize) ; +*) + ignore(proofw#connect#selection_changed (choose_selection proofw)) ; + ignore + ((new GObj.event_ops proofw#as_widget)#connect#button_press + (open_contextual_menu_for_selected_terms proofw)) ; + )) +end +;; + +class empty_page = + let vbox1 = GPack.vbox () in let scrolled_window1 = GBin.scrolled_window ~border_width:10 ~packing:(vbox1#pack ~expand:true ~padding:5) () in - let _ = scrolled_window1#add proofw#coerce in - let hbox3 = - GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in - let exactb = - GButton.button ~label:"Exact" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let outputhtml = - GHtml.xmhtml - ~source:"" - ~width:400 ~height: 200 - ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) - ~show:true () in + let proofw = + TermViewer.sequent_viewer + ~mml_of_cic_sequent:ApplyTransformation.mml_of_cic_sequent + ~width:400 ~height:275 ~packing:(scrolled_window1#add) () in object(self) - method outputhtml = outputhtml - method oldinputt = oldinputt + method proofw = (assert false : TermViewer.sequent_viewer) + method content = vbox1 + method compute = (assert false : unit) +end +;; + +let empty_page = new empty_page;; + +class notebook = +object(self) + val notebook = GPack.notebook () + val pages = ref [] + val mutable skip_switch_page_event = false + val mutable empty = true + method notebook = notebook + method add_page n = + let new_page = new page () in + empty <- false ; + pages := !pages @ [n,lazy (setgoal n),new_page] ; + notebook#append_page + ~tab_label:((GMisc.label ~text:("?" ^ string_of_int n) ())#coerce) + new_page#content#coerce + method remove_all_pages ~skip_switch_page_event:skip = + if empty then + notebook#remove_page 0 (* let's remove the empty page *) + else + List.iter (function _ -> notebook#remove_page 0) !pages ; + pages := [] ; + skip_switch_page_event <- skip + method set_current_page ~may_skip_switch_page_event n = + let (_,_,page) = List.find (function (m,_,_) -> m=n) !pages in + let new_page = notebook#page_num page#content#coerce in + if may_skip_switch_page_event && new_page <> notebook#current_page then + skip_switch_page_event <- true ; + notebook#goto_page new_page + method set_empty_page = + empty <- true ; + pages := [] ; + notebook#append_page + ~tab_label:((GMisc.label ~text:"No proof in progress" ())#coerce) + empty_page#content#coerce + method proofw = + let (_,_,page) = List.nth !pages notebook#current_page in + page#proofw + initializer + ignore + (notebook#connect#switch_page + (function i -> + let skip = skip_switch_page_event in + skip_switch_page_event <- false ; + if not skip then + try + let (metano,setgoal,page) = List.nth !pages i in + set_proof_engine_goal (Some metano) ; + Lazy.force (page#compute) ; + Lazy.force setgoal; + if notify_hbugs_on_goal_change then + Hbugs.notify () + with _ -> () + )) +end +;; + +let dump_environment () = + try + let oc = open_out (Helm_registry.get "gtoplevel.environment_file") in + HelmLogger.log (`Msg (`T "Dumping environment ...")); + CicEnvironment.dump_to_channel oc; + HelmLogger.log (`Msg (`T "... done!")) ; + close_out oc + with exc -> + HelmLogger.log + (`Error (`T (Printf.sprintf "Dump failure, uncaught exception:%s" + (Printexc.to_string exc)))) +;; +let restore_environment () = + try + let ic = open_in (Helm_registry.get "gtoplevel.environment_file") in + HelmLogger.log (`Msg (`T "Restoring environment ... ")); + CicEnvironment.restore_from_channel ic; + HelmLogger.log (`Msg (`T "... done!")); + close_in ic + with exc -> + HelmLogger.log + (`Error (`T (Printf.sprintf "Restore failure, uncaught exception:%s" + (Printexc.to_string exc)))) +;; + +(* Main window *) + +class rendering_window output (notebook : notebook) = + let scratch_window = new scratch_window in + let window = + 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 + ~packing:(vbox_for_menu#pack ~padding:0) () in + let menubar = GMenu.menu_bar ~packing:handle_box#add () in + let factory0 = new GMenu.factory menubar in + let accel_group = factory0#accel_group in + (* file menu *) + let file_menu = factory0#add_submenu "File" in + let factory1 = new GMenu.factory file_menu ~accel_group in + (* let export_to_postscript_menu_item = *) + let _ = + begin + let _ = + factory1#add_item "New Block of (Co)Inductive Definitions..." + ~key:GdkKeysyms._B ~callback:new_inductive + in + let _ = + factory1#add_item "New Proof or Definition..." ~key:GdkKeysyms._N + ~callback:new_proof + in + let reopen_menu_item = + factory1#add_item "Reopen a Finished Proof..." ~key:GdkKeysyms._R + ~callback:open_ + in + let qed_menu_item = + factory1#add_item "Qed" ~key:GdkKeysyms._E ~callback:qed in + ignore (factory1#add_separator ()) ; + ignore + (factory1#add_item "Load Unfinished Proof..." ~key:GdkKeysyms._L + ~callback:load_unfinished_proof) ; + let save_menu_item = + factory1#add_item "Save Unfinished Proof" ~key:GdkKeysyms._S + ~callback:save_unfinished_proof + in + ignore (factory1#add_separator ()) ; + ignore (factory1#add_item "Clear Environment" ~callback:CicEnvironment.empty); + ignore (factory1#add_item "Dump Environment" ~callback:dump_environment); + ignore + (factory1#add_item "Restore Environment" ~callback:restore_environment); + ignore + (save_set_sensitive := function b -> save_menu_item#misc#set_sensitive b); + ignore (!save_set_sensitive false); + ignore (qed_set_sensitive:=function b -> qed_menu_item#misc#set_sensitive b); + ignore (!qed_set_sensitive false); + ignore (factory1#add_separator ()) ; + (* + let export_to_postscript_menu_item = + factory1#add_item "Export to PostScript..." + ~callback:(export_to_postscript output) in + *) + ignore (factory1#add_separator ()) ; + ignore + (factory1#add_item "Exit" ~key:GdkKeysyms._Q ~callback:GMain.Main.quit) (*; + export_to_postscript_menu_item *) + end in + (* edit menu *) + let edit_menu = factory0#add_submenu "Edit Current Proof" in + let factory2 = new GMenu.factory edit_menu ~accel_group in + let focus_and_proveit_set_sensitive = ref (function _ -> assert false) in + let proveit_menu_item = + factory2#add_item "Prove It" ~key:GdkKeysyms._I + ~callback:(function () -> proveit ();!focus_and_proveit_set_sensitive false) + in + let focus_menu_item = + factory2#add_item "Focus" ~key:GdkKeysyms._F + ~callback:(function () -> focus () ; !focus_and_proveit_set_sensitive false) + in + let _ = + focus_and_proveit_set_sensitive := + function b -> + proveit_menu_item#misc#set_sensitive b ; + focus_menu_item#misc#set_sensitive b + in + let _ = !focus_and_proveit_set_sensitive false in + (* edit term menu *) + let edit_term_menu = factory0#add_submenu "Edit Term" in + let factory5 = new GMenu.factory edit_term_menu ~accel_group in + let check_menu_item = + factory5#add_item "Check Term" ~key:GdkKeysyms._C + ~callback:(check scratch_window) in + let _ = check_menu_item#misc#set_sensitive false in + (* search menu *) + 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 searchPattern_menu_item = + factory4#add_item "SearchPattern..." ~key:GdkKeysyms._D + ~callback:completeSearchPattern in + let _ = searchPattern_menu_item#misc#set_sensitive false in + let show_menu_item = + factory4#add_item "Show..." ~key:GdkKeysyms._H ~callback:show + in + let insert_query_item = + 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 _ = + factory6#add_check_item + ~active:false ~key:GdkKeysyms._F5 ~callback:Hbugs.toggle "HBugs enabled" + in + let _ = + factory6#add_item ~key:GdkKeysyms._Return ~callback:Hbugs.notify + "(Re)Submit status!" + in + let _ = factory6#add_separator () in + let _ = + factory6#add_item ~callback:Hbugs.start_web_services "Start Web Services" + in + let _ = + factory6#add_item ~callback:Hbugs.stop_web_services "Stop Web Services" + in + (* settings menu *) + let settings_menu = factory0#add_submenu "Settings" in + let factory3 = new GMenu.factory settings_menu ~accel_group in + let _ = + factory3#add_item "Edit Aliases..." ~key:GdkKeysyms._A + ~callback:edit_aliases in + let _ = + factory3#add_item "Clear Aliases" ~key:GdkKeysyms._K + ~callback:clear_aliases in + let autoitem = + factory3#add_check_item "Auto disambiguation" + ~callback:(fun checked -> auto_disambiguation := checked) in + let _ = factory3#add_separator () in + let _ = + factory3#add_item "MathML Widget Preferences..." ~key:GdkKeysyms._P + ~callback:(function _ -> (settings_window ())#show ()) in + let _ = factory3#add_separator () in + let _ = + factory3#add_item "Reload Stylesheets" + ~callback: + (function _ -> + if ProofEngine.get_proof () <> None then + try + refresh_goals notebook ; + refresh_proof output + with + InvokeTactics.RefreshSequentException e -> + HelmLogger.log + (`Error (`T ("An error occurred while refreshing the " ^ + "sequent: " ^ Printexc.to_string e))) ; + (*notebook#remove_all_pages ~skip_switch_page_event:false ;*) + notebook#set_empty_page + | InvokeTactics.RefreshProofException e -> + HelmLogger.log + (`Error (`T ("An error occurred while refreshing the proof: " ^ Printexc.to_string e))) ; + output#unload + ) in + (* accel group *) + let _ = window#add_accel_group accel_group in + (* end of menus *) + let hbox0 = + GPack.hbox + ~packing:(vbox_for_menu#pack ~expand:true ~fill:true ~padding:5) () in + let vbox = + GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in + let scrolled_window0 = + GBin.scrolled_window ~border_width:10 + ~packing:(vbox#pack ~expand:true ~padding:5) () in + let _ = scrolled_window0#add output#coerce in + let frame = + GBin.frame ~label:"Insert Term" + ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in + let scrolled_window1 = + GBin.scrolled_window ~border_width:5 + ~packing:frame#add () in + let inputt = + TermEditor'.term_editor + ~dbd + ~width:400 ~height:100 ~packing:scrolled_window1#add () + ~isnotempty_callback: + (function b -> + check_menu_item#misc#set_sensitive b ; + searchPattern_menu_item#misc#set_sensitive b) in + let vboxl = + GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in + let _ = + vboxl#pack ~expand:true ~fill:true ~padding:5 notebook#notebook#coerce in + let frame = + GBin.frame ~shadow_type:`IN ~packing:(vboxl#pack ~expand:true ~padding:5) () + in + let _ = + new HelmGtkLogger.html_logger + ~width:400 ~height: 100 ~show:true ~packing:frame#add () + in +object method inputt = inputt - method output = (output : GMathView.math_view) - method proofw = (proofw : GMathView.math_view) - method show () = window#show () + method output = (output : TermViewer.proof_viewer) + method scratch_window = scratch_window + method notebook = notebook + method show = window#show + method set_auto_disambiguation set = autoitem#set_active set initializer - button_export_to_postscript#misc#set_sensitive false ; + notebook#set_empty_page ; + (*export_to_postscript_menu_item#misc#set_sensitive false ;*) + check_term := (check_term_in_scratch scratch_window) ; (* signal handlers here *) ignore(output#connect#selection_changed - (function elem -> proofw#unload ; choose_selection output elem)) ; - ignore(proofw#connect#selection_changed (choose_selection proofw)) ; - ignore(closeb#connect#clicked (fun _ -> GMain.Main.quit ())) ; + (function elem -> + choose_selection output elem ; + !focus_and_proveit_set_sensitive true + )) ; + ignore (output#connect#click (show_in_show_window_callback output)) ; let settings_window = new settings_window output scrolled_window0 - button_export_to_postscript (choose_selection output) in - ignore(settingsb#connect#clicked settings_window#show) ; - ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ; - ignore(proveitb#connect#clicked (proveit self)) ; - ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ; - ignore(executeb#connect#clicked (execute self)) ; - ignore(exactb#connect#clicked (exact self)) ; - Logger.log_callback := - (Logger.log_to_html ~print_and_flush:(output_html outputhtml)) -end;; + (*export_to_postscript_menu_item*)() (choose_selection output) in + set_settings_window settings_window ; + ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) +end (* MAIN *) let initialize_everything () = - let module U = Unix in - let output = GMathView.math_view ~width:400 ~height:280 () - and proofw = GMathView.math_view ~width:400 ~height:275 () - and label = GMisc.label ~text:"gTopLevel" () in - let rendering_window = - new rendering_window output proofw label - in - rendering_window#show () ; - GMain.Main.main () + let output = + TermViewer.proof_viewer + ~mml_of_cic_object:ApplyTransformation.mml_of_cic_object + ~width:350 ~height:280 () + in + let notebook = new notebook in + let rendering_window' = new rendering_window output notebook in + rendering_window'#set_auto_disambiguation !auto_disambiguation; + set_rendering_window rendering_window'; + let print_error_as_html prefix msg = + HelmLogger.log (`Error (`T (prefix ^ msg))) + 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 () ; + if restore_environment_on_boot && + Sys.file_exists (Helm_registry.get "gtoplevel.environment_file") + then + restore_environment (); + GtkThread.main () ;; -let _ = - CicCooking.init () ; - initialize_everything () +let main () = + ignore (GtkMain.Main.init ()) ; + initialize_everything () ; + MQIC.close mqi_handle; + Hbugs.quit () ;; + +try +(* CicEnvironment.set_trust (fun _ -> false); *) + Sys.catch_break true; + main (); +with Sys.Break -> () (* exit nicely, invoking at_exit functions *) +