www

commit fe5adac3db0e5814e3b8c374ea8b9ec08c6249e3
parent 39be2ef9044cd9816a11fc8400cd8732a14de7e8
Author: Milo Turner <iitalics@gmail.com>
Date:   Mon, 10 Jul 2017 13:09:08 -0400

add `define-typed-variable-syntax`

closes #13

Diffstat:
M
macrotypes/typecheck.rkt
 | 
10
++++++++++
M
turnstile/examples/linear-var-assign.rkt
 | 
14
+++-----------
M
turnstile/turnstile.rkt
 | 
14
+++++++++++++-

3 files changed, 26 insertions(+), 12 deletions(-)
diff --git 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
@@ -99,22 +99,14 @@
   )
 
 
-(define-typed-syntax #%linear
-  #:datum-literals (:)
-  [(_ x- : σ) ≫
+(define-typed-variable-syntax
+  #:datum-literals [:]
+  [(_ x- : σ) ≫ ; record use when σ restricted
    #: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) ≫
diff --git 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