@@ -214,6 +214,57 @@ genNetwork =
214214 (Dict, Dict, Dict, Dict) ->
215215 pure (SomeNetwork (Pooling :~> rest :: Network ( Pooling kernelRows kernelCols strideRows strideCols ': layers ) ( ('D2 inRows inCols) ': h ': hs )))
216216 _ -> Gen.discard -- Can't occur
217+ , do -- Build a Pad layer
218+ let output_r = natVal r
219+ let output_c = natVal c
220+
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)
225+
226+ let input_r = output_r - pad_top - pad_bottom
227+ let input_c = output_c - pad_left - pad_right
228+
229+ guard (input_r > 1)
230+ guard (input_c > 1)
231+
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
247+
248+ crop_left <- choose 0 10
249+ crop_right <- choose 0 10
250+ crop_top <- choose 0 10
251+ crop_bottom <- choose 0 10
252+
253+ let input_r = output_r + crop_top + crop_bottom
254+ let input_c = output_c + crop_left + crop_right
255+
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
217268 ]
218269 D3Sing r@SNat c@SNat f@SNat ->
219270 Gen.choice [
@@ -307,7 +358,64 @@ genNetwork =
307358 (Dict, Dict, Dict, Dict, Dict) ->
308359 pure (SomeNetwork (Pooling :~> rest :: Network ( Pooling kernelRows kernelCols strideRows strideCols ': layers ) ( ('D3 inRows inCols filters) ': h ': hs )))
309360 _ -> Gen.discard -- Can't occur
310− ]
361+ , do -- Build a Pad layer
362+ let output_r = natVal r
363+ let output_c = natVal c
364+ let output_f = natVal f
365+
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)
370+
371+ let input_r = output_r - pad_top - pad_bottom
372+ let input_c = output_c - pad_left - pad_right
373+
374+ guard (input_r > 1)
375+ guard (input_c > 1)
376+
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
395+
396+ crop_left <- choose 0 10
397+ crop_right <- choose 0 10
398+ crop_top <- choose 0 10
399+ crop_bottom <- choose 0 10
400+
401+ let input_r = output_r + crop_top + crop_bottom
402+ let input_c = output_c + crop_left + crop_right
403+
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
418+ ]
311419 ]
312420
313421-- | Test a partial derivative numerically for a random network and input
@@ -316,9 +424,9 @@ genNetwork =
316424prop_auto_diff :: Property
317425prop_auto_diff = withDiscards 1000 . withTests 10000 . property $ do
318426 SomeNetwork (network :: Network layers shapes) <- forAll genNetwork
319− (input :: S (Head shapes)) <- forAllRender nice genOfShape
320− (target :: S (Last shapes)) <- forAllRender nice oneUp
321− (tested :: S (Head shapes)) <- forAllRender nice oneUp
427+ (input :: S (Head shapes)) <- forAllWith nice genOfShape
428+ (target :: S (Last shapes)) <- forAllWith nice oneUp
429+ (tested :: S (Head shapes)) <- forAllWith nice oneUp
322430
323431 let (!tapes, !output) = runNetwork network input
324432 let (_, !backgrad) = runGradient network tapes target