keiro-dsl-0.7.0.0: test/conformance-workspace-nominals/Generated/WorkspaceNominalProof/ProjectArtifact/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.ProjectArtifact.Expressions
( transition1EmptyRecordArtifactGuard
, transition1EmptyRecordArtifactWriteProjectId
, transition1EmptyRecordArtifactWritePhase
) where
import Generated.WorkspaceNominalProof.ProjectArtifact.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
transition1EmptyRecordArtifactGuard :: B.PayloadProj ProjectArtifactRegs ProjectArtifactCommand (RegFieldsOf RecordArtifactData) -> K.HsPred ProjectArtifactRegs ProjectArtifactCommand
transition1EmptyRecordArtifactGuard d = K.PAnd (K.PEq (K.inpProj GeneratedNominals.projectIdEqualityWitness inCtorRecordArtifact (#projectId :: K.Index (RegFieldsOf RecordArtifactData) ProjectId)) (K.regProj GeneratedNominals.projectIdEqualityWitness (#projectId :: K.Index ProjectArtifactRegs ProjectId))) (K.PEq (K.inpProj GeneratedNominals.projectPhaseEqualityWitness inCtorRecordArtifact (#phase :: K.Index (RegFieldsOf RecordArtifactData) ProjectPhase)) (K.regProj GeneratedNominals.projectPhaseEqualityWitness (#phase :: K.Index ProjectArtifactRegs ProjectPhase)))
transition1EmptyRecordArtifactWriteProjectId :: B.PayloadProj ProjectArtifactRegs ProjectArtifactCommand (RegFieldsOf RecordArtifactData) -> K.Term ProjectArtifactRegs ProjectArtifactCommand (RegFieldsOf RecordArtifactData) ProjectId
transition1EmptyRecordArtifactWriteProjectId d = d.projectId
transition1EmptyRecordArtifactWritePhase :: B.PayloadProj ProjectArtifactRegs ProjectArtifactCommand (RegFieldsOf RecordArtifactData) -> K.Term ProjectArtifactRegs ProjectArtifactCommand (RegFieldsOf RecordArtifactData) ProjectPhase
transition1EmptyRecordArtifactWritePhase d = d.phase