Character Predicates (RFC 3986 Section 2)

def LeanUri.Internal.isAlpha (c : Char) : Bool

ALPHA = %x41-5A / %x61-7A (A-Z / a-z)

Equations

• LeanUri.Internal.isAlpha c = (decide ('A' ≤ c) && decide (c ≤ 'Z') || decide ('a' ≤ c) && decide (c ≤ 'z'))

def LeanUri.Internal.isHexDigit (c : Char) : Bool

HEXDIG = DIGIT / "A" / "B" / "C" / "D" / "E" / "F"

Equations

• LeanUri.Internal.isHexDigit c = (decide ('0' ≤ c) && decide (c ≤ '9') || decide ('A' ≤ c) && decide (c ≤ 'F') || decide ('a' ≤ c) && decide (c ≤ 'f'))

def LeanUri.Internal.isUnreserved (c : Char) : Bool

unreserved = ALPHA / DIGIT / "-" / "." / "_" / "~"

Equations

• LeanUri.Internal.isUnreserved c = (LeanUri.Internal.isAlpha c || decide ('0' ≤ c) && decide (c ≤ '9') || c == '-' || c == '.' || c == '_' || c == '~')

def LeanUri.Internal.isGenDelim (c : Char) : Bool

gen-delims = ":" / "/" / "?" / "#" / "[" / "]" / "@"

Equations

• LeanUri.Internal.isGenDelim c = (c == ':' || c == '/' || c == '?' || c == '#' || c == '[' || c == ']' || c == '@')

def LeanUri.Internal.isSubDelim (c : Char) : Bool

sub-delims = "!" / "$" / "&" / "'" / "(" / ")" / "*" / "+" / "," / ";" / "="

Equations

• LeanUri.Internal.isSubDelim c = (c == '!' || c == '$' || c == '&' || c == '\'' || c == '(' || c == ')' || c == '*' || c == '+' || c == ',' || c == ';' || c == '=')

def LeanUri.Internal.isReserved (c : Char) : Bool

reserved = gen-delims / sub-delims

Equations

• LeanUri.Internal.isReserved c = (LeanUri.Internal.isGenDelim c || LeanUri.Internal.isSubDelim c)

Basic Parsers (RFC 3986 Section 2)

partial def LeanUri.Internal.manyStrings (p : Std.Internal.Parsec.String.Parser String) (acc : String := "") : Std.Internal.Parsec.String.Parser String

Parse zero or more with a parser and accumulate the results into a string

def LeanUri.Internal.manyStrings1 (p : Std.Internal.Parsec.String.Parser String) : Std.Internal.Parsec.String.Parser String

Equations

• LeanUri.Internal.manyStrings1 p = do let __do_lift ← p LeanUri.Internal.manyStrings p __do_lift

def LeanUri.Internal.pctEncoded : Std.Internal.Parsec.String.Parser String

Parse a percent-encoded octet: pct-encoded = "%" HEXDIG HEXDIG

Equations

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

def LeanUri.Internal.unreserved : Std.Internal.Parsec.String.Parser Char

unreserved = ALPHA / DIGIT / "-" / "." / "_" / "~"

Equations

• LeanUri.Internal.unreserved = Std.Internal.Parsec.satisfy LeanUri.Internal.isUnreserved

def LeanUri.Internal.subDelims : Std.Internal.Parsec.String.Parser Char

sub-delims = "!" / "$" / "&" / "'" / "(" / ")" / "*" / "+" / "," / ";" / "="

Equations

• LeanUri.Internal.subDelims = Std.Internal.Parsec.satisfy LeanUri.Internal.isSubDelim

Component-specific allowed character predicates (RFC 3986)

def LeanUri.Internal.isPathChar (c : Char) : Bool

Allowed in a path segment: unreserved, sub-delims, ':', '@' -

Equations

• LeanUri.Internal.isPathChar c = (LeanUri.Internal.isUnreserved c || LeanUri.Internal.isSubDelim c || c == ':' || c == '@' || c == '/')

def LeanUri.Internal.isQueryOrFragmentChar (c : Char) : Bool

Allowed in a query or fragment: unreserved, sub-delims, ':', '@', '/', '?' -

Equations

• LeanUri.Internal.isQueryOrFragmentChar c = (LeanUri.Internal.isUnreserved c || LeanUri.Internal.isSubDelim c || c == ':' || c == '@' || c == '/' || c == '?')

def LeanUri.Internal.isUserinfoChar (c : Char) : Bool

Allowed in userinfo: unreserved, sub-delims, ':' -

Equations

• LeanUri.Internal.isUserinfoChar c = (LeanUri.Internal.isUnreserved c || LeanUri.Internal.isSubDelim c || c == ':')

def LeanUri.Internal.isRegNameChar (c : Char) : Bool

Allowed in reg-name (host): unreserved, sub-delims -

Equations

• LeanUri.Internal.isRegNameChar c = (LeanUri.Internal.isUnreserved c || LeanUri.Internal.isSubDelim c)

def LeanUri.Internal.isPortChar (c : Char) : Bool

Allowed in port: digit -

Equations

• LeanUri.Internal.isPortChar c = (decide ('0' ≤ c) && decide (c ≤ '9'))

Percent Decoding Chars

def LeanUri.Internal.hexCharToUInt8 (c : Char) : UInt8

Convert a hexadecimal character to its numeric value. Assumes input is a valid HEXDIG (produced by the parser).

Equations

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

def LeanUri.Internal.uInt8toOneHexChar (x : UInt8) : Char

Equations

• LeanUri.Internal.uInt8toOneHexChar x = if x < 10 then Char.ofUInt8 (x + '0'.toUInt8) else if x < 16 then Char.ofUInt8 (x + 'A'.toUInt8) else Char.ofUInt8 0

def LeanUri.Internal.uInt8ToHexChars (c : UInt8) : String

Convert a UInt8 to percent encoded

Equations

• LeanUri.Internal.uInt8ToHexChars c = toString "%" ++ toString (LeanUri.Internal.uInt8toOneHexChar (c / 16)) ++ toString (LeanUri.Internal.uInt8toOneHexChar (c % 16))

def LeanUri.Internal.decodeCharsToUInt8 (h1 h2 : Char) : UInt8

Equations

• LeanUri.Internal.decodeCharsToUInt8 h1 h2 = LeanUri.Internal.hexCharToUInt8 h1 * 16 + LeanUri.Internal.hexCharToUInt8 h2

def LeanUri.Internal.parseOnePctNormalize (allowed : Char → Bool) : Std.Internal.Parsec.String.Parser String

Equations

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

def LeanUri.Internal.pctDecodeOne : Std.Internal.Parsec.String.Parser UInt8

Equations

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

@[specialize #[]]

partial def LeanUri.Internal.manyAppendCore {α ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Std.Internal.Parsec.Input ι elem idx] [Append α] (p : Std.Internal.Parsec ι α) (acc : α) : Std.Internal.Parsec ι α

@[inline]

def LeanUri.Internal.manyAppendArray {ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Std.Internal.Parsec.Input ι elem idx] {β : Type} (p : Std.Internal.Parsec ι (Array β)) : Std.Internal.Parsec ι (Array β)

Equations

• LeanUri.Internal.manyAppendArray p = LeanUri.Internal.manyAppendCore p #[]

@[inline]

def LeanUri.Internal.manyAppendList {ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Std.Internal.Parsec.Input ι elem idx] {β : Type} (p : Std.Internal.Parsec ι (List β)) : Std.Internal.Parsec ι (List β)

Equations

• LeanUri.Internal.manyAppendList p = LeanUri.Internal.manyAppendCore p []

@[inline]

def LeanUri.Internal.manyAppendString {ι elem idx : Type} [DecidableEq idx] [DecidableEq elem] [Std.Internal.Parsec.Input ι elem idx] (p : Std.Internal.Parsec ι String) : Std.Internal.Parsec ι String

Equations

• LeanUri.Internal.manyAppendString p = LeanUri.Internal.manyAppendCore p ""

def LeanUri.Internal.pctDecodeToByteString : Std.Internal.Parsec.String.Parser ByteArray

Equations

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

def LeanUri.Internal.pctEncodeChar (c : Char) : String

Equations

• LeanUri.Internal.pctEncodeChar c = String.join (Array.map LeanUri.Internal.uInt8ToHexChars c.toString.toUTF8.data).toList

def LeanUri.Internal.parsePctNormalize (allowed : Char → Bool) : Std.Internal.Parsec.String.Parser String

Equations

• LeanUri.Internal.parsePctNormalize allowed = LeanUri.Internal.manyAppendString (LeanUri.Internal.parseOnePctNormalize allowed <|> toString <$> Std.Internal.Parsec.any)

def LeanUri.Internal.pctNormalize (allowed : Char → Bool) (s : String) : String

Equations

• LeanUri.Internal.pctNormalize allowed s = match (LeanUri.Internal.parsePctNormalize allowed).run s with | Except.ok result => result | Except.error a => s

def LeanUri.pctDecode (s : String) : Except String String

Decode percent encoded string into ordinary string.

Equations

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

def LeanUri.pctEncode (allowed : Char → Bool) (s : String) : String

Encode all allowed chars in a string to percent encoded bytes

Equations

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