X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=eeb6053aa2615b86a75efc5723d7193894896f3b;hb=0c6a5aadb1a7746681a8e26fc0b009f847c10557;hp=e14c9955bcef09b4b4ad6076f322714374347d19;hpb=5aee2f85474686a307f2acda957ffe363a72eff3;p=helm.git diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index e14c9955b..eeb6053aa 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 = "gTopLevel.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,12 @@ 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 *) + (*let old_working = CicUniv.get_working () in + CicUniv.set_working (CicUniv.get_global ());*) + CicUniv.directly_to_env_begin () ; + prerr_endline "-------------> QED"; if CicReduction.are_convertible [] (CicTypeChecker.type_of_aux' [] [] bo) ty @@ -474,7 +489,16 @@ let qed () = 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 + pathname; + (* add the object to the env *) + CicEnvironment.add_type_checked_term uri ( + Cic.Constant ((UriManager.name_of_uri uri),(Some bo),ty,[])); + (* FIXME: the variable list!! *) + (* + CicUniv.qed (); (* now the env has the right constraints *)*) + CicUniv.directly_to_env_end(); + CicUniv.reset_working (); + prerr_endline "-------------> FINE"; end else raise WrongProof @@ -556,8 +580,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 +675,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);; @@ -681,7 +707,7 @@ let load_unfinished_proof () = 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 +1072,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 +1528,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 ; @@ -1581,7 +1607,8 @@ let open_ () = let notebook = (rendering_window ())#notebook in try let uri = input_or_locate_uri ~title:"Open" in - CicTypeChecker.typecheck uri ; + ignore(CicTypeChecker.typecheck uri); + (* TASSI: typecheck mette la uri nell'env... cosa fa la open_ ?*) let metasenv,bo,ty = match CicEnvironment.get_cooked_obj uri with Cic.Constant (_,Some bo,ty,_) -> [],bo,ty @@ -1590,7 +1617,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 +2094,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 +2288,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 +2369,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 +2393,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 +2527,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 +2550,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 @@ -2835,12 +2869,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;