    {-# LANGUAGE TypeFamilies #-}

    module Agda.Utils.Zipper where

    import Data.Traversable (Traversable)

    class Zipper z where
      type Carrier z
      type Element z
      firstHole :: Carrier z -> Maybe (Element z, z)
      plugHole  :: Element z -> z -> Carrier z
      nextHole  :: Element z -> z -> Either (Carrier z) (Element z, z)

    data ListZipper a = ListZip [a] [a]
      deriving (Eq, Ord, Show, Functor, Foldable, Traversable)

    instance Zipper (ListZipper a) where
      type Carrier (ListZipper a) = [a]
      type Element (ListZipper a) = a
      firstHole (x : xs)               = Just (x, ListZip [] xs)
      firstHole []                     = Nothing
      plugHole x (ListZip ys zs)       = reverse ys ++ x : zs
      nextHole x (ListZip ys [])       = Left (reverse (x : ys))
      nextHole x (ListZip ys (z : zs)) = Right (z, ListZip (x : ys) zs)

    data ComposeZipper f g = ComposeZip f g

    instance (Zipper f, Zipper g, Element f ~ Carrier g) => Zipper (ComposeZipper f g) where
      type Carrier (ComposeZipper f g) = Carrier f
      type Element (ComposeZipper f g) = Element g
      firstHole c1 = do
        (c2, z1) <- firstHole c1
        go c2 z1
        where
          go c2 z1 =
            case firstHole c2 of
              Nothing -> case nextHole c2 z1 of
                Left{} -> Nothing
                Right (c2', z1') -> go c2' z1'
              Just (x, z2) -> Just (x, ComposeZip z1 z2)
      plugHole x (ComposeZip z1 z2) = plugHole (plugHole x z2) z1
      nextHole x (ComposeZip z1 z2) =
        case nextHole x z2 of
          Right (y, z2') -> Right (y, ComposeZip z1 z2')
          Left c2        -> go c2 z1
            where
              go c2 z1 =
                case nextHole c2 z1 of
                  Right (c2', z1') ->
                    case firstHole c2' of
                      Nothing       -> go c2' z1'
                      Just (x, z2') -> Right (x, ComposeZip z1' z2')
                  Left c1 -> Left c1