From 6c888143e7d7ece726d76a0322aa2ee36eb19f64 Mon Sep 17 00:00:00 2001 From: Asumu Takikawa Date: Tue, 2 Jul 2013 18:34:52 -0400 Subject: [PATCH] Add support for synchronizable events --- .../scribblings/reference/types.scrbl | 7 ++ .../typed-racket/base-env/base-env.rkt | 38 ++++++- .../typed-racket/base-env/base-types.rkt | 1 + .../typed-racket/infer/infer-unit.rkt | 23 ++++ .../typed-racket/rep/type-rep.rkt | 4 + .../typed-racket/types/abbrev.rkt | 3 - .../typed-racket/types/base-abbrev.rkt | 5 + .../typed-racket/types/printer.rkt | 1 + .../typed-racket/types/subtype.rkt | 27 +++++ .../tests/typed-racket/succeed/events.rkt | 105 ++++++++++++++++++ .../succeed/type-printer-single-level.rkt | 10 +- .../typed-racket/unit-tests/subtype-tests.rkt | 26 +++++ .../unit-tests/typecheck-tests.rkt | 29 +++++ 13 files changed, 269 insertions(+), 10 deletions(-) create mode 100644 pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/events.rkt diff --git a/pkgs/typed-racket-pkgs/typed-racket-doc/typed-racket/scribblings/reference/types.scrbl b/pkgs/typed-racket-pkgs/typed-racket-doc/typed-racket/scribblings/reference/types.scrbl index 46691cd12f..cda8a5cfdd 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-doc/typed-racket/scribblings/reference/types.scrbl +++ b/pkgs/typed-racket-pkgs/typed-racket-doc/typed-racket/scribblings/reference/types.scrbl @@ -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} diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-env.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-env.rkt index b52eb4e93e..e4c6125861 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-env.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-env.rkt @@ -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))] diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-types.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-types.rkt index bbfc1e5e0e..78aa28852b 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-types.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-types.rkt @@ -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)] diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt index e00ef760e5..d0ac728035 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt @@ -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 diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/rep/type-rep.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/rep/type-rep.rkt index c292e04b51..83fce5f5fe 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/rep/type-rep.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/rep/type-rep.rkt @@ -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 diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/abbrev.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/abbrev.rkt index e80af5644f..3cc295084f 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/abbrev.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/abbrev.rkt @@ -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?)) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/base-abbrev.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/base-abbrev.rkt index b82d5eb8da..b45a4d0eab 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/base-abbrev.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/base-abbrev.rkt @@ -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)) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/printer.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/printer.rkt index 0f7f438ebc..15fdbe5a07 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/printer.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/printer.rkt @@ -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) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/subtype.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/subtype.rkt index 32c9cfb941..365248f08f 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/subtype.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/subtype.rkt @@ -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] diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/events.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/events.rkt new file mode 100644 index 0000000000..8366162748 --- /dev/null +++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/events.rkt @@ -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)))) + diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/type-printer-single-level.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/type-printer-single-level.rkt index 70988225e8..49a86494f7 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/type-printer-single-level.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/type-printer-single-level.rkt @@ -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")) + "Positive-Integer-Not-Fixnum Negative-Integer-Not-Fixnum" + "))\n")) diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/subtype-tests.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/subtype-tests.rkt index ad6ef3a7ad..e8087298a2 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/subtype-tests.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/subtype-tests.rkt @@ -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)] diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt index 5a584a93e6..eca4edbb18 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt @@ -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)))