Transducer.hs

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE QualifiedDo #-}
{-# LANGUAGE TypeApplications #-}
-- @generated by keiro-dsl; do not edit. Regenerated from the .keiro spec.
module Generated.BehaviorComplete.Journey.Transducer
  ( journeyTransducer
  , journeyFoldFingerprint
  , BehaviorOwnership (..)
  , journeyPredicateVerifications
  ) where

import Generated.BehaviorComplete.Journey.Domain
import Data.Text (Text)
import Keiki.Builder qualified as B
import Keiki.Core (HsPred, SymTransducer)
import Keiki.Core qualified as K
import Keiki.Symbolic qualified as S
import Generated.BehaviorComplete.Journey.Expressions qualified as Expressions
import Keiki.Builder ((=:))

journeyTransducer
  :: SymTransducer
       (HsPred JourneyRegs JourneyCommand)
       JourneyRegs
       JourneyVertex
       JourneyCommand
       JourneyEvent
journeyTransducer =
  B.buildTransducer JourneyEmpty initialJourneyRegs isTerminal do
    B.from JourneyEmpty do
      B.onCmd inCtorStart $ \d -> B.do
        B.slot @"lastAmount" =: Expressions.transition1EmptyStartWriteLastAmount d
        B.emit wireStarted (StartedTermFields
          { requestId = d.requestId
          , observedAt = d.observedAt
          , amount = d.amount
          , details = d.details
          })
        B.goto JourneyActive
    B.from JourneyActive do
      B.onCmd inCtorDecide $ \d -> B.do
        B.requireGuard (Expressions.transition2ActiveDecideGuard d)
        B.slot @"lastAmount" =: Expressions.transition2ActiveDecideWriteLastAmount d
        B.emit wireDecisionRecorded (DecisionRecordedTermFields
          { amount = d.amount
          })
        B.goto JourneyActive
      B.onCmd inCtorDecide $ \d -> B.do
        B.requireGuard (Expressions.transition3ActiveDecideGuard d)
        B.slot @"lastAmount" =: Expressions.transition3ActiveDecideWriteLastAmount d
        B.emit wireDecisionRecorded (DecisionRecordedTermFields
          { amount = d.amount
          })
        B.goto JourneyActive
      B.onCmd inCtorPing $ \d -> B.do
        B.noEmit
        B.goto JourneyActive
      B.onCmd inCtorRetire $ \d -> B.do
        B.requireGuard (Expressions.transition5ActiveRetireGuard d)
        B.slot @"lastAmount" =: Expressions.transition5ActiveRetireWriteLastAmount d
        B.emit wireRetired (RetiredTermFields
          { amount = d.amount
          })
        B.emit wireRetirementAudited (RetirementAuditedTermFields
          { amount = d.amount
          })
        B.goto JourneyClosed
      B.onCmd inCtorRetire $ \d -> B.do
        B.replayOnly
        B.requireGuard (Expressions.transition6ActiveRetireGuard d)
        B.slot @"lastAmount" =: Expressions.transition6ActiveRetireWriteLastAmount d
        B.emit wireRetired (RetiredTermFields
          { amount = d.amount
          })
        B.emit wireRetirementAudited (RetirementAuditedTermFields
          { amount = d.amount
          })
        B.goto JourneyClosed
 where
  isTerminal = \case
    JourneyClosed -> True
    _ -> False

journeyFoldFingerprint :: Text
journeyFoldFingerprint = "c5e44f6d33b3dd6f"

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.
journeyPredicateVerifications :: IO [(Text, BehaviorOwnership, S.PredicateVerification)]
journeyPredicateVerifications = sequence
  [ verifyTransition "transition1EmptyStart" GeneratedOwned JourneyEmpty 0
  , verifyTransition "transition2ActiveDecide" GeneratedOwned JourneyActive 0
  , verifyTransition "transition3ActiveDecide" GeneratedOwned JourneyActive 1
  , verifyTransition "transition4ActivePing" GeneratedOwned JourneyActive 2
  , verifyTransition "transition5ActiveRetire" GeneratedOwned JourneyActive 3
  , verifyTransition "transition6ActiveRetire" GeneratedOwned JourneyActive 4
  ]
 where
  verifyTransition label owner source edgeIndex =
    case drop edgeIndex (K.edgesOut journeyTransducer source) of
      K.Edge predicate _ _ _ _ : _ -> (\result -> (label, owner, result)) <$> S.verifyPredicate predicate
      [] -> pure (label, owner, S.UnverifiedSolverFailure "generated transition edge missing")