Eval.hs

{-# LANGUAGE CPP #-}
module Eval ( eval
            , evals
            , app
            , conv
            , fstSVal
            ) where

import Control.Arrow (second)
import Data.List
import Data.Maybe (fromMaybe)
import qualified Debug.Trace as DT

import CTT

debug :: Bool
#ifdef debugmode
debug = True
#else
debug = False
#endif

trace :: String -> a -> a
trace s e = if debug then DT.trace s e else e

look :: Ident -> OEnv -> (Binder, Val)
look x (OEnv (Pair rho (n@(y,l),u)) opaques)
  | x == y    = (n, u)
  | otherwise = look x (OEnv rho opaques)
look x r@(OEnv (PDef es r1) o) = case lookupIdent x es of
  Just (y,t)  -> (y,eval r t)
  Nothing     -> look x (OEnv r1 o)

eval :: OEnv -> Ter -> Val
eval e U                 = VU
eval e (PN pn)           = evalAppPN e pn []
eval e t@(App r s)       = case unApps t of
  (PN pn,us) -> evalAppPN e pn us
  _          -> app (eval e r) (eval e s)
eval e (Var i)           =
  let (x,v) = look i e
  in if x `elem` opaques e then VVar ("opaque_" ++ show x) $ support v else v
eval e (Pi a b)          = VPi (eval e a) (eval e b)
eval e (Lam x t)         = Ter (Lam x t) e -- stop at lambdas
eval e (Sigma a b)       = VSigma (eval e a) (eval e b)
eval e (SPair a b)       = VSPair (eval e a) (eval e b)
eval e (Fst a)           = fstSVal $ eval e a
eval e (Snd a)           = sndSVal $ eval e a
eval e (Where t decls)   = eval (oPDef False decls e) t
eval e (Con name ts)     = VCon name $ map (eval e) ts
eval e (Split pr alts)   = Ter (Split pr alts) e
eval e (Sum pr ntss)     = Ter (Sum pr ntss) e

evals :: OEnv -> [(Binder,Ter)] -> [(Binder,Val)]
evals env = map (second (eval env))

fstSVal, sndSVal :: Val -> Val
fstSVal (VSPair a b)    = a
fstSVal u | isNeutral u = VFst u
          | otherwise   = error $ show u ++ " should be neutral"
sndSVal (VSPair a b)    = b
sndSVal u | isNeutral u = VSnd u
          | otherwise   = error $ show u ++ " should be neutral"

-- Application
app :: Val -> Val -> Val
app (Ter (Lam x t) e) u                         = eval (oPair e (x,u)) t
app u1@(Kan Com (VPi a b) box@(Box dir x v nvs)) u =
  trace "Pi Com" $
  let z     = fresh (u1,u)
      box'  = swap box x z
      ufill = fill (swap a x z) (Box (mirror dir) z u [])
      bcu   = cubeToBox ufill (shapeOfBox box')
  in com (app (swap b x z) ufill) (appBox box' bcu)
app kf@(Kan Fill (VPi a b) box@(Box dir i w nws)) v =
  trace "Pi fill" $
  let x     = fresh (kf, v)
      u     = v `face` (i,dir)
      ufill = fill a (Box (mirror dir) i u [])
      bcu   = cubeToBox ufill (shapeOfBox box)
      vfill = fill a (Box (mirror dir) i u [((x,down),ufill),((x,up),v)])
      vx    = fill (app b ufill) (appBox box bcu)
      vi0   = app w (vfill `face` (i,mirror dir))
      vi1   = com (app b ufill) (appBox box bcu)
      nvs   = [ ((n,d),app ws (vfill `face` (n,d)))
              | ((n,d),ws) <- nws ]
  in com (app b vfill) (Box up x vx (((i,mirror dir),vi0) : ((i,dir),vi1):nvs))
-- app vext@(VExt x bv fv gv pv) w = do
--   -- NB: there are various choices how to construct this
--   let y = fresh (vext, w)
--   w0    <- w `face` (x,down)
--   left  <- app fv w0
--   right <- app gv (swap w x y)
--   pvxw  <- appNameM (app pv w0) x
--   comM (app bv w) (return (Box up y pvxw [((x,down),left),((x,up),right)]))
app vhext@(VHExt x bv fv gv pv) w =
  let a0 = w `face` (x,down)
      a1 = w `face` (x,up)
  in appName (apps pv [a0, a1, Path x w]) x
app (Ter (Split _ nvs) e) (VCon name us) = case lookup name nvs of
    Just (xs,t)  -> eval (upds e (zip xs us)) t
    Nothing -> error $ "app: Split with insufficient arguments; " ++
                        "missing case for " ++ name
app u@(Ter (Split _ _) _) v
  | isNeutral v = VSplit u v -- v should be neutral
  | otherwise   = error $ "app: (VSplit) " ++ show v ++ " is not neutral"
app r s
  | isNeutral r = VApp r s -- r should be neutral
  | otherwise   = error $ "app: (VApp) " ++ show r ++ " is not neutral"

apps :: Val -> [Val] -> Val
apps = foldl app

appBox :: Box Val -> Box Val -> Box Val
appBox (Box dir x v nvs) (Box _ _ u nus) =
  let lookup' x = fromMaybe (error "appBox") . lookup x
  in Box dir x (app v u) [ (nnd,app v (lookup' nnd nus))
                         | (nnd,v) <- nvs ]

appName :: Val -> Name -> Val
appName (Path x u) y | y `elem` [0,1] = u `face` (x,y)
appName p y          | y `elem` [0,1] = VAppName p y -- p has to be neutral
appName (Path x u) y | x == y             = u
                     | y `elem` support u = error ("appName " ++ "\nu = " ++
                                                   show u ++ "\ny = " ++ show y)
                     | otherwise          = swap u x y
appName v y          = VAppName v y

-- Apply a primitive notion
evalAppPN :: OEnv -> PN -> [Ter] -> Val
evalAppPN e pn ts
  | length ts < arity pn =
      -- Eta expand primitive notions
      let r       = arity pn - length ts
          binders = map (\n -> '_' : show n) [1..r]
          vars    = map Var binders
      in Ter (mkLams binders $ mkApps (PN pn) (ts ++ vars)) e
  | otherwise =
      let (args,rest) = splitAt (arity pn) ts
          vas = map (eval e) args
          p   = evalPN (freshs e) pn vas
          r   = map (eval e) rest
      in apps p r

-- Evaluate primitive notions
evalPN :: [Name] -> PN -> [Val] -> Val
evalPN (x:_) Id            [a,a0,a1]     = VId (Path x a) a0 a1
evalPN (x:_) IdP           [_,_,p,a0,a1] = VId p a0 a1
evalPN (x:_) Refl          [_,a]         = Path x a
evalPN (x:_) TransU        [_,_,p,t]     = com (appName p x) (Box up x t [])
evalPN (x:_) TransInvU     [_,_,p,t]     = com (appName p x) (Box down x t [])
evalPN (x:_) TransURef     [a,t]         = Path x $ fill a (Box up x t [])
evalPN (x:_) TransUEquivEq [_,b,f,_,_,u] =
  Path x $ fill b (Box up x (app f u) [])   -- TODO: Check this!
evalPN (x:y:_) CSingl [a,u,v,p] =
  let pv    = appName p y
      theta = fill a (Box up y u [((x,down),u),((x,up),pv)])
      omega = theta `face` (y,up)
  in Path x (VSPair omega (Path y theta))
-- evalPN (x:_)   Ext        [_,b,f,g,p]   = return $ Path x $ VExt x b f g p
evalPN (x:_)   HExt       [_,b,f,g,p]   = Path x $ VHExt x b f g p
evalPN _       Inh        [a]           = VInh a
evalPN _       Inc        [_,t]         = VInc t
evalPN (x:_)   Squash     [_,r,s]       = Path x $ VSquash x r s
evalPN _       InhRec     [_,b,p,phi,a] = inhrec b p phi a
evalPN (x:_)   EquivEq    [a,b,f,s,t]   = Path x $ VEquivEq x a b f s t
evalPN (x:y:_) EquivEqRef [a,s,t]       =
  Path y $ Path x $ VEquivSquare x y a s t
evalPN (x:_)   MapOnPath  [_,_,f,_,_,p]    = Path x $ app f (appName p x)
evalPN (x:_)   MapOnPathD [_,_,f,_,_,p]    = Path x $ app f (appName p x)
evalPN (x:_)   AppOnPath [_,_,_,_,_,_,p,q] =
  Path x $ app (appName p x) (appName q x)
evalPN (x:_)   MapOnPathS [_,_,_,f,_,_,p,_,_,q] =
  Path x $ app (app f (appName p x)) (appName q x)
evalPN _       Circle     []               = VCircle
evalPN _       Base       []               = VBase
evalPN (x:_)   Loop       []               = Path x $ VLoop x
evalPN _       CircleRec  [f,b,l,s]        = circlerec f b l s
evalPN _       I          []               = VI
evalPN _       I0         []               = VI0
evalPN _       I1         []               = VI1
evalPN (x:_)   Line       []               = Path x $ VLine x
evalPN _       IntRec     [f,s,e,l,u]      = intrec f s e l u
evalPN _       u          _                = error ("evalPN " ++ show u)

-- appS1 :: Val -> Val -> Name -> Eval Val
-- appS1 f p x | x `elem` [0,1] = appName p x
-- appS1 f p x = do
--   let y = fresh (p,(f,x))
--   q <- appName p y
--   a <- appName p 0
--   b <- appName p 1
--   newBox <- Box down y b <$>
--             sequenceSnd  [ ((x,down),q `face` (x,down))
--                          , ((x,up),b `face` (x,up))]
--   fb <- app f VBase
--   fl <- app f (VLoop y)
--   tu <- fillM (return VU) (Box down y fb <$>
--                            sequenceSnd [ ((x,down),fl `face` (x,down))
--                                        , ((x,up),fb `face` (x,up))])
--   com tu newBox

-- Compute the face of an environment
faceEnv :: OEnv -> Side -> OEnv
faceEnv e xd = mapOEnv (`face` xd) e

faceName :: Name -> Side -> Name
faceName 0 _                 = 0
faceName 1 _                 = 1
faceName x (y,d) | x == y    = d
                 | otherwise = x

-- -- Compute the face of a value
face :: Val -> Side -> Val
face u xdir@(x,dir) =
  let fc v = v `face` xdir in case u of
  VU      -> VU
  Ter t e -> eval (e `faceEnv` xdir) t
  VId a v0 v1 -> VId (fc a) (fc v0) (fc v1)
  Path y v | x == y    -> u
           | otherwise -> Path y (fc v)
  -- VExt y b f g p | x == y && dir == down -> f
  --                | x == y && dir == up   -> g
  --                | otherwise             ->
  --                  VExt y <$> fc b <*> fc f <*> fc g <*> fc p
  VHExt y b f g p | x == y && dir == down -> f
                  | x == y && dir == up   -> g
                  | otherwise             -> VHExt y (fc b) (fc f) (fc g) (fc p)
  VPi a f    -> VPi (fc a) (fc f)
  VSigma a f -> VSigma (fc a) (fc f)
  VSPair a b -> VSPair (fc a) (fc b)
  VInh v     -> VInh (fc v)
  VInc v     -> VInc (fc v)
  VSquash y v0 v1 | x == y && dir == down -> v0
                  | x == y && dir == up   -> v1
                  | otherwise             -> VSquash y (fc v0) (fc v1)
  VCon c us -> VCon c $ map fc us
  VEquivEq y a b f s t | x == y && dir == down -> a
                       | x == y && dir == up   -> b
                       | otherwise             ->
                         VEquivEq y (fc a) (fc b) (fc f) (fc s) (fc t)
  VPair y a v | x == y && dir == down -> a
              | x == y && dir == up   -> fc v
              | otherwise             -> VPair y (fc a) (fc v)
  VEquivSquare y z a s t | x == y                -> a
                         | x == z && dir == down -> a
                         | x == z && dir == up   ->
                           let idV = Ter (Lam (noLoc "x") (Var "x")) oEmpty
                           in VEquivEq y a a idV s t
                         | otherwise             ->
                          VEquivSquare y z (fc a) (fc s) (fc t)
  VSquare y z v | x == y                -> fc v
                | x == z && dir == down -> fc v
                | x == z && dir == up   ->
                  let v' = fc v
                  in VPair y (v' `face` (y,down)) v'
                | otherwise             -> VSquare y z $ fc v
  Kan Fill a b@(Box dir' y v nvs)
    | x /= y && x `notElem` nonPrincipal b -> fill (fc a) (mapBox fc b)
    | x `elem` nonPrincipal b              -> lookBox (x,dir) b
    | x == y && dir == mirror dir'         -> v
    | otherwise                            -> com a b
  VFillN a b@(Box dir' y v nvs)
    | x /= y && x `notElem` nonPrincipal b -> fill (fc a) (mapBox fc b)
    | x `elem` nonPrincipal b              -> lookBox (x,dir) b
    | x == y && dir == mirror dir'         -> v
    | otherwise                            -> com a b
  Kan Com a b@(Box dir' y v nvs)
    | x == y                     -> u
    | x `notElem` nonPrincipal b -> com (fc a) (mapBox fc b)
    | x `elem` nonPrincipal b    -> lookBox (x,dir) b `face` (y,dir')
  VComN a b@(Box dir' y v nvs)
    | x == y                     -> u
    | x `notElem` nonPrincipal b -> com (fc a) (mapBox fc b)
    | x `elem` nonPrincipal b    -> lookBox (x,dir) b `face` (y,dir')
  VComp b@(Box dir' y _ _)
    | x == y                     -> u
    | x `notElem` nonPrincipal b -> VComp $ mapBox fc b
    | x `elem` nonPrincipal b    -> lookBox (x,dir) b `face` (y,dir')
  VFill z b@(Box dir' y v nvs)
    | x == z                               -> u
    | x /= y && x `notElem` nonPrincipal b -> VFill z $ mapBox fc b
    | (x,dir) `elem` defBox b              ->
      lookBox (x,dir) (mapBox (`face` (z,down)) b)
    | x == y && dir == dir'                ->
        VComp (mapBox (`face` (z,up)) b)
  VInhRec b p h a     -> inhrec (fc b) (fc p) (fc h) (fc a)
  VApp u v            -> app (fc u) (fc v)
  VAppName u n        -> appName (fc u) (faceName n xdir)
  VSplit u v          -> app (fc u) (fc v)
  VVar s d            -> VVar s [ faceName n xdir | n <- d ]
  VFst p              -> fstSVal $ fc p
  VSnd p              -> sndSVal $ fc p
  VCircle             -> VCircle
  VBase               -> VBase
  VLoop y | x == y    -> VBase
          | otherwise -> VLoop y
  VCircleRec f b l s  -> circlerec (fc f) (fc b) (fc l) (fc s)
  VI  -> VI
  VI0 -> VI0
  VI1 -> VI1
  VLine y
    | x == y && dir == down -> VI0
    | x == y && dir == up   -> VI1
    | otherwise             -> VLine y
  VIntRec f s e l u -> intrec (fc f) (fc s) (fc e) (fc l) (fc u)

unCompAs :: Val -> Name -> Box Val
unCompAs (VComp box) y = swap box (pname box) y
unCompAs v           _ = error $ "unCompAs: " ++ show v ++ " is not a VComp"

unFillAs :: Val -> Name -> Box Val
unFillAs (VFill x box) y = swap box x y
unFillAs v             _ = error $ "unFillAs: " ++ show v ++ " is not a VFill"

-- p(x) = <z>q(x,z)
-- a(x) = q(x,0)     b(x) = q(x,1)
-- q(0,y) connects a(0) and b(0)
-- we connect q(0,0) to q(1,1)
-- appDiag :: Val -> Val -> Name -> Val
-- appDiag tu p x | x `elem` [0,1] = appName p x
-- appDiag tu p x =
-- traceb ("appDiag " ++ "\ntu = " ++ show tu ++ "\np = " ++ show p ++ "\nx = "
-- --                       ++ show x ++ " " ++ show y
-- --                       ++ "\nq = " ++ show q) -- "\nnewBox =" ++ show newBox)
--  com tu newBox
--    where y = fresh (p,(tu,x))
--          q = appName p y
--          a = appName p 0
--          b = appName p 1
--          newBox = Box down y b [((x,down),q `face` (x,down)),((x,up),b `face` (x,up))]

cubeToBox :: Val -> Box () -> Box Val
cubeToBox v = modBox (\nd _ -> v `face` nd)

inhrec :: Val -> Val -> Val -> Val -> Val
inhrec _ _ phi (VInc a)          = app phi a
inhrec b p phi (VSquash x a0 a1) =
  let fc w d   = w `face` (x,d)
      b0       = inhrec (fc b down) (fc p down) (fc phi down) a0
      b1       = inhrec (fc b up) (fc p up) (fc phi up) a1
      z        = fresh [b,p,phi,b0,b1]
      b0fill   = fill b (Box up x b0 [])
      b0fillx1 = b0fill `face` (x, up)
      right    = appName (app (app (fc p up) b0fillx1) b1) z
  in com b (Box up z b0fill [((x,down),b0),((x,up),right)])
inhrec b p phi (Kan ktype (VInh a) box) =
  let irec (j,dir) v = let fc v = v `face` (j,dir)
                       in inhrec (fc b) (fc p) (fc phi) v
      box' = modBox irec box
  in kan ktype b box'
inhrec b p phi v = VInhRec b p phi v -- v should be neutral

circlerec :: Val -> Val -> Val -> Val -> Val
circlerec _ b _ VBase       = b
circlerec f b l v@(VLoop x) =
  let y     = fresh [f,b,l,v]
      pxy   = appName l y
      theta = connection VCircle x y v
      a     = app f theta
      px1   = pxy `face` (y,up)
      p11   = px1 `face` (x,up)
      p0y   = pxy `face` (x,down)
  in com a (Box down y px1 [((x,down),p0y),((x,up),p11)])
circlerec f b l v@(Kan ktype VCircle box) = kan ktype ffillv box'
  where y = fresh [f,b,l,v]
        boxxy = swap box (pname box) y
        crec side = let fc w = w `face` side
                    in circlerec (fc f) (fc b) (fc l)
        ffillv = app f (Kan Fill VCircle boxxy)
        box'   = modBox crec boxxy
circlerec f b l v = VCircleRec f b l v -- v should be neutral

-- Assumes y is fresh and x fresh for a; constructs a connection
-- square with faces u (x), u (y), u (1), u (1).
connection :: Val -> Name -> Name -> Val -> Val
connection a x y u =
  let u1      = u `face` (x,up)
      ufill   = fill a (Box down y u1 [((x,down), swap u x y), ((x,up),u1)])
      z       = fresh ([x,y], [a,u])
      ufillzy = swap ufill x z
      ufillzx = swap ufillzy y x
  in com a (Box down z u1 [ ((x,down),ufillzy), ((x,up),u1)
                          , ((y,down),ufillzx), ((y,up),u1)])

intrec :: Val -> Val -> Val -> Val -> Val -> Val
intrec _ s _ _ VI0         = s
intrec _ _ e _ VI1         = e
intrec f s e l v@(VLine x) =
  let y     = fresh [f,s,e,l,v]
      pxy   = appName l y
      theta = connection VI x y v
      a     = app f theta
      px1   = pxy `face` (y,up)
      p11   = px1 `face` (x,up)
      p0y   = pxy `face` (x,down)
  in com a (Box down y px1 [((x,down),p0y),((x,up),p11)])
intrec f s e l v@(Kan ktype VCircle box) =
  let irec side u = let fc w = w `face` side
                    in intrec (fc f) (fc s) (fc e) (fc l) u
      fv   = app f v
      box' = modBox irec box
  in kan ktype fv box'
intrec f s e l v = VIntRec f s e l v -- v should be neutral

kan :: KanType -> Val -> Box Val -> Val
kan Fill = fill
kan Com  = com

isNeutralFill :: Val -> Box Val -> Bool
isNeutralFill v box | isNeutral v               = True
isNeutralFill v@(Ter (PN (Undef _)) _) box      = True
isNeutralFill (Ter (Sum _ _) _) (Box _ _ v nvs) =
 isNeutral v || or [ isNeutral u | (_,u) <- nvs ]
isNeutralFill v@(Kan Com VU tbox') box@(Box d x _ _) = do
  let nK  = nonPrincipal tbox'
      nJ  = nonPrincipal box
      nL  = nJ \\ nK
      aDs = if x `elem` nK then allDirs nL else (x,mirror d):allDirs nL
  or [ isNeutral (lookBox yc box) | yc <- aDs ]
isNeutralFill v@(Kan Fill VU tbox) box =
  or [ isNeutral (lookBox yc box) | yc <- defBox box \\ defBox tbox ]
isNeutralFill v@(VEquivSquare y z _ _ _) box@(Box d x _ _) = do
  let nJ  = nonPrincipal box
      nL  = nJ \\ [y,z]
      aDs = if x `elem` [y,z] then allDirs nL else (x,mirror d) : allDirs nL
  or [ isNeutral (lookBox yc box) | yc <- aDs ]
isNeutralFill v@(VEquivEq z a b f s t) box@(Box d x vx nxs)
  | d == down && z == x = isNeutral $ app s vx
  | otherwise           = -- TODO: check
    let nJ  = nonPrincipal box
        nL  = nJ \\ [z]
        aDs = if x == z then allDirs nL else (x,mirror d) : allDirs nL
    in or [ isNeutral (lookBox yc box) | yc <- aDs ]
isNeutralFill v box = False

-- TODO: Simplify?
fills :: [(Binder,Ter)] -> OEnv -> [Box Val] -> [Val]
fills []         _ []          = []
fills ((x,a):as) e (box:boxes) =
  let v  = fill (eval e a) box
      vs = fills as (oPair e (x,v)) boxes
  in v : vs
fills _ _ _ = error "fills: different lengths of types and values"

unPack :: Name -> Name -> (Name,Dir) -> Val -> Val
unPack x y (z,c) v | z /= x && z /= y  = unSquare v
                   | z == y && c == up = sndVal v
                   | otherwise         = v

-- -- Kan filling
fill :: Val -> Box Val -> Val
fill v box | isNeutralFill v box = VFillN v box
fill vid@(VId a v0 v1) box@(Box dir i v nvs) =
  let x = fresh (vid, box)
      box' = consBox (x,(v0,v1)) (mapBox (`appName` x) box)
  in Path x $ fill (a `appName` x) box'
fill (VSigma a f) box@(Box dir x v nvs) =
  let u = fill a (mapBox fstSVal box)
  in VSPair u $ fill (app f u) (mapBox sndSVal box)
-- assumes cvs are constructor vals
fill v@(Ter (Sum _ nass) env) box@(Box _ _ (VCon n _) _) = case getIdent n nass of
  Just as ->
    let boxes = transposeBox $ mapBox unCon box
    -- fill boxes for each argument position of the constructor
    in VCon n $ fills as env boxes
  Nothing -> error $ "fill: missing constructor in labelled sum " ++ n
fill (VEquivSquare x y a s t) box@(Box dir x' vx' nvs) =
  VSquare x y $ fill a (modBox (unPack x y) box)
fill veq@(VEquivEq x a b f s t) box@(Box dir z vz nvs)
  | x /= z && x `notElem` nonPrincipal box =
    trace "VEquivEq case 1" $
    let ax0 = fill a (mapBox fstVal box)
        bx0 = app f ax0
        bx  = mapBox sndVal box
        bx' = mapBox (`face` (x,up)) bx
        bx1 = fill b bx'        --- independent of x
        v   = fill b $ (x,(bx0,bx1)) `consBox` bx
    in VPair x ax0 v
  | x /= z && x `elem` nonPrincipal box =
    trace "VEquivEq case 2" $
    let ax0 = lookBox (x,down) box

        -- modification function
        mf (ny,dy) vy | x /= ny    = sndVal vy
                      | dy == down = app f ax0
                      | otherwise  = vy

        bx  = modBox mf box
    in VPair x ax0 (fill b bx)
  | x == z && dir == up =
    trace "VEquivEq case 3" $
    let ax0 = vz
        bx0 = app f ax0
        v   = fill b $ Box dir z bx0 [ (nnd,sndVal v) | (nnd,v) <- nvs ]
    in VPair x ax0 v
  | x == z && dir == down =
    trace "VEquivEq case 4" $
    let gbsb    = app s vz
        (gb,sb) = (fstSVal gbsb, sndSVal gbsb)
        y       = fresh (veq, box)
        vy      = appName sb x

        vpTSq :: Name -> Dir -> Val -> (Val,Val)
        vpTSq nz dz (VPair z a0 v0) =
          let vp       = VSPair a0 (Path z v0)
              t0       = t `face` (nz,dz)
              b0       = vz `face` (nz,dz)
              l0sq0    = appName (app (app t0 b0) vp) y
              (l0,sq0) = (fstSVal l0sq0, sndSVal l0sq0)
              sq0x     = appName sq0 x
          in (l0,sq0x)  -- TODO: check the correctness of the square s0

        -- TODO: Use modBox!
        vsqs   = [ ((n,d),vpTSq n d v) | ((n,d),v) <- nvs]
        box1   = Box up y gb [ (nnd,v) | (nnd,(v,_)) <- vsqs ]
        afill  = fill a box1
        acom   = afill `face` (y,up)
        fafill = app f afill
        box2   = Box up y vy (((x,down),fafill) : ((x,up),vz) :
                            [ (nnd,v) | (nnd,(_,v)) <- vsqs ])
        bcom   = com b box2
    in VPair x acom bcom
  | otherwise = error "fill EqEquiv"
fill v@(Kan Com VU tbox') box@(Box dir x' vx' nvs')
  | toAdd /= [] = -- W.l.o.g. assume that box contains faces for
                  -- the non-principal sides of tbox.
    trace "Kan Com 1" $
    let add :: Side -> Val
        add yc = let box' = mapBox (`face` yc) box
                 in fill (lookBox yc tbox `face` (x,tdir)) box'

        sides' = [ (n,(add (n,down),add (n,up))) | n <- toAdd ]

     in fill v (sides' `appendBox` box)
  | x' `notElem` nK =
    trace "Kan Com 2" $
    let principal    = fill tx (mapBox (pickout (x,tdir')) boxL)
        nonprincipal =
          [ let pyc  = principal `face` yc
                side = [((x,tdir),lookBox yc box),((x,tdir'),pyc)]
                v'   = fill (lookBox yc tbox)
                            (side `appendSides` mapBox (pickout yc) boxL)
                in (yc,v')
          | yc <- allDirs nK ]
    in VComp (Box tdir x principal nonprincipal)
  | x' `elem` nK =
    trace "Kan Com 3" $
    let -- assumes zc in defBox tbox
        auxsides zc = [ (yd,pickout zc (lookBox yd box)) | yd <- allDirs nL ]

        -- extend input box along x with orientation tdir'; results
        -- in the non-principal faces on the intersection of defBox
        -- box and defBox tbox; note, that the intersection contains
        -- (x',dir'), but not (x',dir) (and (x,_))
        npintbox = modBox (\yc boxside -> fill (lookBox yc tbox)
                                          (Box tdir' x boxside (auxsides yc)))
                     (subBox (nK `intersect` nJ) box)

        npintfacebox = mapBox (`face` (x,tdir')) npintbox
        principal    = fill tx (auxsides (x,tdir') `appendSides` npintfacebox)
        nplp         = principal `face` (x',dir)
        fnpintboxs   = [ (yc,v `face` (x',dir)) | (yc,v) <- sides npintbox ]
        nplnp        = auxsides (x',dir) ++ fnpintboxs
        -- the missing non-principal face on side (x',dir)
        v'           = fill (lookBox (x',dir) tbox) (Box tdir x nplp nplnp)
        nplast       = ((x',dir),v')

    in VComp (Box tdir x principal (nplast:fromBox npintbox))
  where nK    = nonPrincipal tbox
        nJ    = nonPrincipal box
        z     = fresh (tbox', box)
        -- x is z
        tbox@(Box tdir x tx nvs) = swap tbox' (pname tbox') z
        toAdd = nK \\ (x' : nJ)
        nL    = nJ \\ nK
        boxL  = subBox nL box
        dir'  = mirror dir
        tdir' = mirror tdir
        -- asumes zd is in the sides of tbox
        pickout zd vcomp = lookBox zd (unCompAs vcomp z)
fill v@(Kan Fill VU tbox@(Box tdir x tx nvs)) box@(Box dir x' vx' nvs')
  -- the cases should be (in order):
  -- 1) W.l.o.g. K subset x', J
  -- 2) x' = x &  dir = tdir
  -- 3) x' = x &  dir = mirror tdir
  -- 4) x' `notElem` K
  -- 5) x' `elem` K
  | toAdd /= [] =
    -- W.l.o.g. x,nK subset x':nJ
    trace "Kan Fill VU Case 1" $
    let add :: Side -> Val
        add zc = fill (v `face` zc) (mapBox (`face` zc) box)

        newSides = [ (zc,add zc) | zc <- allDirs toAdd ]
    in fill v (newSides `appendSides` box)
  | x == x' && dir == tdir =
    -- assumes K subset x',J
    trace "Kan Fill VU Case 2" $
    let boxp = lookBox (x,dir') box  -- is vx'
        principal = fill (lookBox (x',tdir') tbox)
                         (Box up z boxp (auxsides (x',tdir')))
        nonprincipal =
          [ (zc,let principzc = lookBox zc box
                    fpzc = principal `face` zc
                    -- "degenerate" along z!
                    ppzc = principzc `face` (x,tdir)
                    sides = [((x,tdir'),fpzc),((x,tdir),ppzc)]
                in fill (lookBox zc tbox)
                        (Box up z principzc (sides ++ auxsides zc)))
          | zc <- allDirs nK ]
    in VFill z (Box tdir x principal nonprincipal)
  | x == x' && dir == mirror tdir =
    -- assumes K subset x',J
    trace "Kan Fill VU Case 3" $
    let -- the principal side of box must be a VComp
        -- should be safe given the neutral test at the beginning
        upperbox = unCompAs (lookBox (x,tdir) box) x
        nonprincipal =
          [ (zc,let top    = lookBox zc upperbox
                    bottom = lookBox zc box
                    princ  = top `face` (x,tdir) -- same as: bottom `face` (x,tdir)
                    sides  = [((z,down),bottom),((z,up),top)]
               in fill (lookBox zc tbox) (Box tdir' x princ -- "degenerate" along z!
                                       (sides ++ auxsides zc)))
          | zc <- allDirs nK ]
        nonprincipalfaces = [ (zc,u `face` (x,dir)) | (zc,u) <- nonprincipal ]
        principal         = fill (lookBox (x,tdir') tbox)
                             (Box up z (lookBox (x,tdir') upperbox)
                                       (nonprincipalfaces ++ auxsides (x,tdir')))
    in VFill z (Box tdir x principal nonprincipal)
  | x' `notElem` nK =
    -- assumes x,K subset x',J
    trace "Kan Fill VU Case 4" $
    let xaux      = unCompAs (lookBox (x,tdir) box) x
        boxprinc  = unFillAs (lookBox (x',dir') box) z
        princnp   = [((z,up),lookBox (x,tdir') xaux),
                     ((z,down),lookBox (x,tdir') box)]
                    ++ auxsides (x,tdir')
        principal = fill (lookBox (x,tdir') tbox) -- tx
                         (Box dir x' (lookBox (x,tdir') boxprinc) princnp)
        nonprincipal = [ let yup  = lookBox yc xaux
                             fyup = yup `face` (x,tdir)
                             np   = [ ((z,up),yup), ((z,down),lookBox yc box)
                                    , ((x,tdir), fyup) -- deg along z!
                                    , ((x,tdir'), principal `face` yc) ]
                                    ++ auxsides yc
                             fb   = fill (lookBox yc tbox)
                                         (Box dir x' (lookBox yc boxprinc) np)
                         in (yc, fb)
                       | yc <- allDirs nK]
    in VFill z (Box tdir x principal nonprincipal)
  | x' `elem` nK =
    -- assumes x,K subset x',J
    trace "Kan Fill VU Case 5" $
    -- surprisingly close to the last case of the Kan-Com-VU filling
    let upperbox = unCompAs (lookBox (x,tdir) box) x
        npintbox = modBox (\zc downside ->
                            let bottom = lookBox zc box
                                top    = lookBox zc upperbox
                                princ  = downside
                                         -- same as bottom `face` (x',tdir) and
                                         -- top `face` (x',tdir)
                                sides  = [((z,down),bottom),((z,up),top)]
                            in fill (lookBox zc tbox)
                                    (Box tdir' x princ (sides ++ auxsides zc)))
                   (subBox (nK `intersect` nJ) box)  -- intersection is nK - x'
        npint = fromBox npintbox
        npintfacebox = mapBox (`face` (x,tdir')) npintbox
        principalbox = ([ ((z,down),lookBox (x,tdir') box)
                        , ((z,up)  ,lookBox (x,tdir') upperbox)]
                        ++ auxsides (x,tdir'))
                       `appendSides` npintfacebox
        principal = fill tx principalbox
        nplp      = lookBox (x',dir) upperbox
        nplnp = [ ((x,tdir), nplp `face` (x',dir)) -- deg along z!
                , ((x,tdir'),principal `face` (x',dir)) ]
                ++ auxsides (x',dir)
                ++ [ (zc,u `face` (x',dir)) | (zc,u) <- sides npintbox ]
        fb = fill (lookBox (x',dir) tbox) (Box down z nplp nplnp)
    in VFill z (Box tdir x principal (((x',dir),fb) : npint))
    where z     = fresh (v, box)
          nK    = nonPrincipal tbox
          nJ    = nonPrincipal box
          toAdd = (x:nK) \\ (x' : nJ)
          nL    = nJ \\ (x : nK)
          dir'  = mirror dir
          tdir' = mirror tdir
          -- asumes zc is in the sides of tbox
          pickout zc vfill = lookBox zc (unFillAs vfill z)
          -- asumes zc is in the sides of tbox
          auxsides zc = [ (yd,pickout zc (lookBox yd box)) | yd <- allDirs nL ]
fill v b = Kan Fill v b

-- -- Composition (ie., the face of fill which is created)
com :: Val -> Box Val -> Val
com u box | isNeutralFill u box = VComN u box
com vid@VId{} box@(Box dir i _ _)         = fill vid box `face` (i,dir)
com vsigma@VSigma{} box@(Box dir i _ _)   = fill vsigma box `face` (i,dir)
com veq@VEquivEq{} box@(Box dir i _ _)    = fill veq box `face` (i,dir)
com u@(Kan Com VU _) box@(Box dir i _ _)  = fill u box `face` (i,dir)
com u@(Kan Fill VU _) box@(Box dir i _ _) = fill u box `face` (i,dir)
com ter@Ter{} box@(Box dir i _ _)         = fill ter box `face` (i,dir)
com v box                                 = Kan Com v box

conv :: Int -> Val -> Val -> Bool
conv k VU VU                                  = True
conv k (Ter (Lam x u) e) (Ter (Lam x' u') e') =
  let v = mkVar k $ support (e, e')
  in conv (k+1) (eval (oPair e (x,v)) u) (eval (oPair e' (x',v)) u')
conv k (Ter (Lam x u) e) u' =
  let v = mkVar k $ support (e,u')
  in conv (k+1) (eval (oPair e (x,v)) u) (app u' v)
conv k u' (Ter (Lam x u) e) =
  let v = mkVar k $ support (u',e)
  in conv (k+1) (app u' v) (eval (oPair e (x,v)) u)
conv k (Ter (Split p _) e) (Ter (Split p' _) e') =
  (p == p') && convEnv k e e'
conv k (Ter (Sum p _) e)   (Ter (Sum p' _) e') =
  (p == p') && convEnv k e e'
conv k (Ter (PN (Undef p)) e) (Ter (PN (Undef p')) e') =
  (p == p') && convEnv k e e'
conv k (VPi u v) (VPi u' v') =
  let w = mkVar k $ support [u,u',v,v']
  in conv k u u' && conv (k+1) (app v w) (app v' w)
conv k (VSigma u v) (VSigma u' v') =
  let w = mkVar k $ support [u,u',v,v']
  in conv k u u' && conv (k+1) (app v w) (app v' w)
conv k (VId a u v) (VId a' u' v') = and [conv k a a', conv k u u', conv k v v']
conv k (Path x u) (Path x' u')    = conv k (swap u x z) (swap u' x' z)
  where z = fresh (u,u')
conv k (Path x u) p'              = conv k (swap u x z) (appName p' z)
  where z = fresh u
conv k p (Path x' u')             = conv k (appName p z) (swap u' x' z)
  where z = fresh u'
-- conv k (VExt x b f g p) (VExt x' b' f' g' p') =
--   andM [x <==> x', conv k b b', conv k f f', conv k g g', conv k p p']
conv k (VHExt x b f g p) (VHExt x' b' f' g' p') =
  and [x == x', conv k b b', conv k f f', conv k g g', conv k p p']
conv k (VFst u) (VFst u')                     = conv k u u'
conv k (VSnd u) (VSnd u')                     = conv k u u'
conv k (VInh u) (VInh u')                     = conv k u u'
conv k (VInc u) (VInc u')                     = conv k u u'
conv k (VSquash x u v) (VSquash x' u' v')     =
  and [x == x', conv k u u', conv k v v']
conv k (VCon c us) (VCon c' us') = (c == c') && and (zipWith (conv k) us us')
conv k (Kan Fill v box) (Kan Fill v' box')    =
  conv k v v' && convBox k box box'
conv k (Kan Com v box) (Kan Com v' box')      =
  and [conv k (swap v x y) (swap v' x' y),
       convBox k (swap box x y) (swap box' x' y)]
  where y      = fresh ((v,v'),(box,box'))
        (x,x') = (pname box, pname box')
conv k (VComN v box) (VComN v' box')      =
  and [conv k (swap v x y) (swap v' x' y),
       convBox k (swap box x y) (swap box' x' y)]
  where y      = fresh ((v,v'),(box,box'))
        (x,x') = (pname box, pname box')
conv k (VFillN v box) (VFillN v' box')      =
  and [conv k v v', convBox k (swap box x y) (swap box' x' y)]
  where y      = fresh ((v,v'),(box,box'))
        (x,x') = (pname box, pname box')
conv k (VEquivEq x a b f s t) (VEquivEq x' a' b' f' s' t') =
  and [x == x', conv k a a', conv k b b',
       conv k f f', conv k s s', conv k t t']
conv k (VEquivSquare x y a s t) (VEquivSquare x' y' a' s' t') =
  and [x == x', y == y', conv k a a', conv k s s', conv k t t']
conv k (VPair x u v) (VPair x' u' v')     =
  and [x == x', conv k u u', conv k v v']
conv k (VSquare x y u) (VSquare x' y' u') =
  and [x == x', y == y', conv k u u']
conv k (VComp box) (VComp box')           =
  convBox k (swap box x y) (swap box' x' y)
  where y      = fresh (box,box')
        (x,x') = (pname box, pname box')
conv k (VFill x box) (VFill x' box')      =
  convBox k (swap box x y) (swap box' x' y)
  where y      = fresh (box,box')
conv k (VSPair u v)   (VSPair u' v')   = conv k u u' && conv k v v'
conv k (VSPair u v)   w                =
  conv k u (fstSVal w) && conv k v (sndSVal w)
conv k w              (VSPair u v)     =
  conv k (fstSVal w) u && conv k (sndSVal w) v
conv k (VApp u v)     (VApp u' v')     = conv k u u' && conv k v v'
conv k (VAppName u x) (VAppName u' x') = conv k u u' && (x == x')
conv k (VSplit u v)   (VSplit u' v')   = conv k u u' && conv k v v'
conv k (VVar x d)     (VVar x' d')     = (x == x') && (d == d')
conv k (VInhRec b p phi v) (VInhRec b' p' phi' v') =
  and [conv k b b', conv k p p', conv k phi phi', conv k v v']
conv k VCircle        VCircle          = True
conv k VBase          VBase            = True
conv k (VLoop x)      (VLoop y)        = x == y
conv k (VCircleRec f b l v) (VCircleRec f' b' l' v') =
  and [conv k f f', conv k b b', conv k l l', conv k v v']
conv k VI             VI               = True
conv k VI0            VI0              = True
conv k VI1            VI1              = True
conv k (VLine x)      (VLine y)        = x == y
conv k (VIntRec f s e l u) (VIntRec f' s' e' l' u') =
  and [conv k f f', conv k s s', conv k e e', conv k l l', conv k u u']
conv k _              _                = False

convBox :: Int -> Box Val -> Box Val -> Bool
convBox k box@(Box d pn _ ss) box'@(Box d' pn' _ ss') =
  if (d == d') && (pn == pn') && (sort np == sort np')
     then and [ conv k (lookBox s box) (lookBox s box')
              | s <- defBox box ]
     else False
  where (np, np') = (nonPrincipal box, nonPrincipal box')

convEnv :: Int -> OEnv -> OEnv -> Bool
convEnv k e e' = and $ zipWith (conv k) (valOfOEnv e) (valOfOEnv e')