Transducer.hs

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE QualifiedDo #-}
{-# LANGUAGE TypeApplications #-}
-- @generated by keiro-dsl 0.8.0.0 (language keiro-dsl 4) from aggregate ScalarLedger; do not edit.
module Generated.AggregateScalars.ScalarLedger.Transducer
  ( scalarLedgerTransducer
  , scalarLedgerFoldFingerprint
  , BehaviorOwnership (..)
  , scalarLedgerPredicateVerifications
  ) where

import Generated.AggregateScalars.ScalarLedger.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 AggregateScalars.ScalarLedger.Holes qualified as Holes
import Keiki.Builder ((=:))

scalarLedgerTransducer
  :: SymTransducer
       (HsPred ScalarLedgerRegs ScalarLedgerCommand)
       ScalarLedgerRegs
       ScalarLedgerVertex
       ScalarLedgerCommand
       ScalarLedgerEvent
scalarLedgerTransducer =
  B.buildTransducer ScalarLedgerEmpty initialScalarLedgerRegs isTerminal do
    B.from ScalarLedgerEmpty do
      B.onCmd inCtorRecord $ \d -> B.do
        B.requireGuard $
          d.observedAt .>= B.reg @"observedAt"
          .&& d.revision .>= B.reg @"revision"
        B.slot @"observedAt" =: d.observedAt
        B.slot @"revision" =: d.revision
        B.emit wireScalarsRecorded (Holes.transition1EmptyRecordOutput1ScalarsRecorded d)
        B.goto ScalarLedgerRecorded
 where
  isTerminal = \case
    ScalarLedgerRecorded -> True
    _ -> False

scalarLedgerFoldFingerprint :: Text
scalarLedgerFoldFingerprint = "c18684310d0f8e508077f8bd61bbabf3"

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