* 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)