diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2014, Alejandro Serrano
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Alejandro Serrano nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/djinn-ghc.cabal b/djinn-ghc.cabal
new file mode 100644
--- /dev/null
+++ b/djinn-ghc.cabal
@@ -0,0 +1,22 @@
+name:           djinn-ghc
+version:        0.0.1
+synopsis:       Generate Haskell code from a type. Bridge from Djinn to GHC API.
+description:    Djinn uses an theorem prover for intuitionistic propositional logic
+                to generate a Haskell expression when given a type.
+                This is the bridge from djinn-lib to GHC API.
+license:        BSD3
+license-file:   LICENSE
+author:         Alejandro Serrano
+maintainer:     trupill@gmail.com   
+category:       Language
+build-type:     Simple
+cabal-version:  >=1.8
+
+library
+  exposed-modules:  Djinn.GHC
+  build-depends:    base >= 4 && < 5,
+                    mtl < 2.2,
+                    ghc,
+                    containers,
+                    djinn-lib == 0.0.1
+  hs-source-dirs:   src
diff --git a/src/Djinn/GHC.hs b/src/Djinn/GHC.hs
new file mode 100644
--- /dev/null
+++ b/src/Djinn/GHC.hs
@@ -0,0 +1,84 @@
+{-# LANGUAGE PatternGuards #-}
+module Djinn.GHC (djinn) where
+
+import Control.Monad (forM)
+import Data.Set (Set, insert, union, unions, empty, toList)
+
+import qualified Djinn.HTypes as D
+import qualified Djinn.LJT as D
+
+import qualified DataCon as G
+import qualified GHC as G
+import qualified Name as G
+import qualified TyCon as G
+import qualified Type as G
+
+data NoExtraInfo = NoExtraInfo
+type HEnvironment1 a = [(D.HSymbol, ([D.HSymbol], D.HType, a))]
+type HEnvironment = HEnvironment1 NoExtraInfo
+
+getConTs :: G.Type -> Set G.Name
+getConTs t | Just (_, i)  <- G.splitForAllTy_maybe t = getConTs i
+getConTs t | Just (c, ts) <- G.splitTyConApp_maybe t = 
+  let args = unions $ map getConTs ts
+   in if G.isTupleTyCon c then args else insert (G.getName c) args
+getConTs t | Just (t1,t2) <- G.splitAppTy_maybe t    = getConTs t1 `union` getConTs t2
+getConTs _                                           = empty
+
+hType :: G.Type -> D.HType
+hType t | Just (_, i)  <- G.splitForAllTy_maybe t = hType i
+hType t | Just (t1,t2) <- G.splitFunTy_maybe t    = D.HTArrow (hType t1) (hType t2)
+hType t | Just (c, ts) <- G.splitTyConApp_maybe t =
+  let args = map hType ts
+   in if G.isTupleTyCon c  -- Check if we have a tuple
+         then D.HTTuple args
+         else createHTApp (G.getOccString c) (reverse args)
+  where createHTApp n []     = D.HTCon n
+        createHTApp n (x:xs) = D.HTApp (createHTApp n xs) x
+hType t | Just (t1,t2) <- G.splitAppTy_maybe t    = D.HTApp (hType t1) (hType t2)
+hType t | Just var <- G.getTyVar_maybe t          = D.HTVar (toHSymbol var)
+hType _                                           = error "Unimplemented"
+
+environment :: G.GhcMonad m => G.Type -> m HEnvironment
+environment = fmap concat . mapM environment1 . toList . getConTs
+
+environment1 :: G.GhcMonad m => G.Name -> m HEnvironment
+environment1 name = do
+  thing <- G.lookupGlobalName name
+  case thing of
+    Just (G.ATyCon tycon) | G.isAlgTyCon tycon -> do
+      let tyconName = toHSymbol $ G.tyConName tycon
+          varsH = map toHSymbol $ G.tyConTyVars tycon
+          Just datacons = G.tyConDataCons_maybe tycon
+      dtypes <- forM datacons $ \dcon -> do
+        let dconN = toHSymbol $ G.dataConName dcon
+            (_,_,dconT,_) = G.dataConSig dcon
+        dconE <- mapM environment dconT
+        return ((dconN, map hType dconT), dconE)
+      let dtypesT = map fst dtypes
+          dtypesE = concatMap snd dtypes
+      return $ (tyconName, (varsH, D.HTUnion dtypesT, NoExtraInfo)) : concat dtypesE
+    Just (G.ATyCon tycon) | G.isSynTyCon tycon -> do
+      -- Get information for this type synonym
+      let tyconName = toHSymbol $ G.tyConName tycon
+          Just (vars, defn) = G.synTyConDefn_maybe tycon
+          varsH = map toHSymbol vars
+          htype = hType defn
+      -- Recursively obtain it for the environment of the type
+      defnEnv <- environment defn
+      return $ (tyconName, (varsH, htype, NoExtraInfo)) : defnEnv
+    _ -> return []
+
+toHSymbol :: G.NamedThing a => a -> D.HSymbol
+toHSymbol = G.getOccString
+
+-- |Obtain the list of expressions which could fill
+-- something with the given type.
+-- The first flag specifies whether to return one
+-- or more solutions to the problem.
+djinn :: G.GhcMonad m => Bool -> G.Type -> m [String]
+djinn multi ty = do
+  env <- environment ty
+  let form = D.hTypeToFormula env (hType ty)
+      prfs = D.prove multi [] form
+  return $ map show prfs