From: Anders Mörtberg Date: Thu, 7 Jan 2016 17:05:22 +0000 (+0100) Subject: remove @@@ X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=8841deac856ea64d2d17760aff81a51a1275abdc;p=cubicaltt.git remove @@@ --- diff --git a/Eval.hs b/Eval.hs index 8605ba9..e181d9f 100644 --- a/Eval.hs +++ b/Eval.hs @@ -204,7 +204,7 @@ app u v = case (u,v) of _ -> error $ "app: missing case in split for " ++ c (Ter (Split _ _ ty hbr) e,VHComp a w ws) -> case eval e ty of VPi _ f -> let j = fresh (e,v) - wsj = Map.map (@@@ j) ws + wsj = Map.map (@@ j) ws w' = app u w ws' = mapWithKey (\alpha -> app (u `face` alpha)) wsj -- a should be constant @@ -214,7 +214,7 @@ app u v = case (u,v) of (VComp (VPath i (VPi a f)) li0 ts,vi1) -> let j = fresh (u,vi1) (aj,fj) = (a,f) `swap` (i,j) - tsj = Map.map (@@@ j) ts + tsj = Map.map (@@ j) ts v = transFillNeg j aj vi1 vi0 = transNeg j aj vi1 in comp j (app fj v) (app li0 vi0) @@ -282,8 +282,8 @@ comp :: Name -> Val -> Val -> System Val -> Val comp i a u ts | eps `member` ts = (ts ! eps) `face` (i ~> 1) comp i a u ts = case a of VIdP p v0 v1 -> let j = fresh (Atom i,a,u,ts) - in VPath j $ comp i (p @@@ j) (u @@@ j) $ - insertsSystem [(j ~> 0,v0),(j ~> 1,v1)] (Map.map (@@@ j) ts) + in VPath j $ comp i (p @@ j) (u @@ j) $ + insertsSystem [(j ~> 0,v0),(j ~> 1,v1)] (Map.map (@@ j) ts) VSigma a f -> VPair ui1 comp_u2 where (t1s, t2s) = (Map.map fstVal ts, Map.map sndVal ts) (u1, u2) = (fstVal u, sndVal u) @@ -307,11 +307,11 @@ compNeg :: Name -> Val -> Val -> System Val -> Val compNeg i a u ts = comp i (a `sym` i) u (ts `sym` i) compLine :: Val -> Val -> System Val -> Val -compLine a u ts = comp i (a @@@ i) u (Map.map (@@@ i) ts) +compLine a u ts = comp i (a @@ i) u (Map.map (@@ i) ts) where i = fresh (a,u,ts) compConstLine :: Val -> Val -> System Val -> Val -compConstLine a u ts = comp i a u (Map.map (@@@ i) ts) +compConstLine a u ts = comp i a u (Map.map (@@ i) ts) where i = fresh (a,u,ts) comps :: Name -> [(Ident,Ter)] -> Env -> [(System Val,Val)] -> [Val] @@ -332,7 +332,7 @@ fillNeg :: Name -> Val -> Val -> System Val -> Val fillNeg i a u ts = (fill i (a `sym` i) u (ts `sym` i)) `sym` i fillLine :: Val -> Val -> System Val -> Val -fillLine a u ts = VPath i $ fill i (a @@@ i) u (Map.map (@@@ i) ts) +fillLine a u ts = VPath i $ fill i (a @@ i) u (Map.map (@@ i) ts) where i = fresh (a,u,ts) -- fills :: Name -> [(Ident,Ter)] -> Env -> [(System Val,Val)] -> [Val] @@ -354,11 +354,11 @@ transNeg :: Name -> Val -> Val -> Val transNeg i a u = trans i (a `sym` i) u transLine :: Val -> Val -> Val -transLine u v = trans i (u @@@ i) v +transLine u v = trans i (u @@ i) v where i = fresh (u,v) transNegLine :: Val -> Val -> Val -transNegLine u v = transNeg i (u @@@ i) v +transNegLine u v = transNeg i (u @@ i) v where i = fresh (u,v) -- TODO: define in terms of comps? @@ -427,7 +427,7 @@ transpHIT i a@(Ter (HSum _ _ nass) env) u = VHComp _ v vs -> hComp (a `face` (i ~> 1)) (transpHIT i a v) $ mapWithKey (\alpha vAlpha -> - VPath j $ transpHIT j (aij `face` alpha) (vAlpha @@@ j)) vs + VPath j $ transpHIT j (aij `face` alpha) (vAlpha @@ j)) vs _ -> error $ "transpHIT: neutral " ++ show u @@ -448,7 +448,7 @@ squeezeHIT i a@(Ter (HSum _ _ nass) env) u = 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 + VPath j $ squeezeHIT j (aij `face` alpha) (vAlpha @@ j)) vs _ -> error $ "squeezeHIT: neutral " ++ show u hComp :: Val -> Val -> System Val -> Val @@ -474,7 +474,6 @@ equivFun = fstVal . sndVal equivContr :: Val -> Val equivContr = sndVal . sndVal - glue :: Val -> System Val -> Val glue b ts | eps `member` ts = equivDom (ts ! eps) | otherwise = VGlue b ts @@ -516,7 +515,7 @@ extend :: Val -> Val -> System Val -> Val extend b q ts = comp i b (fstVal q) ts' where i = fresh (b,q,ts) ts' = mapWithKey - (\alpha tAlpha -> app ((sndVal q) `face` alpha) tAlpha @@@ i) ts + (\alpha tAlpha -> app ((sndVal q) `face` alpha) tAlpha @@ i) ts -- psi/b corresponds to ws -- b0 corresponds to wi0 @@ -583,7 +582,6 @@ pathComp i a u0 u' us = VPath j $ comp i a u0 us' where j = fresh (Atom i,a,us,u0,u') us' = insertsSystem [(j ~> 1, u')] us - ------------------------------------------------------------------------------- -- | Composition in the Universe @@ -824,15 +822,16 @@ instance Convertible Val where (VVar x _, VVar x' _) -> x == x' (VIdP a b c,VIdP a' b' c') -> conv ns a a' && conv ns b b' && conv ns c c' (VPath i a,VPath i' a') -> conv ns (a `swap` (i,j)) (a' `swap` (i',j)) - (VPath i a,p') -> conv ns (a `swap` (i,j)) (p' @@@ j) - (p,VPath i' a') -> conv ns (p @@@ j) (a' `swap` (i',j)) + (VPath i a,p') -> conv ns (a `swap` (i,j)) (p' @@ j) + (p,VPath i' a') -> conv ns (p @@ j) (a' `swap` (i',j)) (VAppFormula u x,VAppFormula u' x') -> conv ns (u,x) (u',x') (VComp a u ts,VComp a' u' ts') -> conv ns (a,u,ts) (a',u',ts') (VHComp a u ts,VHComp a' u' ts') -> conv ns (a,u,ts) (a',u',ts') (VGlue v equivs,VGlue v' equivs') -> conv ns (v,equivs) (v',equivs') (VGlueElem u us,VGlueElem u' us') -> conv ns (u,us) (u',us') -- Anders: these two are from the compU branch: - (VUnGlueElemU u _ _,VUnGlueElemU u' _ _) -> conv ns u u' + (VUnGlueElemU u _ _,VUnGlueElemU u' _ _) -> conv ns u u' -- ?? + (VUnGlueElem u ts,VUnGlueElem u' ts') -> conv ns (u,ts) (u',ts') (VCompU u es,VCompU u' es') -> conv ns (u,es) (u',es') _ -> False