Transducer.hs

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE QualifiedDo #-}
-- @generated by keiro-dsl 0.18.0.0 (language keiro-dsl 6) from aggregate LabelStore; do not edit.
module Generated.StructuralTextSets.LabelStore.Transducer
  ( labelStoreTransducer
  , labelStoreFoldFingerprint
  , BehaviorOwnership (..)
  , labelStorePredicateVerifications
  ) where

import Generated.StructuralTextSets.LabelStore.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 Keiki.Builder ((=:))

labelStoreTransducer
  :: SymTransducer
       (HsPred LabelStoreRegs LabelStoreCommand)
       LabelStoreRegs
       LabelStoreVertex
       LabelStoreCommand
       LabelStoreEvent
labelStoreTransducer =
  B.buildTransducer LabelStoreEmpty initialLabelStoreRegs isTerminal do
    B.from LabelStoreEmpty do
      B.onCmd inCtorStoreLabels $ \d -> B.do
        B.slot @"current" =: d.labels
        B.emit wireLabelsStored (LabelsStoredTermFields
          { labels = d.labels
          , optionalLabels = d.optionalLabels
          , envelope = d.envelope
          })
        B.emit wireLabelsAudited (LabelsAuditedTermFields
          { labels = d.labels
          , optionalLabels = d.optionalLabels
          , envelope = d.envelope
          })
        B.goto LabelStoreStored
      B.onCmd inCtorImportLegacyLabels $ \d -> B.do
        B.replayOnly
        B.slot @"current" =: d.labels
        B.emit wireLegacyLabelsImported (LegacyLabelsImportedTermFields
          { labels = d.labels
          , optionalLabels = d.optionalLabels
          , envelope = d.envelope
          })
        B.goto LabelStoreStored
 where
  isTerminal = \case
    LabelStoreStored -> True
    _ -> False

labelStoreFoldFingerprint :: Text
labelStoreFoldFingerprint = "0c2bb8be00157f35ec32d45a77a0a98e"

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