1 (* Copyright (C) 2000, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 (******************************************************************************)
30 (* Ferruccio Guidi <fguidi@cs.unibo.it> *)
34 (******************************************************************************)
36 (* Query issuing functions **************************************************)
46 let confirm_query = ref (fun _ -> true)
53 let set_confirm_query f =
56 let get_query_info () = ! info
58 let execute_query query =
59 let module Util = MQueryUtil in
60 let mode = [Open_wronly; Open_append; Open_creat; Open_text] in
61 let perm = 64 * 6 + 8 * 6 + 4 in
63 let lt = Unix.localtime (Unix.time ()) in
65 string_of_int (lt.Unix.tm_mon + 1) ^ "-" ^
66 string_of_int (lt.Unix.tm_mday + 1) ^ "-" ^
67 string_of_int (lt.Unix.tm_year + 1900) ^ " " ^
68 string_of_int (lt.Unix.tm_hour) ^ ":" ^
69 string_of_int (lt.Unix.tm_min) ^ ":" ^
70 string_of_int (lt.Unix.tm_sec)
73 let och = open_out_gen mode perm ! log_file in
74 if ! query_num = 1 then output_string och (time () ^ nl);
76 "Query: " ^ string_of_int ! query_num ^ nl ^ Util.text_of_query q ^ nl ^
77 "Result:" ^ nl ^ Util.text_of_result r nl in
78 output_string och str;
82 let r = Mqint.execute q in
83 if ! log_file <> "" then log q r;
84 info := string_of_int ! query_num :: ! info;
88 if ! confirm_query query then execute query else raise Discard
90 (* Query building functions ************************************************)
93 let module M = MathQL in
95 M.Ref (M.Property true M.RefineExact ("objectName", []) (M.Const [s]))
99 let searchPattern e c t must_use can_use =
100 let module M = MathQL in
101 let module L = MQueryLevels in
103 "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion" in
105 "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion" in
106 let in_path s = (s, []) in
107 let assign v p = (in_path v, in_path p) in
108 let v_pos = M.Const [mainConclusion; inConclusion] in
115 (false, M.RefineExact, in_path "refObj",
116 M.Ref (M.RefOf (M.RVar "uri0")),
117 [assign "pos" "position"]),
119 (M.Meet (M.VVar "positions", M.Record ("uri", in_path "pos")))
124 let uri_of_entry (r, b) = r in
125 (*let rec restrict level = function
127 | (u, b, v) :: tail ->
128 if v <= level then (u, b, v) :: restrict level tail
129 else restrict level tail
131 let build_select (r, b) =
132 print_endline (">>>>LA URI: "^r);
133 let pos = if b then mainConclusion else inConclusion in
136 M.Relation (false, M.RefineExact, ("backPointer", []),
137 M.Ref (M.Const [r]), [assign "pos" "position"]),
138 M.Ex ["uri"] (M.Sub (M.Const [pos], M.Record ("uri", in_path "pos")))) in
139 let rec build_intersect = function
140 | [] -> M.Pattern (M.Const ["[.]*"])
141 | [hd] -> build_select hd
142 | hd :: tl -> M.Intersect (build_select hd, build_intersect tl)
145 (* let levels = L.levels_of_term e c t in
146 let rest = restrict level levels in
147 info := [string_of_int (List.length rest)];*)
148 let q_in = build_intersect must_use in
149 let q_select = M.Select ("uri0", q_in, q_where) in
150 let universe = M.Const (List.map uri_of_entry can_use) in
151 let q_let_u = M.LetVVar ("universe", universe, q_select) in
152 let q_let_p = M.LetVVar ("positions", v_pos, q_let_u) in
153 print_endline ("### " ^ MQueryUtil.text_of_query q_let_p) ; flush stdout;
154 execute_query q_let_p