ext-stlc-tests.rkt (5933B)
1 #lang s-exp "../ext-stlc.rkt" 2 (require "rackunit-typechecking.rkt") 3 4 ;; tests for define-type-alias 5 (define-type-alias (A X) (add1 X)) 6 7 (typecheck-fail (λ ([f : (A 1)]) f) #:with-msg "not a valid type") 8 9 ;; tests for stlc extensions 10 ;; new literals and base types 11 (check-type "one" : String) ; literal now supported 12 (check-type #f : Bool) ; literal now supported 13 14 (check-type (λ ([x : Bool]) x) : (→ Bool Bool)) ; Bool is now valid type 15 16 ;; Unit 17 (check-type (void) : Unit) 18 (check-type void : (→ Unit)) 19 20 (typecheck-fail 21 ((λ ([x : Unit]) x) 2) 22 #:with-msg "expected Unit, given Int\n *expression: 2") 23 (typecheck-fail 24 ((λ ([x : Unit]) x) void) 25 #:with-msg "expected Unit, given \\(→ Unit\\)\n *expression: void") 26 27 (check-type ((λ ([x : Unit]) x) (void)) : Unit) 28 29 ;; begin 30 (check-type (begin 1) : Int) 31 32 (typecheck-fail (begin) #:with-msg "expected more terms") 33 ;; 2016-03-06: begin terms dont need to be Unit 34 (check-type (begin 1 2 3) : Int) 35 #;(typecheck-fail 36 (begin 1 2 3) 37 #:with-msg "Expected expression 1 to have Unit type, got: Int") 38 39 (check-type (begin (void) 1) : Int ⇒ 1) 40 (check-type ((λ ([x : Int]) (begin (void) x)) 1) : Int) 41 (check-type ((λ ([x : Int]) (begin x)) 1) : Int) 42 (check-type ((λ ([x : Int]) (begin (begin x))) 1) : Int) 43 (check-type ((λ ([x : Int]) (begin (void) (begin (void) x))) 1) : Int) 44 (check-type ((λ ([x : Int]) (begin (begin (void) x))) 1) : Int) 45 46 ;;ascription 47 (check-type (ann 1 : Int) : Int ⇒ 1) 48 (check-type ((λ ([x : Int]) (ann x : Int)) 10) : Int ⇒ 10) 49 (typecheck-fail (ann 1 : Bool) 50 #:with-msg "ann: type mismatch: expected Bool, given Int\n *expression: 1") 51 ;ann errs 52 (typecheck-fail (ann 1 : Complex) #:with-msg "unbound identifier") 53 (typecheck-fail (ann 1 : 1) #:with-msg "not a well-formed type") 54 (typecheck-fail (ann 1 : (λ ([x : Int]) x)) #:with-msg "not a well-formed type") 55 (typecheck-fail (ann Bool : Int) 56 #:with-msg "ann: type mismatch: expected Int, given an invalid expression\n *expression: Bool") 57 58 ; let 59 (check-type (let () (+ 1 1)) : Int ⇒ 2) 60 (check-type (let ([x 10]) (+ 1 2)) : Int) 61 (check-type (let ([x 10] [y 20]) ((λ ([z : Int] [a : Int]) (+ a z)) x y)) : Int ⇒ 30) 62 (typecheck-fail 63 (let ([x #f]) (+ x 1)) 64 #:with-msg "expected Int, given Bool\n *expression: x") 65 (typecheck-fail (let ([x 10] [y (+ x 1)]) (+ x y)) 66 #:with-msg "x: unbound identifier") 67 68 (check-type (let* ([x 10] [y (+ x 1)]) (+ x y)) : Int ⇒ 21) 69 (typecheck-fail 70 (let* ([x #t] [y (+ x 1)]) 1) 71 #:with-msg "expected Int, given Bool\n *expression: x") 72 73 ; letrec 74 (typecheck-fail 75 (letrec ([(x : Int) #f] [(y : Int) 1]) y) 76 #:with-msg 77 "letrec: type mismatch: expected Int, given Bool\n *expression: #f") 78 (typecheck-fail 79 (letrec ([(y : Int) 1] [(x : Int) #f]) x) 80 #:with-msg 81 "letrec: type mismatch: expected Int, given Bool\n *expression: #f") 82 (typecheck-fail 83 (ann (letrec ([(x : Int) #f] [(y : Int) 1]) y) : Int) 84 #:with-msg 85 "letrec: type mismatch: expected Int, given Bool\n *expression: #f") 86 (typecheck-fail 87 (ann (letrec ([(y : Int) 1] [(x : Int) #f]) x) : Int) 88 #:with-msg 89 "letrec: type mismatch: expected Int, given Bool\n *expression: #f") 90 91 (check-type (letrec ([(x : Int) 1] [(y : Int) (+ x 1)]) (+ x y)) : Int ⇒ 3) 92 93 ;; recursive 94 (check-type 95 (letrec ([(countdown : (→ Int String)) 96 (λ ([i : Int]) 97 (if (= i 0) 98 "liftoff" 99 (countdown (- i 1))))]) 100 (countdown 10)) : String ⇒ "liftoff") 101 102 ;; mutually recursive 103 (check-type 104 (letrec ([(is-even? : (→ Int Bool)) 105 (λ ([n : Int]) 106 (or (zero? n) 107 (is-odd? (sub1 n))))] 108 [(is-odd? : (→ Int Bool)) 109 (λ ([n : Int]) 110 (and (not (zero? n)) 111 (is-even? (sub1 n))))]) 112 (is-odd? 11)) : Bool ⇒ #t) 113 114 ;; check some more err msgs 115 (typecheck-fail 116 (and "1" #f) 117 #:with-msg 118 "and: type mismatch: expected Bool, given String\n *expression: \"1\"") 119 (typecheck-fail 120 (and #t "2") 121 #:with-msg 122 "and: type mismatch: expected Bool, given String\n *expression: \"2\"") 123 (typecheck-fail 124 (or "1" #f) 125 #:with-msg 126 "or: type mismatch: expected Bool, given String\n *expression: \"1\"") 127 (typecheck-fail 128 (or #t "2") 129 #:with-msg 130 "or: type mismatch: expected Bool, given String\n *expression: \"2\"") 131 ;; 2016-03-10: change if to work with non-false vals 132 (check-type (if "true" 1 2) : Int -> 1) 133 (typecheck-fail 134 (if #t 1 "2") 135 #:with-msg 136 "branches have incompatible types: Int and String") 137 138 ;; tests from stlc+lit-tests.rkt -------------------------- 139 ; most should pass, some failing may now pass due to added types/forms 140 (check-type 1 : Int) 141 ;(check-not-type 1 : (Int → Int)) 142 ;(typecheck-fail "one") ; literal now supported 143 ;(typecheck-fail #f) ; literal now supported 144 (check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int)) 145 (check-not-type (λ ([x : Int]) x) : Int) 146 (check-type (λ ([x : Int]) x) : (→ Int Int)) 147 (check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int)) 148 (check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1) 149 150 (typecheck-fail 151 ((λ ([x : Bool]) x) 1) 152 #:with-msg "expected Bool, given Int\n *expression: 1") 153 ;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is now valid type 154 (typecheck-fail 155 (λ ([f : Int]) (f 1 2)) 156 #:with-msg 157 "Expected → type, got: Int") 158 159 (check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) 160 : (→ (→ Int Int Int) Int Int Int)) 161 (check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) 162 : Int ⇒ 3) 163 164 (typecheck-fail 165 (+ 1 (λ ([x : Int]) x)) 166 #:with-msg "expected Int, given \\(→ Int Int\\)\n *expression: \\(λ \\(\\(x : Int\\)\\) x\\)") 167 (typecheck-fail 168 (λ ([x : (→ Int Int)]) (+ x x)) 169 #:with-msg "expected Int, given \\(→ Int Int\\)\n *expression: x") 170 (typecheck-fail 171 ((λ ([x : Int] [y : Int]) y) 1) 172 #:with-msg "wrong number of arguments: expected 2, given 1") 173 174 (check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20) 175