remove @@@

diff --git a/Eval.hs b/Eval.hs
index 8605ba96710994bfe253d3a766ff35e060ad5e27..e181d9fc2fbe754ed61fd28c94cbf3de26252690 100644 (file)
--- 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