From: Anders Mörtberg Date: Wed, 18 Mar 2015 09:15:33 +0000 (+0100) Subject: Clean Resolver X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=8ceaf972c5c3901071cac9a37f207c17fe4e58b5;p=cubicaltt.git Clean Resolver --- diff --git a/TT.hs b/CTT.hs similarity index 98% rename from TT.hs rename to CTT.hs index be00846..9324fe8 100644 --- a/TT.hs +++ b/CTT.hs @@ -1,4 +1,4 @@ -module TT where +module CTT where import Control.Applicative import Data.List @@ -28,8 +28,10 @@ type Tele = [(Binder,Ter)] -- Labelled sum: c (x1 : A1) .. (xn : An) type LblSum = [(Binder,Tele)] +type Decl = (Binder,(Ter,Ter)) + -- Mutual recursive definitions: (x1 : A1) .. (xn : An) and x1 = e1 .. xn = en -type Decls = [(Binder,(Ter,Ter))] +type Decls = [Decl] declBinders :: Decls -> [Binder] declBinders decls = [ x | (x,_) <- decls ] diff --git a/Eval.hs b/Eval.hs index 9146f57..5edca5f 100644 --- a/Eval.hs +++ b/Eval.hs @@ -3,7 +3,7 @@ module Eval where import Data.List import Data.Maybe (fromMaybe) -import TT +import CTT look :: String -> Env -> Val look x (Pair rho ((y,_),u)) | x == y = u diff --git a/Main.hs b/Main.hs index 4b05ded..21e64d8 100644 --- a/Main.hs +++ b/Main.hs @@ -16,7 +16,7 @@ import Exp.Abs hiding (NoArg) import Exp.Layout import Exp.ErrM -import TT +import CTT import Resolver import qualified TypeChecker as TC import qualified Eval as E diff --git a/Resolver.hs b/Resolver.hs index 6af143e..d6a1a5d 100644 --- a/Resolver.hs +++ b/Resolver.hs @@ -4,7 +4,7 @@ module Resolver where import Exp.Abs -import qualified TT +import qualified CTT import Control.Applicative import Control.Monad.Trans @@ -16,7 +16,7 @@ import Data.Functor.Identity import Data.List (nub) import Prelude hiding (pi) -type Ter = TT.Ter +type Ter = CTT.Ter -- | Useful auxiliary functions @@ -25,9 +25,6 @@ type Ter = TT.Ter a <:> b = (:) <$> a <*> b -- Un-something functions -unAIdent :: AIdent -> String -unAIdent (AIdent (_,x)) = x - unVar :: Exp -> Maybe AIdent unVar (Var x) = Just x unVar _ = Nothing @@ -69,7 +66,7 @@ data SymKind = Variable | Constructor -- local environment for constructors data Env = Env { envModule :: String, - variables :: [(TT.Binder,SymKind)] } + variables :: [(CTT.Binder,SymKind)] } deriving (Eq,Show) type Resolver a = ReaderT Env (ErrorT String Identity) a @@ -83,55 +80,46 @@ runResolver x = runIdentity $ runErrorT $ runReaderT x emptyEnv updateModule :: String -> Env -> Env updateModule mod e = e{envModule = mod} -insertBinder :: (TT.Binder,SymKind) -> Env -> Env +insertBinder :: (CTT.Binder,SymKind) -> Env -> Env insertBinder (x@(n,_),var) e | n == "_" || n == "undefined" = e | otherwise = e{variables = (x,var) : variables e} -insertBinders :: [(TT.Binder,SymKind)] -> Env -> Env +insertBinders :: [(CTT.Binder,SymKind)] -> Env -> Env insertBinders = flip $ foldr insertBinder -insertVar :: TT.Binder -> Env -> Env +insertVar :: CTT.Binder -> Env -> Env insertVar x = insertBinder (x,Variable) -insertVars :: [TT.Binder] -> Env -> Env +insertVars :: [CTT.Binder] -> Env -> Env insertVars = flip $ foldr insertVar -insertCon :: TT.Binder -> Env -> Env -insertCon x = insertBinder (x,Constructor) - -insertCons :: [TT.Binder] -> Env -> Env -insertCons = flip $ foldr insertCon - -getModule :: Resolver String -getModule = envModule <$> ask - -getVariables :: Resolver [(TT.Binder,SymKind)] -getVariables = variables <$> ask - -getLoc :: (Int,Int) -> Resolver TT.Loc -getLoc l = TT.Loc <$> getModule <*> pure l +getLoc :: (Int,Int) -> Resolver CTT.Loc +getLoc l = CTT.Loc <$> asks envModule <*> pure l -resolveAIdent :: AIdent -> Resolver TT.Binder +noLoc :: AIdent +noLoc = AIdent ((0,0),"_") + +resolveAIdent :: AIdent -> Resolver CTT.Binder resolveAIdent (AIdent (l,x)) = (x,) <$> getLoc l resolveVar :: AIdent -> Resolver Ter resolveVar (AIdent (l,x)) - | (x == "_") || (x == "undefined") = TT.Undef <$> getLoc l + | (x == "_") || (x == "undefined") = CTT.Undef <$> getLoc l | otherwise = do - modName <- getModule - vars <- getVariables - case TT.lookupIdent x vars of - Just Variable -> return $ TT.Var x - Just Constructor -> return $ TT.Con x [] + modName <- asks envModule + vars <- asks variables + case CTT.lookupIdent x vars of + Just Variable -> return $ CTT.Var x + Just Constructor -> return $ CTT.Con x [] _ -> throwError $ "Cannot resolve variable " ++ x ++ " at position " ++ show l ++ " in module " ++ modName lam :: (AIdent,Exp) -> Resolver Ter -> Resolver Ter lam (a,t) e = do - x <- resolveAIdent a + x <- resolveAIdent a t' <- resolveExp t - TT.Lam x t' <$> local (insertVar x) e + CTT.Lam x t' <$> local (insertVar x) e lams :: [(AIdent,Exp)] -> Resolver Ter -> Resolver Ter lams = flip $ foldr lam @@ -143,122 +131,96 @@ binds :: (Ter -> Ter) -> [(AIdent,Exp)] -> Resolver Ter -> Resolver Ter binds f = flip $ foldr $ bind f resolveExp :: Exp -> Resolver Ter -resolveExp U = return TT.U -resolveExp (Var x) = resolveVar x -resolveExp (App t s) = TT.mkApps <$> resolveExp x <*> mapM resolveExp xs - where (x,xs) = unApps t [s] -resolveExp (Sigma ptele b) = do - tele <- flattenPTele ptele - binds TT.Sigma tele (resolveExp b) -resolveExp (Pi ptele b) = do - tele <- flattenPTele ptele - binds TT.Pi tele (resolveExp b) -resolveExp (Fun a b) = bind TT.Pi (AIdent ((0,0),"_"), a) (resolveExp b) -resolveExp (Lam ptele t) = do - tele <- flattenPTele ptele - lams tele (resolveExp t) -resolveExp (Fst t) = TT.Fst <$> resolveExp t -resolveExp (Snd t) = TT.Snd <$> resolveExp t -resolveExp (Pair t0 t1) = TT.SPair <$> resolveExp t0 <*> resolveExp t1 -resolveExp (Let decls e) = do - (rdecls,names) <- resolveDecls decls - TT.mkWheres rdecls <$> local (insertBinders names) (resolveExp e) +resolveExp e = case e of + U -> return CTT.U + Var x -> resolveVar x + App t s -> CTT.mkApps <$> resolveExp x <*> mapM resolveExp xs + where (x,xs) = unApps t [s] + Sigma ptele b -> do + tele <- flattenPTele ptele + binds CTT.Sigma tele (resolveExp b) + Pi ptele b -> do + tele <- flattenPTele ptele + binds CTT.Pi tele (resolveExp b) + Fun a b -> bind CTT.Pi (noLoc,a) (resolveExp b) + Lam ptele t -> do + tele <- flattenPTele ptele + lams tele (resolveExp t) + Fst t -> CTT.Fst <$> resolveExp t + Snd t -> CTT.Snd <$> resolveExp t + Pair t0 t1 -> CTT.SPair <$> resolveExp t0 <*> resolveExp t1 + Let decls e -> do + (rdecls,names) <- resolveDecls decls + CTT.mkWheres rdecls <$> local (insertBinders names) (resolveExp e) resolveWhere :: ExpWhere -> Resolver Ter resolveWhere = resolveExp . unWhere -resolveBranch :: Branch -> Resolver (TT.Label,([TT.Binder],Ter)) -resolveBranch (Branch lbl args e) = do +resolveBranch :: Branch -> Resolver (CTT.Label,([CTT.Binder],Ter)) +resolveBranch (Branch (AIdent (_,lbl)) args e) = do binders <- mapM resolveAIdent args re <- local (insertVars binders) $ resolveWhere e - return (unAIdent lbl, (binders, re)) + return (lbl, (binders, re)) -resolveTele :: [(AIdent,Exp)] -> Resolver TT.Tele +resolveTele :: [(AIdent,Exp)] -> Resolver CTT.Tele resolveTele [] = return [] resolveTele ((i,d):t) = do x <- resolveAIdent i ((x,) <$> resolveExp d) <:> local (insertVar x) (resolveTele t) -resolveLabel :: Label -> Resolver (TT.Binder,TT.Tele) +resolveLabel :: Label -> Resolver (CTT.Binder,CTT.Tele) resolveLabel (Label n vdecl) = (,) <$> resolveAIdent n <*> resolveTele (flattenTele vdecl) -declsLabels :: [Decl] -> Resolver [TT.Binder] +declsLabels :: [Decl] -> Resolver [CTT.Binder] declsLabels decls = mapM resolveAIdent [ lbl | Label lbl _ <- sums ] where sums = concat [ sum | DeclData _ _ sum <- decls ] piToFam :: Exp -> Resolver Ter -piToFam (Fun a b) = lam (AIdent ((0,0),"_"),a) $ resolveExp b +piToFam (Fun a b) = lam (noLoc,a) $ resolveExp b piToFam (Pi ptele b) = do (x,a):tele <- flattenPTele ptele - lam (x,a) (binds TT.Pi tele (resolveExp b)) - --- Resolve Data or Def or Split declaration -resolveDecl :: Decl -> Resolver ((TT.Binder,(Ter,Ter)),[(TT.Binder,SymKind)]) -resolveDecl (DeclDef n tele t body) = do - f <- resolveAIdent n - let tele' = flattenTele tele - d <- lams tele' (resolveWhere body) - a <- binds TT.Pi tele' (resolveExp t) - return ((f,(a,d)),[(f,Variable)]) -resolveDecl (DeclData n tele sums) = do - f <- resolveAIdent n - let tele' = flattenTele tele - d <- lams tele' $ local (insertVar f) $ - TT.Sum <$> resolveAIdent n <*> mapM resolveLabel sums - a <- binds TT.Pi tele' (return TT.U) - cs <- mapM resolveAIdent [ lbl | Label lbl _ <- sums ] - return ((f,(a,d)),(f,Variable):map (,Constructor) cs) -resolveDecl (DeclSplit n tele t brs) = do - f <- resolveAIdent n - let tele' = flattenTele tele - vars <- mapM resolveAIdent $ map fst tele' - fam <- local (insertVars vars) $ piToFam t - brs' <- local (insertVars (f:vars)) (mapM resolveBranch brs) - a <- binds TT.Pi tele' (resolveExp t) - loc <- getLoc (case brs of Branch (AIdent (l,_)) _ _:_ -> l ; _ -> (0,0)) - body <- lams tele' (return $ TT.Split loc fam brs') - return $ ((f,(a,body)),[(f,Variable)]) - --- Resolve mutual declarations (possibly one) --- resolveMutuals :: [Decl] -> Resolver (TT.Decls,[(TT.Binder,SymKind)]) --- resolveMutuals decls = do --- binders <- mapM resolveAIdent idents --- cs <- declsLabels decls --- let cns = map fst cs ++ names --- when (nub cns /= cns) $ --- throwError $ "Duplicated constructor or ident: " ++ show cns --- rddecls <- --- mapM (local (insertVars binders . insertCons cs) . resolveDDecl) ddecls --- when (names /= map fst rddecls) $ --- throwError $ "Mismatching names in " ++ show decls --- rtdecls <- resolveTele tdecls --- return ([ (x,t,d) | (x,t) <- rtdecls | (_,d) <- rddecls ], --- map (,Constructor) cs ++ map (,Variable) binders) --- where --- idents = [ x | DeclType x _ <- decls ] --- names = [ unAIdent x | x <- idents ] --- tdecls = [ (x,t) | DeclType x t <- decls ] --- ddecls = [ t | t <- decls, not $ isTDecl t ] --- isTDecl d = case d of DeclType{} -> True; _ -> False - --- Resolve declarations -resolveDecls :: [Decl] -> Resolver ([TT.Decls],[(TT.Binder,SymKind)]) -resolveDecls [] = return ([],[]) + lam (x,a) (binds CTT.Pi tele (resolveExp b)) + +-- Resolve Data or Def or Split declarations +resolveDecl :: Decl -> Resolver (CTT.Decl,[(CTT.Binder,SymKind)]) +resolveDecl d = case d of + DeclDef n tele t body -> do + f <- resolveAIdent n + let tele' = flattenTele tele + a <- binds CTT.Pi tele' (resolveExp t) + d <- lams tele' (resolveWhere body) + return ((f,(a,d)),[(f,Variable)]) + DeclData n tele sums -> do + f <- resolveAIdent n + let tele' = flattenTele tele + a <- binds CTT.Pi tele' (return CTT.U) + d <- lams tele' $ local (insertVar f) $ + CTT.Sum <$> resolveAIdent n <*> mapM resolveLabel sums + cs <- mapM resolveAIdent [ lbl | Label lbl _ <- sums ] + return ((f,(a,d)),(f,Variable):map (,Constructor) cs) + DeclSplit n tele t brs -> do + f <- resolveAIdent n + let tele' = flattenTele tele + loc = snd f + a <- binds CTT.Pi tele' (resolveExp t) + vars <- mapM resolveAIdent $ map fst tele' + fam <- local (insertVars vars) $ piToFam t + brs' <- local (insertVars (f:vars)) (mapM resolveBranch brs) + body <- lams tele' (return $ CTT.Split loc fam brs') + return ((f,(a,body)),[(f,Variable)]) + +resolveDecls :: [Decl] -> Resolver ([CTT.Decls],[(CTT.Binder,SymKind)]) +resolveDecls [] = return ([],[]) resolveDecls (d:ds) = do - (rtd,names) <- resolveDecl d -- (TT.Binder,(Ter,Ter)) + (rtd,names) <- resolveDecl d (rds,names') <- local (insertBinders names) $ resolveDecls ds return ([rtd] : rds, names' ++ names) --- resolveDecls (DeclMutual defs : ds) = do --- (rdefs,names) <- resolveMutuals defs --- (rds, names') <- local (insertBinders names) $ resolveDecls ds --- return (rdefs : rds, names' ++ names) --- resolveDecls (decl:_) = throwError $ "Invalid declaration: " ++ show decl -resolveModule :: Module -> Resolver ([TT.Decls],[(TT.Binder,SymKind)]) -resolveModule (Module n imports decls) = - local (updateModule $ unAIdent n) $ resolveDecls decls +resolveModule :: Module -> Resolver ([CTT.Decls],[(CTT.Binder,SymKind)]) +resolveModule (Module (AIdent (_,n)) _ decls) = + local (updateModule n) $ resolveDecls decls -resolveModules :: [Module] -> Resolver ([TT.Decls],[(TT.Binder,SymKind)]) +resolveModules :: [Module] -> Resolver ([CTT.Decls],[(CTT.Binder,SymKind)]) resolveModules [] = return ([],[]) resolveModules (mod:mods) = do (rmod, names) <- resolveModule mod diff --git a/TypeChecker.hs b/TypeChecker.hs index 46fde7f..f9e5e8c 100644 --- a/TypeChecker.hs +++ b/TypeChecker.hs @@ -12,7 +12,7 @@ import Control.Monad.Trans.Reader import Control.Monad.Error (throwError) import Control.Applicative -import TT +import CTT import Eval -- Type checking monad