Transducer.hs

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE QualifiedDo #-}
-- @generated by keiro-dsl 0.18.0.0 (language keiro-dsl 6) from aggregate ReplayTarget; do not edit.
module Generated.CheckedMappingReplay.ReplayTarget.Transducer
  ( replayTargetTransducer
  , replayTargetFoldFingerprint
  , BehaviorOwnership (..)
  , replayTargetPredicateVerifications
  ) where

import Generated.CheckedMappingReplay.ReplayTarget.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 Keiki.Builder ((=:))

replayTargetTransducer
  :: SymTransducer
       (HsPred ReplayTargetRegs ReplayTargetCommand)
       ReplayTargetRegs
       ReplayTargetVertex
       ReplayTargetCommand
       ReplayTargetEvent
replayTargetTransducer =
  B.buildTransducer ReplayTargetReady initialReplayTargetRegs isTerminal do
    B.from ReplayTargetReady do
      B.onCmd inCtorStore $ \d -> B.do
        B.slot @"latest" =: d.envelope
        B.emit wireStored (StoredTermFields
          { retainedId = d.retainedId
          , envelope = d.envelope
          })
        B.goto ReplayTargetReady
 where
  isTerminal = \case

    _ -> False

replayTargetFoldFingerprint :: Text
replayTargetFoldFingerprint = "90fa5667a0617a785985587ae2b487db"

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.
replayTargetPredicateVerifications :: IO [(Text, BehaviorOwnership, S.PredicateVerification)]
replayTargetPredicateVerifications = sequence
  [ verifyTransition "transition1ReadyStore" GeneratedOwned ReplayTargetReady 0
  ]
 where
  verifyTransition label owner source edgeIndex =
    case drop edgeIndex (K.edgesOut replayTargetTransducer source) of
      K.Edge predicate _ _ _ _ : _ -> (\result -> (label, owner, result)) <$> S.verifyPredicate predicate
      [] -> pure (label, owner, S.UnverifiedSolverFailure "generated transition edge missing")