diff --git a/tapl/stlc+occurrence.rkt b/tapl/stlc+occurrence.rkt index 98ea25d..345ab4f 100644 --- a/tapl/stlc+occurrence.rkt +++ b/tapl/stlc+occurrence.rkt @@ -187,6 +187,7 @@ ;; Makes it easy to add a new filter & avoids duplicating this map (begin-for-syntax + (define current-Π (make-parameter (lambda (x) (error 'Π)))) (define (simple-Π τ) (syntax-parse (τ-eval τ) [~Boolean @@ -202,9 +203,13 @@ [(~→ τ* ... τ) (define k (stx-length #'(τ* ...))) #`(lambda (f) (and (procedure? f) (procedure-arity-includes? f #,k #f)))] + [(~∪ τ* ...) + (define filter* (for/list ([τ (in-syntax #'(τ* ...))]) + ((current-Π) τ))) + #`(lambda (v) (for/or ([f (in-list (list #,@filter*))]) (f v)))] [_ (error 'Π "Cannot make filter for type ~a\n" (syntax->datum τ))])) - (define current-Π (make-parameter simple-Π))) + (current-Π simple-Π)) ;; (test (τ ? x) e1 e2) ;; TODO: @@ -228,9 +233,3 @@ ((lambda x2 e2+) x-stx)) : (∪ τ1 τ2))]) -;; - TEST function filters (delayed filters?) -;; - disallow (U (-> ...) (-> ...)) -;; - TEST latent filters -- listof BLAH - -;; - integrate with sysf - diff --git a/tapl/tests/stlc+occurrence-tests.rkt b/tapl/tests/stlc+occurrence-tests.rkt index f815af4..6884199 100644 --- a/tapl/tests/stlc+occurrence-tests.rkt +++ b/tapl/tests/stlc+occurrence-tests.rkt @@ -328,12 +328,65 @@ #:with-msg "Cannot discriminate") ;; ----------------------------------------------------------------------------- -;; --- TODO Filter values (should do nothing) +;; --- Filter with unions + +(check-type + (λ ([x : (∪ Int Str)]) + (test ((∪ Int Str) ? x) + x + "nope")) + : (→ (∪ Int Str) (∪ Int Str))) + +(check-type + (λ ([x : (∪ Int Str Boolean)]) + (test ((∪ Int Str) ? x) + x + "Nope")) + : (→ (∪ Int Str Boolean) (∪ Int Str))) + +(check-type + (λ ([x : (∪ Int Str Boolean)]) + (test ((∪ Int Str) ? x) + (test (Str ? x) + "yes" + "int") + "bool")) + : (→ (∪ Int Str Boolean) Str)) + +(check-type-and-result + ((λ ([x : (∪ Str Boolean)]) + (test ((∪ Int Nat Num) ? x) + x + (+ 1 2))) "hi") + : Num ⇒ 3) + +(check-type-and-result + ((λ ([x : (∪ Str Int Boolean)]) + (test ((∪ Int Str) ? x) + x + "error")) 1) + : (∪ Str Int) ⇒ 1) + +(check-type-and-result + ((λ ([x : (∪ Str Int Boolean)]) + (test ((∪ Int Str) ? x) + x + "error")) "hi") + : (∪ Int Str) ⇒ "hi") + +;; ----------------------------------------------------------------------------- +;; --- TODO CPS filters + +;; ----------------------------------------------------------------------------- +;; --- TODO Filter on values (should do nothing) ;; (check-type ;; (test (Int ? 1) #t #f) ;; : Boolean) +;; ----------------------------------------------------------------------------- +;; --- TODO Values as filters (check equality) + ;; ----------------------------------------------------------------------------- ;; --- TODO Latent filters (on data structures)