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

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