helm/proofChecker/proofChecker.ml

   1 (* Copyright (C) 2002, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 open Printf;;
  27
  28 let default_port = 48084;;
  29
  30 let port =
  31   try
  32     int_of_string (Sys.getenv "PROOF_CHECKER_PORT")
  33   with
  34   | Not_found -> default_port
  35   | Failure "int_of_string" ->
  36       prerr_endline "Warning: invalid port, reverting to default";
  37       default_port
  38 in
  39
  40 let (html_preamble, html_postamble) =
  41   ((fun uri ->
  42     (sprintf
  43 "<html>
  44 <head>
  45  <title>Proof-Checking %s</title>
  46 </head>
  47 <body bgcolor=\"white\">
  48 <h1>Proof-Checking %s:</h1>
  49 "
  50       uri uri)),
  51 ("<h1>Done.</h1>
  52 </body>
  53 </html>
  54 END
  55 "))
  56 in
  57
  58 let bad_request outchan =
  59   printf "INVALID REQUEST !!!!!\n\n";
  60   flush stdout;
  61   Http_daemon.respond_error ~status:(`Client_error `Bad_request) outchan;
  62   flush outchan
  63 in
  64
  65 let callback req outchan =
  66   match req#path with
  67   | "/proofCheck" ->
  68       begin
  69         Logger.log_callback :=
  70           (Logger.log_to_html
  71             ~print_and_flush:(fun s -> fprintf outchan "%s" s; flush outchan));
  72         try
  73           let uri = req#param "uri" in
  74           printf "Request to proof-check \"%s\"..." uri;
  75           flush stdout;
  76           fprintf outchan "%s" (html_preamble uri);
  77           flush outchan;
  78           (try
  79             CicTypeChecker.typecheck (UriManager.uri_of_string uri);
  80            with e ->
  81             fprintf outchan "%s\n" (Printexc.to_string e);
  82             flush outchan);
  83           fprintf outchan "%s" html_postamble;
  84           flush outchan;
  85           printf " done\n\n";
  86           flush stdout
  87         with Not_found -> (* 'uri' argument not found *)
  88           bad_request outchan
  89       end
  90   | req -> bad_request outchan
  91
  92 in
  93
  94 CicCooking.init();
  95 printf "Proof Checker started and listening on port %d\n" port;
  96 flush stdout;
  97 Http_daemon.start' ~port callback;
  98 printf "Proof Checker is terminating, bye!\n"
  99