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

@[reducible, inline]

abbrev Std.Http.URI.Scheme : Type

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

@[implicit_reducible]

instance Std.Http.URI.instInhabitedScheme : Inhabited Scheme

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.

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

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

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.

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

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

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

@[implicit_reducible]

instance Std.Http.URI.instInhabitedUserInfo : Inhabited UserInfo

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

@[implicit_reducible]

instance Std.Http.URI.instReprUserInfo : Repr UserInfo

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

@[implicit_reducible]

instance Std.Http.URI.instBEqUserInfo : BEq UserInfo

@[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.

@[inline]

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

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

@[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.

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

@[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.

@[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

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.

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

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

@[implicit_reducible]

instance Std.Http.URI.instBEqHost : BEq Host

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

@[implicit_reducible]

instance Std.Http.URI.instReprHost : Repr Host

@[implicit_reducible]

instance Std.Http.URI.instToStringHost : ToString Host

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

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

@[implicit_reducible]

instance Std.Http.URI.instReprPort : Repr Port

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

@[implicit_reducible]

instance Std.Http.URI.instDecidableEqPort : DecidableEq Port

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

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

@[implicit_reducible]

instance Std.Http.URI.instInhabitedAuthority : Inhabited Authority

@[implicit_reducible]

instance Std.Http.URI.instReprAuthority : Repr Authority

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

@[implicit_reducible]

instance Std.Http.URI.instBEqAuthority : BEq Authority

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

@[implicit_reducible]

instance Std.Http.URI.instToStringAuthority : ToString Authority

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

@[implicit_reducible]

instance Std.Http.URI.instInhabitedPath : Inhabited Path

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

@[implicit_reducible]

instance Std.Http.URI.instReprPath : Repr Path

@[implicit_reducible]

instance Std.Http.URI.instBEqPath : BEq Path

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

@[implicit_reducible]

instance Std.Http.URI.instToStringPath : ToString Path

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

Returns true if the path has no segments.

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.

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.

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

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

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

Appends an already-encoded segment to the path.

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.

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.

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

@[implicit_reducible]

instance Std.Http.URI.instReprQuery : Repr Query

@[implicit_reducible]

instance Std.Http.URI.instInhabitedQuery : Inhabited Query

@[implicit_reducible]

instance Std.Http.URI.instBEqQuery : BEq Query

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

Extracts all unique query parameter names.

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

Extracts all query parameter values.

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.

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.

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.

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.

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.

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.

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

Adds a query parameter to the query string.

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.

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

Creates an empty query string.

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

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

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

Checks if a query parameter exists.

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.

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

Removes all occurrences of a query parameter by key name.

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.

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.

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.

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.

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"

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

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

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

@[implicit_reducible]

instance Std.Http.instInhabitedURI : Inhabited URI

def Std.Http.instInhabitedURI.default : URI

@[implicit_reducible]

instance Std.Http.instBEqURI : BEq URI

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

@[implicit_reducible]

instance Std.Http.instToStringURI : ToString URI

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

@[implicit_reducible]

instance Std.Http.URI.instInhabitedBuilder : Inhabited Builder

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

Creates an empty URI builder.

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.

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.

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.

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.

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.

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

Sets the host as an IPv4 address.

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

Sets the host as an IPv6 address.

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

Sets the port number.

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

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

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.

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.

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.

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.

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

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

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.

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

Returns a new URI with the scheme replaced.

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

Returns a new URI with the authority replaced.

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

Returns a new URI with the path replaced.

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

Returns a new URI with the query replaced.

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

Returns a new URI with the fragment replaced.

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.

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

def Std.Http.instInhabitedRequestTarget.default : RequestTarget

@[implicit_reducible]

instance Std.Http.instReprRequestTarget : Repr RequestTarget

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

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.

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.

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

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

@[implicit_reducible]

instance Std.Http.RequestTarget.instToString : ToString RequestTarget

@[implicit_reducible]

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