Transducer.hs

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE OverloadedLabels #-}
{-# LANGUAGE QualifiedDo #-}
{-# LANGUAGE TypeApplications #-}
-- @generated by keiro-dsl 0.8.0.0 (language keiro-dsl 4) from aggregate Project; do not edit.
module Generated.WorkspaceNominalProof.Project.Transducer
  ( projectTransducer
  , projectFoldFingerprint
  , BehaviorOwnership (..)
  , projectPredicateVerifications
  ) where

import Generated.WorkspaceNominalProof.Project.Domain
import Data.Text (Text)
import Generated.WorkspaceNominalProof.Nominals (ProjectId, parseProjectId, ProjectPhase (..))
import Generated.WorkspaceNominalProof.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 Keiki.Builder ((=:))
import Keiki.Generics (RegFieldsOf)

projectTransducer
  :: SymTransducer
       (HsPred ProjectRegs ProjectCommand)
       ProjectRegs
       ProjectVertex
       ProjectCommand
       ProjectEvent
projectTransducer =
  B.buildTransducer ProjectEmpty initialProjectRegs isTerminal do
    B.from ProjectEmpty do
      B.onCmd inCtorRegisterProject $ \d -> B.do
        let commandProjectId = K.inpProj GeneratedNominals.projectIdEqualityWitness inCtorRegisterProject (#projectId :: K.Index (RegFieldsOf RegisterProjectData) ProjectId)
            registerProjectId = K.regProj GeneratedNominals.projectIdEqualityWitness (#projectId :: K.Index ProjectRegs ProjectId)
            commandPhase = K.inpProj GeneratedNominals.projectPhaseEqualityWitness inCtorRegisterProject (#phase :: K.Index (RegFieldsOf RegisterProjectData) ProjectPhase)
            registerPhase = K.regProj GeneratedNominals.projectPhaseEqualityWitness (#phase :: K.Index ProjectRegs ProjectPhase)
        B.requireGuard $
          commandProjectId .== registerProjectId
          .&& commandPhase .== registerPhase
        B.slot @"projectId" =: d.projectId
        B.slot @"phase" =: d.phase
        B.emit wireProjectRegistered (ProjectRegisteredTermFields
          { projectId = d.projectId
          , phase = d.phase
          })
        B.goto ProjectLive
    B.from ProjectLive do
      B.onCmd inCtorArchiveProject $ \d -> B.do
        let commandProjectId = K.inpProj GeneratedNominals.projectIdEqualityWitness inCtorArchiveProject (#projectId :: K.Index (RegFieldsOf ArchiveProjectData) ProjectId)
            registerProjectId = K.regProj GeneratedNominals.projectIdEqualityWitness (#projectId :: K.Index ProjectRegs ProjectId)
            commandPhase = K.inpProj GeneratedNominals.projectPhaseEqualityWitness inCtorArchiveProject (#phase :: K.Index (RegFieldsOf ArchiveProjectData) ProjectPhase)
            registerPhase = K.regProj GeneratedNominals.projectPhaseEqualityWitness (#phase :: K.Index ProjectRegs ProjectPhase)
        B.requireGuard $
          commandProjectId .== registerProjectId
          .&& commandPhase .== registerPhase
        B.emit wireArchivalRecorded (ArchivalRecordedTermFields
          { projectId = d.projectId
          , phase = d.phase
          })
        B.goto ProjectArchived
 where
  isTerminal = \case
    ProjectArchived -> True
    _ -> False

projectFoldFingerprint :: Text
projectFoldFingerprint = "45ade9770d9fd050b296ae227bd65aa2"

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