Migrate to `Felix` namespaceHEADhotg

1 files changed, 0 insertions, 838 deletions

diff --git a/source/Checking/Exact/Inductive.hs b/source/Checking/Exact/Inductive.hs
deleted file mode 100644
index 441c773..0000000
--- a/source/Checking/Exact/Inductive.hs
+++ /dev/null
@@ -1,838 +0,0 @@
-{-# LANGUAGE DerivingStrategies #-}
-{-# LANGUAGE NoImplicitPrelude #-}
-
--- | Exact preparation and atomic publication of direct set inductives.
-module Checking.Exact.Inductive
-    ( PreparedExactInductive
-    , preparedExactInductiveCarrierId
-    , preparedExactInductiveCarrierType
-    , preparedExactInductiveCarrierBody
-    , preparedExactInductiveGuardTargets
-    , preparedExactInductiveFacts
-    , prepareExactInductive
-    , CheckedExactInductiveAuthorization
-    , lowerPreparedExactInductive
-    , authorizeCheckedExactInductive
-    , ExactInductiveError(..)
-    , exactInductiveErrorLocation
-    , renderExactInductiveError
-    ) where
-
-import Base hiding (Empty)
-import Checking.Authority
-import Checking.Core
-import Checking.Declaration qualified as Declaration
-import Checking.Exact.Global qualified as ExactGlobal
-import Checking.Exact.Vocabulary
-import Checking.Foundation
-import Checking.Identity
-import Checking.Semantic
-import Checking.Typed.Inductive qualified as Typed
-import Felix.Cache.Codec
-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 qualified as List
-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 Data.Vector qualified as Vector
-
-
-data PreparedExactInductive = PreparedExactInductive
-    !Location
-    !SemanticGlobalKey
-    !ObjectId
-    !(Maybe AssertedObject)
-    !SemanticName
-    !DeclarationSyntaxId
-    !(Typed.PreparedTypedInductive ObjectId)
-    ![SemanticFactOccurrenceFingerprint]
-
-data CheckedExactInductiveAuthorization =
-    CheckedExactInductiveAuthorization
-        !ObjectId
-        !(Typed.PreparedTypedInductive ObjectId)
-        ![SemanticFactOccurrenceFingerprint]
-        ![(Location, Declaration.PreparedVampireObligation Void ())]
-
-preparedExactInductiveCarrierId
-    :: PreparedExactInductive
-    -> ObjectId
-preparedExactInductiveCarrierId
-        (PreparedExactInductive
-            _location _key identity _asserted _alias _syntax _typed _guards) =
-    identity
-
-preparedExactInductiveCarrierType
-    :: PreparedExactInductive
-    -> CoreType
-preparedExactInductiveCarrierType
-        (PreparedExactInductive
-            _location _key _identity _asserted _alias _syntax typed _guards) =
-    Typed.typedInductiveCarrierType typed
-
-preparedExactInductiveCarrierBody
-    :: PreparedExactInductive
-    -> FrozenCheckedCore ObjectId
-preparedExactInductiveCarrierBody
-        (PreparedExactInductive
-            _location _key _identity _asserted _alias _syntax typed _guards) =
-    Typed.typedInductiveCarrierBody typed
-
-preparedExactInductiveGuardTargets
-    :: PreparedExactInductive
-    -> Vector.Vector (FrozenCheckedCore ObjectId)
-preparedExactInductiveGuardTargets
-        (PreparedExactInductive
-            _location _key _identity _asserted _alias _syntax typed _guards) =
-    Typed.typedInductiveGuardTargets typed
-
-preparedExactInductiveFacts
-    :: PreparedExactInductive
-    -> NonEmpty (Typed.PreparedTypedInductiveFact ObjectId)
-preparedExactInductiveFacts
-        (PreparedExactInductive
-            _location _key _identity _asserted _alias _syntax typed _guards) =
-    Typed.typedInductiveFacts typed
-
-data ExactInductiveError
-    = ExactInductiveUnsupportedBlock !Location
-    | ExactInductiveOccurrenceMissing !Location
-    | ExactInductiveOccurrenceAmbiguous !Location
-    | ExactInductiveHeadMismatch !Location
-    | ExactInductiveGlossFailed !Location !Meaning.GlossError
-    | ExactInductiveDuplicateParameter !Location !Internal.VarSymbol
-    | ExactInductiveDomainFreeVariable !Location !Internal.VarSymbol
-    | ExactInductiveDomainMentionsCarrier !Location
-    | ExactInductiveResultShape !Location
-    | ExactInductiveResultMentionsCarrier !Location
-    | ExactInductiveRecursiveTermMentionsCarrier !Location
-    | ExactInductiveRecursiveCarrierWrongArguments !Location
-    | ExactInductiveRecursiveCarrierOutsideMembership !Location
-    | ExactInductiveUnsupportedRecursiveCarrierContext !Location
-    | ExactInductiveFixedSemanticCollision !Location !SemanticGlobalKey
-    | ExactInductiveGlobalAlreadyVisible !Location !SemanticGlobalKey
-    | ExactInductiveGlobalNotVisible !Location !Internal.Symbol
-    | ExactInductiveGlobalAmbiguous !Location !Internal.Symbol
-    | ExactInductiveUnsupportedSymbol !Location !Internal.Symbol
-    | ExactInductiveGlobalContentInvalid !Location !CoreCheckError
-    | ExactInductivePreparationFailed
-        !Location
-        !Typed.TypedInductiveError
-    | ExactInductiveGuardMissing !Location
-    | ExactInductiveGuardAmbiguous !Location
-    deriving stock (Show, Eq)
-
-exactInductiveErrorLocation :: ExactInductiveError -> Location
-exactInductiveErrorLocation = \case
-    ExactInductiveUnsupportedBlock location -> location
-    ExactInductiveOccurrenceMissing location -> location
-    ExactInductiveOccurrenceAmbiguous location -> location
-    ExactInductiveHeadMismatch location -> location
-    ExactInductiveGlossFailed location _failure -> location
-    ExactInductiveDuplicateParameter location _parameter -> location
-    ExactInductiveDomainFreeVariable location _variable -> location
-    ExactInductiveDomainMentionsCarrier location -> location
-    ExactInductiveResultShape location -> location
-    ExactInductiveResultMentionsCarrier location -> location
-    ExactInductiveRecursiveTermMentionsCarrier location -> location
-    ExactInductiveRecursiveCarrierWrongArguments location -> location
-    ExactInductiveRecursiveCarrierOutsideMembership location -> location
-    ExactInductiveUnsupportedRecursiveCarrierContext location -> location
-    ExactInductiveFixedSemanticCollision location _key -> location
-    ExactInductiveGlobalAlreadyVisible location _key -> location
-    ExactInductiveGlobalNotVisible location _symbol -> location
-    ExactInductiveGlobalAmbiguous location _symbol -> location
-    ExactInductiveUnsupportedSymbol location _symbol -> location
-    ExactInductiveGlobalContentInvalid location _failure -> location
-    ExactInductivePreparationFailed location _failure -> location
-    ExactInductiveGuardMissing location -> location
-    ExactInductiveGuardAmbiguous location -> location
-
-renderExactInductiveError :: ExactInductiveError -> Text
-renderExactInductiveError failure =
-    locationToText (exactInductiveErrorLocation failure)
-        <> ": "
-        <> case failure of
-            ExactInductiveUnsupportedBlock{} ->
-                "this inductive source form is not supported by the typed checker"
-            ExactInductiveOccurrenceMissing{} ->
-                "the inductive declaration has no associated syntax occurrence"
-            ExactInductiveOccurrenceAmbiguous{} ->
-                "the inductive declaration has more than one semantic head"
-            ExactInductiveHeadMismatch{} ->
-                "the inductive head does not match its syntax occurrence"
-            ExactInductiveGlossFailed _location glossFailure ->
-                "inductive elaboration failed: " <> shown glossFailure
-            ExactInductiveDuplicateParameter _location parameter ->
-                "the inductive parameter is repeated: " <> shown parameter
-            ExactInductiveDomainFreeVariable _location variable ->
-                "the inductive domain contains an unbound variable: "
-                    <> shown variable
-            ExactInductiveDomainMentionsCarrier{} ->
-                "the inductive domain must be independent of its carrier"
-            ExactInductiveResultShape{} ->
-                "an inductive result must have the form t \\in F(args)"
-            ExactInductiveResultMentionsCarrier{} ->
-                "an inductive result term must not mention its carrier"
-            ExactInductiveRecursiveTermMentionsCarrier{} ->
-                "a recursive occurrence must be in the carrier of a membership premise"
-            ExactInductiveRecursiveCarrierWrongArguments{} ->
-                "the inductive carrier occurs with arguments other than its declared parameters"
-            ExactInductiveRecursiveCarrierOutsideMembership{} ->
-                "an inductive carrier occurrence must be in the set operand of a membership premise"
-            ExactInductiveUnsupportedRecursiveCarrierContext{} ->
-                "this recursive carrier context is outside the supported first-order set-term fragment"
-            ExactInductiveFixedSemanticCollision _location key ->
-                "the inductive carrier collides with fixed semantics for "
-                    <> shown key
-            ExactInductiveGlobalAlreadyVisible _location key ->
-                "the inductive carrier is already visible: " <> shown key
-            ExactInductiveGlobalNotVisible _location symbol ->
-                "an inductive source symbol is not visible: " <> shown symbol
-            ExactInductiveGlobalAmbiguous _location symbol ->
-                "an inductive source symbol has more than one meaning: "
-                    <> shown symbol
-            ExactInductiveUnsupportedSymbol _location symbol ->
-                "this inductive source symbol is not supported: "
-                    <> shown symbol
-            ExactInductiveGlobalContentInvalid _location coreFailure ->
-                "an inductive global has invalid checked content: "
-                    <> shown coreFailure
-            ExactInductivePreparationFailed _location typedFailure ->
-                "typed inductive preparation failed: " <> shown typedFailure
-            ExactInductiveGuardMissing{} ->
-                "an inductive domain guard has no visible authorized fact"
-            ExactInductiveGuardAmbiguous{} ->
-                "an inductive domain guard matches more than one visible fact"
-  where
-    shown :: Show value => value -> Text
-    shown = Text.pack . show
-
-type Prepare =
-    ExceptT
-        ExactInductiveError
-        (Declaration.LoweringDriver)
-
-prepareExactInductive
-    :: CheckedFoundation
-    -> Raw.Block
-    -> [CanonicalLexicalEntry]
-    -> Declaration.LoweringDriver
-        (Either ExactInductiveError PreparedExactInductive)
-prepareExactInductive foundation block entries =
-    Except.runExceptT do
-        (location, marker, rawInductive) <-
-            case block of
-                Raw.BlockInductive blockLocation _title blockMarker inductive ->
-                    pure (blockLocation, blockMarker, inductive)
-                _ ->
-                    Except.throwError
-                        (ExactInductiveUnsupportedBlock (locate block))
-        key <- validateOccurrence location rawInductive entries
-        when
-            (isJust (fixedSemanticMeaning key))
-            (Except.throwError
-                (ExactInductiveFixedSemanticCollision location key))
-        visible <-
-            Except.lift
-                (Declaration.resolveVisibleGlobalLowering key)
-        when (isJust visible)
-            (Except.throwError
-                (ExactInductiveGlobalAlreadyVisible location key))
-        internal <-
-            case Meaning.meaning [block] of
-                Right
-                    [Internal.BlockInductive
-                        _internalLocation _internalMarker inductive] ->
-                            pure inductive
-                Left failure ->
-                    Except.throwError
-                        (ExactInductiveGlossFailed location failure)
-                Right _ ->
-                    Except.throwError
-                        (ExactInductiveUnsupportedBlock location)
-        direct <-
-            Except.liftEither
-                (normalizeDirectInductive internal)
-        (sourceGlobals, globalTypes) <-
-            resolveSourceGlobals location internal direct
-        typed <-
-            Except.liftEither
-                (first
-                    (ExactInductivePreparationFailed location)
-                    (Typed.prepareTypedInductive
-                        (requireGlobalType globalTypes)
-                        foundation
-                        (`Map.lookup` sourceGlobals)
-                        marker
-                        direct))
-        guards <-
-            traverse
-                (resolveGuard location)
-                (Vector.toList
-                    (Typed.typedInductiveGuardTargets typed))
-        theory <- Except.lift Declaration.currentTheoryLowering
-        let carrierType = Typed.typedInductiveCarrierType typed
-            carrierBody = Typed.typedInductiveCarrierBody typed
-            carrierTerm = frozenCoreTerm carrierBody
-            identity =
-                transparentObjectId theory carrierType carrierTerm
-            content =
-                TransparentObjectContent theory carrierType carrierTerm
-            alias = case marker of
-                Raw.Marker name -> semanticName name
-        available <-
-            Except.lift
-                (Declaration.objectAvailableLowering identity)
-        let asserted
-                | available = Nothing
-                | otherwise = Just (assertedObject identity content)
-            syntax =
-                declarationSyntaxId
-                    (encodePreparedInductive key alias typed)
-        pure
-            (PreparedExactInductive
-                location
-                key
-                identity
-                asserted
-                alias
-                syntax
-                typed
-                guards)
-  where
-    requireGlobalType types identity =
-        fromMaybe
-            (impossible
-                "prepared inductive global has no checked type")
-            (Map.lookup identity types)
-
-validateOccurrence
-    :: Location
-    -> Raw.Inductive
-    -> [CanonicalLexicalEntry]
-    -> Prepare SemanticGlobalKey
-validateOccurrence location rawInductive entries = do
-    entry <-
-        case entries of
-            [] ->
-                Except.throwError
-                    (ExactInductiveOccurrenceMissing location)
-            [single] -> pure single
-            _ ->
-                Except.throwError
-                    (ExactInductiveOccurrenceAmbiguous location)
-    key <-
-        maybe
-            (Except.throwError
-                (ExactInductiveHeadMismatch location))
-            pure
-            (semanticGlobalKeyFromLexicalEntry entry)
-    let Raw.SymbolPattern headSymbol _parameters =
-            Raw.inductiveSymbolPattern rawInductive
-        expected =
-            SemanticExpressionFunction
-                (Raw.mixfixPattern headSymbol)
-    unless (key == expected)
-        (Except.throwError
-            (ExactInductiveHeadMismatch location))
-    pure key
-
-normalizeDirectInductive
-    :: Internal.Inductive
-    -> Either ExactInductiveError Typed.DirectInductive
-normalizeDirectInductive inductive = do
-    case firstDuplicate (Internal.inductiveParams inductive) of
-        Just duplicate ->
-            Left
-                (ExactInductiveDuplicateParameter
-                    (locate duplicate)
-                    duplicate)
-        Nothing -> pure ()
-    let parameters = Internal.inductiveParams inductive
-        parameterSet = Set.fromList parameters
-        domain = Internal.inductiveDomain inductive
-        carrier = Internal.inductiveSymbol inductive
-        domainVariables =
-            orderedUnique
-                (toList domain)
-    case find (`Set.notMember` parameterSet) domainVariables of
-        Just variable ->
-            Left
-                (ExactInductiveDomainFreeVariable
-                    (locate variable)
-                    variable)
-        Nothing -> pure ()
-    when
-        (Internal.SymbolMixfix carrier
-            `Set.member` Internal.mentionedSymbols domain)
-        (Left
-            (ExactInductiveDomainMentionsCarrier
-                (termLocation domain)))
-    clauses <-
-        traverse
-            (normalizeClause carrier parameters)
-            (Internal.inductiveIntros inductive)
-    pure
-        (Typed.DirectInductive
-            parameters
-            domain
-            clauses)
-
-normalizeClause
-    :: Internal.FunctionSymbol
-    -> [Internal.VarSymbol]
-    -> Internal.IntroRule
-    -> Either ExactInductiveError Typed.DirectInductiveClause
-normalizeClause carrier parameters rule = do
-    conditions <-
-        traverse
-            (normalizeCondition carrier parameters)
-            (Internal.introConditions rule)
-    result <-
-        normalizeResult
-            carrier
-            parameters
-            (Internal.introResult rule)
-    let parameterSet = Set.fromList parameters
-        variables =
-            List.filter (`Set.notMember` parameterSet)
-                (orderedUnique
-                    ( concatMap toList
-                        (Internal.introConditions rule)
-                      <> toList result
-                    ))
-    pure
-        (Typed.DirectInductiveClause
-            variables
-            conditions
-            result)
-
-normalizeResult
-    :: Internal.FunctionSymbol
-    -> [Internal.VarSymbol]
-    -> Internal.Formula
-    -> Either ExactInductiveError Internal.Term
-normalizeResult carrier parameters = \case
-    Internal.IsElementOf _location result target
-        | not (matchesCarrier carrier parameters target) ->
-            Left (ExactInductiveResultShape (termLocation target))
-        | Internal.SymbolMixfix carrier
-                `Set.member` Internal.mentionedSymbols result ->
-            Left
-                (ExactInductiveResultMentionsCarrier
-                    (termLocation result))
-        | otherwise ->
-            Right result
-    formula ->
-        Left (ExactInductiveResultShape (termLocation formula))
-
-normalizeCondition
-    :: Internal.FunctionSymbol
-    -> [Internal.VarSymbol]
-    -> Internal.Formula
-    -> Either ExactInductiveError Typed.DirectInductiveCondition
-normalizeCondition carrier parameters formula
-    | not
-        (Internal.SymbolMixfix carrier
-            `Set.member` Internal.mentionedSymbols formula) =
-        Right (Typed.DirectSideCondition formula)
-    | otherwise =
-        case formula of
-            Internal.IsElementOf _location recursiveTerm recursiveCarrier
-                | Internal.SymbolMixfix carrier
-                        `Set.member`
-                            Internal.mentionedSymbols recursiveTerm ->
-                    Left
-                        (ExactInductiveRecursiveTermMentionsCarrier
-                            (termLocation recursiveTerm))
-                | otherwise -> do
-                    context <-
-                        first recursiveCarrierContextError
-                            (Typed.prepareRecursiveCarrierContext
-                                carrier parameters recursiveCarrier)
-                    Right
-                        (Typed.DirectRecursiveCondition
-                            recursiveTerm context)
-            _ ->
-                Left
-                    (ExactInductiveRecursiveCarrierOutsideMembership
-                        (termLocation formula))
-
-recursiveCarrierContextError
-    :: Typed.RecursiveCarrierContextError
-    -> ExactInductiveError
-recursiveCarrierContextError = \case
-    Typed.RecursiveCarrierWrongArguments location ->
-        ExactInductiveRecursiveCarrierWrongArguments location
-    Typed.RecursiveCarrierUnsupportedContext location ->
-        ExactInductiveUnsupportedRecursiveCarrierContext location
-
-matchesCarrier
-    :: Internal.FunctionSymbol
-    -> [Internal.VarSymbol]
-    -> Internal.Term
-    -> Bool
-matchesCarrier carrier parameters = \case
-    Internal.TermSymbol _location (Internal.SymbolMixfix actual) arguments ->
-        actual == carrier
-            && length arguments == length parameters
-            && and
-                (zipWith
-                    (\argument parameter ->
-                        argument == Internal.TermVar parameter)
-                    arguments
-                    parameters)
-    _ -> False
-
-resolveSourceGlobals
-    :: Location
-    -> Internal.Inductive
-    -> Typed.DirectInductive
-    -> Prepare
-        ( Map.Map
-            Internal.Symbol
-            (Typed.SourceGlobal ObjectId)
-        , Map.Map ObjectId CoreType
-        )
-resolveSourceGlobals location internal direct =
-    Except.lift
-        (ExactGlobal.resolveExactSourceGlobals symbols)
-        >>= Except.liftEither
-            . first (exactGlobalError location)
-  where
-    carrier = Internal.SymbolMixfix (Internal.inductiveSymbol internal)
-    symbols =
-        Set.delete carrier (directSymbols direct)
-
-exactGlobalError
-    :: Location
-    -> ExactGlobal.ExactGlobalResolutionError
-    -> ExactInductiveError
-exactGlobalError location = \case
-    ExactGlobal.ExactGlobalNotVisible symbol ->
-        ExactInductiveGlobalNotVisible location symbol
-    ExactGlobal.ExactGlobalAmbiguous symbol ->
-        ExactInductiveGlobalAmbiguous location symbol
-    ExactGlobal.ExactGlobalUnsupported symbol ->
-        ExactInductiveUnsupportedSymbol location symbol
-    ExactGlobal.ExactGlobalContextualUnsupported symbol ->
-        ExactInductiveUnsupportedSymbol location symbol
-    ExactGlobal.ExactGlobalContentInvalid failure ->
-        ExactInductiveGlobalContentInvalid location failure
-
-resolveGuard
-    :: Location
-    -> FrozenCheckedCore ObjectId
-    -> Prepare SemanticFactOccurrenceFingerprint
-resolveGuard location target = do
-    matches <-
-        Except.lift
-            (Declaration.resolveVisibleFactTargetsLowering target)
-    case matches of
-        [] ->
-            Except.throwError (ExactInductiveGuardMissing location)
-        [fingerprint] ->
-            pure fingerprint
-        _ ->
-            Except.throwError (ExactInductiveGuardAmbiguous location)
-
-directSymbols :: Typed.DirectInductive -> Set.Set Internal.Symbol
-directSymbols direct =
-    Internal.mentionedSymbols (Typed.directInductiveDomain direct)
-        <> foldMap clauseSymbols
-            (Typed.directInductiveClauses direct)
-  where
-    clauseSymbols clause =
-        foldMap conditionSymbols
-                (Typed.directClauseConditions clause)
-            <> Internal.mentionedSymbols
-                (Typed.directClauseResult clause)
-    conditionSymbols = \case
-        Typed.DirectSideCondition formula ->
-            Internal.mentionedSymbols formula
-        Typed.DirectRecursiveCondition term context ->
-            Internal.mentionedSymbols term
-                <> Typed.recursiveCarrierContextSymbols context
-
-lowerPreparedExactInductive
-    :: PreparedExactInductive
-    -> Declaration.LoweringDriver
-        (Either
-            Declaration.DeclarationError
-            (Declaration.CheckedDeclaration
-                CheckedExactInductiveAuthorization))
-lowerPreparedExactInductive
-        (PreparedExactInductive
-            _location key identity asserted alias syntax typed guards) =
-    do
-        let facts = Typed.typedInductiveFacts typed
-            monotonicities =
-                Vector.toList
-                    (Typed.typedInductiveMonotonicities typed)
-            objects = maybeToList asserted
-        definition <-
-            Declaration.prepareDefinitionEquationSpecLowering
-                objects identity alias
-        preparedMonotonicities <-
-            traverse
-                (\monotonicity -> Except.runExceptT do
-                    let factLocation =
-                            Typed.typedInductiveMonotonicityLocation
-                                monotonicity
-                        target =
-                            Typed.typedInductiveMonotonicityTarget
-                                monotonicity
-                    spec <-
-                        Except.lift
-                            (Declaration.prepareFrozenCandidateSpecLowering
-                                objects target SearchIneligible [])
-                            >>= Except.liftEither
-                    obligation <-
-                        Except.lift
-                            (Declaration.prepareScopedVampireObligationLowering
-                                Vector.empty
-                                (embedClosedCore [] target)
-                                []
-                                []
-                                Declaration.VampireImplicitPremises)
-                            >>= either
-                                (Except.throwError
-                                    . Declaration.ProofObligationFailedAt
-                                        factLocation
-                                    . Declaration.CurrentCandidateVampirePreparationFailed)
-                                pure
-                    pure
-                        ( Declaration.checkedCandidate
-                            spec
-                            (Declaration.checkedSourceProofPlanning
-                                [ Declaration.checkedPlannedVampireRequest
-                                    factLocation obligation
-                                ]
-                                [])
-                        , (factLocation, obligation)
-                        ))
-                monotonicities
-        preparedCandidates <-
-            traverse
-                (\fact -> do
-                    prepared <-
-                        Declaration.prepareCandidateSpecLowering
-                            objects
-                            (embedClosedCore []
-                                (Typed.typedInductiveFactTarget fact))
-                            SearchEligible
-                            [markerAlias
-                                (Typed.typedInductiveFactMarker fact)]
-                    let descriptor =
-                            GuardedFoundationRules
-                                (guardedRuleSet
-                                    (Typed.typedInductiveFactRules fact))
-                        planning
-                            | null monotonicities =
-                                Declaration.checkedKernelPlanning
-                                    descriptor guards
-                            | otherwise =
-                                Declaration.checkedKernelPlanningWithStaged
-                                    descriptor
-                                    guards
-                                    (if Typed.typedInductiveFactRequiresMonotonicities
-                                            fact
-                                        then
-                                            [ Declaration.plannedEarlierCandidate
-                                                1 index
-                                            | (index, _target) <-
-                                                zip [0 ..] monotonicities
-                                            ]
-                                        else [])
-                    pure
-                        (fmap
-                            (\spec ->
-                                Declaration.checkedCandidate spec planning)
-                            prepared))
-                facts
-        pure do
-            definitionSpec <- definition
-            monotonicityCandidates <- sequence preparedMonotonicities
-            factCandidates <- sequence preparedCandidates
-            let stages
-                    | null monotonicityCandidates =
-                        [ Declaration.checkedCandidate definitionSpec
-                            (Declaration.checkedDefinitionEquationPlanning identity)
-                            :| toList factCandidates
-                        ]
-                    | otherwise =
-                        [ Declaration.checkedCandidate definitionSpec
-                            (Declaration.checkedDefinitionEquationPlanning identity)
-                            :| []
-                        , NonEmpty.fromList (fst <$> monotonicityCandidates)
-                        , factCandidates
-                        ]
-            pure
-                (Declaration.checkedCompiledDeclaration
-                    syntax
-                    objects
-                    []
-                    [semanticGlobalBinding key (GlobalReference identity)]
-                    []
-                    stages
-                    (CheckedExactInductiveAuthorization
-                        identity typed guards
-                        (snd <$> monotonicityCandidates)))
-  where
-    markerAlias (Raw.Marker name) =
-        semanticName name
-
-authorizeCheckedExactInductive
-    :: CheckedExactInductiveAuthorization
-    -> [NonEmpty Declaration.ReservedCandidate]
-    -> Declaration.Declaration ()
-authorizeCheckedExactInductive
-        (CheckedExactInductiveAuthorization
-            identity typed guards monotonicityObligations) = \case
-    [definitionCandidate :| candidates] -> do
-        unless (null monotonicityObligations)
-            (Declaration.failDeclaration
-                (Declaration.CheckedAuthorizationCandidateShapeMismatch 3 1))
-        Declaration.authorizeDefinitionEquationCandidate
-            identity definitionCandidate
-        let facts = Typed.typedInductiveFacts typed
-        case NonEmpty.nonEmpty candidates of
-            Just factCandidates
-                | NonEmpty.length factCandidates == NonEmpty.length facts ->
-                    sequence_
-                        (NonEmpty.zipWith
-                            (authorizeFact [])
-                            factCandidates
-                            facts)
-            _ ->
-                Declaration.failDeclaration
-                    (Declaration.CheckedAuthorizationCandidateShapeMismatch
-                        (1 + NonEmpty.length facts)
-                        (1 + length candidates))
-    [ definitionCandidate :| []
-      , monotonicityCandidates
-      , factCandidates
-      ]
-        | NonEmpty.length monotonicityCandidates
-                == length monotonicityObligations
-        , NonEmpty.length factCandidates
-                == NonEmpty.length (Typed.typedInductiveFacts typed) -> do
-            obligations <-
-                maybe
-                    (Declaration.failDeclaration
-                        (Declaration.CheckedAuthorizationCandidateShapeMismatch
-                            1 0))
-                    pure
-                    (NonEmpty.nonEmpty monotonicityObligations)
-            Declaration.authorizeDefinitionEquationCandidate
-                identity definitionCandidate
-            Declaration.authorizeVampireCandidateBatch
-                (NonEmpty.zipWith
-                    (\candidate (factLocation, obligation) ->
-                        (factLocation, candidate, pure obligation))
-                    monotonicityCandidates
-                    obligations)
-            sequence_
-                (NonEmpty.zipWith
-                    (\candidate fact ->
-                        authorizeFact
-                            (if Typed.typedInductiveFactRequiresMonotonicities
-                                    fact
-                                then NonEmpty.toList monotonicityCandidates
-                                else [])
-                            candidate
-                            fact)
-                    factCandidates
-                    (Typed.typedInductiveFacts typed))
-    stages ->
-        Declaration.failDeclaration
-            (Declaration.CheckedAuthorizationCandidateShapeMismatch
-                (if null monotonicityObligations then 1 else 3)
-                (length stages))
-  where
-    authorizeFact monotonicityCandidates candidate fact =
-        Declaration.authorizeKernelConstructionCandidate
-            (GuardedFoundationRules
-                (guardedRuleSet
-                    (Typed.typedInductiveFactRules fact)))
-            candidate do
-                traverse_ Declaration.useAuthorizedFact guards
-                traverse_
-                    Declaration.useStagedCandidate
-                    monotonicityCandidates
-                pure (Typed.typedInductiveFactDerivation fact)
-
-
-encodePreparedInductive
-    :: SemanticGlobalKey
-    -> SemanticName
-    -> Typed.PreparedTypedInductive ObjectId
-    -> ByteString
-encodePreparedInductive key alias typed =
-    encodeCache do
-        putCacheTag 0x04
-        putSemanticGlobalKeyCache key
-        putCoreTypeCache
-            (Typed.typedInductiveCarrierType typed)
-        putCanonicalTermCache putObjectIdCache
-            (frozenCoreTerm
-                (Typed.typedInductiveCarrierBody typed))
-        putCacheList putFrozenTerm
-            (Vector.toList
-                (Typed.typedInductiveContextInventory typed))
-        putCacheList
-            (putFrozenTerm
-                . Typed.typedInductiveMonotonicityTarget)
-            (Vector.toList
-                (Typed.typedInductiveMonotonicities typed))
-        putCacheText (semanticNameText alias)
-        putCacheList putFact
-            (toList (Typed.typedInductiveFacts typed))
-  where
-    putFrozenTerm =
-        putCanonicalTermCache putObjectIdCache . frozenCoreTerm
-
-    putFact fact = do
-        let Raw.Marker marker =
-                Typed.typedInductiveFactMarker fact
-        putCacheText marker
-        putCanonicalTermCache putObjectIdCache
-            (frozenCoreTerm
-                (Typed.typedInductiveFactTarget fact))
-        putCacheList
-            (putCacheBytes . encodeKernelRuleTag)
-            (toList (Typed.typedInductiveFactRules fact))
-
-firstDuplicate :: Ord value => [value] -> Maybe value
-firstDuplicate =
-    go Set.empty
-  where
-    go _seen [] = Nothing
-    go seen (value : remaining)
-        | value `Set.member` seen = Just value
-        | otherwise =
-            go (Set.insert value seen) remaining
-
-orderedUnique :: Ord value => [value] -> [value]
-orderedUnique =
-    reverse . snd . foldl' step (Set.empty, [])
-  where
-    step (seen, values) value
-        | value `Set.member` seen = (seen, values)
-        | otherwise =
-            (Set.insert value seen, value : values)
-
-termLocation :: Internal.Expr -> Location
-termLocation = Internal.exprLocation