High-level API for RFC 3986 URIs

This module exposes a small, convenient surface over the internal parsers, normalizers, and resolvers:

• parsing helpers for absolute URIs and RelativeRefs
• pretty-printers (string serialization) for URI and RelativeRef
• normalization and equivalence checks
• resolution of relative references against a base URI

It delegates to the Internal parser/normalizer/resolver implemented in LeanUri.Parsers, LeanUri.Normalization, and related modules.

@[inline]

def LeanUri.URI.parse : String → Except String URI

Parse an absolute URI from a string without applying normalization.

Returns .ok uri on success or .error msg if parsing fails.

Examples

open LeanUri
match URI.parse "https://example.com/a?b#c" with
| .ok u   => (u.scheme, u.authority.isSome, u.path) = ("https", true, "/a")
| .error _ => False

Equations

• LeanUri.URI.parse = LeanUri.Internal.uri.run

@[inline]

def LeanUri.RelativeRef.parse : String → Except String RelativeRef

Parse a RelativeRef (relative reference) from a string without normalization.

Returns .ok ref on success or .error msg on parse failure.

Examples

open LeanUri
match RelativeRef.parse "../x?y#z" with
| .ok r   => (r.authority, r.path, r.query, r.fragment) = (none, "../x", some "y", some "z")
| .error _ => False

Equations

• LeanUri.RelativeRef.parse = LeanUri.Internal.relativeRef.run

@[inline]

def LeanUri.parseReference : String → Except String (URI ⊕ RelativeRef)

Parse either an absolute URI or a RelativeRef from a string.

Returns Sum.inl uri for an absolute URI, or Sum.inr ref for a relative reference.

Examples

open LeanUri
( parseReference "mailto:user@example.com" ).isOk -- absolute → inl
( parseReference "./a/b" ).isOk                  -- relative → inr

Equations

• LeanUri.parseReference = LeanUri.Internal.uriReference.run

@[inline]

def LeanUri.URI.toString : URI → String

Serialize a URI to a string without applying any normalization.

This is a convenience wrapper around the ToString instance.

Examples

open LeanUri
let u : URI := { scheme := "https", authority := some "example.com", path := "/a", query := some "q=1", fragment := none }
URI.toString u = "https://example.com/a?q=1"

Equations

• LeanUri.URI.toString = toString

@[inline]

def LeanUri.RelativeRef.toString : RelativeRef → String

Serialize a RelativeRef to a string without applying any normalization.

This is a convenience wrapper around the ToString instance.

Examples

open LeanUri
let r : RelativeRef := { authority := some "example.com", path := "/p", query := none, fragment := some "frag" }
RelativeRef.toString r = "//example.com/p#frag"

Equations

• LeanUri.RelativeRef.toString = toString

@[inline]

def LeanUri.URI.normalize : URI → URI

Normalize all components of a URI according to the RFC 3986 rules implemented by this library (e.g., case normalization where applicable, removal of dot segments, etc.).

Examples

open LeanUri
let u : URI := { scheme := "http", authority := some "EXAMPLE.com", path := "/a/./b/../c", query := none, fragment := none }
URI.normalize u |>.toString = "http://example.com/a/c"

Equations

• LeanUri.URI.normalize = LeanUri.Internal.normalizeAll

def LeanUri.URI.resolveURIorRef (baseUri : URI) (reference : URI ⊕ RelativeRef) : URI

Resolve a reference or relative ref against a base URI.

• If reference is an absolute URI, it is returned as-is.
• If reference is a relative reference, it is resolved against baseUri using Internal.resolve.
• Returns .error msg when reference cannot be parsed as a URI or relative reference.

See URI.resolve or URI.resolveRef as well.

Equations

• baseUri.resolveURIorRef (Sum.inl absoluteUri) = absoluteUri
• baseUri.resolveURIorRef (Sum.inr relRef) = LeanUri.Internal.resolve baseUri relRef

def LeanUri.URI.resolve (baseUri : URI) (reference : String) : Except String URI

Resolve a string reference against a base URI.

• If reference is an absolute URI, it is returned as-is.
• If reference is a relative reference, it is resolved against baseUri using Internal.resolve.
• Returns .error msg when reference cannot be parsed as a URI or relative reference.

Examples

open LeanUri
let base : URI := { scheme := "https", authority := some "example.com", path := "/dir/index.html", query := none, fragment := none }
URI.resolve base "../x" = .ok { scheme := "https", authority := some "example.com", path := "/x", query := none, fragment := none }

Equations

• baseUri.resolve reference = match LeanUri.Internal.uriReference.run reference with | Except.ok sum => Except.ok (baseUri.resolveURIorRef sum) | Except.error e => Except.error e

@[inline]

def LeanUri.URI.resolveRef : URI → RelativeRef → URI

Resolve a pre-parsed RelativeRef against a base URI.

Examples

open LeanUri
let base : URI := { scheme := "https", authority := some "example.com", path := "/a/b/", query := none, fragment := none }
let rr   : RelativeRef := { authority := none, path := "c/../d", query := none, fragment := none }
URI.resolveRef base rr |>.toString = "https://example.com/a/d"

Equations

• LeanUri.URI.resolveRef = LeanUri.Internal.resolve

@[inline]

def LeanUri.URI.isAbsolute (uri : URI) : Bool

Return true when the URI has an authority component.

Note: This checks for the presence of an authority (i.e., //…), which is not the same as checking for the presence of a scheme.

Examples

open LeanUri
let a : URI := { scheme := "http",  authority := some "example.com", path := "/", query := none, fragment := none }
let b : URI := { scheme := "mailto", authority := none,               path := "user@example.com", query := none, fragment := none }
(URI.isAbsolute a, URI.isAbsolute b) = (true, false)

Equations

• uri.isAbsolute = uri.authority.isSome

@[inline]

def LeanUri.URI.equivalent (uri1 uri2 : URI) : Bool

Check whether two URIs are equivalent after normalization.

Examples

open LeanUri
let u1 : URI := { scheme := "http", authority := some "EXAMPLE.com", path := "/a/./b/../c", query := some "Q=1", fragment := none }
let u2 : URI := { scheme := "http", authority := some "example.COM", path := "/a/c",         query := some "q=1", fragment := none }
URI.equivalent u1 u2 = true

Equations

• uri1.equivalent uri2 = (uri1.normalize == uri2.normalize)

@[inline]

def LeanUri.URI.encode (scheme : String) (authority : Option String := none) (path : String := "") (query fragment : Option String := none) : URI

Construct a URI from raw (unencoded) components, automatically percent-encoding as required by RFC 3986. This ensures the resulting URI is valid and safe for serialization.

Equations

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

@[inline]

def LeanUri.RelativeRef.encode (authority : Option String := none) (path : String := "") (query fragment : Option String := none) : RelativeRef

Construct a RelativeRef from raw (unencoded) components, automatically percent-encoding as required by RFC 3986. This ensures the resulting RelativeRef is valid and safe for serialization.

Equations

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

@[inline]

def LeanUri.RelativeRef.getAuthority (r : RelativeRef) : Option String

Get the decoded (unescaped) authority component of a RelativeRef, if present.

Equations

• r.getAuthority = do let s ← r.authority match LeanUri.pctDecode s with | Except.ok r => some r | Except.error a => none

@[inline]

def LeanUri.RelativeRef.getPath (r : RelativeRef) : Option String

Get the decoded (unescaped) path component of a RelativeRef.

Equations

• r.getPath = match LeanUri.pctDecode r.path with | Except.ok r => some r | Except.error a => none

@[inline]

def LeanUri.RelativeRef.getQuery (r : RelativeRef) : Option String

Get the decoded (unescaped) query component of a RelativeRef, if present.

Equations

• r.getQuery = do let s ← r.query match LeanUri.pctDecode s with | Except.ok r => some r | Except.error a => none

@[inline]

def LeanUri.RelativeRef.getFragment (r : RelativeRef) : Option String

Get the decoded (unescaped) fragment component of a RelativeRef, if present.

Equations

• r.getFragment = do let s ← r.fragment match LeanUri.pctDecode s with | Except.ok r => some r | Except.error a => none

@[inline]

def LeanUri.URI.getAuthority (u : URI) : Option String

Get the decoded (unescaped) authority component of a URI, if present.

Equations

• u.getAuthority = do let s ← u.authority match LeanUri.pctDecode s with | Except.ok r => some r | Except.error a => none

@[inline]

def LeanUri.URI.getPath (u : URI) : Option String

Get the decoded (unescaped) path component of a URI.

Equations

• u.getPath = match LeanUri.pctDecode u.path with | Except.ok r => some r | Except.error a => none

@[inline]

def LeanUri.URI.getQuery (u : URI) : Option String

Get the decoded (unescaped) query component of a URI, if present.

Equations

• u.getQuery = do let s ← u.query match LeanUri.pctDecode s with | Except.ok r => some r | Except.error a => none

@[inline]

def LeanUri.URI.getFragment (u : URI) : Option String

Get the decoded (unescaped) fragment component of a URI, if present.

Equations

• u.getFragment = do let s ← u.fragment match LeanUri.pctDecode s with | Except.ok r => some r | Except.error a => none