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