1 {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, UndecidableInstances #-}
7 import qualified Data

.Vector

as DV

8 import qualified Data

.Vector

.Unboxed

as DVU

9 import qualified Data

.Vector

.IVector

as DVI

10 import Data

.Vector

.Unboxed

.Unbox

(Unbox

)
13 instance Arbitrary a

=> Arbitrary

(DV

.Vector a

) where
14 arbitrary

= fmap DV

.fromList arbitrary

15 coarbitrary

= coarbitrary

. DV

.toList

17 instance (Arbitrary a

, Unbox a

) => Arbitrary

(DVU

.Vector a

) where
18 arbitrary

= fmap DVU

.fromList arbitrary

19 coarbitrary

= coarbitrary

. DVU

.toList

22 class Model a b | a

-> b

where
23 -- | Convert a concrete value into an abstract model
26 -- The meat of the models
27 instance Model

(DV

.Vector a

) [a

] where model

= DV

.toList

28 instance Unbox a

=> Model

(DVU

.Vector a

) [a

] where model

= DVU

.toList

31 instance Model

Bool Bool where model

= id
32 instance Model

Int Int where model

= id
33 instance Model

Ordering Ordering where model

= id
36 -- All of these need UndecidableInstances although they are actually well founded. Oh well.
37 instance Model a b

=> Model

(Maybe a

) (Maybe b

) where model

= fmap model

38 instance (Model a c

, Model b d

) => Model

(a

, b

) (c

, d

) where model

(a

, b

) = (model a

, model b

)
39 instance (Model c a

, Model b d

) => Model

(a

-> b

) (c

-> d

) where model f

= model

. f

. model

42 eq1 f g

= \a -> model

(f a

) == g

(model a

)
43 eq2 f g

= \a b

-> model

(f a b

) == g

(model a

) (model b

)
44 eq3 f g

= \a b c

-> model

(f a b c

) == g

(model a

) (model b

) (model c

)
46 eqNotNull1 f g

= \x

-> (not (DVI

.null x

)) ==> eq1 f g x

47 eqNotNull2 f g

= \x y

-> (not (DVI

.null y

)) ==> eq2 f g x y

48 eqNotNull3 f g

= \x y z

-> (not (DVI

.null z

)) ==> eq3 f g x y z