dataspace form
This commit is contained in:
parent
1a4fc4dd4f
commit
33af13016b
|
@ -18,27 +18,29 @@
|
||||||
(Observe DepositRequest)
|
(Observe DepositRequest)
|
||||||
(Observe (Observe DepositRequest))))
|
(Observe (Observe DepositRequest))))
|
||||||
|
|
||||||
(spawn ds-type
|
(dataspace 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
|
(spawn ds-type
|
||||||
(print-role
|
(print-role
|
||||||
(start-facet observer
|
(start-facet account-manager
|
||||||
(fields)
|
(fields [balance Int 0])
|
||||||
(on (asserted (account (bind amount Int)))
|
(assert (account (ref balance)))
|
||||||
(displayln amount)))))
|
(on (asserted (deposit (bind amount Int)))
|
||||||
|
(set! balance (+ (ref balance) amount))))))
|
||||||
|
|
||||||
(spawn ds-type
|
(spawn ds-type
|
||||||
(print-role
|
(print-role
|
||||||
(start-facet buyer
|
(start-facet observer
|
||||||
(fields)
|
(fields)
|
||||||
(on (asserted (observe (deposit discard)))
|
(on (asserted (account (bind amount Int)))
|
||||||
(start-facet deposits
|
(displayln amount)))))
|
||||||
(fields)
|
|
||||||
(assert (deposit 100))
|
(spawn ds-type
|
||||||
(assert (deposit -30)))))))
|
(print-role
|
||||||
|
(start-facet buyer
|
||||||
|
(fields)
|
||||||
|
(on (asserted (observe (deposit discard)))
|
||||||
|
(start-facet deposits
|
||||||
|
(fields)
|
||||||
|
(assert (deposit 100))
|
||||||
|
(assert (deposit -30))))))))
|
|
@ -0,0 +1,7 @@
|
||||||
|
#lang typed/syndicate/roles
|
||||||
|
|
||||||
|
(dataspace Int
|
||||||
|
(spawn Int
|
||||||
|
(start-facet _
|
||||||
|
(fields)
|
||||||
|
(assert 42))))
|
|
@ -10,7 +10,7 @@
|
||||||
FacetName Field ★/t
|
FacetName Field ★/t
|
||||||
Observe Inbound Outbound Actor U
|
Observe Inbound Outbound Actor U
|
||||||
;; Statements
|
;; Statements
|
||||||
#;let spawn #;dataspace start-facet set! #;begin #;stop #;unsafe-do
|
#;let spawn dataspace start-facet set! #;begin #;stop #;unsafe-do
|
||||||
;; endpoints
|
;; endpoints
|
||||||
assert on
|
assert on
|
||||||
;; expressions
|
;; expressions
|
||||||
|
@ -408,10 +408,7 @@
|
||||||
(stx-andmap (lambda (t) (<: t t2)) #'(τ1 ...))]
|
(stx-andmap (lambda (t) (<: t t2)) #'(τ1 ...))]
|
||||||
[(_ (~U* τ2:type ...))
|
[(_ (~U* τ2:type ...))
|
||||||
(stx-ormap (lambda (t) (<: t1 t)) #'(τ2 ...))]
|
(stx-ormap (lambda (t) (<: t1 t)) #'(τ2 ...))]
|
||||||
;; TODO
|
[((~Actor τ1) (~Actor τ2))
|
||||||
#;[((~Actor τ1:type) (~Actor τ2:type))
|
|
||||||
;; should these be .norm? Is the invariant that inputs are always fully
|
|
||||||
;; evalutated/expanded?
|
|
||||||
(and (<: #'τ1 #'τ2)
|
(and (<: #'τ1 #'τ2)
|
||||||
(<: (∩ (strip-? #'τ1) #'τ2) #'τ1))]
|
(<: (∩ (strip-? #'τ1) #'τ2) #'τ1))]
|
||||||
[((~AssertionSet τ1) (~AssertionSet τ2))
|
[((~AssertionSet τ1) (~AssertionSet τ2))
|
||||||
|
@ -733,13 +730,30 @@
|
||||||
#:fail-unless (project-safe? (∩ (strip-? #'τ-o) #'τ-c.norm)
|
#:fail-unless (project-safe? (∩ (strip-? #'τ-o) #'τ-c.norm)
|
||||||
#'τ-i)
|
#'τ-i)
|
||||||
"Not prepared to handle all inputs"
|
"Not prepared to handle all inputs"
|
||||||
|
#:with τ-a (type-eval #'(Actor τ-c.norm))
|
||||||
--------------------------------------------------------------------------------------------
|
--------------------------------------------------------------------------------------------
|
||||||
[⊢ (syndicate:spawn (syndicate:on-start s-)) (⇒ : ★/t)
|
[⊢ (syndicate:spawn (syndicate:on-start s-)) (⇒ : ★/t)
|
||||||
(⇒ s ((Actor τ-c)))
|
(⇒ s (τ-a))
|
||||||
(⇒ a ())
|
(⇒ a ())
|
||||||
(⇒ r ())
|
(⇒ r ())
|
||||||
(⇒ f ())])
|
(⇒ 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) ≫
|
(define-typed-syntax (set! x:id e:expr) ≫
|
||||||
[⊢ e ≫ e- (⇒ : τ)]
|
[⊢ e ≫ e- (⇒ : τ)]
|
||||||
#:fail-unless (pure? #'e-) "expression not allowed to have effects"
|
#:fail-unless (pure? #'e-) "expression not allowed to have effects"
|
||||||
|
|
Loading…
Reference in New Issue