Missing case for checking GlueElem against VCompU

diff --git a/TypeChecker.hs b/TypeChecker.hs
index c04b91ca7028f2886b357a6e34554a1ade9363c7..29bdad6b946d84b9a7391f18adb5baae380199e7 100644 (file)
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -210,6 +210,10 @@ check a t = case (a,t) of
     check va u\r
     vu <- evalTyping u\r
     checkGlueElem vu ts us\r
+  (VCompU va ves,GlueElem u us) -> do\r
+    check va u\r
+    vu <- evalTyping u\r
+    checkGlueElemU vu ves us\r
   _ -> do\r
     v <- infer t\r
     unlessM (v === a) $\r
@@ -272,6 +276,21 @@ checkGlueElem vu ts us = do
                    " doesn't match " ++ show vu)\r
   checkCompSystem vus\r
 \r
+-- Check a glueElem against VComp _ ves\r
+checkGlueElemU :: Val -> System Val -> System Ter -> Typing ()\r
+checkGlueElemU vu ves us = do\r
+  unless (keys ves == keys us)\r
+    (throwError ("Keys don't match in " ++ show ves ++ " and " ++ show us))\r
+  rho <- asks env\r
+  checkSystemsWith ves us\r
+    (\alpha ve u -> local (faceEnv alpha) $ check (ve @@ One) u)\r
+  let vus = evalSystem rho us\r
+  checkSystemsWith ves vus (\alpha ve vAlpha ->\r
+    unlessM (eqFun ve vAlpha === (vu `face` alpha)) $\r
+      throwError $ "Transport of glueElem (for compU) component " ++ show vAlpha ++\r
+                   " doesn't match " ++ show vu)\r
+  checkCompSystem vus\r
+\r
 checkGlue :: Val -> System Ter -> Typing ()\r
 checkGlue va ts = do\r
   checkSystemWith ts (\alpha tAlpha -> checkEquiv (va `face` alpha) tAlpha)\r