-
Notifications
You must be signed in to change notification settings - Fork 98
/
PersistentHashSet.lean
98 lines (84 loc) · 2.43 KB
/
PersistentHashSet.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
/-
Copyright (c) 2022 Jannis Limperg. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jannis Limperg
-/
import Lean.Data.PersistentHashSet
namespace Lean.PersistentHashSet
variable [BEq α] [Hashable α]
instance : ForIn m (PersistentHashSet α) α where
forIn s init step := do
let mut state := init
for (k, _) in s.set do
match ← step k state with
| .done state' => return state'
| .yield state' => state := state'
return state
/--
Returns `true` if `f` returns `true` for any element of the set.
-/
@[specialize]
def anyM [Monad m] (s : PersistentHashSet α) (f : α → m Bool) : m Bool := do
for a in s do
if ← f a then
return true
return false
/--
Returns `true` if `f` returns `true` for any element of the set.
-/
@[inline]
def any (s : PersistentHashSet α) (f : α → Bool) : Bool :=
Id.run <| s.anyM f
/--
Returns `true` if `f` returns `true` for all elements of the set.
-/
@[specialize]
def allM [Monad m] (s : PersistentHashSet α) (f : α → m Bool) : m Bool := do
for a in s do
if ! (← f a) then
return false
return true
/--
Returns `true` if `f` returns `true` for all elements of the set.
-/
@[inline]
def all (s : PersistentHashSet α) (f : α → Bool) : Bool :=
Id.run <| s.allM f
instance : BEq (PersistentHashSet α) where
beq s t := s.all (t.contains ·) && t.all (s.contains ·)
/--
Similar to `insert`, but also returns a Boolean flag indicating whether an
existing entry has been replaced with `a ↦ b`.
-/
@[inline]
def insert' (s : PersistentHashSet α) (a : α) : PersistentHashSet α × Bool :=
let oldSize := s.size
let s := s.insert a
(s, s.size == oldSize)
/--
Insert all elements from a collection into a `PersistentHashSet`.
-/
def insertMany [ForIn Id ρ α] (s : PersistentHashSet α) (as : ρ) :
PersistentHashSet α := Id.run do
let mut s := s
for a in as do
s := s.insert a
return s
/--
Obtain a `PersistentHashSet` from an array.
-/
@[inline]
protected def ofArray [BEq α] [Hashable α] (as : Array α) : PersistentHashSet α :=
PersistentHashSet.empty.insertMany as
/--
Obtain a `PersistentHashSet` from a list.
-/
@[inline]
protected def ofList [BEq α] [Hashable α] (as : Array α) : PersistentHashSet α :=
PersistentHashSet.empty.insertMany as
/--
Merge two `PersistentHashSet`s.
-/
@[inline]
def merge (s t : PersistentHashSet α) : PersistentHashSet α :=
s.insertMany t