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
|
(;module:
lux
(lux (control [monad #+ do]
["ex" exception #+ exception:]
pipe)
[function]
(concurrency ["A" atom])
(data [ident]
[number]
[product]
[maybe]
(coll [list "list/" Functor<List>]
[dict #+ Dict])
[text]
text/format)
[meta]
(meta [code]
[type]
(type ["tc" check])))
(luxc ["&" base]
(lang ["la" analysis]
(analysis ["&;" common]
["&;" inference]))
["&;" module]
["&;" scope]))
(exception: #export Not-Variant-Type)
(exception: #export Not-Tuple-Type)
(exception: #export Cannot-Infer-Numeric-Tag)
(type: Type-Error
(-> Type Text))
(def: (not-quantified type)
Type-Error
(format "Not a quantified type: " (%type type)))
(def: #export (analyse-sum analyse tag valueC)
(-> &;Analyser Nat Code (Meta la;Analysis))
(do meta;Monad<Meta>
[expectedT meta;expected-type]
(&;with-stacked-errors
(function [_] (Not-Variant-Type (format " Tag: " (%n tag) "\n"
"Value: " (%code valueC) "\n"
" Type: " (%type expectedT))))
(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-expected-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-expected-type unnamedT
(analyse-sum analyse tag valueC))
(#;Var id)
(do @
[bound? (&;with-type-env
(tc;bound? id))]
(if bound?
(do @
[expectedT' (&;with-type-env
(tc;read id))]
(&;with-expected-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 " Tag: " (%n tag) "\n"
"Value: " (%code valueC) "\n"
" Type: " (%type expectedT)))))
(#;UnivQ _)
(do @
[[var-id var] (&;with-type-env
tc;existential)]
(&;with-expected-type (maybe;assume (type;apply (list var) expectedT))
(analyse-sum analyse tag valueC)))
(#;ExQ _)
(&common;with-var
(function [[var-id var]]
(&;with-expected-type (maybe;assume (type;apply (list var) expectedT))
(analyse-sum analyse tag valueC))))
(#;Apply inputT funT)
(case (type;apply (list inputT) funT)
#;None
(&;fail (not-quantified funT))
(#;Some outputT)
(&;with-expected-type outputT
(analyse-sum analyse tag valueC)))
_
(&;throw Not-Variant-Type (format " Tag: " (%n tag) "\n"
"Value: " (%code valueC) "\n"
" Type: " (%type expectedT)))))))
(def: (analyse-typed-product analyse members)
(-> &;Analyser (List Code) (Meta la;Analysis))
(do meta;Monad<Meta>
[expectedT meta;expected-type]
(loop [expectedT expectedT
members members]
(case [expectedT members]
## 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-expected-type leftT
(analyse leftC))
rightA (recur rightT rightC)]
(wrap (` [(~ leftA) (~ rightA)])))
## If the tuple runs out, whatever expression is the last gets
## matched to the remaining type.
[tailT (#;Cons tailC #;Nil)]
(&;with-expected-type tailT
(analyse tailC))
## 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]
(do @
[g!tail (meta;gensym "tail")]
(&;with-expected-type tailT
(analyse (` ((~' _lux_case) [(~@ tailC)]
(~ g!tail)
(~ g!tail))))))
))))
(def: #export (analyse-product analyse membersC)
(-> &;Analyser (List Code) (Meta la;Analysis))
(do meta;Monad<Meta>
[expectedT meta;expected-type]
(&;with-stacked-errors
(function [_] (Not-Tuple-Type (format " Type: " (%type expectedT) "\n"
"Value: " (%code (` [(~@ membersC)])))))
(case expectedT
(#;Product _)
(analyse-typed-product analyse membersC)
(#;Named name unnamedT)
(&;with-expected-type unnamedT
(analyse-product analyse membersC))
(#;Var id)
(do @
[bound? (&;with-type-env
(tc;bound? id))]
(if bound?
(do @
[expectedT' (&;with-type-env
(tc;read id))]
(&;with-expected-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))))))
(#;UnivQ _)
(do @
[[var-id var] (&;with-type-env
tc;existential)]
(&;with-expected-type (maybe;assume (type;apply (list var) expectedT))
(analyse-product analyse membersC)))
(#;ExQ _)
(&common;with-var
(function [[var-id var]]
(&;with-expected-type (maybe;assume (type;apply (list var) expectedT))
(analyse-product analyse membersC))))
(#;Apply inputT funT)
(case (type;apply (list inputT) funT)
#;None
(&;fail (not-quantified funT))
(#;Some outputT)
(&;with-expected-type outputT
(analyse-product analyse membersC)))
_
(&;throw Not-Tuple-Type (format " Type: " (%type expectedT) "\n"
"Value: " (%code (` [(~@ membersC)]))))
))))
(def: #export (analyse-tagged-sum analyse tag valueC)
(-> &;Analyser Ident Code (Meta la;Analysis))
(do meta;Monad<Meta>
[tag (meta;normalize tag)
[idx group variantT] (meta;resolve-tag tag)
expectedT meta;expected-type]
(case expectedT
(#;Var _)
(do @
[#let [case-size (list;size group)]
inferenceT (&inference;variant idx case-size variantT)
[inferredT valueA+] (&inference;apply-function analyse inferenceT (list valueC))
_ (&;with-type-env
(tc;check expectedT inferredT))
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 meta;Monad<Meta>
(function [[key val]]
(case key
[_ (#;Tag key)]
(do meta;Monad<Meta>
[key (meta;normalize key)]
(wrap [key val]))
_
(&;fail (format "Cannot use non-tag tokens in key positions in records: " (%code key)))))
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
(:: meta;Monad<Meta> wrap [(list) Unit])
(#;Cons [head-k head-v] _)
(do meta;Monad<Meta>
[head-k (meta;normalize head-k)
[_ tag-set recordT] (meta;resolve-tag head-k)
#let [size-record (list;size record)
size-ts (list;size tag-set)]
_ (if (n.= size-ts size-record)
(wrap [])
(&;fail (format "Record size does not match tag-set size." "\n"
"Expected: " (|> size-ts nat-to-int %i) "\n"
" Actual: " (|> size-record nat-to-int %i) "\n"
"For type: " (%type recordT))))
#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 (meta;normalize key)]
(case (dict;get key tag->idx)
#;None
(&;fail (format "Tag " (%code (code;tag key))
" does not belong to tag-set for type " (%type recordT)))
(#;Some idx)
(if (dict;contains? idx idx->val)
(&;fail (format "Cannot repeat tag inside record: " (%code (code;tag key))))
(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 meta;Monad<Meta>
[members (normalize members)
[members recordT] (order members)
expectedT meta;expected-type
inferenceT (&inference;record recordT)
[inferredT membersA] (&inference;apply-function analyse inferenceT members)
_ (&;with-type-env
(tc;check expectedT inferredT))]
(wrap (la;product membersA))))
|
