lambdacube-2008.12.24: CubeExpr.hs
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)