From 07785e92329ce4dc73adcaf6d93b2793ef760f8a Mon Sep 17 00:00:00 2001 From: Tony Garnock-Jones Date: Mon, 29 Feb 2016 10:24:25 -0500 Subject: [PATCH] Add "during". --- doc/notes-on-hll.md | 10 +++ prospect/actor.rkt | 80 +++++++++++++------ prospect/comprehensions.rkt | 2 +- .../examples/actor/file-system-during.rkt | 68 ++++++++++++++++ 4 files changed, 135 insertions(+), 25 deletions(-) create mode 100644 prospect/examples/actor/file-system-during.rkt diff --git a/doc/notes-on-hll.md b/doc/notes-on-hll.md index 9c6062b..64fdb25 100644 --- a/doc/notes-on-hll.md +++ b/doc/notes-on-hll.md @@ -14,6 +14,7 @@ Just a sketch, at the moment. Optional Bindings, B := ;; nothing, or #:collect [(id I) ...] Ongoing actions, O := (on E I ...) + (during P O ...) (once E I ...) ;; ??? (assert P) (assert #:when Pred P) @@ -101,6 +102,15 @@ Note that `exists` (and so `forall`) are tricky because of the nested `Pred`. For now, I'm not implementing them -- we'll see how painful it is to use `track` and plain-old `expr` `Pred`s instead. +`during` is a quasi-macro, with defining equation + + (during P O ...) === (on (asserted P) + (until (retracted P') + O ...)) + +where `P'` is like `P` but with all the binders in `P` instantiated +with their values at the time the `until` is started. + ## Examples ```racket diff --git a/prospect/actor.rkt b/prospect/actor.rkt index 65eb57c..0a1ab9b 100644 --- a/prospect/actor.rkt +++ b/prospect/actor.rkt @@ -34,6 +34,7 @@ (define&provide-dsl-helper-syntaxes "state/until/forever form" [on + during assert track @@ -223,6 +224,10 @@ (pattern (~seq #:init [I ...])) (pattern (~seq) #:attr [I 1] '())) + (define-splicing-syntax-class done + (pattern (~seq #:done [I ...])) + (pattern (~seq) #:attr [I 1] '())) + (define-splicing-syntax-class bindings (pattern (~seq #:collect [(id init) ...])) (pattern (~seq) #:attr [id 1] '() #:attr [init 1] '()))) @@ -236,8 +241,8 @@ ;; Sugar (define-syntax (until stx) (syntax-parse stx - [(_ E init:init bs:bindings O ...) - #'(state #:init [init.I ...] [#:collect [(bs.id bs.init) ...] O ...] [E (values)])])) + [(_ E init:init done:done bs:bindings O ...) + #'(state #:init [init.I ...] [#:collect [(bs.id bs.init) ...] O ...] [E done.I ... (values)])])) ;; Sugar (define-syntax (forever stx) @@ -499,7 +504,8 @@ s)))))) (define (analyze-asserted-or-retracted! endpoint-index asserted? outer-expr-stx P-stx I-stxs L-stx) - (define-values (proj-stx pat match-pat bindings) (analyze-pattern outer-expr-stx P-stx)) + (define-values (proj-stx pat match-pat bindings _instantiated) + (analyze-pattern outer-expr-stx P-stx)) (add-assertion-maintainer! endpoint-index #'sub pat #f L-stx) (add-event-handler! (lambda (evt-stx) @@ -527,7 +533,8 @@ #`(at-meta #,(prepend-at-meta-stx stx (- level 1))))) (define (analyze-message-subscription! endpoint-index outer-expr-stx P-stx I-stxs L-stx) - (define-values (proj pat match-pat bindings) (analyze-pattern outer-expr-stx P-stx)) + (define-values (proj pat match-pat bindings _instantiated) + (analyze-pattern outer-expr-stx P-stx)) (add-assertion-maintainer! endpoint-index #'sub pat #f L-stx) (add-event-handler! (lambda (evt-stx) @@ -567,8 +574,17 @@ #,(make-run-script-call E-stx #'s I-stxs) (transition s '())))))))])) + (define (analyze-during! index P-stx O-stxs) + (define E-stx #`(asserted #,P-stx)) + (define-values (_proj _pat _match-pat _bindings instantiated) (analyze-pattern E-stx P-stx)) + (define I-stx #`(until (retracted #,instantiated) #,@O-stxs)) + (local-require racket/pretty) + (pretty-print (syntax->datum I-stx)) + (analyze-event! index E-stx #`(#,I-stx))) + (define (analyze-assertion! index Pred-stx outer-expr-stx P-stx L-stx) - (define-values (proj pat match-pat bindings) (analyze-pattern outer-expr-stx P-stx)) + (define-values (proj pat match-pat bindings _instantiated) + (analyze-pattern outer-expr-stx P-stx)) (add-assertion-maintainer! index #'core:assert pat Pred-stx L-stx)) (define (analyze-tracks! index track-spec-stxs I-stxs) @@ -589,9 +605,11 @@ (for [(ongoing (in-list (syntax->list ongoings))) (ongoing-index (in-naturals))] (syntax-parse ongoing - #:literals [on assert track] + #:literals [on during assert track] [(on E I ...) (analyze-event! ongoing-index #'E #'(I ...))] + [(during P O ...) + (analyze-during! ongoing-index #'P #'(O ...))] [(assert w:when-pred P L:meta-level) (analyze-assertion! ongoing-index #'w.Pred ongoing #'P #'L.level)] [(track [track-spec ...] I ...) @@ -732,15 +750,15 @@ (and (dollar-id? stx) (datum->syntax stx (string->symbol (substring (symbol->string (syntax-e stx)) 1))))) - ;; Syntax -> (Values Projection AssertionSetPattern MatchPattern (ListOf Identifier)) + ;; Syntax -> (Values Projection AssertionSetPattern MatchPattern (ListOf Identifier) Syntax) (define (analyze-pattern outer-expr-stx pat-stx0) (let walk ((pat-stx pat-stx0)) (syntax-case pat-stx ($ ? quasiquote unquote quote) ;; Extremely limited support for quasiquoting and quoting [(quasiquote (unquote p)) (walk #'p)] [(quasiquote (p ...)) (walk #'(list (quasiquote p) ...))] - [(quasiquote p) (values #''p #''p #''p '())] - [(quote p) (values #''p #''p #''p '())] + [(quasiquote p) (values #''p #''p #''p '() #''p)] + [(quote p) (values #''p #''p #''p '() #''p)] [$v (dollar-id? #'$v) @@ -748,17 +766,19 @@ (values #'(?!) #'? #'v - (list #'v)))] + (list #'v) + #'v))] [($ v p) (let () - (define-values (pr g m bs) (walk #'p)) + (define-values (pr g m bs _ins) (walk #'p)) (when (not (null? bs)) (raise-syntax-error #f "nested bindings not supported" outer-expr-stx pat-stx)) (values #`(?! #,pr) g #`(and v #,m) - (list #'v)))] + (list #'v) + #'v))] [(? pred? p) ;; TODO: support pred? in asserted/retracted as well as message events @@ -770,31 +790,35 @@ "Predicate '?' matching only supported in message events" outer-expr-stx pat-stx)]) - (define-values (pr g m bs) (walk #'p)) + (define-values (pr g m bs ins) (walk #'p)) (values pr g #`(? pred? #,m) - bs))] + bs + ins))] [(ctor p ...) (let () (define parts (if (identifier? #'ctor) #'(p ...) #'(ctor p ...))) - (define-values (pr g m bs) - (for/fold [(pr '()) (g '()) (m '()) (bs '())] [(p (syntax->list parts))] - (define-values (pr1 g1 m1 bs1) (walk p)) + (define-values (pr g m bs ins) + (for/fold [(pr '()) (g '()) (m '()) (bs '()) (ins '())] [(p (syntax->list parts))] + (define-values (pr1 g1 m1 bs1 ins1) (walk p)) (values (cons pr1 pr) (cons g1 g) (cons m1 m) - (append bs bs1)))) + (append bs bs1) + (cons ins1 ins)))) (if (identifier? #'ctor) (values (cons #'ctor (reverse pr)) (cons #'ctor (reverse g)) (cons #'ctor (reverse m)) - bs) + bs + (cons #'ctor (reverse ins))) (values (reverse pr) (reverse g) (reverse m) - bs)))] + bs + (reverse ins))))] [? (raise-syntax-error #f @@ -808,11 +832,13 @@ (values #'? #'? #'_ - '()) + '() + #'_) (values #'non-pair #'non-pair #'(== non-pair) - '()))]))) + '() + #'non-pair))]))) ) @@ -855,11 +881,12 @@ (begin-for-syntax (define (analyze-and-print pat-stx) - (let-values (((pr g m bs) (analyze-pattern pat-stx pat-stx))) + (let-values (((pr g m bs ins) (analyze-pattern pat-stx pat-stx))) (pretty-print `((pr ,(map syntax->datum pr)) (g ,(map syntax->datum g)) (m ,(map syntax->datum m)) - (bs ,(map syntax->datum bs)))))) + (bs ,(map syntax->datum bs)) + (ins ,(map syntax->datum ins)))))) #;(analyze-and-print #'`(hello ,$who))) @@ -867,6 +894,11 @@ #'(actor (until (rising-edge (= count 10)) #:collect [(count 0)] + (during `(present ,$p) + #:collect [(utterance-count 0)] + (on (message `(says ,p ,$what)) + (println "(~a) ~a says: ~a" utterance-count p what) + (+ utterance-count 1))) (on (message `(hello ,$who)) (println "Got hello: ~a" who) (+ count 1)))))) diff --git a/prospect/comprehensions.rkt b/prospect/comprehensions.rkt index 63eca1b..80821e3 100644 --- a/prospect/comprehensions.rkt +++ b/prospect/comprehensions.rkt @@ -17,7 +17,7 @@ ; (SyntaxOf TempVar TempVar Projection-Pattern Match-Pattern) (define (helper pat-stx outer-stx) (match-define (list temp1 temp2) (generate-temporaries #'(tmp1 tmp2))) - (define-values (proj-stx pat match-pat bindings) + (define-values (proj-stx pat match-pat bindings _instantiated) (analyze-pattern outer-stx pat-stx)) (list temp1 temp2 proj-stx bindings))) diff --git a/prospect/examples/actor/file-system-during.rkt b/prospect/examples/actor/file-system-during.rkt new file mode 100644 index 0000000..8030328 --- /dev/null +++ b/prospect/examples/actor/file-system-during.rkt @@ -0,0 +1,68 @@ +#lang prospect +;; Toy file system, based on the example in the ESOP2016 submission. +;; prospect/actor implementation. + +(require prospect/actor) +(require prospect/drivers/timer) +(require (only-in racket/port read-bytes-line-evt)) +(require (only-in racket/string string-trim string-split)) + +(struct file (name content) #:prefab) +(struct save (file) #:prefab) +(struct delete (name) #:prefab) + +(spawn-timer-driver) + +(actor (forever #:collect [(files (hash))] + (during (observe (file $name _)) + #:init [(printf "At least one reader exists for ~v\n" name)] + #:done [(printf "No remaining readers exist for ~v\n" name)] + #:collect [(content (hash-ref files name #f))] + (assert (file name content)) + (on (message (save (file name $content))) content) + (on (message (delete name)) #f)) + (on (message (save (file $name $content))) (hash-set files name content)) + (on (message (delete $name)) (hash-remove files name)))) + +(define (sleep sec) + (define timer-id (gensym 'sleep)) + (until (message (timer-expired timer-id _)) + #:init [(send! (set-timer timer-id (* sec 1000.0) 'relative))])) + +;; Shell +(let ((e (read-bytes-line-evt (current-input-port) 'any))) + (define (print-prompt) + (printf "> ") + (flush-output)) + (define reader-count 0) + (define (generate-reader-id) + (begin0 reader-count + (set! reader-count (+ reader-count 1)))) + (actor (print-prompt) + (until (message (external-event e (list (? eof-object? _))) #:meta-level 1) + (on (message (external-event e (list (? bytes? $bs))) #:meta-level 1) + (match (string-split (string-trim (bytes->string/utf-8 bs))) + [(list "open" name) + (define reader-id (generate-reader-id)) + (actor (printf "Reader ~a opening file ~v.\n" reader-id name) + (until (message `(stop-watching ,name)) + (on (asserted (file name $contents)) + (printf "Reader ~a sees that ~v contains: ~v\n" + reader-id + name + contents))) + (printf "Reader ~a closing file ~v.\n" reader-id name))] + [(list "close" name) + (send! `(stop-watching ,name))] + [(list* "write" name words) + (send! (save (file name words)))] + [(list "delete" name) + (send! (delete name))] + [_ + (printf "I'm afraid I didn't understand that.\n") + (printf "Try: open filename\n") + (printf " close filename\n") + (printf " write filename some text goes here\n") + (printf " delete filename\n")]) + (sleep 0.1) + (print-prompt)))))