suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Add support for synchronizable events

Browse Source
This commit is contained in:
Asumu Takikawa 2013-07-02 18:34:52 -04:00
parent 71ec424c70
commit 6c888143e7
13 changed files with 269 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
pkgs/typed-racket-pkgs/typed-racket-doc/typed-racket/scribblings/reference/types.scrbl
View File

@ -364,6 +364,13 @@ type @racket[_t] on each iteration.}
@defform[(Ephemeronof t)]{An @rtech{ephemeron} whose value is of type @racket[t].}
@defform[(Evtof t)]{A @rtech{synchronizable event} whose @rtech{synchronization result}
is of type @racket[t].
@ex[always-evt
(system-idle-evt)
(ann (thread (λ () (displayln "hello world"))) (Evtof Thread))]
}
@section{Syntax Objects}

38
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-env.rkt
View File

@ -35,6 +35,7 @@
make-ThreadCellTop
make-Ephemeron
make-CustodianBox
make-Evt
make-HeterogeneousVector
make-Continuation-Mark-Keyof
make-Continuation-Mark-KeyTop
@ -285,6 +286,41 @@
[empty? (make-pred-ty (-val null))]
[empty (-val null)]
;; Section 10.2.1
[evt? (make-pred-ty (make-Evt Univ))]
[sync (-poly (a) (->* '() (make-Evt a) a))]
[sync/timeout
(-poly (a b)
(cl->*
(->* (list (-val #f)) (make-Evt a) a)
(->* (list -NonNegReal) (make-Evt a) (-opt a))
(->* (list (-> b)) (make-Evt a) (Un a b))))]
[sync/enable-break (-poly (a) (->* '() (make-Evt a) a))]
[sync/timeout/enable-break
(-poly (a b)
(cl->*
(->* (list (-val #f)) (make-Evt a) a)
(->* (list -NonNegReal) (make-Evt a) (-opt a))
(->* (list (-> b)) (make-Evt a) (Un a b))))]
[choice-evt (-poly (a) (->* '() (make-Evt a) (make-Evt a)))]
[wrap-evt (-poly (a b) (-> (make-Evt a) (-> a b) (make-Evt b)))]
[handle-evt (-poly (a b) (-> (make-Evt a) (-> a b) (make-Evt b)))]
[guard-evt (-poly (a) (-> (-> (make-Evt a)) (make-Evt a)))]
[nack-guard-evt
(-poly (a)
(-> (-> (make-Evt -Void) (make-Evt a))
(make-Evt a)))]
[poll-guard-evt
(-poly (a) (-> (-> -Boolean (make-Evt a)) (make-Evt a)))]
[always-evt (-mu x (make-Evt x))]
[never-evt (make-Evt (Un))]
[system-idle-evt (-> (make-Evt -Void))]
[alarm-evt (-> -NonNegReal (-mu x (make-Evt x)))]
[handle-evt? (make-pred-ty (make-Evt Univ))]
[current-evt-pseudo-random-generator
(-Param -Pseudo-Random-Generator -Pseudo-Random-Generator)]
;; Section 10.2.2
[make-channel (-poly (a) (-> (-channel a)))]
[channel? (make-pred-ty (make-ChannelTop))]
[channel-get (-poly (a) ((-channel a) . -> . a))]
@ -2182,8 +2218,6 @@
[vector->pseudo-random-generator!
(-> -Pseudo-Random-Generator (make-HeterogeneousVector (list -PosInt -PosInt -PosInt -PosInt -PosInt -PosInt)) -Void)]
[current-evt-pseudo-random-generator (-Param -Pseudo-Random-Generator -Pseudo-Random-Generator)]
;Section 9.6
[break-enabled (cl->* (-> B) (-> B -Void))]

1
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-types.rkt
View File

@ -152,6 +152,7 @@
[Channelof (-poly (a) (make-Channel a))]
[Ephemeronof (-poly (a) (make-Ephemeron a))]
[Setof (-poly (e) (make-Set e))]
[Evtof (-poly (r) (make-Evt r))]
[Continuation-Mark-Set -Cont-Mark-Set]
[False (-val #f)]
[True (-val #t)]

23
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt
View File

@ -607,6 +607,29 @@
(cg e e*)]
[((Set: a) (Set: a*))
(cg a a*)]
[((Evt: a) (Evt: a*))
(cg a a*)]
[((Base: 'Semaphore _ _ _ _) (Evt: t))
(cg S t)]
[((Base: 'Output-Port _ _ _ _) (Evt: t))
(cg S t)]
[((Base: 'Input-Port _ _ _ _) (Evt: t))
(cg S t)]
[((Base: 'TCP-Listener _ _ _ _) (Evt: t))
(cg S t)]
[((Base: 'Thread _ _ _ _) (Evt: t))
(cg S t)]
[((Base: 'Subprocess _ _ _ _) (Evt: t))
(cg S t)]
[((Base: 'Will-Executor _ _ _ _) (Evt: t))
(cg S t)]
[((Base: 'LogReceiver _ _ _ _) (Evt: t ))
(cg (make-HeterogeneousVector
(list -Symbol -String Univ
(Un (-val #f) -Symbol)))
t)]
[((CustodianBox: t) (Evt: t*)) (cg S t*)]
[((Channel: t) (Evt: t*)) (cg t t*)]
;; we assume all HTs are mutable at the moment
[((Hashtable: s1 s2) (Hashtable: t1 t2))
;; for mutable hash tables, both are invariant

4
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/rep/type-rep.rkt
View File

@ -182,6 +182,10 @@
(def-type Set ([elem Type/c])
[#:key 'set])
;; elem is a Type
(def-type Evt ([result Type/c])
[#:key #f])
;; name is a Symbol (not a Name)
;; contract is used when generating contracts from types
;; predicate is used to check (at compile-time) whether a value belongs

3
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/abbrev.rkt
View File

@ -87,15 +87,12 @@
(define -Listof (-poly (list-elem) (make-Listof list-elem)))
(define -Boolean (Un (-val #t) (-val #f)))
(define -Symbol (make-Base 'Symbol #'symbol? symbol? #'-Symbol))
(define -Undefined
(make-Base 'Undefined
#'(lambda (x) (equal? (letrec ([y y]) y) x)) ; initial value of letrec bindings
(lambda (x) (equal? (letrec ([y y]) y) x))
#'-Undefined))
(define -Bytes (make-Base 'Bytes #'bytes? bytes? #'-Bytes))
(define -String (make-Base 'String #'string? string? #'-String))
(define -Base-Regexp (make-Base 'Base-Regexp
#'(and/c regexp? (not/c pregexp?))

5
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/base-abbrev.rkt
View File

@ -29,6 +29,11 @@
(define -Char (make-Base 'Char #'char? char? #'-Char #f))
(define (make-Listof elem) (-mu list-rec (simple-Un (-val null) (make-Pair elem list-rec))))
(define (make-MListof elem) (-mu list-rec (simple-Un (-val null) (make-MPair elem list-rec))))
;; Needed for evt checking in subtype.rkt
(define -Symbol (make-Base 'Symbol #'symbol? symbol? #'-Symbol #f))
(define -String (make-Base 'String #'string? string? #'-String #f))
;; Void is needed for Params
(define -Void (make-Base 'Void #'void? void? #'-Void #f))

1
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/printer.rkt
View File

@ -325,6 +325,7 @@
[(Ephemeron: e) (fp "(Ephemeronof ~a)" e)]
[(CustodianBox: e) (fp "(CustodianBoxof ~a)" e)]
[(Set: e) (fp "(Setof ~a)" e)]
[(Evt: r) (fp "(Evtof ~a)" r)]
[(Union: elems) (fp "~a" (cons 'U (print-union type ignored-names)))]
[(Pair: l r) (fp "(Pairof ~a ~a)" l r)]
[(ListDots: dty dbound)

27
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/subtype.rkt
View File

@ -476,6 +476,33 @@
[((CustodianBox: s) (CustodianBox: t))
(subtype* A0 s t)]
[((Set: t) (Set: t*)) (subtype* A0 t t*)]
;; Evts are covariant
[((Evt: t) (Evt: t*)) (subtype* A0 t t*)]
[((Base: 'Semaphore _ _ _ _) (Evt: t))
(subtype* A0 s t)]
[((Base: 'Output-Port _ _ _ _) (Evt: t))
(subtype* A0 s t)]
[((Base: 'Input-Port _ _ _ _) (Evt: t))
(subtype* A0 s t)]
[((Base: 'TCP-Listener _ _ _ _) (Evt: t))
(subtype* A0 s t)]
[((Base: 'Thread _ _ _ _) (Evt: t))
(subtype* A0 s t)]
[((Base: 'Subprocess _ _ _ _) (Evt: t))
(subtype* A0 s t)]
[((Base: 'Will-Executor _ _ _ _) (Evt: t))
(subtype* A0 s t)]
[((Base: 'LogReceiver _ _ _ _) (Evt: t))
(subtype* A0
(make-HeterogeneousVector
(list -Symbol -String Univ
(Un (-val #f) -Symbol)))
t)]
[((CustodianBox: t) (Evt: t*))
;; Note that it's the whole box type that's being
;; compared against t* here
(subtype* A0 s t*)]
[((Channel: t) (Evt: t*)) (subtype* A0 t t*)]
;; Invariant types
[((Box: s) (Box: t)) (type-equiv? A0 s t)]
[((Box: _) (BoxTop:)) A0]

105
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/events.rkt Normal file
View File

@ -0,0 +1,105 @@
#lang typed/racket
;; Integration test for synchronizable events
;;
;; example from unstable/logging
(define-type Log-Receiver-Sync-Result
(Vector Symbol String Any (Option Symbol)))
(: receiver-thread
(Log-Receiver (Channelof 'stop)
(Log-Receiver-Sync-Result -> Void)
-> Thread))
(define (receiver-thread receiver stop-chan intercept)
(thread
(lambda ()
(: clear-events (-> Void))
(define (clear-events)
(let: ([l : (Option Log-Receiver-Sync-Result)
(sync/timeout 0 receiver)])
(when l ; still something to read
(intercept l) ; interceptor gets the whole vector
(clear-events))))
(let loop ()
(let: ([l : (U Log-Receiver-Sync-Result 'stop)
(sync receiver stop-chan)])
(cond [(eq? l 'stop)
;; we received all the events we were supposed
;; to get, read them all (w/o waiting), then
;; stop
(clear-events)]
[else ; keep going
(intercept l)
(loop)]))))))
(struct: listener ([stop-chan : (Channelof 'stop)]
;; ugly, but the thread and the listener need to know each
;; other
[thread : (Option Thread)]
[rev-messages : (Listof Log-Receiver-Sync-Result)]
[done? : Any])
#:mutable)
(: start-recording (Log-Level -> listener))
(define (start-recording log-level)
(let* ([receiver (make-log-receiver (current-logger) log-level)]
[stop-chan ((inst make-channel 'stop))]
[cur-listener (listener stop-chan #f '() #f)]
[t (receiver-thread
receiver stop-chan
(lambda: ([l : Log-Receiver-Sync-Result])
(set-listener-rev-messages!
cur-listener
(cons l (listener-rev-messages cur-listener)))))])
(set-listener-thread! cur-listener t)
cur-listener))
(: stop-recording (listener -> (Listof Log-Receiver-Sync-Result)))
(define (stop-recording cur-listener)
(define the-thread (listener-thread cur-listener))
(unless (or (not the-thread)
(listener-done? cur-listener))
(channel-put (listener-stop-chan cur-listener)
'stop) ; stop the receiver thread
(thread-wait the-thread)
(set-listener-done?! cur-listener #t))
(reverse (listener-rev-messages cur-listener)))
(: with-intercepted-logging
(((Vector Symbol String Any (Option Symbol)) -> Void)
(-> Void)
Log-Level
-> Void))
(define (with-intercepted-logging interceptor proc log-level)
(let* ([orig-logger (current-logger)]
;; We use a local logger to avoid getting messages that didn't
;; originate from proc. Since it's a child of the original logger,
;; the rest of the program still sees the log entries.
[logger (make-logger #f orig-logger)]
[receiver (make-log-receiver logger log-level)]
[stop-chan ((inst make-channel 'stop))]
[t (receiver-thread receiver stop-chan interceptor)])
(begin0
(parameterize ([current-logger logger])
(proc))
(channel-put stop-chan 'stop) ; stop the receiver thread
(thread-wait t))))
(require typed/rackunit)
;; extracted from unstable/logging tests
(let ([l (start-recording 'warning)])
(log-warning "1")
(log-warning "2")
(log-warning "3")
(log-info "4")
(stop-recording l) ; stopping should be idempotent
(let ([out (stop-recording l)])
(check-equal? (map (lambda: ([l : Log-Receiver-Sync-Result])
(vector-ref l 1)) out)
'("1" "2" "3"))
(check-true (andmap (lambda: ([l : Log-Receiver-Sync-Result])
(eq? (vector-ref l 0) 'warning))
out))))

8
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/type-printer-single-level.rkt
View File

@ -28,11 +28,11 @@
(string-append "(U Integer String)\n[can expand further: String Integer]"
"(Foo -> Foo)\n[can expand further: Foo]"
"(Number -> Integer)\n[can expand further: Integer Number]"
"((U 0 1 Byte-Larger-Than-One Positive-Index-Not-Byte "
"((U String 0 1 Byte-Larger-Than-One Positive-Index-Not-Byte "
"Positive-Fixnum-Not-Index Negative-Fixnum "
"Positive-Integer-Not-Fixnum Negative-Integer-Not-Fixnum String) "
"-> (U 0 1 Byte-Larger-Than-One Positive-Index-Not-Byte "
"Positive-Integer-Not-Fixnum Negative-Integer-Not-Fixnum) "
"-> (U String 0 1 Byte-Larger-Than-One Positive-Index-Not-Byte "
"Positive-Fixnum-Not-Index Negative-Fixnum "
"Positive-Integer-Not-Fixnum Negative-Integer-Not-Fixnum"
"String))\n"))
"))\n"))

26
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/subtype-tests.rkt
View File

@ -176,6 +176,32 @@
[(make-Prompt-Tagof t1 t2) (make-Prompt-Tagof t2 t1)]
[(make-Continuation-Mark-Keyof t1) (make-Continuation-Mark-Keyof t2)]
;; evts
[(make-Evt t1) (make-Evt t2)]
[FAIL (make-Evt -Byte) (make-Evt -String)]
[-Semaphore (make-Evt -Semaphore)]
[FAIL -Semaphore (make-Evt -Int)]
[-Output-Port (make-Evt -Output-Port)]
[FAIL -Output-Port (make-Evt -Int)]
[-Input-Port (make-Evt -Input-Port)]
[FAIL -Input-Port (make-Evt -Int)]
[-TCP-Listener (make-Evt -TCP-Listener)]
[FAIL -TCP-Listener (make-Evt -Int)]
[-Thread (make-Evt -Thread)]
[FAIL -Thread (make-Evt -Int)]
[-Subprocess (make-Evt -Subprocess)]
[FAIL -Subprocess (make-Evt -Int)]
[-Will-Executor (make-Evt -Will-Executor)]
[FAIL -Will-Executor (make-Evt -Int)]
[(make-CustodianBox -String) (make-Evt (make-CustodianBox -String))]
[FAIL (make-CustodianBox -String) (make-Evt -String)]
[(-channel -String) (make-Evt -String)]
[FAIL (-channel -String) (make-Evt -Int)]
[-Log-Receiver (make-Evt (make-HeterogeneousVector
(list -Symbol -String Univ
(Un (-val #f) -Symbol))))]
[FAIL -Log-Receiver (make-Evt -Int)]
[(-val 5) (-seq -Nat)]
[(-val 5) (-seq -Byte)]
[-Index (-seq -Index)]

29
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt
View File

@ -1436,6 +1436,35 @@
(let: ((lr : Log-Receiver (make-log-receiver l 'error)))
(log-message l 'error "Message" 'value))) -Void)
;Events
(tc-e (sync (make-semaphore)) -Semaphore)
(tc-e (sync (tcp-listen 5555)) -TCP-Listener)
(tc-e (sync (tcp-listen 5555) (make-semaphore))
(make-Union (list -TCP-Listener -Semaphore)))
(tc-e (sync (thread (λ () 0))) -Thread)
(tc-e (sync (make-will-executor)) -Will-Executor)
(tc-e (sync (make-custodian-box (current-custodian) 0))
(make-CustodianBox (-val 0)))
(tc-e (sync ((inst make-channel String))) -String)
(tc-e (sync always-evt) (-mu x (make-Evt x)))
(tc-e (sync never-evt) -Bottom)
(tc-e (sync never-evt always-evt) (-mu x (make-Evt x)))
(tc-e (sync (system-idle-evt)) -Void)
(tc-e (sync (choice-evt (system-idle-evt))) -Void)
(tc-e (sync (choice-evt (system-idle-evt)
((inst make-channel String))))
(make-Union (list -String -Void)))
(tc-e (sync/timeout 100 (make-semaphore) (tcp-listen 5555))
(make-Union (list (-val #f) -TCP-Listener -Semaphore)))
(tc-e (handle-evt ((inst make-channel Number))
(λ: ([x : Number]) (number->string x)))
(make-Evt -String))
(tc-e (wrap-evt ((inst make-channel Number))
(λ: ([x : Number]) (number->string x)))
(make-Evt -String))
(tc-e (guard-evt (inst make-channel String))
(make-Evt -String))
;Semaphores
(tc-e (make-semaphore) -Semaphore)
(tc-e (let: ((s : Semaphore (make-semaphore 3)))