Sort out examples and testing

Ignore-this: c276879bc5a84833980ff7bbf49c7cb0 darcs-hash:20111027101641-e29d1-fab00102b29463d92b491051ed18dc14ea96eb8a.gz
adamgundry · Oct 27, 2011 · cab2a2d · cab2a2d
1 parent 83bc1df
commit cab2a2d
Show file tree

Hide file tree

Showing 13 changed files with 134 additions and 229 deletions.
diff --git a/examples/Delay.hs b/examples/Delay.hs
@@ -4,17 +4,9 @@
 
 module Delay where
 
-data Pair :: * -> * -> * where
-  Pair :: forall a b. a -> b -> Pair a b
-
-p1 (Pair a _) = a
-p2 (Pair _ b) = b
-
-
-
-
 data D :: Num -> * -> * where
   D :: forall a (n :: Num) . a -> D n a
+  deriving Show
 
 pure = D
 
@@ -38,44 +30,44 @@ fix f = f (pure (fix f))
 data Tree :: * -> * where
   Leaf :: forall a . a -> Tree a
   Node :: forall a . Tree a -> Tree a -> Tree a
-
+  deriving Show
 
 repMin :: forall a. (a -> a -> a) -> Tree a -> Tree a
 repMin min_ t =
-  let help :: Tree a -> a -> Pair (Tree a) a
-      help (Leaf x) y = Pair (Leaf y) x
+  let help :: Tree a -> a -> (Tree a, a)
+      help (Leaf x) y = (Leaf y, x)
       help (Node l r) y =
         let lm = help l y
             rm = help r y
-        in Pair (Node (p1 lm) (p1 rm)) (min_ (p2 lm) (p2 rm))
+        in (Node (fst lm) (fst rm), min_ (snd lm) (snd rm))
 
-      ans = help t (p2 ans)
-  in p1 ans
+      ans = help t (snd ans)
+  in fst ans
 
 
 repMin2 :: forall a. (a -> a -> a) -> Tree a -> D 1 (Tree a)
 repMin2 min_ t =
-  let help :: Tree a -> D 1 a -> Pair (D 1 (Tree a)) a
-      help (Leaf x) dy = Pair (ap (pure Leaf) dy) x
+  let help :: Tree a -> D 1 a -> (D 1 (Tree a), a)
+      help (Leaf x) dy = (ap (pure Leaf) dy, x)
       help (Node l r) dy =
         let lm = help l dy
             rm = help r dy
-        in Pair (ap (ap (pure Node) (p1 lm)) (p1 rm)) (min_ (p2 lm) (p2 rm))
+        in (ap (ap (pure Node) (fst lm)) (fst rm), min_ (snd lm) (snd rm))
 
-      ans = fix (\ x -> help t (ap (pure p2) x))
-  in p1 ans
+      ans = fix (\ x -> help t (ap (pure snd) x))
+  in fst ans
 
 repMin3 :: forall a (n :: Nat). (a -> a -> a) -> Tree a -> D (n+1) (Tree a)
 repMin3 min_ t =
-  let help :: Tree a -> D (n+1) a -> Pair (D (n+1) (Tree a)) a
-      help (Leaf x) dy = Pair (ap (pure Leaf) dy) x
+  let help :: Tree a -> D (n+1) a -> (D (n+1) (Tree a), a)
+      help (Leaf x) dy = (ap (pure Leaf) dy, x)
       help (Node l r) dy =
         let lm = help l dy
             rm = help r dy
-        in Pair (ap (ap (pure Node) (p1 lm)) (p1 rm)) (min_ (p2 lm) (p2 rm))
+        in (ap (ap (pure Node) (fst lm)) (fst rm), min_ (snd lm) (snd rm))
 
-      ans = fix (\ x -> help t (ap (pure p2) x))
-  in p1 ans
+      ans = fix (\ x -> help t (ap (pure snd) x))
+  in fst ans
 
 repMin4 min_ t = splat {1} (repMin3 min_ t)
 
diff --git a/examples/DelayExtras.hs b/examples/DelayExtras.hs
diff --git a/examples/ExampleExtras.hs b/examples/ExampleExtras.hs
diff --git a/examples/InchPrelude.hs b/examples/InchPrelude.hs
@@ -195,10 +195,10 @@ error'            =  error
 undefined'        :: a
 undefined'        =  error "Prelude.undefined"
 
-
-map :: (a -> b) -> [a] -> [b]
-map f []     = []
-map f (x:xs) = f x : map f xs
+-- built in
+map' :: (a -> b) -> [a] -> [b]
+map' f []     = []
+map' f (x:xs) = f x : map' f xs
 
 -- should be (++)
 append :: [a] -> [a] -> [a]

diff --git a/examples/Queue.hs b/examples/Queue.hs
@@ -1,51 +1,71 @@
+{-
+  Purely Functional Queue with Amortised Linear Cost
+
+  Based on section 3 of 
+
+     Christoph Herrmann, Edwin Brady and Kevin Hammond.
+     "Dependently-typed Programming by Composition from Functional
+     Building Blocks."
+
+     In Draft Proceedings of the 12th International Symposium on
+     Trends in Functional Programming, TFP 2011.
+     Tech. Rep. SIC-07/11, Dept. Computer Systems and Computing,
+     Universidad Complutense de Madrid
+-}
+
 {-# OPTIONS_GHC -F -pgmF inch #-}
 {-# LANGUAGE RankNTypes, GADTs, KindSignatures, ScopedTypeVariables,
              NPlusKPatterns #-}
 
 module Queue where
 
-data Pair :: * -> * -> * where
-  Pair :: forall a b . a -> b -> Pair a b
-
-p0 (Pair a b) = a
-p1 (Pair a b) = b
-
 data Vec :: * -> Num -> * where
-  Nil   :: forall a . Vec a 0
-  Cons  :: forall (n :: Nat) a . a -> Vec a n -> Vec a (n+1)
+    Nil   :: forall a . Vec a 0
+    Cons  :: forall (n :: Nat) a . a -> Vec a n -> Vec a (n+1)
+  deriving Show
+
 
 data Queue :: * -> Num -> * where
-  Q :: forall elem . pi (a b c :: Nat) . Vec elem a -> Vec elem b -> Queue elem (c + 3*a + b)
+    Q :: forall elem . pi (a b c :: Nat) .
+             Vec elem a -> Vec elem b -> Queue elem (c + 3*a + b)
+  deriving Show
 
 initQueue = Q {0} {0} {0} Nil Nil
 
-enqueue :: forall elem (paid :: Nat) . elem -> Queue elem paid -> Queue elem (paid + 4)
+enqueue :: forall elem (paid :: Nat) .
+               elem -> Queue elem paid -> Queue elem (paid + 4)
 enqueue x (Q {a} {b} {c} sA sB) = Q {a+1} {b} {c+1} (Cons x sA) sB
 
-reverseS :: forall elem (paid :: Nat) . Queue elem paid -> Queue elem paid
+reverseS :: forall elem (paid :: Nat) .
+                Queue elem paid -> Queue elem paid
 reverseS (Q {0}   {b} {c} Nil         sB) = Q {0} {b} {c} Nil sB
 reverseS (Q {a+1} {b} {c} (Cons x sA) sB) = reverseS (Q {a} {b+1} {c+2} sA (Cons x sB))
 
-dequeue :: forall elem (paid :: Nat) . Queue elem paid -> Pair elem (Queue elem paid)
-dequeue (Q {a} {b+1} {c} sA (Cons x sB)) = Pair x (Q {a} {b} {c+1} sA sB)
+dequeue :: forall elem (paid :: Nat) .
+               Queue elem paid -> (elem, Queue elem paid)
+dequeue (Q {a} {b+1} {c} sA (Cons x sB)) = (x, Q {a} {b} {c+1} sA sB)
 dequeue (Q {a+1} {0} {c} sA Nil)         = dequeue (reverseS (Q {a+1} {0} {c} sA Nil))
 
 
 
 data Queue2 :: * -> Num -> * where
-  Q2 :: forall elem (a b c :: Nat) . Vec elem a -> Vec elem b -> Queue2 elem (c + 3*a + b)
-
+    Q2 :: forall elem (a b c :: Nat) .
+              Vec elem a -> Vec elem b -> Queue2 elem (c + 3*a + b)
+  deriving Show
 
 initQueue2 :: forall elem . Queue2 elem 0
 initQueue2 = Q2 Nil Nil
 
-enqueue2 :: forall elem (paid :: Nat) . elem -> Queue2 elem paid -> Queue2 elem (paid + 4)
+enqueue2 :: forall elem (paid :: Nat) .
+                elem -> Queue2 elem paid -> Queue2 elem (paid + 4)
 enqueue2 x (Q2 sA sB) = Q2 (Cons x sA) sB
 
-reverseS2 :: forall elem (paid :: Nat) . Queue2 elem paid -> Queue2 elem paid
+reverseS2 :: forall elem (paid :: Nat) .
+                 Queue2 elem paid -> Queue2 elem paid
 reverseS2 (Q2 Nil         sB) = Q2 Nil sB
 reverseS2 (Q2 (Cons x sA) sB) = reverseS2 (Q2 sA (Cons x sB))
 
-dequeue2 :: forall elem (paid :: Nat) . Queue2 elem paid -> Pair elem (Queue2 elem paid)
-dequeue2 (Q2 sA (Cons x sB)) = Pair x (Q2 sA sB)
+dequeue2 :: forall elem (paid :: Nat) .
+                Queue2 elem paid -> (elem, Queue2 elem paid)
+dequeue2 (Q2 sA (Cons x sB)) = (x, Q2 sA sB)
 dequeue2 (Q2 sA Nil)         = dequeue2 (reverseS2 (Q2 sA Nil))
diff --git a/examples/QueueExtras.hs b/examples/QueueExtras.hs
diff --git a/examples/RedBlack.hs b/examples/RedBlack.hs
@@ -5,23 +5,26 @@ module RedBlack where
 
 
 data Ex :: (Num -> *) -> * where
-  Ex :: forall (p :: Num -> *)(n :: Num) . p n -> Ex p
+    Ex :: forall (p :: Num -> *)(n :: Num) . p n -> Ex p
+  deriving Show
 
 unEx :: forall a (p :: Num -> *) . (forall (n :: Num) . p n -> a) -> Ex p -> a
 unEx f (Ex x) = f x
 
 
 
 data Colour :: Num -> * where
-  Black  :: Colour 0
-  Red    :: Colour 1
+    Black  :: Colour 0
+    Red    :: Colour 1
+  deriving Show
 
 data Tree :: * -> Num -> Num -> * where
-  E   :: forall a . Tree a 0 0
-  TR  :: forall a (n :: Num) .
-             a -> Tree a 0 n -> Tree a 0 n -> Tree a 1 n
-  TB  :: forall a (cl cr n :: Num) .
-             a -> Tree a cl n -> Tree a cr n -> Tree a 0 (n+1)
+    E   :: forall a . Tree a 0 0
+    TR  :: forall a (n :: Num) .
+               a -> Tree a 0 n -> Tree a 0 n -> Tree a 1 n
+    TB  :: forall a (cl cr n :: Num) .
+               a -> Tree a cl n -> Tree a cr n -> Tree a 0 (n+1)
+  deriving Show
 
 member :: forall a (cl n :: Num) .
               (a -> a -> Ordering) -> a -> Tree a cl n -> Bool
@@ -39,24 +42,27 @@ member cmp x (TB y a b) =
     case_ GT = member cmp x b
   in case_ (cmp x y)
 
-blackHeight :: forall a b (c n :: Num) . b -> (b -> b) -> Tree a c n -> b
-blackHeight zero suc E = zero
-blackHeight zero suc (TB _ l _) = suc (blackHeight zero suc l)
-blackHeight zero suc (TR _ l _) = blackHeight zero suc l
+member' = member compare
+
+blackHeight :: forall a (c n :: Num) . Tree a c n -> Integer
+blackHeight E           = 0
+blackHeight (TB _ l _)  = 1 + blackHeight l
+blackHeight (TR _ l _)  = blackHeight l
 
 
 -- indexed by root colour, root black height, hole colour and hole black height
 
 data TreeZip :: * -> Num -> Num -> Num -> Num -> * where
-  Root  :: forall a (c n :: Num) . TreeZip a c n c n
-  ZRL   :: forall a (n rc rn :: Num) .
-               a -> TreeZip a rc rn 1 n -> Tree a 0 n -> TreeZip a rc rn 0 n
-  ZRR   :: forall a (n rc rn :: Num) .
-               a -> Tree a 0 n -> TreeZip a rc rn 1 n -> TreeZip a rc rn 0 n
-  ZBL   :: forall a (n c rc rn hc :: Num) .
-               a -> TreeZip a rc rn 0 (n+1) -> Tree a c n -> TreeZip a rc rn hc n
-  ZBR   :: forall a (n c rc rn hc :: Num) .
-               a -> Tree a c n -> TreeZip a rc rn 0 (n+1) -> TreeZip a rc rn hc n
+    Root  :: forall a (c n :: Num) . TreeZip a c n c n
+    ZRL   :: forall a (n rc rn :: Num) .
+                 a -> TreeZip a rc rn 1 n -> Tree a 0 n -> TreeZip a rc rn 0 n
+    ZRR   :: forall a (n rc rn :: Num) .
+                 a -> Tree a 0 n -> TreeZip a rc rn 1 n -> TreeZip a rc rn 0 n
+    ZBL   :: forall a (n c rc rn hc :: Num) .
+                 a -> TreeZip a rc rn 0 (n+1) -> Tree a c n -> TreeZip a rc rn hc n
+    ZBR    :: forall a (n c rc rn hc :: Num) .
+                 a -> Tree a c n -> TreeZip a rc rn 0 (n+1) -> TreeZip a rc rn hc n
+  deriving Show
 
 
 plug :: forall a (rc rn c n :: Num) . Tree a c n -> TreeZip a rc rn c n -> Tree a rc rn
@@ -77,14 +83,16 @@ plugBR t (ZBR x l z) = plug t (ZBR x l z)
 
 
 data ColTree :: * -> Num -> * where
-  CT :: forall a (c n :: Num) . Colour c -> Tree a c n -> ColTree a n
+    CT :: forall a (c n :: Num) . Colour c -> Tree a c n -> ColTree a n
+  deriving Show
 
 
 
 data InsProb :: * -> Num -> Num -> * where
-  Level    :: forall a (c ci n :: Num) . Colour ci -> Tree a ci n -> InsProb a c n
-  PanicRB  :: forall a (n :: Num) . a -> Tree a 1 n -> Tree a 0 n -> InsProb a 1 n
-  PanicBR  :: forall a (n :: Num) . a -> Tree a 0 n -> Tree a 1 n -> InsProb a 1 n
+    Level    :: forall a (c ci n :: Num) . Colour ci -> Tree a ci n -> InsProb a c n
+    PanicRB  :: forall a (n :: Num) . a -> Tree a 1 n -> Tree a 0 n -> InsProb a 1 n
+    PanicBR  :: forall a (n :: Num) . a -> Tree a 0 n -> Tree a 1 n -> InsProb a 1 n
+  deriving Show
 
 solveIns :: forall a (c n rc rn :: Num) . 
              InsProb a c n -> TreeZip a rc rn c n -> ColTree a rn
@@ -255,7 +263,8 @@ delete cmp x {n} t = del cmp x {n} t Root
 
 
 data RBT :: * -> * where
-  RBT :: forall a . pi (n :: Nat) . Tree a 0 n -> RBT a
+    RBT :: forall a . pi (n :: Nat) . Tree a 0 n -> RBT a
+  deriving Show
 
 emptyRBT = RBT {0} E
 
@@ -265,3 +274,6 @@ ctToRBT {n} (CT Red t)   = RBT {n+1} (r2b t)
 
 insertRBT cmp x (RBT {n} t) = ctToRBT {n} (ins cmp x t Root)
 deleteRBT cmp x (RBT {n} t) = delete cmp x {n} t
+
+insertRBT' = insertRBT compare
+deleteRBT' = deleteRBT compare
diff --git a/examples/RedBlackCostExtras.hs b/examples/RedBlackCostExtras.hs