path: root/source/Felix/Checking/Exact/Datatype.hs

{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE NoImplicitPrelude #-}

-- | Exact preparation of deterministic datatype declarations.
module Felix.Checking.Exact.Datatype
    ( PreparedExactDatatype
    , preparedExactDatatypeObjects
    , preparedExactDatatypeBindings
    , PreparedExactDatatypeFact
    , preparedExactDatatypeFacts
    , preparedExactDatatypeFactMarker
    , preparedExactDatatypeFactTarget
    , preparedExactDatatypeFactReference
    , preparedExactDatatypeDescriptor
    , prepareExactDatatype
    , CheckedExactDatatypeAuthorization
    , lowerPreparedExactDatatype
    , authorizeCheckedExactDatatype
    , ExactDatatypeError(..)
    , exactDatatypeErrorLocation
    , renderExactDatatypeError
    ) where

import Base hiding (Empty)
import Felix.Checking.Authority
import Felix.Checking.Core
import Felix.Checking.Datatype qualified as Datatype
import Felix.Checking.Declaration qualified as Declaration
import Felix.Checking.Exact.Global qualified as ExactGlobal
import Felix.Checking.Exact.Vocabulary
import Felix.Checking.Identity
import Felix.Checking.Semantic
import Felix.Checking.Typed.Inductive qualified as Typed
import Felix.Cache.Codec
import Felix.Module
import Felix.Meaning qualified as Meaning
import Felix.Report.Location
import Felix.Syntax.Abstract qualified as Raw
import Felix.Syntax.Interface
import Felix.Syntax.Internal qualified as Internal

import Control.Monad (unless, when)
import Control.Monad.Except (ExceptT)
import Control.Monad.Except qualified as Except
import Data.Bifunctor (first)
import Data.ByteString (ByteString)
import Data.List.NonEmpty qualified as NonEmpty
import Data.Map.Strict qualified as Map
import Data.Set qualified as Set
import Data.Text qualified as Text
import Numeric.Natural (Natural)


data PreparedDatatypeObject = PreparedDatatypeObject
    !Internal.Symbol
    !SemanticGlobalKey
    !CoreType
    !ObjectId
    !AssertedObject

data PreparedExactDatatypeFact = PreparedExactDatatypeFact
    !Internal.Marker
    !(FrozenCheckedCore ObjectId)
    !TheoremRef

preparedExactDatatypeFactMarker
    :: PreparedExactDatatypeFact
    -> Internal.Marker
preparedExactDatatypeFactMarker
        (PreparedExactDatatypeFact marker _target _reference) =
    marker

preparedExactDatatypeFactTarget
    :: PreparedExactDatatypeFact
    -> FrozenCheckedCore ObjectId
preparedExactDatatypeFactTarget
        (PreparedExactDatatypeFact _marker target _reference) =
    target

preparedExactDatatypeFactReference
    :: PreparedExactDatatypeFact
    -> TheoremRef
preparedExactDatatypeFactReference
        (PreparedExactDatatypeFact _marker _target reference) =
    reference

data PreparedExactDatatype = PreparedExactDatatype
    !Location
    !DeclarationSyntaxId
    !(NonEmpty PreparedDatatypeObject)
    !(NonEmpty PreparedExactDatatypeFact)
    !DatatypeCompilationDescriptor

data CheckedExactDatatypeAuthorization =
    CheckedExactDatatypeAuthorization
        !DatatypeCompilationDescriptor
        !ObjectId
        !(NonEmpty ObjectId)

preparedExactDatatypeObjects
    :: PreparedExactDatatype
    -> NonEmpty (ObjectId, CoreType)
preparedExactDatatypeObjects
        (PreparedExactDatatype _location _syntax objects _facts _descriptor) =
    fmap
        (\(PreparedDatatypeObject _symbol _key coreType identity _asserted) ->
            (identity, coreType))
        objects

preparedExactDatatypeBindings
    :: PreparedExactDatatype
    -> NonEmpty (SemanticGlobalKey, SemanticGlobalTarget)
preparedExactDatatypeBindings
        (PreparedExactDatatype _location _syntax objects _facts _descriptor) =
    fmap
        (\(PreparedDatatypeObject _symbol key _coreType identity _asserted) ->
            (key, GlobalReference identity))
        objects

preparedExactDatatypeFacts
    :: PreparedExactDatatype
    -> NonEmpty PreparedExactDatatypeFact
preparedExactDatatypeFacts
        (PreparedExactDatatype _location _syntax _objects facts _descriptor) =
    facts

preparedExactDatatypeDescriptor
    :: PreparedExactDatatype
    -> DatatypeCompilationDescriptor
preparedExactDatatypeDescriptor
        (PreparedExactDatatype _location _syntax _objects _facts descriptor) =
    descriptor

lowerPreparedExactDatatype
    :: PreparedExactDatatype
    -> Declaration.LoweringDriver
        (Either
            Declaration.DeclarationError
            (Declaration.CheckedDeclaration
                CheckedExactDatatypeAuthorization))
lowerPreparedExactDatatype
        (PreparedExactDatatype _location syntax objects facts descriptor) =
    do
        prepared <-
            traverse
                (\(PreparedExactDatatypeFact marker target _reference) ->
                    Declaration.prepareFrozenCandidateSpecLowering
                        assertedObjects
                        target
                        SearchEligible
                        [markerAlias marker])
                facts
        pure (buildChecked <$> sequence prepared)
  where
    assertedObjects =
        toList
            (fmap
                (\(PreparedDatatypeObject
                        _symbol _key _coreType _identity asserted) -> asserted)
                objects)
    bindings =
        toList
            (fmap
                (\(PreparedDatatypeObject
                        _symbol key _coreType identity _asserted) ->
                    semanticGlobalBinding key (GlobalReference identity))
                objects)
    carrier :| constructors = fmap objectIdentity objects
    constructorIds =
        case constructors of
            firstConstructor : remainingConstructors ->
                firstConstructor :| remainingConstructors
            [] -> impossible "a prepared datatype has no constructor"
    buildChecked specs =
        Declaration.checkedCompiledDeclaration
            syntax
            assertedObjects
            []
            bindings
            []
            [ fmap
                (\spec ->
                    Declaration.checkedCandidate
                        spec
                        (Declaration.checkedDatatypePlanning descriptor))
                specs
            ]
            (CheckedExactDatatypeAuthorization
                descriptor carrier constructorIds)

    markerAlias (Internal.Marker name) = semanticName name

    objectIdentity
            (PreparedDatatypeObject
                _symbol _key _coreType identity _asserted) =
        identity

authorizeCheckedExactDatatype
    :: CheckedExactDatatypeAuthorization
    -> [NonEmpty Declaration.ReservedCandidate]
    -> Declaration.Declaration ()
authorizeCheckedExactDatatype
        (CheckedExactDatatypeAuthorization descriptor carrier constructors) =
    \case
        [candidates] ->
            Declaration.authorizeDatatypeCompilationCandidates
                descriptor carrier constructors candidates
        stages ->
            Declaration.failDeclaration
                (Declaration.CheckedAuthorizationCandidateShapeMismatch
                    1 (length stages))

data ExactDatatypeError
    = ExactDatatypeUnsupportedBlock !Location
    | ExactDatatypeOccurrenceCountMismatch !Location !Int !Int
    | ExactDatatypeOccurrenceMismatch !Location
    | ExactDatatypeGlossFailed !Location !Meaning.GlossError
    | ExactDatatypeInvalid !Location !Text
    | ExactDatatypeDuplicateGlobal !Location !SemanticGlobalKey
    | ExactDatatypeFixedSemanticCollision !Location !SemanticGlobalKey
    | ExactDatatypeGlobalAlreadyVisible !Location !SemanticGlobalKey
    | ExactDatatypeObjectAlreadyAvailable !Location !ObjectId
    | ExactDatatypeGlobalResolutionFailed
        !Location
        !ExactGlobal.ExactGlobalResolutionError
    | ExactDatatypeLoweringFailed !Location !Typed.TypedInductiveError
    | ExactDatatypeExpectedSet !Location !CoreType
    | ExactDatatypeExpectedProposition !Location !CoreType
    deriving stock (Show, Eq)

exactDatatypeErrorLocation :: ExactDatatypeError -> Location
exactDatatypeErrorLocation = \case
    ExactDatatypeUnsupportedBlock location -> location
    ExactDatatypeOccurrenceCountMismatch location _expected _actual -> location
    ExactDatatypeOccurrenceMismatch location -> location
    ExactDatatypeGlossFailed location _failure -> location
    ExactDatatypeInvalid location _message -> location
    ExactDatatypeDuplicateGlobal location _key -> location
    ExactDatatypeFixedSemanticCollision location _key -> location
    ExactDatatypeGlobalAlreadyVisible location _key -> location
    ExactDatatypeObjectAlreadyAvailable location _identity -> location
    ExactDatatypeGlobalResolutionFailed location _failure -> location
    ExactDatatypeLoweringFailed location _failure -> location
    ExactDatatypeExpectedSet location _actual -> location
    ExactDatatypeExpectedProposition location _actual -> location

renderExactDatatypeError :: ExactDatatypeError -> Text
renderExactDatatypeError failure =
    locationToText (exactDatatypeErrorLocation failure)
        <> ": "
        <> case failure of
            ExactDatatypeUnsupportedBlock{} ->
                "this datatype source form is not supported by the typed checker"
            ExactDatatypeOccurrenceCountMismatch _location expected actual ->
                "the datatype has " <> shown actual
                    <> " syntax occurrences, but " <> shown expected
                    <> " are required"
            ExactDatatypeOccurrenceMismatch{} ->
                "a datatype syntax occurrence does not match its declaration"
            ExactDatatypeGlossFailed _location glossFailure ->
                "datatype elaboration failed: " <> shown glossFailure
            ExactDatatypeInvalid _location message ->
                "invalid datatype declaration: " <> message
            ExactDatatypeDuplicateGlobal _location key ->
                "the datatype declares the semantic key more than once: "
                    <> shown key
            ExactDatatypeFixedSemanticCollision _location key ->
                "the datatype collides with fixed semantics for " <> shown key
            ExactDatatypeGlobalAlreadyVisible _location key ->
                "the datatype global is already visible: " <> shown key
            ExactDatatypeObjectAlreadyAvailable _location identity ->
                "the datatype opaque object is already available: "
                    <> shown identity
            ExactDatatypeGlobalResolutionFailed _location resolution ->
                "datatype global resolution failed: " <> shown resolution
            ExactDatatypeLoweringFailed _location typedFailure ->
                "typed datatype lowering failed: " <> shown typedFailure
            ExactDatatypeExpectedSet _location actual ->
                "a datatype premise domain has type " <> shown actual
                    <> " instead of Set"
            ExactDatatypeExpectedProposition _location actual ->
                "a generated datatype fact has type " <> shown actual
                    <> " instead of Prop"
  where
    shown :: Show value => value -> Text
    shown = Text.pack . show

type Prepare =
    ExceptT ExactDatatypeError (Declaration.LoweringDriver)

type SourceOccurrence = (Location, Raw.Marker, CanonicalLexicalEntry)

exactDatatypeInvalid
    :: Location
    -> Datatype.DatatypeValidationError
    -> ExactDatatypeError
exactDatatypeInvalid declarationLocation failure =
    ExactDatatypeInvalid
        (fromMaybe
            declarationLocation
            (Datatype.datatypeValidationErrorLocation failure))
        (Datatype.renderDatatypeValidationError failure)

prepareExactDatatype
    :: Raw.Block
    -> [SourceOccurrence]
    -> Declaration.LoweringDriver
        (Either ExactDatatypeError PreparedExactDatatype)
prepareExactDatatype block occurrences =
    Except.runExceptT do
        (location, marker, rawDatatype) <-
            case block of
                Raw.BlockData blockLocation _title blockMarker datatype ->
                    pure (blockLocation, blockMarker, datatype)
                _ ->
                    Except.throwError
                        (ExactDatatypeUnsupportedBlock (locate block))
        keys <- validateOccurrences location marker rawDatatype occurrences
        internal <-
            case Meaning.meaning [block] of
                Right
                    [Internal.BlockData
                        _internalLocation _internalMarker datatype] ->
                            pure datatype
                Left failure ->
                    Except.throwError
                        (ExactDatatypeGlossFailed location failure)
                Right _ ->
                    Except.throwError
                        (ExactDatatypeUnsupportedBlock location)
        checked <-
            -- The new opaque carrier has no semantic binding while its
            -- declaration is prepared, so premise recursion cannot depend on
            -- abbreviation expansion. Revisit this if forward aliases become
            -- available.
            Except.lift
                (Datatype.prepareCheckedDatatype pure internal)
                >>= Except.liftEither
                    . first (exactDatatypeInvalid location)
        let symbols =
                Datatype.checkedDatatypeHeadSymbol checked
                    :| toList
                        (Datatype.checkedDatatypeConstructorSymbols checked)
            views = Datatype.checkedDatatypeClauseViews checked
            arities =
                0 :| (length
                    . Datatype.checkedDatatypeClauseViewArguments
                    <$> toList views)
        unless (NonEmpty.length symbols == NonEmpty.length keys)
            (Except.throwError
                (ExactDatatypeOccurrenceCountMismatch
                    location
                    (NonEmpty.length symbols)
                    (NonEmpty.length keys)))
        validateKeys occurrences keys
        slot <- Except.lift Declaration.nextDeclarationSlotLowering
        theory <- Except.lift Declaration.currentTheoryLowering
        objects <-
            sequence
                (NonEmpty.zipWith
                    (\index (occurrenceLocation, symbol, key, arity) ->
                        prepareObject
                            occurrenceLocation
                            slot theory index symbol key arity)
                    (0 :| [1 ..])
                    (NonEmpty.zipWith
                        (\occurrenceLocation (symbol, key, arity) ->
                            (occurrenceLocation, symbol, key, arity))
                        (validatedOccurrenceLocations occurrences)
                        (NonEmpty.zipWith
                            (\(symbol, key) arity ->
                                (symbol, key, arity))
                            (NonEmpty.zip symbols keys)
                            arities)))
        let ownedSymbols = Set.fromList (toList symbols)
            generated = Datatype.checkedDatatypeGeneratedFacts checked
            externalSymbols =
                (foldMap
                    (Internal.mentionedSymbols . snd)
                    generated
                    <> foldMap premiseSymbols views)
                    `Set.difference` ownedSymbols
        external <-
            Except.lift
                (ExactGlobal.resolveExactSourceGlobals externalSymbols)
                >>= Except.liftEither
                    . first (ExactDatatypeGlobalResolutionFailed location)
        let (externalGlobals, externalTypes) = external
            ownedGlobals =
                Map.fromList
                    [ (symbol, Typed.SourceGlobal identity Nothing)
                    | PreparedDatatypeObject
                        symbol _key _coreType identity _asserted <-
                            toList objects
                    ]
            ownedTypes =
                Map.fromList
                    [ (identity, coreType)
                    | PreparedDatatypeObject
                        _symbol _key coreType identity _asserted <-
                            toList objects
                    ]
            sourceGlobals = Map.union ownedGlobals externalGlobals
            globalTypes = Map.union ownedTypes externalTypes
            resolveGlobal = (`Map.lookup` sourceGlobals)
            globalType identity =
                fromMaybe
                    (impossible
                        "prepared datatype global has no checked type")
                    (Map.lookup identity globalTypes)
        preparedClauses <-
            Except.liftEither
                (traverse
                    (prepareClause location globalType resolveGlobal)
                    views)
        facts <-
            Except.liftEither
                (traverse
                    (prepareFact location theory globalType resolveGlobal)
                    generated)
        let carrier = objectIdentity (NonEmpty.head objects)
            constructors = objectIdentity <$> NonEmpty.tail objects
            descriptor =
                case NonEmpty.nonEmpty constructors of
                    Nothing ->
                        impossible
                            "a checked datatype has no constructors"
                    Just nonemptyConstructors ->
                        datatypeCompilationDescriptor
                            carrier
                            nonemptyConstructors
                            (preparedExactDatatypeFactReference
                                <$> toList facts)
            syntax =
                declarationSyntaxId
                    (encodePreparedDatatype
                        objects
                        preparedClauses
                        facts
                        descriptor)
        pure
            (PreparedExactDatatype
                location
                syntax
                objects
                facts
                descriptor)
  where
    objectIdentity
        (PreparedDatatypeObject _symbol _key _coreType identity _asserted) =
        identity

validateOccurrences
    :: Location
    -> Raw.Marker
    -> Raw.Datatype
    -> [SourceOccurrence]
    -> Prepare (NonEmpty SemanticGlobalKey)
validateOccurrences location marker datatype occurrences = do
    expected <-
        Except.liftEither
            (expectedOccurrences location marker datatype)
    unless (length occurrences == NonEmpty.length expected)
        (Except.throwError
            (ExactDatatypeOccurrenceCountMismatch
                location
                (NonEmpty.length expected)
                (length occurrences)))
    keys <-
        sequence
            (NonEmpty.zipWith validateOne expected
                (case NonEmpty.nonEmpty occurrences of
                    Just nonempty -> nonempty
                    Nothing ->
                        impossible
                            "equal nonzero occurrence counts became empty"))
    pure keys
  where
    validateOne
            (expectedLocation, expectedMarker, expectedPattern)
            (actualLocation, actualMarker, entry) =
        case entry of
            CanonicalExpressionFunction pat marker' _fixity
                | actualMarker == expectedMarker
                , marker' == expectedMarker
                , pat == expectedPattern ->
                    pure
                        (SemanticExpressionFunction pat)
            _ ->
                Except.throwError
                    (ExactDatatypeOccurrenceMismatch
                        (bestLocation actualLocation expectedLocation))

    bestLocation actual expected
        | actual == Nowhere = expected
        | otherwise = actual

expectedOccurrences
    :: Location
    -> Raw.Marker
    -> Raw.Datatype
    -> Either
        ExactDatatypeError
        (NonEmpty (Location, Raw.Marker, Raw.Pattern))
expectedOccurrences location blockMarker datatype = do
    headOccurrence <-
        expectedSymbol blockMarker (Raw.datatypeHeadExpr datatype)
    clauses <-
        traverse
            (\clause ->
                case Raw.datatypeClauseConstructorExpr clause of
                    Raw.ExprOp constructorLocation symbol _arguments ->
                        Right
                            ( constructorLocation
                            , Raw.mixfixMarker symbol
                            , Raw.mixfixPattern symbol
                            )
                    expression ->
                        Left
                            (ExactDatatypeOccurrenceMismatch
                                (locate expression)))
            (Raw.datatypeClauses datatype)
    pure (headOccurrence :| toList clauses)
  where
    expectedSymbol expectedMarker = \case
        Raw.ExprOp symbolLocation symbol [] ->
            Right
                ( symbolLocation
                , expectedMarker
                , Raw.mixfixPattern symbol
                )
        expression ->
            Left
                (ExactDatatypeOccurrenceMismatch
                    (case locate expression of
                        Nowhere -> location
                        expressionLocation -> expressionLocation))

validateKeys
    :: [SourceOccurrence]
    -> NonEmpty SemanticGlobalKey
    -> Prepare ()
validateKeys occurrences keys = do
    case duplicateWithLocation of
        Just (duplicate, duplicateLocation) ->
            Except.throwError
                (ExactDatatypeDuplicateGlobal
                    duplicateLocation
                    duplicate)
        Nothing -> pure ()
    traverse_ validateOne (NonEmpty.zip locations keys)
  where
    locations = validatedOccurrenceLocations occurrences

    duplicateWithLocation =
        go Set.empty
            [ (key, occurrenceLocation)
            | (key, (occurrenceLocation, _marker, _entry)) <-
                zip (toList keys) occurrences
            ]

    go _seen [] = Nothing
    go seen ((key, occurrenceLocation) : remaining)
        | key `Set.member` seen = Just (key, occurrenceLocation)
        | otherwise = go (Set.insert key seen) remaining

    validateOne (occurrenceLocation, key) = do
        when (isJust (fixedSemanticMeaning key))
            (Except.throwError
                (ExactDatatypeFixedSemanticCollision occurrenceLocation key))
        visible <-
            Except.lift
                (Declaration.resolveVisibleGlobalLowering key)
        when (isJust visible)
            (Except.throwError
                (ExactDatatypeGlobalAlreadyVisible occurrenceLocation key))

validatedOccurrenceLocations
    :: [SourceOccurrence]
    -> NonEmpty Location
validatedOccurrenceLocations occurrences =
    case NonEmpty.nonEmpty
            [ occurrenceLocation
            | (occurrenceLocation, _marker, _entry) <- occurrences
            ] of
        Just nonempty -> nonempty
        Nothing ->
            impossible "validated datatype occurrences are empty"

prepareObject
    :: Location
    -> DeclarationSlot
    -> TheoryId
    -> Natural
    -> Internal.Symbol
    -> SemanticGlobalKey
    -> Int
    -> Prepare PreparedDatatypeObject
prepareObject location slot theory index symbol key arity = do
    let coreType =
            foldr (const (TyArrow TySet)) TySet [1 .. arity]
        seed =
            opaqueDeclarationSeed
                (declarationSlotModule slot)
                (declarationSlotOrdinal slot)
                DatatypeDeclaration
                (generatedObjectSlot index)
        content = OpaqueObjectContent theory seed coreType
        identity = opaqueObjectId theory seed coreType
    available <- Except.lift (Declaration.objectAvailableLowering identity)
    when available
        (Except.throwError
            (ExactDatatypeObjectAlreadyAvailable location identity))
    pure
        (PreparedDatatypeObject
            symbol
            key
            coreType
            identity
            (assertedObject identity content))

data PreparedClause = PreparedClause
    !Internal.FunctionSymbol
    ![PreparedPremise]

data PreparedPremise
    = PreparedRecursivePremise !(FrozenCheckedCore ObjectId)
    | PreparedNonRecursivePremise !(FrozenCheckedCore ObjectId)

prepareClause
    :: Location
    -> (ObjectId -> CoreType)
    -> (Internal.Symbol -> Maybe (Typed.SourceGlobal ObjectId))
    -> Datatype.CheckedDatatypeClauseView
    -> Either ExactDatatypeError PreparedClause
prepareClause location globalType resolveGlobal view =
    PreparedClause
        (Datatype.checkedDatatypeClauseViewConstructor view)
        <$> traverse preparePremise
            (Datatype.checkedDatatypeClauseViewPremises view)
  where
    preparePremise = \case
        Datatype.CheckedRecursiveDatatypePremise _variable domain ->
            PreparedRecursivePremise
                <$> prepareDomain domain
        Datatype.CheckedNonRecursiveDatatypePremise _variable domain ->
            PreparedNonRecursivePremise
                <$> prepareDomain domain

    prepareDomain domain = do
        checked <-
            first (ExactDatatypeLoweringFailed location)
                (Typed.prepareTypedClosedTerm
                    globalType
                    resolveGlobal
                    domain)
        unless (frozenCoreType checked == TySet)
            (Left
                (ExactDatatypeExpectedSet
                    location
                    (frozenCoreType checked)))
        pure checked

prepareFact
    :: Location
    -> TheoryId
    -> (ObjectId -> CoreType)
    -> (Internal.Symbol -> Maybe (Typed.SourceGlobal ObjectId))
    -> (Internal.Marker, Internal.Formula)
    -> Either ExactDatatypeError PreparedExactDatatypeFact
prepareFact location theory globalType resolveGlobal (marker, formula) = do
    checked <-
        first (ExactDatatypeLoweringFailed location)
            (Typed.prepareTypedClosedFormula
                globalType
                resolveGlobal
                formula)
    unless (frozenCoreType checked == TyProp)
        (Left
            (ExactDatatypeExpectedProposition
                location
                (frozenCoreType checked)))
    pure
        (PreparedExactDatatypeFact
            marker
            checked
            (theoremRef theory
                (propositionIdOf (frozenCoreTerm checked))))

premiseSymbols
    :: Datatype.CheckedDatatypeClauseView
    -> Set.Set Internal.Symbol
premiseSymbols view =
    foldMap symbols
        (Datatype.checkedDatatypeClauseViewPremises view)
  where
    symbols = \case
        Datatype.CheckedRecursiveDatatypePremise _variable domain ->
            Internal.mentionedSymbols domain
        Datatype.CheckedNonRecursiveDatatypePremise _variable domain ->
            Internal.mentionedSymbols domain

encodePreparedDatatype
    :: NonEmpty PreparedDatatypeObject
    -> NonEmpty PreparedClause
    -> NonEmpty PreparedExactDatatypeFact
    -> DatatypeCompilationDescriptor
    -> ByteString
encodePreparedDatatype objects clauses facts descriptor =
    encodeCache do
        putCacheTag 0x05
        putCacheList putObject (toList objects)
        putCacheList putClause (toList clauses)
        putCacheList putFact (toList facts)
        putDirectAuthorizationCache
            (TrustedCompilation
                (DatatypeCompilation descriptor))
  where
    putObject
            (PreparedDatatypeObject
                _symbol key coreType identity _asserted) = do
        putSemanticGlobalKeyCache key
        putCoreTypeCache coreType
        putObjectIdCache identity

    putClause (PreparedClause constructor premises) = do
        putSemanticGlobalKeyCache
            (SemanticExpressionFunction
                (Raw.mixfixPattern constructor))
        putCacheList putPremise premises

    putPremise = \case
        PreparedRecursivePremise domain -> do
            putCacheTag 0x00
            putCanonicalTermCache putObjectIdCache
                (frozenCoreTerm domain)
        PreparedNonRecursivePremise domain -> do
            putCacheTag 0x01
            putCanonicalTermCache putObjectIdCache
                (frozenCoreTerm domain)

    putFact fact = do
        let Internal.Marker marker =
                preparedExactDatatypeFactMarker fact
        putCacheText marker
        putCanonicalTermCache putObjectIdCache
            (frozenCoreTerm
                (preparedExactDatatypeFactTarget fact))
        putTheoremRefCache
            (preparedExactDatatypeFactReference fact)