floating define test

edit info files to enable raco test typed/

racket/info.rkt

@@ -1,38 +1,30 @@
 #lang setup/infotab
 (define collection 'multi)
-(define deps '(
+(define deps '("rfc6455"
+               "turnstile-lib"
+               "turnstile-example"
+               "macrotypes-lib"
+               "rackunit-macrotypes-lib"
 	       "base"
 	       "data-lib"
-	       "htdp-lib"
 	       "net-lib"
+               "web-server-lib"
 	       "profile-lib"
 	       "rackunit-lib"
-	       "sha"
-               "automata"
-               "auxiliary-macro-context"
+	       "htdp-lib"
                "data-enumerate-lib"
                "datalog"
-               "db-lib"
                "draw-lib"
                "gui-lib"
-               "images-lib"
-               "macrotypes-lib"
                "pict-lib"
-               "rackunit-macrotypes-lib"
-               "rfc6455"
-               "sandbox-lib"
                "sgl"
                "struct-defaults"
-               "turnstile-example"
-               "turnstile-lib"
-               "web-server-lib"
-               ))
-(define build-deps '(
-                     "draw-doc"
-                     "gui-doc"
-                     "htdp-doc"
-                     "pict-doc"
-                     "racket-doc"
+               "auxiliary-macro-context"
+               "sandbox-lib"
+               "images-lib"
+               "automata"
+	       "sha"))
+(define build-deps '("racket-doc"
                      "scribble-lib"
                      "sha"
-                     ))
+                     "draw-doc" "gui-doc" "htdp-doc" "pict-doc"))

racket/syndicate-gui-toolbox/info.rkt

@@ -2,7 +2,3 @@
 
 (define compile-omit-paths
   '("examples"))
-
-(define test-omit-paths
-  '(;; depends on Matthias's 7GUI project which is not on the package server
-    "examples"))

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/info.rkt

@@ -3,8 +3,3 @@
 (define racket-launcher-names '("syndicate-broker" "syndicate-render-msd"))
 (define racket-launcher-libraries '("broker/server.rkt" "trace/render-msd.rkt"))
 (define test-include-paths '("syndicate/tests"))
-(define test-omit-paths
-  '(;; Sam: example-plain is interactive, I think
-    "examples/example-plain.rkt"
-    ;; Sam: for whatever reason I get a failure to load libcrypto for f-to-c
-    "examples/actor/f-to-c.rkt"))

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/scribblings/syndicate.scrbl

@@ -3,578 +3,27 @@
 @(require (for-label (except-in racket process field)
             syndicate/actor))
 
-@title{Dataspace Programming with Syndicate}
+@title{High Level Syntax for Syndicate}
 
 
 @defmodule[syndicate/actor]
 
-@section{Overview}
+@section{Instantaneous Actions (I)}
 
-Syndicate is an actor language where all communication occurs through a tightly
-controlled shared memory, dubbed the @emph{dataspace}. The values in the
-dataspace are called @emph{assertions}, representing the information that the
-actors in the system are currently sharing with each other. Assertions are
-@emph{read-only} and @emph{owned} by the actor that entered them into the
-dataspace. Only the originating actor has permission to withdraw an assertion.
-Assertions are linked to the lifetime of their actor, and are withdrawn from the
-dataspace when that actor exits, either normally or via exception.
+@defform[(spawn I ...)]{
+Spawns an actor that executes each instantaneous action @racket[I] in
+sequence.}
 
-To respond to assertions in the dataspace, an actor expresses an @emph{interest}
-in the shape of assertions it wishes to receive. An interest is an assertion
-constructed with @racket[observe] and wildcards where the actor wishes to
-receive any matching assertion. When an actor makes an assertion of interest,
-the dataspace dispatches the set of all matching assertions to that actor.
-Moreover, the dataspace keeps the actor @emph{up-to-date}, informing it when a
-new assertion appears matching its interest, as well as when a matching
-assertion disappears from the dataspace. Thus, dataspaces implement a form of
-publish/subscribe communication.
+@defform[(dataspace I ...)]{
+Spawns a dataspace as a child of the dataspace enclosing the executing actor. The
+new dataspace executes each instantaneous action @racket[I].}
 
-@;{would be nice to link pub/sub}
-
-In addition to assertions, dataspaces support instantaneous @racket[message]
-broadcast. At the time a message is sent, all actors with a matching interest
-receive notification.
-
-In response to an event, that is, a message broadcast or assertion
-appearance/disappearance matching an expressed interest, a Syndicate actor may
-take any of the following actions:
-@itemlist[
-  @item{Updating its internal state;}
-  @item{Making or withdrawing assertions;}
-  @item{Sending broadcast messages;}
-  @item{Spawning additional actors;}
-  @item{Exiting;}
-  @item{Or any combination of these.}
-]
-
-Thus, each individual Syndicate actor has three fudamental concerns:
-
-@itemlist[
-  @item{Defining local state and updating it in response to events;}
-  @item{Publishing aspects of local state/knowledge as assertions; and}
-  @item{Reacting to relevant assertions and messages.}
-]
-
-Each concern is addressed by a separate language construct, which are
-collectively dubbed @emph{endpoints}:
-
-@itemlist[
-  @item{The @racket[field]s of an actor hold its state;}
-  @item{An actor publishes information using @racket[assert]; and}
-  @item{An event-handler endpoint uses @racket[on] to define reactions to
-  particular messages and assertions.}
-]
-
-Endpoints are tied together via @emph{dataflow}. Thus, the assertions of an
-actor automatically reflect the current value of its fields.
-
-Implementing an actor's role in a particular conversation typically involves
-some combination of these behaviors; a @emph{facet} is a collection of related
-endpoints constituting the actor's participation in a particular conversation.
-
-Each actor starts with a single facet, and may add new facets or terminate
-current ones in response to events. The facets of an actor form a tree, where
-the parent of a particular facet is the facet in which it was created. The tree
-structure affects facet shutdown; terminating a facet also terminates all of its
-descendants.
-
-To recap: an actor is a tree of facets, each of which comprises of a collection
-of endpoints.
-
-@section{Programming Syndicate Actors with Facets}
-
-Code within Syndicate actors executes in one of two contexts:
-@itemlist[
-  @item{The @emph{endpoint-installation} context occurs during the creation of a
-  new facet, when all of its endpoints are created.}
-  @item{The @emph{script} context occurs during the execution of event handlers,
-  and permits creating/terminating facets, sending messages, and spawning
-  actors.}
-]
-
-The actions permitted by the two contexts are mutually exclusive, and trying to
-perform an action in the wrong context will give rise to a run-time
-@racket[error].
-
-Within the following descriptions, we use @emph{EI} as a shorthand for
-expressions that execute in an endpoint-installation context and @emph{S} for
-expressions in a script context.
-
-@subsection{Script Actions: Starting and Stopping Actors and Facets}
-
-@defform[(spawn maybe-name
-                maybe-assertions
-                maybe-linkage
-                EI ...+)
-         #:grammar
-         [(maybe-name (code:line)
-                      (code:line #:name name-expr))
-          (maybe-assertions (code:line)
-                            (code:line #:assertions assertion-expr)
-                            (code:line #:assertions* assertions-expr))
-          (maybe-linkage (code:line)
-                         (code:line #:linkage [linkage-expr ...]))]
-         #:contracts
-         ([assertion-expr any/c]
-          [assertions-expr trie?])]{
-Spawn an actor with a single inital facet whose endpoints are installed by
-@racket[EI]. That is, there is an implicit @racket[react] around @racket[EI
-...]. Allowed within a script and module-top-level.
-
-An optionally provided @racket[name-expr] is associated with the created actor.
-The name is only used for error and log messages, thus is mainly useful for
-debugging.
-
-The actor may optionally be given some initial assertions, which come into being
-at the same time as the actor. (Otherwise, the actor spawns, then boots its
-initial facet(s), then establishes any ensuing assertions.) When
-@racket[assertion-expr] is provided, the actors initial assertions are the
-result of interpreting the expression as a @racket[trie] pattern, with
-@racket[?] giving rise to infinte sets. On the other hand,
-@racket[assertions-expr] may be used to specify an entire set of initial
-assertions as an arbitrary @racket[trie].
-
-The optional @racket[linkage-expr]s are executed during facet startup; your
-simple documentation author is not sure why they are useful, as opposed to just
-putting them in the body of the @racket[spawn].
-}
-
-@defform[(react EI ...+)]{
-Create a new facet in the current actor whose endpoints are the result of
-executing @racket[EI ...]. Allowed within a script.
-}
-
-@defform[(stop-facet fid S ...)
-         #:contracts ([fid facet-id?])]{
-Terminate the facet with ID @racket[fid], as well as all of its children.
-Allowed within a script.
-
-The optional script actions @racket[S ...] function like a continuation. They
-run @emph{after} the facet and all of its children finish shutting down, i.e.
-after all @racket[stop] handlers have executed. Moreover, @racket[S ...] runs in
-the context of the @emph{parent} of @racket[fid]. Thus, any facet created by the
-script survives termination and will have @racket[fid]'s parent as its own
-parent.
-
-Note that @racket[fid] must be an ancestor of the current facet.
-}
-
-@defform[(stop-current-facet S ...)]{
-Stop the currently running facet; equivalent to
-@racketblock[(stop-facet (current-facet-id) S ...)].
-
-Allowed within a script.
-}
-
-@defproc[(current-facet-id) facet-id?]{
-Retrieves the ID of the currently running facet.
-}
-
-@defproc[(send! [v any/c])
+@defproc[(send! [v any/c]
+                [#:meta-level level natural-number/c 0])
          void?]{
-Sends a @racket[message] with body @racket[v].
-
-Allowed within a script.
-}
-
-@subsection{Installing Endpoints}
-
-@defform[(field [x init-expr maybe-contract] ...+)
-         #:grammar
-         [(maybe-contract (code:line)
-                          (code:line #:contract in)
-                          (code:line #:contract in out))]]{
-Define fields for the current facet. Each @racket[x] is bound to a handle
-function: calling @racket[(x)] retrieves the current value, while @racket[(x v)]
-sets the field to @racket[v].
-
-Fields may optionally have a contract; the @racket[in] contract is applied when
-writing to a field, while the (optional) @racket[out] contract applies when
-reading a value from a field.
-
-Allowed within an endpoint installation context.
-}
-
-@defform[(assert maybe-pred exp)
-         #:grammar
-         [(maybe-pred (code:line)
-                      (code:line #:when pred))]
-         #:contracts ([pred boolean?])]{
-Make the assertion @racket[exp] while the enclosing facet is active. Publishing
-the assertion can be made conditional on a boolean expression by supplying a
-@racket[#:when] predicate, in which case the assertion is made only when
-@racket[pred] evaluates to a truthy value.
-
-If the expression @racket[exp] refers to any fields, then the assertion created
-by the endpoint is automatically kept up-to-date each time any of those fields
-is updated. More specifically, the will issue a patch retracting the assertion
-of the previous value, replacing it with the results of reevaluating
-@racket[exp] with the current values of each field.
-
-Allowed within an endpoint installation context.
-}
-
-@defform[#:literals (message asserted retracted _ $ ?)
-         (on maybe-pred event-description
-             S ...+)
-         
-         #:grammar
-         [(maybe-pred (code:line)
-                      (code:line #:when pred))
-          (event-description (code:line (message pattern))
-                             (code:line (asserted pattern))
-                             (code:line (retracted pattern)))
-          (pattern (code:line _)
-                   (code:line $id)
-                   (code:line ($ id pattern))
-                   (code:line (? pred pattern))
-                   (code:line (ctor pattern ...))
-                   (code:line expr))]
-         #:contracts ([pred boolean?])]{
-Creates an event handler endpoint that responds to the event specified by
-@racket[event-description]. Executes the body @racket[S ...] for each matching
-event, with any pattern variables bound to their matched value.
-
-The actor will make an assertion of interest in events that could match
-@racket[event-description]. Like with @racket[assert], the interest will be
-refreshed any time a field referenced within the @racket[event-description]
-pattern changes.
-
-The event handler can optionally be made conditional on a boolean expression by
-supplying a @racket[#:when] predicate, in which case the endpoint only reacts to
-events, and only expresses the corresponding assertion of interest, when
-@racket[pred] evaluates to a truthy value.
-
-Allowed within an endpoint installation context.
-
-Event descriptions have one of the following forms:
-@itemlist[
-  @item{@racket[(message pattern)] activates when a message is received with a
-    body matching @racket[pat].}
-
-  @item{@racket[(asserted pattern)] activates when a patch is received with an
-    added assertion matching @racket[pattern]. Additionally, if the actor has
-    @emph{already} received a patch with matching assertions, which can occur if
-    multiple facets in a single actor have overlapping interests, then the
-    endpoint will match those assertions upon facet start up.}
-
-  @item{@racket[(retracted pat)] is similar to @racket[asserted], but for
-    assertions withdrawn in a patch.}
-
-  @;{@item{@racket[(rising-edge expr)] activates when @racket[expr] evaluates to
-    anything besides @racket[#f] (having previously evaluated to @racket[#f]). The
-    condition is checked after each received event.}}
-]
-
-While patterns have the following meanings:
-@itemlist[
-  @item{@racket[_] matches anything.}
-
-  @item{@racket[$id] matches anything and binds the value to @racket[id].}
-
-  @item{@racket[($ id pattern)] matches values that match @racket[pattern] and
-    binds the value to @racket[id].}
-
-  @item{@racket[(? pred pattern)] matches values where @racket[(pred val)] is not
-     @racket[#f] and that match @racket[pattern].}
-
-  @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[(during pattern EI ...+)]{
-Engage in behavior for the duration of a matching assertion. Roughly equivalent
-to:
-
-@racketblock[
-(on (asserted pattern)
-  (react
-    EI ...
-    (on (retracted inst-pattern)
-        (stop-current-facet))))]
-
-where @racket[inst-pattern] is the @racket[pattern] with variables instantiated
-to their matching values.
-
-Allowed within an endpoint installation context.
-}
-
-@defform[(during/spawn pattern
-                        maybe-actor-wrapper
-                        maybe-name
-                        maybe-assertions
-                        maybe-parent-let
-                        maybe-on-crash
-                        EI ...)
-          #:grammar
-          [(maybe-actor-wrapper (code:line)
-                                (code:line #:spawn wrapper-stx))
-           (maybe-parent-let (code:line)
-                             (code:line #:let [x expr] ...))
-           (maybe-on-crash (code:line)
-                           (code:line #:on-crash on-crash-expr))]]{
-Like @racket[during], but in addition to creating a new facet for each matching
-assertion, @racket[spawn]s a new actor. The difference is primarily relevant for
-error propagation; an exception inside @racket[during] causes the entire actor
-to crash, while an exception inside @racket[during/spawn] crashes only the newly
-spawned actor.
-
-The assertion triggering the @racket[during/spawn] may disappear @emph{before}
-the spawned actor boots, in which case it fails to see the retraction event. To
-avoid potential glitches, the @emph{spawning} actor maintains an assertion that
-lets the @racket[spawned] actor know whether the originial assertion still
-exists.
-
-The @racket[maybe-name] and @racket[maybe-assertions] have the same meaning they
-do for @racket[spawn], applied to the newly spawned actor.
-
-The @racket[wrapper-stx] serves as an interposition point; it may be provided to
-change the meaning of "spawning an actor" in response to an assertion. By
-default, it is @racket[#'spawn].
-
-The optional @racket[#:let] clauses can be used to read the values of fields in
-the @emph{spawning} actor so that they can be used in the @emph{spawned} actor.
-Otherwise, the spawned actor has no access to the parent's fields, and trying to
-read or write to such a field will cause a runtime @racket[error].
-
-The @racket[on-crash-expr] provides a hook for script actions that can be
-performed in the @emph{spawning} actor if the @emph{spawned} actor crashes.
-
-Allowed within an endpoint installation context.
-}
-
-@defform[(stop-when maybe-pred event-description S ...)
-         #:grammar
-         [(maybe-pred (code:line)
-                      (code:line #:when pred))]
-         #:contracts ([pred boolean?])]{
-Stop the current facet when an event matching @racket[event-description] occurs.
-Roughly equivalent to
-@racketblock[
-(on event-description
-    (stop-current-facet S ...))]
-
-Allowed within an endpoint installation context.
-}
-
-@subsection{Handling Facet Startup and Shutdown}
-
-In addition to external events, such as assertion (dis)appearance and message
-broadcast, facets can react to their own startup and shutdown. This provides a
-handy way to perform initialization, cleanup, as well as setting up and tearing
-down resources.
-
-@defform[(on-start S ...)]{
-Perform the script actions @racket[S ...] upon facet startup.
-
-Allowed within an endpoint installation context.
-}
-
-@defform[(on-stop S ...)]{
-Perform the script actions @racket[S ...] upon facet shutdown.
-
-The script @racket[S ...] differs from that of @racket[stop-facet] in that it
-executes in the context of the terminating facet, not its parent. Thus, any
-facets created in @racket[S ...] will start up and then immediately shut down.
-
-Allowed within an endpoint installation context.
-}
-
-Note that a single facet may have any number of @racket[on-start] and
-@racket[on-stop] handlers, which do not compete with each other. That is, each
-@racket[on-start] handler runs during facet startup and, likewise, each
-@racket[on-stop] during facet shutdown.
-
-@subsection{Streaming Query Fields}
-
-Syndicate actors often aggregate information about current assertions as part of
-their local state, that is, in a @racket[field]. Since these patterns are
-exceedingly common, Syndicate provides a number of forms for defining fields
-that behave as streaming queries over the assertions in the dataspace.
-
-@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))]]{
-Define a @racket[field] called @racket[name] that is the @racket[set] of values
-extracted from assertions matching @racket[pattern]. Each value is extracted
-from a matching assertion by evaluating @racket[expr], which may refer to
-variables bound by @racket[pattern].
-
-The query set expands to roughly the following code:
-@racketblock[
-(begin
-  (field [name (set)])
-  (on (asserted pattern)
-      (name (set-add (name) expr)))
-  (on (retracted pattern)
-      (name (set-remove (name) expr))))]
-    
-The optional @racket[on-add-expr] is performed inside the @racket[on asserted]
-handler, while @racket[on-remove-expr] runs in the @racket[on retracted]
-handler.
-
-Allowed within an endpoint installation context.
-}
-
-@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))]]{
-Define a @racket[field] called @racket[name] that is a @racket[hash] based on
-assertions matching @racket[pattern]. Each matching assertion establishes a key
-in the hash based on @racket[key-expr] whose value is the result of
-@racket[value-expr], with each expression referring to variables bound by
-@racket[pattern]. When a matching assertion disappears from the dataspace, the
-associated key is removed from the hash.
-
-The optional @racket[maybe-on-add] and @racket[maybe-on-expr] behave the same
-way they do for @racket[define/query-set].
-
-Allowed within an endpoint installation context.
-}
-
-@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))]]{
-Define a @racket[field] called @racket[name] whose value is based on the
-presence of an assertion matching @racket[pattern] in the dataspace. When such
-an assertion is present, the value of the @racket[name] field is the result of
-evaluating @racket[expr], which may refer to @racket[pattern]. When no such
-assertion exists, including initially, the value of @racket[name] is the result
-of @racket[absent-expr].
-
-The optional @racket[maybe-on-add] and @racket[maybe-on-expr] behave the same
-way they do for @racket[define/query-set].
-
-Allowed within an endpoint installation context.
-}
-
-@defform[(define/query-count name pattern key-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))]]{
-Define a @racket[field] called @racket[name] whose value is a @racket[hash]
-counting occurrences of matching assertions in the dataspace. More precisely,
-for each assertion @racket[pattern], evaluating @racket[key-expr] determines a
-key in the hash; the value for that key is incremented when the assertion
-appears and decremented when it disappears. When the count associated with a
-particular key falls to @racket[0], that key is removed from the hash.
-
-The optional @racket[maybe-on-add] and @racket[maybe-on-expr] behave the same
-way they do for @racket[define/query-set].
-
-Allowed within an endpoint installation context.
-}
-
-@subsection{Generalizing Dataflow}
-
-The dataflow mechanism that automatically refreshes @racket[assert] endpoints
-when a referenced field changes may be used to react to local state updates in
-arbitrary ways using @racket[begin/dataflow].
-
-@defform[(begin/dataflow S ...+)]{
-Evaluate and perform the script actions @racket[S ...] during facet startup, and
-then again each time a field referenced by the script updates.
-
-Conceptually, @racket[begin/dataflow] may be thought of as an event handler
-endpoint in the vein of @racket[on], where the event of interest is @emph{update
-of local state}.
-
-Allowed within an endpoint installation context.
-}
-
-@defform[(define/dataflow name expr maybe-default)
-         #:grammar
-         [(maybe-default (code:line)
-                         (code:line #:default default-expr))]]{
-Define a @racket[field] named @racket[name], whose value is reevaluated to the
-result of @racket[expr] each time any referenced field changes.
-
-The value of @racket[name] is either @racket[#f] or, if provided,
-@racket[default-expr]. This initial value is observable for a short time during
-facet startup.
-
-Note that when a field referenced by @racket[expr] changes, there may be some
-time before @racket[name] refreshes, during which "stale" values may be read
-from the field.
-
-Allowed within an endpoint installation context.
-}
-
-
-@subsection{Generalizing Actor-Internal Communication}
-
-Talk about internal assertions and messages.
-
-@subsection{Nesting Dataspaces}
-
-Nested dataspaces, inbound and outbound assertions, quit-datapace.
-
-@defform[(dataspace S ...)]{
-Spawns a dataspace as a child of the dataspace enclosing the executing actor.
-The new dataspace executes each action @racket[S].
-
-Allowed within a script.
-}
-
-
-@section{@hash-lang[] @racket[syndicate] Programs}
-
-In a @hash-lang[] @racket[syndicate] program, the results of top-level
-expressions define the initial group of actors in the dataspace. That is,
-evaluating @racket[spawn] or @racket[dataspace] in the context of the module
-top-level adds that actor specification to the initial dataspace of the program.
-For example, a module such as:
-
-@codeblock[#:line-numbers 0]|{
-#lang syndicate
-
-(define (spawn-fun)
-  (spawn ...))
-
-(spawn ...)
-
-(spawn-fun)
-}|
-
-launches a syndicate program with two initial actors, one the result of the
-@racket[spawn] expression on line 5 and one the result of evaluating the
-@racket[spawn] expresion on line 3 during the course of calling
-@racket[spawn-fun] on line 7.
-
-The initial dataspace is referred to as the @emph{ground} dataspace, and it
-plays a special role in Syndicate programming; see below.
-
-@section{Interacting with the Outside World}
-
-ground dataspace, drivers, etc.
-
-@section{Actors with an Agenda}
-
-Here we talk about @racket[spawn*] and @racket[react/suspend].
-
-@section{Odds and Ends}
+Sends a message with body @racket[v]. The message is sent @racket[level]
+dataspaces removed from the dataspace containing the actor performing the
+@racket[send!].}
 
 @defproc[(assert! [v any/c]
                   [#:meta-level level natural-number/c 0])
@@ -590,6 +39,8 @@ distance from the dataspace containing the enclosing actor.}
 Retracts any assertions made by the immediately enclosing actor at
 @racket[level] dataspaces above the enclosing dataspace of the form @racket[v].}
 
+@section{Ongoing Behaviors (O)}
+
 @defform[(state maybe-init (maybe-bindings O ...) ([E I ...] ...))
          #:grammar
          [(maybe-init (code:line)
@@ -651,3 +102,79 @@ termination event but before the @racket[until] actor exits.}
          #:contracts ([id identifier?])]{
 The @racket[forever] behavior is analogous to a @racket[state] form with no
 termination events.}
+
+@defform[(during pat O ...)]{
+Runs the behaviors @racket[O ...] for the duration of each assertion matching
+@racket[pat].
+
+Roughly equivalent to
+@racket[(on (asserted pat)
+            (until (retracted pat)
+                   O ...))]
+where the @racket[pat] in the @racket[until] clause is specialized to the actual
+value matched by @racket[pat] in the @racket[asserted] clause.
+}
+
+@defform[(assert maybe-pred exp maybe-level)
+         #:grammar
+         [(maybe-pred (code:line)
+                      (code:line #:when pred))
+          (maybe-level (code:line)
+                       (code:line #:meta-level level))]
+         #:contracts ([pred boolean?]
+                      [level natural-number/c])]{
+Makes the assertion @racket[exp] while the enclosing actor is running. If a
+@racket[#:when] predicate is given, the assertion is made conditionally on the
+predicate expression evaluating to true.}
+
+@defform[(on E
+             I ...)]{
+When the event @racket[E] becomes active, executes the instantaneous actions
+@racket[I ...] in the body. The result of the final action is the result of the
+entire behavior.}
+
+@section{Events (E)}
+
+@defform[(message pat)]{
+Activates when a message is received with a body matching @racket[pat].
+The message event establishes the enclosing actor's interest in @racket[pat].}
+
+@defform[(asserted pat)]{
+Activates when a patch is received with an added assertion matching
+@racket[pat]. Establishes the enclosing actor's interest in @racket[pat].}
+
+@defform[(retracted pat)]{
+Similar to @racket[asserted], except for assertions removed in a patch.}
+
+@defform[(rising-edge expr)]{
+Activates when @racket[expr] evaluates to anything besides @racket[#f] (having
+previously evaluated to @racket[#f]). The condition is checked after each
+received event, corresponding to after each instantaneous action is executed.}
+
+@section{Patterns}
+
+@(racketgrammar
+  pat
+  (code:line)
+  (code:line _)
+  (code:line $id)
+  (code:line ($ id pat))
+  (code:line (? pred pat))
+  (code:line (ctor pat ...))
+  (code:line expr))
+
+@racket[_] matches anything.
+
+@racket[$id] matches anything and binds the value to @racket[id].
+
+@racket[($ id pat)] matches values that match @racket[pat] and binds the value
+to @racket[id].
+
+@racket[(? pred pat)] matches values where @racket[(pred val)] is not
+@racket[#f] and that match @racket[pat].
+
+@racket[(ctor pat ...)] matches values built by applying the constructor
+@racket[ctor] to values matching @racket[pat ...].
+
+@racket[expr] patterns match values that are exactly equal to @racket[expr].
+

racket/syndicate/tests/create-new-facet-in-on-stop.rkt

@@ -1,8 +1,7 @@
 #lang syndicate/test
 
-;; The facet in the on-stop should immediately die and its assertion should never be visible.
-;; Pretty sure the little implementation gets that wrong.
-;; the trace does not have a way of saying there should never be a "here" assertion
+;; Reflects the current behavior of the little implementation,
+;; but quite possibly *not* what should happen
 
 (spawn
  (on-stop (react (assert (outbound "here"))))
@@ -10,4 +9,4 @@
 
 (spawn (on-start (send! "stop")))
 
-(trace (message "stop"))
+(trace (assertion-added (outbound "here")))

racket/syndicate/tests/facet-creation-during-stop-from-grandchild.rkt

@@ -5,10 +5,6 @@
 ;; dubious behavior by little implementation;
 ;; create new facets from more nested facets
 
-;; The facet in the on-stop should immediately die and its assertion should never be visible.
-;; Pretty sure the little implementation gets that wrong.
-;; the trace does not have a way of saying there should never be an "inner" assertion
-
 (spawn (on-start
         (react (on-stop
                 (react (assert (outbound "inner"))))))
@@ -17,4 +13,4 @@
 
 (spawn (on-start (send! "stop")))
 
-(trace (message "stop"))
+(trace (assertion-added (outbound "inner")))

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

@@ -5,7 +5,5 @@ pan.c : leader-and-seller.pml
 	spin -a 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/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")
@@ -31,12 +29,12 @@
 
 (define-typed-syntax (bind x:id τ:type) ≫
   ----------------------------------------
-  [⊢ (#%app- error- 'bind "escaped") (⇒ : (Bind τ))])
+  [⊢ (error- 'bind "escaped") (⇒ : (Bind τ))])
 
 (define-typed-syntax discard
   [_ ≫
    --------------------
-   [⊢ (#%app- error- 'discard "escaped") (⇒ : Discard)]])
+   [⊢ (error- 'discard "escaped") (⇒ : Discard)]])
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Core-ish forms
@@ -86,13 +84,12 @@
   ------------------------------------
   [≻ (if e #f (let () s ...))])
 
-
 ;; copied from ext-stlc
 (define-typed-syntax let
   [(_ ([x e] ...) e_body ...) ⇐ τ_expected ≫
    [⊢ e ≫ e- ⇒ : τ_x] ...
    #:fail-unless (stx-andmap pure? #'(e- ...)) "expressions must be pure"
-   [[x ≫ x- : τ_x] ... ⊢ (block e_body ...) ≫ e_body- (⇐ : τ_expected)
+   [[x ≫ x- : τ_x] ... ⊢ (begin e_body ...) ≫ e_body- (⇐ : τ_expected)
                    (⇒ ν-ep (~effs eps ...))
                    (⇒ ν-f (~effs fs ...))
                    (⇒ ν-s (~effs ss ...))]
@@ -104,7 +101,7 @@
   [(_ ([x e] ...) e_body ...) ≫
    [⊢ e ≫ e- ⇒ : τ_x] ...
    #:fail-unless (stx-andmap pure? #'(e- ...)) "expressions must be pure"
-   [[x ≫ x- : τ_x] ... ⊢ (block e_body ...) ≫ e_body- (⇒ : τ_body)
+   [[x ≫ x- : τ_x] ... ⊢ (begin e_body ...) ≫ e_body- (⇒ : τ_body)
                    (⇒ ν-ep (~effs eps ...))
                    (⇒ ν-f (~effs fs ...))
                    (⇒ ν-s (~effs ss ...))]
@@ -118,7 +115,7 @@
 (define-typed-syntax let*
   [(_ () e_body ...) ≫
    --------
-   [≻ (block e_body ...)]]
+   [≻ (begin e_body ...)]]
   [(_ ([x e] [x_rst e_rst] ...) e_body ...) ≫
    --------
    [≻ (let ([x e]) (let* ([x_rst e_rst] ...) e_body ...))]])
@@ -126,7 +123,7 @@
 (define-typed-syntax (cond [pred:expr s ...+] ...+) ≫
   [⊢ pred ≫ pred- (⇐ : Bool)] ...
   #:fail-unless (stx-andmap pure? #'(pred- ...)) "predicates must be pure"
-  [⊢ (block s ...) ≫ s- (⇒ : τ-s)
+  [⊢ (begin s ...) ≫ s- (⇒ : τ-s)
                    (⇒ ν-ep (~effs eps ...))
                    (⇒ ν-f (~effs fs ...))
                    (⇒ ν-s (~effs ss ...))] ...
@@ -144,7 +141,7 @@
   #:with (p/e ...) (for/list ([pat (in-syntax #'(p ...))])
                      (elaborate-pattern/with-type pat #'τ-e))
   #:with (([x τ:type] ...) ...) (stx-map pat-bindings #'(p/e ...))
-  [[x ≫ x- : τ.norm] ... ⊢ (block s ...) ≫ s- (⇒ : τ-s)
+  [[x ≫ x- : τ.norm] ... ⊢ (begin s ...) ≫ s- (⇒ : τ-s)
                 (⇒ ν-ep (~effs eps ...))
                 (⇒ ν-f (~effs fs ...))
                 (⇒ ν-s (~effs ss ...))] ...
@@ -166,15 +163,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 +204,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 +259,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 +276,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 +318,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 +344,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/either.rkt

@@ -22,14 +22,13 @@
 (define (∀ (X Y Z) (partition/either [xs : (List X)]
                                      [pred : (→fn X (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/lorem.txt

@@ -1,48 +0,0 @@
-Lorem ipsum dolor sit amet, consectetur adipiscing elit. Nullam vehicula
-accumsan tristique. Integer sit amet sem metus. Nam porta tempus nisl ac
-ullamcorper. Nulla interdum ante ut odio ultricies lobortis. Nam sollicitudin
-lorem quis pellentesque consequat. Aenean pulvinar diam sed nulla semper, eget
-varius tortor faucibus. Nam sodales mattis elit, ac convallis sem pretium sed.
-Aliquam nibh velit, facilisis sit amet aliquam quis, dapibus vel mauris. Cras
-pharetra arcu tortor, id pharetra massa aliquet non. Maecenas elit libero,
-malesuada nec enim ut, ornare sagittis lectus. Praesent bibendum sed magna id
-euismod. Maecenas vulputate nunc mauris, a dignissim magna volutpat consectetur.
-Fusce malesuada neque sapien, sit amet ultricies urna finibus non. Fusce
-ultrices ipsum vel ligula eleifend, eget eleifend magna interdum. Curabitur
-semper quam nunc, sed laoreet ipsum facilisis at. Etiam ut quam ac eros
-ullamcorper mattis eget vel leo.
-
-Integer ac ipsum augue. Ut molestie ac mi vel varius. Praesent at est et nulla
-facilisis viverra sit amet eu augue. Nullam diam odio, elementum vehicula
-convallis id, hendrerit non magna. Suspendisse porta faucibus feugiat. In
-rhoncus semper diam eu malesuada. Suspendisse ligula metus, rhoncus eget nunc
-et, cursus rutrum sem. Fusce iaculis commodo magna, vitae viverra arcu. Fusce et
-eros et massa sollicitudin bibendum. Etiam convallis, nibh accumsan porttitor
-sollicitudin, mauris orci consectetur nisl, sit amet venenatis nulla enim eget
-risus. Phasellus quam diam, commodo in sodales eget, scelerisque sed odio. Sed
-aliquam massa vel efficitur volutpat. Mauris ut elit dictum, euismod turpis in,
-feugiat lectus.
-
-Vestibulum leo est, feugiat sit amet metus nec, ullamcorper commodo purus. Sed
-non mauris non tellus ullamcorper congue interdum et mauris. Donec sit amet
-mauris urna. Sed in enim nisi. Praesent accumsan sagittis euismod. Donec vel
-nisl turpis. Ut non efficitur erat. Vestibulum quis fermentum elit. Mauris
-molestie nibh posuere fringilla rutrum. Praesent mattis tortor sapien, semper
-varius elit ultrices in.
-
-Etiam non leo lacus. Cras id tincidunt ante. Donec mattis urna fermentum ex
-elementum blandit. Sed ornare vestibulum nulla luctus malesuada. Maecenas
-pulvinar metus tortor. Sed dapibus enim vel sem bibendum, sit amet tincidunt
-ligula varius. Nullam vitae augue at dui blandit cursus. Suspendisse faucibus
-posuere luctus.
-
-Class aptent taciti sociosqu ad litora torquent per conubia nostra, per inceptos
-himenaeos. Aenean suscipit diam eu luctus auctor. Donec non magna quis ex
-tincidunt condimentum. Ut porta maximus quam, non varius sem mattis eu. Fusce
-sit amet vestibulum libero. Aliquam vestibulum sagittis mi a pellentesque. Cras
-maximus cursus libero vitae porttitor. Aenean fermentum erat eget turpis mattis,
-quis commodo magna pharetra. Praesent eu hendrerit arcu. Proin mollis, sem ac
-accumsan dignissim, velit risus ultricies mauris, eu imperdiet dolor ipsum at
-augue. Fusce bibendum, tortor eget pulvinar auctor, leo mi volutpat urna, nec
-convallis sem quam non tellus. Vestibulum fermentum sodales faucibus. Nunc quis
-feugiat quam. Donec pulvinar feugiat mauris non porttitor.

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,9 +1,8 @@
-#lang typed/syndicate
+#lang typed/syndicate/roles
 
 ;; ---------------------------------------------------------------------------------------------------
 ;; Protocol
 
-
 #|
 Conversations in the flink dataspace primarily concern two topics: presence and
 task execution.
@@ -115,8 +114,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 +122,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))
@@ -178,12 +168,9 @@ The JobManager then performs the job and, when finished, asserts
     (printf fmt . args)
     (printf "\n")))
 
-
-
 ;; ---------------------------------------------------------------------------------------------------
 ;; TaskRunner
 
-
 (define (word-count-increment [h : WordCount]
                               [word : String]
                               -> WordCount)
@@ -204,9 +191,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,18 +209,16 @@ 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
 
-
 (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,11 +279,25 @@ 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
 
+;; Task -> Bool
+;; Test if the task is ready to run
+(define (task-ready? [t : PendingTask] -> (Maybe ConcreteTask))
+  (match t
+    [(task $tid (map-work $s))
+     ;; 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]))
+
 ;; Task Int Any -> Task
 ;; If the given task is waiting for this data, replace the waiting ID with the data
 (define (task+data [t : PendingTask]
@@ -323,20 +321,6 @@ The JobManager then performs the job and, when finished, asserts
   (define l (split-at/lenient- xs n))
   (tuple (first l) (second l)))
 
-;; Task -> Bool
-;; Test if the task is ready to run
-(define (task-ready? [t : PendingTask] -> (Maybe ConcreteTask))
-  (match t
-    [(task $tid (map-work $s))
-     ;; 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]))
-
-
 (define (partition-ready-tasks [tasks : (List PendingTask)]
                                -> (Tuple (List PendingTask)
                                          (List ConcreteTask)))
@@ -349,7 +333,6 @@ The JobManager then performs the job and, when finished, asserts
             [none
              (left t)]))))
 
-
 (define (input->pending-task [t : InputTask] -> PendingTask)
   (match t
     [(task $id (map-work $s))
@@ -358,7 +341,6 @@ The JobManager then performs the job and, when finished, asserts
     [(task $id (reduce-work $l $r))
      (task id (reduce-work (left l) (left r)))]))
 
-
 (message-struct tasks-finished : TasksFinished (id results))
 
 ;; assertions used for internal slot-management protocol
@@ -371,8 +353,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 +495,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 +506,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 +528,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,148 @@
+#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))
+          (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)))
+        (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
@@ -115,109 +115,70 @@
      (type-error #:src e
                  #:msg "not an iterable type: ~a" τ)]))
 
-(define-for-syntax (bind-renames renames body)
-  (syntax-parse renames
-    [([x:id x-:id] ...)
-     #:with (x-- ...) (map syntax-local-identifier-as-binding (syntax->list #'(x- ...)))
-     (quasisyntax/loc body
-       (let- ()
-             (define-syntax x (make-variable-like-transformer #'x--)) ...
-             #,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] ⊢ (begin e-body ...) ≫ e-body-
+                           (⇐ : τ-acc)
+                           (⇒ ν-ep (~effs τ-ep ...))
+                           (⇒ ν-s (~effs τ-s ...))
+                           (⇒ ν-f (~effs τ-f ...))]
+  #:with e-body-- (substs #'(x- ...) #'(x-- ...) #'e-body- free-identifier=?)
   -------------------------------------------------------
-  [⊢ (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-
+                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 ...))
-  [[x ≫ x-- : τ] ... ⊢ (block e-body ...) ≫ e-body-
+  [[x ≫ x-- : τ] ... ⊢ (begin e-body ...) ≫ e-body-
                            (⇒ : τ-body)
                            (⇒ ν-ep (~effs τ-ep ...))
                            (⇒ ν-s (~effs τ-s ...))
                            (⇒ ν-f (~effs τ-f ...))]
+  #:with e-body-- (substs #'(x- ...) #'(x-- ...) #'e-body- free-identifier=?)
   ----------------------------------------------------------------------
   [⊢ (for/list- clauses-
-       #,(bind-renames #'([x-- x-] ...) #'e-body-))
-                (⇒ : (List τ-body))
-                (⇒ ν-ep (τ-ep ...))
-                (⇒ ν-s (τ-s ...))
-                (⇒ ν-f (τ-f ...))])
+                e-body--) (⇒ : (List τ-body))
+                          (⇒ ν-ep (τ-ep ...))
+                          (⇒ ν-s (τ-s ...))
+                          (⇒ ν-f (τ-f ...))])
 
 (define-typed-syntax (for/set (clause:iter-clause ...)
                        e-body ...+) ≫
   #:with (clauses- ([x x- τ] ...)) (analyze-for-clauses #'(clause.parend ...))
-  [[x ≫ x-- : τ] ... ⊢ (block e-body ...) ≫ e-body-
+  [[x ≫ x-- : τ] ... ⊢ (begin e-body ...) ≫ e-body-
                            (⇒ : τ-body)
                            (⇒ ν-ep (~effs τ-ep ...))
                            (⇒ ν-s (~effs τ-s ...))
                            (⇒ ν-f (~effs τ-f ...))]
+  #:with e-body-- (substs #'(x- ...) #'(x-- ...) #'e-body- free-identifier=?)
   ----------------------------------------------------------------------
   [⊢ (for/set- clauses-
-       #,(bind-renames #'([x-- x-] ...) #'e-body-))
-              (⇒ : (Set τ-body))
-              (⇒ ν-ep (τ-ep ...))
-              (⇒ ν-s (τ-s ...))
-              (⇒ ν-f (τ-f ...))])
+                e-body--) (⇒ : (Set τ-body))
+                          (⇒ ν-ep (τ-ep ...))
+                          (⇒ ν-s (τ-s ...))
+                          (⇒ ν-f (τ-f ...))])
 
 (define-typed-syntax (for/sum (clause ...)
                        e-body ...+) ≫
@@ -237,17 +198,18 @@
 (define-typed-syntax (for/first (clause:iter-clause ...)
                        e-body ...+) ≫
   #:with (clauses- ([x x- τ] ...)) (analyze-for-clauses #'(clause.parend ...))
-  [[x ≫ x-- : τ] ... ⊢ (block e-body ...) ≫ e-body-
+  [[x ≫ x-- : τ] ... ⊢ (begin e-body ...) ≫ e-body-
                  (⇒ : τ-body)
                  (⇒ ν-ep (~effs τ-ep ...))
                  (⇒ ν-s (~effs τ-s ...))
                  (⇒ ν-f (~effs τ-f ...))]
+  #:with e-body-- (substs #'(x- ...) #'(x-- ...) #'e-body- free-identifier=?)
   [[res ≫ _ : τ-body] ⊢ res  ≫ res- (⇒ : _)]
   ----------------------------------------------------------------------
   [⊢ (let- ()
        (define- res-
          (for/first- clauses-
-                     #,(bind-renames #'([x-- x-] ...) #'e-body-)))
+                     e-body--))
        (if- res-
             (some res-)
             none))

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/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/roles.rkt

@@ -4,25 +4,21 @@
          #%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
          FacetName Field ★/t
          Observe Inbound Outbound Actor U ⊥
-         Computation Value Endpoints Roles Spawns Sends
+         Computation Value Endpoints Roles Spawns
          →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,21 +80,13 @@
 
 (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)
 (require (for-syntax turnstile/mode))
-(require turnstile/typedefs)
 (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 +122,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)
@@ -167,7 +139,7 @@
                (~and τ-k (~Know _))
                ;; untyped syndicate might allow this - TODO
                #;(~and τ-m (~Sends _))
-               (~and τ-r (~Reacts _ _ ...))
+               (~and τ-r (~Reacts _ ...))
                ~MakesField)
           ...)
          ep-effects
@@ -180,51 +152,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)
+  ----------------------------------------------------------------------
+  [⊢ (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)
@@ -256,11 +200,8 @@
 
 (define-typed-syntax (stop facet-name:id cont ...) ≫
   [⊢ facet-name ≫ facet-name- (⇐ : FacetName)]
-  [⊢ (block #f cont ...) ≫ cont-
-                         (⇒ ν-ep (~effs))
-                         (⇒ ν-s (~effs))
-                         (⇒ ν-f (~effs τ-f ...))]
-  #:with τ #'(Stop facet-name- τ-f ...)
+  [⊢ (begin #f cont ...) ≫ cont- (⇒ ν-ep (~effs)) (⇒ ν-s (~effs)) (⇒ ν-f (~effs τ-f ...))]
+  #:with τ (mk-Stop- #`(facet-name- τ-f ...))
   ---------------------------------------------------------------------------------
   [⊢ (syndicate:stop-facet facet-name- cont-) (⇒ : ★/t)
                                               (⇒ ν-f (τ))])
@@ -312,7 +253,7 @@
 (define-typed-syntax on
   #:datum-literals (start stop)
   [(on start s ...) ≫
-   [⊢ (block s ...) ≫ s- (⇒ ν-ep (~effs))
+   [⊢ (begin s ...) ≫ s- (⇒ ν-ep (~effs))
                           (⇒ ν-f (~effs τ-f ...))
                           (⇒ ν-s (~effs τ-s ...))]
    #:with τ-r (type-eval #'(Reacts OnStart τ-f ... τ-s ...))
@@ -320,7 +261,7 @@
    [⊢ (syndicate:on-start s-) (⇒ : ★/t)
       (⇒ ν-ep (τ-r))]]
   [(on stop s ...) ≫
-   [⊢ (block s ...) ≫ s- (⇒ ν-ep (~effs))
+   [⊢ (begin s ...) ≫ s- (⇒ ν-ep (~effs))
                           (⇒ ν-f (~effs τ-f ...))
                           (⇒ ν-s (~effs τ-s ...))]
    #:with τ-r (type-eval #'(Reacts OnStop τ-f ... τ-s ...))
@@ -336,9 +277,8 @@
    #: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-
+   [[x ≫ x- : τ] ... ⊢ (begin s ...) ≫ s-
                  (⇒ ν-ep (~effs))
                  (⇒ ν-f (~effs τ-f ...))
                  (⇒ ν-s (~effs τ-s ...))]
@@ -352,7 +292,7 @@
       (⇒ ν-ep (τ-r))]])
 
 (define-typed-syntax (begin/dataflow s ...+) ≫
-  [⊢ (block s ...) ≫ s-
+  [⊢ (begin s ...) ≫ s-
      (⇒ : _)
      (⇒ ν-ep (~effs))
      (⇒ ν-f (~effs τ-f ...))
@@ -376,16 +316,13 @@
   ;; TODO: check that each τ-f is a Role
   #:mode (communication-type-mode #'τ-c.norm)
     [
-     [⊢ (block s) ≫ s- (⇒ ν-ep (~effs)) (⇒ ν-s (~effs)) (⇒ ν-f (~effs τ-f ...))]
+     [⊢ 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 +394,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 +424,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
@@ -503,7 +447,7 @@
      #'τ]
     [(~U* τ ...)
      (mk-U- (stx-map instantiate-pattern-type #'(τ ...)))]
-    [(~Any/new τ-cons τ ...)
+    [(~Any/bvs τ-cons () τ ...)
      #:when (reassemblable? #'τ-cons)
      (define subitems (for/list ([t (in-syntax #'(τ ...))])
                         (instantiate-pattern-type t)))
@@ -623,16 +567,10 @@
 ;; n.b. this is a blocking operation, so an actor that uses this internally
 ;; won't necessarily terminate.
 (define-typed-syntax (run-ground-dataspace τ-c:type s ...) ≫
-  ;;#:fail-unless (flat-type? #'τ-c.norm) "Communication type must be first-order"
-  #:mode (communication-type-mode #'τ-c.norm)
-  [
-   [⊢ s ≫ s- (⇒ : t1)] ...
-   [⊢ (dataspace τ-c.norm s- ...) ≫ _ (⇒ : t2)]
-  ]
-  #:with τ-out (strip-outbound #'τ-c.norm)
+  [⊢ (dataspace τ-c s ...) ≫ ((~literal erased) ((~literal syndicate:dataspace) s- ...)) (⇒ : t)]
   -----------------------------------------------------------------------------------
-  [⊢ (#%app- syndicate:run-ground (#%app- syndicate:capture-actor-actions (lambda- () (#%app- list- s- ...))))
-     (⇒ : (AssertionSet τ-out))])
+  [⊢ (#%app- syndicate:run-ground s- ...) (⇒ : (AssertionSet τ-c))])
+
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Utilities
@@ -659,218 +597,11 @@
   ----------------------------------------
   [⊢ (#%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
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 (module+ test
-  (check-type
-    (spawn (U (Observe (Tuple Int ★/t)))
-           (start-facet echo
-                        (on (message (tuple 1 $x:Int))
-                            #f)))
-    : ★/t)
   (check-type (spawn (U (Message (Tuple String Int))
                         (Observe (Tuple String ★/t)))
                      (start-facet echo

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/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/ltl.rkt

@@ -1,69 +0,0 @@
-#lang racket
-
-(provide (all-defined-out))
-
-;; an [LTL X] is one of
-;;  - (always [LTL X])
-;;  - (eventually [LTL X])
-;;  - (weak-until [LTL X] [LTL X])
-;;  - (strong-until [LTL X] [LTL X])
-;;  - (ltl-implies [LTL X] [LTL X])
-;;  - (ltl-and [Listof [LTL X]])
-;;  - (ltl-or  [Listof [LTL X]])
-;;  - (ltl-not [LTL X])
-;;  - (atomic X)
-;;  - 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)
-
-;; [LTL X] {X -> Y} -> [LTL Y]
-(define (map-atomic ltl op)
-  (let loop ([ltl ltl])
-    (match ltl
-      [(always p)
-       (always (loop p))]
-      [(eventually p)
-       (eventually (loop p))]
-      [(weak-until p q)
-       (weak-until (loop p) (loop q))]
-      [(strong-until p q)
-       (strong-until (loop p) (loop q))]
-      [(ltl-implies p q)
-       (ltl-implies (loop p) (loop q))]
-      [(ltl-and p q)
-       (ltl-and (loop p) (loop q))]
-      [(ltl-or p q)
-       (ltl-or (loop p) (loop q))]
-      [(ltl-not p)
-       (ltl-not (loop p))]
-      [(atomic x)
-       (atomic (op x))]
-      [#t
-       #t]
-      [#f
-       #f])))
-
-(define (&& . args)
-  (fold-bin-op ltl-and args #t))
-
-(define (|| . args)
-  (fold-bin-op ltl-or args #f))
-
-(define (fold-bin-op op args base)
-  (let loop ([args args])
-    (match args
-      ['()
-       base]
-      [(list x y)
-       (op x y)]
-      [(cons fst rst)
-       (op fst (loop rst))])))

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/syndicate/spin-prelude.pml

@@ -1,10 +0,0 @@
-/* Useful macros */
-
-#define ASSERTED(x) (x##_assertions > 0)
-#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/syntax-serializer.rkt

@@ -1,302 +0,0 @@
-#lang racket/base
-
-(provide serialize-syntax deserialize-syntax)
-
-(require racket/dict racket/match)
-
-(struct serialized-syntax (unique-tag table contents) #:prefab)
-(struct stx-with-props (stx ps) #:prefab)
-(struct syntax-val (stx) #:prefab)
-(struct datum-val (d) #:prefab)
-(struct ref (unique-tag sym) #:prefab)
-
-;(require racket/pretty)
-
-(define (serialize-syntax stx)
-  (define unique-tag (gensym))
-  (define table (hasheq))
-  (define dedup-table (hasheq))
-  (define (dedup k f)
-    (if (hash-has-key? dedup-table k)
-      (hash-ref dedup-table k)
-      (let ([res (f)])
-        (set! dedup-table (hash-set dedup-table k res))
-        res)))
-
-  (define (lift! el)
-    (define tag-sym (gensym))
-    (set! table (hash-set table tag-sym el))
-    (ref unique-tag tag-sym))
-
-  (define (build-props! orig-s d)
-    (stx-with-props
-     (datum->syntax orig-s d orig-s #f)
-     (for/list ([k (syntax-property-symbol-keys orig-s)]
-                #:when (syntax-property-preserved? orig-s k))
-       (define val (syntax-property orig-s k))
-       (define serialized-val
-         (if (syntax? val)
-             (syntax-val (serialize-element! val))
-             (datum-val (serialize-element! val #:always-lift? #t))))
-       (cons k serialized-val))))
-
-  (define (serialize-element! el #:always-lift? [always-lift? #f])
-    (dedup
-      el
-      (lambda ()
-        (syntax-map
-          el
-          (lambda (tail? d) d)
-          (lambda (orig-s d)
-            ;(when (and always-lift? (not (ref? (hash-ref dedup-table orig-s)))) ; TODO
-            ;(error 'dedup "lift error"))
-            (dedup
-              orig-s
-              (lambda ()
-                (if (or always-lift?
-                        (ormap (lambda (p) (syntax-property-preserved? orig-s p))
-                               (syntax-property-symbol-keys orig-s)))
-                  (lift! (build-props! orig-s d))
-                  (datum->syntax orig-s d orig-s #f)))))
-          syntax-e))))
-
-  (define top-s (serialize-element! stx))
-  (define res (datum->syntax #f (serialized-syntax unique-tag table top-s)))
-
-  res)
-
-(define (deserialize-syntax ser)
-  (match (syntax-e ser)
-    [(serialized-syntax unique-tag-stx table-stx contents)
-     (define unique-tag (syntax-e unique-tag-stx))
-     (define table (syntax-e table-stx))
-     (define dedup-table (hasheq))
-     (define (dedup k f)
-       (if (hash-has-key? dedup-table k)
-         (hash-ref dedup-table k)
-         (let ([res (f)])
-           (set! dedup-table (hash-set dedup-table k res))
-           res)))
-
-
-     (define (maybe-syntax-e v)
-       (if (syntax? v) (syntax-e v) v))
-
-     (define (deserialize-stx-with-props ref-sym)
-       (match-define (stx-with-props stx ps) (syntax-e (hash-ref table ref-sym)))
-       (define deserialized-nested-stx (deserialize-element stx))
-       (for/fold ([stx deserialized-nested-stx])
-                 ([stx-pr (syntax->list ps)])
-         (define pr (syntax-e stx-pr))
-         (define k (syntax-e (car pr)))
-         (define v (syntax-e (cdr pr)))
-         (define prop-val
-           (match v
-             [(syntax-val v)
-              (deserialize-element v)]
-             [(datum-val v)
-              (deserialize-element (syntax->datum v))]))
-         (syntax-property stx k prop-val #t)))
-
-     (define (deserialize-element el)
-       (dedup
-         el
-         (lambda ()
-           (syntax-map
-             el
-             (lambda (tail? d)
-               (match d
-                 [(ref tag sym)
-                  #:when (equal? (maybe-syntax-e tag) unique-tag)
-                  (dedup
-                    sym
-                    (lambda () (deserialize-stx-with-props (maybe-syntax-e sym))))]
-                 [_ d]))
-             (lambda (orig-s d)
-               (dedup
-                 orig-s
-                 (lambda () (datum->syntax orig-s d orig-s #f))))
-             syntax-e))))
-
-     (define res (deserialize-element contents))
-     res]))
-   
-(module+ test
-  (require rackunit)
-
-  (define type
-    (syntax-property
-      (syntax-property #'Int ':: #'Type #t)
-      'orig (list #'Int) #t))
-  (define term (syntax-property #`(1 #,(syntax-property #'2 ': type #t)) ': #'Type #t))
-  (define s (serialize-syntax term))
-  (define d (deserialize-syntax s))
-
-  (check-true
-   (bound-identifier=?
-    (syntax-property d ':)
-    #'Type))
-
-  ; syntax with properties inside outer syntax with properties.
-  (check-true
-   (bound-identifier=?
-    (syntax-property (syntax-property (cadr (syntax-e d)) ':) '::)
-    #'Type))
-
-  (check-true
-   (bound-identifier=?
-    (syntax-property (cadr (syntax-e d)) ':)
-    #'Int))
-
-  (check-equal?
-   (syntax-position term)
-   (syntax-position d))
-  
-  (check-equal?
-   (syntax-position (syntax-property (cadr (syntax-e term)) ':))
-   (syntax-position (syntax-property (cadr (syntax-e d)) ':)))
-
-  (check-equal?
-   (syntax-position (car (syntax-e term)))
-   (syntax-position (car (syntax-e d))))
-
-  ; syntax in datum in properties
-  (check-true
-    (bound-identifier=?
-      (car (syntax-property (syntax-property (cadr (syntax-e d)) ':) 'orig))
-      #'Int))
-  )
-
-
-;; ----------------------------------------------------------------
-
-;; syntax-map and datum-map copied from the expander files
-;;    syntax/datum-map.rkt
-;;    syntax/syntax.rkt
-
-(require racket/fixnum racket/prefab)
-
-;; `(datum-map v f)` walks over `v`, traversing objects that
-;; `datum->syntax` traverses to convert content to syntax objects.
-;; 
-;; `(f tail? d)` is called on each datum `d`, where `tail?`
-;; indicates that the value is a pair/null in a `cdr` --- so that it
-;; doesn't need to be wrapped for `datum->syntax`, for example;
-;; the `tail?` argument is actually #f or a fixnum for a lower bound
-;; on `cdr`s that have been taken
-;;
-;; `gf` is like `f`, but `gf` is used when the argument might be
-;; syntax; if `gf` is provided, `f` can assume that its argument
-;; is not syntax
-;;
-;; If a `seen` argument is provided, then it should be an `eq?`-based
-;; hash table, and cycle checking is enabled; when a cycle is
-;; discovered, the procedure attached to 'cycle-fail in the initial
-;; table is called
-;;
-;; If a `known-pairs` argument is provided, then it should be an
-;; `eq?`-based hash table to map pairs that can be returned as-is
-;; in a `tail?` position
-
-;; The inline version uses `f` only in an application position to
-;; help avoid allocating a closure. It also covers only the most common
-;; cases, defering to the general (not inlined) function for other cases.
-(define (datum-map s f [gf f] [seen #f] [known-pairs #f])
-  (let loop ([tail? #f] [s s] [prev-depth 0])
-    (define depth (fx+ 1 prev-depth)) ; avoid cycle-checking overhead for shallow cases
-    (cond
-      [(and seen (depth . fx> . 32))
-       (datum-map-slow tail? s  (lambda (tail? s) (gf tail? s)) seen known-pairs)]
-      [(null? s) (f tail? s)]
-      [(pair? s)
-       (f tail? (cons (loop #f (car s) depth)
-                      (loop 1 (cdr s) depth)))]
-      [(symbol? s) (f #f s)]
-      [(boolean? s) (f #f s)]
-      [(number? s) (f #f s)]
-      [(or (vector? s) (box? s) (prefab-struct-key s) (hash? s))
-       (datum-map-slow tail? s (lambda (tail? s) (gf tail? s)) seen known-pairs)]
-      [else (gf #f s)])))
-
-(define (datum-map-slow tail? s f seen known-pairs)
-  (let loop ([tail? tail?] [s s] [prev-seen seen])
-    (define seen
-      (cond
-        [(and prev-seen (datum-has-elements? s))
-         (cond
-           [(hash-ref prev-seen s #f)
-            ((hash-ref prev-seen 'cycle-fail) s)]
-           [else (hash-set prev-seen s #t)])]
-        [else prev-seen]))
-    (cond
-      [(null? s) (f tail? s)]
-      [(pair? s)
-       (cond
-         [(and known-pairs
-               tail?
-               (hash-ref known-pairs s #f))
-          s]
-         [else
-          (f tail? (cons (loop #f (car s) seen)
-                         (loop (if tail? (fx+ 1 tail?) 1)  (cdr s) seen)))])]
-      [(or (symbol? s) (boolean? s) (number? s))
-       (f #f s)]
-      [(vector? s)
-       (f #f (vector->immutable-vector
-              (for/vector #:length (vector-length s) ([e (in-vector s)])
-                (loop #f e seen))))]
-      [(box? s)
-       (f #f (box-immutable (loop #f (unbox s) seen)))]
-      [(immutable-prefab-struct-key s)
-       => (lambda (key)
-            (f #f
-               (apply make-prefab-struct
-                      key
-                      (for/list ([e (in-vector (struct->vector s) 1)])
-                        (loop #f e seen)))))]
-      [(and (hash? s) (immutable? s))
-       (cond
-         [(hash-eq? s)
-          (f #f
-             (for/hasheq ([(k v) (in-hash s)])
-               (values k (loop #f v seen))))]
-         [(hash-eqv? s)
-          (f #f
-             (for/hasheqv ([(k v) (in-hash s)])
-               (values k (loop #f v seen))))]
-         [else
-          (f #f
-             (for/hash ([(k v) (in-hash s)])
-               (values k (loop #f v seen))))])]
-      [else (f #f s)])))
-
-(define (datum-has-elements? d)
-  (or (pair? d)
-      (vector? d)
-      (box? d)
-      (immutable-prefab-struct-key d)
-      (and (hash? d) (immutable? d) (positive? (hash-count d)))))
-
-;; `(syntax-map s f d->s)` walks over `s`:
-;; 
-;;  * `(f tail? d)` is called to each datum `d`, where `tail?`
-;;    indicates that the value is a pair/null in a `cdr` --- so that it
-;;    doesn't need to be wrapped for `datum->syntax`, for example
-;;
-;;  * `(d->s orig-s d)` is called for each syntax object,
-;;    and the second argument is result of traversing its datum
-;; 
-;;  * the `s-e` function extracts content of a syntax object
-;;
-;; The optional `seen` argument is an `eq?`-based immutable hash table
-;; to detect and reject cycles. See `datum-map`.
-
-(define (syntax-map s f d->s s-e [seen #f])
-  (let loop ([s s])
-    (datum-map s
-               f
-               (lambda (tail? v)
-                 (cond
-                   [(syntax? v) (d->s v (loop (s-e v)))]
-                   [else (f tail? v)]))
-               seen)))

racket/typed/syndicate/test-utils.rkt

@@ -1,17 +0,0 @@
-#lang racket/base
-
-(provide run/timeout
-         define/timeout)
-
-(require racket/engine)
-
-;; (-> A) Real -> (U A Engine)
-;; run the given thunk in an engine for 'fuel' milliseconds
-;; if the engine completes, returns the result, otherwise the engine itself
-(define (run/timeout tnk [fuel 1000])
-  (define e (engine (lambda (p) (tnk))))
-  (define r (engine-run fuel e))
-  (if r (engine-result e) e))
-
-(define-syntax-rule (define/timeout x e)
-  (define x (run/timeout (lambda () e))))

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,9 +0,0 @@
-#lang typed/syndicate
-
-(require rackunit/turnstile)
-
-(check-type (for/list ([x (for/list ([y (list 1 2 3)])
-                            y)])
-              x)
-            : (List Int)
-            ⇒ (list 1 2 3))

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,9 +1,9 @@
-#lang typed/syndicate
+#lang typed/syndicate/roles
 
 (require rackunit/turnstile)
 
 (check-type
- (let ()
+ (begin
   (field [boo Int 0])
   (define x (begin (send! "hi") 5))
   ;; relying on `set` not allowing effects for this to be a good test

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