www

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

lin+var-tests.rkt (2654B)

      1 #lang s-exp turnstile/examples/linear/lin+var
      2 (require turnstile/rackunit-typechecking)
      3 
      4 (check-type (var [left 3]) : (⊕ [left Int] [right String]))
      5 (check-type (var [right "a"]) : (⊕ [left Int] [right String]))
      6 
      7 (typecheck-fail (var [left 3] as (⊕ [yes] [no]))
      8                 #:with-msg "type \\(⊕ \\(yes\\) \\(no\\)\\) does not have variant named 'left'")
      9 
     10 (typecheck-fail (var [left 3] as (⊕ [left Int Int] [right String]))
     11                 #:with-msg "wrong number of arguments to variant: expected 2, got 1")
     12 
     13 (define-type-alias (Either A B) (⊕ [left A] [right B]))
     14 (define-type-alias (Option A) (⊕ [some A] [none]))
     15 
     16 (typecheck-fail (var [middle 3] as (Either Int Float))
     17                 #:with-msg "type \\(Either Int Float\\) does not have variant named 'middle'")
     18 
     19 (check-type (λ (x) x) : (→ (Either Int Float) (Either Int Float)))
     20 (check-type (λ (x) x) : (→ (Either Int Float) (⊕ [left Int] [right Float])))
     21 
     22 (typecheck-fail (let ([x (var [left 3] as (Either Int Int))]) 0)
     23                 #:with-msg "x: linear variable unused")
     24 
     25 (check-type (match (var [left 3] as (Either Int Int))
     26               [(left x) x]
     27               [(right y) (+ y 1)])
     28             : Int ⇒ 3)
     29 
     30 (check-type (match (var [right 5] as (Either Int Int))
     31               [(left x) x]
     32               [(right y) (+ y 1)])
     33             : Int ⇒ 6)
     34 
     35 (typecheck-fail (match (var [left 3] as (Either Int (-o Int Int)))
     36                   [(left x) x]
     37                   [(right f) 0])
     38                 #:with-msg "f: linear variable unused")
     39 
     40 (check-type (match (var [right (λ (x) (+ x x))] as (Either Int (-o Int Int)))
     41               [(left x) x]
     42               [(right f) (f 2)])
     43             : Int ⇒ 4)
     44 
     45 (typecheck-fail (match (var [left 0] as (Either Int String))
     46                   [(left x) x]
     47                   [(right y) y])
     48                 #:with-msg "branches have incompatible types: Int and String")
     49 
     50 (typecheck-fail (match (var [some ()] as (Option Unit))
     51                   [(left x) x]
     52                   [(right y) y])
     53                 #:with-msg "type \\(Option Unit\\) does not have variant named 'left'")
     54 (%%reset-linear-mode)
     55 
     56 (typecheck-fail (match (var [left 0] as (Either Int Int))
     57                   [(left x) x]
     58                   [(right y z) y])
     59                 #:with-msg "wrong number of arguments to variant: expected 1, got 2")
     60 (%%reset-linear-mode)
     61 
     62 (typecheck-fail (let ([f (λ ([x : Int]) x)])
     63                   (match (var [left 0] as (Either Int Int))
     64                     [(left x) (f x)]
     65                     [(right y) y]))
     66                 #:with-msg "f: linear variable may be unused in certain branches")
     67 (%%reset-linear-mode)