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
|
(;module:
lux
(lux (control monad
pipe)
[io #- run]
[function]
(concurrency ["A" atom])
(data [text "T/" Eq<Text>]
text/format
[ident]
(coll [list "L/" Fold<List> Monoid<List> Monad<List>]
["D" dict]
["S" set])
[number]
[product])
[macro #+ Monad<Lux>]
(macro [code])
[type]
(type ["TC" check]))
(luxc ["&" base]
(lang ["la" analysis])
["&;" module]
["&;" env]
(analyser ["&;" common]
["&;" inference])))
(def: #export (analyse-sum analyse tag valueC)
(-> &;Analyser Nat Code (Lux la;Analysis))
(do Monad<Lux>
[expected macro;expected-type]
(&;with-stacked-errors
(function [_] (format "Invalid type for variant: " (%type expected)))
(case expected
(#;Sum _)
(let [flat (type;flatten-variant expected)
type-size (list;size flat)]
(case (list;nth tag flat)
(#;Some variant-type)
(do @
[valueA (&;with-expected-type variant-type
(analyse valueC))
temp &env;next-local]
(wrap (la;sum tag type-size temp valueA)))
#;None
(&common;variant-out-of-bounds-error expected type-size tag)))
(#;Named name unnamedT)
(&;with-expected-type unnamedT
(analyse-sum analyse tag valueC))
(#;Var id)
(do @
[bound? (&;within-type-env
(TC;bound? id))]
(if bound?
(do @
[expected' (&;within-type-env
(TC;read-var id))]
(&;with-expected-type expected'
(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.
(&;fail (format "Invalid type for variant: " (%type expected)))))
(#;UnivQ _)
(do @
[[var-id var] (&;within-type-env
TC;existential)]
(&;with-expected-type (assume (type;apply-type expected var))
(analyse-sum analyse tag valueC)))
(#;ExQ _)
(&common;with-var
(function [[var-id var]]
(&;with-expected-type (assume (type;apply-type expected var))
(analyse-sum analyse tag valueC))))
_
(&;fail "")))))
(def: (analyse-typed-product analyse members)
(-> &;Analyser (List Code) (Lux la;Analysis))
(do Monad<Lux>
[expected macro;expected-type]
(loop [expected expected
members members]
(case [expected 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 (#la;Product 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 (macro;gensym "tail")]
(&;with-expected-type tailT
(analyse (` ((~' _lux_case) [(~@ tailC)]
(~ g!tail)
(~ g!tail))))))
))))
(def: #export (analyse-product analyse membersC)
(-> &;Analyser (List Code) (Lux la;Analysis))
(do Monad<Lux>
[expected macro;expected-type]
(&;with-stacked-errors
(function [_] (format "Invalid type for tuple: " (%type expected)))
(case expected
(#;Product _)
(analyse-typed-product analyse membersC)
(#;Named name unnamedT)
(&;with-expected-type unnamedT
(analyse-product analyse membersC))
(#;Var id)
(do @
[bound? (&;within-type-env
(TC;bound? id))]
(if bound?
(do @
[expected' (&;within-type-env
(TC;read-var id))]
(&;with-expected-type expected'
(analyse-product analyse membersC)))
## Must do inference...
(do @
[membersTA (mapM @ (|>. analyse &common;with-unknown-type)
membersC)
_ (&;within-type-env
(TC;check expected
(type;tuple (L/map product;left membersTA))))]
(wrap (la;product (L/map product;right membersTA))))))
(#;UnivQ _)
(do @
[[var-id var] (&;within-type-env
TC;existential)]
(&;with-expected-type (assume (type;apply-type expected var))
(analyse-product analyse membersC)))
(#;ExQ _)
(&common;with-var
(function [[var-id var]]
(&;with-expected-type (assume (type;apply-type expected var))
(analyse-product analyse membersC))))
_
(&;fail "")
))))
(def: #export (analyse-tagged-sum analyse tag value)
(-> &;Analyser Ident Code (Lux la;Analysis))
(do Monad<Lux>
[tag (macro;normalize tag)
[idx group variantT] (macro;resolve-tag tag)
#let [case-size (list;size group)]
inferenceT (&inference;variant-inference-type idx case-size variantT)
[inferredT valueA+] (&inference;apply-function analyse inferenceT (list value))
expectedT macro;expected-type
_ (&;within-type-env
(TC;check expectedT inferredT))
temp &env;next-local]
(wrap (la;sum idx case-size temp (|> valueA+ list;head assume)))))
## 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]) (Lux (List [Ident Code])))
(mapM Monad<Lux>
(function [[key val]]
(case key
[_ (#;Tag key)]
(do Monad<Lux>
[key (macro;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]) (Lux [(List Code) Type]))
(case record
## empty-record = empty-tuple = unit = []
#;Nil
(:: Monad<Lux> wrap [(list) Unit])
(#;Cons [head-k head-v] _)
(do Monad<Lux>
[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 [])
(&;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 (D;from-list ident;Hash<Ident> (list;zip2 tag-set tuple-range))]
idx->val (foldM @
(function [[key val] idx->val]
(do @
[key (macro;normalize key)]
(case (D;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 (D;contains? idx idx->val)
(&;fail (format "Cannot repeat tag inside record: " (%code (code;tag key))))
(wrap (D;put idx val idx->val))))))
(: (D;Dict Nat Code)
(D;new number;Hash<Nat>))
record)
#let [ordered-tuple (L/map (function [idx] (assume (D;get idx idx->val)))
tuple-range)]]
(wrap [ordered-tuple recordT]))
))
(def: #export (analyse-record analyse members)
(-> &;Analyser (List [Code Code]) (Lux la;Analysis))
(do Monad<Lux>
[members (normalize members)
[members recordT] (order members)
expectedT macro;expected-type
inferenceT (&inference;record-inference-type recordT)
[inferredT membersA] (&inference;apply-function analyse inferenceT members)
_ (&;within-type-env
(TC;check expectedT inferredT))]
(wrap (la;product membersA))))
|
