stlc+reco+sub-tests.rkt (5473B)
1 #lang s-exp "../stlc+reco+sub.rkt" 2 (require "rackunit-typechecking.rkt") 3 4 ;; record subtyping tests 5 (check-type "coffee" : String) 6 (check-type (tup [coffee = 3]) : (× [coffee : Int])) ; element subtyping 7 (check-type (var coffee = 3 as (∨ [coffee : Nat])) : (∨ [coffee : Int])) ; element subtyping 8 ;err 9 (typecheck-fail 10 (var cooffee = 3 as (∨ [coffee : Nat])) 11 #:with-msg "cooffee field does not exist") 12 (check-type (tup [coffee = 3]) : (× [coffee : Nat])) 13 (check-type (tup [coffee = 3]) : (× [coffee : Top])) 14 (check-type (var coffee = 3 as (∨ [coffee : Int])) : (∨ [coffee : Top])) ; element subtyping (twice) 15 (check-type (tup [coffee = 3]) : (× [coffee : Num])) 16 (check-not-type (tup [coffee = -3]) : (× [coffee : Nat])) 17 (check-type (tup [coffee = -3]) : (× [coffee : Num])) 18 (check-type (tup [coffee = -3] [tea = 3]) : (× [coffee : Int])) ; width subtyping 19 (check-type (tup [coffee = -3] [tea = 3]) : (× [coffee : Num])) ; width+element subtyping 20 21 ;; record + fns 22 (check-type (tup [plus = +]) : (× [plus : (→ Num Num Num)])) 23 (check-type + : (→ Num Num Num)) 24 (check-type (tup [plus = +]) : (× [plus : (→ Int Num Num)])) 25 (check-type (tup [plus = +]) : (× [plus : (→ Int Num Top)])) 26 (check-type (tup [plus = +] [mul = *]) : (× [plus : (→ Int Num Top)])) 27 28 ;; examples from tapl ch26, bounded quantification 29 (check-type (λ ([x : (× [a : Int])]) x) : (→ (× [a : Int]) (× [a : Int]))) 30 31 (check-type ((λ ([x : (× [a : Int])]) x) (tup [a = 0])) 32 : (× [a : Int]) ⇒ (tup [a = 0])) 33 (check-type ((λ ([x : (× [a : Int])]) x) (tup [a = 0][b = #t])) 34 : (× [a : Int]) ⇒ (tup [a = 0][b = #t])) 35 36 (check-type (proj ((λ ([x : (× [a : Int])]) x) (tup [a = 0][b = #t])) a) 37 : Int ⇒ 0) 38 39 ;; this should work! but needs bounded quantification, see fsub.rkt 40 (typecheck-fail (proj ((λ ([x : (× [a : Int])]) x) (tup [a = 0][b = #t])) b)) 41 42 ; conditional 43 (check-not-type (λ ([x : Int]) (if #t 1 -1)) : (→ Int Nat)) 44 (check-type (λ ([x : Int]) (if #t 1 -1)) : (→ Int Int)) 45 (check-not-type (λ ([x : Int]) (if #t -1 1)) : (→ Int Nat)) 46 (check-type (λ ([x : Int]) (if #t -1 1)) : (→ Int Int)) 47 (check-type (λ ([x : Bool]) (if x "1" 1)) : (→ Bool Top)) 48 49 ;; previous record tests ------------------------------------------------------ 50 ;; records (ie labeled tuples) 51 (check-type "Stephen" : String) 52 (check-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) : 53 (× [name : String] [phone : Int] [male? : Bool])) 54 (check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) name) 55 : String ⇒ "Stephen") 56 (check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) name) 57 : String ⇒ "Stephen") 58 (check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) phone) 59 : Int ⇒ 781) 60 (check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) male?) 61 : Bool ⇒ #t) 62 (check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) : 63 (× [my-name : String] [phone : Int] [male? : Bool])) 64 (check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) : 65 (× [name : String] [my-phone : Int] [male? : Bool])) 66 (check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) : 67 (× [name : String] [phone : Int] [is-male? : Bool])) 68 69 70 ;; previous basic subtyping tests ------------------------------------------------------ 71 (check-type 1 : Top) 72 (check-type 1 : Num) 73 (check-type 1 : Int) 74 (check-type 1 : Nat) 75 (check-type -1 : Top) 76 (check-type -1 : Num) 77 (check-type -1 : Int) 78 (check-not-type -1 : Nat) 79 (check-type ((λ ([x : Top]) x) 1) : Top ⇒ 1) 80 (check-type ((λ ([x : Top]) x) -1) : Top ⇒ -1) 81 (check-type ((λ ([x : Num]) x) -1) : Num ⇒ -1) 82 (check-type ((λ ([x : Int]) x) -1) : Int ⇒ -1) 83 (typecheck-fail ((λ ([x : Nat]) x) -1)) 84 (check-type (λ ([x : Int]) x) : (→ Int Int)) 85 (check-type (λ ([x : Int]) x) : (→ Int Num)) ; covariant output 86 (check-not-type (λ ([x : Int]) x) : (→ Int Nat)) 87 (check-type (λ ([x : Int]) x) : (→ Nat Int)) ; contravariant input 88 (check-not-type (λ ([x : Int]) x) : (→ Num Int)) 89 90 ;; previous tests ------------------------------------------------------------- 91 ;; some change due to more specific types 92 (check-type 1 : Int) 93 (check-not-type 1 : (→ Int Int)) 94 ;(typecheck-fail "one") ; unsupported literal 95 ;(typecheck-fail #f) ; unsupported literal 96 (check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int)) 97 (check-not-type (λ ([x : Int]) x) : Int) 98 (check-type (λ ([x : Int]) x) : (→ Int Int)) 99 (check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int)) 100 (check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1) 101 ; Bool now defined 102 ;(typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool is not valid type 103 ;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is not valid type 104 (typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type 105 (check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) 106 : (→ (→ Int Int Int) Int Int Int)) 107 ;(check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3) 108 ;; changed test 109 (check-type ((λ ([f : (→ Num Num Num)] [x : Int] [y : Int]) (f x y)) + 1 2) : Num ⇒ 3) 110 (typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int 111 (typecheck-fail (λ ([x : (→ Int Int)]) (+ x x))) ; x should be Int 112 (typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args 113 (check-type ((λ ([x : Int]) (+ x x)) 10) : Num ⇒ 20)