From 7b6927e75468fab90b839beae24466fda7177cf4 Mon Sep 17 00:00:00 2001 From: Simon Huber Date: Tue, 15 Dec 2015 14:53:36 +0100 Subject: [PATCH] Bugfix for type checking glueElems by Fabian Ruch --- TypeChecker.hs | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/TypeChecker.hs b/TypeChecker.hs index c0af283..a342b07 100644 --- a/TypeChecker.hs +++ b/TypeChecker.hs @@ -262,7 +262,8 @@ checkGlueElem vu ts us = do unless (keys ts == keys us) (throwError ("Keys don't match in " ++ show ts ++ " and " ++ show us)) rho <- asks env - checkSystemsWith ts us (\_ vt u -> check (isoDom vt) u) + checkSystemsWith ts us + (\alpha vt u -> local (faceEnv alpha) $ check (isoDom vt) u) let vus = evalSystem rho us checkSystemsWith ts vus (\alpha vt vAlpha -> unlessM (app (isoFun vt) vAlpha === (vu `face` alpha)) $ @@ -291,10 +292,10 @@ mkIso vb = eval rho $ Pi (Lam "x" a $ IdP (Path (Name "_") a) (App g (App f x)) x) where [a,b,f,g,x,y] = map Var ["a","b","f","g","x","y"] rho = upd ("b",vb) emptyEnv - + checkIso :: Val -> Ter -> Typing () checkIso vb iso = check (mkIso vb) iso - + checkBranch :: (Label,Env) -> Val -> Branch -> Val -> Val -> Typing () checkBranch (OLabel _ tele,nu) f (OBranch c ns e) _ _ = do ns' <- asks names -- 2.34.1