From 1805b936be22396bffd2db796db1516f81855da3 Mon Sep 17 00:00:00 2001
From: Sam Caldwell <samc@ccs.neu.edu>
Date: Thu, 5 Nov 2020 11:09:00 -0500
Subject: [PATCH] try syntax-local-lift-module-end for lift+define-role

---
 racket/typed/examples/roles/bank-account.rkt | 15 ++++++++-----
 racket/typed/roles.rkt                       | 22 +++++++++++++++++---
 2 files changed, 29 insertions(+), 8 deletions(-)

diff --git a/racket/typed/examples/roles/bank-account.rkt b/racket/typed/examples/roles/bank-account.rkt
index f4dbb20..9d5ddc4 100644
--- a/racket/typed/examples/roles/bank-account.rkt
+++ b/racket/typed/examples/roles/bank-account.rkt
@@ -32,13 +32,11 @@
   (Role (client)
         (Reacts (Asserted Account))))
 
-(check-simulates client-role client-role)
-(check-simulates client-role account-manager-role)
 
 (run-ground-dataspace ds-type
 
   (spawn ds-type
-    (export-roles "account-manager-role.rktd"
+    (lift+define-role acct-mngr-role
     (start-facet account-manager
       (field [balance Int 0])
       (assert (account (ref balance)))
@@ -46,15 +44,22 @@
           (set! balance (+ (ref balance) amount))))))
 
   (spawn ds-type
-    (print-role
+    (lift+define-role obs-role
     (start-facet observer
       (on (asserted (account (bind amount Int)))
           (displayln amount)))))
 
   (spawn ds-type
-    (print-role
+    (lift+define-role buyer-role
     (start-facet buyer
       (on (asserted (observe (deposit discard)))
           (start-facet deposits
             (assert (deposit 100))
             (assert (deposit -30))))))))
+
+(module+ test
+  (check-simulates acct-mngr-role account-manager-role)
+  (check-simulates obs-role client-role)
+  ;; Tried to write this, then it failed, I looked and buyer doesn't actually implement that spec
+  #;(check-simulates buyer-role client-role)
+  )
diff --git a/racket/typed/roles.rkt b/racket/typed/roles.rkt
index b986ba6..cea84ce 100644
--- a/racket/typed/roles.rkt
+++ b/racket/typed/roles.rkt
@@ -4,6 +4,7 @@
          #%app
          (rename-out [typed-quote quote])
          #%top-interaction
+         module+ module*
          ;; require & provides
          require only-in prefix-in except-in rename-in
          provide all-defined-out all-from-out rename-out except-out
@@ -63,7 +64,7 @@
          ;; DEBUG and utilities
          print-type print-role role-strings
          ;; Behavioral Roles
-         export-roles check-simulates
+         export-roles check-simulates lift+define-role
          ;; Extensions
          match cond
          submod for-syntax for-meta only-in except-in
@@ -659,12 +660,17 @@
   (define (synd->proto ty)
     (let convert ([ty (resugar-type ty)])
       (syntax-parse ty
-        #:literals (★/t Discard ∀/internal →/internal Role/internal Stop Reacts)
+        #:literals (★/t Bind Discard ∀/internal →/internal Role/internal Stop Reacts)
         [(ctor:id t ...)
          #:when (dict-has-key? TRANSLATION# #'ctor)
          (apply (dict-ref TRANSLATION# #'ctor) (stx-map convert #'(t ...)))]
         [★/t proto:⋆]
-        [Discard proto:⋆] ;; TODO - should prob have a Discard type in proto
+        [(Bind t)
+         ;; TODO - this is debatable handling
+         (convert #'t)]
+        [Discard
+         ;; TODO - should prob have a Discard type in proto
+         proto:⋆]
         [(∀/internal (X ...) body)
          ;; TODO
          (error "unimplemented")]
@@ -698,6 +704,15 @@
   ----------------------------------------
   [⊢ e- (⇒ : τ) (⇒ ν-ep (eps ...)) (⇒ ν-f (fs ...)) (⇒ ν-s (ss ...))])
 
+(define-typed-syntax (lift+define-role x:id e:expr) ≫
+  [⊢ e ≫ e- (⇒ : τ) (⇒ ν-ep (~effs)) (⇒ ν-f ((~and r  (~Role (_) _ ...)))) (⇒ ν-s (~effs))]
+  ;; because turnstile introduces a lot of intdef scopes; ideally, we'd be able to synthesize somethign
+  ;; with the right module scopes
+  #:with x+ (syntax-local-introduce (datum->syntax #f (syntax-e #'x)))
+  #:do [(syntax-local-lift-module-end-declaration #`(define-type-alias x+ r))]
+  ----------------------------------------
+  [⊢ e- (⇒ : τ) (⇒ ν-ep ()) (⇒ ν-f (r)) (⇒ ν-s ())])
+
 (define-syntax-parser check-simulates
   [(_ τ-impl:type τ-spec:type)
   (define τ-impl- (synd->proto #'τ-impl.norm))
@@ -708,6 +723,7 @@
     (raise-syntax-error #f "type doesn't simulate spec" this-syntax))
   #'(#%app- void-)])
 
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Tests
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;