Merge branch 'sofia/async-http-h1' into sofia/async-http-server

2026-03-17 18:34:06 +00:00 · 2026-03-13 23:51:15 -03:00
parent 9c87a9f044 1a270555ae
commit ae5a3d2c8b
5 changed files with 251 additions and 57 deletions
--- a/src/Std/Internal/Http/Data/URI.lean
+++ b/src/Std/Internal/Http/Data/URI.lean
@@ -52,9 +52,57 @@ Panics if the string is not a valid origin-form request target.
@[inline]
 def originForm! (path : String) : RequestTarget :=
  match parse? path with
-  | some (.originForm p q) => .originForm p q
+  | some (.originForm o) => .originForm o
  | _ => panic! s!"invalid origin-form request target: {path}"

+namespace PathAndQuery
+
+/--
+Attempts to parse an origin-form request target from a string such as `"/path?key=value"`.
+Returns `none` if the string is not a valid origin-form target.
+-/
+@[inline]
+def parse? (s : String) : Option RequestTarget.PathAndQuery := do
+  match ← RequestTarget.parse? s with
+  | .originForm o => some o
+  | _ => none
+
+/--
+Parses an origin-form request target from a string. Panics if parsing fails.
+Use `parse?` if you need a safe option-returning version.
+-/
+@[inline]
+def parse! (s : String) : RequestTarget.PathAndQuery :=
+  match parse? s with
+  | some o => o
+  | none   => panic! s!"invalid origin-form request target: {s.quote}"
+
+end PathAndQuery
+
+namespace Absolute
+
+/--
+Attempts to parse an absolute-form request target from a string such as `"http://host/path"`.
+Returns `none` if the string is not a valid absolute-form target.
+-/
+@[inline]
+def parse? (s : String) : Option RequestTarget.Absolute := do
+  match ← RequestTarget.parse? s with
+  | .absoluteForm af => some af
+  | _ => none
+
+/--
+Parses an absolute-form request target from a string. Panics if parsing fails.
+Use `parse?` if you need a safe option-returning version.
+-/
+@[inline]
+def parse! (s : String) : RequestTarget.Absolute :=
+  match parse? s with
+  | some af => af
+  | none    => panic! s!"invalid absolute-form request target: {s.quote}"
+
+end Absolute
+
 end RequestTarget

 namespace URI
@@ -76,4 +124,50 @@ def parse! (string : String) : URI :=
  | some res => res
  | none => panic! "invalid URI"

-end URI
+namespace Path
+
+/--
+Attempts to parse a URI path from the given string.
+Returns `none` if the string is not a valid path.
+-/
+@[inline]
+def parse? (s : String) : Option Std.Http.URI.Path :=
+  (Std.Http.URI.Parser.parsePath {} true true <* Std.Internal.Parsec.eof).run s.toUTF8 |>.toOption
+
+/--
+Parses a URI path from the given string. Returns the root path `"/"` if parsing fails.
+-/
+@[inline]
+def parseOrRoot (s : String) : Std.Http.URI.Path :=
+  parse? s |>.getD { segments := #[], absolute := true }
+
+end Std.Http.URI.Path
+
+namespace Std.Http.URI.AuthorityForm
+
+/--
+Attempts to parse a URL with a required authority component.
+Accepts absolute URLs such as `"http://host:8080/path?k=v"`.
+The port defaults to 80 for `http` and 443 for `https` if omitted.
+Returns `none` if the URL is invalid or has no authority.
+-/
+@[inline]
+def parse? (s : String) : Option Std.Http.URI.AuthorityForm := do
+  let uri ← Std.Http.URI.parse? s
+  let auth ← uri.authority
+  let port : UInt16 := match auth.port with
+    | .value p => p
+    | _ => URI.Scheme.defaultPort uri.scheme
+  some { scheme := uri.scheme, host := auth.host, port, path := uri.path, query := uri.query }
+
+/--
+Parses a URL with a required authority component. Panics if parsing fails.
+Use `parse?` if you need a safe option-returning version.
+-/
+@[inline]
+def parse! (s : String) : Std.Http.URI.AuthorityForm :=
+  match parse? s with
+  | some af => af
+  | none    => panic! s!"invalid URL (expected scheme://host/path): {s.quote}"
+
+end Std.Http.URI.AuthorityForm
--- a/src/Std/Internal/Http/Data/URI/Basic.lean
+++ b/src/Std/Internal/Http/Data/URI/Basic.lean
@@ -81,6 +81,18 @@ def ofString! (s : String) : Scheme :=
  | some scheme => scheme
  | none => panic! s!"invalid URI scheme: {s.quote}"

+/--
+Returns the default port number for this URI scheme: 443 for `https`, 80 for everything else.
+-/
+def defaultPort (scheme : URI.Scheme) : UInt16 :=
+  if scheme.val == "https" then 443 else 80
+
+/--
+Returns the URI scheme for a given port: `"https"` for 443, `"http"` otherwise.
+-/
+def ofPort (port : UInt16) : URI.Scheme :=
+  if port == 443 then ⟨"https", by decide⟩ else ⟨"http", by decide⟩
+
 end Scheme

 /--
@@ -104,7 +116,7 @@ structure UserInfo where
  The optional encoded password.
  -/
  password : Option EncodedUserInfo
-deriving Inhabited, Repr
+deriving Inhabited, Repr, BEq

 namespace UserInfo

@@ -268,7 +280,7 @@ structure Authority where
  explicitly empty (`example.com:`), or numeric (`example.com:443`).
  -/
  port : Port := .omitted
-deriving Inhabited, Repr
+deriving Inhabited, Repr, BEq

 instance : ToString Authority where
  toString auth :=
@@ -299,7 +311,7 @@ structure Path where
  Whether the path is absolute (begins with '/') or relative.
  -/
  absolute : Bool
-deriving Inhabited, Repr
+deriving Inhabited, Repr, BEq

 instance : ToString Path where
  toString path :=
@@ -380,7 +392,7 @@ Reference: https://www.rfc-editor.org/rfc/rfc3986.html#section-3.4
 -/
@[expose]
 def Query := Array (EncodedQueryParam × Option EncodedQueryParam)
-deriving Repr, Inhabited
+deriving Repr, Inhabited, BEq

 namespace Query

@@ -584,7 +596,7 @@ structure URI where
  Optional fragment identifier (the part after '#'), percent-encoded.
  -/
  fragment : Option String
-deriving Repr, Inhabited
+deriving Repr, Inhabited, BEq

 instance : ToString URI where
  toString uri :=
@@ -833,6 +845,104 @@ def normalize (uri : URI) : URI :=

 end URI

+namespace URI
+
+/--
+A parsed URL with a required authority component (scheme + host + port + path + query).
+Port defaults are resolved: omitted port uses 80 for `http` and 443 for `https`.
+Suitable for use with `Http.Client`.
+-/
+structure AuthorityForm where
+  /--
+  The URI scheme (e.g., `"http"` or `"https"`).
+  -/
+  scheme : URI.Scheme
+
+  /--
+  The host component (domain name or IP address).
+  -/
+  host   : URI.Host
+
+  /--
+  The port, with the default for the scheme already applied if the URL omitted it.
+  -/
+  port   : UInt16
+
+  /--
+  The path component.
+  -/
+  path   : URI.Path
+
+  /--
+  The query string.
+  -/
+  query  : URI.Query
+deriving Inhabited, Repr, BEq
+
+instance : ToString URI.AuthorityForm where
+  toString af :=
+    let portPart := if af.port == af.scheme.defaultPort then "" else s!":{af.port}"
+    s!"{af.scheme}://{af.host}{portPart}{af.path}{af.query}"
+
+end URI
+
+namespace RequestTarget
+
+/--
+Data for an origin-form request target: an absolute path and optional query string.
+Example: `"/path/to/resource?key=value"` parsed into `path` and `query`.
+-/
+structure PathAndQuery where
+  /--
+  The absolute path.
+  -/
+  path  : URI.Path
+
+  /--
+  The optional query string. `none` means no `?` separator was present.
+  -/
+  query : Option URI.Query
+deriving Inhabited, Repr, BEq
+
+/--
+Data for an absolute-form request target: a complete URI.
+Used when making requests through a proxy.
+Example: `"http://example.com:8080/path?key=value"`.
+-/
+structure Absolute where
+  /--
+  The URI scheme (e.g., "http", "https", "ftp").
+  -/
+  scheme : URI.Scheme
+
+  /--
+  Optional authority component (user info, host, and port).
+  -/
+  authority : Option URI.Authority
+
+  /--
+  The hierarchical path component.
+  -/
+  path : URI.Path
+
+  /--
+  Optional query string as key-value pairs.
+  -/
+  query : URI.Query
+deriving Repr, Inhabited, BEq
+
+instance : ToString Absolute where
+  toString uri :=
+    let schemePart := uri.scheme
+    let authorityPart := match uri.authority with
+      | none => ""
+      | some auth => s!"//{toString auth}"
+    let pathPart := toString uri.path
+    let queryPart := toString uri.query
+    s!"{schemePart}:{authorityPart}{pathPart}{queryPart}"
+
+end RequestTarget
+
 /--
 HTTP request target forms as defined in RFC 9112 Section 3.3.

@@ -843,13 +953,13 @@ inductive RequestTarget where
  Origin-form request target (most common for HTTP requests). Consists of a path and an optional query string.
  Example: `/path/to/resource?key=value`
  -/
-  | originForm (path : URI.Path) (query : Option URI.Query)
+  | originForm (t : RequestTarget.PathAndQuery)

  /--
  Absolute-form request target containing a complete URI. Used when making requests through a proxy.
  Example: `http://example.com:8080/path?key=value`
  -/
-  | absoluteForm (uri : URI) (noFrag : uri.fragment.isNone)
+  | absoluteForm (t : RequestTarget.Absolute)

  /--
  Authority-form request target (used for CONNECT requests).
@@ -871,8 +981,8 @@ Extracts the path component from a request target, if available.
 Returns an empty relative path for targets without a path.
 -/
 def path : RequestTarget → URI.Path
-  | .originForm p _ => p
-  | .absoluteForm u _ => u.path
+  | .originForm o => o.path
+  | .absoluteForm af => af.path
  | _ => { segments := #[], absolute := false }

 /--
@@ -880,8 +990,8 @@ Extracts the query component from a request target, if available.
 Returns an empty array for targets without a query.
 -/
 def query : RequestTarget → URI.Query
-  | .originForm _ q => q.getD URI.Query.empty
-  | .absoluteForm u _ => u.query
+  | .originForm o => o.query.getD URI.Query.empty
+  | .absoluteForm af => af.query
  | _ => URI.Query.empty

 /--
@@ -889,23 +999,16 @@ Extracts the authority component from a request target, if available.
 -/
 def authority? : RequestTarget → Option URI.Authority
  | .authorityForm a => some a
-  | .absoluteForm u _ => u.authority
-  | _ => none
-
-/--
-Extracts the full URI if the request target is in absolute form.
-/
-def uri? : RequestTarget → Option URI
-  | .absoluteForm u _ => some u
+  | .absoluteForm af => af.authority
  | _ => none

 instance : ToString RequestTarget where
  toString
-    | .originForm path query =>
-        let pathStr := toString path
-        let queryStr := query.map toString |>.getD ""
+    | .originForm o =>
+        let pathStr := toString o.path
+        let queryStr := o.query.map toString |>.getD ""
        s!"{pathStr}{queryStr}"
-    | .absoluteForm uri _ => toString uri
+    | .absoluteForm af => toString af
    | .authorityForm auth => toString auth
    | .asteriskForm => "*"

--- a/src/Std/Internal/Http/Data/URI/Parser.lean
+++ b/src/Std/Internal/Http/Data/URI/Parser.lean
@@ -361,7 +361,7 @@ where
      let path ← parsePath config true true
      let query ← optional (skipByte '?'.toUInt8 *> parseQuery config)

-      return .originForm path query
+      return .originForm { path, query }
    else
      fail "not origin"

@@ -371,20 +371,24 @@ where
    let query ← optional (skipByteChar '?' *> parseQuery config)
    let query := query.getD URI.Query.empty

-    return .absoluteForm { path, scheme, authority := auth, query, fragment := none } (by simp)
+    return .absoluteForm { path, scheme, authority := auth, query }

  -- Prefer absolute-form for explicit HTTP(S) scheme targets.
  -- This avoids misclassifying full URIs like `http://host/path` as authority-form.
  absoluteHttp : Parser RequestTarget := attempt do
+    let scheme ← parseScheme config
+    skipByte ':'.toUInt8
+
+    let (authority, path) ← parseHierPart config
+
+    let query ← optional (skipByteChar '?' *> parseQuery config)
+    let query := query.getD .empty
+
    let uri ← parseURI config
    let schemeStr : String := uri.scheme
-    if h : (schemeStr = "http" || schemeStr = "https") && uri.fragment.isNone then
-      have hEqNone : uri.fragment = none := by
-        simp at h
-        exact h.right
-      have hNoFrag : uri.fragment.isNone = true := by
-        simp [hEqNone]
-      return .absoluteForm uri hNoFrag
+    if schemeStr = "http" || schemeStr = "https" then
+      -- Strip any fragment: HTTP request targets do not carry fragments.
+      return .absoluteForm { scheme, path, authority, query }
    else
      fail "not http absolute uri"

--- a/src/Std/Internal/Http/Protocol/H1.lean
+++ b/src/Std/Internal/Http/Protocol/H1.lean
@@ -323,7 +323,7 @@ private def hasSingleAcceptedHostHeader (message : Message.Head .receiving) : Bo
      match message.uri with
      | .asteriskForm =>
        hostValue.value.isEmpty ∨ parsed.isSome
-      | .absoluteForm { scheme, authority := some authority, .. } _ =>
+      | .absoluteForm { scheme, authority := some authority, .. } =>
        match parsed with
        | some hostHeader => hostAuthorityMatches (some scheme) authority hostHeader
        | none => false
--- a/tests/elab/async_http_uri.lean
+++ b/tests/elab/async_http_uri.lean
@@ -251,7 +251,7 @@ info: some " "

 #guard
  match (parseRequestTarget <* Std.Internal.Parsec.eof).run "http:80".toUTF8 with
-  | .ok (.absoluteForm _ _) => true
+  | .ok (.authorityForm _) => true
  | _ => false

 -- Parse failure tests
@@ -282,7 +282,8 @@ info: some " "
 -- ============================================================================

 /--
-info: Std.Http.RequestTarget.originForm { segments := #["path", "with", "encoded%20space"], absolute := true } none
+info: Std.Http.RequestTarget.originForm
+  { path := { segments := #["path", "with", "encoded%20space"], absolute := true }, query := none }
 -/
 #guard_msgs in
 #eval show IO _ from do
@@ -290,7 +291,8 @@ info: Std.Http.RequestTarget.originForm { segments := #["path", "with", "encoded
  IO.println (repr result)

 /--
-info: Std.Http.RequestTarget.originForm { segments := #["", "", "path", "with", "encoded%20space"], absolute := true } none
+info: Std.Http.RequestTarget.originForm
+  { path := { segments := #["", "", "path", "with", "encoded%20space"], absolute := true }, query := none }
 -/
 #guard_msgs in
 #eval show IO _ from do
@@ -314,7 +316,7 @@ info: #[("q", some "hello%20world"), ("category", some "tech%2Bgames")]
  IO.println (repr result.query)

 /--
-info: Std.Http.RequestTarget.originForm { segments := #[], absolute := true } none
+info: Std.Http.RequestTarget.originForm { path := { segments := #[], absolute := true }, query := none }
 -/
 #guard_msgs in
 #eval show IO _ from do
@@ -355,9 +357,7 @@ info: Std.Http.RequestTarget.absoluteForm
                   host := Std.Http.URI.Host.name "example.com",
                   port := Std.Http.URI.Port.value 8080 },
    path := { segments := #["ata"], absolute := true },
-    query := #[],
-    fragment := none }
-  _
+    query := #[] }
 -/
 #guard_msgs in
 #eval show IO _ from do
@@ -371,9 +371,7 @@ info: Std.Http.RequestTarget.absoluteForm
                   host := Std.Http.URI.Host.ipv6 2001:db8::1,
                   port := Std.Http.URI.Port.value 8080 },
    path := { segments := #["path"], absolute := true },
-    query := #[],
-    fragment := none }
-  _
+    query := #[] }
 -/
 #guard_msgs in
 #eval show IO _ from do
@@ -387,9 +385,7 @@ info: Std.Http.RequestTarget.absoluteForm
                   host := Std.Http.URI.Host.name "secure.example.com",
                   port := Std.Http.URI.Port.omitted },
    path := { segments := #["private"], absolute := true },
-    query := #[],
-    fragment := none }
-  _
+    query := #[] }
 -/
 #guard_msgs in
 #eval show IO _ from do
@@ -848,7 +844,8 @@ info: https://user:pass@secure.example.com/private
 -- ============================================================================

 /--
-info: Std.Http.RequestTarget.originForm { segments := #["path%2Fwith%2Fslashes"], absolute := true } none
+info: Std.Http.RequestTarget.originForm
+  { path := { segments := #["path%2Fwith%2Fslashes"], absolute := true }, query := none }
 -/
 #guard_msgs in
 #eval show IO _ from do
@@ -856,7 +853,7 @@ info: Std.Http.RequestTarget.originForm { segments := #["path%2Fwith%2Fslashes"]
  IO.println (repr result)

 /--
-info: Std.Http.RequestTarget.originForm { segments := #["file%20name.txt"], absolute := true } none
+info: Std.Http.RequestTarget.originForm { path := { segments := #["file%20name.txt"], absolute := true }, query := none }
 -/
 #guard_msgs in
 #eval show IO _ from do
@@ -864,7 +861,7 @@ info: Std.Http.RequestTarget.originForm { segments := #["file%20name.txt"], abso
  IO.println (repr result)

 /--
-info: Std.Http.RequestTarget.originForm { segments := #["caf%C3%A9"], absolute := true } none
+info: Std.Http.RequestTarget.originForm { path := { segments := #["caf%C3%A9"], absolute := true }, query := none }
 -/
 #guard_msgs in
 #eval show IO _ from do
@@ -909,9 +906,7 @@ info: Std.Http.RequestTarget.absoluteForm
                   host := Std.Http.URI.Host.name "1example.com",
                   port := Std.Http.URI.Port.omitted },
    path := { segments := #["path"], absolute := true },
-    query := #[],
-    fragment := none }
-  _
+    query := #[] }
 -/
 #guard_msgs in
 #eval show IO _ from do
@@ -925,9 +920,7 @@ info: Std.Http.RequestTarget.absoluteForm
                   host := Std.Http.URI.Host.name "123abc.example.com",
                   port := Std.Http.URI.Port.omitted },
    path := { segments := #["page"], absolute := true },
-    query := #[],
-    fragment := none }
-  _
+    query := #[] }
 -/
 #guard_msgs in
 #eval show IO _ from do