From 33af13016b3f8713b8eca942679f3c6e122958a4 Mon Sep 17 00:00:00 2001
From: Sam Caldwell <samcaldwell@utexas.edu>
Date: Mon, 30 Jul 2018 11:54:05 -0400
Subject: [PATCH] dataspace form

---
 racket/typed/examples/roles/bank-account.rkt  | 46 ++++++++++---------
 .../typed/examples/roles/simple-dataspace.rkt |  7 +++
 racket/typed/roles.rkt                        | 26 ++++++++---
 3 files changed, 51 insertions(+), 28 deletions(-)
 create mode 100644 racket/typed/examples/roles/simple-dataspace.rkt

diff --git a/racket/typed/examples/roles/bank-account.rkt b/racket/typed/examples/roles/bank-account.rkt
index 3c5ef2b..3ed0502 100644
--- a/racket/typed/examples/roles/bank-account.rkt
+++ b/racket/typed/examples/roles/bank-account.rkt
@@ -18,27 +18,29 @@
      (Observe DepositRequest)
      (Observe (Observe DepositRequest))))
 
-(spawn ds-type
-  (print-role
-  (start-facet account-manager
-    (fields [balance Int 0])
-    (assert (account (ref balance)))
-    (on (asserted (deposit (bind amount Int)))
-        (set! balance (+ (ref balance) amount))))))
+(dataspace ds-type
 
-(spawn ds-type
-  (print-role
-  (start-facet observer
-    (fields)
-    (on (asserted (account (bind amount Int)))
-        (displayln amount)))))
+  (spawn ds-type
+    (print-role
+    (start-facet account-manager
+      (fields [balance Int 0])
+      (assert (account (ref balance)))
+      (on (asserted (deposit (bind amount Int)))
+          (set! balance (+ (ref balance) amount))))))
 
-(spawn ds-type
-  (print-role
-  (start-facet buyer
-    (fields)
-    (on (asserted (observe (deposit discard)))
-        (start-facet deposits
-          (fields)
-          (assert (deposit 100))
-          (assert (deposit -30)))))))
\ No newline at end of file
+  (spawn ds-type
+    (print-role
+    (start-facet observer
+      (fields)
+      (on (asserted (account (bind amount Int)))
+          (displayln amount)))))
+
+  (spawn ds-type
+    (print-role
+    (start-facet buyer
+      (fields)
+      (on (asserted (observe (deposit discard)))
+          (start-facet deposits
+            (fields)
+            (assert (deposit 100))
+            (assert (deposit -30))))))))
\ No newline at end of file
diff --git a/racket/typed/examples/roles/simple-dataspace.rkt b/racket/typed/examples/roles/simple-dataspace.rkt
new file mode 100644
index 0000000..350a980
--- /dev/null
+++ b/racket/typed/examples/roles/simple-dataspace.rkt
@@ -0,0 +1,7 @@
+#lang typed/syndicate/roles
+
+(dataspace Int
+  (spawn Int
+    (start-facet _
+      (fields)
+      (assert 42))))
diff --git a/racket/typed/roles.rkt b/racket/typed/roles.rkt
index 51bbbc7..d120525 100644
--- a/racket/typed/roles.rkt
+++ b/racket/typed/roles.rkt
@@ -10,7 +10,7 @@
          FacetName Field ★/t
          Observe Inbound Outbound Actor U
          ;; Statements
-         #;let spawn #;dataspace start-facet set! #;begin #;stop #;unsafe-do
+         #;let spawn dataspace start-facet set! #;begin #;stop #;unsafe-do
          ;; endpoints
          assert on
          ;; expressions
@@ -408,10 +408,7 @@
      (stx-andmap (lambda (t) (<: t t2)) #'(τ1 ...))]
     [(_ (~U* τ2:type ...))
      (stx-ormap (lambda (t) (<: t1 t)) #'(τ2 ...))]
-    ;; TODO
-    #;[((~Actor τ1:type) (~Actor τ2:type))
-     ;; should these be .norm? Is the invariant that inputs are always fully
-     ;; evalutated/expanded?
+    [((~Actor τ1) (~Actor τ2))
      (and (<: #'τ1 #'τ2)
           (<: (∩ (strip-? #'τ1) #'τ2) #'τ1))]
     [((~AssertionSet τ1) (~AssertionSet τ2))
@@ -733,13 +730,30 @@
   #:fail-unless (project-safe? (∩ (strip-? #'τ-o) #'τ-c.norm)
                                #'τ-i)
                 "Not prepared to handle all inputs"
+  #:with τ-a (type-eval #'(Actor τ-c.norm))
   --------------------------------------------------------------------------------------------
   [⊢ (syndicate:spawn (syndicate:on-start s-)) (⇒ : ★/t)
-                                               (⇒ s ((Actor τ-c)))
+                                               (⇒ s (τ-a))
                                                (⇒ a ())
                                                (⇒ r ())
                                                (⇒ f ())])
 
+(define-typed-syntax (dataspace τ-c:type s ...) ≫
+  #:fail-unless (flat-type? #'τ-c.norm) "Communication type must be first-order"
+  [⊢ s ≫ s- (⇒ a (~effs)) (⇒ r (~effs)) (⇒ s (~effs τ-s ...)) (⇒ f (~effs))] ...
+  #:with τ-actor (type-eval #'(Actor τ-c.norm))
+  #:fail-unless (stx-andmap (lambda (t) (<: t #'τ-actor)) #'(τ-s ... ...))
+                "Not all actors conform to communication type"
+  #:with τ-ds-i (strip-inbound #'τ-c.norm)
+  #:with τ-ds-o (strip-outbound #'τ-c.norm)
+  #:with τ-relay (relay-interests #'τ-c.norm)
+  -----------------------------------------------------------------------------------
+  [⊢ (syndicate:dataspace s- ...) (⇒ : ★/t)
+                                  (⇒ s ((Actor (U τ-ds-i τ-ds-o τ-relay))))
+                                  (⇒ a ())
+                                  (⇒ r ())
+                                  (⇒ f ())])
+
 (define-typed-syntax (set! x:id e:expr) ≫
   [⊢ e ≫ e- (⇒ : τ)]
   #:fail-unless (pure? #'e-) "expression not allowed to have effects"