(* *)
(******************************************************************************)
-(* 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 ^ " <h1>Result:</h1> "); MQueryUtil.text_of_result out result "<br>";
- !query
-;;
-
(** This module provides a functor to disambiguate the input **)
(** given a set of user-interface call-backs **)
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=
- " <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>"
- in
- C.output_html html ;
+ C.output_html "<h1>Locate Query: </h1><pre>";
+ MQueryUtil.text_of_query C.output_html query "";
+ C.output_html "<h1>Result:</h1>";
+ MQueryUtil.text_of_result C.output_html result "<br>";
let uris' =
match uris with
[] ->
(* DEBUGGING *)
-module MQI = MQueryInterpreter
+module MQI = MQueryInterpreter
module MQIC = MQIConn
+module MQG = MQueryGenerator
(* GLOBAL CONSTANTS *)
(* 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 ^ " <h1>Result:</h1> "); MQueryUtil.text_of_result out result "<br>";
- !query
-;;
-
let
save_object_to_disk uri annobj ids_to_inner_sorts ids_to_inner_types pathname
=
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 =
- (" <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>")
- in
- output_html outputhtml html ;
+ out "<h1>Locate Query: </h1><pre>";
+ MQueryUtil.text_of_query out query "";
+ out "<h1>Result:</h1>";
+ MQueryUtil.text_of_result out result "<br>";
user_uri_choice ~title:"Ambiguous input."
~msg:
("Ambiguous input \"" ^ id ^
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 ->
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
* http://cs.unibo.it/helm/.
*)
-module MQI = MQueryInterpreter
-
(* Query issuing functions **************************************************)
type uri = string
type only_restrictions =
(r_obj list option * r_rel list option * r_sort list option)
-exception Discard
-
-let nl = " <p>\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
(*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)
* http://cs.unibo.it/helm/.
*)
-(******************************************************************************)
-(* *)
-(* PROJECT HELM *)
-(* *)
-(* Ferruccio Guidi <fguidi@cs.unibo.it> *)
-(* 30/04/2002 *)
-(* *)
-(* *)
-(******************************************************************************)
-
-exception Discard
-
type uri = string
type position = string
type depth = int option
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
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,_ ->
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" ->
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
projects / helm.git / commitdiff