Index: /sizechecking/Examples.hs
===================================================================
--- /sizechecking/Examples.hs	(revision 11)
+++ /sizechecking/Examples.hs	(revision 12)
@@ -4,20 +4,18 @@
 import Lambda
 import SizedExp
-import Prelude (($))
-import Constraints
-import Prelude ( (+), (-), Int, (==), (*), (<), (>), (<=), (>=), (/=) )
+import Constraints()
+import Prelude ( ($), (+), (-), Int, (==), (*), (<), (>), (<=), (>=), (/=) )
 import qualified Prelude as P
 import qualified Control.Monad as M
 import qualified Data.List as List
-import Debug.Trace
 
 head :: (SizedExp se ) => Size se ([l] -> l)
 head = bind headc body
     where 
-    body l = match l true (\x xs -> x) 
+    body l = match l true P.const
 
 tail :: (SizedExp se ) => Size se ([l] -> [l])
 tail = bind tailc body
-    where body l = match l true (\x xs -> xs) 
+    where body l = match l true (\_ xs -> xs)
 
 cons :: (SizedExp se) => Size se (x -> [x] -> [x])
@@ -28,10 +26,10 @@
     where body f x = f `app` (f `app` (f `app` x))
 
-nil :: (SizedExp se) => Size se ([x])
+nil :: (SizedExp se) => Size se [x]
 nil  = bind nils true
 
 map :: (SizedExp se)  => Size se ( (a->b) -> [a] -> [b] )
 map = bind smap body
-    where body f l = match l (nil)
+    where body f l = match l nil
             ( \x xs ->  cons `app` (f `app` x) `app` (map `app` f `app` xs ))
 
@@ -44,5 +42,5 @@
 append :: (SizedExp se) => Size se ([a] -> [a] -> [a])
 append = bind appends body
-    where body l1 l2 = match l1 (l2)
+    where body l1 l2 = match l1 l2
             (\x xs -> cons `app` x `app` (append `app` xs `app` l2))
 
@@ -59,11 +57,11 @@
 
 pam :: (SizedExp se) => Size se ([a -> b] -> a -> [b])
-pam = bind (AAbs 1 2 $ Abs 3 $ List (Var 1) (Abs 4 $ (App (App (Var 2) (Var 4)) (Var 3)))) $ \fl x -> match fl (nil)
+pam = bind (AAbs 1 2 $ Abs 3 $ List (Var 1) (Abs 4 $ App (App (Var 2) (Var 4)) (Var 3))) $ \fl x -> match fl nil
     (\f fs -> cons `app` (f `app` x) `app` (pam `app` fs `app` x))
 
 reverse :: (SizedExp se) => Size se([a] -> [a])
-reverse = bind reverses $ \l -> match l (
+reverse = bind reverses $ \l -> match l
                 nil
-            )(
+            (
                 \x xs -> append `app` (reverse `app` xs) `app` (cons `app` x `app` nil)
             )
@@ -88,26 +86,28 @@
         \f x -> t3 `app` (t3 `app` f) `app` x
 
-add27s = (AAbs 0 1 $ List (Op (Var 0) '+' (Num 27)) (Abs 2 Unsized))
+add27s :: L
+add27s = AAbs 0 1 $ List (Op (Var 0) '+' (Num 27)) (Abs 2 Unsized)
 add27 :: (SizedExp se) => Size se ([P.Int] -> [P.Int])
 add27 = bind add27s $ \x ->  t27 `app` addone `app` x
 
 
+zipWiths :: L
 zipWiths = let q = App (Var 4) $ Op (Op (Var 5) '+' (Var 3)) '-' (Var 1)  in
     (Abs 0 $ AAbs 1 2 $ AAbs 3 4 $ List (Var 1) (Abs 5 $ App (App (Var 0) (App (Var 2) (Var 5))) q ))
 zipWith :: (SizedExp se) => Size se ((a2 -> a1 -> a) -> [a2] -> [a1] -> [a])
 zipWith = bind zipWiths $ \f l1 l2 ->
-        match l1 (
+        match l1
             nil
-        ) (
-            \x xs -> match l2 (
+        (
+            \x xs -> match l2 
                 true
-            ) (
+            (
                 \y ys -> cons `app` (f `app` x `app` y) `app` (zipWith `app` f `app` xs `app` ys)
             )
         )
 appAll :: (SizedExp se) => Size se ( [a -> b] -> a -> [b] )
-appAll = bind (AAbs 0 1 $ Abs 2 $ List (Var 0) (Abs 3 $ Var 1 `App` Var 3 `App` Var 2 ) ) $ \fl x -> match fl ( 
-            nil 
-        ) ( 
+appAll = bind (AAbs 0 1 $ Abs 2 $ List (Var 0) (Abs 3 $ Var 1 `App` Var 3 `App` Var 2 ) ) $ \fl x -> match fl 
+            nil
+        (
             \f fs -> cons `app` (f `app` x) `app` (appAll `app` fs `app` x)
         )
@@ -129,19 +129,19 @@
 sqdiff = bind (let sq l = Op l '*' l in AAbs 0 1 $ AAbs 2 3 $ List (sq $ Op (Var 0) '-' (Var 2)) $ Abs 4 $ List (Num 2) $ Abs 5 Unsized) $
     \l1 l2 -> match l1 (cprod `app` l2 `app` l2)
-        (\hd1 tl1 -> match l2 (cprod `app` l1 `app` l1)
-            (\hd2 tl2 -> sqdiff `app` tl1 `app` tl2))
+        (\_ tl1 -> match l2 (cprod `app` l1 `app` l1)
+            (\_ tl2 -> sqdiff `app` tl1 `app` tl2))
 
 replace :: SizedExp se => Size se (Int -> [Int] -> [Int])
 replace = bind (Abs 0 $ AAbs 1 2 $ List (Var 1) (Abs 3 Unsized)) $
-    \x l -> match l (nil) (\hd tl -> cons `app` (x+hd) `app` tl)
-
-scalar_prod :: (SizedExp se0) =>  Size se0 ([Int] -> [Int] -> [Int])
-scalar_prod = bind (AAbs 0 1 $ AAbs 2 3 $ List (Num 1) (Abs 4  Unsized)) $ 
+    \x l -> match l nil (\hd tl -> cons `app` (x+hd) `app` tl)
+
+scalarProd :: (SizedExp se0) =>  Size se0 ([Int] -> [Int] -> [Int])
+scalarProd = bind (AAbs 0 1 $ AAbs 2 3 $ List (Num 1) (Abs 4  Unsized)) $ 
     \l1 l2 -> match l1 (
         match l2 ( cons `app` 0 `app` nil ) 
-            (\hd2 tl2 -> true)
+            (\_ _ -> true)
     ) ( \hd1 tl1 ->
-        match l2 (true) 
-            ( \hd2 tl2 -> replace `app` (hd1 * hd2) `app` (scalar_prod `app` tl1 `app` tl2) )
+        match l2 true
+            ( \hd2 tl2 -> replace `app` (hd1 * hd2) `app` (scalarProd `app` tl1 `app` tl2) )
     )
 
@@ -157,10 +157,10 @@
 
 take4 :: SizedExp se => Size se (([a] -> [a]) -> [[a]])
-take4 = bind (Abs 0 $ List (Num 1) (Abs 2 (Var 0 `App` (Var 0 `App` List (Num 0) (Abs 1 $ Bottom))))) $
+take4 = bind (Abs 0 $ List (Num 1) (Abs 2 (Var 0 `App` (Var 0 `App` List (Num 0) (Abs 1 Bottom))))) $
     \f ->cons `app` (f `app` (f `app` nil) ) `app` nil
 
 
 merge :: SizedExp se => Size se ([Int] -> [Int] -> [Int])
-merge = bind (AAbs 0 1 $ AAbs 2 3 $ List (Op (Var 0) '+' (Var 2)) (Abs 4 $ Unsized))$
+merge = bind (AAbs 0 1 $ AAbs 2 3 $ List (Op (Var 0) '+' (Var 2)) (Abs 4 Unsized))$
     \l1 l2 -> match l1 l2 (
         \x xs -> match l2 l1 (
@@ -171,12 +171,12 @@
 
 split1 :: SizedExp se => Size se ([Int] -> [Int])
-split1 = bind (AAbs 0 1 $ List (Op (Op (Var 0) '+' (Num 1))'/' (Num 2)) (Abs 2 $ Unsized))  $
+split1 = bind (AAbs 0 1 $ List (Op (Op (Var 0) '+' (Num 1))'/' (Num 2)) (Abs 2 Unsized))  $
     \z -> match z nil (\y ys -> cons `app` y `app` (split2 `app` ys))
 
 split2 :: SizedExp se => Size se ([Int] -> [Int])
-split2 = bind (AAbs 0 1 $ List (Op (Var 0) '/' (Num 2)) (Abs 2 $ Unsized)) $
+split2 = bind (AAbs 0 1 $ List (Op (Var 0) '/' (Num 2)) (Abs 2 Unsized)) $
     \z -> match z nil (\y ys -> split1 `app` ys)
 
-ms = (AAbs 0 1 $ List (Var 0) (Abs 4 $ Unsized))
+ms = AAbs 0 1 $ List (Var 0) (Abs 4 Unsized)
 mergesort :: SizedExp se => Size se ([Int] -> [Int])
 mergesort = bind ms $
@@ -194,5 +194,5 @@
 
 fix :: SizedExp se => Size se ((a -> a) -> a)
-fix = bind (Abs 2 $ App y (Var 2)) $ 
+fix = bind (Abs 2 $ App yComb (Var 2)) $ 
     \f -> f `app` (fix `app` f)
 
@@ -202,19 +202,19 @@
         \x xs -> cons `app` (cons `app` x `app` (heads `app` xss))
             `app` (transpose `app` (cons `app` xs `app` (tails `app` xss)))
-transposec = (AAbs 18 5 $ List len fun ) 
+transposec = AAbs 18 5 $ List len fun
     where
-    len = (AAbs 19 6 $ (Var 19) ) `App` (Var 5 `App` Num 0)
-    fun = Abs 8 $ List (Var 18) (Abs 9 $  (AAbs 19 6 $ Var 6 `App` Var 8 ) `App` (Var 5 `App` Var 9) )
-
-comps = (Abs 2 $ Abs 3 $ Abs 4 $ App (Var 2) (App (Var 3) (Var 4)) )
+    len = AAbs 19 6 (Var 19) `App` (Var 5 `App` Num 0)
+    fun = Abs 8 $ List (Var 18) (Abs 9 $ AAbs 19 6 (Var 6 `App` Var 8) `App` (Var 5 `App` Var 9))
+
+comps = Abs 2 $ Abs 3 $ Abs 4 $ App (Var 2) (App (Var 3) (Var 4))
 comp :: (SizedExp se)  => Size se ( (b->c) -> (a->b) -> a->c )
 comp = bind comps $ \f g x -> f `app` (g `app` x)
 
-test1s = Abs 2 $ AAbs 19 6 $ (Var 2) `App` (List (Var 19) (Var 6))
+test1s = Abs 2 $ AAbs 19 6 $ Var 2 `App` List (Var 19) (Var 6)
 test1 :: (SizedExp se)  => Size se (([a] -> [b]) -> [a] -> [b])
 test1 = bind test1s $ \f l -> match (f `app` l) nil (\x xs -> f `app` l)
 
 
-test2s = Abs 2 $ AAbs 18 5  $ appends `App` (Var 2 `App` (List (Var 18) (Var 5))) `App` (List (Var 18) (Var 5))
+test2s = Abs 2 $ AAbs 18 5  $ appends `App` (Var 2 `App` List (Var 18) (Var 5)) `App` List (Var 18) (Var 5)
 test2 :: (SizedExp se)  => Size se (([a] -> [a]) -> [a] -> [a])
 test2 = bind test2s $ \f l -> append `app` (f `app` l) `app` l
@@ -244,5 +244,5 @@
         , TestCase "appAll" appAll
         , TestCase "conspack" conspack
-        , TestCase "scalar_prod" scalar_prod
+        , TestCase "scalarProd" scalarProd
         , TestCase "sqdiff" sqdiff
         , TestCase "mlist" mlist
@@ -255,13 +255,10 @@
 runTests = do
     failed <- M.forM tests $ \(TestCase name test) -> do
-        P.print$ " +++++++++++++++++++++++++++++++"
-        P.print$ " +  Proving " P.++ name
-        P.print$ " +++++++++++++++++++++++++++++++"
+        P.print " +++++++++++++++++++++++++++++++"
+        P.print $ " +  Proving " P.++ name
+        P.print " +++++++++++++++++++++++++++++++"
 
         s <- prove test
-        if P.not s then
-            M.return [name]
-          else
-            M.return []
+        M.return [name | P.not s]
 
     let f = P.concat failed
@@ -269,5 +266,5 @@
         P.putStrLn "All ok."
       else do
-        P.putStr $ "\n\nFailed test cases: "
+        P.putStr "\n\nFailed test cases: "
         P.putStrLn $ List.intercalate ", " f
 
Index: /sizechecking/Lambda.hs
===================================================================
--- /sizechecking/Lambda.hs	(revision 11)
+++ /sizechecking/Lambda.hs	(revision 12)
@@ -219,5 +219,5 @@
 dupfst = AAbs 19 5 $ List (Op (Num 1) '+' (Var 19)) $ Shift (Var 5) (Op (Var 19) '-' (Num 1)) 
     $ Abs 8 $ App (Var 5) (Op (Var 19) '-' (Num 1))
-y = Abs 18 $ App (Abs 22 $ App (Var 18) (App (Var 22) (Var 22))) (Abs 22 $ App (Var 18) (App (Var 22) (Var 22)))
+yComb = Abs 18 $ App (Abs 22 $ App (Var 18) (App (Var 22) (Var 22))) (Abs 22 $ App (Var 18) (App (Var 22) (Var 22)))
 -- Λs,g.List s (λi.(λx.Λt,f.List (1+t) (Shift f (t-1) x)) U (g i))
 reverses = AAbs 18 5 $ List (Var 18) (Abs 8 $ App (Var 5) $ Op (Op (Var 18) '-' (Num 1)) '-' (Var 8) )
Index: /sizechecking/SizedExp.hs
===================================================================
--- /sizechecking/SizedExp.hs	(revision 11)
+++ /sizechecking/SizedExp.hs	(revision 12)
@@ -11,5 +11,6 @@
 import Constraints 
 import Data.Supply
-
+import Control.Arrow
+import Control.Monad
 
 class TS b => (Unify se a b)  where
@@ -19,8 +20,8 @@
 
 instance (SizedExp se, Unify se a b, se~se1, c1~c2, TS c2) => Unify se (Size se1 c1->a) (c2->b) where
-    unify f g x = f undefined x
+    unify f g = f undefined
 
 instance (SizedExp se, se~se1, c1~c2, TS c2) => Unify se (Size se1 c1) c2 where
-    unify f g x = g undefined x
+    unify f g = g undefined
 
 class SizedExp (se :: * -> *) where
@@ -77,16 +78,16 @@
     (s1, s2, s3) = split3 supply
     freshvars' :: (Unify Q a b) => (a -> (Size Q b, L -> L)) -> (Size Q c -> a) -> (Size Q (c -> b), L -> L)
-    freshvars' u exp = (QSynt $ sizeof $ x, \l -> f $ App l fv)
+    freshvars' u exp = (QSynt $ sizeof x, \l -> f $ App l fv)
         where
         (x, f) = u $ exp $ QSynt $ do 
-            putStrLn $ "[Bind] var="++(show fv)++" of type "++(show $ tk q)
+            putStrLn $ "[Bind] var="++ show fv ++" of type "++ show (tk q)
             return [([], fv)]
         fv = fresh (tk q) s3
 
 addConstraint :: Constraint -> [SExp] -> [SExp]
-addConstraint nc = map (\(c,l) -> (nc:c, l))
+addConstraint nc = map (first ((:) nc))
 
 concatMapM :: (a -> IO [b]) -> [a] -> IO [b]
-concatMapM f l = mapM f l >>= return.concat
+concatMapM f l = liftM concat $ mapM f l
     
 type SExp = ([Constraint], L)
@@ -99,14 +100,14 @@
             match1 (cond, ltype) = do
                     x <- sizeof l
-                    putStrLn $ "ORIGINAL is " ++ (show x)
-                    putStrLn $ "[MATCH] ==> " ++ (show $ ltype)
+                    putStrLn $ "ORIGINAL is " ++ show x
+                    putStrLn $ "[MATCH] ==> " ++ show ltype
                     let lt = rall$  App (AAbs 18 5 $ Var 18) ltype
-                    putStrLn $ " --- NIL  ---" ++ (show lt)
+                    putStrLn $ " --- NIL  ---" ++ show lt
                     nils <- sizeof nil
-                    putStrLn $ show nils
+                    print nils
                     let nilc = foldr addConstraint nils $ Zero lt:cond
                     let tx = rall $ App (AAbs 18 5 $ App (Var 5) (Op (Var 18) '-' (Num 1))) ltype
                     let txs = rall $App (AAbs 18 5 $ List (Op (Var 18) '-' (Num 1)) (Var 5)) ltype
-                    putStrLn $ " --- CONS --- "++(show tx)++" <-> "++(show txs)
+                    putStrLn $ " --- CONS --- "++ show tx ++" <-> "++ show txs
                     conss <- sizeof $ cons (QSynt$return [([], tx)]) (QSynt$return [([], txs)])
                     print conss
@@ -151,7 +152,7 @@
     fromInteger = num
 
-prove :: Size Q b -> IO (Bool)
+prove :: Size Q b -> IO Bool
 prove (QProvable l x) = do
-    (s1,s2,s3) <- newSupply 30 (+1) >>= return.split3
+    (s1,s2,s3) <- liftM split3 $ newSupply 30 (+1)
     c <- x s1
     putStrLn ""