sets
This commit is contained in:
parent
6d2d14459c
commit
632c04139b
|
@ -26,6 +26,9 @@
|
||||||
+ - * / and or not > < >= <= = equal? displayln printf
|
+ - * / and or not > < >= <= = equal? displayln printf
|
||||||
;; lists
|
;; lists
|
||||||
list first rest member? empty? for for/fold
|
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
|
;; DEBUG and utilities
|
||||||
print-type print-role
|
print-type print-role
|
||||||
;; Extensions
|
;; Extensions
|
||||||
|
@ -103,6 +106,24 @@
|
||||||
|
|
||||||
(define-type-constructor U* #:arity >= 0)
|
(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)
|
(define-for-syntax (prune+sort tys)
|
||||||
(stx-sort
|
(stx-sort
|
||||||
(filter-maximal
|
(filter-maximal
|
||||||
|
@ -139,22 +160,6 @@
|
||||||
;; User Defined Types, aka Constructors
|
;; 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
|
(begin-for-syntax
|
||||||
(define-splicing-syntax-class type-constructor-decl
|
(define-splicing-syntax-class type-constructor-decl
|
||||||
(pattern (~seq #:type-constructor TypeCons:id))
|
(pattern (~seq #:type-constructor TypeCons:id))
|
||||||
|
@ -1258,6 +1263,97 @@
|
||||||
(define- (member?- v l)
|
(define- (member?- v l)
|
||||||
(and- (member- v l) #t))
|
(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
|
;; Tests
|
||||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
Loading…
Reference in New Issue