1
2module Agda.Utils.Zipper where
3
4
5class Zipper z where
6  type Carrier z
7  type Element z
8  firstHole :: Carrier z -> Maybe (Element z, z)
9  plugHole  :: Element z -> z -> Carrier z
10  nextHole  :: Element z -> z -> Either (Carrier z) (Element z, z)
11
12data ListZipper a = ListZip [a] [a]
13  deriving (Eq, Ord, Show, Functor, Foldable, Traversable)
14
15instance Zipper (ListZipper a) where
16  type Carrier (ListZipper a) = [a]
17  type Element (ListZipper a) = a
18  firstHole (x : xs)               = Just (x, ListZip [] xs)
19  firstHole []                     = Nothing
20  plugHole x (ListZip ys zs)       = reverse ys ++ x : zs
21  nextHole x (ListZip ys [])       = Left (reverse (x : ys))
22  nextHole x (ListZip ys (z : zs)) = Right (z, ListZip (x : ys) zs)
23
24data ComposeZipper f g = ComposeZip f g
25
26instance (Zipper f, Zipper g, Element f ~ Carrier g) => Zipper (ComposeZipper f g) where
27  type Carrier (ComposeZipper f g) = Carrier f
28  type Element (ComposeZipper f g) = Element g
29  firstHole c1 = do
30    (c2, z1) <- firstHole c1
31    go c2 z1
32    where
33      go c2 z1 =
34        case firstHole c2 of
35          Nothing -> case nextHole c2 z1 of
36            Left{} -> Nothing
37            Right (c2', z1') -> go c2' z1'
38          Just (x, z2) -> Just (x, ComposeZip z1 z2)
39  plugHole x (ComposeZip z1 z2) = plugHole (plugHole x z2) z1
40  nextHole x (ComposeZip z1 z2) =
41    case nextHole x z2 of
42      Right (y, z2') -> Right (y, ComposeZip z1 z2')
43      Left c2        -> go c2 z1
44        where
45          go c2 z1 =
46            case nextHole c2 z1 of
47              Right (c2', z1') ->
48                case firstHole c2' of
49                  Nothing       -> go c2' z1'
50                  Just (x, z2') -> Right (x, ComposeZip z1' z2')
51              Left c1 -> Left c1
52