URI Structure

This module defines an HTTP-oriented URI structure aligned with RFC 3986 and RFC 9110, including schemes, authorities, paths, queries, fragments, and request targets.

Host handling is intentionally strict: this module accepts IPv4, bracketed IPv6, and DNS-style domain names (LDH labels). RFC 3986 reg-name forms that are not DNS-compatible are rejected.

All text components use the encoding types from Std.Http.URI.Encoding to ensure proper percent-encoding is maintained throughout.

References:

• https://www.rfc-editor.org/rfc/rfc3986.html
• https://www.rfc-editor.org/rfc/rfc9110.html#name-uri-references

@[reducible, inline]

abbrev Std.Http.URI.IsValidScheme (s : String) : Prop

Proposition that s is a valid URI scheme per RFC 3986: scheme = ALPHA *( ALPHA / DIGIT / "+" / "-" / "." ).

The scheme value stored in this module is normalized to lowercase.

Reference: https://www.rfc-editor.org/rfc/rfc3986.html#section-3.1

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Std.Http.URI.Scheme : Type

URI scheme identifier (e.g., "http", "https", "ftp").

Equations

• Std.Http.URI.Scheme = { s : String // Std.Http.URI.IsValidScheme s }

@[implicit_reducible]

instance Std.Http.URI.instInhabitedScheme : Inhabited Scheme

Equations

• Std.Http.URI.instInhabitedScheme = { default := ⟨"http", Std.Http.URI.instInhabitedScheme._proof_4⟩ }

def Std.Http.URI.Scheme.ofString? (s : String) : Option Scheme

Attempts to create a Scheme from a string, normalizing to lowercase. Returns none if the scheme is invalid per RFC 3986 Section 3.1.

Equations

• Std.Http.URI.Scheme.ofString? s = if h : Std.Http.URI.IsValidScheme s.toLower then some ⟨s.toLower, h⟩ else none

def Std.Http.URI.Scheme.ofString! (s : String) : Scheme

Creates a Scheme from a string, normalizing to lowercase. Panics if invalid.

Equations

• One or more equations did not get rendered due to their size.

def Std.Http.URI.Scheme.defaultPort (scheme : Scheme) : UInt16

Returns the default port number for this URI scheme: 443 for https, 80 for everything else.

Equations

• scheme.defaultPort = if (scheme.val == "https") = true then 443 else 80

def Std.Http.URI.Scheme.ofPort (port : UInt16) : Scheme

Returns the URI scheme for a given port: "https" for 443, "http" otherwise.

Equations

• Std.Http.URI.Scheme.ofPort port = if (port == 443) = true then ⟨"https", Std.Http.URI.Scheme.ofPort._proof_1✝⟩ else ⟨"http", Std.Http.URI.Scheme.ofPort._proof_2✝⟩

structure Std.Http.URI.UserInfo : Type

User information component containing an encoded username and optional encoded password.

The stored strings use URI userinfo percent-encoding so parsed URIs can be rendered without losing percent-encoding choices (for example, %3A versus :).

Note: embedding passwords in URIs is deprecated per RFC 9110 Section 4.2.4. Avoid using the password field in new code, and never include it in logs or error messages.

Reference: https://www.rfc-editor.org/rfc/rfc3986.html#section-3.2.1

• username : EncodedUserInfo

  The encoded username.

• password : Option EncodedUserInfo

  The optional encoded password.

def Std.Http.URI.instInhabitedUserInfo.default : UserInfo

Equations

• Std.Http.URI.instInhabitedUserInfo.default = { username := default, password := default }

@[implicit_reducible]

instance Std.Http.URI.instInhabitedUserInfo : Inhabited UserInfo

Equations

• Std.Http.URI.instInhabitedUserInfo = { default := Std.Http.URI.instInhabitedUserInfo.default }

def Std.Http.URI.instReprUserInfo.repr : UserInfo → Nat → Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Std.Http.URI.instReprUserInfo : Repr UserInfo

Equations

• Std.Http.URI.instReprUserInfo = { reprPrec := Std.Http.URI.instReprUserInfo.repr }

def Std.Http.URI.instBEqUserInfo.beq : UserInfo → UserInfo → Bool

Equations

• Std.Http.URI.instBEqUserInfo.beq { username := a, password := a_1 } { username := b, password := b_1 } = (a == b && a_1 == b_1)
• Std.Http.URI.instBEqUserInfo.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Std.Http.URI.instBEqUserInfo : BEq UserInfo

Equations

• Std.Http.URI.instBEqUserInfo = { beq := Std.Http.URI.instBEqUserInfo.beq }

@[inline]

def Std.Http.URI.UserInfo.ofStrings (username : String) (password : Option String := none) : UserInfo

Builds a UserInfo value from raw strings by applying userinfo percent-encoding.

Equations

• Std.Http.URI.UserInfo.ofStrings username password = { username := Std.Http.URI.EncodedUserInfo.encode username, password := Std.Http.URI.EncodedUserInfo.encode <$> password }

@[inline]

def Std.Http.URI.UserInfo.username? (ui : UserInfo) : Option String

Returns the decoded username, or none if decoding fails UTF-8 validation.

Equations

• ui.username? = ui.username.decode

@[inline]

def Std.Http.URI.UserInfo.password? (ui : UserInfo) : Option String

Returns the decoded password when present, or none if absent or decoding fails UTF-8 validation.

Equations

• ui.password? = ui.password.bind Std.Http.URI.EncodedUserInfo.decode

def Std.Http.URI.isValidDomainLabel (s : String) : Bool

Checks whether a single domain label is valid. A label must be non-empty, contain only ASCII alphanumeric characters and -, cannot start or end with -, and must be at most 63 characters.

References:

• https://www.rfc-editor.org/rfc/rfc1034.html#section-3.5
• https://www.rfc-editor.org/rfc/rfc1123.html#section-2.1

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Std.Http.URI.IsValidDomainName (s : String) : Prop

Proposition that asserts s is a valid dot-separated domain name. Each label must satisfy IsValidDomainLabel, and the full name must be at most 255 characters.

Equations

• Std.Http.URI.IsValidDomainName s = (¬(s.splitOn ".").isEmpty = true ∧ (s.splitOn ".").all Std.Http.URI.isValidDomainLabel = true ∧ s.length ≤ 255)

@[reducible, inline]

abbrev Std.Http.URI.DomainName : Type

A domain name represented as a validated, lowercase-normalized string. Only ASCII alphanumeric characters, hyphens, and dots are allowed. Each label cannot start or end with - and is limited to 63 characters. Internationalized domain names must be converted to punycode before use.

Reference: https://www.rfc-editor.org/rfc/rfc3986.html#section-3.2.2

Equations

• Std.Http.URI.DomainName = { s : String // Std.Http.Internal.IsLowerCase s ∧ Std.Http.URI.IsValidDomainName s ∧ ¬s.isEmpty = true }

def Std.Http.URI.DomainName.ofString? (s : String) : Option DomainName

Attempts to create a normalized domain name from a string. Returns none if the name is empty, longer than 255 characters, or any label violates DNS label constraints.

Equations

• Std.Http.URI.DomainName.ofString? s = if h₁ : s.toLower.isEmpty = true then none else if h₃ : Std.Http.URI.IsValidDomainName s.toLower then some ⟨s.toLower, ⋯⟩ else none

inductive Std.Http.URI.Host : Type

Host component of a URI, supporting domain names and IP addresses.

Reference: https://www.rfc-editor.org/rfc/rfc3986.html#section-3.2.2

• name (name : DomainName) : Host

  A domain name (lowercase-normalized).

• ipv4 (ipv4 : Net.IPv4Addr) : Host

  An IPv4 address.

• ipv6 (ipv6 : Net.IPv6Addr) : Host

  An IPv6 address.

@[implicit_reducible]

instance Std.Http.URI.instInhabitedHost : Inhabited Host

Equations

• Std.Http.URI.instInhabitedHost = { default := Std.Http.URI.instInhabitedHost.default }

def Std.Http.URI.instInhabitedHost.default : Host

Equations

• Std.Http.URI.instInhabitedHost.default = Std.Http.URI.Host.ipv4 default

@[implicit_reducible]

instance Std.Http.URI.instBEqHost : BEq Host

Equations

• Std.Http.URI.instBEqHost = { beq := Std.Http.URI.instBEqHost.beq }

def Std.Http.URI.instBEqHost.beq : Host → Host → Bool

Equations

• Std.Http.URI.instBEqHost.beq (Std.Http.URI.Host.name a) (Std.Http.URI.Host.name b) = (a == b)
• Std.Http.URI.instBEqHost.beq (Std.Http.URI.Host.ipv4 a) (Std.Http.URI.Host.ipv4 b) = (a == b)
• Std.Http.URI.instBEqHost.beq (Std.Http.URI.Host.ipv6 a) (Std.Http.URI.Host.ipv6 b) = (a == b)
• Std.Http.URI.instBEqHost.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Std.Http.URI.instReprHost : Repr Host

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Std.Http.URI.instToStringHost : ToString Host

Equations

• One or more equations did not get rendered due to their size.

inductive Std.Http.URI.Port : Type

Authority port representation, preserving the distinction between:

• no port separator (example.com)
• empty port (example.com:)
• numeric port (example.com:443)

• omitted : Port

  No : port separator is present (for example, example.com).

• empty : Port

  A : port separator is present with no digits after it (for example, example.com:).

• value (port : UInt16) : Port

  A numeric port value is present (for example, example.com:443).

@[implicit_reducible]

instance Std.Http.URI.instInhabitedPort : Inhabited Port

Equations

• Std.Http.URI.instInhabitedPort = { default := Std.Http.URI.instInhabitedPort.default }

def Std.Http.URI.instInhabitedPort.default : Port

Equations

• Std.Http.URI.instInhabitedPort.default = Std.Http.URI.Port.omitted

@[implicit_reducible]

instance Std.Http.URI.instReprPort : Repr Port

Equations

• Std.Http.URI.instReprPort = { reprPrec := Std.Http.URI.instReprPort.repr }

def Std.Http.URI.instReprPort.repr : Port → Nat → Format

Equations

• One or more equations did not get rendered due to their size.
• Std.Http.URI.instReprPort.repr Std.Http.URI.Port.omitted prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.URI.Port.omitted")).group prec✝
• Std.Http.URI.instReprPort.repr Std.Http.URI.Port.empty prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.URI.Port.empty")).group prec✝

@[implicit_reducible]

instance Std.Http.URI.instDecidableEqPort : DecidableEq Port

Equations

• Std.Http.URI.instDecidableEqPort = Std.Http.URI.instDecidableEqPort.decEq

def Std.Http.URI.instDecidableEqPort.decEq (x✝ x✝¹ : Port) : Decidable (x✝ = x✝¹)

Equations

• Std.Http.URI.instDecidableEqPort.decEq Std.Http.URI.Port.omitted Std.Http.URI.Port.omitted = isTrue ⋯
• Std.Http.URI.instDecidableEqPort.decEq Std.Http.URI.Port.omitted Std.Http.URI.Port.empty = isFalse Std.Http.URI.instDecidableEqPort.decEq._proof_1✝
• Std.Http.URI.instDecidableEqPort.decEq Std.Http.URI.Port.omitted (Std.Http.URI.Port.value port) = isFalse ⋯
• Std.Http.URI.instDecidableEqPort.decEq Std.Http.URI.Port.empty Std.Http.URI.Port.omitted = isFalse Std.Http.URI.instDecidableEqPort.decEq._proof_3✝
• Std.Http.URI.instDecidableEqPort.decEq Std.Http.URI.Port.empty Std.Http.URI.Port.empty = isTrue ⋯
• Std.Http.URI.instDecidableEqPort.decEq Std.Http.URI.Port.empty (Std.Http.URI.Port.value port) = isFalse ⋯
• Std.Http.URI.instDecidableEqPort.decEq (Std.Http.URI.Port.value port) Std.Http.URI.Port.omitted = isFalse ⋯
• Std.Http.URI.instDecidableEqPort.decEq (Std.Http.URI.Port.value port) Std.Http.URI.Port.empty = isFalse ⋯
• Std.Http.URI.instDecidableEqPort.decEq (Std.Http.URI.Port.value a) (Std.Http.URI.Port.value b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

structure Std.Http.URI.Authority : Type

The authority component of a URI, identifying the network location of the resource.

Reference: https://www.rfc-editor.org/rfc/rfc3986.html#section-3.2

• userInfo : Option UserInfo

  Optional user information (username and password).

• host : Host

  The host identifying the network location.

• port : Port

  Port component, preserving whether it is omitted (example.com), explicitly empty (example.com:), or numeric (example.com:443).

def Std.Http.URI.instInhabitedAuthority.default : Authority

Equations

• Std.Http.URI.instInhabitedAuthority.default = { userInfo := default, host := default, port := default }

@[implicit_reducible]

instance Std.Http.URI.instInhabitedAuthority : Inhabited Authority

Equations

• Std.Http.URI.instInhabitedAuthority = { default := Std.Http.URI.instInhabitedAuthority.default }

@[implicit_reducible]

instance Std.Http.URI.instReprAuthority : Repr Authority

Equations

• Std.Http.URI.instReprAuthority = { reprPrec := Std.Http.URI.instReprAuthority.repr }

def Std.Http.URI.instReprAuthority.repr : Authority → Nat → Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Std.Http.URI.instBEqAuthority : BEq Authority

Equations

• Std.Http.URI.instBEqAuthority = { beq := Std.Http.URI.instBEqAuthority.beq }

def Std.Http.URI.instBEqAuthority.beq : Authority → Authority → Bool

Equations

• Std.Http.URI.instBEqAuthority.beq { userInfo := a, host := a_1, port := a_2 } { userInfo := b, host := b_1, port := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Std.Http.URI.instBEqAuthority.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Std.Http.URI.instToStringAuthority : ToString Authority

Equations

• One or more equations did not get rendered due to their size.

structure Std.Http.URI.Path : Type

Hierarchical path component of a URI. Each segment is stored as an EncodedSegment to maintain proper percent-encoding.

Reference: https://www.rfc-editor.org/rfc/rfc3986.html#section-3.3

• segments : Array EncodedSegment

  The path segments making up the hierarchical structure (each segment is percent-encoded).

• absolute : Bool

  Whether the path is absolute (begins with '/') or relative.

def Std.Http.URI.instInhabitedPath.default : Path

Equations

• Std.Http.URI.instInhabitedPath.default = { segments := default, absolute := default }

@[implicit_reducible]

instance Std.Http.URI.instInhabitedPath : Inhabited Path

Equations

• Std.Http.URI.instInhabitedPath = { default := Std.Http.URI.instInhabitedPath.default }

def Std.Http.URI.instReprPath.repr : Path → Nat → Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Std.Http.URI.instReprPath : Repr Path

Equations

• Std.Http.URI.instReprPath = { reprPrec := Std.Http.URI.instReprPath.repr }

@[implicit_reducible]

instance Std.Http.URI.instBEqPath : BEq Path

Equations

• Std.Http.URI.instBEqPath = { beq := Std.Http.URI.instBEqPath.beq }

def Std.Http.URI.instBEqPath.beq : Path → Path → Bool

Equations

• Std.Http.URI.instBEqPath.beq { segments := a, absolute := a_1 } { segments := b, absolute := b_1 } = (a == b && a_1 == b_1)
• Std.Http.URI.instBEqPath.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Std.Http.URI.instToStringPath : ToString Path

Equations

• One or more equations did not get rendered due to their size.

def Std.Http.URI.Path.isEmpty (p : Path) : Bool

Returns true if the path has no segments.

Equations

• p.isEmpty = p.segments.isEmpty

def Std.Http.URI.Path.parent (p : Path) : Path

Returns the parent path by removing the last segment. If the path is empty, returns the path unchanged.

Equations

• p.parent = if p.segments.isEmpty = true then p else { segments := p.segments.pop, absolute := p.absolute }

def Std.Http.URI.Path.join (p1 p2 : Path) : Path

Joins two paths. If the second path is absolute, it is returned as-is. Otherwise, the second path's segments are appended to the first path.

Equations

• p1.join p2 = if p2.absolute = true then p2 else { segments := p1.segments ++ p2.segments, absolute := p1.absolute }

def Std.Http.URI.Path.append (p : Path) (segment : String) : Path

Appends a single segment to the path. The segment will be percent-encoded.

Equations

• p.append segment = { segments := p.segments.push (Std.Http.URI.EncodedSegment.encode segment), absolute := p.absolute }

def Std.Http.URI.Path.appendEncoded (p : Path) (segment : EncodedSegment) : Path

Appends an already-encoded segment to the path.

Equations

• p.appendEncoded segment = { segments := p.segments.push segment, absolute := p.absolute }

def Std.Http.URI.Path.normalize (p : Path) : Path

Removes dot segments from the path according to RFC 3986 Section 5.2.4. This handles "." (current directory) and ".." (parent directory) segments.

Equations

• p.normalize = { segments := (Std.Http.URI.Path.normalize.loop✝ p.segments.toList []).toArray, absolute := p.absolute }

def Std.Http.URI.Path.toDecodedSegments (p : Path) : Array String

Returns the path segments as decoded strings. Segments that cannot be decoded as UTF-8 are returned as their raw encoded form.

Equations

• p.toDecodedSegments = Array.map (fun (seg : Std.Http.URI.EncodedSegment) => seg.decode.getD (toString seg)) p.segments

def Std.Http.URI.Query : Type

Query string represented as an array of key-value pairs. Both keys and values are stored as EncodedQueryParam for proper application/x-www-form-urlencoded encoding. Values are optional to support parameters without values (e.g., "?flag"). Order is preserved based on insertion order.

Reference: https://www.rfc-editor.org/rfc/rfc3986.html#section-3.4

Equations

• Std.Http.URI.Query = Array (Std.Http.URI.EncodedQueryParam × Option Std.Http.URI.EncodedQueryParam)

@[implicit_reducible]

instance Std.Http.URI.instReprQuery : Repr Query

Equations

• Std.Http.URI.instReprQuery = { reprPrec := Std.Http.URI.instReprQuery._aux_1 }

@[implicit_reducible]

instance Std.Http.URI.instInhabitedQuery : Inhabited Query

Equations

• Std.Http.URI.instInhabitedQuery = { default := Std.Http.URI.instInhabitedQuery._aux_1 }

@[implicit_reducible]

instance Std.Http.URI.instBEqQuery : BEq Query

Equations

• Std.Http.URI.instBEqQuery = { beq := Std.Http.URI.instBEqQuery._aux_1 }

def Std.Http.URI.Query.names (query : Query) : Array EncodedQueryParam

Extracts all unique query parameter names.

Equations

• query.names = (Array.map (fun (p : Std.Http.URI.EncodedQueryParam × Option Std.Http.URI.EncodedQueryParam) => p.fst) query).toList.eraseDups.toArray

def Std.Http.URI.Query.values (query : Query) : Array (Option EncodedQueryParam)

Extracts all query parameter values.

Equations

• query.values = Array.map (fun (p : Std.Http.URI.EncodedQueryParam × Option Std.Http.URI.EncodedQueryParam) => p.snd) query

def Std.Http.URI.Query.toArray (query : Query) : Array (EncodedQueryParam × Option EncodedQueryParam)

Returns the query as an array of (key, value) pairs. This is an identity function since Query is already an array of pairs.

Equations

• query.toArray = query

def Std.Http.URI.Query.formatQueryParam (key : EncodedQueryParam) (value : Option EncodedQueryParam) : String

Formats a query parameter as a string in the format "key" or "key=value". The key and value are already percent-encoded as EncodedQueryParam.

Equations

• Std.Http.URI.Query.formatQueryParam key none = toString key
• Std.Http.URI.Query.formatQueryParam key (some v) = toString (toString key) ++ toString "=" ++ toString (toString v)

def Std.Http.URI.Query.findEncoded? (query : Query) (key : EncodedQueryParam) : Option (Option EncodedQueryParam)

Finds the first value of a query parameter by key name. Returns none if the key is not found. The value remains encoded as EncodedQueryParam.

Equations

• One or more equations did not get rendered due to their size.

def Std.Http.URI.Query.find? (query : Query) (key : String) : Option (Option EncodedQueryParam)

Finds the first value of a query parameter by raw key string. The key is percent-encoded before matching. This avoids aliasing between raw and pre-encoded spellings.

Equations

• query.find? key = query.findEncoded? (Std.Http.URI.EncodedQueryParam.encode key)

def Std.Http.URI.Query.findAllEncoded (query : Query) (key : EncodedQueryParam) : Array (Option EncodedQueryParam)

Finds all values of a query parameter by key name. Returns an empty array if the key is not found. The values remain encoded as EncodedQueryParam.

Equations

• One or more equations did not get rendered due to their size.

def Std.Http.URI.Query.findAll (query : Query) (key : String) : Array (Option EncodedQueryParam)

Finds all values of a query parameter by raw key string. The key is percent-encoded before matching.

Equations

• query.findAll key = query.findAllEncoded (Std.Http.URI.EncodedQueryParam.encode key)

def Std.Http.URI.Query.insert (query : Query) (key value : String) : Query

Adds a query parameter to the query string.

Equations

• query.insert key value = Array.push query (Std.Http.URI.EncodedQueryParam.encode key, some (Std.Http.URI.EncodedQueryParam.encode value))

def Std.Http.URI.Query.insertEncoded (query : Query) (key : EncodedQueryParam) (value : Option EncodedQueryParam) : Query

Adds an already-encoded key-value pair to the query string.

Equations

• query.insertEncoded key value = Array.push query (key, value)

def Std.Http.URI.Query.empty : Query

Creates an empty query string.

Equations

• Std.Http.URI.Query.empty = #[]

def Std.Http.URI.Query.ofList (pairs : List (EncodedQueryParam × Option EncodedQueryParam)) : Query

Creates a query string from a list of key-value pairs.

Equations

• Std.Http.URI.Query.ofList pairs = pairs.toArray

def Std.Http.URI.Query.containsEncoded (query : Query) (key : EncodedQueryParam) : Bool

Checks if a query parameter exists.

Equations

• query.containsEncoded key = Array.any query fun (x : Std.Http.URI.EncodedQueryParam × Option Std.Http.URI.EncodedQueryParam) => decide (x.fst.toByteArray = key.toByteArray)

def Std.Http.URI.Query.contains (query : Query) (key : String) : Bool

Checks if a query parameter exists by raw key string. The key is percent-encoded before matching.

Equations

• query.contains key = query.containsEncoded (Std.Http.URI.EncodedQueryParam.encode key)

def Std.Http.URI.Query.eraseEncoded (query : Query) (key : EncodedQueryParam) : Query

Removes all occurrences of a query parameter by key name.

Equations

• query.eraseEncoded key = Array.filter (fun (x : Std.Http.URI.EncodedQueryParam × Option Std.Http.URI.EncodedQueryParam) => decide (x.fst.toByteArray ≠ key.toByteArray)) query

def Std.Http.URI.Query.erase (query : Query) (key : String) : Query

Removes all occurrences of a query parameter by raw key string. The key is percent-encoded before matching.

Equations

• query.erase key = query.eraseEncoded (Std.Http.URI.EncodedQueryParam.encode key)

def Std.Http.URI.Query.get (query : Query) (key : String) : Option String

Gets the first value of a query parameter by key name, decoded as a string. Returns none if the key is not found or if the value cannot be decoded as UTF-8.

Equations

• query.get key = match query.find? key with | none => none | some none => some "" | some (some encoded) => encoded.decode

def Std.Http.URI.Query.getD (query : Query) (key default : String) : String

Gets the first value of a query parameter by key name, decoded as a string. Returns the default value if the key is not found or if the value cannot be decoded.

Equations

• query.getD key default = (query.get key).getD default

def Std.Http.URI.Query.set (query : Query) (key value : String) : Query

Sets a query parameter, replacing all existing values for that key. Both key and value will be automatically percent-encoded.

Equations

• query.set key value = (query.erase key).insert key value

def Std.Http.URI.Query.toRawString (query : Query) : String

Converts the query to a properly encoded query string format. Example: "key1=value1&key2=value2&flag"

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Std.Http.URI.Query.instEmptyCollection : EmptyCollection Query

Equations

• Std.Http.URI.Query.instEmptyCollection = { emptyCollection := Std.Http.URI.Query.empty }

@[implicit_reducible]

instance Std.Http.URI.Query.instSingletonProdString : Singleton (String × String) Query

Equations

• Std.Http.URI.Query.instSingletonProdString = { singleton := fun (x : String × String) => match x with | (k, v) => Std.Http.URI.Query.empty.insert k v }

@[implicit_reducible]

instance Std.Http.URI.Query.instInsertProdString : Insert (String × String) Query

Equations

• Std.Http.URI.Query.instInsertProdString = { insert := fun (x : String × String) (q : Std.Http.URI.Query) => match x with | (k, v) => q.insert k v }

@[implicit_reducible]

instance Std.Http.URI.Query.instToString : ToString Query

Equations

• One or more equations did not get rendered due to their size.

structure Std.Http.URI : Type

Complete URI structure following RFC 3986. All text components use encoded string types to ensure proper percent-encoding.

Reference: https://www.rfc-editor.org/rfc/rfc3986.html

• scheme : Scheme

  The URI scheme (e.g., "http", "https", "ftp").

• authority : Option Authority

  Optional authority component (user info, host, and port).

• path : Path

  The hierarchical path component.

• query : Query

  Optional query string as key-value pairs.

• fragment : Option String

  Optional fragment identifier (the part after '#'), percent-encoded.

@[implicit_reducible]

instance Std.Http.instReprURI : Repr URI

Equations

• Std.Http.instReprURI = { reprPrec := Std.Http.instReprURI.repr }

def Std.Http.instReprURI.repr : URI → Nat → Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Std.Http.instInhabitedURI : Inhabited URI

Equations

• Std.Http.instInhabitedURI = { default := Std.Http.instInhabitedURI.default }

def Std.Http.instInhabitedURI.default : URI

Equations

• Std.Http.instInhabitedURI.default = { scheme := default, authority := default, path := default, query := default, fragment := default }

@[implicit_reducible]

instance Std.Http.instBEqURI : BEq URI

Equations

• Std.Http.instBEqURI = { beq := Std.Http.instBEqURI.beq }

def Std.Http.instBEqURI.beq : URI → URI → Bool

Equations

• One or more equations did not get rendered due to their size.
• Std.Http.instBEqURI.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Std.Http.instToStringURI : ToString URI

Equations

• One or more equations did not get rendered due to their size.

structure Std.Http.URI.Builder : Type

Fluent builder for constructing URIs. Takes raw (unencoded) strings and handles encoding automatically when building the final URI.

• scheme : Option Scheme

  The URI scheme (e.g., "http", "https").

• userInfo : Option UserInfo

  User information (username and optional password).

• host : Option Host

  The host component.

• port : Port

  The port number.

• pathSegments : Array String

  Path segments (will be encoded when building).

• query : Array (String × Option String)

  Query parameters as (key, optional value) pairs (will be encoded when building).

• fragment : Option String

  Fragment identifier (will be encoded when building).

def Std.Http.URI.instInhabitedBuilder.default : Builder

Equations

• Std.Http.URI.instInhabitedBuilder.default = { scheme := default, userInfo := default, host := default, port := default, pathSegments := default, query := default, fragment := default }

@[implicit_reducible]

instance Std.Http.URI.instInhabitedBuilder : Inhabited Builder

Equations

• Std.Http.URI.instInhabitedBuilder = { default := Std.Http.URI.instInhabitedBuilder.default }

def Std.Http.URI.Builder.empty : Builder

Creates an empty URI builder.

Equations

• Std.Http.URI.Builder.empty = { }

def Std.Http.URI.Builder.setScheme? (b : Builder) (scheme : String) : Option Builder

Attempts to set the URI scheme (e.g., "http", "https"). Returns none if the scheme is not a valid RFC 3986 scheme. The stored scheme is normalized to lowercase.

Equations

• One or more equations did not get rendered due to their size.

def Std.Http.URI.Builder.setScheme! (b : Builder) (scheme : String) : Builder

Sets the URI scheme (e.g., "http", "https"). Panics if the scheme is invalid. Use setScheme? if you need a safe option-returning version.

Equations

• One or more equations did not get rendered due to their size.

def Std.Http.URI.Builder.setUserInfo (b : Builder) (username : String) (password : Option String := none) : Builder

Sets the user information with username and optional password. The strings will be automatically percent-encoded.

Equations

• One or more equations did not get rendered due to their size.

def Std.Http.URI.Builder.setHost? (b : Builder) (name : String) : Option Builder

Sets the host as a domain name, returning none if the name contains invalid characters. The domain name will be automatically lowercased. Only ASCII alphanumeric characters, hyphens, and dots are allowed. Each label cannot start or end with - and is limited to 63 characters. Internationalized domain names must be converted to punycode before use.

Equations

• One or more equations did not get rendered due to their size.

def Std.Http.URI.Builder.setHost! (b : Builder) (name : String) : Builder

Sets the host as a domain name, panicking if the name contains invalid characters. The domain name will be automatically lowercased. Only ASCII alphanumeric characters, hyphens, and dots are allowed. Each label cannot start or end with - and is limited to 63 characters. Internationalized domain names must be converted to punycode before use.

Equations

• One or more equations did not get rendered due to their size.

def Std.Http.URI.Builder.setHostIPv4 (b : Builder) (addr : Net.IPv4Addr) : Builder

Sets the host as an IPv4 address.

Equations

• One or more equations did not get rendered due to their size.

def Std.Http.URI.Builder.setHostIPv6 (b : Builder) (addr : Net.IPv6Addr) : Builder

Sets the host as an IPv6 address.

Equations

• One or more equations did not get rendered due to their size.

def Std.Http.URI.Builder.setPort (b : Builder) (port : UInt16) : Builder

Sets the port number.

Equations

• b.setPort port = { scheme := b.scheme, userInfo := b.userInfo, host := b.host, port := Std.Http.URI.Port.value port, pathSegments := b.pathSegments, query := b.query, fragment := b.fragment }

def Std.Http.URI.Builder.setPath (b : Builder) (segments : Array String) : Builder

Replaces all path segments. Segments will be automatically percent-encoded when building.

Equations

• b.setPath segments = { scheme := b.scheme, userInfo := b.userInfo, host := b.host, port := b.port, pathSegments := segments, query := b.query, fragment := b.fragment }

def Std.Http.URI.Builder.appendPathSegment (b : Builder) (segment : String) : Builder

Appends a single segment to the path. The segment will be automatically percent-encoded when building.

Equations

• One or more equations did not get rendered due to their size.

def Std.Http.URI.Builder.addQueryParam (b : Builder) (key value : String) : Builder

Adds a query parameter with a value. Both key and value will be automatically percent-encoded when building.

Equations

• One or more equations did not get rendered due to their size.

def Std.Http.URI.Builder.addQueryFlag (b : Builder) (key : String) : Builder

Adds a query parameter without a value (flag parameter). The key will be automatically percent-encoded when building.

Equations

• b.addQueryFlag key = { scheme := b.scheme, userInfo := b.userInfo, host := b.host, port := b.port, pathSegments := b.pathSegments, query := b.query.push (key, none), fragment := b.fragment }

def Std.Http.URI.Builder.setQuery (b : Builder) (query : Array (String × Option String)) : Builder

Replaces all query parameters. Keys and values will be automatically percent-encoded when building.

Equations

• b.setQuery query = { scheme := b.scheme, userInfo := b.userInfo, host := b.host, port := b.port, pathSegments := b.pathSegments, query := query, fragment := b.fragment }

def Std.Http.URI.Builder.setFragment (b : Builder) (fragment : String) : Builder

Sets the fragment identifier. The fragment will be automatically percent-encoded when building.

Equations

• b.setFragment fragment = { scheme := b.scheme, userInfo := b.userInfo, host := b.host, port := b.port, pathSegments := b.pathSegments, query := b.query, fragment := some fragment }

def Std.Http.URI.Builder.build (b : Builder) : URI

Builds a complete URI from the builder state, encoding all components. Defaults to "https" scheme if none is specified.

Equations

• One or more equations did not get rendered due to their size.

def Std.Http.URI.withScheme! (uri : URI) (scheme : String) : URI

Returns a new URI with the scheme replaced.

Equations

• uri.withScheme! scheme = { scheme := Std.Http.URI.Scheme.ofString! scheme, authority := uri.authority, path := uri.path, query := uri.query, fragment := uri.fragment }

def Std.Http.URI.withAuthority (uri : URI) (authority : Option Authority) : URI

Returns a new URI with the authority replaced.

Equations

• uri.withAuthority authority = { scheme := uri.scheme, authority := authority, path := uri.path, query := uri.query, fragment := uri.fragment }

def Std.Http.URI.withPath (uri : URI) (path : Path) : URI

Returns a new URI with the path replaced.

Equations

• uri.withPath path = { scheme := uri.scheme, authority := uri.authority, path := path, query := uri.query, fragment := uri.fragment }

def Std.Http.URI.withQuery (uri : URI) (query : Query) : URI

Returns a new URI with the query replaced.

Equations

• uri.withQuery query = { scheme := uri.scheme, authority := uri.authority, path := uri.path, query := query, fragment := uri.fragment }

def Std.Http.URI.withFragment (uri : URI) (fragment : Option String) : URI

Returns a new URI with the fragment replaced.

Equations

• uri.withFragment fragment = { scheme := uri.scheme, authority := uri.authority, path := uri.path, query := uri.query, fragment := fragment }

def Std.Http.URI.normalize (uri : URI) : URI

Partially normalizes a URI by removing dot-segments from the path (. and ..) according to RFC 3986 Section 5.2.4.

This does not apply the full normalization set from RFC 3986 Section 6 — for example, case normalization, percent-encoding normalization, and default-port normalization are not performed.

Equations

• uri.normalize = { scheme := uri.scheme, authority := uri.authority, path := uri.path.normalize, query := uri.query, fragment := uri.fragment }

inductive Std.Http.RequestTarget : Type

HTTP request target forms as defined in RFC 9112 Section 3.3.

Reference: https://www.rfc-editor.org/rfc/rfc9112.html#section-3.3

• originForm (path : URI.Path) (query : Option URI.Query) : RequestTarget

  Origin-form request target (most common for HTTP requests). Consists of a path and an optional query string. Example: /path/to/resource?key=value

• absoluteForm (uri : URI) : RequestTarget

  Absolute-form request target containing a complete URI. Used when making requests through a proxy. Example: http://example.com:8080/path?key=value

• authorityForm (authority : URI.Authority) : RequestTarget

  Authority-form request target (used for CONNECT requests). Example: example.com:443

• asteriskForm : RequestTarget

  Asterisk-form request target (used with OPTIONS requests). Example: *

@[implicit_reducible]

instance Std.Http.instInhabitedRequestTarget : Inhabited RequestTarget

Equations

• Std.Http.instInhabitedRequestTarget = { default := Std.Http.instInhabitedRequestTarget.default }

def Std.Http.instInhabitedRequestTarget.default : RequestTarget

Equations

• Std.Http.instInhabitedRequestTarget.default = Std.Http.RequestTarget.originForm default default

@[implicit_reducible]

instance Std.Http.instReprRequestTarget : Repr RequestTarget

Equations

• Std.Http.instReprRequestTarget = { reprPrec := Std.Http.instReprRequestTarget.repr }

def Std.Http.instReprRequestTarget.repr : RequestTarget → Nat → Format

Equations

• One or more equations did not get rendered due to their size.

def Std.Http.RequestTarget.path : RequestTarget → URI.Path

Extracts the path component from a request target, if available. Returns an empty relative path for targets without a path.

Equations

• (Std.Http.RequestTarget.originForm p query).path = p
• (Std.Http.RequestTarget.absoluteForm uri).path = uri.path
• x✝.path = { segments := #[], absolute := false }

def Std.Http.RequestTarget.query : RequestTarget → URI.Query

Extracts the query component from a request target, if available. Returns an empty array for targets without a query.

Equations

• (Std.Http.RequestTarget.originForm p query).query = query.getD Std.Http.URI.Query.empty
• (Std.Http.RequestTarget.absoluteForm uri).query = uri.query
• x✝.query = Std.Http.URI.Query.empty

def Std.Http.RequestTarget.authority? : RequestTarget → Option URI.Authority

Extracts the authority component from a request target, if available.

Equations

• (Std.Http.RequestTarget.authorityForm a).authority? = some a
• (Std.Http.RequestTarget.absoluteForm uri).authority? = uri.authority
• x✝.authority? = none

@[implicit_reducible]

instance Std.Http.RequestTarget.instToString : ToString RequestTarget

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Std.Http.RequestTarget.instEncodeV11 : Internal.Encode Version.v11 RequestTarget

Equations

• Std.Http.RequestTarget.instEncodeV11 = { encode := fun (buffer : Std.Http.Internal.ChunkedBuffer) (target : Std.Http.RequestTarget) => buffer.writeString (toString target) }