/-
Copyright (c) 2022 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison
-/
import Std.Data.HashMap
import Std.Data.RBMap

/-!
# Additional API for `RBMap`.

These should be replaced by proper implementations in Std.
-/

namespace Std.HashMap

variable [
BEq: Type ?u.189 → Type ?u.189
BEq 
α: ?m.4
α] [
Hashable: Sort ?u.21 → Sort (max1?u.21)
Hashable 
α: ?m.4
α]

/-- The list of keys in a `HashMap`. -/
def 
keys: {β : Type ?u.30} → HashMap α β → List α
keys (
m: HashMap α β
m : 
HashMap: (α : Type ?u.31) → Type ?u.30 → [inst : BEq α] → [inst : Hashable α] → Type (max0?u.31?u.30)
HashMap 
α: ?m.15
α 
β: ?m.27
β) : 
List: Type ?u.42 → Type ?u.42
List 
α: ?m.15
α :=
m: HashMap α β
m.
fold: {α : Type ?u.48} →
  {x : BEq α} → {x_1 : Hashable α} → {δ : Type ?u.47} → {β : Type ?u.46} → (δ → α → β → δ) → δ → HashMap α β → δ
fold (fun 
ks: ?m.63
ks 
k: ?m.66
k 
_: ?m.69
_ => 
k: ?m.66
k :: 
ks: ?m.63
ks) 
[]: List ?m.81
[]

/-- The list of values in a `HashMap`. -/
def 
values: {β : Type ?u.201} → HashMap α β → List β
values (
m: HashMap α β
m : 
HashMap: (α : Type ?u.202) → Type ?u.201 → [inst : BEq α] → [inst : Hashable α] → Type (max0?u.202?u.201)
HashMap 
α: ?m.186
α 
β: ?m.198
β) : 
List: Type ?u.213 → Type ?u.213
List 
β: ?m.198
β :=
m: HashMap α β
m.
fold: {α : Type ?u.219} →
  {x : BEq α} → {x_1 : Hashable α} → {δ : Type ?u.218} → {β : Type ?u.217} → (δ → α → β → δ) → δ → HashMap α β → δ
fold (fun 
vs: ?m.234
vs 
_: ?m.237
_ 
v: ?m.240
v => 
v: ?m.240
v :: 
vs: ?m.234
vs) 
[]: List ?m.252
[]

/-- Add a value to a `HashMap α (List β)` viewed as a multimap. -/
def 
consVal: {β : Type ?u.364} → HashMap α (List β) → α → β → HashMap α (List β)
consVal (
self: HashMap α (List β)
self : 
HashMap: (α : Type ?u.363) → Type ?u.362 → [inst : BEq α] → [inst : Hashable α] → Type (max0?u.363?u.362)
HashMap 
α: ?m.346
α (
List: Type ?u.364 → Type ?u.364
List 
β: ?m.359
β)) (
a: α
a : 
α: ?m.346
α) (
b: β
b : 
β: ?m.359
β) : 
HashMap: (α : Type ?u.380) → Type ?u.379 → [inst : BEq α] → [inst : Hashable α] → Type (max0?u.380?u.379)
HashMap 
α: ?m.346
α (
List: Type ?u.381 → Type ?u.381
List 
β: ?m.359
β) :=
match 
self: HashMap α (List β)
self.
find?: {α : Type ?u.394} → {x : BEq α} → {x_1 : Hashable α} → {β : Type ?u.393} → HashMap α β → α → Option β
find? 
a: α
a with
| 
none: {α : Type ?u.411} → Option α
none => 
self: HashMap α (List β)
self.
insert: {α : Type ?u.422} → {x : BEq α} → {x_1 : Hashable α} → {β : Type ?u.421} → HashMap α β → α → β → HashMap α β
insert 
a: α
a [
b: β
b]
| 
some: {α : Type ?u.439} → α → Option α
some 
L: List β
L => 
self: HashMap α (List β)
self.
insert: {α : Type ?u.454} → {x : BEq α} → {x_1 : Hashable α} → {β : Type ?u.453} → HashMap α β → α → β → HashMap α β
insert 
a: α
a (
b: β
b::
L: List β
L)

end Std.HashMap

namespace Std.RBSet

/-- Insert all elements of a list into an `RBSet`. -/
def 
insertList: {α : Type ?u.683} → {cmp : α → α → Ordering} → RBSet α cmp → List α → RBSet α cmp
insertList (
m: RBSet α cmp
m : 
RBSet: (α : Type ?u.683) → (α → α → Ordering) → Type ?u.683
RBSet 
α: ?m.675
α 
cmp: ?m.680
cmp) (
L: List α
L : 
List: Type ?u.688 → Type ?u.688
List 
α: ?m.675
α) : 
RBSet: (α : Type ?u.691) → (α → α → Ordering) → Type ?u.691
RBSet 
α: ?m.675
α 
cmp: ?m.680
cmp :=
L: List α
L.
foldl: {α : Type ?u.704} → {β : Type ?u.703} → (α → β → α) → α → List β → α
foldl (fun 
m: ?m.713
m 
a: ?m.716
a => 
m: ?m.713
m.
insert: {α : Type ?u.718} → {cmp : α → α → Ordering} → RBSet α cmp → α → RBSet α cmp
insert 
a: ?m.716
a) 
m: RBSet α cmp
m

end Std.RBSet