Transducer.hs

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE QualifiedDo #-}
{-# LANGUAGE TypeApplications #-}
-- @generated by keiro-dsl 0.8.0.0 (language keiro-dsl 4) from aggregate Thing; do not edit.
module SkelAggregate.Generated.MyService.Thing.Transducer
  ( thingTransducer
  , thingFoldFingerprint
  , BehaviorOwnership (..)
  , thingPredicateVerifications
  ) where

import SkelAggregate.Generated.MyService.Thing.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 SkelAggregate.MyService.Thing.Holes qualified as Holes

thingTransducer
  :: SymTransducer
       (HsPred ThingRegs ThingCommand)
       ThingRegs
       ThingVertex
       ThingCommand
       ThingEvent
thingTransducer =
  B.buildTransducer ThingPending initialThingRegs isTerminal do
    B.from ThingPending do
      B.onCmd inCtorDoThing $ \d -> B.do
        B.emit wireThingCompleted (Holes.transition1PendingDoThingOutput1ThingCompleted d)
        B.goto ThingDone
 where
  isTerminal = \case
    ThingDone -> True
    _ -> False

thingFoldFingerprint :: Text
thingFoldFingerprint = "79409d44f75b30358aac38c78863ca4e"

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