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

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

-- | Exact lowering for the first ordinary theorem/proof fragment.
--
-- This module is the trusted owner of structural local-proof composition.  Its
-- private prepared tree controls when assumptions and proved local claims
-- become available and executes discharges depth-first.  The declaration
-- boundary validates typed tasks and authority; it does not reconstruct this
-- derivation.
module Felix.Checking.Exact.Proof
    ( PreparedExactProof
    , preparedExactProofSyntaxId
    , preparedExactProofFirstOmission
    , prepareExactProof
    , CheckedExactProofAuthorization
    , lowerPreparedExactProof
    , authorizeCheckedExactProof
    , PreparedFinalPreludeFoundationClaim
    , prepareFinalPreludeFoundationClaim
    , CheckedFinalPreludeFoundationAuthorization
    , lowerPreparedFinalPreludeFoundationClaim
    , authorizeCheckedFinalPreludeFoundationClaim
    , ExactProofError(..)
    , exactProofErrorLocation
    , renderExactProofError
    ) where

import Base
import Felix.Checking.Authority qualified as Authority
import Felix.Checking.Backend.Problem qualified as Backend
import Felix.Checking.Core
import Felix.Checking.Declaration qualified as Declaration
import Felix.Checking.Exact qualified as Exact
import Felix.Checking.Foundation
import Felix.Checking.Identity
import Felix.Checking.Kernel.Derivation (foundationFactDerivation)
import Felix.Checking.Kernel.Proof qualified as KernelProof
import Felix.Checking.SetConstruction
import Felix.Checking.Semantic
import Felix.Cache.Codec
import Felix.Report.Location
import Felix.Syntax.Abstract qualified as Raw

import Control.Monad.Except (ExceptT)
import Control.Monad.Except qualified as Except
import Control.Monad (foldM, unless, when)
import Control.Monad.State.Strict (StateT)
import Control.Monad.State.Strict qualified as State
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 Data.Vector (Vector)
import Data.Vector qualified as Vector
import Numeric.Natural (Natural)


data ExactProofError
    = ExactProofUnsupportedClaim !Location
    | ExactProofUnsupportedStep !Location
    | ExactProofSetInductionVariableRequired !Location
    | ExactProofSetInductionVariableNotActive
        !Location !Raw.VarSymbol
    | ExactProofSetInductionFocusAmbiguous !Location
    | ExactProofSetInductionActiveBinderIneligible
        !Location !Raw.VarSymbol
    | ExactProofSetInductionBinderConflict
        !Location !Raw.VarSymbol
    | ExactProofSetInductionGoalMismatch !Location
    | ExactProofSetExtensionalityGoalMismatch !Location
    | ExactProofSetExtensionalityDirectionsUnavailable !Location
    | ExactProofExpectedUniversalGoal !Location
    | ExactProofExpectedImplicationGoal !Location
    | ExactProofGoalStatementMismatch !Location
    | ExactProofEmptyCaseSplit !Location
    | ExactProofStructuralCompositionFailed
        !Location !KernelProof.KernelProofBuildError
    | ExactProofLocalFunctionBinderMismatch !Location
    | ExactProofLocalFunctionNameConflict !Location
    | ExactProofUnknownReference !Location !Raw.Marker
    | ExactProofElaborationFailed !Exact.ExactCompileError
    | ExactProofObligationPreparationFailed
        !Location
        !(Declaration.VampireObligationPreparationError
            Exact.ExactLocalId)
    | ExactProofFoundationLeafRequiresImplicitAuto !Location
    | ExactProofFoundationLeafTargetMismatch !Location
    | ExactProofFoundationLeafTargetAmbiguous !Location
    deriving stock (Show, Eq)

exactProofErrorLocation :: ExactProofError -> Location
exactProofErrorLocation = \case
    ExactProofUnsupportedClaim location -> location
    ExactProofUnsupportedStep location -> location
    ExactProofSetInductionVariableRequired location -> location
    ExactProofSetInductionVariableNotActive location _variable ->
        location
    ExactProofSetInductionFocusAmbiguous location -> location
    ExactProofSetInductionActiveBinderIneligible location _variable ->
        location
    ExactProofSetInductionBinderConflict location _variable ->
        location
    ExactProofSetInductionGoalMismatch location -> location
    ExactProofSetExtensionalityGoalMismatch location -> location
    ExactProofSetExtensionalityDirectionsUnavailable location -> location
    ExactProofExpectedUniversalGoal location -> location
    ExactProofExpectedImplicationGoal location -> location
    ExactProofGoalStatementMismatch location -> location
    ExactProofEmptyCaseSplit location -> location
    ExactProofStructuralCompositionFailed location _failure -> location
    ExactProofLocalFunctionBinderMismatch location -> location
    ExactProofLocalFunctionNameConflict location -> location
    ExactProofUnknownReference location _marker -> location
    ExactProofElaborationFailed failure ->
        Exact.exactCompileErrorLocation failure
    ExactProofObligationPreparationFailed location _failure -> location
    ExactProofFoundationLeafRequiresImplicitAuto location -> location
    ExactProofFoundationLeafTargetMismatch location -> location
    ExactProofFoundationLeafTargetAmbiguous location -> location

renderExactProofError :: ExactProofError -> Text
renderExactProofError = \case
    ExactProofUnsupportedClaim location ->
        at location <> "this claim is not yet supported by the typed checker"
    ExactProofUnsupportedStep location ->
        at location <> "this proof step is not yet supported by the typed checker"
    ExactProofSetInductionVariableRequired location ->
        at location <> "exact set induction requires a named set variable"
    ExactProofSetInductionVariableNotActive location variable ->
        at location <> "the set-induction variable " <> shown variable
            <> " is not an eligible exact focus"
    ExactProofSetInductionFocusAmbiguous location ->
        at location
            <> "set induction without an explicit variable has no unique focus"
    ExactProofSetInductionActiveBinderIneligible location variable ->
        at location <> "the active binder " <> shown variable
            <> " is not an eligible set-induction focus"
    ExactProofSetInductionBinderConflict location variable ->
        at location <> "the leading set-induction binder " <> shown variable
            <> " conflicts with an active exact binder"
    ExactProofSetInductionGoalMismatch location ->
        at location <> "the set-induction variable does not belong to this goal"
    ExactProofSetExtensionalityGoalMismatch location ->
        at location <> "set extensionality requires a set-equality goal"
    ExactProofSetExtensionalityDirectionsUnavailable location ->
        at location
            <> "set extensionality requires both directions as proved local claims"
    ExactProofExpectedUniversalGoal location ->
        at location <> "this fix step requires a universal goal"
    ExactProofExpectedImplicationGoal location ->
        at location <> "this assume step requires an implication goal"
    ExactProofGoalStatementMismatch location ->
        at location <> "the proof step does not match the current goal"
    ExactProofEmptyCaseSplit location ->
        at location <> "case analysis requires at least one case"
    ExactProofStructuralCompositionFailed location failure ->
        at location <> "invalid structural proof composition: " <> shown failure
    ExactProofLocalFunctionBinderMismatch location ->
        at location <> "the function argument must match its domain binder"
    ExactProofLocalFunctionNameConflict location ->
        at location <> "the function and argument names must be distinct"
    ExactProofUnknownReference location marker ->
        at location <> "the cited fact " <> shown marker <> " is not visible"
    ExactProofElaborationFailed failure ->
        Exact.renderExactCompileError failure
    ExactProofObligationPreparationFailed location failure ->
        at location <> "the exact proof obligation is invalid: " <> shown failure
    ExactProofFoundationLeafRequiresImplicitAuto location ->
        at location
            <> "a confined foundation claim requires an implicit Auto proof"
    ExactProofFoundationLeafTargetMismatch location ->
        at location <> "the claim does not exactly match a foundation axiom"
    ExactProofFoundationLeafTargetAmbiguous location ->
        at location <> "the claim matches more than one foundation axiom"
  where
    at location = locationToText location <> ": "
    shown :: Show value => value -> Text
    shown = Text.pack . show

data ExactLocalOrigin
    = ExactAssumption
    | ExactDerivedClaim
    | ExactLocalDefinition
    | ExactLocalConstructionExtensional
    | ExactLocalConstructionEquation
    deriving stock (Show, Eq, Ord)

data PreparedLocal = PreparedLocal
    !Backend.LocalPremiseOrdinal
    !ExactLocalOrigin
    !(Vector (Exact.ExactLocalId, CoreType))
    !(ScopedCheckedCore ObjectId)

data PreparedJustification
    = PreparedAuto
    | PreparedReferences
        !(NonEmpty SemanticFactOccurrenceFingerprint)
    | PreparedLocalOnly

data PreparedDischarge
    = PreparedVampireDischarge
        !Location
        !PreparedJustification
        !(ScopedCheckedCore ObjectId)
        !(Declaration.PreparedVampireObligation
            Exact.ExactLocalId
            ExactLocalOrigin)
    | PreparedSetExtensionality
        !Location
        !(ScopedCheckedCore ObjectId)

data PreparedCalculationLink = PreparedCalculationLink
    !(ScopedCheckedCore ObjectId)
    !PreparedDischarge

-- The private constructor stores every destination with the discharge derived
-- from its immediately preceding endpoint.  Planning and admission can
-- therefore traverse one immutable sequence without re-associating shapes.
data PreparedCalculation = PreparedCheckedCalculation
    !CoreType
    ![Exact.ExactLocalId]
    !(Maybe (ScopedCheckedCore ObjectId))
    !(ScopedCheckedCore ObjectId)
    !(NonEmpty PreparedCalculationLink)
    !(ScopedCheckedCore ObjectId)

data PreparedSinceEvidence
    = PreparedSinceExisting !PreparedLocal
    | PreparedSinceDischarged !PreparedDischarge !PreparedLocal

data PreparedCase = PreparedCase
    !(ScopedCheckedCore ObjectId)
    !PreparedProof

data PreparedCaseAnalysis = PreparedCaseAnalysis
    !(ScopedCheckedCore ObjectId)
    !(NonEmpty PreparedCase)
    !(ScopedCheckedCore ObjectId)
    !PreparedDischarge

data InitialSetInductionFocus = InitialSetInductionFocus
    !Raw.VarSymbol
    !Exact.ExactLocalId
    !Natural

data InitialSetInductionView = InitialSetInductionView
    ![InitialSetInductionFocus]
    !(Vector (Exact.ExactLocalId, CoreType))
    !(ScopedCheckedCore ObjectId)
    ![ScopedCheckedCore ObjectId]
    !(ScopedCheckedCore ObjectId)
    !(Maybe Raw.VarSymbol)

data SetInductionBoundary
    = InitialClaimInduction !InitialSetInductionView
    -- A direct source-statement goal may retain only its leading binder name.
    -- Recursive proof transformations deliberately discard this hint.
    | SourceStatementInduction !(Maybe Raw.VarSymbol)
    | RecursiveProofInduction

data SelectedSetInductionFocus
    = SelectedInitialSetInduction !InitialSetInductionFocus
    | SelectedLeadingSetInduction !(Maybe Raw.VarSymbol)

data PreparedSetInductionFocus
    = PreparedInitialSetInductionFocus
        !Exact.ExactLocalId
        !Natural
    | PreparedLeadingSetInductionFocus
        !Exact.ExactLocalId

data PreparedSetInduction = PreparedCheckedSetInduction
    !PreparedSetInductionFocus
    !(ScopedCheckedCore ObjectId)
    ![ScopedCheckedCore ObjectId]
    !(ScopedCheckedCore ObjectId)
    !(ScopedCheckedCore ObjectId)
    !(ScopedCheckedCore ObjectId)
    !PreparedProof

data PreparedProof
    = PreparedImplicitAuto !PreparedDischarge
    | PreparedQed !PreparedDischarge
    | PreparedOmitted
        !Location
        !(ScopedCheckedCore ObjectId)
    | PreparedFix ![Exact.ExactLocalId] !PreparedProof
    | PreparedAssume
        !(ScopedCheckedCore ObjectId)
        !PreparedProof
    | PreparedTake
        ![Exact.ExactLocalId]
        !(ScopedCheckedCore ObjectId)
        !PreparedDischarge
        !PreparedProof
    | PreparedSetInduction !PreparedSetInduction
    | PreparedHave
        !(ScopedCheckedCore ObjectId)
        !PreparedDischarge
        !PreparedProof
    | PreparedSuffices
        !(ScopedCheckedCore ObjectId)
        !(ScopedCheckedCore ObjectId)
        !(ScopedCheckedCore ObjectId)
        !PreparedDischarge
        !PreparedProof
    | PreparedCalculate
        !PreparedCalculation
        !PreparedProof
    | PreparedSince
        !(ScopedCheckedCore ObjectId)
        !PreparedSinceEvidence
        !(ScopedCheckedCore ObjectId)
        !PreparedDischarge
        !PreparedProof
    | PreparedSubclaim
        !(ScopedCheckedCore ObjectId)
        !PreparedProof
        !PreparedProof
    | PreparedDefine
        !Exact.ExactLocalId
        !(ScopedCheckedCore ObjectId)
        !(NonEmpty (ScopedCheckedCore ObjectId))
        !PreparedProof
    | PreparedDefineRelational
        !Exact.ExactLocalId
        !(ScopedCheckedCore ObjectId)
        !PreparedDischarge
        !(NonEmpty (ScopedCheckedCore ObjectId))
        !PreparedProof
    | PreparedDefineFunction
        !Exact.ExactLocalId
        !(ScopedCheckedCore ObjectId)
        !(ScopedCheckedCore ObjectId)
        !PreparedProof
    | PreparedByCase !PreparedCaseAnalysis
    | PreparedByContradiction
        !(ScopedCheckedCore ObjectId)
        !(ScopedCheckedCore ObjectId)
        !(ScopedCheckedCore ObjectId)
        !PreparedProof
    | PreparedContradiction
        !(ScopedCheckedCore ObjectId)
        !(ScopedCheckedCore ObjectId)
        !PreparedDischarge

data PreparedExactProof = PreparedExactProof
    !Location
    !SemanticName
    !(ScopedCheckedCore ObjectId)
    !PreparedProof
    !ProofSyntaxId

data PreparedFinalPreludeFoundationClaim =
    PreparedFinalPreludeFoundationClaim
    !Location
    !SemanticName
    !(ScopedCheckedCore ObjectId)
    !FoundationAxiomTag
    !ProofSyntaxId

preparedExactProofSyntaxId :: PreparedExactProof -> ProofSyntaxId
preparedExactProofSyntaxId
        (PreparedExactProof _location _alias _target _proof syntax) =
    syntax

preparedExactProofFirstOmission :: PreparedExactProof -> Maybe Location
preparedExactProofFirstOmission
        (PreparedExactProof _location _alias _target proof _syntax) =
    preparedProofFirstOmission proof

data PrepareState = PrepareState
    { prepareNextLocal :: !Natural
    , prepareNextPremise :: !Natural
    }

type Prepare =
    StateT
        PrepareState
        (ExceptT ExactProofError (Declaration.LoweringDriver))

prepareExactProof
    :: Raw.Block
    -> Maybe Raw.Proof
    -> Declaration.LoweringDriver
        (Either ExactProofError PreparedExactProof)
prepareExactProof block explicitProof =
    Except.runExceptT
        (State.evalStateT prepare initialState)
  where
    initialState = PrepareState 0 0

    prepare =
        case block of
            Raw.BlockClaim
                    _kind location _title (Raw.Marker marker)
                    (Raw.Claim assumptions statement) -> do
                envelope <-
                    liftDriver
                        (Exact.prepareExactClaimEnvelope assumptions statement)
                        >>= either
                            (throwProof . ExactProofElaborationFailed)
                            pure
                let targetCore = Exact.preparedExactClaimTarget envelope
                unless (null (scopedCoreContext targetCore))
                    (throwProof
                        (ExactProofUnsupportedClaim location))
                (context, openedGoal, identities) <-
                    openEnvelopeVariables
                        targetCore
                        (Exact.preparedExactClaimVariables envelope)
                        (Exact.preparedExactClaimContext envelope)
                (locals, bodyGoal, antecedents) <-
                    openEnvelopeAntecedents
                        context
                        openedGoal
                        (Exact.preparedExactClaimAntecedentCount envelope)
                initialInduction <-
                    prepareInitialSetInductionView
                        statement
                        context
                        (Exact.preparedExactClaimVariables envelope)
                        identities
                        antecedents
                        bodyGoal
                bodyProof <-
                    case explicitProof of
                        Nothing ->
                            PreparedImplicitAuto
                                <$> prepareDischarge
                                    location
                                    context
                                    locals
                                    bodyGoal
                                    Raw.JustificationEmpty
                        Just sourceProof ->
                            prepareProof
                                location
                                context
                                locals
                                (InitialClaimInduction initialInduction)
                                bodyGoal
                                sourceProof
                let withAssumptions =
                        foldr PreparedAssume bodyProof antecedents
                    proof =
                        case identities of
                            [] -> withAssumptions
                            _ -> PreparedFix identities withAssumptions
                pure
                    (PreparedExactProof
                        location
                        (semanticName marker)
                        targetCore
                        proof
                        (proofSyntaxId
                            (encodePreparedProof proof)))
            _ ->
                throwProof
                    (ExactProofUnsupportedClaim (locate block))

prepareFinalPreludeFoundationClaim
    :: CheckedFoundation
    -> Raw.Block
    -> Maybe Raw.Proof
    -> Declaration.LoweringDriver
        (Either ExactProofError PreparedFinalPreludeFoundationClaim)
prepareFinalPreludeFoundationClaim foundation block explicitProof =
    Except.runExceptT do
        case (block, explicitProof) of
            ( Raw.BlockClaim
                    _kind location _title (Raw.Marker marker)
                    (Raw.Claim assumptions statement)
              , Nothing
              ) -> do
                envelope <-
                    Except.lift
                        (Exact.prepareExactClaimEnvelope
                            assumptions
                            statement)
                        >>= either
                            (Except.throwError
                                . ExactProofElaborationFailed)
                            pure
                unless
                    ( null (Exact.preparedExactClaimVariables envelope)
                        && Exact.preparedExactClaimAntecedentCount envelope
                            == 0
                    )
                    (Except.throwError
                        (ExactProofFoundationLeafRequiresImplicitAuto
                            location))
                let target = Exact.preparedExactClaimTarget envelope
                    matches =
                        [ tag
                        | tag <- [minBound .. maxBound]
                        , target == foundationTarget tag
                        ]
                tag <- case matches of
                    [] ->
                        Except.throwError
                            (ExactProofFoundationLeafTargetMismatch location)
                    [only] ->
                        pure only
                    _ ->
                        Except.throwError
                            (ExactProofFoundationLeafTargetAmbiguous location)
                pure
                    (PreparedFinalPreludeFoundationClaim
                        location
                        (semanticName marker)
                        target
                        tag
                        (implicitAutoProofSyntaxId target))
            (Raw.BlockClaim _kind location _title _marker _claim, Just{}) ->
                Except.throwError
                    (ExactProofFoundationLeafRequiresImplicitAuto location)
            _ ->
                Except.throwError
                    (ExactProofUnsupportedClaim (locate block))
  where
    foundationTarget tag =
        embedClosedCore []
            (mapFrozenGlobals
                absurd
                (foundationAxiomFrozen foundation tag))

openEnvelopeVariables
    :: ScopedCheckedCore ObjectId
    -> [Raw.VarSymbol]
    -> Exact.ExactBinderContext
    -> Prepare
        ( Exact.ExactBinderContext
        , ScopedCheckedCore ObjectId
        , [Exact.ExactLocalId]
        )
openEnvelopeVariables target variables preparedContext =
    case NonEmpty.nonEmpty variables of
        Nothing ->
            pure (preparedContext, target, [])
        Just nonempty -> do
            (_unannotated, opened, identities) <-
                openFixedVariables
                Exact.emptyExactBinderContext
                target
                nonempty
            let expected =
                    reverse
                        (fst <$> toList
                            (Exact.exactBinderContextSupport preparedContext))
            unless
                (identities == expected)
                (impossible
                    "prepared claim annotations do not match opened binders")
            pure (preparedContext, opened, identities)

openEnvelopeAntecedents
    :: Exact.ExactBinderContext
    -> ScopedCheckedCore ObjectId
    -> Natural
    -> Prepare
        ( [PreparedLocal]
        , ScopedCheckedCore ObjectId
        , [ScopedCheckedCore ObjectId]
        )
openEnvelopeAntecedents context initialGoal initialCount =
    go [] [] initialGoal initialCount
  where
    go locals antecedents goal 0 =
        pure (locals, goal, antecedents)
    go locals antecedents goal remaining = do
        (antecedent, conclusion) <-
            maybe
                (impossible
                    "a prepared claim envelope has too few implications")
                pure
                (openScopedImplication goal)
        local <- allocateLocal ExactAssumption context antecedent
        go
            (locals <> [local])
            (antecedents <> [antecedent])
            conclusion
            (remaining - 1)

prepareInitialSetInductionView
    :: Raw.Stmt
    -> Exact.ExactBinderContext
    -> [Raw.VarSymbol]
    -> [Exact.ExactLocalId]
    -> [ScopedCheckedCore ObjectId]
    -> ScopedCheckedCore ObjectId
    -> Prepare InitialSetInductionView
prepareInitialSetInductionView
        statement context variables identities antecedents bodyGoal = do
    unless (length variables == length identities)
        (impossible
            "opened claim binders lost their source identity association")
    foci <- traverse checkedFocus (zip variables identities)
    let property = foldr implyChecked bodyGoal antecedents
        support = Exact.exactBinderContextSupport context
    unless
        ( scopedCoreContext property
            == (snd <$> Vector.toList support)
        )
        (impossible
            "initial set-induction property changed its checked context")
    pure
        (InitialSetInductionView
            foci support property antecedents bodyGoal
            (claimLeadingUniversalName statement))
  where
    checkedFocus (variable, identity) = do
        index <-
            maybe
                (impossible
                    "an opened claim binder is absent from its exact context")
                pure
                (Exact.exactBinderContextIndex variable context)
        case Exact.exactBinderContextSupport context
                Vector.!? (fromIntegral index) of
            Just (actualIdentity, TySet)
                | actualIdentity == identity ->
                    pure
                        (InitialSetInductionFocus
                            variable identity index)
            _ ->
                impossible
                    "an initial set-induction focus changed identity or type"

    implyChecked antecedent conclusion =
        fromMaybe
            (impossible
                "an exact claim antecedent changed context")
            (implyScopedCore antecedent conclusion)

claimLeadingUniversalName :: Raw.Stmt -> Maybe Raw.VarSymbol
claimLeadingUniversalName = \case
    Raw.StmtFormula
            (Raw.FormulaQuantified _location Raw.Universally
                (variable :| _rest) _bound _formula) ->
        Just variable
    Raw.SymbolicForall _location (variable :| _rest)
            _bound _suchThat _statement ->
        Just variable
    Raw.StmtQuantPhrase
            _location
            (Raw.QuantPhrase Raw.Universally
                (Raw.NounPhrase _left _noun variables _right _suchThat))
            _statement ->
        listToMaybe variables
    Raw.StmtVerbPhrase
            (Raw.TermQuantified Raw.Universally _location
                (Raw.NounPhrase _left _noun variable _right _suchThat)
                :| [])
            _verb ->
        variable
    Raw.StmtNoun
            (Raw.TermQuantified Raw.Universally _location
                (Raw.NounPhrase _left _noun variable _right _suchThat)
                :| [])
            _nounPhrase ->
        variable
    _statement ->
        Nothing

prepareProof
    :: Location
    -> Exact.ExactBinderContext
    -> [PreparedLocal]
    -> SetInductionBoundary
    -> ScopedCheckedCore ObjectId
    -> Raw.Proof
    -> Prepare PreparedProof
prepareProof fallback context locals inductionBoundary goal = \case
    Raw.Omitted location ->
        pure (PreparedOmitted location goal)
    Raw.Qed maybeLocation justification ->
        PreparedQed
            <$> prepareDischarge
                (fromMaybe fallback maybeLocation)
                context
                locals
                goal
                justification
    Raw.FixSymbolic location variables bound continuation -> do
        (context', goal', identities) <-
            openFixedVariables context goal variables
        case bound of
            Raw.Unbounded ->
                PreparedFix identities
                    <$> prepareProof
                        fallback
                        context'
                        locals
                        RecursiveProofInduction
                        goal'
                        continuation
            _ -> do
                constraint <-
                    prepareSymbolicBoundConstraints
                        context' variables bound
                prepareGuardedFix
                    fallback location context' locals goal'
                    identities constraint continuation
    Raw.FixSuchThat location variables statement continuation -> do
        (context', goal', identities) <-
            openFixedVariables context goal variables
        constraint <-
            Exact.preparedExactPropositionCore
                <$> prepareStatement context' statement
        prepareGuardedFix
            fallback location context' locals goal'
            identities constraint continuation
    Raw.Assume location statement continuation -> do
        supplied <- prepareStatement context statement
        when (isNothing (openScopedImplication goal))
            (throwProof (ExactProofExpectedImplicationGoal location))
        (assumption, conclusion) <-
            maybe
                (throwProof (ExactProofGoalStatementMismatch location))
                pure
                (openScopedAssumption
                    (Exact.preparedExactPropositionCore supplied)
                    goal)
        local <- allocateLocal ExactAssumption context assumption
        PreparedAssume assumption
            <$> prepareProof
                fallback
                context
                (locals <> [local])
                RecursiveProofInduction
                conclusion
                continuation
    Raw.TakeVar location variables bound statement justification continuation -> do
        prepareSymbolicTake
            fallback location context locals goal variables bound statement
            justification continuation
    Raw.TakeNoun location nounPhrase justification continuation ->
        prepareNounTake
            fallback location context locals goal nounPhrase
            justification continuation
    Raw.BySetInduction location variable continuation ->
        prepareSetInduction
            fallback location context locals inductionBoundary goal
            variable continuation
    Raw.Have location Nothing
            (Raw.SymbolicExists _existential variables bound statement)
            justification continuation ->
        prepareSymbolicTake
            fallback location context locals goal variables bound statement
            justification continuation
    Raw.Have location Nothing statement justification continuation -> do
        claim <-
            Exact.preparedExactPropositionCore
                <$> prepareStatement context statement
        discharge <-
            prepareDischarge
                location context locals claim justification
        local <- allocateLocal ExactDerivedClaim context claim
        PreparedHave claim discharge
            <$> prepareProof
                fallback
                context
                (locals <> [local])
                RecursiveProofInduction
                goal
                continuation
    Raw.Have location (Just sinceStatement)
            statement justification continuation -> do
        sinceProposition <-
            Exact.preparedExactPropositionCore
                <$> prepareStatement context sinceStatement
        claim <-
            Exact.preparedExactPropositionCore
                <$> prepareStatement context statement
        (evidence, sinceLocals) <-
            case find (localMatches sinceProposition) locals of
                Just existing ->
                    pure (PreparedSinceExisting existing, locals)
                Nothing -> do
                    discharge <-
                        prepareDischarge
                            location
                            context
                            locals
                            sinceProposition
                            Raw.JustificationLocal
                    local <-
                        allocateLocal
                            ExactDerivedClaim context sinceProposition
                    pure
                        ( PreparedSinceDischarged discharge local
                        , locals <> [local]
                        )
        claimDischarge <-
            prepareDischarge
                location context sinceLocals claim justification
        claimLocal <-
            allocateLocal ExactDerivedClaim context claim
        PreparedSince
            sinceProposition evidence claim claimDischarge
            <$> prepareProof
                fallback
                context
                (sinceLocals <> [claimLocal])
                RecursiveProofInduction
                goal
                continuation
    Raw.Suffices location statement justification continuation -> do
        reduction <-
            Exact.preparedExactPropositionCore
                <$> prepareStatement context statement
        implication <-
            maybe
                (impossible
                    "a checked suffices reduction changed lexical context")
                pure
                (implyScopedCore reduction goal)
        discharge <-
            prepareDischarge
                location context locals implication justification
        PreparedSuffices goal reduction implication discharge
            <$> prepareProof
                fallback
                context
                locals
                (SourceStatementInduction
                    (claimLeadingUniversalName statement))
                reduction
                continuation
    Raw.Calc location quantifier calculation continuation -> do
        prepared <-
            prepareCalculation
                location context locals quantifier calculation
        local <-
            allocateLocal
                ExactDerivedClaim
                context
                (preparedCalculationResult prepared)
        PreparedCalculate prepared
            <$> prepareProof
                fallback
                context
                (locals <> [local])
                RecursiveProofInduction
                goal
                continuation
    Raw.Subclaim location statement subproof continuation -> do
        claim <-
            Exact.preparedExactPropositionCore
                <$> prepareStatement context statement
        preparedSubproof <-
            prepareProof
                location
                context
                locals
                (SourceStatementInduction
                    (claimLeadingUniversalName statement))
                claim
                subproof
        local <- allocateLocal ExactDerivedClaim context claim
        PreparedSubclaim claim preparedSubproof
            <$> prepareProof
                fallback
                context
                (locals <> [local])
                RecursiveProofInduction
                goal
                continuation
    Raw.Define location variable expression continuation -> do
        preparedBody <-
            liftDriver
                (Exact.prepareExactSetExpression context expression)
                >>= either
                    (throwProof . ExactProofElaborationFailed)
                    pure
        let body = Exact.preparedExactSetExpressionCore preparedBody
        identity <- allocateLocalIdentity
        context' <-
            either
                (throwProof . ExactProofElaborationFailed)
                pure
                (Exact.extendExactBinderContext
                    ((identity, variable) :| [])
                    context)
        case Exact.preparedExactSetExpressionConstruction preparedBody of
            Nothing -> do
                separationCharacteristic <-
                    liftDriver
                        (Declaration.currentFoundationAxiomLowering
                            SeparationCharacteristic)
                definition <-
                    maybe
                        (impossible
                            "an exact set expression did not form a local definition")
                        pure
                        (scopedSetDefinition separationCharacteristic body)
                local <-
                    allocateLocal ExactLocalDefinition context' definition
                PreparedDefine identity body (definition :| [])
                    <$> prepareProof
                        fallback context' (locals <> [local])
                        RecursiveProofInduction
                        (weakenCheckedScopedCore TySet goal)
                        continuation
            Just (Exact.PreparedUnconditionalSetConstruction construction) -> do
                characteristics <- prepareConstructionFoundation
                (extensional, equation) <-
                    maybe
                        (impossible
                            "a checked named construction has no definition views")
                        pure
                        (namedSetConstructionLocalViews
                            characteristics construction)
                extensionalLocal <-
                    allocateLocal
                        ExactLocalConstructionExtensional context' extensional
                equationLocal <-
                    allocateLocal
                        ExactLocalConstructionEquation context' equation
                PreparedDefine identity body (extensional :| [equation])
                    <$> prepareProof
                        fallback context'
                        (locals <> [extensionalLocal, equationLocal])
                        RecursiveProofInduction
                        (weakenCheckedScopedCore TySet goal)
                        continuation
            Just (Exact.PreparedRelationalSetConstruction construction) -> do
                characteristics <- prepareConstructionFoundation
                let functionality =
                        relationalSetConstructionFunctionality construction
                discharge <-
                    prepareDischarge
                        location context locals functionality
                        Raw.JustificationEmpty
                (extensional, equation) <-
                    maybe
                        (impossible
                            "a checked relational construction has no admitted definition views")
                        pure
                        (relationalSetConstructionLocalViews
                            characteristics construction functionality)
                extensionalLocal <-
                    allocateLocal
                        ExactLocalConstructionExtensional context' extensional
                equationLocal <-
                    allocateLocal
                        ExactLocalConstructionEquation context' equation
                PreparedDefineRelational
                    identity body discharge (extensional :| [equation])
                    <$> prepareProof
                        fallback context'
                        (locals <> [extensionalLocal, equationLocal])
                        RecursiveProofInduction
                        (weakenCheckedScopedCore TySet goal)
                        continuation
    Raw.DefineFunction
            location function argument value bound domain continuation -> do
        unless (argument == bound)
            (throwProof
                (ExactProofLocalFunctionBinderMismatch (locate bound)))
        when (function == argument)
            (throwProof
                (ExactProofLocalFunctionNameConflict (locate function)))
        argumentIdentity <- allocateLocalIdentity
        argumentContext <-
            either
                (throwProof . ExactProofElaborationFailed)
                pure
                (Exact.extendExactBinderContext
                    ((argumentIdentity, argument) :| [])
                    context)
        graph <-
            liftDriver
                (Exact.prepareExactLocalFunctionGraph
                    location context argumentContext domain value)
                >>= either
                    (throwProof . ExactProofElaborationFailed)
                    pure
        functionIdentity <- allocateLocalIdentity
        functionContext <-
            either
                (throwProof . ExactProofElaborationFailed)
                pure
                (Exact.extendExactBinderContext
                    ((functionIdentity, function) :| [])
                    context)
        replacementCharacteristic <-
            liftDriver
                (Declaration.currentFoundationAxiomLowering
                    ReplacementCharacteristic)
        definition <-
            maybe
                (impossible
                    "a checked replacement graph did not form a local definition")
                pure
                (scopedCharacteristicDefinition
                    replacementCharacteristic
                    (Exact.preparedExactLocalFunctionGraphCore graph)
                    ( Exact.preparedExactLocalFunctionGraphDomain graph
                        :| [Exact.preparedExactLocalFunctionGraphMap graph]
                    ))
        local <-
            allocateLocal ExactLocalDefinition functionContext definition
        PreparedDefineFunction
            functionIdentity
            (Exact.preparedExactLocalFunctionGraphCore graph)
            definition
            <$> prepareProof
                fallback
                functionContext
                (locals <> [local])
                RecursiveProofInduction
                (weakenCheckedScopedCore TySet goal)
                continuation
    Raw.ByCase location sourceCases ->
        prepareByCase
            location context locals goal sourceCases
    Raw.ByContradiction location continuation -> do
        let falsum = falsumScopedCore (scopedCoreContext goal)
        negation <-
            maybe
                (structuralFailure
                    location
                    "proof by contradiction requires a proposition goal")
                pure
                (negateScopedCore goal)
        local <- allocateLocal ExactAssumption context negation
        prepared <-
            prepareProof
                location
                context
                (locals <> [local])
                RecursiveProofInduction
                falsum
                continuation
        validateStructuralComposition
            location [goal, negation, falsum]
            (\foundation globalType ->
                KernelProof.validateDoubleNegationComposition
                    foundation globalType goal negation falsum)
        pure
            (PreparedByContradiction
                goal negation falsum prepared)
    Raw.Contradiction location justification -> do
        let falsum = falsumScopedCore (scopedCoreContext goal)
        discharge <-
            prepareDischarge
                location
                context
                locals
                falsum
                justification
        validateStructuralComposition
            location [goal, falsum]
            (\foundation globalType ->
                KernelProof.validateFalsumEliminationComposition
                    foundation globalType goal falsum)
        pure (PreparedContradiction goal falsum discharge)
    proof ->
        throwProof
            (ExactProofUnsupportedStep
                (proofLocation fallback proof))
  where
    localMatches proposition
            (PreparedLocal _ordinal _origin _support local) =
        local == proposition

prepareSetInduction
    :: Location
    -> Location
    -> Exact.ExactBinderContext
    -> [PreparedLocal]
    -> SetInductionBoundary
    -> ScopedCheckedCore ObjectId
    -> Maybe Raw.Term
    -> Raw.Proof
    -> Prepare PreparedProof
prepareSetInduction
        fallback location context locals boundary goal sourceFocus
        continuation = do
    selected <-
        selectSetInductionFocus
            location context boundary goal sourceFocus
    case selected of
        SelectedInitialSetInduction
                (InitialSetInductionFocus _variable identity index) -> do
            (foci, expectedSupport, property, antecedents, childTarget) <-
                case boundary of
                    InitialClaimInduction
                            (InitialSetInductionView
                                foundFoci support foundProperty
                                foundAntecedents foundTarget _leadingName) ->
                        pure
                            ( foundFoci
                            , support
                            , foundProperty
                            , foundAntecedents
                            , foundTarget
                            )
                    RecursiveProofInduction ->
                        impossible
                            "an initial induction focus escaped its claim boundary"
                    SourceStatementInduction _leadingName ->
                        impossible
                            "an initial induction focus escaped its claim boundary"
            unless
                ( Exact.exactBinderContextSupport context == expectedSupport
                    && goal == childTarget
                    && any (sameInitialFocus identity index) foci
                )
                (throwProof
                    (ExactProofSetInductionGoalMismatch location))
            PreparedSetInduction
                <$> prepareCheckedSetInduction
                    fallback location context locals
                    (PreparedInitialSetInductionFocus identity index)
                    index property antecedents childTarget continuation
        SelectedLeadingSetInduction sourceName -> do
            (binderType, property) <-
                maybe
                    (throwProof
                        (ExactProofSetInductionGoalMismatch location))
                    pure
                    (openScopedForall goal)
            unless (binderType == TySet)
                (throwProof
                    (ExactProofSetInductionGoalMismatch location))
            identity <- allocateLocalIdentity
            extendedContext <-
                either
                    (throwProof . ExactProofElaborationFailed)
                    pure
                    (case sourceName of
                        Just variable ->
                            Exact.extendExactBinderContext
                                ((identity, variable) :| [])
                                context
                        Nothing ->
                            Exact.extendExactAnonymousBinderContext
                                identity context)
            let expectedResult = weakenCheckedScopedCore TySet goal
            prepared <- prepareCheckedSetInduction
                fallback location extendedContext locals
                (PreparedLeadingSetInductionFocus identity)
                0 property [] property continuation
            unless
                (preparedSetInductionResult prepared == expectedResult)
                (throwProof
                    (ExactProofSetInductionGoalMismatch location))
            pure (PreparedSetInduction prepared)
  where
    sameInitialFocus expectedIdentity expectedIndex
            (InitialSetInductionFocus _variable identity index) =
        identity == expectedIdentity && index == expectedIndex

prepareCheckedSetInduction
    :: Location
    -> Location
    -> Exact.ExactBinderContext
    -> [PreparedLocal]
    -> PreparedSetInductionFocus
    -> Natural
    -> ScopedCheckedCore ObjectId
    -> [ScopedCheckedCore ObjectId]
    -> ScopedCheckedCore ObjectId
    -> Raw.Proof
    -> Prepare PreparedSetInduction
prepareCheckedSetInduction
        fallback location context locals focus selected property antecedents
        childTarget continuation = do
    (_predicate, hypothesis, _step, result) <-
        maybe
            (throwProof
                (ExactProofSetInductionGoalMismatch location))
            pure
            (scopedSetInductionInstance selected property)
    validateStructuralComposition
        location
        (property : hypothesis : result : childTarget : antecedents)
        (\foundation globalType ->
            KernelProof.validateSetInductionComposition
                foundation globalType selected property antecedents
                childTarget hypothesis result)
    local <- allocateLocal ExactAssumption context hypothesis
    child <-
        prepareProof
            fallback
            context
            (locals <> [local])
            RecursiveProofInduction
            childTarget
            continuation
    pure
        (PreparedCheckedSetInduction
            focus property antecedents childTarget hypothesis result child)

preparedSetInductionResult
    :: PreparedSetInduction
    -> ScopedCheckedCore ObjectId
preparedSetInductionResult
        (PreparedCheckedSetInduction
            _focus _property _antecedents _target _hypothesis result _child) =
    result

selectSetInductionFocus
    :: Location
    -> Exact.ExactBinderContext
    -> SetInductionBoundary
    -> ScopedCheckedCore ObjectId
    -> Maybe Raw.Term
    -> Prepare SelectedSetInductionFocus
selectSetInductionFocus location context boundary goal sourceFocus = do
    explicit <- traverse simpleVariable sourceFocus
    let (initialFoci, retainedLeadingName) =
            case boundary of
                InitialClaimInduction
                        (InitialSetInductionView
                            foci _support _property _antecedents _target
                            leadingName) ->
                    (foci, leadingName)
                SourceStatementInduction leadingName ->
                    ([], leadingName)
                RecursiveProofInduction ->
                    ([], Nothing)
        leadingAvailable =
            case openScopedForall goal of
                Just (TySet, _body) -> True
                _ -> False
    case explicit of
        Just variable ->
            case find (initialNamed variable) initialFoci of
                Just focus ->
                    pure (SelectedInitialSetInduction focus)
                Nothing
                    | leadingAvailable
                    , isJust
                        (Exact.exactBinderContextIndex variable context) ->
                        throwProof
                            (ExactProofSetInductionBinderConflict
                                location variable)
                    | leadingAvailable ->
                        pure
                            (SelectedLeadingSetInduction
                                (Just variable))
                    | isJust
                        (Exact.exactBinderContextIndex variable context) ->
                        throwProof
                            (ExactProofSetInductionActiveBinderIneligible
                                location variable)
                    | otherwise ->
                        throwProof
                            (ExactProofSetInductionVariableNotActive
                                location variable)
        Nothing ->
            case
                ( (SelectedInitialSetInduction <$> initialFoci)
                    <> [ SelectedLeadingSetInduction retainedLeadingName
                       | leadingAvailable
                       ]
                ) of
                [only] -> pure only
                _ ->
                    throwProof
                        (ExactProofSetInductionFocusAmbiguous location)
  where
    simpleVariable = \case
        Raw.TermExpr (Raw.ExprVar variable) ->
            pure variable
        _term ->
            throwProof
                (ExactProofSetInductionVariableRequired location)

    initialNamed variable
            (InitialSetInductionFocus candidate _identity _index) =
        candidate == variable

prepareByCase
    :: Location
    -> Exact.ExactBinderContext
    -> [PreparedLocal]
    -> ScopedCheckedCore ObjectId
    -> [Raw.Case]
    -> Prepare PreparedProof
prepareByCase location context locals goal sourceCases = do
    cases <-
        maybe
            (throwProof (ExactProofEmptyCaseSplit location))
            (traverse prepareCase)
            (NonEmpty.nonEmpty sourceCases)
    exhaustive <-
        foldM disjoin
            (preparedCaseAssumption (NonEmpty.head cases))
            (preparedCaseAssumption <$> NonEmpty.tail cases)
    discharge <-
        prepareDischarge
            location context locals exhaustive Raw.JustificationEmpty
    validateStructuralComposition
        location
        (goal : exhaustive : (preparedCaseAssumption <$> toList cases))
        (\foundation globalType ->
            KernelProof.validateCaseAnalysisComposition
                foundation
                globalType
                goal
                (preparedCaseAssumption <$> cases)
                exhaustive)
    pure
        (PreparedByCase
            (PreparedCaseAnalysis goal cases exhaustive discharge))
  where
    prepareCase (Raw.Case statement child) = do
        assumption <-
            Exact.preparedExactPropositionCore
                <$> prepareStatement context statement
        local <- allocateLocal ExactAssumption context assumption
        prepared <-
            prepareProof
                (locate statement)
                context
                (locals <> [local])
                RecursiveProofInduction
                goal
                child
        pure (PreparedCase assumption prepared)

    disjoin left right =
        maybe
            (structuralFailure
                location
                "case assumptions changed type or lexical context")
            pure
            (disjoinScopedCore left right)

preparedCaseAssumption
    :: PreparedCase
    -> ScopedCheckedCore ObjectId
preparedCaseAssumption (PreparedCase assumption _proof) =
    assumption

preparedCaseProof :: PreparedCase -> PreparedProof
preparedCaseProof (PreparedCase _assumption proof) =
    proof

prepareGuardedFix
    :: Location
    -> Location
    -> Exact.ExactBinderContext
    -> [PreparedLocal]
    -> ScopedCheckedCore ObjectId
    -> [Exact.ExactLocalId]
    -> ScopedCheckedCore ObjectId
    -> Raw.Proof
    -> Prepare PreparedProof
prepareGuardedFix
        fallback location context locals goal identities constraint continuation = do
    (antecedent, conclusion) <-
        maybe
            (throwProof (ExactProofExpectedImplicationGoal location))
            pure
            (openScopedImplication goal)
    unless (constraint == antecedent)
        (throwProof (ExactProofGoalStatementMismatch location))
    local <- allocateLocal ExactAssumption context constraint
    prepared <-
        prepareProof
            fallback
            context
            (locals <> [local])
            RecursiveProofInduction
            conclusion
            continuation
    pure (PreparedFix identities (PreparedAssume constraint prepared))

prepareCalculation
    :: Location
    -> Exact.ExactBinderContext
    -> [PreparedLocal]
    -> Maybe Raw.CalcQuantifier
    -> Raw.Calc
    -> Prepare PreparedCalculation
prepareCalculation location context locals quantifier calculation = do
    (identities, calculationContext, calculationGuard) <-
        prepareCalculationScope context quantifier
    case calculation of
        Raw.Equation first destinations -> do
            firstChecked <- prepareSetEndpoint calculationContext first
            checkedDestinations <-
                traverse
                    (\(destination, justification) -> do
                        checked <-
                            prepareSetEndpoint calculationContext destination
                        pure
                            ( locate destination
                            , checked
                            , justification
                            ))
                    destinations
            finishCalculation
                location context locals TySet identities calculationGuard
                firstChecked checkedDestinations
        Raw.Biconditionals first destinations -> do
            firstChecked <- preparePropositionEndpoint calculationContext first
            checkedDestinations <-
                traverse
                    (\(destination, justification) -> do
                        checked <-
                            preparePropositionEndpoint
                                calculationContext destination
                        pure
                            ( locate destination
                            , checked
                            , justification
                            ))
                    destinations
            finishCalculation
                location context locals TyProp identities calculationGuard
                firstChecked checkedDestinations
  where
    prepareSetEndpoint endpointContext expression =
        Exact.preparedExactSetExpressionCore
            <$> ( liftDriver
                    (Exact.prepareExactSetExpression
                        endpointContext expression)
                    >>= either
                        (throwProof . ExactProofElaborationFailed)
                        pure
                )

    preparePropositionEndpoint endpointContext formula =
        Exact.preparedExactPropositionCore
            <$> prepareStatement endpointContext (Raw.StmtFormula formula)

prepareCalculationScope
    :: Exact.ExactBinderContext
    -> Maybe Raw.CalcQuantifier
    -> Prepare
        ( [Exact.ExactLocalId]
        , Exact.ExactBinderContext
        , Maybe (ScopedCheckedCore ObjectId)
        )
prepareCalculationScope context = \case
    Nothing ->
        pure ([], context, Nothing)
    Just (Raw.CalcQuantifier variables bound suchThat) -> do
        identities <- traverse (const allocateLocalIdentity) variables
        calculationContext <-
            either
                (throwProof . ExactProofElaborationFailed)
                pure
                (Exact.extendExactBinderContext
                    (NonEmpty.zip identities variables)
                    context)
        boundGuard <-
            prepareSymbolicBoundConstraints
                calculationContext variables bound
        suchThatGuard <-
            traverse
                (fmap Exact.preparedExactPropositionCore
                    . prepareStatement calculationContext)
                suchThat
        calculationGuard <-
            normalizeCalculationGuard
                (boundGuard : maybeToList suchThatGuard)
        pure (toList identities, calculationContext, calculationGuard)

normalizeCalculationGuard
    :: [ScopedCheckedCore ObjectId]
    -> Prepare (Maybe (ScopedCheckedCore ObjectId))
normalizeCalculationGuard guards =
    foldM add Nothing guards
  where
    add accumulated constraint
        | isScopedTruth constraint = pure accumulated
        | otherwise =
            case accumulated of
                Nothing -> pure (Just constraint)
                Just previous ->
                    Just
                        <$> maybe
                            (impossible
                                "checked calculation guards changed context")
                            pure
                            (conjoinScopedCore previous constraint)

    isScopedTruth proposition =
        scopedCoreType proposition == TyProp
            && scopedCoreTerm proposition == CImp CFalsum CFalsum

finishCalculation
    :: Location
    -> Exact.ExactBinderContext
    -> [PreparedLocal]
    -> CoreType
    -> [Exact.ExactLocalId]
    -> Maybe (ScopedCheckedCore ObjectId)
    -> ScopedCheckedCore ObjectId
    -> NonEmpty
        ( Location
        , ScopedCheckedCore ObjectId
        , Raw.Justification
        )
    -> Prepare PreparedCalculation
finishCalculation
        fallback context locals operandType identities calculationGuard
        first destinations = do
    links <- prepareCalculationLinks first destinations
    let finalEndpoint = preparedCalculationLinkDestination (NonEmpty.last links)
    resultOpen <-
        calculationEquality first finalEndpoint
    result <-
        closeCalculationProposition identities calculationGuard resultOpen
    pure
        (PreparedCheckedCalculation
            operandType identities calculationGuard first links result)
  where
    prepareCalculationLinks previous (destination :| rest) = do
        (next, firstLink) <- prepareCalculationLink previous destination
        later <- prepareRemainingCalculationLinks next rest
        pure (firstLink :| later)

    prepareRemainingCalculationLinks _previous [] =
        pure []
    prepareRemainingCalculationLinks previous (destination : rest) = do
        (next, link) <- prepareCalculationLink previous destination
        (link :) <$> prepareRemainingCalculationLinks next rest

    prepareCalculationLink previous
            (destinationLocation, destination, justification) = do
            linkOpen <- calculationEquality previous destination
            link <- closeCalculationProposition
                identities calculationGuard linkOpen
            discharge <-
                prepareDischarge
                    (if destinationLocation == Nowhere
                        then fallback
                        else destinationLocation)
                    context
                    locals
                    link
                    justification
            pure
                ( destination
                , PreparedCalculationLink destination discharge
                )

    calculationEquality left right =
        maybe
            (impossible
                "checked calculation endpoints changed type or context")
            pure
            (equalScopedCore left right)

closeCalculationProposition
    :: [Exact.ExactLocalId]
    -> Maybe (ScopedCheckedCore ObjectId)
    -> ScopedCheckedCore ObjectId
    -> Prepare (ScopedCheckedCore ObjectId)
closeCalculationProposition identities calculationGuard proposition = do
    guarded <-
        case calculationGuard of
            Nothing -> pure proposition
            Just constraint ->
                maybe
                    (impossible
                        "a checked calculation guard changed context")
                    pure
                    (implyScopedCore constraint proposition)
    pure (closeBinders (length identities) guarded)
  where
    closeBinders 0 closed = closed
    closeBinders remaining open =
        closeBinders (remaining - 1)
            (fromMaybe
                (impossible
                    "a checked calculation lost a quantified binder")
                (closeScopedForall open))

preparedCalculationResult
    :: PreparedCalculation
    -> ScopedCheckedCore ObjectId
preparedCalculationResult
        (PreparedCheckedCalculation
            _operandType _identities _guard _first _links result) =
    result

preparedCalculationLinkDestination
    :: PreparedCalculationLink
    -> ScopedCheckedCore ObjectId
preparedCalculationLinkDestination
        (PreparedCalculationLink destination _discharge) =
    destination

preparedCalculationLinkDischarge
    :: PreparedCalculationLink
    -> PreparedDischarge
preparedCalculationLinkDischarge
        (PreparedCalculationLink _destination discharge) =
    discharge

preparedDischargeGoal
    :: PreparedDischarge
    -> ScopedCheckedCore ObjectId
preparedDischargeGoal = \case
    PreparedVampireDischarge _location _justification goal _obligation ->
        goal
    PreparedSetExtensionality _location goal ->
        goal

prepareSymbolicBoundConstraints
    :: Exact.ExactBinderContext
    -> NonEmpty Raw.VarSymbol
    -> Raw.Bound
    -> Prepare (ScopedCheckedCore ObjectId)
prepareSymbolicBoundConstraints context variables bound =
    Exact.preparedExactPropositionCore
        <$> ( liftDriver
                (Exact.prepareExactSymbolicBoundConstraints
                    context variables bound)
                >>= either
                    (throwProof . ExactProofElaborationFailed)
                    pure
            )

prepareSymbolicTake
    :: Location
    -> Location
    -> Exact.ExactBinderContext
    -> [PreparedLocal]
    -> ScopedCheckedCore ObjectId
    -> NonEmpty Raw.VarSymbol
    -> Raw.Bound
    -> Raw.Stmt
    -> Raw.Justification
    -> Raw.Proof
    -> Prepare PreparedProof
prepareSymbolicTake
        fallback location context locals goal variables bound statement
        justification continuation = do
    identities <- traverse (const allocateLocalIdentity) variables
    context' <-
        either
            (throwProof . ExactProofElaborationFailed)
            pure
            (Exact.extendExactBinderContext
                (NonEmpty.zip identities variables)
                context)
    witness <-
        Exact.preparedExactPropositionCore
            <$> ( liftDriver
                    (Exact.prepareExactSymbolicWitnessConstraints
                        context' variables bound statement)
                    >>= either
                        (throwProof . ExactProofElaborationFailed)
                        pure
                )
    prepareTake
        fallback location context locals goal context'
        (toList identities) witness justification continuation

prepareNounTake
    :: Location
    -> Location
    -> Exact.ExactBinderContext
    -> [PreparedLocal]
    -> ScopedCheckedCore ObjectId
    -> Raw.NounPhrase []
    -> Raw.Justification
    -> Raw.Proof
    -> Prepare PreparedProof
prepareNounTake
        fallback location context locals goal nounPhrase
        justification continuation = do
    (identities, context') <-
        case nounPhrase of
            Raw.NounPhrase _left _noun variables _right _suchThat ->
                case NonEmpty.nonEmpty variables of
                    Just binders -> do
                        identities <-
                            traverse (const allocateLocalIdentity) binders
                        context' <-
                            either
                                (throwProof . ExactProofElaborationFailed)
                                pure
                                (Exact.extendExactBinderContext
                                    (NonEmpty.zip identities binders)
                                    context)
                        pure (toList identities, context')
                    Nothing -> do
                        identity <- allocateLocalIdentity
                        context' <-
                            either
                                (throwProof . ExactProofElaborationFailed)
                                pure
                                (Exact.extendExactAnonymousBinderContext
                                    identity context)
                        pure ([identity], context')
    witness <-
        Exact.preparedExactPropositionCore
            <$> ( liftDriver
                    (Exact.prepareExactNounWitnessConstraints
                        context' nounPhrase)
                    >>= either
                        (throwProof . ExactProofElaborationFailed)
                        pure
                )
    prepareTake
        fallback location context locals goal context'
        identities witness justification continuation

prepareTake
    :: Location
    -> Location
    -> Exact.ExactBinderContext
    -> [PreparedLocal]
    -> ScopedCheckedCore ObjectId
    -> Exact.ExactBinderContext
    -> [Exact.ExactLocalId]
    -> ScopedCheckedCore ObjectId
    -> Raw.Justification
    -> Raw.Proof
    -> Prepare PreparedProof
prepareTake
        fallback location context locals goal witnessContext
        identities witness justification continuation = do
    let witnessCount = length identities
        existence = closeTakenWitnesses witnessCount witness
        goal' = weakenForTakenWitnesses witnessCount goal
    discharge <-
        prepareDischarge
            location context locals existence justification
    local <- allocateLocal ExactAssumption witnessContext witness
    PreparedTake identities witness discharge
        <$> prepareProof
            fallback
            witnessContext
            (locals <> [local])
            RecursiveProofInduction
            goal'
            continuation

-- The discharged existential and the opened witness premise are the same
-- checked proposition viewed on opposite sides of existential elimination.
closeTakenWitnesses
    :: Int
    -> ScopedCheckedCore ObjectId
    -> ScopedCheckedCore ObjectId
closeTakenWitnesses binderCount = go binderCount
  where
    go 0 proposition = proposition
    go remaining proposition =
        go (remaining - 1)
            (fromMaybe
                (impossible "a taken witness has no checked binder")
                (closeScopedExists proposition))

weakenForTakenWitnesses
    :: Int
    -> ScopedCheckedCore ObjectId
    -> ScopedCheckedCore ObjectId
weakenForTakenWitnesses binderCount = go binderCount
  where
    go 0 proposition = proposition
    go remaining proposition =
        go (remaining - 1)
            (weakenCheckedScopedCore TySet proposition)

openFixedVariables
    :: Exact.ExactBinderContext
    -> ScopedCheckedCore ObjectId
    -> NonEmpty Raw.VarSymbol
    -> Prepare
        ( Exact.ExactBinderContext
        , ScopedCheckedCore ObjectId
        , [Exact.ExactLocalId]
        )
openFixedVariables initialContext initialGoal variables =
    foldM openOne
        (initialContext, initialGoal, [])
        (toList variables)
  where
    openOne (context, goal, identities) variable = do
        (binderType, body) <-
            maybe
                (throwProof
                    (ExactProofExpectedUniversalGoal
                        (locate variable)))
                pure
                (openScopedForall goal)
        unless (binderType == TySet)
            (throwProof
                (ExactProofExpectedUniversalGoal
                    (locate variable)))
        identity <- allocateLocalIdentity
        context' <-
            either
                (throwProof . ExactProofElaborationFailed)
                pure
                (Exact.extendExactBinderContext
                    ((identity, variable) :| [])
                    context)
        pure (context', body, identities <> [identity])

allocateLocalIdentity :: Prepare Exact.ExactLocalId
allocateLocalIdentity = do
    state <- State.get
    State.put
        state
            { prepareNextLocal = prepareNextLocal state + 1
            }
    pure (Exact.exactLocalId (prepareNextLocal state))

allocateLocal
    :: ExactLocalOrigin
    -> Exact.ExactBinderContext
    -> ScopedCheckedCore ObjectId
    -> Prepare PreparedLocal
allocateLocal origin context proposition = do
    state <- State.get
    State.put
        state
            { prepareNextPremise = prepareNextPremise state + 1
            }
    pure
        (PreparedLocal
            (Backend.localPremiseOrdinal
                (prepareNextPremise state))
            origin
            (Exact.exactBinderContextSupport context)
            proposition)

prepareConstructionFoundation
    :: Prepare SetConstructionFoundation
prepareConstructionFoundation = do
    familyUnion <- foundation FamilyUnionCharacteristic
    separation <- foundation SeparationCharacteristic
    replacement <- foundation ReplacementCharacteristic
    setChoose <- foundation SetChooseWitness
    pure
        (setConstructionFoundation
            familyUnion separation replacement setChoose)
  where
    foundation tag =
        liftDriver
            (Declaration.currentFoundationAxiomLowering tag)

prepareDischarge
    :: Location
    -> Exact.ExactBinderContext
    -> [PreparedLocal]
    -> ScopedCheckedCore ObjectId
    -> Raw.Justification
    -> Prepare PreparedDischarge
prepareDischarge location context locals goal justification =
    prepareDischargeWith
        (dischargeModeFor goal)
        [] Nothing location context locals goal justification

-- A contradictory-axioms answer can establish falsum, but never an unrelated
-- proposition directly. Derive that distinction from the checked target so
-- every surface proof spelling reaches the same guarded request path.
dischargeModeFor :: ScopedCheckedCore ObjectId -> DischargeMode
dischargeModeFor goal
    | scopedCoreType goal == TyProp
    , scopedCoreTerm goal == CFalsum =
        IndirectContradictionDischarge
    | otherwise =
        DirectDischarge

data DischargeMode
    = DirectDischarge
    | IndirectContradictionDischarge

prepareDischargeWith
    :: DischargeMode
    -> [FoundationAxiomTag]
    -> Maybe Declaration.VampirePremiseSelection
    -> Location
    -> Exact.ExactBinderContext
    -> [PreparedLocal]
    -> ScopedCheckedCore ObjectId
    -> Raw.Justification
    -> Prepare PreparedDischarge
prepareDischargeWith
        dischargeMode auxiliaries selectionOverride
        location context locals goal justification =
    case justification of
        Raw.JustificationSetExt -> do
            (leftToRight, rightToLeft) <-
                maybe
                    (throwProof
                        (ExactProofSetExtensionalityGoalMismatch location))
                    pure
                    (splitScopedSetEquality goal)
            unless
                ( hasDerivedLocal leftToRight
                    && hasDerivedLocal rightToLeft
                )
                (throwProof
                    (ExactProofSetExtensionalityDirectionsUnavailable
                        location))
            pure (PreparedSetExtensionality location goal)
        _ -> do
            preparedJustification <-
                prepareJustification location justification
            prepared <-
                liftDriver
                    (prepareObligation
                        (Exact.exactBinderContextSupport context)
                        goal
                        (toScopedPremise <$> locals)
                        auxiliaries
                        (fromMaybe
                            (vampirePremiseSelection preparedJustification)
                            selectionOverride))
                    >>= either
                        (throwProof
                            . ExactProofObligationPreparationFailed location)
                        pure
            pure
                (PreparedVampireDischarge
                    location
                    preparedJustification
                    goal
                    prepared)
  where
    prepareObligation =
        case dischargeMode of
            DirectDischarge ->
                Declaration.prepareScopedVampireObligationLowering
            IndirectContradictionDischarge ->
                Declaration.prepareScopedContradictionObligationLowering

    hasDerivedLocal proposition =
        any
            (\case
                PreparedLocal
                        _ordinal ExactDerivedClaim _support local ->
                    local == proposition
                PreparedLocal{} ->
                    False)
            locals

    toScopedPremise
            (PreparedLocal ordinal origin support proposition) =
        Declaration.scopedVampirePremise
            ordinal origin support proposition

prepareJustification
    :: Location
    -> Raw.Justification
    -> Prepare PreparedJustification
prepareJustification _location Raw.JustificationEmpty =
    pure PreparedAuto
prepareJustification location (Raw.JustificationRef markers) = do
    resolved <- traverse (resolveReference location) (toList markers)
    let unique = stableUnique resolved
    case unique of
        [] ->
            impossible "a nonempty citation list resolved to no facts"
        first : rest ->
            pure (PreparedReferences (first :| rest))
prepareJustification _location Raw.JustificationLocal =
    pure PreparedLocalOnly
prepareJustification location Raw.JustificationSetExt =
    throwProof (ExactProofUnsupportedStep location)

vampirePremiseSelection
    :: PreparedJustification
    -> Declaration.VampirePremiseSelection
vampirePremiseSelection = \case
    PreparedAuto ->
        Declaration.VampireImplicitPremises
    PreparedReferences fingerprints ->
        Declaration.VampireExplicitPremises fingerprints
    PreparedLocalOnly ->
        Declaration.VampireLocalPremises

resolveReference
    :: Location
    -> Raw.Marker
    -> Prepare SemanticFactOccurrenceFingerprint
resolveReference location marker@(Raw.Marker name) = do
    resolved <-
        liftDriver
            (Declaration.resolveVisibleFactAliasLowering
                (semanticName name))
    maybe
        (throwProof
            (ExactProofUnknownReference location marker))
        pure
        resolved

prepareStatement
    :: Exact.ExactBinderContext
    -> Raw.Stmt
    -> Prepare Exact.PreparedExactProposition
prepareStatement context statement =
    liftDriver
        (Exact.prepareExactProposition context statement)
        >>= either
            (throwProof . ExactProofElaborationFailed)
            pure

validateStructuralComposition
    :: Location
    -> [ScopedCheckedCore ObjectId]
    -> ( CheckedFoundation
         -> (ObjectId -> Maybe CoreType)
         -> Either KernelProof.KernelProofBuildError ()
       )
    -> Prepare ()
validateStructuralComposition location propositions validate = do
    foundation <-
        liftDriver Declaration.currentFoundationLowering
    let identities =
            Set.toAscList
                (Set.unions
                    ( canonicalTermGlobals . scopedCoreTerm
                        <$> propositions
                    ))
    types <-
        traverse
            (\identity -> do
                coreType <-
                    liftDriver
                        (Declaration.objectTypeLowering identity)
                maybe
                    (impossible
                        "a checked structural proof lost a global object")
                    (\availableType -> pure (identity, availableType))
                    coreType)
            identities
    either
        (throwProof
            . ExactProofStructuralCompositionFailed location)
        pure
        (validate foundation
            (\identity -> Map.lookup identity (Map.fromList types)))

structuralFailure :: Location -> Text -> Prepare value
structuralFailure location message =
    throwProof
        (ExactProofStructuralCompositionFailed
            location
            (KernelProof.ProofStructuralCompositionMismatch message))

data CheckedExactProofAuthorization = CheckedExactProofAuthorization
    !PreparedProof
    !Bool

lowerPreparedExactProof
    :: PreparedExactProof
    -> Declaration.LoweringDriver
        (Either
            Declaration.DeclarationError
            (Declaration.CheckedDeclaration CheckedExactProofAuthorization))
lowerPreparedExactProof
        (PreparedExactProof _location alias target proof syntax) =
    fmap checked
        <$> Declaration.prepareCandidateSpecLowering
            [] target SearchEligible [alias]
  where
    checked spec =
        Declaration.checkedProofDeclaration
            syntax [] [] [] []
            [Declaration.checkedCandidate spec planning :| []]
            (CheckedExactProofAuthorization
                proof
                (isJust (preparedProofFirstOmission proof)))
      where
        requests = plannedProofRequests proof
        planning
            | isJust (preparedProofFirstOmission proof) =
                Declaration.checkedOmittedPlanning requests []
            | otherwise =
                Declaration.checkedSourceProofPlanning requests []

authorizeCheckedExactProof
    :: CheckedExactProofAuthorization
    -> [NonEmpty Declaration.ReservedCandidate]
    -> Declaration.Declaration ()
authorizeCheckedExactProof
        (CheckedExactProofAuthorization proof hasOmission) = \case
    [candidate :| []]
        | hasOmission ->
            Declaration.authorizeOmittedCandidate
                candidate
                (executePreparedProof proof)
        | otherwise ->
            Declaration.authorizeVampireCandidate
                candidate
                (executePreparedProof proof)
    stages ->
        Declaration.failDeclaration
            (Declaration.CheckedAuthorizationCandidateShapeMismatch
                1 (length stages))

data CheckedFinalPreludeFoundationAuthorization =
    CheckedFinalPreludeFoundationAuthorization !FoundationAxiomTag

lowerPreparedFinalPreludeFoundationClaim
    :: PreparedFinalPreludeFoundationClaim
    -> Declaration.LoweringDriver
        (Either
            Declaration.DeclarationError
            (Declaration.CheckedDeclaration
                CheckedFinalPreludeFoundationAuthorization))
lowerPreparedFinalPreludeFoundationClaim
        (PreparedFinalPreludeFoundationClaim
            _location alias target tag syntax) =
    fmap checked
        <$> Declaration.prepareCandidateSpecLowering
            [] target SearchEligible [alias]
  where
    checked spec =
        Declaration.checkedProofDeclaration
            syntax [] [] [] []
            [ Declaration.checkedCandidate spec
                (Declaration.checkedKernelPlanning
                    (Authority.FoundationLeaf tag) [])
                :| []
            ]
            (CheckedFinalPreludeFoundationAuthorization tag)

authorizeCheckedFinalPreludeFoundationClaim
    :: CheckedFinalPreludeFoundationAuthorization
    -> [NonEmpty Declaration.ReservedCandidate]
    -> Declaration.Declaration ()
authorizeCheckedFinalPreludeFoundationClaim
        (CheckedFinalPreludeFoundationAuthorization tag) = \case
    [candidate :| []] ->
        Declaration.authorizeKernelConstructionCandidate
            (Authority.FoundationLeaf tag)
            candidate
            (pure (foundationFactDerivation tag))
    stages ->
        Declaration.failDeclaration
            (Declaration.CheckedAuthorizationCandidateShapeMismatch
                1 (length stages))

preparedProofFirstOmission :: PreparedProof -> Maybe Location
preparedProofFirstOmission = \case
    PreparedImplicitAuto{} -> Nothing
    PreparedQed{} -> Nothing
    PreparedOmitted location _goal -> Just location
    PreparedFix _identities continuation ->
        preparedProofFirstOmission continuation
    PreparedAssume _antecedent continuation ->
        preparedProofFirstOmission continuation
    PreparedTake _identities _witness _discharge continuation ->
        preparedProofFirstOmission continuation
    PreparedSetInduction
            (PreparedCheckedSetInduction
                _focus _property _antecedents _target
                _hypothesis _result child) ->
        preparedProofFirstOmission child
    PreparedHave _claim _discharge continuation ->
        preparedProofFirstOmission continuation
    PreparedSuffices _goal _reduction _implication _discharge continuation ->
        preparedProofFirstOmission continuation
    PreparedCalculate _calculation continuation ->
        preparedProofFirstOmission continuation
    PreparedSince _since _evidence _claim _discharge continuation ->
        preparedProofFirstOmission continuation
    PreparedSubclaim _claim subproof continuation ->
        preparedProofFirstOmission subproof
            <|> preparedProofFirstOmission continuation
    PreparedDefine _identity _body _definition continuation ->
        preparedProofFirstOmission continuation
    PreparedDefineRelational
            _identity _body _functionality _definitions continuation ->
        preparedProofFirstOmission continuation
    PreparedDefineFunction _identity _graph _definition continuation ->
        preparedProofFirstOmission continuation
    PreparedByCase (PreparedCaseAnalysis _goal cases _exhaustive _discharge) ->
        foldr
            ((<|>) . preparedProofFirstOmission . preparedCaseProof)
            Nothing
            cases
    PreparedByContradiction _goal _negation _falsum child ->
        preparedProofFirstOmission child
    PreparedContradiction{} -> Nothing

plannedProofRequests
    :: PreparedProof
    -> [Declaration.CheckedPlannedVampireRequest]
plannedProofRequests = \case
    PreparedImplicitAuto discharge -> plannedDischargeRequests discharge
    PreparedQed discharge -> plannedDischargeRequests discharge
    PreparedOmitted{} -> []
    PreparedFix _identities continuation ->
        plannedProofRequests continuation
    PreparedAssume _antecedent continuation ->
        plannedProofRequests continuation
    PreparedTake _identities _witness discharge continuation ->
        plannedDischargeRequests discharge <> plannedProofRequests continuation
    PreparedSetInduction
            (PreparedCheckedSetInduction
                _focus _property _antecedents _target
                _hypothesis _result child) ->
        plannedProofRequests child
    PreparedHave _claim discharge continuation ->
        plannedDischargeRequests discharge <> plannedProofRequests continuation
    PreparedSuffices _goal _reduction _implication discharge continuation ->
        plannedDischargeRequests discharge <> plannedProofRequests continuation
    PreparedCalculate calculation continuation ->
        plannedCalculationRequests calculation
            <> plannedProofRequests continuation
    PreparedSince _since evidence _claim discharge continuation ->
        plannedSinceEvidenceRequests evidence
            <> plannedDischargeRequests discharge
            <> plannedProofRequests continuation
    PreparedSubclaim _claim subproof continuation ->
        plannedProofRequests subproof <> plannedProofRequests continuation
    PreparedDefine _identity _body _definition continuation ->
        plannedProofRequests continuation
    PreparedDefineRelational
            _identity _body functionality _definitions continuation ->
        plannedDischargeRequests functionality
            <> plannedProofRequests continuation
    PreparedDefineFunction _identity _graph _definition continuation ->
        plannedProofRequests continuation
    PreparedByCase
            (PreparedCaseAnalysis _goal cases _exhaustive discharge) ->
        concatMap
            (plannedProofRequests . preparedCaseProof)
            (toList cases)
            <> plannedDischargeRequests discharge
    PreparedByContradiction _goal _negation _falsum child ->
        plannedProofRequests child
    PreparedContradiction _goal _falsum discharge ->
        plannedDischargeRequests discharge

plannedDischargeRequests
    :: PreparedDischarge
    -> [Declaration.CheckedPlannedVampireRequest]
plannedDischargeRequests = \case
    PreparedVampireDischarge location _justification _goal obligation ->
        [Declaration.checkedPlannedVampireRequest location obligation]
    PreparedSetExtensionality{} -> []

plannedCalculationRequests
    :: PreparedCalculation
    -> [Declaration.CheckedPlannedVampireRequest]
plannedCalculationRequests
        (PreparedCheckedCalculation
            _operandType _identities _guard _first links _result) =
    concatMap
        (plannedDischargeRequests . preparedCalculationLinkDischarge)
        (toList links)

plannedSinceEvidenceRequests
    :: PreparedSinceEvidence
    -> [Declaration.CheckedPlannedVampireRequest]
plannedSinceEvidenceRequests = \case
    PreparedSinceExisting{} -> []
    PreparedSinceDischarged discharge _local ->
        plannedDischargeRequests discharge

executePreparedProof
    :: PreparedProof
    -> Declaration.CandidateProof ()
executePreparedProof = \case
    PreparedImplicitAuto discharge ->
        executeDischarge discharge
    PreparedQed discharge ->
        executeDischarge discharge
    PreparedOmitted _location _goal ->
        Declaration.recordOmittedUse
    PreparedFix _identities continuation ->
        executePreparedProof continuation
    PreparedAssume _antecedent continuation ->
        executePreparedProof continuation
    PreparedTake _identities _witness discharge continuation -> do
        executeDischarge discharge
        executePreparedProof continuation
    PreparedSetInduction
            (PreparedCheckedSetInduction
                _focus _property _antecedents _target
                _hypothesis _result child) ->
        executePreparedProof child
    PreparedHave _claim discharge continuation -> do
        executeDischarge discharge
        executePreparedProof continuation
    PreparedSuffices goal reduction implication discharge continuation -> do
        executeDischarge discharge
        executePreparedProof continuation
        unless
            (implyScopedCore reduction goal == Just implication)
            (impossible "a prepared suffices implication diverged")
    PreparedCalculate calculation continuation -> do
        executePreparedCalculation calculation
        executePreparedProof continuation
    PreparedSince sinceProposition evidence _claim discharge continuation -> do
        executeSinceEvidence sinceProposition evidence
        executeDischarge discharge
        executePreparedProof continuation
    PreparedSubclaim _claim subproof continuation -> do
        executePreparedProof subproof
        executePreparedProof continuation
    PreparedDefine _identity _body _definition continuation ->
        executePreparedProof continuation
    PreparedDefineRelational
            _identity _body functionality _definitions continuation -> do
        executeDischarge functionality
        executePreparedProof continuation
    PreparedDefineFunction _identity _graph _definition continuation ->
        executePreparedProof continuation
    PreparedByCase
            (PreparedCaseAnalysis _goal cases _exhaustive discharge) -> do
        traverse_ (executePreparedProof . preparedCaseProof) cases
        executeDischarge discharge
    PreparedByContradiction _goal _negation _falsum child ->
        executePreparedProof child
    PreparedContradiction _goal _falsum discharge ->
        executeDischarge discharge

executeDischarge
    :: PreparedDischarge
    -> Declaration.CandidateProof ()
executeDischarge
        (PreparedVampireDischarge
            location _justification _goal obligation) =
    Declaration.locateProofObligation location
        (Declaration.acceptPreparedVampireObligation obligation)
executeDischarge PreparedSetExtensionality{} =
    pure ()

executePreparedCalculation
    :: PreparedCalculation
    -> Declaration.CandidateProof ()
executePreparedCalculation
        (PreparedCheckedCalculation
            _operandType _identities _guard _first links _result) =
    traverse_
        (executeDischarge . preparedCalculationLinkDischarge)
        links

executeSinceEvidence
    :: ScopedCheckedCore ObjectId
    -> PreparedSinceEvidence
    -> Declaration.CandidateProof ()
executeSinceEvidence proposition = \case
    PreparedSinceExisting local ->
        unless (preparedLocalProposition local == proposition)
            (impossible "a structural since premise diverged")
    PreparedSinceDischarged discharge local -> do
        executeDischarge discharge
        unless
            ( preparedDischargeGoal discharge == proposition
                && preparedLocalProposition local == proposition
            )
            (impossible "a discharged since premise diverged")

preparedLocalProposition
    :: PreparedLocal
    -> ScopedCheckedCore ObjectId
preparedLocalProposition
        (PreparedLocal _ordinal _origin _support proposition) =
    proposition

encodePreparedProof :: PreparedProof -> ByteString
encodePreparedProof =
    encodeCache . putPreparedProof

putPreparedProof :: PreparedProof -> CachePut
putPreparedProof = \case
    PreparedImplicitAuto discharge -> do
        putCacheTag 0x00
        putPreparedDischarge discharge
    PreparedQed discharge -> do
        putCacheTag 0x01
        putPreparedDischarge discharge
    PreparedOmitted _location goal -> do
        putCacheTag 0x06
        putScopedProposition goal
    PreparedFix identities continuation -> do
        putCacheTag 0x02
        putCacheList
            (putCacheNatural . Exact.exactLocalIdValue)
            identities
        putPreparedProof continuation
    PreparedAssume antecedent continuation -> do
        putCacheTag 0x03
        putScopedProposition antecedent
        putPreparedProof continuation
    PreparedTake identities witness discharge continuation -> do
        putCacheTag 0x08
        putCacheList
            (putCacheNatural . Exact.exactLocalIdValue)
            identities
        putScopedProposition witness
        putPreparedDischarge discharge
        putPreparedProof continuation
    PreparedSetInduction
            (PreparedCheckedSetInduction
                focus property antecedents target hypothesis result child) -> do
        putCacheTag 0x07
        putPreparedSetInductionFocus focus
        putScopedProposition property
        putCacheList putScopedProposition antecedents
        putScopedProposition target
        putScopedProposition hypothesis
        putScopedProposition result
        putPreparedProof child
    PreparedHave claim discharge continuation -> do
        putCacheTag 0x04
        putScopedProposition claim
        putPreparedDischarge discharge
        putPreparedProof continuation
    PreparedSuffices goal reduction implication discharge continuation -> do
        putCacheTag 0x0c
        putScopedProposition goal
        putScopedProposition reduction
        putScopedProposition implication
        putPreparedDischarge discharge
        putPreparedProof continuation
    PreparedCalculate calculation continuation -> do
        putCacheTag 0x0d
        putPreparedCalculation calculation
        putPreparedProof continuation
    PreparedSince sinceProposition evidence claim discharge continuation -> do
        putCacheTag 0x0e
        putScopedProposition sinceProposition
        putPreparedSinceEvidence evidence
        putScopedProposition claim
        putPreparedDischarge discharge
        putPreparedProof continuation
    PreparedSubclaim claim subproof continuation -> do
        putCacheTag 0x05
        putScopedProposition claim
        putPreparedProof subproof
        putPreparedProof continuation
    PreparedDefine identity body definitions continuation -> do
        putCacheTag 0x09
        putCacheNatural (Exact.exactLocalIdValue identity)
        putScopedTerm body
        putCacheList putScopedProposition (toList definitions)
        putPreparedProof continuation
    PreparedDefineRelational
            identity body functionality definitions continuation -> do
        putCacheTag 0x11
        putCacheNatural (Exact.exactLocalIdValue identity)
        putScopedTerm body
        putPreparedDischarge functionality
        putCacheList putScopedProposition (toList definitions)
        putPreparedProof continuation
    PreparedByCase caseAnalysis -> do
        putCacheTag 0x0f
        putPreparedCaseAnalysis caseAnalysis
    PreparedByContradiction goal negation falsum child -> do
        putCacheTag 0x10
        putScopedProposition goal
        putScopedProposition negation
        putScopedProposition falsum
        putPreparedProof child
    PreparedContradiction goal falsum discharge -> do
        putCacheTag 0x0a
        putScopedProposition goal
        putScopedProposition falsum
        putPreparedDischarge discharge
    PreparedDefineFunction identity graph definition continuation -> do
        putCacheTag 0x0b
        putCacheNatural (Exact.exactLocalIdValue identity)
        putScopedTerm graph
        putScopedProposition definition
        putPreparedProof continuation

putPreparedSetInductionFocus
    :: PreparedSetInductionFocus
    -> CachePut
putPreparedSetInductionFocus = \case
    PreparedInitialSetInductionFocus identity index -> do
        putCacheTag 0x00
        putCacheNatural (Exact.exactLocalIdValue identity)
        putCacheNatural index
    PreparedLeadingSetInductionFocus identity -> do
        putCacheTag 0x01
        putCacheNatural (Exact.exactLocalIdValue identity)

putPreparedDischarge :: PreparedDischarge -> CachePut
putPreparedDischarge
        (PreparedVampireDischarge
            _location justification goal _obligation) = do
    putPreparedDischargeSyntax justification goal
putPreparedDischarge
        (PreparedSetExtensionality _location goal) = do
    putCacheTag 0x03
    putScopedProposition goal

putPreparedDischargeSyntax
    :: PreparedJustification
    -> ScopedCheckedCore ObjectId
    -> CachePut
putPreparedDischargeSyntax justification goal = do
    putPreparedJustification justification
    putScopedProposition goal

putPreparedCalculation :: PreparedCalculation -> CachePut
putPreparedCalculation
        (PreparedCheckedCalculation
            operandType identities calculationGuard first links result) = do
    putCoreTypeCache operandType
    putCacheList
        (putCacheNatural . Exact.exactLocalIdValue)
        identities
    putCacheMaybe putScopedProposition calculationGuard
    putCacheList putScopedTerm
        (first : (preparedCalculationLinkDestination <$> toList links))
    putCacheList putPreparedDischarge
        (preparedCalculationLinkDischarge <$> toList links)
    putScopedProposition result

putPreparedSinceEvidence :: PreparedSinceEvidence -> CachePut
putPreparedSinceEvidence = \case
    PreparedSinceExisting local -> do
        putCacheTag 0x00
        putPreparedLocalEvidence local
    PreparedSinceDischarged discharge local -> do
        putCacheTag 0x01
        putPreparedDischarge discharge
        putPreparedLocalEvidence local

putPreparedCaseAnalysis :: PreparedCaseAnalysis -> CachePut
putPreparedCaseAnalysis
        (PreparedCaseAnalysis goal cases exhaustive discharge) = do
    putScopedProposition goal
    putCacheList putPreparedCase (toList cases)
    putScopedProposition exhaustive
    putPreparedDischarge discharge

putPreparedCase :: PreparedCase -> CachePut
putPreparedCase (PreparedCase assumption proof) = do
    putScopedProposition assumption
    putPreparedProof proof

putPreparedLocalEvidence :: PreparedLocal -> CachePut
putPreparedLocalEvidence
        (PreparedLocal ordinal _origin support proposition) = do
    putCacheNatural (Backend.localPremiseOrdinalValue ordinal)
    putCacheList
        (\(identity, coreType) -> do
            putCacheNatural (Exact.exactLocalIdValue identity)
            putCoreTypeCache coreType)
        (Vector.toList support)
    putScopedProposition proposition

implicitAutoProofSyntaxId
    :: ScopedCheckedCore ObjectId
    -> ProofSyntaxId
implicitAutoProofSyntaxId goal =
    proofSyntaxId
        (encodeCache do
            putCacheTag 0x00
            putPreparedDischargeSyntax PreparedAuto goal)

putPreparedJustification :: PreparedJustification -> CachePut
putPreparedJustification = \case
    PreparedAuto ->
        putCacheTag 0x00
    PreparedReferences fingerprints -> do
        putCacheTag 0x01
        putCacheList
            putSemanticFactOccurrenceFingerprintCache
            (toList fingerprints)
    PreparedLocalOnly ->
        putCacheTag 0x02

putScopedProposition
    :: ScopedCheckedCore ObjectId
    -> CachePut
putScopedProposition proposition = do
    putCacheList putCoreTypeCache
        (scopedCoreContext proposition)
    putCanonicalTermCache putObjectIdCache
        (scopedCoreTerm proposition)

putScopedTerm
    :: ScopedCheckedCore ObjectId
    -> CachePut
putScopedTerm term = do
    putCacheList putCoreTypeCache
        (scopedCoreContext term)
    putCoreTypeCache (scopedCoreType term)
    putCanonicalTermCache putObjectIdCache
        (scopedCoreTerm term)

proofLocation :: Location -> Raw.Proof -> Location
proofLocation fallback = \case
    Raw.Omitted location -> location
    Raw.Qed maybeLocation _justification ->
        fromMaybe fallback maybeLocation
    Raw.Contradiction location _justification -> location
    Raw.ByCase location _cases -> location
    Raw.ByContradiction location _proof -> location
    Raw.BySetInduction location _term _proof -> location
    Raw.ByOrdInduction location _proof -> location
    Raw.Assume location _statement _proof -> location
    Raw.FixSymbolic location _variables _bound _proof -> location
    Raw.FixSuchThat location _variables _statement _proof -> location
    Raw.Calc location _quantifier _calculation _proof -> location
    Raw.TakeVar location _variables _bound _statement _justification _proof ->
        location
    Raw.TakeNoun location _noun _justification _proof -> location
    Raw.Have location _since _statement _justification _proof -> location
    Raw.Suffices location _statement _justification _proof -> location
    Raw.Subclaim location _statement _subproof _proof -> location
    Raw.Define location _variable _expression _proof -> location
    Raw.DefineFunction location _function _argument _value _bound _domain _proof ->
        location
    Raw.DefineFunctionLocal
            location _function _argument _value _bound _target _rules _proof ->
        location

throwProof :: ExactProofError -> Prepare value
throwProof =
    State.lift . Except.throwError

liftDriver
    :: Declaration.LoweringDriver value
    -> Prepare value
liftDriver =
    State.lift . Except.lift

stableUnique :: Ord value => [value] -> [value]
stableUnique =
    reverse . snd
        . foldl'
            (\(seen, reversed) value ->
                if value `Set.member` seen
                    then (seen, reversed)
                    else
                        ( Set.insert value seen
                        , value : reversed
                        ))
            (Set.empty, [])