Compare commits
No commits in common. "main" and "wip-typedefs" have entirely different histories.
main
...
wip-typede
|
|
@ -76,7 +76,7 @@
|
|||
(define cleaned-acts (clean-actions acts))
|
||||
(for ([act (in-list cleaned-acts)]
|
||||
#:unless (actor? act))
|
||||
(raise-argument-error 'syndicate-module "top-level actor creation action" act))
|
||||
(error "only actor creation actions allowed at module level"))
|
||||
cleaned-acts)
|
||||
|
||||
(define-syntax (syndicate-module stx)
|
||||
|
|
|
|||
|
|
@ -60,10 +60,7 @@
|
|||
(quit))]
|
||||
[_ #f]))
|
||||
|
||||
(actor (lambda (e s) (quit))
|
||||
#f
|
||||
(message (set-timer 'tick 1000 'relative)))
|
||||
|
||||
(message (set-timer 'tick 1000 'relative))
|
||||
(actor ticker
|
||||
1
|
||||
(patch-seq (sub (observe (set-timer ? ? ?)))
|
||||
|
|
|
|||
|
|
@ -13,7 +13,6 @@
|
|||
(require (for-syntax syntax/parse))
|
||||
(require rackunit)
|
||||
(require racket/engine)
|
||||
(require racket/exn)
|
||||
|
||||
(define mt-scn (scn trie-empty))
|
||||
|
||||
|
|
@ -290,7 +289,7 @@
|
|||
;; leaf behavior function
|
||||
(define (actor-behavior e s)
|
||||
(when e
|
||||
(with-handlers ([exn:fail? (lambda (e) (printf "exception: ~v\n" (exn->string e)) (quit #:exception e (list)))])
|
||||
(with-handlers ([exn:fail? (lambda (e) (eprintf "exception: ~v\n" e) (quit #:exception e (list)))])
|
||||
(match-define (actor-state π-old fts) s)
|
||||
(define-values (actions next-fts)
|
||||
(for/fold ([as '()]
|
||||
|
|
@ -546,7 +545,7 @@
|
|||
;; boot-actor : actor Γ -> Action
|
||||
(define (boot-actor a Γ)
|
||||
(with-handlers ([exn:fail? (lambda (e)
|
||||
(printf "booting actor died with: ~a\n" (exn->string e))
|
||||
(eprintf "booting actor died with: ~v\n" e)
|
||||
#f)])
|
||||
(match a
|
||||
[`(spawn ,O ...)
|
||||
|
|
|
|||
|
|
@ -210,6 +210,8 @@
|
|||
[(tuple p ...)
|
||||
#:with (([x:id τ:type] ...) ...) (stx-map pat-bindings #'(p ...))
|
||||
#'([x τ] ... ...)]
|
||||
#;[(k:kons1 p)
|
||||
(pat-bindings #'p)]
|
||||
[(~constructor-exp cons p ...)
|
||||
#:with (([x:id τ:type] ...) ...) (stx-map pat-bindings #'(p ...))
|
||||
#'([x τ] ... ...)]
|
||||
|
|
@ -263,6 +265,9 @@
|
|||
[(tuple p ...)
|
||||
(quasisyntax/loc pat
|
||||
(tuple #,@(stx-map elaborate-pattern #'(p ...))))]
|
||||
[(k:kons1 p)
|
||||
(quasisyntax/loc pat
|
||||
(k #,(elaborate-pattern #'p)))]
|
||||
[(~constructor-exp ctor p ...)
|
||||
(quasisyntax/loc pat
|
||||
(ctor #,@(stx-map elaborate-pattern #'(p ...))))]
|
||||
|
|
@ -350,6 +355,8 @@
|
|||
#:datum-literals (tuple discard bind)
|
||||
[(tuple p ...)
|
||||
#`(#,list-binding 'tuple #,@(stx-map loop #'(p ...)))]
|
||||
#;[(k:kons1 p)
|
||||
#`(#,(kons1->constructor #'k) #,(loop #'p))]
|
||||
[(bind x:id τ:type)
|
||||
(bind-id-transformer #'x)]
|
||||
[discard
|
||||
|
|
@ -387,6 +387,7 @@
|
|||
#;(define-product-type Inbound #:arity = 1)
|
||||
#;(define-product-type Outbound #:arity = 1)
|
||||
(define-container-type AssertionSet #:arity = 1)
|
||||
(define-container-type Patch #:arity = 2)
|
||||
|
||||
;; functions and type abstractions
|
||||
(define-for-syntax (resugar-∀ ty)
|
||||
|
|
@ -729,7 +730,7 @@
|
|||
;; TODO: this implementation shares a lot with that of define-constructor
|
||||
(define-syntax (require-struct stx)
|
||||
(syntax-parse stx
|
||||
[(_ ucons:id #:as ty-cons:id #:from lib (~optional (~and omit-accs #:omit-accs)))
|
||||
[(_ ucons:id #:as ty-cons:id #:from lib)
|
||||
(with-syntax* ([TypeCons #'ty-cons]
|
||||
[MakeTypeCons (format-id #'TypeCons "make-~a" #'TypeCons)]
|
||||
[GetTypeParams (format-id #'TypeCons "get-~a-type-params" #'TypeCons)]
|
||||
|
|
@ -750,6 +751,7 @@
|
|||
(raise-syntax-error #f "number of slots must be exact" #'#,stx #'ucons))
|
||||
(unless (boolean? sup)
|
||||
(raise-syntax-error #f "structs with super-type not supported" #'#,stx #'ucons))
|
||||
(define accs (cleanup-accs #'ucons accs/rev))
|
||||
(define arity (length accs/rev))
|
||||
)
|
||||
(define-for-syntax (TypeConsExtraInfo stx)
|
||||
|
|
@ -765,14 +767,10 @@
|
|||
(define-syntax GetTypeParams (mk-type-params-fetcher #'TypeCons))
|
||||
(define-syntax Cons- (mk-constructor-type-rule arity #'orig-struct-info #'TypeCons))
|
||||
(define-syntax ucons
|
||||
(user-ctor #'Cons- #'orig-struct-info 'type-tag #'TypeCons (cleanup-accs #'ucons accs/rev)))
|
||||
#,(unless (attribute omit-accs)
|
||||
(quasisyntax/loc stx
|
||||
(begin-
|
||||
(define-syntax mk-struct-accs
|
||||
(define-struct-accs accs/rev #'TypeCons #'lib))
|
||||
(mk-struct-accs ucons))))
|
||||
)))]))
|
||||
(user-ctor #'Cons- #'orig-struct-info 'type-tag #'TypeCons (cleanup-accs #'ucons accs/rev) #;accs))
|
||||
(define-syntax mk-struct-accs
|
||||
(define-struct-accs accs/rev #'TypeCons #'lib))
|
||||
(mk-struct-accs ucons))))]))
|
||||
|
||||
(begin-for-syntax
|
||||
(define-syntax ~constructor-extra-info
|
||||
|
|
@ -840,32 +838,21 @@
|
|||
;; Require & Provide
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
|
||||
(begin-for-syntax
|
||||
(define-syntax-class opaque-require-clause
|
||||
#:datum-literals (= > >=)
|
||||
#:attributes (type-definition)
|
||||
(pattern [#:opaque ty-name:id]
|
||||
#:attr type-definition #'(define-base-type ty-name))
|
||||
(pattern [#:opaque ty-name:id #:arity (~and op (~or* = > >=)) arity:nat]
|
||||
#:attr type-definition #'(define-product-type ty-name #:arity op arity))))
|
||||
|
||||
;; Import and ascribe a type from an untyped module
|
||||
;; TODO: this is where contracts would need to go
|
||||
(define-syntax (require/typed stx)
|
||||
(syntax-parse stx
|
||||
#:datum-literals (:)
|
||||
[(_ lib
|
||||
(~alt [name:id : ty]
|
||||
opaque-clause:opaque-require-clause)
|
||||
...)
|
||||
[(_ lib [name:id : ty:type] ...)
|
||||
#:with (name- ...) (format-ids "~a-" #'(name ...))
|
||||
#:with (serialized-ty ...) (for/list ([t (in-syntax #'(ty.norm ...))])
|
||||
(serialize-syntax t))
|
||||
(syntax/loc stx
|
||||
(begin-
|
||||
opaque-clause.type-definition ...
|
||||
(require (only-in lib [name name-] ...))
|
||||
(define-syntax name
|
||||
(make-variable-like-transformer
|
||||
(add-orig (assign-type #'name- (deserialize-syntax (serialize-syntax (type-eval #'ty)))
|
||||
(add-orig (assign-type #'name- (deserialize-syntax #'serialized-ty)
|
||||
#:wrap? #f) #'name)))
|
||||
...))]))
|
||||
|
||||
|
|
@ -921,6 +908,33 @@
|
|||
(require-struct outbound #:as Outbound #:from syndicate/protocol/standard-relay)
|
||||
(require-struct message #:as Message #:from syndicate/core)
|
||||
|
||||
(begin-for-syntax
|
||||
|
||||
;; constructors with arity one
|
||||
(define-syntax-class kons1
|
||||
(pattern (~or (~datum observe)
|
||||
(~datum inbound)
|
||||
(~datum outbound)
|
||||
(~datum message))))
|
||||
|
||||
(define (kons1->constructor stx)
|
||||
(syntax-parse stx
|
||||
#:datum-literals (observe inbound outbound)
|
||||
[observe #'syndicate:observe]
|
||||
[inbound #'syndicate:inbound]
|
||||
[outbound #'syndicate:outbound]
|
||||
[message #'syndicate:message]))
|
||||
|
||||
(define-syntax-class basic-val
|
||||
(pattern (~or boolean
|
||||
integer
|
||||
string)))
|
||||
|
||||
(define-syntax-class prim-op
|
||||
(pattern (~or (~literal +)
|
||||
(~literal -)
|
||||
(~literal displayln)))))
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;; Utilities Over Types
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
|
|
@ -1098,13 +1112,6 @@
|
|||
(reassemble-type #'τ-cons subitems)]
|
||||
[_ t]))
|
||||
|
||||
;; Type -> Bool
|
||||
;; to prevent observing the linkage assertions used by during/spawn,
|
||||
;; disallow ?★ and ??★
|
||||
(define-for-syntax (allowed-interest? t)
|
||||
(not (or (<: (type-eval #'(Observe ★/t)) t)
|
||||
(<: (type-eval #'(Observe (Observe ★/t))) t))))
|
||||
|
||||
;; Type -> String
|
||||
(define-for-syntax (type->strX ty)
|
||||
;; Identifier -> String
|
||||
|
|
@ -1554,6 +1561,7 @@
|
|||
(make-variable-like-transformer (add-orig (attach #'x- ': (deserialize-syntax #'serialized-τ)) #'x)))
|
||||
(define- x- e))]))
|
||||
|
||||
;; copied from ext-stlc
|
||||
(define-typed-syntax define
|
||||
[(_ x:id (~datum :) τ:type e:expr) ≫
|
||||
#:cut
|
||||
|
|
@ -19,8 +19,13 @@
|
|||
(U (Left A)
|
||||
(Right B)))
|
||||
|
||||
(define (∀ (X) (f [x : X] -> X))
|
||||
x)
|
||||
|
||||
|
||||
(define (∀ (X Y Z) (partition/either [xs : (List X)]
|
||||
[pred : (→fn X (Either Y Z))]
|
||||
[pred : (→fn X (U (Left Y)
|
||||
(Right Z)))]
|
||||
-> (Tuple (List Y) (List Z))))
|
||||
(for/fold ([lefts (List Y) (list)]
|
||||
[rights (List Z) (list)])
|
||||
|
|
@ -0,0 +1,27 @@
|
|||
#lang typed/syndicate
|
||||
|
||||
(define-type-alias ds-type
|
||||
(U (Observe (Tuple String ★)) (Tuple String Int)))
|
||||
|
||||
(dataspace ds-type
|
||||
|
||||
(spawn ds-type
|
||||
(facet _
|
||||
(fields [the-thing Int 0])
|
||||
(assert (tuple "the thing" (ref the-thing)))
|
||||
(on (asserted (tuple "set thing" (bind new-v Int)))
|
||||
(set! the-thing new-v))))
|
||||
|
||||
(spawn ds-type
|
||||
(let [k (λ [10 (begin)]
|
||||
[(bind x Int)
|
||||
(facet _ (fields)
|
||||
(assert (tuple "set thing" (+ x 1))))])]
|
||||
(facet _ (fields)
|
||||
(on (asserted (tuple "the thing" (bind x Int)))
|
||||
(k x)))))
|
||||
|
||||
(spawn ds-type
|
||||
(facet _ (fields)
|
||||
(on (asserted (tuple "the thing" (bind t Int)))
|
||||
(displayln t)))))
|
||||
|
|
@ -1,19 +1,14 @@
|
|||
#lang typed/syndicate
|
||||
|
||||
;; Expected Output
|
||||
;; 0
|
||||
;; 70
|
||||
;; #f
|
||||
|
||||
(define-constructor (account balance)
|
||||
#:type-constructor AccountT
|
||||
#:with Account (AccountT Int)
|
||||
#:with AccountRequest (AccountT ★/t))
|
||||
#:with AccountRequest (AccountT ★))
|
||||
|
||||
(define-constructor (deposit amount)
|
||||
#:type-constructor DepositT
|
||||
#:with Deposit (DepositT Int)
|
||||
#:with DepositRequest (DepositT ★/t))
|
||||
#:with DepositRequest (DepositT ★))
|
||||
|
||||
(define-type-alias ds-type
|
||||
(U Account
|
||||
|
|
@ -23,43 +18,45 @@
|
|||
(Observe DepositRequest)
|
||||
(Observe (Observe DepositRequest))))
|
||||
|
||||
(define-type-alias account-manager-role
|
||||
(Role (account-manager)
|
||||
(Shares Account)
|
||||
(Reacts (Asserted Deposit))))
|
||||
(dataspace ds-type
|
||||
|
||||
(define-type-alias client-role
|
||||
(Role (client)
|
||||
(Reacts (Asserted Account))))
|
||||
(spawn ds-type
|
||||
(facet _
|
||||
(fields [balance Int 0])
|
||||
(assert (account (ref balance)))
|
||||
(on (asserted (deposit (bind amount Int)))
|
||||
(set! balance (+ (ref balance) amount)))))
|
||||
|
||||
(spawn ds-type
|
||||
(facet _
|
||||
(fields)
|
||||
(on (asserted (account (bind amount Int)))
|
||||
(displayln amount))))
|
||||
|
||||
(run-ground-dataspace ds-type
|
||||
(spawn ds-type
|
||||
(facet _
|
||||
(fields)
|
||||
(on (asserted (observe (deposit discard)))
|
||||
(facet _
|
||||
(fields)
|
||||
(assert (deposit 100))
|
||||
(assert (deposit -30)))))))
|
||||
|
||||
(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))))))
|
||||
#|
|
||||
;; Hello-worldish "bank account" example.
|
||||
|
||||
(spawn ds-type
|
||||
(lift+define-role obs-role
|
||||
(start-facet observer
|
||||
(on (asserted (account (bind amount Int)))
|
||||
(displayln amount)))))
|
||||
(struct account (balance) #:prefab)
|
||||
(struct deposit (amount) #:prefab)
|
||||
|
||||
(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 (field [balance 0])
|
||||
(assert (account (balance)))
|
||||
(on (message (deposit $amount))
|
||||
(balance (+ (balance) amount))))
|
||||
|
||||
(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)
|
||||
)
|
||||
(spawn (on (asserted (account $balance))
|
||||
(printf "Balance changed to ~a\n" balance)))
|
||||
|
||||
(spawn* (until (asserted (observe (deposit _))))
|
||||
(send! (deposit +100))
|
||||
(send! (deposit -30)))
|
||||
|#
|
||||
|
|
@ -1,12 +0,0 @@
|
|||
#lang racket
|
||||
|
||||
(struct egg (size day) #:transparent)
|
||||
|
||||
(provide (except-out (struct-out egg)
|
||||
egg-size
|
||||
egg-day))
|
||||
|
||||
|
||||
(struct chicken (eggs) #:transparent)
|
||||
|
||||
(provide chicken)
|
||||
|
|
@ -1,18 +0,0 @@
|
|||
#lang typed/syndicate/roles
|
||||
|
||||
(require-struct egg #:as Egg #:from "lib.rkt" #:omit-accs)
|
||||
|
||||
(define e (egg 5 "Sun"))
|
||||
|
||||
(match e
|
||||
[(egg $sz $d)
|
||||
(displayln sz)
|
||||
(displayln d)])
|
||||
|
||||
(require-struct chicken #:as Chicken #:from "lib.rkt" #:omit-accs)
|
||||
|
||||
(define c (chicken (list e e e)))
|
||||
|
||||
(match c
|
||||
[(chicken $eggs)
|
||||
(displayln eggs)])
|
||||
|
|
@ -1,5 +0,0 @@
|
|||
#lang typed/syndicate
|
||||
|
||||
(require/typed "lib.rkt" [x : Int])
|
||||
|
||||
(displayln (+ x 1))
|
||||
|
|
@ -1,8 +0,0 @@
|
|||
#lang typed/syndicate
|
||||
|
||||
(require/typed "lib.rkt"
|
||||
[#:opaque Vec #:arity = 3]
|
||||
[ones : (Vec Int Int Int)]
|
||||
[vec+ : (→fn (Vec Int Int Int) (Vec Int Int Int) (Vec Int Int Int))])
|
||||
|
||||
(vec+ ones ones)
|
||||
|
|
@ -1,8 +0,0 @@
|
|||
#lang typed/syndicate
|
||||
|
||||
(require/typed "lib.rkt"
|
||||
[#:opaque Vec]
|
||||
[ones : Vec]
|
||||
[vec+ : (→fn Vec Vec Vec)])
|
||||
|
||||
(vec+ ones ones)
|
||||
|
|
@ -1,13 +0,0 @@
|
|||
#lang racket
|
||||
|
||||
(provide ones
|
||||
vec+)
|
||||
|
||||
(struct vec (x y z) #:transparent)
|
||||
|
||||
(define ones (vec 1 1 1))
|
||||
|
||||
(define (vec+ v1 v2)
|
||||
(vec (+ (vec-x v1) (vec-x v2))
|
||||
(+ (vec-y v1) (vec-y v2))
|
||||
(+ (vec-z v1) (vec-z v2))))
|
||||
|
|
@ -1,5 +0,0 @@
|
|||
#lang typed/syndicate
|
||||
|
||||
(require "provides.rkt")
|
||||
|
||||
(a-fun 5)
|
||||
|
|
@ -0,0 +1,65 @@
|
|||
#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)
|
||||
)
|
||||
|
|
@ -1,4 +1,4 @@
|
|||
#lang typed/syndicate
|
||||
#lang typed/syndicate/roles
|
||||
|
||||
;; Expected Output
|
||||
;; leader learns that there are 5 copies of The Wind in the Willows
|
||||
|
|
@ -1,4 +1,4 @@
|
|||
#lang typed/syndicate
|
||||
#lang typed/syndicate/roles
|
||||
|
||||
;; adapted from section 8.3 of Tony's dissertation
|
||||
|
||||
|
|
@ -1,6 +1,6 @@
|
|||
#lang typed/syndicate
|
||||
#lang typed/syndicate/roles
|
||||
|
||||
(require typed/syndicate/drivers/tcp)
|
||||
(require "../../drivers/tcp.rkt")
|
||||
|
||||
;; message
|
||||
(define-constructor (speak who what)
|
||||
|
|
@ -26,7 +26,8 @@
|
|||
|
||||
(spawn chat-ds
|
||||
(start-facet chat-server
|
||||
(during/spawn (tcp-connection (bind id Symbol) (tcp-listener 5999))
|
||||
;; TODO - should be during/spawn
|
||||
(during (tcp-connection (bind id Symbol) (tcp-listener 5999))
|
||||
(assert (tcp-accepted id))
|
||||
(let ([me (gensym 'user)])
|
||||
(assert (present me))
|
||||
|
|
@ -1,4 +1,4 @@
|
|||
#lang typed/syndicate
|
||||
#lang typed/syndicate/roles
|
||||
|
||||
(define-constructor (file name content)
|
||||
#:type-constructor FileT
|
||||
|
|
@ -31,4 +31,4 @@
|
|||
(define-type-alias Writer
|
||||
(Role (writer)
|
||||
(Sends Save)
|
||||
(Sends Delete)))
|
||||
(Sends Delete)))
|
||||
|
|
@ -1,4 +1,4 @@
|
|||
#lang typed/syndicate
|
||||
#lang typed/syndicate/roles
|
||||
|
||||
;; ---------------------------------------------------------------------------------------------------
|
||||
;; 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,7 +570,3 @@ 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))
|
||||
|
|
@ -1,4 +1,4 @@
|
|||
#lang typed/syndicate
|
||||
#lang typed/syndicate/roles
|
||||
|
||||
;; Expected Output:
|
||||
#|
|
||||
|
|
@ -1,4 +1,4 @@
|
|||
#lang typed/syndicate
|
||||
#lang typed/syndicate/roles
|
||||
|
||||
;; Expected Output
|
||||
;; pong: 8339
|
||||
|
|
@ -1,8 +1,8 @@
|
|||
#lang typed/syndicate
|
||||
#lang typed/syndicate/roles
|
||||
|
||||
(provide a-fun)
|
||||
|
||||
(define (a-fun [x : Int] -> Int)
|
||||
(+ x 1))
|
||||
|
||||
#;(a-fun 5)
|
||||
#;(a-fun 5)
|
||||
|
|
@ -1,4 +1,4 @@
|
|||
#lang typed/syndicate
|
||||
#lang typed/syndicate/roles
|
||||
|
||||
;; Expected Output:
|
||||
#|
|
||||
|
|
@ -1,4 +1,4 @@
|
|||
#lang typed/syndicate
|
||||
#lang typed/syndicate/roles
|
||||
|
||||
(require-struct msg #:as Msg
|
||||
#:from "driver.rkt")
|
||||
|
|
@ -0,0 +1,5 @@
|
|||
#lang typed/syndicate/roles
|
||||
|
||||
(require/typed "lib.rkt" [x : Int])
|
||||
|
||||
(displayln (+ x 1))
|
||||
|
|
@ -0,0 +1,5 @@
|
|||
#lang typed/syndicate/roles
|
||||
|
||||
(require "provides.rkt")
|
||||
|
||||
(a-fun 5)
|
||||
|
|
@ -1,4 +1,4 @@
|
|||
#lang typed/syndicate
|
||||
#lang typed/syndicate/roles
|
||||
|
||||
;; Expected Output
|
||||
;; f: 0
|
||||
|
|
@ -1,4 +1,4 @@
|
|||
#lang typed/syndicate
|
||||
#lang typed/syndicate/roles
|
||||
|
||||
(run-ground-dataspace Int
|
||||
(spawn Int
|
||||
|
|
@ -1,4 +1,4 @@
|
|||
#lang typed/syndicate
|
||||
#lang typed/syndicate/roles
|
||||
|
||||
;; Expected Output
|
||||
;; +GO
|
||||
|
|
@ -1,4 +1,4 @@
|
|||
#lang typed/syndicate
|
||||
#lang typed/syndicate/roles
|
||||
|
||||
;; Expected Output
|
||||
;; adding key2 -> 88
|
||||
|
|
@ -1,4 +1,4 @@
|
|||
#lang typed/syndicate
|
||||
#lang typed/syndicate/roles
|
||||
|
||||
;; Expected Output
|
||||
;; size: 0
|
||||
|
|
@ -1,4 +1,4 @@
|
|||
#lang typed/syndicate
|
||||
#lang typed/syndicate/roles
|
||||
|
||||
;; Expected Output
|
||||
;; query: 0
|
||||
|
|
@ -1,4 +1,4 @@
|
|||
#lang typed/syndicate
|
||||
#lang typed/syndicate/roles
|
||||
|
||||
;; Expected Output:
|
||||
;; +42
|
||||
|
|
@ -0,0 +1,163 @@
|
|||
#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))
|
||||
|
|
@ -1,33 +0,0 @@
|
|||
#lang typed/syndicate
|
||||
|
||||
;; Expected Output
|
||||
;; +parent
|
||||
;; +GO
|
||||
;; +ready
|
||||
;; -parent
|
||||
;; -GO
|
||||
;; -ready
|
||||
|
||||
(define-type-alias ds-type
|
||||
(U (Tuple String) (Observe (Tuple ★/t))))
|
||||
|
||||
(run-ground-dataspace ds-type
|
||||
(spawn ds-type
|
||||
(start-facet parent
|
||||
(assert (tuple "parent"))
|
||||
(during/spawn (tuple "GO")
|
||||
(assert (tuple "ready")))
|
||||
(on (asserted (tuple "ready"))
|
||||
(stop parent))))
|
||||
(spawn ds-type
|
||||
(start-facet flag
|
||||
(assert (tuple "GO"))
|
||||
(on (retracted (tuple "parent"))
|
||||
(stop flag))))
|
||||
(spawn ds-type
|
||||
(start-facet obs
|
||||
(during (tuple (bind s String))
|
||||
(on start
|
||||
(printf "+~a\n" s))
|
||||
(on stop
|
||||
(printf "-~a\n" s))))))
|
||||
|
|
@ -20,14 +20,14 @@
|
|||
(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)))
|
||||
#:with QuoteRequest (Observe (QuoteT String ★))
|
||||
#:with QuoteInterest (Observe (QuoteT ★ ★)))
|
||||
|
||||
(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)))
|
||||
#:with SplitRequest (Observe (SplitProposalT String Int Int ★))
|
||||
#:with SplitInterest (Observe (SplitProposalT ★ ★ ★ ★)))
|
||||
|
||||
(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 oid delivery-date)
|
||||
(define-constructor (order title price id 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)))
|
||||
#:with OrderRequest (Observe (OrderT String Int ★ ★))
|
||||
#:with OrderInterest (Observe (OrderT ★ ★ ★ ★)))
|
||||
|
||||
(define-type-alias ds-type
|
||||
(U ;; quotes
|
||||
|
|
@ -60,104 +60,88 @@
|
|||
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
|
||||
(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)))))))))
|
||||
(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))))))))
|
||||
|
||||
;; 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)))))))])))))
|
||||
(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)))))))]))))
|
||||
|
||||
;; 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))
|
||||
(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)))]))))))])))))
|
||||
)
|
||||
|
|
@ -5,7 +5,9 @@
|
|||
for/list
|
||||
for/set
|
||||
for/sum
|
||||
for/first)
|
||||
for/first
|
||||
in-hash-values
|
||||
in-hash-keys)
|
||||
|
||||
(require "core-types.rkt")
|
||||
(require "sequence.rkt")
|
||||
|
|
@ -255,3 +257,14 @@
|
|||
(⇒ ν-ep (τ-ep ...))
|
||||
(⇒ ν-s (τ-s ...))
|
||||
(⇒ ν-f (τ-f ...))])
|
||||
|
||||
|
||||
(define-typed-syntax (in-hash-values h) ≫
|
||||
[⊢ h ≫ h- (⇒ : (~Hash K V))]
|
||||
--------------------
|
||||
[⊢ (#%app- in-hash-values- h-) (⇒ : (Sequence V))])
|
||||
|
||||
(define-typed-syntax (in-hash-keys h) ≫
|
||||
[⊢ h ≫ h- (⇒ : (~Hash K V))]
|
||||
--------------------
|
||||
[⊢ (#%app- in-hash-keys- h-) (⇒ : (Sequence K))])
|
||||
|
|
@ -45,8 +45,10 @@
|
|||
#;[make-hash : (∀ (K V) (→fn (List (ConsPair K V)) (Hash K V)))]
|
||||
[hash-set : (∀ (K V) (→fn (Hash K V) K V (Hash K V)))]
|
||||
[hash-ref : (∀ (K V) (→fn (Hash K V) K V))]
|
||||
;; TODO hash-ref/failure
|
||||
[hash-has-key? : (∀ (K V) (→fn (Hash K V) K Bool))]
|
||||
[hash-update : (∀ (K V) (→fn (Hash K V) K (→fn V V) (Hash K V)))]
|
||||
;; TODO hash-update/failure
|
||||
[hash-remove : (∀ (K V) (→fn (Hash K V) K (Hash K V)))]
|
||||
[hash-map : (∀ (K V R) (→fn (Hash K V) (→fn K V R) (List R)))]
|
||||
[hash-keys : (∀ (K V) (→fn (Hash K V) (List K)))]
|
||||
|
|
@ -59,6 +61,7 @@
|
|||
|
||||
(require/typed racket/hash
|
||||
[hash-union : (∀ (K1 V1 K2 V2) (→fn (Hash K1 V1) (Hash K2 V2) (Hash (U K1 K2) (U V1 V2))))]
|
||||
;; TODO - hash-union with #:combine
|
||||
)
|
||||
|
||||
(define- (hash-ref/failure- h k err)
|
||||
|
|
@ -1,12 +1,8 @@
|
|||
#lang info
|
||||
|
||||
(define scribblings '(("scribblings/typed-syndicate.scrbl" ())))
|
||||
|
||||
(define compile-omit-paths
|
||||
'("examples"
|
||||
"tests"))
|
||||
|
||||
(define test-omit-paths
|
||||
;; a number of the examples use SPIN for model checking which I need
|
||||
;; to figure out how to get working on the package server
|
||||
'("examples/"))
|
||||
'("examples/roles/chat-tcp2.rkt"))
|
||||
|
|
|
|||
|
|
@ -3,14 +3,12 @@
|
|||
(provide List
|
||||
(for-syntax ~List)
|
||||
list
|
||||
(typed-out [[empty- : (List ⊥)] empty]
|
||||
[[empty?- : (∀ (X) (→fn (List X) Bool))] empty?]
|
||||
[[cons- : (∀ (X) (→fn X (List X) (List X)))] cons]
|
||||
[[cons?- : (∀ (X) (→fn X (List X) Bool))] cons?]
|
||||
(typed-out [[cons- : (∀ (X) (→fn X (List X) (List X)))] cons]
|
||||
[[first- : (∀ (X) (→fn (List X) X))] first]
|
||||
[[second- : (∀ (X) (→fn (List X) X))] second]
|
||||
[[rest- : (∀ (X) (→fn (List X) (List X)))] rest]
|
||||
[[member?- (∀ (X) (→fn X (List X) Bool))] member?]
|
||||
[[empty?- (∀ (X) (→fn (List X) Bool))] empty?]
|
||||
[[reverse- (∀ (X) (→fn (List X) (List X)))] reverse]
|
||||
[[partition- (∀ (X) (→fn (List X) (→fn X Bool) (List X)))] partition]
|
||||
[[map- (∀ (X Y) (→fn (→fn X Y) (List X) (List Y)))] map]
|
||||
|
|
@ -2890,9 +2890,7 @@
|
|||
(define jm (run/timeout (thunk (compile jmr)) 5000))
|
||||
(check-true (role-graph? jm))
|
||||
(define jmi (run/timeout (thunk (compile/internal-events jm)) 5000))
|
||||
(check-true (role-graph? jmi))
|
||||
;; TODO : times out, probably due to infinite loop
|
||||
#;(check-true (run/timeout (thunk (simulates?/rg jmi jmi)) 100000))))
|
||||
(check-true (run/timeout (thunk (simulates?/rg jmi jmi)) 5000))))
|
||||
|
||||
(define task-runner-ty
|
||||
'(Role
|
||||
|
|
@ -3027,7 +3025,7 @@
|
|||
(check-false (simulates? tm (parse-T task-performer-spec)))))
|
||||
|
||||
|
||||
#;(module+ test
|
||||
(module+ test
|
||||
(test-case
|
||||
"job manager subgraph(s) implement task assigner"
|
||||
(define jmr (run/timeout (thunk (parse-T job-manager-actual))))
|
||||
|
|
@ -12,7 +12,7 @@
|
|||
;; Start dataspace programs
|
||||
run-ground-dataspace
|
||||
;; Types
|
||||
Tuple Bind Discard → ∀ AssertionSet
|
||||
Tuple Bind Discard → ∀
|
||||
Role Reacts Shares Asserted Retracted Message OnDataflow Stop OnStart OnStop
|
||||
Know Forget Realize
|
||||
Branch Effs
|
||||
|
|
@ -21,8 +21,8 @@
|
|||
Computation Value Endpoints Roles Spawns Sends
|
||||
→fn proc
|
||||
;; Statements
|
||||
let let* if spawn dataspace start-facet set! begin block stop begin/dataflow #;unsafe-do
|
||||
when unless send! realize! define during/spawn
|
||||
let let* if spawn dataspace start-facet set! begin stop begin/dataflow #;unsafe-do
|
||||
when unless send! realize! define
|
||||
;; Derived Forms
|
||||
during During
|
||||
define/query-value
|
||||
|
|
@ -33,7 +33,7 @@
|
|||
;; endpoints
|
||||
assert know on field
|
||||
;; expressions
|
||||
tuple select lambda λ ref (struct-out observe) (struct-out message) (struct-out inbound) (struct-out outbound)
|
||||
tuple select lambda λ ref observe inbound outbound
|
||||
Λ inst call/inst
|
||||
;; making types
|
||||
define-type-alias
|
||||
|
|
@ -182,28 +182,8 @@
|
|||
(⇒ : ★/t)
|
||||
(⇒ ν-f (τ))]])
|
||||
|
||||
(define-typed-syntax (during/spawn pat bdy ...+) ≫
|
||||
#:with pat+ (elaborate-pattern/with-com-ty #'pat)
|
||||
[⊢ pat+ ≫ pat-- (⇒ : τp)]
|
||||
#:fail-unless (pure? #'pat--) "pattern not allowed to have effects"
|
||||
#:fail-unless (allowed-interest? (pattern-sub-type #'τp)) "overly broad interest, ?̱̱★ and ??★ not allowed"
|
||||
#:with ([x:id τ:type] ...) (pat-bindings #'pat+)
|
||||
[[x ≫ x- : τ] ... ⊢ (block bdy ...) ≫ bdy-
|
||||
(⇒ ν-ep (~effs τ-ep ...))
|
||||
(⇒ ν-f (~effs))
|
||||
(⇒ ν-s (~effs))]
|
||||
#:with pat- (substs #'(x- ...) #'(x ...) (compile-syndicate-pattern #'pat+))
|
||||
#:with τc:type (current-communication-type)
|
||||
#:with τ-facet (type-eval #'(Role (_) τ-ep ...))
|
||||
#:with τ-spawn (mk-ActorWithRole- #'(τc.norm τ-facet))
|
||||
#:with τ-endpoint (type-eval #'(Reacts (Asserted τp) τ-spawn))
|
||||
------------------------------
|
||||
[⊢ (syndicate:during/spawn pat- bdy-)
|
||||
(⇒ : ★/t)
|
||||
(⇒ ν-ep (τ-endpoint))])
|
||||
|
||||
(define-typed-syntax field
|
||||
[(_ [x:id (~optional (~datum :)) τ-f:type e:expr] ...) ≫
|
||||
[(_ [x:id τ-f:type e:expr] ...) ≫
|
||||
#:cut
|
||||
#:fail-unless (stx-andmap flat-type? #'(τ-f ...)) "keep your uppity data outta my fields"
|
||||
[⊢ e ≫ e- (⇐ : τ-f)] ...
|
||||
|
|
@ -224,7 +204,6 @@
|
|||
(define-typed-syntax (assert e:expr) ≫
|
||||
[⊢ e ≫ e- (⇒ : τ)]
|
||||
#:fail-unless (pure? #'e-) "expression not allowed to have effects"
|
||||
#:fail-unless (allowed-interest? #'τ) "overly broad interest, ?̱̱★ and ??★ not allowed"
|
||||
#:with τs (mk-Shares- #'(τ))
|
||||
-------------------------------------
|
||||
[⊢ (syndicate:assert e-) (⇒ : ★/t)
|
||||
|
|
@ -336,7 +315,6 @@
|
|||
#:with p/e (if msg? (stx-cadr elab) elab)
|
||||
[⊢ p/e ≫ p-- (⇒ : τp)]
|
||||
#:fail-unless (pure? #'p--) "pattern not allowed to have effects"
|
||||
#:fail-unless (allowed-interest? (pattern-sub-type #'τp)) "overly broad interest, ?̱̱★ and ??★ not allowed"
|
||||
#:with ([x:id τ:type] ...) (pat-bindings #'p/e)
|
||||
[[x ≫ x- : τ] ... ⊢ (block s ...) ≫ s-
|
||||
(⇒ ν-ep (~effs))
|
||||
|
|
@ -457,6 +435,11 @@
|
|||
#:with inst-p (instantiate-pattern #'p+)
|
||||
#:with start-e (if (attribute k) #'know #'asserted)
|
||||
#:with stop-e (if (attribute k) #'forget #'retracted)
|
||||
#:with res #'(on (start-e p+)
|
||||
(start-facet during-inner
|
||||
(on (stop-e inst-p)
|
||||
(stop during-inner))
|
||||
s ...))
|
||||
----------------------------------------
|
||||
[≻ (on (start-e p+)
|
||||
(start-facet during-inner
|
||||
|
|
@ -482,6 +465,8 @@
|
|||
#:datum-literals (tuple discard bind)
|
||||
[(tuple p ...)
|
||||
#`(tuple #,@(stx-map loop #'(p ...)))]
|
||||
[(k:kons1 p)
|
||||
#`(k #,(loop #'p))]
|
||||
[(bind x:id τ)
|
||||
#'x]
|
||||
;; not sure about this
|
||||
|
|
@ -1,776 +0,0 @@
|
|||
#lang scribble/manual
|
||||
|
||||
@(require (for-label (only-in racket struct)
|
||||
typed/syndicate/roles)
|
||||
(prefix-in racket: (for-label racket))
|
||||
(prefix-in untyped: (for-label syndicate/actor)))
|
||||
|
||||
@title{Typed Syndicate}
|
||||
|
||||
|
||||
@defmodule[typed/syndicate/roles]
|
||||
|
||||
@section{Overview}
|
||||
|
||||
@section{Types}
|
||||
|
||||
@deftogether[(@defidform[Int]
|
||||
@defidform[Bool]
|
||||
@defidform[String]
|
||||
@defidform[ByteString]
|
||||
@defidform[Symbol])]{
|
||||
Base types.
|
||||
}
|
||||
|
||||
@defform[(U type ...)]{
|
||||
The type representing the union of @racket[type ...].
|
||||
}
|
||||
|
||||
@defidform[⊥]{
|
||||
An alias for @racket[(U)].
|
||||
}
|
||||
|
||||
@defidform[★/t]{
|
||||
The type representing any possible assertion, and, in an @racket[AssertionSet],
|
||||
the possibility for an infinite set of assertions.
|
||||
}
|
||||
|
||||
@defidform[Discard]{
|
||||
The type of @racket[_] patterns.
|
||||
}
|
||||
|
||||
@defform[(Bind type)]{
|
||||
The type of @racket[$] patterns.
|
||||
}
|
||||
|
||||
@defidform[FacetName]{
|
||||
The type associated with identifiers bound by @racket[start-facet].
|
||||
}
|
||||
|
||||
@defform[(Role (x) type ...)]{
|
||||
The type of a facet named @racket[x] and endpoints described by @racket[type
|
||||
...].
|
||||
}
|
||||
|
||||
@defform[(Stop X type ...)]{
|
||||
The type of a @racket[stop] action.
|
||||
}
|
||||
|
||||
@defform[(Field type)]{
|
||||
The type of a field containing values of @racket[type].
|
||||
}
|
||||
|
||||
|
||||
@defform[(Shares type)]{
|
||||
The type of an @racket[assert] endpoint.
|
||||
}
|
||||
|
||||
@defform[#:literals (OnStart OnStop Asserted Retracted)
|
||||
(Reacts EventDesc type ...)
|
||||
#:grammar
|
||||
[(EventDesc (code:line OnStart)
|
||||
(code:line OnStart)
|
||||
(code:line (Asserted event-type))
|
||||
(code:line (Retracted event-type)))]]{
|
||||
The type of a @racket[on] endpoint that reacts to events described by
|
||||
@racket[EventDesc] with the behavior given by @racket[type ...].
|
||||
}
|
||||
|
||||
@deftogether[(@defidform[OnStart]
|
||||
@defidform[OnStop]
|
||||
@defform[(Asserted type)]
|
||||
@defform[(Retracted type)])]{
|
||||
See @racket[Reacts].
|
||||
}
|
||||
|
||||
@defform[(Actor type)]{
|
||||
The type of an actor that operates in a dataspace with a certain communication
|
||||
@racket[type].
|
||||
}
|
||||
|
||||
@defform[(ActorWithRole comm-type behavior-type)]{
|
||||
An @racket[Actor] type with the additional @racket[behavior-type] describing the
|
||||
actor's behavior in terms of a @racket[Role].
|
||||
}
|
||||
|
||||
@defform[(Sends type)]{
|
||||
The type of a @racket[send!] action.
|
||||
}
|
||||
|
||||
@defform[(Realize type)]{
|
||||
The type of a @racket[realize!] action.
|
||||
}
|
||||
|
||||
@deftogether[(@defform[(Branch type ...)]
|
||||
@defform[(Effs type ...)])]{
|
||||
Types that may arise in descriptions in @racket[Role] types due to branching and
|
||||
sequencing.
|
||||
}
|
||||
|
||||
@defform[(Tuple type ...)]{
|
||||
The type of @racket[tuple] expressions.
|
||||
}
|
||||
|
||||
@defidform[Unit]{
|
||||
An alias for @racket[(Tuple)].
|
||||
}
|
||||
|
||||
@defform[(AssertionSet type)]{
|
||||
The type for a set of assertions of a certain @racket[type]. Note that these are
|
||||
not interoperable with the general purpose @racket[set] data structures.
|
||||
}
|
||||
|
||||
@defform[(∀ (X ...) type)]{
|
||||
Universal quantification over types.
|
||||
}
|
||||
|
||||
@defform[#:literals (Computation Value Endpoints Roles Spawns)
|
||||
(→ type ... (Computation (Value result-type)
|
||||
(Endpoints ep-type ...)
|
||||
(Roles role-type ...)
|
||||
(Spawns spawn-type ...)))]{
|
||||
The type of a function with parameters @racket[type ...] that returns @racket[result-type]. The type includes the effects of any actions performed by the function:
|
||||
@itemlist[
|
||||
@item{@racket[Endpoints]: includes any endpoint installation effects, such as from @racket[assert] and @racket[on].}
|
||||
@item{@racket[Roles]: includes any script action effects, such as from @racket[start-facet], @racket[stop], and @racket[send!].}
|
||||
@item{@racket[Spawns]: includes descriptions of any @racket[spawn] actions.}
|
||||
]
|
||||
}
|
||||
|
||||
@defform[(→fn type-in ... type-out)]{
|
||||
Shorthand for a @racket[→] type with no effects.
|
||||
}
|
||||
|
||||
@defform[(proc maybe-quantifiers type-in ... maybe-arrow type-out
|
||||
maybe-endpoints
|
||||
maybe-roles
|
||||
maybe-spawns)
|
||||
#:grammar
|
||||
[(maybe-quantifiers (code:line)
|
||||
(code:line #:forall (X ...)))
|
||||
(maybe-arrow (code:line)
|
||||
(code:line →)
|
||||
(code:line ->))
|
||||
(maybe-endpoints (code:line)
|
||||
(code:line #:endpoints (e ...)))
|
||||
(maybe-roles (code:line)
|
||||
(code:line #:roles (r ...)))
|
||||
(maybe-spawns (code:line)
|
||||
(code:line #:spawns (s ...)))]]{
|
||||
A more convenient notation for writing (potentially polymorphic) function types
|
||||
with effects. Shorthand for @racket[(∀ (X ...) (→ type-in ... (Computation
|
||||
(Value type-out) (Endpoints e ...) (Roles r ...) (Spawns s ...))))].
|
||||
}
|
||||
|
||||
@deftogether[(@defform[(Computation type ...)]
|
||||
@defform[(Value type)]
|
||||
@defform[(Endpoints type)]
|
||||
@defform[(Roles type)]
|
||||
@defform[(Spawns type)])]{
|
||||
See @racket[→].
|
||||
}
|
||||
|
||||
@section{User Defined Types}
|
||||
|
||||
@defform*[[(define-type-alias id type)
|
||||
(define-type-alias (ty-cons-id arg-id ...) type)]]{
|
||||
Define @racket[id] to be the same as @racket[type], or create a type constructor
|
||||
@racket[(ty-cons-id ty ...)] whose meaning is @racket[type] with references to
|
||||
@racket[arg-id ...] replaced by @racket[ty ...].
|
||||
}
|
||||
|
||||
@defform[(define-constructor (ctor-id slot-id ...)
|
||||
maybe-type-ctor
|
||||
maybe-alias ...)
|
||||
#:grammar
|
||||
[(maybe-type-ctor (code:line)
|
||||
(code:line #:type-constructor type-ctor-id))
|
||||
(maybe-alias (code:line)
|
||||
(code:line #:with alias alias-body))]]{
|
||||
Defines a container analagous to a prefab @racket[struct]. Includes accessor
|
||||
functions for each @racket[slot-id]. (But not, presently, a predicate function).
|
||||
|
||||
When a @racket[type-ctor-id] is provided, the type of such structures is
|
||||
@racket[(type-ctor-id type ...)], where each @racket[type] describes the value
|
||||
of the corresponding slot. When not provided, the type constructor is named by
|
||||
appending @racket["/t"] to @racket[ctor-id].
|
||||
|
||||
Each @racket[alias] and @racket[alias-body] creates an instance of
|
||||
@racket[define-type-alias].
|
||||
}
|
||||
|
||||
@defform[#:literals (:)
|
||||
(define-constructor* (ctor-id : type-ctor-id slot-id ...)
|
||||
maybe-alias ...)]{
|
||||
An abbreviated form of @racket[define-constructor].
|
||||
}
|
||||
|
||||
@defform[#:literals (:)
|
||||
(assertion-struct ctor-id : type-ctor-id (slot-id ...))]{
|
||||
An abbreviated form of @racket[define-constructor].
|
||||
}
|
||||
|
||||
@defform[#:literals (:)
|
||||
(message-struct ctor-id : type-ctor-id (slot-id ...))]{
|
||||
An abbreviated form of @racket[define-constructor].
|
||||
}
|
||||
|
||||
@section{Actor Forms}
|
||||
|
||||
@defform[(run-ground-dataspace type expr ...)]{
|
||||
Starts a ground, i.e. main, dataspace of the program, with the given
|
||||
communication @racket[type] and initial actors spawned by @racket[expr ...].
|
||||
}
|
||||
|
||||
@defform[(spawn maybe-type s)
|
||||
#:grammar
|
||||
[(maybe-type (code:line)
|
||||
(code:line type))]]{
|
||||
Spawns an actor with behavior given by @racket[s]. The @racket[type] gives the
|
||||
communication type of the enclosing dataspace. When absent, @racket[type] is
|
||||
supplied by the nearest lexically enclosing @racket[spawn] or @racket[dataspace]
|
||||
form, if any exist.
|
||||
}
|
||||
|
||||
@defform[(dataspace type expr ...)]{
|
||||
Spawns a dataspace with communication type @racket[type] as a child of the
|
||||
dataspace enclosing the executing actor. The script @racket[expr ...] spawns the
|
||||
initial actors of the new dataspace.
|
||||
}
|
||||
|
||||
@defform[(start-facet id maybe-spec expr ...+)
|
||||
#:grammar
|
||||
[(maybe-spec (code:line)
|
||||
(code:line #:implements type)
|
||||
(code:line #:includes-behavior type))]]{
|
||||
Start a facet with name @racket[id] and endpoints installed through the
|
||||
evaluation of @racket[expr ...].
|
||||
}
|
||||
|
||||
@defform[(stop id expr ...)]{
|
||||
Terminate the facet @racket[id] with continuation script @racket[expr ...]. Any
|
||||
facets started by the continuation script survive the termination of facet
|
||||
@racket[id].
|
||||
}
|
||||
|
||||
@defform[#:literals (start stop message asserted retracted _ $)
|
||||
(on event-description body ...+)
|
||||
#:grammar
|
||||
[(event-description (code:line start)
|
||||
(code:line stop)
|
||||
(code:line (message pattern))
|
||||
(code:line (asserted pattern))
|
||||
(code:line (retracted pattern)))
|
||||
(pattern (code:line _)
|
||||
(code:line ($ id type))
|
||||
(code:line ($ id))
|
||||
(code:line $id)
|
||||
(code:line $id:type)
|
||||
(code:line (ctor pattern ...))
|
||||
(code:line expr))]]{
|
||||
Creates an event handler endpoint that responds to the event specified by
|
||||
@racket[event-description]. Executes the @racket[body ...] for each matching
|
||||
event, with any pattern variables bound to their matched value.
|
||||
|
||||
Patterns have the following meanings:
|
||||
@itemlist[
|
||||
@item{@racket[_] matches anything.}
|
||||
|
||||
@item{@racket[($ id type)] matches any value and binds it to @racket[id] with
|
||||
assumed type @racket[type].}
|
||||
|
||||
@item{@racket[($ id)] is like @racket[($ id type)], but attempts to use the
|
||||
current communication type to fill in the @racket[type] of potential matches.
|
||||
May raise an error if no suitable communication type is in scope.}
|
||||
|
||||
@item{@racket[(? pred pattern)] matches values where @racket[(pred val)] is not
|
||||
@racket[#f] and that match @racket[pattern].}
|
||||
|
||||
@item{@racket[$id:type] is shorthand for @racket[($ id type)].}
|
||||
|
||||
@item{@racket[$id] is shorthand for @racket[($ id)].}
|
||||
|
||||
@item{@racket[(ctor pat ...)] matches values built by applying the constructor
|
||||
@racket[ctor] to values matching @racket[pat ...]. @racket[ctor] is usually
|
||||
a @racket[struct] name.}
|
||||
|
||||
@item{@racket[expr] patterns match values that are @racket[equal?] to
|
||||
@racket[expr].}
|
||||
]
|
||||
}
|
||||
|
||||
@defform[(on-start expr ...+)]{
|
||||
Shorthand for @racket[(on start expr ...)].
|
||||
}
|
||||
|
||||
@defform[(on-stop expr ...+)]{
|
||||
Shorthand for @racket[(on stop expr ...)].
|
||||
}
|
||||
|
||||
@defform[(assert expr)]{
|
||||
Creates an assertion endpoint with the value of @racket[expr].
|
||||
}
|
||||
|
||||
@defform[(know expr)]{
|
||||
Creates an internal assertion endpoint with the value of @racket[expr].
|
||||
}
|
||||
|
||||
@defform[(send! expr)]{
|
||||
Broadcast a dataspace message with the value of @racket[expr].
|
||||
}
|
||||
|
||||
@defform[(realize! expr)]{
|
||||
Broadcast an actor-internal message with the value of @racket[expr].
|
||||
}
|
||||
|
||||
@defform[#:literals (:)
|
||||
(field [id maybe-type expr] ...)
|
||||
#:grammar
|
||||
[(maybe-type (code:line)
|
||||
(code:line type)
|
||||
(code:line : type))]]{
|
||||
Defines fields of type @racket[type] with names @racket[id] and initial values
|
||||
@racket[expr]. If @racket[type] is not provided, the type of the initial
|
||||
expression is used as the type of the field.
|
||||
}
|
||||
|
||||
@defform[(ref id)]{
|
||||
Reference the @racket[field] named @racket[id].
|
||||
}
|
||||
|
||||
@defform[(set! id expr)]{
|
||||
Update the value the @racket[field] named @racket[id].
|
||||
}
|
||||
|
||||
@defform[(begin/dataflow expr ...+)]{
|
||||
Evaluate and perform the script @racket[expr ...], and then again each time a
|
||||
field referenced by the script updates.
|
||||
}
|
||||
|
||||
@defform[(during pattern expr ...+)]{
|
||||
Engage in behavior for the duration of a matching assertion. The syntax of
|
||||
@racket[pattern] is the same as described by @racket[on].
|
||||
}
|
||||
|
||||
@defform[(during/spawn pattern expr ...+)]{
|
||||
Like @racket[during], but spawns an actor for the behavior @racket[expr ...].
|
||||
}
|
||||
|
||||
@defform[(define/query-value name absent-expr pattern expr
|
||||
maybe-on-add
|
||||
maybe-on-remove)
|
||||
#:grammar
|
||||
[(maybe-on-add (code:line)
|
||||
(code:line #:on-add on-add-expr))
|
||||
(maybe-on-remove (code:line)
|
||||
(code:line #:on-remove on-remove-expr))]]{
|
||||
Equivalent to the untyped @racket[untyped:define/query-value].
|
||||
}
|
||||
|
||||
@defform[(define/query-set name pattern expr
|
||||
maybe-on-add
|
||||
maybe-on-remove)
|
||||
#:grammar
|
||||
[(maybe-on-add (code:line)
|
||||
(code:line #:on-add on-add-expr))
|
||||
(maybe-on-remove (code:line)
|
||||
(code:line #:on-remove on-remove-expr))]]{
|
||||
Equivalent to the untyped @racket[untyped:define/query-set].
|
||||
}
|
||||
|
||||
@defform[(define/query-hash name pattern key-expr value-expr
|
||||
maybe-on-add
|
||||
maybe-on-remove)
|
||||
#:grammar
|
||||
[(maybe-on-add (code:line)
|
||||
(code:line #:on-add on-add-expr))
|
||||
(maybe-on-remove (code:line)
|
||||
(code:line #:on-remove on-remove-expr))]]{
|
||||
Equivalent to the untyped @racket[untyped:define/query-hash].
|
||||
}
|
||||
|
||||
@defform[(define/dataflow name maybe-type expr)
|
||||
#:grammar
|
||||
[(maybe-type (code:line)
|
||||
(code:line type))]]{
|
||||
Define a @racket[field] named @racket[name], whose value is reevaluated to the
|
||||
result of @racket[expr] each time any referenced field changes. When
|
||||
@racket[type] is not supplied, the field has the type of the given
|
||||
@racket[expr].
|
||||
}
|
||||
|
||||
@section{Expressions}
|
||||
|
||||
@defform*[#:literals (:)
|
||||
[(ann expr : type)
|
||||
(ann expr type)]]{
|
||||
Ensure that @racket[expr] has the given @racket[type].
|
||||
}
|
||||
|
||||
@defform[(if test-expr then-expr else-expr)]{
|
||||
The same as Racket's @racket[racket:if].
|
||||
}
|
||||
|
||||
@deftogether[(@defform[(cond [test-expr body-expr ...+] ...+)]
|
||||
@defthing[else Bool #:value #t])]{
|
||||
Like Racket's @racket[racket:cond].
|
||||
}
|
||||
|
||||
@defform[(when test-expr expr)]{
|
||||
Like Racket's @racket[racket:when], but results in @racket[#f] when
|
||||
@racket[test-expr] is @racket[#f].
|
||||
}
|
||||
|
||||
@defform[(unless test-expr expr)]{
|
||||
Like Racket's @racket[racket:unless], but results in @racket[#f] when
|
||||
@racket[test-expr] is @racket[#f].
|
||||
}
|
||||
|
||||
@defform[(let ([id expr] ...) body ...+)]{
|
||||
The same as Racket's @racket[racket:let].
|
||||
}
|
||||
|
||||
@defform[(let* ([id expr] ...) body ...+)]{
|
||||
The same as Racket's @racket[racket:let*].
|
||||
}
|
||||
|
||||
@defform[#:literals (:)
|
||||
(lambda ([x opt-: type] ...) expr ...+)
|
||||
#:grammar
|
||||
[(opt-: (code:line)
|
||||
(code:line :))]]{
|
||||
Constructsa an anonymous function.
|
||||
}
|
||||
|
||||
@defidform[λ]{Synonym for @racket[lambda].}
|
||||
|
||||
@defform[(Λ (X ...) expr)]{
|
||||
Parametric abstraction over type variables @racket[X ...].
|
||||
}
|
||||
|
||||
@defform[(inst expr type ...)]{
|
||||
Instantiates the type variables @racket[X ...] with @racket[type ...], where
|
||||
@racket[expr] has type @racket[(∀ (X ...) t)].
|
||||
}
|
||||
|
||||
@defform*[#:literals (: → -> ∀)
|
||||
[(define id : type expr)
|
||||
(define id expr)
|
||||
(define (id [arg-id opt-: arg-type] ... opt-res-ty) expr ...+)
|
||||
(define (∀ (X ...) (id [arg-id opt-: arg-type] ... opt-res-ty)) expr ...+)]
|
||||
#:grammar
|
||||
[(opt-: (code:line) (code:line :))
|
||||
(opt-res-ty (code:line)
|
||||
(code:line arr res-type))
|
||||
(arr (code:line →) (code:line ->))]]{
|
||||
Define a constant or a (potentially polymorphic) function. Note that the
|
||||
function name @racket[id] is @emph{not} bound in the body.
|
||||
}
|
||||
|
||||
@defform[(define-tuple (id ...) expr)]{
|
||||
Define @racket[id ...] to each of the slots of the tuple produced by
|
||||
@racket[expr].
|
||||
}
|
||||
|
||||
@defform[(match-define pattern expr)]{
|
||||
Define the binders of @racket[pattern] to the matching values of @racket[expr].
|
||||
}
|
||||
|
||||
@defform[(begin expr ...+)]{
|
||||
Sequencing form whose value and type is that of the final @racket[expr].
|
||||
}
|
||||
|
||||
@defform[(block expr ...+)]{
|
||||
Like @racket[begin], but also introduces a definition context for its body.
|
||||
}
|
||||
|
||||
@defform[(match expr [pattern body-expr ...+] ...+)]{
|
||||
Like Racket's @racket[racket:match] but with the pattern syntax described by
|
||||
@racket[on].
|
||||
}
|
||||
|
||||
@defform[(tuple expr ...)]{
|
||||
Constructs a tuple of arbitrary arity.
|
||||
}
|
||||
|
||||
@defform[(select i expr)]{
|
||||
Extract the @racket[i]th element of a @racket[tuple].
|
||||
}
|
||||
|
||||
@defthing[unit Unit #:value (tuple)]
|
||||
|
||||
@defform[(error format-expr arg-expr ...)]{
|
||||
Raises an exception using @racket[format-expr] as a format string together with
|
||||
@racket[arg-expr ...].
|
||||
}
|
||||
|
||||
@deftogether[(
|
||||
@defthing[+ (→fn Int Int Int)]
|
||||
@defthing[- (→fn Int Int Int)]
|
||||
@defthing[* (→fn Int Int Int)]
|
||||
@defthing[< (→fn Int Int Bool)]
|
||||
@defthing[> (→fn Int Int Bool)]
|
||||
@defthing[<= (→fn Int Int Bool)]
|
||||
@defthing[>= (→fn Int Int Bool)]
|
||||
@defthing[= (→fn Int Int Bool)]
|
||||
@defthing[even? (→fn Int Bool)]
|
||||
@defthing[odd? (→fn Int Bool)]
|
||||
@defthing[add1 (→fn Int Int)]
|
||||
@defthing[sub1 (→fn Int Int)]
|
||||
@defthing[max (→fn Int Int Int)]
|
||||
@defthing[min (→fn Int Int Int)]
|
||||
@defthing[zero? (→fn Int Bool)]
|
||||
@defthing[positive? (→fn Int Bool)]
|
||||
@defthing[negative? (→fn Int Bool)]
|
||||
@defthing[current-inexact-milleseconds? (→fn Int)]
|
||||
@defthing[string=? (→fn String String Bool)]
|
||||
@defthing[bytes->string/utf-8 (→fn ByteString String)]
|
||||
@defthing[string->bytes/utf-8 (→fn String ByteString)]
|
||||
@defthing[gensym (→fn Symbol Symbol)]
|
||||
@defthing[symbol->string (→fn Symbol String)]
|
||||
@defthing[string->symbol (→fn String Symbol)]
|
||||
@defthing[not (→fn Bool Bool)]
|
||||
@defform[(/ e1 e2)]
|
||||
@defform[(and e ...)]
|
||||
@defform[(or e ...)]
|
||||
@defform[(equal? e1 e2)]
|
||||
@defform[(displayln e)]
|
||||
@defform[(printf fmt-expr val-expr ...)]
|
||||
@defform[(~a e ...)]
|
||||
)]{
|
||||
Primitive operations imported from Racket.
|
||||
}
|
||||
|
||||
@defform[#:literals (:)
|
||||
(for/fold ([acc-id maybe-:ty acc-expr] ...+)
|
||||
(for-clause ...)
|
||||
body-expr ...+)
|
||||
#:grammar
|
||||
[(maybe-:ty (code:line)
|
||||
(code:line : acc-type))
|
||||
(for-clause (code:line [id seq-expr])
|
||||
(code:line [id : type seq-expr])
|
||||
(code:line [(k-id v-id) hash-expr])
|
||||
(code:line #:when test-expr)
|
||||
(code:line #:unless test-expr)
|
||||
(code:line #:break test-expr))]]{
|
||||
Similar to Racket's @racket[racket:for/fold].
|
||||
|
||||
When more than one @racket[acc-id] is used, the body of the loop must evaluate
|
||||
to a @racket[tuple] with one value for each accumulator, with the final tuple
|
||||
also being the result of the entire expression.
|
||||
|
||||
Each @racket[seq-expr] should be of type @racket[Sequence], though expressions
|
||||
of type @racket[List] and @racket[Set] are automatically converted.
|
||||
}
|
||||
|
||||
@deftogether[(
|
||||
@defform[(for/list (for-clause ...) body ...+)]
|
||||
@defform[(for/set (for-clause ...) body ...+)]
|
||||
@defform[(for/sum (for-clause ...) body ...+)]
|
||||
@defform[(for (for-clause ...) body ...+)]
|
||||
@defform[(for/first (for-clause ...) body ...+)]
|
||||
)]{
|
||||
Like their Racket counterparts. See @racket[for/fold] for the description of
|
||||
@racket[for-clause].
|
||||
|
||||
Unlike @racket[racket:for/first], @racket[for/first] returns a @racket[Maybe]
|
||||
value to indicate success/failure.
|
||||
}
|
||||
|
||||
@section{Require & Provide}
|
||||
|
||||
@defform[(struct-out ctor-id)]{
|
||||
}
|
||||
|
||||
@subsection{Requiring From Outside Typed Syndicate}
|
||||
|
||||
@defform[#:literals (:)
|
||||
(require/typed lib clause ...)
|
||||
#:grammar
|
||||
[(clause (code:line [id : type])
|
||||
(code:line opaque))
|
||||
(opaque (code:line [#:opaque type-name])
|
||||
(code:line [#:opaque type-name #:arity op arity-nat]))
|
||||
(opaque (code:line =) (code:line >) (code:line >=))]]{
|
||||
Import and assign types to bindings from outside Typed Syndicate.
|
||||
|
||||
Note that @emph{unlike} Typed Racket, Typed Syndicate does not attach contracts
|
||||
to imported bindings.
|
||||
|
||||
An @racket[#:opaque] declaration defines a type @racket[type-name] (or, in the
|
||||
@racket[#:arity] case, a type constructor) that may be used to describe imports
|
||||
but otherwise has no other operations.
|
||||
}
|
||||
|
||||
@defform[(require-struct ctor-id #:as ty-ctor-id #:from lib maybe-omit-accs)
|
||||
#:grammar
|
||||
[(maybe-omit-accs (code:line)
|
||||
(code:line #:omit-accs))]]{
|
||||
Import a Racket @racket[struct] named @racket[ctor-id] and create a type
|
||||
constructor @racket[ty-ctor-id] for its instances.
|
||||
|
||||
Unless @racket[#:omit-accs] is specified, defines the accessor functions for the
|
||||
struct.
|
||||
}
|
||||
|
||||
|
||||
@section{Builtin Data Structures}
|
||||
|
||||
@deftogether[(@defstruct[observe ([claim any?]) #:omit-constructor]
|
||||
@defform[(Observe type)])]{
|
||||
Constructs an assertion of interest.
|
||||
}
|
||||
|
||||
@deftogether[(@defstruct[inbound ([assertion any?]) #:omit-constructor]
|
||||
@defform[(Inbound type)])]{
|
||||
Constructor for an assertion inbound from an outer dataspace.
|
||||
}
|
||||
|
||||
@deftogether[(@defstruct[outbound ([assertion any?]) #:omit-constructor]
|
||||
@defform[(Outbound type)])]{
|
||||
Constructor for an assertion outbound to an outer dataspace.
|
||||
}
|
||||
|
||||
@deftogether[(@defstruct[message ([body any?]) #:omit-constructor]
|
||||
@defform[(Message type)])]{
|
||||
Constructor for a broadcast message.
|
||||
}
|
||||
|
||||
@subsection{Lists}
|
||||
|
||||
@defform[(List type)]{
|
||||
The type for @racket[cons] lists whose elements are of type @racket[type].
|
||||
}
|
||||
|
||||
@deftogether[(
|
||||
@defthing[empty (List ⊥)]
|
||||
@defthing[empty? (∀ (X) (→fn (List X) Bool))]
|
||||
@defthing[cons (∀ (X) (→fn X (List X) (List X)))]
|
||||
@defthing[cons? (∀ (X) (→fn X (List X) Bool))]
|
||||
@defthing[first (∀ (X) (→fn (List X) X))]
|
||||
@defthing[second (∀ (X) (→fn (List X) X))]
|
||||
@defthing[rest (∀ (X) (→fn (List X) (List X)))]
|
||||
@defthing[member? (∀ (X) (→fn X (List X) Bool))]
|
||||
@defthing[reverse (∀ (X) (→fn (List X) (List X)))]
|
||||
@defthing[partition (∀ (X) (→fn (List X) (→fn X Bool) (List X)))]
|
||||
@defthing[map (∀ (X Y) (→fn (→fn X Y) (List X) (List Y)))]
|
||||
@defthing[argmax (∀ (X) (→fn (→fn X Int) (List X) X))]
|
||||
@defthing[argmin (∀ (X) (→fn (→fn X Int) (List X) X))]
|
||||
@defthing[remove (∀ (X) (→fn X (List X) (List X)))]
|
||||
@defthing[length (∀ (X) (→fn (List X) Int))]
|
||||
@defform[(list e ...)]
|
||||
)]{
|
||||
Like their Racket counterparts.
|
||||
}
|
||||
|
||||
@subsection{Sets}
|
||||
|
||||
@defform[(Set type)]{
|
||||
The type for sets whose elements are of type @racket[type].
|
||||
}
|
||||
|
||||
@deftogether[(
|
||||
@defform[(set e ...)]
|
||||
@defform[(set-union st ...+)]
|
||||
@defform[(set-intersect st ...+)]
|
||||
@defform[(set-subtract st ...+)]
|
||||
@defthing[set-first (∀ (X) (→fn (Set X) X))]
|
||||
@defthing[set-empty? (∀ (X) (→fn (Set X) Bool))]
|
||||
@defthing[set-count (∀ (X) (→fn (Set X) Int))]
|
||||
@defthing[set-add (∀ (X) (→fn (Set X) X (Set X)))]
|
||||
@defthing[set-remove (∀ (X) (→fn (Set X) X (Set X)))]
|
||||
@defthing[set-member? (∀ (X) (→fn (Set X) X Bool))]
|
||||
@defthing[list->set (∀ (X) (→fn (List X) (Set X)))]
|
||||
@defthing[set->list (∀ (X) (→fn (Set X) (List X)))]
|
||||
)]{
|
||||
Like their Racket counterparts.
|
||||
}
|
||||
|
||||
@subsection{Hashes}
|
||||
|
||||
@defform[(Hash key-type value-type)]{
|
||||
The type for key/value hash tables.
|
||||
}
|
||||
|
||||
@deftogether[(
|
||||
@defform[(hash key val ... ...)]
|
||||
@defthing[hash-set (∀ (K V) (→fn (Hash K V) K V (Hash K V)))]
|
||||
@defthing[hash-ref (∀ (K V) (→fn (Hash K V) K V))]
|
||||
@defthing[hash-ref/failure (∀ (K V) (→fn (Hash K V) K V V))]
|
||||
@defthing[hash-empty? (∀ (K V) (→fn (Hash K V) Bool))]
|
||||
@defthing[hash-has-key? (∀ (K V) (→fn (Hash K V) K Bool))]
|
||||
@defthing[hash-count (∀ (K V) (→fn (Hash K V) Int))]
|
||||
@defthing[hash-update (∀ (K V) (→fn (Hash K V) K (→fn V V) (Hash K V)))]
|
||||
@defthing[hash-update/failure (∀ (K V) (→fn (Hash K V) K (→fn V V) V (Hash K V)))]
|
||||
@defthing[hash-remove (∀ (K V) (→fn (Hash K V) K (Hash K V)))]
|
||||
@defthing[hash-map (∀ (K V R) (→fn (Hash K V) (→fn K V R) (List R)))]
|
||||
@defthing[hash-keys (∀ (K V) (→fn (Hash K V) (List K)))]
|
||||
@defthing[hash-values (∀ (K V) (→fn (Hash K V) (List V)))]
|
||||
@defthing[hash-union (∀ (K1 V1 K2 V2) (→fn (Hash K1 V1) (Hash K2 V2) (Hash (U K1 K2) (U V1 V2))))]
|
||||
@defthing[hash-union/combine (∀ (K V) (→fn (Hash K V) (Hash K V) (→fn V V V) (Hash K V)))]
|
||||
@defthing[hash-keys-subset? (∀ (K1 V1 K2 V2) (→fn (Hash K1 V1) (Hash K2 V2) Bool))]
|
||||
)]{
|
||||
Like their Racket counterparts. The /failure and /combine suffixes are in place
|
||||
of keyword arguments, which Typed Syndicate does not presently support.
|
||||
}
|
||||
|
||||
@subsection{Sequences}
|
||||
|
||||
@defform[(Sequence type)]{
|
||||
The type for a sequence of @racket[type] values.
|
||||
}
|
||||
|
||||
@deftogether[(
|
||||
@defthing[empty-sequence (Sequence ⊥)]
|
||||
@defthing[sequence->list (∀ (X) (→fn (Sequence X) (List X)))]
|
||||
@defthing[sequence-length (∀ (X) (→fn (Sequence X) Int))]
|
||||
@defthing[sequence-ref (∀ (X) (→fn (Sequence X) Int Int))]
|
||||
@defthing[sequence-tail (∀ (X) (→fn (Sequence X) Int (Sequence X)))]
|
||||
@defthing[sequence-append (∀ (X) (→fn (Sequence X) (Sequence X) (Sequence X)))]
|
||||
@defthing[sequence-map (∀ (A B) (→fn (→fn A B) (Sequence A) (Sequence B)))]
|
||||
@defthing[sequence-andmap (∀ (X) (→fn (→fn X Bool) (Sequence X) Bool))]
|
||||
@defthing[sequence-ormap (∀ (X) (→fn (→fn X Bool) (Sequence X) Bool))]
|
||||
@defthing[sequence-fold (∀ (A B) (→fn (→fn A B A) (Sequence B) A))]
|
||||
@defthing[sequence-count (∀ (X) (→fn (→fn X Bool) (Sequence X) Int))]
|
||||
@defthing[sequence-filter (∀ (X) (→fn (→fn X Bool) (Sequence X) (Sequence X)))]
|
||||
@defthing[sequence-add-between (∀ (X) (→fn (Sequence X) X (Sequence X)))]
|
||||
@defthing[in-list (∀ (X) (→fn (List X) (Sequence X)))]
|
||||
@defthing[in-hash-keys (∀ (K V) (→fn (Hash K V) (Sequence K)))]
|
||||
@defthing[in-hash-values (∀ (K V) (→fn (Hash K V) (Sequence V)))]
|
||||
@defthing[in-range (→fn Int (Sequence Int))]
|
||||
@defthing[in-set (∀ (X) (→fn (Set X) (Sequence X)))]
|
||||
)]{
|
||||
Like their Racket counterparts.
|
||||
}
|
||||
|
||||
@subsection{Maybe}
|
||||
|
||||
@deftogether[(
|
||||
@defidform[None]
|
||||
@defthing[none None]
|
||||
@defstruct[some ([v any?]) #:omit-constructor]
|
||||
@defform[(Some type)]
|
||||
@defform[(Maybe type)]
|
||||
)]{
|
||||
@racket[(Maybe type)] is an alias for @racket[(U None (Some type))].
|
||||
}
|
||||
|
||||
@subsection{Either}
|
||||
|
||||
@deftogether[(
|
||||
@defstruct[left ([v any?]) #:omit-constructor]
|
||||
@defform[(Left type)]
|
||||
@defstruct[right ([v any?]) #:omit-constructor]
|
||||
@defform[(Right type)]
|
||||
@defform[(Either left-type right-type)]
|
||||
)]{
|
||||
@racket[(Either left-type right-type)] is an alias for @racket[(U (Left
|
||||
left-type) (Right right-type))].
|
||||
}
|
||||
|
||||
@defthing[partition/either (∀ (X Y Z) (→fn (List X) (→fn X (Either Y Z)) (Tuple (List Y) (List Z))))]{
|
||||
Partition a list based on a function that returns an @racket[Either] value.
|
||||
}
|
||||
|
||||
@section{Behavioral Checking}
|
||||
|
|
@ -17,15 +17,12 @@
|
|||
sequence-add-between
|
||||
in-list
|
||||
in-set
|
||||
in-hash-keys
|
||||
in-hash-values
|
||||
in-range
|
||||
)
|
||||
|
||||
(require "core-types.rkt")
|
||||
(require (only-in "list.rkt" List))
|
||||
(require (only-in "set.rkt" Set))
|
||||
(require (only-in "hash.rkt" Hash))
|
||||
(require (only-in "prim.rkt" Int Bool))
|
||||
#;(require (postfix-in - racket/sequence))
|
||||
|
||||
|
|
@ -53,8 +50,25 @@
|
|||
|
||||
(require/typed racket/base
|
||||
[in-list : (∀ (X) (→fn (List X) (Sequence X)))]
|
||||
[in-hash-keys : (∀ (K V) (→fn (Hash K V) (Sequence K)))]
|
||||
[in-hash-values : (∀ (K V) (→fn (Hash K V) (Sequence V)))]
|
||||
[in-range : (→fn Int (Sequence Int))])
|
||||
(require/typed racket/set
|
||||
[in-set : (∀ (X) (→fn (Set X) (Sequence X)))])
|
||||
|
||||
#;(define-typed-syntax empty-sequence
|
||||
[_ ≫
|
||||
--------------------
|
||||
[⊢ empty-sequence- (⇒ : (Sequence (U)))]])
|
||||
|
||||
;; er, this is making everything a macro, as opposed to a procedure...
|
||||
;; think I ought to add polymorphous first :\
|
||||
#;(define-typed-syntax (sequence->list s) ≫
|
||||
[⊢ s ≫ s- (⇒ : (~Sequence τ))]
|
||||
#:fail-unless (pure? #'s-)
|
||||
------------------------------
|
||||
[⊢ (sequence->list- s-) (⇒ : (List τ))])
|
||||
|
||||
#;(define-typed-syntax (sequence-length s) ≫
|
||||
[⊢ s ≫ s- (⇒ : (~Sequence τ))]
|
||||
#:fail-unless (pure? #'s-)
|
||||
------------------------------
|
||||
[⊢ (sequence-length- s-) (⇒ : Int)])
|
||||
|
|
@ -3,24 +3,19 @@
|
|||
(provide Set
|
||||
(for-syntax ~Set)
|
||||
set
|
||||
;; set-member?
|
||||
;; set-add
|
||||
;; set-remove
|
||||
;; set-count
|
||||
set-member?
|
||||
set-add
|
||||
set-remove
|
||||
set-count
|
||||
set-union
|
||||
set-subtract
|
||||
set-intersect
|
||||
;; list->set
|
||||
;; set->list
|
||||
(typed-out [[set-first- : (∀ (X) (→fn (Set X) X))] set-first]
|
||||
[[set-empty?- : (∀ (X) (→fn (Set X) Bool))] set-empty?]
|
||||
[[set-count- : (∀ (X) (→fn (Set X) Int))] set-count]
|
||||
[[set-add- : (∀ (X) (→fn (Set X) X (Set X)))] set-add]
|
||||
[[set-remove- : (∀ (X) (→fn (Set X) X (Set X)))] set-remove]
|
||||
[[set-member?- : (∀ (X) (→fn (Set X) X Bool))] set-member?]
|
||||
[[list->set- : (∀ (X) (→fn (List X) (Set X)))] list->set]
|
||||
[[set->list- : (∀ (X) (→fn (Set X) (List X)))] set->list]
|
||||
))
|
||||
list->set
|
||||
set->list
|
||||
(typed-out [[set-first- : (∀ (X) (→fn (Set X) X))]
|
||||
set-first]
|
||||
[[set-empty?- : (∀ (X) (→fn (Set X) Bool))]
|
||||
set-empty?]))
|
||||
|
||||
(require "core-types.rkt")
|
||||
(require (only-in "prim.rkt" Int Bool))
|
||||
|
|
@ -40,6 +35,38 @@
|
|||
---------------
|
||||
[⊢ (#%app- set- e- ...) ⇒ (Set (U τ ...))])
|
||||
|
||||
(define-typed-syntax (set-count e) ≫
|
||||
[⊢ e ≫ e- ⇒ (~Set _)]
|
||||
#:fail-unless (pure? #'e-) "expression must be pure"
|
||||
----------------------
|
||||
[⊢ (#%app- set-count- e-) ⇒ Int])
|
||||
|
||||
(define-typed-syntax (set-add st v) ≫
|
||||
[⊢ st ≫ st- ⇒ (~Set τs)]
|
||||
#:fail-unless (pure? #'st-) "expression must be pure"
|
||||
[⊢ v ≫ v- ⇒ τv]
|
||||
#:fail-unless (pure? #'v-) "expression must be pure"
|
||||
-------------------------
|
||||
[⊢ (#%app- set-add- st- v-) ⇒ (Set (U τs τv))])
|
||||
|
||||
(define-typed-syntax (set-remove st v) ≫
|
||||
[⊢ st ≫ st- ⇒ (~Set τs)]
|
||||
#:fail-unless (pure? #'st-) "expression must be pure"
|
||||
[⊢ v ≫ v- ⇐ τs]
|
||||
#:fail-unless (pure? #'v-) "expression must be pure"
|
||||
-------------------------
|
||||
[⊢ (#%app- set-remove- st- v-) ⇒ (Set τs)])
|
||||
|
||||
(define-typed-syntax (set-member? st v) ≫
|
||||
[⊢ st ≫ st- ⇒ (~Set τs)]
|
||||
#:fail-unless (pure? #'st-) "expression must be pure"
|
||||
[⊢ v ≫ v- ⇒ τv]
|
||||
#:fail-unless (pure? #'v-) "expression must be pure"
|
||||
#:fail-unless (<: #'τv #'τs)
|
||||
"type mismatch"
|
||||
-------------------------------------
|
||||
[⊢ (#%app- set-member?- st- v-) ⇒ Bool])
|
||||
|
||||
(define-typed-syntax (set-union st0 st ...) ≫
|
||||
[⊢ st0 ≫ st0- ⇒ (~Set τ-st0)]
|
||||
#:fail-unless (pure? #'st0-) "expression must be pure"
|
||||
|
|
@ -64,3 +91,15 @@
|
|||
#:fail-unless (all-pure? #'(st- ...)) "expressions must be pure"
|
||||
-------------------------------------
|
||||
[⊢ (#%app- set-subtract- st0- st- ...) ⇒ (Set τ-st0)])
|
||||
|
||||
(define-typed-syntax (list->set l) ≫
|
||||
[⊢ l ≫ l- ⇒ (~List τ)]
|
||||
#:fail-unless (pure? #'l-) "expression must be pure"
|
||||
-----------------------
|
||||
[⊢ (#%app- list->set- l-) ⇒ (Set τ)])
|
||||
|
||||
(define-typed-syntax (set->list s) ≫
|
||||
[⊢ s ≫ s- ⇒ (~Set τ)]
|
||||
#:fail-unless (pure? #'s-) "expression must be pure"
|
||||
-----------------------
|
||||
[⊢ (#%app- set->list- s-) ⇒ (List τ)])
|
||||
|
|
@ -1,2 +1,2 @@
|
|||
#lang s-exp syntax/module-reader
|
||||
typed/syndicate/roles
|
||||
typed/main
|
||||
|
|
|
|||
|
|
@ -1,2 +1,2 @@
|
|||
#lang s-exp syntax/module-reader
|
||||
typed/syndicate/roles
|
||||
typed/roles
|
||||
|
|
@ -1,4 +1,4 @@
|
|||
#lang typed/syndicate
|
||||
#lang typed/syndicate/roles
|
||||
|
||||
(require rackunit/turnstile)
|
||||
|
||||
|
|
|
|||
|
|
@ -1,26 +0,0 @@
|
|||
#lang typed/syndicate
|
||||
|
||||
(assertion-struct ping : Ping (v))
|
||||
(assertion-struct pong : Pong (v))
|
||||
|
||||
(assertion-struct flip : Flip (v))
|
||||
(assertion-struct flop : Flop (v))
|
||||
|
||||
(define-type-alias Pinger (Ping Int))
|
||||
(define-type-alias Ponger (U (Ping Int)
|
||||
(Pong Int)
|
||||
(Observe (Ping ★/t))))
|
||||
(define-type-alias PingPong (U Pinger Ponger))
|
||||
|
||||
(define-type-alias Flipper (Flip Int))
|
||||
(define-type-alias Flopper (U (Flip Int)
|
||||
(Flop Int)
|
||||
(Observe (Flip ★/t))))
|
||||
(define-type-alias FlipFlop (U Flipper Flopper))
|
||||
|
||||
(run-ground-dataspace (U PingPong FlipFlop)
|
||||
(spawn Pinger (start-facet _ (assert (ping 5))))
|
||||
(spawn Ponger (start-facet _ (during (ping $v) (assert (pong v)))))
|
||||
|
||||
(spawn Flipper (start-facet _ (assert (flip 8))))
|
||||
(spawn Flopper (start-facet _ (during (flip $v) (assert (flop v))))))
|
||||
|
|
@ -1,4 +1,4 @@
|
|||
#lang typed/syndicate
|
||||
#lang typed/syndicate/roles
|
||||
|
||||
(run-ground-dataspace (U)
|
||||
(spawn (U)
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
#lang typed/syndicate
|
||||
#lang typed/syndicate/roles
|
||||
|
||||
(require rackunit/turnstile)
|
||||
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
#lang typed/syndicate
|
||||
#lang typed/syndicate/roles
|
||||
|
||||
(require rackunit/turnstile)
|
||||
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
#lang typed/syndicate
|
||||
#lang typed/syndicate/roles
|
||||
|
||||
(require rackunit/turnstile)
|
||||
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
#lang typed/syndicate
|
||||
#lang typed/syndicate/roles
|
||||
|
||||
(require rackunit/turnstile)
|
||||
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
#lang typed/syndicate
|
||||
#lang typed/syndicate/roles
|
||||
|
||||
(require rackunit/turnstile)
|
||||
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
#lang typed/syndicate
|
||||
#lang typed/syndicate/roles
|
||||
|
||||
(require rackunit/turnstile)
|
||||
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
#lang typed/syndicate
|
||||
#lang typed/syndicate/roles
|
||||
|
||||
(require rackunit/turnstile)
|
||||
|
||||
|
|
|
|||
|
|
@ -1,22 +0,0 @@
|
|||
#lang typed/syndicate
|
||||
|
||||
(require rackunit/turnstile)
|
||||
|
||||
(typecheck-fail (spawn ⊥
|
||||
(start-facet x
|
||||
(on (asserted $x:Int)
|
||||
#f)))
|
||||
#:with-msg "overly broad interest")
|
||||
|
||||
(typecheck-fail (spawn ⊥
|
||||
(start-facet x
|
||||
(on (asserted (observe $x:Int))
|
||||
#f)))
|
||||
#:with-msg "overly broad interest")
|
||||
|
||||
;; TODO - but this one seems fine?
|
||||
(typecheck-fail (spawn ⊥
|
||||
(start-facet x
|
||||
(on (asserted _)
|
||||
#f)))
|
||||
#:with-msg "overly broad interest")
|
||||
|
|
@ -1,4 +1,4 @@
|
|||
#lang typed/syndicate
|
||||
#lang typed/syndicate/roles
|
||||
|
||||
(require rackunit/turnstile)
|
||||
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
#lang typed/syndicate
|
||||
#lang typed/syndicate/roles
|
||||
|
||||
(require rackunit/turnstile)
|
||||
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
#lang typed/syndicate
|
||||
#lang typed/syndicate/roles
|
||||
|
||||
(require rackunit/turnstile)
|
||||
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
#lang typed/syndicate
|
||||
#lang typed/syndicate/roles
|
||||
|
||||
(require rackunit/turnstile)
|
||||
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
#lang typed/syndicate
|
||||
#lang typed/syndicate/roles
|
||||
|
||||
(require rackunit/turnstile)
|
||||
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
#lang typed/syndicate
|
||||
#lang typed/syndicate/roles
|
||||
|
||||
(require rackunit/turnstile)
|
||||
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
#lang typed/syndicate
|
||||
#lang typed/syndicate/roles
|
||||
|
||||
(require rackunit/turnstile)
|
||||
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
#lang typed/syndicate
|
||||
#lang typed/syndicate/roles
|
||||
|
||||
(require rackunit/turnstile)
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue