feat: add connection data to the connection

Author: algebraic-dev

Http/IO/Server.lean

@@ -15,13 +15,13 @@ open Http.Data.Headers
 open Http.Classes
 open Http.Data
 
-def simpleStatusResponse (status: Status) (conn: Connection) := do
+def simpleStatusResponse (status: Status) (conn: Connection α) := do
   conn.response.modify λres => res
     |>.withHeaderStd .connection ConnectionHeader.close
     |>.withStatus status
   conn.end
 
-def handleError (conn: Connection) : ParsingError → IO Unit
+def handleError (conn: Connection α) : ParsingError → IO Unit
   | .invalidMessage _ => simpleStatusResponse .badRequest conn
   | .uriTooLong => simpleStatusResponse .uriTooLong conn
   | .bodyTooLong => simpleStatusResponse .payloadTooLarge conn
@@ -31,7 +31,7 @@ def handleError (conn: Connection) : ParsingError → IO Unit
 def keepAlive (config: Config) : KeepAlive :=
   KeepAlive.new (some $ config.idleTimeout / 1000) config.maxKeepAliveRequests
 
-def onRequest (config: Config) (connRef: IO.Ref Connection) (onReq: Connection → IO Unit) (request: Request) : IO Bool := do
+def onRequest (config: Config) (connRef: IO.Ref (Connection α)) (onReq: Connection α → IO Unit) (request: Request) : IO Bool := do
   let conn ← connRef.get
   conn.requests.modify (· + 1)
 
@@ -64,17 +64,18 @@ def onRequest (config: Config) (connRef: IO.Ref Connection) (onReq: Connection 
 
   return ¬isClosing
 
-def closeConnectionTimeout (conn: IO.Ref Connection) : IO Unit := do
+def closeConnectionTimeout (conn: IO.Ref (Connection α)) : IO Unit := do
   let connection ← conn.get
   connection.close
 
 def readSocket
   (loop: UV.Loop)
   (config: Config)
   (socket: UV.TCP)
-  (onReq: Connection → IO Unit)
-  (onData: Connection → Chunk → IO Unit)
-  (onTrailer: Connection → Trailers → IO Unit)
+  (onReq: Connection α → IO Unit)
+  (onData: Connection α → Chunk → IO Unit)
+  (onTrailer: Connection α → Trailers → IO Unit)
+  (data : α)
   : UV.IO Unit
   := do
     let timer ← loop.mkTimer
@@ -84,10 +85,10 @@ def readSocket
       socket.read_stop
       socket.stop
 
-    let conn ← Connection.new socket (λ_ => UV.IO.run $ onEnd ())
+    let conn ← Connection.new socket (λ_ => UV.IO.run $ onEnd ()) data
     let connRef ← IO.toUVIO (IO.mkRef conn)
 
-    let readRef : {x y: Type} → (Connection → y → IO x) → y → IO x := λfunc y => do
+    let readRef : {x y: Type} → (Connection α → y → IO x) → y → IO x := λfunc y => do
       let conn ← connRef.get
       func conn y
 
@@ -119,12 +120,14 @@ def readSocket
             IO.toUVIO $ handleError conn err
 
 def server
+  [Inhabited α]
   (host: String)
   (port: UInt16)
   (config: Config := Inhabited.default)
-  (onReq: Connection → IO Unit := (λ_ => pure ()))
-  (onData: Connection → Chunk → IO Unit := (λ_ _ => pure ()))
-  (onEnd: Connection → Trailers → IO Unit := (λ_ _ => pure ()))
+  (onReq: Connection α → IO Unit := (λ_ => pure ()))
+  (onData: Connection α → Chunk → IO Unit := (λ_ _ => pure ()))
+  (onEnd: Connection α → Trailers → IO Unit := (λ_ _ => pure ()))
+  (data : α := Inhabited.default)
   : IO Unit := do
   let go : UV.IO Unit := do
     let loop ← UV.mkLoop
@@ -134,6 +137,6 @@ def server
     server.listen 128 do
       let client ← loop.mkTCP
       server.accept client
-      readSocket loop config client onReq onData onEnd
+      readSocket loop config client onReq onData onEnd data
     let _ ← loop.run
   UV.IO.run go

Http/IO/Server/Connection.lean

@@ -11,7 +11,7 @@ open Http.Data.Headers
 open Http.Data
 open Http.Classes
 
-structure Connection where
+structure Connection (α: Type) where
   isClosing: IO.Ref Bool
   sentHeaders: IO.Ref Bool
   isChunked: IO.Ref Bool
@@ -26,7 +26,9 @@ structure Connection where
   socket: UV.TCP
   onEnd: Unit → IO Unit
 
-def Connection.new (socket: UV.TCP) (onEnd: Unit → IO Unit) : UV.IO Connection := do
+  data: IO.Ref α
+
+def Connection.new (socket: UV.TCP) (onEnd: Unit → IO Unit) (data: α) : UV.IO (Connection α) := do
   return { isClosing := ← IO.mkRef false
          , isHead := ← IO.mkRef false
          , requests := ← IO.mkRef 0
@@ -37,33 +39,34 @@ def Connection.new (socket: UV.TCP) (onEnd: Unit → IO Unit) : UV.IO Connection
          , request := Data.Request.empty
          , buffer := ← IO.mkRef #[ByteArray.empty]
          , response := ← IO.mkRef Data.Response.empty
+         , data := ← IO.mkRef data
          , socket
          , onEnd }
 
-def Connection.guard (connection: Connection) (func: IO Unit) : IO Unit := do
+def Connection.guard (connection: Connection α) (func: IO Unit) : IO Unit := do
   let isClosing ← connection.isClosing.get
   if ¬isClosing then func
 
-def Connection.withHeader (connection: Connection) (name: String) (value: String) : IO Unit := connection.guard do
+def Connection.withHeader (connection: Connection α) (name: String) (value: String) : IO Unit := connection.guard do
   let sentHeaders ← connection.sentHeaders.get
   if sentHeaders then
     throw (IO.userError (toString "cannot write headers after they were sent"))
   connection.response.modify (·.withHeader name value)
 
-def Connection.setStatus (connection: Connection) (status: Status) : IO Unit := connection.guard do
+def Connection.setStatus (connection: Connection α) (status: Status) : IO Unit := connection.guard do
   connection.response.modify ({· with status := status})
 
-def Connection.withHeaderStd (connection: Connection) [Canonical .text α] (name: Headers.HeaderName.Standard) (value: α) [Headers.Header name α] : IO Unit := connection.guard do
+def Connection.withHeaderStd (connection: Connection β) [Canonical .text α] (name: Headers.HeaderName.Standard) (value: α) [Headers.Header name α] : IO Unit := connection.guard do
   let sentHeaders ← connection.sentHeaders.get
   if sentHeaders then
     throw (IO.userError (toString "cannot write headers after they were sent"))
   connection.response.modify (·.withHeaderStd name value)
 
-def Connection.close (connection: Connection) : IO Unit := connection.guard do
+def Connection.close (connection: Connection α) : IO Unit := connection.guard do
   connection.isClosing.set true
   connection.onEnd ()
 
-def Connection.writeByteArray (connection: Connection) (data: ByteArray) : IO Unit := connection.guard do
+def Connection.writeByteArray (connection: Connection α) (data: ByteArray) : IO Unit := connection.guard do
   let isChunked ← connection.isChunked.get
   let data :=
     if isChunked
@@ -72,19 +75,19 @@ def Connection.writeByteArray (connection: Connection) (data: ByteArray) : IO Un
   connection.size.modify (· + data.size)
   connection.buffer.modify (λx => x.push data)
 
-def Connection.write (connection: Connection) (data: String) : IO Unit := connection.guard do
+def Connection.write (connection: Connection α) (data: String) : IO Unit := connection.guard do
   connection.writeByteArray (String.toUTF8 data)
 
-def Connection.rawWrite (connection: Connection) (buffer: Array ByteArray) : IO Unit := connection.guard do
+def Connection.rawWrite (connection: Connection α) (buffer: Array ByteArray) : IO Unit := connection.guard do
   if buffer.size > 0 then
     UV.IO.run do let _ ← connection.socket.write buffer (λ_ => pure ())
 
-def Connection.sendLastChunk (connection: Connection) : IO Unit := connection.guard do
+def Connection.sendLastChunk (connection: Connection α) : IO Unit := connection.guard do
   let isChunked ← connection.isChunked.get
   if isChunked then
     connection.rawWrite #[Canonical.binary Chunk.zeroed]
 
-def Connection.sendHeaders (connection: Connection) : IO Unit := connection.guard do
+def Connection.sendHeaders (connection: Connection α) : IO Unit := connection.guard do
   let sent ← connection.sentHeaders.get
 
   if ¬sent then
@@ -102,12 +105,12 @@ def Connection.sendHeaders (connection: Connection) : IO Unit := connection.guar
     connection.rawWrite #[String.toUTF8 $ Canonical.text response]
     connection.sentHeaders.set true
 
-def Connection.flush (connection: Connection) : IO Unit := connection.guard do
+def Connection.flush (connection: Connection α) : IO Unit := connection.guard do
   connection.sendHeaders
   let buffer ← connection.buffer.swap #[]
   connection.rawWrite buffer
 
-def Connection.end (connection: Connection) : IO Unit := connection.guard do
+def Connection.end (connection: Connection α) : IO Unit := connection.guard do
   connection.flush
   connection.sendLastChunk