open Printf;; open Http_types;; module Stack = Continuationals.Stack let rt_path () = Helm_registry.get "matita.rt_base_dir" let libdir uid = (rt_path ()) ^ "/users/" ^ uid let utf8_length = Netconversion.ustring_length `Enc_utf8 (*** 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 = HExtlib.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*) utf8_length parsed_text (*let save_moo status = let script = MatitaScript.current () in let baseuri = status#baseuri in match script#bos, script#eos with | true, _ -> () | _, true -> GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) status | _ -> clean_current_baseuri status ;;*) let sequent_size = ref 40;; let include_paths = ref [];; (* * * ... * ... * * * ... * *) 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 !sequent_size 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 prerr_endline "pippo1"; let markup = Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () markup in let markup = "" ^ markup ^ "" in prerr_endline "pippo2"; let sequent = Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () (sequent sw) in let txt0 = "" ^ sequent ^ "" in "" ^ markup ^ txt0 ^ "" ^ acc in let res = "" ^ (Stack.fold ~env:(render_sequent true) ~cont:(render_sequent false) ~todo:(render_sequent false) "" s#stack) ^ "" in prerr_endline ("sending metasenv:\n" ^ res); res ;; (* 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 ;; *) let html_of_matita s = prerr_endline ("input: " ^ s); let patt1 = Str.regexp "\005" in let patt2 = Str.regexp "\006" in let patt3 = Str.regexp "<" in let patt4 = Str.regexp ">" in let res = Str.global_replace patt4 ">" s in prerr_endline ("output: " ^ res); let res = Str.global_replace patt3 "<" res in prerr_endline ("output: " ^ res); let res = Str.global_replace patt2 ">" res in prerr_endline ("output: " ^ res); let res = Str.global_replace patt1 "<" res in prerr_endline ("output: " ^ res); res ;; 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 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 retrieve (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in let env = cgi#environment in (try let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in let sid = HExtlib.unopt sid in let uid = MatitaAuthentication.user_of_session sid in (* cgi # set_header ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" (); *) let filename = libdir uid ^ "/" ^ (cgi # argument_value "file") in prerr_endline ("reading file " ^ filename); let body = Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () (html_of_matita (read_file filename)) in (* html_of_matita (read_file filename) in *) prerr_endline ("sending:\nBEGIN\n" ^ body ^ "\nEND"); let body = "" ^ body ^ "" in let baseuri, incpaths = try let root, baseuri, _fname, _tgt = Librarian.baseuri_of_script ~include_paths:[] filename in let includes = try Str.split (Str.regexp " ") (List.assoc "include_paths" (Librarian.load_root_file (root^"/root"))) with Not_found -> [] in let rc = root :: includes in List.iter (HLog.debug) rc; baseuri, rc with Librarian.NoRootFor _ | Librarian.FileNotFound _ -> "",[] in include_paths := incpaths; let status = MatitaAuthentication.get_status sid in MatitaAuthentication.set_status sid (status#set_baseuri baseuri); cgi # set_header ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" (); cgi#out_channel#output_string body; with | Not_found _ -> cgi # set_header ~status:`Internal_server_error ~cache:`No_cache ~content_type:"text/html; charset=\"utf-8\"" ()); cgi#out_channel#commit_work() ;; let advance0 sid text = let status = MatitaAuthentication.get_status sid in let status = status#reset_disambiguate_db () in let (st,new_statements,new_unparsed),(* newtext TODO *) _,parsed_len = try eval_statement !include_paths (*buffer*) status (`Raw text) with | HExtlib.Localized (_,e) -> raise e (*| End_of_file -> raise Margin *) in let stringbuf = Ulexing.from_utf8_string new_statements in let interpr = GrafiteDisambiguate.get_interpr st#disambiguate_db in let outstr = ref "" in ignore (SmallLexer.mk_small_printer interpr outstr stringbuf); prerr_endline ("parser output: " ^ !outstr); MatitaAuthentication.set_status sid st; parsed_len, Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () (html_of_matita !outstr), new_unparsed, st let register (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in let env = cgi#environment in assert (cgi#arguments <> []); let uid = cgi#argument_value "userid" in let userpw = cgi#argument_value "password" in (try MatitaAuthentication.add_user uid userpw; (* env#set_output_header_field "Location" "/index.html" *) cgi#out_channel#output_string ("" ^ "Redirecting to login page...") with | MatitaAuthentication.UsernameCollision _ -> cgi#set_header ~cache:`No_cache ~content_type:"text/html; charset=\"utf-8\"" (); cgi#out_channel#output_string "Error: User id collision!" | MatitaFilesystem.SvnError msg -> cgi#set_header ~cache:`No_cache ~content_type:"text/html; charset=\"utf-8\"" (); cgi#out_channel#output_string ("

Error: Svn checkout failed!

")); cgi#out_channel#commit_work() ;; let login (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in let env = cgi#environment in assert (cgi#arguments <> []); let uid = cgi#argument_value "userid" in let userpw = cgi#argument_value "password" in let pw,_ = MatitaAuthentication.lookup_user uid in if pw = userpw then begin let _ = MatitaFilesystem.html_of_library uid in let sid = MatitaAuthentication.create_session uid in (* let cookie = Netcgi.Cookie.make "session" (Uuidm.to_string sid) in cgi#set_header ~set_cookies:[cookie] (); *) env#set_output_header_field "Set-Cookie" ("session=" ^ (Uuidm.to_string sid)); (* env#set_output_header_field "Location" "/index.html" *) cgi#out_channel#output_string ("" ^ "Redirecting to Matita page...") end else begin prerr_endline ("ERROR: received " ^ userpw ^ "but the password is " ^ pw); cgi#set_header ~cache:`No_cache ~content_type:"text/html; charset=\"utf-8\"" (); cgi#out_channel#output_string "Authentication error" end; cgi#out_channel#commit_work() ;; let logout (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in let env = cgi#environment in (try let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in let sid = HExtlib.unopt sid in MatitaAuthentication.logout_user sid; cgi # set_header ~cache:`No_cache ~content_type:"text/html; charset=\"utf-8\"" (); let text = read_file (rt_path () ^ "/logout.html") in cgi#out_channel#output_string text with | Not_found _ -> cgi # set_header ~status:`Internal_server_error ~cache:`No_cache ~content_type:"text/html; charset=\"utf-8\"" ()); cgi#out_channel#commit_work() ;; exception File_already_exists;; let save (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in let env = cgi#environment in (try let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in let sid = HExtlib.unopt sid in let status = MatitaAuthentication.get_status sid in let uid = MatitaAuthentication.user_of_session sid in assert (cgi#arguments <> []); let locked = cgi#argument_value "locked" in let unlocked = cgi#argument_value "unlocked" in let filename = libdir uid ^ "/" ^ (cgi # argument_value "file") in let force = bool_of_string (cgi#argument_value "force") in prerr_endline ("Matita will save the file for user " ^ uid); if ((not force) && (Sys.file_exists filename)) then raise File_already_exists; let oc = open_out filename in output_string oc (locked ^ unlocked); close_out oc; if MatitaEngine.eos status unlocked then begin prerr_endline ("serializing proof objects..."); GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string status#baseuri) status; prerr_endline ("adding to the commit queue..."); MatitaFilesystem.add_user uid; prerr_endline ("done."); end; cgi # set_header ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" (); cgi#out_channel#output_string "ok" with | File_already_exists -> cgi#out_channel#output_string "cancelled" | Sys_error _ -> cgi # set_header ~status:`Internal_server_error ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" ()); cgi#out_channel#commit_work() ;; let initiate_commit (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in let env = cgi#environment in (try let errors = MatitaFilesystem.do_global_commit () in prerr_endline ("commit errors: " ^ (String.concat " " errors)); cgi # set_header ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" (); cgi#out_channel#output_string "ok" with | Not_found _ -> cgi # set_header ~status:`Internal_server_error ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" ()); cgi#out_channel#commit_work() ;; (* returns the length of the executed text and an html representation of the * current metasenv*) let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in let env = cgi#environment in (try let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in let sid = HExtlib.unopt sid in (* cgi # set_header ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" (); *) let text = cgi#argument_value "body" in prerr_endline ("body =\n" ^ text); let history = MatitaAuthentication.get_history sid in let parsed_len, new_parsed, new_unparsed, new_status = advance0 sid text in MatitaAuthentication.set_history sid (new_status::history); let txt = output_status new_status in let body = "" ^ new_parsed ^ "" ^ txt ^ "" in prerr_endline ("sending advance response:\n" ^ body); cgi # set_header ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" (); cgi#out_channel#output_string body with | Not_found _ -> cgi # set_header ~status:`Internal_server_error ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" ()); cgi#out_channel#commit_work() ;; let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in let env = cgi#environment in (try let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in let sid = HExtlib.unopt sid in let history = MatitaAuthentication.get_history sid in let rec aux parsed_len parsed_txt text = try prerr_endline ("evaluating: " ^ first_line text); let plen,new_parsed,new_unparsed,_new_status = advance0 sid text in aux (parsed_len+plen) (parsed_txt ^ new_parsed) new_unparsed with | End_of_file -> let status = MatitaAuthentication.get_status sid in GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string status#baseuri) status; if parsed_len > 0 then MatitaAuthentication.set_history sid (status::history); parsed_len, parsed_txt | _ -> parsed_len, parsed_txt in (* cgi # set_header ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" (); *) let text = cgi#argument_value "body" in prerr_endline ("body =\n" ^ text); let parsed_len, new_parsed = aux 0 "" text in let status = MatitaAuthentication.get_status sid in let txt = output_status status in let body = "" ^ new_parsed ^ "" ^ txt ^ "" in (*let body = "" ^ txt ^ "" in*) prerr_endline ("sending goto bottom response:\n" ^ body); cgi # set_header ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" (); cgi#out_channel#output_string body with Not_found -> cgi#set_header ~status:`Internal_server_error ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" ()); cgi#out_channel#commit_work() ;; let retract (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in let env = cgi#environment in prerr_endline "executing retract"; (try let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in let sid = HExtlib.unopt sid in (* cgi # set_header ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" (); *) let history = MatitaAuthentication.get_history sid in let new_history,new_status = match history with _::(status::_ as history) -> history, status | [_] -> (prerr_endline "singleton";failwith "retract") | _ -> (prerr_endline "nil"; assert false) in prerr_endline "before time_travel"; NCicLibrary.time_travel new_status; prerr_endline "after time travel"; MatitaAuthentication.set_history sid new_history; MatitaAuthentication.set_status sid new_status; prerr_endline ("after retract history.length = " ^ string_of_int (List.length new_history)); let body = output_status new_status in cgi # set_header ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" (); cgi#out_channel#output_string body with _ -> cgi#set_header ~status:`Internal_server_error ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" ()); cgi#out_channel#commit_work() ;; let viewLib (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in let env = cgi#environment in let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in let sid = HExtlib.unopt sid in (* cgi # set_header ~cache:`No_cache ~content_type:"text/html; charset=\"utf-8\"" (); *) let uid = MatitaAuthentication.user_of_session sid in let html = MatitaFilesystem.html_of_library uid in cgi # set_header ~cache:`No_cache ~content_type:"text/html; charset=\"utf-8\"" (); cgi#out_channel#output_string ((* "\n" ^ "XML Tree Control\n" ^ "\n" ^ "\n" ^ "\n" ^ *) html (* ^ "\n" *) ); cgi#out_channel#commit_work() ;; let resetLib (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in MatitaAuthentication.reset (); cgi # set_header ~cache:`No_cache ~content_type:"text/html; charset=\"utf-8\"" (); cgi#out_channel#output_string ("\n" ^ "Matitaweb Reset\n" ^ "

Reset completed

"); cgi#out_channel#commit_work() open Netcgi1_compat.Netcgi_types;; (**********************************************************************) (* Create the webserver *) (**********************************************************************) let start() = let (opt_list, cmdline_cfg) = Netplex_main.args() in let use_mt = ref true in let opt_list' = [ "-mt", Arg.Set use_mt, " Use multi-threading instead of multi-processing" ] @ opt_list in Arg.parse opt_list' (fun s -> raise (Arg.Bad ("Don't know what to do with: " ^ s))) "usage: netplex [options]"; let parallelizer = if !use_mt then Netplex_mt.mt() (* multi-threading *) else Netplex_mp.mp() in (* multi-processing *) (* let adder = { Nethttpd_services.dyn_handler = (fun _ -> process1); dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered; dyn_uri = None; (* not needed *) dyn_translator = (fun _ -> ""); (* not needed *) dyn_accept_all_conditionals = false; } in *) let do_advance = { Nethttpd_services.dyn_handler = (fun _ -> advance); dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered; dyn_uri = None; (* not needed *) dyn_translator = (fun _ -> ""); (* not needed *) dyn_accept_all_conditionals = false; } in let do_retract = { Nethttpd_services.dyn_handler = (fun _ -> retract); dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered; dyn_uri = None; (* not needed *) dyn_translator = (fun _ -> ""); (* not needed *) dyn_accept_all_conditionals = false; } in let goto_bottom = { Nethttpd_services.dyn_handler = (fun _ -> gotoBottom); dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered; dyn_uri = None; (* not needed *) dyn_translator = (fun _ -> ""); (* not needed *) dyn_accept_all_conditionals = false; } in let retrieve = { Nethttpd_services.dyn_handler = (fun _ -> retrieve); dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered; dyn_uri = None; (* not needed *) dyn_translator = (fun _ -> ""); (* not needed *) dyn_accept_all_conditionals = false; } in let do_register = { Nethttpd_services.dyn_handler = (fun _ -> register); dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered; dyn_uri = None; (* not needed *) dyn_translator = (fun _ -> ""); (* not needed *) dyn_accept_all_conditionals = false; } in let do_login = { Nethttpd_services.dyn_handler = (fun _ -> login); dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered; dyn_uri = None; (* not needed *) dyn_translator = (fun _ -> ""); (* not needed *) dyn_accept_all_conditionals = false; } in let do_logout = { Nethttpd_services.dyn_handler = (fun _ -> logout); dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered; dyn_uri = None; (* not needed *) dyn_translator = (fun _ -> ""); (* not needed *) dyn_accept_all_conditionals = false; } in let do_viewlib = { Nethttpd_services.dyn_handler = (fun _ -> viewLib); dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered; dyn_uri = None; (* not needed *) dyn_translator = (fun _ -> ""); (* not needed *) dyn_accept_all_conditionals = false; } in let do_resetlib = { Nethttpd_services.dyn_handler = (fun _ -> resetLib); dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered; dyn_uri = None; (* not needed *) dyn_translator = (fun _ -> ""); (* not needed *) dyn_accept_all_conditionals = false; } in let do_save = { Nethttpd_services.dyn_handler = (fun _ -> save); dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered; dyn_uri = None; (* not needed *) dyn_translator = (fun _ -> ""); (* not needed *) dyn_accept_all_conditionals = false; } in let do_commit = { Nethttpd_services.dyn_handler = (fun _ -> initiate_commit); dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered; dyn_uri = None; (* not needed *) dyn_translator = (fun _ -> ""); (* not needed *) dyn_accept_all_conditionals = false; } in let nethttpd_factory = Nethttpd_plex.nethttpd_factory ~handlers:[ "advance", do_advance ; "retract", do_retract ; "bottom", goto_bottom ; "open", retrieve ; "register", do_register ; "login", do_login ; "logout", do_logout ; "reset", do_resetlib ; "viewlib", do_viewlib ; "save", do_save ; "commit", do_commit] () in MatitaInit.initialize_all (); MatitaAuthentication.deserialize (); Netplex_main.startup parallelizer Netplex_log.logger_factories (* allow all built-in logging styles *) Netplex_workload.workload_manager_factories (* ... all ways of workload management *) [ nethttpd_factory ] (* make this nethttpd available *) cmdline_cfg ;; Sys.set_signal Sys.sigpipe Sys.Signal_ignore; start();;