From: Simon Huber Date: Thu, 3 Mar 2016 16:31:39 +0000 (+0100) Subject: Fix squeezeHIT for non-recursive HITs X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=1400bae1262d8488f696a4bfc95b1292d01b8311;p=cubicaltt.git Fix squeezeHIT for non-recursive HITs --- diff --git a/Eval.hs b/Eval.hs index 69deb63..15d268f 100644 --- a/Eval.hs +++ b/Eval.hs @@ -435,7 +435,6 @@ transpHIT i a@(Ter (HSum _ _ nass) env) u = squeezeHIT :: Name -> Val -> Val -> Val squeezeHIT i a@(Ter (HSum _ _ nass) env) u = let j = fresh (a,u) - aij = swap a (i,j) in case u of VCon n us -> case lookupLabel n nass of @@ -444,10 +443,14 @@ squeezeHIT i a@(Ter (HSum _ _ nass) env) u = VPCon c _ ws0 phis -> case lookupLabel c nass of Just as -> pcon c (a `face` (i ~> 1)) (squeezes i as env ws0) phis Nothing -> error $ "squeezeHIT: missing path constructor " ++ c - VHComp _ v vs -> - hComp (a `face` (i ~> 1)) (squeezeHIT i a v) $ - mapWithKey (\alpha vAlpha -> - VPath j $ squeezeHIT j (aij `face` alpha) (vAlpha @@ j)) vs + VHComp _ v vs -> hComp (a `face` (i ~> 1)) (squeezeHIT i a v) $ + mapWithKey + (\alpha vAlpha -> case Map.lookup i alpha of + Nothing -> VPath j $ squeezeHIT i (a `face` alpha) (vAlpha @@ j) + Just Zero -> VPath j $ transpHIT i + (a `face` (Map.delete i alpha)) (vAlpha @@ j) + Just One -> vAlpha) + vs _ -> error $ "squeezeHIT: neutral " ++ show u hComp :: Val -> Val -> System Val -> Val