From 09151f33b14507e4d20380f3100a6db5f49f3f46 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 30 Apr 2003 13:56:57 +0000 Subject: [PATCH] MQueryInterpreter: interface updated --- helm/gTopLevel/disambiguate.ml | 8 ++--- helm/gTopLevel/disambiguate.mli | 1 + helm/gTopLevel/gTopLevel.ml | 28 +++++++++-------- helm/gTopLevel/termEditor.ml | 4 +-- helm/gTopLevel/termEditor.mli | 1 + helm/gTopLevel/texTermEditor.ml | 3 +- helm/gTopLevel/texTermEditor.mli | 1 + .../ocaml/mquery_generator/mQueryGenerator.ml | 29 +++++------------- .../mquery_generator/mQueryGenerator.mli | 6 ++-- helm/ocaml/tactics/tacticChaser.ml | 4 +-- helm/ocaml/tactics/tacticChaser.mli | 2 +- helm/searchEngine/searchEngine.ml | 30 ++++++++----------- 12 files changed, 51 insertions(+), 66 deletions(-) diff --git a/helm/gTopLevel/disambiguate.ml b/helm/gTopLevel/disambiguate.ml index afa47790a..1e71be5b2 100644 --- a/helm/gTopLevel/disambiguate.ml +++ b/helm/gTopLevel/disambiguate.ml @@ -77,8 +77,8 @@ type domain_and_interpretation = module Make(C:Callbacks) = struct - let locate_one_id id = - let result = MQueryGenerator.locate id in + let locate_one_id mqi_handle id = + let result = MQueryGenerator.locate mqi_handle id in let uris = List.map (function uri,_ -> @@ -121,7 +121,7 @@ module Make(C:Callbacks) = Uris of CicTextualParser0.uri list | Symbols of (CicTextualParser0.interpretation -> Cic.term) list - let disambiguate_input context metasenv dom mk_metasenv_and_expr ~id_to_uris= + let disambiguate_input mqi_handle context metasenv dom mk_metasenv_and_expr ~id_to_uris= let known_ids,resolve_id = id_to_uris in let dom' = let rec filter = @@ -136,7 +136,7 @@ module Make(C:Callbacks) = let list_of_uris = List.map (function - CicTextualParser0.Id id -> Uris (locate_one_id id) + CicTextualParser0.Id id -> Uris (locate_one_id mqi_handle id) | CicTextualParser0.Symbol (descr,choices) -> (* CSC: Implementare la funzione di filtraggio manuale *) (* CSC: corrispondente alla locate_one_id *) diff --git a/helm/gTopLevel/disambiguate.mli b/helm/gTopLevel/disambiguate.mli index 40ad3ec2e..9fdfb8993 100644 --- a/helm/gTopLevel/disambiguate.mli +++ b/helm/gTopLevel/disambiguate.mli @@ -63,6 +63,7 @@ module Make (C : Callbacks) : sig exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput val disambiguate_input : + MQIConn.handle -> Cic.context -> Cic.metasenv -> CicTextualParser0.interpretation_domain_item list -> diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index cfc11e921..4f6cab6af 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -37,16 +37,13 @@ open Printf;; (* DEBUGGING *) -module MQICallbacks = - struct - let log s = prerr_string s - end - -module MQI = MQueryInterpreter.Make(MQICallbacks) +module MQI = MQueryInterpreter +module MQIC = MQIConn (* GLOBAL CONSTANTS *) -let mqi_options = "" (* default MathQL interpreter options *) +let mqi_flags = [] (* default MathQL interpreter options *) +let mqi_handle = MQIC.init mqi_flags prerr_string let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";; @@ -960,7 +957,7 @@ let user_uri_choice ~title ~msg uris = let locate_callback id = let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in - let result = MQueryGenerator.locate id in + let result = MQueryGenerator.locate mqi_handle id in let uris = List.map (function uri,_ -> @@ -1255,6 +1252,7 @@ let new_inductive () = ~packing:(vbox#pack ~expand:true ~padding:0) () in let newinputt = TexTermEditor'.term_editor + mqi_handle ~width:400 ~height:20 ~packing:scrolled_window#add ~share_id_to_uris_with:inputt () ~isnotempty_callback: @@ -1366,6 +1364,7 @@ let new_inductive () = ~packing:(vbox#pack ~expand:true ~padding:0) () in let newinputt = TexTermEditor'.term_editor + mqi_handle ~width:400 ~height:20 ~packing:scrolled_window#add ~share_id_to_uris_with:inputt () ~isnotempty_callback: @@ -1509,7 +1508,9 @@ let new_proof () = ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in (* moved here to have visibility of the ok button *) let newinputt = - TexTermEditor'.term_editor ~width:400 ~height:100 ~packing:scrolled_window#add + TexTermEditor'.term_editor + mqi_handle + ~width:400 ~height:100 ~packing:scrolled_window#add ~share_id_to_uris_with:inputt () ~isnotempty_callback: (function b -> @@ -1924,7 +1925,7 @@ 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 must' only in + let results = MQueryGenerator.searchPattern mqi_handle must' only in show_query_results results with e -> @@ -1991,7 +1992,7 @@ let insertQuery () = None -> () | Some q -> let results = - MQI.execute mqi_options (MQueryUtil.query_of_text (Lexing.from_string q)) + MQI.execute mqi_handle (MQueryUtil.query_of_text (Lexing.from_string q)) in show_query_results results with @@ -2139,6 +2140,7 @@ let searchPattern () = | Some metano -> let uris' = TacticChaser.searchPattern + mqi_handle ~output_html:(output_html outputhtml) ~choose_must () ~status:(proof, metano) in @@ -2780,6 +2782,7 @@ class rendering_window output (notebook : notebook) = ~packing:frame#add () in let inputt = TexTermEditor'.term_editor + mqi_handle ~width:400 ~height:100 ~packing:scrolled_window1#add () ~isnotempty_callback: (function b -> @@ -2848,10 +2851,9 @@ let initialize_everything () = ;; let main () = - if !usedb then ignore (MQI.init mqi_options) ; ignore (GtkMain.Main.init ()) ; initialize_everything () ; - if !usedb then MQI.close mqi_options; + MQIC.close mqi_handle; Hbugs.quit () ;; diff --git a/helm/gTopLevel/termEditor.ml b/helm/gTopLevel/termEditor.ml index 90ce49ae4..48f5adb63 100644 --- a/helm/gTopLevel/termEditor.ml +++ b/helm/gTopLevel/termEditor.ml @@ -55,7 +55,7 @@ module Make(C:Disambiguate.Callbacks) = module Disambiguate' = Disambiguate.Make(C);; - class term_editor_impl ?packing ?width ?height ?isnotempty_callback + class term_editor_impl mqi_handle ?packing ?width ?height ?isnotempty_callback ?share_id_to_uris_with () : term_editor = let id_to_uris = @@ -96,7 +96,7 @@ module Make(C:Disambiguate.Callbacks) = ~context:name_context ~metasenv CicTextualLexer.token lexbuf in let id_to_uris',metasenv,expr = - Disambiguate'.disambiguate_input + Disambiguate'.disambiguate_input mqi_handle context metasenv dom mk_metasenv_and_expr ~id_to_uris:!id_to_uris in id_to_uris := id_to_uris' ; diff --git a/helm/gTopLevel/termEditor.mli b/helm/gTopLevel/termEditor.mli index 44c543276..55746ff1e 100644 --- a/helm/gTopLevel/termEditor.mli +++ b/helm/gTopLevel/termEditor.mli @@ -40,6 +40,7 @@ val empty_id_to_uris : Disambiguate.domain_and_interpretation module Make (C : Disambiguate.Callbacks) : sig val term_editor : + MQIConn.handle -> ?packing:(GObj.widget -> unit) -> ?width:int -> ?height:int -> diff --git a/helm/gTopLevel/texTermEditor.ml b/helm/gTopLevel/texTermEditor.ml index 789b77d81..b8375b3ea 100644 --- a/helm/gTopLevel/texTermEditor.ml +++ b/helm/gTopLevel/texTermEditor.ml @@ -56,6 +56,7 @@ module Make(C:Disambiguate.Callbacks) = module Disambiguate' = Disambiguate.Make(C);; class term_editor_impl + mqi_handle ?packing ?width ?height ?isnotempty_callback ?share_id_to_uris_with () : term_editor = @@ -191,7 +192,7 @@ module Make(C:Disambiguate.Callbacks) = ~context:name_context ~metasenv TexCicTextualLexer.token lexbuf in let id_to_uris',metasenv,expr = - Disambiguate'.disambiguate_input + Disambiguate'.disambiguate_input mqi_handle context metasenv dom mk_metasenv_and_expr ~id_to_uris:!id_to_uris in id_to_uris := id_to_uris' ; diff --git a/helm/gTopLevel/texTermEditor.mli b/helm/gTopLevel/texTermEditor.mli index 44c543276..55746ff1e 100644 --- a/helm/gTopLevel/texTermEditor.mli +++ b/helm/gTopLevel/texTermEditor.mli @@ -40,6 +40,7 @@ val empty_id_to_uris : Disambiguate.domain_and_interpretation module Make (C : Disambiguate.Callbacks) : sig val term_editor : + MQIConn.handle -> ?packing:(GObj.widget -> unit) -> ?width:int -> ?height:int -> diff --git a/helm/ocaml/mquery_generator/mQueryGenerator.ml b/helm/ocaml/mquery_generator/mQueryGenerator.ml index ec9f98d1c..82363c987 100644 --- a/helm/ocaml/mquery_generator/mQueryGenerator.ml +++ b/helm/ocaml/mquery_generator/mQueryGenerator.ml @@ -23,22 +23,7 @@ * http://cs.unibo.it/helm/. *) -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Ferruccio Guidi *) -(* 30/04/2002 *) -(* *) -(* *) -(******************************************************************************) - -module MQICallbacks = - struct - let log s = prerr_string s - end - -module MQI = MQueryInterpreter.Make(MQICallbacks) +module MQI = MQueryInterpreter (* Query issuing functions **************************************************) @@ -75,7 +60,7 @@ let set_confirm_query f = let get_query_info () = ! info -let execute_query query = +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 @@ -98,7 +83,7 @@ let execute_query query = flush och in let execute q = - let r = MQI.execute "" q in + let r = MQI.execute handle q in if ! log_file <> "" then log q r; info := string_of_int ! query_num :: ! info; incr query_num; @@ -108,14 +93,14 @@ let execute_query query = (* Query building functions ************************************************) -let locate s = +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 q + execute_query handle q -let searchPattern must_use can_use = +let searchPattern handle must_use can_use = let module M = MathQL in let in_path s = (s, []) in let assign v p = (in_path v, in_path p) in @@ -556,4 +541,4 @@ let searchPattern 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 (q_let_po opos 1) + execute_query handle (q_let_po opos 1) diff --git a/helm/ocaml/mquery_generator/mQueryGenerator.mli b/helm/ocaml/mquery_generator/mQueryGenerator.mli index b1db11142..37a98adec 100644 --- a/helm/ocaml/mquery_generator/mQueryGenerator.mli +++ b/helm/ocaml/mquery_generator/mQueryGenerator.mli @@ -55,10 +55,10 @@ 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 : MathQL.query -> MathQL.result +val execute_query : MQIConn.handle -> MathQL.query -> MathQL.result -val locate : string -> MathQL.result +val locate : MQIConn.handle -> string -> MathQL.result -val searchPattern : must_restrictions -> only_restrictions -> MathQL.result +val searchPattern : MQIConn.handle -> must_restrictions -> only_restrictions -> MathQL.result val get_query_info : unit -> string list diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml index d09eacc49..47adfeee5 100644 --- a/helm/ocaml/tactics/tacticChaser.ml +++ b/helm/ocaml/tactics/tacticChaser.ml @@ -34,7 +34,7 @@ (******************************************************************************) (* search arguments on which Apply tactic doesn't fail *) -let searchPattern ?(output_html = (fun _ -> ())) ~choose_must () ~status = +let searchPattern mqi_handle ?(output_html = (fun _ -> ())) ~choose_must () ~status = let ((_, metasenv, _, _), metano) = status in let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in let list_of_must,only = MQueryLevels.out_restr metasenv ey ty in @@ -51,7 +51,7 @@ let searchPattern ?(output_html = (fun _ -> ())) ~choose_must () ~status = let rigth_must = List.map torigth_restriction must in let rigth_only = Some (List.map torigth_restriction only) in let result = - MQueryGenerator.searchPattern + MQueryGenerator.searchPattern mqi_handle (rigth_must,[],[]) (rigth_only,None,None) in let uris = List.map diff --git a/helm/ocaml/tactics/tacticChaser.mli b/helm/ocaml/tactics/tacticChaser.mli index b5acbf7cb..f514360ac 100644 --- a/helm/ocaml/tactics/tacticChaser.mli +++ b/helm/ocaml/tactics/tacticChaser.mli @@ -23,7 +23,7 @@ * http://cs.unibo.it/helm/. *) -val searchPattern : +val searchPattern : MQIConn.handle -> ?output_html:(string -> unit) -> (* boolean value: true = in main position *) choose_must:((MQueryGenerator.uri * bool) list list -> diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml index 5e742b243..0e28725fe 100644 --- a/helm/searchEngine/searchEngine.ml +++ b/helm/searchEngine/searchEngine.ml @@ -33,14 +33,7 @@ Http_common.debug := true;; (** accepted HTTP servers for ask_uwobo method forwarding *) let valid_servers = [ "mowgli.cs.unibo.it:58080" ; "mowgli.cs.unibo.it" ; "localhost:58080" ] ;; -module MQICallbacks = - struct - let log s = debug_print s - end - -module MQI = MQueryInterpreter.Make(MQICallbacks) - -let mqi_options = "" (* default MathQL interpreter options *) +let mqi_flags = [] (* default MathQL interpreter options *) open Printf;; @@ -183,19 +176,21 @@ in let callback (req: Http_types.request) outchan = try debug_print (sprintf "Received request: %s" req#path); - if req#path <> "/getpage" then - ignore (MQI.init mqi_options); (match req#path with | "/execute" -> + let mqi_handle = MQIConn.init mqi_flags debug_print in 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 query in + let result = MQueryGenerator.execute_query 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 id in + let result = MQueryGenerator.locate mqi_handle id in + MQIConn.close mqi_handle; Http_daemon.respond ~headers:[contype] ~body:(pp_result result) outchan | "/getpage" -> (* TODO implement "is_permitted" *) @@ -252,6 +247,7 @@ let callback (req: Http_types.request) outchan = | "/searchPattern" | "/matchConclusion" | "/locateInductivePrinciple" -> + let mqi_handle = MQIConn.init mqi_flags debug_print in let term_string = req#param "term" in let lexbuf = Lexing.from_string term_string in let (context, metasenv) = ([], []) in @@ -396,13 +392,13 @@ List.iter (fun u -> prerr_endline ("<" ^ Netencoding.Url.decode u ^ ">")) tail; in let module Disambiguate' = Disambiguate.Make (Chat) in let (id_to_uris', metasenv', term') = - Disambiguate'.disambiguate_input + Disambiguate'.disambiguate_input mqi_handle context metasenv dom mk_metasenv_and_expr id_to_uris in (match metasenv' with | [] -> let must',only = get_constraints term' req#path in - let results = MQueryGenerator.searchPattern must' only in + let results = MQueryGenerator.searchPattern mqi_handle must' only in Http_daemon.send_basic_headers ~code:200 outchan ; Http_daemon.send_CRLF outchan ; iter_file @@ -437,12 +433,10 @@ List.iter (fun u -> prerr_endline ("<" ^ Netencoding.Url.decode u ^ ">")) tail; Http_daemon.respond ~headers:[contype] ~body:"some implicit variables are still unistantiated :-(" - outchan) - + outchan); + MQIConn.close mqi_handle | invalid_request -> Http_daemon.respond_error ~status:(`Client_error `Bad_request) outchan); - if req#path <> "/getpage" then - MQI.close mqi_options; debug_print (sprintf "%s done!" req#path) with | Chat_unfinished -> prerr_endline "Chat unfinished, Try again!" -- 2.39.2