From 632e36f751ea454874548cdb62d6cb73694c773d Mon Sep 17 00:00:00 2001
From: Vincent St-Amour <stamourv@racket-lang.org>
Date: Thu, 28 Apr 2011 18:21:21 -0400
Subject: [PATCH] Add set types to TR.

Original patch by Eric Dobson.
---
 collects/tests/typed-scheme/succeed/set.rkt   | 40 +++++++++++++++++++
 collects/typed-scheme/infer/infer-unit.rkt    |  2 +
 collects/typed-scheme/private/base-env.rkt    | 20 ++++++++++
 collects/typed-scheme/private/base-types.rkt  |  1 +
 collects/typed-scheme/rep/type-rep.rkt        |  4 ++
 .../scribblings/ts-reference.scrbl            |  4 ++
 collects/typed-scheme/types/abbrev.rkt        |  1 +
 collects/typed-scheme/types/printer.rkt       |  1 +
 collects/typed-scheme/types/subtype.rkt       |  1 +
 9 files changed, 74 insertions(+)
 create mode 100644 collects/tests/typed-scheme/succeed/set.rkt

diff --git a/collects/tests/typed-scheme/succeed/set.rkt b/collects/tests/typed-scheme/succeed/set.rkt
new file mode 100644
index 0000000000..de9d5cb179
--- /dev/null
+++ b/collects/tests/typed-scheme/succeed/set.rkt
@@ -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)
diff --git a/collects/typed-scheme/infer/infer-unit.rkt b/collects/typed-scheme/infer/infer-unit.rkt
index 51c3ce685f..c58d490bed 100644
--- a/collects/typed-scheme/infer/infer-unit.rkt
+++ b/collects/typed-scheme/infer/infer-unit.rkt
@@ -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
diff --git a/collects/typed-scheme/private/base-env.rkt b/collects/typed-scheme/private/base-env.rkt
index 05313abf6d..24b2bf2c13 100644
--- a/collects/typed-scheme/private/base-env.rkt
+++ b/collects/typed-scheme/private/base-env.rkt
@@ -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]
diff --git a/collects/typed-scheme/private/base-types.rkt b/collects/typed-scheme/private/base-types.rkt
index 6f81bf6698..1f63fe699b 100644
--- a/collects/typed-scheme/private/base-types.rkt
+++ b/collects/typed-scheme/private/base-types.rkt
@@ -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)]
diff --git a/collects/typed-scheme/rep/type-rep.rkt b/collects/typed-scheme/rep/type-rep.rkt
index 2c013717f5..1c70bb5fd2 100644
--- a/collects/typed-scheme/rep/type-rep.rkt
+++ b/collects/typed-scheme/rep/type-rep.rkt
@@ -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
diff --git a/collects/typed-scheme/scribblings/ts-reference.scrbl b/collects/typed-scheme/scribblings/ts-reference.scrbl
index 759d4a281f..06248aca7d 100644
--- a/collects/typed-scheme/scribblings/ts-reference.scrbl
+++ b/collects/typed-scheme/scribblings/ts-reference.scrbl
@@ -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))
diff --git a/collects/typed-scheme/types/abbrev.rkt b/collects/typed-scheme/types/abbrev.rkt
index 397f56c471..460818bef4 100644
--- a/collects/typed-scheme/types/abbrev.rkt
+++ b/collects/typed-scheme/types/abbrev.rkt
@@ -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))
diff --git a/collects/typed-scheme/types/printer.rkt b/collects/typed-scheme/types/printer.rkt
index 29995c352c..8509d0cac8 100644
--- a/collects/typed-scheme/types/printer.rkt
+++ b/collects/typed-scheme/types/printer.rkt
@@ -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) 
diff --git a/collects/typed-scheme/types/subtype.rkt b/collects/typed-scheme/types/subtype.rkt
index 199b268a4b..548a6bf8c8 100644
--- a/collects/typed-scheme/types/subtype.rkt
+++ b/collects/typed-scheme/types/subtype.rkt
@@ -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]