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 option
  43 type sort = string
  44
  45 type r_obj = (uri * position * depth)
  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 only_restrictions =
  51  (r_obj list option * r_rel list option * r_sort list option)
  52
  53 exception Discard
  54
  55 let nl = " <p>\n"
  56
  57 let query_num = ref 1
  58
  59 let log_file = ref ""
  60
  61 let confirm_query = ref (fun _ -> true)
  62
  63 let info = ref []
  64
  65 let set_log_file f =
  66    log_file := f
  67
  68 let set_confirm_query f =
  69    confirm_query := f
  70
  71 let get_query_info () = ! info
  72
  73 let execute_query query =
  74    let module Util = MQueryUtil in
  75    let mode = [Open_wronly; Open_append; Open_creat; Open_text] in
  76    let perm = 64 * 6 + 8 * 6 + 4 in
  77    let time () =
  78       let lt = Unix.localtime (Unix.time ()) in
  79       "NEW LOG: " ^
  80       string_of_int (lt.Unix.tm_mon + 1) ^ "-" ^
  81       string_of_int (lt.Unix.tm_mday + 1) ^ "-" ^
  82       string_of_int (lt.Unix.tm_year + 1900) ^ " " ^
  83       string_of_int (lt.Unix.tm_hour) ^ ":" ^
  84       string_of_int (lt.Unix.tm_min) ^ ":" ^
  85       string_of_int (lt.Unix.tm_sec)
  86    in
  87    let log q r =
  88       let och = open_out_gen mode perm ! log_file in
  89       if ! query_num = 1 then output_string och (time () ^ nl);
  90       let str =
  91        "Query: " ^ string_of_int ! query_num ^ nl ^ Util.text_of_query q ^ nl ^
  92        "Result:" ^ nl ^ Util.text_of_result r nl in
  93       output_string och str;
  94       flush och
  95    in
  96    let execute q =
  97       let r = Mqint.execute q in
  98       if ! log_file <> "" then log q r;
  99       info := string_of_int ! query_num :: ! info;
 100       incr query_num;
 101       r
 102    in
 103    if ! confirm_query query then execute query else raise Discard
 104
 105 (* Query building functions  ************************************************)
 106
 107 let locate s =
 108    let module M = MathQL in
 109    let q =
 110     M.Ref (M.Property true M.RefineExact ("objectName", []) (M.Const [s]))
 111    in
 112     execute_query q
 113
 114 let searchPattern must_use can_use =
 115    let module M = MathQL in
 116    let in_path s = (s, []) in
 117    let assign v p = (in_path v, in_path p) in
 118
 119 (* can restrictions *)
 120
 121    let (cr_o,cr_r,cr_s) = can_use in
 122
 123    let uri_of_entry (r, p, d) = r in
 124
 125    let universe =
 126      match cr_o with
 127        None -> []
 128      | Some cr_o -> List.map uri_of_entry cr_o
 129    in
 130
 131    let tfst (a,b,c) = a in
 132    let tsnd (a,b,c) = b in
 133    let trd (a,b,c) = c in
 134
 135    let to_int_list l d =
 136    match d with
 137      None -> l
 138    | Some d -> l@[d]
 139    in
 140
 141    let opos =
 142      match cr_o with
 143        None -> []
 144      | Some cr_o -> (List.map tsnd cr_o) in
 145
 146    let odep =
 147      match cr_o with
 148        None -> []
 149      | Some cr_o -> let odep_option_list = List.map trd cr_o in
 150                     let lo_dep_int = List.fold_left to_int_list [] odep_option_list in
 151                       List.map string_of_int lo_dep_int
 152    in
 153
 154    let rpos =
 155      match cr_r with
 156        None -> []
 157      | Some cr_r -> (List.map fst cr_r) in
 158
 159    let rdep =
 160      match cr_r with
 161        None -> []
 162      | Some cr_r -> let rdep_option_list = List.map snd cr_r in
 163                     let lr_dep_int = List.fold_left to_int_list [] rdep_option_list in
 164                       List.map string_of_int lr_dep_int
 165    in
 166
 167
 168    let spos =
 169      match cr_s with
 170        None -> []
 171      | Some cr_s -> (List.map tfst cr_s) in
 172
 173
 174    let sdep =
 175      match cr_s with
 176        None -> []
 177      | Some cr_s -> let sdep_option_list = List.map tsnd cr_s in
 178                     let ls_dep_int = List.fold_left to_int_list [] sdep_option_list in
 179                       List.map string_of_int ls_dep_int
 180    in
 181
 182
 183    let sor =
 184      match cr_s with
 185        None -> []
 186      | Some cr_s -> List.map trd cr_s in
 187
 188
 189    let q_where_obj = function
 190        Some l ->
 191          if odep = [] then
 192            M.Sub
 193            (M.RefOf
 194            (M.Select
 195               ("uri",
 196               M.Relation (false, M.RefineExact, in_path "refObj", M.Ref (M.RefOf (M.RVar "uri0")), [assign "pos" "position"]),
 197               M.Ex ["uri"]
 198               (M.Meet (M.VVar "obj_positions", M.Record ("uri", in_path "pos"))))),
 199            M.VVar "universe")
 200          else
 201            M.Sub
 202            (M.RefOf
 203             (M.Select
 204               ("uri",
 205                 M.Relation
 206                  (false, M.RefineExact, in_path "refObj",
 207                    M.Ref (M.RefOf (M.RVar "uri0")),
 208                    [assign "p" "position"; assign "d" "depth"]
 209                  ),
 210                 M.Ex ["uri"]
 211                  (M.And
 212                   ((M.Meet(M.VVar "obj_positions",M.Record("uri",in_path "p"))),
 213                    (M.Meet(M.VVar "obj_depths", M.Record("uri",in_path "d")))))
 214               )
 215             ),
 216             M.VVar "universe"
 217            )
 218
 219      | None -> M.True
 220    in
 221
 222    let q_where_rel = function
 223        Some l ->
 224          let q0 =
 225           M.Sub
 226            (M.Property
 227              (false, M.RefineExact, ("refRel", ["position"]),
 228                M.RefOf(M.RVar "uri0")),
 229             M.VVar "rel_positions")
 230          in
 231           if rdep = [] then q0
 232           else
 233             M.And
 234              (q0,
 235                M.Sub
 236                 (M.Property
 237                   (false, M.RefineExact, ("refRel", ["depth"]),
 238                     M.RefOf(M.RVar "uri0")),
 239                  M.VVar "rel_depths"))
 240      | None -> M.True
 241    in
 242
 243    let q_where_sort = function
 244        Some l ->
 245         let q0 =
 246          M.And
 247           (M.Sub
 248             (M.Property
 249               (false, M.RefineExact, ("refSort", ["position"]),
 250                 M.RefOf(M.RVar "uri0")
 251                ),
 252                M.VVar "sort_positions"),
 253            M.Sub
 254             (M.Property
 255               (false, M.RefineExact, ("refSort", ["sort"]),
 256                 M.RefOf(M.RVar "uri0")),
 257              M.VVar "sorts"))
 258          in
 259           if sdep = [] then
 260            q0
 261           else
 262            M.And
 263             (q0,
 264               M.Sub
 265                (M.VVar "sort_depths",
 266                 M.Property
 267                  (false, M.RefineExact, ("refSort", ["depth"]),
 268                    M.RefOf(M.RVar "uri0"))))
 269      | None -> M.True
 270    in
 271
 272    let q_where cr =
 273      let (cr_o,cr_r,cr_s) = cr in
 274      M.And(M.And(q_where_obj cr_o, q_where_rel cr_r), q_where_sort cr_s)
 275
 276        in
 277
 278 (* must restrictions *)
 279
 280    let build_select_obj (r, pos, dep) =
 281      match dep with
 282        None -> M.Select
 283                  ("uri",
 284                   M.Relation (false, M.RefineExact, ("backPointer", []),
 285                               M.Ref (M.Const [r]), [assign "pos" "position"]),
 286                   M.Ex ["uri"]
 287                   ((M.Sub (M.Const [pos], M.Record ("uri", in_path "pos")))))
 288      | Some dep -> let string_dep = string_of_int dep in
 289                    M.Select
 290                      ("uri",
 291                       M.Relation (false, M.RefineExact, ("backPointer", []),
 292                                   M.Ref (M.Const [r]), [assign "p" "position";assign "d" "depth"]),
 293                       M.Ex ["uri"]
 294                       (M.And
 295                       ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))),
 296                       (M.Sub (M.Const [string_dep], M.Record ("uri", in_path "d"))))))
 297    in
 298
 299    let build_select_rel (pos, dep) =
 300      match dep with
 301        None -> M.Select
 302                  ("uri",
 303                   M.Relation (true, M.RefineExact, ("refRel", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth"]),
 304                   M.Ex ["uri"]
 305                   (M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))))
 306      | Some dep -> let string_dep = string_of_int dep in
 307                    M.Select
 308                      ("uri",
 309                       M.Relation (true, M.RefineExact, ("refRel", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth"]),
 310                       M.Ex ["uri"]
 311                       (M.And
 312                       ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))),
 313                       (M.Sub (M.Const [string_dep], M.Record ("uri", in_path "d"))))))
 314    in
 315
 316    let build_select_sort (pos, dep, sor) =
 317      match dep with
 318        None -> M.Select
 319                  ("uri",
 320                   M.Relation (true, M.RefineExact, ("refSort", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth";assign "s" "sort"]),
 321                   M.Ex ["uri"]
 322                   (M.And
 323                   ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))),
 324                   (M.Sub (M.Const [sor], M.Record ("uri", in_path "s"))))))
 325
 326      | Some dep -> let string_dep = string_of_int dep in
 327                    M.Select
 328                      ("uri",
 329                       M.Relation (true, M.RefineExact, ("refSort", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth";assign "s" "sort"]),
 330                       M.Ex ["uri"]
 331                       (M.And
 332                       ((M.And
 333                       ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))),
 334                       (M.Sub (M.Const [string_dep], M.Record ("uri", in_path "d"))))),
 335                       (M.Sub (M.Const [sor], M.Record ("uri", in_path "s"))))))
 336    in
 337
 338    let rec build_intersect_obj = function
 339        []       -> M.Pattern (M.Const ["[.]*"])
 340      | [hd]     -> build_select_obj hd
 341      | hd :: tl -> M.Intersect (build_select_obj hd, build_intersect_obj tl)
 342    in
 343
 344    let rec build_intersect_rel = function
 345        []       -> M.Ref(M.Const [])
 346      | [hd]     -> build_select_rel hd
 347      | hd :: tl -> M.Intersect (build_select_rel hd, build_intersect_rel tl)
 348    in
 349
 350    let rec build_intersect_sort = function
 351        []       -> M.Ref(M.Const [])
 352      | [hd]     -> build_select_sort hd
 353      | hd :: tl -> M.Intersect (build_select_sort hd, build_intersect_sort tl)
 354    in
 355
 356    let build_intersect = function
 357 (*      let tostring_sort (a,b,c) =
 358         let b1 = string_of_int b in
 359           (a,b1,c)
 360       in
 361       let tostring_rel (a,b) =
 362         let b1 = string_of_int b in
 363           (a,b1)
 364       in*)
 365
 366 (*      let (l1,l2,l3) = must in
 367       match (l1,l2,l3) with *)
 368         l1,[],[] -> build_intersect_obj l1
 369       | [],l2,[] -> (*let lrel = List.map tostring_rel l2 in*)
 370                       build_intersect_rel l2
 371       | [],[],l3 ->(* let lsort = List.map tostring_sort l3 in*)
 372                       build_intersect_sort l3
 373       | l1,l2,[] -> (*let lrel = List.map tostring_rel l2 in*)
 374                       M.Intersect (build_intersect_obj l1, build_intersect_rel l2)
 375       | l1,[],l3 ->(* let lsort = List.map tostring_sort l3 in                *)
 376                       M.Intersect (build_intersect_obj l1, build_intersect_sort l3)
 377       | [],l2,l3 ->(* let lrel = List.map tostring_rel l2 in
 378                     let lsort = List.map tostring_sort l3 in*)
 379                       M.Intersect (build_intersect_rel l2, build_intersect_sort l3)
 380       | l1,l2,l3 ->(* let lrel = List.map tostring_rel l2 in
 381              let lsort = List.map tostring_sort l3 in *)
 382               M.Intersect (M.Intersect (build_intersect_obj l1, build_intersect_rel l2), build_intersect_sort l3)
 383    in
 384
 385    let q_in = build_intersect must_use in
 386    let q_select = M.Select ("uri0", q_in, q_where can_use) in
 387
 388 (* variables for can restrictions *)
 389
 390    let q_let_u = M.LetVVar ("universe", M.Const universe, q_select) in
 391
 392    let q_let_s = M.LetVVar ("sorts", M.Const sor, q_let_u) in
 393
 394    let q_let_ds = M.LetVVar ("sort_depths", M.Const sdep, q_let_s) in
 395
 396    let q_let_dr = M.LetVVar ("rel_depths", M.Const rdep, q_let_ds) in
 397
 398    let q_let_do = M.LetVVar ("obj_depths", M.Const odep, q_let_dr) in
 399
 400    let q_let_ps = M.LetVVar ("sort_positions", M.Const spos, q_let_do) in
 401
 402    let q_let_pr = M.LetVVar ("rel_positions", M.Const rpos, q_let_ps) in
 403
 404    let q_let_po = M.LetVVar ("obj_positions", M.Const opos, q_let_pr) in
 405 print_endline ("### " ^ MQueryUtil.text_of_query q_let_po) ; flush stdout;
 406    execute_query q_let_po