tricu

0e9b65a67a02911e0fc4e6e4fed4275207d60af7ec236bae97a59b16d86df066.tri (23863B)

---

 !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)
 
 -- 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
 -- ---------------------------------------------------------------------------
 
 bit0? = (x :
   isZero? x)
 
 bit1? = (x :
   triage
     false
     (a : isZero? a)
     (_ _ : false)
     x)
 
 low3 = (b0 b1 b2 :
   matchBool
     (matchBool
       (matchBool 7 6 (bit1? b0))
       (matchBool 5 4 (bit1? b0))
       (bit1? b1))
     (matchBool
       (matchBool 3 2 (bit1? b0))
       (matchBool 1 0 (bit1? b0))
       (bit1? b1))
     (bit1? b2))
 
 decimalDigit = (c :
   triage
     nothing
     (_ : nothing)
     (b0 r0 :
       triage
         nothing
         (_ : nothing)
         (b1 r1 :
           triage
             nothing
             (_ : nothing)
             (b2 r2 :
               triage
                 nothing
                 (_ : nothing)
                 (b3 r3 :
                   triage
                     nothing
                     (_ : nothing)
                     (b4 r4 :
                       triage
                         nothing
                         (_ : nothing)
                         (b5 r5 :
                           matchBool
                             (matchBool
                               (matchBool
                                 (matchBool
                                   (matchBool
                                     (just (low3 b0 b1 b2))
                                     (matchBool
                                       (matchBool
                                         (just (matchBool 9 8 (bit1? b0)))
                                         nothing
                                         (bit0? b2))
                                       nothing
                                       (bit0? b1))
                                     (bit0? b3))
                                   nothing
                                   (bit1? b5))
                                 nothing
                                 (bit1? b4))
                               nothing
                               (isZero? r5))
                             nothing
                             true)
                         r4)
                     r3)
                 r2)
             r1)
         r0)
     c)
 
 readDecimal_ = (self bytes acc :
   matchList
     (just acc)
     (h r :
       matchMaybe
         nothing
         (d : self r (add (mul acc 10) d))
         (decimalDigit h))
     bytes)
 
 readDecimal = (bytes :
   matchBool
     nothing
     (y readDecimal_ bytes 0)
     (emptyList? bytes))
 
 maxBodyBytesDecimal = "1048576"
 
 byte0? b = equal? b 48
 digitLtMax? maxDigit digit = lt? digit maxDigit
 
 stripLeadingZeros_ self raw =
   lazyList
     (_ : t)
     (c r :
       lazyBool
         (_ : self r)
         (_ : raw)
         (byte0? c))
     raw
 
 decimalLengthLte_ self max raw =
   lazyList
     (_ : true)
     (_ rest :
       lazyList
         (_ : false)
         (_ maxRest : self maxRest rest)
         max)
     raw
 
 decimalSameLength_ self max raw =
   lazyList
     (_ :
       lazyList
         (_ : true)
         (_ _ : false)
         max)
     (_ rest :
       lazyList
         (_ : false)
         (_ maxRest : self maxRest rest)
         max)
     raw
 
 sameLengthDecimalLte_ self max raw less =
   lazyList
     (_ : true)
     (digit rest :
       lazyList
         (_ : false)
         (maxDigit maxRest :
           lazyBool
             (_ : self maxRest rest true)
             (_ :
               lazyBool
                 (_ : self maxRest rest true)
                 (_ :
                   lazyBool
                     (_ : self maxRest rest false)
                     (_ : false)
                     (equal? digit maxDigit))
                 (digitLtMax? maxDigit digit))
             less)
         max)
     raw
 
 decimalLengthLte? max raw = y decimalLengthLte_ max raw
 
 decimalSameLength? max raw = y decimalSameLength_ max raw
 
 decimalBytesLte? max raw =
   let trimmed = y stripLeadingZeros_ raw in
   lazyBool
     (_ : y sameLengthDecimalLte_ max trimmed false)
     (_ : decimalLengthLte? max trimmed)
     (decimalSameLength? max trimmed)
 
 -- This digit predicate reuses the existing structural byte decoder: asking
 -- generic numeric comparisons about abstract byte trees would make importing
 -- this module hang before any request has been received.
 httpDecimalDigit? byte =
   lazyMaybe
     (_ : false)
     (digit : true)
     (decimalDigit byte)
 
 httpDecimalReply =
   parserContext "content-length"
     (parserBind
       (parserLabel "decimal-digit"
         (parserSome (parserSatisfy httpDecimalDigit?)))
       (digits : parserThen
         (parserLabel "end-of-decimal" parserEof)
         (lazyMaybe
           (_ : parserFailure
             (parserDiagnostic 2 "decimal-digit" t t t))
           (number : parserPure number)
           (readDecimal digits))))
 
 -- Retain the earlier validator as an oracle until all header consumers have
 -- been exercised with the generic decimal reply.
 parseContentLengthValueLegacy = (raw :
   matchMaybe
     (err 400 "Bad Request\n")
     (n :
       lazyBool
         (_ : ok (just n) t)
         (_ : err 413 "Request body too large\n")
         (decimalBytesLte? maxBodyBytesDecimal raw))
     (readDecimal raw))
 
 parseContentLengthValue = (raw :
   parserMatchReply
     (diagnostic rest consumed committed : err 400 "Bad Request\n")
     (n rest consumed committed :
       lazyBool
         (_ : ok (just n) t)
         (_ : err 413 "Request body too large\n")
         (decimalBytesLte? maxBodyBytesDecimal raw))
     (httpDecimalReply raw))
 
 contentLength_ = (self headers :
   matchList
     (ok nothing t)
     (h r :
       matchBool
         (parseContentLengthValue (snd h))
         (self r)
         (equal? "content-length" (fst h)))
     headers)
 
 contentLength = (headers :
   y contentLength_ headers)
 
 -- ---------------------------------------------------------------------------
 --  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)))