preserve sharing in serializer

fix the serializer

racket/syndicate/actor.rkt

@@ -409,7 +409,6 @@
     [(_ [id:id init maybe-contract ...] ...)
      (quasisyntax/loc stx
        (begin
-         (ensure-in-endpoint-context! 'field)
          (when (and (in-script?) (pair? (current-facet-id)))
            (error 'field
                   "~a: Cannot declare fields in a script; are you missing a (react ...)?"
@@ -488,17 +487,13 @@
   (syntax-parse stx
     [(_ script ...)
      (quasisyntax/loc stx
-       (begin
-         (ensure-in-endpoint-context! 'on-start)
-         (schedule-script! (lambda () (begin/void-default script ...)))))]))
+       (schedule-script! (lambda () (begin/void-default script ...))))]))
 
 (define-syntax (on-stop stx)
   (syntax-parse stx
     [(_ script ...)
      (quasisyntax/loc stx
-       (begin
-         (ensure-in-endpoint-context! 'on-stop)
-         (add-stop-script! (lambda () (begin/void-default script ...)))))]))
+       (add-stop-script! (lambda () (begin/void-default script ...))))]))
 
 (define-syntax (on-event stx)
   (syntax-parse stx
@@ -1121,12 +1116,11 @@
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Endpoint Creation
 
-(define (ensure-in-endpoint-context! who)
-  (when (or (in-script?) (null? (current-facet-id)))
-    (error who "Attempt to add endpoint out of installation context; are you missing a (react ...)?")))
-
 (define (add-endpoint! where internal? patch-fn handler-fn)
-  (ensure-in-endpoint-context! 'add-endpoint!)
+  (when (in-script?)
+    (error 'add-endpoint!
+           "~a: Cannot add endpoint in script; are you missing a (react ...)?"
+           where))
   (define-values (new-eid delta-aggregate)
     (let ()
       (define a (current-actor-state))

racket/syndicate/core-lang.rkt

@@ -8,7 +8,6 @@
 (require "main.rkt")
 (require (submod "actor.rkt" for-module-begin))
 (require "store.rkt")
-(require (only-in "core.rkt" clean-actions))
 
 (provide (rename-out [module-begin #%module-begin])
          activate
@@ -72,13 +71,6 @@
                           #%declare
                           begin-for-declarations))))
 
-(define (ensure-spawn-actions! acts)
-  (define cleaned-acts (clean-actions acts))
-  (for ([act (in-list cleaned-acts)]
-        #:unless (actor? act))
-    (raise-argument-error 'syndicate-module "top-level actor creation action" act))
-  cleaned-acts)
-
 (define-syntax (syndicate-module stx)
   (syntax-parse stx
     [(_ (action-ids ...) (form forms ...))
@@ -97,9 +89,8 @@
         #`(begin
             (define-values (tmp ...) (values #,@(make-list (length (syntax->list #'(x ...))) #'#f)))
             (define action-id
-              (ensure-spawn-actions!
-               (capture-actor-actions
-               (lambda () (set!-values (tmp ...) e)))))
+              (capture-actor-actions
+               (lambda () (set!-values (tmp ...) e))))
             (define-values (x ...) (values tmp ...))
             (syndicate-module (action-ids ... action-id) (forms ...)))]
        [(head rest ...)
@@ -108,9 +99,8 @@
            #`(begin #,expanded (syndicate-module (action-ids ...) (forms ...)))]
           [else
            (with-syntax ([action-id (car (generate-temporaries (list #'form)))])
-             #`(begin
-                 (define action-id (ensure-spawn-actions! (capture-actor-actions (lambda () #,expanded))))
-                 (syndicate-module (action-ids ... action-id) (forms ...))))])]
+             #`(begin (define action-id (capture-actor-actions (lambda () #,expanded)))
+                      (syndicate-module (action-ids ... action-id) (forms ...))))])]
        [non-pair-syntax
         #'(begin form (syndicate-module (action-ids ...) (forms ...)))])]
     [(_ (action-ids ...) ())

racket/syndicate/examples/example-lang.rkt

@@ -60,10 +60,7 @@
          (quit))]
     [_ #f]))
 
-(actor (lambda (e s) (quit))
-       #f
-       (message (set-timer 'tick 1000 'relative)))
-
+(message (set-timer 'tick 1000 'relative))
 (actor ticker
        1
        (patch-seq (sub (observe (set-timer ? ? ?)))

racket/syndicate/little-actors/core.rkt

@@ -13,7 +13,6 @@
 (require (for-syntax syntax/parse))
 (require rackunit)
 (require racket/engine)
-(require racket/exn)
 
 (define mt-scn (scn trie-empty))
 
@@ -290,7 +289,7 @@
 ;; leaf behavior function
 (define (actor-behavior e s)
   (when e
-    (with-handlers ([exn:fail? (lambda (e) (printf "exception: ~v\n" (exn->string e)) (quit #:exception e (list)))])
+    (with-handlers ([exn:fail? (lambda (e) (eprintf "exception: ~v\n" e) (quit #:exception e (list)))])
       (match-define (actor-state π-old fts) s)
       (define-values (actions next-fts)
         (for/fold ([as '()]
@@ -546,7 +545,7 @@
 ;; boot-actor : actor Γ -> Action
 (define (boot-actor a Γ)
   (with-handlers ([exn:fail? (lambda (e)
-                               (printf "booting actor died with: ~a\n" (exn->string e))
+                               (eprintf "booting actor died with: ~v\n" e)
                                #f)])
     (match a
       [`(spawn ,O ...)

racket/syndicate/trace/msd.rkt

@@ -1,7 +1,5 @@
 #lang racket/base
 
-(provide start-tracing!)
-
 (require racket/match)
 (require racket/set)
 (require racket/string)
@@ -14,7 +12,7 @@
 
 (define-logger syndicate/trace/msd)
 
-(define (start-tracing! output-filename)
+(let ((output-filename (getenv "SYNDICATE_MSD")))
   (when output-filename
     (define names (make-hash (list (cons '() "'ground"))))
     (define (open-output cause)
@@ -106,5 +104,3 @@
                     (loop)))))
       (channel-get ch)
       (current-trace-procedures (cons msd-trace (current-trace-procedures))))))
-
-(start-tracing! (getenv "SYNDICATE_MSD"))

racket/typed/Makefile

@@ -6,6 +6,5 @@ pan.c : leader-and-seller.pml
 
 # -a to analyze, -f for (weak) fairness
 # -n to elide report of unreached states
-# -N spec-name to verify a particular specification
 check: pan
-	./pan -a -f -n
+	./pan -a -f

racket/typed/compile-spin.rkt

@@ -0,0 +1,635 @@
+#lang racket
+
+;; TODO - syntax for LTL
+
+(require "proto.rkt")
+(require "ltl.rkt")
+
+(module+ test
+  (require rackunit)
+  (require "test-utils.rkt"))
+
+;; a SpinProgram is a
+;;   (sprog Assignment [Listof SpinProcess] [LTL SName])
+(struct sprog [assignment procs spec] #:transparent)
+
+
+;; a SpinProcess is a
+;;   (sproc SName [Setof SName] Assignment [Listof SName] [Setof SpinState])
+(struct sproc [name state-names init initial-assertions states] #:transparent)
+
+;; an Assignment is a [Hashof SVar SValue]
+
+;; a SName is a Symbol that is a legal variable name in Spin
+
+;; a SVar is a
+;;   (svar SName SType)
+(struct svar [name ty] #:transparent)
+
+;; a SValue is one of
+;;   - Int
+;;   - Bool
+;;   - SName
+;; and must be a valid Spin literal
+
+;; a SType is one of
+;;  - 'SInt
+;;  - 'SBool
+;;  - 'mtype
+(define SInt 'SInt)
+(define SBool 'SBool)
+(define mtype 'mtype)
+
+;; a SpinState is a
+;;   (sstate SName [Sequenceof SBranch])
+(struct sstate [name branches] #:transparent)
+
+;; a SBranch is a
+;;   (sbranch D+ SName [Listof SAction])
+(struct sbranch [event dest actions] #:transparent)
+
+;; a SAction is one of
+;;   - (assert ?)
+;;   - (retract ?)
+;;   - (send ?)
+;;   - (incorporate D+)
+;;   - (transition-to SName)
+(struct assert [ty] #:transparent)
+(struct retract [ty] #:transparent)
+;; send defined in proto.rkt
+(struct incorporate [evt] #:transparent)
+(struct transition-to [dest] #:transparent)
+
+;; each process has a local variable that determines its current state
+(define CURRENT-STATE (svar 'current mtype))
+
+;; a NameEnvironment is a [Hashof τ SName]
+
+;; [Sequenceof RoleGraph] [LTL τ] -> SpinProgram
+(define (program->spin rgs [spec #t])
+  (define assertion-tys (all-assertions rgs))
+  (define event-tys (all-events rgs))
+  (define event-subty# (make-event-map assertion-tys event-tys))
+  (define all-mentioned-tys (set-union assertion-tys event-tys))
+  (define name-env (make-name-env all-mentioned-tys))
+  (define globals (initial-assertion-vars-for all-mentioned-tys name-env))
+  (define procs (for/list ([rg rgs]) (rg->spin rg event-subty# name-env)))
+  (define spec-spin (rename-ltl spec name-env))
+  (sprog globals procs spec-spin))
+
+;; RoleGraph [Hashof τ [Setof τ]] NameEnvironment -> SpinProcess
+(define (rg->spin rg event-subty# name-env #:name [name (gensym 'proc)])
+  (match-define (role-graph st0 states) rg)
+  (define all-events (all-event-types (in-hash-values states)))
+  (define state-renaming (make-state-rename (hash-keys states)))
+  (define states- (for/list ([st (in-hash-values states)])
+                    (state->spin st states event-subty# name-env state-renaming)))
+  (define st0- (hash-ref state-renaming st0))
+  ;; ergh the invariant for when I tack on _assertions to a name is getting tricksy
+  (define st0-assertions (rename-all name-env (super-type-closure (state-assertions (hash-ref states st0)) event-subty#)))
+  (define assignment (local-variables-for st0- all-events name-env))
+  (sproc name (hash-values-set state-renaming) assignment st0-assertions (list->set states-)))
+
+;; State [Sequenceof State] [Hashof τ [Setof τ]] NameEnvironment [Hashof StateName SName] -> SpinState
+(define (state->spin st states event-subty# name-env state-env)
+  (match-define (state name transitions assertions) st)
+  (define name- (hash-ref state-env name))
+  (define branches (for*/list ([(D+ txns) (in-hash transitions)]
+                               [txn (in-set txns)])
+                     (match-define (transition effs dest) txn)
+                     (match-define (state _ _ dest-assertions) (hash-ref states dest))
+                     (define dest- (hash-ref state-env dest))
+                     (branch-on D+ assertions dest- dest-assertions effs event-subty# name-env)))
+  (sstate name- branches))
+
+;; [Setof τ] -> NameEnvironment
+(define (make-name-env tys)
+  (let loop ([name-depth 3])
+    (when (> name-depth 10)
+      (raise-argument-error 'make-name-env "types able to be named" tys))
+    (define renaming
+      (for/hash ([ty (in-set tys)])
+        (values ty
+                (type->id ty #:depth name-depth))))
+    (define names (hash-values-set renaming))
+    (cond
+      [(equal? (set-count names) (set-count tys))
+       renaming]
+      [else
+       (loop (add1 name-depth))])))
+
+;; SName -> SName
+(define (assertions-var-name s)
+  (string->symbol (format "~a_assertions" s)))
+
+;; SName -> SName
+(define (active-var-name s)
+  (string->symbol (format "know_~a" s)))
+
+;; [Setof τ] [Setof τ] -> [Hashof τ [Setof τ]]
+(define (make-event-map assertion-tys event-tys)
+  ;; TODO - potentially use non-empty intersection
+  (for/hash ([a (in-set assertion-tys)])
+    (values a
+            (all-supertypes-of a event-tys))))
+
+;; τ [Setof τ] -> [Setof τ]
+(define (all-supertypes-of τ tys)
+  (for*/set ([ty (in-set tys)]
+             #:when (<:? τ ty))
+    ty))
+
+;; [Setof τ] [Hashof τ [Setof τ]]
+(define (super-type-closure asserts event-subty#)
+  (for*/set ([a (in-set asserts)]
+             [supers (in-value (hash-ref event-subty# a))]
+             [τ (in-set (set-add supers a))])
+    τ))
+
+;; [Setof τ] NameEnvironment -> Assignment
+(define (initial-assertion-vars-for assertion-tys name-env)
+  (for/hash ([τ (in-set assertion-tys)])
+    (values (svar (assertions-var-name (hash-ref name-env τ)) SInt)
+            0)))
+
+;; NameEnvironment [Setof τ] -> [Sequenceof SName]
+(define (rename-all name-env asserts)
+  (for/set ([a (in-set asserts)])
+    (hash-ref name-env a)))
+
+;; [Sequenceof RoleGraph] -> [Setof τ]
+(define (all-assertions rgs)
+  ;; RoleGraph -> (Setof τ)
+  (define (all-assertions-of rg)
+    (for*/set ([st (in-hash-values (role-graph-states rg))]
+               [τ (in-set (state-assertions st))])
+      τ))
+  (for/fold ([as (set)])
+            ([rg rgs])
+    (set-union as (all-assertions-of rg))))
+
+;; [Sequenceof RoleGraph] -> [Setof τ]
+(define (all-events rgs)
+  ;; RoleGraph -> (Setof τ)
+  (define (all-events-of rg)
+    (all-event-types (hash-values (role-graph-states rg))))
+  (for/fold ([as (set)])
+            ([rg rgs])
+    (set-union as (all-events-of rg)))
+  )
+
+;; [Sequenceof State] -> ?
+(define (all-event-types states)
+  (for*/set ([st states]
+             [D+ (in-hash-keys (state-transitions st))])
+    (match D+
+      [(or (Asserted τ) (Retracted τ))
+       τ]
+      [(Message τ)
+       (raise-argument-error 'all-event-types "messages not supported yet" D+)]
+      [_
+       (raise-argument-error 'all-event-types "internal events not allowed" D+)])))
+
+;; SName [Setof τ] NameEnvironment -> Assignment
+(define (local-variables-for st0 all-events name-env)
+  (define assign
+    (for/hash ([evt (in-set all-events)])
+      (values (svar (active-var-name (hash-ref name-env evt))
+                    SBool)
+              #f)))
+  (hash-set assign CURRENT-STATE st0))
+
+;; D+ [Setof τ] SName [Setof τ] [Listof TransitionEffect] [Hashof τ [Setof τ]] NameEnvironment -> SBranch
+(define (branch-on D+ curr-assertions dest dest-assertions effs event-subty# name-env)
+  (define new-assertions (super-type-closure (set-subtract dest-assertions curr-assertions) event-subty#))
+  (define retractions (super-type-closure (set-subtract curr-assertions dest-assertions) event-subty#))
+  (define (lookup ty) (hash-ref name-env ty))
+  (define asserts (set-map new-assertions (compose assert lookup)))
+  (define retracts (set-map retractions (compose retract lookup)))
+  (unless (empty? effs)
+    (raise-argument-error 'branch-on "messages not supported" effs))
+  (define renamed-evt (rename-event D+ name-env))
+  (sbranch renamed-evt dest (list* (transition-to dest)
+                                   (incorporate renamed-evt)
+                                   (append asserts retracts effs))))
+
+;; D+ NameEnvironment -> D+
+(define (rename-event D+ name-env)
+  (match D+
+    [(Asserted τ)
+     (Asserted (hash-ref name-env τ))]
+    [(Retracted τ)
+     (Retracted (hash-ref name-env τ))]
+    [(Message τ)
+     (raise-argument-error 'rename-event "messages not implemented yet" D+)]))
+
+;; [LTL τ] -> [LTL SName]
+(define (rename-ltl ltl name-env)
+  (define (lookup τ) (hash-ref name-env τ))
+  (map-atomic ltl lookup))
+
+(module+ test
+  (test-case
+      "sanity: compile book seller type"
+    (define/timeout seller-rg (compile seller-actual))
+    (define name-env (hash
+                      (Observe (Observe (Struct 'BookQuoteT (list (Base 'String) (Mk⋆)))))
+                      'Obs_Obs_BookQuoteT
+                      (Observe (Struct 'BookQuoteT (list (Base 'String) (Mk⋆))))
+                      'Obs_BookQuoteT_String_star
+                      (Struct 'BookQuoteT (list (Base 'String) (U (list (Base 'Int) (Base 'Int)))))
+                      'BookQuoteT_String_U_Int_Int))
+    (define event# (hash
+                    (Observe (Observe (Struct 'BookQuoteT (list (Base 'String) (Mk⋆)))))
+                    (set)
+                    (Struct 'BookQuoteT (list (Base 'String) (U (list (Base 'Int) (Base 'Int)))))
+                    (set)))
+    (define/timeout seller-spin (rg->spin seller-rg event# name-env))
+    (check-true (sproc? seller-spin))))
+
+(define tab-level (make-parameter 0))
+
+(define TAB-WIDTH 2)
+
+(define (indent)
+  (display (make-string (* TAB-WIDTH (tab-level)) #\space)))
+
+(define-syntax-rule (with-indent bdy ...)
+  (parameterize ([tab-level (add1 (tab-level))])
+    bdy ...))
+
+(define SPIN_ID_RX #rx"[a-zA-Z][a-zA-Z0-9_]*")
+(define SPIN_ID_TRAILING_CHAR #rx"[a-zA-Z0-9_]+")
+
+;; (U Symbol String) -> Bool
+(define (spin-id? s)
+  (when (symbol? s)
+    (set! s (symbol->string s)))
+  (regexp-match? SPIN_ID_RX s))
+
+(define SPIN-KEYWORDS
+  '(active assert atomic bit bool break byte chan d_step D_proctype do
+		else empty enabled fi full goto hidden if init int len mtype nempty
+    never nfull od of pc_value printf priority proctype provided run
+		short skip timeout typedef unless unsigned xr xs))
+
+;; Symbol -> Symbol
+(define (unkeyword s)
+  (if (member s SPIN-KEYWORDS)
+      (gensym s)
+      s))
+
+;; (U Symbol String) -> SName
+(define (make-spin-id s)
+  (when (symbol? s)
+    (set! s (symbol->string s)))
+  (define with_legal_prefix (string-append "ty_" s))
+  (match (regexp-match* SPIN_ID_TRAILING_CHAR with_legal_prefix)
+    ['("ty_")
+     (raise-argument-error 'make-spin-id "unable to make spin id" s)]
+    [(cons fst rst)
+     (define match-str (apply string-append fst rst))
+     (define without-added-prefix (substring match-str 3))
+     (if (spin-id? without-added-prefix)
+         (unkeyword (string->symbol without-added-prefix))
+         (unkeyword (string->symbol match-str)))]))
+
+;; τ -> SName
+(define (type->id ty #:depth [depth 3])
+  (define ctors (type-constructors ty depth))
+  (define rough-name (string-join (map symbol->string ctors) "_"))
+  (make-spin-id rough-name))
+
+;; [Listof StateName] -> [Hashof StateName SName]
+(define (make-state-rename state-names)
+  (let loop ([prefix 3])
+    (define renaming (for/hash ([nm (in-list state-names)])
+                       (values nm
+                               (state-name->spin-id nm #:prefix prefix))))
+    (define distinct-names (hash-values-set renaming))
+    (cond
+      [(equal? (set-count distinct-names) (set-count state-names))
+       renaming]
+      [(> prefix 20)
+       (raise-argument-error 'make-state-rename "able to make renaming" state-names)]
+      [else
+       (loop (add1 prefix))])))
+
+;; StateName -> SName
+(define (state-name->spin-id nm #:prefix [prefix 3])
+  (cond
+    [(set-empty? nm)
+     (gensym 'inert)]
+    [else
+     (define (take-prefix s) (substring s 0 (min prefix (string-length s))))
+     (define rough-name (string-join (set-map nm (compose take-prefix symbol->string)) "_"))
+     (make-spin-id rough-name)]))
+
+;; τ -> [Listof Symbol]
+(define (type-constructors ty depth)
+  (cond
+    [(zero? depth) '()]
+    [else
+     (match ty
+       [(Struct name tys)
+        ;; TODO - consider camel-casing struct name
+        (cons name (append-map (λ (ty) (type-constructors ty (sub1 depth))) tys))]
+       [(Observe ty)
+        (cons 'Obs (type-constructors ty (sub1 depth)))]
+       [(U tys)
+        (cons 'U (append-map (λ (ty) (type-constructors ty (sub1 depth))) tys))]
+       [(== ⋆)
+        (list 'star)]
+       [(Base name)
+        (list name)]
+       [(List _)
+        (list 'List)]
+       [(Set _)
+        (list 'Set)]
+       [(Hash _ _)
+        (list 'Hash)]
+       [(internal-label _ _)
+        (raise-argument-error 'type-constructors "internal events not supported" ty)])]))
+
+(module+ test
+  (test-case
+      "type-constructors basics"
+    (define bi (Struct 'BookInterestT (list (Base 'String) (Base 'String) (Base 'Bool))))
+    (check-equal? (type-constructors bi 1)
+                  '(BookInterestT))
+    (check-equal? (type-constructors bi 2)
+                  '(BookInterestT String String Bool))
+    (check-equal? (type-constructors bi 3)
+                  '(BookInterestT String String Bool))
+    (check-equal? (type-constructors (Observe bi) 3)
+                  '(Obs BookInterestT String String Bool)))
+  (test-case
+      "type->id basics"
+    (define bi (Struct 'BookInterestT (list (Base 'String) (Base 'String) (Base 'Bool))))
+    (check-equal? (type->id bi)
+                  'BookInterestT_String_String_Bool)
+    (check-equal? (type->id (Observe bi))
+                  'Obs_BookInterestT_String_String_Bool)
+    (check-equal? (type->id (Struct 'hi-mom '()))
+                  'himom)
+    (check-equal? (type->id bi #:depth 1)
+                  'BookInterestT)
+    (check-exn exn:fail?
+               (lambda () (type->id (Struct '--- '())))
+               "unable to make spin id")))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Code Generation
+
+(define SPIN-PRELUDE (file->string "spin-prelude.pml"))
+
+;; SpinThang FilePath -> Void
+(define (gen-spin/to-file spin name)
+  (with-output-to-file name
+    (lambda () (gen-spin spin))
+    #:mode 'text
+    #:exists 'replace))
+
+;; SpinThang -> Void
+(define (gen-spin spin)
+  (match spin
+    [(sprog assignment procs spec)
+     (display SPIN-PRELUDE)
+     (gen-assignment assignment)
+     (newline)
+     (for ([p procs])
+       (gen-spin p)
+       (newline))
+     (gen-spec "spec" (lambda () (gen-ltl spec)))
+     (newline)
+     (gen-sanity-ltl assignment)]
+    [(sproc name state-names init asserts states)
+     (indent) (declare-mtype state-names)
+     (indent) (printf "active proctype ~a() {\n" name)
+     (with-indent
+       (gen-assignment init)
+       (for ([a asserts])
+         (gen-spin (assert a)))
+       (indent) (displayln "end: do")
+       (with-indent
+         (for ([st states])
+           (gen-spin st)))
+       (indent) (displayln "od;")
+       )
+     (indent) (displayln "}")]
+    [(sstate name branches)
+     (indent) (printf ":: ~a == ~a ->\n" (svar-name CURRENT-STATE) name)
+     (with-indent
+       (indent) (displayln "if")
+       (with-indent
+         (cond
+           [(empty? branches)
+            (indent) (displayln ":: true -> skip;")]
+           [else
+            (for ([branch branches])
+              (gen-spin branch))]))
+       (indent) (displayln "fi;"))]
+    [(sbranch event dest actions)
+     (indent) (printf ":: ~a ->\n" (predicate-for event))
+     ;; TODO - make the body atomic
+     (with-indent
+       (indent) (displayln "atomic {")
+       (with-indent
+         (for ([act actions])
+           (gen-spin act)))
+       (indent) (displayln "}"))]
+    [(assert x)
+     (indent) (printf "ASSERT(~a);\n" x)]
+    [(retract x)
+     (indent) (printf "RETRACT(~a);\n" x)]
+    [(send x)
+     (raise-argument-error 'gen-spin "message sending not supported yet" spin)]
+    [(incorporate evt)
+     (indent) (update-for evt)]
+    [(transition-to dest)
+     (indent) (printf "~a = ~a;\n" (svar-name CURRENT-STATE) dest)]))
+
+;; [Setof SName] -> Void
+(define (declare-mtype state-names)
+  (display "mtype = {")
+  (display (string-join (set-map state-names symbol->string) ", "))
+  (displayln "}"))
+
+;; Assignment -> Void
+(define (gen-assignment assign)
+  (for ([(var val) (in-hash assign)])
+    (indent) (printf "~a = ~a;\n"
+                     (declare-var var)
+                     (spin-val->string val))))
+
+;; SVar -> Void
+(define (declare-var var)
+  (match-define (svar name ty) var)
+  (format "~a ~a" (spin-type->string ty) name))
+
+;; SValue -> String
+(define (spin-val->string v)
+  (cond
+    [(boolean? v)
+     (if v "true" "false")]
+    [(exact-integer? v)
+     (~a v)]
+    [(symbol? v)
+     (~a v)]))
+
+;; SType -> String
+(define (spin-type->string ty)
+  (match ty
+    [(== SInt) "int"]
+    [(== SBool) "bool"]
+    [(== mtype) "mtype"]))
+
+;; D+ -> String
+(define (predicate-for event)
+  (match event
+    [(Asserted nm)
+     (define assertion-var nm)
+     (define active-var (active-var-name nm))
+     (format "ASSERTED(~a) && !~a" assertion-var active-var)]
+    [(Retracted nm)
+     (define assertion-var nm)
+     (define active-var (active-var-name nm))
+     (format "RETRACTED(~a) && ~a" assertion-var active-var)]
+    [(Message nm)
+     (raise-argument-error 'predicate-for "message sending not supported yet" event)]))
+
+;; D+ -> Void
+(define (update-for event)
+  (match event
+    [(Asserted nm)
+     (define active-var (active-var-name nm))
+     (printf "~a = ~a;\n" active-var (spin-val->string #t))]
+    [(Retracted nm)
+     (define active-var (active-var-name nm))
+     (printf "~a = ~a;\n" active-var (spin-val->string #f))]
+    [(Message nm)
+     (raise-argument-error 'predicate-for "message sending not supported yet" event)]))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; LTL
+
+;; String {-> Void} -> Void
+(define (gen-spec name mk-body)
+  (indent) (printf "ltl ~a {\n" name)
+  (with-indent
+    (mk-body))
+  (newline)
+  (indent) (displayln "}"))
+
+;; [LTL SName] -> Void
+(define (gen-ltl ltl)
+  (match ltl
+    [(always p)
+     (indent) (displayln "[](")
+     (with-indent
+       (gen-ltl p))
+     (indent) (displayln ")")]
+    [(eventually p)
+     (indent) (displayln "<>(")
+     (with-indent
+       (gen-ltl p))
+     (indent) (displayln ")")]
+    [(weak-until p q)
+     (gen-ltl-bin-op "W" p q)]
+    [(strong-until p q)
+     (gen-ltl-bin-op "U" p q)]
+    [(ltl-implies p q)
+     (gen-ltl-bin-op "->" p q)]
+    [(ltl-and p q)
+     (gen-ltl-bin-op "&&" p q)]
+    [(ltl-or p q)
+     (gen-ltl-bin-op "||" p q)]
+    [(ltl-not p)
+     (indent) (display "!(")
+     (gen-ltl p)
+     (displayln ")")]
+    [(atomic nm)
+     (printf "ASSERTED(~a)\n" nm)]
+    [#t
+     (display "true")]
+    [#f
+     (display "false")]))
+
+;; String [LTL SName] [LTL SName] -> Void
+(define (gen-ltl-bin-op name p q)
+  (indent) (display "(") (gen-ltl p) (display ") ")
+  (displayln name)
+  (newline)
+  (indent) (display "(") (gen-ltl q) (displayln ")"))
+
+;; Assignment -> Void
+(define (gen-sanity-ltl assignment)
+  (gen-spec "sanity"
+            (lambda ()
+              (indent) (displayln "[](")
+              (with-indent
+                (for ([assertion-var (in-hash-keys assignment)])
+                  (indent) (printf "~a >= 0 &&\n" (svar-name assertion-var)))
+                (indent) (displayln "true"))
+              (indent) (displayln ")"))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Misc Utils
+
+;; [Hashof K V] -> [Setof V]
+(define (hash-values-set h)
+  (for/set ([x (in-hash-values h)])
+    x))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Test Case
+
+(module+ leader-and-seller
+  (define leader-rg (compile (parse-T
+    '(Role ; = react
+      (get-quotes)
+      (Reacts ; = on
+       (Asserted (BookQuoteT String (Bind Int)))
+       (Branch
+        (Effs (Branch (Effs (Stop get-quotes)) (Effs)))
+        (Effs
+         (Role
+          (poll-members)
+          (Reacts
+           (Asserted (BookInterestT String (Bind String) Discard))
+           (Branch
+            (Effs (Stop poll-members (Branch (Effs (Stop get-quotes)) (Effs))))
+            (Effs))
+           (Branch
+            (Effs
+             (Stop get-quotes (Role (announce) (Shares (BookOfTheMonthT String)))))
+            (Effs)))
+          (Reacts (Retracted (BookInterestT String (Bind String) Bool)))
+          (Reacts (Asserted (BookInterestT String (Bind String) Bool)))
+          (Reacts (Retracted (BookInterestT String (Bind String) Bool)))
+          (Reacts (Asserted (BookInterestT String (Bind String) Bool)))))))
+      (Reacts (Retracted (ClubMemberT (Bind String))))
+      (Reacts (Asserted (ClubMemberT (Bind String))))))))
+  (define seller-rg (compile seller-actual))
+  (define member-rg (compile member-actual))
+  (define bq (book-quote String ⋆))
+  (define bi (book-interest String ⋆ ⋆))
+  (define book-club-spec
+    (&& (eventually (atomic bq))
+        (always (ltl-implies (atomic (Observe bq))
+                             (eventually (atomic bq))))
+        (always (ltl-implies (atomic (Observe bi))
+                             (eventually (atomic bi))))))
+  (define book-club-spin (program->spin (list leader-rg seller-rg member-rg)
+                                        book-club-spec))
+  (gen-spin/to-file book-club-spin "gen-book-club.pml"))
+
+(module+ flink
+  (define (import r)
+    (define r+ (parse-T r))
+    (compile/internal-events (compile r+) #f))
+  (define jm-rg (import job-manager-actual))
+  (define tm-rg (import task-manager-ty))
+  (define tr-rg (import task-runner-ty))
+  (define flink-spin (program->spin (list tr-rg tm-rg jm-rg)))
+  (gen-spin/to-file flink-spin "gen-flink.pml"))

racket/typed/core-expressions.rkt

@@ -17,8 +17,6 @@
          error
          define-tuple
          match-define
-         mk-tuple
-         tuple-select
          (for-syntax (all-defined-out)))
 
 (require "core-types.rkt")
@@ -166,15 +164,12 @@
      (⇒ ν-s #,(make-Branch #'((ss ...) ...)))])
 
 
-;; (Listof Value) -> Value
-(define- (mk-tuple es)
-  (#%app- cons- 'tuple es))
 
 (define-typed-syntax (tuple e:expr ...) ≫
   [⊢ e ≫ e- (⇒ : τ)] ...
   #:fail-unless (stx-andmap pure? #'(e- ...)) "expressions not allowed to have effects"
   -----------------------
-  [⊢ (#%app- mk-tuple (#%app- list- e- ...)) (⇒ : (Tuple τ ...))])
+  [⊢ (#%app- list- 'tuple e- ...) (⇒ : (Tuple τ ...))])
 
 (define unit : Unit (tuple))
 
@@ -210,6 +205,8 @@
     [(tuple p ...)
      #:with (([x:id τ:type] ...) ...) (stx-map pat-bindings #'(p ...))
      #'([x τ] ... ...)]
+    #;[(k:kons1 p)
+     (pat-bindings #'p)]
     [(~constructor-exp cons p ...)
      #:with (([x:id τ:type] ...) ...) (stx-map pat-bindings #'(p ...))
      #'([x τ] ... ...)]
@@ -263,6 +260,9 @@
       [(tuple p ...)
        (quasisyntax/loc pat
          (tuple #,@(stx-map elaborate-pattern #'(p ...))))]
+      [(k:kons1 p)
+       (quasisyntax/loc pat
+         (k #,(elaborate-pattern #'p)))]
       [(~constructor-exp ctor p ...)
        (quasisyntax/loc pat
          (ctor #,@(stx-map elaborate-pattern #'(p ...))))]
@@ -277,14 +277,10 @@
       [x:dollar-ann-id
        (syntax/loc pat (bind x.id x.ty))]
       [x:dollar-id
-       (when (bot? ty)
-         (raise-syntax-error #f "unable to instantiate pattern with matching part of type" pat))
        (quasisyntax/loc pat (bind x.id #,ty))]
       [($ x:id ty)
        (syntax/loc pat (bind x ty))]
       [($ x:id)
-       (when (bot? ty)
-         (raise-syntax-error #f "unable to instantiate pattern with matching part of type" pat))
        (quasisyntax/loc pat (bind x #,ty))]
       [(tuple p ...)
        (define (matching? t)
@@ -323,7 +319,6 @@
        (define (proj t i)
          (syntax-parse t
            [(~constructor-type _ tt ...)
-            #:when (matching? t)
             (if (= i -1)
                 t
                 (stx-list-ref #'(tt ...) i))]
@@ -350,6 +345,8 @@
         #:datum-literals (tuple discard bind)
         [(tuple p ...)
          #`(#,list-binding 'tuple #,@(stx-map loop #'(p ...)))]
+        #;[(k:kons1 p)
+         #`(#,(kons1->constructor #'k) #,(loop #'p))]
         [(bind x:id τ:type)
          (bind-id-transformer #'x)]
         [discard

racket/typed/core-types.rkt

@@ -3,10 +3,7 @@
 (provide (except-out (all-defined-out) → ∀ Role)
          (rename-out [→+ →]
                      [∀+ ∀]
-                     [Role+Body Role]
-                     [Role Role/internal]
-                     [∀ ∀/internal]
-                     [→ →/internal])
+                     [Role+Body Role])
          (for-syntax (except-out (all-defined-out) ~→ ~∀ ~Role)
                      (rename-out [~→+ ~→]
                                  [~∀+ ~∀]
@@ -38,8 +35,7 @@
 (require (postfix-in - racket/set))
 (require (postfix-in - racket/match))
 (require (postfix-in - (only-in racket/format ~a)))
-(require (for-syntax racket/provide-transform)
-         racket/provide-syntax)
+(require (for-syntax "syntax-serializer.rkt"))
 
 
 (module+ test
@@ -49,36 +45,6 @@
 (begin-for-syntax
   (current-use-stop-list? #f))
 
-(define-for-syntax KIND-TAG ':)
-
-#;(require (for-syntax "syntax-serializer.rkt"))
-(define-for-syntax (lazy-serialize t) t)
-(define-for-syntax (lazy-deserialize t)
-  (define TYPE (type-eval #'Type))
-  (define FN (type-eval #'FacetName))
-  (let loop ([t t])
-    (syntax-parse t
-      #:literals (#%plain-app #%plain-lambda list)
-      [_:id
-       (attach t KIND-TAG TYPE)]
-      [(#%plain-app tycons τ-in (#%plain-lambda (X) τ-out))
-       #:do [(define var-ty (if (equal? 'Role (syntax-e #'typecons)) FN TYPE))]
-       #:with τ-in- (attach (loop #'τ-in) KIND-TAG var-ty)
-       #:with X- (attach #'X KIND-TAG var-ty)
-       #:with τ-out- (loop #'τ-out)
-       (define reconstructed #`(#%plain-app tycons τ-in- (#%plain-lambda (X-) τ-out-)))
-       (attach (add-orig reconstructed t) KIND-TAG TYPE)]
-      [(#%plain-app tycons (~or* (~seq ty ... (#%plain-app (~and lst list) . more-tys))
-                                 (~seq ty ...)) )
-       #:with more-tys- (if (attribute more-tys) (stx-map loop #'more-tys) #'())
-       (define reconstructed #`(#%plain-app tycons
-                                            #,@(stx-map loop #'(ty ...))
-                                            (~? (#%plain-app lst . more-tys-))))
-       (attach (add-orig reconstructed t) KIND-TAG TYPE)])))
-(define-for-syntax serialize-syntax lazy-serialize)
-(define-for-syntax deserialize-syntax lazy-deserialize)
-
-
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Type Checking Conventions
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -90,15 +56,6 @@
 ;; ν-f key aggregates facet effects (starting/stopping a facet) as `Role`s & `Stop`s and message sends, `Sends`
 ;; ν-s key aggregates spawned actors as `Actor`s
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Type Renaming
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(define-simple-macro (define-typed-variable-rename+ x:id (~datum ≫) x-:id (~datum :) τ:type)
-    #:with serialized-τ (serialize-syntax #'τ.norm)
-    (define-syntax x
-      (make-variable-like-transformer (add-orig (attach #'x- ': (deserialize-syntax #'serialized-τ)) #'x))))
-
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Types
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -118,10 +75,20 @@
     (hash-set! TypeInfo#
                ty-cons
                (type-metadata isec cons)))
+  ;; Identifier -> Symbol
+  ;; XYZ-.*
+  ;; based on the convention used by turnstile *shrug*
+  (define (un- id)
+    (define match?
+      (regexp-match #px"^(\\S*)-\\S*$" (symbol->string (syntax-e id))))
+    (if match?
+        (string->symbol (second match?))
+        (begin (printf "no match! ~a\n" id)
+               match?)))
 
   ;; Identifier -> (U #f type-metadata)
   (define (get-type-info ty-cons)
-    (hash-ref TypeInfo# (syntax-e ty-cons) #f))
+    (hash-ref TypeInfo# (un- ty-cons) #f))
 
   ;; Identifier -> (U #f isec-desc)
   (define (get-type-isec-desc ty-cons)
@@ -179,28 +146,13 @@
       (error "expected to find type-cons-key"))
     (tycons args)))
 
-(begin-for-syntax
-  (define ((mk-ctor-rewriter Name-) stx)
-    (syntax-parse stx
-      [(_ . ts)
-       (quasisyntax/loc stx
-         (#,Name- . ts))]))
-  (begin-for-syntax
-    (define ((mk-ctor-rewriter Name-) stx)
-      (syntax-parse stx
-        [(_ . ts)
-         (quasisyntax/loc stx
-           (#,Name- . ts))])))
-  )
-
 (define-syntax (define-type-constructor+ stx)
   (syntax-parse stx
     [(_ Name:id
         #:arity op arity
         #:arg-variances variances
         #:isect-desc desc:isect-desc
-        (~optional (~seq #:extra-info extra-info))
-        (~optional (~seq #:implements meths ...)))
+        (~optional (~seq #:extra-info extra-info)))
      #:with Name- (mk-- #'Name)
      #:with NamePat (mk-~ #'Name)
      #:with NamePat- (mk-~ #'Name-)
@@ -208,13 +160,25 @@
      #:with mk- (format-id #'Name- "mk-~a-" (syntax-e #'Name-))
      (quasisyntax/loc stx
        (begin-
-         (define-type-constructor Name
+         (define-type-constructor Name-
            #:arity op arity
            #:arg-variances variances
-           (~? (~@ #:extra-info extra-info))
-           (~? (~@ #:implements meths ...)))
+           #,@(if (attribute extra-info)
+                  #'(#:extra-info extra-info)
+                  #'()))
+         (define-syntax (Name stx)
+           (syntax-parse stx
+             [(_ . ts)
+              (syntax/loc stx
+                (Name- . ts))]))
          (begin-for-syntax
-           (set-type-info! 'Name '#,(attribute desc.val) mk))))]))
+           (set-type-info! 'Name '#,(attribute desc.val) mk-)
+           (define-syntax NamePat
+             (pattern-expander
+              (syntax-parser
+                [(_ . p)
+                 #'(NamePat- . p)]))))
+         (define-for-syntax mk mk-)))]))
 
 (begin-for-syntax
   ;; Syntax -> (Listof Variant)
@@ -230,15 +194,15 @@
 (define-syntax (define-container-type stx)
   (syntax-parse stx
     [(_ Name:id #:arity op arity
-        (~optional (~seq #:extra-info extra-info))
-        (~optional (~seq #:implements meths ...)))
+        (~optional (~seq #:extra-info extra-info)))
      (quasisyntax/loc stx
        (define-type-constructor+ Name
          #:arity op arity
          #:arg-variances mk-covariant
          #:isect-desc CONTAINER-LIKE
-         (~? (~@ #:extra-info extra-info))
-         (~? (~@ #:implements meths ...))))]))
+         #,@(if (attribute extra-info)
+                #'(#:extra-info extra-info)
+                #'())))]))
 
 ;; Define a type constructor that acts like a product:
 ;;   - covariant
@@ -246,15 +210,15 @@
 (define-syntax (define-product-type stx)
   (syntax-parse stx
     [(_ Name:id #:arity op arity
-        (~optional (~seq #:extra-info extra-info))
-        (~optional (~seq #:implements meths ...)))
+        (~optional (~seq #:extra-info extra-info)))
      (quasisyntax/loc stx
        (define-type-constructor+ Name
          #:arity op arity
          #:arg-variances mk-covariant
          #:isect-desc PRODUCT-LIKE
-         (~? (~@ #:extra-info extra-info))
-         (~? (~@ #:implements meths ...))))]))
+         #,@(if (attribute extra-info)
+                #'(#:extra-info extra-info)
+                #'())))]))
 
 (define-type Type : Type)
 
@@ -268,6 +232,8 @@
   (define (new-type? t)
     (or (type?- t)
         (Type? (detach t ':))))
+  #;(require racket/trace)
+  #;(trace new-type?)
 
   (current-type? new-type?))
 
@@ -302,30 +268,44 @@
       [>
        (append prefix (list #'Type #'Type #'*))]
       [>=
-       (append prefix (list #'Type #'*))])))
+       (append prefix (list #'Type #'*))]))
+
+  ;; PatternExpander (Syntax-Listof ID) ID -> Pattern
+  (define (make-type-recognizer pat dom ty)
+    (define pats (for/list ([t (in-syntax dom)])
+                   (if (free-identifier=? t #'Type)
+                       #'_
+                       #'(... ...))))
+    #`(syntax-parse ty
+        [(#,pat #,@pats) #t]
+        [_ #f])))
 
 (define-syntax (define-type-constructor stx)
   (syntax-parse stx
     [(_ Name:id #:arity op arity:nat
                 (~optional (~seq #:arg-variances variances))
-                (~optional (~seq #:extra-info extra-info))
-                (~optional (~seq #:implements meths ...)))
-     #:with Name- (mk-- #'Name)
-     #:with mk- (mk-mk #'Name-)
+                (~optional (~seq #:extra-info extra-info)))
+     #:with mk- (mk-mk (mk-- #'Name))
      #:with Name? (mk-? #'Name)
+     #:with Name-exp (mk-~ #'Name)
      #:with dom (make-arity-domain #'op (syntax-e #'arity))
      #:do [
-           (define implements? (if (or (attribute variances) (attribute extra-info) (attribute meths))
+           (define arg-var-meth #'(~? (get-arg-variances-data variances)
+                                      ()))
+           (define extra-info-meth #'(~? (get-extra-info-data extra-info)
+                                         ()))
+           (define implements? (if (or (attribute variances) (attribute extra-info))
                                    #'(#:implements)
                                    #'()))]
      #`(begin-
          (define-type Name : #,@#'dom -> Type
            #,@implements?
-           (~? (~@ get-arg-variances-data variances))
-           (~? (~@ get-extra-info-data extra-info))
-           (~? (~@ meths ...)))
+           #,@arg-var-meth
+           #,@extra-info-meth)
          (define-for-syntax (mk- args)
-           ((current-type-eval) #`(Name #,@args))))]))
+           ((current-type-eval) #`(Name #,@args)))
+         (define-for-syntax (Name? ty)
+           #,(make-type-recognizer #'Name-exp #'dom #'ty)))]))
 
 (define-simple-macro (define-base-type Name:id)
   (define-type Name : Type))
@@ -337,17 +317,11 @@
 
 (define-type FacetName : FacetName)
 
-(define-type RoleBody : Type * -> Type)
-(define-type Role #:with-binders [X : FacetName] : Type -> Type
-  #:implements get-resugar-info
-  (syntax-parser
-    [(~Role (nm : _) (~RoleBody body ...))
-     (list* #'Role (list #'nm) (stx-map resugar-type #'(body ...)))]))
-(define-for-syntax (Role? stx)
-  (syntax-parse stx
-    [(~Role (_ : _) _) #t]
-    [_ #f]))
+#;(define-type-constructor? Shares #:arity = 1)
 
+#;(define-binding-type Role #:arity >= 0 #:bvs = 1)
+(define-type Role #:with-binders [X : FacetName] : Type -> Type)
+(define-type RoleBody : Type * -> Type)
 (define-type-constructor Shares #:arity = 1)
 (define-type-constructor Sends #:arity = 1)
 (define-type-constructor Realizes #:arity = 1)
@@ -369,17 +343,6 @@
 (define-base-types OnStart OnStop OnDataflow MakesField)
 (define-for-syntax field-prop-name 'fields)
 (define-type-constructor Actor #:arity = 1)
-(define-type-constructor ActorWithRole #:arity >= 1)
-;; usage: (ActorWithRole τc τr)
-;;  τc is the communication type
-;;  τr is the Role type of the root facet
-(begin-for-syntax
-  (define-syntax ~AnyActor
-    (pattern-expander
-    (syntax-parser
-      [(_ τc-pat)
-       #'(~or* (~Actor τc-pat)
-               (~ActorWithRole τc-pat _))]))))
 
 #;(define-product-type Message #:arity = 1)
 (define-product-type Tuple #:arity >= 0)
@@ -387,22 +350,12 @@
 #;(define-product-type Inbound #:arity = 1)
 #;(define-product-type Outbound #:arity = 1)
 (define-container-type AssertionSet #:arity = 1)
+(define-container-type Patch #:arity = 2)
 
 ;; functions and type abstractions
-(define-for-syntax (resugar-∀ ty)
-  (syntax-parse (flatten-∀ ty)
-    [((X ...) body)
-     (list* #'∀ (syntax->list #'(X ...)) (resugar-type #'body))]))
-
-(define-type ∀ #:with-binders [X : Type] : Type -> Type
-  #:implements get-resugar-info
-  resugar-∀)
-
-(define-type-constructor → #:arity > 0
-  #:implements get-resugar-info
-  (syntax-parser
-    [(~→ o i ...)
-     (cons #'→ (stx-map resugar-type #'(i ... o)))]))
+#;(define-binding-type ∀)
+(define-type ∀ #:with-binders [X : Type] : Type -> Type)
+(define-type-constructor → #:arity > 0)
 
 (define-simple-macro (→+ in ... out)
   (→ out in ...))
@@ -472,11 +425,6 @@
 
 (define-type-constructor U* #:arity >= 0)
 
-(define-for-syntax ((mk-type-alias-rewriter xs body) stx)
-  (syntax-parse stx
-    [(_ ty ...)
-     (type-eval (substs #'(ty ...) xs body))]))
-
 ;; τ.norm in 1st case causes "not valid type" error when referring to ⊥ in another file.
 ;; however, this version expands the type at every reference, incurring a potentially large
 ;; overhead---2x in the case of book-club.rkt
@@ -484,11 +432,17 @@
 (define-syntax define-type-alias
   (syntax-parser
     [(_ alias:id τ:type)
+     ;; #:with kind (detach #'τ.norm ':)
      #:with serialized-τ (serialize-syntax #'τ.norm)
      #'(define-syntax- alias
          (make-variable-like-transformer (deserialize-syntax #'serialized-τ)))]
     [(_ (f:id x:id ...) ty)
-     #'(define-syntax- f (mk-type-alias-rewriter #'(x ...) #'ty))]))
+     #'(define-syntax- (f stx)
+         (syntax-parse stx
+           [(_ x ...)
+            #'ty
+            ;; #:with τ:any-type #'ty
+            #;#'τ.norm]))]))
 
 (define-type-alias ⊥ (U*))
 (define-type-alias Unit (Tuple))
@@ -621,7 +575,7 @@
     (pattern (~seq #:type-constructor TypeCons:id))
     (pattern (~seq) #:attr TypeCons #f))
 
-  (struct user-ctor (typed-ctor untyped-ctor type-tag type-ctor field-ids)
+  (struct user-ctor (typed-ctor untyped-ctor type-tag)
     #:property prop:procedure
     (lambda (v stx)
       (define transformer (user-ctor-typed-ctor v))
@@ -638,29 +592,6 @@
          #:type-constructor TyCons
          clause ...)]))
 
-(begin-for-syntax
-  (define ((mk-type-params-fetcher TypeCons) ty)
-    (syntax-parse ty
-      [(_ (~Any/new τcons t ...))
-       #:when (free-identifier=? #'τcons TypeCons)
-       #'(t ...)]))
-
-  (define ((mk-constructor-type-rule arity StructName TypeCons) stx)
-    (syntax-parse/typecheck stx
-      [(_ e ...) ≫
-       #:fail-unless (= arity (stx-length #'(e ...))) "arity mismatch"
-       [⊢ e ≫ e- (⇒ : τ)] ...
-       #:fail-unless (all-pure? #'(e- ...)) "expressions must be pure"
-       ----------------------
-       [⊢ (#%app- #,StructName e- ...) (⇒ : (#,TypeCons τ ...))]])))
-
-(define-for-syntax ((resugar-ctor ty-cons) t)
-  ;; because typedefs defines 0-arity constructors as base types,
-  ;; make a custom resugar that always parenthesizes constructors
-  (syntax-parse t
-    [(~Any/new _ args ...)
-     (cons ty-cons (stx-map resugar-type #'(args ...)))]))
-
 (define-syntax (define-constructor stx)
   (syntax-parse stx
     [(_ (Cons:id slot:id ...)
@@ -673,52 +604,34 @@
      #: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 ...))])
-                             (format-id slot-name "~a-~a" #'Cons slot-name))
-     #:with (accessor- ...) (for/list ([slot-name (in-syntax #'(slot ...))])
-                              (format-id #'StructName "~a-~a" #'StructName slot-name))
-     #:with (acc-defs ...) (mk-accessors #'(accessor ...) #'(accessor- ...) #'TypeCons #'(slot ...))
      (define arity (stx-length #'(slot ...)))
      #`(begin-
          (struct- StructName (slot ...) #:reflection-name 'Cons #:transparent)
          (define-for-syntax (TypeConsExtraInfo stx)
-           (list #'type-tag #'MakeTypeCons #'GetTypeParams))
+           (list #'type-tag #'MakeTypeCons #'GetTypeParams)
+           #;(syntax-parse stx
+             [(_ X (... ...)) #'(#%app- 'type-tag 'MakeTypeCons 'GetTypeParams)]))
          (define-product-type TypeCons
            #:arity = #,arity
-           #:extra-info TypeConsExtraInfo
-           #:implements get-resugar-info (resugar-ctor #'TypeCons))
-         (define-type-alias Alias AliasBody) ...
-         (define-syntax MakeTypeCons (mk-ctor-rewriter #'TypeCons))
-         (define-syntax GetTypeParams (mk-type-params-fetcher #'TypeCons))
+           #:extra-info TypeConsExtraInfo)
+         (define-syntax (MakeTypeCons stx)
+           (syntax-parse stx
+             [(_ . ts)
+              #:fail-unless (= #,arity (stx-length #'ts)) "arity mismatch"
+              #'(TypeCons . ts)]))
+         (define-syntax (GetTypeParams stx)
+           (syntax-parse stx
+             [(_ (~Any/new (~literal TypeCons) t (... ...)))
+              #'(t (... ...))]))
          (define-syntax Cons
-           (user-ctor #'Cons- #'StructName 'type-tag #'TypeCons (list #'accessor ...)))
-         (define-syntax Cons- (mk-constructor-type-rule #,arity #'StructName #'TypeCons))
-         #,@(mk-accessors #'(accessor ...) #'(accessor- ...) #'TypeCons #'(slot ...)))]))
-
-(define-for-syntax (mk-accessors accessors accessors- TypeCons slots)
-  (for/list ([accessor (in-syntax accessors)]
-             [accessor- (in-syntax accessors-)]
-             [slot (in-syntax slots)])
-    (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)
-  (syntax-parse stx
-    [(_ ucons:id)
-     (define accs (cleanup-accs #'ucons accs/rev))
-     (define accs- (map mk-- accs))
-     (define slots (generate-temporaries accs))
-     (define renames (for/list ([acc (in-list accs)]
-                                [acc- (in-list accs-)])
-                       #`[#,acc #,acc-]))
-     (quasisyntax/loc TypeCons
-       (begin-
-         (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))])
-    (format-id ucons "~a" (syntax-e acc))))
+           (user-ctor #'Cons- #'StructName 'type-tag))
+         (define-typed-syntax (Cons- e (... ...)) ≫
+           #:fail-unless (= #,arity (stx-length #'(e (... ...)))) "arity mismatch"
+           [⊢ e ≫ e- (⇒ : τ)] (... ...)
+           #:fail-unless (all-pure? #'(e- (... ...))) "expressions must be pure"
+           ----------------------
+           [⊢ (#%app- StructName e- (... ...)) (⇒ : (TypeCons τ (... ...)))])
+         (define-type-alias Alias AliasBody) ...)]))
 
 ;; (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
@@ -729,7 +642,7 @@
 ;; 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)
      (with-syntax* ([TypeCons #'ty-cons]
                     [MakeTypeCons (format-id #'TypeCons "make-~a" #'TypeCons)]
                     [GetTypeParams (format-id #'TypeCons "get-~a-type-params" #'TypeCons)]
@@ -745,34 +658,38 @@
              (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 (false? (last accs/rev))
+             (match-define (list desc cons pred accs muts sup) (extract-struct-info info))
+             (when (false? (last accs))
                (raise-syntax-error #f "number of slots must be exact" #'#,stx #'ucons))
-             (unless (boolean? sup)
+             (unless (equal? #t sup)
                (raise-syntax-error #f "structs with super-type not supported" #'#,stx #'ucons))
-             (define arity (length accs/rev))
-             )
+             (define arity (length accs)))
            (define-for-syntax (TypeConsExtraInfo stx)
              (list #'type-tag #'MakeTypeCons #'GetTypeParams)
-             )
+             #;(syntax-parse stx
+               [(_ X (... ...)) #'(#%app- 'type-tag 'MakeTypeCons 'GetTypeParams)]))
            (define-product-type TypeCons
              ;; issue: arity needs to parse as an exact-nonnegative-integer
              ;; fix: check arity in MakeTypeCons
              #:arity >= 0
-             #:extra-info TypeConsExtraInfo
-             #:implements get-resugar-info (resugar-ctor #'TypeCons))
-           (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))
+             #:extra-info TypeConsExtraInfo)
+           (define-syntax (MakeTypeCons stx)
+             (syntax-parse stx
+               [(_ t (... ...))
+                #:fail-unless (= arity (stx-length #'(t (... ...)))) "arity mismatch"
+                #'(TypeCons t (... ...))]))
+           (define-syntax (GetTypeParams stx)
+             (syntax-parse stx
+               [(_ (~Any/new (~literal TypeCons) t (... ...)))
+                #'(t (... ...))]))
+           (define-typed-syntax (Cons- e (... ...)) ≫
+             #:fail-unless (= arity (stx-length #'(e (... ...)))) "arity mismatch"
+             [⊢ e ≫ e- (⇒ : τ)] (... ...)
+             #:fail-unless (all-pure? #'(e- (... ...))) "expressions must be pure"
+             ----------------------
+             [⊢ (#%app- orig-struct-info e- (... ...)) (⇒ : (TypeCons τ (... ...)))])
            (define-syntax ucons
-             (user-ctor #'Cons- #'orig-struct-info 'type-tag #'TypeCons (cleanup-accs #'ucons accs/rev)))
-           #,(unless (attribute omit-accs)
-               (quasisyntax/loc stx
-                 (begin-
-                   (define-syntax mk-struct-accs
-                     (define-struct-accs accs/rev #'TypeCons #'lib))
-                   (mk-struct-accs ucons))))
-           )))]))
+             (user-ctor #'Cons- #'orig-struct-info 'type-tag)))))]))
 
 (begin-for-syntax
   (define-syntax ~constructor-extra-info
@@ -797,7 +714,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 ...)))]))
@@ -810,19 +727,30 @@
 
   (define (get-type-tag t)
     (match (get-extra-info/new t)
-      [(list tag _ _) tag]))
+      [(list tag _ _) tag])
+    #;(syntax-parse (get-extra-info t)
+      [(~constructor-extra-info tag _ _)
+       (syntax-e #'tag)]))
 
   (define (get-type-args t)
     (match  (get-extra-info/new t)
       [(list _ _ get)
        (define f (syntax-local-value get))
-       (syntax->list (f #`(#,get #,t)))]))
+       (syntax->list (f #`(#,get #,t)))])
+    #;(syntax-parse (get-extra-info t)
+      [(~constructor-extra-info _ _ get)
+       (define f (syntax-local-value #'get))
+       (syntax->list (f #`(get #,t)))]))
 
   (define (make-cons-type t args)
     (match  (get-extra-info/new t)
       [(list _ mk _)
        (define f (syntax-local-value mk))
-       (type-eval (f #`(#,mk #,@args)))]))
+       (type-eval (f #`(#,mk #,@args)))])
+    #;(syntax-parse (get-extra-info t)
+      [(~constructor-extra-info _ mk _)
+       (define f (syntax-local-value #'mk))
+        (type-eval (f #`(mk #,@args)))]))
 
   (define (ctor-id? stx)
     (and (identifier? stx)
@@ -840,32 +768,21 @@
 ;; Require & Provide
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-(begin-for-syntax
-  (define-syntax-class opaque-require-clause
-    #:datum-literals (= > >=)
-    #:attributes (type-definition)
-    (pattern [#:opaque ty-name:id]
-             #:attr type-definition #'(define-base-type ty-name))
-    (pattern [#:opaque ty-name:id #:arity (~and op (~or* = > >=)) arity:nat]
-             #:attr type-definition #'(define-product-type ty-name #:arity op arity))))
-
 ;; Import and ascribe a type from an untyped module
 ;; TODO: this is where contracts would need to go
 (define-syntax (require/typed stx)
   (syntax-parse stx
     #:datum-literals (:)
-    [(_ lib
-        (~alt [name:id : ty]
-              opaque-clause:opaque-require-clause)
-        ...)
+    [(_ lib [name:id : ty:type] ...)
      #:with (name- ...) (format-ids "~a-" #'(name ...))
+     #:with (serialized-ty ...) (for/list ([t (in-syntax #'(ty.norm ...))])
+                                  (serialize-syntax t))
      (syntax/loc stx
        (begin-
-         opaque-clause.type-definition ...
          (require (only-in lib [name name-] ...))
          (define-syntax name
            (make-variable-like-transformer
-            (add-orig (assign-type #'name- (deserialize-syntax (serialize-syntax (type-eval #'ty)))
+            (add-orig (assign-type #'name- (deserialize-syntax #'serialized-ty)
                                    #:wrap? #f) #'name)))
          ...))]))
 
@@ -883,18 +800,6 @@
     (match-define (list name- ty name) (syntax->list iti))
     (add-orig (assign-type name- ty #:wrap? #f) name)))
 
-(define-syntax struct-out
-  (make-provide-transformer
-   (lambda (stx modes)
-     (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 (list* #'ctor (user-ctor-type-ctor val) accs))])
-          (make-export f (syntax-e f) (syntax-local-phase-level) #f f))]))))
-
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Conveniences
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -916,10 +821,37 @@
 ;; Syntax
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-(require-struct observe #:as Observe #:from syndicate/patch)
-(require-struct inbound #:as Inbound #:from syndicate/protocol/standard-relay)
-(require-struct outbound #:as Outbound #:from syndicate/protocol/standard-relay)
-(require-struct message #:as Message #:from syndicate/core)
+(require-struct observe #:as Observe #:from syndicate/actor-lang)
+(require-struct inbound #:as Inbound #:from syndicate/actor-lang)
+(require-struct outbound #:as Outbound #:from syndicate/actor-lang)
+(require-struct message #:as Message #:from syndicate/actor-lang)
+
+(begin-for-syntax
+
+  ;; constructors with arity one
+  (define-syntax-class kons1
+    (pattern (~or (~datum observe)
+                  (~datum inbound)
+                  (~datum outbound)
+                  (~datum message))))
+
+  (define (kons1->constructor stx)
+    (syntax-parse stx
+      #:datum-literals (observe inbound outbound)
+      [observe #'syndicate:observe]
+      [inbound #'syndicate:inbound]
+      [outbound #'syndicate:outbound]
+      [message #'syndicate:message]))
+
+  (define-syntax-class basic-val
+    (pattern (~or boolean
+                  integer
+                  string)))
+
+  (define-syntax-class prim-op
+    (pattern (~or (~literal +)
+                  (~literal -)
+                  (~literal displayln)))))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Utilities Over Types
@@ -935,7 +867,7 @@
 (define-for-syntax (flat-type? τ)
   (syntax-parse τ
     [(~→+ i ... o) #f]
-    [(~AnyActor τ) #f]
+    [(~Actor τ) #f]
     [(~Role+Body (_) _ ...) #f]
     [_ #t]))
 
@@ -1013,7 +945,7 @@
     [(~Stop name:id τ-r ...)
      #:with (τ-i τ-o τ-i/i τ-o/i τ-a) (analyze-roles #'(τ-r ...))
      (values #'τ-i #'τ-o #'τ-i/i #'τ-o/i #'τ-a)]
-    [(~AnyActor τc)
+    [(~Actor τc)
      (values bot bot bot bot t)]
     [(~Sends τ-m)
      (values bot (mk-Message- #'(τ-m)) bot bot bot)]
@@ -1098,13 +1030,6 @@
      (reassemble-type #'τ-cons subitems)]
     [_ t]))
 
-;; Type -> Bool
-;; to prevent observing the linkage assertions used by during/spawn,
-;; disallow ?★ and ??★
-(define-for-syntax (allowed-interest? t)
-  (not (or (<: (type-eval #'(Observe ★/t)) t)
-           (<: (type-eval #'(Observe (Observe ★/t))) t))))
-
 ;; Type -> String
 (define-for-syntax (type->strX ty)
   ;; Identifier -> String
@@ -1171,7 +1096,7 @@
       (stx-andmap (lambda (t) (<: t t2)) #'(τ1 ...))]
      [(_ (~U* τ2 ...))
       (stx-ormap (lambda (t) (<: t1 t)) #'(τ2 ...))]
-     [((~AnyActor τ1) (~AnyActor τ2))
+     [((~Actor τ1) (~Actor τ2))
       (and (<: #'τ1 #'τ2)
            (<: (∩ (strip-? #'τ1) #'τ2) #'τ1))]
      [((~proc τ-in1 ... -> τ-out1 #:spawns (~seq S1 ...)
@@ -1183,9 +1108,7 @@
       (and (stx-length=? #'(τ-in1 ...) #'(τ-in2 ...))
            (stx-andmap <: #'(τ-in2 ...) #'(τ-in1 ...))
            (<: #'τ-out1 #'τ-out2)
-           ;; TODO!
-           (<: (mk-U*- #'(S1 ...)) (mk-U*- #'(S2 ...)))
-           #;(<: (mk-Actor- (list (mk-U*- #'(S1 ...))))
+           (<: (mk-Actor- (list (mk-U*- #'(S1 ...))))
                (mk-Actor- (list (mk-U*- #'(S2 ...)))))
            (<: (mk-U*- #'(R1 ...))
                (mk-U*- #'(R2 ...)))
@@ -1194,13 +1117,31 @@
      [(~Discard _)
       #t]
      [(X:id Y:id)
-      (free-identifier=? #'X #'Y)]
+      (or (free-identifier=? #'X #'Y)
+          #;(let ()
+            (printf "X:\n")
+            (pretty-print (syntax-debug-info (values #;syntax-local-introduce #'X)))
+            (pretty-print (identifier-binding #'X))
+            (printf ":\n")
+            (pretty-print (syntax-debug-info (values #;syntax-local-introduce #'Y)))
+            (pretty-print (identifier-binding #'Y))
+            #f))]
      [((~∀+ (X:id ...) τ1) (~∀+ (Y:id ...) τ2))
       #:when (stx-length=? #'(X ...) #'(Y ...))
       #:with τ2-X/Y (substs #'(X ...) #'(Y ...) #'τ2)
+      ;; #:do [(displayln "∀ <: ∀")
+            ;; (displayln #'τ2-X/Y)]
       (<: #'τ1 #'τ2-X/Y)]
      [((~Base τ1:id) (~Base τ2:id))
-      (free-identifier=? #'τ1 #'τ2)]
+      (or (free-identifier=? #'τ1 #'τ2)
+          (let ()
+            (printf "τ1:\n")
+            (pretty-print (syntax-debug-info (values #;syntax-local-introduce #'τ1)))
+            (pretty-print (identifier-binding #'τ1))
+            (printf "τ2:\n")
+            (pretty-print (syntax-debug-info (values #;syntax-local-introduce #'τ2)))
+            (pretty-print (identifier-binding #'τ2))
+            #f))]
      [((~Role+Body (x) _ ...) (~Role+Body (y) _ ...))
       ;; Extremely Coarse subtyping for Role types
       (type=? t1 t2)]
@@ -1379,8 +1320,6 @@
                                                           (Roles τ-f ...)
                                                           (Spawns τ-s ...))))])
 
-(define-syntax λ (make-variable-like-transformer #'lambda))
-
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Type Abstraction
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -1414,6 +1353,10 @@
       (and (flat-type? ty)
            (finite? ty))))
 
+#;(begin-for-syntax
+  (require racket/trace)
+  (trace instantiable?))
+
 (begin-for-syntax
   ;; CONVENTION: Type variables for effects are prefixed with ρ
   (define (row-variable? x)
@@ -1455,16 +1398,14 @@
 (define-for-syntax (int-def-ctx-bind-type-rename x x- t ctx)
   (when DEBUG-BINDINGS?
     (printf "adding to context ~a\n" (syntax-debug-info x)))
-  ;; at some point these serialize/deserialze-syntax calls seemed to fix an issue, but
-  ;; in principle it doesn't seem like they should be necessary and things seem to be
-  ;; working w/o them *shrug*
-  (define serialized-ty (values #;serialize-syntax t))
+  (define serialized-ty (serialize-syntax t))
   (syntax-local-bind-syntaxes (list x-) #f ctx)
   (syntax-local-bind-syntaxes (list x)
                               #`(make-rename-transformer
                                  (add-orig
-                                  (attach #'#,x- ': (values #;deserialize-syntax #'#,serialized-ty))
-                                  #'#,x))
+                                  (attach #'#,x- ': (deserialize-syntax #'#,serialized-ty))
+                                  #'#,x)
+                                 #;(add-orig (assign-type #'#,x- #'#,t #:wrap? #f) #'#,x))
                               ctx))
 
 (define-for-syntax (add-bindings-to-ctx e- def-ctx)
@@ -1543,6 +1484,8 @@
     [(_ [x:id x-:id τ e-] ...)
      #'(syndicate:field [x- e-] ...)]))
 
+(define-for-syntax KIND-TAG ':)
+
 (define-syntax (define/intermediate stx)
   (syntax-parse stx
     [(_ x:id x-:id τ e)
@@ -1554,6 +1497,7 @@
            (make-variable-like-transformer (add-orig (attach #'x- ': (deserialize-syntax #'serialized-τ)) #'x)))
          (define- x- e))]))
 
+;; copied from ext-stlc
 (define-typed-syntax define
   [(_ x:id (~datum :) τ:type e:expr) ≫
    #:cut
@@ -1604,24 +1548,31 @@
                      (~or (~datum →) (~datum ->)) ty_out))
       e ...+) ≫
    #:cut
+   #:do [(displayln 'A)]
    #:with e+ #'(Λ (X ...)
                   (lambda ([x : ty] ...)
                     (block e ...)))
+   #:do [(displayln 'B)]
    [[X ≫ X- : Type] ... ⊢ e+ ≫ e- (⇒ : TTTT)
                        #;(⇒ : (~and res-ty
                                   (~∀+ (Y ...)
                                       (~→ (~not (~Computation _ _ _ _)) ...
                                           (~Computation (~Value τ-v) _ _ _)))))]
+   #:do [(displayln 'C)
+         (local-require turnstile/typedefs)
+         (pretty-print (resugar-type #'TTTT))]
    #:with (~and res-ty
                 (~∀+ (Y ...)
                      (~→+ (~not (~Computation _ _ _ _)) ...
                           (~Computation (~Value τ-v) _ _ _)))) #'TTTT
+   #:do [(displayln 'D)]
    #:with ty_out- (substs #'(X- ...) #'(X ...) #'ty_out)
    #:with actual (type-eval #'(∀+ (Y ...) τ-v))
    #:with expected (type-eval #'(∀+ (X- ...) ty_out-))
    #:fail-unless (<: #'actual #'expected)
                  (format "expected different return type\n got ~a\n expected ~a\n"
                          (resugar-type #'actual) (resugar-type #'expected))
+   #:do [(displayln 'E)]
    #:with f- (add-orig (generate-temporary #'f) #'f)
    -------------------------------------------------------
    [⊢ (erased (define/intermediate f f- res-ty e-)) (⇒ : ★/t)]]
@@ -1669,6 +1620,7 @@
    [⊢ e_fn ≫ e_fn- ⇒ (~∀+ Xs (~→fn tyX_in ... tyX_out))]
    ;; successfully matched a polymorphic fn type, don't backtrack
    #:cut
+   #:do [(printf "A\n")]
    #:with tyX_args #'(tyX_in ... tyX_out)
    ;; solve for type variables Xs
    #:with [[e_arg- ...] Xs* cs] (solve #'Xs #'tyX_args this-syntax)
@@ -1679,6 +1631,7 @@
                    (instantiable? x ty))
                  "type variables must be flat and finite"
    ;; instantiate polymorphic function type
+   #:do [(printf "B\n")]
    #:with [τ_in ... τ_out] (ttc:inst-types/cs #'Xs* #'cs #'tyX_args)
    #:with (unsolved-X ...) (find-free-Xs #'Xs* #'τ_out)
    ;; arity check
@@ -1690,6 +1643,7 @@
    #:with (τ_arg ...) (stx-map typeof #'(e_arg- ...))
    ;; typecheck args
    [τ_arg τ⊑ τ_in #:for e_arg] ...
+   #:do [(printf "C\n")]
    #:with τ_out* (if (stx-null? #'(unsolved-X ...))
                      #'τ_out
                      (syntax-parse #'τ_out
@@ -1703,6 +1657,7 @@
                              (mk-app-poly-infer-error this-syntax #'(τ_in ...) #'(τ_arg ...) #'e_fn)
                              this-syntax)))
                         (type-eval #'(∀+ (unsolved-X ... Y ...) τ_out))]))
+   #:do [(printf "D\n")]
    --------
    [⊢ (#%plain-app- e_fn- e_arg- ...) ⇒ τ_out*]]
   ;; All Other Functions
@@ -1863,3 +1818,17 @@
        (stx-map (λ _ irrelevant) Xs)]
       [_ (stx-map (λ _ invariant) Xs)])))
 
+#;(begin-for-syntax
+  (define t #'Unit)
+  (define t- ((current-type-eval) t))
+  (displayln ((current-type?) t-))
+  (define tt (syntax-parse (detach t- ':)
+               [(#%plain-app x) #'x]))
+  (pretty-print (syntax-debug-info tt)))
+
+#;(begin-for-syntax
+  (define t #'(→ Unit Unit))
+  #;(define t #'(Actor Unit))
+  (define t- ((current-type-eval) t))
+  (values #;displayln ((current-type?) t-))
+  (printf "flat-type? ~a\n" (flat-type? t-)))

racket/typed/either.rkt

@@ -19,17 +19,21 @@
   (U (Left A)
      (Right B)))
 
+(define (∀ (X) (f [x : X] -> X))
+  x)
+
+
 (define (∀ (X Y Z) (partition/either [xs : (List X)]
-                                     [pred : (→fn X (Either Y Z))]
+                                     [pred : (→fn X (U (Left Y)
+                                                       (Right Z)) #;(Either Y Z))]
                                      -> (Tuple (List Y) (List Z))))
-  (for/fold ([lefts (List Y) (list)]
-             [rights (List Z) (list)])
+  (for/fold ([acc (Tuple (List Y) (List Z)) (tuple (list) (list))])
             ([x xs])
     (define y-or-z (pred x))
     (match y-or-z
       [(left (bind y Y))
-       (tuple (cons y lefts)
-              rights)]
+       (tuple (cons y (select 0 acc))
+              (select 1 acc))]
       [(right (bind z Z))
-       (tuple lefts
-              (cons z rights))])))
+       (tuple (select 0 acc)
+              (cons z (select 1 acc)))])))

racket/typed/example.rkt

@@ -0,0 +1,27 @@
+#lang typed/syndicate
+
+(define-type-alias ds-type
+   (U (Observe (Tuple String ★)) (Tuple String Int)))
+
+(dataspace ds-type
+
+           (spawn ds-type
+                  (facet _
+                         (fields [the-thing Int 0])
+                         (assert (tuple "the thing" (ref the-thing)))
+                         (on (asserted (tuple "set thing" (bind new-v Int)))
+                             (set! the-thing new-v))))
+
+           (spawn ds-type
+                  (let [k (λ [10 (begin)]
+                            [(bind x Int)
+                             (facet _ (fields)
+                                    (assert (tuple "set thing" (+ x 1))))])]
+                    (facet _ (fields)
+                           (on (asserted (tuple "the thing" (bind x Int)))
+                               (k x)))))
+
+           (spawn ds-type
+                  (facet _ (fields)
+                         (on (asserted (tuple "the thing" (bind t Int)))
+                             (displayln t)))))

racket/typed/examples/bank-account.rkt

@@ -1,19 +1,14 @@
 #lang typed/syndicate
 
-;; Expected Output
-;; 0
-;; 70
-;; #f
-
 (define-constructor (account balance)
   #:type-constructor AccountT
   #:with Account (AccountT Int)
-  #:with AccountRequest (AccountT ★/t))
+  #:with AccountRequest (AccountT ★))
 
 (define-constructor (deposit amount)
   #:type-constructor DepositT
   #:with Deposit (DepositT Int)
-  #:with DepositRequest (DepositT ★/t))
+  #:with DepositRequest (DepositT ★))
 
 (define-type-alias ds-type
   (U Account
@@ -23,43 +18,45 @@
      (Observe DepositRequest)
      (Observe (Observe DepositRequest))))
 
-(define-type-alias account-manager-role
-  (Role (account-manager)
-        (Shares Account)
-        (Reacts (Asserted Deposit))))
+(dataspace ds-type
 
-(define-type-alias client-role
-  (Role (client)
-        (Reacts (Asserted Account))))
+           (spawn ds-type
+                  (facet _
+                         (fields [balance Int 0])
+                         (assert (account (ref balance)))
+                         (on (asserted (deposit (bind amount Int)))
+                             (set! balance (+ (ref balance) amount)))))
 
+           (spawn ds-type
+                  (facet _
+                         (fields)
+                         (on (asserted (account (bind amount Int)))
+                             (displayln amount))))
 
-(run-ground-dataspace ds-type
+           (spawn ds-type
+                  (facet _
+                         (fields)
+                         (on (asserted (observe (deposit discard)))
+                               (facet _
+                                      (fields)
+                                      (assert (deposit 100))
+                                      (assert (deposit -30)))))))
 
-  (spawn ds-type
-    (lift+define-role acct-mngr-role
-    (start-facet account-manager
-      (field [balance Int 0])
-      (assert (account (ref balance)))
-      (on (asserted (deposit (bind amount Int)))
-          (set! balance (+ (ref balance) amount))))))
+#|
+;; Hello-worldish "bank account" example.
 
-  (spawn ds-type
-    (lift+define-role obs-role
-    (start-facet observer
-      (on (asserted (account (bind amount Int)))
-          (displayln amount)))))
+(struct account (balance) #:prefab)
+(struct deposit (amount) #:prefab)
 
-  (spawn ds-type
-    (lift+define-role buyer-role
-    (start-facet buyer
-      (on (asserted (observe (deposit discard)))
-          (start-facet deposits
-            (assert (deposit 100))
-            (assert (deposit -30))))))))
+(spawn (field [balance 0])
+       (assert (account (balance)))
+       (on (message (deposit $amount))
+           (balance (+ (balance) amount))))
 
-(module+ test
-  (check-simulates acct-mngr-role account-manager-role)
-  (check-simulates obs-role client-role)
-  ;; Tried to write this, then it failed, I looked and buyer doesn't actually implement that spec
-  #;(check-simulates buyer-role client-role)
-  )
+(spawn (on (asserted (account $balance))
+           (printf "Balance changed to ~a\n" balance)))
+
+(spawn* (until (asserted (observe (deposit _))))
+        (send! (deposit +100))
+        (send! (deposit -30)))
+|#

racket/typed/examples/ping-pong.rkt

@@ -1,36 +0,0 @@
-#lang typed/syndicate
-
-;; Expected Output
-;; pong: 8339
-
-(message-struct ping : Ping (v))
-(message-struct pong : Pong (v))
-
-(define-type-alias ds-type
-  (U (Message (Ping Int))
-     (Message (Pong Int))
-     (Observe (Ping ★/t))
-     (Observe (Pong ★/t))
-     (Observe (Observe (Ping ★/t)))))
-
-(run-ground-dataspace ds-type
-  (spawn ds-type
-    (lift+define-role ponger
-    (start-facet echo
-      (on (message (ping $v))
-          (send! (pong v))))))
-  (spawn ds-type
-    (lift+define-role pinger
-    (start-facet serve
-      (on (asserted (observe (ping _)))
-          (send! (ping 8339)))
-      (on (message (pong $x))
-          (printf "pong: ~v\n" x))))))
-
-(module+ test
-  (verify-actors (And (Eventually (M (Ping Int)))
-                      (Eventually (M (Pong Int)))
-                      (Always (Implies (M (Ping Int))
-                                       (Eventually (M (Pong Int))))))
-                 pinger
-                 ponger))

racket/typed/examples/require-struct/omit-accs/lib.rkt

@@ -1,12 +0,0 @@
-#lang racket
-
-(struct egg (size day) #:transparent)
-
-(provide (except-out (struct-out egg)
-                     egg-size
-                     egg-day))
-
-
-(struct chicken (eggs) #:transparent)
-
-(provide chicken)

racket/typed/examples/require-struct/omit-accs/require-omit-accs.rkt

@@ -1,18 +0,0 @@
-#lang typed/syndicate/roles
-
-(require-struct egg #:as Egg #:from "lib.rkt" #:omit-accs)
-
-(define e (egg 5 "Sun"))
-
-(match e
-  [(egg $sz $d)
-   (displayln sz)
-   (displayln d)])
-
-(require-struct chicken #:as Chicken #:from "lib.rkt" #:omit-accs)
-
-(define c (chicken (list e e e)))
-
-(match c
-  [(chicken $eggs)
-   (displayln eggs)])

racket/typed/examples/require:typed/client.rkt

@@ -1,5 +0,0 @@
-#lang typed/syndicate
-
-(require/typed "lib.rkt" [x : Int])
-
-(displayln (+ x 1))

racket/typed/examples/require:typed/opaque/client-arity.rkt

@@ -1,8 +0,0 @@
-#lang typed/syndicate
-
-(require/typed "lib.rkt"
-  [#:opaque Vec #:arity = 3]
-  [ones : (Vec Int Int Int)]
-  [vec+ : (→fn (Vec Int Int Int) (Vec Int Int Int) (Vec Int Int Int))])
-
-(vec+ ones ones)

racket/typed/examples/require:typed/opaque/client.rkt

@@ -1,8 +0,0 @@
-#lang typed/syndicate
-
-(require/typed "lib.rkt"
-  [#:opaque Vec]
-  [ones : Vec]
-  [vec+ : (→fn Vec Vec Vec)])
-
-(vec+ ones ones)

racket/typed/examples/require:typed/opaque/lib.rkt

@@ -1,13 +0,0 @@
-#lang racket
-
-(provide ones
-         vec+)
-
-(struct vec (x y z) #:transparent)
-
-(define ones (vec 1 1 1))
-
-(define (vec+ v1 v2)
-  (vec (+ (vec-x v1) (vec-x v2))
-       (+ (vec-y v1) (vec-y v2))
-       (+ (vec-z v1) (vec-z v2))))

racket/typed/examples/requires.rkt

@@ -1,5 +0,0 @@
-#lang typed/syndicate
-
-(require "provides.rkt")
-
-(a-fun 5)

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

@@ -0,0 +1,57 @@
+#lang typed/syndicate/roles
+
+;; Expected Output
+;; 0
+;; 70
+;; #f
+
+(define-constructor (account balance)
+  #:type-constructor AccountT
+  #:with Account (AccountT Int)
+  #:with AccountRequest (AccountT ★/t))
+
+(define-constructor (deposit amount)
+  #:type-constructor DepositT
+  #:with Deposit (DepositT Int)
+  #:with DepositRequest (DepositT ★/t))
+
+(define-type-alias ds-type
+  (U Account
+     (Observe AccountRequest)
+     (Observe (Observe AccountRequest))
+     Deposit
+     (Observe DepositRequest)
+     (Observe (Observe DepositRequest))))
+
+(define-type-alias account-manager-role
+  (Role (account-manager)
+        (Shares Account)
+        (Reacts (Know (Deposit Int)))))
+
+(define-type-alias client-role
+  (Role (client)
+        (Reacts (Know Account))))
+
+(run-ground-dataspace ds-type
+
+  (spawn ds-type
+    (print-role
+    (start-facet account-manager
+      (field [balance Int 0])
+      (assert (account (ref balance)))
+      (on (asserted (deposit (bind amount Int)))
+          (set! balance (+ (ref balance) amount))))))
+
+  (spawn ds-type
+    (print-role
+    (start-facet observer
+      (on (asserted (account (bind amount Int)))
+          (displayln amount)))))
+
+  (spawn ds-type
+    (print-role
+    (start-facet buyer
+      (on (asserted (observe (deposit discard)))
+          (start-facet deposits
+            (assert (deposit 100))
+            (assert (deposit -30))))))))

racket/typed/examples/roles/book-club.rkt

@@ -1,4 +1,4 @@
-#lang typed/syndicate
+#lang typed/syndicate/roles
 
 ;; Expected Output
 ;; leader learns that there are 5 copies of The Wind in the Willows
@@ -59,19 +59,17 @@
            (Role (_)
                  ;; nb no mention of retracting this assertion
                  (Shares (BookQuoteT String Int))))))
-(export-type "seller-role.rktd" seller-role)
 
 (define (spawn-seller [inventory : Inventory])
   (spawn τc
-    (export-roles "seller-impl.rktd"
-    (lift+define-role seller-impl
+    (begin
     (start-facet seller
       (field [books Inventory inventory])
 
       ;; Give quotes to interested parties.
       (during (observe (book-quote $title _))
         ;; TODO - lookup
-        (assert (book-quote title (lookup title (ref books))))))))))
+        (assert (book-quote title (lookup title (ref books)))))))))
 
 (define-type-alias leader-role
   (Role (leader)
@@ -79,16 +77,16 @@
                 (Role (poll)
                       (Reacts (Asserted (BookInterestT String String Bool))
                               ;; this is actually implemented indirectly through dataflow
-                              (Branch (Stop leader
-                                            (Role (_)
-                                                  (Shares (BookOfTheMonthT String))))
-                                      (Stop poll)))))))
+                              (U (Stop leader
+                                       (Role (_)
+                                             (Shares (BookOfTheMonthT String))))
+                                 (Stop poll)))))))
 
 (define-type-alias leader-actual
-  (Role (get-quotes)
+  (Role (get-quotes31)
         (Reacts (Asserted (BookQuoteT String (Bind Int)))
                 (Stop get-quotes)
-                (Role (poll-members)
+                (Role (poll-members36)
                       (Reacts OnDataflow
                               (Stop poll-members
                                     (Stop get-quotes))
@@ -104,8 +102,7 @@
 
 (define (spawn-leader [titles : (List String)])
   (spawn τc
-   (export-roles "leader-impl.rktd"
-   (lift+define-role leader-impl
+   (print-role
    (start-facet get-quotes
      (field [book-list (List String) (rest titles)]
             [title String (first titles)])
@@ -157,7 +154,7 @@
                (when (> (set-count (ref nays))
                         (/ (set-count (ref members)) 2))
                  (printf "leader finds enough negative nancys for ~a\n" (ref title))
-                 (stop poll-members (next-book)))))])))))))
+                 (stop poll-members (next-book)))))]))))))
 
 (define-type-alias member-role
   (Role (member)
@@ -170,8 +167,7 @@
 (define (spawn-club-member [name : String]
                            [titles : (List String)])
   (spawn τc
-   (export-roles "member-impl.rktd"
-   (lift+define-role member-impl
+   (print-role
    (start-facet member
      ;; assert our presence
      (assert (club-member name))
@@ -179,7 +175,7 @@
      (during (observe (book-interest $title _ _))
        (define answer (member? title titles))
        (printf "~a responds to suggested book ~a: ~a\n" name title answer)
-       (assert (book-interest title name answer))))))))
+       (assert (book-interest title name answer)))))))
 
 (run-ground-dataspace τc
   (spawn-seller (list (tuple "The Wind in the Willows" 5)
@@ -191,19 +187,3 @@
                       "Encyclopaedia Brittannica"))
   (spawn-club-member "tony" (list "Candide"))
   (spawn-club-member "sam" (list "Encyclopaedia Brittannica" "Candide")))
-
-(module+ test
-  (verify-actors (And (Eventually (A BookQuote))
-                      (Always (Implies (A (Observe (BookQuoteT String ★/t)))
-                                       (Eventually (A BookQuote))))
-                      (Always (Implies (A (Observe (BookInterestT String ★/t ★/t)))
-                                       (Eventually (A BookInterest)))))
-                 leader-impl
-                 seller-impl
-                 member-impl))
-
-(module+ test
-  (check-simulates leader-impl leader-impl)
-  (check-has-simulating-subgraph leader-impl leader-role)
-  (check-simulates seller-impl seller-impl)
-  (check-has-simulating-subgraph seller-impl seller-role))

racket/typed/examples/roles/cell.rkt

@@ -1,4 +1,4 @@
-#lang typed/syndicate
+#lang typed/syndicate/roles
 
 ;; adapted from section 8.3 of Tony's dissertation
 
@@ -22,11 +22,11 @@
   (Role (cell-factory)
         (Reacts (Message (CreateCellT ID Value))
                 ;; want to say that what it spawns is a Cell
-                (Spawns ★/t))))
+                (Spawn ★/t))))
 
 (define-type-alias Reader
   (Role (reader)
-        (Shares (Observe (CellT ID ★/t)))))
+        (Shares (Observe (Cell ID ★/t)))))
 
 (define-type-alias Writer
   (Role (writer)
@@ -68,4 +68,4 @@
       (on (asserted (cell id (bind value Value)))
           (printf "Cell ~a updated to: ~a\n" id value))
       (on (retracted (cell id discard))
-          (printf "Cell ~a deleted\n" id)))))
+          (printf "Cell ~a deleted\n" id)))))

racket/typed/examples/roles/chat-tcp2.rkt

@@ -1,6 +1,6 @@
-#lang typed/syndicate
+#lang typed/syndicate/roles
 
-(require typed/syndicate/drivers/tcp)
+(require "../../drivers/tcp.rkt")
 
 ;; message
 (define-constructor (speak who what)
@@ -26,7 +26,8 @@
 
   (spawn chat-ds
    (start-facet chat-server
-     (during/spawn (tcp-connection (bind id Symbol) (tcp-listener 5999))
+     ;; TODO - should be during/spawn
+     (during (tcp-connection (bind id Symbol) (tcp-listener 5999))
              (assert (tcp-accepted id))
              (let ([me (gensym 'user)])
                (assert (present me))

racket/typed/examples/roles/file-system.rkt

@@ -1,4 +1,4 @@
-#lang typed/syndicate
+#lang typed/syndicate/roles
 
 (define-constructor (file name content)
   #:type-constructor FileT
@@ -31,4 +31,4 @@
 (define-type-alias Writer
   (Role (writer)
         (Sends Save)
-        (Sends Delete)))
+        (Sends Delete)))

racket/typed/examples/roles/flink.rkt

@@ -1,4 +1,4 @@
-#lang typed/syndicate
+#lang typed/syndicate/roles
 
 ;; ---------------------------------------------------------------------------------------------------
 ;; Protocol
@@ -115,8 +115,7 @@ JobManager and the TaskManager, and one between the TaskManager and its
 TaskRunners.
 |#
 
-;; I think this is wrong by explicitly requiring that the facet stop in response
-(define-type-alias TaskAssigner-v1
+(define-type-alias TaskAssigner
   (Role (assign)
     (Shares (Observe (TaskPerformance ID ConcreteTask ★/t)))
     ;; would be nice to say how the TaskIDs relate to each other
@@ -124,14 +123,6 @@ TaskRunners.
             (Branch (Stop assign)
                     (Effs)))))
 
-(define-type-alias TaskAssigner
-  (Role (assign)
-    ;; would be nice to say how the TaskIDs relate to each other
-    (Reacts (Asserted (TaskPerformance ID ConcreteTask TaskStateDesc))
-            )))
-
-(export-type "task-assigner.rktd" TaskAssigner)
-
 (define-type-alias TaskPerformer
   (Role (listen)
     (During (Observe (TaskPerformance ID ConcreteTask ★/t))
@@ -204,9 +195,8 @@ The JobManager then performs the job and, when finished, asserts
 
 (define (spawn-task-runner [id : ID] [tm-id : ID])
   (spawn τc
-   (export-roles "task-runner-impl.rktd"
-   (lift+define-role task-runner-impl
-   (start-facet runner ;; #:includes-behavior TaskPerformer
+   (begin
+   (start-facet runner
     (assert (task-runner id))
     (on (retracted (task-manager tm-id _))
         (stop runner))
@@ -223,7 +213,7 @@ The JobManager then performs the job and, when finished, asserts
          (set! state (finished wc))]
         [(reduce-work $left $right)
          (define wc (hash-union/combine left right +))
-         (set! state (finished wc))])))))))
+         (set! state (finished wc))]))))))
 
 ;; ---------------------------------------------------------------------------------------------------
 ;; TaskManager
@@ -232,9 +222,8 @@ The JobManager then performs the job and, when finished, asserts
 (define (spawn-task-manager [num-task-runners : Int])
   (define id (gensym 'task-manager))
   (spawn τc
-   (export-roles "task-manager-impl.rktd"
-   (#;begin  lift+define-role task-manager-impl
-   (start-facet tm ;; #:includes-behavior TaskAssigner
+   (begin
+   (start-facet tm
     (log "Task Manager (TM) ~a is running" id)
     (during (job-manager-alive)
      (log "TM ~a learns about JM" id)
@@ -295,7 +284,7 @@ The JobManager then performs the job and, when finished, asserts
                [OVERLOAD/ts
                 (set! status OVERLOAD/ts)]
                [(finished discard)
-                (set! status st)]))))))))))
+                (set! status st)])))))))))
 
 ;; ---------------------------------------------------------------------------------------------------
 ;; JobManager
@@ -350,6 +339,26 @@ The JobManager then performs the job and, when finished, asserts
              (left t)]))))
 
 
+#;(define (partition-ready-tasks [tasks : (List Int)]
+                               -> (Tuple (List Int)
+                                         (List Int)))
+  (define part (inst partition/either Int Int Int))
+  (part tasks
+        (lambda ([t : Int])
+          (right 0)
+          #;(match (some 5)
+            [(some $ct)
+             (right ct)]
+            [none
+             (left 0)]))))
+
+#;(define (debug [tasks : (List Int)] -> (Tuple (List String) (List Int)))
+  (define part (inst partition/either Int String Int))
+  (tuple (list) (list))
+  (part tasks
+        (lambda ([t : Int])
+          (left "hi"))))
+
 (define (input->pending-task [t : InputTask] -> PendingTask)
   (match t
     [(task $id (map-work $s))
@@ -371,8 +380,8 @@ The JobManager then performs the job and, when finished, asserts
 
 (define (spawn-job-manager)
   (spawn τc
-    (lift+define-role job-manager-impl ;; export-roles "job-manager-impl.rktd"
-    (start-facet jm ;; #:includes-behavior TaskAssigner
+   (begin
+   (start-facet jm
     (assert (job-manager-alive))
     (log "Job Manager Up")
 
@@ -513,7 +522,7 @@ The JobManager then performs the job and, when finished, asserts
          (on (realize (tasks-finished job-id $data:TaskResult))
              (stop delegate-tasks
                    (start-facet done (assert (job-completion job-id tasks data)))))
-         (on (realize (task-is-ready job-id $t:ConcreteTask))
+         (on (realize (task-is-ready job-id $t))
              (perform-task t push-results)))
        (for ([t (in-list ready)])
          (add-ready-task! t))))))))
@@ -524,12 +533,10 @@ The JobManager then performs the job and, when finished, asserts
 ;; Job -> Void
 (define (spawn-client [j : JobDesc])
   (spawn τc
-   (export-roles "client-impl.rktd"
-   (lift+define-role client-impl
    (start-facet _
     (match-define (job $id $tasks) j)
     (on (asserted (job-completion id tasks $data))
-        (printf "job done!\n~a\n" data)))))))
+        (printf "job done!\n~a\n" data)))))
 
 ;; ---------------------------------------------------------------------------------------------------
 ;; Main
@@ -548,29 +555,3 @@ The JobManager then performs the job and, when finished, asserts
   (spawn-task-manager 3)
   (spawn-client (file->job "lorem.txt"))
   (spawn-client (string->job INPUT)))
-
-(module+ test
-  #;(verify-actors #;(Eventually (A (JobCompletion ID (List InputTask) TaskResult)))
-                 (Always (Implies (A (Observe (JobCompletion ID (List InputTask) ★/t)))
-                                  (Eventually (A (JobCompletion ID (List InputTask) TaskResult)))))
-                 job-manager-impl
-                 task-manager-impl
-                 client-impl)
-
-  (verify-actors (And (Always (Implies (A (Observe (TaskPerformance ID ConcreteTask ★/t)))
-                                       (Eventually (A (TaskPerformance ID ConcreteTask TaskStateDesc)))))
-                      (Eventually (A (TaskPerformance ID ConcreteTask TaskStateDesc))))
-                 TaskAssigner
-                 TaskPerformer))
-
-(module+ test
-  (check-simulates task-runner-impl task-runner-impl)
-  (check-has-simulating-subgraph task-runner-impl TaskPerformer)
-  (check-simulates task-manager-impl task-manager-impl)
-  (check-has-simulating-subgraph task-manager-impl TaskPerformer)
-  (check-has-simulating-subgraph task-manager-impl TaskAssigner)
-  (check-has-simulating-subgraph job-manager-impl TaskAssigner))
-
-;; infinite loop?
-#;(module+ test
-  (check-simulates job-manager-impl job-manager-impl))

racket/typed/examples/roles/internal-knowledge.rkt

@@ -1,4 +1,4 @@
-#lang typed/syndicate
+#lang typed/syndicate/roles
 
 ;; Expected Output:
 #|

racket/typed/examples/roles/ping-pong.rkt

@@ -0,0 +1,20 @@
+#lang typed/syndicate/roles
+
+;; Expected Output
+;; pong: 8339
+
+(define-type-alias ds-type
+  (U (Message (Tuple String Int))
+     (Observe (Tuple String ★/t))))
+
+(run-ground-dataspace ds-type
+  (spawn ds-type
+    (start-facet echo
+      (on (message (tuple "ping" (bind x Int)))
+          (send! (tuple "pong" x)))))
+  (spawn ds-type
+    (start-facet serve
+      (on start
+          (send! (tuple "ping" 8339)))
+      (on (message (tuple "pong" (bind x Int)))
+          (printf "pong: ~v\n" x)))))

racket/typed/examples/roles/provides.rkt

@@ -1,8 +1,8 @@
-#lang typed/syndicate
+#lang typed/syndicate/roles
 
 (provide a-fun)
 
 (define (a-fun [x : Int] -> Int)
   (+ x 1))
 
-#;(a-fun 5)
+#;(a-fun 5)

racket/typed/examples/roles/realize.rkt

@@ -1,4 +1,4 @@
-#lang typed/syndicate
+#lang typed/syndicate/roles
 
 ;; Expected Output:
 #|

racket/typed/examples/roles/require-struct/client.rkt

@@ -1,16 +1,13 @@
-#lang typed/syndicate
+#lang typed/syndicate/roles
 
 (require-struct msg #:as Msg
                 #:from "driver.rkt")
 
 (define m (msg 1 "hi"))
 
-(msg-in m)
-(msg-out m)
-
 (match m
   [(msg (bind x Int) discard)
    (displayln x)])
 
 ;; error: msg/checked: arity mismatch
-#;(msg 1 2 3)
+#;(msg 1 2 3)

racket/typed/examples/roles/require:typed/client.rkt

@@ -0,0 +1,5 @@
+#lang typed/syndicate/roles
+
+(require/typed "lib.rkt" [x : Int])
+
+(displayln (+ x 1))

racket/typed/examples/roles/requires.rkt

@@ -0,0 +1,5 @@
+#lang typed/syndicate/roles
+
+(require "provides.rkt")
+
+(a-fun 5)

racket/typed/examples/roles/simple-dataflow.rkt

@@ -1,4 +1,4 @@
-#lang typed/syndicate
+#lang typed/syndicate/roles
 
 ;; Expected Output
 ;; f: 0

racket/typed/examples/roles/simple-dataspace.rkt

@@ -1,4 +1,4 @@
-#lang typed/syndicate
+#lang typed/syndicate/roles
 
 (run-ground-dataspace Int
   (spawn Int

racket/typed/examples/roles/simple-during.rkt

@@ -1,4 +1,4 @@
-#lang typed/syndicate
+#lang typed/syndicate/roles
 
 ;; Expected Output
 ;; +GO

racket/typed/examples/roles/simple-query-hash.rkt

@@ -1,4 +1,4 @@
-#lang typed/syndicate
+#lang typed/syndicate/roles
 
 ;; Expected Output
 ;; adding key2 -> 88

racket/typed/examples/roles/simple-query-set.rkt

@@ -1,4 +1,4 @@
-#lang typed/syndicate
+#lang typed/syndicate/roles
 
 ;; Expected Output
 ;; size: 0

racket/typed/examples/roles/simple-query-value.rkt

@@ -1,4 +1,4 @@
-#lang typed/syndicate
+#lang typed/syndicate/roles
 
 ;; Expected Output
 ;; query: 0

racket/typed/examples/roles/simple-stop-facet.rkt

@@ -1,4 +1,4 @@
-#lang typed/syndicate
+#lang typed/syndicate/roles
 
 ;; Expected Output:
 ;; +42

racket/typed/examples/roles/two-buyer-protocol.rkt

@@ -0,0 +1,150 @@
+#lang typed/syndicate/roles
+
+;; Expected Output
+;; Completed Order:
+;; Catch 22
+;; 10001483
+;; March 9th
+
+(define-constructor (price v)
+  #:type-constructor PriceT
+  #:with Price (PriceT Int))
+
+(define-constructor (out-of-stock)
+  #:type-constructor OutOfStockT
+  #:with OutOfStock (OutOfStockT))
+
+(define-type-alias QuoteAnswer
+  (U Price OutOfStock))
+
+(define-constructor (quote title answer)
+  #:type-constructor QuoteT
+  #:with Quote (QuoteT String QuoteAnswer)
+  #:with QuoteRequest (Observe (QuoteT String ★/t))
+  #:with QuoteInterest (Observe (QuoteT ★/t ★/t)))
+
+(define-constructor (split-proposal title price contribution accepted)
+  #:type-constructor SplitProposalT
+  #:with SplitProposal (SplitProposalT String Int Int Bool)
+  #:with SplitRequest (Observe (SplitProposalT String Int Int ★/t))
+  #:with SplitInterest (Observe (SplitProposalT ★/t ★/t ★/t ★/t)))
+
+(define-constructor (order-id id)
+  #:type-constructor OrderIdT
+  #:with OrderId (OrderIdT Int))
+
+(define-constructor (delivery-date date)
+  #:type-constructor DeliveryDateT
+  #:with DeliveryDate (DeliveryDateT String))
+
+(define-type-alias (Maybe t)
+  (U t Bool))
+
+(define-constructor (order title price id delivery-date)
+  #:type-constructor OrderT
+  #:with Order (OrderT String Int (Maybe OrderId) (Maybe DeliveryDate))
+  #:with OrderRequest (Observe (OrderT String Int ★/t ★/t))
+  #:with OrderInterest (Observe (OrderT ★/t ★/t ★/t ★/t)))
+
+(define-type-alias ds-type
+  (U ;; quotes
+   Quote
+   QuoteRequest
+   (Observe QuoteInterest)
+   ;; splits
+   SplitProposal
+   SplitRequest
+   (Observe SplitInterest)
+   ;; orders
+   Order
+   OrderRequest
+   (Observe OrderInterest)))
+
+(define-type-alias seller-role
+  (Role (seller)
+    (Reacts (Asserted (Observe (QuoteT String ★/t)))
+            (Role (_)
+              (Shares (QuoteT String Int))))))
+
+(run-ground-dataspace ds-type
+
+;; seller
+(spawn ds-type
+  (start-facet _
+    (field [book (Tuple String Int) (tuple "Catch 22" 22)]
+           [next-order-id Int 10001483])
+    (on (asserted (observe (quote (bind title String) discard)))
+        (start-facet x
+          (on (retracted (observe (quote title discard)))
+              (stop x))
+          (define answer
+            (match title
+              ["Catch 22"
+               (price 22)]
+              [_
+               (out-of-stock)]))
+          (assert (quote title answer))))
+    (on (asserted (observe (order (bind title String) (bind offer Int) discard discard)))
+        (start-facet x
+          (on (retracted (observe (order title offer discard discard)))
+              (stop x))
+          (let ([asking-price 22])
+            (if (and (equal? title "Catch 22") (>= offer asking-price))
+                (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))))))))
+
+;; buyer A
+(spawn ds-type
+  (start-facet buyer
+    (field [title String "Catch 22"]
+           [budget Int 1000])
+    (on (asserted (quote (ref title) (bind answer QuoteAnswer)))
+        (match answer
+          [(out-of-stock)
+           (stop buyer)]
+          [(price (bind amount Int))
+           (start-facet negotiation
+             (field [contribution Int (/ amount 2)])
+             (on (asserted (split-proposal (ref title) amount (ref contribution) (bind accept? Bool)))
+                 (if accept?
+                     (stop buyer)
+                     (if (> (ref contribution) (- amount 5))
+                         (stop negotiation (displayln "negotiation failed"))
+                         (set! contribution
+                               (+ (ref contribution) (/ (- amount (ref contribution)) 2)))))))]))))
+
+;; buyer B
+(spawn ds-type
+  (start-facet buyer-b
+    (field [funds Int 5])
+    (on (asserted (observe (split-proposal (bind title String) (bind price Int) (bind their-contribution Int) discard)))
+        (let ([my-contribution (- price their-contribution)])
+          (cond
+            [(> my-contribution (ref funds))
+             (start-facet decline
+               (assert (split-proposal title price their-contribution #f))
+               (on (retracted (observe (split-proposal title price their-contribution discard)))
+                   (stop decline)))]
+            [#t
+             (start-facet accept
+               (assert (split-proposal title price their-contribution #t))
+               (on (retracted (observe (split-proposal title price their-contribution discard)))
+                   (stop accept))
+               (on start
+                   (spawn ds-type
+                     (start-facet purchase
+                       (on (asserted (order title price (bind order-id? (Maybe OrderId)) (bind delivery-date? (Maybe DeliveryDate))))
+                           (match (tuple order-id? delivery-date?)
+                             [(tuple (order-id (bind id Int)) (delivery-date (bind date String)))
+                              ;; complete!
+                              (begin (displayln "Completed Order:")
+                                     (displayln title)
+                                     (displayln id)
+                                     (displayln date)
+                                     (stop purchase))]
+                             [discard
+                              (begin (displayln "Order Rejected")
+                                     (stop purchase))]))))))])))))
+)

racket/typed/examples/simple-during-spawn.rkt

@@ -1,33 +0,0 @@
-#lang typed/syndicate
-
-;; Expected Output
-;; +parent
-;; +GO
-;; +ready
-;; -parent
-;; -GO
-;; -ready
-
-(define-type-alias ds-type
-  (U (Tuple String) (Observe (Tuple ★/t))))
-
-(run-ground-dataspace ds-type
-                      (spawn ds-type
-                             (start-facet parent
-                                          (assert (tuple "parent"))
-                                          (during/spawn (tuple "GO")
-                                                        (assert (tuple "ready")))
-                                          (on (asserted (tuple "ready"))
-                                              (stop parent))))
-                      (spawn ds-type
-                             (start-facet flag
-                                          (assert (tuple "GO"))
-                                          (on (retracted (tuple "parent"))
-                                              (stop flag))))
-                      (spawn ds-type
-                             (start-facet obs
-                                          (during (tuple (bind s String))
-                                                  (on start
-                                                      (printf "+~a\n" s))
-                                                  (on stop
-                                                      (printf "-~a\n" s))))))

racket/typed/examples/struct-out/client.rkt

@@ -1,7 +0,0 @@
-#lang typed/syndicate/roles
-
-(require "typed-out.rkt")
-
-(define c : (Cow Int) (cow 5))
-
-(cow-moos c)

racket/typed/examples/struct-out/struct-in.rkt

@@ -1,7 +0,0 @@
-#lang typed/syndicate/roles
-
-(require "struct-out.rkt")
-
-(happy-days (happy 5))
-
-(define classic : (Happy Int) (happy 100))

racket/typed/examples/struct-out/struct-out.rkt

@@ -1,5 +0,0 @@
-#lang typed/syndicate/roles
-
-(provide (struct-out happy))
-
-(define-constructor* (happy : Happy days))

racket/typed/examples/struct-out/typed-out.rkt

@@ -1,5 +0,0 @@
-#lang typed/syndicate/roles
-
-(require-struct cow #:as Cow #:from "untyped.rkt")
-
-(provide (struct-out cow))

racket/typed/examples/struct-out/untyped.rkt

@@ -1,5 +0,0 @@
-#lang racket
-
-(provide (struct-out cow))
-
-(struct cow (moos) #:transparent)

racket/typed/examples/two-buyer-protocol.rkt

@@ -20,14 +20,14 @@
 (define-constructor (quote title answer)
   #:type-constructor QuoteT
   #:with Quote (QuoteT String QuoteAnswer)
-  #:with QuoteRequest (Observe (QuoteT String ★/t))
-  #:with QuoteInterest (Observe (QuoteT ★/t ★/t)))
+  #:with QuoteRequest (Observe (QuoteT String ★))
+  #:with QuoteInterest (Observe (QuoteT ★ ★)))
 
 (define-constructor (split-proposal title price contribution accepted)
   #:type-constructor SplitProposalT
   #:with SplitProposal (SplitProposalT String Int Int Bool)
-  #:with SplitRequest (Observe (SplitProposalT String Int Int ★/t))
-  #:with SplitInterest (Observe (SplitProposalT ★/t ★/t ★/t ★/t)))
+  #:with SplitRequest (Observe (SplitProposalT String Int Int ★))
+  #:with SplitInterest (Observe (SplitProposalT ★ ★ ★ ★)))
 
 (define-constructor (order-id id)
   #:type-constructor OrderIdT
@@ -40,11 +40,11 @@
 (define-type-alias (Maybe t)
   (U t Bool))
 
-(define-constructor (order title price oid delivery-date)
+(define-constructor (order title price id delivery-date)
   #:type-constructor OrderT
   #:with Order (OrderT String Int (Maybe OrderId) (Maybe DeliveryDate))
-  #:with OrderRequest (Observe (OrderT String Int ★/t ★/t))
-  #:with OrderInterest (Observe (OrderT ★/t ★/t ★/t ★/t)))
+  #:with OrderRequest (Observe (OrderT String Int ★ ★))
+  #:with OrderInterest (Observe (OrderT ★ ★ ★ ★)))
 
 (define-type-alias ds-type
   (U ;; quotes
@@ -60,104 +60,88 @@
    OrderRequest
    (Observe OrderInterest)))
 
-(define-type-alias seller-role
-  (Role (seller)
-    (During (Observe (QuoteT String ★/t))
-      (Shares (QuoteT String QuoteAnswer)))
-    #;(Reacts (Asserted (Observe (QuoteT String ★/t)))
-            (Role (_)
-              ;; QuoteAnswer was originally, erroneously, Int
-              (Shares (QuoteT String QuoteAnswer))))))
-
-(run-ground-dataspace ds-type
+(dataspace ds-type
 
 ;; seller
 (spawn ds-type
-  (lift+define-role seller-impl
-  (start-facet _ ;; #:implements seller-role
-    (field [book (Tuple String Int) (tuple "Catch 22" 22)]
-           [next-order-id Int 10001483])
-    (on (asserted (observe (quote (bind title String) discard)))
-        (start-facet x
-          (on (retracted (observe (quote title discard)))
-              (stop x))
-          (define answer
-            (match title
-              ["Catch 22"
-               (price 22)]
-              [_
-               (out-of-stock)]))
-          (assert (quote title answer))))
-    (on (asserted (observe (order (bind title String) (bind offer Int) discard discard)))
-        (start-facet x
-          (on (retracted (observe (order title offer discard discard)))
-              (stop x))
-          (let ([asking-price 22])
-            (if (and (equal? title "Catch 22") (>= offer asking-price))
-                (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)))))))))
+       (facet _
+              (fields [book (Tuple String Int) (tuple "Catch 22" 22)]
+                      [next-order-id Int 10001483])
+              (on (asserted (observe (quote (bind title String) discard)))
+                  (facet x
+                         (fields)
+                         (on (retracted (observe (quote title discard)))
+                             (stop x (begin)))
+                         (match title
+                           ["Catch 22"
+                            (assert (quote title (price 22)))]
+                           [discard
+                            (assert (quote title (out-of-stock)))])))
+              (on (asserted (observe (order (bind title String) (bind offer Int) discard discard)))
+                  (facet x
+                         (fields)
+                         (on (retracted (observe (order title offer discard discard)))
+                             (stop x (begin)))
+                         (let [asking-price 22]
+                           (if (and (equal? title "Catch 22") (>= offer asking-price))
+                               (let [id (ref next-order-id)]
+                                 (begin (set! next-order-id (+ 1 id))
+                                        (assert (order title offer (order-id id) (delivery-date "March 9th")))))
+                               (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])
-    (on (asserted (quote (ref title) (bind answer QuoteAnswer)))
-        (match answer
-          [(out-of-stock)
-           (stop buyer)]
-          [(price (bind amount Int))
-           (start-facet negotiation
-             (field [contribution Int (/ amount 2)])
-             (on (asserted (split-proposal (ref title) amount (ref contribution) (bind accept? Bool)))
-                 (if accept?
-                     (stop buyer)
-                     (if (> (ref contribution) (- amount 5))
-                         (stop negotiation (displayln "negotiation failed"))
-                         (set! contribution
-                               (+ (ref contribution) (/ (- amount (ref contribution)) 2)))))))])))))
+       (facet buyer
+              (fields [title String "Catch 22"]
+                      [budget Int 1000])
+              (on (asserted (quote (ref title) (bind answer QuoteAnswer)))
+                  (match answer
+                    [(out-of-stock)
+                     (stop buyer (begin))]
+                    [(price (bind amount Int))
+                     (facet negotiation
+                            (fields [contribution Int (/ amount 2)])
+                            (on (asserted (split-proposal (ref title) amount (ref contribution) (bind accept? Bool)))
+                                (if accept?
+                                    (stop buyer (begin))
+                                    (if (> (ref contribution) (- amount 5))
+                                        (stop negotiation (displayln "negotiation failed"))
+                                        (set! contribution
+                                              (+ (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)))
-        (let ([my-contribution (- price their-contribution)])
-          (cond
-            [(> my-contribution (ref funds))
-             (start-facet decline
-               (assert (split-proposal title price their-contribution #f))
-               (on (retracted (observe (split-proposal title price their-contribution discard)))
-                   (stop decline)))]
-            [#t
-             (start-facet accept
-               (assert (split-proposal title price their-contribution #t))
-               (on (retracted (observe (split-proposal title price their-contribution discard)))
-                   (stop accept))
-               (on start
-                   (spawn ds-type
-                     (start-facet purchase
-                       (on (asserted (order title price (bind order-id? (Maybe OrderId)) (bind delivery-date? (Maybe DeliveryDate))))
-                           (match (tuple order-id? delivery-date?)
-                             [(tuple (order-id (bind id Int)) (delivery-date (bind date String)))
-                              ;; complete!
-                              (begin (displayln "Completed Order:")
-                                     (displayln title)
-                                     (displayln id)
-                                     (displayln date)
-                                     (stop purchase))]
-                             [discard
-                              (begin (displayln "Order Rejected")
-                                     (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))
+       (facet buyer-b
+              (fields [funds Int 5])
+              (on (asserted (observe (split-proposal (bind title String) (bind price Int) (bind their-contribution Int) discard)))
+                  (let [my-contribution (- price their-contribution)]
+                    (cond
+                      [(> my-contribution (ref funds))
+                       (facet decline
+                              (fields)
+                              (assert (split-proposal title price their-contribution #f))
+                              (on (retracted (observe (split-proposal title price their-contribution discard)))
+                                  (stop decline (begin))))]
+                      [#t
+                       (facet accept
+                              (fields)
+                              (assert (split-proposal title price their-contribution #t))
+                              (on (retracted (observe (split-proposal title price their-contribution discard)))
+                                  (stop accept (begin)))
+                              (on start
+                                  (spawn ds-type
+                                         (facet purchase
+                                                (fields)
+                                                (on (asserted (order title price (bind order-id? (Maybe OrderId)) (bind delivery-date? (Maybe DeliveryDate))))
+                                                    (match (tuple order-id? delivery-date?)
+                                                      [(tuple (order-id (bind id Int)) (delivery-date (bind date String)))
+                                                       ;; complete!
+                                                       (begin (displayln "Completed Order:")
+                                                              (displayln title)
+                                                              (displayln id)
+                                                              (displayln date)
+                                                              (stop purchase (begin)))]
+                                                      [discard
+                                                       (begin (displayln "Order Rejected")
+                                                           (stop purchase (begin)))]))))))])))))
+)

racket/typed/for-loops.rkt

@@ -13,7 +13,7 @@
 (require (only-in "set.rkt" Set ~Set))
 (require (only-in "hash.rkt" Hash ~Hash))
 (require (only-in "prim.rkt" Bool + #%datum))
-(require (only-in "core-expressions.rkt" let unit tuple-select mk-tuple))
+(require (only-in "core-expressions.rkt" let unit))
 (require "maybe.rkt")
 
 (require (postfix-in - (only-in racket/set
@@ -125,68 +125,36 @@
              #,body))]))
 
 (define-typed-syntax for/fold
-  [(for/fold ([acc:id (~optional (~datum :)) τ-acc init] ...+)
+  [(for/fold ([acc:id (~optional (~datum :)) τ-acc init])
              (clause:iter-clause
               ...)
      e-body ...+) ≫
-  [⊢ init ≫ init- (⇐ : τ-acc)] ...
-  #:fail-unless (all-pure? #'(init- ...)) "expression must be pure"
+  [⊢ init ≫ init- (⇐ : τ-acc)]
+  #:fail-unless (pure? #'init-) "expression must be pure"
   #:with (clauses- ([x x- τ] ...)) (analyze-for-clauses #'(clause.parend ...))
-  #:do [(define num-accs (length (syntax->list #'(τ-acc ...))))]
-  #:with body-ty (if (= 1 num-accs)
-                     (first (syntax->list #'(τ-acc ...)))
-                     (type-eval #'(Tuple (~@ τ-acc ...))))
-  [[[x ≫ x-- : τ] ...]
-   [[acc ≫ acc- : τ-acc] ...] ⊢ (block e-body ...) ≫ e-body-
-                               (⇐ : body-ty)
-                               (⇒ ν-ep (~effs τ-ep ...))
-                               (⇒ ν-s (~effs τ-s ...))
-                               (⇒ ν-f (~effs τ-f ...))]
+  [[x ≫ x-- : τ] ...
+   [acc ≫ acc- : τ-acc] ⊢ (block e-body ...) ≫ e-body-
+                           (⇐ : τ-acc)
+                           (⇒ ν-ep (~effs τ-ep ...))
+                           (⇒ ν-s (~effs τ-s ...))
+                           (⇒ ν-f (~effs τ-f ...))]
   -------------------------------------------------------
-  [⊢ (values->tuple #,num-accs
-       (for/fold- ([acc- init-] ...)
-         clauses-
-         #,(bind-renames #'([x-- x-] ...) #`(tuple->values #,num-accs e-body-))))
-     (⇒ : body-ty)
+  [⊢ (for/fold- ([acc- init-])
+                clauses-
+                #,(bind-renames #'([x-- x-] ...) #'e-body-))
+     (⇒ : τ-acc)
      (⇒ ν-ep (τ-ep ...))
      (⇒ ν-s (τ-s ...))
      (⇒ ν-f (τ-f ...))]]
-  [(for/fold (accs ... [acc:id init] more-accs ...)
+  [(for/fold ([acc:id init])
              clauses
      e-body ...+) ≫
    [⊢ init ≫ _ (⇒ : τ-acc)]
    ---------------------------------------------------
-   [≻ (for/fold (accs ... [acc τ-acc init] more-accs ...)
+   [≻ (for/fold ([acc τ-acc init])
                 clauses
         e-body ...)]])
 
-(define-syntax-parser tuple->values
-  [(_ n:nat e:expr)
-   (define arity (syntax-e #'n))
-   (cond
-     [(= 1 arity)
-      #'e]
-     [else
-      (define/with-syntax tmp (generate-temporary 'tup))
-      (define projections
-        (for/list ([i (in-range arity)])
-          #`(#%app- tuple-select #,i tmp)))
-      #`(let- ([tmp e])
-          (#%app- values- #,@projections))])])
-
-#;(tuple->values 1 (tuple 0))
-
-(define-syntax-parser values->tuple
-  [(_ n:nat e:expr)
-   (define arity (syntax-e #'n))
-   (cond
-     [(= 1 arity)
-      #'e]
-     [else
-      (define/with-syntax (tmp ...) (generate-temporaries (make-list arity 'values->tuple)))
-      #`(let-values- ([(tmp ...) e])
-          (#%app- mk-tuple (#%app- list- tmp ...)))])])
-
 (define-typed-syntax (for/list (clause:iter-clause ...)
                        e-body ...+) ≫
   #:with (clauses- ([x x- τ] ...)) (analyze-for-clauses #'(clause.parend ...))

racket/typed/hash.rkt

@@ -33,20 +33,32 @@
 
 (define-container-type Hash #:arity = 2)
 
-(define-typed-syntax (hash (~seq key:expr val:expr) ...) ≫
+(begin-for-syntax
+  (define-splicing-syntax-class key-val-list
+    #:attributes (items)
+    (pattern (~seq k1 v1 rest:key-val-list)
+             #:attr items #`((k1 v1) #,@#'rest.items))
+    (pattern (~seq)
+             #:attr items #'())))
+
+(define-typed-syntax (hash keys&vals:key-val-list) ≫
+  #:with ((key val) ...) #'keys&vals.items
   [⊢ key ≫ key- (⇒ : τ-k)] ...
   [⊢ val ≫ val- (⇒ : τ-val)] ...
   #:fail-unless (all-pure? #'(key- ... val- ...)) "gotta be pure"
+  #:with together-again (stx-flatten #'((key- val-) ...))
   --------------------------------------------------
-  [⊢ (#%app- hash- (~@ key val) ...) (⇒ : (Hash (U τ-k ...) (U τ-val ...)))])
+  [⊢ (#%app- hash- #,@#'together-again) (⇒ : (Hash (U τ-k ...) (U τ-val ...)))])
 
 (require/typed racket/base
   ;; don't have a type for ConsPair
   #;[make-hash : (∀ (K V) (→fn (List (ConsPair K V)) (Hash K V)))]
   [hash-set : (∀ (K V) (→fn (Hash K V) K V (Hash K V)))]
   [hash-ref : (∀ (K V) (→fn (Hash K V) K V))]
+  ;; TODO hash-ref/failure
   [hash-has-key? : (∀ (K V) (→fn (Hash K V) K Bool))]
   [hash-update : (∀ (K V) (→fn (Hash K V) K (→fn V V) (Hash K V)))]
+  ;; TODO hash-update/failure
   [hash-remove : (∀ (K V) (→fn (Hash K V) K (Hash K V)))]
   [hash-map : (∀ (K V R) (→fn (Hash K V) (→fn K V R) (List R)))]
   [hash-keys : (∀ (K V) (→fn (Hash K V) (List K)))]
@@ -59,6 +71,7 @@
 
 (require/typed racket/hash
   [hash-union : (∀ (K1 V1 K2 V2) (→fn (Hash K1 V1) (Hash K2 V2) (Hash (U K1 K2) (U V1 V2))))]
+  ;; TODO - hash-union with #:combine
   )
 
 (define- (hash-ref/failure- h k err)

racket/typed/info.rkt

@@ -1,12 +1,8 @@
 #lang info
 
-(define scribblings '(("scribblings/typed-syndicate.scrbl" ())))
-
 (define compile-omit-paths
   '("examples"
     "tests"))
 
 (define test-omit-paths
-  ;; a number of the examples use SPIN for model checking which I need
-  ;; to figure out how to get working on the package server
-  '("examples/"))
+  '("examples/roles/chat-tcp2.rkt"))

racket/typed/list.rkt

@@ -3,24 +3,18 @@
 (provide List
          (for-syntax ~List)
          list
-         (typed-out [[empty- : (List ⊥)] empty]
-                    [[empty?- : (∀ (X) (→fn (List X) Bool))] empty?]
-                    [[cons- : (∀ (X) (→fn X (List X) (List X)))] cons]
-                    [[cons?- : (∀ (X) (→fn X (List X) Bool))] cons?]
+         (typed-out [[cons- : (∀ (X) (→fn X (List X) (List X)))] cons]
                     [[first- : (∀ (X) (→fn (List X) X))] first]
                     [[second- : (∀ (X) (→fn (List X) X))] second]
                     [[rest- : (∀ (X) (→fn (List X) (List X)))] rest]
                     [[member?- (∀ (X) (→fn X (List X) Bool))] member?]
+                    [[empty?- (∀ (X) (→fn (List X) Bool))] empty?]
                     [[reverse- (∀ (X) (→fn (List X) (List X)))] reverse]
                     [[partition- (∀ (X) (→fn (List X) (→fn X Bool) (List X)))] partition]
-                    [[map- (∀ (X Y) (→fn (→fn X Y) (List X) (List Y)))] map]
-                    [[argmax- : (∀ (X) (→fn (→fn X Int) (List X) X))] argmax]
-                    [[argmin- : (∀ (X) (→fn (→fn X Int) (List X) X))] argmin]
-                    [[remove- : (∀ (X) (→fn X (List X) (List X)))] remove]
-                    [[length- : (∀ (X) (→fn (List X) Int))] length]))
+                    [[map- (∀ (X Y) (→fn (→fn X Y) (List X) (List Y)))] map]))
 
 (require "core-types.rkt")
-(require (only-in "prim.rkt" Bool Int))
+(require (only-in "prim.rkt" Bool))
 (require (postfix-in - racket/list))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

racket/typed/ltl.rkt

@@ -15,15 +15,15 @@
 ;;  - Bool
 ;; where X represents the type of atomic propositions
 
-(struct always [p] #:prefab)
-(struct eventually [p] #:prefab)
-(struct atomic [p] #:prefab)
-(struct weak-until [p q] #:prefab)
-(struct strong-until [p q] #:prefab)
-(struct ltl-implies [p q] #:prefab)
-(struct ltl-and [p q] #:prefab)
-(struct ltl-or [p q] #:prefab)
-(struct ltl-not [p] #:prefab)
+(struct always [p] #:transparent)
+(struct eventually [p] #:transparent)
+(struct atomic [p] #:transparent)
+(struct weak-until [p q] #:transparent)
+(struct strong-until [p q] #:transparent)
+(struct ltl-implies [p q] #:transparent)
+(struct ltl-and [p q] #:transparent)
+(struct ltl-or [p q] #:transparent)
+(struct ltl-not [p] #:transparent)
 
 ;; [LTL X] {X -> Y} -> [LTL Y]
 (define (map-atomic ltl op)

racket/typed/prim.rkt

@@ -32,8 +32,6 @@
 (define-primop zero? (→fn Int Bool))
 (define-primop positive? (→fn Int Bool))
 (define-primop negative? (→fn Int Bool))
-(define-primop current-inexact-milliseconds (→fn Int))
-(define-primop string=? (→fn String String Bool))
 
 (define-primop bytes->string/utf-8 (→ ByteString (Computation (Value String) (Endpoints) (Roles) (Spawns))))
 (define-primop string->bytes/utf-8 (→ String (Computation (Value ByteString) (Endpoints) (Roles) (Spawns))))

racket/typed/proto.rkt

@@ -20,26 +20,26 @@
 ;;   - (Sends τ)
 ;;   - (Realizes τ)
 ;;   - (Stop FacetName Body)
-(struct Role (nm eps) #:prefab)
-(struct Spawn (ty) #:prefab)
-(struct Sends (ty) #:prefab)
-(struct Realizes (ty) #:prefab)
-(struct Stop (nm body) #:prefab)
+(struct Role (nm eps) #:transparent)
+(struct Spawn (ty) #:transparent)
+(struct Sends (ty) #:transparent)
+(struct Realizes (ty) #:transparent)
+(struct Stop (nm body) #:transparent)
 
 ;; 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) #:prefab)
-(struct Shares (ty) #:prefab)
-(struct Know (ty) #:prefab)
+(struct Reacts (evt body) #:transparent)
+(struct Shares (ty) #:transparent)
+(struct Know (ty) #:transparent)
 
 ;; a Body describes actions carried out in response to some event, and
 ;; is one of
 ;;   - T
 ;;   - (Listof Body)
 ;;   - (Branch (Listof Body))
-(struct Branch (arms) #:prefab)
+(struct Branch (arms) #:transparent)
 
 ;; 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) #:prefab)
-(struct Retracted (ty) #:prefab)
-(struct Message (ty) #:prefab)
-(struct Forget (ty) #:prefab)
-(struct Realize (ty) #:prefab)
+(struct Asserted (ty) #:transparent)
+(struct Retracted (ty) #:transparent)
+(struct Message (ty) #:transparent)
+(struct Forget (ty) #:transparent)
+(struct Realize (ty) #:transparent)
 (define StartEvt 'Start)
 (define StopEvt 'Stop)
 (define DataflowEvt 'Dataflow)
@@ -68,8 +68,8 @@
 ;; specified facet,
 ;;   - (StartOf FacetName)
 ;;   - (StopOf FacetName)
-(struct StartOf (fn) #:prefab)
-(struct StopOf (fn) #:prefab)
+(struct StartOf (fn) #:transparent)
+(struct StopOf (fn) #:transparent)
 
 ;; 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) #: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)
+(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)
 ;; TODO this might be a problem when used as a match pattern
 (define ⋆ (Mk⋆))
-(struct Base (name) #:prefab)
+(struct Base (name) #:transparent)
 (define Int (Base 'Int))
 (define String (Base 'String))
 (define Bool (Base 'Bool))
@@ -237,25 +237,24 @@
     (match-define (role-graph st0 st#) rg)
     (check-true (hash-has-key? st# (set 'x 'y)))))
 
-;; a DetectedCylce is a (detected-cycle StateName (Listof TraversalStep)), as in
-;;   (detected-cycle start steps)
-;; where path represents the sequences of states containing a cycle,
-(struct detected-cycle (start steps) #:transparent)
-
-;; a TraversalStep is a (traversal-step D StateName)
-;; representing a state transition along an edge matching D to a destination state
-(struct traversal-step (evt dest) #:transparent)
+;; a DetectedCylce is a (List (Listof StateName) D D D), as in
+;;   (list path init evt D)
+;; where
+;;   - path represents the sequences of states containing a cycle,
+;;   - init is the external event that initiated this activity
+;;   - evt is the last-taken internal event
+;;   - D is the edge in the graph that matched evt
 
 ;; RoleGraph Role -> (U RoleGraph DetectedCycle)
 ;; "Optimize" the given role graph with respect to internal events.
 ;; The resulting graph will have transitions of only external events.
-(define (compile/internal-events rg)
+(define (compile/internal-events rg role)
   (match-define (role-graph st0 orig-st#) rg)
   ;; doing funny business with state (set) here
   (define orig-st#+ (hash-set orig-st# (set) (state (set) (hash) (set))))
 
   ;; a WorkItem is a
-  ;;   (work-item TraversalStep (Listof TraversalStep) D+ (Listof D+) (Listof TransitionEffect))
+  ;;   (work-item StateName (Listof StateName) D+ (Listof D+) (Listof TransitionEffect))
   ;; such as (work-item from path/r to by with effs), where
   ;;   - from is the origin state for this chain of events
   ;;   - path/r is the list of states in the path to this point, *after* from, in reverse
@@ -265,7 +264,6 @@
   ;;   - with is a list of pending events to be processed
   ;;   - effs are the external effects emitted on this path
   (struct work-item (from path/r to by with effs) #:transparent)
-
   (let/ec fail
     (define (walk work visited st#)
       (match work
@@ -292,21 +290,20 @@
            (set! states (hash-set states (set) (state (set) (hash) (set)))))
          (role-graph new-st0 states)]
         [(cons (work-item from path/r to by with effs) more-work)
-         (match-define (traversal-step last-evt cur-st) to)
-         (define prev (if (empty? path/r) from (traversal-step-dest (first path/r))))
+         (define prev (if (empty? path/r) from (first path/r)))
          (define prev-assertions (state-assertions (hash-ref orig-st#+ prev)))
-         (match-define (state _ txn# cur-assertions) (hash-ref orig-st#+ cur-st))
+         (match-define (state _ txn# cur-assertions) (hash-ref orig-st#+ to))
          (define new-state-changes (route-internal prev-assertions
                                                    cur-assertions))
          (define state-changes* (for/list ([D (in-set new-state-changes)]
                                            #:when (for/or ([D/actual (in-hash-keys txn#)])
                                                     (D<:? D D/actual)))
                                   D))
-         (define started (for*/list ([fn (in-set (set-subtract cur-st prev))]
+         (define started (for*/list ([fn (in-set (set-subtract to prev))]
                                      [D (in-value (StartOf fn))]
                                      #:when (hash-has-key? txn# D))
                            D))
-         (define stopped (for*/list ([fn (in-set (set-subtract prev cur-st))]
+         (define stopped (for*/list ([fn (in-set (set-subtract prev to))]
                                      [D (in-value (StopOf fn))]
                                      #:when (hash-has-key? txn# D))
                            D))
@@ -335,12 +332,18 @@
                           #:when (implies (DataflowEvt? D) (DataflowEvt? evt))
                           [t (in-set ts)])
                 (match-define (transition more-effs dest) t)
-                (check-for-cycle! from path/r+ evt dest fail)
+                (when (and (member dest path/r+)
+                           ;; TODO - cycles involving Start/Stop are tricky. Punt for now
+                           (not (start/stop-evt? evt)))
+                  (fail (list (cons from (reverse (cons dest path/r+)))
+                              by
+                              evt
+                              D)))
                 (define-values (internal-effs external-effs)
                   (partition-transition-effects more-effs))
                 (work-item from
                            path/r+
-                           (traversal-step evt dest)
+                           dest
                            by
                            (append more-pending internal-effs)
                            (append effs external-effs)))]))
@@ -358,9 +361,9 @@
          (cond
            [(ormap empty? induced-work)
             ;; this is the end of some path
-            (define visited+ (set-add visited cur-st))
+            (define visited+ (set-add visited to))
             (define new-paths-work
-              (for*/list (#:unless (set-member? visited cur-st)
+              (for*/list (#:unless (set-member? visited to)
                           [(D txns) (in-hash txn#)]
                           #:when (external-evt? D)
                           #:unless (equal? D DataflowEvt)
@@ -368,43 +371,21 @@
                 (match-define (transition es dst) t)
                 (define-values (internal-effs external-effs)
                   (partition-transition-effects es))
-                (work-item cur-st '() (traversal-step D dst) D internal-effs external-effs)))
-            (define new-st# (update-path st# from cur-st by effs))
+                (work-item to '() dst D internal-effs external-effs)))
+            (define new-st# (update-path st# from to by effs))
             (walk (append more-work induced-work* new-paths-work) visited+ new-st#)]
            [else
             (walk (append more-work induced-work*) visited st#)])]))
-    (walk (list (work-item (set) '() (traversal-step StartEvt st0) StartEvt '() '()))
+    (walk (list (work-item (set) '() st0 StartEvt '() '()))
           (set)
           (hash))))
 
-;; (Listof TraceStep) D StateName (DetectedCycle -> X) -> (U X Void)
-;; the path is in reverse, and the final step is the pair evt/dest;
-;; so their is a cycle if the sequence from the first occurrence of
-;; dest in the path matches the sequence from the second occurrence to
-;; the first.
-(define (check-for-cycle! from path/r evt dest fail)
-  ;; TraceStep -> Bool
-  (define (same-state? step) (equal? dest (traversal-step-dest step)))
-
-  ;; (Listof TraceStep) -> (Values (Listof TraceStep) (Listof TraceStep))
-  (define (split-at-same-state steps) (splitf-at steps (compose not same-state?)))
-
-  (define-values (loop1 trail) (split-at-same-state path/r))
-  (when (cons? trail)
-    (match-define (cons prior-last trail2) trail)
-    (define-values (loop2 trail3) (split-at-same-state trail2))
-    (define last-step (traversal-step evt dest))
-    (when (and (cons? trail3)
-               (equal? (cons last-step loop1)
-                       (cons prior-last loop2)))
-      (fail (detected-cycle from (reverse (cons last-step path/r)))))))
-
 (module+ test
   (test-case
       "most minimal functionality for removing internal events"
     ;; manager role has basically nothing to it
     (define m (compile manager))
-    (define i (compile/internal-events m))
+    (define i (compile/internal-events m manager))
     (check-true (role-graph? i))
     (check-true (simulates?/rg i m))
     (check-true (simulates?/rg m i))
@@ -415,7 +396,7 @@
     ;; because it doesn't use any internal events, it should be unaffected
     (define tmr (parse-T task-runner-ty))
     (define tm (compile tmr))
-    (define tmi (compile/internal-events tm))
+    (define tmi (compile/internal-events tm tmr))
     (check-true (role-graph? tmi))
     ;; I'm not exactly sure how the two should be related via simulation :S
     (check-true (simulates?/rg tmi tm)))
@@ -429,15 +410,15 @@
                      (Realizes Int))))
     (define r (parse-T cyclic))
     (define rg (compile r))
-    (define i (run/timeout (thunk (compile/internal-events rg))))
-    (check-true (detected-cycle? i))
-    (check-match i
-                 (detected-cycle
-                  (== (set))
-                  (list (traversal-step 'Start (== (set 'x)))
-                        (traversal-step (StartOf 'x) (== (set 'x)))
-                        (traversal-step (Realize (internal-label _ (== Int))) (== (set 'x)))
-                        (traversal-step (Realize (internal-label _ (== Int))) (== (set 'x)))))))
+    (define i (run/timeout (thunk (compile/internal-events rg r))))
+    (check-true (list? i))
+    (check-equal? (length i) 4)
+    (match-define (list path kick-off evt edge) i)
+    ;; the first 'x -> 'x cycle is ignored because it's a Start event
+    (check-equal? path (list (set) (set 'x) (set 'x) (set 'x)))
+    (check-equal? kick-off StartEvt)
+    (check-match evt (Realize (internal-label _ (== Int))))
+    (check-match edge (Realize (internal-label _ (== Int)))))
   (test-case
       "interesting internal start event"
     (test-case
@@ -452,7 +433,7 @@
       (define r (parse-T strt))
       (define rg (run/timeout (thunk (compile r))))
       (check-true (role-graph? rg))
-      (define rgi (run/timeout (thunk (compile/internal-events rg))))
+      (define rgi (run/timeout (thunk (compile/internal-events rg r))))
       (check-true (role-graph? rgi))
       (match-define (role-graph st0 st#) rgi)
       (check-equal? st0 (set 'x 'y))
@@ -473,7 +454,7 @@
                                 (Role 'y (list)))))))
     (define rg (run/timeout (thunk (compile role))))
     (check-true (role-graph? rg))
-    (define rgi (run/timeout (thunk (compile/internal-events rg))))
+    (define rgi (run/timeout (thunk (compile/internal-events rg role))))
     (check-true (role-graph? rgi))
     (define state# (role-graph-states rgi))
     (check-true (hash-has-key? state# (set 'x)))
@@ -490,7 +471,7 @@
     (define role (run/timeout (thunk (parse-T desc))))
     (define rg (run/timeout (thunk (compile role))))
     (check-true (role-graph? rg))
-    (define rgi (run/timeout (thunk (compile/internal-events rg))))
+    (define rgi (run/timeout (thunk (compile/internal-events rg role))))
     (check-true (role-graph? rgi))
     (check-match rgi
                  (role-graph (== (set 'x 'y))
@@ -665,9 +646,9 @@
     (check-equal? sn0 (set 'seller))
     (check-true (hash-has-key? seller# (set 'seller)))
     (check-true (hash-has-key? seller# (set 'seller 'fulfill)))
-    (check-equal? (list->set (hash-keys seller#))
-                  (set (set 'seller 'fulfill)
-                       (set 'seller)))
+    (check-equal? (hash-keys seller#)
+                  (list (set 'seller 'fulfill)
+                        (set 'seller)))
     (define st0 (hash-ref seller# (set 'seller)))
     (define transitions (state-transitions st0))
     (define quote-request
@@ -821,12 +802,12 @@
     (define seller+spawn (Role 'start (list (Reacts StartEvt (Spawn seller)))))
     (define rg (run/timeout (thunk (compile seller+spawn))))
     (check-true (role-graph? rg))
-    (define rgi (compile/internal-events rg))
+    (define rgi (compile/internal-events rg seller+spawn))
     (check-true (role-graph? rgi))
     (define srg (compile seller))
     (check-true (run/timeout (thunk (simulates?/rg rg rg))))
     (check-false (run/timeout (thunk (simulates?/rg rg srg))))
-    (check-true (run/timeout (thunk (simulates?/rg srg rg))))
+    (check-false (run/timeout (thunk (simulates?/rg srg rg))))
     (check-true (run/timeout (thunk (simulates?/rg rgi srg))))
     (check-true (run/timeout (thunk (simulates?/rg srg rgi)))))
   (test-case
@@ -841,7 +822,7 @@
                                                 (Role 'know (list))))))))))
     (define rg (run/timeout (thunk (compile role))))
     (check-true (role-graph? rg))
-    (define rgi (run/timeout (thunk (compile/internal-events rg))))
+    (define rgi (run/timeout (thunk (compile/internal-events rg role))))
     (check-true (role-graph? rgi))
     (define state-names (hash-keys (role-graph-states rgi)))
     (for ([sn (in-list state-names)])
@@ -998,24 +979,19 @@
             (for/fold ([st st])
                       ([c (in-list children)])
               (set-remove st c)))
-          (define-values (final-txns _)
-            (for/fold ([txns (set (transition '() st-))]
-                       [pending-effs rest])
-                      ([f-name (in-list children)])
-              (define stop-effs (hash-ref (hash-ref txn# f-name) (StopOf f-name)))
-              (define stop-effs+ (if (set-empty? stop-effs)
-                                     (set '())
-                                     stop-effs))
-              (define new-txns
-                (for*/set ([txn (in-set txns)]
-                           [st (in-value (transition-dest txn))]
-                           [effs* (in-set stop-effs+)]
-                           [next-txn (in-set (loop st (append pending-effs effs*)))])
-                  (transition (append (transition-effs txn)
-                                      (transition-effs next-txn))
-                              (transition-dest next-txn))))
-              (values new-txns '())))
-          final-txns])])))
+          (for/fold ([txns (set (transition '() st-))])
+                    ([f-name (in-list children)])
+            (define stop-effs (hash-ref (hash-ref txn# f-name) (StopOf f-name)))
+            (define stop-effs+ (if (set-empty? stop-effs)
+                                   (set '())
+                                   stop-effs))
+            (for*/set ([txn (in-set txns)]
+                       [st (in-value (transition-dest txn))]
+                       [effs* (in-set stop-effs+)]
+                       [next-txn (in-set (loop st (append effs* rest)))])
+              (transition (append (transition-effs txn)
+                                  (transition-effs next-txn))
+                          (transition-dest next-txn))))])])))
 
 (module+ test
   (test-case
@@ -1025,61 +1001,7 @@
                                 (set)
                                 (facet-tree (hash) (hash))
                                 (hash)))
-    (check-equal? txns (set (transition (list (realize Int) (realize String)) (set)))))
-  (test-case
-      "another bug in apply-effects"
-    ;; was duplicating some effects
-    (define r #s(Role
-                 run-a-round342
-                 (#s(Shares
-                     #s(Struct
-                        RoundT
-                        (#s(Base Symbol) #s(Base String) #s(List #s(Base String)))))
-                  #s(Reacts
-                     Start
-                     #s(Role
-                        wait364
-                        (#s(Reacts
-                            #s(Asserted #s(Struct LaterThanT (#s(Base Int))))
-                            #s(Branch
-                               ((#s(Branch
-                                    ((#s(Stop
-                                         run-a-round342
-                                         (#s(Role
-                                             over356
-                                             (#s(Shares
-                                                 #s(Struct
-                                                    ElectedT
-                                                    (#s(Base String)
-                                                     #s(Base String)))))))))
-                                     (#s(Stop
-                                         run-a-round342
-                                         (#s(Realizes
-                                             #s(Struct
-                                                StartRoundT
-                                                (#s(Set #s(Base String))
-                                                 #s(Set #s(Base String)))))))))))
-                                ())))))))))
-    (define labeled-role (label-internal-events r))
-    (define roles# (describe-roles labeled-role))
-    (define ft (make-facet-tree r))
-    (define current (set 'wait364 'run-a-round342))
-    (define eff* (list
-                  (stop 'run-a-round342)
-                  (realize
-                   '#s(internal-label
-                       initial31336
-                       #s(Struct
-                          StartRoundT
-                          (#s(Set #s(Base String)) #s(Set #s(Base String))))))))
-    (check-equal? (apply-effects eff* current ft roles#)
-                  (set (transition
-                        (list
-                         (realize
-                          '#s(internal-label
-                              initial31336
-                              #s(Struct StartRoundT (#s(Set #s(Base String)) #s(Set #s(Base String)))))))
-                        (set))))))
+    (check-equal? txns (set (transition (list (realize Int) (realize String)) (set))))))
 
 ;; FacetTree FacetName (Setof FacetName) -> (List FacetName)
 ;; return the facets in names that are children of the given facet nm, ordered
@@ -1596,7 +1518,6 @@
            (verify g (set-add assumptions goal)))
          (unless (same-on-specified-events? transitions1
                                             transitions2
-                                            sn1
                                             verify/with-current-assumed)
            (return #f))
          (return (same-on-extra-events? transitions1
@@ -1623,178 +1544,6 @@
              ))])))
   (verify (equiv st0-1 st0-2) (set)))
 
-;; Role Role -> Bool
-(define (simulates?/report-error impl spec)
-  (define impl-rg (compile/internal-events (compile impl)))
-  (define spec-rg (compile/internal-events (compile spec)))
-  (cond
-    [(detected-cycle? impl-rg)
-     (printf "Detected Cycle in Implementation!\n")
-     (describe-detected-cycle impl-rg)
-     #f]
-    [(detected-cycle? spec-rg)
-     (printf "Detected Cycle in Specification!\n")
-     (describe-detected-cycle spec-rg)
-     #f]
-    [(simulates?/rg impl-rg spec-rg)
-     #t]
-    [else
-     (define trace (find-simulation-counterexample impl-rg spec-rg))
-     (print-failing-trace trace impl-rg spec-rg)
-     #f]))
-
-;; DetectedCycle -> Void
-(define (describe-detected-cycle dc)
-  (printf "Initial State: ~a\n" (detected-cycle-start dc))
-  (for ([step (in-list (detected-cycle-steps dc))])
-    (printf "  :: ~a ==> ~a\n" (D->label (traversal-step-evt step)) (traversal-step-dest step))))
-
-;; a FailingTrace is a (failing-trace (Listof Transition) (Listof Transition) (Listof TraceStep))
-(struct failing-trace (impl-path spec-path steps) #:transparent)
-
-;; a TraceStep is one of
-;; - (both-step D)
-;; - (impl-step D)
-;; - (spec-step D)
-;; describing either both the spec and the implementation responding to an
-;; event, only the implementation, or only the spec
-(struct both-step (evt) #:transparent)
-(struct impl-step (evt) #:transparent)
-(struct spec-step (evt) #:transparent)
-
-;; FailingTrace RoleGraph RoleGraph -> Void
-(define (print-failing-trace trace impl-rg spec-rg)
-  (match-define (role-graph _ impl-st#) impl-rg)
-  (match-define (role-graph _ spec-st#) spec-rg)
-  (match-define (failing-trace impl-path spec-path steps) trace)
-  (define SEP (make-string 40 #\;))
-  (define (print-sep)
-    (newline)
-    (displayln SEP)
-    (newline))
-  (let loop ([steps steps]
-             [impl-path impl-path]
-             [spec-path spec-path]
-             ;; because the path might end with an impl-step or spec-step, remember the last
-             ;; states we've seen so we can print its assertions at the right time
-             [last-spec-state (transition-dest (car spec-path))]
-             [last-impl-state (transition-dest (car impl-path))])
-    (define (get-spec-dest)
-      (transition-dest (car spec-path)))
-    (define (get-impl-dest)
-      (transition-dest (car impl-path)))
-    (match steps
-      [(cons step more-steps)
-       (print-sep)
-       (printf "In response to event:\n")
-       (match step
-         [(or (both-step D)
-              (impl-step D)
-              (spec-step D))
-          (pretty-print D)])
-       (when (or (both-step? step) (impl-step? step))
-         (define impl-effs (transition-effs (car impl-path)))
-         (printf "Implementation steps to state:\n")
-         (pretty-print (get-impl-dest))
-         (unless (empty? impl-effs)
-           (printf "With Effects:\n")
-           (pretty-print impl-effs)))
-       (when (empty? more-steps)
-         (define impl-final (if (spec-step? step) last-impl-state (get-impl-dest)))
-         (printf "Implementation Assertions:\n")
-         (pretty-print (state-assertions (hash-ref impl-st# impl-final))))
-       (when (or (both-step? step) (spec-step? step))
-         (define spec-effs (transition-effs (car spec-path)))
-         (printf "Specification steps to state:\n")
-         (pretty-print (get-spec-dest))
-         (unless (empty? spec-effs)
-           (printf "With Effects:\n")
-           (pretty-print spec-effs)))
-       (when (empty? more-steps)
-         (define spec-final (if (impl-step? step) last-spec-state (get-spec-dest)))
-         (printf "Specification Assertions:\n")
-         (pretty-print (state-assertions (hash-ref spec-st# spec-final))))
-       (loop more-steps
-             (if (spec-step? step) impl-path (cdr impl-path))
-             (if (impl-step? step) spec-path (cdr spec-path))
-             (if (impl-step? step) last-spec-state (get-spec-dest))
-             (if (spec-step? step) last-impl-state (get-impl-dest)))]
-      [_
-       (newline)
-       (void)])))
-
-;; RoleGraph RoleGraph -> Trace
-;; assuming impl-rg does not simulate spec-rg, find a trace of transitions
-;; (event + effects + destination assertions) demonstrating different behaviors
-(define (find-simulation-counterexample impl-rg spec-rg)
-  (match-define (role-graph impl-st0 impl-st#) impl-rg)
-  (match-define (role-graph spec-st0 spec-st#) spec-rg)
-  ;; inside loop, the each trace field is in reverse
-  (let loop ([work (list (failing-trace (list (transition '() impl-st0))
-                                        (list (transition '() spec-st0))
-                                        (list (both-step StartEvt))))]
-             #;[visited (set)])
-    (match work
-      [(cons (failing-trace impl-path/rev spec-path/rev steps/rev) more-work)
-       (match-define (transition impl-effs impl-dest) (car impl-path/rev))
-       (match-define (transition spec-effs spec-dest) (car spec-path/rev))
-       (define last-step (car steps/rev))
-       (cond
-         [(or (impl-step? last-step)
-              ;; when only the implementation steps, no need to compare effects on transitions
-              (and (spec-step? last-step) (empty? spec-effs))
-              (effects-subsequence? spec-effs impl-effs))
-          ;; cascading conds will help with development and isolating where things go wrong
-          (match-define (state _ impl-transition# impl-assertions) (hash-ref impl-st# impl-dest))
-          (match-define (state _ spec-transition# spec-assertions) (hash-ref spec-st# spec-dest))
-          (cond
-            ;; n.b. internal events should be compiled away by now or this wouldn't work
-            [(assertion-superset? impl-assertions spec-assertions)
-             ;; same effects and same assertions, compare transitions
-             ;; TODO: similarity to `same-on-specified-events?`
-             (define spec-matching-txns
-               (for*/list ([(spec-D spec-txns) (in-hash spec-transition#)]
-                           [(impl-D impl-txns) (in-hash impl-transition#)]
-                           #:when (D<:? spec-D impl-D)
-                           [spec-txn (in-set spec-txns)]
-                           [impl-txn (in-set impl-txns)])
-                 (failing-trace (cons impl-txn impl-path/rev)
-                                (cons spec-txn spec-path/rev)
-                                (cons (both-step spec-D) steps/rev))))
-             ;; transitions that the spec has but the implementation doesn't respond to
-             ;; TODO: similarity to `same-on-extra-events?`
-             (define impl-evts (hash-keys impl-transition#))
-             (define spec-extra-txns
-               (for*/list ([(spec-D spec-txns) (in-hash spec-transition#)]
-                           ;; TODO - this more or less assumes that *any* event matching impl-D also matches spec-evt, which I'm not sure is quite right
-                           #:unless (for/or ([impl-evt (in-list impl-evts)])
-                                      (D<:? impl-evt spec-D))
-                           [spec-txn (in-set spec-txns)])
-                 (failing-trace impl-path/rev
-                                (cons spec-txn spec-path/rev)
-                                (cons (spec-step spec-D) steps/rev))))
-             ;; TODO: similarity to above code
-             ;; transitions that the implementation has that the spec doesn't respond to
-             (define spec-evts (hash-keys spec-transition#))
-             (define impl-extra-txns
-               (for*/list ([(impl-D impl-txns) (in-hash impl-transition#)]
-                           ;; TODO - this more or less assumes that *any* event matching impl-D also matches spec-evt, which I'm not sure is quite right
-                           #:unless (for/or ([spec-evt (in-list spec-evts)])
-                                      (D<:? spec-evt impl-D))
-                           [impl-txn (in-set impl-txns)])
-                 (failing-trace (cons impl-txn impl-path/rev)
-                                spec-path/rev
-                                (cons (impl-step impl-D) steps/rev))))
-             (loop (append more-work spec-matching-txns spec-extra-txns impl-extra-txns))]
-            [else
-             ;; states have different assertions
-             (failing-trace (reverse impl-path/rev) (reverse spec-path/rev) (reverse steps/rev))])]
-         [else
-          ;; transitions have different effects
-          (failing-trace (reverse impl-path/rev) (reverse spec-path/rev) (reverse steps/rev))])]
-      [_
-       (error "ran out of work")])))
-
 ;; (List Role) -> (Hashof RoleName (Setof τ))
 ;; map each role's name to the assertions it contributes
 (define (all-roles-assertions roles)
@@ -1822,11 +1571,7 @@
 ;;   as determined by the verify procedure
 ;;   and the effects on the edge going to Y are a supersequence of the effects
 ;;   on the edge to Y
-;; and:
-;; Determine if the events in transitions2 that don't have any match in transitions1, are:
-;;   - all effect free
-;;   - verify with sn1 matched to each destination
-(define (same-on-specified-events? transitions1 transitions2 sn1 verify)
+(define (same-on-specified-events? transitions1 transitions2 verify)
   (for/and ([(D2 edges2) (in-hash transitions2)])
     (define edges1
       (for/fold ([agg (set)])
@@ -1840,11 +1585,7 @@
         (set-union agg txns1)))
     (cond
       [(set-empty? edges1)
-       ;; - I think this is right, as long as the current state of the implementation
-       ;; matches all states the spec steps to --- unless there are effects on the transition
-       (for/and ([txn (in-set edges2)])
-         (and (empty? (transition-effs txn))
-              (verify (equiv sn1 (transition-dest txn)))))]
+       #f]
       [else
        (define combos (make-combinations edges1 edges2))
        (verify (one-of combos))])))
@@ -1953,69 +1694,19 @@
 (define (simulating-subgraphs impl spec)
   ;; assume spec doesn't have any internal events
   (define spec-rg (compile spec))
-  (define impl-rg (compile/internal-events (compile impl)))
+  (define impl-rg (compile/internal-events (compile impl) impl))
   (define evts (relevant-events spec-rg))
   (for/list ([srg (subgraphs impl-rg evts)]
              #:when (simulates?/rg srg spec-rg))
     srg))
 
-;; Role Role -> (Maybe RoleGraph)
-;; try to find any subgraph of the implementation simulating the spec
-;; TODO: would be nice to find the largest
-(define (find-simulating-subgraph impl spec)
-  (define spec-rg (compile spec))
-  (define impl-rg (compile/internal-events (compile impl)))
-  (find-simulating-subgraph/rg impl-rg spec-rg))
-
-;; RoleGraph RoleGraph -> (Maybe RoleGraph)
-(define (find-simulating-subgraph/rg impl-rg spec-rg)
-  (define evts (relevant-events spec-rg))
-  (for/first ([srg (subgraphs impl-rg evts)]
-              #:when (simulates?/rg srg spec-rg))
-    srg))
-
-;; Role Role -> Bool
-(define (find-simulating-subgraph/report-error impl spec)
-  (define spec-rg (compile spec))
-  (define impl-rg (compile/internal-events (compile impl)))
-  (define ans (find-simulating-subgraph/rg impl-rg spec-rg))
-  (cond
-    [ans
-     #t]
-    [else
-     (define-values (ft sg) (find-largest-simulating-subgraph-counterexample impl-rg spec-rg))
-     (print-failing-trace ft impl-rg spec-rg)
-     #f]))
-
-;; RoleGraph RoleGraph -> (Values FailingTrace RoleGraph)
-;; assuming impl does not have any simulating subgraphs of spec
-;; largest *trace*, not largest subgraph
-(define (find-largest-simulating-subgraph-counterexample impl-rg spec-rg)
-  (define evts (relevant-events spec-rg))
-  (define-values (trace len rg)
-    (for/fold ([best-trace #f]
-               [best-length 0]
-               [best-subgraph #f])
-              ([srg (subgraphs impl-rg evts)])
-      (define ft (find-simulation-counterexample srg spec-rg))
-      (define len (failing-trace-length ft))
-      ;; thing >= will prefer larger graphs
-      (if (>= len best-length)
-          (values ft len srg)
-          (values best-trace best-length best-subgraph))))
-  (values trace rg))
-
-;; FailingTrace -> Int
-(define (failing-trace-length ft)
-  (length (failing-trace-steps ft)))
-
 (module+ test
   (test-case
       "task manager has task performer subgraphs"
     (define tpr (parse-T task-performer-spec))
     (define tmr (parse-T task-manager-ty))
     (define ans (simulating-subgraphs tmr tpr))
-    (check-equal? (length ans) 340)
+    (check-equal? (length ans) 68)
     (define tprg (compile tpr))
     (check-true (simulates?/rg (first ans) tprg))
     (check-true (simulates?/rg (second ans) tprg))))
@@ -2055,16 +1746,15 @@
      (define st#
        (for/hash ([st (in-list states*)])
          (match-define (state _ orig-txn# assertions) (hash-ref state# st))
-         (define (enabled-txns D)
-           (define orig-txns (hash-ref orig-txn# D))
-           (for/set ([txn (in-set orig-txns)]
-                     #:when (set-member? states (transition-dest txn)))
-             txn))
          (define txn#
-           (for*/hash ([D (in-hash-keys orig-txn#)]
-                       #:when (event-enabled? D)
-                       [new-txns (in-value (enabled-txns D))]
-                       #:unless (set-empty? new-txns))
+           (for/hash ([D (in-hash-keys orig-txn#)]
+                      #:when (event-enabled? D))
+             (define orig-txns (hash-ref orig-txn# D))
+             (define new-txns
+               (for/set ([txn (in-set orig-txns)]
+                         #:when (set-member? states (transition-dest txn)))
+                 txn))
+             ;; TODO - what if new-txns is empty?
              (values D new-txns)))
          (values st (state st txn# assertions))))
      (for ([st0 (in-list states*)])
@@ -2887,12 +2577,10 @@
       "job manager reads and compiles"
     (define jmr (run/timeout (thunk (parse-T job-manager-actual))))
     (check-true (Role? jmr))
-    (define jm (run/timeout (thunk (compile jmr)) 5000))
+    (define jm (run/timeout (thunk (compile jmr))))
     (check-true (role-graph? jm))
-    (define jmi (run/timeout (thunk (compile/internal-events jm)) 5000))
-    (check-true (role-graph? jmi))
-    ;; TODO : times out, probably due to infinite loop
-    #;(check-true (run/timeout (thunk (simulates?/rg jmi jmi)) 100000))))
+    (define jmi (run/timeout (thunk (compile/internal-events jm jmr))))
+    (check-true (run/timeout (thunk (simulates?/rg jmi jmi))))))
 
 (define task-runner-ty
   '(Role
@@ -3027,12 +2715,12 @@
     (check-false (simulates? tm (parse-T task-performer-spec)))))
 
 
-#;(module+ test
+(module+ test
   (test-case
       "job manager subgraph(s) implement task assigner"
     (define jmr (run/timeout (thunk (parse-T job-manager-actual))))
     (define tar (parse-T task-assigner-spec))
-    (define ans (run/timeout (thunk (simulating-subgraphs jmr tar)) 4000))
+    (define ans (run/timeout (thunk (simulating-subgraphs jmr tar)) 1800))
     (check-true (list? ans))
     (check-false (empty? ans))))
 
@@ -3302,40 +2990,7 @@
                                  (Stop y))))))
   (define r (parse-T ty))
   (define rg (compile r))
-  (define rgi (compile/internal-events rg))
+  (define rgi (compile/internal-events rg r))
   (render-to-file rg "before.dot")
   (render-to-file rgi "after.dot")
 )
-
-(module+ test
-  (test-case
-    "regression: ok for implementation not to have edges if the current state matches"
-    (define a (role-graph
-               (set 'seller341 'during-inner343)
-               (hash
-                (set 'seller341 'during-inner343)
-                (state
-                 (set 'seller341 'during-inner343)
-                 '#hash()
-                 (set
-                  '#s(Observe #s(Observe #s(Struct BookQuoteT (#s(Base String) #s(Mk⋆)))))
-                  '#s(Struct BookQuoteT (#s(Base String) #s(Base Int))))))))
-    (define b (role-graph
-               (set 'seller)
-               (hash
-                (set 'seller)
-                (state
-                 (set 'seller)
-                 (hash
-                  '#s(Asserted #s(Observe #s(Struct BookQuoteT (#s(Base String) #s(Mk⋆)))))
-                  (set (transition '() (set '_ 'seller))))
-                 (set
-                  '#s(Observe #s(Observe #s(Struct BookQuoteT (#s(Base String) #s(Mk⋆)))))))
-                (set '_ 'seller)
-                (state
-                 (set '_ 'seller)
-                 '#hash()
-                 (set
-                  '#s(Observe #s(Observe #s(Struct BookQuoteT (#s(Base String) #s(Mk⋆)))))
-                  '#s(Struct BookQuoteT (#s(Base String) #s(Base Int))))))))
-    (check-true (run/timeout (thunk (simulates?/rg a b))))))

racket/typed/roles.rkt

@@ -4,15 +4,11 @@
          #%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
+         require only-in
          ;; Start dataspace programs
          run-ground-dataspace
          ;; Types
-         Tuple Bind Discard → ∀ AssertionSet
+         Tuple Bind Discard → ∀
          Role Reacts Shares Asserted Retracted Message OnDataflow Stop OnStart OnStop
          Know Forget Realize
          Branch Effs
@@ -21,8 +17,8 @@
          Computation Value Endpoints Roles Spawns Sends
          →fn proc
          ;; Statements
-         let let* if spawn dataspace start-facet set! begin block stop begin/dataflow #;unsafe-do
-         when unless send! realize! define during/spawn
+         let let* if spawn dataspace start-facet set! begin stop begin/dataflow #;unsafe-do
+         when unless send! realize! define
          ;; Derived Forms
          during During
          define/query-value
@@ -33,7 +29,7 @@
          ;; endpoints
          assert know on field
          ;; expressions
-         tuple select lambda λ ref (struct-out observe) (struct-out message) (struct-out inbound) (struct-out outbound)
+         tuple select lambda ref observe inbound outbound
          Λ inst call/inst
          ;; making types
          define-type-alias
@@ -47,7 +43,7 @@
          ;; primitives
          (all-from-out "prim.rkt")
          ;; expressions
-         (except-out (all-from-out "core-expressions.rkt") mk-tuple tuple-select)
+         (all-from-out "core-expressions.rkt")
          ;; lists
          (all-from-out "list.rkt")
          ;; sets
@@ -63,13 +59,10 @@
          (all-from-out "either.rkt")
          ;; DEBUG and utilities
          print-type print-role role-strings
-         ;; Behavioral Roles
-         export-roles export-type check-simulates check-has-simulating-subgraph lift+define-role
-         verify-actors
-         ;; LTL Syntax
-         True False Always Eventually Until WeakUntil Implies And Or Not A M
          ;; Extensions
          match cond
+         ;; require & provides
+         require provide
          submod for-syntax for-meta only-in except-in
          require/typed
          require-struct
@@ -87,7 +80,6 @@
 
 (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)
@@ -96,12 +88,6 @@
 (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))
@@ -137,20 +123,7 @@
 ;; Core forms
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-(define-typed-syntax start-facet
-  [(_ name:id #:implements ~! spec:type ep ...+) ≫
-   [⊢ (start-facet name ep ...) ≫ e- (⇒ ν-f (~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- (⇒ ν-f (~effs impl-ty))]
-   #:fail-unless (type-has-simulating-subgraphs? #'impl-ty #'spec.norm)
-                 "no subset implements specified behavior"
-   ------------------------------------------------------------
-   [≻ e-]]
-  [(_ name:id ep ...+) ≫
+(define-typed-syntax (start-facet 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)
@@ -180,51 +153,23 @@
   [⊢ (syndicate:react (let- ([#,name-- (#%app- syndicate:current-facet-id)])
                         #,@ep-...))
      (⇒ : ★/t)
-     (⇒ ν-f (τ))]])
+     (⇒ ν-f (τ))])
 
-(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-
-                (⇒ ν-ep (~effs τ-ep ...))
-                (⇒ ν-f (~effs))
-                (⇒ ν-s (~effs))]
-  #:with pat- (substs #'(x- ...) #'(x ...) (compile-syndicate-pattern #'pat+))
-  #:with τc:type (current-communication-type)
-  #:with τ-facet (type-eval #'(Role (_) τ-ep ...))
-  #:with τ-spawn (mk-ActorWithRole- #'(τc.norm τ-facet))
-  #:with τ-endpoint (type-eval #'(Reacts (Asserted τp) τ-spawn))
-  ------------------------------
-  [⊢ (syndicate:during/spawn pat- bdy-)
+(define-typed-syntax (field [x:id τ-f:type e:expr] ...) ≫
+  #:fail-unless (stx-andmap flat-type? #'(τ-f ...)) "keep your uppity data outta my fields"
+  [⊢ e ≫ e- (⇐ : τ-f)] ...
+  #:fail-unless (stx-andmap pure? #'(e- ...)) "field initializers not allowed to have effects"
+  #:with (x- ...) (generate-temporaries #'(x ...))
+  #:with (τ ...) (stx-map type-eval #'((Field τ-f.norm) ...))
+  #:with MF (type-eval #'MakesField)
+  ----------------------------------------------------------------------
+  [⊢ (erased (field/intermediate [x x- τ e-] ...))
      (⇒ : ★/t)
-     (⇒ ν-ep (τ-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 (stx-andmap pure? #'(e- ...)) "field initializers not allowed to have effects"
-   #:with (x- ...) (generate-temporaries #'(x ...))
-   #:with (τ ...) (stx-map type-eval #'((Field τ-f.norm) ...))
-   #:with MF (type-eval #'MakesField)
-   ----------------------------------------------------------------------
-   [⊢ (erased (field/intermediate [x x- τ e-] ...))
-      (⇒ : ★/t)
-      (⇒ ν-ep (MF))]]
-  [(_ flds ... [x:id e:expr] more-flds ...) ≫
-   #:cut
-   [⊢ e ≫ e- (⇒ : τ)]
-   --------------------
-   [≻ (field flds ... [x τ e-] more-flds ...)]])
+     (⇒ ν-ep (MF))])
 
 (define-typed-syntax (assert e:expr) ≫
   [⊢ e ≫ e- (⇒ : τ)]
   #:fail-unless (pure? #'e-) "expression not allowed to have effects"
-  #:fail-unless (allowed-interest? #'τ) "overly broad interest, ?̱̱★ and ??★ not allowed"
   #:with τs (mk-Shares- #'(τ))
   -------------------------------------
   [⊢ (syndicate:assert e-) (⇒ : ★/t)
@@ -336,7 +281,6 @@
    #: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-
                  (⇒ ν-ep (~effs))
@@ -379,13 +323,10 @@
      [⊢ (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 (<: #'τ-o #'τ-c.norm)
                 (format "Output ~a not valid in dataspace ~a" (type->str #'τ-o) (type->str #'τ-c.norm))
-  #:with τ-final #;(mk-Actor- #'(τ-c.norm)) (mk-ActorWithRole- #'(τ-c.norm τ-f ...))
+  #:with τ-final (mk-Actor- #'(τ-c.norm))
   #:fail-unless (<: #'τ-a #'τ-final)
                 "Spawned actors not valid in dataspace"
   #:fail-unless (project-safe? (∩ (strip-? #'τ-o) #'τ-c.norm)
@@ -457,6 +398,11 @@
   #:with inst-p (instantiate-pattern #'p+)
   #:with start-e (if (attribute k) #'know #'asserted)
   #:with stop-e (if (attribute k) #'forget #'retracted)
+  #:with res #'(on (start-e p+)
+                   (start-facet during-inner
+                                (on (stop-e inst-p)
+                                    (stop during-inner))
+                                s ...))
   ----------------------------------------
   [≻ (on (start-e p+)
          (start-facet during-inner
@@ -482,6 +428,8 @@
       #:datum-literals (tuple discard bind)
       [(tuple p ...)
        #`(tuple #,@(stx-map loop #'(p ...)))]
+      [(k:kons1 p)
+       #`(k #,(loop #'p))]
       [(bind x:id τ)
        #'x]
       ;; not sure about this
@@ -629,10 +577,8 @@
    [⊢ 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))])
+  [⊢ (#%app- syndicate:run-ground s- ...) (⇒ : (AssertionSet τ-c))])
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Utilities
@@ -659,207 +605,6 @@
   ----------------------------------------
   [⊢ (#%app- list- (#%datum- . s) ...) (⇒ : (List String))])
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; LTL Syntax
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(define-type LTL : LTL)
-
-(define-type True : LTL)
-(define-type False : 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 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
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; 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 Spawns proto:Spawn
-                    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
-                    ;; LTL
-                    True #t
-                    False #f
-                    Always proto:always
-                    Eventually proto:eventually
-                    Until proto:strong-until
-                    WeakUntil proto:weak-until
-                    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))))
-
-  (define (synd->proto ty)
-    (let convert ([ty (resugar-type ty)])
-      (syntax-parse ty
-        #:literals (★/t Bind Discard ∀/internal →/internal Role/internal Stop Reacts Actor ActorWithRole)
-        [(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) body ...)
-         (proto:Role (syntax-e #'nm) (stx-map convert #'(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+)]
-        [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-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- (⇒ : τ) (⇒ ν-ep (~effs)) (⇒ ν-f ((~and r  (~Role (_) _ ...)))) (⇒ ν-s (~effs))]
-  ;; 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- (⇒ : τ) (⇒ ν-ep ()) (⇒ ν-f (r)) (⇒ ν-s ())])
-
-
-;; 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 " 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 ...))))])
-
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Tests
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -868,7 +613,7 @@
   (check-type
     (spawn (U (Observe (Tuple Int ★/t)))
            (start-facet echo
-                        (on (message (tuple 1 $x:Int))
+                        (on (message (tuple 1 $x))
                             #f)))
     : ★/t)
   (check-type (spawn (U (Message (Tuple String Int))

racket/typed/scribblings/typed-syndicate.scrbl

@@ -1,776 +0,0 @@
-#lang scribble/manual
-
-@(require (for-label (only-in racket struct)
-                     typed/syndicate/roles)
-          (prefix-in racket: (for-label racket))
-          (prefix-in untyped: (for-label syndicate/actor)))
-
-@title{Typed Syndicate}
-
-
-@defmodule[typed/syndicate/roles]
-
-@section{Overview}
-
-@section{Types}
-
-@deftogether[(@defidform[Int]
-              @defidform[Bool]
-              @defidform[String]
-              @defidform[ByteString]
-              @defidform[Symbol])]{
-Base types.
-}
-
-@defform[(U type ...)]{
-The type representing the union of @racket[type ...].
-}
-
-@defidform[⊥]{
-An alias for @racket[(U)].
-}
-
-@defidform[★/t]{
-The type representing any possible assertion, and, in an @racket[AssertionSet],
-the possibility for an infinite set of assertions.
-}
-
-@defidform[Discard]{
-The type of @racket[_] patterns.
-}
-
-@defform[(Bind type)]{
-The type of @racket[$] patterns.
-}
-
-@defidform[FacetName]{
-The type associated with identifiers bound by @racket[start-facet].
-}
-
-@defform[(Role (x) type ...)]{
-The type of a facet named @racket[x] and endpoints described by @racket[type
-...].
-}
-
-@defform[(Stop X type ...)]{
-The type of a @racket[stop] action.
-}
-
-@defform[(Field type)]{
-The type of a field containing values of @racket[type].
-}
-
-
-@defform[(Shares type)]{
-The type of an @racket[assert] endpoint.
-}
-
-@defform[#:literals (OnStart OnStop Asserted Retracted)
-         (Reacts EventDesc type ...)
-         #:grammar
-         [(EventDesc (code:line OnStart)
-                     (code:line OnStart)
-                     (code:line (Asserted event-type))
-                     (code:line (Retracted event-type)))]]{
-The type of a @racket[on] endpoint that reacts to events described by
-@racket[EventDesc] with the behavior given by @racket[type ...].
-}
-
-@deftogether[(@defidform[OnStart]
-              @defidform[OnStop]
-              @defform[(Asserted type)]
-              @defform[(Retracted type)])]{
-See @racket[Reacts].
-}
-
-@defform[(Actor type)]{
-The type of an actor that operates in a dataspace with a certain communication
-@racket[type].
-}
-
-@defform[(ActorWithRole comm-type behavior-type)]{
-An @racket[Actor] type with the additional @racket[behavior-type] describing the
-actor's behavior in terms of a @racket[Role].
-}
-
-@defform[(Sends type)]{
-The type of a @racket[send!] action.
-}
-
-@defform[(Realize type)]{
-The type of a @racket[realize!] action.
-}
-
-@deftogether[(@defform[(Branch type ...)]
-              @defform[(Effs type ...)])]{
-Types that may arise in descriptions in @racket[Role] types due to branching and
-sequencing.
-}
-
-@defform[(Tuple type ...)]{
-The type of @racket[tuple] expressions.
-}
-
-@defidform[Unit]{
-An alias for @racket[(Tuple)].
-}
-
-@defform[(AssertionSet type)]{
-The type for a set of assertions of a certain @racket[type]. Note that these are
-not interoperable with the general purpose @racket[set] data structures.
-}
-
-@defform[(∀ (X ...) type)]{
-Universal quantification over types.
-}
-
-@defform[#:literals (Computation Value Endpoints Roles Spawns)
-         (→ type ... (Computation (Value result-type)
-                                  (Endpoints ep-type ...)
-                                  (Roles role-type ...)
-                                  (Spawns spawn-type ...)))]{
-The type of a function with parameters @racket[type ...] that returns @racket[result-type]. The type includes the effects of any actions performed by the function:
-@itemlist[
-  @item{@racket[Endpoints]: includes any endpoint installation effects, such as from @racket[assert] and @racket[on].}
-  @item{@racket[Roles]: includes any script action effects, such as from @racket[start-facet], @racket[stop], and @racket[send!].}
-  @item{@racket[Spawns]: includes descriptions of any @racket[spawn] actions.}
-]
-}
-
-@defform[(→fn type-in ... type-out)]{
-Shorthand for a @racket[→] type with no effects.
-}
-
-@defform[(proc maybe-quantifiers type-in ... maybe-arrow type-out
-               maybe-endpoints
-               maybe-roles
-               maybe-spawns)
-         #:grammar
-         [(maybe-quantifiers (code:line)
-                             (code:line #:forall (X ...)))
-          (maybe-arrow (code:line)
-                       (code:line →)
-                       (code:line ->))
-          (maybe-endpoints (code:line)
-                           (code:line #:endpoints (e ...)))
-          (maybe-roles (code:line)
-                       (code:line #:roles (r ...)))
-          (maybe-spawns (code:line)
-                        (code:line #:spawns (s ...)))]]{
-A more convenient notation for writing (potentially polymorphic) function types
-with effects. Shorthand for @racket[(∀ (X ...) (→ type-in ... (Computation
-(Value type-out) (Endpoints e ...) (Roles r ...) (Spawns s ...))))].
-}
-
-@deftogether[(@defform[(Computation type ...)]
-              @defform[(Value type)]
-              @defform[(Endpoints type)]
-              @defform[(Roles type)]
-              @defform[(Spawns type)])]{
-See @racket[→].
-}
-
-@section{User Defined Types}
-
-@defform*[[(define-type-alias id type)
-           (define-type-alias (ty-cons-id arg-id ...) type)]]{
-Define @racket[id] to be the same as @racket[type], or create a type constructor
-@racket[(ty-cons-id ty ...)] whose meaning is @racket[type] with references to
-@racket[arg-id ...] replaced by @racket[ty ...].
-}
-
-@defform[(define-constructor (ctor-id slot-id ...)
-               maybe-type-ctor
-               maybe-alias ...)
-         #:grammar
-         [(maybe-type-ctor (code:line)
-                           (code:line #:type-constructor type-ctor-id))
-          (maybe-alias (code:line)
-                       (code:line #:with alias alias-body))]]{
-Defines a container analagous to a prefab @racket[struct]. Includes accessor
-functions for each @racket[slot-id]. (But not, presently, a predicate function).
-
-When a @racket[type-ctor-id] is provided, the type of such structures is
-@racket[(type-ctor-id type ...)], where each @racket[type] describes the value
-of the corresponding slot. When not provided, the type constructor is named by
-appending @racket["/t"] to @racket[ctor-id].
-
-Each @racket[alias] and @racket[alias-body] creates an instance of
-@racket[define-type-alias].
-}
-
-@defform[#:literals (:)
-         (define-constructor* (ctor-id : type-ctor-id slot-id ...)
-               maybe-alias ...)]{
-An abbreviated form of @racket[define-constructor].
-}
-
-@defform[#:literals (:)
-         (assertion-struct ctor-id : type-ctor-id (slot-id ...))]{
-An abbreviated form of @racket[define-constructor].
-}
-
-@defform[#:literals (:)
-         (message-struct ctor-id : type-ctor-id (slot-id ...))]{
-An abbreviated form of @racket[define-constructor].
-}
-
-@section{Actor Forms}
-
-@defform[(run-ground-dataspace type expr ...)]{
-Starts a ground, i.e. main, dataspace of the program, with the given
-communication @racket[type] and initial actors spawned by @racket[expr ...].
-}
-
-@defform[(spawn maybe-type s)
-         #:grammar
-         [(maybe-type (code:line)
-                      (code:line type))]]{
-Spawns an actor with behavior given by @racket[s]. The @racket[type] gives the
-communication type of the enclosing dataspace. When absent, @racket[type] is
-supplied by the nearest lexically enclosing @racket[spawn] or @racket[dataspace]
-form, if any exist.
-}
-
-@defform[(dataspace type expr ...)]{
-Spawns a dataspace with communication type @racket[type] as a child of the
-dataspace enclosing the executing actor. The script @racket[expr ...] spawns the
-initial actors of the new dataspace.
-}
-
-@defform[(start-facet id maybe-spec expr ...+)
-         #:grammar
-         [(maybe-spec (code:line)
-                      (code:line #:implements type)
-                      (code:line #:includes-behavior type))]]{
-Start a facet with name @racket[id] and endpoints installed through the
-evaluation of @racket[expr ...].
-}
-
-@defform[(stop id expr ...)]{
-Terminate the facet @racket[id] with continuation script @racket[expr ...]. Any
-facets started by the continuation script survive the termination of facet
-@racket[id].
-}
-
-@defform[#:literals (start stop message asserted retracted _ $)
-         (on event-description body ...+)
-         #:grammar
-         [(event-description (code:line start)
-                             (code:line stop)
-                             (code:line (message pattern))
-                             (code:line (asserted pattern))
-                             (code:line (retracted pattern)))
-          (pattern (code:line _)
-                   (code:line ($ id type))
-                   (code:line ($ id))
-                   (code:line $id)
-                   (code:line $id:type)
-                   (code:line (ctor pattern ...))
-                   (code:line expr))]]{
-Creates an event handler endpoint that responds to the event specified by
-@racket[event-description]. Executes the @racket[body ...] for each matching
-event, with any pattern variables bound to their matched value.
-
-Patterns have the following meanings:
-@itemlist[
-  @item{@racket[_] matches anything.}
-
-  @item{@racket[($ id type)] matches any value and binds it to @racket[id] with
-  assumed type @racket[type].}
-
-  @item{@racket[($ id)] is like @racket[($ id type)], but attempts to use the
-  current communication type to fill in the @racket[type] of potential matches.
-  May raise an error if no suitable communication type is in scope.}
-
-  @item{@racket[(? pred pattern)] matches values where @racket[(pred val)] is not
-     @racket[#f] and that match @racket[pattern].}
-
-  @item{@racket[$id:type] is shorthand for @racket[($ id type)].}
-
-  @item{@racket[$id] is shorthand for @racket[($ id)].}
-
-  @item{@racket[(ctor pat ...)] matches values built by applying the constructor
-    @racket[ctor] to values matching @racket[pat ...]. @racket[ctor] is usually
-    a @racket[struct] name.}
-
-  @item{@racket[expr] patterns match values that are @racket[equal?] to
-    @racket[expr].}
-]
-}
-
-@defform[(on-start expr ...+)]{
-Shorthand for @racket[(on start expr ...)].
-}
-
-@defform[(on-stop expr ...+)]{
-Shorthand for @racket[(on stop expr ...)].
-}
-
-@defform[(assert expr)]{
-Creates an assertion endpoint with the value of @racket[expr].
-}
-
-@defform[(know expr)]{
-Creates an internal assertion endpoint with the value of @racket[expr].
-}
-
-@defform[(send! expr)]{
-Broadcast a dataspace message with the value of @racket[expr].
-}
-
-@defform[(realize! expr)]{
-Broadcast an actor-internal message with the value of @racket[expr].
-}
-
-@defform[#:literals (:)
-         (field [id maybe-type expr] ...)
-         #:grammar
-         [(maybe-type (code:line)
-                      (code:line type)
-                      (code:line : type))]]{
-Defines fields of type @racket[type] with names @racket[id] and initial values
-@racket[expr]. If @racket[type] is not provided, the type of the initial
-expression is used as the type of the field.
-}
-
-@defform[(ref id)]{
-Reference the @racket[field] named @racket[id].
-}
-
-@defform[(set! id expr)]{
-Update the value  the @racket[field] named @racket[id].
-}
-
-@defform[(begin/dataflow expr ...+)]{
-Evaluate and perform the script @racket[expr ...], and then again each time a
-field referenced by the script updates.
-}
-
-@defform[(during pattern expr ...+)]{
-Engage in behavior for the duration of a matching assertion. The syntax of
-@racket[pattern] is the same as described by @racket[on].
-}
-
-@defform[(during/spawn pattern expr ...+)]{
-Like @racket[during], but spawns an actor for the behavior @racket[expr ...].
-}
-
-@defform[(define/query-value name absent-expr pattern expr
-                             maybe-on-add
-                             maybe-on-remove)
-         #:grammar
-         [(maybe-on-add (code:line)
-                        (code:line #:on-add on-add-expr))
-          (maybe-on-remove (code:line)
-                           (code:line #:on-remove on-remove-expr))]]{
-Equivalent to the untyped @racket[untyped:define/query-value].
-}
-
-@defform[(define/query-set name pattern expr
-                           maybe-on-add
-                           maybe-on-remove)
-         #:grammar
-         [(maybe-on-add (code:line)
-                        (code:line #:on-add on-add-expr))
-          (maybe-on-remove (code:line)
-                           (code:line #:on-remove on-remove-expr))]]{
-Equivalent to the untyped @racket[untyped:define/query-set].
-}
-
-@defform[(define/query-hash name pattern key-expr value-expr
-                            maybe-on-add
-                            maybe-on-remove)
-         #:grammar
-         [(maybe-on-add (code:line)
-                        (code:line #:on-add on-add-expr))
-          (maybe-on-remove (code:line)
-                           (code:line #:on-remove on-remove-expr))]]{
-Equivalent to the untyped @racket[untyped:define/query-hash].
-}
-
-@defform[(define/dataflow name maybe-type expr)
-         #:grammar
-         [(maybe-type (code:line)
-                      (code:line type))]]{
-Define a @racket[field] named @racket[name], whose value is reevaluated to the
-result of @racket[expr] each time any referenced field changes. When
-@racket[type] is not supplied, the field has the type of the given
-@racket[expr].
-}
-
-@section{Expressions}
-
-@defform*[#:literals (:)
-          [(ann expr : type)
-           (ann expr type)]]{
-Ensure that @racket[expr] has the given @racket[type].
-}
-
-@defform[(if test-expr then-expr else-expr)]{
-The same as Racket's @racket[racket:if].
-}
-
-@deftogether[(@defform[(cond [test-expr body-expr ...+] ...+)]
-              @defthing[else Bool #:value #t])]{
-Like Racket's @racket[racket:cond].
-}
-
-@defform[(when test-expr expr)]{
-Like Racket's @racket[racket:when], but results in @racket[#f] when
-@racket[test-expr] is @racket[#f].
-}
-
-@defform[(unless test-expr expr)]{
-Like Racket's @racket[racket:unless], but results in @racket[#f] when
-@racket[test-expr] is @racket[#f].
-}
-
-@defform[(let ([id expr] ...) body ...+)]{
-The same as Racket's @racket[racket:let].
-}
-
-@defform[(let* ([id expr] ...) body ...+)]{
-The same as Racket's @racket[racket:let*].
-}
-
-@defform[#:literals (:)
-         (lambda ([x opt-: type] ...) expr ...+)
-         #:grammar
-         [(opt-: (code:line)
-                 (code:line :))]]{
-Constructsa an anonymous function.
-}
-
-@defidform[λ]{Synonym for @racket[lambda].}
-
-@defform[(Λ (X ...) expr)]{
-Parametric abstraction over type variables @racket[X ...].
-}
-
-@defform[(inst expr type ...)]{
-Instantiates the type variables @racket[X ...] with @racket[type ...], where
-@racket[expr] has type @racket[(∀ (X ...) t)].
-}
-
-@defform*[#:literals (: → -> ∀)
-          [(define id : type expr)
-           (define id expr)
-           (define (id [arg-id opt-: arg-type] ... opt-res-ty) expr ...+)
-           (define (∀ (X ...) (id [arg-id opt-: arg-type] ... opt-res-ty)) expr ...+)]
-          #:grammar
-          [(opt-: (code:line) (code:line :))
-           (opt-res-ty (code:line)
-                       (code:line arr res-type))
-           (arr (code:line →) (code:line ->))]]{
-Define a constant or a (potentially polymorphic) function. Note that the
-function name @racket[id] is @emph{not} bound in the body.
-}
-
-@defform[(define-tuple (id ...) expr)]{
-Define @racket[id ...] to each of the slots of the tuple produced by
-@racket[expr].
-}
-
-@defform[(match-define pattern expr)]{
-Define the binders of @racket[pattern] to the matching values of @racket[expr].
-}
-
-@defform[(begin expr ...+)]{
-Sequencing form whose value and type is that of the final @racket[expr].
-}
-
-@defform[(block expr ...+)]{
-Like @racket[begin], but also introduces a definition context for its body.
-}
-
-@defform[(match expr [pattern body-expr ...+] ...+)]{
-Like Racket's @racket[racket:match] but with the pattern syntax described by
-@racket[on].
-}
-
-@defform[(tuple expr ...)]{
-Constructs a tuple of arbitrary arity.
-}
-
-@defform[(select i expr)]{
-Extract the @racket[i]th element of a @racket[tuple].
-}
-
-@defthing[unit Unit #:value (tuple)]
-
-@defform[(error format-expr arg-expr ...)]{
-Raises an exception using @racket[format-expr] as a format string together with
-@racket[arg-expr ...].
-}
-
-@deftogether[(
-@defthing[+ (→fn Int Int Int)]
-@defthing[- (→fn Int Int Int)]
-@defthing[* (→fn Int Int Int)]
-@defthing[< (→fn Int Int Bool)]
-@defthing[> (→fn Int Int Bool)]
-@defthing[<= (→fn Int Int Bool)]
-@defthing[>= (→fn Int Int Bool)]
-@defthing[= (→fn Int Int Bool)]
-@defthing[even? (→fn Int Bool)]
-@defthing[odd? (→fn Int Bool)]
-@defthing[add1 (→fn Int Int)]
-@defthing[sub1 (→fn Int Int)]
-@defthing[max (→fn Int Int Int)]
-@defthing[min (→fn Int Int Int)]
-@defthing[zero? (→fn Int Bool)]
-@defthing[positive? (→fn Int Bool)]
-@defthing[negative? (→fn Int Bool)]
-@defthing[current-inexact-milleseconds? (→fn Int)]
-@defthing[string=? (→fn String String Bool)]
-@defthing[bytes->string/utf-8 (→fn ByteString String)]
-@defthing[string->bytes/utf-8 (→fn String ByteString)]
-@defthing[gensym (→fn Symbol Symbol)]
-@defthing[symbol->string (→fn Symbol String)]
-@defthing[string->symbol (→fn String Symbol)]
-@defthing[not (→fn Bool Bool)]
-@defform[(/ e1 e2)]
-@defform[(and e ...)]
-@defform[(or e ...)]
-@defform[(equal? e1 e2)]
-@defform[(displayln e)]
-@defform[(printf fmt-expr val-expr ...)]
-@defform[(~a e ...)]
-)]{
-Primitive operations imported from Racket.
-}
-
-@defform[#:literals (:)
-         (for/fold ([acc-id maybe-:ty acc-expr] ...+)
-                   (for-clause ...)
-           body-expr ...+)
-         #:grammar
-         [(maybe-:ty (code:line)
-                     (code:line : acc-type))
-          (for-clause (code:line [id seq-expr])
-                      (code:line [id : type seq-expr])
-                      (code:line [(k-id v-id) hash-expr])
-                      (code:line #:when test-expr)
-                      (code:line #:unless test-expr)
-                      (code:line #:break test-expr))]]{
-Similar to Racket's @racket[racket:for/fold].
-
-When more than one @racket[acc-id] is used, the body of the loop must evaluate
-to a @racket[tuple] with one value for each accumulator, with the final tuple
-also being the result of the entire expression.
-
-Each @racket[seq-expr] should be of type @racket[Sequence], though expressions
-of type @racket[List] and @racket[Set] are automatically converted.
-}
-
-@deftogether[(
-@defform[(for/list (for-clause ...) body ...+)]
-@defform[(for/set (for-clause ...) body ...+)]
-@defform[(for/sum (for-clause ...) body ...+)]
-@defform[(for (for-clause ...) body ...+)]
-@defform[(for/first (for-clause ...) body ...+)]
-)]{
-Like their Racket counterparts. See @racket[for/fold] for the description of
-@racket[for-clause].
-
-Unlike @racket[racket:for/first], @racket[for/first] returns a @racket[Maybe]
-value to indicate success/failure.
-}
-
-@section{Require & Provide}
-
-@defform[(struct-out ctor-id)]{
-}
-
-@subsection{Requiring From Outside Typed Syndicate}
-
-@defform[#:literals (:)
-         (require/typed lib clause ...)
-         #:grammar
-         [(clause (code:line [id : type])
-                  (code:line opaque))
-          (opaque (code:line [#:opaque type-name])
-                  (code:line [#:opaque type-name #:arity op arity-nat]))
-          (opaque (code:line =) (code:line >) (code:line >=))]]{
-Import and assign types to bindings from outside Typed Syndicate.
-
-Note that @emph{unlike} Typed Racket, Typed Syndicate does not attach contracts
-to imported bindings.
-
-An @racket[#:opaque] declaration defines a type @racket[type-name] (or, in the
-@racket[#:arity] case, a type constructor) that may be used to describe imports
-but otherwise has no other operations.
-}
-
-@defform[(require-struct ctor-id #:as ty-ctor-id #:from lib maybe-omit-accs)
-         #:grammar
-         [(maybe-omit-accs (code:line)
-                           (code:line #:omit-accs))]]{
-Import a Racket @racket[struct] named @racket[ctor-id] and create a type
-constructor @racket[ty-ctor-id] for its instances.
-
-Unless @racket[#:omit-accs] is specified, defines the accessor functions for the
-struct.
-}
-
-
-@section{Builtin Data Structures}
-
-@deftogether[(@defstruct[observe ([claim any?]) #:omit-constructor]
-              @defform[(Observe type)])]{
-Constructs an assertion of interest.
-}
-
-@deftogether[(@defstruct[inbound ([assertion any?]) #:omit-constructor]
-              @defform[(Inbound type)])]{
-Constructor for an assertion inbound from an outer dataspace.
-}
-
-@deftogether[(@defstruct[outbound ([assertion any?]) #:omit-constructor]
-              @defform[(Outbound type)])]{
-Constructor for an assertion outbound to an outer dataspace.
-}
-
-@deftogether[(@defstruct[message ([body any?]) #:omit-constructor]
-              @defform[(Message type)])]{
-Constructor for a broadcast message.
-}
-
-@subsection{Lists}
-
-@defform[(List type)]{
-The type for @racket[cons] lists whose elements are of type @racket[type].
-}
-
-@deftogether[(
-@defthing[empty (List ⊥)]
-@defthing[empty? (∀ (X) (→fn (List X) Bool))]
-@defthing[cons (∀ (X) (→fn X (List X) (List X)))]
-@defthing[cons? (∀ (X) (→fn X (List X) Bool))]
-@defthing[first (∀ (X) (→fn (List X) X))]
-@defthing[second (∀ (X) (→fn (List X) X))]
-@defthing[rest (∀ (X) (→fn (List X) (List X)))]
-@defthing[member? (∀ (X) (→fn X (List X) Bool))]
-@defthing[reverse (∀ (X) (→fn (List X) (List X)))]
-@defthing[partition (∀ (X) (→fn (List X) (→fn X Bool) (List X)))]
-@defthing[map (∀ (X Y) (→fn (→fn X Y) (List X) (List Y)))]
-@defthing[argmax (∀ (X) (→fn (→fn X Int) (List X) X))]
-@defthing[argmin (∀ (X) (→fn (→fn X Int) (List X) X))]
-@defthing[remove (∀ (X) (→fn X (List X) (List X)))]
-@defthing[length (∀ (X) (→fn (List X) Int))]
-@defform[(list e ...)]
-)]{
-Like their Racket counterparts.
-}
-
-@subsection{Sets}
-
-@defform[(Set type)]{
-The type for sets whose elements are of type @racket[type].
-}
-
-@deftogether[(
-@defform[(set e ...)]
-@defform[(set-union st ...+)]
-@defform[(set-intersect st ...+)]
-@defform[(set-subtract st ...+)]
-@defthing[set-first (∀ (X) (→fn (Set X) X))]
-@defthing[set-empty? (∀ (X) (→fn (Set X) Bool))]
-@defthing[set-count (∀ (X) (→fn (Set X) Int))]
-@defthing[set-add (∀ (X) (→fn (Set X) X (Set X)))]
-@defthing[set-remove (∀ (X) (→fn (Set X) X (Set X)))]
-@defthing[set-member? (∀ (X) (→fn (Set X) X Bool))]
-@defthing[list->set (∀ (X) (→fn (List X) (Set X)))]
-@defthing[set->list (∀ (X) (→fn (Set X) (List X)))]
-)]{
-Like their Racket counterparts.
-}
-
-@subsection{Hashes}
-
-@defform[(Hash key-type value-type)]{
-The type for key/value hash tables.
-}
-
-@deftogether[(
-@defform[(hash key val ... ...)]
-@defthing[hash-set (∀ (K V) (→fn (Hash K V) K V (Hash K V)))]
-@defthing[hash-ref (∀ (K V) (→fn (Hash K V) K V))]
-@defthing[hash-ref/failure (∀ (K V) (→fn (Hash K V) K V V))]
-@defthing[hash-empty? (∀ (K V) (→fn (Hash K V) Bool))]
-@defthing[hash-has-key? (∀ (K V) (→fn (Hash K V) K Bool))]
-@defthing[hash-count (∀ (K V) (→fn (Hash K V) Int))]
-@defthing[hash-update (∀ (K V) (→fn (Hash K V) K (→fn V V) (Hash K V)))]
-@defthing[hash-update/failure (∀ (K V) (→fn (Hash K V) K (→fn V V) V (Hash K V)))]
-@defthing[hash-remove (∀ (K V) (→fn (Hash K V) K (Hash K V)))]
-@defthing[hash-map (∀ (K V R) (→fn (Hash K V) (→fn K V R) (List R)))]
-@defthing[hash-keys (∀ (K V) (→fn (Hash K V) (List K)))]
-@defthing[hash-values (∀ (K V) (→fn (Hash K V) (List V)))]
-@defthing[hash-union (∀ (K1 V1 K2 V2) (→fn (Hash K1 V1) (Hash K2 V2) (Hash (U K1 K2) (U V1 V2))))]
-@defthing[hash-union/combine (∀ (K V) (→fn (Hash K V) (Hash K V) (→fn V V V) (Hash K V)))]
-@defthing[hash-keys-subset? (∀ (K1 V1 K2 V2) (→fn (Hash K1 V1) (Hash K2 V2) Bool))]
-)]{
-Like their Racket counterparts. The /failure and /combine suffixes are in place
-of keyword arguments, which Typed Syndicate does not presently support.
-}
-
-@subsection{Sequences}
-
-@defform[(Sequence type)]{
-The type for a sequence of @racket[type] values.
-}
-
-@deftogether[(
-@defthing[empty-sequence (Sequence ⊥)]
-@defthing[sequence->list (∀ (X) (→fn (Sequence X) (List X)))]
-@defthing[sequence-length (∀ (X) (→fn (Sequence X) Int))]
-@defthing[sequence-ref (∀ (X) (→fn (Sequence X) Int Int))]
-@defthing[sequence-tail (∀ (X) (→fn (Sequence X) Int (Sequence X)))]
-@defthing[sequence-append (∀ (X) (→fn (Sequence X) (Sequence X) (Sequence X)))]
-@defthing[sequence-map (∀ (A B) (→fn (→fn A B) (Sequence A) (Sequence B)))]
-@defthing[sequence-andmap (∀ (X) (→fn (→fn X Bool) (Sequence X) Bool))]
-@defthing[sequence-ormap (∀ (X) (→fn (→fn X Bool) (Sequence X) Bool))]
-@defthing[sequence-fold (∀ (A B) (→fn (→fn A B A) (Sequence B) A))]
-@defthing[sequence-count (∀ (X) (→fn (→fn X Bool) (Sequence X) Int))]
-@defthing[sequence-filter (∀ (X) (→fn (→fn X Bool) (Sequence X) (Sequence X)))]
-@defthing[sequence-add-between (∀ (X) (→fn (Sequence X) X (Sequence X)))]
-@defthing[in-list (∀ (X) (→fn (List X) (Sequence X)))]
-@defthing[in-hash-keys (∀ (K V) (→fn (Hash K V) (Sequence K)))]
-@defthing[in-hash-values (∀ (K V) (→fn (Hash K V) (Sequence V)))]
-@defthing[in-range (→fn Int (Sequence Int))]
-@defthing[in-set (∀ (X) (→fn (Set X) (Sequence X)))]
-)]{
-Like their Racket counterparts.
-}
-
-@subsection{Maybe}
-
-@deftogether[(
-@defidform[None]
-@defthing[none None]
-@defstruct[some ([v any?]) #:omit-constructor]
-@defform[(Some type)]
-@defform[(Maybe type)]
-)]{
-@racket[(Maybe type)] is an alias for @racket[(U None (Some type))].
-}
-
-@subsection{Either}
-
-@deftogether[(
-@defstruct[left ([v any?]) #:omit-constructor]
-@defform[(Left type)]
-@defstruct[right ([v any?]) #:omit-constructor]
-@defform[(Right type)]
-@defform[(Either left-type right-type)]
-)]{
-@racket[(Either left-type right-type)] is an alias for @racket[(U (Left
-left-type) (Right right-type))].
-}
-
-@defthing[partition/either (∀ (X Y Z) (→fn (List X) (→fn X (Either Y Z)) (Tuple (List Y) (List Z))))]{
-Partition a list based on a function that returns an @racket[Either] value.
-}
-
-@section{Behavioral Checking}

racket/typed/sequence.rkt

@@ -17,15 +17,12 @@
          sequence-add-between
          in-list
          in-set
-         in-hash-keys
-         in-hash-values
          in-range
          )
 
 (require "core-types.rkt")
 (require (only-in "list.rkt" List))
 (require (only-in "set.rkt" Set))
-(require (only-in "hash.rkt" Hash))
 (require (only-in "prim.rkt" Int Bool))
 #;(require (postfix-in - racket/sequence))
 
@@ -53,8 +50,25 @@
 
 (require/typed racket/base
   [in-list : (∀ (X) (→fn (List X) (Sequence X)))]
-  [in-hash-keys : (∀ (K V) (→fn (Hash K V) (Sequence K)))]
-  [in-hash-values : (∀ (K V) (→fn (Hash K V) (Sequence V)))]
   [in-range : (→fn Int (Sequence Int))])
 (require/typed racket/set
   [in-set : (∀ (X) (→fn (Set X) (Sequence X)))])
+
+#;(define-typed-syntax empty-sequence
+  [_ ≫
+   --------------------
+   [⊢ empty-sequence- (⇒ : (Sequence (U)))]])
+
+;; er, this is making everything a macro, as opposed to a procedure...
+;; think I ought to add polymorphous first :\
+#;(define-typed-syntax (sequence->list s) ≫
+  [⊢ s ≫ s- (⇒ : (~Sequence τ))]
+  #:fail-unless (pure? #'s-)
+  ------------------------------
+  [⊢ (sequence->list- s-) (⇒ : (List τ))])
+
+#;(define-typed-syntax (sequence-length s) ≫
+    [⊢ s ≫ s- (⇒ : (~Sequence τ))]
+    #:fail-unless (pure? #'s-)
+    ------------------------------
+    [⊢ (sequence-length- s-) (⇒ : Int)])

racket/typed/set.rkt

@@ -3,28 +3,23 @@
 (provide Set
          (for-syntax ~Set)
          set
-         ;; set-member?
-         ;; set-add
-         ;; set-remove
-         ;; set-count
+         set-member?
+         set-add
+         set-remove
+         set-count
          set-union
          set-subtract
          set-intersect
-         ;; list->set
-         ;; set->list
-         (typed-out [[set-first- : (∀ (X) (→fn (Set X) X))] set-first]
-                    [[set-empty?- : (∀ (X) (→fn (Set X) Bool))] set-empty?]
-                    [[set-count- : (∀ (X) (→fn (Set X) Int))] set-count]
-                    [[set-add- : (∀ (X) (→fn (Set X) X (Set X)))] set-add]
-                    [[set-remove- : (∀ (X) (→fn (Set X) X (Set X)))] set-remove]
-                    [[set-member?- : (∀ (X) (→fn (Set X) X Bool))] set-member?]
-                    [[list->set- : (∀ (X) (→fn (List X) (Set X)))] list->set]
-                    [[set->list- : (∀ (X) (→fn (Set X) (List X)))] set->list]
-                    ))
+         list->set
+         set->list
+         (typed-out [[set-first- : (∀ (X) (→fn (Set X) X))]
+                     set-first]
+                    [[set-empty?- : (∀ (X) (→fn (Set X) Bool))]
+                     set-empty?]))
 
 (require "core-types.rkt")
 (require (only-in "prim.rkt" Int Bool))
-(require (only-in "list.rkt" ~List List))
+(require (only-in "list.rkt" ~List))
 
 (require (postfix-in - racket/set))
 
@@ -40,6 +35,38 @@
   ---------------
   [⊢ (#%app- set- e- ...) ⇒ (Set (U τ ...))])
 
+(define-typed-syntax (set-count e) ≫
+  [⊢ e ≫ e- ⇒ (~Set _)]
+  #:fail-unless (pure? #'e-) "expression must be pure"
+  ----------------------
+  [⊢ (#%app- set-count- e-) ⇒ Int])
+
+(define-typed-syntax (set-add st v) ≫
+  [⊢ st ≫ st- ⇒ (~Set τs)]
+  #:fail-unless (pure? #'st-) "expression must be pure"
+  [⊢ v ≫ v- ⇒ τv]
+  #:fail-unless (pure? #'v-) "expression must be pure"
+  -------------------------
+  [⊢ (#%app- set-add- st- v-) ⇒ (Set (U τs τv))])
+
+(define-typed-syntax (set-remove st v) ≫
+  [⊢ st ≫ st- ⇒ (~Set τs)]
+  #:fail-unless (pure? #'st-) "expression must be pure"
+  [⊢ v ≫ v- ⇐ τs]
+  #:fail-unless (pure? #'v-) "expression must be pure"
+  -------------------------
+  [⊢ (#%app- set-remove- st- v-) ⇒ (Set τs)])
+
+(define-typed-syntax (set-member? st v) ≫
+  [⊢ st ≫ st- ⇒ (~Set τs)]
+  #:fail-unless (pure? #'st-) "expression must be pure"
+  [⊢ v ≫ v- ⇒ τv]
+  #:fail-unless (pure? #'v-) "expression must be pure"
+  #:fail-unless (<: #'τv #'τs)
+    "type mismatch"
+  -------------------------------------
+  [⊢ (#%app- set-member?- st- v-) ⇒ Bool])
+
 (define-typed-syntax (set-union st0 st ...) ≫
   [⊢ st0 ≫ st0- ⇒ (~Set τ-st0)]
   #:fail-unless (pure? #'st0-) "expression must be pure"
@@ -64,3 +91,15 @@
   #:fail-unless (all-pure? #'(st- ...)) "expressions must be pure"
   -------------------------------------
   [⊢ (#%app- set-subtract- st0- st- ...) ⇒ (Set τ-st0)])
+
+(define-typed-syntax (list->set l) ≫
+  [⊢ l ≫ l- ⇒ (~List τ)]
+  #:fail-unless (pure? #'l-) "expression must be pure"
+  -----------------------
+  [⊢ (#%app- list->set- l-) ⇒ (Set τ)])
+
+(define-typed-syntax (set->list s) ≫
+  [⊢ s ≫ s- ⇒ (~Set τ)]
+  #:fail-unless (pure? #'s-) "expression must be pure"
+  -----------------------
+  [⊢ (#%app- set->list- s-) ⇒ (List τ)])

racket/typed/spin-prelude.pml

@@ -4,7 +4,6 @@
 #define RETRACTED(x) (x##_assertions == 0)
 #define ASSERT(x) x##_assertions = x##_assertions + 1
 #define RETRACT(x) x##_assertions = x##_assertions - 1
-#define SEND(x) x##_messages = x##_messages + 1
 
 /* Rest of Program */
 

racket/typed/syndicate/drivers/timestate.rkt

@@ -1,22 +0,0 @@
-#lang typed/syndicate/roles
-
-(provide activate!
-         later-than
-         LaterThanT
-         LaterThan
-         TimeStateDriver)
-
-(require-struct later-than
-                #:as LaterThanT
-                #:from syndicate/drivers/timestate)
-
-(define-type-alias LaterThan (LaterThanT Int))
-
-(define-type-alias TimeStateDriver
-  (U LaterThan
-     (Observe (LaterThanT ★/t))))
-
-;; TODO ignoring other driver underneath it
-
-(require/typed (submod syndicate/drivers/timestate syndicate-main)
-  [activate! : (proc → ⊥ #:spawns ((Actor TimeStateDriver)))])

racket/typed/syndicate/lang/reader.rkt

@@ -1,2 +1,2 @@
 #lang s-exp syntax/module-reader
-typed/syndicate/roles
+typed/main

racket/typed/syndicate/replay-trail.sh

@@ -1,3 +0,0 @@
-#!/bin/sh
-
-spin -p -t $1

racket/typed/syndicate/roles/lang/reader.rkt

@@ -1,2 +1,2 @@
 #lang s-exp syntax/module-reader
-typed/syndicate/roles
+typed/roles

racket/typed/syndicate/run-spin.sh

@@ -1,12 +0,0 @@
-#!/bin/sh
-
-pushd ${1%/*}/
-
-EXE="$1-verifier.o"
-
-spin -a $1
-gcc -o $EXE pan.c
-$EXE -a -f -n -N $2
-rm $EXE pan.c
-
-popd

racket/typed/syntax-serializer.rkt

@@ -13,6 +13,11 @@
 ;(require racket/pretty)
 
 (define (serialize-syntax stx)
+  (displayln 'serialize)
+  ;(print-syntax-width +inf.0)
+  ;(println stx)
+  ;(pretty-print (syntax->datum stx))
+
   (define unique-tag (gensym))
   (define table (hasheq))
   (define dedup-table (hasheq))
@@ -63,9 +68,16 @@
   (define top-s (serialize-element! stx))
   (define res (datum->syntax #f (serialized-syntax unique-tag table top-s)))
 
+  ;(displayln 'serialize-out)
+  ;(println res)
+  ;(pretty-print (syntax->datum res))
   res)
 
 (define (deserialize-syntax ser)
+  (displayln 'deserialize)
+  ;(print-syntax-width +inf.0)
+  ;(println ser)
+  ;(pretty-print (syntax->datum ser))
   (match (syntax-e ser)
     [(serialized-syntax unique-tag-stx table-stx contents)
      (define unique-tag (syntax-e unique-tag-stx))
@@ -119,6 +131,9 @@
              syntax-e))))
 
      (define res (deserialize-element contents))
+     ;(displayln 'deserialize-out)
+     ;(println res)
+     ;(pretty-print (syntax->datum res))
      res]))
    
 (module+ test

racket/typed/tests/basic-bad-assertion.rkt

@@ -1,4 +1,4 @@
-#lang typed/syndicate
+#lang typed/syndicate/roles
 
 (require rackunit/turnstile)
 

racket/typed/tests/comm-ty-composition.rkt

@@ -1,26 +0,0 @@
-#lang typed/syndicate
-
-(assertion-struct ping : Ping (v))
-(assertion-struct pong : Pong (v))
-
-(assertion-struct flip : Flip (v))
-(assertion-struct flop : Flop (v))
-
-(define-type-alias Pinger (Ping Int))
-(define-type-alias Ponger (U (Ping Int)
-                             (Pong Int)
-                             (Observe (Ping ★/t))))
-(define-type-alias PingPong (U Pinger Ponger))
-
-(define-type-alias Flipper (Flip Int))
-(define-type-alias Flopper (U (Flip Int)
-                              (Flop Int)
-                              (Observe (Flip ★/t))))
-(define-type-alias FlipFlop (U Flipper Flopper))
-
-(run-ground-dataspace (U PingPong FlipFlop)
-  (spawn Pinger (start-facet _ (assert (ping 5))))
-  (spawn Ponger (start-facet _ (during (ping $v) (assert (pong v)))))
-
-  (spawn Flipper (start-facet _ (assert (flip 8))))
-  (spawn Flopper (start-facet _ (during (flip $v) (assert (flop v))))))

racket/typed/tests/define-dataflow.rkt

@@ -1,4 +1,4 @@
-#lang typed/syndicate
+#lang typed/syndicate/roles
 
 (run-ground-dataspace (U)
 (spawn (U)

racket/typed/tests/effect-polymorhpism.rkt

@@ -1,4 +1,4 @@
-#lang typed/syndicate
+#lang typed/syndicate/roles
 
 (require rackunit/turnstile)
 

racket/typed/tests/expressions.rkt

@@ -1,4 +1,4 @@
-#lang typed/syndicate
+#lang typed/syndicate/roles
 
 (require rackunit/turnstile)
 

racket/typed/tests/floating-define.rkt

@@ -1,4 +1,4 @@
-#lang typed/syndicate
+#lang typed/syndicate/roles
 
 (require rackunit/turnstile)
 

racket/typed/tests/for-loop-regression.rkt

@@ -1,4 +1,4 @@
-#lang typed/syndicate
+#lang typed/syndicate/roles
 
 (require rackunit/turnstile)
 

racket/typed/tests/for-loops.rkt

@@ -1,4 +1,4 @@
-#lang typed/syndicate
+#lang typed/syndicate/roles
 
 (require rackunit/turnstile)
 

racket/typed/tests/hashes.rkt

@@ -1,4 +1,4 @@
-#lang typed/syndicate
+#lang typed/syndicate/roles
 
 (require rackunit/turnstile)
 

racket/typed/tests/inference.rkt

@@ -1,4 +1,4 @@
-#lang typed/syndicate
+#lang typed/syndicate/roles
 
 (require rackunit/turnstile)
 

racket/typed/tests/overly-broad-interests.rkt

@@ -1,22 +0,0 @@
-#lang typed/syndicate
-
-(require rackunit/turnstile)
-
-(typecheck-fail (spawn ⊥
-                       (start-facet x
-                                    (on (asserted $x:Int)
-                                        #f)))
-                #:with-msg "overly broad interest")
-
-(typecheck-fail (spawn ⊥
-                       (start-facet x
-                                    (on (asserted (observe $x:Int))
-                                        #f)))
-                #:with-msg "overly broad interest")
-
-;; TODO - but this one seems fine?
-(typecheck-fail (spawn ⊥
-                 (start-facet x
-                              (on (asserted _)
-                                  #f)))
-                #:with-msg "overly broad interest")

racket/typed/tests/pattern-annotations.rkt

@@ -1,4 +1,4 @@
-#lang typed/syndicate
+#lang typed/syndicate/roles
 
 (require rackunit/turnstile)
 

racket/typed/tests/phantom-rho.rkt

@@ -1,4 +1,4 @@
-#lang typed/syndicate
+#lang typed/syndicate/roles
 
 (require rackunit/turnstile)
 

racket/typed/tests/primitives.rkt

@@ -1,4 +1,4 @@
-#lang typed/syndicate
+#lang typed/syndicate/roles
 
 (require rackunit/turnstile)
 

racket/typed/tests/regression-count-new-words.rkt

@@ -1,4 +1,4 @@
-#lang typed/syndicate
+#lang typed/syndicate/roles
 
 (require rackunit/turnstile)
 

racket/typed/tests/regression-define-with-effects.rkt

@@ -1,4 +1,4 @@
-#lang typed/syndicate
+#lang typed/syndicate/roles
 
 (require rackunit/turnstile)
 

racket/typed/tests/sequences.rkt

@@ -1,4 +1,4 @@
-#lang typed/syndicate
+#lang typed/syndicate/roles
 
 (require rackunit/turnstile)
 

racket/typed/tests/sets.rkt

@@ -1,4 +1,4 @@
-#lang typed/syndicate
+#lang typed/syndicate/roles
 
 (require rackunit/turnstile)
 

racket/typed/tests/spawn.rkt

@@ -1,4 +1,4 @@
-#lang typed/syndicate
+#lang typed/syndicate/roles
 
 (require rackunit/turnstile)
 
@@ -15,7 +15,7 @@
         (start-facet _
                      (on (asserted (tuple $x:Int))
                          (add1 x))))
- #:with-msg "spawn: Not prepared to handle inputs:\n\\(Tuple String\\)")
+ #:with-msg "spawn: Not prepared to handle inputs:\n\\(Tuple- String\\)")
 
 (check-type
  (spawn (U)
@@ -32,4 +32,4 @@
                      (know (tuple "hi"))
                      (on (know (tuple $x:Int))
                          (add1 x))))
- #:with-msg "spawn: Not prepared to handle internal events:\n\\(Tuple String\\)")
+ #:with-msg "spawn: Not prepared to handle internal events:\n\\(Tuple- String\\)")

racket/typed/tmp.rkt

@@ -0,0 +1,163 @@
+#lang typed/syndicate/roles
+
+#;(require "core-types.rkt")
+#;(require "core-expressions.rkt")
+#;(require "prim.rkt")
+#;(require "for-loops.rkt")
+#;(require "list.rkt")
+#;(require "roles.rkt")
+#;(require "maybe.rkt")
+
+#;(require macro-debugger/stepper)
+
+;; (define-type-alias ID Symbol)
+;; (require-struct task #:as Task #:from "examples/roles/flink-support.rkt")
+;; (require-struct map-work #:as MapWork #:from "examples/roles/flink-support.rkt")
+;; (require-struct reduce-work #:as ReduceWork #:from "examples/roles/flink-support.rkt")
+;; (define-type-alias TaskID (Tuple Int ID))
+;; (define-type-alias WordCount (Hash String Int))
+;; (define-type-alias TaskResult WordCount)
+;; (define-type-alias Reduce
+;;   (ReduceWork (Either Int TaskResult)
+;;               (Either Int TaskResult)))
+;; (define-type-alias Work
+;;   (U Reduce (MapWork String)))
+;; (define-type-alias ConcreteWork
+;;   (U (ReduceWork TaskResult TaskResult)
+;;      (MapWork String)))
+;; (define-type-alias PendingTask
+;;   (Task TaskID Work))
+;; (define-type-alias ConcreteTask
+;;   (Task TaskID ConcreteWork))
+
+#;(define (task-ready? [t : PendingTask] -> (Maybe ConcreteTask))
+  (match t
+    #;[(tuple $tid)
+     ;; having to re-produce this is directly bc of no occurrence typing
+     (some (task tid (map-work s)))]
+    #;[(task $tid (reduce-work (right $v1)
+                             (right $v2)))
+     (some (task tid (reduce-work v1 v2)))]
+    [_
+     none]))
+
+#;(cons (lambda () 0) (ann (list) (List (→fn Int))))
+
+#;(Λ (X) (lambda ([x (Maybe X)]) (match x [none #f])))
+#;(lambda ([x Int]) (match x [none #f]))
+#;(match 1 [none #f])
+#;(if #t 1 none)
+#;none
+
+#;(define (∀ (X) (unwrap! [x : (Maybe X)] -> Bool))
+  #;(error "")
+  (match x
+    #;[(some (bind v X))
+     v]
+    [none
+     #f
+     #;(error "none")]))
+
+#;(lambda ([tasks : (List (Maybe Int))])
+  (define part (inst partition/either (Maybe Int) Int Int))
+  (part tasks
+        (lambda ([t : (Maybe Int)])
+          (left 0)
+          #;(match t
+            [(some $ct)
+             (right ct)]
+            [none
+             (left 0)]))))
+
+#;(define (debug [tasks : (List Int)] -> (Tuple (List String) (List Int)))
+  (define part (inst partition/either Int String Int))
+  (part tasks
+        (lambda ([t : Int])
+          (left "hi"))))
+
+(define (partition-ready-tasks [tasks : (List Int)]
+                               -> (Tuple (List Int)
+                                         (List Int)))
+  (define part (inst partition/either Int Int Int))
+  (part tasks
+        (lambda ([t : Int])
+          (right 0)
+          #;(match (some 5)
+              [(some $ct)
+               (right ct)]
+              [none
+               (left 0)]))))
+
+
+#;(define id : (∀ (X) (→fn X (List X) (List X)))
+  (Λ (X) (lambda ([x X] [y (List X)]) (list x))))
+
+#;(spawn (U)
+         (start-facet echo
+                      (on (message (tuple 1 1))
+                          #f)))
+
+#;(for/fold ([acc Int 0])
+          ([x (list 1)])
+  x)
+
+#;(define-constructor* (left : Left v))
+
+#;(define (f [x (Left Int)] -> Int)
+    (define y x)
+    (match y
+    [(left (bind z Int))
+     z]))
+
+#;(#%app- expand/step #'(lambda ([x : Int])
+    (define y x)
+    y))
+
+#;(lambda ([x : Int])
+    (define y x)
+    y)
+#;(begin-for-syntax
+  (define t #'(Maybe Unit))
+  (define t- ((current-type-eval) t))
+  (values #;displayln ((current-type?) t-))
+  (define tt (syntax-parse (detach t- ':)
+               [(#%plain-app x) #'x]))
+  (pretty-print (syntax-debug-info tt)))
+
+#;(begin-for-syntax
+    (define t #'PendingTask)
+    (define t- ((current-type-eval) t))
+    (displayln ((current-type?) t-))
+    )
+
+#;(define t1 '(→ (Computation (Value ★/t)
+                (Endpoints)
+                (Roles (Branch (Effs (Realizes (TasksFinished- Symbol (Hash- String Int))))
+                               (Effs (Branch (Effs (Realizes (TaskIsReady- Symbol (Task- (Tuple- Int Symbol) (U* (MapWork- String) (ReduceWork- (Hash- String Int) (Hash- String Int)))))))
+                                             (Effs)))))
+                (Spawns))
+   (Tuple- Int Symbol)
+   (Hash- String Int)))
+
+#;(define t2 '(→ (Computation (Value ★/t)
+                (Endpoints)
+                (Roles (Branch (Effs (Realizes (TasksFinished- Symbol (Hash- String Int))))
+                               (Effs (Branch (Effs (Realizes (TaskIsReady- Symbol (Task- (Tuple- Int Symbol) (U* (MapWork- String) (ReduceWork- (Hash- String Int) (Hash- String Int)))))))
+                                             (Effs)))))
+                (Spawns))
+   (Tuple- Int Symbol)
+   (Hash- String Int)))
+
+#;(lambda ()
+  (role-strings
+  (start-facet x
+    (define (push-results)
+      (cond
+        [(zero? 0)
+         (start-facet done (assert #t))]
+        [else
+         #f]))
+    (define (∀ (ρ) (perform-task [k : (proc -> ★/t #:roles (ρ))]))
+      (start-facet perform
+                   (on start (stop perform (k)))))
+    (on start (call/inst perform-task push-results)))))