From 6d496741c60b9edc6d4f508e2f24a2334bb6ec34 Mon Sep 17 00:00:00 2001
From: Milo Turner <iitalics@gmail.com>
Date: Thu, 24 Aug 2017 14:56:34 -0400
Subject: [PATCH] created fabUL-like langauge using lin + ext-stlc

closes #21
---
 turnstile/examples/linear/fabul-utils.rkt     |  71 ++++++
 turnstile/examples/linear/fabul.rkt           | 241 ++++++++++++++++++
 turnstile/examples/linear/lin.rkt             |   1 +
 .../examples/tests/linear/fabul-tests.rkt     |  75 ++++++
 4 files changed, 388 insertions(+)
 create mode 100644 turnstile/examples/linear/fabul-utils.rkt
 create mode 100644 turnstile/examples/linear/fabul.rkt
 create mode 100644 turnstile/examples/tests/linear/fabul-tests.rkt

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