!import "prelude.tri"     !Local
!import "io.tri"          !Local
!import "socket.tri"      !Local

-- ---------------------------------------------------------------------------
--  Constants
-- ---------------------------------------------------------------------------

maxHeaderBytes = 65536
maxBodyBytes = 1048576
maxUriBytes = 8192

crlf = pair 13 (pair 10 t)
crlfcrlf = pair 13 (pair 10 (pair 13 (pair 10 t)))

-- ---------------------------------------------------------------------------
--  Small byte/list helpers
-- ---------------------------------------------------------------------------

chomp = (xs :
  lazyList
    (_ : t)
    (h r :
      lazyBool
        (_ : reverse r)
        (_ : xs)
        (equal? h 13))
    (reverse xs))

-- ---------------------------------------------------------------------------
--  Response construction
-- ---------------------------------------------------------------------------

statusPhrase = (code :
  lazyBool
    (_ : "OK")
    (_ :
      lazyBool
        (_ : "Created")
        (_ :
          lazyBool
            (_ : "No Content")
            (_ :
              lazyBool
                (_ : "Bad Request")
                (_ :
                  lazyBool
                    (_ : "Not Found")
                    (_ :
                      lazyBool
                        (_ : "Method Not Allowed")
                        (_ :
                          lazyBool
                            (_ : "Request Header Fields Too Large")
                            (_ :
                              lazyBool
                                (_ : "Not Implemented")
                                (_ :
                                  lazyBool
                                    (_ : "HTTP Version Not Supported")
                                    (_ : "Internal Server Error")
                                    (equal? code 505))
                                (equal? code 501))
                            (equal? code 431))
                        (equal? code 405))
                    (equal? code 404))
                (equal? code 400))
            (equal? code 204))
        (equal? code 201))
    (equal? code 200))

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)

headersOnly_ = (y (self bs s1 s2 s3 acc :
  lazyList
    (_ : reverse acc)
    (h r :
      lazyBool
        (_ :
          lazyBool
            (_ :
              lazyBool
                (_ :
                  lazyBool
                    (_ : reverse (pair 10 (pair 13 (pair 10 (pair 13 acc)))))
                    (_ : self r true false false (pair h acc))
                    (equal? h 10))
                (_ : self r false false false (pair h acc))
                s3)
            (_ : self r false true false (pair h acc))
            (and? s2 (equal? h 13)))
        (_ :
          lazyBool
            (_ : self r false false true (pair h acc))
            (_ : self r false false false (pair h acc))
            (and? s1 (equal? h 10)))
        (equal? h 13))
    bs))

headersOnly = (response :
  headersOnly_ response false false false 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 1)
    (err :
      pure (err 400 acc))
    (chunk :
      lazyBool
        (_ : pure (err 400 acc))
        (_ :
          ((chunkLen :
            ((nextLen :
              ((next :
                lazyBool
                  (_ :
                    lazyBool
                      (_ : pure (ok next t))
                      (_ : self sock pattern maxBytes next nextLen)
                      (contains? pattern next))
                  (_ : pure (err 431 next))
                  (lte? nextLen maxBytes))
               (append acc chunk)))
             (add accLen chunkLen)))
           (length chunk)))
        (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
-- ---------------------------------------------------------------------------

readLineBytes_ = (y (self bs acc :
  lazyList
    (_ : pair (reverse acc) t)
    (h r :
      lazyBool
        (_ : pair (reverse acc) r)
        (_ :
          lazyBool
            (_ : self r acc)
            (_ : self r (pair h acc))
            (equal? h 13))
        (equal? h 10))
    bs))

readLineBytes = (bs :
  ((result :
    pair (chomp (fst result)) (snd result))
   (readLineBytes_ bs t)))

parseThreeWords_ = (y (self bs phase acc w1 w2 :
  lazyList
    (_ :
      lazyBool
        (_ : ok (pair w1 (pair w2 (reverse acc))) t)
        (_ : err 400 "Bad Request\n")
        (equal? phase 2))
    (h r :
      lazyBool
        (_ :
          lazyBool
            (_ : self r 1 t (reverse acc) w2)
            (_ :
              lazyBool
                (_ : self r 2 t w1 (reverse acc))
                (_ : err 400 "Bad Request\n")
                (equal? phase 1))
            (equal? phase 0))
        (_ : self r phase (pair h acc) w1 w2)
        (equal? h 32))
    bs))

parseThreeWords = (bs :
  parseThreeWords_ bs 0 t t t)

parseRequestLine = (bs :
  ((lineRest :
    lazyResult
      (code bad : err 400 "Bad Request\n")
      (req ignored : ok req (snd lineRest))
      (parseThreeWords (fst lineRest)))
   (readLineBytes bs)))

-- ---------------------------------------------------------------------------
--  Header parsing
-- ---------------------------------------------------------------------------


-- ASCII byte helpers below are structural on the Tree Calculus numeral
-- spine. Do not replace them with lte?/sub based checks: these names are
-- normalized at import time under abstract byte inputs.
boolNot? = (b :
  matchBool false true b)

boolOr? = (a b :
  matchBool true b a)

boolAnd? = (a b :
  matchBool b false a)

low5NonZero? = (b0 b1 b2 b3 b4 :
  boolOr?
    (bit1? b0)
    (boolOr?
      (bit1? b1)
      (boolOr?
        (bit1? b2)
        (boolOr?
          (bit1? b3)
          (bit1? b4)))))

low5TooHighForUpper? = (b0 b1 b2 b3 b4 :
  boolAnd?
    (bit1? b4)
    (boolAnd?
      (bit1? b3)
      (boolOr?
        (bit1? b2)
        (boolAnd?
          (bit1? b1)
          (bit1? b0)))))

upperLow5? = (b0 b1 b2 b3 b4 :
  boolAnd?
    (low5NonZero? b0 b1 b2 b3 b4)
    (boolNot?
      (low5TooHighForUpper? b0 b1 b2 b3 b4)))

lowerAsciiBits = (b0 b1 b2 b3 b4 :
  pair b0
    (pair b1
      (pair b2
        (pair b3
          (pair b4
            (pair true
              (pair true 0)))))))

toLowerAsciiByte = (c :
  triage
    c
    (_ : c)
    (b0 r0 :
      triage
        c
        (_ : c)
        (b1 r1 :
          triage
            c
            (_ : c)
            (b2 r2 :
              triage
                c
                (_ : c)
                (b3 r3 :
                  triage
                    c
                    (_ : c)
                    (b4 r4 :
                      triage
                        c
                        (_ : c)
                        (b5 r5 :
                          triage
                            c
                            (_ : c)
                            (b6 r6 :
                              matchBool
                                (lowerAsciiBits b0 b1 b2 b3 b4)
                                c
                                (boolAnd?
                                  (isZero? r6)
                                  (boolAnd?
                                    (bit1? b6)
                                    (boolAnd?
                                      (bit0? b5)
                                      (upperLow5? b0 b1 b2 b3 b4)))))
                            r5)
                        r4)
                    r3)
                r2)
            r1)
        r0)
    c)

finishHeaderLine = (self r headers key value seenColon :
  matchBool
    (matchBool
      (err 400 "Bad Request\n")
      (ok (reverse headers) r)
      seenColon)
    (matchBool
      (self r
        (pair (pair (reverse key) (reverse value)) headers)
        t
        t
        false
        true)
      (err 400 "Bad Request\n")
      seenColon)
    (emptyList? key))

finishHeaderEOF = (headers key value seenColon :
  matchBool
    (ok (reverse headers) t)
    (matchBool
      (ok (reverse (pair (pair (reverse key) (reverse value)) headers)) t)
      (err 400 "Bad Request\n")
      seenColon)
    (emptyList? key))

parseHeaders_ = (self bs headers key value seenColon trimValue :
  matchList
    (finishHeaderEOF headers key value seenColon)
    (h r :
      matchBool
        (finishHeaderLine self r headers key value seenColon)
        (matchBool
          (self r headers key value seenColon trimValue)
          (matchBool
            (matchBool
              (self r headers key value true true)
              (self r headers key (pair h value) true false)
              (boolAnd? trimValue (equal? h 32)))
            (matchBool
              (self r headers key value true true)
              (self r headers (pair (toLowerAsciiByte h) key) value false true)
              (equal? h 58))
            seenColon)
          (equal? h 13))
        (equal? h 10))
    bs)

parseHeaders = (bs :
  y parseHeaders_ bs t t t false true)

-- ---------------------------------------------------------------------------
--  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))

parseContentLengthValue = (raw :
  matchMaybe
    (err 400 "Bad Request\n")
    (n : ok (just n) t)
    (readDecimal 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)

readBodyRecv = (self sock remaining accRev recvBytes :
  onResult_ (recv sock recvBytes)
    (errMsg :
      pure
        (err
          400
          (append "recv failed while reading body: " errMsg)))
    (chunk :
      ((state :
        ((nextRemaining :
          ((nextAccRev :
            lazyBool
              (_ : pure (ok (reverse nextAccRev) (bodyReadRest state)))
              (_ : self sock nextRemaining nextAccRev)
              (isZero? nextRemaining))
           (bodyReadAccRev state)))
         (bodyReadRemaining state)))
       (takeBodyBytes chunk remaining accRev))))

readBodyMore_ = (self sock remaining accRev :
  lazyBool
    (_ : pure (ok (reverse accRev) t))
    (_ :
      lazyBool
        (_ : readBodyRecv self sock remaining accRev 4096)
        (_ :
          lazyBool
            (_ : readBodyRecv self sock remaining accRev 1024)
            (_ :
              lazyBool
                (_ : readBodyRecv self sock remaining accRev 256)
                (_ :
                  lazyBool
                    (_ : readBodyRecv self sock remaining accRev 64)
                    (_ :
                      lazyBool
                        (_ : readBodyRecv self sock remaining accRev 16)
                        (_ : readBodyRecv self sock remaining accRev 1)
                        (lte? 16 remaining))
                    (lte? 64 remaining))
                (lte? 256 remaining))
            (lte? 1024 remaining))
        (lte? 4096 remaining))
    (isZero? remaining))

readBodyMore = (sock remaining accRev :
  y readBodyMore_ sock remaining accRev)

readBodyExact = (sock expected initialBytes :
  ((state :
    ((remaining :
      ((accRev :
        lazyBool
          (_ : pure (ok (reverse accRev) (bodyReadRest state)))
          (_ : readBodyMore sock remaining accRev)
          (isZero? remaining))
       (bodyReadAccRev state)))
     (bodyReadRemaining state)))
   (takeBodyBytes initialBytes expected t)))

validateBodyLength = (expected body rest :
  ((actual :
    lazyBool
      (_ : pure (ok body rest))
      (_ :
        pure
          (err
            400
            (append
              "body length mismatch expected="
              (append
                (showNumber expected)
                (append
                  " actual="
                  (showNumber actual))))))
      (equal? actual expected))
   (length body)))

readBody = (sock headers initialBytes :
  matchResult
    (status msg :
      pure (err status msg))
    (maybeLen rest :
      lazyMaybe
        (_ : pure (ok t initialBytes))
        (n :
          lazyBool
            (_ :
              onOk (readBodyExact sock n initialBytes)
                (body rest :
                  validateBodyLength n body rest))
            (_ : pure (err 400 "Request body too large\n"))
            (lte? n maxBodyBytes))
        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)))