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