Don't use syndicate's action-collecting module-begin

Implicitly starting a dataspace with top-level actions is a hole for
the type system, which needs to know the type of possible assertions.

Instead, provide `run-ground-dataspace` for kicking off the program.

examples/ircd/message.rkt

@@ -64,7 +64,7 @@
 (define (parse-command prefix line)
   (match-define (pregexp #px"^([^ ]+)( +([^:]+)?(:(.*))?)?$" (list _ command _ params _ rest)) line)
   (irc-message prefix
-               (string-upcase command)
+               command
                (string-split (or params ""))
                rest))
 

examples/ircd/session.rkt

@@ -154,15 +154,6 @@
                                     (irc-privmsg (irc-source-nick (nick) (user)) T Text))))]
              [_ (void)]))])))
 
-(spawn #:name 'ison-responder
-       (stop-when-reloaded)
-       (define/query-set nicks (ircd-connection-info _ $N _) N)
-       (on (message (ircd-action $conn (irc-message _ "ISON" $SomeNicks $MoreNicks)))
-           (define Nicks (append SomeNicks (string-split (or MoreNicks ""))))
-           (define (on? N) (set-member? (nicks) N))
-           (define Present (string-join (filter on? Nicks) " "))
-           (send! (ircd-event conn (irc-message server-prefix 303 '("*") Present)))))
-
 (spawn #:name 'session-listener-factory
        (stop-when-reloaded)
        (during/spawn (ircd-listener $port)

racket/info.rkt

@@ -1,43 +1,26 @@
 #lang setup/infotab
 (define collection 'multi)
-(define deps '(
+(define deps '("rfc6455"
 	       "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"
-                     ))
-
-(define test-omit-paths
-  ;; There's some shared library related build issue with the syndicate-gl things
-  '("syndicate-gl/"
-    "syndicate-ide/"))
+                     "draw-doc" "gui-doc" "htdp-doc" "pict-doc"))

racket/syndicate-gui-toolbox/examples/7-GUIS/cells-canvas.rkt

@@ -1,44 +0,0 @@
-#lang syndicate
-
-;; actor adapter for canvas-double-click% and cells-canvas%
-(require 7GUI/canvas-double-click)
-(require 7GUI/task-7-view)
-(require (only-in "../../widgets.rkt" qc))
-
-(provide spawn-cells-canvas
-         (struct-out single-click)
-         (struct-out double-click)
-         (struct-out update-grid))
-
-(require racket/gui/base
-         (except-in racket/class field))
-
-(message-struct single-click (x y))
-(message-struct double-click (x y))
-(message-struct update-grid (cells))
-
-;; ---------------------------------------------------------------------------------------------------
-(define cells-canvas%
-  (class canvas-double-click%
-    (define/augment-final (on-click x y) (send-ground-message (single-click x y)))
-    (define/augment-final (on-double-click x y) (send-ground-message (double-click x y)))
-    (define *content #f)
-    (define/public (update-grid cells)
-      (set! *content cells)
-      (qc (define dc (send this get-dc))
-          (paint-grid dc *content)))
-    (super-new [paint-callback (lambda (_self dc) (when *content (paint-grid dc *content)))])))
-
-(define (spawn-cells-canvas parent width height)
-  (define parent-component (seal-contents parent))
-  (define canvas (new cells-canvas% [parent parent-component] [style '(hscroll vscroll)]))
-  (qc (send canvas init-auto-scrollbars width height 0. 0.)
-      (send canvas show-scrollbars #t #t))
-
-  (spawn
-   (on (message (update-grid $cells))
-       (qc (send canvas update-grid cells)))
-   (on (message (inbound (single-click $x $y)))
-       (send! (single-click x y)))
-   (on (message (inbound (double-click $x $y)))
-       (send! (double-click x y)))))

racket/syndicate-gui-toolbox/examples/7-GUIS/task-1.rkt

@@ -1,22 +0,0 @@
-#lang syndicate
-
-(require "../../widgets.rkt")
-(require (only-in racket/format ~a))
-
-;; a mouse-click counter
-
-(define frame (spawn-frame #:label "Counter"))
-(define pane  (spawn-horizontal-pane #:parent frame))
-(define view  (spawn-text-field #:parent pane #:label "" #:init-value "0" #:enabled #f #:min-width 100))
-(define _but  (spawn-button #:parent pane #:label "Count"))
-
-(spawn
- (field [counter 0])
- (on (message (button-press _but))
-     (counter (add1 (counter)))
-     (send! (set-text-field view (~a (counter)))))
- (on-start
-  (send! (show frame #t))))
-
-(module+ main
-  (void))

racket/syndicate-gui-toolbox/examples/7-GUIS/task-2.rkt

@@ -1,59 +0,0 @@
-#lang syndicate
-
-(require "../../widgets.rkt")
-(require (only-in racket/format ~a ~r))
-
-;; a bi-directional temperature converter (Fahrenheit vs Celsius)
-
-(define ((callback setter) field val)
-  (define-values (field:num last) (string->number* val))
-  (cond
-    [(and field:num (rational? field:num))
-     (define inexact-n (* #i1.0 field:num))
-     (setter inexact-n)
-     (render field inexact-n last)]
-    [else (send! (set-text-field-background field "red"))]))
-
-(define (string->number* str)
-  (define n (string->number str))
-  (values n (and n (string-ref str (- (string-length str) 1)))))
-
-(define (flow *from --> *to to-field)
-  (λ (x)
-    (*from x)
-    (*to (--> x))
-    (render to-field (*to) "")))
-
-(define (render to-field *to last)
-  (send! (set-text-field-background to-field "white"))
-  (send! (set-text-field to-field (~a (~r *to #:precision 4) (if (eq? #\. last) "." "")))))
-
-(define frame   (spawn-frame #:label "temperature converter"))
-(define pane    (spawn-horizontal-pane #:parent frame))
-
-(define (make-field v0 lbl)
-  (spawn-text-field #:parent pane
-                    #:min-width 199
-                    #:label lbl
-                    #:init-value v0))
-
-(define C0 0)
-(define F0 32)
-
-(define C-field (make-field  (~a C0) "celsius:"))
-(define F-field (make-field  (~a F0) " = fahrenheit:"))
-
-(spawn
-
- (field [*C C0]
-        [*F F0])
-
- (define celsius->fahrenheit (callback (flow *C (λ (c) (+  (* c 9/5) 32)) *F F-field)))
- (define fahrenheit->celsius (callback (flow *F (λ (f) (* (- f 32) 5/9))  *C C-field)))
-
- (on (message (text-field-update C-field $val))
-     (celsius->fahrenheit C-field val))
- (on (message (text-field-update F-field $val))
-     (fahrenheit->celsius F-field val))
- (on-start
-  (send! (show frame #t))))

racket/syndicate-gui-toolbox/examples/7-GUIS/task-3.rkt

@@ -1,67 +0,0 @@
-#lang syndicate
-
-(require "../../widgets.rkt")
-
-;; a flight booker that allows a choice between one-way and return bookings
-;; and, depending on the choice, a start date or a start date and an end date. 
-
-;; ---------------------------------------------------------------------------------------------------
-(require gregor)
-
-;; gregor should not raise an exception when parsing fails, but return #f
-(define (to-date d) (with-handlers ([exn? (λ (_) #f)]) (parse-date d "d.M.y")))
-
-;; ---------------------------------------------------------------------------------------------------
-(define DATE0   "27.03.2014")
-(define ONE     "one-way flight")
-(define RETURN  "return flight")
-(define CHOICES `(,ONE ,RETURN))
-(define RED     "red")
-(define WHITE   "white")
-
-(define (make-field enabled)
-  (spawn-text-field #:parent frame
-                    #:label ""
-                    #:init-value DATE0
-                    #:enabled enabled))
-
-(define frame    (spawn-frame #:label "flight booker"))
-(define choice   (spawn-choice #:label "" #:parent frame #:choices CHOICES))
-(define start-d  (make-field #t))
-(define return-d (make-field #f))
-(define book     (spawn-button #:label "Book" #:parent frame))
-
-(spawn
- (field [*kind-flight (list-ref CHOICES 0)]  ;; one of the CHOICES
-        [*start-date  (to-date DATE0)]       ;; date
-        [*return-date (to-date DATE0)])      ;; date
-
- (define (field-cb self val date-setter!)
-   (define date (to-date val))
-   (cond
-     [date (send! (set-text-field-background self WHITE)) (date-setter! date) (enable-book)]
-     [else (send! (set-text-field-background self RED))   (enable-book #f #f)]))
-
- (define (enable-book [start-date (*start-date)] [return-date (*return-date)])
-   (send! (enable book #f))
-   (when (and start-date (date<=? (today) start-date)
-              (or (and (string=? ONE (*kind-flight)))
-                  (and return-date (date<=? start-date return-date))))
-     (send! (enable book #t))))
-
- (define (enable-return-book selection)
-   (*kind-flight selection)
-   (send! (enable return-d (string=? RETURN (*kind-flight))))
-   (enable-book))
-
- (on (message (text-field-update start-d $val))
-     (field-cb start-d val *start-date))
- (on (message (text-field-update return-d $val))
-     (field-cb return-d val *return-date))
- (on (message (choice-selection choice $sel))
-     (enable-return-book sel))
- (on (message (button-press book))
-     (displayln "confirmed"))
-
- (on-start (send! (show frame #t))
-           (enable-return-book (*kind-flight))))

racket/syndicate-gui-toolbox/examples/7-GUIS/task-4.rkt

@@ -1,58 +0,0 @@
-#lang syndicate
-
-(require "../../widgets.rkt")
-(require/activate syndicate/drivers/timestate)
-
-;; notes on MF impl:
-;;  - reset button doesn't do anything if duration is at 0
-;;  - duration is meant to update as slider is moved, not just when released
-
-;; a timer that permits the continuous setting of a new interval, plusanything if duration is at 0
-;;  - duration is meant to update as slider is moved, not just when released
-;; a gauge and a text field that display the fraction of the elapsed time
-;; a reset button that sends the elapsed time back to 0
-
-(define INTERVAL 100)
-
-(define (next-time) (+ (current-milliseconds) INTERVAL))
-
-(define frame   (spawn-frame #:label "timer"))
-(define elapsed (spawn-gauge #:label "elapsed" #:parent frame #:enabled #f #:range 100))
-(define text    (spawn-text-field #:parent frame #:init-value "0" #:label ""))
-(define slider  (spawn-slider #:label "duration" #:parent frame #:min-value 0 #:max-value 100))
-(define button  (spawn-button #:label "reset" #:parent frame))
-
-(spawn
- (field [*elapsed 0]  ;; INTERVAL/1000 ms accumulated elapsed time
-        [*duration 0] ;; INTERVAL/1000 ms set duration interval
-        [t (next-time)])
-
- (define (timer-cb)
-   (unless (>= (*elapsed) (*duration))
-     (*elapsed (+ (*elapsed) 1))
-     (t (next-time))
-     (elapsed-cb)))
-
- (define (elapsed-cb)
-   (send! (set-text-field text (format "elapsed ~a" (*elapsed))))
-   (unless (zero? (*duration))
-     (define r (quotient (* 100 (*elapsed)) (*duration)))
-     (send! (set-gauge-value elapsed r))))
-
- (define (reset-cb)
-   (*elapsed 0)
-   (timer-cb))
-
- (define (duration-cb new-duration)
-   (unless (= new-duration (*duration))
-     (*duration new-duration)
-     (timer-cb)))
-
- (on (asserted (later-than (t)))
-     (timer-cb))
- (on (message (button-press button))
-     (reset-cb))
- (on (message (slider-update slider $val))
-     (duration-cb val))
- (on-start (elapsed-cb)
-           (send! (show frame #t))))

racket/syndicate-gui-toolbox/examples/7-GUIS/task-5.rkt

@@ -1,71 +0,0 @@
-#lang syndicate
-
-(require "../../widgets.rkt")
-(require (only-in racket/string string-prefix?))
-(require (only-in racket/function curry))
-(require (only-in racket/list first rest))
-
-;; a create-read-update-deleted MVC implementation 
-
-;; ---------------------------------------------------------------------------------------------------
-(define frame   (spawn-frame #:label "CRUD"))
-(define hpane1  (spawn-horizontal-pane #:parent frame #:border 10 #:alignment '(left bottom)))
-(define vpane1  (spawn-vertical-pane #:parent hpane1))
-(define filter-tf (spawn-text-field #:parent vpane1 #:label "Filter prefix: " #:init-value ""))
-(define lbox    (spawn-list-box #:parent vpane1 #:label #f #:choices '() #:min-width 100 #:min-height 100))
-(define vpane2  (spawn-vertical-pane #:parent hpane1 #:alignment '(right center)))
-(define name    (spawn-text-field #:parent vpane2 #:label "Name:      " #:init-value "" #:min-width 200))
-(define surname (spawn-text-field #:parent vpane2 #:label "Surname: " #:init-value "" #:min-width 200))
-(define hpane2  (spawn-horizontal-pane #:parent frame))
-(define create-but (spawn-button #:label "Create" #:parent hpane2))
-(define update-but (spawn-button #:label "Update" #:parent hpane2))
-(define delete-but (spawn-button #:label "Delete" #:parent hpane2))
-
-(spawn
- (field [*data '("Emil, Hans" "Mustermann, Max" "Tisch, Roman")]
-        [*selector ""]
-        [*selected (*data)]) ;; selected = (filter select data)
- ;; ---------------------------------------------------------------------------------------------------
-(define (selector! nu) (*selector nu) (data->selected!))
-(define (select s) (string-prefix? s (*selector)))
-(define (data->selected!)  (*selected (if (string=? "" (*selector)) (*data) (filter select (*data)))))
-
-(define-syntax-rule (def-! (name x ...) exp) (define (name x ...) (*data exp) (data->selected!)))
-(def-! (create-entry new-entry) (append (*data) (list new-entry)))
-(def-! (update-entry new-entry i) (operate-on i (curry cons new-entry) (*data) select (*selected)))
-(def-! (delete-from i) (operate-on i  values))
-
-#; {N [[Listof X] -> [Listof X]] [Listof X] [X -> Boolean] [Listof X] -> [Listof X]}
-;; traverse list to the i-th position of selected in data, then apply operator to rest (efficiency)
-;; ASSUME selected = (filter selector data)
-;; ASSUME i <= (length selected)
-(define (operate-on i operator [data (*data)] [select select] [selected (*selected)])
-  (let sync ((i i) (data data) (selected selected))
-    (if (select (first data))
-        (if (zero? i)
-            (operator (rest data))
-            (cons (first data) (sync (sub1 i) (rest data) (rest selected))))
-        (cons (first data) (sync i (rest data) selected)))))
-
-;; ---------------------------------------------------------------------------------------------------
-(define-syntax-rule (def-cb (name x) exp ...) (define (name x) exp ... (send! (set-list-box-choices lbox (*selected)))))
-(def-cb (prefix-cb prefix) (selector! prefix))
-(def-cb (Create-cb _b) (create-entry (retrieve-name)))
-(def-cb (Update-cb _b) (common-cb (curry update-entry (retrieve-name))))
-(def-cb (Delete-cb _b) (common-cb delete-from))
-
-(on (message (text-field-update filter-tf $prefix)) (prefix-cb prefix))
-(on (message (button-press create-but)) (Create-cb create-but))
-(on (message (button-press update-but)) (Update-cb update-but))
-(on (message (button-press delete-but)) (Delete-cb delete-but))
-
-(define/query-value current-selection #f (list-box@ lbox $selection) selection)
-(define/query-value *surname "" (text-field@ surname $val) val)
-(define/query-value *name "" (text-field@ name $val) val)
-
-(local-require 7GUI/should-be-racket)
-(define (common-cb f) (when* (current-selection) => f))
-(define (retrieve-name) (string-append (*surname) ", " (*name)))
-
-(on-start (prefix-cb "")
-          (send! (show frame #t))))

racket/syndicate-gui-toolbox/examples/7-GUIS/task-6.rkt

@@ -1,206 +0,0 @@
-#lang syndicate
-
-(require "../../widgets.rkt")
-(require racket/list
-         racket/gui/base
-         (except-in racket/class field))
-
-;; a circle drawer with undo/redo facilities (unclear spec for resizing)
-
-(message-struct circle-canvas-event (type x y))
-(message-struct resize (circ d))
-(message-struct draw-circles (closest others))
-
-;; ---------------------------------------------------------------------------------------------------
-(define Default-Diameter 20)
-
-(struct circle (x y d action) #:transparent)
-
-(define (draw-1-circle dc brush c)
-  (match-define (circle x y d _a) c)
-  (send dc set-brush brush)
-  (define r (/ d 2))
-  (send dc draw-ellipse (- x r) (- y r) d d))
-
-
-;; N N (Circle -> Real]
-(define ((distance xm ym) c)
-  (match-define (circle xc yc _d _a) c)
-  (sqrt (+ (expt (- xc xm) 2) (expt (- yc ym) 2))))
-
-;; ---------------------------------------------------------------------------------------------------
-(define solid-gray  (new brush% [color "gray"]))
-(define white-brush (new brush% [color "white"]))
-
-(define circle-canvas%
-  (class canvas%
-    (inherit on-paint get-dc)
-
-    (define/override (on-event evt)
-      (define type (send evt get-event-type))
-      (define x (send evt get-x))
-      (define y (send evt get-y))
-      (send-ground-message (circle-canvas-event type x y)))
-
-    (define (paint-callback _self _evt)
-      (draw-circles *last-closest *last-others))
-
-    (define *last-closest #f)
-    (define *last-others #f)
-
-    (define/public (draw-circles closest (others-without-closest #f))
-      (set! *last-closest closest)
-      (set! *last-others others-without-closest)
-      (define dc (get-dc))
-      (send dc clear)
-      (when others-without-closest
-        (for ((c others-without-closest)) (draw-1-circle dc white-brush c)))
-      (when closest (draw-1-circle dc solid-gray closest)))
-
-    (super-new [paint-callback paint-callback])))
-
-(define (spawn-circle-canvas parent frame undo-but redo-but)
-  (define cc (new circle-canvas% [parent (seal-contents parent)][style '(border)]))
-
-  (spawn
-   (field [*circles '()]
-          [*history '()]
-          [*x 0]
-          [*y 0]
-          [*in-adjuster #f])
-
-   (define (add-circle! x y)
-     (define added (circle x y Default-Diameter 'added))
-     (*circles (cons added (*circles))))
-
-   (define (resize! old-closest new-d)
-     (match-define (circle x y d a) old-closest)
-     (define resized
-       (match a
-         ['added (circle x y new-d `(resized (,d)))]
-         [`(resized . ,old-sizes) (circle x y new-d `(resized ,(cons d old-sizes)))]))
-     (*circles (cons resized (remq old-closest (*circles)))))
-
-   (define (undo)
-     (when (cons? (*circles))
-       (define fst (first (*circles)))
-       (match fst
-         [(circle x y d 'added) (*circles (rest (*circles)))]
-         [(circle x y d `(resized (,r0 . ,sizes)))
-          (*circles (cons (circle x y r0 `(resized (,d))) (rest (*circles))))])
-       (*history (cons fst (*history)))))
-
-   (define (redo)
-     (when (cons? (*history))
-       (define fst (first (*history)))
-       (if (eq? (circle-action fst) 'added)
-           (begin (*circles (cons fst (*circles))) (*history (rest (*history))))
-           (begin (*circles (cons fst (rest (*circles)))) (*history (rest (*history)))))))
-
-   (define (the-closest xm ym (circles (*circles)))
-     (define cdistance (distance xm ym))
-     (define-values (good-circles distance*)
-       (for*/fold ([good-circles '()][distance* '()])
-                  ((c circles) (d (in-value (cdistance c))) #:when (< d (/ (circle-d c) 2)))
-         (values (cons c good-circles) (cons d distance*))))
-     (and (cons? distance*) (first (argmin second (map list good-circles distance*)))))
-
-   (define (is-empty-area xm ym (circles (*circles)))
-     (define dist (distance xm ym))
-     (for/and ((c circles)) (> (dist c) (/ (+ (circle-d c) Default-Diameter) 2))))
-
-   (on (message 'unlock-canvas) (*in-adjuster #f))
-   (on (message 'lock-canvas) (*in-adjuster #t))
-
-   ;; no closest
-   (define (draw!)
-     (send cc draw-circles #f (*circles)))
-
-   (on (message (resize $old-closest $new-d))
-       (resize! old-closest new-d)
-       (draw!))
-
-   (on (message (draw-circles $close $others))
-       (send cc draw-circles close others))
-
-   (on (message (button-press undo-but))
-       (undo)
-       (draw!))
-
-   (on (message (button-press redo-but))
-       (redo)
-       (draw!))
-
-   (on (message (inbound (circle-canvas-event $type $x $y)))
-       (unless (*in-adjuster)
-         (*x x)
-         (*y y)
-         (cond
-           [(eq? 'leave type) (*x #f)]
-           [(eq? 'enter type) (*x 0)]
-           [(and (eq? 'left-down type) (is-empty-area (*x) (*y)))
-            (add-circle! (*x) (*y))
-            (draw!)]
-           [(and (eq? 'right-down type) (the-closest (*x) (*y)))
-            => (λ (tc)
-                 (*in-adjuster #t)
-                 (popup-adjuster tc *circles frame)
-                 (send cc draw-circles tc (*circles)))])))
-   ))
-
-(define (popup-adjuster closest-circle *circles frame)
-  (define pid (gensym 'popup))
-  (send! (popup-menu frame pid "adjuster" 100 100 (list "adjust radius")))
-  (react (stop-when (message (no-popdown-selected pid)) (send! 'unlock-canvas))
-         (stop-when (message (popdown-item-selected pid _)) (adjuster! closest-circle *circles))))
-
-(define (adjuster! closest-circle *circles)
-  (define d0 (circle-d closest-circle))
-  (define frame (spawn-adjuster-dialog closest-circle (remq closest-circle (*circles))))
-  (spawn-adjuster-slider #:parent frame #:init-value d0))
-
-(define adjuster-dialog%
-  (class frame% (init-field closest-circle)
-    (match-define (circle x* y* _d _a) closest-circle)
-
-    (define/augment (on-close)
-      (send-ground-message 'adjuster-closed))
-
-    (super-new [label (format "Adjust radius of circle at (~a,~a)" x* y*)])))
-
-(define (spawn-adjuster-dialog closest-circle others)
-  (match-define (circle x* y* old-d _a) closest-circle)
-  (define dialog
-    (parameterize ((current-eventspace (make-eventspace)))
-      (new adjuster-dialog% [closest-circle closest-circle])))
-  (send dialog show #t)
-  (spawn
-   ;; well, there's only one slider
-   (define/query-value *d old-d (slider@ _ $v) v)
-   (on (message (slider-update _ $v))
-       ;; resize locally while adjusting
-       (send! (draw-circles (circle x* y* (*d) '_dummy_) others)))
-   (on (message (inbound 'adjuster-closed))
-       ;; resize globally
-       (send! 'unlock-canvas)
-       (send! (resize closest-circle (*d)))
-       (stop-current-facet)))
-  (seal dialog))
-
-
-(define (spawn-adjuster-slider #:parent parent
-                               #:init-value init-value)
-  (spawn-slider #:parent parent #:label "" #:min-value 10 #:max-value 100 #:init-value init-value))
-
-;; ---------------------------------------------------------------------------------------------------
-(define frame  (spawn-frame #:label "Circle Drawer" #:width 400))
-(define hpane1 (spawn-horizontal-pane #:parent frame #:min-height 20 #:alignment '(center center)))
-(define undo-but (spawn-button #:label "Undo" #:parent hpane1))
-(define redo-but (spawn-button #:label "Redo" #:parent hpane1))
-(define hpane2 (spawn-horizontal-panel #:parent frame #:min-height 400 #:alignment '(center center)))
-(define canvas (spawn-circle-canvas hpane2 frame undo-but redo-but))
-
-(spawn
- (on (asserted (frame@ frame))
-     (send! (show frame #t))
-     (stop-current-facet)))

racket/syndicate-gui-toolbox/examples/7-GUIS/task-7.rkt

@@ -1,96 +0,0 @@
-#lang syndicate
-
-(require "../../widgets.rkt")
-(require "cells-canvas.rkt")
-(require racket/set racket/list racket/format)
-
-;; a simple spreadsheet (will not check for circularities)
-
-(require 7GUI/task-7-exp)
-(require 7GUI/task-7-view)
-
-;; -----------------------------------------------------------------------------
-(struct formula (formula dependents) #:transparent)
-#; {Formula    =  [formula Exp* || Number || (Setof Ref*)]}
-
-(define (spawn-control frame)
-  (spawn
-   (field [*content  (make-immutable-hash)] ;; [Hashof Ref* Integer]
-          [*formulas (make-immutable-hash)] ;; [Hashof Ref* Formula]
-          )
-
-
-(define-syntax-rule (iff selector e default) (let ([v e]) (if v (selector v) default)))
-(define (get-exp ref*) (iff formula-formula (hash-ref (*formulas) ref* #f) 0))
-(define (get-dep ref*) (iff formula-dependents (hash-ref (*formulas) ref* #f) (set)))
-(define (get-content ref*) (hash-ref (*content) ref* 0))
-
-(local-require 7GUI/should-be-racket)
-(define (set-content! ref* vc)
-  (define current (get-content ref*))
-  (*content (hash-set (*content) ref* vc))
-  (when (and current (not (= current vc)))
-    (when* (get-dep ref*) => propagate-to)))
-
-(define (propagate-to dependents)
-  (for ((d (in-set dependents)))
-    (set-content! d (evaluate (get-exp d) (*content)))))
-
-(define (set-formula! ref* exp*)
-  (define new     (formula exp* (or (get-dep ref*) (set))))
-  (*formulas (hash-set (*formulas) ref* new))
-  (register-with-dependents (depends-on exp*) ref*)
-  (set-content! ref* (evaluate exp* (*content))))
-
-(define (register-with-dependents dependents ref*)
-  (for ((d (in-set dependents)))
-    (*formulas (hash-set (*formulas) d (formula (get-exp d) (set-add (get-dep d) ref*))))))
-
-;; ---------------------------------------------------------------------------------------------------
-;; cells and contents
-(define ((mk-edit title-fmt validator registration source frame) x y)
-  (define cell (list (x->A x) (y->0 y)))
-  (when (and (first cell) (second cell))
-    (react
-     (define value0 (~a (or (source cell) "")))
-     ;; maybe need to make use of queue-callback ?
-     (define dialog (spawn-dialog #:parent #f
-                                  #:style '(close-button)
-                                  #:label (format title-fmt cell)))
-     (define tf (spawn-text-field #:parent dialog
-                                  #:label #f
-                                  #:min-width 200
-                                  #:min-height 80
-                                  #:init-value value0))
-     (on (message (text-field-enter tf $contents))
-         (when* (validator contents)
-                => (lambda (valid)
-                     (stop-current-facet
-                      (send! (show dialog #f))
-                      (registration cell valid)
-                      (send! (update-grid (*content)))))))
-     (on (asserted (dialog@ dialog))
-         (send! (show dialog #t))))))
-
-(define content-edit (mk-edit "content for cell ~a" valid-content set-content! get-content frame))
-
-(define formula-fmt "a formula for cell ~a")
-(define formula-edit (mk-edit formula-fmt string->exp* set-formula! (compose exp*->string get-exp) frame))
-
-;; ---------------------------------------------------------------------------------------------------
-(on (message (single-click $x $y))
-    (content-edit x y))
-(on (message (double-click $x $y))
-    (formula-edit x y))
-(on-start (send! (update-grid (*content))))
-))
-
-;; ---------------------------------------------------------------------------------------------------
-(define frame  (spawn-frame #:label "Cells" #:width (/ WIDTH 2) #:height (/ HEIGHT 3)))
-(define canvas (spawn-cells-canvas frame WIDTH HEIGHT))
-(spawn-control frame)
-
-(spawn
- (on (asserted (frame@ frame))
-     (send! (show frame #t))
-     (stop-current-facet)))

racket/syndicate-gui-toolbox/info.rkt

@@ -1,8 +0,0 @@
-#lang setup/infotab
-
-(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-gui-toolbox/widgets.rkt

@@ -1,387 +0,0 @@
-#lang syndicate
-
-(provide gui-eventspace
-         gui-callback
-         qc
-         spawn-frame
-         spawn-horizontal-pane
-         spawn-horizontal-panel
-         spawn-vertical-pane
-         spawn-text-field
-         spawn-button
-         spawn-choice
-         spawn-gauge
-         spawn-slider
-         spawn-list-box
-         spawn-dialog
-         (struct-out frame@)
-         (struct-out show)
-         (struct-out horizontal-pane@)
-         (struct-out horizontal-panel@)
-         (struct-out vertical-pane@)
-         (struct-out text-field@)
-         (struct-out set-text-field)
-         (struct-out button@)
-         (struct-out button-press)
-         (struct-out set-text-field-background)
-         (struct-out text-field-update)
-         (struct-out text-field-enter)
-         (struct-out choice@)
-         (struct-out choice-selection)
-         (struct-out set-selection)
-         (struct-out enable)
-         (struct-out gauge@)
-         (struct-out set-gauge-value)
-         (struct-out slider@)
-         (struct-out slider-update)
-         (struct-out list-box@)
-         (struct-out list-box-selection)
-         (struct-out set-list-box-choices)
-         (struct-out popup-menu)
-         (struct-out no-popdown-selected)
-         (struct-out popdown-item-selected)
-         (struct-out dialog@))
-
-(require (only-in racket/class
-                  new
-                  send
-                  make-object))
-(require racket/gui/base)
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Eventspace Shennanigans
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(define gui-eventspace (make-parameter (make-eventspace)))
-
-(define (gui-callback thnk)
-  (parameterize ([current-eventspace (gui-eventspace)])
-    (queue-callback thnk)))
-
-(define-syntax-rule (qc expr ...)
-  (gui-callback (lambda () expr ...)))
-
-
-;; an ID is a (Sealof Any)
-;; an Alignment is a (List (U 'left 'center 'right) (U 'top 'center 'bottom))
-
-(message-struct enable (id val))
-
-(assertion-struct frame@ (id))
-(message-struct show (id value))
-(message-struct popup-menu (parent-id id title x y items))
-(message-struct no-popdown-selected (id))
-(message-struct popdown-item-selected (id item))
-
-(assertion-struct horizontal-pane@ (id))
-(assertion-struct vertical-pane@ (id))
-(assertion-struct horizontal-panel@ (id))
-
-(assertion-struct text-field@ (id value))
-(message-struct set-text-field (id value))
-(message-struct set-text-field-background (id color))
-(message-struct text-field-update (id value))
-(message-struct text-field-enter (id value))
-
-(assertion-struct button@ (id))
-(message-struct button-press (id))
-
-(assertion-struct choice@ (id selection))
-(message-struct choice-selection (id val))
-(message-struct set-selection (id idx))
-
-(assertion-struct gauge@ (id))
-(message-struct set-gauge-value (id value))
-
-(assertion-struct slider@ (id value))
-(message-struct slider-update (id value))
-
-(assertion-struct list-box@ (id idx))
-(message-struct list-box-selection (id idx))
-(message-struct set-list-box-choices (id choices))
-
-(assertion-struct dialog@ (id))
-
-(define (enable/disable-handler self my-id)
-  (on (message (enable my-id $val))
-      (qc (send self enable val))))
-
-;; String -> ID
-(define (spawn-frame #:label label
-                     #:width [width #f]
-                     #:height [height #f])
-  (define frame
-    (parameterize ((current-eventspace (gui-eventspace)))
-      (new frame%
-           [label label]
-           [width width]
-           [height height])))
-  (define id (seal frame))
-
-  (define ((on-popdown! pid) self evt)
-    (when (eq? (send evt get-event-type) 'menu-popdown-none)
-      (send-ground-message (no-popdown-selected pid))))
-  (define ((popdown-item! pid i) . _x)
-    (send-ground-message (popdown-item-selected pid i)))
-
-  (spawn
-   (assert (frame@ id))
-   (on (message (show id $val))
-       (qc (send frame show val)))
-   (on (message (popup-menu id $pid $title $x $y $items))
-       (define pm (new popup-menu% [title title] [popdown-callback (on-popdown! pid)]))
-       (for ([i (in-list items)])
-         (new menu-item% [parent pm] [label i] [callback (popdown-item! pid i)]))
-       (qc (send frame popup-menu pm x y))
-       (react (stop-when (message (inbound (no-popdown-selected pid))) (send! (no-popdown-selected pid)))
-              (stop-when (message (inbound (popdown-item-selected pid $i))) (send! (popdown-item-selected pid i))))))
-  id)
-
-;; ID ... -> ID
-(define (spawn-horizontal-pane #:parent parent
-                               #:border [border 0]
-                               #:min-height [min-height #f]
-                               #:alignment [alignment '(left center)])
-  (define parent-component (seal-contents parent))
-  (define pane (new horizontal-pane%
-                    [parent parent-component]
-                    [border border]
-                    [min-height min-height]
-                    [alignment alignment]))
-  (define id (seal pane))
-
-  (spawn
-   (assert (horizontal-pane@ id)))
-
-  id)
-
-;; ID ... -> ID
-(define (spawn-horizontal-panel #:parent parent
-                                #:border [border 0]
-                                #:min-height [min-height #f]
-                                #:alignment [alignment '(left center)])
-  (define parent-component (seal-contents parent))
-  (define panel (new horizontal-panel%
-                     [parent parent-component]
-                     [border border]
-                     [min-height min-height]
-                     [alignment alignment]))
-  (define id (seal panel))
-
-  (spawn
-   (assert (horizontal-panel@ id)))
-
-  id)
-
-;; ID Alignment -> ID
-(define (spawn-vertical-pane #:parent parent
-                             #:alignment [alignment '(center top)])
-  (define parent-component (seal-contents parent))
-  (define pane (new vertical-pane%
-                    [parent parent-component]
-                    [alignment alignment]))
-  (define id (seal pane))
-
-  (spawn
-   (assert (vertical-pane@ id)))
-
-  id)
-
-; ID String String Bool Nat -> ID
-(define (spawn-text-field #:parent parent
-                          #:label label
-                          #:init-value init
-                          #:enabled [enabled? #t]
-                          #:min-width [min-width #f]
-                          #:min-height [min-height #f])
-  (define parent-component (seal-contents parent))
-
-  (define (inject-text-field-update! _ evt)
-    (case (send evt get-event-type)
-      [(text-field)
-       (send-ground-message (text-field-update id (send tf get-value)))]
-      [(text-field-enter)
-       (send-ground-message (text-field-enter id (send tf get-value)))]))
-
-  (define tf (new text-field%
-                  [parent parent-component]
-                  [label label]
-                  [init-value init]
-                  [enabled enabled?]
-                  [min-width min-width]
-                  [min-height min-height]
-                  [callback inject-text-field-update!]))
-  (define id (seal tf))
-
-  (spawn
-   (field [val (send tf get-value)])
-   (assert (text-field@ id (val)))
-   (enable/disable-handler tf id)
-   (on (message (set-text-field id $value))
-       (qc (send tf set-value value))
-       (val value))
-   (on (message (set-text-field-background id $color))
-       (define c (make-object color% color))
-       (qc (send tf set-field-background c)))
-   (on (message (inbound (text-field-update id $value)))
-       (val value)
-       (send! (text-field-update id value)))
-   (on (message (inbound (text-field-enter id $value)))
-       (val value)
-       (send! (text-field-enter id value))))
-
-  id)
-
-;; ID String -> ID
-(define (spawn-button #:parent parent
-                      #:label label)
-  (define (inject-button-press! b e)
-    (send-ground-message (button-press id)))
-  (define parent-component (seal-contents parent))
-  (define but (new button%
-                   [parent parent-component]
-                   [label label]
-                   [callback inject-button-press!]))
-  (define id (seal but))
-
-  (spawn
-   (assert (button@ id))
-   (enable/disable-handler but id)
-   ;; NOTE - this assumes we are one level away from ground
-   (on (message (inbound (button-press id)))
-       (send! (button-press id))))
-
-  id)
-
-;; ID String (Listof String) -> ID
-(define (spawn-choice #:parent parent
-                      #:label label
-                      #:choices choices)
-  (define (inject-selection! c e)
-    (send-ground-message (choice-selection id (send ch get-string-selection))))
-  (define parent-component (seal-contents parent))
-  (define ch (new choice%
-                  [parent parent-component]
-                  [label label]
-                  [choices choices]
-                  [callback inject-selection!]))
-  (define id (seal ch))
-
-  (spawn
-   (field [selection (send ch get-string-selection)])
-   (assert (choice@ id (selection)))
-
-   (enable/disable-handler ch id)
-   (on (message (inbound (choice-selection id $val)))
-       (selection val)
-       (send! (choice-selection id val)))
-   (on (message (set-selection id $idx))
-       (qc (send ch set-selection idx))
-       (selection (send ch get-string-selection))))
-
-  id)
-
-;; ID String Bool Nat -> ID
-(define (spawn-gauge #:parent parent
-                     #:label label
-                     #:enabled [enabled? #t]
-                     #:range [range 100])
-  (define parent-component (seal-contents parent))
-  (define g (new gauge%
-                 [parent parent-component]
-                 [label label]
-                 [enabled enabled?]
-                 [range range]))
-  (define id (seal g))
-
-  (spawn
-   (assert (gauge@ id))
-   (on (message (set-gauge-value id $v))
-       (qc (send g set-value v))))
-
-  id)
-
-;; ID String Nat Nat -> ID
-(define (spawn-slider #:parent parent
-                      #:label label
-                      #:min-value min-value
-                      #:max-value max-value
-                      #:init-value [init-value min-value])
-  (define (inject-slider-event! self evt)
-    (send-ground-message (slider-update id (get))))
-
-  (define parent-component (seal-contents parent))
-  (define s (new slider%
-                 [parent parent-component]
-                 [label label]
-                 [min-value min-value]
-                 [max-value max-value]
-                 [init-value init-value]
-                 [callback inject-slider-event!]))
-  (define id (seal s))
-
-  (define (get) (send s get-value))
-
-  (spawn
-   (field [current (get)])
-   (assert (slider@ id (current)))
-   (on (message (inbound (slider-update id $val)))
-       (current val)
-       (send! (slider-update id val))))
-
-  id)
-
-;; ID (U String #f) (Listof String) ... -> ID
-(define (spawn-list-box #:parent parent
-                        #:label label
-                        #:choices choices
-                        #:min-width [min-width #f]
-                        #:min-height [min-height #f])
-  (define (inject-list-box-selection! self evt)
-    (send-ground-message (list-box-selection id (get))))
-  (define parent-component (seal-contents parent))
-  (define lb (new list-box%
-                  [parent parent-component]
-                  [label label]
-                  [choices choices]
-                  [min-width min-width]
-                  [min-height min-height]
-                  [callback inject-list-box-selection!]))
-  (define id (seal lb))
-  (define (get)
-    (send lb get-selection))
-
-  (spawn
-   (field [selection (get)])
-   (assert (list-box@ id (selection)))
-   (on (message (inbound (list-box-selection id $val)))
-       (selection val)
-       (send! (list-box-selection id val)))
-   (on (message (set-list-box-choices id $val))
-       (qc (send lb set val))
-       (selection (get))))
-
-  id)
-
-(define (spawn-dialog #:label label
-                      #:parent [parent #f]
-                      #:style [style null])
-  (define parent-component (and parent (seal-contents parent)))
-  (define evt-spc (if parent-component
-                      (send parent-component get-eventspace)
-                      (make-eventspace) #;(gui-eventspace)))
-  (define d (parameterize ((current-eventspace evt-spc))
-              (new dialog%
-                   [label label]
-                   [parent parent-component]
-                   [style style])))
-  (define id (seal d))
-
-  (spawn
-   (assert (dialog@ id))
-
-   (on (message (show id $show?))
-       (qc (send d show show?))
-       (unless show? (stop-current-facet))))
-
-  id)

racket/syndicate/actor.rkt

@@ -31,9 +31,6 @@
          retracted
          rising-edge
          (rename-out [core:message message])
-         know
-         forget
-         realize
 
          let-event
 
@@ -61,7 +58,6 @@
          perform-actions!
          flush!
          quit-dataspace!
-         realize!
 
          syndicate-effects-available?
 
@@ -84,7 +80,6 @@
 (require racket/set)
 (require racket/match)
 (require racket/contract)
-(require (only-in racket/list flatten))
 
 (require (for-syntax racket/base))
 (require (for-syntax syntax/parse))
@@ -203,15 +198,10 @@
                endpoints ;; (Hash EID Endpoint)
                stop-scripts ;; (Listof Script) -- IN REVERSE ORDER
                children ;; (Setof FID)
-               previous-knowledge ;; AssertionSet of internal knowledge
-               knowledge ;; AssertionSet of internal knowledge
                ) #:prefab)
 
 (struct endpoint (id patch-fn handler-fn) #:prefab)
 
-(struct internal-knowledge (v) #:prefab)
-(define internal-knowledge-parenthesis (open-parenthesis 1 struct:internal-knowledge))
-
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Script priorities. These are used to ensure that the results of
 ;; some *side effects* are visible to certain pieces of code.
@@ -259,12 +249,6 @@
 ;; Storeof (Constreeof Action)
 (define current-pending-actions (make-store))
 
-;; Storeof Patch
-(define current-pending-internal-patch (make-store))
-
-;; Storeof (Constreeof Action)
-(define current-pending-internal-events (make-store))
-
 ;; Storeof (Vector (Queue Script) ...)
 ;; Mutates the vector!
 (define current-pending-scripts (make-store))
@@ -409,7 +393,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 ...)?"
@@ -424,7 +407,6 @@
        (analyze-pattern stx #'P))
      (quasisyntax/loc stx
        (add-endpoint! #,(source-location->string stx)
-                      #f
                       (lambda ()
                         #,(let ((patch-stx #`(core:assert #,pat)))
                             (if #'w.Pred
@@ -432,22 +414,6 @@
                                 patch-stx)))
                       void))]))
 
-(define-syntax (know stx)
-  (syntax-parse stx
-    [(_ w:when-pred P)
-     (define-values (proj pat bindings _instantiated)
-       (analyze-pattern stx #'P))
-     (quasisyntax/loc stx
-       (add-endpoint!
-        #,(source-location->string stx)
-        #t
-        (lambda ()
-          #,(let ((patch-stx #`(core:assert (internal-knowledge #,pat))))
-              (if #'w.Pred
-                  #`(if w.Pred #,patch-stx patch-empty)
-                  patch-stx)))
-        void))]))
-
 (define (fid-ancestor? fid maybe-ancestor)
   (and (pair? fid) ;; empty fid lists obviously no ancestors at all!
        (or (equal? fid maybe-ancestor)
@@ -488,17 +454,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
@@ -512,7 +474,6 @@
 
 (define (on-event* where proc #:priority [priority *normal-priority*])
   (add-endpoint! where
-                 #f
                  (lambda () patch-empty)
                  (lambda (e _current-interests _synthetic?)
                    (schedule-script! #:priority priority (lambda () (proc e))))))
@@ -528,18 +489,14 @@
 
 (define-syntax (during stx)
   (syntax-parse stx
-    #:literals (know)
-    [(_ (~or (~and K (know P)) P) O ...)
-     (define E-stx  (quasisyntax/loc #'P #,(if (attribute K)
-                                               #'K
-                                               #'(asserted P))))
-     (define R-stx (if (attribute K) #'forget #'retracted))
+    [(_ P O ...)
+     (define E-stx (syntax/loc #'P (asserted P)))
      (define-values (_proj _pat _bindings instantiated)
        (analyze-pattern E-stx #'P))
      (quasisyntax/loc stx
        (on #,E-stx
            (let ((p #,instantiated))
-             (react (stop-when (#,R-stx p))
+             (react (stop-when (retracted p))
                     O ...))))]))
 
 (define-syntax (during/spawn stx)
@@ -590,7 +547,6 @@
      (quasisyntax/loc stx
        (let ()
          (add-endpoint! #,(source-location->string stx)
-                        #f
                         (lambda ()
                           (define subject-id (current-dataflow-subject-id))
                           (schedule-script!
@@ -614,8 +570,6 @@
 (define-syntax (asserted stx) (raise-syntax-error #f "asserted: Used outside event spec" stx))
 (define-syntax (retracted stx) (raise-syntax-error #f "retracted: Used outside event spec" stx))
 (define-syntax (rising-edge stx) (raise-syntax-error #f "rising-edge: Used outside event spec" stx))
-(define-syntax (forget stx) (raise-syntax-error #f "forget: Used outside event spec" stx))
-(define-syntax (realize stx) (raise-syntax-error #f "realize: Used outside event spec" stx))
 
 (define-syntax (suspend-script stx)
   (syntax-parse stx
@@ -803,7 +757,7 @@
   #:macro-definer-name define-event-expander
   #:introducer-parameter-name current-event-expander-introducer
   #:local-introduce-name syntax-local-event-expander-introduce
-  #:expander-form-predicate-name event-expander-form?
+  #:expander-id-predicate-name event-expander-id?
   #:expander-transform-name event-expander-transform)
 
 (provide (for-syntax
@@ -811,132 +765,69 @@
           event-expander?
           event-expander-proc
           syntax-local-event-expander-introduce
-          event-expander-form?
+          event-expander-id?
           event-expander-transform)
          define-event-expander)
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Syntax-time support
 
-(define (interests-pre-and-post-patch pat synthetic? retrieve-knowledge)
+(define (interests-pre-and-post-patch pat synthetic?)
   (define (or* x y) (or x y))
-  (define-values (prev current) (retrieve-knowledge synthetic?))
-  (define old (trie-lookup prev pat #f #:wildcard-union or*))
-  (define new (trie-lookup current pat #f #:wildcard-union or*))
-  (values old new))
-
-(define (interest-just-appeared-matching? pat synthetic? retrieve-knowledge)
-  (define-values (old new) (interests-pre-and-post-patch pat synthetic? retrieve-knowledge))
-  (and (not old) new))
-
-(define (interest-just-disappeared-matching? pat synthetic? retrieve-knowledge)
-  (define-values (old new) (interests-pre-and-post-patch pat synthetic? retrieve-knowledge))
-  (and old (not new)))
-
-;; Bool -> (Values AssertionSet AssertionSet)
-;; retrieve the previous and current knowledge fields from the current actor state
-(define (current-actor-state-knowledges synthetic?)
   (define a (current-actor-state))
   (define previous-knowledge (if synthetic? trie-empty (actor-state-previous-knowledge a)))
-  (define current-knowledge (actor-state-knowledge a))
-  (values previous-knowledge current-knowledge))
+  (define old (trie-lookup previous-knowledge pat #f #:wildcard-union or*))
+  (define new (trie-lookup (actor-state-knowledge a) pat #f #:wildcard-union or*))
+  (values old new))
 
-;; Bool -> (Values AssertionSet AssertionSet)
-;; retrieve the previous and current knowledge fields from the current facet
-(define (current-facet-knowledges synthetic?)
-  (define f (lookup-facet (current-facet-id)))
-  (define previous-knowledge (if synthetic? trie-empty (facet-previous-knowledge f)))
-  (define current-knowledge (facet-knowledge f))
-  (values previous-knowledge current-knowledge))
+(define (interest-just-appeared-matching? pat synthetic?)
+  (define-values (old new) (interests-pre-and-post-patch pat synthetic?))
+  (and (not old) new))
 
-(define-for-syntax (analyze-appear/disappear outer-expr-stx
-                                             when-pred-stx
-                                             event-stx
-                                             script-stx
-                                             asserted?
-                                             P-stx
-                                             priority-stx
-                                             internal?)
-  (define P+
-    (if internal? #`(internal-knowledge #,P-stx) P-stx))
+(define (interest-just-disappeared-matching? pat synthetic?)
+  (define-values (old new) (interests-pre-and-post-patch pat synthetic?))
+  (and old (not new)))
+
+(define-for-syntax (analyze-asserted/retracted outer-expr-stx
+                                               when-pred-stx
+                                               event-stx
+                                               script-stx
+                                               asserted?
+                                               P-stx
+                                               priority-stx)
   (define-values (proj-stx pat bindings _instantiated)
-    (analyze-pattern event-stx P+))
-  (define interest-stx
-    (if internal?
-        #`(patch-seq (core:sub #,pat)
-                     ;; Allow other facets to see our interest
-                     (core:assert (internal-knowledge (observe #,(cadr pat)))))
-        #`(core:sub #,pat)))
+    (analyze-pattern event-stx P-stx))
   (define event-predicate-stx (if asserted? #'patch/added? #'patch/removed?))
   (define patch-accessor-stx (if asserted? #'patch-added #'patch-removed))
   (define change-detector-stx
     (if asserted? #'interest-just-appeared-matching? #'interest-just-disappeared-matching?))
-  (define knowledge-retriever
-    (if internal? #'current-facet-knowledges #'current-actor-state-knowledges))
   (quasisyntax/loc outer-expr-stx
-    (add-endpoint!
-     #,(source-location->string outer-expr-stx)
-     #,internal?
-     (lambda () (if #,when-pred-stx
-                    #,interest-stx
-                    patch-empty))
-     (lambda (e current-interests synthetic?)
-       (when (not (trie-empty? current-interests))
-         (core:match-event e
-           [(? #,event-predicate-stx p)
-            (define proj #,proj-stx)
-            (define proj-arity (projection-arity proj))
-            (define entry-set (trie-project/set #:take proj-arity
-                                                (#,patch-accessor-stx p)
-                                                proj))
-            (when (not entry-set)
-              (error 'asserted
-                     "Wildcard interest discovered while projecting by ~v at ~a"
-                     proj
-                     #,(source-location->string P-stx)))
-            (for [(entry (in-set entry-set))]
-              (let ((instantiated (instantiate-projection proj entry)))
-                (and (#,change-detector-stx instantiated synthetic? #,knowledge-retriever)
-                     (schedule-script!
-                      #:priority #,priority-stx
-                      (lambda ()
-                        (match-define (list #,@bindings) entry)
-                        #,script-stx)))))]))))))
-
-(define-for-syntax (analyze-message outer-expr-stx
-                                    when-pred-stx
-                                    event-stx
-                                    script-stx
-                                    P-stx
-                                    priority-stx
-                                    internal?)
-  (define-values (proj pat bindings _instantiated)
-       (analyze-pattern event-stx P-stx))
-  (define sub
-    (if internal? #`(internal-knowledge #,pat) pat))
-  (define matchp
-    (if internal? #'(internal-knowledge body) #'body))
-  (quasisyntax/loc outer-expr-stx
-    (add-endpoint!
-     #,(source-location->string outer-expr-stx)
-     #,internal?
-     (lambda () (if #,when-pred-stx
-                    (core:sub #,sub)
-                    patch-empty))
-     (lambda (e current-interests _synthetic?)
-       (when (not (trie-empty? current-interests))
-         (core:match-event e
-           [(core:message #,matchp)
-            (define capture-vals
-              (match-value/captures
-               body
-               #,proj))
-            (and capture-vals
-                 (schedule-script!
-                  #:priority #,priority-stx
-                  (lambda ()
-                    (apply (lambda #,bindings #,script-stx)
-                           capture-vals))))]))))))
+    (add-endpoint! #,(source-location->string outer-expr-stx)
+                   (lambda () (if #,when-pred-stx
+                                  (core:sub #,pat)
+                                  patch-empty))
+                   (lambda (e current-interests synthetic?)
+                     (when (not (trie-empty? current-interests))
+                       (core:match-event e
+                         [(? #,event-predicate-stx p)
+                          (define proj #,proj-stx)
+                          (define proj-arity (projection-arity proj))
+                          (define entry-set (trie-project/set #:take proj-arity
+                                                              (#,patch-accessor-stx p)
+                                                              proj))
+                          (when (not entry-set)
+                            (error 'asserted
+                                   "Wildcard interest discovered while projecting by ~v at ~a"
+                                   proj
+                                   #,(source-location->string P-stx)))
+                          (for [(entry (in-set entry-set))]
+                            (let ((instantiated (instantiate-projection proj entry)))
+                              (and (#,change-detector-stx instantiated synthetic?)
+                                   (schedule-script!
+                                    #:priority #,priority-stx
+                                    (lambda ()
+                                      (match-define (list #,@bindings) entry)
+                                      #,script-stx)))))]))))))
 
 (define-for-syntax orig-insp
   (variable-reference->module-declaration-inspector (#%variable-reference)))
@@ -948,9 +839,9 @@
                                   priority-stx)
   (define event-stx (syntax-disarm armed-event-stx orig-insp))
   (syntax-parse event-stx
-    #:literals [core:message asserted retracted rising-edge know forget realize]
-    [expander
-     #:when (event-expander-form? #'expander)
+    #:literals [core:message asserted retracted rising-edge]
+    [(expander args ...)
+     #:when (event-expander-id? #'expander)
      (event-expander-transform
       event-stx
       (lambda (result)
@@ -960,23 +851,33 @@
                        script-stx
                        priority-stx)))]
     [(core:message P)
-     (analyze-message outer-expr-stx when-pred-stx event-stx script-stx
-                      #'P priority-stx #f)]
+     (define-values (proj pat bindings _instantiated)
+       (analyze-pattern event-stx #'P))
+     (quasisyntax/loc outer-expr-stx
+       (add-endpoint! #,(source-location->string outer-expr-stx)
+                      (lambda () (if #,when-pred-stx
+                                     (core:sub #,pat)
+                                     patch-empty))
+                      (lambda (e current-interests _synthetic?)
+                        (when (not (trie-empty? current-interests))
+                          (core:match-event e
+                            [(core:message body)
+                             (define capture-vals
+                               (match-value/captures
+                                body
+                                #,proj))
+                             (and capture-vals
+                                  (schedule-script!
+                                   #:priority #,priority-stx
+                                   (lambda ()
+                                     (apply (lambda #,bindings #,script-stx)
+                                            capture-vals))))])))))]
     [(asserted P)
-     (analyze-appear/disappear outer-expr-stx when-pred-stx event-stx script-stx
-                               #t #'P priority-stx #f)]
+     (analyze-asserted/retracted outer-expr-stx when-pred-stx event-stx script-stx
+                                 #t #'P priority-stx)]
     [(retracted P)
-     (analyze-appear/disappear outer-expr-stx when-pred-stx event-stx script-stx
-                               #f #'P priority-stx #f)]
-    [(realize P)
-     (analyze-message outer-expr-stx when-pred-stx event-stx script-stx
-                      #'P priority-stx #t)]
-    [(know P)
-     (analyze-appear/disappear outer-expr-stx when-pred-stx event-stx script-stx
-                               #t #'P priority-stx #t)]
-    [(forget P)
-     (analyze-appear/disappear outer-expr-stx when-pred-stx event-stx script-stx
-                               #f #'P priority-stx #t)]
+     (analyze-asserted/retracted outer-expr-stx when-pred-stx event-stx script-stx
+                                 #f #'P priority-stx)]
     [(rising-edge Pred)
      (define field-name
        (datum->syntax event-stx
@@ -986,7 +887,6 @@
        (let ()
          (field [#,field-name #f])
          (add-endpoint! #,(source-location->string outer-expr-stx)
-                        #f
                         (lambda ()
                           (when #,when-pred-stx
                             (define old-val (#,field-name))
@@ -1103,30 +1003,14 @@
     (current-pending-actions (list (current-pending-actions)
                                    ((current-action-transformer) p)))))
 
-(define (schedule-internal-event! ac)
-  (if (patch? ac)
-      (when (patch-non-empty? ac)
-        (current-pending-internal-patch (compose-patch ac (current-pending-internal-patch))))
-      (begin (flush-pending-internal-patch!)
-             (current-pending-internal-events (list (current-pending-internal-events)
-                                                     ((current-action-transformer) ac))))))
-
-(define (flush-pending-internal-patch!)
-  (define p (current-pending-internal-patch))
-  (when (patch-non-empty? p)
-    (current-pending-internal-patch patch-empty)
-    (current-pending-internal-events (list (current-pending-internal-events)
-                                            ((current-action-transformer) p)))))
-
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; 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!)
+(define (add-endpoint! where patch-fn handler-fn)
+  (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))
@@ -1146,9 +1030,7 @@
                                       (hash-set (facet-endpoints f)
                                                 new-eid
                                                 (endpoint new-eid patch-fn handler-fn))]))))
-  (if internal?
-      (schedule-internal-event! delta-aggregate)
-      (schedule-action! delta-aggregate)))
+  (schedule-action! delta-aggregate))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Facet Lifecycle
@@ -1163,7 +1045,7 @@
   (define fid-uid next-fid-uid)
   (define fid (cons fid-uid parent-fid))
   (set! next-fid-uid (+ next-fid-uid 1))
-  (update-facet! fid (lambda (_f) (facet fid (hasheqv) '() (set) trie-empty trie-empty)))
+  (update-facet! fid (lambda (_f) (facet fid (hasheqv) '() (set))))
   (update-facet! parent-fid
                  (lambda (pf)
                    (and pf (struct-copy facet pf
@@ -1212,21 +1094,8 @@
          (dataflow-forget-subject! (actor-state-field-dataflow a) (list fid eid))
          (define-values (new-mux _eid _delta delta-aggregate)
            (mux-remove-stream (actor-state-mux a) eid))
-         (define-values (internal external) (split-internal/external delta-aggregate))
-         (current-actor-state (struct-copy actor-state a
-                                           [mux new-mux]))
-         (schedule-script!
-          #:priority *gc-priority*
-          ;; need to do this later for the forget change detector
-          (lambda ()
-            (define a (current-actor-state))
-            (define new-knowledge
-              (apply-patch (actor-state-knowledge a) internal))
-            (current-actor-state (struct-copy actor-state a
-                                              [knowledge new-knowledge]))))
-
-         (schedule-internal-event! internal)
-         (schedule-action! external))))
+         (current-actor-state (struct-copy actor-state a [mux new-mux]))
+         (schedule-action! delta-aggregate))))
 
     (schedule-script!
      #:priority *gc-priority*
@@ -1255,8 +1124,6 @@
                              (make-dataflow-graph)))
                (current-pending-patch patch-empty)
                (current-pending-actions '())
-               (current-pending-internal-patch patch-empty)
-               (current-pending-internal-events '())
                (current-pending-scripts (make-empty-pending-scripts))
                (current-action-transformer values)]
     (with-current-facet '() #f
@@ -1284,7 +1151,6 @@
   (when script
     (script)
     (refresh-facet-assertions!)
-    (dispatch-internal-events!)
     (run-all-pending-scripts!)))
 
 (define (run-scripts!)
@@ -1296,20 +1162,6 @@
       (core:quit pending-actions)
       (core:transition (current-actor-state) pending-actions)))
 
-;; dispatch the internal events that have accumulated during script execution
-(define (dispatch-internal-events!)
-  (flush-pending-internal-patch!)
-  (define pending (flatten (current-pending-internal-events)))
-  (current-pending-internal-events '())
-  (define a (current-actor-state))
-  (for* ([e (in-list pending)]
-         [(fid f) (in-hash (actor-state-facets a))])
-    (when (patch? e)
-      (define a (current-actor-state))
-      (current-actor-state (struct-copy actor-state a
-                                        [knowledge (apply-patch (actor-state-knowledge a) e)])))
-    (facet-handle-event! fid f e #f)))
-
 (define (refresh-facet-assertions!)
   (dataflow-repair-damage! (actor-state-field-dataflow (current-actor-state))
                            (lambda (subject-id)
@@ -1337,9 +1189,7 @@
   (define-values (new-mux _eid _delta delta-aggregate)
     (mux-update-stream (actor-state-mux a) eid patch))
   (current-actor-state (struct-copy actor-state a [mux new-mux]))
-  (define-values (internal external) (split-internal/external delta-aggregate))
-  (schedule-internal-event! internal)
-  (schedule-action! external))
+  (schedule-action! delta-aggregate))
 
 (define (actor-behavior e a)
   (and e
@@ -1347,12 +1197,10 @@
                      (if (patch? e)
                          (struct-copy actor-state a
                                       [previous-knowledge (actor-state-knowledge a)]
-                                      [knowledge (apply-patch (actor-state-knowledge a) e)])
+                                      [knowledge (update-interests (actor-state-knowledge a) e)])
                          a))
                     (current-pending-patch patch-empty)
                     (current-pending-actions '())
-                    (current-pending-internal-patch patch-empty)
-                    (current-pending-internal-events '())
                     (current-pending-scripts (make-empty-pending-scripts))
                     (current-action-transformer values)]
          (for [((fid f) (in-hash (actor-state-facets a)))]
@@ -1362,14 +1210,6 @@
 (define (facet-handle-event! fid f e synthetic?)
   (define mux (actor-state-mux (current-actor-state)))
   (with-current-facet fid #f
-    (when (patch? e)
-      (define internal (internal-patch e))
-      (update-facet! fid
-                     (lambda (f)
-                       (and f
-                            (struct-copy facet f
-                                         [previous-knowledge (facet-knowledge f)]
-                                         [knowledge (apply-patch (facet-knowledge f) internal)])))))
     (for [(ep (in-hash-values (facet-endpoints f)))]
       ((endpoint-handler-fn ep) e (mux-interests-of mux (endpoint-id ep)) synthetic?))))
 
@@ -1466,10 +1306,6 @@
   (ensure-in-script! 'send!)
   (schedule-action! (core:message M)))
 
-(define (realize! M)
-  (ensure-in-script! 'realize!)
-  (schedule-internal-event! (core:message (internal-knowledge M))))
-
 (define *adhoc-label* -1)
 
 (define (assert! P)
@@ -1501,23 +1337,6 @@
   (ensure-in-script! 'quit-dataspace!)
   (schedule-action! (core:quit-dataspace)))
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Helpers
-
-;; Patch -> (Values Patch Patch)
-;; split a patch into its internal and external components
-(define (split-internal/external e)
-  (define internal (internal-patch e))
-  (values internal
-          (patch (trie-subtract (patch-added e) (patch-added internal))
-                 (trie-subtract (patch-removed e) (patch-removed internal)))))
-
-;; Patch -> Patch
-;; Remove all items from a patch not constructed with internal-knowledge
-(define (internal-patch e)
-  (patch-prepend internal-knowledge-parenthesis
-                 (patch-step e internal-knowledge-parenthesis)))
-
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 (define (format-field-descriptor d)
@@ -1533,7 +1352,7 @@
   (fprintf p " - Knowledge:\n   ~a" (trie->pretty-string knowledge #:indent 3))
   (fprintf p " - Facets:\n")
   (for ([(fid f) (in-hash facets)])
-    (match-define (facet _fid endpoints _ children _ _) f)
+    (match-define (facet _fid endpoints _ children) f)
     (fprintf p "    ---- facet ~a, children=~a" fid (set->list children))
     (when (not (hash-empty? endpoints))
       (fprintf p ", endpoints=~a" (hash-keys endpoints)))

racket/syndicate/core-lang.rkt

@@ -2,13 +2,11 @@
 
 (require (for-syntax racket/base syntax/kerncase))
 (require (for-syntax syntax/parse))
-(require (for-syntax (only-in racket/list make-list)))
 
 (require racket/match)
 (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
@@ -49,35 +47,7 @@
      ;; the inclusion of (module+ syndicate-main) is because it seems that the appearance order
      ;; of module+ forms determines the mutual visibility. So syndicate-main is ensured to be the
      ;; first module+ and consequently the main submodule can require it.
-     #'(#%module-begin
-        (syndicate-module () ((module+ syndicate-main)
-                              (module+ main (current-ground-dataspace run-ground))
-                              forms ...)))]))
-
-;; Identifier -> Bool
-;; Is the identifier a form that shouldn't capture actor actions?
-;; note the absence of define-values
-(define-for-syntax (kernel-id? x)
-  (ormap (lambda (i) (free-identifier=? x i))
-         (syntax->list #'(require
-                          provide
-                          define-values
-                          define-syntaxes
-                          begin-for-syntax
-                          module
-                          module*
-                          module+
-                          #%require
-                          #%provide
-                          #%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)
+     #'(#%module-begin (syndicate-module () ((module+ syndicate-main) forms ...)))]))
 
 (define-syntax (syndicate-module stx)
   (syntax-parse stx
@@ -88,29 +58,27 @@
                                                    #'begin-for-declarations)
                                              (kernel-form-identifier-list))))
      (syntax-parse expanded
-       #:literals (begin define-values)
+       #:literals (begin)
        [(begin more-forms ...)
         #'(syndicate-module (action-ids ...) (more-forms ... forms ...))]
-       [(define-values (x:id ...) e)
-        #:with action-id (car (generate-temporaries (list #'form)))
-        #:with (tmp ...) (generate-temporaries #'(x ...))
-        #`(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)))))
-            (define-values (x ...) (values tmp ...))
-            (syndicate-module (action-ids ... action-id) (forms ...)))]
        [(head rest ...)
-        (cond
-          [(kernel-id? #'head)
-           #`(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 ...))))])]
+        (if (ormap (lambda (i) (free-identifier=? #'head i))
+                   (syntax->list #'(require
+                                     provide
+                                     define-values
+                                     define-syntaxes
+                                     begin-for-syntax
+                                     module
+                                     module*
+                                     module+
+                                     #%require
+                                     #%provide
+                                     #%declare
+                                     begin-for-declarations)))
+            #`(begin #,expanded (syndicate-module (action-ids ...) (forms ...)))
+            (with-syntax ([action-id (car (generate-temporaries (list #'form)))])
+              #`(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 ...) ())
@@ -123,6 +91,8 @@
                          (when (not activated?)
                            (set! activated? #t)
                            boot-actions)))
+                     (module+ main
+                       (current-ground-dataspace run-ground))
                      (module+ main
                        (require (submod ".." syndicate-main))
                        ((current-ground-dataspace) (activate!))))])

racket/syndicate/drivers/websocket.rkt

@@ -215,19 +215,16 @@
 
 (define (spawn-connection local-addr remote-addr id c control-ch)
   (actor #:name (list 'drivers/websocket:connect local-addr remote-addr id)
-         #:assertions*
-         (patch-added
-          (patch-seq
-           (let-values (((la lp ra rp) (ws-conn-peer-addresses c)))
-             (assert (websocket-peer-details local-addr remote-addr la lp ra rp)))
-           (sub (observe (websocket-message remote-addr local-addr ?))) ;; monitor peer
-           (pub (websocket-message remote-addr local-addr ?)) ;; may send messages to peer
-           (sub (websocket-message local-addr remote-addr ?)) ;; want segments from peer
-           (sub (inbound (websocket-incoming-message id ?))) ;; segments from driver thd
-           ))
          websocket-connection-behaviour
-         (connection-state local-addr remote-addr c control-ch)
-         '()))
+	 (connection-state local-addr remote-addr c control-ch)
+         (patch-seq
+          (let-values (((la lp ra rp) (ws-conn-peer-addresses c)))
+            (assert (websocket-peer-details local-addr remote-addr la lp ra rp)))
+          (sub (observe (websocket-message remote-addr local-addr ?))) ;; monitor peer
+          (pub (websocket-message remote-addr local-addr ?)) ;; may send messages to peer
+          (sub (websocket-message local-addr remote-addr ?)) ;; want segments from peer
+          (sub (inbound (websocket-incoming-message id ?))) ;; segments from driver thd
+          )))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 

racket/syndicate/examples/actor/flink.rkt

@@ -1,619 +0,0 @@
-#lang syndicate
-
-(require racket/set)
-(require (only-in racket/list
-                  first
-                  partition
-                  empty?
-                  split-at))
-(require (only-in racket/hash
-                  hash-union))
-(require (only-in racket/string
-                  string-split
-                  string-trim))
-(require (only-in racket/sequence
-                  sequence->list))
-(require (only-in racket/function const))
-
-(module+ test
-  (require rackunit))
-
-;; ---------------------------------------------------------------------------------------------------
-;; Protocol
-
-#|
-Conversations in the flink dataspace primarily concern two topics: presence and
-task execution.
-
-Presence Protocol
------------------
-
-The JobManager (JM) asserts its presence with (job-manager-alive). The operation
-of each TaskManager (TM) is contingent on the presence of a job manager.
-|#
-(assertion-struct job-manager-alive ())
-#|
-In turn, TaskManagers advertise their presence with (task-manager ID slots),
-where ID is a unique id, and slots is a natural number. The number of slots
-dictates how many tasks the TM can take on. To reduce contention, the JM
-should only assign a task to a TM if the TM actually has the resources to
-perform a task.
-|#
-(assertion-struct task-manager (id slots))
-;; an ID is a symbol or a natural number.
-;; Any -> Bool
-;; recognize IDs
-(define (id? x)
-  (or (symbol? x) (exact-nonnegative-integer? x)))
-#|
-The resources available to a TM are its associated TaskRunners (TRs). TaskRunners
-assert their presence with (task-runner ID)
-
-|#
-(assertion-struct task-runner (id))
-#|
-a Status is one of
-- IDLE, when the TR is not executing a task
-- (executing ID), when the TR is executing the task with the given ID
-- OVERLOAD, when the TR has been asked to perform a task before it has
-finished its previous assignment. For the purposes of this model, it indicates a
-failure in the protocol; like the exchange between the JM and the TM, a TR
-should only receive tasks when it is IDLE.
-|#
-(define IDLE 'idle)
-(define OVERLOAD 'overload)
-(struct executing (id) #:transparent)
-
-#|
-Task Delegation Protocol
------------------------
-
-Task Delegation has two roles, TaskAssigner (TA) and TaskPerformer (TP).
-
-A TaskAssigner requests the performance of a Task with a particular TaskPerformer
-through the assertion of interest
-    (observe (task-performance ID Task ★))
-where the ID identifies the TP
-|#
-(assertion-struct task-performance (assignee task desc))
-#|
-A Task is a (task TaskID Work), where Work is one of
-  - (map-work String)
-  - (reduce-work (U ID TaskResult) (U ID TaskResult)), referring to either the
-    ID of the dependent task or its results. A reduce-work is ready to be executed
-    when it has both results.
-
-A TaskID is a (list ID ID), where the first ID is specific to the individual
-task and the second identifies the job it belongs to.
-
-A TaskResult is a (Hashof String Natural), counting the occurrences of words
-|#
-(struct task (id desc) #:transparent)
-(struct map-work (data) #:transparent)
-(struct reduce-work (left right) #:transparent)
-
-#|
-The TaskPerformer responds to a request by describing its state with respect
-to that task,
-    (task-performance ID Task TaskStateDesc)
-
-A TaskStateDesc is one of
-  - ACCEPTED, when the TP has the resources to perform the task. (TODO - not sure if this is ever visible, currently)
-  - OVERLOAD, when the TP does not have the resources to perform the task.
-  - RUNNING, indicating that the task is being performed
-  - (finished TaskResult), describing the results
-|#
-(struct finished (data) #:transparent)
-(define ACCEPTED 'accepted)
-(define RUNNING 'running)
-#|
-Two instances of the Task Delegation Protocol take place: one between the
-JobManager and the TaskManager, and one between the TaskManager and its
-TaskRunners.
-|#
-
-#|
-Job Submission Protocol
------------------------
-
-Finally, Clients submit their jobs to the JobManager by asserting interest
-    (observe (job-completion ID (Listof Task) ★))
-
-The JobManager then performs the job and, when finished, asserts
-    (job-completion ID (Listof Task) TaskResults)
-|#
-(struct job (id tasks) #:transparent)
-(assertion-struct job-completion (id data result))
-
-;; ---------------------------------------------------------------------------------------------------
-;; Logging
-
-(define (log fmt . args)
-  (displayln (apply format fmt args)))
-
-;; ---------------------------------------------------------------------------------------------------
-;; Generic Implementation of Task Delegation Protocol
-
-;; a TaskFun is a
-;; (Task ID (TaskResults -> Void) ((U ACCEPTED OVERLOAD RUNNING) -> Void) -> Void)
-
-;; ID (-> Bool) TaskFun -> TaskPerformer
-;; doesn't really account for long-running tasks
-;; gonna need some effect polymorphism to type uses of this
-(define (task-performer my-id can-accept? perform-task)
-  (react
-   (during (observe (task-performance my-id $task _))
-     (field [status #f])
-     (assert (task-performance my-id task (status)))
-     (cond
-       [(can-accept?)
-        (status RUNNING)
-        (define (on-complete results)
-          (status (finished results)))
-        (perform-task task on-complete status)]
-       [else
-        (status OVERLOAD)]))))
-
-;; Task
-;; ID
-;; (-> Void)
-;; (TaskResults -> Void)
-;; -> TaskAssigner
-(define (task-assigner tsk performer on-overload! on-complete!)
-  (react
-   (on (asserted (task-performance performer tsk $status))
-       (match status
-         [(or (== ACCEPTED)
-              (== RUNNING))
-          (void)]
-         [(== OVERLOAD)
-          (stop-current-facet (on-overload!))]
-         [(finished results)
-          (stop-current-facet (on-complete! results))]))))
-
-;; ---------------------------------------------------------------------------------------------------
-;; TaskRunner
-;; ID ID -> Spawn
-(define (spawn-task-runner id tm-id)
-  (spawn #:name id
-   (assert (task-runner id))
-   (stop-when (retracted (task-manager tm-id _)))
-   ;; Task (TaskStateDesc -> Void) -> Void
-   (define (perform-task tsk on-complete! update-status!)
-     (match-define (task tid desc) tsk)
-     (match desc
-       [(map-work data)
-        (define wc (count-new-words (hash) (string->words data)))
-        (on-complete! wc)]
-       [(reduce-work left right)
-        (define wc (hash-union left right #:combine +))
-        (on-complete! wc)]))
-   (on-start
-    (task-performer id (const #t) perform-task))))
-
-;; (Hash String Nat) String -> (Hash String Nat)
-(define (word-count-increment h word)
-  (hash-update h
-               word
-               add1
-               (λ x 0)))
-
-;; (Hash String Nat) (Listof String) -> (Hash String Nat)
-(define (count-new-words word-count words)
-  (for/fold ([result word-count])
-            ([word words])
-    (word-count-increment result word)))
-
-;; String -> (Listof String)
-;; Return the white space-separated words, trimming off leading & trailing punctuation
-(define (string->words s)
-  (map (lambda (w) (string-trim w #px"\\p{P}")) (string-split s)))
-
-(module+ test
-  (check-equal? (string->words "good day sir")
-                (list "good" "day" "sir"))
-  (check-equal? (string->words "")
-                (list))
-  (check-equal? (string->words "good eve ma'am")
-                (list "good" "eve" "ma'am"))
-  (check-equal? (string->words "please sir. may I have another?")
-                (list "please" "sir" "may" "I" "have" "another"))
-  ;; currently fails, doesn't seem worth fixing
-  #;(check-equal? (string->words "but wait---there's more")
-                (list "but" "wait" "there's" "more")))
-
-;; ---------------------------------------------------------------------------------------------------
-;; TaskManager
-
-;; PosInt -> Spawn
-(define (spawn-task-manager num-task-runners)
-  (define id (gensym 'task-manager))
-  (spawn #:name id
-   (log "Task Manager (TM) ~a is running" id)
-   (during (job-manager-alive)
-     (log "TM ~a learns about JM" id)
-
-     (field [task-runners (set)])
-
-     ;; Create & Monitor Task Runners
-     (on-start
-      (for ([_ (in-range num-task-runners)])
-        (define tr-id (gensym 'task-runner))
-        (react
-         (on-start (spawn-task-runner tr-id id))
-         (on (asserted (task-runner tr-id))
-             (log "TM ~a successfully created task-runner ~a" id tr-id)
-             (task-runners (set-add (task-runners) tr-id)))
-         (on (retracted (task-runner tr-id))
-             (log "TM ~a detected failure of task runner ~a, restarting" id tr-id)
-             (task-runners (set-remove (task-runners) tr-id))
-             (spawn-task-runner tr-id id)))))
-
-     ;; Assign incoming tasks
-     (field [busy-runners (set)])
-
-     (define (idle-runners)
-       (set-count (set-subtract (task-runners) (busy-runners))))
-
-     (assert (task-manager id (idle-runners)))
-
-     (define (can-accept?)
-       (positive? (idle-runners)))
-     (define (select-runner)
-       (define runner (for/first ([r (in-set (task-runners))]
-                                  #:unless (set-member? (busy-runners) r))
-                        r))
-       (unless runner
-         (log "ERROR: TM ~a failed to select a runner.\nrunners: ~a\nbusy: ~a" id (task-runners) (busy-runners)))
-       (busy-runners (set-add (busy-runners) runner))
-       runner)
-     (define (perform-task tsk on-complete! update-status!)
-       (match-define (task task-id desc) tsk)
-       (define runner (select-runner))
-       (log "TM ~a assigns task ~a to runner ~a" id task-id runner)
-       (on-stop (busy-runners (set-remove (busy-runners) runner)))
-       (on-start
-        (task-assigner tsk runner
-                      (lambda () (update-status! OVERLOAD))
-                      (lambda (results) (on-complete! results)))))
-     (on-start
-      (task-performer id can-accept? perform-task)))))
-
-;; ---------------------------------------------------------------------------------------------------
-;; JobManager
-
-;; assertions used for internal slot-management protocol
-(assertion-struct slots (v))
-(assertion-struct slot-assignment (who mngr))
-;; tid is the TaskID, rid is a unique symbol to a particular request for a slot
-(struct request-id (tid rid) #:prefab)
-
-(message-struct task-is-ready (job-id task))
-
-(define (spawn-job-manager)
-  (spawn
-    (assert (job-manager-alive))
-    (log "Job Manager Up")
-
-    (on-start
-      (react
-
-        ;; keep track of task managers, how many slots they say are open, and how many tasks we have assigned.
-        ;; (Hashof TaskManagerID Nat)
-        (define/query-hash task-managers (task-manager $id $slots) id slots
-          #:on-add (log "JM learns that ~a has ~v slots" id slots))
-
-        (field [requests-in-flight (hash)] ;; (Hashof ID Nat)
-               [assignments (hash)]) ;; (Hashof ID ID) request ID to manager ID
-
-        ;; to better understand the supply of slots for each task manager, keep track of the number
-        ;; of requested tasks that we have yet to hear back about
-        (define (slots-available)
-          (for/sum ([(id v) (in-hash (task-managers))])
-            (max 0 (- v (hash-ref (requests-in-flight) id 0)))))
-
-        ;; ID -> (U #f ID)
-        (define (try-take-slot! me)
-          (define mngr
-            (for/first ([(id slots) (in-hash (task-managers))]
-                        #:when (positive? (- slots (hash-ref (requests-in-flight) id 0))))
-              id))
-          (when mngr
-            (assignments (hash-set (assignments) me mngr))
-            (requests-in-flight (hash-update (requests-in-flight) mngr add1 0)))
-          mngr)
-
-        (know (slots (slots-available)))
-
-        (during (know (observe (slot-assignment (request-id $tid $who) _)))
-          (on-start
-           (react
-            ;; what if one manager gains a slot but another loses one, so n stays the same?
-            (on (know (slots $n))
-              #;(log "Dispatcher request ~a learns there are ~a slots" tid n)
-              (unless (or (zero? n) (hash-has-key? (assignments) who))
-                (define mngr (try-take-slot! who))
-                (when mngr
-                  (stop-current-facet
-                   (log "Dispatcher assigns task ~a to ~a" tid mngr)
-                   (react (know (slot-assignment (request-id tid who) mngr)))
-                   (react
-                    (define waiting-for-answer (current-facet-id))
-                    (on (asserted (observe (task-performance mngr (task tid $x) _)))
-                        (react (on (asserted (task-performance mngr (task tid x) _))
-                                   (log "Dispatcher sees answer for ~a" tid)
-                                   (stop-facet waiting-for-answer))))
-                    (on-stop
-                     (requests-in-flight (hash-update (requests-in-flight) mngr sub1))))))))))
-          (on-stop (assignments (hash-remove (assignments) who))))))
-
-    (during (observe (job-completion $job-id $tasks _))
-      (log "JM receives job ~a" job-id)
-      (define-values (ready not-ready) (partition task-ready? tasks))
-      (field [waiting-tasks not-ready]
-             [tasks-in-progress 0])
-
-      (on-start (for [(t ready)] (add-ready-task! t)))
-      (on (realize (task-is-ready job-id $t))
-          (perform-task t push-results))
-
-      ;; Task -> Void
-      (define (add-ready-task! t)
-        ;; TODO - use functional-queue.rkt from ../../
-        (log "JM marks task ~a as ready" (task-id t))
-        (realize! (task-is-ready job-id t)))
-
-      ;; Task (ID TaskResult -> Void) -> Void
-      ;; Requires (task-ready? t)
-      (define (perform-task t k)
-        (react
-         (define task-facet (current-facet-id))
-         (on-start (tasks-in-progress (add1 (tasks-in-progress))))
-         (on-stop (tasks-in-progress (sub1 (tasks-in-progress))))
-         (match-define (task this-id desc) t)
-         (log "JM begins on task ~a" this-id)
-
-
-         (define (select-a-task-manager)
-           (react
-            (define req-id (gensym 'perform-task))
-            (on (know (slot-assignment (request-id this-id req-id) $mngr))
-                (assign-task mngr))))
-
-         ;; ID -> ...
-         (define (assign-task mngr)
-           (define this-facet (current-facet-id))
-           (react
-            #;(define this-facet (current-facet-id))
-            (on (retracted (task-manager mngr _))
-                ;; our task manager has crashed
-                (stop-current-facet (select-a-task-manager)))
-            (on-start
-             (log "JM assigns task ~a to manager ~a" this-id mngr)
-             (task-assigner t mngr
-                            (lambda ()
-                              ;; need to find a new task manager
-                              ;; don't think we need a release-slot! here, because if we've heard back from a task manager,
-                              ;; they should have told us a different slot count since we tried to give them work
-                              (log "JM overloaded manager ~a with task ~a" mngr this-id)
-                              (stop-facet this-facet (select-a-task-manager)))
-                            (lambda (results)
-                              (log "JM receives the results of task ~a" this-id)
-                              (stop-facet task-facet (k (first this-id) results)))))))
-
-         (on-start (select-a-task-manager))))
-
-      ;; ID Data -> Void
-      ;; Update any dependent tasks with the results of the given task, moving
-      ;; them to the ready queue when possible
-      (define (push-results task-id data)
-        (cond
-          ;; this is an interesting scenario wrt stop handlers running; this code is assuming
-          ;; it runs after the on-stop above that decrements `tasks-in-progress`
-          [(and (zero? (tasks-in-progress))
-                (empty? (waiting-tasks)))
-           (log "JM finished with job ~a" job-id)
-           (react (assert (job-completion job-id tasks data)))]
-          [else
-           ;; TODO - in MapReduce, there should be either 1 waiting task, or 0, meaning the job is done.
-           (define still-waiting
-             (for/fold ([ts '()])
-                       ([t (in-list (waiting-tasks))])
-               (define t+ (task+data t task-id data))
-               (cond
-                 [(task-ready? t+)
-                  (add-ready-task! t+)
-                  ts]
-                 [else
-                  (cons t+ ts)])))
-           (waiting-tasks still-waiting)]))
-      #f)))
-
-;; Task -> Bool
-;; Test if the task is ready to run
-(define (task-ready? t)
-  (match t
-    [(task _ (reduce-work l r))
-     (not (or (id? l) (id? r)))]
-    [_ #t]))
-
-;; Task Id Any -> Task
-;; If the given task is waiting for this data, replace the waiting ID with the data
-(define (task+data t id data)
-  (match t
-    [(task tid (reduce-work (== id) r))
-     (task tid (reduce-work data r))]
-    [(task tid (reduce-work l (== id)))
-     (task tid (reduce-work l data))]
-    [_ t]))
-
-
-;; (Listof A) Nat -> (Values (Listof A) (Listof A))
-;; like split-at but allow a number larger than the length of the list
-(define (split-at/lenient lst n)
-  (split-at lst (min n (length lst))))
-
-;; ---------------------------------------------------------------------------------------------------
-;; Client
-
-;; Job -> Void
-(define (spawn-client j)
-  (spawn
-   (on (asserted (job-completion (job-id j) (job-tasks j) $data))
-       (printf "job done!\n~a\n" data))))
-
-;; ---------------------------------------------------------------------------------------------------
-;; Observe interaction between task and job manager
-
-(define (spawn-observer)
-  (spawn
-   (during (job-manager-alive)
-     (during (task-manager $tm-id _)
-       (define/query-set requests (observe (task-performance tm-id (task $tid _) _)) tid)
-       (field [high-water-mark 0])
-       (on (asserted (task-manager tm-id $slots))
-           (when (> slots (high-water-mark))
-             (high-water-mark slots)))
-       (begin/dataflow
-         (when (> (set-count (requests)) (high-water-mark))
-           (log "!! DEMAND > SUPPLY !!")))))))
-
-;; ---------------------------------------------------------------------------------------------------
-;; Creating a Job
-
-;; (Listof WorkDesc) -> (Values (Listof WorkDesc) (Optionof WorkDesc))
-;; Pair up elements of the input list into a list of reduce tasks, and if the input list is odd also
-;; return the odd-one out.
-;; Conceptually, it does something like this:
-;;   '(a b c d) => '((a b) (c d))
-;;   '(a b c d e) => '((a b) (c d) e)
-(define (pair-up ls)
-  (let loop ([ls ls]
-             [reductions '()])
-    (match ls
-      ['()
-       (values reductions #f)]
-      [(list x)
-       (values reductions x)]
-      [(list-rest x y more)
-       (loop more (cons (reduce-work x y) reductions))])))
-
-
-;; a TaskTree is one of
-;;   (map-work data)
-;;   (reduce-work TaskTree TaskTree)
-
-;; (Listof String) -> TaskTree
-;; Create a tree structure of tasks
-(define (create-task-tree lines)
-  (define map-works
-    (for/list ([line (in-list lines)])
-      (map-work line)))
-  ;; build the tree up from the leaves
-  (let loop ([nodes map-works])
-    (match nodes
-      ['()
-       ;; input was empty
-       (map-work "")]
-      [(list x)
-       x]
-      [_
-       (define-values (reductions left-over?)
-         (pair-up nodes))
-       (loop (if left-over?
-                 (cons left-over? reductions)
-                 reductions))])))
-
-;; TaskTree -> (Listof Task)
-;; flatten a task tree by assigning job-unique IDs
-(define (task-tree->list tt job-id)
-  (define-values (tasks _)
-    ;; TaskTree ID -> (Values (Listof Task) ID)
-    ;; the input id is for the current node of the tree
-    ;; returned id is the "next available" id, given ids are assigned in strict ascending order
-    (let loop ([tt tt]
-               [next-id 0])
-      (match tt
-        [(map-work _)
-         (values (list (task (list next-id job-id) tt))
-                       (add1 next-id))]
-        [(reduce-work left right)
-         (define left-id (add1 next-id))
-         (define-values (lefts right-id)
-           (loop left left-id))
-         (define-values (rights next)
-           (loop right right-id))
-         (values (cons (task (list next-id job-id) (reduce-work left-id right-id))
-                       (append lefts rights))
-                 next)])))
-  tasks)
-
-;; InputPort -> Job
-(define (create-job in)
-  (define job-id (gensym 'job))
-  (define input-lines (sequence->list (in-lines in)))
-  (define tasks (task-tree->list (create-task-tree input-lines) job-id))
-  (job job-id tasks))
-
-;; String -> Job
-(define (string->job s)
-  (create-job (open-input-string s)))
-
-;; PathString -> Job
-(define (file->job path)
-  (define in (open-input-file path))
-  (define j (create-job in))
-  (close-input-port in)
-  j)
-
-(module+ test
-  (test-case
-      "two-line job parsing"
-    (define input "a b c\nd e f")
-    (define j (string->job input))
-    (check-true (job? j))
-    (match-define (job jid tasks) j)
-    (check-true (id? jid))
-    (check-true (list? tasks))
-    (check-true (andmap task? tasks))
-    (match tasks
-      [(list-no-order (task rid (reduce-work left right))
-                      (task mid1 (map-work data1))
-                      (task mid2 (map-work data2)))
-       (check-true (id? left))
-       (check-true (id? right))
-       (check-equal? (set left right) (set (first mid1) (first mid2)))
-       (check-equal? (set data1 data2)
-                     (set "a b c" "d e f"))]
-      [_
-       (displayln tasks)]))
-  (test-case
-      "empty input"
-    (define input "")
-    (define j (string->job input))
-    (check-true (job? j))
-    (match-define (job jid tasks) j)
-    (check-true (id? jid))
-    (check-true (list? tasks))
-    (check-equal? (length tasks) 1)
-    (check-equal? (task-desc (car tasks))
-                  (map-work ""))))
-
-
-;; ---------------------------------------------------------------------------------------------------
-;; Main
-
-(define input "a b c a b c\na b\n a b\na b")
-(define j (string->job input))
-;; expected:
-;; #hash((a . 5) (b . 5) (c . 2))
-
-(spawn-client j)
-(spawn-client (file->job "lorem.txt"))
-(spawn-job-manager)
-(spawn-task-manager 2)
-(spawn-task-manager 3)
-(spawn-observer)
-
-(module+ main
-  (void))

racket/syndicate/examples/actor/internal-knowledge.rkt

@@ -1,61 +0,0 @@
-#lang syndicate
-
-;; Expected Output:
-#|
-balance = 0
-balance = 5
-balance = 0
-JEEPERS
-know overdraft!
-balance = -1
-balance = -2
-no longer in overdraft
-balance = 8
-|#
-
-(assertion-struct balance (v))
-(message-struct deposit (v))
-
-(spawn
- ;; Internal Events
- (message-struct new-transaction (old new))
- (assertion-struct overdraft ())
-
- (field [account 0])
-
- (assert (balance (account)))
-
- (on (message (deposit $v))
-     (define prev (account))
-     (account (+ v (account)))
-     (realize! (new-transaction prev (account))))
-
- (on (realize (new-transaction $old $new))
-     (when (and (negative? new)
-                (not (negative? old)))
-       (react
-        ;; (this print is to make sure only one of these facets is created)
-        (printf "JEEPERS\n")
-        (know (overdraft))
-        (on (realize (new-transaction $old $new))
-            (when (not (negative? new))
-              (stop-current-facet))))))
-
- (during (know (overdraft))
-   (on-start (printf "know overdraft!\n"))
-   (on-stop (printf "no longer in overdraft\n"))))
-
-(spawn
- (on (asserted (balance $v))
-     (printf "balance = ~a\n" v)))
-
-(spawn*
- (send! (deposit 5))
- (flush!)
- (send! (deposit -5))
- (flush!)
- (send! (deposit -1))
- (flush!)
- (send! (deposit -1))
- (flush!)
- (send! (deposit 10)))

racket/syndicate/examples/actor/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/syndicate/examples/actor/realize.rkt

@@ -1,19 +0,0 @@
-#lang syndicate
-
-;; Expected Output:
-#|
-received message bad
-realized good
-|#
-
-(message-struct ping (v))
-
-(spawn
- (on (realize (ping $v))
-     (printf "realized ~a\n" v))
- (on (message (ping $v))
-     (printf "received message ~a\n" v)
-     (realize! (ping 'good))))
-
-(spawn*
- (send! (ping 'bad)))

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,11 +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"
-    ;; Sam: this test displays to stderr which the package server does not like
-    "tests/nested-spawn-exceptions.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/patch.rkt

@@ -14,7 +14,6 @@
          limit-patch
          patch-step
          patch-step*
-         patch-prepend
          compute-aggregate-patch
          apply-patch
          update-interests
@@ -126,13 +125,6 @@
 (define (patch-step* p keys)
   (foldl (lambda (key p) (patch-step p key)) p keys))
 
-;; (U Sigma OpenParenthesis) Trie -> Trie
-;; Prepend both added and removed sets
-(define (patch-prepend key p)
-  (match-define (patch added removed) p)
-  (patch (trie-prepend key added)
-         (trie-prepend key removed)))
-
 ;; Entries labelled with `label` may already exist in `base`; the
 ;; patch `p` MUST already have been limited to add only where no
 ;; `label`-labelled portions of `base` exist, and to remove only where

racket/syndicate/pattern.rkt

@@ -28,7 +28,7 @@
   #:macro-definer-name define-assertion-expander
   #:introducer-parameter-name current-assertion-expander-introducer
   #:local-introduce-name syntax-local-assertion-expander-introduce
-  #:expander-form-predicate-name assertion-expander-form?
+  #:expander-id-predicate-name assertion-expander-id?
   #:expander-transform-name assertion-expander-transform)
 
 (provide (for-syntax
@@ -36,7 +36,7 @@
           assertion-expander?
           assertion-expander-proc
           syntax-local-assertion-expander-introduce
-          assertion-expander-form?
+          assertion-expander-id?
           assertion-expander-transform)
          define-assertion-expander)
 
@@ -153,8 +153,8 @@
                    bs
                    ins))]
 
-        [expander
-         (assertion-expander-form? #'expander)
+        [(expander args ...)
+         (assertion-expander-id? #'expander)
          (assertion-expander-transform pat-stx (lambda (r) (walk (syntax-rearm r pat-stx))))]
 
         [(ctor p ...)

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/.gitignore

@@ -1,4 +0,0 @@
-*.pml
-*.trail
-*.rktd
-*.tmp

racket/typed/Makefile

@@ -1,11 +0,0 @@
-pan : pan.c
-	gcc -o pan pan.c
-
-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

racket/typed/core.rkt

@@ -54,7 +54,7 @@
 
 (module+ test
   (require rackunit)
-  (require rackunit/turnstile))
+  (require turnstile/rackunit-typechecking))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Needed Forms
@@ -1182,4 +1182,4 @@
               : (Instruction Bool ⊥ ⊥)
               -> (syndicate:transition #f (list-)))
   (check-type (quit) : (Instruction ⊥ ⊥ ⊥))
-  (check-type (quit (list)) : (Instruction ⊥ ⊥ ⊥)))
+  (check-type (quit (list)) : (Instruction ⊥ ⊥ ⊥)))

racket/typed/drivers/tcp.rkt

@@ -62,7 +62,7 @@
   (U (Observe (Observe (TcpConnection ★/t (TcpListener ★/t))))
      (Observe (TcpConnection ★/t (TcpListener Int)))
      (Observe (TcpConnection ★/t (TcpListener Int)))
-     (Advertise (Observe (TcpChannel ★/t (TcpListener (TcpHandle (Seal ★/t))) ★/t)))
+     (Advertise (Observe (TcpChannel ★/t (TcpListener (TcpHandle (Seal ★/t)) ★/t))))
      (Observe (Advertise (TcpChannel (TcpAddress String Int) (TcpHandle (Seal ★/t)) ★/t)))
      (TcpAccepted ★/t)
      (Advertise (TcpChannel (TcpHandle (Seal ★/t)) (TcpAddress String Int) ★/t))
@@ -102,7 +102,7 @@
 
 (require/typed syndicate/drivers/tcp2)
 (require/typed (submod syndicate/drivers/tcp2 syndicate-main)
-  [activate! : (proc → (U) #:effects ((Actor Tcp2Driver))) #;(→ (Computation (Value (U))
+               [activate! : (→ (Computation (Value (U))
                                             (Endpoints)
                                             (Roles)
                                             (Spawns (Actor Tcp2Driver))))])

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/flink-support.rkt

@@ -1,132 +0,0 @@
-#lang racket
-
-(provide string->words
-         split-at/lenient-
-         (struct-out job)
-         (struct-out task)
-         (struct-out map-work)
-         (struct-out reduce-work)
-         string->job
-         file->job)
-
-(require (only-in racket/list
-                  split-at))
-(module+ test
-  (require rackunit))
-
-(define (string->words s)
-    (map (lambda (w) (string-trim w #px"\\p{P}")) (string-split s)))
-
-(module+ test
-  (check-equal? (string->words "good day sir")
-                (list "good" "day" "sir"))
-  (check-equal? (string->words "")
-                (list))
-  (check-equal? (string->words "good eve ma'am")
-                (list "good" "eve" "ma'am"))
-  (check-equal? (string->words "please sir. may I have another?")
-                (list "please" "sir" "may" "I" "have" "another"))
-  ;; TODO - currently fails
-  #;(check-equal? (string->words "but wait---there's more")
-                  (list "but" "wait" "there's" "more")))
-
-;; (Listof A) Nat -> (List (Listof A) (Listof A))
-;; like split-at but allow a number larger than the length of the list
-(define (split-at/lenient- lst n)
-  (define-values (a b)
-    (split-at lst (min n (length lst))))
-  (list a b))
-
-;; ---------------------------------------------------------------------------------------------------
-;; Creating a Job
-
-(struct job (id tasks) #:transparent)
-(struct task (id desc) #:transparent)
-(struct map-work (data) #:transparent)
-(struct reduce-work (left right) #:transparent)
-
-;; (Listof WorkDesc) -> (Values (Listof WorkDesc) (Optionof WorkDesc))
-;; Pair up elements of the input list into a list of reduce tasks, and if the input list is odd also
-;; return the odd-one out.
-;; Conceptually, it does something like this:
-;;   '(a b c d) => '((a b) (c d))
-;;   '(a b c d e) => '((a b) (c d) e)
-(define (pair-up ls)
-  (let loop ([ls ls]
-             [reductions '()])
-    (match ls
-      ['()
-       (values reductions #f)]
-      [(list x)
-       (values reductions x)]
-      [(list-rest x y more)
-       (loop more (cons (reduce-work x y) reductions))])))
-
-
-;; a TaskTree is one of
-;;   (map-work data)
-;;   (reduce-work TaskTree TaskTree)
-
-;; (Listof String) -> TaskTree
-;; Create a tree structure of tasks
-(define (create-task-tree lines)
-  (define map-works
-    (for/list ([line (in-list lines)])
-      (map-work line)))
-  ;; build the tree up from the leaves
-  (let loop ([nodes map-works])
-    (match nodes
-      ['()
-       ;; input was empty
-       (map-work "")]
-      [(list x)
-       x]
-      [_
-       (define-values (reductions left-over?)
-         (pair-up nodes))
-       (loop (if left-over?
-                 (cons left-over? reductions)
-                 reductions))])))
-
-;; TaskTree ID -> (Listof Task)
-;; flatten a task tree by assigning job-unique IDs
-(define (task-tree->list tt job-id)
-  (define-values (tasks _)
-    ;; TaskTree ID -> (Values (Listof Task) ID)
-    ;; the input id is for the current node of the tree
-    ;; returned id is the "next available" id, given ids are assigned in strict ascending order
-    (let loop ([tt tt]
-               [next-id 0])
-      (match tt
-        [(map-work _)
-         ;; NOTE : utilizing knowledge of Tuple representation here
-         (values (list (task (list 'tuple next-id job-id) tt))
-                       (add1 next-id))]
-        [(reduce-work left right)
-         (define left-id (add1 next-id))
-         (define-values (lefts right-id)
-           (loop left left-id))
-         (define-values (rights next)
-           (loop right right-id))
-         (values (cons (task (list 'tuple next-id job-id) (reduce-work left-id right-id))
-                        (append lefts rights))
-                 next)])))
-  tasks)
-
-;; InputPort -> Job
-(define (create-job in)
-  (define job-id (gensym 'job))
-  (define input-lines (sequence->list (in-lines in)))
-  (define tasks (task-tree->list (create-task-tree input-lines) job-id))
-  (job job-id tasks))
-
-;; String -> Job
-(define (string->job s)
-  (create-job (open-input-string s)))
-
-;; PathString -> Job
-(define (file->job path)
-  (define in (open-input-file path))
-  (define j (create-job in))
-  (close-input-port in)
-  j)

racket/typed/examples/flink.rkt

@@ -1,576 +0,0 @@
-#lang typed/syndicate
-
-;; ---------------------------------------------------------------------------------------------------
-;; Protocol
-
-
-#|
-Conversations in the flink dataspace primarily concern two topics: presence and
-task execution.
-
-Presence Protocol
------------------
-
-The JobManager (JM) asserts its presence with (job-manager-alive). The operation
-of each TaskManager (TM) is contingent on the presence of a job manager.
-|#
-(assertion-struct job-manager-alive : JobManagerAlive ())
-#|
-In turn, TaskManagers advertise their presence with (task-manager ID slots),
-where ID is a unique id, and slots is a natural number. The number of slots
-dictates how many tasks the TM can take on. To reduce contention, the JM
-should only assign a task to a TM if the TM actually has the resources to
-perform a task.
-|#
-(assertion-struct task-manager : TaskManager (id slots))
-;; an ID is a symbol
-(define-type-alias ID Symbol)
-#|
-The resources available to a TM are its associated TaskRunners (TRs). TaskRunners
-assert their presence with (task-runner ID),
-|#
-(assertion-struct task-runner : TaskRunner (id))
-
-#|
-A Status is one of
-- IDLE, when the TR is not executing a task
-- (executing Int), when the TR is executing the task with identified by the Int
-- OVERLOAD, when the TR has been asked to perform a task before it has
-finished its previous assignment. For the purposes of this model, it indicates a
-failure in the protocol; like the exchange between the JM and the TM, a TR
-should only receive tasks when it is IDLE.
-|#
-(define-constructor* (executing : Executing id))
-(define-type-alias Status (U Symbol (Executing Int)))
-(define IDLE : Status 'idle)
-(define OVERLOAD : Status 'overload)
-
-#|
-Task Delegation Protocol
------------------------
-
-Task Delegation has two roles, TaskAssigner (TA) and TaskPerformer (TP).
-
-A TaskAssigner requests the performance of a Task with a particular TaskPerformer
-through the assertion of interest
-(observe (task-performance ID Task ★))
-where the ID identifies the TP
-|#
-(assertion-struct task-performance : TaskPerformance (assignee task desc))
-#|
-A Task is a (task TaskID Work), where Work is one of
-  - (map-work String)
-  - (reduce-work (U Int TaskResult) (U Int TaskResult)), referring to either the
-    ID of the dependent task or its results. A reduce-work is ready to be executed
-    when it has both results.
-
-A TaskID is a (Tuple Int ID), where the first Int is specific to the individual
-task and the second identifies the job it belongs to.
-
-A TaskResult is a (Hashof String Natural), counting the occurrences of words
-|#
-(require-struct task #:as Task #:from "flink-support.rkt")
-(require-struct map-work #:as MapWork #:from "flink-support.rkt")
-(require-struct reduce-work #:as ReduceWork #:from "flink-support.rkt")
-(define-type-alias TaskID (Tuple Int ID))
-(define-type-alias WordCount (Hash String Int))
-(define-type-alias TaskResult WordCount)
-(define-type-alias Reduce
-  (ReduceWork (Either Int TaskResult)
-              (Either Int TaskResult)))
-(define-type-alias ReduceInput
-  (ReduceWork Int Int))
-(define-type-alias Work
-  (U Reduce (MapWork String)))
-(define-type-alias ConcreteWork
-  (U (ReduceWork TaskResult TaskResult)
-     (MapWork String)))
-(define-type-alias InputTask
-  (Task TaskID (U ReduceInput (MapWork String))))
-(define-type-alias PendingTask
-  (Task TaskID Work))
-(define-type-alias ConcreteTask
-  (Task TaskID ConcreteWork))
-#|
-The TaskPerformer responds to a request by describing its state with respect
-to that task,
-(task-performance ID Task TaskStateDesc)
-
-A TaskStateDesc is one of
-  - ACCEPTED, when the TP has the resources to perform the task. (TODO - not sure if this is ever visible, currently)
-  - OVERLOAD/ts, when the TP does not have the resources to perform the task.
-  - RUNNING, indicating that the task is being performed
-  - (finished TaskResult), describing the results
-|#
-(define-constructor* (finished : Finished data))
-(define-type-alias TaskStateDesc
-  (U Symbol (Finished TaskResult)))
-(define ACCEPTED : TaskStateDesc 'accepted)
-(define RUNNING : TaskStateDesc 'running)
-;; this is gross, it's needed in part because equal? requires two of args of the same type
-(define OVERLOAD/ts : TaskStateDesc 'overload)
-#|
-Two instances of the Task Delegation Protocol take place: one between the
-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
-  (Role (assign)
-    (Shares (Observe (TaskPerformance ID ConcreteTask ★/t)))
-    ;; would be nice to say how the TaskIDs relate to each other
-    (Reacts (Asserted (TaskPerformance ID ConcreteTask ★/t))
-            (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))
-      ;; would be nice to say how the IDs and TaskIDs relate to each other
-      ;; BUG in spec; ConcreteTask used to be just TaskID (when I streamlined protocol)
-      (Shares (TaskPerformance ID ConcreteTask TaskStateDesc)))))
-
-#|
-Job Submission Protocol
------------------------
-
-Finally, Clients submit their jobs to the JobManager by asserting interest
-    (observe (job-completion ID (Listof Task) ★))
-
-The JobManager then performs the job and, when finished, asserts
-    (job-completion ID (Listof Task) TaskResult)
-
-|#
-(require-struct job #:as Job #:from "flink-support.rkt")
-(assertion-struct job-completion : JobCompletion (id data result))
-(define-type-alias JobDesc (Job ID (List InputTask)))
-
-(define-type-alias τc
-  (U (TaskRunner ID)
-     (Observe (TaskPerformance ID ConcreteTask ★/t))
-     (TaskPerformance ID ConcreteTask TaskStateDesc)
-     (Observe (Observe (TaskPerformance ID ★/t ★/t)))
-     (JobManagerAlive)
-     (Observe (JobManagerAlive))
-     (Observe★ TaskRunner)
-     (TaskManager ID Int)
-     (Observe★ TaskManager)
-     (JobCompletion ID (List InputTask) TaskResult)
-     (Observe (JobCompletion ID (List InputTask) ★/t))
-     (Observe (Observe★ JobCompletion))))
-
-;; ---------------------------------------------------------------------------------------------------
-;; Util Macros
-
-(require syntax/parse/define)
-
-(define-simple-macro (log fmt . args)
-  (begin
-    (printf fmt . args)
-    (printf "\n")))
-
-
-
-;; ---------------------------------------------------------------------------------------------------
-;; TaskRunner
-
-
-(define (word-count-increment [h : WordCount]
-                              [word : String]
-                              -> WordCount)
-  (hash-update/failure h
-                       word
-                       add1
-                       0))
-
-(define (count-new-words [word-count : WordCount]
-                         [words : (List String)]
-                         -> WordCount)
-  (for/fold ([result word-count])
-            ([word words])
-    (word-count-increment result word)))
-
-(require/typed "flink-support.rkt"
-  [string->words : (→fn String (List String))])
-
-(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
-    (assert (task-runner id))
-    (on (retracted (task-manager tm-id _))
-        (stop runner))
-    (during (observe (task-performance id $t _))
-      (match-define (task $task-id $desc) t)
-      (field [state TaskStateDesc ACCEPTED])
-      (assert (task-performance id t (ref state)))
-      ;; since we currently finish everything in one turn, these changes to status aren't
-      ;; actually visible.
-      (set! state RUNNING)
-      (match desc
-        [(map-work $data)
-         (define wc (count-new-words (ann (hash) WordCount) (string->words data)))
-         (set! state (finished wc))]
-        [(reduce-work $left $right)
-         (define wc (hash-union/combine left right +))
-         (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
-    (log "Task Manager (TM) ~a is running" id)
-    (during (job-manager-alive)
-     (log "TM ~a learns about JM" id)
-
-     (field [task-runners (Set ID) (set)])
-
-     (on start
-       (for ([_ (in-range num-task-runners)])
-         (define tr-id (gensym 'task-runner))
-         (start-facet monitor-task-runner
-           (on start (spawn-task-runner tr-id id))
-           (on (asserted (task-runner tr-id))
-               (log "TM ~a successfully created task-runner ~a" id tr-id)
-               (set! task-runners (set-add (ref task-runners) tr-id)))
-           (on (retracted (task-runner tr-id))
-               (log "TM ~a detected failure of task runner ~a, restarting" id tr-id)
-               (set! task-runners (set-remove (ref task-runners) tr-id))
-               (spawn-task-runner tr-id id)))))
-
-
-     (field [busy-runners (Set ID) (set)])
-
-     (define/dataflow idle-runners
-       (set-count (set-subtract (ref task-runners) (ref busy-runners))))
-
-     (assert (task-manager id (ref idle-runners)))
-
-     (define (can-accept?)
-       (positive? (ref idle-runners)))
-
-     (define (select-runner)
-       (define runner (for/first ([r (in-set (ref task-runners))]
-                                  #:unless (set-member? (ref busy-runners) r))
-                        r))
-       (match runner
-         [(some $r)
-          (set! busy-runners (set-add (ref busy-runners) r))
-          r]
-         [none
-          (error "need to call can-accept? before selecting a runner")]))
-
-     (during (observe (task-performance id $t _))
-       (match-define (task $task-id $desc) t)
-       (define status0 : TaskStateDesc
-         (if (can-accept?)
-             RUNNING
-             OVERLOAD/ts))
-       (field [status TaskStateDesc status0])
-       (assert (task-performance id t (ref status)))
-       (when (can-accept?)
-         (define runner (select-runner))
-         (log "TM ~a assigns task ~a to runner ~a" id task-id runner)
-         (on stop (set! busy-runners (set-remove (ref busy-runners) runner)))
-         (on (asserted (task-performance runner t $st))
-             (match st
-               [ACCEPTED #f]
-               [RUNNING #f]
-               [OVERLOAD/ts
-                (set! status OVERLOAD/ts)]
-               [(finished discard)
-                (set! status st)]))))))))))
-
-;; ---------------------------------------------------------------------------------------------------
-;; JobManager
-
-;; 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]
-                   [id : Int]
-                   [data : TaskResult]
-                   -> PendingTask)
-  (match t
-    [(task $tid (reduce-work (left id) $r))
-     (task tid (reduce-work (right data) r))]
-    [(task $tid (reduce-work $l (left id)))
-     (task tid (reduce-work l (right data)))]
-    [_ t]))
-
-
-(require/typed "flink-support.rkt"
-  [split-at/lenient- : (∀ (X) (→fn (List X) Int (List (List X))))])
-
-(define (∀ (X) (split-at/lenient [xs : (List X)]
-                                 [n : Int]
-                                 -> (Tuple (List X) (List X))))
-  (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)))
-  (define part (inst partition/either PendingTask PendingTask ConcreteTask))
-  (part tasks
-        (lambda ([t : PendingTask])
-          (match (task-ready? t)
-            [(some $ct)
-             (right ct)]
-            [none
-             (left t)]))))
-
-
-(define (input->pending-task [t : InputTask] -> PendingTask)
-  (match t
-    [(task $id (map-work $s))
-     ;; with occurrence typing, could just return t
-     (task id (map-work s))]
-    [(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
-(assertion-struct slots : Slots (v))
-(assertion-struct slot-assignment : SlotAssignment (who mngr))
-;; tid is the TaskID, rid is a unique symbol to a particular request for a slot
-(define-constructor* (request-id : ReqID tid rid))
-(define-type-alias RequestID (ReqID TaskID ID))
-(message-struct task-is-ready : TaskIsReady (job-id task))
-
-(define (spawn-job-manager)
-  (spawn τc
-    (lift+define-role job-manager-impl ;; export-roles "job-manager-impl.rktd"
-    (start-facet jm ;; #:includes-behavior TaskAssigner
-    (assert (job-manager-alive))
-    (log "Job Manager Up")
-
-    (on start
-      (start-facet slot-manager
-        ;; keep track of task managers, how many slots they say are open, and how many tasks we have assigned.
-        (define/query-hash task-managers (task-manager $id:ID $slots:Int) id slots
-          #:on-add (log "JM learns that ~a has ~v slots" id (hash-ref (ref task-managers) id)))
-
-        (field ;; how many outstanding assignments there are for each task manager
-               [requests-in-flight (Hash ID Int) (hash)]
-               ;; map a request's ID to the manager it is assigned to
-               [assignments (Hash ID ID) (hash)])
-        (define (slots-available)
-          (for/sum ([(id v) (ref task-managers)])
-            (max 0 (- v (hash-ref/failure (ref requests-in-flight) id 0)))))
-
-        (define (try-take-slot! [me : ID] -> (Maybe ID))
-          (define mngr?
-            (for/first ([(id slots) (ref task-managers)]
-                        #:when (positive? (- slots (hash-ref/failure (ref requests-in-flight) id 0))))
-              id))
-          (match mngr?
-            [(some $m)
-             (set! assignments (hash-set (ref assignments) me m))
-             (set! requests-in-flight (hash-update/failure (ref requests-in-flight) m add1 0))]
-            [none
-             #f])
-          mngr?)
-
-        (know (slots (slots-available)))
-
-        (during (know (observe (slot-assignment (request-id $tid:TaskID $who:ID) _)))
-          (on start
-           (start-facet assign-manager
-            ;; what if one manager gains a slot but another loses one, so n stays the same?
-            (on (know (slots $n:Int))
-              #;(log "Dispatcher request ~a learns there are ~a slots" tid n)
-              (unless (or (zero? n) (hash-has-key? (ref assignments) who))
-                (define mngr? (try-take-slot! who))
-                (match mngr?
-                  [(some $mngr)
-                  (stop assign-manager
-                   (log "Dispatcher assigns task ~a to ~a" tid mngr)
-                   (start-facet _ (know (slot-assignment (request-id tid who) mngr)))
-                   (start-facet waiting-for-answer
-                    (on (asserted (observe (task-performance mngr (task tid $x) _)))
-                        (start-facet _ (on (asserted (task-performance mngr (task tid x) _))
-                                           (log "Dispatcher sees answer for ~a" tid)
-                                           (stop waiting-for-answer))))
-                    (on stop
-                     (set! requests-in-flight (hash-update (ref requests-in-flight) mngr sub1)))))]
-                  [_ #f])))))
-          (on stop (set! assignments (hash-remove (ref assignments) who))))))
-
-    (during (observe (job-completion $job-id $tasks _))
-      (log "JM receives job ~a" job-id)
-      (define pending (for/list ([t tasks])
-                        (input->pending-task t)))
-      (define-tuple (not-ready ready) (partition-ready-tasks pending))
-      (field [waiting-tasks (List PendingTask) not-ready]
-             [tasks-in-progress Int 0])
-
-      ;; Task -> Void
-      (define (add-ready-task! [t : ConcreteTask])
-        ;; TODO - use functional-queue.rkt from ../../
-        (match-define (task $tid _) t)
-        (log "JM marks task ~a as ready" tid)
-        (realize! (task-is-ready job-id t)))
-
-      ;; ID Data -> Void
-      ;; Update any dependent tasks with the results of the given task, moving
-      ;; them to the ready queue when possible
-      (define (push-results [task-id : TaskID]
-                            [data : TaskResult])
-        (cond
-          [(and (zero? (ref tasks-in-progress))
-                (empty? (ref waiting-tasks)))
-           (log "JM finished with job ~a" job-id)
-           (realize! (tasks-finished job-id data))]
-          [else
-           ;; TODO - in MapReduce, there should be either 1 waiting task, or 0, meaning the job is done.
-           (define still-waiting
-             (for/fold ([ts : (List PendingTask) (list)])
-                       ([t (ref waiting-tasks)])
-               (define t+ (task+data t (select 0 task-id) data))
-               (match (task-ready? t+)
-                 [(some $ready)
-                  (add-ready-task! ready)
-                  ts]
-                 [_
-                  (cons t+ ts)])))
-           (set! waiting-tasks still-waiting)]))
-
-      ;; Task (ID TaskResult -> Void) -> Void
-      ;; Requires (task-ready? t)
-      (define (∀ (ρ) (perform-task [t : ConcreteTask]
-                                   [k : (proc TaskID TaskResult -> ★/t
-                                              #:effects (ρ))]))
-        (start-facet perform
-         (on start (set! tasks-in-progress (add1 (ref tasks-in-progress))))
-         (on stop (set! tasks-in-progress (sub1 (ref tasks-in-progress))))
-         (match-define (task $this-id $desc) t)
-         (log "JM begins on task ~a" this-id)
-
-         ;; ID -> ...
-         (define (∀ (ρ) (assign-task [mngr : ID]
-                                     [request-again! : (proc -> ★/t #:effects (ρ))]))
-           (start-facet assign
-            (on (retracted (task-manager mngr _))
-                ;; our task manager has crashed
-                (stop assign (request-again!)))
-            (on (asserted (task-performance mngr t $status))
-                (match status
-                  [ACCEPTED #f]
-                  [RUNNING #f]
-                  [OVERLOAD/ts
-                   ;; need to find a new task manager
-                   ;; don't think we need a release-slot! here, because if we've heard back from a task manager,
-                   ;; they should have told us a different slot count since we tried to give them work
-                   (log "JM overloaded manager ~a with task ~a" mngr this-id)
-                   (stop assign (request-again!))]
-                  [(finished $results)
-                   (log "JM receives the results of task ~a" this-id)
-                   (stop perform (k this-id results))]))))
-
-           (define (select-a-task-manager)
-             (start-facet select
-               (field [req-id ID (gensym 'perform-task)])
-               (define (request-again!) (set! req-id (gensym 'perform-task)))
-               (on (know (slot-assignment (request-id this-id (ref req-id)) $mngr:ID))
-                   (assign-task mngr request-again!))))
-
-         (on start (select-a-task-manager))))
-
-      (on start
-       (start-facet delegate-tasks
-         (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))
-             (perform-task t push-results)))
-       (for ([t (in-list ready)])
-         (add-ready-task! t))))))))
-
-;; ---------------------------------------------------------------------------------------------------
-;; Client
-
-;; 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)))))))
-
-;; ---------------------------------------------------------------------------------------------------
-;; Main
-
-(require/typed "flink-support.rkt"
-  [string->job : (→fn String JobDesc)]
-  [file->job : (→fn String JobDesc)])
-
-(define INPUT "a b c a b c\na b\n a b\na b")
-;; expected:
-;; #hash((a . 5) (b . 5) (c . 2))
-
-(run-ground-dataspace τc
-  (spawn-job-manager)
-  (spawn-task-manager 2)
-  (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/internal-knowledge.rkt

@@ -1,88 +0,0 @@
-#lang typed/syndicate
-
-;; Expected Output:
-#|
-balance = 0
-balance = 5
-balance = 0
-JEEPERS
-know overdraft!
-balance = -1
-balance = -2
-no longer in overdraft
-balance = 8
-|#
-
-(assertion-struct balance : Balance (v))
-(message-struct deposit : Deposit (v))
-
-;; Internal Events
-(message-struct new-transaction : NewTransaction (old new))
-(assertion-struct overdraft : Overdraft ())
-
-(define-type-alias τc/external
-  (U (Balance Int)
-     (Message (Deposit Int))
-     (Observe ★/t)))
-
-(define-type-alias τc/internal
-  (U (Message (NewTransaction Int Int))
-     (Overdraft)
-     (Observe ★/t)))
-
-(define-type-alias τc
-  (U τc/external
-     τc/internal))
-
-(run-ground-dataspace τc/external
-
-(spawn
- (begin
- (start-facet bank
-   (field [account Int 0])
-
-   (assert (balance (ref account)))
-
-   (on (message (deposit $v))
-       (define prev (ref account))
-       (set! account (+ v prev))
-       (realize! (new-transaction prev (ref account))))
-
-   (on (realize (new-transaction $old:Int $new:Int))
-       (when (and (negative? new)
-                  (not (negative? old)))
-         (start-facet neg
-          ;; (this print is to make sure only one of these facets is created)
-          (printf "JEEPERS\n")
-          (know (overdraft))
-          (on (realize (new-transaction _ $new:Int))
-              (when (not (negative? new))
-                (stop neg))))))
-
-   (during (know (overdraft))
-       (on-start (printf "know overdraft!\n"))
-       (on-stop (printf "no longer in overdraft\n"))))))
-
-(spawn
- (start-facet obs
-   (on (asserted (balance $v))
-       (printf "balance = ~a\n" v))))
-
-(spawn
- (start-facet _
-   (on start
-    (send! (deposit 5))
-    (spawn
-     (start-facet _
-      (on start
-       (send! (deposit -5))
-       (spawn
-        (start-facet _
-         (on start
-          (send! (deposit -1))
-          (spawn
-           (start-facet _
-            (on start
-             (send! (deposit -1))
-             (spawn (start-facet _ (on start (send! (deposit 10)))))))))))))))))
-)

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/observe-star.rkt

@@ -1,21 +0,0 @@
-#lang typed/syndicate
-;; Expected Output:
-;; got: new
-
-(define-constructor* (something : SomethingT new blue)
-  #:with Something (SomethingT String Int))
-
-(define-type-alias τc
-  (U Something
-     (Observe★ SomethingT)))
-
-(run-ground-dataspace
- τc
- (spawn
-  (start-facet _
-    (assert (something "new" 42))))
- (spawn
-  (start-facet _
-    (on (asserted (something $x 42))
-        (printf "got: ~a\n" x))))
- )

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

@@ -1,27 +0,0 @@
-#lang typed/syndicate
-
-;; Expected Output:
-#|
-received message bad
-realized good
-|#
-
-(message-struct ping : Ping (v))
-
-(define-type-alias τc
-  (U (Message (Ping Symbol))
-     (Observe ★/t)))
-
-(run-ground-dataspace τc
-(spawn
- (start-facet _
-  (on (realize (ping $v:Symbol))
-      (printf "realized ~a\n" v))
-  (on (message (ping $v))
-      (printf "received message ~a\n" v)
-      (realize! (ping 'good)))))
-
-(spawn
- (start-facet _
-  (on start (send! (ping 'bad)))))
-)

racket/typed/examples/require-struct/client2.rkt

@@ -1,17 +0,0 @@
-#lang typed/syndicate
-
-;; using different syntax than "client.rkt"
-
-(require/typed "driver.rkt" [#:struct msg])
-
-(define m : (MsgT Int String) (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)

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
@@ -34,152 +34,133 @@
 (define-type-alias τc
   (U BookQuote
      (Observe (BookQuoteT String ★/t))
-     (Observe (Observe★ BookQuoteT))
+     (Observe (Observe (BookQuoteT ★/t ★/t)))
      ClubMember
-     (Observe★ ClubMemberT)
+     (Observe (ClubMemberT ★/t))
      BookInterest
      (Observe (BookInterestT String ★/t ★/t))
-     (Observe (Observe★ BookInterestT))
+     (Observe (Observe (BookInterestT ★/t ★/t ★/t)))
      BookOfTheMonth
-     (Observe★ BookOfTheMonthT)))
+     (Observe (BookOfTheMonthT ★/t))))
 
 (define-type-alias Inventory (List (Tuple String Int)))
 
 (define (lookup [title : String]
                 [inv : Inventory] -> Int)
-  (for/fold ([stock 0])
-            ([item inv])
+  (for/fold [stock 0]
+            [item inv]
     (if (equal? title (select 0 item))
         (select 1 item)
         stock)))
 
 (define-type-alias seller-role
   (Role (seller)
-   (Reacts (Asserted (Observe (BookQuoteT String ★/t)))
+   (Reacts (Know (Observe (BookQuoteT String ★/t)))
            (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
     (start-facet seller
       (field [books Inventory inventory])
 
       ;; Give quotes to interested parties.
-      (during (observe (book-quote $title _))
+      (during (observe (book-quote (bind title String) discard))
         ;; TODO - lookup
-        (assert (book-quote title (lookup title (! books))))))))))
+        (assert (book-quote title (lookup title (ref books))))))))
 
 (define-type-alias leader-role
   (Role (leader)
-        (Reacts (Asserted (BookQuoteT String Int))
+        (Reacts (Know (BookQuoteT String Int))
                 (Role (poll)
-                      (Reacts (Asserted (BookInterestT String String Bool))
+                      (Reacts (Know (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)
-        (Reacts (Asserted (BookQuoteT String (Bind Int)))
+  (Role (get-quotes31)
+        (Reacts (Know (BookQuoteT String (Bind Int)))
                 (Stop get-quotes)
-                (Role (poll-members)
+                (Role (poll-members36)
                       (Reacts OnDataflow
                               (Stop poll-members
                                     (Stop get-quotes))
                               (Stop get-quotes
                                     (Role (announce39)
                                           (Shares (BookOfTheMonthT String)))))
-                      (Reacts (Retracted (BookInterestT String (Bind String) Bool)))
-                      (Reacts (Asserted (BookInterestT String (Bind String) Bool)))
-                      (Reacts (Retracted (BookInterestT String (Bind String) Bool)))
-                      (Reacts (Asserted (BookInterestT String (Bind String) Bool)))))
-        (Reacts (Retracted (ClubMemberT (Bind String))))
-        (Reacts (Asserted (ClubMemberT (Bind String))))))
+                      (Reacts (¬Know (BookInterestT String (Bind String) Bool)))
+                      (Reacts (Know (BookInterestT String (Bind String) Bool)))
+                      (Reacts (¬Know (BookInterestT String (Bind String) Bool)))
+                      (Reacts (Know (BookInterestT String (Bind String) Bool)))))
+        (Reacts (¬Know (ClubMemberT (Bind String))))
+        (Reacts (Know (ClubMemberT (Bind String))))))
 
 (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)])
      (define (next-book)
        (cond
-         [(empty? (! book-list))
+         [(empty? (ref book-list))
           (printf "leader fails to find a suitable book\n")
           (stop get-quotes)]
          [#t
-          (:= title (first (! book-list)))
-          (:= book-list (rest (! book-list)))]))
+          (set! title (first (ref book-list)))
+          (set! book-list (rest (ref book-list)))]))
 
      ;; keep track of book club members
-     (define/query-set members (club-member $name) name
+     (define/query-set members (club-member (bind name String)) name
          #;#:on-add #;(printf "leader acknowledges member ~a\n" name))
 
-     (on (asserted (book-quote (! title) $quantity))
-         (printf "leader learns that there are ~a copies of ~a\n" quantity (! title))
+     (on (asserted (book-quote (ref title) (bind quantity Int)))
+         (printf "leader learns that there are ~a copies of ~a\n" quantity (ref title))
          (cond
-           [(< quantity (+ 1 (set-count (! members))))
+           [(< quantity (+ 1 (set-count (ref members))))
             ;; not enough in stock for each member
             (next-book)]
            [#t
             ;; find out if at least half of the members want to read the book
             (start-facet poll-members
-             (define/query-set yays (book-interest (! title) $name #t) name)
-             (define/query-set nays (book-interest (! title) $name #f) name)
-             (on (asserted (book-interest (! title) $name _))
-                 ;; count the leader as a 'yay'
-                 (when (>= (set-count (! yays))
-                           (/ (set-count (! members)) 2))
-                   (printf "leader finds enough affirmation for ~a\n" (! title))
-                   (stop get-quotes
-                         (start-facet announce
-                                      (assert (book-of-the-month (! title))))))
-                 (when (> (set-count (! nays))
-                          (/ (set-count (! members)) 2))
-                   (printf "leader finds enough negative nancys for ~a\n" (! title))
-                   (stop poll-members (next-book))))
-             ;; begin/dataflow is a problem for simulation checking
-             #;(begin/dataflow
+             (define/query-set yays (book-interest (ref title) (bind name String) #t) name)
+             (define/query-set nays (book-interest (ref title) (bind name String) #f) name)
+             (begin/dataflow
                ;; count the leader as a 'yay'
-               (when (>= (set-count (! yays))
-                         (/ (set-count (! members)) 2))
-                 (printf "leader finds enough affirmation for ~a\n" (! title))
+               (when (>= (set-count (ref yays))
+                         (/ (set-count (ref members)) 2))
+                 (printf "leader finds enough affirmation for ~a\n" (ref title))
                  (stop get-quotes
                        (start-facet announce
-                         (assert (book-of-the-month (! title))))))
-               (when (> (set-count (! nays))
-                        (/ (set-count (! members)) 2))
-                 (printf "leader finds enough negative nancys for ~a\n" (! title))
-                 (stop poll-members (next-book)))))])))))))
+                         (assert (book-of-the-month (ref title))))))
+               (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)))))]))))))
 
 (define-type-alias member-role
   (Role (member)
         (Shares (ClubMemberT String))
         ;; should this be the type of the pattern? or lowered to concrete types?
-        (Reacts (Asserted (Observe (BookInterestT String ★/t ★/t)))
+        (Reacts (Know (Observe (BookInterestT String ★/t ★/t)))
                 (Role (_)
                       (Shares (BookInterestT String String Bool))))))
-
+                       
 (define (spawn-club-member [name : String]
                            [titles : (List String)])
   (spawn τc
-   (export-roles "member-impl.rktd"
-   (lift+define-role member-impl
    (start-facet member
      ;; assert our presence
      (assert (club-member name))
      ;; respond to polls
-     (during (observe (book-interest $title _ _))
+     (during (observe (book-interest (bind title String) discard discard))
        (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 +172,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
-                (ActorWithRole ★/t Cell))))
+                (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/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/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-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 (Know (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/simple-query-hash.rkt

@@ -1,36 +0,0 @@
-#lang typed/syndicate
-
-;; Expected Output
-;; adding key2 -> 88
-;; adding key1 -> 18
-;; size: 0
-;; size: 2
-;; removing key2
-;; adding key2 -> 99
-
-(assertion-struct output : Output (v))
-
-(define-type-alias ds-type
-  (U (Tuple String Int)
-     (Output Int)
-     (Observe ★/t)))
-
-(run-ground-dataspace ds-type
-  (spawn ds-type
-   (start-facet querier
-     (define/query-hash key# (tuple (bind k String) (bind v Int)) k v
-       #:on-add (printf "adding ~a -> ~a\n" k v)
-       #:on-remove (printf "removing ~a\n" k))
-     (assert (output (hash-count (ref key#))))))
-   (spawn ds-type
-    (start-facet client
-      (assert (tuple "key1" 18))
-      (on start
-          (start-facet tmp
-            (field [v Int 88])
-            (assert (tuple "key2" (ref v)))
-            (on (asserted (output 2))
-                (set! v 99))))
-      (during (output (bind v Int))
-        (on start
-            (printf "size: ~v\n" v))))))

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/examples/with-facets.rkt

@@ -1,22 +0,0 @@
-#lang typed/syndicate
-
-(define (wf1)
-(spawn
- (with-facets
-   ([onn (facet (assert (tuple 'on))
-                (on start (printf "on\n")))]
-    [off (facet (on (asserted (tuple 'go))
-                    (stop off
-                          (start onn)))
-                (on start (printf "off\n")))])
-   off)))
-
-(run-ground-dataspace
- (wf1)
- (spawn (start-facet _ (assert (tuple 'go)))))
-
-;; BAD
-#;(spawn
- (with-facets
-   [on (facet (on start (start on)))]
-   on))

racket/typed/info.rkt

@@ -1,13 +0,0 @@
-#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/"
-    "tests/spin/"))

racket/typed/leader-and-seller.pml

@@ -1,174 +0,0 @@
-/* Useful macros */
-
-#define ASSERTED(x) (x##_assertions > 0)
-#define ASSERT(x) x##_assertions = x##_assertions + 1
-#define RETRACT(x) x##_assertions = x##_assertions - 1
-
-/* Global stuff */
-
-/* Book Quote */
-int BQ_assertions = 0;
-int IBQ_assertions = 0;
-int IIBQ_assertions = 0;
-
-/* Book Interest */
-int BI_assertions = 0;
-int IBI_assertions = 0;
-int IIBI_assertions = 0;
-
-/* Club Members */
-int CM_assertions = 0;
-int ICM_assertions = 0;
-
-/* Announcements */
-int BoTM_assertions = 0;
-
-/* Seller stuff */
-mtype = { seller, seller_during};
-
-active proctype Seller() {
-  mtype current_state = seller;
-  bool asserting_IIBQ = true;
-  bool asserting_BQ = false;
-  bool know_IBQ = false;
-  ASSERT(IIBQ);
-  do
-    :: current_state == seller ->
-       if
-         :: ASSERTED(IBQ) && !know_IBQ ->
-            current_state = seller_during;
-            asserting_BQ = true;
-            ASSERT(BQ);
-       fi;
-       know_IBQ = ASSERTED(IBQ);
-    :: current_state == seller_during ->
-       if
-         :: !ASSERTED(IBQ) && know_IBQ ->
-            current_state = seller;
-            asserting_BQ = false;
-            RETRACT(BQ);
-       fi;
-       know_IBQ = ASSERTED(IBQ);
-  od;
-}
-
-mtype = { get_quotes, announce, poll, none };
-mtype leader_state = get_quotes;
-
-active proctype Leader() {
-  bool asserting_IBI = false;
-  bool asserting_BoTM = false;
-  bool asserting_IBQ = true;
-  bool asserting_ICM = true;
-  bool know_BQ = false;
-  bool know_BI = false;
-  ASSERT(IBQ);
-  ASSERT(ICM);
-  do
-    :: leader_state == get_quotes ->
-       if
-         :: ASSERTED(BQ) && !know_BQ ->
-            leader_state = poll;
-            asserting_IBI = true;
-            ASSERT(IBI);
-         :: ASSERTED(BQ) && !know_BQ ->
-            leader_state = none;
-            asserting_IBQ = false;
-            asserting_ICM = false;
-            RETRACT(IBQ);
-            RETRACT(ICM);
-       fi;
-       know_BQ = ASSERTED(BQ)
-    :: leader_state == announce ->
-       skip;
-    :: leader_state == poll ->
-       if
-         :: ASSERTED(BI) && !know_BI ->
-            leader_state = get_quotes;
-            assert(asserting_IBI);
-            asserting_IBI = false;
-            RETRACT(IBI);
-         :: ASSERTED(BI) && !know_BI ->
-            leader_state = announce;
-            assert(asserting_IBI);
-            asserting_IBI = false;
-            RETRACT(IBI);
-            asserting_BoTM = true;
-            ASSERT(BoTM);
-         :: ASSERTED(BI) && !know_BI ->
-            leader_state = none;
-            assert(asserting_IBI);
-            asserting_IBQ = false;
-            asserting_ICM = false;
-            asserting_IBI = false;
-            RETRACT(IBQ);
-            RETRACT(ICM);
-            RETRACT(IBI);
-         :: ASSERTED(BQ) && !know_BQ ->
-            leader_state = none;
-            assert(asserting_IBI);
-            asserting_IBQ = false;
-            asserting_ICM = false;
-            asserting_IBI = false;
-            RETRACT(IBQ);
-            RETRACT(ICM);
-            RETRACT(IBI);
-       fi;
-       know_BI = ASSERTED(BI);
-       know_BQ = ASSERTED(BQ);
-    :: leader_state == none ->
-       skip;
-  od
-}
-
-mtype = { member, during_member };
-
-active proctype Member() {
-  mtype current_state = member;
-  bool asserting_BI = false;
-  bool asserting_IIBI = true;
-  bool asserting_CM = true;
-  ASSERT(IIBI);
-  ASSERT(CM);
-  bool know_IBI = false;
-  do
-    :: current_state == member ->
-       if
-         :: ASSERTED(IBI) && !know_IBI ->
-            current_state = during_member;
-            asserting_BI = true;
-            ASSERT(BI);
-       fi;
-       know_IBI = ASSERTED(IBI);
-    :: current_state == during_member ->
-       if
-         :: !ASSERTED(IBI) && know_IBI ->
-            current_state = member;
-            asserting_BI = false;
-            RETRACT(BI);
-       fi;
-       know_IBI = ASSERTED(IBI);
-  od
-}
-
-ltl sanity {
-  [](BQ_assertions >= 0 &&
-     IBQ_assertions >= 0 &&
-     IIBQ_assertions >= 0 &&
-     BI_assertions >= 0 &&
-     IBI_assertions >= 0 &&
-     IIBI_assertions >= 0 &&
-     CM_assertions >= 0 &&
-     ICM_assertions >= 0 &&
-     BoTM_assertions >= 0)
-  &&
-  <> (BQ_assertions > 0)
-  &&
-  [] (ASSERTED(IBQ) -> <> ASSERTED(BQ))
-  &&
-  [] (ASSERTED(IBI) -> <> ASSERTED(BI))
-  /*
-  &&
-  <> (leader_state == announce || leader_state == none)
-   */
-}

racket/typed/main.rkt

@@ -36,7 +36,7 @@
 
 (module+ test
   (require rackunit)
-  (require rackunit/turnstile))
+  (require turnstile/rackunit-typechecking))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Types
@@ -721,7 +721,7 @@ is meant to be
 
 (define-typed-syntax (λ [p s] ...) ≫
   #:with (([x:id τ:type] ...) ...) (stx-map pat-bindings #'(p ...))
-  [[x ≫ x- : τ] ... ⊢ s ≫ s- (⇒ : τv) (⇒ :i τ1) (⇒ :o τ2) (⇒ :a τ3)] ...
+  [[x ≫ x- : τ :i (U) :o (U) :a (U)] ... ⊢ s ≫ s- (⇒ : τv) (⇒ :i τ1) (⇒ :o τ2) (⇒ :a τ3)] ...
   ;; REALLY not sure how to handle p/p-/p.match-pattern,
   ;; particularly w.r.t. typed terms that appear in p.match-pattern
   [⊢ p ≫ _ ⇒ τ-p] ...
@@ -944,4 +944,4 @@ is meant to be
            (syntax-parse e
              [(~var _ class) #'#t]
              [_ #'#f]))
-         (test-result))]))
+         (test-result))]))

racket/typed/scribblings/typed-syndicate.scrbl

@@ -1,778 +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]. The
-@racket[on-add-expr] and @racket[on-remove-expr], when given, execute after
-@racket[name] has been updated.
-}
-
-@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/syndicate/core-expressions.rkt

@@ -1,391 +0,0 @@
-#lang turnstile
-
-(provide bind
-         discard
-         ann
-         if
-         when
-         unless
-         let
-         let*
-         cond
-         else
-         match
-         tuple
-         unit
-         select
-         error
-         define-tuple
-         match-define
-         mk-tuple
-         tuple-select
-         (for-syntax (all-defined-out)))
-
-(require "core-types.rkt")
-(require (only-in "prim.rkt" Bool String #%datum))
-(require (postfix-in - racket/match))
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Patterns
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(define-typed-syntax (bind x:id τ:type) ≫
-  ----------------------------------------
-  [⊢ (#%app- error- 'bind "escaped") (⇒ : (Bind τ))])
-
-(define-typed-syntax discard
-  [_ ≫
-   --------------------
-   [⊢ (#%app- error- 'discard "escaped") (⇒ : Discard)]])
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Core-ish forms
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-;; copied from stlc
-(define-typed-syntax (ann e (~optional (~datum :)) τ:type) ≫
-  [⊢ e ≫ e- (⇐ : τ.norm) (⇒ ν (~effs eff ...))]
-  ------------------------------------------------
-  [⊢ e- (⇒ : τ.norm) (⇒ ν (eff ...))])
-
-;; copied from ext-stlc
-(define-typed-syntax if
-  [(_ e_tst e1 e2) ⇐ τ-expected ≫
-   [⊢ e_tst ≫ e_tst- ⇒ _] ; Any non-false value is truthy.
-   #:fail-unless (pure? #'e_tst-) "expression must be pure"
-   [⊢ e1 ≫ e1- (⇐ : τ-expected) (⇒ ν (~effs eff1 ...))]
-   [⊢ e2 ≫ e2- (⇐ : τ-expected) (⇒ ν (~effs eff2 ...))]
-   --------
-   [⊢ (if- e_tst- e1- e2-)
-      (⇒ : τ-expected)
-      (⇒ ν #,(make-Branch #'((eff1 ...) (eff2 ...))))]]
-  [(_ e_tst e1 e2) ≫
-   [⊢ e_tst ≫ e_tst- ⇒ _] ; Any non-false value is truthy.
-   #:fail-unless (pure? #'e_tst-) "expression must be pure"
-   [⊢ e1 ≫ e1- (⇒ : τ1) (⇒ ν (~effs eff1 ...))]
-   [⊢ e2 ≫ e2- (⇒ : τ2) (⇒ ν (~effs eff2 ...))]
-   #:with τ (mk-U- #'(τ1 τ2))
-   --------
-   [⊢ (if- e_tst- e1- e2-) (⇒ : τ)
-      (⇒ ν #,(make-Branch #'((eff1 ...) (eff2 ...))))]])
-
-(define-typed-syntax (when e s ...+) ≫
-  ------------------------------------
-  [≻ (if e (let () s ...) #f)])
-
-(define-typed-syntax (unless e s ...+) ≫
-  ------------------------------------
-  [≻ (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)
-                   (⇒ ν (~effs eff ...))]
-   ----------------------------------------------------------
-   [⊢ (let- ([x- e-] ...) e_body-) (⇒ : τ_expected)
-      (⇒ ν (eff ...))]]
-  [(_ ([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)
-                   (⇒ ν (~effs eff ...))]
-   ----------------------------------------------------------
-   [⊢ (let- ([x- e-] ...) e_body-) (⇒ : τ_body)
-      (⇒ ν (eff ...))]])
-
-;; copied from ext-stlc
-(define-typed-syntax let*
-  [(_ () e_body ...) ≫
-   --------
-   [≻ (block e_body ...)]]
-  [(_ ([x e] [x_rst e_rst] ...) e_body ...) ≫
-   --------
-   [≻ (let ([x e]) (let* ([x_rst e_rst] ...) e_body ...))]])
-
-(define-typed-syntax (cond [pred:expr s ...+] ...+) ≫
-  [⊢ pred ≫ pred- (⇐ : Bool)] ...
-  #:fail-unless (stx-andmap pure? #'(pred- ...)) "predicates must be pure"
-  [⊢ (block s ...) ≫ s- (⇒ : τ-s)
-                   (⇒ ν (~effs eff ...))] ...
-  ------------------------------------------------
-  [⊢ (cond- [pred- s-] ...) (⇒ : (U τ-s ...))
-     (⇒ ν #,(make-Branch #'((eff ...) ...)))])
-
-(define else #t)
-
-(define-typed-syntax (match e [p s ...+] ...+) ≫
-  [⊢ e ≫ e- (⇒ : τ-e)]
-  #:fail-unless (pure? #'e-) "expression must be pure"
-  #: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)
-                (⇒ ν (~effs eff ...))] ...
-  ;; REALLY not sure how to handle p/p-/p.match-pattern,
-  ;; particularly w.r.t. typed terms that appear in p.match-pattern
-  [⊢ p/e ≫ p-- ⇒ τ-p] ...
-  #:fail-unless (project-safe? #'τ-e (mk-U*- #'(τ-p ...))) "possibly unsafe pattern match"
-  #:fail-unless (stx-andmap pure? #'(p-- ...)) "patterns must be pure"
-  #:with (p- ...) (stx-map (lambda (p x-s xs) (substs x-s xs (compile-match-pattern p)))
-                           #'(p/e ...)
-                           #'((x- ...) ...)
-                           #'((x ...) ...))
-  --------------------------------------------------------------
-  [⊢ (match- e- [p- s-] ...
-                [_ (#%app- error- "incomplete pattern match")])
-     (⇒ : (U τ-s ...))
-     (⇒ ν #,(make-Branch #'((eff ...) ...)))])
-
-
-;; (Listof Value) -> Value
-(define- (mk-tuple es)
-  (#%app- cons- 'tuple es))
-
-(define-typed-syntax (tuple e:expr ...) ≫
-  [⊢ e ≫ e- (⇒ : τ) (⇒ ν (~effs F ...))] ...
-  -----------------------
-  [⊢ (#%app- mk-tuple (#%app- list- e- ...))
-     (⇒ : (Tuple τ ...))
-     (⇒ ν (F ... ...))])
-
-(define unit : Unit (tuple))
-
-(define-typed-syntax (select n:nat e:expr) ≫
-  [⊢ e ≫ e- (⇒ : (~Tuple τ ...)) (⇒ ν (~effs F ...))]
-  #:do [(define i (syntax->datum #'n))]
-  #:fail-unless (< i (stx-length #'(τ ...))) "index out of range"
-  #:with τr (list-ref (stx->list #'(τ ...)) i)
-  --------------------------------------------------------------
-  [⊢ (#%app- tuple-select n e-) (⇒ : τr) (⇒ ν (F ...))])
-
-(define- (tuple-select n t)
-  (#%app- list-ref- t (#%app- add1- n)))
-
-(define-typed-syntax (error msg args ...) ≫
-  [⊢ msg ≫ msg- (⇐ : String)]
-  [⊢ args ≫ args- (⇒ : τ)] ...
-  #:fail-unless (all-pure? #'(msg- args- ...)) "expressions must be pure"
-  ----------------------------------------
-  [⊢ (#%app- error- msg- args- ...) (⇒ : ⊥)])
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Helpers
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-;; pat -> ([Id Type] ...)
-(define-for-syntax (pat-bindings stx)
-  (syntax-parse stx
-    #:datum-literals (bind tuple)
-    [(bind x:id τ:type)
-     #'([x τ])]
-    [(tuple p ...)
-     #:with (([x:id τ:type] ...) ...) (stx-map pat-bindings #'(p ...))
-     #'([x τ] ... ...)]
-    [(~constructor-exp cons p ...)
-     #:with (([x:id τ:type] ...) ...) (stx-map pat-bindings #'(p ...))
-     #'([x τ] ... ...)]
-    [_
-     #'()]))
-
-(begin-for-syntax
-  ;; Any -> Bool
-  (define (dollar-variable? x)
-    (and (identifier? x)
-         (char=? (string-ref (symbol->string (syntax-e x)) 0) #\$)))
-
-  ;; dollar-id -> Identifier
-  (define (un-dollar x)
-    (datum->syntax x (string->symbol (substring (symbol->string (syntax-e x)) 1))))
-
-  (define-syntax-class dollar-id
-    #:attributes (id)
-    (pattern x:id
-             #:when (dollar-variable? #'x)
-             #:attr id (un-dollar #'x)))
-
-  ;; match things of the for "$X...:Y..." where X and Y are things without
-  ;; spaces (i.e. likely but not definitely legal identifiers)
-  (define DOLLAR-ANN-RX #px"^\\$(\\S*):(\\S*)$")
-
-  ;; Any -> RegexpMatchResults
-  (define (dollar-ann-variable? x)
-    (and (identifier? x)
-         (regexp-match DOLLAR-ANN-RX (symbol->string (syntax-e x)))))
-
-  (define-syntax-class dollar-ann-id
-    #:attributes (id ty)
-    (pattern x:id
-             #:do [(define match? (dollar-ann-variable? #'x))]
-             #:when match?
-             #:attr id (datum->syntax #'x (string->symbol (second match?)))
-             #:attr ty (datum->syntax #'x (string->symbol (third match?)))))
-
-  ;; expand uses of $ short-hand
-  ;; doesn't handle uses of $id or ($) w/o a type
-  (define (elaborate-pattern pat)
-    (syntax-parse pat
-      #:datum-literals (tuple _ $)
-      [_
-       #'discard]
-      [x:dollar-ann-id
-       (syntax/loc pat (bind x.id x.ty))]
-      [($ x:id ty)
-       (syntax/loc pat (bind x ty))]
-      [(tuple p ...)
-       (quasisyntax/loc pat
-         (tuple #,@(stx-map elaborate-pattern #'(p ...))))]
-      [(~constructor-exp ctor p ...)
-       (define field-tys (ctor-field-tys #'ctor))
-       (define sub-pats
-         (for/list ([field-pat (in-syntax #'(p ...))]
-                    [field-ty? (in-list field-tys)])
-           (if field-ty?
-               (elaborate-pattern/with-type field-pat field-ty?)
-               (elaborate-pattern field-pat))))
-       (quasisyntax/loc pat
-         (ctor #,@sub-pats))]
-      [e:expr
-       #'e]))
-
-  (define (elaborate-pattern/with-type pat ty)
-    (syntax-parse pat
-      #:datum-literals (tuple $)
-      [(~datum _)
-       #'discard]
-      [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)
-         (syntax-parse t
-           [(~Tuple tt ...)
-            #:when (stx-length=? #'(p ...) #'(tt ...))
-            #t]
-           [_ #f]))
-       (define (proj t i)
-         (syntax-parse t
-           [(~Tuple tt ...)
-            (if (= i -1)
-                t
-                (stx-list-ref #'(tt ...) i))]
-           [(~U* (~or (~and tt (~fail #:unless (or (U*? #'tt) (matching? #'tt))))
-                      _) ...)
-            (mk-U- (stx-map (lambda (x) (proj x i)) #'(tt ...)))]
-           [_
-            (mk-U*- '())]))
-       (define selected (proj ty -1))
-       (define sub-pats
-         (for/list ([pat (in-syntax #'(p ...))]
-                    [i (in-naturals)])
-           (elaborate-pattern/with-type pat (proj selected i))))
-       (quasisyntax/loc pat
-         (tuple #,@sub-pats))]
-      [(~constructor-exp ctor p ...)
-       (define tag (ctor-type-tag #'ctor))
-       (define (matching? t)
-         (syntax-parse t
-           [(~constructor-type tag2 tt ...)
-            #:when (equal? tag (syntax-e #'tag2))
-            #:when (stx-length=? #'(p ...) #'(tt ...))
-            #t]
-           [_ #f]))
-       (define (proj t i)
-         (syntax-parse t
-           [(~constructor-type _ tt ...)
-            #:when (matching? t)
-            (if (= i -1)
-                t
-                (stx-list-ref #'(tt ...) i))]
-           [(~U* (~or (~and tt (~fail #:unless (or (U*? #'tt) (matching? #'tt))))
-                      _) ...)
-            (mk-U- (stx-map (lambda (x) (proj x i)) #'(tt ...)))]
-           [_
-            (mk-U*- '())]))
-       (define selected (proj ty -1))
-       (define sub-pats
-         (for/list ([pat (in-syntax #'(p ...))]
-                    [i (in-naturals)])
-           (elaborate-pattern/with-type pat (proj selected i))))
-       (quasisyntax/loc pat
-         (ctor #,@sub-pats))]
-      [e:expr
-       #'e])))
-
-;; TODO - figure out why this needs different list identifiers
-(define-for-syntax (compile-pattern pat list-binding bind-id-transformer exp-transformer)
-    (define (l-e stx) (local-expand stx 'expression '()))
-    (let loop ([pat pat])
-      (syntax-parse pat
-        #:datum-literals (tuple discard bind)
-        [(tuple p ...)
-         #`(#,list-binding 'tuple #,@(stx-map loop #'(p ...)))]
-        [(bind x:id τ:type)
-         (bind-id-transformer #'x)]
-        [discard
-         #'_]
-        [(~constructor-exp ctor p ...)
-         (define/with-syntax uctor (untyped-ctor #'ctor))
-         #`(uctor #,@(stx-map loop #'(p ...)))]
-        [_
-         ;; local expanding "expression-y" syntax allows variable references to transform
-         ;; according to the mappings set up by turnstile.
-         (exp-transformer (l-e pat))])))
-
-(define-for-syntax (compile-match-pattern pat)
-  (compile-pattern pat
-                   #'list
-                   identity
-                   (lambda (exp) #`(==- #,exp))))
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Derived Forms
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(define-typed-syntax (define-tuple (x:id ...) e:expr) ≫
-  [⊢ e ≫ e- (⇒ (~Tuple τ ...))]
-  #:fail-unless (stx-length=? #'(x ...) #'(τ ...))
-                "mismatched size"
-  #:with (sel ...) (for/list ([y (in-syntax #'(x ...))]
-                              [t (in-syntax #'(τ ...))]
-                              [i (in-naturals)])
-                     (quasisyntax/loc this-syntax
-                       (select #,i it)))
-  ----------------------------------------
-  [≻ (begin
-       (define it e-)
-       (define x : τ sel) ...)])
-
-(define-typed-syntax (match-define pat:expr e:expr) ≫
-  [⊢ e ≫ e- (⇒ : τ-e)]
-  #:with pat+ (elaborate-pattern/with-type #'pat #'τ-e)
-  #:with ([x τ] ...) (pat-bindings #'pat+)
-  ----------------------------------------
-  [≻ (define-tuple (x ...)
-       (match e-
-         [pat+
-          (tuple x ...)]))])
-
-;; extremely limited match-define for `define-constructor`-d things
-
-#;(define-typed-syntax (match-define (~constructor-exp ctor x:id ...) e:expr) ≫
-  [⊢ e ≫ e- (⇒ (~constructor-type tag1 τ ...))]
-  #:fail-unless (stx-length=? #'(x ...) #'(τ ...))
-                "mismatched size"
-  [⊢ (ctor (bind x τ) ...) ≫ pat- (⇒ (~constructor-type tag2 _ ...))]
-  #:fail-unless (equal? #'tag1 #'tag2)
-                (~format "type mismatch: ~a, ~a" #'tag1 #'tag2)
-  ------------------------------------------------------------
-  )

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

@@ -1,35 +0,0 @@
-#lang turnstile
-
-(provide Left
-         Right
-         Either
-         left
-         right
-         partition/either)
-
-(require "core-types.rkt")
-(require "core-expressions.rkt")
-(require "for-loops.rkt")
-(require "list.rkt")
-
-(define-constructor* (left : Left v))
-(define-constructor* (right : Right v))
-
-(define-type-alias (Either A B)
-  (U (Left A)
-     (Right B)))
-
-(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)])
-            ([x xs])
-    (define y-or-z (pred x))
-    (match y-or-z
-      [(left (bind y Y))
-       (tuple (cons y lefts)
-              rights)]
-      [(right (bind z Z))
-       (tuple lefts
-              (cons z rights))])))

racket/typed/syndicate/for-loops.rkt

@@ -1,245 +0,0 @@
-#lang turnstile
-
-(provide for/fold
-         for
-         for/list
-         for/set
-         for/sum
-         for/first)
-
-(require "core-types.rkt")
-(require "sequence.rkt")
-(require (only-in "list.rkt" List ~List))
-(require (only-in "set.rkt" Set ~Set))
-(require (only-in "hash.rkt" Hash ~Hash))
-(require (only-in "prim.rkt" Int Bool + #%datum))
-(require (only-in "core-expressions.rkt" let unit tuple-select mk-tuple))
-(require "maybe.rkt")
-
-(require (postfix-in - (only-in racket/set
-                                for/set
-                                in-set)))
-
-(begin-for-syntax
-  (define-splicing-syntax-class iter-clause
-    #:attributes (parend)
-    #:datum-literals (:)
-    (pattern [x:id seq:expr]
-             #:attr parend #'[x seq])
-    (pattern [x:id : τ:type seq:expr]
-             #:attr parend #'[x : τ seq])
-    (pattern [(k:id v:id) hash-seq:expr]
-             #:attr parend #'[(k v) hash-seq])
-    (pattern (~seq #:when pred:expr)
-             #:attr parend #'(#:when pred))
-    (pattern (~seq #:unless pred:expr)
-             #:attr parend #'(#:unless pred))
-    (pattern (~seq #:break pred:expr)
-             #:attr parend #'(#:break pred))))
-
-;; a Binding is a (SyntaxList Id Id Type), i.e. #'(x x- τ-x)
-(begin-for-syntax
-  (struct loop-clause (exp bindings) #:transparent)
-  (struct directive (kw exp) #:transparent))
-
-
-;; (SyntaxListOf LoopClause) -> (Syntax LoopClause- (Binding ...))
-(define-for-syntax (analyze-for-clauses clauses)
-  (define-values (br binds)
-    (for/fold ([body-rev '()]
-               [bindings '()])
-              ([clause (in-syntax clauses)])
-      (match (analyze-for-clause clause bindings)
-        [(loop-clause exp bs)
-         (values (cons exp body-rev)
-                 (append bindings bs))]
-        [(directive kw exp)
-         (values (list* exp kw body-rev)
-                 bindings)])))
-  #`(#,(reverse br)
-     #,binds))
-
-;; iter-clause (Listof Binding) -> (U iter-clause directive)
-(define-for-syntax (analyze-for-clause clause ctx)
-  (define/with-syntax ([y y- τ-y] ...) ctx)
-  (syntax-parse clause
-    #:datum-literals (:)
-    [[x:id seq:expr]
-     #:and (~typecheck
-             [[y ≫ y-- : τ-y] ... ⊢ seq ≫ seq- (⇒ : τ-seq)])
-     #:fail-unless (pure? #'seq-) "pure"
-     #:with x- (generate-temporary #'x)
-     #:do [(define-values (seq-- τ-elems) (make-sequence #'seq- #'τ-seq))]
-     (loop-clause (substs #'(y- ...) #'(y-- ...)
-                          #`[x- #,seq--]
-                          free-identifier=?)
-                  (list #`(x x- #,τ-elems)))]
-    [[x:id : τ:type seq:expr]
-     #:with seq+ (add-expected-type #'seq #'τ.norm)
-     #:do [(match-define (list seq- (list (list x- τ-elems)))
-             (analyze-for-clause (syntax/loc clause [x seq+])))]
-     #:fail-unless (<: τ-elems #'τ.norm) "unexpected type"
-     (loop-clause #`[#,x- #,seq-]
-                  (list #`(x #,x- τ.norm)))]
-    [[(k:id v:id) hash-seq:expr]
-     #:and (~typecheck
-            [[y ≫ y-- : τ-y] ... ⊢ hash-seq ≫ hash-seq- (⇒ : (~Hash K V))])
-     #:fail-unless (pure? #'hash-seq-) "pure"
-     #:with (k- v-) (generate-temporaries #'(k v))
-     (loop-clause (substs #'(y- ...) #'(y-- ...)
-                          #`[(k- v-) (in-hash- hash-seq-)]
-                          free-identifier=?)
-                  (list #'(k k- K) #'(v v- V)))]
-    [(dir:keyword pred)
-     #:and (~typecheck
-            [[y ≫ y-- : τ-y] ... ⊢ pred ≫ pred- (⇐ : Bool)])
-     #:fail-unless (pure? #'pred-) "pure"
-     (directive #'dir (substs #'(y- ...) #'(y-- ...)
-                              #'pred-
-                              free-identifier=?))]))
-
-;; Expression Type -> (Values Expression Type)
-;; Determine what kind of sequence we're dealing with;
-;; if it's not already in Sequence form, wrap the expression in the appropriate in-* form
-;; also figure out what the type of elements are to associate with the loop variable
-;; hashes handled separately
-(define-for-syntax (make-sequence e τ)
-  (syntax-parse τ
-    [(~Sequence t)
-     (values e #'t)]
-    [(~List t)
-     (values #`(in-list- #,e) #'t)]
-    [(~Set t)
-     (values #`(in-set- #,e) #'t)]
-    [_
-     (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] ...+)
-             (clause:iter-clause
-              ...)
-     e-body ...+) ≫
-  [⊢ init ≫ init- (⇐ : τ-acc)] ...
-  #:fail-unless (all-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)
-                               (⇒ ν (~effs F ...))]
-  -------------------------------------------------------
-  [⊢ (values->tuple #,num-accs
-       (for/fold- ([acc- init-] ...)
-         clauses-
-         #,(bind-renames #'([x-- x-] ...) #`(tuple->values #,num-accs e-body-))))
-     (⇒ : body-ty)
-     (⇒ ν (F ...))]]
-  [(for/fold (accs ... [acc:id init] more-accs ...)
-             clauses
-     e-body ...+) ≫
-   [⊢ init ≫ _ (⇒ : τ-acc)]
-   ---------------------------------------------------
-   [≻ (for/fold (accs ... [acc τ-acc init] more-accs ...)
-                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-
-                           (⇒ : τ-body)
-                           (⇒ ν-ep (~effs τ-ep ...))
-                           (⇒ ν-s (~effs τ-s ...))
-                           (⇒ ν-f (~effs τ-f ...))]
-  ----------------------------------------------------------------------
-  [⊢ (for/list- clauses-
-       #,(bind-renames #'([x-- x-] ...) #'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-
-                           (⇒ : τ-body)
-                           (⇒ ν (~effs F ...))]
-  ----------------------------------------------------------------------
-  [⊢ (for/set- clauses-
-       #,(bind-renames #'([x-- x-] ...) #'e-body-))
-              (⇒ : (Set τ-body))
-              (⇒ ν (F ...))])
-
-(define-typed-syntax (for/sum (clause ...)
-                       e-body ...+) ≫
-  ----------------------------------------------------------------------
-  [≻ (for/fold ([acc Int 0])
-               (clause ...)
-       (+ acc (let () e-body ...)))])
-
-(define-typed-syntax (for (clause ...)
-                       e-body ...+) ≫
-  ----------------------------------------------------------------------
-  [≻ (for/fold ([acc unit])
-               (clause ...)
-       e-body ...
-       acc)])
-
-(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-
-                 (⇒ : τ-body)
-                 (⇒ ν (~effs F ...))]
-  [[res ≫ _ : τ-body] ⊢ res  ≫ res- (⇒ : _)]
-  ----------------------------------------------------------------------
-  [⊢ (let- ()
-       (define- res-
-         (for/first- clauses-
-                     #,(bind-renames #'([x-- x-] ...) #'e-body-)))
-       (if- res-
-            (some res-)
-            none))
-     (⇒ : (Maybe τ-body))
-     (⇒ ν (F ...))])

racket/typed/syndicate/hash.rkt

@@ -1,71 +0,0 @@
-#lang turnstile
-
-(provide Hash
-         (for-syntax ~Hash)
-         hash
-         hash-set
-         hash-ref
-         (typed-out [[hash-ref/failure- : (∀ (K V) (→fn (Hash K V) K V V))]
-                     hash-ref/failure])
-         hash-has-key?
-         hash-update
-         (typed-out [[hash-update/failure- : (∀ (K V) (→fn (Hash K V) K (→fn V V) V (Hash K V)))]
-                     hash-update/failure])
-         hash-remove
-         hash-map
-         hash-keys
-         hash-values
-         hash-keys-subset?
-         hash-count
-         hash-empty?
-         hash-union
-         (typed-out [[hash-union/combine- : (∀ (K V) (→fn (Hash K V) (Hash K V) (→fn V V V) (Hash K V)))]
-                     hash-union/combine])
-         )
-
-(require "core-types.rkt")
-(require (only-in "list.rkt" List))
-(require (only-in "prim.rkt" Int Bool))
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Immutable Hash Tables
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(define-container-type Hash #:arity = 2)
-
-(define-typed-syntax (hash (~seq key:expr val:expr) ...) ≫
-  [⊢ key ≫ key- (⇒ : τ-k)] ...
-  [⊢ val ≫ val- (⇒ : τ-val)] ...
-  #:fail-unless (all-pure? #'(key- ... val- ...)) "gotta be pure"
-  --------------------------------------------------
-  [⊢ (#%app- hash- (~@ key val) ...) (⇒ : (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))]
-  [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)))]
-  [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)))]
-  [hash-values : (∀ (K V) (→fn (Hash K V) (List V)))]
-  ;; TODO hash->list makes cons pairs
-  #;[hash->list : (∀ (K V) (→fn (Hash K V) (List (ConsPair K V))))]
-  [hash-keys-subset? : (∀ (K1 V1 K2 V2) (→fn (Hash K1 V1) (Hash K2 V2) Bool))]
-  [hash-count : (∀ (K V) (→fn (Hash K V) Int))]
-  [hash-empty? : (∀ (K V) (→fn (Hash K V) Bool))])
-
-(require/typed racket/hash
-  [hash-union : (∀ (K1 V1 K2 V2) (→fn (Hash K1 V1) (Hash K2 V2) (Hash (U K1 K2) (U V1 V2))))]
-  )
-
-(define- (hash-ref/failure- h k err)
-  (#%app- hash-ref- h k err))
-
-(define- (hash-update/failure- h k u err)
-  (#%app- hash-update- h k u err))
-
-(define- (hash-union/combine- h1 h2 combine)
-  (#%app- hash-union- h1 h2 #:combine combine))

racket/typed/syndicate/lang/reader.rkt

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

racket/typed/syndicate/list.rkt

@@ -1,39 +0,0 @@
-#lang turnstile
-
-(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?]
-                    [[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?]
-                    [[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]))
-
-(require "core-types.rkt")
-(require (only-in "prim.rkt" Bool Int))
-(require (postfix-in - racket/list))
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Lists
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(define-container-type List #:arity = 1)
-
-(define-typed-syntax (list e ...) ≫
-  [⊢ e ≫ e- ⇒ τ] ...
-  #:fail-unless (all-pure? #'(e- ...)) "expressions must be pure"
-  -------------------
-  [⊢ (#%app- list- e- ...) ⇒ (List (U τ ...))])
-
-(define- (member?- v l)
-  (and- (#%app- member- v l) #t))

racket/typed/syndicate/ltl.rkt

@@ -1,73 +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])
-;;  - (release [LTL X] [LTL X])
-;;  - (ltl-implies [LTL X] [LTL X])
-;;  - (ltl-and [LTL X] [LTL X])
-;;  - (ltl-or  [LTL X] [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 release [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))]
-      [(release p q)
-       (release (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/maybe.rkt

@@ -1,47 +0,0 @@
-#lang turnstile
-
-(provide Maybe
-         None
-         None*
-         Some
-         some
-         none
-         has?)
-
-(require "core-types.rkt")
-(require "prim.rkt")
-(require "core-expressions.rkt")
-
-
-(define-constructor* (none* : None*))
-(define-constructor* (some : Some v))
-
-(define-type-alias None (None*))
-
-(define none : None
-  (none*))
-
-(define-type-alias (Maybe X)
-  (U None
-     (Some X)))
-
-#;(define (∀ (X Y) (partition/maybe [xs : (List X)]
-                                  [pred : (→fn X (Maybe Y))]
-                                  -> (Tuple (List Y) (List X))))
-    #f)
-
-#;(require (only-in "core-expressions.rkt" match error discard)
-         "prim.rkt")
-#;(define (∀ (X) (unwrap! [x : (Maybe X)] -> (Maybe X)))
-  (match x
-    [(some discard)
-     (error "some")]
-    [none
-     (error "none")]))
-
-(define (∀ (X) (has? [v : (Maybe X)] [p : (→fn X Bool)] -> Bool))
-  (match v
-    [none
-     #f]
-    [(some $x)
-     (p x)]))

racket/typed/syndicate/prim.rkt

@@ -1,137 +0,0 @@
-#lang turnstile
-
-(provide (all-defined-out)
-         True False Bool
-         (for-syntax (all-defined-out)))
-
-(require "core-types.rkt")
-(require (rename-in racket/math [exact-truncate exact-truncate-]))
-(require (postfix-in - (only-in racket/format ~a ~v)))
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Primitives
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(define-base-types Zero NonZero String ByteString Symbol)
-
-(define-type-alias Int (U Zero NonZero))
-
-;; hmmm
-(define-primop + (→fn Int Int Int))
-(define-primop - (→fn Int Int Int))
-(define-primop * (→fn Int Int Int))
-(define-primop not (→fn Bool Bool))
-(define-primop < (→fn Int Int Bool))
-(define-primop > (→fn Int Int Bool))
-(define-primop <= (→fn Int Int Bool))
-(define-primop >= (→fn Int Int Bool))
-(define-primop = (→fn Int Int Bool))
-(define-primop even? (→fn Int Bool))
-(define-primop odd? (→fn Int Bool))
-(define-primop add1 (→fn Int Int))
-(define-primop sub1 (→fn Int Int))
-(define-primop max (→fn Int Int Int))
-(define-primop min (→fn Int Int Int))
-(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 (→fn ByteString String))
-(define-primop string->bytes/utf-8 (→fn String ByteString))
-(define-primop gensym (→fn Symbol Symbol))
-(define-primop symbol->string (→fn Symbol String))
-(define-primop string->symbol (→fn String Symbol))
-
-(define-typed-syntax (/ e1 e2) ≫
-  [⊢ e1 ≫ e1- (⇐ : Int)]
-  [⊢ e2 ≫ e2- (⇐ : Int)]
-  #:fail-unless (pure? #'e1-) "expression not allowed to have effects"
-  #:fail-unless (pure? #'e2-) "expression not allowed to have effects"
-  ------------------------
-  [⊢ (#%app- exact-truncate- (#%app- /- e1- e2-)) (⇒ : Int)])
-
-;; I think defining `and` and `or` as primops doesn't work because they're syntax
-(define-typed-syntax (and e ...) ≫
-  [⊢ e ≫ e- (⇐ : Bool)] ...
-  #:fail-unless (stx-andmap pure? #'(e- ...)) "expressions not allowed to have effects"
-  ------------------------
-  [⊢ (and- e- ...) (⇒ : Bool)])
-
-(define-typed-syntax (or e ...) ≫
-  [⊢ e ≫ e- (⇐ : Bool)] ...
-  #:fail-unless (stx-andmap pure? #'(e- ...)) "expressions not allowed to have effects"
-  ------------------------
-  [⊢ (or- e- ...) (⇒ : Bool)])
-
-(define-typed-syntax (equal? e1:expr e2:expr) ≫
-  [⊢ e1 ≫ e1- (⇒ : τ1)]
-  [⊢ e2 ≫ e2- (⇒ : τ2)]
-  #:fail-unless (flat-type? #'τ1)
-    (format "equality only available on flat data; got ~a" (type->str #'τ1))
-  #:fail-unless (flat-type? #'τ2)
-    (format "equality only available on flat data; got ~a" (type->str #'τ2))
-  #:with int (∩ #'τ1 #'τ2)
-  #:fail-unless (not (bot? #'int))
-    (format "empty overlap between types ~a and ~a" (type->str #'τ1) (type->str #'τ2))
-  #:fail-unless (pure? #'e1-) "expression not allowed to have effects"
-  #:fail-unless (pure? #'e2-) "expression not allowed to have effects"
-  ---------------------------------------------------------------------------
-  [⊢ (#%app- equal?- e1- e2-) (⇒ : Bool)])
-
-(define-typed-syntax (displayln e:expr) ≫
-  [⊢ e ≫ e- (⇒ : τ)]
-  #:fail-unless (pure? #'e-) "expression not allowed to have effects"
-  ---------------
-  [⊢ (#%app- displayln- e-) (⇒ : ★/t)])
-
-(define-typed-syntax (printf e ...+) ≫
-  [⊢ e ≫ e- (⇒ : τ)] ...
-  #:fail-unless (stx-andmap pure? #'(e- ...)) "expression not allowed to have effects"
-  ---------------
-  [⊢ (#%app- printf- e- ...) (⇒ : ★/t)])
-
-(define-typed-syntax (~a e ...) ≫
-  [⊢ e ≫ e- (⇒ : τ)] ...
-  #:fail-unless (stx-andmap flat-type? #'(τ ...))
-                "expressions must be string-able"
-  --------------------------------------------------
-  [⊢ (#%app- ~a- e- ...) (⇒ : String)])
-
-(define-typed-syntax (~v e ...) ≫
-  [⊢ e ≫ e- (⇒ : τ)] ...
-  #:fail-unless (stx-andmap flat-type? #'(τ ...))
-  "expressions must be string-able"
-  --------------------------------------------------
-  [⊢ (#%app- ~v- e- ...) (⇒ : String)])
-
-(define-typed-syntax (format s e ...) ≫
-  [⊢ s ≫ s- (⇐ : String)]
-  [⊢ e ≫ e- (⇒ : τ)] ...
-  #:fail-unless (stx-andmap flat-type? #'(τ ...))
-  "expressions must be string-able"
-  --------------------------------------------------
-  [⊢ (#%app- format- s- e- ...) (⇒ : String)])
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Basic Values
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(define-typed-syntax #%datum
-  [(_ . n:integer) ≫
-   #:with T (if (zero? (syntax-e #'n)) #'Zero #'NonZero)
-  ----------------
-  [⊢ (#%datum- . n) (⇒ : T)]]
-  [(_ . b:boolean)
-   ≫
-   #:with T (if (syntax-e #'b) #'True #'False)
-  ----------------
-  [⊢ (#%datum- . b) (⇒ : T)]]
-  [(_ . s:string) ≫
-  ----------------
-  [⊢ (#%datum- . s) (⇒ : String)]])
-
-(define-typed-syntax (typed-quote x:id) ≫
-  -------------------------------
-  [⊢ (quote- x) (⇒ : Symbol)])

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,21 +0,0 @@
-#!/bin/sh
-
-pushd ${1%/*}/ > /dev/null
-
-EXE="$1-verifier.o"
-
-spin -a $1
-if [[ $? -ne 0 ]]; then
-    popd > /dev/null
-    exit 1
-fi
-
-gcc -o $EXE -D NFAIR=3 pan.c
-
-# -a to analyze, -f for (weak) fairness
-# -n to elide report of unreached states
-# -N spec-name to verify a particular specification
-$EXE -a -f -n -N $2
-rm $EXE pan.*
-
-popd > /dev/null