@@ -52,93 +52,165 @@ newtype GenericArbitrary a = GenericArbitrary { unGenericArbitrary :: a }
5252
5353instance
5454 ( Generic a,
55− GArbitrary a (Rep a),
55+ GArbitrary a (Rep a) 'True,
5656 RecursivelyShrink (Rep a),
5757 GSubterms (Rep a) a
5858 ) => Arbitrary (GenericArbitrary a) where
5959 arbitrary = coerce (genericArbitrary :: Gen a)
6060 shrink = coerce (genericShrink :: a -> [a])
6161
62−-- | Class of finite types
63−class Finite a where
64− -- | Generates final element, when size = 0.
65− final :: QC.Gen a
6662
67−class GArbitrary self a where
68− gArbitrary :: Proxy self -> QC.Gen (a x)
63+-- type family FinalConstructors self (a :: * -> *) :: [* -> *] where
64+-- FinalConstructors self (a :+: b) =
65+-- FinalConstructors self a :++: FinalConstructors self b
66+-- FinalConstructors self (M1 C t f) = If (AllFieldsFinal self f) '[M1 C t f] '[]
6967
70−-- | Unit type instance
71−instance GArbitrary self G.U1 where
72− gArbitrary _ = pure G.U1
68+type family AllFieldsFinal self (a :: * -> *) :: Bool where
69+ AllFieldsFinal self U1 = 'True
70+ AllFieldsFinal self (a :*: b) = AllFieldsFinal self a && AllFieldsFinal self b
71+ AllFieldsFinal self (M1 S t (K1 R self)) = 'False
72+ AllFieldsFinal self (M1 S t (K1 R other)) = 'True
7373
74−-- | Data of the constructor field
75−instance Arbitrary c => GArbitrary self (Rec0 c) where
76− gArbitrary _ = G.K1 <$> arbitrary
74+type family Finite self (a :: * -> *) :: Bool where
75+ Finite self U1 = 'True
76+ -- | The constructor field is the ADT itself. Not finite.
77+ Finite self (K1 R self) = 'False
78+ Finite self (K1 R other) = 'True
79+ Finite self (a :*: b) = Finite self a && Finite self b
80+ Finite self (M1 D t f) = Finite self f
81+ Finite self (a :+: b) = Finite self a || Finite self b
82+ Finite self (M1 C c f) = AllFieldsFinal self f
83+ Finite self (M1 S s f) = Finite self f
7784
78−-- | Data type with single constructor
79−instance
80− ( AllFieldsFinal self f ~ 'True
81− , GArbitrary self (C1 c f)
82− ) => GArbitrary self (D1 t (C1 c f)) where
83− gArbitrary _ = G.M1 <$> gArbitrary (Proxy @self)
85+-- | Calculates count of constructors encoded by particular ':+:'.
86+-- Internal use only.
87+type family SumLen a :: Nat where
88+ SumLen (a G.:+: b) = (SumLen a) + (SumLen b)
89+ SumLen a = 1
90+
91+-- | Generic arbitrary.
92+--
93+-- Parameters are:
94+-- * self: the ADT we generating instance for
95+-- * a: some part of the `Rep self`
96+-- * finite: Is `a` finite? Infinite type has no finite values (like Stream)
97+class (Finite self a ~ finite) => GArbitrary self a (finite :: Bool) where
98+ gArbitrary :: QC.Gen (a x)
8499
85−-- | Data type with multiple constructors
86100instance
87− ( FinalConstructors self (a :+: b) ~ (x ': y)
88− , GArbitrary self (a :+: b)
89− ) => GArbitrary self (D1 t (a :+: b)) where
90− gArbitrary _ = G.M1 <$> gArbitrary (Proxy @self)
101+ ( GArbitrary self (C1 c f) 'True
102+ ) => GArbitrary self (D1 t (C1 c f)) 'True where
103+ gArbitrary = M1 <$> gArbitrary @self
91104
92105-- | The constructor meta information
93−instance GArbitrary self f => GArbitrary self (C1 c f) where
94− gArbitrary _ = G.M1 <$> scale predNat (gArbitrary (Proxy @self))
106+instance
107+ ( GArbitrary self f some
108+ , AllFieldsFinal self f ~ some
109+ ) => GArbitrary self (C1 c f) some where
110+ gArbitrary = M1 <$> scale predNat (gArbitrary @self)
95111 where
96112 predNat 0 = 0
97113 predNat n = pred n
98114
115+-- | Unit type instance
116+instance GArbitrary self U1 'True where
117+ gArbitrary = pure U1
118+
99119-- | Constructor field meta information
100−instance GArbitrary self f => GArbitrary self (S1 t f) where
101− gArbitrary _ = G.M1 <$> gArbitrary (Proxy @self)
120+instance GArbitrary self f some => GArbitrary self (S1 t f) some where
121+ gArbitrary = M1 <$> gArbitrary @self
102122
103−-- | Product
104−instance (GArbitrary self a, GArbitrary self b) => GArbitrary self (a :*: b) where
105− gArbitrary _ = liftA2 (:*:) (gArbitrary (Proxy @self)) (gArbitrary (Proxy @self))
123+-- | Data of the constructor field
124+instance
125+ ( Arbitrary t
126+ , Finite self (Rec0 t) ~ some
127+ ) => GArbitrary self (Rec0 t) some where
128+ gArbitrary = K1 <$> arbitrary
106129
107−-- | Calculates count of constructors encoded by particular ':+:'.
108−-- Internal use only.
109−type family SumLen a :: Nat where
110− SumLen (a G.:+: b) = (SumLen a) + (SumLen b)
111− SumLen a = 1
130+-- | Product
131+instance
132+ ( GArbitrary self a af
133+ , GArbitrary self b bf
134+ , (af && bf) ~ some
135+ ) => GArbitrary self (a :*: b) some where
136+ gArbitrary = liftA2 (:*:) (gArbitrary @self) (gArbitrary @self)
112137
113−type family FinalConstructors self (a :: * -> *) :: [* -> *] where
114− FinalConstructors self (a :+: b) =
115− FinalConstructors self a :++: FinalConstructors self b
116− FinalConstructors self (M1 C t f) = If (AllFieldsFinal self f) '[M1 C t f] '[]
138+instance
139+ ( TypeError (ShowType self :<>: Text " refers to itself in all constructors")
140+ , AllFieldsFinal self f ~ 'False
141+ ) => GArbitrary self (D1 t (C1 c f)) 'False where
142+ gArbitrary = error "Unreachable"
117143
118−type family AllFieldsFinal self (a :: * -> *) :: Bool where
119− AllFieldsFinal self U1 = 'True
120− AllFieldsFinal self (a :*: b) = AllFieldsFinal self a && AllFieldsFinal self b
121− AllFieldsFinal self (M1 S t (K1 R self)) = 'False
122− AllFieldsFinal self (M1 S t (K1 R other)) = 'True
144+-- | ADT declaration with multiple constructors
145+instance
146+ ( FiniteSum self a b af bf
147+ , GArbitrary self (a :+: b) 'True
148+ ) => GArbitrary self (D1 t (a :+: b)) 'True where
149+ gArbitrary = sized $ \s -> M1 <$>
150+ if s > 1 then gArbitrary @self else finiteSum @self
123151
124−-- | Sum
125−instance ( GArbitrary self a, GArbitrary self b
126− , KnownNat (SumLen a), KnownNat (SumLen b)
127− ) => GArbitrary self (a :+: b) where
128− gArbitrary _ = do
129− sized $ \s ->
130− if s > 1 then usual else final
152+-- | Any sum inside of declaration
153+instance
154+ ( GArbitrary self a af, GArbitrary self b bf
155+ , KnownNat (SumLen a), KnownNat (SumLen b)
156+ , (af || bf) ~ some
157+ ) => GArbitrary self (a :+: b) some where
158+ gArbitrary = frequency
159+ [ (lfreq, G.L1 <$> gArbitrary @self)
160+ , (rfreq, G.R1 <$> gArbitrary @self) ]
131161 where
132− usual = frequency
133− [ (lfreq, G.L1 <$> (gArbitrary (Proxy @self)))
134− , (rfreq, G.R1 <$> (gArbitrary (Proxy @self))) ]
135− where
136− lfreq = fromIntegral $ natVal (Proxy :: Proxy (SumLen a))
137− rfreq = fromIntegral $ natVal (Proxy :: Proxy (SumLen b))
138− final = (Prelude.error "FIXME: not implemented")
162+ lfreq = fromIntegral $ natVal (Proxy :: Proxy (SumLen a))
163+ rfreq = fromIntegral $ natVal (Proxy :: Proxy (SumLen b))
164+
165+class
166+ ( Finite self a ~ af, Finite self b ~ bf
167+ ) => FiniteSum self (a :: * -> *) (b :: * -> *) af bf where
168+ finiteSum :: Gen ((a :+: b) p)
169+
170+instance
171+ ( FiniteSumElem self a, FiniteSumElem self b
172+ , Finite self a ~ 'True
173+ , Finite self b ~ 'True
174+ ) => FiniteSum self a b 'True 'True where
175+ finiteSum = oneof
176+ [ L1 <$> finiteElem @self
177+ , R1 <$> finiteElem @self ]
178+
179+instance
180+ ( FiniteSumElem self a
181+ , Finite self a ~ 'True
182+ , Finite self b ~ 'False
183+ ) => FiniteSum self a b 'True 'False where
184+ finiteSum = L1 <$> finiteElem @self
185+
186+instance
187+ ( FiniteSumElem self b
188+ , Finite self a ~ 'False
189+ , Finite self b ~ 'True
190+ ) => FiniteSum self a b 'False 'True where
191+ finiteSum = R1 <$> finiteElem @self
192+
193+class FiniteSumElem self a where
194+ finiteElem :: Gen (a p)
195+
196+instance
197+ ( FiniteSum self a b af bf
198+ ) => FiniteSumElem self (a :+: b) where
199+ finiteElem = finiteSum @self
200+
201+instance
202+ ( GArbitrary self (C1 c f) 'True
203+ ) => FiniteSumElem self (C1 c f) where
204+ finiteElem = gArbitrary @self
205+
206+instance
207+ ( TypeError (ShowType self :<>: Text " refers to itself in all constructors")
208+ , (Finite self a || Finite self b) ~ 'False
209+ ) => GArbitrary self (D1 t (a :+: b)) 'False where
210+ gArbitrary = error "Unreachable"
139211
140212genericArbitrary
141− :: forall a ga
142− . (Generic a, GArbitrary a ga, ga ~ G.Rep a)
213+ :: forall a ga some
214+ . (Generic a, GArbitrary a ga some, ga ~ Rep a)
143215 => Gen a
144−genericArbitrary = G.to <$> gArbitrary (Proxy @a)
216+genericArbitrary = G.to <$> gArbitrary @a