isNeutralComp, small fixes to comp and comment things in bool

diff --git a/CTT.hs b/CTT.hs
index 6932cc69cde99e026028aa5366dcc71060d1ab28..717f5be165feaf675844dd32de5c0e1892557189 100644 (file)
--- 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 5f1078d865a16f6ffa9d78f8444b08f72c9f137b..23777ac1810cdf0905f2a12851d1a108d9f52e61 100644 (file)
--- 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 f94af65514c3905122ec0965b99f6f56a46e2d3e..b88db124d0d47b74279e82e6dc90e11b26cfc6e8 100644 (file)
--- 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 = <i> glueElem oneF2 [ (i = 0) -> true ]
-test1 : IdP boolEqF2 true oneF2 = lemTest bool F2 boolEqF2 true
+-- test : IdP boolEqF2 true oneF2 = <i> 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 = 
   <i> transport (<j> boolEqF2 @ i /\ j) true
 
-test6 : Id bool true true =
-  <i> transport (<j> F2EqBool @ i \/ j) (test5 @ - i)
+-- test6 : Id bool true true =
+--   <i> transport (<j> 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 (<i> Id U (boolEqF2 @ i) (boolEqF2 @ i)) (refl U bool)
 
-p : Id U F2 bool = <i> comp U bool [ (i = 0) -> boolEqF2 ]
-q : Id U F2 F2 = <i> p @ (i /\ - i)
\ No newline at end of file
+-- p : Id U F2 bool = <i> comp U bool [ (i = 0) -> boolEqF2 ]
+-- q : Id U F2 F2 = <i> p @ (i /\ - i)
\ No newline at end of file