From 6caaebab03b6f774ac0fcb5fc2930931c6bfc209 Mon Sep 17 00:00:00 2001 From: Simon Huber Date: Thu, 17 Sep 2015 16:05:33 +0200 Subject: [PATCH] Removed unGlue --- CTT.hs | 4 ---- Eval.hs | 21 +++++++++++---------- 2 files changed, 11 insertions(+), 14 deletions(-) diff --git a/CTT.hs b/CTT.hs index 9bccf6c..c122be1 100644 --- a/CTT.hs +++ b/CTT.hs @@ -153,7 +153,6 @@ data Val = VU | VVar Ident Val | VFst Val | VSnd Val - | VUnGlueElem Val Val (System Val) | VSplit Val Val | VApp Val Val | VAppFormula Val Formula @@ -171,7 +170,6 @@ isNeutral v = case v of VSplit{} -> True VApp{} -> True VAppFormula{} -> True - VUnGlueElem{} -> True _ -> False isNeutralSystem :: System Val -> Bool @@ -383,8 +381,6 @@ showVal v = case v of VVar x _ -> text x VFst u -> showVal1 u <> text ".1" VSnd u -> showVal1 u <> text ".2" - VUnGlueElem v b hs -> text "unGlueElem" <+> showVals [v,b] - <+> text (showSystem hs) VIdP v0 v1 v2 -> text "IdP" <+> showVals [v0,v1,v2] VAppFormula v phi -> showVal v <+> char '@' <+> showFormula phi VComp v0 v1 vs -> diff --git a/Eval.hs b/Eval.hs index 7daadbc..0ef2366 100644 --- a/Eval.hs +++ b/Eval.hs @@ -71,7 +71,6 @@ instance Nominal Val where VSplit u v -> support (u,v) VGlue a ts -> support (a,ts) VGlueElem a ts -> support (a,ts) - VUnGlueElem a b hs -> support (a,b,hs) act u (i, phi) | i `notElem` support u = u | otherwise = @@ -102,7 +101,6 @@ 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 b hs -> unGlue (acti a) (acti b) (acti hs) -- This increases efficiency as it won't trigger computation. swap u ij@(i,j) = @@ -129,7 +127,6 @@ 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 b hs -> VUnGlueElem (sw a) (sw b) (sw hs) ----------------------------------------------------------------------- @@ -249,7 +246,6 @@ inferType v = case v of ty -> error $ "inferType: expected IdP type for " ++ show v ++ ", got " ++ show ty VComp a _ _ -> a @@ One - VUnGlueElem _ b _ -> b _ -> error $ "inferType: not neutral " ++ show v (@@) :: ToFormula a => Val -> a -> Val @@ -279,7 +275,7 @@ comp i a u ts = case a of comp_u2 = comp i (app f fill_u1) u2 t2s VPi{} -> VComp (VPath i a) u (Map.map (VPath i) ts) VU -> glue u (Map.map (eqToIso . VPath i) ts) - VGlue b isos -> compGlue i b isos u ts + VGlue b isos | not (isNeutralGlue i isos u ts) -> compGlue i b isos u ts Ter (Sum _ _ nass) env -> case u of VCon n us | all isCon (elems ts) -> case lookupLabel n nass of Just as -> let tsus = transposeSystemAndList (Map.map unCon ts) us @@ -462,7 +458,7 @@ isoSec = fstVal . sndVal . sndVal . sndVal isoRet :: Val -> Val isoRet = sndVal . sndVal . sndVal . sndVal - + -- -- Every path in the universe induces an iso eqToIso :: Val -> Val eqToIso e = VPair e1 (VPair f (VPair g (VPair s t))) @@ -502,8 +498,15 @@ unGlue :: Val -> Val -> System Val -> Val unGlue w b isos | eps `member` isos = app (isoFun (isos ! eps)) w | otherwise = case w of VGlueElem v us -> v - _ -> VUnGlueElem w b isos - + _ -> error ("unGlue: neutral" ++ show w) + +isNeutralGlue :: Name -> System Val -> Val -> System Val -> Bool +isNeutralGlue i isos u0 ts = (eps `notMember` isosi0 && isNeutral u0) || + any (\(alpha,talpha) -> + eps `notMember` (isos `face` alpha) && isNeutral talpha) + (assocs ts) + where isosi0 = isos `face` (i ~> 0) + compGlue :: Name -> Val -> System Val -> Val -> System Val -> Val compGlue i b isos wi0 ws = glueElem vi1'' usi1'' where bi1 = b `face` (i ~> 1) @@ -645,7 +648,6 @@ instance Convertible Val where (VHComp a u ts,VHComp a' u' ts') -> conv ns (a,u,ts) (a',u',ts') (VGlue v isos,VGlue v' isos') -> conv ns (v,isos) (v',isos') (VGlueElem u us,VGlueElem u' us') -> conv ns (u,us) (u',us') - (VUnGlueElem u _ _,VUnGlueElem u' _ _) -> conv ns u u' _ -> False instance Convertible Ctxt where @@ -702,7 +704,6 @@ instance Normal Val where VHComp u v vs -> hComp (normal ns u) (normal ns v) (normal ns vs) VGlue u isos -> glue (normal ns u) (normal ns isos) VGlueElem u us -> glueElem (normal ns u) (normal ns us) - VUnGlueElem u b hs -> unGlue (normal ns u) (normal ns b) (normal ns hs) VVar x t -> VVar x t -- (normal ns t) VFst t -> fstVal (normal ns t) VSnd t -> sndVal (normal ns t) -- 2.34.1