www

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

fabul-tests.rkt (2430B)

      1 #lang s-exp turnstile/examples/linear/fabul
      2 (require turnstile/rackunit-typechecking)
      3 
      4 (%U (define birthday : (× Int Int Int)
      5      (tup 10 10 97)))
      6 
      7 (%U (check-type birthday : (× Int Int Int)))
      8 (%L (check-type (%U birthday) : (⊗ Int Int Int) ⇒ (tup 10 10 97)))
      9 
     10 (%U (typecheck-fail
     11     (%L (let ([bday (%U birthday)]) 0))
     12     #:with-msg "bday: linear variable unused"))
     13 
     14 (%L (typecheck-fail
     15     (let ([x (%U birthday)]) (%U x))
     16     #:with-msg "x: cannot use linear variable from unrestricted language"))
     17 
     18 (%L (check-type (let ([bday (%U birthday)])
     19                   (%U (%L bday)))
     20                : (⊗ Int Int Int)))
     21 
     22 (%L (check-type (%U (cons 1 (cons 2 (nil {Int}))))
     23                : (MList Int)
     24                ⇒ (cons 1 (cons 2 (nil)))))
     25 
     26 (%U (check-type (%L (cons 1 (cons 2 (nil))))
     27                : (List Int)
     28                ⇒ (cons 1 (cons 2 (nil {Int})))))
     29 
     30 (%L (check-type (let ([f (%U (λ () (cons 1 (nil {Int}))))]) f)
     31                : (→ (MList Int))))
     32 
     33 (%L (check-type (let ([f (%U (λ () (cons 1 (nil {Int}))))]) (f))
     34                : (MList Int)
     35                ⇒ (cons 1 (nil))))
     36 
     37 
     38 
     39 (%L (define (partition [pred : (→ Int Bool)]
     40                       [lst : (MList Int)]) (⊗ (MList Int) (MList Int))
     41      (match-list lst
     42        [(cons x xs @ l)
     43         (let* ([(yes no) (partition pred xs)])
     44           (if (pred x)
     45               (tup (cons x yes @ l) no)
     46               (tup yes (cons x no @ l))))]
     47        [(nil)
     48         (tup (nil {Int}) (nil {Int}))])))
     49 
     50 (%L (check-type (partition (λ (n) (< n 3))
     51                           (cons 1 (cons 2 (cons 4 (cons 5 (nil))))))
     52                : (⊗ (MList Int) (MList Int))
     53                ⇒ (tup (cons 1 (cons 2 (nil)))
     54                       (cons 4 (cons 5 (nil))))))
     55 
     56 
     57 (%L (define (mqsort [lst : (MList Int)] [acc : (MList Int)]) (MList Int)
     58      (match-list lst
     59        [(cons piv xs @ l)
     60         (let* ([(lt gt) (partition (λ (x) (< x piv)) xs)])
     61           (mqsort lt (cons piv (mqsort gt acc) @ l)))]
     62        [(nil) acc])))
     63 
     64 (%L (check-type (mqsort (cons 4 (cons 7 (cons 2 (cons 1 (nil))))) (nil))
     65                : (MList Int)
     66                ⇒ (cons 1 (cons 2 (cons 4 (cons 7 (nil)))))))
     67 
     68 
     69 
     70 (%U (define (qsort [lst : (List Int)]) (List Int)
     71      (%L (mqsort (%U lst) (nil)))))
     72 
     73 (%U (check-type (qsort (cons 4 (cons 7 (cons 2 (cons 1 (nil {Int}))))))
     74                : (List Int)
     75                ⇒ (cons 1 (cons 2 (cons 4 (cons 7 (nil {Int})))))))