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