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 byte_parsed_text_len = String.length parsed_text in
let unparsed_txt' =
String.sub unparsed_text byte_parsed_text_len
(String.length unparsed_text - byte_parsed_text_len)
in
let status =
MatitaEngine.eval_ast ~include_paths ~do_heavy_checks:false status ("",0,ast)
in
(status, parsed_text, unparsed_txt'),"",(*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 -> "?" ^ (string_of_int i) ^ ""
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 -> "" ^ (render_switch sw) ^ " "
| 0, _ ->
Printf.sprintf "|%d: %s" pos (render_switch sw)
| 1, pos when Stack.head_tag s#stack = `BranchTag ->
Printf.sprintf "|%d : %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);
("Goal ?" ^ (string_of_int nmeta) ^ "\n" ^ txt0)::acc)
[] metasenv
in
String.concat "\n\n" txt
;; *)
(* returns the length of the executed text and an html representation of the
* current metasenv*)
let advance text (* (?bos=false) *) =
let (st,new_statements,new_unparsed),(* 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, new_unparsed, txt
;;
let heading_nl_RE = Pcre.regexp "^\\s*\n\\s*";;
let first_line s =
let s = Pcre.replace ~rex:heading_nl_RE s in
try
let nl_pos = String.index s '\n' in
String.sub s 0 nl_pos
with Not_found -> s
;;
let gotoBottom =
let rec aux parsed_len metasenv text =
try
prerr_endline ("evaluating: " ^ first_line text);
let plen,new_unparsed,cur_metasenv = advance text in
aux (parsed_len+plen) cur_metasenv new_unparsed
with
| End_of_file -> parsed_len, metasenv
| _ ->
prerr_endline ("goto bottom debug: metasenv = \n" ^ metasenv);
parsed_len, metasenv
in aux 0 ""
;;
let retract () =
let new_history,new_status =
match !history with
_::(status::_ as history) ->
history, status
| [_] -> (prerr_endline "singleton";failwith "retract")
| _ -> (prerr_endline "nil"; 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 "\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
let is_png =
try String.sub filename (String.length filename - 4) 4 = ".png"
with Invalid_argument _ -> false
in
let contenttype = if is_png then "image/png" else "text/html" in
Http_daemon.respond ~headers:["Content-Type", contenttype] ~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
| "/bottom" ->
let script = req#body in
prerr_endline ("body length = " ^ (string_of_int (String.length script)));
let (parsed_len,txt), res, code =
try gotoBottom 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
prerr_endline "retract OK";
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
;;