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