blob: 49447e847087bfbf501545f7a366ab01795bebc0 (
plain)
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
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
|
(.module:
[lux #*
[abstract
["." monad (#+ do)]]
[control
["ex" exception (#+ exception:)]
["." state]]
[data
["." name]
["." product]
["." maybe]
[number
["n" nat]]
[text
["%" format (#+ format)]]
[collection
["." list ("#@." functor)]
["." dictionary (#+ Dictionary)]]]
["." type
["." check]]
["." macro
["." code]]]
["." // #_
["#." type]
["#." primitive]
["#." inference]
["#/" //
["#." extension]
[//
["/" analysis (#+ Tag Analysis Operation Phase)]]]])
(exception: #export (invalid-variant-type {type Type} {tag Tag} {code Code})
(ex.report ["Type" (%.type type)]
["Tag" (%.nat tag)]
["Expression" (%.code code)]))
(template [<name>]
[(exception: #export (<name> {type Type} {members (List Code)})
(ex.report ["Type" (%.type type)]
["Expression" (%.code (` [(~+ members)]))]))]
[invalid-tuple-type]
[cannot-analyse-tuple]
)
(exception: #export (not-a-quantified-type {type Type})
(%.type type))
(template [<name>]
[(exception: #export (<name> {type Type} {tag Tag} {code Code})
(ex.report ["Type" (%.type type)]
["Tag" (%.nat tag)]
["Expression" (%.code code)]))]
[cannot-analyse-variant]
[cannot-infer-numeric-tag]
)
(exception: #export (record-keys-must-be-tags {key Code} {record (List [Code Code])})
(ex.report ["Key" (%.code key)]
["Record" (%.code (code.record record))]))
(template [<name>]
[(exception: #export (<name> {key Name} {record (List [Name Code])})
(ex.report ["Tag" (%.code (code.tag key))]
["Record" (%.code (code.record (list@map (function (_ [keyI valC])
[(code.tag keyI) valC])
record)))]))]
[cannot-repeat-tag]
)
(exception: #export (tag-does-not-belong-to-record {key Name} {type Type})
(ex.report ["Tag" (%.code (code.tag key))]
["Type" (%.type type)]))
(exception: #export (record-size-mismatch {expected Nat} {actual Nat} {type Type} {record (List [Name Code])})
(ex.report ["Expected" (%.nat expected)]
["Actual" (%.nat actual)]
["Type" (%.type type)]
["Expression" (%.code (|> record
(list@map (function (_ [keyI valueC])
[(code.tag keyI) valueC]))
code.record))]))
(def: #export (sum analyse tag valueC)
(-> Phase Nat Code (Operation Analysis))
(do ///.monad
[expectedT (///extension.lift macro.expected-type)
expectedT' (//type.with-env
(check.clean expectedT))]
(/.with-stack cannot-analyse-variant [expectedT' tag valueC]
(case expectedT
(#.Sum _)
(let [flat (type.flatten-variant expectedT)
type-size (list.size flat)
right? (n.= (dec type-size)
tag)
lefts (if right?
(dec tag)
tag)]
(case (list.nth tag flat)
(#.Some variant-type)
(do @
[valueA (//type.with-type variant-type
(analyse valueC))]
(wrap (/.variant [lefts right? valueA])))
#.None
(/.throw //inference.variant-tag-out-of-bounds [type-size tag expectedT])))
(#.Named name unnamedT)
(//type.with-type unnamedT
(sum analyse tag valueC))
(#.Var id)
(do @
[?expectedT' (//type.with-env
(check.read id))]
(case ?expectedT'
(#.Some expectedT')
(//type.with-type expectedT'
(sum analyse tag valueC))
_
## Cannot do inference when the tag is numeric.
## This is because there is no way of knowing how many
## cases the inferred sum type would have.
(/.throw cannot-infer-numeric-tag [expectedT tag valueC])
))
(^template [<tag> <instancer>]
(<tag> _)
(do @
[[instance-id instanceT] (//type.with-env <instancer>)]
(//type.with-type (maybe.assume (type.apply (list instanceT) expectedT))
(sum analyse tag valueC))))
([#.UnivQ check.existential]
[#.ExQ check.var])
(#.Apply inputT funT)
(case funT
(#.Var funT-id)
(do @
[?funT' (//type.with-env (check.read funT-id))]
(case ?funT'
(#.Some funT')
(//type.with-type (#.Apply inputT funT')
(sum analyse tag valueC))
_
(/.throw invalid-variant-type [expectedT tag valueC])))
_
(case (type.apply (list inputT) funT)
(#.Some outputT)
(//type.with-type outputT
(sum analyse tag valueC))
#.None
(/.throw not-a-quantified-type funT)))
_
(/.throw invalid-variant-type [expectedT tag valueC])))))
(def: (typed-product analyse members)
(-> Phase (List Code) (Operation Analysis))
(do ///.monad
[expectedT (///extension.lift macro.expected-type)
membersA+ (: (Operation (List Analysis))
(loop [membersT+ (type.flatten-tuple expectedT)
membersC+ members]
(case [membersT+ membersC+]
[(#.Cons memberT #.Nil) _]
(//type.with-type memberT
(:: @ map (|>> list) (analyse (code.tuple membersC+))))
[_ (#.Cons memberC #.Nil)]
(//type.with-type (type.tuple membersT+)
(:: @ map (|>> list) (analyse memberC)))
[(#.Cons memberT membersT+') (#.Cons memberC membersC+')]
(do @
[memberA (//type.with-type memberT
(analyse memberC))
memberA+ (recur membersT+' membersC+')]
(wrap (#.Cons memberA memberA+)))
_
(/.throw cannot-analyse-tuple [expectedT members]))))]
(wrap (/.tuple membersA+))))
(def: #export (product analyse membersC)
(-> Phase (List Code) (Operation Analysis))
(do ///.monad
[expectedT (///extension.lift macro.expected-type)]
(/.with-stack cannot-analyse-tuple [expectedT membersC]
(case expectedT
(#.Product _)
(..typed-product analyse membersC)
(#.Named name unnamedT)
(//type.with-type unnamedT
(product analyse membersC))
(#.Var id)
(do @
[?expectedT' (//type.with-env
(check.read id))]
(case ?expectedT'
(#.Some expectedT')
(//type.with-type expectedT'
(product analyse membersC))
_
## Must do inference...
(do @
[membersTA (monad.map @ (|>> analyse //type.with-inference)
membersC)
_ (//type.with-env
(check.check expectedT
(type.tuple (list@map product.left membersTA))))]
(wrap (/.tuple (list@map product.right membersTA))))))
(^template [<tag> <instancer>]
(<tag> _)
(do @
[[instance-id instanceT] (//type.with-env <instancer>)]
(//type.with-type (maybe.assume (type.apply (list instanceT) expectedT))
(product analyse membersC))))
([#.UnivQ check.existential]
[#.ExQ check.var])
(#.Apply inputT funT)
(case funT
(#.Var funT-id)
(do @
[?funT' (//type.with-env (check.read funT-id))]
(case ?funT'
(#.Some funT')
(//type.with-type (#.Apply inputT funT')
(product analyse membersC))
_
(/.throw invalid-tuple-type [expectedT membersC])))
_
(case (type.apply (list inputT) funT)
(#.Some outputT)
(//type.with-type outputT
(product analyse membersC))
#.None
(/.throw not-a-quantified-type funT)))
_
(/.throw invalid-tuple-type [expectedT membersC])
))))
(def: #export (tagged-sum analyse tag valueC)
(-> Phase Name Code (Operation Analysis))
(do ///.monad
[tag (///extension.lift (macro.normalize tag))
[idx group variantT] (///extension.lift (macro.resolve-tag tag))
expectedT (///extension.lift macro.expected-type)]
(case expectedT
(#.Var _)
(do @
[#let [case-size (list.size group)]
inferenceT (//inference.variant idx case-size variantT)
[inferredT valueA+] (//inference.general analyse inferenceT (list valueC))
#let [right? (n.= (dec case-size) idx)
lefts (if right?
(dec idx)
idx)]]
(wrap (/.variant [lefts right? (|> valueA+ list.head maybe.assume)])))
_
(..sum analyse idx valueC))))
## There cannot be any ambiguity or improper syntax when analysing
## records, so they must be normalized for further analysis.
## Normalization just means that all the tags get resolved to their
## canonical form (with their corresponding module identified).
(def: #export (normalize record)
(-> (List [Code Code]) (Operation (List [Name Code])))
(monad.map ///.monad
(function (_ [key val])
(case key
[_ (#.Tag key)]
(do ///.monad
[key (///extension.lift (macro.normalize key))]
(wrap [key val]))
_
(/.throw record-keys-must-be-tags [key record])))
record))
## Lux already possesses the means to analyse tuples, so
## re-implementing the same functionality for records makes no sense.
## Records, thus, get transformed into tuples by ordering the elements.
(def: #export (order record)
(-> (List [Name Code]) (Operation [(List Code) Type]))
(case record
## empty-record = empty-tuple = unit = []
#.Nil
(:: ///.monad wrap [(list) Any])
(#.Cons [head-k head-v] _)
(do ///.monad
[head-k (///extension.lift (macro.normalize head-k))
[_ tag-set recordT] (///extension.lift (macro.resolve-tag head-k))
#let [size-record (list.size record)
size-ts (list.size tag-set)]
_ (if (n.= size-ts size-record)
(wrap [])
(/.throw record-size-mismatch [size-ts size-record recordT record]))
#let [tuple-range (list.indices size-ts)
tag->idx (dictionary.from-list name.hash (list.zip2 tag-set tuple-range))]
idx->val (monad.fold @
(function (_ [key val] idx->val)
(do @
[key (///extension.lift (macro.normalize key))]
(case (dictionary.get key tag->idx)
(#.Some idx)
(if (dictionary.contains? idx idx->val)
(/.throw cannot-repeat-tag [key record])
(wrap (dictionary.put idx val idx->val)))
#.None
(/.throw tag-does-not-belong-to-record [key recordT]))))
(: (Dictionary Nat Code)
(dictionary.new n.hash))
record)
#let [ordered-tuple (list@map (function (_ idx) (maybe.assume (dictionary.get idx idx->val)))
tuple-range)]]
(wrap [ordered-tuple recordT]))
))
(def: #export (record analyse members)
(-> Phase (List [Code Code]) (Operation Analysis))
(case members
(^ (list))
//primitive.unit
(^ (list [_ singletonC]))
(analyse singletonC)
_
(do ///.monad
[members (normalize members)
[membersC recordT] (order members)
expectedT (///extension.lift macro.expected-type)]
(case expectedT
(#.Var _)
(do @
[inferenceT (//inference.record recordT)
[inferredT membersA] (//inference.general analyse inferenceT membersC)]
(wrap (/.tuple membersA)))
_
(..product analyse membersC)))))
|