-
Notifications
You must be signed in to change notification settings - Fork 0
/
type-check-Lany.rkt
175 lines (161 loc) · 6.46 KB
/
type-check-Lany.rkt
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
#lang racket
(require "utilities.rkt")
(require "type-check-Lvec.rkt")
(require "type-check-Lvecof.rkt")
(require "type-check-Llambda.rkt")
(provide type-check-Lany type-check-Lany-has-type
type-check-Lany-class type-check-any-mixin)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Type Checker for the Any type and inject, project, etc.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define (type-check-any-mixin super-class)
(class super-class
(super-new)
(inherit check-type-equal?)
(define/override (operator-types)
(append
'((integer? . ((Any) . Boolean))
(boolean? . ((Any) . Boolean))
(vector? . ((Any) . Boolean))
(procedure? . ((Any) . Boolean))
(void? . ((Any) . Boolean))
(tag-of-any . ((Any) . Integer))
(make-any . ((_ Integer) . Any))
)
(super operator-types)))
(define/public (join-types t1 t2)
(match (list t1 t2)
[(list '_ t2) t2]
[(list t1 '_) t1]
[(list `(Vector ,ts1 ...)
`(Vector ,ts2 ...))
`(Vector ,@(for/list ([t1 ts1] [t2 ts2])
(join-types t1 t2)))]
[(list `(,ts1 ... -> ,rt1)
`(,ts2 ... -> ,rt2))
`(,@(for/list ([t1 ts1] [t2 ts2])
(join-types t1 t2))
-> ,(join-types rt1 rt2))]
[else
t1]))
(define/public (flat-ty? ty)
(match ty
[(or `Integer `Boolean '_ `Void)
#t]
;; The following is a special case to handle programs
;; after closure conversion. -Jeremy
[`(Vector ((Vector _) ,ts ... -> Any))
(for/and ([t ts]) (eq? t 'Any))]
[`(Vector ,ts ...)
(for/and ([t ts]) (eq? t 'Any))]
['(Vectorof Any) #t]
[`(,ts ... -> ,rt)
(and (eq? rt 'Any) (for/and ([t ts]) (eq? t 'Any)))]
[else
#f]
))
(define/override (type-check-exp env)
(lambda (e)
(debug 'type-check-exp "any" e)
(define recur (type-check-exp env))
(match e
[(Prim 'any-vector-length (list e1))
(define-values (e1^ t1) (recur e1))
(check-type-equal? t1 'Any e)
(values (Prim 'any-vector-length (list e1^)) 'Integer)]
[(Prim 'any-vectorof-length (list e1))
(define-values (e1^ t1) (recur e1))
(check-type-equal? t1 'Any e)
(values (Prim 'any-vectorof-length (list e1^)) 'Integer)]
[(Prim 'any-vector-ref (list e1 e2))
(define-values (e1^ t1) (recur e1))
(define-values (e2^ t2) (recur e2))
(check-type-equal? t1 'Any e)
(check-type-equal? t2 'Integer e)
(values (Prim 'any-vector-ref (list e1^ e2^)) 'Any)]
[(Prim 'any-vectorof-ref (list e1 e2))
(define-values (e1^ t1) (recur e1))
(define-values (e2^ t2) (recur e2))
(check-type-equal? t1 'Any e)
(check-type-equal? t2 'Integer e)
(values (Prim 'any-vectorof-ref (list e1^ e2^)) 'Any)]
[(Prim 'any-vector-set! (list e1 e2 e3))
(define-values (e1^ t1) (recur e1))
(define-values (e2^ t2) (recur e2))
(define-values (e3^ t3) (recur e3))
(check-type-equal? t1 'Any e)
(check-type-equal? t2 'Integer e)
(check-type-equal? t3 'Any e)
(values (Prim 'any-vector-set! (list e1^ e2^ e3^)) 'Void)]
[(Prim 'any-vectorof-set! (list e1 e2 e3))
(define-values (e1^ t1) (recur e1))
(define-values (e2^ t2) (recur e2))
(define-values (e3^ t3) (recur e3))
(check-type-equal? t1 'Any e)
(check-type-equal? t2 'Integer e)
(check-type-equal? t3 'Any e)
(values (Prim 'any-vectorof-set! (list e1^ e2^ e3^)) 'Void)]
[(ValueOf e ty)
(define-values (new-e e-ty) (recur e))
(values (ValueOf new-e ty) ty)]
[else ((super type-check-exp env) e)])))
))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; type-check-Lany
(define type-check-Lany-class
(class (type-check-any-mixin type-check-Llambda-class)
(super-new)
(inherit check-type-equal? join-types operator-types flat-ty?)
(define/public (type-predicates)
(set 'boolean? 'integer? 'vector? 'procedure? 'void?))
(define/override (type-check-exp env)
(lambda (e)
(debug 'type-check-exp "Lany" e)
(define recur (type-check-exp env))
(match e
;; Change If to use join-types
[(If cnd thn els)
(define-values (cnd^ Tc) (recur cnd))
(define-values (thn^ Tt) (recur thn))
(define-values (els^ Te) (recur els))
(check-type-equal? Tc 'Boolean cnd)
(check-type-equal? Tt Te e)
(values (If cnd^ thn^ els^) (join-types Tt Te))]
[(Inject e1 ty)
(unless (flat-ty? ty)
(error 'type-check "may only inject from flat type, not ~a" ty))
(define-values (new-e1 e-ty) (recur e1))
(check-type-equal? e-ty ty e)
(values (Inject new-e1 ty) 'Any)]
[(Project e1 ty)
(unless (flat-ty? ty)
(error 'type-check "may only project to flat type, not ~a" ty))
(define-values (new-e1 e-ty) (recur e1))
(check-type-equal? e-ty 'Any e)
(values (Project new-e1 ty) ty)]
[(Prim pred (list e1))
#:when (set-member? (type-predicates) pred)
(define-values (new-e1 e-ty) (recur e1))
(check-type-equal? e-ty 'Any e)
(values (Prim pred (list new-e1)) 'Boolean)]
[(Prim 'eq? (list arg1 arg2))
(define-values (e1 t1) (recur arg1))
(define-values (e2 t2) (recur arg2))
(match* (t1 t2)
;; allow comparison of vectors of different element types
[(`(Vector ,ts1 ...) `(Vector ,ts2 ...)) (void)]
[(`(Vectorof ,t1) `(Vectorof ,t2)) (void)]
[(other wise) (check-type-equal? t1 t2 e)])
(values (Prim 'eq? (list e1 e2)) 'Boolean)]
[else ((super type-check-exp env) e)])))
))
(define (type-check-Lany p)
(send (new type-check-Lany-class) type-check-program p))
(define (type-check-Lany-has-type p)
(begin
(typed-vec #t)
(typed-vecof #t)
(define t (send (new type-check-Lany-class) type-check-program p))
(typed-vec #f)
(typed-vecof #f)
t))