Transducer.hs

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE QualifiedDo #-}
{-# LANGUAGE TypeApplications #-}
-- @generated by keiro-dsl; do not edit. Regenerated from the .keiro spec.
module Generated.WorkspaceNominalProof.ProjectArtifact.Transducer
  ( projectArtifactTransducer
  , projectArtifactFoldFingerprint
  , BehaviorOwnership (..)
  , projectArtifactPredicateVerifications
  ) where

import Generated.WorkspaceNominalProof.ProjectArtifact.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 Generated.WorkspaceNominalProof.ProjectArtifact.Expressions qualified as Expressions
import Keiki.Builder ((=:))

projectArtifactTransducer
  :: SymTransducer
       (HsPred ProjectArtifactRegs ProjectArtifactCommand)
       ProjectArtifactRegs
       ProjectArtifactVertex
       ProjectArtifactCommand
       ProjectArtifactEvent
projectArtifactTransducer =
  B.buildTransducer ProjectArtifactEmpty initialProjectArtifactRegs isTerminal do
    B.from ProjectArtifactEmpty do
      B.onCmd inCtorRecordArtifact $ \d -> B.do
        B.requireGuard (Expressions.transition1EmptyRecordArtifactGuard d)
        B.slot @"projectId" =: Expressions.transition1EmptyRecordArtifactWriteProjectId d
        B.slot @"phase" =: Expressions.transition1EmptyRecordArtifactWritePhase d
        B.emit wireArtifactRecorded (ArtifactRecordedTermFields
          { projectId = d.projectId
          , phase = d.phase
          })
        B.goto ProjectArtifactRecorded
 where
  isTerminal = \case
    ProjectArtifactRecorded -> True
    _ -> False

projectArtifactFoldFingerprint :: Text
projectArtifactFoldFingerprint = "f9264cc50ea1c28f"

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