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 _ = Helm_registry.load_from "proofChecker.conf.xml";;
  29
  30 let port =
  31  try
  32   Helm_registry.get_int "proofchecker.port"
  33  with
  34   Helm_registry.Key_not_found _ -> 48084
  35 ;;
  36
  37 let (html_preamble, html_postamble) =
  38   ((fun uri ->
  39     (sprintf
  40 "<html>
  41 <head>
  42  <title>Proof-Checking %s</title>
  43 </head>
  44 <body bgcolor=\"white\">
  45 <h1>Proof-Checking %s:</h1>
  46 "
  47       uri uri)),
  48 ("<h1>Done.</h1>
  49 </body>
  50 </html>
  51 END
  52 "))
  53 ;;
  54
  55 let bad_request outchan =
  56   printf "INVALID REQUEST !!!!!\n\n";
  57   flush stdout;
  58   Http_daemon.respond_error ~status:(`Client_error `Bad_request) outchan;
  59   flush outchan
  60 ;;
  61
  62 let usage_string =
  63 "
  64 <html>
  65   <head>
  66     <title>ProofChecker's help message</title>
  67   </head>
  68   <body>
  69     <h1>ProofChecker</h1>
  70     <h2>Usage</h2>
  71     <p>
  72     Usage: <kbd>http://hostname:proofcheckerport/</kbd><em>command</em>
  73     </p>
  74     <p>
  75     Available commands:
  76     </p>
  77     <p>
  78       <b><kbd>help</kbd></b><br />
  79       display this help message
  80     </p>
  81     <p>
  82       <b><kbd>proofCheck?uri=uri</kbd></b><br />
  83       proof-checks the object whose URI is specified by <em>uri</em>
  84     </p>
  85   </body>
  86 </html>
  87 "
  88 ;;
  89
  90 let outchan = ref stderr;;
  91
  92 let _ =
  93  HelmLogger.register_log_callback
  94   (fun ?append_NL msg ->
  95     output_string !outchan (HelmLogger.html_of_html_msg msg) ;
  96     flush !outchan)
  97 ;;
  98
  99 let callback (req : Http_types.request) outchan' =
 100   match req#path with
 101   | "/proofCheck" ->
 102       begin
 103         outchan := outchan' ;
 104         try
 105           let uri = req#param "uri" in
 106           Http_daemon.send_basic_headers ~code:200 outchan' ;
 107           Http_daemon.send_header "Content-type" "text/html" outchan' ;
 108           Http_daemon.send_CRLF outchan' ;
 109           printf "Request to proof-check \"%s\"..." uri;
 110           flush stdout;
 111           fprintf outchan' "%s" (html_preamble uri);
 112           flush outchan';
 113           (try
 114             CicTypeChecker.typecheck (UriManager.uri_of_string uri);
 115            with e ->
 116             fprintf outchan' "%s\n" (Printexc.to_string e);
 117             flush outchan');
 118           fprintf outchan' "%s" html_postamble;
 119           flush outchan';
 120           printf " done\n\n";
 121           flush stdout
 122         with Http_types.Param_not_found _ -> (* 'uri' argument not found *)
 123           bad_request outchan'
 124       end
 125   | "/help" ->
 126       Http_daemon.respond ~body:usage_string
 127        ~headers:["Content-Type", "text/html"] outchan'
 128   | req -> bad_request outchan'
 129
 130 in
 131
 132 printf "Proof Checker started and listening on port %d\n" port;
 133 flush stdout;
 134 Http_daemon.start' ~port ~mode:`Fork callback ;
 135 printf "Proof Checker is terminating, bye!\n"