module Data.Ix.Static
( IxStatic(..)
, fromNat
, (:.)
, Nil
, D2
, D3
, D4
, D5
) where
import GHC.TypeLits
import Data.Ix
import Data.Proxy
import Data.Tagged
fromNat :: forall (proxy :: Nat -> *) (n :: Nat). SingI n => proxy n -> Int
fromNat _ = fromInteger $ fromSing (sing :: Sing n)
class Ix (Index d) => IxStatic d where
type Index d :: *
taggedBounds :: Tagged d (Index d, Index d)
instance SingI a => IxStatic (a :: Nat) where
type Index a = Int
taggedBounds = Tagged (0, fromNat (Proxy :: Proxy a) 1)
instance SingI n => IxStatic ('[n] :: [Nat]) where
type Index ('[n]) = Int
taggedBounds = Tagged (0, fromNat (Proxy :: Proxy n) 1)
instance (SingI n, IxStatic (n2 ': ns)) =>
IxStatic ((n ': n2 ': ns) :: [Nat]) where
type Index (n ': n2 ': ns) = (Int, Index (n2 ': ns))
taggedBounds = Tagged ((0, b0), (fromNat (Proxy :: Proxy n) 1, bn))
where
(b0, bn) = proxy taggedBounds (Proxy :: Proxy (n2 ': ns))
instance (SingI a, SingI b) => IxStatic ('(a, b) :: (Nat, Nat)) where
type Index '(a, b) = (Int, Int)
taggedBounds = Tagged ((0, 0),
(fromNat (Proxy :: Proxy a) 1,
fromNat (Proxy :: Proxy b) 1))
instance (SingI a, SingI b, SingI c) =>
IxStatic ('(a, b, c) :: (Nat, Nat, Nat)) where
type Index '(a, b, c) = (Int, Int, Int)
taggedBounds = Tagged ((0, 0, 0),
(fromNat (Proxy :: Proxy a) 1,
fromNat (Proxy :: Proxy b) 1,
fromNat (Proxy :: Proxy c) 1))
instance (SingI a, SingI b, SingI c, SingI d) =>
IxStatic ('(a, b, c, d) :: (Nat, Nat, Nat, Nat)) where
type Index '(a, b, c, d) = (Int, Int, Int, Int)
taggedBounds = Tagged ((0, 0, 0, 0),
(fromNat (Proxy :: Proxy a) 1,
fromNat (Proxy :: Proxy b) 1,
fromNat (Proxy :: Proxy c) 1,
fromNat (Proxy :: Proxy d) 1))
instance (SingI a, SingI b, SingI c, SingI d, SingI e) =>
IxStatic ('(a, b, c, d, e) :: (Nat, Nat, Nat, Nat, Nat)) where
type Index '(a, b, c, d, e) = (Int, Int, Int, Int, Int)
taggedBounds = Tagged ((0, 0, 0, 0, 0),
(fromNat (Proxy :: Proxy a) 1,
fromNat (Proxy :: Proxy b) 1,
fromNat (Proxy :: Proxy c) 1,
fromNat (Proxy :: Proxy d) 1,
fromNat (Proxy :: Proxy e) 1))
data a :. b
infixr 3 :.
data Nil
instance SingI n => IxStatic ((n :: Nat) :. Nil) where
type Index (n :. Nil) = Int
taggedBounds = Tagged (0, fromNat (Proxy :: Proxy n) 1)
instance (SingI n, IxStatic (n2 :. ns)) =>
IxStatic ((n :: Nat) :. n2 :. ns) where
type Index (n :. n2 :. ns) = (Int, Index (n2 :. ns))
taggedBounds = Tagged ((0, b0), (fromNat (Proxy :: Proxy n) 1, bn))
where
(b0, bn) = proxy taggedBounds (Proxy :: Proxy (n2 :. ns))
data D2 (a :: Nat) (b :: Nat)
instance (SingI a, SingI b) => IxStatic (D2 a b) where
type Index (D2 a b) = (Int, Int)
taggedBounds = Tagged ((0, 0),
(fromNat (Proxy :: Proxy a) 1,
fromNat (Proxy :: Proxy b) 1))
data D3 (a :: Nat) (b :: Nat) (c :: Nat)
instance (SingI a, SingI b, SingI c) => IxStatic (D3 a b c) where
type Index (D3 a b c) = (Int, Int, Int)
taggedBounds = Tagged ((0, 0, 0),
(fromNat (Proxy :: Proxy a) 1,
fromNat (Proxy :: Proxy b) 1,
fromNat (Proxy :: Proxy c) 1))
data D4 (a :: Nat) (b :: Nat) (c :: Nat) (d :: Nat)
instance (SingI a, SingI b, SingI c, SingI d) => IxStatic (D4 a b c d) where
type Index (D4 a b c d) = (Int, Int, Int, Int)
taggedBounds = Tagged ((0, 0, 0, 0),
(fromNat (Proxy :: Proxy a) 1,
fromNat (Proxy :: Proxy b) 1,
fromNat (Proxy :: Proxy c) 1,
fromNat (Proxy :: Proxy d) 1))
data D5 (a :: Nat) (b :: Nat) (c :: Nat) (d :: Nat) (e :: Nat)
instance (SingI a, SingI b, SingI c, SingI d, SingI e) =>
IxStatic (D5 a b c d e) where
type Index (D5 a b c d e) = (Int, Int, Int, Int, Int)
taggedBounds = Tagged ((0, 0, 0, 0, 0),
(fromNat (Proxy :: Proxy a) 1,
fromNat (Proxy :: Proxy b) 1,
fromNat (Proxy :: Proxy c) 1,
fromNat (Proxy :: Proxy d) 1,
fromNat (Proxy :: Proxy e) 1))