From 41bff376f8f9518a15795e03c1462e7645271d37 Mon Sep 17 00:00:00 2001 From: Anders Date: Thu, 19 Mar 2015 18:53:47 +0100 Subject: [PATCH] Finish implementing comp --- CTT.hs | 7 +++++- Connections.hs | 10 +++++--- Eval.hs | 64 ++++++++++++++++++++++++++++++++++++++++++------ TypeChecker.hs | 59 +++++++++++++++++++++++--------------------- examples/nat.ctt | 23 ++++++++++++++++- 5 files changed, 123 insertions(+), 40 deletions(-) diff --git a/CTT.hs b/CTT.hs index e0d673f..3269bc2 100644 --- a/CTT.hs +++ b/CTT.hs @@ -124,6 +124,11 @@ isNeutral v = case v of mkVar :: Int -> Val -> Val mkVar k = VVar ('X' : show k) +unCon :: Val -> [Val] +unCon (VCon _ vs) = vs +-- unCon (KanUElem _ u) = unCon u +unCon v = error $ "unCon: not a constructor: " ++ show v + -------------------------------------------------------------------------------- -- | Environments @@ -248,7 +253,7 @@ showVal v = case v of VSnd u -> showVal u <> text ".2" VIdP v0 v1 v2 -> text "IdP" <+> showVals [v0,v1,v2] VPath i v -> char '<' <> text (show i) <> char '>' <+> showVal v - VAppFormula v phi -> showVal1 v <> char '@' <> text (show phi) + VAppFormula v phi -> showVal1 v <+> char '@' <+> text (show phi) VComp v0 v1 vs -> text "comp" <+> showVals [v0,v1] <+> text (showSystem vs) VTrans v0 v1 -> text "trans" <+> showVals [v0,v1] showVal1 v = case v of diff --git a/Connections.hs b/Connections.hs index c9facd9..ce52a5b 100644 --- a/Connections.hs +++ b/Connections.hs @@ -61,7 +61,7 @@ instance Arbitrary Face where arbitrary = Map.fromList <$> arbitrary showFace :: Face -> String -showFace alpha = concat [ "(" ++ show i ++ "," ++ show d ++ ")" +showFace alpha = concat [ "(" ++ show i ++ " = " ++ show d ++ ")" | (i,d) <- Map.toList alpha ] swapFace :: Face -> (Name,Name) -> Face @@ -100,6 +100,9 @@ meetId xs = xs `meet` xs == xs meets :: [Face] -> [Face] -> [Face] meets xs ys = nub [ meet x y | x <- xs, y <- ys, compatible x y ] +meetss :: [[Face]] -> [Face] +meetss xss = foldr meets [eps] xss + leq :: Face -> Face -> Bool alpha `leq` beta = meetMaybe alpha beta == Just alpha @@ -330,8 +333,9 @@ face = Map.foldWithKey (\i d a -> act a (i,Dir d)) type System a = Map Face a showSystem :: Show a => System a -> String -showSystem ts = concat $ intersperse ", " [ showFace alpha ++ " |-> " ++ show u - | (alpha,u) <- Map.toList ts ] +showSystem ts = + "[ " ++ concat (intersperse ", " [ showFace alpha ++ " |-> " ++ show u + | (alpha,u) <- Map.toList ts ]) ++ " ]" insertSystem :: Face -> a -> System a -> System a insertSystem alpha v ts = case find (comparable alpha) (Map.keys ts) of diff --git a/Eval.hs b/Eval.hs index eca1162..292c899 100644 --- a/Eval.hs +++ b/Eval.hs @@ -147,8 +147,14 @@ evals :: Env -> [(Ident,Ter)] -> [(Ident,Val)] evals env bts = [ (b,eval env t) | (b,t) <- bts ] evalSystem :: Env -> System Ter -> System Val -evalSystem rho = undefined -- Map.mapWithKey (\alpha -> eval (rho `face` alpha)) - +evalSystem rho ts = + let out = concat [ let betas = meetss [ invFormula (lookName i rho) d + | (i,d) <- Map.assocs alpha ] + in [ (beta,eval (rho `face` beta) talpha) | beta <- betas ] + | (alpha,talpha) <- Map.assocs ts ] + in mkSystem out + +-- TODO: Write using case-of app :: Val -> Val -> Val app (Ter (Lam x _ t) e) u = eval (Pair e (x,u)) t app (Ter (Split _ _ nvs) e) (VCon name us) = case lookup name nvs of @@ -156,6 +162,18 @@ app (Ter (Split _ _ nvs) e) (VCon name us) = case lookup name nvs of Nothing -> error $ "app: Split with insufficient arguments; " ++ " missing case for " ++ name app u@(Ter (Split _ _ _) _) v | isNeutral v = VSplit u v + +app kan@(VTrans (VPath i (VPi a f)) li0) ui1 = + let j = fresh (kan,ui1) + (aj,fj) = (a,f) `swap` (i,j) + u = transFillNeg j aj ui1 + ui0 = transNeg j aj ui1 + in trans j (app fj u) (app li0 ui0) +app kan@(VComp (VPi a f) li0 ts) ui1 = + let j = fresh (kan,ui1) + tsj = Map.map (@@ j) ts + in comp j (app f ui1) (app li0 ui1) + (Map.intersectionWith app tsj (border ui1 tsj)) app r s | isNeutral r = VApp r s app _ _ = error "app" @@ -198,7 +216,7 @@ transLine :: Val -> Val -> Val transLine u v = trans i (u @@ i) v where i = fresh (u,v) -trans :: Name -> Val -> Val -> Val +trans, transNeg :: Name -> Val -> Val -> Val trans i v0 v1 = case (v0,v1) of (VIdP a u v,w) -> let j = fresh (Atom i, v0, w) @@ -216,6 +234,7 @@ trans i v0 v1 = case (v0,v1) of Nothing -> error $ "comp: missing constructor in labelled sum " ++ n _ | isNeutral v0 || isNeutral v1 -> VTrans (VPath i v0) v1 | otherwise -> error "trans not implemented" +transNeg i a u = trans i (a `sym` i) u transFill, transFillNeg :: Name -> Val -> Val -> Val transFill i a u = trans j (a `conj` (i,j)) u @@ -238,10 +257,6 @@ compLine :: Val -> Val -> System Val -> Val compLine a u ts = comp i (a @@ i) u (Map.map (@@ i) ts) where i = fresh (a,u,ts) --- compNeg a u ts = comp a u (ts `sym` i) -comp :: Name -> Val -> Val -> System Val -> Val -comp = undefined - genComp, genCompNeg :: Name -> Val -> Val -> System Val -> Val genComp i a u ts | Map.null ts = trans i a u genComp i a u ts = comp i ai1 (trans i a u) ts' @@ -251,6 +266,11 @@ genComp i a u ts = comp i ai1 (trans i a u) ts' ts' = Map.mapWithKey comp' ts genCompNeg i a u ts = genComp i (a `sym` i) u (ts `sym` i) +fill, fillNeg :: Name -> Val -> Val -> System Val -> Val +fill i a u ts = comp j a u (ts `conj` (i,j)) + where j = fresh (Atom i,a,u,ts) +fillNeg i a u ts = (fill i a u (ts `sym` i)) `sym` i + genFill, genFillNeg :: Name -> Val -> Val -> System Val -> Val genFill i a u ts = genComp j (a `conj` (i,j)) u (ts `conj` (i,j)) where j = fresh (Atom i,a,u,ts) @@ -265,6 +285,33 @@ comps i ((x,a):as) e ((ts,u):tsus) = in vi1 : vs comps _ _ _ _ = error "comps: different lengths of types and values" +-- compNeg a u ts = comp a u (ts `sym` i) + +-- i is independent of a and u +comp :: Name -> Val -> Val -> System Val -> Val +comp i a u ts | eps `Map.member` ts = (ts ! eps) `face` (i ~> 1) +comp i a u ts | i `notElem` support ts = u +comp i a u ts | not (Map.null indep) = comp i a u ts' + where (ts',indep) = Map.partition (\t -> i `elem` support t) ts +comp i a u ts = let j = fresh (Atom i,a,u,ts) -- maybe only in vid?? + in case a of + VIdP p _ _ -> VPath j $ comp i (p @@ j) (u @@ j) (Map.map (@@ j) ts) + VSigma a f -> VSPair ui1 comp_u2 + where (t1s, t2s) = (Map.map fstVal ts, Map.map sndVal ts) + (u1, u2) = (fstVal u, sndVal u) + fill_u1 = fill i a u1 t1s + ui1 = comp i a u1 t1s + comp_u2 = genComp i (app f fill_u1) u2 t2s + VPi{} -> VComp a u (Map.map (VPath i) ts) + VU -> VComp VU u (Map.map (VPath i) ts) + _ | isNeutral a || isNeutralSystem ts || isNeutral u -> + VComp a u (Map.map (VPath i) ts) + Ter (Sum _ _ nass) env -> case u of + VCon n us -> case lookup n nass of + Just as -> VCon n $ comps i as env tsus + where tsus = transposeSystemAndList (Map.map unCon ts) us + Nothing -> error $ "comp: missing constructor in labelled sum " ++ n + _ -> error "comp ter sum" -- fills :: Name -> [(Ident,Ter)] -> Env -> [(System Val,Val)] -> [Val] -- fills i [] _ [] = [] @@ -278,6 +325,9 @@ comps _ _ _ _ = error "comps: different lengths of types and values" ------------------------------------------------------------------------------- -- | Conversion +isNeutralSystem :: System Val -> Bool +isNeutralSystem = any isNeutral . Map.elems + class Convertible a where conv :: Int -> a -> a -> Bool diff --git a/TypeChecker.hs b/TypeChecker.hs index 029dc41..a71aa28 100644 --- a/TypeChecker.hs +++ b/TypeChecker.hs @@ -122,6 +122,9 @@ checkFam (Lam x a b) = do localM (addType (x,a)) $ check VU b checkFam _ = throwError "checkFam" +constPath :: Val -> Val +constPath v = VPath (Name "_") v + -- Check that t has type a check :: Val -> Ter -> Typing () check a t = case (a,t) of @@ -158,18 +161,10 @@ check a t = case (a,t) of checkDecls d local (addDecls d) $ check a e (_,Undef _) -> return () - (VU,IdP a e0 e1) -> case a of - Path{} -> do - (b0,b1) <- checkPath a - check b0 e0 - check b1 e1 - _ -> do - b <- infer a - case b of - VIdP (VPath _ VU) b0 b1 -> do - check b0 e0 - check b1 e1 - _ -> throwError ("IdP expects a path but got " ++ show a) + (VU,IdP a e0 e1) -> do + (a0,a1) <- checkPath (constPath VU) a + check a0 e0 + check a1 e1 (VIdP p a0 a1,Path i e) -> do rho <- asks env k <- asks index @@ -179,7 +174,7 @@ check a t = case (a,t) of let u0 = eval (Sub rho (i,Dir 0)) e u1 = eval (Sub rho (i,Dir 1)) e unless (conv k a0 u0 && conv k a1 u1) $ - throwError $ "path endpoints don't match " ++ show e + throwError $ "path endpoints don't match " ++ show e ++ " \nu0 = " ++ show u0 ++ " \nu1 = " ++ show u1 ++ " \na0 = " ++ show a0 ++ " \na1 = " ++ show a1 ++ " \np = " ++ show p _ -> do v <- infer t k <- index <$> ask @@ -244,16 +239,10 @@ infer e = case e of case t of VIdP a _ _ -> return $ a @@ phi _ -> throwError (show e ++ " is not a path") - Trans p t -> case p of - Path{} -> do - (a0,a1) <- checkPath p - check a0 t - return a1 - _ -> do - b <- infer p - case b of - VIdP (VPath _ VU) _ b1 -> return b1 - _ -> throwError $ "transport expects a path but got " ++ show p + Trans p t -> do + (a0,a1) <- checkPath (constPath VU) p + check a0 t + return a1 Comp a t0 ts -> do check VU a rho <- asks env @@ -263,7 +252,14 @@ infer e = case e of -- check rho alpha |- t_alpha : a alpha sequence $ Map.elems $ Map.mapWithKey (\alpha talpha -> - local (faceEnv alpha) (check (va `face` alpha) talpha)) ts + local (faceEnv alpha) $ do + rhoAlpha <- asks env + (a0,_) <- checkPath (constPath (va `face` alpha)) talpha + k <- asks index + unless (conv k a0 (eval rhoAlpha t0)) + (throwError ("incompatible system with " ++ show t0)) + ) ts + -- check that the system is compatible k <- asks index @@ -272,15 +268,22 @@ infer e = case e of return va _ -> throwError ("infer " ++ show e) - -- Check that a term is a path and output the source and target -checkPath :: Ter -> Typing (Val,Val) -checkPath (Path i a) = do +checkPath :: Val -> Ter -> Typing (Val,Val) +checkPath v (Path i a) = do rho <- asks env when (i `elem` support rho) (throwError $ show i ++ " is already declared") - local (addSub (i,Atom i)) $ check VU a + local (addSub (i,Atom i)) $ check (v @@ i) a return (eval (Sub rho (i,Dir 0)) a,eval (Sub rho (i,Dir 1)) a) +checkPath v t = do + vt <- infer t + k <- asks index + case vt of + VIdP a a0 a1 -> do + unless (conv k a v) (throwError "checkPath") + return (a0,a1) + _ -> throwError "checkPath" checks :: (Tele,Env) -> [Ter] -> Typing () checks _ [] = return () diff --git a/examples/nat.ctt b/examples/nat.ctt index 68f3dbc..ebd1af3 100644 --- a/examples/nat.ctt +++ b/examples/nat.ctt @@ -75,5 +75,26 @@ defEqJ (A : U) (a : A) (C : (x : A) -> Id A a x -> U) (d : C a (refl A a)) : test0 (A : U) (a b : A) (p : Id A a b) : Id A a a = refl A (p @ 0) test1 (A : U) (a b : A) (p : Id A a b) : Id A b b = refl A (p @ 1) +compEmpty (A : U) (a b : A) (p : Id A a b) : Id A a b = + comp A (p @ i) [ ] + compId (A : U) (a b c : A) (p : Id A a b) (q : Id A b c) : Id A a c = - comp A (p @ i) [ (i = 1) -> q ] \ No newline at end of file + comp A (p @ i) [ (i = 1) -> q ] + +kan (A : U) (a b c d : A) (p : Id A a b) (q : Id A a c) + (r : Id A b d) : Id A c d = + comp A (p @ i) [ (i = 0) -> q, (i = 1) -> r ] + +inv (A : U) (a b : A) (p : Id A a b) : Id A b a = p @ -i + +-- lemSimpl (A : U) (a b c : A) (p : Id A a b) (q q' : Id A b c) +-- (s : Id (Id A a c) (compId A a b c p q) (compId A a b c p q')) : Id (Id A b c) q q' = +-- comp A a [ (j = 0) -> ... ] + +-- evalPN (i:j:k:_) LemSimpl [v,a,b,c,p,q,q',s] = +-- Path j $ Path k $ comp Pos i v ss a +-- where ss = mkSystem [(j ~> 0,fill Pos k v (mkSystem [(i ~> 0,a),(i ~> 1,q @@ j)]) (p @@ i)), +-- (j ~> 1,fill Pos k v (mkSystem [(i ~> 0,a),(i ~> 1,(q' @@ j))]) (p @@ i)), +-- (k ~> 0,p @@ i), +-- (k ~> 1,(s @@ j) @@ i)] + -- 2.34.1