Transducer.hs

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE OverloadedLabels #-}
{-# LANGUAGE QualifiedDo #-}
{-# LANGUAGE TypeApplications #-}
-- @generated by keiro-dsl 0.8.0.0 (language keiro-dsl 4) from aggregate NominalLedger; do not edit.
module Generated.NominalScalars.NominalLedger.Transducer
  ( nominalLedgerTransducer
  , nominalLedgerFoldFingerprint
  , BehaviorOwnership (..)
  , nominalLedgerPredicateVerifications
  ) where

import Generated.NominalScalars.NominalLedger.Domain
import Data.Text (Text)
import Generated.NominalScalars.NominalProjections qualified as NominalProjections
import NominalConformance.Domain qualified
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 ((=:))
import Keiki.Generics (RegFieldsOf)

nominalLedgerTransducer
  :: SymTransducer
       (HsPred NominalLedgerRegs NominalLedgerCommand)
       NominalLedgerRegs
       NominalLedgerVertex
       NominalLedgerCommand
       NominalLedgerEvent
nominalLedgerTransducer =
  B.buildTransducer NominalLedgerEmpty initialNominalLedgerRegs isTerminal do
    B.from NominalLedgerEmpty do
      B.onCmd inCtorRecordNominals $ \d -> B.do
        let commandOrderId = K.inpProj NominalProjections.orderIdEqualityWitness inCtorRecordNominals (#orderId :: K.Index (RegFieldsOf RecordNominalsData) NominalConformance.Domain.OrderId)
            registerOrderId = K.regProj NominalProjections.orderIdEqualityWitness (#orderId :: K.Index NominalLedgerRegs NominalConformance.Domain.OrderId)
            commandStatus = K.inpProj NominalProjections.orderStatusEqualityWitness inCtorRecordNominals (#status :: K.Index (RegFieldsOf RecordNominalsData) NominalConformance.Domain.OrderStatus)
            registerStatus = K.regProj NominalProjections.orderStatusEqualityWitness (#status :: K.Index NominalLedgerRegs NominalConformance.Domain.OrderStatus)
        B.requireGuard $
          commandOrderId .== registerOrderId
          .&& commandStatus .== registerStatus
        B.slot @"orderId" =: d.orderId
        B.slot @"status" =: d.status
        B.slot @"accountNumber" =: d.accountNumber
        B.slot @"riskScore" =: d.riskScore
        B.slot @"sequenceNumber" =: d.sequenceNumber
        B.slot @"featureFlag" =: d.featureFlag
        B.slot @"observedAt" =: d.observedAt
        B.emit wireNominalsRecorded (NominalsRecordedTermFields
          { orderId = d.orderId
          , status = d.status
          , accountNumber = d.accountNumber
          , riskScore = d.riskScore
          , sequenceNumber = d.sequenceNumber
          , featureFlag = d.featureFlag
          , observedAt = d.observedAt
          })
        B.goto NominalLedgerRecorded
 where
  isTerminal = \case
    NominalLedgerRecorded -> True
    _ -> False

nominalLedgerFoldFingerprint :: Text
nominalLedgerFoldFingerprint = "757ae5b82b33565e6c0c7fe2af1b527c"

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