module Darcs.Patch.Witnesses.WZipper
( FZipper(..)
, focus
, leftmost
, left
, rightmost
, right
, jokers
, clowns
, flToZipper
, lengthFZ
, nullFZ
, toEnd
, toStart
)
where
import Darcs.Prelude
import Darcs.Patch.Witnesses.Ordered
( FL(..)
, RL(..)
, nullFL
, nullRL
, lengthFL
, lengthRL
, reverseFL
, reverseRL
, (+<+)
, (+>+)
)
import Darcs.Patch.Witnesses.Sealed(Sealed2(..), Sealed(..), FlippedSeal(..))
data FZipper a wX wZ where
FZipper :: RL a wX wY -> FL a wY wZ -> FZipper a wX wZ
flToZipper :: FL a wX wY -> FZipper a wX wY
flToZipper :: forall (a :: * -> * -> *) wX wY. FL a wX wY -> FZipper a wX wY
flToZipper = RL a wX wX -> FL a wX wY -> FZipper a wX wY
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> FL a wY wZ -> FZipper a wX wZ
FZipper RL a wX wX
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL
nullFZ :: FZipper a wX wY -> Bool
nullFZ :: forall (a :: * -> * -> *) wX wY. FZipper a wX wY -> Bool
nullFZ (FZipper RL a wX wY
l FL a wY wY
r) = RL a wX wY -> Bool
forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> Bool
nullRL RL a wX wY
l Bool -> Bool -> Bool
&& FL a wY wY -> Bool
forall (a :: * -> * -> *) wX wZ. FL a wX wZ -> Bool
nullFL FL a wY wY
r
lengthFZ :: FZipper a wX wY -> Int
lengthFZ :: forall (a :: * -> * -> *) wX wY. FZipper a wX wY -> Int
lengthFZ (FZipper RL a wX wY
l FL a wY wY
r) = RL a wX wY -> Int
forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> Int
lengthRL RL a wX wY
l Int -> Int -> Int
forall a. Num a => a -> a -> a
+ FL a wY wY -> Int
forall (a :: * -> * -> *) wX wZ. FL a wX wZ -> Int
lengthFL FL a wY wY
r
focus :: FZipper a wX wY -> Maybe (Sealed2 a)
focus :: forall (a :: * -> * -> *) wX wY.
FZipper a wX wY -> Maybe (Sealed2 a)
focus (FZipper RL a wX wY
_ (a wY wY
x :>: FL a wY wY
_)) = Sealed2 a -> Maybe (Sealed2 a)
forall a. a -> Maybe a
Just (Sealed2 a -> Maybe (Sealed2 a)) -> Sealed2 a -> Maybe (Sealed2 a)
forall a b. (a -> b) -> a -> b
$ a wY wY -> Sealed2 a
forall (a :: * -> * -> *) wX wY. a wX wY -> Sealed2 a
Sealed2 a wY wY
x
focus FZipper a wX wY
_ = Maybe (Sealed2 a)
forall a. Maybe a
Nothing
clowns :: FZipper a wX wY -> Sealed ((RL a) wX)
clowns :: forall (a :: * -> * -> *) wX wY.
FZipper a wX wY -> Sealed (RL a wX)
clowns (FZipper RL a wX wY
l FL a wY wY
_) = RL a wX wY -> Sealed (RL a wX)
forall (a :: * -> *) wX. a wX -> Sealed a
Sealed RL a wX wY
l
jokers :: FZipper a wX wY -> FlippedSeal (FL a) wY
jokers :: forall (a :: * -> * -> *) wX wY.
FZipper a wX wY -> FlippedSeal (FL a) wY
jokers (FZipper RL a wX wY
_ FL a wY wY
r) = FL a wY wY -> FlippedSeal (FL a) wY
forall (a :: * -> * -> *) wX wY. a wX wY -> FlippedSeal a wY
FlippedSeal FL a wY wY
r
rightmost :: FZipper p wX wY -> Bool
rightmost :: forall (a :: * -> * -> *) wX wY. FZipper a wX wY -> Bool
rightmost (FZipper RL p wX wY
_ FL p wY wY
NilFL) = Bool
True
rightmost FZipper p wX wY
_ = Bool
False
right :: FZipper p wX wY -> FZipper p wX wY
right :: forall (p :: * -> * -> *) wX wY. FZipper p wX wY -> FZipper p wX wY
right (FZipper RL p wX wY
l (p wY wY
m:>:FL p wY wY
r)) = RL p wX wY -> FL p wY wY -> FZipper p wX wY
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> FL a wY wZ -> FZipper a wX wZ
FZipper (RL p wX wY
l RL 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
m) FL p wY wY
r
right x :: FZipper p wX wY
x@(FZipper RL p wX wY
_ FL p wY wY
NilFL) = FZipper p wX wY
x
leftmost :: FZipper p wX wY -> Bool
leftmost :: forall (a :: * -> * -> *) wX wY. FZipper a wX wY -> Bool
leftmost (FZipper RL p wX wY
NilRL FL p wY wY
_) = Bool
True
leftmost FZipper p wX wY
_ = Bool
False
left :: FZipper p wX wY -> FZipper p wX wY
left :: forall (p :: * -> * -> *) wX wY. FZipper p wX wY -> FZipper p wX wY
left (FZipper (RL p wX wY
l :<: p wY wY
m) FL p wY wY
r) = RL p wX wY -> FL p wY wY -> FZipper p wX wY
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> FL a wY wZ -> FZipper a wX wZ
FZipper RL p wX wY
l (p wY wY
m p wY wY -> FL p wY wY -> FL p wY wY
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p wY wY
r)
left x :: FZipper p wX wY
x@(FZipper RL p wX wY
NilRL FL p wY wY
_) = FZipper p wX wY
x
toEnd :: FZipper p wX wY -> FZipper p wX wY
toEnd :: forall (p :: * -> * -> *) wX wY. FZipper p wX wY -> FZipper p wX wY
toEnd (FZipper RL p wX wY
l FL p wY wY
r) = RL p wX wY -> FL p wY wY -> FZipper p wX wY
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> FL a wY wZ -> FZipper a wX wZ
FZipper (RL p wX wY
l RL p wX wY -> RL p wY wY -> RL p wX wY
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> RL a wY wZ -> RL a wX wZ
+<+ FL p wY wY -> RL p wY wY
forall (a :: * -> * -> *) wX wZ. FL a wX wZ -> RL a wX wZ
reverseFL FL p wY wY
r) FL p wY wY
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL
toStart :: FZipper p wX wY -> FZipper p wX wY
toStart :: forall (p :: * -> * -> *) wX wY. FZipper p wX wY -> FZipper p wX wY
toStart (FZipper RL p wX wY
l FL p wY wY
r) = RL p wX wX -> FL p wX wY -> FZipper p wX wY
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> FL a wY wZ -> FZipper a wX wZ
FZipper RL p wX wX
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL (FL p wX wY -> FZipper p wX wY) -> FL p wX wY -> FZipper p wX wY
forall a b. (a -> b) -> a -> b
$ RL p wX wY -> FL p wX wY
forall (a :: * -> * -> *) wX wZ. RL a wX wZ -> FL a wX wZ
reverseRL RL p wX wY
l FL p wX wY -> FL p wY wY -> FL p wX wY
forall (a :: * -> * -> *) wX wY wZ.
FL a wX wY -> FL a wY wZ -> FL a wX wZ
+>+ FL p wY wY
r