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 (******************************************************************************)
38 let log s = prerr_string s
41 module MQI = MQueryInterpreter.Make(MQICallbacks)
43 (* Query issuing functions **************************************************)
46 type position = string
47 type depth = int option
50 type r_obj = (uri * position * depth)
51 type r_rel = (position* depth)
52 type r_sort = (position* depth * sort)
54 type must_restrictions = (r_obj list * r_rel list * r_sort list)
55 type only_restrictions =
56 (r_obj list option * r_rel list option * r_sort list option)
66 let confirm_query = ref (fun _ -> true)
73 let set_confirm_query f =
76 let get_query_info () = ! info
78 let execute_query query =
79 let module Util = MQueryUtil in
80 let mode = [Open_wronly; Open_append; Open_creat; Open_text] in
81 let perm = 64 * 6 + 8 * 6 + 4 in
83 let lt = Unix.localtime (Unix.time ()) in
85 string_of_int (lt.Unix.tm_mon + 1) ^ "-" ^
86 string_of_int (lt.Unix.tm_mday + 1) ^ "-" ^
87 string_of_int (lt.Unix.tm_year + 1900) ^ " " ^
88 string_of_int (lt.Unix.tm_hour) ^ ":" ^
89 string_of_int (lt.Unix.tm_min) ^ ":" ^
90 string_of_int (lt.Unix.tm_sec)
93 let och = open_out_gen mode perm ! log_file in
94 let out = output_string och in
95 if ! query_num = 1 then out (time () ^ nl);
96 out ("Query: " ^ string_of_int ! query_num ^ nl); Util.text_of_query out q nl;
97 out ("Result:" ^ nl); Util.text_of_result out r nl;
101 let r = MQI.execute "" q in
102 if ! log_file <> "" then log q r;
103 info := string_of_int ! query_num :: ! info;
107 if ! confirm_query query then execute query else raise Discard
109 (* Query building functions ************************************************)
112 let module M = MathQL in
114 M.Ref (M.Property true M.RefineExact ("objectName", []) (M.Const [s]))
118 let searchPattern must_use can_use =
119 let module M = MathQL in
120 let in_path s = (s, []) in
121 let assign v p = (in_path v, in_path p) in
123 (* can restrictions *)
125 let (cr_o,cr_r,cr_s) = can_use in
127 let uri_of_entry (r, p, d) = r in
132 | Some cr_o -> List.map uri_of_entry cr_o
135 let tfst (a,b,c) = a in
136 let tsnd (a,b,c) = b in
137 let trd (a,b,c) = c in
139 let to_int_list l d =
148 | Some cr_o -> (List.map tsnd cr_o) in
153 | Some cr_o -> List.map trd cr_o
154 (* let odep_option_list = List.map trd cr_o in
155 let lo_dep_int = List.fold_left to_int_list [] odep_option_list in
156 List.map string_of_int lo_dep_int*)
158 print_string "#### LUNGHEZZA ODEP: "; print_int (List.length odep); flush stdout;
163 | Some cr_r -> (List.map fst cr_r) in
168 | Some cr_r -> List.map snd cr_r
169 (* let rdep_option_list = List.map snd cr_r in
170 let lr_dep_int = List.fold_left to_int_list [] rdep_option_list in
171 List.map string_of_int lr_dep_int *)
178 | Some cr_s -> (List.map tfst cr_s) in
184 | Some cr_s -> List.map tsnd cr_s
185 (* let sdep_option_list = List.map tsnd cr_s in
186 let ls_dep_int = List.fold_left to_int_list [] sdep_option_list in
187 List.map string_of_int ls_dep_int*)
194 | Some cr_s -> List.map trd cr_s in
196 (* let q_where_obj = function
203 M.Relation (false, M.RefineExact, in_path "refObj", M.Ref (M.RefOf (M.RVar "uri0")), [assign "pos" "position"]),
205 (M.Meet (M.VVar "obj_positions", M.Record ("uri", in_path "pos"))))),
213 (false, M.RefineExact, in_path "refObj",
214 M.Ref (M.RefOf (M.RVar "uri0")),
215 [assign "p" "position"; assign "d" "depth"]
219 ((M.Meet(M.VVar "obj_positions",M.Record("uri",in_path "p"))),
220 (M.Meet(M.VVar "obj_depths", M.Record("uri",in_path "d")))))
231 let q_where_obj n = function
233 let rec q_ex n = function
236 M.Meet (M.VVar ("obj_position" ^ string_of_int n), M.Record ("uri", in_path "p"))
239 print_string "@@@@@ IN-WHERE-OBJ"; flush stdout;
242 (M.Meet(M.VVar ("obj_position" ^ string_of_int n),M.Record("uri",in_path "p")),
243 M.Meet(M.VVar ("obj_depth" ^ string_of_int n), M.Record("uri",in_path "d")))
246 (M.Meet (M.VVar ("obj_position" ^ string_of_int n), M.Record ("uri", in_path "p")),
249 print_string "@@@@@ IN-WHERE-OBJ"; flush stdout;
253 ((M.Meet(M.VVar ("obj_position" ^ string_of_int n),M.Record("uri",in_path "p"))),
254 (M.Meet(M.VVar ("obj_depth" ^ string_of_int n), M.Record("uri",in_path "d"))))),
262 (false, M.RefineExact, in_path "refObj",
263 M.Ref (M.RefOf (M.RVar "uri0")),
264 [assign "p" "position"; assign "d" "depth"]
275 let rec q_where_rel n cr_r= (*function*)
280 (false, M.RefineExact, ("refRel", ["position"]),
281 M.RefOf(M.RVar "uri0")),
282 M.VVar ("rel_position" ^ string_of_int n))
286 | Some [(p,None)] -> q0
292 (false, M.RefineExact, ("refRel", ["depth"]),
293 M.RefOf(M.RVar "uri0")),
294 M.VVar ("rel_depth" ^ string_of_int n)))
295 | Some ((p,None)::tl) ->
298 q_where_rel (n+1) (Some tl))
299 | Some ((p,d)::tl) ->
305 (false, M.RefineExact, ("refRel", ["depth"]),
306 M.RefOf(M.RVar "uri0")),
307 M.VVar ("rel_depth" ^ string_of_int n))),
308 q_where_rel (n+1) (Some tl))
312 let rec q_where_sort n cr_s = (*function *)
318 (false, M.RefineExact, ("refSort", ["position"]),
319 M.RefOf(M.RVar "uri0")
321 M.VVar ("sort_position" ^ string_of_int n)),
324 (false, M.RefineExact, ("refSort", ["sort"]),
325 M.RefOf(M.RVar "uri0")),
326 M.VVar ("sort" ^ string_of_int n)))
330 | Some [(p,None,s)] -> q0
337 (false, M.RefineExact, ("refSort", ["depth"]),
338 M.RefOf(M.RVar "uri0")),
339 M.VVar ("sort_depth" ^ string_of_int n)))
341 | Some ((p,None,s)::tl) ->
344 q_where_sort (n+1) (Some tl))
346 | Some((p,d,s)::tl) ->
352 (false, M.RefineExact, ("refSort", ["depth"]),
353 M.RefOf(M.RVar "uri0")),
354 M.VVar ("sort_depth" ^ string_of_int n))),
355 q_where_sort (n+1) (Some tl))
363 let (cr_o,cr_r,cr_s) = cr in
364 M.And(M.And(q_where_obj 1 cr_o, (q_where_rel 1 cr_r)), (q_where_sort 1 cr_s))
368 (* must restrictions *)
370 let build_select_obj (r, pos, dep) =
374 M.Relation (false, M.RefineExact, ("backPointer", []),
375 M.Ref (M.Const [r]), [assign "p" "position"]),
377 ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p")))))
378 | Some dep -> let string_dep = string_of_int dep in
381 M.Relation (false, M.RefineExact, ("backPointer", []),
382 M.Ref (M.Const [r]), [assign "p" "position";assign "d" "depth"]),
385 ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))),
386 (M.Sub (M.Const [string_dep], M.Record ("uri", in_path "d"))))))
389 let build_select_rel (pos, dep) =
393 M.Relation (true, M.RefineExact, ("refRel", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth"]),
395 (M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))))
396 | Some dep -> let string_dep = string_of_int dep in
399 M.Relation (true, M.RefineExact, ("refRel", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth"]),
402 ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))),
403 (M.Sub (M.Const [string_dep], M.Record ("uri", in_path "d"))))))
406 let build_select_sort (pos, dep, sor) =
410 M.Relation (true, M.RefineExact, ("refSort", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth";assign "s" "sort"]),
413 ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))),
414 (M.Sub (M.Const [sor], M.Record ("uri", in_path "s"))))))
416 | Some dep -> let string_dep = string_of_int dep in
419 M.Relation (true, M.RefineExact, ("refSort", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth";assign "s" "sort"]),
423 ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))),
424 (M.Sub (M.Const [string_dep], M.Record ("uri", in_path "d"))))),
425 (M.Sub (M.Const [sor], M.Record ("uri", in_path "s"))))))
428 let rec build_intersect_obj = function
429 [] -> M.Pattern (M.Const ["[.]*"])
430 | [hd] -> build_select_obj hd
431 | hd :: tl -> M.Intersect (build_select_obj hd, build_intersect_obj tl)
434 let rec build_intersect_rel = function
435 [] -> M.Ref(M.Const [])
436 | [hd] -> build_select_rel hd
437 | hd :: tl -> M.Intersect (build_select_rel hd, build_intersect_rel tl)
440 let rec build_intersect_sort = function
441 [] -> M.Ref(M.Const [])
442 | [hd] -> build_select_sort hd
443 | hd :: tl -> M.Intersect (build_select_sort hd, build_intersect_sort tl)
446 let build_intersect = function
447 (* let tostring_sort (a,b,c) =
448 let b1 = string_of_int b in
451 let tostring_rel (a,b) =
452 let b1 = string_of_int b in
456 (* let (l1,l2,l3) = must in
457 match (l1,l2,l3) with *)
458 l1,[],[] -> build_intersect_obj l1
459 | [],l2,[] -> (*let lrel = List.map tostring_rel l2 in*)
460 build_intersect_rel l2
461 | [],[],l3 ->(* let lsort = List.map tostring_sort l3 in*)
462 build_intersect_sort l3
463 | l1,l2,[] -> (*let lrel = List.map tostring_rel l2 in*)
464 M.Intersect (build_intersect_obj l1, build_intersect_rel l2)
465 | l1,[],l3 ->(* let lsort = List.map tostring_sort l3 in *)
466 M.Intersect (build_intersect_obj l1, build_intersect_sort l3)
467 | [],l2,l3 ->(* let lrel = List.map tostring_rel l2 in
468 let lsort = List.map tostring_sort l3 in*)
469 M.Intersect (build_intersect_rel l2, build_intersect_sort l3)
470 | l1,l2,l3 ->(* let lrel = List.map tostring_rel l2 in
471 let lsort = List.map tostring_sort l3 in *)
472 M.Intersect (M.Intersect (build_intersect_obj l1, build_intersect_rel l2), build_intersect_sort l3)
475 let q_in = build_intersect must_use in
476 let q_select = M.Select ("uri0", q_in, q_where can_use) in
478 (* variables for can restrictions *)
480 let q_let_u = M.LetVVar ("universe", M.Const universe, q_select) in
482 let rec q_let_s sor n =
485 | [s] -> M.LetVVar ("sort" ^ (string_of_int n), M.Const [s], q_let_u)
486 | s::tl -> M.LetVVar ("sort" ^ (string_of_int n), M.Const [s], q_let_s tl (n+1))
489 (* let q_let_s = M.LetVVar ("sorts", M.Const sor, q_let_u) in *)
491 let rec q_let_ds sdep n =
494 | [None] -> q_let_s sor 1
495 | (None)::tl -> q_let_ds tl (n+1)
496 | [Some d] -> M.LetVVar ("sort_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_s sor 1)
497 | (Some d)::tl -> M.LetVVar ("sort_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_ds tl (n+1))
500 (* let q_let_ds = M.LetVVar ("sort_depths", M.Const sdep, q_let_s) in *)
502 let rec q_let_dr rdep n =
505 | [None] -> q_let_ds sdep 1
506 | (None)::tl -> q_let_dr tl (n+1)
507 | [Some d] -> M.LetVVar ("rel_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_ds sdep 1)
508 | (Some d)::tl -> M.LetVVar ("rel_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_dr tl (n+1))
512 (*let q_let_dr = M.LetVVar ("rel_depths", M.Const rdep, q_let_ds) in*)
514 let rec q_let_do odep n =
517 | [None] -> q_let_dr rdep 1
518 | (None)::tl -> q_let_do tl (n+1)
519 | [Some d] -> M.LetVVar ("obj_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_dr rdep 1)
520 | (Some d)::tl -> M.LetVVar ("obj_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_do tl (n+1))
524 (* let q_let_do = M.LetVVar ("obj_depths", M.Const odep, q_let_dr) in *)
527 let rec q_let_ps spos n =
529 [] -> q_let_do odep 1
530 | [p] -> M.LetVVar ("sort_position" ^ (string_of_int n), M.Const [p], q_let_do odep 1)
531 | p::tl -> M.LetVVar ("sort_position" ^ (string_of_int n), M.Const [p], q_let_ps tl (n+1))
535 (* let q_let_ps = M.LetVVar ("sort_positions", M.Const spos, q_let_do) in *)
538 let rec q_let_pr rpos n =
540 [] -> q_let_ps spos 1
541 | [p] -> M.LetVVar ("rel_position" ^ (string_of_int n), M.Const [p], q_let_ps spos 1)
542 | p::tl -> M.LetVVar ("rel_position" ^ (string_of_int n), M.Const [p], q_let_pr tl (n+1))
547 (* let q_let_pr = M.LetVVar ("rel_positions", M.Const rpos, q_let_ps) in *)
549 let rec q_let_po opos n =
551 [] -> q_let_pr rpos 1
552 | [p] -> M.LetVVar ("obj_position" ^ (string_of_int n), M.Const [p], q_let_pr rpos 1)
553 | p::tl -> M.LetVVar ("obj_position" ^ (string_of_int n), M.Const [p], q_let_po tl (n+1))
556 (*let q_let_po = M.LetVVar ("obj_positions", M.Const opos, q_let_pr) in*)
558 print_endline "### "; MQueryUtil.text_of_query print_string (q_let_po opos 1) "\n"; flush stdout;
559 execute_query (q_let_po opos 1)