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