{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- | Code which defines a class that encapsulates what it means to be a Spec
--   Eventually this will repace the most of the tests in Spec.hs
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)

-- import Lens.Micro (Lens')

{-
-- NOtes about current functions and their types for each Spec. This helps
-- design what the SpecClass should provide.
class (Monoid spec, LiftT spec) => Specification spec t | spec -> t where
  type Count :: Type -> Type
  -- type Count Size = ()
  --      Count RelSpec = Int
  --      Count RngSpec = Int
  --      Count MapSpec = Int
  --      Count SetSpec = Int
  --      Count ElemSpec = Size
  --      Count ListSpec = Size
  --      Count AddsSpec = () -- This is not ready yet. TODO
  type Generators spec :: Type
  -- type Generators Size = ()
  -- type Generators (MapSpec era dom rng) = (Gen dom, Gen rng)
  -- type Generators (RelSpec era dom) = Gen dom
  -- ...
  runS :: t -> spec -> Bool
  genS :: [String] -> Count spec -> Generators spec -> Gen spec
  sizeForS :: spec -> Size
  genFromS :: [String] -> Int -> Generators spec -> spec -> Gen t

Notes:

genFromSize     ::                                                                 Size              -> Gen Int
genFromRelSpec  :: forall era t. Ord t => [String] -> Gen t            -> Int   -> RelSpec era t     -> Gen (Set t)
genFromRngSpec  :: forall era r.          [String] -> Gen r            -> Int   -> RngSpec era r     -> Gen [r]
genFromMapSpec  ::              String -> [String] -> Gen dom -> Gen w          -> MapSpec era dom w -> Gen (Map dom w)
genFromSetSpec  :: forall era a.          [String] -> Gen a                     -> SetSpec era a     -> Gen (Set a)
genFromElemSpec ::                        [String] -> Gen r            -> Int   -> ElemSpec era r    -> Gen [r]
genFromListSpec ::                        [String] -> Gen r                     -> ListSpec era r    -> Gen [r]
genFromAddsSpec ::                        [String]                              -> AddsSpec c        -> Gen Int

genConsistentSize
genConsistentRelSpec ::                          [String] -> Gen dom -> RelSpec era dom -> Gen (RelSpec era dom)
genConsistentRngSpec :: ( Adds w , Sums w c ) => Int -> Gen w -> Rep era w -> Rep era c -> Gen (RngSpec era w, RngSpec era w)
TODO
genConsisent*Spec for all the other Specs
-}

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

  -- genConsistentS :: [String] -> Count spec -> Generators spec -> Reps spec -> spec -> Gen spec
  -- genConsistentS :: [String] -> Count spec -> Generators spec -> Reps spec -> gen (spec, 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 {- HasRep dom, HasRep rng, HasRep c, -}, 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
          ]
      ]