Index: /sizechecking/branches/macs/Exp.hs
===================================================================
--- /sizechecking/branches/macs/Exp.hs	(revision 26)
+++ /sizechecking/branches/macs/Exp.hs	(revision 27)
@@ -4,4 +4,5 @@
 import Ops
 import Data.Supply as S
+import Data.Lens.Light
 
 class LOps l => Exp l where
@@ -21,28 +22,31 @@
     cond c tbranch fbranch = if unQ c then tbranch else fbranch
     undefined = Prelude.undefined 
-instance Exp S where
-    nil = S $ \_ _ -> showString "[]"
-    undefined = S $ \_ _ -> showString "undefined"
-    match list nbranch cbranch = S $ \s p ->
-        let (s1, s2, ss) = S.split3 s
+
+instance SContext s => Exp (S s) where
+    nil = S $ \_ -> showString "[]"
+    undefined = S $ \_ -> showString "undefined"
+    match list nbranch cbranch = S $ \ctx ->
+        let (s1, s2, ss) = S.split3 (getL supply ctx)
             (s3, s4, s5) = S.split3 ss
             v1           = S.supplyValue s4
-            showV1       = S $ \_ _ -> showVar v1
+            showV1       = S $ \_ -> showVar v1
             v2           = S.supplyValue s5
-            showV2       = S $ \_ _ -> showVar v2
+            showV2       = S $ \_ -> showVar v2
+            p = getL prec ctx
         in showParen (p>0) $ 
             showString "case ".
-            unS list s1 0 .
+            unS list (updateCtx s1 0 ctx) .
             showString " of [] => ".
-            unS nbranch s2 0 .
+            unS nbranch (updateCtx s2 0 ctx) .
             showString "; (" .  showVar v1 . showChar ':' . showVar v2 . showString ") => " .
-            unS (cbranch showV1 showV2) s3 0
-    cond c tbranch fbranch = S $ \s p ->
-        let (s1, s2, s3) = S.split3 s
+            unS (cbranch showV1 showV2) (updateCtx s3 0 ctx)
+    cond c tbranch fbranch = S $ \ctx ->
+        let (s1, s2, s3) = S.split3 (getL supply ctx)
+            p = getL prec ctx
         in showParen (p>0) $ 
             showString "if ".
-            unS c s1 0 .
+            unS c (updateCtx s1 0 ctx).
             showString " then " .
-            unS tbranch s2 0 .
+            unS tbranch (updateCtx s2 0 ctx).
             showString " else " .
-            unS fbranch s3 0
+            unS fbranch (updateCtx s3 0 ctx)
Index: /sizechecking/branches/macs/Lambda.hs
===================================================================
--- /sizechecking/branches/macs/Lambda.hs	(revision 26)
+++ /sizechecking/branches/macs/Lambda.hs	(revision 27)
@@ -1,3 +1,3 @@
-{-# LANGUAGE TypeFamilies, GADTs #-}
+{-# LANGUAGE TypeFamilies, GADTs, Rank2Types, TemplateHaskell #-}
 
 module Lambda where
@@ -5,6 +5,5 @@
 import qualified Data.Supply as S
 import qualified Data.Char as C
-import Control.Monad.IO.Class (MonadIO, liftIO)
-import Data.IORef (newIORef, readIORef, writeIORef)
+import Data.Lens.Light 
 
 {-
@@ -29,6 +28,6 @@
 
 {-
- - show interpreter
- -}
+- show interpreter
+-}
 showVar :: Int -> String -> String
 showVar x = if x>28 
@@ -36,38 +35,39 @@
     else showChar $ C.chr $ C.ord 'a' + x
 
-newtype S a = S { unS :: S.Supply Int -> Int -> ShowS }
+class SContext a where
+  supply :: Lens a (S.Supply Int)
+  prec :: Lens a Int
 
-instance Lambda S where
-    lit a = S (\_ p -> showsPrec p a)
-    app (S fun) (S arg) = S (\s p -> 
-        let (s1, s2) = S.split2 s 
-        in showParen (p>6) $ fun s1 6 . showChar ' ' . arg s2 7)
-    lam fun = S (\s p -> 
-        let (s1, s2) = S.split2 s
+newtype S ctx a = S { unS :: ctx -> ShowS }
+
+instance SContext ctx => Lambda (S ctx) where
+    lit a = S (\ctx -> showsPrec (getL prec ctx) a)
+    app (S fun) (S arg) = S (\ctx ->
+        let (s1, s2) = S.split2 (getL supply ctx)
+            p = getL prec ctx
+        in showParen (p>6) $ fun (updateCtx s1 6 ctx) . showChar ' ' . arg (updateCtx s2 7 ctx))
+    lam fun = S (\ctx -> 
+        let (s1, s2) = S.split2 (getL supply ctx)
             v        = S.supplyValue s1
-            showV = S $ \_ _ -> showVar v
-        in showParen (p>0) $ showChar 'λ' . showVar v . showChar '.' . unS (fun showV) s2 0)
+            p        = getL prec ctx
+            showV = S $ \ctx -> showVar v
+        in showParen (p>0) $ showChar 'λ' . showVar v . showChar '.' . unS (fun showV) (updateCtx s2 0 ctx))
 
-ast :: S a -> IO ShowS
+updateCtx :: SContext ctx => S.Supply Int -> Int -> ctx -> ctx
+updateCtx s p = setL supply s . setL prec p
+
+data SData = SData { _getSDataSupply :: S.Supply Int, _getSDataPrec :: Int }
+$(makeLens ''SData)
+
+instance SContext SData where
+  supply = getSDataSupply
+  prec = getSDataPrec
+
+ast :: S SData a -> IO ShowS
 ast a = do
     s <- S.newSupply 0 (+1)
-    return $ unS a s 0
+    return $ unS a $ SData s 0
 
-printAst :: S a -> IO ()
+printAst :: S SData a -> IO ()
 printAst l = ast l >>= (\s -> putStrLn $ s "")
 
-
-{-
- - reduction
- -}
-data IR h t where
-    Lit :: Int -> IR h Int
-    App :: IR h (a -> b) -> IR h a -> IR h b
-    Lam :: (IR h a -> IR h b) -> IR h (a -> b)
-
-instance Lambda (IR h) where
-    lam = Lam
-    app = App
-    lit = Lit
-
-toFinal :: (Lambda l) => IR h t
Index: /sizechecking/branches/macs/Ops.hs
===================================================================
--- /sizechecking/branches/macs/Ops.hs	(revision 26)
+++ /sizechecking/branches/macs/Ops.hs	(revision 27)
@@ -7,4 +7,5 @@
 import qualified Prelude
 import Lambda
+import Data.Lens.Light
 
 -- infix operatorok, ezek beagyazasa picit necces, lasd a type family kesobb
@@ -32,26 +33,28 @@
     fun _ = Q
 
-instance LOps S where
-    fun name _ = S (\_ p -> Prelude.showsPrec p name)
+instance (SContext s) => LOps (S s) where
+    fun name _ = S (\ctx -> Prelude.showsPrec (getL prec ctx) name)
 
-    infixopl name prec _ lhs rhs = S(\s p ->
-        let (s1, s2) = S.split2 s
-        in Prelude.showParen (p Prelude.> prec) $
-            unS lhs s1 prec .
+    infixopl name p _ lhs rhs = S(\ctx ->
+        let (s1, s2) = S.split2 (getL supply ctx)
+        in Prelude.showParen ((getL prec ctx) Prelude.> p) $
+            unS lhs (setL supply s1 $ setL prec p ctx) .
             Prelude.showString name .
-            unS rhs s2 (Prelude.succ prec)
+            unS rhs (setL supply s2 $ setL prec (Prelude.succ p) ctx)
         )
-    infixop name prec _ lhs rhs = S(\s p ->
-        let (s1, s2) = S.split2 s
-        in Prelude.showParen (p Prelude.> prec) $
-            unS lhs s1 (Prelude.succ prec) .
+
+    infixop  name p _ lhs rhs = S(\ctx ->
+        let (s1, s2) = S.split2 (getL supply ctx)
+        in Prelude.showParen ((getL prec ctx) Prelude.> p) $
+            unS lhs (setL supply s1 $ setL prec (Prelude.succ p) ctx) .
             Prelude.showString name .
-            unS rhs s2 (Prelude.succ prec)
+            unS rhs (setL supply s2 $ setL prec (Prelude.succ p) ctx)
         )
-    infixopr name prec _ lhs rhs = S(\s p ->
-        let (s1, s2) = S.split2 s
-        in Prelude.showParen (p Prelude.> prec) $
-            unS lhs s1 (Prelude.succ prec) .
+
+    infixopr name p _ lhs rhs = S(\ctx ->
+        let (s1, s2) = S.split2 (getL supply ctx)
+        in Prelude.showParen ((getL prec ctx) Prelude.> p) $
+            unS lhs (setL supply s1 $ setL prec (Prelude.succ p) ctx) .
             Prelude.showString name .
-            unS rhs s2 prec
+            unS rhs (setL supply s2 $ setL prec p ctx)
         )
Index: /sizechecking/branches/macs/Size.hs
===================================================================
--- /sizechecking/branches/macs/Size.hs	(revision 26)
+++ /sizechecking/branches/macs/Size.hs	(revision 27)
@@ -8,4 +8,5 @@
 import Ops
 import Data.Supply as S
+import Data.Lens.Light
 
 data Unsized
@@ -19,20 +20,22 @@
 
 
-instance Size S where
-    unsized = S $ \_ _ -> showChar 'U'
-    bottom = S $ \_ _ -> showChar '┮'
-    list size sexp = S $ \s p ->
-        let (s1, s2) = S.split2 s
+instance SContext s => Size (S s) where
+    unsized = S $ \_ -> showChar 'U'
+    bottom = S $ \_ -> showChar '┮'
+    list size sexp = S $ \ctx ->
+        let (s1, s2) = S.split2 (getL supply ctx)
+            p = getL prec ctx
         in showParen (p>0) $
             showString "List " .
-            unS size s1 9 .
+            unS size (updateCtx s1 9 ctx) .
             showChar ' ' .
-            unS sexp s2 9
-    slam f = S $ \s p ->
-        let (s1, s2, s3) = S.split3 s
+            unS sexp (updateCtx s2 9 ctx)
+    slam f = S $ \ctx ->
+        let (s1, s2, s3) = S.split3 (getL supply ctx)
             v1           = S.supplyValue s1
-            showV1       = S $ \_ _ -> showVar v1
+            showV1       = S $ \_ -> showVar v1
             v2           = S.supplyValue s2
-            showV2       = S $ \_ _ -> showVar v2
+            showV2       = S $ \_ -> showVar v2
+            p = getL prec ctx
         in showParen (p>0) $
             showChar 'Λ' .
@@ -41,13 +44,14 @@
             showVar v2 .
             showChar '.' .
-            unS (f showV1 showV2) s3 0
-    shift e1 ss e2 = S $ \s p ->
-        let (s1, s2, s3) = S.split3 s
+            unS (f showV1 showV2) (updateCtx s3 0 ctx)
+    shift e1 ss e2 = S $ \ctx ->
+        let (s1, s2, s3) = S.split3 (getL supply ctx)
+            p = getL prec ctx
         in showParen (p>0)
         $ showString "Shift "
-        . unS e1 s1 2
+        . unS e1 (updateCtx s1 2 ctx)
         . showChar ' '
-        . unS ss s2 2
+        . unS ss (updateCtx s2 2 ctx)
         . showChar ' '
-        . unS e2 s3 2
+        . unS e2 (updateCtx s3 2 ctx)
 
Index: /sizechecking/branches/macs/SizedFun.hs
===================================================================
--- /sizechecking/branches/macs/SizedFun.hs	(revision 27)
+++ /sizechecking/branches/macs/SizedFun.hs	(revision 27)
@@ -0,0 +1,68 @@
+{-# LANGUAGE TypeFamilies,TemplateHaskell,MultiParamTypeClasses,FlexibleContexts,FlexibleInstances,OverlappingInstances,IncoherentInstances #-}
+{-# LANGUAGE GADTs #-}
+
+module SizedFun where
+
+import Lambda
+import Size
+import Exp
+import Ops
+
+import qualified Data.Supply as S
+import Data.Lens.Light
+
+class Infer a b where
+instance (Infer a b, Infer p q) => Infer (a->p) (b->q)
+instance Infer a b => Infer [a] [b]
+instance (a~b) => Infer a b
+instance Infer Unsized Int
+
+class (Exp e, Size (SizeExp e)) => SizedFun e where
+  type SizeExp e :: * -> *
+  bind :: Infer a b => String -> SizeExp e a -> e b -> e b
+
+class SContext s => SBContext s where
+    bound :: Lens s Bool
+
+instance SBContext s => SizedFun (S s) where
+  type SizeExp (S s) = S s
+  bind name size exp = S $ \ctxo -> if getL bound ctxo then
+      showString name
+      else let (s1, s2) = S.split2 (getL supply ctxo)
+               ctx = setL bound True ctxo
+      in showString name . showString " :: " . unS size (updateCtx s1 0 ctx) . showChar '\n'.
+         showString name . showString " = "  . unS exp (updateCtx s2 0 ctx) 
+
+data SBData = SBData { _getSBDataSupply :: S.Supply Int, _getSBDataPrec :: Int, _getSBDataBound :: Bool }
+$(makeLens ''SBData)
+
+instance SContext SBData where
+    supply = getSBDataSupply
+    prec = getSBDataPrec
+
+instance SBContext SBData where
+    bound = getSBDataBound
+
+astf :: S SBData a -> IO ShowS
+astf a = do
+    s <- S.newSupply 0 (Prelude.+1)
+    return $ unS a $ SBData s 0 False
+
+printFun :: S SBData a -> IO ()
+printFun l = astf l >>= (\s -> putStrLn $ s "")
+
+instance SizedFun Q where
+    type SizeExp Q = S SBData
+    bind name size exp = exp
+
+data DeclSize b where
+  DeclSize :: Infer a b => S SData a -> DeclSize b
+
+instance Lambda DeclSize where
+instance LOps DeclSize where
+instance Exp DeclSize where
+instance SizedFun DeclSize where
+    type SizeExp DeclSize = S SData
+    bind name size exp = DeclSize size
+
+--getDeclSize (DeclSize size) = size
Index: /sizechecking/branches/macs/Tests/BindTest.hs
===================================================================
--- /sizechecking/branches/macs/Tests/BindTest.hs	(revision 27)
+++ /sizechecking/branches/macs/Tests/BindTest.hs	(revision 27)
@@ -0,0 +1,16 @@
+{-# LANGUAGE NoMonomorphismRestriction #-}
+
+module Tests.BindTest where
+
+import Lambda
+import SizedFun
+import Exp
+import Prelude ( ($), Int, (==), return, sequence, (>>=), and, (.), IO, Bool, String, const )
+import qualified Control.Monad
+import qualified Tests.SizeTest as S
+import qualified Tests.ExpTest as E
+
+addOne = bind "addone" S.testAddOne E.testAddOne
+
+concat = bind "concat" S.testConcat
+  (lam $ \l1 -> lam $ \l2 -> match l1 l2 $ \x xs -> cons x (concat `app` xs `app` l2))
Index: /sizechecking/branches/macs/Tests/ExpTest.hs
===================================================================
--- /sizechecking/branches/macs/Tests/ExpTest.hs	(revision 26)
+++ /sizechecking/branches/macs/Tests/ExpTest.hs	(revision 27)
@@ -30,5 +30,5 @@
 testD2Cons = cons (cons (lit 1) nil) nil
 
-checkAST :: S a -> String -> IO Bool
+checkAST :: S SData a -> String -> IO Bool
 checkAST exp repr = ast exp >>= (\t -> return $ t "" == repr )
 
Index: /sizechecking/branches/macs/Tests/SizeTest.hs
===================================================================
--- /sizechecking/branches/macs/Tests/SizeTest.hs	(revision 26)
+++ /sizechecking/branches/macs/Tests/SizeTest.hs	(revision 27)
@@ -21,9 +21,17 @@
 testTail = slam $ \s f -> list (s - lit 1) f
 
+testAddOne :: (Size l) => l ([Unsized] -> [Unsized])
+testAddOne = slam $ \s f -> list (s + lit 1) (lam $ const unsized)
+
 testCons :: Size l => l (a -> [a] -> [a])
 testCons = lam $ \x -> slam $ \s f ->
     list (s + lit 1) $ shift f s (lam $ const x)
 
-checkAst :: S a -> String -> IO Bool
+testConcat :: Size l => l ([a] -> [a] -> [a])
+testConcat = slam $ \s1 f1 -> slam $ \s2 f2 ->
+    list (s1 + s2) $ shift f1 s1 f2
+
+
+checkAst :: S SData a -> String -> IO Bool
 checkAst exp repr = ast exp >>= (\t -> return $ t "" == repr)
 
Index: /sizechecking/branches/macs/sizechecking.cabal
===================================================================
--- /sizechecking/branches/macs/sizechecking.cabal	(revision 26)
+++ /sizechecking/branches/macs/sizechecking.cabal	(revision 27)
@@ -55,3 +55,3 @@
   -- Other library packages from which modules are imported.
   build-depends:       base ==4.*, containers ==0.5.*, sbv, value-supply,
-                       transformers
+                       transformers, data-lens-light