Add "during".
This commit is contained in:
parent
5b328a1786
commit
07785e9232
|
@ -14,6 +14,7 @@ Just a sketch, at the moment.
|
||||||
Optional Bindings, B := ;; nothing, or
|
Optional Bindings, B := ;; nothing, or
|
||||||
#:collect [(id I) ...]
|
#:collect [(id I) ...]
|
||||||
Ongoing actions, O := (on E I ...)
|
Ongoing actions, O := (on E I ...)
|
||||||
|
(during P O ...)
|
||||||
(once E I ...) ;; ???
|
(once E I ...) ;; ???
|
||||||
(assert P)
|
(assert P)
|
||||||
(assert #:when Pred 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
|
`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.
|
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
|
## Examples
|
||||||
|
|
||||||
```racket
|
```racket
|
||||||
|
|
|
@ -34,6 +34,7 @@
|
||||||
|
|
||||||
(define&provide-dsl-helper-syntaxes "state/until/forever form"
|
(define&provide-dsl-helper-syntaxes "state/until/forever form"
|
||||||
[on
|
[on
|
||||||
|
during
|
||||||
assert
|
assert
|
||||||
track
|
track
|
||||||
|
|
||||||
|
@ -223,6 +224,10 @@
|
||||||
(pattern (~seq #:init [I ...]))
|
(pattern (~seq #:init [I ...]))
|
||||||
(pattern (~seq) #:attr [I 1] '()))
|
(pattern (~seq) #:attr [I 1] '()))
|
||||||
|
|
||||||
|
(define-splicing-syntax-class done
|
||||||
|
(pattern (~seq #:done [I ...]))
|
||||||
|
(pattern (~seq) #:attr [I 1] '()))
|
||||||
|
|
||||||
(define-splicing-syntax-class bindings
|
(define-splicing-syntax-class bindings
|
||||||
(pattern (~seq #:collect [(id init) ...]))
|
(pattern (~seq #:collect [(id init) ...]))
|
||||||
(pattern (~seq) #:attr [id 1] '() #:attr [init 1] '())))
|
(pattern (~seq) #:attr [id 1] '() #:attr [init 1] '())))
|
||||||
|
@ -236,8 +241,8 @@
|
||||||
;; Sugar
|
;; Sugar
|
||||||
(define-syntax (until stx)
|
(define-syntax (until stx)
|
||||||
(syntax-parse stx
|
(syntax-parse stx
|
||||||
[(_ E init:init bs:bindings O ...)
|
[(_ E init:init done:done bs:bindings O ...)
|
||||||
#'(state #:init [init.I ...] [#:collect [(bs.id bs.init) ...] O ...] [E (values)])]))
|
#'(state #:init [init.I ...] [#:collect [(bs.id bs.init) ...] O ...] [E done.I ... (values)])]))
|
||||||
|
|
||||||
;; Sugar
|
;; Sugar
|
||||||
(define-syntax (forever stx)
|
(define-syntax (forever stx)
|
||||||
|
@ -499,7 +504,8 @@
|
||||||
s))))))
|
s))))))
|
||||||
|
|
||||||
(define (analyze-asserted-or-retracted! endpoint-index asserted? outer-expr-stx P-stx I-stxs L-stx)
|
(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-assertion-maintainer! endpoint-index #'sub pat #f L-stx)
|
||||||
(add-event-handler!
|
(add-event-handler!
|
||||||
(lambda (evt-stx)
|
(lambda (evt-stx)
|
||||||
|
@ -527,7 +533,8 @@
|
||||||
#`(at-meta #,(prepend-at-meta-stx stx (- level 1)))))
|
#`(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 (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-assertion-maintainer! endpoint-index #'sub pat #f L-stx)
|
||||||
(add-event-handler!
|
(add-event-handler!
|
||||||
(lambda (evt-stx)
|
(lambda (evt-stx)
|
||||||
|
@ -567,8 +574,17 @@
|
||||||
#,(make-run-script-call E-stx #'s I-stxs)
|
#,(make-run-script-call E-stx #'s I-stxs)
|
||||||
(transition s '())))))))]))
|
(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 (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))
|
(add-assertion-maintainer! index #'core:assert pat Pred-stx L-stx))
|
||||||
|
|
||||||
(define (analyze-tracks! index track-spec-stxs I-stxs)
|
(define (analyze-tracks! index track-spec-stxs I-stxs)
|
||||||
|
@ -589,9 +605,11 @@
|
||||||
(for [(ongoing (in-list (syntax->list ongoings)))
|
(for [(ongoing (in-list (syntax->list ongoings)))
|
||||||
(ongoing-index (in-naturals))]
|
(ongoing-index (in-naturals))]
|
||||||
(syntax-parse ongoing
|
(syntax-parse ongoing
|
||||||
#:literals [on assert track]
|
#:literals [on during assert track]
|
||||||
[(on E I ...)
|
[(on E I ...)
|
||||||
(analyze-event! ongoing-index #'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)
|
[(assert w:when-pred P L:meta-level)
|
||||||
(analyze-assertion! ongoing-index #'w.Pred ongoing #'P #'L.level)]
|
(analyze-assertion! ongoing-index #'w.Pred ongoing #'P #'L.level)]
|
||||||
[(track [track-spec ...] I ...)
|
[(track [track-spec ...] I ...)
|
||||||
|
@ -732,15 +750,15 @@
|
||||||
(and (dollar-id? stx)
|
(and (dollar-id? stx)
|
||||||
(datum->syntax stx (string->symbol (substring (symbol->string (syntax-e stx)) 1)))))
|
(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)
|
(define (analyze-pattern outer-expr-stx pat-stx0)
|
||||||
(let walk ((pat-stx pat-stx0))
|
(let walk ((pat-stx pat-stx0))
|
||||||
(syntax-case pat-stx ($ ? quasiquote unquote quote)
|
(syntax-case pat-stx ($ ? quasiquote unquote quote)
|
||||||
;; Extremely limited support for quasiquoting and quoting
|
;; Extremely limited support for quasiquoting and quoting
|
||||||
[(quasiquote (unquote p)) (walk #'p)]
|
[(quasiquote (unquote p)) (walk #'p)]
|
||||||
[(quasiquote (p ...)) (walk #'(list (quasiquote p) ...))]
|
[(quasiquote (p ...)) (walk #'(list (quasiquote p) ...))]
|
||||||
[(quasiquote p) (values #''p #''p #''p '())]
|
[(quasiquote p) (values #''p #''p #''p '() #''p)]
|
||||||
[(quote p) (values #''p #''p #''p '())]
|
[(quote p) (values #''p #''p #''p '() #''p)]
|
||||||
|
|
||||||
[$v
|
[$v
|
||||||
(dollar-id? #'$v)
|
(dollar-id? #'$v)
|
||||||
|
@ -748,17 +766,19 @@
|
||||||
(values #'(?!)
|
(values #'(?!)
|
||||||
#'?
|
#'?
|
||||||
#'v
|
#'v
|
||||||
(list #'v)))]
|
(list #'v)
|
||||||
|
#'v))]
|
||||||
|
|
||||||
[($ v p)
|
[($ v p)
|
||||||
(let ()
|
(let ()
|
||||||
(define-values (pr g m bs) (walk #'p))
|
(define-values (pr g m bs _ins) (walk #'p))
|
||||||
(when (not (null? bs))
|
(when (not (null? bs))
|
||||||
(raise-syntax-error #f "nested bindings not supported" outer-expr-stx pat-stx))
|
(raise-syntax-error #f "nested bindings not supported" outer-expr-stx pat-stx))
|
||||||
(values #`(?! #,pr)
|
(values #`(?! #,pr)
|
||||||
g
|
g
|
||||||
#`(and v #,m)
|
#`(and v #,m)
|
||||||
(list #'v)))]
|
(list #'v)
|
||||||
|
#'v))]
|
||||||
|
|
||||||
[(? pred? p)
|
[(? pred? p)
|
||||||
;; TODO: support pred? in asserted/retracted as well as message events
|
;; TODO: support pred? in asserted/retracted as well as message events
|
||||||
|
@ -770,31 +790,35 @@
|
||||||
"Predicate '?' matching only supported in message events"
|
"Predicate '?' matching only supported in message events"
|
||||||
outer-expr-stx
|
outer-expr-stx
|
||||||
pat-stx)])
|
pat-stx)])
|
||||||
(define-values (pr g m bs) (walk #'p))
|
(define-values (pr g m bs ins) (walk #'p))
|
||||||
(values pr
|
(values pr
|
||||||
g
|
g
|
||||||
#`(? pred? #,m)
|
#`(? pred? #,m)
|
||||||
bs))]
|
bs
|
||||||
|
ins))]
|
||||||
|
|
||||||
[(ctor p ...)
|
[(ctor p ...)
|
||||||
(let ()
|
(let ()
|
||||||
(define parts (if (identifier? #'ctor) #'(p ...) #'(ctor p ...)))
|
(define parts (if (identifier? #'ctor) #'(p ...) #'(ctor p ...)))
|
||||||
(define-values (pr g m bs)
|
(define-values (pr g m bs ins)
|
||||||
(for/fold [(pr '()) (g '()) (m '()) (bs '())] [(p (syntax->list parts))]
|
(for/fold [(pr '()) (g '()) (m '()) (bs '()) (ins '())] [(p (syntax->list parts))]
|
||||||
(define-values (pr1 g1 m1 bs1) (walk p))
|
(define-values (pr1 g1 m1 bs1 ins1) (walk p))
|
||||||
(values (cons pr1 pr)
|
(values (cons pr1 pr)
|
||||||
(cons g1 g)
|
(cons g1 g)
|
||||||
(cons m1 m)
|
(cons m1 m)
|
||||||
(append bs bs1))))
|
(append bs bs1)
|
||||||
|
(cons ins1 ins))))
|
||||||
(if (identifier? #'ctor)
|
(if (identifier? #'ctor)
|
||||||
(values (cons #'ctor (reverse pr))
|
(values (cons #'ctor (reverse pr))
|
||||||
(cons #'ctor (reverse g))
|
(cons #'ctor (reverse g))
|
||||||
(cons #'ctor (reverse m))
|
(cons #'ctor (reverse m))
|
||||||
bs)
|
bs
|
||||||
|
(cons #'ctor (reverse ins)))
|
||||||
(values (reverse pr)
|
(values (reverse pr)
|
||||||
(reverse g)
|
(reverse g)
|
||||||
(reverse m)
|
(reverse m)
|
||||||
bs)))]
|
bs
|
||||||
|
(reverse ins))))]
|
||||||
|
|
||||||
[?
|
[?
|
||||||
(raise-syntax-error #f
|
(raise-syntax-error #f
|
||||||
|
@ -808,11 +832,13 @@
|
||||||
(values #'?
|
(values #'?
|
||||||
#'?
|
#'?
|
||||||
#'_
|
#'_
|
||||||
'())
|
'()
|
||||||
|
#'_)
|
||||||
(values #'non-pair
|
(values #'non-pair
|
||||||
#'non-pair
|
#'non-pair
|
||||||
#'(== non-pair)
|
#'(== non-pair)
|
||||||
'()))])))
|
'()
|
||||||
|
#'non-pair))])))
|
||||||
|
|
||||||
)
|
)
|
||||||
|
|
||||||
|
@ -855,11 +881,12 @@
|
||||||
|
|
||||||
(begin-for-syntax
|
(begin-for-syntax
|
||||||
(define (analyze-and-print pat-stx)
|
(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))
|
(pretty-print `((pr ,(map syntax->datum pr))
|
||||||
(g ,(map syntax->datum g))
|
(g ,(map syntax->datum g))
|
||||||
(m ,(map syntax->datum m))
|
(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)))
|
#;(analyze-and-print #'`(hello ,$who)))
|
||||||
|
|
||||||
|
@ -867,6 +894,11 @@
|
||||||
#'(actor
|
#'(actor
|
||||||
(until (rising-edge (= count 10))
|
(until (rising-edge (= count 10))
|
||||||
#:collect [(count 0)]
|
#: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))
|
(on (message `(hello ,$who))
|
||||||
(println "Got hello: ~a" who)
|
(println "Got hello: ~a" who)
|
||||||
(+ count 1))))))
|
(+ count 1))))))
|
||||||
|
|
|
@ -17,7 +17,7 @@
|
||||||
; (SyntaxOf TempVar TempVar Projection-Pattern Match-Pattern)
|
; (SyntaxOf TempVar TempVar Projection-Pattern Match-Pattern)
|
||||||
(define (helper pat-stx outer-stx)
|
(define (helper pat-stx outer-stx)
|
||||||
(match-define (list temp1 temp2) (generate-temporaries #'(tmp1 tmp2)))
|
(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))
|
(analyze-pattern outer-stx pat-stx))
|
||||||
(list temp1 temp2 proj-stx bindings)))
|
(list temp1 temp2 proj-stx bindings)))
|
||||||
|
|
||||||
|
|
|
@ -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)))))
|
Loading…
Reference in New Issue