{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Test.Cardano.Ledger.Constrained.SpecClass where
import Cardano.Ledger.Coin (Coin, DeltaCoin)
import Cardano.Ledger.Era (Era)
import Data.Kind
import Data.Map.Strict (Map)
import Data.Set (Set)
import Data.Word (Word64)
import Test.Cardano.Ledger.Common (Arbitrary (arbitrary), Gen)
import Test.Cardano.Ledger.Constrained.Classes (Adds)
import Test.Cardano.Ledger.Constrained.Monad (LiftT)
import Test.Cardano.Ledger.Constrained.Size (Size (..), genFromSize, runSize)
import Test.Cardano.Ledger.Constrained.Spec (
ElemSpec,
ListSpec,
MapSpec,
PairSpec,
RelSpec,
RngSpec,
SetSpec,
SomeLens (SomeLens),
TT,
genElemSpec,
genFromElemSpec,
genFromListSpec,
genFromMapSpec,
genFromPairSpec,
genFromRelSpec,
genFromRngSpec,
genFromSetSpec,
genListSpec,
genMapSpec,
genPairSpec,
genRelSpec,
genRngSpec,
genSetSpec,
genSize,
intDeltaCoinL,
runElemSpec,
runListSpec,
runMapSpec,
runPairSpec,
runRelSpec,
runRngSpec,
runSetSpec,
sizeForElemSpec,
sizeForListSpec,
sizeForMapSpec,
sizeForPairSpec,
sizeForRel,
sizeForRng,
sizeForSetSpec,
word64CoinL,
)
import Test.Cardano.Ledger.Constrained.TypeRep (Rep (..))
import Test.Tasty (defaultMain, testGroup)
import Test.Tasty.QuickCheck (testProperty)
class Arbitrary t => HasRep t where
hasRep :: Rep era t
instance HasRep Word64 where
hasRep :: forall era. Rep era Word64
hasRep = forall era. Rep era Word64
Word64R
instance HasRep Int where
hasRep :: forall era. Rep era Int
hasRep = forall era. Rep era Int
IntR
instance HasRep Coin where
hasRep :: forall era. Rep era Coin
hasRep = forall era. Rep era Coin
CoinR
instance HasRep DeltaCoin where
hasRep :: forall era. Rep era DeltaCoin
hasRep = forall era. Rep era DeltaCoin
DeltaCoinR
class (Monoid spec, LiftT spec) => Specification spec t | spec -> t where
type Count spec :: Type
type Generators spec :: Type
type Reps spec :: Type
type Lenses spec :: Type
runS :: t -> spec -> Bool
genS :: [String] -> Count spec -> Generators spec -> Reps spec -> Lenses spec -> Gen spec
sizeForS :: spec -> Size
genFromS :: [String] -> Int -> Generators spec -> spec -> Gen t
instance Specification Size Int where
type Count Size = ()
type Generators Size = ()
type Reps Size = ()
type Lenses Size = ()
runS :: Int -> Size -> Bool
runS = Int -> Size -> Bool
runSize
genS :: [String]
-> Count Size
-> Generators Size
-> Reps Size
-> Lenses Size
-> Gen Size
genS [String]
_ Count Size
_ Generators Size
_ Reps Size
_ Lenses Size
_ = Gen Size
genSize
sizeForS :: Size -> Size
sizeForS = forall a. a -> a
id
genFromS :: [String] -> Int -> Generators Size -> Size -> Gen Int
genFromS [String]
_ Int
_ Generators Size
_ = Size -> Gen Int
genFromSize
instance
(Era era, Ord dom , Ord rng, Adds rng) =>
Specification (MapSpec era dom rng) (Map dom rng)
where
type Count (MapSpec era dom rng) = Int
type Generators (MapSpec era dom rng) = (Gen dom, Gen rng)
type Reps (MapSpec era dom rng) = (Rep era dom, Rep era rng)
type Lenses (MapSpec era dom rng) = SomeLens era rng
runS :: Map dom rng -> MapSpec era dom rng -> Bool
runS = forall d r era. (Ord d, Eq r) => Map d r -> MapSpec era d r -> Bool
runMapSpec
genS :: [String]
-> Count (MapSpec era dom rng)
-> Generators (MapSpec era dom rng)
-> Reps (MapSpec era dom rng)
-> Lenses (MapSpec era dom rng)
-> Gen (MapSpec era dom rng)
genS [String]
_ Count (MapSpec era dom rng)
count (Gen dom
genD, Gen rng
_) (Rep era dom
domRep, Rep era rng
rngRep) Lenses (MapSpec era dom rng)
sl = forall era dom w.
(Ord dom, Era era, Ord w, Adds w) =>
Gen dom
-> Rep era dom
-> Rep era w
-> SomeLens era w
-> Int
-> Gen (MapSpec era dom w)
genMapSpec Gen dom
genD Rep era dom
domRep Rep era rng
rngRep Lenses (MapSpec era dom rng)
sl Count (MapSpec era dom rng)
count
sizeForS :: MapSpec era dom rng -> Size
sizeForS = forall era d r. MapSpec era d r -> Size
sizeForMapSpec
genFromS :: [String]
-> Int
-> Generators (MapSpec era dom rng)
-> MapSpec era dom rng
-> Gen (Map dom rng)
genFromS [String]
msgs Int
_count (Gen dom
genD, Gen rng
genR) MapSpec era dom rng
spec = forall era w dom.
(Era era, Ord dom) =>
String
-> [String]
-> Gen dom
-> Gen w
-> MapSpec era dom w
-> Gen (Map dom w)
genFromMapSpec String
"genFromMapSpec" [String]
msgs Gen dom
genD Gen rng
genR MapSpec era dom rng
spec
instance
(Era era, Ord dom, Eq rng, HasRep dom, HasRep rng) =>
Specification (PairSpec era dom rng) (Map dom rng)
where
type Count (PairSpec era dom rng) = Int
type Generators (PairSpec era dom rng) = ()
type Reps (PairSpec era dom rng) = ()
type Lenses (PairSpec era dom rng) = ()
runS :: Map dom rng -> PairSpec era dom rng -> Bool
runS = forall dom rng era.
(Ord dom, Eq rng) =>
Map dom rng -> PairSpec era dom rng -> Bool
runPairSpec
genS :: [String]
-> Count (PairSpec era dom rng)
-> Generators (PairSpec era dom rng)
-> Reps (PairSpec era dom rng)
-> Lenses (PairSpec era dom rng)
-> Gen (PairSpec era dom rng)
genS [String]
_msgs Count (PairSpec era dom rng)
_count Generators (PairSpec era dom rng)
_g Reps (PairSpec era dom rng)
_ Lenses (PairSpec era dom rng)
_ = forall era dom rng.
(Ord dom, Eq rng) =>
Rep era dom -> Rep era rng -> Gen (PairSpec era dom rng)
genPairSpec forall t era. HasRep t => Rep era t
hasRep forall t era. HasRep t => Rep era t
hasRep
sizeForS :: PairSpec era dom rng -> Size
sizeForS = forall era dom rng. PairSpec era dom rng -> Size
sizeForPairSpec
genFromS :: [String]
-> Int
-> Generators (PairSpec era dom rng)
-> PairSpec era dom rng
-> Gen (Map dom rng)
genFromS [String]
msgs Int
_count () PairSpec era dom rng
spec = forall era dom rng.
Ord dom =>
[String] -> PairSpec era dom rng -> Gen (Map dom rng)
genFromPairSpec [String]
msgs PairSpec era dom rng
spec
instance
(Era era, Ord dom, HasRep dom) =>
Specification (RelSpec era dom) (Set dom)
where
type Count (RelSpec era dom) = Int
type Generators (RelSpec era dom) = Gen dom
type Reps (RelSpec era dom) = ()
type Lenses (RelSpec era dom) = ()
runS :: Set dom -> RelSpec era dom -> Bool
runS = forall t era. Ord t => Set t -> RelSpec era t -> Bool
runRelSpec
genS :: [String]
-> Count (RelSpec era dom)
-> Generators (RelSpec era dom)
-> Reps (RelSpec era dom)
-> Lenses (RelSpec era dom)
-> Gen (RelSpec era dom)
genS [String]
msgs Count (RelSpec era dom)
count Generators (RelSpec era dom)
g Reps (RelSpec era dom)
_ Lenses (RelSpec era dom)
_ = forall dom era.
Ord dom =>
[String] -> Gen dom -> Rep era dom -> Int -> Gen (RelSpec era dom)
genRelSpec [String]
msgs Generators (RelSpec era dom)
g forall t era. HasRep t => Rep era t
hasRep Count (RelSpec era dom)
count
sizeForS :: RelSpec era dom -> Size
sizeForS = forall era dom. RelSpec era dom -> Size
sizeForRel
genFromS :: [String]
-> Int
-> Generators (RelSpec era dom)
-> RelSpec era dom
-> Gen (Set dom)
genFromS [String]
msgs Int
count Generators (RelSpec era dom)
g RelSpec era dom
spec = forall era t.
(Era era, Ord t) =>
[String] -> Gen t -> Int -> RelSpec era t -> Gen (Set t)
genFromRelSpec [String]
msgs Generators (RelSpec era dom)
g Int
count RelSpec era dom
spec
instance
(Era era, Adds rng, Ord rng) =>
Specification (RngSpec era rng) [rng]
where
type Count (RngSpec era rng) = Int
type Generators (RngSpec era rng) = Gen rng
type Reps (RngSpec era rng) = Rep era rng
type Lenses (RngSpec era rng) = SomeLens era rng
runS :: [rng] -> RngSpec era rng -> Bool
runS = forall r era. [r] -> RngSpec era r -> Bool
runRngSpec
genS :: [String]
-> Count (RngSpec era rng)
-> Generators (RngSpec era rng)
-> Reps (RngSpec era rng)
-> Lenses (RngSpec era rng)
-> Gen (RngSpec era rng)
genS [String]
_msgs Count (RngSpec era rng)
count Generators (RngSpec era rng)
g Reps (RngSpec era rng)
r Lenses (RngSpec era rng)
sl = forall w era.
(Ord w, Adds w) =>
Gen w -> Rep era w -> SomeLens era w -> Int -> Gen (RngSpec era w)
genRngSpec Generators (RngSpec era rng)
g Reps (RngSpec era rng)
r Lenses (RngSpec era rng)
sl Count (RngSpec era rng)
count
sizeForS :: RngSpec era rng -> Size
sizeForS = forall dom era. RngSpec era dom -> Size
sizeForRng
genFromS :: [String]
-> Int
-> Generators (RngSpec era rng)
-> RngSpec era rng
-> Gen [rng]
genFromS [String]
msgs Int
count Generators (RngSpec era rng)
g RngSpec era rng
spec = forall era r.
Era era =>
[String] -> Gen r -> Int -> RngSpec era r -> Gen [r]
genFromRngSpec [String]
msgs Generators (RngSpec era rng)
g Int
count RngSpec era rng
spec
instance
(Era era, Ord a, HasRep a) =>
Specification (SetSpec era a) (Set a)
where
type Count (SetSpec era a) = Int
type Generators (SetSpec era a) = Gen a
type Reps (SetSpec era a) = ()
type Lenses (SetSpec era a) = ()
runS :: Set a -> SetSpec era a -> Bool
runS = forall a era. Set a -> SetSpec era a -> Bool
runSetSpec
genS :: [String]
-> Count (SetSpec era a)
-> Generators (SetSpec era a)
-> Reps (SetSpec era a)
-> Lenses (SetSpec era a)
-> Gen (SetSpec era a)
genS [String]
msgs Count (SetSpec era a)
count Generators (SetSpec era a)
g Reps (SetSpec era a)
_ Lenses (SetSpec era a)
_ = forall s era.
Ord s =>
[String] -> Gen s -> Rep era s -> Int -> Gen (SetSpec era s)
genSetSpec [String]
msgs Generators (SetSpec era a)
g forall t era. HasRep t => Rep era t
hasRep Count (SetSpec era a)
count
sizeForS :: SetSpec era a -> Size
sizeForS = forall era a. SetSpec era a -> Size
sizeForSetSpec
genFromS :: [String]
-> Int
-> Generators (SetSpec era a)
-> SetSpec era a
-> Gen (Set a)
genFromS [String]
msgs Int
_count Generators (SetSpec era a)
g SetSpec era a
spec = forall era a.
Era era =>
[String] -> Gen a -> SetSpec era a -> Gen (Set a)
genFromSetSpec [String]
msgs Generators (SetSpec era a)
g SetSpec era a
spec
instance
(Era era, HasRep a, Adds a) =>
Specification (ElemSpec era a) [a]
where
type Count (ElemSpec era a) = Size
type Generators (ElemSpec era a) = Gen a
type Reps (ElemSpec era a) = ()
type Lenses (ElemSpec era a) = SomeLens era a
runS :: [a] -> ElemSpec era a -> Bool
runS = forall a era. [a] -> ElemSpec era a -> Bool
runElemSpec
genS :: [String]
-> Count (ElemSpec era a)
-> Generators (ElemSpec era a)
-> Reps (ElemSpec era a)
-> Lenses (ElemSpec era a)
-> Gen (ElemSpec era a)
genS [String]
_msgs Count (ElemSpec era a)
count Generators (ElemSpec era a)
_g Reps (ElemSpec era a)
_ Lenses (ElemSpec era a)
sl = forall w era.
Adds w =>
Rep era w -> SomeLens era w -> Size -> Gen (ElemSpec era w)
genElemSpec forall t era. HasRep t => Rep era t
hasRep Lenses (ElemSpec era a)
sl Count (ElemSpec era a)
count
sizeForS :: ElemSpec era a -> Size
sizeForS = forall a era. ElemSpec era a -> Size
sizeForElemSpec
genFromS :: [String]
-> Int -> Generators (ElemSpec era a) -> ElemSpec era a -> Gen [a]
genFromS [String]
msgs Int
count Generators (ElemSpec era a)
g ElemSpec era a
spec = forall era r. [String] -> Gen r -> Int -> ElemSpec era r -> Gen [r]
genFromElemSpec [String]
msgs Generators (ElemSpec era a)
g Int
count ElemSpec era a
spec
instance
(Era era, HasRep a, Adds a) =>
Specification (ListSpec era a) [a]
where
type Count (ListSpec era a) = Size
type Generators (ListSpec era a) = Gen a
type Reps (ListSpec era a) = ()
type Lenses (ListSpec era a) = SomeLens era a
runS :: [a] -> ListSpec era a -> Bool
runS = forall a era. [a] -> ListSpec era a -> Bool
runListSpec
genS :: [String]
-> Count (ListSpec era a)
-> Generators (ListSpec era a)
-> Reps (ListSpec era a)
-> Lenses (ListSpec era a)
-> Gen (ListSpec era a)
genS [String]
_msgs Count (ListSpec era a)
count Generators (ListSpec era a)
_g Reps (ListSpec era a)
_ Lenses (ListSpec era a)
sl = forall w era.
Adds w =>
Rep era w -> SomeLens era w -> Size -> Gen (ListSpec era w)
genListSpec forall t era. HasRep t => Rep era t
hasRep Lenses (ListSpec era a)
sl Count (ListSpec era a)
count
sizeForS :: ListSpec era a -> Size
sizeForS = forall era t. ListSpec era t -> Size
sizeForListSpec
genFromS :: [String]
-> Int -> Generators (ListSpec era a) -> ListSpec era a -> Gen [a]
genFromS [String]
msgs Int
_count Generators (ListSpec era a)
g ListSpec era a
spec = forall era r. [String] -> Gen r -> ListSpec era r -> Gen [r]
genFromListSpec [String]
msgs Generators (ListSpec era a)
g ListSpec era a
spec
testSound ::
forall spec t.
Specification spec t =>
Lenses spec ->
Reps spec ->
Count spec ->
Generators spec ->
Gen Bool
testSound :: forall spec t.
Specification spec t =>
Lenses spec
-> Reps spec -> Count spec -> Generators spec -> Gen Bool
testSound Lenses spec
l Reps spec
r Count spec
c Generators spec
g = do
spec
spec <- forall spec t.
Specification spec t =>
[String]
-> Count spec
-> Generators spec
-> Reps spec
-> Lenses spec
-> Gen spec
genS @spec [String
"testSound"] Count spec
c Generators spec
g Reps spec
r Lenses spec
l
t
ans <- forall spec t.
Specification spec t =>
[String] -> Int -> Generators spec -> spec -> Gen t
genFromS @spec [String
"testSound"] Int
10 Generators spec
g spec
spec
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall spec t. Specification spec t => t -> spec -> Bool
runS t
ans spec
spec
main :: IO ()
main :: IO ()
main =
TestTree -> IO ()
defaultMain forall a b. (a -> b) -> a -> b
$
String -> [TestTree] -> TestTree
testGroup
String
"Generic Specification class tests"
[ String -> [TestTree] -> TestTree
testGroup
String
"Generic testSound"
[ forall a. Testable a => String -> a -> TestTree
testProperty String
"Size" forall a b. (a -> b) -> a -> b
$ forall spec t.
Specification spec t =>
Lenses spec
-> Reps spec -> Count spec -> Generators spec -> Gen Bool
testSound @Size @Int ()
, forall a. Testable a => String -> a -> TestTree
testProperty String
"MapSpec" forall a b. (a -> b) -> a -> b
$
forall spec t.
Specification spec t =>
Lenses spec
-> Reps spec -> Count spec -> Generators spec -> Gen Bool
testSound @(MapSpec TT Int Word64) (forall c t era. Adds c => Lens' t c -> SomeLens era t
SomeLens Lens' Word64 Coin
word64CoinL) (forall era. Rep era Int
IntR, forall era. Rep era Word64
Word64R) Int
10 (forall a. Arbitrary a => Gen a
arbitrary, forall a. Arbitrary a => Gen a
arbitrary)
, forall a. Testable a => String -> a -> TestTree
testProperty String
"PairSpec" forall a b. (a -> b) -> a -> b
$ forall spec t.
Specification spec t =>
Lenses spec
-> Reps spec -> Count spec -> Generators spec -> Gen Bool
testSound @(PairSpec TT Int Word64) () () Int
10
, forall a. Testable a => String -> a -> TestTree
testProperty String
"RelSpec" forall a b. (a -> b) -> a -> b
$ forall spec t.
Specification spec t =>
Lenses spec
-> Reps spec -> Count spec -> Generators spec -> Gen Bool
testSound @(RelSpec TT Int) () () Int
10 forall a. Arbitrary a => Gen a
arbitrary
, forall a. Testable a => String -> a -> TestTree
testProperty String
"RngSpec" forall a b. (a -> b) -> a -> b
$
forall spec t.
Specification spec t =>
Lenses spec
-> Reps spec -> Count spec -> Generators spec -> Gen Bool
testSound @(RngSpec TT Int) (forall c t era. Adds c => Lens' t c -> SomeLens era t
SomeLens Lens' Int DeltaCoin
intDeltaCoinL) forall era. Rep era Int
IntR Int
10 forall a. Arbitrary a => Gen a
arbitrary
, forall a. Testable a => String -> a -> TestTree
testProperty String
"ListSpec" forall a b. (a -> b) -> a -> b
$
forall spec t.
Specification spec t =>
Lenses spec
-> Reps spec -> Count spec -> Generators spec -> Gen Bool
testSound @(ListSpec TT Int) (forall c t era. Adds c => Lens' t c -> SomeLens era t
SomeLens Lens' Int DeltaCoin
intDeltaCoinL) () Size
SzAny forall a. Arbitrary a => Gen a
arbitrary
, forall a. Testable a => String -> a -> TestTree
testProperty String
"ElemSpec" forall a b. (a -> b) -> a -> b
$
forall spec t.
Specification spec t =>
Lenses spec
-> Reps spec -> Count spec -> Generators spec -> Gen Bool
testSound @(ElemSpec TT Int) (forall c t era. Adds c => Lens' t c -> SomeLens era t
SomeLens Lens' Int DeltaCoin
intDeltaCoinL) () Size
SzAny forall a. Arbitrary a => Gen a
arbitrary
]
]