reintroduce faceEnv

diff --git a/TypeChecker.hs b/TypeChecker.hs
index 6af84eccbefd0c7498891c7f59ac5879efdbb5ef..83431da252c5f19518619e19a666fa186046afea 100644 (file)
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -82,6 +82,9 @@ addDecls d (TEnv k rho v) = TEnv k (Def d rho) v
 addTele :: Tele -> TEnv -> Typing TEnv\r
 addTele xas lenv = foldM (flip addType) lenv xas\r
 \r
+faceEnv :: Face -> TEnv -> TEnv\r
+faceEnv alpha tenv = tenv{env=env tenv `face` alpha}\r
+\r
 -------------------------------------------------------------------------------\r
 -- | Various useful functions\r
 \r
@@ -231,8 +234,8 @@ checkCompSystem vus = do
 \r
 -- Check the values at corresponding faces with a function, assumes\r
 -- systems have the same faces\r
-checkSystemsWith ::\r
-  System a -> System b -> (Face -> a -> b -> Typing c) -> Typing ()\r
+checkSystemsWith :: System a -> System b -> (Face -> a -> b -> Typing c) ->\r
+                    Typing ()\r
 checkSystemsWith us vs f = sequence_ $ elems $ intersectionWithKey f us vs\r
 \r
 -- Check the faces of a system\r
@@ -332,11 +335,13 @@ checkPathSystem :: Ter -> Val -> System Ter -> Typing (System Val)
 checkPathSystem t0 va ps = do\r
   rho <- asks env\r
   checkCompSystem (evalSystem rho ps)\r
-  T.sequence $ mapWithKey (\alpha pAlpha -> do\r
-    (a0,a1) <- checkPath (constPath (va `face` alpha)) pAlpha\r
-    unlessM (a0 === eval (rho `face` alpha) t0) $\r
-      throwError $ "Incompatible system with " ++ show t0\r
-    return a1) ps\r
+  T.sequence $ mapWithKey (\alpha pAlpha ->\r
+    local (faceEnv alpha) $ do\r
+      rhoAlpha <- asks env\r
+      (a0,a1)  <- checkPath (constPath (va `face` alpha)) pAlpha\r
+      unlessM (a0 === eval rhoAlpha t0) $\r
+        throwError $ "Incompatible system with " ++ show t0\r
+      return a1) ps\r
 \r
 checks :: (Tele,Env) -> [Ter] -> Typing ()\r
 checks _              []     = return ()\r