From 9f2de8067cb0da920fbf0c194256833d61149ffa Mon Sep 17 00:00:00 2001
From: Milo Turner <iitalics@gmail.com>
Date: Thu, 8 Jun 2017 15:06:23 -0400
Subject: [PATCH 1/4] var-transformer configurable thru #:var-stx keyword to
 (infer ...)

---
 macrotypes/typecheck.rkt | 84 ++++++++++++++++++++++++++++------------
 1 file changed, 60 insertions(+), 24 deletions(-)

diff --git a/macrotypes/typecheck.rkt b/macrotypes/typecheck.rkt
index bd554755..48063192 100644
--- a/macrotypes/typecheck.rkt
+++ b/macrotypes/typecheck.rkt
@@ -919,42 +919,78 @@
   ;;       but I'm not sure it properly generalizes
   ;;       eg, what if I need separate type-eval and kind-eval fns?
   ;; - should infer be moved into define-syntax-category?
-  (define (infer es #:ctx [ctx null] #:tvctx [tvctx null]
-                    #:tag [tag (current-tag)] ; the "type" to return from es
-                    #:expa [expa expand/df] ; used to expand e
-                    #:tev [tev #'(current-type-eval)]  ; type-eval (τ in ctx)
-                    #:key [kev #'(current-type-eval)]) ; kind-eval (tvk in tvctx)
-     (syntax-parse ctx
-       [((~or X:id [x:id (~seq sep:id τ) ...]) ...) ; dont expand; τ may reference to tv
-       #:with (~or (~and (tv:id ...)
+  ;; added: '#:var-stx lst' specifies the variable transformers used to bind
+  ;;   ctx in the expansion of the expressions.
+  ;; TODO: delete #:tev and #:kev?
+  (define (infer es
+                 #:tvctx [tvctx '()]
+                 #:ctx [ctx '()]
+                 #:tag [tag (current-tag)]
+                 #:expa [expa expand/df]
+                 #:tev [tev #'(current-type-eval)]
+                 #:kev [kev #'(current-type-eval)]
+                 #:var-stx [var-stxs (var-transformers-for-context ctx tag tev kev)])
+    (syntax-parse es
+      [(e ...)
+       #:with (var-stx ...) var-stxs
+       #:with (x ...) (stx-map (lambda (ctx-elem)
+                                 (if (identifier? ctx-elem)
+                                     ctx-elem
+                                     (stx-car ctx-elem)))
+                               ctx)
+       ; TODO: turnstile syntax no longer uses tvctx.
+       ; is it obsolete? should we just prepend tvctx to ctx?
+       #:with (~or ([tv:id (~seq tvsep:id tvk) ...] ...)
+                   (~and (tv:id ...)
                          (~parse ([(tvsep ...) (tvk ...)] ...)
-                                 (stx-map (λ _ #'[(::) (#%type)]) #'(tv ...))))
-                   ([tv (~seq tvsep:id tvk) ...] ...))
-                   tvctx
-       #:with (e ...) es
+                                 (stx-map (λ _ #'[(::) (#%type)]) #'(tv ...)))))
+              tvctx
        #:with ((~literal #%plain-lambda) tvs+
                (~let*-syntax
                 ((~literal #%expression)
                  ((~literal #%plain-lambda) xs+
                   (~let*-syntax
                    ((~literal #%expression) e+) ... (~literal void))))))
-        (expa
+       (expa
         #`(λ (tv ...)
-            (let*-syntax ([tv (make-rename-transformer
+            (let*-syntax ([tv (make-rename-transformer ; TODO: make this an argument too?
                                (mk-tyvar
                                 (attachs #'tv '(tvsep ...) #'(tvk ...)
                                          #:ev #,kev)))] ...)
-              (λ (X ... x ...)
-                (let*-syntax ([X (make-variable-like-transformer
-                                 (mk-tyvar (attach #'X ':: (#,kev #'#%type))))] ...
-                              [x (make-variable-like-transformer
-                                  (attachs #'x '(sep ...) #'(τ ...)
-                                           #:ev #,tev))] ...)
+              (λ (x ...)
+                (let*-syntax ([x var-stx] ...)
                   (#%expression e) ... void)))))
-       (list #'tvs+ #'xs+ 
-             #'(e+ ...) 
-             (stx-map (λ (e) (detach e tag)) #'(e+ ...)))]
-      [([x τ] ...) (infer es #:ctx #`([x #,tag τ] ...) #:tvctx tvctx #:tag tag)]))
+       (list #'tvs+
+             #'xs+
+             #'(e+ ...)
+             (stx-map (λ (e) (detach e tag)) #'(e+ ...)))]))
+
+  (define (var-transformers-for-context ctx tag tev kev)
+    (stx-map (syntax-parser
+               ; missing seperator
+               [[x:id τ] #'(VAR x : τ)]
+               ; seperators given
+               [[x:id . props] #'(VAR x . props)]
+               ; just variable; interpreted as type variable
+               [X:id #'(TYVAR X)])
+             ctx))
+
+  ; variable syntax for regular typed variables
+  (define-syntax VAR
+    (syntax-parser
+      [(_ x (~seq tag prop) ...)
+       #`(make-variable-like-transformer
+          (attachs #'x '(tag ...) #'(prop ...)
+                   #:ev (current-type-eval)))]))
+
+  ; variable syntax for regular kinded type variables
+  (define-syntax TYVAR
+    (syntax-parser
+      [(_ X)
+       #`(make-variable-like-transformer
+          (mk-tyvar (attach #'X ':: ((current-type-eval) #'#%type))))]))
+
+  
 
   ;; fns derived from infer ---------------------------------------------------
   ;; some are syntactic shortcuts, some are for backwards compat

From cb42c24c59a288ebd146f2b766e55ceaeff4ec7c Mon Sep 17 00:00:00 2001
From: Milo Turner <iitalics@gmail.com>
Date: Thu, 8 Jun 2017 15:07:13 -0400
Subject: [PATCH 2/4] rewrote turnstile clause syntax; more intuitive + access
 to var-stx

---
 turnstile/turnstile.rkt | 393 +++++++++++++++++++++++-----------------
 1 file changed, 225 insertions(+), 168 deletions(-)

diff --git a/turnstile/turnstile.rkt b/turnstile/turnstile.rkt
index b6981ff1..d90a0450 100644
--- a/turnstile/turnstile.rkt
+++ b/turnstile/turnstile.rkt
@@ -21,34 +21,88 @@
   (require (for-meta -1 (except-in macrotypes/typecheck #%module-begin))
            (only-in lens/common lens-view lens-set)
            (only-in lens/private/syntax/stx stx-flatten/depth-lens))
-  ;; infer/depth returns a list of three values:
-  ;;   tvxs- ; a stx-list of the expanded versions of type variables in the tvctx
-  ;;   xs-   ; a stx-list of the expanded versions of variables in the ctx
-  ;;   es*-  ; a nested list a depth given by the depth argument, with the same structure
-  ;;         ; as es*, containing the expanded es*, with the types attached
-  (define (infer/depth #:ctx ctx #:tvctx tvctx depth es* origs*
-                       #:tag [tag (current-tag)])
-    (define flat (stx-flatten/depth-lens depth))
-    (define es (lens-view flat es*))
-    (define origs (lens-view flat origs*))
-    (define/with-syntax [tvxs- xs- es- _]
-      (infer #:tvctx tvctx #:ctx ctx (stx-map pass-orig es origs) #:tag tag))
-    (define es*- (lens-set flat es* #`es-))
-    (list #'tvxs- #'xs- es*-))
-  ;; infers/depths
-  (define (infers/depths clause-depth tc-depth tvctxs/ctxs/ess/origss*
-                         #:tag [tag (current-tag)])
-    (define flat (stx-flatten/depth-lens clause-depth))
-    (define tvctxs/ctxs/ess/origss
-      (lens-view flat tvctxs/ctxs/ess/origss*))
-    (define tcs
-      (for/list ([tvctx/ctx/es/origs (in-list (stx->list tvctxs/ctxs/ess/origss))])
-        (match-define (list tvctx ctx es origs)
-          (stx->list tvctx/ctx/es/origs))
-        (infer/depth #:tvctx tvctx #:ctx ctx tc-depth es origs #:tag tag)))
-    (define res
-      (lens-set flat tvctxs/ctxs/ess/origss* tcs))
-    res)
+
+  ; stx-map/depth : int (stx -> stx) stx-tree -> stx-tree
+  (define (stx-map/depth d fn stx)
+    (cond
+      [(zero? d) (fn stx)]
+      [(stx-null? stx) stx]
+      [else
+       (cons (stx-map/depth (sub1 d) fn (stx-car stx))
+             (stx-map/depth d        fn (stx-cdr stx)))]))
+
+  ; stx-flat/depths : (listof int) (stx-listof stx-tree) -> (listof stx-elem)
+  (define (stx-flat/depths ds stxs)
+    (define (flat d stx)
+      (cond
+        [(zero? d) (list stx)]
+        [(stx-null? stx) '()]
+        [else
+         (append (flat (sub1 d) (stx-car stx))
+                 (flat d        (stx-cdr stx)))]))
+    (append* (stx-map flat ds stxs)))
+
+  ; stx-unflatten/depths : (listof int) (stx-listof stx-tree) (listof stx-elem)
+  ;                          -> (stx-listof stx-tree)
+  (define (stx-unflatten/depths ds origs lst)
+    (define (next)
+      (begin0 (stx-car lst)
+        (set! lst (stx-cdr lst))))
+    (define (unflat d orig)
+      (cond
+        [(zero? d) (next)]
+        [(stx-null? orig) orig]
+        [else
+         ; TODO: removed datum->syntax ?
+         ;   this is a likely futile effort to improve error msgs in
+         ;   case something goes wrong.
+         (datum->syntax (if (syntax? orig) orig #f)
+          (cons (unflat (sub1 d) (stx-car orig))
+                (unflat d        (stx-cdr orig))))]))
+    (datum->syntax (if (syntax? origs) origs #f)
+     (stx-map unflat ds origs)))
+
+
+  ; invokes (infer ...) ONCE on the given expressions, context and var syntax,
+  ; retaining the shape according to es-deps, ctx-deps and the shapes of
+  ; the given syntax
+  ; returns a list of two values, the expanded variables (x- ...) and the
+  ; expanded expressions (e- ...)
+  ; => (xs- es-)
+  (define (infer/depths ctx-deps es-deps
+                        #:vars vars
+                        #:ctx ctx
+                        #:exprs es
+                        #:origs origs
+                        #:tag tag)
+    (syntax-parse (infer (stx-map pass-orig
+                                  (stx-flat/depths es-deps es)
+                                  (stx-flat/depths es-deps origs))
+                         #:ctx (stx-flat/depths ctx-deps ctx)
+                         #:var-stx (stx-flat/depths ctx-deps vars)
+                         #:tag tag)
+      [(_ xs+ es+ _)
+       (list (stx-unflatten/depths ctx-deps ctx #'xs+)
+             (stx-unflatten/depths es-deps es #'es+))]))
+
+  ; invokes (infer ...) many times, for each var/ctx/expr/orig group in the
+  ; given structure (with given depth = dep). retains the shape but transforms
+  ; each leaf into (xs- es-), per the behavior of infer/depths function
+  (define (infers/depths dep
+                         ctx-deps es-deps
+                         v/c/e/os
+                         #:tag tag)
+    (stx-map/depth dep
+                   (syntax-parser
+                     [(vars ctx es origs)
+                      (infer/depths ctx-deps es-deps
+                                    #:vars #'vars
+                                    #:ctx #'ctx
+                                    #:exprs #'es
+                                    #:origs #'origs
+                                    #:tag tag)])
+                   v/c/e/os))
+
   (define (raise-⇐-expected-type-error ⇐-stx body expected-type existing-type)
     (raise-syntax-error
      '⇐
@@ -61,6 +115,7 @@
              (type->str existing-type))
      ⇐-stx
      body)))
+
 (module syntax-classes racket/base
   (provide (all-defined-out))
   (require (for-meta 0 (submod ".." typecheck+))
@@ -75,6 +130,7 @@
                            "expected a separator consisting of dashes"
              #:fail-unless (>= (string-length str-dashes) 3)
                            "expected a separator of three or more dashes"])
+
   (define-syntax-class elipsis
     [pattern (~literal ...)])
 
@@ -85,50 +141,35 @@
            (with-depth (list stx (stx-car elipses))
                        (stx-cdr elipses))]))
 
-  ;; add-lists : Any Natural -> Any
-  (define (add-lists stx n)
-    (cond [(zero? n) stx]
-          [else (add-lists (list stx) (sub1 n))]))
-  
-  (define-splicing-syntax-class props
-    [pattern (~and (~seq stuff ...) (~seq (~seq k:id v) ...))])
-  (define-splicing-syntax-class ⇒-prop
+  ; matches a list of tag/type properties
+  (define-syntax-class props
+    [pattern [(~seq tag:id prop) ...]])
+
+  ; matches ⇒ pattern, surrounded in parenthesis, e.g. (⇒ : τ) or (⇒ τ)
+  (define-syntax-class ⇒-prop
+    #:attributes (e-pat) ; e-pat = pattern to apply to expanded form
     #:datum-literals (⇒)
-    #:attributes (e-pat)
-    [pattern (~or (~seq ⇒ tag-pat ; implicit tag
-                          (~parse tag #',(current-tag))
-                          (tag-prop:⇒-prop) ...)
-                  (~seq ⇒ tag:id tag-pat (tag-prop:⇒-prop) ...)) ; explicit tag
+    [pattern (~or (~and (⇒ tag:id prop-pat inner:⇒-prop ...))
+                  (~and (⇒        prop-pat inner:⇒-prop ...) (~parse tag #',(current-tag))))
              #:with e-tmp (generate-temporary)
              #:with e-pat
              #'(~and e-tmp
-                     (~parse
-                      (~and tag-prop.e-pat ... tag-pat)
-                      (detach #'e-tmp `tag)))])
-  (define-splicing-syntax-class ⇒-prop/conclusion
-    #:datum-literals (⇒)
-    #:attributes (tag tag-expr)
-    [pattern (~or (~seq ⇒ tag-stx ; implicit tag
-                          (~parse tag #',(current-tag))
-                          (~parse (tag-prop.tag ...) #'())
-                          (~parse (tag-prop.tag-expr ...) #'()))
-                  (~seq ⇒ tag:id tag-stx (tag-prop:⇒-prop/conclusion) ...))
-             #:with tag-expr
-             (for/fold ([tag-expr #'#`tag-stx])
-                       ([k (in-stx-list #'[tag-prop.tag ...])]
-                        [v (in-stx-list #'[tag-prop.tag-expr ...])])
-               (with-syntax ([tag-expr tag-expr] [k k] [v v])
-                 #'(attach tag-expr `k ((current-ev) v))))])
-  (define-splicing-syntax-class ⇐-prop
+                     (~parse (~and inner.e-pat ... prop-pat)
+                             (detach #'e-tmp `tag)))])
+
+  ; matches ⇐ pattern, surrounded in parenthesis, e.g. (⇐ : τ) or (⇐ τ)
+  ; the .type attribute contains τ in the above examples, and the .e-pat
+  ; attribute contains patterns to apply to expanded form
+  (define-syntax-class ⇐-prop
+    #:attributes (type e-pat)
     #:datum-literals (⇐)
-    #:attributes (τ-stx e-pat)
-    [pattern (~or (~seq ⇐ τ-stx (~parse tag #',(current-tag)))
-                  (~seq ⇐ tag:id τ-stx))
+    [pattern (~or (~and (⇐ tag:id type))
+                  (~and (⇐        type) (~parse tag #',(current-tag))))
              #:with e-tmp (generate-temporary)
-             #:with τ-tmp (generate-temporary)
              #:with τ-exp (generate-temporary)
+             #:with τ-tmp (generate-temporary)
              #:with e-pat
-             #`(~and e-tmp
+             #'(~and e-tmp
                      (~parse τ-exp (get-expected-type #'e-tmp))
                      (~parse τ-tmp (detach #'e-tmp `tag))
                      (~parse
@@ -137,115 +178,106 @@
                                           (get-orig #'e-tmp))
                               (typecheck-fail-msg/1 #'τ-exp #'τ-tmp #'e-tmp)))
                       (get-orig #'e-tmp)))])
-  (define-splicing-syntax-class ⇒-props
-    #:attributes (e-pat)
-    [pattern (~seq :⇒-prop)]
-    [pattern (~seq (p:⇒-prop) ...)
-             #:with e-pat #'(~and p.e-pat ...)])
-  (define-splicing-syntax-class ⇐-props
-    #:attributes (τ-stx e-pat)
-    [pattern (~seq :⇐-prop)]
-    [pattern (~seq (p:⇐-prop) (p2:⇒-prop) ...)
-             #:with τ-stx #'p.τ-stx
-             #:with e-pat #'(~and p.e-pat p2.e-pat ...)])
-  (define-splicing-syntax-class ⇒-props/conclusion
-    #:attributes ([tag 1] [tag-expr 1])
-    [pattern (~seq p:⇒-prop/conclusion)
-             #:with [tag ...] #'[p.tag]
-             #:with [tag-expr ...] #'[p.tag-expr]]
-    [pattern (~seq (:⇒-prop/conclusion) ...+)])
-  (define-splicing-syntax-class id+props+≫
+
+  ;; clause for the entire context (lhs of ⊢)
+  (define-syntax-class tc-context
+    #:attributes ([deps 1] vars ctx pat)
     #:datum-literals (≫)
-    #:attributes ([x- 1] [ctx 1])
-    [pattern (~seq (~and X:id (~not _:elipsis)))
-             #:with [x- ...] #'[_]
-             #:with [ctx ...] #'[[X :: #%type]]]
-    [pattern (~seq X:id ooo:elipsis)
-             #:with [x- ...] #'[_ ooo]
-             #:with [ctx ...] #'[[X :: #%type] ooo]]
-    [pattern (~seq [x:id ≫ x--:id props:props])
-             #:with [x- ...] #'[x--]
-             #:with [ctx ...] #'[[x props.stuff ...]]]
-    [pattern (~seq [x:id ≫ x--:id props:props] ooo:elipsis)
-             #:with [x- ...] #'[x-- ooo]
-             #:with [ctx ...] #'[[x props.stuff ...] ooo]])
-  (define-splicing-syntax-class id-props+≫*
-    #:attributes ([x- 1] [ctx 1])
-    [pattern (~seq ctx1:id+props+≫ ...)
-             #:with [x- ...] #'[ctx1.x- ... ...]
-             #:with [ctx ...] #'[ctx1.ctx ... ...]])
-  (define-syntax-class tc-elem
-    #:datum-literals (⊢ ⇒ ⇐ ≫)
-    #:attributes (e-stx e-stx-orig e-pat)
-    [pattern [e-stx ≫ e-pat* props:⇒-props]
-             #:with e-stx-orig #'e-stx
-             #:with e-pat #'(~and props.e-pat e-pat*)]
-    [pattern [e-stx* ≫ e-pat* props:⇐-props]
-             #:with e-tmp (generate-temporary #'e-pat*)
-             #:with τ-tmp (generate-temporary 'τ)
-             #:with τ-exp-tmp (generate-temporary 'τ_expected)
-             #:with e-stx #'(add-expected e-stx* props.τ-stx)
-             #:with e-stx-orig #'e-stx*
-             #:with e-pat #'(~and props.e-pat e-pat*)])
-  (define-splicing-syntax-class tc
-    #:attributes (depth es-stx es-stx-orig es-pat)
-    [pattern (~seq tc:tc-elem ooo:elipsis ...)
-             #:with depth (stx-length #'[ooo ...])
-             #:with es-stx (with-depth #'tc.e-stx #'[ooo ...])
-             #:with es-stx-orig (with-depth #'tc.e-stx-orig #'[ooo ...])
-             #:with es-pat
-             #`(~post
-                #,(with-depth #'tc.e-pat #'[ooo ...]))])
-  (define-syntax-class tc*
-    #:attributes (depth es-stx es-stx-orig es-pat)
-    [pattern tc:tc-elem
-             #:with depth 0
-             #:with es-stx #'tc.e-stx
-             #:with es-stx-orig #'tc.e-stx-orig
-             #:with es-pat #'tc.e-pat]
-    [pattern (tc:tc ...)
-             #:do [(define ds (stx-map syntax-e #'[tc.depth ...]))
-                   (define max-d (apply max 0 ds))]
-             #:with depth (add1 max-d)
-             #:with [[es-stx* es-stx-orig* es-pat*] ...]
-             (for/list ([tc-es-stx (in-stx-list #'[tc.es-stx ...])]
-                        [tc-es-stx-orig (in-stx-list #'[tc.es-stx-orig ...])]
-                        [tc-es-pat (in-stx-list #'[tc.es-pat ...])]
-                        [d (in-list ds)])
-               (list
-                (add-lists tc-es-stx (- max-d d))
-                (add-lists tc-es-stx-orig (- max-d d))
-                (add-lists tc-es-pat (- max-d d))))
-             #:with es-stx #'[es-stx* ...]
-             #:with es-stx-orig #'[es-stx-orig* ...]
-             #:with es-pat #'[es-pat* ...]])
+    ; consecutive context elems
+    [pattern [(~seq ce:ctx-elem ~! ooo:elipsis ...) ...]
+             #:with (deps ...) (stx-map stx-length #'([ooo ...] ...))
+             #:with vars (stx-map with-depth #'(ce.var-stx ...) #'([ooo ...] ...))
+             #:with ctx  (stx-map with-depth #'(ce.x+props ...) #'([ooo ...] ...))
+             #:with pat  (stx-map with-depth #'(ce.pat ...)     #'([ooo ...] ...))]
+    ; groups contexts, e.g. [(X Y) [x ≫ x- : t] ... ⊢ ...]
+    ; NOTE:
+    ;  some grouping, e.g. [[x ≫ x-] (X Y) ⊢ ...] doesn't work. but this is never
+    ;  done in any examples. try to implement or not?
+    [pattern [c1:tc-context . c2:tc-context]
+             #:with (deps ...) #'(c1.deps ... c2.deps ...)
+             #:with vars (append (stx->list #'c1.vars) (stx->list #'c2.vars))
+             #:with ctx  (append (stx->list #'c1.ctx) (stx->list #'c2.ctx))
+             #:with pat  (append (stx->list #'c1.pat) (stx->list #'c2.pat))])
+
+  ;; single context element; variable [x ≫ x-] or type variable X
+  ;; note: new syntax: [MACRO x ≫ x-] allows the variable transformer to
+  ;; be overriden. in fact, a lone X is just syntax sugar for [TYVAR X ≫ _]
+  (define-syntax-class ctx-elem
+    #:attributes (var-stx x+props pat)
+    #:datum-literals (≫)
+    [pattern [x:id ≫ ~! pat . props:props]
+             #:with var-stx #'(VAR x . props)
+             #:with x+props #'(x . props)]
+    [pattern [mac:id x:id ≫ ~! pat . props:props]
+             #:with var-stx #'(mac x . props)
+             #:with x+props #'(x . props)]
+    [pattern (~and X:id (~not (~var _ elipsis)))
+             #:with var-stx #'(TYVAR X)
+             #:with x+props #'X
+             #:with pat #'_])
+
+  ;; list of type clauses under a context (rhs of ⊢)
+  (define-syntax-class tcs
+    #:attributes ([deps 1] es origs pat)
+    ; multiple clauses, e.g. [... ⊢ [e1 ≫ e1-] [e2 ≫ e2-]]
+    [pattern [(~seq tc:tc ooo:elipsis ...) ...]
+             #:with (deps ...) (stx-map stx-length #'([ooo ...] ...))
+             #:with es    (stx-map with-depth #'(tc.tem ...) #'([ooo ...] ...))
+             #:with origs (stx-map with-depth #'(tc.stx ...) #'([ooo ...] ...))
+             #:with pat   (stx-map with-depth #'(tc.pat ...) #'([ooo ...] ...))]
+    ; single clause, e.g. [... ⊢ e1 ≫ e1-]
+    [pattern tc:tc
+             #:with (deps ...) '(0)
+             #:with es    #'(tc.tem)
+             #:with origs #'(tc.stx)
+             #:with pat   #'(tc.pat)])
+
+  ;; single type clause ( e ≫ e- ...)
+  (define-syntax-class tc
+    #:attributes (stx tem pat)
+    #:datum-literals (≫ ⇒ ⇐)
+    ; synthesis (match the output type)
+    [pattern [stx ≫ expa . out:⇒-prop]
+             #:with tem #'stx
+             #:with pat #'(~and expa out.e-pat)]
+    [pattern [stx ≫ expa out:⇒-prop ...]
+             #:with tem #'stx
+             #:with pat #'(~and expa out.e-pat ...)]
+    ; checking
+    [pattern [stx ≫ expa . chk:⇐-prop]
+             #:with tem #'(add-expected stx chk.type)
+             #:with pat #'(~and expa chk.e-pat)]
+    ; both
+    [pattern [stx ≫ expa chk:⇐-prop out:⇒-prop ...]
+             #:with tem #'(add-expected stx chk.type)
+             #:with pat #'(~and expa
+                                chk.e-pat
+                                out.e-pat ...)])
+
+  ;; clause with a turnstile in the middle, and possibly ellipsis at the end
   (define-splicing-syntax-class tc-clause
     #:attributes (pat)
-    #:datum-literals (⊢)
-    [pattern (~or (~seq [⊢ . tc:tc*] ooo:elipsis ...
-                        (~parse ((ctx.x- ctx.ctx tvctx.x- tvctx.ctx) ...) #'()))
-                  (~seq [ctx:id-props+≫* ⊢ . tc:tc*] ooo:elipsis ...
-                        (~parse ((tvctx.x- tvctx.ctx) ...) #'()))
-                  (~seq [(ctx:id-props+≫*) ⊢ . tc:tc*] ooo:elipsis ...
-                        (~parse ((tvctx.x- tvctx.ctx) ...) #'()))
-                  (~seq [(tvctx:id-props+≫*) (ctx:id-props+≫*) ⊢ . tc:tc*] ooo:elipsis ...))
-             #:with clause-depth (stx-length #'[ooo ...])
-             #:with tcs-pat
-             (with-depth
-              #'[(tvctx.x- ...) (ctx.x- ...) tc.es-pat]
-              #'[ooo ...])
-             #:with tvctxs/ctxs/ess/origs
-             (with-depth
-              #`[(tvctx.ctx ...) (ctx.ctx ...) tc.es-stx tc.es-stx-orig]
-              #'[ooo ...])
+    #:datum-literals (⊢ ≫)
+    [pattern (~seq [l ... ⊢ ~! . rhs:tcs] ooo:elipsis ...)
+             ; TODO: the [l ...] pattern makes things easy but may produce slightly
+             ; confusing error messages, since the error will refer to the parenthesized
+             ; (l ...) which never technically appears inyour code.
+             #:with lhs:tc-context #'[l ...]
+             #:with dep (stx-length #'[ooo ...])
+             #:with vars/ctx/es/origs
+             (with-depth #'(lhs.vars lhs.ctx rhs.es rhs.origs) #'[ooo ...])
+             #:with xs/es-pats
+             (with-depth #'(lhs.pat rhs.pat) #'[ooo ...])
              #:with pat
-             #`(~post
+             #'(~post
                 (~post
-                 (~parse
-                  tcs-pat
-                  (infers/depths 'clause-depth 'tc.depth #`tvctxs/ctxs/ess/origs
-                                 #:tag (current-tag)))))]
-    )
+                 (~parse xs/es-pats
+                         (infers/depths 'dep
+                                        '(lhs.deps ...)
+                                        '(rhs.deps ...)
+                                        #`vars/ctx/es/origs
+                                        #:tag (current-tag)))))])
+
   (define-splicing-syntax-class clause
     #:attributes (pat)
     #:datum-literals (τ⊑ τ=) ; TODO: drop the τ in τ⊑ and τ=
@@ -306,6 +338,28 @@
              #:with pat
              #'(~post (~fail #:unless condition message))]
     )
+
+  (define-splicing-syntax-class ⇒-prop/conclusion
+    #:datum-literals (⇒)
+    #:attributes (tag tag-expr)
+    [pattern (~or (~seq ⇒ tag-stx ; implicit tag
+                          (~parse tag #',(current-tag))
+                          (~parse (tag-prop.tag ...) #'())
+                          (~parse (tag-prop.tag-expr ...) #'()))
+                  (~seq ⇒ tag:id tag-stx (tag-prop:⇒-prop/conclusion) ...))
+             #:with tag-expr
+             (for/fold ([tag-expr #'#`tag-stx])
+                       ([k (in-stx-list #'[tag-prop.tag ...])]
+                        [v (in-stx-list #'[tag-prop.tag-expr ...])])
+               (with-syntax ([tag-expr tag-expr] [k k] [v v])
+                 #'(attach tag-expr `k ((current-ev) v))))])
+  (define-splicing-syntax-class ⇒-props/conclusion
+    #:attributes ([tag 1] [tag-expr 1])
+    [pattern (~seq p:⇒-prop/conclusion)
+             #:with [tag ...] #'[p.tag]
+             #:with [tag-expr ...] #'[p.tag-expr]]
+    [pattern (~seq (:⇒-prop/conclusion) ...+)])
+
   (define-syntax-class last-clause
     #:datum-literals (⊢ ≫ ≻ ⇒ ⇐)
     #:attributes ([pat 0] [stuff 1] [body 0])
@@ -361,6 +415,7 @@
              #:with body:expr
              ;; should never get here
              #'(error msg)])
+
   (define-splicing-syntax-class pat #:datum-literals (⇐)
     [pattern (~seq pat)
              #:attr transform-body identity]
@@ -383,6 +438,7 @@
                    (when (and ty-b (not (check? ty-b #'τ)))
                      (raise-⇐-expected-type-error #'left b #'τ ty-b))
                    (attach b `tag #'τ)))])
+
   (define-syntax-class rule #:datum-literals (≫)
     [pattern [pat:pat ≫
               clause:clause ...
@@ -400,6 +456,7 @@
                         (~seq :keyword))
                    ...)])
   )
+
 (require (for-meta 1 'syntax-classes)
          (for-meta 2 'syntax-classes))
 

From a46c66a7c690d80bbfb76c6af37243a11a3e4597 Mon Sep 17 00:00:00 2001
From: Milo Turner <iitalics@gmail.com>
Date: Mon, 12 Jun 2017 14:16:16 -0400
Subject: [PATCH 3/4] added phase-0 syntax `define-typed-variable-syntax`

---
 turnstile/turnstile.rkt | 33 ++++++++++++++++++++++++++++++++-
 1 file changed, 32 insertions(+), 1 deletion(-)

diff --git a/turnstile/turnstile.rkt b/turnstile/turnstile.rkt
index d90a0450..bfaf9033 100644
--- a/turnstile/turnstile.rkt
+++ b/turnstile/turnstile.rkt
@@ -1,8 +1,9 @@
 #lang racket/base
 
-(provide (except-out (all-from-out macrotypes/typecheck) 
+(provide (except-out (all-from-out macrotypes/typecheck)
                      -define-typed-syntax -define-syntax-category)
          define-typed-syntax define-syntax-category
+         define-typed-variable-syntax
          (rename-out [define-typed-syntax define-typerule]
                      [define-typed-syntax define-syntax/typecheck])
          (for-syntax syntax-parse/typecheck
@@ -527,3 +528,33 @@
                                [current-tag 'key1])
                   (syntax-parse/typecheck stx kw-stuff (... ...)
                     rule (... ...))))])))]))
+
+(define-syntax define-typed-variable-syntax
+  (syntax-parser
+    [(_ (NAME:id orig-var-pat . props-pat)
+        (~and (~seq kw-stuff ...) :stxparse-kws)
+        rule ...+)
+     #:with ((~seq tag:id _) ...) #'props-pat
+     #:with make-transformer (generate-temporary #'name)
+     #:with invalid-invok-str (format "invalid invocation of var, expected tags: ~a"
+                                      (syntax->datum #'(tag ...)))
+     #'(begin-for-syntax
+         (define (make-transformer stx)
+           (syntax-parse stx
+             #:datum-literals (tag ...)
+             [(orig-var-pat . props-pat)
+              (make-set!-transformer
+               (syntax-parser
+                 [(~var _ identifier)
+                  (syntax-parse/typecheck this-syntax
+                                          kw-stuff ...
+                                          rule ...)]
+                 [(id . args)
+                  #:with ap (datum->syntax this-syntax '#%app)
+                  (syntax/loc this-syntax (ap id . args))]))]
+             [_
+              (raise-syntax-error #f 'invalid-invok-str this-syntax)]))
+         (define-syntax (NAME stx)
+           (syntax-case stx ()
+             [(_ . args)
+              #'(make-transformer #'args)])))]))

From 6891da26675beb94f56017644baf74266fafb391 Mon Sep 17 00:00:00 2001
From: Milo Turner <iitalics@gmail.com>
Date: Tue, 13 Jun 2017 13:04:21 -0400
Subject: [PATCH 4/4] create example linear language + tests

---
 turnstile/examples/linear.rkt             | 191 ++++++++++++++++++++++
 turnstile/examples/tests/linear-tests.rkt |  62 +++++++
 2 files changed, 253 insertions(+)
 create mode 100644 turnstile/examples/linear.rkt
 create mode 100644 turnstile/examples/tests/linear-tests.rkt

diff --git a/turnstile/examples/linear.rkt b/turnstile/examples/linear.rkt
new file mode 100644
index 00000000..761676b2
--- /dev/null
+++ b/turnstile/examples/linear.rkt
@@ -0,0 +1,191 @@
+#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-variable-syntax (LIN x- : σ)
+  [x ≫
+   #:when (unrestricted-type? #'σ)
+   --------
+   [⊢ x- ⇒ σ]]
+  [x ≫
+   #:do [(use-lin-var #'x-)]
+   --------
+   [⊢ x- ⇒ σ]])
+
+
+(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- ⇒ σ] ...]
+   [[LIN 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 ...)
+   [[LIN 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 ...)
+   [[LIN 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-) ⇒ σ]])
diff --git a/turnstile/examples/tests/linear-tests.rkt b/turnstile/examples/tests/linear-tests.rkt
new file mode 100644
index 00000000..6eb36e81
--- /dev/null
+++ b/turnstile/examples/tests/linear-tests.rkt
@@ -0,0 +1,62 @@
+#lang s-exp "../linear.rkt"
+(require "rackunit-typechecking.rkt")
+(require (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\n  at: p")
+
+
+(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")