helm/searchEngine/searchEngine.ml

   1 (* Copyright (C) 2002, 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 let debug = true;;
  27 let debug_print s = if debug then prerr_endline s;;
  28 Http_common.debug := true;;
  29
  30 open Printf;;
  31
  32 let postgresConnectionString =
  33  try
  34   Sys.getenv "POSTGRESQL_CONNECTION_STRING"
  35  with
  36   Not_found -> "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm"
  37 ;;
  38
  39 let daemon_name = "Search Engine";;
  40 let default_port = 58085;;
  41 let port_env_var = "SEARCH_ENGINE_PORT";;
  42
  43 let pages_dir = "html";; (* relative to searchEngine's document root *)
  44 let interactive_user_uri_choice_TPL = pages_dir ^ "/templateambigpdq1.html";;
  45 let interactive_interpretation_choice_TPL = pages_dir ^ "/templateambigpdq2.html";;
  46 let final_results_TPL = pages_dir ^ "/templateambigpdq3.html";;
  47
  48 exception Chat_unfinished
  49
  50   (** pretty print a MathQL query result to a string *)
  51 let text_of_result result sep =
  52  let res_string = ref "" in
  53   let app = function s -> res_string := !res_string ^ s in
  54    MQueryUtil.text_of_result app result sep ;
  55    !res_string
  56 ;;
  57
  58   (** chain application of Pcre substitutions *)
  59 let rec apply_substs substs line =
  60   match substs with
  61   | [] -> line
  62   | (rex, templ) :: rest -> apply_substs rest (Pcre.replace ~rex ~templ line)
  63   (** fold like function on files *)
  64 let fold_file f init fname =
  65   let inchan = open_in fname in
  66   let rec fold_lines' value =
  67     try
  68       let line = input_line inchan in
  69       fold_lines' (f value line)
  70     with End_of_file -> value
  71   in
  72   let res = (try fold_lines' init with e -> (close_in inchan; raise e)) in
  73   close_in inchan;
  74   res
  75   (** iter like function on files *)
  76 let iter_file f = fold_file (fun _ line -> f line) ()
  77
  78 let (title_tag_RE, choices_tag_RE, msg_tag_RE, id_to_uris_RE, id_RE,
  79     interpretations_RE, interpretations_labels_RE, results_RE, new_aliases_RE) =
  80   (Pcre.regexp "@TITLE@", Pcre.regexp "@CHOICES@", Pcre.regexp "@MSG@",
  81   Pcre.regexp "@ID_TO_URIS@", Pcre.regexp "@ID@",
  82   Pcre.regexp "@INTERPRETATIONS@", Pcre.regexp "@INTERPRETATIONS_LABELS@",
  83   Pcre.regexp "@RESULTS@", Pcre.regexp "@NEW_ALIASES@")
  84
  85 let port =
  86   try
  87     int_of_string (Sys.getenv port_env_var)
  88   with
  89   | Not_found -> default_port
  90   | Failure "int_of_string" ->
  91       prerr_endline "Warning: invalid port, reverting to default";
  92       default_port
  93 in
  94 let pp_result result =
  95  let res_string = text_of_result result "\n" in
  96   (sprintf "<html>\n<head>\n</head>\n<body>\n<pre>%s</pre>\n</body>\n</html>"
  97     res_string)
  98 in
  99 let pp_error = sprintf "<html><body><h1>Error: %s</h1></body></html>" in
 100 let bad_request body outchan =
 101   Http_daemon.respond_error ~status:(`Client_error `Bad_request) ~body outchan
 102 in
 103 let contype = "Content-Type", "text/html" in
 104
 105 (* SEARCH ENGINE functions *)
 106
 107 let refine_constraints (x, y, z) = (x, y, z), (Some x, Some y, Some z) in
 108
 109 (* HTTP DAEMON CALLBACK *)
 110
 111 let callback (req: Http_types.request) outchan =
 112   try
 113     debug_print (sprintf "Received request: %s" req#path);
 114     (match req#path with
 115     | "/execute" ->
 116         let query_string = req#param "query" in
 117         let lexbuf = Lexing.from_string query_string in
 118         let query = MQueryUtil.query_of_text lexbuf in
 119         let result = MQueryGenerator.execute_query query in
 120         let result_string = text_of_result result "\n" in
 121         Http_daemon.respond
 122           ~body:
 123             (sprintf "<html><body><pre>%s</pre></body></html>" result_string)
 124           ~headers:[contype] outchan
 125     | "/locate" ->
 126         let id = req#param "id" in
 127         let result = MQueryGenerator.locate id in
 128         Http_daemon.respond ~headers:[contype] ~body:(pp_result result) outchan
 129     | "/getpage" ->
 130         (* TODO implement "is_permitted" *)
 131         (let is_permitted _ = true in
 132         let remove_fragment uri = Pcre.replace ~pat:"#.*" uri in
 133         let page = remove_fragment (req#param "url") in
 134         match page with
 135         | page when is_permitted page ->
 136             Http_daemon.respond_file
 137               ~fname:(sprintf "%s/%s" pages_dir (remove_fragment page)) outchan
 138         | page -> Http_daemon.respond_forbidden ~url:page outchan)
 139     | "/searchPattern" ->
 140         let term_string = req#param "term" in
 141         let lexbuf = Lexing.from_string term_string in
 142         let (context, metasenv) = ([], []) in
 143         let (dom, mk_metasenv_and_expr) =
 144           CicTextualParserContext.main
 145             ~context ~metasenv CicTextualLexer.token lexbuf
 146         in
 147         let id_to_uris_raw = req#param "aliases" in
 148         let tokens = Pcre.split ~pat:"\\s" id_to_uris_raw in
 149         let rec parse_tokens keys lookup = function (* TODO spostarla fuori *)
 150           | [] -> keys, lookup
 151           | "alias" :: key :: value :: rest ->
 152               let key' = CicTextualParser0.Id key in
 153                parse_tokens
 154                  (key'::keys)
 155                  (fun id ->
 156                    if id = key' then
 157                      Some
 158                       (CicTextualParser0.Uri (MQueryMisc.cic_textual_parser_uri_of_string value))
 159                    else lookup id)
 160                  rest
 161           | _ -> failwith "Can't parse aliases"
 162         in
 163         let parse_choices choices_raw =
 164           let choices = Pcre.split ~pat:";" choices_raw in
 165           List.fold_left
 166             (fun f x ->
 167               match Pcre.split ~pat:"\\s" x with
 168               | ""::id::tail
 169               | id::tail when id<>"" ->
 170                   (fun id' ->
 171                     if id = id' then
 172                       Some (List.map (fun u -> Netencoding.Url.decode u) tail)
 173                     else
 174                       f id')
 175               | _ -> failwith "Can't parse choices")
 176             (fun _ -> None)
 177             choices
 178         in
 179         let (id_to_uris : Disambiguate.domain_and_interpretation) =
 180          parse_tokens [] (fun _ -> None) tokens in
 181         let id_to_choices =
 182           try
 183             let choices_raw = req#param "choices" in
 184             parse_choices choices_raw
 185           with Http_types.Param_not_found _ -> (fun _ -> None)
 186         in
 187         let module Chat: Disambiguate.Callbacks =
 188           struct
 189
 190             let get_metasenv () =
 191              !CicTextualParser0.metasenv
 192
 193             let set_metasenv metasenv =
 194               CicTextualParser0.metasenv := metasenv
 195
 196             let output_html = prerr_endline
 197
 198             let interactive_user_uri_choice
 199               ~selection_mode ?ok
 200               ?enable_button_for_non_vars ~(title: string) ~(msg: string)
 201               ~(id: string) (choices: string list)
 202               =
 203                 (match id_to_choices id with
 204                 | Some choices -> choices
 205                 | None ->
 206                   let msg = Pcre.replace ~pat:"\"" ~templ:"\\\"" msg in
 207                   (match selection_mode with
 208                   | `SINGLE -> assert false
 209                   | `EXTENDED ->
 210                       iter_file
 211                         (fun line ->
 212                           let formatted_choices =
 213                             String.concat ","
 214                               (List.map (fun uri -> sprintf "\"%s\"" uri) choices)
 215                           in
 216                           let processed_line =
 217                             apply_substs
 218                               [title_tag_RE, title;
 219                                choices_tag_RE, formatted_choices;
 220                                msg_tag_RE, msg;
 221                                id_to_uris_RE, id_to_uris_raw;
 222                                id_RE, id]
 223                               line
 224                           in
 225                           output_string outchan processed_line)
 226                         interactive_user_uri_choice_TPL;
 227                       raise Chat_unfinished))
 228
 229             let interactive_interpretation_choice interpretations =
 230               let html_interpretations_labels =
 231                 String.concat ", "
 232                   (List.map
 233                     (fun l ->
 234                       "\"" ^
 235                       (String.concat "<br />"
 236                         (List.map
 237                           (fun (id, value) ->
 238                             (sprintf "alias %s %s" id value))
 239                           l)) ^
 240                       "\"")
 241                   interpretations)
 242               in
 243               let html_interpretations =
 244                 String.concat ", "
 245                   (List.map
 246                     (fun l ->
 247                       "\"" ^
 248                       (String.concat " "
 249                         (List.map
 250                           (fun (id, value) ->
 251                             (sprintf "alias %s %s"
 252                               id
 253                               (MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format'
 254                                 value)))
 255                           l)) ^
 256                       "\"")
 257                     interpretations)
 258               in
 259               iter_file
 260                 (fun line ->
 261                   let processed_line =
 262                     apply_substs
 263                       [interpretations_RE, html_interpretations;
 264                        interpretations_labels_RE, html_interpretations_labels]
 265                       line
 266                   in
 267                   output_string outchan processed_line)
 268                 interactive_interpretation_choice_TPL;
 269               raise Chat_unfinished
 270
 271             let input_or_locate_uri ~title =
 272               UriManager.uri_of_string "cic:/Coq/Init/DataTypes/nat_ind.con"
 273
 274           end
 275         in
 276         let module Disambiguate' = Disambiguate.Make (Chat) in
 277         let (id_to_uris', metasenv', term') =
 278           Disambiguate'.disambiguate_input
 279             context metasenv dom mk_metasenv_and_expr id_to_uris
 280         in
 281         (match metasenv' with
 282         | [] ->
 283             let must = MQueryLevels2.get_constraints term' in
 284             let must',only = refine_constraints must in
 285             let results = MQueryGenerator.searchPattern must' only in
 286             iter_file
 287               (fun line ->
 288                 let new_aliases =
 289                   match id_to_uris' with
 290                   | (domain, f) ->
 291                       String.concat ", "
 292                         (List.map
 293                           (fun name ->
 294                             sprintf "\"alias %s cic:%s\""
 295                               (match name with
 296                                   CicTextualParser0.Id name -> name
 297                                 | _ -> assert false (*CSC: completare *))
 298                               (match f name with
 299                               | None -> assert false
 300                               | Some (CicTextualParser0.Uri t) ->
 301                                   MQueryMisc.string_of_cic_textual_parser_uri
 302                                     t
 303                               | _ -> assert false (*CSC: completare *)))
 304                           domain)
 305                 in
 306                 let processed_line =
 307                   apply_substs
 308                     [results_RE, text_of_result results "\n";
 309                      new_aliases_RE, new_aliases]
 310                     line
 311                 in
 312                 output_string outchan processed_line)
 313               final_results_TPL
 314         | _ -> (* unable to instantiate some implicit variable *)
 315             Http_daemon.respond
 316               ~headers:[contype]
 317               ~body:"some implicit variables are still unistantiated :-("
 318               outchan)
 319
 320     | invalid_request ->
 321         Http_daemon.respond_error ~status:(`Client_error `Bad_request) outchan);
 322     debug_print (sprintf "%s done!" req#path)
 323   with
 324   | Chat_unfinished -> prerr_endline "Chat unfinished, Try again!"
 325   | Http_types.Param_not_found attr_name ->
 326       bad_request (sprintf "Parameter '%s' is missing" attr_name) outchan
 327   | exc ->
 328       Http_daemon.respond
 329         ~body:(pp_error ("Uncaught exception: " ^ (Printexc.to_string exc)))
 330         outchan
 331 in
 332 printf "%s started and listening on port %d\n" daemon_name port;
 333 printf "current directory is %s\n" (Sys.getcwd ());
 334 flush stdout;
 335 Unix.putenv "http_proxy" "";
 336 Mqint.set_database Mqint.postgres_db;
 337 Mqint.init postgresConnectionString;
 338 Http_daemon.start' ~port callback;
 339 Mqint.close ();
 340 printf "%s is terminating, bye!\n" daemon_name
 341