fsub-tests.rkt (7173B)
1 #lang s-exp "../fsub.rkt" 2 (require "rackunit-typechecking.rkt") 3 4 ;; examples from tapl ch26, bounded quantification 5 ;; (same tests from stlc+reco+sub.rkt, but last one should not typecheck) 6 (check-type (λ ([x : (× [a : Int])]) x) : (→ (× [a : Int]) (× [a : Int]))) 7 8 (define ra (tup [a = 0])) 9 (check-type ((λ ([x : (× [a : Int])]) x) ra) 10 : (× [a : Int]) ⇒ (tup [a = 0])) 11 (define rab (tup [a = 0][b = #t])) 12 (check-type ((λ ([x : (× [a : Int])]) x) rab) 13 : (× [a : Int]) ⇒ (tup [a = 0][b = #t])) 14 15 (check-type (proj ((λ ([x : (× [a : Int])]) x) rab) a) 16 : Int ⇒ 0) 17 18 (check-type (Λ ([X <: Top]) (λ ([x : X]) x)) : (∀ ([X <: Top]) (→ X X))) 19 (check-type (inst (Λ ([X <: Top]) (λ ([x : X]) x)) (× [a : Int][b : Bool])) 20 : (→ (× [a : Int][b : Bool]) (× [a : Int][b : Bool]))) 21 22 (check-type (proj ((inst (Λ ([X <: Top]) (λ ([x : X]) x)) 23 (× [a : Int][b : Bool])) 24 rab) b) 25 : Bool ⇒ #t) 26 27 (define f2 (λ ([x : (× [a : Nat])]) (tup [orig = x] [asucc = (+ 1 (proj x a))]))) 28 (check-type f2 : (→ (× [a : Nat]) (× [orig : (× [a : Nat])] [asucc : Nat]))) 29 (check-type (f2 ra) : (× [orig : (× [a : Nat])][asucc : Nat])) 30 (check-type (f2 rab) : (× [orig : (× [a : Nat])][asucc : Nat])) 31 32 ; check expose properly called for primops 33 (define fNat (Λ ([X <: Nat]) (λ ([x : X]) (+ x 1)))) 34 (check-type fNat : (∀ ([X <: Nat]) (→ X Nat))) 35 36 ;; check type constructors properly call expose 37 (define f2poly 38 (Λ ([X <: (× [a : Nat])]) 39 (λ ([x : X]) 40 (tup [orig = x][asucc = (+ (proj x a) 1)])))) 41 42 (check-type f2poly : (∀ ([X <: (× [a : Nat])]) (→ X (× [orig : X][asucc : Nat])))) 43 44 ; inst f2poly with (× [a : Nat]) 45 (check-type (inst f2poly (× [a : Nat])) 46 : (→ (× [a : Nat]) 47 (× [orig : (× [a : Nat])][asucc : Nat]))) 48 (check-type ((inst f2poly (× [a : Nat])) ra) 49 : (× [orig : (× [a : Nat])][asucc : Nat]) 50 ⇒ (tup [orig = ra][asucc = 1])) 51 52 (check-type ((inst f2poly (× [a : Nat])) rab) 53 : (× [orig : (× [a : Nat])][asucc : Nat]) 54 ⇒ (tup [orig = rab][asucc = 1])) 55 56 (typecheck-fail (proj (proj ((inst f2poly (× [a : Nat])) rab) orig) b)) 57 58 ;; inst f2poly with (× [a : Nat][b : Bool]) 59 (check-type (inst f2poly (× [a : Nat][b : Bool])) 60 : (→ (× [a : Nat][b : Bool]) 61 (× [orig : (× [a : Nat][b : Bool])][asucc : Nat]))) 62 (typecheck-fail ((inst f2poly (× [a : Nat][b : Bool])) ra)) 63 64 (check-type ((inst f2poly (× [a : Nat][b : Bool])) rab) 65 : (× [orig : (× [a : Nat][b : Bool])][asucc : Nat]) 66 ⇒ (tup [orig = rab][asucc = 1])) 67 68 (check-type (proj (proj ((inst f2poly (× [a : Nat][b : Bool])) rab) orig) b) 69 : Bool ⇒ #t) 70 71 ;; make sure inst still checks args 72 (typecheck-fail (inst (Λ ([X <: Nat]) 1) Int)) 73 74 ; ch28 75 (define f (Λ ([X <: (→ Nat Nat)]) (λ ([y : X]) (y 5)))) 76 (check-type f : (∀ ([X <: (→ Nat Nat)]) (→ X Nat))) 77 (check-type (inst f (→ Nat Nat)) : (→ (→ Nat Nat) Nat)) 78 (check-type (inst f (→ Int Nat)) : (→ (→ Int Nat) Nat)) 79 (typecheck-fail (inst f (→ Nat Int))) 80 (check-type ((inst f (→ Int Nat)) (λ ([z : Int]) 5)) : Nat) 81 (check-type ((inst f (→ Int Nat)) (λ ([z : Num]) 5)) : Nat) 82 (typecheck-fail ((inst f (→ Int Nat)) (λ ([z : Nat]) 5))) 83 84 85 ;; old sysf tests ------------------------------------------------------------- 86 ;; old syntax no longer valid 87 ;(check-type (Λ (X) (λ ([x : X]) x)) : (∀ (X) (→ X X))) 88 ; 89 ;(check-type (Λ (X) (λ ([t : X] [f : X]) t)) : (∀ (X) (→ X X X))) ; true 90 ;(check-type (Λ (X) (λ ([t : X] [f : X]) f)) : (∀ (X) (→ X X X))) ; false 91 ;(check-type (Λ (X) (λ ([t : X] [f : X]) f)) : (∀ (Y) (→ Y Y Y))) ; false, alpha equiv 92 ; 93 ;(check-type (Λ (t1) (Λ (t2) (λ ([x : t1]) (λ ([y : t2]) y)))) 94 ; : (∀ (t1) (∀ (t2) (→ t1 (→ t2 t2))))) 95 ; 96 ;(check-type (Λ (t1) (Λ (t2) (λ ([x : t1]) (λ ([y : t2]) y)))) 97 ; : (∀ (t3) (∀ (t4) (→ t3 (→ t4 t4))))) 98 ; 99 ;(check-not-type (Λ (t1) (Λ (t2) (λ ([x : t1]) (λ ([y : t2]) y)))) 100 ; : (∀ (t4) (∀ (t3) (→ t3 (→ t4 t4))))) 101 ; 102 ;(check-type (inst (Λ (t) (λ ([x : t]) x)) Int) : (→ Int Int)) 103 ;(check-type (inst (Λ (t) 1) (→ Int Int)) : Int) 104 ;; first inst should be discarded 105 ;(check-type (inst (inst (Λ (t) (Λ (t) (λ ([x : t]) x))) (→ Int Int)) Int) : (→ Int Int)) 106 ;; second inst is discarded 107 ;(check-type (inst (inst (Λ (t1) (Λ (t2) (λ ([x : t1]) x))) Int) (→ Int Int)) : (→ Int Int)) 108 ; 109 ;;;; polymorphic arguments 110 ;(check-type (Λ (t) (λ ([x : t]) x)) : (∀ (t) (→ t t))) 111 ;(check-type (Λ (t) (λ ([x : t]) x)) : (∀ (s) (→ s s))) 112 ;(check-type (Λ (s) (Λ (t) (λ ([x : t]) x))) : (∀ (s) (∀ (t) (→ t t)))) 113 ;(check-type (Λ (s) (Λ (t) (λ ([x : t]) x))) : (∀ (r) (∀ (t) (→ t t)))) 114 ;(check-type (Λ (s) (Λ (t) (λ ([x : t]) x))) : (∀ (r) (∀ (s) (→ s s)))) 115 ;(check-type (Λ (s) (Λ (t) (λ ([x : t]) x))) : (∀ (r) (∀ (u) (→ u u)))) 116 ;(check-type (λ ([x : (∀ (t) (→ t t))]) x) : (→ (∀ (s) (→ s s)) (∀ (u) (→ u u)))) 117 ;(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) (λ ([x : Int]) x))) 118 ;(typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) 1)) 119 ;(check-type ((λ ([x : (∀ (t) (→ t t))]) x) (Λ (s) (λ ([y : s]) y))) : (∀ (u) (→ u u))) 120 ;(check-type 121 ; (inst ((λ ([x : (∀ (t) (→ t t))]) x) (Λ (s) (λ ([y : s]) y))) Int) : (→ Int Int)) 122 ;(check-type 123 ; ((inst ((λ ([x : (∀ (t) (→ t t))]) x) (Λ (s) (λ ([y : s]) y))) Int) 10) 124 ; : Int ⇒ 10) 125 ;(check-type (λ ([x : (∀ (t) (→ t t))]) (inst x Int)) : (→ (∀ (t) (→ t t)) (→ Int Int))) 126 ;(check-type (λ ([x : (∀ (t) (→ t t))]) ((inst x Int) 10)) : (→ (∀ (t) (→ t t)) Int)) 127 ;(check-type ((λ ([x : (∀ (t) (→ t t))]) ((inst x Int) 10)) 128 ; (Λ (s) (λ ([y : s]) y))) 129 ; : Int ⇒ 10) 130 131 132 ;;; previous tests ------------------------------------------------------------- 133 (check-type 1 : Int) 134 (check-not-type 1 : (→ Int Int)) 135 ;; strings and boolean literals now ok 136 ;(typecheck-fail "one") ; unsupported literal 137 ;(typecheck-fail #f) ; unsupported literal 138 (check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int)) 139 (check-not-type (λ ([x : Int]) x) : Int) 140 (check-type (λ ([x : Int]) x) : (→ Int Int)) 141 (check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int)) 142 (check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1) 143 (typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool is not valid type 144 ;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is not valid type 145 (typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type 146 (check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) 147 : (→ (→ Int Int Int) Int Int Int)) 148 ;; edited from sysf test to handle subtyping 149 (check-type ((λ ([f : (→ Nat Nat Nat)] [x : Nat] [y : Nat]) (f x y)) + 1 2) : Num ⇒ 3) 150 (typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int 151 (typecheck-fail (λ ([x : (→ Int Int)]) (+ x x))) ; x should be Int 152 (typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args 153 (check-type ((λ ([x : Nat]) (+ x x)) 10) : Num ⇒ 20)