{-# LANGUAGE FlexibleContexts #-}

module Test.LedgerTables
  ( prop_hasledgertables_laws
  , prop_stowable_laws
  ) where

import Data.Function (on)
import Ouroboros.Consensus.Ledger.Basics
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)
  ) =>
  LedgerState blk mk ->
  LedgerState blk mk ->
  Property
==? :: forall (mk :: MapKind) blk.
(CanMapMK mk, CanMapKeysMK mk, ZeroableMK mk, EqMK mk, ShowMK mk,
 HasLedgerTables (LedgerState blk)) =>
LedgerState blk mk -> LedgerState blk mk -> Property
(==?) = LedgerTables (LedgerState blk) mk
-> LedgerTables (LedgerState blk) mk -> Property
forall a. (Eq a, Show a) => a -> a -> Property
(===) (LedgerTables (LedgerState blk) mk
 -> LedgerTables (LedgerState blk) mk -> Property)
-> (LedgerState blk mk -> LedgerTables (LedgerState 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 (LedgerState blk) mk
forall (mk :: MapKind).
(CanMapMK mk, CanMapKeysMK mk, ZeroableMK mk) =>
LedgerState blk mk -> LedgerTables (LedgerState blk) mk
forall (l :: LedgerStateKind) (mk :: MapKind).
(HasLedgerTables l, CanMapMK mk, CanMapKeysMK mk, ZeroableMK mk) =>
l mk -> LedgerTables l 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)
  ) =>
  LedgerState blk EmptyMK ->
  LedgerState blk ValuesMK ->
  Property
prop_stowable_laws :: forall blk.
(HasLedgerTables (LedgerState blk),
 CanStowLedgerTables (LedgerState 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)) =>
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)) =>
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) =>
  LedgerState blk EmptyMK ->
  LedgerTables (LedgerState blk) ValuesMK ->
  Property
prop_hasledgertables_laws :: forall blk.
HasLedgerTables (LedgerState blk) =>
LedgerState blk EmptyMK
-> LedgerTables (LedgerState blk) ValuesMK -> Property
prop_hasledgertables_laws = \LedgerState blk EmptyMK
ls LedgerTables (LedgerState blk) ValuesMK
tbs ->
  (LedgerState blk EmptyMK
ls LedgerState blk EmptyMK
-> LedgerTables (LedgerState blk) EmptyMK
-> LedgerState blk EmptyMK
forall (mk :: MapKind) (any :: MapKind).
(CanMapMK mk, CanMapKeysMK mk, ZeroableMK mk) =>
LedgerState blk any
-> LedgerTables (LedgerState blk) mk -> LedgerState blk mk
forall (l :: LedgerStateKind) (mk :: MapKind) (any :: MapKind).
(HasLedgerTables l, CanMapMK mk, CanMapKeysMK mk, ZeroableMK mk) =>
l any -> LedgerTables l mk -> l mk
`withLedgerTables` (LedgerState blk EmptyMK -> LedgerTables (LedgerState blk) EmptyMK
forall (mk :: MapKind).
(CanMapMK mk, CanMapKeysMK mk, ZeroableMK mk) =>
LedgerState blk mk -> LedgerTables (LedgerState blk) mk
forall (l :: LedgerStateKind) (mk :: MapKind).
(HasLedgerTables l, CanMapMK mk, CanMapKeysMK mk, ZeroableMK mk) =>
l mk -> LedgerTables l 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)) =>
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 (LedgerState blk) ValuesMK
forall (mk :: MapKind).
(CanMapMK mk, CanMapKeysMK mk, ZeroableMK mk) =>
LedgerState blk mk -> LedgerTables (LedgerState blk) mk
forall (l :: LedgerStateKind) (mk :: MapKind).
(HasLedgerTables l, CanMapMK mk, CanMapKeysMK mk, ZeroableMK mk) =>
l mk -> LedgerTables l mk
projectLedgerTables (LedgerState blk EmptyMK
ls LedgerState blk EmptyMK
-> LedgerTables (LedgerState blk) ValuesMK
-> LedgerState blk ValuesMK
forall (mk :: MapKind) (any :: MapKind).
(CanMapMK mk, CanMapKeysMK mk, ZeroableMK mk) =>
LedgerState blk any
-> LedgerTables (LedgerState blk) mk -> LedgerState blk mk
forall (l :: LedgerStateKind) (mk :: MapKind) (any :: MapKind).
(HasLedgerTables l, CanMapMK mk, CanMapKeysMK mk, ZeroableMK mk) =>
l any -> LedgerTables l mk -> l mk
`withLedgerTables` LedgerTables (LedgerState blk) ValuesMK
tbs) LedgerTables (LedgerState blk) ValuesMK
-> LedgerTables (LedgerState blk) ValuesMK -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== LedgerTables (LedgerState blk) ValuesMK
tbs