tricu

2c0ccdaabea661d7288e7faf58dbbdb9f0823f8929892391d2402200d87993b9.tri (20373B)

---

 !import prelude *
 !import io *
 !import patterns *
 !import socket *
 !import parser *
 !import native_math as Nat
 !export *
 
 -- ---------------------------------------------------------------------------
 --  Constants
 -- ---------------------------------------------------------------------------
 
 maxHeaderBytes = 65536
 maxBodyBytes = 1048576
 maxUriBytes = 8192
 
 crlf = pair 13 (pair 10 t)
 crlfcrlf = pair 13 (pair 10 (pair 13 (pair 10 t)))
 
 -- ---------------------------------------------------------------------------
 --  Response construction
 -- ---------------------------------------------------------------------------
 
 statusPhrases =
   [(pair 200 "OK")
    (pair 201 "Created")
    (pair 204 "No Content")
    (pair 400 "Bad Request")
    (pair 404 "Not Found")
    (pair 405 "Method Not Allowed")
    (pair 431 "Request Header Fields Too Large")
    (pair 501 "Not Implemented")
    (pair 505 "HTTP Version Not Supported")]
 
 lookupStatusPhrase_ self code phrases =
   lazyList
     (_ : "Internal Server Error")
     (h r :
       lazyBool
         (_ : snd h)
         (_ : self code r)
         (equal? code (fst h)))
     phrases
 
 statusPhrase = (code :
   y lookupStatusPhrase_ code statusPhrases)
 
 statusLine = (code phrase :
   append "HTTP/1.1 " (append (showNumber code) (append " " (append phrase "\r\n"))))
 
 headerLine = (key value :
   append key (append ": " (append value "\r\n")))
 
 buildResponse = (status headers body :
   append
     (statusLine status (statusPhrase status))
     (append
       (foldl (acc h : append acc (headerLine (fst h) (snd h))) "" headers)
       (append "\r\n" body)))
 
 response = (status contentType body :
   buildResponse status
     [(pair "Content-Type" contentType)
      (pair "Content-Length" (showNumber (length body)))
      (pair "Connection" "close")]
     body)
 
 emptyResponse = (status :
   buildResponse status
     [(pair "Content-Length" "0")
      (pair "Connection" "close")]
     "")
 
 okResponse = (body :
   response 200 "text/plain; charset=utf-8" body)
 
 textResponse = (body :
   response 200 "text/plain; charset=utf-8" body)
 
 jsonResponse = (body :
   response 200 "application/json" body)
 
 htmlResponse = (body :
   response 200 "text/html; charset=utf-8" body)
 
 createdResponse = (body :
   response 201 "text/plain; charset=utf-8" body)
 
 notFoundResponse = (
   response 404 "text/plain; charset=utf-8" "Not found\n")
 
 badRequestResponse = (msg :
   response 400 "text/plain; charset=utf-8" msg)
 
 errorResponse = (status msg :
   response status "text/plain; charset=utf-8" msg)
 
 headerEndState state h =
   lazyBool
     (_ :
       lazyBool
         (_ : 3)
         (_ : 1)
         (equal? state 2))
     (_ :
       lazyBool
         (_ :
           lazyBool
             (_ : 4)
             (_ : 2)
             (equal? state 3))
         (_ : 0)
         (boolAnd?
           (equal? h 10)
           (boolOr? (equal? state 1) (equal? state 3))))
     (equal? h 13)
 
 headersOnly_ self bs state acc =
   lazyList
     (_ : reverse acc)
     (h r :
       let nextAcc = pair h acc in
       let nextState = headerEndState state h in
       lazyBool
         (_ : reverse nextAcc)
         (_ : self r nextState nextAcc)
         (equal? nextState 4))
     bs
 
 headersOnly = (response :
   y headersOnly_ response 0 t)
 
 responseForMethod = (method resp :
   lazyBool
     (_ : headersOnly resp)
     (_ : resp)
     (equal? method "HEAD"))
 
 -- ---------------------------------------------------------------------------
 --  Header receive / framing
 -- ---------------------------------------------------------------------------
 
 recvUntilMax_ = (y (self sock pattern maxBytes acc accLen :
   onResult_ (recv sock 4096)
     (err :
       pure (err 400 acc))
     (chunk :
       lazyBool
         (_ : pure (err 400 acc))
         (_ :
           let chunkLen = length chunk in
           let nextLen = add accLen chunkLen in
           let next = append acc chunk in
           lazyBool
             (_ :
               lazyBool
                 (_ : pure (ok next t))
                 (_ : self sock pattern maxBytes next nextLen)
                 (contains? pattern next))
             (_ : pure (err 431 next))
             (lte? nextLen maxBytes))
         (emptyList? chunk))))
 
 recvUntilMax = (sock pattern maxBytes :
   recvUntilMax_ sock pattern maxBytes t 0)
 
 recvUntil = (sock pattern :
   recvUntilMax sock pattern maxHeaderBytes)
 
 recvHeaders = (sock :
   recvUntilMax sock crlfcrlf maxHeaderBytes)
 
 -- ---------------------------------------------------------------------------
 --  Request line parsing
 -- ---------------------------------------------------------------------------
 
 -- HTTP/1.1 lines require CRLF. A bare CR/LF is an error, never a byte to
 -- discard. Failure retains the offending suffix and prior consumption; EOF
 -- cannot masquerade as a successfully parsed empty line.
 httpLineError code found rest consumed = (parserReplyFail
   (parserDiagnostic code "CRLF" found t ["http-line"])
   rest consumed false)
 
 httpScanLine [13 10 | rest] reversed = parserReplyOk (reverse reversed) rest true false
 httpScanLine input{[13 | _]} reversed = httpLineError 2 13 input (not? (emptyList? reversed))
 httpScanLine input{[10 | _]} reversed = httpLineError 2 10 input (not? (emptyList? reversed))
 httpScanLine [byte | rest] reversed = httpScanLine rest (pair byte reversed)
 httpScanLine [] reversed = httpLineError 1 t [] (not? (emptyList? reversed))
 httpScanLine input reversed = httpLineError 2 input input (not? (emptyList? reversed))
 
 httpLineReply input = httpScanLine input []
 httpBadRequest = err 400 "Bad Request\n"
 
 -- Unlike the old pair-only helper, this Result distinguishes a blank CRLF
 -- line from truncated/malformed input. Both callers propagate the failure.
 readLineBytes input = (parserMatchReply
   (_ _ _ _ : httpBadRequest)
   (line rest _ _ : ok line rest)
   (httpLineReply input))
 
 -- The finite request line is already framed by readLineBytes. Deliberately
 -- retain the historical three-fields grammar: empty fields are permitted,
 -- but a third separating space is an error. The parser reply exposes byte
 -- consumption to new clients, while parseThreeWords preserves HTTP's public
 -- Result/400 boundary and the original "Bad Request" remainder.
 httpNonSpace? byte = not? (equal? byte 32)
 
 httpThreeWordsReply =
   parserContext "request-line"
     (parserBind (parserTakeWhile httpNonSpace?) (method :
       parserThen (parserExpect 32)
         (parserBind (parserTakeWhile httpNonSpace?) (target :
           parserThen (parserExpect 32)
             (parserBind (parserTakeWhile httpNonSpace?) (version :
               parserMap (_ : pair method (pair target version))
                 parserEof))))))
 
 parseThreeWords = (bs :
   parserMatchReply
     (diagnostic rest consumed committed : err 400 "Bad Request\n")
     (words rest consumed committed : ok words rest)
     (httpThreeWordsReply bs))
 
 parseRequestLine input = (let
   parseLine ((t t), (line, rest)) = (lazyResult
     (_ _ : httpBadRequest)
     (request _ : ok request rest)
     (parseThreeWords line))
   parseLine _ = httpBadRequest
   in parseLine (readLineBytes input))
 
 -- ---------------------------------------------------------------------------
 --  Header parsing
 -- ---------------------------------------------------------------------------
 
 
 boolOr? = (a b :
   matchBool true b a)
 
 boolAnd? = (a b :
   matchBool b false a)
 
 bit0? = (x :
   isZero? x)
 
 bit1? = (x :
   triage
     false
     (a : isZero? a)
     (_ _ : false)
     x)
 
 -- Preserve the old bit predicate's truthiness, even for malformed bit trees.
 httpAsciiBit bit = matchBool true false (bit1? bit)
 
 -- Uppercase ASCII is 65..90. For byte inputs the normalized code below is
 -- the input itself once the high-bit checks pass. Keep original low-bit trees
 -- in the result: the historical helper also accepts some malformed bit trees,
 -- and this readability rewrite does not change that policy.
 toLowerAsciiByte byte{[b0 b1 b2 b3 b4 b5 b6 | rest]} = (let
   code = [(httpAsciiBit b0) (httpAsciiBit b1) (httpAsciiBit b2)
           (httpAsciiBit b3) (httpAsciiBit b4) false true]
   lower ^true = [b0 b1 b2 b3 b4 true true]
   lower _ = byte
   in lower (and? (isZero? rest)
     (and? (bit1? b6) (and? (bit0? b5)
       (Nat.inRange code 65 90)))))
 toLowerAsciiByte byte = byte
 
 -- RFC 9110 token names, OWS, and field-value bytes. obs-text (128..255)
 -- stays opaque; only the ASCII header name is lowercased. Reject obs-fold.
 httpTokenByte? byte = (or? (Nat.letter byte)
   (or? (Nat.digit byte) (any? (equal? byte) "!#$%&'*+-.^_`|~")))
 httpOws? byte = or? (equal? byte 32) (equal? byte 9)
 httpFieldByte? byte = (or? (equal? byte 9)
   (or? (Nat.printable byte) (Nat.inRange byte 128 255)))
 httpTrimOws value = reverse (dropWhile httpOws? (reverse (dropWhile httpOws? value)))
 
 -- Parse exactly one finite line, excluding CRLF. Preserve parser diagnostics
 -- and consumption, but never accept a valid prefix followed by invalid bytes.
 httpHeaderLineReply = (parserContext "header-line"
     (parserBind
       (parserLabel "header-name"
         (parserSome (parserSatisfy httpTokenByte?)))
       (name : parserThen (parserLabel "colon" (parserExpect 58))
         (parserMap (value : pair (map toLowerAsciiByte name)
           (httpTrimOws value))
           (parserLabel "header-value"
             (parserBefore (parserTakeWhile httpFieldByte?) parserEof))))))
 
 -- Only an actual empty CRLF line ends the headers. The returned suffix is
 -- opaque body data, even if it contains CR, LF, NUL or header-looking bytes.
 httpParseHeaderLines input reversedHeaders = (let
   parseLine ((t t), ([], rest)) = ok (reverse reversedHeaders) rest
   parseLine ((t t), (line, rest)) = (let
     continue ((t t), (header, _)) = httpParseHeaderLines rest (pair header reversedHeaders)
     continue _ = httpBadRequest
     in continue (httpHeaderLineReply line))
   parseLine _ = httpBadRequest
   in parseLine (readLineBytes input))
 
 parseHeaders input = httpParseHeaderLines input []
 
 -- ---------------------------------------------------------------------------
 --  Content-Length parsing
 -- ---------------------------------------------------------------------------
 
 -- The accumulator never exceeds maxBodyBytes. A single checked step can
 -- reach at most 10 * maxBodyBytes + 9; after that, validate digits without
 -- constructing a larger number. Trailing junk still means 400, not 413.
 httpBodyTooLarge = err 413 "Request body too large\n"
 
 httpLengthOverflow [] = httpBodyTooLarge
 httpLengthOverflow [byte | rest] = (let
   continue ^true = httpLengthOverflow rest
   continue _ = httpBadRequest
   in continue (Nat.digit byte))
 httpLengthOverflow _ = httpBadRequest
 
 httpLengthDigits [] value = ok (just value) t
 httpLengthDigits [byte | rest] value = (let
   digit ^true = (let
     next = Nat.decimal value (Nat.subtract byte 48)
     bounded ^true = httpLengthDigits rest next
     bounded _ = httpLengthOverflow rest
     in bounded (Nat.lte next maxBodyBytes))
   digit _ = httpBadRequest
   in digit (Nat.digit byte))
 httpLengthDigits _ _ = httpBadRequest
 
 -- Input is a finite canonical byte list, with no OWS: parseHeaders already
 -- trims field edges. Empty strings, signs, commas and interior whitespace fail.
 parseContentLengthValue input{[_ | _]} = httpLengthDigits input 0
 parseContentLengthValue _ = httpBadRequest
 
 -- Input names are normalized by parseHeaders. Select the sole raw length
 -- before decoding: duplicate fields and unsupported transfer coding are 400
 -- regardless of field order or whether a length would otherwise exceed limits.
 -- This server supports Content-Length framing only, not chunked decoding.
 httpSelectLength [] t = ok nothing t
 httpSelectLength [] (t value) = parseContentLengthValue value
 httpSelectLength [("transfer-encoding", _) | _] _ = httpBadRequest
 httpSelectLength [("content-length", value) | rest] t = httpSelectLength rest (just value)
 httpSelectLength [("content-length", _) | _] _ = httpBadRequest
 httpSelectLength [(_, _) | rest] selected = httpSelectLength rest selected
 httpSelectLength _ _ = httpBadRequest
 
 contentLength headers = httpSelectLength headers nothing
 
 -- ---------------------------------------------------------------------------
 --  Body reading
 -- ---------------------------------------------------------------------------
 
 bodyReadState = (remaining accRev rest :
   pair remaining (pair accRev rest))
 
 bodyReadRemaining = (state :
   fst state)
 
 bodyReadAccRev = (state :
   fst (snd state))
 
 bodyReadRest = (state :
   snd (snd state))
 
 takeBodyBytes_ = (self bytes remaining accRev :
   lazyBool
     (_ : bodyReadState 0 accRev bytes)
     (_ :
       lazyList
         (_ : bodyReadState remaining accRev t)
         (h r :
           self r (pred remaining) (pair h accRev))
         bytes)
     (isZero? remaining))
 
 takeBodyBytes = (bytes remaining accRev :
   y takeBodyBytes_ bytes remaining accRev)
 
 shiftRight1 n = triage 0 (_ : 0) (_ rest : rest) n
 
 shiftRight2 n = shiftRight1 (shiftRight1 n)
 shiftRight4 n = shiftRight2 (shiftRight2 n)
 shiftRight8 n = shiftRight4 (shiftRight4 n)
 shiftRight12 n = shiftRight4 (shiftRight8 n)
 
 shiftRight6 n = shiftRight2 (shiftRight4 n)
 
 atLeast16? n = not? (isZero? (shiftRight4 n))
 atLeast64? n = not? (isZero? (shiftRight6 n))
 atLeast256? n = not? (isZero? (shiftRight8 n))
 atLeast1024? n = not? (isZero? (shiftRight2 (shiftRight8 n)))
 atLeast4096? n = not? (isZero? (shiftRight12 n))
 
 recvChunkMax4096 remaining =
   lazyBool
     (_ : 4096)
     (_ :
       lazyBool
         (_ : 1024)
         (_ :
           lazyBool
             (_ : 256)
             (_ :
               lazyBool
                 (_ : 64)
                 (_ :
                   lazyBool
                     (_ : 16)
                     (_ : 1)
                     (atLeast16? remaining))
                 (atLeast64? remaining))
             (atLeast256? remaining))
         (atLeast1024? remaining))
     (atLeast4096? remaining)
 
 readBodyRecv = (self sock remaining accRev recvBytes :
   onResult_ (recv sock recvBytes)
     (errMsg :
       pure
         (err
           400
           (append "recv failed while reading body: " errMsg)))
     (chunk :
       let state = takeBodyBytes chunk remaining accRev in
       let nextRemaining = bodyReadRemaining state in
       let nextAccRev = bodyReadAccRev state in
       lazyBool
         (_ : pure (ok (reverse nextAccRev) (bodyReadRest state)))
         (_ : self sock nextRemaining nextAccRev)
         (isZero? nextRemaining)))
 
 readBodyMore_ = (self sock remaining accRev :
   lazyBool
     (_ : pure (ok (reverse accRev) t))
     (_ : readBodyRecv self sock remaining accRev (recvChunkMax4096 remaining))
     (isZero? remaining))
 
 readBodyMore = (sock remaining accRev :
   y readBodyMore_ sock remaining accRev)
 
 readBodyExact = (sock expected initialBytes :
   let state = takeBodyBytes initialBytes expected t in
   let remaining = bodyReadRemaining state in
   let accRev = bodyReadAccRev state in
   lazyBool
     (_ : pure (ok (reverse accRev) (bodyReadRest state)))
     (_ : readBodyMore sock remaining accRev)
     (isZero? remaining))
 
 validateBodyLength = (expected body rest :
   let actual = length body in
   lazyBool
     (_ : pure (ok body rest))
     (_ :
       pure
         (err
           400
           (append
             "body length mismatch expected="
             (append
               (showNumber expected)
               (append
                 " actual="
                 (showNumber actual))))))
     (equal? actual expected))
 
 readBody = (sock headers initialBytes :
   matchResult
     (status msg :
       pure (err status msg))
     (maybeLen rest :
       lazyMaybe
         (_ : pure (ok t initialBytes))
         (n :
           onOk (readBodyExact sock n initialBytes)
             (body rest :
               validateBodyLength n body rest))
         maybeLen)
     (contentLength headers))
 
 -- ---------------------------------------------------------------------------
 -- Request validation
 -- ---------------------------------------------------------------------------
 
 validMethod? = (method :
   lazyBool
     (_ : true)
     (_ :
       lazyBool
         (_ : true)
         (_ :
           lazyBool
             (_ : true)
             (_ : false)
             (equal? method "HEAD"))
         (equal? method "POST"))
     (equal? method "GET"))
 
 validVersion? = (version :
   lazyBool
     (_ : true)
     (_ : equal? version "HTTP/1.0")
     (equal? version "HTTP/1.1"))
 
 validTarget? = (target :
   startsWith? "/" target)
 
 validateRequest = (method target version headers :
   lazyBool
     (_ :
       lazyBool
         (_ :
           lazyBool
             (_ : ok t t)
             (_ : err 400 "Bad Request\n")
             (validTarget? target))
         (_ : err 505 "HTTP Version Not Supported\n")
         (validVersion? version))
     (_ : err 400 "Bad Request\n")
     (validMethod? method))
 
 -- ---------------------------------------------------------------------------
 -- 11. Handler pipeline
 -- ---------------------------------------------------------------------------
 
 routerMethod = (method :
   lazyBool
     (_ : "GET")
     (_ : method)
     (equal? method "HEAD"))
 
 respondAndClose = (sock resp :
   onOk_ (finally (send sock resp) (closeSocket_ sock)) (_ :
     pure (ok t t)))
 
 handleReadableRequest = (router client method target headers rest3 :
   onResult (readBody client headers rest3)
     (status msg :
       respondAndClose client
         (responseForMethod method
           (errorResponse status msg)))
     (body rest :
       respondAndClose client
         (responseForMethod method
           (router (routerMethod method) target headers body))))
 
 handleParsedHeaders = (router client method target version rest2 :
   matchResult
     (code bad :
       respondAndClose client (badRequestResponse "Bad Request\n"))
     (headers rest3 :
       matchResult
         (status msg :
           respondAndClose client
             (responseForMethod method (errorResponse status msg)))
         (ignored rest :
           handleReadableRequest router client method target headers rest3)
         (validateRequest method target version headers))
     (parseHeaders rest2))
 
 handleParsedRequest = (router client req rest2 :
   ((method :
     ((target :
       ((version :
         handleParsedHeaders router client method target version rest2)
        (snd (snd req))))
      (fst (snd req))))
    (fst req)))
 
 httpHandler = (router client peer :
   onResult_ (recvHeaders client)
     (status :
       respondAndClose client
         (badRequestResponse "Bad Request\n"))
     (raw :
       matchResult
         (code bad :
           respondAndClose client (badRequestResponse "Bad Request\n"))
         (req rest2 :
           handleParsedRequest router client req rest2)
         (parseRequestLine raw)))
 
 -- ---------------------------------------------------------------------------
 -- 12. IO-aware handler pipeline
 -- ---------------------------------------------------------------------------
 
 handleReadableRequestIO = (routerIO client method target headers rest3 :
   onResult (readBody client headers rest3)
     (status msg :
       respondAndClose client
         (responseForMethod method
           (errorResponse status msg)))
     (body rest :
       bind (routerIO (routerMethod method) target headers body) (resp :
         respondAndClose client (responseForMethod method resp))))
 
 handleParsedHeadersIO = (routerIO client method target version rest2 :
   matchResult
     (code bad :
       respondAndClose client (badRequestResponse "Bad Request\n"))
     (headers rest3 :
       matchResult
         (status msg :
           respondAndClose client
             (responseForMethod method (errorResponse status msg)))
         (ignored rest :
           handleReadableRequestIO routerIO client method target headers rest3)
         (validateRequest method target version headers))
     (parseHeaders rest2))
 
 handleParsedRequestIO = (routerIO client req rest2 :
   ((method :
     ((target :
       ((version :
         handleParsedHeadersIO routerIO client method target version rest2)
        (snd (snd req))))
      (fst (snd req))))
    (fst req)))
 
 httpHandlerIO = (routerIO client peer :
   onResult_ (recvHeaders client)
     (status :
       respondAndClose client
         (badRequestResponse "Bad Request\n"))
     (raw :
       matchResult
         (code bad :
           respondAndClose client (badRequestResponse "Bad Request\n"))
         (req rest2 :
           handleParsedRequestIO routerIO client req rest2)
         (parseRequestLine raw)))