Expressions.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE OverloadedLabels #-}
{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE TypeApplications #-}
-- @generated by keiro-dsl; do not edit. Regenerated from the .keiro spec.
module Generated.WorkspaceNominalProof.Project.Expressions
  ( transition1EmptyRegisterProjectGuard
  , transition1EmptyRegisterProjectWriteProjectId
  , transition1EmptyRegisterProjectWritePhase
  , transition2LiveArchiveProjectGuard
  ) where

import Generated.WorkspaceNominalProof.Project.Domain
import Keiki.Builder qualified as B
import Keiki.Core qualified as K
import Keiki.Generics (RegFieldsOf)
import Data.Text (Text)
import Generated.WorkspaceNominalProof.Nominals (ProjectId (..), ProjectPhase (..))
import Generated.WorkspaceNominalProof.Nominals qualified as GeneratedNominals

transition1EmptyRegisterProjectGuard :: B.PayloadProj ProjectRegs ProjectCommand (RegFieldsOf RegisterProjectData) -> K.HsPred ProjectRegs ProjectCommand
transition1EmptyRegisterProjectGuard d = K.PAnd (K.PEq (K.inpProj GeneratedNominals.projectIdEqualityWitness inCtorRegisterProject (#projectId :: K.Index (RegFieldsOf RegisterProjectData) ProjectId)) (K.regProj GeneratedNominals.projectIdEqualityWitness (#projectId :: K.Index ProjectRegs ProjectId))) (K.PEq (K.inpProj GeneratedNominals.projectPhaseEqualityWitness inCtorRegisterProject (#phase :: K.Index (RegFieldsOf RegisterProjectData) ProjectPhase)) (K.regProj GeneratedNominals.projectPhaseEqualityWitness (#phase :: K.Index ProjectRegs ProjectPhase)))

transition1EmptyRegisterProjectWriteProjectId :: B.PayloadProj ProjectRegs ProjectCommand (RegFieldsOf RegisterProjectData) -> K.Term ProjectRegs ProjectCommand (RegFieldsOf RegisterProjectData) ProjectId
transition1EmptyRegisterProjectWriteProjectId d = d.projectId

transition1EmptyRegisterProjectWritePhase :: B.PayloadProj ProjectRegs ProjectCommand (RegFieldsOf RegisterProjectData) -> K.Term ProjectRegs ProjectCommand (RegFieldsOf RegisterProjectData) ProjectPhase
transition1EmptyRegisterProjectWritePhase d = d.phase

transition2LiveArchiveProjectGuard :: B.PayloadProj ProjectRegs ProjectCommand (RegFieldsOf ArchiveProjectData) -> K.HsPred ProjectRegs ProjectCommand
transition2LiveArchiveProjectGuard d = K.PAnd (K.PEq (K.inpProj GeneratedNominals.projectIdEqualityWitness inCtorArchiveProject (#projectId :: K.Index (RegFieldsOf ArchiveProjectData) ProjectId)) (K.regProj GeneratedNominals.projectIdEqualityWitness (#projectId :: K.Index ProjectRegs ProjectId))) (K.PEq (K.inpProj GeneratedNominals.projectPhaseEqualityWitness inCtorArchiveProject (#phase :: K.Index (RegFieldsOf ArchiveProjectData) ProjectPhase)) (K.regProj GeneratedNominals.projectPhaseEqualityWitness (#phase :: K.Index ProjectRegs ProjectPhase)))