Index: sizechecking_branches/L.hs
===================================================================
--- sizechecking_branches/L.hs	(revision 10)
+++ sizechecking_branches/L.hs	(revision 15)
@@ -1,5 +1,6 @@
-{-# Language GADTs, FlexibleInstances, FlexibleContexts, MultiParamTypeClasses, FunctionalDependencies, ScopedTypeVariables, TypeFamilies, NoMonomorphismRestriction, OverlappingInstances #-}
+{-# Language GADTs, FlexibleInstances, FlexibleContexts, MultiParamTypeClasses, FunctionalDependencies, ScopedTypeVariables, TypeFamilies, NoMonomorphismRestriction, OverlappingInstances, IncoherentInstances #-}
 module L where
 
+import qualified Data.SBV as SBV
 import Data.Char(ord, chr)
 import Control.Monad.State
@@ -13,9 +14,10 @@
 type Arr repr a b = repr a -> repr b
 
-class Lambda l where
+class (Num (LInt l)) => Lambda l where
+    type LInt l :: *
     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
+    lit     :: (LInt l) -> l (LInt l)
+    op      :: l (LInt l) -> OpName -> l (LInt l) -> l (LInt l)
 
 class SizeExp l where
@@ -27,11 +29,5 @@
     unsized :: l ()
 
-instance Lambda l => Show (l a) where
-    showsPrec _ e = error "Error: no show"
-
-instance Lambda l => Eq (l a) where
-    (==) _ _ = error "Error: no eq"
-
-instance Lambda l => Num (l Int) where
+instance (Lambda l, LInt l ~ a) => Num (l a) where
     fromInteger = lit . fromIntegral
     lhs + rhs   = op lhs PLUS rhs
@@ -45,4 +41,5 @@
 
 instance Lambda LPrint where
+  type LInt LPrint = Int
   lit x      = LPrint $ \_ -> return $ shows x
   op m opc n = LPrint $ \p -> do
@@ -99,5 +96,4 @@
 x = aabs (\s _ -> s) `app` list (lit 0) (labs $ \_ -> undef)
 y = list 0 $ labs $ \_ -> undef
-z = (labs $ \s -> s+1) `app` (lit 1+2)
 conss = labs $ \x -> aabs $ \ys yf -> list (ys + 1) $ shift yf ys (labs $ \_ -> x)
 concats = aabs $ \xs xf -> (aabs $ \ys yf -> list (xs+ys) $ shift xf xs yf)
@@ -112,8 +108,19 @@
 l12 = list (lit 1) (labs $ \_ -> list (lit 2) (labs $ \_ -> unsized))
 
+v = (labs $ \s -> s+1) `app` (lit 1+2)
+w1 = (labs $ \s -> s+ lit 1)
+w2 = (labs $ \s -> s+ lit 2)
+q1 :: (Lambda l, a ~ LInt l, Num (l a)) => l (Arr l b (Arr l a a))
+q1 = (labs $ \q -> labs $ \s -> s + lit 1)
+q2 :: (Lambda l, a ~ LInt l, Num (l a)) => l (Arr l a (Arr l a a))
+q2 = (labs $ \q -> labs $ \s -> s + q)
+q3 = (labs $ \q -> labs $ \s -> q + s)
+
 {- Evaluating -}
+eval = unR
 newtype R a = R { unR :: a }
 instance Lambda R where
-  labs f      = R $ f 
+  type LInt R = Int
+  labs f      = R $ f
   app e1 e2   = (unR e1) e2
   lit i       = R i
@@ -136,74 +143,62 @@
   shift a s c = R $ \i -> if (unR 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 a = ([Condition], IntExp)
-newtype Compile a = Compile { unCompile :: SExp a }
-
---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)
+newtype E a = E { unE :: a }
+instance Lambda E where
+  type LInt E = SBV.SInteger
+  labs f = E $ f
+  app e1 e2   = (unE e1) e2
+  lit         = E 
+  op e1 op e2 = let opm = case op of
+                                  PLUS  -> (+)
+                                  MINUS -> (-)
+                                  MUL   -> (*)
+                in E $ opm (unE e1) (unE e2)
+
+class Sizeable' a where
+  getl' :: E (Arr E a b) -> SBV.Symbolic b
+
+instance Sizeable' (SBV.SInteger) where
+  getl' f = do
+    x <- SBV.sInteger "x"
+    return $ unE $ (unE f) $ E x
+
+{-
+getEq f = SBV.proveWith (SBV.z3 {SBV.verbose=True}) $ do
+  x <- getl f
+  return $ x SBV..== x
+-}
+data ST  = ST
+
+class Instantiateable a r | a -> r where
+  instantiate :: a -> SBV.Symbolic r
+
+instance Instantiateable SBV.SInteger SBV.SInteger where
+  instantiate _ = do
+    liftIO $ putStrLn " INT VARIABLE x"
+    SBV.sInteger "x"
+
+instance Instantiateable a ST where
+  instantiate _ = do
+    liftIO $ putStrLn " ? VARIABLE x"
+    return $ undefined -- SBV.uninterpret "f"
+
+class Sizeable a where
+  type Ret a :: *
+  getl :: a -> a -> SBV.Symbolic (Ret a, Ret a)
+
+instance (Instantiateable a r, Sizeable b) => Sizeable (Arr E a b) where
+  type Ret (Arr E a b) = Ret b
+  getl f g = do
+    liftIO $ putStrLn " -> x"
+    x <- instantiate (undefined :: a)
+    let f' = unE $ f $ E x
+    let g' = unE $ g $ E x
+    getl f' g'
+
+instance Sizeable (SBV.SInteger) where
+  type Ret SBV.SInteger = SBV.SInteger
+  getl f g = return (f,g)
+
+getEq f g = SBV.proveWith (SBV.z3 {SBV.verbose=True}) $ do
+  (x,y) <- getl (unE f) (unE g)
+  return $ x SBV..== y
Index: sizechecking_branches/LL.hs
===================================================================
--- sizechecking_branches/LL.hs	(revision 10)
+++ sizechecking_branches/LL.hs	(revision 15)
@@ -1,9 +1,10 @@
-{-# Language GADTs, 
-        FlexibleInstances, 
-        FlexibleContexts, 
-        ScopedTypeVariables, 
-        TypeFamilies, 
+{-# Language GADTs,
+        FlexibleInstances,
+        FlexibleContexts,
+        ScopedTypeVariables,
+        TypeFamilies,
         NoMonomorphismRestriction,
         OverlappingInstances #-}
+module LL where
 
 import Data.Char
@@ -14,7 +15,7 @@
   deriving Show
 
-type family Arr (repr :: * -> *) (a :: *) (b :: *) :: *
 
 class Lambda l where
+    type Arr l (a :: *) (b :: *) :: *
     labs    :: (l a -> l b) -> l (Arr l a b)
     app     :: l (Arr l a b) -> l a -> l b
@@ -49,7 +50,7 @@
 
 newtype LPrint a = LPrint { unPrint :: Int -> Int -> ShowS }
-type instance Arr LPrint a b = a -> b
 
 instance Lambda LPrint where
+  type Arr LPrint a b = a -> b
   lit x      = LPrint $ \_ -> return $ shows x
   op m opc n = LPrint $ \p -> do
@@ -75,7 +76,7 @@
 {- Evaluating -}
 newtype R a = R { unR :: a }
-type instance Arr R a b = R a -> R b
 
 instance Lambda R where
+  type Arr R a b = R a -> R b
   labs        = R
   app         = unR
@@ -94,3 +95,3 @@
 eval = unR
 
-z = labs ( \s -> s + 1) `app` ( 1 + lit 2)
+z = labs (\s -> s + lit 1) `app` (lit 1 + 2)
Index: sizechecking_branches/SE.hs
===================================================================
--- sizechecking_branches/SE.hs	(revision 15)
+++ sizechecking_branches/SE.hs	(revision 15)
@@ -0,0 +1,42 @@
+{-# Language GADTs,
+        FlexibleInstances,
+        FlexibleContexts,
+        ScopedTypeVariables,
+        TypeFamilies,
+        NoMonomorphismRestriction,
+        OverlappingInstances #-}
+
+module SE where
+
+import LL
+
+class SizeExp l where
+    type List l :: * -> *
+    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 ()
+
+
+instance SizeExp R where
+  type List R = RList
+  undef       = R $ Bottom
+  unsized     = R $ ()
+  list s f    = R $ RList (unR s, unR . (unR f) . R )
+  aabs e = R $ ( \(RList (s,f)) -> (e (R s) (R (R . f . unR))) ) . unR
+  shift a s c = R $ \i -> if (unR i)<(unR s) then unR a i else unR c i
+
+x = aabs (\s _ -> s) `app` list (lit 0) (labs $ \_ -> undef)
+--y = list 0 $ labs $ \_ -> undef
+--conss = labs $ \x -> aabs $ \ys yf -> list (ys + 1) $ shift yf ys (labs $ \_ -> x)
+--concats = aabs $ \xs xf -> (aabs $ \ys yf -> list (xs+ys) $ shift xf xs yf)
+--maps = labs $ \x -> aabs $ \ys yf -> list ys ( x `app` yf )
+--l0 = list (lit 0) (labs $ \_ -> unsized)
+--l1 = list (lit 1) (labs $ \_ -> unsized)
+--l2 = list (lit 2) (labs $ \_ -> unsized)
+--l00 = list (lit 0) (labs $ \_ -> list (lit 0) (labs $ \_ -> unsized))
+--l10 = list (lit 1) (labs $ \_ -> list (lit 0) (labs $ \_ -> unsized))
+--l01 = list (lit 0) (labs $ \_ -> list (lit 1) (labs $ \_ -> unsized))
+--l11 = list (lit 1) (labs $ \_ -> list (lit 1) (labs $ \_ -> unsized))
+--l12 = list (lit 1) (labs $ \_ -> list (lit 2) (labs $ \_ -> unsized))
Index: sizechecking_branches/SVB.hs
===================================================================
--- sizechecking_branches/SVB.hs	(revision 15)
+++ sizechecking_branches/SVB.hs	(revision 15)
@@ -0,0 +1,5 @@
+{-# LANGUAGE DeriveDataTypeable #-}
+
+import Data.Data
+import Data.SBV
+import LL