NominalLeaves.hs

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

import Data.Aeson (Value (..), withText)
import Data.Aeson.Types (Parser)
import Data.KindID qualified as KindID
import Keiro.Codec.IdDomain (parseKindIdV7Text)
import Keiro.Codec.Nominal (nominalFromRepresentation, nominalToRepresentation)
import WorkspaceNominalProof.Bindings qualified as Bindings
import WorkspaceNominalProof.Domain (ClaimId)

encodeClaimIdLeaf :: ClaimId -> Value
encodeClaimIdLeaf = String . KindID.toText . nominalToRepresentation Bindings.claimIdBinding
{-# NOINLINE encodeClaimIdLeaf #-}

parseClaimIdLeaf :: Value -> Parser ClaimId
parseClaimIdLeaf = withText "ClaimId" $ \input ->
  case parseKindIdV7Text @"claim" input of
    Left reason -> fail (show reason)
    Right representation -> pure (nominalFromRepresentation Bindings.claimIdBinding representation)
{-# NOINLINE parseClaimIdLeaf #-}