{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Ouroboros.Consensus.Block.NestedContent (
    -- * Block contents
    HasNestedContent (..)
  , NestedCtxt_
  , curriedNest
    -- * Flip type arguments
  , NestedCtxt (..)
  , castNestedCtxt
  , mapNestedCtxt
    -- * Existentials
  , castSomeNestedCtxt
  , mapSomeNestedCtxt
    -- * Convenience re-exports
  , module Ouroboros.Consensus.Util.DepPair
  , SomeSecond (..)
  ) where

import           Data.Kind (Type)
import           Data.Maybe (isJust)
import           Data.Proxy
import           Data.Type.Equality
import           Data.Typeable (Typeable)
import           NoThunks.Class (InspectHeap (..), NoThunks)
import           Ouroboros.Consensus.Util (SomeSecond (..))
import           Ouroboros.Consensus.Util.DepPair

{-------------------------------------------------------------------------------
  Block contents
-------------------------------------------------------------------------------}

-- | Nested content inside a block
--
-- Consider a simplified version of the hard fork combinator, defining
--
-- > type HardFork a b = Either a b
--
-- Then encoding @Hardfork ByronBlock ShelleyBlock@ is easy, in the same way
-- that we encode /any/ @Either@. The /header/ of such a block will have type
--
-- > HardFork (Header ByronBlock) (Header ShelleyBlock)
--
-- and encoding those (for example, to send them across the network) is
-- similarly trivial. But now suppose we want to read a header from disk. We do
-- not store headers directly, but instead store the blocks. The DB will know
-- the offset and length (both in bytes) of the header inside the block, but
-- how do we decode such a header? If it's a Byron block, we should use the
-- decoder for @Header ByronBlock@, and similarly for Shelley, but how should
-- we express this more generally?
--
-- Here is where 'HasNestedContent' comes in. Continuing the example, we can
-- @unnest@ a @Header (HardFork ByronBlock ShelleyBlock)@ into a pair of values,
-- where the first value (a @NestedCtxt@) tells us what type of block we have,
-- and the second value gives us the actual header. So, if the first value says
-- "this is a Byron block", the second value is a @Header ByronBlock@, and vice
-- versa. In other words, this is a dependent pair.
--
-- This then solves the serialisation problem: we expect a /dependent/ decoder
-- which, /given/ a @NestedCtxt@ identifying the block type, decodes the raw
-- bytes from the block into the type indicated by that @NestedCtxt@.
--
-- TODO: We could perhaps define this independent of blocks in 'DepPair'.
class ( forall a. Show (NestedCtxt_ blk f a)
      , SameDepIndex (NestedCtxt_ blk f)
      ) => HasNestedContent f blk where
  unnest :: f blk -> DepPair (NestedCtxt f blk)
  nest   :: DepPair (NestedCtxt f blk) -> f blk

  -- Defaults when there is only a single type

  default unnest :: ( TrivialDependency (NestedCtxt f blk)
                    , TrivialIndex (NestedCtxt f blk) ~ f blk
                    )
                 => f blk -> DepPair (NestedCtxt f blk)
  unnest = NestedCtxt f blk (f blk) -> f blk -> DepPair (NestedCtxt f blk)
forall (f :: * -> *) a. f a -> a -> DepPair f
DepPair NestedCtxt f blk (f blk)
NestedCtxt f blk (TrivialIndex (NestedCtxt f blk))
forall (f :: * -> *). TrivialDependency f => f (TrivialIndex f)
indexIsTrivial

  default nest :: ( TrivialDependency (NestedCtxt f blk)
                  , TrivialIndex (NestedCtxt f blk) ~ f blk
                  )
               => DepPair (NestedCtxt f blk) -> f blk
  nest (DepPair NestedCtxt f blk a
x a
y) = NestedCtxt f blk a -> a -> TrivialIndex (NestedCtxt f blk)
forall (f :: * -> *) a.
TrivialDependency f =>
f a -> a -> TrivialIndex f
fromTrivialDependency NestedCtxt f blk a
x a
y

curriedNest :: HasNestedContent f blk => NestedCtxt f blk a -> a -> f blk
curriedNest :: forall (f :: * -> *) blk a.
HasNestedContent f blk =>
NestedCtxt f blk a -> a -> f blk
curriedNest NestedCtxt f blk a
ctxt a
a = DepPair (NestedCtxt f blk) -> f blk
forall (f :: * -> *) blk.
HasNestedContent f blk =>
DepPair (NestedCtxt f blk) -> f blk
nest (NestedCtxt f blk a -> a -> DepPair (NestedCtxt f blk)
forall (f :: * -> *) a. f a -> a -> DepPair f
DepPair NestedCtxt f blk a
ctxt a
a)

-- | Context identifying what kind of block we have
--
-- In almost all places we will use 'NestedCtxt' rather than 'NestedCtxt_'.
data family NestedCtxt_ blk :: (Type -> Type) -> (Type -> Type)

{-------------------------------------------------------------------------------
  Flip arguments
-------------------------------------------------------------------------------}

-- | Version of 'NestedCtxt_' with the type arguments swapped
--
-- 'NestedCtxt' must be indexed on @blk@: it is the block that determines this
-- type. However, we often want to partially apply the second argument (the
-- functor), leaving the block type not yet defined.
newtype NestedCtxt f blk a = NestedCtxt {
      forall (f :: * -> *) blk a.
NestedCtxt f blk a -> NestedCtxt_ blk f a
flipNestedCtxt :: NestedCtxt_ blk f a
    }

deriving instance Show (NestedCtxt_ blk f a)
               => Show (NestedCtxt f blk a)

instance SameDepIndex (NestedCtxt_ blk f)
      => SameDepIndex (NestedCtxt f blk) where
  sameDepIndex :: forall a b.
NestedCtxt f blk a -> NestedCtxt f blk b -> Maybe (a :~: b)
sameDepIndex (NestedCtxt NestedCtxt_ blk f a
ctxt) (NestedCtxt NestedCtxt_ blk f b
ctxt') =
      NestedCtxt_ blk f a -> NestedCtxt_ blk f b -> Maybe (a :~: b)
forall a b.
NestedCtxt_ blk f a -> NestedCtxt_ blk f b -> Maybe (a :~: b)
forall (f :: * -> *) a b.
SameDepIndex f =>
f a -> f b -> Maybe (a :~: b)
sameDepIndex NestedCtxt_ blk f a
ctxt NestedCtxt_ blk f b
ctxt'

instance TrivialDependency (NestedCtxt_ blk f)
      => TrivialDependency (NestedCtxt f blk) where
  type TrivialIndex (NestedCtxt f blk) = TrivialIndex (NestedCtxt_ blk f)
  hasSingleIndex :: forall a b. NestedCtxt f blk a -> NestedCtxt f blk b -> a :~: b
hasSingleIndex (NestedCtxt NestedCtxt_ blk f a
ctxt) (NestedCtxt NestedCtxt_ blk f b
ctxt') =
      NestedCtxt_ blk f a -> NestedCtxt_ blk f b -> a :~: b
forall a b. NestedCtxt_ blk f a -> NestedCtxt_ blk f b -> a :~: b
forall (f :: * -> *) a b.
TrivialDependency f =>
f a -> f b -> a :~: b
hasSingleIndex NestedCtxt_ blk f a
ctxt NestedCtxt_ blk f b
ctxt'
  indexIsTrivial :: NestedCtxt f blk (TrivialIndex (NestedCtxt f blk))
indexIsTrivial =
      NestedCtxt_ blk f (TrivialIndex (NestedCtxt_ blk f))
-> NestedCtxt f blk (TrivialIndex (NestedCtxt_ blk f))
forall (f :: * -> *) blk a.
NestedCtxt_ blk f a -> NestedCtxt f blk a
NestedCtxt NestedCtxt_ blk f (TrivialIndex (NestedCtxt_ blk f))
forall (f :: * -> *). TrivialDependency f => f (TrivialIndex f)
indexIsTrivial

castNestedCtxt :: (NestedCtxt_ blk f a -> NestedCtxt_ blk' f a)
               -> NestedCtxt f blk  a
               -> NestedCtxt f blk' a
castNestedCtxt :: forall blk (f :: * -> *) a blk'.
(NestedCtxt_ blk f a -> NestedCtxt_ blk' f a)
-> NestedCtxt f blk a -> NestedCtxt f blk' a
castNestedCtxt NestedCtxt_ blk f a -> NestedCtxt_ blk' f a
coerce (NestedCtxt NestedCtxt_ blk f a
ctxt) = NestedCtxt_ blk' f a -> NestedCtxt f blk' a
forall (f :: * -> *) blk a.
NestedCtxt_ blk f a -> NestedCtxt f blk a
NestedCtxt (NestedCtxt_ blk f a -> NestedCtxt_ blk' f a
coerce NestedCtxt_ blk f a
ctxt)

mapNestedCtxt :: (NestedCtxt_ blk f a -> NestedCtxt_ blk' f' a')
              -> NestedCtxt f  blk  a
              -> NestedCtxt f' blk' a'
mapNestedCtxt :: forall blk (f :: * -> *) a blk' (f' :: * -> *) a'.
(NestedCtxt_ blk f a -> NestedCtxt_ blk' f' a')
-> NestedCtxt f blk a -> NestedCtxt f' blk' a'
mapNestedCtxt NestedCtxt_ blk f a -> NestedCtxt_ blk' f' a'
f (NestedCtxt NestedCtxt_ blk f a
ctxt) = NestedCtxt_ blk' f' a' -> NestedCtxt f' blk' a'
forall (f :: * -> *) blk a.
NestedCtxt_ blk f a -> NestedCtxt f blk a
NestedCtxt (NestedCtxt_ blk f a -> NestedCtxt_ blk' f' a'
f NestedCtxt_ blk f a
ctxt)

deriving instance (HasNestedContent f blk, forall a. Show (g a))
               => Show (GenDepPair g (NestedCtxt f blk))

{-------------------------------------------------------------------------------
  Existentials
-------------------------------------------------------------------------------}

deriving instance HasNestedContent f blk => Show (SomeSecond (NestedCtxt f) blk)

-- | We can write a manual instance using the following quantified constraint:
--
-- > forall a. NoThunks (f blk a)
--
-- However, this constraint would have to be propagated all the way up, which is
-- rather verbose and annoying (standalone deriving has to be used), hence we
-- use 'InspectHeap' for convenience.
deriving via InspectHeap (SomeSecond (NestedCtxt f) blk)
  instance (Typeable f, Typeable blk) => NoThunks (SomeSecond (NestedCtxt f) blk)

instance SameDepIndex (NestedCtxt_ blk f)
      => Eq (SomeSecond (NestedCtxt f) blk) where
  SomeSecond NestedCtxt f blk b
ctxt == :: SomeSecond (NestedCtxt f) blk
-> SomeSecond (NestedCtxt f) blk -> Bool
== SomeSecond NestedCtxt f blk b
ctxt' = Maybe (b :~: b) -> Bool
forall a. Maybe a -> Bool
isJust (NestedCtxt f blk b -> NestedCtxt f blk b -> Maybe (b :~: b)
forall a b.
NestedCtxt f blk a -> NestedCtxt f blk b -> Maybe (a :~: b)
forall (f :: * -> *) a b.
SameDepIndex f =>
f a -> f b -> Maybe (a :~: b)
sameDepIndex NestedCtxt f blk b
ctxt NestedCtxt f blk b
ctxt')

castSomeNestedCtxt :: (forall a. NestedCtxt_ blk f a -> NestedCtxt_ blk' f a)
                   -> SomeSecond (NestedCtxt f) blk
                   -> SomeSecond (NestedCtxt f) blk'
castSomeNestedCtxt :: forall blk (f :: * -> *) blk'.
(forall a. NestedCtxt_ blk f a -> NestedCtxt_ blk' f a)
-> SomeSecond (NestedCtxt f) blk -> SomeSecond (NestedCtxt f) blk'
castSomeNestedCtxt forall a. NestedCtxt_ blk f a -> NestedCtxt_ blk' f a
coerce (SomeSecond NestedCtxt f blk b
ctxt) = NestedCtxt f blk' b -> SomeSecond (NestedCtxt f) blk'
forall {k1} {k2} (f :: k1 -> k2 -> *) (a :: k1) (b :: k2).
f a b -> SomeSecond f a
SomeSecond ((NestedCtxt_ blk f b -> NestedCtxt_ blk' f b)
-> NestedCtxt f blk b -> NestedCtxt f blk' b
forall blk (f :: * -> *) a blk'.
(NestedCtxt_ blk f a -> NestedCtxt_ blk' f a)
-> NestedCtxt f blk a -> NestedCtxt f blk' a
castNestedCtxt NestedCtxt_ blk f b -> NestedCtxt_ blk' f b
forall a. NestedCtxt_ blk f a -> NestedCtxt_ blk' f a
coerce NestedCtxt f blk b
ctxt)

mapSomeNestedCtxt :: (forall a. NestedCtxt_ blk f a -> NestedCtxt_ blk' f' a)
                  -> SomeSecond (NestedCtxt f)  blk
                  -> SomeSecond (NestedCtxt f') blk'
mapSomeNestedCtxt :: forall blk (f :: * -> *) blk' (f' :: * -> *).
(forall a. NestedCtxt_ blk f a -> NestedCtxt_ blk' f' a)
-> SomeSecond (NestedCtxt f) blk -> SomeSecond (NestedCtxt f') blk'
mapSomeNestedCtxt forall a. NestedCtxt_ blk f a -> NestedCtxt_ blk' f' a
f (SomeSecond NestedCtxt f blk b
ctxt) = NestedCtxt f' blk' b -> SomeSecond (NestedCtxt f') blk'
forall {k1} {k2} (f :: k1 -> k2 -> *) (a :: k1) (b :: k2).
f a b -> SomeSecond f a
SomeSecond ((NestedCtxt_ blk f b -> NestedCtxt_ blk' f' b)
-> NestedCtxt f blk b -> NestedCtxt f' blk' b
forall blk (f :: * -> *) a blk' (f' :: * -> *) a'.
(NestedCtxt_ blk f a -> NestedCtxt_ blk' f' a')
-> NestedCtxt f blk a -> NestedCtxt f' blk' a'
mapNestedCtxt NestedCtxt_ blk f b -> NestedCtxt_ blk' f' b
forall a. NestedCtxt_ blk f a -> NestedCtxt_ blk' f' a
f NestedCtxt f blk b
ctxt)