Safe Haskell	None
Language	Haskell2010

SizedGrid.Coord.Class

Synopsis

coordFromNatCollapse :: forall a x y. Dict (CoordFromNat (CoordFromNat a x) y ~ CoordFromNat a y)
coordFromNatSame :: (CoordFromNat a ~ CoordFromNat b) :- (a ~ CoordFromNat b (CoordSized a))
coordSizedCollapse :: forall c n. Dict (CoordSized (CoordFromNat c n) ~ n)
class (1 <= CoordSized c, KnownNat (CoordSized c)) => IsCoord c where
- type CoordSized c :: Nat
- type CoordFromNat c :: Nat -> *
- asOrdinal :: Iso' c (Ordinal (CoordSized c))
- zeroPosition :: c
- sCoordSized :: proxy c -> Proxy (CoordSized c)
- maxCoordSize :: proxy c -> Integer
- maxCoord :: c
- asSizeProxy :: c -> (forall n. (KnownNat n, (n + 1) <= CoordSized c) => Proxy n -> x) -> x
- weakenIsCoord :: IsCoord (CoordFromNat c n) => c -> Maybe (CoordFromNat c n)
- strengthenIsCoord :: (IsCoord (CoordFromNat c n), CoordSized c <= CoordSized (CoordFromNat c n)) => c -> CoordFromNat c n
allCoordLike :: IsCoord c => [c]

Documentation

coordFromNatCollapse :: forall a x y. Dict (CoordFromNat (CoordFromNat a x) y ~ CoordFromNat a y) Source #

Proof an idiom about how CoordFromNat works. This relies on 'CoordFromNat a (CoordSized a ~ a'

coordFromNatSame :: (CoordFromNat a ~ CoordFromNat b) :- (a ~ CoordFromNat b (CoordSized a)) Source #

coordSizedCollapse :: forall c n. Dict (CoordSized (CoordFromNat c n) ~ n) Source #

class (1 <= CoordSized c, KnownNat (CoordSized c)) => IsCoord c where Source #

Everything that can be uses as a Coordinate. The only required function is asOrdinal and the type instance of CoordSized: the rest can be derived automatically.

This is kind * -> Constraint for ease of use later. There is some argument that it should be of kind (Nat -> *) -> Constraint and we could remove CoordSized, but that has other complications

Minimal complete definition

asOrdinal

Associated Types

type CoordSized c :: Nat Source #

The maximum number of values that a Coord can take

type CoordFromNat c :: Nat -> * Source #

Methods

asOrdinal :: Iso' c (Ordinal (CoordSized c)) Source #

As each coord represents a finite number of states, it must be isomorphic to an Ordinal

zeroPosition :: c Source #

The origin. If c is an instance of Monoid, this should be mempty

zeroPosition :: Monoid c => c Source #

The origin. If c is an instance of Monoid, this should be mempty

sCoordSized :: proxy c -> Proxy (CoordSized c) Source #

Retrive a Proxy of the size

maxCoordSize :: proxy c -> Integer Source #

The largest possible number expressable

maxCoord :: c Source #

asSizeProxy :: c -> (forall n. (KnownNat n, (n + 1) <= CoordSized c) => Proxy n -> x) -> x Source #

weakenIsCoord :: IsCoord (CoordFromNat c n) => c -> Maybe (CoordFromNat c n) Source #

strengthenIsCoord :: (IsCoord (CoordFromNat c n), CoordSized c <= CoordSized (CoordFromNat c n)) => c -> CoordFromNat c n Source #

Instances

(1 <= n, KnownNat n) => IsCoord (Ordinal n) Source #
Instance details Defined in SizedGrid.Coord.Class Associated Types type CoordSized (Ordinal n) :: Nat Source # type CoordFromNat (Ordinal n) :: Nat -> Type Source # Methods asOrdinal :: Iso' (Ordinal n) (Ordinal (CoordSized (Ordinal n))) Source # zeroPosition :: Ordinal n Source # sCoordSized :: proxy (Ordinal n) -> Proxy (CoordSized (Ordinal n)) Source # maxCoordSize :: proxy (Ordinal n) -> Integer Source # maxCoord :: Ordinal n Source # asSizeProxy :: Ordinal n -> (forall (n0 :: Nat). (KnownNat n0, (n0 + 1) <= CoordSized (Ordinal n)) => Proxy n0 -> x) -> x Source # weakenIsCoord :: IsCoord (CoordFromNat (Ordinal n) n0) => Ordinal n -> Maybe (CoordFromNat (Ordinal n) n0) Source # strengthenIsCoord :: (IsCoord (CoordFromNat (Ordinal n) n0), CoordSized (Ordinal n) <= CoordSized (CoordFromNat (Ordinal n) n0)) => Ordinal n -> CoordFromNat (Ordinal n) n0 Source #
(1 <= n, KnownNat n) => IsCoord (Periodic n) Source #
Instance details Defined in SizedGrid.Coord.Periodic Associated Types type CoordSized (Periodic n) :: Nat Source # type CoordFromNat (Periodic n) :: Nat -> Type Source # Methods asOrdinal :: Iso' (Periodic n) (Ordinal (CoordSized (Periodic n))) Source # zeroPosition :: Periodic n Source # sCoordSized :: proxy (Periodic n) -> Proxy (CoordSized (Periodic n)) Source # maxCoordSize :: proxy (Periodic n) -> Integer Source # maxCoord :: Periodic n Source # asSizeProxy :: Periodic n -> (forall (n0 :: Nat). (KnownNat n0, (n0 + 1) <= CoordSized (Periodic n)) => Proxy n0 -> x) -> x Source # weakenIsCoord :: IsCoord (CoordFromNat (Periodic n) n0) => Periodic n -> Maybe (CoordFromNat (Periodic n) n0) Source # strengthenIsCoord :: (IsCoord (CoordFromNat (Periodic n) n0), CoordSized (Periodic n) <= CoordSized (CoordFromNat (Periodic n) n0)) => Periodic n -> CoordFromNat (Periodic n) n0 Source #
(1 <= n, KnownNat n) => IsCoord (HardWrap n) Source #
Instance details Defined in SizedGrid.Coord.HardWrap Associated Types type CoordSized (HardWrap n) :: Nat Source # type CoordFromNat (HardWrap n) :: Nat -> Type Source # Methods asOrdinal :: Iso' (HardWrap n) (Ordinal (CoordSized (HardWrap n))) Source # zeroPosition :: HardWrap n Source # sCoordSized :: proxy (HardWrap n) -> Proxy (CoordSized (HardWrap n)) Source # maxCoordSize :: proxy (HardWrap n) -> Integer Source # maxCoord :: HardWrap n Source # asSizeProxy :: HardWrap n -> (forall (n0 :: Nat). (KnownNat n0, (n0 + 1) <= CoordSized (HardWrap n)) => Proxy n0 -> x) -> x Source # weakenIsCoord :: IsCoord (CoordFromNat (HardWrap n) n0) => HardWrap n -> Maybe (CoordFromNat (HardWrap n) n0) Source # strengthenIsCoord :: (IsCoord (CoordFromNat (HardWrap n) n0), CoordSized (HardWrap n) <= CoordSized (CoordFromNat (HardWrap n) n0)) => HardWrap n -> CoordFromNat (HardWrap n) n0 Source #

allCoordLike :: IsCoord c => [c] Source #

Enumerate all possible values of a coord, in order