on master help sign in
Pattern match on SNat to remove withKnownNat
commit950971997fa90847d4b9bb75ce3592be7879c9a5 authorHuw Campbell <huw.campbell@ambiata.com> dateSat 22 Apr 2017, 09:19 (9 years ago) parent2f66456
2 files changed+21−30
src/Grenade/Core/Shape.hs+15−24 test/Test/Grenade/Network.hs+6−6
src/Grenade/Core/Shape.hs+15−24
@@ -139,16 +139,13 @@ randomOfShape :: forall x m. ( MonadRandom m, SingI x ) => m (S x)
139139randomOfShape = do
140140 seed :: Int <- getRandom
141141 return $ case (sing :: Sing x) of
142− D1Sing l ->
143− withKnownNat l $
142+ D1Sing SNat ->
144143 S1D (randomVector seed Uniform * 2 - 1)
145144
146− D2Sing r c ->
147− withKnownNat r $ withKnownNat c $
145+ D2Sing SNat SNat ->
148146 S2D (uniformSample seed (-1) 1)
149147
150− D3Sing r c d ->
151− withKnownNat r $ withKnownNat c $ withKnownNat d $
148+ D3Sing SNat SNat SNat ->
152149 S3D (uniformSample seed (-1) 1)
153150
154151-- | Generate a shape from a Storable Vector.
@@ -156,17 +153,14 @@ randomOfShape = do
156153-- Returns Nothing if the vector is of the wrong size.
157154fromStorable :: forall x. SingI x => Vector Double -> Maybe (S x)
158155fromStorable xs = case sing :: Sing x of
159− D1Sing l ->
160− withKnownNat l $
161− S1D <$> H.create xs
156+ D1Sing SNat ->
157+ S1D <$> H.create xs
162158
163− D2Sing r c ->
164− withKnownNat r $ withKnownNat c $
165− S2D <$> mkL xs
159+ D2Sing SNat SNat ->
160+ S2D <$> mkL xs
166161
167− D3Sing r c d ->
168− withKnownNat r $ withKnownNat c $ withKnownNat d $
169− S3D <$> mkL xs
162+ D3Sing SNat SNat SNat ->
163+ S3D <$> mkL xs
170164 where
171165 mkL :: forall rows columns. (KnownNat rows, KnownNat columns)
172166 => Vector Double -> Maybe (L rows columns)
@@ -192,14 +186,11 @@ n2 f (S3D x) (S3D y) = S3D (f x y)
192186-- Helper function for creating the number instances
193187nk :: forall x. SingI x => Double -> S x
194188nk x = case (sing :: Sing x) of
195− D1Sing l ->
196− withKnownNat l $
197− S1D (konst x)
189+ D1Sing SNat ->
190+ S1D (konst x)
198191
199− D2Sing r c ->
200− withKnownNat r $ withKnownNat c $
201− S2D (konst x)
192+ D2Sing SNat SNat ->
193+ S2D (konst x)
202194
203− D3Sing r c d ->
204− withKnownNat r $ withKnownNat c $ withKnownNat d $
205− S3D (konst x)
195+ D3Sing SNat SNat SNat ->
196+ S3D (konst x)
test/Test/Grenade/Network.hs+6−6
@@ -66,7 +66,7 @@ genNetwork =
6666 SCons ( h :: Sing h ) ( _ :: Sing hs ) ->
6767 withSingI h $
6868 case h of
69− D1Sing l -> withKnownNat l $
69+ D1Sing l@SNat ->
7070 Gen.choice [
7171 pure (SomeNetwork (Tanh :~> rest :: Network ( Tanh ': layers ) ( h ': h ': hs )))
7272 , pure (SomeNetwork (Logit :~> rest :: Network ( Logit ': layers ) ( h ': h ': hs )))
@@ -87,7 +87,7 @@ genNetwork =
8787 pure (SomeNetwork (Reshape :~> rest :: Network ( Reshape ': layers ) ( ('D2 inRows inCols) ': h ': hs )))
8888 _ -> Gen.discard -- Doesn't occur
8989 ]
90− D2Sing r c -> withKnownNat r $ withKnownNat c $
90+ D2Sing r@SNat c@SNat ->
9191 Gen.choice [
9292 pure (SomeNetwork (Tanh :~> rest :: Network ( Tanh ': layers ) ( h ': h ': hs )))
9393 , pure (SomeNetwork (Logit :~> rest :: Network ( Logit ': layers ) ( h ': h ': hs )))
@@ -215,7 +215,7 @@ genNetwork =
215215 pure (SomeNetwork (Pooling :~> rest :: Network ( Pooling kernelRows kernelCols strideRows strideCols ': layers ) ( ('D2 inRows inCols) ': h ': hs )))
216216 _ -> Gen.discard -- Can't occur
217217 ]
218− D3Sing r c d -> withKnownNat d $ withKnownNat r $ withKnownNat c $
218+ D3Sing SNat SNat SNat ->
219219 Gen.choice [
220220 pure (SomeNetwork (Tanh :~> rest :: Network ( Tanh ': layers ) ( h ': h ': hs )))
221221 , pure (SomeNetwork (Logit :~> rest :: Network ( Logit ': layers ) ( h ': h ': hs )))
@@ -247,7 +247,7 @@ prop_auto_diff = withTests 10000 . property $ do
247247oneUp :: forall shape m. ( Monad m, SingI shape ) => Gen.Gen m (S shape)
248248oneUp =
249249 case ( sing :: Sing shape ) of
250− D1Sing l -> withKnownNat l $
250+ D1Sing SNat ->
251251 let x = 0 :: S ( shape )
252252 in case x of
253253 ( S1D x' ) -> do
@@ -259,7 +259,7 @@ oneUp =
259259 VS.freeze ex'
260260 maybe Gen.discard pure . fromStorable $ nx
261261
262− D2Sing r c -> withKnownNat r $ withKnownNat c $
262+ D2Sing SNat SNat ->
263263 let x = 0 :: S ( shape )
264264 in case x of
265265 ( S2D x' ) -> do
@@ -271,7 +271,7 @@ oneUp =
271271 VS.freeze ex'
272272 maybe Gen.discard pure . fromStorable $ nx
273273
274− D3Sing r c d -> withKnownNat r $ withKnownNat c $ withKnownNat d $
274+ D3Sing SNat SNat SNat ->
275275 let x = 0 :: S ( shape )
276276 in case x of
277277 ( S3D x' ) -> do