{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}

module Byron.Spec.Chain.STS.Rule.Bupi where

import Byron.Spec.Ledger.Core (VKey)
import Byron.Spec.Ledger.Update (ProtVer, UPIEND, UPIEnv, UPIREG, UPIState, UPIVOTES, UProp, Vote)
import Control.State.Transition (
  Embed,
  Environment,
  PredicateFailure,
  STS (..),
  Signal,
  State,
  TRC (TRC),
  TransitionRule,
  initialRules,
  judgmentContext,
  trans,
  transitionRules,
  wrapFailed,
 )
import Data.Data (Data)

type UpdatePayload =
  ( Maybe UProp
  , [Vote]
  , (ProtVer, VKey)
  )

data BUPI deriving (Typeable BUPI
Typeable BUPI =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> BUPI -> c BUPI)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c BUPI)
-> (BUPI -> Constr)
-> (BUPI -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c BUPI))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BUPI))
-> ((forall b. Data b => b -> b) -> BUPI -> BUPI)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BUPI -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BUPI -> r)
-> (forall u. (forall d. Data d => d -> u) -> BUPI -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> BUPI -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> BUPI -> m BUPI)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> BUPI -> m BUPI)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> BUPI -> m BUPI)
-> Data BUPI
BUPI -> Constr
BUPI -> DataType
(forall b. Data b => b -> b) -> BUPI -> BUPI
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> BUPI -> u
forall u. (forall d. Data d => d -> u) -> BUPI -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BUPI -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BUPI -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BUPI -> m BUPI
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BUPI -> m BUPI
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BUPI
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BUPI -> c BUPI
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BUPI)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BUPI)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BUPI -> c BUPI
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BUPI -> c BUPI
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BUPI
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BUPI
$ctoConstr :: BUPI -> Constr
toConstr :: BUPI -> Constr
$cdataTypeOf :: BUPI -> DataType
dataTypeOf :: BUPI -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BUPI)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BUPI)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BUPI)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BUPI)
$cgmapT :: (forall b. Data b => b -> b) -> BUPI -> BUPI
gmapT :: (forall b. Data b => b -> b) -> BUPI -> BUPI
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BUPI -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BUPI -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BUPI -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BUPI -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> BUPI -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> BUPI -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> BUPI -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> BUPI -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BUPI -> m BUPI
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> BUPI -> m BUPI
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BUPI -> m BUPI
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BUPI -> m BUPI
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BUPI -> m BUPI
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> BUPI -> m BUPI
Data)

data BupiPredicateFailure
  = UPIREGFailure (PredicateFailure UPIREG)
  | UPIVOTESFailure (PredicateFailure UPIVOTES)
  | UPIENDFailure (PredicateFailure UPIEND)
  deriving (BupiPredicateFailure -> BupiPredicateFailure -> Bool
(BupiPredicateFailure -> BupiPredicateFailure -> Bool)
-> (BupiPredicateFailure -> BupiPredicateFailure -> Bool)
-> Eq BupiPredicateFailure
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BupiPredicateFailure -> BupiPredicateFailure -> Bool
== :: BupiPredicateFailure -> BupiPredicateFailure -> Bool
$c/= :: BupiPredicateFailure -> BupiPredicateFailure -> Bool
/= :: BupiPredicateFailure -> BupiPredicateFailure -> Bool
Eq, Int -> BupiPredicateFailure -> ShowS
[BupiPredicateFailure] -> ShowS
BupiPredicateFailure -> String
(Int -> BupiPredicateFailure -> ShowS)
-> (BupiPredicateFailure -> String)
-> ([BupiPredicateFailure] -> ShowS)
-> Show BupiPredicateFailure
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BupiPredicateFailure -> ShowS
showsPrec :: Int -> BupiPredicateFailure -> ShowS
$cshow :: BupiPredicateFailure -> String
show :: BupiPredicateFailure -> String
$cshowList :: [BupiPredicateFailure] -> ShowS
showList :: [BupiPredicateFailure] -> ShowS
Show, Typeable BupiPredicateFailure
Typeable BupiPredicateFailure =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g)
 -> BupiPredicateFailure
 -> c BupiPredicateFailure)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c BupiPredicateFailure)
-> (BupiPredicateFailure -> Constr)
-> (BupiPredicateFailure -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c BupiPredicateFailure))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c BupiPredicateFailure))
-> ((forall b. Data b => b -> b)
    -> BupiPredicateFailure -> BupiPredicateFailure)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> BupiPredicateFailure -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> BupiPredicateFailure -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> BupiPredicateFailure -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> BupiPredicateFailure -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> BupiPredicateFailure -> m BupiPredicateFailure)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> BupiPredicateFailure -> m BupiPredicateFailure)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> BupiPredicateFailure -> m BupiPredicateFailure)
-> Data BupiPredicateFailure
BupiPredicateFailure -> Constr
BupiPredicateFailure -> DataType
(forall b. Data b => b -> b)
-> BupiPredicateFailure -> BupiPredicateFailure
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> BupiPredicateFailure -> u
forall u.
(forall d. Data d => d -> u) -> BupiPredicateFailure -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BupiPredicateFailure -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BupiPredicateFailure -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> BupiPredicateFailure -> m BupiPredicateFailure
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> BupiPredicateFailure -> m BupiPredicateFailure
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BupiPredicateFailure
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> BupiPredicateFailure
-> c BupiPredicateFailure
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BupiPredicateFailure)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c BupiPredicateFailure)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> BupiPredicateFailure
-> c BupiPredicateFailure
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> BupiPredicateFailure
-> c BupiPredicateFailure
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BupiPredicateFailure
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c BupiPredicateFailure
$ctoConstr :: BupiPredicateFailure -> Constr
toConstr :: BupiPredicateFailure -> Constr
$cdataTypeOf :: BupiPredicateFailure -> DataType
dataTypeOf :: BupiPredicateFailure -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BupiPredicateFailure)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c BupiPredicateFailure)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c BupiPredicateFailure)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c BupiPredicateFailure)
$cgmapT :: (forall b. Data b => b -> b)
-> BupiPredicateFailure -> BupiPredicateFailure
gmapT :: (forall b. Data b => b -> b)
-> BupiPredicateFailure -> BupiPredicateFailure
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BupiPredicateFailure -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BupiPredicateFailure -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BupiPredicateFailure -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BupiPredicateFailure -> r
$cgmapQ :: forall u.
(forall d. Data d => d -> u) -> BupiPredicateFailure -> [u]
gmapQ :: forall u.
(forall d. Data d => d -> u) -> BupiPredicateFailure -> [u]
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> BupiPredicateFailure -> u
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> BupiPredicateFailure -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> BupiPredicateFailure -> m BupiPredicateFailure
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> BupiPredicateFailure -> m BupiPredicateFailure
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> BupiPredicateFailure -> m BupiPredicateFailure
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> BupiPredicateFailure -> m BupiPredicateFailure
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> BupiPredicateFailure -> m BupiPredicateFailure
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> BupiPredicateFailure -> m BupiPredicateFailure
Data)

instance STS BUPI where
  type Environment BUPI = UPIEnv

  type State BUPI = UPIState

  type Signal BUPI = UpdatePayload

  type PredicateFailure BUPI = BupiPredicateFailure

  initialRules :: [InitialRule BUPI]
initialRules = []

  transitionRules :: [TransitionRule BUPI]
transitionRules =
    [ do
        TRC (Environment BUPI
_, State BUPI
_, (Maybe UProp
mProp, [Vote]
_, (ProtVer, VKey)
_)) <- Rule BUPI 'Transition (RuleContext 'Transition BUPI)
F (Clause BUPI 'Transition) (TRC BUPI)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        case Maybe UProp
mProp of
          Just UProp
prop -> UProp -> TransitionRule BUPI
hasProposalRule UProp
prop
          Maybe UProp
Nothing -> F (Clause BUPI 'Transition) UPIState
TransitionRule BUPI
noProposalRule
    ]
    where
      hasProposalRule :: UProp -> TransitionRule BUPI
      hasProposalRule :: UProp -> TransitionRule BUPI
hasProposalRule UProp
prop = do
        TRC (Environment BUPI
env, State BUPI
us, (Maybe UProp
_, [Vote]
votes, (ProtVer, VKey)
end)) <- Rule BUPI 'Transition (RuleContext 'Transition BUPI)
F (Clause BUPI 'Transition) (TRC BUPI)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        UPIState
us' <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @UPIREG (RuleContext 'Transition UPIREG
 -> Rule BUPI 'Transition (State UPIREG))
-> RuleContext 'Transition UPIREG
-> Rule BUPI 'Transition (State UPIREG)
forall a b. (a -> b) -> a -> b
$ (Environment UPIREG, State UPIREG, Signal UPIREG) -> TRC UPIREG
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment UPIREG
Environment BUPI
env, State UPIREG
State BUPI
us, UProp
Signal UPIREG
prop)
        UPIState
us'' <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @UPIVOTES (RuleContext 'Transition UPIVOTES
 -> Rule BUPI 'Transition (State UPIVOTES))
-> RuleContext 'Transition UPIVOTES
-> Rule BUPI 'Transition (State UPIVOTES)
forall a b. (a -> b) -> a -> b
$ (Environment UPIVOTES, State UPIVOTES, Signal UPIVOTES)
-> TRC UPIVOTES
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment UPIVOTES
Environment BUPI
env, UPIState
State UPIVOTES
us', [Vote]
Signal UPIVOTES
votes)
        UPIState
us''' <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @UPIEND (RuleContext 'Transition UPIEND
 -> Rule BUPI 'Transition (State UPIEND))
-> RuleContext 'Transition UPIEND
-> Rule BUPI 'Transition (State UPIEND)
forall a b. (a -> b) -> a -> b
$ (Environment UPIEND, State UPIEND, Signal UPIEND) -> TRC UPIEND
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment UPIEND
Environment BUPI
env, UPIState
State UPIEND
us'', (ProtVer, VKey)
Signal UPIEND
end)
        UPIState -> F (Clause BUPI 'Transition) UPIState
forall a. a -> F (Clause BUPI 'Transition) a
forall (m :: * -> *) a. Monad m => a -> m a
return (UPIState -> F (Clause BUPI 'Transition) UPIState)
-> UPIState -> F (Clause BUPI 'Transition) UPIState
forall a b. (a -> b) -> a -> b
$! UPIState
us'''

      noProposalRule :: TransitionRule BUPI
      noProposalRule :: TransitionRule BUPI
noProposalRule = do
        TRC (Environment BUPI
env, State BUPI
us, (Maybe UProp
_, [Vote]
votes, (ProtVer, VKey)
end)) <- Rule BUPI 'Transition (RuleContext 'Transition BUPI)
F (Clause BUPI 'Transition) (TRC BUPI)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        UPIState
us' <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @UPIVOTES (RuleContext 'Transition UPIVOTES
 -> Rule BUPI 'Transition (State UPIVOTES))
-> RuleContext 'Transition UPIVOTES
-> Rule BUPI 'Transition (State UPIVOTES)
forall a b. (a -> b) -> a -> b
$ (Environment UPIVOTES, State UPIVOTES, Signal UPIVOTES)
-> TRC UPIVOTES
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment UPIVOTES
Environment BUPI
env, State UPIVOTES
State BUPI
us, [Vote]
Signal UPIVOTES
votes)
        UPIState
us'' <- forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @UPIEND (RuleContext 'Transition UPIEND
 -> Rule BUPI 'Transition (State UPIEND))
-> RuleContext 'Transition UPIEND
-> Rule BUPI 'Transition (State UPIEND)
forall a b. (a -> b) -> a -> b
$ (Environment UPIEND, State UPIEND, Signal UPIEND) -> TRC UPIEND
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment UPIEND
Environment BUPI
env, UPIState
State UPIEND
us', (ProtVer, VKey)
Signal UPIEND
end)
        UPIState -> F (Clause BUPI 'Transition) UPIState
forall a. a -> F (Clause BUPI 'Transition) a
forall (m :: * -> *) a. Monad m => a -> m a
return (UPIState -> F (Clause BUPI 'Transition) UPIState)
-> UPIState -> F (Clause BUPI 'Transition) UPIState
forall a b. (a -> b) -> a -> b
$! UPIState
us''

instance Embed UPIREG BUPI where
  wrapFailed :: PredicateFailure UPIREG -> PredicateFailure BUPI
wrapFailed = PredicateFailure UPIREG -> PredicateFailure BUPI
PredicateFailure UPIREG -> BupiPredicateFailure
UPIREGFailure

instance Embed UPIVOTES BUPI where
  wrapFailed :: PredicateFailure UPIVOTES -> PredicateFailure BUPI
wrapFailed = PredicateFailure UPIVOTES -> PredicateFailure BUPI
PredicateFailure UPIVOTES -> BupiPredicateFailure
UPIVOTESFailure

instance Embed UPIEND BUPI where
  wrapFailed :: PredicateFailure UPIEND -> PredicateFailure BUPI
wrapFailed = PredicateFailure UPIEND -> PredicateFailure BUPI
PredicateFailure UPIEND -> BupiPredicateFailure
UPIENDFailure