typed: add default types to constructor fields and alternate actor
typechecking path Default types for fields means we can elaborate a binding pattern without a current communication type. Then a potential communication type can be the output of type checking an actor, that is checked when it is instantiated, such as in a dataspace or other context.
This commit is contained in:
Sam Caldwell
parent
d2e753d303
commit
b9f655766f
|
|
@ -264,8 +264,15 @@
|
|||
(quasisyntax/loc pat
|
||||
(tuple #,@(stx-map elaborate-pattern #'(p ...))))]
|
||||
[(~constructor-exp ctor p ...)
|
||||
(define field-tys (ctor-field-tys #'ctor))
|
||||
(define sub-pats
|
||||
(for/list ([field-pat (in-syntax #'(p ...))]
|
||||
[field-ty? (in-list field-tys)])
|
||||
(if field-ty?
|
||||
(elaborate-pattern/with-type field-pat field-ty?)
|
||||
(elaborate-pattern field-pat))))
|
||||
(quasisyntax/loc pat
|
||||
(ctor #,@(stx-map elaborate-pattern #'(p ...))))]
|
||||
(ctor #,@sub-pats))]
|
||||
[e:expr
|
||||
#'e]))
|
||||
|
||||
|
|
|
|||
|
|
@ -663,7 +663,18 @@
|
|||
(pattern (~seq #:type-constructor TypeCons:id))
|
||||
(pattern (~seq) #:attr TypeCons #f))
|
||||
|
||||
(struct user-ctor (typed-ctor untyped-ctor type-tag type-ctor field-ids)
|
||||
(define-syntax-class slot-decl
|
||||
#:attributes (name type)
|
||||
(pattern name:id #:attr type #f)
|
||||
(pattern [name:id (~optional (~datum :)) type]))
|
||||
|
||||
;; typed-ctor : ID; the name of function implementing the type rule
|
||||
;; untyped-ctor : ID; the name of the constructor for the (run time) struct
|
||||
;; type-tag : ID; a unique tag for instances of this type
|
||||
;; type-ctor : ID: the name of the type constructor for instances of this struct
|
||||
;; field-ids : (Listof ID): the names of each field accessor
|
||||
;; field-tys : (Listof (U #f Syntax)): the default type (serialized) of each field, if known
|
||||
(struct user-ctor (typed-ctor untyped-ctor type-tag type-ctor field-ids field-tys)
|
||||
#:property prop:procedure
|
||||
(lambda (v stx)
|
||||
(define transformer (user-ctor-typed-ctor v))
|
||||
|
|
@ -675,11 +686,11 @@
|
|||
(define-syntax (define-constructor* stx)
|
||||
(syntax-parse stx
|
||||
#:datum-literals (:)
|
||||
[(_ (Cons:id : TyCons:id slot:id ...) clause ...)
|
||||
[(_ (Cons:id : TyCons:id slot:slot-decl ...) clause ...)
|
||||
#'(define-constructor (Cons slot ...)
|
||||
#:type-constructor TyCons
|
||||
clause ...)]
|
||||
[(_ (Cons:id slot:id ...) clause ...)
|
||||
[(_ (Cons:id slot:slot-decl ...) clause ...)
|
||||
#:with TyCons ((current-type-constructor-convention) #'Cons)
|
||||
(syntax/loc stx
|
||||
(define-constructor (Cons slot ...)
|
||||
|
|
@ -711,7 +722,7 @@
|
|||
|
||||
(define-syntax (define-constructor stx)
|
||||
(syntax-parse stx
|
||||
[(_ (Cons:id slot:id ...)
|
||||
[(_ (Cons:id slot:slot-decl ...)
|
||||
ty-cons:type-constructor-decl
|
||||
(~seq #:with
|
||||
Alias AliasBody) ...)
|
||||
|
|
@ -721,14 +732,18 @@
|
|||
#:with TypeConsExpander (format-id #'TypeCons "~~~a" #'TypeCons)
|
||||
#:with TypeConsExtraInfo (format-id #'TypeCons "~a-extra-info" #'TypeCons)
|
||||
#:with (StructName Cons- type-tag) (generate-temporaries #'(Cons Cons Cons))
|
||||
#:with (accessor ...) (for/list ([slot-name (in-syntax #'(slot ...))])
|
||||
#:with (accessor ...) (for/list ([slot-name (in-syntax #'(slot.name ...))])
|
||||
(format-id slot-name "~a-~a" #'Cons slot-name))
|
||||
#:with (accessor- ...) (for/list ([slot-name (in-syntax #'(slot ...))])
|
||||
#:with (accessor- ...) (for/list ([slot-name (in-syntax #'(slot.name ...))])
|
||||
(format-id #'StructName "~a-~a" #'StructName slot-name))
|
||||
#:with (acc-defs ...) (mk-accessors #'(accessor ...) #'(accessor- ...) #'TypeCons #'(slot ...))
|
||||
#:with (acc-defs ...) (mk-accessors #'(accessor ...) #'(accessor- ...) #'TypeCons #'(slot.name ...))
|
||||
#:with (field-ty? ...) (for/list ([ty? (in-list (attribute slot.type))])
|
||||
(if ty?
|
||||
(serialize-syntax (type-eval ty?))
|
||||
#'#f))
|
||||
(define arity (stx-length #'(slot ...)))
|
||||
#`(begin-
|
||||
(struct- StructName (slot ...) #:reflection-name 'Cons #:transparent)
|
||||
(struct- StructName (slot.name ...) #:reflection-name 'Cons #:transparent)
|
||||
(define-for-syntax (TypeConsExtraInfo stx)
|
||||
(list #'type-tag #'MakeTypeCons #'GetTypeParams))
|
||||
(define-product-type TypeCons
|
||||
|
|
@ -739,9 +754,14 @@
|
|||
(define-syntax MakeTypeCons (mk-ctor-rewriter #'TypeCons))
|
||||
(define-syntax GetTypeParams (mk-type-params-fetcher #'TypeCons))
|
||||
(define-syntax Cons
|
||||
(user-ctor #'Cons- #'StructName 'type-tag #'TypeCons (list #'accessor ...)))
|
||||
(user-ctor #'Cons-
|
||||
#'StructName
|
||||
'type-tag
|
||||
#'TypeCons
|
||||
(list #'accessor ...)
|
||||
(list #'field-ty? ...)))
|
||||
(define-syntax Cons- (mk-constructor-type-rule #,arity #'StructName #'TypeCons))
|
||||
#,@(mk-accessors #'(accessor ...) #'(accessor- ...) #'TypeCons #'(slot ...)))]))
|
||||
acc-defs ...)]))
|
||||
|
||||
(define-for-syntax (mk-accessors accessors accessors- TypeCons slots)
|
||||
(for/list ([accessor (in-syntax accessors)]
|
||||
|
|
@ -750,13 +770,16 @@
|
|||
(quasisyntax/loc TypeCons
|
||||
(define-typed-variable-rename+ #,accessor ≫ #,accessor- : (∀+ #,slots (→fn (#,TypeCons #,@slots) #,slot))))))
|
||||
|
||||
(define-for-syntax ((define-struct-accs accs/rev TypeCons lib) stx)
|
||||
(define-for-syntax ((define-struct-accs accs/rev field-accs? TypeCons lib) stx)
|
||||
(syntax-parse stx
|
||||
[(_ ucons:id)
|
||||
(define accs (cleanup-accs #'ucons accs/rev))
|
||||
(define accs- (map mk-- accs))
|
||||
(define cleaned-accs (cleanup-accs #'ucons accs/rev))
|
||||
(define accs (if (empty? field-accs?)
|
||||
cleaned-accs
|
||||
(format-all #'ucons field-accs?)))
|
||||
(define accs- (map mk-- cleaned-accs))
|
||||
(define slots (generate-temporaries accs))
|
||||
(define renames (for/list ([acc (in-list accs)]
|
||||
(define renames (for/list ([acc (in-list cleaned-accs)]
|
||||
[acc- (in-list accs-)])
|
||||
#`[#,acc #,acc-]))
|
||||
(quasisyntax/loc TypeCons
|
||||
|
|
@ -764,10 +787,13 @@
|
|||
(require- (only-in- #,lib #,@renames))
|
||||
#,@(mk-accessors accs accs- TypeCons slots)))]))
|
||||
|
||||
(define-for-syntax (cleanup-accs ucons accs/rev)
|
||||
(for/list ([acc (in-list (reverse accs/rev))])
|
||||
(define-for-syntax (format-all ucons accs)
|
||||
(for/list ([acc (in-list accs)])
|
||||
(format-id ucons "~a" (syntax-e acc))))
|
||||
|
||||
(define-for-syntax (cleanup-accs ucons accs/rev)
|
||||
(format-all ucons (reverse accs/rev)))
|
||||
|
||||
;; (require-struct chicken #:as Chicken #:from "some-mod.rkt") will
|
||||
;; - extract the struct-info for chicken, and ensure that it is immutable, has a set number of fields
|
||||
;; - determine the number of slots, N, chicken has
|
||||
|
|
@ -777,34 +803,66 @@
|
|||
;; 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
|
||||
(~optional (~seq slot:slot-decl ...))
|
||||
(~optional (~and omit-accs #:omit-accs)))
|
||||
;; TBH I'm not sure why I don't need to SLIAB TypeCons and Cons-
|
||||
(with-syntax* ([TypeCons #'ty-cons]
|
||||
[MakeTypeCons (format-id #'TypeCons "make-~a" #'TypeCons)]
|
||||
[GetTypeParams (format-id #'TypeCons "get-~a-type-params" #'TypeCons)]
|
||||
[TypeConsExpander (format-id #'TypeCons "~~~a" #'TypeCons)]
|
||||
[TypeConsExtraInfo (format-id #'TypeCons "~a-extra-info" #'TypeCons)]
|
||||
[Cons- (format-id #'ucons "~a/checked" #'ucons)]
|
||||
[orig-struct-info (generate-temporary #'ucons)]
|
||||
[type-tag (generate-temporary #'ucons)])
|
||||
(quasisyntax/loc stx
|
||||
(begin-
|
||||
(require- (only-in- lib [ucons orig-struct-info]))
|
||||
(begin-for-syntax
|
||||
(define info (syntax-local-value #'orig-struct-info))
|
||||
(unless (struct-info? info)
|
||||
(raise-syntax-error #f "expected struct" #'#,stx #'ucons))
|
||||
(match-define (list desc cons pred accs/rev muts sup) (extract-struct-info info))
|
||||
(when (and (cons? accs/rev) (false? (last accs/rev)))
|
||||
(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 arity (length accs/rev))
|
||||
)
|
||||
(define-syntax finish-type-defs
|
||||
(finish-require-struct-typedef #'lib #'Cons- #'TypeConsExtraInfo #'type-tag #'MakeTypeCons #'GetTypeParams #'orig-struct-info #'accs/rev arity #,(attribute omit-accs)))
|
||||
(finish-type-defs ucons TypeCons)
|
||||
)))]))
|
||||
#:with TypeCons #'ty-cons
|
||||
#:with MakeTypeCons (format-id #'TypeCons "make-~a" #'TypeCons)
|
||||
#:with GetTypeParams (format-id #'TypeCons "get-~a-type-params" #'TypeCons)
|
||||
#:with TypeConsExpander (format-id #'TypeCons "~~~a" #'TypeCons)
|
||||
#:with TypeConsExtraInfo (format-id #'TypeCons "~a-extra-info" #'TypeCons)
|
||||
#:with Cons- (format-id #'ucons "~a/checked" #'ucons)
|
||||
#:with orig-struct-info (generate-temporary #'ucons)
|
||||
#:with type-tag (generate-temporary #'ucons)
|
||||
#:with (field-ty? ...) (for/list ([ty? (in-list (attribute slot.type))])
|
||||
(if ty?
|
||||
#`#,(serialize-syntax (type-eval ty?))
|
||||
#f))
|
||||
#:with (field-acc ...) (for/list ([name? (in-list (attribute slot.name))])
|
||||
(if name?
|
||||
(format-id #'ucons "~a-~a" #'ucons name?)
|
||||
#f))
|
||||
(quasisyntax/loc stx
|
||||
(begin-
|
||||
(require- (only-in- lib [ucons orig-struct-info]))
|
||||
(begin-for-syntax
|
||||
(define info (syntax-local-value #'orig-struct-info))
|
||||
(unless (struct-info? info)
|
||||
(raise-syntax-error #f "expected struct" #'#,stx #'ucons))
|
||||
(match-define (list desc cons pred accs/rev muts sup) (extract-struct-info info))
|
||||
(when (and (cons? accs/rev) (false? (last accs/rev)))
|
||||
(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 arity (length accs/rev))
|
||||
(define field-tys (list #'field-ty? ...))
|
||||
(define field-accs? (list #'field-acc ...))
|
||||
(define slots-given (length field-tys))
|
||||
(unless (or (zero? slots-given)
|
||||
(equal? slots-given arity))
|
||||
(raise-syntax-error
|
||||
#f
|
||||
(format "incorrect number of slots specified, given ~a expected ~a" slots-given arity)
|
||||
#'#,stx
|
||||
#'(slot ...)))
|
||||
)
|
||||
(define-syntax finish-type-defs
|
||||
(finish-require-struct-typedef #'lib
|
||||
#'Cons-
|
||||
#'TypeConsExtraInfo
|
||||
#'type-tag
|
||||
#'MakeTypeCons
|
||||
#'GetTypeParams
|
||||
#'orig-struct-info
|
||||
#'accs/rev
|
||||
arity
|
||||
#,(attribute omit-accs)
|
||||
#'field-tys
|
||||
#'field-accs?
|
||||
#;(list #'field-acc ...)))
|
||||
(finish-type-defs ucons TypeCons)
|
||||
))]))
|
||||
|
||||
;; This is so that the arity of the struct can be included in the generated typedef
|
||||
(define-for-syntax ((finish-require-struct-typedef lib
|
||||
|
|
@ -816,10 +874,15 @@
|
|||
orig-struct-info
|
||||
accs/rev
|
||||
arity
|
||||
omit-accs?)
|
||||
omit-accs?
|
||||
field-tys
|
||||
field-accs?)
|
||||
stx)
|
||||
(syntax-parse stx
|
||||
[(_ ucons:id TypeCons:id)
|
||||
#:with field-accs #`(if (empty? #,field-accs?)
|
||||
(cleanup-accs #'ucons #,accs/rev)
|
||||
(format-all #'ucons #,field-accs?))
|
||||
(quasisyntax/loc #'ucons
|
||||
(begin-
|
||||
(define-for-syntax (#,TypeConsExtraInfo stx)
|
||||
|
|
@ -832,12 +895,17 @@
|
|||
(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)))
|
||||
(user-ctor #'#,Cons-
|
||||
#'#,orig-struct-info
|
||||
'#,type-tag
|
||||
#'TypeCons
|
||||
field-accs
|
||||
#,field-tys))
|
||||
#,(unless omit-accs?
|
||||
(quasisyntax/loc #'ucons
|
||||
(begin-
|
||||
(define-syntax mk-struct-accs
|
||||
(define-struct-accs #,accs/rev #'TypeCons #'#,lib))
|
||||
(define-struct-accs #,accs/rev #,field-accs? #'TypeCons #'#,lib))
|
||||
(mk-struct-accs ucons))))))]))
|
||||
|
||||
(begin-for-syntax
|
||||
|
|
@ -900,7 +968,15 @@
|
|||
;; requires (ctor-id? stx)
|
||||
;; fetch the type tag
|
||||
(define (ctor-type-tag stx)
|
||||
(user-ctor-type-tag (syntax-local-value stx (const #f)))))
|
||||
(user-ctor-type-tag (syntax-local-value stx (const #f))))
|
||||
|
||||
;; requires (ctor-id? stx)
|
||||
;; fetch the field types
|
||||
(define (ctor-field-tys stx)
|
||||
(define tys (user-ctor-field-tys (syntax-local-value stx (const #f))))
|
||||
(for/list ([ty? (in-list tys)])
|
||||
(and ty? (deserialize-syntax ty?))))
|
||||
)
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;; Require & Provide
|
||||
|
|
@ -922,9 +998,13 @@
|
|||
|
||||
(define-syntax-class struct-require-clause
|
||||
#:datum-literals (:)
|
||||
#:attributes (Cons TyCons omit-accs)
|
||||
(pattern [#:struct Cons:id #:as TyCons:id (~optional (~and omit-accs #:omit-accs))])
|
||||
(pattern [#:struct Cons:id (~optional (~and omit-accs #:omit-accs))]
|
||||
#:attributes (Cons TyCons omit-accs [slot 1] [slot.name 1] [slot.type 1])
|
||||
(pattern [#:struct Cons:id #:as TyCons:id
|
||||
(~optional (~seq slot:slot-decl ...))
|
||||
(~optional (~and omit-accs #:omit-accs))])
|
||||
(pattern [#:struct Cons:id
|
||||
(~optional (~seq slot:slot-decl ...))
|
||||
(~optional (~and omit-accs #:omit-accs))]
|
||||
#:attr TyCons ((current-type-constructor-convention) #'Cons)))
|
||||
)
|
||||
|
||||
|
|
@ -941,7 +1021,10 @@
|
|||
#:with (name- ...) (format-ids "~a-" #'(name ...))
|
||||
(syntax/loc stx
|
||||
(begin-
|
||||
(require-struct struct-clause.Cons #:as struct-clause.TyCons #:from lib (~? struct-clause.omit-accs)) ...
|
||||
(require-struct struct-clause.Cons #:as struct-clause.TyCons
|
||||
#:from lib
|
||||
(~? (~@ struct-clause.slot ...))
|
||||
(~? struct-clause.omit-accs)) ...
|
||||
opaque-clause.type-definition ...
|
||||
(require (only-in lib [name name-] ...))
|
||||
(define-syntax name
|
||||
|
|
|
|||
|
|
@ -386,7 +386,7 @@
|
|||
"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->str #'τ-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"
|
||||
|
|
@ -402,11 +402,33 @@
|
|||
#:do [(define τc (current-communication-type))]
|
||||
#:when τc
|
||||
----------------------------------------
|
||||
[≻ (spawn #,τc s)]])
|
||||
[≻ (spawn #,τc s)]]
|
||||
[(spawn s) ≫
|
||||
[⊢ (block s) ≫ s- (⇒ ν-ep (~effs)) (⇒ ν-s (~effs)) (⇒ ν-f (~effs τ-f ...))]
|
||||
;; TODO: s shouldn't refer to facets or fields!
|
||||
#:fail-unless (and (stx-andmap Role? #'(τ-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 (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))
|
||||
#:with τ-i/o (pattern-matching-assertions #'τ-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 ...))
|
||||
#: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 ...))
|
||||
#:fail-unless (<: #'τ-a #'τ-final)
|
||||
"Spawned actors not valid in dataspace"
|
||||
----------------------------------------
|
||||
[⊢ (syndicate:spawn (syndicate:on-start s-)) (⇒ : ★/t)
|
||||
(⇒ ν-s (τ-final))]])
|
||||
|
||||
;; (Listof Type) -> String
|
||||
(define-for-syntax (tys->str tys)
|
||||
(string-join (map type->str tys) ",\n"))
|
||||
(string-join (map type->strX tys) ",\n"))
|
||||
|
||||
;; Type Type -> String
|
||||
(define-for-syntax (make-output-error-message τ-o τ-c)
|
||||
|
|
@ -425,11 +447,12 @@
|
|||
|
||||
;; Type Type Type -> String
|
||||
(define-for-syntax (make-actor-error-message τ-i τ-o τ-c)
|
||||
(define mismatches (find-surprising-inputs τ-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)
|
||||
(define-for-syntax (find-surprising-inputs τ-i τ-o τ-c surprising?)
|
||||
(define incoming (∩ (strip-? τ-o) τ-c))
|
||||
;; Type -> (Listof Type)
|
||||
(let loop ([ty incoming])
|
||||
|
|
@ -438,44 +461,56 @@
|
|||
(apply append (map loop (syntax->list #'(τ ...))))]
|
||||
[_
|
||||
(cond
|
||||
[(project-safe? ty τ-i)
|
||||
'()]
|
||||
[(surprising? ty τ-i)
|
||||
(list ty)]
|
||||
[else
|
||||
(list ty)])])))
|
||||
(list)])])))
|
||||
|
||||
(define-typed-syntax (dataspace τ-c:type s ...) ≫
|
||||
#:fail-unless (flat-type? #'τ-c.norm) "Communication type must be first-order"
|
||||
#:mode (communication-type-mode #'τ-c.norm)
|
||||
[
|
||||
[⊢ s ≫ s- (⇒ ν-ep (~effs)) (⇒ ν-s (~effs τ-s ...)) (⇒ ν-f (~effs))] ...
|
||||
]
|
||||
#:with τ-actor (mk-Actor- #'(τ-c.norm))
|
||||
#:do [(define errs (for/list ([t (in-syntax #'(τ-s ... ...))]
|
||||
#: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))])
|
||||
(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- (⇒ ν-ep (~effs)) (⇒ ν-s (~effs τ-s ...)) (⇒ ν-f (~effs))] ...
|
||||
]
|
||||
#:with τ-actor (mk-Actor- #'(τ-c.norm))
|
||||
#:do [(define errs (for/list ([t (in-syntax #'(τ-s ... ...))]
|
||||
#: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- (⇒ ν-ep (~effs)) (⇒ ν-s (~effs τ-s ...)) (⇒ ν-f (~effs))] ...
|
||||
#:cut
|
||||
#:with ((~AnyActor τc/spawned) ...) #'(τ-s ... ...)
|
||||
#: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; found the following mismatches:\n")
|
||||
(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->str #'τ))
|
||||
(printf "Actor with communication type ~a:\n" (type->strX #'τ))
|
||||
(cond
|
||||
[(<: #'τ tc)
|
||||
(define msg (make-actor-error-message #'τ #'τ 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))
|
||||
|
|
@ -666,17 +701,26 @@
|
|||
|
||||
;; n.b. this is a blocking operation, so an actor that uses this internally
|
||||
;; won't necessarily terminate.
|
||||
(define-typed-syntax (run-ground-dataspace τ-c:type s ...) ≫
|
||||
;;#:fail-unless (flat-type? #'τ-c.norm) "Communication type must be first-order"
|
||||
#:mode (communication-type-mode #'τ-c.norm)
|
||||
[
|
||||
(define-typed-syntax run-ground-dataspace
|
||||
[(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 τ-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))])
|
||||
[⊢ (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
|
||||
|
|
|
|||
|
|
@ -0,0 +1,41 @@
|
|||
#lang typed/syndicate
|
||||
|
||||
(require rackunit/turnstile)
|
||||
|
||||
(define-constructor* (run [distance : Int] [windy? : Bool]))
|
||||
|
||||
(check-type
|
||||
(spawn
|
||||
(start-facet runner
|
||||
(assert (run 5 #t))))
|
||||
: ★/t)
|
||||
|
||||
(check-type
|
||||
(spawn
|
||||
(start-facet longer
|
||||
(on (asserted (run $d $w?))
|
||||
(printf "run ~a ~a\n" (add1 d) (if w? "brr" "")))))
|
||||
: ★/t)
|
||||
|
||||
(check-type
|
||||
(dataspace
|
||||
(spawn
|
||||
(start-facet runner
|
||||
(assert (run 5 #t))))
|
||||
(spawn
|
||||
(start-facet longer
|
||||
(on (asserted (run $d $w?))
|
||||
(printf "run ~a ~a\n" (add1 d) (if w? "brr" ""))))))
|
||||
: ★/t)
|
||||
|
||||
(typecheck-fail
|
||||
(dataspace
|
||||
(spawn
|
||||
(start-facet runner
|
||||
;; NB
|
||||
(assert (run "FAR" #t))))
|
||||
(spawn
|
||||
(start-facet longer
|
||||
(on (asserted (run $d $w?))
|
||||
(printf "run ~a ~a\n" (add1 d) (if w? "brr" ""))))))
|
||||
#:verb-msg "unprepared to handle inputs: (RunT String Bool)")
|
||||
|
|
@ -0,0 +1,12 @@
|
|||
#lang typed/syndicate
|
||||
|
||||
(require rackunit/turnstile)
|
||||
|
||||
(require/typed "struct-provider.rkt"
|
||||
[#:struct donkey [weight : Int] [grey? : Bool]])
|
||||
|
||||
(check-type (donkey 5 #t)
|
||||
: (DonkeyT Int Bool))
|
||||
|
||||
(check-type (donkey-grey? (donkey 5 #t))
|
||||
: Bool)
|
||||
|
|
@ -0,0 +1,5 @@
|
|||
#lang racket
|
||||
|
||||
(struct donkey (weight stubborn?) #:transparent)
|
||||
|
||||
(provide (struct-out donkey))
|
||||
Loading…
Reference in New Issue