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
|
(.module:
lux
(lux (control [monad #+ do]
["ex" exception #+ exception:])
(data [ident]
[number]
[product]
[maybe]
(coll [list "list/" Functor<List>]
(dictionary ["dict" unordered #+ Dict]))
text/format)
[macro]
(macro [code]))
(//// [type]
(type ["tc" check]))
[///]
[// #+ Tag Analysis Operation Compiler]
[//type]
[//primitive]
[//inference])
(exception: #export (invalid-variant-type {type Type} {tag Tag} {code Code})
(ex.report ["Type" (%type type)]
["Tag" (%n tag)]
["Expression" (%code code)]))
(do-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))
(do-template [<name>]
[(exception: #export (<name> {type Type} {tag Tag} {code Code})
(ex.report ["Type" (%type type)]
["Tag" (%n 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))]))
(do-template [<name>]
[(exception: #export (<name> {key Ident} {record (List [Ident 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 Ident} {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 [Ident Code])})
(ex.report ["Expected" (|> expected .int %i)]
["Actual" (|> actual .int %i)]
["Type" (%type type)]
["Expression" (%code (|> record
(list/map (function (_ [keyI valueC])
[(code.tag keyI) valueC]))
code.record))]))
(def: #export (sum analyse tag valueC)
(-> Compiler Nat Code (Operation Analysis))
(do ///.Monad<Operation>
[expectedT macro.expected-type]
(///.with-stack cannot-analyse-variant [expectedT tag valueC]
(case expectedT
(#.Sum _)
(let [flat (type.flatten-variant expectedT)
type-size (list.size flat)]
(case (list.nth tag flat)
(#.Some variant-type)
(do @
[valueA (//type.with-type variant-type
(analyse valueC))]
(wrap (//.sum-analysis type-size tag 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
(tc.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 tc.existential]
[#.ExQ tc.var])
(#.Apply inputT funT)
(case funT
(#.Var funT-id)
(do @
[?funT' (//type.with-env (tc.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)
#.None
(///.throw not-a-quantified-type funT)
(#.Some outputT)
(//type.with-type outputT
(sum analyse tag valueC))))
_
(///.throw invalid-variant-type [expectedT tag valueC])))))
(def: (typed-product analyse membersC+)
(-> Compiler (List Code) (Operation Analysis))
(do ///.Monad<Operation>
[expectedT macro.expected-type]
(loop [expectedT expectedT
membersC+ membersC+]
(case [expectedT membersC+]
## If the tuple runs out, whatever expression is the last gets
## matched to the remaining type.
[tailT (#.Cons tailC #.Nil)]
(//type.with-type tailT
(analyse tailC))
## If the type and the code are still ongoing, match each
## sub-expression to its corresponding type.
[(#.Product leftT rightT) (#.Cons leftC rightC)]
(do @
[leftA (//type.with-type leftT
(analyse leftC))
rightA (recur rightT rightC)]
(wrap (#//.Structure (#//.Product leftA rightA))))
## If, however, the type runs out but there is still enough
## tail, the remaining elements get packaged into another
## tuple.
## The reason for this is that it is assumed that the type of
## the tuple represents the expectations of the user.
## If the type is for a 3-tuple, but a 5-tuple is provided, it
## is assumed that the user intended the following layout:
## [0, 1, [2, 3, 4]]
## but that, for whatever reason, it was written in a flat
## way.
[tailT tailC]
(|> tailC
code.tuple
analyse
(//type.with-type tailT)
(:: @ map (|>> //.no-op)))))))
(def: #export (product analyse membersC)
(-> Compiler (List Code) (Operation Analysis))
(do ///.Monad<Operation>
[expectedT 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
(tc.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
(tc.check expectedT
(type.tuple (list/map product.left membersTA))))]
(wrap (//.product-analysis (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 tc.existential]
[#.ExQ tc.var])
(#.Apply inputT funT)
(case funT
(#.Var funT-id)
(do @
[?funT' (//type.with-env (tc.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)
#.None
(///.throw not-a-quantified-type funT)
(#.Some outputT)
(//type.with-type outputT
(product analyse membersC))))
_
(///.throw invalid-tuple-type [expectedT membersC])
))))
(def: #export (tagged-sum analyse tag valueC)
(-> Compiler Ident Code (Operation Analysis))
(do ///.Monad<Operation>
[tag (macro.normalize tag)
[idx group variantT] (macro.resolve-tag tag)
expectedT 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))]
(wrap (//.sum-analysis case-size idx (|> 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 [Ident Code])))
(monad.map ///.Monad<Operation>
(function (_ [key val])
(case key
[_ (#.Tag key)]
(do ///.Monad<Operation>
[key (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 [Ident Code]) (Operation [(List Code) Type]))
(case record
## empty-record = empty-tuple = unit = []
#.Nil
(:: ///.Monad<Operation> wrap [(list) Any])
(#.Cons [head-k head-v] _)
(do ///.Monad<Operation>
[head-k (macro.normalize head-k)
[_ tag-set recordT] (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.n/range +0 (dec size-ts))
tag->idx (dict.from-list ident.Hash<Ident> (list.zip2 tag-set tuple-range))]
idx->val (monad.fold @
(function (_ [key val] idx->val)
(do @
[key (macro.normalize key)]
(case (dict.get key tag->idx)
#.None
(///.throw tag-does-not-belong-to-record [key recordT])
(#.Some idx)
(if (dict.contains? idx idx->val)
(///.throw cannot-repeat-tag [key record])
(wrap (dict.put idx val idx->val))))))
(: (Dict Nat Code)
(dict.new number.Hash<Nat>))
record)
#let [ordered-tuple (list/map (function (_ idx) (maybe.assume (dict.get idx idx->val)))
tuple-range)]]
(wrap [ordered-tuple recordT]))
))
(def: #export (record analyse members)
(-> Compiler (List [Code Code]) (Operation Analysis))
(do ///.Monad<Operation>
[members (normalize members)
[membersC recordT] (order members)]
(case membersC
(^ (list))
//primitive.unit
(^ (list singletonC))
(analyse singletonC)
_
(do @
[expectedT macro.expected-type]
(case expectedT
(#.Var _)
(do @
[inferenceT (//inference.record recordT)
[inferredT membersA] (//inference.general analyse inferenceT membersC)]
(wrap (//.product-analysis membersA)))
_
(..product analyse membersC))))))
|