{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module SizedGrid.Coord.Class where
import SizedGrid.Ordinal
import Control.Lens
import Data.Maybe (fromJust)
import Data.Proxy
import GHC.TypeLits
class IsCoord (c :: Nat -> *) where
asOrdinal :: Iso' (c n) (Ordinal n)
zeroPosition :: (1 <= n, KnownNat n) => c n
default zeroPosition :: Monoid (c n) => c n
zeroPosition = mempty
sCoordSized :: Proxy (c n) -> Proxy n
sCoordSized _ = Proxy
maxCoordSize :: KnownNat n => Proxy (c n) -> Integer
maxCoordSize p = natVal (sCoordSized p) - 1
maxCoord :: KnownNat n => Proxy n -> c n
maxCoord _ = view (re asOrdinal) (maxCoord (Proxy :: Proxy n))
asSizeProxy ::
c n
-> (forall m. (KnownNat m, m + 1 <= n) =>
Proxy m -> x)
-> x
asSizeProxy c = asSizeProxy (view asOrdinal c)
weakenIsCoord :: KnownNat m => c n -> Maybe (c m)
weakenIsCoord = fmap (review asOrdinal) . weakenOrdinal . view asOrdinal
strengthenIsCoord :: (KnownNat m, (n <= m)) => c n -> c m
strengthenIsCoord = review asOrdinal . strengthenOrdinal . view asOrdinal
class ( x ~ ((CoordContainer x) (CoordNat x))
, 1 <= CoordNat x
, IsCoord (CoordContainer x)
, KnownNat (CoordNat x)
) =>
IsCoordLifted x
where
type CoordContainer x :: Nat -> *
type CoordNat x :: Nat
instance (KnownNat n, 1 <= n, IsCoord c) => IsCoordLifted (c n) where
type CoordContainer (c n) = c
type CoordNat (c n) = n
instance IsCoord Ordinal where
asOrdinal = id
zeroPosition = Ordinal (Proxy @0)
asSizeProxy (Ordinal p) func = func p
maxCoord :: forall n proxy . KnownNat n => proxy n -> Ordinal n
maxCoord _ = fromJust $ numToOrdinal (maxCoordSize (Proxy :: Proxy (Ordinal n)))
allCoordLike :: (1 <= n, IsCoord c, KnownNat n) => [c n]
allCoordLike = toListOf (traverse . re asOrdinal) [minBound .. maxBound]