diff --git a/racket/typed/examples/bank-account.rkt b/racket/typed/examples/bank-account.rkt index a3d4ed1..b6bcf34 100644 --- a/racket/typed/examples/bank-account.rkt +++ b/racket/typed/examples/bank-account.rkt @@ -1,14 +1,19 @@ #lang typed/syndicate +;; Expected Output +;; 0 +;; 70 +;; #f + (define-constructor (account balance) #:type-constructor AccountT #:with Account (AccountT Int) - #:with AccountRequest (AccountT ★)) + #:with AccountRequest (AccountT ★/t)) (define-constructor (deposit amount) #:type-constructor DepositT #:with Deposit (DepositT Int) - #:with DepositRequest (DepositT ★)) + #:with DepositRequest (DepositT ★/t)) (define-type-alias ds-type (U Account @@ -18,45 +23,43 @@ (Observe DepositRequest) (Observe (Observe DepositRequest)))) -(dataspace ds-type +(define-type-alias account-manager-role + (Role (account-manager) + (Shares Account) + (Reacts (Asserted Deposit)))) - (spawn ds-type - (facet _ - (fields [balance Int 0]) - (assert (account (ref balance))) - (on (asserted (deposit (bind amount Int))) - (set! balance (+ (ref balance) amount))))) +(define-type-alias client-role + (Role (client) + (Reacts (Asserted Account)))) - (spawn ds-type - (facet _ - (fields) - (on (asserted (account (bind amount Int))) - (displayln amount)))) - (spawn ds-type - (facet _ - (fields) - (on (asserted (observe (deposit discard))) - (facet _ - (fields) - (assert (deposit 100)) - (assert (deposit -30))))))) +(run-ground-dataspace ds-type -#| -;; Hello-worldish "bank account" example. + (spawn ds-type + (lift+define-role acct-mngr-role + (start-facet account-manager + (field [balance Int 0]) + (assert (account (ref balance))) + (on (asserted (deposit (bind amount Int))) + (set! balance (+ (ref balance) amount)))))) -(struct account (balance) #:prefab) -(struct deposit (amount) #:prefab) + (spawn ds-type + (lift+define-role obs-role + (start-facet observer + (on (asserted (account (bind amount Int))) + (displayln amount))))) -(spawn (field [balance 0]) - (assert (account (balance))) - (on (message (deposit $amount)) - (balance (+ (balance) amount)))) + (spawn ds-type + (lift+define-role buyer-role + (start-facet buyer + (on (asserted (observe (deposit discard))) + (start-facet deposits + (assert (deposit 100)) + (assert (deposit -30)))))))) -(spawn (on (asserted (account $balance)) - (printf "Balance changed to ~a\n" balance))) - -(spawn* (until (asserted (observe (deposit _)))) - (send! (deposit +100)) - (send! (deposit -30))) -|# \ No newline at end of file +(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/examples/roles/book-club.rkt b/racket/typed/examples/book-club.rkt similarity index 99% rename from racket/typed/examples/roles/book-club.rkt rename to racket/typed/examples/book-club.rkt index 77c792a..0897892 100644 --- a/racket/typed/examples/roles/book-club.rkt +++ b/racket/typed/examples/book-club.rkt @@ -1,4 +1,4 @@ -#lang typed/syndicate/roles +#lang typed/syndicate ;; Expected Output ;; leader learns that there are 5 copies of The Wind in the Willows diff --git a/racket/typed/examples/roles/cell.rkt b/racket/typed/examples/cell.rkt similarity index 98% rename from racket/typed/examples/roles/cell.rkt rename to racket/typed/examples/cell.rkt index e9c0131..321b190 100644 --- a/racket/typed/examples/roles/cell.rkt +++ b/racket/typed/examples/cell.rkt @@ -1,4 +1,4 @@ -#lang typed/syndicate/roles +#lang typed/syndicate ;; adapted from section 8.3 of Tony's dissertation diff --git a/racket/typed/examples/roles/chat-tcp2.rkt b/racket/typed/examples/chat-tcp2.rkt similarity index 97% rename from racket/typed/examples/roles/chat-tcp2.rkt rename to racket/typed/examples/chat-tcp2.rkt index 90fc97d..913bf7d 100644 --- a/racket/typed/examples/roles/chat-tcp2.rkt +++ b/racket/typed/examples/chat-tcp2.rkt @@ -1,4 +1,4 @@ -#lang typed/syndicate/roles +#lang typed/syndicate (require typed/syndicate/drivers/tcp) diff --git a/racket/typed/examples/roles/file-system.rkt b/racket/typed/examples/file-system.rkt similarity index 93% rename from racket/typed/examples/roles/file-system.rkt rename to racket/typed/examples/file-system.rkt index 7113c3c..827ecaa 100644 --- a/racket/typed/examples/roles/file-system.rkt +++ b/racket/typed/examples/file-system.rkt @@ -1,4 +1,4 @@ -#lang typed/syndicate/roles +#lang typed/syndicate (define-constructor (file name content) #:type-constructor FileT @@ -31,4 +31,4 @@ (define-type-alias Writer (Role (writer) (Sends Save) - (Sends Delete))) \ No newline at end of file + (Sends Delete))) diff --git a/racket/typed/examples/roles/flink-support.rkt b/racket/typed/examples/flink-support.rkt similarity index 100% rename from racket/typed/examples/roles/flink-support.rkt rename to racket/typed/examples/flink-support.rkt diff --git a/racket/typed/examples/roles/flink.rkt b/racket/typed/examples/flink.rkt similarity index 98% rename from racket/typed/examples/roles/flink.rkt rename to racket/typed/examples/flink.rkt index ff0456e..521a544 100644 --- a/racket/typed/examples/roles/flink.rkt +++ b/racket/typed/examples/flink.rkt @@ -1,4 +1,4 @@ -#lang typed/syndicate/roles +#lang typed/syndicate ;; --------------------------------------------------------------------------------------------------- ;; Protocol @@ -550,8 +550,8 @@ The JobManager then performs the job and, when finished, asserts (spawn-client (string->job INPUT))) (module+ test - (verify-actors (Eventually (A (JobCompletion ID (List InputTask) TaskResult))) - #;(Always (Implies (A (Observe (JobCompletion ID (List InputTask) ★/t))) + #;(verify-actors #;(Eventually (A (JobCompletion ID (List InputTask) TaskResult))) + (Always (Implies (A (Observe (JobCompletion ID (List InputTask) ★/t))) (Eventually (A (JobCompletion ID (List InputTask) TaskResult))))) job-manager-impl task-manager-impl @@ -570,3 +570,7 @@ The JobManager then performs the job and, when finished, asserts (check-has-simulating-subgraph task-manager-impl TaskPerformer) (check-has-simulating-subgraph task-manager-impl TaskAssigner) (check-has-simulating-subgraph job-manager-impl TaskAssigner)) + +;; infinite loop? +#;(module+ test + (check-simulates job-manager-impl job-manager-impl)) diff --git a/racket/typed/examples/roles/internal-knowledge.rkt b/racket/typed/examples/internal-knowledge.rkt similarity index 98% rename from racket/typed/examples/roles/internal-knowledge.rkt rename to racket/typed/examples/internal-knowledge.rkt index 65c6cf8..fe91fea 100644 --- a/racket/typed/examples/roles/internal-knowledge.rkt +++ b/racket/typed/examples/internal-knowledge.rkt @@ -1,4 +1,4 @@ -#lang typed/syndicate/roles +#lang typed/syndicate ;; Expected Output: #| diff --git a/racket/typed/examples/roles/ping-pong.rkt b/racket/typed/examples/ping-pong.rkt similarity index 97% rename from racket/typed/examples/roles/ping-pong.rkt rename to racket/typed/examples/ping-pong.rkt index f0cd762..66ad6f8 100644 --- a/racket/typed/examples/roles/ping-pong.rkt +++ b/racket/typed/examples/ping-pong.rkt @@ -1,4 +1,4 @@ -#lang typed/syndicate/roles +#lang typed/syndicate ;; Expected Output ;; pong: 8339 diff --git a/racket/typed/examples/roles/provides.rkt b/racket/typed/examples/provides.rkt similarity index 61% rename from racket/typed/examples/roles/provides.rkt rename to racket/typed/examples/provides.rkt index 3ab3d46..4505275 100644 --- a/racket/typed/examples/roles/provides.rkt +++ b/racket/typed/examples/provides.rkt @@ -1,8 +1,8 @@ -#lang typed/syndicate/roles +#lang typed/syndicate (provide a-fun) (define (a-fun [x : Int] -> Int) (+ x 1)) -#;(a-fun 5) \ No newline at end of file +#;(a-fun 5) diff --git a/racket/typed/examples/roles/realize.rkt b/racket/typed/examples/realize.rkt similarity index 94% rename from racket/typed/examples/roles/realize.rkt rename to racket/typed/examples/realize.rkt index d11a04d..72ee32d 100644 --- a/racket/typed/examples/roles/realize.rkt +++ b/racket/typed/examples/realize.rkt @@ -1,4 +1,4 @@ -#lang typed/syndicate/roles +#lang typed/syndicate ;; Expected Output: #| diff --git a/racket/typed/examples/roles/require-struct/client.rkt b/racket/typed/examples/require-struct/client.rkt similarity index 89% rename from racket/typed/examples/roles/require-struct/client.rkt rename to racket/typed/examples/require-struct/client.rkt index 8066afd..ee93840 100644 --- a/racket/typed/examples/roles/require-struct/client.rkt +++ b/racket/typed/examples/require-struct/client.rkt @@ -1,4 +1,4 @@ -#lang typed/syndicate/roles +#lang typed/syndicate (require-struct msg #:as Msg #:from "driver.rkt") diff --git a/racket/typed/examples/roles/require-struct/driver.rkt b/racket/typed/examples/require-struct/driver.rkt similarity index 100% rename from racket/typed/examples/roles/require-struct/driver.rkt rename to racket/typed/examples/require-struct/driver.rkt diff --git a/racket/typed/examples/require:typed/client.rkt b/racket/typed/examples/require:typed/client.rkt new file mode 100644 index 0000000..5bc3310 --- /dev/null +++ b/racket/typed/examples/require:typed/client.rkt @@ -0,0 +1,5 @@ +#lang typed/syndicate + +(require/typed "lib.rkt" [x : Int]) + +(displayln (+ x 1)) diff --git a/racket/typed/examples/roles/require:typed/lib.rkt b/racket/typed/examples/require:typed/lib.rkt similarity index 100% rename from racket/typed/examples/roles/require:typed/lib.rkt rename to racket/typed/examples/require:typed/lib.rkt diff --git a/racket/typed/examples/requires.rkt b/racket/typed/examples/requires.rkt new file mode 100644 index 0000000..d4aebdc --- /dev/null +++ b/racket/typed/examples/requires.rkt @@ -0,0 +1,5 @@ +#lang typed/syndicate + +(require "provides.rkt") + +(a-fun 5) diff --git a/racket/typed/examples/roles/bank-account.rkt b/racket/typed/examples/roles/bank-account.rkt deleted file mode 100644 index 9d5ddc4..0000000 --- a/racket/typed/examples/roles/bank-account.rkt +++ /dev/null @@ -1,65 +0,0 @@ -#lang typed/syndicate/roles - -;; Expected Output -;; 0 -;; 70 -;; #f - -(define-constructor (account balance) - #:type-constructor AccountT - #:with Account (AccountT Int) - #:with AccountRequest (AccountT ★/t)) - -(define-constructor (deposit amount) - #:type-constructor DepositT - #:with Deposit (DepositT Int) - #:with DepositRequest (DepositT ★/t)) - -(define-type-alias ds-type - (U Account - (Observe AccountRequest) - (Observe (Observe AccountRequest)) - Deposit - (Observe DepositRequest) - (Observe (Observe DepositRequest)))) - -(define-type-alias account-manager-role - (Role (account-manager) - (Shares Account) - (Reacts (Asserted Deposit)))) - -(define-type-alias client-role - (Role (client) - (Reacts (Asserted Account)))) - - -(run-ground-dataspace ds-type - - (spawn ds-type - (lift+define-role acct-mngr-role - (start-facet account-manager - (field [balance Int 0]) - (assert (account (ref balance))) - (on (asserted (deposit (bind amount Int))) - (set! balance (+ (ref balance) amount)))))) - - (spawn ds-type - (lift+define-role obs-role - (start-facet observer - (on (asserted (account (bind amount Int))) - (displayln amount))))) - - (spawn ds-type - (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/examples/roles/require:typed/client.rkt b/racket/typed/examples/roles/require:typed/client.rkt deleted file mode 100644 index 8a3509b..0000000 --- a/racket/typed/examples/roles/require:typed/client.rkt +++ /dev/null @@ -1,5 +0,0 @@ -#lang typed/syndicate/roles - -(require/typed "lib.rkt" [x : Int]) - -(displayln (+ x 1)) \ No newline at end of file diff --git a/racket/typed/examples/roles/requires.rkt b/racket/typed/examples/roles/requires.rkt deleted file mode 100644 index 4cae840..0000000 --- a/racket/typed/examples/roles/requires.rkt +++ /dev/null @@ -1,5 +0,0 @@ -#lang typed/syndicate/roles - -(require "provides.rkt") - -(a-fun 5) \ No newline at end of file diff --git a/racket/typed/examples/roles/two-buyer-protocol.rkt b/racket/typed/examples/roles/two-buyer-protocol.rkt deleted file mode 100644 index de94a32..0000000 --- a/racket/typed/examples/roles/two-buyer-protocol.rkt +++ /dev/null @@ -1,163 +0,0 @@ -#lang typed/syndicate/roles - -;; Expected Output -;; Completed Order: -;; Catch 22 -;; 10001483 -;; March 9th - -(define-constructor (price v) - #:type-constructor PriceT - #:with Price (PriceT Int)) - -(define-constructor (out-of-stock) - #:type-constructor OutOfStockT - #:with OutOfStock (OutOfStockT)) - -(define-type-alias QuoteAnswer - (U Price OutOfStock)) - -(define-constructor (quote title answer) - #:type-constructor QuoteT - #:with Quote (QuoteT String QuoteAnswer) - #:with QuoteRequest (Observe (QuoteT String ★/t)) - #:with QuoteInterest (Observe (QuoteT ★/t ★/t))) - -(define-constructor (split-proposal title price contribution accepted) - #:type-constructor SplitProposalT - #:with SplitProposal (SplitProposalT String Int Int Bool) - #:with SplitRequest (Observe (SplitProposalT String Int Int ★/t)) - #:with SplitInterest (Observe (SplitProposalT ★/t ★/t ★/t ★/t))) - -(define-constructor (order-id id) - #:type-constructor OrderIdT - #:with OrderId (OrderIdT Int)) - -(define-constructor (delivery-date date) - #:type-constructor DeliveryDateT - #:with DeliveryDate (DeliveryDateT String)) - -(define-type-alias (Maybe t) - (U t Bool)) - -(define-constructor (order title price oid delivery-date) - #:type-constructor OrderT - #:with Order (OrderT String Int (Maybe OrderId) (Maybe DeliveryDate)) - #:with OrderRequest (Observe (OrderT String Int ★/t ★/t)) - #:with OrderInterest (Observe (OrderT ★/t ★/t ★/t ★/t))) - -(define-type-alias ds-type - (U ;; quotes - Quote - QuoteRequest - (Observe QuoteInterest) - ;; splits - SplitProposal - SplitRequest - (Observe SplitInterest) - ;; orders - Order - OrderRequest - (Observe OrderInterest))) - -(define-type-alias seller-role - (Role (seller) - (During (Observe (QuoteT String ★/t)) - (Shares (QuoteT String QuoteAnswer))) - #;(Reacts (Asserted (Observe (QuoteT String ★/t))) - (Role (_) - ;; QuoteAnswer was originally, erroneously, Int - (Shares (QuoteT String QuoteAnswer)))))) - -(run-ground-dataspace ds-type - -;; seller -(spawn ds-type - (lift+define-role seller-impl - (start-facet _ ;; #:implements seller-role - (field [book (Tuple String Int) (tuple "Catch 22" 22)] - [next-order-id Int 10001483]) - (on (asserted (observe (quote (bind title String) discard))) - (start-facet x - (on (retracted (observe (quote title discard))) - (stop x)) - (define answer - (match title - ["Catch 22" - (price 22)] - [_ - (out-of-stock)])) - (assert (quote title answer)))) - (on (asserted (observe (order (bind title String) (bind offer Int) discard discard))) - (start-facet x - (on (retracted (observe (order title offer discard discard))) - (stop x)) - (let ([asking-price 22]) - (if (and (equal? title "Catch 22") (>= offer asking-price)) - (let ([id (ref next-order-id)]) - (set! next-order-id (+ 1 id)) - (assert (order title offer (order-id id) (delivery-date "March 9th")))) - (assert (order title offer #f #f))))))))) - -;; buyer A -(spawn ds-type - (lift+define-role buyer-a-impl - (start-facet buyer - (field [title String "Catch 22"] - [budget Int 1000]) - (on (asserted (quote (ref title) (bind answer QuoteAnswer))) - (match answer - [(out-of-stock) - (stop buyer)] - [(price (bind amount Int)) - (start-facet negotiation - (field [contribution Int (/ amount 2)]) - (on (asserted (split-proposal (ref title) amount (ref contribution) (bind accept? Bool))) - (if accept? - (stop buyer) - (if (> (ref contribution) (- amount 5)) - (stop negotiation (displayln "negotiation failed")) - (set! contribution - (+ (ref contribution) (/ (- amount (ref contribution)) 2)))))))]))))) - -;; buyer B -(spawn ds-type - (lift+define-role buyer-b-impl - (start-facet buyer-b - (field [funds Int 5]) - (on (asserted (observe (split-proposal (bind title String) (bind price Int) (bind their-contribution Int) discard))) - (let ([my-contribution (- price their-contribution)]) - (cond - [(> my-contribution (ref funds)) - (start-facet decline - (assert (split-proposal title price their-contribution #f)) - (on (retracted (observe (split-proposal title price their-contribution discard))) - (stop decline)))] - [#t - (start-facet accept - (assert (split-proposal title price their-contribution #t)) - (on (retracted (observe (split-proposal title price their-contribution discard))) - (stop accept)) - (on start - (spawn ds-type - (start-facet purchase - (on (asserted (order title price (bind order-id? (Maybe OrderId)) (bind delivery-date? (Maybe DeliveryDate)))) - (match (tuple order-id? delivery-date?) - [(tuple (order-id (bind id Int)) (delivery-date (bind date String))) - ;; complete! - (begin (displayln "Completed Order:") - (displayln title) - (displayln id) - (displayln date) - (stop purchase))] - [discard - (begin (displayln "Order Rejected") - (stop purchase))]))))))])))))) -) - -(module+ test - (check-simulates seller-impl seller-impl) - ;; found a bug in spec, see seller-role above - (check-simulates seller-impl seller-role) - (check-simulates buyer-a-impl buyer-a-impl) - (check-simulates buyer-b-impl buyer-b-impl)) diff --git a/racket/typed/examples/roles/simple-dataflow.rkt b/racket/typed/examples/simple-dataflow.rkt similarity index 93% rename from racket/typed/examples/roles/simple-dataflow.rkt rename to racket/typed/examples/simple-dataflow.rkt index 25fd91d..35a1182 100644 --- a/racket/typed/examples/roles/simple-dataflow.rkt +++ b/racket/typed/examples/simple-dataflow.rkt @@ -1,4 +1,4 @@ -#lang typed/syndicate/roles +#lang typed/syndicate ;; Expected Output ;; f: 0 diff --git a/racket/typed/examples/roles/simple-dataspace.rkt b/racket/typed/examples/simple-dataspace.rkt similarity index 74% rename from racket/typed/examples/roles/simple-dataspace.rkt rename to racket/typed/examples/simple-dataspace.rkt index a7d3740..c5a3b56 100644 --- a/racket/typed/examples/roles/simple-dataspace.rkt +++ b/racket/typed/examples/simple-dataspace.rkt @@ -1,4 +1,4 @@ -#lang typed/syndicate/roles +#lang typed/syndicate (run-ground-dataspace Int (spawn Int diff --git a/racket/typed/examples/roles/simple-during.rkt b/racket/typed/examples/simple-during.rkt similarity index 95% rename from racket/typed/examples/roles/simple-during.rkt rename to racket/typed/examples/simple-during.rkt index 54bf507..b29cb5e 100644 --- a/racket/typed/examples/roles/simple-during.rkt +++ b/racket/typed/examples/simple-during.rkt @@ -1,4 +1,4 @@ -#lang typed/syndicate/roles +#lang typed/syndicate ;; Expected Output ;; +GO diff --git a/racket/typed/examples/roles/simple-query-hash.rkt b/racket/typed/examples/simple-query-hash.rkt similarity index 96% rename from racket/typed/examples/roles/simple-query-hash.rkt rename to racket/typed/examples/simple-query-hash.rkt index bb25fe3..0e1c32b 100644 --- a/racket/typed/examples/roles/simple-query-hash.rkt +++ b/racket/typed/examples/simple-query-hash.rkt @@ -1,4 +1,4 @@ -#lang typed/syndicate/roles +#lang typed/syndicate ;; Expected Output ;; adding key2 -> 88 diff --git a/racket/typed/examples/roles/simple-query-set.rkt b/racket/typed/examples/simple-query-set.rkt similarity index 94% rename from racket/typed/examples/roles/simple-query-set.rkt rename to racket/typed/examples/simple-query-set.rkt index 8ee7f38..d48f6cd 100644 --- a/racket/typed/examples/roles/simple-query-set.rkt +++ b/racket/typed/examples/simple-query-set.rkt @@ -1,4 +1,4 @@ -#lang typed/syndicate/roles +#lang typed/syndicate ;; Expected Output ;; size: 0 diff --git a/racket/typed/examples/roles/simple-query-value.rkt b/racket/typed/examples/simple-query-value.rkt similarity index 94% rename from racket/typed/examples/roles/simple-query-value.rkt rename to racket/typed/examples/simple-query-value.rkt index bd1f0ad..5c97a64 100644 --- a/racket/typed/examples/roles/simple-query-value.rkt +++ b/racket/typed/examples/simple-query-value.rkt @@ -1,4 +1,4 @@ -#lang typed/syndicate/roles +#lang typed/syndicate ;; Expected Output ;; query: 0 diff --git a/racket/typed/examples/roles/simple-stop-facet.rkt b/racket/typed/examples/simple-stop-facet.rkt similarity index 96% rename from racket/typed/examples/roles/simple-stop-facet.rkt rename to racket/typed/examples/simple-stop-facet.rkt index f771442..15da21d 100644 --- a/racket/typed/examples/roles/simple-stop-facet.rkt +++ b/racket/typed/examples/simple-stop-facet.rkt @@ -1,4 +1,4 @@ -#lang typed/syndicate/roles +#lang typed/syndicate ;; Expected Output: ;; +42 diff --git a/racket/typed/examples/roles/struct-out/client.rkt b/racket/typed/examples/struct-out/client.rkt similarity index 100% rename from racket/typed/examples/roles/struct-out/client.rkt rename to racket/typed/examples/struct-out/client.rkt diff --git a/racket/typed/examples/roles/struct-out/struct-in.rkt b/racket/typed/examples/struct-out/struct-in.rkt similarity index 100% rename from racket/typed/examples/roles/struct-out/struct-in.rkt rename to racket/typed/examples/struct-out/struct-in.rkt diff --git a/racket/typed/examples/roles/struct-out/struct-out.rkt b/racket/typed/examples/struct-out/struct-out.rkt similarity index 100% rename from racket/typed/examples/roles/struct-out/struct-out.rkt rename to racket/typed/examples/struct-out/struct-out.rkt diff --git a/racket/typed/examples/roles/struct-out/typed-out.rkt b/racket/typed/examples/struct-out/typed-out.rkt similarity index 100% rename from racket/typed/examples/roles/struct-out/typed-out.rkt rename to racket/typed/examples/struct-out/typed-out.rkt diff --git a/racket/typed/examples/roles/struct-out/untyped.rkt b/racket/typed/examples/struct-out/untyped.rkt similarity index 100% rename from racket/typed/examples/roles/struct-out/untyped.rkt rename to racket/typed/examples/struct-out/untyped.rkt diff --git a/racket/typed/examples/two-buyer-protocol.rkt b/racket/typed/examples/two-buyer-protocol.rkt index 7143182..525fc38 100644 --- a/racket/typed/examples/two-buyer-protocol.rkt +++ b/racket/typed/examples/two-buyer-protocol.rkt @@ -20,14 +20,14 @@ (define-constructor (quote title answer) #:type-constructor QuoteT #:with Quote (QuoteT String QuoteAnswer) - #:with QuoteRequest (Observe (QuoteT String ★)) - #:with QuoteInterest (Observe (QuoteT ★ ★))) + #:with QuoteRequest (Observe (QuoteT String ★/t)) + #:with QuoteInterest (Observe (QuoteT ★/t ★/t))) (define-constructor (split-proposal title price contribution accepted) #:type-constructor SplitProposalT #:with SplitProposal (SplitProposalT String Int Int Bool) - #:with SplitRequest (Observe (SplitProposalT String Int Int ★)) - #:with SplitInterest (Observe (SplitProposalT ★ ★ ★ ★))) + #:with SplitRequest (Observe (SplitProposalT String Int Int ★/t)) + #:with SplitInterest (Observe (SplitProposalT ★/t ★/t ★/t ★/t))) (define-constructor (order-id id) #:type-constructor OrderIdT @@ -40,11 +40,11 @@ (define-type-alias (Maybe t) (U t Bool)) -(define-constructor (order title price id delivery-date) +(define-constructor (order title price oid delivery-date) #:type-constructor OrderT #:with Order (OrderT String Int (Maybe OrderId) (Maybe DeliveryDate)) - #:with OrderRequest (Observe (OrderT String Int ★ ★)) - #:with OrderInterest (Observe (OrderT ★ ★ ★ ★))) + #:with OrderRequest (Observe (OrderT String Int ★/t ★/t)) + #:with OrderInterest (Observe (OrderT ★/t ★/t ★/t ★/t))) (define-type-alias ds-type (U ;; quotes @@ -60,88 +60,104 @@ OrderRequest (Observe OrderInterest))) -(dataspace ds-type +(define-type-alias seller-role + (Role (seller) + (During (Observe (QuoteT String ★/t)) + (Shares (QuoteT String QuoteAnswer))) + #;(Reacts (Asserted (Observe (QuoteT String ★/t))) + (Role (_) + ;; QuoteAnswer was originally, erroneously, Int + (Shares (QuoteT String QuoteAnswer)))))) + +(run-ground-dataspace ds-type ;; seller (spawn ds-type - (facet _ - (fields [book (Tuple String Int) (tuple "Catch 22" 22)] - [next-order-id Int 10001483]) - (on (asserted (observe (quote (bind title String) discard))) - (facet x - (fields) - (on (retracted (observe (quote title discard))) - (stop x (begin))) - (match title - ["Catch 22" - (assert (quote title (price 22)))] - [discard - (assert (quote title (out-of-stock)))]))) - (on (asserted (observe (order (bind title String) (bind offer Int) discard discard))) - (facet x - (fields) - (on (retracted (observe (order title offer discard discard))) - (stop x (begin))) - (let [asking-price 22] - (if (and (equal? title "Catch 22") (>= offer asking-price)) - (let [id (ref next-order-id)] - (begin (set! next-order-id (+ 1 id)) - (assert (order title offer (order-id id) (delivery-date "March 9th"))))) - (assert (order title offer #f #f)))))))) + (lift+define-role seller-impl + (start-facet _ ;; #:implements seller-role + (field [book (Tuple String Int) (tuple "Catch 22" 22)] + [next-order-id Int 10001483]) + (on (asserted (observe (quote (bind title String) discard))) + (start-facet x + (on (retracted (observe (quote title discard))) + (stop x)) + (define answer + (match title + ["Catch 22" + (price 22)] + [_ + (out-of-stock)])) + (assert (quote title answer)))) + (on (asserted (observe (order (bind title String) (bind offer Int) discard discard))) + (start-facet x + (on (retracted (observe (order title offer discard discard))) + (stop x)) + (let ([asking-price 22]) + (if (and (equal? title "Catch 22") (>= offer asking-price)) + (let ([id (ref next-order-id)]) + (set! next-order-id (+ 1 id)) + (assert (order title offer (order-id id) (delivery-date "March 9th")))) + (assert (order title offer #f #f))))))))) ;; buyer A (spawn ds-type - (facet buyer - (fields [title String "Catch 22"] - [budget Int 1000]) - (on (asserted (quote (ref title) (bind answer QuoteAnswer))) - (match answer - [(out-of-stock) - (stop buyer (begin))] - [(price (bind amount Int)) - (facet negotiation - (fields [contribution Int (/ amount 2)]) - (on (asserted (split-proposal (ref title) amount (ref contribution) (bind accept? Bool))) - (if accept? - (stop buyer (begin)) - (if (> (ref contribution) (- amount 5)) - (stop negotiation (displayln "negotiation failed")) - (set! contribution - (+ (ref contribution) (/ (- amount (ref contribution)) 2)))))))])))) + (lift+define-role buyer-a-impl + (start-facet buyer + (field [title String "Catch 22"] + [budget Int 1000]) + (on (asserted (quote (ref title) (bind answer QuoteAnswer))) + (match answer + [(out-of-stock) + (stop buyer)] + [(price (bind amount Int)) + (start-facet negotiation + (field [contribution Int (/ amount 2)]) + (on (asserted (split-proposal (ref title) amount (ref contribution) (bind accept? Bool))) + (if accept? + (stop buyer) + (if (> (ref contribution) (- amount 5)) + (stop negotiation (displayln "negotiation failed")) + (set! contribution + (+ (ref contribution) (/ (- amount (ref contribution)) 2)))))))]))))) ;; buyer B (spawn ds-type - (facet buyer-b - (fields [funds Int 5]) - (on (asserted (observe (split-proposal (bind title String) (bind price Int) (bind their-contribution Int) discard))) - (let [my-contribution (- price their-contribution)] - (cond - [(> my-contribution (ref funds)) - (facet decline - (fields) - (assert (split-proposal title price their-contribution #f)) - (on (retracted (observe (split-proposal title price their-contribution discard))) - (stop decline (begin))))] - [#t - (facet accept - (fields) - (assert (split-proposal title price their-contribution #t)) - (on (retracted (observe (split-proposal title price their-contribution discard))) - (stop accept (begin))) - (on start - (spawn ds-type - (facet purchase - (fields) - (on (asserted (order title price (bind order-id? (Maybe OrderId)) (bind delivery-date? (Maybe DeliveryDate)))) - (match (tuple order-id? delivery-date?) - [(tuple (order-id (bind id Int)) (delivery-date (bind date String))) - ;; complete! - (begin (displayln "Completed Order:") - (displayln title) - (displayln id) - (displayln date) - (stop purchase (begin)))] - [discard - (begin (displayln "Order Rejected") - (stop purchase (begin)))]))))))]))))) -) \ No newline at end of file + (lift+define-role buyer-b-impl + (start-facet buyer-b + (field [funds Int 5]) + (on (asserted (observe (split-proposal (bind title String) (bind price Int) (bind their-contribution Int) discard))) + (let ([my-contribution (- price their-contribution)]) + (cond + [(> my-contribution (ref funds)) + (start-facet decline + (assert (split-proposal title price their-contribution #f)) + (on (retracted (observe (split-proposal title price their-contribution discard))) + (stop decline)))] + [#t + (start-facet accept + (assert (split-proposal title price their-contribution #t)) + (on (retracted (observe (split-proposal title price their-contribution discard))) + (stop accept)) + (on start + (spawn ds-type + (start-facet purchase + (on (asserted (order title price (bind order-id? (Maybe OrderId)) (bind delivery-date? (Maybe DeliveryDate)))) + (match (tuple order-id? delivery-date?) + [(tuple (order-id (bind id Int)) (delivery-date (bind date String))) + ;; complete! + (begin (displayln "Completed Order:") + (displayln title) + (displayln id) + (displayln date) + (stop purchase))] + [discard + (begin (displayln "Order Rejected") + (stop purchase))]))))))])))))) +) + +(module+ test + (check-simulates seller-impl seller-impl) + ;; found a bug in spec, see seller-role above + (check-simulates seller-impl seller-role) + (check-simulates buyer-a-impl buyer-a-impl) + (check-simulates buyer-b-impl buyer-b-impl)) diff --git a/racket/typed/main.rkt b/racket/typed/syndicate/first-facet-lang-attempt.rkt similarity index 100% rename from racket/typed/main.rkt rename to racket/typed/syndicate/first-facet-lang-attempt.rkt diff --git a/racket/typed/syndicate/lang/reader.rkt b/racket/typed/syndicate/lang/reader.rkt index 8205c5d..0411511 100644 --- a/racket/typed/syndicate/lang/reader.rkt +++ b/racket/typed/syndicate/lang/reader.rkt @@ -1,2 +1,2 @@ #lang s-exp syntax/module-reader -typed/main +typed/syndicate/roles diff --git a/racket/typed/tests/basic-bad-assertion.rkt b/racket/typed/tests/basic-bad-assertion.rkt index a817088..6e23c50 100644 --- a/racket/typed/tests/basic-bad-assertion.rkt +++ b/racket/typed/tests/basic-bad-assertion.rkt @@ -1,4 +1,4 @@ -#lang typed/syndicate/roles +#lang typed/syndicate (require rackunit/turnstile) diff --git a/racket/typed/tests/comm-ty-composition.rkt b/racket/typed/tests/comm-ty-composition.rkt index e10d633..cbcbeab 100644 --- a/racket/typed/tests/comm-ty-composition.rkt +++ b/racket/typed/tests/comm-ty-composition.rkt @@ -1,4 +1,4 @@ -#lang typed/syndicate/roles +#lang typed/syndicate (assertion-struct ping : Ping (v)) (assertion-struct pong : Pong (v)) diff --git a/racket/typed/tests/define-dataflow.rkt b/racket/typed/tests/define-dataflow.rkt index 2947bb8..08908af 100644 --- a/racket/typed/tests/define-dataflow.rkt +++ b/racket/typed/tests/define-dataflow.rkt @@ -1,4 +1,4 @@ -#lang typed/syndicate/roles +#lang typed/syndicate (run-ground-dataspace (U) (spawn (U) diff --git a/racket/typed/tests/effect-polymorhpism.rkt b/racket/typed/tests/effect-polymorhpism.rkt index 7223291..33b4c9c 100644 --- a/racket/typed/tests/effect-polymorhpism.rkt +++ b/racket/typed/tests/effect-polymorhpism.rkt @@ -1,4 +1,4 @@ -#lang typed/syndicate/roles +#lang typed/syndicate (require rackunit/turnstile) diff --git a/racket/typed/tests/expressions.rkt b/racket/typed/tests/expressions.rkt index dcec5bd..93e11d0 100644 --- a/racket/typed/tests/expressions.rkt +++ b/racket/typed/tests/expressions.rkt @@ -1,4 +1,4 @@ -#lang typed/syndicate/roles +#lang typed/syndicate (require rackunit/turnstile) diff --git a/racket/typed/tests/floating-define.rkt b/racket/typed/tests/floating-define.rkt index e93a5d9..8ce0f95 100644 --- a/racket/typed/tests/floating-define.rkt +++ b/racket/typed/tests/floating-define.rkt @@ -1,4 +1,4 @@ -#lang typed/syndicate/roles +#lang typed/syndicate (require rackunit/turnstile) diff --git a/racket/typed/tests/for-loop-regression.rkt b/racket/typed/tests/for-loop-regression.rkt index 3a29747..fb56756 100644 --- a/racket/typed/tests/for-loop-regression.rkt +++ b/racket/typed/tests/for-loop-regression.rkt @@ -1,4 +1,4 @@ -#lang typed/syndicate/roles +#lang typed/syndicate (require rackunit/turnstile) diff --git a/racket/typed/tests/for-loops.rkt b/racket/typed/tests/for-loops.rkt index 0096cb2..2d630c0 100644 --- a/racket/typed/tests/for-loops.rkt +++ b/racket/typed/tests/for-loops.rkt @@ -1,4 +1,4 @@ -#lang typed/syndicate/roles +#lang typed/syndicate (require rackunit/turnstile) diff --git a/racket/typed/tests/hashes.rkt b/racket/typed/tests/hashes.rkt index d2c4571..cf5db55 100644 --- a/racket/typed/tests/hashes.rkt +++ b/racket/typed/tests/hashes.rkt @@ -1,4 +1,4 @@ -#lang typed/syndicate/roles +#lang typed/syndicate (require rackunit/turnstile) diff --git a/racket/typed/tests/inference.rkt b/racket/typed/tests/inference.rkt index 8719c50..6a5fffd 100644 --- a/racket/typed/tests/inference.rkt +++ b/racket/typed/tests/inference.rkt @@ -1,4 +1,4 @@ -#lang typed/syndicate/roles +#lang typed/syndicate (require rackunit/turnstile) diff --git a/racket/typed/tests/pattern-annotations.rkt b/racket/typed/tests/pattern-annotations.rkt index 8eab565..e7503c8 100644 --- a/racket/typed/tests/pattern-annotations.rkt +++ b/racket/typed/tests/pattern-annotations.rkt @@ -1,4 +1,4 @@ -#lang typed/syndicate/roles +#lang typed/syndicate (require rackunit/turnstile) diff --git a/racket/typed/tests/phantom-rho.rkt b/racket/typed/tests/phantom-rho.rkt index bad4152..e18185c 100644 --- a/racket/typed/tests/phantom-rho.rkt +++ b/racket/typed/tests/phantom-rho.rkt @@ -1,4 +1,4 @@ -#lang typed/syndicate/roles +#lang typed/syndicate (require rackunit/turnstile) diff --git a/racket/typed/tests/primitives.rkt b/racket/typed/tests/primitives.rkt index 10cff18..627ea76 100644 --- a/racket/typed/tests/primitives.rkt +++ b/racket/typed/tests/primitives.rkt @@ -1,4 +1,4 @@ -#lang typed/syndicate/roles +#lang typed/syndicate (require rackunit/turnstile) diff --git a/racket/typed/tests/regression-count-new-words.rkt b/racket/typed/tests/regression-count-new-words.rkt index d1bb797..9236768 100644 --- a/racket/typed/tests/regression-count-new-words.rkt +++ b/racket/typed/tests/regression-count-new-words.rkt @@ -1,4 +1,4 @@ -#lang typed/syndicate/roles +#lang typed/syndicate (require rackunit/turnstile) diff --git a/racket/typed/tests/regression-define-with-effects.rkt b/racket/typed/tests/regression-define-with-effects.rkt index 1ac74e1..e8293a2 100644 --- a/racket/typed/tests/regression-define-with-effects.rkt +++ b/racket/typed/tests/regression-define-with-effects.rkt @@ -1,4 +1,4 @@ -#lang typed/syndicate/roles +#lang typed/syndicate (require rackunit/turnstile) diff --git a/racket/typed/tests/sequences.rkt b/racket/typed/tests/sequences.rkt index 2d093a3..324d68e 100644 --- a/racket/typed/tests/sequences.rkt +++ b/racket/typed/tests/sequences.rkt @@ -1,4 +1,4 @@ -#lang typed/syndicate/roles +#lang typed/syndicate (require rackunit/turnstile) diff --git a/racket/typed/tests/sets.rkt b/racket/typed/tests/sets.rkt index ecd89e1..1663704 100644 --- a/racket/typed/tests/sets.rkt +++ b/racket/typed/tests/sets.rkt @@ -1,4 +1,4 @@ -#lang typed/syndicate/roles +#lang typed/syndicate (require rackunit/turnstile) diff --git a/racket/typed/tests/spawn.rkt b/racket/typed/tests/spawn.rkt index 3e60b41..5a88ed4 100644 --- a/racket/typed/tests/spawn.rkt +++ b/racket/typed/tests/spawn.rkt @@ -1,4 +1,4 @@ -#lang typed/syndicate/roles +#lang typed/syndicate (require rackunit/turnstile)