-let main () =
- let uris = ref [] in
- Arg.parse []
- (fun uri -> uris := uri :: !uris)
- "
-usage: proofChecker uri ...
-
-List of options:";
- uris := List.rev !uris;
- List.iter
- (function uri ->
- try
- CicTypeChecker.typecheck (UriManager.uri_of_string uri)
- with
- e -> print_newline () ; flush stdout ; raise e
- ) !uris
-;;
-
-CicCooking.init() ;
-main ();;
+open Printf;;
+
+let default_port = 48084;;
+
+let port =
+ try
+ int_of_string (Sys.getenv "PROOF_CHECKER_PORT")
+ with
+ | Not_found -> default_port
+ | Failure "int_of_string" ->
+ prerr_endline "Warning: invalid port, reverting to default";
+ default_port
+in
+
+let (html_preamble, html_postamble) =
+ ((fun uri ->
+ (sprintf
+"<html>
+<head>
+ <title>Proof-Checking %s</title>
+</head>
+<body bgcolor=\"white\">
+<h1>Proof-Checking %s:</h1>
+"
+ uri uri)),
+("<h1>Done.</h1>
+</body>
+</html>
+END
+"))
+in
+
+let bad_request outchan =
+ printf "INVALID REQUEST !!!!!\n\n";
+ flush stdout;
+ Http_daemon.respond_error ~status:(`Client_error `Bad_request) outchan;
+ flush outchan
+in
+
+let callback req outchan =
+ match req#path with
+ | "/proofCheck" ->
+ begin
+ Logger.log_callback :=
+ (Logger.log_to_html
+ ~print_and_flush:(fun s -> fprintf outchan "%s" s; flush outchan));
+ try
+ let uri = req#param "uri" in
+ printf "Request to proof-check \"%s\"..." uri;
+ flush stdout;
+ fprintf outchan "%s" (html_preamble uri);
+ flush outchan;
+ (try
+ CicTypeChecker.typecheck (UriManager.uri_of_string uri);
+ with e ->
+ fprintf outchan "%s\n" (Printexc.to_string e);
+ flush outchan);
+ fprintf outchan "%s" html_postamble;
+ flush outchan;
+ printf " done\n\n";
+ flush stdout
+ with Not_found -> (* 'uri' argument not found *)
+ bad_request outchan
+ end
+ | req -> bad_request outchan
+
+in
+
+CicCooking.init();
+printf "Proof Checker started and listening on port %d\n" port;
+flush stdout;
+Http_daemon.start' ~port callback;
+printf "Proof Checker is terminating, bye!\n"
+