-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Shape
-- Copyright   :  (c) 2011 University of Minho
-- License     :  BSD3
--
-- Maintainer  :  hpacheco@di.uminho.pt
-- Stability   :  experimental
-- Portability :  non-portable
--
-- Pointless Lenses:
-- bidirectional lenses with point-free programming
-- 
-- This module defines a class of shapely functors that separate shape and data for polymorphic data types.
--
-----------------------------------------------------------------------------

module Data.Shape where

import Data.Relation
import Generics.Pointless.HFunctors

import Generics.Pointless.Functors
import Generics.Pointless.Combinators

import Data.Set as Set

-- | The type of positions (not a dependent type since it is not supported in Haskell)
type Pos a = Int

-- * The class of shapely functors and corresponding operations

-- | Class of shapely functors
class Shapely (s :: * -> *) where
	-- operations
    traverse :: ((a,x) -> (b,x)) -> (s a,x) -> (s b,x)
    smap     :: (a -> b) -> s a -> s b
    shape    :: s a -> s One
    data_    :: s a -> [a]
    recover  :: (s One,[a]) -> s a
    arity    :: s a -> Int
    locs     :: s a -> Set (Pos (s a))
    -- default definitions
    smap f = fst . traverse (\(a,x) -> (f a,x)) . (id /\ bang)
    shape = fst . traverse (bang >< id) . (id /\ bang)
    data_ = snd . traverse (\(v,l) -> (v,l++[v])) . (id /\ const [])
    recover = fst . traverse f
      where f (v,[]) = error "recover undefined: insuficient elements"
            f (v,x:xs) = (x,xs)
    arity = snd . traverse (\(v,n) -> (v,succ n)) . (id /\ const 0)
    locs s = Set.fromList $ [0..pred (arity s)]

instance Shapely Id where
    traverse f (IdF v,p) = (IdF >< id) $ f (v,p)

instance Shapely (Const c) where
    traverse f (ConsF b,p) = (ConsF b,p)

instance (Shapely f,Shapely g) => Shapely (f :*: g) where
    traverse f (ProdF fa ga,p) = (ProdF fb gb,p'')
        where (fb,p') = traverse f (fa,p)
              (gb,p'') = traverse f (ga,p')

instance (Shapely f,Shapely g) => Shapely (f :+: g) where
    traverse f (InlF fa,p) = (InlF >< id) $ traverse f (fa,p)
    traverse f (InrF ga,p) = (InrF >< id) $ traverse f (ga,p)

instance (Shapely f,Shapely g) => Shapely (f :@: g) where
    traverse f (CompF fga,p) = (CompF >< id) $ traverse (traverse f) (fga,p)

-- * The class of shapely higher-order functors, simply to avoid recursive definitions of Shapely
instance Shapely [] where
    traverse f = (hinn >< id) . traverse f . (hout >< id)

-- | Shapely instance that should be automatically generated
--instance (Hu f,Shapely (H f f)) => Shapely f where
--    traverse f = (hinn >< id) . traverse f . (hout >< id)

-- ** Special relations over shapes

-- | Correflexive with the locations of a value
locsR :: Shapely s => s a -> Pos (s a) :->: Pos (s a)
locsR = idR . locs

-- | Relation between the positions of a pair and positions of left elements
fstPosR :: (Shapely f,Shapely g) => (f a,g b) -> Pos (f a,g b) :->: Pos (f a)
fstPosR (fa,gb) = locsR fa

-- | Relation between the positions of a pair and positions of right elements
sndPosR :: (Shapely f,Shapely g) => (f a,g b) -> Pos (f a,g b) :->: Pos (g b)
sndPosR (fa,gb) = inv $ funR (+arity fa) (locs gb)

inlPosR :: (Shapely f,Shapely g) => (f a,g b) -> Pos (f a) :->: Pos (f a,g b)
inlPosR p = inv (fstPosR p)

inrPosR :: (Shapely f,Shapely g) => (f a,g b) -> Pos (g b) :->: Pos (f a,g b)
inrPosR p = inv (sndPosR p)

-- | Isomorphism between the positions of a pair and the sum of left and right positions
posPairR :: (Shapely f,Shapely g) => (f a,g b) -> Pos (f a,g b) :->: Either (Pos (f a)) (Pos (g b))
posPairR p@(fa,gb) = ((inlR (locs fa) .~ fstPosR p) `unionR` (inrR (locs gb) .~ sndPosR p))

-- | Either relation applied to the left and right locations of a pair
eitherPosR :: (Shapely f,Shapely g)
           => (f a,g b) -> (Pos (f a) :->: Pos (h c)) -> (Pos (g b) :->: Pos (h c)) -> (Pos (f a,g b) :->: Pos (h c))
eitherPosR p@(fa,gb) r s = (r \/~ s) .~ posPairR p

-- | Sum relation applied to pairs
sumPosR :: (Shapely f,Shapely g,Shapely h,Shapely i)
        => (f a,g b) -> (h c,i d) -> (Pos (f a) :->: Pos (h c)) -> (Pos (g b) :->: Pos (i d)) -> (Pos (f a,g b) :->: Pos (h c,i d))
sumPosR p p' r s = inv (posPairR p') .~ (r -|-~ s) .~ posPairR p