{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

-- | Describes modes under which we might validate certain rules in the ledger.
--
--   What does this mean? Sometimes, we will want to check only certain
--   conditions specified in the rules. For example, when replaying a previously
--   validated chain, we do not care about rerunning _any_ checks, only making
--   the relevant changes to the ledger state.
module Cardano.Ledger.Rules.ValidationMode (
  -- $static
  lblStatic,
  (?!#),
  (?!#:),
  failBecauseS,

  -- * Interface for independent Tests
  Inject (..),
  Test,
  runTest,
  runTestOnSignal,
)
where

import Cardano.Ledger.BaseTypes (Inject (..))
import Cardano.Ledger.Core
import Control.State.Transition.Extended
import Data.List.NonEmpty (NonEmpty)
import qualified Data.List.NonEmpty as NE
import Validation

--------------------------------------------------------------------------------
-- Static checks
--------------------------------------------------------------------------------

-- * Static checks

--

-- $static
--
-- Static checks are used to indicate that a particular predicate depends only
-- on the signal to the transition, rather than the state or environment. This
-- is particularly relevant where the signal is something such as a transaction,
-- which is fixed, whereas the state and environment depend upon the chain tip
-- upon which we are trying to build a block.

-- | Indicates that this check depends only upon the signal to the transition,
-- not the state or environment.
lblStatic :: Label
lblStatic :: Label
lblStatic = Label
"static"

-- | Construct a static predicate check.
--
--   The choice of '#' as a postfix here is made because often these are crypto
--   checks.
(?!#) :: Bool -> PredicateFailure sts -> Rule sts ctx ()
?!# :: forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
(?!#) = forall sts (ctx :: RuleType).
NonEmpty Label -> Bool -> PredicateFailure sts -> Rule sts ctx ()
labeledPred forall a b. (a -> b) -> a -> b
$ Label
lblStatic forall a. a -> [a] -> NonEmpty a
NE.:| []

infix 1 ?!#

-- | Construct a static predicate check with an explanation.
--
--   The choice of '#' as a postfix here is made because often these are crypto
--   checks.
(?!#:) :: Either e () -> (e -> PredicateFailure sts) -> Rule sts ctx ()
?!#: :: forall e sts (ctx :: RuleType).
Either e () -> (e -> PredicateFailure sts) -> Rule sts ctx ()
(?!#:) = forall e sts (ctx :: RuleType).
NonEmpty Label
-> Either e () -> (e -> PredicateFailure sts) -> Rule sts ctx ()
labeledPredE forall a b. (a -> b) -> a -> b
$ Label
lblStatic forall a. a -> [a] -> NonEmpty a
NE.:| []

infix 1 ?!#:

-- | Fail, if static checks are enabled.
failBecauseS :: PredicateFailure sts -> Rule sts ctx ()
failBecauseS :: forall sts (ctx :: RuleType).
PredicateFailure sts -> Rule sts ctx ()
failBecauseS = (Bool
False forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?!#)

-- ===========================================================

type Test failure = Validation (NonEmpty failure) ()

runTest :: InjectRuleFailure rule f era => Test (f era) -> Rule (EraRule rule era) ctx ()
runTest :: forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTest = forall e sts (ctx :: RuleType).
(e -> PredicateFailure sts)
-> Validation (NonEmpty e) () -> Rule sts ctx ()
validateTrans forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure

runTestOnSignal :: InjectRuleFailure rule f era => Test (f era) -> Rule (EraRule rule era) ctx ()
runTestOnSignal :: forall (rule :: Symbol) (f :: * -> *) era (ctx :: RuleType).
InjectRuleFailure rule f era =>
Test (f era) -> Rule (EraRule rule era) ctx ()
runTestOnSignal = forall e sts (ctx :: RuleType).
(e -> PredicateFailure sts)
-> NonEmpty Label -> Validation (NonEmpty e) () -> Rule sts ctx ()
validateTransLabeled forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure forall a b. (a -> b) -> a -> b
$ Label
lblStatic forall a. a -> [a] -> NonEmpty a
NE.:| []