{-|
Module : Sheet
Description : Spreadsheets, what else?
Maintainer : gatlin@niltag.net

A 'Sheet' is a multi-dimensional convolutional computational space.
The fabric of the universe comes in sheets like this but with a higher thread-
count.

Re-implementation of Kenneth Foner's @ComonadSheet@ library.
Some bug fixes and packaging upgrades have been made; additionally, for
idiosyncratic reasons, where possible functional dependencies have been replaced
with associated type families.
-}

{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances, TypeFamilies, TypeOperators #-}
{-# LANGUAGE RankNTypes, ExistentialQuantification, ScopedTypeVariables #-}
{-# LANGUAGE PolyKinds, DataKinds, ConstraintKinds #-}
{-# LANGUAGE StandaloneDeriving, InstanceSigs, BangPatterns #-}

module Sheet
    ( -- * Defining and executing sheets.
      evaluate
    , evaluateF
    , cell
    , cells
    , sheet
    , change
    , sheetFromNested
    , indexedSheet
      -- * Inexhaustible streams
    , Stream(..)
    , (<:>)
    , repeat
    , zipWith
    , unzip
    , iterateStream
    , unfoldStream
    , takeStream
    , takeStreamNat
      -- * Tapes: bidirectional streams with a focus
    , Tape(..)
    , tapeOf
    , moveL
    , moveR
    , iterate
    , enumerate
    , unfold
      -- * References, indices, and coordinates
    , Ref(..)
    , getRef
    , CombineRefTypes(..)
    , RefType(..)
      -- * Reference lists
    , RefList
    , CombineRefLists(..)
    , merge
    , diff
    , eitherFromRef
    , getMovement
    , dimensional
      -- ** Coordinates
    , Coordinate
    , Indexed(..)
    , Cross(..)
      -- ** Indexed
    , Indexable
    , indices
      -- * Type-level 'Tape' manipulation with 'Coordinate's and 'Ref's.
      -- ** Take
    , Take(..)
    , tapeTake
      -- ** View
    , View(..)
    , tapeView
      -- ** Go
    , Go(..)
    , tapeGo
    , Signed(..)
      -- * Insertion
    , InsertBase(..)
    , InsertNested(..)
    , AddNest
    , AsNestedAs
      -- * Dimensions
    , DimensionalAs(..)
    , slice
    , insert
      -- ** First Dimension
    , Abs1
    , Rel1
    , Nat1
    , nat1
    , Sheet1
    , ISheet1
    , here1
    , d1
    , columnAt
    , column
    , rightBy
    , leftBy
    , right
    , left
      -- ** Second Dimension
    , Abs2
    , Rel2
    , Nat2
    , nat2
    , Sheet2
    , ISheet2
    , here2
    , d2
    , rowAt
    , row
    , belowBy
    , aboveBy
    , above
    , below
      -- ** Third Dimension
    , Abs3
    , Rel3
    , Nat3
    , nat3
    , Sheet3
    , ISheet3
    , here3
    , d3
    , levelAt
    , level
    , outwardBy
    , inwardBy
    , outward
    , inward
      -- ** Fourth Dimension
    , Abs4
    , Rel4
    , Nat4
    , nat4
    , Sheet4
    , ISheet4
    , here4
    , d4
    , spaceAt
    , space
    , anaBy
    , cataBy
    , ana
    , cata
      -- * Utilities
    , (&&&)
    )
where

import Peano
  ( S
  , Z
  , Natural(..)
  , ReifyNatural(..)
  , type (<)
  , type (<=)
  , type (+)
  , type (-)
  )
import Nested
  ( Nested (..)
  , F
  , N
  , UnNest
  , unNest
  , NestedCountable(type NestedCount)
  , NestedNTimes
  )
import Lists
  ( Counted(..)
  , count
  , padTo
  , replicate
  , Conic(..)
  , Nil
  , (:-:)
  , nth
  , heterogenize
  , homogenize
  , Tackable(type Tack, tack)
  , HasLength(type Length)
  , Replicable(type Replicate)
  )

import Prelude hiding ( repeat
                      , zipWith
                      , iterate
                      , replicate
                      , take
                      , unzip
                      )
import qualified Prelude as P

import qualified Data.List as L

import Control.Monad
import Control.Applicative
import Control.Comonad
import Data.Bifunctor (bimap)
import Data.Profunctor
import Data.Distributive
import Data.Functor ((<&>))
import Data.Functor.Rep (Representable(..), distributeRep)
import Data.Foldable
import Data.Kind (Type)

-- = Util

(&&&) :: (t -> a) -> (t -> b) -> t -> (a, b)
t -> a
f &&& :: forall t a b. (t -> a) -> (t -> b) -> t -> (a, b)
&&& t -> b
g = \t
v -> (t -> a
f t
v, t -> b
g t
v)

-- = Stream

-- | A 'Stream t' is an inexhaustible source of values of type @t@.
-- Unlike the ordinary builtin list type '[]' a 'Stream' cannot ever be empty
-- or exhausted.
data Stream t = Cons t (Stream t)
--deriving instance Functor Stream
deriving instance (Show t) => Show (Stream t)

(<:>) :: t -> Stream t -> Stream t
<:> :: forall t. t -> Stream t -> Stream t
(<:>) = forall t. t -> Stream t -> Stream t
Cons

-- | Construct an infinite 'Stream a' from a value of type @a@.
repeat :: t -> Stream t
repeat :: forall t. t -> Stream t
repeat t
x = forall t. t -> Stream t -> Stream t
Cons t
x (forall t. t -> Stream t
repeat t
x)

-- | Combines two infinite streams element-wise using the provided function.
zipWith :: (a -> b -> c) -> Stream a -> Stream b -> Stream c
zipWith :: forall a b c. (a -> b -> c) -> Stream a -> Stream b -> Stream c
zipWith a -> b -> c
f ~(Cons a
x Stream a
xs) ~(Cons b
y Stream b
ys) = let !fxy :: c
fxy = a -> b -> c
f a
x b
y in forall t. t -> Stream t -> Stream t
Cons c
fxy (forall a b c. (a -> b -> c) -> Stream a -> Stream b -> Stream c
zipWith a -> b -> c
f Stream a
xs Stream b
ys)

unzip :: Stream (a, b) -> (Stream a, Stream b)
unzip :: forall a b. Stream (a, b) -> (Stream a, Stream b)
unzip ~(Cons ~(!a
x, !b
y) Stream (a, b)
xys) = forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (forall t. t -> Stream t -> Stream t
Cons a
x) (forall t. t -> Stream t -> Stream t
Cons b
y) (Stream a, Stream b)
xys' where
  xys' :: (Stream a, Stream b)
xys' = forall a b. Stream (a, b) -> (Stream a, Stream b)
unzip Stream (a, b)
xys

-- | Repeatedly apply a 'step' function to an initial @value@ to generate the
-- next @value@
iterateStream :: (value -> value) -> value -> Stream value
iterateStream :: forall value. (value -> value) -> value -> Stream value
iterateStream value -> value
step value
v = forall t. t -> Stream t -> Stream t
Cons value
v (forall value. (value -> value) -> value -> Stream value
iterateStream value -> value
step (value -> value
step value
v))

unfoldStream
  :: (state -> (value, state))
  -> state
  -> Stream value
unfoldStream :: forall state value.
(state -> (value, state)) -> state -> Stream value
unfoldStream state -> (value, state)
step state
state =
  let (value
result, state
state') = state -> (value, state)
step state
state
  in  forall t. t -> Stream t -> Stream t
Cons value
result (forall state value.
(state -> (value, state)) -> state -> Stream value
unfoldStream state -> (value, state)
step state
state')

-- | Prepends an exhaustible stream ('[value]') to an inexhaustible stream
-- '(Stream value)'.
prefixStream :: [value] -> Stream value -> Stream value
prefixStream :: forall value. [value] -> Stream value -> Stream value
prefixStream [value]
xs Stream value
ys = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall t. t -> Stream t -> Stream t
Cons Stream value
ys [value]
xs

-- | Capture 'n' values from an infinite 'Stream value'.
takeStream :: Int -> Stream value -> [value]
takeStream :: forall value. Int -> Stream value -> [value]
takeStream Int
n ~(Cons value
x Stream value
xs)
  | Int
n forall a. Eq a => a -> a -> Bool
== Int
0 = []
  | Int
n forall a. Ord a => a -> a -> Bool
>  Int
0 = value
x forall a. a -> [a] -> [a]
: forall value. Int -> Stream value -> [value]
takeStream (Int
n forall a. Num a => a -> a -> a
- Int
1) Stream value
xs
  | Bool
otherwise = forall a. HasCallStack => String -> a
error String
"takeStream: negative argument"

-- | Alternate implementation of 'takeStream' which trades the inelegance but
-- convenience of @error@ for the type safety and inconvenience of requiring
-- some kind of evil type witness to convey how many items to grab from the
-- 'Stream value'.
takeStreamNat
  :: (Z < S n)
  => Natural n
  -> Stream value
  -> [value]
takeStreamNat :: forall n value. (Z < S n) => Natural n -> Stream value -> [value]
takeStreamNat Natural n
Zero Stream value
_ = []
takeStreamNat (Succ Natural t
n) ~(Cons value
x Stream value
xs) = value
x forall a. a -> [a] -> [a]
: forall n value. (Z < S n) => Natural n -> Stream value -> [value]
takeStreamNat Natural t
n Stream value
xs

instance Functor Stream where
  fmap :: forall a b. (a -> b) -> Stream a -> Stream b
fmap !a -> b
f ~(Cons !a
x Stream a
xs) =
    let !x' :: b
x' = a -> b
f a
x
        xs' :: Stream b
xs' = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f Stream a
xs
    in  forall t. t -> Stream t -> Stream t
Cons b
x' Stream b
xs'

instance Applicative Stream where
  pure :: forall t. t -> Stream t
pure = forall t. t -> Stream t
repeat
  <*> :: forall a b. Stream (a -> b) -> Stream a -> Stream b
(<*>) = forall a b c. (a -> b -> c) -> Stream a -> Stream b -> Stream c
zipWith forall a b. (a -> b) -> a -> b
($)

instance Monad Stream where
  return :: forall t. t -> Stream t
return = forall (f :: * -> *) a. Applicative f => a -> f a
pure
  Stream a
s >>= :: forall a b. Stream a -> (a -> Stream b) -> Stream b
>>= a -> Stream b
f = forall a. Stream (Stream a) -> Stream a
_join (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Stream b
f Stream a
s)
    where _join :: Stream (Stream a) -> Stream a
          _join :: forall a. Stream (Stream a) -> Stream a
_join ~(Cons Stream a
xs Stream (Stream a)
xss) =
            forall t. t -> Stream t -> Stream t
Cons (forall (w :: * -> *) a. Comonad w => w a -> a
extract Stream a
xs) (forall a. Stream (Stream a) -> Stream a
_join (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ (Cons a
_ Stream a
t1) -> Stream a
t1) Stream (Stream a)
xss))

instance Comonad Stream where
  extract :: forall a. Stream a -> a
extract (Cons !a
x Stream a
_) = a
x
  duplicate :: forall a. Stream a -> Stream (Stream a)
duplicate s :: Stream a
s@(Cons a
_ Stream a
xs) = let xs' :: Stream (Stream a)
xs' = forall (w :: * -> *) a. Comonad w => w a -> w (w a)
duplicate Stream a
xs in forall t. t -> Stream t -> Stream t
Cons Stream a
s Stream (Stream a)
xs'

instance ComonadApply Stream where
  <@> :: forall a b. Stream (a -> b) -> Stream a -> Stream b
(<@>) = forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
(<*>)

-- = Tape

-- | Two infinite 'Stream's of type @a@ joined with a center value in 'focus'.
-- A 'Tape' is named for tape in a Turing machine.
data Tape a = Tape
  { forall a. Tape a -> Stream a
viewL :: Stream a
  , forall a. Tape a -> a
focus :: a
  , forall a. Tape a -> Stream a
viewR :: Stream a
  } -- deriving (Functor)

-- | Utilities to move a 'Tape' one cell to the left or right.
moveL, moveR :: Tape a -> Tape a
moveL :: forall a. Tape a -> Tape a
moveL ~(Tape ~(Cons a
l Stream a
ls) a
c Stream a
rs) = forall a. Stream a -> a -> Stream a -> Tape a
Tape Stream a
ls a
l (forall t. t -> Stream t -> Stream t
Cons a
c Stream a
rs)
moveR :: forall a. Tape a -> Tape a
moveR ~(Tape Stream a
ls a
c ~(Cons a
r Stream a
rs)) = forall a. Stream a -> a -> Stream a -> Tape a
Tape (forall t. t -> Stream t -> Stream t
Cons a
c Stream a
ls) a
r Stream a
rs

-- | Builds a 'Tape' out of two generator functions and an initial seed value.
-- 'prev' will generate the left-hand 'Stream' while 'next' will generate the
-- right-hand 'Stream'.
iterate :: (t -> t) -> (t -> t) -> t -> Tape t
iterate :: forall t. (t -> t) -> (t -> t) -> t -> Tape t
iterate t -> t
prev t -> t
next t
seed =
  forall a. Stream a -> a -> Stream a -> Tape a
Tape
    (forall value. (value -> value) -> value -> Stream value
iterateStream t -> t
prev (t -> t
prev t
seed))
    t
seed
    (forall value. (value -> value) -> value -> Stream value
iterateStream t -> t
next (t -> t
next t
seed))

-- | Unfolds a 'Tape' from two 'Stream' unfold functions, a function to generate
-- the initial 'focus', and a seed value.
unfold
  :: (c -> (a, c))
  -> (c -> a)
  -> (c -> (a, c))
  -> c
  -> Tape a
unfold :: forall c a.
(c -> (a, c)) -> (c -> a) -> (c -> (a, c)) -> c -> Tape a
unfold c -> (a, c)
prev c -> a
center c -> (a, c)
next c
seed =
  forall a. Stream a -> a -> Stream a -> Tape a
Tape
    (forall state value.
(state -> (value, state)) -> state -> Stream value
unfoldStream c -> (a, c)
prev c
seed)
    (c -> a
center c
seed)
    (forall state value.
(state -> (value, state)) -> state -> Stream value
unfoldStream c -> (a, c)
next c
seed)

-- | Constructs a 'Tape' from any 'Enum'erable type.
enumerate :: (Enum a) => a -> Tape a
enumerate :: forall a. Enum a => a -> Tape a
enumerate = forall t. (t -> t) -> (t -> t) -> t -> Tape t
iterate forall a. Enum a => a -> a
pred forall a. Enum a => a -> a
succ

instance Functor Tape where
  fmap :: forall a b. (a -> b) -> Tape a -> Tape b
fmap !a -> b
f ~(Tape !Stream a
ls !a
c !Stream a
rs) = forall a. Stream a -> a -> Stream a -> Tape a
Tape Stream b
ls' b
c' Stream b
rs' where
    !ls' :: Stream b
ls' = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ (!a
l) -> a -> b
f a
l) Stream a
ls
    !rs' :: Stream b
rs' = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ (!a
r) -> a -> b
f a
r) Stream a
rs
    !c' :: b
c' = a -> b
f a
c

instance Comonad Tape where
  extract :: forall a. Tape a -> a
extract = forall a. Tape a -> a
focus
  duplicate :: forall a. Tape a -> Tape (Tape a)
duplicate = forall t. (t -> t) -> (t -> t) -> t -> Tape t
iterate forall a. Tape a -> Tape a
moveL forall a. Tape a -> Tape a
moveR

instance ComonadApply Tape where
  ~(Tape Stream (a -> b)
ls a -> b
c Stream (a -> b)
rs) <@> :: forall a b. Tape (a -> b) -> Tape a -> Tape b
<@> ~(Tape Stream a
ls' !a
c' Stream a
rs') =
    forall a. Stream a -> a -> Stream a -> Tape a
Tape (Stream (a -> b)
ls forall (w :: * -> *) a b.
ComonadApply w =>
w (a -> b) -> w a -> w b
<@> Stream a
ls') (a -> b
c a
c') (Stream (a -> b)
rs forall (w :: * -> *) a b.
ComonadApply w =>
w (a -> b) -> w a -> w b
<@> Stream a
rs')

instance Applicative Tape where
  <*> :: forall a b. Tape (a -> b) -> Tape a -> Tape b
(<*>) = forall (w :: * -> *) a b.
ComonadApply w =>
w (a -> b) -> w a -> w b
(<@>)
  pure :: forall a. a -> Tape a
pure = forall a. Stream a -> a -> Stream a -> Tape a
Tape forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. a -> a
id forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure

instance Distributive Tape where
  distribute :: forall (f :: * -> *) a. Functor f => f (Tape a) -> Tape (f a)
distribute =
    forall c a.
(c -> (a, c)) -> (c -> a) -> (c -> (a, c)) -> c -> Tape a
unfold
      (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (w :: * -> *) a. Comonad w => w a -> a
extract forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Tape a -> Tape a
moveL) forall t a b. (t -> a) -> (t -> b) -> t -> (a, b)
&&& forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Tape a -> Tape a
moveL)
      (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (w :: * -> *) a. Comonad w => w a -> a
extract)
      (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (w :: * -> *) a. Comonad w => w a -> a
extract forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Tape a -> Tape a
moveR) forall t a b. (t -> a) -> (t -> b) -> t -> (a, b)
&&& forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Tape a -> Tape a
moveR)

instance Representable Tape where
  type Rep Tape = Int
  index :: forall a. Tape a -> Rep Tape -> a
index !Tape a
t Rep Tape
0 = let t' :: a
t' = forall (w :: * -> *) a. Comonad w => w a -> a
extract Tape a
t in a
t'
  index !Tape a
t !Rep Tape
n
    | Rep Tape
n forall a. Ord a => a -> a -> Bool
> Int
0 = let
                !moveR_t :: Tape a
moveR_t = forall a. Tape a -> Tape a
moveR Tape a
t
                !moved :: a
moved = forall (f :: * -> *) a. Representable f => f a -> Rep f -> a
index Tape a
moveR_t forall a b. (a -> b) -> a -> b
$! Rep Tape
nforall a. Num a => a -> a -> a
-Int
1
              in a
moved
    | Rep Tape
n forall a. Ord a => a -> a -> Bool
< Int
0 = let
                !moveL_t :: Tape a
moveL_t = forall a. Tape a -> Tape a
moveL Tape a
t
                !moved :: a
moved = forall (f :: * -> *) a. Representable f => f a -> Rep f -> a
index Tape a
moveL_t forall a b. (a -> b) -> a -> b
$! Rep Tape
nforall a. Num a => a -> a -> a
+Int
1
              in a
moved
    | Bool
otherwise = let !t' :: a
t' = forall (w :: * -> *) a. Comonad w => w a -> a
extract Tape a
t in a
t'
  {-# INLINABLE index #-}
  tabulate :: forall a. (Rep Tape -> a) -> Tape a
tabulate Rep Tape -> a
describe =
    let !t :: Tape Int
t = forall a. Enum a => a -> Tape a
enumerate Int
0
        !t' :: Tape a
t' = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Rep Tape -> a
describe Tape Int
t
    in Tape a
t'

-- | 'Tape' unit.
tapeOf :: a -> Tape a
tapeOf :: forall a. a -> Tape a
tapeOf = forall (f :: * -> *) a. Applicative f => a -> f a
pure

-- = References

-- | There are two kinds reference types: 'Relative' and 'Absolute'.
data RefType = Relative | Absolute

-- | A @Ref@ is indexed by a @RefType@ kind (confusing name, to be sure) and
-- represents some unique value. Here that unique value is carried by an @Int@
-- property.
-- An absolute reference denotes a coordinate in a fixed frame of reference.
-- A relative reference denotes some distance to be applied to another anchor
-- reference (relative or absolute).
data Ref (t :: RefType)
  = (t ~ 'Relative) => Rel Int
  | (t ~ 'Absolute) => Abs Int
deriving instance Show (Ref t)
deriving instance Eq (Ref t)
deriving instance Ord (Ref t)

instance Num (Ref 'Relative) where
  Rel Int
x + :: Ref 'Relative -> Ref 'Relative -> Ref 'Relative
+ Rel Int
y = forall (t :: RefType). (t ~ 'Relative) => Int -> Ref t
Rel (Int
x forall a. Num a => a -> a -> a
+ Int
y)
  Rel Int
x * :: Ref 'Relative -> Ref 'Relative -> Ref 'Relative
* Rel Int
y = forall (t :: RefType). (t ~ 'Relative) => Int -> Ref t
Rel (Int
x forall a. Num a => a -> a -> a
* Int
y)
  abs :: Ref 'Relative -> Ref 'Relative
abs (Rel Int
x)   = forall (t :: RefType). (t ~ 'Relative) => Int -> Ref t
Rel (forall a. Num a => a -> a
abs Int
x)
  negate :: Ref 'Relative -> Ref 'Relative
negate (Rel Int
x) = forall (t :: RefType). (t ~ 'Relative) => Int -> Ref t
Rel (forall a. Num a => a -> a
negate Int
x)
  signum :: Ref 'Relative -> Ref 'Relative
signum (Rel Int
x) = forall (t :: RefType). (t ~ 'Relative) => Int -> Ref t
Rel (forall a. Num a => a -> a
signum Int
x)
  fromInteger :: Integer -> Ref 'Relative
fromInteger = forall (t :: RefType). (t ~ 'Relative) => Int -> Ref t
Rel forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral

instance Num (Ref 'Absolute) where
  Abs Int
x + :: Ref 'Absolute -> Ref 'Absolute -> Ref 'Absolute
+ Abs Int
y = forall (t :: RefType). (t ~ 'Absolute) => Int -> Ref t
Abs (Int
x forall a. Num a => a -> a -> a
+ Int
y)
  Abs Int
x * :: Ref 'Absolute -> Ref 'Absolute -> Ref 'Absolute
* Abs Int
y = forall (t :: RefType). (t ~ 'Absolute) => Int -> Ref t
Abs (Int
x forall a. Num a => a -> a -> a
* Int
y)
  abs :: Ref 'Absolute -> Ref 'Absolute
abs (Abs Int
x)   = forall (t :: RefType). (t ~ 'Absolute) => Int -> Ref t
Abs (forall a. Num a => a -> a
abs Int
x)
  negate :: Ref 'Absolute -> Ref 'Absolute
negate (Abs Int
x) = forall (t :: RefType). (t ~ 'Absolute) => Int -> Ref t
Abs (forall a. Num a => a -> a
negate Int
x)
  signum :: Ref 'Absolute -> Ref 'Absolute
signum (Abs Int
x) = forall (t :: RefType). (t ~ 'Absolute) => Int -> Ref t
Abs (forall a. Num a => a -> a
signum Int
x)
  fromInteger :: Integer -> Ref 'Absolute
fromInteger = forall (t :: RefType). (t ~ 'Absolute) => Int -> Ref t
Abs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral

instance Enum (Ref 'Relative) where
  fromEnum :: Ref 'Relative -> Int
fromEnum (Rel Int
r) = Int
r
  toEnum :: Int -> Ref 'Relative
toEnum = forall (t :: RefType). (t ~ 'Relative) => Int -> Ref t
Rel

instance Enum (Ref 'Absolute) where
  fromEnum :: Ref 'Absolute -> Int
fromEnum (Abs Int
r) = Int
r
  toEnum :: Int -> Ref 'Absolute
toEnum = forall (t :: RefType). (t ~ 'Absolute) => Int -> Ref t
Abs

-- | For when we want to throw away the type information and access the raw
-- @Int@ value beneath the @Ref@.
getRef :: Ref t -> Int
getRef :: forall (t :: RefType). Ref t -> Int
getRef (Abs Int
x) = Int
x
getRef (Rel Int
x) = Int
x

class CombineRefTypes (a :: RefType) (b :: RefType) where
  type Combine a b :: RefType
  combine :: Ref a -> Ref b -> Ref (Combine a b)

instance CombineRefTypes 'Absolute 'Relative where
  type Combine 'Absolute 'Relative = 'Absolute
  combine :: Ref 'Absolute -> Ref 'Relative -> Ref (Combine 'Absolute 'Relative)
combine (Abs Int
a) (Rel Int
b) = forall (t :: RefType). (t ~ 'Absolute) => Int -> Ref t
Abs (Int
a forall a. Num a => a -> a -> a
+ Int
b)

instance CombineRefTypes 'Relative 'Absolute where
  type Combine 'Relative 'Absolute = 'Absolute
  combine :: Ref 'Relative -> Ref 'Absolute -> Ref (Combine 'Relative 'Absolute)
combine (Rel Int
a) (Abs Int
b) = forall (t :: RefType). (t ~ 'Absolute) => Int -> Ref t
Abs (Int
a forall a. Num a => a -> a -> a
+ Int
b)

instance CombineRefTypes 'Relative 'Relative where
  type Combine 'Relative 'Relative = 'Relative
  combine :: Ref 'Relative -> Ref 'Relative -> Ref (Combine 'Relative 'Relative)
combine (Rel Int
a) (Rel Int
b) = forall (t :: RefType). (t ~ 'Relative) => Int -> Ref t
Rel (Int
a forall a. Num a => a -> a -> a
+ Int
b)

-- | A 'RefList' is a 'Conic' list of references.
type RefList = Conic Ref

infixr 4 &
-- | Type family permitting the combination of 'Conic' lists.
-- This is handy as a 'RefList' is a 'Conic' list!
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.
class CombineRefLists as bs where
  (&) :: RefList as -> RefList bs -> RefList (as & bs)

instance ( CombineRefTypes a b
         , CombineRefLists as bs )
  => CombineRefLists (a :-: as) (b :-: bs) where
  (Ref a
a :-: Conic Ref rest
as) & :: RefList (a :-: as)
-> RefList (b :-: bs) -> RefList ((a :-: as) & (b :-: bs))
& (Ref a
b :-: Conic Ref rest
bs) = forall (a :: RefType) (b :: RefType).
CombineRefTypes a b =>
Ref a -> Ref b -> Ref (Combine a b)
combine Ref a
a Ref a
b forall {k} (f :: k -> *) ts rest (a :: k).
(ts ~ (a :-: rest)) =>
f a -> Conic f rest -> Conic f ts
:-: (Conic Ref rest
as forall as bs.
CombineRefLists as bs =>
RefList as -> RefList bs -> RefList (as & bs)
& Conic Ref rest
bs)

instance CombineRefLists Nil (b :-: bs) where
  RefList Nil
ConicNil & :: RefList Nil -> RefList (b :-: bs) -> RefList (Nil & (b :-: bs))
& RefList (b :-: bs)
bs = RefList (b :-: bs)
bs

instance CombineRefLists (a :-: as) Nil where
  RefList (a :-: as)
as & :: RefList (a :-: as) -> RefList Nil -> RefList ((a :-: as) & Nil)
& RefList Nil
ConicNil = RefList (a :-: as)
as

instance CombineRefLists Nil Nil where
  RefList Nil
ConicNil & :: RefList Nil -> RefList Nil -> RefList (Nil & Nil)
& RefList Nil
ConicNil = forall {k} (f :: k -> *) ts. (ts ~ Nil) => Conic f ts
ConicNil

-- | Given a homogenous list of length n containing relative references, we can
-- merge those relative positions with a homogenous list of absolute
-- references.
merge
  :: (ReifyNatural n)
  => Counted n (Ref 'Relative)
  -> Counted n (Ref 'Absolute)
  -> Counted n (Ref 'Absolute)
merge :: forall n.
ReifyNatural n =>
Counted n (Ref 'Relative)
-> Counted n (Ref 'Absolute) -> Counted n (Ref 'Absolute)
merge Counted n (Ref 'Relative)
rs Counted n (Ref 'Absolute)
as = (\ (Rel Int
r) (Abs Int
a) -> forall (t :: RefType). (t ~ 'Absolute) => Int -> Ref t
Abs (Int
r forall a. Num a => a -> a -> a
+ Int
a)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Counted n (Ref 'Relative)
rs forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Counted n (Ref 'Absolute)
as

-- | Finds the relative movement necessary to move from a given absolute
-- coordinate to the location specified by a list of a relative and absolute
-- coordinates.
diff
  :: Counted n (Either (Ref 'Relative) (Ref 'Absolute))
  -> Counted n (Ref 'Absolute)
  -> Counted n (Ref 'Relative)
diff :: forall n.
Counted n (Either (Ref 'Relative) (Ref 'Absolute))
-> Counted n (Ref 'Absolute) -> Counted n (Ref 'Relative)
diff (Left (Rel Int
r) ::: Counted t (Either (Ref 'Relative) (Ref 'Absolute))
rs) (Abs Int
_ ::: Counted t (Ref 'Absolute)
is) = forall (t :: RefType). (t ~ 'Relative) => Int -> Ref t
Rel Int
r forall n a t. (n ~ S t) => a -> Counted t a -> Counted n a
::: forall n.
Counted n (Either (Ref 'Relative) (Ref 'Absolute))
-> Counted n (Ref 'Absolute) -> Counted n (Ref 'Relative)
diff Counted t (Either (Ref 'Relative) (Ref 'Absolute))
rs Counted t (Ref 'Absolute)
is
diff (Right (Abs Int
r) ::: Counted t (Either (Ref 'Relative) (Ref 'Absolute))
rs) (Abs Int
i ::: Counted t (Ref 'Absolute)
is) = forall (t :: RefType). (t ~ 'Relative) => Int -> Ref t
Rel (Int
r forall a. Num a => a -> a -> a
- Int
i) forall n a t. (n ~ S t) => a -> Counted t a -> Counted n a
::: forall n.
Counted n (Either (Ref 'Relative) (Ref 'Absolute))
-> Counted n (Ref 'Absolute) -> Counted n (Ref 'Relative)
diff Counted t (Either (Ref 'Relative) (Ref 'Absolute))
rs Counted t (Ref 'Absolute)
is
diff Counted n (Either (Ref 'Relative) (Ref 'Absolute))
CountedNil Counted n (Ref 'Absolute)
_ = forall n a. (n ~ Z) => Counted n a
CountedNil

-- | Given a @Ref@, forget the type-level information about whether it's
-- absolute or relative by casting it into an Either type, with the left branch
-- holding relative reference and the right branch absolute.
eitherFromRef :: Ref t -> Either (Ref 'Relative) (Ref 'Absolute)
eitherFromRef :: forall (t :: RefType).
Ref t -> Either (Ref 'Relative) (Ref 'Absolute)
eitherFromRef (Rel Int
r) = forall a b. a -> Either a b
Left (forall (t :: RefType). (t ~ 'Relative) => Int -> Ref t
Rel Int
r)
eitherFromRef (Abs Int
a) = forall a b. b -> Either a b
Right (forall (t :: RefType). (t ~ 'Absolute) => Int -> Ref t
Abs Int
a)

-- | 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
  -> Counted n (Ref 'Absolute)
  -> Counted n (Ref 'Relative)
getMovement :: forall ts n.
(Length ts <= n, ((n - Length ts) + Length ts) ~ n) =>
RefList ts
-> Counted n (Ref 'Absolute) -> Counted n (Ref 'Relative)
getMovement RefList ts
refs Counted n (Ref 'Absolute)
coords =
  forall m n x.
(m <= n) =>
Natural n -> x -> Counted m x -> Counted ((n - m) + m) x
padTo (forall n a. Counted n a -> Natural n
count Counted n (Ref 'Absolute)
coords) (forall a b. a -> Either a b
Left (forall (t :: RefType). (t ~ 'Relative) => Int -> Ref t
Rel Int
0)) (forall {k} (f :: k -> *) a ts.
(forall (t :: k). f t -> a) -> Conic f ts -> Counted (Length ts) a
homogenize forall (t :: RefType).
Ref t -> Either (Ref 'Relative) (Ref 'Absolute)
eitherFromRef RefList ts
refs) forall n.
Counted n (Either (Ref 'Relative) (Ref 'Absolute))
-> Counted n (Ref 'Absolute) -> Counted n (Ref 'Relative)
`diff` Counted n (Ref 'Absolute)
coords

-- | 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 references refers to the nth dimension.
dimensional
  :: (Tackable t (Replicate n 'Relative))
  => Natural (S n)
  -> Ref t
  -> RefList (Tack t (Replicate n 'Relative))
dimensional :: forall (t :: RefType) n.
Tackable t (Replicate n 'Relative) =>
Natural (S n) -> Ref t -> RefList (Tack t (Replicate n 'Relative))
dimensional (Succ Natural t
n) Ref t
a  = forall k (x :: k) xs (f :: k -> *).
Tackable x xs =>
f x -> Conic f xs -> Conic f (Tack x xs)
tack Ref t
a (forall {k} a (f :: k -> *) (t :: k) n.
(a -> f t) -> Counted n a -> Conic f (Replicate n t)
heterogenize forall a. a -> a
id (forall n x. Natural n -> x -> Counted n x
replicate Natural t
n (forall (t :: RefType). (t ~ 'Relative) => Int -> Ref t
Rel Int
0)))

--  | An 'n'-dimensional vector of 'Absolute' 'Ref'erences.
type Coordinate n = Counted n (Ref 'Absolute)

-- | A 'Nested' functor paired with a valid 'index' to one of its members.
data Indexed ts a = Indexed
  { forall ts a. Indexed ts a -> Coordinate (NestedCount ts)
origin :: Coordinate (NestedCount ts)
  , forall ts a. Indexed ts a -> Nested ts a
unindexed :: Nested ts a
  }

instance Functor (Nested ts) => Functor (Indexed ts) where
  fmap :: forall a b. (a -> b) -> Indexed ts a -> Indexed ts b
fmap a -> b
f (Indexed Coordinate (NestedCount ts)
i Nested ts a
t) = forall ts a.
Coordinate (NestedCount ts) -> Nested ts a -> Indexed ts a
Indexed Coordinate (NestedCount ts)
i (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f Nested ts a
t)

class Cross n t where
  cross :: Counted n (t a) -> Nested (NestedNTimes n t) (Counted n a)

instance (Functor t) => Cross (S Z) t where
  cross :: forall a.
Counted Nat1 (t a) -> Nested (NestedNTimes Nat1 t) (Counted Nat1 a)
cross (t a
t ::: Counted t (t a)
_) = forall fs a (f :: * -> *). (fs ~ F f) => f a -> Nested fs a
Flat forall a b. (a -> b) -> a -> b
$ (forall n a t. (n ~ S t) => a -> Counted t a -> Counted n a
::: forall n a. (n ~ Z) => Counted n a
CountedNil) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t a
t

instance ( Cross (S n) t
         , Functor t
         , Functor (Nested (NestedNTimes (S n) t)) )
    => Cross (S (S n)) t where
  cross :: forall a.
Counted (S (S n)) (t a)
-> Nested (NestedNTimes (S (S n)) t) (Counted (S (S n)) a)
cross (t a
t ::: Counted t (t a)
ts) =
    forall fs a fs' (f :: * -> *).
(fs ~ N fs' f) =>
Nested fs' (f a) -> Nested fs a
Nest forall a b. (a -> b) -> a -> b
$ (\Counted t a
xs -> (forall n a t. (n ~ S t) => a -> Counted t a -> Counted n a
::: Counted t a
xs) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t a
t) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall n (t :: * -> *) a.
Cross n t =>
Counted n (t a) -> Nested (NestedNTimes n t) (Counted n a)
cross Counted t (t a)
ts

type Indexable ts = ( Cross (NestedCount ts) Tape
                    , ts ~ NestedNTimes (NestedCount ts) Tape )

instance (ComonadApply (Nested ts), Indexable ts) => Comonad (Indexed ts) where
  extract :: forall a. Indexed ts a -> a
extract = forall (w :: * -> *) a. Comonad w => w a -> a
extract forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ts a. Indexed ts a -> Nested ts a
unindexed
  duplicate :: forall a. Indexed ts a -> Indexed ts (Indexed ts a)
duplicate Indexed ts a
it = forall ts a.
Coordinate (NestedCount ts) -> Nested ts a -> Indexed ts a
Indexed (forall ts a. Indexed ts a -> Coordinate (NestedCount ts)
origin Indexed ts a
it) forall a b. (a -> b) -> a -> b
$
    forall ts a.
Coordinate (NestedCount ts) -> Nested ts a -> Indexed ts a
Indexed forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall n.
Cross n Tape =>
Coordinate n -> Nested (NestedNTimes n Tape) (Coordinate n)
indices (forall ts a. Indexed ts a -> Coordinate (NestedCount ts)
origin Indexed ts a
it)
      forall (w :: * -> *) a b.
ComonadApply w =>
w (a -> b) -> w a -> w b
<@> forall (w :: * -> *) a. Comonad w => w a -> w (w a)
duplicate (forall ts a. Indexed ts a -> Nested ts a
unindexed Indexed ts a
it)

instance (ComonadApply (Nested ts), Indexable ts)
  => ComonadApply (Indexed ts) where
    (Indexed Coordinate (NestedCount ts)
i Nested ts (a -> b)
fs) <@> :: forall a b. Indexed ts (a -> b) -> Indexed ts a -> Indexed ts b
<@> (Indexed Coordinate (NestedCount ts)
_ Nested ts a
xs) = forall ts a.
Coordinate (NestedCount ts) -> Nested ts a -> Indexed ts a
Indexed Coordinate (NestedCount ts)
i (Nested ts (a -> b)
fs forall (w :: * -> *) a b.
ComonadApply w =>
w (a -> b) -> w a -> w b
<@> Nested ts a
xs)

indices
  :: (Cross n Tape)
  => Coordinate n
  -> Nested (NestedNTimes n Tape) (Coordinate n)
indices :: forall n.
Cross n Tape =>
Coordinate n -> Nested (NestedNTimes n Tape) (Coordinate n)
indices = forall n (t :: * -> *) a.
Cross n t =>
Counted n (t a) -> Nested (NestedNTimes n t) (Counted n a)
cross forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Enum a => a -> Tape a
enumerate

-- | Take all the items between the current 'focus' and the item specified by
-- the 'Relative' 'Ref'erence and return them as a list '[a]'.
tapeTake :: Ref 'Relative -> Tape a -> [a]
tapeTake :: forall a. Ref 'Relative -> Tape a -> [a]
tapeTake (Rel Int
r) Tape a
t | Int
r forall a. Ord a => a -> a -> Bool
> Int
0 = forall a. Tape a -> a
focus Tape a
t forall a. a -> [a] -> [a]
: forall value. Int -> Stream value -> [value]
takeStream Int
r (forall a. Tape a -> Stream a
viewR Tape a
t)
tapeTake (Rel Int
r) Tape a
t | Int
r forall a. Ord a => a -> a -> Bool
< Int
0 = forall a. Tape a -> a
focus Tape a
t forall a. a -> [a] -> [a]
: forall value. Int -> Stream value -> [value]
takeStream (forall a. Num a => a -> a
abs Int
r) (forall a. Tape a -> Stream a
viewL Tape a
t)
tapeTake Ref 'Relative
_ Tape a
_ = []

class Take r t where
  type ListFrom t a
  take :: RefList r -> t a -> ListFrom t a

instance (Take Nil (Nested ts), Functor (Nested ts))
  => Take Nil (Nested (N ts Tape)) where
  type ListFrom (Nested (N ts Tape)) a = ListFrom (Nested ts) [a]
  take :: forall a.
RefList Nil
-> Nested (N ts Tape) a -> ListFrom (Nested (N ts Tape)) a
take RefList Nil
_ = forall r (t :: * -> *) a.
Take r t =>
RefList r -> t a -> ListFrom t a
take (forall (t :: RefType). (t ~ 'Relative) => Int -> Ref t
Rel Int
0 forall {k} (f :: k -> *) ts rest (a :: k).
(ts ~ (a :-: rest)) =>
f a -> Conic f rest -> Conic f ts
:-: forall {k} (f :: k -> *) ts. (ts ~ Nil) => Conic f ts
ConicNil)

instance Take ('Relative :-: Nil) (Nested (F Tape)) where
  type ListFrom (Nested (F Tape)) a = [a]
  take :: forall a.
Conic Ref Rel1 -> Nested (F Tape) a -> ListFrom (Nested (F Tape)) a
take (Ref a
r :-: Conic Ref rest
_) (Flat f a
t) = forall a. Ref 'Relative -> Tape a -> [a]
tapeTake Ref a
r f a
t

instance ( Functor (Nested ts)
         , Take rs (Nested ts) )
  => Take ('Relative :-: rs) (Nested (N ts Tape)) where
  type ListFrom (Nested (N ts Tape)) a = ListFrom (Nested ts) [a]
  take :: forall a.
RefList ('Relative :-: rs)
-> Nested (N ts Tape) a -> ListFrom (Nested (N ts Tape)) a
take (Ref a
r :-: Conic Ref rest
rs) (Nest Nested fs' (f a)
t) = forall r (t :: * -> *) a.
Take r t =>
RefList r -> t a -> ListFrom t a
take Conic Ref rest
rs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. Ref 'Relative -> Tape a -> [a]
tapeTake Ref a
r) forall a b. (a -> b) -> a -> b
$ Nested fs' (f a)
t

instance ( Take (Replicate (NestedCount ts) 'Relative) (Nested ts)
         , Length r <= NestedCount ts
         , ((NestedCount ts - Length r) + Length r) ~ NestedCount ts
         ) => Take r (Indexed ts) where
  type ListFrom (Indexed ts) a = ListFrom (Nested ts) a
  take :: forall a. RefList r -> Indexed ts a -> ListFrom (Indexed ts) a
take RefList r
r (Indexed Coordinate (NestedCount ts)
i Nested ts a
t) = forall r (t :: * -> *) a.
Take r t =>
RefList r -> t a -> ListFrom t a
take (forall {k} a (f :: k -> *) (t :: k) n.
(a -> f t) -> Counted n a -> Conic f (Replicate n t)
heterogenize forall a. a -> a
id (forall ts n.
(Length ts <= n, ((n - Length ts) + Length ts) ~ n) =>
RefList ts
-> Counted n (Ref 'Absolute) -> Counted n (Ref 'Relative)
getMovement RefList r
r Coordinate (NestedCount ts)
i)) Nested ts a
t

tapeView :: Ref 'Relative -> Tape a -> Stream a
tapeView :: forall a. Ref 'Relative -> Tape a -> Stream a
tapeView (Rel Int
r) Tape a
t | Int
r forall a. Ord a => a -> a -> Bool
>= Int
0    = forall a. Tape a -> a
focus Tape a
t forall t. t -> Stream t -> Stream t
<:> forall a. Tape a -> Stream a
viewR Tape a
t
tapeView (Rel Int
_) Tape a
t = forall a. Tape a -> a
focus Tape a
t forall t. t -> Stream t -> Stream t
<:> forall a. Tape a -> Stream a
viewL Tape a
t

class View r t where
  -- | Type of an n-dimensional stream extracted from an n-dimensional sheet.
  type StreamFrom t a
  view :: RefList r -> t a -> StreamFrom t a

instance View Nil (Nested (F Tape)) where
  type StreamFrom (Nested (F Tape)) a = Stream a
  view :: forall a.
RefList Nil -> Nested (F Tape) a -> StreamFrom (Nested (F Tape)) a
view RefList Nil
_ (Flat f a
t) = forall a. Ref 'Relative -> Tape a -> Stream a
tapeView (forall (t :: RefType). (t ~ 'Relative) => Int -> Ref t
Rel Int
0) f a
t

instance ( View Nil (Nested ts)
         , Functor (Nested ts)
         ) => View Nil (Nested (N ts Tape)) where
  type StreamFrom (Nested (N ts Tape)) a = StreamFrom (Nested ts) (Stream a)
  view :: forall a.
RefList Nil
-> Nested (N ts Tape) a -> StreamFrom (Nested (N ts Tape)) a
view RefList Nil
_ = forall r (t :: * -> *) a.
View r t =>
RefList r -> t a -> StreamFrom t a
view (forall (t :: RefType). (t ~ 'Relative) => Int -> Ref t
Rel Int
0 forall {k} (f :: k -> *) ts rest (a :: k).
(ts ~ (a :-: rest)) =>
f a -> Conic f rest -> Conic f ts
:-: forall {k} (f :: k -> *) ts. (ts ~ Nil) => Conic f ts
ConicNil)

instance View ('Relative :-: Nil) (Nested (F Tape)) where
  type StreamFrom (Nested (F Tape)) a = (Stream a)
  view :: forall a.
Conic Ref Rel1
-> Nested (F Tape) a -> StreamFrom (Nested (F Tape)) a
view (Ref a
r :-: Conic Ref rest
_) (Flat f a
t) = forall a. Ref 'Relative -> Tape a -> Stream a
tapeView Ref a
r f a
t

instance ( Functor (Nested ts)
         , View rs (Nested ts)
         ) => View ('Relative :-: rs) (Nested (N ts Tape)) where
  type StreamFrom (Nested (N ts Tape)) a = StreamFrom (Nested ts) (Stream a)
  view :: forall a.
RefList ('Relative :-: rs)
-> Nested (N ts Tape) a -> StreamFrom (Nested (N ts Tape)) a
view (Ref a
r :-: Conic Ref rest
rs) (Nest Nested fs' (f a)
t) = forall r (t :: * -> *) a.
View r t =>
RefList r -> t a -> StreamFrom t a
view Conic Ref rest
rs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. Ref 'Relative -> Tape a -> Stream a
tapeView Ref a
r) forall a b. (a -> b) -> a -> b
$ Nested fs' (f a)
t

instance ( View (Replicate (NestedCount ts) 'Relative) (Nested ts)
         , Length r <= NestedCount ts
         , (( NestedCount ts - Length r) + Length r) ~ NestedCount ts
         ) => View r (Indexed ts) where
  type StreamFrom (Indexed ts) a = StreamFrom (Nested ts) a
  view :: forall a. RefList r -> Indexed ts a -> StreamFrom (Indexed ts) a
view RefList r
r (Indexed Coordinate (NestedCount ts)
i Nested ts a
t) = forall r (t :: * -> *) a.
View r t =>
RefList r -> t a -> StreamFrom t a
view (forall {k} a (f :: k -> *) (t :: k) n.
(a -> f t) -> Counted n a -> Conic f (Replicate n t)
heterogenize forall a. a -> a
id (forall ts n.
(Length ts <= n, ((n - Length ts) + Length ts) ~ n) =>
RefList ts
-> Counted n (Ref 'Absolute) -> Counted n (Ref 'Relative)
getMovement RefList r
r Coordinate (NestedCount ts)
i)) Nested ts a
t

tapeGo :: Ref 'Relative -> Tape a -> Tape a
tapeGo :: forall a. Ref 'Relative -> Tape a -> Tape a
tapeGo ~(Rel !Int
r) = forall {c}. Int -> (c -> c) -> c -> c
fpow (forall a. Num a => a -> a
abs Int
r) (if Int
r forall a. Ord a => a -> a -> Bool
> Int
0 then forall a. Tape a -> Tape a
moveR else forall a. Tape a -> Tape a
moveL)
  where fpow :: Int -> (c -> c) -> c -> c
fpow Int
n = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) forall a. a -> a
id forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Int -> a -> [a]
P.replicate Int
n
        {-# INLINE fpow #-}

class Go r t where
  -- | Move to the location specified by the given @RefList@.
  go :: RefList r -> t a -> t a

instance Go ('Relative :-: Nil) (Nested (F Tape)) where
  go :: forall a. Conic Ref Rel1 -> Nested (F Tape) a -> Nested (F Tape) a
go (Ref a
r :-: Conic Ref rest
_) (Flat f a
t) = forall fs a (f :: * -> *). (fs ~ F f) => f a -> Nested fs a
Flat forall a b. (a -> b) -> a -> b
$ forall a. Ref 'Relative -> Tape a -> Tape a
tapeGo Ref a
r f a
t

instance Go Nil (Nested ts) where go :: forall a. RefList Nil -> Nested ts a -> Nested ts a
go RefList Nil
_ = forall a. a -> a
id

instance ( Go rs (Nested ts)
         , Functor (Nested ts)
         ) => Go ('Relative :-: rs) (Nested (N ts Tape)) where
  go :: forall a.
RefList ('Relative :-: rs)
-> Nested (N ts Tape) a -> Nested (N ts Tape) a
go (Ref a
r :-: Conic Ref rest
rs) (Nest Nested fs' (f a)
t) = forall fs a fs' (f :: * -> *).
(fs ~ N fs' f) =>
Nested fs' (f a) -> Nested fs a
Nest forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} r (t :: k -> *) (a :: k).
Go r t =>
RefList r -> t a -> t a
go Conic Ref rest
rs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. Ref 'Relative -> Tape a -> Tape a
tapeGo Ref a
r) forall a b. (a -> b) -> a -> b
$ Nested fs' (f a)
t

instance ( Go (Replicate (NestedCount ts) 'Relative) (Nested ts)
         , Length r <= NestedCount ts
         , ((NestedCount ts - Length r) + Length r) ~ NestedCount ts
         , ReifyNatural (NestedCount ts)
         ) => Go r (Indexed ts) where
  go :: forall a. RefList r -> Indexed ts a -> Indexed ts a
go RefList r
r (Indexed Coordinate (NestedCount ts)
i Nested ts a
t) =
    let move :: Counted (NestedCount ts) (Ref 'Relative)
move = forall ts n.
(Length ts <= n, ((n - Length ts) + Length ts) ~ n) =>
RefList ts
-> Counted n (Ref 'Absolute) -> Counted n (Ref 'Relative)
getMovement RefList r
r Coordinate (NestedCount ts)
i
    in  forall ts a.
Coordinate (NestedCount ts) -> Nested ts a -> Indexed ts a
Indexed (forall n.
ReifyNatural n =>
Counted n (Ref 'Relative)
-> Counted n (Ref 'Absolute) -> Counted n (Ref 'Absolute)
merge Counted (NestedCount ts) (Ref 'Relative)
move Coordinate (NestedCount ts)
i) (forall {k} r (t :: k -> *) (a :: k).
Go r t =>
RefList r -> t a -> t a
go (forall {k} a (f :: k -> *) (t :: k) n.
(a -> f t) -> Counted n a -> Conic f (Replicate n t)
heterogenize forall a. a -> a
id Counted (NestedCount ts) (Ref 'Relative)
move) Nested ts a
t)

-- | A 'Signed' @f@ is an 'f a' annotated with a sign: either 'Positive' or
-- 'Negative'. This is a useful type for specifying direction when inserting
-- into sheets. By wrapping a list or stream in 'Negative' and then inserting
-- it into a sheet, you insert it in the opposite direction of the usual one.
data Signed f a = Positive (f a) | Negative (f a)
  deriving (Signed f a -> Signed f a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (f :: k -> *) (a :: k).
Eq (f a) =>
Signed f a -> Signed f a -> Bool
/= :: Signed f a -> Signed f a -> Bool
$c/= :: forall k (f :: k -> *) (a :: k).
Eq (f a) =>
Signed f a -> Signed f a -> Bool
== :: Signed f a -> Signed f a -> Bool
$c== :: forall k (f :: k -> *) (a :: k).
Eq (f a) =>
Signed f a -> Signed f a -> Bool
Eq, Signed f a -> Signed f a -> Bool
Signed f a -> Signed f a -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {k} {f :: k -> *} {a :: k}. Ord (f a) => Eq (Signed f a)
forall k (f :: k -> *) (a :: k).
Ord (f a) =>
Signed f a -> Signed f a -> Bool
forall k (f :: k -> *) (a :: k).
Ord (f a) =>
Signed f a -> Signed f a -> Ordering
forall k (f :: k -> *) (a :: k).
Ord (f a) =>
Signed f a -> Signed f a -> Signed f a
min :: Signed f a -> Signed f a -> Signed f a
$cmin :: forall k (f :: k -> *) (a :: k).
Ord (f a) =>
Signed f a -> Signed f a -> Signed f a
max :: Signed f a -> Signed f a -> Signed f a
$cmax :: forall k (f :: k -> *) (a :: k).
Ord (f a) =>
Signed f a -> Signed f a -> Signed f a
>= :: Signed f a -> Signed f a -> Bool
$c>= :: forall k (f :: k -> *) (a :: k).
Ord (f a) =>
Signed f a -> Signed f a -> Bool
> :: Signed f a -> Signed f a -> Bool
$c> :: forall k (f :: k -> *) (a :: k).
Ord (f a) =>
Signed f a -> Signed f a -> Bool
<= :: Signed f a -> Signed f a -> Bool
$c<= :: forall k (f :: k -> *) (a :: k).
Ord (f a) =>
Signed f a -> Signed f a -> Bool
< :: Signed f a -> Signed f a -> Bool
$c< :: forall k (f :: k -> *) (a :: k).
Ord (f a) =>
Signed f a -> Signed f a -> Bool
compare :: Signed f a -> Signed f a -> Ordering
$ccompare :: forall k (f :: k -> *) (a :: k).
Ord (f a) =>
Signed f a -> Signed f a -> Ordering
Ord, Int -> Signed f a -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (f :: k -> *) (a :: k).
Show (f a) =>
Int -> Signed f a -> ShowS
forall k (f :: k -> *) (a :: k).
Show (f a) =>
[Signed f a] -> ShowS
forall k (f :: k -> *) (a :: k). Show (f a) => Signed f a -> String
showList :: [Signed f a] -> ShowS
$cshowList :: forall k (f :: k -> *) (a :: k).
Show (f a) =>
[Signed f a] -> ShowS
show :: Signed f a -> String
$cshow :: forall k (f :: k -> *) (a :: k). Show (f a) => Signed f a -> String
showsPrec :: Int -> Signed f a -> ShowS
$cshowsPrec :: forall k (f :: k -> *) (a :: k).
Show (f a) =>
Int -> Signed f a -> ShowS
Show)

class InsertBase l where
  insertBase :: l a -> Tape a -> Tape a

instance InsertBase Tape where
  insertBase :: forall a. Tape a -> Tape a -> Tape a
insertBase Tape a
t Tape a
_ = Tape a
t

instance InsertBase Stream where
  insertBase :: forall a. Stream a -> Tape a -> Tape a
insertBase (Cons a
x Stream a
xs) (Tape Stream a
ls a
_ Stream a
_) = forall a. Stream a -> a -> Stream a -> Tape a
Tape Stream a
ls a
x Stream a
xs

instance InsertBase (Signed Stream) where
  insertBase :: forall a. Signed Stream a -> Tape a -> Tape a
insertBase (Positive (Cons a
x Stream a
xs)) (Tape Stream a
ls a
_ Stream a
_) = forall a. Stream a -> a -> Stream a -> Tape a
Tape Stream a
ls a
x Stream a
xs
  insertBase (Negative (Cons a
x Stream a
xs)) (Tape Stream a
_ a
_ Stream a
rs) = forall a. Stream a -> a -> Stream a -> Tape a
Tape Stream a
xs a
x Stream a
rs

instance InsertBase [] where
  insertBase :: forall a. [a] -> Tape a -> Tape a
insertBase [] Tape a
t = Tape a
t
  insertBase (a
x : [a]
xs) (Tape Stream a
ls a
c Stream a
rs) =
    forall a. Stream a -> a -> Stream a -> Tape a
Tape Stream a
ls a
x (forall value. [value] -> Stream value -> Stream value
prefixStream [a]
xs (forall t. t -> Stream t -> Stream t
Cons a
c Stream a
rs))

instance InsertBase (Signed []) where
  insertBase :: forall a. Signed [] a -> Tape a -> Tape a
insertBase (Positive []) Tape a
t = Tape a
t
  insertBase (Negative []) Tape a
t = Tape a
t
  insertBase (Positive (a
x : [a]
xs)) (Tape Stream a
ls a
c Stream a
rs) =
    forall a. Stream a -> a -> Stream a -> Tape a
Tape Stream a
ls a
x (forall value. [value] -> Stream value -> Stream value
prefixStream [a]
xs (forall t. t -> Stream t -> Stream t
Cons a
c Stream a
rs))
  insertBase (Negative (a
x : [a]
xs)) (Tape Stream a
ls a
c Stream a
rs) =
    forall a. Stream a -> a -> Stream a -> Tape a
Tape (forall value. [value] -> Stream value -> Stream value
prefixStream [a]
xs (forall t. t -> Stream t -> Stream t
Cons a
c Stream a
ls)) a
x Stream a
rs

class InsertNested l t where
  insertNested :: l a -> t a -> t a

instance (InsertBase l) => InsertNested (Nested (F l)) (Nested (F Tape)) where
  insertNested :: forall a. Nested (F l) a -> Nested (F Tape) a -> Nested (F Tape) a
insertNested (Flat f a
l) (Flat f a
t) = forall fs a (f :: * -> *). (fs ~ F f) => f a -> Nested fs a
Flat forall a b. (a -> b) -> a -> b
$ forall (l :: * -> *) a. InsertBase l => l a -> Tape a -> Tape a
insertBase f a
l f a
t

instance ( InsertBase l
         , InsertNested (Nested ls) (Nested ts)
         , Functor (Nested ls)
         , Applicative (Nested ts) )
  => InsertNested (Nested (N ls l)) (Nested (N ts Tape)) where
  insertNested :: forall a.
Nested (N ls l) a -> Nested (N ts Tape) a -> Nested (N ts Tape) a
insertNested (Nest Nested fs' (f a)
l) (Nest Nested fs' (f a)
t) =
    forall fs a fs' (f :: * -> *).
(fs ~ N fs' f) =>
Nested fs' (f a) -> Nested fs a
Nest forall a b. (a -> b) -> a -> b
$ forall {k} (l :: k -> *) (t :: k -> *) (a :: k).
InsertNested l t =>
l a -> t a -> t a
insertNested (forall (l :: * -> *) a. InsertBase l => l a -> Tape a -> Tape a
insertBase forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Nested fs' (f a)
l) (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. a -> a
id) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Nested fs' (f a)
t

instance ( InsertNested l (Nested ts)) => InsertNested l (Indexed ts) where
  insertNested :: forall a. l a -> Indexed ts a -> Indexed ts a
insertNested l a
l (Indexed Coordinate (NestedCount ts)
i Nested ts a
t) = forall ts a.
Coordinate (NestedCount ts) -> Nested ts a -> Indexed ts a
Indexed Coordinate (NestedCount ts)
i (forall {k} (l :: k -> *) (t :: k -> *) (a :: k).
InsertNested l t =>
l a -> t a -> t a
insertNested l a
l Nested ts a
t)

type family AddNest x where
  AddNest (Nested fs (f x)) = Nested (N fs f) x

type family AsNestedAs x y where
  (f x) `AsNestedAs` (Nested (F g) b) = Nested (F f) x
  x `AsNestedAs` y = AddNest (x `AsNestedAs` UnNest y)

class NestedAs x y where
  asNestedAs :: x -> y -> x `AsNestedAs` y

instance ( AsNestedAs (f a) (Nested (F g) b) ~ Nested (F f) a)
  => NestedAs (f a) (Nested (F g) b) where
  f a
x asNestedAs :: f a -> Nested (F g) b -> AsNestedAs (f a) (Nested (F g) b)
`asNestedAs` Nested (F g) b
_ = forall fs a (f :: * -> *). (fs ~ F f) => f a -> Nested fs a
Flat f a
x

instance ( AsNestedAs (f a) (UnNest (Nested (N g h) b)) ~ Nested fs (f' a')
         , AddNest (Nested fs (f' a')) ~ Nested (N fs f') a'
         , NestedAs (f a) (UnNest (Nested (N g h) b)) )
  => NestedAs (f a) (Nested (N g h) b) where
  f a
x asNestedAs :: f a -> Nested (N g h) b -> AsNestedAs (f a) (Nested (N g h) b)
`asNestedAs` Nested (N g h) b
y = forall fs a fs' (f :: * -> *).
(fs ~ N fs' f) =>
Nested fs' (f a) -> Nested fs a
Nest (f a
x forall x y. NestedAs x y => x -> y -> AsNestedAs x y
`asNestedAs` forall fs a. Nested fs a -> UnNest (Nested fs a)
unNest Nested (N g h) b
y)

-- | 'DimensionalAs' provides a mechanism to "lift" an n-deep nested structure
-- into an explicit 'Nested' type. This is the way in which raw
-- lists-of-lists-of-lists-, etc. can be inserted (without manual annotation of
-- nesting depth) into a sheet.
class DimensionalAs (x :: Type) (y :: Type) where
  type AsDimensionalAs x y
  asDimensionalAs :: x -> y -> x `AsDimensionalAs` y

-- ! These instances break everything:
instance ( NestedAs x (Nested ts y)
         , AsDimensionalAs x (Nested ts y) ~ AsNestedAs x (Nested ts y)
         ) => DimensionalAs x (Nested ts y) where
  type x `AsDimensionalAs` (Nested ts y) = x `AsNestedAs` Nested ts y
  asDimensionalAs :: x -> Nested ts y -> AsDimensionalAs x (Nested ts y)
asDimensionalAs = forall x y. NestedAs x y => x -> y -> AsNestedAs x y
asNestedAs

instance (NestedAs x (Nested ts y)) => DimensionalAs x (Indexed ts y) where
  type x `AsDimensionalAs` (Indexed ts y) = x `AsNestedAs` Nested ts y
  x
x asDimensionalAs :: x -> Indexed ts y -> AsDimensionalAs x (Indexed ts y)
`asDimensionalAs` (Indexed Coordinate (NestedCount ts)
_ Nested ts y
t) = x
x forall x y. NestedAs x y => x -> y -> AsNestedAs x y
`asNestedAs` Nested ts y
t

-- | Combination of 'go' and 'take': moves to the location specified by the
-- first argument, then takes the amount specified by the second argument.
slice :: (Take r' t, Go r t) => RefList r -> RefList r' -> t a -> ListFrom t a
slice :: forall r' (t :: * -> *) r a.
(Take r' t, Go r t) =>
RefList r -> RefList r' -> t a -> ListFrom t a
slice RefList r
r RefList r'
r' = forall r (t :: * -> *) a.
Take r t =>
RefList r -> t a -> ListFrom t a
take RefList r'
r' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} r (t :: k -> *) (a :: k).
Go r t =>
RefList r -> t a -> t a
go RefList r
r

-- | Insert a (possibly nested) list-like structure into a (possibly
-- many-dimensional) sheet.
-- The depth of the nesting structure being inserted must match the number of
-- dimensions of the sheet into which it is being inserted.
-- The structure being inserted need not be a 'Nested' type: it need only have
-- enough levels of structure (ie, number of nested lists) to match the
-- dimensionality of the sheet.
insert
  :: ( DimensionalAs x (t a)
     , InsertNested l t
     , AsDimensionalAs x (t a) ~ l a )
  => x
  -> t a
  -> t a
insert :: forall {k} x (t :: k -> *) (a :: k) (l :: k -> *).
(DimensionalAs x (t a), InsertNested l t,
 AsDimensionalAs x (t a) ~ l a) =>
x -> t a -> t a
insert x
l t a
t = forall {k} (l :: k -> *) (t :: k -> *) (a :: k).
InsertNested l t =>
l a -> t a -> t a
insertNested (x
l forall x y. DimensionalAs x y => x -> y -> AsDimensionalAs x y
`asDimensionalAs` t a
t) t a
t

-- = Sheets

-- == 1-D Sheets
type Abs1 = 'Absolute :-: Nil
type Rel1 = 'Relative :-: Nil
type Nat1 = S Z

nat1 :: Natural Nat1
nat1 :: Natural Nat1
nat1 = forall n. ReifyNatural n => Natural n
reifyNatural

type Sheet1 = Nested (NestedNTimes Nat1 Tape)
type ISheet1 = Indexed (NestedNTimes Nat1 Tape)

here1 :: RefList Rel1
here1 :: Conic Ref Rel1
here1 = forall (t :: RefType). (t ~ 'Relative) => Int -> Ref t
Rel Int
0 forall {k} (f :: k -> *) ts rest (a :: k).
(ts ~ (a :-: rest)) =>
f a -> Conic f rest -> Conic f ts
:-: forall {k} (f :: k -> *) ts. (ts ~ Nil) => Conic f ts
ConicNil

d1 :: (CombineRefLists Rel1 x) => RefList x -> RefList (Rel1 & x)
d1 :: forall x. CombineRefLists Rel1 x => RefList x -> RefList (Rel1 & x)
d1 = (Conic Ref Rel1
here1 forall as bs.
CombineRefLists as bs =>
RefList as -> RefList bs -> RefList (as & bs)
&)

columnAt :: Int -> RefList ('Absolute :-: Nil)
columnAt :: Int -> RefList ('Absolute :-: Nil)
columnAt = forall (t :: RefType) n.
Tackable t (Replicate n 'Relative) =>
Natural (S n) -> Ref t -> RefList (Tack t (Replicate n 'Relative))
dimensional Natural Nat1
nat1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: RefType). (t ~ 'Absolute) => Int -> Ref t
Abs

column :: (Z < NestedCount ts) => Indexed ts x -> Int
column :: forall ts x. (Z < NestedCount ts) => Indexed ts x -> Int
column = forall (t :: RefType). Ref t -> Int
getRef forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n m a. (n < m) => Natural n -> Counted m a -> a
nth forall n. (n ~ Z) => Natural n
Zero forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ts a. Indexed ts a -> Coordinate (NestedCount ts)
origin

rightBy, leftBy :: Int -> RefList Rel1
rightBy :: Int -> Conic Ref Rel1
rightBy = forall (t :: RefType) n.
Tackable t (Replicate n 'Relative) =>
Natural (S n) -> Ref t -> RefList (Tack t (Replicate n 'Relative))
dimensional Natural Nat1
nat1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: RefType). (t ~ 'Relative) => Int -> Ref t
Rel
leftBy :: Int -> Conic Ref Rel1
leftBy = Int -> Conic Ref Rel1
rightBy forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Num a => a -> a
negate

right, left :: RefList Rel1
right :: Conic Ref Rel1
right = Int -> Conic Ref Rel1
rightBy Int
1
left :: Conic Ref Rel1
left = Int -> Conic Ref Rel1
leftBy Int
1

-- == 2-D Sheets
type Abs2 = 'Absolute :-: Abs1
type Rel2 = 'Relative :-: Rel1
type Nat2 = S Nat1

nat2 :: Natural Nat2
nat2 :: Natural Nat2
nat2 = forall n. ReifyNatural n => Natural n
reifyNatural

type Sheet2 = Nested (NestedNTimes Nat2 Tape)
type ISheet2 = Indexed (NestedNTimes Nat2 Tape)

here2 :: RefList Rel2
here2 :: RefList Rel2
here2 = forall (t :: RefType). (t ~ 'Relative) => Int -> Ref t
Rel Int
0 forall {k} (f :: k -> *) ts rest (a :: k).
(ts ~ (a :-: rest)) =>
f a -> Conic f rest -> Conic f ts
:-: Conic Ref Rel1
here1

d2 :: (CombineRefLists Rel2 x) => RefList x -> RefList (Rel2 & x)
d2 :: forall x. CombineRefLists Rel2 x => RefList x -> RefList (Rel2 & x)
d2 = (RefList Rel2
here2 forall as bs.
CombineRefLists as bs =>
RefList as -> RefList bs -> RefList (as & bs)
&)

rowAt :: Int -> RefList (Tack 'Absolute Rel1)
rowAt :: Int -> RefList (Tack 'Absolute Rel1)
rowAt = forall (t :: RefType) n.
Tackable t (Replicate n 'Relative) =>
Natural (S n) -> Ref t -> RefList (Tack t (Replicate n 'Relative))
dimensional Natural Nat2
nat2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: RefType). (t ~ 'Absolute) => Int -> Ref t
Abs

row :: (Nat1 < NestedCount ts) => Indexed ts x -> Int
row :: forall ts x. (Nat1 < NestedCount ts) => Indexed ts x -> Int
row = forall (t :: RefType). Ref t -> Int
getRef forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n m a. (n < m) => Natural n -> Counted m a -> a
nth Natural Nat1
nat1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ts a. Indexed ts a -> Coordinate (NestedCount ts)
origin

belowBy, aboveBy :: Int -> RefList Rel2
belowBy :: Int -> RefList Rel2
belowBy = forall (t :: RefType) n.
Tackable t (Replicate n 'Relative) =>
Natural (S n) -> Ref t -> RefList (Tack t (Replicate n 'Relative))
dimensional Natural Nat2
nat2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: RefType). (t ~ 'Relative) => Int -> Ref t
Rel
aboveBy :: Int -> RefList Rel2
aboveBy = Int -> RefList Rel2
belowBy forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Num a => a -> a
negate

below, above :: RefList Rel2
below :: RefList Rel2
below = Int -> RefList Rel2
belowBy Int
1
above :: RefList Rel2
above = Int -> RefList Rel2
aboveBy Int
1

-- == 3-D Sheets
type Abs3 = 'Absolute :-: Abs2
type Rel3 = 'Relative :-: Rel2
type Nat3 = S Nat2

nat3 :: Natural Nat3
nat3 :: Natural Nat3
nat3 = forall n. ReifyNatural n => Natural n
reifyNatural

type Sheet3 = Nested (NestedNTimes Nat3 Tape)
type ISheet3 = Indexed (NestedNTimes Nat3 Tape)

here3 :: RefList Rel3
here3 :: RefList Rel3
here3 = forall (t :: RefType). (t ~ 'Relative) => Int -> Ref t
Rel Int
0 forall {k} (f :: k -> *) ts rest (a :: k).
(ts ~ (a :-: rest)) =>
f a -> Conic f rest -> Conic f ts
:-: RefList Rel2
here2

d3 :: (CombineRefLists Rel3 x) => RefList x -> RefList (Rel3 & x)
d3 :: forall x. CombineRefLists Rel3 x => RefList x -> RefList (Rel3 & x)
d3 = (RefList Rel3
here3 forall as bs.
CombineRefLists as bs =>
RefList as -> RefList bs -> RefList (as & bs)
&)

levelAt :: Int -> RefList (Tack 'Absolute Rel2)
levelAt :: Int -> RefList (Tack 'Absolute Rel2)
levelAt = forall (t :: RefType) n.
Tackable t (Replicate n 'Relative) =>
Natural (S n) -> Ref t -> RefList (Tack t (Replicate n 'Relative))
dimensional Natural Nat3
nat3 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: RefType). (t ~ 'Absolute) => Int -> Ref t
Abs

level :: (Nat2 < NestedCount ts) => Indexed ts x -> Int
level :: forall ts x. (Nat2 < NestedCount ts) => Indexed ts x -> Int
level = forall (t :: RefType). Ref t -> Int
getRef forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n m a. (n < m) => Natural n -> Counted m a -> a
nth Natural Nat2
nat2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ts a. Indexed ts a -> Coordinate (NestedCount ts)
origin

outwardBy, inwardBy :: Int -> RefList Rel3
outwardBy :: Int -> RefList Rel3
outwardBy = forall (t :: RefType) n.
Tackable t (Replicate n 'Relative) =>
Natural (S n) -> Ref t -> RefList (Tack t (Replicate n 'Relative))
dimensional Natural Nat3
nat3 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: RefType). (t ~ 'Relative) => Int -> Ref t
Rel
inwardBy :: Int -> RefList Rel3
inwardBy = Int -> RefList Rel3
outwardBy forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Num a => a -> a
negate

outward, inward :: RefList Rel3
outward :: RefList Rel3
outward = Int -> RefList Rel3
outwardBy Int
1
inward :: RefList Rel3
inward = Int -> RefList Rel3
inwardBy Int
1

-- == 4-D Sheets
type Abs4 = 'Absolute :-: Abs3
type Rel4 = 'Relative :-: Rel3
type Nat4 = S Nat3

nat4 :: Natural Nat4
nat4 :: Natural Nat4
nat4 = forall n. ReifyNatural n => Natural n
reifyNatural

type Sheet4 = Nested (NestedNTimes Nat4 Tape)
type ISheet4 = Indexed (NestedNTimes Nat4 Tape)

here4 :: RefList Rel4
here4 :: RefList Rel4
here4 = forall (t :: RefType). (t ~ 'Relative) => Int -> Ref t
Rel Int
0 forall {k} (f :: k -> *) ts rest (a :: k).
(ts ~ (a :-: rest)) =>
f a -> Conic f rest -> Conic f ts
:-: RefList Rel3
here3

d4 :: (CombineRefLists Rel4 x) => RefList x -> RefList (Rel4 & x)
d4 :: forall x. CombineRefLists Rel4 x => RefList x -> RefList (Rel4 & x)
d4 = (RefList Rel4
here4 forall as bs.
CombineRefLists as bs =>
RefList as -> RefList bs -> RefList (as & bs)
&)

spaceAt :: Int -> RefList (Tack 'Absolute Rel3)
spaceAt :: Int -> RefList (Tack 'Absolute Rel3)
spaceAt = forall (t :: RefType) n.
Tackable t (Replicate n 'Relative) =>
Natural (S n) -> Ref t -> RefList (Tack t (Replicate n 'Relative))
dimensional Natural Nat4
nat4 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: RefType). (t ~ 'Absolute) => Int -> Ref t
Abs

space :: (Nat3 < NestedCount ts) => Indexed ts x -> Int
space :: forall ts x. (Nat3 < NestedCount ts) => Indexed ts x -> Int
space = forall (t :: RefType). Ref t -> Int
getRef forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n m a. (n < m) => Natural n -> Counted m a -> a
nth Natural Nat3
nat3 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ts a. Indexed ts a -> Coordinate (NestedCount ts)
origin

anaBy, cataBy :: Int -> RefList Rel4
anaBy :: Int -> RefList Rel4
anaBy = forall (t :: RefType) n.
Tackable t (Replicate n 'Relative) =>
Natural (S n) -> Ref t -> RefList (Tack t (Replicate n 'Relative))
dimensional Natural Nat4
nat4 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: RefType). (t ~ 'Relative) => Int -> Ref t
Rel
cataBy :: Int -> RefList Rel4
cataBy = Int -> RefList Rel4
anaBy forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Num a => a -> a
negate

ana, cata :: RefList Rel4
ana :: RefList Rel4
ana = Int -> RefList Rel4
anaBy Int
1
cata :: RefList Rel4
cata = Int -> RefList Rel4
cataBy Int
1

-- = Magic

fix :: (t -> t) -> t
fix :: forall t. (t -> t) -> t
fix t -> t
f = let x :: t
x = t -> t
f t
x in t
x

evaluate :: (ComonadApply w) => w (w a -> a) -> w a
evaluate :: forall (w :: * -> *) a. ComonadApply w => w (w a -> a) -> w a
evaluate w (w a -> a)
fs = forall t. (t -> t) -> t
fix forall a b. (a -> b) -> a -> b
$ (w (w a -> a)
fs forall (w :: * -> *) a b.
ComonadApply w =>
w (a -> b) -> w a -> w b
<@>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (w :: * -> *) a. Comonad w => w a -> w (w a)
duplicate

evaluateF :: (ComonadApply w, Functor f) => w (f (w (f a) -> a)) -> w (f a)
evaluateF :: forall (w :: * -> *) (f :: * -> *) a.
(ComonadApply w, Functor f) =>
w (f (w (f a) -> a)) -> w (f a)
evaluateF w (f (w (f a) -> a))
fs = forall t. (t -> t) -> t
fix forall a b. (a -> b) -> a -> b
$ (forall (w :: * -> *) a b.
ComonadApply w =>
w (a -> b) -> w a -> w b
<@> w (f (w (f a) -> a))
fs) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. (a -> b) -> a -> b
($)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (w :: * -> *) a. Comonad w => w a -> w (w a)
duplicate

cell :: (Comonad w, Go r w) => RefList r -> w a -> a
cell :: forall (w :: * -> *) r a.
(Comonad w, Go r w) =>
RefList r -> w a -> a
cell = (forall (w :: * -> *) a. Comonad w => w a -> a
extract forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} r (t :: k -> *) (a :: k).
Go r t =>
RefList r -> t a -> t a
go

cells :: (Traversable t, Comonad w, Go r w) => t (RefList r) -> w a -> t a
cells :: forall (t :: * -> *) (w :: * -> *) r a.
(Traversable t, Comonad w, Go r w) =>
t (RefList r) -> w a -> t a
cells = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall (w :: * -> *) r a.
(Comonad w, Go r w) =>
RefList r -> w a -> a
cell

-- | Construct a sheet of values from a default value and an insertable
-- container of values.
sheet
  :: ( InsertNested l t
     , Applicative t
     , DimensionalAs x (t a)
     , AsDimensionalAs x (t a) ~ l a)
  => a
  -> x
  -> t a
sheet :: forall (l :: * -> *) (t :: * -> *) x a.
(InsertNested l t, Applicative t, DimensionalAs x (t a),
 AsDimensionalAs x (t a) ~ l a) =>
a -> x -> t a
sheet a
background x
list = forall {k} x (t :: k -> *) (a :: k) (l :: k -> *).
(DimensionalAs x (t a), InsertNested l t,
 AsDimensionalAs x (t a) ~ l a) =>
x -> t a -> t a
insert x
list (forall (f :: * -> *) a. Applicative f => a -> f a
pure a
background)

change
  :: ( InsertNested l w
     , ComonadApply w
     , DimensionalAs x (w (w a -> a))
     , AsDimensionalAs x (w (w a -> a)) ~ l (w a -> a))
  => x
  -> w a
  -> w a
change :: forall (l :: * -> *) (w :: * -> *) x a.
(InsertNested l w, ComonadApply w, DimensionalAs x (w (w a -> a)),
 AsDimensionalAs x (w (w a -> a)) ~ l (w a -> a)) =>
x -> w a -> w a
change x
new w a
old = forall (w :: * -> *) a. ComonadApply w => w (w a -> a) -> w a
evaluate forall a b. (a -> b) -> a -> b
$ forall {k} x (t :: k -> *) (a :: k) (l :: k -> *).
(DimensionalAs x (t a), InsertNested l t,
 AsDimensionalAs x (t a) ~ l a) =>
x -> t a -> t a
insert x
new (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. a -> b -> a
const w a
old)

sheetFromNested
  :: ( InsertNested (Nested fs) (Nested (NestedNTimes (NestedCount fs) Tape))
     , Applicative (Nested (NestedNTimes (NestedCount fs) Tape)))
  => a
  -> Nested fs a
  -> Nested (NestedNTimes (NestedCount fs) Tape) a
sheetFromNested :: forall fs a.
(InsertNested
   (Nested fs) (Nested (NestedNTimes (NestedCount fs) Tape)),
 Applicative (Nested (NestedNTimes (NestedCount fs) Tape))) =>
a -> Nested fs a -> Nested (NestedNTimes (NestedCount fs) Tape) a
sheetFromNested a
background Nested fs a
list = forall {k} (l :: k -> *) (t :: k -> *) (a :: k).
InsertNested l t =>
l a -> t a -> t a
insertNested Nested fs a
list (forall (f :: * -> *) a. Applicative f => a -> f a
pure a
background)

-- | Construct an indexed sheet from an origin index, a default value, and an
-- insertable container of values.
indexedSheet
  :: ( InsertNested l (Nested ts)
     , Applicative (Nested ts)
     , DimensionalAs x (Nested ts a)
     , AsDimensionalAs x (Nested ts a) ~ l a)
  => Coordinate (NestedCount ts)
  -> a
  -> x
  -> Indexed ts a
indexedSheet :: forall (l :: * -> *) ts x a.
(InsertNested l (Nested ts), Applicative (Nested ts),
 DimensionalAs x (Nested ts a),
 AsDimensionalAs x (Nested ts a) ~ l a) =>
Coordinate (NestedCount ts) -> a -> x -> Indexed ts a
indexedSheet Coordinate (NestedCount ts)
i = (forall ts a.
Coordinate (NestedCount ts) -> Nested ts a -> Indexed ts a
Indexed Coordinate (NestedCount ts)
i forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (l :: * -> *) (t :: * -> *) x a.
(InsertNested l t, Applicative t, DimensionalAs x (t a),
 AsDimensionalAs x (t a) ~ l a) =>
a -> x -> t a
sheet

instance
  ( ComonadApply (Nested ts)
  , ReifyNatural (NestedCount ts)
  , Cross (NestedCount ts) Tape
  , ts ~ NestedNTimes (NestedCount ts) Tape
  , Go (Replicate (NestedCount ts) 'Relative) (Nested ts)
  ) => Representable (Indexed ts) where
  type Rep (Indexed ts) = Counted (NestedCount ts) Int
  index :: forall a. Indexed ts a -> Rep (Indexed ts) -> a
index (Indexed Coordinate (NestedCount ts)
ogn Nested ts a
sh) Rep (Indexed ts)
crd = forall (w :: * -> *) r a.
(Comonad w, Go r w) =>
RefList r -> w a -> a
cell Conic Ref (Replicate (NestedCount ts) 'Relative)
crd' Nested ts a
sh where
    crd' :: Conic Ref (Replicate (NestedCount ts) 'Relative)
crd' = forall {k} a (f :: k -> *) (t :: k) n.
(a -> f t) -> Counted n a -> Conic f (Replicate n t)
heterogenize forall a. a -> a
id (forall n.
Counted n (Either (Ref 'Relative) (Ref 'Absolute))
-> Counted n (Ref 'Absolute) -> Counted n (Ref 'Relative)
diff (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (t :: RefType).
Ref t -> Either (Ref 'Relative) (Ref 'Absolute)
eitherFromRef forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: RefType). (t ~ 'Absolute) => Int -> Ref t
Abs) Rep (Indexed ts)
crd) Coordinate (NestedCount ts)
ogn)
    {-# INLINE crd' #-}
  tabulate :: forall a. (Rep (Indexed ts) -> a) -> Indexed ts a
tabulate Rep (Indexed ts) -> a
describe = forall ts a.
Coordinate (NestedCount ts) -> Nested ts a -> Indexed ts a
Indexed Coordinate (NestedCount ts)
ogn forall a b. (a -> b) -> a -> b
$ Rep (Indexed ts) -> a
describe forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Coordinate (NestedCount ts)
-> Nested
     (NestedNTimes (NestedCount ts) Tape) (Counted (NestedCount ts) Int)
indices' Coordinate (NestedCount ts)
ogn where
    ogn :: Coordinate (NestedCount ts)
ogn = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (t :: RefType). (t ~ 'Absolute) => Int -> Ref t
Abs Int
0)
    indices' :: Coordinate (NestedCount ts)
-> Nested
     (NestedNTimes (NestedCount ts) Tape) (Counted (NestedCount ts) Int)
indices' = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (t :: RefType). Ref t -> Int
getRef)) forall n.
Cross n Tape =>
Coordinate n -> Nested (NestedNTimes n Tape) (Coordinate n)
indices
    {-# INLINE indices' #-}

instance
  ( ComonadApply (Nested ts)
  , ReifyNatural (NestedCount ts)
  , Cross (NestedCount ts) Tape
  , ts ~ NestedNTimes (NestedCount ts) Tape
  , Go (Replicate (NestedCount ts) 'Relative) (Nested ts)
  ) => Distributive (Indexed ts) where
  distribute :: forall (f :: * -> *) a.
Functor f =>
f (Indexed ts a) -> Indexed ts (f a)
distribute = forall (f :: * -> *) (w :: * -> *) a.
(Representable f, Functor w) =>
w (f a) -> f (w a)
distributeRep
  {-# INLINE distribute #-}