{-# LANGUAGE FlexibleContexts #-}

module Test.LedgerTables
  ( prop_hasledgertables_laws
  , prop_stowable_laws
  ) where

import Data.Function (on)
import Ouroboros.Consensus.Ledger.Abstract
import Test.QuickCheck

-- | We compare the Ledger Tables of the result because the comparison with the
-- rest of the LedgerState takes considerably more time to run.
(==?) ::
  ( CanMapMK mk
  , CanMapKeysMK mk
  , ZeroableMK mk
  , EqMK mk
  , ShowMK mk
  , HasLedgerTables LedgerState blk
  , Show (TxIn blk)
  , Show (TxOut blk)
  ) =>
  LedgerState blk mk ->
  LedgerState blk mk ->
  Property
==? :: forall (mk :: MapKind) blk.
(CanMapMK mk, CanMapKeysMK mk, ZeroableMK mk, EqMK mk, ShowMK mk,
 HasLedgerTables LedgerState blk, Show (TxIn blk),
 Show (TxOut blk)) =>
LedgerState blk mk -> LedgerState blk mk -> Property
(==?) = LedgerTables blk mk -> LedgerTables blk mk -> Property
forall a. (Eq a, Show a) => a -> a -> Property
(===) (LedgerTables blk mk -> LedgerTables blk mk -> Property)
-> (LedgerState blk mk -> LedgerTables blk mk)
-> LedgerState blk mk
-> LedgerState blk mk
-> Property
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` LedgerState blk mk -> LedgerTables blk mk
forall (mk :: MapKind).
(CanMapMK mk, CanMapKeysMK mk, ZeroableMK mk) =>
LedgerState blk mk -> LedgerTables blk mk
forall (l :: StateKind) blk (mk :: MapKind).
(HasLedgerTables l blk, CanMapMK mk, CanMapKeysMK mk,
 ZeroableMK mk) =>
l blk mk -> LedgerTables blk mk
projectLedgerTables

infix 4 ==?

-- | The StowableLedgerTables instances should follow these two laws:
--
-- > stow . unstow == id
--
-- > unstow . stow == id
prop_stowable_laws ::
  ( HasLedgerTables LedgerState blk
  , CanStowLedgerTables (LedgerState blk)
  , Show (TxIn blk)
  , Show (TxOut blk)
  ) =>
  LedgerState blk EmptyMK ->
  LedgerState blk ValuesMK ->
  Property
prop_stowable_laws :: forall blk.
(HasLedgerTables LedgerState blk,
 CanStowLedgerTables (LedgerState blk), Show (TxIn blk),
 Show (TxOut blk)) =>
LedgerState blk EmptyMK -> LedgerState blk ValuesMK -> Property
prop_stowable_laws = \LedgerState blk EmptyMK
ls LedgerState blk ValuesMK
ls' ->
  LedgerState blk ValuesMK -> LedgerState blk EmptyMK
forall (l :: LedgerStateKind).
CanStowLedgerTables l =>
l ValuesMK -> l EmptyMK
stowLedgerTables (LedgerState blk EmptyMK -> LedgerState blk ValuesMK
forall (l :: LedgerStateKind).
CanStowLedgerTables l =>
l EmptyMK -> l ValuesMK
unstowLedgerTables LedgerState blk EmptyMK
ls) LedgerState blk EmptyMK -> LedgerState blk EmptyMK -> Property
forall (mk :: MapKind) blk.
(CanMapMK mk, CanMapKeysMK mk, ZeroableMK mk, EqMK mk, ShowMK mk,
 HasLedgerTables LedgerState blk, Show (TxIn blk),
 Show (TxOut blk)) =>
LedgerState blk mk -> LedgerState blk mk -> Property
==? LedgerState blk EmptyMK
ls
    Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. LedgerState blk EmptyMK -> LedgerState blk ValuesMK
forall (l :: LedgerStateKind).
CanStowLedgerTables l =>
l EmptyMK -> l ValuesMK
unstowLedgerTables (LedgerState blk ValuesMK -> LedgerState blk EmptyMK
forall (l :: LedgerStateKind).
CanStowLedgerTables l =>
l ValuesMK -> l EmptyMK
stowLedgerTables LedgerState blk ValuesMK
ls') LedgerState blk ValuesMK -> LedgerState blk ValuesMK -> Property
forall (mk :: MapKind) blk.
(CanMapMK mk, CanMapKeysMK mk, ZeroableMK mk, EqMK mk, ShowMK mk,
 HasLedgerTables LedgerState blk, Show (TxIn blk),
 Show (TxOut blk)) =>
LedgerState blk mk -> LedgerState blk mk -> Property
==? LedgerState blk ValuesMK
ls'

-- | The HasLedgerTables instances should follow these two laws:
--
-- > with . project == id
--
-- > project . with == id
prop_hasledgertables_laws ::
  ( HasLedgerTables LedgerState blk
  , Show (TxIn blk)
  , Show (TxOut blk)
  ) =>
  LedgerState blk EmptyMK ->
  LedgerTables blk ValuesMK ->
  Property
prop_hasledgertables_laws :: forall blk.
(HasLedgerTables LedgerState blk, Show (TxIn blk),
 Show (TxOut blk)) =>
LedgerState blk EmptyMK -> LedgerTables blk ValuesMK -> Property
prop_hasledgertables_laws = \LedgerState blk EmptyMK
ls LedgerTables blk ValuesMK
tbs ->
  (LedgerState blk EmptyMK
ls LedgerState blk EmptyMK
-> LedgerTables blk EmptyMK -> LedgerState blk EmptyMK
forall (mk :: MapKind) (any :: MapKind).
(CanMapMK mk, CanMapKeysMK mk, ZeroableMK mk) =>
LedgerState blk any -> LedgerTables blk mk -> LedgerState blk mk
forall (l :: StateKind) blk (mk :: MapKind) (any :: MapKind).
(HasLedgerTables l blk, CanMapMK mk, CanMapKeysMK mk,
 ZeroableMK mk) =>
l blk any -> LedgerTables blk mk -> l blk mk
`withLedgerTables` (LedgerState blk EmptyMK -> LedgerTables blk EmptyMK
forall (mk :: MapKind).
(CanMapMK mk, CanMapKeysMK mk, ZeroableMK mk) =>
LedgerState blk mk -> LedgerTables blk mk
forall (l :: StateKind) blk (mk :: MapKind).
(HasLedgerTables l blk, CanMapMK mk, CanMapKeysMK mk,
 ZeroableMK mk) =>
l blk mk -> LedgerTables blk mk
projectLedgerTables LedgerState blk EmptyMK
ls)) LedgerState blk EmptyMK -> LedgerState blk EmptyMK -> Property
forall (mk :: MapKind) blk.
(CanMapMK mk, CanMapKeysMK mk, ZeroableMK mk, EqMK mk, ShowMK mk,
 HasLedgerTables LedgerState blk, Show (TxIn blk),
 Show (TxOut blk)) =>
LedgerState blk mk -> LedgerState blk mk -> Property
==? LedgerState blk EmptyMK
ls
    Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. LedgerState blk ValuesMK -> LedgerTables blk ValuesMK
forall (mk :: MapKind).
(CanMapMK mk, CanMapKeysMK mk, ZeroableMK mk) =>
LedgerState blk mk -> LedgerTables blk mk
forall (l :: StateKind) blk (mk :: MapKind).
(HasLedgerTables l blk, CanMapMK mk, CanMapKeysMK mk,
 ZeroableMK mk) =>
l blk mk -> LedgerTables blk mk
projectLedgerTables (LedgerState blk EmptyMK
ls LedgerState blk EmptyMK
-> LedgerTables blk ValuesMK -> LedgerState blk ValuesMK
forall (mk :: MapKind) (any :: MapKind).
(CanMapMK mk, CanMapKeysMK mk, ZeroableMK mk) =>
LedgerState blk any -> LedgerTables blk mk -> LedgerState blk mk
forall (l :: StateKind) blk (mk :: MapKind) (any :: MapKind).
(HasLedgerTables l blk, CanMapMK mk, CanMapKeysMK mk,
 ZeroableMK mk) =>
l blk any -> LedgerTables blk mk -> l blk mk
`withLedgerTables` LedgerTables blk ValuesMK
tbs) LedgerTables blk ValuesMK -> LedgerTables blk ValuesMK -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== LedgerTables blk ValuesMK
tbs