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               parse_tokens
 153                 (key::keys)
 154                 (fun id ->
 155                   if id = key then
 156                     Some (MQueryMisc.cic_textual_parser_uri_of_string value)
 157                   else lookup id)
 158                 rest
 159           | _ -> failwith "Can't parse aliases"
 160         in
 161         let parse_choices choices_raw =
 162           let choices = Pcre.split ~pat:";" choices_raw in
 163           List.fold_left
 164             (fun f x ->
 165               match Pcre.split ~pat:"\\s" x with
 166               | ""::id::tail
 167               | id::tail when id<>"" ->
 168                   (fun id' ->
 169                     if id = id' then
 170                       Some (List.map (fun u -> Netencoding.Url.decode u) tail)
 171                     else
 172                       f id')
 173               | _ -> failwith "Can't parse choices")
 174             (fun _ -> None)
 175             choices
 176         in
 177         let id_to_uris = parse_tokens [] (fun _ -> None) tokens in
 178         let id_to_choices =
 179           try
 180             let choices_raw = req#param "choices" in
 181             parse_choices choices_raw
 182           with Http_types.Param_not_found _ -> (fun _ -> None)
 183         in
 184         let module Chat: Disambiguate.Callbacks =
 185           struct
 186
 187             let output_html = prerr_endline
 188
 189             let interactive_user_uri_choice
 190               ~selection_mode ?ok
 191               ?enable_button_for_non_vars ~(title: string) ~(msg: string)
 192               ~(id: string) (choices: string list)
 193               =
 194                 (match id_to_choices id with
 195                 | Some choices -> choices
 196                 | None ->
 197                   let msg = Pcre.replace ~pat:"\"" ~templ:"\\\"" msg in
 198                   (match selection_mode with
 199                   | `SINGLE -> assert false
 200                   | `EXTENDED ->
 201                       iter_file
 202                         (fun line ->
 203                           let formatted_choices =
 204                             String.concat ","
 205                               (List.map (fun uri -> sprintf "\"%s\"" uri) choices)
 206                           in
 207                           let processed_line =
 208                             apply_substs
 209                               [title_tag_RE, title;
 210                                choices_tag_RE, formatted_choices;
 211                                msg_tag_RE, msg;
 212                                id_to_uris_RE, id_to_uris_raw;
 213                                id_RE, id]
 214                               line
 215                           in
 216                           output_string outchan processed_line)
 217                         interactive_user_uri_choice_TPL;
 218                       raise Chat_unfinished))
 219
 220             let interactive_interpretation_choice interpretations =
 221               let html_interpretations_labels =
 222                 String.concat ", "
 223                   (List.map
 224                     (fun l ->
 225                       "\"" ^
 226                       (String.concat "<br />"
 227                         (List.map
 228                           (fun (id, value) ->
 229                             (sprintf "alias %s %s" id value))
 230                           l)) ^
 231                       "\"")
 232                   interpretations)
 233               in
 234               let html_interpretations =
 235                 String.concat ", "
 236                   (List.map
 237                     (fun l ->
 238                       "\"" ^
 239                       (String.concat " "
 240                         (List.map
 241                           (fun (id, value) ->
 242                             (sprintf "alias %s %s"
 243                               id
 244                               (MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format'
 245                                 value)))
 246                           l)) ^
 247                       "\"")
 248                     interpretations)
 249               in
 250               iter_file
 251                 (fun line ->
 252                   let processed_line =
 253                     apply_substs
 254                       [interpretations_RE, html_interpretations;
 255                        interpretations_labels_RE, html_interpretations_labels]
 256                       line
 257                   in
 258                   output_string outchan processed_line)
 259                 interactive_interpretation_choice_TPL;
 260               raise Chat_unfinished
 261
 262             let input_or_locate_uri ~title =
 263               UriManager.uri_of_string "cic:/Coq/Init/DataTypes/nat_ind.con"
 264
 265           end
 266         in
 267         let module Disambiguate' = Disambiguate.Make (Chat) in
 268         let (id_to_uris', metasenv', term') =
 269           Disambiguate'.disambiguate_input
 270             context metasenv dom mk_metasenv_and_expr id_to_uris
 271         in
 272         (match metasenv' with
 273         | [] ->
 274             let must = MQueryLevels2.get_constraints term' in
 275             let must',only = refine_constraints must in
 276             let results = MQueryGenerator.searchPattern must' only in
 277             iter_file
 278               (fun line ->
 279                 let new_aliases =
 280                   match id_to_uris' with
 281                   | (domain, f) ->
 282                       String.concat ", "
 283                         (List.map
 284                           (fun name ->
 285                             sprintf "\"alias %s cic:%s\""
 286                               name
 287                               (match f name with
 288                               | None -> assert false
 289                               | Some t ->
 290                                   MQueryMisc.string_of_cic_textual_parser_uri
 291                                     t))
 292                           domain)
 293                 in
 294                 let processed_line =
 295                   apply_substs
 296                     [results_RE, text_of_result results "\n";
 297                      new_aliases_RE, new_aliases]
 298                     line
 299                 in
 300                 output_string outchan processed_line)
 301               final_results_TPL
 302         | _ -> (* unable to instantiate some implicit variable *)
 303             Http_daemon.respond
 304               ~headers:[contype]
 305               ~body:"some implicit variables are still unistantiated :-("
 306               outchan)
 307
 308     | invalid_request ->
 309         Http_daemon.respond_error ~status:(`Client_error `Bad_request) outchan);
 310     debug_print (sprintf "%s done!" req#path)
 311   with
 312   | Chat_unfinished -> prerr_endline "Chat unfinished, Try again!"
 313   | Http_types.Param_not_found attr_name ->
 314       bad_request (sprintf "Parameter '%s' is missing" attr_name) outchan
 315   | exc ->
 316       Http_daemon.respond
 317         ~body:(pp_error ("Uncaught exception: " ^ (Printexc.to_string exc)))
 318         outchan
 319 in
 320 printf "%s started and listening on port %d\n" daemon_name port;
 321 printf "current directory is %s\n" (Sys.getcwd ());
 322 flush stdout;
 323 Unix.putenv "http_proxy" "";
 324 Mqint.set_database Mqint.postgres_db;
 325 Mqint.init postgresConnectionString;
 326 Http_daemon.start' ~port callback;
 327 Mqint.close ();
 328 printf "%s is terminating, bye!\n" daemon_name
 329