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       let out = output_string och in
  90       if ! query_num = 1 then out (time () ^ nl);
  91       out ("Query: " ^ string_of_int ! query_num ^ nl); Util.text_of_query out q nl;
  92       out ("Result:" ^ nl); Util.text_of_result out r nl;
  93       flush och
  94    in
  95    let execute q =
  96       let r = Mqint.execute q in
  97       if ! log_file <> "" then log q r;
  98       info := string_of_int ! query_num :: ! info;
  99       incr query_num;
 100       r
 101    in
 102    if ! confirm_query query then execute query else raise Discard
 103
 104 (* Query building functions  ************************************************)
 105
 106 let locate s =
 107    let module M = MathQL in
 108    let q =
 109     M.Ref (M.Property true M.RefineExact ("objectName", []) (M.Const [s]))
 110    in
 111     execute_query q
 112
 113 let searchPattern must_use can_use =
 114    let module M = MathQL in
 115    let in_path s = (s, []) in
 116    let assign v p = (in_path v, in_path p) in
 117
 118 (* can restrictions *)
 119
 120    let (cr_o,cr_r,cr_s) = can_use in
 121
 122    let uri_of_entry (r, p, d) = r in
 123
 124    let universe =
 125      match cr_o with
 126        None -> []
 127      | Some cr_o -> List.map uri_of_entry cr_o
 128    in
 129
 130    let tfst (a,b,c) = a in
 131    let tsnd (a,b,c) = b in
 132    let trd (a,b,c) = c in
 133
 134    let to_int_list l d =
 135    match d with
 136      None -> l
 137    | Some d -> l@[d]
 138    in
 139
 140    let opos =
 141      match cr_o with
 142        None -> []
 143      | Some cr_o -> (List.map tsnd cr_o) in
 144
 145    let odep =
 146      match cr_o with
 147        None -> []
 148      | Some cr_o -> List.map trd cr_o
 149                   (*  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    print_string "#### LUNGHEZZA ODEP: "; print_int (List.length odep); flush stdout;
 154    print_endline"";
 155    let rpos =
 156      match cr_r with
 157        None -> []
 158      | Some cr_r -> (List.map fst cr_r) in
 159
 160    let rdep =
 161      match cr_r with
 162        None -> []
 163      | Some cr_r -> List.map snd cr_r
 164                    (* let rdep_option_list = List.map snd cr_r in
 165                     let lr_dep_int = List.fold_left to_int_list [] rdep_option_list in
 166                       List.map string_of_int lr_dep_int *)
 167    in
 168
 169
 170    let spos =
 171      match cr_s with
 172        None -> []
 173      | Some cr_s -> (List.map tfst cr_s) in
 174
 175
 176    let sdep =
 177      match cr_s with
 178        None -> []
 179      | Some cr_s -> List.map tsnd cr_s
 180                    (* let sdep_option_list = List.map tsnd cr_s in
 181                     let ls_dep_int = List.fold_left to_int_list [] sdep_option_list in
 182                       List.map string_of_int ls_dep_int*)
 183    in
 184
 185
 186    let sor =
 187      match cr_s with
 188        None -> []
 189      | Some cr_s -> List.map trd cr_s in
 190
 191   (* let q_where_obj = function
 192        Some l ->
 193          if odep = [] then
 194            M.Sub
 195            (M.RefOf
 196            (M.Select
 197               ("uri",
 198               M.Relation (false, M.RefineExact, in_path "refObj", M.Ref (M.RefOf (M.RVar "uri0")), [assign "pos" "position"]),
 199               M.Ex ["uri"]
 200               (M.Meet (M.VVar "obj_positions", M.Record ("uri", in_path "pos"))))),
 201            M.VVar "universe")
 202          else
 203            M.Sub
 204            (M.RefOf
 205             (M.Select
 206               ("uri",
 207                 M.Relation
 208                  (false, M.RefineExact, in_path "refObj",
 209                    M.Ref (M.RefOf (M.RVar "uri0")),
 210                    [assign "p" "position"; assign "d" "depth"]
 211                  ),
 212                 M.Ex ["uri"]
 213                  (M.And
 214                   ((M.Meet(M.VVar "obj_positions",M.Record("uri",in_path "p"))),
 215                    (M.Meet(M.VVar "obj_depths", M.Record("uri",in_path "d")))))
 216               )
 217             ),
 218             M.VVar "universe"
 219            )
 220
 221      | None -> M.True
 222    in*)
 223
 224
 225
 226    let q_where_obj n = function
 227        Some l ->
 228          let rec q_ex n = function
 229              [] -> M.True
 230            | [(u,p,None)] ->
 231                              M.Meet (M.VVar ("obj_position" ^ string_of_int n), M.Record ("uri", in_path "p"))
 232
 233            | [(u,p,d)] ->
 234                           print_string "@@@@@ IN-WHERE-OBJ"; flush stdout;
 235                                                           print_endline"";
 236                           M.And
 237                             (M.Meet(M.VVar ("obj_position" ^ string_of_int n),M.Record("uri",in_path "p")),
 238                              M.Meet(M.VVar ("obj_depth" ^ string_of_int n), M.Record("uri",in_path "d")))
 239            | (u,p,None)::tl ->
 240                                M.Or
 241                                 (M.Meet (M.VVar ("obj_position" ^ string_of_int n), M.Record ("uri", in_path "p")),
 242                                  q_ex (n+1) tl)
 243            | (u,p,d)::tl ->
 244                              print_string "@@@@@ IN-WHERE-OBJ"; flush stdout;
 245                                 print_endline"";
 246                             M.Or
 247                              ((M.And
 248                                ((M.Meet(M.VVar ("obj_position" ^ string_of_int n),M.Record("uri",in_path "p"))),
 249                                 (M.Meet(M.VVar ("obj_depth" ^ string_of_int n), M.Record("uri",in_path "d"))))),
 250                              q_ex (n+1) tl)
 251          in
 252          M.Sub
 253            (M.RefOf
 254             (M.Select
 255               ("uri",
 256                 M.Relation
 257                  (false, M.RefineExact, in_path "refObj",
 258                    M.Ref (M.RefOf (M.RVar "uri0")),
 259                    [assign "p" "position"; assign "d" "depth"]
 260                  ),
 261                 M.Ex ["uri"]
 262                 (q_ex 1 l))),
 263             M.VVar "universe")
 264        | None -> M.True
 265    in
 266
 267
 268
 269
 270    let rec q_where_rel n cr_r= (*function*)
 271      (*  Some l ->*)
 272          let q0 =
 273           M.Sub
 274            (M.Property
 275              (false, M.RefineExact, ("refRel", ["position"]),
 276                M.RefOf(M.RVar "uri0")),
 277             M.VVar ("rel_position" ^ string_of_int n))
 278            in
 279            match cr_r with
 280              Some [] -> M.True
 281            | Some [(p,None)] -> q0
 282            | Some [(p,d)] ->
 283                         M.And
 284                          (q0,
 285                           M.Sub
 286                            (M.Property
 287                              (false, M.RefineExact, ("refRel", ["depth"]),
 288                               M.RefOf(M.RVar "uri0")),
 289                             M.VVar ("rel_depth" ^ string_of_int n)))
 290            | Some ((p,None)::tl) ->
 291                                M.Or
 292                                 (q0,
 293                                  q_where_rel (n+1) (Some tl))
 294            | Some ((p,d)::tl) ->
 295                             M.Or
 296                              (M.And
 297                                (q0,
 298                                 M.Sub
 299                                  (M.Property
 300                                    (false, M.RefineExact, ("refRel", ["depth"]),
 301                                     M.RefOf(M.RVar "uri0")),
 302                                   M.VVar ("rel_depth" ^ string_of_int n))),
 303                               q_where_rel (n+1) (Some tl))
 304            | None -> M.True
 305    in
 306
 307    let rec q_where_sort n cr_s = (*function *)
 308      (*  Some l ->*)
 309         let q0 =
 310          M.And
 311           (M.Sub
 312             (M.Property
 313               (false, M.RefineExact, ("refSort", ["position"]),
 314                 M.RefOf(M.RVar "uri0")
 315                ),
 316              M.VVar ("sort_position" ^ string_of_int n)),
 317            M.Sub
 318             (M.Property
 319               (false, M.RefineExact, ("refSort", ["sort"]),
 320                 M.RefOf(M.RVar "uri0")),
 321              M.VVar ("sort" ^ string_of_int n)))
 322         in
 323         match cr_s with
 324           Some [] -> M.True
 325         | Some [(p,None,s)] -> q0
 326
 327         | Some [(p,d,s)] ->
 328                        M.And
 329                         (q0,
 330                          M.Sub
 331                           (M.Property
 332                             (false, M.RefineExact, ("refSort", ["depth"]),
 333                              M.RefOf(M.RVar "uri0")),
 334                            M.VVar ("sort_depth" ^ string_of_int n)))
 335
 336         | Some ((p,None,s)::tl) ->
 337                             M.Or
 338                              (q0,
 339                               q_where_sort (n+1) (Some tl))
 340
 341         | Some((p,d,s)::tl) ->
 342                            M.Or
 343                             (M.And
 344                               (q0,
 345                                M.Sub
 346                                 (M.Property
 347                                   (false, M.RefineExact, ("refSort", ["depth"]),
 348                                    M.RefOf(M.RVar "uri0")),
 349                                  M.VVar ("sort_depth" ^ string_of_int n))),
 350                              q_where_sort (n+1) (Some tl))
 351         | None -> M.True
 352    in
 353
 354
 355
 356
 357    let q_where cr =
 358      let (cr_o,cr_r,cr_s) = cr in
 359      M.And(M.And(q_where_obj 1 cr_o, (q_where_rel 1 cr_r)), (q_where_sort 1 cr_s))
 360
 361        in
 362
 363 (* must restrictions *)
 364
 365    let build_select_obj (r, pos, dep) =
 366      match dep with
 367        None -> M.Select
 368                  ("uri",
 369                   M.Relation (false, M.RefineExact, ("backPointer", []),
 370                               M.Ref (M.Const [r]), [assign "p" "position"]),
 371                   M.Ex ["uri"]
 372                   ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p")))))
 373      | Some dep -> let string_dep = string_of_int dep in
 374                    M.Select
 375                      ("uri",
 376                       M.Relation (false, M.RefineExact, ("backPointer", []),
 377                                   M.Ref (M.Const [r]), [assign "p" "position";assign "d" "depth"]),
 378                       M.Ex ["uri"]
 379                       (M.And
 380                       ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))),
 381                       (M.Sub (M.Const [string_dep], M.Record ("uri", in_path "d"))))))
 382    in
 383
 384    let build_select_rel (pos, dep) =
 385      match dep with
 386        None -> M.Select
 387                  ("uri",
 388                   M.Relation (true, M.RefineExact, ("refRel", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth"]),
 389                   M.Ex ["uri"]
 390                   (M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))))
 391      | Some dep -> let string_dep = string_of_int dep in
 392                    M.Select
 393                      ("uri",
 394                       M.Relation (true, M.RefineExact, ("refRel", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth"]),
 395                       M.Ex ["uri"]
 396                       (M.And
 397                       ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))),
 398                       (M.Sub (M.Const [string_dep], M.Record ("uri", in_path "d"))))))
 399    in
 400
 401    let build_select_sort (pos, dep, sor) =
 402      match dep with
 403        None -> M.Select
 404                  ("uri",
 405                   M.Relation (true, M.RefineExact, ("refSort", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth";assign "s" "sort"]),
 406                   M.Ex ["uri"]
 407                   (M.And
 408                   ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))),
 409                   (M.Sub (M.Const [sor], M.Record ("uri", in_path "s"))))))
 410
 411      | Some dep -> let string_dep = string_of_int dep in
 412                    M.Select
 413                      ("uri",
 414                       M.Relation (true, M.RefineExact, ("refSort", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth";assign "s" "sort"]),
 415                       M.Ex ["uri"]
 416                       (M.And
 417                       ((M.And
 418                       ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))),
 419                       (M.Sub (M.Const [string_dep], M.Record ("uri", in_path "d"))))),
 420                       (M.Sub (M.Const [sor], M.Record ("uri", in_path "s"))))))
 421    in
 422
 423    let rec build_intersect_obj = function
 424        []       -> M.Pattern (M.Const ["[.]*"])
 425      | [hd]     -> build_select_obj hd
 426      | hd :: tl -> M.Intersect (build_select_obj hd, build_intersect_obj tl)
 427    in
 428
 429    let rec build_intersect_rel = function
 430        []       -> M.Ref(M.Const [])
 431      | [hd]     -> build_select_rel hd
 432      | hd :: tl -> M.Intersect (build_select_rel hd, build_intersect_rel tl)
 433    in
 434
 435    let rec build_intersect_sort = function
 436        []       -> M.Ref(M.Const [])
 437      | [hd]     -> build_select_sort hd
 438      | hd :: tl -> M.Intersect (build_select_sort hd, build_intersect_sort tl)
 439    in
 440
 441    let build_intersect = function
 442 (*      let tostring_sort (a,b,c) =
 443         let b1 = string_of_int b in
 444           (a,b1,c)
 445       in
 446       let tostring_rel (a,b) =
 447         let b1 = string_of_int b in
 448           (a,b1)
 449       in*)
 450
 451 (*      let (l1,l2,l3) = must in
 452       match (l1,l2,l3) with *)
 453         l1,[],[] -> build_intersect_obj l1
 454       | [],l2,[] -> (*let lrel = List.map tostring_rel l2 in*)
 455                       build_intersect_rel l2
 456       | [],[],l3 ->(* let lsort = List.map tostring_sort l3 in*)
 457                       build_intersect_sort l3
 458       | l1,l2,[] -> (*let lrel = List.map tostring_rel l2 in*)
 459                       M.Intersect (build_intersect_obj l1, build_intersect_rel l2)
 460       | l1,[],l3 ->(* let lsort = List.map tostring_sort l3 in                *)
 461                       M.Intersect (build_intersect_obj l1, build_intersect_sort l3)
 462       | [],l2,l3 ->(* let lrel = List.map tostring_rel l2 in
 463                     let lsort = List.map tostring_sort l3 in*)
 464                       M.Intersect (build_intersect_rel l2, build_intersect_sort l3)
 465       | l1,l2,l3 ->(* let lrel = List.map tostring_rel l2 in
 466              let lsort = List.map tostring_sort l3 in *)
 467               M.Intersect (M.Intersect (build_intersect_obj l1, build_intersect_rel l2), build_intersect_sort l3)
 468    in
 469
 470    let q_in = build_intersect must_use in
 471    let q_select = M.Select ("uri0", q_in, q_where can_use) in
 472
 473 (* variables for can restrictions *)
 474
 475    let q_let_u = M.LetVVar ("universe", M.Const universe, q_select) in
 476
 477    let rec q_let_s sor n =
 478      match sor with
 479        [] -> q_let_u
 480      | [s] -> M.LetVVar ("sort" ^ (string_of_int n), M.Const [s], q_let_u)
 481      | s::tl -> M.LetVVar ("sort" ^ (string_of_int n), M.Const [s], q_let_s tl (n+1))
 482    in
 483
 484 (*   let q_let_s = M.LetVVar ("sorts", M.Const sor, q_let_u) in *)
 485
 486    let rec q_let_ds sdep n =
 487      match sdep with
 488        []
 489      | [None] -> q_let_s sor 1
 490      | (None)::tl -> q_let_ds tl (n+1)
 491      | [Some d] -> M.LetVVar ("sort_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_s sor 1)
 492      | (Some d)::tl -> M.LetVVar ("sort_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_ds tl (n+1))
 493    in
 494
 495 (*   let q_let_ds = M.LetVVar ("sort_depths", M.Const sdep, q_let_s) in   *)
 496
 497    let rec q_let_dr rdep n =
 498      match rdep with
 499        []
 500      | [None] -> q_let_ds sdep 1
 501      | (None)::tl -> q_let_dr tl (n+1)
 502      | [Some d] -> M.LetVVar ("rel_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_ds sdep 1)
 503      | (Some d)::tl -> M.LetVVar ("rel_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_dr tl (n+1))
 504    in
 505
 506
 507    (*let q_let_dr = M.LetVVar ("rel_depths", M.Const rdep, q_let_ds) in*)
 508
 509    let rec q_let_do odep n =
 510      match odep with
 511        []
 512      | [None] -> q_let_dr rdep 1
 513      | (None)::tl -> q_let_do tl (n+1)
 514      |  [Some d] -> M.LetVVar ("obj_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_dr rdep 1)
 515      | (Some d)::tl -> M.LetVVar ("obj_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_do tl (n+1))
 516    in
 517
 518
 519 (*   let q_let_do = M.LetVVar ("obj_depths", M.Const odep, q_let_dr) in  *)
 520
 521
 522    let rec q_let_ps spos n =
 523      match spos with
 524        [] -> q_let_do odep 1
 525      | [p] -> M.LetVVar ("sort_position" ^ (string_of_int n), M.Const [p], q_let_do odep 1)
 526      | p::tl -> M.LetVVar ("sort_position" ^ (string_of_int n), M.Const [p], q_let_ps tl (n+1))
 527    in
 528
 529
 530 (*   let q_let_ps = M.LetVVar ("sort_positions", M.Const spos, q_let_do) in *)
 531
 532
 533    let rec q_let_pr rpos n =
 534      match rpos with
 535        [] -> q_let_ps spos 1
 536      | [p] -> M.LetVVar ("rel_position" ^ (string_of_int n), M.Const [p], q_let_ps spos 1)
 537      | p::tl -> M.LetVVar ("rel_position" ^ (string_of_int n), M.Const [p], q_let_pr tl (n+1))
 538    in
 539
 540
 541
 542 (*   let q_let_pr = M.LetVVar ("rel_positions", M.Const rpos, q_let_ps) in *)
 543
 544    let rec q_let_po opos n =
 545      match opos with
 546        [] -> q_let_pr rpos 1
 547      | [p] -> M.LetVVar ("obj_position" ^ (string_of_int n), M.Const [p], q_let_pr rpos 1)
 548      | p::tl -> M.LetVVar ("obj_position" ^ (string_of_int n), M.Const [p], q_let_po tl (n+1))
 549    in
 550
 551    (*let q_let_po = M.LetVVar ("obj_positions", M.Const opos, q_let_pr) in*)
 552
 553 print_endline "### ";  MQueryUtil.text_of_query print_string (q_let_po opos 1) "\n"; flush stdout;
 554    execute_query (q_let_po opos 1)