@@ -1,504 +0,0 @@
1−{-# LANGUAGE CPP #-}
2−{-# LANGUAGE BangPatterns #-}
3−{-# LANGUAGE RankNTypes #-}
4−{-# LANGUAGE DataKinds #-}
5−{-# LANGUAGE ScopedTypeVariables #-}
6−{-# LANGUAGE PolyKinds #-}
7−{-# LANGUAGE GADTs #-}
8−{-# LANGUAGE TypeOperators #-}
9−{-# LANGUAGE TemplateHaskell #-}
10−{-# LANGUAGE FlexibleContexts #-}
11−module Test.Grenade.Network where
12−
13−import Control.Monad ( guard )
14−import Control.Monad.ST ( runST )
15−
16−import Data.Constraint
17−import qualified Data.Vector.Storable as VS
18−import qualified Data.Vector.Storable.Mutable as VS ( write )
19−import Data.Singletons
20−import Data.Singletons.Prelude.List
21−import Data.Singletons.TypeLits
22−
23−import Hedgehog
24−import qualified Hedgehog.Gen as Gen
25−import Hedgehog.Internal.Source
26−import Hedgehog.Internal.Property ( failWith )
27−
28−import Grenade
29−
30−#if MIN_VERSION_base(4,11,0)
31−import GHC.TypeLits hiding (natVal)
32−#else
33−import GHC.TypeLits
34−#endif
35−#if MIN_VERSION_base(4,9,0)
36−import Data.Kind (Type)
37−#endif
38−
39−import GHC.TypeLits.Witnesses
40−import Test.Hedgehog.Compat
41−import Test.Hedgehog.TypeLits
42−import Test.Hedgehog.Hmatrix
43−import Test.Grenade.Layers.Convolution
44−
45−import Numeric.LinearAlgebra ( flatten )
46−import Numeric.LinearAlgebra.Static ( extract, norm_Inf )
47−import Unsafe.Coerce
48−
49−data SomeNetwork :: Type where
50− SomeNetwork :: ( SingI shapes, SingI (Head shapes), SingI (Last shapes), Show (Network layers shapes) ) => Network layers shapes -> SomeNetwork
51−
52−instance Show SomeNetwork where
53− show (SomeNetwork net) = show net
54−
55−-- | Generate a random network of a random type
56−--
57−-- This is slightly insane for a few reasons. Everything must be wrapped up
58−-- in a SomeNetwork.
59−genNetwork :: Gen SomeNetwork
60−genNetwork =
61− Gen.recursive Gen.choice [
62− do SomeSing ( r :: Sing final ) <- genShape
63− withSingI r $
64− pure (SomeNetwork (NNil :: Network '[] '[ final ] ))
65− ] [
66− do SomeNetwork ( rest :: Network layers shapes ) <- genNetwork
67− case ( sing :: Sing shapes ) of
68− SNil -> Gen.discard -- Can't occur
69− SCons ( h :: Sing h ) ( _ :: Sing hs ) ->
70− withSingI h $
71− case h of
72− D1Sing l@SNat ->
73− Gen.choice [
74− pure (SomeNetwork (Tanh :~> rest :: Network ( Tanh ': layers ) ( h ': h ': hs )))
75− , pure (SomeNetwork (Logit :~> rest :: Network ( Logit ': layers ) ( h ': h ': hs )))
76− , pure (SomeNetwork (Relu :~> rest :: Network ( Relu ': layers ) ( h ': h ': hs )))
77− , pure (SomeNetwork (Elu :~> rest :: Network ( Elu ': layers ) ( h ': h ': hs )))
78− , pure (SomeNetwork (Softmax :~> rest :: Network ( Softmax ': layers ) ( h ': h ': hs )))
79− , do -- Reshape to two dimensions
80− let divisors :: Integer -> [Integer]
81− divisors n = 1 : [x | x <- [2..(n-1)], n `rem` x == 0]
82− let len = fromIntegral $ natVal l
83− rs <- Gen.element $ divisors len
84− let cs = len `quot` rs
85− case ( someNatVal rs, someNatVal cs, someNatVal len ) of
86− ( Just (SomeNat (rs' :: Proxy inRows)), Just (SomeNat (cs' :: Proxy inCols)), Just (SomeNat (_ :: Proxy outLen ) )) ->
87− let p1 = natDict rs'
88− p2 = natDict cs'
89− in case ( p1 %* p2, unsafeCoerce (Dict :: Dict ()) :: Dict ((inRows * inCols) ~ outLen), unsafeCoerce (Dict :: Dict ()) :: Dict (( 'D1 outLen ) ~ h )) of
90− ( Dict, Dict, Dict ) ->
91− pure (SomeNetwork (Reshape :~> rest :: Network ( Reshape ': layers ) ( ('D2 inRows inCols) ': h ': hs )))
92− _ -> Gen.discard -- Doesn't occur
93− ]
94− D2Sing r@SNat c@SNat ->
95− Gen.choice [
96− pure (SomeNetwork (Tanh :~> rest :: Network ( Tanh ': layers ) ( h ': h ': hs )))
97− , pure (SomeNetwork (Logit :~> rest :: Network ( Logit ': layers ) ( h ': h ': hs )))
98− , pure (SomeNetwork (Relu :~> rest :: Network ( Relu ': layers ) ( h ': h ': hs )))
99− , pure (SomeNetwork (Elu :~> rest :: Network ( Elu ': layers ) ( h ': h ': hs )))
100− , do -- Build a convolution layer with one filter output
101− -- Figure out some kernel sizes which work for this layer
102− -- There must be a better way than this...
103− let output_r = fromIntegral $ natVal r
104− let output_c = fromIntegral $ natVal c
105−
106− let ok extent kernel = [stride | stride <- [ 1 .. extent ], (extent - kernel) `mod` stride == 0]
107−
108− -- Get some kernels which will fit
109− kernel_r <- choose 1 output_r
110− kernel_c <- choose 1 output_c
111−
112− -- Build up some strides which also fit
113− stride_r <- Gen.element $ ok output_r kernel_r
114− stride_c <- Gen.element $ ok output_c kernel_c
115−
116− -- Determine the input size
117− let input_r = (output_r - 1) * stride_r + kernel_r
118− let input_c = (output_c - 1) * stride_c + kernel_c
119−
120− guard (input_r < 100)
121− guard (input_c < 100)
122−
123− -- Remake types for input
124− case ( 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
125− ( Just (SomeNat (_ :: Proxy inRows)), Just (SomeNat (_ :: Proxy inCols)),
126− Just (SomeNat (_ :: Proxy outRows)), Just (SomeNat (_ :: Proxy outCols)),
127− Just (SomeNat (pkr :: Proxy kernelRows)), Just (SomeNat (pkc :: Proxy kernelCols)),
128− Just (SomeNat (_ :: Proxy strideRows)), Just (SomeNat (_ :: Proxy strideCols))) ->
129− let p1 = natDict pkr
130− p2 = natDict pkc
131− in case ( p1 %* p2
132− -- Fake it till you make it.
133− , (unsafeCoerce (Dict :: Dict ()) :: Dict ( ( 'D2 outRows outCols ) ~ h ))
134− , (unsafeCoerce (Dict :: Dict ()) :: Dict (((outRows - 1) * strideRows) ~ (inRows - kernelRows)))
135− , (unsafeCoerce (Dict :: Dict ()) :: Dict (((outCols - 1) * strideCols) ~ (inCols - kernelCols)))) of
136− (Dict, Dict, Dict, Dict) -> do
137− conv <- genConvolution
138− pure (SomeNetwork (conv :~> rest :: Network ( Convolution 1 1 kernelRows kernelCols strideRows strideCols ': layers ) ( ('D2 inRows inCols) ': h ': hs )))
139− _ -> Gen.discard -- Can't occur
140− , do -- Build a convolution layer with one filter output
141− -- Figure out some kernel sizes which work for this layer
142− -- There must be a better way than this...
143− let output_r = fromIntegral $ natVal r
144− let output_c = fromIntegral $ natVal c
145−
146− let ok extent kernel = [stride | stride <- [ 1 .. extent ], (extent - kernel) `mod` stride == 0]
147−
148− -- Get some kernels which will fit
149− kernel_r <- choose 1 output_r
150− kernel_c <- choose 1 output_c
151− channels <- choose 1 10
152−
153− -- Build up some strides which also fit
154− stride_r <- Gen.element $ ok output_r kernel_r
155− stride_c <- Gen.element $ ok output_c kernel_c
156−
157− -- Determine the input size
158− let input_r = (output_r - 1) * stride_r + kernel_r
159− let input_c = (output_c - 1) * stride_c + kernel_c
160−
161− guard (input_r < 100)
162− guard (input_c < 100)
163−
164− -- Remake types for input
165− case ( someNatVal channels, 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
166− ( Just (SomeNat (chan :: Proxy channels)),
167− Just (SomeNat (pinr :: Proxy inRows)), Just (SomeNat (_ :: Proxy inCols)),
168− Just (SomeNat (_ :: Proxy outRows)), Just (SomeNat (_ :: Proxy outCols)),
169− Just (SomeNat (pkr :: Proxy kernelRows)), Just (SomeNat (pkc :: Proxy kernelCols)),
170− Just (SomeNat (_ :: Proxy strideRows)), Just (SomeNat (_ :: Proxy strideCols))) ->
171− let p1 = natDict pkr
172− p2 = natDict pkc
173− p3 = natDict chan
174− in case ( p1 %* p2 %* p3
175− , natDict pinr %* natDict chan
176− -- Fake it till you make it.
177− , (unsafeCoerce (Dict :: Dict ()) :: Dict ( ( 'D2 outRows outCols ) ~ h ))
178− , (unsafeCoerce (Dict :: Dict ()) :: Dict (((outRows - 1) * strideRows) ~ (inRows - kernelRows)))
179− , (unsafeCoerce (Dict :: Dict ()) :: Dict (((outCols - 1) * strideCols) ~ (inCols - kernelCols)))) of
180− (Dict, Dict, Dict, Dict, Dict) -> do
181− conv <- genConvolution
182− 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
184− , do -- Build a Pooling layer
185− let output_r = fromIntegral $ natVal r
186− let output_c = fromIntegral $ natVal c
187−
188− let ok extent kernel = [stride | stride <- [ 1 .. extent ], (extent - kernel) `mod` stride == 0]
189−
190− -- Get some kernels which will fit
191− kernel_r <- choose 1 output_r
192− kernel_c <- choose 1 output_c
193−
194− -- Build up some strides which also fit
195− stride_r <- Gen.element $ ok output_r kernel_r
196− stride_c <- Gen.element $ ok output_c kernel_c
197−
198− -- Determine the input size
199− let input_r = (output_r - 1) * stride_r + kernel_r
200− let input_c = (output_c - 1) * stride_c + kernel_c
201−
202− guard (input_r < 100)
203− guard (input_c < 100)
204−
205− -- Remake types for input
206− case ( 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
207− ( Just (SomeNat (_ :: Proxy inRows)), Just (SomeNat (_ :: Proxy inCols)),
208− Just (SomeNat (_ :: Proxy outRows)), Just (SomeNat (_ :: Proxy outCols)),
209− Just (SomeNat (pkr :: Proxy kernelRows)), Just (SomeNat (pkc :: Proxy kernelCols)),
210− Just (SomeNat (_ :: Proxy strideRows)), Just (SomeNat (_ :: Proxy strideCols))) ->
211− let p1 = natDict pkr
212− p2 = natDict pkc
213− in case ( p1 %* p2
214− -- Fake it till you make it.
215− , (unsafeCoerce (Dict :: Dict ()) :: Dict ( ( 'D2 outRows outCols ) ~ h ))
216− , (unsafeCoerce (Dict :: Dict ()) :: Dict (((outRows - 1) * strideRows) ~ (inRows - kernelRows)))
217− , (unsafeCoerce (Dict :: Dict ()) :: Dict (((outCols - 1) * strideCols) ~ (inCols - kernelCols)))) of
218− (Dict, Dict, Dict, Dict) ->
219− pure (SomeNetwork (Pooling :~> rest :: Network ( Pooling kernelRows kernelCols strideRows strideCols ': layers ) ( ('D2 inRows inCols) ': h ': hs )))
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
224−
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)
229−
230− let input_r = output_r - pad_top - pad_bottom
231− let input_c = output_c - pad_left - pad_right
232−
233− guard (input_r > 1)
234− guard (input_c > 1)
235−
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
251−
252− crop_left <- choose 0 10
253− crop_right <- choose 0 10
254− crop_top <- choose 0 10
255− crop_bottom <- choose 0 10
256−
257− let input_r = output_r + crop_top + crop_bottom
258− let input_c = output_c + crop_left + crop_right
259−
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
272− ]
273− D3Sing r@SNat c@SNat f@SNat ->
274− Gen.choice [
275− pure (SomeNetwork (Tanh :~> rest :: Network ( Tanh ': layers ) ( h ': h ': hs )))
276− , pure (SomeNetwork (Logit :~> rest :: Network ( Logit ': layers ) ( h ': h ': hs )))
277− , pure (SomeNetwork (Relu :~> rest :: Network ( Relu ': 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
285−
286− let ok extent kernel = [stride | stride <- [ 1 .. extent ], (extent - kernel) `mod` stride == 0]
287−
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
292−
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
296−
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
300−
301− guard (input_r < 100)
302− guard (input_c < 100)
303−
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
312− p2 = natDict pkc
313− p3 = natDict chan
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
328−
329− let ok extent kernel = [stride | stride <- [ 1 .. extent ], (extent - kernel) `mod` stride == 0]
330−
331− -- Get some kernels which will fit
332− kernel_r <- choose 1 output_r
333− kernel_c <- choose 1 output_c
334−
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
338−
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
342−
343− guard (input_r < 100)
344− guard (input_c < 100)
345−
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
354− p2 = natDict pkc
355− p3 = natDict chan
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
369−
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)
374−
375− let input_r = output_r - pad_top - pad_bottom
376− let input_c = output_c - pad_left - pad_right
377−
378− guard (input_r > 1)
379− guard (input_c > 1)
380−
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
399−
400− crop_left <- choose 0 10
401− crop_right <- choose 0 10
402− crop_top <- choose 0 10
403− crop_bottom <- choose 0 10
404−
405− let input_r = output_r + crop_top + crop_bottom
406− let input_c = output_c + crop_left + crop_right
407−
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
422− ]
423− ]
424−
425−-- | Test a partial derivative numerically for a random network and input
426−--
427−-- This is the most important test.
428−prop_auto_diff :: Property
429−prop_auto_diff = withDiscards 1000 . withTests 10000 . property $ do
430− SomeNetwork (network :: Network layers shapes) <- forAll genNetwork
431− (input :: S (Head shapes)) <- forAllWith nice genOfShape
432− (target :: S (Last shapes)) <- forAllWith nice oneUp
433− (tested :: S (Head shapes)) <- forAllWith nice oneUp
434−
435− let (!tapes, !output) = runNetwork network input
436− let (_, !backgrad) = runGradient network tapes target
437− let inputDiff = input + tested * 0.00001
438− let expected = maxVal ( backgrad * tested )
439− let (_, !outputDiff) = runNetwork network inputDiff
440− let result = maxVal ( outputDiff * target - output * target ) / 0.00001
441−
442− result ~~~ expected
443−
444−-- Make a shape where all are 0 except for 1 value, which is 1.
445−oneUp :: forall shape. ( SingI shape ) => Gen (S shape)
446−oneUp =
447− case ( sing :: Sing shape ) of
448− D1Sing SNat ->
449− let x = 0 :: S ( shape )
450− in case x of
451− ( S1D x' ) -> do
452− let ex = extract x'
453− let len = VS.length ex
454− ix <- choose 0 (len - 1)
455− let nx = runST $ do ex' <- VS.thaw ex
456− VS.write ex' ix 1.0
457− VS.freeze ex'
458− maybe Gen.discard pure . fromStorable $ nx
459−
460− D2Sing SNat SNat ->
461− let x = 0 :: S ( shape )
462− in case x of
463− ( S2D x' ) -> do
464− let ex = flatten ( extract x' )
465− let len = VS.length ex
466− ix <- choose 0 (len - 1)
467− let nx = runST $ do ex' <- VS.thaw ex
468− VS.write ex' ix 1
469− VS.freeze ex'
470− maybe Gen.discard pure . fromStorable $ nx
471−
472− D3Sing SNat SNat SNat ->
473− let x = 0 :: S ( shape )
474− in case x of
475− ( S3D x' ) -> do
476− let ex = flatten ( extract x' )
477− let len = VS.length ex
478− ix <- choose 0 (len - 1)
479− let nx = runST $ do ex' <- VS.thaw ex
480− VS.write ex' ix 1
481− VS.freeze ex'
482− maybe Gen.discard pure . fromStorable $ nx
483−
484−maxVal :: S shape -> Double
485−maxVal ( S1D x ) = norm_Inf x
486−maxVal ( S2D x ) = norm_Inf x
487−maxVal ( S3D x ) = norm_Inf x
488−
489−(~~~) :: (Monad m, HasCallStack) => Double -> Double -> PropertyT m ()
490−(~~~) x y =
491− if abs (x - y) < 2e-5 then
492− success
493− else
494− withFrozenCallStack $
495− failWith Nothing $ unlines [
496− "━━━ Not Simliar ━━━"
497− , show x
498− , show y
499− ]
500−infix 4 ~~~
501−
502−
503−tests :: IO Bool
504−tests = checkParallel $$(discover)