@@ -14,12 +14,17 @@ import Control.Monad ( guard )
14import Control.Monad.ST ( runST )
14import Control.Monad.ST ( runST )
16import Data.Constraint
16import Data.Constraint
17+#if __GLASGOW_HASKELL__ < 800
17import qualified Data.Vector.Storable as VS
20import qualified Data.Vector.Storable as VS
18import qualified Data.Vector.Storable.Mutable as VS ( write )
21import qualified Data.Vector.Storable.Mutable as VS ( write )
19import Data.Singletons
22import Data.Singletons
20import Data.Singletons.Prelude.List
23import Data.Singletons.Prelude.List
21import Data.Singletons.TypeLits
24import Data.Singletons.TypeLits
26+-- import Data.Type.Equality
23import Hedgehog
28import Hedgehog
24import qualified Hedgehog.Gen as Gen
29import qualified Hedgehog.Gen as Gen
25import Hedgehog.Internal.Source
30import Hedgehog.Internal.Source
@@ -27,15 +32,7 @@ import Hedgehog.Internal.Property ( failWith )
28import Grenade
33import Grenade
30−#if MIN_VERSION_base(4,11,0)
31−import GHC.TypeLits hiding (natVal)
33import GHC.TypeLits
35import GHC.TypeLits
35−#if MIN_VERSION_base(4,9,0)
36−import Data.Kind (Type)
39import GHC.TypeLits.Witnesses
36import GHC.TypeLits.Witnesses
40import Test.Hedgehog.Compat
37import Test.Hedgehog.Compat
41import Test.Hedgehog.TypeLits
38import Test.Hedgehog.TypeLits
@@ -46,7 +43,7 @@ import Numeric.LinearAlgebra ( flatten )
46import Numeric.LinearAlgebra.Static ( extract, norm_Inf )
43import Numeric.LinearAlgebra.Static ( extract, norm_Inf )
47import Unsafe.Coerce
44import Unsafe.Coerce
49−data SomeNetwork :: Type where
46+data SomeNetwork :: * where
50 SomeNetwork :: ( SingI shapes, SingI (Head shapes), SingI (Last shapes), Show (Network layers shapes) ) => Network layers shapes -> SomeNetwork
47 SomeNetwork :: ( SingI shapes, SingI (Head shapes), SingI (Last shapes), Show (Network layers shapes) ) => Network layers shapes -> SomeNetwork
52instance Show SomeNetwork where
49instance Show SomeNetwork where
@@ -77,9 +74,8 @@ genNetwork =
77 , pure (SomeNetwork (Elu :~> rest :: Network ( Elu ': layers ) ( h ': h ': hs )))
74 , pure (SomeNetwork (Elu :~> rest :: Network ( Elu ': layers ) ( h ': h ': hs )))
78 , pure (SomeNetwork (Softmax :~> rest :: Network ( Softmax ': layers ) ( h ': h ': hs )))
75 , pure (SomeNetwork (Softmax :~> rest :: Network ( Softmax ': layers ) ( h ': h ': hs )))
79 , do -- Reshape to two dimensions
76 , do -- Reshape to two dimensions
80− let divisors :: Integer -> [Integer]
81− divisors n = 1 : [x | x <- [2..(n-1)], n `rem` x == 0]
77+ let divisors n = 1 : [x | x <- [2..(n-1)], n `rem` x == 0]
82− let len = fromIntegral $ natVal l
78+ let len = natVal l
83 rs <- Gen.element $ divisors len
79 rs <- Gen.element $ divisors len
84 let cs = len `quot` rs
80 let cs = len `quot` rs
85 case ( someNatVal rs, someNatVal cs, someNatVal len ) of
81 case ( someNatVal rs, someNatVal cs, someNatVal len ) of
@@ -100,8 +96,8 @@ genNetwork =
100 , do -- Build a convolution layer with one filter output
96 , do -- Build a convolution layer with one filter output
101 -- Figure out some kernel sizes which work for this layer
97 -- Figure out some kernel sizes which work for this layer
102 -- There must be a better way than this...
98 -- There must be a better way than this...
103− let output_r = fromIntegral $ natVal r
99+ let output_r = natVal r
104− let output_c = fromIntegral $ natVal c
100+ let output_c = natVal c
106 let ok extent kernel = [stride | stride <- [ 1 .. extent ], (extent - kernel) `mod` stride == 0]
102 let ok extent kernel = [stride | stride <- [ 1 .. extent ], (extent - kernel) `mod` stride == 0]
@@ -140,8 +136,8 @@ genNetwork =
140 , do -- Build a convolution layer with one filter output
136 , do -- Build a convolution layer with one filter output
141 -- Figure out some kernel sizes which work for this layer
137 -- Figure out some kernel sizes which work for this layer
142 -- There must be a better way than this...
138 -- There must be a better way than this...
143− let output_r = fromIntegral $ natVal r
139+ let output_r = natVal r
144− let output_c = fromIntegral $ natVal c
140+ let output_c = natVal c
146 let ok extent kernel = [stride | stride <- [ 1 .. extent ], (extent - kernel) `mod` stride == 0]
142 let ok extent kernel = [stride | stride <- [ 1 .. extent ], (extent - kernel) `mod` stride == 0]
@@ -182,8 +178,8 @@ genNetwork =
182 pure (SomeNetwork (conv :~> rest :: Network ( Convolution channels 1 kernelRows kernelCols strideRows strideCols ': layers ) ( ('D3 inRows inCols channels) ': h ': hs )))
178 pure (SomeNetwork (conv :~> rest :: Network ( Convolution channels 1 kernelRows kernelCols strideRows strideCols ': layers ) ( ('D3 inRows inCols channels) ': h ': hs )))
183 _ -> Gen.discard -- Can't occur
179 _ -> Gen.discard -- Can't occur
184 , do -- Build a Pooling layer
180 , do -- Build a Pooling layer
185− let output_r = fromIntegral $ natVal r
181+ let output_r = natVal r
186− let output_c = fromIntegral $ natVal c
182+ let output_c = natVal c
188 let ok extent kernel = [stride | stride <- [ 1 .. extent ], (extent - kernel) `mod` stride == 0]
184 let ok extent kernel = [stride | stride <- [ 1 .. extent ], (extent - kernel) `mod` stride == 0]
@@ -219,8 +215,8 @@ genNetwork =
219 pure (SomeNetwork (Pooling :~> rest :: Network ( Pooling kernelRows kernelCols strideRows strideCols ': layers ) ( ('D2 inRows inCols) ': h ': hs )))
215 pure (SomeNetwork (Pooling :~> rest :: Network ( Pooling kernelRows kernelCols strideRows strideCols ': layers ) ( ('D2 inRows inCols) ': h ': hs )))
220 _ -> Gen.discard -- Can't occur
216 _ -> Gen.discard -- Can't occur
221 , do -- Build a Pad layer
217 , do -- Build a Pad layer
222− let output_r = fromIntegral $ natVal r
218+ let output_r = natVal r
223− let output_c = fromIntegral $ natVal c
219+ let output_c = natVal c
225 pad_left <- choose 0 (output_r - 1)
221 pad_left <- choose 0 (output_r - 1)
226 pad_right <- choose 0 (output_r - 1 - pad_left)
222 pad_right <- choose 0 (output_r - 1 - pad_left)
@@ -246,8 +242,8 @@ genNetwork =
246 pure (SomeNetwork (Pad :~> rest :: Network ( Pad padLeft padTop padRight padBottom ': layers ) ( ('D2 inputRows inputColumns) ': h ': hs )))
242 pure (SomeNetwork (Pad :~> rest :: Network ( Pad padLeft padTop padRight padBottom ': layers ) ( ('D2 inputRows inputColumns) ': h ': hs )))
247 _ -> Gen.discard -- Can't occur
243 _ -> Gen.discard -- Can't occur
248 , do -- Build a Crop layer
244 , do -- Build a Crop layer
249− let output_r = fromIntegral $ natVal r
245+ let output_r = natVal r
250− let output_c = fromIntegral $ natVal c
246+ let output_c = natVal c
252 crop_left <- choose 0 10
248 crop_left <- choose 0 10
253 crop_right <- choose 0 10
249 crop_right <- choose 0 10
@@ -279,9 +275,9 @@ genNetwork =
279 , do -- Build a convolution layer with one filter output
275 , do -- Build a convolution layer with one filter output
280 -- Figure out some kernel sizes which work for this layer
276 -- Figure out some kernel sizes which work for this layer
281 -- There must be a better way than this...
277 -- There must be a better way than this...
282− let output_r = fromIntegral $ natVal r
278+ let output_r = natVal r
283− let output_c = fromIntegral $ natVal c
279+ let output_c = natVal c
284− let output_f = fromIntegral $ natVal f
280+ let output_f = natVal f
286 let ok extent kernel = [stride | stride <- [ 1 .. extent ], (extent - kernel) `mod` stride == 0]
282 let ok extent kernel = [stride | stride <- [ 1 .. extent ], (extent - kernel) `mod` stride == 0]
@@ -322,9 +318,9 @@ genNetwork =
322 pure (SomeNetwork (conv :~> rest :: Network ( Convolution channels filters kernelRows kernelCols strideRows strideCols ': layers ) ( ('D3 inRows inCols channels) ': h ': hs )))
318 pure (SomeNetwork (conv :~> rest :: Network ( Convolution channels filters kernelRows kernelCols strideRows strideCols ': layers ) ( ('D3 inRows inCols channels) ': h ': hs )))
323 _ -> Gen.discard -- Can't occur
319 _ -> Gen.discard -- Can't occur
324 , do -- Build a Pooling layer
320 , do -- Build a Pooling layer
325− let output_r = fromIntegral $ natVal r
321+ let output_r = natVal r
326− let output_c = fromIntegral $ natVal c
322+ let output_c = natVal c
327− let output_f = fromIntegral $ natVal f
323+ let output_f = natVal f
329 let ok extent kernel = [stride | stride <- [ 1 .. extent ], (extent - kernel) `mod` stride == 0]
325 let ok extent kernel = [stride | stride <- [ 1 .. extent ], (extent - kernel) `mod` stride == 0]
@@ -363,9 +359,9 @@ genNetwork =
363 pure (SomeNetwork (Pooling :~> rest :: Network ( Pooling kernelRows kernelCols strideRows strideCols ': layers ) ( ('D3 inRows inCols filters) ': h ': hs )))
359 pure (SomeNetwork (Pooling :~> rest :: Network ( Pooling kernelRows kernelCols strideRows strideCols ': layers ) ( ('D3 inRows inCols filters) ': h ': hs )))
364 _ -> Gen.discard -- Can't occur
360 _ -> Gen.discard -- Can't occur
365 , do -- Build a Pad layer
361 , do -- Build a Pad layer
366− let output_r = fromIntegral $ natVal r
362+ let output_r = natVal r
367− let output_c = fromIntegral $ natVal c
363+ let output_c = natVal c
368− let output_f = fromIntegral $ natVal f
364+ let output_f = natVal f
370 pad_left <- choose 0 (output_r - 1)
366 pad_left <- choose 0 (output_r - 1)
371 pad_right <- choose 0 (output_r - 1 - pad_left)
367 pad_right <- choose 0 (output_r - 1 - pad_left)
@@ -393,9 +389,9 @@ genNetwork =
393 pure (SomeNetwork (Pad :~> rest :: Network ( Pad padLeft padTop padRight padBottom ': layers ) ( ('D3 inputRows inputColumns filters) ': h ': hs )))
389 pure (SomeNetwork (Pad :~> rest :: Network ( Pad padLeft padTop padRight padBottom ': layers ) ( ('D3 inputRows inputColumns filters) ': h ': hs )))
394 _ -> Gen.discard -- Can't occur
390 _ -> Gen.discard -- Can't occur
395 , do -- Build a Crop layer
391 , do -- Build a Crop layer
396− let output_r = fromIntegral $ natVal r
392+ let output_r = natVal r
397− let output_c = fromIntegral $ natVal c
393+ let output_c = natVal c
398− let output_f = fromIntegral $ natVal f
394+ let output_f = natVal f
400 crop_left <- choose 0 10
396 crop_left <- choose 0 10
401 crop_right <- choose 0 10
397 crop_right <- choose 0 10
@@ -448,7 +444,7 @@ oneUp =
448 D1Sing SNat ->
444 D1Sing SNat ->
449 let x = 0 :: S ( shape )
445 let x = 0 :: S ( shape )
450 in case x of
446 in case x of
451− ( S1D x' ) -> do
447+ ( S1D x' ) -> do
452 let ex = extract x'
448 let ex = extract x'
453 let len = VS.length ex
449 let len = VS.length ex
454 ix <- choose 0 (len - 1)
450 ix <- choose 0 (len - 1)
@@ -460,7 +456,7 @@ oneUp =
460 D2Sing SNat SNat ->
456 D2Sing SNat SNat ->
461 let x = 0 :: S ( shape )
457 let x = 0 :: S ( shape )
462 in case x of
458 in case x of
463− ( S2D x' ) -> do
459+ ( S2D x' ) -> do
464 let ex = flatten ( extract x' )
460 let ex = flatten ( extract x' )
465 let len = VS.length ex
461 let len = VS.length ex
466 ix <- choose 0 (len - 1)
462 ix <- choose 0 (len - 1)
@@ -472,7 +468,7 @@ oneUp =
472 D3Sing SNat SNat SNat ->
468 D3Sing SNat SNat SNat ->
473 let x = 0 :: S ( shape )
469 let x = 0 :: S ( shape )
474 in case x of
470 in case x of
475− ( S3D x' ) -> do
471+ ( S3D x' ) -> do
476 let ex = flatten ( extract x' )
472 let ex = flatten ( extract x' )
477 let len = VS.length ex
473 let len = VS.length ex
478 ix <- choose 0 (len - 1)
474 ix <- choose 0 (len - 1)