2019-04-26 19:16:08 +00:00
|
|
|
#lang turnstile
|
|
|
|
|
|
|
|
(provide List
|
|
|
|
(for-syntax ~List)
|
|
|
|
list
|
2019-05-10 14:28:42 +00:00
|
|
|
(typed-out [[cons- : (∀ (X) (→fn X (List X) (List X)))] cons]
|
|
|
|
[[first- : (∀ (X) (→fn (List X) X))] first]
|
2019-05-17 14:34:14 +00:00
|
|
|
[[second- : (∀ (X) (→fn (List X) X))] second]
|
2019-05-10 14:28:42 +00:00
|
|
|
[[rest- : (∀ (X) (→fn (List X) (List X)))] rest]
|
|
|
|
[[member?- (∀ (X) (→fn X (List X) Bool))] member?]
|
|
|
|
[[empty?- (∀ (X) (→fn (List X) Bool))] empty?]
|
2019-05-17 14:34:14 +00:00
|
|
|
[[reverse- (∀ (X) (→fn (List X) (List X)))] reverse]
|
2019-05-24 16:30:26 +00:00
|
|
|
[[partition- (∀ (X) (→fn (List X) (→fn X Bool) (List X)))] partition]
|
|
|
|
[[map- (∀ (X Y) (→fn (→fn X Y) (List X) (List Y)))] map]))
|
2019-04-26 19:16:08 +00:00
|
|
|
|
|
|
|
(require "core-types.rkt")
|
2019-05-09 14:23:15 +00:00
|
|
|
(require (only-in "prim.rkt" Bool))
|
2019-04-26 19:16:08 +00:00
|
|
|
(require (postfix-in - racket/list))
|
|
|
|
|
|
|
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
|
|
;; Lists
|
|
|
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
|
|
|
|
|
|
(define-container-type List #:arity = 1)
|
|
|
|
|
|
|
|
(define-typed-syntax (list e ...) ≫
|
|
|
|
[⊢ e ≫ e- ⇒ τ] ...
|
|
|
|
#:fail-unless (all-pure? #'(e- ...)) "expressions must be pure"
|
|
|
|
-------------------
|
2019-05-13 19:35:38 +00:00
|
|
|
[⊢ (#%app- list- e- ...) ⇒ (List (U τ ...))])
|
2019-04-26 19:16:08 +00:00
|
|
|
|
|
|
|
(define- (member?- v l)
|
2019-05-13 19:35:38 +00:00
|
|
|
(and- (#%app- member- v l) #t))
|