add example of linear language + tests

(Based on @iitalics work in pull request 11)

macrotypes/typecheck.rkt

@@ -788,16 +788,6 @@
   (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

turnstile/examples/linear-var-assign.rkt

@@ -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-) ⇒ σ]])

turnstile/examples/linear/fabul-utils.rkt

@@ -1,71 +0,0 @@
-#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)]))

turnstile/examples/linear/fabul.rkt

@@ -1,241 +0,0 @@
-#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 #'τ))]])

turnstile/examples/linear/lin+chan.rkt

@@ -1,61 +0,0 @@
-#lang turnstile/lang
-(extends "lin+tup.rkt")
-
-(provide (type-out InChan OutChan)
-         make-channel channel-put channel-get
-         thread sleep)
-
-(define-type-constructor InChan #:arity = 1)
-(define-type-constructor OutChan #:arity = 1)
-
-(begin-for-syntax
-  (current-linear-type? (or/c InChan? (current-linear-type?))))
-
-
-(define-typed-syntax make-channel
-  [(_ {ty:type}) ≫
-   #:with σ #'ty.norm
-   #:with tmp (generate-temporary)
-   --------
-   [⊢ (let ([tmp (#%app- make-channel-)])
-            (list tmp tmp))
-      ⇒ (⊗ (InChan σ) (OutChan σ))]])
-
-
-(define-typed-syntax channel-put
-  [(_ ch e) ≫
-   [⊢ ch ≫ ch- ⇒ (~OutChan σ)]
-   [⊢ e ≫ e- ⇐ σ]
-   --------
-   [⊢ (channel-put- ch- e-) ⇒ Unit]])
-
-
-(define-typed-syntax channel-get
-  [(_ ch) ≫
-   [⊢ ch ≫ ch- ⇒ (~InChan σ)]
-   #:with tmp (generate-temporary #'ch)
-   --------
-   [⊢ (let ([tmp ch-])
-            (list tmp (channel-get- tmp)))
-      ⇒ (⊗ (InChan σ) σ)]])
-
-
-(define-typed-syntax thread
-  [(_ f) ≫
-   [⊢ f ≫ f- ⇒ (~-o _)]
-   --------
-   [⊢ (void (thread- f-)) ⇒ Unit]])
-
-
-(define-typed-syntax sleep
-  [(_) ≫
-   --------
-   [⊢ (sleep-) ⇒ Unit]]
-
-  [(_ e) ≫
-   [⊢ e ≫ e- ⇒ σ]
-   #:fail-unless (or (Int? #'σ)
-                     (Float? #'σ))
-   "invalid sleep time, expected Int or Float"
-   --------
-   [⊢ (sleep- e-) ⇒ Unit]])

turnstile/examples/linear/lin+cons.rkt

@@ -1,80 +0,0 @@
-#lang turnstile/lang
-(extends "lin+tup.rkt")
-
-(provide (type-out MList MList0)
-         cons nil match-list)
-
-(define-type-constructor MList #:arity = 1)
-(define-base-type MList0)
-
-(begin-for-syntax
-  (current-linear-type? (or/c MList? MList0? (current-linear-type?))))
-
-
-(define-typed-syntax cons
-  #:datum-literals (@)
-
-  ; implicit memory location created
-  [(_ e e_rest) ≫
-   [⊢ e ≫ e- ⇒ σ]
-   [⊢ e_rest ≫ e_rest- ⇐ (MList σ)]
-   --------
-   [⊢ (#%app- mcons- e- e_rest-) ⇒ (MList σ)]]
-
-  ; with memory location given
-  [(_ e e_rest @ e_loc) ≫
-   [⊢ e ≫ e- ⇒ σ]
-   [⊢ e_rest ≫ e_rest- ⇐ (MList σ)]
-   [⊢ e_loc ≫ e_loc- ⇐ MList0]
-   #:with tmp (generate-temporary #'e_loc)
-   --------
-   [⊢ (let- ([tmp e_loc-])
-            (set-mcar!- tmp e-)
-            (set-mcdr!- tmp e_rest-)
-            tmp)
-      ⇒ (MList σ)]])
-
-
-(define-typed-syntax nil
-  [(_ {ty:type}) ≫
-   --------
-   [⊢ '() ⇒ (MList ty.norm)]]
-  [(_) ⇐ (~MList σ) ≫
-   --------
-   [⊢ '()]])
-
-
-(define-typed-syntax match-list
-  #:datum-literals (cons nil @)
-  [(_ e_list
-      (~or [(cons x+:id xs+:id @ l+:id) e_cons+]
-           [(nil) e_nil+]) ...) ≫
-   #:with [(l x xs e_cons)] #'[(l+ x+ xs+ e_cons+) ...]
-   #:with [e_nil] #'[e_nil+ ...]
-
-   ; list
-   [⊢ e_list ≫ e_list- ⇒ (~MList σ)]
-   #:with σ_xs ((current-type-eval) #'(MList σ))
-   #:with σ_l ((current-type-eval) #'MList0)
-
-   #:mode (make-linear-branch-mode 2)
-     (; cons branch
-      #:submode (branch-nth 0)
-        ([[x ≫ x- : σ]
-          [xs ≫ xs- : σ_xs]
-          [l ≫ l- : σ_l]
-          ⊢ e_cons ≫ e_cons- ⇒ σ_out]
-         #:do [(linear-out-of-scope! #'([x- : σ] [xs- : σ_xs] [l- : σ_l]))])
-
-      ; nil branch
-      #:submode (branch-nth 1)
-        ([⊢ [e_nil ≫ e_nil- ⇐ σ_out]]))
-
-   --------
-   [⊢ (let- ([l- e_list-])
-            (if- (null? l-)
-                 e_nil-
-                 (let- ([x- (mcar- l-)]
-                        [xs- (mcdr- l-)])
-                       e_cons-)))
-      ⇒ σ_out]])

turnstile/examples/linear/lin+tup.rkt

@@ -1,112 +0,0 @@
-#lang turnstile/lang
-(extends "lin.rkt")
-
-(provide (type-out ⊗) tup let*)
-(begin-for-syntax (provide in-cad*rs
-                           list-destructure-syntax))
-
-(define-type-constructor ⊗ #:arity >= 2)
-
-(begin-for-syntax
-  (define (num-tuple-fail-msg σs xs)
-    (format "wrong number of tuple elements: expected ~a, got ~a"
-            (stx-length xs)
-            (stx-length σs)))
-
-  (current-linear-type? (or/c ⊗? (current-linear-type?))))
-
-
-(define-typed-syntax tup
-  [(_ e1 e2 ...+) ≫
-   [⊢ e1 ≫ e1- ⇒ σ1]
-   [⊢ e2 ≫ e2- ⇒ σ2] ...
-   --------
-   [⊢ (list- e1- e2- ...) ⇒ (⊗ σ1 σ2 ...)]])
-
-
-(define-typed-syntax let*
-  ; normal let* recursive bindings
-  [(_ ([x:id e_rhs] . xs) . body) ≫
-   [⊢ e_rhs ≫ e_rhs- ⇒ σ]
-   [[x ≫ x- : σ] ⊢ (let* xs . body) ≫ e_body- ⇒ σ_out]
-   #:do [(linear-out-of-scope! #'([x- : σ]))]
-   --------
-   [⊢ (let- ([x- e_rhs-]) e_body-) ⇒ σ_out]]
-
-  ; tuple unpacking with (let* ([(x ...) tup]) ...)
-  [(_ ([(x:id ...) e_rhs] . xs) . body) ≫
-   [⊢ e_rhs ≫ e_rhs- ⇒ (~⊗ σ ...)]
-   #:fail-unless (stx-length=? #'[σ ...] #'[x ...])
-                 (num-tuple-fail-msg #'[σ ...] #'[x ...])
-
-   [[x ≫ x- : σ] ... ⊢ (let* xs . body) ≫ e_body- ⇒ σ_out]
-   #:do [(linear-out-of-scope! #'([x- : σ] ...))]
-
-   #:with tmp (generate-temporary #'e_tup)
-   #:with destr (list-destructure-syntax #'[x- ...] #'tmp #:unsafe? #t
-                                         #'e_body-)
-   --------
-   [⊢ (let- ([tmp e_rhs-]) destr) ⇒ σ_out]]
-
-  [(_ () e) ≫
-   --------
-   [≻ e]]
-
-  [(_ () e ...+) ≫
-   --------
-   [≻ (lin:begin e ...)]])
-
-
-
-(require racket/unsafe/ops)
-
-;; generate infinite sequence of cad*r syntax, e.g.
-;;   (car e) (cadr e) (caddr e) ...
-(define-for-syntax (in-cad*rs e #:unsafe? [unsafe? #f])
-  (make-do-sequence
-   (λ ()
-     (values (λ (s)
-               (if unsafe?
-                   (quasisyntax/loc e (unsafe-car #,s))
-                   (quasisyntax/loc e (car #,s))))
-             (λ (s)
-               (if unsafe?
-                   (quasisyntax/loc e (unsafe-cdr #,s))
-                   (quasisyntax/loc e (cdr #,s))))
-             e
-             #f #f #f))))
-
-
-;; (list-destructure-syntax #'(x y z ...) #'rhs #'body)
-;;   =
-;; (let ([x (car rhs)]
-;;       [y (cadr rhs)]
-;;       [z (caddr rhs)]
-;;       ...)
-;;   body)
-(define-for-syntax (list-destructure-syntax xs rhs body #:unsafe? [unsafe? #f])
-  (with-syntax ([binds (for/list ([c (in-cad*rs rhs #:unsafe? unsafe?)]
-                                  [x (in-syntax xs)])
-                         (list x c))]
-                [body body])
-    (syntax/loc rhs
-      (let- binds body))))
-
-
-
-(module+ test
-  (begin-for-syntax
-    (require  rackunit)
-    (check-equal? (for/list ([c (in-cad*rs #'x)]
-                             [i (in-range 4)])
-                    (syntax->datum c))
-                  '[(car x)
-                    (car (cdr x))
-                    (car (cdr (cdr x)))
-                    (car (cdr (cdr (cdr x))))])
-
-    (check-equal? (syntax->datum
-                   (list-destructure-syntax #'[x y] #'lst #'z #:unsafe? #t))
-                  '(let- ([x (unsafe-car lst)]
-                          [y (unsafe-car (unsafe-cdr lst))])
-                         z))))

turnstile/examples/linear/lin+var.rkt

@@ -1,118 +0,0 @@
-#lang turnstile/lang
-(extends "lin.rkt")
-(require (only-in "lin+tup.rkt" list-destructure-syntax))
-
-(provide ⊕ var match)
-
-(define-internal-type-constructor ⊕/i)
-
-(define-syntax ⊕
-  (syntax-parser
-    [(_ (V:id t ...) ...)
-     (add-orig (mk-type #'(⊕/i- (#%app 'V t ...) ...))
-               this-syntax)]))
-
-(begin-for-syntax
-  (provide ⊕? ~⊕)
-  (define ⊕? ⊕/i?)
-
-  (define (fail/no-variant type V [src V])
-    (raise-syntax-error #f
-       (format "expected type ~a does not have variant named '~a'\n"
-               (type->str type)
-               (stx->datum V))
-       src))
-
-  (define (num-var-args-fail-msg σs xs)
-    (format "wrong number of arguments to variant: expected ~a, got ~a"
-            (stx-length σs)
-            (stx-length xs)))
-
-
-  (define (unvariant type)
-    (syntax-parse type
-      [(~⊕/i ((~literal #%plain-app) ((~literal quote) U) τ ...) ...)
-       #'[(U τ ...) ...]]))
-
-  (define-syntax ~⊕
-    (pattern-expander
-     (λ (stx)
-       (syntax-case stx ()
-         [(_ . pat)
-          (with-syntax ([(x) (generate-temporaries #'(x))])
-            #'(~and x (~⊕/i . _) (~parse pat (unvariant #'x))))]))))
-
-  (define (has-variant? type v)
-    (syntax-parse type
-      [(~⊕ [U . _] ...)
-       (for/or ([u (in-syntax #'[U ...])])
-         (eq? (stx->datum u) (stx->datum v)))]
-      [_ #f]))
-
-  (define (get-variant type v)
-    (syntax-parse type
-      [(~⊕ [U τ ...] ...)
-       (for/first ([u (in-syntax #'[U ...])]
-                   [ts (in-syntax #'[(τ ...) ...])]
-                   #:when (eq? (stx->datum u) (stx->datum v)))
-         ts)]))
-
-  (current-linear-type? (or/c ⊕? (current-linear-type?)))
-  )
-
-
-(define-typed-syntax var
-  [(_ [V:id e ...]) ⇐ σ_var ≫
-   #:when (⊕? #'σ_var)
-   #:fail-unless (has-variant? #'σ_var #'V)
-                 (fail/no-variant #'σ_var #'V this-syntax)
-   #:with [σ ...] (get-variant #'σ_var #'V)
-   #:fail-unless (stx-length=? #'[σ ...] #'[e ...])
-                 (num-var-args-fail-msg #'[σ ...] #'[e ...])
-   [⊢ e ≫ e- ⇐ σ] ...
-   --------
-   [⊢ (list 'V e- ...)]]
-
-  [(_ [V:id e ...] (~datum as) t) ≫
-   --------
-   [≻ (lin:ann (var [V e ...]) : t)]])
-
-
-
-(define-typed-syntax match
-  [(_ e_var [(V:id x:id ...) e_bra] ...) ≫
-   [⊢ e_var ≫ e_var- ⇒ σ_var]
-   #:fail-unless (⊕? #'σ_var)
-   (format "expected type ⊕, given ~a" (type->str #'σ_var))
-
-   #:mode (make-linear-branch-mode (stx-length #'[e_bra ...]))
-     (#:with ([(x- ...) e_bra- σ_bra] ...)
-      (for/list ([q (in-syntax #'([V (x ...) e_bra] ...))]
-                 [i (in-naturals)])
-        (syntax-parse/typecheck q
-         [(V (x ...) e) ≫
-          #:fail-unless (has-variant? #'σ_var #'V)
-                        (fail/no-variant #'σ_var #'V)
-
-          #:with [σ ...] (get-variant #'σ_var #'V)
-          #:fail-unless (stx-length=? #'[σ ...] #'[x ...])
-                        (num-var-args-fail-msg #'[σ ...] #'[x ...])
-
-          #:submode (branch-nth i)
-            ([[x ≫ x- : σ] ... ⊢ e ≫ e- ⇒ σ_bra]
-             #:do [(linear-out-of-scope! #'([x- : σ] ...))])
-          --------
-          [≻ [(x- ...) e- σ_bra]]])))
-
-   #:with tmp (generate-temporary)
-   #:with (destr ...) (stx-map (λ (l) (apply list-destructure-syntax (stx->list l)))
-                               #'[([x- ...]
-                                   (cdr tmp)
-                                   e_bra-) ...])
-   --------
-   [⊢ (let ([tmp e_var-])
-        (case (car tmp)
-          [(V) destr] ...
-          [else (printf "~a\n" tmp)
-                (error '"unhandled case: " (car tmp))]))
-      ⇒ (⊔ σ_bra ...)]])

turnstile/examples/linear/lin.rkt

@@ -1,350 +0,0 @@
-#lang turnstile
-(extends "../ext-stlc.rkt" #:except define if begin let let* letrec λ #%app)
-
-(provide (for-syntax current-linear-type?
-                     linear-type?
-                     unrestricted-type?
-
-                     linear-mode?
-                     linear-scope
-                     linear-in-scope?
-                     linear-use-var!
-                     linear-out-of-scope!
-                     linear-merge-scopes!
-                     linear-merge-scopes*!
-
-                     ;; TODO: should these be in turnstile/mode ?
-                     branch-nth
-                     branch-then
-                     branch-else
-
-                     make-empty-linear-mode
-                     make-fresh-linear-mode
-                     make-linear-branch-mode)
-
-         %%reset-linear-mode
-
-         (type-out Unit Int String Bool -o)
-         #%top-interaction #%module-begin require only-in
-         begin drop
-         #%app #%lin-var
-         λ (rename-out [λ lambda])
-         let letrec
-         if
-         define
-         )
-
-
-(define-type-constructor -o #:arity >= 1)
-
-
-(begin-for-syntax
-  (require syntax/id-set
-           racket/set
-           racket/generic
-           turnstile/mode)
-
-  (define (fail/multiple-use x)
-    (raise-syntax-error #f "linear variable used more than once" x))
-  (define (fail/unused x)
-    (raise-syntax-error #f "linear variable unused" x))
-  (define (fail/unbalanced-branches x)
-    (raise-syntax-error #f "linear variable may be unused in certain branches" x))
-  (define (fail/unrestricted-fn x)
-    (raise-syntax-error #f "linear variable may not be used by unrestricted function" x))
-
-
-  ;; this parameter defines the linear-type? function.
-  ;; we defining new types that are linear, modify this
-  ;; parameter like so:
-  ;;   (current-linear-type? (or/c MYTYPE? (current-linear-type?)))
-  ;;
-  ;; current-linear-type? : (Parameter (Type -> Bool))
-  (define current-linear-type?
-    (make-parameter -o?))
-
-  ;; is the given type [linear|unrestricted]?
-  ;; Type -> Bool
-  (define (linear-type? T)
-    ((current-linear-type?) T))
-  (define (unrestricted-type? T)
-    (not ((current-linear-type?) T)))
-
-
-
-  ;; mode object to be used during linear typing.
-  ;; the field 'scope' contains a free-id-set of
-  ;; variables that have been used, and therefore
-  ;; can't be used again.
-  (struct linear-mode mode (scope))
-
-  ;; get the current scope (as described above)
-  ;; based on (current-mode)
-  (define (linear-scope)
-    (linear-mode-scope (current-mode)))
-
-  ;; is the given variable available for use?
-  ;; linear-in-scope? : Id -> Bool
-  (define (linear-in-scope? x)
-    (not (set-member? (linear-scope) x)))
-
-  ;; set the variable to be used in this scope, or raise
-  ;; an error if it's already used.
-  ;;
-  ;; linear-use-var! : Id Type -> void
-  (define (linear-use-var! x T #:fail [fail fail/multiple-use])
-    (when (linear-type? T)
-      (when (set-member? (linear-scope) x)
-        (fail x))
-      (set-add! (linear-scope) x)))
-
-
-  ;; call this with the ([x : t] ...) context after introducing variables,
-  ;; to remove those variables from the linear scope
-  ;;
-  ;; linear-out-of-scope! : Ctx -> Void
-  (define (linear-out-of-scope! ctx #:fail [fail fail/unused])
-    (syntax-parse ctx
-      #:datum-literals (:)
-      [([x : σ] ...)
-       (for ([var (in-syntax #'[x ...])]
-             [T (in-syntax #'[σ ...])] #:when (linear-type? T))
-         (if (linear-in-scope? var)
-             (fail var)
-             (set-remove! (linear-scope) var)))]))
-
-  ;; linear-merge-scopes! : (or '∪ '∩) FreeIdSet ... -> void
-  (define (linear-merge-scopes! op #:fail [fail fail/unbalanced-branches] . ss)
-    (linear-merge-scopes*! op ss #:fail fail))
-
-  ;; linear-merge-scopes*! : (or '∪ '∩) (Listof FreeIdSet) -> void
-  (define (linear-merge-scopes*! op ss #:fail [fail fail/unbalanced-branches])
-    (define s0
-      (case op
-        [(∩)
-         (let ([s0 (set-copy (car ss))])
-           (for ([s (in-list (cdr ss))])
-             (set-intersect! s0 s))
-           (for* ([s (in-list ss)]
-                  [x (in-set s)] #:when (not (set-member? s0 x)))
-             (fail x))
-           s0)]
-
-        [(∪) (apply set-union ss)]))
-
-    (set-clear! (linear-scope))
-    (set-union! (linear-scope) s0))
-
-
-
-  ;; a mode that contains submodes, for use
-  ;; in branching (if, cond, etc.)
-  (struct branch-mode mode (sub-modes))
-
-  ;; for use as `#:submode (branch-nth n)`
-  (define ((branch-nth n) bm)
-    (list-ref (branch-mode-sub-modes bm) n))
-  (define branch-then (branch-nth 0))
-  (define branch-else (branch-nth 1))
-
-  ;; creates a branch-mode with n branches (default: 2)
-  ;; which merges the linear sub-scopes during teardown.
-  ;; see 'if' syntax.
-  ;;
-  ;; make-linear-branch : Int -> BranchMode
-  (define (make-linear-branch-mode [n 2])
-    (define scopes
-      (for/list ([i (in-range n)])
-        (set-copy (linear-scope))))
-
-    (branch-mode void
-                 (λ () (linear-merge-scopes*! '∩ scopes))
-                 (for/list ([s (in-list scopes)])
-                   (linear-mode void void s))))
-
-
-  ;; creates a linear mode that disallows (on teardown) use
-  ;; of variables from outside of the current scope.
-  ;; see unrestricted λ syntax.
-  ;;
-  ;; make-fresh-linear-context : -> linear-mode?
-  (define (make-fresh-linear-mode #:fail [fail fail/unrestricted-fn])
-    (let ([ls #f])
-      (linear-mode (λ () (set! ls (set-copy (linear-scope))))
-                   (λ () (linear-merge-scopes! '∩ (linear-scope) ls #:fail fail))
-                   (linear-scope))))
-
-
-  ;; creates an empty linear mode.
-  ;;
-  ;; make-empty-linear-mode : -> LinearMode
-  (define (make-empty-linear-mode)
-    (linear-mode void void (mutable-free-id-set)))
-
-  (current-mode (make-empty-linear-mode))
-
-  )
-
-;; this function resets the mode to be an empty
-;; linear-mode. this should ONLY be used by tests
-;; that screw up the state of current-mode, and
-;; need to reset it for the next test. this is because
-;; we don't have proper backtracking facilities, so
-;; errors in the middle of inference screw up the
-;; global state
-(define-syntax %%reset-linear-mode
-  (syntax-parser
-    [(_)
-     #:do [(current-mode (make-empty-linear-mode))]
-     #'(#%app- void-)]))
-
-
-
-(define-typed-syntax begin
-  [(begin e ... e0) ≫
-   [⊢ [e ≫ e- ⇐ Unit] ... [e0 ≫ e0- ⇒ σ]]
-   --------
-   [⊢ (begin- e- ... e0-) ⇒ σ]]
-
-  [(begin e ... e0) ⇐ σ ≫
-   [⊢ [e ≫ e- ⇐ Unit] ... [e0 ≫ e0- ⇐ σ]]
-   --------
-   [⊢ (begin- e- ... e0-)]])
-
-
-
-(define-typed-syntax drop
-  [(drop e) ≫
-   [⊢ e ≫ e- ⇒ _]
-   --------
-   [⊢ (#%app- void- e-) ⇒ Unit]])
-
-
-
-(define-typed-syntax #%app
-  [(_) ≫
-   --------
-   [⊢ (#%app- void-) ⇒ Unit]]
-
-  [(#%app fun arg ...) ≫
-   [⊢ fun ≫ fun- ⇒ σ_fun]
-   #:with (~or (~-o σ_in ... σ_out)
-               (~→ σ_in ... σ_out)
-               (~post (~fail "expected linear function type")))
-          #'σ_fun
-   [⊢ [arg ≫ arg- ⇐ σ_in] ...]
-   --------
-   [⊢ (#%app- fun- arg- ...) ⇒ σ_out]])
-
-
-
-(define-typed-variable-syntax
-  #:name #%lin-var
-  [(#%var x- : σ) ≫
-   #:do [(linear-use-var! #'x- #'σ)]
-   ----------
-   [⊢ x- ⇒ σ]])
-
-
-(define-typed-syntax λ
-  #:datum-literals (: !)
-  ;; linear lambda; annotations
-  [(λ ([x:id : T:type] ...) b) ≫
-   #:with [σ ...] #'[T.norm ...]
-   [[x ≫ x- : σ] ... ⊢ b ≫ b- ⇒ σ_out]
-   #:do [(linear-out-of-scope! #'([x- : σ] ...))]
-   --------
-   [⊢ (λ- (x- ...) b-) ⇒ (-o σ ... σ_out)]]
-
-  ;; unrestricted lambda; annotations
-  [(λ ! ([x:id : T:type] ...) b) ≫
-   #:with [σ ...] #'[T.norm ...]
-   #:mode (make-fresh-linear-mode)
-     ([[x ≫ x- : σ] ... ⊢ b ≫ b- ⇒ σ_out]
-      #:do [(linear-out-of-scope! #'([x- : σ] ...))])
-   --------
-   [⊢ (λ- (x- ...) b-) ⇒ (→ σ ... σ_out)]]
-
-  ;; linear lambda; inferred
-  [(λ (x:id ...) b) ⇐ (~-o σ ... σ_out) ≫
-   #:fail-unless (stx-length=? #'[x ...] #'[σ ...])
-                 (num-args-fail-msg this-syntax #'[x ...] #'[σ ...])
-   [[x ≫ x- : σ] ... ⊢ b ≫ b- ⇐ σ_out]
-   #:do [(linear-out-of-scope! #'([x- : σ] ...))]
-   --------
-   [⊢ (λ- (x- ...) b-)]]
-
-  ;; unrestricted lambda; inferred
-  [(λ (x:id ...) b) ⇐ (~→ σ ... σ_out) ≫
-   #:fail-unless (stx-length=? #'[x ...] #'[σ ...])
-                 (num-args-fail-msg this-syntax #'[x ...] #'[σ ...])
-   #:mode (make-fresh-linear-mode)
-     ([[x ≫ x- : σ] ... ⊢ b ≫ b- ⇐ σ_out]
-      #:do [(linear-out-of-scope! #'([x- : σ] ...))])
-   --------
-   [⊢ (λ- (x- ...) b-)]])
-
-
-
-(define-typed-syntax let
-  [(let ([x e] ...) b) ≫
-   [⊢ [e ≫ e- ⇒ σ] ...]
-   [[x ≫ x- : σ] ... ⊢ b ≫ b- ⇒ σ_out]
-   #:do [(linear-out-of-scope! #'([x- : σ] ...))]
-   --------
-   [⊢ (let- ([x- e-] ...) b-) ⇒ σ_out]])
-
-
-
-(define-typed-syntax letrec
-  [(letrec ([b:type-bind rhs] ...) e ...) ≫
-   #:fail-when (ormap linear-type? (stx->list #'[b.type ...]))
-               (format "may not bind linear type ~a in letrec"
-                       (type->str (findf linear-type? (stx->list #'[b.type ...]))))
-   [[b.x ≫ x- : b.type] ...
-    ⊢ [rhs ≫ rhs- ⇐ b.type] ...
-       [(begin e ...) ≫ e- ⇒ σ_out]]
-   #:do [(linear-out-of-scope! #'([x- : b.type] ...))]
-   --------
-   [⊢ (letrec- ([x- rhs-] ...) e-) ⇒ σ_out]])
-
-
-
-(define-typed-syntax if
-  [(_ c e1 e2) ⇐ σ ≫
-   [⊢ c ≫ c- ⇐ Bool]
-   #:mode (make-linear-branch-mode 2)
-     ([⊢ [e1 ≫ e1- ⇐ σ] #:submode branch-then]
-      [⊢ [e2 ≫ e2- ⇐ σ] #:submode branch-else])
-   --------
-   [⊢ (if- c- e1- e2-)]]
-
-  [(_ c e1 e2) ≫
-   [⊢ c ≫ c- ⇐ Bool]
-   #:mode (make-linear-branch-mode 2)
-     ([⊢ [e1 ≫ e1- ⇒ σ1] #:submode branch-then]
-      [⊢ [e2 ≫ e2- ⇒ σ2] #:submode branch-else])
-   --------
-   [⊢ (if- c- e1- e2-) ⇒ (⊔ σ1 σ2)]])
-
-
-
-(define-typed-syntax define
-  #:datum-literals (:)
-  [(define (f [x:id : ty] ...) ret
-     e ...+) ≫
-   --------
-   [≻ (define f : (→ ty ... ret)
-        (letrec ([{f : (→ ty ... ret)}
-                  (λ ! ([x : ty] ...)
-                    (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)))]])

turnstile/examples/tests/linear-var-assign-tests.rkt

@@ -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")

turnstile/examples/tests/linear/fabul-tests.rkt

@@ -1,75 +0,0 @@
-#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})))))))

turnstile/examples/tests/linear/lin+chan-tests.rkt

@@ -1,18 +0,0 @@
-#lang s-exp turnstile/examples/linear/lin+chan
-(require turnstile/rackunit-typechecking)
-
-(check-type
- (let* ([(c c-out) (make-channel {Int})])
-   (thread (λ () (channel-put c-out 5)))
-   (thread (λ () (channel-put c-out 4)))
-   (let* ([(c1 x) (channel-get c)]
-          [(c2 y) (channel-get c1)])
-     (drop c2)
-     (+ x y)))
- : Int -> 9)
-
-(typecheck-fail
- (let* ([(c-in c-out) (make-channel {String})])
-   (thread (λ () (channel-get c-in)))
-   (channel-get c-in))
- #:with-msg "c-in: linear variable used more than once")

turnstile/examples/tests/linear/lin+cons-tests.rkt

@@ -1,28 +0,0 @@
-#lang s-exp turnstile/examples/linear/lin+cons
-(require turnstile/rackunit-typechecking)
-
-
-(define (length [lst : (MList Int)]) Int
-  (match-list lst
-    [(cons _ xs @ l)
-     (begin (drop l)
-            (add1 (length xs)))]
-    [(nil) 0]))
-
-(check-type (length (cons 9 (cons 8 (cons 7 (nil))))) : Int -> 3)
-
-
-
-(define (rev-append [lst : (MList String)]
-                    [acc : (MList String)]) (MList String)
-  (match-list lst
-    [(cons x xs @ l) (rev-append xs (cons x acc @ l))]
-    [(nil) acc]))
-
-(define (rev [lst : (MList String)]) (MList String)
-  (rev-append lst (nil)))
-
-
-(check-type (rev (cons "a" (cons "b" (cons "c" (nil)))))
-            : (MList String)
-            -> (cons "c" (cons "b" (cons "a" (nil)))))

turnstile/examples/tests/linear/lin+tup-tests.rkt

@@ -1,29 +0,0 @@
-#lang s-exp turnstile/examples/linear/lin+tup
-
-(require turnstile/rackunit-typechecking
-         (only-in racket/base quote))
-
-(check-type (tup 1 #t) : (⊗ Int Bool) -> '(1 #t))
-(check-type (tup 1 2 3) : (⊗ Int Int Int) -> '(1 2 3))
-
-(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 (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")
-
-(check-type (λ ([x : Int]) (tup x x)) : (-o 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 (let* ([x 3] [y x]) y) : Int -> 3)
-(check-type (let* ([(x y) (tup 1 #f)]) x) : Int -> 1)
-(typecheck-fail (let* ([(x y) (tup (tup 1 2) 3)]) y)
-                #:with-msg "x: linear variable unused")

turnstile/examples/tests/linear/lin+var-tests.rkt

@@ -1,67 +0,0 @@
-#lang s-exp turnstile/examples/linear/lin+var
-(require turnstile/rackunit-typechecking)
-
-(check-type (var [left 3]) : (⊕ [left Int] [right String]))
-(check-type (var [right "a"]) : (⊕ [left Int] [right String]))
-
-(typecheck-fail (var [left 3] as (⊕ [yes] [no]))
-                #:with-msg "type \\(⊕ \\(yes\\) \\(no\\)\\) does not have variant named 'left'")
-
-(typecheck-fail (var [left 3] as (⊕ [left Int Int] [right String]))
-                #:with-msg "wrong number of arguments to variant: expected 2, got 1")
-
-(define-type-alias (Either A B) (⊕ [left A] [right B]))
-(define-type-alias (Option A) (⊕ [some A] [none]))
-
-(typecheck-fail (var [middle 3] as (Either Int Float))
-                #:with-msg "type \\(Either Int Float\\) does not have variant named 'middle'")
-
-(check-type (λ (x) x) : (→ (Either Int Float) (Either Int Float)))
-(check-type (λ (x) x) : (→ (Either Int Float) (⊕ [left Int] [right Float])))
-
-(typecheck-fail (let ([x (var [left 3] as (Either Int Int))]) 0)
-                #:with-msg "x: linear variable unused")
-
-(check-type (match (var [left 3] as (Either Int Int))
-              [(left x) x]
-              [(right y) (+ y 1)])
-            : Int ⇒ 3)
-
-(check-type (match (var [right 5] as (Either Int Int))
-              [(left x) x]
-              [(right y) (+ y 1)])
-            : Int ⇒ 6)
-
-(typecheck-fail (match (var [left 3] as (Either Int (-o Int Int)))
-                  [(left x) x]
-                  [(right f) 0])
-                #:with-msg "f: linear variable unused")
-
-(check-type (match (var [right (λ (x) (+ x x))] as (Either Int (-o Int Int)))
-              [(left x) x]
-              [(right f) (f 2)])
-            : Int ⇒ 4)
-
-(typecheck-fail (match (var [left 0] as (Either Int String))
-                  [(left x) x]
-                  [(right y) y])
-                #:with-msg "branches have incompatible types: Int and String")
-
-(typecheck-fail (match (var [some ()] as (Option Unit))
-                  [(left x) x]
-                  [(right y) y])
-                #:with-msg "type \\(Option Unit\\) does not have variant named 'left'")
-(%%reset-linear-mode)
-
-(typecheck-fail (match (var [left 0] as (Either Int Int))
-                  [(left x) x]
-                  [(right y z) y])
-                #:with-msg "wrong number of arguments to variant: expected 1, got 2")
-(%%reset-linear-mode)
-
-(typecheck-fail (let ([f (λ ([x : Int]) x)])
-                  (match (var [left 0] as (Either Int Int))
-                    [(left x) (f x)]
-                    [(right y) y]))
-                #:with-msg "f: linear variable may be unused in certain branches")
-(%%reset-linear-mode)

turnstile/examples/tests/linear/lin-tests.rkt

@@ -1,76 +0,0 @@
-#lang s-exp turnstile/examples/linear/lin
-(require turnstile/rackunit-typechecking
-         (only-in racket/base quote))
-
-(check-type #t : Bool)
-(check-type 4 : Int)
-(check-type () : Unit)
-
-(check-type (let ([x 3] [y 4]) y) : Int -> 4)
-
-(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 "branches have incompatible types: Int and Unit")
-(%%reset-linear-mode)
-
-(check-type (λ ([x : Int]) x) : (-o Int Int))
-(check-type (λ ! ([x : Int]) x) : (→ Int Int))
-(check-type (λ (x) x) : (-o String String))
-(check-type (λ (x) x) : (→ String String))
-
-(check-type + : (→ Int Int Int))
-(check-type (+ 1 2) : Int -> 3)
-(check-type ((λ ([x : Int]) (+ x 1)) 4) : Int -> 5)
-
-
-(typecheck-fail (λ ([p : (-o Int Bool)]) 0)
-                #:with-msg "p: linear variable unused")
-
-(typecheck-fail (let ([f (λ ([x : Int]) x)])
-                  0)
-                #:with-msg "f: linear variable unused")
-
-(typecheck-fail (let ([f (λ ([x : Int]) x)])
-                  (f (f 3)))
-                #:with-msg "f: linear variable used more than once")
-
-(typecheck-fail (let ([f (λ ([x : Int]) x)])
-                  (if #t
-                      (f 3)
-                      4))
-                #:with-msg "f: linear variable may be unused in certain branches")
-
-(typecheck-fail (let ([f (λ ([x : Int]) x)])
-                  (λ ! ([x : Int]) f))
-                #:with-msg "f: linear variable may not be used by unrestricted function")
-(%%reset-linear-mode)
-
-(check-type (let ([twice (λ ! ([x : Int]) (+ x x))])
-              (+ (twice 8)
-                 (twice 9)))
-            : Int -> 34)
-
-(check-type (let ([f (λ ([x : Int]) #t)])
-              (begin (drop f)
-                     3))
-            : Int -> 3)
-
-(check-type (letrec ([{<= : (→ Int Int Bool)}
-                      (λ (n m)
-                         (if (zero? n)
-                             #t
-                             (if (zero? m)
-                                 #f
-                                 (<= (sub1 n) (sub1 m)))))])
-              (if (<= 4 1) 999
-                  (if (<= 3 3)
-                      0
-                      888)))
-            : Int -> 0)
-
-(typecheck-fail (letrec ([{f : (-o Int Int)}
-                          (λ (x) (f x))])
-                  (f 3))
-                #:with-msg "may not bind linear type \\(-o Int Int\\) in letrec")

turnstile/mode.rkt

@@ -1,70 +0,0 @@
-#lang racket/base
-(provide (struct-out mode)
-         make-mode
-         current-mode
-         with-mode
-         make-param-mode)
-
-
-;; mode object. contains setup routine and teardown routine
-;; as fields.
-(struct mode (setup-fn teardown-fn))
-
-(define (make-mode #:setup [setup-fn void]
-                   #:teardown [teardown-fn void])
-  (mode setup-fn teardown-fn))
-
-
-;; apply the given mode for the successive expressions.
-;; e.g.
-;; (with-mode (mode (λ () (display "before "))
-;;                        (λ () (display "after\n")))
-;;   (display "middle "))
-;; ->
-;;   before middle after
-;;
-;; (with-mode <mode> <body> ...)
-(define-syntax-rule (with-mode mode-expr body ...)
-  (let* ([the-mode mode-expr])
-    ((mode-setup-fn the-mode))
-    (begin0 (parameterize ([current-mode the-mode]) body ...)
-      ((mode-teardown-fn the-mode)))))
-
-
-;; the current set mode. useful for #:submode/mode
-(define current-mode
-  (make-parameter (mode void void)))
-
-
-;; returns a mode that sets the given
-;; parameter to the given value, for its duration.
-;; similar to (parameterize ([P value]) ...)
-;;
-;; make-param-mode : ∀T. (parameterof T) T -> mode?
-(define (make-param-mode P value)
-  (let* ([swap! (λ ()
-                  (let ([cur (P)])
-                    (P value)
-                    (set! value cur)))])
-    (mode swap! swap!)))
-
-
-
-(module+ test
-  (require rackunit)
-
-  (define color (make-parameter 'red))
-
-  (define ->blue (make-param-mode color 'blue))
-  (define ->green (make-param-mode color 'green))
-
-  (with-mode ->blue
-    (check-equal? (color) 'blue))
-  (check-equal? (color) 'red)
-
-  (with-mode ->green
-    (check-equal? (color) 'green)
-    (with-mode ->blue
-      (check-equal? (color) 'blue))
-    (check-equal? (color) 'green))
-  )

turnstile/scribblings/reference.scrbl

@@ -2,7 +2,6 @@
 
 @(require scribble/example racket/sandbox
           (for-label racket/base
-                     turnstile/mode
                      (except-in turnstile/turnstile ⊢ stx mk-~ mk-?))
           "doc-utils.rkt" "common.rkt")
 
@@ -60,17 +59,15 @@ and then press Control-@litchar{\}.
    [expr-template (code:line @#,racket[quasisyntax] @#,tech:template)]
    [type-template (code:line @#,racket[quasisyntax] @#,tech:template)]
    [key identifier?]
-   [premise (code:line [⊢ tc ... prem-options] ooo ...)
-            (code:line [ctx-elem ... ⊢ tc ... prem-options] ooo ...)
-            (code:line [ctx ⊢ tc ... prem-options] ooo ...)
-            (code:line [ctx ctx ⊢ tc ... prem-options] ooo ...)
+   [premise (code:line [⊢ tc ...] ooo ...)
+            (code:line [ctx ⊢ tc ...] ooo ...)
+            (code:line [ctx-elem ... ⊢ tc ...] ooo ...)
+            (code:line [ctx ctx ⊢ tc ...] ooo ...)
             (code:line [⊢ . tc-elem] ooo ...)
-            (code:line [ctx-elem ... ⊢ . tc-elem] ooo ...)
             (code:line [ctx ⊢ . tc-elem] ooo ...)
+            (code:line [ctx-elem ... ⊢ . tc-elem] ooo ...)
             (code:line [ctx ctx ⊢ . tc-elem] ooo ...)
             type-relation
-            (code:line #:mode mode-expr (premise ...))
-            (code:line #:submode fn-expr (premise ...))
             (code:line @#,racket[syntax-parse] @#,tech:pat-directive)]
    [ctx (ctx-elem ...)]
    [ctx-elem (code:line [id ≫ id key template ... ...] ooo ...)
@@ -86,9 +83,6 @@ and then press Control-@litchar{\}.
                   (code:line [type-template τ= type-template #:for expr-template] ooo ...)
                   (code:line [type-template τ⊑ type-template] ooo ...)
                   (code:line [type-template τ⊑ type-template #:for expr-template] ooo ...)]
-   [prem-options (code:line)
-                 (code:line #:mode mode-expr)
-                 (code:line #:submode fn-expr)]
    [conclusion [⊢ expr-template ⇒ type-template]
                [⊢ expr-template ⇒ key template]
                [⊢ expr-template (⇒ key template) ooo ...]
@@ -148,26 +142,6 @@ pattern @racket[x ... y ...] will not work as expected.
 For convenience, lone identifiers written to the left of the turnstile are
 automatically treated as type variables.
 
-@italic{Modes}
-
-The keyword @racket[#:mode], when appearing at end of a typechecking rule,
-sets the parameter @racket[current-mode] to the @racket[mode] object supplied
-by @racket[_mode-expr], for the extent of that rule. @racket[#:mode], when
-appearing as its own premise, sets the @racket[current-mode] parameter for the
-extent of all the grouped sub-premises.
-
-The keyword @racket[#:submode] is similar to @racket[#:mode], but it calls
-@racket[(_fn-expr (current-mode))] to obtain the new mode object. Thus,
-@racket[#:mode (_fn-expr (current-mode))] is identical to @racket[#:submode
-_fn-expr].
-
-See @secref{Modes} for more details.
-
-WARNING: @racket[#:mode] is unaware of the backtracking behavior of
-@racket[syntax-parse]. If pattern backtracking escapes a @racket[#:mode] group, it may
-leave @racket[current-mode] in an undesirable state.
-
-
 @; ----------------------------------------------------------------------------
 @bold{Conclusion}
 
@@ -718,70 +692,7 @@ The possible variances are:
 
 @defproc[(variance? [v any/c]) boolean/c]{
  Predicate that recognizes the variance values.}
-
-
-@section{Modes}
-
-@defmodule[turnstile/mode #:use-sources (turnstile/mode)]
-@(define mode-ev
-   (let ([ev (make-base-eval)])
-     (ev '(require turnstile/mode))
-     ev))
-
-Modes are typically used by the @racket[#:mode] and @racket[#:submode]
-keywords in @racket[define-typed-syntax] (and related forms). When judgements
-are parameterized by a @racket[mode] value, the parameter
-@racket[current-mode] is set to that value for the extend of the
-sub-premises. Additionally, the function @racket[mode-setup-fn] is called
-before setting @racket[current-mode], and the function
-@racket[mode-teardown-fn] is called after @racket[current-mode] is restored to
-its previous value.
-
-@defstruct*[mode ([setup-fn (-> any)] [teardown-fn (-> any)])]{
-  Structure type for modes. Modes can be used to parameterize type judgements
-  or groups of type judgements, to give additional context and to help enable
-  flow-sensitive languages.
-
-  User defined modes should be defined as structs that inherit from @racket[mode].
-}
-
-@defproc[(make-mode [#:setup setup-fn (-> any) void]
-                    [#:teardown teardown-fn (-> any) void]) mode?]{
-  Constructs a new @racket[mode] object with the given setup and teardown functions.
-}
-
-@defparam[current-mode mode mode? #:value (make-mode)]{
-  A parameter that holds the current mode. Typically parameterized using the keywords
-  @racket[#:mode] and @racket[#:submode] from @racket[define-typed-syntax] forms.
-}
-
-@defform[(with-mode mode-expr body ...+)
-         #:contracts ([mode-expr mode?])]{
-  The result of @racket[with-mode] is the result of the last @racket[_body].
-  The parameter @racket[current-mode] is assigned to the result of
-  @racket[_mode-expr] for the extent of the @racket[_body] expressions. The
-  function @racket[mode-setup-fn] is called on the result of
-  @racket[_mode-expr] before @racket[current-mode] is set, and the function
-  @racket[mode-teardown-fn] is called after @racket[current-mode] is restored
-  to its previous value.
-
-  @examples[#:eval mode-ev
-    (define-struct (my-mode mode) ())
-    (define M (make-my-mode (λ () (displayln "M setup"))
-                            (λ () (displayln "M teardown"))))
-    (with-mode M
-      (displayln (current-mode)))]}
-
-@defproc[(make-param-mode [param parameter?] [value any/c]) mode?]{
-  Creates a @racket[mode] that assigns the given parameter to the given
-  value for the extent of the mode.
-
-  @examples[#:eval mode-ev
-    (define current-scope (make-parameter 'outer))
-    (with-mode (make-param-mode current-scope 'inner)
-      (displayln (current-scope)))]}
-
-
+                                      
 @section{Miscellaneous Syntax Object Functions}
 
 These are all phase 1 functions.

turnstile/turnstile.rkt

@@ -1,10 +1,8 @@
 #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-typed-variable-syntax
-         define-syntax-category
+         define-typed-syntax define-syntax-category
          (rename-out [define-typed-syntax define-typerule]
                      [define-typed-syntax define-syntax/typecheck])
          (for-syntax syntax-parse/typecheck
@@ -66,9 +64,8 @@
 (module syntax-classes racket/base
   (provide (all-defined-out))
   (require (for-meta 0 (submod ".." typecheck+))
-           (for-meta -1 (submod ".." typecheck+)
-                     (except-in macrotypes/typecheck #%module-begin mk-~ mk-?)
-                     "mode.rkt")
+           (for-meta -1 (submod ".." typecheck+) 
+                     (except-in macrotypes/typecheck #%module-begin mk-~ mk-?))
            (for-meta -2 (except-in macrotypes/typecheck #%module-begin)))
   (define-syntax-class ---
     [pattern dashes:id
@@ -92,7 +89,7 @@
   (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
@@ -200,14 +197,13 @@
              #`(~post
                 #,(with-depth #'tc.e-pat #'[ooo ...]))])
   (define-syntax-class tc*
-    #:attributes (depth es-stx es-stx-orig es-pat wrap-computation)
+    #: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
-             #:attr wrap-computation (λ (stx) stx)]
-    [pattern (tc:tc ... opts:tc-post-options ...)
+             #: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)
@@ -222,19 +218,7 @@
                 (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* ...]
-             #:attr wrap-computation
-             (λ (stx)
-               (foldr (λ (fun stx) (fun stx))
-                      stx
-                      (attribute opts.wrap)))])
-  (define-splicing-syntax-class tc-post-options
-    #:attributes (wrap)
-    [pattern (~seq #:mode mode-expr)
-             #:attr wrap (λ (stx) #`(with-mode mode-expr #,stx))]
-    [pattern (~seq #:submode fn-expr)
-             #:attr wrap (λ (stx) #`(with-mode (fn-expr (current-mode)) #,stx))]
-    )
+             #:with es-pat #'[es-pat* ...]])
   (define-splicing-syntax-class tc-clause
     #:attributes (pat)
     #:datum-literals (⊢)
@@ -254,12 +238,13 @@
              (with-depth
               #`[(tvctx.ctx ...) (ctx.ctx ...) tc.es-stx tc.es-stx-orig]
               #'[ooo ...])
-             #:with inf #'(infers/depths 'clause-depth
-                                         'tc.depth
-                                         #`tvctxs/ctxs/ess/origs
-                                         #:tag (current-tag))
-             #:with inf+ ((attribute tc.wrap-computation) #'inf)
-             #:with pat #`(~post (~post (~parse tcs-pat inf+)))]
+             #:with pat
+             #`(~post
+                (~post
+                 (~parse
+                  tcs-pat
+                  (infers/depths 'clause-depth 'tc.depth #`tvctxs/ctxs/ess/origs
+                                 #:tag (current-tag)))))]
     )
   (define-splicing-syntax-class clause
     #:attributes (pat)
@@ -320,26 +305,6 @@
     [pattern (~seq #:fail-unless condition:expr message:expr)
              #:with pat
              #'(~post (~fail #:unless condition message))]
-    [pattern (~seq #:mode mode-expr (sub-clause:clause ...))
-             #:with (the-mode tmp) (generate-temporaries #'(the-mode tmp))
-             #:with pat
-             #'(~and (~do (define the-mode mode-expr)
-                          ((mode-setup-fn the-mode))
-                          (define tmp (current-mode))
-                          (current-mode the-mode))
-                     sub-clause.pat ...
-                     (~do (current-mode tmp)
-                          ((mode-teardown-fn the-mode))))]
-    [pattern (~seq #:submode fn-expr (sub-clause:clause ...))
-             #:with (the-mode tmp) (generate-temporaries #'(the-mode tmp))
-             #:with pat
-             #'(~and (~do (define the-mode (fn-expr (current-mode)))
-                          ((mode-setup-fn the-mode))
-                          (define tmp (current-mode))
-                          (current-mode the-mode))
-                     sub-clause.pat ...
-                     (~do (current-mode tmp)
-                          ((mode-teardown-fn the-mode))))]
     )
   (define-syntax-class last-clause
     #:datum-literals (⊢ ≫ ≻ ⇒ ⇐)
@@ -477,16 +442,6 @@
                         [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