From 86d23727c88aa18870a311f44460c8ab0fdc6428 Mon Sep 17 00:00:00 2001 From: Simon Huber Date: Tue, 16 Jun 2015 10:15:22 +0200 Subject: [PATCH] Don't require equivalences to be eta-expanded --- Eval.hs | 17 +++-------------- Resolver.hs | 8 +------- TypeChecker.hs | 52 ++++++++++++++------------------------------------ 3 files changed, 18 insertions(+), 59 deletions(-) diff --git a/Eval.hs b/Eval.hs index 7103af6..21bc555 100644 --- a/Eval.hs +++ b/Eval.hs @@ -429,13 +429,10 @@ hComp a u us | eps `Map.member` us = (us ! eps) @@ One -- with fiber a b f y = (x : a) * (f x = y) equivDom :: Val -> Val -equivDom (VPair a _) = a -equivDom x = error $ "equivDom: Not an equivalence: " ++ show x +equivDom = fstVal equivFun :: Val -> Val -equivFun (VPair _ (VPair f _)) = f -equivFun x = - error $ "equivFun: Not an equivalence: " ++ show x +equivFun = sndVal . fstVal -- TODO: adapt to equivs -- Every path in the universe induces an hiso @@ -465,19 +462,11 @@ equivFun x = -- ,(j ~> 1, inv (edown x))] -- t = Ter (Lam "x" ev1 $ Path j $ Comp ev (eminus x) tsys) eenv --- An equivalence for a type b is a four-tuple (a,f,s,t) where --- a : U --- f : a -> b --- s : (y : b) -> fiber a b f y --- t : (y : b) (w : fiber a b f y) -> s y = w --- with fiber a b f y = (x : a) * (f x = y) - - -- Every path in the universe induces an equivalence eqToEquiv :: Val -> Val eqToEquiv e = VPair e1 (VPair f (VPair s t)) where e1 = e @@ One - (i,j,k,x,y,w,ev) = (Name "i",Name "j",Name "k",Var "x",Var "y",Var "w",Var "E") + (i,j,x,y,w,ev) = (Name "i",Name "j",Var "x",Var "y",Var "w",Var "E") inv t = Path i $ AppFormula t (NegAtom i) evinv = inv ev (ev0, ev1) = (AppFormula ev (Dir Zero),AppFormula ev (Dir One)) -- (b,a) diff --git a/Resolver.hs b/Resolver.hs index 7d6e863..96ddc4d 100644 --- a/Resolver.hs +++ b/Resolver.hs @@ -205,13 +205,7 @@ resolveExp e = case e of IdP x y z -> CTT.IdP <$> resolveExp x <*> resolveExp y <*> resolveExp z Comp u v ts -> CTT.Comp <$> resolveExp u <*> resolveExp v <*> resolveSystem ts Fill u v ts -> CTT.Fill <$> resolveExp u <*> resolveExp v <*> resolveSystem ts - Glue u ts -> do - rs <- resolveSystem ts - let isEquiv (CTT.Pair _ (CTT.Pair _ (CTT.Pair _ _))) = True - isEquiv _ = False - unless (all isEquiv $ Map.elems rs) - (throwError $ "Not a system of equivalences: " ++ show rs) - CTT.Glue <$> resolveExp u <*> pure rs + Glue u ts -> CTT.Glue <$> resolveExp u <*> resolveSystem ts -- GlueElem u ts -> CTT.GlueElem <$> resolveExp u <*> resolveSystem ts -- GlueLine phi psi u -> -- CTT.GlueLine <$> resolveExp u <*> resolveFormula phi <*> resolveFormula psi diff --git a/TypeChecker.hs b/TypeChecker.hs index 13d0ba7..c1b33e4 100644 --- a/TypeChecker.hs +++ b/TypeChecker.hs @@ -112,35 +112,6 @@ mkVars ns ((x,a):xas) nu = let w@(VVar n _) = mkVarNice ns x (eval nu a) in (x,w) : mkVars (n:ns) xas (upd (x,w) nu) --- Construct "(_ : va) -> vb" -mkFun :: Val -> Val -> Val -mkFun va vb = VPi va (eval rho (Lam "_" (Var "a") (Var "b"))) - where rho = upd ("b",vb) (upd ("a",va) empty) - --- -- Construct "(x : b) -> IdP (<_> b) (f (g x)) x" --- mkSection :: Val -> Val -> Val -> Val --- mkSection vb vf vg = --- VPi vb (eval rho (Lam "x" b (IdP (Path (Name "_") b) (App f (App g x)) x))) --- where [b,x,f,g] = map Var ["b","x","f","g"] --- rho = upd ("g",vg) (upd ("f",vf) (upd ("b",vb) empty)) - --- Construct "(y : b) -> (x : va) * Id vb (vf x) y" -mkFiberCenter :: Val -> Val -> Val -> Val -mkFiberCenter va vb vf = - eval rho $ Pi (Lam "y" b $ - Sigma (Lam "x" a $ IdP (Path (Name "_") b) (App f x) y)) - where [a,b,f,x,y] = map Var ["a","b","f","x","y"] - rho = upds (zip ["a","b","f"] [va,vb,vf]) empty - --- Construct "(y : vb) (w : fiber va vb vf y) -> vs y = w -mkFiberIsCenter :: Val -> Val -> Val -> Val -> Val -mkFiberIsCenter va vb vf vs = - eval rho $ Pi (Lam "y" b $ - Pi (Lam "w" fib $ IdP (Path (Name "_") fib) (App s y) w)) - where [a,b,f,x,y,s,w] = map Var ["a","b","f","x","y","s","w"] - rho = upds (zip ["a","b","f","s"] [va,vb,vf,vs]) empty - fib = Sigma (Lam "x" a $ IdP (Path (Name "_") b) (App f x) y) - -- Test if two values are convertible (===) :: Convertible a => a -> a -> Typing Bool u === v = conv <$> asks names <*> pure u <*> pure v @@ -319,15 +290,18 @@ checkGlue va ts = do -- s : (y : b) -> fiber a b f y -- t : (y : b) (w : fiber a b f y) -> s y = w -- with fiber a b f y = (x : a) * (f x = y) +mkEquiv :: Val -> Val +mkEquiv vb = eval rho $ + Sigma $ Lam "a" U $ + Sigma $ Lam "f" (Pi (Lam "_" a b)) $ + Sigma $ Lam "s" (Pi (Lam "y" b $ fib)) $ + Pi (Lam "y" b $ Pi (Lam "w" fib $ IdP (Path (Name "_") fib) (App s y) w)) + where [a,b,f,x,y,s,w] = map Var ["a","b","f","x","y","s","w"] + rho = upd ("b",vb) empty + fib = Sigma (Lam "x" a $ IdP (Path (Name "_") b) (App f x) y) + checkEquiv :: Val -> Ter -> Typing () -checkEquiv vb (Pair a (Pair f (Pair s t))) = do - check VU a - va <- evalTyping a - check (mkFun va vb) f - vf <- evalTyping f - check (mkFiberCenter va vb vf) s - vs <- evalTyping s - check (mkFiberIsCenter va vb vf vs) t +checkEquiv vb equiv = check (mkEquiv vb) equiv checkBranch :: (Label,Env) -> Val -> Branch -> Val -> Val -> Typing () checkBranch (OLabel _ tele,nu) f (OBranch c ns e) _ _ = do @@ -390,7 +364,9 @@ checkPathSystem t0 va ps = do rhoAlpha <- asks env (a0,a1) <- checkPath (va `face` alpha) pAlpha unlessM (a0 === eval rhoAlpha t0) $ - throwError $ "Incompatible system " ++ showSystem ps ++ " with " ++ show t0 + throwError $ "Incompatible system " ++ showSystem ps ++ + ", component\n " ++ show pAlpha ++ + "\nincompatible with\n " ++ show t0 return a1) ps checkCompSystem (evalSystem rho ps) return v -- 2.34.1