packages feed

keiro-dsl-0.17.0.0: test/conformance-workspace-nominals/Generated/WorkspaceNominalProof/StructuralConformance.hs

-- @generated by keiro-dsl 0.17.0.0 (language keiro-dsl 6) from context workspace-nominal-proof structural conformance; do not edit.
module Generated.WorkspaceNominalProof.StructuralConformance
  ( structuralConformanceAssertions
  ) where

import Data.List (nub)
import Data.List.NonEmpty qualified as NonEmpty
import Data.Proxy (Proxy (..))
import Data.Text qualified as T
import Keiki.Core (fieldWitnessAgrees)
import Keiki.Shape (CanonicalTypeName (..))
import Keiro.Codec.Nominal (nominalDomainRoundTrip, nominalFixtureCases, nominalFixtureDomain, nominalRepresentationRoundTrip, nominalToRepresentation)
import Keiro.Codec.Structural (FixtureCases (..), bindingDomainRoundTrip, bindingShapeRoundTrip, bindingToShape)
import Generated.WorkspaceNominalProof.StructuralProjections qualified as StructuralProjections
import WorkspaceNominalProof.Bindings qualified as Bindings
import WorkspaceNominalProof.Domain (ArtifactClaim, ClaimId, ProjectClaim)

structuralConformanceAssertions :: [(String, Bool)]
structuralConformanceAssertions =
  concat
    [ artifactClaimBindingAssertions
    , projectClaimBindingAssertions
    , claimIdNominalAssertions
    , [("fixture coverage: workspace-nominal-proof.ArtifactClaim.v1", coverageArtifactClaim)]
    , [("fixture coverage: workspace-nominal-proof.ProjectClaim.v1", coverageProjectClaim)]
    , structuralProjectionAssertions
    ]

validFixtureLabels :: NonEmpty.NonEmpty (T.Text, value) -> Bool
validFixtureLabels cases =
  all (not . T.null) labels && length labels == length (nub labels)
  where
    labels = map fst (NonEmpty.toList cases)

artifactClaimBindingAssertions :: [(String, Bool)]
artifactClaimBindingAssertions =
  ("fixture labels: workspace-nominal-proof.ArtifactClaim.v1", validFixtureLabels cases) :
  ("canonical identity: workspace-nominal-proof.ArtifactClaim.v1", canonicalTypeName (Proxy @ArtifactClaim) == "workspace-nominal-proof.ArtifactClaim.v1") :
  concat
    [ [ ("binding domain round-trip: workspace-nominal-proof.ArtifactClaim.v1/" <> T.unpack label, bindingDomainRoundTrip Bindings.artifactClaimBinding value)
      , ("binding shape round-trip: workspace-nominal-proof.ArtifactClaim.v1/" <> T.unpack label, bindingShapeRoundTrip Bindings.artifactClaimBinding (bindingToShape Bindings.artifactClaimBinding value))
      ]
    | (label, value) <- NonEmpty.toList cases
    ]
  where
    cases = fixtureCases Bindings.artifactClaimFixtures

projectClaimBindingAssertions :: [(String, Bool)]
projectClaimBindingAssertions =
  ("fixture labels: workspace-nominal-proof.ProjectClaim.v1", validFixtureLabels cases) :
  ("canonical identity: workspace-nominal-proof.ProjectClaim.v1", canonicalTypeName (Proxy @ProjectClaim) == "workspace-nominal-proof.ProjectClaim.v1") :
  concat
    [ [ ("binding domain round-trip: workspace-nominal-proof.ProjectClaim.v1/" <> T.unpack label, bindingDomainRoundTrip Bindings.projectClaimBinding value)
      , ("binding shape round-trip: workspace-nominal-proof.ProjectClaim.v1/" <> T.unpack label, bindingShapeRoundTrip Bindings.projectClaimBinding (bindingToShape Bindings.projectClaimBinding value))
      ]
    | (label, value) <- NonEmpty.toList cases
    ]
  where
    cases = fixtureCases Bindings.projectClaimFixtures

claimIdNominalAssertions :: [(String, Bool)]
claimIdNominalAssertions =
  [ ("nominal domain law: ClaimId", all (nominalDomainRoundTrip Bindings.claimIdBinding . nominalFixtureDomain) cases)
  , ("nominal representation law: ClaimId", all (\fixture -> let domainValue = nominalFixtureDomain fixture in nominalRepresentationRoundTrip Bindings.claimIdBinding (nominalToRepresentation Bindings.claimIdBinding domainValue)) cases)
  , ("nominal canonical identity: ClaimId", canonicalTypeName (Proxy @ClaimId) == "workspace-nominal-proof.ClaimId.v1")
  ]
  where
    cases = NonEmpty.toList (nominalFixtureCases Bindings.claimIdFixtures)

coverageArtifactClaim :: Bool
coverageArtifactClaim = True

coverageProjectClaim :: Bool
coverageProjectClaim = True

structuralProjectionAssertions :: [(String, Bool)]
structuralProjectionAssertions =
  [ ("projection witness agreement: workspace-nominal-proof.ArtifactClaim.v1/claimId", all (\(_, owner) -> fieldWitnessAgrees StructuralProjections.artifactClaimClaimIdWitness (\referenceOwner -> StructuralProjections.artifactClaimClaimIdGet referenceOwner) owner) (NonEmpty.toList (fixtureCases Bindings.artifactClaimFixtures)))
  , ("projection witness agreement: workspace-nominal-proof.ProjectClaim.v1/claimId", all (\(_, owner) -> fieldWitnessAgrees StructuralProjections.projectClaimClaimIdWitness (\referenceOwner -> StructuralProjections.projectClaimClaimIdGet referenceOwner) owner) (NonEmpty.toList (fixtureCases Bindings.projectClaimFixtures)))
  ]