Index: /sizechecking/L.hs
===================================================================
--- /sizechecking/L.hs	(revision 7)
+++ /sizechecking/L.hs	(revision 8)
@@ -3,5 +3,5 @@
 import Data.Char(ord, chr)
 import Control.Monad.State
-import Data.Supply
+--import Data.Supply
 
 data OpName = PLUS | MINUS | MUL
@@ -10,7 +10,9 @@
 
 {- Lambda calculus without free variables -}
+type Arr repr a b = repr a -> repr b
+
 class Lambda l where
-    labs    :: (l a -> l b) -> l (a -> b)
-    app     :: l (a -> b) -> l a -> l b
+    labs    :: (l a -> l b) -> l (Arr l a b)
+    app     :: l (Arr l a b) -> l a -> l b
     lit     :: Int -> l Int
     op      :: l Int -> OpName -> l Int -> l Int
@@ -18,7 +20,7 @@
 class SizeExp l where
     type List l :: * -> *
-    list    :: l Int -> l (Int -> b) -> l (List l b)
-    aabs    :: (l Int -> l (Int -> a) -> l b) -> l (List l a -> b)
-    shift   :: l (Int -> a) -> l Int -> l (Int -> a) -> l (Int -> a)
+    list    :: l Int -> l (Arr l Int b) -> l (List l b)
+    aabs    :: (l Int -> l (Arr l Int a) -> l b) -> l (Arr l (List l a) b)
+    shift   :: l (Arr l Int a) -> l Int -> l (Arr l Int a) -> l (Arr l Int a)
     undef   :: l Bottom
     unsized :: l ()
@@ -33,8 +35,8 @@
 
 {- Printing -}
-newtype LPrint a = LPrint { unPrint :: Int -> State Int ShowS }
+newtype LPrint a = LPrint { unPrint :: Int -> Int -> ShowS }
 
 instance Lambda LPrint where
-  lit x      = LPrint $ \p -> return $ shows x
+  lit x      = LPrint $ \_ -> return $ shows x
   op m opc n = LPrint $ \p -> do
     let (prec, lprec, rprec, c) = getPrec opc
@@ -46,19 +48,17 @@
     l2 <- unPrint v 7
     return $ showParen (p>6) $ l1 . showChar ' ' . l2
-  labs e      = LPrint $ \p -> do
-    v <- getVar
-    let var = LPrint $ \_ -> return $ showVar v
-    l <- unPrint (e var) 0 
-    return $ showParen (p>0) $ showChar 'λ' . showVar v . showChar '.' . l
+  labs e      = LPrint $ \p v -> let
+    var = LPrint $ \_ -> return $ showVar v
+    l = unPrint (e var) 0 $ succ v
+    in showParen (p>0) $ showChar 'λ' . showVar v . showChar '.' . l
 
 instance SizeExp LPrint where
   type List LPrint = []
-  aabs f   = LPrint $ \p -> do
-    v1 <- getVar
-    v2 <- getVar
-    let var1 = LPrint $ \_ -> return $ showVar v1
-        var2 = LPrint $ \_ -> return $ showVar v2
-    l <- unPrint (f var1 var2) 0
-    return $ showParen (p>0) $ showChar 'Λ' . showVar v1 . showChar ',' . showVar v2 . showChar '.' . l
+  aabs f   = LPrint $ \p v -> let 
+    v2 = succ v
+    var1 = LPrint $ \_ _ -> showVar v
+    var2 = LPrint $ \_ _ -> showVar v2
+    l = unPrint (f var1 var2) 0 (v+2)
+    in showParen (p>0) $ showChar 'Λ' . showVar v . showChar ',' . showVar v2 . showChar '.' . l
   list s f = LPrint $ \p -> do
     l1 <- unPrint s 9
@@ -73,5 +73,8 @@
   unsized = LPrint $ \_ -> return $ showChar 'U'
 
-mprint x = putStrLn $ (fst $ runState (unPrint x 0) 0) ""
+view :: LPrint a -> LPrint a
+view = id
+instance Show (LPrint a) where
+    showsPrec _ e = unPrint e 0 0
 
 showVar x = if x>28 
@@ -105,6 +108,6 @@
 newtype R a = R { unR :: a }
 instance Lambda R where
-  labs f      = R $ unR . f . R
-  app e1 e2   = R $ (unR e1) (unR e2)
+  labs f      = R $ f 
+  app e1 e2   = (unR e1) e2
   lit i       = R i
   op e1 op e2 = let opm = case op of
@@ -115,6 +118,6 @@
 
 newtype RList a = RList { unList :: (Int, Int -> a)  }
-instance (Show a) => Show (RList a) where
-  show (RList (s,f)) = show (map f [0..s-1])
+--instance (Show a) => Show (RList a) where
+--  show (RList (s,f)) = show (map f [0..s-1])
 
 instance SizeExp R where
@@ -122,28 +125,79 @@
   undef       = R $ Bottom
   unsized     = R $ ()
-  list s f    = R $ RList (unR s, unR f)
-  aabs e      = R $ \(RList (s,f)) -> unR (e (R s) (R f))
-  shift a s c = R $ \i -> if i<(unR s) then unR a i else unR c i
-
-{- Create a restricted deep embedding to work with the expression -}
-
-{- sized [a] to prove -}
-data Nil
-data Cons a
-data SLInt a where
-  SLNil  :: SLInt Nil
-  SLCons :: Int -> SLInt a -> SLInt (Cons a)
-
-class MGS a where
-  mgs :: Supply Int -> a -> a
-  mgs = mgs' []
-  mgs' :: [Int] -> Supply Int -> a -> a
-
-
-instance MGS () where
-  mgs' _ _ _ = ()
-instance MGS a => MGS (RList a) where
-  mgs' bound supp  _ = RList undefined
-    where
-    (s1, s2, s3) = split3 supp
-    listsize = mgs' bound supp (undefined :: a)
+  list s f    = R $ RList (unR s, unR . (unR f) . R )
+--aabs    :: Arr l Int (Arr l (Arr l Int a) b) -> l (Arr l (List l a) b)
+--  aabs e      = R $ \(RList (s,f)) -> unR (e (R s) (R f))
+--  shift a s c = R $ \i -> if i<(unR s) then unR a i else unR c i
+
+-- Type level int to count arity
+data Zero
+data Succ a
+
+data Exp a where
+    Lit :: Int -> Exp Zero
+    Op  :: Exp Zero -> OpName -> Exp Zero -> Exp Zero
+    App :: Exp (Succ a) -> Exp Zero -> Exp a
+    Var :: Int -> Exp a
+
+instance Show (Exp a) where
+    showsPrec _ (Lit a)         = shows a
+    showsPrec p (Op lhs op rhs) =
+        let (prec, lprec, rprec, c) = getPrec op
+        in showParen (p>prec) $  showsPrec lprec lhs . showChar c . showsPrec rprec rhs
+    showsPrec p (App lhs rhs)   =
+        showParen (p>6) $ showsPrec 6 lhs . showChar ' ' . showsPrec 7 rhs
+    showsPrec _ (Var i)         = showVar i
+
+type IntExp = Exp Zero
+data Condition = Eq IntExp IntExp | Gt IntExp IntExp | Lt IntExp IntExp
+type SExp = ([Condition], IntExp)
+newtype Compile a = Compile { unCompile :: SExp }
+
+--instance Lambda Compile where
+--  labs :: (l a -> l b) -> l (a -> b)
+--    labs f = Compile $ f
+
+
+--{- Create a restricted deep embedding to work with the expression -}
+--{- sized [a] to prove -}
+--
+--class Restricted a where
+--    kind :: a -> Int
+--
+--instance Restricted Int where
+--    kind _ = 0
+--
+--instance Restricted a => Restricted (Int -> a) where
+--    kind _ = succ $ kind $ (undefined :: a)
+--
+--class Var l where
+--    var :: Restricted a => Int -> l a
+--
+--showVar2 x = showChar '_' . showVar x
+--
+--newtype Count a = C { count :: Int }
+--cnv :: Restricted a => Count a -> a
+--cnv = undefined
+--
+--ckind :: (Restricted a) => Count a -> Int
+--ckind = kind . cnv
+--
+--instance Var Count where
+--    var _ = undefined
+--
+--instance Var LPrint where
+--    var x = LPrint $ \_ -> return $ showVar2 x
+--
+--class MGS a where
+--  mgs :: Supply Int -> a -> a
+--  mgs = mgs' []
+--  mgs' :: [Int] -> Supply Int -> a -> a
+--
+--instance MGS () where
+--  mgs' _ _ _ = ()
+--
+--instance MGS a => MGS (RList a) where
+--  mgs' bound supp  _ = RList (listsize, undefined)
+--    where
+--    (s1, s2, s3) = split3 supp
+--    listsize = mgs' bound supp (undefined :: a)