infer-tests.rkt (13569B)
1 #lang s-exp "../infer.rkt" 2 (require turnstile/examples/tests/rackunit-typechecking) 3 4 (typecheck-fail (λ (x) x) #:with-msg "could not infer type of x; add annotation\\(s\\)") 5 6 ; should bidirectional checking work for this case? 7 ; I think no, since TR doesnt handle it either 8 ;(typecheck-fail (λ (x) (+ x 1)) #:with-msg "add annotations") 9 ; 2015-12-18: can infer this type now 10 (check-type (λ (x) (+ x 1)) : (→ Int Int)) 11 ; can't check this case either 12 (typecheck-fail ((λ (f) (f 10)) (λ (x) x)) #:with-msg "add annotation\\(s\\)") 13 14 ; stlc+lit tests with app, but infer types (no annotations) 15 (check-type ((λ (x) x) 1) : Int ⇒ 1) 16 (check-type ((λ (f x y) (f x y)) + 1 2) : Int ⇒ 3) 17 (check-type ((λ (x) (+ x x)) 10) : Int ⇒ 20) 18 19 (check-type ((λ (x) ((λ (y) y) x)) 10) : Int ⇒ 10) 20 21 ; top level functions 22 (define (f [x : Int] → Int) x) 23 (check-type f : (→ Int Int)) 24 (check-type (f 1) : Int ⇒ 1) 25 (typecheck-fail (f (λ ([x : Int]) x))) 26 27 (define {X} (g [x : X] → X) x) 28 (check-type g : (→ {X} X X)) 29 30 ; (inferred) polymorpic instantiation 31 (check-type (g 1) : Int ⇒ 1) 32 (check-type (g #f) : Bool ⇒ #f) ; different instantiation 33 (check-type (g add1) : (→ Int Int)) 34 (check-type (g +) : (→ Int Int Int)) 35 36 ; function polymorphic in list element 37 (define {X} (g2 [lst : (List X)] → (List X)) lst) 38 (check-type g2 : (→ {X} (List X) (List X))) 39 (typecheck-fail (g2 1) #:with-msg "expected: \\(List X\\)\n *given: Int") ; TODO: more precise err msg 40 (check-type (g2 (nil {Int})) : (List Int) ⇒ (nil {Int})) 41 (check-type (g2 (nil {Bool})) : (List Bool) ⇒ (nil {Bool})) 42 (check-type (g2 (nil {(List Int)})) : (List (List Int)) ⇒ (nil {(List Int)})) 43 (check-type (g2 (nil {(→ Int Int)})) : (List (→ Int Int)) ⇒ (nil {(List (→ Int Int))})) 44 (check-type (g2 (cons 1 nil)) : (List Int) ⇒ (cons 1 nil)) 45 (check-type (g2 (cons "1" nil)) : (List String) ⇒ (cons "1" nil)) 46 47 (define {X} (g3 [lst : (List X)] → X) (hd lst)) 48 (check-type g3 : (→ {X} (List X) X)) 49 (check-type g3 : (→ {A} (List A) A)) 50 (check-not-type g3 : (→ {A B} (List A) B)) 51 (typecheck-fail (g3) #:with-msg "Expected.+arguments with type.+List") ; TODO: more precise err msg 52 (check-type (g3 (nil {Int})) : Int) ; runtime fail 53 (check-type (g3 (nil {Bool})) : Bool) ; runtime fail 54 (check-type (g3 (cons 1 nil)) : Int ⇒ 1) 55 (check-type (g3 (cons "1" nil)) : String ⇒ "1") 56 57 ; recursive fn 58 (define (recf [x : Int] → Int) (recf x)) 59 (check-type recf : (→ Int Int)) 60 61 (define (countdown [x : Int] → Int) 62 (if (zero? x) 63 0 64 (countdown (sub1 x)))) 65 (check-type (countdown 0) : Int ⇒ 0) 66 (check-type (countdown 10) : Int ⇒ 0) 67 (typecheck-fail (countdown "10") #:with-msg "expected: Int\n *given: String") 68 69 ; list abbrv 70 (check-type (list 1 2 3) : (List Int)) 71 (typecheck-fail (list 1 "3") 72 #:with-msg "expected \\(List Int\\), given \\(List String\\)\n *expression: \\(list \"3\"\\)") 73 74 75 (define {X Y} (map [f : (→ X Y)] [lst : (List X)] → (List Y)) 76 (if (nil? lst) 77 nil ; test expected-type propagation of if and define 78 ; recursive call should instantiate to "concrete" X and Y types 79 (cons (f (hd lst)) (map f (tl lst))))) 80 81 (check-type map : (→ {X Y} (→ X Y) (List X) (List Y))) 82 (check-type map : (→ {Y X} (→ Y X) (List Y) (List X))) 83 (check-type map : (→ {A B} (→ A B) (List A) (List B))) 84 (check-not-type map : (→ {X Y} (→ X X) (List X) (List X))) 85 (check-not-type map : (→ {X} (→ X X) (List X) (List X))) 86 87 ; nil without annotation tests fn-first, left-to-right arg inference (2nd #%app case) 88 (check-type (map add1 nil) : (List Int) ⇒ (nil {Int})) 89 (check-type (map add1 (list)) : (List Int) ⇒ (nil {Int})) 90 (check-type (map add1 (list 1 2 3)) : (List Int) ⇒ (list 2 3 4)) 91 (typecheck-fail (map add1 (list "1")) #:with-msg 92 (string-append 93 "couldn't unify Int and String\n" 94 " *expected: \\(→ X Y\\), \\(List X\\)\n" 95 " *given: \\(→ Int Int\\), \\(List String\\)")) 96 (check-type (map (λ ([x : Int]) (+ x 2)) (list 1 2 3)) : (List Int) ⇒ (list 3 4 5)) 97 ; doesnt work yet 98 ;; 2015-12-18: dont need annotations on lambdas with concrete type 99 (check-type (map (λ (x) (+ x 2)) (list 1 2 3)) : (List Int) ⇒ (list 3 4 5)) 100 101 (define {X} (filter [p? : (→ X Bool)] [lst : (List X)] → (List X)) 102 (if (nil? lst) 103 nil 104 (if (p? (hd lst)) 105 (cons (hd lst) (filter p? (tl lst))) 106 (filter p? (tl lst))))) 107 (define {X} (filter/let [p? : (→ X Bool)] [lst : (List X)] → (List X)) 108 (if (nil? lst) 109 nil 110 (let ([x (hd lst)] [filtered-rst (filter p? (tl lst))]) 111 (if (p? x) (cons x filtered-rst) filtered-rst)))) 112 113 (check-type (filter zero? nil) : (List Int) ⇒ (nil {Int})) 114 (check-type (filter zero? (list 1 2 3)) : (List Int) ⇒ (nil {Int})) 115 (check-type (filter zero? (list 0 1 2)) : (List Int) ⇒ (list 0)) 116 (check-type (filter (λ ([x : Int]) (not (zero? x))) (list 0 1 2)) : (List Int) ⇒ (list 1 2)) 117 ;; 2015-12-18: dont need annotations on lambdas with concrete type 118 (check-type (filter (λ (x) (not (zero? x))) (list 0 1 2)) : (List Int) ⇒ (list 1 2)) 119 120 (define {X Y} (foldr [f : (→ X Y Y)] [base : Y] [lst : (List X)] → Y) 121 (if (nil? lst) 122 base 123 (f (hd lst) (foldr f base (tl lst))))) 124 (define {X Y} (foldl [f : (→ X Y Y)] [acc : Y] [lst : (List X)] → Y) 125 (if (nil? lst) 126 acc 127 (foldr f (f (hd lst) acc) (tl lst)))) 128 129 (define {X} (all? [p? : (→ X Bool)] [lst : (List X)] → Bool) 130 (if (nil? lst) 131 #t 132 (and (p? (hd lst)) (all? p? (tl lst))))) 133 134 (define {X} (tails [lst : (List X)] → (List (List X))) 135 (if (nil? lst) 136 (list nil) 137 (cons lst (tails (tl lst))))) 138 139 ; creates backwards list 140 (define {X} (build-list [n : Int] [f : (→ Int X)] → (List X)) 141 (if (zero? (sub1 n)) 142 (list (f 0)) 143 (cons (f (sub1 n)) (build-list (sub1 n) f)))) 144 (check-type (build-list 1 add1) : (List Int) ⇒ (list 1)) 145 (check-type (build-list 3 add1) : (List Int) ⇒ (list 3 2 1)) 146 (check-type (build-list 5 sub1) : (List Int) ⇒ (list 3 2 1 0 -1)) 147 148 (define {X} (append [lst1 : (List X)] [lst2 : (List X)] → (List X)) 149 (if (nil? lst1) 150 lst2 151 (cons (hd lst1) (append (tl lst1) lst2)))) 152 153 ; nqueens 154 (define-type-alias Queen (× Int Int)) 155 (define (q-x [q : Queen] → Int) (proj q 0)) 156 (define (q-y [q : Queen] → Int) (proj q 1)) 157 (define (Q [x : Int] [y : Int] → Queen) (tup x y)) 158 159 (define (safe? [q1 : Queen] [q2 : Queen] → Bool) 160 (let ([x1 (q-x q1)][y1 (q-y q1)] 161 [x2 (q-x q2)][y2 (q-y q2)]) 162 (not (or (= x1 x2) (= y1 y2) (= (abs (- x1 x2)) (abs (- y1 y2))))))) 163 (define (safe/list? [qs : (List Queen)] → Bool) 164 (if (nil? qs) 165 #t 166 (let ([q1 (hd qs)]) 167 (all? (λ ([q2 : Queen]) (safe? q1 q2)) (tl qs))))) 168 (define (valid? [lst : (List Queen)] → Bool) 169 (all? safe/list? (tails lst))) 170 171 (define (nqueens [n : Int] → (List Queen)) 172 (let* ([process-row 173 (λ ;([r : Int] [all-possible-so-far : (List (List Queen))]) 174 (r all-possible-so-far) 175 (foldr 176 ;; 2015-12-18: dont need annotations on lambdas with concrete type 177 (λ ;([qs : (List Queen)] [new-qss : (List (List Queen))]) 178 (qs new-qss) 179 (append 180 (map 181 ;; 2015-12-18: dont need annotations on lambdas with concrete type 182 (λ (c) (cons (Q r c) qs)) 183 (build-list n add1)) 184 new-qss)) 185 nil 186 all-possible-so-far))] 187 [all-possible (foldl process-row (list nil) (build-list n add1))]) 188 (let ([solns (filter valid? all-possible)]) 189 (if (nil? solns) 190 nil 191 (hd solns))))) 192 193 (check-type nqueens : (→ Int (List Queen))) 194 (check-type (nqueens 1) : (List Queen) ⇒ (list (list 1 1))) 195 (check-type (nqueens 2) : (List Queen) ⇒ (nil {Queen})) 196 (check-type (nqueens 3) : (List Queen) ⇒ (nil {Queen})) 197 (check-type (nqueens 4) : (List Queen) ⇒ (list (Q 3 1) (Q 2 4) (Q 1 2) (Q 4 3))) 198 (check-type (nqueens 5) : (List Queen) ⇒ (list (Q 4 2) (Q 3 4) (Q 2 1) (Q 1 3) (Q 5 5))) 199 200 ; -------------------------------------------------- 201 ; all ext-stlc tests should still pass (copied below): 202 ;; tests for stlc extensions 203 ;; new literals and base types 204 (check-type "one" : String) ; literal now supported 205 (check-type #f : Bool) ; literal now supported 206 207 (check-type (λ ([x : Bool]) x) : (→ Bool Bool)) ; Bool is now valid type 208 209 ;; Unit 210 (check-type (void) : Unit) 211 (check-type void : (→ Unit)) 212 213 (typecheck-fail 214 ((λ ([x : Unit]) x) 2) 215 #:with-msg 216 "expected: Unit\n *given: Int") 217 (typecheck-fail 218 ((λ ([x : Unit]) x) void) 219 #:with-msg 220 "expected: Unit\n *given: \\(→ Unit\\)") 221 222 (check-type ((λ ([x : Unit]) x) (void)) : Unit) 223 224 ;; begin 225 (check-type (begin 1) : Int) 226 227 (typecheck-fail (begin) #:with-msg "expected more terms") 228 ;; 2016-03-06: begin terms dont need to be Unit 229 (check-type (begin 1 2 3) : Int) 230 #;(typecheck-fail 231 (begin 1 2 3) 232 #:with-msg "Expected expression 1 to have Unit type, got: Int") 233 234 (check-type (begin (void) 1) : Int ⇒ 1) 235 (check-type ((λ ([x : Int]) (begin (void) x)) 1) : Int) 236 (check-type ((λ ([x : Int]) (begin x)) 1) : Int) 237 (check-type ((λ ([x : Int]) (begin (begin x))) 1) : Int) 238 (check-type ((λ ([x : Int]) (begin (void) (begin (void) x))) 1) : Int) 239 (check-type ((λ ([x : Int]) (begin (begin (void) x))) 1) : Int) 240 241 ;;ascription 242 (check-type (ann 1 : Int) : Int ⇒ 1) 243 (check-type ((λ ([x : Int]) (ann x : Int)) 10) : Int ⇒ 10) 244 (typecheck-fail (ann 1 : Bool) #:with-msg "expected Bool, given Int\n *expression: 1") 245 ;ann errs 246 (typecheck-fail (ann 1 : Complex) #:with-msg "unbound identifier") 247 (typecheck-fail (ann 1 : 1) #:with-msg "not a well-formed type") 248 (typecheck-fail (ann 1 : (λ ([x : Int]) x)) #:with-msg "not a well-formed type") 249 (typecheck-fail (ann Bool : Int) #:with-msg "expected Int, given an invalid expression\n *expression: Bool") 250 251 ; let 252 (check-type (let () (+ 1 1)) : Int ⇒ 2) 253 (check-type (let ([x 10]) (+ 1 2)) : Int) 254 (check-type (let ([x 10] [y 20]) ((λ ([z : Int] [a : Int]) (+ a z)) x y)) : Int ⇒ 30) 255 (typecheck-fail 256 (let ([x #f]) (+ x 1)) 257 #:with-msg 258 "expected: Int, Int\n *given: Bool, Int") 259 (typecheck-fail (let ([x 10] [y (+ x 1)]) (+ x y)) 260 #:with-msg "x: unbound identifier") 261 262 (check-type (let* ([x 10] [y (+ x 1)]) (+ x y)) : Int ⇒ 21) 263 (typecheck-fail 264 (let* ([x #t] [y (+ x 1)]) 1) 265 #:with-msg 266 "expected: Int, Int\n *given: Bool, Int") 267 268 ; letrec 269 (typecheck-fail 270 (letrec ([(x : Int) #f] [(y : Int) 1]) y) 271 #:with-msg 272 "letrec: type mismatch\n *expected: +Int, Int\n *given: +Bool, Int\n *expressions: #f, 1") 273 (typecheck-fail 274 (letrec ([(y : Int) 1] [(x : Int) #f]) x) 275 #:with-msg 276 "letrec: type mismatch\n *expected: +Int, Int\n *given: +Int, Bool\n *expressions: 1, #f") 277 278 (check-type (letrec ([(x : Int) 1] [(y : Int) (+ x 1)]) (+ x y)) : Int ⇒ 3) 279 280 ;; recursive 281 (check-type 282 (letrec ([(countdown : (→ Int String)) 283 (λ ([i : Int]) 284 (if (= i 0) 285 "liftoff" 286 (countdown (- i 1))))]) 287 (countdown 10)) : String ⇒ "liftoff") 288 289 ;; mutually recursive 290 (check-type 291 (letrec ([(is-even? : (→ Int Bool)) 292 (λ ([n : Int]) 293 (or (zero? n) 294 (is-odd? (sub1 n))))] 295 [(is-odd? : (→ Int Bool)) 296 (λ ([n : Int]) 297 (and (not (zero? n)) 298 (is-even? (sub1 n))))]) 299 (is-odd? 11)) : Bool ⇒ #t) 300 301 ;; check some more err msgs 302 (typecheck-fail 303 (and "1" #f) 304 #:with-msg "and: type mismatch: expected Bool, given String\n *expression: \"1\"") 305 (typecheck-fail 306 (and #t "2") 307 #:with-msg 308 "and: type mismatch: expected Bool, given String\n *expression: \"2\"") 309 (typecheck-fail 310 (or "1" #f) 311 #:with-msg 312 "or: type mismatch\n expected: +Bool, Bool\n *given: +String, Bool\n *expressions: \"1\", #f") 313 (typecheck-fail 314 (or #t "2") 315 #:with-msg 316 "or: type mismatch\n expected: +Bool, Bool\n *given: +Bool, String\n *expressions: #t, \"2\"") 317 ;; 2016-03-10: change if to work with non-false vals 318 (check-type (if "true" 1 2) : Int -> 1) 319 (typecheck-fail 320 (if #t 1 "2") 321 #:with-msg 322 "branches have incompatible types: Int and String") 323 324 ;; tests from stlc+lit-tests.rkt -------------------------- 325 ; most should pass, some failing may now pass due to added types/forms 326 (check-type 1 : Int) 327 ;(check-not-type 1 : (Int → Int)) 328 ;(typecheck-fail "one") ; literal now supported 329 ;(typecheck-fail #f) ; literal now supported 330 (check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int)) 331 (check-not-type (λ ([x : Int]) x) : Int) 332 (check-type (λ ([x : Int]) x) : (→ Int Int)) 333 (check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int)) 334 (check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1) 335 336 (typecheck-fail 337 ((λ ([x : Bool]) x) 1) 338 #:with-msg 339 "expected: Bool\n *given: Int") 340 ;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is now valid type 341 (typecheck-fail 342 (λ ([f : Int]) (f 1 2)) 343 #:with-msg 344 "Expected expression f to have ∀ type, got: Int") 345 346 (check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) 347 : (→ (→ Int Int Int) Int Int Int)) 348 (check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) 349 : Int ⇒ 3) 350 351 (typecheck-fail 352 (+ 1 (λ ([x : Int]) x)) 353 #:with-msg 354 "expected: Int, Int\n *given: Int, \\(→ Int Int\\)") 355 (typecheck-fail 356 (λ ([x : (→ Int Int)]) (+ x x)) 357 #:with-msg 358 "expected: Int, Int\n *given: \\(→ Int Int\\), \\(→ Int Int\\)") 359 (typecheck-fail 360 ((λ ([x : Int] [y : Int]) y) 1) 361 #:with-msg "Wrong number of arguments") 362 363 (check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20) 364