This file defines a simple map data types, backed by a sorted duplicate-free list of key-value. Functions maps assume but don't require that their inputs are well-formed (sorted and duplicate-free). Separate theorems show that these functions produce well-formed outputs when given well-formed inputs.

Use Map.make to construct well-formed maps from lists of key-value pairs.

inductive Cedar.Data.Map (α : Type u) (β : Type v) : Type (max u v)

• mk {α : Type u} {β : Type v} : List (α × β) → Map α β

instance Cedar.Data.instReprMap {α✝ : Type u_1} {β✝ : Type u_2} [Repr α✝] [Repr β✝] : Repr (Map α✝ β✝)

Equations

• Cedar.Data.instReprMap = { reprPrec := Cedar.Data.instReprMap.repr }

def Cedar.Data.instReprMap.repr {α✝ : Type u_1} {β✝ : Type u_2} [Repr α✝] [Repr β✝] : Map α✝ β✝ → Nat → Std.Format

Equations

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

def Cedar.Data.instDecidableEqMap.decEq {α✝ : Type u_1} {β✝ : Type u_2} [DecidableEq α✝] [DecidableEq β✝] (x✝ x✝¹ : Map α✝ β✝) : Decidable (x✝ = x✝¹)

Equations

• Cedar.Data.instDecidableEqMap.decEq (Cedar.Data.Map.mk a) (Cedar.Data.Map.mk b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance Cedar.Data.instDecidableEqMap {α✝ : Type u_1} {β✝ : Type u_2} [DecidableEq α✝] [DecidableEq β✝] : DecidableEq (Map α✝ β✝)

Equations

• Cedar.Data.instDecidableEqMap = Cedar.Data.instDecidableEqMap.decEq

def Cedar.Data.instInhabitedMap.default {a✝ : Type u_1} {a✝¹ : Type u_2} : Map a✝ a✝¹

Equations

• Cedar.Data.instInhabitedMap.default = Cedar.Data.Map.mk default

instance Cedar.Data.instInhabitedMap {a✝ : Type u_1} {a✝¹ : Type u_2} : Inhabited (Map a✝ a✝¹)

Equations

• Cedar.Data.instInhabitedMap = { default := Cedar.Data.instInhabitedMap.default }

def Cedar.Data.Map.make {α : Type u_1} {β : Type u_2} [LT α] [DecidableLT α] (kvs : List (α × β)) : Map α β

Creates a well-formed map from the given list of pairs.

Equations

• Cedar.Data.Map.make kvs = Cedar.Data.Map.mk (List.canonicalize Prod.fst kvs)

def Cedar.Data.Map.empty {α : Type u_1} {β : Type u_2} : Map α β

Empty map

Equations

• Cedar.Data.Map.empty = Cedar.Data.Map.mk []

def Cedar.Data.Map.toList {α : Type u} {β : Type v} (m : Map α β) : List (α × β)

Returns an ordered and duplicate free list provided the given map is well-formed.

Equations

• m.toList = m.1

def Cedar.Data.Map.keys {α : Type u_1} {β : Type u_2} (m : Map α β) : Set α

Returns the keys of m as a set.

Equations

• m.keys = Cedar.Data.Set.mk (List.map Prod.fst m.toList)

def Cedar.Data.Map.values {α : Type u_1} {β : Type u_2} (m : Map α β) : List β

Returns the values of m as a list.

Equations

• m.values = List.map Prod.snd m.toList

def Cedar.Data.Map.find? {α : Type u_1} {β : Type u_2} [BEq α] (m : Map α β) (k : α) : Option β

Returns the binding for k in m, if any.

Equations

• m.find? k = match List.find? (fun (x : α × β) => match x with | (k', snd) => k' == k) m.toList with | some (fst, v) => some v | x => none

def Cedar.Data.Map.contains {α : Type u_1} {β : Type u_2} [BEq α] (m : Map α β) (k : α) : Bool

Returns true if m contains a mapping for the key k.

Equations

• m.contains k = (m.find? k).isSome

def Cedar.Data.Map.findOrErr {α : Type u_1} {β : Type u_2} {ε : Type u_3} [BEq α] (m : Map α β) (k : α) (err : ε) : Except ε β

Returns the binding for k in m or err if none is found.

Equations

• m.findOrErr k err = match m.find? k with | some v => Except.ok v | x => Except.error err

def Cedar.Data.Map.find! {α : Type u_1} {β : Type u_2} [Repr α] [BEq α] [Inhabited β] (m : Map α β) (k : α) : β

Returns the binding for k in m, or panics if none is found.

Equations

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

def Cedar.Data.Map.filter {α : Type u_1} {β : Type u_2} (f : α → β → Bool) (m : Map α β) : Map α β

Filters m using f.

Equations

• Cedar.Data.Map.filter f m = Cedar.Data.Map.mk (List.filter (fun (x : α × β) => match x with | (k, v) => f k v) m.toList)

def Cedar.Data.Map.size {α : Type u_1} {β : Type u_2} (m : Map α β) : Nat

Equations

• m.size = m.toList.length

def Cedar.Data.Map.mapOnValues {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β → γ) (m : Map α β) : Map α γ

Equations

• Cedar.Data.Map.mapOnValues f m = Cedar.Data.Map.mk (List.map (fun (x : α × β) => match x with | (k, v) => (k, f v)) m.toList)

def Cedar.Data.Map.mapOnKeys {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LT γ] [DecidableLT γ] (f : α → γ) (m : Map α β) : Map γ β

Equations

• Cedar.Data.Map.mapOnKeys f m = Cedar.Data.Map.make (List.map (fun (x : α × β) => match x with | (k, v) => (f k, v)) m.toList)

def Cedar.Data.Map.mapMOnValues {m : Type (max u_1 u_2) → Type u_3} {α : Type u_2} {β : Type u_4} {γ : Type (max u_1 u_2)} [LT α] [DecidableLT α] [Monad m] (f : β → m γ) (map : Map α β) : m (Map α γ)

Equations

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

def Cedar.Data.Map.mapMOnKeys {m : Type (max u_1 u_2) → Type u_3} {α : Type u_4} {β : Type u_2} {γ : Type (max u_1 u_2)} [LT γ] [DecidableLT γ] [Monad m] (f : α → m γ) (map : Map α β) : m (Map γ β)

Equations

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

def Cedar.Data.Map.mapOnValues₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SizeOf α] [SizeOf β] (m : Map α β) (f : { x : β // sizeOf x < sizeOf m } → γ) : Map α γ

Equations

• m.mapOnValues₂ f = Cedar.Data.Map.mk (m.toList.map₂ fun (x : { x : α × β // sizeOf x.snd < 1 + sizeOf m.toList }) => match x with | ⟨(k, v), h⟩ => (k, f ⟨v, ⋯⟩))

def Cedar.Data.Map.mapMOnValues₂ {m : Type (max u_1 u_2) → Type u_3} {α : Type u_2} {β : Type u_4} {γ : Type (max u_1 u_2)} [SizeOf α] [SizeOf β] [Monad m] (map : Map α β) (f : { x : β // sizeOf x < sizeOf map } → m γ) : m (Map α γ)

Equations

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

def Cedar.Data.Map.wellFormed {α : Type u_1} {β : Type u_2} [LT α] [DecidableLT α] (m : Map α β) : Bool

Equations

• m.wellFormed = m.toList.isSortedBy Prod.fst

instance Cedar.Data.Map.instLTOfProd {α : Type u_1} {β : Type u_2} [LT (α × β)] : LT (Map α β)

Equations

• Cedar.Data.Map.instLTOfProd = { lt := fun (a b : Cedar.Data.Map α β) => a.1 < b.1 }

instance Cedar.Data.Map.decLt {α : Type u_1} {β : Type u_2} [LT (α × β)] [DecidableEq (α × β)] [DecidableLT (α × β)] (n m : Map α β) : Decidable (n < m)

Equations

• (Cedar.Data.Map.mk nkvs).decLt (Cedar.Data.Map.mk mkvs) = nkvs.decidableLT mkvs

instance Cedar.Data.Map.instMembership {α : Type u_1} {β : Type u_2} : Membership α (Map α β)

Equations

• Cedar.Data.Map.instMembership = { mem := fun (m : Cedar.Data.Map α β) (a : α) => List.Mem a (List.map Prod.fst m.toList) }

instance Cedar.Data.Map.instHAppendOfDecidableLT {α : Type u_1} {β : Type u_2} [LT α] [DecidableLT α] : HAppend (Map α β) (Map α β) (Map α β)

Equations

• Cedar.Data.Map.instHAppendOfDecidableLT = { hAppend := fun (a b : Cedar.Data.Map α β) => Cedar.Data.Map.make (a.toList ++ b.toList) }