    module Agda.Utils.Zipper where

    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 (ListZipper a -> ListZipper a -> Bool
    (ListZipper a -> ListZipper a -> Bool)
    -> (ListZipper a -> ListZipper a -> Bool) -> Eq (ListZipper a)
    forall a. Eq a => ListZipper a -> ListZipper a -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: ListZipper a -> ListZipper a -> Bool
    $c/= :: forall a. Eq a => ListZipper a -> ListZipper a -> Bool
    == :: ListZipper a -> ListZipper a -> Bool
    $c== :: forall a. Eq a => ListZipper a -> ListZipper a -> Bool
    Eq, Eq (ListZipper a)
    Eq (ListZipper a)
    -> (ListZipper a -> ListZipper a -> Ordering)
    -> (ListZipper a -> ListZipper a -> Bool)
    -> (ListZipper a -> ListZipper a -> Bool)
    -> (ListZipper a -> ListZipper a -> Bool)
    -> (ListZipper a -> ListZipper a -> Bool)
    -> (ListZipper a -> ListZipper a -> ListZipper a)
    -> (ListZipper a -> ListZipper a -> ListZipper a)
    -> Ord (ListZipper a)
    ListZipper a -> ListZipper a -> Bool
    ListZipper a -> ListZipper a -> Ordering
    ListZipper a -> ListZipper a -> ListZipper a
    forall a.
    Eq a
    -> (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    forall {a}. Ord a => Eq (ListZipper a)
    forall a. Ord a => ListZipper a -> ListZipper a -> Bool
    forall a. Ord a => ListZipper a -> ListZipper a -> Ordering
    forall a. Ord a => ListZipper a -> ListZipper a -> ListZipper a
    min :: ListZipper a -> ListZipper a -> ListZipper a
    $cmin :: forall a. Ord a => ListZipper a -> ListZipper a -> ListZipper a
    max :: ListZipper a -> ListZipper a -> ListZipper a
    $cmax :: forall a. Ord a => ListZipper a -> ListZipper a -> ListZipper a
    >= :: ListZipper a -> ListZipper a -> Bool
    $c>= :: forall a. Ord a => ListZipper a -> ListZipper a -> Bool
    > :: ListZipper a -> ListZipper a -> Bool
    $c> :: forall a. Ord a => ListZipper a -> ListZipper a -> Bool
    <= :: ListZipper a -> ListZipper a -> Bool
    $c<= :: forall a. Ord a => ListZipper a -> ListZipper a -> Bool
    < :: ListZipper a -> ListZipper a -> Bool
    $c< :: forall a. Ord a => ListZipper a -> ListZipper a -> Bool
    compare :: ListZipper a -> ListZipper a -> Ordering
    $ccompare :: forall a. Ord a => ListZipper a -> ListZipper a -> Ordering
    Ord, Int -> ListZipper a -> ShowS
    [ListZipper a] -> ShowS
    ListZipper a -> String
    (Int -> ListZipper a -> ShowS)
    -> (ListZipper a -> String)
    -> ([ListZipper a] -> ShowS)
    -> Show (ListZipper a)
    forall a. Show a => Int -> ListZipper a -> ShowS
    forall a. Show a => [ListZipper a] -> ShowS
    forall a. Show a => ListZipper a -> String
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [ListZipper a] -> ShowS
    $cshowList :: forall a. Show a => [ListZipper a] -> ShowS
    show :: ListZipper a -> String
    $cshow :: forall a. Show a => ListZipper a -> String
    showsPrec :: Int -> ListZipper a -> ShowS
    $cshowsPrec :: forall a. Show a => Int -> ListZipper a -> ShowS
    Show, (forall a b. (a -> b) -> ListZipper a -> ListZipper b)
    -> (forall a b. a -> ListZipper b -> ListZipper a)
    -> Functor ListZipper
    forall a b. a -> ListZipper b -> ListZipper a
    forall a b. (a -> b) -> ListZipper a -> ListZipper b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    <$ :: forall a b. a -> ListZipper b -> ListZipper a
    $c<$ :: forall a b. a -> ListZipper b -> ListZipper a
    fmap :: forall a b. (a -> b) -> ListZipper a -> ListZipper b
    $cfmap :: forall a b. (a -> b) -> ListZipper a -> ListZipper b
    Functor, (forall m. Monoid m => ListZipper m -> m)
    -> (forall m a. Monoid m => (a -> m) -> ListZipper a -> m)
    -> (forall m a. Monoid m => (a -> m) -> ListZipper a -> m)
    -> (forall a b. (a -> b -> b) -> b -> ListZipper a -> b)
    -> (forall a b. (a -> b -> b) -> b -> ListZipper a -> b)
    -> (forall b a. (b -> a -> b) -> b -> ListZipper a -> b)
    -> (forall b a. (b -> a -> b) -> b -> ListZipper a -> b)
    -> (forall a. (a -> a -> a) -> ListZipper a -> a)
    -> (forall a. (a -> a -> a) -> ListZipper a -> a)
    -> (forall a. ListZipper a -> [a])
    -> (forall a. ListZipper a -> Bool)
    -> (forall a. ListZipper a -> Int)
    -> (forall a. Eq a => a -> ListZipper a -> Bool)
    -> (forall a. Ord a => ListZipper a -> a)
    -> (forall a. Ord a => ListZipper a -> a)
    -> (forall a. Num a => ListZipper a -> a)
    -> (forall a. Num a => ListZipper a -> a)
    -> Foldable ListZipper
    forall a. Eq a => a -> ListZipper a -> Bool
    forall a. Num a => ListZipper a -> a
    forall a. Ord a => ListZipper a -> a
    forall m. Monoid m => ListZipper m -> m
    forall a. ListZipper a -> Bool
    forall a. ListZipper a -> Int
    forall a. ListZipper a -> [a]
    forall a. (a -> a -> a) -> ListZipper a -> a
    forall m a. Monoid m => (a -> m) -> ListZipper a -> m
    forall b a. (b -> a -> b) -> b -> ListZipper a -> b
    forall a b. (a -> b -> b) -> b -> ListZipper a -> b
    forall (t :: * -> *).
    (forall m. Monoid m => t m -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. t a -> [a])
    -> (forall a. t a -> Bool)
    -> (forall a. t a -> Int)
    -> (forall a. Eq a => a -> t a -> Bool)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> Foldable t
    product :: forall a. Num a => ListZipper a -> a
    $cproduct :: forall a. Num a => ListZipper a -> a
    sum :: forall a. Num a => ListZipper a -> a
    $csum :: forall a. Num a => ListZipper a -> a
    minimum :: forall a. Ord a => ListZipper a -> a
    $cminimum :: forall a. Ord a => ListZipper a -> a
    maximum :: forall a. Ord a => ListZipper a -> a
    $cmaximum :: forall a. Ord a => ListZipper a -> a
    elem :: forall a. Eq a => a -> ListZipper a -> Bool
    $celem :: forall a. Eq a => a -> ListZipper a -> Bool
    length :: forall a. ListZipper a -> Int
    $clength :: forall a. ListZipper a -> Int
    null :: forall a. ListZipper a -> Bool
    $cnull :: forall a. ListZipper a -> Bool
    toList :: forall a. ListZipper a -> [a]
    $ctoList :: forall a. ListZipper a -> [a]
    foldl1 :: forall a. (a -> a -> a) -> ListZipper a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> ListZipper a -> a
    foldr1 :: forall a. (a -> a -> a) -> ListZipper a -> a
    $cfoldr1 :: forall a. (a -> a -> a) -> ListZipper a -> a
    foldl' :: forall b a. (b -> a -> b) -> b -> ListZipper a -> b
    $cfoldl' :: forall b a. (b -> a -> b) -> b -> ListZipper a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> ListZipper a -> b
    $cfoldl :: forall b a. (b -> a -> b) -> b -> ListZipper a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> ListZipper a -> b
    $cfoldr' :: forall a b. (a -> b -> b) -> b -> ListZipper a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> ListZipper a -> b
    $cfoldr :: forall a b. (a -> b -> b) -> b -> ListZipper a -> b
    foldMap' :: forall m a. Monoid m => (a -> m) -> ListZipper a -> m
    $cfoldMap' :: forall m a. Monoid m => (a -> m) -> ListZipper a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> ListZipper a -> m
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> ListZipper a -> m
    fold :: forall m. Monoid m => ListZipper m -> m
    $cfold :: forall m. Monoid m => ListZipper m -> m
    Foldable, Functor ListZipper
    Foldable ListZipper
    Functor ListZipper
    -> Foldable ListZipper
    -> (forall (f :: * -> *) a b.
        Applicative f =>
        (a -> f b) -> ListZipper a -> f (ListZipper b))
    -> (forall (f :: * -> *) a.
        Applicative f =>
        ListZipper (f a) -> f (ListZipper a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> ListZipper a -> m (ListZipper b))
    -> (forall (m :: * -> *) a.
        Monad m =>
        ListZipper (m a) -> m (ListZipper a))
    -> Traversable ListZipper
    forall (t :: * -> *).
    Functor t
    -> Foldable t
    -> (forall (f :: * -> *) a b.
        Applicative f =>
        (a -> f b) -> t a -> f (t b))
    -> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> t a -> m (t b))
    -> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
    -> Traversable t
    forall (m :: * -> *) a.
    Monad m =>
    ListZipper (m a) -> m (ListZipper a)
    forall (f :: * -> *) a.
    Applicative f =>
    ListZipper (f a) -> f (ListZipper a)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> ListZipper a -> m (ListZipper b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> ListZipper a -> f (ListZipper b)
    sequence :: forall (m :: * -> *) a.
    Monad m =>
    ListZipper (m a) -> m (ListZipper a)
    $csequence :: forall (m :: * -> *) a.
    Monad m =>
    ListZipper (m a) -> m (ListZipper a)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> ListZipper a -> m (ListZipper b)
    $cmapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> ListZipper a -> m (ListZipper b)
    sequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    ListZipper (f a) -> f (ListZipper a)
    $csequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    ListZipper (f a) -> f (ListZipper a)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> ListZipper a -> f (ListZipper b)
    $ctraverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> ListZipper a -> f (ListZipper b)
    Traversable)

    instance Zipper (ListZipper a) where
      type Carrier (ListZipper a) = [a]
      type Element (ListZipper a) = a
      firstHole :: Carrier (ListZipper a)
    -> Maybe (Element (ListZipper a), ListZipper a)
    firstHole (a
    x : [a]
    xs)               = (a, ListZipper a) -> Maybe (a, ListZipper a)
    forall a. a -> Maybe a
    Just (a
    x, [a] -> [a] -> ListZipper a
    forall a. [a] -> [a] -> ListZipper a
    ListZip [] [a]
    xs)
      firstHole []                     = Maybe (Element (ListZipper a), ListZipper a)
    forall a. Maybe a
    Nothing
      plugHole :: Element (ListZipper a) -> ListZipper a -> Carrier (ListZipper a)
    plugHole Element (ListZipper a)
    x (ListZip [a]
    ys [a]
    zs)       = [a] -> [a]
    forall a. [a] -> [a]
    reverse [a]
    ys [a] -> [a] -> [a]
    forall a. [a] -> [a] -> [a]
    ++ a
    Element (ListZipper a)
    x a -> [a] -> [a]
    forall a. a -> [a] -> [a]
    : [a]
    zs
      nextHole :: Element (ListZipper a)
    -> ListZipper a
    -> Either
         (Carrier (ListZipper a)) (Element (ListZipper a), ListZipper a)
    nextHole Element (ListZipper a)
    x (ListZip [a]
    ys [])       = [a] -> Either [a] (a, ListZipper a)
    forall a b. a -> Either a b
    Left ([a] -> [a]
    forall a. [a] -> [a]
    reverse (a
    Element (ListZipper a)
    x a -> [a] -> [a]
    forall a. a -> [a] -> [a]
    : [a]
    ys))
      nextHole Element (ListZipper a)
    x (ListZip [a]
    ys (a
    z : [a]
    zs)) = (a, ListZipper a) -> Either [a] (a, ListZipper a)
    forall a b. b -> Either a b
    Right (a
    z, [a] -> [a] -> ListZipper a
    forall a. [a] -> [a] -> ListZipper a
    ListZip (a
    Element (ListZipper a)
    x a -> [a] -> [a]
    forall a. a -> [a] -> [a]
    : [a]
    ys) [a]
    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 :: Carrier (ComposeZipper f g)
    -> Maybe (Element (ComposeZipper f g), ComposeZipper f g)
    firstHole Carrier (ComposeZipper f g)
    c1 = do
        (Carrier g
    c2, f
    z1) <- Carrier f -> Maybe (Element f, f)
    forall z. Zipper z => Carrier z -> Maybe (Element z, z)
    firstHole Carrier f
    Carrier (ComposeZipper f g)
    c1
        Carrier g -> f -> Maybe (Element g, ComposeZipper f g)
    forall {g} {f}.
    (Zipper g, Zipper f, Element f ~ Carrier g) =>
    Carrier g -> f -> Maybe (Element g, ComposeZipper f g)
    go Carrier g
    c2 f
    z1
        where
          go :: Carrier g -> f -> Maybe (Element g, ComposeZipper f g)
    go Carrier g
    c2 f
    z1 =
            case Carrier g -> Maybe (Element g, g)
    forall z. Zipper z => Carrier z -> Maybe (Element z, z)
    firstHole Carrier g
    c2 of
              Maybe (Element g, g)
    Nothing -> case Element f -> f -> Either (Carrier f) (Element f, f)
    forall z.
    Zipper z =>
    Element z -> z -> Either (Carrier z) (Element z, z)
    nextHole Carrier g
    Element f
    c2 f
    z1 of
                Left{} -> Maybe (Element g, ComposeZipper f g)
    forall a. Maybe a
    Nothing
                Right (Element f
    c2', f
    z1') -> Carrier g -> f -> Maybe (Element g, ComposeZipper f g)
    go Carrier g
    Element f
    c2' f
    z1'
              Just (Element g
    x, g
    z2) -> (Element g, ComposeZipper f g)
    -> Maybe (Element g, ComposeZipper f g)
    forall a. a -> Maybe a
    Just (Element g
    x, f -> g -> ComposeZipper f g
    forall f g. f -> g -> ComposeZipper f g
    ComposeZip f
    z1 g
    z2)
      plugHole :: Element (ComposeZipper f g)
    -> ComposeZipper f g -> Carrier (ComposeZipper f g)
    plugHole Element (ComposeZipper f g)
    x (ComposeZip f
    z1 g
    z2) = Element f -> f -> Carrier f
    forall z. Zipper z => Element z -> z -> Carrier z
    plugHole (Element g -> g -> Carrier g
    forall z. Zipper z => Element z -> z -> Carrier z
    plugHole Element g
    Element (ComposeZipper f g)
    x g
    z2) f
    z1
      nextHole :: Element (ComposeZipper f g)
    -> ComposeZipper f g
    -> Either
         (Carrier (ComposeZipper f g))
         (Element (ComposeZipper f g), ComposeZipper f g)
    nextHole Element (ComposeZipper f g)
    x (ComposeZip f
    z1 g
    z2) =
        case Element g -> g -> Either (Carrier g) (Element g, g)
    forall z.
    Zipper z =>
    Element z -> z -> Either (Carrier z) (Element z, z)
    nextHole Element g
    Element (ComposeZipper f g)
    x g
    z2 of
          Right (Element g
    y, g
    z2') -> (Element g, ComposeZipper f g)
    -> Either (Carrier f) (Element g, ComposeZipper f g)
    forall a b. b -> Either a b
    Right (Element g
    y, f -> g -> ComposeZipper f g
    forall f g. f -> g -> ComposeZipper f g
    ComposeZip f
    z1 g
    z2')
          Left Carrier g
    c2        -> Carrier g -> f -> Either (Carrier f) (Element g, ComposeZipper f g)
    forall {f} {g}.
    (Zipper f, Zipper g, Element f ~ Carrier g) =>
    Carrier g -> f -> Either (Carrier f) (Element g, ComposeZipper f g)
    go Carrier g
    c2 f
    z1
            where
              go :: Carrier g -> f -> Either (Carrier f) (Element g, ComposeZipper f g)
    go Carrier g
    c2 f
    z1 =
                case Element f -> f -> Either (Carrier f) (Element f, f)
    forall z.
    Zipper z =>
    Element z -> z -> Either (Carrier z) (Element z, z)
    nextHole Carrier g
    Element f
    c2 f
    z1 of
                  Right (Element f
    c2', f
    z1') ->
                    case Carrier g -> Maybe (Element g, g)
    forall z. Zipper z => Carrier z -> Maybe (Element z, z)
    firstHole Carrier g
    Element f
    c2' of
                      Maybe (Element g, g)
    Nothing       -> Carrier g -> f -> Either (Carrier f) (Element g, ComposeZipper f g)
    go Carrier g
    Element f
    c2' f
    z1'
                      Just (Element g
    x, g
    z2') -> (Element g, ComposeZipper f g)
    -> Either (Carrier f) (Element g, ComposeZipper f g)
    forall a b. b -> Either a b
    Right (Element g
    x, f -> g -> ComposeZipper f g
    forall f g. f -> g -> ComposeZipper f g
    ComposeZip f
    z1' g
    z2')
                  Left Carrier f
    c1 -> Carrier f -> Either (Carrier f) (Element g, ComposeZipper f g)
    forall a b. a -> Either a b
    Left Carrier f
    c1