diff --git a/AST.hs b/AST.hs
new file mode 100644
--- /dev/null
+++ b/AST.hs
@@ -0,0 +1,174 @@
+{-# LANGUAGE  
+ DeriveFunctor,
+ FlexibleInstances,
+ PatternGuards
+ #-}
+module AST where
+
+import qualified Data.Foldable as F
+import Data.List
+import Data.Maybe
+import Data.Monoid
+import Data.Functor
+import qualified Data.Map as M
+import qualified Data.Set as S
+--------------------------------------------------------------------
+----------------------- DATA TYPES ---------------------------------
+--------------------------------------------------------------------
+type Name = String
+              
+data Variable = Var  Name
+              | Cons Name
+              deriving (Ord, Eq)
+                       
+data Tm = AbsImp Name Tp Tm
+        | Abs Name Tp Tm
+        | Spine Variable [Tp] 
+        deriving (Eq, Ord)
+                 
+var nm = Spine (Var nm) []
+cons nm = Spine (Cons nm) []
+
+data Constraint a = a :=: a
+                  deriving (Eq, Ord, Functor, Show)
+
+data Tp = Atom Tm
+        | Forall Name Tp Tp
+        | ForallImp Name Tp Tp
+        deriving (Eq, Ord)
+
+data Predicate = Predicate { predName::Name
+                           , predType::Tp 
+                           , predConstructors::[(Name, Tp)]
+                           } 
+               | Query { predName :: Name, predType::Tp }
+               deriving (Eq)
+
+infixl 1 :|-
+data Judgement = (:|-) { antecedent :: [(Name,Tp)] , succedent :: Tp }
+
+
+atom = Atom $ cons "atom"
+
+
+--------------------------------------------------------------------
+----------------------- PRETTY PRINT -------------------------------
+--------------------------------------------------------------------
+instance Show Variable where
+  show (Var n)  = n
+  show (Cons n) = n
+showWithParens t = if (case t of
+                          Forall _ _ _ -> True
+                          Atom (Spine _ lst) -> not $ null lst
+                          Atom (Abs _ _ _) -> True
+                          Atom (AbsImp _ _ _) -> True
+                      ) then "("++show t++")" else show t 
+
+instance Show Tm where
+  show (Abs nm ty tm) = "λ "++nm++" : "++showWithParens ty++" . "++show tm
+  show (AbsImp nm ty tm) = "?λ "++nm++" : "++showWithParens ty++" . "++show tm
+  show (Spine cons apps) = show cons++concatMap (\s -> " "++showWithParens s) apps
+instance Show Tp where
+  show t = case t of
+    Atom t -> show t
+    Forall nm t t' | not (S.member nm (freeVariables t')) -> showWithParens++" → "++ show t'
+      where showWithParens = case t of
+              Forall _ _ _ -> "(" ++ show t ++ ")"
+              _ ->  show t
+    Forall nm ty t -> "∀ "++nm++" : "++show ty++" . "++show t
+    
+    ForallImp nm t t' | not (S.member nm (freeVariables t')) -> showWithParens++" ⇒ "++ show t'
+      where showWithParens = case t of
+              Forall _ _ _ -> "(" ++ show t ++ ")"
+              _ ->  show t
+    ForallImp nm ty t -> "?∀ "++nm++" : "++show ty++" . "++show t
+  
+instance Show Judgement where 
+  show (a :|- b) =  removeHdTl (show a) ++" ⊢ "++ show b
+    where removeHdTl = reverse . tail . reverse . tail    
+
+instance Show Predicate where
+  show (Predicate nm ty []) =  ""++"defn "++nm++" : "++show ty++";"
+  show (Predicate nm ty (a:cons)) = 
+      ""++"defn "++nm++" : "++show ty++"\n"
+      ++  "  as "++showSingle a++concatMap (\x->
+        "\n   | "++showSingle x) cons++";"
+        where showSingle (nm,ty) = nm++" = "++show ty
+  show (Query nm ty) = "query "++nm++" = "++show ty
+
+--------------------------------------------------------------------
+----------------------- SUBSTITUTION -------------------------------
+--------------------------------------------------------------------
+type Substitution = M.Map Name Tm
+
+infixr 1 |->
+infixr 0 ***
+m1 *** m2 = M.union m2 (subst m2 <$> m1)
+(|->) = M.singleton
+(!) = flip M.lookup
+
+
+rebuildSpine :: Tm -> [Tp] -> Tm
+rebuildSpine s [] = s
+rebuildSpine (Spine c apps) apps' = Spine c (apps ++ apps')
+rebuildSpine (Abs nm _ rst) (a:apps') = rebuildSpine (subst (nm |-> tpToTm a) $ rst) apps'
+
+newName nm s = (nm',s')
+  where s' = if nm == nm' then s else M.insert nm (var nm') s 
+        nm' = fromJust $ find free $ nm:map (\s -> show s ++ "/") [0..]
+        fv = mappend (M.keysSet s) (freeVariables s)
+        free k = not $ S.member k fv
+
+class Subst a where
+  subst :: Substitution -> a -> a
+instance (Functor f , Subst a) => Subst (f a) where
+  subst foo t = subst foo <$> t
+instance Subst Tm where
+  subst s (Abs nm t rst) = Abs nm' (subst s t) $ subst s' rst
+    where (nm',s') = newName nm s
+  subst s (AbsImp nm t rst) = AbsImp nm' (subst s t) $ subst s' rst
+    where (nm',s') = newName nm s          
+  subst s (Spine head apps) = let apps' = subst s <$> apps  in
+    case head of
+      Var nm | Just head' <- s ! nm -> rebuildSpine head' apps'
+      _ -> Spine head apps'
+instance Subst Tp where
+  subst s t = case t of
+    Atom t -> Atom $ subst s t
+    ForallImp nm ty t -> ForallImp nm' (subst s ty) $ subst s' t  -- THIS RULE is unsafe capture!
+        where (nm',s') = newName nm s
+    Forall nm ty t -> Forall nm' (subst s ty) $ subst s' t  -- THIS RULE is unsafe capture!
+        where (nm',s') = newName nm s
+instance Subst Judgement where 
+  subst foo (c :|- s) = subst foo c :|- subst foo s
+
+--------------------------------------------------------------------
+----------------------- FREE VARIABLES -----------------------------
+--------------------------------------------------------------------
+class FV a where         
+  freeVariables :: a -> S.Set Name
+  
+instance (FV a, F.Foldable f) => FV (f a) where
+  freeVariables m = F.foldMap freeVariables m
+instance FV Tp where
+  freeVariables t = case t of
+    Forall a ty t -> (S.delete a $ freeVariables t) `S.union` (freeVariables ty)
+    ForallImp a ty t -> (S.delete a $ freeVariables t) `S.union` (freeVariables ty)
+    Atom a -> freeVariables a
+instance FV Tm where
+  freeVariables t = case t of
+    Abs nm t p -> S.delete nm $ freeVariables p
+    AbsImp nm t p -> S.delete nm $ freeVariables p    
+    Spine head others -> mappend (freeVariables head) $ mconcat $ freeVariables <$> others
+instance FV Variable where    
+  freeVariables (Var a) = S.singleton a
+  freeVariables _ = mempty
+instance (FV a,FV b) => FV (a,b) where 
+  freeVariables (a,b) = freeVariables a `S.union` freeVariables b
+  
+class ToTm t where
+  tpToTm :: t -> Tm
+instance ToTm Tp where
+  tpToTm (Forall n ty t) = Spine (Cons "forall") [Atom $ Abs n ty $ tpToTm t ]
+  tpToTm (ForallImp n ty t) = AbsImp n ty $ tpToTm t
+  tpToTm (Atom tm) = tm
diff --git a/Choice.hs b/Choice.hs
new file mode 100644
--- /dev/null
+++ b/Choice.hs
@@ -0,0 +1,78 @@
+{-# LANGUAGE 
+ DeriveFunctor, 
+ FlexibleContexts,
+ TypeSynonymInstances
+ #-}
+
+module Choice where
+import Control.Monad
+import Data.Functor
+import Control.Applicative
+import Control.Monad.Error (ErrorT, runErrorT)
+import Control.Monad.Error.Class (catchError, throwError, MonadError)
+import Control.Monad.State.Class
+import Control.Monad.Trans.Class
+import Control.Monad.Trans.Maybe
+import Data.Maybe
+
+data Choice a = Choice a :<|>: Choice a 
+              | Fail String
+              | Success a
+              deriving (Functor)
+
+instance Monad Choice where 
+  fail a = Fail a
+  return = Success
+  Fail a >>= _ = Fail a
+  (m :<|>: m') >>= f = (m >>= f) :<|>: (m' >>= f)
+  Success a >>= f = f a
+  
+instance Applicative Choice where  
+  pure = Success
+  mf <*> ma = mf >>= (<$> ma)
+  
+instance Alternative Choice where
+  empty = Fail ""
+  (<|>) = (:<|>:)
+        
+instance MonadPlus Choice where        
+  mzero = Fail ""
+  mplus = (:<|>:)
+  
+class RunChoice m where  
+  runError :: m a -> Either String a
+  
+instance RunChoice Choice where
+  runError chs = case dropWhile notSuccess lst of
+    [] -> case dropWhile notFail lst of 
+      Fail a:_ -> Left a
+      _ -> error "this result makes no sense"
+    (Success a):_ -> Right a
+    _ -> error "this result makes no sense"
+    where lst = chs:queue lst 1
+          
+          queue l 0 = []
+          queue ((a :<|>: b):l) q = a:b:queue l (q + 1)
+          queue (_:l) q = queue l (q - 1)
+          
+          notFail (Fail a) = False
+          notFail _ = True
+          
+          notSuccess (Success a) = False
+          notSuccess _ = True
+  
+appendErr :: (MonadError String m) => String -> m a -> m a
+appendErr s m = catchError m $ \s' -> throwError $ s' ++ "\n" ++ s
+  
+instance MonadError String Choice where
+  throwError a = Fail a
+  catchError try1 foo_try2 = case runError try1 of
+    Left s -> foo_try2 s
+    Right a -> Success a
+
+getNew :: (MonadState Integer m) => m String
+getNew = do 
+  st <- get
+  let n = 1 + st
+  put n
+  return $! show n
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,320 @@
+                    GNU GENERAL PUBLIC LICENSE
+                       Version 3, 29 June 2007
+
+ Copyright (C) 2007 Free Software Foundation, Inc. <http://fsf.org/>
+ Everyone is permitted to copy and distribute verbatim copies
+ of this license document, but changing it is not allowed.
+
+                            Preamble
+
+  The GNU General Public License is a free, copyleft license for
+software and other kinds of works.
+
+  The licenses for most software and other practical works are designed
+to take away your freedom to share and change the works.  By contrast,
+the GNU General Public License is intended to guarantee your freedom to
+share and change all versions of a program--to make sure it remains free
+software for all its users.  We, the Free Software Foundation, use the
+GNU General Public License for most of our software; it applies also to
+any other work released this way by its authors.  You can apply it to
+your programs, too.
+
+  When we speak of free software, we are referring to freedom, not
+price.  Our General Public Licenses are designed to make sure that you
+have the freedom to distribute copies of free software (and charge for
+them if you wish), that you receive source code or can get it if you
+want it, that you can change the software or use pieces of it in new
+free programs, and that you know you can do these things.
+
+  To protect your rights, we need to prevent others from denying you
+these rights or asking you to surrender the rights.  Therefore, you have
+certain responsibilities if you distribute copies of the software, or if
+you modify it: responsibilities to respect the freedom of others.
+
+  For example, if you distribute copies of such a program, whether
+gratis or for a fee, you must pass on to the recipients the same
+freedoms that you received.  You must make sure that they, too, receive
+or can get the source code.  And you must show them these terms so they
+know their rights.
+
+  Developers that use the GNU GPL protect your rights with two steps:
+(1) assert copyright on the software, and (2) offer you this License
+giving you legal permission to copy, distribute and/or modify it.
+
+  For the developers' and authors' protection, the GPL clearly explains
+that there is no warranty for this free software.  For both users' and
+authors' sake, the GPL requires that modified versions be marked as
+changed, so that their problems will not be attributed erroneously to
+authors of previous versions.
+
+  Some devices are designed to deny users access to install or run
+modified versions of the software inside them, although the manufacturer
+can do so.  This is fundamentally incompatible with the aim of
+protecting users' freedom to change the software.  The systematic
+pattern of such abuse occurs in the area of products for individuals to
+use, which is precisely where it is most unacceptable.  Therefore, we
+have designed this version of the GPL to prohibit the practice for those
+products.  If such problems arise substantially in other domains, we
+stand ready to extend this provision to those domains in future versions
+of the GPL, as needed to protect the freedom of users.
+
+  Finally, every program is threatened constantly by software patents.
+States should not allow patents to restrict development and use of
+software on general-purpose computers, but in those that do, we wish to
+avoid the special danger that patents applied to a free program could
+make it effectively proprietary.  To prevent this, the GPL assures that
+patents cannot be used to render the program non-free.
+
+  The precise terms and conditions for copying, distribution and
+modification follow.
+
+                       TERMS AND CONDITIONS
+
+  0. Definitions.
+
+  "This License" refers to version 3 of the GNU General Public License.
+
+  "Copyright" also means copyright-like laws that apply to other kinds of
+works, such as semiconductor masks.
+
+  "The Program" refers to any copyrightable work licensed under this
+License.  Each licensee is addressed as "you".  "Licensees" and
+"recipients" may be individuals or organizations.
+
+  To "modify" a work means to copy from or adapt all or part of the work
+in a fashion requiring copyright permission, other than the making of an
+exact copy.  The resulting work is called a "modified version" of the
+earlier work or a work "based on" the earlier work.
+
+  A "covered work" means either the unmodified Program or a work based
+on the Program.
+
+  To "propagate" a work means to do anything with it that, without
+permission, would make you directly or secondarily liable for
+infringement under applicable copyright law, except executing it on a
+computer or modifying a private copy.  Propagation includes copying,
+distribution (with or without modification), making available to the
+public, and in some countries other activities as well.
+
+  To "convey" a work means any kind of propagation that enables other
+parties to make or receive copies.  Mere interaction with a user through
+a computer network, with no transfer of a copy, is not conveying.
+
+  An interactive user interface displays "Appropriate Legal Notices"
+to the extent that it includes a convenient and prominently visible
+feature that (1) displays an appropriate copyright notice, and (2)
+tells the user that there is no warranty for the work (except to the
+extent that warranties are provided), that licensees may convey the
+work under this License, and how to view a copy of this License.  If
+the interface presents a list of user commands or options, such as a
+menu, a prominent item in the list meets this criterion.
+
+  1. Source Code.
+
+  The "source code" for a work means the preferred form of the work
+for making modifications to it.  "Object code" means any non-source
+form of a work.
+
+  A "Standard Interface" means an interface that either is an official
+standard defined by a recognized standards body, or, in the case of
+interfaces specified for a particular programming language, one that
+is widely used among developers working in that language.
+
+  The "System Libraries" of an executable work include anything, other
+than the work as a whole, that (a) is included in the normal form of
+packaging a Major Component, but which is not part of that Major
+Component, and (b) serves only to enable use of the work with that
+Major "Major Component", in this context, means a major essential component
+(kernel, window system, and so on) of the specific operating system
+(if any) on which the executable work r, it does not include the work's
+System Libraries, or general-purpose tools or generally available free
+programs which are used unmodified in performing those activities but
+which are not part of the work.  For eose
+subprograms and other parts of the work.
+
+  The Corresponding Source need not include anything that users
+can regenerate automatically from other parts of the  work.
+
+  2. Basic Permissions.
+
+  All rights gran unmodified Program.  The output from running a
+covered work is covered by this
+
+  You may make, run and propagate covered works that you do not
+convey, without conditions so long as your license otherwise remainyou, or proively on your behalf, under your direction
+and control, on terms that prohibit them from making any copies of
+your copyrighted material outside their relationship with you.
+
+  Conveying under any otherg obligations under article
+11 of the WIPO copyright treaty adopted on 20 December 1996, or
+similar laws prohibiting or restricting circumvention of such
+measures.
+
+  When you convey a covered work, you waive any k's
+users, your or third parties' legal rights to forbidsly and
+appropriately publish on each copy an appropriate copyright notice;
+keep intact all notices stating that this License and any
+non-permissive terms amay convey a work based on the Program, or the modifications to
+produce it from the Program, in the form of source code under the
+terms of section 4, provided that you also meet all of these conditions:
+
+    a) T
+    "keep intact all notices".
+
+    c) You must license the entire work, as a whole, under this
+    License to anyone who comes into possession of a copy.  This
+    License will therefore apply, along with any ae work has interactive user interfaces, each must display
+    Appropriate Legal Notices; however, if the Program has interactive
+    interfaces that do not display Apered work with other separate and independent
+regate" if the compilation and its resulting copyright are not
+used to limit the access or legal rights of the c the other
+parts of the aggregate.
+
+  6. Conveying Non-Source Forms.
+
+  You may convey a covered woricensware interchange.
+
+    b) Convey the object code in, or embodied in, a physical product
+    (including a physical distribution medium), accompanied by a
+    written offer, valid for at least three years and ly used for software interchange, for a price no
+    more than your reasonable cost of physically performing this
+    conveying of source, or (2) access to copy the
+    Correes of the object code with a copy of tection 6b.
+
+    d) Convey the object code by offering access from a designated
+    place (gratis or for a charge),quire recipients to copy the
+    Corresponding Source along with the object code.  If the place toequival  available for as long as needed to satisfy these requirements.
+
+    e) Convey the object code using peer-to-peer transmission, provided
+    you inform other peers where the object code and Corresponding
+her (1) a "consumer product", which means any
+tangible personal property which is normally used for personal, family,
+or household purposes, or (2) anything designed or sold for incorporation
+into a dwelling.  Inway in which the particular user
+ly significant mode of use of the product.
+
+  "Installation Information" for a User Product means any methods,
+procedures, authorization keys, or other information required to insbject code work under this section in, or with, or
+specifically for use in, a User Product, and the conveying occurs as
+part of a transaction in which the right of possession and use of the
+User Product is transf ability to install
+modified object code on the User Product (for example, the work has
+been installed in ROM).
+
+  The requirement to provide Installation Information does not include a
+requirement to continue totwork or violates the rules and
+protocols for communica available to the public in
+source code form), and must require no special password or key for
+unpacking, reading or copying.
+
+  7. Additional Terms.
+
+  "Addpart of the Program, that part may be used separately
+under those permissions, but the entire Program remains governed by
+this License without regard to the additional permissions.
+
+  When you convey a copy of a  work,
+for which you have or can give appropriate copyright permission.
+
+  Notwithstanding any other provision of this License, for material you
+add to a covered work, you may (if authorized by the copyright f thaterial or in the Apt from the original version; or
+
+    d) Limiting the use for publicity purposes of names of licensors or
+    authors of the material; or
+
+    e) Declining to grant rights under trademark law fsumptions directly impose on
+    those licensors and authors.
+
+  All other non-permissive additional terms are considered "further
+restrictions" within the meaning of section 10.  If the Program as you
+received itmaterial governed by the terms
+of that license document, provided that the further restriction does
+not survive such relicensing or conveying.
+
+  If you add terms to a covered work in accord with this section, yo
+the above requirements apply either way.
+
+  8. Termination.
+
+  You may not propagate or rights under
+this License (including any patent licenses granted under the third
+paragraph of section 11).
+
+  However, if y particular copyright holder is
+reinstated permanently if the copyright holder notifies you of the
+violation by some reasonable means, this is the first time you have
+received notice of violation of this License en terminated and not permanently
+reinstated, you do not qualify to receive new licenses for the same
+material under section 10.
+
+  9. Acceptance Not Required for Having Copies.
+
+  You are not required to accepy agate or
+modify any covered work.  These actions infringe copyright if you do
+not accept this License.  Therefore, by ecipients.
+
+  Each time you convey a covered work, the recipient automatically
+receives a licey transaction, each party to that
+transaction who receives a copy of the work also receives whatever
+licenses to the work the party's predecessor in interest had or could
+give under the previous paragraph, plus a ot impose a license fee, royalty, or other charge for exercise of
+rights granted under this License, and you may not initiate litigation
+(including a cross-claim or counterclaim in a lawsuit) allling, offering fd the contributor's "contributor version".
+
+  A contributor's "essential patent claims" are all patent claims
+owned oLicense, of making, using, or selling its contributor version,
+but do not include claims that wimport and otherwise run, modify and
+propagate the contents of its contributor version.
+
+  In the following three paragraphs, a "patent license" is any express
+agreement or commitment, however denominated, not toing on a patent license,
+and the Corresponding Source of the work is not available for anyone
+to copy, free of charge and under the terms of this1) cause the Corresponding Source to be so
+available, or (2) arrangse to downstream recipients.  "Knowingly relying" means you have
+actual kble patents in that
+country that you have reason to believe are valid.
+
+  If, pursuant to or in connection with a single transaction or
+arratent license is "discriminatory" if it does not include within
+the scope of its coverage, prohibits the exercise of, or is
+conditioned on the non-exercise of one or more of the rights that are
+specifically grantrty grants, to any of the
+parties who would receive the covered work from you, a discriminatory
+patent license (a) in connection with copies of the c specific products or compilations that
+contain the covered workse orions of this License, they do not
+excuse you from the conditions of this License.  If you cannot convey a
+covered work so as to satisfy simultaneously your obligations under this
+License and any other pertinom conveying the Program.
+
+  13. Use with the GNU Affero General Public License.
+
+  Notwithstanding any other provision of this License, you have
+permission to link or combine any covered work with a work licensening interaction through a network will apply to the
+combination as such.
+
+  14. Revised Versions of this License.
+
+  The Free Software Foundation may pubns will
+be similar in spirit to the present version, but m License "or any later version" ap the
+GNU General Public License, you may choose any version ever published
+by the Free Software Foundation.
+
+  If the Program specifies that a proxy can decide which future
+versis a result of your choosing to follow a
+later version.
+
+  15. Disclaimer of Warranty.
+
+  THERE IS NO WARRANTY FOR THE PROGRAM, TO THE EXTENT PERMITTED BY
+APPLICABLE LAW.  EXCEPT WHEN OTHERWISE STATED IN WRITING TOGRAM
+IS WITH YOU.  SHOULD THE PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF
+ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
+
+  16. Limitation of Liability.
+
+  IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGITED TO LOSS OF
+DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD
+PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER PROGRAMS),
+EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN A7. ute waiver of all civil liability in connection with the
+Program, unless a warranty or assumption of liability accompanies a
+copy of the Program in return for a Your New Programs
diff --git a/Main.hs b/Main.hs
new file mode 100644
--- /dev/null
+++ b/Main.hs
@@ -0,0 +1,50 @@
+module Main where
+
+import AST
+import Choice
+import Solver
+import Parser
+import System.Environment
+import Data.Foldable as F (msum, forM_)
+import Data.Functor
+import Data.List (partition)
+import Text.Parsec
+import Data.Monoid
+
+-----------------------------------------------------------------------
+-------------------------- MAIN ---------------------------------------
+-----------------------------------------------------------------------
+checkAndRun decs = do
+  
+  putStrLn "\nTYPE CHECKING: "
+  decs <- case runError $ typeCheckAll $ decs of
+    Left e -> error e
+    Right e -> do putStrLn "Type checking success!" >> return e
+  let (predicates, targets) = flip partition decs $ \x -> case x of 
+        Predicate _ _ _ -> True
+        _ -> False
+
+  
+  putStrLn $ "\nAXIOMS: "
+  forM_ predicates  $ \s -> putStrLn $ show s++"\n"
+  
+  putStrLn $ "\nTARGETS: "
+  forM_ targets  $ \s -> putStrLn $ show s++"\n"
+
+  let allTypes c = (predName c, predType c):predConstructors c
+  forM_ targets $ \target -> 
+    case solver (concatMap allTypes predicates) $ predType target of
+      Left e -> putStrLn $ "ERROR: "++e
+      Right sub -> putStrLn $ 
+                   "\nTARGET: \n"++show target
+                   ++"\n\nSOLVED WITH:\n"
+                   ++concatMap (\(a,b) -> a++" => "++show b++"\n") sub
+
+main = do
+  [fname] <- getArgs
+  file <- readFile fname
+  let mError = runP decls (ParseState 0 mempty) fname file
+  decs   <- case mError of
+    Left e -> error $ show e
+    Right l -> return l
+  checkAndRun decs 
diff --git a/Parser.hs b/Parser.hs
new file mode 100644
--- /dev/null
+++ b/Parser.hs
@@ -0,0 +1,151 @@
+{-# LANGUAGE RecordWildCards, TupleSections #-}
+module Parser where
+
+import AST
+
+import Data.Foldable as F (msum, forM_)
+import Data.Functor
+import Text.Parsec.String
+import Text.Parsec
+import Data.Monoid
+import Control.Monad (unless)
+import Text.Parsec.Language (haskellDef)
+import Text.Parsec.Expr
+import Data.Maybe
+import qualified Text.Parsec.Token as P
+import qualified Data.Set as S
+
+-----------------------------------------------------------------------
+-------------------------- PARSER -------------------------------------
+-----------------------------------------------------------------------
+
+data ParseState = ParseState { currentVar :: Integer, currentSet :: S.Set Name }
+
+modifySet f s = s { currentSet = f $ currentSet s }
+modifyVar f s = s { currentVar = f $ currentVar s }
+
+getNextVar = do
+  v <- currentVar <$> getState
+  modifyState $ modifyVar (+1)
+  return $ show v++"@?_?"
+
+decls = do
+  whiteSpace
+  lst <- many (query <|> defn <?> "declaration")
+  eof
+  return lst
+
+query = do 
+  reserved "query" 
+  (nm,ty) <- named dec_pred
+  optional semi
+  return $ Query nm ty
+
+defn =  do
+  reserved "defn" 
+  (nm,ty) <- named dec_tipe
+  let more =  do reserved "as"
+                 lst <- flip sepBy1 (reservedOp "|") $ named dec_pred
+                 optional semi
+                 return $ Predicate nm ty lst
+      none = do optional semi
+                return $ Predicate nm ty []
+  more <|> none <?> "definition"
+
+pAtom =  do reserved "_"
+            nm <- getNextVar
+            return $ var nm
+     <|> do r <- id_var
+            return $ var r
+     <|> do r <- identifier
+            mp <- currentSet <$> getState 
+            return $ (if S.member r mp then var else cons) r
+
+     <|> (tpToTm <$> parens tipe)
+     <?> "atom"
+  
+trm =  parens trm 
+   <|> do reservedOp "λ" <|> reservedOp "\\"
+          (nm,tp) <- parens anonNamed <|> anonNamed
+          reservedOp "."
+          tp' <- tmpState nm trm
+          return $ AbsImp nm tp tp'
+   <|> do reservedOp "?λ" <|> reservedOp "?\\"
+          (nm,tp) <- parens anonNamed <|> anonNamed
+          reservedOp "."
+          tp' <- tmpState nm trm
+          return $ Abs nm tp tp'          
+   <|> do t <- pAtom
+          tps <- many $ (parens tipe) <|> (Atom <$> pAtom)
+          return $ rebuildSpine t tps
+   <?> "term"
+
+fall = Forall ""
+fallImp = ForallImp ""
+
+table = [ [ binary (reservedOp "->" <|> reservedOp "→") fall AssocRight
+          , binary (reservedOp "=>" <|> reservedOp "⇒") fallImp AssocRight
+          ] 
+        , [ binary (reservedOp "<-" <|> reservedOp "←") (flip fall) AssocLeft
+          , binary (reservedOp "<=" <|> reservedOp "⇐") (flip fallImp) AssocLeft ]
+        ]
+  where  binary  name fun assoc = Infix (name >> return fun) assoc
+         
+ 
+dec_tipe = (getId lower, ":")
+dec_pred = (getId lower, "=")
+id_var = getId $ upper <|> char '\''
+dec_anon = (getId $ letter <|> char '\'' , ":")
+
+named (ident, sep) = do
+  nm <- ident
+  reservedOp sep
+  ty <- tipe
+  return (nm, ty)
+
+anonNamed = do
+  let (ident,sep) = dec_anon 
+  nm <- ident
+  ty <- optionMaybe $ reservedOp sep >> tipe
+  nm' <- getNextVar
+  return (nm,fromMaybe (Atom $ var nm') ty)
+
+tmpState nm m = do
+  s <- currentSet <$> getState
+  let b = S.member nm s
+  modifyState $ modifySet (S.insert nm)
+  r <- m
+  unless b $ modifyState $ modifySet $ S.delete nm
+  return r
+
+tipe = buildExpressionParser table ( 
+        parens tipe
+    <|> (Atom <$> trm)
+    <|> do (nm,tp) <- brackets anonNamed 
+           tp' <- tmpState nm tipe
+           return $ Forall nm tp tp'
+    <|> do (nm,tp) <- braces anonNamed 
+           tp' <- tmpState nm tipe
+           return $ ForallImp nm tp tp'           
+    <|> do reservedOp "∀" <|> reserved "forall"
+           (nm,tp) <- parens anonNamed <|> anonNamed
+           reservedOp "."
+           tp' <- tmpState nm tipe
+           return $ Forall nm tp tp'
+    <|> do reservedOp "?∀" <|> reserved "?forall"
+           (nm,tp) <- parens anonNamed <|> anonNamed
+           reservedOp "."
+           tp' <- tmpState nm tipe
+           return $ ForallImp nm tp tp'           
+    <?> "type")
+  
+           
+P.TokenParser{..} = P.makeTokenParser $ mydef
+mydef = haskellDef 
+ { P.identStart = lower
+ , P.identLetter = alphaNum <|> oneOf "_'-/"
+ , P.reservedNames = ["defn", "as", "query", "forall", "?forall", "_"]
+ , P.caseSensitive = True
+ , P.reservedOpNames = ["->", "=>", "<=", "⇐", "⇒", "→", "<-", "←", ":", "|", "\\","?\\", "λ","?λ","∀","?∀", "."]
+ }
+getId start = P.identifier $ P.makeTokenParser $ mydef { P.identStart = start }
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,122 @@
+Caledon Language
+================
+
+Caledon is a dependently typed, polymorphic, higher order logic programming language. ie, everything you need to have a conversation with your computer.
+
+Background
+----------
+
+* This is part of my masters thesis.  Feedback would be appreciated. Considering this, it is still in the very early research stages.  Syntax is liable to change, there will be bugs, and it doesn't yet have IO (I'm still working out how to do IO cleanly, but this WILL come).
+
+* Its named caledon after the "New Caledonian Crow" - a crow which can make tools and meta tools.  Since this language supports meta programming with holes, implicits, polymorphism, and dependent types, I thought this crow might be a good masscot. Also, file extensions are ".ncc"
+
+* This language was inspired by twelf, haskell and agda.  
+
+Goals
+-----
+
+* Make logic programming less repetative
+
+* A logic programming language that is good at defining DSLs
+
+* A language/system for conversing with the machine in a manner less one sided and instructional than regular programming.
+
+Philosophies 
+------------
+
+* Metaprogramming should be easy and thus first class.
+
+* User facing code should not crash - runtime code should be type checked.
+
+* Metacode should be optionally typechecked, but well type checked.
+
+* Metaprogramming should not require AST traversal.  
+
+* your programming language should be turing complete - totality checking is annoying.
+
+* Syntax should be elegant.
+
+* Primitives should be minimal, libraries should be extensive.  Learning a culture is easy if you speak the language.  Learning a language by cultural immersion isn't as trivial.
+
+Features
+--------
+
+* Logic programming:  Currently it uses a breadth first proof search. This is done for completeness, since the proof search is also used in type inference.  This could (and should) possibly change in the future for the running semantics of the language.  
+
+``` 
+defn num  : atom
+  as zero = num
+   | succ = num -> num
+
+defn add  : num -> num -> num -> atom
+  as add_zero = {N} add zero N N
+   | add_succ = {N}{M}{R} add (succ N) M (succ R) <- add N M R
+
+-- we can define subtraction from addition!
+query subtract = add (succ (succ zero)) 'v (succ (succ (succ zero)))
+```
+* Higher order logic programming: like in twelf and lambda-prolog.  This makes HOAS much easier to do.  
+
+``` 
+defn trm : atom
+  as lam = (trm -> trm) -> trm
+   | app = trm -> trm -> trm
+
+-- we can check that a term is linear!
+defn linear : (trm → trm) → atom
+  as linear_var = linear ( λ v . v )
+   | linear_app1 = {V}{F} linear (λ v . app (F v) V) 
+                        ← linear F
+   | linear_app2 = ?∀ V . ?∀ F . linear (λ v . app F (V v)) 
+                               ← linear V
+```
+
+* Polymorphism:  This isn't sound. ie, atom : atom.  The unsoundness shouldn't be too problematic, since types are used for proof search and to ensure progress and not for theorem proving.  This language doesn't support totality, worlds, or universe checking yet, since it's goal is to be a query programming language.
+
+``` 
+defn maybe   : atom → atom
+  as nothing = {a} maybe a
+   | just    = {a} a → maybe a
+```
+
+* Indulgent type inferring nondeterminism:  The entire type checking process is a nondeterministic search for a type check proof.  This could be massively slow, but at least it is complete.  The size of this search is bounded by the size of the types and not the whole program, so this shouldn't be too slow in practice.  (function cases should be small).  I'm working on adding search control primitives to make this more efficient.
+
+* Holes:  types can have holes, terms can have holes.  The same proof search that is used in semantics is used in type inference, so you can use the same computational reasoning you use to program to reason about whether the type checker can infer types!  Holes get filled by a proof search on their type and the current context.  Since the entire type checking process is nondeterministic, if they get filled by a wrong term, they can always be filled again.
+
+``` 
+defn fsum_maybe  : {a}{b} (a -> b -> atom) -> maybe a -> maybe b → atom
+  as fsum_nothing = {a}{b}[F : a -> b -> atom] maybe_fsum F nothing nothing
+   | fsum_just    = {a}{b}[F : _ -> _ -> atom][av : a][bv : b]
+                   maybe_fsum F (just av) (just bv)
+                   <- F av bv
+```
+
+* Implicit arguments:  These are arguments that automagically get filled with holes when they need to be.  They form the basis for typeclasses (records to be added), although they are far more general. This is also where the language is most modern and interesting.  I'm curious to see what uses beyond typeclasses there are for these.
+
+``` 
+defn functor : (atom → atom) → atom
+  as isFunctor = ∀ F . ({a}{b : _ } (a → b → atom) → F a → F b → atom) → functor F.
+
+defn fsum : {F} functor F => {a}{b} (a → b → atom) → F a → F b → atom
+  as get_fsum = [F] functor F -> [FSUM][Foo][Fa][Fb] FSUM Foo Fa Fb -> fsum Foo Fa Fb
+
+defn functor_maybe : functor maybe -> atom.
+  as is_functor_maybe = functor_maybe (isFunctor fsum_maybe).
+
+-- this syntax is rather verbose for the moment.  I have yet to add proper records or typeclass syntax sugar.
+```
+
+* Optional unicode syntax: Monad m ⇒ ∀ t : goats . m (λ x : t . t → t).  
+    * implication :  "a -> b"  or "a → b" or "a <- b"  or "a ← b" 
+    * implicits:  "a => b"  or "a ⇒ b" 
+    * Quantification: "[x:A] t"  or  "∀ x:A . t" or "forall x:A . t"
+    * abstraction: "λ x . t" or "\x.t"
+    * Quantified implicits: "{x:A} t"  or  "?∀ x:A . t" or "?forall x:A . t"
+
+
+Usage
+-----
+
+* To install, cabal install
+
+* To run, caledon file.ncc
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,3 @@
+import Distribution.Simple
+
+main = defaultMain
diff --git a/Solver.hs b/Solver.hs
new file mode 100644
--- /dev/null
+++ b/Solver.hs
@@ -0,0 +1,356 @@
+{-# LANGUAGE 
+ FlexibleContexts,  
+ FlexibleInstances,
+ TupleSections
+ #-}
+module Solver where
+
+import AST
+import Choice
+
+import Control.Monad (void)
+import Control.Applicative ((<|>), empty)
+import Control.Monad.Error (ErrorT, throwError, runErrorT, lift, unless, when)
+import Control.Monad.Error.Class
+import Control.Monad.State (StateT, get, put, runStateT, modify)
+import Control.Monad.State.Class
+import Control.Monad.Writer (WriterT, runWriterT, listens)
+import Control.Monad.Writer.Class
+import Control.Monad.RWS (RWST, RWS, get, put, tell, runRWST, runRWS, ask)
+import Control.Monad.Identity (Identity, runIdentity)
+import Control.Monad.Trans.Class
+import Data.Monoid
+import Data.Functor
+import Data.Traversable (forM)
+import Data.Foldable as F (msum, forM_, foldr', foldl', fold, Foldable, foldl')
+import qualified Data.Map as M
+import qualified Data.Set as S
+import Debug.Trace
+
+--------------------------------------------------------------------
+----------------------- UNIFICATION --------------------------------
+--------------------------------------------------------------------
+type VarGen = StateT Integer Choice
+
+
+class HasVar a where
+  getV :: a -> Integer
+  setV :: Integer -> a -> a
+instance HasVar Integer where  
+  getV = id
+  setV a _ = a
+      
+unifyAll envE env [] = return mempty
+unifyAll envE env (a:l) = do
+  s <- appendErr ("IN: "++show a) $ unify envE env a
+  s' <- unifyAll envE env (subst s l)
+  return $ s *** s'
+
+unify :: M.Map Name Tp -> M.Map Name Tp -> Constraint Tm -> VarGen Substitution
+unify envE env constraint@(a :=: b) = 
+  let badConstraint = throwError $ show constraint
+      unify'' = unify envE env
+      unify' = unify envE
+      doUntoBoth m n = F.foldl' act (return mempty) (zip m n)
+      act prev (mt,nt) = do
+        sub <- prev 
+        sub' <- unify' (subst sub env) $ subst sub (tpToTm mt :=: tpToTm nt)
+        return $ sub *** sub'
+
+  in case a :=: b of
+    _ :=: _ | a > b -> unify' env $ b :=: a
+    AbsImp n ty t :=: _ -> do
+      (v',s) <- solve $ (M.toList envE)++(M.toList env) :|- ty
+      unify' env $ subst s (subst (n |-> v') t) :=: (subst s b)
+    Abs n ty t :=: Abs n' ty' t' -> do  
+      s <- unify'' $ tpToTm ty :=: tpToTm ty'
+      nm <- getNew
+      s' <- unify' (subst s $ M.insert nm ty env) $ subst (M.insert n (var nm) s) t :=: subst (M.insert n' (var nm) s) t'
+      return $ s *** M.delete nm s'
+    Abs n ty t :=: _ -> do  
+      nm <- getNew
+      s <- unify' (M.insert nm ty env) $ subst (n |-> var nm) t :=: rebuildSpine b [Atom $ var nm]
+      return $ M.delete nm s
+    
+    Spine (Var a) [] :=: Spine (Var a') [] | a == a' -> 
+      return mempty
+    Spine (Var a) [] :=: _ | not (M.member a env) && (not $ S.member a $ freeVariables b) -> 
+      return $ a |-> b
+    Spine (Var a) m :=: Spine (Var a') n | a == a' && M.member a env && length m == length n ->  -- the var has the same rule whether it is quantified or not.
+      doUntoBoth m n
+      
+    Spine (Cons c) _ :=: Spine (Cons c') _ | c /= c' -> 
+      badConstraint
+    Spine (Cons c) m :=: Spine (Cons c') n | length m == length n -> 
+      doUntoBoth m n
+      
+    Spine (Var x) n :=: Spine (Cons c) m | not $ M.member x env -> do -- Gvar-Const
+      us <- forM n $ const $ getNew
+      usty <- forM n $ const $ Atom <$> var <$> getNew
+      xs <- forM m $ const $ Var <$> getNew
+      let l = Spine (Cons c) $ (\xi -> Atom $ Spine xi $ Atom <$> var <$> us) <$> xs
+          s = x |-> foldr' (\(v,ty) t -> Abs v ty t) l (zip us usty)
+      s' <- unify' (subst s env) $ subst s (a :=: b)
+      return $ (s *** s')
+      
+    Spine (Var a) n :=: Spine (Var a') m | a == a' && length m == length n -> do -- Gvar-Gvar - same
+      h <- getNew
+      let act (xi, yi) next = do
+            vi <- getNew
+            sub' <- catchError (Just <$> unify'' (tpToTm xi :=: tpToTm yi)) $ \_ -> return Nothing
+            (xs,zs,sub) <- next
+            case sub' of
+              Just sub' -> return (vi:xs,vi:zs, sub' *** sub)              
+              Nothing   -> return (vi:xs,zs, sub)
+                
+      (xs,zs,sub) <- foldr' act (return (mempty, mempty, mempty)) (zip n m)
+      
+      let base = Spine (Var h) (Atom <$> var <$> zs)
+          f' = foldr' (\v t -> Abs v undefined t) base xs
+      return (sub *** a |-> f')
+      
+    Spine (Var f) xs :=: Spine (Var g) ys | f /= g -> do -- Gvar-Gvar - diff
+      h <- getNew
+      let act xi next = do
+            sub' <- flip catchError (const $ return Nothing) $ msum $ flip fmap ys $ \yi -> do
+              sub <- unify'' (tpToTm xi :=: tpToTm yi)
+              return $ Just (yi,sub)
+            (zs,sub) <- next
+            case sub' of
+              Just (yi,sub') -> return ((xi,yi):zs, sub' *** sub)              
+              Nothing  -> return (zs, sub)
+      (zs,sub) <- foldr' act (return (mempty, mempty)) xs
+      
+      let toVar (Atom (Spine (Var x) [])) = do
+            t <- getNew
+            return (x, Atom $ var t)
+          toVar _ = badConstraint
+      
+      xs' <- mapM toVar xs
+      ys' <- mapM toVar ys
+      
+      let baseF = Spine (Var h) (fst <$> zs)
+          f' = foldr' (\(v,vt) t -> Abs v vt t) baseF xs'
+          
+          baseG = Spine (Var h) (snd <$> zs)
+          g' = foldr' (\(v,vt) t -> Abs v vt t) baseG ys'
+      return (sub *** (f |-> f' *** g |-> g'))
+      
+    _ :=: _ -> badConstraint
+
+genUnifyEngine env consts = do
+  s <- unifyAll env mempty consts
+  return $ finishSubst s
+  
+recSubst :: (Eq b, Subst b) => Substitution -> b -> b
+recSubst s f = fst $ head $ dropWhile (not . uncurry (==)) $ iterate (\(_,b) -> (b,subst s b)) (f,subst s f)  
+
+finishSubst s = recSubst s s
+
+finishSubstWith w s = case M.lookup w s of
+  Just (Spine (Var v) []) -> finishSubst $ M.insert v (var w) (M.delete w s)
+  _ -> s
+
+
+----------------------------------------------------------------------
+----------------------- LOGIC ENGINE ---------------------------------
+----------------------------------------------------------------------
+type Reification = VarGen (Tm,Substitution)
+type Deduction = VarGen Substitution
+
+unifier :: [(Name,Tp)] -> Tp -> Reification 
+unifier cons t = do
+  t' <- case t of
+    Atom k -> return k
+    _ -> empty
+  i <- get
+  let isAtom (Atom _) = True
+      isAtom _ = False
+  msum $ flip map (filter (isAtom . snd) cons) $ \(x,Atom con) -> do
+    s <- genUnifyEngine (M.fromList cons) [con :=: t']
+    return $ (var x,s) 
+
+left :: Judgement -> Reification
+left judge@((x,f):context :|- r) = case f of
+  Atom _ -> unifier [(x,f)] r
+  ForallImp nm t1 t2 -> do
+    nm' <- getNew
+    y <- getNew
+    (m,so) <- left $ (y,subst (nm |-> var nm') t2):context :|- r
+    let n = case M.lookup nm' so of
+          Nothing -> var nm'
+          Just a -> a
+        s = seq n $ M.delete nm' so
+    s' <- natural (subst s $ (x,f):context) $ subst s (n,t1)
+    return (subst s' $ subst (y |-> Spine (Var x) []) m, s *** s')
+    
+  Forall nm t1 t2 -> do
+    nm' <- getNew
+    y <- getNew
+    (m,so) <- left $ (y,subst (nm |-> var nm') t2):context :|- r
+    let n = case M.lookup nm' so of
+          Nothing -> var nm'
+          Just a -> a
+        s = seq n $ M.delete nm' so
+    s' <- natural (subst s $ (x,f):context) $ subst s (n,t1)
+    return (subst s' $ subst (y |-> Spine (Var x) [Atom n]) m, s *** s')
+
+
+right :: Judgement -> Reification
+right judge@(context :|- r) = case r of
+  Atom _ -> unifier context r
+  ForallImp nm t1 t2 -> do
+    nm' <- getNew
+    (v,s) <- solve $ (nm', t1):context :|- subst (nm |-> cons nm') t2
+    return $ (tpToTm $ ForallImp nm' t1 (Atom v), s)
+  Forall nm t1 t2 -> do
+    nm' <- getNew
+    (v,s) <- solve $ (nm', t1):context :|- subst (nm |-> cons nm') t2
+    return $ (tpToTm $ Forall nm' t1 (Atom v), s)
+
+solve :: Judgement -> Reification
+solve judge@(context :|- r) = right judge <|> (msum $ useSingle (\f ctx -> left $ f:ctx :|- r) context)
+  where useSingle f lst = sw id lst
+          where sw _ [] = []
+                sw placeOnEnd (a:lst) =  f a (placeOnEnd lst):sw (placeOnEnd . (a:)) lst
+
+natural :: [(Name, Tp)] -> (Tm,Tp) -> Deduction
+natural cont (tm,ty) = do
+  let env = M.fromList cont
+  (_, constraints) <- runWriterT $ checkTerm env tm ty
+  genUnifyEngine (M.fromList cont) constraints
+  
+
+solver :: [(Name,Tp)] -> Tp -> Either String [(Name, Tm)]
+solver axioms t = case runError $ runStateT (solve $ axioms :|- t) 0 of
+  Right ((tm,s),_) -> Right $ ("query" , varsToCons tm):(recSubst s $ map (\a -> (a,var a)) $ S.toList $ freeVariables t)
+    where varsToCons = subst $ M.fromList $ map (\(a,_) -> (a,cons a)) axioms
+  Left s -> Left $ "reification not possible: "++s
+  
+-----------------------------------------------------------------
+----------------------- Type Checker ----------------------------    
+-----------------------------------------------------------------
+type Environment = M.Map Name Tp
+type NatDeduct = WriterT [Constraint Tm] (StateT Integer Choice)
+
+checkVariable :: Environment -> Variable -> Tp -> NatDeduct Tp
+checkVariable env v t = case v of
+  Cons nm -> case env ! nm of
+    Nothing -> error $ nm++" was not found in the environment in "++show v
+    Just t' -> do
+      tell [tpToTm t' :=: tpToTm t]
+      return t'
+  Var nm -> case env ! nm of
+    Nothing -> do 
+      (t'',s) <- lift $ solve $ M.toList env :|- t
+      tell $ map (\(s,t) -> var s :=: t ) $ M.toList s 
+      tell [var nm :=: t'']
+      return t
+      -- I'm not sure this makes sense at all.
+      -- in the mean time, assume there is only one use of each unbound variable
+    Just t' -> do
+      tell [tpToTm t' :=: tpToTm t]
+      return t'
+      
+checkTerm :: Environment -> Tm -> Tp -> NatDeduct (Tm,Tp)
+checkTerm env v t = case v of
+  Spine a l -> do
+    nm   <- (++'α':show a) <$> getNew
+    tv1  <- (++':':show a) <$> getNew
+    tv2l <- forM l $ \b -> do
+      bty <- getNew
+      nm' <- getNew
+      t'  <- checkTerm env (tpToTm b) $ Atom $ var bty
+      return (nm',t')
+      
+    tv1' <- checkVariable env a $ Atom $ var $ tv1
+    
+    tell [ tpToTm tv1' :=: tpToTm (foldr (\(nm,b) tp -> Forall nm (snd b) tp) t tv2l ) ]
+    return $ (Spine a $ map (Atom . fst . snd) tv2l, t)
+        
+  AbsImp nm ty tm -> do  
+    ty' <- checkTipe env ty
+    v1  <- (++':':'<':nm) <$> getNew
+    nm' <- (++'@':nm) <$> getNew
+    v2  <- (++':':'>':nm) <$> getNew
+    tell [ tpToTm (ForallImp v1 ty $ Atom $ var v2) :=: tpToTm t ]
+    ((tm',t'),constraints) <- listen $ checkTerm (M.insert nm' ty env) (subst (nm |-> var nm') tm) $ Atom $ var v2
+    s <- finishSubstWith nm' <$> (lift $ genUnifyEngine env constraints)
+    tell $ map (\(s,t) -> var s :=: t ) $ M.toList s
+    let s' = s *** nm' |-> var nm 
+    return $ (AbsImp nm ty' $ subst s' tm' , ForallImp v1 ty t')
+    
+  Abs nm ty tm -> do
+    ty' <- checkTipe env ty
+    v1  <- (++':':'<':nm) <$> getNew
+    nm' <- (++'@':nm) <$> getNew
+    v2  <- (++':':'>':nm) <$> getNew
+
+    tell [ tpToTm (Forall v1 ty $ Atom $ var v2) :=: tpToTm t ]
+    
+    ((tm',t'),constraints) <- listen $ checkTerm (M.insert nm' ty env) (subst (nm |-> var nm') tm) $ Atom $ var v2
+    s <- finishSubstWith nm' <$> (lift $ genUnifyEngine env constraints)
+    tell $ map (\(s,t) -> var s :=: t ) $ M.toList s
+    let s' = s *** nm' |-> var nm 
+    return $ (Abs nm ty' $ subst s' tm' , Forall v1 ty t')
+    
+checkTipe :: Environment -> Tp -> NatDeduct Tp
+checkTipe env v = case v of
+  Atom tm -> do
+    (a,t) <- checkTerm env tm atom
+    return $ Atom a
+  ForallImp nm ty t -> do
+    Forall nm' ty' t' <- checkTipe env (Forall nm ty t)
+    return $ ForallImp nm' ty' t'
+  Forall nm ty t -> do
+    ty' <- checkTipe env ty
+    nm' <- (++'*':nm) <$> getNew
+    (a,constraints) <- listen $ checkTipe (M.insert nm' ty env) $ subst (nm |-> var nm') t
+    s <- finishSubstWith nm' <$> (lift $ genUnifyEngine env constraints)
+    
+    tell $ map (\(s,t) -> var s :=: t ) $ M.toList s
+    let s' = s *** nm' |-> var nm 
+    return $ Forall nm ty' (subst s' a)
+    
+getCons tm = case tm of
+  Spine (Cons t) _ -> return t
+  Abs _ _ t -> getCons t
+  _ -> throwError $ "can't place a non constructor term here: "++ show tm
+
+getPred tp = case tp of
+  Atom t -> getCons t
+  Forall _ _ t -> getPred t
+  ForallImp _ _ t -> getPred t
+
+-- need to do a topological sort of types and predicates.
+-- such that types get minimal correct bindings
+checkType :: Environment -> Name -> Tp -> Choice Tp
+checkType env base ty = fmap fst $ flip runStateT 0 $ appendErr ("FOR: "++show ty) $ do
+  con <- getPred ty
+  unless (null base || con == base) 
+    $ throwError $ "non local name \""++con++"\" expecting "++base
+  (ty',constraints) <- runWriterT $ checkTipe env ty
+  
+  s <- appendErr ("CONSTRAINTS: "++show constraints) $ genUnifyEngine env constraints
+  
+  return $ subst s ty'
+
+typeCheckPredicate :: Environment -> Predicate -> Choice Predicate
+typeCheckPredicate env (Query nm ty) = appendErr ("in query : "++show ty) $ do
+  ty' <- checkType env "" ty
+  return $ Query nm ty
+typeCheckPredicate env pred@(Predicate pnm pty plst) = appendErr ("in\n"++show pred) $ do
+  pty' <- appendErr ("in name: "++ pnm ++" : "++show pty) $
+    checkType env "atom" pty
+  plst' <- forM plst $ \(nm,ty) -> 
+    appendErr ("in case: " ++nm ++ " = "++show ty) $ (nm,) <$> checkType env pnm ty
+  return $ Predicate pnm pty' plst'
+
+typeCheckAll :: [Predicate] -> Choice [Predicate]
+typeCheckAll preds = forM preds $ typeCheckPredicate assumptions
+  where assumptions = M.fromList $ 
+                      ("atom", atom): -- atom : atom is a given.
+                      ("forall", Atom $ Abs "_" (Atom $ Abs "_" atom $ cons "atom") $ cons "atom"): -- atom : atom is a given.
+                      concatMap (\st -> case st of
+                                    Query _ _ -> []
+                                    _ -> (predName st, predType st):predConstructors st) preds
diff --git a/caledon.cabal b/caledon.cabal
new file mode 100644
--- /dev/null
+++ b/caledon.cabal
@@ -0,0 +1,46 @@
+Name: caledon
+
+Version: 0.0.0.0
+
+Description:         a dependently typed, polymorphic, higher order logic programming language. ie, everything you need to have a conversation with your computer.
+
+Synopsis:            a dependently typed, polymorphic, higher order logic programming language
+
+Homepage:            https://github.com/mmirman/caledon
+
+License:             GPL-3
+
+License-file:        LICENSE
+
+Author:              Matthew Mirman
+
+Maintainer:          Matthew Mirman <mmirman@andrew.cmu.edu>
+
+Category:            Language, Interpreter
+
+Build-type: Simple
+
+Cabal-version: >= 1.6
+
+Source-repository head
+  Type:     git
+  Location: git://github.com/mmirman/caledon.git
+
+executable caledon
+  main-is: Main.hs
+  other-modules: Solver, Choice, Parser
+
+  Build-depends: base >= 4.0 && < 5.0,
+                 mtl >= 2.0 && < 3.0,
+                 parsec >= 3.0 && < 4.0, 
+                 containers >= 0.4 && < 1.0, 
+                 transformers >= 0.3 && < 1.0
+
+  Extensions: DeriveFunctor,
+              FlexibleContexts,
+              FlexibleInstances,
+              MultiParamTypeClasses,
+              PatternGuards,
+              RecordWildCards,
+              TupleSections,
+              TypeSynonymInstances
diff --git a/linear.ncc b/linear.ncc
new file mode 100644
--- /dev/null
+++ b/linear.ncc
@@ -0,0 +1,6 @@
+defn trm : atom
+  as lam = (trm -> trm) -> trm
+   | app = trm -> trm -> trm
+
+defn linear : (trm -> trm) -> atom
+  as linearVar = linear ( λ v : trm . v )
diff --git a/prelude.ncc b/prelude.ncc
new file mode 100644
--- /dev/null
+++ b/prelude.ncc
@@ -0,0 +1,18 @@
+defn num  : atom
+  as zero = num
+   | succ = num → num
+
+defn add   : num → num → num → atom
+  as add_z = {N} add zero N N
+   | add_s = {N}{M}{R} add N M R → add (succ N) M (succ R)
+
+defn sub   : num → num → num → atom
+  as sub_with_add : {N}{M}{R} sub N M R ← add N R M
+
+defn maybe : atom → atom
+  as nothing = {a} maybe a
+   | just = {a} a → maybe a
+
+defn list : atom → atom
+  as nil = {a} nil a
+   | cons = {a} a → list a → list a
diff --git a/test.ncc b/test.ncc
new file mode 100644
--- /dev/null
+++ b/test.ncc
@@ -0,0 +1,11 @@
+defn num  : atom
+  as zero = num
+   | succ = num → num
+
+defn add   : num → num → num → atom
+  as add-z = [N] add zero N N
+   | add-s = [N][M][R] add N M R → add (succ N) M (succ R)
+
+query sum-1 = add (succ zero) (succ (succ zero)) 'v
+query sum-2 = add (succ zero) 'v (succ (succ (succ zero)))
+query sum-3 = add zero (succ zero) 'v