From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 22 Oct 2004 12:55:40 +0000 (+0000)
Subject: - support also DBI handle
X-Git-Tag: V_0_0_10~23
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3a16e3e866b994997972f28b394cc6a69f163210;p=helm.git

- support also DBI handle
- no longer use MQueryMisc
---

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 4c6a6588b..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 _ =
@@ -63,6 +64,7 @@ let _ =
 
 let mqi_debug_fun s = debug_print ~level:2 s
 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 *)
@@ -175,10 +148,7 @@ let check_window uris =
           ~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
@@ -536,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" 
@@ -679,6 +649,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
+  let dbh = dbh
  end
 ;;
 module InvokeTactics' = InvokeTactics.Make (InvokeTacticsCallbacks);;
@@ -942,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
 ;;
 
@@ -1010,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."))) ;
@@ -1193,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 ;
@@ -1223,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:
@@ -1335,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:
@@ -1481,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:
@@ -1514,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 ()
@@ -1668,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 ()
@@ -2095,10 +2054,7 @@ let searchPattern () =
      match !ProofEngine.goal with
       | None -> ()
       | Some metano ->
-         let uris' =
-           TacticChaser.matchConclusion mqi_handle
-            ~choose_must () (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:"
@@ -2827,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 ->