@@ -14,17 +14,12 @@ 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
20import qualified Data.Vector.Storable as VS
17import qualified Data.Vector.Storable as VS
21import qualified Data.Vector.Storable.Mutable as VS ( write )
18import qualified Data.Vector.Storable.Mutable as VS ( write )
22import Data.Singletons
19import Data.Singletons
23import Data.Singletons.Prelude.List
20import Data.Singletons.Prelude.List
24import Data.Singletons.TypeLits
21import Data.Singletons.TypeLits
26−-- import Data.Type.Equality
28import Hedgehog
23import Hedgehog
29import qualified Hedgehog.Gen as Gen
24import qualified Hedgehog.Gen as Gen
30import Hedgehog.Internal.Source
25import Hedgehog.Internal.Source
@@ -32,7 +27,15 @@ import Hedgehog.Internal.Property ( failWith )
33import Grenade
28import Grenade
30+#if MIN_VERSION_base(4,11,0)
31+import GHC.TypeLits hiding (natVal)
35import GHC.TypeLits
33import GHC.TypeLits
35+#if MIN_VERSION_base(4,9,0)
36+import Data.Kind (Type)
36import GHC.TypeLits.Witnesses
39import GHC.TypeLits.Witnesses
37import Test.Hedgehog.Compat
40import Test.Hedgehog.Compat
38import Test.Hedgehog.TypeLits
41import Test.Hedgehog.TypeLits
@@ -43,7 +46,7 @@ import Numeric.LinearAlgebra ( flatten )
43import Numeric.LinearAlgebra.Static ( extract, norm_Inf )
46import Numeric.LinearAlgebra.Static ( extract, norm_Inf )
44import Unsafe.Coerce
47import Unsafe.Coerce
46−data SomeNetwork :: * where
49+data SomeNetwork :: Type where
47 SomeNetwork :: ( SingI shapes, SingI (Head shapes), SingI (Last shapes), Show (Network layers shapes) ) => Network layers shapes -> SomeNetwork
50 SomeNetwork :: ( SingI shapes, SingI (Head shapes), SingI (Last shapes), Show (Network layers shapes) ) => Network layers shapes -> SomeNetwork
49instance Show SomeNetwork where
52instance Show SomeNetwork where
@@ -53,7 +56,7 @@ instance Show SomeNetwork where
54-- This is slightly insane for a few reasons. Everything must be wrapped up
57-- This is slightly insane for a few reasons. Everything must be wrapped up
55-- in a SomeNetwork.
58-- in a SomeNetwork.
56−genNetwork :: Monad m => Gen.Gen m SomeNetwork
59+genNetwork :: Gen SomeNetwork
57genNetwork =
60genNetwork =
58 Gen.recursive Gen.choice [
61 Gen.recursive Gen.choice [
59 do SomeSing ( r :: Sing final ) <- genShape
62 do SomeSing ( r :: Sing final ) <- genShape
@@ -62,7 +65,7 @@ genNetwork =
63 do SomeNetwork ( rest :: Network layers shapes ) <- genNetwork
66 do SomeNetwork ( rest :: Network layers shapes ) <- genNetwork
64 case ( sing :: Sing shapes ) of
67 case ( sing :: Sing shapes ) of
65− SNil -> Gen.discard
68+ SNil -> Gen.discard -- Can't occur
66 SCons ( h :: Sing h ) ( _ :: Sing hs ) ->
69 SCons ( h :: Sing h ) ( _ :: Sing hs ) ->
67 withSingI h $
70 withSingI h $
@@ -74,8 +77,9 @@ genNetwork =
74 , pure (SomeNetwork (Elu :~> rest :: Network ( Elu ': layers ) ( h ': h ': hs )))
77 , pure (SomeNetwork (Elu :~> rest :: Network ( Elu ': layers ) ( h ': h ': hs )))
75 , pure (SomeNetwork (Softmax :~> rest :: Network ( Softmax ': layers ) ( h ': h ': hs )))
78 , pure (SomeNetwork (Softmax :~> rest :: Network ( Softmax ': layers ) ( h ': h ': hs )))
76 , do -- Reshape to two dimensions
79 , do -- Reshape to two dimensions
80+ let divisors :: Integer -> [Integer]
77− let divisors n = 1 : [x | x <- [2..(n-1)], n `rem` x == 0]
81+ divisors n = 1 : [x | x <- [2..(n-1)], n `rem` x == 0]
78− let len = natVal l
82+ let len = fromIntegral $ natVal l
79 rs <- Gen.element $ divisors len
83 rs <- Gen.element $ divisors len
80 let cs = len `quot` rs
84 let cs = len `quot` rs
81 case ( someNatVal rs, someNatVal cs, someNatVal len ) of
85 case ( someNatVal rs, someNatVal cs, someNatVal len ) of
@@ -96,8 +100,8 @@ genNetwork =
96 , do -- Build a convolution layer with one filter output
100 , do -- Build a convolution layer with one filter output
97 -- Figure out some kernel sizes which work for this layer
101 -- Figure out some kernel sizes which work for this layer
98 -- There must be a better way than this...
102 -- There must be a better way than this...
99− let output_r = natVal r
103+ let output_r = fromIntegral $ natVal r
100− let output_c = natVal c
104+ let output_c = fromIntegral $ natVal c
102 let ok extent kernel = [stride | stride <- [ 1 .. extent ], (extent - kernel) `mod` stride == 0]
106 let ok extent kernel = [stride | stride <- [ 1 .. extent ], (extent - kernel) `mod` stride == 0]
@@ -136,8 +140,8 @@ genNetwork =
136 , do -- Build a convolution layer with one filter output
140 , do -- Build a convolution layer with one filter output
137 -- Figure out some kernel sizes which work for this layer
141 -- Figure out some kernel sizes which work for this layer
138 -- There must be a better way than this...
142 -- There must be a better way than this...
139− let output_r = natVal r
143+ let output_r = fromIntegral $ natVal r
140− let output_c = natVal c
144+ let output_c = fromIntegral $ natVal c
142 let ok extent kernel = [stride | stride <- [ 1 .. extent ], (extent - kernel) `mod` stride == 0]
146 let ok extent kernel = [stride | stride <- [ 1 .. extent ], (extent - kernel) `mod` stride == 0]
@@ -178,8 +182,8 @@ genNetwork =
178 pure (SomeNetwork (conv :~> rest :: Network ( Convolution channels 1 kernelRows kernelCols strideRows strideCols ': layers ) ( ('D3 inRows inCols channels) ': h ': hs )))
182 pure (SomeNetwork (conv :~> rest :: Network ( Convolution channels 1 kernelRows kernelCols strideRows strideCols ': layers ) ( ('D3 inRows inCols channels) ': h ': hs )))
179 _ -> Gen.discard -- Can't occur
183 _ -> Gen.discard -- Can't occur
180 , do -- Build a Pooling layer
184 , do -- Build a Pooling layer
181− let output_r = natVal r
185+ let output_r = fromIntegral $ natVal r
182− let output_c = natVal c
186+ let output_c = fromIntegral $ natVal c
184 let ok extent kernel = [stride | stride <- [ 1 .. extent ], (extent - kernel) `mod` stride == 0]
188 let ok extent kernel = [stride | stride <- [ 1 .. extent ], (extent - kernel) `mod` stride == 0]
@@ -214,25 +218,219 @@ genNetwork =
214 (Dict, Dict, Dict, Dict) ->
218 (Dict, Dict, Dict, Dict) ->
215 pure (SomeNetwork (Pooling :~> rest :: Network ( Pooling kernelRows kernelCols strideRows strideCols ': layers ) ( ('D2 inRows inCols) ': h ': hs )))
219 pure (SomeNetwork (Pooling :~> rest :: Network ( Pooling kernelRows kernelCols strideRows strideCols ': layers ) ( ('D2 inRows inCols) ': h ': hs )))
216 _ -> Gen.discard -- Can't occur
220 _ -> Gen.discard -- Can't occur
221+ , do -- Build a Pad layer
222+ let output_r = fromIntegral $ natVal r
223+ let output_c = fromIntegral $ natVal c
225+ pad_left <- choose 0 (output_r - 1)
226+ pad_right <- choose 0 (output_r - 1 - pad_left)
227+ pad_top <- choose 0 (output_c - 1)
228+ pad_bottom <- choose 0 (output_c - 1 - pad_top)
230+ let input_r = output_r - pad_top - pad_bottom
231+ let input_c = output_c - pad_left - pad_right
236+ -- Remake types for input
237+ case ( someNatVal input_r, someNatVal input_c, someNatVal output_r, someNatVal output_c, someNatVal pad_left, someNatVal pad_right, someNatVal pad_top, someNatVal pad_bottom ) of
238+ ( Just (SomeNat (_ :: Proxy inputRows)), Just (SomeNat (_ :: Proxy inputColumns)),
239+ Just (SomeNat (_ :: Proxy outputRows)), Just (SomeNat (_ :: Proxy outputColumns)),
240+ Just (SomeNat (_ :: Proxy padLeft)), Just (SomeNat (_ :: Proxy padRight)),
241+ Just (SomeNat (_ :: Proxy padTop)), Just (SomeNat (_ :: Proxy padBottom))) ->
242+ case ( (unsafeCoerce (Dict :: Dict ()) :: Dict ( ( 'D2 outputRows outputColumns) ~ h ))
243+ , (unsafeCoerce (Dict :: Dict ()) :: Dict ( (inputRows + padTop + padBottom) ~ outputRows) )
244+ , (unsafeCoerce (Dict :: Dict ()) :: Dict ( (inputColumns + padLeft + padRight) ~ outputColumns ))) of
245+ ( Dict, Dict, Dict ) ->
246+ pure (SomeNetwork (Pad :~> rest :: Network ( Pad padLeft padTop padRight padBottom ': layers ) ( ('D2 inputRows inputColumns) ': h ': hs )))
247+ _ -> Gen.discard -- Can't occur
248+ , do -- Build a Crop layer
249+ let output_r = fromIntegral $ natVal r
250+ let output_c = fromIntegral $ natVal c
252+ crop_left <- choose 0 10
253+ crop_right <- choose 0 10
254+ crop_top <- choose 0 10
255+ crop_bottom <- choose 0 10
257+ let input_r = output_r + crop_top + crop_bottom
258+ let input_c = output_c + crop_left + crop_right
260+ -- Remake types for input
261+ case ( someNatVal input_r, someNatVal input_c, someNatVal output_r, someNatVal output_c, someNatVal crop_left, someNatVal crop_right, someNatVal crop_top, someNatVal crop_bottom ) of
262+ ( Just (SomeNat (_ :: Proxy inputRows)), Just (SomeNat (_ :: Proxy inputColumns)),
263+ Just (SomeNat (_ :: Proxy outputRows)), Just (SomeNat (_ :: Proxy outputColumns)),
264+ Just (SomeNat (_ :: Proxy cropLeft)), Just (SomeNat (_ :: Proxy cropRight)),
265+ Just (SomeNat (_ :: Proxy cropTop)), Just (SomeNat (_ :: Proxy cropBottom))) ->
266+ case ( (unsafeCoerce (Dict :: Dict ()) :: Dict ( ( 'D2 outputRows outputColumns) ~ h ))
267+ , (unsafeCoerce (Dict :: Dict ()) :: Dict ( (outputRows + cropTop + cropBottom) ~ inputRows ) )
268+ , (unsafeCoerce (Dict :: Dict ()) :: Dict ( (outputColumns + cropLeft + cropRight) ~ inputColumns ))) of
269+ (Dict, Dict, Dict) ->
270+ pure (SomeNetwork (Crop :~> rest :: Network ( Crop cropLeft cropTop cropRight cropBottom ': layers ) ( ('D2 inputRows inputColumns) ': h ': hs )))
271+ _ -> Gen.discard -- Can't occur
218− D3Sing SNat SNat SNat ->
273+ D3Sing r@SNat c@SNat f@SNat ->
219 Gen.choice [
274 Gen.choice [
220 pure (SomeNetwork (Tanh :~> rest :: Network ( Tanh ': layers ) ( h ': h ': hs )))
275 pure (SomeNetwork (Tanh :~> rest :: Network ( Tanh ': layers ) ( h ': h ': hs )))
221 , pure (SomeNetwork (Logit :~> rest :: Network ( Logit ': layers ) ( h ': h ': hs )))
276 , pure (SomeNetwork (Logit :~> rest :: Network ( Logit ': layers ) ( h ': h ': hs )))
222 , pure (SomeNetwork (Relu :~> rest :: Network ( Relu ': layers ) ( h ': h ': hs )))
277 , pure (SomeNetwork (Relu :~> rest :: Network ( Relu ': layers ) ( h ': h ': hs )))
223 , pure (SomeNetwork (Elu :~> rest :: Network ( Elu ': layers ) ( h ': h ': hs )))
278 , pure (SomeNetwork (Elu :~> rest :: Network ( Elu ': layers ) ( h ': h ': hs )))
279+ , do -- Build a convolution layer with one filter output
280+ -- Figure out some kernel sizes which work for this layer
281+ -- There must be a better way than this...
282+ let output_r = fromIntegral $ natVal r
283+ let output_c = fromIntegral $ natVal c
284+ let output_f = fromIntegral $ natVal f
286+ let ok extent kernel = [stride | stride <- [ 1 .. extent ], (extent - kernel) `mod` stride == 0]
288+ -- Get some kernels which will fit
289+ kernel_r <- choose 1 output_r
290+ kernel_c <- choose 1 output_c
291+ channels <- choose 1 10
293+ -- Build up some strides which also fit
294+ stride_r <- Gen.element $ ok output_r kernel_r
295+ stride_c <- Gen.element $ ok output_c kernel_c
297+ -- Determine the input size
298+ let input_r = (output_r - 1) * stride_r + kernel_r
299+ let input_c = (output_c - 1) * stride_c + kernel_c
301+ guard (input_r < 100)
302+ guard (input_c < 100)
304+ -- Remake types for input
305+ case ( someNatVal channels, someNatVal output_f, someNatVal input_r, someNatVal input_c, someNatVal output_r, someNatVal output_c, someNatVal kernel_r, someNatVal kernel_c, someNatVal stride_r, someNatVal stride_c ) of
306+ ( Just (SomeNat (chan :: Proxy channels)), Just (SomeNat (_ :: Proxy filters)),
307+ Just (SomeNat (pinr :: Proxy inRows)), Just (SomeNat (_ :: Proxy inCols)),
308+ Just (SomeNat (_ :: Proxy outRows)), Just (SomeNat (_ :: Proxy outCols)),
309+ Just (SomeNat (pkr :: Proxy kernelRows)), Just (SomeNat (pkc :: Proxy kernelCols)),
310+ Just (SomeNat (_ :: Proxy strideRows)), Just (SomeNat (_ :: Proxy strideCols))) ->
311+ let p1 = natDict pkr
314+ in case ( p1 %* p2 %* p3
315+ , natDict pinr %* natDict chan
316+ -- Fake it till you make it.
317+ , (unsafeCoerce (Dict :: Dict ()) :: Dict ( ( 'D3 outRows outCols filters) ~ h ))
318+ , (unsafeCoerce (Dict :: Dict ()) :: Dict (((outRows - 1) * strideRows) ~ (inRows - kernelRows)))
319+ , (unsafeCoerce (Dict :: Dict ()) :: Dict (((outCols - 1) * strideCols) ~ (inCols - kernelCols)))) of
320+ (Dict, Dict, Dict, Dict, Dict) -> do
321+ conv <- genConvolution
322+ 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
324+ , do -- Build a Pooling layer
325+ let output_r = fromIntegral $ natVal r
326+ let output_c = fromIntegral $ natVal c
327+ let output_f = fromIntegral $ natVal f
329+ let ok extent kernel = [stride | stride <- [ 1 .. extent ], (extent - kernel) `mod` stride == 0]
331+ -- Get some kernels which will fit
332+ kernel_r <- choose 1 output_r
333+ kernel_c <- choose 1 output_c
335+ -- Build up some strides which also fit
336+ stride_r <- Gen.element $ ok output_r kernel_r
337+ stride_c <- Gen.element $ ok output_c kernel_c
339+ -- Determine the input size
340+ let input_r = (output_r - 1) * stride_r + kernel_r
341+ let input_c = (output_c - 1) * stride_c + kernel_c
343+ guard (input_r < 100)
344+ guard (input_c < 100)
346+ -- Remake types for input
347+ case ( someNatVal output_f, someNatVal input_r, someNatVal input_c, someNatVal output_r, someNatVal output_c, someNatVal kernel_r, someNatVal kernel_c, someNatVal stride_r, someNatVal stride_c ) of
348+ ( Just (SomeNat (chan :: Proxy filters)),
349+ Just (SomeNat (pinr :: Proxy inRows)), Just (SomeNat (_ :: Proxy inCols)),
350+ Just (SomeNat (_ :: Proxy outRows)), Just (SomeNat (_ :: Proxy outCols)),
351+ Just (SomeNat (pkr :: Proxy kernelRows)), Just (SomeNat (pkc :: Proxy kernelCols)),
352+ Just (SomeNat (_ :: Proxy strideRows)), Just (SomeNat (_ :: Proxy strideCols))) ->
353+ let p1 = natDict pkr
356+ in case ( p1 %* p2 %* p3
357+ , natDict pinr %* natDict chan
358+ -- Fake it till you make it.
359+ , (unsafeCoerce (Dict :: Dict ()) :: Dict ( ( 'D3 outRows outCols filters) ~ h ))
360+ , (unsafeCoerce (Dict :: Dict ()) :: Dict (((outRows - 1) * strideRows) ~ (inRows - kernelRows)))
361+ , (unsafeCoerce (Dict :: Dict ()) :: Dict (((outCols - 1) * strideCols) ~ (inCols - kernelCols)))) of
362+ (Dict, Dict, Dict, Dict, Dict) ->
363+ pure (SomeNetwork (Pooling :~> rest :: Network ( Pooling kernelRows kernelCols strideRows strideCols ': layers ) ( ('D3 inRows inCols filters) ': h ': hs )))
364+ _ -> Gen.discard -- Can't occur
365+ , do -- Build a Pad layer
366+ let output_r = fromIntegral $ natVal r
367+ let output_c = fromIntegral $ natVal c
368+ let output_f = fromIntegral $ natVal f
370+ pad_left <- choose 0 (output_r - 1)
371+ pad_right <- choose 0 (output_r - 1 - pad_left)
372+ pad_top <- choose 0 (output_c - 1)
373+ pad_bottom <- choose 0 (output_c - 1 - pad_top)
375+ let input_r = output_r - pad_top - pad_bottom
376+ let input_c = output_c - pad_left - pad_right
381+ -- Remake types for input
382+ case ( someNatVal output_f, someNatVal input_r, someNatVal input_c, someNatVal output_r, someNatVal output_c, someNatVal pad_left, someNatVal pad_right, someNatVal pad_top, someNatVal pad_bottom ) of
383+ ( Just (SomeNat (chan :: Proxy filters)),
384+ Just (SomeNat (pinr :: Proxy inputRows)), Just (SomeNat (_ :: Proxy inputColumns)),
385+ Just (SomeNat (_ :: Proxy outputRows)), Just (SomeNat (_ :: Proxy outputColumns)),
386+ Just (SomeNat (_ :: Proxy padLeft)), Just (SomeNat (_ :: Proxy padRight)),
387+ Just (SomeNat (_ :: Proxy padTop)), Just (SomeNat (_ :: Proxy padBottom))) ->
388+ case ( natDict pinr %* natDict chan
389+ , (unsafeCoerce (Dict :: Dict ()) :: Dict ( ( 'D3 outputRows outputColumns filters) ~ h ))
390+ , (unsafeCoerce (Dict :: Dict ()) :: Dict ( (inputRows + padTop + padBottom) ~ outputRows) )
391+ , (unsafeCoerce (Dict :: Dict ()) :: Dict ( (inputColumns + padLeft + padRight) ~ outputColumns ))) of
392+ (Dict, Dict, Dict, Dict) ->
393+ pure (SomeNetwork (Pad :~> rest :: Network ( Pad padLeft padTop padRight padBottom ': layers ) ( ('D3 inputRows inputColumns filters) ': h ': hs )))
394+ _ -> Gen.discard -- Can't occur
395+ , do -- Build a Crop layer
396+ let output_r = fromIntegral $ natVal r
397+ let output_c = fromIntegral $ natVal c
398+ let output_f = fromIntegral $ natVal f
400+ crop_left <- choose 0 10
401+ crop_right <- choose 0 10
402+ crop_top <- choose 0 10
403+ crop_bottom <- choose 0 10
405+ let input_r = output_r + crop_top + crop_bottom
406+ let input_c = output_c + crop_left + crop_right
408+ -- Remake types for input
409+ case ( someNatVal output_f, someNatVal input_r, someNatVal input_c, someNatVal output_r, someNatVal output_c, someNatVal crop_left, someNatVal crop_right, someNatVal crop_top, someNatVal crop_bottom ) of
410+ ( Just (SomeNat (chan :: Proxy filters)),
411+ Just (SomeNat (pinr :: Proxy inputRows)), Just (SomeNat (_ :: Proxy inputColumns)),
412+ Just (SomeNat (_ :: Proxy outputRows)), Just (SomeNat (_ :: Proxy outputColumns)),
413+ Just (SomeNat (_ :: Proxy cropLeft)), Just (SomeNat (_ :: Proxy cropRight)),
414+ Just (SomeNat (_ :: Proxy cropTop)), Just (SomeNat (_ :: Proxy cropBottom))) ->
415+ case ( natDict pinr %* natDict chan
416+ , (unsafeCoerce (Dict :: Dict ()) :: Dict ( ( 'D3 outputRows outputColumns filters) ~ h ))
417+ , (unsafeCoerce (Dict :: Dict ()) :: Dict ( (outputRows + cropTop + cropBottom) ~ inputRows ) )
418+ , (unsafeCoerce (Dict :: Dict ()) :: Dict ( (outputColumns + cropLeft + cropRight) ~ inputColumns ))) of
419+ (Dict, Dict, Dict, Dict) ->
420+ pure (SomeNetwork (Crop :~> rest :: Network ( Crop cropLeft cropTop cropRight cropBottom ': layers ) ( ('D3 inputRows inputColumns filters) ': h ': hs )))
421+ _ -> Gen.discard -- Can't occur
227-- | Test a partial derivative numerically for a random network and input
425-- | Test a partial derivative numerically for a random network and input
229-- This is the most important test.
427-- This is the most important test.
230prop_auto_diff :: Property
428prop_auto_diff :: Property
231−prop_auto_diff = withTests 10000 . property $ do
429+prop_auto_diff = withDiscards 1000 . withTests 10000 . property $ do
232 SomeNetwork (network :: Network layers shapes) <- forAll genNetwork
430 SomeNetwork (network :: Network layers shapes) <- forAll genNetwork
233− (input :: S (Head shapes)) <- forAllRender nice genOfShape
431+ (input :: S (Head shapes)) <- forAllWith nice genOfShape
234− (target :: S (Last shapes)) <- forAllRender nice oneUp
432+ (target :: S (Last shapes)) <- forAllWith nice oneUp
235− (tested :: S (Head shapes)) <- forAllRender nice oneUp
433+ (tested :: S (Head shapes)) <- forAllWith nice oneUp
237 let (!tapes, !output) = runNetwork network input
435 let (!tapes, !output) = runNetwork network input
238 let (_, !backgrad) = runGradient network tapes target
436 let (_, !backgrad) = runGradient network tapes target
@@ -244,13 +442,13 @@ prop_auto_diff = withTests 10000 . property $ do
244 result ~~~ expected
442 result ~~~ expected
246-- Make a shape where all are 0 except for 1 value, which is 1.
444-- Make a shape where all are 0 except for 1 value, which is 1.
247−oneUp :: forall shape m. ( Monad m, SingI shape ) => Gen.Gen m (S shape)
445+oneUp :: forall shape. ( SingI shape ) => Gen (S shape)
249 case ( sing :: Sing shape ) of
447 case ( sing :: Sing shape ) of
250 D1Sing SNat ->
448 D1Sing SNat ->
251 let x = 0 :: S ( shape )
449 let x = 0 :: S ( shape )
252 in case x of
450 in case x of
253− ( S1D x' ) -> do
451+ ( S1D x' ) -> do
254 let ex = extract x'
452 let ex = extract x'
255 let len = VS.length ex
453 let len = VS.length ex
256 ix <- choose 0 (len - 1)
454 ix <- choose 0 (len - 1)
@@ -262,7 +460,7 @@ oneUp =
262 D2Sing SNat SNat ->
460 D2Sing SNat SNat ->
263 let x = 0 :: S ( shape )
461 let x = 0 :: S ( shape )
264 in case x of
462 in case x of
265− ( S2D x' ) -> do
463+ ( S2D x' ) -> do
266 let ex = flatten ( extract x' )
464 let ex = flatten ( extract x' )
267 let len = VS.length ex
465 let len = VS.length ex
268 ix <- choose 0 (len - 1)
466 ix <- choose 0 (len - 1)
@@ -274,7 +472,7 @@ oneUp =
274 D3Sing SNat SNat SNat ->
472 D3Sing SNat SNat SNat ->
275 let x = 0 :: S ( shape )
473 let x = 0 :: S ( shape )
276 in case x of
474 in case x of
277− ( S3D x' ) -> do
475+ ( S3D x' ) -> do
278 let ex = flatten ( extract x' )
476 let ex = flatten ( extract x' )
279 let len = VS.length ex
477 let len = VS.length ex
280 ix <- choose 0 (len - 1)
478 ix <- choose 0 (len - 1)
@@ -288,9 +486,9 @@ maxVal ( S1D x ) = norm_Inf x
288maxVal ( S2D x ) = norm_Inf x
486maxVal ( S2D x ) = norm_Inf x
289maxVal ( S3D x ) = norm_Inf x
487maxVal ( S3D x ) = norm_Inf x
291−(~~~) :: (Monad m, HasCallStack) => Double -> Double -> Test m ()
489+(~~~) :: (Monad m, HasCallStack) => Double -> Double -> PropertyT m ()
292(~~~) x y =
490(~~~) x y =
293− if abs (x - y) < 1e-5 then
491+ if abs (x - y) < 2e-5 then
296 withFrozenCallStack $
494 withFrozenCallStack $