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