{-# 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 ()
(?!#) = NonEmpty Label -> Bool -> PredicateFailure sts -> Rule sts ctx ()
forall sts (ctx :: RuleType).
NonEmpty Label -> Bool -> PredicateFailure sts -> Rule sts ctx ()
labeledPred (NonEmpty Label -> Bool -> PredicateFailure sts -> Rule sts ctx ())
-> NonEmpty Label
-> Bool
-> PredicateFailure sts
-> Rule sts ctx ()
forall a b. (a -> b) -> a -> b
$ Label
lblStatic Label -> [Label] -> NonEmpty Label
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 ()
(?!#:) = NonEmpty Label
-> Either e () -> (e -> PredicateFailure sts) -> Rule sts ctx ()
forall e sts (ctx :: RuleType).
NonEmpty Label
-> Either e () -> (e -> PredicateFailure sts) -> Rule sts ctx ()
labeledPredE (NonEmpty Label
 -> Either e () -> (e -> PredicateFailure sts) -> Rule sts ctx ())
-> NonEmpty Label
-> Either e ()
-> (e -> PredicateFailure sts)
-> Rule sts ctx ()
forall a b. (a -> b) -> a -> b
$ Label
lblStatic Label -> [Label] -> NonEmpty Label
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 Bool -> PredicateFailure sts -> Rule sts ctx ()
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 = (f era -> PredicateFailure (EraRule rule era))
-> Validation (NonEmpty (f era)) ()
-> F (Clause (EraRule rule era) ctx) ()
forall e sts (ctx :: RuleType).
(e -> PredicateFailure sts)
-> Validation (NonEmpty e) () -> Rule sts ctx ()
validateTrans f era -> PredicateFailure (EraRule rule era)
f era -> EraRuleFailure rule era
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 = (f era -> PredicateFailure (EraRule rule era))
-> NonEmpty Label
-> Validation (NonEmpty (f era)) ()
-> Rule (EraRule rule era) ctx ()
forall e sts (ctx :: RuleType).
(e -> PredicateFailure sts)
-> NonEmpty Label -> Validation (NonEmpty e) () -> Rule sts ctx ()
validateTransLabeled f era -> PredicateFailure (EraRule rule era)
f era -> EraRuleFailure rule era
forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure (NonEmpty Label
 -> Validation (NonEmpty (f era)) ()
 -> Rule (EraRule rule era) ctx ())
-> NonEmpty Label
-> Validation (NonEmpty (f era)) ()
-> Rule (EraRule rule era) ctx ()
forall a b. (a -> b) -> a -> b
$ Label
lblStatic Label -> [Label] -> NonEmpty Label
forall a. a -> [a] -> NonEmpty a
NE.:| []