Index: /sizechecking/Constraints.hs
===================================================================
--- /sizechecking/Constraints.hs	(revision 5)
+++ /sizechecking/Constraints.hs	(revision 5)
@@ -0,0 +1,331 @@
+{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances,
+             IncoherentInstances, RankNTypes, ScopedTypeVariables,
+             FlexibleContexts,UndecidableInstances #-}
+module Constraints where
+
+import Lambda
+import qualified Data.List as List
+import qualified Data.Set as Set
+import qualified Data.Map as Map
+import qualified Data.Ord as Ord
+import qualified Data.SBV as SBV
+import Data.SBV ( (.==), (.<), (.>=))
+import Control.Monad
+import Data.IORef
+import Data.Supply as S
+
+asType :: a -> a -> a
+asType a b = a
+
+data D = D { var::Int, cond::[Condition] } 
+
+data TypeKind = V | L TypeKind | F TypeKind TypeKind | U
+    deriving Show
+
+
+class TS a where
+    tk :: a -> TypeKind
+instance (TS a, TS b) => TS (a -> b) where
+    tk _ = F (tk (undefined :: a)) (tk (undefined :: b))
+instance TS a => TS [a] where
+    tk _ = L (tk (undefined :: a))
+instance TS a where
+    tk _ = V
+instance TS Int where
+    tk _ = U
+
+appall :: Int -> [L] -> L
+appall var l = foldl (App) (Var $ var) $  l
+
+
+data Condition = Condition [Constraint] L L
+
+instance Show Condition where
+    showsPrec _ (Condition d a b) = shows d . showString "|- " . shows a . showString " = " . shows b
+    showList [] = showString ""
+    showList [x] = shows x
+    showList (x:xs) = shows x . showString "\n" . shows xs
+
+data Constraint = Zero L | LTC L L | GEC L L
+    deriving Eq
+
+instance Show Constraint where
+    showList []     = id
+    showList [s]    = shows s . showChar ' '
+    showList (x:xs) = shows x . showString ", " . shows xs
+    showsPrec _ (Zero s) = shows s . showString " = 0"
+    showsPrec _ (LTC s1 s2) = shows s1 . showString " < " . shows s2
+    showsPrec _ (GEC s1 s2) = shows s1 . showString " >= " . shows s2
+
+normalize :: L -> L
+normalize l = delzero $ foldl (\a b -> Op a '-' b) (foldl (\a b -> Op  a '+' b) (f1 $ List.sortBy (Ord.comparing snd) a) c) d
+    where
+    (a,b,c,d) = norm l
+    f1 ((0,l):xs) = f1 xs
+    f1 ((1,l):xs) = Op (f1 xs) '+' (Var l)
+    f1 ((-1,l):xs) = Op (f1 xs) '-' (Var l)
+    f1 [] = Num b
+
+    delzero (Op (Num 0) '+' b) = b
+    delzero (Op a c b) = Op (delzero a) c b
+    delzero l          = l
+
+gnormalize :: L -> (L, Int)
+gnormalize l = case (c,d) of
+        ([], []) -> case nonzero of
+            [] -> (Num 0, b)
+            _  -> (expr, b)
+        (_, _)   -> error $ "Expression in condition" ++ (show c)
+    where
+    nonzero = List.sortBy (Ord.comparing snd) $ filter ((/=0).fst) a
+    proc (1, l) = Var l
+    proc (-1, l) = Op (Num (-1)) '*' (Var l)
+    t :: L -> (Int, Int) -> L
+    t l (1, var) = Op l '+' (Var var)
+    t l (-1, var) = Op l '-' (Var var)
+    expr = foldl t (proc $ head nonzero) (tail nonzero)
+
+    (a,b,c,d) = norm l
+
+normalizec :: Constraint -> Constraint
+normalizec (Zero l) = Zero $ normalize l
+normalizec (LTC a b) = LTC (normalize a) (normalize b)
+normalizec (GEC a b) = GEC (normalize a) (normalize b)
+--normalizec (LTC a b) = LTC x (Num (-y))
+--    where (x,y) = gnormalize $ Op a '-' b 
+--normalizec (GEC a b) = GEC x (Num (-y))
+--    where (x,y) = gnormalize $ Op a '-' b 
+
+normalizecs :: [Constraint] -> [Constraint]
+normalizecs = normalizecs' . Prelude.map normalizec
+    where
+    normalizecs' [] = []
+    normalizecs' (x:xs) = x:normalizecs' (filter (/=x) xs)
+
+{-
+ - Takes an extended lambda expression and 
+ -}
+norm :: L -> ([(Int, Int)], Int, [L], [L])
+norm (App a b)     = ([], 0, [App (normalize a) (normalize b)], [])
+norm (List a b)    = ([], 0, [List (normalize a) (normalize b)], [])
+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], [])
+norm (Abs i l)     = ([], 0, [Abs i $ normalize l], [])
+norm (Var i)       = ([(1, i)], 0, [], [])
+norm (Num i)       = ([], i, [], [])
+norm q@(Op a c b)  = case c of
+    '+' -> (a1++b1, a2+b2, a3++b3, a4++b4)
+    '-' -> (sub a1 b1, a2-b2, a3++b4, a4++b3)
+    '*' -> case a of
+            (Num cnt) -> (map (mul cnt) b1, cnt*b2, map (Op (Num cnt) '*') b3, map (Op (Num cnt) '*') b4)
+            _         -> ([], 0, [q], [])
+    _   -> ([], 0, [q], [])
+    where
+        mul c (x,var) = (c*x, var)
+        (a1, a2, a3, a4) = norm a
+        (b1, b2, b3, b4) = norm b
+        sub l1 ((c,i):xs) = sub (sub' l1 c i) xs
+            where
+            sub' [] c i = [(-c, i)]
+            sub' ((cc,ii):xs) c i = if i==ii then (cc-c,i):xs else (cc,ii):sub' xs c i
+        sub l1 [] = l1
+
+tnorm = Op (Num 1) '+' (Op (Var 0) '-' (Num 1))
+
+checkCond :: Supply Int -> [Condition] -> IO [Condition]
+checkCond v l = do
+    ll <- mapM (checkCond1 v) l
+    return $ concat ll
+
+    where
+--    checkCond1 v p@(Condition d a b) | a==b = do
+--        return  []
+    checkCond1 v z@(Condition d (List a b) (List p q)) = do
+--        i <- freshtypevar v
+        let (v1,v2,v3) = split3 v
+        let i = supplyValue v1
+        let b' = rall $ App b (Var i)
+        let q' = rall $ App q (Var i)
+        l1 <- checkCond1 v2 (Condition ((Var i `GEC` Num 0):d) a p) 
+        l2 <- checkCond1 v3 (Condition ((Var i `GEC` Num 0):(Var i `LTC` a):(Var i `LTC` p):d) b' q')
+        return $ l1++l2
+    checkCond1 v z@(Condition d (App (Shift e f g) h) x) = do
+        let (v1,v2,v3) = split3 v
+        let e' = rall $ App e h
+        let g' = rall $ App g $ Op h '-' f
+        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)
+        return $ l1 ++ l2
+    checkCond1 v z@(Condition d (App (Var a) x) (App (Var b) y)) | a==b = do
+        checkCond1 v (Condition d x y)
+    checkCond1 v p@(Condition d x z@(App (Shift e f g) h)) = do
+        checkCond1 v (Condition d z x)
+    checkCond1 v z@(Condition d a b) = return $ [Condition dd (normalize a) (normalize b)]
+        where
+        dd = normalizecs d
+
+subst ndl hst (App a b)     = App (subst ndl hst a) (subst ndl hst b)
+subst ndl hst (List a b)    = List (subst ndl hst a) (subst ndl hst b)
+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
+subst ndl hst q@(Abs i l)   = if ndl==i then q else Abs i $ subst ndl hst l
+subst ndl hst q@(Var i)     = if ndl==i then hst else q
+subst ndl hst (Num i)       = Num i
+subst ndl hst (Op a c b)    = Op (subst ndl hst a) c (subst ndl hst b)
+
+substc ndl hst (Zero l)  = Zero $ subst ndl hst l
+substc ndl hst (LTC a b) = LTC (subst ndl hst a) (subst ndl hst b)
+substc ndl hst (GEC a b) = GEC (subst ndl hst a) (subst ndl hst b)
+
+reorder cs = if any check cs 
+        then Just (map r cs)
+        else Nothing
+    where
+    check (Zero _)        = False
+    check (LTC a (Num 0)) = False 
+    check (GEC a (Num 0)) = False 
+    check _               = True
+    r (LTC a b) = LTC (normalize (Op a '-' b)) (Num 0)
+    r (GEC a b) = GEC (normalize (Op a '-' b)) (Num 0)
+    r l         = l
+
+solve :: [Condition] -> Supply Int -> IO [Condition]
+solve l supply = do
+    ll <- forM (zip l $ split supply) (\(c,s) -> do
+        putStrLn $ "\nSOLVING "++(show c)
+        solve1 s c
+        )
+    return $ concat ll
+    where
+
+    searchzero (Zero (Var a):xs) = Just (a,xs)
+    searchzero (x:xs)            = do
+        (a,l) <- searchzero xs
+        return (a,x:l)
+    searchzero []                = Nothing
+
+
+    searcheq (q@(GEC (Var var) exp):xs) prev = case findeq (List.reverse prev ++ xs) [] of
+            Nothing -> searcheq xs (q:prev)
+            l       -> l
+        where
+        expinc = normalize $ Op exp '+' $ Num 1
+        findeq []                       _     = Nothing
+        findeq (LTC (Var var2) exp2:xs) prev2 | var==var2 && exp2==expinc = Just (var, exp, List.reverse prev2 ++ xs)
+        findeq (x:xs)                   prev2 = findeq xs (x:prev2)
+
+    searcheq (x:xs)                 prev = searcheq xs (x:prev) 
+    searcheq []                     _    = Nothing
+
+    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 (_:xs) = checkConds xs
+
+    checkConds2 (LTC (Num a) (Num b):xs) | a>=b = Nothing
+    checkConds2 (LTC (Num a) (Num b):xs) | a<b  = checkConds2 xs
+    checkConds2 (GEC (Num a) (Num b):xs) | a<b  = Nothing
+    checkConds2 (GEC (Num a) (Num b):xs) | a>=b = checkConds2 xs
+    checkConds2 (x:xs)                          = do { y <- checkConds2 xs; return (x:y) }
+    checkConds2 []                              = Just []
+
+--    applyList a b d supp = do
+--        let (s1,s2,s3) = split3 supp
+--        let t = fresh (L V) s1
+--        let dd = (Condition d (rall $ App a t) (rall $ App b t))
+--        putStrLn $ "Applying a fresh variable: "++(show t) ++"\n"++(show dd)
+--        x <- checkCond s2 [dd] >>= mapM (solve1 s3)
+--        return $ concat x
+
+    solve1  supp c@(Condition d a b) = case checkConds2 d of
+        Nothing -> do
+            putStrLn "Contradiction in preconditions"
+            return []
+        Just d' -> solve1' supp $ Condition d a b
+
+    solve1' supp c@(Condition d a b)
+        | checkConds d = do
+            putStrLn "Contradiction in preconditions"
+            return []
+        | a==b = do
+            putStrLn $ "Equals"
+            return []
+        | Just (var, nl) <- searchzero d = do
+            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)
+            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 )
+                        (normalize$subst var exp a)
+                        (normalize$subst var exp b)
+                    )
+            putStrLn $ "New equations:\n" ++ (show x)
+            solve1 supp x 
+        | App p q <- a, App r s <- b = do
+            putStrLn $ "Branching!"
+            nc <- checkCond supp [Condition d p r, Condition d q s] 
+            solve nc supp
+
+
+--        | Abs _ _ <- a, Abs _ _ <- b = do
+--            let (s1, s2) = split2 supp
+--            let t = fresh (tk a) s1
+--            let dd= (Condition d (rall $ App a t) (rall $ App b t))
+--            putStrLn $ "Applying a fresh variable: "++(show t) ++"\n"++(show dd)
+--            solve1 s2 dd
+--        | AAbs _ _ _ <- a, Abs  _ _   <- b = applyList a b d supp
+--        | 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)
+            solve1 supp $ Condition dd a b
+        | otherwise = do
+            putStrLn "Tying to call solver"
+            let x = compiletosolver a b d
+            y <- SBV.prove x
+            print y
+            case y of
+                (SBV.ThmResult (SBV.Unsatisfiable _)) -> return []
+                otherwise -> return [c]
+
+fvc (Zero a)  = fv a
+fvc (LTC a b) = fv a `Set.union` fv b
+fvc (GEC a b) = fv a `Set.union` fv b
+
+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 varmap = Map.fromList $ zip fvs vars
+    mapM SBV.constrain $ map (compilec varmap) d
+    return $ (compilel varmap a) .== (compilel varmap b)
+
+compilec v (Zero a)  = compilel v a .== (0::SBV.SInteger)
+compilec v (LTC a b) = compilel v a .<  compilel v b
+compilec v (GEC a b) = compilel v a .>= compilel v b
+
+compilel :: Map.Map Int SBV.SInteger -> L -> SBV.SInteger
+compilel v (Op a c b) = case c of 
+    '+' -> al + bl
+    '-' -> al - bl
+    '*' -> al * bl
+    where
+    al = compilel v a
+    bl = compilel v b
+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)
Index: /sizechecking/Examples.hs
===================================================================
--- /sizechecking/Examples.hs	(revision 5)
+++ /sizechecking/Examples.hs	(revision 5)
@@ -0,0 +1,263 @@
+{-# LANGUAGE ScopedTypeVariables, ExistentialQuantification, Rank2Types #-}
+module Examples where
+
+import Lambda
+import SizedExp
+import Prelude (($))
+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) 
+
+tail :: (SizedExp se ) => Size se ([l] -> [l])
+tail = bind tailc body
+    where body l = match l true (\x xs -> xs) 
+
+cons :: (SizedExp se) => Size se (x -> [x] -> [x])
+cons = bind conss true
+
+t3 :: (SizedExp se) => Size se ( (a -> a) -> a -> a )
+t3 = bind t3s body
+    where body f x = f `app` (f `app` (f `app` 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)
+            ( \x xs ->  cons `app` (f `app` x) `app` (map `app` f `app` xs ))
+
+heads :: (SizedExp se) => Size se ( [[a]] -> [a] )
+heads = bind sheads $ \l ->  map `app` head `app` l
+
+tails :: (SizedExp se) => Size se ( [[a]] -> [[a]] )
+tails = bind stails $ \l ->  map `app` tail `app` l
+
+append :: (SizedExp se) => Size se ([a] -> [a] -> [a])
+append = bind appends body
+    where body l1 l2 = match l1 (l2)
+            (\x xs -> cons `app` x `app` (append `app` xs `app` l2))
+
+t27 :: (SizedExp se) => Size se ((a -> a) -> a -> a)
+t27 = bind ( App t3s t3s) $ t3 `app` t3
+
+t27_ :: (SizedExp se) => Size se ((a -> a) -> a -> a)
+t27_ = bind ( App t3s t3s) $ 
+        \f ->  t3 `app` t3 `app` f
+
+t27__ :: (SizedExp se) => Size se ((a -> a) -> a -> a)
+t27__ = bind ( App t3s t3s) $ \f x ->
+            t3 `app` t3 `app` f `app` x
+
+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)
+    (\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 (
+                nil
+            )(
+                \x xs -> append `app` (reverse `app` xs) `app` (cons `app` x `app` nil)
+            )
+
+addone :: (SizedExp se) => Size se ([P.Int] -> [P.Int])
+addone = bind addones $ \l -> cons `app` 1 `app` l
+
+add3 :: (SizedExp se) => Size se ([P.Int] -> [P.Int])
+add3 = bind (AAbs 0 1 $ List (Op (Var 0) '+' (Num 3)) (Var 1)) $
+        \l -> t3 `app` addone `app` l
+
+add3_ :: (SizedExp se) => Size se ([P.Int] -> [P.Int])
+add3_ = bind (AAbs 0 1 $ List (Op (Var 0) '+' (Num 3)) (Var 1)) $
+        t3 `app` addone 
+
+t9_ :: (SizedExp se) => Size se ((a -> a) -> a -> a)
+t9_ = bind ( Abs 0 $ App t3s (App t3s (Var 0))) $
+        \f -> t3 `app` (t3 `app` f)
+
+t9 :: (SizedExp se) => Size se ((a -> a) -> a -> a)
+t9 = bind ( Abs 0 $ App t3s (App t3s (Var 0))) $
+        \f x -> t3 `app` (t3 `app` f) `app` x
+
+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 = 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 (
+            nil
+        ) (
+            \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 
+        ) ( 
+            \f fs -> cons `app` (f `app` x) `app` (appAll `app` fs `app` x)
+        )
+
+conspack :: (SizedExp se) => Size se (P.Int -> [P.Int] -> [P.Int])
+conspack = bind (Abs 0 $ AAbs 1 2 $ List (Op (Var 1) '+' (Num 1)) (Abs 3 Unsized)) $ \x l ->
+    match l (cons `app` x `app` l) 
+    (\hd tl -> iff (x == hd) (
+            cons `app` x `app` l
+        ) (
+            cons `app` hd `app` (conspack `app` x `app` tl)
+        )
+    )
+
+cprod :: (SizedExp se) => Size se ([P.Int] -> [P.Int] -> [[P.Int]])
+cprod = known  (AAbs 0 1 $ AAbs 2 3 $ List (Op (Var 0) '*' (Var 2)) $ Abs 4 $ List (Num 2) $ Abs 5 Unsized) 
+
+sqdiff :: SizedExp se => Size se ([Int] -> [Int] -> [[Int]])
+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))
+
+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)) $ 
+    \l1 l2 -> match l1 (
+        match l2 ( cons `app` 0 `app` nil ) 
+            (\hd2 tl2 -> true)
+    ) ( \hd1 tl1 ->
+        match l2 (true) 
+            ( \hd2 tl2 -> replace `app` (hd1 * hd2) `app` (scalar_prod `app` tl1 `app` tl2) )
+    )
+
+mlist :: SizedExp se => Size se (a -> [a -> x] -> [x])
+mlist = bind (Abs 0 $ AAbs 1 2 $ List (Var 1) (Abs 3 $ Var 2 `App` Var 3 `App` Var 0)) 
+    $ \x l -> match l nil (\f fs -> cons `app` (f `app` x) `app` (mlist `app` x `app` fs))
+
+strange :: (SizedExp se) => Size se ([Int] -> [Int])
+strange = bind (AAbs 0 1 $ List (Num 2) (Abs 2 Unsized)) $ \l1 ->
+    let b = match l1 nil (\x1 l2 -> match l2 nil (\x2 l3 ->  cons `app` x2 `app` (cons `app` x1 `app` nil)))
+    in match b (cons `app` 0 `app` (cons `app` 0 `app` nil)) (\x xs -> b)
+
+
+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))))) $
+    \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))$
+    \l1 l2 -> match l1 l2 (
+        \x xs -> match l2 l1 (
+                \y ys -> iff (x>y) (cons `app` x `app` (merge `app` xs `app` l2))
+                                  (cons `app` y `app` (merge `app` l1 `app` ys))
+            )
+        )
+
+split1 :: SizedExp se => Size se ([Int] -> [Int])
+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)) $
+    \z -> match z nil (\y ys -> split1 `app` ys)
+
+ms = (AAbs 0 1 $ List (Var 0) (Abs 4 $ Unsized))
+mergesort :: SizedExp se => Size se ([Int] -> [Int])
+mergesort = bind ms $
+    \l -> match l nil (\x xs ->
+        merge `app` (mergesort `app` (split1 `app` l)) `app` (mergesort `app` (split2 `app` l))
+    )
+
+last :: SizedExp se => Size se ([a] -> a)
+last = bind (AAbs 0 1 $ App (Var 1) (Num 0)) $
+    \l -> match l true (\x xs -> match xs x (\_ _ -> last `app` xs))
+
+charm :: SizedExp se => Size se (([a] -> [a]) -> a)
+charm = bind (Abs 0 $ App (AAbs 2 3 $ App (Var 3) (Num 0)) (App (Var 0) (List (Num 0) $ Abs 1 Bottom))) $
+    \ f -> last `app` (f `app` nil)
+
+fix :: SizedExp se => Size se ((a -> a) -> a)
+fix = bind (Abs 2 $ App y (Var 2)) $ 
+    \f -> f `app` (fix `app` f)
+
+transpose :: SizedExp se => Size se ([[a]] -> [[a]])
+transpose = bind transposec $ \l -> match l true $
+    \l1 xss -> match l1 true $
+        \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 ) 
+    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)) )
+comp :: (SizedExp se)  => Size se ( (b->c) -> (a->b) -> a->c )
+comp = bind comps $ \f g x -> f `app` (g `app` x)
+
+data TestCase = forall a . TestCase P.String (forall se. SizedExp se => Size se a)
+
+tests :: [TestCase]
+tests = [
+          TestCase "append" append 
+        , TestCase "reverse" reverse 
+        , TestCase "heads" heads 
+        , TestCase "map" map 
+        , TestCase "pam" pam
+        , TestCase "head" head
+        , TestCase "tail" tail
+        , TestCase "t3" t3
+        , TestCase "t9" t9
+--        , TestCase "t9_" t9_  -- too few arguments in definition
+        , TestCase "t27" t27
+        , TestCase "t27_" t27_
+        , TestCase "t27__" t27__
+        , TestCase "addone" addone
+        , TestCase "add3" add3
+--        , TestCase "add3_" add3_ -- too few arguments in definition
+        , TestCase "add27" add27
+        , TestCase "zipWith" zipWith
+        , TestCase "appAll" appAll
+        , TestCase "conspack" conspack
+        , TestCase "scalar_prod" scalar_prod
+        , TestCase "sqdiff" sqdiff
+        , TestCase "mlist" mlist
+        , TestCase "strange" strange
+        , TestCase "take4" take4
+        , TestCase "charm" charm
+        , TestCase "comp" comp
+    ]
+
+runTests = do
+    failed <- M.forM tests $ \(TestCase name test) -> do
+        P.print$ " +++++++++++++++++++++++++++++++"
+        P.print$ " +  Proving " P.++ name
+        P.print$ " +++++++++++++++++++++++++++++++"
+
+        s <- prove test
+        if P.not s then
+            M.return [name]
+        else
+            M.return []
+
+    let f = P.concat failed
+    if List.null f then 
+        P.putStrLn "All ok."
+    else do
+        P.putStr $ "\n\nFailed test cases: "
+        P.putStrLn $ List.intercalate ", " f
Index: /sizechecking/Lambda.hs
===================================================================
--- /sizechecking/Lambda.hs	(revision 5)
+++ /sizechecking/Lambda.hs	(revision 5)
@@ -0,0 +1,244 @@
+module Lambda where
+
+{- 
+   Ez a cikkben megadott lambda kalkulus egy implementacioja + redukcio + peldak.
+
+   Hasznalat: lasd Lambda_proof.hs
+
+ -}
+import Data.List
+import qualified Data.Set as Set
+import Data.Char
+
+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
+    deriving Eq
+
+showVar x = if x>28 
+    then showVar (x `div` 29) . (showChar $ chr $ ord 'a' + (x `mod` 29))
+    else showChar $ chr $ ord 'a' + x
+
+getPrec :: Char -> (Int,Int,Int)
+getPrec '+' = (4,4,5)
+getPrec '-' = (4,4,5)
+getPrec '*' = (5,5,6)
+getPrec '/' = (5,5,6)
+
+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 (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 p (Op m op n) = showParen (p>prec) $ showsPrec lprec m . showChar op . showsPrec rprec n
+        where (prec,lprec,rprec)=getPrec op
+    showsPrec p (List s f) = showParen (p>0) $ showString "List " . showsPrec 9 s . showChar ' ' . showsPrec 9 f
+    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
+
+t3s = Abs 1 $ Abs 0 $ App t (App t (App t x))
+    where t = Var 1
+          x = Var 0
+
+subs (App x z)   var exp = App (subs x var exp) (subs z var exp)
+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
+                         | otherwise = e
+subs x@(Abs v e) var exp | v==var    = x
+                         | otherwise = Abs v (subs e var exp)
+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
+
+
+alpha (App x z)   from to = App (alpha x from to) (alpha z from to)
+alpha (List x z)  from to = List (alpha x from to) (alpha z from to)
+alpha (Op x c z)  from to = Op (alpha x from to) c (alpha z from to)
+alpha (Shift x y z) from to = Shift (alpha x from to) (alpha y from to) (alpha z from to)
+alpha e@(Var _)   _    _  = e
+alpha e@(Num _)   _    _  = e
+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' (App x z)   from to = App (alpha' x from to) (alpha' z from to)
+alpha' (List x z)  from to = List (alpha' x from to) (alpha' z from to)
+alpha' (Op x c z)  from to = Op (alpha' x from to) c (alpha' z from to)
+alpha' (Shift x y z) from to = Shift (alpha' x from to) (alpha' y from to) (alpha' z from to)
+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' x@(Num _)   _    _  = x
+alpha' x@Bottom   _    _  = x
+alpha' x@Unsized   _    _  = x
+
+fv (Var x) = Set.singleton x
+fv (App x y) = fv x `Set.union` fv y
+fv (Op x _ y) = fv x `Set.union` fv y
+fv (Abs v e) = v `Set.delete` fv e 
+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 (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 (App x y) = bv x `Set.union` bv y
+bv (Op x _ y) = bv x `Set.union` bv y
+bv (List x y) = bv x `Set.union` bv y
+bv (Abs v e) = v `Set.insert` bv e
+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 Unsized = Set.empty
+bv Bottom = Set.empty
+
+maxv (Var x)   = x
+maxv (Num i)   = 0
+maxv Unsized = 0
+maxv Bottom = 0
+maxv (App x y) = maxv x `max` maxv y
+maxv (Op x _ y) = maxv x `max` maxv y
+maxv (Shift x y z) = maxv x `max` maxv y `max` maxv z
+maxv (List x y) = maxv x `max` maxv y
+maxv (Abs v e) = v `max` maxv e
+maxv (AAbs v1 v2 e) = v1 `max` v2 `max` maxv e
+
+rsubs oexp var exp = subs renamed var exp
+    where
+    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
+    
+
+reduce (App (Abs var exp) z) = return $ rsubs exp var z
+reduce (App (AAbs s f exp) (List s' f')) = return $ rsubs (App (Abs f exp) f') s s'
+reduce (App e f) = case reduce e of
+        Just e' -> return $ App e' f
+        _       -> reduce f >>= \f' -> return $ App e f'
+reduce (Abs v e) = reduce e >>= \e' -> return $ Abs v e'
+reduce (Var _) = Nothing
+reduce (Num _) = Nothing
+reduce (List e f) = case reduce e of
+        Just e' -> return $ List e' f
+        _       -> reduce f >>= \f' -> return $ List e f'
+reduce (AAbs v1 v2 e) = reduce e >>= \e' -> return $ AAbs v1 v2 e'
+reduce Unsized = Nothing
+reduce Bottom  = Nothing
+reduce (Shift e1 e2 e3) = case reduce e1 of
+        Just e' -> return $ Shift e' e2 e3
+        _       -> case reduce e2 of
+            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
+    '-' | (Num i, Num j) <- (m,n) -> return $ Num $ i-j
+    '*' | (Num i, Num j) <- (m,n) -> return $ Num $ i*j
+    '+' | (Num 0) <- m            -> reduce n
+    '+' | (Num 0) <- n            -> reduce m
+    '*' | (Num 0) <- m            -> return $ Num 0
+    '*' | (Num 0) <- n            -> return $ Num 0
+    '*' | (Num 1) <- m            -> reduce n
+    '*' | (Num 1) <- n            -> reduce m
+    '-' | (Num 0) <- n            -> reduce m
+    _ ->  case reduce m of
+        Just m' -> return $ Op m' c n
+        _       -> reduce n >>= \n' -> return $ Op m c n'
+
+r :: Maybe L -> Maybe L
+r x = x >>= reduce 
+
+it f x = it' f (Just x)
+    where
+    it' f Nothing  = []
+    it' f (Just x) = x:it' f (f x)
+
+rchain :: L -> [L]
+rchain exp = it reduce exp
+
+pchain = putStrLn . intercalate "\n-> " . map show . rchain
+
+lplus = Abs m $ Abs n $ Abs f $ Abs x $ App (App (Var m) (Var f)) $ App (App (Var n) (Var f)) (Var x)
+    where [m,n,f,x] = [0..3]
+lzero = Abs f $ Abs x $ Var x
+    where [f,x] = [0,1]
+lsucc = Abs n $ Abs f $ Abs x $ App (Var f) $ App (App (Var n) (Var f)) (Var x)
+    where [n,f,x] = [0..2]
+lone = last $ it reduce $ App lsucc lzero
+ltwo = last $ it reduce $ App lsucc lone
+
+lpred = Abs n $ Abs f $ Abs x $ App (App (App (Var n) u1) (Abs u $ Var x)) (Abs u $ Var u)
+    where 
+    u1 = Abs g $ Abs h $ App (Var h) $ App (Var g) (Var f)
+    [n,f,x,g,h,u] = [0..5]
+    
+lsub = Abs m $ Abs n $ App (App (Var n) lpred) (Var m)
+    where (m,n) = (0,1)
+
+ltrue = Abs 0 $ Abs 1 $ Var 0
+lfalse = Abs 0 $ Abs 1 $ Var 1
+
+liszero = Abs n $ App (App (Var n) (Abs x $ lfalse)) ltrue
+    where (n,x) = (0,1)
+
+land = Abs 0 $ Abs 1 $ App (App (Var 0) (Var 1)) (Var 1)
+lleq = Abs 0 $ Abs 1 $ App liszero $ App (App lsub (Var 0)) (Var 1)
+leq = Abs 0 $ Abs 1 $ App (App land l1) l2
+    where
+    l1 = App (App lleq (Var 0)) (Var 1)
+    l2 = App (App lleq (Var 1)) (Var 0)
+
+test = Abs 0 $ Abs 1 $ App (App leq xpy) ypx
+xpy = App (App lplus (Var 0)) (Var 1)
+ypx = App (App lplus (Var 1)) (Var 0)
+
+smap  = Abs 5 $ AAbs 18 6 $ List (Var 18) (Abs 8$ App (Var 5) (App (Var 6) (Var 8)))
+conss = Abs 23 $ AAbs 19 5 $ List (Op (Num 1) '+' (Var 19)) $ Shift (Var 5) (Var 19)  (Abs 8 $ Var 23)
+addones = AAbs 19 5 $ List (Op (Num 1) '+' (Var 19)) (Abs 8 Unsized)
+nils = List (Num 0) (Abs 8 Bottom)
+lz n = List (Num n) (Abs 8 Unsized)
+srep n x = List (Num n) (Abs 8 x)
+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)))
+-- Î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
+    [] -> []
+    (x:xs) -> x:reverse' xs
+appends = AAbs 18 5 $ AAbs 19 6 $ List (Op (Var 18) '+' (Var 19)) $ Shift (Var 6) (Var 19) (Var 5)
+
+headc = AAbs 18 5 $ App (Var 5) (Op (Var 18) '-' (Num 1))
+tailc = AAbs 18 5 $ List (Op (Var 18) '-' (Num 1)) (Var 5)
+rall = last . it reduce 
+
+sheads = rall $ App smap headc
+stails = rall $ App smap tailc
Index: /sizechecking/NC.hs
===================================================================
--- /sizechecking/NC.hs	(revision 5)
+++ /sizechecking/NC.hs	(revision 5)
@@ -0,0 +1,28 @@
+
+{- Constraints -}
+newtype Term = Term [String]
+    deriving (Show, Eq, Ord)
+nullterm = Term []
+newtype Arithmetics = Arithmetics (Map Term Int)
+    deriving (Show, Eq)
+
+termmul (Term a) (Term b) = Term $ termmul' a b
+    where
+    termmul' []        l         = l
+    termmul' l         []        = l
+    termmul' l1@(x:xs) l2@(y:ys) = if x<y then x:termmul' xs l2
+                                          else y:termmul' l1 ys
+
+instance Num Arithmetics where
+    fromInteger l = Arithmetics $ singleton nullterm $ fromInteger l
+    (Arithmetics a) + (Arithmetics b) = Arithmetics $ unionWith (+) a b
+    (Arithmetics a) * (Arithmetics b) = Arithmetics amul
+        where
+        amul = foldrWithKey tmul empty a
+        tmul :: Term -> Int -> Map Term Int -> Map Term Int
+        tmul t1 v1 val = unionWith (+) val (mapKeys (termmul t1) $ M.map (*v1) b)
+    abs = undefined
+    signum = undefined
+
+data Condition = ZC Arithmetics | LTC Arithmetics Arithmetics | GEC Arithmetics Arithmetics
+    deriving (Show)
Index: /sizechecking/README.html
===================================================================
--- /sizechecking/README.html	(revision 5)
+++ /sizechecking/README.html	(revision 5)
@@ -0,0 +1,89 @@
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml">
+<head>
+  <meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
+  <meta http-equiv="Content-Style-Type" content="text/css" />
+  <meta name="generator" content="pandoc" />
+  <title></title>
+</head>
+<body>
+<h2 id="prerequisites">Prerequisites</h2>
+<p>You need at least version 2011.4.0.0 of haskell platform and the package value-supply. If you have haskell platform installed you can install value-supply by typing</p>
+<pre><code>cabal install value-supply</code></pre>
+<h2 id="source-files">Source files</h2>
+<dl>
+<dt>Examples.hs</dt>
+<dd>Some examples
+</dd>
+<dt>SizedExp.hs</dt>
+<dd>Embedded language to prove size expressions
+</dd>
+<dt>Lambda.hs</dt>
+<dd>Size expressions
+</dd>
+<dt>Constraints.hs</dt>
+<dd>Constraint solver
+</dd>
+</dl>
+<h2 id="using-the-examples">Using the examples</h2>
+<pre><code>$ ghci Examples.hs 
+GHCi, version 7.0.4: http://www.haskell.org/ghc/  :? for help
+Loading package ghc-prim ... linking ... done.
+Loading package integer-gmp ... linking ... done.
+Loading package base ... linking ... done.
+Loading package ffi-1.0 ... linking ... done.
+[1 of 4] Compiling Lambda           ( Lambda.hs, interpreted )
+[2 of 4] Compiling Constraints      ( Constraints.hs, interpreted )
+[3 of 4] Compiling SizedExp         ( SizedExp.hs, interpreted )
+[4 of 4] Compiling Main             ( Examples.hs, interpreted )
+Ok, modules loaded: Lambda, SizedExp, Constraints, Main.
+*Main&gt; </code></pre>
+<p>Type â<code>runTests</code>â to run all test cases or type â<code>prove map</code>â to prove the function named map.</p>
+<h2 id="under-windows">Under Windows</h2>
+<p>It is not perfect, and you will see a box after every special character, but at least it works.</p>
+<ul>
+<li>Open a console by running the program <code>cmd</code></li>
+<li>Issue the command <code>chcp 65001</code></li>
+<li>In the console cd to the trunk directory</li>
+<li>Now, you can run <code>ghci Examples.hs</code></li>
+</ul>
+<h2 id="introduction-to-haskell-syntax">Introduction to Haskell syntax</h2>
+<p>Haskell syntax is very much like Clean, however there are some expressions you cannot find in Clean.</p>
+<h3 id="backtick">Backtick</h3>
+<p>Every haskell function can be used as infix operator. For example the following two expressions are the same.</p>
+<pre><code>func a b
+a `func` b</code></pre>
+<h3 id="dollar">Dollar</h3>
+<p>Dollar sign is just explicit application (but with different precedence), so it can be used as a backward pipe operator. The following expressions are the same.</p>
+<pre><code>func (a b)
+func $ a b</code></pre>
+<h2 id="the-embedded-language">The Embedded Language</h2>
+<p>As an example the function <code>map</code> is examined.</p>
+<pre><code>1 smap  = Abs 5 $ AAbs 18 6 $ List (Var 18) (Abs 8$ App (Var 5) (App (Var 6) (Var 8)))
+2 map :: (SizedExp se)  =&gt; Size se ( (a-&gt;b) -&gt; [a] -&gt; [b] )
+3 map = bind smap body
+4     where body f l = match l (nil)
+5             ( \x xs -&gt;  cons `app` (f `app` x) `app` (map `app` f `app` xs ))</code></pre>
+<p>Here line 3 tells us map is a top-level binding, where the body of the function is defined in line 4â5 and its size expression is in line 1. Unfortunately the size expression language has not yet been embedded, so it is a bit difficult to read. Type <code>smap</code> in the GHC console to get a pretty printed form.</p>
+<pre><code>*Main&gt; smap
+Î»f.Îs,g.List s (Î»i.f (g i))</code></pre>
+<p>The type of the function tells us the underlying type, ie. <code>(a-&gt;b) -&gt; [a] -&gt; [b]</code>.</p>
+<p>The body of map corresponds to the following expression</p>
+<pre><code>match l of
+   nil       -&gt; nil
+   cons x xs -&gt; cons (f x) (map f xs)</code></pre>
+<p>In the embedded language <code>bind</code>, <code>match</code> and <code>app</code> are supercombinators.</p>
+<dl>
+<dt><code>bind sexp exp</code></dt>
+<dd><p>combines a size and an expression and creates a top-level binding</p>
+</dd>
+<dt><code>match list nilexp consexp</code></dt>
+<dd><p>embedding of the match operator of our language to haskell</p>
+</dd>
+<dt><code>app exp1 exp2</code></dt>
+<dd><p>embedding of the function application of our language to haskell</p>
+</dd>
+</dl>
+<p>There is also a function called <code>true</code> to denote we do not want to prove that branch.</p>
+</body>
+</html>
Index: /sizechecking/README.txt
===================================================================
--- /sizechecking/README.txt	(revision 5)
+++ /sizechecking/README.txt	(revision 5)
@@ -0,0 +1,135 @@
+Prerequisites
+-------------
+
+You need at least version 2011.4.0.0 of haskell platform and the package
+value-supply. If you have haskell platform installed you can install
+value-supply by typing 
+
+	cabal install value-supply
+
+
+Source files
+------------
+
+Examples.hs
+  ~ Some examples
+SizedExp.hs
+  ~ Embedded language to prove size expressions
+Lambda.hs
+  ~ Size expressions
+Constraints.hs
+  ~ Constraint solver
+
+Using the examples
+------------------
+
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+$ ghci Examples.hs 
+GHCi, version 7.0.4: http://www.haskell.org/ghc/  :? for help
+Loading package ghc-prim ... linking ... done.
+Loading package integer-gmp ... linking ... done.
+Loading package base ... linking ... done.
+Loading package ffi-1.0 ... linking ... done.
+[1 of 4] Compiling Lambda           ( Lambda.hs, interpreted )
+[2 of 4] Compiling Constraints      ( Constraints.hs, interpreted )
+[3 of 4] Compiling SizedExp         ( SizedExp.hs, interpreted )
+[4 of 4] Compiling Main             ( Examples.hs, interpreted )
+Ok, modules loaded: Lambda, SizedExp, Constraints, Main.
+*Main> 
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Type "`runTests`" to run all test cases or type "`prove map`" to prove the
+function named map.
+
+Under Windows
+-------------
+It is not perfect, and you will see a box after every special character, but at
+least it works.
+
+ - Open a console by running the program `cmd`
+ - Issue the command `chcp 65001`
+ - In the console cd to the trunk directory
+ - Now, you can run `ghci Examples.hs`
+
+
+Introduction to Haskell syntax
+------------------------------
+
+Haskell syntax is very much like Clean, however there are some expressions you
+cannot find in Clean.
+
+### Backtick ###
+
+Every haskell function can be used as infix operator. For example the
+following two expressions are the same.
+
+~~~~~~~~~~~
+func a b
+a `func` b
+~~~~~~~~~~~
+
+### Dollar ###
+
+Dollar sign is just explicit application (but with different precedence), so it
+can be used as a backward pipe operator. The following expressions are the
+same.
+
+~~~~~~~~~~~~~~
+func (a b)
+func $ a b
+~~~~~~~~~~~~~~
+
+
+
+The Embedded Language
+---------------------
+
+As an example the function `map` is examined.
+
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+1 smap  = Abs 5 $ AAbs 18 6 $ List (Var 18) (Abs 8$ App (Var 5) (App (Var 6) (Var 8)))
+2 map :: (SizedExp se)  => Size se ( (a->b) -> [a] -> [b] )
+3 map = bind smap body
+4     where body f l = match l (nil)
+5             ( \x xs ->  cons `app` (f `app` x) `app` (map `app` f `app` xs ))
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Here line 3 tells us map is a top-level binding, where the body of the function is
+defined in line 4--5 and its size expression is in line 1. Unfortunately the
+size expression language has not yet been embedded, so it is a bit difficult to
+read. Type `smap` in the GHC console to get a pretty printed form.
+
+~~~~~~~~~~~~~~~~~
+*Main> smap
+Î»f.Îs,g.List s (Î»i.f (g i))
+~~~~~~~~~~~~~~~~~
+
+The type of the function tells us the underlying type, ie. `(a->b) -> [a] -> [b]`.
+
+The body of map corresponds to the following expression
+
+~~~~~~~~~~~~~~~~~~~~~~~
+match l of
+   nil       -> nil
+   cons x xs -> cons (f x) (map f xs)
+~~~~~~~~~~~~~~~~~~~~~~~
+
+
+In the embedded language `bind`, `match` and `app` are supercombinators.
+
+`bind sexp exp`
+
+  : combines a size and an expression and creates a top-level binding
+
+`match list nilexp consexp`
+
+  : embedding of the match operator of our language to haskell
+
+`app exp1 exp2`
+
+  : embedding of the function application of our language to haskell
+
+There is also a function called `true` to denote we do not want to prove that
+branch.
+
+
Index: /sizechecking/SizedExp.hs
===================================================================
--- /sizechecking/SizedExp.hs	(revision 5)
+++ /sizechecking/SizedExp.hs	(revision 5)
@@ -0,0 +1,179 @@
+{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances,
+             IncoherentInstances, RankNTypes, ScopedTypeVariables,
+             FlexibleContexts,UndecidableInstances #-}
+
+module SizedExp  where
+--    (
+--        SizedExp(..), ($), unQ, prove
+--    ) where
+
+import Lambda as L 
+import Constraints 
+import Data.Supply
+
+
+class TS b => (Unify se a b)  where
+    unify :: (forall a b c. (TS c, Unify se a b) => c -> (Size se c -> a) -> (Size se (c -> b), d)) -> 
+        (b -> Size se b -> (Size se b, d)) -> 
+        a -> (Size se b, d)
+
+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
+
+instance (SizedExp se, se~se1, c1~c2, TS c2) => Unify se (Size se1 c1) c2 where
+    unify f g x = g undefined x
+
+class SizedExp (se :: * -> *) where
+    data Size se :: * -> *
+    true  :: Size se x
+    known  :: L -> Size se x
+    match :: Size se [l] -> Size se r -> (Size se l -> Size se [l] -> Size se r) ->  Size se r
+    bind  :: (Unify se a b) => L.L -> a -> Size se b
+    app   :: Size se (a->b) -> Size se a -> Size se b
+    iff   :: Bool -> Size se a -> Size se a -> Size se a
+    num   :: Integer -> Size se Int
+
+instance Show (Size se a) where
+    show (==) = error "no show on Size!"
+instance Eq (Size se a) where
+    (==) = undefined
+instance (SizedExp se) => Num (Size se Int) where
+    fromInteger = num
+    x + y = num 0
+    x * y = num 0
+    abs = undefined
+    signum = undefined
+instance (SizedExp se) => Ord(Size se Int) where
+
+{-
+ - Implementation of constraints
+ -}
+sizeof :: Size Q a -> IO [SExp]
+sizeof (QSynt s)       = s
+sizeof (QProvable l _) = return [([], l)]
+
+fresh :: TypeKind -> Supply Int -> L
+fresh sig var = fresh' sig [] var
+    where 
+    fresh' U _ _ = Unsized
+    fresh' V l var = appall (supplyValue var) l
+    fresh' (F _ b) l var = Abs i $ fresh' b (Var i:l) v2
+        where
+        (v1,v2) = split2 var
+        i = supplyValue v1
+    fresh' (L a) l var = List (appall i l) (Abs j $ fresh' a (Var j:l) v3)
+        where
+        (v1,v2,v3) = split3 var
+        i = supplyValue v1
+        j = supplyValue v2
+
+
+freshvars2 :: (TS b, Unify Q (Size Q a) a) => Supply Int -> b -> Size Q a -> (Size Q a, L -> L)
+freshvars2 supply q exp = (exp , id)
+
+freshvars :: (TS c, Unify Q a b) => Supply Int -> c -> (Size Q c -> a) -> (Size Q (c -> b), L -> L)
+freshvars supply q = freshvars' (unify (freshvars s1) (freshvars2 s2)) 
+    where 
+    (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)
+        where
+        (x, f) = u $ exp $ QSynt $ do 
+            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))
+
+concatMapM :: (a -> IO [b]) -> [a] -> IO [b]
+concatMapM f l = mapM f l >>= return.concat
+    
+type SExp = ([Constraint], L)
+newtype Q a = Q { unQ :: () }
+instance SizedExp Q where
+    data Size Q a = QSynt (IO [SExp]) | QProvable L (Supply Int -> IO [Condition]) 
+    known l = QSynt $return [([], l)]
+    true = QSynt $ return []
+    match l nil cons = let
+            match1 (cond, ltype) = do
+                    x <- sizeof l
+                    putStrLn $ "ORIGINAL is " ++ (show x)
+                    putStrLn $ "[MATCH] ==> " ++ (show $ ltype)
+                    let lt = rall$  App (AAbs 18 5 $ Var 18) ltype
+                    putStrLn $ " --- NIL  ---" ++ (show lt)
+                    nils <- sizeof nil
+                    putStrLn $ show 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)
+                    conss <- sizeof $ cons (QSynt$return [([], tx)]) (QSynt$return [([], txs)])
+                    print conss
+                    let consc = foldr addConstraint conss $ lt `GEC` Num 1:cond
+                    print "END MATCH"
+                    print  $ nilc ++ consc
+                    return $ nilc ++ consc
+        in QSynt $ sizeof l >>= concatMapM match1 
+
+    iff _ l1 l2 = QSynt $ do 
+        ll1 <- sizeof l1
+        ll2 <- sizeof l2
+        return $ ll1 ++ ll2
+
+    app l1 l2 = QSynt $ do
+            ll1 <- sizeof l1
+            ll2 <- sizeof l2
+            return  [ (c1 ++ c2,  App e1 e2) | (c1,e1) <- ll1, (c2,e2) <- ll2]
+
+    bind l exp = z $ \supply -> let (s1,s2) = split2 supply in unify (freshvars s1) (freshvars2 s2) exp
+        where
+        z :: (Supply Int -> (Size Q c, L -> L)) -> Size Q c
+        z x = QProvable l $ \supply -> let
+                (sexp, f) = x supply
+                ll = rall $ f l
+                rr (Zero a) = Zero $ rall a
+                rr (GEC a b) = rall a `GEC` rall b
+                rr (LTC a b) = rall a `LTC` rall b
+            in do 
+                l3 <- sizeof sexp 
+                print l
+                print ll
+                return $ map (\(c,l2) -> Condition (map rr c) ll (rall l2)) l3
+
+    num n = QSynt $return [([], Unsized)]
+
+instance Num (Size Q Int) where
+    (+) = undefined
+    (*) = undefined
+    abs = undefined
+    signum = undefined
+    fromInteger = num
+
+prove :: Size Q b -> IO (Bool)
+prove (QProvable l x) = do
+    (s1,s2,s3) <- newSupply 30 (+1) >>= return.split3
+    c <- x s1
+    putStrLn ""
+    putStrLn "------------"
+    putStrLn "Conditions: "
+    print c
+    putStrLn ""
+    putStrLn "------------"
+    putStrLn "Equations: "
+    x <- checkCond s2 c
+    print x
+    putStrLn ""
+    putStrLn "------------"
+    putStrLn "Solving: "
+    y <- solve x s3
+    putStrLn ""
+    if null y then do
+        putStrLn "QED"
+        return True
+    else do
+        putStrLn "------------"
+        putStrLn "Cannot prove: "
+        print y
+        return False
+
