Transducer.hs

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE QualifiedDo #-}
-- @generated by keiro-dsl 0.15.0.0 (language keiro-dsl 3) from aggregate OrderBook; do not edit.
module Generated.IdDomainMigration.OrderBook.Transducer
  ( orderBookTransducer
  , orderBookFoldFingerprint
  , BehaviorOwnership (..)
  , orderBookPredicateVerifications
  ) where

import Generated.IdDomainMigration.OrderBook.Domain
import Data.Text (Text)
import Generated.IdDomainMigration.Nominals (OrderId)
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 ((=:))

orderBookTransducer
  :: SymTransducer
       (HsPred OrderBookRegs OrderBookCommand)
       OrderBookRegs
       OrderBookVertex
       OrderBookCommand
       OrderBookEvent
orderBookTransducer =
  B.buildTransducer OrderBookEmpty initialOrderBookRegs isTerminal do
    B.from OrderBookEmpty do
      B.onCmd inCtorRecord $ \d -> B.do
        B.slot @"orderId" =: d.orderId
        B.emit wireOrderRecorded (OrderRecordedTermFields
          { orderId = d.orderId
          })
        B.goto OrderBookRecorded
 where
  isTerminal = \case
    OrderBookRecorded -> True
    _ -> False

orderBookFoldFingerprint :: Text
orderBookFoldFingerprint = "d169ad9824b76fafe43c6c86bb601ebd"

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