diff --git a/ChangeLog.md b/ChangeLog.md --- a/ChangeLog.md +++ b/ChangeLog.md @@ -1,6 +1,12 @@ # Revision history for sized-grid -## 0.1.1.5 -- 2018-11-21 +## 0.2.0.0 -- NOT PUBLISHED + +* _WrappedCoord is now an Iso + +* IsCoord is now of kind Nat -> *. Introduced IsCoordLifted. This is unfortunatly a breaking change + +## 0.1.1.6 -- 2018-11-21 * Reduced bound on generics-sop diff --git a/README.lhs b/README.lhs --- a/README.lhs +++ b/README.lhs @@ -96,7 +96,7 @@ ```haskell applyRule :: - ( All IsCoord cs + ( All IsCoordLifted cs , All Monoid cs , All Semigroup cs , All AffineSpace cs @@ -121,8 +121,8 @@ displayTileState Alive = '#' displayTileState Dead = '.' -displayGrid :: (KnownNat (CoordSized x), KnownNat (CoordSized y)) => - Grid '[x, y] TileState -> String +displayGrid :: (KnownNat (x GHC.* y), KnownNat x, KnownNat y) => + Grid '[f x, g y] TileState -> String displayGrid = unlines . collapseGrid . fmap displayTileState ``` @@ -130,13 +130,13 @@ ```haskell glider :: - ( KnownNat (CoordSized x GHC.* CoordSized y) + ( KnownNat (CoordNat x GHC.* CoordNat y) , Semigroup x , Semigroup y , Monoid x , Monoid y - , IsCoord x - , IsCoord y + , IsCoordLifted x + , IsCoordLifted y , AffineSpace x , AffineSpace y , Diff x ~ Integer diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -96,7 +96,7 @@ ```haskell applyRule :: - ( All IsCoord cs + ( All IsCoordLifted cs , All Monoid cs , All Semigroup cs , All AffineSpace cs @@ -121,8 +121,8 @@ displayTileState Alive = '#' displayTileState Dead = '.' -displayGrid :: (KnownNat (CoordSized x), KnownNat (CoordSized y)) => - Grid '[x, y] TileState -> String +displayGrid :: (KnownNat (x GHC.* y), KnownNat x, KnownNat y) => + Grid '[f x, g y] TileState -> String displayGrid = unlines . collapseGrid . fmap displayTileState ``` @@ -130,13 +130,13 @@ ```haskell glider :: - ( KnownNat (CoordSized x GHC.* CoordSized y) + ( KnownNat (CoordNat x GHC.* CoordNat y) , Semigroup x , Semigroup y , Monoid x , Monoid y - , IsCoord x - , IsCoord y + , IsCoordLifted x + , IsCoordLifted y , AffineSpace x , AffineSpace y , Diff x ~ Integer diff --git a/sized-grid.cabal b/sized-grid.cabal --- a/sized-grid.cabal +++ b/sized-grid.cabal @@ -1,5 +1,5 @@ name: sized-grid -version: 0.1.1.6 +version: 0.2.0.1 cabal-version: >=1.10 category: Data build-type: Simple @@ -41,7 +41,7 @@ comonad >=5.0 && <5.1, constraints >= 0.9 && < 0.11, distributive >=0.5 && <1, - generics-sop >=0.3 && <0.5, + generics-sop >=0.3 && <0.6, lens >=4.15 && <5, mtl >=2.2.2 && <2.3, random ==1.1.*, @@ -61,10 +61,10 @@ HUnit >=1.6.0.0 && <1.7, aeson >=1.2 && <1.5, adjunctions >= 4.3 && < 4.5, - generics-sop >=0.3 && <0.5, + generics-sop >=0.3 && <0.6, lens >=4.15 && <5, sized-grid -any, - tasty >=1.0 && <1.2, + tasty >=1.0 && <2.1, tasty-hunit >=0.10 && <0.11, vector >=0.12 && <0.13, vector-space >=0.10 && < 2, @@ -81,7 +81,7 @@ main-is: README.lhs build-depends: base >=4.9 && <4.13, - ansi-terminal >=0.8.0.2 && <0.9, + ansi-terminal >=0.8.0.2 && <0.10, adjunctions >= 4.3 && < 4.5, comonad >=5.0 && <5.1, distributive >=0.5 && <1, diff --git a/src/SizedGrid/Coord.hs b/src/SizedGrid/Coord.hs --- a/src/SizedGrid/Coord.hs +++ b/src/SizedGrid/Coord.hs @@ -61,8 +61,8 @@ infixr 5 :| -_WrappedCoord :: Lens' (Coord cs) (NP I cs) -_WrappedCoord f (Coord n) = Coord <$> f n +_WrappedCoord :: Iso' (Coord cs) (NP I cs) +_WrappedCoord = dimap unCoord (fmap Coord) instance All Eq cs => Eq (Coord cs) where Coord a == Coord b = @@ -206,30 +206,37 @@ -- | Generate all possible coords in order allCoord :: - forall cs. (All IsCoord cs) + forall cs. (All IsCoordLifted cs) => [Coord cs] -allCoord = Coord <$> hsequence (hcpure (Proxy :: Proxy IsCoord) allCoordLike) +allCoord = + Coord <$> + hsequence + (hcpure (Proxy :: Proxy IsCoordLifted) (allCoordLike)) -- | The number of elements a coord can have. This is equal to the product of the `CoordSized` of each element type family MaxCoordSize (cs :: [k]) :: GHC.Nat where MaxCoordSize '[] = 1 - MaxCoordSize (c ': cs) = (CoordSized c) GHC.* (MaxCoordSize cs) + MaxCoordSize ((c n) ': cs) = n GHC.* (MaxCoordSize cs) -- | Convert a `Coord` to its position in a vector -coordPosition :: (All IsCoord cs) => Coord cs -> Int +coordPosition :: (All IsCoordLifted cs) => Coord cs -> Int coordPosition (Coord a) = - let helper :: (All IsCoord xs) => NP I xs -> Integer + let helper :: (All IsCoordLifted xs) => NP I xs -> Integer helper Nil = 0 helper (I c :* (cs :: NP I ys)) = ordinalToNum (c ^. asOrdinal) * sizeOfList cs + helper cs - sizeOfList :: All IsCoord xs => NP I xs -> Integer + sizeOfList :: All IsCoordLifted xs => NP I xs -> Integer sizeOfList = product . hcollapse . hcmap - (Proxy :: Proxy IsCoord) - (\(I (_ :: a)) -> K $ 1 + maxCoordSize (Proxy :: Proxy a)) - in fromIntegral $ helper a + (Proxy :: Proxy IsCoordLifted) + (\(I (_ :: a)) -> + K $ + 1 + + maxCoordSize + (Proxy :: Proxy ((CoordContainer a) (CoordNat a)))) + in fromIntegral $ helper a -- | All Diffs of the members of the list must be equal type family AllDiffSame a xs :: Constraint where @@ -283,8 +290,8 @@ tranposeCoord (Coord (a :* b :* Nil)) = Coord (b :* a :* Nil) -- | The zero position for a coord -zeroCoord :: All IsCoord cs => Coord cs -zeroCoord = Coord $ hcpure (Proxy :: Proxy IsCoord) (I $ zeroPosition) +zeroCoord :: All IsCoordLifted cs => Coord cs +zeroCoord = Coord $ hcpure (Proxy :: Proxy IsCoordLifted) (I $ zeroPosition) class AllSizedKnown (cs :: [*]) where sizeProof :: Dict (KnownNat (MaxCoordSize cs)) @@ -292,12 +299,12 @@ instance AllSizedKnown '[] where sizeProof = Dict -instance (KnownNat (CoordSized a), AllSizedKnown as) => - AllSizedKnown (a ': as) where +instance (KnownNat n, AllSizedKnown as) => + AllSizedKnown ((c n) ': as) where sizeProof = withDict (sizeProof @as) - (Dict \\ (timesNat @(CoordSized a) @(MaxCoordSize as))) + (Dict \\ (timesNat @n @(MaxCoordSize as))) class WeakenCoord as bs where weakenCoord :: Coord as -> Maybe (Coord bs) @@ -305,17 +312,13 @@ instance WeakenCoord '[] '[] where weakenCoord c = Just c -instance ( b ~ CoordFromNat a n - , WeakenCoord as bs - , IsCoord a - , IsCoord (CoordFromNat a n) - ) => - WeakenCoord (a ': as) (b ': bs) where - weakenCoord (a :| as) = do - bs <- weakenCoord as - b <- weakenIsCoord a - return (b :| bs) - weakenCoord _ = error "Unreachable pattern in weakenCoord" +instance (WeakenCoord as bs, IsCoord c, KnownNat m) => + WeakenCoord ((c n) ': as) ((c m) ': bs) where + weakenCoord (a :| as) = do + bs <- weakenCoord as + b <- weakenIsCoord a + return (b :| bs) + weakenCoord _ = error "Unreachable pattern in weakenCoord" class StrengthenCoord as bs where strengthenCoord :: Coord as -> Coord bs @@ -324,11 +327,10 @@ strengthenCoord c = c instance ( StrengthenCoord as bs - , IsCoord (CoordFromNat a n) - , IsCoord a - , b ~ CoordFromNat a n - , CoordSized a <= CoordSized (CoordFromNat a n) + , IsCoord c + , n <= m + , KnownNat m ) => - StrengthenCoord (a ': as) (b ': bs) where + StrengthenCoord ((c n) ': as) ((c m) ': bs) where strengthenCoord (a :| as) = strengthenIsCoord a :| strengthenCoord as strengthenCoord _ = error "Unreachable pattern in strengthenCoord" diff --git a/src/SizedGrid/Coord/Class.hs b/src/SizedGrid/Coord/Class.hs --- a/src/SizedGrid/Coord/Class.hs +++ b/src/SizedGrid/Coord/Class.hs @@ -1,85 +1,85 @@ -{-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE DefaultSignatures #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeOperators #-} +{-# 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.Constraint import Data.Maybe (fromJust) import Data.Proxy import GHC.TypeLits -import Unsafe.Coerce (unsafeCoerce) --- | Proof an idiom about how `CoordFromNat` works. This relies on 'CoordFromNat a (CoordSized a ~ a' -coordFromNatCollapse :: - forall a x y. Dict (CoordFromNat (CoordFromNat a x) y ~ CoordFromNat a y) -coordFromNatCollapse = unsafeCoerce (Dict :: Dict (z ~ z)) - -coordFromNatSame :: - (CoordFromNat a ~ CoordFromNat b) :- (a ~ CoordFromNat b (CoordSized a)) -coordFromNatSame = Sub (unsafeCoerce (Dict :: Dict (a ~ a))) - -coordSizedCollapse :: forall c n . Dict (CoordSized (CoordFromNat c n) ~ n) -coordSizedCollapse = unsafeCoerce (Dict :: Dict (a ~ a)) - -- | 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 -class (1 <= CoordSized c, KnownNat (CoordSized c)) => IsCoord c where - -- | The maximum number of values that a Coord can take - type CoordSized c :: Nat - type CoordFromNat c :: (Nat -> *) +class IsCoord (c :: Nat -> *) where -- | As each coord represents a finite number of states, it must be isomorphic to an Ordinal - asOrdinal :: Iso' c (Ordinal (CoordSized c)) + asOrdinal :: Iso' (c n) (Ordinal n) + -- | The origin. If c is an instance of `Monoid`, this should be mempty - zeroPosition :: c - default zeroPosition :: Monoid c => c + zeroPosition :: (1 <= n, KnownNat n) => c n + default zeroPosition :: Monoid (c n) => c n zeroPosition = mempty + -- | Retrive a `Proxy` of the size - sCoordSized :: proxy c -> Proxy (CoordSized c) + sCoordSized :: Proxy (c n) -> Proxy n sCoordSized _ = Proxy + -- | The largest possible number expressable - maxCoordSize :: proxy c -> Integer + maxCoordSize :: KnownNat n => Proxy (c n) -> Integer maxCoordSize p = natVal (sCoordSized p) - 1 - maxCoord :: c - maxCoord = view (re asOrdinal) maxCoord + -- | The maximum value of a coord + maxCoord :: KnownNat n => Proxy n -> c n + maxCoord _ = view (re asOrdinal) (maxCoord (Proxy :: Proxy n)) asSizeProxy :: - c - -> (forall n. (KnownNat n, n + 1 <= (CoordSized c)) => - Proxy n -> x) + c n + -> (forall m. (KnownNat m, m + 1 <= n) => + Proxy m -> x) -> x asSizeProxy c = asSizeProxy (view asOrdinal c) - weakenIsCoord :: IsCoord (CoordFromNat c n) => c -> Maybe (CoordFromNat c n) + weakenIsCoord :: KnownNat m => c n -> Maybe (c m) weakenIsCoord = fmap (review asOrdinal) . weakenOrdinal . view asOrdinal - strengthenIsCoord :: - (IsCoord (CoordFromNat c n), CoordSized c <= CoordSized (CoordFromNat c n)) - => c - -> CoordFromNat c n + strengthenIsCoord :: (KnownNat m, (n <= m)) => c n -> c m strengthenIsCoord = review asOrdinal . strengthenOrdinal . view asOrdinal -instance (1 <= n, KnownNat n) => IsCoord (Ordinal n) where - type CoordSized (Ordinal n) = n - type CoordFromNat (Ordinal n) = Ordinal +-- | Sometimes it useful to work with Coords of type *, not Nat -> *. This is away of doing so. +-- | +-- | It should be autogenerated for all valid instances of `IsCoord` +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 = fromJust $ numToOrdinal (maxCoordSize (Proxy :: Proxy (Ordinal n))) + maxCoord :: forall n proxy . KnownNat n => proxy n -> Ordinal n + maxCoord _ = fromJust $ numToOrdinal (maxCoordSize (Proxy :: Proxy (Ordinal n))) -- | Enumerate all possible values of a coord, in order -allCoordLike :: IsCoord c => [c] +allCoordLike :: (1 <= n, IsCoord c, KnownNat n) => [c n] allCoordLike = toListOf (traverse . re asOrdinal) [minBound .. maxBound] diff --git a/src/SizedGrid/Coord/HardWrap.hs b/src/SizedGrid/Coord/HardWrap.hs --- a/src/SizedGrid/Coord/HardWrap.hs +++ b/src/SizedGrid/Coord/HardWrap.hs @@ -36,10 +36,8 @@ deriving instance KnownNat n => ToJSONKey (HardWrap n) deriving instance KnownNat n => FromJSONKey (HardWrap n) -instance (1 <= n, KnownNat n) => IsCoord (HardWrap n) where - type CoordSized (HardWrap n) = n - type CoordFromNat (HardWrap n) = HardWrap - asOrdinal = iso unHardWrap HardWrap +instance IsCoord HardWrap where + asOrdinal = iso unHardWrap HardWrap instance (1 <= n, KnownNat n) => Semigroup (HardWrap n) where HardWrap a <> HardWrap b = diff --git a/src/SizedGrid/Coord/Periodic.hs b/src/SizedGrid/Coord/Periodic.hs --- a/src/SizedGrid/Coord/Periodic.hs +++ b/src/SizedGrid/Coord/Periodic.hs @@ -50,10 +50,8 @@ (fromIntegral x) `mod` (maxCoordSize (Proxy @(Periodic n))) fromEnum (Periodic o) = ordinalToNum o -instance (1 <= n, KnownNat n) => IsCoord (Periodic n) where - type CoordSized (Periodic n) = n - type CoordFromNat (Periodic n) = Periodic - asOrdinal = iso unPeriodic Periodic +instance IsCoord Periodic where + asOrdinal = iso unPeriodic Periodic instance (1 <= n, KnownNat n) => Semigroup (Periodic n) where Periodic a <> Periodic b = diff --git a/src/SizedGrid/Grid/Class.hs b/src/SizedGrid/Grid/Class.hs --- a/src/SizedGrid/Grid/Class.hs +++ b/src/SizedGrid/Grid/Class.hs @@ -32,7 +32,7 @@ -- | Convert to, or run a function over, a `FocusedGrid` asFocusedGrid :: Lens' (grid a) (FocusedGrid cs a) -instance (AllSizedKnown cs, All IsCoord cs) => +instance (AllSizedKnown cs, All IsCoordLifted cs) => IsGrid cs (Grid cs) where gridIndex coord = lens @@ -42,7 +42,7 @@ asFocusedGrid = lens (\g -> FocusedGrid g zeroCoord) (\_ fg -> focusedGrid fg) -instance (AllSizedKnown cs, All IsCoord cs) => +instance (AllSizedKnown cs, All IsCoordLifted cs) => IsGrid cs (FocusedGrid cs) where gridIndex c = (\f (FocusedGrid g p) -> (\g' -> FocusedGrid g' p) <$> f g) . diff --git a/src/SizedGrid/Grid/Focused.hs b/src/SizedGrid/Grid/Focused.hs --- a/src/SizedGrid/Grid/Focused.hs +++ b/src/SizedGrid/Grid/Focused.hs @@ -25,7 +25,7 @@ } deriving (Functor,Foldable,Traversable) instance ( AllSizedKnown cs - , All IsCoord cs + , All IsCoordLifted cs , All Monoid cs , All Semigroup cs , SListI cs @@ -35,7 +35,7 @@ duplicate (FocusedGrid g p) = FocusedGrid (tabulate (FocusedGrid g)) p instance ( AllSizedKnown cs - , All IsCoord cs + , All IsCoordLifted cs , All Monoid cs , All Semigroup cs , SListI cs diff --git a/src/SizedGrid/Grid/Grid.hs b/src/SizedGrid/Grid/Grid.hs --- a/src/SizedGrid/Grid/Grid.hs +++ b/src/SizedGrid/Grid/Grid.hs @@ -51,27 +51,27 @@ (fromIntegral $ GHC.natVal (Proxy :: Proxy (MaxCoordSize cs)))) Grid fs <*> Grid as = Grid $ V.zipWith ($) fs as -instance (AllSizedKnown cs, All IsCoord cs) => +instance (AllSizedKnown cs, All IsCoordLifted cs) => Monad (Grid cs) where g >>= f = imap (\p a -> f a `index` p) g -instance (AllSizedKnown cs, All IsCoord cs) => +instance (AllSizedKnown cs, All IsCoordLifted cs) => Distributive (Grid cs) where distribute = distributeRep -instance (All IsCoord cs, AllSizedKnown cs) => +instance (All IsCoordLifted cs, AllSizedKnown cs) => Representable (Grid cs) where type Rep (Grid cs) = Coord cs tabulate func = Grid $ V.fromList $ map func $ allCoord index (Grid v) c = v V.! coordPosition c -instance (All IsCoord cs) => FunctorWithIndex (Coord cs) (Grid cs) where +instance (All IsCoordLifted cs) => FunctorWithIndex (Coord cs) (Grid cs) where imap func (Grid v) = Grid $ V.zipWith func (V.fromList allCoord) v -instance (All IsCoord cs) => FoldableWithIndex (Coord cs) (Grid cs) where +instance (All IsCoordLifted cs) => FoldableWithIndex (Coord cs) (Grid cs) where ifoldMap func (Grid v) = foldMap id $ V.zipWith func (V.fromList allCoord) v -instance (All IsCoord cs) => TraversableWithIndex (Coord cs) (Grid cs) where +instance (All IsCoordLifted cs) => TraversableWithIndex (Coord cs) (Grid cs) where itraverse func (Grid v) = Grid <$> sequenceA (V.zipWith func (V.fromList allCoord) v) @@ -91,10 +91,12 @@ -- | A Constraint that all grid sizes are instances of `KnownNat` type family AllGridSizeKnown cs :: Constraint where AllGridSizeKnown '[] = () - AllGridSizeKnown cs = ( GHC.KnownNat (CoordSized (Head cs)) + AllGridSizeKnown cs = ( GHC.KnownNat (CoordNat (Head cs)) , GHC.KnownNat (MaxCoordSize (Tail cs)) + , GHC.KnownNat (MaxCoordSize (cs)) , AllGridSizeKnown (Tail cs)) + -- | Convert a vector into a list of `Vector`s, where all the elements of the list have the given size. splitVectorBySize :: Int -> V.Vector a -> [V.Vector a] splitVectorBySize n v @@ -110,10 +112,10 @@ collapseGrid (Grid v) = case (shape :: Shape cs) of ShapeNil -> v V.! 0 - ShapeCons _ -> - map (collapseGrid . Grid @(Tail cs)) $ + ShapeCons (_ :: Shape xs) -> + map (collapseGrid . Grid @xs) $ splitVectorBySize - (fromIntegral $ GHC.natVal (Proxy @(MaxCoordSize (Tail cs)))) + (fromIntegral $ GHC.natVal (Proxy @(MaxCoordSize xs))) v -- | Convert a series of nested lists to a grid. If the size of the grid does not match the size of lists this will be `Nothing` @@ -125,7 +127,7 @@ case (shape :: Shape cs) of ShapeNil -> Just $ Grid $ V.singleton $ cg ShapeCons _ -> - if length cg == fromIntegral (GHC.natVal (Proxy @(CoordSized (Head cs)))) + if length cg == fromIntegral (GHC.natVal (Proxy @(CoordNat (Head cs)))) then Grid . mconcat <$> traverse (fmap unGrid . gridFromList @(Tail cs)) cg else Nothing @@ -141,7 +143,7 @@ (fromIntegral $ GHC.natVal (Proxy @(MaxCoordSize (Tail cs)))) v -instance (All IsCoord cs, FromJSON a) => FromJSON (Grid cs a) where +instance (All IsCoordLifted cs, FromJSON a) => FromJSON (Grid cs a) where parseJSON v = case (shape :: Shape cs) of ShapeNil -> Grid . V.singleton <$> parseJSON v @@ -152,11 +154,13 @@ transposeGrid :: ( IsCoord h , IsCoord w - , GHC.KnownNat (MaxCoordSize '[ w, h]) - , GHC.KnownNat (MaxCoordSize '[ h, w]) + , GHC.KnownNat x + , GHC.KnownNat y + , 1 <= y + , 1 <= x ) - => Grid '[ w, h] a - -> Grid '[ h, w] a + => Grid '[ w x, h y] a + -> Grid '[ h y, w x] a transposeGrid g = tabulate $ \i -> index g $ tranposeCoord i splitGrid :: @@ -178,40 +182,39 @@ combineGrid (Grid v) = Grid (v >>= unGrid) combineHigherDim :: - ( CoordFromNat a ~ CoordFromNat b - , c ~ CoordFromNat a ((GHC.+) (CoordSized a) (CoordSized b))) - => Grid (a ': as) x - -> Grid (b ': as) x - -> Grid (c ': as) x + ( IsCoord c) + => Grid (c n ': as) x + -> Grid (c m ': as) x + -> Grid (c (n + m) ': as) x combineHigherDim (Grid v1) (Grid v2) = Grid (v1 <> v2) dropGrid :: KnownNat n => Proxy n - -> Grid '[ c] x - -> Grid '[ CoordFromNat c (CoordSized c - n)] x + -> Grid '[ c m] x + -> Grid '[ c (m - n)] x dropGrid p (Grid v) = Grid $ V.drop (fromIntegral $ natVal p) v -takeGrid :: KnownNat n => Proxy n -> Grid '[c] x -> Grid '[CoordFromNat c n] x +takeGrid :: KnownNat n => Proxy n -> Grid '[c m] x -> Grid '[c n] x takeGrid p (Grid v) = Grid $ V.take (fromIntegral $ natVal p) v - splitHigherDim :: - forall a b c as x. - ( KnownNat (CoordSized b) - , c ~ CoordFromNat a (CoordSized a - CoordSized b) - , CoordSized b <= CoordSized a + forall c as x y z a. + ( KnownNat x + , KnownNat y + , y <= x , AllSizedKnown as + , IsCoord c ) - => Grid (a ': as) x - -> (Grid (b ': as) x, Grid (c ': as) x) + => Grid (c x ': as) a + -> (Grid (c y ': as) a, Grid (c z ': as) a) splitHigherDim (Grid v) = let (a, b) = withDict (sizeProof @as) (V.splitAt (fromIntegral $ - GHC.natVal (Proxy @(CoordSized b)) * + GHC.natVal (Proxy @y) * GHC.natVal (Proxy @(MaxCoordSize as))) v) in (Grid a, Grid b) @@ -236,23 +239,19 @@ instance ShrinkableGrid '[] '[] '[] where shrinkGrid _ (Grid v) = Grid v -instance ( KnownNat (CoordSized b) +instance ( KnownNat z , AllSizedKnown as , IsCoord c , ShrinkableGrid cs as bs - , CoordFromNat b ~ CoordFromNat a - , CoordSized b <= (CoordSized a - CoordSized c + 1) + , z <= (x - y + 1) ) => - ShrinkableGrid (c ': cs) (a ': as) (b ': bs) where + ShrinkableGrid (c x ': cs) (c y ': as) (c z ': bs) where shrinkGrid (c :| cs) = combineGrid . fmap (shrinkGrid cs) . helper . splitGrid where - helper :: Grid '[ a] x -> Grid '[ b] x + helper :: Grid '[ c y] a -> Grid '[ c z] a helper g = asSizeProxy c $ \(pTake :: Proxy n) -> - withDict - (coordFromNatCollapse @a @(CoordSized a - n) @(CoordSized b)) - (takeGrid (Proxy :: Proxy (CoordSized b)) (dropGrid pTake g) \\ - coordFromNatSame @b @a) + takeGrid (Proxy :: Proxy z) (dropGrid pTake g) shrinkGrid _ = error "Impossible pattern in shrinkGrid" diff --git a/tests/Main.hs b/tests/Main.hs --- a/tests/Main.hs +++ b/tests/Main.hs @@ -53,26 +53,26 @@ in assertBool "Ordered" . helper testAllCoordOrdered :: - forall cs proxy. (All Eq cs, All Ord cs, All IsCoord cs) + forall cs proxy. (All Eq cs, All Ord cs, All IsCoordLifted cs) => proxy (Coord cs) -> TestTree testAllCoordOrdered _ = testCase "allCoord is ordered" $ assertOrderd (allCoord @cs) gridTests :: - forall cs a x y. + forall cs a x y f g. ( Show (Coord cs) , Eq (Coord cs) - , All IsCoord cs + , All IsCoordLifted cs , AllSizedKnown cs , Show a , Eq a - , cs ~ '[ x, y] - , KnownNat (CoordSized y GHC.* CoordSized x) - , KnownNat (CoordSized x GHC.* CoordSized y) + , cs ~ '[ f x, g y] + , KnownNat (y GHC.* x) + , KnownNat (x GHC.* y) , Arbitrary a - , Arbitrary x - , Arbitrary y + , Arbitrary (f x) + , Arbitrary (g y) ) => Proxy (Coord cs) -> Proxy a @@ -88,8 +88,8 @@ uncollapseCollapse = property $ do cg :: [[a]] <- - replicateM (fromIntegral $ natVal (Proxy @(CoordSized x))) $ - replicateM (fromIntegral $ natVal (Proxy @(CoordSized y))) $ + replicateM (fromIntegral $ natVal (Proxy @x)) $ + replicateM (fromIntegral $ natVal (Proxy @y)) $ arbitrary return (Just cg === (collapseGrid <$> gridFromList @cs cg)) doubleTranspose = @@ -103,32 +103,32 @@ ] splitTests :: - forall c cs a. + forall c x cs a. ( Show a , Eq a , Num a - , All IsCoord (c ': cs) - , KnownNat (CoordSized c GHC.* MaxCoordSize cs) + , All IsCoordLifted ((c x) ': cs) + , KnownNat (x GHC.* MaxCoordSize cs) , KnownNat (MaxCoordSize cs) , KnownNat (5 GHC.* MaxCoordSize cs) , KnownNat (3 GHC.* MaxCoordSize cs) , KnownNat (2 GHC.* MaxCoordSize cs) - , KnownNat (CoordSized (CoordFromNat c 2) GHC.* MaxCoordSize cs) - , KnownNat (CoordSized (CoordFromNat c 2)) + , KnownNat (2 GHC.* MaxCoordSize cs) + , KnownNat 2 , AllSizedKnown cs , Arbitrary a ) - => Proxy (c ': cs) + => Proxy ((c x) ': cs) -> Proxy a -> [TestTree] splitTests _ _ = let splitAndCombine = property $ do - g :: Grid (c ': cs) a <- sequenceA $ pure arbitrary + g :: Grid ((c x) ': cs) a <- sequenceA $ pure arbitrary return (g === combineGrid (splitGrid g)) combineAndSplit = property $ do - g :: Grid '[ c] (Grid cs a) <- + g :: Grid '[ c x] (Grid cs a) <- sequenceA $ pure (sequenceA $ pure arbitrary) return (g === splitGrid (combineGrid g)) higherSplitAndCombine = diff --git a/tests/Test/Utils.hs b/tests/Test/Utils.hs --- a/tests/Test/Utils.hs +++ b/tests/Test/Utils.hs @@ -1,9 +1,12 @@ {-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} module Test.Utils where @@ -109,10 +112,8 @@ applicativeLaws :: forall f a. ( Applicative f - , Traversable f , Show (f a) , Eq (f a) - , Show a , Arbitrary a , Arbitrary1 f , Function a @@ -189,25 +190,25 @@ [testProperty "Pure Id" pureId, testProperty "Compose" compose] isCoordLaws :: - forall a. (IsCoord a) - => Proxy a + forall c n. (IsCoord c, 1 <= n, KnownNat n) + => Proxy (c n) -> TestTree isCoordLaws p = testCase "IsCoord Laws" $ do assertEqual "Max coord size is sCoordSized" - (maxCoordSize p) + (maxCoordSize (Proxy :: Proxy (c n))) (natVal (sCoordSized p) - 1) assertEqual "zeroPosition is Zero" (0 :: Int) - (ordinalToNum $ view asOrdinal (zeroPosition @a)) + (ordinalToNum $ view asOrdinal (zeroPosition @c @n)) assertEqual "Size Proxy Zero" (0 :: Integer) - (asSizeProxy (zeroPosition @a) natVal) + (asSizeProxy (zeroPosition @c @n) natVal) assertEqual "Max size equality" - (ordinalToNum $ view asOrdinal (maxCoord @a)) + (ordinalToNum $ view (asOrdinal @c) (maxCoord (Proxy @n))) (maxCoordSize p)