@@ -1,5 +1,3 @@
1−{-# LANGUAGE UndecidableInstances, TypeOperators, DataKinds, TypeFamilies, ScopedTypeVariables#-}
2−
31{- |
42
53Generic implementation of the 'arbitrary' method. Example usage:
@@ -38,43 +36,63 @@ module Test.QuickCheck.Arbitrary.Generic
3836 , genericShrink
3937 ) where
4038
41−import Control.Applicative
42−import Data.Coerce (coerce)
43−import Data.Proxy
44−import GHC.Generics as G
45−import GHC.TypeLits
46−import Test.QuickCheck as QC
47−import Test.QuickCheck.Arbitrary (GSubterms, RecursivelyShrink)
39+import Control.Applicative
40+import Data.Coerce (coerce)
41+import Data.Proxy
42+import Data.Type.Bool
43+import GHC.Generics as G
44+import GHC.TypeLits
45+import Test.QuickCheck as QC
46+import Test.QuickCheck.Arbitrary (GSubterms, RecursivelyShrink)
47+import TypeFun.Data.Eq
48+import TypeFun.Data.List
4849
4950newtype GenericArbitrary a = GenericArbitrary { unGenericArbitrary :: a }
5051 deriving (Show, Eq)
5152
5253instance
5354 ( Generic a,
54− GArbitrary (Rep a),
55+ GArbitrary (Rep a) (Rep a),
5556 RecursivelyShrink (Rep a),
5657 GSubterms (Rep a) a
5758 ) => Arbitrary (GenericArbitrary a) where
5859 arbitrary = coerce (genericArbitrary :: Gen a)
5960 shrink = coerce (genericShrink :: a -> [a])
6061
61−class GArbitrary a where
62− gArbitrary :: QC.Gen (a x)
62+-- | Class of finite types
63+class Finite a where
64+ -- | Generates final element, when size = 0.
65+ final :: QC.Gen a
66+
67+class GArbitrary root a where
68+ gArbitrary :: Proxy root -> QC.Gen (a x)
69+
70+-- | Unit type instance
71+instance GArbitrary root G.U1 where
72+ gArbitrary _ = pure G.U1
6373
64−instance GArbitrary G.U1 where
65− gArbitrary = pure G.U1
74+-- | Data of the constructor field
75+instance Arbitrary c => GArbitrary root (Rec0 c) where
76+ gArbitrary _ = G.K1 <$> arbitrary
6677
67−instance Arbitrary c => GArbitrary (G.K1 i c) where
68− gArbitrary = G.K1 <$> scale predNat arbitrary
78+-- | Data type meta information
79+instance GArbitrary (D1 t f) f => GArbitrary (D1 t f) (D1 t f) where
80+ gArbitrary _ = G.M1 <$> gArbitrary (Proxy @(D1 t f))
81+
82+-- | The constructor meta information
83+instance GArbitrary root f => GArbitrary root (C1 c f) where
84+ gArbitrary _ = G.M1 <$> scale predNat (gArbitrary (Proxy @root))
6985 where
7086 predNat 0 = 0
7187 predNat n = pred n
7288
73−instance GArbitrary f => GArbitrary (G.M1 i c f) where
74− gArbitrary = G.M1 <$> gArbitrary
89+-- | Constructor field meta information
90+instance GArbitrary root f => GArbitrary root (S1 t f) where
91+ gArbitrary _ = G.M1 <$> gArbitrary (Proxy @root)
7592
76−instance (GArbitrary a, GArbitrary b) => GArbitrary (a G.:*: b) where
77− gArbitrary = liftA2 (G.:*:) gArbitrary gArbitrary
93+-- | Product
94+instance (GArbitrary root a, GArbitrary root b) => GArbitrary root (a :*: b) where
95+ gArbitrary _ = liftA2 (:*:) (gArbitrary (Proxy @root)) (gArbitrary (Proxy @root))
7896
7997-- | Calculates count of constructors encoded by particular ':+:'.
8098-- Internal use only.
@@ -82,14 +100,35 @@ type family SumLen a :: Nat where
82100 SumLen (a G.:+: b) = (SumLen a) + (SumLen b)
83101 SumLen a = 1
84102
85−instance (GArbitrary a, GArbitrary b, KnownNat (SumLen a), KnownNat (SumLen b)
86− ) => GArbitrary (a G.:+: b) where
87− gArbitrary = frequency
88− [ (lfreq, G.L1 <$> gArbitrary)
89− , (rfreq, G.R1 <$> gArbitrary) ]
103+type family FinalConstructors root (a :: * -> *) :: [* -> *] where
104+ FinalConstructors root (a :+: b) =
105+ FinalConstructors root a :++: FinalConstructors root b
106+ FinalConstructors root (M1 C t f) = If (AllFieldsFinal root f) '[M1 C t f] '[]
107+
108+type family AllFieldsFinal root (a :: * -> *) :: Bool where
109+ AllFieldsFinal root U1 = 'True
110+ AllFieldsFinal root (a :*: b) = AllFieldsFinal root a && AllFieldsFinal root b
111+ AllFieldsFinal root (M1 S t (K1 R typ)) = Not (Equal (Rep typ) root)
112+
113+-- | Sum
114+instance ( (FinalConstructors root (a :+: b) ~ (x ': y))
115+ , GArbitrary root a, GArbitrary root b
116+ , KnownNat (SumLen a), KnownNat (SumLen b)
117+ ) => GArbitrary root (a :+: b) where
118+ gArbitrary _ = do
119+ sized $ \s ->
120+ if s > 1 then usual else final
90121 where
91− lfreq = fromIntegral $ natVal (Proxy :: Proxy (SumLen a))
92− rfreq = fromIntegral $ natVal (Proxy :: Proxy (SumLen b))
93−
94−genericArbitrary :: (Generic a, GArbitrary ga, ga ~ G.Rep a) => Gen a
95−genericArbitrary = G.to <$> gArbitrary
122+ usual = frequency
123+ [ (lfreq, G.L1 <$> (gArbitrary (Proxy @root)))
124+ , (rfreq, G.R1 <$> (gArbitrary (Proxy @root))) ]
125+ where
126+ lfreq = fromIntegral $ natVal (Proxy :: Proxy (SumLen a))
127+ rfreq = fromIntegral $ natVal (Proxy :: Proxy (SumLen b))
128+ final = (Prelude.error "FIXME: not implemented")
129+
130+genericArbitrary
131+ :: forall a ga
132+ . (Generic a, GArbitrary ga ga, ga ~ G.Rep a)
133+ => Gen a
134+genericArbitrary = G.to <$> gArbitrary (Proxy @ga)