Migrate to `Felix` namespaceHEADhotg

1 files changed, 751 insertions, 0 deletions

diff --git a/source/Felix/Checking/Exact/Datatype.hs b/source/Felix/Checking/Exact/Datatype.hs
new file mode 100644
index 0000000..be943cd
--- /dev/null
+++ b/source/Felix/Checking/Exact/Datatype.hs
@@ -0,0 +1,751 @@
+{-# 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)