packages feed

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