src/Tools/WWW_Find/scgi_server.ML
author wenzelm
Sat, 09 Jul 2011 21:53:27 +0200
changeset 43721 fad8634cee62
parent 43075 6fde0c323c15
child 45026 5c0b0d67f9b1
permissions -rw-r--r--
echo prover input via raw_messages, for improved protocol tracing;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33823
24090eae50b6 standardized headers;
wenzelm
parents: 33817
diff changeset
     1
(*  Title:      Tools/WWW_Find/scgi_server.ML
33817
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
     2
    Author:     Timothy Bourke, NICTA
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
     3
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
     4
Simple SCGI server.
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
     5
*)
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
     6
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
     7
signature SCGI_SERVER =
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
     8
sig
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
     9
  val max_threads : int Unsynchronized.ref
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    10
  type handler = ScgiReq.t * Word8Vector.vector * (string -> unit) -> unit
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    11
  val register : (string * Mime.t option * handler) -> unit
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    12
  val server : string -> int -> unit
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    13
  val server' : int -> string -> int -> unit (* keeps trying for port *)
43074
8b566f0d226c generic ScgiServer.simple_handler
krauss
parents: 41522
diff changeset
    14
  val simple_handler : (string Symtab.table -> (string -> unit) -> unit) -> handler
43075
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents: 43074
diff changeset
    15
  val raw_post_handler : (string -> string) -> handler
33817
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    16
end;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    17
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    18
structure ScgiServer : SCGI_SERVER =
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    19
struct
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    20
val max_threads = Unsynchronized.ref 5;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    21
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    22
type handler = ScgiReq.t * Word8Vector.vector * (string -> unit) -> unit;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    23
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    24
local
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    25
val servers = Unsynchronized.ref (Symtab.empty : (Mime.t option * handler) Symtab.table);
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    26
in
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    27
fun register (name, mime, f) =
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    28
  Unsynchronized.change servers (Symtab.update_new (name, (mime, f)));
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    29
fun lookup name = Symtab.lookup (!servers) name;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    30
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    31
fun dump_handlers () = (
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    32
    tracing("  with handlers:");
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    33
    app (fn (x, _) => tracing ("    - " ^ x)) (Symtab.dest (!servers)))
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    34
end;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    35
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    36
fun server server_prefix port =
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    37
  let
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    38
    val passive_sock = SocketUtil.init_server_socket (SOME "localhost") port;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    39
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    40
    val thread_wait = ConditionVar.conditionVar ();
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    41
    val thread_wait_mutex = Mutex.mutex ();
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    42
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    43
    local
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    44
    val threads = Unsynchronized.ref ([] : Thread.thread list);
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    45
    fun purge () = Unsynchronized.change threads (filter Thread.isActive);
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    46
    in
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    47
    fun add_thread th = Unsynchronized.change threads (cons th);
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    48
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    49
    fun launch_thread threadf =
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    50
      (purge ();
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    51
       if length (!threads) < (!max_threads) then ()
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    52
       else (tracing ("Waiting for a free thread...");
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    53
             ConditionVar.wait (thread_wait, thread_wait_mutex));
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    54
       add_thread
39155
3e94ebe282f1 some results of concurrency code inspection;
wenzelm
parents: 33823
diff changeset
    55
         (Thread.fork   (* FIXME avoid low-level Poly/ML thread primitives *)
33817
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    56
            (fn () => exception_trace threadf,
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    57
             [Thread.EnableBroadcastInterrupt true,
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    58
              Thread.InterruptState
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    59
              Thread.InterruptAsynchOnce])))
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    60
    end;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    61
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    62
    fun loop () =
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    63
      let
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    64
        val (sock, _)= Socket.accept passive_sock;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    65
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    66
        val (sin, sout) = SocketUtil.make_streams sock;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    67
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    68
        fun send msg = BinIO.output (sout, Byte.stringToBytes msg);
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    69
        fun send_log msg = (tracing msg; send msg);
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    70
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    71
        fun get_content (st, 0) = Word8Vector.fromList []
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    72
          | get_content x = BinIO.inputN x;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    73
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    74
        fun do_req () =
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    75
          let
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    76
            val (req as ScgiReq.Req {path_info, request_method, ...},
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    77
                 content_is) =
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    78
              ScgiReq.parse sin
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    79
              handle ScgiReq.InvalidReq s =>
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    80
                (send
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    81
                   (HttpUtil.reply_header (HttpStatus.bad_request, NONE, []));
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    82
                 raise Fail ("Invalid request: " ^ s));
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    83
            val () = tracing ("request: " ^ path_info);
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    84
          in
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    85
            (case lookup (unprefix server_prefix path_info) of
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    86
               NONE => send (HttpUtil.reply_header (HttpStatus.not_found, NONE, []))
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    87
             | SOME (NONE, f) => f (req, get_content content_is, send)
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    88
             | SOME (t, f) =>
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    89
                (send (HttpUtil.reply_header (HttpStatus.ok, t, []));
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    90
                 if request_method = ScgiReq.Head then ()
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    91
                 else f (req, get_content content_is, send)))
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    92
          end;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    93
41522
42d13d00ccfb more FIXMEs concerning bad catch-all exception handlers;
wenzelm
parents: 41491
diff changeset
    94
        fun thread_req () =  (* FIXME avoid handle e *)
33817
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    95
          (do_req () handle e => (warning (exnMessage e));
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    96
           BinIO.closeOut sout handle e => warning (exnMessage e);
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    97
           BinIO.closeIn sin handle e => warning (exnMessage e);
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    98
           Socket.close sock handle e => warning (exnMessage e);
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    99
           tracing ("request done.");
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   100
           ConditionVar.signal thread_wait);
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   101
      in
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   102
        launch_thread thread_req;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   103
        loop ()
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   104
      end;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   105
  in
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   106
    tracing ("SCGI server started.");
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   107
    dump_handlers ();
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   108
    loop ();
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   109
    Socket.close passive_sock
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   110
  end;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   111
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   112
local
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   113
val delay = 5;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   114
in
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   115
fun server' 0 server_prefix port = (warning "Giving up."; exit 1)
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   116
  | server' countdown server_prefix port =
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   117
      server server_prefix port
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   118
        handle OS.SysErr ("bind failed", _) =>
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   119
          (warning ("Could not acquire port "
41491
a2ad5b824051 eliminated Int.toString;
wenzelm
parents: 39155
diff changeset
   120
                    ^ string_of_int port ^ ". Trying again in "
a2ad5b824051 eliminated Int.toString;
wenzelm
parents: 39155
diff changeset
   121
                    ^ string_of_int delay ^ " seconds...");
33817
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   122
           OS.Process.sleep (Time.fromSeconds delay);
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   123
           server' (countdown - 1) server_prefix port);
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   124
end;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   125
43074
8b566f0d226c generic ScgiServer.simple_handler
krauss
parents: 41522
diff changeset
   126
fun simple_handler h (ScgiReq.Req {request_method, query_string, ...}, content, send) =
8b566f0d226c generic ScgiServer.simple_handler
krauss
parents: 41522
diff changeset
   127
  h (case request_method of
8b566f0d226c generic ScgiServer.simple_handler
krauss
parents: 41522
diff changeset
   128
     ScgiReq.Get => query_string
8b566f0d226c generic ScgiServer.simple_handler
krauss
parents: 41522
diff changeset
   129
   | ScgiReq.Post =>
8b566f0d226c generic ScgiServer.simple_handler
krauss
parents: 41522
diff changeset
   130
      content
8b566f0d226c generic ScgiServer.simple_handler
krauss
parents: 41522
diff changeset
   131
      |> Byte.bytesToString
8b566f0d226c generic ScgiServer.simple_handler
krauss
parents: 41522
diff changeset
   132
      |> HttpUtil.parse_query_string
8b566f0d226c generic ScgiServer.simple_handler
krauss
parents: 41522
diff changeset
   133
   | ScgiReq.Head => raise Fail "Cannot handle Head requests.")
8b566f0d226c generic ScgiServer.simple_handler
krauss
parents: 41522
diff changeset
   134
  send;
8b566f0d226c generic ScgiServer.simple_handler
krauss
parents: 41522
diff changeset
   135
43075
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents: 43074
diff changeset
   136
fun raw_post_handler h (ScgiReq.Req {request_method=ScgiReq.Post, ...}, content, send) =
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents: 43074
diff changeset
   137
      send (h (Byte.bytesToString content))
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents: 43074
diff changeset
   138
  | raw_post_handler _ _ = raise Fail "Can only handle POST request.";
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents: 43074
diff changeset
   139
33817
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   140
end;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   141