1401 lines
55 KiB
Racket
1401 lines
55 KiB
Racket
#lang turnstile
|
||
|
||
(provide #%module-begin
|
||
#%app
|
||
(rename-out [typed-quote quote])
|
||
#%top-interaction
|
||
module+ module*
|
||
;; require & provides
|
||
require only-in prefix-in except-in rename-in
|
||
provide all-defined-out all-from-out rename-out except-out
|
||
for-syntax for-template for-label for-meta struct-out
|
||
;; Start dataspace programs
|
||
run-ground-dataspace
|
||
;; Types
|
||
Tuple Bind Discard → ∀ AssertionSet
|
||
Role Reacts Shares Asserted Retracted Message OnDataflow Stop OnStart OnStop Sends
|
||
Know Forget Realize
|
||
Branch Effs
|
||
FacetName Field ★/t
|
||
Observe Inbound Outbound Actor ActorWithRole U ⊥
|
||
→fn proc
|
||
True False Bool
|
||
(all-from-out "sugar.rkt")
|
||
;; Statements
|
||
let let* if spawn dataspace start-facet set! := begin block stop begin/dataflow #;unsafe-do
|
||
when unless send! realize! define during/spawn
|
||
with-facets start WithFacets Start
|
||
;; Derived Forms
|
||
during During
|
||
define/query-value
|
||
define/query-set
|
||
define/query-hash
|
||
define/dataflow
|
||
on-start on-stop
|
||
;; endpoints
|
||
assert know on field
|
||
;; expressions
|
||
tuple select lambda λ ref ! (struct-out observe) (struct-out message) (struct-out inbound) (struct-out outbound)
|
||
Λ inst call/inst
|
||
;; making types
|
||
define-type-alias
|
||
assertion-struct
|
||
message-struct
|
||
define-constructor define-constructor*
|
||
;; values
|
||
#%datum
|
||
;; patterns
|
||
bind discard
|
||
;; primitives
|
||
(all-from-out "prim.rkt")
|
||
;; expressions
|
||
(except-out (all-from-out "core-expressions.rkt") mk-tuple tuple-select)
|
||
;; lists
|
||
(all-from-out "list.rkt")
|
||
;; sets
|
||
(all-from-out "set.rkt")
|
||
;; sequences
|
||
(all-from-out "sequence.rkt")
|
||
;; hash tables
|
||
(all-from-out "hash.rkt")
|
||
;; for loops
|
||
(all-from-out "for-loops.rkt")
|
||
;; utility datatypes
|
||
(all-from-out "maybe.rkt")
|
||
(all-from-out "either.rkt")
|
||
;; DEBUG and utilities
|
||
print-type print-role role-strings print-effects
|
||
;; Behavioral Roles
|
||
export-roles export-type check-simulates check-has-simulating-subgraph lift+define-role
|
||
verify-actors verify-actors/fail
|
||
;; LTL Syntax
|
||
TT FF Always Eventually Until WeakUntil Release Implies And Or Not A M
|
||
define-ltl
|
||
;; Extensions
|
||
match cond
|
||
submod for-syntax for-meta only-in except-in
|
||
require/typed
|
||
require-struct
|
||
)
|
||
(require "core-types.rkt")
|
||
(require "core-expressions.rkt")
|
||
(require "list.rkt")
|
||
(require "set.rkt")
|
||
(require "prim.rkt")
|
||
(require "sequence.rkt")
|
||
(require "hash.rkt")
|
||
(require "for-loops.rkt")
|
||
(require "maybe.rkt")
|
||
(require "either.rkt")
|
||
(require "sugar.rkt")
|
||
|
||
(require (prefix-in syndicate: syndicate/actor-lang))
|
||
(require (submod syndicate/actor priorities))
|
||
(require (prefix-in syndicate: (submod syndicate/actor for-module-begin)))
|
||
|
||
(require (for-meta 2 macrotypes/stx-utils racket/list syntax/stx syntax/parse racket/base))
|
||
(require macrotypes/postfix-in)
|
||
(require (for-syntax turnstile/mode))
|
||
(require turnstile/typedefs)
|
||
(require (postfix-in - racket/list))
|
||
(require (postfix-in - racket/set))
|
||
|
||
(require (for-syntax (prefix-in proto: "proto.rkt")
|
||
(prefix-in proto: "ltl.rkt")
|
||
syntax/id-table)
|
||
(prefix-in proto: "proto.rkt")
|
||
(prefix-in proto: "compile-spin.rkt"))
|
||
|
||
(module+ test
|
||
(require rackunit)
|
||
(require rackunit/turnstile)
|
||
|
||
(begin-for-syntax
|
||
(require rackunit)))
|
||
|
||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||
;; Creating Communication Types
|
||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||
|
||
(define-simple-macro (assertion-struct name:id (~datum :) Name:id (slot:id ...))
|
||
(define-constructor* (name : Name slot ...)))
|
||
|
||
(define-simple-macro (message-struct name:id (~datum :) Name:id (slot:id ...))
|
||
(define-constructor* (name : Name slot ...)))
|
||
|
||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||
;; Compile-time State
|
||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||
|
||
(begin-for-syntax
|
||
(define current-communication-type (make-parameter #f))
|
||
;; Type -> Mode
|
||
(define (communication-type-mode ty)
|
||
(make-param-mode current-communication-type ty))
|
||
|
||
(define (elaborate-pattern/with-com-ty pat)
|
||
(define τ? (current-communication-type))
|
||
(if τ?
|
||
(elaborate-pattern/with-type pat τ?)
|
||
(elaborate-pattern pat))))
|
||
|
||
|
||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||
;; Effect Categories
|
||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||
|
||
(begin-for-syntax
|
||
(define (effects-andmap p eff)
|
||
(syntax-parse eff
|
||
[(~or* (~Effs F ...)
|
||
(~Branch F ...))
|
||
(stx-andmap (curry effects-andmap p) #'(F ...))]
|
||
[_
|
||
(p eff)]))
|
||
|
||
;; Any -> Bool
|
||
;; Recognizes effects that are allowed in an endpoint installation context
|
||
(define (endpoint-effect? eff)
|
||
(or (Shares? eff)
|
||
(Know? eff)
|
||
(Reacts? eff)
|
||
(MakesField? eff)
|
||
(ReadsField? eff)
|
||
(WritesField? eff)
|
||
(VarAssert? eff)
|
||
(row-variable? eff)))
|
||
|
||
;; Any -> Bool
|
||
;; Recognizes effects that are allowed in a script context
|
||
(define (script-effect? eff)
|
||
(or (TypeStartsFacet? eff)
|
||
(Stop? eff)
|
||
(Sends? eff)
|
||
(Realizes? eff)
|
||
(AnyActor? eff)
|
||
(Start? eff)
|
||
(ReadsField? eff)
|
||
(WritesField? eff)
|
||
(row-variable? eff)))
|
||
|
||
(define endpoint-effects? (curry effects-andmap endpoint-effect?))
|
||
(define script-effects? (curry effects-andmap script-effect?))
|
||
|
||
)
|
||
|
||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||
;; Core forms
|
||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||
|
||
(define-typed-syntax start-facet
|
||
[(_ name:id #:implements ~! spec:type ep ...+) ≫
|
||
[⊢ (start-facet name ep ...) ≫ e- (⇒ ν (~effs impl-ty))]
|
||
#:fail-unless (simulating-types? #'impl-ty #'spec.norm)
|
||
"facet does not implement specification"
|
||
------------------------------------------------------------
|
||
[≻ e-]]
|
||
[(_ name:id #:includes-behavior ~! spec:type ep ...+) ≫
|
||
[⊢ (start-facet name ep ...) ≫ e- (⇒ ν (~effs impl-ty))]
|
||
#:fail-unless (type-has-simulating-subgraphs? #'impl-ty #'spec.norm)
|
||
"no subset implements specified behavior"
|
||
------------------------------------------------------------
|
||
[≻ e-]]
|
||
[(_ name:id ep ...+) ≫
|
||
#:with name- (syntax-local-identifier-as-binding (syntax-local-introduce (generate-temporary #'name)))
|
||
#:with name+ (syntax-local-identifier-as-binding #'name)
|
||
#:with facet-name-ty (type-eval #'FacetName)
|
||
#:do [(define ctx (syntax-local-make-definition-context))
|
||
(define unique (gensym 'start-facet))
|
||
(define name-- (add-orig (internal-definition-context-introduce ctx #'name- 'add)
|
||
#'name))
|
||
(int-def-ctx-bind-type-rename #'name+ #'name- #'facet-name-ty ctx)
|
||
(define-values (ep-... τ... effects) (walk/bind #'(ep ...) ctx unique))
|
||
(ensure-all! endpoint-effects? effects "only endpoint effects allowed")
|
||
#;(unless (andmap endpoint-effect? effects)
|
||
(type-error #:src #'(ep ...) #:msg "only endpoint effects allowed"))]
|
||
#:with ((~or (~and τ-a (~Shares _))
|
||
(~and τ-k (~Know _))
|
||
;; untyped syndicate might allow this - TODO
|
||
#;(~and τ-m (~Sends _))
|
||
(~and τ-r (~Reacts _ _ ...))
|
||
(~MakesField _ _ _)
|
||
τ-other)
|
||
...)
|
||
effects
|
||
#:with τ (type-eval #`(Role (#,name--) #,@effects)
|
||
#;#`(Role (#,name--)
|
||
τ-a ...
|
||
τ-k ...
|
||
;; τ-m ...
|
||
τ-r ...
|
||
τ-other ...))
|
||
--------------------------------------------------------------
|
||
[⊢ (syndicate:react (let- ([#,name-- (#%app- syndicate:current-facet-id)])
|
||
#,@ep-...))
|
||
(⇒ : ★/t)
|
||
(⇒ ν (τ))]])
|
||
|
||
(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-
|
||
(⇒ ν (~effs F ...))]
|
||
#:fail-unless (stx-andmap endpoint-effects? #'(F ...)) "only endpoint effects allowed"
|
||
#:with pat- (substs #'(x- ...) #'(x ...) (compile-syndicate-pattern #'pat+))
|
||
#:with τc:type (current-communication-type)
|
||
#:with τ-facet (type-eval #'(Role (_) F ...))
|
||
#:with τ-spawn (mk-ActorWithRole- #'(τc.norm τ-facet))
|
||
#:with τ-endpoint (type-eval #'(Reacts (Asserted τp) τ-spawn))
|
||
------------------------------
|
||
[⊢ (syndicate:during/spawn pat- bdy-)
|
||
(⇒ : ★/t)
|
||
(⇒ ν (τ-endpoint))])
|
||
|
||
(define-typed-syntax field
|
||
[(_ [x:id (~optional (~datum :)) τ-f:type e:expr] ...) ≫
|
||
#:cut
|
||
#:fail-unless (stx-andmap flat-type? #'(τ-f ...)) "keep your uppity data outta my fields"
|
||
[⊢ e ≫ e- (⇐ : τ-f)] ...
|
||
#:fail-unless (all-pure? #'(e- ...)) "field initializers not allowed to have effects"
|
||
#:with (x- ...) (generate-temporaries #'(x ...))
|
||
#:with (τ ...) (stx-map type-eval #'((Field τ-f.norm) ...))
|
||
#:with (MF ...) (stx-map mk-MakesField #'(x ...) #'(τ-f.norm ...) (stx-map typeof #'(e- ...)))
|
||
----------------------------------------------------------------------
|
||
[⊢ (erased (field/intermediate [x x- τ e-] ...))
|
||
(⇒ : ★/t)
|
||
(⇒ ν (MF ...))]]
|
||
[(_ flds ... [x:id e:expr] more-flds ...) ≫
|
||
#:cut
|
||
[⊢ e ≫ e- (⇒ : τ)]
|
||
--------------------
|
||
[≻ (field flds ... [x τ e-] more-flds ...)]])
|
||
|
||
(define-typed-syntax (assert e:expr) ≫
|
||
[⊢ e ≫ e- (⇒ : τ) (⇒ ν (~effs F ...))]
|
||
#:fail-unless (pure? #'e-) "expression not allowed to have effects"
|
||
#:fail-unless (allowed-interest? #'τ) "overly broad interest, ?̱̱★ and ??★ not allowed"
|
||
#:with τs (mk-Shares- #'(τ))
|
||
#:with kont (syntax-parse #'(F ...)
|
||
[(~and ((~and RF (~ReadsField _)))
|
||
(~parse x:id (get-orig-field-name #'RF))
|
||
(~typecheck [⊢ x ≫ x- (⇒ : (~Field τ-f))])
|
||
(~parse (~and τ-U (~U* _ _)) (find-union #'τ-f)))
|
||
#'(type-varying-assert e e- x x- τ-f τ-U)]
|
||
[_ #'(just-assert e-)])
|
||
-------------------------------------
|
||
[≻ kont])
|
||
|
||
(define-typed-syntax (just-assert e-) ≫
|
||
#:with τ (detach #'e- ':)
|
||
#:with τs (mk-Shares- #'(τ))
|
||
-------------------------------------
|
||
[⊢ (syndicate:assert e-)
|
||
(⇒ : ★/t)
|
||
(⇒ ν (τs))])
|
||
|
||
;; need to make sure that the type has exactly one, binary union
|
||
(define-typed-syntax (type-varying-assert e e- x x- τ-f τ-U) ≫
|
||
;; #:do [(displayln 'A)]
|
||
#:with τe (detach #'e- ':)
|
||
;; #:do [(displayln 'B)]
|
||
#:with (~U* τi ...) #'τ-U
|
||
;; #:do [(displayln 'C)]
|
||
#:with ((τ-specific τe_i) ...) (for/list ([ti (in-syntax #'(τi ...))])
|
||
(define specific (type-subst #'τ-U ti #'τ-f))
|
||
(syntax-parse/typecheck null
|
||
[_ ≫
|
||
;; perhaps I should make sure the result is a subtype of the original?
|
||
[[x ≫ _ : (Field #,specific)] ⊢ e ≫ _ (⇒ : τe_i)]
|
||
----------------------------------------
|
||
[≻ (#,specific τe_i)]]))
|
||
;; #:do [(displayln 'D)]
|
||
;; [[x ≫ _ : Type] ⊢ x ≫ x--]
|
||
;; #:do [(displayln 'E)]
|
||
#:with VA (mk-VarAssert #'x #'[--> τ-f τe] #'([--> τ-specific τe_i] ...))
|
||
;; #:do [(pretty-display (type->strX #'VA))]
|
||
-------------------------------------------------------------------------
|
||
[⊢ (syndicate:assert e-)
|
||
(⇒ : ★/t)
|
||
(⇒ ν (VA))])
|
||
|
||
(begin-for-syntax
|
||
|
||
;; Type -> Type
|
||
(define (find-union t)
|
||
(syntax-parse t
|
||
[(~U* _ ...)
|
||
t]
|
||
[(~Any/new tycons tsub ...)
|
||
(stx-ormap find-union #'(tsub ...))]
|
||
[_
|
||
#f]))
|
||
|
||
;; replace τ1 with τ2 in e
|
||
;; TODO - possibly want a version that performs at most one substitution
|
||
(define (type-subst τ1 τ2 e)
|
||
(syntax-parse e
|
||
[t
|
||
#:when (type=? e τ1)
|
||
#;(transfer-stx-props τ (merge-type-tags (syntax-track-origin τ e e)))
|
||
τ2]
|
||
[(~Any/new tycons tsub ...)
|
||
#:when (reassemblable? #'tycons)
|
||
#:with subs (stx-map (λ (t1) (type-subst τ1 τ2 t1)) #'(tsub ...))
|
||
(transfer-stx-props (reassemble-type #'tycons #'subs) e #:ctx e)]
|
||
[_ e]))
|
||
)
|
||
|
||
(module+ test
|
||
(define-constructor* (bacon [pieces NonZero] [crispyness Bool]))
|
||
(begin-for-syntax
|
||
(test-case
|
||
"find-union"
|
||
(define T (type-eval #'(U Int String)))
|
||
(check type=? (find-union T)
|
||
T)
|
||
(check-false (find-union (type-eval #'Symbol)))
|
||
(check type=? (find-union (type-eval #`(Tuple #,T)))
|
||
T))
|
||
|
||
(test-case
|
||
"find-union struct"
|
||
(define B (type-eval #'Bacon))
|
||
(check type=? (find-union B)
|
||
(type-eval #'Bool))
|
||
|
||
(test-case
|
||
"type-subst"
|
||
(define I (type-eval #'Int))
|
||
(define S (type-eval #'String))
|
||
(check type=? (type-subst I S I)
|
||
S)
|
||
(check type=? (type-subst I S S)
|
||
S)
|
||
(define T (type-eval #'(Tuple Int String)))
|
||
(define TII (type-eval #'(Tuple Int Int)))
|
||
(check type=? (type-subst S I T)
|
||
TII)
|
||
(check type=? (type-subst I S T)
|
||
(type-eval #'(Tuple String String))))
|
||
|
||
(test-case
|
||
"type-subst union"
|
||
(define B (type-eval #'Bool))
|
||
(define TB (type-eval #'(Tuple Bool)))
|
||
(define T (type-eval #'True))
|
||
(check type=? (type-subst B T B)
|
||
T)
|
||
(check type=? (type-subst B T TB)
|
||
(type-eval #'(Tuple True)))
|
||
|
||
(define BCN (type-eval #'Bacon))
|
||
(define BCT (type-eval #'(BaconT NonZero True)))
|
||
(check type=? (type-subst B T BCN)
|
||
BCT))
|
||
)))
|
||
|
||
(define-typed-syntax (know e:expr) ≫
|
||
[⊢ e ≫ e- (⇒ : τ)]
|
||
#:fail-unless (pure? #'e-) "expression not allowed to have effects"
|
||
#:with τs (mk-Know- #'(τ))
|
||
-------------------------------------
|
||
[⊢ (syndicate:know e-) (⇒ : ★/t)
|
||
(⇒ ν (τs))])
|
||
|
||
(define-typed-syntax (send! e:expr) ≫
|
||
[⊢ e ≫ e- (⇒ : τ)]
|
||
#:fail-unless (pure? #'e-) "expression not allowed to have effects"
|
||
#:with τm (mk-Sends- #'(τ))
|
||
--------------------------------------
|
||
[⊢ (#%app- syndicate:send! e-) (⇒ : ★/t)
|
||
(⇒ ν (τm))])
|
||
|
||
(define-typed-syntax (realize! e:expr) ≫
|
||
[⊢ e ≫ e- (⇒ : τ)]
|
||
#:fail-unless (pure? #'e-) "expression not allowed to have effects"
|
||
#:with τm (mk-Realizes- #'(τ))
|
||
--------------------------------------
|
||
[⊢ (#%app- syndicate:realize! e-)
|
||
(⇒ : ★/t)
|
||
(⇒ ν (τm))])
|
||
|
||
(define-typed-syntax (stop facet-name:id cont ...) ≫
|
||
[⊢ facet-name ≫ facet-name- (⇐ : FacetName)]
|
||
[⊢ (block #f cont ...) ≫ cont- (⇒ ν (F ...))]
|
||
#:do [(ensure-all! script-effects? (syntax->list #'(F ...)) "only script effects allowed in stop continuation")]
|
||
;; #:fail-unless (stx-andmap script-effects? #'(F ...)) "only script effects allowed"
|
||
#:with τ (type-eval #'(Stop facet-name- F ...))
|
||
---------------------------------------------------------------------------------
|
||
[⊢ (syndicate:stop-facet facet-name- cont-) (⇒ : ★/t)
|
||
(⇒ ν (τ))])
|
||
|
||
(begin-for-syntax
|
||
(define-syntax-class event-cons
|
||
#:attributes (syndicate-kw ty-cons)
|
||
#:datum-literals (asserted retracted message know forget realize)
|
||
(pattern (~or (~and asserted
|
||
(~bind [syndicate-kw #'syndicate:asserted]
|
||
[ty-cons #'Asserted]))
|
||
(~and retracted
|
||
(~bind [syndicate-kw #'syndicate:retracted]
|
||
[ty-cons #'Retracted]))
|
||
(~and message
|
||
(~bind [syndicate-kw #'syndicate:message]
|
||
[ty-cons #'Message]))
|
||
(~and know
|
||
(~bind [syndicate-kw #'syndicate:know]
|
||
[ty-cons #'Know]))
|
||
(~and forget
|
||
(~bind [syndicate-kw #'syndicate:forget]
|
||
[ty-cons #'Forget]))
|
||
(~and realize
|
||
(~bind [syndicate-kw #'syndicate:realize]
|
||
[ty-cons #'Realize])))))
|
||
(define-syntax-class priority-level
|
||
#:literals (*query-priority-high*
|
||
*query-priority*
|
||
*query-handler-priority*
|
||
*normal-priority*
|
||
*gc-priority*
|
||
*idle-priority*)
|
||
(pattern (~and level
|
||
(~or *query-priority-high*
|
||
*query-priority*
|
||
*query-handler-priority*
|
||
*normal-priority*
|
||
*gc-priority*
|
||
*idle-priority*))))
|
||
(define-splicing-syntax-class priority
|
||
#:attributes (level)
|
||
(pattern (~seq #:priority l:priority-level)
|
||
#:attr level #'l.level)
|
||
(pattern (~seq)
|
||
#:attr level #'*normal-priority*))
|
||
)
|
||
|
||
(define-typed-syntax on
|
||
#:datum-literals (start stop)
|
||
[(on start s ...+) ≫
|
||
[⊢ (block s ...) ≫ s- (⇒ ν (~effs F ...))]
|
||
#:fail-unless (stx-andmap script-effects? #'(F ...)) "only script effects allowed"
|
||
#:with τ-r (type-eval #'(Reacts OnStart F ...))
|
||
-----------------------------------
|
||
[⊢ (syndicate:on-start s-)
|
||
(⇒ : ★/t)
|
||
(⇒ ν (τ-r))]]
|
||
[(on stop s ...+) ≫
|
||
[⊢ (block s ...) ≫ s- (⇒ ν (~effs F ...))]
|
||
#:fail-unless (stx-andmap script-effects? #'(F ...)) "only script effects allowed"
|
||
#:with τ-r (type-eval #'(Reacts OnStop F ...))
|
||
-----------------------------------
|
||
[⊢ (syndicate:on-stop s-)
|
||
(⇒ : ★/t)
|
||
(⇒ ν (τ-r))]]
|
||
[(on (evt:event-cons p)
|
||
priority:priority
|
||
s ...+) ≫
|
||
#:do [(define msg? (free-identifier=? #'syndicate:message (attribute evt.syndicate-kw)))
|
||
(define elab
|
||
(elaborate-pattern/with-com-ty (if msg? #'(message p) #'p)))]
|
||
#: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-
|
||
(⇒ ν (~effs F ...))]
|
||
#:fail-unless (stx-andmap script-effects? #'(F ...)) "only script effects allowed"
|
||
#:with p- (substs #'(x- ...) #'(x ...) (compile-syndicate-pattern #'p/e))
|
||
#:with τ-r (type-eval #'(Reacts (evt.ty-cons τp) F ...))
|
||
-----------------------------------
|
||
[⊢ (syndicate:on (evt.syndicate-kw p-)
|
||
#:priority priority.level
|
||
s-)
|
||
(⇒ : ★/t)
|
||
(⇒ ν (τ-r))]])
|
||
|
||
(define-typed-syntax (begin/dataflow s ...+) ≫
|
||
[⊢ (block s ...) ≫ s-
|
||
(⇒ ν (~effs F ...))]
|
||
#:with τ-r (type-eval #'(Reacts OnDataflow F ...))
|
||
--------------------------------------------------
|
||
[⊢ (syndicate:begin/dataflow s-)
|
||
(⇒ : ★/t)
|
||
(⇒ ν (τ-r))])
|
||
|
||
(define-for-syntax (compile-syndicate-pattern pat)
|
||
(compile-pattern pat
|
||
#'list-
|
||
(lambda (id) #`($ #,id))
|
||
identity))
|
||
|
||
(define-typed-syntax spawn
|
||
[(spawn tc s) ≫
|
||
;; this setup is to avoid re-expansion of the tc position :<
|
||
#:cut
|
||
#:with τ-c:type #'tc
|
||
#:fail-unless (flat-type? #'τ-c.norm) "Communication type must be first-order"
|
||
;; TODO: check that each τ-f is a Role
|
||
#:mode (communication-type-mode #'τ-c.norm)
|
||
[
|
||
[⊢ (block s) ≫ s- (⇒ ν (~effs F ...))]
|
||
]
|
||
;; TODO: s shouldn't refer to facets or fields!
|
||
#:do [(ensure! (lambda (Fs) (= 1 (stx-length Fs))) #'(F ...) "expected exactly one Role for body")
|
||
(ensure-all! TypeStartsFacet? (syntax->list #'(F ...)) "only effects that start a facet allowed")]
|
||
;;#:fail-unless (and (stx-andmap TypeStartsFacet? #'(F ...))
|
||
;;(= 1 (length (syntax->list #'(F ...)))))
|
||
;;"expected exactly one Role for body"
|
||
#:with (τ-i τ-o τ-i/i τ-o/i τ-a) (analyze-roles #'(F ...))
|
||
#:fail-unless (<: #'τ-o #'τ-c.norm)
|
||
(format "Outputs ~a not valid in dataspace ~a" (make-output-error-message #'τ-o #'τ-c.norm) (type->strX #'τ-c.norm))
|
||
#:with τ-final #;(mk-Actor- #'(τ-c.norm)) (mk-ActorWithRole- #'(τ-c.norm F ...))
|
||
#:fail-unless (<: #'τ-a #'τ-final)
|
||
"Spawned actors not valid in dataspace"
|
||
#:fail-unless (project-safe? (∩ (strip-? #'τ-o) #'τ-c.norm)
|
||
#'τ-i)
|
||
(string-append "Not prepared to handle inputs:\n" (make-actor-error-message #'τ-i #'τ-o #'τ-c.norm))
|
||
#:fail-unless (project-safe? (∩ (strip-? #'τ-o/i) #'τ-o/i) #'τ-i/i)
|
||
(string-append "Not prepared to handle internal events:\n" (make-actor-error-message #'τ-i/i #'τ-o/i #'τ-o/i))
|
||
--------------------------------------------------------------------------------------------
|
||
[⊢ (syndicate:spawn (syndicate:on-start s-)) (⇒ : ★/t)
|
||
(⇒ ν (τ-final))]]
|
||
[(spawn s) ≫
|
||
#:do [(define τc (current-communication-type))]
|
||
#:when τc
|
||
#:cut
|
||
----------------------------------------
|
||
[≻ (spawn #,τc s)]]
|
||
[(spawn s) ≫
|
||
#:cut
|
||
[⊢ (block s) ≫ s- (⇒ ν (~effs F ...))]
|
||
;; TODO: s shouldn't refer to facets or fields!
|
||
#:fail-unless (and (stx-andmap TypeStartsFacet? #'(F ...))
|
||
(= 1 (length (syntax->list #'(F ...)))))
|
||
"expected exactly one Role for body"
|
||
#:with (τ-i τ-o τ-i/i τ-o/i τ-a) (analyze-roles #'(F ...))
|
||
#:do [(ensure-inputs! #'τ-i/i #'τ-o/i #'τ-o/i this-syntax)]
|
||
;; #:fail-unless (project-safe? (∩ (strip-? #'τ-o/i) #'τ-o/i) #'τ-i/i)
|
||
;; (string-append "Not prepared to handle internal events:\n" (make-actor-error-message #'τ-i/i #'τ-o/i #'τ-o/i))
|
||
;; if there are Discards in pattern types, this will take more specific instances from other patterns
|
||
#:with τ-i/o (replace-bind-and-discard-with-★ (instantiate-pattern-type #'τ-i))
|
||
#:with (~U* (~AnyActor τ-c/spawned) ...) #'τ-a
|
||
#:with τ-c/this-actor (type-eval #'(U τ-i/o τ-o))
|
||
#:with τ-c/final (type-eval #'(U τ-c/this-actor τ-c/spawned ...))
|
||
#:do [(ensure-inputs! #'τ-i #'τ-o #'τ-c/final this-syntax)]
|
||
;; #:fail-unless (project-safe? (∩ (strip-? #'τ-o) #'τ-c/final)
|
||
;; #'τ-i)
|
||
;; (string-append "Not prepared to handle inputs:\n" (make-actor-error-message #'τ-i #'τ-o #'τ-c/final))
|
||
#:with τ-final (mk-ActorWithRole- #'(τ-c/final F ...))
|
||
#:do [(for ([t/spawned (in-syntax #'(τ-c/spawned ...))])
|
||
(ensure-actor-sub! t/spawned #'τ-c/final this-syntax))]
|
||
;; #:fail-unless (<: #'τ-a #'τ-final)
|
||
;; "Spawned actors not valid in dataspace"
|
||
----------------------------------------
|
||
[⊢ (syndicate:spawn (syndicate:on-start s-)) (⇒ : ★/t)
|
||
(⇒ ν (τ-final))]])
|
||
|
||
(define-for-syntax (ensure-outputs! τ-o τ-c [loc τ-o])
|
||
(unless (<: τ-o τ-c)
|
||
(define msg (format "Outputs ~a not valid in dataspace ~a"
|
||
(make-output-error-message τ-o τ-c)
|
||
(type->strX τ-c)))
|
||
(type-error #:src loc #:msg msg)))
|
||
|
||
(define-for-syntax (ensure-inputs! τ-i τ-o τ-c [loc τ-i])
|
||
(unless (project-safe? (∩ (strip-? τ-o) τ-c) τ-i)
|
||
(define msg (string-append "Not prepared to handle inputs:\n"
|
||
(make-actor-error-message τ-i τ-o τ-c)))
|
||
(type-error #:src loc #:msg msg)))
|
||
|
||
(define-for-syntax (ensure-actor-type! τ-i τ-o τ-c [loc τ-i])
|
||
(ensure-outputs! τ-o τ-c loc)
|
||
(ensure-inputs! τ-i τ-o τ-c loc))
|
||
|
||
(define-for-syntax (ensure-actor-sub! τ-a τ-c [loc τ-a])
|
||
(ensure-outputs! τ-a τ-c loc)
|
||
(unless (<: (∩ (strip-? τ-a) τ-c) τ-a)
|
||
(define mismatches (find-surprising-inputs τ-a τ-a τ-c (lambda (t1 t2) (not (<: t1 t2)))))
|
||
(define msg (string-append "Spawned actor not prepared to handle inputs:\n"
|
||
(tys->str mismatches)
|
||
"\nContext:\n"
|
||
(type->strX τ-a)))
|
||
(type-error #:src loc
|
||
#:msg msg)))
|
||
|
||
;; (Listof Type) -> String
|
||
(define-for-syntax (tys->str tys)
|
||
(string-join (map type->strX tys) ",\n"))
|
||
|
||
;; Type Type -> String
|
||
(define-for-syntax (make-output-error-message τ-o τ-c)
|
||
;; Type -> (Listof Type)
|
||
(define (flatten-U τ)
|
||
(syntax-parse τ
|
||
[(~U* τs ...)
|
||
(apply append (stx-map flatten-U #'(τs ...)))]
|
||
[_
|
||
(list τ)]))
|
||
(define offenders
|
||
(for/list ([t (in-list (flatten-U τ-o))]
|
||
#:unless (<: t τ-c))
|
||
t))
|
||
(tys->str offenders))
|
||
|
||
;; Type Type Type -> String
|
||
(define-for-syntax (make-actor-error-message τ-i τ-o τ-c)
|
||
(define mismatches (find-surprising-inputs τ-i τ-o τ-c
|
||
(lambda (t1 t2) (not (project-safe? t1 t2)))))
|
||
(tys->str mismatches))
|
||
|
||
;; Type Type Type -> (Listof Type)
|
||
(define-for-syntax (find-surprising-inputs τ-i τ-o τ-c surprising?)
|
||
(define incoming (∩ (strip-? τ-o) τ-c))
|
||
;; Type -> (Listof Type)
|
||
(let loop ([ty incoming])
|
||
(syntax-parse ty
|
||
[(~U* τ ...)
|
||
(apply append (map loop (syntax->list #'(τ ...))))]
|
||
[_
|
||
(cond
|
||
[(surprising? ty τ-i)
|
||
(list ty)]
|
||
[else
|
||
(list)])])))
|
||
|
||
(define-typed-syntax dataspace
|
||
[(dataspace τ-c:type s ...) ≫
|
||
#:cut
|
||
#:fail-unless (flat-type? #'τ-c.norm) "Communication type must be first-order"
|
||
#:mode (communication-type-mode #'τ-c.norm)
|
||
[
|
||
[⊢ s ≫ s- (⇒ ν (~effs F ...))] ...
|
||
]
|
||
#:with τ-actor (mk-Actor- #'(τ-c.norm))
|
||
#:fail-unless (stx-andmap AnyActor? #'(F ... ...)) "only actor spawning effects allowed"
|
||
#:do [(define errs (for/list ([t (in-syntax #'(F ... ...))]
|
||
#:unless (<: t #'τ-actor))
|
||
t))]
|
||
#:fail-unless (empty? errs) (make-dataspace-error-message errs #'τ-c.norm)
|
||
;; #:fail-unless (stx-andmap (lambda (t) (<: t #'τ-actor)) #'(τ-s ... ...))
|
||
;; "Not all actors conform to communication type"
|
||
#:with τ-ds-i (strip-inbound #'τ-c.norm)
|
||
#:with τ-ds-o (strip-outbound #'τ-c.norm)
|
||
#:with τ-relay (relay-interests #'τ-c.norm)
|
||
#:with τ-ds-act (mk-Actor- (list (mk-U- #'(τ-ds-i τ-ds-o τ-relay))))
|
||
-----------------------------------------------------------------------------------
|
||
[⊢ (syndicate:dataspace s- ...) (⇒ : ★/t)
|
||
(⇒ ν-s (τ-ds-act))]]
|
||
[(dataspace s ...) ≫
|
||
[⊢ s ≫ s- (⇒ ν (~effs F ...))] ...
|
||
#:cut
|
||
#:fail-unless (stx-andmap AnyActor? #'(F ... ...)) "only actor spawning effects allowed"
|
||
#:with ((~AnyActor τc/spawned) ...) #'(F ... ...)
|
||
#:with τc (type-eval #'(U τc/spawned ...))
|
||
-----------------------------------------------------------------------------------
|
||
[≻ (dataspace τc s- ...)]])
|
||
|
||
;; (Listof Type) Type -> String
|
||
(define-for-syntax (make-dataspace-error-message errs tc)
|
||
(with-output-to-string
|
||
(lambda ()
|
||
(printf "Not all actors conform to communication type:\n")
|
||
(pretty-display (type->strX tc))
|
||
(printf "found the following mismatches:\n")
|
||
(for ([err (in-list errs)])
|
||
(syntax-parse err
|
||
[(~AnyActor τ)
|
||
(printf "Actor with communication type ~a:\n" (type->strX #'τ))
|
||
(cond
|
||
[(<: #'τ tc)
|
||
(define mismatches (find-surprising-inputs #'τ #'τ tc (lambda (t1 t2) (not (<: t1 t2)))))
|
||
(define msg (tys->str mismatches))
|
||
(printf " unprepared to handle inputs: ~a\n" msg)]
|
||
[else
|
||
(define msg (make-output-error-message #'τ tc))
|
||
(printf " outputs not valid: ~a\n" msg)])
|
||
])))))
|
||
|
||
(define-typed-syntax (set! x:id e:expr) ≫
|
||
[⊢ e ≫ e- (⇒ : τ) (⇒ ν (~effs F ...))]
|
||
[⊢ x ≫ x- (⇒ : (~Field τ-x:type))]
|
||
#:fail-unless (<: #'τ #'τ-x) "Ill-typed field write"
|
||
#:with WF (mk-WritesField #'x #'τ)
|
||
----------------------------------------------------
|
||
[⊢ (#%app- x- e-) (⇒ : ★/t) (⇒ ν (WF F ...))])
|
||
|
||
(define-simple-macro (:= e ...)
|
||
(set! e ...))
|
||
|
||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||
;; With Facets
|
||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||
|
||
(define-for-syntax (walk/with-facets e... [unique (gensym 'walk/with-facets)])
|
||
(define-values (rev-e-... effects)
|
||
(let loop ([e... (syntax->list e...)]
|
||
[rev-e-... '()]
|
||
[effects '()])
|
||
(match e...
|
||
['()
|
||
(values rev-e-... effects)]
|
||
[(cons e more)
|
||
(define e- (local-expand e (list unique) (list #'erased)))
|
||
(syntax-parse e-
|
||
#:literals (erased)
|
||
[(erased impl)
|
||
(define effs (syntax->list (get-effect e- EFF-KEY)))
|
||
(loop more
|
||
(cons #'impl rev-e-...)
|
||
(append effs effects))])])))
|
||
(values (reverse rev-e-...)
|
||
effects))
|
||
|
||
(define-typed-syntax (with-facets ([x:id impl:expr] ...) fst:id) ≫
|
||
#:fail-unless (for/or ([y (in-syntax #'(x ...))]) (free-identifier=? #'fst y))
|
||
"must select one facet to start"
|
||
[[x ≫ x- : StartableFacet] ... ⊢ (with-facets-impls ([x impl] ...) fst) ≫ impl- (⇒ ν (~effs wsf-body))]
|
||
#:with WSFs (type-eval #'(WithStartableFacets [x- ...] wsf-body))
|
||
----------------------------------------
|
||
[⊢ impl- (⇒ : ★/t) (⇒ ν (WSFs))])
|
||
|
||
(define-typed-syntax (with-facets-impls ([x impl] ...) fst) ≫
|
||
#:do [(define-values (bodies FIs) (walk/with-facets #'([facet-impl x impl] ...)))]
|
||
[⊢ fst ≫ fst-]
|
||
----------------------------------------
|
||
[⊢ (let- ()
|
||
#,@bodies
|
||
(#%app- fst-))
|
||
(⇒ ν ((WSFBody (FacetImpls #,@FIs) fst-)))])
|
||
|
||
(define-typed-syntax (facet-impl x ((~datum facet) impl ...+)) ≫
|
||
[⊢ x ≫ x-]
|
||
[⊢ (start-facet x impl ...) ≫ impl- (⇒ ν (~effs (~and R (~Role (x--) Body ...))))]
|
||
----------------------------------------
|
||
[⊢ (erased (define- (x-) impl-)) (⇒ ν ((FacetImpl x- R)))])
|
||
|
||
(define-typed-syntax (start x:id) ≫
|
||
[⊢ x ≫ x- (⇒ : ~StartableFacet)]
|
||
#:with Sx (type-eval #'(Start x))
|
||
----------------------------------------
|
||
[⊢ (#%app- x-) (⇒ : ★/t) (⇒ ν (Sx))])
|
||
|
||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||
;; Derived Forms
|
||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||
|
||
(define-typed-syntax during
|
||
#:literals (know)
|
||
[(_ (~or (~and k (know p)) p) s ...) ≫
|
||
#:with p+ (elaborate-pattern/with-com-ty #'p)
|
||
#:with inst-p (instantiate-pattern #'p+)
|
||
#:with start-e (if (attribute k) #'know #'asserted)
|
||
#:with stop-e (if (attribute k) #'forget #'retracted)
|
||
----------------------------------------
|
||
[≻ (on (start-e p+)
|
||
(start-facet during-inner
|
||
(on (stop-e inst-p)
|
||
(stop during-inner))
|
||
s ...))]])
|
||
|
||
(define-simple-macro (During (~or (~and K ((~literal Know) τ:type)) τ:type)
|
||
EP ...)
|
||
#:with τ/inst (instantiate-pattern-type #'τ.norm)
|
||
#:with start-e (if (attribute K) #'Know #'Asserted)
|
||
#:with stop-e (if (attribute K) #'Forget #'Retracted)
|
||
(Reacts (start-e τ)
|
||
(Role (during-inner)
|
||
(Reacts (stop-e τ/inst)
|
||
(Stop during-inner))
|
||
EP ...)))
|
||
|
||
;; TODO - reconcile this with `compile-pattern`
|
||
(define-for-syntax (instantiate-pattern pat)
|
||
(let loop ([pat pat])
|
||
(syntax-parse pat
|
||
#:datum-literals (tuple discard bind)
|
||
[(tuple p ...)
|
||
#`(tuple #,@(stx-map loop #'(p ...)))]
|
||
[(bind x:id τ)
|
||
#'x]
|
||
;; not sure about this
|
||
[discard
|
||
#'discard]
|
||
[(~constructor-exp ctor p ...)
|
||
(define/with-syntax uctor (untyped-ctor #'ctor))
|
||
#`(ctor #,@(stx-map loop #'(p ...)))]
|
||
[_
|
||
pat])))
|
||
|
||
;; Type -> Type
|
||
;; replace occurrences of (Bind τ) with τ in a type, in much the same way
|
||
;; instantiate-pattern does for patterns
|
||
;; TODO - this is almost exactly the same as replace-bind-and-discard-with-★
|
||
(define-for-syntax (instantiate-pattern-type ty)
|
||
(syntax-parse ty
|
||
[(~Bind τ)
|
||
#'τ]
|
||
[(~U* τ ...)
|
||
(mk-U- (stx-map instantiate-pattern-type #'(τ ...)))]
|
||
[(~Any/new τ-cons τ ...)
|
||
#:when (reassemblable? #'τ-cons)
|
||
(define subitems (for/list ([t (in-syntax #'(τ ...))])
|
||
(instantiate-pattern-type t)))
|
||
(reassemble-type #'τ-cons subitems)]
|
||
[_ ty]))
|
||
|
||
(begin-for-syntax
|
||
(define-splicing-syntax-class on-add
|
||
#:attributes (expr)
|
||
(pattern (~seq #:on-add add-e)
|
||
#:attr expr #'add-e)
|
||
(pattern (~seq)
|
||
#:attr expr #'#f))
|
||
|
||
(define-splicing-syntax-class on-remove
|
||
#:attributes (expr)
|
||
(pattern (~seq #:on-remove remove-e)
|
||
#:attr expr #'remove-e)
|
||
(pattern (~seq)
|
||
#:attr expr #'#f)))
|
||
|
||
|
||
(define-typed-syntax (define/query-value (~or* x:id
|
||
[x:id (~optional (~datum :)) τ:type])
|
||
e0
|
||
p
|
||
e
|
||
(~optional add:on-add)
|
||
(~optional remove:on-remove)) ≫
|
||
[⊢ e0 ≫ e0- (⇒ : τ0)]
|
||
#:do [(when (and (attribute τ)
|
||
(not (<: #'τ0 (attribute τ.norm))))
|
||
(type-error #:src #'e0
|
||
#:msg "initial expression doesn't match given type;\ngot ~a\nexpected ~a"
|
||
(type->strX #'τ0)
|
||
(type->strX #'τ.norm)))]
|
||
#:fail-unless (pure? #'e0-) "expression must be pure"
|
||
----------------------------------------
|
||
[≻ (begin (field [x (~? τ.norm) e0-])
|
||
(on (asserted p)
|
||
#:priority *query-priority*
|
||
(set! x e)
|
||
add.expr)
|
||
(on (retracted p)
|
||
#:priority *query-priority-high*
|
||
(set! x e0-)
|
||
remove.expr))])
|
||
|
||
(define-typed-syntax (define/query-set x:id p e
|
||
(~optional add:on-add)
|
||
(~optional remove:on-remove)) ≫
|
||
#:with p+ (elaborate-pattern/with-com-ty #'p)
|
||
#:with ([y τ] ...) (pat-bindings #'p+)
|
||
;; e will be re-expanded :/
|
||
[[y ≫ y- : τ] ... ⊢ e ≫ e- ⇒ τ-e]
|
||
----------------------------------------
|
||
[≻ (begin (field [x (Set τ-e) (set)])
|
||
(on (asserted p+)
|
||
#:priority *query-priority*
|
||
(set! x (set-add (ref x) e))
|
||
add.expr)
|
||
(on (retracted p+)
|
||
#:priority *query-priority-high*
|
||
(set! x (set-remove (ref x) e))
|
||
remove.expr))])
|
||
|
||
(define-typed-syntax (define/query-hash x:id p e-key e-value
|
||
(~optional add:on-add)
|
||
(~optional remove:on-remove)) ≫
|
||
#:with p+ (elaborate-pattern/with-com-ty #'p)
|
||
#:with ([y τ] ...) (pat-bindings #'p+)
|
||
;; e-key and e-value will be re-expanded :/
|
||
;; but it's the most straightforward way to keep bindings in sync with
|
||
;; pattern
|
||
[[y ≫ y- : τ] ... ⊢ e-key ≫ e-key- ⇒ τ-key]
|
||
[[y ≫ y-- : τ] ... ⊢ e-value ≫ e-value- ⇒ τ-value]
|
||
;; TODO - this is gross, is there a better way to do this?
|
||
;; #:with e-value-- (substs #'(y- ...) #'(y-- ...) #'e-value- free-identifier=?)
|
||
;; I thought I could put e-key- and e-value-(-) in the output below, but that
|
||
;; gets their references to pattern variables out of sync with `p`
|
||
----------------------------------------
|
||
[≻ (begin (field [x (Hash τ-key τ-value) (hash)])
|
||
(on (asserted p+)
|
||
#:priority *query-priority*
|
||
(set! x (hash-set (ref x) e-key e-value))
|
||
add.expr)
|
||
(on (retracted p+)
|
||
#:priority *query-priority-high*
|
||
(set! x (hash-remove (ref x) e-key))
|
||
remove.expr))])
|
||
|
||
(define-simple-macro (on-start e ...)
|
||
(on start e ...))
|
||
|
||
(define-simple-macro (on-stop e ...)
|
||
(on stop e ...))
|
||
|
||
(define-typed-syntax define/dataflow
|
||
[(define/dataflow x:id τ:type e) ≫
|
||
[⊢ e ≫ e- (⇐ : τ)]
|
||
#:fail-unless (pure? #'e-) "expression must be pure"
|
||
;; because the begin/dataflow body is scheduled to run at some later point,
|
||
;; the initial value is visible e.g. immediately after the define/dataflow
|
||
;; #:with place-holder (attach #'(#%datum- #f) ': #'τ.norm)
|
||
----------------------------------------
|
||
[≻ (begin (field [x τ e-])
|
||
(begin/dataflow (set! x e-)))]]
|
||
[(define/dataflow x:id e) ≫
|
||
[⊢ e ≫ e- (⇒ : τ)]
|
||
#:fail-unless (pure? #'e-) "expression must be pure"
|
||
----------------------------------------
|
||
[≻ (define/dataflow x τ e-)]])
|
||
|
||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||
;; Expressions
|
||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||
|
||
(define-typed-syntax (ref x:id) ≫
|
||
[⊢ x ≫ x- ⇒ (~Field τ)]
|
||
#:with RF (mk-ReadsField #'x)
|
||
------------------------
|
||
[⊢ (#%app- x-)
|
||
(⇒ : τ)
|
||
(⇒ ν (RF))])
|
||
|
||
(define-simple-macro (! e ...) (ref e ...))
|
||
|
||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||
;; Ground Dataspace
|
||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||
|
||
;; n.b. this is a blocking operation, so an actor that uses this internally
|
||
;; won't necessarily terminate.
|
||
(define-typed-syntax run-ground-dataspace
|
||
;; TODO : this has the same problem with re-expansion of what's in the τ-c position as spawn
|
||
[(run-ground-dataspace τ-c:type s ...) ≫
|
||
#:fail-unless (flat-type? #'τ-c.norm) "Communication type must be first-order"
|
||
#:mode (communication-type-mode #'τ-c.norm)
|
||
[
|
||
[⊢ s ≫ s- (⇒ : t1)] ...
|
||
[⊢ (dataspace τ-c.norm s- ...) ≫ _ (⇒ : t2)]
|
||
]
|
||
#:with τ-out (strip-outbound #'τ-c.norm)
|
||
-----------------------------------------------------------------------------------
|
||
[⊢ (#%app- syndicate:run-ground (#%app- syndicate:capture-actor-actions (lambda- () (#%app- list- s- ...))))
|
||
(⇒ : (AssertionSet τ-out))]]
|
||
[(run-ground-dataspace s ...) ≫
|
||
[⊢ s ≫ s- (⇒ : t1)] ...
|
||
[⊢ (dataspace s- ...) ≫ _ (⇒ : t2)]
|
||
#:with τ-out (strip-outbound #'τ-c.norm)
|
||
-----------------------------------------------------------------------------------
|
||
[⊢ (#%app- syndicate:run-ground (#%app- syndicate:capture-actor-actions (lambda- () (#%app- list- s- ...))))
|
||
(⇒ : (AssertionSet τ-out))]
|
||
])
|
||
|
||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||
;; Utilities
|
||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||
|
||
(define-typed-syntax print-type
|
||
[(print-type τ:type) ≫
|
||
#:do [(pretty-display (type->strX #'τ.norm))]
|
||
----------------------------------
|
||
[⊢ 0 (⇒ : Int)]]
|
||
[(print-type e) ≫
|
||
[⊢ e ≫ e- (⇒ : τ) (⇒ ν (~effs F ...))]
|
||
#:do [(pretty-display (type->strX #'τ))]
|
||
----------------------------------
|
||
[⊢ e- (⇒ : τ) (⇒ ν (F ...))]])
|
||
|
||
(define-typed-syntax (print-role e) ≫
|
||
[⊢ e ≫ e- (⇒ : τ) (⇒ ν (~effs F ...))]
|
||
#:do [(for ([r (in-syntax #'(F ...))]
|
||
#:when (TypeStartsFacet? r))
|
||
(pretty-display (type->strX r)))]
|
||
----------------------------------
|
||
[⊢ e- (⇒ : τ) (⇒ ν (F ...))])
|
||
|
||
(define-typed-syntax (print-effects e) ≫
|
||
[⊢ e ≫ e- (⇒ : τ) (⇒ ν (~effs F ...))]
|
||
#:do [(for ([f (in-syntax #'(F ...))])
|
||
(pretty-display (type->strX f)))]
|
||
----------------------------------
|
||
[⊢ e- (⇒ : τ) (⇒ ν (F ...))])
|
||
|
||
;; this is mainly for testing
|
||
(define-typed-syntax (role-strings e) ≫
|
||
[⊢ e ≫ e- (⇒ : τ) (⇒ ν (~effs F ...))]
|
||
#:with (s ...) (for/list ([r (in-syntax #'(F ...))]
|
||
#:when (TypeStartsFacet? r))
|
||
(type->strX r))
|
||
----------------------------------------
|
||
[⊢ (#%app- list- (#%datum- . s) ...) (⇒ : (List String))])
|
||
|
||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||
;; LTL Syntax
|
||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||
|
||
(define-type LTL : LTL)
|
||
|
||
(define-for-syntax (LTL? stx)
|
||
(syntax-parse (detach stx KIND-TAG)
|
||
[~LTL #t]
|
||
[_ #f]))
|
||
|
||
(define-type TT : LTL)
|
||
(define-type FF : LTL)
|
||
(define-type Always : LTL -> LTL)
|
||
(define-type Eventually : LTL -> LTL)
|
||
(define-type Until : LTL LTL -> LTL)
|
||
(define-type WeakUntil : LTL LTL -> LTL)
|
||
(define-type Release : LTL LTL -> LTL)
|
||
(define-type Implies : LTL LTL -> LTL)
|
||
(define-type And : LTL * -> LTL)
|
||
(define-type Or : LTL * -> LTL)
|
||
(define-type Not : LTL -> LTL)
|
||
(define-type A : Type -> LTL) ;; Assertions
|
||
(define-type M : Type -> LTL) ;; Messages
|
||
|
||
(define-syntax define-ltl
|
||
(syntax-parser
|
||
[(_ alias:id ltl)
|
||
#:cut
|
||
#:with ltl- (type-eval #'ltl)
|
||
#:fail-unless (LTL? #'ltl-) "expected an LTL formula"
|
||
#:with serialized (serialize-syntax #'ltl-)
|
||
#'(define-syntax- alias
|
||
(make-variable-like-transformer (deserialize-syntax #'serialized)))]
|
||
[(_ (f:id x:id ...) ltl)
|
||
#'(define-syntax- f (mk-type-alias-rewriter #'(x ...) #'ltl))]))
|
||
|
||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||
;; Behavioral Analysis
|
||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||
|
||
(begin-for-syntax
|
||
|
||
(define ID-PHASE 0)
|
||
|
||
(define-syntax (build-id-table stx)
|
||
(syntax-parse stx
|
||
[(_ (~seq key val) ...)
|
||
#'(make-free-id-table (hash (~@ #'key val) ...) #:phase ID-PHASE)]))
|
||
|
||
(define (mk-proto:U . args)
|
||
(proto:U args))
|
||
(define (mk-proto:Branch . args)
|
||
(proto:Branch args))
|
||
|
||
(define TRANSLATION#
|
||
(build-id-table Sends proto:Sends
|
||
Realizes proto:Realizes
|
||
Shares proto:Shares
|
||
Know proto:Know
|
||
Branch mk-proto:Branch
|
||
Effs list
|
||
Asserted proto:Asserted
|
||
Retracted proto:Retracted
|
||
Message proto:Message
|
||
Forget proto:Forget
|
||
Realize proto:Realize
|
||
U* mk-proto:U
|
||
Observe proto:Observe
|
||
List proto:List
|
||
Set proto:Set
|
||
Hash proto:Hash
|
||
OnStart proto:StartEvt
|
||
OnStop proto:StopEvt
|
||
OnDataflow proto:DataflowEvt
|
||
;; Type Varying Assertion Stuff
|
||
ReadsField (lambda (nm) (list))
|
||
--> list
|
||
;; LTL
|
||
TT #t
|
||
FF #f
|
||
Always proto:always
|
||
Eventually proto:eventually
|
||
Until proto:strong-until
|
||
WeakUntil proto:weak-until
|
||
Release proto:release
|
||
Implies proto:ltl-implies
|
||
And proto:&&
|
||
Or proto:||
|
||
Not proto:ltl-not
|
||
A proto:atomic
|
||
M (compose proto:atomic proto:Message)))
|
||
|
||
(define (double-check)
|
||
(for/first ([id (in-dict-keys TRANSLATION#)]
|
||
#:when (false? (identifier-binding id)))
|
||
(pretty-print id)
|
||
(pretty-print (syntax-debug-info id))))
|
||
|
||
;; used for communicating field type/internal message types between synd->proto and VarAssertCompiler
|
||
(define FIELD-TY#-KEY 'FIELD-TY#)
|
||
|
||
(define (synd->proto ty)
|
||
;; (Hashof Symbol (Listof (List Type Type)))
|
||
;; for each VarAssert field name, keep track of the message type associated with each field type
|
||
(define write-field# (make-weak-hash))
|
||
(define field-ty0# (make-weak-hash))
|
||
(define (lookup field-nm field-ty)
|
||
(match (hash-ref write-field# field-nm #f)
|
||
[#f #f]
|
||
[ty#
|
||
#;(printf "got type#: ~a\n" ty#)
|
||
(for/first ([l (in-list ty#)]
|
||
#:when (type=? (first l) field-ty))
|
||
(second l))]))
|
||
|
||
(let convert ([ty (resugar-type ty)])
|
||
(syntax-parse ty
|
||
#:literals (★/t Bind Discard ∀/internal →/internal Role/internal Stop Reacts Actor ActorWithRole
|
||
VarAssert WritesField MakesField)
|
||
[(ctor:id t ...)
|
||
#:when (dict-has-key? TRANSLATION# #'ctor)
|
||
(apply (dict-ref TRANSLATION# #'ctor) (stx-map convert #'(t ...)))]
|
||
[nm:id
|
||
#:when (dict-has-key? TRANSLATION# #'nm)
|
||
(dict-ref TRANSLATION# #'nm)]
|
||
[(Actor _)
|
||
(error "only able to convert actors with roles")]
|
||
[(ActorWithRole _ r)
|
||
(proto:Spawn (convert #'r))]
|
||
[★/t proto:⋆]
|
||
[(Bind t)
|
||
;; TODO - this is debatable handling
|
||
(convert #'t)]
|
||
[Discard
|
||
;; TODO - should prob have a Discard type in proto
|
||
proto:⋆]
|
||
[(∀/internal (X ...) body)
|
||
;; TODO
|
||
(error "unimplemented")]
|
||
[(→/internal ty-in ... ty-out)
|
||
;; TODO
|
||
(error "unimplemented")]
|
||
[(Role/internal (nm) (~alt (~and MF (MakesField . _))
|
||
(~and VA (VarAssert . _))
|
||
body) ...)
|
||
;; need to do VarAsserts first so they update the hash in time for the WriteFields to see
|
||
;; and MakesField before VarAsserts to get the initial type
|
||
(proto:Role (syntax-e #'nm) (stx-map convert #'(MF ... VA ... body ...)))]
|
||
[(Stop nm body ...)
|
||
(proto:Stop (syntax-e #'nm) (stx-map convert #'(body ...)))]
|
||
[(Reacts evt body ...)
|
||
(define converted-body (stx-map convert #'(body ...)))
|
||
(define body+
|
||
(if (= 1 (length converted-body))
|
||
(first converted-body)
|
||
converted-body))
|
||
(proto:Reacts (convert #'evt) body+)]
|
||
[(MakesField nm t t0)
|
||
#;(printf "MakesField: ~a\n" (syntax-e #'nm))
|
||
(hash-set! field-ty0# (syntax-e #'nm) #'t0)
|
||
(list)]
|
||
[(VarAssert nm t1 . ts)
|
||
;; pretty confident that the language forces field declarations to appear before any references
|
||
(define t0 (hash-ref field-ty0# (syntax-e #'nm)))
|
||
(define VA- (type-eval (quasisyntax/loc ty (VarAssertCompiler nm #,t0 t1 . ts))))
|
||
(define type# (syntax-property VA- FIELD-TY#-KEY))
|
||
(hash-set! write-field# (syntax-e #'nm) type#)
|
||
(convert (resugar-type VA-))]
|
||
[(WritesField nm t)
|
||
#;(printf "WritesField ~a\n" #'t)
|
||
#;(pretty-display write-field#)
|
||
(match (lookup (syntax-e #'nm) #'t)
|
||
[#f '()]
|
||
[msg-nm (proto:Realizes (proto:Base (syntax-e msg-nm)))])]
|
||
[t:id
|
||
(proto:Base (syntax-e #'t))]
|
||
[(ctor:id args ...)
|
||
;; assume it's a struct
|
||
(proto:Struct (syntax-e #'ctor) (stx-map convert #'(args ...)))]
|
||
[unrecognized (error (format "unrecognized type: ~a" #'unrecognized))]))))
|
||
|
||
;; need to translate (WritesField x τ) to the appropriate UpdateMsgNm
|
||
(define-typed-syntax (VarAssertCompiler nm t0 t1 ts ...) ≫
|
||
#:with all-ts #'(t1 ts ...)
|
||
;; NB these have been resugared so ~--> won't work, but is in principle the right thing
|
||
;; #:do [(displayln 'AA)
|
||
;; (printf "nm: ~a\n" #'nm)]
|
||
#:with ([_ τf τa] ...) #'all-ts
|
||
;; Relying on synd->proto interpreting each UpdateMsg as a Base type
|
||
#:with ((UpdateMsgNmi VAi) ...) (for/list ([t (in-syntax #'all-ts)]
|
||
[i (in-naturals)])
|
||
(list (format-id #f "Update~aMsg~a" #'nm i)
|
||
(format-id #f "VA~a~a" #'nm i)))
|
||
;; #:do [(displayln 'BB)]
|
||
#:with (role-i-starter ...)
|
||
(for/list ([stx (in-syntax #'((UpdateMsgNmi VAi) ...))]
|
||
[t-a (in-syntax #'(τa ...))])
|
||
(with-syntax ([(myUMN myVA) stx]
|
||
[my-τ-a t-a])
|
||
#'(Reacts (Realize myUMN)
|
||
(Role (myVA)
|
||
(Shares my-τ-a)
|
||
(Reacts (Realize UpdateMsgNmi) (Stop myVA))
|
||
...))))
|
||
;; #:do [(displayln 'CC)]
|
||
;; #:do [(displayln #'t0)
|
||
;; (displayln #'(τf ...))]
|
||
#:with UpdateMsg0 (for/first ([t-a (in-syntax #'(τf ...))]
|
||
[msgi (in-syntax #'(UpdateMsgNmi ...))]
|
||
#:when (type=? #'t0 t-a))
|
||
msgi)
|
||
;; #:do [(printf "UpdateMsg0: ~a\n" (syntax-e #'UpdateMsg0))]
|
||
;; #:with (UpdateMsg0 . _) #'(UpdateMsgNmi ...)
|
||
[[UpdateMsgNmi ≫ UpdateMsgNmi- : Type] ...
|
||
⊢ (Reacts OnStart
|
||
(Role (dispatcher)
|
||
role-i-starter ...
|
||
(Reacts OnStart (Realizes UpdateMsg0))))
|
||
≫ compiled]
|
||
;; #:do [(displayln 'DD)
|
||
;; #;(pretty-display (resugar-type #'compiled))]
|
||
#:do [(define type# (for/list ([tf (in-syntax #'(τf ...))]
|
||
[msg-nm (in-syntax #'(UpdateMsgNmi ...))])
|
||
(list tf msg-nm)))]
|
||
------------------------------------------------------
|
||
[≻ #,(syntax-property #'compiled FIELD-TY#-KEY type#)])
|
||
|
||
(define-typed-syntax (export-roles dest:string e:expr) ≫
|
||
[⊢ e ≫ e- (⇒ : τ) (⇒ ν (~effs F ...))]
|
||
#:do [(with-output-to-file (syntax-e #'dest)
|
||
(thunk (for ([f (in-syntax #'(F ...))]
|
||
#:when (TypeStartsFacet? f))
|
||
(pretty-write (synd->proto f))))
|
||
#:exists 'replace)]
|
||
----------------------------------------
|
||
[⊢ e- (⇒ : τ) (⇒ ν (F ...))])
|
||
|
||
(define-typed-syntax (export-type dest:string τ:type) ≫
|
||
#:do [(with-output-to-file (syntax-e #'dest)
|
||
(thunk (pretty-write (synd->proto #'τ.norm)))
|
||
#:exists 'replace)]
|
||
----------------------------------------
|
||
[⊢ (#%app- void-) (⇒ : ★/t)])
|
||
|
||
(define-typed-syntax (lift+define-role x:id e:expr) ≫
|
||
[⊢ e ≫ e- (⇒ : τ) (⇒ ν (~effs (~and r (~Role (_) _ ...))))]
|
||
;; because turnstile introduces a lot of intdef scopes; ideally, we'd be able to synthesize somethign
|
||
;; with the right module scopes
|
||
#:with x+ (syntax-local-introduce (datum->syntax #f (syntax-e #'x)))
|
||
#:do [(define r- (synd->proto #'r))
|
||
(syntax-local-lift-module-end-declaration #`(define- x+ '#,r-))]
|
||
----------------------------------------
|
||
[⊢ e- (⇒ : τ) (⇒ ν (r))])
|
||
|
||
|
||
;; Type Type -> Bool
|
||
;; (normalized Types)
|
||
(define-for-syntax (simulating-types? ty-impl ty-spec)
|
||
(define ty-impl- (synd->proto ty-impl))
|
||
(define ty-spec- (synd->proto ty-spec))
|
||
(proto:simulates?/report-error ty-impl- ty-spec-))
|
||
|
||
;; Type Type -> Bool
|
||
;; (normalized Types)
|
||
(define-for-syntax (type-has-simulating-subgraphs? ty-impl ty-spec)
|
||
(define ty-impl- (synd->proto ty-impl))
|
||
(define ty-spec- (synd->proto ty-spec))
|
||
(define ans (proto:find-simulating-subgraph/report-error ty-impl- ty-spec-))
|
||
(unless ans
|
||
(pretty-print ty-impl-)
|
||
(pretty-print ty-spec-))
|
||
ans)
|
||
|
||
(define- (ensure-Role! r)
|
||
(unless- (#%app- proto:Role? r)
|
||
(#%app- error- 'check-simulates "expected a Role type, got ~a" r))
|
||
r)
|
||
|
||
(begin-for-syntax
|
||
(define-syntax-class type-or-proto
|
||
#:attributes (role)
|
||
(pattern t:type #:attr role #`(quote- #,(synd->proto #'t.norm)))
|
||
(pattern x:id #:attr role #'(#%app- ensure-Role! x))
|
||
#;(pattern ((~literal quote-) r)
|
||
#:do [(define r- (syntax-e ))]
|
||
#:when (proto:Role? r-)
|
||
#:attr role r-)))
|
||
|
||
(require rackunit)
|
||
|
||
(define-syntax-parser check-simulates
|
||
[(_ τ-impl:type-or-proto τ-spec:type-or-proto)
|
||
(syntax/loc this-syntax
|
||
(check-true (#%app- proto:simulates?/report-error τ-impl.role τ-spec.role)))])
|
||
|
||
(define-syntax-parser check-has-simulating-subgraph
|
||
[(_ τ-impl:type-or-proto τ-spec:type-or-proto)
|
||
(syntax/loc this-syntax
|
||
(check-not-false (#%app- proto:find-simulating-subgraph/report-error τ-impl.role τ-spec.role)))])
|
||
|
||
(define-syntax-parser verify-actors
|
||
[(_ spec actor-ty:type-or-proto ...)
|
||
#:with spec- #`(quote- #,(synd->proto (type-eval #'spec)))
|
||
(syntax/loc this-syntax
|
||
(check-true (#%app- proto:compile+verify spec- (#%app- list- actor-ty.role ...))))])
|
||
|
||
(define-syntax-parser verify-actors/fail
|
||
[(_ spec actor-ty:type-or-proto ...)
|
||
#:with spec- #`(quote- #,(synd->proto (type-eval #'spec)))
|
||
(syntax/loc this-syntax
|
||
(check-false (#%app- proto:compile+verify spec- (#%app- list- actor-ty.role ...))))])
|
||
|
||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||
;; Tests
|
||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||
|
||
(module+ test
|
||
(check-type
|
||
(spawn (U (Observe (Tuple Int ★/t)))
|
||
(start-facet echo
|
||
(on (message (tuple 1 $x:Int))
|
||
#f)))
|
||
: ★/t)
|
||
(check-type (spawn (U (Message (Tuple String Int))
|
||
(Observe (Tuple String ★/t)))
|
||
(start-facet echo
|
||
(on (message (tuple "ping" $x))
|
||
(send! (tuple "pong" x)))))
|
||
: ★/t)
|
||
(typecheck-fail (spawn (U (Message (Tuple String Int))
|
||
(Message (Tuple String String))
|
||
(Observe (Tuple String ★/t)))
|
||
(start-facet echo
|
||
(on (message (tuple "ping" (bind x Int)))
|
||
(send! (tuple "pong" x)))))))
|
||
|
||
;; local definitions
|
||
#;(module+ test
|
||
;; these cause an error in rackunit-typechecking, don't know why :/
|
||
#;(check-type (let ()
|
||
(begin
|
||
(define id : Int 1234)
|
||
id))
|
||
: Int
|
||
-> 1234)
|
||
#;(check-type (let ()
|
||
(define (spawn-cell [initial-value : Int])
|
||
(define id 1234)
|
||
id)
|
||
(typed-app spawn-cell 42))
|
||
: Int
|
||
-> 1234)
|
||
(check-equal? (let ()
|
||
(define id : Int 1234)
|
||
id)
|
||
1234)
|
||
#;(check-equal? (let ()
|
||
(define (spawn-cell [initial-value : Int])
|
||
(define id 1234)
|
||
id)
|
||
(typed-app spawn-cell 42))
|
||
1234))
|