diff --git a/Cube.hs b/Cube.hs
new file mode 100644
--- /dev/null
+++ b/Cube.hs
@@ -0,0 +1,117 @@
+-- Simple interface to lambda cube type checker.
+import System.Environment(getArgs)
+import Data.Char(isSpace)
+import Data.List(sortBy)
+import Data.Function(on)
+import REPL
+import CubeExpr
+
+main :: IO ()
+main = do
+    args <- getArgs
+    case args of
+	["-?"] -> usage
+	["-help"] -> usage
+	["--help"] -> usage
+        [] -> interactive
+	_  -> batch args
+
+usage :: IO ()
+usage = putStr "\
+\Usage: cube           -- start in interactive mode\n\
+\       cube files     -- concatenate files, type check, evaluate\n\
+\       cube - files   -- insert let&in, concatenate files, type check, evaluate\n\
+\"
+
+batch :: [FilePath] -> IO ()
+batch ("-":names) = mapM readFile names >>= batch' . addIn . ("let " :)
+  where addIn ss = init ss ++ [" in "] ++ [last ss]
+batch names = mapM readFile names >>= batch'
+
+batch' :: [String] -> IO ()
+batch' files = do
+    let expr = unRight "Parse error: " $ unreads $ concat files
+        typ = unRight "Type error: " $ typeCheck expr
+    putStrLn $ "Type:\n" ++ show typ
+    putStrLn $ "Value:\n" ++ show (nf expr)
+
+unRight :: String -> Either String a -> a
+unRight msg (Left msg') = error $ msg ++ msg'
+unRight _ (Right a) = a
+
+unreads :: (Show a, Read a) => String -> Either String a
+unreads s =
+    let xss = reads s
+    in  case filter (null . snd) xss of
+        (x, _) : _ -> Right x  -- pick first when ambiguous.
+        _ -> 
+	    -- Find the shortest suffix and report error there.
+	    let rest = head $ sortBy (compare `on` length) $ map snd xss ++ [s]
+	        ls = length (filter (=='\n') s)
+		lrest = length (filter (=='\n') rest)
+	    in  Left $ "line " ++ show (ls - lrest) ++ ": " ++ rest
+
+data State = State { defs :: String, skipLam :: Bool } deriving (Show)
+
+interactive :: IO ()
+interactive = repl $ REPL { repl_init = cinit, repl_eval = ceval, repl_exit = cexit }
+  where cinit = do
+          putStrLn "Welcome to the Cube."
+	  putStrLn "Use :help to get help."
+	  return ("Cube> ", State "" False)
+	cexit _ = putStrLn "Bye."
+	ceval s line = do
+	    let rest = dropWhile isSpace $ dropWhile (not . isSpace) line
+	        load = readFile rest >>= addFile s
+		quit = return (True, s)
+		help = do putStrLn helpMsg; return (False, s)
+	    case words line of
+	      [] -> return (False, s)
+	      ":h" : _ -> help
+	      ":help" : _ -> help
+	      ":q" : _ -> quit
+	      ":quit" : _ -> quit
+	      ":let" : _ -> addFile s (rest ++ ";\n")
+	      ":l" : _ -> load
+	      ":load" : _ -> load
+	      ":defs" : _ -> do putStrLn (defs s); return (False, s)
+	      ":skip" : _ -> return (False, s { skipLam = not (skipLam s) })
+	      _ -> do evalPrint s line 
+	              return (False, s)
+
+        evalPrint s se = do
+	    mt <- readAndCheck s se
+	    case mt of
+	         Nothing -> return ()
+		 Just (e, t) -> do
+		     let v = nf e
+		         (v', t') = if skipLam s then skipLambda v t else (v, t)
+		     putStrLn $ show v' ++ "\n  ::\n" ++ show t'
+	    return (False, s)
+
+        addFile s n = do
+	     let s' = s { defs = defs s ++ n }
+	     mt <- readAndCheck s' "\\ (a::*) -> a"
+	     case mt of
+	         Nothing -> return (False, s)
+		 Just _ ->  return (False, s')
+
+	readAndCheck s e =
+	     case unreads $ "let " ++ defs s ++ " in " ++ e of
+	     Left msg -> do putStrLn $ "Syntax error: " ++ msg; return Nothing
+	     Right expr ->
+	         case typeCheck expr of
+		 Left msg -> do putStrLn $ "Type error: " ++ msg; return Nothing
+		 Right typ -> return $ Just (expr, typ)
+
+helpMsg :: String
+helpMsg = "\
+\Commands:\n\
+\  :defs        show loaded definitions\n\
+\  :let def     add definition\n\
+\  :load name   load file with definitions\n\
+\  :help        show this message\n\
+\  :quit        quit\n\
+\  :skip        toggle skipping initial lambdas\n\
+\  expr         evaluate expression\n\
+\"
diff --git a/CubeExpr.hs b/CubeExpr.hs
new file mode 100644
--- /dev/null
+++ b/CubeExpr.hs
@@ -0,0 +1,402 @@
+module CubeExpr(
+    Sym, Expr(..), Type,
+    subst, nf, alphaEq, typeCheck, skipLambda
+    ) where
+import Data.Char(isAlphaNum, isAlpha)
+import Data.List(union, (\\))
+import Control.Monad.Error
+import Text.PrettyPrint.HughesPJ(Doc, renderStyle, style, text, (<>), (<+>), parens, ($$),
+       				 vcat, punctuate, sep, fsep, nest)
+import Text.ParserCombinators.ReadP(ReadP, (+++), char, munch1, many1, string, pfail, sepBy,
+                                    optional, many, skipSpaces, readP_to_S, look)
+
+type Sym = String
+
+data Expr
+        = Var Sym
+        | App Expr Expr
+        | Lam Sym Type Expr
+        | Pi Sym Type Type
+	| Let Sym Type Expr Expr
+        | Kind Kind
+        deriving (Eq)
+
+type Type = Expr
+
+data Kind = Star | Box deriving (Eq)
+
+expandLet :: Sym -> Type -> Expr -> Expr -> Expr
+expandLet i t e b = App (Lam i t b) e
+
+freeVars :: Expr -> [Sym]
+freeVars (Var s) = [s]
+freeVars (App f a) = freeVars f `union` freeVars a
+freeVars (Lam i t e) = freeVars t `union` (freeVars e \\ [i])
+freeVars (Pi i k t) = freeVars k `union` (freeVars t \\ [i])
+freeVars (Let i t e b) = freeVars (expandLet i t e b)
+freeVars (Kind _) = []
+
+subst :: Sym -> Expr -> Expr -> Expr
+subst v x = sub
+  where sub e@(Var i) = if i == v then x else e
+        sub (App f a) = App (sub f) (sub a)
+        sub (Lam i t e) = abstr Lam i t e
+        sub (Pi i t e) = abstr Pi i t e
+	sub (Let i t e b) = let App (Lam i' t' b') e' = sub (expandLet i t e b)
+	    	       	    in  Let i' t' e' b'
+        sub (Kind k) = Kind k
+        fvx = freeVars x
+        cloneSym e i = loop i
+           where loop i' = if i' `elem` vars then loop (i ++ "'") else i'
+                 vars = fvx ++ freeVars e
+        abstr con i t e =
+            if v == i then
+                con i (sub t) e
+            else if i `elem` fvx then
+                let i' = cloneSym e i
+                    e' = substVar i i' e
+                in  con i' (sub t) (sub e')
+            else
+                con i (sub t) (sub e)
+
+whnf :: Expr -> Expr
+whnf ee = spine ee []
+  where spine (App f a) as = spine f (a:as)
+        spine (Lam s _ e) (a:as) = spine (subst s a e) as
+	spine (Let i t e b) as = spine (expandLet i t e b) as
+        spine f as = foldl App f as
+
+nf :: Expr -> Expr
+nf ee = spine ee []
+  where spine (App f a) as = spine f (a:as)
+        spine (Lam s t e) [] = Lam s (nf t) (nf e)
+        spine (Lam s _ e) (a:as) = spine (subst s a e) as
+        spine (Pi s k t) as = app (Pi s (nf k) (nf t)) as
+	spine (Let i t e b) as = spine (expandLet i t e b) as
+        spine f as = app f as
+        app f as = foldl App f (map nf as)
+
+substVar :: Sym -> Sym -> Expr -> Expr
+substVar s s' e = subst s (Var s') e
+
+alphaEq :: Expr -> Expr -> Bool
+alphaEq (App f a)   (App f' a')    = alphaEq f f' && alphaEq a a'
+alphaEq (Lam s t e) (Lam s' t' e') = alphaEq t t' && alphaEq e (substVar s' s e')
+alphaEq (Pi s k t)  (Pi s' k' t')  = alphaEq k k' && alphaEq t (substVar s' s t')
+alphaEq (Let s t e b) (Let s' t' e' b') = alphaEq t t' && alphaEq e e' && alphaEq b (substVar s' s b')
+alphaEq (Var s)     (Var s')       = s == s'
+alphaEq (Kind k)    (Kind k')      = k == k'
+alphaEq _ _ = False
+
+betaEq :: Expr -> Expr -> Bool
+betaEq e1 e2 = alphaEq (nf e1) (nf e2)
+
+-------------------------------
+
+type ErrorMsg = String
+
+data Env = Env [(Sym, Type)] deriving (Show)
+
+initalEnv :: Env
+initalEnv = Env []
+
+extend :: Sym -> Type -> Env -> Env
+extend s t (Env r) = Env ((s, t) : r)
+
+findVar :: Env -> Sym -> TC Type
+findVar (Env r) s =
+    case lookup s r of
+    Just t -> return t
+    Nothing -> throwError ("Cannot find variable " ++ s)
+
+type TC a = Either ErrorMsg a
+
+tCheck :: Env -> Expr -> TC Type
+tCheck r (Var s) =
+    findVar r s
+tCheck r (Let s t a e) = do
+    --tCheck r (expandLet s t a e)
+    tCheck r t
+    ta <- tCheck r a
+    when (not (betaEq ta t)) $ throwError $ "Bad let def\n" ++ show (ta, t)
+    te <- tCheck r (subst s a e)
+    tCheck r (Pi s t te)
+    return te
+tCheck r (App f a) = do
+    tf <- tCheckRed r f
+    case tf of
+     Pi x at rt -> do
+        ta <- tCheck r a
+        when (not (betaEq ta at)) $ throwError $ "Bad function argument type:\n" ++
+	     	  	     	    	       	 "Function: " ++ show (nf f) ++ "\n" ++
+						 "argument: " ++ show (nf a) ++ "\n" ++
+						 "expected type: " ++ show at ++ "\n" ++
+						 "     got type: " ++ show ta
+        return $ subst x a rt
+     _ -> throwError $ "Non-function in application: " ++ show tf
+tCheck r (Lam s t e) = do
+    tCheck r t
+    let r' = extend s t r
+    te <- tCheck r' e
+    let lt = Pi s t te
+    tCheck r lt
+    return lt
+tCheck r (Pi x a b) = do
+    s <- tCheckRed r a
+    let r' = extend x a r
+    t <- tCheckRed r' b
+    when ((s, t) `notElem` allowedKinds) $ throwError $ "Bad abstraction: " ++ show (Pi x a b)
+    return t
+tCheck _ (Kind Star) = return $ Kind Box
+tCheck _ (Kind Box) = throwError "Found a Box"
+
+allowedKinds :: [(Type, Type)]
+allowedKinds = [(Kind Star, Kind Star), (Kind Star, Kind Box), (Kind Box, Kind Star), (Kind Box, Kind Box)]
+
+tCheckRed :: Env -> Expr -> TC Type
+tCheckRed r e = do
+    t <- tCheck r e
+    return $ whnf t
+
+typeCheck :: Expr -> Either ErrorMsg Type
+typeCheck e = fmap nf $ tCheck initalEnv e
+--    case  of
+--    Left msg -> error ("Type error:\n" ++ msg)
+--    Right t -> nf t
+
+typeCheck' :: Expr -> Type
+typeCheck' e =
+    case tCheck initalEnv e of
+    Left msg -> error ("Type error:\n" ++ msg)
+    Right t -> nf t
+
+---------------------------------------------------------------------
+
+ppsExpr :: Expr -> String
+ppsExpr e = renderStyle style $ ppExpr 0 e
+
+ppExpr :: Int -> Expr -> Doc
+ppExpr p (Pi s t e) | s `notElem` freeVars e = pparens (p > 0) $ ppExpr 1 t <> text "->" <> ppExpr 0 e
+--ppExpr p (Pi s t e) = pparens (p > 0) $ (parens $ text s <> text "::" <> ppExpr 0 t) <> text "->" <> ppExpr 0 e
+ppExpr p l@(Pi _ _ _) = pparens (p > 0) $ text "forall" <+> (fsep $ args ++ [text ".", ppExpr 0 b])
+  where (args, b) = collectPi [] l
+        collectPi vts (Pi v t e) | v `elem` freeVars e = collectPi (ppBound v t : vts) e
+	collectPi vts e = (reverse vts, e)
+ppExpr p l@(Lam _ _ _) = pparens (p > 0) $ text "\\" <+> (fsep $ args ++ [text "->", ppExpr 0 b])
+  where (args, b) = collectLam [] l
+        collectLam vts (Lam v t e) = collectLam (ppBound v t : vts) e
+	collectLam vts e = (reverse vts, e)
+
+ppExpr p ee@(Let _ _ _ _) = 
+    let (stes, body) = collectBinds [] ee
+	ppBind (s, t, Just e) = sep [text s <+> text "::" <+> ppExpr 0 t <> text " =", nest 4 $ ppExpr 0 e]
+	ppBind (s, t, Nothing) = text s <+> text "::" <+> ppExpr 0 t
+	ppBinds xs = vcat $ punctuate (text ";") (map ppBind xs)
+	collectBinds bs (Let s t e b) = collectBinds (bs ++ [(s, t, Just e)]) b
+--	collectBinds bs (Lam s t b) = collectBinds (bs ++ [(s, t, Nothing)]) b
+	collectBinds bs b = (bs, b)
+    in  pparens (p > 0) $
+        (text "let " <> ppBinds stes) $$ (text "in  " <> ppExpr 0 body)
+
+ppExpr p (App f a) = pparens (p > 9) $ ppExpr 9 f <> text " " <> ppExpr 10 a
+ppExpr _ (Var s) = text s
+ppExpr _ (Kind Star) = text "*"
+ppExpr _ (Kind Box) = text "[]"
+
+ppBound :: Sym -> Expr -> Doc
+ppBound v t = parens $ text v <+> text "::" <+> ppExpr 0 t
+
+pparens :: Bool -> Doc -> Doc
+pparens True d = parens d
+pparens False d = d
+
+instance Show Expr where
+    show e = ppsExpr e
+
+-------------------------------------------------------
+
+instance Read Expr where
+    readsPrec _ = readP_to_S pTop . removeComments
+
+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 Expr
+pTop = do
+    e <- pExpr
+    skipSpaces
+    return e
+
+pExpr :: ReadP Expr
+pExpr = pAExpr +++ pPi +++ pLam +++ pLet
+
+pAExpr :: ReadP Expr
+pAExpr = pAtomExpr +++ pApply
+
+pType :: ReadP Expr
+pType = pExpr
+
+pAtomExpr :: ReadP Expr
+pAtomExpr = pVar +++ pKind +++ pParen pExpr
+
+pParen :: ReadP a -> ReadP a
+pParen p = do
+    schar '('
+    e <- p
+    schar ')'
+    return e
+
+pApply :: ReadP Expr
+pApply = do
+    f <- pAtomExpr
+    as <- many1 pAtomExpr
+    return $ foldl App f as
+
+pLet :: ReadP Expr
+pLet = do
+    skeyword "let"
+    stes <- sepBy pBind (schar ';')
+    optional (schar ';')
+    skeyword "in"
+    b <- pExpr
+    return $ eLets' stes b
+
+pBind :: ReadP (Sym, Type, Maybe Expr)
+pBind = pBindH +++ pBindR
+
+pBindH :: ReadP (Sym, Type, Maybe Expr)
+pBindH = do
+    sy <- pSym
+    sstring "::"
+    ty <- pType
+    schar ';'
+    sy' <- pSym
+    as <- many pSym
+    schar '='
+    b <- pExpr
+    e <- matchH ty as b
+    if sy /= sy' then
+        pfail
+     else
+        return (sy, ty, Just e)
+
+matchH :: Expr -> [Sym] -> Expr -> ReadP Expr
+matchH _ [] e = return e
+matchH (Pi v t t') (a:as) e | v == a || v == "_" = do
+    e' <- matchH t' as e
+    return (Lam a t e')
+matchH _ _ _ = pfail
+
+pBindR :: ReadP (Sym, Type, Maybe Expr)
+pBindR = do
+    let addT (s, t) r = Pi s t r
+	addE (s, t) e = Lam s t e
+    sy <- pSym
+    args <- many pArg
+    sstring "::"
+    rt <- pType
+    (do
+        schar '='
+        be <- pExpr
+        return (sy, foldr addT rt args, Just $ foldr addE be args)
+     ) +++
+       (return (sy, foldr addT rt args, Nothing))
+
+eLet' :: (Sym, Type, Maybe Expr) -> Expr -> Expr
+eLet' (s, t, Nothing) b = Lam s t b
+eLet' (s, t, Just e) b = Let s t e b
+
+eLets' :: [(Sym, Type, Maybe Expr)] -> Expr -> Expr
+eLets' stes b = foldr eLet' b stes
+
+pPi :: ReadP Expr
+pPi = pPiQuant +++ pPiArrow
+
+pPiQuant :: ReadP Expr
+pPiQuant = do
+    sstring "forall" -- +++ sstring "\\/"
+    sts <- (fmap (:[]) pVarType) +++ many1 (pParen pVarType)
+    schar '.'
+    e <- pType
+    return $ foldr (uncurry Pi) e sts
+--Pi s t e
+
+pPiArrow :: ReadP Expr
+pPiArrow = do
+    ts <- many1 (do e <- pPiArg; sstring "->"; return e)
+    rt <- pAExpr
+    return $ foldr (\ (s, t) r -> Pi s t r) rt ts
+  where pPiArg = pPiNoDep +++ pArg
+	pPiNoDep = do
+	    t <- pAExpr
+	    return ("_", t)
+
+pArg :: ReadP (Sym, Type)
+pArg = pParen pVarType
+
+pVarType :: ReadP (Sym, Type)
+pVarType = do
+    s <- pSym
+    sstring "::"
+    t <- pType
+    return (s, t)
+    
+pLam :: ReadP Expr
+pLam = do
+    schar '\\' --  +++ sstring "/\\"
+    sts <- fmap (:[]) pVarType +++ many1 (pParen pVarType)
+    sstring "->"
+    e <- pExpr
+    return $ foldr (uncurry Lam) e sts
+
+pVar :: ReadP Expr
+pVar = do
+    s <- pSym
+    return $ Var s
+
+pKind :: ReadP Expr
+pKind = do
+    (do schar '*'; return $ Kind Star) +++ (do sstring "[]"; return $ Kind Box)
+
+pSym :: ReadP Sym
+pSym = do
+    skipSpaces
+    cs <- munch1 isSym
+    if cs `elem` ["let", "in", "forall", "_"] then
+	pfail
+     else
+        return cs
+
+schar :: Char -> ReadP ()
+schar c = do
+    skipSpaces
+    char c
+    return ()
+
+sstring :: String -> ReadP ()
+sstring s = do
+    skipSpaces
+    string s
+    return ()
+
+skeyword :: String -> ReadP ()
+skeyword s = do
+    sstring s
+    cs <- look
+    case cs of
+     c:_ | isAlpha c -> pfail
+     _ -> return ()
+
+isSym :: Char -> Bool
+isSym c = isAlphaNum c || c `elem` "_'"
+
+-------
+
+skipLambda :: Expr -> Type -> (Expr, Type)
+skipLambda (Lam _ _ e) (Pi _ _ t) = skipLambda e t
+skipLambda e t = (e, t)
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,31 @@
+Copyright (c) 2007 Lennart Augustsson
+All rights reserved.
+
+This code is derived from software written by Lennart Augustsson
+(lennart@augustsson.net).
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+1. Redistributions of source code must retain the above copyright
+   notice, this list of conditions and the following disclaimer.
+2. Redistributions in binary form must reproduce the above copyright
+   notice, this list of conditions and the following disclaimer in the
+   documentation and/or other materials provided with the distribution.
+3. None of the names of the copyright holders may be used to endorse
+   or promote products derived from this software without specific
+   prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS ``AS IS'' AND ANY
+EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
+PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE COPYRIGHT HOLDERS BE
+LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
+CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR
+BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,
+WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE
+OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN
+IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+
+*** End of disclaimer. ***
diff --git a/Setup.lhs b/Setup.lhs
new file mode 100644
--- /dev/null
+++ b/Setup.lhs
@@ -0,0 +1,6 @@
+#!/usr/bin/runhaskell
+> module Main where
+
+> import Distribution.Simple
+
+> main = defaultMain
diff --git a/bool.cube b/bool.cube
new file mode 100644
--- /dev/null
+++ b/bool.cube
@@ -0,0 +1,22 @@
+-- The Bool type.
+
+Bool :: *;
+Bool = forall (boolT::*) . boolT->boolT->boolT;
+
+False :: Bool;
+False = \ (boolT::*) (false::boolT) (true::boolT) -> false;
+
+True  :: Bool;
+True = \ (boolT::*) (false::boolT) (true::boolT) -> true;
+
+if :: forall (a::*) . Bool -> a -> a -> a;
+if a b t f = b a f t;
+
+not :: Bool -> Bool;
+not b = if Bool b False True;
+
+and :: Bool -> Bool -> Bool;
+and x y = if Bool x y False;
+
+or :: Bool -> Bool -> Bool;
+or x y = if Bool x True y;
diff --git a/char.cube b/char.cube
new file mode 100644
--- /dev/null
+++ b/char.cube
@@ -0,0 +1,17 @@
+Char :: *;
+Char = forall (charT::*) . charT->charT->charT->charT->charT;
+
+'a' :: Char;
+'a' = \ (charT::*) (_'a'::charT) (_'b'::charT) (_'c'::charT) (_'d'::charT) -> _'a';
+'b' :: Char;
+'b' = \ (charT::*) (_'a'::charT) (_'b'::charT) (_'c'::charT) (_'d'::charT) -> _'b';
+'c' :: Char;
+'c' = \ (charT::*) (_'a'::charT) (_'b'::charT) (_'c'::charT) (_'d'::charT) -> _'c';
+'d' :: Char;
+'d' = \ (charT::*) (_'a'::charT) (_'b'::charT) (_'c'::charT) (_'d'::charT) -> _'d';
+
+eqChar :: Char -> Char -> Bool;
+eqChar x y = x Bool (y Bool True False False False)
+       	       	    (y Bool False True False False)
+		    (y Bool False False True False)
+		    (y Bool False False False True);
diff --git a/either.cube b/either.cube
new file mode 100644
--- /dev/null
+++ b/either.cube
@@ -0,0 +1,11 @@
+Either :: * -> * -> *;
+Either a b = forall (eitherT::*) . (a->eitherT) -> (b->eitherT) -> eitherT;
+
+Left :: forall (a::*) (b::*) . a -> Either a b;
+Left a b x = \ (eitherT::*) (left::a->eitherT) (right::b->eitherT) -> left x;
+
+Right :: forall (a::*) (b::*) . b -> Either a b;
+Right a b y = \ (r::*) (left::a->r) (right::b->r) -> right y;
+
+either :: forall (a::*) (b::*) (r::*) . (a->r) -> (b->r) -> Either a b -> r;
+either a b r left right s = s r left right;
diff --git a/exists.cube b/exists.cube
new file mode 100644
--- /dev/null
+++ b/exists.cube
@@ -0,0 +1,8 @@
+Exists :: forall (a::*) . (a->*) -> *;
+Exists a p = forall (r::*) . (forall x::a . (p x -> r)) -> r;
+
+pack :: forall (a::*) (p::a->*) . (x :: a) -> p x -> Exists a p;
+pack a p x q = \ (r::*) (f :: (forall y::a . (p y -> r))) -> f x q;
+
+unpack :: forall (a::*) (p::a->*) (r::*) . ((x::a)->p x->r) -> Exists a p -> r;
+unpack a p r f e = e r f;
diff --git a/extchar.cube b/extchar.cube
new file mode 100644
--- /dev/null
+++ b/extchar.cube
@@ -0,0 +1,6 @@
+Char :: *;
+'a' :: Char;
+'b' :: Char;
+'c' :: Char;
+'d' :: Char;
+eqChar :: Char->Char->Bool;
diff --git a/lambdacube.cabal b/lambdacube.cabal
new file mode 100644
--- /dev/null
+++ b/lambdacube.cabal
@@ -0,0 +1,32 @@
+Name:		lambdacube
+Version:	2008.12.24
+License:	BSD3
+License-file:	LICENSE
+Author:		Lennart Augustsson <lennart@augustsson.net>
+Maintainer:	Lennart Augustsson <lennart@augustsson.net>
+Category:	Compilers/Interpreters
+Synopsis:	A simple lambda cube type checker.
+Description:	A simple interactive lambda cube type checker and evaluator.
+Build-Depends:	base, pretty, mtl, editline
+Build-Type:	Simple
+Extra-source-files:
+		bool.cube
+		char.cube
+		either.cube
+		exists.cube
+		extchar.cube
+		list.cube
+		listmisc.cube
+		maybe.cube
+		misc.cube
+		nat.cube
+		natmisc.cube
+		pair.cube
+		test.cube
+		unit.cube
+		void.cube
+
+Executable:	cube
+Main-Is:	Cube.hs
+Other-modules:	CubeExpr
+
diff --git a/list.cube b/list.cube
new file mode 100644
--- /dev/null
+++ b/list.cube
@@ -0,0 +1,23 @@
+List :: * -> *;
+List e = forall (listT::*) . listT -> (e->listT->listT) -> listT;
+
+Nil :: forall (e::*) . List e;
+Nil e = \ (listT::*) (nil::listT) (cons::e->listT->listT) -> nil;
+
+Cons :: forall (e::*) . e -> List e -> List e;
+Cons e x xs = \ (listT::*) (nil::listT) (cons::e->listT->listT) -> cons x (xs listT nil cons);
+
+foldr :: forall (a::*) (b::*) . (a->b->b) -> b -> List a -> b;
+foldr a b f z xs = xs b z f;
+
+foldl :: forall (a::*) (b::*) . (b->a->b) -> b -> List a -> b;
+foldl a b f z xs = foldr a (b->b) (\ (x::a) (g::b->b) (v::b) -> g (f v x)) (\ (x::b) -> x) xs z;
+
+map :: forall (a::*) (b::*) . (a->b) -> List a -> List b;
+map a b f xs = foldr a (List b) (\ (x::a) (r::List b) -> Cons b (f x) r) (Nil b) xs;
+
+append :: forall (a::*) . List a -> List a -> List a;
+append a xs ys = foldr a (List a) (Cons a) ys xs;
+
+reverse :: forall (a::*) . List a -> List a;
+reverse a xs = foldl a (List a) (\ (r :: List a) (x :: a) -> Cons a x r) (Nil a) xs;
diff --git a/listmisc.cube b/listmisc.cube
new file mode 100644
--- /dev/null
+++ b/listmisc.cube
@@ -0,0 +1,26 @@
+
+iota :: Nat -> List Nat;
+iota n =
+    let LNat :: *;
+    	LNat = List Nat;
+        T :: *;
+        T = Pair Nat LNat;
+        step :: T -> T;
+        step nl = split Nat LNat T
+                        (\ (n::Nat) (l::LNat) -> PairC Nat LNat
+			   	    	     	       (Succ n) (Cons Nat n l))
+			nl;
+	start :: T;
+	start = PairC Nat LNat 0 (Nil Nat);
+        res :: T;
+	res = natprim T step start n;
+    in  reverse Nat (snd Nat LNat res);
+
+replicate :: forall (a::*) . Nat -> a -> List a;
+replicate a n x = map Nat a (\ i :: Nat -> x) (iota n);
+
+any :: forall a::* . (a -> Bool) -> List a -> Bool;
+any a p = foldr a Bool (\ (x::a) -> or (p x)) False;
+
+all :: forall a::* . (a -> Bool) -> List a -> Bool;
+all a p = foldr a Bool (\ (x::a) -> and (p x)) True;
diff --git a/maybe.cube b/maybe.cube
new file mode 100644
--- /dev/null
+++ b/maybe.cube
@@ -0,0 +1,11 @@
+Maybe :: * -> *;
+Maybe a = forall (maybeT::*) . maybeT->(a->maybeT)->maybeT;
+
+Nothing :: forall (a::*) . Maybe a;
+Nothing a = \ (maybeT::*) (nothing::maybeT) (just::a->maybeT) -> nothing;
+
+Just :: forall (a::*) . a -> Maybe a;
+Just a x = \ (maybeT::*) (nothing::maybeT) (just::a->maybeT) -> just x;
+
+maybe :: forall (a::*) (r::*) . r -> (a->r) -> Maybe a -> r;
+maybe a r nothing just s = s r nothing just;
diff --git a/misc.cube b/misc.cube
new file mode 100644
--- /dev/null
+++ b/misc.cube
@@ -0,0 +1,8 @@
+-- Some useful functions.
+
+id :: forall (a::*) . a -> a;
+id a x = x;
+
+const :: forall (a::*) (b::*) . a -> b -> a;
+const a b x y = x;
+
diff --git a/nat.cube b/nat.cube
new file mode 100644
--- /dev/null
+++ b/nat.cube
@@ -0,0 +1,30 @@
+Nat :: *;
+Nat = forall (natT::*) . natT -> (natT->natT) -> natT;
+
+0 :: Nat;
+0 = \ (natT::*) (zero::natT) (succ::natT->natT) -> zero;
+
+Succ :: Nat -> Nat;
+Succ n = \ (natT::*) (zero::natT) (succ::natT->natT) -> succ (n natT zero succ);
+
+natprim :: forall (r::*) . (r->r) -> r -> Nat -> r;
+natprim r succ zero n = n r zero succ;
+
+add :: Nat -> Nat -> Nat;
+add x y = x Nat y Succ;
+
+mul :: Nat -> Nat -> Nat;
+mul x y = x Nat 0 (add y);
+
+power :: Nat -> Nat -> Nat;
+power x y = y Nat (Succ 0) (mul x);
+
+isZero :: Nat -> Bool;
+isZero n = n Bool True (\ a::Bool -> False);
+
+1 :: Nat;
+1 = Succ 0;
+2 :: Nat;
+2 = Succ 1;
+3 :: Nat;
+3 = Succ 2;
diff --git a/natmisc.cube b/natmisc.cube
new file mode 100644
--- /dev/null
+++ b/natmisc.cube
@@ -0,0 +1,21 @@
+-- Predecessor, (provably) takes O(n) with these kind of numbers.
+-- pred 0 = 0
+pred :: Nat -> Nat;
+pred n = 
+    let BN :: *;
+        BN = Pair Bool Nat;
+        step :: BN -> BN;
+        step = split Bool Nat BN (\ (b::Bool) (p::Nat) -> PairC Bool Nat True (if Nat b (Succ p) 0));
+        bn :: BN;
+        bn = natprim BN step (PairC Bool Nat False 0) n;
+    in  snd Bool Nat bn;
+
+-- This subtraction is O(m*n).  Wow, it's bad. :)
+sub :: Nat -> Nat -> Nat;
+sub x y = natprim Nat pred x y;
+
+leNat :: Nat -> Nat -> Bool;
+leNat x y = isZero (sub x y);
+
+eqNat :: Nat -> Nat -> Bool;
+eqNat x y = and (leNat x y) (leNat y x);
diff --git a/pair.cube b/pair.cube
new file mode 100644
--- /dev/null
+++ b/pair.cube
@@ -0,0 +1,14 @@
+Pair :: * -> * -> *;
+Pair a b = forall (pairT::*) . (a->b->pairT) -> pairT;
+
+PairC :: forall (a::*) (b::*) . a -> b -> Pair a b;
+PairC a b x y = \ (pairT::*) (pair :: a->b->pairT) -> pair x y;
+
+fst :: forall (a::*) (b::*) . Pair a b -> a;
+fst a b p = p a (\ (x::a) (y::b) -> x);
+
+snd :: forall (a::*) (b::*) . Pair a b -> b;
+snd a b p = p b (\ (x::a) (y::b) -> y);
+
+split :: forall (a::*) (b::*) (r::*) . (a->b->r) -> Pair a b -> r;
+split a b r f p = p r f;
diff --git a/test.cube b/test.cube
new file mode 100644
--- /dev/null
+++ b/test.cube
@@ -0,0 +1,6 @@
+let Char :: *;
+    'b' :: Char;
+in
+
+replicate Char 3 'b'
+
diff --git a/unit.cube b/unit.cube
new file mode 100644
--- /dev/null
+++ b/unit.cube
@@ -0,0 +1,4 @@
+Unit :: *;
+Unit = forall unitT::* . unitT -> unitT;
+unit :: Unit;
+unit = \ (unitT::*) (x::unitT) -> x;
diff --git a/void.cube b/void.cube
new file mode 100644
--- /dev/null
+++ b/void.cube
@@ -0,0 +1,3 @@
+Void :: *;
+Void = forall voidT::* . voidT;
+void (r::*) (v::Void) :: r = v r;