@@ -214,6 +214,57 @@ genNetwork =
214 (Dict, Dict, Dict, Dict) ->
214 (Dict, Dict, Dict, Dict) ->
215 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 )))
216 _ -> Gen.discard -- Can't occur
216 _ -> Gen.discard -- Can't occur
217+ , do -- Build a Pad layer
218+ let output_r = natVal r
219+ let output_c = natVal c
221+ pad_left <- choose 0 (output_r - 1)
222+ pad_right <- choose 0 (output_r - 1 - pad_left)
223+ pad_top <- choose 0 (output_c - 1)
224+ pad_bottom <- choose 0 (output_c - 1 - pad_top)
226+ let input_r = output_r - pad_top - pad_bottom
227+ let input_c = output_c - pad_left - pad_right
232+ -- Remake types for input
233+ 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
234+ ( Just (SomeNat (_ :: Proxy inputRows)), Just (SomeNat (_ :: Proxy inputColumns)),
235+ Just (SomeNat (_ :: Proxy outputRows)), Just (SomeNat (_ :: Proxy outputColumns)),
236+ Just (SomeNat (_ :: Proxy padLeft)), Just (SomeNat (_ :: Proxy padRight)),
237+ Just (SomeNat (_ :: Proxy padTop)), Just (SomeNat (_ :: Proxy padBottom))) ->
238+ case ( (unsafeCoerce (Dict :: Dict ()) :: Dict ( ( 'D2 outputRows outputColumns) ~ h ))
239+ , (unsafeCoerce (Dict :: Dict ()) :: Dict ( (inputRows + padTop + padBottom) ~ outputRows) )
240+ , (unsafeCoerce (Dict :: Dict ()) :: Dict ( (inputColumns + padLeft + padRight) ~ outputColumns ))) of
241+ ( Dict, Dict, Dict ) ->
242+ pure (SomeNetwork (Pad :~> rest :: Network ( Pad padLeft padTop padRight padBottom ': layers ) ( ('D2 inputRows inputColumns) ': h ': hs )))
243+ _ -> Gen.discard -- Can't occur
244+ , do -- Build a Crop layer
245+ let output_r = natVal r
246+ let output_c = natVal c
248+ crop_left <- choose 0 10
249+ crop_right <- choose 0 10
250+ crop_top <- choose 0 10
251+ crop_bottom <- choose 0 10
253+ let input_r = output_r + crop_top + crop_bottom
254+ let input_c = output_c + crop_left + crop_right
256+ -- Remake types for input
257+ 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
258+ ( Just (SomeNat (_ :: Proxy inputRows)), Just (SomeNat (_ :: Proxy inputColumns)),
259+ Just (SomeNat (_ :: Proxy outputRows)), Just (SomeNat (_ :: Proxy outputColumns)),
260+ Just (SomeNat (_ :: Proxy cropLeft)), Just (SomeNat (_ :: Proxy cropRight)),
261+ Just (SomeNat (_ :: Proxy cropTop)), Just (SomeNat (_ :: Proxy cropBottom))) ->
262+ case ( (unsafeCoerce (Dict :: Dict ()) :: Dict ( ( 'D2 outputRows outputColumns) ~ h ))
263+ , (unsafeCoerce (Dict :: Dict ()) :: Dict ( (outputRows + cropTop + cropBottom) ~ inputRows ) )
264+ , (unsafeCoerce (Dict :: Dict ()) :: Dict ( (outputColumns + cropLeft + cropRight) ~ inputColumns ))) of
265+ (Dict, Dict, Dict) ->
266+ pure (SomeNetwork (Crop :~> rest :: Network ( Crop cropLeft cropTop cropRight cropBottom ': layers ) ( ('D2 inputRows inputColumns) ': h ': hs )))
267+ _ -> Gen.discard -- Can't occur
218 D3Sing r@SNat c@SNat f@SNat ->
269 D3Sing r@SNat c@SNat f@SNat ->
219 Gen.choice [
270 Gen.choice [
@@ -307,7 +358,64 @@ genNetwork =
307 (Dict, Dict, Dict, Dict, Dict) ->
358 (Dict, Dict, Dict, Dict, Dict) ->
308 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 )))
309 _ -> Gen.discard -- Can't occur
360 _ -> Gen.discard -- Can't occur
361+ , do -- Build a Pad layer
362+ let output_r = natVal r
363+ let output_c = natVal c
364+ let output_f = natVal f
366+ pad_left <- choose 0 (output_r - 1)
367+ pad_right <- choose 0 (output_r - 1 - pad_left)
368+ pad_top <- choose 0 (output_c - 1)
369+ pad_bottom <- choose 0 (output_c - 1 - pad_top)
371+ let input_r = output_r - pad_top - pad_bottom
372+ let input_c = output_c - pad_left - pad_right
377+ -- Remake types for input
378+ 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
379+ ( Just (SomeNat (chan :: Proxy filters)),
380+ Just (SomeNat (pinr :: Proxy inputRows)), Just (SomeNat (_ :: Proxy inputColumns)),
381+ Just (SomeNat (_ :: Proxy outputRows)), Just (SomeNat (_ :: Proxy outputColumns)),
382+ Just (SomeNat (_ :: Proxy padLeft)), Just (SomeNat (_ :: Proxy padRight)),
383+ Just (SomeNat (_ :: Proxy padTop)), Just (SomeNat (_ :: Proxy padBottom))) ->
384+ case ( natDict pinr %* natDict chan
385+ , (unsafeCoerce (Dict :: Dict ()) :: Dict ( ( 'D3 outputRows outputColumns filters) ~ h ))
386+ , (unsafeCoerce (Dict :: Dict ()) :: Dict ( (inputRows + padTop + padBottom) ~ outputRows) )
387+ , (unsafeCoerce (Dict :: Dict ()) :: Dict ( (inputColumns + padLeft + padRight) ~ outputColumns ))) of
388+ (Dict, Dict, Dict, Dict) ->
389+ pure (SomeNetwork (Pad :~> rest :: Network ( Pad padLeft padTop padRight padBottom ': layers ) ( ('D3 inputRows inputColumns filters) ': h ': hs )))
390+ _ -> Gen.discard -- Can't occur
391+ , do -- Build a Crop layer
392+ let output_r = natVal r
393+ let output_c = natVal c
394+ let output_f = natVal f
396+ crop_left <- choose 0 10
397+ crop_right <- choose 0 10
398+ crop_top <- choose 0 10
399+ crop_bottom <- choose 0 10
401+ let input_r = output_r + crop_top + crop_bottom
402+ let input_c = output_c + crop_left + crop_right
404+ -- Remake types for input
405+ 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
406+ ( Just (SomeNat (chan :: Proxy filters)),
407+ Just (SomeNat (pinr :: Proxy inputRows)), Just (SomeNat (_ :: Proxy inputColumns)),
408+ Just (SomeNat (_ :: Proxy outputRows)), Just (SomeNat (_ :: Proxy outputColumns)),
409+ Just (SomeNat (_ :: Proxy cropLeft)), Just (SomeNat (_ :: Proxy cropRight)),
410+ Just (SomeNat (_ :: Proxy cropTop)), Just (SomeNat (_ :: Proxy cropBottom))) ->
411+ case ( natDict pinr %* natDict chan
412+ , (unsafeCoerce (Dict :: Dict ()) :: Dict ( ( 'D3 outputRows outputColumns filters) ~ h ))
413+ , (unsafeCoerce (Dict :: Dict ()) :: Dict ( (outputRows + cropTop + cropBottom) ~ inputRows ) )
414+ , (unsafeCoerce (Dict :: Dict ()) :: Dict ( (outputColumns + cropLeft + cropRight) ~ inputColumns ))) of
415+ (Dict, Dict, Dict, Dict) ->
416+ pure (SomeNetwork (Crop :~> rest :: Network ( Crop cropLeft cropTop cropRight cropBottom ': layers ) ( ('D3 inputRows inputColumns filters) ': h ': hs )))
417+ _ -> Gen.discard -- Can't occur
313-- | Test a partial derivative numerically for a random network and input
421-- | Test a partial derivative numerically for a random network and input
@@ -316,9 +424,9 @@ genNetwork =
316prop_auto_diff :: Property
424prop_auto_diff :: Property
317prop_auto_diff = withDiscards 1000 . withTests 10000 . property $ do
425prop_auto_diff = withDiscards 1000 . withTests 10000 . property $ do
318 SomeNetwork (network :: Network layers shapes) <- forAll genNetwork
426 SomeNetwork (network :: Network layers shapes) <- forAll genNetwork
319− (input :: S (Head shapes)) <- forAllRender nice genOfShape
427+ (input :: S (Head shapes)) <- forAllWith nice genOfShape
320− (target :: S (Last shapes)) <- forAllRender nice oneUp
428+ (target :: S (Last shapes)) <- forAllWith nice oneUp
321− (tested :: S (Head shapes)) <- forAllRender nice oneUp
429+ (tested :: S (Head shapes)) <- forAllWith nice oneUp
323 let (!tapes, !output) = runNetwork network input
431 let (!tapes, !output) = runNetwork network input
324 let (_, !backgrad) = runGradient network tapes target
432 let (_, !backgrad) = runGradient network tapes target