From: Anders <mortberg@chalmers.se>
Date: Tue, 21 Apr 2015 09:36:29 +0000 (+0200)
Subject: Remove unnecessary monadic code in Typechecker (no more localM!)
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=0e54eae0f8b9f7c2f8fccca50aaf0d402c5d2782;p=cubicaltt.git

Remove unnecessary monadic code in Typechecker (no more localM!)
---

diff --git a/TypeChecker.hs b/TypeChecker.hs
index bd5ea08..bebce36 100644
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -71,8 +71,8 @@ addSub iphi (TEnv k ind rho v) = TEnv k ind (Sub rho iphi) v
 addSubs :: [(Name,Formula)] -> TEnv -> TEnv
 addSubs = flip $ foldr addSub
 
-addType :: (Ident,Ter) -> TEnv -> Typing TEnv
-addType (x,a) tenv@(TEnv _ _ rho _) = return $ addTypeVal (x,eval rho a) tenv
+addType :: (Ident,Ter) -> TEnv -> TEnv
+addType (x,a) tenv@(TEnv _ _ rho _) = addTypeVal (x,eval rho a) tenv
 
 addBranch :: [(Ident,Val)] -> (Tele,Env) -> TEnv -> TEnv
 addBranch nvs (tele,env) (TEnv k ind rho v) =
@@ -81,8 +81,8 @@ addBranch nvs (tele,env) (TEnv k ind rho v) =
 addDecls :: [Decl] -> TEnv -> TEnv
 addDecls d (TEnv k ind rho v) = TEnv k ind (Def d rho) v
 
-addTele :: Tele -> TEnv -> Typing TEnv
-addTele xas lenv = foldM (flip addType) lenv xas
+addTele :: Tele -> TEnv -> TEnv
+addTele xas lenv = foldl (flip addType) lenv xas
 
 faceEnv :: Face -> TEnv -> TEnv
 faceEnv alpha tenv = tenv{env=env tenv `face` alpha}
@@ -98,13 +98,6 @@ getLblType c (Ter (Sum _ _ cas) r) = case lookupLabel c cas of
 getLblType c u = throwError ("expected a data type for the constructor "
                              ++ c ++ " but got " ++ show u)
 
--- Monadic version of local
-localM :: (TEnv -> Typing TEnv) -> Typing a -> Typing a
-localM f r = do
-  e <- ask
-  a <- f e
-  local (const a) r
-
 -- Monadic version of unless
 unlessM :: Monad m => m Bool -> m () -> m ()
 unlessM mb x = mb >>= flip unless x
@@ -167,7 +160,7 @@ check a t = case (a,t) of
         throwError $ "names in path label system" -- TODO
       mapM_ checkFresh is
       let iis = zip is (map Atom is)
-      local (addSubs iis) $ localM (addTele tele) $ do
+      local (addSubs iis . addTele tele) $ do
         checkSystemWith ts $ \alpha talpha ->
           local (faceEnv alpha) $ do
             -- NB: the type doesn't depend on is
@@ -236,13 +229,13 @@ checkTele :: Tele -> Typing ()
 checkTele []          = return ()
 checkTele ((x,a):xas) = do
   check VU a
-  localM (addType (x,a)) $ checkTele xas
+  local (addType (x,a)) $ checkTele xas
 
 -- Check a family
 checkFam :: Ter -> Typing ()
 checkFam (Lam x a b) = do
   check VU a
-  localM (addType (x,a)) $ check VU b
+  local (addType (x,a)) $ check VU b
 checkFam x = throwError $ "checkFam: " ++ show x
 
 -- Check that a system is compatible