Transducer.hs

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE OverloadedLabels #-}
{-# LANGUAGE QualifiedDo #-}
{-# LANGUAGE TypeApplications #-}
-- @generated by keiro-dsl 0.8.0.0 (language keiro-dsl 4) from aggregate Subscription; do not edit.
module Generated.Billing.Subscription.Transducer
  ( subscriptionTransducer
  , subscriptionFoldFingerprint
  , BehaviorOwnership (..)
  , subscriptionPredicateVerifications
  ) where

import Generated.Billing.Subscription.Domain
import Data.Text (Text)
import Generated.Billing.Nominals (Plan (..))
import Generated.Billing.Nominals qualified as GeneratedNominals
import Keiki.Builder qualified as B
import Keiki.Core (HsPred, SymTransducer, (./=))
import Keiki.Core qualified as K
import Keiki.Symbolic qualified as S
import Billing.Subscription.Holes qualified as Holes
import Keiki.Generics (RegFieldsOf)

subscriptionTransducer
  :: SymTransducer
       (HsPred SubscriptionRegs SubscriptionCommand)
       SubscriptionRegs
       SubscriptionVertex
       SubscriptionCommand
       SubscriptionEvent
subscriptionTransducer =
  B.buildTransducer SubscriptionInactive initialSubscriptionRegs isTerminal do
    B.from SubscriptionInactive do
      B.onCmd inCtorActivateSubscription $ \d -> B.do
        let commandPlan = K.inpProj GeneratedNominals.planEqualityWitness inCtorActivateSubscription (#plan :: K.Index (RegFieldsOf ActivateSubscriptionData) Plan)
        B.requireGuard $
          commandPlan ./= K.lit ("free" :: Text)
        B.emit wireSubscriptionActivated (SubscriptionActivatedTermFields
          { subscriptionId = d.subscriptionId
          , customerId = d.customerId
          , plan = d.plan
          })
        B.goto SubscriptionActive
    B.from SubscriptionActive do
      B.onCmd inCtorCancelSubscription $ \d -> B.do
        B.emit wireSubscriptionCancelled (Holes.transition2ActiveCancelSubscriptionOutput1SubscriptionCancelled d)
        B.goto SubscriptionClosed
 where
  isTerminal = \case
    SubscriptionClosed -> True
    _ -> False

subscriptionFoldFingerprint :: Text
subscriptionFoldFingerprint = "8fdbe22f164b53fe045097803ecdfa2c"

data BehaviorOwnership = GeneratedOwned | HoleOwned
  deriving stock (Eq, Show)

-- Every checked transition predicate is audited through Keiki's conservative
-- symbolic verifier. Opaque Hole terms remain explicitly unverified.
subscriptionPredicateVerifications :: IO [(Text, BehaviorOwnership, S.PredicateVerification)]
subscriptionPredicateVerifications = sequence
  [ verifyTransition "transition1InactiveActivateSubscription" GeneratedOwned SubscriptionInactive 0
  , verifyTransition "transition2ActiveCancelSubscription" GeneratedOwned SubscriptionActive 0
  ]
 where
  verifyTransition label owner source edgeIndex =
    case drop edgeIndex (K.edgesOut subscriptionTransducer source) of
      K.Edge predicate _ _ _ _ : _ -> (\result -> (label, owner, result)) <$> S.verifyPredicate predicate
      [] -> pure (label, owner, S.UnverifiedSolverFailure "generated transition edge missing")