Core data types for RFC 3986 URIs

This module defines the URI (absolute URI) and RelativeRef (relative reference) records, plus basic conversions and printer instances. Strings in fields are stored without their leading delimiters (no leading ? for query, no # for fragment, no // for authority).

The types store components exactly as parsed; normalization is performed elsewhere.

structure LeanUri.URI : Type

An absolute Uniform Resource Identifier as defined by RFC 3986.

All components are stored as they appear (no normalization is performed here).

• scheme : String
• authority : Option String
• path : String
• query : Option String
• fragment : Option String

instance LeanUri.instReprURI : Repr URI

Equations

• LeanUri.instReprURI = { reprPrec := LeanUri.instReprURI.repr }

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

Equations

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

def LeanUri.instBEqURI.beq : URI → URI → Bool

Equations

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

instance LeanUri.instBEqURI : BEq URI

Equations

• LeanUri.instBEqURI = { beq := LeanUri.instBEqURI.beq }

def LeanUri.instHashableURI.hash : URI → UInt64

Equations

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

instance LeanUri.instHashableURI : Hashable URI

Equations

• LeanUri.instHashableURI = { hash := LeanUri.instHashableURI.hash }

instance LeanUri.instInhabitedURI : Inhabited URI

Equations

• LeanUri.instInhabitedURI = { default := { scheme := "data", path := "" } }

structure LeanUri.RelativeRef : Type

A relative reference per RFC 3986 (i.e., no scheme).

This type can still include an authority, path, query, and fragment.

• authority : Option String
• path : String
• query : Option String
• fragment : Option String

def LeanUri.instInhabitedRelativeRef.default : RelativeRef

Equations

• LeanUri.instInhabitedRelativeRef.default = { authority := default, path := default, query := default, fragment := default }

instance LeanUri.instInhabitedRelativeRef : Inhabited RelativeRef

Equations

• LeanUri.instInhabitedRelativeRef = { default := LeanUri.instInhabitedRelativeRef.default }

def LeanUri.instReprRelativeRef.repr : RelativeRef → Nat → Std.Format

Equations

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

instance LeanUri.instReprRelativeRef : Repr RelativeRef

Equations

• LeanUri.instReprRelativeRef = { reprPrec := LeanUri.instReprRelativeRef.repr }

instance LeanUri.instBEqRelativeRef : BEq RelativeRef

Equations

• LeanUri.instBEqRelativeRef = { beq := LeanUri.instBEqRelativeRef.beq }

def LeanUri.instBEqRelativeRef.beq : RelativeRef → RelativeRef → Bool

Equations

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

def LeanUri.instHashableRelativeRef.hash : RelativeRef → UInt64

Equations

• LeanUri.instHashableRelativeRef.hash { authority := a, path := a_1, query := a_2, fragment := a_3 } = mixHash (mixHash (mixHash (mixHash 0 (hash a)) (hash a_1)) (hash a_2)) (hash a_3)

instance LeanUri.instHashableRelativeRef : Hashable RelativeRef

Equations

• LeanUri.instHashableRelativeRef = { hash := LeanUri.instHashableRelativeRef.hash }

def LeanUri.URI.toRelativeRef (uri : URI) : RelativeRef

Drop the scheme of a URI and convert it to a RelativeRef, keeping all other components unchanged.

Equations

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

instance LeanUri.instToStringRelativeRef : ToString RelativeRef

Serialize a RelativeRef to its RFC 3986 string form.

Includes //authority when present, appends ?query and #fragment when present, and does not apply any normalization.

Equations

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

instance LeanUri.instToStringURI : ToString URI

Serialize a URI to scheme ":" followed by the serialization of its relative part. The output is not normalized.

Equations

• LeanUri.instToStringURI = { toString := fun (uri : LeanUri.URI) => uri.scheme ++ ":" ++ toString uri.toRelativeRef }