Transducer.hs

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE OverloadedLabels #-}
{-# LANGUAGE QualifiedDo #-}
-- @generated by keiro-dsl 0.17.0.0 (language keiro-dsl 6) from aggregate TemplateCatalog; do not edit.
module Generated.StructuralNominalLeaves.TemplateCatalog.Transducer
  ( templateCatalogTransducer
  , templateCatalogFoldFingerprint
  , BehaviorOwnership (..)
  , templateCatalogPredicateVerifications
  ) where

import Generated.StructuralNominalLeaves.TemplateCatalog.Domain
import Data.Text (Text)
import Generated.StructuralNominalLeaves.Nominals (TemplateId)
import Generated.StructuralNominalLeaves.StructuralProjections qualified as StructuralProjections
import Generated.StructuralNominalLeaves.Nominals qualified as GeneratedNominals
import Conformance.StructuralNominals.Domain (TemplateState)
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)

templateCatalogTransducer
  :: SymTransducer
       (HsPred TemplateCatalogRegs TemplateCatalogCommand)
       TemplateCatalogRegs
       TemplateCatalogVertex
       TemplateCatalogCommand
       TemplateCatalogEvent
templateCatalogTransducer =
  B.buildTransducer TemplateCatalogEmpty initialTemplateCatalogRegs isTerminal do
    B.from TemplateCatalogEmpty do
      B.onCmd inCtorRecordTemplate $ \d -> B.do
        let registerActiveTemplateId = K.regProj GeneratedNominals.templateIdEqualityWitness (#activeTemplateId :: K.Index TemplateCatalogRegs TemplateId)
            commandStateTemplateId = K.inpProj StructuralProjections.templateStateTemplateIdWitness inCtorRecordTemplate (#state :: K.Index (RegFieldsOf RecordTemplateData) TemplateState)
        B.requireGuard $
          commandStateTemplateId .== registerActiveTemplateId
        B.slot @"book" =: d.book
        B.emit wireTemplateRecorded (TemplateRecordedTermFields
          { state = d.state
          , reference = d.reference
          , book = d.book
          })
        B.goto TemplateCatalogRecorded
    B.from TemplateCatalogRecorded do
      B.onCmd inCtorRouteTemplate $ \d -> B.do
        B.emit wireTemplateRouted (TemplateRoutedTermFields
          { templateId = d.templateId
          , claimId = d.claimId
          })
        B.goto TemplateCatalogRouted
 where
  isTerminal = \case
    TemplateCatalogRouted -> True
    _ -> False

templateCatalogFoldFingerprint :: Text
templateCatalogFoldFingerprint = "19cd35d7ec57e20e4a9f0383da843a58"

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