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 ;;
  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 ;;
  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 ;;
  64
  65 let usage_string =
  66 "
  67 <html>
  68   <head>
  69     <title>ProofChecker's help message</title>
  70   </head>
  71   <body>
  72     <h1>ProofChecker</h1>
  73     <h2>Usage</h2>
  74     <p>
  75     Usage: <kbd>http://hostname:proofcheckerport/</kbd><em>command</em>
  76     </p>
  77     <p>
  78     Available commands:
  79     </p>
  80     <p>
  81       <b><kbd>help</kbd></b><br />
  82       display this help message
  83     </p>
  84     <p>
  85       <b><kbd>proofCheck?uri=uri</kbd></b><br />
  86       proof-checks the object whose URI is specified by <em>uri</em>
  87     </p>
  88   </body>
  89 </html>
  90 "
  91 ;;
  92
  93 let callback (req : Http_types.request) outchan =
  94   match req#path with
  95   | "/proofCheck" ->
  96       begin
  97         Logger.log_callback :=
  98           (Logger.log_to_html
  99             ~print_and_flush:(fun s -> fprintf outchan "%s" s; flush outchan));
 100         try
 101           let uri = req#param "uri" in
 102           printf "Request to proof-check \"%s\"..." uri;
 103           flush stdout;
 104           fprintf outchan "%s" (html_preamble uri);
 105           flush outchan;
 106           (try
 107             CicTypeChecker.typecheck (UriManager.uri_of_string uri);
 108            with e ->
 109             fprintf outchan "%s\n" (Printexc.to_string e);
 110             flush outchan);
 111           fprintf outchan "%s" html_postamble;
 112           flush outchan;
 113           printf " done\n\n";
 114           flush stdout
 115         with Not_found -> (* 'uri' argument not found *)
 116           bad_request outchan
 117       end
 118   | "/help" ->
 119       Http_daemon.respond ~body:usage_string
 120        ~headers:["Content-Type", "text/html"] outchan
 121   | req -> bad_request outchan
 122
 123 in
 124
 125 printf "Proof Checker started and listening on port %d\n" port;
 126 flush stdout;
 127 Http_daemon.start' ~port callback;
 128 printf "Proof Checker is terminating, bye!\n"