open Printf;;
open Http_types;;

(*** from matitaScript.ml ***)
(* let only_dust_RE = Pcre.regexp "^(\\s|\n|%%[^\n]*\n)*$" *)

let eval_statement include_paths (* (buffer : GText.buffer) *) status (* script *)
 statement
=
  let ast,unparsed_text =
    match statement with
    | `Raw text ->
        (* if Pcre.pmatch ~rex:only_dust_RE text then raise Margin; *)
        let strm =
         GrafiteParser.parsable_statement status
          (Ulexing.from_utf8_string text) in
        let ast = MatitaEngine.get_ast status include_paths strm in
         ast, text
    | `Ast (st, text) -> st, text
  in
  let floc = match ast with
  | GrafiteAst.Executable (loc, _)
  | GrafiteAst.Comment (loc, _) -> loc in
  
  let _,lend = HExtlib.loc_of_floc floc in 
  let parsed_text, parsed_text_len = 
    MatitaGtkMisc.utf8_parsed_text unparsed_text (HExtlib.floc_of_loc (0,lend)) in
  
  let status = 
    MatitaEngine.eval_ast ~include_paths ~do_heavy_checks:false status ("",0,ast)
  in 
  (status, parsed_text),"",(*parsed_text_len*) Glib.Utf8.length parsed_text


let status = ref (new MatitaEngine.status "cic:/matita");;

let include_paths = ["/home/barolo/matitaB/matita/lib"];;

let advance text (* (?bos=false) *) =
   (* if bos then LibraryClean.clean_baseuris [self#buri_of_current_file];
   (* HLog.debug ("evaluating: " ^ first_line s ^ " ...");*)
   let time1 = Unix.gettimeofday () in
   let entries, newtext, parsed_len = *)
     let (st,_),_,parsed_len =
       (* try *)
         eval_statement include_paths (*buffer*) !status (`Raw text)
       (* with End_of_file -> raise Margin *)
     in
     status := st; 
     let _,_,metasenv,subst,_ = !status#obj in
     let txt = List.fold_left 
       (fun acc (nmeta,_ as meta) ->
         let txt0 = Netencoding.Html.encode ~in_enc:`Enc_utf8 ()
           (snd (ApplyTransformation.ntxt_of_cic_sequent 
            ~metasenv ~subst ~map_unicode_to_tex:false 80 !status meta)) in
         ("<B>Goal ?" ^ (string_of_int nmeta) ^ "</B>\n" ^ txt0)::acc)
       [] metasenv
     in
     let txt = String.concat "\n\n" txt in
     parsed_len, txt
   (*in
   let time2 = Unix.gettimeofday () in
   HLog.debug ("... done in " ^ string_of_float (time2 -. time1) ^ "s");
   let new_statuses, new_statements =
     let statuses, texts = List.split entries in
     statuses, texts
   in
   history <- new_statuses @ history;
   statements <- new_statements @ statements;
   let start = buffer#get_iter_at_mark (`MARK locked_mark) in
   let new_text = String.concat "" (List.rev new_statements) in
   if statement <> None then
     buffer#insert ~iter:start new_text
   else begin
     let parsed_text = String.sub s 0 parsed_len in
     if new_text <> parsed_text then begin
       let stop = start#copy#forward_chars (Glib.Utf8.length parsed_text) in
       buffer#delete ~start ~stop;
       buffer#insert ~iter:start new_text;
     end;
   end;
   self#moveMark (Glib.Utf8.length new_text);
   buffer#insert ~iter:(buffer#get_iter_at_mark (`MARK locked_mark)) newtext*)
;;

let read_file fname =
  let chan = open_in fname in
  let lines = ref [] in
  (try
     while true do
       lines := input_line chan :: !lines
     done;
   with End_of_file -> close_in chan);
  String.concat "\r\n" (List.rev !lines)
;;

let load_index outchan =
  let s = read_file "index.html" in
  Http_daemon.respond ~headers:["Content-Type", "text/html"] ~code:(`Code 200) ~body:s outchan
;;

let call_service outchan =
  try 
   (ignore(MatitaEngine.assert_ng 
     ~include_paths:["/home/barolo/matitaB/matita/lib"] (* ~outch:outchan *)
    "/home/barolo/matitaB/matita/lib/basics/pts.ma");
    prerr_endline "fatto";
    let s = read_file "/home/barolo/matitaB/matita/lib/basics/pts.ma.mad"
    in
    Http_daemon.respond ~headers:["Content-Type", "text/html"] ~code:(`Code 200) ~body:s outchan
   )
  with
  e -> Http_daemon.respond ~code:(`Code 500) outchan
;;

let callback req outchan =
  let str = 
    (sprintf "request path = %s\n"  req#path) ^
    (sprintf "request GET params = %s\n"
      (String.concat ";"
        (List.map (fun (h,v) -> String.concat "=" [h;v]) req#params_GET))) ^
    (sprintf "request POST params = %s\n"
      (String.concat ";"
        (List.map (fun (h,v) -> String.concat "=" [h;v]) req#params_POST))) ^
    (sprintf "request ALL params = %s\n"
      (String.concat ";"
        (List.map (fun (h,v) -> String.concat "=" [h;v]) req#params))) ^
    (sprintf "cookies = %s\n"
      (match req#cookies with
      | None ->
          "NO COOKIES "
          ^ (if req#hasHeader ~name:"cookie"
             then "('Cookie:' header was '" ^ req#header ~name:"cookie" ^ "')"
             else "(No 'Cookie:' header received)")
      | Some cookies ->
          (String.concat ";"
            (List.map (fun (n,v) -> String.concat "=" [n;v]) cookies)))) ^
    (sprintf "request BODY = '%s'\n\n" req#body)
  in
  (* Http_daemon.respond ~code:(`Code 200) ~body: str outchan *)

  prerr_endline str;

  match req#path with
  | "/" -> load_index outchan
  | "/matita" -> call_service outchan
  | "/open" ->
      prerr_endline "getting 'file' argument";
      let filename = List.assoc "file" req#params_GET in
      prerr_endline ("reading file " ^ filename);
      let body = read_file filename in
      let _,baseuri,_,_ = 
        Librarian.baseuri_of_script ~include_paths:[] filename
      in
      status := (!status)#set_baseuri baseuri;
      Http_daemon.respond ~code:(`Code 200) ~body outchan
  | "/advance" ->
      let script = req#body in
      prerr_endline ("body length = " ^ (string_of_int (String.length script)));
      let (parsed_len,txt), res, code =
        try advance script, "OK", `Code 200
        with 
        | HExtlib.Localized(_,e) 
        | e -> 
                (prerr_endline ("exception: " ^ Printexc.to_string e);
                (try 
                  NTacStatus.pp_tac_status !status
                with e -> prerr_endline ("inner exception: " ^
                  Printexc.to_string e));
                prerr_endline "end status";
                let _,_,metasenv,subst,_ = !status#obj in
                let txt = List.fold_left 
                  (fun acc (nmeta,_ as meta) ->
                    let txt0 = Netencoding.Html.encode ~in_enc:`Enc_utf8 ()
                      (snd (ApplyTransformation.ntxt_of_cic_sequent 
                       ~metasenv ~subst ~map_unicode_to_tex:false 80 !status meta)) in
                    ("<B>Goal ?" ^ (string_of_int nmeta) ^ "</B>\n" ^ txt0)::acc)
                  [] metasenv
                in
                let txt = String.concat "\n\n" txt in
                (0,txt), Printexc.to_string e, `Code 500)
      in
      let txt = Netencoding.Url.encode ~plus:false txt in
      let body = (string_of_int parsed_len) ^ "#" ^ txt in
      Http_daemon.respond ~code ~body outchan
  | url -> Http_daemon.respond_not_found ~url outchan  

;;



let spec =
  { Http_daemon.default_spec with
      callback = callback;
      port = 9999;
      mode = `Single;
  }
;;

let _ =
  MatitaInit.initialize_all ();
  Http_daemon.main spec
;;