Internal String Helpers

Shared string utilities for HTTP: token validation and quoted-string encoding/decoding for header parameter values and chunk extensions.

def Std.Http.Internal.quoteCore (c : Char) (h₀ : Char.quotedStringChar c = true) : String

Core character quoting used by quoteHttpString.

Emits qdtext characters directly and " / \\ as quoted-pair. The proof h₀ : quotedStringChar c guarantees the impossible branch is unreachable.

Equations

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

def Std.Http.Internal.quoteHttpString (s : String) (h : s.toList.all Char.quotedStringChar = true) : String

Quotes s as an HTTP quoted-string: DQUOTE *( qdtext / quoted-pair ) DQUOTE.

If every character is a tchar and the string is non-empty, the string is returned as-is (it is already a valid token). Otherwise the string is wrapped in double quotes, escaping " and \ as quoted-pair.

Requires a proof that every character passes quotedStringChar.

Equations

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

def Std.Http.Internal.quoteHttpString? (s : String) : Option String

Attempts to quote s as an HTTP quoted-string.

Returns some with the quoted result when every character passes quotedStringChar, or none when any character cannot be represented by the grammar.

Equations

• Std.Http.Internal.quoteHttpString? s = if h : s.toList.all Std.Http.Internal.Char.quotedStringChar = true then some (Std.Http.Internal.quoteHttpString s h) else none

def Std.Http.Internal.quoteHttpString! (s : String) : String

Quotes s as an HTTP quoted-string, panicking if s contains characters that cannot be represented by qdtext/quoted-pair.

Equations

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

def Std.Http.Internal.unquoteHttpString? (s : String) : Option String

Parses an HTTP quoted-string, returning the unescaped content when valid.

Equations

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

def Std.Http.Internal.isToken (s : String) : Bool

Checks whether a string is a valid non-empty HTTP token.

Equations

• Std.Http.Internal.isToken s = decide (¬s.toList.isEmpty = true ∧ s.toList.all Std.Http.Internal.Char.tchar = true)