stlc+union.rkt (3753B)
1 #lang s-exp "../stlc+union.rkt" 2 (require "rackunit-typechecking.rkt") 3 4 (check-type 1 : Nat) 5 (check-type -1 : NegInt) 6 (check-type 1.1 : Float) 7 (check-type (+ 1 1.1) : Num -> 2.1) 8 (check-type (+ 1.1 1) : Num -> 2.1) 9 (typecheck-fail (+ "1" 1) #:with-msg "expected Num, given String") 10 11 (check-type ((λ ([f : (→ Int Int)]) (f 10)) add1) : Int -> 11) 12 13 ;; Alex's example 14 ;; illustrates flattening 15 (define-type-alias A Int) 16 (define-type-alias B String) 17 (define-type-alias C Bool) 18 (define-type-alias AC (U A C)) 19 (define-type-alias BC (U B C)) 20 (define-type-alias A-BC (U A BC)) 21 (define-type-alias B-AC (U B AC)) 22 (check-type ((λ ([x : A-BC]) x) ((λ ([x : B-AC]) x) "1")) : A-BC -> "1") 23 24 ; check pruning and collapsing 25 (define-type-alias NN (U Nat Nat)) 26 (check-type ((λ ([x : NN]) x) 1) : Nat -> 1) 27 (define-type-alias NNN (U (U Nat Nat) (U (U Nat Nat Nat) (U Nat Nat)))) 28 (check-type ((λ ([x : NNN]) x) 1) : Nat -> 1) 29 30 ; check that pruning and collapsing don't throw away types when the union 31 ; contains another empty union 32 (typecheck-fail 33 (λ ([x : (U (U) String)]) 34 (ann x : (U))) 35 #:with-msg 36 "expected \\(U\\), given \\(U \\(U\\) String\\)") 37 38 39 ;; tests from stlc+sub --------------------- 40 (check-type 1 : Num) 41 (check-type 1 : Int) 42 (check-type -1 : Num) 43 (check-type -1 : Int) 44 (check-not-type -1 : Nat) 45 (check-type ((λ ([x : Num]) x) -1) : Num ⇒ -1) 46 (check-type ((λ ([x : Int]) x) -1) : Int ⇒ -1) 47 (typecheck-fail ((λ ([x : Nat]) x) -1) #:with-msg "expected Nat, given NegInt") 48 (check-type (λ ([x : Int]) x) : (→ Int Int)) 49 ; TODO: no function subtypes for now 50 ;(check-type (λ ([x : Int]) x) : (→ Int Num)) ; covariant output 51 (check-not-type (λ ([x : Int]) x) : (→ Int Nat)) 52 ;(check-type (λ ([x : Int]) x) : (→ Nat Int)) ; contravariant input 53 (check-not-type (λ ([x : Int]) x) : (→ Num Int)) 54 55 (check-type ((λ ([f : (→ Int Int)]) (f -1)) add1) : Int ⇒ 0) 56 ; (check-type ((λ ([f : (→ Nat Int)]) (f 1)) add1) : Int ⇒ 2) 57 (typecheck-fail ((λ ([f : (→ Num Int)]) (f 1.1)) add1)) 58 ;(check-type ((λ ([f : (→ Nat Num)]) (f 1)) add1) : Num ⇒ 2) 59 (typecheck-fail ((λ ([f : (→ Num Num)]) (f 1.1)) add1)) 60 61 (check-type + : (→ Num Num Num)) 62 ;(check-type + : (→ Int Num Num)) 63 ;(check-type + : (→ Int Int Num)) 64 ;(check-not-type + : (→ Top Int Num)) 65 (check-not-type + : (→ Int Int Int)) 66 ;(check-type + : (→ Nat Int Top)) 67 68 ;; previous tests ------------------------------------------------------------- 69 ;; some change due to more specific types 70 (check-not-type 1 : (→ Int Int)) 71 (check-type "one" : String) 72 (check-type #f : Bool) 73 (check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int)) 74 (check-type ((λ ([x : Int] [y : Int]) x) -1 1) : Int -> -1) 75 (check-not-type (λ ([x : Int]) x) : Int) 76 (check-type (λ ([x : Int]) x) : (→ Int Int)) 77 (check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) PosInt)) 78 (check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Nat)) 79 (check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1) 80 (typecheck-fail ((λ ([x : Sym]) x) 1)) ; Sym is not valid type 81 (typecheck-fail (λ ([x : Sym]) x)) ; Sym is not valid type 82 (typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type 83 (check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) 84 : (→ (→ Int Int Int) Int Int Int)) 85 (check-type ((λ ([f : (→ Num Num Num)] [x : Int] [y : Int]) (f x y)) + 1 2) : Num ⇒ 3) 86 (typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int 87 (typecheck-fail (λ ([x : (→ Int Int)]) (+ x x))) ; x should be Int 88 (typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args 89 (check-type ((λ ([x : Int]) (+ x x)) 10) : Num ⇒ 20) 90 91 (check-not-type (λ ([x : Int] [y : Int]) x) : (→ Int Int)) 92 (check-not-type (λ ([x : Int]) x) : (→ Int Int Int Int))