@[reducible, inline]

abbrev Maps (α : Type u) (β : Type v) : Type (max v u)

Equations

• Maps α β = List (Map α β)

@[implicit_reducible]

instance instInhabitedMaps {α : Type u_1} {β : Type u_2} : Inhabited (Maps α β)

Equations

• instInhabitedMaps = { default := [] }

def Maps.format' {α : Type u_1} {β : Type u_2} [Std.ToFormat (Map α β)] (ms : Maps α β) : Std.Format

Equations

• Maps.format' [] = Std.Format.text ""
• Maps.format' [m] = Std.format (Std.format "[" ++ Std.format m ++ Std.format "]")
• Maps.format' (m :: rest) = Std.format (Std.format "[" ++ Std.format m ++ Std.format "]" ++ Std.format Std.Format.line) ++ Maps.format' rest

@[implicit_reducible]

instance instToFormatMapsOfMap {α : Type u_1} {β : Type u_2} [Std.ToFormat (Map α β)] : Std.ToFormat (Maps α β)

Equations

• instToFormatMapsOfMap = { format := Maps.format' }

def Maps.keys {α : Type u_1} {β : Type u_2} (ms : Maps α β) : List α

Equations

• Maps.keys [] = []
• Maps.keys (m :: mrest) = m.keys ++ Maps.keys mrest

def Maps.values {α : Type u_1} {β : Type u_2} (ms : Maps α β) : List β

Equations

• Maps.values [] = []
• Maps.values (m :: mrest) = m.values ++ Maps.values mrest

def Maps.isEmpty {α : Type u_1} {β : Type u_2} (m : Maps α β) : Bool

Equations

• Maps.isEmpty [] = true
• m.isEmpty = false

def Maps.push {α : Type u_1} {β : Type u_2} (ms : Maps α β) (m : Map α β) : Maps α β

Add Map m to the beginning of Maps ms.

Equations

• ms.push m = m :: ms

def Maps.pop {α : Type u_1} {β : Type u_2} (ms : Maps α β) : Maps α β

Remove the newest Map in ms. Do nothing if ms is empty.

Equations

• Maps.pop [] = []
• Maps.pop (m :: mrest) = mrest

def Maps.oldest {α : Type u_1} {β : Type u_2} (ms : Maps α β) : Map α β

Get the oldest map (i.e., from the end) in ms.

Equations

• ms.oldest = List.getLastD ms []

def Maps.dropOldest {α : Type u_1} {β : Type u_2} (ms : Maps α β) : Maps α β

Drop the oldest map in ms.

Equations

• ms.dropOldest = List.dropLast ms

def Maps.newest {α : Type u_1} {β : Type u_2} (ms : Maps α β) : Map α β

Get the newest map (i.e., from the beginning) in ms.

Equations

• Maps.newest [] = []
• Maps.newest (m :: mrest) = m

def Maps.addInNewest {α : Type u_1} {β : Type u_2} (ms : Maps α β) (m : Map α β) : Maps α β

Append m to the end of the newest map in ms.

Equations

• ms.addInNewest m = ms.pop.push (ms.newest ++ m)

def Maps.toSingleMap {α : Type u_1} {β : Type u_2} (ms : Maps α β) : Map α β

Flatten the Maps ms to get a single map.

Searching for (x : α) after flattening will proceed from the newest to the oldest Map.

Equations

• ms.toSingleMap = List.flatten ms

def Maps.find? {α : Type u_1} {β : Type u_2} [DecidableEq α] (ms : Maps α β) (x : α) : Option β

Look up (x : α) in all the maps in ms.

Equations

• Maps.find? [] x = none
• Maps.find? (m :: rest) x = match m.find? x with | none => Maps.find? rest x | some v => some v

def Maps.findD {α : Type u_1} {β : Type u_2} [DecidableEq α] (ms : Maps α β) (x : α) (d : β) : β

Look up (x : α) in all the maps in ms, returning the default element d if x is not found.

Equations

• Maps.findD [] x d = d
• Maps.findD (m :: rest) x d = match m.find? x with | none => Maps.findD rest x d | some v => v

def Maps.remove {α : Type u_1} {β : Type u_2} [DecidableEq α] (ms : Maps α β) (x : α) : Maps α β

Remove x and its associated value from ms.

Equations

• Maps.remove [] x = []
• Maps.remove (m :: mrest) x = m.erase x :: Maps.remove mrest x

def Maps.update {α : Type u_1} {β : Type u_2} [DecidableEq α] (ms : Maps α β) (x : α) (v : β) : Maps α β

Update x with v in ms. Do nothing if x is not in ms.

Equations

• Maps.update [] x v = []
• Maps.update (m :: mrest) x v = match m.find? x with | none => m :: Maps.update mrest x v | some val => m.insert x v :: mrest

def Maps.insert {α : Type u_1} {β : Type u_2} [DecidableEq α] (ms : Maps α β) (x : α) (v : β) : Maps α β

Insert (x, v) in ms. If x is already in ms, update that entry. Else add it to the most recent map.

Equations

• ms.insert x v = match ms.find? x with | none => have m := ms.newest; have m' := m.insert x v; ms.pop.push m' | some val => ms.update x v

def Maps.insertInOldest {α : Type u_1} {β : Type u_2} [DecidableEq α] (ms : Maps α β) (x : α) (v : β) : Maps α β

Insert (x, v) in the oldest map in ms. Do nothing if x is already in ms.

Equations

• ms.insertInOldest x v = Maps.insertInOldest.go✝ x v [] ms

def Maps.addInOldest {α : Type u_1} {β : Type u_2} [DecidableEq α] (ms : Maps α β) (xs : List α) (vs : List β) : Maps α β

Insert (xi, vi) -- where xi and vi are corresponding elements of xs and vs -- in the oldest map in ms, only if xi is not in ms.

Equations

• ms.addInOldest [] vs = ms
• ms.addInOldest xs [] = ms
• ms.addInOldest (x :: xrest) (v :: vrest) = (ms.insertInOldest x v).addInOldest xrest vrest