helm/ocaml/mquery_generator/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 module MQICallbacks =
  37    struct
  38       let log s = prerr_string s
  39    end
  40
  41 module MQI = MQueryInterpreter.Make(MQICallbacks)
  42
  43 (* Query issuing functions **************************************************)
  44
  45 type uri = string
  46 type position = string
  47 type depth = int option
  48 type sort = string
  49
  50 type r_obj = (uri * position * depth)
  51 type r_rel = (position* depth)
  52 type r_sort = (position* depth * sort)
  53
  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)
  57
  58 exception Discard
  59
  60 let nl = " <p>\n"
  61
  62 let query_num = ref 1
  63
  64 let log_file = ref ""
  65
  66 let confirm_query = ref (fun _ -> true)
  67
  68 let info = ref []
  69
  70 let set_log_file f =
  71    log_file := f
  72
  73 let set_confirm_query f =
  74    confirm_query := f
  75
  76 let get_query_info () = ! info
  77
  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
  82    let time () =
  83       let lt = Unix.localtime (Unix.time ()) in
  84       "NEW LOG: " ^
  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)
  91    in
  92    let log q r =
  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;
  98       flush och
  99    in
 100    let execute q =
 101       let r = MQI.execute "" q in
 102       if ! log_file <> "" then log q r;
 103       info := string_of_int ! query_num :: ! info;
 104       incr query_num;
 105       r
 106    in
 107    if ! confirm_query query then execute query else raise Discard
 108
 109 (* Query building functions  ************************************************)
 110
 111 let locate s =
 112    let module M = MathQL in
 113    let q =
 114     M.Ref (M.Property true M.RefineExact ("objectName", []) (M.Const [s]))
 115    in
 116     execute_query q
 117
 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
 122
 123 (* can restrictions *)
 124
 125    let (cr_o,cr_r,cr_s) = can_use in
 126
 127    let uri_of_entry (r, p, d) = r in
 128
 129    let universe =
 130      match cr_o with
 131        None -> []
 132      | Some cr_o -> List.map uri_of_entry cr_o
 133    in
 134
 135    let tfst (a,b,c) = a in
 136    let tsnd (a,b,c) = b in
 137    let trd (a,b,c) = c in
 138
 139    let to_int_list l d =
 140    match d with
 141      None -> l
 142    | Some d -> l@[d]
 143    in
 144
 145    let opos =
 146      match cr_o with
 147        None -> []
 148      | Some cr_o -> (List.map tsnd cr_o) in
 149
 150    let odep =
 151      match cr_o with
 152        None -> []
 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*)
 157    in
 158    print_string "#### LUNGHEZZA ODEP: "; print_int (List.length odep); flush stdout;
 159    print_endline"";
 160    let rpos =
 161      match cr_r with
 162        None -> []
 163      | Some cr_r -> (List.map fst cr_r) in
 164
 165    let rdep =
 166      match cr_r with
 167        None -> []
 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 *)
 172    in
 173
 174
 175    let spos =
 176      match cr_s with
 177        None -> []
 178      | Some cr_s -> (List.map tfst cr_s) in
 179
 180
 181    let sdep =
 182      match cr_s with
 183        None -> []
 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*)
 188    in
 189
 190
 191    let sor =
 192      match cr_s with
 193        None -> []
 194      | Some cr_s -> List.map trd cr_s in
 195
 196   (* let q_where_obj = function
 197        Some l ->
 198          if odep = [] then
 199            M.Sub
 200            (M.RefOf
 201            (M.Select
 202               ("uri",
 203               M.Relation (false, M.RefineExact, in_path "refObj", M.Ref (M.RefOf (M.RVar "uri0")), [assign "pos" "position"]),
 204               M.Ex ["uri"]
 205               (M.Meet (M.VVar "obj_positions", M.Record ("uri", in_path "pos"))))),
 206            M.VVar "universe")
 207          else
 208            M.Sub
 209            (M.RefOf
 210             (M.Select
 211               ("uri",
 212                 M.Relation
 213                  (false, M.RefineExact, in_path "refObj",
 214                    M.Ref (M.RefOf (M.RVar "uri0")),
 215                    [assign "p" "position"; assign "d" "depth"]
 216                  ),
 217                 M.Ex ["uri"]
 218                  (M.And
 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")))))
 221               )
 222             ),
 223             M.VVar "universe"
 224            )
 225
 226      | None -> M.True
 227    in*)
 228
 229
 230
 231    let q_where_obj n = function
 232        Some l ->
 233          let rec q_ex n = function
 234              [] -> M.True
 235            | [(u,p,None)] ->
 236                              M.Meet (M.VVar ("obj_position" ^ string_of_int n), M.Record ("uri", in_path "p"))
 237
 238            | [(u,p,d)] ->
 239                           print_string "@@@@@ IN-WHERE-OBJ"; flush stdout;
 240                                                           print_endline"";
 241                           M.And
 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")))
 244            | (u,p,None)::tl ->
 245                                M.Or
 246                                 (M.Meet (M.VVar ("obj_position" ^ string_of_int n), M.Record ("uri", in_path "p")),
 247                                  q_ex (n+1) tl)
 248            | (u,p,d)::tl ->
 249                              print_string "@@@@@ IN-WHERE-OBJ"; flush stdout;
 250                                 print_endline"";
 251                             M.Or
 252                              ((M.And
 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"))))),
 255                              q_ex (n+1) tl)
 256          in
 257          M.Sub
 258            (M.RefOf
 259             (M.Select
 260               ("uri",
 261                 M.Relation
 262                  (false, M.RefineExact, in_path "refObj",
 263                    M.Ref (M.RefOf (M.RVar "uri0")),
 264                    [assign "p" "position"; assign "d" "depth"]
 265                  ),
 266                 M.Ex ["uri"]
 267                 (q_ex 1 l))),
 268             M.VVar "universe")
 269        | None -> M.True
 270    in
 271
 272
 273
 274
 275    let rec q_where_rel n cr_r= (*function*)
 276      (*  Some l ->*)
 277          let q0 =
 278           M.Sub
 279            (M.Property
 280              (false, M.RefineExact, ("refRel", ["position"]),
 281                M.RefOf(M.RVar "uri0")),
 282             M.VVar ("rel_position" ^ string_of_int n))
 283            in
 284            match cr_r with
 285              Some [] -> M.True
 286            | Some [(p,None)] -> q0
 287            | Some [(p,d)] ->
 288                         M.And
 289                          (q0,
 290                           M.Sub
 291                            (M.Property
 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) ->
 296                                M.Or
 297                                 (q0,
 298                                  q_where_rel (n+1) (Some tl))
 299            | Some ((p,d)::tl) ->
 300                             M.Or
 301                              (M.And
 302                                (q0,
 303                                 M.Sub
 304                                  (M.Property
 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))
 309            | None -> M.True
 310    in
 311
 312    let rec q_where_sort n cr_s = (*function *)
 313      (*  Some l ->*)
 314         let q0 =
 315          M.And
 316           (M.Sub
 317             (M.Property
 318               (false, M.RefineExact, ("refSort", ["position"]),
 319                 M.RefOf(M.RVar "uri0")
 320                ),
 321              M.VVar ("sort_position" ^ string_of_int n)),
 322            M.Sub
 323             (M.Property
 324               (false, M.RefineExact, ("refSort", ["sort"]),
 325                 M.RefOf(M.RVar "uri0")),
 326              M.VVar ("sort" ^ string_of_int n)))
 327         in
 328         match cr_s with
 329           Some [] -> M.True
 330         | Some [(p,None,s)] -> q0
 331
 332         | Some [(p,d,s)] ->
 333                        M.And
 334                         (q0,
 335                          M.Sub
 336                           (M.Property
 337                             (false, M.RefineExact, ("refSort", ["depth"]),
 338                              M.RefOf(M.RVar "uri0")),
 339                            M.VVar ("sort_depth" ^ string_of_int n)))
 340
 341         | Some ((p,None,s)::tl) ->
 342                             M.Or
 343                              (q0,
 344                               q_where_sort (n+1) (Some tl))
 345
 346         | Some((p,d,s)::tl) ->
 347                            M.Or
 348                             (M.And
 349                               (q0,
 350                                M.Sub
 351                                 (M.Property
 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))
 356         | None -> M.True
 357    in
 358
 359
 360
 361
 362    let q_where cr =
 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))
 365
 366        in
 367
 368 (* must restrictions *)
 369
 370    let build_select_obj (r, pos, dep) =
 371      match dep with
 372        None -> M.Select
 373                  ("uri",
 374                   M.Relation (false, M.RefineExact, ("backPointer", []),
 375                               M.Ref (M.Const [r]), [assign "p" "position"]),
 376                   M.Ex ["uri"]
 377                   ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p")))))
 378      | Some dep -> let string_dep = string_of_int dep in
 379                    M.Select
 380                      ("uri",
 381                       M.Relation (false, M.RefineExact, ("backPointer", []),
 382                                   M.Ref (M.Const [r]), [assign "p" "position";assign "d" "depth"]),
 383                       M.Ex ["uri"]
 384                       (M.And
 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"))))))
 387    in
 388
 389    let build_select_rel (pos, dep) =
 390      match dep with
 391        None -> M.Select
 392                  ("uri",
 393                   M.Relation (true, M.RefineExact, ("refRel", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth"]),
 394                   M.Ex ["uri"]
 395                   (M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))))
 396      | Some dep -> let string_dep = string_of_int dep in
 397                    M.Select
 398                      ("uri",
 399                       M.Relation (true, M.RefineExact, ("refRel", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth"]),
 400                       M.Ex ["uri"]
 401                       (M.And
 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"))))))
 404    in
 405
 406    let build_select_sort (pos, dep, sor) =
 407      match dep with
 408        None -> M.Select
 409                  ("uri",
 410                   M.Relation (true, M.RefineExact, ("refSort", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth";assign "s" "sort"]),
 411                   M.Ex ["uri"]
 412                   (M.And
 413                   ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))),
 414                   (M.Sub (M.Const [sor], M.Record ("uri", in_path "s"))))))
 415
 416      | Some dep -> let string_dep = string_of_int dep in
 417                    M.Select
 418                      ("uri",
 419                       M.Relation (true, M.RefineExact, ("refSort", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth";assign "s" "sort"]),
 420                       M.Ex ["uri"]
 421                       (M.And
 422                       ((M.And
 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"))))))
 426    in
 427
 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)
 432    in
 433
 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)
 438    in
 439
 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)
 444    in
 445
 446    let build_intersect = function
 447 (*      let tostring_sort (a,b,c) =
 448         let b1 = string_of_int b in
 449           (a,b1,c)
 450       in
 451       let tostring_rel (a,b) =
 452         let b1 = string_of_int b in
 453           (a,b1)
 454       in*)
 455
 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)
 473    in
 474
 475    let q_in = build_intersect must_use in
 476    let q_select = M.Select ("uri0", q_in, q_where can_use) in
 477
 478 (* variables for can restrictions *)
 479
 480    let q_let_u = M.LetVVar ("universe", M.Const universe, q_select) in
 481
 482    let rec q_let_s sor n =
 483      match sor with
 484        [] -> q_let_u
 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))
 487    in
 488
 489 (*   let q_let_s = M.LetVVar ("sorts", M.Const sor, q_let_u) in *)
 490
 491    let rec q_let_ds sdep n =
 492      match sdep with
 493        []
 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))
 498    in
 499
 500 (*   let q_let_ds = M.LetVVar ("sort_depths", M.Const sdep, q_let_s) in   *)
 501
 502    let rec q_let_dr rdep n =
 503      match rdep with
 504        []
 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))
 509    in
 510
 511
 512    (*let q_let_dr = M.LetVVar ("rel_depths", M.Const rdep, q_let_ds) in*)
 513
 514    let rec q_let_do odep n =
 515      match odep with
 516        []
 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))
 521    in
 522
 523
 524 (*   let q_let_do = M.LetVVar ("obj_depths", M.Const odep, q_let_dr) in  *)
 525
 526
 527    let rec q_let_ps spos n =
 528      match spos with
 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))
 532    in
 533
 534
 535 (*   let q_let_ps = M.LetVVar ("sort_positions", M.Const spos, q_let_do) in *)
 536
 537
 538    let rec q_let_pr rpos n =
 539      match rpos with
 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))
 543    in
 544
 545
 546
 547 (*   let q_let_pr = M.LetVVar ("rel_positions", M.Const rpos, q_let_ps) in *)
 548
 549    let rec q_let_po opos n =
 550      match opos with
 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))
 554    in
 555
 556    (*let q_let_po = M.LetVVar ("obj_positions", M.Const opos, q_let_pr) in*)
 557
 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)