{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDeriving #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}

module Cardano.Ledger.Core.Era (
  -- * Era
  Era (..),
  ByronEra,

  -- ** Rules
  EraRule,
  EraRuleFailure,
  EraRuleEvent,
  VoidEraRule,
  absurdEraRule,
  InjectRuleFailure (..),
  InjectRuleEvent (..),

  -- ** Protocol Version
  AtMostEra,
  AtLeastEra,
  ExactEra,
  ProtVerAtMost,
  ProtVerAtLeast,
  ProtVerInBounds,
  atLeastEra,
  atMostEra,
  notSupportedInThisEra,
  notSupportedInThisEraL,
  eraProtVerLow,
  eraProtVerHigh,
  toEraCBOR,
  fromEraCBOR,
  fromEraShareCBOR,
  eraDecoder,
)
where

import Cardano.Ledger.Binary
import qualified Cardano.Ledger.Binary.Plain as Plain
import Cardano.Ledger.Crypto
import Control.DeepSeq (NFData (..))
import Control.State.Transition.Extended (PredicateFailure, STS (..))
import Data.Kind (Constraint, Type)
import Data.Typeable (Typeable)
import GHC.Stack (HasCallStack)
import GHC.TypeLits
import Lens.Micro

--------------------------------------------------------------------------------
-- Era
--------------------------------------------------------------------------------

class
  ( Crypto (EraCrypto era)
  , Typeable era
  , KnownNat (ProtVerLow era)
  , KnownNat (ProtVerHigh era)
  , ProtVerLow era <= ProtVerHigh era
  , MinVersion <= ProtVerLow era
  , MinVersion <= ProtVerHigh era
  , -- We need to make sure that there is never a case that MaxVersion equals to the highest
    -- protocol version for the era, otherwise we can never upgrade to the next version:
    CmpNat (ProtVerLow era) MaxVersion ~ 'LT
  , CmpNat (ProtVerHigh era) MaxVersion ~ 'LT
  , -- These two are redundant and can be removed once support for GHC-8.10 is dropped:
    ProtVerLow era <= MaxVersion
  , ProtVerHigh era <= MaxVersion
  ) =>
  Era era
  where
  type EraCrypto era :: Type

  -- | Map an era to its predecessor.
  --
  -- For example:
  --
  -- > type instance PreviousEra (AllegraEra c) = ShelleyEra c
  type PreviousEra era = (r :: Type) | r -> era

  -- | Lowest major protocol version for this era
  type ProtVerLow era :: Nat

  -- | Highest major protocol version for this era. By default se to `ProtVerLow`
  type ProtVerHigh era :: Nat

  type ProtVerHigh era = ProtVerLow era

  -- | Textual name of the current era.
  --
  -- Designed to be used with @TypeApplications@:
  --
  -- >>> eraName @(ByronEra StandardCrypto)
  -- Byron
  eraName :: String

-- | This is the era that preceded Shelley era. It cannot have any other class instances,
-- except for `Era` type class.
data ByronEra c

-- | This is a non-existent era and is defined for satisfying the `PreviousEra` type family injectivity
data VoidEra c

instance Crypto c => Era (ByronEra c) where
  type EraCrypto (ByronEra c) = c
  type PreviousEra (ByronEra c) = VoidEra c
  type ProtVerLow (ByronEra c) = 0
  type ProtVerHigh (ByronEra c) = 1

  eraName :: String
eraName = String
"Byron"

-----------------------------
-- Rules --------------------
-----------------------------

-- | Era STS map
type family EraRule (rule :: Symbol) era = (r :: Type) | r -> rule

-- | `EraRuleFailure` type family is needed for injectivity, which STS' `PredicateFailure`
-- does not provide for us unfortunately.
type family EraRuleFailure (rule :: Symbol) era = (r :: Type) | r -> rule era

type family EraRuleEvent (rule :: Symbol) era = (r :: Type) | r -> rule era

-- | This is a type with no inhabitans for the rules. It is used to indicate that a rule
-- does not have a predicate failure as well as marking rules that have been disabled when
-- comparing to prior eras.
data VoidEraRule (rule :: Symbol) era
  deriving (Int -> VoidEraRule rule era -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (rule :: Symbol) era. Int -> VoidEraRule rule era -> ShowS
forall (rule :: Symbol) era. [VoidEraRule rule era] -> ShowS
forall (rule :: Symbol) era. VoidEraRule rule era -> String
showList :: [VoidEraRule rule era] -> ShowS
$cshowList :: forall (rule :: Symbol) era. [VoidEraRule rule era] -> ShowS
show :: VoidEraRule rule era -> String
$cshow :: forall (rule :: Symbol) era. VoidEraRule rule era -> String
showsPrec :: Int -> VoidEraRule rule era -> ShowS
$cshowsPrec :: forall (rule :: Symbol) era. Int -> VoidEraRule rule era -> ShowS
Show, VoidEraRule rule era -> VoidEraRule rule era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (rule :: Symbol) era.
VoidEraRule rule era -> VoidEraRule rule era -> Bool
/= :: VoidEraRule rule era -> VoidEraRule rule era -> Bool
$c/= :: forall (rule :: Symbol) era.
VoidEraRule rule era -> VoidEraRule rule era -> Bool
== :: VoidEraRule rule era -> VoidEraRule rule era -> Bool
$c== :: forall (rule :: Symbol) era.
VoidEraRule rule era -> VoidEraRule rule era -> Bool
Eq, VoidEraRule rule era -> VoidEraRule rule era -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall (rule :: Symbol) era. Eq (VoidEraRule rule era)
forall (rule :: Symbol) era.
VoidEraRule rule era -> VoidEraRule rule era -> Bool
forall (rule :: Symbol) era.
VoidEraRule rule era -> VoidEraRule rule era -> Ordering
forall (rule :: Symbol) era.
VoidEraRule rule era
-> VoidEraRule rule era -> VoidEraRule rule era
min :: VoidEraRule rule era
-> VoidEraRule rule era -> VoidEraRule rule era
$cmin :: forall (rule :: Symbol) era.
VoidEraRule rule era
-> VoidEraRule rule era -> VoidEraRule rule era
max :: VoidEraRule rule era
-> VoidEraRule rule era -> VoidEraRule rule era
$cmax :: forall (rule :: Symbol) era.
VoidEraRule rule era
-> VoidEraRule rule era -> VoidEraRule rule era
>= :: VoidEraRule rule era -> VoidEraRule rule era -> Bool
$c>= :: forall (rule :: Symbol) era.
VoidEraRule rule era -> VoidEraRule rule era -> Bool
> :: VoidEraRule rule era -> VoidEraRule rule era -> Bool
$c> :: forall (rule :: Symbol) era.
VoidEraRule rule era -> VoidEraRule rule era -> Bool
<= :: VoidEraRule rule era -> VoidEraRule rule era -> Bool
$c<= :: forall (rule :: Symbol) era.
VoidEraRule rule era -> VoidEraRule rule era -> Bool
< :: VoidEraRule rule era -> VoidEraRule rule era -> Bool
$c< :: forall (rule :: Symbol) era.
VoidEraRule rule era -> VoidEraRule rule era -> Bool
compare :: VoidEraRule rule era -> VoidEraRule rule era -> Ordering
$ccompare :: forall (rule :: Symbol) era.
VoidEraRule rule era -> VoidEraRule rule era -> Ordering
Ord)

instance NFData (VoidEraRule (rule :: Symbol) era) where
  rnf :: VoidEraRule rule era -> ()
rnf = forall (rule :: Symbol) era a. VoidEraRule rule era -> a
absurdEraRule

instance (KnownSymbol rule, Era era) => ToCBOR (VoidEraRule (rule :: Symbol) era) where
  toCBOR :: VoidEraRule rule era -> Encoding
toCBOR = forall (rule :: Symbol) era a. VoidEraRule rule era -> a
absurdEraRule

instance (KnownSymbol rule, Era era) => EncCBOR (VoidEraRule (rule :: Symbol) era)

instance (KnownSymbol rule, Era era) => FromCBOR (VoidEraRule (rule :: Symbol) era) where
  fromCBOR :: forall s. Decoder s (VoidEraRule rule era)
fromCBOR = forall (m :: * -> *) e a. (MonadFail m, Buildable e) => e -> m a
cborError DecoderError
DecoderErrorVoid

instance (KnownSymbol rule, Era era) => DecCBOR (VoidEraRule (rule :: Symbol) era)

absurdEraRule :: VoidEraRule rule era -> a
absurdEraRule :: forall (rule :: Symbol) era a. VoidEraRule rule era -> a
absurdEraRule VoidEraRule rule era
a = case VoidEraRule rule era
a of {}

-- Rules that should never have a predicate failures
type instance EraRuleFailure "EPOCH" era = VoidEraRule "EPOCH" era
type instance EraRuleFailure "NEWEPOCH" era = VoidEraRule "NEWEPOCH" era
type instance EraRuleFailure "MIR" era = VoidEraRule "MIR" era
type instance EraRuleFailure "NEWPP" era = VoidEraRule "NEWPP" era
type instance EraRuleFailure "SNAP" era = VoidEraRule "SNAP" era
type instance EraRuleFailure "TICK" era = VoidEraRule "TICK" era
type instance EraRuleFailure "TICKF" era = VoidEraRule "TICKF" era
type instance EraRuleFailure "UPEC" era = VoidEraRule "UPEC" era
type instance EraRuleFailure "RUPD" era = VoidEraRule "RUPD" era
type instance EraRuleFailure "POOLREAP" era = VoidEraRule "POOLREAP" era

class
  EraRuleFailure rule era ~ PredicateFailure (EraRule rule era) =>
  InjectRuleFailure (rule :: Symbol) t era
  where
  injectFailure :: t era -> EraRuleFailure rule era
  default injectFailure :: t era ~ EraRuleFailure rule era => t era -> EraRuleFailure rule era
  injectFailure = forall a. a -> a
id

class
  EraRuleEvent rule era ~ Event (EraRule rule era) =>
  InjectRuleEvent (rule :: Symbol) t era
  where
  injectEvent :: t era -> EraRuleEvent rule era
  default injectEvent :: t era ~ EraRuleEvent rule era => t era -> EraRuleEvent rule era
  injectEvent = forall a. a -> a
id

-----------------------------
-- Protocol version bounds --
-----------------------------

type family ProtVerIsInBounds (check :: Symbol) era (v :: Nat) (b :: Bool) :: Constraint where
  ProtVerIsInBounds check era v 'True = ()
  ProtVerIsInBounds check era v 'False =
    TypeError
      ( 'ShowType era
          ':<>: 'Text " protocol version bounds are: ["
          ':<>: 'ShowType (ProtVerLow era)
          ':<>: 'Text ", "
          ':<>: 'ShowType (ProtVerHigh era)
          ':<>: 'Text "], but required is "
          ':<>: 'Text check
          ':<>: 'Text " "
          ':<>: 'ShowType v
      )

-- | Requirement for the era's highest protocol version to be higher or equal to
-- the supplied value
type family ProtVerAtLeast era (l :: Nat) :: Constraint where
  ProtVerAtLeast era l = ProtVerIsInBounds "at least" era l (l <=? ProtVerHigh era)

-- | Requirement for the era's lowest protocol version to be lower or equal to
-- the supplied value
type family ProtVerAtMost era (h :: Nat) :: Constraint where
  ProtVerAtMost era h = ProtVerIsInBounds "at most" era h (ProtVerLow era <=? h)

-- | Restrict a lower and upper bounds of the protocol version for the particular era
type ProtVerInBounds era l h = (ProtVerAtLeast era l, ProtVerAtMost era h)

-- | Restrict an era to the specific era through the protocol version. This is
-- equivalent to @(inEra (Crypto era) ~ era)@
type ExactEra (inEra :: Type -> Type) era =
  ProtVerInBounds era (ProtVerLow (inEra (EraCrypto era))) (ProtVerHigh (inEra (EraCrypto era)))

-- | Restrict the @era@ to equal to @eraName@ or come after it
type AtLeastEra (eraName :: Type -> Type) era =
  ProtVerAtLeast era (ProtVerLow (eraName (EraCrypto era)))

-- | Restrict the @era@ to equal to @eraName@ or come before it.
type AtMostEra (eraName :: Type -> Type) era =
  ProtVerAtMost era (ProtVerHigh (eraName (EraCrypto era)))

-- | Get the value level `Version` of the lowest major protocol version for the supplied @era@.
eraProtVerLow :: forall era. Era era => Version
eraProtVerLow :: forall era. Era era => Version
eraProtVerLow = forall (v :: Nat).
(KnownNat v, MinVersion <= v, v <= MaxVersion) =>
Version
natVersion @(ProtVerLow era)

-- | Get the value level `Version` of the highest major protocol version for the supplied @era@.
eraProtVerHigh :: forall era. Era era => Version
eraProtVerHigh :: forall era. Era era => Version
eraProtVerHigh = forall (v :: Nat).
(KnownNat v, MinVersion <= v, v <= MaxVersion) =>
Version
natVersion @(ProtVerHigh era)

-- | Enforce era to be at least the specified era at the type level. In other words
-- compiler will produce type error when applied to eras prior to the specified era.
-- This function should be used in order to avoid redundant constraints warning.
--
-- For example these will type check
--
-- >>> atLeastEra @BabbageEra @(ConwayEra StandardCrypto)
-- >>> atLeastEra @BabbageEra @(BabbageEra StandardCrypto)
--
-- However this will result in a type error
--
-- >>> atLeastEra @BabbageEra @(AlonzoEra StandardCrypto)
atLeastEra :: AtLeastEra eraName era => ()
atLeastEra :: forall (eraName :: * -> *) era. AtLeastEra eraName era => ()
atLeastEra = ()

-- | Enforce era to be at most the specified era at the type level. In other words
-- compiler will produce type error when applied to eras prior to the specified era.
-- This function should be used in order to avoid redundant constraints warning.
--
-- For example these will type check
--
-- >>> atMostEra @BabbageEra @(ShelleyEra StandardCrypto)
-- >>> atMostEra @AlonzoEra @(MaryEra StandardCrypto)
--
-- However this will result in a type error
--
-- >>> atMostEra @BabbageEra @(ConwayEra StandardCrypto)
atMostEra :: AtMostEra eraName era => ()
atMostEra :: forall (eraName :: * -> *) era. AtMostEra eraName era => ()
atMostEra = ()

notSupportedInThisEra :: HasCallStack => a
notSupportedInThisEra :: forall a. HasCallStack => a
notSupportedInThisEra = forall a. HasCallStack => String -> a
error String
"Impossible: Function is not supported in this era"

-- Without using `lens` we hit a ghc bug, which results in a redundant constraint warning
notSupportedInThisEraL :: HasCallStack => Lens' a b
notSupportedInThisEraL :: forall a b. HasCallStack => Lens' a b
notSupportedInThisEraL = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens forall a. HasCallStack => a
notSupportedInThisEra forall a. HasCallStack => a
notSupportedInThisEra

-- | Convert a type that implements `EncCBOR` to plain `Plain.Encoding` using the lowest
-- protocol version for the supplied @era@
toEraCBOR :: forall era t. (Era era, EncCBOR t) => t -> Plain.Encoding
toEraCBOR :: forall era t. (Era era, EncCBOR t) => t -> Encoding
toEraCBOR = Version -> Encoding -> Encoding
toPlainEncoding (forall era. Era era => Version
eraProtVerLow @era) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. EncCBOR a => a -> Encoding
encCBOR
{-# INLINE toEraCBOR #-}

-- | Convert a type that implements `DecCBOR` to plain `Plain.Decoder` using the lowest
-- protocol version for the supplied @era@
fromEraCBOR :: forall era t s. (Era era, DecCBOR t) => Plain.Decoder s t
fromEraCBOR :: forall era t s. (Era era, DecCBOR t) => Decoder s t
fromEraCBOR = forall era t s. Era era => Decoder s t -> Decoder s t
eraDecoder @era forall a s. DecCBOR a => Decoder s a
decCBOR
{-# INLINE fromEraCBOR #-}

-- | Convert a type that implements `DecShareCBOR` to plain `Plain.Decoder` using the lowest
-- protocol version for the supplied @era@
fromEraShareCBOR :: forall era t s. (Era era, DecShareCBOR t) => Plain.Decoder s t
fromEraShareCBOR :: forall era t s. (Era era, DecShareCBOR t) => Decoder s t
fromEraShareCBOR = forall era t s. Era era => Decoder s t -> Decoder s t
eraDecoder @era forall a s. DecShareCBOR a => Decoder s a
decNoShareCBOR
{-# INLINE fromEraShareCBOR #-}

-- | Convert a versioned `Decoder` to plain a `Plain.Decoder` using the lowest protocol
-- version for the supplied @era@
eraDecoder :: forall era t s. Era era => Decoder s t -> Plain.Decoder s t
eraDecoder :: forall era t s. Era era => Decoder s t -> Decoder s t
eraDecoder = forall s a. Version -> Decoder s a -> Decoder s a
toPlainDecoder (forall era. Era era => Version
eraProtVerLow @era)
{-# INLINE eraDecoder #-}