Index: sizechecking/branches/macs/Exp.hs
===================================================================
--- sizechecking/branches/macs/Exp.hs	(revision 22)
+++ sizechecking/branches/macs/Exp.hs	(revision 22)
@@ -0,0 +1,8 @@
+module Exp where
+
+import Size
+
+class Exp l where
+    nil :: l [a]
+    cons :: l a -> l [a] -> l [a]
+    match :: l [a] -> l b -> l (a -> [a] -> b) -> [b]
Index: sizechecking/branches/macs/Size.hs
===================================================================
--- sizechecking/branches/macs/Size.hs	(revision 22)
+++ sizechecking/branches/macs/Size.hs	(revision 22)
@@ -0,0 +1,47 @@
+module Size where
+
+import Lambda
+import Ops
+import Data.Supply as S
+
+data Unsized
+
+class (LOps l) => Size l where
+    list :: l Int -> l (Int -> a) -> l [a]
+    slam :: (l Int -> l (Int -> a) -> l b) -> l ([a] -> b)
+    shift :: l (Int -> a) -> l Int -> l (Int -> a) -> l (Int -> a)
+    unsized :: l Unsized
+    bottom :: l a
+
+instance Size S where
+    unsized = S $ \_ _ -> showChar 'U'
+    bottom = S $ \_ _ -> showChar '┴'
+    list size sexp = S $ \s p ->
+        let (s1, s2) = S.split2 s
+        in showParen (p>0) $
+            showString "List " .
+            unS size s1 9 .
+            showChar ' ' .
+            unS sexp s2 9
+    slam f = S $ \s p ->
+        let (s1, s2, s3) = S.split3 s
+            v1           = S.supplyValue s1
+            showV1       = S $ \_ _ -> showVar v1
+            v2           = S.supplyValue s2
+            showV2       = S $ \_ _ -> showVar v2
+        in showParen (p>0) $
+            showChar 'Λ' .
+            showVar v1 .
+            showChar ',' .
+            showVar v2 .
+            showChar '.' .
+            unS (f showV1 showV2) s3 0
+    shift e1 ss e2 = S $ \s p ->
+        let (s1, s2, s3) = S.split3 s
+        in showParen (p>0)
+        $ showString "Shift "
+        . unS e1 s1 2
+        . showChar ' '
+        . unS ss s2 2
+        . showChar ' '
+        . unS e2 s3 2
Index: sizechecking/branches/macs/SizedExp.hs
===================================================================
--- sizechecking/branches/macs/SizedExp.hs	(revision 22)
+++ sizechecking/branches/macs/SizedExp.hs	(revision 22)
@@ -0,0 +1,3 @@
+import Ops
+
+:e
Index: sizechecking/branches/macs/tests/ExpTest.hs
===================================================================
--- sizechecking/branches/macs/tests/ExpTest.hs	(revision 22)
+++ sizechecking/branches/macs/tests/ExpTest.hs	(revision 22)
@@ -0,0 +1,13 @@
+{-# LANGUAGE NoMonomorphismRestriction #-}
+
+module Tests.ExpTest where
+
+import Lambda
+import Exp
+import Ops
+import Prelude ( ($), Int, (==), return, sequence, (>>=), and, (.), IO, Bool )
+
+testNil :: Exp e => e [a]
+testNil = nil
+
+addOne :: Exp e => e [Int]
Index: sizechecking/branches/macs/tests/OpsTest.hs
===================================================================
--- sizechecking/branches/macs/tests/OpsTest.hs	(revision 21)
+++ sizechecking/branches/macs/tests/OpsTest.hs	(revision 22)
@@ -11,10 +11,34 @@
 test1 = app (lam $ \x -> const 3 + x) (const 2)
 
+test2 :: (LOps l) => l Int
+test2 = app (lam $ \x -> const 3 * x) (const 2)
+
+test3 :: (LOps l) => l Int
+test3 = app (lam $ \x -> const 2 * x + const 1) (const 5 - const 2)
+
+
 test1ast :: IO Bool
 test1ast = do
     t <- ast test1
     return $ t "" == "(λa.3+a) 2"
+
 test1eval :: IO Bool
 test1eval = return $ eval test1 == 5
+
+test2ast :: IO Bool
+test2ast = do
+    t <- ast test2
+    return $ t "" == "(λa.3*a) 2"
+
+test2eval :: IO Bool
+test2eval = return $ eval test2 == 6
+
+test3ast :: IO Bool
+test3ast = do
+    t <- ast test3
+    return $ t "" == "(λa.2*a+1) (5-2)"
+
+test3eval :: IO Bool
+test3eval = return $ eval test3 == 7
 
 tests :: [IO Bool]
Index: sizechecking/branches/macs/tests/SizeTest.hs
===================================================================
--- sizechecking/branches/macs/tests/SizeTest.hs	(revision 22)
+++ sizechecking/branches/macs/tests/SizeTest.hs	(revision 22)
@@ -0,0 +1,24 @@
+{-# LANGUAGE NoMonomorphismRestriction #-}
+
+module Tests.SizeTest where
+
+import Size
+import Lambda
+import Ops
+import Prelude ( ($), Int, (==), return, sequence, (>>=), and, (.), IO, Bool )
+
+testEmpty1 :: (Size l) => l [Unsized]
+testEmpty1 = list (const 0) (lam $ \_ -> unsized)
+
+testNil :: (Size l) => l [a]
+testNil = list (const 0) (lam $ \_ -> bottom)
+
+testHead :: (Size l) => l ([a] -> a)
+testHead = slam $ \s f -> f `app` (s - const 1)
+
+testTail :: (Size l) => l ([a] -> [a])
+testTail = slam $ \s f -> list (s - const 1) f
+
+testCons :: Size l => l (a -> [a] -> [a])
+testCons = lam $ \x -> slam $ \s f ->
+    list (s + const 1) $ shift f s (lam $ \_ -> x)