Don't use syndicate's action-collecting module-begin
Implicitly starting a dataspace with top-level actions is a hole for the type system, which needs to know the type of possible assertions. Instead, provide `run-ground-dataspace` for kicking off the program.
This commit is contained in:
parent
d363bd0c46
commit
0897036557
|
@ -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
|
||||
|
|
|
@ -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)))
|
||||
|
|
|
@ -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")))))))))))
|
||||
|
|
|
@ -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)))
|
||||
|
|
|
@ -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])
|
||||
|
|
|
@ -1,6 +1,6 @@
|
|||
#lang typed/syndicate/roles
|
||||
|
||||
(dataspace Int
|
||||
(run-ground-dataspace Int
|
||||
(spawn Int
|
||||
(start-facet _
|
||||
(assert 42))))
|
||||
|
|
|
@ -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")
|
||||
|
|
|
@ -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)
|
||||
|
|
|
@ -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))
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -66,7 +66,7 @@
|
|||
(Role (_)
|
||||
(Shares (QuoteT String Int))))))
|
||||
|
||||
(dataspace ds-type
|
||||
(run-ground-dataspace ds-type
|
||||
|
||||
;; seller
|
||||
(spawn ds-type
|
||||
|
|
|
@ -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
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
|
|
Loading…
Reference in New Issue