www

Unnamed repository; edit this file 'description' to name the repository.
Log | Files | Refs | README

lin+tup-tests.rkt (1191B)

      1 #lang s-exp turnstile/examples/linear/lin+tup
      2 
      3 (require turnstile/rackunit-typechecking
      4          (only-in racket/base quote))
      5 
      6 (check-type (tup 1 #t) : (⊗ Int Bool) -> '(1 #t))
      7 (check-type (tup 1 2 3) : (⊗ Int Int Int) -> '(1 2 3))
      8 
      9 (check-type (let ([p (tup 1 2)]) p) : (⊗ Int Int) -> '(1 2))
     10 (typecheck-fail (let ([p (tup 1 2)]) ())
     11                 #:with-msg "p: linear variable unused")
     12 (typecheck-fail (let ([p (tup 1 2)]) (tup p p))
     13                 #:with-msg "p: linear variable used more than once")
     14 
     15 (check-type (let ([p (tup 1 ())]) (if #t p p)) : (⊗ Int Unit))
     16 (typecheck-fail (let ([p (tup 1 ())]) (if #t p (tup 2 ())))
     17                 #:with-msg "linear variable may be unused in certain branches")
     18 
     19 (check-type (λ ([x : Int]) (tup x x)) : (-o Int (⊗ Int Int)))
     20 (typecheck-fail (λ ([x : (⊗ Int Int)]) ())
     21                 #:with-msg "x: linear variable unused")
     22 
     23 (check-type (let ([p (tup 1 2)]) (λ ([x : Int]) p))
     24             : (-o Int (⊗ Int Int)))
     25 
     26 (check-type (let* ([x 3] [y x]) y) : Int -> 3)
     27 (check-type (let* ([(x y) (tup 1 #f)]) x) : Int -> 1)
     28 (typecheck-fail (let* ([(x y) (tup (tup 1 2) 3)]) y)
     29                 #:with-msg "x: linear variable unused")