Transducer.hs

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE QualifiedDo #-}
-- @generated by keiro-dsl 0.9.0.0 (language keiro-dsl 4) from aggregate CollisionLedger; do not edit.
module Generated.ImportPlanningCollisions.CollisionLedger.Transducer
  ( collisionLedgerTransducer
  , collisionLedgerFoldFingerprint
  , BehaviorOwnership (..)
  , collisionLedgerPredicateVerifications
  ) where

import Generated.ImportPlanningCollisions.CollisionLedger.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

collisionLedgerTransducer
  :: SymTransducer
       (HsPred CollisionLedgerRegs CollisionLedgerCommand)
       CollisionLedgerRegs
       CollisionLedgerVertex
       CollisionLedgerCommand
       CollisionLedgerEvent
collisionLedgerTransducer =
  B.buildTransducer CollisionLedgerEmpty initialCollisionLedgerRegs isTerminal do
    B.from CollisionLedgerEmpty do
      B.onCmd inCtorRecord $ \d -> B.do
        B.emit wireRecordedValues (RecordedValuesTermFields
          { orderStatus = d.orderStatus
          , invoiceStatus = d.invoiceStatus
          , localCollision = d.localCollision
          , details = d.details
          })
        B.goto CollisionLedgerRecorded
 where
  isTerminal = \case
    CollisionLedgerRecorded -> True
    _ -> False

collisionLedgerFoldFingerprint :: Text
collisionLedgerFoldFingerprint = "50d5e219d56ca914fb73dc08b51ab6f1"

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