Clean Resolver

diff --git a/TT.hs b/CTT.hs
similarity index 98%
rename from TT.hs
rename to CTT.hs
index be008461ef682881c6e6f4005337be3e4275a5b9..9324fe8fee06d0402c1ad3734a946d5293f10af4 100644 (file)
--- 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 9146f573012306e839660758b7d5a4807e6053f6..5edca5f598f4000959925a6259f87c48a9243f08 100644 (file)
--- 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 4b05ded5ee45e7cdf38d131e0a93dc752bfaad70..21e64d88936324d4dc45de16edd9f53e54c65e1d 100644 (file)
--- 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 6af143e5560f8d89fd11b3bbf9af84daa25ab704..d6a1a5dadd364d9f5db7513409d28aa4ca1326da 100644 (file)
--- 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 46fde7f2e2bdfa227300543ae9754dce325bfba5..f9e5e8c0a08304f5ce6a2920a450ff9f7bc7c86a 100644 (file)
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -12,7 +12,7 @@ import Control.Monad.Trans.Reader
 import Control.Monad.Error (throwError)\r
 import Control.Applicative\r
 \r
-import TT\r
+import CTT\r
 import Eval\r
 \r
 -- Type checking monad\r