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