diff --git a/Djinn/Djinn.hs b/Djinn/Djinn.hs
deleted file mode 100644
--- a/Djinn/Djinn.hs
+++ /dev/null
@@ -1,387 +0,0 @@
---
--- 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
deleted file mode 100644
--- a/Djinn/HCheck.hs
+++ /dev/null
@@ -1,152 +0,0 @@
---
--- 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
deleted file mode 100644
--- a/Djinn/HTypes.hs
+++ /dev/null
@@ -1,452 +0,0 @@
---
--- 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
deleted file mode 100644
--- a/Djinn/Help.hs
+++ /dev/null
@@ -1,177 +0,0 @@
-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
deleted file mode 100644
--- a/Djinn/LJT.hs
+++ /dev/null
@@ -1,468 +0,0 @@
---
--- 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
deleted file mode 100644
--- a/Djinn/LJTFormula.hs
+++ /dev/null
@@ -1,103 +0,0 @@
---
--- 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
deleted file mode 100644
--- a/Djinn/LJTParse.hs
+++ /dev/null
@@ -1,98 +0,0 @@
---
--- 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
deleted file mode 100644
--- a/Djinn/MLJT.hs
+++ /dev/null
@@ -1,30 +0,0 @@
---
--- 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
deleted file mode 100644
--- a/Djinn/REPL.hs
+++ /dev/null
@@ -1,34 +0,0 @@
---
--- 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
deleted file mode 100644
--- a/Djinn/Util/Digraph.hs
+++ /dev/null
@@ -1,393 +0,0 @@
-{- |
- 
-  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
deleted file mode 100644
--- a/Djinn/Util/Sort.hs
+++ /dev/null
@@ -1,110 +0,0 @@
-{- 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/Setup.lhs b/Setup.lhs
--- a/Setup.lhs
+++ b/Setup.lhs
@@ -1,4 +1,4 @@
-#!/usr/bin/runhaskell
+#!/usr/bin/env runhaskell
 > module Main where
 
 > import Distribution.Simple
diff --git a/djinn.cabal b/djinn.cabal
--- a/djinn.cabal
+++ b/djinn.cabal
@@ -1,5 +1,5 @@
 Name:		djinn
-Version:	2008.1.18
+Version:	2008.8.10
 License:	BSD3
 License-file:	LICENSE
 Author:		Lennart Augustsson
@@ -9,14 +9,14 @@
 Category:	source-tools
 Homepage:	http://www.augustsson.net/Darcs/Djinn/
 Synopsis:	Generate Haskell code from a type
+Build-type:	Simple
 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
+Hs-Source-Dirs: src
+Other-modules:  Help, HCheck,  LJT, HTypes, LJTFormula, REPL
 
-ghc-options:         -O2 -Wall -Werror -optl-Wl
+--ghc-options:         -O2 -Wall -Werror -optl-Wl
+ghc-options:         -Wall -optl-Wl
 ghc-prof-options:    -prof -auto-all
diff --git a/src/Djinn.hs b/src/Djinn.hs
new file mode 100644
--- /dev/null
+++ b/src/Djinn.hs
@@ -0,0 +1,425 @@
+--
+-- Copyright (c) 2005 Lennart Augustsson
+-- See LICENSE for licensing details.
+--
+module Main(main) where
+import Data.Char(isAlpha, isSpace)
+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 HTypes
+import HCheck(htCheckEnv, htCheckType)
+import Help
+
+--import Debug.Trace
+
+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 = 200
+    }
+ 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-08-10"
+
+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 $ prHSymbolOp 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) =
+    query s i ctx g
+runCmd s (Class c) = do
+    return (False, s { classes = c : classes s })
+
+query :: State -> String -> [Context] -> HType -> IO (Bool, State)
+query s 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 ps' = take (cutOff s) ps
+            let score 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  --trace (hPrClause c ++ " ++++ " ++ show r)
+                       (r, c)
+                e:es = nub $ 
+                        if sorted s then
+                            map snd $ sortBy (\ (x,_) (y,_) -> compare x y) $ map score ps'
+                        else
+                            map (termToHClause i) ps'
+                pr = putStrLn . hPrClause
+                sctx = if null ctx then "" else showContexts ctx ++ " => "
+            when (debug s) $ putStrLn ("+++ " ++ show (head ps))
+            putStrLn $ prHSymbolOp i ++ " :: " ++ sctx ++ show g
+            pr e
+            when (multi s) $ mapM_ (\ x -> putStrLn "-- or" >> pr x) es
+            return (False, 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) = prHSymbolOp i ++ " :: " ++ show t
+
+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),
+        (":verboseHelp",        "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 <methods>", "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 +++ pHSymbolOp
+    return $ Del s
+
+pLoad :: ReadP Cmd
+pLoad = do
+    skipSpaces
+    s <- munch1 (not . isSpace)
+    return $ Load s
+
+pAdd :: ReadP Cmd
+pAdd = do
+    i <- pHSymbolOp
+    sstring "::"
+    t <- pHType
+    optional $ schar ';'
+    return $ Add i t
+
+pQuery :: ReadP Cmd
+pQuery = do
+    i <- pHSymbolOp
+    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)
+    ctx <- 
+        do
+          schar '('
+          ctx <- sepBy1 pCtx (schar ',')
+          schar ')'
+          return ctx
+       +++
+        do
+          ctx <- pCtx
+          return [ctx]
+    sstring "=>"
+    return ctx
+
+pType :: ReadP Cmd
+pType = do
+    sstring "type"
+    syn <- pHSymbol True
+    do args <- many (pHSymbol False)
+       schar '='
+       t <- pHType
+       return $ Type (syn, (args, t, undefined))
+     +++
+      do
+       schar ':'; char ':'
+       k <- pHKind
+       return $ Type (syn, ([], HTAbstract syn k, 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))
+      +++
+     do
+       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
+    i <- pHSymbolOp
+    sstring "::"
+    t <- pHType
+    return (i, t)
+
+pHSymbolOp :: ReadP HSymbol
+pHSymbolOp = do
+    let pOpSym = satisfy (`elem` "~!#$%^&*-+=<>.:")
+    pHSymbol False +++ do schar '('; op <- many1 pOpSym; schar ')'; return op
+
+pSet :: ReadP Cmd
+pSet = pSetFlag +++ pSetVal
+
+pSetFlag :: ReadP Cmd
+pSetFlag = 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
+
+pSetVal :: ReadP Cmd
+pSetVal = do
+    pPrefix "cutoff"
+    schar '='
+    n <- many1 (satisfy (`elem` ['0'..'9']))
+    return $ Set $ \ s -> s { cutOff = read n }
+
+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 ] ++
+    [ "    cutoff=" ++ show (cutOff s) ++ " maximum number of solutions generated" ]
+
diff --git a/src/HCheck.hs b/src/HCheck.hs
new file mode 100644
--- /dev/null
+++ b/src/HCheck.hs
@@ -0,0 +1,154 @@
+--
+-- 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 Data.Graph(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 _ _ (HTAbstract _ k) = return k
+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
+iHKind _ (HTAbstract _ _) = error "iHKind HTAbstract"
+
+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: " ++ show (k1, k2)
+        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 $ "Undefined type variable " ++ v
+
+getConHKind :: KEnv -> HSymbol -> M HKind
+getConHKind env v =
+    case lookup v env of
+    Just k -> return k
+    Nothing -> lift $ Left $ "Undefined type " ++ v
+
+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 ]
+getHTCons (HTAbstract _ _) = []
diff --git a/src/HTypes.hs b/src/HTypes.hs
new file mode 100644
--- /dev/null
+++ b/src/HTypes.hs
@@ -0,0 +1,507 @@
+--
+-- Copyright (c) 2005 Lennart Augustsson
+-- See LICENSE for licensing details.
+--
+module HTypes(HKind(..), HType(..), HSymbol, hTypeToFormula, pHSymbol, pHType, pHDataType, pHTAtom, pHKind,
+        prHSymbolOp,
+        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
+	| HTAbstract HSymbol HKind              -- XXX Uninterpreted type, like a variable but different kind checking
+        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
+    showsPrec _ (HTAbstract s _) = showString s
+
+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
+
+pHKind :: ReadP HKind
+pHKind = do
+    ts <- sepBy1 pHKindA (do schar '-'; char '>')
+    return $ foldr1 KArrow ts
+
+pHKindA :: ReadP HKind
+pHKindA = (do schar '*'; return KStar) +++ pParen pHKind
+
+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 ]
+substHT _ t@(HTAbstract _ _) = t
+
+
+-------------------------------
+
+
+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 (prHSymbolOp f) <+> sep [sep (map (ppPat 10) ps) <+> text "=",
+                                               	    	     nest 2 $ ppExpr 0 e]
+
+prHSymbolOp :: HSymbol -> String
+prHSymbolOp s@(c:_) | not (isAlphaNum c) = "(" ++ s ++ ")"
+prHSymbolOp s = s
+
+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 $ collapeCase $ fixSillyAt $ 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 [ y | (x, y) <- ss, x == hs ] of
+                [] -> HPVar hs
+                [p] -> HPAt hs p
+                ps -> HPAt hs $ foldr1 combPat ps
+
+        combPat p p' | p == p' = p
+	combPat (HPVar v) p = HPAt v p
+	combPat p (HPVar v) = HPAt v p
+	combPat (HPTuple ps) (HPTuple ps') = HPTuple (zipWith combPat ps ps')
+	combPat p p' = error $ "unimplemented combPat: " ++ show (p, p')
+
+        hETuple [e] = e
+        hETuple es = HETuple es
+
+-- XXX This should be integrated into some earlier phase, but this is simpler.
+fixSillyAt :: HExpr -> HExpr
+fixSillyAt = fixAt []
+  where fixAt s (HELam ps e) = HELam ps' (fixAt (concat ss ++ s) e) where (ps', ss) = unzip $ map findSilly ps
+        fixAt s (HEApply f a) = HEApply (fixAt s f) (fixAt s a)
+	fixAt _ e@(HECon _) = e
+  	fixAt s e@(HEVar v) = maybe e HEVar $ lookup v s
+	fixAt s (HETuple es) = HETuple (map (fixAt s) es)
+	fixAt s (HECase e alts) = HECase (fixAt s e) (map (fixAtAlt s) alts)
+	fixAtAlt s (p, e) = (p', fixAt (s' ++ s) e) where (p', s') = findSilly p
+	findSilly p@(HPVar _) = (p, [])
+	findSilly p@(HPCon _) = (p, [])
+	findSilly (HPTuple ps) = (HPTuple ps', concat ss) where (ps', ss) = unzip $ map findSilly ps
+	findSilly (HPAt v p) = case findSilly p of
+	                       (p'@(HPVar v'), s) -> (p', (v, v'):s)
+			       (p', s) -> (HPAt v p', s)
+	findSilly (HPApply f a) = (HPApply f' a', sf ++ sa) where (f', sf) = findSilly f; (a', sa) = findSilly a
+
+-- XXX This shouldn't be needed.  There's similar code in hECase,
+-- but the fixSillyAt reveals new opportunities.
+collapeCase :: HExpr -> HExpr
+collapeCase (HELam ps e) = HELam ps (collapeCase e)
+collapeCase (HEApply f a) = HEApply (collapeCase f) (collapeCase a)
+collapeCase e@(HECon _) = e
+collapeCase e@(HEVar _) = e
+collapeCase (HETuple es) = HETuple (map collapeCase es)
+collapeCase (HECase e alts) =
+    case [(p, collapeCase b) | (p, b) <- alts ] of
+    (p, b) : pes | noBound p && all (\ (p', b') -> alphaEq b b' && noBound p') pes -> b
+    pes -> HECase (collapeCase e) pes
+ where noBound = all (== "_") . getBinderVarsHP
+
+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/src/Help.hs b/src/Help.hs
new file mode 100644
--- /dev/null
+++ b/src/Help.hs
@@ -0,0 +1,202 @@
+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 a = a\n\
+\   Djinn> sel ? ((a,b),(c,d)) -> (b,c)\n\
+\   sel :: ((a, b), (c, d)) -> (b, c)\n\
+\   sel ((_, a), (b, _)) = (a, b)\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 _ a = a\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 a = bar (foo a)\n\
+\  This feature is not as powerful as it first might seem.  Djinn does\n\
+\*not* instantiate polymorphic functions.  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 a = a\n\
+\\n\
+\type <sym> :: <kind>\n\
+\  Add an abstract (uninterpreted) type of the given type.\n\
+\An uninterpreted type behaves like a type variable during deduction.\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 a = C a a a\n\
+\\n\
+\data <sym> <vars>\n\
+\  Add an empty type.\n\
+\\n\
+\class <sym> <vars> where <methods>\n\
+\  Add a type class.  Example:\n\
+\   class Ord a where compare :: a -> a -> Ordering\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\
+\     cutoff=N  compute at most N solutions\n\
+\  The heuristic used to sort the solutions is that as many of the\n\
+\bound variables as possible should be used and that the function\n\
+\should be as short as possible.\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 a = CD (\\ b -> b a)\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 a b =\n\
+\         case a of\n\
+\         CD c -> CD (\\ d ->\n\
+\                     c (\\ e ->\n\
+\                        case b e of\n\
+\                        CD f -> f d))\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 a =\n\
+\          CD (\\ b ->\n\
+\              case a (\\ c -> CD (\\ _ -> b c)) of\n\
+\              CD d -> d b)\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 a b = (a, b)\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 a b c =\n\
+\        case a c of\n\
+\        (d, e) -> b d e\n\
+\\n\
+\\n\
+\  The function type may have a type class context, e.g.,\n\
+\   Djinn> refl ? (Eq a) => a -> Bool\n\
+\   refl :: (Eq a) => a -> Bool\n\
+\   refl a = a == a\n\
+\A context is simply interpreted as an additional (hidden) argument\n\
+\that contains all the methods.  Again, there is no instantiation of\n\
+\polymorphic functions, so classes where the methods are polymorphic\n\
+\do not work as expected.\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\
+\sometimes called Void in Haskell, and Djinn assumes an elimination\n\
+\rule for the 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 a = void (a (Right (\\ b -> a (Left b))))\n\
+\  The Not type has the definition 'type Not x = x -> Void'.  The\n\
+\regular version of the law of excluded middle cannot be proven, of\n\
+\course.\n\
+\   Djinn> f ? Either x (Not x)\n\
+\   -- f cannot be realized.\n\
+\"
diff --git a/src/LJT.hs b/src/LJT.hs
new file mode 100644
--- /dev/null
+++ b/src/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 use 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/src/LJTFormula.hs b/src/LJTFormula.hs
new file mode 100644
--- /dev/null
+++ b/src/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/src/REPL.hs b/src/REPL.hs
new file mode 100644
--- /dev/null
+++ b/src/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