stlc+sub-tests.rkt (2767B)
1 #lang s-exp "../stlc+sub.rkt" 2 (require "rackunit-typechecking.rkt") 3 4 ;; subtyping tests 5 (check-type 1 : Top) 6 (check-type 1 : Num) 7 (check-type 1 : Int) 8 (check-type 1 : Nat) 9 (check-type -1 : Top) 10 (check-type -1 : Num) 11 (check-type -1 : Int) 12 (check-not-type -1 : Nat) 13 (check-type ((λ ([x : Top]) x) 1) : Top ⇒ 1) 14 (check-type ((λ ([x : Top]) x) -1) : Top ⇒ -1) 15 (check-type ((λ ([x : Num]) x) -1) : Num ⇒ -1) 16 (check-type ((λ ([x : Int]) x) -1) : Int ⇒ -1) 17 (typecheck-fail ((λ ([x : Nat]) x) -1)) 18 (check-type (λ ([x : Int]) x) : (→ Int Int)) 19 (check-type (λ ([x : Int]) x) : (→ Int Num)) ; covariant output 20 (check-not-type (λ ([x : Int]) x) : (→ Int Nat)) 21 (check-type (λ ([x : Int]) x) : (→ Nat Int)) ; contravariant input 22 (check-not-type (λ ([x : Int]) x) : (→ Num Int)) 23 24 (check-type ((λ ([f : (→ Int Int)]) (f -1)) add1) : Int ⇒ 0) 25 (check-type ((λ ([f : (→ Nat Int)]) (f 1)) add1) : Int ⇒ 2) 26 (typecheck-fail ((λ ([f : (→ Num Int)]) (f 1.1)) add1)) 27 (check-type ((λ ([f : (→ Nat Num)]) (f 1)) add1) : Num ⇒ 2) 28 (typecheck-fail ((λ ([f : (→ Num Num)]) (f 1.1)) add1)) 29 30 (check-type + : (→ Num Num Num)) 31 (check-type + : (→ Int Num Num)) 32 (check-type + : (→ Int Int Num)) 33 (check-not-type + : (→ Top Int Num)) 34 (check-not-type + : (→ Top Int Int)) 35 (check-type + : (→ Nat Int Top)) 36 37 ;; previous tests ------------------------------------------------------------- 38 ;; some change due to more specific types 39 (check-type 1 : Int) 40 (check-not-type 1 : (→ Int Int)) 41 (check-type "one" : String) 42 (check-type #f : Bool) 43 (check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int)) 44 (check-not-type (λ ([x : Int]) x) : Int) 45 (check-type (λ ([x : Int]) x) : (→ Int Int)) 46 (check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int)) 47 (check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1) 48 (typecheck-fail ((λ ([x : Sym]) x) 1)) ; Sym is not valid type 49 (typecheck-fail (λ ([x : Sym]) x)) ; Sym is not valid type 50 (typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type 51 (check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) 52 : (→ (→ Int Int Int) Int Int Int)) 53 ;(check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3) 54 ;; changed test 55 (check-type ((λ ([f : (→ Num Num Num)] [x : Int] [y : Int]) (f x y)) + 1 2) : Num ⇒ 3) 56 (typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int 57 (typecheck-fail (λ ([x : (→ Int Int)]) (+ x x))) ; x should be Int 58 (typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args 59 (check-type ((λ ([x : Int]) (+ x x)) 10) : Num ⇒ 20) 60 61 (check-not-type (λ ([x : Int]) x) : Int) 62 (check-not-type (λ ([x : Int] [y : Int]) x) : (→ Int Int)) 63 (check-not-type (λ ([x : Int]) x) : (→ Int Int Int Int))