-- Copyright (C) 2009 Florent Becker
--
-- 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.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(..))

-- forward zipper
data FZipper a wX wZ where
    FZipper :: RL a wX wY -> FL a wY wZ -> FZipper a wX wZ

-- Constructors
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

--destructors
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 to the left of me, jokers to the right.  Here I am, stuck
--   in the middle of you\"
--   <http://en.wikipedia.org/wiki/Stuck_in_the_Middle>
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

-- | See 'clowns'
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