diff --git a/racket/typed/core-types.rkt b/racket/typed/core-types.rkt index ace7ceb..887ec17 100644 --- a/racket/typed/core-types.rkt +++ b/racket/typed/core-types.rkt @@ -170,7 +170,8 @@ #:arity op arity #:arg-variances variances #:isect-desc desc:isect-desc - (~optional (~seq #:extra-info extra-info))) + (~optional (~seq #:extra-info extra-info)) + (~optional (~seq #:implements meths ...))) #:with Name- (mk-- #'Name) #:with NamePat (mk-~ #'Name) #:with NamePat- (mk-~ #'Name-) @@ -181,9 +182,8 @@ (define-type-constructor Name #:arity op arity #:arg-variances variances - #,@(if (attribute extra-info) - #'(#:extra-info extra-info) - #'())) + (~? (~@ #:extra-info extra-info)) + (~? (~@ #:implements meths ...))) (begin-for-syntax (set-type-info! 'Name '#,(attribute desc.val) mk))))])) @@ -201,15 +201,15 @@ (define-syntax (define-container-type stx) (syntax-parse stx [(_ Name:id #:arity op arity - (~optional (~seq #:extra-info extra-info))) + (~optional (~seq #:extra-info extra-info)) + (~optional (~seq #:implements meths ...))) (quasisyntax/loc stx (define-type-constructor+ Name #:arity op arity #:arg-variances mk-covariant #:isect-desc CONTAINER-LIKE - #,@(if (attribute extra-info) - #'(#:extra-info extra-info) - #'())))])) + (~? (~@ #:extra-info extra-info)) + (~? (~@ #:implements meths ...))))])) ;; Define a type constructor that acts like a product: ;; - covariant @@ -217,15 +217,15 @@ (define-syntax (define-product-type stx) (syntax-parse stx [(_ Name:id #:arity op arity - (~optional (~seq #:extra-info extra-info))) + (~optional (~seq #:extra-info extra-info)) + (~optional (~seq #:implements meths ...))) (quasisyntax/loc stx (define-type-constructor+ Name #:arity op arity #:arg-variances mk-covariant #:isect-desc PRODUCT-LIKE - #,@(if (attribute extra-info) - #'(#:extra-info extra-info) - #'())))])) + (~? (~@ #:extra-info extra-info)) + (~? (~@ #:implements meths ...))))])) (define-type Type : Type) @@ -619,6 +619,13 @@ ---------------------- [⊢ (#%app- #,StructName e- ...) (⇒ : (#,TypeCons τ ...))]]))) +(define-for-syntax (resugar-ctor ty) + ;; because typedefs defines 0-arity constructors as base types, + ;; make a custom resugar that always parenthesizes constructors + (syntax-parse ty + [(~Any/new nm args ...) + (cons #'nm (stx-map resugar-type #'(args ...)))])) + (define-syntax (define-constructor stx) (syntax-parse stx [(_ (Cons:id slot:id ...) @@ -643,7 +650,8 @@ (list #'type-tag #'MakeTypeCons #'GetTypeParams)) (define-product-type TypeCons #:arity = #,arity - #:extra-info TypeConsExtraInfo) + #:extra-info TypeConsExtraInfo + #:implements get-resugar-info resugar-ctor) (define-type-alias Alias AliasBody) ... (define-syntax MakeTypeCons (mk-ctor-rewriter #'TypeCons)) (define-syntax GetTypeParams (mk-type-params-fetcher #'TypeCons)) @@ -716,7 +724,8 @@ ;; issue: arity needs to parse as an exact-nonnegative-integer ;; fix: check arity in MakeTypeCons #:arity >= 0 - #:extra-info TypeConsExtraInfo) + #:extra-info TypeConsExtraInfo + #:implements get-resugar-info resugar-ctor) (define-syntax MakeTypeCons (mk-ctor-rewriter #'TypeCons)) (define-syntax GetTypeParams (mk-type-params-fetcher #'TypeCons)) (define-syntax Cons- (mk-constructor-type-rule arity #'orig-struct-info #'TypeCons)) @@ -836,16 +845,6 @@ (for/list ([f (in-list (list* #'ctor (user-ctor-type-ctor val) accs))]) (make-export f (syntax-e f) (syntax-local-phase-level) #f f))])))) -#;(define-provide-syntax (struct-out stx) - (syntax-parse stx - [(_ ctor:id) - (define val (syntax-local-value #'ctor (const #f))) - (unless (user-ctor? val) - (raise-syntax-error (format "not a constructor: ~a" (syntax-e #'ctor)) this-syntax)) - (define accs (user-ctor-field-ids val)) - (for/list ([f (in-list (cons #'ctor accs))]) - (make-export f (syntax-e f) (sub1 (syntax-local-phase-level)) #f f))])) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Conveniences ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; diff --git a/racket/typed/examples/roles/two-buyer-protocol.rkt b/racket/typed/examples/roles/two-buyer-protocol.rkt index 7c8f497..6c576c5 100644 --- a/racket/typed/examples/roles/two-buyer-protocol.rkt +++ b/racket/typed/examples/roles/two-buyer-protocol.rkt @@ -62,14 +62,18 @@ (define-type-alias seller-role (Role (seller) - (Reacts (Asserted (Observe (QuoteT String ★/t))) + (During (Observe (QuoteT String ★/t)) + (Shares (QuoteT String QuoteAnswer))) + #;(Reacts (Asserted (Observe (QuoteT String ★/t))) (Role (_) - (Shares (QuoteT String Int)))))) + ;; 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 _ (field [book (Tuple String Int) (tuple "Catch 22" 22)] [next-order-id Int 10001483]) @@ -93,10 +97,11 @@ (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)))))))) + (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]) @@ -113,10 +118,11 @@ (if (> (ref contribution) (- amount 5)) (stop negotiation (displayln "negotiation failed")) (set! contribution - (+ (ref contribution) (/ (- amount (ref contribution)) 2)))))))])))) + (+ (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))) @@ -146,5 +152,12 @@ (stop purchase))] [discard (begin (displayln "Order Rejected") - (stop purchase))]))))))]))))) + (stop purchase))]))))))])))))) ) + +(module+ test + (check-simulates seller-impl seller-impl) + ;; found a bug in spec, see seller-role above + (check-simulates seller-impl seller-role) + (check-simulates buyer-a-impl buyer-a-impl) + (check-simulates buyer-b-impl buyer-b-impl)) diff --git a/racket/typed/roles.rkt b/racket/typed/roles.rkt index 146b82c..9afa85f 100644 --- a/racket/typed/roles.rkt +++ b/racket/typed/roles.rkt @@ -633,19 +633,25 @@ [(_ (~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 Spawns proto:Spawn Sends proto:Sends Realizes proto:Realizes Shares proto:Shares Know proto:Know - Branch proto:Branch + Branch mk-proto:Branch + Effs list Asserted proto:Asserted Retracted proto:Retracted Message proto:Message Forget proto:Forget Realize proto:Realize - U* proto:U + U* mk-proto:U Observe proto:Observe List proto:List Set proto:Set