diff --git a/Djinn/Djinn.hs b/Djinn/Djinn.hs
new file mode 100644
--- /dev/null
+++ b/Djinn/Djinn.hs
@@ -0,0 +1,387 @@
+--
+-- Copyright (c) 2005 Lennart Augustsson
+-- See LICENSE for licensing details.
+--
+module Main(main) where
+import Data.Char(isAlpha, isSpace, isAlphaNum)
+import Data.List(sortBy, nub, intersperse)
+import Data.Ratio
+import Text.ParserCombinators.ReadP
+import Control.Monad(when)
+import Control.Monad.Error()
+import System.IO
+import System.Exit
+import System.Environment
+
+import REPL
+import LJT
+--import MJ
+import HTypes
+import HCheck(htCheckEnv, htCheckType)
+import Help
+
+main :: IO ()
+main = do
+    args <- getArgs
+    let decodeOptions (('-':cs) : as) st = decodeOption cs >>= \f -> decodeOptions as (f False st)
+        decodeOptions (('+':cs) : as) st = decodeOption cs >>= \f -> decodeOptions as (f True  st)
+        decodeOptions as st = return (as, st)
+        decodeOption cs = case [ set | (cmd, _, _, set) <- options, isPrefix cs cmd ] of
+                          [] -> do usage; exitWith (ExitFailure 1)
+                          set : _ -> return set
+    (args', state) <- decodeOptions args startState
+    case args' of
+        [] -> repl (hsGenRepl state)
+        _ -> loop state args'
+              where loop _ [] = return ()
+                    loop s (a:as) = do
+                        putStrLn $ "-- loading file " ++ a
+                        (q, s') <- loadFile s a
+                        if q then
+                            return ()
+                         else
+                            loop s' as
+
+usage :: IO ()
+usage = putStrLn "Usage: djinn [option ...] [file ...]"
+
+hsGenRepl :: State -> REPL State
+hsGenRepl state = REPL {
+    repl_init = inIt state,
+    repl_eval = eval,
+    repl_exit = exit
+    }
+
+data State = State {
+    synonyms :: [(HSymbol, ([HSymbol], HType, HKind))],
+    axioms :: [(HSymbol, HType)],
+    classes :: [ClassDef],
+    multi :: Bool,
+    sorted :: Bool,
+    debug :: Bool,
+    cutOff :: Int
+    }
+    deriving (Show)
+
+startState :: State
+startState = State {
+    synonyms = syns,
+    classes = clss,
+    axioms = [],
+    multi = False,
+    sorted = True,
+    debug = False,
+    cutOff = 100
+    }
+ where syns = either (const $ error "Bad initial environment") id $ htCheckEnv $ reverse [
+        ("()",     ([],        HTUnion [("()",[])],                                      undefined)),
+        ("Either", (["a","b"], HTUnion [("Left", [HTVar "a"]), ("Right", [HTVar "b"])],  undefined)),
+        ("Maybe",  (["a"],     HTUnion [("Nothing", []), ("Just", [HTVar "a"])],         undefined)),
+        ("Bool",   ([],        HTUnion [("False", []), ("True", [])],                    undefined)),
+        ("Void",   ([],        HTUnion [],                                               undefined)),
+        ("Not",    (["x"],     htNot "x",                                                undefined))
+        ]
+       clss = [("Eq", (["a"], [("==", a `HTArrow` (a `HTArrow` HTCon "Bool"))]))]
+       a = HTVar "a"
+
+
+version :: String
+version = "version 2008-01-18"
+
+inIt :: State -> IO (String, State)
+inIt state = do
+    putStrLn $ "Welcome to Djinn " ++ version ++ "."
+    putStrLn $ "Type :h to get help."
+    return ("Djinn> ", state)
+
+eval :: State -> String -> IO (Bool, State)
+eval s line =
+    case filter (null . snd) (readP_to_S pCmd line) of
+    [] -> do
+                putStrLn $ "Cannot parse command"
+                return (False, s)
+    (cmd, "") : _ -> runCmd s cmd
+    _ -> error "eval"
+
+exit :: State -> IO ()
+exit _s = do
+    putStrLn "Bye."
+    return ()
+
+type Context = (HSymbol, [HType])
+type ClassDef = (HSymbol, ([HSymbol], [Method]))
+
+data Cmd = Help Bool | Quit | Add HSymbol HType | Query HSymbol [Context] HType | Del HSymbol | Load HSymbol | Noop | Env |
+           Type (HSymbol, ([HSymbol], HType, HKind)) | Set (State -> State) | Clear | Class ClassDef
+
+pCmd :: ReadP Cmd
+pCmd = do
+    skipSpaces
+    let adds (':':s) p = do schar ':'; pPrefix (takeWhile (/= ' ') s); c <- p; skipSpaces; return c
+        adds _ p = do c <- p; skipSpaces; return c
+    cmd <- foldr1 (+++) [ adds s p | (s, _, p) <- commands ]
+    skipSpaces
+    return cmd
+
+pPrefix :: String -> ReadP String
+pPrefix s = do
+    skipSpaces
+    cs <- look
+    let w = takeWhile isAlpha cs
+    if isPrefix w s then
+        string w
+     else
+        pfail
+
+isPrefix :: String -> String -> Bool
+isPrefix p s = not (null p) && length p <= length s && take (length p) s == p
+
+runCmd :: State -> Cmd -> IO (Bool, State)
+runCmd s Noop = return (False, s)
+runCmd s (Help verbose) = do
+    putStr $ helpText ++ unlines (map getHelp commands) ++ getSettings s
+    when verbose $ putStr verboseHelp
+    return (False, s)
+runCmd s Quit = 
+    return (True, s)
+runCmd s (Load f) = loadFile s f
+runCmd s (Add i t) = 
+    case htCheckType (synonyms s) t of
+    Left msg -> do putStrLn $ "Error: " ++ msg; return (False, s)
+    Right _ -> return (False, s { axioms = (i, t) : axioms s })
+runCmd _ Clear =
+    return (False, startState)
+runCmd s (Del i) = 
+    return (False, s { axioms   = filter ((i /=) . fst) (axioms s)
+                     , synonyms = filter ((i /=) . fst) (synonyms s)
+                     , classes = filter ((i /=) . fst) (classes s) })
+runCmd s Env = do
+--    print s
+    let tname t = if isHTUnion t then "data" else "type"
+        showd (HTUnion []) = ""
+        showd t = " = " ++ show t
+    mapM_ (\ (i, (vs, t, _)) -> putStrLn $ tname t ++ " " ++ unwords (i:vs) ++ showd t) (reverse $ synonyms s)
+    mapM_ (\ (i, t) -> putStrLn $ i ++ " :: " ++ show t) (reverse $ axioms s)
+    mapM_ (putStrLn . showClass) (reverse $ classes s)
+    return (False, s)
+runCmd s (Type syn) = do
+    case htCheckEnv (syn : synonyms s) of
+        Left msg -> do putStrLn $ "Error: " ++ msg; return (False, s)
+        Right syns -> return (False, s { synonyms = syns })
+runCmd s (Set f) =
+    return (False, f s)
+runCmd s (Query i ctx g) =
+   case htCheckType (synonyms s) g >> mapM (ctxLookup (classes s)) ctx of
+   Left msg -> do putStrLn $ "Error: " ++ msg; return (False, s)
+   Right mss -> do
+    let form = hTypeToFormula (synonyms s) g
+        env = [ (Symbol v, hTypeToFormula (synonyms s) t) | (v, t) <- axioms s ] ++ ctxEnv
+        ctxEnv = [ (Symbol v, hTypeToFormula (synonyms s) t) | ms <- mss, (v, t) <- ms ]
+        mpr = prove (multi s || sorted s) env form
+    when (debug s) $ putStrLn ("*** " ++ show form)
+    case mpr of
+        [] -> do
+            putStrLn $ "-- " ++ i ++ " cannot be realized."
+            return (False, s)
+        ps -> do
+            let f p =
+                   let c = termToHClause i p
+                       bvs = getBinderVars c
+                       r = if null bvs then (0, 0) else (length (filter (== "_") bvs) % length bvs, length bvs)
+                   in  (r, c)
+                e:es = nub $ 
+                        if sorted s then
+                            map snd $ sortBy (\ (x,_) (y,_) -> compare x y) $ map f $ take (cutOff s) ps
+                        else
+                            map (termToHClause i) $ take (cutOff s) ps
+                pr = putStrLn . hPrClause
+                sctx = if null ctx then "" else showContexts ctx ++ " => "
+            when (debug s) $ putStrLn ("+++ " ++ show (head ps))
+            putStrLn $ i ++ " :: " ++ sctx ++ show g
+            pr e
+            when (multi s) $ mapM_ (\ x -> putStrLn "-- or" >> pr x) es
+            return (False, s)
+runCmd s (Class c) = do
+    return (False, s { classes = c : classes s })
+
+loadFile :: State -> String -> IO (Bool, State)
+loadFile s name = do
+    file <- readFile name
+    evalCmds s $ lines $ stripComments file
+
+stripComments :: String -> String
+stripComments "" = ""
+stripComments ('-':'-':cs) = skip cs
+  where skip "" = ""
+        skip s@('\n':_) = stripComments s
+        skip (_:s) = skip s
+stripComments (c:cs) = c : stripComments cs
+
+showClass :: ClassDef -> String
+showClass (c, (as, ms)) = "class " ++ showContext (c, map HTVar as) ++ " where " ++ concat (intersperse "; " $ map sm ms)
+  where sm (i, t) = pp i ++ " :: " ++ show t
+        pp i@(ch:_) | not (isAlphaNum ch) = "(" ++ i ++ ")"
+        pp i = i
+
+showContext :: Context -> String
+showContext (c, as) = show $ foldl HTApp (HTCon c) as
+
+showContexts :: [Context] -> String
+showContexts [] = ""
+showContexts cs = "(" ++ concat (intersperse ", " $ map showContext cs) ++ ")"
+
+ctxLookup :: [ClassDef] -> Context -> Either String [Method]
+ctxLookup clss (c, as) =
+    case lookup c clss of
+    Nothing -> Left $ "Class not found: " ++ c
+    Just (ps, ms) -> Right [(m, substHT (zip ps as) t) | (m, t) <- ms ]
+
+evalCmds :: State -> [String] -> IO (Bool, State)
+evalCmds state [] = return (False, state)
+evalCmds state (l:ls) = do
+    qs@(q, state') <- eval state l
+    if q then
+        return qs
+     else
+        evalCmds state' ls
+
+commands :: [(String, String, ReadP Cmd)]
+commands = [
+        (":clear",              "Clear the envirnment",         return Clear),
+        (":delete <sym>",       "Delete from environment.",     pDel),
+        (":environment",        "Show environment",             return Env),
+        (":help",               "Print this message.",          return (Help False)),
+        (":load <file>",        "Load a file",                  pLoad),
+        (":quit",               "Quit program.",                return Quit),
+        (":set <option>",       "Set options",                  pSet),
+        (":verbose-help",       "Print verbose help.",          return (Help True)),
+        ("type <sym> <vars> = <type>", "Add a type synonym",    pType),
+        ("data <sym> <vars> = <datatype>", "Add a data type",   pData),
+        ("class <sym> <vars> where <method>...", "Add a class", pClass),
+        ("<sym> :: <type>",     "Add to environment",           pAdd),
+        ("<sym> ? <type>",      "Query",                        pQuery),
+        ("",                    "",                             return Noop)
+        ]
+
+options :: [(String, String, State->Bool, Bool->State->State)]
+options = [
+          ("multi",             "print multiple solutions",     multi,  \ v s -> s { multi  = v }),
+          ("sorted",            "sort solutions",               sorted, \ v s -> s { sorted = v }),
+          ("debug",             "debug mode",                   debug,  \ v s -> s { debug  = v })
+          ]
+
+getHelp :: (String, String, a) -> String
+getHelp (cmd, help, _) = cmd ++ replicate (35 - length cmd) ' ' ++ help
+
+pDel :: ReadP Cmd
+pDel = do
+    s <- pHSymbol True +++ pHSymbol False
+    return $ Del s
+
+pLoad :: ReadP Cmd
+pLoad = do
+    skipSpaces
+    s <- munch1 (not . isSpace)
+    return $ Load s
+
+pAdd :: ReadP Cmd
+pAdd = do
+    i <- pHSymbol False
+    sstring "::"
+    t <- pHType
+    optional $ schar ';'
+    return $ Add i t
+
+pQuery :: ReadP Cmd
+pQuery = do
+    i <- pHSymbol False
+    schar '?'
+    c <- option [] pContext
+    t <- pHType
+    optional $ schar ';'
+    return $ Query i c t
+
+pContext :: ReadP [Context]
+pContext = do
+    let pCtx = do c <- pHSymbol True; ts <- many pHTAtom; return (c, ts)
+    schar '('
+    ctx <- sepBy1 pCtx (schar ',')
+    schar ')'
+    sstring "=>"
+    return ctx
+
+pType :: ReadP Cmd
+pType = do
+    sstring "type"
+    syn <- pHSymbol True
+    args <- many (pHSymbol False)
+    schar '='
+    t <- pHType
+    return $ Type (syn, (args, t, undefined))
+
+pData :: ReadP Cmd
+pData = do
+    sstring "data"
+    syn <- pHSymbol True
+    args <- many (pHSymbol False)
+    (do schar '='; t <- pHDataType; return $ Type (syn, (args, t, undefined))) +++ (return $ Type (syn, (args, HTUnion [], undefined)))
+
+pClass :: ReadP Cmd
+pClass = do
+    sstring "class"
+    cls <- pHSymbol True
+    args <- many (pHSymbol False)
+    sstring "where"
+    mets <- sepBy pMethod (schar ';')
+    return $ Class (cls, (args, mets))
+
+type Method = (HSymbol, HType)
+
+pMethod :: ReadP Method
+pMethod = do
+    let pOpSym = satisfy (`elem` "~!#$%^&*-+=<>.:")
+    i <- pHSymbol False +++ do schar '('; op <- many1 pOpSym; schar ')'; return op
+    sstring "::"
+    t <- pHType
+    return (i, t)
+
+pSet :: ReadP Cmd
+pSet = do
+    val <- (do schar '+'; return True) +++ (do schar '-'; return False) 
+    f <- foldr (+++) pfail [ do pPrefix s; return (set val) | (s, _, _, set) <- options ]
+    return $ Set $ f
+
+schar :: Char -> ReadP ()
+schar c = do
+    skipSpaces
+    char c
+    return ()
+
+sstring :: String -> ReadP ()
+sstring s = do
+    skipSpaces
+    string s
+    return ()
+
+helpText :: String
+helpText = "\
+\Djinn is a program that generates Haskell code from a type.\n\
+\Given a type the program will deduce an expression of this type,\n\
+\if one exists.  If the Djinn says the type is not realizable it is\n\
+\because there is no (total) expression of the given type.\n\
+\Djinn only knows about tuples, ->, and some data types in the\n\
+\initial environment (do :e for a list).\n\
+\\n\
+\Caveat emptor: The expression will have the right type, but it\n\
+\may not be what you were looking for.\n\
+\\n\
+\Send any comments and feedback to lennart@augustsson.net\n\
+\\n\
+\Commands (may be abbreviated):\n\
+\"
+
+getSettings :: State -> String
+getSettings s = unlines $ [
+    "",
+    "Current settings" ] ++ [ "    " ++ (if gett s then "+" else "-") ++ name ++ replicate (10 - length name) ' ' ++ descr |
+                              (name, descr, gett, _set) <- options ]
diff --git a/Djinn/HCheck.hs b/Djinn/HCheck.hs
new file mode 100644
--- /dev/null
+++ b/Djinn/HCheck.hs
@@ -0,0 +1,152 @@
+--
+-- Copyright (c) 2005 Lennart Augustsson
+-- See LICENSE for licensing details.
+--
+module HCheck(htCheckEnv, htCheckType) where
+import Data.List(union)
+--import Control.Monad.Trans
+import Control.Monad.Error()
+import Control.Monad.State
+import Data.IntMap(IntMap, insert, (!), empty)
+
+import Util.Digraph(stronglyConnComp, SCC(..))
+
+import HTypes
+
+--import Debug.Trace
+
+type KState = (Int, IntMap (Maybe HKind))
+initState :: KState
+initState = (0, empty)
+
+type M a = StateT KState (Either String) a
+
+type KEnv = [(HSymbol, HKind)]
+
+newKVar :: M HKind
+newKVar = do
+    (i, m) <- get
+    put (i+1, insert i Nothing m)
+    return $ KVar i
+
+getVar :: Int -> M (Maybe HKind)
+getVar i = do
+    (_, m) <- get
+    case m!i of
+        Just (KVar i') -> getVar i'
+        mk -> return mk
+
+addMap :: Int -> HKind -> M ()
+addMap i k = do
+    (n, m) <- get
+    put (n, insert i (Just k) m)
+
+clearState :: M ()
+clearState = put initState
+
+htCheckType :: [(HSymbol, ([HSymbol], HType, HKind))] -> HType -> Either String ()
+htCheckType its t = flip evalStateT initState $ do
+    let vs = getHTVars t
+    ks <- mapM (const newKVar) vs
+    let env = zip vs ks ++ [(i, k) | (i, (_, _, k)) <- its ]
+    iHKindStar env t        
+
+htCheckEnv :: [(HSymbol, ([HSymbol], HType, a))] -> Either String [(HSymbol, ([HSymbol], HType, HKind))]
+htCheckEnv its =
+    let graph = [ (n, i, getHTCons t) | n@(i, (_, t, _)) <- its ]
+        order = stronglyConnComp graph
+    in  case [ c | CyclicSCC c <- order ] of
+        c : _ -> Left $ "Recursive types are not allowed: " ++ unwords [ i | (i, _) <- c ]
+        [] -> flip evalStateT initState $ addKinds
+            where addKinds = do
+                        env <- inferHKinds [] $ map (\ (AcyclicSCC n) -> n) order
+                        let getK i = maybe (error $ "htCheck " ++ i) id $ lookup i env
+                        return [ (i, (vs, t, getK i)) | (i, (vs, t, _)) <- its ]
+
+inferHKinds :: KEnv -> [(HSymbol, ([HSymbol], HType, a))] -> M KEnv
+inferHKinds env [] = return env
+inferHKinds env ((i, (vs, t, _)) : its) = do
+    k <- inferHKind env vs t
+    inferHKinds ((i, k) : env) its
+
+inferHKind :: KEnv -> [HSymbol] -> HType -> M HKind
+inferHKind env vs t = do
+    clearState
+    ks <- mapM (const newKVar) vs
+    let env' = zip vs ks ++ env
+    k <- iHKind env' t
+    ground $ foldr KArrow k ks
+
+iHKind :: KEnv -> HType -> M HKind
+iHKind env (HTApp f a) = do
+    kf <- iHKind env f
+    ka <- iHKind env a
+    r <- newKVar
+    unifyK (KArrow ka r) kf
+    return r
+iHKind env (HTVar v) = do
+    getVarHKind env v
+iHKind env (HTCon c) = do
+    getConHKind env c
+iHKind env (HTTuple ts) = do
+    mapM_ (iHKindStar env) ts
+    return KStar
+iHKind env (HTArrow f a) = do
+    iHKindStar env f
+    iHKindStar env a
+    return KStar
+iHKind env (HTUnion cs) = do
+    mapM_ (\ (_, ts) -> mapM_ (iHKindStar env) ts) cs
+    return KStar
+
+iHKindStar :: KEnv -> HType -> M ()
+iHKindStar env t = do
+    k <- iHKind env t
+    unifyK k KStar
+
+unifyK :: HKind -> HKind -> M ()
+unifyK k1 k2 = do
+    let follow k@(KVar i) = getVar i >>= return . maybe k id 
+        follow k = return k
+        unify KStar KStar = return ()
+        unify (KArrow k11 k12) (KArrow k21 k22) = do unifyK k11 k21; unifyK k12 k22
+        unify (KVar i1) (KVar i2) | i1 == i2 = return ()
+        unify (KVar i) k = do occurs i k; addMap i k
+        unify k (KVar i) = do occurs i k; addMap i k
+        unify _ _ = lift $ Left "kind error"
+        occurs _ KStar = return ()
+        occurs i (KArrow f a) = do follow f >>= occurs i; follow a >>= occurs i
+        occurs i (KVar i') = if i == i' then lift $ Left "cyclic kind" else return ()
+    k1' <- follow k1
+    k2' <- follow k2
+    unify k1' k2'
+    
+
+getVarHKind :: KEnv -> HSymbol -> M HKind
+getVarHKind env v =
+    case lookup v env of
+    Just k -> return k
+    Nothing -> lift $ Left $ "type variable not bound " ++ v
+
+getConHKind :: KEnv -> HSymbol -> M HKind
+getConHKind env v =
+    case lookup v env of
+    Just k -> return k
+    Nothing -> newKVar          -- allow uninterpreted type constructors
+
+ground :: HKind -> M HKind
+ground KStar = return KStar
+ground (KArrow k1 k2) = liftM2 KArrow (ground k1) (ground k2)
+ground (KVar i) = do
+    mk <- getVar i
+    case mk of
+        Just k -> return k
+        Nothing -> return KStar
+
+getHTCons :: HType -> [HSymbol]
+getHTCons (HTApp f a) = getHTCons f `union` getHTCons a
+getHTCons (HTVar _) = []
+getHTCons (HTCon s) = [s]
+getHTCons (HTTuple ts) = foldr union [] (map getHTCons ts)
+getHTCons (HTArrow f a) = getHTCons f `union` getHTCons a
+getHTCons (HTUnion alts) = foldr union [] [ getHTCons t | (_, ts) <- alts, t <- ts ]
diff --git a/Djinn/HTypes.hs b/Djinn/HTypes.hs
new file mode 100644
--- /dev/null
+++ b/Djinn/HTypes.hs
@@ -0,0 +1,452 @@
+--
+-- Copyright (c) 2005 Lennart Augustsson
+-- See LICENSE for licensing details.
+--
+module HTypes(HKind(..), HType(..), HSymbol, hTypeToFormula, pHSymbol, pHType, pHDataType, pHTAtom,
+        htNot, isHTUnion, getHTVars, substHT,
+        HClause, HPat, HExpr(HEVar), hPrClause, termToHExpr, termToHClause, getBinderVars) where
+import Text.PrettyPrint.HughesPJ(Doc, renderStyle, style, text, (<>), parens, ($$), vcat, punctuate,
+         sep, fsep, nest, comma, (<+>))
+import Data.Char(isAlphaNum, isAlpha, isUpper)
+import Data.List(union, (\\))
+import Control.Monad(zipWithM)
+import Text.ParserCombinators.ReadP
+import LJTFormula
+
+--import Debug.Trace
+
+type HSymbol = String
+
+data HKind
+    = KStar
+    | KArrow HKind HKind
+    | KVar Int
+    deriving (Eq, Show)
+
+data HType
+        = HTApp HType HType
+        | HTVar HSymbol
+        | HTCon HSymbol
+        | HTTuple [HType]
+        | HTArrow HType HType
+        | HTUnion [(HSymbol, [HType])]          -- Only for data types; only at top level
+        deriving (Eq)
+
+isHTUnion :: HType -> Bool
+isHTUnion (HTUnion _) = True
+isHTUnion _ = False
+
+htNot :: HSymbol -> HType
+htNot x = HTArrow (HTVar x) (HTCon "Void")
+
+instance Show HType where
+    showsPrec _ (HTApp (HTCon "[]") t) = showString "[" . showsPrec 0 t . showString "]"
+    showsPrec p (HTApp f a) = showParen (p > 2) $ showsPrec 2 f . showString " " . showsPrec 3 a
+    showsPrec _ (HTVar s) = showString s
+    showsPrec _ (HTCon s) = showString s
+    showsPrec _ (HTTuple ss) = showParen True $ f ss
+        where f [] = error "showsPrec HType"
+              f [t] = showsPrec 0 t
+              f (t:ts) = showsPrec 0 t . showString ", " . f ts
+    showsPrec p (HTArrow s t) = showParen (p > 0) $ showsPrec 1 s . showString " -> " . showsPrec 0 t
+    showsPrec _ (HTUnion cs) = f cs
+        where f [] = id
+              f [cts] = scts cts
+              f (cts : ctss) = scts cts . showString " | " . f ctss
+              scts (c, ts) = foldl (\ s t -> s . showString " " . showsPrec 10 t) (showString c) ts
+
+instance Read HType where
+    readsPrec _ = readP_to_S pHType'
+
+pHType' :: ReadP HType
+pHType' = do
+    t <- pHType
+    skipSpaces
+    return t
+
+pHType :: ReadP HType
+pHType = do
+    ts <- sepBy1 pHTypeApp (do schar '-'; char '>')
+    return $ foldr1 HTArrow ts
+
+pHDataType :: ReadP HType
+pHDataType = do
+    let con = do
+            c <- pHSymbol True
+            ts <- many pHTAtom
+            return (c, ts)
+    cts <- sepBy con (schar '|')
+    return $ HTUnion cts
+
+pHTAtom :: ReadP HType
+pHTAtom = pHTVar +++ pHTCon +++ pHTList +++ pParen pHTTuple +++ pParen pHType +++ pUnit
+
+pUnit :: ReadP HType
+pUnit = do
+    schar '('
+    char ')'
+    return $ HTCon "()"
+
+pHTCon :: ReadP HType
+pHTCon = pHSymbol True >>= return . HTCon
+
+pHTVar :: ReadP HType
+pHTVar = pHSymbol False >>= return . HTVar
+
+pHSymbol :: Bool -> ReadP HSymbol
+pHSymbol con = do
+    skipSpaces
+    c <- satisfy $ \ c -> isAlpha c && isUpper c == con
+    let isSym d = isAlphaNum d || d == '\'' || d == '.'
+    cs <- munch isSym
+    return $ c:cs
+
+pHTTuple :: ReadP HType
+pHTTuple = do
+    t <- pHType
+    ts <- many1 (do schar ','; pHType)
+    return $ HTTuple $ t:ts
+
+pHTypeApp :: ReadP HType
+pHTypeApp = do
+    ts <- many1 pHTAtom
+    return $ foldl1 HTApp ts
+
+pHTList :: ReadP HType
+pHTList = do
+    schar '['
+    t <- pHType
+    schar ']'
+    return $ HTApp (HTCon "[]") t
+
+pParen :: ReadP a -> ReadP a
+pParen p = do
+    schar '('
+    e <- p
+    schar ')'
+    return e
+
+schar :: Char -> ReadP ()
+schar c = do
+    skipSpaces
+    char c
+    return ()
+
+getHTVars :: HType -> [HSymbol]
+getHTVars (HTApp f a) = getHTVars f `union` getHTVars a
+getHTVars (HTVar v) = [v]
+getHTVars (HTCon _) = []
+getHTVars (HTTuple ts) = foldr union [] (map getHTVars ts)
+getHTVars (HTArrow f a) = getHTVars f `union` getHTVars a
+getHTVars _ = error "getHTVars"
+
+-------------------------------
+
+hTypeToFormula :: [(HSymbol, ([HSymbol], HType, a))] -> HType -> Formula
+hTypeToFormula ss (HTTuple ts) = Conj (map (hTypeToFormula ss) ts)
+hTypeToFormula ss (HTArrow t1 t2) = hTypeToFormula ss t1 :-> hTypeToFormula ss t2
+hTypeToFormula ss (HTUnion ctss) = Disj [ (ConsDesc c (length ts), hTypeToFormula ss (HTTuple ts)) | (c, ts) <- ctss ]
+hTypeToFormula ss t = 
+    case expandSyn ss t [] of
+    Nothing -> PVar $ Symbol $ show t
+    Just t' -> hTypeToFormula ss t'
+
+expandSyn :: [(HSymbol, ([HSymbol], HType, a))] -> HType -> [HType] -> Maybe HType
+expandSyn ss (HTApp f a) as = expandSyn ss f (a:as)
+expandSyn ss (HTCon c) as =
+    case lookup c ss of
+    Just (vs, t, _) | length vs == length as -> Just $ substHT (zip vs as) t
+    _ -> Nothing
+expandSyn _ _ _ = Nothing
+
+substHT :: [(HSymbol, HType)] -> HType -> HType
+substHT r (HTApp f a) = HTApp (substHT r f) (substHT r a)
+substHT r t@(HTVar v) =
+    case lookup v r of
+    Nothing -> t
+    Just t' -> t'
+substHT _ t@(HTCon _) = t
+substHT r (HTTuple ts) = HTTuple (map (substHT r) ts)
+substHT r (HTArrow f a) = HTArrow (substHT r f) (substHT r a)
+substHT r (HTUnion (ctss)) = HTUnion [ (c, map (substHT r) ts) | (c, ts) <- ctss ]
+
+
+-------------------------------
+
+
+data HClause = HClause HSymbol [HPat] HExpr
+    deriving (Show, Eq)
+
+data HPat = HPVar HSymbol | HPCon HSymbol | HPTuple [HPat] | HPAt HSymbol HPat | HPApply HPat HPat
+    deriving (Show, Eq)
+
+data HExpr = HELam [HPat] HExpr | HEApply HExpr HExpr | HECon HSymbol | HEVar HSymbol | HETuple [HExpr] |
+        HECase HExpr [(HPat, HExpr)]
+    deriving (Show, Eq)
+
+hPrClause :: HClause -> String
+hPrClause c = renderStyle style $ ppClause 0 c
+
+ppClause :: Int -> HClause -> Doc
+ppClause _p (HClause f ps e) = text f <+> sep [sep (map (ppPat 10) ps) <+> text "=",
+                                               nest 2 $ ppExpr 0 e]
+
+ppPat :: Int -> HPat -> Doc
+ppPat _ (HPVar s) = text s
+ppPat _ (HPCon s) = text s
+ppPat _ (HPTuple ps) = parens $ fsep $ punctuate comma (map (ppPat 0) ps)
+ppPat _ (HPAt s p) = text s <> text "@" <> ppPat 10 p
+ppPat p (HPApply a b) = pparens (p > 1) $ ppPat 1 a <+> ppPat 2 b
+
+ppExpr :: Int -> HExpr -> Doc
+ppExpr p (HELam ps e) = pparens (p > 0) $ sep [ text "\\" <+> sep (map (ppPat 10) ps) <+> text "->",
+                                                ppExpr 0 e]
+ppExpr p (HEApply (HEApply (HEVar f@(c:_)) a1) a2) | not (isAlphaNum c) =
+     pparens (p > 4) $ ppExpr 5 a1 <+> text f <+> ppExpr 5 a2
+ppExpr p (HEApply f a) = pparens (p > 11) $ ppExpr 11 f <+> ppExpr 12 a
+ppExpr _ (HECon s) = text s
+ppExpr _ (HEVar s@(c:_)) | not (isAlphaNum c) = pparens True $ text s
+ppExpr _ (HEVar s) = text s
+ppExpr _ (HETuple es) = parens $ fsep $ punctuate comma (map (ppExpr 0) es)
+ppExpr p (HECase s alts) = pparens (p > 0) $ (text "case" <+> ppExpr 0 s <+> text "of") $$
+                            vcat (map ppAlt alts)
+  where ppAlt (pp, e) = ppPat 0 pp <+> text "->" <+> ppExpr 0 e
+
+
+pparens :: Bool -> Doc -> Doc
+pparens True d = parens d
+pparens False d = d
+
+-------------------------------
+
+
+unSymbol :: Symbol -> HSymbol
+unSymbol (Symbol s) = s
+
+termToHExpr :: Term -> HExpr
+termToHExpr term = niceNames $ etaReduce $ remUnusedVars $ fst $ conv [] term
+  where conv _vs (Var s) = (HEVar $ unSymbol s, [])
+        conv vs (Lam s te) = 
+                let hs = unSymbol s
+                    (te', ss) = conv (hs : vs) te
+                in  (hELam [convV hs ss] te', ss)
+        conv vs (Apply (Cinj (ConsDesc s n) _) a) = (f $ foldl HEApply (HECon s) as, ss)
+                where (f, as) = unTuple n ha
+                      (ha, ss) = conv vs a
+        conv vs (Apply te1 te2) = convAp vs te1 [te2]
+        conv _vs (Ctuple 0) = (HECon "()", [])
+        conv _vs e = error $ "termToHExpr " ++ show e
+
+        unTuple 0 _ = (id, [])
+        unTuple 1 a = (id, [a])
+        unTuple n (HETuple as) | length as == n = (id, as)
+        unTuple n e = error $ "unTuple: unimplemented " ++ show (n, e)
+
+        unTupleP 0 _ = []
+--      unTupleP 1 p = [p]
+        unTupleP n (HPTuple ps) | length ps == n = ps
+        unTupleP n p = error $ "unTupleP: unimplemented " ++ show (n, p)
+
+        convAp vs (Apply te1 te2) as = convAp vs te1 (te2:as)
+        convAp vs (Ctuple n) as | length as == n =
+                let (es, sss) = unzip $ map (conv vs) as
+                in  (hETuple es, concat sss)
+        convAp vs (Ccases cds) (se : es) =
+                let (alts, ass) = unzip $ zipWith cAlt es cds
+                    cAlt (Lam v e) (ConsDesc c n) =
+                        let hv = unSymbol v
+                            (he, ss) = conv (hv : vs) e
+                            ps = case lookup hv ss of
+                                 Nothing -> replicate n (HPVar "_")
+                                 Just p -> unTupleP n p
+                        in  ((foldl HPApply (HPCon c) ps, he), ss)
+                    cAlt e _ = error $ "cAlt " ++ show e
+                    (e', ess) = conv vs se
+                in  (hECase e' alts, ess ++ concat ass)
+        convAp vs (Csplit n) (b : a : as) =
+                let (hb, sb) = conv vs b
+                    (a', sa) = conv vs a
+                    (as', sss) = unzip $ map (conv vs) as
+                    (ps, b') = unLam n hb
+                    unLam 0 e = ([], e)
+                    unLam k (HELam ps0 e) | length ps0 >= n = let (ps1, ps2) = splitAt k ps0 in (ps1, hELam ps2 e)
+                    unLam k e = error $ "unLam: unimplemented" ++ show (k, e)
+                in  case a' of
+                        HEVar v | v `elem` vs && null as -> (b', [(v, HPTuple ps)] ++ sb ++ sa)
+                        _ -> (foldr HEApply (hECase a' [(HPTuple ps, b')]) as',
+                              sb ++ sa ++ concat sss)
+                    
+        convAp vs f as = 
+                let (es, sss) = unzip $ map (conv vs) (f:as)
+                in  (foldl1 HEApply es, concat sss)
+
+        convV hs ss =
+                case lookup hs ss of
+                Nothing -> HPVar hs
+                Just p -> HPAt hs p
+
+        hETuple [e] = e
+        hETuple es = HETuple es
+
+niceNames :: HExpr -> HExpr
+niceNames e =
+    let bvars = filter (/= "_") $ getBinderVarsHE e
+        nvars = [[c] | c <- ['a'..'z']] ++ [ "x" ++ show i | i <- [1::Integer ..]]
+        freevars = getAllVars e \\ bvars
+        vars = nvars \\ freevars
+        sub = zip bvars vars
+    in  hESubst sub e
+
+hELam :: [HPat] -> HExpr -> HExpr
+hELam [] e = e
+hELam ps (HELam ps' e) = HELam (ps ++ ps') e
+hELam ps e = HELam ps e
+
+hECase :: HExpr -> [(HPat, HExpr)] -> HExpr
+hECase e [] = HEApply (HEVar "void") e
+hECase _ [(HPCon "()", e)] = e
+hECase e pes | all (uncurry eqPatExpr) pes = e
+hECase e [(p, HELam ps b)] = HELam ps $ hECase e [(p, b)]
+hECase se alts@((_, HELam ops _):_) | m > 0 = HELam (take m ops) $ hECase se alts'
+  where m = minimum (map (numBind . snd) alts)
+        numBind (HELam ps _) = length (takeWhile isPVar ps)
+        numBind _ = 0
+        isPVar (HPVar _) = True
+        isPVar _ = False
+        alts' = [ let (ps1, ps2) = splitAt m ps in (cps, hELam ps2 $ hESubst (zipWith (\ (HPVar v) n -> (v, n)) ps1 ns) e)
+                  | (cps, HELam ps e) <- alts ]
+        ns = [ n | HPVar n <- take m ops ]
+-- if all arms are equal and there are at least two alternatives there can be no bound vars
+-- from the patterns
+hECase _ ((_,e):alts@(_:_)) | all (alphaEq e . snd) alts = e
+hECase e alts = HECase e alts
+
+eqPatExpr :: HPat -> HExpr -> Bool
+eqPatExpr (HPVar s) (HEVar s') = s == s'
+eqPatExpr (HPCon s) (HECon s') = s == s'
+eqPatExpr (HPTuple ps) (HETuple es) = and (zipWith eqPatExpr ps es)
+eqPatExpr (HPApply pf pa) (HEApply ef ea) = eqPatExpr pf ef && eqPatExpr pa ea
+eqPatExpr _ _ = False
+
+alphaEq :: HExpr -> HExpr -> Bool
+alphaEq e1 e2 | e1 == e2 = True
+alphaEq (HELam ps1 e1) (HELam ps2 e2) =
+    Nothing /= do
+        s <- matchPat (HPTuple ps1) (HPTuple ps2)
+        if alphaEq (hESubst s e1) e2 then
+            return ()
+         else
+            Nothing
+alphaEq (HEApply f1 a1) (HEApply f2 a2) = alphaEq f1 f2 && alphaEq a1 a2
+alphaEq (HECon s1) (HECon s2) = s1 == s2
+alphaEq (HEVar s1) (HEVar s2) = s1 == s2
+alphaEq (HETuple es1) (HETuple es2) | length es1 == length es2 = and (zipWith alphaEq es1 es2)
+alphaEq (HECase e1 alts1) (HECase e2 alts2) =
+    alphaEq e1 e2 && and (zipWith alphaEq [ HELam [p] e | (p, e) <- alts1 ] [ HELam [p] e | (p, e) <- alts2 ])
+alphaEq _ _ = False
+
+matchPat :: HPat -> HPat -> Maybe [(HSymbol, HSymbol)]
+matchPat (HPVar s1) (HPVar s2) = return [(s1, s2)]
+matchPat (HPCon s1) (HPCon s2) | s1 == s2 = return []
+matchPat (HPTuple ps1) (HPTuple ps2) | length ps1 == length ps2 = do
+    ss <- zipWithM matchPat ps1 ps2
+    return $ concat ss
+matchPat (HPAt s1 p1) (HPAt s2 p2) = do
+    s <- matchPat p1 p2
+    return $ (s1, s2) : s
+matchPat (HPApply f1 a1) (HPApply f2 a2) = do
+    s1 <- matchPat f1 f2
+    s2 <- matchPat a1 a2
+    return $ s1 ++ s2
+matchPat _ _ = Nothing
+
+hESubst :: [(HSymbol, HSymbol)] -> HExpr -> HExpr
+hESubst s (HELam ps e) = HELam (map (hPSubst s) ps) (hESubst s e)
+hESubst s (HEApply f a) = HEApply (hESubst s f) (hESubst s a)
+hESubst _ e@(HECon _) = e
+hESubst s (HEVar v) = HEVar $ maybe v id $ lookup v s
+hESubst s (HETuple es) = HETuple (map (hESubst s) es)
+hESubst s (HECase e alts) = HECase (hESubst s e) [(hPSubst s p, hESubst s b) | (p, b) <- alts]
+
+hPSubst :: [(HSymbol, HSymbol)] -> HPat -> HPat
+hPSubst s (HPVar v) = HPVar $ maybe v id $ lookup v s
+hPSubst _ p@(HPCon _) = p
+hPSubst s (HPTuple ps) = HPTuple (map (hPSubst s) ps)
+hPSubst s (HPAt v p) = HPAt (maybe v id $ lookup v s) (hPSubst s p)
+hPSubst s (HPApply f a) = HPApply (hPSubst s f) (hPSubst s a)
+
+
+termToHClause :: HSymbol -> Term -> HClause
+termToHClause i term =
+    case termToHExpr term of
+    HELam ps e -> HClause i ps e
+    e -> HClause i [] e
+
+remUnusedVars :: HExpr -> HExpr
+remUnusedVars expr = fst $ remE expr
+  where remE (HELam ps e) =
+            let (e', vs) = remE e
+            in  (HELam (map (remP vs) ps) e', vs)
+        remE (HEApply f a) =
+            let (f', fs) = remE f
+                (a', as) = remE a
+            in  (HEApply f' a', fs ++ as)
+        remE (HETuple es) =
+            let (es', sss) = unzip (map remE es)
+            in  (HETuple es', concat sss)
+        remE (HECase e alts) =
+            let (e', es) = remE e
+                (alts', sss) = unzip [ let (ee', ss) = remE ee in ((remP ss p, ee'), ss) | (p, ee) <- alts ]
+            in  case alts' of
+                [(HPVar "_", b)] -> (b, concat sss)
+                _ -> (hECase e' alts', es ++ concat sss)
+        remE e@(HECon _) = (e, [])
+        remE e@(HEVar v) = (e, [v])
+        remP vs p@(HPVar v) = if v `elem` vs then p else HPVar "_"
+        remP _vs p@(HPCon _) = p
+        remP vs (HPTuple ps) = hPTuple (map (remP vs) ps)
+        remP vs (HPAt v p) = if v `elem` vs then HPAt v (remP vs p) else remP vs p
+        remP vs (HPApply f a) = HPApply (remP vs f) (remP vs a)
+        hPTuple ps | all (== HPVar "_") ps = HPVar "_"
+        hPTuple ps = HPTuple ps
+
+getBinderVars :: HClause -> [HSymbol]
+getBinderVars (HClause _ pats expr) = concatMap getBinderVarsHP pats ++ getBinderVarsHE expr
+
+getBinderVarsHE :: HExpr -> [HSymbol]
+getBinderVarsHE expr = gbExp expr
+  where gbExp (HELam ps e) = concatMap getBinderVarsHP ps ++ gbExp e
+        gbExp (HEApply f a) = gbExp f ++ gbExp a
+        gbExp (HETuple es) = concatMap gbExp es
+        gbExp (HECase se alts) = gbExp se ++ concatMap (\ (p, e) -> getBinderVarsHP p ++ gbExp e) alts
+        gbExp _ = []
+
+getBinderVarsHP :: HPat -> [HSymbol]
+getBinderVarsHP pat = gbPat pat
+  where gbPat (HPVar s) = [s]
+        gbPat (HPCon _) = []
+        gbPat (HPTuple ps) = concatMap gbPat ps
+        gbPat (HPAt s p) = s : gbPat p
+        gbPat (HPApply f a) = gbPat f ++ gbPat a
+
+getAllVars :: HExpr -> [HSymbol]
+getAllVars expr = gaExp expr
+  where gaExp (HELam _ps e) = gaExp e
+        gaExp (HEApply f a) = gaExp f `union` gaExp a
+        gaExp (HETuple es) = foldr union [] (map gaExp es)
+        gaExp (HECase se alts) = foldr union (gaExp se) (map (\ (_p, e) -> gaExp e) alts)
+        gaExp (HEVar s) = [s]
+        gaExp _ = []
+
+etaReduce :: HExpr -> HExpr
+etaReduce expr = fst $ eta expr
+  where eta (HELam [HPVar v] (HEApply f (HEVar v'))) | v == v' && v `notElem` vs = (f', vs)
+            where (f', vs) = eta f
+        eta (HELam ps e) = (HELam ps e', vs) where (e', vs) = eta e
+        eta (HEApply f a) = (HEApply f' a', fvs++avs) where (f', fvs) = eta f; (a', avs) = eta a
+        eta e@(HECon _) = (e, [])
+        eta e@(HEVar s) = (e, [s])
+        eta (HETuple es) = (HETuple es', concat vss) where (es', vss) = unzip $ map eta es
+        eta (HECase e alts) = (HECase e' alts', vs ++ concat vss) where (e', vs) = eta e
+                                                                        (alts', vss) = unzip $ [ let (a', ss) = eta a in ((p, a'), ss)
+                                                                                                 | (p, a) <- alts ]
diff --git a/Djinn/Help.hs b/Djinn/Help.hs
new file mode 100644
--- /dev/null
+++ b/Djinn/Help.hs
@@ -0,0 +1,177 @@
+module Help where
+verboseHelp :: String
+verboseHelp = "\
+\\n\
+\\n\
+\Djinn commands explained\n\
+\========================\n\
+\\n\
+\<sym> ? <type>\n\
+\  Try to find a function of the specified type.  Djinn knows about the\n\
+\function type, tuples, Either, Maybe, (), and can be given new type\n\
+\definitions.  (Djinn also knows about the empty type, Void, but this\n\
+\is less useful.)  Further functions, type synonyms, and data types can\n\
+\be added by using the commands below.  If a function can be found it\n\
+\is printed in a style suitable for inclusion in a Haskell program.  If\n\
+\no function can be found this will be reported as well.  Examples:\n\
+\  Djinn> f ? a->a\n\
+\  f :: a -> a\n\
+\  f x1 = x1\n\
+\  Djinn> sel ? ((a,b),(c,d)) -> (b,c)\n\
+\  sel :: ((a, b), (c, d)) -> (b, c)\n\
+\  sel ((_, v5), (v6, _)) = (v5, v6)\n\
+\  Djinn> cast ? a->b\n\
+\  -- cast cannot be realized.\n\
+\  Djinn will always find a (total) function if one exists.  (The worst\n\
+\case complexity is bad, but unlikely for typical examples.)  If no\n\
+\function exists Djinn will always terminate and say so.\n\
+\  When multiple implementations of the type exists Djinn will only\n\
+\give one of them.  Example:\n\
+\  Djinn> f ? a->a->a\n\
+\  f :: a -> a -> a\n\
+\  f _ x2 = x2\n\
+\\n\
+\Warning: The given type expression is not checked in any way (i.e., no\n\
+\kind checking).\n\
+\\n\
+\\n\
+\<sym> :: <type>\n\
+\  Add a new function available for Djinn to construct the result.\n\
+\Example:\n\
+\  Djinn> foo :: Int -> Char\n\
+\  Djinn> bar :: Char -> Bool\n\
+\  Djinn> f ? Int -> Bool\n\
+\  f :: Int -> Bool\n\
+\  f x3 = bar (foo x3)\n\
+\This feature is not as powerful as it first might seem.  Djinn does\n\
+\*not* instantiate polymorphic function.  It will only use the function\n\
+\with exactly the given type.  Example:\n\
+\  Djinn> cast :: a -> b\n\
+\  Djinn> f ? c->d\n\
+\  -- f cannot be realized.\n\
+\\n\
+\type <sym> <vars> = <type>\n\
+\  Add a Haskell style type synonym.  Type synonyms are expanded before\n\
+\Djinn starts looking for a realization.\n\
+\  Example:\n\
+\  Djinn> type Id a = a->a\n\
+\  Djinn> f ? Id a\n\
+\  f :: Id a\n\
+\  f x1 = x1\n\
+\\n\
+\data <sym> <vars> = <type>\n\
+\  Add a Haskell style data type.\n\
+\  Example:\n\
+\  Djinn> data Foo a = C a a a\n\
+\  Djinn> f ? a -> Foo a\n\
+\  f :: a -> Foo a\n\
+\  f x1 = C x1 x1 x1\n\
+\\n\
+\\n\
+\:clear\n\
+\  Set the environment to the start environment.\n\
+\\n\
+\\n\
+\:delete <sym>\n\
+\  Remove a symbol that has been added with the add command.\n\
+\\n\
+\\n\
+\:environment\n\
+\  List all added symbols and their types.\n\
+\\n\
+\\n\
+\:help\n\
+\  Show a short help message.\n\
+\\n\
+\\n\
+\:load <file>\n\
+\  Read and execute a file with commands.  The file may include Haskell\n\
+\style -- comments.\n\
+\\n\
+\\n\
+\:quit\n\
+\  Quit Djinn.\n\
+\\n\
+\\n\
+\:set\n\
+\  Set runtime options.\n\
+\     +multi    show multiple solutions\n\
+\               This will not show all solutions since there might be\n\
+\               infinitly many.\n\
+\     -multi    show one solution\n\
+\     +sorted   sort solutions according to a heuristic criterion\n\
+\     -sorted   do not sort solutions\n\
+\  The heuristic used to sort the solutions is that as many of the\n\
+\bound variables as possible should be used.\n\
+\\n\
+\:verbose-help\n\
+\  Print this message.\n\
+\\n\
+\\n\
+\Further examples\n\
+\================\n\
+\  calvin% djinn\n\
+\  Welcome to Djinn version 2005-12-11.\n\
+\  Type :h to get help.\n\
+\\n\
+\  -- return, bind, and callCC in the continuation monad\n\
+\  Djinn> data CD r a = CD ((a -> r) -> r)\n\
+\  Djinn> returnCD ? a -> CD r a\n\
+\  returnCD :: a -> CD r a\n\
+\  returnCD x1 = CD (\\ c15 -> c15 x1)\n\
+\\n\
+\  Djinn> bindCD ? CD r a -> (a -> CD r b) -> CD r b\n\
+\  bindCD :: CD r a -> (a -> CD r b) -> CD r b\n\
+\  bindCD x1 x4 =\n\
+\           case x1 of\n\
+\           CD v3 -> CD (\\ c49 ->\n\
+\                        v3 (\\ c50 ->\n\
+\                            case x4 c50 of\n\
+\                            CD c52 -> c52 c49))\n\
+\\n\
+\  Djinn> callCCD ? ((a -> CD r b) -> CD r a) -> CD r a\n\
+\  callCCD :: ((a -> CD r b) -> CD r a) -> CD r a\n\
+\  callCCD x1 =\n\
+\            CD (\\ c68 ->\n\
+\                case x1 (\\ c69 -> CD (\\ _ -> c68 c69)) of\n\
+\                CD c72 -> c72 c68)\n\
+\\n\
+\\n\
+\  -- return and bind in the state monad\n\
+\  Djinn> type S s a = (s -> (a, s))\n\
+\  Djinn> returnS ? a -> S s a\n\
+\  returnS :: a -> S s a\n\
+\  returnS x1 x2 = (x1, x2)\n\
+\  Djinn> bindS ? S s a -> (a -> S s b) -> S s b\n\
+\  bindS :: S s a -> (a -> S s b) -> S s b\n\
+\  bindS x1 x2 x3 =\n\
+\          case x1 x3 of\n\
+\          (v4, v5) -> x2 v4 v5\n\
+\\n\
+\\n\
+\Theory\n\
+\======\n\
+\  Djinn interprets a Haskell type as a logic formula using the\n\
+\Curry-Howard isomorphism and then uses a decision procedure for\n\
+\Intuitionistic Propositional Calculus.  This decision procedure is\n\
+\based on Gentzen's LJ sequent calculus, but in a modified form, LJT,\n\
+\that ensures termination.  This variation on LJ has a long history,\n\
+\but the particular formulation used in Djinn is due to Roy Dyckhoff.\n\
+\The decision procedure has been extended to generate a proof object\n\
+\(i.e., a lambda term).  It is this lambda term (in normal form) that\n\
+\constitutes the Haskell code.\n\
+\  See http://www.dcs.st-and.ac.uk/~rd/publications/jsl57.pdf for more\n\
+\on the exact method used by Djinn.\n\
+\\n\
+\  Since Djinn handles propositional calculus it also knows about the\n\
+\absurd proposition, corresponding to the empty set.  This set is\n\
+\called Void in Haskell, and Djinn assumes an elimination rule for the\n\
+\Void type:\n\
+\  void :: Void -> a\n\
+\Using Void is of little use for programming, but can be interesting\n\
+\for theorem proving.  Example, the double negation of the law of\n\
+\excluded middle:\n\
+\  Djinn> f ? Not (Not (Either x (Not x)))\n\
+\  f :: Not (Not (Either x (Not x)))\n\
+\  f x1 = void (x1 (Right (\\ c23 -> void (x1 (Left c23)))))\n\
+\"
diff --git a/Djinn/LJT.hs b/Djinn/LJT.hs
new file mode 100644
--- /dev/null
+++ b/Djinn/LJT.hs
@@ -0,0 +1,468 @@
+--
+-- Copyright (c) 2005, 2008 Lennart Augustsson
+-- See LICENSE for licensing details.
+--
+-- Intuitionistic theorem prover
+-- Written by Roy Dyckhoff, Summer 1991
+-- Modified to use the LWB syntax  Summer 1997
+-- and simplified in various ways...
+--
+-- Translated to Haskell by Lennart Augustsson December 2005
+--
+-- Incorporates the Vorob'ev-Hudelmaier etc calculus (I call it LJT)
+-- See RD's paper in JSL 1992:
+-- "Contraction-free calculi for intuitionistic logic"
+--
+-- Torkel Franzen (at SICS) gave me good ideas about how to write this
+-- properly, taking account of first-argument indexing,
+-- and I learnt a trick or two from Neil Tennant's "Autologic" book.
+
+module LJT (module LJTFormula, provable,
+            prove, Proof) where
+
+import Control.Monad
+import Data.List (partition)
+import Debug.Trace
+
+import LJTFormula
+
+mtrace :: String -> a -> a
+mtrace m x = if debug then trace m x else x
+-- wrap :: (Show a, Show b) => String -> a -> b -> b
+-- wrap fun args ret = mtrace (fun ++ ": " ++ show args) $
+--                     let o = show ret in seq o $
+--                     mtrace (fun ++ " returns: " ++ o) ret
+wrapM :: (Show a, Show b, Monad m) => String -> a -> m b -> m b
+wrapM fun args mret = do
+    () <- mtrace (fun ++ ": " ++ show args) $ return ()
+    ret <- mret
+    () <- mtrace (fun ++ " returns: " ++ show ret) $ return ()
+    return ret
+debug :: Bool
+debug = False
+
+type MoreSolutions = Bool
+
+provable :: Formula -> Bool
+provable a = not $ null $ prove False [] a
+
+prove :: MoreSolutions -> [(Symbol, Formula)] -> Formula -> [Proof]
+prove more env a = runP $ redtop more env a
+
+redtop :: MoreSolutions -> [(Symbol, Formula)] -> Formula -> P Proof
+redtop more ifs a = do
+    let form = foldr (:->) a (map snd ifs)
+    p <- redant more [] [] [] [] form
+    nf (foldl Apply p (map (Var . fst) ifs))
+
+------------------------------
+-----
+type Proof = Term
+
+subst :: Term -> Symbol -> Term -> P Term
+subst b x term = sub term
+  where sub t@(Var s') = if x == s' then copy [] b else return t
+        sub (Lam s t) = liftM (Lam s) (sub t)
+        sub (Apply t1 t2) = liftM2 Apply (sub t1) (sub t2)
+        sub t = return t
+
+copy :: [(Symbol, Symbol)] -> Term -> P Term
+copy r (Var s) = return $ Var $ maybe s id $ lookup s r
+copy r (Lam s t) = do
+    s' <- newSym "c"
+    liftM (Lam s') $ copy ((s, s'):r) t
+copy r (Apply t1 t2) = liftM2 Apply (copy r t1) (copy r t2)
+copy _r t = return t
+
+------------------------------
+
+-- XXX The symbols used in the functions below must not clash
+-- XXX with any symbols from newSym.
+
+applyAtom :: Term -> Term -> Term
+applyAtom f a = Apply f a
+
+curryt :: Int -> Term -> Term
+curryt n p = foldr Lam (Apply p (applys (Ctuple n) (map Var xs))) xs
+  where xs = [ Symbol ("x_" ++ show i) | i <- [0 .. n-1] ]
+
+inj :: ConsDesc -> Int -> Term -> Term
+inj cd i p = Lam x $ Apply p (Apply (Cinj cd i) (Var x))
+  where x = Symbol "x"
+
+applyImp :: Term -> Term -> Term
+applyImp p q = Apply p (Apply q (Lam y $ Apply p (Lam x (Var y))))
+  where x = Symbol "x"
+        y = Symbol "y"
+
+-- ((c->d)->false) -> ((c->false)->false, d->false)
+-- p : (c->d)->false)
+-- replace p1 and p2 with the components of the pair
+cImpDImpFalse :: Symbol -> Symbol -> Term -> Term -> P Term
+cImpDImpFalse p1 p2 cdf gp = do
+    let p1b = Lam cf $ Apply cdf $ Lam x $ Apply (Ccases []) $ Apply (Var cf) (Var x)
+        p2b = Lam d $ Apply cdf $ Lam c $ Var d
+        cf = Symbol "cf"
+        x = Symbol "x"
+        d = Symbol "d"
+        c = Symbol "c"
+    subst p1b p1 gp >>= subst p2b p2
+
+------------------------------
+
+-- More simplifications:
+--  split where no variables used can be removed
+--  either with equal RHS can me merged.
+
+-- Compute the normal form
+nf :: Term -> P Term
+nf ee = spine ee []
+  where spine (Apply f a) as = do a' <- nf a; spine f (a' : as)
+        spine (Lam s e) [] = liftM (Lam s) (nf e)
+        spine (Lam s e) (a : as) = do e' <- subst a s e; spine e' as
+        spine (Csplit n) (b : tup : args) | istup && n <= length xs = spine (applys b xs) args
+          where (istup, xs) = getTup tup
+                getTup (Ctuple _) = (True, [])
+                getTup (Apply f a) = let (tf, as) = getTup f in (tf, a:as)
+                getTup _ = (False, [])
+        spine (Ccases []) (e@(Apply (Ccases []) _) : as) = spine e as
+        spine (Ccases cds) (Apply (Cinj _ i) x : as) | length as >= n = spine (Apply (as!!i) x) (drop n as)
+                where n = length cds
+        spine f as = return $ applys f as
+
+
+------------------------------
+----- Our Proof monad, P, a monad with state and multiple results
+
+-- Note, this is the non-standard way to combine state with multiple
+-- results.  But this is much better for backtracking.
+newtype P a = P { unP :: PS -> [(PS, a)] }
+
+instance Monad P where
+    return x = P $ \ s -> [(s, x)]
+    P m >>= f = P $ \ s ->
+        [ y | (s',x) <- m s, y <- unP (f x) s' ]
+
+instance Functor P where
+    fmap f (P m) = P $ \ s ->
+        [ (s', f x) | (s', x) <- m s ]
+
+instance MonadPlus P where
+    mzero = P $ \ _s -> []
+    P fxs `mplus` P fys = P $ \ s -> fxs s ++ fys s
+
+-- The state, just an integer for generating new variables
+data PS = PS !Integer
+startPS :: PS
+startPS = PS 1
+
+nextInt :: P Integer
+nextInt = P $ \ (PS i) -> [(PS (i+1), i)]
+
+none :: P a
+none = mzero
+
+many :: [a] -> P a
+many xs = P $ \ s -> zip (repeat s) xs
+
+atMostOne :: P a -> P a
+atMostOne (P f) = P $ \ s -> take 1 (f s)
+
+runP :: P a -> [a]
+runP (P m) = map snd (m startPS)
+
+
+------------------------------
+----- Atomic formulae
+data AtomF = AtomF Term Symbol
+    deriving (Eq)
+instance Show AtomF where
+    show (AtomF p s) = show p ++ ":" ++ show s
+
+type AtomFs = [AtomF]
+
+findAtoms :: Symbol -> AtomFs -> [Term]
+findAtoms s atoms = [ p | AtomF p s' <- atoms, s == s' ]
+
+--removeAtom :: Symbol -> AtomFs -> AtomFs
+--removeAtom s atoms = [ a | a@(AtomF _ s') <- atoms, s /= s' ]
+
+addAtom :: AtomF -> AtomFs -> AtomFs
+addAtom a as = if a `elem` as then as else a : as
+
+------------------------------
+----- Implications of one atom
+
+data AtomImp = AtomImp Symbol Antecedents
+     deriving (Show)
+type AtomImps = [AtomImp]
+
+extract :: AtomImps -> Symbol -> ([Antecedent], AtomImps)
+extract aatomImps@(atomImp@(AtomImp a' bs) : atomImps) a =
+    case compare a a' of
+    GT -> let (rbs, restImps) = extract atomImps a in (rbs, atomImp : restImps)
+    EQ -> (bs, atomImps)
+    LT -> ([], aatomImps)
+extract _ _ = ([], [])
+
+insert :: AtomImps -> AtomImp -> AtomImps
+insert [] ai = [ ai ]
+insert aatomImps@(atomImp@(AtomImp a' bs') : atomImps) ai@(AtomImp a bs) =
+    case compare a a' of
+    GT -> atomImp : insert atomImps ai
+    EQ -> AtomImp a (bs ++ bs') : atomImps
+    LT -> ai : aatomImps
+
+------------------------------
+----- Nested implications, (a -> b) -> c
+
+data NestImp = NestImp Term Formula Formula Formula -- NestImp a b c represents (a :-> b) :-> c
+    deriving (Eq)
+instance Show NestImp where
+    show (NestImp _ a b c) = show $ (a :-> b) :-> c
+
+type NestImps = [NestImp]
+
+addNestImp :: NestImp -> NestImps -> NestImps
+addNestImp n ns = if n `elem` ns then ns else n : ns
+
+------------------------------
+----- Ordering of nested implications
+heuristics :: Bool
+heuristics = True
+
+order :: NestImps -> Formula -> AtomImps -> NestImps
+order nestImps g atomImps =
+    if heuristics then
+        nestImps
+    else
+        let
+            good_for (NestImp _ _ _ (Disj [])) = True
+            good_for (NestImp _ _ _ g') = g == g'
+            nice_for (NestImp _ _ _ (PVar s)) =
+                case extract atomImps s of
+                (bs', _) -> let bs = [ b | A _ b <- bs'] in g `elem` bs || false `elem` bs
+            nice_for _ = False
+            (good, ok) = partition good_for nestImps
+            (nice, bad) = partition nice_for ok
+        in  good ++ nice ++ bad
+
+------------------------------
+----- Generate a new unique variable
+newSym :: String -> P Symbol
+newSym pre = do
+   i <- nextInt
+   return $ Symbol $ pre ++ show i
+
+------------------------------
+----- Generate all ways to select one element of a list
+select :: [a] -> P (a, [a])
+select zs = many [ del n zs | n <- [0 .. length zs - 1] ]
+  where del 0 (x:xs) = (x, xs)
+        del n (x:xs) = let (y,ys) = del (n-1) xs in (y, x:ys)
+        del _ _ = error "select"
+
+------------------------------
+-----
+
+data Antecedent = A Term Formula deriving (Show)
+type Antecedents = [Antecedent]
+
+type Goal = Formula
+
+--
+-- This is the main loop of the proof search.
+--
+-- The redant functions reduce antecedents and the redsucc
+-- function reduces the goal (succedent).
+--
+-- The antecedents are kept in four groups: Antecedents, AtomImps, NestImps, AtomFs
+--   Antecedents contains as yet unclassified antecedents; the redant functions
+--     go through them one by one and reduces and classifies them.
+--   AtomImps contains implications of the form (a -> b), where `a' is an atom.
+--     To speed up the processing it is stored as a map from the `a' to all the
+--     formulae it implies.
+--   NestImps contains implications of the form ((b -> c) -> d)
+--   AtomFs contains atomic formulae.
+--
+-- There is also a proof object associated with each antecedent.
+--
+redant :: MoreSolutions -> Antecedents -> AtomImps -> NestImps -> AtomFs -> Goal -> P Proof
+redant more antes atomImps nestImps atoms goal =
+    wrapM "redant" (antes, atomImps, nestImps, atoms, goal) $
+    case antes of
+    [] -> redsucc goal
+    a:l -> redant1 a l goal
+  where redant0 l g = redant more l atomImps nestImps atoms g
+        redant1 :: Antecedent -> Antecedents -> Goal -> P Proof
+        redant1 a@(A p f) l g =
+            wrapM "redant1" ((a, l), atomImps, nestImps, atoms, g) $
+            if f == g then
+                -- The goal is the antecedent, we're done.
+                -- XXX But we might want more?
+                if more then
+                    return p `mplus` redant1' a l g
+                else
+                    return p
+            else
+                redant1' a l g
+
+        -- Reduce the first antecedent
+        redant1' :: Antecedent -> Antecedents -> Goal -> P Proof
+        redant1' (A p (PVar s)) l g =
+           let af = AtomF p s
+               (bs, restAtomImps) = extract atomImps s
+           in  redant more ([A (Apply f p) b | A f b <- bs] ++ l) restAtomImps nestImps (addAtom af atoms) g
+        redant1' (A p (Conj bs)) l g = do
+           vs <- mapM (const (newSym "v")) bs
+           gp <- redant0 (zipWith (\ v a -> A (Var v) a) vs bs ++ l) g
+           return $ applys (Csplit (length bs)) [foldr Lam gp vs, p]
+        redant1' (A p (Disj ds)) l g = do
+           vs <- mapM (const (newSym "d")) ds
+           ps <- mapM (\ (v, (_, d)) -> redant1 (A (Var v) d) l g) (zip vs ds)
+           if null ds && g == Disj [] then
+               -- We are about to construct `void p : Void', so we shortcut
+               -- it with just `p'.
+               return p
+            else
+               return $ applys (Ccases (map fst ds)) (p : zipWith Lam vs ps)
+        redant1' (A p (a :-> b)) l g = redantimp p a b l g
+
+        redantimp :: Term -> Formula -> Formula -> Antecedents -> Goal -> P Proof
+        redantimp t c d a g =
+            wrapM "redantimp" (c,d,a,g) $
+            redantimp' t c d a g
+
+        -- Reduce an implication antecedent
+        redantimp' :: Term -> Formula -> Formula -> Antecedents -> Goal -> P Proof
+        -- p : PVar s -> b
+        redantimp' p (PVar s) b l g = redantimpatom p s b l g
+        -- p : (c & d) -> b
+        redantimp' p (Conj cs) b l g = do
+            x <- newSym "x"
+            let imp = foldr (:->) b cs
+            gp <- redant1 (A (Var x) imp) l g
+            subst (curryt (length cs) p) x gp
+        -- p : (c | d) -> b
+        redantimp' p (Disj ds) b l g = do
+            vs <- mapM (const (newSym "d")) ds
+            gp <- redant0 (zipWith (\ v (_, d) -> A (Var v) (d :-> b)) vs ds ++ l) g
+            foldM (\ r (i, v, (cd, _)) -> subst (inj cd i p) v r) gp (zip3 [0..] vs ds)
+        -- p : (c -> d) -> b
+        redantimp' p (c :-> d) b l g = redantimpimp p c d b l g
+
+        redantimpimp :: Term -> Formula -> Formula -> Formula -> Antecedents -> Goal -> P Proof
+        redantimpimp f b c d a g =
+            wrapM "redantimpimp" (b,c,d,a,g) $
+            redantimpimp' f b c d a g
+
+        -- Reduce a double implication antecedent
+        redantimpimp' :: Term -> Formula -> Formula -> Formula -> Antecedents -> Goal -> P Proof
+        -- next clause exploits ~(C->D) <=> (~~C & ~D)
+        -- which isn't helpful when D = false
+        redantimpimp' p c d (Disj []) l g | d /= false = do
+            x <- newSym "x"
+            y <- newSym "y"
+            gp <- redantimpimp (Var x) c false false (A (Var y) (d :-> false) : l) g
+            cImpDImpFalse x y p gp
+        -- p : (c -> d) -> b
+        redantimpimp' p c d b l g = redant more l atomImps (addNestImp (NestImp p c d b) nestImps) atoms g
+
+        -- Reduce an atomic implication
+        redantimpatom :: Term -> Symbol -> Formula -> Antecedents -> Goal -> P Proof
+        redantimpatom p s b l g =
+            wrapM "redantimpatom" (s,b,l,g) $
+            redantimpatom' p s b l g
+
+        redantimpatom' :: Term -> Symbol -> Formula -> Antecedents -> Goal -> P Proof
+        redantimpatom' p s b l g =
+          do
+            a <- cutSearch more $ many (findAtoms s atoms)
+            x <- newSym "x"
+            gp <- redant1 (A (Var x) b) l g
+            mtrace "redantimpatom: LLL" $
+             subst (applyAtom p a) x gp
+          `mplus`
+            (mtrace "redantimpatom: RRR" $
+             redant more l (insert atomImps (AtomImp s [A p b])) nestImps atoms g)
+{-
+            let ps = wrap "redantimpatom findAtoms" atoms $ findAtoms s atoms
+            in  if not (null ps) then do
+                    a <- cutSearch more $ many ps
+                    x <- newSym "x"
+                    gp <- redant1 (A (Var x) b) l g
+                    mtrace "redantimpatom: LLL" $
+                     subst (applyAtom p a) x gp
+                else
+                    mtrace "redantimpatom: RRR" $
+                     redant more l (insert atomImps (AtomImp s [A p b])) nestImps atoms g
+-}
+        -- Reduce the goal, with all antecedents already being classified
+        redsucc :: Goal -> P Proof
+        redsucc g =
+            wrapM "redsucc" (g, atomImps, nestImps, atoms) $
+            redsucc' g
+
+        redsucc' :: Goal -> P Proof
+        redsucc' a@(PVar s) =
+            (cutSearch more $ many (findAtoms s atoms))
+          `mplus`
+            -- The posin check is an optimization.  It gets a little slower without the test.
+            (if posin s atomImps nestImps then
+                redsucc_choice a
+            else
+                none)
+        redsucc' (Conj cs) = do
+            ps <- mapM redsucc cs
+            return $ applys (Ctuple (length cs)) ps
+        -- next clause deals with succedent (A v B) by pushing the
+        -- non-determinism into the treatment of implication on the left
+        redsucc' (Disj ds) = do
+            s1 <- newSym "_"
+            let v = PVar s1
+            redant0 [ A (Cinj cd i) $ d :-> v | (i, (cd, d)) <- zip [0..] ds ] v
+        redsucc' (a :-> b) = do
+            s <- newSym "x"
+            p <- redant1 (A (Var s) a) [] b
+            return $ Lam s p
+
+        -- Now we have the hard part; maybe lots of formulae
+        -- of form (C->D)->B  in nestImps to choose from!
+        -- Which one to take first? We user the order heuristic.
+        redsucc_choice :: Goal -> P Proof
+        redsucc_choice g =
+            wrapM "redsucc_choice" g $
+            redsucc_choice' g
+
+        redsucc_choice' :: Goal -> P Proof
+        redsucc_choice' g = do
+            let ordImps = order nestImps g atomImps
+            (NestImp p c d b, restImps) <-
+                mtrace ("redsucc_choice: order=" ++ show ordImps) $
+                select ordImps
+            x <- newSym "x"
+            z <- newSym "z"
+            qz <- redant more [A (Var z) $ d :-> b] atomImps restImps atoms (c :-> d)
+            gp <- redant more [A (Var x) b] atomImps restImps atoms g
+            subst (applyImp p (Lam z qz)) x gp
+
+posin :: Symbol -> AtomImps -> NestImps -> Bool
+posin g atomImps nestImps = posin1 g atomImps || posin2 g [ (a :-> b) :-> c | NestImp _ a b c <- nestImps ]
+
+posin1 :: Symbol -> AtomImps -> Bool
+posin1 g atomImps = any (\ (AtomImp _ bs) -> posin2 g [ b | A _ b <- bs]) atomImps
+
+posin2 :: Symbol -> [Formula] -> Bool
+posin2 g bs = any (posin3 g) bs
+
+posin3 :: Symbol -> Formula -> Bool
+posin3 g (Disj as) = all (posin3 g) (map snd as)
+posin3 g (Conj as) = any (posin3 g) as
+posin3 g (_ :-> b) = posin3 g b
+posin3 s (PVar s') = s == s'
+
+cutSearch :: MoreSolutions -> P a -> P a
+cutSearch False p = atMostOne p
+cutSearch True p = p
+
+---------------------------
diff --git a/Djinn/LJTFormula.hs b/Djinn/LJTFormula.hs
new file mode 100644
--- /dev/null
+++ b/Djinn/LJTFormula.hs
@@ -0,0 +1,103 @@
+--
+-- Copyright (c) 2005 Lennart Augustsson
+-- See LICENSE for licensing details.
+--
+module LJTFormula(Symbol(..), Formula(..), (<->), (&), (|:), fnot, false, true,
+        ConsDesc(..),
+        Term(..), applys, freeVars
+        ) where
+import Data.List(union, (\\))
+
+infixr 2 :->
+infix  2 <->
+infixl 3 |:
+infixl 4 &
+
+newtype Symbol = Symbol String
+     deriving (Eq, Ord)
+
+instance Show Symbol where
+    show (Symbol s) = s
+
+data ConsDesc = ConsDesc String Int     -- name and arity
+     deriving (Eq, Ord, Show)
+
+data Formula
+        = Conj [Formula]
+        | Disj [(ConsDesc, Formula)]
+        | Formula :-> Formula
+        | PVar Symbol
+     deriving (Eq, Ord)
+
+(<->) :: Formula -> Formula -> Formula
+x <-> y = (x:->y) & (y:->x)
+
+(&) :: Formula -> Formula -> Formula
+x & y = Conj [x, y]
+
+(|:) :: Formula -> Formula -> Formula
+x |: y = Disj [((ConsDesc "Left" 1), x), ((ConsDesc "Right" 1), y)]
+
+fnot :: Formula -> Formula
+fnot x = x :-> false
+
+false :: Formula
+false = Disj []
+
+true :: Formula
+true = Conj []
+
+-- Show formulae the LJT way
+instance Show Formula where
+    showsPrec _ (Conj []) = showString "true"
+    showsPrec _ (Conj [c]) = showParen True $ showString "&" . showsPrec 0 c
+    showsPrec p (Conj cs) =
+        showParen (p>40) $ loop cs
+          where loop [f] = showsPrec 41 f
+                loop (f : fs) = showsPrec 41 f . showString " & " . loop fs
+                loop [] = error "showsPrec Conj"
+    showsPrec _ (Disj []) = showString "false"
+    showsPrec _ (Disj [(_,c)]) = showParen True $ showString "|" . showsPrec 0 c
+    showsPrec p (Disj ds) =
+        showParen (p>30) $ loop ds
+          where loop [(_,f)] = showsPrec 31 f
+                loop ((_,f) : fs) = showsPrec 31 f . showString " v " . loop fs
+                loop [] = error "showsPrec Disj"
+    showsPrec _ (f1 :-> Disj []) =
+        showString "~" . showsPrec 100 f1
+    showsPrec p (f1 :-> f2) =
+        showParen (p>20) $ showsPrec 21 f1 . showString " -> " . showsPrec 20 f2
+    showsPrec p (PVar s) = showsPrec p s
+
+------------------------------
+
+data Term
+        = Var Symbol
+        | Lam Symbol Term
+        | Apply Term Term
+        | Ctuple Int
+        | Csplit Int
+        | Cinj ConsDesc Int
+        | Ccases [ConsDesc]
+        | Xsel Int Int Term             --- XXX just temporary by MJ
+    deriving (Eq, Ord)
+
+instance Show Term where
+    showsPrec p (Var s) = showsPrec p s
+    showsPrec p (Lam s e) = showParen (p > 0) $ showString "\\" . showsPrec 0 s . showString "." . showsPrec 0 e
+    showsPrec p (Apply f a) = showParen (p > 1) $ showsPrec 1 f . showString " " . showsPrec 2 a
+    showsPrec _ (Cinj _ i) = showString $ "Inj" ++ show i
+    showsPrec _ (Ctuple i) = showString $ "Tuple" ++ show i
+    showsPrec _ (Csplit n) = showString $ "split" ++ show n
+    showsPrec _ (Ccases cds) = showString $ "cases" ++ show (length cds)
+    showsPrec p (Xsel i n e) = showParen (p > 0) $ showString ("sel_" ++ show i ++ "_" ++ show n) . showString " " . showsPrec 2 e
+
+applys :: Term -> [Term] -> Term
+applys f as = foldl Apply f as
+
+freeVars :: Term -> [Symbol]
+freeVars (Var s) = [s]
+freeVars (Lam s e) = freeVars e \\ [s]
+freeVars (Apply f a) = freeVars f `union` freeVars a
+freeVars (Xsel _ _ e) = freeVars e
+freeVars _ = []
diff --git a/Djinn/LJTParse.hs b/Djinn/LJTParse.hs
new file mode 100644
--- /dev/null
+++ b/Djinn/LJTParse.hs
@@ -0,0 +1,98 @@
+--
+-- Copyright (c) 2005 Lennart Augustsson
+-- See LICENSE for licensing details.
+--
+module LJTParse(parseFormula, parseLJT) where
+import Data.Char(isAlphaNum)
+import Text.ParserCombinators.ReadP(ReadP, (+++), char, sepBy1, readP_to_S, skipSpaces, munch1, many)
+import LJTFormula
+
+parseFormula :: String -> Formula
+parseFormula = parser pTop
+
+parseLJT :: String -> Formula
+parseLJT = parser pLJT
+
+parser :: (Show a) => ReadP a -> String -> a
+parser p s =
+    let ess = readP_to_S p (removeComments s)
+    in  case filter (null . snd) ess of
+        [(e, "")] -> e
+        _ -> error ("bad parse: " ++ show ess)
+
+removeComments :: String -> String
+removeComments "" = ""
+removeComments ('%':cs) = skip cs
+  where skip "" = ""
+        skip s@('\n':_) = removeComments s
+        skip (_:s) = skip s
+removeComments (c:cs) = c : removeComments cs
+
+pTop :: ReadP Formula
+pTop = do
+   f <- pFormula
+   skipSpaces
+   return f
+
+pLJT :: ReadP Formula
+pLJT = do
+   schar 'f'
+   f <- pFormula
+   schar '.'
+   skipSpaces
+   return f
+
+pFormula :: ReadP Formula
+pFormula = do
+   f1 <- pDisjuction
+   ods <- many (do o <- pArrow; d <- pDisjuction; return (o, d))
+   let (op, f2) = foldr (\ (no, d) (oo, r) -> (no, d `oo` r)) (const, undefined) ods
+   return $ f1 `op` f2
+
+pArrow :: ReadP (Formula -> Formula -> Formula)
+pArrow =
+   (do schar '-'; char '>'; return (:->))
+   +++
+   (do schar '<'; char '-'; char '>'; return (<->))
+
+pDisjuction :: ReadP Formula
+pDisjuction = do
+   fs <- sepBy1 pConjunction (schar 'v')
+   return $ foldl1 (|:) fs
+
+pConjunction :: ReadP Formula
+pConjunction = do
+   fs <- sepBy1 pAtomic (schar '&')
+   return $ foldl1 (&) fs
+
+pAtomic :: ReadP Formula
+pAtomic = pNegation +++ pParen pFormula +++ pVar
+
+pNegation :: ReadP Formula
+pNegation = do
+    schar '~'
+    f <- pAtomic
+    return $ fnot f
+
+pVar :: ReadP Formula
+pVar = do
+    skipSpaces
+    cs <- munch1 isAlphaNum
+    case cs of
+        "false" -> return false
+        "true" -> return true
+        _ -> return $ PVar $ Symbol cs
+
+pParen :: ReadP a -> ReadP a
+pParen p = do
+    schar '('
+    e <- p
+    schar ')'
+    return e
+
+schar :: Char -> ReadP ()
+schar c = do
+    skipSpaces
+    char c
+    return ()
+
diff --git a/Djinn/MLJT.hs b/Djinn/MLJT.hs
new file mode 100644
--- /dev/null
+++ b/Djinn/MLJT.hs
@@ -0,0 +1,30 @@
+--
+-- Copyright (c) 2005 Lennart Augustsson
+-- See LICENSE for licensing details.
+--
+import System.IO
+import LJTParse
+import MJ
+
+main :: IO ()
+main = do
+    hSetBuffering stdout NoBuffering
+    hSetBuffering stderr NoBuffering
+    args <- getArgs
+    file <-
+            case args of
+                [a] -> readFile a
+                _ -> hGetContents stdin
+    let form = parseLJT file
+--      pr = provable form
+--      cpr = provable (fnot (fnot form))
+        mpr = take 25 $ prove False [] form
+    print form
+--    putStrLn $ "Classical " ++ show cpr
+--    putStrLn $ "Intuitionistic " ++ show pr
+--    putStrLn $ show mpr
+    case mpr of
+        [] -> return ()
+        terms -> do
+            putStrLn $ "proof : " ++ show form
+            putStrLn $ unlines (map (("proof = " ++) . show) terms)
diff --git a/Djinn/REPL.hs b/Djinn/REPL.hs
new file mode 100644
--- /dev/null
+++ b/Djinn/REPL.hs
@@ -0,0 +1,34 @@
+--
+-- Copyright (c) 2005 Lennart Augustsson
+-- See LICENSE for licensing details.
+--
+module REPL(REPL(..), repl) where
+import qualified Control.Exception
+import System.Console.Readline(readline, addHistory)
+
+data REPL s = REPL {
+    repl_init :: IO (String, s),                -- prompt and initial state
+    repl_eval :: s -> String -> IO (Bool, s),           -- quit flag and new state
+    repl_exit :: s -> IO ()
+    }
+
+repl :: REPL s -> IO ()
+repl p = do
+    (prompt, state) <- repl_init p
+    let loop s = (do
+            mline <- readline prompt
+            case mline of
+                Nothing -> loop s
+                Just line -> do
+                    (quit, s') <- repl_eval p s line
+                    if quit then
+                        repl_exit p s'
+                     else do
+                        addHistory line
+                        loop s'
+            ) `Control.Exception.catch` ( \ exc ->
+                do
+                    putStrLn $ "\nInterrupted (" ++ show exc ++ ")"
+                    loop s
+            )
+    loop state
diff --git a/Djinn/Util/Digraph.hs b/Djinn/Util/Digraph.hs
new file mode 100644
--- /dev/null
+++ b/Djinn/Util/Digraph.hs
@@ -0,0 +1,393 @@
+{- |
+ 
+  Module      :  Util.Digraph
+  Copyright   : 
+
+  Maintainer      : lib@galois.com
+  Stability       : 
+  Portability     : 
+  
+  Functional graph algorithms; code taken from King
+  and Launchbury's POPL paper (via GHC sources.)
+-}
+module Util.Digraph(
+
+	-- At present the only one with a "nice" external interface
+	stronglyConnComp, stronglyConnCompR, SCC(..),
+
+	Graph, Vertex, 
+	graphFromEdges, buildG, transposeG, reverseE, outdegree, indegree,
+
+	Tree(..), Forest,
+	showTree, showForest,
+
+	dfs, dff,
+	topSort,
+	components,
+	scc,
+	back, cross, forward,
+	reachable, path,
+	bcc
+
+    ) where
+
+------------------------------------------------------------------------------
+-- A version of the graph algorithms described in:
+-- 
+-- ``Lazy Depth-First Search and Linear Graph Algorithms in Haskell''
+--   by David King and John Launchbury
+-- 
+-- Also included is some additional code for printing tree structures ...
+------------------------------------------------------------------------------
+
+
+import Util.Sort ( sortLe ) -- merge sosrt
+
+import Control.Monad.ST
+import Data.Array.ST ( STArray, newArray, writeArray, readArray )
+
+-- std interfaces
+import Data.Maybe
+import Data.Array
+import Data.List  ( (\\) )
+
+{-
+%************************************************************************
+%*									*
+%*	External interface
+%*									*
+%************************************************************************
+-}
+
+data SCC vertex = AcyclicSCC vertex
+	        | CyclicSCC  [vertex] deriving Show
+
+stronglyConnComp
+	:: Ord key
+	=> [(node, key, [key])]		-- The graph; its ok for the
+					-- out-list to contain keys which arent
+					-- a vertex key, they are ignored
+	-> [SCC node]
+
+stronglyConnComp edges1
+  = map get_node (stronglyConnCompR edges1)
+  where
+    get_node (AcyclicSCC (n, _, _)) = AcyclicSCC n
+    get_node (CyclicSCC triples)     = CyclicSCC [n | (n,_,_) <- triples]
+
+-- The "R" interface is used when you expect to apply SCC to
+-- the (some of) the result of SCC, so you dont want to lose the dependency info
+stronglyConnCompR
+	:: Ord key
+	=> [(node, key, [key])]		-- The graph; its ok for the
+					-- out-list to contain keys which arent
+					-- a vertex key, they are ignored
+	-> [SCC (node, key, [key])]
+
+stronglyConnCompR [] = []  -- added to avoid creating empty array in graphFromEdges -- SOF
+stronglyConnCompR edges1
+  = map decode forest
+  where
+    (graph, vertex_fn) = graphFromEdges edges1
+    forest	       = scc graph
+    decode (Node v []) | mentions_itself v = CyclicSCC [vertex_fn v]
+		       | otherwise	   = AcyclicSCC (vertex_fn v)
+    decode other = CyclicSCC (dec other [])
+		 where
+		   dec (Node v ts) vs = vertex_fn v : foldr dec vs ts
+    mentions_itself v = v `elem` (graph ! v)
+
+{-
+%************************************************************************
+%*									*
+%*	Graphs
+%*									*
+%************************************************************************
+-}
+
+type Vertex  = Int
+type Table a = Array Vertex a
+type Graph   = Table [Vertex]
+type Bounds  = (Vertex, Vertex)
+type Edge    = (Vertex, Vertex)
+
+
+vertices :: Graph -> [Vertex]
+vertices  = indices
+
+edges    :: Graph -> [Edge]
+edges g   = [ (v, w) | v <- vertices g, w <- g!v ]
+
+mapT    :: (Vertex -> a -> b) -> Table a -> Table b
+mapT f t = array (bounds t) [ (,) v (f v (t!v)) | v <- indices t ]
+
+buildG :: Bounds -> [Edge] -> Graph
+buildG bounds1 edges1
+  = accumArray (flip (:)) [] bounds1 [(,) k v | (k,v) <- edges1]
+
+transposeG  :: Graph -> Graph
+transposeG g = buildG (bounds g) (reverseE g)
+
+reverseE    :: Graph -> [Edge]
+reverseE g   = [ (w, v) | (v, w) <- edges g ]
+
+outdegree :: Graph -> Table Int
+outdegree  = mapT numEdges
+             where numEdges _ ws = length ws
+
+indegree :: Graph -> Table Int
+indegree  = outdegree . transposeG
+
+
+graphFromEdges
+	:: Ord key
+	=> [(node, key, [key])]
+	-> (Graph, Vertex -> (node, key, [key]))
+graphFromEdges edgs
+  = (graph, \v -> vertex_map ! v)
+  where
+    max_v      	    = length edgs - 1
+    bounds1         = (0,max_v) :: (Vertex, Vertex)
+    sorted_edges    = sortLe le edgs
+      where
+       (_,k1,_) `le` (_,k2,_) = case k1 `compare` k2 of { GT -> False; _other -> True }
+    edges1	    = zipWith (,) [0..] sorted_edges
+
+    graph	    = array bounds1 [(,) v (mapMaybe key_vertex ks) | (,) v (_,    _, ks) <- edges1]
+    key_map	    = array bounds1 [(,) v k			       | (,) v (_,    k, _ ) <- edges1]
+    vertex_map	    = array bounds1 edges1
+
+    -- key_vertex :: key -> Maybe Vertex
+    -- 	returns Nothing for non-interesting vertices
+    key_vertex k   = find 0 max_v 
+		   where
+		     find a b | a > b 
+			      = Nothing
+		     find a b = case compare k (key_map ! mid) of
+				   LT -> find a (mid-1)
+				   EQ -> Just mid
+				   GT -> find (mid+1) b
+			      where
+			 	mid = (a + b) `div` 2
+
+{-
+%************************************************************************
+%*									*
+%*	Trees and forests
+%*									*
+%************************************************************************
+-}
+
+data Tree a   = Node a (Forest a)
+type Forest a = [Tree a]
+
+mapTree              :: (a -> b) -> (Tree a -> Tree b)
+mapTree f (Node x ts) = Node (f x) (map (mapTree f) ts)
+
+
+instance Show a => Show (Tree a) where
+  show t = showTree t
+
+showTree :: Show a => Tree a -> String
+showTree  = drawTree . mapTree show
+
+showForest :: Show a => Forest a -> String
+showForest  = unlines . map showTree
+
+drawTree        :: Tree String -> String
+drawTree         = unlines . draw
+ where
+  draw (Node x ts) = grp this (space (length this)) (stLoop ts)
+   where
+       this          = s1 ++ x ++ " "
+       space n       = take n (repeat ' ')
+
+       stLoop []     = [""]
+       stLoop [t]    = grp s2 "  " (draw t)
+       stLoop (t:xs) = grp s3 s4 (draw t) ++ [s4] ++ rsLoop xs
+
+       rsLoop []     = []
+       rsLoop [t]    = grp s5 "  " (draw t)
+       rsLoop (t:xs) = grp s6 s4 (draw t) ++ [s4] ++ rsLoop xs
+
+       grp a   rst   = zipWith (++) (a:repeat rst)
+
+       [s1,s2,s3,s4,s5,s6] = ["- ", "--", "-+", " |", " `", " +"]
+
+
+{-
+%************************************************************************
+%*									*
+%*	Depth first search
+%*									*
+%************************************************************************
+-}
+
+--type Set s    = MutableArray s Vertex Bool
+type Set s    = STArray s Vertex Bool
+
+mkEmpty      :: Bounds -> ST s (Set s)
+mkEmpty bnds  = newArray bnds False
+
+contains     :: Set s -> Vertex -> ST s Bool
+contains m v  = readArray m v
+
+include      :: Set s -> Vertex -> ST s ()
+include m v   = writeArray m v True
+
+
+dff          :: Graph -> Forest Vertex
+dff g         = dfs g (vertices g)
+
+dfs          :: Graph -> [Vertex] -> Forest Vertex
+dfs g vs      = prune (bounds g) (map (generate g) vs)
+
+generate     :: Graph -> Vertex -> Tree Vertex
+generate g v  = Node v (map (generate g) (g!v))
+
+prune        :: Bounds -> Forest Vertex -> Forest Vertex
+prune bnds ts = runST (mkEmpty bnds  >>= \m ->
+                       chop m ts)
+
+chop         :: Set s -> Forest Vertex -> ST s (Forest Vertex)
+chop _ []     = return []
+chop m (Node v ts : us)
+              = contains m v >>= \visited ->
+                if visited then
+                  chop m us
+                else
+                  include m v >>= \_  ->
+                  chop m ts   >>= \as ->
+                  chop m us   >>= \bs ->
+                  return (Node v as : bs)
+
+
+{-
+%************************************************************************
+%*									*
+%*	Algorithms
+%*									*
+%************************************************************************
+-}
+
+------------------------------------------------------------
+-- Algorithm 1: depth first search numbering
+------------------------------------------------------------
+
+preorder            :: Tree a -> [a]
+preorder (Node a ts) = a : preorderF ts
+
+preorderF           :: Forest a -> [a]
+preorderF ts         = concat (map preorder ts)
+
+{- UNUSED:
+preOrd :: Graph -> [Vertex]
+preOrd  = preorderF . dff
+-}
+
+tabulate        :: Bounds -> [Vertex] -> Table Int
+tabulate bnds vs = array bnds (zipWith (,) vs [1..])
+
+preArr          :: Bounds -> Forest Vertex -> Table Int
+preArr bnds      = tabulate bnds . preorderF
+
+
+------------------------------------------------------------
+-- Algorithm 2: topological sorting
+------------------------------------------------------------
+
+postorder :: Tree a -> [a]
+postorder (Node a ts) = postorderF ts ++ [a]
+
+postorderF   :: Forest a -> [a]
+postorderF ts = concat (map postorder ts)
+
+postOrd      :: Graph -> [Vertex]
+postOrd       = postorderF . dff
+
+topSort      :: Graph -> [Vertex]
+topSort       = reverse . postOrd
+
+
+------------------------------------------------------------
+-- Algorithm 3: connected components
+------------------------------------------------------------
+
+components   :: Graph -> Forest Vertex
+components    = dff . undirected
+
+undirected   :: Graph -> Graph
+undirected g  = buildG (bounds g) (edges g ++ reverseE g)
+
+
+------------------------------------------------------------
+-- Algorithm 4: strongly connected components
+------------------------------------------------------------
+
+scc  :: Graph -> Forest Vertex
+scc g = dfs g (reverse (postOrd (transposeG g)))
+
+
+------------------------------------------------------------
+-- Algorithm 5: Classifying edges
+------------------------------------------------------------
+
+{- UNUSED:
+tree              :: Bounds -> Forest Vertex -> Graph
+tree bnds ts       = buildG bnds (concat (map flat ts))
+		   where
+		     flat (Node v rs) = [ (v, w) | Node w us <- ts ] ++
+                    		        concat (map flat ts)
+
+-}
+
+back              :: Graph -> Table Int -> Graph
+back g post        = mapT select g
+ where select v ws = [ w | w <- ws, post!v < post!w ]
+
+cross             :: Graph -> Table Int -> Table Int -> Graph
+cross g pre post   = mapT select g
+ where select v ws = [ w | w <- ws, post!v > post!w, pre!v > pre!w ]
+
+forward           :: Graph -> Graph -> Table Int -> Graph
+forward g tree pre = mapT select g
+ where select v ws = [ w | w <- ws, pre!v < pre!w ] \\ tree!v
+
+
+------------------------------------------------------------
+-- Algorithm 6: Finding reachable vertices
+------------------------------------------------------------
+
+reachable    :: Graph -> Vertex -> [Vertex]
+reachable g v = preorderF (dfs g [v])
+
+path         :: Graph -> Vertex -> Vertex -> Bool
+path g v w    = w `elem` (reachable g v)
+
+------------------------------------------------------------
+-- Algorithm 7: Biconnected components
+------------------------------------------------------------
+
+
+bcc :: Graph -> Forest [Vertex]
+bcc g = (concat . map bicomps . map (label g dnum)) forest
+ where forest = dff g
+       dnum   = preArr (bounds g) forest
+
+label :: Graph -> Table Int -> Tree Vertex -> Tree (Vertex,Int,Int)
+label g dnum (Node v ts) = Node (v,dnum!v,lv) us
+ where us = map (label g dnum) ts
+       lv = minimum ([dnum!v] ++ [dnum!w | w <- g!v]
+                     ++ [lu | Node (_, _, lu) _ <- us])
+
+bicomps :: Tree (Vertex,Int,Int) -> Forest [Vertex]
+bicomps (Node (v,_,_) ts)
+      = [ Node (v:vs) us | (_, Node vs us) <- map collect ts]
+
+collect :: Tree (Vertex,Int,Int) -> (Int, Tree [Vertex])
+collect (Node (v,dv,lv) ts) = (lv, Node (v:vs) cs)
+ where collected = map collect ts
+       vs = concat [ ws | (lw, Node ws _) <- collected, lw<dv]
+       cs = concat [ if lw<dv then us else [Node (v:ws) us]
+                        | (lw, Node ws us) <- collected ]
+
diff --git a/Djinn/Util/Sort.hs b/Djinn/Util/Sort.hs
new file mode 100644
--- /dev/null
+++ b/Djinn/Util/Sort.hs
@@ -0,0 +1,110 @@
+{- Copyright (c) 2001,2002 Galois Connections, Inc.
+ -}
+{- |
+ 
+  Module      :  Util.Sort
+  Copyright   :  (c) Galois Connections 2001, 2002
+
+  Maintainer      : lib@galois.com
+  Stability       : 
+  Portability     : 
+  
+  Extra sorting functions - copied from GHC compiler sources (util\/Util.lhs)
+-}
+module Util.Sort where
+
+sortLt :: (a -> a -> Bool) 		-- Less-than predicate
+       -> [a] 				-- Input list
+       -> [a]				-- Result list
+
+sortLt lt l = qsort lt l []
+
+-- qsort is stable and does not concatenate.
+qsort :: (a -> a -> Bool) -- Less-than predicate
+      -> [a]		  -- xs, Input list
+      -> [a]              -- r,  Concatenate this list to the sorted input list
+      -> [a]		  -- Result = sort xs ++ r
+
+qsort _  []     r = r
+qsort _  [x]    r = x:r
+qsort lt (x:xs) r = qpart lt x xs [] [] r
+
+-- qpart partitions and sorts the sublists
+-- rlt contains things less than x,
+-- rge contains the ones greater than or equal to x.
+-- Both have equal elements reversed with respect to the original list.
+
+qpart :: (a -> a -> Bool) -> a -> [a] -> [a] -> [a] -> [a] -> [a]
+qpart lt x [] rlt rge r =
+    -- rlt and rge are in reverse order and must be sorted with an
+    -- anti-stable sorting
+    rqsort lt rlt (x : rqsort lt rge r)
+
+qpart lt x (y:ys) rlt rge r =
+    if lt y x then
+	-- y < x
+	qpart lt x ys (y:rlt) rge r
+    else
+	-- y >= x
+	qpart lt x ys rlt (y:rge) r
+
+-- rqsort is as qsort but anti-stable, i.e. reverses equal elements
+rqsort :: (a -> a -> Bool)    -- Less-than predicate
+       -> [a]		      -- xs, Input list
+       -> [a]		      -- r,  Concatenate this list to the sorted input
+       -> [a]		      -- Result = sort xs ++ r
+rqsort _ []      r = r
+rqsort _ [x]     r = x:r
+rqsort lt (x:xs) r = rqpart lt x xs [] [] r
+
+rqpart :: (a -> a -> Bool) -> a -> [a] -> [a] -> [a] -> [a] -> [a]
+rqpart lt x [] rle rgt r =
+    qsort lt rle (x : qsort lt rgt r)
+
+rqpart lt x (y:ys) rle rgt r =
+    if lt x y then
+	-- y > x
+	rqpart lt x ys rle (y:rgt) r
+    else
+	-- y <= x
+	rqpart lt x ys (y:rle) rgt r
+
+sortLe :: (a->a->Bool) -> [a] -> [a]
+sortLe le = generalNaturalMergeSort le
+
+mergeSort, naturalMergeSort :: Ord a => [a] -> [a]
+mergeSort = generalMergeSort (<=)
+naturalMergeSort = generalNaturalMergeSort (<=)
+
+generalMergeSort :: (a->a->Bool) -> [a] -> [a]
+generalMergeSort _ [] = []
+generalMergeSort p xs = (balancedFold (generalMerge p) . map (: [])) xs
+
+generalMerge :: (a -> a -> Bool) -> [a] -> [a] -> [a]
+generalMerge _ xs [] = xs
+generalMerge _ [] ys = ys
+generalMerge p (x:xs) (y:ys) | x `p` y   = x : generalMerge p xs (y:ys)
+			     | otherwise = y : generalMerge p (x:xs) ys
+
+balancedFold :: (a -> a -> a) -> [a] -> a
+balancedFold _ [] = error "Util.Sort.balancedFold: can't reduce an empty list"
+balancedFold _ [x] = x
+balancedFold f l  = balancedFold f (balancedFold' f l)
+
+balancedFold' :: (a -> a -> a) -> [a] -> [a]
+balancedFold' f (x:y:xs) = f x y : balancedFold' f xs
+balancedFold' _ xs = xs
+
+generalNaturalMergeSort :: (a -> a -> Bool) -> [a] -> [a]
+generalNaturalMergeSort _   [] = []
+generalNaturalMergeSort prd rs = (balancedFold (generalMerge prd) . group prd) rs
+  where
+   --group :: (a -> a -> Bool) -> [a] -> [[a]]
+   group _ []     = []
+   group p (l:ls) = group' ls l l (l:)
+    where
+     group' []     _     _     s  = [s []]
+     group' (x:xs) x_min x_max s 
+	| not (x `p` x_max) = group' xs x_min x (s . (x :)) 
+	| x `p` x_min       = group' xs x x_max ((x :) . s) 
+	| otherwise         = s [] : group' xs x x (x :) 
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,32 @@
+Copyright (c) 2005 Lennart Augustsson, Thomas Johnsson
+    Chalmers University of Technology
+All rights reserved.
+
+This code is derived from software written by Lennart Augustsson
+(lennart@augustsson.net).
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+1. Redistributions of source code must retain the above copyright
+   notice, this list of conditions and the following disclaimer.
+2. 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.
+3. None of the names of the copyright holders 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 ``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 HOLDERS 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.
+
+*** End of disclaimer. ***
diff --git a/Setup.lhs b/Setup.lhs
new file mode 100644
--- /dev/null
+++ b/Setup.lhs
@@ -0,0 +1,6 @@
+#!/usr/bin/runhaskell
+> module Main where
+
+> import Distribution.Simple
+
+> main = defaultMain
diff --git a/djinn.cabal b/djinn.cabal
new file mode 100644
--- /dev/null
+++ b/djinn.cabal
@@ -0,0 +1,22 @@
+Name:		djinn
+Version:	2008.1.18
+License:	BSD3
+License-file:	LICENSE
+Author:		Lennart Augustsson
+Maintainer:	lennart@augustsson.net
+Description:	Djinn uses an theorem prover for intuitionistic propositional logic
+		to generate a Haskell expression when given a type.
+Category:	source-tools
+Homepage:	http://www.augustsson.net/Darcs/Djinn/
+Synopsis:	Generate Haskell code from a type
+Build-Depends:	base, mtl, readline, pretty, array, containers
+
+Executable:     djinn
+Main-Is:        Djinn.hs
+Hs-Source-Dirs: Djinn/
+Other-modules:  Help, LJTParse, HCheck,  LJT, MLJT
+                HTypes, LJTFormula, REPL,
+                Util.Digraph, Util.Sort
+
+ghc-options:         -O2 -Wall -Werror -optl-Wl
+ghc-prof-options:    -prof -auto-all