Transducer.hs

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE QualifiedDo #-}
-- @generated by keiro-dsl 0.12.0.0 (language keiro-dsl 5) from aggregate Shipments; do not edit.
module Generated.CatalogDemo.Shipments.Transducer
  ( shipmentsTransducer
  , shipmentsFoldFingerprint
  , BehaviorOwnership (..)
  , shipmentsPredicateVerifications
  ) where

import Generated.CatalogDemo.Shipments.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 ((=:))

shipmentsTransducer
  :: SymTransducer
       (HsPred ShipmentsRegs ShipmentsCommand)
       ShipmentsRegs
       ShipmentsVertex
       ShipmentsCommand
       ShipmentsEvent
shipmentsTransducer =
  B.buildTransducer ShipmentsEmpty initialShipmentsRegs isTerminal do
    B.from ShipmentsEmpty do
      B.onCmd inCtorRecordShipment $ \d -> B.do
        B.slot @"accepted" =: d.accepted
        B.emit wireShipmentRecorded (ShipmentRecordedTermFields
          { sharedReference = d.sharedReference
          , accepted = d.accepted
          })
        B.goto ShipmentsRecorded
 where
  isTerminal = \case
    ShipmentsRecorded -> True
    _ -> False

shipmentsFoldFingerprint :: Text
shipmentsFoldFingerprint = "6108a2aa4b5d59c62a6e703eb7120853"

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