{-# LANGUAGE TypeOperators, Rank2Types, EmptyDataDecls, 
             MultiParamTypeClasses, FunctionalDependencies, 
             FlexibleContexts, FlexibleInstances, UndecidableInstances,
             IncoherentInstances, OverlappingInstances #-}
module Data.Rope.Annotated.Internal 
    ( A(A,rope)
    , Ann
    , Annotation(..)
    , (:~>)

    , null      -- :: A s a -> Bool
    -- * Unpackable Ropes
    , head      -- :: Unpackable t => A s a -> t
    , last      -- :: Unpackable t => A s a -> t
    , unpack    -- :: Unpackable t => A s a -> [t]
    , uncons    -- :: (Annotation f, Unpackable t) => Ann a f -> Maybe (t, Ann (Tail t a) f)
    , unsnoc    -- :: (Annotation f, Unpackable t) => Ann a f -> Maybe (t, Ann (Init a t) f)

    -- * Splitting Ropes
    , drop      -- :: (Annotation f) => Int -> Ann a f -> (forall n. Ann (Drop n a) f -> r) -> r
    , take      -- :: (Annotation f) => Int -> Ann a f -> (forall n. Ann (Take n a) f -> r) -> r
    , splitAt   -- :: (Annotation f) => Int -> Ann a f -> (forall n. Ann (Take n a) f -> Ann (Drop n a) f -> r) -> r

    -- * Building Ropes
    , unit      -- :: (Annotation f, Reducer t Rope) => t -> Ann a f
    , snoc      -- :: (Annotation f, Reducer t Rope) => t -> Ann a f -> (forall c. Ann (Snoc c t a) f -> r) -> r
    , cons      -- :: (Annotation f, Reducer t Rope) => Ann a f -> t -> (forall c. Ann (Cons c t a) f -> r) -> r
    , empty     -- :: (Annotation f) => Ann Empty f 
    , append    -- :: (Annotation f, ) => Ann a f -> Ann b f -> Ann (a :<> b) f

    -- * Breaking Ropes

    , break     -- :: (Annotation f, Breakable t) => (t -> Bool) -> Ann a f -> (forall n. Ann (Take n a) f -> Ann (Drop n a) f -> r) -> r
    , span      -- :: (Annotation f, Breakable t) => (t -> Bool) -> Ann a f -> (forall n. Ann (Take n a) f -> Ann (Drop n a) f -> r) -> r
    , takeWhile -- :: (Annotation f, Breakable t) => (t -> Bool) -> Ann a f -> (forall n. Ann (Take n a) f -> r) -> r
    , dropWhile -- :: (Annotation f, Breakable t) => (t -> Bool) -> Ann a f -> (forall n. Ann (Drop n a) f -> r) -> r

    -- * Type-level constructors
    , Drop, Take, Snoc, Cons, Tail, Init, Empty, (:<>)

    -- * Annotation Products
    , (:*:)(..), fstF, sndF
    ) where

import Prelude hiding (null, head, last, take, drop, span, break, splitAt, takeWhile, dropWhile)
import Control.Applicative hiding (empty)
import Data.Rope.Util.Comonad
import Data.Monoid
import qualified Data.Rope.Util.Reducer as Reducer
import Data.Rope.Util.Reducer (Reducer)
import Data.FingerTree (Measured(..))
import Data.Foldable (Foldable, foldMap)
import qualified Data.Foldable
import Data.Traversable (Traversable(traverse))
import qualified Data.Rope.Internal as Rope
import Data.Rope.Body (Offset(..))
import Data.Rope.Internal (Rope(..),Breakable, Unpackable)

type f :~> g = forall a. f a -> g a

data A s a = A { rope :: !Rope, extractA :: a }

null :: A s a -> Bool
null = Rope.null . rope

head :: Unpackable t => A s a -> t
head = Rope.head . rope

last :: Unpackable t => A s a -> t
last = Rope.last . rope

type Ann a f = A a (f a)

instance Measured Offset (A s a) where
    measure = measure . rope

instance Functor (A s) where
    fmap f (A s a) = A s (f a) 

instance Comonad (A s) where
    extract = extractA
    extend f a@(A s _) = A s (f a)
    duplicate a@(A s _) = A s a

instance Foldable (A s) where
    foldr f z (A _ a) = f a z
    foldr1 _ (A _ a) = a
    foldl f z (A _ a) = f z a
    foldl1 _ (A _ a) = a
    foldMap f (A _ a) = f a

instance Traversable (A s) where
    traverse f (A s a) = A s <$> f a

class Annotation f where
    unitA    :: Rope -> f a
    splitAtA :: Int -> Rope -> f a -> (f b, f c)
    takeA    :: Int -> Rope -> f a -> f b
    dropA    :: Int -> Rope -> f a -> f b
    snocA    :: Rope -> Int -> f a -> f b
    consA    :: Int -> Rope -> f a -> f b
    emptyA   :: f Empty
    appendA  :: Ann a f -> Ann b f -> f (a :<> b)

    takeA n r = fst . splitAtA n r
    dropA n r = snd . splitAtA n r

empty :: Annotation f => Ann Empty f
empty = A Rope.empty emptyA


unit :: (Reducer t Rope, Annotation f) => t -> Ann a f
unit t = A r (unitA r)
    where 
        r :: Rope
        r = Reducer.unit t

splitAt :: Annotation f => Int -> Ann a f -> (forall n. Ann (Take n a)  f -> Ann (Drop n a) f -> r) -> r
splitAt n (A r a) k = k (A r b) (A r c) 
    where (b, c) = splitAtA n r a

drop :: Annotation f => Int -> Ann a f -> (forall n. Ann (Drop n a) f -> r) -> r
drop n (A r a) k = k (A r (dropA n r a))

take :: Annotation f => Int -> Ann a f -> (forall n. Ann (Take n a) f -> r) -> r
take n (A r a) k = k (A r (takeA n r a))

snoc :: (Annotation f, Reducer t Rope) => Ann a f -> t -> (forall c. Ann (Snoc c t a) f -> r) -> r
snoc (A r a) t k = k (A r' (snocA r' (Rope.length r' - Rope.length r) a))
    where r' = Reducer.snoc r t 

cons :: (Annotation f, Reducer t Rope) => t -> Ann a f -> (forall c. Ann (Cons c t a) f -> r) -> r
cons t (A r a) k = k (A r' (consA (Rope.length r' - Rope.length r) r' a))
    where r' = Reducer.cons t r

append :: Annotation f => Ann a f -> Ann b f -> Ann (a :<> b) f
append a@(A r _) b@(A s _) = A (r `mappend` s) (a `appendA` b)

break     :: (Annotation f, Breakable t) => (t -> Bool) -> Ann a f -> (forall n. Ann (Take n a) f -> Ann (Drop n a) f -> r) -> r
break p (A r a) k = k (A x b) (A y c) where
    (x,y) = Rope.break p r
    (b,c) = splitAtA (Rope.length x) r a

span      :: (Annotation f, Breakable t) => (t -> Bool) -> Ann a f -> (forall n. Ann (Take n a) f -> Ann (Drop n a) f -> r) -> r
span p (A r a) k = k (A x b) (A y c) where
    (x,y) = Rope.span p r
    (b,c) = splitAtA (Rope.length x) r a

takeWhile :: (Annotation f, Breakable t) => (t -> Bool) -> Ann a f -> (forall n. Ann (Take n a) f -> r) -> r
takeWhile p (A r a) k = k (A x b) where
    x = Rope.takeWhile p r
    b = takeA (Rope.length x) r a

dropWhile :: (Annotation f, Breakable t) => (t -> Bool) -> Ann a f -> (forall n. Ann (Drop n a) f -> r) -> r
dropWhile p (A r a) k = k (A y c) where
    y = Rope.dropWhile p r
    c = dropA (Rope.length r - Rope.length y) r a

uncons :: (Annotation f, Unpackable t) => Ann a f -> Maybe (t, Ann (Tail t a) f)
uncons (A r a) = case Rope.uncons r of
    Just (c,cs) -> Just (c, A cs (dropA (Rope.length r - Rope.length cs) r a))
    Nothing -> Nothing

unsnoc :: (Annotation f, Unpackable t) => Ann a f -> Maybe (Ann (Init a t) f, t)
unsnoc (A r a) = case Rope.unsnoc r of
    Just (cs,c) -> Just (A cs (dropA (Rope.length cs) r a), c)
    Nothing -> Nothing

-- annotation product

infixr 5 :*:

data (f :*: g) a = f a :*: g a

fstF :: (f :*: g) :~> f
fstF ~(f :*: _) = f

sndF :: (f :*: g) :~> g
sndF ~(_ :*: g) = g

instance (Functor f, Functor g)  => Functor (f :*: g) where
    fmap f (a :*: b) = fmap f a :*: fmap f b

instance (Applicative f, Applicative g) => Applicative (f :*: g) where
    pure a = pure a :*: pure a
    (f :*: g) <*> (a :*: b) = (f <*> a) :*: (g <*> b)

instance (Foldable f, Foldable g) => Foldable (f :*: g) where
    foldMap f (a :*: b) = foldMap f a `mappend` foldMap f b
    
instance (Traversable f, Traversable g) => Traversable (f :*: g) where
    traverse f (a :*: b) = (:*:) <$> traverse f a <*> traverse f b

instance (Annotation f, Annotation g) => Annotation (f :*: g) where
    unitA r = unitA r :*: unitA r
    emptyA = emptyA :*: emptyA
    dropA n r (f :*: g) = dropA n r f :*: dropA n r g
    takeA n r (f :*: g) = takeA n r f :*: takeA n r g
    splitAtA n r (f :*: g) = (f' :*: g' , f'' :*: g'') where
        (f',f'') = splitAtA n r f
        (g',g'') = splitAtA n r g
    snocA r n (f :*: g) = snocA r n f :*: snocA r n g
    consA n r (f :*: g) = consA n r f :*: consA n r g
    appendA (A r (a :*: a')) (A s (b :*: b')) = 
        appendA (A r a) (A s b) :*: appendA (A r a') (A s b')

    
data Take n a
data Drop n a
data Empty
data Cons s t a
data Snoc a s t
data (:<>) a b
data Tail t a
data Init a t

{-
class Append a b c | a b -> c
instance Append Empty a a
instance Append b c d => Append (a :<> b) c (a :<> d)
instance Append a b c => Append (Cons s t a) b (Cons s t c)
instance Append (Take n a) (Drop n a) a
instance Append a Empty a 
instance Append a b (a :<> b)

class Uncons t a b | t a -> b
instance Uncons t (Cons s t a) a
instance Uncons t a (Tail t a)

class Unsnoc a t b | a t -> b
instance Unsnoc (Snoc a s t) t a
instance Unsnoc a t (Init a t)
-}

unpack :: Unpackable t => A s a -> [t]
unpack (A s _) = Rope.unpack s