diff --git a/macrotypes/typecheck.rkt b/macrotypes/typecheck.rkt index 1db8ae3..07315e7 100644 --- a/macrotypes/typecheck.rkt +++ b/macrotypes/typecheck.rkt @@ -788,6 +788,16 @@ (define (var-assign x seps τs) (attachs x seps τs #:ev (current-type-eval))) + ;; macro-var-assign : Id -> (Id (Listof Sym) (StxListof TypeStx) -> Stx) + ;; generate a function for current-var-assign that expands + ;; to an invocation of the macro by the given identifier + ;; e.g. + ;; > (current-var-assign (macro-var-assign #'foo)) + ;; > ((current-var-assign) #'x '(:) #'(τ)) + ;; #'(foo x : τ) + (define ((macro-var-assign mac-id) x seps τs) + (datum->syntax x `(,mac-id ,x . ,(stx-appendmap list seps τs)))) + ;; current-var-assign : ;; (Parameterof [Id (Listof Sym) (StxListof TypeStx) -> Stx]) (define current-var-assign diff --git a/turnstile/examples/linear-var-assign.rkt b/turnstile/examples/linear-var-assign.rkt index 7b69382..9222634 100644 --- a/turnstile/examples/linear-var-assign.rkt +++ b/turnstile/examples/linear-var-assign.rkt @@ -99,22 +99,14 @@ ) -(define-typed-syntax #%linear - #:datum-literals (:) +(define-typed-variable-syntax + #:datum-literals [:] [(_ x- : σ) ≫ #:do [(unless (unrestricted-type? #'σ) (use-linear-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) - #`(#%linear #,x #,@(stx-append-map list seps types))))) - (define-typed-syntax begin [(_ e ... e0) ≫ @@ -122,7 +114,6 @@ -------- [⊢ (begin- e- ... e0-) ⇒ σ]]) - (define-typed-syntax tup [(_ e1 e2) ≫ [⊢ e1 ≫ e1- ⇒ σ1] @@ -130,7 +121,6 @@ -------- [⊢ (#%app- list- e1- e2-) ⇒ (⊗ σ1 σ2)]]) - (define-typed-syntax let [(let ([x rhs] ...) e) ≫ [⊢ [rhs ≫ rhs- ⇒ σ] ...] diff --git a/turnstile/turnstile.rkt b/turnstile/turnstile.rkt index 781da99..c6e1212 100644 --- a/turnstile/turnstile.rkt +++ b/turnstile/turnstile.rkt @@ -2,7 +2,9 @@ (provide (except-out (all-from-out macrotypes/typecheck) -define-typed-syntax -define-syntax-category) - define-typed-syntax define-syntax-category + define-typed-syntax + define-typed-variable-syntax + define-syntax-category (rename-out [define-typed-syntax define-typerule] [define-typed-syntax define-syntax/typecheck]) (for-syntax syntax-parse/typecheck @@ -468,6 +470,16 @@ [current-tag (type-key1)]) (syntax-parse/typecheck stx kw-stuff ... rule ...)))])) +(define-syntax define-typed-variable-syntax + (syntax-parser + [(_ (~optional (~seq #:name name:id) #:defaults ([name (generate-temporary '#%var)])) + (~and (~seq kw-stuff ...) :stxparse-kws) + rule:rule ...+) + #'(begin + (define-typed-syntax name kw-stuff ... rule ...) + (begin-for-syntax + (current-var-assign (macro-var-assign #'name))))])) + (define-syntax define-syntax-category (syntax-parser [(_ name:id) ; default key1 = ': for types