|
24 | 24 | (define/override (type-check env)
|
25 | 25 | (lambda (e)
|
26 | 26 | (match e
|
| 27 | + [`(vector-ref ,(app (type-check env) e t) ,i) |
| 28 | + (match t |
| 29 | + [`(Vector ,ts ...) |
| 30 | + (unless (and (exact-nonnegative-integer? i) |
| 31 | + (i . < . (length ts))) |
| 32 | + (error 'type-check "invalid index ~a" i)) |
| 33 | + (let ([t (list-ref ts i)]) |
| 34 | + (values `(has-type (vector-ref ,e (has-type ,i Integer)) ,t) t))] |
| 35 | + [`(Vectorof ,t) |
| 36 | + (unless (exact-nonnegative-integer? i) |
| 37 | + (error 'type-check "invalid index ~a" i)) |
| 38 | + (values `(has-type (vector-ref ,e (has-type ,i Integer)) ,t) t)] |
| 39 | + [else (error "expected a vector in vector-ref, not" t)])] |
| 40 | + [`(vector-set! ,e-vec ,i ,e-arg) |
| 41 | + (define-values (e-vec^ t-vec) ((type-check env) e-vec)) |
| 42 | + (define-values (e-arg^ t-arg) ((type-check env) e-arg)) |
| 43 | + (match t-vec |
| 44 | + [`(Vector ,ts ...) |
| 45 | + (unless (and (exact-nonnegative-integer? i) |
| 46 | + (i . < . (length ts))) |
| 47 | + (error 'type-check "invalid index ~a" i)) |
| 48 | + (unless (equal? (list-ref ts i) t-arg) |
| 49 | + (error 'type-check "type mismatch in vector-set! ~a ~a" |
| 50 | + (list-ref ts i) t-arg)) |
| 51 | + (values `(has-type (vector-set! ,e-vec^ |
| 52 | + (has-type ,i Integer) |
| 53 | + ,e-arg^) Void) 'Void)] |
| 54 | + [`(Vectorof ,t) |
| 55 | + (unless (exact-nonnegative-integer? i) |
| 56 | + (error 'type-check "invalid index ~a" i)) |
| 57 | + (unless (equal? t t-arg) |
| 58 | + (error 'type-check "type mismatch in vector-set! ~a ~a" |
| 59 | + t t-arg)) |
| 60 | + (values `(has-type (vector-set! ,e-vec^ |
| 61 | + (has-type ,i Integer) |
| 62 | + ,e-arg^) Void) 'Void)] |
| 63 | + [else (error 'type-check |
| 64 | + "expected a vector in vector-set!, not ~a" |
| 65 | + t-vec)])] |
27 | 66 | [`(inject ,e ,ty)
|
28 | 67 | (define-values (new-e e-ty) ((type-check env) e))
|
29 | 68 | (cond
|
|
127 | 166 | (define (any-tag ty)
|
128 | 167 | (match ty
|
129 | 168 | ['Integer 0]
|
| 169 | + ['Void 0] |
130 | 170 | ['Boolean 1]
|
131 | 171 | [`(Vector ,ts ...) 2]
|
132 | 172 | [`(Vectorof ,t) 2]
|
|
238 | 278 | [`(- ,e) `(inject (- (project ,((cast-insert) e) Integer)) Integer)]
|
239 | 279 | [`(let ([,x ,e1]) ,e2) `(let ([,x ,((cast-insert) e1)]) ,((cast-insert) e2))]
|
240 | 280 | [#t `(inject #t Boolean)]
|
241 |
| - [#t `(inject #f Boolean)] |
| 281 | + [#f `(inject #f Boolean)] |
242 | 282 | [`(and ,e1 ,e2) (let ([gen (gensym)])
|
243 | 283 | `(let ([,gen ,((cast-insert) e1)])
|
244 | 284 | (if (eq? ,gen (inject #f Boolean))
|
|
247 | 287 | [`(not ,e) `(inject (not (project ,((cast-insert) e) Boolean)) Boolean)]
|
248 | 288 | [`(eq? ,e1 ,e2) `(inject (eq? ,((cast-insert) e1),((cast-insert) e2)) Boolean)]
|
249 | 289 | [`(if ,eq ,et ,ef) `(if (eq? ,((cast-insert) eq) (inject #t Boolean)) ,((cast-insert) et) ,((cast-insert) ef))]
|
250 |
| - [`(vector ,es ...) `(inject (vector ,@(map (cast-insert) es)) (Vectorof Any))] |
251 |
| - [`(vector-ref ,e1 ,n) `(vector-ref (project ,((cast-insert) e1) (Vectorof Any)) n)] |
252 |
| - [`(vector-set! ,e1 ,n ,e2) `(vector-set! (project ,((cast-insert) e1) (Vectorof Any)) n ,((cast-insert) e2))] |
| 290 | + [`(vector ,es ...) `(inject (vector ,@(map (cast-insert) es)) (Vector ,@(map (lambda (x) 'Any) es)))] |
| 291 | + [`(vector-ref ,e1 ,n) `(vector-ref (project ,((cast-insert) e1) (Vectorof Any)) ,n)] |
| 292 | + [`(vector-set! ,e1 ,n ,e2) `(vector-set! (project ,((cast-insert) e1) (Vectorof Any)) ,n ,((cast-insert) e2))] |
253 | 293 | [`(void) `(inject (void) Void)] ; ???
|
254 | 294 | [`(lambda (,xs ...) ,e) `(inject (lambda: (,@(map (lambda (x) `[,x : Any]) xs)) : Any ,((cast-insert) e)) (,@(map (lambda (x) 'Any) xs) -> Any))]
|
255 | 295 | [`(app ,e ,es ...) `(app (project ,((cast-insert) e) (,@(map (lambda (x) 'Any) es) -> Any)) ,@(map (cast-insert) es))]
|
|
335 | 375 | (cond
|
336 | 376 | [(lookup e funs #f) `(function-ref ,e ,(lookup e funs))]
|
337 | 377 | [else e])]
|
| 378 | + ['(void) '(void)] |
338 | 379 | [`(program ,ds ... ,body) #:when (or (null? ds) (not (eq? (caar ds) 'type)))
|
339 | 380 | (define funs
|
340 | 381 | (for/list ([d ds])
|
|
0 commit comments