(* Copyright (C) 2002-2005, 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

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 *)

  (** raised by elim when a MutInd is required but not found *)
exception Not_a_MutInd

let daemon_name = "Whelp"
let configuration_file = "/projects/helm/etc/whelp.conf.xml"

let placeholders = [
  "ACTION"; "ADVANCED"; "ADVANCED_CHECKED"; "CHOICES"; "CURRENT_CHOICES";
  "EXPRESSION"; "ID"; "IDEN"; "ID_TO_URIS"; "INTERPRETATIONS";
  "INTERPRETATIONS_LABELS"; "MSG"; "NEW_ALIASES"; "NEXT_LINK"; "NO_CHOICES";
  "PAGE"; "PAGES"; "PAGELIST"; "PREV_LINK"; "QUERY_KIND"; "QUERY_SUMMARY"; "RESULTS";
  "SEARCH_ENGINE_URL"; "SIMPLE_CHECKED"; "TITLE";
]

let tag =
  let regexps = Hashtbl.create 25 in
  List.iter
    (fun tag -> Hashtbl.add regexps tag (Pcre.regexp (sprintf "@%s@" tag)))
    placeholders;
  fun name ->
    try
      Hashtbl.find regexps name
    with Not_found -> assert false

  (* 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 moogle_TPL = pages_dir ^ "/moogle.html"
let choices_TPL = pages_dir ^ "/moogle_chat.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 _ = Helm_registry.set "search_engine.my_own_url" my_own_url

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 nonvar uri =
  let s = UriManager.string_of_uri uri in
  let len = String.length s in
  let suffix = String.sub s (len-4) 4 in
  not (suffix  = ".var")

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 page_RE = Pcre.regexp "&param\\.page=\\d+"
let identifier_RE = Pcre.regexp "^\\s*(\\w|')+\\s*$"
let qualified_mutind_RE =
 Pcre.regexp "^\\s*cic:(/(\\w|')+)+\\.ind#xpointer\\(1/\\d+\\)\\s*$"

let query_kind_of_req (req: Http_types.request) =
  match req#path with
  | "/match" -> "Match"
  | "/hint" -> "Hint"
  | "/locate" -> "Locate"
  | "/elim" -> "Elim"
  | "/instance" -> "Instance"
  | _ -> ""

  (* given a uri with a query part in input try to find in it a string
   * "&param_name=..." (where param_name is given). If found its value will be
   * set to param_value. If not, a trailing "&param_name=param_value" (where
   * both are given) is added to the input string *)
let patch_param param_name param_value url =
  let rex = Pcre.regexp (sprintf "&%s=[^&]*" (Pcre.quote param_name)) in
  if Pcre.pmatch ~rex url then
    Pcre.replace ~rex ~templ:(sprintf "%s=%s" param_name param_value) url
  else
    sprintf "%s&%s=%s" url param_name param_value

  (** HTML encoding, e.g.: "<" -> "&lt;" *)
let html_encode = Netencoding.Html.encode_from_latin1

let fold_n_to_m f n m acc =
 let rec aux acc =
  function
     i when i <= m -> aux (f i acc) (i + 1)
   | _ -> acc
 in
  aux acc n

let send_results results
  ?(id_to_uris = DisambiguateTypes.empty_environment) 
   (req: Http_types.request) outchan
  =
  let query_kind = query_kind_of_req req in
  let interp = try req#param "interp" with Http_types.Param_not_found _ -> "" in
  let page_link anchor page =
    try
      let this = req#param "this" in
      let target =
        (patch_param "param.interp" interp
           (patch_param "param.page" (string_of_int page)
              this))
      in
      let target = Pcre.replace ~pat:"&" ~templ:"&amp;" target in
      sprintf "<a href=\"%s\">%s</a>" target anchor
    with Http_types.Param_not_found _ -> ""
  in
  Http_daemon.send_basic_headers ~code:(`Code 200) outchan ;
  Http_daemon.send_header "Content-Type" "text/xml" outchan;
  Http_daemon.send_CRLF outchan ;
  let subst =
    match results with
    | `Results results ->
        let page = try int_of_string (req#param "page") with _ -> 1 in
        let results_no = List.length results in
        let results_per_page =
          Helm_registry.get_int "search_engine.results_per_page"
        in
        let pages =
          if results_no mod results_per_page = 0 then
            results_no / results_per_page
          else
            results_no / results_per_page + 1
        in
        let pages = if pages = 0 then 1 else pages in
        let additional_pages = 3 in
        let (summary, results) = MooglePp.theory_of_result page results in
        [ tag "PAGE", string_of_int page;
          tag "PAGES", string_of_int pages ^ " Pages";
          tag "PAGELIST",
          (let inf = page - additional_pages in
           let sup = page + additional_pages in
           let superinf = inf - (sup - pages) in
           let supersup = sup + (1 - inf) in
           let n,m =
            if inf >= 1 && sup <= pages then
             inf,sup
            else if inf < 1 then
             1, (if supersup <= pages then supersup else pages)
            else (* sup > pages *)
             (if superinf >= 1 then superinf else 1),pages
           in
            fold_n_to_m
             (fun n acc -> acc ^ " " ^
                          (if n = page then string_of_int n
                           else page_link (string_of_int n) n))
             n m "");
          tag "PREV_LINK", (if page > 1 then page_link "Prev" (page-1) else "");
          tag "NEXT_LINK",
            (if page < pages then page_link "Next" (page+1) else "");
          tag "QUERY_KIND", query_kind;
          tag "QUERY_SUMMARY", summary;
          tag "RESULTS", results ]
    | `Error msg ->
        [ tag "PAGE", "1";
          tag "PAGES", "1 Page";
          tag "PAGELIST", "";
          tag "PREV_LINK", "";
          tag "NEXT_LINK", "";
          tag "QUERY_KIND", query_kind;
          tag "QUERY_SUMMARY", "error";
          tag "RESULTS", msg ]
  in
  let advanced =
    try
      req#param "advanced"
    with Http_types.Param_not_found _ -> "no"
  in
  let subst =
    (tag "SEARCH_ENGINE_URL", my_own_url) ::
    (tag "ADVANCED", advanced) ::
    (tag "EXPRESSION", html_encode (req#param "expression")) ::
    add_param_substs req#params @
    (if advanced = "no" then
      [ tag "SIMPLE_CHECKED", "checked='true'";
        tag "ADVANCED_CHECKED", "" ]
    else
      [ tag "SIMPLE_CHECKED", "";
        tag "ADVANCED_CHECKED", "checked='true'" ]) @
    subst
  in
  iter_file
    (fun line ->
      let new_aliases = DisambiguatePp.pp_environment id_to_uris in
      let processed_line =
        apply_substs
          (* CSC: Bug here: this is a string, not an array! *)
          ((tag "NEW_ALIASES", "'" ^ javascript_quote new_aliases ^ "'") ::
            subst) 
          line
      in
      output_string outchan (processed_line ^ "\n"))
    moogle_TPL

let exec_action dbd (req: Http_types.request) outchan =
  let term_str = req#param "expression" in
  try
    if req#path = "/elim" &&
     not (Pcre.pmatch ~rex:identifier_RE term_str ||
          Pcre.pmatch ~rex:qualified_mutind_RE term_str) then
      raise Not_a_MutInd;
    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 -> UriManager.uri_of_string
                          (Netencoding.Url.decode u)) 
                        tail)
                    else
                      f id')
             | _ -> failwith "Can't parse choices")
        (fun _ -> None)
        choices
    in
    let id_to_uris = DisambiguatePp.parse_environment 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: UriManager.uri list)
        =
          match id_to_choices id with
          | Some choices -> choices
          | None -> List.filter nonvar choices

        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 ;
              let advanced =
                try
                  req#param "advanced"
                with Http_types.Param_not_found _ -> "no"
              in
              let query_kind = query_kind_of_req req in
              iter_file
                (fun line ->
                   let processed_line =
                     apply_substs
                       [ tag "SEARCH_ENGINE_URL", my_own_url;
                         tag "ADVANCED", advanced;
                         tag "INTERPRETATIONS", html_interpretations;
                         tag "CURRENT_CHOICES", req#param "choices";
                         tag "EXPRESSION", html_encode (req#param "expression");
                         tag "QUERY_KIND", query_kind;
                         tag "QUERY_SUMMARY", "disambiguation";
                         tag "ACTION", string_tail req#path ]
                       line
                   in
                   output_string outchan (processed_line ^ "\n"))
                choices_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 = Grammar.Entry.parse CicNotationParser.term (Stream.of_string term_str) in
    let (id_to_uris, metasenv, term) =
      match
        Disambiguate'.disambiguate_term ~dbd ~context ~metasenv
          ~aliases:id_to_uris ast
      with
      | [id_to_uris,metasenv,term,_] -> id_to_uris,metasenv,term
      | _ -> assert false
    in
    let uris =
      match req#path with
      | "/match" -> MetadataQuery.match_term ~dbd term
      | "/instance" -> MetadataQuery.instance ~dbd 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.experimental_hint ~dbd (proof, goal))
          | _ -> assert false)
      | "/elim" ->
          let uri =
            match term with
            | Cic.MutInd (uri, typeno, _) ->
                UriManager.uri_of_uriref uri typeno None 
            | _ -> raise Not_a_MutInd
          in
          MetadataQuery.elim ~dbd uri
      | _ -> assert false
    in
    let uris = List.map UriManager.string_of_uri uris in
    send_results ~id_to_uris (`Results uris) req outchan
  with
  | Not_a_MutInd ->
      send_results (`Error (MooglePp.pp_error "Not an inductive type"
        ("elim requires as input an identifier corresponding to an inductive"
         ^ " type")))
        req outchan

let callback dbd (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 page = not (Pcre.pmatch ~pat:"/" page) in
        let page = req#param "url" in
        let fname = sprintf "%s/%s" pages_dir page 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 && Sys.file_exists fname ->
            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
                       ((tag "SEARCH_ENGINE_URL", my_own_url) ::
                        (tag "ADVANCED", "no") ::
                        (tag "RESULTS", "") ::
                        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 begin
          let results = MetadataQuery.locate ~dbd expression in
          let results = List.map UriManager.string_of_uri results in
          send_results (`Results results) req outchan
        end
    | "/hint"
    | "/elim"
    | "/instance"
    | "/match" -> exec_action dbd 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
  | CicNotationParser.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 restore_environment () =
  match
    Helm_registry.get_opt Helm_registry.string "search_engine.environment_dump"
  with
  | None -> ()
  | Some fname ->
      printf "Restoring Cic environment from %s ... " fname; flush stdout;
      let ic = open_in fname in
      CicEnvironment.restore_from_channel ic;
      close_in ic;
      printf "done!\n"; flush stdout

let read_notation () =
 CicNotation.load_notation (Helm_registry.get "search_engine.notations");
 CicNotation.load_notation (Helm_registry.get "search_engine.interpretations")

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 dbd =
    Mysql.quick_connect
      ~host:(Helm_registry.get "db.host")
      ~database:(Helm_registry.get "db.database")
      ~user:(Helm_registry.get "db.user")
      ()
  in
  restore_environment ();
  read_notation ();
  Http_daemon.start' ~port (callback dbd);
  printf "%s is terminating, bye!\n" daemon_name