Transducer.hs

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE QualifiedDo #-}
{-# LANGUAGE TypeApplications #-}
-- @generated by keiro-dsl; do not edit. Regenerated from the .keiro spec.
module Generated.AggregateScalarExpressions.ScalarAccount.Transducer
  ( scalarAccountTransducer
  , scalarAccountFoldFingerprint
  , BehaviorOwnership (..)
  , scalarAccountPredicateVerifications
  ) where

import Generated.AggregateScalarExpressions.ScalarAccount.Domain
import AggregateScalarExpressions.ScalarAccount.Holes qualified as Holes
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 Generated.AggregateScalarExpressions.ScalarAccount.Expressions qualified as Expressions
import Data.Text qualified as T
import Keiki.Builder ((=:))
import Keiro.Snapshot.Codec (FoldVersion (..))

scalarAccountTransducer
  :: SymTransducer
       (HsPred ScalarAccountRegs ScalarAccountCommand)
       ScalarAccountRegs
       ScalarAccountVertex
       ScalarAccountCommand
       ScalarAccountEvent
scalarAccountTransducer =
  B.buildTransducer ScalarAccountOpen initialScalarAccountRegs isTerminal do
    B.from ScalarAccountOpen do
      B.onCmd inCtorAdjust $ \d -> B.do
        B.requireGuard (Expressions.transition1OpenAdjustGuard d)
        B.slot @"balance" =: Expressions.transition1OpenAdjustWriteBalance d
        B.slot @"reserved" =: Expressions.transition1OpenAdjustWriteReserved d
        B.slot @"machine" =: Expressions.transition1OpenAdjustWriteMachine d
        B.slot @"label" =: Expressions.transition1OpenAdjustWriteLabel d
        B.slot @"active" =: Expressions.transition1OpenAdjustWriteActive d
        B.slot @"mode" =: Expressions.transition1OpenAdjustWriteMode d
        B.slot @"requestId" =: Expressions.transition1OpenAdjustWriteRequestId d
        B.slot @"openedAt" =: Expressions.transition1OpenAdjustWriteOpenedAt d
        B.slot @"limits" =: Expressions.transition1OpenAdjustWriteLimits d
        B.emit wireAdjusted (Holes.transition1OpenAdjustOutput1Adjusted d)
        B.goto ScalarAccountReviewed
    B.from ScalarAccountReviewed do
      B.onCmd inCtorClose $ \d -> B.do
        Holes.transition2ReviewedCloseHole d
        B.emit wireClosedEvent (Holes.transition2ReviewedCloseOutput1ClosedEvent d)
        B.goto ScalarAccountClosed
 where
  isTerminal = \case
    ScalarAccountClosed -> True
    _ -> False

scalarAccountFoldFingerprint :: Text
scalarAccountFoldFingerprint = T.intercalate "|" ("dec0c7c5688740a8" : [foldToken Holes.transition2ReviewedCloseHoleFoldVersion] ) where foldToken (FoldVersion token) = T.pack (show (T.length token)) <> ":" <> token

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