From: Ferruccio Guidi Date: Tue, 20 May 2003 14:52:11 +0000 (+0000) Subject: MathQL query generator: new interface X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fc3a73230e9c3a8359944ecbc5546f8f63acac25;p=helm.git MathQL query generator: new interface --- diff --git a/helm/gTopLevel/disambiguate.ml b/helm/gTopLevel/disambiguate.ml index 1e71be5b2..ce41208dd 100644 --- a/helm/gTopLevel/disambiguate.ml +++ b/helm/gTopLevel/disambiguate.ml @@ -33,19 +33,6 @@ (* *) (******************************************************************************) -(* CSC: IMPERATIVE AND NOT VERY CLEAN, TO GET THE LAST ISSUED QUERY *) -(* FG : THIS FUNCTION IS BECOMING A REAL NONSENSE *) -let get_last_query = - let query = ref "" in - let out s = query := ! query ^ s in - MQueryGenerator.set_confirm_query - (function q -> - query := ""; MQueryUtil.text_of_query out q ""; true); - function result -> - out (!query ^ "

Result:

"); MQueryUtil.text_of_result out result "
"; - !query -;; - (** This module provides a functor to disambiguate the input **) (** given a set of user-interface call-backs **) @@ -78,16 +65,17 @@ module Make(C:Callbacks) = struct let locate_one_id mqi_handle id = - let result = MQueryGenerator.locate mqi_handle id in + let query = MQueryGenerator.locate id in + let result = MQueryInterpreter.execute mqi_handle query in let uris = List.map (function uri,_ -> MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri ) result in - let html= - "

Locate Query: 

" ^ get_last_query result ^ "
" - in - C.output_html html ; + C.output_html "

Locate Query: 

";
+     MQueryUtil.text_of_query C.output_html query ""; 
+     C.output_html "
Result:
";
+     MQueryUtil.text_of_result C.output_html result "
";
      let uris' =
       match uris with
          [] ->
diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 3dd457384..6f6b85404 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -37,8 +37,9 @@ open Printf;;
 
 (* DEBUGGING *)
 
-module MQI = MQueryInterpreter
+module MQI  = MQueryInterpreter
 module MQIC = MQIConn
+module MQG  = MQueryGenerator
 
 (* GLOBAL CONSTANTS *)
 
@@ -384,19 +385,6 @@ let interactive_interpretation_choice interpretations =
 
 (* MISC FUNCTIONS *)
 
-(* CSC: IMPERATIVE AND NOT VERY CLEAN, TO GET THE LAST ISSUED QUERY *)
-(* FG : THIS FUNCTION IS BECOMING A REAL NONSENSE                   *)
-let get_last_query = 
- let query = ref "" in
-  let out s = query := ! query ^ s in
-  MQueryGenerator.set_confirm_query
-   (function q -> 
-    query := ""; MQueryUtil.text_of_query out q ""; true);
-  function result ->
-   out (!query ^ " 
Result:
 "); MQueryUtil.text_of_result out result "
";
-   !query
-;;
-
 let
  save_object_to_disk uri annobj ids_to_inner_sorts ids_to_inner_types pathname
 =
@@ -957,16 +945,18 @@ let user_uri_choice ~title ~msg uris =
 
 let locate_callback id =
  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
- let result = MQueryGenerator.locate mqi_handle id in
+ let out = output_html outputhtml in
+ 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
- let html =
-  (" 
Locate Query: 
" ^ get_last_query result ^ "
")
- in
-  output_html outputhtml html ;
+  out "
Locate Query: 
";
+  MQueryUtil.text_of_query out query ""; 
+  out "
Result:
";
+  MQueryUtil.text_of_result out result "
";
   user_uri_choice ~title:"Ambiguous input."
    ~msg:
      ("Ambiguous input \"" ^ id ^
@@ -1930,7 +1920,8 @@ let completeSearchPattern () =
    let metasenv,expr = inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in
    let must = MQueryLevels2.get_constraints expr in
    let must',only = refine_constraints must in
-   let results = MQueryGenerator.searchPattern mqi_handle must' only in 
+   let query = MQG.searchPattern must' only in
+   let results = MQI.execute mqi_handle query in 
     show_query_results results
   with
    e ->
diff --git a/helm/ocaml/mquery_generator/Makefile b/helm/ocaml/mquery_generator/Makefile
index 423c17d37..2e1ed8e7d 100644
--- a/helm/ocaml/mquery_generator/Makefile
+++ b/helm/ocaml/mquery_generator/Makefile
@@ -1,7 +1,5 @@
 PACKAGE = mquery_generator
-REQUIRES = \
-	helm-urimanager postgres unix natile-galax helm-mathql \
-	helm-mathql_interpreter helm-cic helm-cic_proof_checking
+REQUIRES = helm-urimanager helm-mathql helm-cic helm-cic_proof_checking
 PREDICATES =
 
 INTERFACE_FILES = mQueryLevels.mli mQueryLevels2.mli mQueryGenerator.mli
diff --git a/helm/ocaml/mquery_generator/mQueryGenerator.ml b/helm/ocaml/mquery_generator/mQueryGenerator.ml
index 82363c987..378a8e264 100644
--- a/helm/ocaml/mquery_generator/mQueryGenerator.ml
+++ b/helm/ocaml/mquery_generator/mQueryGenerator.ml
@@ -23,8 +23,6 @@
  * http://cs.unibo.it/helm/.
  *)
 
-module MQI = MQueryInterpreter
-
 (* Query issuing functions **************************************************)
 
 type uri = string
@@ -40,68 +38,27 @@ type must_restrictions = (r_obj list * r_rel list * r_sort list)
 type only_restrictions =
  (r_obj list option * r_rel list option * r_sort list option)
 
-exception Discard  
-
-let nl = " 
\n"
-
-let query_num = ref 1
-
-let log_file = ref ""
-
-let confirm_query = ref (fun _ -> true)
-
-let info = ref []
-
-let set_log_file f = 
-   log_file := f
+let builtin s = 
+   let ns = "h:" in
+   match s with
+      | "MH"   -> ns ^ "MainHypothesis"
+      | "IH"   -> ns ^ "InHypothesis"
+      | "MC"   -> ns ^ "MainConclusion"
+      | "IC"   -> ns ^ "InConclusion"
+      | "IB"   -> ns ^ "InBody"
+      | "SET"  -> ns ^ "Set"
+      | "PROP" -> ns ^ "Prop"
+      | "TYPE" -> ns ^ "Type"
+      | _      -> raise (Failure "MQueryGenerator.builtin")
 
-let set_confirm_query f =
-   confirm_query := f
-
-let get_query_info () = ! info
-
-let execute_query handle query =
-   let module Util = MQueryUtil in
-   let mode = [Open_wronly; Open_append; Open_creat; Open_text] in
-   let perm = 64 * 6 + 8 * 6 + 4 in
-   let time () =
-      let lt = Unix.localtime (Unix.time ()) in
-      "NEW LOG: " ^
-      string_of_int (lt.Unix.tm_mon + 1) ^ "-" ^
-      string_of_int (lt.Unix.tm_mday + 1) ^ "-" ^
-      string_of_int (lt.Unix.tm_year + 1900) ^ " " ^
-      string_of_int (lt.Unix.tm_hour) ^ ":" ^
-      string_of_int (lt.Unix.tm_min) ^ ":" ^
-      string_of_int (lt.Unix.tm_sec) 
-   in
-   let log q r = 
-      let och = open_out_gen mode perm ! log_file in
-      let out = output_string och in
-      if ! query_num = 1 then out (time () ^ nl);
-      out ("Query: " ^ string_of_int ! query_num ^ nl); Util.text_of_query out q nl; 
-      out ("Result:" ^ nl); Util.text_of_result out r nl; 
-      flush och 
-   in
-   let execute q =
-      let r = MQI.execute handle q in    
-      if ! log_file <> "" then log q r; 
-      info := string_of_int ! query_num :: ! info;
-      incr query_num;
-      r
-   in 
-   if ! confirm_query query then execute query else raise Discard
-                          
 (* Query building functions  ************************************************)   
 
-let locate handle s =
-   let module M = MathQL in
-   let q =
-    M.Ref (M.Property true M.RefineExact ("objectName", []) (M.Const [s]))
-   in
-    execute_query handle q
+module M = MathQL
+
+let locate s =
+   M.Ref (M.Property true M.RefineExact ("objectName", []) (M.Const [s]))
 
-let searchPattern handle must_use can_use =    
-   let module M = MathQL in
+let searchPattern must_use can_use =    
    let in_path s = (s, []) in
    let assign v p = (in_path v, in_path p) in 
   
@@ -541,4 +498,4 @@ let searchPattern handle must_use can_use =
    (*let q_let_po = M.LetVVar ("obj_positions", M.Const opos, q_let_pr) in*)
 
 print_endline "### ";  MQueryUtil.text_of_query print_string (q_let_po opos 1) "\n"; flush stdout;
-   execute_query handle (q_let_po opos 1)
+   (q_let_po opos 1)
diff --git a/helm/ocaml/mquery_generator/mQueryGenerator.mli b/helm/ocaml/mquery_generator/mQueryGenerator.mli
index 37a98adec..e1ad25caf 100644
--- a/helm/ocaml/mquery_generator/mQueryGenerator.mli
+++ b/helm/ocaml/mquery_generator/mQueryGenerator.mli
@@ -23,18 +23,6 @@
  * http://cs.unibo.it/helm/.
  *)
 
-(******************************************************************************)
-(*                                                                            *)
-(*                               PROJECT HELM                                 *)
-(*                                                                            *)
-(*                     Ferruccio Guidi                    *)
-(*                                 30/04/2002                                 *)
-(*                                                                            *)
-(*                                                                            *)
-(******************************************************************************)
-
-exception Discard  
-
 type uri = string
 type position = string
 type depth = int option
@@ -48,17 +36,8 @@ type must_restrictions = (r_obj list * r_rel list * r_sort list)
 type only_restrictions =
  (r_obj list option * r_rel list option * r_sort list option)
 
+val locate        : string -> MathQL.query
 
+val searchPattern : must_restrictions -> only_restrictions -> MathQL.query
 
-val set_log_file      : string -> unit
-
-(* the callback function must return false iff the query must be skipped *)
-val set_confirm_query : (MathQL.query -> bool) -> unit
-
-val execute_query     : MQIConn.handle -> MathQL.query -> MathQL.result
-
-val locate            : MQIConn.handle -> string -> MathQL.result
-
-val searchPattern     : MQIConn.handle -> must_restrictions -> only_restrictions -> MathQL.result
-
-val get_query_info    : unit -> string list
+val builtin       : MathQL.vvar -> string
diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml
index 47adfeee5..f38258d1e 100644
--- a/helm/ocaml/tactics/tacticChaser.ml
+++ b/helm/ocaml/tactics/tacticChaser.ml
@@ -51,8 +51,9 @@ let searchPattern mqi_handle ?(output_html = (fun _ -> ())) ~choose_must () ~sta
   let rigth_must = List.map torigth_restriction must in
   let rigth_only = Some (List.map torigth_restriction only) in
   let result =
-	 MQueryGenerator.searchPattern mqi_handle
-		(rigth_must,[],[]) (rigth_only,None,None) in 
+	 MQueryInterpreter.execute mqi_handle 
+	    (MQueryGenerator.searchPattern
+		(rigth_must,[],[]) (rigth_only,None,None)) in 
 	let uris =
 	 List.map
 		(function uri,_ ->
diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml
index b7c241371..ecedf5ab7 100644
--- a/helm/searchEngine/searchEngine.ml
+++ b/helm/searchEngine/searchEngine.ml
@@ -303,14 +303,15 @@ let callback (req: Http_types.request) outchan =
         let query_string = req#param "query" in
         let lexbuf = Lexing.from_string query_string in
         let query = MQueryUtil.query_of_text lexbuf in
-        let result = MQueryGenerator.execute_query mqi_handle query in
+        let result = MQueryInterpreter.execute mqi_handle query in
         let result_string = pp_result result in
 	      MQIConn.close mqi_handle;
         Http_daemon.respond ~body:result_string ~headers:[contype] outchan
     | "/locate" ->
         let mqi_handle = MQIConn.init mqi_flags debug_print in
         let id = req#param "id" in
-        let result = MQueryGenerator.locate mqi_handle id in
+        let query = MQueryGenerator.locate id in
+	let result = MQueryInterpreter.execute mqi_handle query in
 	      MQIConn.close mqi_handle;
         Http_daemon.respond ~headers:[contype] ~body:(pp_result result) outchan
     | "/getpage" ->
@@ -591,8 +592,8 @@ List.iter (fun u -> prerr_endline ("<" ^ Netencoding.Url.decode u ^ ">")) tail;
                   constraints_choice_TPL;
                   raise Chat_unfinished)
             in
-            let results =
-             MQueryGenerator.searchPattern mqi_handle must'' only' in 
+            let query = MQueryGenerator.searchPattern must'' only' in
+	    let results = MQueryInterpreter.execute mqi_handle query in 
             Http_daemon.send_basic_headers ~code:200 outchan ;
             Http_daemon.send_CRLF outchan ;
             iter_file