Transducer.hs

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE QualifiedDo #-}
-- @generated by keiro-dsl 0.9.0.0 (language keiro-dsl 4) from aggregate ArtifactCatalog; do not edit.
module Generated.StructuralConformance.ArtifactCatalog.Transducer
  ( artifactCatalogTransducer
  , artifactCatalogFoldFingerprint
  , BehaviorOwnership (..)
  , artifactCatalogPredicateVerifications
  ) where

import Generated.StructuralConformance.ArtifactCatalog.Domain
import Data.Text (Text)
import Conformance.Structural.Domain (ArtifactInfo, Geometry)
import Keiki.Builder qualified as B
import Keiki.Core (HsPred, SymTransducer)
import Keiki.Core qualified as K
import Keiki.Symbolic qualified as S
import StructuralConformance.ArtifactCatalog.Holes qualified as Holes
import Keiki.Builder ((=:))

artifactCatalogTransducer
  :: SymTransducer
       (HsPred ArtifactCatalogRegs ArtifactCatalogCommand)
       ArtifactCatalogRegs
       ArtifactCatalogVertex
       ArtifactCatalogCommand
       ArtifactCatalogEvent
artifactCatalogTransducer =
  B.buildTransducer ArtifactCatalogEmpty initialArtifactCatalogRegs isTerminal do
    B.from ArtifactCatalogEmpty do
      B.onCmd inCtorObserveArtifact $ \d -> B.do
        B.slot @"currentArtifact" =: d.artifact
        B.slot @"currentGeometry" =: d.geometry
        B.slot @"acceptedCount" =: B.reg @"acceptedCount"
        B.emit wireArtifactRecorded (ArtifactRecordedTermFields
          { artifact = d.artifact
          , geometry = d.geometry
          , accepted = d.accepted
          })
        B.emit wireArtifactAccepted (Holes.transition1EmptyObserveArtifactOutput2ArtifactAccepted d)
        B.goto ArtifactCatalogObserved
 where
  isTerminal = \case
    ArtifactCatalogObserved -> True
    _ -> False

artifactCatalogFoldFingerprint :: Text
artifactCatalogFoldFingerprint = "e31d3344ae234ff96862f11e9c823f9d"

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