www

commit 3877a28a753f6324d3ce166ba31f7eb961f445f4
parent d1a18786acc9883f0a86fc573f9d7fc48f4f3db4
Author: Ben Greenman <types@ccs.neu.edu>
Date:   Mon, 19 Oct 2015 13:53:15 -0400

[o+] some examples from ICFP'10 paper

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

1 file changed, 56 insertions(+), 0 deletions(-)
diff --git a/tapl/tests/stlc+occurrence-tests.rkt b/tapl/tests/stlc+occurrence-tests.rkt
@@ -207,6 +207,15 @@
  : Boolean
  ⇒ #t)
 
+;; Can refine non-union types
+(check-type-and-result
+ ((λ ([x : Top])
+    (test (Str ? x)
+          x
+          "nope"))
+  "yes")
+ : Str ⇒ "yes")
+
 ;; ----------------------------------------------------------------------------- 
 ;; --- misc subtyping + filters (regression tests)
 (check-type
@@ -548,6 +557,53 @@
  : (List Num))
 
 ;; -----------------------------------------------------------------------------
+;; --- ICFP'10 examples
+
+;; -- Exaple 1 (x can have any type)
+(check-type
+ (λ ([x : Top])
+    (test (Num ? x)
+       (+ 1 x)
+       0))
+ : (→ Top Num))
+
+;; -- Example 2
+(check-type
+ (λ ([x : (∪ Str Num)]
+     [str-length : (→ Str Num)])
+    (test (Num ? x)
+          (+ 1 x)
+          (str-length x)))
+ : (→ (∪ Str Num) (→ Str Num) Num))
+
+;; -- TODO Example 3 (requires IF)
+;; (check-type
+;;  (λ ([member : (→ Num (List Num) Boolean)])
+;;     (λ ([x : Num] [l : (List Num)])
+;;        (if (member x l)
+;;            <compute with x>
+;;            <fail>)))
+;;  : <compute-result>
+
+;; -- Example 4
+(check-type
+ (λ ([x : (∪ Num Str Top)] [f : (→ (∪ Num Str) Num)])
+    (test ((∪ Num Str) ? x)
+          (f x)
+          0))
+ : (→ (∪ Num Str Top) (→ (∪ Num Str) Num) Num))
+
+;; Exmample 10 (we don't allow non-homogenous lists, so need to select head before filtering)
+(check-type
+ (λ ([p : (List (∪ Nat Str))])
+    ((λ ([x : (∪ Nat Str)])
+       (test (Num ? x)
+             (+ 1 x)
+             7))
+    (head p)))
+ : (→ (List (∪ Nat Str)) Num))
+
+;; -----------------------------------------------------------------------------
 ;; --- TODO CPS filters
 
 ;; -----------------------------------------------------------------------------