From 8808b5aca94f9219a17f0103fb917ace41ae697c Mon Sep 17 00:00:00 2001 From: Sam Caldwell Date: Wed, 16 May 2018 15:58:02 -0400 Subject: [PATCH] typed book club --- racket/typed/core.rkt | 12 ++- racket/typed/examples/core/book-club.rkt | 102 ++++++++++++++++++++++- 2 files changed, 108 insertions(+), 6 deletions(-) diff --git a/racket/typed/core.rkt b/racket/typed/core.rkt index 04c0e75..708c431 100644 --- a/racket/typed/core.rkt +++ b/racket/typed/core.rkt @@ -35,6 +35,8 @@ ;; DEBUG and utilities print-type (rename-out [printf- printf]) + begin-for-syntax + (for-syntax #%app displayln type-eval current-type? syntax) ;; Extensions ) @@ -128,9 +130,9 @@ ;; (copied from ext-stlc example) (define-syntax define-type-alias (syntax-parser - [(_ alias:id τ:any-type) + [(_ alias:id τ) #'(define-syntax- alias - (make-variable-like-transformer #'τ.norm))] + (make-variable-like-transformer #'τ))] [(_ (f:id x:id ...) ty) #'(define-syntax- (f stx) (syntax-parse stx @@ -563,7 +565,7 @@ [⊢ e-as ≫ e-as- ⇒ (~List τ)] ;; this parsing of actions is getting realllly hacky #:with (~or (~Action τ-o τ-a) - (~parse (τ-o τ-a) #'(⊥ ⊥))) #'τ + (~parse (τ-o τ-a) (stx-map type-eval #'(⊥ ⊥)))) #'τ ----------------------------------------- [⊢ (syndicate:transition e-s- e-as-) ⇒ (Instruction τ-s τ-o τ-a)]) @@ -1176,4 +1178,6 @@ (module+ test (check-type (transition #f (list)) : (Instruction Bool ⊥ ⊥) - -> (syndicate:transition #f (list-)))) \ No newline at end of file + -> (syndicate:transition #f (list-))) + (check-type (quit) : (Instruction ⊥ ⊥ ⊥)) + (check-type (quit (list)) : (Instruction ⊥ ⊥ ⊥))) \ No newline at end of file diff --git a/racket/typed/examples/core/book-club.rkt b/racket/typed/examples/core/book-club.rkt index 8da4084..046d4d2 100644 --- a/racket/typed/examples/core/book-club.rkt +++ b/racket/typed/examples/core/book-club.rkt @@ -17,12 +17,15 @@ (define-type-alias τc (U (ClubMember String) + (Observe (ClubMember ★/t)) (BookInterest String String Bool) (Observe (BookInterest String ★/t ★/t)) (Observe (Observe (BookInterest ★/t ★/t ★/t))) (InStock String Int) (Observe (InStock String ★/t)) - (Observe (Observe (InStock ★/t ★/t))))) + (Observe (Observe (InStock ★/t ★/t))) + (BookOfTheMonth String) + (Observe (BookOfTheMonth ★/t)))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Leader @@ -78,6 +81,86 @@ (unsub (book-interest ★ ★ ★)) (sub (in-stock next ★)))))))) +(define (leader-learns [quantity : Int] + [title : String] + -> (Tuple)) + (displayln "leader learns that there are") + (displayln quantity) + (displayln "copies of") + (displayln title) + (tuple)) + +(define (respond-to-quotes [added : (AssertionSet τc)] + [title : String] + [interests : (List String)] + [members : (Set String)] + [changed? Bool] + -> (Instruction LeaderState τc τc)) + (let ([answers (project [(in-stock title (bind n Int)) added] n)]) + (if (empty? answers) + (if changed? + (transition (leader-state title interests members "quote" (set) (set)) (list)) + idle) + (let ([quantity (first answers)]) + (leader-learns quantity title) + (if (<= quantity (set-count members)) + (begin (displayln "there aren't enough copies to go around") + (next-book interests members)) + (transition (leader-state title interests members "poll" (set) (set)) + (list (sub (book-interest title ★ ★))))))))) + +(define (respond-to-interests [added : (AssertionSet τc)] + [title : String] + [books : (List String)] + [members : (Set String)] + [yays : (Set String)] + [nays : (Set String)] + -> (Instruction LeaderState τc τc)) + (let ([yups (set-union yays (list->set (project [(book-interest title (bind name String) #t) added] + name)))] + [nups (set-union nays (list->set (project [(book-interest title (bind name String) #f) added] + name)))]) + (if (>= (set-count yups) (/ (set-count members) 2)) + (begin (displayln "leader finds enough affirmation for") (displayln title) + (transition (leader-state title books members "complete" yays nays) + (list (patch-seq (assert (book-of-the-month title)) + (unsub (book-interest ★ ★ ★)))))) + (if (> (set-count nups) (/ (set-count members) 2)) + (begin (displayln "leader finds enough negative nancys for") (displayln title) + (next-book books members)) + (transition (leader-state title books members "poll" yups nups) (list)))))) + +(define (leader-behavior [e : (Event τc)] + [s : LeaderState] + -> (Instruction LeaderState τc τc)) + (let* ([added (patch-added e)] + [retracted (patch-removed e)] + [title (leader-state-current-title s)] + [books (leader-state-interests s)] + [members (leader-state-members s)] + [state (leader-state-conv s)] + [yays (leader-state-yays s)] + [nays (leader-state-nays s)] + [new-members (update-members members added retracted)] + [changed? (not (equal? new-members members))]) + (if changed? + (begin (displayln "leader knows about") (displayln new-members) #f) + #f) + (if (equal? state "quote") + (respond-to-quotes added title books new-members changed?) + (if (equal? state "poll") + (respond-to-interests added title books new-members yays nays) + idle)))) + +(define (make-leader [interests : (List String)] -> (Actor τc)) + (let ([first-book (first interests)] + [books (rest interests)]) + (actor τc + leader-behavior + (leader-state first-book books (set) "quote" (set) (set)) + (make-assertion-set (observe (in-stock first-book ★)) + (observe (club-member ★)))))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Seller @@ -122,4 +205,19 @@ (transition s answers))) #f (make-assertion-set (club-member name) - (observe (observe (book-interest ★ ★ ★)))))) \ No newline at end of file + (observe (observe (book-interest ★ ★ ★)))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Main + +(dataspace τc + (list + (make-book-seller (list (tuple "The Wind in the Willows" 5) + (tuple "Catch 22" 2) + (tuple "Candide" 3))) + (make-leader (list "The Wind in the Willows" + "Catch 22" + "Candide" + "Encyclopaedia Brittannica")) + (make-club-member "tony" (list "Candide")) + (make-club-member "sam" (list "Encyclopaedia Brittannica" "Candide")))) \ No newline at end of file