Milo Turner
Stephen Chang
parent
3ea1f05c51
commit
5d412504fb
|
|
@ -1,184 +0,0 @@
|
|||
#lang turnstile
|
||||
(extends "ext-stlc.rkt"
|
||||
#:except
|
||||
define-type-alias
|
||||
define if begin let let* letrec λ #%app
|
||||
⊔ zero? = add1 sub1 not void +)
|
||||
|
||||
(provide (for-syntax current-linear?
|
||||
linear-scope
|
||||
linear-var-in-scope?
|
||||
use-linear-var!)
|
||||
|
||||
(type-out Unit Int String Bool -o ⊗ !!)
|
||||
#%top-interaction #%module-begin require only-in
|
||||
begin tup let λ #%app if
|
||||
(rename-out [λ lambda])
|
||||
|
||||
(typed-out [+ : (!! (-o Int Int Int))]
|
||||
[< : (!! (-o Int Int Bool))]
|
||||
[displayln : (!! (-o String Unit))]))
|
||||
|
||||
|
||||
(define-type-constructor -o #:arity >= 1)
|
||||
(define-type-constructor ⊗ #:arity = 2)
|
||||
(define-type-constructor !! #:arity = 1)
|
||||
|
||||
|
||||
(begin-for-syntax
|
||||
(require syntax/id-set)
|
||||
(define (sym-diff s0 . ss)
|
||||
(for*/fold ([s0 s0])
|
||||
([s (in-list ss)]
|
||||
[x (in-set s)])
|
||||
(if (set-member? s0 x)
|
||||
(set-remove s0 x)
|
||||
(set-add s0 x))))
|
||||
|
||||
|
||||
(define (fail/multiple-use x)
|
||||
(raise-syntax-error #f "linear variable used more than once" x))
|
||||
(define (fail/unused x)
|
||||
(raise-syntax-error #f "linear variable unused" x))
|
||||
(define (fail/unbalanced-branches x)
|
||||
(raise-syntax-error #f "linear variable may be unused in certain branches" x))
|
||||
(define (fail/unrestricted-fn x)
|
||||
(raise-syntax-error #f "linear variable may not be used by unrestricted function" x))
|
||||
|
||||
|
||||
; current-linear : (Parameter (TypeStx -> Bool))
|
||||
(define current-linear?
|
||||
(make-parameter (or/c -o? ⊗?)))
|
||||
|
||||
; linear-type? : TypeStx -> Bool
|
||||
(define (linear-type? t)
|
||||
((current-linear?) t))
|
||||
|
||||
; unrestricted-type? : TypeStx -> Bool
|
||||
(define (unrestricted-type? t)
|
||||
(not (linear-type? t)))
|
||||
|
||||
|
||||
; linear-scope : FreeIdSet
|
||||
; holds a list of all linear variables that have been used.
|
||||
(define linear-scope
|
||||
(immutable-free-id-set))
|
||||
|
||||
; linear-var-in-scope? : Id -> Bool
|
||||
(define (linear-var-in-scope? x)
|
||||
(not (set-member? linear-scope x)))
|
||||
|
||||
; use-linear-var! : Id -> Void
|
||||
(define (use-linear-var! x #:fail [fail fail/multiple-use])
|
||||
(unless (linear-var-in-scope? x)
|
||||
(fail x))
|
||||
(set! linear-scope (set-add linear-scope x)))
|
||||
|
||||
; pop-linear-scope! : StxList -> Void
|
||||
; drops from scope the linear variables in the given context
|
||||
; ignores unrestricted types in the context, but checks that
|
||||
; variables with linear types must be used already.
|
||||
; the context is a syntax list of the form #'([x τ] ...)
|
||||
(define (pop-linear-scope! ctx #:fail [fail fail/unused])
|
||||
(syntax-parse ctx
|
||||
[([X T] ...)
|
||||
(for ([x (in-syntax #'[X ...])]
|
||||
[t (in-syntax #'[T ...])])
|
||||
(when (and (linear-type? t)
|
||||
(linear-var-in-scope? x))
|
||||
(fail x)))]))
|
||||
|
||||
; merge-linear-scope! : FreeIdSet -> Void
|
||||
; ensure that the current scope and the given scope are compatible,
|
||||
; e.g. when unifying the branches in a conditional
|
||||
(define (merge-linear-scope! merge-scope #:fail [fail fail/unbalanced-branches])
|
||||
(for ([x (in-set (sym-diff linear-scope
|
||||
merge-scope))])
|
||||
(fail x)))
|
||||
|
||||
)
|
||||
|
||||
|
||||
(define-typed-variable-syntax
|
||||
#:datum-literals [:]
|
||||
[(_ x- : σ) ≫ ; record use when σ restricted
|
||||
#:do [(unless (unrestricted-type? #'σ)
|
||||
(use-linear-var! #'x-))]
|
||||
--------
|
||||
[⊢ x- ⇒ σ]])
|
||||
|
||||
|
||||
(define-typed-syntax begin
|
||||
[(_ e ... e0) ≫
|
||||
[⊢ [e ≫ e- ⇒ _] ... [e0 ≫ e0- ⇒ σ]]
|
||||
--------
|
||||
[⊢ (begin- e- ... e0-) ⇒ σ]])
|
||||
|
||||
|
||||
(define-typed-syntax tup
|
||||
[(_ e1 e2) ≫
|
||||
[⊢ e1 ≫ e1- ⇒ σ1]
|
||||
[⊢ e2 ≫ e2- ⇒ σ2]
|
||||
--------
|
||||
[⊢ (#%app- list- e1- e2-) ⇒ (⊗ σ1 σ2)]])
|
||||
|
||||
|
||||
(define-typed-syntax let
|
||||
[(let ([x rhs] ...) e) ≫
|
||||
[⊢ [rhs ≫ rhs- ⇒ σ] ...]
|
||||
[[x ≫ x- : σ] ... ⊢ e ≫ e- ⇒ σ_out]
|
||||
#:do [(pop-linear-scope! #'([x- σ] ...))]
|
||||
--------
|
||||
[⊢ (let- ([x- rhs-] ...) e-) ⇒ σ_out]])
|
||||
|
||||
|
||||
(define-typed-syntax λ
|
||||
#:datum-literals (: !)
|
||||
; linear function
|
||||
[(λ ([x:id : T:type] ...) e) ≫
|
||||
#:with (σ ...) #'(T.norm ...)
|
||||
[[x ≫ x- : σ] ... ⊢ e ≫ e- ⇒ σ_out]
|
||||
#:do [(pop-linear-scope! #'([x- σ] ...))]
|
||||
--------
|
||||
[⊢ (λ- (x- ...) e-) ⇒ (-o σ ... σ_out)]]
|
||||
|
||||
; unrestricted function
|
||||
[(λ ! ([x:id : T:type] ...) e) ≫
|
||||
#:with (σ ...) #'(T.norm ...)
|
||||
#:do [(define scope-prev linear-scope)]
|
||||
[[x ≫ x- : σ] ... ⊢ e ≫ e- ⇒ σ_out]
|
||||
#:do [(pop-linear-scope! #'([x- σ] ...))
|
||||
(merge-linear-scope! scope-prev
|
||||
#:fail fail/unrestricted-fn)]
|
||||
--------
|
||||
[⊢ (λ- (x- ...) e-) ⇒ (!! (-o σ ... σ_out))]])
|
||||
|
||||
|
||||
(define-typed-syntax #%app
|
||||
[(_) ≫
|
||||
--------
|
||||
[⊢ (#%app- void-) ⇒ Unit]]
|
||||
|
||||
[(#%app fun arg ...) ≫
|
||||
[⊢ fun ≫ fun- ⇒ σ_fun]
|
||||
#:with (~or (~-o σ_in ... σ_out)
|
||||
(~!! (~-o σ_in ... σ_out))
|
||||
(~post (~fail "expected linear function type")))
|
||||
#'σ_fun
|
||||
[⊢ [arg ≫ arg- ⇐ σ_in] ...]
|
||||
--------
|
||||
[⊢ (#%app- fun- arg- ...) ⇒ σ_out]])
|
||||
|
||||
|
||||
(define-typed-syntax if
|
||||
[(if c e1 e2) ≫
|
||||
[⊢ c ≫ c- ⇐ Bool]
|
||||
#:do [(define scope-pre-branch linear-scope)]
|
||||
[⊢ e1 ≫ e1- ⇒ σ]
|
||||
#:do [(define scope-then linear-scope)
|
||||
(set! linear-scope scope-pre-branch)]
|
||||
[⊢ e2 ≫ e2- ⇐ σ]
|
||||
#:do [(merge-linear-scope! scope-then
|
||||
#:fail fail/unbalanced-branches)]
|
||||
--------
|
||||
[⊢ (if- c- e1- e2-) ⇒ σ]])
|
||||
61
turnstile/examples/linear/lin+chan.rkt
Normal file
61
turnstile/examples/linear/lin+chan.rkt
Normal file
|
|
@ -0,0 +1,61 @@
|
|||
#lang turnstile/lang
|
||||
(extends "lin+tup.rkt")
|
||||
|
||||
(provide (type-out InChan OutChan)
|
||||
make-channel channel-put channel-get
|
||||
thread sleep)
|
||||
|
||||
(define-type-constructor InChan #:arity = 1)
|
||||
(define-type-constructor OutChan #:arity = 1)
|
||||
|
||||
(begin-for-syntax
|
||||
(current-linear-type? (or/c InChan? (current-linear-type?))))
|
||||
|
||||
|
||||
(define-typed-syntax make-channel
|
||||
[(_ {ty:type}) ≫
|
||||
#:with σ #'ty.norm
|
||||
#:with tmp (generate-temporary)
|
||||
--------
|
||||
[⊢ (let ([tmp (#%app- make-channel-)])
|
||||
(list tmp tmp))
|
||||
⇒ (⊗ (InChan σ) (OutChan σ))]])
|
||||
|
||||
|
||||
(define-typed-syntax channel-put
|
||||
[(_ ch e) ≫
|
||||
[⊢ ch ≫ ch- ⇒ (~OutChan σ)]
|
||||
[⊢ e ≫ e- ⇐ σ]
|
||||
--------
|
||||
[⊢ (channel-put- ch- e-) ⇒ Unit]])
|
||||
|
||||
|
||||
(define-typed-syntax channel-get
|
||||
[(_ ch) ≫
|
||||
[⊢ ch ≫ ch- ⇒ (~InChan σ)]
|
||||
#:with tmp (generate-temporary #'ch)
|
||||
--------
|
||||
[⊢ (let ([tmp ch-])
|
||||
(list tmp (channel-get- tmp)))
|
||||
⇒ (⊗ (InChan σ) σ)]])
|
||||
|
||||
|
||||
(define-typed-syntax thread
|
||||
[(_ f) ≫
|
||||
[⊢ f ≫ f- ⇒ (~-o _)]
|
||||
--------
|
||||
[⊢ (void (thread- f-)) ⇒ Unit]])
|
||||
|
||||
|
||||
(define-typed-syntax sleep
|
||||
[(_) ≫
|
||||
--------
|
||||
[⊢ (sleep-) ⇒ Unit]]
|
||||
|
||||
[(_ e) ≫
|
||||
[⊢ e ≫ e- ⇒ σ]
|
||||
#:fail-unless (or (Int? #'σ)
|
||||
(Float? #'σ))
|
||||
"invalid sleep time, expected Int or Float"
|
||||
--------
|
||||
[⊢ (sleep- e-) ⇒ Unit]])
|
||||
80
turnstile/examples/linear/lin+cons.rkt
Normal file
80
turnstile/examples/linear/lin+cons.rkt
Normal file
|
|
@ -0,0 +1,80 @@
|
|||
#lang turnstile/lang
|
||||
(extends "lin+tup.rkt")
|
||||
|
||||
(provide (type-out MList MList0)
|
||||
cons nil match-list)
|
||||
|
||||
(define-type-constructor MList #:arity = 1)
|
||||
(define-base-type MList0)
|
||||
|
||||
(begin-for-syntax
|
||||
(current-linear-type? (or/c MList? MList0? (current-linear-type?))))
|
||||
|
||||
|
||||
(define-typed-syntax cons
|
||||
#:datum-literals (@)
|
||||
|
||||
; implicit memory location created
|
||||
[(_ e e_rest) ≫
|
||||
[⊢ e ≫ e- ⇒ σ]
|
||||
[⊢ e_rest ≫ e_rest- ⇐ (MList σ)]
|
||||
--------
|
||||
[⊢ (#%app- mcons- e- e_rest-) ⇒ (MList σ)]]
|
||||
|
||||
; with memory location given
|
||||
[(_ e e_rest @ e_loc) ≫
|
||||
[⊢ e ≫ e- ⇒ σ]
|
||||
[⊢ e_rest ≫ e_rest- ⇐ (MList σ)]
|
||||
[⊢ e_loc ≫ e_loc- ⇐ MList0]
|
||||
#:with tmp (generate-temporary #'e_loc)
|
||||
--------
|
||||
[⊢ (let- ([tmp e_loc-])
|
||||
(set-mcar!- tmp e-)
|
||||
(set-mcdr!- tmp e_rest-)
|
||||
tmp)
|
||||
⇒ (MList σ)]])
|
||||
|
||||
|
||||
(define-typed-syntax nil
|
||||
[(_ {ty:type}) ≫
|
||||
--------
|
||||
[⊢ '() ⇒ (MList ty.norm)]]
|
||||
[(_) ⇐ (~MList σ) ≫
|
||||
--------
|
||||
[⊢ '()]])
|
||||
|
||||
|
||||
(define-typed-syntax match-list
|
||||
#:datum-literals (cons nil @)
|
||||
[(_ e_list
|
||||
(~or [(cons x+:id xs+:id @ l+:id) e_cons+]
|
||||
[(nil) e_nil+]) ...) ≫
|
||||
#:with [(l x xs e_cons)] #'[(l+ x+ xs+ e_cons+) ...]
|
||||
#:with [e_nil] #'[e_nil+ ...]
|
||||
|
||||
; list
|
||||
[⊢ e_list ≫ e_list- ⇒ (~MList σ)]
|
||||
#:with σ_xs ((current-type-eval) #'(MList σ))
|
||||
#:with σ_l ((current-type-eval) #'MList0)
|
||||
|
||||
#:mode (make-linear-branch-mode 2)
|
||||
(; cons branch
|
||||
#:submode (branch-nth 0)
|
||||
([[x ≫ x- : σ]
|
||||
[xs ≫ xs- : σ_xs]
|
||||
[l ≫ l- : σ_l]
|
||||
⊢ e_cons ≫ e_cons- ⇒ σ_out]
|
||||
#:do [(linear-out-of-scope! #'([x- : σ] [xs- : σ_xs] [l- : σ_l]))])
|
||||
|
||||
; nil branch
|
||||
#:submode (branch-nth 1)
|
||||
([⊢ [e_nil ≫ e_nil- ⇐ σ_out]]))
|
||||
|
||||
--------
|
||||
[⊢ (let- ([l- e_list-])
|
||||
(if- (null? l-)
|
||||
e_nil-
|
||||
(let- ([x- (mcar- l-)]
|
||||
[xs- (mcdr- l-)])
|
||||
e_cons-)))
|
||||
⇒ σ_out]])
|
||||
112
turnstile/examples/linear/lin+tup.rkt
Normal file
112
turnstile/examples/linear/lin+tup.rkt
Normal file
|
|
@ -0,0 +1,112 @@
|
|||
#lang turnstile/lang
|
||||
(extends "lin.rkt")
|
||||
|
||||
(provide (type-out ⊗) tup let*)
|
||||
(begin-for-syntax (provide in-cad*rs
|
||||
list-destructure-syntax))
|
||||
|
||||
(define-type-constructor ⊗ #:arity >= 2)
|
||||
|
||||
(begin-for-syntax
|
||||
(define (num-tuple-fail-msg σs xs)
|
||||
(format "wrong number of tuple elements: expected ~a, got ~a"
|
||||
(stx-length xs)
|
||||
(stx-length σs)))
|
||||
|
||||
(current-linear-type? (or/c ⊗? (current-linear-type?))))
|
||||
|
||||
|
||||
(define-typed-syntax tup
|
||||
[(_ e1 e2 ...+) ≫
|
||||
[⊢ e1 ≫ e1- ⇒ σ1]
|
||||
[⊢ e2 ≫ e2- ⇒ σ2] ...
|
||||
--------
|
||||
[⊢ (list- e1- e2- ...) ⇒ (⊗ σ1 σ2 ...)]])
|
||||
|
||||
|
||||
(define-typed-syntax let*
|
||||
; normal let* recursive bindings
|
||||
[(_ ([x:id e_rhs] . xs) . body) ≫
|
||||
[⊢ e_rhs ≫ e_rhs- ⇒ σ]
|
||||
[[x ≫ x- : σ] ⊢ (let* xs . body) ≫ e_body- ⇒ σ_out]
|
||||
#:do [(linear-out-of-scope! #'([x- : σ]))]
|
||||
--------
|
||||
[⊢ (let- ([x- e_rhs-]) e_body-) ⇒ σ_out]]
|
||||
|
||||
; tuple unpacking with (let* ([(x ...) tup]) ...)
|
||||
[(_ ([(x:id ...) e_rhs] . xs) . body) ≫
|
||||
[⊢ e_rhs ≫ e_rhs- ⇒ (~⊗ σ ...)]
|
||||
#:fail-unless (stx-length=? #'[σ ...] #'[x ...])
|
||||
(num-tuple-fail-msg #'[σ ...] #'[x ...])
|
||||
|
||||
[[x ≫ x- : σ] ... ⊢ (let* xs . body) ≫ e_body- ⇒ σ_out]
|
||||
#:do [(linear-out-of-scope! #'([x- : σ] ...))]
|
||||
|
||||
#:with tmp (generate-temporary #'e_tup)
|
||||
#:with destr (list-destructure-syntax #'[x- ...] #'tmp #:unsafe? #t
|
||||
#'e_body-)
|
||||
--------
|
||||
[⊢ (let- ([tmp e_rhs-]) destr) ⇒ σ_out]]
|
||||
|
||||
[(_ () e) ≫
|
||||
--------
|
||||
[≻ e]]
|
||||
|
||||
[(_ () e ...+) ≫
|
||||
--------
|
||||
[≻ (lin:begin e ...)]])
|
||||
|
||||
|
||||
|
||||
(require racket/unsafe/ops)
|
||||
|
||||
;; generate infinite sequence of cad*r syntax, e.g.
|
||||
;; (car e) (cadr e) (caddr e) ...
|
||||
(define-for-syntax (in-cad*rs e #:unsafe? [unsafe? #f])
|
||||
(make-do-sequence
|
||||
(λ ()
|
||||
(values (λ (s)
|
||||
(if unsafe?
|
||||
(quasisyntax/loc e (unsafe-car #,s))
|
||||
(quasisyntax/loc e (car #,s))))
|
||||
(λ (s)
|
||||
(if unsafe?
|
||||
(quasisyntax/loc e (unsafe-cdr #,s))
|
||||
(quasisyntax/loc e (cdr #,s))))
|
||||
e
|
||||
#f #f #f))))
|
||||
|
||||
|
||||
;; (list-destructure-syntax #'(x y z ...) #'rhs #'body)
|
||||
;; =
|
||||
;; (let ([x (car rhs)]
|
||||
;; [y (cadr rhs)]
|
||||
;; [z (caddr rhs)]
|
||||
;; ...)
|
||||
;; body)
|
||||
(define-for-syntax (list-destructure-syntax xs rhs body #:unsafe? [unsafe? #f])
|
||||
(with-syntax ([binds (for/list ([c (in-cad*rs rhs #:unsafe? unsafe?)]
|
||||
[x (in-syntax xs)])
|
||||
(list x c))]
|
||||
[body body])
|
||||
(syntax/loc rhs
|
||||
(let- binds body))))
|
||||
|
||||
|
||||
|
||||
(module+ test
|
||||
(begin-for-syntax
|
||||
(require rackunit)
|
||||
(check-equal? (for/list ([c (in-cad*rs #'x)]
|
||||
[i (in-range 4)])
|
||||
(syntax->datum c))
|
||||
'[(car x)
|
||||
(car (cdr x))
|
||||
(car (cdr (cdr x)))
|
||||
(car (cdr (cdr (cdr x))))])
|
||||
|
||||
(check-equal? (syntax->datum
|
||||
(list-destructure-syntax #'[x y] #'lst #'z #:unsafe? #t))
|
||||
'(let- ([x (unsafe-car lst)]
|
||||
[y (unsafe-car (unsafe-cdr lst))])
|
||||
z))))
|
||||
118
turnstile/examples/linear/lin+var.rkt
Normal file
118
turnstile/examples/linear/lin+var.rkt
Normal file
|
|
@ -0,0 +1,118 @@
|
|||
#lang turnstile/lang
|
||||
(extends "lin.rkt")
|
||||
(require (only-in "lin+tup.rkt" list-destructure-syntax))
|
||||
|
||||
(provide ⊕ var match)
|
||||
|
||||
(define-internal-type-constructor ⊕/i)
|
||||
|
||||
(define-syntax ⊕
|
||||
(syntax-parser
|
||||
[(_ (V:id t ...) ...)
|
||||
(add-orig (mk-type #'(⊕/i- (#%app 'V t ...) ...))
|
||||
this-syntax)]))
|
||||
|
||||
(begin-for-syntax
|
||||
(provide ⊕? ~⊕)
|
||||
(define ⊕? ⊕/i?)
|
||||
|
||||
(define (fail/no-variant type V [src V])
|
||||
(raise-syntax-error #f
|
||||
(format "expected type ~a does not have variant named '~a'\n"
|
||||
(type->str type)
|
||||
(stx->datum V))
|
||||
src))
|
||||
|
||||
(define (num-var-args-fail-msg σs xs)
|
||||
(format "wrong number of arguments to variant: expected ~a, got ~a"
|
||||
(stx-length σs)
|
||||
(stx-length xs)))
|
||||
|
||||
|
||||
(define (unvariant type)
|
||||
(syntax-parse type
|
||||
[(~⊕/i ((~literal #%plain-app) ((~literal quote) U) τ ...) ...)
|
||||
#'[(U τ ...) ...]]))
|
||||
|
||||
(define-syntax ~⊕
|
||||
(pattern-expander
|
||||
(λ (stx)
|
||||
(syntax-case stx ()
|
||||
[(_ . pat)
|
||||
(with-syntax ([(x) (generate-temporaries #'(x))])
|
||||
#'(~and x (~⊕/i . _) (~parse pat (unvariant #'x))))]))))
|
||||
|
||||
(define (has-variant? type v)
|
||||
(syntax-parse type
|
||||
[(~⊕ [U . _] ...)
|
||||
(for/or ([u (in-syntax #'[U ...])])
|
||||
(eq? (stx->datum u) (stx->datum v)))]
|
||||
[_ #f]))
|
||||
|
||||
(define (get-variant type v)
|
||||
(syntax-parse type
|
||||
[(~⊕ [U τ ...] ...)
|
||||
(for/first ([u (in-syntax #'[U ...])]
|
||||
[ts (in-syntax #'[(τ ...) ...])]
|
||||
#:when (eq? (stx->datum u) (stx->datum v)))
|
||||
ts)]))
|
||||
|
||||
(current-linear-type? (or/c ⊕? (current-linear-type?)))
|
||||
)
|
||||
|
||||
|
||||
(define-typed-syntax var
|
||||
[(_ [V:id e ...]) ⇐ σ_var ≫
|
||||
#:when (⊕? #'σ_var)
|
||||
#:fail-unless (has-variant? #'σ_var #'V)
|
||||
(fail/no-variant #'σ_var #'V this-syntax)
|
||||
#:with [σ ...] (get-variant #'σ_var #'V)
|
||||
#:fail-unless (stx-length=? #'[σ ...] #'[e ...])
|
||||
(num-var-args-fail-msg #'[σ ...] #'[e ...])
|
||||
[⊢ e ≫ e- ⇐ σ] ...
|
||||
--------
|
||||
[⊢ (list 'V e- ...)]]
|
||||
|
||||
[(_ [V:id e ...] (~datum as) t) ≫
|
||||
--------
|
||||
[≻ (lin:ann (var [V e ...]) : t)]])
|
||||
|
||||
|
||||
|
||||
(define-typed-syntax match
|
||||
[(_ e_var [(V:id x:id ...) e_bra] ...) ≫
|
||||
[⊢ e_var ≫ e_var- ⇒ σ_var]
|
||||
#:fail-unless (⊕? #'σ_var)
|
||||
(format "expected type ⊕, given ~a" (type->str #'σ_var))
|
||||
|
||||
#:mode (make-linear-branch-mode (stx-length #'[e_bra ...]))
|
||||
(#:with ([(x- ...) e_bra- σ_bra] ...)
|
||||
(for/list ([q (in-syntax #'([V (x ...) e_bra] ...))]
|
||||
[i (in-naturals)])
|
||||
(syntax-parse/typecheck q
|
||||
[(V (x ...) e) ≫
|
||||
#:fail-unless (has-variant? #'σ_var #'V)
|
||||
(fail/no-variant #'σ_var #'V)
|
||||
|
||||
#:with [σ ...] (get-variant #'σ_var #'V)
|
||||
#:fail-unless (stx-length=? #'[σ ...] #'[x ...])
|
||||
(num-var-args-fail-msg #'[σ ...] #'[x ...])
|
||||
|
||||
#:submode (branch-nth i)
|
||||
([[x ≫ x- : σ] ... ⊢ e ≫ e- ⇒ σ_bra]
|
||||
#:do [(linear-out-of-scope! #'([x- : σ] ...))])
|
||||
--------
|
||||
[≻ [(x- ...) e- σ_bra]]])))
|
||||
|
||||
#:with tmp (generate-temporary)
|
||||
#:with (destr ...) (stx-map (λ (l) (apply list-destructure-syntax (stx->list l)))
|
||||
#'[([x- ...]
|
||||
(cdr tmp)
|
||||
e_bra-) ...])
|
||||
--------
|
||||
[⊢ (let ([tmp e_var-])
|
||||
(case (car tmp)
|
||||
[(V) destr] ...
|
||||
[else (printf "~a\n" tmp)
|
||||
(error '"unhandled case: " (car tmp))]))
|
||||
⇒ (⊔ σ_bra ...)]])
|
||||
349
turnstile/examples/linear/lin.rkt
Normal file
349
turnstile/examples/linear/lin.rkt
Normal file
|
|
@ -0,0 +1,349 @@
|
|||
#lang turnstile
|
||||
(extends "../ext-stlc.rkt" #:except define if begin let let* letrec λ #%app)
|
||||
|
||||
(provide (for-syntax current-linear-type?
|
||||
linear-type?
|
||||
unrestricted-type?
|
||||
|
||||
linear-scope
|
||||
linear-in-scope?
|
||||
linear-use-var!
|
||||
linear-out-of-scope!
|
||||
linear-merge-scopes!
|
||||
linear-merge-scopes*!
|
||||
|
||||
;; TODO: should these be in turnstile/mode ?
|
||||
branch-nth
|
||||
branch-then
|
||||
branch-else
|
||||
|
||||
make-empty-linear-mode
|
||||
make-fresh-linear-mode
|
||||
make-linear-branch-mode)
|
||||
|
||||
%%reset-linear-mode
|
||||
|
||||
(type-out Unit Int String Bool -o)
|
||||
#%top-interaction #%module-begin require only-in
|
||||
begin drop
|
||||
#%app #%lin-var
|
||||
λ (rename-out [λ lambda])
|
||||
let letrec
|
||||
if
|
||||
define
|
||||
)
|
||||
|
||||
|
||||
(define-type-constructor -o #:arity >= 1)
|
||||
|
||||
|
||||
(begin-for-syntax
|
||||
(require syntax/id-set
|
||||
racket/set
|
||||
racket/generic
|
||||
turnstile/mode)
|
||||
|
||||
(define (fail/multiple-use x)
|
||||
(raise-syntax-error #f "linear variable used more than once" x))
|
||||
(define (fail/unused x)
|
||||
(raise-syntax-error #f "linear variable unused" x))
|
||||
(define (fail/unbalanced-branches x)
|
||||
(raise-syntax-error #f "linear variable may be unused in certain branches" x))
|
||||
(define (fail/unrestricted-fn x)
|
||||
(raise-syntax-error #f "linear variable may not be used by unrestricted function" x))
|
||||
|
||||
|
||||
;; this parameter defines the linear-type? function.
|
||||
;; we defining new types that are linear, modify this
|
||||
;; parameter like so:
|
||||
;; (current-linear-type? (or/c MYTYPE? (current-linear-type?)))
|
||||
;;
|
||||
;; current-linear-type? : (Parameter (Type -> Bool))
|
||||
(define current-linear-type?
|
||||
(make-parameter -o?))
|
||||
|
||||
;; is the given type [linear|unrestricted]?
|
||||
;; Type -> Bool
|
||||
(define (linear-type? T)
|
||||
((current-linear-type?) T))
|
||||
(define (unrestricted-type? T)
|
||||
(not ((current-linear-type?) T)))
|
||||
|
||||
|
||||
|
||||
;; mode object to be used during linear typing.
|
||||
;; the field 'scope' contains a free-id-set of
|
||||
;; variables that have been used, and therefore
|
||||
;; can't be used again.
|
||||
(struct linear-mode mode (scope))
|
||||
|
||||
;; get the current scope (as described above)
|
||||
;; based on (current-mode)
|
||||
(define (linear-scope)
|
||||
(linear-mode-scope (current-mode)))
|
||||
|
||||
;; is the given variable available for use?
|
||||
;; linear-in-scope? : Id -> Bool
|
||||
(define (linear-in-scope? x)
|
||||
(not (set-member? (linear-scope) x)))
|
||||
|
||||
;; set the variable to be used in this scope, or raise
|
||||
;; an error if it's already used.
|
||||
;;
|
||||
;; linear-use-var! : Id Type -> void
|
||||
(define (linear-use-var! x T #:fail [fail fail/multiple-use])
|
||||
(when (linear-type? T)
|
||||
(when (set-member? (linear-scope) x)
|
||||
(fail x))
|
||||
(set-add! (linear-scope) x)))
|
||||
|
||||
|
||||
;; call this with the ([x : t] ...) context after introducing variables,
|
||||
;; to remove those variables from the linear scope
|
||||
;;
|
||||
;; linear-out-of-scope! : Ctx -> Void
|
||||
(define (linear-out-of-scope! ctx #:fail [fail fail/unused])
|
||||
(syntax-parse ctx
|
||||
#:datum-literals (:)
|
||||
[([x : σ] ...)
|
||||
(for ([var (in-syntax #'[x ...])]
|
||||
[T (in-syntax #'[σ ...])] #:when (linear-type? T))
|
||||
(if (linear-in-scope? var)
|
||||
(fail var)
|
||||
(set-remove! (linear-scope) var)))]))
|
||||
|
||||
;; linear-merge-scopes! : (or '∪ '∩) FreeIdSet ... -> void
|
||||
(define (linear-merge-scopes! op #:fail [fail fail/unbalanced-branches] . ss)
|
||||
(linear-merge-scopes*! op ss #:fail fail))
|
||||
|
||||
;; linear-merge-scopes*! : (or '∪ '∩) (Listof FreeIdSet) -> void
|
||||
(define (linear-merge-scopes*! op ss #:fail [fail fail/unbalanced-branches])
|
||||
(define s0
|
||||
(case op
|
||||
[(∩)
|
||||
(let ([s0 (set-copy (car ss))])
|
||||
(for ([s (in-list (cdr ss))])
|
||||
(set-intersect! s0 s))
|
||||
(for* ([s (in-list ss)]
|
||||
[x (in-set s)] #:when (not (set-member? s0 x)))
|
||||
(fail x))
|
||||
s0)]
|
||||
|
||||
[(∪) (apply set-union ss)]))
|
||||
|
||||
(set-clear! (linear-scope))
|
||||
(set-union! (linear-scope) s0))
|
||||
|
||||
|
||||
|
||||
;; a mode that contains submodes, for use
|
||||
;; in branching (if, cond, etc.)
|
||||
(struct branch-mode mode (sub-modes))
|
||||
|
||||
;; for use as `#:submode (branch-nth n)`
|
||||
(define ((branch-nth n) bm)
|
||||
(list-ref (branch-mode-sub-modes bm) n))
|
||||
(define branch-then (branch-nth 0))
|
||||
(define branch-else (branch-nth 1))
|
||||
|
||||
;; creates a branch-mode with n branches (default: 2)
|
||||
;; which merges the linear sub-scopes during teardown.
|
||||
;; see 'if' syntax.
|
||||
;;
|
||||
;; make-linear-branch : Int -> BranchMode
|
||||
(define (make-linear-branch-mode [n 2])
|
||||
(define scopes
|
||||
(for/list ([i (in-range n)])
|
||||
(set-copy (linear-scope))))
|
||||
|
||||
(branch-mode void
|
||||
(λ () (linear-merge-scopes*! '∩ scopes))
|
||||
(for/list ([s (in-list scopes)])
|
||||
(linear-mode void void s))))
|
||||
|
||||
|
||||
;; creates a linear mode that disallows (on teardown) use
|
||||
;; of variables from outside of the current scope.
|
||||
;; see unrestricted λ syntax.
|
||||
;;
|
||||
;; make-fresh-linear-context : -> linear-mode?
|
||||
(define (make-fresh-linear-mode #:fail [fail fail/unrestricted-fn])
|
||||
(let ([ls #f])
|
||||
(linear-mode (λ () (set! ls (set-copy (linear-scope))))
|
||||
(λ () (linear-merge-scopes! '∩ (linear-scope) ls #:fail fail))
|
||||
(linear-scope))))
|
||||
|
||||
|
||||
;; creates an empty linear mode.
|
||||
;;
|
||||
;; make-empty-linear-mode : -> LinearMode
|
||||
(define (make-empty-linear-mode)
|
||||
(linear-mode void void (mutable-free-id-set)))
|
||||
|
||||
(current-mode (make-empty-linear-mode))
|
||||
|
||||
)
|
||||
|
||||
;; this function resets the mode to be an empty
|
||||
;; linear-mode. this should ONLY be used by tests
|
||||
;; that screw up the state of current-mode, and
|
||||
;; need to reset it for the next test. this is because
|
||||
;; we don't have proper backtracking facilities, so
|
||||
;; errors in the middle of inference screw up the
|
||||
;; global state
|
||||
(define-syntax %%reset-linear-mode
|
||||
(syntax-parser
|
||||
[(_)
|
||||
#:do [(current-mode (make-empty-linear-mode))]
|
||||
#'(#%app- void-)]))
|
||||
|
||||
|
||||
|
||||
(define-typed-syntax begin
|
||||
[(begin e ... e0) ≫
|
||||
[⊢ [e ≫ e- ⇐ Unit] ... [e0 ≫ e0- ⇒ σ]]
|
||||
--------
|
||||
[⊢ (begin- e- ... e0-) ⇒ σ]]
|
||||
|
||||
[(begin e ... e0) ⇐ σ ≫
|
||||
[⊢ [e ≫ e- ⇐ Unit] ... [e0 ≫ e0- ⇐ σ]]
|
||||
--------
|
||||
[⊢ (begin- e- ... e0-)]])
|
||||
|
||||
|
||||
|
||||
(define-typed-syntax drop
|
||||
[(drop e) ≫
|
||||
[⊢ e ≫ e- ⇒ _]
|
||||
--------
|
||||
[⊢ (#%app- void- e-) ⇒ Unit]])
|
||||
|
||||
|
||||
|
||||
(define-typed-syntax #%app
|
||||
[(_) ≫
|
||||
--------
|
||||
[⊢ (#%app- void-) ⇒ Unit]]
|
||||
|
||||
[(#%app fun arg ...) ≫
|
||||
[⊢ fun ≫ fun- ⇒ σ_fun]
|
||||
#:with (~or (~-o σ_in ... σ_out)
|
||||
(~→ σ_in ... σ_out)
|
||||
(~post (~fail "expected linear function type")))
|
||||
#'σ_fun
|
||||
[⊢ [arg ≫ arg- ⇐ σ_in] ...]
|
||||
--------
|
||||
[⊢ (#%app- fun- arg- ...) ⇒ σ_out]])
|
||||
|
||||
|
||||
|
||||
(define-typed-variable-syntax
|
||||
#:name #%lin-var
|
||||
[(#%var x- : σ) ≫
|
||||
#:do [(linear-use-var! #'x- #'σ)]
|
||||
----------
|
||||
[⊢ x- ⇒ σ]])
|
||||
|
||||
|
||||
(define-typed-syntax λ
|
||||
#:datum-literals (: !)
|
||||
;; linear lambda; annotations
|
||||
[(λ ([x:id : T:type] ...) b) ≫
|
||||
#:with [σ ...] #'[T.norm ...]
|
||||
[[x ≫ x- : σ] ... ⊢ b ≫ b- ⇒ σ_out]
|
||||
#:do [(linear-out-of-scope! #'([x- : σ] ...))]
|
||||
--------
|
||||
[⊢ (λ- (x- ...) b-) ⇒ (-o σ ... σ_out)]]
|
||||
|
||||
;; unrestricted lambda; annotations
|
||||
[(λ ! ([x:id : T:type] ...) b) ≫
|
||||
#:with [σ ...] #'[T.norm ...]
|
||||
#:mode (make-fresh-linear-mode)
|
||||
([[x ≫ x- : σ] ... ⊢ b ≫ b- ⇒ σ_out]
|
||||
#:do [(linear-out-of-scope! #'([x- : σ] ...))])
|
||||
--------
|
||||
[⊢ (λ- (x- ...) b-) ⇒ (→ σ ... σ_out)]]
|
||||
|
||||
;; linear lambda; inferred
|
||||
[(λ (x:id ...) b) ⇐ (~-o σ ... σ_out) ≫
|
||||
#:fail-unless (stx-length=? #'[x ...] #'[σ ...])
|
||||
(num-args-fail-msg this-syntax #'[x ...] #'[σ ...])
|
||||
[[x ≫ x- : σ] ... ⊢ b ≫ b- ⇐ σ_out]
|
||||
#:do [(linear-out-of-scope! #'([x- : σ] ...))]
|
||||
--------
|
||||
[⊢ (λ- (x- ...) b-)]]
|
||||
|
||||
;; unrestricted lambda; inferred
|
||||
[(λ (x:id ...) b) ⇐ (~→ σ ... σ_out) ≫
|
||||
#:fail-unless (stx-length=? #'[x ...] #'[σ ...])
|
||||
(num-args-fail-msg this-syntax #'[x ...] #'[σ ...])
|
||||
#:mode (make-fresh-linear-mode)
|
||||
([[x ≫ x- : σ] ... ⊢ b ≫ b- ⇐ σ_out]
|
||||
#:do [(linear-out-of-scope! #'([x- : σ] ...))])
|
||||
--------
|
||||
[⊢ (λ- (x- ...) b-)]])
|
||||
|
||||
|
||||
|
||||
(define-typed-syntax let
|
||||
[(let ([x e] ...) b) ≫
|
||||
[⊢ [e ≫ e- ⇒ σ] ...]
|
||||
[[x ≫ x- : σ] ... ⊢ b ≫ b- ⇒ σ_out]
|
||||
#:do [(linear-out-of-scope! #'([x- : σ] ...))]
|
||||
--------
|
||||
[⊢ (let- ([x- e-] ...) b-) ⇒ σ_out]])
|
||||
|
||||
|
||||
|
||||
(define-typed-syntax letrec
|
||||
[(letrec ([b:type-bind rhs] ...) e ...) ≫
|
||||
#:fail-when (ormap linear-type? (stx->list #'[b.type ...]))
|
||||
(format "may not bind linear type ~a in letrec"
|
||||
(type->str (findf linear-type? (stx->list #'[b.type ...]))))
|
||||
[[b.x ≫ x- : b.type] ...
|
||||
⊢ [rhs ≫ rhs- ⇐ b.type] ...
|
||||
[(begin e ...) ≫ e- ⇒ σ_out]]
|
||||
#:do [(linear-out-of-scope! #'([x- : b.type] ...))]
|
||||
--------
|
||||
[⊢ (letrec- ([x- rhs-] ...) e-) ⇒ σ_out]])
|
||||
|
||||
|
||||
|
||||
(define-typed-syntax if
|
||||
[(_ c e1 e2) ⇐ σ ≫
|
||||
[⊢ c ≫ c- ⇐ Bool]
|
||||
#:mode (make-linear-branch-mode 2)
|
||||
([⊢ [e1 ≫ e1- ⇐ σ] #:submode branch-then]
|
||||
[⊢ [e2 ≫ e2- ⇐ σ] #:submode branch-else])
|
||||
--------
|
||||
[⊢ (if- c- e1- e2-)]]
|
||||
|
||||
[(_ c e1 e2) ≫
|
||||
[⊢ c ≫ c- ⇐ Bool]
|
||||
#:mode (make-linear-branch-mode 2)
|
||||
([⊢ [e1 ≫ e1- ⇒ σ1] #:submode branch-then]
|
||||
[⊢ [e2 ≫ e2- ⇒ σ2] #:submode branch-else])
|
||||
--------
|
||||
[⊢ (if- c- e1- e2-) ⇒ (⊔ σ1 σ2)]])
|
||||
|
||||
|
||||
|
||||
(define-typed-syntax define
|
||||
#:datum-literals (:)
|
||||
[(define (f [x:id : ty] ...) ret
|
||||
e ...+) ≫
|
||||
--------
|
||||
[≻ (define f : (→ ty ... ret)
|
||||
(letrec ([{f : (→ ty ... ret)}
|
||||
(λ ! ([x : ty] ...)
|
||||
(begin e ...))])
|
||||
f))]]
|
||||
|
||||
[(_ x:id : τ:type e:expr) ≫
|
||||
#:fail-when (linear-type? #'τ.norm)
|
||||
"cannot define linear type globally"
|
||||
#:with y (generate-temporary #'x)
|
||||
--------
|
||||
[≻ (begin-
|
||||
(define-syntax x (make-rename-transformer (⊢ y : τ.norm)))
|
||||
(define- y (ann e : τ.norm)))]])
|
||||
|
|
@ -1,63 +0,0 @@
|
|||
#lang s-exp turnstile/examples/linear-var-assign
|
||||
|
||||
(require turnstile/rackunit-typechecking
|
||||
(only-in racket/base quote))
|
||||
|
||||
(check-type #t : Bool)
|
||||
(check-type 4 : Int)
|
||||
(check-type () : Unit)
|
||||
|
||||
(check-type (tup 1 #t) : (⊗ Int Bool) -> '(1 #t))
|
||||
(check-type (tup 1 (tup 2 3)) : (⊗ Int (⊗ Int Int)) -> '(1 (2 3)))
|
||||
|
||||
(check-type (let ([x 3] [y 4]) y) : Int -> 4)
|
||||
(check-type (let ([p (tup 1 2)]) p) : (⊗ Int Int) -> '(1 2))
|
||||
|
||||
(typecheck-fail (let ([p (tup 1 2)]) ())
|
||||
#:with-msg "p: linear variable unused")
|
||||
(typecheck-fail (let ([p (tup 1 2)]) (tup p p))
|
||||
#:with-msg "p: linear variable used more than once")
|
||||
|
||||
(check-type (if #t 1 2) : Int -> 1)
|
||||
(typecheck-fail (if 1 2 3)
|
||||
#:with-msg "expected Bool, given Int")
|
||||
(typecheck-fail (if #t 2 ())
|
||||
#:with-msg "expected Int, given Unit")
|
||||
|
||||
(check-type (let ([p (tup 1 ())]) (if #t p p)) : (⊗ Int Unit))
|
||||
(typecheck-fail (let ([p (tup 1 ())]) (if #t p (tup 2 ())))
|
||||
#:with-msg "linear variable may be unused in certain branches")
|
||||
(typecheck-fail (let ([p (tup 1 ())]) (if #t p (begin p p)))
|
||||
#:with-msg "p: linear variable used more than once")
|
||||
|
||||
|
||||
(check-type (λ ([x : Int]) (tup x x)) : (-o Int (⊗ Int Int)))
|
||||
(check-type (λ ([x : (⊗ Int Int)]) x) : (-o (⊗ Int Int) (⊗ Int Int)))
|
||||
(typecheck-fail (λ ([x : (⊗ Int Int)]) ())
|
||||
#:with-msg "x: linear variable unused")
|
||||
|
||||
(check-type (let ([p (tup 1 2)]) (λ ([x : Int]) p))
|
||||
: (-o Int (⊗ Int Int)))
|
||||
|
||||
(check-type (λ ! ([x : Int]) x) : (!! (-o Int Int)))
|
||||
(typecheck-fail (let ([p (tup 1 2)]) (λ ! ([x : Int]) p))
|
||||
#:with-msg "linear variable may not be used by unrestricted function")
|
||||
|
||||
|
||||
(check-type (let ([f (λ ([x : Int] [y : Int]) y)])
|
||||
(f 3 4))
|
||||
: Int -> 4)
|
||||
(check-type + : (!! (-o Int Int Int)))
|
||||
(check-type (+ 1 2) : Int -> 3)
|
||||
(check-type (< 3 4) : Bool -> #t)
|
||||
|
||||
|
||||
(check-type (let ([×2 (λ ! ([x : Int]) (+ x x))])
|
||||
(+ (×2 8)
|
||||
(×2 9)))
|
||||
: Int -> 34)
|
||||
|
||||
(typecheck-fail (let ([×2 (λ ([x : Int]) (+ x x))])
|
||||
(+ (×2 8)
|
||||
(×2 9)))
|
||||
#:with-msg "×2: linear variable used more than once")
|
||||
18
turnstile/examples/tests/linear/lin+chan-tests.rkt
Normal file
18
turnstile/examples/tests/linear/lin+chan-tests.rkt
Normal file
|
|
@ -0,0 +1,18 @@
|
|||
#lang s-exp turnstile/examples/linear/lin+chan
|
||||
(require turnstile/rackunit-typechecking)
|
||||
|
||||
(check-type
|
||||
(let* ([(c c-out) (make-channel {Int})])
|
||||
(thread (λ () (channel-put c-out 5)))
|
||||
(thread (λ () (channel-put c-out 4)))
|
||||
(let* ([(c1 x) (channel-get c)]
|
||||
[(c2 y) (channel-get c1)])
|
||||
(drop c2)
|
||||
(+ x y)))
|
||||
: Int -> 9)
|
||||
|
||||
(typecheck-fail
|
||||
(let* ([(c-in c-out) (make-channel {String})])
|
||||
(thread (λ () (channel-get c-in)))
|
||||
(channel-get c-in))
|
||||
#:with-msg "c-in: linear variable used more than once")
|
||||
28
turnstile/examples/tests/linear/lin+cons-tests.rkt
Normal file
28
turnstile/examples/tests/linear/lin+cons-tests.rkt
Normal file
|
|
@ -0,0 +1,28 @@
|
|||
#lang s-exp turnstile/examples/linear/lin+cons
|
||||
(require turnstile/rackunit-typechecking)
|
||||
|
||||
|
||||
(define (length [lst : (MList Int)]) Int
|
||||
(match-list lst
|
||||
[(cons _ xs @ l)
|
||||
(begin (drop l)
|
||||
(add1 (length xs)))]
|
||||
[(nil) 0]))
|
||||
|
||||
(check-type (length (cons 9 (cons 8 (cons 7 (nil))))) : Int -> 3)
|
||||
|
||||
|
||||
|
||||
(define (rev-append [lst : (MList String)]
|
||||
[acc : (MList String)]) (MList String)
|
||||
(match-list lst
|
||||
[(cons x xs @ l) (rev-append xs (cons x acc @ l))]
|
||||
[(nil) acc]))
|
||||
|
||||
(define (rev [lst : (MList String)]) (MList String)
|
||||
(rev-append lst (nil)))
|
||||
|
||||
|
||||
(check-type (rev (cons "a" (cons "b" (cons "c" (nil)))))
|
||||
: (MList String)
|
||||
-> (cons "c" (cons "b" (cons "a" (nil)))))
|
||||
29
turnstile/examples/tests/linear/lin+tup-tests.rkt
Normal file
29
turnstile/examples/tests/linear/lin+tup-tests.rkt
Normal file
|
|
@ -0,0 +1,29 @@
|
|||
#lang s-exp turnstile/examples/linear/lin+tup
|
||||
|
||||
(require turnstile/rackunit-typechecking
|
||||
(only-in racket/base quote))
|
||||
|
||||
(check-type (tup 1 #t) : (⊗ Int Bool) -> '(1 #t))
|
||||
(check-type (tup 1 2 3) : (⊗ Int Int Int) -> '(1 2 3))
|
||||
|
||||
(check-type (let ([p (tup 1 2)]) p) : (⊗ Int Int) -> '(1 2))
|
||||
(typecheck-fail (let ([p (tup 1 2)]) ())
|
||||
#:with-msg "p: linear variable unused")
|
||||
(typecheck-fail (let ([p (tup 1 2)]) (tup p p))
|
||||
#:with-msg "p: linear variable used more than once")
|
||||
|
||||
(check-type (let ([p (tup 1 ())]) (if #t p p)) : (⊗ Int Unit))
|
||||
(typecheck-fail (let ([p (tup 1 ())]) (if #t p (tup 2 ())))
|
||||
#:with-msg "linear variable may be unused in certain branches")
|
||||
|
||||
(check-type (λ ([x : Int]) (tup x x)) : (-o Int (⊗ Int Int)))
|
||||
(typecheck-fail (λ ([x : (⊗ Int Int)]) ())
|
||||
#:with-msg "x: linear variable unused")
|
||||
|
||||
(check-type (let ([p (tup 1 2)]) (λ ([x : Int]) p))
|
||||
: (-o Int (⊗ Int Int)))
|
||||
|
||||
(check-type (let* ([x 3] [y x]) y) : Int -> 3)
|
||||
(check-type (let* ([(x y) (tup 1 #f)]) x) : Int -> 1)
|
||||
(typecheck-fail (let* ([(x y) (tup (tup 1 2) 3)]) y)
|
||||
#:with-msg "x: linear variable unused")
|
||||
67
turnstile/examples/tests/linear/lin+var-tests.rkt
Normal file
67
turnstile/examples/tests/linear/lin+var-tests.rkt
Normal file
|
|
@ -0,0 +1,67 @@
|
|||
#lang s-exp turnstile/examples/linear/lin+var
|
||||
(require turnstile/rackunit-typechecking)
|
||||
|
||||
(check-type (var [left 3]) : (⊕ [left Int] [right String]))
|
||||
(check-type (var [right "a"]) : (⊕ [left Int] [right String]))
|
||||
|
||||
(typecheck-fail (var [left 3] as (⊕ [yes] [no]))
|
||||
#:with-msg "type \\(⊕ \\(yes\\) \\(no\\)\\) does not have variant named 'left'")
|
||||
|
||||
(typecheck-fail (var [left 3] as (⊕ [left Int Int] [right String]))
|
||||
#:with-msg "wrong number of arguments to variant: expected 2, got 1")
|
||||
|
||||
(define-type-alias (Either A B) (⊕ [left A] [right B]))
|
||||
(define-type-alias (Option A) (⊕ [some A] [none]))
|
||||
|
||||
(typecheck-fail (var [middle 3] as (Either Int Float))
|
||||
#:with-msg "type \\(Either Int Float\\) does not have variant named 'middle'")
|
||||
|
||||
(check-type (λ (x) x) : (→ (Either Int Float) (Either Int Float)))
|
||||
(check-type (λ (x) x) : (→ (Either Int Float) (⊕ [left Int] [right Float])))
|
||||
|
||||
(typecheck-fail (let ([x (var [left 3] as (Either Int Int))]) 0)
|
||||
#:with-msg "x: linear variable unused")
|
||||
|
||||
(check-type (match (var [left 3] as (Either Int Int))
|
||||
[(left x) x]
|
||||
[(right y) (+ y 1)])
|
||||
: Int ⇒ 3)
|
||||
|
||||
(check-type (match (var [right 5] as (Either Int Int))
|
||||
[(left x) x]
|
||||
[(right y) (+ y 1)])
|
||||
: Int ⇒ 6)
|
||||
|
||||
(typecheck-fail (match (var [left 3] as (Either Int (-o Int Int)))
|
||||
[(left x) x]
|
||||
[(right f) 0])
|
||||
#:with-msg "f: linear variable unused")
|
||||
|
||||
(check-type (match (var [right (λ (x) (+ x x))] as (Either Int (-o Int Int)))
|
||||
[(left x) x]
|
||||
[(right f) (f 2)])
|
||||
: Int ⇒ 4)
|
||||
|
||||
(typecheck-fail (match (var [left 0] as (Either Int String))
|
||||
[(left x) x]
|
||||
[(right y) y])
|
||||
#:with-msg "branches have incompatible types: Int and String")
|
||||
|
||||
(typecheck-fail (match (var [some ()] as (Option Unit))
|
||||
[(left x) x]
|
||||
[(right y) y])
|
||||
#:with-msg "type \\(Option Unit\\) does not have variant named 'left'")
|
||||
(%%reset-linear-mode)
|
||||
|
||||
(typecheck-fail (match (var [left 0] as (Either Int Int))
|
||||
[(left x) x]
|
||||
[(right y z) y])
|
||||
#:with-msg "wrong number of arguments to variant: expected 1, got 2")
|
||||
(%%reset-linear-mode)
|
||||
|
||||
(typecheck-fail (let ([f (λ ([x : Int]) x)])
|
||||
(match (var [left 0] as (Either Int Int))
|
||||
[(left x) (f x)]
|
||||
[(right y) y]))
|
||||
#:with-msg "f: linear variable may be unused in certain branches")
|
||||
(%%reset-linear-mode)
|
||||
76
turnstile/examples/tests/linear/lin-tests.rkt
Normal file
76
turnstile/examples/tests/linear/lin-tests.rkt
Normal file
|
|
@ -0,0 +1,76 @@
|
|||
#lang s-exp turnstile/examples/linear/lin
|
||||
(require turnstile/rackunit-typechecking
|
||||
(only-in racket/base quote))
|
||||
|
||||
(check-type #t : Bool)
|
||||
(check-type 4 : Int)
|
||||
(check-type () : Unit)
|
||||
|
||||
(check-type (let ([x 3] [y 4]) y) : Int -> 4)
|
||||
|
||||
(check-type (if #t 1 2) : Int -> 1)
|
||||
(typecheck-fail (if 1 2 3)
|
||||
#:with-msg "expected Bool, given Int")
|
||||
(typecheck-fail (if #t 2 ())
|
||||
#:with-msg "branches have incompatible types: Int and Unit")
|
||||
(%%reset-linear-mode)
|
||||
|
||||
(check-type (λ ([x : Int]) x) : (-o Int Int))
|
||||
(check-type (λ ! ([x : Int]) x) : (→ Int Int))
|
||||
(check-type (λ (x) x) : (-o String String))
|
||||
(check-type (λ (x) x) : (→ String String))
|
||||
|
||||
(check-type + : (→ Int Int Int))
|
||||
(check-type (+ 1 2) : Int -> 3)
|
||||
(check-type ((λ ([x : Int]) (+ x 1)) 4) : Int -> 5)
|
||||
|
||||
|
||||
(typecheck-fail (λ ([p : (-o Int Bool)]) 0)
|
||||
#:with-msg "p: linear variable unused")
|
||||
|
||||
(typecheck-fail (let ([f (λ ([x : Int]) x)])
|
||||
0)
|
||||
#:with-msg "f: linear variable unused")
|
||||
|
||||
(typecheck-fail (let ([f (λ ([x : Int]) x)])
|
||||
(f (f 3)))
|
||||
#:with-msg "f: linear variable used more than once")
|
||||
|
||||
(typecheck-fail (let ([f (λ ([x : Int]) x)])
|
||||
(if #t
|
||||
(f 3)
|
||||
4))
|
||||
#:with-msg "f: linear variable may be unused in certain branches")
|
||||
|
||||
(typecheck-fail (let ([f (λ ([x : Int]) x)])
|
||||
(λ ! ([x : Int]) f))
|
||||
#:with-msg "f: linear variable may not be used by unrestricted function")
|
||||
(%%reset-linear-mode)
|
||||
|
||||
(check-type (let ([twice (λ ! ([x : Int]) (+ x x))])
|
||||
(+ (twice 8)
|
||||
(twice 9)))
|
||||
: Int -> 34)
|
||||
|
||||
(check-type (let ([f (λ ([x : Int]) #t)])
|
||||
(begin (drop f)
|
||||
3))
|
||||
: Int -> 3)
|
||||
|
||||
(check-type (letrec ([{<= : (→ Int Int Bool)}
|
||||
(λ (n m)
|
||||
(if (zero? n)
|
||||
#t
|
||||
(if (zero? m)
|
||||
#f
|
||||
(<= (sub1 n) (sub1 m)))))])
|
||||
(if (<= 4 1) 999
|
||||
(if (<= 3 3)
|
||||
0
|
||||
888)))
|
||||
: Int -> 0)
|
||||
|
||||
(typecheck-fail (letrec ([{f : (-o Int Int)}
|
||||
(λ (x) (f x))])
|
||||
(f 3))
|
||||
#:with-msg "may not bind linear type \\(-o Int Int\\) in letrec")
|
||||
Loading…
Reference in New Issue
Block a user