-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathClient.lean
170 lines (135 loc) · 4.38 KB
/
Client.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
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
import SafeIdx
namespace SafeIdx.Tests.Client
/-- Client indices. -/
index Client.Idx where
UidMap => Clients
UidMapD => ClientsD
export Client.Idx (FUid)
structure Client where
name : String
email : String
idx : Client.Idx
deriving Inhabited, Repr
instance : ToString Client where
toString self :=
s!"{self.name} <{self.email}> {self.idx}"
def Client.mk'
(name email : String)
(idx : Client.Idx.FUid n)
: Client :=
⟨name, email, idx⟩
def run : IO Unit := do
println! "building `DMap`, accessing with indices from `DMap.pushIdx`"
-- vvvvvvv~~~~ `Client.Idx.DArray 0 Client`
let clients := ClientsD.mkEmpty 17
-- vvvvvvv~~~~ `Client.Idx.DArray 1 Client`
let (cat, clients) :=
Client.mk' "cat" "[email protected]"
|> clients.pushIdx
-- vvvvvvv~~~~ `Client.Idx.DArray 2 Client`
let (dog, clients) :=
Client.mk' "dog" "[email protected]"
|> clients.pushIdx
-- vvvvvvv~~~~ `Client.Idx.DArray 3 Client`
let (jef, clients) :=
Client.mk' "jef" "[email protected]"
|> clients.pushIdx
-- `GetElem` notation (`array[idx]`) requires a proof that the index is in-bound, which here is
-- inferred automatically thanks to various lemmas behind the scene
println! " jef : {clients[jef]}"
println! " cat : {clients[cat]}"
println! " dog : {clients[dog]}"
println! "\nfor-loop on `clients`"
for client in clients do
println! "- {client}"
println! "\nfor-loop on `clients.iterIdx`"
for (idx, client) in clients.iterIdx do
println! "- {idx} ↦ {client}"
println! "\nfor-loop on `clients.indices`"
for idx in clients.indices do
println! "- idx : {idx}"
println! "\nfolding"
let s := clients.foldlIdx
(fun s uid client =>
let sep := if s.isEmpty then "" else ", "
s ++ sep ++ s!"{client} ({uid})")
""
println! "- foldl : {s}"
let s := clients.foldrIdx
(fun uid client s =>
let sep := if s.isEmpty then "" else ", "
s ++ sep ++ s!"{client} ({uid})")
""
println! "- foldr : {s}"
println! "\n\nswitching to `Map`, accessing with indices from `DMap`:"
-- vvvvvvvv~~~~ `Client.Idx.Array Client`, length has been erased from the type
let clients' :=
clients.toMap
-- proof that indices are in-bound also inferred thanks to various lemmas again
println! " jef : {clients'[jef]}"
println! " cat : {clients'[cat]}"
println! " dog : {clients'[dog]}"
println! "\nfolding"
let s := clients'.foldlIdx
(fun s uid client =>
let sep := if s.isEmpty then "" else ", "
s ++ sep ++ s!"{client} ({uid})")
""
println! "- foldl : {s}"
let s := clients'.foldrIdx
(fun uid client s =>
let sep := if s.isEmpty then "" else ", "
s ++ sep ++ s!"{client} ({uid})")
""
println! "- foldr : {s}"
println! "\nfor-loop on `clients'`"
for client in clients' do
println! "- {client}"
println! "\nfor-loop on `clients'.iterIdx`"
for (idx, client) in clients'.iterIdx do
println! "- {idx} ↦ {client}"
println! "\nfor-loop on `clients'.indices`"
for idx in clients'.indices do
println! "- idx : {idx}"
/-- info:
building `DMap`, accessing with indices from `DMap.pushIdx`
jef : jef <[email protected]> #2
cat : cat <[email protected]> #0
dog : dog <[email protected]> #1
for-loop on `clients`
- cat <[email protected]> #0
- dog <[email protected]> #1
- jef <[email protected]> #2
for-loop on `clients.iterIdx`
- #0<3 ↦ cat <[email protected]> #0
- #1<3 ↦ dog <[email protected]> #1
- #2<3 ↦ jef <[email protected]> #2
for-loop on `clients.indices`
- idx : #0<3
- idx : #1<3
- idx : #2<3
folding
- foldl : cat <[email protected]> #0 (#0<3), dog <[email protected]> #1 (#1<3), jef <[email protected]> #2 (#2<3)
- foldr : jef <[email protected]> #2 (#2<3), dog <[email protected]> #1 (#1<3), cat <[email protected]> #0 (#0<3)
switching to `Map`, accessing with indices from `DMap`:
jef : jef <[email protected]> #2
cat : cat <[email protected]> #0
dog : dog <[email protected]> #1
folding
- foldl : cat <[email protected]> #0 (#0<3), dog <[email protected]> #1 (#1<3), jef <[email protected]> #2 (#2<3)
- foldr : jef <[email protected]> #2 (#2<3), dog <[email protected]> #1 (#1<3), cat <[email protected]> #0 (#0<3)
for-loop on `clients'`
- cat <[email protected]> #0
- dog <[email protected]> #1
- jef <[email protected]> #2
for-loop on `clients'.iterIdx`
- #0<3 ↦ cat <[email protected]> #0
- #1<3 ↦ dog <[email protected]> #1
- #2<3 ↦ jef <[email protected]> #2
for-loop on `clients'.indices`
- idx : #0<3
- idx : #1<3
- idx : #2<3
-/
#guard_msgs in
#eval run