(* Copyright (C) 2002-2004, 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/.
 *)

open Printf

module DB = Dbi_mysql

let debug = true
let debug_print s = if debug then prerr_endline s
let _ = Http_common.debug := false

exception Chat_unfinished
exception Unbound_identifier of string
exception Invalid_action of string  (* invalid action for "/search" method *)

let daemon_name = "Moogle"
let configuration_file = "/projects/helm/etc/moogle.conf.xml" 

let expression_tag_RE = Pcre.regexp "@EXPRESSION@"
let action_tag_RE = Pcre.regexp "@ACTION@"
let advanced_tag_RE = Pcre.regexp "@ADVANCED@"
let advanced_checked_RE = Pcre.regexp "@ADVANCED_CHECKED@"
let simple_checked_RE = Pcre.regexp "@SIMPLE_CHECKED@"
let title_tag_RE = Pcre.regexp "@TITLE@"
let no_choices_tag_RE = Pcre.regexp "@NO_CHOICES@"
let current_choices_tag_RE = Pcre.regexp "@CURRENT_CHOICES@"
let choices_tag_RE = Pcre.regexp "@CHOICES@"
let msg_tag_RE = Pcre.regexp "@MSG@"
let id_to_uris_RE = Pcre.regexp "@ID_TO_URIS@"
let id_RE = Pcre.regexp "@ID@"
let iden_tag_RE = Pcre.regexp "@IDEN@"
let interpretations_RE = Pcre.regexp "@INTERPRETATIONS@"
let interpretations_labels_RE = Pcre.regexp "@INTERPRETATIONS_LABELS@"
let results_RE = Pcre.regexp "@RESULTS@"
let new_aliases_RE = Pcre.regexp "@NEW_ALIASES@"
let search_engine_url_RE = Pcre.regexp "@SEARCH_ENGINE_URL@"

  (* First of all we load the configuration *)
let _ = Helm_registry.load_from configuration_file
let port = Helm_registry.get_int "search_engine.port"
let pages_dir = Helm_registry.get "search_engine.html_dir"

let interactive_interpretation_choice_TPL = pages_dir ^ "/moogle_chat2.html"
let moogle_TPL = pages_dir ^ "/moogle.html"

let my_own_url =
 let ic = Unix.open_process_in "hostname -f" in
 let hostname = input_line ic in
 ignore (Unix.close_process_in ic);
 sprintf "http://%s:%d" hostname port

let bad_request body outchan =
  Http_daemon.respond_error ~code:(`Status (`Client_error `Bad_request)) ~body
    outchan

  (** chain application of Pcre substitutions *)
let rec apply_substs substs line =
  match substs with
  | [] -> line
  | (rex, templ) :: rest -> apply_substs rest (Pcre.replace ~rex ~templ line)
  (** fold like function on files *)
let fold_file f init fname =
  let inchan = open_in fname in
  let rec fold_lines' value =
    try 
      let line = input_line inchan in 
      fold_lines' (f value line)
    with End_of_file -> value
  in
  let res = (try fold_lines' init with e -> (close_in inchan; raise e)) in
  close_in inchan;
  res
  (** iter like function on files *)
let iter_file f = fold_file (fun _ line -> f line) ()
let javascript_quote s =
 let rex = Pcre.regexp "'" in
 let rex' = Pcre.regexp "\"" in
  Pcre.replace ~rex ~templ:"\\'"
   (Pcre.replace ~rex:rex' ~templ:"\\\"" s)
let string_tail s =
  let len = String.length s in
  String.sub s 1 (len-1)

let add_param_substs params =
  List.map
    (fun (key,value) ->
      let key' = (Pcre.extract ~pat:"param\\.(.*)" key).(1) in
      Pcre.regexp ("@" ^ key' ^ "@"), value)
    (List.filter
      (fun ((key,_) as p) -> Pcre.pmatch ~pat:"^param\\." key)
      params)

let send_results results
  ?(id_to_uris = CicTextualParser2.EnvironmentP3.of_string "") 
   (req: Http_types.request) outchan
  =
  Http_daemon.send_basic_headers ~code:(`Code 200) outchan ;
  Http_daemon.send_header "Content-Type" "text/xml" outchan;
  Http_daemon.send_CRLF outchan ;
  let results_string =
    match results with
    | `Results r -> MooglePp.theory_of_result req r
    | `Error msg -> msg
  in
  let subst =
    (search_engine_url_RE, my_own_url) ::
    (results_RE, results_string) ::
    (advanced_tag_RE, req#param "advanced") ::
    (expression_tag_RE, req#param "expression") ::
    add_param_substs req#params @
    (if req#param "advanced" = "no" then
      [ simple_checked_RE, "checked='true'";
        advanced_checked_RE, "" ]
    else
      [ simple_checked_RE, "";
        advanced_checked_RE, "checked='true'" ])
  in
  iter_file
    (fun line ->
      let new_aliases =
        CicTextualParser2.EnvironmentP3.to_string id_to_uris
      in
      let processed_line =
        apply_substs
          (* CSC: Bug here: this is a string, not an array! *)
          ((new_aliases_RE, "'" ^ javascript_quote new_aliases ^ "'")::subst) 
          line
      in
      output_string outchan (processed_line ^ "\n"))
    moogle_TPL

let exec_action dbh (req: Http_types.request) outchan =
  let term_str = req#param "expression" in
  let (context, metasenv) = ([], []) in
  let id_to_uris_raw = 
    try req#param "aliases" 
    with Http_types.Param_not_found _ -> ""
  in
  let parse_interpretation_choices choices =
    List.map int_of_string (Pcre.split ~pat:" " choices) in
  let parse_choices choices_raw =
    let choices = Pcre.split ~pat:";" choices_raw in
      List.fold_left
        (fun f x ->
           match Pcre.split ~pat:"\\s" x with
             | ""::id::tail
             | id::tail when id<>"" ->
                 (fun id' ->
                    if id = id' then
                      Some (List.map (fun u -> Netencoding.Url.decode u) tail)
                    else
                      f id')
             | _ -> failwith "Can't parse choices")
        (fun _ -> None)
        choices
  in
  let id_to_uris = CicTextualParser2.EnvironmentP3.of_string id_to_uris_raw in
  let id_to_choices =
    try
      parse_choices (req#param "choices")
    with Http_types.Param_not_found _ -> (fun _ -> None)
  in
  let interpretation_choices =
    try
      let choices_raw = req#param "interpretation_choices" in
      if choices_raw = "" then None 
      else Some (parse_interpretation_choices choices_raw)
    with Http_types.Param_not_found _ -> None
  in 
  let module Chat: DisambiguateTypes.Callbacks =
    struct
      let interactive_user_uri_choice ~selection_mode ?ok
        ?enable_button_for_non_vars ~(title: string) ~(msg: string)
        ~(id: string) (choices: string list)
      =
        match id_to_choices id with
        | Some choices -> choices
        | None -> assert false

      let interactive_interpretation_choice interpretations =
        match interpretation_choices with
        | Some l -> l
        | None ->
            let html_interpretations =
              MooglePp.html_of_interpretations interpretations
            in
            Http_daemon.send_basic_headers ~code:(`Code 200) outchan ;
            Http_daemon.send_CRLF outchan ;
            iter_file
              (fun line ->
                 let processed_line =
                   apply_substs
                     [advanced_tag_RE, req#param "advanced";
                      interpretations_RE, html_interpretations;
                      current_choices_tag_RE, req#param "choices";
                      expression_tag_RE, req#param "expression";
                      action_tag_RE, string_tail req#path ]
                      line
                 in
                 output_string outchan (processed_line ^ "\n"))
              interactive_interpretation_choice_TPL;
            raise Chat_unfinished

      let input_or_locate_uri ~title ?id () =
        match id with
        | Some id -> raise (Unbound_identifier id)
        | None -> assert false
    end
  in
  let module Disambiguate' = Disambiguate.Make(Chat) in
  let ast = CicTextualParser2.parse_term (Stream.of_string term_str) in
  let (id_to_uris, metasenv, term) =
    match
      Disambiguate'.disambiguate_term dbh context metasenv ast id_to_uris
    with
    | [id_to_uris,metasenv,term] -> id_to_uris,metasenv,term
    | _ -> assert false
  in
  let uris =
    match req#path with
    | "/match" -> MetadataQuery.match_term ~dbh term
    | "/hint" ->
        let status = ProofEngineTypes.initial_status term metasenv in
        let intros = PrimitiveTactics.intros_tac () in
        let subgoals = ProofEngineTypes.apply_tactic intros status in
        (match subgoals with
        | proof, [goal] ->
            let (uri,metasenv,bo,ty) = proof in
            List.map fst (MetadataQuery.hint ~dbh (proof, goal))
        | _ -> assert false)
    | "/elim" ->
        let uri =
          match term with
          | Cic.MutInd (uri, typeno, _) ->
              UriManager.string_of_uriref (uri, [typeno])
          | _ -> assert false
        in
        MetadataQuery.elim ~dbh uri
    | _ -> assert false
  in
  send_results ~id_to_uris (`Results uris) req outchan

let callback dbh (req: Http_types.request) outchan =
  try
    debug_print (sprintf "Received request: %s" req#path);
    (match req#path with
    | "/getpage" ->
          (* TODO implement "is_permitted" *)
        (let is_permitted _ = true in
        let remove_fragment uri = Pcre.replace ~pat:"#.*" uri in
        let page = remove_fragment (req#param "url") in
        let preprocess =
          (try
            bool_of_string (req#param "preprocess")
          with Invalid_argument _ | Http_types.Param_not_found _ -> false)
        in
        (match page with
        | page when is_permitted page ->
            (let fname = sprintf "%s/%s" pages_dir (remove_fragment page) in
            Http_daemon.send_basic_headers ~code:(`Code 200) outchan;
            Http_daemon.send_header "Content-Type" "text/html" outchan;
            Http_daemon.send_CRLF outchan;
            if preprocess then begin
              iter_file
                (fun line ->
                  output_string outchan
                    ((apply_substs
                       ((search_engine_url_RE, my_own_url) ::
                        (advanced_tag_RE, "no") ::
                        (results_RE, "") ::
                        add_param_substs req#params)
                       line) ^
                    "\n"))
                fname
            end else
              Http_daemon.send_file ~src:(Http_types.FileSrc fname) outchan)
        | page -> Http_daemon.respond_forbidden ~url:page outchan))
    | "/help" -> Http_daemon.respond ~body:daemon_name outchan
    | "/locate" ->
        let initial_expression =
          try req#param "expression" with Http_types.Param_not_found _ -> ""
        in
        let expression =
          Pcre.replace ~pat:"\\s*$"
            (Pcre.replace ~pat:"^\\s*" initial_expression)
        in
        if expression = "" then
          send_results (`Results []) req outchan
        else
          let results = MetadataQuery.locate ~dbh expression in
          send_results (`Results results) req outchan
    | "/hint"
    | "/elim"
    | "/match" -> exec_action dbh req outchan
    | invalid_request ->
        Http_daemon.respond_error ~code:(`Status (`Client_error `Bad_request))
          outchan);
    debug_print (sprintf "%s done!" req#path)
  with
  | Chat_unfinished -> ()
  | Http_types.Param_not_found attr_name ->
      bad_request (sprintf "Parameter '%s' is missing" attr_name) outchan
  | CicTextualParser2.Parse_error msg ->
      send_results (`Error (MooglePp.pp_error "Parse_error" msg)) req outchan
  | Unbound_identifier id ->
      send_results (`Error (MooglePp.pp_error "Unbound identifier" id)) req
        outchan
  | exn ->
      let exn_string = Printexc.to_string exn in
      debug_print exn_string;
      let msg = MooglePp.pp_error "Uncaught exception" exn_string in
      send_results (`Error msg) req outchan

let _ =
  printf "%s started and listening on port %d\n" daemon_name port;
  printf "Current directory is %s\n" (Sys.getcwd ());
  printf "HTML directory is %s\n" pages_dir;
  flush stdout;
  Unix.putenv "http_proxy" "";
  let dbh =
    new DB.connection ~host:(Helm_registry.get "db.host")
      ~user:(Helm_registry.get "db.user") (Helm_registry.get "db.database")
  in
  Http_daemon.start' ~port (callback dbh);
  printf "%s is terminating, bye!\n" daemon_name