Add set types to TR.

Original patch by Eric Dobson.
This commit is contained in:
Vincent St-Amour 2011-04-28 18:21:21 -04:00
parent d2a21d717c
commit 632e36f751
9 changed files with 74 additions and 0 deletions

View File

@ -0,0 +1,40 @@
#lang typed/racket
(define s (set 0 1 2 3))
(define q (seteq 0 1 2 3))
(define v (seteqv 0 1 2 3))
(define s0 (ann (set) (Setof Byte)))
(set-empty? s)
(set-empty? q)
(set-empty? v)
(set-empty? s0)
(set-count s)
(set-count q)
(set-count v)
(set-count s0)
(set-member? s 0)
(set-member? q 0)
(set-member? v 0)
(set-member? s0 0)
(set-add s 4)
(set-add q 4)
(set-add v 4)
(set-add s0 4)
(set-remove s 4)
(set-remove q 4)
(set-remove v 4)
(set-remove s0 4)
(subset? s s0)
(set-map v add1)
(set-for-each s0 display)
(set-equal? s)
(set-eqv? v)
(set-eq? q)
(set? s0)

View File

@ -497,6 +497,8 @@
(cset-meet (cg e e*) (cg e* e))]
[((Ephemeron: e) (Ephemeron: e*))
(cg e e*)]
[((Set: a) (Set: a*))
(cg a a*)]
;; we assume all HTs are mutable at the moment
[((Hashtable: s1 s2) (Hashtable: t1 t2))
;; for mutable hash tables, both are invariant

View File

@ -18,6 +18,7 @@
racket/function
racket/mpair
racket/base
racket/set
(only-in string-constants/private/only-once maybe-print-message)
(only-in mzscheme make-namespace)
(only-in racket/match/runtime match:error matchable? match-equality-test))
@ -599,6 +600,25 @@
[hash-iterate-value (-poly (a b)
((-HT a b) -Integer . -> . b))]
;Set operations
[set (-poly (e) (->* (list) e (-set e)))]
[seteqv (-poly (e) (->* (list) e (-set e)))]
[seteq (-poly (e) (->* (list) e (-set e)))]
[set-empty? (-poly (e) (-> (-set e) B))]
[set-count (-poly (e) (-> (-set e) -Index))]
[set-member? (-poly (e) (-> (-set e) e B))]
[set-add (-poly (e) (-> (-set e) e (-set e)))]
[set-remove (-poly (e) (-> (-set e) e (-set e)))]
[subset? (-poly (e) (-> (-set e) (-set e) B))]
[set-map (-poly (e b) (-> (-set e) (-> e b) (-lst b)))]
[set-for-each (-poly (e b) (-> (-set e) (-> e b) -Void))]
[set? (make-pred-ty (-poly (e) (-set e)))]
[set-equal? (-poly (e) (-> (-set e) B))]
[set-eqv? (-poly (e) (-> (-set e) B))]
[set-eq? (-poly (e) (-> (-set e) B))]
[bytes (->* (list) -Integer -Bytes)]
[bytes? (make-pred-ty -Bytes)]
[make-bytes (cl-> [(-Integer -Integer) -Bytes]

View File

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

View File

@ -135,6 +135,10 @@
[#:key 'ephemeron])
;; elem is a Type
(dt Set ([elem Type/c]) [#:key 'set])
;; 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

View File

@ -163,6 +163,10 @@ corresponding to @racket[trest], where @racket[bound]
@ex[#hash((a . 1) (b . 2))]
}
@defform[(Setof t)]{is the type of a @rtech{set} of @racket[t].
@ex[(set 0 1 2 3)]
}
@defform[(Channelof t)]{A @rtech{channel} on which only @racket[t]s can be sent.
@ex[
(ann (make-channel) (Channelof Symbol))

View File

@ -29,6 +29,7 @@
(define -Param make-Param)
(define -box make-Box)
(define -channel make-Channel)
(define -set make-Set)
(define -vec make-Vector)
(define -future make-Future)
(define (-seq . args) (make-Sequence args))

View File

@ -172,6 +172,7 @@
[(Future: e) (fp "(Futureof ~a)" e)]
[(Channel: e) (fp "(Channelof ~a)" e)]
[(Ephemeron: e) (fp "(Ephemeronof ~a)" e)]
[(Set: e) (fp "(Setof ~a)" e)]
[(Union: elems) (fp "~a" (cons 'U elems))]
[(Pair: l r) (fp "(Pairof ~a ~a)" l r)]
[(ListDots: dty dbound)

View File

@ -361,6 +361,7 @@
[((Ephemeron: s) (Ephemeron: t))
(subtype* A0 s t)]
[((Box: _) (BoxTop:)) A0]
[((Set: t) (Set: t*)) (subtype* A0 t t*)]
[((Channel: _) (ChannelTop:)) A0]
[((Vector: _) (VectorTop:)) A0]
[((HeterogenousVector: _) (VectorTop:)) A0]