helm/gTopLevel/mQueryGenerator.ml

   1 (* Copyright (C) 2000, HELM Team.
   2  *
   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.
   6  *
   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.
  11  *
  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.
  16  *
  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,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (******************************************************************************)
  27 (*                                                                            *)
  28 (*                               PROJECT HELM                                 *)
  29 (*                                                                            *)
  30 (*                     Ferruccio Guidi <fguidi@cs.unibo.it>                   *)
  31 (*                                 30/04/2002                                 *)
  32 (*                                                                            *)
  33 (*                                                                            *)
  34 (******************************************************************************)
  35
  36 (* Query issuing functions **************************************************)
  37
  38
  39
  40 type uri = string
  41 type position = string
  42 type depth = int
  43 type sort = string
  44
  45 type r_obj = (uri * position * depth option)
  46 type r_rel = (position* depth)
  47 type r_sort = (position* depth * sort)
  48
  49 type must_restrictions = (r_obj list * r_rel list * r_sort list)
  50 type can_restrictions = (r_obj list option * r_rel list option * r_sort list option)
  51
  52
  53
  54
  55
  56
  57
  58
  59
  60 exception Discard
  61
  62 let nl = " <p>\n"
  63
  64 let query_num = ref 1
  65
  66 let log_file = ref ""
  67
  68 let confirm_query = ref (fun _ -> true)
  69
  70 let info = ref []
  71
  72 let set_log_file f =
  73    log_file := f
  74
  75 let set_confirm_query f =
  76    confirm_query := f
  77
  78 let get_query_info () = ! info
  79
  80 let execute_query query =
  81    let module Util = MQueryUtil in
  82    let mode = [Open_wronly; Open_append; Open_creat; Open_text] in
  83    let perm = 64 * 6 + 8 * 6 + 4 in
  84    let time () =
  85       let lt = Unix.localtime (Unix.time ()) in
  86       "NEW LOG: " ^
  87       string_of_int (lt.Unix.tm_mon + 1) ^ "-" ^
  88       string_of_int (lt.Unix.tm_mday + 1) ^ "-" ^
  89       string_of_int (lt.Unix.tm_year + 1900) ^ " " ^
  90       string_of_int (lt.Unix.tm_hour) ^ ":" ^
  91       string_of_int (lt.Unix.tm_min) ^ ":" ^
  92       string_of_int (lt.Unix.tm_sec)
  93    in
  94    let log q r =
  95       let och = open_out_gen mode perm ! log_file in
  96       if ! query_num = 1 then output_string och (time () ^ nl);
  97       let str =
  98        "Query: " ^ string_of_int ! query_num ^ nl ^ Util.text_of_query q ^ nl ^
  99        "Result:" ^ nl ^ Util.text_of_result r nl in
 100       output_string och str;
 101       flush och
 102    in
 103    let execute q =
 104       let r = Mqint.execute q in
 105       if ! log_file <> "" then log q r;
 106       info := string_of_int ! query_num :: ! info;
 107       incr query_num;
 108       r
 109    in
 110    if ! confirm_query query then execute query else raise Discard
 111
 112 (* Query building functions  ************************************************)
 113
 114 let locate s =
 115    let module M = MathQL in
 116    let q =
 117     M.Ref (M.Property true M.RefineExact ("objectName", []) (M.Const [s]))
 118    in
 119     execute_query q
 120
 121 let searchPattern must_use can_use =
 122    let module M = MathQL in
 123    let in_path s = (s, []) in
 124    let assign v p = (in_path v, in_path p) in
 125
 126    let q_where_obj = function
 127        Some l ->
 128          M.Sub
 129          (M.RefOf
 130            (M.Select
 131              ("uri",
 132                M.Relation
 133                 (false, M.RefineExact, in_path "refObj",
 134                  M.Ref (M.RefOf (M.RVar "uri0")),
 135                  [assign "pos" "position"]),
 136                M.Ex ["uri"]
 137                 (M.Meet (M.VVar "obj_positions", M.Record ("uri", in_path "pos")))
 138               )
 139            ),
 140            M.VVar "universe"
 141          )
 142      | None -> M.True
 143    in
 144
 145    let q_where_rel = function
 146        Some l ->
 147          M.And
 148         (M.Sub(M.VVar "rel_positions", M.Property(false, M.RefineExact, ("refRel", ["position"]), M.RefOf(M.RVar "uri0"))),
 149          M.Sub(M.VVar "rel_depths", M.Property(false, M.RefineExact, ("refRel", ["depth"]), M.RefOf(M.RVar "uri0"))))
 150      | None -> M.True
 151    in
 152
 153    let q_where_sort = function
 154        Some l ->
 155          M.And
 156         (M.And
 157         (M.Sub(M.VVar "sort_positions", M.Property(false, M.RefineExact, ("refSort", ["position"]), M.RefOf(M.RVar "uri0"))),
 158          M.Sub(M.VVar "sort_depths", M.Property(false, M.RefineExact, ("refSort", ["depth"]), M.RefOf(M.RVar "uri0")))),
 159          M.Sub(M.VVar "sorts", M.Property(false, M.RefineExact, ("refSort", ["sort"]), M.RefOf(M.RVar "uri0"))))
 160      | None -> M.True
 161    in
 162
 163    let q_where cr =
 164      let (cr_o,cr_r,cr_s) = cr in
 165      M.And(M.And(q_where_obj cr_o, q_where_rel cr_r), q_where_sort cr_s)
 166
 167        in
 168
 169    let uri_of_entry (r, p, d) = r in
 170
 171    let build_select_obj (r, pos, dep) =
 172      match dep with
 173        None -> M.Select
 174                  ("uri",
 175                   M.Relation (false, M.RefineExact, ("backPointer", []),
 176                               M.Ref (M.Const [r]), [assign "pos" "position"]),
 177                   M.Ex ["uri"]
 178                   ((M.Sub (M.Const [pos], M.Record ("uri", in_path "pos")))))
 179      | Some dep -> let string_dep = string_of_int dep in
 180                    M.Select
 181                      ("uri",
 182                       M.Relation (false, M.RefineExact, ("backPointer", []),
 183                                   M.Ref (M.Const [r]), [assign "p" "position";assign "d" "depth"]),
 184                       M.Ex ["uri"]
 185                       (M.And
 186                       ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))),
 187                       (M.Sub (M.Const [string_dep], M.Record ("uri", in_path "d"))))))
 188    in
 189
 190    let build_select_rel (pos, dep) =
 191       M.Select
 192        ("uri",
 193         M.Relation (true, M.RefineExact, ("refRel", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth"]),
 194         M.Ex ["uri"]
 195         (M.And
 196         ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))),
 197         (M.Sub (M.Const [dep], M.Record ("uri", in_path "d"))))))
 198    in
 199
 200    let build_select_sort (pos, dep, sor) =
 201       M.Select
 202        ("uri",
 203         M.Relation (true, M.RefineExact, ("refSort", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth";assign "s" "sort"]),
 204         M.Ex ["uri"]
 205         (M.And
 206         ((M.And
 207         ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))),
 208         (M.Sub (M.Const [dep], M.Record ("uri", in_path "d"))))),
 209         (M.Sub (M.Const [sor], M.Record ("uri", in_path "s"))))))
 210    in
 211
 212    let rec build_intersect_obj = function
 213        []       -> M.Pattern (M.Const ["[.]*"])
 214      | [hd]     -> build_select_obj hd
 215      | hd :: tl -> M.Intersect (build_select_obj hd, build_intersect_obj tl)
 216    in
 217
 218    let rec build_intersect_rel = function
 219        []       -> M.Ref(M.Const [])
 220      | [hd]     -> build_select_rel hd
 221      | hd :: tl -> M.Intersect (build_select_rel hd, build_intersect_rel tl)
 222    in
 223
 224    let rec build_intersect_sort = function
 225        []       -> M.Ref(M.Const [])
 226      | [hd]     -> build_select_sort hd
 227      | hd :: tl -> M.Intersect (build_select_sort hd, build_intersect_sort tl)
 228    in
 229
 230    let build_intersect must =
 231       let tostring_sort (a,b,c) =
 232         let b1 = string_of_int b in
 233           (a,b1,c)
 234       in
 235       let tostring_rel (a,b) =
 236         let b1 = string_of_int b in
 237           (a,b1)
 238       in
 239
 240       let (l1,l2,l3) = must in
 241       match (l1,l2,l3) with
 242         l1,[],[] -> build_intersect_obj l1
 243       | [],l2,[] -> let lrel = List.map tostring_rel l2 in
 244                       build_intersect_rel lrel
 245       | [],[],l3 -> let lsort = List.map tostring_sort l3 in
 246                       build_intersect_sort lsort
 247       | l1,l2,[] -> let lrel = List.map tostring_rel l2 in
 248                       M.Intersect (build_intersect_obj l1, build_intersect_rel lrel)
 249       | l1,[],l3 -> let lsort = List.map tostring_sort l3 in
 250                       M.Intersect (build_intersect_obj l1, build_intersect_sort lsort)
 251       | [],l2,l3 -> let lrel = List.map tostring_rel l2 in
 252                     let lsort = List.map tostring_sort l3 in
 253                       M.Intersect (build_intersect_rel lrel, build_intersect_sort lsort)
 254       | _ -> let lrel = List.map tostring_rel l2 in
 255              let lsort = List.map tostring_sort l3 in
 256               M.Intersect (M.Intersect (build_intersect_obj l1, build_intersect_rel lrel), build_intersect_sort lsort)
 257    in
 258
 259    let q_in = build_intersect must_use in
 260    let q_select = M.Select ("uri0", q_in, q_where can_use) in
 261
 262    let (cr_o,cr_r,cr_s) = can_use in
 263
 264    let universe =
 265      match cr_o with
 266        None -> M.Const []
 267      | Some cr_o -> M.Const (List.map uri_of_entry cr_o)
 268    in
 269
 270    let tfst (a,b,c) = a in
 271    let tsnd (a,b,c) = b in
 272    let trd (a,b,c) = c in
 273
 274    let opos =
 275      match cr_o with
 276        None -> M.Const []
 277      | Some cr_o -> M.Const (List.map tsnd cr_o) in
 278
 279    let odep =
 280      match cr_o with
 281        None -> M.Const []
 282      | Some cr_o -> let lofc = List.map trd cr_o in
 283                     let f l c =
 284                     match c with
 285                       None -> l
 286                     | Some c -> l@[c]
 287                     in
 288                     let lof_dep_int = List.fold_left f [] lofc in
 289                       M.Const(List.map string_of_int lof_dep_int)
 290    in
 291
 292    let rpos =
 293      match cr_r with
 294        None -> M.Const []
 295      | Some cr_r -> M.Const (List.map fst cr_r) in
 296
 297    let rdep =
 298      match cr_r with
 299        None -> M.Const []
 300      | Some cr_r -> let rdep_int = List.map snd cr_r in
 301                       M.Const (List.map string_of_int rdep_int)
 302    in
 303
 304
 305    let spos =
 306      match cr_s with
 307        None -> M.Const []
 308      | Some cr_s -> M.Const (List.map tfst cr_s) in
 309
 310
 311    let sdep =
 312      match cr_s with
 313        None -> M.Const []
 314      | Some cr_s -> let sdep_int = List.map tsnd cr_s in
 315                       M.Const (List.map string_of_int sdep_int)
 316    in
 317
 318
 319    let sor =
 320      match cr_s with
 321        None -> M.Const[]
 322      | Some cr_s -> M.Const (List.map trd cr_s) in
 323
 324    let q_let_u = M.LetVVar ("universe", universe, q_select) in
 325
 326    let q_let_s = M.LetVVar ("sorts", sor, q_let_u) in
 327
 328    let q_let_ds = M.LetVVar ("sort_depths", sdep, q_let_s) in
 329
 330    let q_let_dr = M.LetVVar ("rel_depths", rdep, q_let_ds) in
 331
 332    let q_let_do = M.LetVVar ("obj_depths", odep, q_let_dr) in
 333
 334    let q_let_ps = M.LetVVar ("sort_positions", spos, q_let_do) in
 335
 336    let q_let_pr = M.LetVVar ("rel_positions", rpos, q_let_ps) in
 337
 338    let q_let_po = M.LetVVar ("obj_positions", opos, q_let_pr) in
 339 print_endline ("### " ^ MQueryUtil.text_of_query q_let_po) ; flush stdout;
 340    execute_query q_let_po