feat: request type has request target

Author: algebraic-dev

src/Std/Internal/Http/Data/Request.lean

@@ -9,6 +9,7 @@ prelude
 public import Std.Internal.Http.Data.Method
 public import Std.Internal.Http.Data.Version
 public import Std.Internal.Http.Data.Headers
+public import Std.Internal.Http.Data.URI
 
 public section
 
@@ -40,7 +41,7 @@ structure Request.Head where
   /--
   The request target/URI indicating the resource being requested
   -/
-  uri : String := ""
+  uri : RequestTarget := .asteriskForm
 
   /--
   Collection of HTTP headers for the request (Content-Type, Authorization, etc.)
@@ -88,7 +89,7 @@ instance : Encode .v11 Head where
   encode buffer req :=
     let buffer := Encode.encode (v := .v11) buffer req.method
     let buffer := buffer.writeChar ' '
-    let buffer := buffer.writeString req.uri
+    let buffer := Encode.encode (v := .v11) buffer req.uri
     let buffer := buffer.writeChar ' '
     let buffer := Encode.encode (v := .v11) buffer req.version
     let buffer := buffer.writeString "\r\n"
@@ -124,9 +125,16 @@ def version (builder : Builder) (version : Version) : Builder :=
 /--
 Sets the request target/URI for the request being built
 -/
-def uri (builder : Builder) (uri : String) : Builder :=
+def uri (builder : Builder) (uri : RequestTarget) : Builder :=
   { builder with head := { builder.head with uri := uri } }
 
+/--
+Sets the request target/URI for the request being built
+-/
+def uri! (builder : Builder) (uri : String) : Builder :=
+  let uri := RequestTarget.parse! uri
+  { builder with head := { builder.head with uri } }
+
 /--
 Sets the headers for the request being built
 -/
@@ -166,39 +174,39 @@ end Builder
 /--
 Creates a new HTTP GET Request with the specified URI
 -/
-def get (uri : String) : Builder :=
+def get (uri : RequestTarget) : Builder :=
   new
   |>.method .get
   |>.uri uri
 
 /--
 Creates a new HTTP POST Request builder with the specified URI.
 -/
-def post (uri : String) : Builder :=
+def post (uri : RequestTarget) : Builder :=
   new
   |>.method .post
   |>.uri uri
 
 /--
 Creates a new HTTP PUT Request builder with the specified URI.
 -/
-def put (uri : String) : Builder :=
+def put (uri : RequestTarget) : Builder :=
   new
   |>.method .put
   |>.uri uri
 
 /--
 Creates a new HTTP DELETE Request builder with the specified URI
 -/
-def delete (uri : String) : Builder :=
+def delete (uri : RequestTarget) : Builder :=
   new
   |>.method .delete
   |>.uri uri
 
 /--
 Creates a new HTTP PATCH Request builder with the specified URI
 -/
-def patch (uri : String) : Builder :=
+def patch (uri : RequestTarget) : Builder :=
   new
   |>.method .patch
   |>.uri uri
@@ -207,33 +215,33 @@ def patch (uri : String) : Builder :=
 Creates a new HTTP HEAD Request builder with the specified URI.
 Named `head'` to avoid conflict with the `head` field accessor.
 -/
-def head' (uri : String) : Builder :=
+def head' (uri : RequestTarget) : Builder :=
   new
   |>.method .head
   |>.uri uri
 
 /--
 Creates a new HTTP OPTIONS Request builder with the specified URI.
-Use `Request.options (String.asteriskForm)` for server-wide OPTIONS.
+Use `Request.options (RequestTarget.asteriskForm)` for server-wide OPTIONS.
 -/
-def options (uri : String) : Builder :=
+def options (uri : RequestTarget) : Builder :=
   new
   |>.method .options
   |>.uri uri
 
 /--
 Creates a new HTTP CONNECT Request builder with the specified URI.
-Typically used with `String.authorityForm` for tunneling.
+Typically used with `RequestTarget.authorityForm` for tunneling.
 -/
-def connect (uri : String) : Builder :=
+def connect (uri : RequestTarget) : Builder :=
   new
   |>.method .connect
   |>.uri uri
 
 /--
 Creates a new HTTP TRACE Request builder with the specified URI
 -/
-def trace (uri : String) : Builder :=
+def trace (uri : RequestTarget) : Builder :=
   new
   |>.method .trace
   |>.uri uri

src/Std/Internal/Http/Data/URI/Basic.lean

@@ -726,4 +726,7 @@ instance : ToString RequestTarget where
     | .authorityForm auth => toString auth
     | .asteriskForm => "*"
 
+instance : Encode .v11 RequestTarget where
+  encode buffer target := buffer.writeString (toString target)
+
 end Std.Http.RequestTarget

tests/lean/run/async_http_encode.lean

@@ -132,13 +132,13 @@ info: "X-Custom-Header: value\x0d\n"
 info: "GET /path HTTP/1.1\x0d\n\x0d\n"
 -/
 #guard_msgs in
-#eval encodeStr ({ method := .get, version := .v11, uri := "/path" } : Request.Head)
+#eval encodeStr ({ method := .get, version := .v11, uri := .parse! "/path" } : Request.Head)
 
 /--
 info: "POST /submit HTTP/1.1\x0d\n\x0d\n"
 -/
 #guard_msgs in
-#eval encodeStr ({ method := .post, version := .v11, uri := "/submit" } : Request.Head)
+#eval encodeStr ({ method := .post, version := .v11, uri := .parse! "/submit" } : Request.Head)
 
 /--
 info: "PUT /resource HTTP/2.0\x0d\nContent-Type: application/json\x0d\n\x0d\n"
@@ -147,7 +147,7 @@ info: "PUT /resource HTTP/2.0\x0d\nContent-Type: application/json\x0d\n\x0d\n"
 #eval encodeStr ({
     method := .put
     version := .v20
-    uri := "/resource"
+    uri := .parse! "/resource"
     headers := Headers.empty.insert! "content-type" "application/json"
   } : Request.Head)