-- Copyright (C) 2007 David Roundy -- -- This program is free software; you can redistribute it and/or modify -- it under the terms of the GNU General Public License as published by -- the Free Software Foundation; either version 2, or (at your option) -- any later version. -- -- This program is distributed in the hope that it will be useful, -- but WITHOUT ANY WARRANTY; without even the implied warranty of -- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -- GNU General Public License for more details. -- -- You should have received a copy of the GNU General Public License -- along with this program; see the file COPYING. If not, write to -- the Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor, -- Boston, MA 02110-1301, USA. module Darcs.Patch.Witnesses.Ordered ( -- * Directed Types -- $DirectedTypes (:>)(..) , FL(..) , RL(..) -- * Merge Types -- $MergeTypes , (:\/:)(..) , (:/\:)(..) , (:||:)(..) , Fork(..) -- * Functions for 'FL's and 'RL's , nullFL , nullRL , lengthFL , lengthRL , mapFL , mapRL , mapFL_FL , mapRL_RL , foldrFL , foldlRL , foldrwFL , foldlwRL , allFL , allRL , anyFL , anyRL , filterFL , filterRL , foldFL_M , foldRL_M , splitAtFL , splitAtRL , filterOutFLFL , filterOutRLRL , reverseFL , reverseRL , (+>+) , (+<+) , (+>>+) , (+<<+) , concatFL , concatRL , dropWhileFL , dropWhileRL -- * 'FL' only , bunchFL , spanFL , spanFL_M , zipWithFL , toFL , mapFL_FL_M , sequenceFL_ , eqFL , eqFLUnsafe , initsFL -- * 'RL' only , isShorterThanRL , snocRLSealed , spanRL , breakRL , takeWhileRL , concatRLFL ) where import Darcs.Prelude import Darcs.Patch.Witnesses.Show import Darcs.Patch.Witnesses.Sealed ( FlippedSeal(..) , flipSeal , Sealed(..) , FreeLeft , unFreeLeft , Sealed2(..) , seal ) import Darcs.Patch.Witnesses.Eq ( Eq2(..), EqCheck(..) ) -- * Directed Types -- $DirectedTypes -- Darcs patches have a notion of transforming between contexts. This -- naturally leads us to container types that are \"directed\" and -- transform from one context to another. -- -- For example, the swap of names of files x and y could be represented -- with the following sequence of patches: -- -- @ Move x z ':>' Move y x ':>' Move z y @ -- -- or using forward lists, like -- -- @ Move x z ':>:' Move y x ':>:' Move z y ':>:' NilFL @ -- | Directed Forward Pairs data (a1 :> a2) wX wY = forall wZ . (a1 wX wZ) :> (a2 wZ wY) infixr 1 :> -- | Forward lists data FL a wX wZ where (:>:) :: a wX wY -> FL a wY wZ -> FL a wX wZ NilFL :: FL a wX wX -- | Reverse lists data RL a wX wZ where (:<:) :: RL a wX wY -> a wY wZ -> RL a wX wZ NilRL :: RL a wX wX instance Show2 a => Show (FL a wX wZ) where showsPrec :: Int -> FL a wX wZ -> ShowS showsPrec Int _ FL a wX wZ NilFL = String -> ShowS showString String "NilFL" showsPrec Int d (a wX wY x :>: FL a wY wZ xs) = Bool -> ShowS -> ShowS showParen (Int d Int -> Int -> Bool forall a. Ord a => a -> a -> Bool > Int prec) (ShowS -> ShowS) -> ShowS -> ShowS forall a b. (a -> b) -> a -> b $ Int -> a wX wY -> ShowS forall (a :: * -> * -> *) wX wY. Show2 a => Int -> a wX wY -> ShowS showsPrec2 (Int prec Int -> Int -> Int forall a. Num a => a -> a -> a + Int 1) a wX wY x ShowS -> ShowS -> ShowS forall b c a. (b -> c) -> (a -> b) -> a -> c . String -> ShowS showString String " :>: " ShowS -> ShowS -> ShowS forall b c a. (b -> c) -> (a -> b) -> a -> c . Int -> FL a wY wZ -> ShowS forall a. Show a => Int -> a -> ShowS showsPrec (Int prec Int -> Int -> Int forall a. Num a => a -> a -> a + Int 1) FL a wY wZ xs where prec :: Int prec = Int 5 instance Show2 a => Show1 (FL a wX) instance Show2 a => Show2 (FL a) instance Show2 a => Show (RL a wX wZ) where showsPrec :: Int -> RL a wX wZ -> ShowS showsPrec Int _ RL a wX wZ NilRL = String -> ShowS showString String "NilRL" showsPrec Int d (RL a wX wY xs :<: a wY wZ x) = Bool -> ShowS -> ShowS showParen (Int d Int -> Int -> Bool forall a. Ord a => a -> a -> Bool > Int prec) (ShowS -> ShowS) -> ShowS -> ShowS forall a b. (a -> b) -> a -> b $ Int -> RL a wX wY -> ShowS forall a. Show a => Int -> a -> ShowS showsPrec (Int prec Int -> Int -> Int forall a. Num a => a -> a -> a + Int 1) RL a wX wY xs ShowS -> ShowS -> ShowS forall b c a. (b -> c) -> (a -> b) -> a -> c . String -> ShowS showString String " :<: " ShowS -> ShowS -> ShowS forall b c a. (b -> c) -> (a -> b) -> a -> c . Int -> a wY wZ -> ShowS forall (a :: * -> * -> *) wX wY. Show2 a => Int -> a wX wY -> ShowS showsPrec2 (Int prec Int -> Int -> Int forall a. Num a => a -> a -> a + Int 1) a wY wZ x where prec :: Int prec = Int 5 instance Show2 a => Show1 (RL a wX) instance Show2 a => Show2 (RL a) instance (Show2 a, Show2 b) => Show1 ((a :> b) wX) -- * Merge Types -- $MergeTypes -- When we have two patches which commute and share the same pre-context we can -- merge the patches. Whenever patches, or sequences of patches, share a -- pre-context we say they are Forking Pairs (':\/:'). The same way, when -- patches or sequences of patches, share a post-context we say they are -- Joining Pairs (':/\:'). -- -- The following diagram shows the symmetry of merge types: -- -- @ wZ -- ':/\:' -- a3 / \ a4 -- / \ -- wX wY -- \ / -- a1 \ / a2 -- ':\/:' -- wZ -- @ -- -- (non-haddock version) -- wZ -- :/\: -- a3 / \ a4 -- / \ -- wX wY -- \ / -- a1 \ / a2 -- :\/: -- wZ -- infix 1 :/\:, :\/:, :||: -- | Forking Pairs (Implicit starting context) data (a1 :\/: a2) wX wY = forall wZ . (a1 wZ wX) :\/: (a2 wZ wY) -- | Joining Pairs data (a3 :/\: a4) wX wY = forall wZ . (a3 wX wZ) :/\: (a4 wY wZ) -- | Forking Pair (Explicit starting context) -- -- @ wX wY -- \ / -- \ / -- \ / -- wU -- | -- | -- | -- wA -- @ -- -- (non-haddock version) -- -- wX wY -- \ / -- \ / -- \ / -- wU -- | -- | -- | -- wA -- data Fork common left right wA wX wY = forall wU. Fork (common wA wU) (left wU wX) (right wU wY) -- | Parallel Pairs data (a1 :||: a2) wX wY = (a1 wX wY) :||: (a2 wX wY) instance (Show2 a, Show2 b) => Show ( (a :> b) wX wY ) where showsPrec :: Int -> (:>) a b wX wY -> ShowS showsPrec Int d (a wX wZ x :> b wZ wY y) = Int -> String -> Int -> a wX wZ -> b wZ wY -> ShowS forall (a :: * -> * -> *) (b :: * -> * -> *) wW wX wY wZ. (Show2 a, Show2 b) => Int -> String -> Int -> a wW wX -> b wY wZ -> ShowS showOp2 Int 1 String ":>" Int d a wX wZ x b wZ wY y instance (Eq2 a, Eq2 b) => Eq2 (a :> b) where (a wA wZ a1 :> b wZ wB b1) =\/= :: (:>) a b wA wB -> (:>) a b wA wC -> EqCheck wB wC =\/= (a wA wZ a2 :> b wZ wC b2) | EqCheck wZ wZ IsEq <- a wA wZ a1 a wA wZ -> a wA wZ -> EqCheck wZ wZ forall (p :: * -> * -> *) wA wB wC. Eq2 p => p wA wB -> p wA wC -> EqCheck wB wC =\/= a wA wZ a2 = b wZ wB b1 b wZ wB -> b wZ wC -> EqCheck wB wC forall (p :: * -> * -> *) wA wB wC. Eq2 p => p wA wB -> p wA wC -> EqCheck wB wC =\/= b wZ wC b wZ wC b2 | Bool otherwise = EqCheck wB wC forall wA wB. EqCheck wA wB NotEq instance (Eq2 a, Eq2 b) => Eq ((a :> b) wX wY) where == :: (:>) a b wX wY -> (:>) a b wX wY -> Bool (==) = (:>) a b wX wY -> (:>) a b wX wY -> Bool forall (p :: * -> * -> *) wA wB wC wD. Eq2 p => p wA wB -> p wC wD -> Bool unsafeCompare instance (Show2 a, Show2 b) => Show2 (a :> b) instance (Show2 a, Show2 b) => Show ( (a :\/: b) wX wY ) where showsPrec :: Int -> (:\/:) a b wX wY -> ShowS showsPrec Int d (a wZ wX x :\/: b wZ wY y) = Int -> String -> Int -> a wZ wX -> b wZ wY -> ShowS forall (a :: * -> * -> *) (b :: * -> * -> *) wW wX wY wZ. (Show2 a, Show2 b) => Int -> String -> Int -> a wW wX -> b wY wZ -> ShowS showOp2 Int 9 String ":\\/:" Int d a wZ wX x b wZ wY y instance (Show2 a, Show2 b) => Show2 (a :\/: b) instance (Show2 a, Show2 b) => Show ( (a :/\: b) wX wY ) where showsPrec :: Int -> (:/\:) a b wX wY -> ShowS showsPrec Int d (a wX wZ x :/\: b wY wZ y) = Int -> String -> Int -> a wX wZ -> b wY wZ -> ShowS forall (a :: * -> * -> *) (b :: * -> * -> *) wW wX wY wZ. (Show2 a, Show2 b) => Int -> String -> Int -> a wW wX -> b wY wZ -> ShowS showOp2 Int 1 String ":/\\:" Int d a wX wZ x b wY wZ y instance (Show2 a, Show2 b) => Show2 ( (a :/\: b) ) -- * Functions infixr 5 :>:, +>+ infixl 5 :<:, +<+ nullFL :: FL a wX wZ -> Bool nullFL :: FL a wX wZ -> Bool nullFL FL a wX wZ NilFL = Bool True nullFL FL a wX wZ _ = Bool False nullRL :: RL a wX wZ -> Bool nullRL :: RL a wX wZ -> Bool nullRL RL a wX wZ NilRL = Bool True nullRL RL a wX wZ _ = Bool False -- | @filterOutFLFL p xs@ deletes any @x@ in @xs@ for which @p x == IsEq@ -- (indicating that @x@ has no effect as far as we are concerned, and can be -- safely removed from the chain) filterOutFLFL :: (forall wX wY . p wX wY -> EqCheck wX wY) -> FL p wW wZ -> FL p wW wZ filterOutFLFL :: (forall wX wY. p wX wY -> EqCheck wX wY) -> FL p wW wZ -> FL p wW wZ filterOutFLFL forall wX wY. p wX wY -> EqCheck wX wY _ FL p wW wZ NilFL = FL p wW wZ forall (a :: * -> * -> *) wX. FL a wX wX NilFL filterOutFLFL forall wX wY. p wX wY -> EqCheck wX wY f (p wW wY x:>:FL p wY wZ xs) | EqCheck wW wY IsEq <- p wW wY -> EqCheck wW wY forall wX wY. p wX wY -> EqCheck wX wY f p wW wY x = (forall wX wY. p wX wY -> EqCheck wX wY) -> FL p wY wZ -> FL p wY wZ forall (p :: * -> * -> *) wW wZ. (forall wX wY. p wX wY -> EqCheck wX wY) -> FL p wW wZ -> FL p wW wZ filterOutFLFL forall wX wY. p wX wY -> EqCheck wX wY f FL p wY wZ xs | Bool otherwise = p wW wY x p wW wY -> FL p wY wZ -> FL p wW wZ forall (a :: * -> * -> *) wX wY wZ. a wX wY -> FL a wY wZ -> FL a wX wZ :>: (forall wX wY. p wX wY -> EqCheck wX wY) -> FL p wY wZ -> FL p wY wZ forall (p :: * -> * -> *) wW wZ. (forall wX wY. p wX wY -> EqCheck wX wY) -> FL p wW wZ -> FL p wW wZ filterOutFLFL forall wX wY. p wX wY -> EqCheck wX wY f FL p wY wZ xs filterOutRLRL :: (forall wX wY . p wX wY -> EqCheck wX wY) -> RL p wW wZ -> RL p wW wZ filterOutRLRL :: (forall wX wY. p wX wY -> EqCheck wX wY) -> RL p wW wZ -> RL p wW wZ filterOutRLRL forall wX wY. p wX wY -> EqCheck wX wY _ RL p wW wZ NilRL = RL p wW wZ forall (a :: * -> * -> *) wX. RL a wX wX NilRL filterOutRLRL forall wX wY. p wX wY -> EqCheck wX wY f (RL p wW wY xs:<:p wY wZ x) | EqCheck wY wZ IsEq <- p wY wZ -> EqCheck wY wZ forall wX wY. p wX wY -> EqCheck wX wY f p wY wZ x = (forall wX wY. p wX wY -> EqCheck wX wY) -> RL p wW wY -> RL p wW wY forall (p :: * -> * -> *) wW wZ. (forall wX wY. p wX wY -> EqCheck wX wY) -> RL p wW wZ -> RL p wW wZ filterOutRLRL forall wX wY. p wX wY -> EqCheck wX wY f RL p wW wY xs | Bool otherwise = (forall wX wY. p wX wY -> EqCheck wX wY) -> RL p wW wY -> RL p wW wY forall (p :: * -> * -> *) wW wZ. (forall wX wY. p wX wY -> EqCheck wX wY) -> RL p wW wZ -> RL p wW wZ filterOutRLRL forall wX wY. p wX wY -> EqCheck wX wY f RL p wW wY xs RL p wW wY -> p wY wZ -> RL p wW wZ forall (a :: * -> * -> *) wX wY wZ. RL a wX wY -> a wY wZ -> RL a wX wZ :<: p wY wZ x filterRL :: (forall wX wY . p wX wY -> Bool) -> RL p wA wB -> [Sealed2 p] filterRL :: (forall wX wY. p wX wY -> Bool) -> RL p wA wB -> [Sealed2 p] filterRL forall wX wY. p wX wY -> Bool _ RL p wA wB NilRL = [] filterRL forall wX wY. p wX wY -> Bool f (RL p wA wY xs :<: p wY wB x) | p wY wB -> Bool forall wX wY. p wX wY -> Bool f p wY wB x = p wY wB -> Sealed2 p forall (a :: * -> * -> *) wX wY. a wX wY -> Sealed2 a Sealed2 p wY wB x Sealed2 p -> [Sealed2 p] -> [Sealed2 p] forall a. a -> [a] -> [a] : ((forall wX wY. p wX wY -> Bool) -> RL p wA wY -> [Sealed2 p] forall (p :: * -> * -> *) wA wB. (forall wX wY. p wX wY -> Bool) -> RL p wA wB -> [Sealed2 p] filterRL forall wX wY. p wX wY -> Bool f RL p wA wY xs) | Bool otherwise = (forall wX wY. p wX wY -> Bool) -> RL p wA wY -> [Sealed2 p] forall (p :: * -> * -> *) wA wB. (forall wX wY. p wX wY -> Bool) -> RL p wA wB -> [Sealed2 p] filterRL forall wX wY. p wX wY -> Bool f RL p wA wY xs (+>+) :: FL a wX wY -> FL a wY wZ -> FL a wX wZ FL a wX wY NilFL +>+ :: FL a wX wY -> FL a wY wZ -> FL a wX wZ +>+ FL a wY wZ ys = FL a wX wZ FL a wY wZ ys (a wX wY x:>:FL a wY wY xs) +>+ FL a wY wZ ys = a wX wY x a wX wY -> FL a wY wZ -> FL a wX wZ forall (a :: * -> * -> *) wX wY wZ. a wX wY -> FL a wY wZ -> FL a wX wZ :>: FL a wY wY xs FL a wY wY -> FL a wY wZ -> FL a wY wZ forall (a :: * -> * -> *) wX wY wZ. FL a wX wY -> FL a wY wZ -> FL a wX wZ +>+ FL a wY wZ ys (+<+) :: RL a wX wY -> RL a wY wZ -> RL a wX wZ RL a wX wY xs +<+ :: RL a wX wY -> RL a wY wZ -> RL a wX wZ +<+ RL a wY wZ NilRL = RL a wX wY RL a wX wZ xs RL a wX wY xs +<+ (RL a wY wY ys:<:a wY wZ y) = RL a wX wY xs RL a wX wY -> RL a wY wY -> RL a wX wY forall (a :: * -> * -> *) wX wY wZ. RL a wX wY -> RL a wY wZ -> RL a wX wZ +<+ RL a wY wY ys RL a wX wY -> a wY wZ -> RL a wX wZ forall (a :: * -> * -> *) wX wY wZ. RL a wX wY -> a wY wZ -> RL a wX wZ :<: a wY wZ y reverseFL :: FL a wX wZ -> RL a wX wZ reverseFL :: FL a wX wZ -> RL a wX wZ reverseFL FL a wX wZ xs = RL a wX wX -> FL a wX wZ -> RL a wX wZ forall (a :: * -> * -> *) wL wM wO. RL a wL wM -> FL a wM wO -> RL a wL wO r RL a wX wX forall (a :: * -> * -> *) wX. RL a wX wX NilRL FL a wX wZ xs where r :: RL a wL wM -> FL a wM wO -> RL a wL wO r :: RL a wL wM -> FL a wM wO -> RL a wL wO r RL a wL wM ls FL a wM wO NilFL = RL a wL wM RL a wL wO ls r RL a wL wM ls (a wM wY a:>:FL a wY wO as) = RL a wL wY -> FL a wY wO -> RL a wL wO forall (a :: * -> * -> *) wL wM wO. RL a wL wM -> FL a wM wO -> RL a wL wO r (RL a wL wM lsRL a wL wM -> a wM wY -> RL a wL wY forall (a :: * -> * -> *) wX wY wZ. RL a wX wY -> a wY wZ -> RL a wX wZ :<:a wM wY a) FL a wY wO as reverseRL :: RL a wX wZ -> FL a wX wZ reverseRL :: RL a wX wZ -> FL a wX wZ reverseRL RL a wX wZ xs = FL a wZ wZ -> RL a wX wZ -> FL a wX wZ forall (a :: * -> * -> *) wM wO wL. FL a wM wO -> RL a wL wM -> FL a wL wO r FL a wZ wZ forall (a :: * -> * -> *) wX. FL a wX wX NilFL RL a wX wZ xs where r :: FL a wM wO -> RL a wL wM -> FL a wL wO r :: FL a wM wO -> RL a wL wM -> FL a wL wO r FL a wM wO ls RL a wL wM NilRL = FL a wM wO FL a wL wO ls r FL a wM wO ls (RL a wL wY as:<:a wY wM a) = FL a wY wO -> RL a wL wY -> FL a wL wO forall (a :: * -> * -> *) wM wO wL. FL a wM wO -> RL a wL wM -> FL a wL wO r (a wY wM aa wY wM -> FL a wM wO -> FL a wY wO forall (a :: * -> * -> *) wX wY wZ. a wX wY -> FL a wY wZ -> FL a wX wZ :>:FL a wM wO ls) RL a wL wY as concatFL :: FL (FL a) wX wZ -> FL a wX wZ concatFL :: FL (FL a) wX wZ -> FL a wX wZ concatFL FL (FL a) wX wZ NilFL = FL a wX wZ forall (a :: * -> * -> *) wX. FL a wX wX NilFL concatFL (FL a wX wY a:>:FL (FL a) wY wZ as) = FL a wX wY a FL a wX wY -> FL a wY wZ -> FL a wX wZ forall (a :: * -> * -> *) wX wY wZ. FL a wX wY -> FL a wY wZ -> FL a wX wZ +>+ FL (FL a) wY wZ -> FL a wY wZ forall (a :: * -> * -> *) wX wZ. FL (FL a) wX wZ -> FL a wX wZ concatFL FL (FL a) wY wZ as concatRL :: RL (RL a) wX wZ -> RL a wX wZ concatRL :: RL (RL a) wX wZ -> RL a wX wZ concatRL RL (RL a) wX wZ NilRL = RL a wX wZ forall (a :: * -> * -> *) wX. RL a wX wX NilRL concatRL (RL (RL a) wX wY as:<:RL a wY wZ a) = RL (RL a) wX wY -> RL a wX wY forall (a :: * -> * -> *) wX wZ. RL (RL a) wX wZ -> RL a wX wZ concatRL RL (RL a) wX wY as RL a wX wY -> RL a wY wZ -> RL a wX wZ forall (a :: * -> * -> *) wX wY wZ. RL a wX wY -> RL a wY wZ -> RL a wX wZ +<+ RL a wY wZ a spanFL :: (forall wW wY . a wW wY -> Bool) -> FL a wX wZ -> (FL a :> FL a) wX wZ spanFL :: (forall wW wY. a wW wY -> Bool) -> FL a wX wZ -> (:>) (FL a) (FL a) wX wZ spanFL forall wW wY. a wW wY -> Bool f (a wX wY x:>:FL a wY wZ xs) | a wX wY -> Bool forall wW wY. a wW wY -> Bool f a wX wY x = case (forall wW wY. a wW wY -> Bool) -> FL a wY wZ -> (:>) (FL a) (FL a) wY wZ forall (a :: * -> * -> *) wX wZ. (forall wW wY. a wW wY -> Bool) -> FL a wX wZ -> (:>) (FL a) (FL a) wX wZ spanFL forall wW wY. a wW wY -> Bool f FL a wY wZ xs of FL a wY wZ ys :> FL a wZ wZ zs -> (a wX wY xa wX wY -> FL a wY wZ -> FL a wX wZ forall (a :: * -> * -> *) wX wY wZ. a wX wY -> FL a wY wZ -> FL a wX wZ :>:FL a wY wZ ys) FL a wX wZ -> FL a wZ wZ -> (:>) (FL a) (FL a) wX wZ forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> FL a wZ wZ zs spanFL forall wW wY. a wW wY -> Bool _ FL a wX wZ xs = FL a wX wX forall (a :: * -> * -> *) wX. FL a wX wX NilFL FL a wX wX -> FL a wX wZ -> (:>) (FL a) (FL a) wX wZ forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> FL a wX wZ xs spanFL_M :: forall a m wX wZ. Monad m => (forall wW wY . a wW wY -> m Bool) -> FL a wX wZ -> m ((FL a :> FL a) wX wZ) spanFL_M :: (forall wW wY. a wW wY -> m Bool) -> FL a wX wZ -> m ((:>) (FL a) (FL a) wX wZ) spanFL_M forall wW wY. a wW wY -> m Bool f (a wX wY x:>:FL a wY wZ xs) = do Bool continue <- a wX wY -> m Bool forall wW wY. a wW wY -> m Bool f a wX wY x if Bool continue then do (FL a wY wZ ys :> FL a wZ wZ zs) <- (forall wW wY. a wW wY -> m Bool) -> FL a wY wZ -> m ((:>) (FL a) (FL a) wY wZ) forall (a :: * -> * -> *) (m :: * -> *) wX wZ. Monad m => (forall wW wY. a wW wY -> m Bool) -> FL a wX wZ -> m ((:>) (FL a) (FL a) wX wZ) spanFL_M forall wW wY. a wW wY -> m Bool f FL a wY wZ xs (:>) (FL a) (FL a) wX wZ -> m ((:>) (FL a) (FL a) wX wZ) forall (m :: * -> *) a. Monad m => a -> m a return ((:>) (FL a) (FL a) wX wZ -> m ((:>) (FL a) (FL a) wX wZ)) -> (:>) (FL a) (FL a) wX wZ -> m ((:>) (FL a) (FL a) wX wZ) forall a b. (a -> b) -> a -> b $ (a wX wY x a wX wY -> FL a wY wZ -> FL a wX wZ forall (a :: * -> * -> *) wX wY wZ. a wX wY -> FL a wY wZ -> FL a wX wZ :>: FL a wY wZ ys) FL a wX wZ -> FL a wZ wZ -> (:>) (FL a) (FL a) wX wZ forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> FL a wZ wZ zs else (:>) (FL a) (FL a) wX wZ -> m ((:>) (FL a) (FL a) wX wZ) forall (m :: * -> *) a. Monad m => a -> m a return ((:>) (FL a) (FL a) wX wZ -> m ((:>) (FL a) (FL a) wX wZ)) -> (:>) (FL a) (FL a) wX wZ -> m ((:>) (FL a) (FL a) wX wZ) forall a b. (a -> b) -> a -> b $ FL a wX wX forall (a :: * -> * -> *) wX. FL a wX wX NilFL FL a wX wX -> FL a wX wZ -> (:>) (FL a) (FL a) wX wZ forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> (a wX wY x a wX wY -> FL a wY wZ -> FL a wX wZ forall (a :: * -> * -> *) wX wY wZ. a wX wY -> FL a wY wZ -> FL a wX wZ :>: FL a wY wZ xs) spanFL_M forall wW wY. a wW wY -> m Bool _ (FL a wX wZ NilFL) = (:>) (FL a) (FL a) wX wX -> m ((:>) (FL a) (FL a) wX wX) forall (m :: * -> *) a. Monad m => a -> m a return ((:>) (FL a) (FL a) wX wX -> m ((:>) (FL a) (FL a) wX wX)) -> (:>) (FL a) (FL a) wX wX -> m ((:>) (FL a) (FL a) wX wX) forall a b. (a -> b) -> a -> b $ FL a wX wX forall (a :: * -> * -> *) wX. FL a wX wX NilFL FL a wX wX -> FL a wX wX -> (:>) (FL a) (FL a) wX wX forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> FL a wX wX forall (a :: * -> * -> *) wX. FL a wX wX NilFL splitAtFL :: Int -> FL a wX wZ -> (FL a :> FL a) wX wZ splitAtFL :: Int -> FL a wX wZ -> (:>) (FL a) (FL a) wX wZ splitAtFL Int 0 FL a wX wZ xs = FL a wX wX forall (a :: * -> * -> *) wX. FL a wX wX NilFL FL a wX wX -> FL a wX wZ -> (:>) (FL a) (FL a) wX wZ forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> FL a wX wZ xs splitAtFL Int _ FL a wX wZ NilFL = FL a wX wX forall (a :: * -> * -> *) wX. FL a wX wX NilFL FL a wX wX -> FL a wX wX -> (:>) (FL a) (FL a) wX wX forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> FL a wX wX forall (a :: * -> * -> *) wX. FL a wX wX NilFL splitAtFL Int n (a wX wY x:>:FL a wY wZ xs) = case Int -> FL a wY wZ -> (:>) (FL a) (FL a) wY wZ forall (a :: * -> * -> *) wX wZ. Int -> FL a wX wZ -> (:>) (FL a) (FL a) wX wZ splitAtFL (Int nInt -> Int -> Int forall a. Num a => a -> a -> a -Int 1) FL a wY wZ xs of (FL a wY wZ xs':>FL a wZ wZ xs'') -> (a wX wY xa wX wY -> FL a wY wZ -> FL a wX wZ forall (a :: * -> * -> *) wX wY wZ. a wX wY -> FL a wY wZ -> FL a wX wZ :>:FL a wY wZ xs' FL a wX wZ -> FL a wZ wZ -> (:>) (FL a) (FL a) wX wZ forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> FL a wZ wZ xs'') splitAtRL :: Int -> RL a wX wZ -> (RL a :> RL a) wX wZ splitAtRL :: Int -> RL a wX wZ -> (:>) (RL a) (RL a) wX wZ splitAtRL Int 0 RL a wX wZ xs = RL a wX wZ xs RL a wX wZ -> RL a wZ wZ -> (:>) (RL a) (RL a) wX wZ forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> RL a wZ wZ forall (a :: * -> * -> *) wX. RL a wX wX NilRL splitAtRL Int _ RL a wX wZ NilRL = RL a wX wX forall (a :: * -> * -> *) wX. RL a wX wX NilRL RL a wX wX -> RL a wX wX -> (:>) (RL a) (RL a) wX wX forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> RL a wX wX forall (a :: * -> * -> *) wX. RL a wX wX NilRL splitAtRL Int n (RL a wX wY xs:<:a wY wZ x) = case Int -> RL a wX wY -> (:>) (RL a) (RL a) wX wY forall (a :: * -> * -> *) wX wZ. Int -> RL a wX wZ -> (:>) (RL a) (RL a) wX wZ splitAtRL (Int nInt -> Int -> Int forall a. Num a => a -> a -> a -Int 1) RL a wX wY xs of (RL a wX wZ xs'':>RL a wZ wY xs') -> (RL a wX wZ xs''RL a wX wZ -> RL a wZ wZ -> (:>) (RL a) (RL a) wX wZ forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> RL a wZ wY xs'RL a wZ wY -> a wY wZ -> RL a wZ wZ forall (a :: * -> * -> *) wX wY wZ. RL a wX wY -> a wY wZ -> RL a wX wZ :<:a wY wZ x) -- 'bunchFL n' groups patches into batches of n, except that it always puts -- the first patch in its own group, this being a recognition that the -- first patch is often *very* large. bunchFL :: Int -> FL a wX wY -> FL (FL a) wX wY bunchFL :: Int -> FL a wX wY -> FL (FL a) wX wY bunchFL Int _ FL a wX wY NilFL = FL (FL a) wX wY forall (a :: * -> * -> *) wX. FL a wX wX NilFL bunchFL Int n (a wX wY x:>:FL a wY wY xs) = (a wX wY x a wX wY -> FL a wY wY -> FL a wX wY forall (a :: * -> * -> *) wX wY wZ. a wX wY -> FL a wY wZ -> FL a wX wZ :>: FL a wY wY forall (a :: * -> * -> *) wX. FL a wX wX NilFL) FL a wX wY -> FL (FL a) wY wY -> FL (FL a) wX wY forall (a :: * -> * -> *) wX wY wZ. a wX wY -> FL a wY wZ -> FL a wX wZ :>: FL a wY wY -> FL (FL a) wY wY forall (a :: * -> * -> *) wX wY. FL a wX wY -> FL (FL a) wX wY bFL FL a wY wY xs where bFL :: FL a wX wY -> FL (FL a) wX wY bFL :: FL a wX wY -> FL (FL a) wX wY bFL FL a wX wY NilFL = FL (FL a) wX wY forall (a :: * -> * -> *) wX. FL a wX wX NilFL bFL FL a wX wY bs = case Int -> FL a wX wY -> (:>) (FL a) (FL a) wX wY forall (a :: * -> * -> *) wX wZ. Int -> FL a wX wZ -> (:>) (FL a) (FL a) wX wZ splitAtFL Int n FL a wX wY bs of FL a wX wZ a :> FL a wZ wY b -> FL a wX wZ a FL a wX wZ -> FL (FL a) wZ wY -> FL (FL a) wX wY forall (a :: * -> * -> *) wX wY wZ. a wX wY -> FL a wY wZ -> FL a wX wZ :>: FL a wZ wY -> FL (FL a) wZ wY forall (a :: * -> * -> *) wX wY. FL a wX wY -> FL (FL a) wX wY bFL FL a wZ wY b -- | Monadic fold over an 'FL' associating to the left, sequencing -- effects from left to right. -- The order of arguments follows the standard 'foldM' from base. foldFL_M :: Monad m => (forall wA wB. r wA -> p wA wB -> m (r wB)) -> r wX -> FL p wX wY -> m (r wY) foldFL_M :: (forall wA wB. r wA -> p wA wB -> m (r wB)) -> r wX -> FL p wX wY -> m (r wY) foldFL_M forall wA wB. r wA -> p wA wB -> m (r wB) _ r wX r FL p wX wY NilFL = r wX -> m (r wX) forall (m :: * -> *) a. Monad m => a -> m a return r wX r foldFL_M forall wA wB. r wA -> p wA wB -> m (r wB) f r wX r (p wX wY x :>: FL p wY wY xs) = r wX -> p wX wY -> m (r wY) forall wA wB. r wA -> p wA wB -> m (r wB) f r wX r p wX wY x m (r wY) -> (r wY -> m (r wY)) -> m (r wY) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b >>= \r wY r' -> (forall wA wB. r wA -> p wA wB -> m (r wB)) -> r wY -> FL p wY wY -> m (r wY) forall (m :: * -> *) (r :: * -> *) (p :: * -> * -> *) wX wY. Monad m => (forall wA wB. r wA -> p wA wB -> m (r wB)) -> r wX -> FL p wX wY -> m (r wY) foldFL_M forall wA wB. r wA -> p wA wB -> m (r wB) f r wY r' FL p wY wY xs -- | Monadic fold over an 'FL' associating to the right, sequencing -- effects from right to left. -- Mostly useful for prepend-like operations with an effect where the -- order of effects is not relevant. foldRL_M :: Monad m => (forall wA wB. p wA wB -> r wB -> m (r wA)) -> RL p wX wY -> r wY -> m (r wX) foldRL_M :: (forall wA wB. p wA wB -> r wB -> m (r wA)) -> RL p wX wY -> r wY -> m (r wX) foldRL_M forall wA wB. p wA wB -> r wB -> m (r wA) _ RL p wX wY NilRL r wY r = r wY -> m (r wY) forall (m :: * -> *) a. Monad m => a -> m a return r wY r foldRL_M forall wA wB. p wA wB -> r wB -> m (r wA) f (RL p wX wY xs :<: p wY wY x) r wY r = p wY wY -> r wY -> m (r wY) forall wA wB. p wA wB -> r wB -> m (r wA) f p wY wY x r wY r m (r wY) -> (r wY -> m (r wX)) -> m (r wX) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b >>= (forall wA wB. p wA wB -> r wB -> m (r wA)) -> RL p wX wY -> r wY -> m (r wX) forall (m :: * -> *) (p :: * -> * -> *) (r :: * -> *) wX wY. Monad m => (forall wA wB. p wA wB -> r wB -> m (r wA)) -> RL p wX wY -> r wY -> m (r wX) foldRL_M forall wA wB. p wA wB -> r wB -> m (r wA) f RL p wX wY xs allFL :: (forall wX wY . a wX wY -> Bool) -> FL a wW wZ -> Bool allFL :: (forall wX wY. a wX wY -> Bool) -> FL a wW wZ -> Bool allFL forall wX wY. a wX wY -> Bool f FL a wW wZ xs = [Bool] -> Bool forall (t :: * -> *). Foldable t => t Bool -> Bool and ([Bool] -> Bool) -> [Bool] -> Bool forall a b. (a -> b) -> a -> b $ (forall wX wY. a wX wY -> Bool) -> FL a wW wZ -> [Bool] forall (a :: * -> * -> *) b wX wY. (forall wW wZ. a wW wZ -> b) -> FL a wX wY -> [b] mapFL forall wX wY. a wX wY -> Bool f FL a wW wZ xs anyFL :: (forall wX wY . a wX wY -> Bool) -> FL a wW wZ -> Bool anyFL :: (forall wX wY. a wX wY -> Bool) -> FL a wW wZ -> Bool anyFL forall wX wY. a wX wY -> Bool f FL a wW wZ xs = [Bool] -> Bool forall (t :: * -> *). Foldable t => t Bool -> Bool or ([Bool] -> Bool) -> [Bool] -> Bool forall a b. (a -> b) -> a -> b $ (forall wX wY. a wX wY -> Bool) -> FL a wW wZ -> [Bool] forall (a :: * -> * -> *) b wX wY. (forall wW wZ. a wW wZ -> b) -> FL a wX wY -> [b] mapFL forall wX wY. a wX wY -> Bool f FL a wW wZ xs allRL :: (forall wA wB . a wA wB -> Bool) -> RL a wX wY -> Bool allRL :: (forall wA wB. a wA wB -> Bool) -> RL a wX wY -> Bool allRL forall wA wB. a wA wB -> Bool f RL a wX wY xs = [Bool] -> Bool forall (t :: * -> *). Foldable t => t Bool -> Bool and ([Bool] -> Bool) -> [Bool] -> Bool forall a b. (a -> b) -> a -> b $ (forall wA wB. a wA wB -> Bool) -> RL a wX wY -> [Bool] forall (a :: * -> * -> *) b wX wY. (forall wW wZ. a wW wZ -> b) -> RL a wX wY -> [b] mapRL forall wA wB. a wA wB -> Bool f RL a wX wY xs anyRL :: (forall wA wB . a wA wB -> Bool) -> RL a wX wY -> Bool anyRL :: (forall wA wB. a wA wB -> Bool) -> RL a wX wY -> Bool anyRL forall wA wB. a wA wB -> Bool f RL a wX wY xs = [Bool] -> Bool forall (t :: * -> *). Foldable t => t Bool -> Bool or ([Bool] -> Bool) -> [Bool] -> Bool forall a b. (a -> b) -> a -> b $ (forall wA wB. a wA wB -> Bool) -> RL a wX wY -> [Bool] forall (a :: * -> * -> *) b wX wY. (forall wW wZ. a wW wZ -> b) -> RL a wX wY -> [b] mapRL forall wA wB. a wA wB -> Bool f RL a wX wY xs -- | The "natural" fold over an 'FL' i.e. associating to the right. -- Like 'Prelude.foldr' only with the more useful order of arguments. foldrFL :: (forall wA wB . p wA wB -> r -> r) -> FL p wX wY -> r -> r foldrFL :: (forall wA wB. p wA wB -> r -> r) -> FL p wX wY -> r -> r foldrFL forall wA wB. p wA wB -> r -> r _ FL p wX wY NilFL r r = r r foldrFL forall wA wB. p wA wB -> r -> r f (p wX wY p:>:FL p wY wY ps) r r = p wX wY -> r -> r forall wA wB. p wA wB -> r -> r f p wX wY p ((forall wA wB. p wA wB -> r -> r) -> FL p wY wY -> r -> r forall (p :: * -> * -> *) r wX wY. (forall wA wB. p wA wB -> r -> r) -> FL p wX wY -> r -> r foldrFL forall wA wB. p wA wB -> r -> r f FL p wY wY ps r r) -- | The "natural" fold over an RL i.e. associating to the left. foldlRL :: (forall wA wB . r -> p wA wB -> r) -> r -> RL p wX wY -> r foldlRL :: (forall wA wB. r -> p wA wB -> r) -> r -> RL p wX wY -> r foldlRL forall wA wB. r -> p wA wB -> r _ r r RL p wX wY NilRL = r r foldlRL forall wA wB. r -> p wA wB -> r f r r (RL p wX wY ps:<:p wY wY p) = r -> p wY wY -> r forall wA wB. r -> p wA wB -> r f ((forall wA wB. r -> p wA wB -> r) -> r -> RL p wX wY -> r forall r (p :: * -> * -> *) wX wY. (forall wA wB. r -> p wA wB -> r) -> r -> RL p wX wY -> r foldlRL forall wA wB. r -> p wA wB -> r f r r RL p wX wY ps) p wY wY p -- | Right associative fold for 'FL's that transforms a witnessed state -- in the direction opposite to the 'FL'. -- This is the "natural" fold for 'FL's i.e. the one which replaces the -- ':>:' with the passed operator. foldrwFL :: (forall wA wB . p wA wB -> r wB -> r wA) -> FL p wX wY -> r wY -> r wX foldrwFL :: (forall wA wB. p wA wB -> r wB -> r wA) -> FL p wX wY -> r wY -> r wX foldrwFL forall wA wB. p wA wB -> r wB -> r wA _ FL p wX wY NilFL r wY r = r wX r wY r foldrwFL forall wA wB. p wA wB -> r wB -> r wA f (p wX wY p:>:FL p wY wY ps) r wY r = p wX wY -> r wY -> r wX forall wA wB. p wA wB -> r wB -> r wA f p wX wY p ((forall wA wB. p wA wB -> r wB -> r wA) -> FL p wY wY -> r wY -> r wY forall (p :: * -> * -> *) (r :: * -> *) wX wY. (forall wA wB. p wA wB -> r wB -> r wA) -> FL p wX wY -> r wY -> r wX foldrwFL forall wA wB. p wA wB -> r wB -> r wA f FL p wY wY ps r wY r) -- | The analog of 'foldrwFL' for 'RL's. -- This is the "natural" fold for 'RL's i.e. the one which replaces the -- ':<:' with the passed operator. foldlwRL :: (forall wA wB . r wA -> p wA wB -> r wB) -> r wX -> RL p wX wY -> r wY foldlwRL :: (forall wA wB. r wA -> p wA wB -> r wB) -> r wX -> RL p wX wY -> r wY foldlwRL forall wA wB. r wA -> p wA wB -> r wB _ r wX r RL p wX wY NilRL = r wX r wY r foldlwRL forall wA wB. r wA -> p wA wB -> r wB f r wX r (RL p wX wY ps:<:p wY wY p) = r wY -> p wY wY -> r wY forall wA wB. r wA -> p wA wB -> r wB f ((forall wA wB. r wA -> p wA wB -> r wB) -> r wX -> RL p wX wY -> r wY forall (r :: * -> *) (p :: * -> * -> *) wX wY. (forall wA wB. r wA -> p wA wB -> r wB) -> r wX -> RL p wX wY -> r wY foldlwRL forall wA wB. r wA -> p wA wB -> r wB f r wX r RL p wX wY ps) p wY wY p mapFL_FL :: (forall wW wY . a wW wY -> b wW wY) -> FL a wX wZ -> FL b wX wZ mapFL_FL :: (forall wW wY. a wW wY -> b wW wY) -> FL a wX wZ -> FL b wX wZ mapFL_FL forall wW wY. a wW wY -> b wW wY _ FL a wX wZ NilFL = FL b wX wZ forall (a :: * -> * -> *) wX. FL a wX wX NilFL mapFL_FL forall wW wY. a wW wY -> b wW wY f (a wX wY a:>:FL a wY wZ as) = a wX wY -> b wX wY forall wW wY. a wW wY -> b wW wY f a wX wY a b wX wY -> FL b wY wZ -> FL b wX wZ forall (a :: * -> * -> *) wX wY wZ. a wX wY -> FL a wY wZ -> FL a wX wZ :>: (forall wW wY. a wW wY -> b wW wY) -> FL a wY wZ -> FL b wY wZ forall (a :: * -> * -> *) (b :: * -> * -> *) wX wZ. (forall wW wY. a wW wY -> b wW wY) -> FL a wX wZ -> FL b wX wZ mapFL_FL forall wW wY. a wW wY -> b wW wY f FL a wY wZ as mapFL_FL_M :: Monad m => (forall wW wY . a wW wY -> m (b wW wY)) -> FL a wX wZ -> m (FL b wX wZ) mapFL_FL_M :: (forall wW wY. a wW wY -> m (b wW wY)) -> FL a wX wZ -> m (FL b wX wZ) mapFL_FL_M forall wW wY. a wW wY -> m (b wW wY) _ FL a wX wZ NilFL = FL b wX wX -> m (FL b wX wX) forall (m :: * -> *) a. Monad m => a -> m a return FL b wX wX forall (a :: * -> * -> *) wX. FL a wX wX NilFL mapFL_FL_M forall wW wY. a wW wY -> m (b wW wY) f (a wX wY a:>:FL a wY wZ as) = do b wX wY b <- a wX wY -> m (b wX wY) forall wW wY. a wW wY -> m (b wW wY) f a wX wY a FL b wY wZ bs <- (forall wW wY. a wW wY -> m (b wW wY)) -> FL a wY wZ -> m (FL b wY wZ) forall (m :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) wX wZ. Monad m => (forall wW wY. a wW wY -> m (b wW wY)) -> FL a wX wZ -> m (FL b wX wZ) mapFL_FL_M forall wW wY. a wW wY -> m (b wW wY) f FL a wY wZ as FL b wX wZ -> m (FL b wX wZ) forall (m :: * -> *) a. Monad m => a -> m a return (b wX wY bb wX wY -> FL b wY wZ -> FL b wX wZ forall (a :: * -> * -> *) wX wY wZ. a wX wY -> FL a wY wZ -> FL a wX wZ :>:FL b wY wZ bs) sequenceFL_ :: Monad m => (forall wW wZ . a wW wZ -> m b) -> FL a wX wY -> m () sequenceFL_ :: (forall wW wZ. a wW wZ -> m b) -> FL a wX wY -> m () sequenceFL_ forall wW wZ. a wW wZ -> m b f = [m b] -> m () forall (t :: * -> *) (m :: * -> *) a. (Foldable t, Monad m) => t (m a) -> m () sequence_ ([m b] -> m ()) -> (FL a wX wY -> [m b]) -> FL a wX wY -> m () forall b c a. (b -> c) -> (a -> b) -> a -> c . (forall wW wZ. a wW wZ -> m b) -> FL a wX wY -> [m b] forall (a :: * -> * -> *) b wX wY. (forall wW wZ. a wW wZ -> b) -> FL a wX wY -> [b] mapFL forall wW wZ. a wW wZ -> m b f zipWithFL :: (forall wX wY . a -> p wX wY -> q wX wY) -> [a] -> FL p wW wZ -> FL q wW wZ zipWithFL :: (forall wX wY. a -> p wX wY -> q wX wY) -> [a] -> FL p wW wZ -> FL q wW wZ zipWithFL forall wX wY. a -> p wX wY -> q wX wY f (a x:[a] xs) (p wW wY y :>: FL p wY wZ ys) = a -> p wW wY -> q wW wY forall wX wY. a -> p wX wY -> q wX wY f a x p wW wY y q wW wY -> FL q wY wZ -> FL q wW wZ forall (a :: * -> * -> *) wX wY wZ. a wX wY -> FL a wY wZ -> FL a wX wZ :>: (forall wX wY. a -> p wX wY -> q wX wY) -> [a] -> FL p wY wZ -> FL q wY wZ forall a (p :: * -> * -> *) (q :: * -> * -> *) wW wZ. (forall wX wY. a -> p wX wY -> q wX wY) -> [a] -> FL p wW wZ -> FL q wW wZ zipWithFL forall wX wY. a -> p wX wY -> q wX wY f [a] xs FL p wY wZ ys zipWithFL forall wX wY. a -> p wX wY -> q wX wY _ [a] _ FL p wW wZ NilFL = FL q wW wZ forall (a :: * -> * -> *) wX. FL a wX wX NilFL zipWithFL forall wX wY. a -> p wX wY -> q wX wY _ [] (p wW wY _:>:FL p wY wZ _) = String -> FL q wW wZ forall a. HasCallStack => String -> a error String "zipWithFL called with too short a list" mapRL_RL :: (forall wW wY . a wW wY -> b wW wY) -> RL a wX wZ -> RL b wX wZ mapRL_RL :: (forall wW wY. a wW wY -> b wW wY) -> RL a wX wZ -> RL b wX wZ mapRL_RL forall wW wY. a wW wY -> b wW wY _ RL a wX wZ NilRL = RL b wX wZ forall (a :: * -> * -> *) wX. RL a wX wX NilRL mapRL_RL forall wW wY. a wW wY -> b wW wY f (RL a wX wY as:<:a wY wZ a) = (forall wW wY. a wW wY -> b wW wY) -> RL a wX wY -> RL b wX wY forall (a :: * -> * -> *) (b :: * -> * -> *) wX wZ. (forall wW wY. a wW wY -> b wW wY) -> RL a wX wZ -> RL b wX wZ mapRL_RL forall wW wY. a wW wY -> b wW wY f RL a wX wY as RL b wX wY -> b wY wZ -> RL b wX wZ forall (a :: * -> * -> *) wX wY wZ. RL a wX wY -> a wY wZ -> RL a wX wZ :<: a wY wZ -> b wY wZ forall wW wY. a wW wY -> b wW wY f a wY wZ a {-# INLINABLE mapFL #-} mapFL :: (forall wW wZ . a wW wZ -> b) -> FL a wX wY -> [b] mapFL :: (forall wW wZ. a wW wZ -> b) -> FL a wX wY -> [b] mapFL forall wW wZ. a wW wZ -> b _ FL a wX wY NilFL = [] mapFL forall wW wZ. a wW wZ -> b f (a wX wY a :>: FL a wY wY b) = a wX wY -> b forall wW wZ. a wW wZ -> b f a wX wY a b -> [b] -> [b] forall a. a -> [a] -> [a] : (forall wW wZ. a wW wZ -> b) -> FL a wY wY -> [b] forall (a :: * -> * -> *) b wX wY. (forall wW wZ. a wW wZ -> b) -> FL a wX wY -> [b] mapFL forall wW wZ. a wW wZ -> b f FL a wY wY b filterFL :: (forall wX wY . a wX wY -> Bool) -> FL a wW wZ -> [Sealed2 a] filterFL :: (forall wX wY. a wX wY -> Bool) -> FL a wW wZ -> [Sealed2 a] filterFL forall wX wY. a wX wY -> Bool _ FL a wW wZ NilFL = [] filterFL forall wX wY. a wX wY -> Bool f (a wW wY a :>: FL a wY wZ b) = if a wW wY -> Bool forall wX wY. a wX wY -> Bool f a wW wY a then (a wW wY -> Sealed2 a forall (a :: * -> * -> *) wX wY. a wX wY -> Sealed2 a Sealed2 a wW wY a)Sealed2 a -> [Sealed2 a] -> [Sealed2 a] forall a. a -> [a] -> [a] :((forall wX wY. a wX wY -> Bool) -> FL a wY wZ -> [Sealed2 a] forall (a :: * -> * -> *) wW wZ. (forall wX wY. a wX wY -> Bool) -> FL a wW wZ -> [Sealed2 a] filterFL forall wX wY. a wX wY -> Bool f FL a wY wZ b) else (forall wX wY. a wX wY -> Bool) -> FL a wY wZ -> [Sealed2 a] forall (a :: * -> * -> *) wW wZ. (forall wX wY. a wX wY -> Bool) -> FL a wW wZ -> [Sealed2 a] filterFL forall wX wY. a wX wY -> Bool f FL a wY wZ b mapRL :: (forall wW wZ . a wW wZ -> b) -> RL a wX wY -> [b] mapRL :: (forall wW wZ. a wW wZ -> b) -> RL a wX wY -> [b] mapRL forall wW wZ. a wW wZ -> b _ RL a wX wY NilRL = [] mapRL forall wW wZ. a wW wZ -> b f (RL a wX wY as :<: a wY wY a) = a wY wY -> b forall wW wZ. a wW wZ -> b f a wY wY a b -> [b] -> [b] forall a. a -> [a] -> [a] : (forall wW wZ. a wW wZ -> b) -> RL a wX wY -> [b] forall (a :: * -> * -> *) b wX wY. (forall wW wZ. a wW wZ -> b) -> RL a wX wY -> [b] mapRL forall wW wZ. a wW wZ -> b f RL a wX wY as lengthFL :: FL a wX wZ -> Int lengthFL :: FL a wX wZ -> Int lengthFL FL a wX wZ xs = FL a wX wZ -> Int -> Int forall (a :: * -> * -> *) wX wZ. FL a wX wZ -> Int -> Int l FL a wX wZ xs Int 0 where l :: FL a wX wZ -> Int -> Int l :: FL a wX wZ -> Int -> Int l FL a wX wZ NilFL Int n = Int n l (a wX wY _:>:FL a wY wZ as) Int n = FL a wY wZ -> Int -> Int forall (a :: * -> * -> *) wX wZ. FL a wX wZ -> Int -> Int l FL a wY wZ as (Int -> Int) -> Int -> Int forall a b. (a -> b) -> a -> b $! Int nInt -> Int -> Int forall a. Num a => a -> a -> a +Int 1 lengthRL :: RL a wX wZ -> Int lengthRL :: RL a wX wZ -> Int lengthRL RL a wX wZ xs = RL a wX wZ -> Int -> Int forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> Int -> Int l RL a wX wZ xs Int 0 where l :: RL a wX wZ -> Int -> Int l :: RL a wX wZ -> Int -> Int l RL a wX wZ NilRL Int n = Int n l (RL a wX wY as:<:a wY wZ _) Int n = RL a wX wY -> Int -> Int forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> Int -> Int l RL a wX wY as (Int -> Int) -> Int -> Int forall a b. (a -> b) -> a -> b $! Int nInt -> Int -> Int forall a. Num a => a -> a -> a +Int 1 isShorterThanRL :: RL a wX wY -> Int -> Bool isShorterThanRL :: RL a wX wY -> Int -> Bool isShorterThanRL RL a wX wY _ Int n | Int n Int -> Int -> Bool forall a. Ord a => a -> a -> Bool <= Int 0 = Bool False isShorterThanRL RL a wX wY NilRL Int _ = Bool True isShorterThanRL (RL a wX wY xs:<:a wY wY _) Int n = RL a wX wY -> Int -> Bool forall (a :: * -> * -> *) wX wY. RL a wX wY -> Int -> Bool isShorterThanRL RL a wX wY xs (Int nInt -> Int -> Int forall a. Num a => a -> a -> a -Int 1) snocRLSealed :: FlippedSeal (RL a) wY -> a wY wZ -> FlippedSeal (RL a) wZ snocRLSealed :: FlippedSeal (RL a) wY -> a wY wZ -> FlippedSeal (RL a) wZ snocRLSealed (FlippedSeal RL a wX wY as) a wY wZ a = RL a wX wZ -> FlippedSeal (RL a) wZ forall (a :: * -> * -> *) wX wY. a wX wY -> FlippedSeal a wY flipSeal (RL a wX wZ -> FlippedSeal (RL a) wZ) -> RL a wX wZ -> FlippedSeal (RL a) wZ forall a b. (a -> b) -> a -> b $ RL a wX wY as RL a wX wY -> a wY wZ -> RL a wX wZ forall (a :: * -> * -> *) wX wY wZ. RL a wX wY -> a wY wZ -> RL a wX wZ :<: a wY wZ a toFL :: [FreeLeft a] -> Sealed (FL a wX) toFL :: [FreeLeft a] -> Sealed (FL a wX) toFL [] = FL a wX wX -> Sealed (FL a wX) forall (a :: * -> *) wX. a wX -> Sealed a Sealed FL a wX wX forall (a :: * -> * -> *) wX. FL a wX wX NilFL toFL (FreeLeft a x:[FreeLeft a] xs) = case FreeLeft a -> Sealed (a wX) forall (p :: * -> * -> *) wX. FreeLeft p -> Sealed (p wX) unFreeLeft FreeLeft a x of Sealed a wX wX y -> case [FreeLeft a] -> Sealed (FL a wX) forall (a :: * -> * -> *) wX. [FreeLeft a] -> Sealed (FL a wX) toFL [FreeLeft a] xs of Sealed FL a wX wX ys -> FL a wX wX -> Sealed (FL a wX) forall (a :: * -> *) wX. a wX -> Sealed a Sealed (a wX wX y a wX wX -> FL a wX wX -> FL a wX wX forall (a :: * -> * -> *) wX wY wZ. a wX wY -> FL a wY wZ -> FL a wX wZ :>: FL a wX wX ys) dropWhileFL :: (forall wX wY . a wX wY -> Bool) -> FL a wR wV -> FlippedSeal (FL a) wV dropWhileFL :: (forall wX wY. a wX wY -> Bool) -> FL a wR wV -> FlippedSeal (FL a) wV dropWhileFL forall wX wY. a wX wY -> Bool _ FL a wR wV NilFL = FL a wV wV -> FlippedSeal (FL a) wV forall (a :: * -> * -> *) wX wY. a wX wY -> FlippedSeal a wY flipSeal FL a wV wV forall (a :: * -> * -> *) wX. FL a wX wX NilFL dropWhileFL forall wX wY. a wX wY -> Bool p xs :: FL a wR wV xs@(a wR wY x:>:FL a wY wV xs') | a wR wY -> Bool forall wX wY. a wX wY -> Bool p a wR wY x = (forall wX wY. a wX wY -> Bool) -> FL a wY wV -> FlippedSeal (FL a) wV forall (a :: * -> * -> *) wR wV. (forall wX wY. a wX wY -> Bool) -> FL a wR wV -> FlippedSeal (FL a) wV dropWhileFL forall wX wY. a wX wY -> Bool p FL a wY wV xs' | Bool otherwise = FL a wR wV -> FlippedSeal (FL a) wV forall (a :: * -> * -> *) wX wY. a wX wY -> FlippedSeal a wY flipSeal FL a wR wV xs dropWhileRL :: (forall wX wY . a wX wY -> Bool) -> RL a wR wV -> Sealed (RL a wR) dropWhileRL :: (forall wX wY. a wX wY -> Bool) -> RL a wR wV -> Sealed (RL a wR) dropWhileRL forall wX wY. a wX wY -> Bool _ RL a wR wV NilRL = RL a wR wR -> Sealed (RL a wR) forall (a :: * -> *) wX. a wX -> Sealed a seal RL a wR wR forall (a :: * -> * -> *) wX. RL a wX wX NilRL dropWhileRL forall wX wY. a wX wY -> Bool p xs :: RL a wR wV xs@(RL a wR wY xs':<:a wY wV x) | a wY wV -> Bool forall wX wY. a wX wY -> Bool p a wY wV x = (forall wX wY. a wX wY -> Bool) -> RL a wR wY -> Sealed (RL a wR) forall (a :: * -> * -> *) wR wV. (forall wX wY. a wX wY -> Bool) -> RL a wR wV -> Sealed (RL a wR) dropWhileRL forall wX wY. a wX wY -> Bool p RL a wR wY xs' | Bool otherwise = RL a wR wV -> Sealed (RL a wR) forall (a :: * -> *) wX. a wX -> Sealed a seal RL a wR wV xs -- | Like 'takeWhile' only for 'RL's. This function is supposed to be lazy: -- elements before the split point should not be touched. takeWhileRL :: (forall wA wB . a wA wB -> Bool) -> RL a wX wY -> FlippedSeal (RL a) wY takeWhileRL :: (forall wA wB. a wA wB -> Bool) -> RL a wX wY -> FlippedSeal (RL a) wY takeWhileRL forall wA wB. a wA wB -> Bool f RL a wX wY xs = case (forall wA wB. a wA wB -> Bool) -> RL a wX wY -> (:>) (RL a) (RL a) wX wY forall (p :: * -> * -> *) wX wY. (forall wA wB. p wA wB -> Bool) -> RL p wX wY -> (:>) (RL p) (RL p) wX wY spanRL forall wA wB. a wA wB -> Bool f RL a wX wY xs of RL a wX wZ _ :> RL a wZ wY r -> RL a wZ wY -> FlippedSeal (RL a) wY forall (a :: * -> * -> *) wX wY. a wX wY -> FlippedSeal a wY flipSeal RL a wZ wY r -- | Like 'span' only for 'RL's. This function is supposed to be lazy: -- elements before the split point should not be touched. spanRL :: (forall wA wB . p wA wB -> Bool) -> RL p wX wY -> (RL p :> RL p) wX wY spanRL :: (forall wA wB. p wA wB -> Bool) -> RL p wX wY -> (:>) (RL p) (RL p) wX wY spanRL forall wA wB. p wA wB -> Bool _ RL p wX wY NilRL = RL p wX wX forall (a :: * -> * -> *) wX. RL a wX wX NilRL RL p wX wX -> RL p wX wX -> (:>) (RL p) (RL p) wX wX forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> RL p wX wX forall (a :: * -> * -> *) wX. RL a wX wX NilRL spanRL forall wA wB. p wA wB -> Bool f left :: RL p wX wY left@(RL p wX wY ps :<: p wY wY p) | p wY wY -> Bool forall wA wB. p wA wB -> Bool f p wY wY p = case (forall wA wB. p wA wB -> Bool) -> RL p wX wY -> (:>) (RL p) (RL p) wX wY forall (p :: * -> * -> *) wX wY. (forall wA wB. p wA wB -> Bool) -> RL p wX wY -> (:>) (RL p) (RL p) wX wY spanRL forall wA wB. p wA wB -> Bool f RL p wX wY ps of RL p wX wZ left' :> RL p wZ wY right -> RL p wX wZ left' RL p wX wZ -> RL p wZ wY -> (:>) (RL p) (RL p) wX wY forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> RL p wZ wY right RL p wZ wY -> p wY wY -> RL p wZ wY forall (a :: * -> * -> *) wX wY wZ. RL a wX wY -> a wY wZ -> RL a wX wZ :<: p wY wY p | Bool otherwise = RL p wX wY left RL p wX wY -> RL p wY wY -> (:>) (RL p) (RL p) wX wY forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> RL p wY wY forall (a :: * -> * -> *) wX. RL a wX wX NilRL -- | Like 'break' only for 'RL's. This function is supposed to be lazy: -- elements before the split point should not be touched. breakRL :: (forall wA wB . p wA wB -> Bool) -> RL p wX wY -> (RL p :> RL p) wX wY breakRL :: (forall wA wB. p wA wB -> Bool) -> RL p wX wY -> (:>) (RL p) (RL p) wX wY breakRL forall wA wB. p wA wB -> Bool f = (forall wA wB. p wA wB -> Bool) -> RL p wX wY -> (:>) (RL p) (RL p) wX wY forall (p :: * -> * -> *) wX wY. (forall wA wB. p wA wB -> Bool) -> RL p wX wY -> (:>) (RL p) (RL p) wX wY spanRL (Bool -> Bool not (Bool -> Bool) -> (p wA wB -> Bool) -> p wA wB -> Bool forall b c a. (b -> c) -> (a -> b) -> a -> c . p wA wB -> Bool forall wA wB. p wA wB -> Bool f) -- |Check that two 'FL's are equal element by element. -- This differs from the 'Eq2' instance for 'FL' which -- uses commutation. eqFL :: Eq2 a => FL a wX wY -> FL a wX wZ -> EqCheck wY wZ eqFL :: FL a wX wY -> FL a wX wZ -> EqCheck wY wZ eqFL FL a wX wY NilFL FL a wX wZ NilFL = EqCheck wY wZ forall wA. EqCheck wA wA IsEq eqFL (a wX wY x:>:FL a wY wY xs) (a wX wY y:>:FL a wY wZ ys) | EqCheck wY wY IsEq <- a wX wY x a wX wY -> a wX wY -> EqCheck wY wY forall (p :: * -> * -> *) wA wB wC. Eq2 p => p wA wB -> p wA wC -> EqCheck wB wC =\/= a wX wY y, EqCheck wY wZ IsEq <- FL a wY wY -> FL a wY wZ -> EqCheck wY wZ forall (a :: * -> * -> *) wX wY wZ. Eq2 a => FL a wX wY -> FL a wX wZ -> EqCheck wY wZ eqFL FL a wY wY xs FL a wY wZ FL a wY wZ ys = EqCheck wY wZ forall wA. EqCheck wA wA IsEq eqFL FL a wX wY _ FL a wX wZ _ = EqCheck wY wZ forall wA wB. EqCheck wA wB NotEq eqFLUnsafe :: Eq2 a => FL a wX wY -> FL a wZ wW -> Bool eqFLUnsafe :: FL a wX wY -> FL a wZ wW -> Bool eqFLUnsafe FL a wX wY NilFL FL a wZ wW NilFL = Bool True eqFLUnsafe (a wX wY x:>:FL a wY wY xs) (a wZ wY y:>:FL a wY wW ys) = a wX wY -> a wZ wY -> Bool forall (p :: * -> * -> *) wA wB wC wD. Eq2 p => p wA wB -> p wC wD -> Bool unsafeCompare a wX wY x a wZ wY y Bool -> Bool -> Bool && FL a wY wY -> FL a wY wW -> Bool forall (a :: * -> * -> *) wX wY wZ wW. Eq2 a => FL a wX wY -> FL a wZ wW -> Bool eqFLUnsafe FL a wY wY xs FL a wY wW ys eqFLUnsafe FL a wX wY _ FL a wZ wW _ = Bool False infixr 5 +>>+ infixl 5 +<<+ -- | Prepend an 'RL' to an 'FL'. This traverses only the left hand side. (+>>+) :: RL p wX wY -> FL p wY wZ -> FL p wX wZ RL p wX wY NilRL +>>+ :: RL p wX wY -> FL p wY wZ -> FL p wX wZ +>>+ FL p wY wZ ys = FL p wX wZ FL p wY wZ ys (RL p wX wY xs:<:p wY wY x) +>>+ FL p wY wZ ys = RL p wX wY xs RL p wX wY -> FL p wY wZ -> FL p wX wZ forall (p :: * -> * -> *) wX wY wZ. RL p wX wY -> FL p wY wZ -> FL p wX wZ +>>+ (p wY wY x p wY wY -> FL p wY wZ -> FL p wY wZ forall (a :: * -> * -> *) wX wY wZ. a wX wY -> FL a wY wZ -> FL a wX wZ :>: FL p wY wZ ys) -- | Append an 'FL' to an 'RL'. This traverses only the right hand side. (+<<+) :: RL p wX wY -> FL p wY wZ -> RL p wX wZ RL p wX wY xs +<<+ :: RL p wX wY -> FL p wY wZ -> RL p wX wZ +<<+ FL p wY wZ NilFL = RL p wX wY RL p wX wZ xs RL p wX wY xs +<<+ (p wY wY y:>:FL p wY wZ ys) = (RL p wX wY xsRL p wX wY -> p wY wY -> RL p wX wY forall (a :: * -> * -> *) wX wY wZ. RL a wX wY -> a wY wZ -> RL a wX wZ :<:p wY wY y) RL p wX wY -> FL p wY wZ -> RL p wX wZ forall (a :: * -> * -> *) wL wM wO. RL a wL wM -> FL a wM wO -> RL a wL wO +<<+ FL p wY wZ ys initsFL :: FL p wX wY -> [Sealed ((p :> FL p) wX)] initsFL :: FL p wX wY -> [Sealed ((:>) p (FL p) wX)] initsFL FL p wX wY NilFL = [] initsFL (p wX wY x :>: FL p wY wY xs) = (:>) p (FL p) wX wY -> Sealed ((:>) p (FL p) wX) forall (a :: * -> *) wX. a wX -> Sealed a Sealed (p wX wY x p wX wY -> FL p wY wY -> (:>) p (FL p) wX wY forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> FL p wY wY forall (a :: * -> * -> *) wX. FL a wX wX NilFL) Sealed ((:>) p (FL p) wX) -> [Sealed ((:>) p (FL p) wX)] -> [Sealed ((:>) p (FL p) wX)] forall a. a -> [a] -> [a] : (Sealed ((:>) p (FL p) wY) -> Sealed ((:>) p (FL p) wX)) -> [Sealed ((:>) p (FL p) wY)] -> [Sealed ((:>) p (FL p) wX)] forall a b. (a -> b) -> [a] -> [b] map (\(Sealed (y :> xs')) -> (:>) p (FL p) wX wX -> Sealed ((:>) p (FL p) wX) forall (a :: * -> *) wX. a wX -> Sealed a Sealed (p wX wY x p wX wY -> FL p wY wX -> (:>) p (FL p) wX wX forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ. a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY :> p wY wZ y p wY wZ -> FL p wZ wX -> FL p wY wX forall (a :: * -> * -> *) wX wY wZ. a wX wY -> FL a wY wZ -> FL a wX wZ :>: FL p wZ wX xs')) (FL p wY wY -> [Sealed ((:>) p (FL p) wY)] forall (p :: * -> * -> *) wX wY. FL p wX wY -> [Sealed ((:>) p (FL p) wX)] initsFL FL p wY wY xs) concatRLFL :: RL (FL p) wX wY -> RL p wX wY concatRLFL :: RL (FL p) wX wY -> RL p wX wY concatRLFL RL (FL p) wX wY NilRL = RL p wX wY forall (a :: * -> * -> *) wX. RL a wX wX NilRL concatRLFL (RL (FL p) wX wY ps :<: FL p wY wY p) = RL (FL p) wX wY -> RL p wX wY forall (p :: * -> * -> *) wX wY. RL (FL p) wX wY -> RL p wX wY concatRLFL RL (FL p) wX wY ps RL p wX wY -> FL p wY wY -> RL p wX wY forall (a :: * -> * -> *) wL wM wO. RL a wL wM -> FL a wM wO -> RL a wL wO +<<+ FL p wY wY p