stlc+box-tests.rkt (9665B)
1 #lang s-exp "../stlc+box.rkt" 2 (require "rackunit-typechecking.rkt") 3 4 (define x (ref 10)) 5 (check-type x : (Ref Int)) 6 (check-type (deref x) : Int ⇒ 10) 7 (check-type (:= x 20) : Unit) ; x still 10 because check-type does not evaluate 8 (check-type (begin (:= x 20) (deref x)) : Int ⇒ 20) 9 (check-type x : (Ref Int)) 10 (check-type (deref (ref 20)) : Int ⇒ 20) 11 (check-type (deref x) : Int ⇒ 20) 12 13 (check-type ((λ ([b : (Ref Int)]) (deref b)) (ref 10)) : Int ⇒ 10) 14 (check-type ((λ ([b : (Ref Int)]) (begin (begin (:= b 20) (deref b)))) (ref 10)) : Int ⇒ 20) 15 16 ;; Ref err msgs 17 ; wrong arity 18 (typecheck-fail 19 (λ ([lst : (Ref Int Int)]) lst) 20 #:with-msg 21 "Improper usage of type constructor Ref: \\(Ref Int Int\\), expected = 1 arguments") 22 (typecheck-fail 23 (λ ([lst : (Ref)]) lst) 24 #:with-msg 25 "Improper usage of type constructor Ref: \\(Ref\\), expected = 1 arguments") 26 (typecheck-fail 27 (deref 1) 28 #:with-msg 29 "Expected Ref type, got: Int") 30 (typecheck-fail 31 (:= 1 1) 32 #:with-msg 33 "Expected Ref type, got: Int") 34 (typecheck-fail 35 (:= (ref 1) "hi") 36 #:with-msg 37 ":=: type mismatch: expected Int, given String\n *expression: \"hi\"") 38 39 ;; previous tests: ------------------------------------------------------------ 40 (typecheck-fail (cons 1 2)) 41 ;(typecheck-fail (cons 1 nil)) ; works now 42 (check-type (cons 1 nil) : (List Int)) 43 (check-type (cons 1 (nil {Int})) : (List Int)) 44 (typecheck-fail nil) 45 (typecheck-fail (nil Int)) 46 (typecheck-fail (nil (Int))) 47 ; passes bc ⇒-rhs is only used for its runtime value 48 (check-type (nil {Int}) : (List Int) ⇒ (nil {Bool})) 49 (check-not-type (nil {Bool}) : (List Int)) 50 (check-type (nil {Bool}) : (List Bool)) 51 (check-type (nil {(→ Int Int)}) : (List (→ Int Int))) 52 (define fn-lst (cons (λ ([x : Int]) (+ 10 x)) (nil {(→ Int Int)}))) 53 (check-type fn-lst : (List (→ Int Int))) 54 (check-type (isnil fn-lst) : Bool ⇒ #f) 55 (typecheck-fail (isnil (head fn-lst))) ; head lst is not List 56 (check-type (isnil (tail fn-lst)) : Bool ⇒ #t) 57 (check-type (head fn-lst) : (→ Int Int)) 58 (check-type ((head fn-lst) 25) : Int ⇒ 35) 59 (check-type (tail fn-lst) : (List (→ Int Int)) ⇒ (nil {(→ Int Int)})) 60 61 ;; previous tests: ------------------------------------------------------------ 62 ;; define-type-alias 63 (define-type-alias Integer Int) 64 (define-type-alias ArithBinOp (→ Int Int Int)) 65 66 (check-type ((λ ([x : Int]) (+ x 2)) 3) : Integer) 67 (check-type ((λ ([x : Integer]) (+ x 2)) 3) : Int) 68 (check-type ((λ ([x : Integer]) (+ x 2)) 3) : Integer) 69 (check-type + : ArithBinOp) 70 (check-type (λ ([f : ArithBinOp]) (f 1 2)) : (→ (→ Int Int Int) Int)) 71 72 (check-type "Stephen" : String) 73 (check-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) : 74 (× [name : String] [phone : Int] [male? : Bool])) 75 (check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) name) 76 : String ⇒ "Stephen") 77 (check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) name) 78 : String ⇒ "Stephen") 79 (check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) phone) 80 : Int ⇒ 781) 81 (check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) male?) 82 : Bool ⇒ #t) 83 (check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) : 84 (× [my-name : String] [phone : Int] [male? : Bool])) 85 (check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) : 86 (× [name : String] [my-phone : Int] [male? : Bool])) 87 (check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) : 88 (× [name : String] [phone : Int] [is-male? : Bool])) 89 90 91 (check-type (var coffee = (void) as (∨ [coffee : Unit])) : (∨ [coffee : Unit])) 92 (check-not-type (var coffee = (void) as (∨ [coffee : Unit])) : (∨ [coffee : Unit] [tea : Unit])) 93 (typecheck-fail ((λ ([x : (∨ [coffee : Unit] [tea : Unit])]) x) 94 (var coffee = (void) as (∨ [coffee : Unit])))) 95 (check-type (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit])) 96 : (∨ [coffee : Unit] [tea : Unit])) 97 (check-type (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit] [coke : Unit])) 98 : (∨ [coffee : Unit] [tea : Unit] [coke : Unit])) 99 100 (typecheck-fail 101 (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit])) 102 [coffee x => 1])) ; not enough clauses 103 (typecheck-fail 104 (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit])) 105 [coffee x => 1] 106 [teaaaaaa x => 2])) ; wrong clause 107 (typecheck-fail 108 (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit])) 109 [coffee x => 1] 110 [tea x => 2] 111 [coke x => 3])) ; too many clauses 112 (typecheck-fail 113 (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit])) 114 [coffee x => "1"] 115 [tea x => 2])) ; mismatched branch types 116 (check-type 117 (case (var coffee = 1 as (∨ [coffee : Int] [tea : Unit])) 118 [coffee x => x] 119 [tea x => 2]) : Int ⇒ 1) 120 (define-type-alias Drink (∨ [coffee : Int] [tea : Unit] [coke : Bool])) 121 (check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20) 122 (check-type (λ ([x : Int]) (+ (+ x x) (+ x x))) : (→ Int Int)) 123 (check-type 124 (case ((λ ([d : Drink]) d) 125 (var coffee = 1 as (∨ [coffee : Int] [tea : Unit] [coke : Bool]))) 126 [coffee x => (+ (+ x x) (+ x x))] 127 [tea x => 2] 128 [coke y => 3]) 129 : Int ⇒ 4) 130 131 (check-type 132 (case ((λ ([d : Drink]) d) (var coffee = 1 as Drink)) 133 [coffee x => (+ (+ x x) (+ x x))] 134 [tea x => 2] 135 [coke y => 3]) 136 : Int ⇒ 4) 137 138 ;; previous tests: ------------------------------------------------------------ 139 ;; tests for tuples ----------------------------------------------------------- 140 ; fail bc tuple changed syntax 141 ;(check-type (tup 1 2 3) : (× Int Int Int)) 142 ;(check-type (tup 1 "1" #f +) : (× Int String Bool (→ Int Int Int))) 143 ;(check-not-type (tup 1 "1" #f +) : (× Unit String Bool (→ Int Int Int))) 144 ;(check-not-type (tup 1 "1" #f +) : (× Int Unit Bool (→ Int Int Int))) 145 ;(check-not-type (tup 1 "1" #f +) : (× Int String Unit (→ Int Int Int))) 146 ;(check-not-type (tup 1 "1" #f +) : (× Int String Bool (→ Int Int Unit))) 147 ; 148 ;(check-type (proj (tup 1 "2" #f) 0) : Int ⇒ 1) 149 ;(check-type (proj (tup 1 "2" #f) 1) : String ⇒ "2") 150 ;(check-type (proj (tup 1 "2" #f) 2) : Bool ⇒ #f) 151 ;(typecheck-fail (proj (tup 1 "2" #f) 3)) ; index too large 152 ;(typecheck-fail (proj 1 2)) ; not tuple 153 154 ;; ext-stlc.rkt tests --------------------------------------------------------- 155 ;; should still pass 156 157 ;; new literals and base types 158 (check-type "one" : String) ; literal now supported 159 (check-type #f : Bool) ; literal now supported 160 161 (check-type (λ ([x : Bool]) x) : (→ Bool Bool)) ; Bool is now valid type 162 163 ;; Unit 164 (check-type (void) : Unit) 165 (check-type void : (→ Unit)) 166 (typecheck-fail ((λ ([x : Unit]) x) 2)) 167 (typecheck-fail ((λ ([x : Unit])) void)) 168 (check-type ((λ ([x : Unit]) x) (void)) : Unit) 169 170 ;; begin 171 (typecheck-fail (begin)) 172 (check-type (begin 1) : Int) 173 ;; 2016-03-06: begin terms dont need to be Unit 174 (check-type (begin 1 2 3) : Int) 175 #;(typecheck-fail 176 (begin 1 2 3) 177 #:with-msg "Expected expression 1 to have Unit type, got: Int") 178 (check-type (begin (void) 1) : Int ⇒ 1) 179 180 ;;ascription 181 (typecheck-fail (ann 1 : Bool)) 182 (check-type (ann 1 : Int) : Int ⇒ 1) 183 (check-type ((λ ([x : Int]) (ann x : Int)) 10) : Int ⇒ 10) 184 185 ; let 186 (check-type (let () (+ 1 1)) : Int ⇒ 2) 187 (check-type (let ([x 10]) (+ 1 2)) : Int) 188 (typecheck-fail (let ([x #f]) (+ x 1))) 189 (check-type (let ([x 10] [y 20]) ((λ ([z : Int] [a : Int]) (+ a z)) x y)) : Int ⇒ 30) 190 (typecheck-fail (let ([x 10] [y (+ x 1)]) (+ x y))) ; unbound identifier 191 192 (check-type (let* ([x 10] [y (+ x 1)]) (+ x y)) : Int ⇒ 21) 193 (typecheck-fail (let* ([x #t] [y (+ x 1)]) 1)) 194 195 ; letrec 196 (typecheck-fail (letrec ([(x : Int) #f] [(y : Int) 1]) y)) 197 (typecheck-fail (letrec ([(y : Int) 1] [(x : Int) #f]) x)) 198 199 (check-type (letrec ([(x : Int) 1] [(y : Int) (+ x 1)]) (+ x y)) : Int ⇒ 3) 200 201 ;; recursive 202 (check-type 203 (letrec ([(countdown : (→ Int String)) 204 (λ ([i : Int]) 205 (if (= i 0) 206 "liftoff" 207 (countdown (- i 1))))]) 208 (countdown 10)) : String ⇒ "liftoff") 209 210 ;; mutually recursive 211 (check-type 212 (letrec ([(is-even? : (→ Int Bool)) 213 (λ ([n : Int]) 214 (or (zero? n) 215 (is-odd? (sub1 n))))] 216 [(is-odd? : (→ Int Bool)) 217 (λ ([n : Int]) 218 (and (not (zero? n)) 219 (is-even? (sub1 n))))]) 220 (is-odd? 11)) : Bool ⇒ #t) 221 222 ;; tests from stlc+lit-tests.rkt -------------------------- 223 ; most should pass, some failing may now pass due to added types/forms 224 (check-type 1 : Int) 225 ;(check-not-type 1 : (Int → Int)) 226 ;(typecheck-fail "one") ; literal now supported 227 ;(typecheck-fail #f) ; literal now supported 228 (check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int)) 229 (check-not-type (λ ([x : Int]) x) : Int) 230 (check-type (λ ([x : Int]) x) : (→ Int Int)) 231 (check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int)) 232 (check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1) 233 (typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool now valid type, but arg has wrong type 234 ;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is now valid type 235 (typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type 236 (check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) 237 : (→ (→ Int Int Int) Int Int Int)) 238 (check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3) 239 (typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int 240 (typecheck-fail (λ ([x : (→ Int Int)]) (+ x x))) ; x should be Int 241 (typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args 242 (check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20) 243