work on proto tie-in

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
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

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))

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