From c98ad6506c0a18c7d2ab3f40a5dc1778db4f9cf9 Mon Sep 17 00:00:00 2001 From: Anders Date: Wed, 3 Jun 2015 17:16:08 +0200 Subject: [PATCH] isNeutralComp, small fixes to comp and comment things in bool --- CTT.hs | 32 +++++++++++++++++++++++--------- Eval.hs | 9 +++++---- examples/bool.ctt | 16 ++++++++-------- 3 files changed, 36 insertions(+), 21 deletions(-) diff --git a/CTT.hs b/CTT.hs index 6932cc6..717f5be 100644 --- a/CTT.hs +++ b/CTT.hs @@ -216,15 +216,29 @@ isNeutralPath _ = True -- -- TODO: case for VGLueLine -- isNeutralTrans u _ = isNeutral u --- TODO: adapt for non-regular setting isNeutralComp :: Val -> Val -> System Val -> Bool -isNeutralComp a _ _ | isNeutral a = True -isNeutralComp (Ter Sum{} _) u ts = isNeutral u || isNeutralSystem ts -isNeutralComp (VGlue _ as) u ts = - isNeutral u || isNeutralSystem (filterWithKey testFace ts) - where shas = shape as - testFace beta _ = let shasBeta = shas `face` beta - in not (Map.null shasBeta || eps `Map.member` shasBeta) +isNeutralComp (VPath i a) u ts = isNeutralComp' i a u ts + where isNeutralComp' i a u ts | isNeutral a = True + isNeutralComp' i (Ter Sum{} _) u ts = isNeutral u || isNeutralSystem ts + isNeutralComp' i (VGlue _ as) u ts = + isNeutral u && isNeutralSystem (filterWithKey testFace ts) + where shas = shape as `face` (i ~> 0) + testFace beta _ = let shasBeta = shas `face` beta + in shasBeta /= Map.empty && eps `Map.member` shasBeta +-- isNeutralComp' _ _ _ _ = isNeutral u +isNeutralComp _ u _ = isNeutral u + +-- -- TODO: adapt for non-regular setting +-- isNeutralComp :: Val -> Val -> System Val -> Bool +-- isNeutralComp a _ _ | isNeutral a = True +-- isNeutralComp (Ter Sum{} _) u ts = isNeutral u || isNeutralSystem ts +-- isNeutralComp (VGlue _ as) u ts = +-- isNeutral u || isNeutralSystem (filterWithKey testFace ts) +-- where shas = shape as +-- testFace beta _ = let shasBeta = shas `face` beta +-- in not (Map.null shasBeta || eps `Map.member` shasBeta) + + -- TODO -- isNeutralComp (VGlueLine _ phi psi) u ts = -- isNeutral u || isNeutralSystem (filterWithKey (not . test) ts) || and (elems ws) @@ -235,7 +249,7 @@ isNeutralComp (VGlue _ as) u ts = -- (\alpha -> let phiAlpha0 = invFormula (phi `face` alpha) Zero -- in isNeutral (u `face` alpha) || isNeutralSystem ) -- fs -isNeutralComp _ _ _ = False +-- isNeutralComp _ _ _ = False mkVar :: Int -> String -> Val -> Val diff --git a/Eval.hs b/Eval.hs index 5f1078d..23777ac 100644 --- a/Eval.hs +++ b/Eval.hs @@ -431,11 +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 -> VComp VU u (Map.map (VPath i) ts) + VU -> VComp (VPath i 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 + where w = VComp (VPath i a) u (Map.map (VPath i) ts) + VComp (VPath _ 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 @@ -451,7 +451,8 @@ comp i a u ts = case a of -- VCompElem _ _ u1 _ -> comp i a u1 ts -- VElimComp _ _ u1 -> comp i a u1 ts _ -> error $ "comp ter sum" ++ show u - + _ -> error $ "comp: case missing for " ++ show i ++ " " ++ show a ++ " " ++ show u ++ " " ++ showSystem ts + compNeg :: Name -> Val -> Val -> System Val -> Val compNeg i a u ts = comp i (a `sym` i) u (ts `sym` i) diff --git a/examples/bool.ctt b/examples/bool.ctt index f94af65..b88db12 100644 --- a/examples/bool.ctt +++ b/examples/bool.ctt @@ -40,11 +40,11 @@ boolEqF2 : Id U bool F2 = negF2 : F2 -> F2 = subst U (\(X : U) -> (X -> X)) bool F2 boolEqF2 negBool -lemTest (A : U) : (B : U) (p : Id U A B) (a : A) -> IdP p a (transport p a) = - J U A (\(B : U) (p : Id U A B) -> (a : A) -> IdP p a (transport p a)) (refl A) +-- lemTest (A : U) : (B : U) (p : Id U A B) (a : A) -> IdP p a (transport p a) = +-- J U A (\(B : U) (p : Id U A B) -> (a : A) -> IdP p a (transport p a)) (refl A) -test : IdP boolEqF2 true oneF2 = glueElem oneF2 [ (i = 0) -> true ] -test1 : IdP boolEqF2 true oneF2 = lemTest bool F2 boolEqF2 true +-- test : IdP boolEqF2 true oneF2 = glueElem oneF2 [ (i = 0) -> true ] +-- test1 : IdP boolEqF2 true oneF2 = lemTest bool F2 boolEqF2 true F2EqBool : Id U F2 bool = inv U bool F2 boolEqF2 @@ -71,8 +71,8 @@ squareBoolF2 : Square U bool bool (refl U bool) bool F2 test5 : IdP boolEqF2 true oneF2 = transport ( boolEqF2 @ i /\ j) true -test6 : Id bool true true = - transport ( F2EqBool @ i \/ j) (test5 @ - i) +-- test6 : Id bool true true = +-- transport ( F2EqBool @ i \/ j) (test5 @ - i) test7 : Id U F2 F2 = subst U (\(X:U) -> Id U X X) bool F2 boolEqF2 negNegEq @@ -83,5 +83,5 @@ test8 : Id U F2 F2 = test9 : Id U F2 F2 = transport ( Id U (boolEqF2 @ i) (boolEqF2 @ i)) (refl U bool) -p : Id U F2 bool = comp U bool [ (i = 0) -> boolEqF2 ] -q : Id U F2 F2 = p @ (i /\ - i) \ No newline at end of file +-- p : Id U F2 bool = comp U bool [ (i = 0) -> boolEqF2 ] +-- q : Id U F2 F2 = p @ (i /\ - i) \ No newline at end of file -- 2.34.1