Compare commits
146 Commits
Author | SHA1 | Date |
---|---|---|
Stephen Chang | a6719eb124 | |
Sam Caldwell | 39c54e77f3 | |
Sam Caldwell | 555c41a153 | |
Sam Caldwell | 33ef42818d | |
Sam Caldwell | 8afed87e99 | |
Sam Caldwell | f5331eb24f | |
Sam Caldwell | 80ebab5ed7 | |
Sam Caldwell | d29afb6679 | |
Sam Caldwell | 123037ba51 | |
Sam Caldwell | 5e61e9941b | |
Sam Caldwell | 7374c8c506 | |
Sam Caldwell | 2610ceb541 | |
Sam Caldwell | a8e890ab30 | |
Sam Caldwell | 96daa7518a | |
Sam Caldwell | eb56a1006f | |
Sam Caldwell | 142206d8e3 | |
Sam Caldwell | 479ea2fc1f | |
Sam Caldwell | 42d025cc7f | |
Sam Caldwell | 33b516b7a6 | |
Sam Caldwell | 2fa30c6066 | |
Sam Caldwell | 5ef44987ca | |
Sam Caldwell | 04e34c58ea | |
Sam Caldwell | 29f589d7c4 | |
Sam Caldwell | 443e1f9ac1 | |
Sam Caldwell | 4e2ae45b0b | |
Sam Caldwell | 8949193977 | |
Sam Caldwell | 0e44970bef | |
Sam Caldwell | ded2629296 | |
Sam Caldwell | a259153470 | |
Sam Caldwell | cdca416d21 | |
Sam Caldwell | de1fab2cb5 | |
Sam Caldwell | 064a2e1462 | |
Sam Caldwell | 3c65281a2e | |
Sam Caldwell | 997a3099fd | |
Sam Caldwell | e018359204 | |
Sam Caldwell | 9a21a811a3 | |
Sam Caldwell | 3c3291ffa4 | |
Sam Caldwell | b17cba59ed | |
Sam Caldwell | 16175c7bb4 | |
Sam Caldwell | 27abf8ab1e | |
Sam Caldwell | e6524174e1 | |
Sam Caldwell | 135e6b655b | |
Sam Caldwell | 202bcd6842 | |
Sam Caldwell | fa8822e40d | |
Sam Caldwell | c40b773282 | |
Sam Caldwell | be5bc19fcc | |
Sam Caldwell | 537b3fd272 | |
Sam Caldwell | 8f8f4c416f | |
Sam Caldwell | 5f38b6cc94 | |
Sam Caldwell | f597fdc499 | |
Sam Caldwell | 963676c0c6 | |
Sam Caldwell | 7462af708b | |
Sam Caldwell | e6b733325c | |
Sam Caldwell | affa47a2a5 | |
Sam Caldwell | 458bf93fef | |
Sam Caldwell | c38bfdc2c0 | |
Sam Caldwell | ee726c9177 | |
Sam Caldwell | 5dee1981b6 | |
Sam Caldwell | da900a258a | |
Sam Caldwell | 32f117df16 | |
Sam Caldwell | dcc4e3c411 | |
Sam Caldwell | 703a4c9589 | |
Sam Caldwell | 3ebcf413c9 | |
Sam Caldwell | 47ca363b18 | |
Sam Caldwell | 0711cd3232 | |
Sam Caldwell | 6b272ad3d3 | |
Sam Caldwell | d93dc085fe | |
Sam Caldwell | 3e1d4d108f | |
Sam Caldwell | 3ad0457bd5 | |
Sam Caldwell | ce0c296b5c | |
Sam Caldwell | 60ed8c2677 | |
Sam Caldwell | eba7ed072c | |
Sam Caldwell | c811b9a45f | |
Sam Caldwell | 3faaa1c580 | |
Sam Caldwell | 23bee726b1 | |
Sam Caldwell | 3aedb63a9c | |
Sam Caldwell | 807e6bb8f7 | |
Sam Caldwell | 98a779bdc1 | |
Sam Caldwell | c37c060dc9 | |
Sam Caldwell | c78b76b38c | |
Sam Caldwell | 22a228ab4b | |
Sam Caldwell | 296a77d714 | |
Sam Caldwell | 4fdce7fc0c | |
Sam Caldwell | 13e988fe58 | |
Sam Caldwell | 24efe43a6f | |
Sam Caldwell | 99d5916bd1 | |
Sam Caldwell | 20693f234e | |
Sam Caldwell | deca0a82be | |
Sam Caldwell | 96e9431e15 | |
Sam Caldwell | 8cf13a9bbf | |
Sam Caldwell | c283dae7e4 | |
Sam Caldwell | 559e9bb11b | |
Sam Caldwell | df9f3ebbd2 | |
Sam Caldwell | c8a1253d7b | |
Sam Caldwell | fc220a4e16 | |
Sam Caldwell | a84b80a49b | |
Sam Caldwell | ed695c66d6 | |
Sam Caldwell | 4420f6cd74 | |
Sam Caldwell | d9e651a668 | |
Sam Caldwell | 66a3ece353 | |
Sam Caldwell | db41cb63d7 | |
Sam Caldwell | 349fa19d26 | |
Sam Caldwell | 5238b74912 | |
Sam Caldwell | 3def83502a | |
Sam Caldwell | 5fda25a42e | |
Sam Caldwell | 9dd11ef7db | |
Sam Caldwell | 8f92368d8f | |
Sam Caldwell | dc0e434caa | |
Sam Caldwell | fd40ab2e52 | |
Sam Caldwell | 5310956848 | |
Sam Caldwell | 1590687e7a | |
Sam Caldwell | 68f14919d7 | |
Sam Caldwell | 309d6867d9 | |
Sam Caldwell | 8819af878e | |
Sam Caldwell | 3b35000a5e | |
Sam Caldwell | 69660e02dd | |
Sam Caldwell | 4b692428af | |
Sam Caldwell | 2c0bef7da4 | |
Sam Caldwell | 75539d0ec3 | |
Sam Caldwell | 47d2568a93 | |
Sam Caldwell | 1bdb9b7820 | |
Sam Caldwell | 97b3a9a0b5 | |
Sam Caldwell | 63089efdbc | |
Sam Caldwell | 1b2527920e | |
Sam Caldwell | 899d8c460d | |
Sam Caldwell | af56bc283d | |
Sam Caldwell | 33522647fd | |
Sam Caldwell | c9563cd0a2 | |
Sam Caldwell | 80ef12ef4d | |
Sam Caldwell | 1c9f53590d | |
Sam Caldwell | c9a44ab45e | |
Sam Caldwell | e3c7926b92 | |
Sam Caldwell | 7815fad415 | |
Sam Caldwell | e16db164df | |
Sam Caldwell | 362d7c877d | |
Sam Caldwell | 19f915620e | |
Sam Caldwell | c726fb2bdd | |
Sam Caldwell | 47dc84f034 | |
Sam Caldwell | 0cc550ea43 | |
Sam Caldwell | 324557e8b5 | |
Sam Caldwell | 50448f41a7 | |
Sam Caldwell | 126046caa9 | |
Sam Caldwell | a8d398eec7 | |
Sam Caldwell | 170e2b28ce | |
Sam Caldwell | 480b67ea51 | |
Sam Caldwell | 64016053ff |
|
@ -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)))))
|
|
@ -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))
|
|
@ -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))))
|
|
@ -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))))
|
|
@ -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))))
|
|
@ -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))))
|
|
@ -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)))
|
|
@ -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)))
|
|
@ -0,0 +1,4 @@
|
||||||
|
#lang setup/infotab
|
||||||
|
|
||||||
|
(define compile-omit-paths
|
||||||
|
'("examples"))
|
|
@ -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)
|
|
@ -31,6 +31,9 @@
|
||||||
retracted
|
retracted
|
||||||
rising-edge
|
rising-edge
|
||||||
(rename-out [core:message message])
|
(rename-out [core:message message])
|
||||||
|
know
|
||||||
|
forget
|
||||||
|
realize
|
||||||
|
|
||||||
let-event
|
let-event
|
||||||
|
|
||||||
|
@ -58,6 +61,7 @@
|
||||||
perform-actions!
|
perform-actions!
|
||||||
flush!
|
flush!
|
||||||
quit-dataspace!
|
quit-dataspace!
|
||||||
|
realize!
|
||||||
|
|
||||||
syndicate-effects-available?
|
syndicate-effects-available?
|
||||||
|
|
||||||
|
@ -80,6 +84,7 @@
|
||||||
(require racket/set)
|
(require racket/set)
|
||||||
(require racket/match)
|
(require racket/match)
|
||||||
(require racket/contract)
|
(require racket/contract)
|
||||||
|
(require (only-in racket/list flatten))
|
||||||
|
|
||||||
(require (for-syntax racket/base))
|
(require (for-syntax racket/base))
|
||||||
(require (for-syntax syntax/parse))
|
(require (for-syntax syntax/parse))
|
||||||
|
@ -198,10 +203,15 @@
|
||||||
endpoints ;; (Hash EID Endpoint)
|
endpoints ;; (Hash EID Endpoint)
|
||||||
stop-scripts ;; (Listof Script) -- IN REVERSE ORDER
|
stop-scripts ;; (Listof Script) -- IN REVERSE ORDER
|
||||||
children ;; (Setof FID)
|
children ;; (Setof FID)
|
||||||
|
previous-knowledge ;; AssertionSet of internal knowledge
|
||||||
|
knowledge ;; AssertionSet of internal knowledge
|
||||||
) #:prefab)
|
) #:prefab)
|
||||||
|
|
||||||
(struct endpoint (id patch-fn handler-fn) #: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
|
;; Script priorities. These are used to ensure that the results of
|
||||||
;; some *side effects* are visible to certain pieces of code.
|
;; some *side effects* are visible to certain pieces of code.
|
||||||
|
@ -249,6 +259,12 @@
|
||||||
;; Storeof (Constreeof Action)
|
;; Storeof (Constreeof Action)
|
||||||
(define current-pending-actions (make-store))
|
(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) ...)
|
;; Storeof (Vector (Queue Script) ...)
|
||||||
;; Mutates the vector!
|
;; Mutates the vector!
|
||||||
(define current-pending-scripts (make-store))
|
(define current-pending-scripts (make-store))
|
||||||
|
@ -407,6 +423,7 @@
|
||||||
(analyze-pattern stx #'P))
|
(analyze-pattern stx #'P))
|
||||||
(quasisyntax/loc stx
|
(quasisyntax/loc stx
|
||||||
(add-endpoint! #,(source-location->string stx)
|
(add-endpoint! #,(source-location->string stx)
|
||||||
|
#f
|
||||||
(lambda ()
|
(lambda ()
|
||||||
#,(let ((patch-stx #`(core:assert #,pat)))
|
#,(let ((patch-stx #`(core:assert #,pat)))
|
||||||
(if #'w.Pred
|
(if #'w.Pred
|
||||||
|
@ -414,6 +431,22 @@
|
||||||
patch-stx)))
|
patch-stx)))
|
||||||
void))]))
|
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)
|
(define (fid-ancestor? fid maybe-ancestor)
|
||||||
(and (pair? fid) ;; empty fid lists obviously no ancestors at all!
|
(and (pair? fid) ;; empty fid lists obviously no ancestors at all!
|
||||||
(or (equal? fid maybe-ancestor)
|
(or (equal? fid maybe-ancestor)
|
||||||
|
@ -474,6 +507,7 @@
|
||||||
|
|
||||||
(define (on-event* where proc #:priority [priority *normal-priority*])
|
(define (on-event* where proc #:priority [priority *normal-priority*])
|
||||||
(add-endpoint! where
|
(add-endpoint! where
|
||||||
|
#f
|
||||||
(lambda () patch-empty)
|
(lambda () patch-empty)
|
||||||
(lambda (e _current-interests _synthetic?)
|
(lambda (e _current-interests _synthetic?)
|
||||||
(schedule-script! #:priority priority (lambda () (proc e))))))
|
(schedule-script! #:priority priority (lambda () (proc e))))))
|
||||||
|
@ -489,14 +523,18 @@
|
||||||
|
|
||||||
(define-syntax (during stx)
|
(define-syntax (during stx)
|
||||||
(syntax-parse stx
|
(syntax-parse stx
|
||||||
[(_ P O ...)
|
#:literals (know)
|
||||||
(define E-stx (syntax/loc #'P (asserted P)))
|
[(_ (~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)
|
(define-values (_proj _pat _bindings instantiated)
|
||||||
(analyze-pattern E-stx #'P))
|
(analyze-pattern E-stx #'P))
|
||||||
(quasisyntax/loc stx
|
(quasisyntax/loc stx
|
||||||
(on #,E-stx
|
(on #,E-stx
|
||||||
(let ((p #,instantiated))
|
(let ((p #,instantiated))
|
||||||
(react (stop-when (retracted p))
|
(react (stop-when (#,R-stx p))
|
||||||
O ...))))]))
|
O ...))))]))
|
||||||
|
|
||||||
(define-syntax (during/spawn stx)
|
(define-syntax (during/spawn stx)
|
||||||
|
@ -547,6 +585,7 @@
|
||||||
(quasisyntax/loc stx
|
(quasisyntax/loc stx
|
||||||
(let ()
|
(let ()
|
||||||
(add-endpoint! #,(source-location->string stx)
|
(add-endpoint! #,(source-location->string stx)
|
||||||
|
#f
|
||||||
(lambda ()
|
(lambda ()
|
||||||
(define subject-id (current-dataflow-subject-id))
|
(define subject-id (current-dataflow-subject-id))
|
||||||
(schedule-script!
|
(schedule-script!
|
||||||
|
@ -570,6 +609,8 @@
|
||||||
(define-syntax (asserted stx) (raise-syntax-error #f "asserted: Used outside event spec" stx))
|
(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 (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 (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)
|
(define-syntax (suspend-script stx)
|
||||||
(syntax-parse stx
|
(syntax-parse stx
|
||||||
|
@ -772,37 +813,59 @@
|
||||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
;; Syntax-time support
|
;; 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 (or* x y) (or x y))
|
||||||
(define a (current-actor-state))
|
(define-values (prev current) (retrieve-knowledge synthetic?))
|
||||||
(define previous-knowledge (if synthetic? trie-empty (actor-state-previous-knowledge a)))
|
(define old (trie-lookup prev pat #f #:wildcard-union or*))
|
||||||
(define old (trie-lookup previous-knowledge pat #f #:wildcard-union or*))
|
(define new (trie-lookup current pat #f #:wildcard-union or*))
|
||||||
(define new (trie-lookup (actor-state-knowledge a) pat #f #:wildcard-union or*))
|
|
||||||
(values old new))
|
(values old new))
|
||||||
|
|
||||||
(define (interest-just-appeared-matching? pat synthetic?)
|
(define (interest-just-appeared-matching? pat synthetic? retrieve-knowledge)
|
||||||
(define-values (old new) (interests-pre-and-post-patch pat synthetic?))
|
(define-values (old new) (interests-pre-and-post-patch pat synthetic? retrieve-knowledge))
|
||||||
(and (not old) new))
|
(and (not old) new))
|
||||||
|
|
||||||
(define (interest-just-disappeared-matching? pat synthetic?)
|
(define (interest-just-disappeared-matching? pat synthetic? retrieve-knowledge)
|
||||||
(define-values (old new) (interests-pre-and-post-patch pat synthetic?))
|
(define-values (old new) (interests-pre-and-post-patch pat synthetic? retrieve-knowledge))
|
||||||
(and old (not new)))
|
(and old (not new)))
|
||||||
|
|
||||||
(define-for-syntax (analyze-asserted/retracted outer-expr-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
|
when-pred-stx
|
||||||
event-stx
|
event-stx
|
||||||
script-stx
|
script-stx
|
||||||
asserted?
|
asserted?
|
||||||
P-stx
|
P-stx
|
||||||
priority-stx)
|
priority-stx
|
||||||
|
internal?)
|
||||||
|
(define P+
|
||||||
|
(if internal? #`(internal-knowledge #,P-stx) P-stx))
|
||||||
(define-values (proj-stx pat bindings _instantiated)
|
(define-values (proj-stx pat bindings _instantiated)
|
||||||
(analyze-pattern event-stx P-stx))
|
(analyze-pattern event-stx P+))
|
||||||
(define event-predicate-stx (if asserted? #'patch/added? #'patch/removed?))
|
(define event-predicate-stx (if asserted? #'patch/added? #'patch/removed?))
|
||||||
(define patch-accessor-stx (if asserted? #'patch-added #'patch-removed))
|
(define patch-accessor-stx (if asserted? #'patch-added #'patch-removed))
|
||||||
(define change-detector-stx
|
(define change-detector-stx
|
||||||
(if asserted? #'interest-just-appeared-matching? #'interest-just-disappeared-matching?))
|
(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
|
(quasisyntax/loc outer-expr-stx
|
||||||
(add-endpoint! #,(source-location->string outer-expr-stx)
|
(add-endpoint!
|
||||||
|
#,(source-location->string outer-expr-stx)
|
||||||
|
#,internal?
|
||||||
(lambda () (if #,when-pred-stx
|
(lambda () (if #,when-pred-stx
|
||||||
(core:sub #,pat)
|
(core:sub #,pat)
|
||||||
patch-empty))
|
patch-empty))
|
||||||
|
@ -822,13 +885,48 @@
|
||||||
#,(source-location->string P-stx)))
|
#,(source-location->string P-stx)))
|
||||||
(for [(entry (in-set entry-set))]
|
(for [(entry (in-set entry-set))]
|
||||||
(let ((instantiated (instantiate-projection proj entry)))
|
(let ((instantiated (instantiate-projection proj entry)))
|
||||||
(and (#,change-detector-stx instantiated synthetic?)
|
(and (#,change-detector-stx instantiated synthetic? #,knowledge-retriever)
|
||||||
(schedule-script!
|
(schedule-script!
|
||||||
#:priority #,priority-stx
|
#:priority #,priority-stx
|
||||||
(lambda ()
|
(lambda ()
|
||||||
(match-define (list #,@bindings) entry)
|
(match-define (list #,@bindings) entry)
|
||||||
#,script-stx)))))]))))))
|
#,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
|
(define-for-syntax orig-insp
|
||||||
(variable-reference->module-declaration-inspector (#%variable-reference)))
|
(variable-reference->module-declaration-inspector (#%variable-reference)))
|
||||||
|
|
||||||
|
@ -839,7 +937,7 @@
|
||||||
priority-stx)
|
priority-stx)
|
||||||
(define event-stx (syntax-disarm armed-event-stx orig-insp))
|
(define event-stx (syntax-disarm armed-event-stx orig-insp))
|
||||||
(syntax-parse event-stx
|
(syntax-parse event-stx
|
||||||
#:literals [core:message asserted retracted rising-edge]
|
#:literals [core:message asserted retracted rising-edge know forget realize]
|
||||||
[(expander args ...)
|
[(expander args ...)
|
||||||
#:when (event-expander-id? #'expander)
|
#:when (event-expander-id? #'expander)
|
||||||
(event-expander-transform
|
(event-expander-transform
|
||||||
|
@ -851,33 +949,23 @@
|
||||||
script-stx
|
script-stx
|
||||||
priority-stx)))]
|
priority-stx)))]
|
||||||
[(core:message P)
|
[(core:message P)
|
||||||
(define-values (proj pat bindings _instantiated)
|
(analyze-message outer-expr-stx when-pred-stx event-stx script-stx
|
||||||
(analyze-pattern event-stx #'P))
|
#'P priority-stx #f)]
|
||||||
(quasisyntax/loc outer-expr-stx
|
|
||||||
(add-endpoint! #,(source-location->string outer-expr-stx)
|
|
||||||
(lambda () (if #,when-pred-stx
|
|
||||||
(core:sub #,pat)
|
|
||||||
patch-empty))
|
|
||||||
(lambda (e current-interests _synthetic?)
|
|
||||||
(when (not (trie-empty? current-interests))
|
|
||||||
(core:match-event e
|
|
||||||
[(core:message body)
|
|
||||||
(define capture-vals
|
|
||||||
(match-value/captures
|
|
||||||
body
|
|
||||||
#,proj))
|
|
||||||
(and capture-vals
|
|
||||||
(schedule-script!
|
|
||||||
#:priority #,priority-stx
|
|
||||||
(lambda ()
|
|
||||||
(apply (lambda #,bindings #,script-stx)
|
|
||||||
capture-vals))))])))))]
|
|
||||||
[(asserted P)
|
[(asserted P)
|
||||||
(analyze-asserted/retracted outer-expr-stx when-pred-stx event-stx script-stx
|
(analyze-appear/disappear outer-expr-stx when-pred-stx event-stx script-stx
|
||||||
#t #'P priority-stx)]
|
#t #'P priority-stx #f)]
|
||||||
[(retracted P)
|
[(retracted P)
|
||||||
(analyze-asserted/retracted outer-expr-stx when-pred-stx event-stx script-stx
|
(analyze-appear/disappear outer-expr-stx when-pred-stx event-stx script-stx
|
||||||
#f #'P priority-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)
|
[(rising-edge Pred)
|
||||||
(define field-name
|
(define field-name
|
||||||
(datum->syntax event-stx
|
(datum->syntax event-stx
|
||||||
|
@ -887,6 +975,7 @@
|
||||||
(let ()
|
(let ()
|
||||||
(field [#,field-name #f])
|
(field [#,field-name #f])
|
||||||
(add-endpoint! #,(source-location->string outer-expr-stx)
|
(add-endpoint! #,(source-location->string outer-expr-stx)
|
||||||
|
#f
|
||||||
(lambda ()
|
(lambda ()
|
||||||
(when #,when-pred-stx
|
(when #,when-pred-stx
|
||||||
(define old-val (#,field-name))
|
(define old-val (#,field-name))
|
||||||
|
@ -1003,10 +1092,25 @@
|
||||||
(current-pending-actions (list (current-pending-actions)
|
(current-pending-actions (list (current-pending-actions)
|
||||||
((current-action-transformer) p)))))
|
((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
|
;; Endpoint Creation
|
||||||
|
|
||||||
(define (add-endpoint! where patch-fn handler-fn)
|
(define (add-endpoint! where internal? patch-fn handler-fn)
|
||||||
(when (in-script?)
|
(when (in-script?)
|
||||||
(error 'add-endpoint!
|
(error 'add-endpoint!
|
||||||
"~a: Cannot add endpoint in script; are you missing a (react ...)?"
|
"~a: Cannot add endpoint in script; are you missing a (react ...)?"
|
||||||
|
@ -1030,7 +1134,9 @@
|
||||||
(hash-set (facet-endpoints f)
|
(hash-set (facet-endpoints f)
|
||||||
new-eid
|
new-eid
|
||||||
(endpoint new-eid patch-fn handler-fn))]))))
|
(endpoint new-eid patch-fn handler-fn))]))))
|
||||||
(schedule-action! delta-aggregate))
|
(if internal?
|
||||||
|
(schedule-internal-event! delta-aggregate)
|
||||||
|
(schedule-action! delta-aggregate)))
|
||||||
|
|
||||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
;; Facet Lifecycle
|
;; Facet Lifecycle
|
||||||
|
@ -1045,7 +1151,7 @@
|
||||||
(define fid-uid next-fid-uid)
|
(define fid-uid next-fid-uid)
|
||||||
(define fid (cons fid-uid parent-fid))
|
(define fid (cons fid-uid parent-fid))
|
||||||
(set! next-fid-uid (+ next-fid-uid 1))
|
(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
|
(update-facet! parent-fid
|
||||||
(lambda (pf)
|
(lambda (pf)
|
||||||
(and pf (struct-copy facet pf
|
(and pf (struct-copy facet pf
|
||||||
|
@ -1094,8 +1200,24 @@
|
||||||
(dataflow-forget-subject! (actor-state-field-dataflow a) (list fid eid))
|
(dataflow-forget-subject! (actor-state-field-dataflow a) (list fid eid))
|
||||||
(define-values (new-mux _eid _delta delta-aggregate)
|
(define-values (new-mux _eid _delta delta-aggregate)
|
||||||
(mux-remove-stream (actor-state-mux a) eid))
|
(mux-remove-stream (actor-state-mux a) eid))
|
||||||
(current-actor-state (struct-copy actor-state a [mux new-mux]))
|
(define internal (patch-step delta-aggregate internal-knowledge-parenthesis))
|
||||||
(schedule-action! delta-aggregate))))
|
(define external (patch (trie-subtract (patch-added delta-aggregate) (patch-added internal))
|
||||||
|
(trie-subtract (patch-removed delta-aggregate) (patch-removed internal))))
|
||||||
|
(current-actor-state (struct-copy actor-state a
|
||||||
|
[mux new-mux]))
|
||||||
|
(define internal-aggregate (patch-prepend internal-knowledge-parenthesis internal))
|
||||||
|
(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-aggregate)
|
||||||
|
(schedule-action! external))))
|
||||||
|
|
||||||
(schedule-script!
|
(schedule-script!
|
||||||
#:priority *gc-priority*
|
#:priority *gc-priority*
|
||||||
|
@ -1124,6 +1246,8 @@
|
||||||
(make-dataflow-graph)))
|
(make-dataflow-graph)))
|
||||||
(current-pending-patch patch-empty)
|
(current-pending-patch patch-empty)
|
||||||
(current-pending-actions '())
|
(current-pending-actions '())
|
||||||
|
(current-pending-internal-patch patch-empty)
|
||||||
|
(current-pending-internal-events '())
|
||||||
(current-pending-scripts (make-empty-pending-scripts))
|
(current-pending-scripts (make-empty-pending-scripts))
|
||||||
(current-action-transformer values)]
|
(current-action-transformer values)]
|
||||||
(with-current-facet '() #f
|
(with-current-facet '() #f
|
||||||
|
@ -1151,6 +1275,7 @@
|
||||||
(when script
|
(when script
|
||||||
(script)
|
(script)
|
||||||
(refresh-facet-assertions!)
|
(refresh-facet-assertions!)
|
||||||
|
(dispatch-internal-events!)
|
||||||
(run-all-pending-scripts!)))
|
(run-all-pending-scripts!)))
|
||||||
|
|
||||||
(define (run-scripts!)
|
(define (run-scripts!)
|
||||||
|
@ -1162,6 +1287,20 @@
|
||||||
(core:quit pending-actions)
|
(core:quit pending-actions)
|
||||||
(core:transition (current-actor-state) 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!)
|
(define (refresh-facet-assertions!)
|
||||||
(dataflow-repair-damage! (actor-state-field-dataflow (current-actor-state))
|
(dataflow-repair-damage! (actor-state-field-dataflow (current-actor-state))
|
||||||
(lambda (subject-id)
|
(lambda (subject-id)
|
||||||
|
@ -1197,10 +1336,12 @@
|
||||||
(if (patch? e)
|
(if (patch? e)
|
||||||
(struct-copy actor-state a
|
(struct-copy actor-state a
|
||||||
[previous-knowledge (actor-state-knowledge a)]
|
[previous-knowledge (actor-state-knowledge a)]
|
||||||
[knowledge (update-interests (actor-state-knowledge a) e)])
|
[knowledge (apply-patch (actor-state-knowledge a) e)])
|
||||||
a))
|
a))
|
||||||
(current-pending-patch patch-empty)
|
(current-pending-patch patch-empty)
|
||||||
(current-pending-actions '())
|
(current-pending-actions '())
|
||||||
|
(current-pending-internal-patch patch-empty)
|
||||||
|
(current-pending-internal-events '())
|
||||||
(current-pending-scripts (make-empty-pending-scripts))
|
(current-pending-scripts (make-empty-pending-scripts))
|
||||||
(current-action-transformer values)]
|
(current-action-transformer values)]
|
||||||
(for [((fid f) (in-hash (actor-state-facets a)))]
|
(for [((fid f) (in-hash (actor-state-facets a)))]
|
||||||
|
@ -1210,6 +1351,16 @@
|
||||||
(define (facet-handle-event! fid f e synthetic?)
|
(define (facet-handle-event! fid f e synthetic?)
|
||||||
(define mux (actor-state-mux (current-actor-state)))
|
(define mux (actor-state-mux (current-actor-state)))
|
||||||
(with-current-facet fid #f
|
(with-current-facet fid #f
|
||||||
|
(when (patch? e)
|
||||||
|
;; quick-and-dirty intersection with (internal-knowledge ?)
|
||||||
|
(define internal (patch-prepend internal-knowledge-parenthesis
|
||||||
|
(patch-step e internal-knowledge-parenthesis)))
|
||||||
|
(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)))]
|
(for [(ep (in-hash-values (facet-endpoints f)))]
|
||||||
((endpoint-handler-fn ep) e (mux-interests-of mux (endpoint-id ep)) synthetic?))))
|
((endpoint-handler-fn ep) e (mux-interests-of mux (endpoint-id ep)) synthetic?))))
|
||||||
|
|
||||||
|
@ -1306,6 +1457,10 @@
|
||||||
(ensure-in-script! 'send!)
|
(ensure-in-script! 'send!)
|
||||||
(schedule-action! (core:message M)))
|
(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 *adhoc-label* -1)
|
||||||
|
|
||||||
(define (assert! P)
|
(define (assert! P)
|
||||||
|
@ -1352,7 +1507,7 @@
|
||||||
(fprintf p " - Knowledge:\n ~a" (trie->pretty-string knowledge #:indent 3))
|
(fprintf p " - Knowledge:\n ~a" (trie->pretty-string knowledge #:indent 3))
|
||||||
(fprintf p " - Facets:\n")
|
(fprintf p " - Facets:\n")
|
||||||
(for ([(fid f) (in-hash facets)])
|
(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))
|
(fprintf p " ---- facet ~a, children=~a" fid (set->list children))
|
||||||
(when (not (hash-empty? endpoints))
|
(when (not (hash-empty? endpoints))
|
||||||
(fprintf p ", endpoints=~a" (hash-keys endpoints)))
|
(fprintf p ", endpoints=~a" (hash-keys endpoints)))
|
||||||
|
|
|
@ -2,6 +2,7 @@
|
||||||
|
|
||||||
(require (for-syntax racket/base syntax/kerncase))
|
(require (for-syntax racket/base syntax/kerncase))
|
||||||
(require (for-syntax syntax/parse))
|
(require (for-syntax syntax/parse))
|
||||||
|
(require (for-syntax (only-in racket/list make-list)))
|
||||||
|
|
||||||
(require racket/match)
|
(require racket/match)
|
||||||
(require "main.rkt")
|
(require "main.rkt")
|
||||||
|
@ -52,20 +53,11 @@
|
||||||
(module+ main (current-ground-dataspace run-ground))
|
(module+ main (current-ground-dataspace run-ground))
|
||||||
forms ...)))]))
|
forms ...)))]))
|
||||||
|
|
||||||
(define-syntax (syndicate-module stx)
|
;; Identifier -> Bool
|
||||||
(syntax-parse stx
|
;; Is the identifier a form that shouldn't capture actor actions?
|
||||||
[(_ (action-ids ...) (form forms ...))
|
;; note the absence of define-values
|
||||||
(define expanded (local-expand #'form
|
(define-for-syntax (kernel-id? x)
|
||||||
'module
|
(ormap (lambda (i) (free-identifier=? x i))
|
||||||
(append (list #'module+
|
|
||||||
#'begin-for-declarations)
|
|
||||||
(kernel-form-identifier-list))))
|
|
||||||
(syntax-parse expanded
|
|
||||||
#:literals (begin)
|
|
||||||
[(begin more-forms ...)
|
|
||||||
#'(syndicate-module (action-ids ...) (more-forms ... forms ...))]
|
|
||||||
[(head rest ...)
|
|
||||||
(if (ormap (lambda (i) (free-identifier=? #'head i))
|
|
||||||
(syntax->list #'(require
|
(syntax->list #'(require
|
||||||
provide
|
provide
|
||||||
define-values
|
define-values
|
||||||
|
@ -77,11 +69,38 @@
|
||||||
#%require
|
#%require
|
||||||
#%provide
|
#%provide
|
||||||
#%declare
|
#%declare
|
||||||
begin-for-declarations)))
|
begin-for-declarations))))
|
||||||
#`(begin #,expanded (syndicate-module (action-ids ...) (forms ...)))
|
|
||||||
|
(define-syntax (syndicate-module stx)
|
||||||
|
(syntax-parse stx
|
||||||
|
[(_ (action-ids ...) (form forms ...))
|
||||||
|
(define expanded (local-expand #'form
|
||||||
|
'module
|
||||||
|
(append (list #'module+
|
||||||
|
#'begin-for-declarations)
|
||||||
|
(kernel-form-identifier-list))))
|
||||||
|
(syntax-parse expanded
|
||||||
|
#: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 ...)
|
||||||
|
(cond
|
||||||
|
[(kernel-id? #'head)
|
||||||
|
#`(begin #,expanded (syndicate-module (action-ids ...) (forms ...)))]
|
||||||
|
[else
|
||||||
(with-syntax ([action-id (car (generate-temporaries (list #'form)))])
|
(with-syntax ([action-id (car (generate-temporaries (list #'form)))])
|
||||||
#`(begin (define action-id (capture-actor-actions (lambda () #,expanded)))
|
#`(begin (define action-id (capture-actor-actions (lambda () #,expanded)))
|
||||||
(syndicate-module (action-ids ... action-id) (forms ...)))))]
|
(syndicate-module (action-ids ... action-id) (forms ...))))])]
|
||||||
[non-pair-syntax
|
[non-pair-syntax
|
||||||
#'(begin form (syndicate-module (action-ids ...) (forms ...)))])]
|
#'(begin form (syndicate-module (action-ids ...) (forms ...)))])]
|
||||||
[(_ (action-ids ...) ())
|
[(_ (action-ids ...) ())
|
||||||
|
|
|
@ -1,12 +1,8 @@
|
||||||
#lang syndicate
|
#lang syndicate
|
||||||
|
|
||||||
(require (only-in racket/set
|
(require racket/set)
|
||||||
set
|
|
||||||
set-count
|
|
||||||
set-empty?
|
|
||||||
set-first
|
|
||||||
set-remove))
|
|
||||||
(require (only-in racket/list
|
(require (only-in racket/list
|
||||||
|
first
|
||||||
partition
|
partition
|
||||||
empty?
|
empty?
|
||||||
split-at))
|
split-at))
|
||||||
|
@ -17,6 +13,7 @@
|
||||||
string-trim))
|
string-trim))
|
||||||
(require (only-in racket/sequence
|
(require (only-in racket/sequence
|
||||||
sequence->list))
|
sequence->list))
|
||||||
|
(require (only-in racket/function const))
|
||||||
|
|
||||||
(module+ test
|
(module+ test
|
||||||
(require rackunit))
|
(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),
|
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
|
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
|
should only assign a task to a TM if the TM actually has the resources to
|
||||||
perform a task.
|
perform a task.
|
||||||
|#
|
|#
|
||||||
(assertion-struct task-manager (id slots))
|
(assertion-struct task-manager (id slots))
|
||||||
;; an ID is a symbol or a natural number.
|
;; an ID is a symbol or a natural number.
|
||||||
;; Any -> Bool
|
;; Any -> Bool
|
||||||
;; recognize ids
|
;; recognize IDs
|
||||||
(define (id? x)
|
(define (id? x)
|
||||||
(or (symbol? x) (exact-nonnegative-integer? x)))
|
(or (symbol? x) (exact-nonnegative-integer? x)))
|
||||||
#|
|
#|
|
||||||
The resources available to a TM are its associated TaskRunners (TRs). TaskRunners
|
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
|
assert their presence with (task-runner ID)
|
||||||
- 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
|
(assertion-struct task-runner (id))
|
||||||
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
|
a Status is one of
|
||||||
should only receive tasks when it is IDLE.
|
- 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 IDLE 'idle)
|
||||||
(define OVERLOAD 'overload)
|
(define OVERLOAD 'overload)
|
||||||
(struct executing (id) #:transparent)
|
(struct executing (id) #:transparent)
|
||||||
|
@ -69,19 +70,22 @@ Task Delegation Protocol
|
||||||
|
|
||||||
Task Delegation has two roles, TaskAssigner (TA) and TaskPerformer (TP).
|
Task Delegation has two roles, TaskAssigner (TA) and TaskPerformer (TP).
|
||||||
|
|
||||||
A TaskAssigner asserts the association of a Task with a particular TaskPerformer
|
A TaskAssigner requests the performance of a Task with a particular TaskPerformer
|
||||||
through
|
through the assertion of interest
|
||||||
(task-assignment ID ID Task)
|
(observe (task-performance ID Task ★))
|
||||||
where the first ID identifies the TP and the second identifies the job.
|
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)
|
- (map-work String)
|
||||||
- (reduce-work (U ID TaskResult) (U ID TaskResult)), referring to either the
|
- (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
|
ID of the dependent task or its results. A reduce-work is ready to be executed
|
||||||
when it has both results.
|
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
|
A TaskResult is a (Hashof String Natural), counting the occurrences of words
|
||||||
|#
|
|#
|
||||||
(struct task (id desc) #:transparent)
|
(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)
|
(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,
|
to that task,
|
||||||
(task-state ID ID ID TaskStateDesc)
|
(task-performance ID Task TaskStateDesc)
|
||||||
where the first ID is that of the TP, the second is that of the job,
|
|
||||||
and the third that of the task.
|
|
||||||
|
|
||||||
A TaskStateDesc is one of
|
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)
|
- 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
|
- RUNNING, indicating that the task is being performed
|
||||||
- (finished TaskResult), describing the results
|
- (finished TaskResult), describing the results
|
||||||
|#
|
|#
|
||||||
(assertion-struct task-state (assignee job-id task-id desc))
|
|
||||||
(struct finished (data) #:transparent)
|
(struct finished (data) #:transparent)
|
||||||
(define ACCEPTED 'accepted)
|
(define ACCEPTED 'accepted)
|
||||||
(define RUNNING 'running)
|
(define RUNNING 'running)
|
||||||
|
@ -115,11 +116,14 @@ TaskRunners.
|
||||||
Job Submission Protocol
|
Job Submission Protocol
|
||||||
-----------------------
|
-----------------------
|
||||||
|
|
||||||
Finally, Clients submit their jobs to the JobManager by asserting a Job, which is a (job ID (Listof Task)).
|
Finally, Clients submit their jobs to the JobManager by asserting interest
|
||||||
The JobManager then performs the job and, when finished, asserts (job-finished ID TaskResult)
|
(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))
|
(struct job (id tasks) #:transparent)
|
||||||
(assertion-struct job-finished (id data))
|
(assertion-struct job-completion (id data result))
|
||||||
|
|
||||||
;; ---------------------------------------------------------------------------------------------------
|
;; ---------------------------------------------------------------------------------------------------
|
||||||
;; Logging
|
;; Logging
|
||||||
|
@ -128,35 +132,64 @@ The JobManager then performs the job and, when finished, asserts (job-finished I
|
||||||
(displayln (apply format fmt args)))
|
(displayln (apply format fmt args)))
|
||||||
|
|
||||||
;; ---------------------------------------------------------------------------------------------------
|
;; ---------------------------------------------------------------------------------------------------
|
||||||
;; TaskRunner
|
;; Generic Implementation of Task Delegation Protocol
|
||||||
|
|
||||||
(define (spawn-task-runner)
|
;; a TaskFun is a
|
||||||
(define id (gensym 'task-runner))
|
;; (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
|
(spawn #:name id
|
||||||
(field [status IDLE])
|
(assert (task-runner id))
|
||||||
(define (idle?) (equal? IDLE (status)))
|
(stop-when (retracted (task-manager tm-id _)))
|
||||||
(assert (task-runner id (status)))
|
;; Task (TaskStateDesc -> Void) -> Void
|
||||||
(begin/dataflow
|
(define (perform-task tsk on-complete! update-status!)
|
||||||
(log "task-runner ~v state is: ~a" id (status)))
|
(match-define (task tid desc) tsk)
|
||||||
(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
|
(match desc
|
||||||
[(map-work data)
|
[(map-work data)
|
||||||
(word-count (count-new-words (word-count) (string->words data)))
|
(define wc (count-new-words (hash) (string->words data)))
|
||||||
(execution-state (finished (word-count)))]
|
(on-complete! wc)]
|
||||||
[(reduce-work left right)
|
[(reduce-work left right)
|
||||||
(word-count (hash-union left right #:combine +))
|
(define wc (hash-union left right #:combine +))
|
||||||
(execution-state (finished (word-count)))]))))))
|
(on-complete! wc)]))
|
||||||
|
(on-start
|
||||||
|
(task-performer id (const #t) perform-task))))
|
||||||
|
|
||||||
;; (Hash String Nat) String -> (Hash String Nat)
|
;; (Hash String Nat) String -> (Hash String Nat)
|
||||||
(define (word-count-increment h word)
|
(define (word-count-increment h word)
|
||||||
|
@ -185,61 +218,66 @@ The JobManager then performs the job and, when finished, asserts (job-finished I
|
||||||
(list "good" "eve" "ma'am"))
|
(list "good" "eve" "ma'am"))
|
||||||
(check-equal? (string->words "please sir. may I have another?")
|
(check-equal? (string->words "please sir. may I have another?")
|
||||||
(list "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")
|
#;(check-equal? (string->words "but wait---there's more")
|
||||||
(list "but" "wait" "there's" "more")))
|
(list "but" "wait" "there's" "more")))
|
||||||
|
|
||||||
;; ---------------------------------------------------------------------------------------------------
|
;; ---------------------------------------------------------------------------------------------------
|
||||||
;; TaskManager
|
;; TaskManager
|
||||||
|
|
||||||
(define (spawn-task-manager)
|
;; PosInt -> Spawn
|
||||||
|
(define (spawn-task-manager num-task-runners)
|
||||||
(define id (gensym 'task-manager))
|
(define id (gensym 'task-manager))
|
||||||
(spawn #:name id
|
(spawn #:name id
|
||||||
(log "Task Manager (TM) ~a is running" id)
|
(log "Task Manager (TM) ~a is running" id)
|
||||||
(during (job-manager-alive)
|
(during (job-manager-alive)
|
||||||
(log "TM learns about JM")
|
(log "TM ~a learns about JM" id)
|
||||||
(define/query-set task-runners (task-runner $id _) id
|
|
||||||
#:on-add (log "TM learns about task-runner ~a" id))
|
(field [task-runners (set)])
|
||||||
;; I wonder just how inefficient this is
|
|
||||||
(define/query-set idle-runners (task-runner $id IDLE) id
|
;; Create & Monitor Task Runners
|
||||||
#:on-add (log "TM learns that task-runner ~a is IDLE" id)
|
(on-start
|
||||||
#:on-remove (log "TM learns that task-runner ~a is NOT IDLE" id))
|
(for ([_ (in-range num-task-runners)])
|
||||||
(assert (task-manager id (set-count (idle-runners))))
|
(define tr-id (gensym 'task-runner))
|
||||||
(field [busy-runners (list)])
|
(react
|
||||||
(during (task-assignment id $job-id $t)
|
(on-start (spawn-task-runner tr-id id))
|
||||||
(match-define (task task-id desc) t)
|
(on (asserted (task-runner tr-id))
|
||||||
#;(on-start (log "TM receives task ~a" task-id))
|
(log "TM ~a successfully created task-runner ~a" id tr-id)
|
||||||
(log "TM receives task ~a" task-id)
|
(task-runners (set-add (task-runners) tr-id)))
|
||||||
(on-stop (log "TM finished with task ~a" task-id))
|
(on (retracted (task-runner tr-id))
|
||||||
(field [status ACCEPTED])
|
(log "TM ~a detected failure of task runner ~a, restarting" id tr-id)
|
||||||
;; TODO - could delegate this assertion, in the non-overloaded case, to TaskRunner
|
(task-runners (set-remove (task-runners) tr-id))
|
||||||
;; (also removing the first id from task-state)
|
(spawn-task-runner tr-id id)))))
|
||||||
(assert (task-state id job-id task-id (status)))
|
|
||||||
(cond
|
;; Assign incoming tasks
|
||||||
[(set-empty? (idle-runners))
|
(field [busy-runners (set)])
|
||||||
(log "TM can't run ~a right now" task-id)
|
|
||||||
(status OVERLOAD)]
|
(define (idle-runners)
|
||||||
[else
|
(set-count (set-subtract (task-runners) (busy-runners))))
|
||||||
(define runner (set-first (idle-runners)))
|
|
||||||
;; n.b. modifying a query set is questionable
|
(assert (task-manager id (idle-runners)))
|
||||||
;; 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
|
(define (can-accept?)
|
||||||
(idle-runners (set-remove (idle-runners) runner))
|
(positive? (idle-runners)))
|
||||||
(log "TM assigns task ~a to runner ~a" task-id runner)
|
(define (select-runner)
|
||||||
(assert (task-assignment runner job-id t))
|
(define runner (for/first ([r (in-set (task-runners))]
|
||||||
(status RUNNING)
|
#:unless (set-member? (busy-runners) r))
|
||||||
(on (asserted (task-state runner job-id task-id $state))
|
r))
|
||||||
(match state
|
(unless runner
|
||||||
[(or (== ACCEPTED)
|
(log "ERROR: TM ~a failed to select a runner.\nrunners: ~a\nbusy: ~a" id (task-runners) (busy-runners)))
|
||||||
(== RUNNING))
|
(busy-runners (set-add (busy-runners) runner))
|
||||||
;; nothing to do
|
runner)
|
||||||
(void)]
|
(define (perform-task tsk on-complete! update-status!)
|
||||||
[(== OVERLOAD)
|
(match-define (task task-id desc) tsk)
|
||||||
(log "TM overloaded TR with task ~a" task-id)
|
(define runner (select-runner))
|
||||||
(status OVERLOAD)]
|
(log "TM ~a assigns task ~a to runner ~a" id task-id runner)
|
||||||
[(finished results)
|
(on-stop (busy-runners (set-remove (busy-runners) runner)))
|
||||||
(log "TM receives the results of task ~a" task-id)
|
(on-start
|
||||||
(status state)]))])))))
|
(task-assigner tsk runner
|
||||||
|
(lambda () (update-status! OVERLOAD))
|
||||||
|
(lambda (results) (on-complete! results)))))
|
||||||
|
(on-start
|
||||||
|
(task-performer id can-accept? perform-task)))))
|
||||||
|
|
||||||
;; ---------------------------------------------------------------------------------------------------
|
;; ---------------------------------------------------------------------------------------------------
|
||||||
;; JobManager
|
;; JobManager
|
||||||
|
@ -263,14 +301,13 @@ The JobManager then performs the job and, when finished, asserts (job-finished I
|
||||||
;; ID -> Void
|
;; ID -> Void
|
||||||
;; mark that we have requested the given task manager to perform a task
|
;; mark that we have requested the given task manager to perform a task
|
||||||
(define (take-slot! id)
|
(define (take-slot! id)
|
||||||
(log "JM assigns a task to ~a" id)
|
|
||||||
(requests-in-flight (hash-update (requests-in-flight) id add1 0)))
|
(requests-in-flight (hash-update (requests-in-flight) id add1 0)))
|
||||||
;; ID -> Void
|
;; ID -> Void
|
||||||
;; mark that we have heard back from the given manager about a requested task
|
;; mark that we have heard back from the given manager about a requested task
|
||||||
(define (received-answer! id)
|
(define (received-answer! id)
|
||||||
(requests-in-flight (hash-update (requests-in-flight) id sub1)))
|
(requests-in-flight (hash-update (requests-in-flight) id sub1)))
|
||||||
|
|
||||||
(during (job $job-id $tasks)
|
(during (observe (job-completion $job-id $tasks _))
|
||||||
(log "JM receives job ~a" job-id)
|
(log "JM receives job ~a" job-id)
|
||||||
(define-values (ready not-ready) (partition task-ready? tasks))
|
(define-values (ready not-ready) (partition task-ready? tasks))
|
||||||
(field [ready-tasks ready]
|
(field [ready-tasks ready]
|
||||||
|
@ -297,43 +334,53 @@ The JobManager then performs the job and, when finished, asserts (job-finished I
|
||||||
;; Requires (task-ready? t)
|
;; Requires (task-ready? t)
|
||||||
(define (perform-task t k)
|
(define (perform-task t k)
|
||||||
(react
|
(react
|
||||||
|
(define task-facet (current-facet-id))
|
||||||
(on-start (tasks-in-progress (add1 (tasks-in-progress))))
|
(on-start (tasks-in-progress (add1 (tasks-in-progress))))
|
||||||
(on-stop (tasks-in-progress (sub1 (tasks-in-progress))))
|
(on-stop (tasks-in-progress (sub1 (tasks-in-progress))))
|
||||||
(match-define (task this-id desc) t)
|
(match-define (task this-id desc) t)
|
||||||
(log "JM begins on task ~a" this-id)
|
(log "JM begins on task ~a" this-id)
|
||||||
|
|
||||||
(field [task-mngr #f])
|
(define (select-a-task-manager)
|
||||||
|
(react
|
||||||
|
(field [selection #f])
|
||||||
(begin/dataflow
|
(begin/dataflow
|
||||||
;; n.b. cyclic data-flow dependency
|
(unless (selection)
|
||||||
(unless (task-mngr)
|
|
||||||
(define mngr
|
(define mngr
|
||||||
(for/first ([(id slots) (in-hash (task-managers))]
|
(for/first ([(id slots) (in-hash (task-managers))]
|
||||||
#:when (positive? (- slots (hash-ref (requests-in-flight) id 0))))
|
#:when (positive? (- slots (hash-ref (requests-in-flight) id 0))))
|
||||||
id))
|
id))
|
||||||
(when mngr
|
(when mngr
|
||||||
|
(selection mngr)
|
||||||
(take-slot! mngr)
|
(take-slot! mngr)
|
||||||
(react (stop-when (asserted (task-state mngr job-id this-id _))
|
(log "JM assigns task ~a to ~a" this-id mngr)
|
||||||
|
(stop-current-facet (assign-task mngr)))))))
|
||||||
|
|
||||||
|
;; ID -> ...
|
||||||
|
(define (assign-task mngr)
|
||||||
|
(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
|
||||||
|
;; N.B. when this line was here, and not after `(when mngr ...)` above,
|
||||||
|
;; things didn't work. I think that due to script scheduling, all ready
|
||||||
|
;; tasks were being assigned to the manager
|
||||||
|
#;(take-slot! mngr)
|
||||||
|
(react (stop-when (asserted (task-performance mngr t _))
|
||||||
(received-answer! mngr)))
|
(received-answer! mngr)))
|
||||||
(task-mngr mngr))))
|
(task-assigner t mngr
|
||||||
;; TODO - should respond if task manager dies
|
(lambda ()
|
||||||
(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
|
;; 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,
|
;; 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
|
;; 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)
|
(log "JM overloaded manager ~a with task ~a" mngr this-id)
|
||||||
(task-mngr #f)]
|
(stop-facet this-facet (select-a-task-manager)))
|
||||||
[(finished results)
|
(lambda (results)
|
||||||
(log "JM receives the results of task ~a" this-id)
|
(log "JM receives the results of task ~a" this-id)
|
||||||
(stop-current-facet (k this-id results))]))))
|
(stop-facet task-facet (k (first this-id) results)))))))
|
||||||
|
|
||||||
|
(on-start (select-a-task-manager))))
|
||||||
|
|
||||||
;; ID Data -> Void
|
;; ID Data -> Void
|
||||||
;; Update any dependent tasks with the results of the given task, moving
|
;; Update any dependent tasks with the results of the given task, moving
|
||||||
|
@ -344,7 +391,7 @@ The JobManager then performs the job and, when finished, asserts (job-finished I
|
||||||
(empty? (ready-tasks))
|
(empty? (ready-tasks))
|
||||||
(empty? (waiting-tasks)))
|
(empty? (waiting-tasks)))
|
||||||
(log "JM finished with job ~a" job-id)
|
(log "JM finished with job ~a" job-id)
|
||||||
(react (assert (job-finished job-id data)))]
|
(react (assert (job-completion job-id tasks data)))]
|
||||||
[else
|
[else
|
||||||
;; TODO - in MapReduce, there should be either 1 waiting task, or 0, meaning the job is done.
|
;; TODO - in MapReduce, there should be either 1 waiting task, or 0, meaning the job is done.
|
||||||
(define still-waiting
|
(define still-waiting
|
||||||
|
@ -390,8 +437,7 @@ The JobManager then performs the job and, when finished, asserts (job-finished I
|
||||||
;; Job -> Void
|
;; Job -> Void
|
||||||
(define (spawn-client j)
|
(define (spawn-client j)
|
||||||
(spawn
|
(spawn
|
||||||
(assert j)
|
(on (asserted (job-completion (job-id j) (job-tasks j) $data))
|
||||||
(on (asserted (job-finished (job-id j) $data))
|
|
||||||
(printf "job done!\n~a\n" data))))
|
(printf "job done!\n~a\n" data))))
|
||||||
|
|
||||||
;; ---------------------------------------------------------------------------------------------------
|
;; ---------------------------------------------------------------------------------------------------
|
||||||
|
@ -401,7 +447,7 @@ The JobManager then performs the job and, when finished, asserts (job-finished I
|
||||||
(spawn
|
(spawn
|
||||||
(during (job-manager-alive)
|
(during (job-manager-alive)
|
||||||
(during (task-manager $tm-id _)
|
(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])
|
(field [high-water-mark 0])
|
||||||
(on (asserted (task-manager tm-id $slots))
|
(on (asserted (task-manager tm-id $slots))
|
||||||
(when (> slots (high-water-mark))
|
(when (> slots (high-water-mark))
|
||||||
|
@ -458,7 +504,7 @@ The JobManager then performs the job and, when finished, asserts (job-finished I
|
||||||
|
|
||||||
;; TaskTree -> (Listof Task)
|
;; TaskTree -> (Listof Task)
|
||||||
;; flatten a task tree by assigning job-unique IDs
|
;; flatten a task tree by assigning job-unique IDs
|
||||||
(define (task-tree->list tt)
|
(define (task-tree->list tt job-id)
|
||||||
(define-values (tasks _)
|
(define-values (tasks _)
|
||||||
;; TaskTree ID -> (Values (Listof Task) ID)
|
;; TaskTree ID -> (Values (Listof Task) ID)
|
||||||
;; the input id is for the current node of the tree
|
;; the input id is for the current node of the tree
|
||||||
|
@ -467,7 +513,7 @@ The JobManager then performs the job and, when finished, asserts (job-finished I
|
||||||
[next-id 0])
|
[next-id 0])
|
||||||
(match tt
|
(match tt
|
||||||
[(map-work _)
|
[(map-work _)
|
||||||
(values (list (task next-id tt))
|
(values (list (task (list next-id job-id) tt))
|
||||||
(add1 next-id))]
|
(add1 next-id))]
|
||||||
[(reduce-work left right)
|
[(reduce-work left right)
|
||||||
(define left-id (add1 next-id))
|
(define left-id (add1 next-id))
|
||||||
|
@ -475,7 +521,7 @@ The JobManager then performs the job and, when finished, asserts (job-finished I
|
||||||
(loop left left-id))
|
(loop left left-id))
|
||||||
(define-values (rights next)
|
(define-values (rights next)
|
||||||
(loop right right-id))
|
(loop right right-id))
|
||||||
(values (cons (task next-id (reduce-work left-id right-id))
|
(values (cons (task (list next-id job-id) (reduce-work left-id right-id))
|
||||||
(append lefts rights))
|
(append lefts rights))
|
||||||
next)])))
|
next)])))
|
||||||
tasks)
|
tasks)
|
||||||
|
@ -484,7 +530,7 @@ The JobManager then performs the job and, when finished, asserts (job-finished I
|
||||||
(define (create-job in)
|
(define (create-job in)
|
||||||
(define job-id (gensym 'job))
|
(define job-id (gensym 'job))
|
||||||
(define input-lines (sequence->list (in-lines in)))
|
(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))
|
(job job-id tasks))
|
||||||
|
|
||||||
;; String -> Job
|
;; String -> Job
|
||||||
|
@ -514,7 +560,7 @@ The JobManager then performs the job and, when finished, asserts (job-finished I
|
||||||
(task mid2 (map-work data2)))
|
(task mid2 (map-work data2)))
|
||||||
(check-true (id? left))
|
(check-true (id? left))
|
||||||
(check-true (id? right))
|
(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)
|
(check-equal? (set data1 data2)
|
||||||
(set "a b c" "d e f"))]
|
(set "a b c" "d e f"))]
|
||||||
[_
|
[_
|
||||||
|
@ -540,9 +586,12 @@ The JobManager then performs the job and, when finished, asserts (job-finished I
|
||||||
;; expected:
|
;; expected:
|
||||||
;; #hash((a . 5) (b . 5) (c . 2))
|
;; #hash((a . 5) (b . 5) (c . 2))
|
||||||
|
|
||||||
|
(spawn-client j)
|
||||||
(spawn-client (file->job "lorem.txt"))
|
(spawn-client (file->job "lorem.txt"))
|
||||||
(spawn-job-manager)
|
(spawn-job-manager)
|
||||||
(spawn-task-manager)
|
(spawn-task-manager 2)
|
||||||
(spawn-task-runner)
|
(spawn-task-manager 3)
|
||||||
(spawn-task-runner)
|
|
||||||
(spawn-observer)
|
(spawn-observer)
|
||||||
|
|
||||||
|
(module+ main
|
||||||
|
(void))
|
||||||
|
|
|
@ -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)))
|
|
@ -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)))
|
|
@ -14,6 +14,7 @@
|
||||||
limit-patch
|
limit-patch
|
||||||
patch-step
|
patch-step
|
||||||
patch-step*
|
patch-step*
|
||||||
|
patch-prepend
|
||||||
compute-aggregate-patch
|
compute-aggregate-patch
|
||||||
apply-patch
|
apply-patch
|
||||||
update-interests
|
update-interests
|
||||||
|
@ -125,6 +126,13 @@
|
||||||
(define (patch-step* p keys)
|
(define (patch-step* p keys)
|
||||||
(foldl (lambda (key p) (patch-step p key)) 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
|
;; Entries labelled with `label` may already exist in `base`; the
|
||||||
;; patch `p` MUST already have been limited to add only where no
|
;; patch `p` MUST already have been limited to add only where no
|
||||||
;; `label`-labelled portions of `base` exist, and to remove only where
|
;; `label`-labelled portions of `base` exist, and to remove only where
|
||||||
|
|
|
@ -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
|
|
@ -0,0 +1,404 @@
|
||||||
|
#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 (eps ... ...))
|
||||||
|
(⇒ ν-f #,(make-Branch #'((fs ...) ...)))
|
||||||
|
(⇒ ν-s (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)
|
||||||
|
------------------------------------------------------------
|
||||||
|
)
|
File diff suppressed because it is too large
Load Diff
|
@ -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)))])))
|
|
@ -47,34 +47,35 @@
|
||||||
|
|
||||||
(define (lookup [title : String]
|
(define (lookup [title : String]
|
||||||
[inv : Inventory] -> Int)
|
[inv : Inventory] -> Int)
|
||||||
(for/fold [stock 0]
|
(for/fold ([stock 0])
|
||||||
[item inv]
|
([item inv])
|
||||||
(if (equal? title (select 0 item))
|
(if (equal? title (select 0 item))
|
||||||
(select 1 item)
|
(select 1 item)
|
||||||
stock)))
|
stock)))
|
||||||
|
|
||||||
(define-type-alias seller-role
|
(define-type-alias seller-role
|
||||||
(Role (seller)
|
(Role (seller)
|
||||||
(Reacts (Know (Observe (BookQuoteT String ★/t)))
|
(Reacts (Asserted (Observe (BookQuoteT String ★/t)))
|
||||||
(Role (_)
|
(Role (_)
|
||||||
;; nb no mention of retracting this assertion
|
;; nb no mention of retracting this assertion
|
||||||
(Shares (BookQuoteT String Int))))))
|
(Shares (BookQuoteT String Int))))))
|
||||||
|
|
||||||
(define (spawn-seller [inventory : Inventory])
|
(define (spawn-seller [inventory : Inventory])
|
||||||
(spawn τc
|
(spawn τc
|
||||||
|
(begin
|
||||||
(start-facet seller
|
(start-facet seller
|
||||||
(field [books Inventory inventory])
|
(field [books Inventory inventory])
|
||||||
|
|
||||||
;; Give quotes to interested parties.
|
;; Give quotes to interested parties.
|
||||||
(during (observe (book-quote (bind title String) discard))
|
(during (observe (book-quote $title _))
|
||||||
;; TODO - lookup
|
;; TODO - lookup
|
||||||
(assert (book-quote title (lookup title (ref books))))))))
|
(assert (book-quote title (lookup title (ref books)))))))))
|
||||||
|
|
||||||
(define-type-alias leader-role
|
(define-type-alias leader-role
|
||||||
(Role (leader)
|
(Role (leader)
|
||||||
(Reacts (Know (BookQuoteT String Int))
|
(Reacts (Asserted (BookQuoteT String Int))
|
||||||
(Role (poll)
|
(Role (poll)
|
||||||
(Reacts (Know (BookInterestT String String Bool))
|
(Reacts (Asserted (BookInterestT String String Bool))
|
||||||
;; this is actually implemented indirectly through dataflow
|
;; this is actually implemented indirectly through dataflow
|
||||||
(U (Stop leader
|
(U (Stop leader
|
||||||
(Role (_)
|
(Role (_)
|
||||||
|
@ -83,7 +84,7 @@
|
||||||
|
|
||||||
(define-type-alias leader-actual
|
(define-type-alias leader-actual
|
||||||
(Role (get-quotes31)
|
(Role (get-quotes31)
|
||||||
(Reacts (Know (BookQuoteT String (Bind Int)))
|
(Reacts (Asserted (BookQuoteT String (Bind Int)))
|
||||||
(Stop get-quotes)
|
(Stop get-quotes)
|
||||||
(Role (poll-members36)
|
(Role (poll-members36)
|
||||||
(Reacts OnDataflow
|
(Reacts OnDataflow
|
||||||
|
@ -92,12 +93,12 @@
|
||||||
(Stop get-quotes
|
(Stop get-quotes
|
||||||
(Role (announce39)
|
(Role (announce39)
|
||||||
(Shares (BookOfTheMonthT String)))))
|
(Shares (BookOfTheMonthT String)))))
|
||||||
(Reacts (¬Know (BookInterestT String (Bind String) Bool)))
|
(Reacts (Retracted (BookInterestT String (Bind String) Bool)))
|
||||||
(Reacts (Know (BookInterestT String (Bind String) Bool)))
|
(Reacts (Asserted (BookInterestT String (Bind String) Bool)))
|
||||||
(Reacts (¬Know (BookInterestT String (Bind String) Bool)))
|
(Reacts (Retracted (BookInterestT String (Bind String) Bool)))
|
||||||
(Reacts (Know (BookInterestT String (Bind String) Bool)))))
|
(Reacts (Asserted (BookInterestT String (Bind String) Bool)))))
|
||||||
(Reacts (¬Know (ClubMemberT (Bind String))))
|
(Reacts (Retracted (ClubMemberT (Bind String))))
|
||||||
(Reacts (Know (ClubMemberT (Bind String))))))
|
(Reacts (Asserted (ClubMemberT (Bind String))))))
|
||||||
|
|
||||||
(define (spawn-leader [titles : (List String)])
|
(define (spawn-leader [titles : (List String)])
|
||||||
(spawn τc
|
(spawn τc
|
||||||
|
@ -115,10 +116,10 @@
|
||||||
(set! book-list (rest (ref book-list)))]))
|
(set! book-list (rest (ref book-list)))]))
|
||||||
|
|
||||||
;; keep track of book club members
|
;; 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-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))
|
(printf "leader learns that there are ~a copies of ~a\n" quantity (ref title))
|
||||||
(cond
|
(cond
|
||||||
[(< quantity (+ 1 (set-count (ref members))))
|
[(< quantity (+ 1 (set-count (ref members))))
|
||||||
|
@ -127,9 +128,22 @@
|
||||||
[#t
|
[#t
|
||||||
;; find out if at least half of the members want to read the book
|
;; find out if at least half of the members want to read the book
|
||||||
(start-facet poll-members
|
(start-facet poll-members
|
||||||
(define/query-set yays (book-interest (ref title) (bind name String) #t) name)
|
(define/query-set yays (book-interest (ref title) $name #t) name)
|
||||||
(define/query-set nays (book-interest (ref title) (bind name String) #f) name)
|
(define/query-set nays (book-interest (ref title) $name #f) name)
|
||||||
(begin/dataflow
|
(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'
|
;; count the leader as a 'yay'
|
||||||
(when (>= (set-count (ref yays))
|
(when (>= (set-count (ref yays))
|
||||||
(/ (set-count (ref members)) 2))
|
(/ (set-count (ref members)) 2))
|
||||||
|
@ -146,21 +160,22 @@
|
||||||
(Role (member)
|
(Role (member)
|
||||||
(Shares (ClubMemberT String))
|
(Shares (ClubMemberT String))
|
||||||
;; should this be the type of the pattern? or lowered to concrete types?
|
;; 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 (_)
|
(Role (_)
|
||||||
(Shares (BookInterestT String String Bool))))))
|
(Shares (BookInterestT String String Bool))))))
|
||||||
|
|
||||||
(define (spawn-club-member [name : String]
|
(define (spawn-club-member [name : String]
|
||||||
[titles : (List String)])
|
[titles : (List String)])
|
||||||
(spawn τc
|
(spawn τc
|
||||||
|
(print-role
|
||||||
(start-facet member
|
(start-facet member
|
||||||
;; assert our presence
|
;; assert our presence
|
||||||
(assert (club-member name))
|
(assert (club-member name))
|
||||||
;; respond to polls
|
;; respond to polls
|
||||||
(during (observe (book-interest (bind title String) discard discard))
|
(during (observe (book-interest $title _ _))
|
||||||
(define answer (member? title titles))
|
(define answer (member? title titles))
|
||||||
(printf "~a responds to suggested book ~a: ~a\n" name title answer)
|
(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
|
(run-ground-dataspace τc
|
||||||
(spawn-seller (list (tuple "The Wind in the Willows" 5)
|
(spawn-seller (list (tuple "The Wind in the Willows" 5)
|
||||||
|
|
|
@ -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)
|
|
@ -0,0 +1,531 @@
|
||||||
|
#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)))]))
|
||||||
|
|
||||||
|
(assertion-struct assigned-task : SelectedTM (mngr))
|
||||||
|
(message-struct tasks-finished : TasksFinished (id results))
|
||||||
|
|
||||||
|
(define (spawn-job-manager)
|
||||||
|
(spawn τc
|
||||||
|
(begin
|
||||||
|
(start-facet jm
|
||||||
|
(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 (hash-ref (ref task-managers) id)))
|
||||||
|
|
||||||
|
;; (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 ID Int) (hash)])
|
||||||
|
(define (slots-available)
|
||||||
|
(for/sum ([(id v) (ref task-managers)])
|
||||||
|
(max 0 (- v (hash-ref/failure (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 : ID])
|
||||||
|
(log "JM assigns a task to ~a" id)
|
||||||
|
(set! requests-in-flight (hash-update/failure (ref 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 : ID])
|
||||||
|
(set! requests-in-flight (hash-update (ref requests-in-flight) id sub1)))
|
||||||
|
|
||||||
|
(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 [ready-tasks (List ConcreteTask) ready]
|
||||||
|
[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)
|
||||||
|
(set! ready-tasks (cons t (ref ready-tasks))))
|
||||||
|
|
||||||
|
;; 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 ready-tasks))
|
||||||
|
(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)
|
||||||
|
|
||||||
|
(define not-a-real-task-manager (gensym 'FAKE))
|
||||||
|
(field [task-mngr ID not-a-real-task-manager])
|
||||||
|
|
||||||
|
;; ID -> ...
|
||||||
|
(define (assign-task [mngr : ID])
|
||||||
|
(start-facet assign
|
||||||
|
(know (assigned-task mngr))
|
||||||
|
(on (retracted (task-manager mngr _))
|
||||||
|
;; our task manager has crashed
|
||||||
|
(stop assign))
|
||||||
|
(on start
|
||||||
|
;; N.B. when this line was here, and not after `(when mngr ...)` above,
|
||||||
|
;; things didn't work. I think that due to script scheduling, all ready
|
||||||
|
;; tasks were being assigned to the manager
|
||||||
|
#;(take-slot! mngr)
|
||||||
|
(start-facet take-slot
|
||||||
|
(on (asserted (task-performance mngr t _))
|
||||||
|
(stop take-slot
|
||||||
|
(received-answer! mngr)))))
|
||||||
|
(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)]
|
||||||
|
[(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 [mngr (Maybe ID) none])
|
||||||
|
|
||||||
|
(define (try-assign!)
|
||||||
|
(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)
|
||||||
|
(take-slot! m)
|
||||||
|
(set! mngr (some m))
|
||||||
|
(assign-task m)]
|
||||||
|
[none
|
||||||
|
#f]))
|
||||||
|
|
||||||
|
(begin/dataflow
|
||||||
|
(when (equal? (ref mngr) none)
|
||||||
|
(try-assign!)))
|
||||||
|
|
||||||
|
(on (forget (assigned-task $m:ID))
|
||||||
|
(when (equal? (some m) (ref mngr))
|
||||||
|
(set! mngr none)))))
|
||||||
|
|
||||||
|
(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)))))
|
||||||
|
(begin/dataflow
|
||||||
|
(define slots (slots-available))
|
||||||
|
(define-tuple (ts readys)
|
||||||
|
(split-at/lenient (ref ready-tasks) slots))
|
||||||
|
(for ([t ts])
|
||||||
|
(perform-task t push-results))
|
||||||
|
(unless (empty? ts)
|
||||||
|
;; the empty? check may be necessary to avoid a dataflow loop
|
||||||
|
(set! ready-tasks readys))))))))))
|
||||||
|
|
||||||
|
;; ---------------------------------------------------------------------------------------------------
|
||||||
|
;; 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)))
|
|
@ -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)))))))))))))))))
|
||||||
|
)
|
|
@ -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.
|
|
@ -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)))))
|
||||||
|
)
|
|
@ -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))))))
|
|
@ -62,7 +62,7 @@
|
||||||
|
|
||||||
(define-type-alias seller-role
|
(define-type-alias seller-role
|
||||||
(Role (seller)
|
(Role (seller)
|
||||||
(Reacts (Know (Observe (QuoteT String ★/t)))
|
(Reacts (Asserted (Observe (QuoteT String ★/t)))
|
||||||
(Role (_)
|
(Role (_)
|
||||||
(Shares (QuoteT String Int))))))
|
(Shares (QuoteT String Int))))))
|
||||||
|
|
||||||
|
|
|
@ -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 ...))])
|
|
@ -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))
|
|
@ -0,0 +1,8 @@
|
||||||
|
#lang info
|
||||||
|
|
||||||
|
(define compile-omit-paths
|
||||||
|
'("examples"
|
||||||
|
"tests"))
|
||||||
|
|
||||||
|
(define test-omit-paths
|
||||||
|
'("examples/roles/chat-tcp2.rkt"))
|
|
@ -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)
|
||||||
|
*/
|
||||||
|
}
|
|
@ -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))
|
|
@ -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")]))
|
|
@ -0,0 +1,109 @@
|
||||||
|
#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 or (→ Bool Bool (Computation (Value Bool) (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)])
|
||||||
|
|
||||||
|
;; for some reason defining `and` as a prim op doesn't work
|
||||||
|
(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 (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)])
|
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
|
@ -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)])
|
|
@ -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 τ)])
|
|
@ -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))
|
||||||
|
)
|
|
@ -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))))
|
|
@ -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")
|
|
@ -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)
|
|
@ -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)
|
|
@ -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)
|
|
@ -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))))
|
|
@ -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)))))))"))
|
|
@ -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))
|
|
@ -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"))
|
Loading…
Reference in New Issue