X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=82317959a12b576739672dcb797d5ee0083dab83;hb=a7ab0ef67114c3152920f03ae1d7bfaaf1fae290;hp=5df73dc1cacbc71b3fb61443838829c32582888c;hpb=29442b4d21cf07992ad4e5c981085dada1f90fe4;p=helm.git diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 5df73dc1c..82317959a 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -48,6 +48,7 @@ module MQGT = MQGTypes module MQGU = MQGUtil module MQG = MQueryGenerator +module DB = Dbi_mysql (* first of all let's initialize the Helm_registry *) let _ = @@ -62,7 +63,8 @@ let _ = (* GLOBAL CONSTANTS *) let mqi_debug_fun s = debug_print ~level:2 s -let mqi_handle = MQIC.init ~log:mqi_debug_fun () +let mqi_handle = MQIC.init_if_connected ~log:mqi_debug_fun () +let dbh = new DB.connection ~host:"mowgli.cs.unibo.it" ~user:"helm" "mowgli" let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";; @@ -120,35 +122,6 @@ let argspec = in Arg.parse argspec ignore "" -(* MISC FUNCTIONS *) - -let term_of_cic_textual_parser_uri uri = - let module C = Cic in - let module CTP = CicTextualParser0 in - match uri with - CTP.ConUri uri -> C.Const (uri,[]) - | CTP.VarUri uri -> C.Var (uri,[]) - | CTP.IndTyUri (uri,tyno) -> C.MutInd (uri,tyno,[]) - | CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[]) -;; - -let string_of_cic_textual_parser_uri uri = - let module C = Cic in - let module CTP = CicTextualParser0 in - let uri' = - match uri with - CTP.ConUri uri -> UriManager.string_of_uri uri - | CTP.VarUri uri -> UriManager.string_of_uri uri - | CTP.IndTyUri (uri,tyno) -> - UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) - | CTP.IndConUri (uri,tyno,consno) -> - UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) ^ "/" ^ - string_of_int consno - in - (* 4 = String.length "cic:" *) - String.sub uri' 4 (String.length uri' - 4) -;; - (* UTILITY FUNCTIONS TO DISAMBIGUATE AN URI *) (* Check window *) @@ -172,12 +145,10 @@ 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 = - term_of_cic_textual_parser_uri - (MQueryMisc.cic_textual_parser_uri_of_string uri) - in + let term = CicUtil.term_of_uri uri in (Cic.Cast (term, CicTypeChecker.type_of_aux' [] [] term)) in try @@ -196,9 +167,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 @@ -467,6 +438,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 @@ -482,7 +459,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 @@ -520,9 +506,9 @@ let decompose_uris_choice_callback uris = let module U = UriManager in List.map (function uri -> - match MQueryMisc.cic_textual_parser_uri_of_string uri with - CicTextualParser0.IndTyUri (uri,typeno) -> (uri,typeno,[]) - | _ -> assert false) + 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" @@ -564,8 +550,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 @@ -619,7 +606,10 @@ let refresh_goals ?(empty_notebook=true) notebook = begin notebook#set_current_page ~may_skip_switch_page_event:true metano ; - notebook#proofw#load_sequent metasenv currentsequent +prerr_endline "CIAO CIAO" ; +prerr_endline ("SEQUENTE CORRENTE: " ^ SequentPp.TextualPp.print_sequent currentsequent) ; + notebook#proofw#load_sequent metasenv currentsequent ; +prerr_endline "pASSO CIAO CIAO" end with e -> @@ -658,6 +648,8 @@ 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 + let dbh = dbh end ;; module InvokeTactics' = InvokeTactics.Make (InvokeTacticsCallbacks);; @@ -689,7 +681,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 @@ -874,7 +866,7 @@ let in window#set_title (UriManager.string_of_uri uri) ; window#misc#hide () ; window#show () ; - mmlwidget#load_doc mml ; + mmlwidget#load_root mml#get_documentElement ; with e -> HelmLogger.log @@ -884,7 +876,7 @@ let let obj = CicEnvironment.get_obj uri in show_in_show_window_obj uri obj in - let show_in_show_window_callback mmlwidget (n : Gdome.element option) _ = + let show_in_show_window_callback mmlwidget ((n : Gdome.element option),_,_,_) = match n with None -> () | Some n' -> @@ -921,21 +913,12 @@ let user_uri_choice ~title ~msg uris = ;; let locate_callback id = - let query = MQG.locate id in - let result = MQI.execute mqi_handle query in - let uris = - List.map - (function uri,_ -> - MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri) - result in - HelmLogger.log (`Msg (`T "Locate Query:")) ; - MQueryUtil.text_of_query (fun m -> HelmLogger.log (`Msg (`T m))) "" query; + let uris = MetadataQuery.locate ~dbh id in + HelmLogger.log (`Msg (`T ("Locate Query: " ^ id))) ; HelmLogger.log (`Msg (`T "Result:")) ; - MQueryUtil.text_of_result (fun m -> HelmLogger.log (`Msg (`T m))) "" result; + List.iter (fun uri -> HelmLogger.log (`Msg (`T uri))) uris; user_uri_choice ~title:"Ambiguous input." - ~msg: - ("Ambiguous input \"" ^ id ^ - "\". Please, choose one interpetation:") + ~msg:(sprintf "Ambiguous input \"%s\". Please, choose one interpetation:" id) uris ;; @@ -989,7 +972,7 @@ let input_or_locate_uri ~title = HelmLogger.log (`Msg (`T "OK")) ; true with - Http_getter_types.Unresolvable_URI _ -> + Http_getter_types.Key_not_found _ -> HelmLogger.log (`Error (`T ("URI " ^ uri ^ " does not correspond to any object."))) ; @@ -1054,7 +1037,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 ;; @@ -1172,7 +1155,7 @@ let new_inductive () = try ignore (Http_getter.resolve' uri) ; raise UriAlreadyInUse - with Http_getter_types.Unresolvable_URI _ -> + with Http_getter_types.Key_not_found _ -> get_uri := (function () -> uri) ; get_names := (function () -> names) ; inductive := inductiveb#active ; @@ -1202,7 +1185,7 @@ let new_inductive () = ~packing:(vbox#pack ~expand:true ~padding:0) () in let newinputt = TermEditor'.term_editor - mqi_handle + ~dbh ~width:400 ~height:20 ~packing:scrolled_window#add ~share_environment_with:inputt () ~isnotempty_callback: @@ -1314,7 +1297,7 @@ let new_inductive () = ~packing:(vbox#pack ~expand:true ~padding:0) () in let newinputt = TermEditor'.term_editor - mqi_handle + ~dbh ~width:400 ~height:20 ~packing:scrolled_window#add ~share_environment_with:inputt () ~isnotempty_callback: @@ -1460,7 +1443,7 @@ let new_proof () = (* moved here to have visibility of the ok button *) let newinputt = TermEditor'.term_editor - mqi_handle + ~dbh ~width:400 ~height:100 ~packing:scrolled_window#add ~share_environment_with:inputt () ~isnotempty_callback: @@ -1493,7 +1476,7 @@ let new_proof () = try ignore (Http_getter.resolve' uri) ; raise UriAlreadyInUse - with Http_getter_types.Unresolvable_URI _ -> + with Http_getter_types.Key_not_found _ -> get_metasenv_and_term := (function () -> metasenv,parsed) ; get_uri := (function () -> uri) ; window#destroy () @@ -1510,7 +1493,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 ; @@ -1589,7 +1572,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 @@ -1598,7 +1582,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 ; @@ -1646,16 +1630,13 @@ let show_query_results results = (clist#connect#select_row (fun ~row ~column ~event -> let (uristr,_) = List.nth results row in - match - MQueryMisc.cic_textual_parser_uri_of_string - (MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' - uristr) - with - CicTextualParser0.ConUri uri - | CicTextualParser0.VarUri uri - | CicTextualParser0.IndTyUri (uri,_) - | CicTextualParser0.IndConUri (uri,_,_) -> + 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 () @@ -2073,10 +2054,7 @@ let searchPattern () = match !ProofEngine.goal with | None -> () | Some metano -> - let uris' = - TacticChaser.matchConclusion mqi_handle - ~choose_must () ~status:(proof, metano) - in + let uris' = List.map fst (MetadataQuery.hint ~dbh (proof, metano)) in let uri' = user_uri_choice ~title:"Ambiguous input." ~msg: "Many lemmas can be successfully applied. Please, choose one:" @@ -2269,6 +2247,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 *) @@ -2349,8 +2328,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 @@ -2372,6 +2352,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 = @@ -2503,6 +2486,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) ; @@ -2525,8 +2509,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 @@ -2798,7 +2783,7 @@ class rendering_window output (notebook : notebook) = ~packing:frame#add () in let inputt = TermEditor'.term_editor - mqi_handle + ~dbh ~width:400 ~height:100 ~packing:scrolled_window1#add () ~isnotempty_callback: (function b -> @@ -2843,9 +2828,16 @@ end (* MAIN *) let initialize_everything () = - let output = TermViewer.proof_viewer ~width:350 ~height:280 () in +prerr_endline "STO PER CREARE LA PROOF WINDOW" ; + let output = + TermViewer.proof_viewer + ~mml_of_cic_object:ChosenTransformer.mml_of_cic_object + ~width:350 ~height:280 () + in +prerr_endline "CREATA" ; let notebook = new notebook in let rendering_window' = new rendering_window output notebook in +prerr_endline "OK" ; rendering_window'#set_auto_disambiguation !auto_disambiguation; set_rendering_window rendering_window'; let print_error_as_html prefix msg = @@ -2863,6 +2855,7 @@ let initialize_everything () = ;; let main () = +prerr_endline "CIAO" ; ignore (GtkMain.Main.init ()) ; initialize_everything () ; MQIC.close mqi_handle;