{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE DuplicateRecordFields #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

-- | Collection functions and exported symbols to be able to run a
-- 'quickcheck-state-machine' counterexample using the GHC repl.
--
-- To test a counterexample first fire up the repl, and enable the
-- 'FlexibleContexts' and 'TypeFamilies' extensions, and set multi-line input.
--
-- > cabal new-repl test-storage
-- > import Test.Ouroboros.Storage.ChainDB.StateMachine.Utils.RunOnRepl
-- > :set -XFlexibleContexts -XTypeFamilies +m
--
-- The commands that are part of the counterexample are usually several lines
-- long. Thus it is better to create a local definition for them:
--
-- > cmds = (<PASTE THE COMMANDS OF THE COUNTEREXAMPLE HERE>)
--
-- Note the use of parentheses to prevent GHCi from ending the multiline input
-- prematurely (the copied counterexample in this case).
--
-- Then, the model and system under tests can be tested for lockstep agreement
-- by running:
--
-- > quickCheckCmdsLockStep someLoE someClockSkew someChunkInfo counterexample
--
-- Where 'someClockSkew' and 'someChunkInfo' are the ones given by the
-- counterexample found by quickcheck-statemachine, and 'someLoE' is @LoEEnabled
-- ()@ or @LoEDisabled@.
module Test.Ouroboros.Storage.ChainDB.StateMachine.Utils.RunOnRepl (
    -- * Running the counterexamples
    quickCheckCmdsLockStep
    -- * Patterns needed to disambiguate the 'At' and 'Command' symbols printed
    --   by the 'ChainDB.StateMachine' tests.
  , pattern At
  , pattern Command
    -- * Re-exports needed for compiling a 'ChainDB.StateMachine' inside the repl.
    -- ** quickcheck-state-machine re-exports
  , Commands (..)
  , Reference (Reference)
  , Symbolic (Symbolic)
  , Var (Var)
    -- ** ChainDB.StateMachine re-exports
  , Cmd (..)
  , Resp (..)
  , Success (..)
  , runCmdsLockstep
    -- ** Test packages re-exports
  , ChainLength (..)
  , EBB (EBB, RegularBlock)
  , SmallChunkInfo (SmallChunkInfo)
  , TestBlock (..)
  , TestBody (..)
  , TestBodyHash (..)
  , TestHeader (..)
  , TestHeaderHash (..)
    -- ** Ouroboros consensus re-exports
  , Block (..)
  , BlockNo (..)
  , ChainHash (..)
  , ChainType (TentativeChain)
  , ChainUpdate (RollBack)
  , ChunkInfo (..)
  , ChunkSize (..)
  , EpochNo (..)
  , SlotNo (..)
  ) where

import           Ouroboros.Consensus.Block (BlockNo (BlockNo),
                     ChainHash (BlockHash, GenesisHash), EpochNo (EpochNo),
                     SlotNo (SlotNo))
import           Ouroboros.Consensus.Storage.ChainDB
                     (ChainType (TentativeChain), LoE)
import           Ouroboros.Consensus.Storage.ImmutableDB
                     (ChunkInfo (UniformChunkSize),
                     ChunkSize (ChunkSize, chunkCanContainEBB, numRegularBlocks))
import           Ouroboros.Network.Block (ChainUpdate (RollBack))
import qualified Ouroboros.Network.Block as Block
import           Ouroboros.Network.Point (Block (..))
import qualified Ouroboros.Network.Point as Point
import qualified Test.Ouroboros.Storage.ChainDB.StateMachine as StateMachine
import           Test.Ouroboros.Storage.ChainDB.StateMachine (Cmd (..),
                     FollowerRef, IterRef, Resp (..), Success (..),
                     runCmdsLockstep)
import           Test.Ouroboros.Storage.Orphans ()
import           Test.Ouroboros.Storage.TestBlock (ChainLength (ChainLength),
                     EBB (EBB, RegularBlock), TestBlock (..), TestBody (..),
                     TestBodyHash (..), TestHeader (..), TestHeaderHash (..))
import           Test.QuickCheck (quickCheck)
import qualified Test.StateMachine.Types as StateMachine.Types
import           Test.StateMachine.Types (Commands (Commands),
                     Reference (Reference), Symbolic (Symbolic), Var (Var))
import           Test.Util.ChunkInfo (SmallChunkInfo (SmallChunkInfo))
import           Test.Util.Orphans.ToExpr ()

pattern At :: Block SlotNo (Block.HeaderHash blk) -> Block.Point blk
pattern $mAt :: forall {r} {blk}.
Point blk
-> (Block SlotNo (HeaderHash blk) -> r) -> ((# #) -> r) -> r
$bAt :: forall blk. Block SlotNo (HeaderHash blk) -> Point blk
At x = Block.Point (Point.At x)

pattern Command ::
     t1 blk1 (IterRef blk1 m1 Symbolic) (FollowerRef blk1 m1 Symbolic)
  -> t2 blk2 (IterRef blk2 m2 Symbolic) (FollowerRef blk2 m2 Symbolic)
  -> [Var]
  -> StateMachine.Types.Command (StateMachine.At t1 blk1 m1) (StateMachine.At t2 blk2 m2)
pattern $mCommand :: forall {r} {t1 :: * -> * -> * -> *} {blk1} {m1 :: * -> *}
       {t2 :: * -> * -> * -> *} {blk2} {m2 :: * -> *}.
Command (At t1 blk1 m1) (At t2 blk2 m2)
-> (t1
      blk1 (IterRef blk1 m1 Symbolic) (FollowerRef blk1 m1 Symbolic)
    -> t2
         blk2 (IterRef blk2 m2 Symbolic) (FollowerRef blk2 m2 Symbolic)
    -> [Var]
    -> r)
-> ((# #) -> r)
-> r
$bCommand :: forall (t1 :: * -> * -> * -> *) blk1 (m1 :: * -> *)
       (t2 :: * -> * -> * -> *) blk2 (m2 :: * -> *).
t1 blk1 (IterRef blk1 m1 Symbolic) (FollowerRef blk1 m1 Symbolic)
-> t2
     blk2 (IterRef blk2 m2 Symbolic) (FollowerRef blk2 m2 Symbolic)
-> [Var]
-> Command (At t1 blk1 m1) (At t2 blk2 m2)
Command cmd rsp xs =
  StateMachine.Types.Command (StateMachine.At cmd) (StateMachine.At rsp) xs

quickCheckCmdsLockStep ::
     LoE ()
  -> SmallChunkInfo
  -> Commands (StateMachine.At Cmd TestBlock IO) (StateMachine.At Resp TestBlock IO)
  -> IO ()
quickCheckCmdsLockStep :: LoE ()
-> SmallChunkInfo
-> Commands (At Cmd TestBlock IO) (At Resp TestBlock IO)
-> IO ()
quickCheckCmdsLockStep LoE ()
loe SmallChunkInfo
chunkInfo Commands (At Cmd TestBlock IO) (At Resp TestBlock IO)
cmds =
  Property -> IO ()
forall prop. Testable prop => prop -> IO ()
quickCheck (Property -> IO ()) -> Property -> IO ()
forall a b. (a -> b) -> a -> b
$ LoE ()
-> SmallChunkInfo
-> Commands (At Cmd TestBlock IO) (At Resp TestBlock IO)
-> Property
runCmdsLockstep LoE ()
loe SmallChunkInfo
chunkInfo Commands (At Cmd TestBlock IO) (At Resp TestBlock IO)
cmds