diff --git a/racket/typed/examples/roles/bank-account.rkt b/racket/typed/examples/roles/bank-account.rkt index 45bfb4c..a5fe16a 100644 --- a/racket/typed/examples/roles/bank-account.rkt +++ b/racket/typed/examples/roles/bank-account.rkt @@ -3,6 +3,7 @@ ;; Expected Output ;; 0 ;; 70 +;; #f (define-constructor (account balance) #:type-constructor AccountT @@ -31,7 +32,7 @@ (Role (client) (Reacts (Know Account)))) -(dataspace ds-type +(run-ground-dataspace ds-type (spawn ds-type (print-role @@ -53,4 +54,4 @@ (on (asserted (observe (deposit discard))) (start-facet deposits (assert (deposit 100)) - (assert (deposit -30)))))))) \ No newline at end of file + (assert (deposit -30)))))))) diff --git a/racket/typed/examples/roles/book-club.rkt b/racket/typed/examples/roles/book-club.rkt index 0f83ace..01c8664 100644 --- a/racket/typed/examples/roles/book-club.rkt +++ b/racket/typed/examples/roles/book-club.rkt @@ -162,7 +162,7 @@ (printf "~a responds to suggested book ~a: ~a\n" name title answer) (assert (book-interest title name answer)))))) -(dataspace τc +(run-ground-dataspace τc (spawn-seller (list (tuple "The Wind in the Willows" 5) (tuple "Catch 22" 2) (tuple "Candide" 3))) @@ -171,4 +171,4 @@ "Candide" "Encyclopaedia Brittannica")) (spawn-club-member "tony" (list "Candide")) - (spawn-club-member "sam" (list "Encyclopaedia Brittannica" "Candide"))) \ No newline at end of file + (spawn-club-member "sam" (list "Encyclopaedia Brittannica" "Candide"))) diff --git a/racket/typed/examples/roles/chat-tcp2.rkt b/racket/typed/examples/roles/chat-tcp2.rkt index 1e0d73d..2790024 100644 --- a/racket/typed/examples/roles/chat-tcp2.rkt +++ b/racket/typed/examples/roles/chat-tcp2.rkt @@ -21,11 +21,7 @@ (U chat-comm Tcp2Driver)) -;; without this line, there's no check on what type of actors `activate!` -;; spawns. However, putting these actors in a dataspace interferes with the -;; ground activity performed by the tcp driver (by making all activity one level -;; removed) -;; (dataspace chat-ds +(run-ground-dataspace chat-ds (activate!) (spawn chat-ds @@ -43,4 +39,4 @@ (on stop (send! (tcp-out id (string->bytes/utf-8 (~a user " left\n"))))) (on (message (speak user (bind text String))) - (send! (tcp-out id (string->bytes/utf-8 (~a user " says '" text "'\n")))))))))) + (send! (tcp-out id (string->bytes/utf-8 (~a user " says '" text "'\n"))))))))))) diff --git a/racket/typed/examples/roles/ping-pong.rkt b/racket/typed/examples/roles/ping-pong.rkt index f32677e..0e99f64 100644 --- a/racket/typed/examples/roles/ping-pong.rkt +++ b/racket/typed/examples/roles/ping-pong.rkt @@ -7,7 +7,7 @@ (U (Message (Tuple String Int)) (Observe (Tuple String ★/t)))) -(dataspace ds-type +(run-ground-dataspace ds-type (spawn ds-type (start-facet echo (on (message (tuple "ping" (bind x Int))) @@ -17,4 +17,4 @@ (on start (send! (tuple "ping" 8339))) (on (message (tuple "pong" (bind x Int))) - (printf "pong: ~v\n" x))))) \ No newline at end of file + (printf "pong: ~v\n" x))))) diff --git a/racket/typed/examples/roles/simple-dataflow.rkt b/racket/typed/examples/roles/simple-dataflow.rkt index b3ce7f5..25fd91d 100644 --- a/racket/typed/examples/roles/simple-dataflow.rkt +++ b/racket/typed/examples/roles/simple-dataflow.rkt @@ -8,7 +8,7 @@ (U (Tuple String Int) (Observe ★/t))) -(dataspace ds-type +(run-ground-dataspace ds-type (spawn ds-type (start-facet server (field [f Int 0]) @@ -18,4 +18,4 @@ (set! f v)))) (spawn ds-type (start-facet client - (assert (tuple "key" 18))))) \ No newline at end of file + (assert (tuple "key" 18))))) diff --git a/racket/typed/examples/roles/simple-dataspace.rkt b/racket/typed/examples/roles/simple-dataspace.rkt index 3ab69c9..a7d3740 100644 --- a/racket/typed/examples/roles/simple-dataspace.rkt +++ b/racket/typed/examples/roles/simple-dataspace.rkt @@ -1,6 +1,6 @@ #lang typed/syndicate/roles -(dataspace Int +(run-ground-dataspace Int (spawn Int (start-facet _ (assert 42)))) diff --git a/racket/typed/examples/roles/simple-during.rkt b/racket/typed/examples/roles/simple-during.rkt index 335821e..54bf507 100644 --- a/racket/typed/examples/roles/simple-during.rkt +++ b/racket/typed/examples/roles/simple-during.rkt @@ -9,7 +9,7 @@ (define-type-alias ds-type (U (Tuple String) (Observe (Tuple ★/t)))) -(dataspace ds-type +(run-ground-dataspace ds-type (spawn ds-type (start-facet _ (during (tuple "GO") diff --git a/racket/typed/examples/roles/simple-query-set.rkt b/racket/typed/examples/roles/simple-query-set.rkt index 059be43..8ee7f38 100644 --- a/racket/typed/examples/roles/simple-query-set.rkt +++ b/racket/typed/examples/roles/simple-query-set.rkt @@ -8,7 +8,7 @@ (U (Tuple String Int) (Observe ★/t))) -(dataspace ds-type +(run-ground-dataspace ds-type (spawn ds-type (start-facet querier (define/query-set key (tuple "key" (bind v Int)) v) @@ -19,4 +19,4 @@ (assert (tuple "key" 88)) (during (tuple "size" (bind v Int)) (on start - (printf "size: ~v\n" v)))))) \ No newline at end of file + (printf "size: ~v\n" v)))))) diff --git a/racket/typed/examples/roles/simple-query-value.rkt b/racket/typed/examples/roles/simple-query-value.rkt index 32c51c5..bd1f0ad 100644 --- a/racket/typed/examples/roles/simple-query-value.rkt +++ b/racket/typed/examples/roles/simple-query-value.rkt @@ -8,7 +8,7 @@ (U (Tuple String Int) (Observe ★/t))) -(dataspace ds-type +(run-ground-dataspace ds-type (spawn ds-type (start-facet querier (define/query-value key 0 (tuple "key" (bind v Int)) (+ v 1)) @@ -18,4 +18,4 @@ (assert (tuple "key" 18)) (during (tuple "query" (bind v Int)) (on start - (printf "query: ~v\n" v)))))) \ No newline at end of file + (printf "query: ~v\n" v)))))) diff --git a/racket/typed/examples/roles/simple-stop-facet.rkt b/racket/typed/examples/roles/simple-stop-facet.rkt index fbf54a5..f771442 100644 --- a/racket/typed/examples/roles/simple-stop-facet.rkt +++ b/racket/typed/examples/roles/simple-stop-facet.rkt @@ -12,7 +12,7 @@ (U (Tuple Int) (Observe (Tuple ★/t)))) -(dataspace ds-type +(run-ground-dataspace ds-type (spawn ds-type (print-role (start-facet doomed @@ -35,4 +35,4 @@ (start-facet meep (assert (tuple 9)) (on (asserted (tuple 88)) - (stop meep))))) \ No newline at end of file + (stop meep))))) diff --git a/racket/typed/examples/roles/two-buyer-protocol.rkt b/racket/typed/examples/roles/two-buyer-protocol.rkt index 9027eea..a49aee3 100644 --- a/racket/typed/examples/roles/two-buyer-protocol.rkt +++ b/racket/typed/examples/roles/two-buyer-protocol.rkt @@ -66,7 +66,7 @@ (Role (_) (Shares (QuoteT String Int)))))) -(dataspace ds-type +(run-ground-dataspace ds-type ;; seller (spawn ds-type @@ -145,4 +145,4 @@ [discard (begin (displayln "Order Rejected") (stop purchase))]))))))]))))) -) \ No newline at end of file +) diff --git a/racket/typed/roles.rkt b/racket/typed/roles.rkt index 417ea53..11a1d19 100644 --- a/racket/typed/roles.rkt +++ b/racket/typed/roles.rkt @@ -1,10 +1,12 @@ #lang turnstile -(provide (rename-out [syndicate:#%module-begin #%module-begin]) +(provide #%module-begin (rename-out [typed-app #%app]) (rename-out [typed-quote quote]) #%top-interaction require only-in + ;; Start dataspace programs + run-ground-dataspace ;; Types Int Bool String Tuple Bind Discard → List ByteString Symbol Role Reacts Shares Know ¬Know Message OnDataflow Stop OnStart OnStop @@ -1677,6 +1679,17 @@ (⇒ ν-f (fs ... ...)) (⇒ ν-s (ss ... ...))]) +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Ground Dataspace +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; n.b. this is a blocking operation, so an actor that uses this internally +;; won't necessarily terminate. +(define-typed-syntax (run-ground-dataspace τ-c:type s ...) ≫ + [⊢ (dataspace τ-c s ...) ≫ ((~literal erased) ((~literal syndicate:dataspace) s- ...)) (⇒ : t)] + ----------------------------------------------------------------------------------- + [⊢ (syndicate:run-ground s- ...) (⇒ : (AssertionSet τ-c))]) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Primitives ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;