-- 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 &#47;    &#92; a4  
--       &#47;      &#92;    
--      wX      wY       
--       &#92;      &#47;    
--     a1 &#92;    &#47; 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       
--       &#92;     &#47;    
--        &#92;   &#47;
--         &#92; &#47;     
--          wU
--          &#124;
--          &#124;
--          &#124;
--          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