From 632c04139b5fe3b37650e32bcc5c6ef5add09949 Mon Sep 17 00:00:00 2001
From: Sam Caldwell <samcaldwell@utexas.edu>
Date: Wed, 1 Aug 2018 10:52:56 -0400
Subject: [PATCH] sets

---
 racket/typed/roles.rkt | 128 +++++++++++++++++++++++++++++++++++------
 1 file changed, 112 insertions(+), 16 deletions(-)

diff --git a/racket/typed/roles.rkt b/racket/typed/roles.rkt
index 5d2722a..3ebde04 100644
--- a/racket/typed/roles.rkt
+++ b/racket/typed/roles.rkt
@@ -26,6 +26,9 @@
          + - * / and or not > < >= <= = equal? displayln printf
          ;; lists
          list first rest member? empty? for for/fold
+         ;; sets
+         Set set set-member? set-add set-count set-union set-subtract set-intersect
+         list->set set->list
          ;; DEBUG and utilities
          print-type print-role
          ;; Extensions
@@ -103,6 +106,24 @@
 
 (define-type-constructor U* #:arity >= 0)
 
+;; τ.norm in 1st case causes "not valid type" error when referring to ⊥ in another file.
+;; however, this version expands the type at every reference, incurring a potentially large
+;; overhead---2x in the case of book-club.rkt
+;; (copied from ext-stlc example)
+(define-syntax define-type-alias
+  (syntax-parser
+    [(_ alias:id τ)
+     #'(define-syntax- alias
+         (make-variable-like-transformer #'τ))]
+    [(_ (f:id x:id ...) ty)
+     #'(define-syntax- (f stx)
+         (syntax-parse stx
+           [(_ x ...)
+            #:with τ:any-type #'ty
+            #'τ.norm]))]))
+
+(define-type-alias ⊥ (U*))
+
 (define-for-syntax (prune+sort tys)
   (stx-sort 
    (filter-maximal 
@@ -139,22 +160,6 @@
 ;; User Defined Types, aka Constructors
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-;; τ.norm in 1st case causes "not valid type" error when referring to ⊥ in another file.
-;; however, this version expands the type at every reference, incurring a potentially large
-;; overhead---2x in the case of book-club.rkt
-;; (copied from ext-stlc example)
-(define-syntax define-type-alias
-  (syntax-parser
-    [(_ alias:id τ)
-     #'(define-syntax- alias
-         (make-variable-like-transformer #'τ))]
-    [(_ (f:id x:id ...) ty)
-     #'(define-syntax- (f stx)
-         (syntax-parse stx
-           [(_ x ...)
-            #:with τ:any-type #'ty
-            #'τ.norm]))]))
-
 (begin-for-syntax
   (define-splicing-syntax-class type-constructor-decl
     (pattern (~seq #:type-constructor TypeCons:id))
@@ -1258,6 +1263,97 @@
 (define- (member?- v l)
   (and- (member- v l) #t))
 
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Sets
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(define-typed-syntax (set e ...) ≫
+  [⊢ e ≫ e- ⇒ τ] ...
+  #:fail-unless (all-pure? #'(e- ...)) "expressions must be pure"
+  ---------------
+  [⊢ (set- e- ...) ⇒ (Set (U τ ...))])
+
+(define-typed-syntax (set-count e) ≫
+  [⊢ e ≫ e- ⇒ (~Set _)]
+  #:fail-unless (pure? #'e-) "expression must be pure"
+  ----------------------
+  [⊢ (set-count- e-) ⇒ Int])
+
+(define-typed-syntax (set-add st v) ≫
+  [⊢ st ≫ st- ⇒ (~Set τs)]
+  #:fail-unless (pure? #'st-) "expression must be pure"
+  [⊢ v ≫ v- ⇒ τv]
+  #:fail-unless (pure? #'v-) "expression must be pure"
+  -------------------------
+  [⊢ (set-add- st- v-) ⇒ (Set (U τs τv))])
+
+(define-typed-syntax (set-member? st v) ≫
+  [⊢ st ≫ st- ⇒ (~Set τs)]
+  #:fail-unless (pure? #'st-) "expression must be pure"
+  [⊢ v ≫ v- ⇒ τv]
+  #:fail-unless (pure? #'v-) "expression must be pure"
+  #:fail-unless (<: #'τv #'τs)
+    "type mismatch"
+  -------------------------------------
+  [⊢ (set-member?- st- v-) ⇒ Bool])
+
+(define-typed-syntax (set-union st0 st ...) ≫
+  [⊢ st0 ≫ st0- ⇒ (~Set τ-st0)]
+  #:fail-unless (pure? #'st0-) "expression must be pure"
+  [⊢ st ≫ st- ⇒ (~Set τ-st)] ...
+  #:fail-unless (all-pure? #'(st- ...)) "expressions must be pure"
+  -------------------------------------
+  [⊢ (set-union- st0- st- ...) ⇒ (Set (U τ-st0 τ-st ...))])
+
+(define-typed-syntax (set-intersect st0 st ...) ≫
+  [⊢ st0 ≫ st0- ⇒ (~Set τ-st0)]
+  #:fail-unless (pure? #'st0-) "expression must be pure"
+  [⊢ st ≫ st- ⇒ (~Set τ-st)] ...
+  #:fail-unless (all-pure? #'(st- ...)) "expressions must be pure"
+  #:with τr (∩ #'τ-st0 (type-eval #'(U τ-st ...)))
+  -------------------------------------
+  [⊢ (set-intersect- st0- st- ...) ⇒ (Set τr)])
+
+(define-typed-syntax (set-subtract st0 st ...) ≫
+  [⊢ st0 ≫ st0- ⇒ (~Set τ-st0)]
+  #:fail-unless (pure? #'st0-) "expression must be pure"
+  [⊢ st ≫ st- ⇒ (~Set _)] ...
+  #:fail-unless (all-pure? #'(st- ...)) "expressions must be pure"
+  -------------------------------------
+  [⊢ (set-subtract- st0- st- ...) ⇒ (Set τ-st0)])
+
+(define-typed-syntax (list->set l) ≫
+  [⊢ l ≫ l- ⇒ (~List τ)]
+  #:fail-unless (pure? #'l-) "expression must be pure"
+  -----------------------
+  [⊢ (list->set- l-) ⇒ (Set τ)])
+
+(define-typed-syntax (set->list s) ≫
+  [⊢ s ≫ s- ⇒ (~Set τ)]
+  #:fail-unless (pure? #'s-) "expression must be pure"
+  -----------------------
+  [⊢ (set->list- s-) ⇒ (List τ)])
+
+(module+ test
+  (check-type (set 1 2 3)
+              : (Set Int)
+              -> (set- 2 3 1))
+  (check-type (set 1 "hello" 3)
+              : (Set (U Int String))
+              -> (set- "hello" 3 1))
+  (check-type (set-count (set 1 "hello" 3))
+              : Int
+              -> 3)
+  (check-type (set-union (set 1 2 3) (set "hello" "world"))
+              : (Set (U Int String))
+              -> (set- 1 2 3 "hello" "world"))
+  (check-type (set-intersect (set 1 2 3) (set "hello" "world"))
+              : (Set ⊥)
+              -> (set-))
+  (check-type (set-intersect (set 1 "hello" 3) (set #t "world" #f "hello"))
+              : (Set String)
+              -> (set- "hello")))
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Tests
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
\ No newline at end of file