path: root/source/Felix/Checking/Backend/Problem.hs

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

-- | Complete-problem FOF/TH0 classification and construction.
module Felix.Checking.Backend.Problem
    ( SupportedProposition
    , supportedProposition
    , projectSupportedProposition
    , supportedPropositionSupport
    , supportedPropositionTerm
    , weakenClosedSupportedProposition
    , SupportedPropositionError(..)
    , SupportedPropositionProjectionError(..)
    , CheckedFofProjection
    , checkedFofProjectionProposition
    , FofCapability(..)
    , BackendFofExclusion(..)
    , BackendClassificationError(..)
    , classifySupportedProposition
    , TypedBackendFact
    , typedBackendFact
    , typedBackendFactReference
    , typedBackendFactProposition
    , typedBackendFactCapability
    , LocalPremiseOrdinal
    , localPremiseOrdinal
    , localPremiseOrdinalValue
    , TypedLocalPremise
    , typedLocalPremise
    , typedLocalPremiseOrdinal
    , typedLocalPremiseOrigin
    , typedLocalPremiseProposition
    , typedLocalPremiseCapability
    , TypedFoundationAuxiliaryInput
    , typedFoundationAuxiliaryInput
    , TypedProblemAuxiliary
    , typedProblemAuxiliaryOrdinal
    , typedProblemAuxiliaryTag
    , typedProblemAuxiliaryProposition
    , typedProblemAuxiliaryCapability
    , LocalPremisePolicy(..)
    , HigherOrderJustificationPolicy(..)
    , selectTypedLocalPremises
    , TypedProblemRoute(..)
    , TypedProblem
    , planTypedProblem
    , typedProblemRoute
    , typedProblemClaim
    , typedProblemGlobalPremises
    , typedProblemLocalPremises
    , typedProblemAuxiliaries
    , typedProblemGlobalTypes
    , typedProblemLocalTypes
    , TypedProblemError(..)
    ) where

import Base
import Felix.Checking.Core
import Felix.Checking.Foundation

import Control.Monad (foldM, unless)
import Data.Bifunctor (first)
import Data.List qualified as List
import Data.Map.Strict qualified as Map
import Data.Set qualified as Set
import Data.Vector (Vector)
import Data.Vector qualified as Vector
import Numeric.Natural (Natural)


-- | A proposition under its exact nearest-first ambient-local support.
data SupportedProposition local global =
    SupportedProposition
        !(Vector (local, CoreType))
        !(ScopedCheckedCore global)
    deriving stock (Eq)

data SupportedPropositionError local
    = SupportedPropositionIsNotProposition !CoreType
    | SupportedPropositionContextMismatch
        ![CoreType]
        ![CoreType]
    | DuplicateSupportedLocal !local
    | UnusedSupportedLocal !local
    deriving stock (Show, Eq)

data SupportedPropositionProjectionError local
    = SupportedProjectionContextMismatch
        ![CoreType]
        ![CoreType]
    | SupportedProjectionDuplicateLocal !local
    | SupportedProjectionIndexMissing !Natural
    | SupportedProjectionCoreCheckFailed !CoreCheckError
    | SupportedProjectionValidationFailed
        !(SupportedPropositionError local)
    deriving stock (Show, Eq)

supportedProposition
    :: Ord local
    => Vector (local, CoreType)
    -> ScopedCheckedCore global
    -> Either
        (SupportedPropositionError local)
        (SupportedProposition local global)
supportedProposition support statement = do
    unless
        (scopedCoreType statement == TyProp)
        (Left
            (SupportedPropositionIsNotProposition
                (scopedCoreType statement)))
    let expectedContext =
            snd <$> Vector.toList support
        actualContext =
            scopedCoreContext statement
    unless
        (actualContext == expectedContext)
        (Left
            (SupportedPropositionContextMismatch
                expectedContext
                actualContext))
    void
        (foldM
            (\seen (local, _coreType) ->
                if local `Set.member` seen
                    then
                        Left
                            (DuplicateSupportedLocal local)
                    else
                        Right (Set.insert local seen))
            Set.empty
            support)
    case
        List.find
            (\(ordinal, _entry) ->
                fromIntegral ordinal
                    `Set.notMember`
                        ambientIndices
                            (scopedCoreTerm statement))
            (Vector.toList
                (Vector.indexed support)) of
        Just (_ordinal, (local, _coreType)) ->
            Left (UnusedSupportedLocal local)
        Nothing ->
            pure ()
    pure
        (SupportedProposition
            support
            statement)

-- | Retain exactly the ambient locals used by a checked proposition and
-- remap its indices to that dense nearest-first support.
projectSupportedProposition
    :: Ord local
    => (global -> Maybe CoreType)
    -> Vector (local, CoreType)
    -> ScopedCheckedCore global
    -> Either
        (SupportedPropositionProjectionError local)
        (SupportedProposition local global)
projectSupportedProposition globalType available statement = do
    let expectedContext = snd <$> Vector.toList available
        actualContext = scopedCoreContext statement
    unless (expectedContext == actualContext)
        (Left
            (SupportedProjectionContextMismatch
                expectedContext
                actualContext))
    void
        (foldM
            (\seen (local, _coreType) ->
                if local `Set.member` seen
                    then Left (SupportedProjectionDuplicateLocal local)
                    else Right (Set.insert local seen))
            Set.empty
            available)
    let used =
            Set.toAscList
                (ambientIndices
                    (scopedCoreTerm statement))
    selected <- traverse (lookupNatural available) used
    let remapping =
            Map.fromAscList
                (zip used [0 ..])
    remapped <- remapAmbientIndices remapping 0
        (scopedCoreTerm statement)
    checked <-
        first SupportedProjectionCoreCheckFailed
            (checkScopedCanonicalCore
                globalType
                (snd <$> selected)
                remapped)
    first SupportedProjectionValidationFailed
        (supportedProposition
            (Vector.fromList selected)
            checked)
  where
    lookupNatural values index =
        maybe
            (Left (SupportedProjectionIndexMissing index))
            Right
            (go index (Vector.toList values))

    go _index [] =
        Nothing
    go 0 (value : _rest) =
        Just value
    go index (_value : rest) =
        go (index - 1) rest

    remapAmbientIndices remapping depth = \case
        CBound index
            | index < depth ->
                Right (CBound index)
            | otherwise ->
                maybe
                    (Left
                        (SupportedProjectionIndexMissing
                            (index - depth)))
                    (Right . CBound . (+ depth))
                    (Map.lookup (index - depth) remapping)
        CGlobal global ->
            Right (CGlobal global)
        CIntrinsic intrinsic ->
            Right (CIntrinsic intrinsic)
        COpaqueInteger integer ->
            Right (COpaqueInteger integer)
        CApp function argument ->
            CApp
                <$> remapAmbientIndices remapping depth function
                <*> remapAmbientIndices remapping depth argument
        CLam binderType body ->
            CLam binderType
                <$> remapAmbientIndices remapping (depth + 1) body
        CFalsum ->
            Right CFalsum
        CImp premise conclusion ->
            CImp
                <$> remapAmbientIndices remapping depth premise
                <*> remapAmbientIndices remapping depth conclusion
        CEq operandType left right ->
            CEq operandType
                <$> remapAmbientIndices remapping depth left
                <*> remapAmbientIndices remapping depth right
        CForall binderType body ->
            CForall binderType
                <$> remapAmbientIndices remapping (depth + 1) body

ambientIndices
    :: CanonicalTerm global
    -> Set Natural
ambientIndices =
    go 0
  where
    go depth = \case
        CBound index
            | index < depth ->
                mempty
            | otherwise ->
                Set.singleton (index - depth)
        CGlobal{} ->
            mempty
        CIntrinsic{} ->
            mempty
        COpaqueInteger{} ->
            mempty
        CApp function argument ->
            go depth function <> go depth argument
        CLam _binderType body ->
            go (depth + 1) body
        CFalsum ->
            mempty
        CImp premise conclusion ->
            go depth premise <> go depth conclusion
        CEq _operandType left right ->
            go depth left <> go depth right
        CForall _binderType body ->
            go (depth + 1) body

supportedPropositionSupport
    :: SupportedProposition local global
    -> Vector (local, CoreType)
supportedPropositionSupport
        (SupportedProposition support _statement) =
    support

supportedPropositionTerm
    :: SupportedProposition local global
    -> CanonicalTerm global
supportedPropositionTerm
        (SupportedProposition _support statement) =
    scopedCoreTerm statement

weakenClosedSupportedProposition
    :: SupportedProposition Void global
    -> SupportedProposition local global
weakenClosedSupportedProposition
        (SupportedProposition support statement) =
    SupportedProposition
        (fmap
            (\(local, coreType) ->
                (absurd local, coreType))
            support)
        statement


newtype CheckedFofProjection local global =
    CheckedFofProjection
        (SupportedProposition local global)
    deriving stock (Eq)

checkedFofProjectionProposition
    :: CheckedFofProjection local global
    -> SupportedProposition local global
checkedFofProjectionProposition
        (CheckedFofProjection proposition) =
    proposition

data FofCapability projection
    = FofProjectable !projection
    | RequiresTh0 !(NonEmpty BackendFofExclusion)
    deriving stock (Eq)

data BackendFofExclusion
    = StructuralFofExclusion !FofExclusion
    | HigherOrderGlobalType !CoreType
    | HigherOrderAmbientLocal !CoreType
    deriving stock (Show, Eq, Ord)

data BackendClassificationError global
    = UnknownBackendGlobal !global
    | BackendFofProjectionInvariantFailed
    deriving stock (Show, Eq)

classifySupportedProposition
    :: Ord global
    => (global -> Maybe CoreType)
    -> SupportedProposition local global
    -> Either
        (BackendClassificationError global)
        (FofCapability
            (CheckedFofProjection local global))
classifySupportedProposition globalType proposition = do
    globalExclusions <-
        foldM
            collectGlobal
            Set.empty
            (Set.toAscList
                (canonicalGlobals
                    (supportedPropositionTerm proposition)))
    let structuralExclusions =
            case classifyScopedStructure proposition of
                FoundationFofProjectable ->
                    Set.empty
                FoundationRequiresTh0 structural ->
                    Set.fromList
                        (StructuralFofExclusion
                            <$> toList structural)
        localExclusions =
            Set.fromList
                [ HigherOrderAmbientLocal coreType
                | (_local, coreType) <-
                    Vector.toList
                        (supportedPropositionSupport
                            proposition)
                , coreType /= TySet
                ]
        exclusions =
            structuralExclusions
                <> globalExclusions
                <> localExclusions
    case Set.toAscList exclusions of
        [] ->
            if isFirstOrderProposition
                    globalType
                    proposition
                then
                    Right
                        (FofProjectable
                            (CheckedFofProjection
                                proposition))
                else
                    Left BackendFofProjectionInvariantFailed
        firstExclusion : remainingExclusions ->
            Right
                (RequiresTh0
                    (firstExclusion
                        :| remainingExclusions))
  where
    collectGlobal exclusions global =
        case globalType global of
            Nothing ->
                Left (UnknownBackendGlobal global)
            Just coreType ->
                Right
                    (if isFirstOrderGlobalType coreType
                        then exclusions
                        else
                            Set.insert
                                (HigherOrderGlobalType
                                    coreType)
                                exclusions)

classifyScopedStructure
    :: SupportedProposition local global
    -> FoundationBackendClass
classifyScopedStructure =
    classifyCanonicalFofStructure
        . supportedPropositionTerm

isFirstOrderGlobalType :: CoreType -> Bool
isFirstOrderGlobalType =
    go
  where
    go = \case
        TySet ->
            True
        TyProp ->
            True
        TyArrow TySet result ->
            go result
        TyArrow _argument _result ->
            False

-- The structural and type exclusions make this projection total. This final
-- walk catches an accidentally unsaturated first-order head.
isFirstOrderProposition
    :: (global -> Maybe CoreType)
    -> SupportedProposition local global
    -> Bool
isFirstOrderProposition globalType proposition =
    isFormula initialContext
        (supportedPropositionTerm proposition)
  where
    initialContext =
        snd
            <$> Vector.toList
                (supportedPropositionSupport
                    proposition)

    isFormula context = \case
        CFalsum ->
            True
        CImp premise conclusion ->
            isFormula context premise
                && isFormula context conclusion
        CEq TySet left right ->
            isTerm context left
                && isTerm context right
        CEq TyProp left right ->
            isFormula context left
                && isFormula context right
        CForall TySet body ->
            isFormula (TySet : context) body
        application ->
            case applicationHead application of
                (CGlobal global, arguments) ->
                    maybe
                        False
                        (\coreType ->
                            applicationResult
                                coreType
                                arguments
                                == Just TyProp
                                && all
                                    (isTerm context)
                                    arguments)
                        (globalType global)
                (CIntrinsic intrinsic, arguments) ->
                    applicationResult
                        (coreIntrinsicType intrinsic)
                        arguments
                        == Just TyProp
                        && all
                            (isTerm context)
                            arguments
                _ ->
                    False

    isTerm context = \case
        CBound index ->
            contextAt index context
                == Just TySet
        CGlobal global ->
            globalType global == Just TySet
        CIntrinsic intrinsic ->
            coreIntrinsicType intrinsic == TySet
        COpaqueInteger{} ->
            True
        application ->
            case applicationHead application of
                (CGlobal global, arguments) ->
                    maybe
                        False
                        (\coreType ->
                            applicationResult
                                coreType
                                arguments
                                == Just TySet
                                && all
                                    (isTerm context)
                                    arguments)
                        (globalType global)
                (CIntrinsic intrinsic, arguments) ->
                    applicationResult
                        (coreIntrinsicType intrinsic)
                        arguments
                        == Just TySet
                        && all
                            (isTerm context)
                            arguments
                _ ->
                    False

applicationHead
    :: CanonicalTerm global
    -> (CanonicalTerm global, [CanonicalTerm global])
applicationHead =
    go []
  where
    go arguments = \case
        CApp function argument ->
            go (argument : arguments) function
        headTerm ->
            (headTerm, arguments)

applicationResult
    :: CoreType
    -> [CanonicalTerm global]
    -> Maybe CoreType
applicationResult =
    foldM
        (\coreType _argument ->
            case coreType of
                TyArrow TySet result ->
                    Just result
                _ ->
                    Nothing)

contextAt :: Natural -> [value] -> Maybe value
contextAt _index [] =
    Nothing
contextAt 0 (value : _remaining) =
    Just value
contextAt index (_value : remaining) =
    contextAt (index - 1) remaining

canonicalGlobals
    :: Ord global
    => CanonicalTerm global
    -> Set global
canonicalGlobals = \case
    CBound{} ->
        mempty
    CGlobal global ->
        Set.singleton global
    CIntrinsic{} ->
        mempty
    COpaqueInteger{} ->
        mempty
    CApp function argument ->
        canonicalGlobals function
            <> canonicalGlobals argument
    CLam _binderType body ->
        canonicalGlobals body
    CFalsum ->
        mempty
    CImp premise conclusion ->
        canonicalGlobals premise
            <> canonicalGlobals conclusion
    CEq _operandType left right ->
        canonicalGlobals left
            <> canonicalGlobals right
    CForall _binderType body ->
        canonicalGlobals body


data TypedBackendFact ref global =
    TypedBackendFact
        !ref
        !(SupportedProposition Void global)
        !(FofCapability
            (CheckedFofProjection Void global))
    deriving stock (Eq)

typedBackendFact
    :: ref
    -> SupportedProposition Void global
    -> FofCapability
        (CheckedFofProjection Void global)
    -> TypedBackendFact ref global
typedBackendFact =
    TypedBackendFact

typedBackendFactReference
    :: TypedBackendFact ref global
    -> ref
typedBackendFactReference
        (TypedBackendFact
            reference
            _proposition
            _capability) =
    reference

typedBackendFactProposition
    :: TypedBackendFact ref global
    -> SupportedProposition Void global
typedBackendFactProposition
        (TypedBackendFact
            _reference
            proposition
            _capability) =
    proposition

typedBackendFactCapability
    :: TypedBackendFact ref global
    -> FofCapability
        (CheckedFofProjection Void global)
typedBackendFactCapability
        (TypedBackendFact
            _reference
            _proposition
            capability) =
    capability


newtype LocalPremiseOrdinal =
    LocalPremiseOrdinal Natural
    deriving stock (Show, Eq, Ord)

localPremiseOrdinal :: Natural -> LocalPremiseOrdinal
localPremiseOrdinal =
    LocalPremiseOrdinal

localPremiseOrdinalValue
    :: LocalPremiseOrdinal
    -> Natural
localPremiseOrdinalValue
        (LocalPremiseOrdinal ordinal) =
    ordinal

data TypedLocalPremise local origin global =
    TypedLocalPremise
        !LocalPremiseOrdinal
        !origin
        !(SupportedProposition local global)
        !(FofCapability
            (CheckedFofProjection local global))
    deriving stock (Eq)

typedLocalPremise
    :: Ord global
    => (global -> Maybe CoreType)
    -> LocalPremiseOrdinal
    -> origin
    -> SupportedProposition local global
    -> Either
        (BackendClassificationError global)
        (TypedLocalPremise local origin global)
typedLocalPremise globalType ordinal premiseOrigin proposition =
    TypedLocalPremise
        ordinal
        premiseOrigin
        proposition
        <$> classifySupportedProposition
            globalType
            proposition

typedLocalPremiseOrdinal
    :: TypedLocalPremise local origin global
    -> LocalPremiseOrdinal
typedLocalPremiseOrdinal
        (TypedLocalPremise
            ordinal
            _origin
            _proposition
            _capability) =
    ordinal

typedLocalPremiseOrigin
    :: TypedLocalPremise local origin global
    -> origin
typedLocalPremiseOrigin
        (TypedLocalPremise
            _ordinal
            premiseOrigin
            _proposition
            _capability) =
    premiseOrigin

typedLocalPremiseProposition
    :: TypedLocalPremise local origin global
    -> SupportedProposition local global
typedLocalPremiseProposition
        (TypedLocalPremise
            _ordinal
            _origin
            proposition
            _capability) =
    proposition

typedLocalPremiseCapability
    :: TypedLocalPremise local origin global
    -> FofCapability
        (CheckedFofProjection local global)
typedLocalPremiseCapability
        (TypedLocalPremise
            _ordinal
            _origin
            _proposition
            capability) =
    capability


data TypedFoundationAuxiliaryInput global =
    TypedFoundationAuxiliaryInput
        !FoundationAxiomTag
        !(SupportedProposition Void global)
        !(FofCapability
            (CheckedFofProjection Void global))

typedFoundationAuxiliaryInput
    :: CheckedFoundation
    -> FoundationAxiomTag
    -> TypedFoundationAuxiliaryInput global
typedFoundationAuxiliaryInput foundation tag =
    TypedFoundationAuxiliaryInput
        tag
        proposition
        capability
  where
    proposition =
        SupportedProposition
            Vector.empty
            (embedClosedCore
                []
                (mapFrozenGlobals
                    absurd
                    (foundationAxiomFrozen
                        foundation
                        tag)))
    capability =
        case foundationAxiomBackendClass
                foundation
                tag of
            FoundationFofProjectable ->
                FofProjectable
                    (CheckedFofProjection
                        proposition)
            FoundationRequiresTh0 exclusions ->
                RequiresTh0
                    (StructuralFofExclusion
                        <$> exclusions)

data TypedProblemAuxiliary global =
    TypedProblemAuxiliary
        !Natural
        !FoundationAxiomTag
        !(SupportedProposition Void global)
        !(FofCapability
            (CheckedFofProjection Void global))
    deriving stock (Eq)

typedProblemAuxiliaryOrdinal
    :: TypedProblemAuxiliary global
    -> Natural
typedProblemAuxiliaryOrdinal
        (TypedProblemAuxiliary
            ordinal
            _tag
            _proposition
            _capability) =
    ordinal

typedProblemAuxiliaryTag
    :: TypedProblemAuxiliary global
    -> FoundationAxiomTag
typedProblemAuxiliaryTag
        (TypedProblemAuxiliary
            _ordinal
            tag
            _proposition
            _capability) =
    tag

typedProblemAuxiliaryProposition
    :: TypedProblemAuxiliary global
    -> SupportedProposition Void global
typedProblemAuxiliaryProposition
        (TypedProblemAuxiliary
            _ordinal
            _tag
            proposition
            _capability) =
    proposition

typedProblemAuxiliaryCapability
    :: TypedProblemAuxiliary global
    -> FofCapability
        (CheckedFofProjection Void global)
typedProblemAuxiliaryCapability
        (TypedProblemAuxiliary
            _ordinal
            _tag
            _proposition
            capability) =
    capability


-- | Source justification policy for premise selection. Higher-order routing
-- is validated separately after the complete selected problem is known.
data LocalPremisePolicy
    = FirstOrderLocals
    | CompleteLocals
    deriving stock (Show, Eq)

-- | Whether selected higher-order components must be justified by one of the
-- two approved inline construction forms.  Premise selection has already
-- happened when this policy is applied.
data HigherOrderJustificationPolicy
    = ImplicitConstructionJustification
    | ExplicitHigherOrderJustification
    deriving stock (Show, Eq)

selectTypedLocalPremises
    :: LocalPremisePolicy
    -> [TypedLocalPremise local origin global]
    -> Vector (TypedLocalPremise local origin global)
selectTypedLocalPremises selection availableLocals =
    Vector.fromList
        (List.sortOn
            typedLocalPremiseOrdinal
            (case selection of
                FirstOrderLocals ->
                    List.filter
                        (isFofCapability
                            . typedLocalPremiseCapability)
                        availableLocals
                CompleteLocals ->
                    availableLocals))

data ImplicitHigherOrderConstruction
    = ImplicitSeparation
    | ImplicitFunctionalReplacement
    deriving stock (Show, Eq, Ord)

data TypedProblemRoute
    = RouteFof
    | RouteTh0
    deriving stock (Show, Eq)

data TypedProblem ref local origin global =
    TypedProblem
        !TypedProblemRoute
        !(SupportedProposition local global)
        !(Vector (TypedBackendFact ref global))
        !(Vector (TypedLocalPremise local origin global))
        !(Vector (TypedProblemAuxiliary global))
        !(Map global CoreType)
        !(Map local CoreType)
    deriving stock (Eq)

data TypedProblemError local global
    = TypedProblemClaimClassificationFailed
        !(BackendClassificationError global)
    | TypedProblemExplicitHigherOrderJustificationRequired
        !(NonEmpty BackendFofExclusion)
    | TypedProblemDuplicateLocalPremiseOrdinal
        !LocalPremiseOrdinal
    | TypedProblemLocalTypeMismatch
        !local
        !CoreType
        !CoreType
    deriving stock (Show, Eq)

planTypedProblem
    :: (Ord local, Ord global)
    => (global -> Maybe CoreType)
    -> Vector (TypedBackendFact ref global)
    -> SupportedProposition local global
    -> [TypedLocalPremise local origin global]
    -> [TypedFoundationAuxiliaryInput global]
    -> LocalPremisePolicy
    -> HigherOrderJustificationPolicy
    -> Either
        (TypedProblemError local global)
        (TypedProblem ref local origin global)
planTypedProblem
        globalType
        selectedFacts
        claim
        availableLocals
        auxiliaries
        localPolicy
        higherOrderPolicy = do
    validateLocalPremiseOrdinals
        availableLocals
    claimCapability <-
        first
            TypedProblemClaimClassificationFailed
            (classifySupportedProposition
                globalType
                claim)
    let selectedLocals =
            selectTypedLocalPremises
                localPolicy
                availableLocals
    let preparedAuxiliaries =
            zipWith
                prepareAuxiliary
                [0..]
                auxiliaries
    case higherOrderPolicy of
        ImplicitConstructionJustification ->
            validateImplicitHigherOrderAdmission
                claim
                claimCapability
                selectedFacts
                selectedLocals
                preparedAuxiliaries
        ExplicitHigherOrderJustification ->
            pure ()
    let selectedFofCapabilities =
            isFofCapability claimCapability
                : (isFofCapability
                    . typedBackendFactCapability
                    <$> Vector.toList selectedFacts)
                <> (isFofCapability
                    . typedLocalPremiseCapability
                    <$> Vector.toList selectedLocals)
                <> (isFofCapability
                    . typedProblemAuxiliaryCapability
                    <$> preparedAuxiliaries)
        route =
            if and selectedFofCapabilities
                then RouteFof
                else RouteTh0
    globalTypes <-
        collectProblemGlobals
            globalType
            claim
            selectedFacts
            selectedLocals
            preparedAuxiliaries
    localTypes <-
        collectProblemLocals
            claim
            selectedLocals
    pure
        (TypedProblem
            route
            claim
            selectedFacts
            selectedLocals
            (Vector.fromList preparedAuxiliaries)
            globalTypes
            localTypes)
  where
    prepareAuxiliary
            ordinal
            (TypedFoundationAuxiliaryInput
                tag
                proposition
                capability) =
        TypedProblemAuxiliary
            ordinal
            tag
            proposition
            capability

-- | Implicit automation admits higher-order routing only for a checked
-- proposition that itself contains one of the two approved set constructions.
-- This classification selects no premise and grants no authority.
implicitConstructionAdmission
    :: SupportedProposition local global
    -> FofCapability projection
    -> Maybe (Set ImplicitHigherOrderConstruction)
implicitConstructionAdmission proposition capability =
    case capability of
        FofProjectable{} ->
            Nothing
        RequiresTh0 exclusions
            | Set.null constructions ->
                Nothing
            | all (admittedExclusion constructions) exclusions ->
                Just constructions
            | otherwise ->
                Nothing
  where
    dependencies =
        foundationAxiomDependencies
            (supportedPropositionTerm proposition)
    constructions =
        Set.fromList
            ( [ ImplicitSeparation
              | SeparationCharacteristic `Set.member` dependencies
              ]
                <> [ ImplicitFunctionalReplacement
                   | ReplacementCharacteristic `Set.member` dependencies
                   ]
            )

    admittedExclusion allowed = \case
        StructuralFofExclusion HigherOrderLambda ->
            True
        StructuralFofExclusion (HigherOrderIntrinsic Sep) ->
            ImplicitSeparation `Set.member` allowed
        StructuralFofExclusion (HigherOrderIntrinsic Repl) ->
            ImplicitFunctionalReplacement `Set.member` allowed
        -- The checked proposition is the deliberate granularity: its typed
        -- global occurrences neither select another fact nor grant authority.
        HigherOrderGlobalType{} ->
            True
        StructuralFofExclusion{} ->
            False
        HigherOrderAmbientLocal{} ->
            False

validateImplicitHigherOrderAdmission
    :: SupportedProposition local global
    -> FofCapability claimProjection
    -> Vector (TypedBackendFact ref global)
    -> Vector (TypedLocalPremise local origin global)
    -> [TypedProblemAuxiliary global]
    -> Either (TypedProblemError local global) ()
validateImplicitHigherOrderAdmission
        claim claimCapability selectedFacts selectedLocals auxiliaries = do
    claimConstructions <-
        admittedPropositionConstructions claim claimCapability
    traverse_ requireFirstOrderGlobal selectedFacts
    localConstructions <-
        foldM
            (\admitted premise ->
                (admitted <>)
                    <$> admittedPropositionConstructions
                        (typedLocalPremiseProposition premise)
                        (typedLocalPremiseCapability premise))
            Set.empty
            (Vector.toList selectedLocals)
    let admitted = claimConstructions <> localConstructions
    traverse_ (requireAdmittedAuxiliary admitted) auxiliaries
  where
    admittedPropositionConstructions proposition = \case
        FofProjectable{} ->
            Right Set.empty
        RequiresTh0 exclusions ->
            maybe
                (Left
                    (TypedProblemExplicitHigherOrderJustificationRequired
                        exclusions))
                Right
                (implicitConstructionAdmission
                    proposition
                    (RequiresTh0 exclusions))

    requireFirstOrderGlobal fact =
        case typedBackendFactCapability fact of
            FofProjectable{} ->
                Right ()
            RequiresTh0 exclusions ->
                Left
                    (TypedProblemExplicitHigherOrderJustificationRequired
                        exclusions)

    requireAdmittedAuxiliary admitted auxiliary =
        case typedProblemAuxiliaryCapability auxiliary of
            FofProjectable{} ->
                Right ()
            RequiresTh0 exclusions
                | auxiliaryAdmitted admitted
                        (typedProblemAuxiliaryTag auxiliary) ->
                    Right ()
                | otherwise ->
                    Left
                        (TypedProblemExplicitHigherOrderJustificationRequired
                            exclusions)

    auxiliaryAdmitted admitted = \case
        SeparationCharacteristic ->
            ImplicitSeparation `Set.member` admitted
        ReplacementCharacteristic ->
            ImplicitFunctionalReplacement `Set.member` admitted
        _ ->
            False

validateLocalPremiseOrdinals
    :: [TypedLocalPremise local origin global]
    -> Either
        (TypedProblemError local global)
        ()
validateLocalPremiseOrdinals =
    void
        . foldM
            (\seen premise ->
                let ordinal =
                        typedLocalPremiseOrdinal premise
                in
                    if ordinal `Set.member` seen
                        then
                            Left
                                (TypedProblemDuplicateLocalPremiseOrdinal
                                    ordinal)
                        else
                            Right
                                (Set.insert
                                    ordinal
                                    seen))
            Set.empty

isFofCapability :: FofCapability projection -> Bool
isFofCapability = \case
    FofProjectable{} ->
        True
    RequiresTh0{} ->
        False

collectProblemGlobals
    :: Ord global
    => (global -> Maybe CoreType)
    -> SupportedProposition local global
    -> Vector (TypedBackendFact ref global)
    -> Vector (TypedLocalPremise local origin global)
    -> [TypedProblemAuxiliary global]
    -> Either
        (TypedProblemError local global)
        (Map global CoreType)
collectProblemGlobals
        globalType
        claim
        facts
        locals
        auxiliaries =
    Map.fromAscList
        <$> traverse
            resolveGlobal
            (Set.toAscList globals)
  where
    globals =
        canonicalGlobals
            (supportedPropositionTerm claim)
            <> foldMap
                (canonicalGlobals
                    . supportedPropositionTerm
                    . typedBackendFactProposition)
                facts
            <> foldMap
                (canonicalGlobals
                    . supportedPropositionTerm
                    . typedLocalPremiseProposition)
                locals
            <> foldMap
                (canonicalGlobals
                    . supportedPropositionTerm
                    . typedProblemAuxiliaryProposition)
                auxiliaries

    resolveGlobal global =
        case globalType global of
            Nothing ->
                Left
                    (TypedProblemClaimClassificationFailed
                        (UnknownBackendGlobal global))
            Just coreType ->
                Right (global, coreType)

collectProblemLocals
    :: Ord local
    => SupportedProposition local global
    -> Vector (TypedLocalPremise local origin global)
    -> Either
        (TypedProblemError local global)
        (Map local CoreType)
collectProblemLocals claim locals =
    foldM
        insertSupport
        Map.empty
        supports
  where
    supports =
        Vector.toList
            (supportedPropositionSupport claim)
            <> concatMap
                (Vector.toList
                    . supportedPropositionSupport
                    . typedLocalPremiseProposition)
                (Vector.toList locals)

    insertSupport current (local, coreType) =
        case Map.lookup local current of
            Nothing ->
                Right
                    (Map.insert
                        local
                        coreType
                        current)
            Just previousType
                | previousType == coreType ->
                    Right current
                | otherwise ->
                    Left
                        (TypedProblemLocalTypeMismatch
                            local
                            previousType
                            coreType)

typedProblemRoute
    :: TypedProblem ref local origin global
    -> TypedProblemRoute
typedProblemRoute
        (TypedProblem
            route
            _claim
            _facts
            _locals
            _auxiliaries
            _globals
            _localTypes) =
    route

typedProblemClaim
    :: TypedProblem ref local origin global
    -> SupportedProposition local global
typedProblemClaim
        (TypedProblem
            _route
            claim
            _facts
            _locals
            _auxiliaries
            _globals
            _localTypes) =
    claim

typedProblemGlobalPremises
    :: TypedProblem ref local origin global
    -> Vector (TypedBackendFact ref global)
typedProblemGlobalPremises
        (TypedProblem
            _route
            _claim
            facts
            _locals
            _auxiliaries
            _globals
            _localTypes) =
    facts

typedProblemLocalPremises
    :: TypedProblem ref local origin global
    -> Vector (TypedLocalPremise local origin global)
typedProblemLocalPremises
        (TypedProblem
            _route
            _claim
            _facts
            locals
            _auxiliaries
            _globals
            _localTypes) =
    locals

typedProblemAuxiliaries
    :: TypedProblem ref local origin global
    -> Vector (TypedProblemAuxiliary global)
typedProblemAuxiliaries
        (TypedProblem
            _route
            _claim
            _facts
            _locals
            auxiliaries
            _globals
            _localTypes) =
    auxiliaries

typedProblemGlobalTypes
    :: TypedProblem ref local origin global
    -> Map global CoreType
typedProblemGlobalTypes
        (TypedProblem
            _route
            _claim
            _facts
            _locals
            _auxiliaries
            globals
            _localTypes) =
    globals

typedProblemLocalTypes
    :: TypedProblem ref local origin global
    -> Map local CoreType
typedProblemLocalTypes
        (TypedProblem
            _route
            _claim
            _facts
            _locals
            _auxiliaries
            _globals
            localTypes) =
    localTypes