www

commit 92b1f8ec453ab8a689c46b2c19834961de6604e5
parent 5e1d3f1e223e99de0cc6d87b250f2b09ec9aa44e
Author: Stephen Chang <stchang@ccs.neu.edu>
Date:   Mon, 28 Mar 2016 17:26:30 -0400

add implicitqueue tests to polyrecur.mlish

Diffstat:
M
tapl/tests/mlish/polyrecur.mlish
 | 
40
++++++++++++++++++++++++++++++++++++++++

1 file changed, 40 insertions(+), 0 deletions(-)
diff --git a/tapl/tests/mlish/polyrecur.mlish b/tapl/tests/mlish/polyrecur.mlish
@@ -26,3 +26,43 @@
 (check-type 
   (size (Cons 1 (Cons (tup 2 3) (Cons (tup (tup 4 5) (tup 6 7)) Nil)))) 
   : Int -> 7)
+
+(define-type (Digit X)
+  (Zero)
+  (One X)
+  (Two X X))
+
+(define-type (ImplicitQueue X)
+  [Shallow (d : (Digit X))]
+  [Deep (f : (Digit X))
+        (m : (ImplicitQueue (× X X)))
+        (r : (Digit X))])
+
+(define (empty -> (ImplicitQueue X))
+  (Shallow (Zero)))
+
+(define (iq-isEmpty [iq : (ImplicitQueue A)] → Bool)
+  (match iq with
+   [Shallow d ->
+    (match d with
+     [Zero -> #t]
+     [One x -> #f]
+     [Two x y -> #f])]
+   [Deep a b c -> #f]))
+
+(define (iq-snoc [iq : (ImplicitQueue A)] [y : A] → (ImplicitQueue A))
+  (match iq with
+   [Shallow d ->
+    (match d with
+     [Zero -> (Shallow (One y))]
+     [One x -> (Deep (Two x y) (empty) Zero)]
+     [Two x y -> (empty)])] ;; Error
+   [Deep f m d ->
+    (match d with
+     [Zero -> (Deep f m (One y))]
+     [One x -> (Deep f (iq-snoc m (tup x y)) Zero)]
+     [Two x y -> (empty)])])) ; Error
+  
+(check-type (iq-isEmpty (Shallow (Zero {Int}))) : Bool -> #t)
+
+(check-type (iq-isEmpty (iq-snoc (Shallow (Zero {Int})) 5)) : Bool -> #f)