Transducer.hs

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE QualifiedDo #-}
-- @generated by keiro-dsl 0.21.0.0 (language keiro-dsl 6) from aggregate Lifecycle; do not edit.
module Generated.MappedRegisterConstruction.Lifecycle.Transducer
  ( lifecycleTransducer
  , lifecycleFoldFingerprint
  , BehaviorOwnership (..)
  , lifecyclePredicateVerifications
  ) where

import Generated.MappedRegisterConstruction.Lifecycle.Domain
import Data.Text (Text)
import Conformance.MappedRegisterConstruction.Bindings qualified as Bindings
import Conformance.MappedRegisterConstruction.Lift qualified as Lift
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 ((=:))

lifecycleTransducer
  :: SymTransducer
       (HsPred LifecycleRegs LifecycleCommand)
       LifecycleRegs
       LifecycleVertex
       LifecycleCommand
       LifecycleEvent
lifecycleTransducer =
  B.buildTransducer LifecycleEmpty initialLifecycleRegs isTerminal do
    B.from LifecycleEmpty do
      B.onCmd inCtorCreate $ \d -> B.do
        B.slot @"dormantSince" =: K.opaqueLit Bindings.noTime
        B.slot @"automatic" =: d.automatic
        B.emit wireCreated (CreatedTermFields
          { automatic = d.automatic
          })
        B.goto LifecycleAwake
    B.from LifecycleAwake do
      B.onCmd inCtorMark $ \d -> B.do
        B.slot @"dormantSince" =: K.TApp1 Lift.atTime (d.markedAt)
        B.emit wireMarked (MarkedTermFields
          { markedAt = d.markedAt
          })
        B.goto LifecycleDormant
      B.onCmd inCtorClose $ \d -> B.do
        B.emit wireClosedEvent (ClosedEventTermFields
          { closedAt = d.closedAt
          })
        B.goto LifecycleClosed
    B.from LifecycleDormant do
      B.onCmd inCtorPing $ \d -> B.do
        B.requireGuard $
          B.reg @"automatic" .== K.lit True
        B.slot @"dormantSince" =: K.opaqueLit Bindings.noTime
        B.emit wirePinged (PingedTermFields
          { markedAt = d.markedAt
          })
        B.goto LifecycleAwake
      B.onCmd inCtorPing $ \d -> B.do
        B.requireGuard $
          B.reg @"automatic" .== K.lit False
        B.slot @"dormantSince" =: K.TApp1 Lift.atTime (d.markedAt)
        B.emit wirePinged (PingedTermFields
          { markedAt = d.markedAt
          })
        B.goto LifecycleDormant
      B.onCmd inCtorAwaken $ \d -> B.do
        B.slot @"dormantSince" =: K.opaqueLit Bindings.noTime
        B.emit wireAwakened (AwakenedTermFields
          { awakenedAt = d.awakenedAt
          })
        B.goto LifecycleAwake
    B.from LifecycleClosed do
      B.onCmd inCtorReopen $ \d -> B.do
        B.slot @"dormantSince" =: K.opaqueLit Bindings.noTime
        B.emit wireReopened (ReopenedTermFields
          { reopenedAt = d.reopenedAt
          })
        B.goto LifecycleAwake
 where
  isTerminal = \case

    _ -> False

lifecycleFoldFingerprint :: Text
lifecycleFoldFingerprint = "36d736d8808e56273d8ad11b24937942"

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.
lifecyclePredicateVerifications :: IO [(Text, BehaviorOwnership, S.PredicateVerification)]
lifecyclePredicateVerifications = sequence
  [ verifyTransition "transition1EmptyCreate" GeneratedOwned LifecycleEmpty 0
  , verifyTransition "transition2AwakeMark" GeneratedOwned LifecycleAwake 0
  , verifyTransition "transition6AwakeClose" GeneratedOwned LifecycleAwake 1
  , verifyTransition "transition3DormantPing" GeneratedOwned LifecycleDormant 0
  , verifyTransition "transition4DormantPing" GeneratedOwned LifecycleDormant 1
  , verifyTransition "transition5DormantAwaken" GeneratedOwned LifecycleDormant 2
  , verifyTransition "transition7ClosedReopen" GeneratedOwned LifecycleClosed 0
  ]
 where
  verifyTransition label owner source edgeIndex =
    case drop edgeIndex (K.edgesOut lifecycleTransducer source) of
      K.Edge predicate _ _ _ _ : _ -> (\result -> (label, owner, result)) <$> S.verifyPredicate predicate
      [] -> pure (label, owner, S.UnverifiedSolverFailure "generated transition edge missing")