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 exception Discard
  39
  40 let nl = " <p>\n"
  41
  42 let query_num = ref 1
  43
  44 let log_file = ref ""
  45
  46 let confirm_query = ref (fun _ -> true)
  47
  48 let info = ref []
  49
  50 let set_log_file f =
  51    log_file := f
  52
  53 let set_confirm_query f =
  54    confirm_query := f
  55
  56 let get_query_info () = ! info
  57
  58 let execute_query query =
  59    let module Util = MQueryUtil in
  60    let mode = [Open_wronly; Open_append; Open_creat; Open_text] in
  61    let perm = 64 * 6 + 8 * 6 + 4 in
  62    let time () =
  63       let lt = Unix.localtime (Unix.time ()) in
  64       "NEW LOG: " ^
  65       string_of_int (lt.Unix.tm_mon + 1) ^ "-" ^
  66       string_of_int (lt.Unix.tm_mday + 1) ^ "-" ^
  67       string_of_int (lt.Unix.tm_year + 1900) ^ " " ^
  68       string_of_int (lt.Unix.tm_hour) ^ ":" ^
  69       string_of_int (lt.Unix.tm_min) ^ ":" ^
  70       string_of_int (lt.Unix.tm_sec)
  71    in
  72    let log q r =
  73       let och = open_out_gen mode perm ! log_file in
  74       if ! query_num = 1 then output_string och (time () ^ nl);
  75       let str =
  76        "Query: " ^ string_of_int ! query_num ^ nl ^ Util.text_of_query q ^ nl ^
  77        "Result:" ^ nl ^ Util.text_of_result r nl in
  78       output_string och str;
  79       flush och
  80    in
  81    let execute q =
  82       let r = Mqint.execute q in
  83       if ! log_file <> "" then log q r;
  84       info := string_of_int ! query_num :: ! info;
  85       incr query_num;
  86       r
  87    in
  88    if ! confirm_query query then execute query else raise Discard
  89
  90 (* Query building functions  ************************************************)
  91
  92 let locate s =
  93    let module M = MathQL in
  94    let q =
  95     M.Ref (M.Property true M.RefineExact ("objectName", []) (M.Const [s]))
  96    in
  97     execute_query q
  98
  99 let searchPattern e c t level =
 100    let module M = MathQL in
 101    let module L = MQueryLevels in
 102    let mainConclusion =
 103     "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion" in
 104    let inConclusion =
 105     "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion" in
 106    let in_path s = (s, []) in
 107    let assign v p = (in_path v, in_path p) in
 108    let v_pos = M.Const [mainConclusion; inConclusion] in
 109    let q_where =
 110     M.Sub
 111      (M.RefOf
 112        (M.Select
 113          ("uri",
 114            M.Relation
 115             (false, M.RefineExact, in_path "refObj",
 116              M.Ref (M.RefOf (M.RVar "uri0")),
 117              [assign "pos" "position"]),
 118            M.Ex ["uri"]
 119             (M.Meet (M.VVar "positions", M.Record ("uri", in_path "pos")))
 120           )
 121        ),
 122        M.VVar "universe"
 123      ) in
 124    let uri_of_entry (r, b, v) = r in
 125    let rec restrict level = function
 126       | []                -> []
 127       | (u, b, v) :: tail ->
 128          if v <= level then (u, b, v) :: restrict level tail
 129          else restrict level tail
 130    in
 131    let build_select (r, b, v) =
 132     let pos = if b then mainConclusion else inConclusion in
 133       M.Select
 134        ("uri",
 135         M.Relation (false, M.RefineExact, ("backPointer", []),
 136                     M.Ref (M.Const [r]), [assign "pos" "position"]),
 137         M.Ex ["uri"] (M.Sub (M.Const [pos], M.Record ("uri", in_path "pos")))) in
 138    let rec build_intersect = function
 139       | []       -> M.Pattern (M.Const ["[.]*"])
 140       | [hd]     -> build_select hd
 141       | hd :: tl -> M.Intersect (build_select hd, build_intersect tl)
 142    in
 143    let levels = L.levels_of_term e c t in
 144    let rest = restrict level levels in
 145    info := [string_of_int (List.length rest)];
 146    let q_in = build_intersect rest in
 147    let q_select = M.Select ("uri0", q_in, q_where) in
 148    let universe = M.Const (List.map uri_of_entry levels) in
 149    let q_let_u = M.LetVVar ("universe", universe, q_select) in
 150    let q_let_p = M.LetVVar ("positions", v_pos, q_let_u) in
 151 prerr_endline ("### " ^ MQueryUtil.text_of_query q_let_p) ;
 152    execute_query q_let_p