sysf-tests.rkt (3771B)
1 #lang s-exp "../sysf.rkt" 2 (require "rackunit-typechecking.rkt") 3 4 (check-type (Λ (X) (λ ([x : X]) x)) : (∀ (X) (→ X X))) 5 6 (check-type (Λ (X) (λ ([t : X] [f : X]) t)) : (∀ (X) (→ X X X))) ; true 7 (check-type (Λ (X) (λ ([t : X] [f : X]) f)) : (∀ (X) (→ X X X))) ; false 8 (check-type (Λ (X) (λ ([t : X] [f : X]) f)) : (∀ (Y) (→ Y Y Y))) ; false, alpha equiv 9 10 (check-type (Λ (t1) (Λ (t2) (λ ([x : t1]) (λ ([y : t2]) y)))) 11 : (∀ (t1) (∀ (t2) (→ t1 (→ t2 t2))))) 12 13 (check-type (Λ (t1) (Λ (t2) (λ ([x : t1]) (λ ([y : t2]) y)))) 14 : (∀ (t3) (∀ (t4) (→ t3 (→ t4 t4))))) 15 16 (check-not-type (Λ (t1) (Λ (t2) (λ ([x : t1]) (λ ([y : t2]) y)))) 17 : (∀ (t4) (∀ (t3) (→ t3 (→ t4 t4))))) 18 19 (check-type (inst (Λ (t) (λ ([x : t]) x)) Int) : (→ Int Int)) 20 (check-type (inst (Λ (t) 1) (→ Int Int)) : Int) 21 ; first inst should be discarded 22 (check-type (inst (inst (Λ (t) (Λ (t) (λ ([x : t]) x))) (→ Int Int)) Int) : (→ Int Int)) 23 ; second inst is discarded 24 (check-type (inst (inst (Λ (t1) (Λ (t2) (λ ([x : t1]) x))) Int) (→ Int Int)) : (→ Int Int)) 25 26 ;; inst err 27 (typecheck-fail 28 (inst 1 Int) 29 #:with-msg 30 "Expected ∀ type, got: Int") 31 32 ;; polymorphic arguments 33 (check-type (Λ (t) (λ ([x : t]) x)) : (∀ (t) (→ t t))) 34 (check-type (Λ (t) (λ ([x : t]) x)) : (∀ (s) (→ s s))) 35 (check-type (Λ (s) (Λ (t) (λ ([x : t]) x))) : (∀ (s) (∀ (t) (→ t t)))) 36 (check-type (Λ (s) (Λ (t) (λ ([x : t]) x))) : (∀ (r) (∀ (t) (→ t t)))) 37 (check-type (Λ (s) (Λ (t) (λ ([x : t]) x))) : (∀ (r) (∀ (s) (→ s s)))) 38 (check-type (Λ (s) (Λ (t) (λ ([x : t]) x))) : (∀ (r) (∀ (u) (→ u u)))) 39 (check-type (λ ([x : (∀ (t) (→ t t))]) x) : (→ (∀ (s) (→ s s)) (∀ (u) (→ u u)))) 40 (typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) (λ ([x : Int]) x))) 41 (typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) 1)) 42 (check-type ((λ ([x : (∀ (t) (→ t t))]) x) (Λ (s) (λ ([y : s]) y))) : (∀ (u) (→ u u))) 43 (check-type 44 (inst ((λ ([x : (∀ (t) (→ t t))]) x) (Λ (s) (λ ([y : s]) y))) Int) : (→ Int Int)) 45 (check-type 46 ((inst ((λ ([x : (∀ (t) (→ t t))]) x) (Λ (s) (λ ([y : s]) y))) Int) 10) 47 : Int ⇒ 10) 48 (check-type (λ ([x : (∀ (t) (→ t t))]) (inst x Int)) : (→ (∀ (t) (→ t t)) (→ Int Int))) 49 (check-type (λ ([x : (∀ (t) (→ t t))]) ((inst x Int) 10)) : (→ (∀ (t) (→ t t)) Int)) 50 (check-type ((λ ([x : (∀ (t) (→ t t))]) ((inst x Int) 10)) 51 (Λ (s) (λ ([y : s]) y))) 52 : Int ⇒ 10) 53 54 ; ∀ errs 55 (typecheck-fail (λ ([x : (∀ (y) (+ 1 y))]) x)) 56 57 ;; previous tests ------------------------------------------------------------- 58 (check-type 1 : Int) 59 (check-not-type 1 : (→ Int Int)) 60 (typecheck-fail "one") ; unsupported literal 61 (typecheck-fail #f) ; unsupported literal 62 (check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int)) 63 (check-not-type (λ ([x : Int]) x) : Int) 64 (check-type (λ ([x : Int]) x) : (→ Int Int)) 65 (check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int)) 66 (check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1) 67 (typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool is not valid type 68 (typecheck-fail (λ ([x : Bool]) x)) ; Bool is not valid type 69 (typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type 70 (check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) 71 : (→ (→ Int Int Int) Int Int Int)) 72 (check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3) 73 (typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int 74 (typecheck-fail (λ ([x : (→ Int Int)]) (+ x x))) ; x should be Int 75 (typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args 76 (check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)