Index: sizechecking/Constraints.hs
===================================================================
--- sizechecking/Constraints.hs	(revision 5)
+++ sizechecking/Constraints.hs	(revision 6)
@@ -12,9 +12,9 @@
 import Data.SBV ( (.==), (.<), (.>=))
 import Control.Monad
-import Data.IORef
+import Data.IORef()
 import Data.Supply as S
 
 asType :: a -> a -> a
-asType a b = a
+asType a _ = a
 
 data D = D { var::Int, cond::[Condition] } 
@@ -36,5 +36,5 @@
 
 appall :: Int -> [L] -> L
-appall var l = foldl (App) (Var $ var) $  l
+appall var = foldl App (Var var)
 
 
@@ -76,5 +76,5 @@
             [] -> (Num 0, b)
             _  -> (expr, b)
-        (_, _)   -> error $ "Expression in condition" ++ (show c)
+        (_, _)   -> error $ "Expression in condition" ++ show c
     where
     nonzero = List.sortBy (Ord.comparing snd) $ filter ((/=0).fst) a
@@ -111,5 +111,4 @@
 norm (AAbs a b e)  = ([], 0, [AAbs a b (normalize e)], [])
 norm (Shift a b c) = ([], 0, [Shift (normalize a) (normalize b) (normalize c)], [])
-norm (Aggr a b c)  = ([], 0, [Aggr a (normalize b) (normalize c)], [])
 norm (Unsized)     = ([], 0, [Unsized], [])
 norm (Bottom)      = ([], 0, [Bottom], [])
@@ -159,12 +158,12 @@
         l1 <- checkCond1 v1 (Condition ((h `LTC` f):d) e' x)
         l2 <- checkCond1 v2 (Condition ((h `GEC` f):d) g' x)
-        putStrLn $ " -> " ++ (show l1)
-        putStrLn $ " -> " ++ (show l2)
+        putStrLn $ " -> " ++ show l1
+        putStrLn $ " -> " ++ show l2
         return $ l1 ++ l2
-    checkCond1 v z@(Condition d (App (Var a) x) (App (Var b) y)) | a==b = do
+    checkCond1 v z@(Condition d (App (Var a) x) (App (Var b) y)) | a==b =
         checkCond1 v (Condition d x y)
-    checkCond1 v p@(Condition d x z@(App (Shift e f g) h)) = do
+    checkCond1 v p@(Condition d x z@(App (Shift e f g) h)) =
         checkCond1 v (Condition d z x)
-    checkCond1 v z@(Condition d a b) = return $ [Condition dd (normalize a) (normalize b)]
+    checkCond1 v z@(Condition d a b) = return [Condition dd (normalize a) (normalize b)]
         where
         dd = normalizecs d
@@ -174,5 +173,4 @@
 subst ndl hst (AAbs a b e)  = AAbs a b (subst ndl hst e)
 subst ndl hst (Shift a b c) = Shift (subst ndl hst a) (subst ndl hst b) (subst ndl hst c)
-subst ndl hst (Aggr a b c)  = Aggr a (subst ndl hst b) (subst ndl hst c)
 subst ndl hst (Unsized)     = Unsized
 subst ndl hst (Bottom)      = Bottom
@@ -201,5 +199,5 @@
 solve l supply = do
     ll <- forM (zip l $ split supply) (\(c,s) -> do
-        putStrLn $ "\nSOLVING "++(show c)
+        putStrLn $ "\nSOLVING " ++ show c 
         solve1 s c
         )
@@ -227,8 +225,8 @@
 
     checkConds [] = False
-    checkConds ((LTC a b):xs) | (elem (GEC a b) xs)            = True
-    checkConds ((GEC a b):xs) | (elem (LTC a b) xs)            = True
-    checkConds ((LTC a (Num b)):xs) | b<=0 && elem (Zero a) xs = True
-    checkConds ((GEC a (Num b)):xs) | b>0  && elem (Zero a) xs = True
+    checkConds (LTC a b : xs) | GEC a b `elem` xs            = True
+    checkConds (GEC a b : xs) | LTC a b `elem` xs            = True
+    checkConds (LTC a (Num b) : xs) | b<=0 && elem (Zero a) xs = True
+    checkConds (GEC a (Num b) : xs) | b>0  && elem (Zero a) xs = True
     checkConds (_:xs) = checkConds xs
 
@@ -259,23 +257,22 @@
             return []
         | a==b = do
-            putStrLn $ "Equals"
+            putStrLn "Equals"
             return []
         | Just (var, nl) <- searchzero d = do
-            let x = (Condition (Prelude.map (normalizec.substc var (Num 0)) nl)
+            let x = Condition (Prelude.map (normalizec.substc var (Num 0)) nl)
                         (normalize$subst var (Num 0) a)
                         (normalize$subst var (Num 0) b)
-                    )
-            putStrLn $ (show $ Var var) ++" is zero:\n" ++ (show x)
+
+            putStrLn $ show (Var var) ++ " is zero:\n" ++ show x
             solve1 supp x 
         | Just (var, exp, nl) <- searcheq d [] = do
-            putStrLn $ "Found equation "++(show $ Var var) ++ " = "++(show exp)
-            let x = (Condition (Prelude.map (normalizec.substc var exp) nl )
+            putStrLn $ "Found equation " ++ show (Var var) ++ " = " ++ show exp
+            let x = Condition (Prelude.map (normalizec.substc var exp) nl )
                         (normalize$subst var exp a)
                         (normalize$subst var exp b)
-                    )
-            putStrLn $ "New equations:\n" ++ (show x)
+            putStrLn $ "New equations:\n" ++ show x
             solve1 supp x 
         | App p q <- a, App r s <- b = do
-            putStrLn $ "Branching!"
+            putStrLn "Branching!"
             nc <- checkCond supp [Condition d p r, Condition d q s] 
             solve nc supp
@@ -291,6 +288,6 @@
 --        | Abs  _ _   <- a, AAbs _ _ _ <- b = applyList a b d supp
 --        | AAbs _ _ _ <- a, AAbs _ _ _ <- b = applyList a b d supp
-        | Just dd <- reorder d = do 
-            putStrLn $ "Reorder " ++ (show dd)
+        | Just dd <- reorder d = do
+            putStrLn $ "Reorder " ++ show dd
             solve1 supp $ Condition dd a b
         | otherwise = do
@@ -309,9 +306,9 @@
 compiletosolver :: L -> L -> [Constraint] -> SBV.Symbolic SBV.SBool
 compiletosolver a b d = do
-    let fvs = Set.toList $ Set.unions $ (fv a):(fv b):(map fvc d)
-    (vars::[SBV.SInteger]) <- mapM SBV.free $ map (flip showVar "") fvs
+    let fvs = Set.toList $ Set.unions $ fv a : fv b : map fvc d
+    (vars::[SBV.SInteger]) <- mapM (SBV.free . flip showVar "") fvs
     let varmap = Map.fromList $ zip fvs vars
-    mapM SBV.constrain $ map (compilec varmap) d
-    return $ (compilel varmap a) .== (compilel varmap b)
+    mapM_ (SBV.constrain . compilec varmap) d
+    return $ compilel varmap a .== compilel varmap b
 
 compilec v (Zero a)  = compilel v a .== (0::SBV.SInteger)
@@ -329,3 +326,3 @@
 compilel v (Var a) | Just x<-Map.lookup a v = x
 compilel v (Num a) = SBV.literal $ fromIntegral a
-compilel v a = error $ "Cannot compile "++(show a)
+compilel v a = error $ "Cannot compile " ++ show a
Index: sizechecking/Lambda.hs
===================================================================
--- sizechecking/Lambda.hs	(revision 5)
+++ sizechecking/Lambda.hs	(revision 6)
@@ -12,9 +12,9 @@
 
 data L = Abs Int L | App L L | Var Int | Num Int | Op L Char L | List L L | AAbs Int Int L
-    | Shift L L L | Unsized | Bottom | Aggr String L L
+    | Shift L L L | Unsized | Bottom 
     deriving Eq
 
 showVar x = if x>28 
-    then showVar (x `div` 29) . (showChar $ chr $ ord 'a' + (x `mod` 29))
+    then showVar (x `div` 29) . showChar (chr $ ord 'a' + (x `mod` 29))
     else showChar $ chr $ ord 'a' + x
 
@@ -24,11 +24,12 @@
 getPrec '*' = (5,5,6)
 getPrec '/' = (5,5,6)
+getPrec c   = error $ "Unknown operator "++[c]
 
 instance Show L where
-    showsPrec p (Abs s l) = showParen (p>0) $ showChar 'Î»' . showVar s . showChar '.' . showsPrec 0 l
-    showsPrec p (AAbs f s l) = showParen (p>0) $ showChar 'Î' . showVar f . showChar ',' . showVar s . showChar '.' . showsPrec 0 l
+    showsPrec p (Abs s l) = showParen (p>0) $ showChar 'Î»' . showVar s . showChar '.' . shows l
+    showsPrec p (AAbs f s l) = showParen (p>0) $ showChar 'Î' . showVar f . showChar ',' . showVar s . showChar '.' . shows l
     showsPrec p (App m n) = showParen (p>6) $ showsPrec 6 m . showChar ' ' . showsPrec 7 n
-    showsPrec p (Var s) = showVar s
-    showsPrec p (Num i) = shows i
+    showsPrec _ (Var s) = showVar s
+    showsPrec _ (Num i) = shows i
     showsPrec p (Op m op n) = showParen (p>prec) $ showsPrec lprec m . showChar op . showsPrec rprec n
         where (prec,lprec,rprec)=getPrec op
@@ -36,7 +37,6 @@
     showsPrec p (Shift e1 s e2) = showParen (p>0) $ showString "Shift " .showsPrec 2 e1 .
         showChar ' ' . showsPrec 2 s . showChar ' ' . showsPrec 2 e2
-    showsPrec p Bottom = showChar 'âŽ'
-    showsPrec p Unsized = showChar 'U'
-    showsPrec p (Aggr name e1 e2) = showParen (p>0) $ showString name .showChar ' ' . showsPrec 2 e1 . showChar ' ' . showsPrec 2 e2
+    showsPrec _ Bottom = showChar 'âŽ'
+    showsPrec _ Unsized = showChar 'U'
 
 t3s = Abs 1 $ Abs 0 $ App t (App t (App t x))
@@ -47,5 +47,4 @@
 subs (List s f)  var exp = List (subs s var exp) (subs f var exp)
 subs (Shift e1 e2 e3) var exp = Shift (subs e1 var exp) (subs e2 var exp) (subs e3 var exp)
-subs (Aggr name e1 e2) var exp = Aggr name (subs e1 var exp) (subs e2 var exp)
 subs (Op x c z)  var exp = Op (subs x var exp) c (subs z var exp)
 subs e@(Var v)   var exp | v==var    = exp
@@ -55,7 +54,7 @@
 subs x@(AAbs s f e) var exp | s==var||f==var = x
                             | otherwise = AAbs s f (subs e var exp)
-subs x@(Num _)   var exp = x
-subs x@Bottom   var exp = x
-subs x@Unsized   var exp = x
+subs x@(Num _)   _ _ = x
+subs x@Bottom    _ _ = x
+subs x@Unsized   _ _ = x
 
 
@@ -68,9 +67,9 @@
 alpha e@Bottom   _    _  = e
 alpha e@Unsized   _    _  = e
-alpha x@(Abs v e) from to | v==from   = Abs to (alpha' e from to)
-                          | otherwise = Abs v (alpha e from to)
-alpha x@(AAbs v1 v2 e) from to | v1==from  = AAbs to v2 (alpha' e from to)
-                               | v2==from  = AAbs v1 to (alpha' e from to)
-                               | otherwise = AAbs v1 v2 (alpha e from to)
+alpha (Abs v e) from to | v==from   = Abs to (alpha' e from to)
+                        | otherwise = Abs v (alpha e from to)
+alpha (AAbs v1 v2 e) from to | v1==from  = AAbs to v2 (alpha' e from to)
+                             | v2==from  = AAbs v1 to (alpha' e from to)
+                             | otherwise = AAbs v1 v2 (alpha e from to)
 
 alpha' (App x z)   from to = App (alpha' x from to) (alpha' z from to)
@@ -80,9 +79,9 @@
 alpha' e@(Var v)   from to | v==from   = Var to
                            | otherwise = e
-alpha' x@(Abs v e) from to | v==from   = Abs to (alpha' e from to)
-                           | otherwise = Abs v (alpha' e from to)
-alpha' x@(AAbs v1 v2 e) from to | v1==from  = AAbs to v2 (alpha' e from to)
-                                | v2==from  = AAbs v1 to (alpha' e from to)
-                                | otherwise = AAbs v1 v2 (alpha' e from to)
+alpha' (Abs v e) from to | v==from   = Abs to (alpha' e from to)
+                         | otherwise = Abs v (alpha' e from to)
+alpha' (AAbs v1 v2 e) from to | v1==from  = AAbs to v2 (alpha' e from to)
+                              | v2==from  = AAbs v1 to (alpha' e from to)
+                              | otherwise = AAbs v1 v2 (alpha' e from to)
 alpha' x@(Num _)   _    _  = x
 alpha' x@Bottom   _    _  = x
@@ -95,11 +94,10 @@
 fv (AAbs x y e) = x `Set.delete` ( y `Set.delete` fv e)
 fv (List s e) = fv s `Set.union` fv e
-fv (Num i) = Set.empty
+fv (Num _) = Set.empty
 fv (Shift e1 e2 e3) = fv e1 `Set.union` fv e2 `Set.union` fv e3
-fv (Aggr _ e1 e2) = fv e1 `Set.union` fv e2 
 fv Unsized = Set.empty
 fv Bottom = Set.empty
 
-bv (Var x) = Set.empty
+bv (Var _) = Set.empty
 bv (App x y) = bv x `Set.union` bv y
 bv (Op x _ y) = bv x `Set.union` bv y
@@ -108,11 +106,10 @@
 bv (AAbs v1 v2 e) = v1 `Set.insert` (v2 `Set.insert` bv e)
 bv (Shift e1 e2 e3) = bv e1 `Set.union` bv e2 `Set.union` bv e3
-bv (Aggr _ e1 e2) = bv e1 `Set.union` bv e2 
-bv (Num i)   = Set.empty
+bv (Num _)   = Set.empty
 bv Unsized = Set.empty
 bv Bottom = Set.empty
 
 maxv (Var x)   = x
-maxv (Num i)   = 0
+maxv (Num _)   = 0
 maxv Unsized = 0
 maxv Bottom = 0
@@ -126,10 +123,10 @@
 rsubs oexp var exp = subs renamed var exp
     where
-    dvar = (fv exp) `Set.intersection` (bv oexp)
+    dvar = fv exp `Set.intersection` bv oexp
     m = maxv exp `max` maxv oexp
     renames = zip (Set.toList dvar) [m+1..]
     renamed = foldr rename oexp renames
-    rename (from,to) exp = alpha oexp from to
-    
+    rename (from,to) _ = alpha oexp from to
+
 
 reduce (App (Abs var exp) z) = return $ rsubs exp var z
@@ -152,9 +149,4 @@
             Just e' -> return $ Shift e1 e' e3
             _       -> reduce e3 >>= \e' -> return $ Shift e1 e2 e'
-reduce (Aggr name e1 e2) = case reduce e1 of
-        Just e -> return $ Aggr name e e2
-        Nothing -> do
-            e <- reduce e2
-            return $ Aggr name e1 e
 reduce (Op m c n) = case c of
     '+' | (Num i, Num j) <- (m,n) -> return $ Num $ i+j
@@ -177,9 +169,9 @@
 it f x = it' f (Just x)
     where
-    it' f Nothing  = []
+    it' _ Nothing  = []
     it' f (Just x) = x:it' f (f x)
 
 rchain :: L -> [L]
-rchain exp = it reduce exp
+rchain = it reduce
 
 pchain = putStrLn . intercalate "\n-> " . map show . rchain
@@ -205,5 +197,5 @@
 lfalse = Abs 0 $ Abs 1 $ Var 1
 
-liszero = Abs n $ App (App (Var n) (Abs x $ lfalse)) ltrue
+liszero = Abs n $ App (App (Var n) (Abs x lfalse)) ltrue
     where (n,x) = (0,1)
 
@@ -229,6 +221,4 @@
 y = 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))
-transposes = AAbs 18 5 $ List ( App (AAbs 15 6 $ Var 15) (Aggr "max" (Var 18) (Var 5)) )-- (App (Var 5) (Num 0)) ) 
-    (Abs 8 $ List (Var 18) $ Abs 9 $ App (AAbs 15 6 $ App (Var 6) (Var 8)) (App (Var 5) (Var 9)))
 reverses = AAbs 18 5 $ List (Var 18) (Abs 8 $ App (Var 5) $ Op (Op (Var 18) '-' (Num 1)) '-' (Var 8) )
 reverse' l = case l of
