first bit of linking proto analysis into language

racket/typed/core-types.rkt

@@ -3,7 +3,10 @@
 (provide (except-out (all-defined-out) → ∀ Role)
          (rename-out [→+ →]
                      [∀+ ∀]
-                     [Role+Body Role])
+                     [Role+Body Role]
+                     [Role Role/internal]
+                     [∀ ∀/internal]
+                     [→ →/internal])
          (for-syntax (except-out (all-defined-out) ~→ ~∀ ~Role)
                      (rename-out [~→+ ~→]
                                  [~∀+ ~∀]
@@ -712,7 +715,7 @@
         #'(~and (cons . rst)
                 (~fail #:unless (ctor-id? #'cons)))])))
 
-  (define (inspect t)
+  #;(define (inspect t)
     (syntax-parse t
       [(~constructor-type tag t ...)
        (list (syntax-e #'tag) (stx-map type->str #'(t ...)))]))

racket/typed/examples/roles/bank-account.rkt

@@ -26,16 +26,19 @@
 (define-type-alias account-manager-role
   (Role (account-manager)
         (Shares Account)
-        (Reacts (Know Deposit))))
+        (Reacts (Asserted Deposit))))
 
 (define-type-alias client-role
   (Role (client)
-        (Reacts (Know Account))))
+        (Reacts (Asserted Account))))
+
+(check-simulates client-role client-role)
+(check-simulates client-role account-manager-role)
 
 (run-ground-dataspace ds-type
 
   (spawn ds-type
-    (print-role
+    (export-roles "account-manager-role.rktd"
     (start-facet account-manager
       (field [balance Int 0])
       (assert (account (ref balance)))

racket/typed/proto.rkt

@@ -20,26 +20,26 @@
 ;;   - (Sends τ)
 ;;   - (Realizes τ)
 ;;   - (Stop FacetName Body)
-(struct Role (nm eps) #:transparent)
-(struct Spawn (ty) #:transparent)
-(struct Sends (ty) #:transparent)
-(struct Realizes (ty) #:transparent)
-(struct Stop (nm body) #:transparent)
+(struct Role (nm eps) #:prefab)
+(struct Spawn (ty) #:prefab)
+(struct Sends (ty) #:prefab)
+(struct Realizes (ty) #:prefab)
+(struct Stop (nm body) #:prefab)
 
 ;; a EP is one of
 ;;   - (Reacts D Body), describing an event handler
 ;;   - (Shares τ), describing an assertion
 ;;   - (Know τ), describing an internal assertion
-(struct Reacts (evt body) #:transparent)
-(struct Shares (ty) #:transparent)
-(struct Know (ty) #:transparent)
+(struct Reacts (evt body) #:prefab)
+(struct Shares (ty) #:prefab)
+(struct Know (ty) #:prefab)
 
 ;; a Body describes actions carried out in response to some event, and
 ;; is one of
 ;;   - T
 ;;   - (Listof Body)
 ;;   - (Branch (Listof Body))
-(struct Branch (arms) #:transparent)
+(struct Branch (arms) #:prefab)
 
 ;; a D is one of
 ;;   - (Asserted τ), reaction to assertion
@@ -51,11 +51,11 @@
 ;;   - StartEvt, reaction to facet startup
 ;;   - StopEvt, reaction to facet shutdown
 ;;   - DataflowEvt, reaction to field updates
-(struct Asserted (ty) #:transparent)
-(struct Retracted (ty) #:transparent)
-(struct Message (ty) #:transparent)
-(struct Forget (ty) #:transparent)
-(struct Realize (ty) #:transparent)
+(struct Asserted (ty) #:prefab)
+(struct Retracted (ty) #:prefab)
+(struct Message (ty) #:prefab)
+(struct Forget (ty) #:prefab)
+(struct Realize (ty) #:prefab)
 (define StartEvt 'Start)
 (define StopEvt 'Stop)
 (define DataflowEvt 'Dataflow)
@@ -68,8 +68,8 @@
 ;; specified facet,
 ;;   - (StartOf FacetName)
 ;;   - (StopOf FacetName)
-(struct StartOf (fn) #:transparent)
-(struct StopOf (fn) #:transparent)
+(struct StartOf (fn) #:prefab)
+(struct StopOf (fn) #:prefab)
 
 ;; NOTE: because I'm adding D+ after writing a bunch of code using only D,
 ;; expect inconsistencies in signatures and names
@@ -84,17 +84,17 @@
 ;;   - ⋆
 ;;   - (Base Symbol)
 ;;   - (internal-label Symbol τ)
-(struct U (tys) #:transparent)
-(struct Struct (nm tys) #:transparent)
-(struct Observe (ty) #:transparent)
-(struct List (ty) #:transparent)
-(struct Set (ty) #:transparent)
-(struct Hash (ty-k ty-v) #:transparent)
-(struct Mk⋆ () #:transparent)
-(struct internal-label (actor-id ty) #:transparent)
+(struct U (tys) #:prefab)
+(struct Struct (nm tys) #:prefab)
+(struct Observe (ty) #:prefab)
+(struct List (ty) #:prefab)
+(struct Set (ty) #:prefab)
+(struct Hash (ty-k ty-v) #:prefab)
+(struct Mk⋆ () #:prefab)
+(struct internal-label (actor-id ty) #:prefab)
 ;; TODO this might be a problem when used as a match pattern
 (define ⋆ (Mk⋆))
-(struct Base (name) #:transparent)
+(struct Base (name) #:prefab)
 (define Int (Base 'Int))
 (define String (Base 'String))
 (define Bool (Base 'Bool))

racket/typed/roles.rkt

@@ -62,6 +62,8 @@
          (all-from-out "either.rkt")
          ;; DEBUG and utilities
          print-type print-role role-strings
+         ;; Behavioral Roles
+         export-roles check-simulates
          ;; Extensions
          match cond
          submod for-syntax for-meta only-in except-in
@@ -89,6 +91,9 @@
 (require (postfix-in - racket/list))
 (require (postfix-in - racket/set))
 
+(require (for-syntax (prefix-in proto: "proto.rkt")
+                     syntax/id-table))
+
 (module+ test
   (require rackunit)
   (require rackunit/turnstile))
@@ -614,6 +619,95 @@
   ----------------------------------------
   [⊢ (#%app- list- (#%datum- . s) ...) (⇒ : (List String))])
 
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; 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 TRANSLATION#
+    (build-id-table Spawns proto:Spawn
+                    Sends proto:Sends
+                    Realizes proto:Realizes
+                    Shares proto:Shares
+                    Know proto:Know
+                    Branch proto:Branch
+                    Asserted proto:Asserted
+                    Retracted proto:Retracted
+                    Message proto:Message
+                    Forget proto:Forget
+                    Realize proto:Realize
+                    U* proto:U
+                    Observe proto:Observe
+                    List proto:List
+                    Set proto:Set
+                    Hash proto:Hash))
+
+  (define (double-check)
+    (for/first ([id (in-dict-keys TRANSLATION#)]
+                #:when (false? (identifier-binding id)))
+      (pretty-print id)
+      (pretty-print (syntax-debug-info id))))
+
+  (define (synd->proto ty)
+    (let convert ([ty (resugar-type ty)])
+      (syntax-parse ty
+        #:literals (★/t Discard ∀/internal →/internal Role/internal Stop Reacts)
+        [(ctor:id t ...)
+         #:when (dict-has-key? TRANSLATION# #'ctor)
+         (apply (dict-ref TRANSLATION# #'ctor) (stx-map convert #'(t ...)))]
+        [★/t proto:⋆]
+        [Discard proto:⋆] ;; TODO - should prob have a Discard type in proto
+        [(∀/internal (X ...) body)
+         ;; TODO
+         (error "unimplemented")]
+        [(→/internal ty-in ... ty-out)
+         ;; TODO
+         (error "unimplemented")]
+        [(Role/internal (nm) body ...)
+         (proto:Role (syntax-e #'nm) (stx-map convert #'(body ...)))]
+        [(Stop nm body ...)
+         (proto:Role (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+)]
+        [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))]))))
+
+(define-typed-syntax (export-roles dest:string e:expr) ≫
+  [⊢ e ≫ e- (⇒ : τ) (⇒ ν-ep (~effs eps ...)) (⇒ ν-f (~effs fs ...)) (⇒ ν-s (~effs ss ...))]
+  #:do [(with-output-to-file (syntax-e #'dest)
+          (thunk (for ([f (in-syntax #'(fs ...))])
+                   (pretty-write (synd->proto f))))
+          #:exists 'replace)]
+  ----------------------------------------
+  [⊢ e- (⇒ : τ) (⇒ ν-ep (eps ...)) (⇒ ν-f (fs ...)) (⇒ ν-s (ss ...))])
+
+(define-syntax-parser check-simulates
+  [(_ τ-impl:type τ-spec:type)
+  (define τ-impl- (synd->proto #'τ-impl.norm))
+  (define τ-spec- (synd->proto #'τ-spec.norm))
+  (pretty-print τ-impl-)
+  (pretty-print τ-spec-)
+  (unless (proto:simulates? τ-impl- τ-spec-)
+    (raise-syntax-error #f "type doesn't simulate spec" this-syntax))
+  #'(#%app- void-)])
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Tests
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;