X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=1726725c15370b146e42439def72b6b34c23c655;hb=36f71caeee72cb15185ecbc7644ed1da5c6f8186;hp=ba334ac036908b166c779037acbda0be2bb443b5;hpb=883959e875abadf3336e1a93292bc1fcc8f92696;p=helm.git diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index ba334ac03..1726725c1 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -48,13 +48,21 @@ module MQGT = MQGTypes module MQGU = MQGUtil module MQG = MQueryGenerator -(* GLOBAL CONSTANTS *) -let configuration_file = "triciclo.conf.xml" +(* 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 mqi_debug_fun s = debug_print ~level:2 s -let mqi_flags = [MQIC.Postgres ; MQIC.Stat ; MQIC.Warn ; MQIC.Log] -let mqi_handle = MQIC.init mqi_flags mqi_debug_fun +let mqi_handle = MQIC.init ~log:mqi_debug_fun () let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";; @@ -164,6 +172,7 @@ let check_window uris = lazy (let mmlwidget = TermViewer.sequent_viewer + ~mml_of_cic_sequent:ChosenTransformer.mml_of_cic_sequent ~packing:scrolled_window#add ~width:400 ~height:280 () in let expr = let term = @@ -188,9 +197,9 @@ let check_window uris = exception NoChoice;; -let - interactive_user_uri_choice ~(selection_mode:[`MULTIPLE|`SINGLE]) ?(ok="Ok") - ?(enable_button_for_non_vars=false) ~title ~msg uris +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 @@ -371,7 +380,7 @@ let interactive_interpretation_choice interpretations = GtkThread.main (); match !chosen with None -> raise NoChoice - | Some n -> n + | Some n -> [n] ;; @@ -459,6 +468,7 @@ 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 if CicReduction.are_convertible [] (CicTypeChecker.type_of_aux' [] [] bo) ty @@ -484,8 +494,8 @@ let qed () = (** 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 "triciclo.proof_file_type" in - let proof_file = Helm_registry.get "triciclo.proof_file" 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 ~quiet:true xml (Some proof_file_type) ; HelmLogger.log (`Msg (`T ("Current proof type saved to " ^ proof_file_type))) ; @@ -556,8 +566,9 @@ let refresh_proof (output : TermViewer.proof_viewer) = else Hbugs.notify () ; (*CSC: Wrong: [] is just plainly wrong *) - uri, - (Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, [])) + 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 uri currentproof) with @@ -650,6 +661,7 @@ module InvokeTacticsCallbacks = let decompose_uris_choice_callback = decompose_uris_choice_callback let mk_fresh_name_callback = mk_fresh_name_callback + let mqi_handle = mqi_handle end ;; module InvokeTactics' = InvokeTactics.Make (InvokeTacticsCallbacks);; @@ -676,12 +688,12 @@ let load_unfinished_proof () = None -> raise NoChoice | Some uri0 -> let uri = UriManager.uri_of_string ("cic:" ^ uri0) in - let proof_file_type = Helm_registry.get "triciclo.proof_file_type" in - let proof_file = Helm_registry.get "triciclo.proof_file" 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 (uri, metasenv, bo, ty)) ; + ProofEngine.set_proof (Some (Some uri, metasenv, bo, ty)); refresh_proof output ; set_proof_engine_goal (match metasenv with @@ -1046,7 +1058,7 @@ module DisambiguateCallbacks = 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 = input_or_locate_uri + let input_or_locate_uri ~title ?id = input_or_locate_uri ~title end ;; @@ -1502,7 +1514,7 @@ let new_proof () = let metasenv,expr = !get_metasenv_and_term () in let _ = CicTypeChecker.type_of_aux' metasenv [] expr in ProofEngine.set_proof - (Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr)) ; + (Some (Some (!get_uri ()), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr)); set_proof_engine_goal (Some 1) ; refresh_goals notebook ; refresh_proof output ; @@ -1590,7 +1602,7 @@ let open_ () = | Cic.Variable _ | Cic.InductiveDefinition _ -> raise NotADefinition in - ProofEngine.set_proof (Some (uri, metasenv, bo, ty)) ; + ProofEngine.set_proof (Some (Some uri, metasenv, bo, ty)) ; set_proof_engine_goal None ; refresh_goals notebook ; refresh_proof output ; @@ -2067,7 +2079,7 @@ let searchPattern () = | Some metano -> let uris' = TacticChaser.matchConclusion mqi_handle - ~choose_must () ~status:(proof, metano) + ~choose_must () (proof, metano) in let uri' = user_uri_choice ~title:"Ambiguous input." @@ -2261,6 +2273,7 @@ class scratch_window = ~packing:(vbox#pack ~expand:true ~padding:5) () in let sequent_viewer = TermViewer.sequent_viewer + ~mml_of_cic_sequent:ChosenTransformer.mml_of_cic_sequent ~packing:(scrolled_window#add) ~width:400 ~height:280 () in object(self) val mutable term = Cic.Rel 1 (* dummy value *) @@ -2341,8 +2354,9 @@ object(self) GBin.scrolled_window ~border_width:10 ~packing:(vbox1#pack ~expand:true ~padding:5) () in let proofw = - TermViewer.sequent_viewer ~width:400 ~height:275 - ~packing:(scrolled_window1#add) () in + TermViewer.sequent_viewer + ~mml_of_cic_sequent:ChosenTransformer.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 @@ -2364,6 +2378,9 @@ object(self) 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 = @@ -2495,6 +2512,7 @@ object(self) 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) ; @@ -2517,8 +2535,9 @@ class empty_page = GBin.scrolled_window ~border_width:10 ~packing:(vbox1#pack ~expand:true ~padding:5) () in let proofw = - TermViewer.sequent_viewer ~width:400 ~height:275 - ~packing:(scrolled_window1#add) () in + TermViewer.sequent_viewer + ~mml_of_cic_sequent:ChosenTransformer.mml_of_cic_sequent + ~width:400 ~height:275 ~packing:(scrolled_window1#add) () in object(self) method proofw = (assert false : TermViewer.sequent_viewer) method content = vbox1 @@ -2585,7 +2604,7 @@ end let dump_environment () = try - let oc = open_out (Helm_registry.get "triciclo.environment_file") in + 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!")) ; @@ -2597,7 +2616,7 @@ let dump_environment () = ;; let restore_environment () = try - let ic = open_in (Helm_registry.get "triciclo.environment_file") in + 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!")); @@ -2835,12 +2854,11 @@ end (* MAIN *) let initialize_everything () = - 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; - let output = TermViewer.proof_viewer ~width:350 ~height:280 () in + let output = + TermViewer.proof_viewer + ~mml_of_cic_object:ChosenTransformer.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; @@ -2853,7 +2871,7 @@ let initialize_everything () = (Some (print_error_as_html "XSLT Debug Message: ")); rendering_window'#show () ; if restore_environment_on_boot && - Sys.file_exists (Helm_registry.get "triciclo.environment_file") + Sys.file_exists (Helm_registry.get "gtoplevel.environment_file") then restore_environment (); GtkThread.main ()