Migrate to `Felix` namespaceHEADhotg

1 files changed, 0 insertions, 751 deletions

diff --git a/source/Checking/Exact/Datatype.hs b/source/Checking/Exact/Datatype.hs
deleted file mode 100644
index 61d99e5..0000000
--- a/source/Checking/Exact/Datatype.hs
+++ /dev/null
@@ -1,751 +0,0 @@
-{-# LANGUAGE DerivingStrategies #-}
-{-# LANGUAGE NamedFieldPuns #-}
-{-# LANGUAGE NoImplicitPrelude #-}
-
--- | Exact preparation of deterministic datatype declarations.
-module 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 Checking.Authority
-import Checking.Core
-import Checking.Datatype qualified as Datatype
-import Checking.Declaration qualified as Declaration
-import Checking.Exact.Global qualified as ExactGlobal
-import Checking.Exact.Vocabulary
-import Checking.Identity
-import Checking.Semantic
-import Checking.Typed.Inductive qualified as Typed
-import Felix.Cache.Codec
-import Felix.Module
-import Felix.Meaning qualified as Meaning
-import Report.Location
-import Syntax.Abstract qualified as Raw
-import Syntax.Interface
-import 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)