Migrate to `Felix` namespaceHEADhotg

1 files changed, 0 insertions, 1301 deletions

diff --git a/source/Checking/Backend/Problem.hs b/source/Checking/Backend/Problem.hs
deleted file mode 100644
index 8d3a071..0000000
--- a/source/Checking/Backend/Problem.hs
+++ /dev/null
@@ -1,1301 +0,0 @@
-{-# LANGUAGE DerivingStrategies #-}
-{-# LANGUAGE NoImplicitPrelude #-}
-
--- | Complete-problem FOF/TH0 classification and construction.
-module 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 Checking.Core
-import 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