fix: client uri

src/Std/Internal/Http/Client.lean

@@ -187,7 +187,7 @@ def queryParam (rb : Client.RequestBuilder) (key : String) (value : String) : Cl
     | .originForm o =>
         .originForm { o with query := some ((o.query.getD URI.Query.empty).insert key value) }
     | .absoluteForm af =>
-        .absoluteForm { af with uri := { af.uri with query := af.uri.query.insert key value } }
+        .absoluteForm { af with query := af.query.insert key value }
     | other => other
   { rb with builder := { rb.builder with line := { rb.builder.line with uri := newTarget } } }
 
@@ -241,7 +241,7 @@ private def mkRequest
     (method : Request.Builder → Request.Builder)
     (client : Client) (url : URI.AuthorityForm) : Client.RequestBuilder :=
   let target : RequestTarget :=
-    .originForm (RequestTarget.OriginForm.mk url.path (if url.query.isEmpty then none else some url.query))
+    .originForm (RequestTarget.PathAndQuery.mk url.path (if url.query.isEmpty then none else some url.query))
   { client, host := url.host, port := url.port,
     builder := method (Request.new |>.uri target) }
 

src/Std/Internal/Http/Client/Agent.lean

@@ -136,7 +136,7 @@ def injectCookies (cookieJar : Cookie.Jar) (host : URI.Host)
     (request : Request Body.AnyBody) : Async (Request Body.AnyBody) := do
   let path := match request.line.uri with
     | .originForm o   => toString o.path
-    | .absoluteForm af => toString af.uri.path
+    | .absoluteForm af => toString af.path
     | _ => "/"
   let cookies ← cookieJar.cookiesFor host path
   match Cookie.Jar.toCookieHeader cookies with
@@ -376,7 +376,7 @@ private def withCookies [Transport α] (rb : Agent.RequestBuilder α) : Async (A
     return rb
   let path := match rb.builder.line.uri with
     | .originForm o   => toString o.path
-    | .absoluteForm af => toString af.uri.path
+    | .absoluteForm af => toString af.path
     | _ => "/"
   let cookies ← rb.agent.cookieJar.cookiesFor rb.agent.host path
   match Cookie.Jar.toCookieHeader cookies with
@@ -428,7 +428,7 @@ def queryParam [Transport α] (rb : Agent.RequestBuilder α) (key : String) (val
     | .originForm o =>
         .originForm { o with query := some ((o.query.getD URI.Query.empty).insert key value) }
     | .absoluteForm af =>
-        .absoluteForm { af with uri := { af.uri with query := af.uri.query.insert key value } }
+        .absoluteForm { af with query := af.query.insert key value }
     | other => other
   { rb with builder := { rb.builder with line := { rb.builder.line with uri := newTarget } } }
 

src/Std/Internal/Http/Data/Headers/Name.lean

@@ -177,4 +177,19 @@ Standard Expect header name
 -/
 def expect : Header.Name := .mk "expect"
 
+/--
+Standard Cookie header name (client → server)
+-/
+def cookie : Header.Name := .mk "cookie"
+
+/--
+Standard Set-Cookie header name (server → client)
+-/
+def setCookie : Header.Name := .mk "set-cookie"
+
+/--
+Standard Location header name
+-/
+def location : Header.Name := .mk "location"
+
 end Std.Http.Header.Name