open Printf;;
open Http_types;;

module Stack = Continuationals.Stack

(*** 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 history = ref [!status];;

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

(* lista [meta n., goal; meta n., goal; ... ] *)
(* "item1#item2#...#" *)

let output_status s =
  let _,_,metasenv,subst,_ = s#obj in
  let render_switch = function 
  | Stack.Open i -> "?" ^ (string_of_int i) 
  | Stack.Closed i -> "<S>?" ^ (string_of_int i) ^ "</S>"
  in
  let int_of_switch = function
  | Stack.Open i | Stack.Closed i -> i
  in
  let sequent = function
  | Stack.Open i ->
      let meta = List.assoc i metasenv in
      snd (ApplyTransformation.ntxt_of_cic_sequent 
        ~metasenv ~subst ~map_unicode_to_tex:false 80 s (i,meta))
  | Stack.Closed _ -> "This goal has already been closed."
  in
  let render_sequent is_loc acc depth tag (pos,sw) =
    let metano = int_of_switch sw in
    let markup = 
      if is_loc then
        (match depth, pos with
         | 0, 0 -> "<B>" ^ (render_switch sw) ^ "</B> "
         | 0, _ -> 
            Printf.sprintf "<B>|<SUB>%d</SUB>: %s</B>" pos (render_switch sw)
         | 1, pos when Stack.head_tag s#stack = `BranchTag ->
             Printf.sprintf "|<SUB>%d</SUB> : %s" pos (render_switch sw)
         | _ -> render_switch sw)
      else render_switch sw
    in
    let markup = Netencoding.Url.encode ~plus:false markup in
    let txt0 = Netencoding.Url.encode ~plus:false (sequent sw) in
    (string_of_int metano ^ "|" ^ markup ^ "|" ^ txt0 ^ "#" ^ acc)
  in
  Stack.fold 
    ~env:(render_sequent true) ~cont:(render_sequent false) 
    ~todo:(render_sequent false) "" s#stack
;;

(* let html_of_status s =
  let _,_,metasenv,subst,_ = s#obj in
  let txt = List.fold_left 
    (fun acc (nmeta,_ as meta) ->
       let txt0 = snd (ApplyTransformation.ntxt_of_cic_sequent 
         ~metasenv ~subst ~map_unicode_to_tex:false 80 s meta)
       in
       prerr_endline ("### txt0 = " ^ txt0);
      ("<B>Goal ?" ^ (string_of_int nmeta) ^ "</B>\n" ^ txt0)::acc)
    [] metasenv
  in
  String.concat "\n\n" txt
;; *)

let advance text (* (?bos=false) *) =
     let (st,new_statements),(* newtext TODO *) _,parsed_len =
       (* try *)
         eval_statement include_paths (*buffer*) !status (`Raw text)
       (* with End_of_file -> raise Margin *)
     in
     status := st;
     history := st :: !history;
     let txt = output_status !status in
     parsed_len, txt
;;

let retract () =
  let new_history,new_status =
     match !history with
       _::(status::_ as history) ->
        history, status
    | [_] -> failwith "retract"
    | _ -> assert false in
  NCicLibrary.time_travel !status;
  history := new_history;
  status := new_status;
  output_status !status
;;

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 load_doc filename outchan =
  let s = read_file filename 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 txt = output_status !status in
                (0,txt), Printexc.to_string e, `Code 500)
      in
      prerr_endline ("server response:\n" ^ txt);
      let body = (string_of_int parsed_len) ^ "@" ^ txt in
      Http_daemon.respond ~code ~body outchan
  | "/retract" ->
      (try
        let body = retract () in
        Http_daemon.respond ~code:(`Code 200) ~body outchan
       with e -> 
        (prerr_endline (Printexc.to_string e);
         Http_daemon.respond ~code:(`Code 500) outchan))
  | url -> 
     try 
       let url = String.sub url 1 (String.length url - 1) in
       load_doc url outchan
     with _ -> Http_daemon.respond_not_found ~url outchan  
;;

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

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