content: {- |
  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")
  