Headers

This module defines the Headers type, which represents a collection of HTTP header name-value pairs.

Reference: https://www.rfc-editor.org/rfc/rfc9110.html#section-5

structure Std.Http.Headers : Type

A structure for managing HTTP headers as key-value pairs.

Reference: https://www.rfc-editor.org/rfc/rfc9110.html#section-5

• map : Internal.IndexMultiMap Header.Name Header.Value

  The underlying multimap that stores headers.

@[implicit_reducible]

instance Std.Http.instInhabitedHeaders : Inhabited Headers

Equations

• Std.Http.instInhabitedHeaders = { default := Std.Http.instInhabitedHeaders.default }

def Std.Http.instInhabitedHeaders.default : Headers

Equations

• Std.Http.instInhabitedHeaders.default = { map := default }

@[implicit_reducible]

instance Std.Http.instReprHeaders : Repr Headers

Equations

• Std.Http.instReprHeaders = { reprPrec := Std.Http.instReprHeaders.repr }

def Std.Http.instReprHeaders.repr : Headers → Nat → Format

Equations

• Std.Http.instReprHeaders.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "map" ++ Std.Format.text " := " ++ (Std.Format.nest 7 (repr x✝.map)).group) " }"

@[implicit_reducible]

instance Std.Http.instMembershipNameHeaders : Membership Header.Name Headers

Equations

• Std.Http.instMembershipNameHeaders = { mem := fun (headers : Std.Http.Headers) (name : Std.Http.Header.Name) => name ∈ headers.map }

@[implicit_reducible]

instance Std.Http.instDecidableMemNameHeaders (name : Header.Name) (h : Headers) : Decidable (name ∈ h)

Equations

• Std.Http.instDecidableMemNameHeaders name h = (h.map.indexes.inner.contains name).decEq true

@[inline]

def Std.Http.Headers.get (headers : Headers) (name : Header.Name) (h : name ∈ headers) : Header.Value

Retrieves the first Header.Value for the given key.

Equations

• headers.get name h = headers.map.get name h

@[inline]

def Std.Http.Headers.getAll (headers : Headers) (name : Header.Name) (h : name ∈ headers) : Array Header.Value

Retrieves all Header.Value entries for the given key.

Equations

• headers.getAll name h = headers.map.getAll name h

@[inline]

def Std.Http.Headers.getAll? (headers : Headers) (name : Header.Name) : Option (Array Header.Value)

Like getAll, but returns none instead of requiring a membership proof. Returns none if the header is absent.

Equations

• headers.getAll? name = headers.map.getAll? name

@[inline]

def Std.Http.Headers.get? (headers : Headers) (name : Header.Name) : Option Header.Value

Retrieves the first Header.Value for the given key. Returns none if the header is absent.

Equations

• headers.get? name = headers.map.get? name

@[inline]

def Std.Http.Headers.hasEntry (headers : Headers) (name : Header.Name) (value : Header.Value) : Bool

Checks if the entry is present in the Headers.

Equations

• headers.hasEntry name value = headers.map.hasEntry name value

@[inline]

def Std.Http.Headers.getLast? (headers : Headers) (name : Header.Name) : Option Header.Value

Retrieves the last header value for the given key. Returns none if the header is absent.

Equations

• headers.getLast? name = headers.map.getLast? name

@[inline]

def Std.Http.Headers.getD (headers : Headers) (name : Header.Name) (d : Header.Value) : Header.Value

Like get?, but returns a default value if absent.

Equations

• headers.getD name d = headers.map.getD name d

@[inline]

def Std.Http.Headers.get! (headers : Headers) (name : Header.Name) : Header.Value

Like get?, but panics if absent.

Equations

• headers.get! name = headers.map.get! name

@[inline]

def Std.Http.Headers.insert (headers : Headers) (key : Header.Name) (value : Header.Value) : Headers

Inserts a new key-value pair into the headers.

Equations

• headers.insert key value = { map := headers.map.insert key value }

@[inline]

def Std.Http.Headers.insert! (headers : Headers) (name value : String) : Headers

Adds a header from string name and value, panicking if either is invalid.

Equations

• headers.insert! name value = headers.insert (Std.Http.Header.Name.ofString! name) (Std.Http.Header.Value.ofString! value)

@[inline]

def Std.Http.Headers.insert? (headers : Headers) (name value : String) : Option Headers

Adds a header from string name and value. Returns none if either the header name or value is invalid.

Equations

• headers.insert? name value = do let name ← Std.Http.Header.Name.ofString? name let value ← Std.Http.Header.Value.ofString? value pure (headers.insert name value)

@[inline]

def Std.Http.Headers.insertMany (headers : Headers) (key : Header.Name) (values : Array Header.Value) : Headers

Inserts a new key with an array of values.

Equations

• headers.insertMany key values = { map := headers.map.insertMany key values }

def Std.Http.Headers.empty : Headers

Creates empty headers.

Equations

• Std.Http.Headers.empty = { map := ∅ }

def Std.Http.Headers.ofList (pairs : List (Header.Name × Header.Value)) : Headers

Creates headers from a list of key-value pairs.

Equations

• Std.Http.Headers.ofList pairs = { map := Std.Internal.IndexMultiMap.ofList pairs }

@[inline]

def Std.Http.Headers.contains (headers : Headers) (name : Header.Name) : Bool

Checks if a header with the given name exists.

Equations

• headers.contains name = headers.map.contains name

@[inline]

def Std.Http.Headers.erase (headers : Headers) (name : Header.Name) : Headers

Removes a header with the given name.

Equations

• headers.erase name = { map := headers.map.erase name }

@[inline]

def Std.Http.Headers.size (headers : Headers) : Nat

Gets the number of headers.

Equations

• headers.size = headers.map.size

@[inline]

def Std.Http.Headers.isEmpty (headers : Headers) : Bool

Checks if the headers are empty.

Equations

• headers.isEmpty = headers.map.isEmpty

def Std.Http.Headers.merge (headers1 headers2 : Headers) : Headers

Merges two headers, accumulating values for duplicate keys from both.

Equations

• headers1.merge headers2 = { map := headers1.map ∪ headers2.map }

def Std.Http.Headers.toList (headers : Headers) : List (Header.Name × Header.Value)

Converts the headers to a list of key-value pairs (flattened). Each header with multiple values produces multiple pairs.

Equations

• headers.toList = headers.map.toList

def Std.Http.Headers.toArray (headers : Headers) : Array (Header.Name × Header.Value)

Converts the headers to an array of key-value pairs (flattened). Each header with multiple values produces multiple pairs.

Equations

• headers.toArray = headers.map.toArray

def Std.Http.Headers.fold {α : Type u_1} (headers : Headers) (init : α) (f : α → Header.Name → Header.Value → α) : α

Folds over all key-value pairs in the headers.

Equations

• headers.fold init f = Array.foldl (fun (acc : α) (x : Std.Http.Header.Name × Std.Http.Header.Value) => match x with | (k, v) => f acc k v) init headers.map.toArray

def Std.Http.Headers.mapValues (headers : Headers) (f : Header.Name → Header.Value → Header.Value) : Headers

Maps a function over all header values, producing new headers.

Equations

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

def Std.Http.Headers.filterMap (headers : Headers) (f : Header.Name → Header.Value → Option Header.Value) : Headers

Filters and maps over header key-value pairs. Returns only the pairs for which the function returns some.

Equations

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

def Std.Http.Headers.filter (headers : Headers) (f : Header.Name → Header.Value → Bool) : Headers

Filters header key-value pairs, keeping only those that satisfy the predicate.

Equations

• headers.filter f = headers.filterMap fun (k : Std.Http.Header.Name) (v : Std.Http.Header.Value) => if f k v = true then some v else none

def Std.Http.Headers.update (headers : Headers) (name : Header.Name) (f : Header.Value → Header.Value) : Headers

Updates all the values of a header if it exists.

Equations

• headers.update name f = { map := headers.map.update name f }

@[inline]

def Std.Http.Headers.replaceLast (headers : Headers) (name : Header.Name) (value : Header.Value) : Headers

Replaces the last value for the given header name. If the header is absent, returns the headers unchanged.

Equations

• headers.replaceLast name value = { map := headers.map.replaceLast name value }

@[implicit_reducible]

instance Std.Http.Headers.instToString : ToString Headers

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance Std.Http.Headers.instEmptyCollection : EmptyCollection Headers

Equations

• Std.Http.Headers.instEmptyCollection = { emptyCollection := Std.Http.Headers.empty }

@[implicit_reducible]

instance Std.Http.Headers.instSingletonProdNameValue : Singleton (Header.Name × Header.Value) Headers

Equations

• Std.Http.Headers.instSingletonProdNameValue = { singleton := fun (x : Std.Http.Header.Name × Std.Http.Header.Value) => match x with | (a, b) => ∅.insert a b }

@[implicit_reducible]

instance Std.Http.Headers.instInsertProdNameValue : Insert (Header.Name × Header.Value) Headers

Equations

• Std.Http.Headers.instInsertProdNameValue = { insert := fun (x : Std.Http.Header.Name × Std.Http.Header.Value) (s : Std.Http.Headers) => match x with | (a, b) => s.insert a b }

@[implicit_reducible]

instance Std.Http.Headers.instUnion : Union Headers

Equations

• Std.Http.Headers.instUnion = { union := Std.Http.Headers.merge }

@[implicit_reducible]

instance Std.Http.Headers.instForInProdNameValueOfMonad {m : Type u_1 → Type u_2} [Monad m] : ForIn m Headers (Header.Name × Header.Value)

Equations

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