stlc+tup-tests.rkt (4116B)
1 #lang s-exp "../stlc+tup.rkt" 2 (require "rackunit-typechecking.rkt") 3 4 ;; tests for tuples 5 (check-type (tup 1 2 3) : (× Int Int Int)) 6 (check-type (tup 1 "1" #f +) : (× Int String Bool (→ Int Int Int))) 7 (check-not-type (tup 1 "1" #f +) : (× Unit String Bool (→ Int Int Int))) 8 (check-not-type (tup 1 "1" #f +) : (× Int Unit Bool (→ Int Int Int))) 9 (check-not-type (tup 1 "1" #f +) : (× Int String Unit (→ Int Int Int))) 10 (check-not-type (tup 1 "1" #f +) : (× Int String Bool (→ Int Int Unit))) 11 12 (check-type (proj (tup 1 "2" #f) 0) : Int ⇒ 1) 13 (check-type (proj (tup 1 "2" #f) 1) : String ⇒ "2") 14 (check-type (proj (tup 1 "2" #f) 2) : Bool ⇒ #f) 15 (typecheck-fail (proj (tup 1 "2" #f) -1) #:with-msg "expected exact-nonnegative-integer") 16 (typecheck-fail (proj (tup 1 "2" #f) 3) #:with-msg "index too large") 17 (typecheck-fail 18 (proj 1 2) 19 #:with-msg 20 "proj: Expected × type, got: Int") 21 22 ;; ext-stlc.rkt tests --------------------------------------------------------- 23 ;; should still pass 24 25 ;; new literals and base types 26 (check-type "one" : String) ; literal now supported 27 (check-type #f : Bool) ; literal now supported 28 29 (check-type (λ ([x : Bool]) x) : (→ Bool Bool)) ; Bool is now valid type 30 31 ;; Unit 32 (check-type (void) : Unit) 33 (check-type void : (→ Unit)) 34 (typecheck-fail ((λ ([x : Unit]) x) 2)) 35 (typecheck-fail ((λ ([x : Unit])) void)) 36 (check-type ((λ ([x : Unit]) x) (void)) : Unit) 37 38 ;; begin 39 (typecheck-fail (begin)) 40 (check-type (begin 1) : Int) 41 ;(typecheck-fail (begin 1 2 3)) 42 (check-type (begin (void) 1) : Int ⇒ 1) 43 44 ;;ascription 45 (typecheck-fail (ann 1 : Bool)) 46 (check-type (ann 1 : Int) : Int ⇒ 1) 47 (check-type ((λ ([x : Int]) (ann x : Int)) 10) : Int ⇒ 10) 48 49 ; let 50 (check-type (let () (+ 1 1)) : Int ⇒ 2) 51 (check-type (let ([x 10]) (+ 1 2)) : Int) 52 (typecheck-fail (let ([x #f]) (+ x 1))) 53 (check-type (let ([x 10] [y 20]) ((λ ([z : Int] [a : Int]) (+ a z)) x y)) : Int ⇒ 30) 54 (typecheck-fail (let ([x 10] [y (+ x 1)]) (+ x y))) ; unbound identifier 55 56 (check-type (let* ([x 10] [y (+ x 1)]) (+ x y)) : Int ⇒ 21) 57 (typecheck-fail (let* ([x #t] [y (+ x 1)]) 1)) 58 59 ; letrec 60 (typecheck-fail (letrec ([(x : Int) #f] [(y : Int) 1]) y)) 61 (typecheck-fail (letrec ([(y : Int) 1] [(x : Int) #f]) x)) 62 63 (check-type (letrec ([(x : Int) 1] [(y : Int) (+ x 1)]) (+ x y)) : Int ⇒ 3) 64 65 ;; recursive 66 (check-type 67 (letrec ([(countdown : (→ Int String)) 68 (λ ([i : Int]) 69 (if (= i 0) 70 "liftoff" 71 (countdown (- i 1))))]) 72 (countdown 10)) : String ⇒ "liftoff") 73 74 ;; mutually recursive 75 (check-type 76 (letrec ([(is-even? : (→ Int Bool)) 77 (λ ([n : Int]) 78 (or (zero? n) 79 (is-odd? (sub1 n))))] 80 [(is-odd? : (→ Int Bool)) 81 (λ ([n : Int]) 82 (and (not (zero? n)) 83 (is-even? (sub1 n))))]) 84 (is-odd? 11)) : Bool ⇒ #t) 85 86 ;; tests from stlc+lit-tests.rkt -------------------------- 87 ; most should pass, some failing may now pass due to added types/forms 88 (check-type 1 : Int) 89 ;(check-not-type 1 : (Int → Int)) 90 ;(typecheck-fail "one") ; literal now supported 91 ;(typecheck-fail #f) ; literal now supported 92 (check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int)) 93 (check-not-type (λ ([x : Int]) x) : Int) 94 (check-type (λ ([x : Int]) x) : (→ Int Int)) 95 (check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int)) 96 (check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1) 97 (typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool now valid type, but arg has wrong type 98 ;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is now valid type 99 (typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type 100 (check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) 101 : (→ (→ Int Int Int) Int Int Int)) 102 (check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3) 103 (typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int 104 (typecheck-fail (λ ([x : (→ Int Int)]) (+ x x))) ; x should be Int 105 (typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args 106 (check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20) 107