From: Simon Huber <hubsim@gmail.com>
Date: Mon, 18 Jan 2016 10:42:15 +0000 (+0100)
Subject: Missing case for checking GlueElem against VCompU
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=e631cc9abf127464efa5cd8fba7004b914903863;p=cubicaltt.git

Missing case for checking GlueElem against VCompU
---

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