www

commit 36d568b512520df677078145ba25eae922c57809
parent dfaab96a29c50f0bd041319d95b6455930ffd183
Author: Ben Greenman <types@ccs.neu.edu>
Date:   Thu, 15 Oct 2015 15:08:25 -0400

[o+] allow unions as filters

Diffstat:
M
tapl/stlc+occurrence.rkt
 | 
13
++++++-------
M
tapl/tests/stlc+occurrence-tests.rkt
 | 
55
++++++++++++++++++++++++++++++++++++++++++++++++++++++-

2 files changed, 60 insertions(+), 8 deletions(-)
diff --git 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
@@ -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)