From f16c5998446198b03fdf235a6306cdc2360804b6 Mon Sep 17 00:00:00 2001 From: Simon Huber Date: Thu, 4 Jun 2015 10:35:41 +0200 Subject: [PATCH] Added neutral values for unglue --- CTT.hs | 67 ++++++++++++++++++++++++++++++--------------------------- Eval.hs | 36 +++++++++++++++++++------------ 2 files changed, 57 insertions(+), 46 deletions(-) diff --git a/CTT.hs b/CTT.hs index 9bcc3ae..a0e08ee 100644 --- a/CTT.hs +++ b/CTT.hs @@ -169,6 +169,8 @@ data Val = VU | VVar Ident Val | VFst Val | VSnd Val + | VUnGlueElem Val (System Val) + | VUnGlueElemU Val (System Val) | VSplit Val Val | VApp Val Val | VAppFormula Val Formula @@ -186,26 +188,25 @@ data Val = VU isNeutral :: Val -> Bool isNeutral v = case v of - Ter Undef{} _ -> True - Ter Hole{} _ -> True - VVar _ _ -> True - VFst v -> isNeutral v - VSnd v -> isNeutral v - VSplit _ v -> isNeutral v - VApp v _ -> isNeutral v - VAppFormula v _ -> isNeutral v - VComp a u ts -> isNeutralComp a u ts - -- VTrans a u -> isNeutralTrans a u - -- VCompElem _ _ u _ -> isNeutral u - -- VElimComp _ _ u -> isNeutral u - _ -> False - -isNeutralSystem :: System Val -> Bool -isNeutralSystem = any isNeutralPath . Map.elems - -isNeutralPath :: Val -> Bool -isNeutralPath (VPath _ v) = isNeutral v -isNeutralPath _ = True + Ter Undef{} _ -> True + Ter Hole{} _ -> True + VVar{} -> True + VComp{} -> True + VFst{} -> True + VSnd{} -> True + VSplit{} -> True + VApp{} -> True + VAppFormula{} -> True + VUnGlueElem{} -> True + VUnGlueElemU{} -> True + _ -> False + +-- isNeutralSystem :: System Val -> Bool +-- isNeutralSystem = any isNeutralPath . Map.elems + +-- isNeutralPath :: Val -> Bool +-- isNeutralPath (VPath _ v) = isNeutral v +-- isNeutralPath _ = True -- isNeutralTrans :: Val -> Val -> Bool -- isNeutralTrans (VPath i a) u = foo i a u @@ -219,18 +220,18 @@ isNeutralPath _ = True -- -- TODO: case for VGLueLine -- isNeutralTrans u _ = isNeutral u --- TODO: fix -isNeutralComp :: Val -> Val -> System Val -> Bool -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' _ _ _ _ = False -isNeutralComp _ u _ = isNeutral u +-- -- TODO: fix +-- isNeutralComp :: Val -> Val -> System Val -> Bool +-- 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' _ _ _ _ = False +-- isNeutralComp _ u _ = isNeutral u -- -- TODO: adapt for non-regular setting -- isNeutralComp :: Val -> Val -> System Val -> Bool @@ -456,6 +457,8 @@ showVal v = case v of VVar x _ -> text x VFst u -> showVal1 u <> text ".1" VSnd u -> showVal1 u <> text ".2" + VUnGlueElem v hs -> text "unGlueElem" <+> showVal1 v <+> text (showSystem hs) + VUnGlueElemU v es -> text "unGlueElemU" <+> showVal1 v <+> text (showSystem es) VIdP v0 v1 v2 -> text "IdP" <+> showVals [v0,v1,v2] VAppFormula v phi -> showVal v <+> char '@' <+> showFormula phi VComp v0 v1 vs -> text "comp" <+> showVals [v0,v1] <+> text (showSystem vs) diff --git a/Eval.hs b/Eval.hs index 1529d15..713e9aa 100644 --- a/Eval.hs +++ b/Eval.hs @@ -76,6 +76,8 @@ instance Nominal Val where VGlue a ts -> support (a,ts) VGlueElem a ts -> support (a,ts) VCompU a ts -> support (a,ts) + VUnGlueElem a hs -> support (a,hs) + VUnGlueElemU a es -> support (a,es) -- VGlueLine a phi psi -> support (a,phi,psi) -- VGlueLineElem a phi psi -> support (a,phi,psi) -- VCompElem a es u us -> support (a,es,u,us) @@ -110,6 +112,8 @@ instance Nominal Val where VSplit u v -> app (acti u) (acti v) VGlue a ts -> glue (acti a) (acti ts) VGlueElem a ts -> glueElem (acti a) (acti ts) + VUnGlueElem a hs -> unGlue (acti a) (acti hs) + VUnGlueElemU a es -> unGlueU (acti a) (acti es) VCompU a ts -> compUniv (acti a) (acti ts) -- VGlueLine a phi psi -> glueLine (acti a) (acti phi) (acti psi) -- VGlueLineElem a phi psi -> glueLineElem (acti a) (acti phi) (acti psi) @@ -141,6 +145,8 @@ instance Nominal Val where VSplit u v -> VSplit (sw u) (sw v) VGlue a ts -> VGlue (sw a) (sw ts) VGlueElem a ts -> VGlueElem (sw a) (sw ts) + VUnGlueElem a hs -> VUnGlueElem (sw a) (sw hs) + VUnGlueElemU a es -> VUnGlueElemU (sw a) (sw es) VCompU a ts -> VCompU (sw a) (sw ts) -- VGlueLine a phi psi -> VGlueLine (sw a) (sw phi) (sw psi) -- VGlueLineElem a phi psi -> VGlueLineElem (sw a) (sw phi) (sw psi) @@ -436,8 +442,6 @@ comp i a u ts = case a of VPi{} -> VComp (VPath i a) u (Map.map (VPath i) ts) VU -> compUniv u (Map.map (VPath i) ts) -- VGlue u (Map.map (eqToIso i) ts) - _ | isNeutral w -> w - where w = VComp (VPath i a) u (Map.map (VPath i) ts) VCompU 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 @@ -454,7 +458,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 + _ -> VComp (VPath i a) u (Map.map (VPath i) ts) + -- _ -> 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) @@ -512,15 +517,15 @@ glueElem v us | Map.null us = v | eps `Map.member` us = us ! eps | otherwise = VGlueElem v us -unGlue :: System Val -> Val -> Val -unGlue hisos w +unGlue :: Val -> System Val -> Val +unGlue w hisos | Map.null hisos = w | eps `Map.member` hisos = app (hisoFun (hisos ! eps)) w | otherwise = case w of VGlueElem v us -> v -- VElimComp _ _ v -> unGlue hisos v -- VCompElem a es v vs -> unGlue hisos v - _ -> error $ "unGlue: " ++ show w ++ " should be neutral!" + _ -> VUnGlueElem w hisos -- transGlue :: Name -> Val -> System Val -> Val -> Val -- transGlue i b hisos wi0 = glueElem vi1'' usi1 @@ -566,9 +571,9 @@ compGlue :: Name -> Val -> System Val -> Val -> System Val -> Val compGlue i b hisos wi0 ws = glueElem vi1'' usi1'' where bi1 = b `face` (i ~> 1) vs = mapWithKey - (\alpha wAlpha -> unGlue (hisos `face` alpha) wAlpha) ws + (\alpha wAlpha -> unGlue wAlpha (hisos `face` alpha)) ws vsi1 = vs `face` (i ~> 1) -- same as: border vi1 vs - vi0 = unGlue (hisos `face` (i ~> 0)) wi0 -- in b(i0) + vi0 = unGlue wi0 (hisos `face` (i ~> 0)) -- 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) @@ -765,13 +770,13 @@ gradLemma b hiso@(VPair a (VPair f (VPair g (VPair s t)))) us v = ------------------------------------------------------------------------------- -- | Composition in the Universe (to be replaced as glue) -unGlueU :: System Val -> Val -> Val -unGlueU es w +unGlueU :: Val -> System Val -> Val +unGlueU w es | 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!" + _ -> VUnGlueElemU w es compUniv :: Val -> System Val -> Val compUniv b es | Map.null es = b @@ -782,10 +787,9 @@ compUniv b es | Map.null es = b 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 + vs = mapWithKey (\alpha wAlpha -> unGlueU wAlpha (es `face` alpha)) ws vsi1 = vs `face` (i ~> 1) -- same as: border vi1 vs - vi0 = unGlueU (es `face` (i ~> 0)) wi0 -- in b(i0) + vi0 = unGlueU wi0 (es `face` (i ~> 0)) -- 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) @@ -1061,6 +1065,8 @@ instance Convertible Val where (VComp a u ts,VComp a' u' ts') -> conv ns (a,u,ts) (a',u',ts') (VGlue v hisos,VGlue v' hisos') -> conv ns (v,hisos) (v',hisos') (VGlueElem u us,VGlueElem u' us') -> conv ns (u,us) (u',us') + (VUnGlueElem _ u,VUnGlueElem _ u') -> conv ns u u' + (VUnGlueElemU _ u,VUnGlueElemU _ u') -> conv ns u u' -- (VCompElem a es u us,VCompElem a' es' u' us') -> -- conv ns (a,es,u,us) (a',es',u',us') -- (VElimComp a es u,VElimComp a' es' u') -> conv ns (a,es,u) (a',es',u') @@ -1119,6 +1125,8 @@ instance Normal Val where -- VTrans u v -> transLine (normal ns u) (normal ns v) VGlue u hisos -> glue (normal ns u) (normal ns hisos) VGlueElem u us -> glueElem (normal ns u) (normal ns us) + VUnGlueElem u hs -> unGlue (normal ns u) (normal ns hs) + VUnGlueElemU u es -> unGlueU (normal ns u) (normal ns es) VCompU u es -> compUniv (normal ns u) (normal ns es) -- VCompElem a es u us -> compElem (normal ns a) (normal ns es) (normal ns u) (normal ns us) -- VElimComp a es u -> elimComp (normal ns a) (normal ns es) (normal ns u) -- 2.34.1