src/Tools/WWW_Find/scgi_req.ML
author blanchet
Mon, 26 Nov 2012 13:35:05 +0100
changeset 50222 40e3c3be6bca
parent 43703 c37a1f29bbc0
permissions -rw-r--r--
added file headers
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_req.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
Parses an SCGI (Simple Common Gateway Interface) header.
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
     5
See: http://python.ca/scgi/protocol.txt
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
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
     8
signature SCGI_REQ =
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
     9
sig
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    10
  exception InvalidReq of string
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    11
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    12
  datatype req_method = Get | Head | Post
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    13
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    14
  datatype t = Req of {
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    15
      path_info : string,
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    16
      path_translated : string,
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    17
      script_name : string,
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    18
      request_method : req_method,
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    19
      query_string : string Symtab.table,
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    20
      content_type : Mime.t option,
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    21
      environment : Word8VectorSlice.slice Symtab.table
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    22
    }
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
  val parse : BinIO.instream ->  t * (BinIO.instream * int)
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    25
  val test : string -> unit
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    26
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    27
  val show : t -> string
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    28
end;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    29
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    30
structure ScgiReq : SCGI_REQ =
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    31
struct
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    32
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    33
exception InvalidReq of string;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    34
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    35
datatype req_method = Get | Head | Post;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    36
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    37
datatype t = Req of {
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    38
    path_info : string,
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    39
    path_translated : string,
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    40
    script_name : string,
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    41
    request_method : req_method,
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    42
    query_string : string Symtab.table,
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    43
    content_type : Mime.t option,
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    44
    environment : Word8VectorSlice.slice Symtab.table
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    45
  };
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    46
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    47
fun parse_req_method "POST" = Post
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    48
  | parse_req_method "HEAD" = Head
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    49
  | parse_req_method _ = Get;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    50
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    51
fun show_req_method Get = "Get"
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    52
  | show_req_method Post = "Post"
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    53
  | show_req_method Head = "Head";
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    54
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    55
fun find_nulls (idx, 0wx00, idxs) = idx::idxs
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    56
  | find_nulls (_, _, idxs) = idxs;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    57
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    58
fun read_net_string fin =
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    59
  let
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    60
    fun read_size (_, NONE) = raise InvalidReq "Bad netstring length."
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    61
      | read_size (t, SOME 0wx3a) = t
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    62
      | read_size (t, SOME d) =
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 n = (Word8.toInt d) - 0x30;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    65
          in
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    66
            if n >=0 andalso n <= 9
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    67
            then read_size (t * 10 + n, BinIO.input1 fin)
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    68
            else read_size (t, NONE)
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    69
          end;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    70
    val size = read_size (0, BinIO.input1 fin);
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    71
    val payload = BinIO.inputN (fin, size);
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    72
  in
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    73
    (case (Word8Vector.length payload = size, BinIO.input1 fin) of
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    74
       (true, SOME 0wx2c) => payload
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    75
     | _ => raise InvalidReq "Bad netstring.")
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    76
  end;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    77
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    78
fun split_fields vec =
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    79
  let
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    80
    val nulls = ~1 :: (Word8Vector.foldri find_nulls [] vec);
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    81
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    82
    fun pr NONE = "NONE"
41491
a2ad5b824051 eliminated Int.toString;
wenzelm
parents: 40152
diff changeset
    83
      | pr (SOME i) = "SOME " ^ string_of_int i;
33817
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    84
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    85
    fun hd_diff (i1::i2::_) = SOME (i2 - i1 - 1)
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    86
      | hd_diff _ = NONE;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    87
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    88
    fun slice [] = []
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    89
      | slice (idxs as idx::idxs') =
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    90
          Word8VectorSlice.slice (vec, idx + 1, hd_diff idxs) :: slice idxs';
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    91
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    92
    fun make_pairs (x::y::xys) = (Byte.unpackStringVec x, y) :: make_pairs xys
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    93
      | make_pairs _ = [];
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    94
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    95
  in make_pairs (slice nulls) end;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    96
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    97
fun parse fin =
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    98
  let
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    99
    val raw_fields = read_net_string fin;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   100
    val fields = split_fields raw_fields;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   101
    val env = Symtab.make fields;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   102
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   103
    fun field name =
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   104
      (case Symtab.lookup env name of
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   105
         NONE => ""
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   106
       | SOME wv => Byte.unpackStringVec wv);
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   107
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   108
    val content_length =
40152
51e026049e4d do not handle arbitrary exceptions;
wenzelm
parents: 33823
diff changeset
   109
      (case Int.fromString (field "CONTENT_LENGTH") of
51e026049e4d do not handle arbitrary exceptions;
wenzelm
parents: 33823
diff changeset
   110
        SOME n => n
51e026049e4d do not handle arbitrary exceptions;
wenzelm
parents: 33823
diff changeset
   111
      | NONE => raise InvalidReq "Bad CONTENT_LENGTH");
33817
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   112
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   113
    val req = Req {
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   114
        path_info = field "PATH_INFO",
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   115
        path_translated = field "PATH_TRANSLATED",
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   116
        script_name = field "SCRIPT_NAME",
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   117
        request_method = (parse_req_method o field) "REQUEST_METHOD",
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   118
        query_string = (HttpUtil.parse_query_string o field) "QUERY_STRING",
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   119
        content_type = (Mime.parse_type o field) "CONTENT_TYPE",
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   120
        environment = env
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   121
      }
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   122
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   123
   in (req, (fin, content_length)) end; 
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   124
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   125
fun show (Req {path_info, path_translated, script_name,
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   126
               request_method, query_string, content_type, environment}) =
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   127
  let
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   128
    fun show_symtab to_string table = let
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   129
        fun show (n, v) r = ["\t", n, " = \"", to_string v, "\"\n"] @ r;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   130
      in Symtab.fold show table [] end;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   131
  in
43703
c37a1f29bbc0 standardized String.concat towards implode;
wenzelm
parents: 41491
diff changeset
   132
    implode
33817
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   133
      (["path_info: \"", path_info, "\"\n",
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   134
        "path_translated: \"", path_translated, "\"\n",
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   135
        "script_name: \"", script_name, "\"\n",
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   136
        "request_method: \"", show_req_method request_method, "\"\n",
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   137
        "query_string:\n"]
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   138
       @
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   139
       show_symtab I query_string
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   140
       @
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   141
       ["content_type: ",
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   142
          (the_default "" o Option.map Mime.show_type) content_type, "\n",
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   143
        "environment:\n"]
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   144
       @
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   145
       show_symtab Byte.unpackStringVec environment)
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   146
  end;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   147
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   148
fun test path =
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   149
  let
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   150
    val fin = BinIO.openIn path;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   151
    val (req, cs) = parse fin;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   152
    val () = TextIO.print (show req);
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   153
    val () =
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   154
      BinIO.inputN cs
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   155
      |> Word8VectorSlice.full
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   156
      |> Byte.unpackStringVec
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   157
      |> TextIO.print;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   158
  in BinIO.closeIn fin end;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   159
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   160
end;
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
   161