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