{- |
Module      :  Control.Comonad.Sheet.Reference
Description :  Relative and absolute references to locations in arbitrary-dimensional sheets.
Copyright   :  Copyright (c) 2014 Kenneth Foner

Maintainer  :  kenneth.foner@gmail.com
Stability   :  experimental
Portability :  non-portable

This module defines the types needed to construct and manipulate references to locations in n-dimensional sheets.
All sheets support relative references, but only 'Indexed' sheets support absolute references; the type system prevents
the use of absolute references for sheets without an index.
-}

{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE StandaloneDeriving    #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}

module Control.Comonad.Sheet.Reference where

import Data.Numeric.Witness.Peano
import Data.List.Indexed

import Control.Applicative
import Data.List ( intercalate )

import Prelude hiding ( replicate , length )

-- | A 'Ref' is either absolute or relative. This type exists solely to be lifted to the type/kind level.
data RefType = Relative | Absolute

-- | A @Ref@ is either absolute or relative. Either holds an @Int@, but their semantics differ.
data Ref (t :: RefType) where
   Rel :: Int -> Ref Relative
   Abs :: Int -> Ref Absolute
deriving instance Show (Ref t)

-- | Extract the raw @Int@ from a @Ref@. Use this sparingly, as every time you do, you risk accidentally converting
--   to the other variety of @Ref@ if you're not careful.
getRef :: Ref t -> Int
getRef (Abs x) = x
getRef (Rel x) = x

instance Enum (Ref Relative) where
   fromEnum (Rel r) = r
   toEnum = Rel

instance Enum (Ref Absolute) where
   fromEnum (Abs r) = r
   toEnum = Abs

-- | Two absolute references cannot be combined into a single reference, but relative and absolute references can be
--   combined to form an absolute reference, and two relative references can be combined into one relative reference.
type family Combine a b where
   Combine Relative Absolute = Absolute
   Combine Absolute Relative = Absolute
   Combine Relative Relative = Relative

-- | Combine @Ref@s which can be meaningfully combined. Note the absence of the absolute-absolute case; there's no
--   good meaning for combining two absolute references, so it is statically prohibited.
class CombineRefs a b where
   combine :: Ref a -> Ref b -> Ref (Combine a b)
instance CombineRefs Absolute Relative where
   combine (Abs a) (Rel b) = Abs (a + b)
instance CombineRefs Relative Absolute where
   combine (Rel a) (Abs b) = Abs (a + b)
instance CombineRefs Relative Relative where
   combine (Rel a) (Rel b) = Rel (a + b)

-- | A @RefList@ is a list of @Ref@s, each of which may be individually relative or absolute.
type RefList = ConicList Ref

infixr 4 &
type family a & b where
   (a :-: as) & (b :-: bs) = Combine a b :-: (as & bs)
   Nil        & bs         = bs
   as         & Nil        = as

-- | We can combine lists of references if their corresponding elements can be combined. When combining two lists of
--   references, any trailing elements from the longer list will be preserved at the end; this is /unlike/ the behavior
--   of, e.g., @zip@.
class CombineRefLists as bs where
   (&) :: RefList as -> RefList bs -> RefList (as & bs)
instance (CombineRefs a b, CombineRefLists as bs)
      => CombineRefLists (a :-: as) (b :-: bs) where (a :-: as) & (b :-: bs) = combine a b :-: (as & bs)
instance CombineRefLists Nil        (b :-: bs) where ConicNil & bs           = bs
instance CombineRefLists (a :-: as) Nil        where as       & ConicNil     = as
instance CombineRefLists Nil        Nil        where ConicNil & ConicNil     = ConicNil

-- | Given a homogeneous list of length n containing relative references, we can merge those relative positions with a
--   homogeneous list of absolute references. This yields another list of absolute references.
merge :: (ReifyNatural n)
      => CountedList n (Ref Relative)
      -> CountedList n (Ref Absolute)
      -> CountedList n (Ref Absolute)
merge rs as = (\(Rel r) (Abs a) -> Abs (r + a)) <$> rs <*> as

-- | Finds the relative movement necessary to move from a given absolute coordinate to the location specified by a
--   list of relative and absolute coordinates.
diff :: CountedList n (Either (Ref Relative) (Ref Absolute))
     -> CountedList n (Ref Absolute)
     -> CountedList n (Ref Relative)
diff (Left  (Rel r) ::: rs) (Abs i ::: is) = Rel  r      ::: diff rs is
diff (Right (Abs r) ::: rs) (Abs i ::: is) = Rel (r - i) ::: diff rs is
diff CountedNil _  = CountedNil
diff _  CountedNil = CountedNil

-- | Given a list of relative and absolute references (an n-dimensional reference) and an n-dimensional coordinate,
--   we can obtain the relative movement necessary to get from the coordinate to the location specified by the 
--   references given.
getMovement :: (Length ts <= n, ((n - Length ts) + Length ts) ~ n)
            => RefList ts -> CountedList n (Ref Absolute) -> CountedList n (Ref Relative)
getMovement refs coords =
   padTo (count coords) (Left (Rel 0)) (homogenize eitherFromRef refs) `diff` coords

-- | Given a @Ref@, forget the type-level information about whether it's absolute or relative by casting it into an
--   @Either@ type where the @Left@ branch holds a relative reference or the @Right@ holds an absolute one.
eitherFromRef :: Ref t -> Either (Ref Relative) (Ref Absolute)
eitherFromRef (Rel r) = Left  (Rel r)
eitherFromRef (Abs a) = Right (Abs a)

-- | Given a number /n/ greater than zero and some reference, prepend (n - 1) relative references of value zero to the
--   reference given, thus creating an n-dimensional reference where the original reference refers to the nth dimension.
dimensional :: Natural (Succ n) -> Ref t -> RefList (Tack t (Replicate n Relative))
dimensional (Succ n) a = tack a (heterogenize id (replicate n (Rel 0)))

instance Show (RefList ts) where
   showsPrec p xs = showParen (p > 10) $
      (showString $ ( intercalate " :-: "
                    $ map (either show show)
                    $ unCount
                    $ homogenize eitherFromRef xs ) ++ " :-: ConicNil")