-- 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
    , foldlFL
    , foldlRL
    , allFL
    , allRL
    , anyFL
    , anyRL
    , filterFL
    , filterRL
    , splitAtFL
    , splitAtRL
    , filterOutFLFL
    , filterOutRLRL
    , reverseFL
    , reverseRL
    , (+>+)
    , (+<+)
    , (+>>+)
    , (+<<+)
    , concatFL
    , concatRL
    , dropWhileFL
    , dropWhileRL
    -- * 'FL' only
    , bunchFL
    , foldFL_M
    , spanFL
    , spanFL_M
    , zipWithFL
    , toFL
    , mapFL_FL_M
    , sequenceFL_
    , eqFL
    , eqFLRev
    , eqFLUnsafe
    , initsFL
    -- * 'RL' only
    , isShorterThanRL
    , snocRLSealed
    ) where

import Prelude ()
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 _ NilFL = String -> ShowS
showString "NilFL"
   showsPrec d :: Int
d (x :: a wX wY
x :>: xs :: 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
+ 1) a wX wY
x ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                            String -> ShowS
showString " :>: " 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
+ 1) FL a wY wZ
xs
       where prec :: Int
prec = 5

instance Show2 a => Show1 (FL a wX) where
   showDict1 :: ShowDict (FL a wX wX)
showDict1 = ShowDict (FL a wX wX)
forall a. Show a => ShowDict a
ShowDictClass

instance Show2 a => Show2 (FL a) where
   showDict2 :: ShowDict (FL a wX wY)
showDict2 = ShowDict (FL a wX wY)
forall a. Show a => ShowDict a
ShowDictClass

instance Show2 a => Show (RL a wX wZ) where
   showsPrec :: Int -> RL a wX wZ -> ShowS
showsPrec _ NilRL = String -> ShowS
showString "NilRL"
   showsPrec d :: Int
d (xs :: RL a wX wY
xs :<: x :: 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
+ 1) RL a wX wY
xs ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                            String -> ShowS
showString " :<: " 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
+ 1) a wY wZ
x
       where prec :: Int
prec = 5

instance Show2 a => Show1 (RL a wX) where
   showDict1 :: ShowDict (RL a wX wX)
showDict1 = ShowDict (RL a wX wX)
forall a. Show a => ShowDict a
ShowDictClass

instance Show2 a => Show2 (RL a) where
   showDict2 :: ShowDict (RL a wX wY)
showDict2 = ShowDict (RL a wX wY)
forall a. Show a => ShowDict a
ShowDictClass

instance (Show2 a, Show2 b) => Show1 ((a :> b) wX) where
   showDict1 :: ShowDict ((:>) a b wX wX)
showDict1 = ShowDict ((:>) a b wX wX)
forall a. Show a => ShowDict a
ShowDictClass

-- * 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 d :: Int
d (x :: a wX wZ
x :> y :: 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 1 ":>" Int
d a wX wZ
x b wZ wY
y

instance (Eq2 a, Eq2 b) => Eq2 (a :> b) where
    (a1 :: a wA wZ
a1 :> b1 :: b wZ wB
b1) =\/= :: (:>) a b wA wB -> (:>) a b wA wC -> EqCheck wB wC
=\/= (a2 :: a wA wZ
a2 :> b2 :: 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) where
    showDict2 :: ShowDict ((:>) a b wX wY)
showDict2 = ShowDict ((:>) a b wX wY)
forall a. Show a => ShowDict a
ShowDictClass

instance (Show2 a, Show2 b) => Show ( (a :\/: b) wX wY ) where
    showsPrec :: Int -> (:\/:) a b wX wY -> ShowS
showsPrec d :: Int
d (x :: a wZ wX
x :\/: y :: 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 9 ":\\/:" Int
d a wZ wX
x b wZ wY
y

instance (Show2 a, Show2 b) => Show2 (a :\/: b) where
    showDict2 :: ShowDict ((:\/:) a b wX wY)
showDict2 = ShowDict ((:\/:) a b wX wY)
forall a. Show a => ShowDict a
ShowDictClass

instance (Show2 a, Show2 b) => Show ( (a :/\: b) wX wY ) where
    showsPrec :: Int -> (:/\:) a b wX wY -> ShowS
showsPrec d :: Int
d (x :: a wX wZ
x :/\: y :: 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 1 ":/\\:" Int
d a wX wZ
x b wY wZ
y

instance (Show2 a, Show2 b) => Show2 ( (a :/\: b) ) where
    showDict2 :: ShowDict ((:/\:) a b wX wY)
showDict2 = ShowDict ((:/\:) a b wX wY)
forall a. Show a => ShowDict a
ShowDictClass

-- * Functions

infixr 5 :>:, +>+
infixl 5 :<:, +<+

nullFL :: FL a wX wZ -> Bool
nullFL :: FL a wX wZ -> Bool
nullFL NilFL = Bool
True
nullFL _ = Bool
False

nullRL :: RL a wX wZ -> Bool
nullRL :: RL a wX wZ -> Bool
nullRL NilRL = Bool
True
nullRL _ = 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 _ NilFL = FL p wW wZ
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL
filterOutFLFL f :: forall wX wY. p wX wY -> EqCheck wX wY
f (x :: p wW wY
x:>:xs :: 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 _ NilRL = RL p wW wZ
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL
filterOutRLRL f :: forall wX wY. p wX wY -> EqCheck wX wY
f (xs :: RL p wW wY
xs:<:x :: 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 _ NilRL = []
filterRL f :: forall wX wY. p wX wY -> Bool
f (xs :: RL p wA wY
xs :<: x :: 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
NilFL +>+ :: FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ ys :: FL a wY wZ
ys = FL a wX wZ
FL a wY wZ
ys
(x :: a wX wY
x:>:xs :: FL a wY wY
xs) +>+ ys :: 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
xs :: RL a wX wY
xs +<+ :: RL a wX wY -> RL a wY wZ -> RL a wX wZ
+<+ NilRL = RL a wX wY
RL a wX wZ
xs
xs :: RL a wX wY
xs +<+ (ys :: RL a wY wY
ys:<:y :: 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 xs :: 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 ls :: RL a wL wM
ls NilFL = RL a wL wM
RL a wL wO
ls
        r ls :: RL a wL wM
ls (a :: a wM wY
a:>:as :: 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 xs :: 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 ls :: FL a wM wO
ls NilRL = FL a wM wO
FL a wL wO
ls
        r ls :: FL a wM wO
ls (as :: RL a wL wY
as:<:a :: 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 NilFL = FL a wX wZ
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL
concatFL (a :: FL a wX wY
a:>:as :: 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 NilRL = RL a wX wZ
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL
concatRL (as :: RL (RL a) wX wY
as:<:a :: 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 f :: forall wW wY. a wW wY -> Bool
f (x :: a wX wY
x:>:xs :: 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
                            ys :: FL a wY wZ
ys :> zs :: 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 _ xs :: 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 f :: forall wW wY. a wW wY -> m Bool
f (x :: a wX wY
x:>:xs :: 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 (ys :: FL a wY wZ
ys :> zs :: 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 _ (FL a wX wZ
NilFL) = (:>) (FL a) (FL a) wX wX -> m ((:>) (FL a) (FL a) wX wZ)
forall (m :: * -> *) a. Monad m => a -> m a
return ((:>) (FL a) (FL a) wX wX -> m ((:>) (FL a) (FL a) wX wZ))
-> (:>) (FL a) (FL a) wX wX -> 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 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 0 xs :: 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 _ 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 n :: Int
n (x :: a wX wY
x:>:xs :: 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
-1) FL a wY wZ
xs of
                       (xs' :: FL a wY wZ
xs':>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 0 xs :: 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 _ 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 n :: Int
n (xs :: RL a wX wY
xs:<:x :: 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
-1) RL a wX wY
xs of
                       (xs'' :: RL a wX wZ
xs'':>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 _ NilFL = FL (FL a) wX wY
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL
bunchFL n :: Int
n (x :: a wX wY
x:>:xs :: 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 NilFL = FL (FL a) wX wY
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL
          bFL bs :: 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
                   a :: FL a wX wZ
a :> b :: 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, i.e. 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 _ r :: r wX
r NilFL = r wX -> m (r wX)
forall (m :: * -> *) a. Monad m => a -> m a
return r wX
r
foldFL_M f :: forall wA wB. r wA -> p wA wB -> m (r wB)
f r :: r wX
r (x :: p wX wY
x :>: xs :: 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' :: 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

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 f :: forall wX wY. a wX wY -> Bool
f xs :: 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 f :: forall wX wY. a wX wY -> Bool
f xs :: 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 f :: forall wA wB. a wA wB -> Bool
f xs :: 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 f :: forall wA wB. a wA wB -> Bool
f xs :: 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

foldlFL :: (forall wW wY . a -> b wW wY -> a) -> a -> FL b wX wZ -> a
foldlFL :: (forall wW wY. a -> b wW wY -> a) -> a -> FL b wX wZ -> a
foldlFL _ x :: a
x NilFL = a
x
foldlFL f :: forall wW wY. a -> b wW wY -> a
f x :: a
x (y :: b wX wY
y:>:ys :: FL b wY wZ
ys) = (forall wW wY. a -> b wW wY -> a) -> a -> FL b wY wZ -> a
forall a (b :: * -> * -> *) wX wZ.
(forall wW wY. a -> b wW wY -> a) -> a -> FL b wX wZ -> a
foldlFL forall wW wY. a -> b wW wY -> a
f (a -> b wX wY -> a
forall wW wY. a -> b wW wY -> a
f a
x b wX wY
y) FL b wY wZ
ys

foldlRL :: (forall wW wY . a -> b wW wY -> a) -> a -> RL b wX wZ -> a
foldlRL :: (forall wW wY. a -> b wW wY -> a) -> a -> RL b wX wZ -> a
foldlRL _ x :: a
x NilRL = a
x
foldlRL f :: forall wW wY. a -> b wW wY -> a
f x :: a
x (ys :: RL b wX wY
ys:<:y :: b wY wZ
y) = (forall wW wY. a -> b wW wY -> a) -> a -> RL b wX wY -> a
forall a (b :: * -> * -> *) wX wZ.
(forall wW wY. a -> b wW wY -> a) -> a -> RL b wX wZ -> a
foldlRL forall wW wY. a -> b wW wY -> a
f (a -> b wY wZ -> a
forall wW wY. a -> b wW wY -> a
f a
x b wY wZ
y) RL b wX wY
ys

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 _ NilFL = FL b wX wZ
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL
mapFL_FL f :: forall wW wY. a wW wY -> b wW wY
f (a :: a wX wY
a:>:as :: 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 _ 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 f :: forall wW wY. a wW wY -> m (b wW wY)
f (a :: a wX wY
a:>:as :: 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_ f :: 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 f :: forall wX wY. a -> p wX wY -> q wX wY
f (x :: a
x:xs :: [a]
xs) (y :: p wW wY
y :>: ys :: 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 _ _ NilFL = FL q wW wZ
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL
zipWithFL _ [] (_:>:_) = String -> FL q wW wZ
forall a. String -> a
bug "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 _ NilRL = RL b wX wZ
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL
mapRL_RL f :: forall wW wY. a wW wY -> b wW wY
f (as :: RL a wX wY
as:<:a :: 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

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 _ NilFL = []
mapFL f :: forall wW wZ. a wW wZ -> b
f (a :: a wX wY
a :>: b :: 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 _ NilFL = []
filterFL f :: forall wX wY. a wX wY -> Bool
f (a :: a wW wY
a :>: b :: 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 _ NilRL = []
mapRL f :: forall wW wZ. a wW wZ -> b
f (as :: RL a wX wY
as :<: a :: 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 xs :: 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 0
  where l :: FL a wX wZ -> Int -> Int
        l :: FL a wX wZ -> Int -> Int
l NilFL n :: Int
n = Int
n
        l (_:>:as :: FL a wY wZ
as) n :: 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
+1

lengthRL :: RL a wX wZ -> Int
lengthRL :: RL a wX wZ -> Int
lengthRL xs :: 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 0
  where l :: RL a wX wZ -> Int -> Int
        l :: RL a wX wZ -> Int -> Int
l NilRL n :: Int
n = Int
n
        l (as :: RL a wX wY
as:<:_) n :: 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
+1

isShorterThanRL :: RL a wX wY -> Int -> Bool
isShorterThanRL :: RL a wX wY -> Int -> Bool
isShorterThanRL _ n :: Int
n | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= 0 = Bool
False
isShorterThanRL NilRL _ = Bool
True
isShorterThanRL (xs :: RL a wX wY
xs:<:_) n :: 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
-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 as :: RL a wX wY
as) a :: 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 (x :: FreeLeft a
x:xs :: [FreeLeft a]
xs) = case FreeLeft a -> Sealed (a wX)
forall (p :: * -> * -> *) wX. FreeLeft p -> Sealed (p wX)
unFreeLeft FreeLeft a
x of Sealed y :: 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 ys :: 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 _ 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 p :: forall wX wY. a wX wY -> Bool
p xs :: FL a wR wV
xs@(x :: a wR wY
x:>:xs' :: 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 _ 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 p :: forall wX wY. a wX wY -> Bool
p xs :: RL a wR wV
xs@(xs' :: RL a wR wY
xs':<:x :: 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

-- |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 NilFL NilFL = EqCheck wY wZ
forall wA. EqCheck wA wA
IsEq
eqFL (x :: a wX wY
x:>:xs :: FL a wY wY
xs) (y :: a wX wY
y:>:ys :: 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 _ _ = EqCheck wY wZ
forall wA wB. EqCheck wA wB
NotEq

eqFLRev :: Eq2 a => FL a wX wZ -> FL a wY wZ -> EqCheck wX wY
eqFLRev :: FL a wX wZ -> FL a wY wZ -> EqCheck wX wY
eqFLRev NilFL NilFL = EqCheck wX wY
forall wA. EqCheck wA wA
IsEq
eqFLRev (x :: a wX wY
x:>:xs :: FL a wY wZ
xs) (y :: a wY wY
y:>:ys :: FL a wY wZ
ys) | EqCheck wY wY
IsEq <- FL a wY wZ -> FL a wY wZ -> EqCheck wY wY
forall (a :: * -> * -> *) wX wZ wY.
Eq2 a =>
FL a wX wZ -> FL a wY wZ -> EqCheck wX wY
eqFLRev FL a wY wZ
xs FL a wY wZ
ys, EqCheck wX wY
IsEq <- a wX wY
x a wX wY -> a wY wY -> EqCheck wX wY
forall (p :: * -> * -> *) wA wC wB.
Eq2 p =>
p wA wC -> p wB wC -> EqCheck wA wB
=/\= a wY wY
a wY wY
y = EqCheck wX wY
forall wA. EqCheck wA wA
IsEq
eqFLRev _ _ = EqCheck wX wY
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 NilFL NilFL = Bool
True
eqFLUnsafe (x :: a wX wY
x:>:xs :: FL a wY wY
xs) (y :: a wZ wY
y:>:ys :: 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 _ _ = 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
NilRL +>>+ :: RL p wX wY -> FL p wY wZ -> FL p wX wZ
+>>+ ys :: FL p wY wZ
ys = FL p wX wZ
FL p wY wZ
ys
(xs :: RL p wX wY
xs:<:x :: p wY wY
x) +>>+ ys :: 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
xs :: RL p wX wY
xs +<<+ :: RL p wX wY -> FL p wY wZ -> RL p wX wZ
+<<+ NilFL = RL p wX wY
RL p wX wZ
xs
xs :: RL p wX wY
xs +<<+ (y :: p wY wY
y:>:ys :: 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 NilFL = []
initsFL (x :: p wX wY
x :>: xs :: 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)