(* Copyright (C) 2000, HELM Team.
 * 
 * This file is part of HELM, an Hypertextual, Electronic
 * Library of Mathematics, developed at the Computer Science
 * Department, University of Bologna, Italy.
 * 
 * HELM is free software; you can redistribute it and/or
 * modify it under the terms of the GNU General Public License
 * as published by the Free Software Foundation; either version 2
 * of the License, or (at your option) any later version.
 * 
 * HELM is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with HELM; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
 * MA  02111-1307, USA.
 * 
 * For details, see the HELM World-Wide-Web page,
 * http://cs.unibo.it/helm/.
 *)

(******************************************************************************)
(*                                                                            *)
(*                               PROJECT HELM                                 *)
(*                                                                            *)
(*                     Ferruccio Guidi <fguidi@cs.unibo.it>                   *)
(*                                 30/04/2002                                 *)
(*                                                                            *)
(*                                                                            *)
(******************************************************************************)

(* Query issuing functions **************************************************)

exception Discard  

let nl = " <p>\n"

let query_num = ref 1

let log_file = ref ""

let confirm_query = ref (fun _ -> true)

let info = ref []

let set_log_file f = 
   log_file := f

let set_confirm_query f =
   confirm_query := f

let get_query_info () = ! info

let execute_query query =
   let module Util = MQueryUtil in
   let mode = [Open_wronly; Open_append; Open_creat; Open_text] in
   let perm = 64 * 6 + 8 * 6 + 4 in
   let time () =
      let lt = Unix.localtime (Unix.time ()) in
      "NEW LOG: " ^
      string_of_int (lt.Unix.tm_mon + 1) ^ "-" ^
      string_of_int (lt.Unix.tm_mday + 1) ^ "-" ^
      string_of_int (lt.Unix.tm_year + 1900) ^ " " ^
      string_of_int (lt.Unix.tm_hour) ^ ":" ^
      string_of_int (lt.Unix.tm_min) ^ ":" ^
      string_of_int (lt.Unix.tm_sec) 
   in
   let log q r = 
      let och = open_out_gen mode perm ! log_file in
      if ! query_num = 1 then output_string och (time () ^ nl);
      let str =
       "Query: " ^ string_of_int ! query_num ^ nl ^ Util.text_of_query q ^ nl ^ 
       "Result:" ^ nl ^ Util.text_of_result r nl in
      output_string och str; 
      flush och 
   in
   let execute q =
      let r = Mqint.execute q in    
      if ! log_file <> "" then log q r; 
      info := string_of_int ! query_num :: ! info;
      incr query_num;
      r
   in 
   if ! confirm_query query then execute query else raise Discard
                          
(* Query building functions  ************************************************)   

let locate s =
   let module M = MathQL in
   let q =
    M.Ref (M.Property true M.RefineExact ("objectName", []) (M.Const [s]))
   in
    execute_query q

let searchPattern e c t level =
   let module M = MathQL in
   let module L = MQueryLevels in
   let in_path s = (s, []) in
   let assign v p = (in_path v, in_path p) in 
   let v_pos = M.Const ["MainConclusion"; "InConclusion"] in
   let q_where =
    M.Sub
     (M.RefOf
       (M.Select
         ("uri", 
           M.Relation
            (false, M.RefineExact, in_path "refObj", M.RVar "uri0", 
	     [assign "pos" "position"]),
           M.Ex ["uri"]
            (M.Meet (M.VVar "positions", M.Record ("uri", in_path "pos")))
	  )
       ),
       M.VVar "universe"
     ) in
   let uri_of_entry (r, b, v) = r in
   let rec restrict level = function
      | []                -> []
      | (u, b, v) :: tail ->
         if v <= level then (u, b, v) :: restrict level tail
         else restrict level tail
   in
   let build_select (r, b, v) =
    let pos = if b then "MainConclusion" else "InConclusion" in
      M.Select
       ("uri", 
        M.Relation (false, M.RefineExact, ("backPointer", []),
	            M.Ref (M.Const [r]), [assign "pos" "position"]),
        M.Ex ["uri"] (M.Sub (M.Const [pos], M.Record ("uri", in_path "pos")))) in 
   let rec build_intersect = function
      | []       -> M.Pattern (M.Const ["[.]*"])
      | [hd]     -> build_select hd
      | hd :: tl -> M.Intersect (build_select hd, build_intersect tl)
   in
   let levels = L.levels_of_term e c t in
   let rest = restrict level levels in
   info := [string_of_int (List.length rest)];
   let q_in = build_intersect rest in
   let q_select = M.Select ("uri0", q_in, q_where) in
   let universe = M.Const (List.map uri_of_entry levels) in
   let q_let_u = M.LetVVar ("universe", universe, q_select) in
   let q_let_p = M.LetVVar ("positions", v_pos, q_let_u) in
   execute_query q_let_p