lin-tests.rkt (2459B)
1 #lang s-exp turnstile/examples/linear/lin 2 (require turnstile/rackunit-typechecking 3 (only-in racket/base quote)) 4 5 (check-type #t : Bool) 6 (check-type 4 : Int) 7 (check-type () : Unit) 8 9 (check-type (let ([x 3] [y 4]) y) : Int -> 4) 10 11 (check-type (if #t 1 2) : Int -> 1) 12 (typecheck-fail (if 1 2 3) 13 #:with-msg "expected Bool, given Int") 14 (typecheck-fail (if #t 2 ()) 15 #:with-msg "branches have incompatible types: Int and Unit") 16 (%%reset-linear-mode) 17 18 (check-type (λ ([x : Int]) x) : (-o Int Int)) 19 (check-type (λ ! ([x : Int]) x) : (→ Int Int)) 20 (check-type (λ (x) x) : (-o String String)) 21 (check-type (λ (x) x) : (→ String String)) 22 23 (check-type + : (→ Int Int Int)) 24 (check-type (+ 1 2) : Int -> 3) 25 (check-type ((λ ([x : Int]) (+ x 1)) 4) : Int -> 5) 26 27 28 (typecheck-fail (λ ([p : (-o Int Bool)]) 0) 29 #:with-msg "p: linear variable unused") 30 31 (typecheck-fail (let ([f (λ ([x : Int]) x)]) 32 0) 33 #:with-msg "f: linear variable unused") 34 35 (typecheck-fail (let ([f (λ ([x : Int]) x)]) 36 (f (f 3))) 37 #:with-msg "f: linear variable used more than once") 38 39 (typecheck-fail (let ([f (λ ([x : Int]) x)]) 40 (if #t 41 (f 3) 42 4)) 43 #:with-msg "f: linear variable may be unused in certain branches") 44 45 (typecheck-fail (let ([f (λ ([x : Int]) x)]) 46 (λ ! ([x : Int]) f)) 47 #:with-msg "f: linear variable may not be used by unrestricted function") 48 (%%reset-linear-mode) 49 50 (check-type (let ([twice (λ ! ([x : Int]) (+ x x))]) 51 (+ (twice 8) 52 (twice 9))) 53 : Int -> 34) 54 55 (check-type (let ([f (λ ([x : Int]) #t)]) 56 (begin (drop f) 57 3)) 58 : Int -> 3) 59 60 (check-type (letrec ([{<= : (→ Int Int Bool)} 61 (λ (n m) 62 (if (zero? n) 63 #t 64 (if (zero? m) 65 #f 66 (<= (sub1 n) (sub1 m)))))]) 67 (if (<= 4 1) 999 68 (if (<= 3 3) 69 0 70 888))) 71 : Int -> 0) 72 73 (typecheck-fail (letrec ([{f : (-o Int Int)} 74 (λ (x) (f x))]) 75 (f 3)) 76 #:with-msg "may not bind linear type \\(-o Int Int\\) in letrec")