-
Notifications
You must be signed in to change notification settings - Fork 14
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
add current-var-assign parameter (#12)
* add current-var-assign parameter * add example of linear language + tests (Based on @iitalics work in pull request #11)
- Loading branch information
1 parent
7acbcbb
commit 9d3c55d
Showing
3 changed files
with
277 additions
and
3 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,200 @@ | ||
#lang turnstile | ||
|
||
(provide (type-out Unit Int Str Bool -o ⊗ !!) | ||
#%top-interaction #%module-begin require only-in | ||
#%datum begin tup let λ #%app if | ||
(rename-out [λ lambda])) | ||
|
||
(provide (typed-out [+ : (!! (-o Int Int Int))] | ||
[< : (!! (-o Int Int Bool))] | ||
[displayln : (!! (-o Str Unit))])) | ||
|
||
(define-base-types Unit Int Str Bool) | ||
(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 unrestricted-type? | ||
(or/c Int? Str? !!?)) | ||
|
||
|
||
(define used-vars (immutable-free-id-set)) | ||
|
||
(define (lin-var-in-scope? x) | ||
(not (set-member? used-vars x))) | ||
|
||
(define (use-lin-var x) | ||
(unless (lin-var-in-scope? x) | ||
(raise-syntax-error #f "linear variable used more than once" x)) | ||
(set! used-vars (set-add used-vars x))) | ||
|
||
(define (pop-vars xs ts) | ||
(set! used-vars | ||
(for/fold ([uv used-vars]) | ||
([x (in-syntax xs)] | ||
[t (in-syntax ts)]) | ||
(unless (unrestricted-type? t) | ||
(when (lin-var-in-scope? x) | ||
(raise-syntax-error #f "linear variable unused" x))) | ||
(set-remove uv x)))) | ||
|
||
|
||
|
||
(define scope-stack '()) | ||
|
||
(define (save-scope) | ||
(set! scope-stack (cons used-vars scope-stack))) | ||
|
||
(define (merge-scope #:fail-msg fail-msg | ||
#:fail-src [fail-src #f]) | ||
(for ([x (in-set (sym-diff used-vars (car scope-stack)))]) | ||
(raise-syntax-error #f fail-msg fail-src x)) | ||
(set! scope-stack (cdr scope-stack))) | ||
|
||
(define (swap-scope) | ||
(set! used-vars | ||
(begin0 (car scope-stack) | ||
(set! scope-stack | ||
(cons used-vars (cdr scope-stack)))))) | ||
|
||
) | ||
|
||
|
||
(define-typed-syntax #%top-interaction | ||
[(_ . e) ≫ | ||
[⊢ e ≫ e- ⇒ τ] | ||
-------- | ||
[≻ (#%app- printf- '"~a : ~a\n" | ||
e- | ||
'#,(type->str #'τ))]]) | ||
|
||
|
||
(define-typed-syntax LIN | ||
#:datum-literals [:] | ||
[(_ x- : σ) ≫ | ||
#:when (unrestricted-type? #'σ) | ||
-------- | ||
[⊢ x- ⇒ σ]] | ||
[(_ x- : σ) ≫ | ||
#:do [(use-lin-var #'x-)] | ||
-------- | ||
[⊢ x- ⇒ σ]]) | ||
|
||
(begin-for-syntax | ||
(define (stx-append-map f . lsts) | ||
(append* (apply stx-map f lsts))) | ||
|
||
(current-var-assign | ||
(lambda (x seps types) | ||
#`(LIN #,x #,@(stx-append-map list seps types))))) | ||
|
||
|
||
(define-typed-syntax #%datum | ||
[(_ . n:exact-integer) ≫ | ||
-------- | ||
[⊢ (#%datum- . n) ⇒ Int]] | ||
[(_ . b:boolean) ≫ | ||
-------- | ||
[⊢ (#%datum- . b) ⇒ Bool]] | ||
[(_ . s:str) ≫ | ||
-------- | ||
[⊢ (#%datum- . s) ⇒ Str]] | ||
[(_ . x) ≫ | ||
-------- | ||
[#:error (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)]]) | ||
|
||
|
||
(define-typed-syntax begin | ||
[(_ e ... e0) ≫ | ||
[⊢ [e ≫ e- ⇒ _] ... [e0 ≫ e0- ⇒ σ]] | ||
-------- | ||
[⊢ (begin- e- ... e0-) ⇒ σ]]) | ||
|
||
|
||
(define-typed-syntax tup | ||
#:datum-literals (!) | ||
[(_ e1 e2) ≫ | ||
[⊢ e1 ≫ e1- ⇒ σ1] | ||
[⊢ e2 ≫ e2- ⇒ σ2] | ||
-------- | ||
[⊢ (#%app- list- e1- e2-) ⇒ (⊗ σ1 σ2)]] | ||
|
||
[(_ ! e1 e2) ≫ | ||
#:do [(save-scope)] | ||
[⊢ e1 ≫ e1- ⇒ σ1] | ||
[⊢ e2 ≫ e2- ⇒ σ2] | ||
#:do [(merge-scope #:fail-msg "linear variable may not be used by unrestricted tuple" | ||
#:fail-src this-syntax)] | ||
-------- | ||
[⊢ (#%app- list- e1- e2-) ⇒ (!! (⊗ σ1 σ2))]]) | ||
|
||
|
||
(define-typed-syntax let | ||
[(let ([x rhs] ...) e) ≫ | ||
[⊢ [rhs ≫ rhs- ⇒ σ] ...] | ||
[[x ≫ x- : σ] ... ⊢ e ≫ e- ⇒ σ_out] | ||
#:do [(pop-vars #'(x- ...) #'(σ ...))] | ||
-------- | ||
[⊢ (let- ([x- rhs-] ...) e-) ⇒ σ_out]]) | ||
|
||
|
||
(define-typed-syntax λ | ||
#:datum-literals (: !) | ||
; linear function | ||
[(λ ([x:id : ty:type] ...) e) ≫ | ||
#:with (σ ...) #'(ty.norm ...) | ||
[[x ≫ x- : σ] ... ⊢ e ≫ e- ⇒ σ_out] | ||
#:do [(pop-vars #'(x- ...) #'(σ ...))] | ||
-------- | ||
[⊢ (λ- (x- ...) e-) ⇒ (-o σ ... σ_out)]] | ||
|
||
; unrestricted function | ||
[(λ ! ([x:id : ty:type] ...) e) ≫ | ||
#:do [(save-scope)] | ||
#:with (σ ...) #'(ty.norm ...) | ||
[[x ≫ x- : σ] ... ⊢ e ≫ e- ⇒ σ_out] | ||
#:do [(pop-vars #'(x- ...) #'(σ ...)) | ||
(merge-scope #:fail-msg "linear variable may not be used by unrestricted function" | ||
#:fail-src this-syntax)] | ||
-------- | ||
[⊢ (λ- (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 function type"))) | ||
#'σ_fun | ||
[⊢ [arg ≫ arg- ⇐ σ_in] ...] | ||
-------- | ||
[⊢ (#%app- fun- arg- ...) ⇒ σ_out]]) | ||
|
||
|
||
(define-typed-syntax if | ||
[(if c e1 e2) ≫ | ||
[⊢ c ≫ c- ⇐ Bool] | ||
#:do [(save-scope)] | ||
[⊢ e1 ≫ e1- ⇒ σ] | ||
#:do [(swap-scope)] | ||
[⊢ e2 ≫ e2- ⇐ σ] | ||
#:do [(merge-scope #:fail-msg "linear variable may be unused in certain branches" | ||
#:fail-src this-syntax)] | ||
-------- | ||
[⊢ (if- c- e1- e2-) ⇒ σ]]) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,63 @@ | ||
#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") |