831fd86 · grenade · git.iko.soy

62 ] [

63 do SomeNetwork ( rest :: Network layers shapes ) <- genNetwork

64 case ( sing :: Sing shapes ) of

65− SNil -> Gen.discard

65+ SNil -> Gen.discard -- Can't occur

66 SCons ( h :: Sing h ) ( _ :: Sing hs ) ->

67 withSingI h $

68 case h of

215 pure (SomeNetwork (Pooling :~> rest :: Network ( Pooling kernelRows kernelCols strideRows strideCols ': layers ) ( ('D2 inRows inCols) ': h ': hs )))

216 _ -> Gen.discard -- Can't occur

217 ]

218− D3Sing SNat SNat SNat ->

218+ D3Sing r@SNat c@SNat f@SNat ->

219 Gen.choice [

220 pure (SomeNetwork (Tanh :~> rest :: Network ( Tanh ': layers ) ( h ': h ': hs )))

221 , pure (SomeNetwork (Logit :~> rest :: Network ( Logit ': layers ) ( h ': h ': hs )))

222 , pure (SomeNetwork (Relu :~> rest :: Network ( Relu ': layers ) ( h ': h ': hs )))

223 , pure (SomeNetwork (Elu :~> rest :: Network ( Elu ': layers ) ( h ': h ': hs )))

224+ , do -- Build a convolution layer with one filter output

225+ -- Figure out some kernel sizes which work for this layer

226+ -- There must be a better way than this...

227+ let output_r = natVal r

228+ let output_c = natVal c

229+ let output_f = natVal f

230+

231+ let ok extent kernel = [stride | stride <- [ 1 .. extent ], (extent - kernel) `mod` stride == 0]

232+

233+ -- Get some kernels which will fit

234+ kernel_r <- choose 1 output_r

235+ kernel_c <- choose 1 output_c

236+ channels <- choose 1 10

237+

238+ -- Build up some strides which also fit

239+ stride_r <- Gen.element $ ok output_r kernel_r

240+ stride_c <- Gen.element $ ok output_c kernel_c

241+

242+ -- Determine the input size

243+ let input_r = (output_r - 1) * stride_r + kernel_r

244+ let input_c = (output_c - 1) * stride_c + kernel_c

245+

246+ guard (input_r < 100)

247+ guard (input_c < 100)

248+

249+ -- Remake types for input

250+ 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

251+ ( Just (SomeNat (chan :: Proxy channels)), Just (SomeNat (_ :: Proxy filters)),

252+ Just (SomeNat (pinr :: Proxy inRows)), Just (SomeNat (_ :: Proxy inCols)),

253+ Just (SomeNat (_ :: Proxy outRows)), Just (SomeNat (_ :: Proxy outCols)),

254+ Just (SomeNat (pkr :: Proxy kernelRows)), Just (SomeNat (pkc :: Proxy kernelCols)),

255+ Just (SomeNat (_ :: Proxy strideRows)), Just (SomeNat (_ :: Proxy strideCols))) ->

256+ let p1 = natDict pkr

257+ p2 = natDict pkc

258+ p3 = natDict chan

259+ in case ( p1 %* p2 %* p3

260+ , natDict pinr %* natDict chan

261+ -- Fake it till you make it.

262+ , (unsafeCoerce (Dict :: Dict ()) :: Dict ( ( 'D3 outRows outCols filters) ~ h ))

263+ , (unsafeCoerce (Dict :: Dict ()) :: Dict (((outRows - 1) * strideRows) ~ (inRows - kernelRows)))

264+ , (unsafeCoerce (Dict :: Dict ()) :: Dict (((outCols - 1) * strideCols) ~ (inCols - kernelCols)))) of

265+ (Dict, Dict, Dict, Dict, Dict) -> do

266+ conv <- genConvolution

267+ pure (SomeNetwork (conv :~> rest :: Network ( Convolution channels filters kernelRows kernelCols strideRows strideCols ': layers ) ( ('D3 inRows inCols channels) ': h ': hs )))

268+ _ -> Gen.discard -- Can't occur

269+ , do -- Build a Pooling layer

270+ let output_r = natVal r

271+ let output_c = natVal c

272+ let output_f = natVal f

273+

274+ let ok extent kernel = [stride | stride <- [ 1 .. extent ], (extent - kernel) `mod` stride == 0]

275+

276+ -- Get some kernels which will fit

277+ kernel_r <- choose 1 output_r

278+ kernel_c <- choose 1 output_c

279+

280+ -- Build up some strides which also fit

281+ stride_r <- Gen.element $ ok output_r kernel_r

282+ stride_c <- Gen.element $ ok output_c kernel_c

283+

284+ -- Determine the input size

285+ let input_r = (output_r - 1) * stride_r + kernel_r

286+ let input_c = (output_c - 1) * stride_c + kernel_c

287+

288+ guard (input_r < 100)

289+ guard (input_c < 100)

290+

291+ -- Remake types for input

292+ 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

293+ ( Just (SomeNat (chan :: Proxy filters)),

294+ Just (SomeNat (pinr :: Proxy inRows)), Just (SomeNat (_ :: Proxy inCols)),

295+ Just (SomeNat (_ :: Proxy outRows)), Just (SomeNat (_ :: Proxy outCols)),

296+ Just (SomeNat (pkr :: Proxy kernelRows)), Just (SomeNat (pkc :: Proxy kernelCols)),

297+ Just (SomeNat (_ :: Proxy strideRows)), Just (SomeNat (_ :: Proxy strideCols))) ->

298+ let p1 = natDict pkr

299+ p2 = natDict pkc

300+ p3 = natDict chan

301+ in case ( p1 %* p2 %* p3

302+ , natDict pinr %* natDict chan

303+ -- Fake it till you make it.

304+ , (unsafeCoerce (Dict :: Dict ()) :: Dict ( ( 'D3 outRows outCols filters) ~ h ))

305+ , (unsafeCoerce (Dict :: Dict ()) :: Dict (((outRows - 1) * strideRows) ~ (inRows - kernelRows)))

306+ , (unsafeCoerce (Dict :: Dict ()) :: Dict (((outCols - 1) * strideCols) ~ (inCols - kernelCols)))) of

307+ (Dict, Dict, Dict, Dict, Dict) ->

308+ pure (SomeNetwork (Pooling :~> rest :: Network ( Pooling kernelRows kernelCols strideRows strideCols ': layers ) ( ('D3 inRows inCols filters) ': h ': hs )))

309+ _ -> Gen.discard -- Can't occur

224 ]

310 ]

225 ]

311 ]

226

312

228--

314--

229-- This is the most important test.

315-- This is the most important test.

230prop_auto_diff :: Property

316prop_auto_diff :: Property

231−prop_auto_diff = withTests 10000 . property $ do

317+prop_auto_diff = withDiscards 1000 . withTests 10000 . property $ do

232 SomeNetwork (network :: Network layers shapes) <- forAll genNetwork

318 SomeNetwork (network :: Network layers shapes) <- forAll genNetwork

233 (input :: S (Head shapes)) <- forAllRender nice genOfShape

319 (input :: S (Head shapes)) <- forAllRender nice genOfShape

234 (target :: S (Last shapes)) <- forAllRender nice oneUp

320 (target :: S (Last shapes)) <- forAllRender nice oneUp