path: root/source/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 Checking.Exact.Proof
    ( PreparedExactProof
    , preparedExactProofSyntaxId
    , preparedExactProofFirstOmission
    , prepareExactProof
    , CheckedExactProofAuthorization
    , lowerPreparedExactProof
    , authorizeCheckedExactProof
    , PreparedFinalPreludeFoundationClaim
    , prepareFinalPreludeFoundationClaim
    , CheckedFinalPreludeFoundationAuthorization
    , lowerPreparedFinalPreludeFoundationClaim
    , authorizeCheckedFinalPreludeFoundationClaim
    , ExactProofError(..)
    , exactProofErrorLocation
    , renderExactProofError
    ) where

import Base
import Checking.Authority qualified as Authority
import Checking.Backend.Problem qualified as Backend
import Checking.Core
import Checking.Declaration qualified as Declaration
import Checking.Exact qualified as Exact
import Checking.Foundation
import Checking.Identity
import Checking.Kernel.Derivation (foundationFactDerivation)
import Checking.Semantic
import Felix.Cache.Codec
import Report.Location
import 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.Set qualified as Set
import Data.Text qualified as Text
import Data.Vector (Vector)
import Numeric.Natural (Natural)


data ExactProofError
    = ExactProofUnsupportedClaim !Location
    | ExactProofUnsupportedStep !Location
    | ExactProofSetInductionVariableRequired !Location
    | ExactProofSetInductionVariableNotActive
        !Location !Raw.VarSymbol
    | ExactProofSetInductionNotOutermost !Location
    | ExactProofSetInductionGoalMismatch !Location
    | ExactProofSetExtensionalityGoalMismatch !Location
    | ExactProofSetExtensionalityDirectionsUnavailable !Location
    | ExactProofExpectedUniversalGoal !Location
    | ExactProofExpectedImplicationGoal !Location
    | ExactProofGoalStatementMismatch !Location
    | ExactProofContradictionGoalMismatch !Location
    | 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
    ExactProofSetInductionNotOutermost location -> location
    ExactProofSetInductionGoalMismatch location -> location
    ExactProofSetExtensionalityGoalMismatch location -> location
    ExactProofSetExtensionalityDirectionsUnavailable location -> location
    ExactProofExpectedUniversalGoal location -> location
    ExactProofExpectedImplicationGoal location -> location
    ExactProofGoalStatementMismatch location -> location
    ExactProofContradictionGoalMismatch location -> 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 active exact binder"
    ExactProofSetInductionNotOutermost location ->
        at location <> "set induction must currently be outermost"
    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"
    ExactProofContradictionGoalMismatch location ->
        at location <> "contradiction requires falsum as the current goal"
    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
    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 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
        !(ScopedCheckedCore ObjectId)
        !PreparedDischarge
    | PreparedHave
        !(ScopedCheckedCore ObjectId)
        !PreparedDischarge
        !PreparedProof
    | PreparedSubclaim
        !(ScopedCheckedCore ObjectId)
        !PreparedProof
        !PreparedProof
    | PreparedDefine
        !Exact.ExactLocalId
        !(ScopedCheckedCore ObjectId)
        !(ScopedCheckedCore ObjectId)
        !PreparedProof
    | PreparedDefineFunction
        !Exact.ExactLocalId
        !(ScopedCheckedCore ObjectId)
        !(ScopedCheckedCore ObjectId)
        !PreparedProof
    | PreparedContradiction !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)
                bodyProof <-
                    case explicitProof of
                        Nothing ->
                            PreparedImplicitAuto
                                <$> prepareDischargeWith
                                    DirectDischarge
                                    []
                                    Nothing
                                    location
                                    context
                                    locals
                                    bodyGoal
                                    Raw.JustificationEmpty
                        Just sourceProof ->
                            prepareProof
                                location
                                context
                                locals
                                (Just antecedents)
                                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)

prepareProof
    :: Location
    -> Exact.ExactBinderContext
    -> [PreparedLocal]
    -- Only the initial proof carries set-induction antecedents.
    -> Maybe [ScopedCheckedCore ObjectId]
    -> ScopedCheckedCore ObjectId
    -> Raw.Proof
    -> Prepare PreparedProof
prepareProof fallback context locals inductionAntecedents 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
                        Nothing
                        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])
                Nothing
                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 ->
        case (inductionAntecedents, continuation) of
            (Nothing, _proof) ->
                throwProof
                    (ExactProofSetInductionNotOutermost location)
            (Just antecedents, Raw.Qed maybeLocation justification) -> do
                sourceVariable <-
                    case variable of
                        Just (Raw.TermExpr (Raw.ExprVar candidate)) ->
                            pure candidate
                        _ ->
                            throwProof
                                (ExactProofSetInductionVariableRequired
                                    location)
                selected <-
                    maybe
                        (throwProof
                            (ExactProofSetInductionVariableNotActive
                                location
                                sourceVariable))
                        pure
                        (Exact.exactBinderContextIndex
                            sourceVariable context)
                let property =
                        foldr implyChecked goal antecedents
                hypothesis <-
                    maybe
                        (throwProof
                            (ExactProofSetInductionGoalMismatch
                                location))
                        pure
                        (scopedSetInductionHypothesis selected property)
                local <- allocateLocal ExactAssumption context hypothesis
                PreparedSetInduction hypothesis
                    <$> prepareDischarge
                        (fromMaybe location maybeLocation)
                        context
                        (locals <> [local])
                        goal
                        justification
            (Just _antecedents, _proof) ->
                throwProof (ExactProofUnsupportedStep location)
    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 since statement justification continuation -> do
        when (isJust since)
            (throwProof (ExactProofUnsupportedStep location))
        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])
                Nothing
                goal
                continuation
    Raw.Subclaim location statement subproof continuation -> do
        claim <-
            Exact.preparedExactPropositionCore
                <$> prepareStatement context statement
        preparedSubproof <-
            prepareProof
                location
                context
                locals
                Nothing
                claim
                subproof
        local <- allocateLocal ExactDerivedClaim context claim
        PreparedSubclaim claim preparedSubproof
            <$> prepareProof
                fallback
                context
                (locals <> [local])
                Nothing
                goal
                continuation
    Raw.Define _location variable expression continuation -> do
        body <-
            Exact.preparedExactSetExpressionCore
                <$> ( liftDriver
                        (Exact.prepareExactSetExpression
                            context expression)
                        >>= either
                            (throwProof . ExactProofElaborationFailed)
                            pure
                    )
        identity <- allocateLocalIdentity
        context' <-
            either
                (throwProof . ExactProofElaborationFailed)
                pure
                (Exact.extendExactBinderContext
                    ((identity, variable) :| [])
                    context)
        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])
                Nothing
                (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])
                Nothing
                (weakenCheckedScopedCore TySet goal)
                continuation
    Raw.Contradiction location justification -> do
        unless
            ( scopedCoreType goal == TyProp
                && scopedCoreTerm goal == CFalsum
            )
            (throwProof
                (ExactProofContradictionGoalMismatch location))
        PreparedContradiction
            <$> prepareDischargeWith
                IndirectContradictionDischarge
                []
                Nothing
                location
                context
                locals
                goal
                justification
    proof ->
        throwProof
            (ExactProofUnsupportedStep
                (proofLocation fallback proof))
  where
    implyChecked antecedent conclusion =
        fromMaybe
            (impossible "an exact claim antecedent changed context")
            (implyScopedCore antecedent conclusion)

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])
            Nothing
            conclusion
            continuation
    pure (PreparedFix identities (PreparedAssume constraint prepared))

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])
            Nothing
            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)

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

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

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 _hypothesis _discharge -> Nothing
    PreparedHave _claim _discharge continuation ->
        preparedProofFirstOmission continuation
    PreparedSubclaim _claim subproof continuation ->
        preparedProofFirstOmission subproof
            <|> preparedProofFirstOmission continuation
    PreparedDefine _identity _body _definition continuation ->
        preparedProofFirstOmission continuation
    PreparedDefineFunction _identity _graph _definition continuation ->
        preparedProofFirstOmission continuation
    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 _hypothesis discharge ->
        plannedDischargeRequests discharge
    PreparedHave _claim discharge continuation ->
        plannedDischargeRequests discharge <> plannedProofRequests continuation
    PreparedSubclaim _claim subproof continuation ->
        plannedProofRequests subproof <> plannedProofRequests continuation
    PreparedDefine _identity _body _definition continuation ->
        plannedProofRequests continuation
    PreparedDefineFunction _identity _graph _definition continuation ->
        plannedProofRequests continuation
    PreparedContradiction discharge ->
        plannedDischargeRequests discharge

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

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 _hypothesis discharge ->
        executeDischarge discharge
    PreparedHave _claim discharge continuation -> do
        executeDischarge discharge
        executePreparedProof continuation
    PreparedSubclaim _claim subproof continuation -> do
        executePreparedProof subproof
        executePreparedProof continuation
    PreparedDefine _identity _body _definition continuation ->
        executePreparedProof continuation
    PreparedDefineFunction _identity _graph _definition continuation ->
        executePreparedProof continuation
    PreparedContradiction discharge ->
        executeDischarge discharge

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

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 hypothesis discharge -> do
        putCacheTag 0x07
        putScopedProposition hypothesis
        putPreparedDischarge discharge
    PreparedHave claim discharge continuation -> do
        putCacheTag 0x04
        putScopedProposition claim
        putPreparedDischarge discharge
        putPreparedProof continuation
    PreparedSubclaim claim subproof continuation -> do
        putCacheTag 0x05
        putScopedProposition claim
        putPreparedProof subproof
        putPreparedProof continuation
    PreparedDefine identity body definition continuation -> do
        putCacheTag 0x09
        putCacheNatural (Exact.exactLocalIdValue identity)
        putScopedTerm body
        putScopedProposition definition
        putPreparedProof continuation
    PreparedContradiction discharge -> do
        putCacheTag 0x0a
        putPreparedDischarge discharge
    PreparedDefineFunction identity graph definition continuation -> do
        putCacheTag 0x0b
        putCacheNatural (Exact.exactLocalIdValue identity)
        putScopedTerm graph
        putScopedProposition definition
        putPreparedProof continuation

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

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, [])