sized-grid 0.1.1.6 → 0.2.0.1
raw patch · 13 files changed
+184/−180 lines, 13 filesdep ~ansi-terminaldep ~generics-sopdep ~tasty
Dependency ranges changed: ansi-terminal, generics-sop, tasty
Files
- ChangeLog.md +7/−1
- README.lhs +6/−6
- README.md +6/−6
- sized-grid.cabal +5/−5
- src/SizedGrid/Coord.hs +34/−32
- src/SizedGrid/Coord/Class.hs +51/−51
- src/SizedGrid/Coord/HardWrap.hs +2/−4
- src/SizedGrid/Coord/Periodic.hs +2/−4
- src/SizedGrid/Grid/Class.hs +2/−2
- src/SizedGrid/Grid/Focused.hs +2/−2
- src/SizedGrid/Grid/Grid.hs +40/−41
- tests/Main.hs +18/−18
- tests/Test/Utils.hs +9/−8
ChangeLog.md view
@@ -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
README.lhs view
@@ -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
README.md view
@@ -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
sized-grid.cabal view
@@ -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,
src/SizedGrid/Coord.hs view
@@ -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"
src/SizedGrid/Coord/Class.hs view
@@ -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]
src/SizedGrid/Coord/HardWrap.hs view
@@ -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 =
src/SizedGrid/Coord/Periodic.hs view
@@ -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 =
src/SizedGrid/Grid/Class.hs view
@@ -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) .
src/SizedGrid/Grid/Focused.hs view
@@ -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
src/SizedGrid/Grid/Grid.hs view
@@ -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"
tests/Main.hs view
@@ -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 =
tests/Test/Utils.hs view
@@ -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)