\chapter{The modified zipper}

\label{app:zipperfix}

The following two sections list the modules that make up the modified zipper,
based \texttt{zipper-0.3} on
Hackage\footnote{\url{http://hackage.haskell.org/package/zipper-0.3}}. The
first module is a subset of the module zipper, mostly unmodified. The second
module contains functions for zippers that work specifically on |HFix| fixed
points. There is also a version that works on shallow values, where all the
original subtrees are original |ix| values and only the context is represented
generically; this version is not included here because it is not used in this
thesis.

\section{module Annotations.MultiRec.Zipper}

\begin{code}
{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE GADTs                  #-}
{-# LANGUAGE KindSignatures         #-}
{-# LANGUAGE MultiParamTypeClasses  #-}
{-# LANGUAGE RankNTypes             #-}
{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE TypeOperators          #-}
{-# LANGUAGE ScopedTypeVariables    #-}

module Annotations.MultiRec.Zipper where

import Prelude hiding (last)

import Control.Monad
import Control.Applicative
import Data.Maybe

import Generics.MultiRec.Base
import Generics.MultiRec.HFunctor

data Loc :: (* -> *) -> ((* -> *) -> * -> *) -> (* -> *) -> * -> * where
  Loc :: phi ix -> r ix -> Ctxs phi f ix r a -> Loc phi f r a

data Ctxs :: (* -> *) -> ((* -> *) -> * -> *) -> * -> (* -> *) -> * -> * where
  Empty :: Ctxs phi f a r a
  Push  :: phi ix -> Ctx f b r ix -> Ctxs phi f ix r a -> Ctxs phi f b r a

data family Ctx f :: * -> (* -> *) -> * -> *

data instance Ctx (K a)       b r ix
data instance Ctx U           b r ix
data instance Ctx (f :+: g)   b r ix  =  CL    (Ctx f b r ix)
                                      |  CR    (Ctx g b r ix)
data instance Ctx (f :*: g)   b r ix  =  C1    (Ctx f b r ix) (g r ix)
                                      |  C2    (f r ix)       (Ctx g b r ix)
data instance Ctx (I xi)      b r ix  =  CId   (b :=: xi)
data instance Ctx (f :>: xi)  b r ix  =  CTag  (ix :=: xi) (Ctx f b r ix)
data instance Ctx (C c f)     b r ix  =  CC    (Ctx f b r ix)

instance Zipper phi f => HFunctor phi (Ctx f b)       where
  hmapA                    = cmapA

instance Zipper phi f => HFunctor phi (Ctxs phi f b)  where
  hmapA f p' Empty         = pure Empty
  hmapA f p' (Push p c s)  = liftA2 (Push p) (hmapA f p c) (hmapA f p' s)

instance Zipper phi f => HFunctor phi (Loc phi f)     where
  hmapA f p' (Loc p x s)    = liftA2 (Loc p) (f p x) (hmapA f p' s)

class HFunctor phi f => Zipper phi f where
  cmapA        :: Applicative a => (forall ix. phi ix -> r ix -> a (r' ix)) ->
                    phi ix -> Ctx f b r ix -> a (Ctx f b r' ix)
  fill         :: phi b -> Ctx f b r ix -> r b -> f r ix
  first, last  :: (forall b. phi b -> r b -> Ctx f b r ix -> a) ->
                    f r ix -> Maybe a
  next, prev   :: (forall b. phi b -> r b -> Ctx f b r ix -> a) ->
                    phi b -> Ctx f b r ix -> r b -> Maybe a

instance El phi xi => Zipper phi (I xi) where
  cmapA f p (CId prf)    =  pure (CId prf)
  fill    p (CId prf) x  =  castId prf I x
  first f (I x)          =  return (f proof x (CId Refl))
  last  f (I x)          =  return (f proof x (CId Refl))
  next  f p (CId prf) x  =  Nothing
  prev  f p (CId prf) x  =  Nothing

instance Zipper phi (K a) where
  cmapA f p void         =  impossible void
  fill    p void x       =  impossible void
  first f (K a)          =  Nothing
  last  f (K a)          =  Nothing
  next  f p void x       =  impossible void
  prev  f p void x       =  impossible void

instance Zipper phi U where
  cmapA f p void         =  impossible void
  fill    p void x       =  impossible void
  first f U              =  Nothing
  last  f U              =  Nothing
  next  f p void x       =  impossible void
  prev  f p void x       =  impossible void

instance (Zipper phi f, Zipper phi g) => Zipper phi (f :+: g) where
  cmapA f p (CL c)       =  liftA CL (cmapA f p c)
  cmapA f p (CR c)       =  liftA CR (cmapA f p c)
  fill    p (CL c) x     =  L (fill p c x)
  fill    p (CR c) y     =  R (fill p c y)
  first f (L x)          =  first (\p z -> f p z . CL) x
  first f (R y)          =  first (\p z -> f p z . CR) y
  last  f (L x)          =  last  (\p z -> f p z . CL) x
  last  f (R y)          =  last  (\p z -> f p z . CR) y
  next  f p (CL c) x     =  next  (\p z -> f p z . CL) p c x
  next  f p (CR c) y     =  next  (\p z -> f p z . CR) p c y
  prev  f p (CL c) x     =  prev  (\p z -> f p z . CL) p c x
  prev  f p (CR c) y     =  prev  (\p z -> f p z . CR) p c y

instance (Zipper phi f, Zipper phi g) => Zipper phi (f :*: g) where
  cmapA f p (C1 c y)     =  liftA2 C1 (cmapA f p c) (hmapA f p y)
  cmapA f p (C2 x c)     =  liftA2 C2 (hmapA f p x) (cmapA f p c)
  fill    p (C1 c y) x   =  fill p c x :*: y
  fill    p (C2 x c) y   =  x :*: fill p c y
  first f (x :*: y)      =  first  (\p z c  -> f p z (C1 c y)) x `mplus`
                            first  (\p z c  -> f p z (C2 x c)) y
  last  f (x :*: y)      =  last   (\p z c  -> f p z (C2 x c)) y `mplus`
                            last   (\p z c  -> f p z (C1 c y)) x
  next  f p (C1 c y) x   =  next   (\p' z c' -> f p' z (C1 c'            y   )) p c x `mplus`
                            first  (\p' z c' -> f p' z (C2 (fill p c x)  c'  )) y
  next  f p (C2 x c) y   =  next   (\p' z c' -> f p' z (C2 x c')) p c y
  prev  f p (C1 c y) x   =  prev   (\p' z c' -> f p' z (C1 c' y )) p c x
  prev  f p (C2 x c) y   =  prev   (\p' z c' -> f p' z (C2 x   c'            )) p c y `mplus`
                            last   (\p' z c' -> f p' z (C1 c'  (fill p c y)  )) x

instance Zipper phi f => Zipper phi (f :>: xi) where
  cmapA  f  p  (CTag prf c)     = liftA (CTag prf) (cmapA f p c)
  fill      p  (CTag prf c)  x  = castTag prf Tag (fill p c x)
  first  f     (Tag x)          = first  (\p z -> f p z . CTag Refl)      x
  last   f     (Tag x)          = last   (\p z -> f p z . CTag Refl)      x
  next   f  p  (CTag prf c)  x  = next   (\p z -> f p z . CTag prf)  p c  x
  prev   f  p  (CTag prf c)  x  = prev   (\p z -> f p z . CTag prf)  p c  x

instance (Constructor c, Zipper phi f) => Zipper phi (C c f) where
  cmapA  f  p  (CC c)           =  liftA CC (cmapA f p c)
  fill      p  (CC c)  x        =  C (fill p c x)
  first  f     (C x)            =  first  (\p z -> f p z . CC)      x
  last   f     (C x)            =  last   (\p z -> f p z . CC)      x
  next   f  p  (CC c)  x        =  next   (\p z -> f p z . CC) p c  x
  prev   f  p  (CC c)  x        =  prev   (\p z -> f p z . CC) p c  x

enter :: Zipper phi f => phi ix -> r ix -> Loc phi f r ix
enter p x = Loc p x Empty

on :: (forall xi. phi xi -> r xi -> a) -> Loc phi f r ix -> a
on f (Loc p x _) = f p x

update :: (forall xi. phi xi -> r xi -> r xi) -> Loc phi f r ix -> Loc phi f r ix
update f (Loc p x s) = Loc p (f p x) s

impossible :: a -> b
impossible _ = error "impossible"

castId   :: (b :=: xi) -> (r xi -> I xi r ix) -> (r b  -> I xi r ix)
castId   Refl = id

castTag  :: (ix :=: xi) -> (f r ix -> (f :>: ix) r ix) -> (f r ix -> (f :>: xi) r ix)
castTag  Refl = id
\end{code}

\section{module Annotations.MultiRec.ZipperFix}

\begin{code}
{-# LANGUAGE RankNTypes #-}

module Annotations.MultiRec.ZipperFix where

import Annotations.MultiRec.Zipper
import Generics.MultiRec.HFix

import Prelude hiding (last)
import Data.Maybe

type FixZipper phi f = Loc phi f (HFix f)

type Nav = forall phi f ix. Zipper phi f => FixZipper phi f ix -> Maybe (FixZipper phi f ix)

down, down', up, right, left :: Nav

down   (Loc p (HIn x) s)        =  first  (\p' z c  -> Loc p' z (Push p c  s)) x
down'  (Loc p (HIn x) s)        =  last   (\p' z c  -> Loc p' z (Push p c  s)) x
up     (Loc p x Empty)          =  Nothing
up     (Loc p x (Push p' c s))  =  return (Loc p' (HIn $ fill p c x) s)
right  (Loc p x Empty)          =  Nothing
right  (Loc p x (Push p' c s))  =  next   (\p z c' -> Loc p z (Push p' c' s)) p c x
left   (Loc p x Empty)          =  Nothing
left   (Loc p x (Push p' c s))  =  prev   (\p z c' -> Loc p z (Push p' c' s)) p c x

df :: (a -> Maybe a) -> (a -> Maybe a) -> (a -> Maybe a) -> a -> Maybe a
df d u lr l =
    case d l of
      Nothing -> df' l
      r       -> r
  where
    df' l =
      case lr l of
        Nothing ->
          case u l of
            Nothing -> Nothing
            Just l' -> df' l'
        r       -> r

dfnext :: Nav
dfnext = df down up right

dfprev :: Nav
dfprev = df down' up left

leave :: Zipper phi f => Loc phi f (HFix f) ix -> HFix f ix
leave (Loc p x Empty) = x
leave loc             = leave (fromJust (up loc))
\end{code}