Compare commits

...

159 Commits
main ... behav

Author SHA1 Message Date
Sam Caldwell 9113d93acf floating define test 2020-03-10 10:57:54 -04:00
Sam Caldwell 65d14de735 track branching for each kind of effect in match 2020-03-10 10:57:35 -04:00
Sam Caldwell 311108fbcf typed flink: replace dataflow in job manager with internal events 2020-02-26 16:34:24 -05:00
Sam Caldwell 01a544b0d9 Allow `define`d expressions to have effects 2020-02-26 14:50:35 -05:00
Sam Caldwell 86258acc6c improve function application error messages 2020-02-26 14:50:08 -05:00
Sam Caldwell b6c934b9f3 TODO: keep track of match branching 2020-02-25 16:16:19 -05:00
Sam Caldwell 66226ac725 improve spawn error messages 2020-02-25 16:14:30 -05:00
Sam Caldwell 772faec0bc cleanup 2020-02-25 13:02:33 -05:00
Sam Caldwell 99e53d9729 fix typed `or` 2020-02-24 15:10:59 -05:00
Sam Caldwell 0074fcb566 flink: remove use of dataflow 2020-02-24 13:34:22 -05:00
Sam Caldwell 5d5b827535 flink: replace a lot of dataflow in job manager with internal events 2020-02-21 15:49:46 -05:00
Sam Caldwell 220d112393 fix bugs in internal events 2020-02-21 15:48:12 -05:00
Sam Caldwell e06eb1bfcf
Merge pull request #37 from stchang/behav
edit info files to enable raco test typed/
2020-02-10 08:49:05 -05:00
Stephen Chang a6719eb124 edit info files to enable raco test typed/ 2020-02-09 23:24:37 -05:00
Sam Caldwell 39c54e77f3 new job manager role 2020-01-07 11:52:02 -05:00
Sam Caldwell 555c41a153 task manager role 2019-12-31 13:55:59 -05:00
Sam Caldwell 33ef42818d fixup format of task performer spec 2019-12-30 17:13:29 -05:00
Sam Caldwell 8afed87e99 stuff 2019-12-30 16:27:29 -05:00
Sam Caldwell f5331eb24f typed flink: unify task-state and task-assignment, job and job-finished 2019-10-21 12:22:10 -04:00
Sam Caldwell 80ebab5ed7 untyped flink: use interest as request for jobs 2019-10-16 16:21:00 -04:00
Sam Caldwell d29afb6679 untyped flink: unify task-assignment and task-state assertions 2019-10-16 16:13:19 -04:00
Sam Caldwell 123037ba51 typed flink: streamline ids 2019-10-16 12:25:04 -04:00
Sam Caldwell 5e61e9941b untyped flink: finish streamlining ids, resolve dataflow issue 2019-10-15 11:40:55 -04:00
Sam Caldwell 7374c8c506 untyped flink: work on streamlining ids, demonstrating dataflow issue 2019-10-15 11:16:46 -04:00
Sam Caldwell 2610ceb541 untyped flink: fiddle with race in task manager 2019-10-10 13:45:33 -04:00
Sam Caldwell a8e890ab30 typed flink: associate task runners with a particular task manager 2019-10-10 13:44:38 -04:00
Sam Caldwell 96daa7518a add in-range 2019-10-10 13:43:59 -04:00
Sam Caldwell eb56a1006f typed flink: task runners don't need a status 2019-10-03 16:09:40 -04:00
Sam Caldwell 142206d8e3 typed define/dataflow 2019-10-03 15:24:31 -04:00
Sam Caldwell 479ea2fc1f associate task runners with a particular task manager 2019-10-01 16:44:43 -04:00
Sam Caldwell 42d025cc7f flink: task runners don't need a status 2019-10-01 10:12:31 -04:00
Sam Caldwell 33b516b7a6 verify request/response property in leader-and-seller 2019-09-26 13:39:28 -04:00
Sam Caldwell 2fa30c6066 fix bug in leader-and-seller 2019-09-26 13:39:01 -04:00
Sam Caldwell 5ef44987ca fiddling with spin 2019-09-24 09:52:41 -04:00
Sam Caldwell 04e34c58ea start cleaning up/streamlining flink 2019-08-26 11:09:35 -04:00
Sam Caldwell 29f589d7c4 fix a couple bugs 2019-08-26 11:09:34 -04:00
Sam Caldwell 443e1f9ac1 Label internal events & handlers with actor-unique IDs 2019-08-26 11:09:34 -04:00
Sam Caldwell 4e2ae45b0b initial take on supporting spawn actions in role graphs 2019-08-26 11:09:34 -04:00
Sam Caldwell 8949193977 utilize define-spawns to clean up 7-GUIS examples 2019-08-26 11:09:34 -04:00
Sam Caldwell 0e44970bef Modify syndicate's module-begin to capture actions on the RHS of define
Example. consider a procedure that spawns an actor and then returns
some value relevant to communicating to that actor:

(define (spawn-an-actor)
  (define name (gensym))
  (spawn
    (on (asserted (... name ...))
         ...)
     ...)
  name)

And the module top level tries to boot and use this actor with a define:

(define the-name (spawn-an-actor))
(spawn ... use the-name ...)

The new module-begin analyzes (forms that expand to) define-values to
wrap the body with a capture-actor-actions, allowing such spawns to be
detected.
2019-08-26 11:09:34 -04:00
Sam Caldwell ded2629296 7-GUIS port task 7 2019-08-26 11:09:34 -04:00
Sam Caldwell a259153470 7-GUIS port task 6 2019-08-26 11:09:33 -04:00
Sam Caldwell cdca416d21 7-GUIS port task 5 2019-08-26 11:09:33 -04:00
Sam Caldwell de1fab2cb5 7-GUIS port task 4 2019-08-26 11:09:33 -04:00
Sam Caldwell 064a2e1462 7-GUIS port task 3 2019-08-26 11:09:33 -04:00
Sam Caldwell 3c65281a2e 7-GUIS port task 2 2019-08-26 11:09:33 -04:00
Sam Caldwell 997a3099fd start on racket guis, 7-GUIS task 1 2019-08-26 11:09:33 -04:00
Sam Caldwell e018359204 consider more potential schedulings of events 2019-08-26 11:09:32 -04:00
Sam Caldwell 9a21a811a3 internal event business 2019-08-26 11:09:32 -04:00
Sam Caldwell 3c3291ffa4 compile internal events, compresses job manager graph by a lot 2019-08-26 11:09:32 -04:00
Sam Caldwell b17cba59ed remove self loops, things working better 2019-08-26 11:09:32 -04:00
Sam Caldwell 16175c7bb4 fix bug in flink 2019-08-26 11:09:32 -04:00
Sam Caldwell 27abf8ab1e detect cycles when compiling internal events 2019-08-26 11:09:32 -04:00
Sam Caldwell e6524174e1 first take on inlining internal events 2019-08-26 11:09:31 -04:00
Sam Caldwell 135e6b655b rudimentary support for internal events in proto 2019-08-26 11:09:31 -04:00
Sam Caldwell 202bcd6842 add messages to proto 2019-08-26 11:09:31 -04:00
Sam Caldwell fa8822e40d small cleanup 2019-08-26 11:09:31 -04:00
Sam Caldwell c40b773282 reorganize examples 2019-08-26 11:09:31 -04:00
Sam Caldwell be5bc19fcc job manager role 2019-08-26 11:09:31 -04:00
Sam Caldwell 537b3fd272 more event constructors in proto 2019-08-26 11:09:31 -04:00
Sam Caldwell 8f8f4c416f replace some dataflow with internal events in typed flink 2019-08-26 11:09:30 -04:00
Sam Caldwell 5f38b6cc94 allow equal? when there's overlap 2019-08-26 11:09:30 -04:00
Sam Caldwell f597fdc499 internal events for typed lang 2019-08-26 11:09:30 -04:00
Sam Caldwell 963676c0c6 Change type names Know -> Asserted, \negKnow -> Retracted 2019-08-26 11:09:30 -04:00
Sam Caldwell 7462af708b (during (know P) O ...) for internal knowledge 2019-08-26 11:09:30 -04:00
Sam Caldwell e6b733325c Create an actor-internal event system oriented around assertions and
messges.

internal form        ~ external form
(know v)             ~ (assert v)
(on (know p) ...)    ~ (on (asserted p) ...)
(on (forget p) ...)  ~ (on (retracted p) ...)
(realize! v)         ~ (send! v)
(on (realize v) ...) ~ (on (message v) ...)
2019-08-26 11:09:30 -04:00
Sam Caldwell affa47a2a5 minor printing stuff in examples 2019-08-26 11:09:29 -04:00
Sam Caldwell 458bf93fef subgraph stuff working better 2019-08-26 11:09:29 -04:00
Sam Caldwell c38bfdc2c0 some work on checking/finding subgraphs 2019-08-26 11:09:29 -04:00
Sam Caldwell ee726c9177 task assigner spec and task manager type 2019-08-26 11:09:29 -04:00
Sam Caldwell 5dee1981b6 provide Branch and Effs types 2019-08-26 11:09:29 -04:00
Sam Caldwell da900a258a extract some code from verify body 2019-08-26 11:09:29 -04:00
Sam Caldwell 32f117df16 task performer spec and task runner type 2019-08-26 11:09:28 -04:00
Sam Caldwell dcc4e3c411 During type abbreviation 2019-08-26 11:09:28 -04:00
Sam Caldwell 703a4c9589 support for dataflow, misc fixes and improvements 2019-08-26 11:09:28 -04:00
Sam Caldwell 3ebcf413c9 more accurate job manager type 2019-08-26 11:09:28 -04:00
Sam Caldwell 47ca363b18 add container types to proto 2019-08-26 11:09:28 -04:00
Sam Caldwell 0711cd3232 print types different 2019-08-26 11:09:28 -04:00
Sam Caldwell 6b272ad3d3 cleanups and improvements 2019-08-26 11:09:27 -04:00
Sam Caldwell d93dc085fe remove stop-when abomination 2019-08-26 11:09:27 -04:00
Sam Caldwell 3e1d4d108f initial support for on start and on stop 2019-08-26 11:09:27 -04:00
Sam Caldwell 3ad0457bd5 small cleanup 2019-08-26 11:09:27 -04:00
Sam Caldwell ce0c296b5c parse quoted turnstile types 2019-08-26 11:09:27 -04:00
Sam Caldwell 60ed8c2677 tweak how types are printed 2019-08-26 11:09:27 -04:00
Sam Caldwell eba7ed072c cleanup 2019-08-26 11:09:27 -04:00
Sam Caldwell c811b9a45f forgot to add maybe.rkt and either.rkt 2019-08-26 11:09:26 -04:00
Sam Caldwell 3faaa1c580 typed flink working! 2019-08-26 11:09:26 -04:00
Sam Caldwell 23bee726b1 priorities for query handlers, on-add, on-remove 2019-08-26 11:09:26 -04:00
Sam Caldwell 3aedb63a9c client and jobs (not working) 2019-08-26 11:09:26 -04:00
Sam Caldwell 807e6bb8f7 map list op 2019-08-26 11:09:26 -04:00
Sam Caldwell 98a779bdc1 resolve mutual dependency in flink via dataflow 2019-08-26 11:09:25 -04:00
Sam Caldwell c37c060dc9 fancify patterns in flink 2019-08-26 11:09:24 -04:00
Sam Caldwell c78b76b38c fancify the patterns in book-club 2019-08-26 11:09:24 -04:00
Sam Caldwell 22a228ab4b Use the communication type (via a turnstile `mode`) when elaborating
patterns in facets
2019-08-26 11:09:24 -04:00
Sam Caldwell 296a77d714 clean up patterns in flink 2019-08-26 11:09:24 -04:00
Sam Caldwell 4fdce7fc0c elaborate more patterns 2019-08-26 11:09:24 -04:00
Sam Caldwell 13e988fe58 some work towards a better pattern language 2019-08-26 11:09:24 -04:00
Sam Caldwell 24efe43a6f typed flink getting closer 2019-08-26 11:09:24 -04:00
Sam Caldwell 99d5916bd1 limited support for effect polymorphism 2019-08-26 11:09:23 -04:00
Sam Caldwell 20693f234e more flink 2019-08-26 11:09:23 -04:00
Sam Caldwell deca0a82be progress on flink 2019-08-26 11:09:23 -04:00
Sam Caldwell 96e9431e15 first take on match-define-like form 2019-08-26 11:09:23 -04:00
Sam Caldwell 8cf13a9bbf stop-when derived form 2019-08-26 11:09:23 -04:00
Sam Caldwell c283dae7e4 positive? primitive 2019-08-26 11:09:23 -04:00
Sam Caldwell 559e9bb11b for/first 2019-08-26 11:09:22 -04:00
Sam Caldwell df9f3ebbd2 zero? primitive 2019-08-26 11:09:22 -04:00
Sam Caldwell c8a1253d7b examples/flink.rkt: work on job manager and utilities 2019-08-26 11:09:22 -04:00
Sam Caldwell fc220a4e16 Use a mutable, compile-time table for type metadata 2019-08-26 11:09:22 -04:00
Sam Caldwell a84b80a49b Make inference slightly more lenient wrt unions
some tests not working because of syntax-property failure
2019-08-26 11:09:22 -04:00
Sam Caldwell ed695c66d6 add error form 2019-08-26 11:09:22 -04:00
Sam Caldwell 4420f6cd74 improve handling of type variables 2019-08-26 11:09:21 -04:00
Sam Caldwell d9e651a668 tweak how pattern types are handled 2019-08-26 11:09:21 -04:00
Sam Caldwell 66a3ece353 flink-support 2019-08-26 11:09:21 -04:00
Sam Caldwell db41cb63d7 query-hash 2019-08-26 11:09:21 -04:00
Sam Caldwell 349fa19d26 require&provide maybe,either 2019-08-26 11:09:21 -04:00
Sam Caldwell 5238b74912 move patterns to core expressions 2019-08-26 11:09:21 -04:00
Sam Caldwell 3def83502a more primitive operations 2019-08-26 11:09:20 -04:00
Sam Caldwell 5fda25a42e more hash operations 2019-08-26 11:09:20 -04:00
Sam Caldwell 9dd11ef7db more list operations 2019-08-26 11:09:20 -04:00
Sam Caldwell 8f92368d8f typed-flink: task manager 2019-08-26 11:09:20 -04:00
Sam Caldwell dc0e434caa make sure begin always has a definition context 2019-08-26 11:09:20 -04:00
Sam Caldwell fd40ab2e52 more set operations 2019-08-26 11:09:20 -04:00
Sam Caldwell 5310956848 more hash functions 2019-08-26 11:09:20 -04:00
Sam Caldwell 1590687e7a typed flink - task runner 2019-08-26 11:09:19 -04:00
Sam Caldwell 68f14919d7 fix output type for actors without interests 2019-08-26 11:09:19 -04:00
Sam Caldwell 309d6867d9 fix argument order bug in hash-update 2019-08-26 11:09:19 -04:00
Sam Caldwell 8819af878e typed flink data definitions 2019-08-26 11:09:19 -04:00
Sam Caldwell 3b35000a5e assertion-struct macro 2019-08-26 11:09:19 -04:00
Sam Caldwell 69660e02dd split out core-expressions with #%app, which is now more explicit 2019-08-26 11:09:19 -04:00
Sam Caldwell 4b692428af Improve scoping structure of for-clauses 2019-08-26 11:09:18 -04:00
Sam Caldwell 2c0bef7da4 make list operations polymorphic functions 2019-08-26 11:09:18 -04:00
Sam Caldwell 75539d0ec3 fix ty-var bug 2019-08-26 11:09:18 -04:00
Sam Caldwell 47d2568a93 first take on local inference 2019-08-26 11:09:18 -04:00
Sam Caldwell 1bdb9b7820 move definition of primitive base types 2019-08-26 11:09:18 -04:00
Sam Caldwell 97b3a9a0b5 subtyping for effect-free functions 2019-08-26 11:09:18 -04:00
Sam Caldwell 63089efdbc fixup fold in book club 2019-08-26 11:09:17 -04:00
Sam Caldwell 1b2527920e start on for loops 2019-08-26 11:09:17 -04:00
Sam Caldwell 899d8c460d hash tables 2019-08-26 11:09:17 -04:00
Sam Caldwell af56bc283d add sequences 2019-08-26 11:09:17 -04:00
Sam Caldwell 33522647fd allow polymorphic function definitions 2019-08-26 11:09:17 -04:00
Sam Caldwell c9563cd0a2 type abstractions 2019-08-26 11:09:17 -04:00
Sam Caldwell 80ef12ef4d split out primitives 2019-08-26 11:09:16 -04:00
Sam Caldwell 1c9f53590d split out files 2019-08-26 11:09:16 -04:00
Sam Caldwell c9a44ab45e Attach useful metadata as syntax properties to some types
In order to make defining judgments like subytping and intersection
more extensible, introduce a form for defining type constructors that
describes:
  - how it behaves wrt intersction (product-like or container-like)
  - variances for subtyping
  - the type constructor transformer, for making new instances

This eliminates a lot of very repetitive code, and should make things
much more extensible
2019-08-26 11:09:16 -04:00
Sam Caldwell e3c7926b92 simplify implementation of overlaps? 2019-08-26 11:09:16 -04:00
Sam Caldwell 7815fad415 examples/flink: implement task delegation roles in terms of abstract
templates
2019-08-26 11:09:16 -04:00
Sam Caldwell e16db164df look more at book club roles 2019-08-26 11:09:16 -04:00
Sam Caldwell 362d7c877d More leader-related role finangling 2019-08-26 11:09:15 -04:00
Sam Caldwell 19f915620e Keep track of branches for role effects in turnstile lang 2019-08-26 11:09:15 -04:00
Sam Caldwell c726fb2bdd look into leader impl simulating spec a bit 2019-08-26 11:09:15 -04:00
Sam Caldwell 47dc84f034 some more simulation tests 2019-08-26 11:09:15 -04:00
Sam Caldwell 0cc550ea43 leader-spec simulates itself! 2019-08-26 11:09:15 -04:00
Sam Caldwell 324557e8b5 simplest simulation example passes 2019-08-26 11:09:14 -04:00
Sam Caldwell 50448f41a7 subtyping 2019-08-26 11:09:14 -04:00
Sam Caldwell 126046caa9 remember initial state when compiling 2019-08-26 11:09:14 -04:00
Sam Caldwell a8d398eec7 small improvements 2019-08-26 11:09:13 -04:00
Sam Caldwell 170e2b28ce incorporate branching! 2019-08-26 11:09:13 -04:00
Sam Caldwell 480b67ea51 More on facet states, including graphviz view 2019-08-26 11:09:13 -04:00
Sam Caldwell 64016053ff prototyping interpretation of roles as state machines 2019-08-26 11:09:13 -04:00
54 changed files with 9074 additions and 2001 deletions

View File

@ -0,0 +1,44 @@
#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)))))

View File

@ -0,0 +1,22 @@
#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))

View File

@ -0,0 +1,59 @@
#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))))

View File

@ -0,0 +1,67 @@
#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))))

View File

@ -0,0 +1,58 @@
#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))))

View File

@ -0,0 +1,71 @@
#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))))

View File

@ -0,0 +1,206 @@
#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)))

View File

@ -0,0 +1,96 @@
#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)))

View File

@ -0,0 +1,4 @@
#lang setup/infotab
(define compile-omit-paths
'("examples"))

View File

@ -0,0 +1,387 @@
#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)

View File

@ -31,6 +31,9 @@
retracted
rising-edge
(rename-out [core:message message])
know
forget
realize
let-event
@ -58,6 +61,7 @@
perform-actions!
flush!
quit-dataspace!
realize!
syndicate-effects-available?
@ -80,6 +84,7 @@
(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))
@ -198,10 +203,15 @@
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.
@ -249,6 +259,12 @@
;; 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))
@ -407,6 +423,7 @@
(analyze-pattern stx #'P))
(quasisyntax/loc stx
(add-endpoint! #,(source-location->string stx)
#f
(lambda ()
#,(let ((patch-stx #`(core:assert #,pat)))
(if #'w.Pred
@ -414,6 +431,22 @@
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)
@ -474,6 +507,7 @@
(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))))))
@ -489,14 +523,18 @@
(define-syntax (during stx)
(syntax-parse stx
[(_ P O ...)
(define E-stx (syntax/loc #'P (asserted P)))
#: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))
(define-values (_proj _pat _bindings instantiated)
(analyze-pattern E-stx #'P))
(quasisyntax/loc stx
(on #,E-stx
(let ((p #,instantiated))
(react (stop-when (retracted p))
(react (stop-when (#,R-stx p))
O ...))))]))
(define-syntax (during/spawn stx)
@ -547,6 +585,7 @@
(quasisyntax/loc stx
(let ()
(add-endpoint! #,(source-location->string stx)
#f
(lambda ()
(define subject-id (current-dataflow-subject-id))
(schedule-script!
@ -570,6 +609,8 @@
(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
@ -772,62 +813,125 @@
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Syntax-time support
(define (interests-pre-and-post-patch pat synthetic?)
(define (interests-pre-and-post-patch pat synthetic? retrieve-knowledge)
(define (or* x y) (or x y))
(define a (current-actor-state))
(define previous-knowledge (if synthetic? trie-empty (actor-state-previous-knowledge a)))
(define old (trie-lookup previous-knowledge pat #f #:wildcard-union or*))
(define new (trie-lookup (actor-state-knowledge a) pat #f #:wildcard-union or*))
(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?)
(define-values (old new) (interests-pre-and-post-patch pat synthetic?))
(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?)
(define-values (old new) (interests-pre-and-post-patch pat synthetic?))
(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)))
(define-for-syntax (analyze-asserted/retracted outer-expr-stx
when-pred-stx
event-stx
script-stx
asserted?
P-stx
priority-stx)
;; 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))
;; 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-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-values (proj-stx pat bindings _instantiated)
(analyze-pattern event-stx P-stx))
(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)))
(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)
(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)))))]))))))
(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))))]))))))
(define-for-syntax orig-insp
(variable-reference->module-declaration-inspector (#%variable-reference)))
@ -839,7 +943,7 @@
priority-stx)
(define event-stx (syntax-disarm armed-event-stx orig-insp))
(syntax-parse event-stx
#:literals [core:message asserted retracted rising-edge]
#:literals [core:message asserted retracted rising-edge know forget realize]
[(expander args ...)
#:when (event-expander-id? #'expander)
(event-expander-transform
@ -851,33 +955,23 @@
script-stx
priority-stx)))]
[(core:message P)
(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))))])))))]
(analyze-message outer-expr-stx when-pred-stx event-stx script-stx
#'P priority-stx #f)]
[(asserted P)
(analyze-asserted/retracted outer-expr-stx when-pred-stx event-stx script-stx
#t #'P priority-stx)]
(analyze-appear/disappear outer-expr-stx when-pred-stx event-stx script-stx
#t #'P priority-stx #f)]
[(retracted P)
(analyze-asserted/retracted outer-expr-stx when-pred-stx event-stx script-stx
#f #'P priority-stx)]
(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)]
[(rising-edge Pred)
(define field-name
(datum->syntax event-stx
@ -887,6 +981,7 @@
(let ()
(field [#,field-name #f])
(add-endpoint! #,(source-location->string outer-expr-stx)
#f
(lambda ()
(when #,when-pred-stx
(define old-val (#,field-name))
@ -1003,10 +1098,25 @@
(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 (add-endpoint! where patch-fn handler-fn)
(define (add-endpoint! where internal? patch-fn handler-fn)
(when (in-script?)
(error 'add-endpoint!
"~a: Cannot add endpoint in script; are you missing a (react ...)?"
@ -1030,7 +1140,9 @@
(hash-set (facet-endpoints f)
new-eid
(endpoint new-eid patch-fn handler-fn))]))))
(schedule-action! delta-aggregate))
(if internal?
(schedule-internal-event! delta-aggregate)
(schedule-action! delta-aggregate)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Facet Lifecycle
@ -1045,7 +1157,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))))
(update-facet! fid (lambda (_f) (facet fid (hasheqv) '() (set) trie-empty trie-empty)))
(update-facet! parent-fid
(lambda (pf)
(and pf (struct-copy facet pf
@ -1094,8 +1206,21 @@
(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))
(current-actor-state (struct-copy actor-state a [mux new-mux]))
(schedule-action! delta-aggregate))))
(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))))
(schedule-script!
#:priority *gc-priority*
@ -1124,6 +1249,8 @@
(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
@ -1151,6 +1278,7 @@
(when script
(script)
(refresh-facet-assertions!)
(dispatch-internal-events!)
(run-all-pending-scripts!)))
(define (run-scripts!)
@ -1162,6 +1290,20 @@
(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)
@ -1189,7 +1331,9 @@
(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]))
(schedule-action! delta-aggregate))
(define-values (internal external) (split-internal/external delta-aggregate))
(schedule-internal-event! internal)
(schedule-action! external))
(define (actor-behavior e a)
(and e
@ -1197,10 +1341,12 @@
(if (patch? e)
(struct-copy actor-state a
[previous-knowledge (actor-state-knowledge a)]
[knowledge (update-interests (actor-state-knowledge a) e)])
[knowledge (apply-patch (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)))]
@ -1210,6 +1356,14 @@
(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?))))
@ -1306,6 +1460,10 @@
(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)
@ -1337,6 +1495,23 @@
(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)
@ -1352,7 +1527,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)))

View File

@ -2,6 +2,7 @@
(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")
@ -52,6 +53,24 @@
(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-syntax (syndicate-module stx)
(syntax-parse stx
[(_ (action-ids ...) (form forms ...))
@ -61,27 +80,27 @@
#'begin-for-declarations)
(kernel-form-identifier-list))))
(syntax-parse expanded
#:literals (begin)
#:literals (begin define-values)
[(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
(capture-actor-actions
(lambda () (set!-values (tmp ...) e))))
(define-values (x ...) (values tmp ...))
(syndicate-module (action-ids ... action-id) (forms ...)))]
[(head rest ...)
(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 ...)))))]
(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 (capture-actor-actions (lambda () #,expanded)))
(syndicate-module (action-ids ... action-id) (forms ...))))])]
[non-pair-syntax
#'(begin form (syndicate-module (action-ids ...) (forms ...)))])]
[(_ (action-ids ...) ())

View File

@ -1,12 +1,8 @@
#lang syndicate
(require (only-in racket/set
set
set-count
set-empty?
set-first
set-remove))
(require racket/set)
(require (only-in racket/list
first
partition
empty?
split-at))
@ -17,6 +13,7 @@
string-trim))
(require (only-in racket/sequence
sequence->list))
(require (only-in racket/function const))
(module+ test
(require rackunit))
@ -38,27 +35,31 @@ of each TaskManager (TM) is contingent on the presence of a job manager.
#|
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, we the JM
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
;; 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 Status), where 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.
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.
|#
(assertion-struct task-runner (id status))
(define IDLE 'idle)
(define OVERLOAD 'overload)
(struct executing (id) #:transparent)
@ -69,19 +70,22 @@ Task Delegation Protocol
Task Delegation has two roles, TaskAssigner (TA) and TaskPerformer (TP).
A TaskAssigner asserts the association of a Task with a particular TaskPerformer
through
(task-assignment ID ID Task)
where the first ID identifies the TP and the second identifies the job.
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-assignment (assignee job-id task))
(assertion-struct task-performance (assignee task desc))
#|
A Task is a (task ID Work), where Work is one of
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)
@ -89,11 +93,9 @@ A TaskResult is a (Hashof String Natural), counting the occurrences of words
(struct reduce-work (left right) #:transparent)
#|
The TaskPerformer responds to a task-assignment by describing its state with respect
The TaskPerformer responds to a request by describing its state with respect
to that task,
(task-state ID ID ID TaskStateDesc)
where the first ID is that of the TP, the second is that of the job,
and the third that of the 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)
@ -101,7 +103,6 @@ A TaskStateDesc is one of
- RUNNING, indicating that the task is being performed
- (finished TaskResult), describing the results
|#
(assertion-struct task-state (assignee job-id task-id desc))
(struct finished (data) #:transparent)
(define ACCEPTED 'accepted)
(define RUNNING 'running)
@ -115,11 +116,14 @@ TaskRunners.
Job Submission Protocol
-----------------------
Finally, Clients submit their jobs to the JobManager by asserting a Job, which is a (job ID (Listof Task)).
The JobManager then performs the job and, when finished, asserts (job-finished ID TaskResult)
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)
|#
(assertion-struct job (id tasks))
(assertion-struct job-finished (id data))
(struct job (id tasks) #:transparent)
(assertion-struct job-completion (id data result))
;; ---------------------------------------------------------------------------------------------------
;; Logging
@ -128,35 +132,64 @@ The JobManager then performs the job and, when finished, asserts (job-finished I
(displayln (apply format fmt args)))
;; ---------------------------------------------------------------------------------------------------
;; TaskRunner
;; Generic Implementation of Task Delegation Protocol
(define (spawn-task-runner)
(define id (gensym 'task-runner))
;; 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
(field [status IDLE])
(define (idle?) (equal? IDLE (status)))
(assert (task-runner id (status)))
(begin/dataflow
(log "task-runner ~v state is: ~a" id (status)))
(during (task-assignment id $job-id (task $tid $desc))
(field [execution-state (if (idle?) RUNNING OVERLOAD)]
[word-count (hash)])
(assert (task-state id job-id tid (execution-state)))
;; we have to avoid asking a non-idle runner to do anything
(when (idle?)
(on-stop (status IDLE))
(on-start
(status (executing tid))
;; since we currently finish everything in one turn, allow other actors to observe the changes in our
;; task-runner state by flushing pending actions.
(flush!)
(match desc
[(map-work data)
(word-count (count-new-words (word-count) (string->words data)))
(execution-state (finished (word-count)))]
[(reduce-work left right)
(word-count (hash-union left right #:combine +))
(execution-state (finished (word-count)))]))))))
(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)
@ -185,166 +218,202 @@ The JobManager then performs the job and, when finished, asserts (job-finished I
(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
;; currently fails, doesn't seem worth fixing
#;(check-equal? (string->words "but wait---there's more")
(list "but" "wait" "there's" "more")))
;; ---------------------------------------------------------------------------------------------------
;; TaskManager
(define (spawn-task-manager)
;; 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 learns about JM")
(define/query-set task-runners (task-runner $id _) id
#:on-add (log "TM learns about task-runner ~a" id))
;; I wonder just how inefficient this is
(define/query-set idle-runners (task-runner $id IDLE) id
#:on-add (log "TM learns that task-runner ~a is IDLE" id)
#:on-remove (log "TM learns that task-runner ~a is NOT IDLE" id))
(assert (task-manager id (set-count (idle-runners))))
(field [busy-runners (list)])
(during (task-assignment id $job-id $t)
(match-define (task task-id desc) t)
#;(on-start (log "TM receives task ~a" task-id))
(log "TM receives task ~a" task-id)
(on-stop (log "TM finished with task ~a" task-id))
(field [status ACCEPTED])
;; TODO - could delegate this assertion, in the non-overloaded case, to TaskRunner
;; (also removing the first id from task-state)
(assert (task-state id job-id task-id (status)))
(cond
[(set-empty? (idle-runners))
(log "TM can't run ~a right now" task-id)
(status OVERLOAD)]
[else
(define runner (set-first (idle-runners)))
;; n.b. modifying a query set is questionable
;; but if we wait for the IDLE assertion to be retracted, we might assign multiple tasks to the same runner.
;; Could use the busy-runners field to avoid that
(idle-runners (set-remove (idle-runners) runner))
(log "TM assigns task ~a to runner ~a" task-id runner)
(assert (task-assignment runner job-id t))
(status RUNNING)
(on (asserted (task-state runner job-id task-id $state))
(match state
[(or (== ACCEPTED)
(== RUNNING))
;; nothing to do
(void)]
[(== OVERLOAD)
(log "TM overloaded TR with task ~a" task-id)
(status OVERLOAD)]
[(finished results)
(log "TM receives the results of task ~a" task-id)
(status state)]))])))))
(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")
;; 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 $slots) id slots
#:on-add (log "JM learns that ~a has ~v slots" id slots))
(on-start
(react
;; (Hashof TaskManagerID Nat)
;; 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
(field [requests-in-flight (hash)])
(define (slots-available)
(for/sum ([(id v) (in-hash (task-managers))])
(max 0 (- v (hash-ref (requests-in-flight) id 0)))))
;; ID -> Void
;; mark that we have requested the given task manager to perform a task
(define (take-slot! id)
(log "JM assigns a task to ~a" id)
(requests-in-flight (hash-update (requests-in-flight) id add1 0)))
;; ID -> Void
;; mark that we have heard back from the given manager about a requested task
(define (received-answer! id)
(requests-in-flight (hash-update (requests-in-flight) id sub1)))
;; 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))
(during (job $job-id $tasks)
(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 [ready-tasks ready]
[waiting-tasks not-ready]
(field [waiting-tasks not-ready]
[tasks-in-progress 0])
(begin/dataflow
(define slots (slots-available))
(define-values (ts readys)
(split-at/lenient (ready-tasks) slots))
(for ([t ts])
(on-start (for [(t ready)] (add-ready-task! t)))
(on (realize (task-is-ready job-id $t))
(perform-task t push-results))
(unless (empty? ts)
;; the empty? check may be necessary to avoid a dataflow loop
(ready-tasks readys)))
;; Task -> Void
(define (add-ready-task! t)
;; TODO - use functional-queue.rkt from ../../
(log "JM marks task ~a as ready" (task-id t))
(ready-tasks (cons t (ready-tasks))))
(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)
(field [task-mngr #f])
(begin/dataflow
;; n.b. cyclic data-flow dependency
(unless (task-mngr)
(define mngr
(for/first ([(id slots) (in-hash (task-managers))]
#:when (positive? (- slots (hash-ref (requests-in-flight) id 0))))
id))
(when mngr
(take-slot! mngr)
(react (stop-when (asserted (task-state mngr job-id this-id _))
(received-answer! mngr)))
(task-mngr mngr))))
;; TODO - should respond if task manager dies
(assert #:when (task-mngr)
(task-assignment (task-mngr) job-id t))
(on #:when (task-mngr)
(asserted (task-state (task-mngr) job-id this-id $state))
(match state
[(or (== ACCEPTED)
(== RUNNING))
;; nothing to do
(void)]
[(== OVERLOAD)
;; 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" (task-mngr) this-id)
(task-mngr #f)]
[(finished results)
(log "JM receives the results of task ~a" this-id)
(stop-current-facet (k this-id results))]))))
(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? (ready-tasks))
(empty? (waiting-tasks)))
(log "JM finished with job ~a" job-id)
(react (assert (job-finished job-id data)))]
(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
@ -390,8 +459,7 @@ The JobManager then performs the job and, when finished, asserts (job-finished I
;; Job -> Void
(define (spawn-client j)
(spawn
(assert j)
(on (asserted (job-finished (job-id j) $data))
(on (asserted (job-completion (job-id j) (job-tasks j) $data))
(printf "job done!\n~a\n" data))))
;; ---------------------------------------------------------------------------------------------------
@ -401,7 +469,7 @@ The JobManager then performs the job and, when finished, asserts (job-finished I
(spawn
(during (job-manager-alive)
(during (task-manager $tm-id _)
(define/query-set requests (task-assignment tm-id _ (task $tid _)) tid)
(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))
@ -458,7 +526,7 @@ The JobManager then performs the job and, when finished, asserts (job-finished I
;; TaskTree -> (Listof Task)
;; flatten a task tree by assigning job-unique IDs
(define (task-tree->list tt)
(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
@ -467,7 +535,7 @@ The JobManager then performs the job and, when finished, asserts (job-finished I
[next-id 0])
(match tt
[(map-work _)
(values (list (task next-id tt))
(values (list (task (list next-id job-id) tt))
(add1 next-id))]
[(reduce-work left right)
(define left-id (add1 next-id))
@ -475,8 +543,8 @@ The JobManager then performs the job and, when finished, asserts (job-finished I
(loop left left-id))
(define-values (rights next)
(loop right right-id))
(values (cons (task next-id (reduce-work left-id right-id))
(append lefts rights))
(values (cons (task (list next-id job-id) (reduce-work left-id right-id))
(append lefts rights))
next)])))
tasks)
@ -484,7 +552,7 @@ The JobManager then performs the job and, when finished, asserts (job-finished I
(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)))
(define tasks (task-tree->list (create-task-tree input-lines) job-id))
(job job-id tasks))
;; String -> Job
@ -514,7 +582,7 @@ The JobManager then performs the job and, when finished, asserts (job-finished I
(task mid2 (map-work data2)))
(check-true (id? left))
(check-true (id? right))
(check-equal? (set left right) (set mid1 mid2))
(check-equal? (set left right) (set (first mid1) (first mid2)))
(check-equal? (set data1 data2)
(set "a b c" "d e f"))]
[_
@ -540,9 +608,12 @@ The JobManager then performs the job and, when finished, asserts (job-finished I
;; expected:
;; #hash((a . 5) (b . 5) (c . 2))
(spawn-client j)
(spawn-client (file->job "lorem.txt"))
(spawn-job-manager)
(spawn-task-manager)
(spawn-task-runner)
(spawn-task-runner)
(spawn-task-manager 2)
(spawn-task-manager 3)
(spawn-observer)
(module+ main
(void))

View File

@ -0,0 +1,61 @@
#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)))

View File

@ -0,0 +1,19 @@
#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)))

View File

@ -14,6 +14,7 @@
limit-patch
patch-step
patch-step*
patch-prepend
compute-aggregate-patch
apply-patch
update-interests
@ -125,6 +126,13 @@
(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

9
racket/typed/Makefile Normal file
View File

@ -0,0 +1,9 @@
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
check: pan
./pan -a -f

View File

@ -0,0 +1,406 @@
#lang turnstile
(provide bind
discard
ann
if
when
unless
let
let*
cond
else
match
tuple
unit
select
error
define-tuple
match-define
(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)
----------------------------------------
[ (error- 'bind "escaped") ( : (Bind τ))])
(define-typed-syntax discard
[_
--------------------
[ (error- 'discard "escaped") ( : Discard)]])
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Core-ish forms
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; copied from stlc
(define-typed-syntax (ann e (~optional (~datum :)) τ:type)
[ e e- ( : τ.norm)]
#:fail-unless (pure? #'e-) "expression must be pure"
------------------------------------------------
[ e- ( : τ.norm) ])
;; 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)
( ν-ep (~effs eps1 ...)) ( ν-f (~effs fs1 ...)) ( ν-s (~effs ss1 ...))]
[ e2 e2- ( : τ-expected)
( ν-ep (~effs eps2 ...)) ( ν-f (~effs fs2 ...)) ( ν-s (~effs ss2 ...))]
--------
[ (if- e_tst- e1- e2-)
( : τ-expected)
( ν-ep (eps1 ... eps2 ...))
( ν-f #,(make-Branch #'((fs1 ...) (fs2 ...))))
( ν-s (ss1 ... ss2 ...))]]
[(_ 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)
( ν-ep (~effs eps1 ...)) ( ν-f (~effs fs1 ...)) ( ν-s (~effs ss1 ...))]
[ e2 e2- ( : τ2)
( ν-ep (~effs eps2 ...)) ( ν-f (~effs fs2 ...)) ( ν-s (~effs ss2 ...))]
#:with τ (mk-U- #'(τ1 τ2))
--------
[ (if- e_tst- e1- e2-) ( : τ)
( ν-ep (eps1 ... eps2 ...))
( ν-f #,(make-Branch #'((fs1 ...) (fs2 ...))))
( ν-s (ss1 ... ss2 ...))]])
(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] ... (begin e_body ...) e_body- ( : τ_expected)
( ν-ep (~effs eps ...))
( ν-f (~effs fs ...))
( ν-s (~effs ss ...))]
----------------------------------------------------------
[ (let- ([x- e-] ...) e_body-) ( : τ_expected)
( ν-ep (eps ...))
( ν-f (fs ...))
( ν-s (ss ...))]]
[(_ ([x e] ...) e_body ...)
[ e e- : τ_x] ...
#:fail-unless (stx-andmap pure? #'(e- ...)) "expressions must be pure"
[[x x- : τ_x] ... (begin e_body ...) e_body- ( : τ_body)
( ν-ep (~effs eps ...))
( ν-f (~effs fs ...))
( ν-s (~effs ss ...))]
----------------------------------------------------------
[ (let- ([x- e-] ...) e_body-) ( : τ_body)
( ν-ep (eps ...))
( ν-f (fs ...))
( ν-s (ss ...))]])
;; copied from ext-stlc
(define-typed-syntax let*
[(_ () e_body ...)
--------
[ (begin 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"
[ (begin s ...) s- ( : τ-s)
( ν-ep (~effs eps ...))
( ν-f (~effs fs ...))
( ν-s (~effs ss ...))] ...
------------------------------------------------
[ (cond- [pred- s-] ...) ( : (U τ-s ...))
( ν-ep (eps ... ...))
( ν-f #,(make-Branch #'((fs ...) ...)))
( ν-s (ss ... ...))])
(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] ... (begin s ...) s- ( : τ-s)
( ν-ep (~effs eps ...))
( ν-f (~effs fs ...))
( ν-s (~effs ss ...))] ...
;; 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 ...))
( ν-ep #,(make-Branch #'((eps ...) ...)))
( ν-f #,(make-Branch #'((fs ...) ...)))
( ν-s #,(make-Branch #'((ss ...) ...)))])
(define-typed-syntax (tuple e:expr ...)
[ e e- ( : τ)] ...
#:fail-unless (stx-andmap pure? #'(e- ...)) "expressions not allowed to have effects"
-----------------------
[ (#%app- list- 'tuple e- ...) ( : (Tuple τ ...))])
(define unit : Unit (tuple))
(define-typed-syntax (select n:nat e:expr)
[ e e- ( : (~Tuple τ ...))]
#:fail-unless (pure? #'e-) "expression not allowed to have effects"
#: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)])
(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 τ] ... ...)]
#;[(k:kons1 p)
(pat-bindings #'p)]
[(~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 ...))))]
[(k:kons1 p)
(quasisyntax/loc pat
(k #,(elaborate-pattern #'p)))]
[(~constructor-exp ctor p ...)
(quasisyntax/loc pat
(ctor #,@(stx-map elaborate-pattern #'(p ...))))]
[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
(quasisyntax/loc pat (bind x.id #,ty))]
[($ x:id ty)
(syntax/loc pat (bind x ty))]
[($ x:id)
(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 ...)
(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 ...)))]
#;[(k:kons1 p)
#`(#,(kons1->constructor #'k) #,(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"
#:fail-unless (pure? #'e-) "expr must be pure"
#: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)
------------------------------------------------------------
)

1547
racket/typed/core-types.rkt Normal file

File diff suppressed because it is too large Load Diff

34
racket/typed/either.rkt Normal file
View File

@ -0,0 +1,34 @@
#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 ([acc (Tuple (List Y) (List Z)) (tuple (list) (list))])
([x xs])
(define y-or-z (pred x))
(match y-or-z
[(left (bind y Y))
(tuple (cons y (select 0 acc))
(select 1 acc))]
[(right (bind z Z))
(tuple (select 0 acc)
(cons z (select 1 acc)))])))

View File

@ -47,34 +47,35 @@
(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 (Know (Observe (BookQuoteT String ★/t)))
(Reacts (Asserted (Observe (BookQuoteT String ★/t)))
(Role (_)
;; nb no mention of retracting this assertion
(Shares (BookQuoteT String Int))))))
(define (spawn-seller [inventory : Inventory])
(spawn τc
(begin
(start-facet seller
(field [books Inventory inventory])
;; Give quotes to interested parties.
(during (observe (book-quote (bind title String) discard))
(during (observe (book-quote $title _))
;; TODO - lookup
(assert (book-quote title (lookup title (ref books))))))))
(assert (book-quote title (lookup title (ref books)))))))))
(define-type-alias leader-role
(Role (leader)
(Reacts (Know (BookQuoteT String Int))
(Reacts (Asserted (BookQuoteT String Int))
(Role (poll)
(Reacts (Know (BookInterestT String String Bool))
(Reacts (Asserted (BookInterestT String String Bool))
;; this is actually implemented indirectly through dataflow
(U (Stop leader
(Role (_)
@ -83,7 +84,7 @@
(define-type-alias leader-actual
(Role (get-quotes31)
(Reacts (Know (BookQuoteT String (Bind Int)))
(Reacts (Asserted (BookQuoteT String (Bind Int)))
(Stop get-quotes)
(Role (poll-members36)
(Reacts OnDataflow
@ -92,12 +93,12 @@
(Stop get-quotes
(Role (announce39)
(Shares (BookOfTheMonthT 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))))))
(Reacts (Retracted (BookInterestT String (Bind String) Bool)))
(Reacts (Asserted (BookInterestT String (Bind String) Bool)))
(Reacts (Retracted (BookInterestT String (Bind String) Bool)))
(Reacts (Asserted (BookInterestT String (Bind String) Bool)))))
(Reacts (Retracted (ClubMemberT (Bind String))))
(Reacts (Asserted (ClubMemberT (Bind String))))))
(define (spawn-leader [titles : (List String)])
(spawn τc
@ -115,10 +116,10 @@
(set! book-list (rest (ref book-list)))]))
;; keep track of book club members
(define/query-set members (club-member (bind name String)) name
(define/query-set members (club-member $name) name
#;#:on-add #;(printf "leader acknowledges member ~a\n" name))
(on (asserted (book-quote (ref title) (bind quantity Int)))
(on (asserted (book-quote (ref title) $quantity))
(printf "leader learns that there are ~a copies of ~a\n" quantity (ref title))
(cond
[(< quantity (+ 1 (set-count (ref members))))
@ -127,9 +128,22 @@
[#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 (ref title) (bind name String) #t) name)
(define/query-set nays (book-interest (ref title) (bind name String) #f) name)
(begin/dataflow
(define/query-set yays (book-interest (ref title) $name #t) name)
(define/query-set nays (book-interest (ref title) $name #f) name)
(on (asserted (book-interest (ref title) $name _))
;; count the leader as a 'yay'
(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 (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))))
;; begin/dataflow is a problem for simulation checking
#;(begin/dataflow
;; count the leader as a 'yay'
(when (>= (set-count (ref yays))
(/ (set-count (ref members)) 2))
@ -146,21 +160,22 @@
(Role (member)
(Shares (ClubMemberT String))
;; should this be the type of the pattern? or lowered to concrete types?
(Reacts (Know (Observe (BookInterestT String ★/t ★/t)))
(Reacts (Asserted (Observe (BookInterestT String ★/t ★/t)))
(Role (_)
(Shares (BookInterestT String String Bool))))))
(define (spawn-club-member [name : String]
[titles : (List String)])
(spawn τc
(print-role
(start-facet member
;; assert our presence
(assert (club-member name))
;; respond to polls
(during (observe (book-interest (bind title String) discard discard))
(during (observe (book-interest $title _ _))
(define answer (member? title titles))
(printf "~a responds to suggested book ~a: ~a\n" name title answer)
(assert (book-interest title name answer))))))
(assert (book-interest title name answer)))))))
(run-ground-dataspace τc
(spawn-seller (list (tuple "The Wind in the Willows" 5)

View File

@ -0,0 +1,132 @@
#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)

View File

@ -0,0 +1,530 @@
#lang typed/syndicate/roles
;; ---------------------------------------------------------------------------------------------------
;; 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.
|#
(define-type-alias TaskAssigner
(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 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 ★/t))
(TaskManager ID Int)
(Observe (TaskManager ★/t ★/t))
(JobCompletion ID (List InputTask) TaskResult)
(Observe (JobCompletion ID (List InputTask) ★/t))
(Observe (Observe (JobCompletion ★/t ★/t ★/t)))))
;; ---------------------------------------------------------------------------------------------------
;; 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
(begin
(start-facet runner
(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
(begin
(start-facet tm
(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 -> Bool
;; Test if the task is ready to run
(define (task-ready? [t : PendingTask] -> (Maybe ConcreteTask))
(match t
[(task $tid (map-work $s))
;; having to re-produce this is directly bc of no occurrence typing
(some (task tid (map-work s)))]
[(task $tid (reduce-work (right $v1)
(right $v2)))
(some (task tid (reduce-work v1 v2)))]
[_
none]))
;; Task Int Any -> Task
;; If the given task is waiting for this data, replace the waiting ID with the data
(define (task+data [t : PendingTask]
[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)))
(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
(begin
(start-facet jm
(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
#:roles (ρ))]))
(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! : (→fn ★/t)])
(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))
(perform-task t push-results)))
(for ([t (in-list ready)])
(add-ready-task! t))))))))
;; ---------------------------------------------------------------------------------------------------
;; Client
;; Job -> Void
(define (spawn-client [j : JobDesc])
(spawn τc
(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)))

View File

@ -0,0 +1,88 @@
#lang typed/syndicate/roles
;; 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)))))))))))))))))
)

View File

@ -0,0 +1,48 @@
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.

View File

@ -0,0 +1,27 @@
#lang typed/syndicate/roles
;; 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)))))
)

View File

@ -0,0 +1,36 @@
#lang typed/syndicate/roles
;; 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))))))

View File

@ -62,7 +62,7 @@
(define-type-alias seller-role
(Role (seller)
(Reacts (Know (Observe (QuoteT String ★/t)))
(Reacts (Asserted (Observe (QuoteT String ★/t)))
(Role (_)
(Shares (QuoteT String Int))))))

219
racket/typed/for-loops.rkt Normal file
View File

@ -0,0 +1,219 @@
#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" Bool + #%datum))
(require (only-in "core-expressions.rkt" let unit))
(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-typed-syntax for/fold
[(for/fold ([acc:id (~optional (~datum :)) τ-acc init])
(clause:iter-clause
...)
e-body ...+)
[ init init- ( : τ-acc)]
#:fail-unless (pure? #'init-) "expression must be pure"
#:with (clauses- ([x x- τ] ...)) (analyze-for-clauses #'(clause.parend ...))
[[x x-- : τ] ...
[acc acc- : τ-acc] (begin e-body ...) e-body-
( : τ-acc)
( ν-ep (~effs τ-ep ...))
( ν-s (~effs τ-s ...))
( ν-f (~effs τ-f ...))]
#:with e-body-- (substs #'(x- ...) #'(x-- ...) #'e-body- free-identifier=?)
-------------------------------------------------------
[ (for/fold- ([acc- init-])
clauses-
e-body--)
( : τ-acc)
( ν-ep (τ-ep ...))
( ν-s (τ-s ...))
( ν-f (τ-f ...))]]
[(for/fold ([acc:id init])
clauses
e-body ...+)
[ init _ ( : τ-acc)]
---------------------------------------------------
[ (for/fold ([acc τ-acc init])
clauses
e-body ...)]])
(define-typed-syntax (for/list (clause:iter-clause ...)
e-body ...+)
#:with (clauses- ([x x- τ] ...)) (analyze-for-clauses #'(clause.parend ...))
[[x x-- : τ] ... (begin e-body ...) e-body-
( : τ-body)
( ν-ep (~effs τ-ep ...))
( ν-s (~effs τ-s ...))
( ν-f (~effs τ-f ...))]
#:with e-body-- (substs #'(x- ...) #'(x-- ...) #'e-body- free-identifier=?)
----------------------------------------------------------------------
[ (for/list- clauses-
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-- : τ] ... (begin e-body ...) e-body-
( : τ-body)
( ν-ep (~effs τ-ep ...))
( ν-s (~effs τ-s ...))
( ν-f (~effs τ-f ...))]
#:with e-body-- (substs #'(x- ...) #'(x-- ...) #'e-body- free-identifier=?)
----------------------------------------------------------------------
[ (for/set- clauses-
e-body--) ( : (Set τ-body))
( ν-ep (τ-ep ...))
( ν-s (τ-s ...))
( ν-f (τ-f ...))])
(define-typed-syntax (for/sum (clause ...)
e-body ...+)
----------------------------------------------------------------------
[ (for/fold ([acc 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-- : τ] ... (begin e-body ...) e-body-
( : τ-body)
( ν-ep (~effs τ-ep ...))
( ν-s (~effs τ-s ...))
( ν-f (~effs τ-f ...))]
#:with e-body-- (substs #'(x- ...) #'(x-- ...) #'e-body- free-identifier=?)
[[res _ : τ-body] res res- ( : _)]
----------------------------------------------------------------------
[ (let- ()
(define- res-
(for/first- clauses-
e-body--))
(if- res-
(some res-)
none))
( : (Maybe τ-body))
( ν-ep (τ-ep ...))
( ν-s (τ-s ...))
( ν-f (τ-f ...))])

84
racket/typed/hash.rkt Normal file
View File

@ -0,0 +1,84 @@
#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)
(begin-for-syntax
(define-splicing-syntax-class key-val-list
#:attributes (items)
(pattern (~seq k1 v1 rest:key-val-list)
#:attr items #`((k1 v1) #,@#'rest.items))
(pattern (~seq)
#:attr items #'())))
(define-typed-syntax (hash keys&vals:key-val-list)
#:with ((key val) ...) #'keys&vals.items
[ key key- ( : τ-k)] ...
[ val val- ( : τ-val)] ...
#:fail-unless (all-pure? #'(key- ... val- ...)) "gotta be pure"
#:with together-again (stx-flatten #'((key- val-) ...))
--------------------------------------------------
[ (#%app- hash- #,@#'together-again) ( : (Hash (U τ-k ...) (U τ-val ...)))])
(require/typed racket/base
;; don't have a type for ConsPair
#;[make-hash : ( (K V) (→fn (List (ConsPair K V)) (Hash K V)))]
[hash-set : ( (K V) (→fn (Hash K V) K V (Hash K V)))]
[hash-ref : ( (K V) (→fn (Hash K V) K V))]
;; TODO hash-ref/failure
[hash-has-key? : ( (K V) (→fn (Hash K V) K Bool))]
[hash-update : ( (K V) (→fn (Hash K V) K (→fn V V) (Hash K V)))]
;; TODO hash-update/failure
[hash-remove : ( (K V) (→fn (Hash K V) K (Hash K V)))]
[hash-map : ( (K V R) (→fn (Hash K V) (→fn K V R) (List R)))]
[hash-keys : ( (K V) (→fn (Hash K V) (List K)))]
[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))))]
;; TODO - hash-union with #:combine
)
(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))

8
racket/typed/info.rkt Normal file
View File

@ -0,0 +1,8 @@
#lang info
(define compile-omit-paths
'("examples"
"tests"))
(define test-omit-paths
'("examples/roles/chat-tcp2.rkt"))

View File

@ -0,0 +1,174 @@
/* 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)
*/
}

33
racket/typed/list.rkt Normal file
View File

@ -0,0 +1,33 @@
#lang turnstile
(provide List
(for-syntax ~List)
list
(typed-out [[cons- : ( (X) (→fn X (List X) (List X)))] cons]
[[first- : ( (X) (→fn (List X) X))] first]
[[second- : ( (X) (→fn (List X) X))] second]
[[rest- : ( (X) (→fn (List X) (List X)))] rest]
[[member?- ( (X) (→fn X (List X) Bool))] member?]
[[empty?- ( (X) (→fn (List X) Bool))] empty?]
[[reverse- ( (X) (→fn (List X) (List X)))] reverse]
[[partition- ( (X) (→fn (List X) (→fn X Bool) (List X)))] partition]
[[map- ( (X Y) (→fn (→fn X Y) (List X) (List Y)))] map]))
(require "core-types.rkt")
(require (only-in "prim.rkt" Bool))
(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))

37
racket/typed/maybe.rkt Normal file
View File

@ -0,0 +1,37 @@
#lang turnstile
(provide Maybe
None
None*
Some
some
none)
(require "core-types.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")]))

114
racket/typed/prim.rkt Normal file
View File

@ -0,0 +1,114 @@
#lang turnstile
(provide (all-defined-out)
(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)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Primitives
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define-base-types Int Bool String ByteString Symbol)
;; hmmm
(define-primop + ( Int Int (Computation (Value Int) (Endpoints) (Roles) (Spawns))))
(define-primop - ( Int Int (Computation (Value Int) (Endpoints) (Roles) (Spawns))))
(define-primop * ( Int Int (Computation (Value Int) (Endpoints) (Roles) (Spawns))))
(define-primop not ( Bool (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
(define-primop < ( Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
(define-primop > ( Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
(define-primop <= ( Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
(define-primop >= ( Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
(define-primop = ( Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
(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 bytes->string/utf-8 ( ByteString (Computation (Value String) (Endpoints) (Roles) (Spawns))))
(define-primop string->bytes/utf-8 ( String (Computation (Value ByteString) (Endpoints) (Roles) (Spawns))))
(define-primop gensym ( Symbol (Computation (Value Symbol) (Endpoints) (Roles) (Spawns))))
(define-primop symbol->string ( Symbol (Computation (Value String) (Endpoints) (Roles) (Spawns))))
(define-primop string->symbol ( String (Computation (Value Symbol) (Endpoints) (Roles) (Spawns))))
(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)])
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Basic Values
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define-typed-syntax #%datum
[(_ . n:integer)
----------------
[ (#%datum- . n) ( : Int)]]
[(_ . b:boolean)
----------------
[ (#%datum- . b) ( : Bool)]]
[(_ . s:string)
----------------
[ (#%datum- . s) ( : String)]])
(define-typed-syntax (typed-quote x:id)
-------------------------------
[ (quote- x) ( : Symbol)])

2856
racket/typed/proto.rkt Normal file

File diff suppressed because it is too large Load Diff

File diff suppressed because it is too large Load Diff

74
racket/typed/sequence.rkt Normal file
View File

@ -0,0 +1,74 @@
#lang turnstile
(provide Sequence
(for-syntax ~Sequence)
empty-sequence
sequence->list
sequence-length
sequence-ref
sequence-tail
sequence-append
sequence-map
sequence-andmap
sequence-ormap
sequence-fold
sequence-count
sequence-filter
sequence-add-between
in-list
in-set
in-range
)
(require "core-types.rkt")
(require (only-in "list.rkt" List))
(require (only-in "set.rkt" Set))
(require (only-in "prim.rkt" Int Bool))
#;(require (postfix-in - racket/sequence))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Sequences
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define-container-type Sequence #:arity = 1)
(require/typed racket/sequence
[empty-sequence : (Sequence (U))]
[sequence->list : ( (X) (→fn (Sequence X) (List X)))]
[sequence-length : ( (X) (→fn (Sequence X) Int))]
[sequence-ref : ( (X) (→fn (Sequence X) Int Int))]
[sequence-tail : ( (X) (→fn (Sequence X) Int (Sequence X)))]
[sequence-append : ( (X) (→fn (Sequence X) (Sequence X) (Sequence X)))]
[sequence-map : ( (A B) (→fn (→fn A B) (Sequence A) (Sequence B)))]
[sequence-andmap : ( (X) (→fn (→fn X Bool) (Sequence X) Bool))]
[sequence-ormap : ( (X) (→fn (→fn X Bool) (Sequence X) Bool))]
;; sequence-for-each omitted until a better accounting of effects (TODO)
[sequence-fold : ( (A B) (→fn (→fn A B A) (Sequence B) A))]
[sequence-count : ( (X) (→fn (→fn X Bool) (Sequence X) Int))]
[sequence-filter : ( (X) (→fn (→fn X Bool) (Sequence X) (Sequence X)))]
[sequence-add-between : ( (X) (→fn (Sequence X) X (Sequence X)))])
(require/typed racket/base
[in-list : ( (X) (→fn (List X) (Sequence X)))]
[in-range : (→fn Int (Sequence Int))])
(require/typed racket/set
[in-set : ( (X) (→fn (Set X) (Sequence X)))])
#;(define-typed-syntax empty-sequence
[_
--------------------
[ empty-sequence- ( : (Sequence (U)))]])
;; er, this is making everything a macro, as opposed to a procedure...
;; think I ought to add polymorphous first :\
#;(define-typed-syntax (sequence->list s)
[ s s- ( : (~Sequence τ))]
#:fail-unless (pure? #'s-)
------------------------------
[ (sequence->list- s-) ( : (List τ))])
#;(define-typed-syntax (sequence-length s)
[ s s- ( : (~Sequence τ))]
#:fail-unless (pure? #'s-)
------------------------------
[ (sequence-length- s-) ( : Int)])

105
racket/typed/set.rkt Normal file
View File

@ -0,0 +1,105 @@
#lang turnstile
(provide Set
(for-syntax ~Set)
set
set-member?
set-add
set-remove
set-count
set-union
set-subtract
set-intersect
list->set
set->list
(typed-out [[set-first- : ( (X) (→fn (Set X) X))]
set-first]
[[set-empty?- : ( (X) (→fn (Set X) Bool))]
set-empty?]))
(require "core-types.rkt")
(require (only-in "prim.rkt" Int Bool))
(require (only-in "list.rkt" ~List))
(require (postfix-in - racket/set))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Sets
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define-container-type Set #:arity = 1)
(define-typed-syntax (set e ...)
[ e e- τ] ...
#:fail-unless (all-pure? #'(e- ...)) "expressions must be pure"
---------------
[ (#%app- set- e- ...) (Set (U τ ...))])
(define-typed-syntax (set-count e)
[ e e- (~Set _)]
#:fail-unless (pure? #'e-) "expression must be pure"
----------------------
[ (#%app- set-count- e-) Int])
(define-typed-syntax (set-add st v)
[ st st- (~Set τs)]
#:fail-unless (pure? #'st-) "expression must be pure"
[ v v- τv]
#:fail-unless (pure? #'v-) "expression must be pure"
-------------------------
[ (#%app- set-add- st- v-) (Set (U τs τv))])
(define-typed-syntax (set-remove st v)
[ st st- (~Set τs)]
#:fail-unless (pure? #'st-) "expression must be pure"
[ v v- τs]
#:fail-unless (pure? #'v-) "expression must be pure"
-------------------------
[ (#%app- set-remove- st- v-) (Set τs)])
(define-typed-syntax (set-member? st v)
[ st st- (~Set τs)]
#:fail-unless (pure? #'st-) "expression must be pure"
[ v v- τv]
#:fail-unless (pure? #'v-) "expression must be pure"
#:fail-unless (<: #'τv #'τs)
"type mismatch"
-------------------------------------
[ (#%app- set-member?- st- v-) Bool])
(define-typed-syntax (set-union st0 st ...)
[ st0 st0- (~Set τ-st0)]
#:fail-unless (pure? #'st0-) "expression must be pure"
[ st st- (~Set τ-st)] ...
#:fail-unless (all-pure? #'(st- ...)) "expressions must be pure"
-------------------------------------
[ (#%app- set-union- st0- st- ...) (Set (U τ-st0 τ-st ...))])
(define-typed-syntax (set-intersect st0 st ...)
[ st0 st0- (~Set τ-st0)]
#:fail-unless (pure? #'st0-) "expression must be pure"
[ st st- (~Set τ-st)] ...
#:fail-unless (all-pure? #'(st- ...)) "expressions must be pure"
#:with τr ( #'τ-st0 (type-eval #'(U τ-st ...)))
-------------------------------------
[ (#%app- set-intersect- st0- st- ...) (Set τr)])
(define-typed-syntax (set-subtract st0 st ...)
[ st0 st0- (~Set τ-st0)]
#:fail-unless (pure? #'st0-) "expression must be pure"
[ st st- (~Set _)] ...
#:fail-unless (all-pure? #'(st- ...)) "expressions must be pure"
-------------------------------------
[ (#%app- set-subtract- st0- st- ...) (Set τ-st0)])
(define-typed-syntax (list->set l)
[ l l- (~List τ)]
#:fail-unless (pure? #'l-) "expression must be pure"
-----------------------
[ (#%app- list->set- l-) (Set τ)])
(define-typed-syntax (set->list s)
[ s s- (~Set τ)]
#:fail-unless (pure? #'s-) "expression must be pure"
-----------------------
[ (#%app- set->list- s-) (List τ)])

View File

@ -0,0 +1,11 @@
#lang typed/syndicate/roles
(run-ground-dataspace (U)
(spawn (U)
(start-facet x
(field [y Int 0])
(define/dataflow x (add1 (ref y)))
(displayln (add1 (ref x)))
;; print 2
#f))
)

View File

@ -0,0 +1,17 @@
#lang typed/syndicate/roles
(require rackunit/turnstile)
(define ( (ρ) (assert-something! [p : (proc ★/t #:endpoints (ρ))]))
(p))
(define (test-fun)
(call/inst assert-something! (lambda () (assert 5))))
(check-type test-fun : (proc ★/t #:endpoints ((Shares Int))))
(define (test-call/inst-insertion)
(assert-something! (lambda () (assert 5))))
(check-type test-call/inst-insertion : (proc ★/t #:endpoints ((Shares Int))))

View File

@ -0,0 +1,93 @@
#lang typed/syndicate/roles
(require rackunit/turnstile)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Type Abstraction
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define id
(Λ [τ]
(lambda ([x : τ])
x)))
(check-type id : ( (τ) (→fn τ τ)))
(check-type ((inst id Int) 1)
: Int
1)
(check-type ((inst id String) "hello")
: String
"hello")
(define poly-first
(Λ [τ σ]
(lambda ([t : (Tuple τ σ)])
(select 0 t))))
(check-type poly-first : ( (A B) (→fn (Tuple A B) A)))
(check-type ((inst poly-first Int String) (tuple 13 "XD"))
: Int
13)
(check-type ((inst poly-first Int String) (tuple 13 "XD"))
: Int
13)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Polymorphic Definitions
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define ( (X) (id2 [x : X] -> X))
x)
(check-type ((inst id2 Int) 42)
: Int
42)
(define ( (X) (id3 [x : X]))
x)
(check-type (+ ((inst id3 Int) 42) 1)
: Int
43)
;; test type variable scoping
(define ( (X) (id4 [x : X] -> X))
(match x
[(bind y X) y]))
(check-type ((inst id2 String) "shelly flowers")
: String
"shelly flowers")
(define id5
(Λ [τ]
(lambda ([x : τ])
(match x
[(bind y τ) y]))))
(typecheck-fail (inst id5 (→fn Int Int))
#:with-msg "types must be instantiable")
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Shorthands for match
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(check-type (match 5
[$x:Int (add1 x)])
: Int
6)
(check-type (match (tuple 3 "hello")
[(tuple _ $str:String)
str])
: String
"hello")
(check-type (match (tuple 3 "hello")
[(tuple _ $str)
str])
: String
"hello")

View File

@ -0,0 +1,9 @@
#lang typed/syndicate/roles
(require rackunit/turnstile)
;; TODO - currently fails with a racket error. Is that OK?
;; (ideally, this would fail with a better error message)
(typecheck-fail
(let ([x (define y 5)])
(add1 1)))

View File

@ -0,0 +1,103 @@
#lang typed/syndicate/roles
(require rackunit/turnstile)
(check-type (for/fold ([x 0])
([y (list 1 2 3)])
x)
: Int
0)
(check-type (for/fold ([x 0])
([y (list 1 2 3)])
y)
: Int
3)
(define-type-alias Inventory (List (Tuple String Int)))
(define inventory0 (list (tuple "The Wind in the Willows" 5)
(tuple "Catch 22" 2)
(tuple "Candide" 33)))
(check-type (for/fold ([stock 0])
([item inventory0])
(select 1 item))
: Int
33)
(check-type (for/fold ([stock 0])
([item inventory0])
(if (equal? "Catch 22" (select 0 item))
(select 1 item)
stock))
: Int
2)
(define (lookup [title : String]
[inv : Inventory] -> Int)
(for/fold ([stock 0])
([item inv])
(if (equal? title (select 0 item))
(select 1 item)
stock)))
(check-type lookup : (→fn String Inventory Int))
(define (zip [xs : (List Int)]
[ys : (List Int)])
((inst reverse (Tuple Int Int))
(for/fold ([acc : (List (Tuple Int Int))
(list)])
([x xs]
[y ys])
(cons (tuple x y) acc))))
(check-type (zip (list 1 2 3) (list 4 5 6))
: (List (Tuple Int Int))
(list (tuple 1 4) (tuple 2 5) (tuple 3 6)))
(define (zip-even [xs : (List Int)]
[ys : (List Int)])
((inst reverse (Tuple Int Int))
(for/fold ([acc : (List (Tuple Int Int))
(list)])
([x xs]
#:when (even? x)
[y ys]
#:unless (odd? y))
(cons (tuple x y) acc))))
(check-type (zip-even (list 1 2 3) (list 5 6 7))
: (List (Tuple Int Int))
(list (tuple 2 6)))
(check-type (for/list ([x (list 1 2 3 4 5 6)]
#:when (even? x))
(add1 x))
: (List Int)
(list 3 5 7))
(check-type (for/set ([x (set 1 2 3 4 5 6)]
#:when (even? x))
(add1 x))
: (Set Int)
(set 5 3 7))
(check-type (for/sum ([x (set 8 7 2)])
(* x 2))
: Int
34)
(check-type (for/first ([x (list 1 2 3 4 5)]
#:when (even? x))
x)
: (Maybe Int)
(some 2))
(check-type (for/first ([x (list 1 2 3 4 5)]
#:when (and (even? x)
(< x 2)))
x)
: (Maybe Int)
none)

View File

@ -0,0 +1,34 @@
#lang typed/syndicate/roles
(require rackunit/turnstile)
(check-type (hash) : (Hash (U) (U)))
(check-type (hash 1 2) : (Hash Int Int))
(check-type (hash "greetings" 8) : (Hash String Int))
(check-type (hash "smelly" 0
"feet" 18
"robust" 9)
: (Hash String Int))
(check-type (hash "smelly" 0
"feet" "grosss"
"robust" #t)
: (Hash String (U Int String Bool)))
(define a-hash
(hash "smelly" 0
"feet" 18
"robust" 9))
(define hash-ref/inst (inst hash-ref String Int))
(check-type (hash-ref/inst a-hash "smelly")
: Int
0)
(check-type ((inst hash-count String Int) a-hash)
: Int
3)

View File

@ -0,0 +1,49 @@
#lang typed/syndicate/roles
(require rackunit/turnstile)
(define ( (X) (poly-cons [x : X]
[xs : (List X)]
-> (List X)))
(cons x xs))
(define int-list : (List Int) (list 1 2 3))
(check-type (poly-cons 0 int-list)
: (List Int)
-> (list 0 1 2 3))
(define string-list : (List String) (list "group" "of" "helpful" "badgers"))
(check-type (poly-cons "a" string-list)
: (List String)
-> (list "a" "group" "of" "helpful" "badgers"))
(typecheck-fail (poly-cons "hello" int-list))
(define string-int-list : (List (U String Int))
(list "hi" 42 "badgers"))
;; fails because unification is too strict, requiring equality as opposed to
;; upper&lower bounds
(check-type (poly-cons (ann "go" (U String Int)) string-int-list)
: (List (U String Int)))
(typecheck-fail (poly-cons "go" string-int-list))
(typecheck-fail (poly-cons (lambda () 0) (ann (list) (List (→fn Int))))
#:with-msg "type variables must be flat and finite")
;; Failure because inference doesn't handle variables under unions
(define ( (X) (unwrap! [x : (Maybe X)] -> X))
(match x
[(some (bind v X))
v]
[none
(error "none")]))
(typecheck-fail (unwrap! (some 5))
#:with-msg "can't infer types with unions")
(check-type ((inst unwrap! Int) (some 5))
: Int
-> 5)

View File

@ -0,0 +1,20 @@
#lang typed/syndicate/roles
(require rackunit/turnstile)
(define-type-alias τc
(U (Tuple Int)
(Observe (Tuple ★/t))))
;; I actually think this is OK, since elaborating the pattern inserts a type
;; that will still be checked by `project-safe?`
(check-type (lambda ()
(spawn τc
(begin
(define (on!)
(on (asserted (tuple $x))
#f))
(start-facet x
(on!)))))
: (proc -> ★/t #:spawns ((Actor τc))))

View File

@ -0,0 +1,21 @@
#lang typed/syndicate/roles
(require rackunit/turnstile)
;; make sure that we can look at the type of the facet without the ρ in it
(check-type
(role-strings
(start-facet x
(define (push-results)
(cond
[(zero? 0)
(start-facet done (assert #t))]
[else
#f]))
(define ( (ρ) (perform-task [k : (proc -> ★/t #:roles (ρ))]))
(start-facet perform
(on start (stop perform (k)))))
(on start (call/inst perform-task push-results))))
: (List String)
-> (list
"(Role (x) (Reacts OnStart (Role (perform) (Reacts OnStart (Stop perform (Branch (Effs (Role (done) (Shares Bool))) (Effs)))))))"))

View File

@ -0,0 +1,27 @@
#lang typed/syndicate/roles
(require rackunit/turnstile)
(check-type (or #f #t)
: Bool
#t)
(check-type (and #t #f)
: Bool
#f)
(check-type (or)
: Bool
#f)
(check-type (and)
: Bool
#t)
(check-type (or #f #f #f #f #f #t)
: Bool
#t)
(check-type (and #t #t #t #t #t #f)
: Bool
#f)

View File

@ -0,0 +1,31 @@
#lang typed/syndicate/roles
(require rackunit/turnstile)
(define-type-alias WordCount (Hash String Int))
(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)))
(check-type (count-new-words (hash) (list "hi" "bye"))
: WordCount
(hash "bye" 1 "hi" 1))
;; OG error:
; <pkgs>/syndicate/typed/tests/regression-count-new-words.rkt:20.4: #%app: bad syntax
; in: (#%app word-count-increment result word)
;; turns out I needed a #:cut in the rule for #%app (even tho it was the last
;; syntax-parse case??)

View File

@ -0,0 +1,17 @@
#lang typed/syndicate/roles
(require rackunit/turnstile)
(check-type
(begin
(field [boo Int 0])
(define x (begin (send! "hi") 5))
;; relying on `set` not allowing effects for this to be a good test
(set! boo x)
3)
: Int)
;; Used to get the error:
; <pkgs>/syndicate/typed/tests/define-with-effects.rkt:10.2: set!: expression not allowed to have effects
; at: (set! boo x)
; in: (set! boo x)

View File

@ -0,0 +1,17 @@
#lang typed/syndicate/roles
(require rackunit/turnstile)
(check-type empty-sequence : (Sequence (U)))
(check-type (sequence-length empty-sequence)
: Int
0)
(define sequence-length/Int (inst sequence-length Int))
(define sequence->list/Int (inst sequence->list Int))
(define in-list/Int (inst in-list Int))
(check-type (sequence->list/Int (in-list/Int (list 3 9 20)))
: (List Int)
(list 3 9 20))

View File

@ -0,0 +1,22 @@
#lang typed/syndicate/roles
(require rackunit/turnstile)
(check-type (set 1 2 3)
: (Set Int)
-> (set 2 3 1))
(check-type (set 1 "hello" 3)
: (Set (U Int String))
-> (set "hello" 3 1))
(check-type (set-count (set 1 "hello" 3))
: Int
-> 3)
(check-type (set-union (set 1 2 3) (set "hello" "world"))
: (Set (U Int String))
-> (set 1 2 3 "hello" "world"))
(check-type (set-intersect (set 1 2 3) (set "hello" "world"))
: (Set )
-> (set))
(check-type (set-intersect (set 1 "hello" 3) (set #t "world" #f "hello"))
: (Set String)
-> (set "hello"))

View File

@ -0,0 +1,35 @@
#lang typed/syndicate/roles
(require rackunit/turnstile)
(check-type
(spawn (U (Tuple Int) (Observe (Tuple ★/t)))
(start-facet _
(on (asserted (tuple $x))
(add1 x))))
;; wanted: ν-s ((Actor (Tuple Int)))
: ★/t)
(typecheck-fail
(spawn (U (Tuple String) (Observe (Tuple ★/t)))
(start-facet _
(on (asserted (tuple $x:Int))
(add1 x))))
#:with-msg "spawn: Not prepared to handle inputs:\n\\(Tuple- String\\)")
(check-type
(spawn (U)
(start-facet _
(know (tuple 5))
(on (know (tuple $x:Int))
(add1 x))))
;; wanted: ν-s ((Actor (U)))
: ★/t)
(typecheck-fail
(spawn (U)
(start-facet _
(know (tuple "hi"))
(on (know (tuple $x:Int))
(add1 x))))
#:with-msg "spawn: Not prepared to handle internal events:\n\\(Tuple- String\\)")