diff --git a/LambdaPrettyQuote.cabal b/LambdaPrettyQuote.cabal
--- a/LambdaPrettyQuote.cabal
+++ b/LambdaPrettyQuote.cabal
@@ -7,10 +7,10 @@
 -- The package version. See the Haskell package versioning policy
 -- (http://www.haskell.org/haskellwiki/Package_versioning_policy) for
 -- standards guiding when and how versions should be incremented.
-Version:             0.0.0.6
+Version:             0.0.0.7
 
 -- A short (one-line) description of the package.
-Synopsis:            Parser, pretty printer, quasiquoter, and Arbitrary helpers for the untyped lambda calculus.
+Synopsis:            Quasiquoter, and Arbitrary helpers for the lambda calculus.
 
 homepage: http://github.com/jfischoff/LambdaPrettyQuote
 
@@ -51,7 +51,7 @@
 
 Library
   -- Modules exported by the library.
-  Exposed-modules: Language.Lambda.Arbitrary, Language.Lambda.Parser, Language.Lambda.Pretty, Language.Lambda.Quote
+  Exposed-modules: Language.Lambda.Untyped.Arbitrary, Language.Lambda.Untyped.Parser, Language.Lambda.Untyped.Pretty, Language.Lambda.Untyped.Quote, Language.Lambda.SimplyTyped.Arbitrary,  Language.Lambda.SimplyTyped.Pretty, Language.Lambda.SimplyTyped.TypeCheck 
   Hs-Source-Dirs: src
   -- Packages needed in order to build this package.
   Build-depends: base >= 4.0 && <= 6.0,
@@ -59,14 +59,16 @@
                  test-framework-quickcheck2 >= 0.2.10,
                  test-framework-hunit >= 0.2.7,
                  test-framework >= 0.4.1.1,
-                 lambda-ast >= 0.0.4,
+                 lambda-ast >= 0.0.9,
                  HUnit >= 1.2.4.2,
                  DebugTraceHelpers >= 0.12,
                  template-haskell >= 2.6.0.0,
                  transformers >= 0.2.2.0,
                  parsec >= 3.1.2,
                  uniplate >= 1.6.5,
-                 syb >= 0.3.5
+                 syb >= 0.3.5,
+                 mtl >= 2.0.1.0,
+                 tuple >= 0.2.0.1
   ghc-options:            -Wall
 
 Test-Suite tests
@@ -78,7 +80,7 @@
                     test-framework-quickcheck2 >= 0.2.10,
                     test-framework-hunit >= 0.2.7,
                     test-framework >= 0.4.1.1,
-                    lambda-ast >= 0.0.4,
+                    lambda-ast >= 0.0.9,
                     HUnit >= 1.2.4.2,
                     DebugTraceHelpers >= 0.12,
                     template-haskell >= 2.6.0.0,
@@ -86,5 +88,8 @@
                     parsec >= 3.1.2,     
                     uniplate >= 1.6.5,
                     th-instances >= 0.1.0.2,
-                    syb >= 0.3.5
-  
+                    syb >= 0.3.5,
+                    mtl >= 2.0.1.0,
+                    derive >= 2.5.4,
+                    tuple >= 0.2.0.1,
+                    checkers >= 0.2.8
diff --git a/src/Language/Lambda/Arbitrary.hs b/src/Language/Lambda/Arbitrary.hs
deleted file mode 100644
--- a/src/Language/Lambda/Arbitrary.hs
+++ /dev/null
@@ -1,47 +0,0 @@
-{- | This module provides the code of QuickCheck instances, but doesn't declare the instances
-   Of the whole orphan deal, oh well. 
- 
-    Anyway, to use you will need to copy the following code somewhere
-> Instance Arbitrary Expr where
->     arbitrary = expr_arb  
->     shrink    = gexpr_shrink
- There is also a gexpr_arb that takes in a generator for the symbol type
--}
-module Language.Lambda.Arbitrary where
-import Test.QuickCheck
-import Control.Applicative ((<*>), (<$>))
-import Data.List
-import Language.Lambda.AST
-
--- | An arbitrary function for Expr. See the example above.
-expr_arb :: Gen Expr
-expr_arb = gexpr_arb sym_arbitrary
-
--- | Generates a string like "x_{n}" where n is positive integer
-sym_arbitrary :: Gen String 
-sym_arbitrary = do
-    index <- suchThat (arbitrary :: Gen Int) (>0)
-    return $ ("x_" ++ (show index))
-    
--- | Shrink function for an GExpr. See the example at the top of the module    
-gexpr_shrink :: GExpr a -> [GExpr a]
-gexpr_shrink x@(Var _) = [x]
-gexpr_shrink (App x y) = [x, y]
-gexpr_shrink (Lam _ y) = [y]
-   
--- | Helper function for creating generators for GExpr. Takes in a generator for the symbol type
-gexpr_arb :: Gen a -> Gen (GExpr a) 
-gexpr_arb sym_gen = sized $ \x -> gexpr_arb' x sym_gen
-
--- | Helper function for creating generators for GExpr. Takes in a generator for the symbol type and the
--- "depth" of the expression tree
-gexpr_arb' :: Int -> Gen s -> Gen (GExpr s)
-gexpr_arb' 0 s_arb = Var <$> s_arb
-gexpr_arb' n s_arb = do
-    option <- choose(0, 2) :: Gen Int
-    case option of
-        0 -> Var <$> s_arb
-        1 -> App <$> gexpr_arb' (n - 1) s_arb <*> gexpr_arb' (n - 1) s_arb
-        2 -> Lam <$> s_arb                    <*> gexpr_arb' (n - 1) s_arb
-        _ -> error "choose messed up!"
-        
diff --git a/src/Language/Lambda/Parser.hs b/src/Language/Lambda/Parser.hs
deleted file mode 100644
--- a/src/Language/Lambda/Parser.hs
+++ /dev/null
@@ -1,122 +0,0 @@
-{-# LANGUAGE FlexibleContexts, DeriveDataTypeable #-}
-{-- | Parser for the lambda AST built of parsec. Converts to an intermediate format for antiexpressions -}
-module Language.Lambda.Parser where
-import Text.Parsec
-import Text.Parsec.Language
-import Text.Parsec.Token 
-import Language.Lambda.AST
-import Data.Functor.Identity
-import Data.List
-import Data.Data
-
-type M = Identity
-
-data MetaExpr s = MVar (MetaSym s)
-              | MApp (MetaExpr s) (MetaExpr s)
-              | MLam (MetaSym s) (MetaExpr s)
-              | AntiExpr String
-              | AntiVar  String
-              deriving(Show, Eq, Data, Typeable)
-              
-data MetaSym s = S s
-               | AntiSym String
-              deriving(Show, Eq, Data, Typeable)
-
-type Output s = MetaExpr s
-
-type SymParser u s = ParsecT String u M s
-
-top_expr :: SymParser u s -> ParsecT String u M (Output s)
-top_expr sp = do 
-    spaces
-    e <- parse_expr sp
-    spaces
-    eof
-    return e
-    
-parse_expr :: SymParser u s -> ParsecT String u M (Output s)
-parse_expr sp = try (parse_aexpr sp)
-          <|> try (parse_lambda sp)
-          <|> try parse_anti_expr
- 
-parse_aexpr :: SymParser u s -> ParsecT String u M (Output s)
-parse_aexpr sp =  try (parse_app sp)
-              <|> try (parse_atom sp)
-           
-parse_anti_expr :: ParsecT String u M (Output s)
-parse_anti_expr = do
-    _ <- string "$"
-    i <- (identifier haskell)
-    return $ AntiExpr i
-
-parse_lambda :: SymParser u s -> ParsecT String u M (Output s)
-parse_lambda sp = do
-    _ <- char '\\'
-    spaces
-    sym  <- (p_sym sp) <?> "lambda argument"
-    _ <- char '.'
-    spaces
-    expr <- (parse_expr sp) <?> "lambda expression"
-    return $ MLam sym expr
-
-parse_app :: SymParser u s -> ParsecT String u M (Output s)
-parse_app sp = do
-    expr_0 <- (parse_atom sp) <?> "first apply argument"
-    spaces
-    as <-  sepBy1 (parse_atom sp) spaces <?> "other apply arguments"
-    return $ foldl' MApp expr_0 as
-
-parse_atom :: SymParser u s -> ParsecT String u M (Output s)
-parse_atom sp =  try  (parens'  (parse_expr sp))
-          <|> try (parse_var sp)
-          <|> try parse_anti_expr
-          
-parse_var sp = try (parse_var' sp) <|> parse_anti_var 
-          
-parse_var' :: SymParser u s -> ParsecT String u M (Output s)
-parse_var' sp = do
-    spaces
-    sym <- (p_sym sp) <?> "Var symbol"
-    return $ MVar sym  
- 
-parse_anti_var = do 
-    spaces 
-    _ <- string "*"
-    i <- (identifier haskell)
-    return $ AntiVar i
-    
-p_sym :: SymParser u s -> ParsecT String u M (MetaSym s)
-p_sym sp = try (S `fmap` sp) <|> try parse_anti_sym
-
-parse_anti_sym :: ParsecT String u M (MetaSym s)
-parse_anti_sym = do
-    _ <- string "^"
-    i <- (identifier haskell)
-    return $ AntiSym i
-    
-parse_sym :: ParsecT String u M Sym
-parse_sym = many1 (alphaNum <|> char '_') <?> "symbol"
-
-parens' :: Stream s m Char => ParsecT s u m b -> ParsecT s u m b
-parens' p = do 
-    _ <- char '('
-    e <- p
-    _ <- char ')'
-    return e
-
-meta_to_expr :: MetaExpr s -> GExpr s
-meta_to_expr (MVar (S x))     = Var x
-meta_to_expr (MApp x y)   = App (meta_to_expr x) (meta_to_expr y)
-meta_to_expr (MLam (S x) y)   = Lam x (meta_to_expr y)
-meta_to_expr _ = error "meta_to_expr should not be used if the MetaExpr tree has AntiExpr"
-
-to_meta :: GExpr s -> MetaExpr s
-to_meta (Var x)   = MVar (S x)
-to_meta (App x y) = MApp (to_meta x) (to_meta y)
-to_meta (Lam x y) = MLam (S x) (to_meta y)
-
-
-
-
-
-
diff --git a/src/Language/Lambda/Pretty.hs b/src/Language/Lambda/Pretty.hs
deleted file mode 100644
--- a/src/Language/Lambda/Pretty.hs
+++ /dev/null
@@ -1,15 +0,0 @@
-{-- | Pretty printers for lambda expression -}
-module Language.Lambda.Pretty where
-import Language.Lambda.AST
-
--- | Pretty prints a Expr
-ppr :: Expr -> String
-ppr (Var x)   = x
-ppr (App x y) = "(" ++ ppr x ++ " " ++ ppr y ++ ")" 
-ppr (Lam x y) = "(\\" ++ x ++ "." ++ ppr y ++ ")"
-
--- | Pretty prints a GExpr 
-g_ppr :: (Show a) => GExpr a -> String
-g_ppr (Var x)   = show x
-g_ppr (App x y) = "(" ++ g_ppr x ++ " " ++ g_ppr y ++ ")" 
-g_ppr (Lam x y) = "(\\" ++ show x ++ "." ++ g_ppr y ++ ")"
diff --git a/src/Language/Lambda/Quote.hs b/src/Language/Lambda/Quote.hs
deleted file mode 100644
--- a/src/Language/Lambda/Quote.hs
+++ /dev/null
@@ -1,88 +0,0 @@
-{-# LANGUAGE TemplateHaskell, QuasiQuotes, RankNTypes #-}
-module Language.Lambda.Quote (lam, g_lam) where
-import Language.Haskell.TH.Quote
-import Language.Haskell.TH
-import Language.Lambda.Parser
-import Text.Parsec (runParser)
-import Data.Generics.Aliases
-import Data.Generics.Uniplate.Data
-import Language.Lambda.AST
-import Data.Data
-import Debug.Trace.Helpers
- 
-lam :: QuasiQuoter
-lam = g_lam parse_sym
-
-g_lam :: (Data s, Show s) => SymParser () s -> QuasiQuoter
-g_lam sp = QuasiQuoter (g_quoteExprExp sp) (g_quoteExprPat sp) undefined undefined
-
-
-parseExpr :: Monad m => SymParser () s -> (String, Int, Int) -> String -> m (Output s)
-parseExpr sp (file, line, col) s = result where
-    result = case runParser (top_expr sp) () file s of
-                  Left err  -> fail $ (show err ++ " at file " ++ file ++ " at line " ++ 
-                                          show line ++ " at col " ++ show col)
-                  Right e   -> return e
-    
-
-    
-g_quoteExprExp :: (Data s, Show s,  Typeable s) => SymParser () s -> String -> ExpQ
-g_quoteExprExp sp r =  do  
-    loc <- location
-    let pos =  (loc_filename loc,
-             fst (loc_start loc),
-             snd (loc_start loc))
-    parsed_expr <- (parseExpr sp) pos r
-    appE (varE $ mkName "meta_to_expr") $ dataToExpQ (const Nothing `extQ` 
-        (antiExprExp sp)) $ parsed_expr
-             
-antiExprExp :: (Data s, Typeable s) => SymParser () s -> MetaExpr s -> Maybe (Q Exp)
-antiExprExp d (MLam (AntiSym v) x) = Just $ appE (appE (conE $ mkName "MLam") $ appE (conE $ mkName "S") $ varE (mkName v))
-                                         $ dataToExpQ (const Nothing `extQ` (antiExprExp d)) x
-antiExprExp d (MVar (AntiSym v))   = Just $ appE (conE $ mkName "MVar") $ appE (conE $ mkName "S") $ varE (mkName v)
-antiExprExp d (AntiExpr v)         = Just $ appE (varE $ mkName "to_meta") $ varE (mkName v)
-antiExprExp d (AntiVar v)          = Just $ [| MVar (S $(varE $ mkName v)) |]
-antiExprExp _ _                    = Nothing
-
-g_quoteExprPat :: (Data s, Show s, Typeable s) => SymParser () s ->  String -> PatQ
-g_quoteExprPat sp r =  do  
-    loc <- location
-    let pos =  (loc_filename loc,
-             fst (loc_start loc),
-             snd (loc_start loc))
-    parsed_expr <- (parseExpr sp) pos r
-    th_pat <- dataToPatQ (const Nothing `extQ` (antiExprPat sp)) parsed_expr
-    return $ to_e th_pat where
-        to_e p = transform to_e' p
-
-        to_e' (ConP n xs) | show n == "MVar" = ConP (to_expr_name n) [collapse_meta_sym $ head xs]
-        to_e' (ConP n xs) | show n == "MLam" = ConP (to_expr_name n) ((collapse_meta_sym $ head xs):(tail xs))
-        to_e' (ConP n xs) | otherwise        = ConP (to_expr_name n) xs
-        to_e' x = x
-
-        to_expr_name name | show name == "MVar" = mkName "Var" 
-        to_expr_name name | show name == "MApp" = mkName "App" 
-        to_expr_name name | show name == "MLam" = mkName "Lam"
-        to_expr_name name | otherwise           = name
-        
-        collapse_meta_sym (ConP n xs) | nameBase n == "S" = head xs
-        collapse_meta_sym p@(ConP n xs) | otherwise = error ("collapse_meta_sym not used on a S " ++ show p)
-             
-antiExprPat :: (Data s, Typeable s) => SymParser () s -> MetaExpr s -> Maybe (Q Pat)
-antiExprPat d (MLam (AntiSym v) x) = Just $ conP (mkName "MLam") [conP (mkName "S") [varP (mkName v)], 
-                                        dataToPatQ (const Nothing `extQ` (antiExprPat d)) x]
-antiExprPat d (MVar (AntiSym v))   = Just $ conP (mkName "MVar") [conP (mkName "S") [varP (mkName v)]]
-antiExprPat d (AntiExpr v)         = Just $ varP (mkName v)
-antiExprPat d (AntiVar v)          = Just $ conP (mkName "MVar") [conP (mkName "S") [varP $ mkName v]]
-antiExprPat _ _                    = Nothing
-
-
-
-
-
-
-
-
-
-
-
diff --git a/src/Language/Lambda/SimplyTyped/Arbitrary.hs b/src/Language/Lambda/SimplyTyped/Arbitrary.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Lambda/SimplyTyped/Arbitrary.hs
@@ -0,0 +1,189 @@
+module Language.Lambda.SimplyTyped.Arbitrary (
+    module Language.Lambda.Common.Arbitrary,
+    Env,
+    gen_type,
+    gen_expr,
+    --gen_env,
+    gen_with_env,
+    shrink_expr
+) where
+import Test.QuickCheck
+import Control.Applicative ((<*>), (<$>))
+import Data.List
+import Language.Lambda.SimplyTyped.Syntax
+import Control.Monad.RWS.Strict
+import Control.Applicative
+import Test.QuickCheck.Gen
+import Data.Tuple.Select
+import Language.Lambda.Common.Arbitrary
+import Data.Maybe
+import Debug.Trace.Helpers
+import Debug.Trace
+
+type Env a s = [(s, Type a)]
+
+null_const_gen = arbitrary :: Gen (Maybe ())
+
+gen_type :: (Eq a, Eq s) => Gen a -> Gen s -> Gen (Type a)
+gen_type x y = gen_with_env arb_type x y $ const null_const_gen
+
+gen_expr :: (Eq a, Eq s) => Gen a -> Gen s -> (Type a -> Gen (Maybe c)) -> Gen (Expr s a c)
+gen_expr = gen_with_env arb_expr
+
+shrink_expr :: Expr s a c -> [Expr s a c]
+shrink_expr x@(Constant _) = []
+shrink_expr x@(Var _)      = []
+shrink_expr (App x y)      = []
+shrink_expr (Lam s t e)    = []
+
+gen_with_env :: (Eq a, Eq s) => EnvGen a s c b -> Gen a -> Gen s -> (Type a -> Gen (Maybe c)) -> Gen b
+gen_with_env gen x y z = sized $ \i -> gen_with_env' gen (min i 5) x y z
+    
+gen_with_env' :: (Eq a, Eq s) => EnvGen a s c b -> Int -> Gen a -> Gen s -> (Type a -> Gen (Maybe c)) -> Gen b
+gen_with_env' gen size a_gen s_gen c_gen = do
+    (result, _) <- evalRWST gen (a_gen, s_gen, size, c_gen, []) ()
+    return result
+
+type EnvGen a s c = RWST (Gen a, Gen s, Int, Type a -> Gen (Maybe c), (Env a s)) () () Gen
+
+arb_type :: (Eq a, Eq s) => EnvGen a s c (Type a)
+arb_type = arb_type' =<< get_size 
+
+arb_type' :: (Eq a, Eq s) => Int -> EnvGen a s c (Type a)
+arb_type' 0    = Base <$> arb_base
+arb_type' size = do
+    option <- lift (choose (0, 1 :: Int))
+    case option of
+        0 -> Base  <$> arb_base
+        1 -> Arrow <$> arb_type' (size - 1) <*> arb_type' (size - 1)
+
+arb_expr :: (Eq a, Eq s) => EnvGen a s c (Expr s a c)
+arb_expr = trace ("arb_expr") $ do
+    i <- get_size 
+    input  <- arb_type
+    output <- arb_type
+    arb_lam i (Arrow input output)
+
+--This is good, but it is not useful for 
+arb_var typ = do
+    lookuped_value <- lookup_var_by_type typ
+    case lookuped_value of
+        (Just x) -> return $ Var $ fst x
+        _ -> error "bad symbol name"
+ 
+var_type_exists :: (Eq a, Eq s) => Type a -> EnvGen a s c (Bool)
+var_type_exists typ = isJust <$> lookup_var_by_type typ
+    
+lookup_var_by_type :: (Eq a, Eq s) => Type a -> EnvGen a s c (Maybe (s, Type a))
+lookup_var_by_type typ = do
+    vars <- gets_env (filter ((typ==) . snd))
+    if length vars > 0 
+        then do v <- lift $ elements vars
+                return $ Just v 
+        else return Nothing
+ 
+-- the right has to be it
+-- and the left has to be type -> whatever it was told to be  
+arb_app i typ = do
+     output_type <- arb_type
+     let f = Arrow output_type typ
+     arb_app_typ i f output_type
+
+arb_app_typ i input_type output_type = trace ("arb_app_typ" ++ show i) $ do
+    App <$> arb_expr' input_type (i - 1) <*> arb_expr' output_type (i - 1)
+
+
+fourth f (x, y, z, w, u) = (x, y, z, w, u)
+
+arb_lam :: (Eq a, Eq s) => Int -> Type a -> EnvGen a s c (Expr s a c) 
+arb_lam 0 x = terminal_lambda x
+arb_lam i (Arrow input output) = do
+    sym <- uniq_sym
+    local (fourth (extend sym input)) $ do 
+        Lam sym input <$> (arb_expr' output (i - 1))
+
+arb_expr' :: (Eq a, Eq s) => Type a -> Int -> EnvGen a s c (Expr s a c)
+arb_expr' typ i = trace ("arb_expr'" ++ show i) $ do
+    option <-lift $ choose (0, 10 :: Int)
+    if option == 0
+        then attemp_constant_expr typ i  
+        else non_constant_expr typ i
+        
+app_or_lam typ 0 = terminal_lambda typ 
+app_or_lam typ@(Arrow _ _) i = trace ("app_or_lam" ++ show i) $ do
+    option <- lift arbitrary
+    if option
+        then arb_app i typ
+        else arb_lam i typ
+app_or_lam typ i = trace ("app_or_lam" ++ show i) $ do
+    arb_app i typ
+        
+terminal_lambda :: (Eq a, Eq s) => Type a -> EnvGen a s c (Expr s a c) 
+terminal_lambda typ@(Base _) = do 
+    c <- arb_constant typ
+    return $ Constant $ fromJust c
+terminal_lambda (Arrow input output) = do
+    sym <- uniq_sym
+    Lam sym input <$> terminal_lambda output
+
+     
+non_constant_expr :: (Eq a, Eq s) => Type a -> Int -> EnvGen a s c (Expr s a c)
+non_constant_expr typ@(Arrow _ _) 0 = arb_lam 0 typ
+non_constant_expr typ@(Arrow _ _) i = trace ("non_constant_expr" ++ show i) $ do
+        option <- lift $ choose (0, 2 :: Int)
+        case option of 
+            0 -> do can_make_var <- var_type_exists typ
+                    if can_make_var
+                        then arb_var typ
+                        else app_or_lam typ i
+            1 -> arb_app i typ
+            2 -> arb_lam i typ
+non_constant_expr typ@(Base _) i = trace ("non_constant_expr" ++ show i) $ do
+        c <- arb_constant typ
+        return $ Constant $ fromJust c
+
+attemp_constant_expr :: (Eq a, Eq s) => Type a -> Int -> EnvGen a s c (Expr s a c)
+attemp_constant_expr typ i = trace ("attemp_constant_expr" ++ show i) $ do
+    constant <- arb_constant typ
+    case constant of
+        Just x  -> return $ Constant x
+        Nothing -> non_constant_expr typ i
+            
+extend :: (Eq a, Eq s) => s -> Type a -> Env a s -> Env a s
+extend s t xs = (s, t):xs
+
+get_env :: (Eq a, Eq s) => EnvGen a s c (Env a s)
+get_env = asks sel5
+
+gets_env :: (Eq a, Eq s) => (Env a s -> d) ->  EnvGen a s c d
+gets_env f = asks (f . sel5)
+    
+arb_s :: (Eq a, Eq s) => EnvGen a s c s
+arb_s = lift =<< asks sel2
+    
+arb_base :: (Eq a, Eq s) => EnvGen a s c a
+arb_base = lift =<< asks sel1
+
+get_size :: (Eq a, Eq s) => EnvGen a s c Int
+get_size = asks ((\x -> trace ("size " ++ show x) x) . sel3)
+
+arb_constant :: (Eq a, Eq s) => (Type a) -> EnvGen a s c (Maybe c)
+arb_constant x = lift =<< asks (($ x) . sel4)
+
+uniq_sym :: (Eq a, Eq s) => EnvGen a s c s
+uniq_sym = do
+    s_gen <- asks sel2
+    env <- get_env
+    lift $ suchThat s_gen ( `notElem` (map fst env))
+
+
+    
+    
+    
+    
+    
+    
+    
+    
+    
+
diff --git a/src/Language/Lambda/SimplyTyped/Pretty.hs b/src/Language/Lambda/SimplyTyped/Pretty.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Lambda/SimplyTyped/Pretty.hs
@@ -0,0 +1,16 @@
+{-- | Pretty printers for lambda expression -}
+module Language.Lambda.SimplyTyped.Pretty where
+import Language.Lambda.SimplyTyped.Syntax
+
+-- | Pretty prints a Expr
+ppr :: Show a => Expr String a String -> String
+ppr (Var x)   = x
+ppr (App x y) = "(" ++ ppr x ++ " " ++ ppr y ++ ")" 
+ppr (Lam x t y) = "(\\" ++ x ++ ":" ++ ppr_type t ++ " ." ++ ppr y ++ ")"
+ppr (Constant x) = x
+
+
+ppr_type (Base x) = show x
+ppr_type (Arrow x y) = "(" ++ ppr_type x ++ "->" ++ ppr_type y ++ ")"
+
+
diff --git a/src/Language/Lambda/SimplyTyped/TypeCheck.hs b/src/Language/Lambda/SimplyTyped/TypeCheck.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Lambda/SimplyTyped/TypeCheck.hs
@@ -0,0 +1,72 @@
+module Language.Lambda.SimplyTyped.TypeCheck (type_check) where 
+import Language.Lambda.SimplyTyped.Syntax
+import Control.Monad.Error
+import Control.Monad.Reader
+import Control.Monad.Identity
+import Data.Tuple.Select
+import Control.Arrow
+    
+type M = Identity
+type TypeError = String
+
+type TypeCheckEnv a s c o = ErrorT TypeError (ReaderT ((c -> Type a), Env a s) M) o
+
+type_check :: (Show s, Eq s, Eq a, Show a) => (c -> Type a) -> Expr s a c -> Either TypeError (Type a)
+type_check const_to_type expr = runIdentity $ 
+    runReaderT (runErrorT (type_check' expr)) (const_to_type, [])
+
+------------------------------------------------------------------------------------------------------
+
+type Env a s = [(s, Type a)]
+
+extend :: s -> Type a -> Env a s -> Env a s
+extend sym typ xs = (sym, typ):xs
+
+find_var :: (Show s, Eq s) => s -> TypeCheckEnv a s c (Type a)
+find_var s = unmaybe ("could not find variable named " ++ show s) =<< (lift $ asks (lookup s . sel2))
+        
+type_check' :: (Show s, Eq s, Eq a, Show a) => Expr s a c -> TypeCheckEnv a s c (Type a)
+type_check' (Var sym)   = find_var sym
+type_check' (App function argument) = do
+    function_type <- type_check'  function
+    --split the function type into its input and output
+    function_input_type  <- input_type  function_type 
+    function_output_type <- output_type function_type
+
+    --argument must match function input
+    argument_type <- type_check' argument
+    when (function_input_type /= argument_type) $ 
+        throwError $ ("Type Error: expected " ++ show function_input_type ++ " but got" 
+            ++ show argument_type)
+
+    return function_output_type
+type_check' (Lam sym input_typ expr) = do
+   local (second (extend sym input_typ)) $ do
+        output_typ <- type_check' expr
+        return $ Arrow input_typ output_typ
+type_check' (Constant c) = asks (($ c) . sel1)
+    
+    
+unmaybe :: String -> Maybe o -> TypeCheckEnv a s c o
+unmaybe error_string Nothing  = throwError error_string
+unmaybe error_string (Just x) = return x
+
+input_type (Arrow x _) = return x
+input_type _           = throwError "Not a function type"
+    
+output_type (Arrow _ y) = return y
+output_type _           = throwError "Not a function type"
+    
+    
+    
+    
+    
+    
+    
+    
+    
+    
+    
+    
+    
+    
diff --git a/src/Language/Lambda/Untyped/Arbitrary.hs b/src/Language/Lambda/Untyped/Arbitrary.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Lambda/Untyped/Arbitrary.hs
@@ -0,0 +1,47 @@
+{- | This module provides the code of QuickCheck instances, but doesn't declare the instances
+   Of the whole orphan deal, oh well. 
+ 
+    Anyway, to use you will need to copy the following code somewhere
+> Instance Arbitrary Expr where
+>     arbitrary = expr_arb  
+>     shrink    = gexpr_shrink
+ There is also a gexpr_arb that takes in a generator for the symbol type
+-}
+module Language.Lambda.Untyped.Arbitrary (
+    module Language.Lambda.Common.Arbitrary,
+    expr_arb,
+    gexpr_shrink, 
+    gexpr_arb,
+    gexpr_arb'
+) where
+import Test.QuickCheck
+import Control.Applicative ((<*>), (<$>))
+import Language.Lambda.Untyped.Syntax
+import Language.Lambda.Common.Arbitrary
+
+-- | An arbitrary function for Expr. See the example above.
+expr_arb :: Gen Expr
+expr_arb = gexpr_arb sym_arbitrary
+    
+-- | Shrink function for an GExpr. See the example at the top of the module    
+gexpr_shrink :: GExpr a -> [GExpr a]
+gexpr_shrink x@(Var _) = [x]
+gexpr_shrink (App x y) = [x, y]
+gexpr_shrink (Lam _ y) = [y]
+   
+-- | Helper function for creating generators for GExpr. Takes in a generator for the symbol type
+gexpr_arb :: Gen a -> Gen (GExpr a) 
+gexpr_arb sym_gen = sized $ \x -> gexpr_arb' x sym_gen
+
+-- | Helper function for creating generators for GExpr. Takes in a generator for the symbol type and the
+-- "depth" of the expression tree
+gexpr_arb' :: Int -> Gen s -> Gen (GExpr s)
+gexpr_arb' 0 s_arb = Var <$> s_arb
+gexpr_arb' n s_arb = do
+    option <- choose(0, 2) :: Gen Int
+    case option of
+        0 -> Var <$> s_arb
+        1 -> App <$> gexpr_arb' (n - 1) s_arb <*> gexpr_arb' (n - 1) s_arb
+        2 -> Lam <$> s_arb                    <*> gexpr_arb' (n - 1) s_arb
+        _ -> error "choose messed up!"
+        
diff --git a/src/Language/Lambda/Untyped/Parser.hs b/src/Language/Lambda/Untyped/Parser.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Lambda/Untyped/Parser.hs
@@ -0,0 +1,122 @@
+{-# LANGUAGE FlexibleContexts, DeriveDataTypeable #-}
+{-- | Parser for the lambda AST built of parsec. Converts to an intermediate format for antiexpressions -}
+module Language.Lambda.Untyped.Parser where
+import Text.Parsec
+import Text.Parsec.Language
+import Text.Parsec.Token 
+import Language.Lambda.Untyped.Syntax
+import Data.Functor.Identity
+import Data.List
+import Data.Data
+
+type M = Identity
+
+data MetaExpr s = MVar (MetaSym s)
+              | MApp (MetaExpr s) (MetaExpr s)
+              | MLam (MetaSym s) (MetaExpr s)
+              | AntiExpr String
+              | AntiVar  String
+              deriving(Show, Eq, Data, Typeable)
+              
+data MetaSym s = S s
+               | AntiSym String
+              deriving(Show, Eq, Data, Typeable)
+
+type Output s = MetaExpr s
+
+type SymParser u s = ParsecT String u M s
+
+top_expr :: SymParser u s -> ParsecT String u M (Output s)
+top_expr sp = do 
+    spaces
+    e <- parse_expr sp
+    spaces
+    eof
+    return e
+    
+parse_expr :: SymParser u s -> ParsecT String u M (Output s)
+parse_expr sp = try (parse_aexpr sp)
+          <|> try (parse_lambda sp)
+          <|> try parse_anti_expr
+ 
+parse_aexpr :: SymParser u s -> ParsecT String u M (Output s)
+parse_aexpr sp =  try (parse_app sp)
+              <|> try (parse_atom sp)
+           
+parse_anti_expr :: ParsecT String u M (Output s)
+parse_anti_expr = do
+    _ <- string "$"
+    i <- (identifier haskell)
+    return $ AntiExpr i
+
+parse_lambda :: SymParser u s -> ParsecT String u M (Output s)
+parse_lambda sp = do
+    _ <- char '\\'
+    spaces
+    sym  <- (p_sym sp) <?> "lambda argument"
+    _ <- char '.'
+    spaces
+    expr <- (parse_expr sp) <?> "lambda expression"
+    return $ MLam sym expr
+
+parse_app :: SymParser u s -> ParsecT String u M (Output s)
+parse_app sp = do
+    expr_0 <- (parse_atom sp) <?> "first apply argument"
+    spaces
+    as <-  sepBy1 (parse_atom sp) spaces <?> "other apply arguments"
+    return $ foldl' MApp expr_0 as
+
+parse_atom :: SymParser u s -> ParsecT String u M (Output s)
+parse_atom sp =  try  (parens'  (parse_expr sp))
+          <|> try (parse_var sp)
+          <|> try parse_anti_expr
+          
+parse_var sp = try (parse_var' sp) <|> parse_anti_var 
+          
+parse_var' :: SymParser u s -> ParsecT String u M (Output s)
+parse_var' sp = do
+    spaces
+    sym <- (p_sym sp) <?> "Var symbol"
+    return $ MVar sym  
+ 
+parse_anti_var = do 
+    spaces 
+    _ <- string "*"
+    i <- (identifier haskell)
+    return $ AntiVar i
+    
+p_sym :: SymParser u s -> ParsecT String u M (MetaSym s)
+p_sym sp = try (S `fmap` sp) <|> try parse_anti_sym
+
+parse_anti_sym :: ParsecT String u M (MetaSym s)
+parse_anti_sym = do
+    _ <- string "^"
+    i <- (identifier haskell)
+    return $ AntiSym i
+    
+parse_sym :: ParsecT String u M Sym
+parse_sym = many1 (alphaNum <|> char '_') <?> "symbol"
+
+parens' :: Stream s m Char => ParsecT s u m b -> ParsecT s u m b
+parens' p = do 
+    _ <- char '('
+    e <- p
+    _ <- char ')'
+    return e
+
+meta_to_expr :: MetaExpr s -> GExpr s
+meta_to_expr (MVar (S x))     = Var x
+meta_to_expr (MApp x y)   = App (meta_to_expr x) (meta_to_expr y)
+meta_to_expr (MLam (S x) y)   = Lam x (meta_to_expr y)
+meta_to_expr _ = error "meta_to_expr should not be used if the MetaExpr tree has AntiExpr"
+
+to_meta :: GExpr s -> MetaExpr s
+to_meta (Var x)   = MVar (S x)
+to_meta (App x y) = MApp (to_meta x) (to_meta y)
+to_meta (Lam x y) = MLam (S x) (to_meta y)
+
+
+
+
+
+
diff --git a/src/Language/Lambda/Untyped/Pretty.hs b/src/Language/Lambda/Untyped/Pretty.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Lambda/Untyped/Pretty.hs
@@ -0,0 +1,15 @@
+{-- | Pretty printers for lambda expression -}
+module Language.Lambda.Untyped.Pretty where
+import Language.Lambda.Untyped.Syntax
+
+-- | Pretty prints a Expr
+ppr :: Expr -> String
+ppr (Var x)   = x
+ppr (App x y) = "(" ++ ppr x ++ " " ++ ppr y ++ ")" 
+ppr (Lam x y) = "(\\" ++ x ++ "." ++ ppr y ++ ")"
+
+-- | Pretty prints a GExpr 
+g_ppr :: (Show a) => GExpr a -> String
+g_ppr (Var x)   = show x
+g_ppr (App x y) = "(" ++ g_ppr x ++ " " ++ g_ppr y ++ ")" 
+g_ppr (Lam x y) = "(\\" ++ show x ++ "." ++ g_ppr y ++ ")"
diff --git a/src/Language/Lambda/Untyped/Quote.hs b/src/Language/Lambda/Untyped/Quote.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Lambda/Untyped/Quote.hs
@@ -0,0 +1,88 @@
+{-# LANGUAGE TemplateHaskell, QuasiQuotes, RankNTypes #-}
+module Language.Lambda.Untyped.Quote (lam, g_lam) where
+import Language.Haskell.TH.Quote
+import Language.Haskell.TH
+import Language.Lambda.Untyped.Parser
+import Text.Parsec (runParser)
+import Data.Generics.Aliases
+import Data.Generics.Uniplate.Data
+import Language.Lambda.Untyped.Syntax
+import Data.Data
+import Debug.Trace.Helpers
+ 
+lam :: QuasiQuoter
+lam = g_lam parse_sym
+
+g_lam :: (Data s, Show s) => SymParser () s -> QuasiQuoter
+g_lam sp = QuasiQuoter (g_quoteExprExp sp) (g_quoteExprPat sp) undefined undefined
+
+
+parseExpr :: Monad m => SymParser () s -> (String, Int, Int) -> String -> m (Output s)
+parseExpr sp (file, line, col) s = result where
+    result = case runParser (top_expr sp) () file s of
+                  Left err  -> fail $ (show err ++ " at file " ++ file ++ " at line " ++ 
+                                          show line ++ " at col " ++ show col)
+                  Right e   -> return e
+    
+
+    
+g_quoteExprExp :: (Data s, Show s,  Typeable s) => SymParser () s -> String -> ExpQ
+g_quoteExprExp sp r =  do  
+    loc <- location
+    let pos =  (loc_filename loc,
+             fst (loc_start loc),
+             snd (loc_start loc))
+    parsed_expr <- (parseExpr sp) pos r
+    appE (varE $ mkName "meta_to_expr") $ dataToExpQ (const Nothing `extQ` 
+        (antiExprExp sp)) $ parsed_expr
+             
+antiExprExp :: (Data s, Typeable s) => SymParser () s -> MetaExpr s -> Maybe (Q Exp)
+antiExprExp d (MLam (AntiSym v) x) = Just $ appE (appE (conE $ mkName "MLam") $ appE (conE $ mkName "S") $ varE (mkName v))
+                                         $ dataToExpQ (const Nothing `extQ` (antiExprExp d)) x
+antiExprExp d (MVar (AntiSym v))   = Just $ appE (conE $ mkName "MVar") $ appE (conE $ mkName "S") $ varE (mkName v)
+antiExprExp d (AntiExpr v)         = Just $ appE (varE $ mkName "to_meta") $ varE (mkName v)
+antiExprExp d (AntiVar v)          = Just $ [| MVar (S $(varE $ mkName v)) |]
+antiExprExp _ _                    = Nothing
+
+g_quoteExprPat :: (Data s, Show s, Typeable s) => SymParser () s ->  String -> PatQ
+g_quoteExprPat sp r =  do  
+    loc <- location
+    let pos =  (loc_filename loc,
+             fst (loc_start loc),
+             snd (loc_start loc))
+    parsed_expr <- (parseExpr sp) pos r
+    th_pat <- dataToPatQ (const Nothing `extQ` (antiExprPat sp)) parsed_expr
+    return $ to_e th_pat where
+        to_e p = transform to_e' p
+
+        to_e' (ConP n xs) | show n == "MVar" = ConP (to_expr_name n) [collapse_meta_sym $ head xs]
+        to_e' (ConP n xs) | show n == "MLam" = ConP (to_expr_name n) ((collapse_meta_sym $ head xs):(tail xs))
+        to_e' (ConP n xs) | otherwise        = ConP (to_expr_name n) xs
+        to_e' x = x
+
+        to_expr_name name | show name == "MVar" = mkName "Var" 
+        to_expr_name name | show name == "MApp" = mkName "App" 
+        to_expr_name name | show name == "MLam" = mkName "Lam"
+        to_expr_name name | otherwise           = name
+        
+        collapse_meta_sym (ConP n xs) | nameBase n == "S" = head xs
+        collapse_meta_sym p@(ConP n xs) | otherwise = error ("collapse_meta_sym not used on a S " ++ show p)
+             
+antiExprPat :: (Data s, Typeable s) => SymParser () s -> MetaExpr s -> Maybe (Q Pat)
+antiExprPat d (MLam (AntiSym v) x) = Just $ conP (mkName "MLam") [conP (mkName "S") [varP (mkName v)], 
+                                        dataToPatQ (const Nothing `extQ` (antiExprPat d)) x]
+antiExprPat d (MVar (AntiSym v))   = Just $ conP (mkName "MVar") [conP (mkName "S") [varP (mkName v)]]
+antiExprPat d (AntiExpr v)         = Just $ varP (mkName v)
+antiExprPat d (AntiVar v)          = Just $ conP (mkName "MVar") [conP (mkName "S") [varP $ mkName v]]
+antiExprPat _ _                    = Nothing
+
+
+
+
+
+
+
+
+
+
+