From: Simon Huber Date: Wed, 3 Jun 2015 14:04:57 +0000 (+0200) Subject: Finished first version X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=0034fb8d4674b2795d5850be0046c4c3403b6216;p=cubicaltt.git Finished first version --- diff --git a/Eval.hs b/Eval.hs index eda61ac..5f1078d 100644 --- a/Eval.hs +++ b/Eval.hs @@ -431,12 +431,11 @@ comp i a u ts = case a of ui1 = comp i a u1 t1s comp_u2 = comp i (app f fill_u1) u2 t2s VPi{} -> VComp (VPath i a) u (Map.map (VPath i) ts) - VU -> undefined - -- VComp VU u (Map.map (VPath i) ts) + VU -> VComp VU u (Map.map (VPath i) ts) -- VGlue u (Map.map (eqToIso i) ts) _ | isNeutral w -> w where w = VComp a u (Map.map (VPath i) ts) - -- VComp VU a es -> compU i a es u ts + VComp VU a es -> compU i a es u ts VGlue b hisos -> compGlue i b hisos u ts -- VGlueLine b phi psi -> compGlueLine i b phi psi u ts Ter (Sum _ _ nass) env -> case u of @@ -519,45 +518,45 @@ unGlue hisos w -- VCompElem a es v vs -> unGlue hisos v _ -> error $ "unGlue: " ++ show w ++ " should be neutral!" -transGlue :: Name -> Val -> System Val -> Val -> Val -transGlue i b hisos wi0 = glueElem vi1'' usi1 - where vi0 = unGlue (hisos `face` (i ~> 0)) wi0 -- in b(i0) +-- transGlue :: Name -> Val -> System Val -> Val -> Val +-- transGlue i b hisos wi0 = glueElem vi1'' usi1 +-- where vi0 = unGlue (hisos `face` (i ~> 0)) wi0 -- in b(i0) - vi1 = trans i b vi0 -- in b(i1) +-- vi1 = trans i b vi0 -- in b(i1) - hisosI1 = hisos `face` (i ~> 1) - hisos'' = - filterWithKey (\alpha _ -> alpha `Map.notMember` hisos) hisosI1 - - -- set of elements in hisos independent of i - hisos' = filterWithKey (\alpha _ -> i `Map.notMember` alpha) hisos - - us' = mapWithKey (\gamma isoG -> - transFill i (hisoDom isoG) (wi0 `face` gamma)) - hisos' - usi1' = mapWithKey (\gamma isoG -> - trans i (hisoDom isoG) (wi0 `face` gamma)) - hisos' +-- hisosI1 = hisos `face` (i ~> 1) +-- hisos'' = +-- filterWithKey (\alpha _ -> alpha `Map.notMember` hisos) hisosI1 - ls' = mapWithKey (\gamma isoG -> - VPath i $ squeeze i (b `face` gamma) - (hisoFun isoG `app` (us' ! gamma))) - hisos' - bi1 = b `face` (i ~> 1) - vi1' = compLine bi1 vi1 ls' - - uls'' = mapWithKey (\gamma isoG -> - gradLemma (bi1 `face` gamma) isoG (usi1' `face` gamma) - (vi1' `face` gamma)) - hisos'' - - vi1'' = compLine bi1 vi1' (Map.map snd uls'') - - usi1 = mapWithKey (\gamma _ -> - if gamma `Map.member` usi1' - then usi1' ! gamma - else fst (uls'' ! gamma)) - hisosI1 +-- -- set of elements in hisos independent of i +-- hisos' = filterWithKey (\alpha _ -> i `Map.notMember` alpha) hisos + +-- us' = mapWithKey (\gamma isoG -> +-- transFill i (hisoDom isoG) (wi0 `face` gamma)) +-- hisos' +-- usi1' = mapWithKey (\gamma isoG -> +-- trans i (hisoDom isoG) (wi0 `face` gamma)) +-- hisos' + +-- ls' = mapWithKey (\gamma isoG -> +-- VPath i $ squeeze i (b `face` gamma) +-- (hisoFun isoG `app` (us' ! gamma))) +-- hisos' +-- bi1 = b `face` (i ~> 1) +-- vi1' = compLine bi1 vi1 ls' + +-- uls'' = mapWithKey (\gamma isoG -> +-- gradLemma (bi1 `face` gamma) isoG (usi1' `face` gamma) +-- (vi1' `face` gamma)) +-- hisos'' + +-- vi1'' = compLine bi1 vi1' (Map.map snd uls'') + +-- usi1 = mapWithKey (\gamma _ -> +-- if gamma `Map.member` usi1' +-- then usi1' ! gamma +-- else fst (uls'' ! gamma)) +-- hisosI1 compGlue :: Name -> Val -> System Val -> Val -> System Val -> Val compGlue i b hisos wi0 ws = glueElem vi1'' usi1'' @@ -761,6 +760,103 @@ gradLemma b hiso@(VPair a (VPair f (VPair g (VPair s t)))) us v = ------------------------------------------------------------------------------- -- | Composition in the Universe + +unGlueU :: System Val -> Val -> Val +unGlueU es w + | Map.null es = w + | eps `Map.member` es = transNegLine (es ! eps) w + | otherwise = case w of + VGlueElem v us -> v + _ -> error $ "unGlueU: " ++ show w ++ " should be neutral!" + +compU :: Name -> Val -> System Val -> Val -> System Val -> Val +compU i b es wi0 ws = glueElem vi1'' usi1'' + where bi1 = b `face` (i ~> 1) + vs = mapWithKey + (\alpha wAlpha -> unGlueU (es `face` alpha) wAlpha) ws + vsi1 = vs `face` (i ~> 1) -- same as: border vi1 vs + vi0 = unGlueU (es `face` (i ~> 0)) wi0 -- in b(i0) + + v = fill i b vi0 vs -- in b + vi1 = comp i b vi0 vs -- is v `face` (i ~> 1) in b(i1) + + esI1 = es `face` (i ~> 1) + es' = filterWithKey (\alpha _ -> i `Map.notMember` alpha) es + -- es'' = filterWithKey (\alpha _ -> not (alpha `Map.member` es)) esI1 + es'' = filterWithKey (\alpha _ -> not (alpha `Map.member` es')) esI1 + + us' = mapWithKey (\gamma eGamma -> + fill i (eGamma @@ One) (wi0 `face` gamma) (ws `face` gamma)) + es' + usi1' = mapWithKey (\gamma eGamma -> + comp i (eGamma @@ One) (wi0 `face` gamma) (ws `face` gamma)) + es' + + ls' = mapWithKey (\gamma eGamma -> + pathComp i (b `face` gamma) (v `face` gamma) + (transNegLine eGamma (us' ! gamma)) (vs `face` gamma)) + es' + + vi1' = compLine (constPath bi1) vi1 (ls' `unionSystem` vsi1) + + wsi1 = ws `face` (i ~> 1) + + -- for gamma in es'', (i1) gamma is in es, so wsi1 gamma + -- is in the domain of isoGamma + uls'' = mapWithKey (\gamma eGamma -> + gradLemmaU (bi1 `face` gamma) eGamma + ((usi1' `face` gamma) `unionSystem` (wsi1 `face` gamma)) + (vi1' `face` gamma)) + es'' + + vsi1' = border vi1' es' + + vi1'' = compLine (constPath bi1) vi1' + (Map.map snd uls'' `unionSystem` vsi1' `unionSystem` vsi1) + + usi1'' = Map.mapWithKey (\gamma _ -> + if gamma `Map.member` usi1' then usi1' ! gamma + else fst (uls'' ! gamma)) + esI1 + + + +-- Grad Lemma, takes a line eq in U, a system us and a value v, s.t. f us = +-- border v. Outputs (u,p) s.t. border u = us and a path p between v +-- and f u, where f is transNegLine eq +gradLemmaU :: Val -> Val -> System Val -> Val -> (Val, Val) +gradLemmaU b eq us v = (u, VPath i theta'') + where i:j:_ = freshs (eq,us,v) + a = eq @@ One + g = transLine + f = transNegLine + s e b = VPath j $ compNeg j (e @@ j) (trans j (e @@ j) b) + (mkSystem [(j ~> 0, transFill j (e @@ j) b) + ,(j ~> 1, transFillNeg j (e @@ j) + (trans j (e @@ j) b))]) + t e a = VPath j $ comp j (e @@ j) (transNeg j (e @@ j) a) + (mkSystem [(j ~> 0, transFill j (e @@ j) + (transNeg j (e @@ j) a)) + ,(j ~> 1, transFillNeg j (e @@ j) a)]) + gv = g eq v + us' = mapWithKey (\alpha uAlpha -> + t (eq `face` alpha) uAlpha @@ i) us + theta = fill i a gv us' + u = comp i a gv us' -- Same as "theta `face` (i ~> 1)" + ws = insertSystem (i ~> 0) gv $ + insertSystem (i ~> 1) (t eq u @@ j) $ + mapWithKey + (\alpha uAlpha -> + t (eq `face` alpha) uAlpha @@ (Atom i :/\: Atom j)) us + theta' = compNeg j a theta ws + xs = insertSystem (i ~> 0) (s eq v @@ j) $ + insertSystem (i ~> 1) (s eq (f eq u) @@ j) $ + mapWithKey + (\alpha uAlpha -> + s (eq `face` alpha) (f (eq `face` alpha) uAlpha) @@ j) us + theta'' = comp j b (f eq theta') xs + + -- isConstPath :: Val -> Bool -- isConstPath (VPath i u) = i `notElem` support u -- isConstPath _ = False diff --git a/Exp.cf b/Exp.cf index 8958783..0b5e55b 100644 --- a/Exp.cf +++ b/Exp.cf @@ -34,11 +34,11 @@ IdP. Exp3 ::= "IdP" Exp4 Exp4 Exp4 ; Trans. Exp3 ::= "transport" Exp4 Exp4 ; Comp. Exp3 ::= "comp" Exp4 Exp4 System ; Glue. Exp3 ::= "glue" Exp4 System ; -GlueElem. Exp3 ::= "glueElem" Exp4 System ; -CompElem. Exp3 ::= "compElem" Exp4 System Exp4 System ; -GlueLine. Exp3 ::= "glueLine" Formula Formula Exp4 ; -GlueLineElem. Exp3 ::= "glueLineElem" Formula Formula Exp4 ; -ElimComp. Exp3 ::= "elimComp" Exp4 System Exp4 ; +-- GlueElem. Exp3 ::= "glueElem" Exp4 System ; +-- CompElem. Exp3 ::= "compElem" Exp4 System Exp4 System ; +-- GlueLine. Exp3 ::= "glueLine" Formula Formula Exp4 ; +-- GlueLineElem. Exp3 ::= "glueLineElem" Formula Formula Exp4 ; +-- ElimComp. Exp3 ::= "elimComp" Exp4 System Exp4 ; Fst. Exp4 ::= Exp4 ".1" ; Snd. Exp4 ::= Exp4 ".2" ; Pair. Exp5 ::= "(" Exp "," [Exp] ")" ; diff --git a/Resolver.hs b/Resolver.hs index a3248e6..56758ac 100644 --- a/Resolver.hs +++ b/Resolver.hs @@ -202,9 +202,10 @@ resolveExp e = case e of CTT.PCon (unAIdent n) <$> resolveExp a <*> mapM resolveExp xs <*> mapM resolveFormula phis _ -> CTT.AppFormula <$> resolveExp t <*> resolveFormula phi - Trans x y -> CTT.Trans <$> resolveExp x <*> resolveExp y + Trans x y -> CTT.Comp <$> resolveExp x <*> resolveExp y <*> pure Map.empty IdP x y z -> CTT.IdP <$> resolveExp x <*> resolveExp y <*> resolveExp z - Comp u v ts -> CTT.Comp <$> resolveExp u <*> resolveExp v <*> resolveSystem ts + Comp u v ts -> CTT.Comp <$> (CTT.Path (C.Name "_") <$> resolveExp u) + <*> resolveExp v <*> resolveSystem ts Glue u ts -> do rs <- resolveSystem ts let isIso (CTT.Pair _ (CTT.Pair _ (CTT.Pair _ (CTT.Pair _ _)))) = True @@ -212,15 +213,15 @@ resolveExp e = case e of unless (all isIso $ Map.elems rs) (throwError $ "Not a system of isomorphisms: " ++ show rs) CTT.Glue <$> resolveExp u <*> pure rs - GlueElem u ts -> CTT.GlueElem <$> resolveExp u <*> resolveSystem ts - GlueLine phi psi u -> - CTT.GlueLine <$> resolveExp u <*> resolveFormula phi <*> resolveFormula psi - GlueLineElem phi psi u -> - CTT.GlueLineElem <$> resolveExp u <*> resolveFormula phi - <*> resolveFormula psi - CompElem a es t ts -> CTT.CompElem <$> resolveExp a <*> resolveSystem es - <*> resolveExp t <*> resolveSystem ts - ElimComp a es t -> CTT.ElimComp <$> resolveExp a <*> resolveSystem es <*> resolveExp t + -- GlueElem u ts -> CTT.GlueElem <$> resolveExp u <*> resolveSystem ts + -- GlueLine phi psi u -> + -- CTT.GlueLine <$> resolveExp u <*> resolveFormula phi <*> resolveFormula psi + -- GlueLineElem phi psi u -> + -- CTT.GlueLineElem <$> resolveExp u <*> resolveFormula phi + -- <*> resolveFormula psi + -- CompElem a es t ts -> CTT.CompElem <$> resolveExp a <*> resolveSystem es + -- <*> resolveExp t <*> resolveSystem ts + -- ElimComp a es t -> CTT.ElimComp <$> resolveExp a <*> resolveSystem es <*> resolveExp t _ -> do modName <- asks envModule throwError ("Could not resolve " ++ show e ++ " in module " ++ modName) diff --git a/TypeChecker.hs b/TypeChecker.hs index d70220a..4eb75e4 100644 --- a/TypeChecker.hs +++ b/TypeChecker.hs @@ -200,18 +200,18 @@ check a t = case (a,t) of check VU a rho <- asks env checkGlue (eval rho a) ts - (VGlue va ts,GlueElem u us) -> do - check va u - vu <- evalTyping u - checkGlueElem vu ts us - (VU,GlueLine b phi psi) -> do - check VU b - checkFormula phi - checkFormula psi - (VGlueLine vb phi psi,GlueLineElem r phi' psi') -> do - check vb r - unlessM ((phi,psi) === (phi',psi')) $ - throwError "GlueLineElem: formulas don't match" + -- (VGlue va ts,GlueElem u us) -> do + -- check va u + -- vu <- evalTyping u + -- checkGlueElem vu ts us + -- (VU,GlueLine b phi psi) -> do + -- check VU b + -- checkFormula phi + -- checkFormula psi + -- (VGlueLine vb phi psi,GlueLineElem r phi' psi') -> do + -- check vb r + -- unlessM ((phi,psi) === (phi',psi')) $ + -- throwError "GlueLineElem: formulas don't match" _ -> do v <- infer t unlessM (v === a) $ @@ -355,7 +355,7 @@ checkPathSystem t0 va ps = do v <- T.sequence $ mapWithKey (\alpha pAlpha -> local (faceEnv alpha) $ do rhoAlpha <- asks env - (a0,a1) <- checkPath (constPath (va `face` alpha)) pAlpha + (a0,a1) <- checkPath (va `face` alpha) pAlpha unlessM (a0 === eval rhoAlpha t0) $ throwError $ "Incompatible system with " ++ show t0 return a1) ps @@ -404,41 +404,41 @@ infer e = case e of case t of VIdP a _ _ -> return $ a @@ phi _ -> throwError (show e ++ " is not a path") - Trans p t -> do - (a0,a1) <- checkPath (constPath VU) p - check a0 t - return a1 + -- Trans p t -> do + -- (a0,a1) <- checkPath (constPath VU) p + -- check a0 t + -- return a1 Comp a t0 ps -> do - check VU a + checkPath (constPath VU) a va <- evalTyping a - check va t0 + check (va @@ Zero) t0 checkPathSystem t0 va ps - return va - CompElem a es u us -> do - check VU a - rho <- asks env - let va = eval rho a - ts <- checkPathSystem a VU es - let ves = evalSystem rho es - unless (keys es == keys us) - (throwError ("Keys don't match in " ++ show es ++ " and " ++ show us)) - check va u - let vu = eval rho u - checkSystemsWith ts us (const check) - let vus = evalSystem rho us - checkCompSystem vus - checkSystemsWith ves vus (\alpha eA vuA -> - unlessM (transNegLine eA vuA === (vu `face` alpha)) $ - throwError $ "Malformed compElem: " ++ show us) - return $ compLine VU va ves - ElimComp a es u -> do - check VU a - rho <- asks env - let va = eval rho a - checkPathSystem a VU es - let ves = evalSystem rho es - check (compLine VU va ves) u - return va + return (va @@ One) + -- CompElem a es u us -> do + -- check VU a + -- rho <- asks env + -- let va = eval rho a + -- ts <- checkPathSystem a VU es + -- let ves = evalSystem rho es + -- unless (keys es == keys us) + -- (throwError ("Keys don't match in " ++ show es ++ " and " ++ show us)) + -- check va u + -- let vu = eval rho u + -- checkSystemsWith ts us (const check) + -- let vus = evalSystem rho us + -- checkCompSystem vus + -- checkSystemsWith ves vus (\alpha eA vuA -> + -- unlessM (transNegLine eA vuA === (vu `face` alpha)) $ + -- throwError $ "Malformed compElem: " ++ show us) + -- return $ compLine VU va ves + -- ElimComp a es u -> do + -- check VU a + -- rho <- asks env + -- let va = eval rho a + -- checkPathSystem a VU es + -- let ves = evalSystem rho es + -- check (compLine VU va ves) u + -- return va PCon c a es phis -> do check VU a va <- evalTyping a