Transducer.hs

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE OverloadedLabels #-}
{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE QualifiedDo #-}
-- @generated by keiro-dsl 0.9.0.0 (language keiro-dsl 4) from aggregate Reservation; do not edit.
module Generated.HospitalCapacity.Reservation.Transducer
  ( reservationTransducer
  , reservationFoldFingerprint
  , BehaviorOwnership (..)
  , reservationPredicateVerifications
  ) where

import Generated.HospitalCapacity.Reservation.Domain
import Data.Text (Text)
import Generated.HospitalCapacity.Nominals (DivertStatus (..))
import Generated.HospitalCapacity.Nominals qualified as GeneratedNominals
import Keiki.Builder qualified as B
import Keiki.Core (HsPred, SymTransducer, (.==), (./=), (.||))
import Keiki.Core qualified as K
import Keiki.Symbolic qualified as S
import HospitalCapacity.Reservation.Holes qualified as Holes
import Keiki.Generics (RegFieldsOf)

reservationTransducer
  :: SymTransducer
       (HsPred ReservationRegs ReservationCommand)
       ReservationRegs
       ReservationVertex
       ReservationCommand
       ReservationEvent
reservationTransducer =
  B.buildTransducer ReservationUnrequested initialReservationRegs isTerminal do
    B.from ReservationUnrequested do
      B.onCmd inCtorRequestTransferReservation $ \d -> B.do
        let commandDivertStatus = K.inpProj GeneratedNominals.divertStatusEqualityWitness inCtorRequestTransferReservation (#divertStatus :: K.Index (RegFieldsOf RequestTransferReservationData) DivertStatus)
        B.requireGuard $
          commandDivertStatus ./= K.lit ("total-divert" :: Text)
          .|| d.lifeCriticalOverride .== K.lit True
        B.emit wireTransferReservationCreated (Holes.transition1UnrequestedRequestTransferReservationOutput1TransferReservationCreated d)
        B.goto ReservationHeld
    B.from ReservationHeld do
      B.onCmd inCtorConfirmReservation $ \d -> B.do
        B.emit wireTransferReservationConfirmed (Holes.transition2HeldConfirmReservationOutput1TransferReservationConfirmed d)
        B.goto ReservationConfirmed
 where
  isTerminal = \case
    ReservationExpired -> True
    ReservationAdmitted -> True
    ReservationReleased -> True
    _ -> False

reservationFoldFingerprint :: Text
reservationFoldFingerprint = "742bcb162938503b2d6ee4ff05b877ea"

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