lambdacube (empty) → 2008.12.24

raw patch · 20 files changed

+798/−0 lines, 20 filesdep +basedep +editlinedep +mtlsetup-changed

Dependencies added: base, editline, mtl, pretty

Files

• Cube.hs +117/−0
• CubeExpr.hs +402/−0
• LICENSE +31/−0
• Setup.lhs +6/−0
• bool.cube +22/−0
• char.cube +17/−0
• either.cube +11/−0
• exists.cube +8/−0
• extchar.cube +6/−0
• lambdacube.cabal +32/−0
• list.cube +23/−0
• listmisc.cube +26/−0
• maybe.cube +11/−0
• misc.cube +8/−0
• nat.cube +30/−0
• natmisc.cube +21/−0
• pair.cube +14/−0
• test.cube +6/−0
• unit.cube +4/−0
• void.cube +3/−0

@@ -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\+\"

@@ -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)

@@ -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. ***

@@ -0,0 +1,6 @@+#!/usr/bin/runhaskell+> module Main where++> import Distribution.Simple++> main = defaultMain

@@ -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;

@@ -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);

@@ -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;

@@ -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;

@@ -0,0 +1,6 @@+Char :: *;+'a' :: Char;+'b' :: Char;+'c' :: Char;+'d' :: Char;+eqChar :: Char->Char->Bool;

@@ -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+

@@ -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;

@@ -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;

@@ -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;

@@ -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;+

@@ -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;

@@ -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);

@@ -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;

@@ -0,0 +1,6 @@+let Char :: *;+    'b' :: Char;+in++replicate Char 3 'b'+

@@ -0,0 +1,4 @@+Unit :: *;+Unit = forall unitT::* . unitT -> unitT;+unit :: Unit;+unit = \ (unitT::*) (x::unitT) -> x;

@@ -0,0 +1,3 @@+Void :: *;+Void = forall voidT::* . voidT;+void (r::*) (v::Void) :: r = v r;