Milo Turner
Stephen Chang
parent
5d412504fb
commit
6d496741c6
71
turnstile/examples/linear/fabul-utils.rkt
Normal file
71
turnstile/examples/linear/fabul-utils.rkt
Normal file
|
|
@ -0,0 +1,71 @@
|
|||
#lang racket
|
||||
(require syntax/parse
|
||||
turnstile/mode
|
||||
(for-syntax syntax/parse syntax/stx racket/syntax)
|
||||
(for-template macrotypes/typecheck
|
||||
(only-in "lin.rkt"
|
||||
linear-mode?
|
||||
make-empty-linear-mode)))
|
||||
|
||||
(provide current-language
|
||||
language-name
|
||||
type-converter
|
||||
unrestricted-mode?
|
||||
make-empty-unrestricted-mode
|
||||
L->U
|
||||
U->L
|
||||
)
|
||||
|
||||
(struct unrestricted-mode mode (lin-mode))
|
||||
|
||||
(define (make-empty-unrestricted-mode)
|
||||
(unrestricted-mode void void (make-empty-linear-mode)))
|
||||
|
||||
(define (L->U lin-mode)
|
||||
(unrestricted-mode void void lin-mode))
|
||||
|
||||
(define (U->L un-mode)
|
||||
(unrestricted-mode-lin-mode un-mode))
|
||||
|
||||
|
||||
(define (current-language)
|
||||
(if (linear-mode? (current-mode))
|
||||
'L
|
||||
'U))
|
||||
|
||||
(define (language-name [lang (current-language)])
|
||||
(case lang
|
||||
[(L) "linear"]
|
||||
[(U) "unrestricted"]))
|
||||
|
||||
|
||||
; generates function to convert type into language
|
||||
; e.g. (type-converter [ <clauses> ... ]
|
||||
; [ A => B ]
|
||||
; [ C => D ]
|
||||
; <fail-function>)
|
||||
(define-syntax type-converter
|
||||
(syntax-parser
|
||||
#:datum-literals (=>)
|
||||
[(_ (stxparse ...)
|
||||
([from:id => to:id] ...)
|
||||
fail-fn)
|
||||
#:with self (generate-temporary)
|
||||
#:with [(lhs rhs) ...] #'[(from to) ... (to to) ...]
|
||||
#:with [tycon-clause ...]
|
||||
(stx-map (λ (tycon/l tycon/r)
|
||||
(with-syntax ([patn (format-id tycon/l "~~~a" tycon/l)]
|
||||
[ctor tycon/r]
|
||||
[t (generate-temporary)]
|
||||
[s (generate-temporary)])
|
||||
#'[(patn t (... ...))
|
||||
#:with [s (... ...)] (stx-map self #'[t (... ...)])
|
||||
(syntax/loc this-syntax (ctor s (... ...)))]))
|
||||
#'[lhs ...]
|
||||
#'[rhs ...])
|
||||
#'(letrec ([self (syntax-parser
|
||||
stxparse ...
|
||||
tycon-clause ...
|
||||
[(~not (~Any _ . _)) this-syntax]
|
||||
[_ (fail-fn this-syntax)])])
|
||||
self)]))
|
||||
241
turnstile/examples/linear/fabul.rkt
Normal file
241
turnstile/examples/linear/fabul.rkt
Normal file
|
|
@ -0,0 +1,241 @@
|
|||
#lang turnstile
|
||||
(require (for-syntax "fabul-utils.rkt"
|
||||
turnstile/mode))
|
||||
|
||||
(provide begin let let* letrec λ lambda #%app if tup cons nil
|
||||
drop match-list
|
||||
proj isnil head tail list-ref member
|
||||
define
|
||||
%L %U
|
||||
#%module-begin #%top-interaction require
|
||||
(typed-out [= : (→ Int Int Int)]
|
||||
[< : (→ Int Int Bool)]
|
||||
[sub1 : (→ Int Int)]
|
||||
[add1 : (→ Int Int)]
|
||||
[zero? : (→ Int Bool)]))
|
||||
|
||||
; import other languages
|
||||
(require (prefix-in U: "../ext-stlc.rkt")
|
||||
(prefix-in U: (except-in "../stlc+cons.rkt" tup proj))
|
||||
(prefix-in U: (only-in "../stlc+tup.rkt" tup proj))
|
||||
(prefix-in L: "lin.rkt")
|
||||
(prefix-in L: "lin+cons.rkt")
|
||||
(only-in "../ext-stlc.rkt" → ~→)
|
||||
(only-in "../stlc+tup.rkt" × ~×)
|
||||
(only-in "../stlc+cons.rkt" List ~List)
|
||||
(only-in "lin+cons.rkt" ⊗ ~⊗ MList ~MList)
|
||||
(only-in "lin+tup.rkt" in-cad*rs)
|
||||
"lin.rkt" #| this includes base types like Int, Unit, etc. |#)
|
||||
|
||||
; reuse types
|
||||
(reuse Unit Bool Int Float String → #:from "../ext-stlc.rkt")
|
||||
(reuse × #:from "../stlc+tup.rkt")
|
||||
(reuse List #:from "../stlc+cons.rkt")
|
||||
(reuse -o ⊗ MList #:from "lin+cons.rkt")
|
||||
|
||||
; reuse forms
|
||||
(reuse #%datum ann and or define-type-alias #:from "../ext-stlc.rkt")
|
||||
|
||||
|
||||
|
||||
; begin in unrestricted mode
|
||||
(begin-for-syntax
|
||||
(current-mode (make-empty-unrestricted-mode)))
|
||||
|
||||
|
||||
; dispatch some forms to L: or U: variant, based on [current-language]
|
||||
(define-syntax language-dispatch
|
||||
(syntax-parser
|
||||
[(_ [lang ...] form)
|
||||
#:with (form/lang ...) (stx-map (λ (X) (format-id X "~a:~a" X #'form)) #'[lang ...])
|
||||
#'(define-syntax form
|
||||
(syntax-parser
|
||||
[(_ . args)
|
||||
#:when (eq? (current-language) 'lang)
|
||||
(syntax/loc this-syntax
|
||||
(form/lang . args))] ...
|
||||
[_
|
||||
(raise-syntax-error 'form
|
||||
(format "form not allowed inside ~a language"
|
||||
(language-name)))]))]
|
||||
|
||||
[(_ [lang ...] form ...+)
|
||||
#'(begin-
|
||||
(language-dispatch [lang ...] form) ...)]))
|
||||
|
||||
(language-dispatch [L U] begin let let* letrec λ lambda #%app if tup cons nil)
|
||||
(language-dispatch [L] drop match-list)
|
||||
(language-dispatch [U] proj isnil head tail list-ref member)
|
||||
|
||||
|
||||
(begin-for-syntax
|
||||
(define (fully-unrestricted? type)
|
||||
(and (unrestricted-type? type)
|
||||
(syntax-parse type
|
||||
[(~Any _ τ ...) (for/and ([t (in-syntax #'[τ ...])])
|
||||
(fully-unrestricted? t))]
|
||||
[_ #t])))
|
||||
|
||||
(define (fail/type-convert src lang ty)
|
||||
(raise-syntax-error #f (format "cannot convert type ~a into ~a language"
|
||||
(type->str ty)
|
||||
(language-name lang))
|
||||
src))
|
||||
|
||||
; convert-type : Symbol Type -> Type
|
||||
; converts a type into a more appropriate variant for the given language
|
||||
(define (convert-type lang type
|
||||
#:src [fail-src #f]
|
||||
#:fail [fail (λ (_) (fail/type-convert fail-src lang type))])
|
||||
(define converter
|
||||
(case lang
|
||||
[(L)
|
||||
(type-converter ([σ #:when (linear-type? #'σ) #'σ])
|
||||
([List => MList]
|
||||
[× => ⊗]
|
||||
[→ => →]
|
||||
[-o => -o])
|
||||
fail)]
|
||||
|
||||
[(U)
|
||||
(type-converter ([τ #:when (fully-unrestricted? #'τ) #'τ])
|
||||
([MList => List]
|
||||
[⊗ => ×]
|
||||
[→ => →])
|
||||
fail)]
|
||||
|
||||
[else (error "invalid language" lang)]))
|
||||
|
||||
((current-type-eval) (converter type)))
|
||||
|
||||
; convert-syntax : Type Type Syntax -> Syntax
|
||||
; creates an expression that wraps the given syntax such that
|
||||
; it converts objects from the first type into the second type.
|
||||
; the resulting syntax will never evaluate the original syntax twice.
|
||||
; e.g.
|
||||
; (convert-stx #'(List Int) #'(MList Int) #'x)
|
||||
; ->
|
||||
; #'(foldr mcons '() x)
|
||||
(define (convert-syntax . args)
|
||||
(syntax-parse args
|
||||
[[τ σ src] #:when (type=? #'τ #'σ) #'src]
|
||||
|
||||
; convert tuples
|
||||
[[(~or (~⊗ τ ...) (~× τ ...)) (~or (~⊗ σ ...) (~× σ ...)) src]
|
||||
#:with [out ...] (for/list ([cad*r (in-cad*rs #'tmp)]
|
||||
[T (in-syntax #'[τ ...])]
|
||||
[S (in-syntax #'[σ ...])])
|
||||
(convert-syntax T S cad*r))
|
||||
#'(let- ([tmp src]) (#%app- list- out ...))]
|
||||
|
||||
; convert lists
|
||||
[[(~List τ) (~MList σ) src]
|
||||
#:with x+ (convert-syntax #'τ #'σ #'x)
|
||||
#'(#%app- foldr- (λ- (x l) (#%app- mcons- x+ l)) '() src)]
|
||||
|
||||
[[(~MList τ) (~List σ) src]
|
||||
#:with x+ (convert-syntax #'τ #'σ #'x)
|
||||
#'(for/list- ([x (in-mlist src)]) x+)]
|
||||
|
||||
; convert functions
|
||||
[[(~or (~→ τ ... τ_out) (~-o τ ... τ_out))
|
||||
(~or (~→ σ ... σ_out) (~-o σ ... σ_out))
|
||||
src]
|
||||
#:with (x ...) (stx-map generate-temporary #'[τ ...])
|
||||
#:with (x+ ...) (stx-map convert-syntax #'[σ ...] #'[τ ...] #'[x ...])
|
||||
#:with out (convert-syntax #'τ_out #'σ_out #'(#%app- f x+ ...))
|
||||
#'(let- ([f src]) (λ- (x ...) out))]))
|
||||
|
||||
)
|
||||
|
||||
|
||||
; generate barrier crossing macros
|
||||
(define-syntax define-barrier
|
||||
(syntax-parser
|
||||
[(_ form LANG A->B)
|
||||
#'(define-typed-syntax form
|
||||
[(_ e) ≫
|
||||
#:when (eq? (syntax-local-context) 'expression)
|
||||
#:fail-when (eq? (current-language) 'LANG)
|
||||
(format "already in ~a language"
|
||||
(language-name 'LANG))
|
||||
[⊢ [e ≫ e- ⇒ τ] #:submode A->B]
|
||||
#:with σ (convert-type (current-language) #'τ #:src this-syntax)
|
||||
#:with e-- (convert-syntax #'τ #'σ #'e-)
|
||||
--------
|
||||
[⊢ e-- ⇒ σ]]
|
||||
|
||||
; expand toplevels using different syntax, bleh
|
||||
[(_ e ...+) ≫
|
||||
#:submode (if (eq? (current-language) 'LANG)
|
||||
values
|
||||
A->B)
|
||||
(#:with e- (local-expand #'(begin- e (... ...))
|
||||
'top-level
|
||||
'()))
|
||||
--------
|
||||
[≻ e-]])]))
|
||||
|
||||
(define-barrier %L L U->L)
|
||||
(define-barrier %U U L->U)
|
||||
|
||||
|
||||
; variable syntax
|
||||
(define-typed-variable-syntax
|
||||
#:datum-literals (:)
|
||||
[(_ x- : τ) ≫
|
||||
#:when (eq? (current-language) 'U)
|
||||
#:fail-unless (fully-unrestricted? #'τ)
|
||||
(raise-syntax-error #f "cannot use linear variable from unrestricted language" #'x-)
|
||||
--------
|
||||
[⊢ x- ⇒ τ]]
|
||||
|
||||
[(_ x- : σ) ≫
|
||||
#:when (eq? (current-language) 'L)
|
||||
--------
|
||||
[≻ (#%lin-var x- : σ)]])
|
||||
|
||||
; define syntax
|
||||
(define-typed-syntax define
|
||||
#:datum-literals (:)
|
||||
[(define (f [x:id : ty] ...) ret
|
||||
e ...+) ≫
|
||||
--------
|
||||
[≻ (define f : (→ ty ... ret)
|
||||
(letrec ([{f : (→ ty ... ret)}
|
||||
(λ (x ...)
|
||||
(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)))]])
|
||||
|
||||
|
||||
; REPL prints expression types
|
||||
; enter :lang=L or :lang=U to switch language in REPL
|
||||
(define-typed-syntax #%top-interaction
|
||||
[(_ . d) ≫
|
||||
#:when (regexp-match? #px":lang=L" (~a (syntax-e #'d)))
|
||||
#:do [(when (unrestricted-mode? (current-mode))
|
||||
(current-mode (U->L (current-mode))))]
|
||||
--------
|
||||
[≻ (#%app- void-)]]
|
||||
|
||||
[(_ . d) ≫
|
||||
#:when (regexp-match? #px":lang=U" (~a (syntax-e #'d)))
|
||||
#:do [(when (linear-mode? (current-mode))
|
||||
(current-mode (L->U (current-mode))))]
|
||||
--------
|
||||
[≻ (#%app- void-)]]
|
||||
|
||||
[(_ . e) ≫
|
||||
#:do [(printf "; language: ~a\n" (language-name))]
|
||||
[⊢ e ≫ e- ⇒ τ]
|
||||
--------
|
||||
[≻ (#%app- printf- '"~v : ~a\n" e- '#,(type->str #'τ))]])
|
||||
|
|
@ -5,6 +5,7 @@
|
|||
linear-type?
|
||||
unrestricted-type?
|
||||
|
||||
linear-mode?
|
||||
linear-scope
|
||||
linear-in-scope?
|
||||
linear-use-var!
|
||||
|
|
|
|||
75
turnstile/examples/tests/linear/fabul-tests.rkt
Normal file
75
turnstile/examples/tests/linear/fabul-tests.rkt
Normal file
|
|
@ -0,0 +1,75 @@
|
|||
#lang s-exp turnstile/examples/linear/fabul
|
||||
(require turnstile/rackunit-typechecking)
|
||||
|
||||
(%U (define birthday : (× Int Int Int)
|
||||
(tup 10 10 97)))
|
||||
|
||||
(%U (check-type birthday : (× Int Int Int)))
|
||||
(%L (check-type (%U birthday) : (⊗ Int Int Int) ⇒ (tup 10 10 97)))
|
||||
|
||||
(%U (typecheck-fail
|
||||
(%L (let ([bday (%U birthday)]) 0))
|
||||
#:with-msg "bday: linear variable unused"))
|
||||
|
||||
(%L (typecheck-fail
|
||||
(let ([x (%U birthday)]) (%U x))
|
||||
#:with-msg "x: cannot use linear variable from unrestricted language"))
|
||||
|
||||
(%L (check-type (let ([bday (%U birthday)])
|
||||
(%U (%L bday)))
|
||||
: (⊗ Int Int Int)))
|
||||
|
||||
(%L (check-type (%U (cons 1 (cons 2 (nil {Int}))))
|
||||
: (MList Int)
|
||||
⇒ (cons 1 (cons 2 (nil)))))
|
||||
|
||||
(%U (check-type (%L (cons 1 (cons 2 (nil))))
|
||||
: (List Int)
|
||||
⇒ (cons 1 (cons 2 (nil {Int})))))
|
||||
|
||||
(%L (check-type (let ([f (%U (λ () (cons 1 (nil {Int}))))]) f)
|
||||
: (→ (MList Int))))
|
||||
|
||||
(%L (check-type (let ([f (%U (λ () (cons 1 (nil {Int}))))]) (f))
|
||||
: (MList Int)
|
||||
⇒ (cons 1 (nil))))
|
||||
|
||||
|
||||
|
||||
(%L (define (partition [pred : (→ Int Bool)]
|
||||
[lst : (MList Int)]) (⊗ (MList Int) (MList Int))
|
||||
(match-list lst
|
||||
[(cons x xs @ l)
|
||||
(let* ([(yes no) (partition pred xs)])
|
||||
(if (pred x)
|
||||
(tup (cons x yes @ l) no)
|
||||
(tup yes (cons x no @ l))))]
|
||||
[(nil)
|
||||
(tup (nil {Int}) (nil {Int}))])))
|
||||
|
||||
(%L (check-type (partition (λ (n) (< n 3))
|
||||
(cons 1 (cons 2 (cons 4 (cons 5 (nil))))))
|
||||
: (⊗ (MList Int) (MList Int))
|
||||
⇒ (tup (cons 1 (cons 2 (nil)))
|
||||
(cons 4 (cons 5 (nil))))))
|
||||
|
||||
|
||||
(%L (define (mqsort [lst : (MList Int)] [acc : (MList Int)]) (MList Int)
|
||||
(match-list lst
|
||||
[(cons piv xs @ l)
|
||||
(let* ([(lt gt) (partition (λ (x) (< x piv)) xs)])
|
||||
(mqsort lt (cons piv (mqsort gt acc) @ l)))]
|
||||
[(nil) acc])))
|
||||
|
||||
(%L (check-type (mqsort (cons 4 (cons 7 (cons 2 (cons 1 (nil))))) (nil))
|
||||
: (MList Int)
|
||||
⇒ (cons 1 (cons 2 (cons 4 (cons 7 (nil)))))))
|
||||
|
||||
|
||||
|
||||
(%U (define (qsort [lst : (List Int)]) (List Int)
|
||||
(%L (mqsort (%U lst) (nil)))))
|
||||
|
||||
(%U (check-type (qsort (cons 4 (cons 7 (cons 2 (cons 1 (nil {Int}))))))
|
||||
: (List Int)
|
||||
⇒ (cons 1 (cons 2 (cons 4 (cons 7 (nil {Int})))))))
|
||||
Loading…
Reference in New Issue
Block a user