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