git.iko.soy/grenade
on master help sign in
Pattern match on SNat to remove withKnownNat
9509719Huw Campbell
src/Grenade/Core/Shape.hs+15−24
compare with master
unifiedsplit
@@ -139,16 +139,13 @@ randomOfShape :: forall x m. ( MonadRandom m, SingI x ) => m (S x)
139randomOfShape = do
139randomOfShape = do
140 seed :: Int <- getRandom
140 seed :: Int <- getRandom
141 return $ case (sing :: Sing x) of
141 return $ case (sing :: Sing x) of
142− D1Sing l ->
142+ D1Sing SNat ->
143− withKnownNat l $
144 S1D (randomVector seed Uniform * 2 - 1)
143 S1D (randomVector seed Uniform * 2 - 1)
145
144
146− D2Sing r c ->
145+ D2Sing SNat SNat ->
147− withKnownNat r $ withKnownNat c $
148 S2D (uniformSample seed (-1) 1)
146 S2D (uniformSample seed (-1) 1)
149
147
150− D3Sing r c d ->
148+ D3Sing SNat SNat SNat ->
151− withKnownNat r $ withKnownNat c $ withKnownNat d $
152 S3D (uniformSample seed (-1) 1)
149 S3D (uniformSample seed (-1) 1)
153
150
154-- | Generate a shape from a Storable Vector.
151-- | Generate a shape from a Storable Vector.
@@ -156,17 +153,14 @@ randomOfShape = do
156-- Returns Nothing if the vector is of the wrong size.
153-- Returns Nothing if the vector is of the wrong size.
157fromStorable :: forall x. SingI x => Vector Double -> Maybe (S x)
154fromStorable :: forall x. SingI x => Vector Double -> Maybe (S x)
158fromStorable xs = case sing :: Sing x of
155fromStorable xs = case sing :: Sing x of
159− D1Sing l ->
156+ D1Sing SNat ->
160− withKnownNat l $
161− S1D <$> H.create xs
157+ S1D <$> H.create xs
162
158
163− D2Sing r c ->
159+ D2Sing SNat SNat ->
164− withKnownNat r $ withKnownNat c $
165− S2D <$> mkL xs
160+ S2D <$> mkL xs
166
161
167− D3Sing r c d ->
162+ D3Sing SNat SNat SNat ->
168− withKnownNat r $ withKnownNat c $ withKnownNat d $
169− S3D <$> mkL xs
163+ S3D <$> mkL xs
170 where
164 where
171 mkL :: forall rows columns. (KnownNat rows, KnownNat columns)
165 mkL :: forall rows columns. (KnownNat rows, KnownNat columns)
172 => Vector Double -> Maybe (L rows columns)
166 => Vector Double -> Maybe (L rows columns)
@@ -192,14 +186,11 @@ n2 f (S3D x) (S3D y) = S3D (f x y)
192-- Helper function for creating the number instances
186-- Helper function for creating the number instances
193nk :: forall x. SingI x => Double -> S x
187nk :: forall x. SingI x => Double -> S x
194nk x = case (sing :: Sing x) of
188nk x = case (sing :: Sing x) of
195− D1Sing l ->
189+ D1Sing SNat ->
196− withKnownNat l $
197− S1D (konst x)
190+ S1D (konst x)
198
191
199− D2Sing r c ->
192+ D2Sing SNat SNat ->
200− withKnownNat r $ withKnownNat c $
201− S2D (konst x)
193+ S2D (konst x)
202
194
203− D3Sing r c d ->
195+ D3Sing SNat SNat SNat ->
204− withKnownNat r $ withKnownNat c $ withKnownNat d $
205− S3D (konst x)
196+ S3D (konst x)
test/Test/Grenade/Network.hs+6−6
@@ -66,7 +66,7 @@ genNetwork =
66 SCons ( h :: Sing h ) ( _ :: Sing hs ) ->
66 SCons ( h :: Sing h ) ( _ :: Sing hs ) ->
67 withSingI h $
67 withSingI h $
68 case h of
68 case h of
69− D1Sing l -> withKnownNat l $
69+ D1Sing l@SNat ->
70 Gen.choice [
70 Gen.choice [
71 pure (SomeNetwork (Tanh :~> rest :: Network ( Tanh ': layers ) ( h ': h ': hs )))
71 pure (SomeNetwork (Tanh :~> rest :: Network ( Tanh ': layers ) ( h ': h ': hs )))
72 , pure (SomeNetwork (Logit :~> rest :: Network ( Logit ': layers ) ( h ': h ': hs )))
72 , pure (SomeNetwork (Logit :~> rest :: Network ( Logit ': layers ) ( h ': h ': hs )))
@@ -87,7 +87,7 @@ genNetwork =
87 pure (SomeNetwork (Reshape :~> rest :: Network ( Reshape ': layers ) ( ('D2 inRows inCols) ': h ': hs )))
87 pure (SomeNetwork (Reshape :~> rest :: Network ( Reshape ': layers ) ( ('D2 inRows inCols) ': h ': hs )))
88 _ -> Gen.discard -- Doesn't occur
88 _ -> Gen.discard -- Doesn't occur
89 ]
89 ]
90− D2Sing r c -> withKnownNat r $ withKnownNat c $
90+ D2Sing r@SNat c@SNat ->
91 Gen.choice [
91 Gen.choice [
92 pure (SomeNetwork (Tanh :~> rest :: Network ( Tanh ': layers ) ( h ': h ': hs )))
92 pure (SomeNetwork (Tanh :~> rest :: Network ( Tanh ': layers ) ( h ': h ': hs )))
93 , pure (SomeNetwork (Logit :~> rest :: Network ( Logit ': layers ) ( h ': h ': hs )))
93 , pure (SomeNetwork (Logit :~> rest :: Network ( Logit ': layers ) ( h ': h ': hs )))
@@ -215,7 +215,7 @@ genNetwork =
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 ]
217 ]
218− D3Sing r c d -> withKnownNat d $ withKnownNat r $ withKnownNat c $
218+ D3Sing SNat SNat SNat ->
219 Gen.choice [
219 Gen.choice [
220 pure (SomeNetwork (Tanh :~> rest :: Network ( Tanh ': layers ) ( h ': h ': hs )))
220 pure (SomeNetwork (Tanh :~> rest :: Network ( Tanh ': layers ) ( h ': h ': hs )))
221 , pure (SomeNetwork (Logit :~> rest :: Network ( Logit ': layers ) ( h ': h ': hs )))
221 , pure (SomeNetwork (Logit :~> rest :: Network ( Logit ': layers ) ( h ': h ': hs )))
@@ -247,7 +247,7 @@ prop_auto_diff = withTests 10000 . property $ do
247oneUp :: forall shape m. ( Monad m, SingI shape ) => Gen.Gen m (S shape)
247oneUp :: forall shape m. ( Monad m, SingI shape ) => Gen.Gen m (S shape)
248oneUp =
248oneUp =
249 case ( sing :: Sing shape ) of
249 case ( sing :: Sing shape ) of
250− D1Sing l -> withKnownNat l $
250+ D1Sing SNat ->
251 let x = 0 :: S ( shape )
251 let x = 0 :: S ( shape )
252 in case x of
252 in case x of
253 ( S1D x' ) -> do
253 ( S1D x' ) -> do
@@ -259,7 +259,7 @@ oneUp =
259 VS.freeze ex'
259 VS.freeze ex'
260 maybe Gen.discard pure . fromStorable $ nx
260 maybe Gen.discard pure . fromStorable $ nx
261
261
262− D2Sing r c -> withKnownNat r $ withKnownNat c $
262+ D2Sing SNat SNat ->
263 let x = 0 :: S ( shape )
263 let x = 0 :: S ( shape )
264 in case x of
264 in case x of
265 ( S2D x' ) -> do
265 ( S2D x' ) -> do
@@ -271,7 +271,7 @@ oneUp =
271 VS.freeze ex'
271 VS.freeze ex'
272 maybe Gen.discard pure . fromStorable $ nx
272 maybe Gen.discard pure . fromStorable $ nx
273
273
274− D3Sing r c d -> withKnownNat r $ withKnownNat c $ withKnownNat d $
274+ D3Sing SNat SNat SNat ->
275 let x = 0 :: S ( shape )
275 let x = 0 :: S ( shape )
276 in case x of
276 in case x of
277 ( S3D x' ) -> do
277 ( S3D x' ) -> do