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