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
|
(.module:
lux
(lux (control [monad #+ do]
["ex" exception #+ exception:])
(data [ident]
[number]
[product]
[maybe]
(coll [list "list/" Functor<List>]
[dict #+ Dict])
text/format)
[macro]
(macro [code])
(lang [type]
(type ["tc" check])))
(luxc ["&" lang]
(lang ["&." scope]
["&." module]
["la" analysis]
(analysis ["&." common]
[".A" primitive]
["&." inference]))))
(exception: #export Invalid-Variant-Type)
(exception: #export Invalid-Tuple-Type)
(exception: #export Not-Quantified-Type)
(exception: #export Cannot-Analyse-Variant)
(exception: #export Cannot-Analyse-Tuple)
(exception: #export Cannot-Infer-Numeric-Tag)
(exception: #export Record-Keys-Must-Be-Tags)
(exception: #export Cannot-Repeat-Tag)
(exception: #export Tag-Does-Not-Belong-To-Record)
(exception: #export Record-Size-Mismatch)
(def: #export (analyse-sum analyse tag valueC)
(-> &.Analyser Nat Code (Meta la.Analysis))
(do macro.Monad<Meta>
[expectedT macro.expected-type]
(&.with-stacked-errors
(function [_] (Cannot-Analyse-Variant (format " Type: " (%type expectedT) "\n"
" Tag: " (%n tag) "\n"
"Expression: " (%code 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 (&.with-type variant-type
(analyse valueC))
temp &scope.next-local]
(wrap (la.sum tag type-size temp valueA)))
#.None
(&common.variant-out-of-bounds-error expectedT type-size tag)))
(#.Named name unnamedT)
(&.with-type unnamedT
(analyse-sum analyse tag valueC))
(#.Var id)
(do @
[?expectedT' (&.with-type-env
(tc.read id))]
(case ?expectedT'
(#.Some expectedT')
(&.with-type expectedT'
(analyse-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 (format " Type: " (%type expectedT) "\n"
" Tag: " (%n tag) "\n"
"Expression: " (%code valueC)))
))
(^template [<tag> <instancer>]
(<tag> _)
(do @
[[instance-id instanceT] (&.with-type-env <instancer>)]
(&.with-type (maybe.assume (type.apply (list instanceT) expectedT))
(analyse-sum analyse tag valueC))))
([#.UnivQ tc.existential]
[#.ExQ tc.var])
(#.Apply inputT funT)
(case funT
(#.Var funT-id)
(do @
[?funT' (&.with-type-env (tc.read funT-id))]
(case ?funT'
(#.Some funT')
(&.with-type (#.Apply inputT funT')
(analyse-sum analyse tag valueC))
_
(&.throw Invalid-Variant-Type (format " Type: " (%type expectedT) "\n"
" Tag: " (%n tag) "\n"
"Expression: " (%code valueC)))))
_
(case (type.apply (list inputT) funT)
#.None
(&.throw Not-Quantified-Type (%type funT))
(#.Some outputT)
(&.with-type outputT
(analyse-sum analyse tag valueC))))
_
(&.throw Invalid-Variant-Type (format " Type: " (%type expectedT) "\n"
" Tag: " (%n tag) "\n"
"Expression: " (%code valueC)))))))
(def: (analyse-typed-product analyse membersC+)
(-> &.Analyser (List Code) (Meta la.Analysis))
(do macro.Monad<Meta>
[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)]
(&.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 (&.with-type leftT
(analyse leftC))
rightA (recur rightT rightC)]
(wrap (` [(~ leftA) (~ rightA)])))
## If, however, the type runs out but there is still enough
## tail, the remaining elements get packaged into another
## tuple, and analysed through the intermediation of a
## temporary local variable.
## 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.
## The reason why an intermediate variable is used is that if
## the code was just re-written with just tuple nesting, the
## resulting analysis would have undone the explicity nesting,
## since Product nodes rely on nesting inherently, thereby
## blurring the line between what was wanted (the separation)
## and what was analysed.
[tailT tailC]
(macro.with-gensyms [g!tail]
(&.with-type tailT
(analyse (` ("lux case" [(~+ tailC)]
(~ g!tail)
(~ g!tail))))))
))))
(def: #export (analyse-product analyse membersC)
(-> &.Analyser (List Code) (Meta la.Analysis))
(do macro.Monad<Meta>
[expectedT macro.expected-type]
(&.with-stacked-errors
(function [_] (Cannot-Analyse-Tuple (format " Type: " (%type expectedT) "\n"
"Expression: " (%code (` [(~+ membersC)])))))
(case expectedT
(#.Product _)
(analyse-typed-product analyse membersC)
(#.Named name unnamedT)
(&.with-type unnamedT
(analyse-product analyse membersC))
(#.Var id)
(do @
[?expectedT' (&.with-type-env
(tc.read id))]
(case ?expectedT'
(#.Some expectedT')
(&.with-type expectedT'
(analyse-product analyse membersC))
_
## Must do inference...
(do @
[membersTA (monad.map @ (|>> analyse &common.with-unknown-type)
membersC)
_ (&.with-type-env
(tc.check expectedT
(type.tuple (list/map product.left membersTA))))]
(wrap (la.product (list/map product.right membersTA))))))
(^template [<tag> <instancer>]
(<tag> _)
(do @
[[instance-id instanceT] (&.with-type-env <instancer>)]
(&.with-type (maybe.assume (type.apply (list instanceT) expectedT))
(analyse-product analyse membersC))))
([#.UnivQ tc.existential]
[#.ExQ tc.var])
(#.Apply inputT funT)
(case funT
(#.Var funT-id)
(do @
[?funT' (&.with-type-env (tc.read funT-id))]
(case ?funT'
(#.Some funT')
(&.with-type (#.Apply inputT funT')
(analyse-product analyse membersC))
_
(&.throw Invalid-Tuple-Type (format " Type: " (%type expectedT) "\n"
"Expression: " (%code (` [(~+ membersC)]))))))
_
(case (type.apply (list inputT) funT)
#.None
(&.throw Not-Quantified-Type (%type funT))
(#.Some outputT)
(&.with-type outputT
(analyse-product analyse membersC))))
_
(&.throw Invalid-Tuple-Type (format " Type: " (%type expectedT) "\n"
"Expression: " (%code (` [(~+ membersC)]))))
))))
(def: #export (analyse-tagged-sum analyse tag valueC)
(-> &.Analyser Ident Code (Meta la.Analysis))
(do macro.Monad<Meta>
[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))
temp &scope.next-local]
(wrap (la.sum idx case-size temp (|> valueA+ list.head maybe.assume))))
_
(analyse-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]) (Meta (List [Ident Code])))
(monad.map macro.Monad<Meta>
(function [[key val]]
(case key
[_ (#.Tag key)]
(do macro.Monad<Meta>
[key (macro.normalize key)]
(wrap [key val]))
_
(&.throw Record-Keys-Must-Be-Tags (format " Key: " (%code key) "\n"
"Record: " (%code (code.record 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]) (Meta [(List Code) Type]))
(case record
## empty-record = empty-tuple = unit = []
#.Nil
(:: macro.Monad<Meta> wrap [(list) Unit])
(#.Cons [head-k head-v] _)
(do macro.Monad<Meta>
[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
(format " Expected: " (|> size-ts nat-to-int %i) "\n"
" Actual: " (|> size-record nat-to-int %i) "\n"
" Type: " (%type recordT) "\n"
"Expression: " (%code (|> record
(list/map (function [[keyI valueC]]
[(code.tag keyI) valueC]))
code.record)))))
#let [tuple-range (list.n/range +0 (n/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
(format " Tag: " (%code (code.tag key)) "\n"
"Type: " (%type recordT)))
(#.Some idx)
(if (dict.contains? idx idx->val)
(&.throw Cannot-Repeat-Tag
(format " Tag: " (%code (code.tag key)) "\n"
"Record: " (%code (code.record (list/map (function [[keyI valC]]
[(code.tag keyI) valC])
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 (analyse-record analyse members)
(-> &.Analyser (List [Code Code]) (Meta la.Analysis))
(do macro.Monad<Meta>
[members (normalize members)
[membersC recordT] (order members)]
(case membersC
(^ (list))
primitiveA.analyse-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 (la.product membersA)))
_
(analyse-product analyse membersC))))))
|
