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.

@[instance_reducible]

instance Std.Http.instInhabitedHeaders : Inhabited Headers

Equations

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

@[instance_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) " }"

@[instance_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 }

@[instance_reducible]

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

Equations

• Std.Http.instDecidableMemNameHeaders name h = Std.Internal.IndexMultiMap.instDecidableMem name h.map

@[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.eraseMany (headers : Headers) (names : Array Header.Name) : Headers

Removes all headers whose names appear in names. Names not present are ignored. Cheaper than chaining erase calls because IndexMultiMap.eraseMany rebuilds the index once in total rather than once per erase call.

Equations

• headers.eraseMany names = { map := headers.map.eraseMany names }

@[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 }

@[instance_reducible]

instance Std.Http.Headers.instToString : ToString Headers

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

instance Std.Http.Headers.instEmptyCollection : EmptyCollection Headers

Equations

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

@[instance_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 }

@[instance_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 }

@[instance_reducible]

instance Std.Http.Headers.instUnion : Union Headers

Equations

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

@[instance_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.