-
Notifications
You must be signed in to change notification settings - Fork 26
/
UnorderedArraySet.lean
145 lines (108 loc) · 3.93 KB
/
UnorderedArraySet.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
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
/-
Copyright (c) 2021 Jannis Limperg. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jannis Limperg
-/
import Std.Data.Array.Basic
import Std.Data.Array.Merge
open Lean
namespace Aesop
structure UnorderedArraySet (α) [BEq α] where
private mk ::
private rep : Array α
deriving Inhabited
namespace UnorderedArraySet
variable [BEq α]
/-- O(1) -/
protected def empty : UnorderedArraySet α :=
⟨#[]⟩
instance : EmptyCollection (UnorderedArraySet α) :=
⟨UnorderedArraySet.empty⟩
/-- O(1) -/
protected def singleton (a : α) : UnorderedArraySet α :=
⟨#[a]⟩
/-- O(n) -/
def insert (x : α) : UnorderedArraySet α → UnorderedArraySet α
| ⟨rep⟩ => if rep.contains x then ⟨rep⟩ else ⟨rep.push x⟩
/-- Precondition: `xs` contains no duplicates. -/
protected def ofDeduplicatedArray (xs : Array α) : UnorderedArraySet α :=
⟨xs⟩
/-- Precondition: `xs` is sorted. -/
protected def ofSortedArray (xs : Array α) : UnorderedArraySet α :=
⟨xs.deduplicateSorted⟩
set_option linter.unusedVariables false in
/-- O(n*log(n)) -/
protected def ofArray [ord : Ord α] [Inhabited α] (xs : Array α) :
UnorderedArraySet α :=
⟨xs.sortAndDeduplicate⟩
/-- O(n^2) -/
protected def ofArraySlow (xs : Array α) : UnorderedArraySet α :=
xs.foldl (init := {}) λ s x => s.insert x
protected def ofHashSet [Hashable α] (xs : HashSet α) : UnorderedArraySet α :=
⟨xs.toArray⟩
protected def ofPersistentHashSet [Hashable α] (xs : PersistentHashSet α) : UnorderedArraySet α :=
⟨xs.fold (init := Array.mkEmpty xs.size) λ as a => as.push a⟩
protected def toArray (s : UnorderedArraySet α) : Array α :=
s.rep
/-- O(n) -/
def erase (x : α) (s : UnorderedArraySet α) : UnorderedArraySet α :=
⟨s.rep.erase x⟩
/-- O(n) -/
def filterM [Monad m] (p : α → m Bool) (s : UnorderedArraySet α) :
m (UnorderedArraySet α) :=
return ⟨← s.rep.filterM p⟩
/-- O(n) -/
def filter (p : α → Bool) (s : UnorderedArraySet α) : UnorderedArraySet α :=
⟨s.rep.filter p⟩
/-- O(n*m) -/
def merge (s t : UnorderedArraySet α) : UnorderedArraySet α :=
⟨s.rep.mergeUnsortedDeduplicating t.rep⟩
instance : Append (UnorderedArraySet α) :=
⟨merge⟩
/-- O(n) -/
def contains (x : α) (s : UnorderedArraySet α) : Bool :=
s.rep.contains x
/-- O(n) -/
def foldM [Monad m] (f : σ → α → m σ) (init : σ) (s : UnorderedArraySet α) :
m σ :=
s.rep.foldlM f init
instance [Monad m] : ForIn m (UnorderedArraySet α) α where
forIn s := s.rep.forIn
/-- O(n) -/
def fold (f : σ → α → σ) (init : σ) (s : UnorderedArraySet α) : σ :=
s.rep.foldl f init
def partition (f : α → Bool) (s : UnorderedArraySet α) :
(UnorderedArraySet α × UnorderedArraySet α) :=
let (xs, ys) := s.rep.partition f
(⟨xs⟩, ⟨ys⟩)
/-- O(1) -/
def size (s : UnorderedArraySet α) : Nat :=
s.rep.size
/-- O(1) -/
def isEmpty (s : UnorderedArraySet α) : Bool :=
s.rep.isEmpty
/-- O(n) -/
def anyM [Monad m] (p : α → m Bool) (s : UnorderedArraySet α) (start := 0)
(stop := s.size) : m Bool :=
s.rep.anyM p start stop
/-- O(n) -/
def any (p : α → Bool) (s : UnorderedArraySet α) (start := 0) (stop := s.size) :
Bool :=
s.rep.any p start stop
/-- O(n) -/
def allM [Monad m] (p : α → m Bool) (s : UnorderedArraySet α) (start := 0)
(stop := s.size) : m Bool :=
s.rep.allM p start stop
/-- O(n) -/
def all (p : α → Bool) (s : UnorderedArraySet α) (start := 0) (stop := s.size) :
Bool :=
s.rep.all p start stop
instance : BEq (UnorderedArraySet α) where
beq s t := s.rep.equalSet t.rep
instance [ToString α] : ToString (UnorderedArraySet α) where
toString s := toString s.rep
instance [ToFormat α] : ToFormat (UnorderedArraySet α) where
format s := format s.rep
instance [ToMessageData α] : ToMessageData (UnorderedArraySet α) where
toMessageData s := toMessageData s.rep
end Aesop.UnorderedArraySet