#include "gadts.h"
module Darcs.Witnesses.WZipper ( FZipper(..), focus, leftmost, left
, rightmost, right, jokers, clowns
, flToZipper, lengthFZ, nullFZ
, toEnd, toStart
)
where
import Darcs.Witnesses.Ordered ( FL(..), RL(..), nullFL, nullRL
, lengthFL, lengthRL, (+<+)
, reverseFL, reverseRL, (+>+)
)
import Darcs.Witnesses.Sealed(Sealed2(..), Sealed(..), FlippedSeal(..))
data FZipper a C(x z) where
FZipper :: RL a C(x y) -> FL a C(y z) -> FZipper a C(x z)
flToZipper :: FL a C(x y) -> FZipper a C(x y)
flToZipper l = FZipper NilRL l
--destructors
nullFZ :: FZipper a C(x y) -> Bool
nullFZ (FZipper l r) = nullRL l && nullFL r
lengthFZ :: FZipper a C(x y) -> Int
lengthFZ (FZipper l r) = lengthRL l + lengthFL r
focus :: FZipper a C(x y) -> Maybe (Sealed2 a)
focus (FZipper _ (x :>: _)) = Just $ Sealed2 x
focus _ = Nothing
clowns :: FZipper a C(x y) -> Sealed ((RL a) C(x))
clowns (FZipper l _) = Sealed l
jokers :: FZipper a C(x y) -> FlippedSeal (FL a) C(y)
jokers (FZipper _ r) = FlippedSeal r
rightmost :: FZipper p C(x y) -> Bool
rightmost (FZipper _ NilFL) = True
rightmost _ = False
right :: FZipper p C(x y) -> FZipper p C(x y)
right (FZipper l (b:>:r)) = FZipper (b :<: l) r
right x@(FZipper _ NilFL) = x
leftmost :: FZipper p C(x y) -> Bool
leftmost (FZipper NilRL _) = True
leftmost _ = False
left :: FZipper p C(x y) -> FZipper p C(x y)
left (FZipper (b :<: l) r) = FZipper l (b :>: r)
left x@(FZipper NilRL _) = x
toEnd :: FZipper p C(x y) -> FZipper p C(x y)
toEnd (FZipper l r) = FZipper (reverseFL r +<+ l) NilFL
toStart :: FZipper p C(x y) -> FZipper p C(x y)
toStart (FZipper l r) = FZipper NilRL ((reverseRL l) +>+ r)