Migrate to `Felix` namespaceHEADhotg

2 files changed, 0 insertions, 2582 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
diff --git a/source/Checking/Backend/Tptp.hs b/source/Checking/Backend/Tptp.hs
deleted file mode 100644
index e70277e..0000000
--- a/source/Checking/Backend/Tptp.hs
+++ /dev/null
@@ -1,1281 +0,0 @@
-{-# LANGUAGE DerivingStrategies #-}
-{-# LANGUAGE NoImplicitPrelude #-}
-
--- | Deterministic task-wide TPTP preparation for checked typed problems.
-module Checking.Backend.Tptp
-    ( TypedFormulaOccurrence(..)
-    , TypedTptpNameOrigin(..)
-    , PreparedTypedTptpProblem
-    , prepareTypedTptpProblem
-    , preparedTypedTptpRoute
-    , preparedTypedTptpText
-    , preparedTypedTptpTextNewline
-    , preparedTypedTptpConjectureText
-    , preparedTypedTptpNameOrigins
-    , TypedTptpPreparationError(..)
-    ) where
-
-import Base hiding (Empty)
-import Checking.Backend.Problem
-import Checking.Core
-import Tptp.UnsortedFirstOrder qualified as Tptp
-
-import Control.Monad (foldM)
-import Control.Monad.State.Strict (StateT)
-import Control.Monad.State.Strict qualified as State
-import Control.Monad.Trans.Class (lift)
-import Data.Map.Strict qualified as Map
-import Data.Set qualified as Set
-import Data.Text qualified as Text
-import Data.Vector qualified as Vector
-import Numeric.Natural (Natural)
-import TextBuilder
-
-
-data TypedFormulaOccurrence ref
-    = TypedGlobalPremiseOccurrence !ref
-    | TypedLocalPremiseOccurrence !LocalPremiseOrdinal
-    | TypedAuxiliaryOccurrence !Natural
-    | TypedConjectureOccurrence
-    deriving stock (Show, Eq, Ord)
-
-data TypedTptpNameOrigin ref local global
-    = TypedGlobalNameOrigin !global
-    | TypedLocalNameOrigin !local
-    | TypedIntrinsicNameOrigin !CoreIntrinsicTag
-    | TypedIntegerNameOrigin !Integer
-    | TypedBinderNameOrigin !Natural
-    | TypedFormulaNameOrigin !(TypedFormulaOccurrence ref)
-    deriving stock (Show, Eq, Ord)
-
-data PreparedTypedTptpProblem ref local global =
-    PreparedTypedTptpProblem
-        !TypedProblemRoute
-        !Text
-        !Text
-        !(Map
-            Text
-            (TypedTptpNameOrigin ref local global))
-    deriving stock (Eq)
-
-preparedTypedTptpRoute
-    :: PreparedTypedTptpProblem ref local global
-    -> TypedProblemRoute
-preparedTypedTptpRoute
-        (PreparedTypedTptpProblem
-            route
-            _text
-            _conjecture
-            _origins) =
-    route
-
-preparedTypedTptpText
-    :: PreparedTypedTptpProblem ref local global
-    -> Text
-preparedTypedTptpText
-        (PreparedTypedTptpProblem
-            _route
-            problemText
-            _conjecture
-            _origins) =
-    problemText
-
-preparedTypedTptpTextNewline
-    :: PreparedTypedTptpProblem ref local global
-    -> Text
-preparedTypedTptpTextNewline =
-    (`Text.snoc` '\n')
-        . preparedTypedTptpText
-
-preparedTypedTptpConjectureText
-    :: PreparedTypedTptpProblem ref local global
-    -> Text
-preparedTypedTptpConjectureText
-        (PreparedTypedTptpProblem
-            _route
-            _text
-            conjecture
-            _origins) =
-    conjecture
-
-preparedTypedTptpNameOrigins
-    :: PreparedTypedTptpProblem ref local global
-    -> Map
-        Text
-        (TypedTptpNameOrigin ref local global)
-preparedTypedTptpNameOrigins
-        (PreparedTypedTptpProblem
-            _route
-            _text
-            _conjecture
-            origins) =
-    origins
-
-data TypedTptpPreparationError local global
-    = InvalidGeneratedTypedTptpName !Text
-    | DuplicateGeneratedTypedTptpName !Text
-    | TypedTptpUnknownGlobal !global
-    | TypedTptpUnknownLocal !local
-    | TypedTptpUnboundIndex !Natural
-    | TypedTptpFofProjectionMismatch
-    deriving stock (Show, Eq)
-
-
-data NameEnvironment ref local global =
-    NameEnvironment
-        !(Map global Tptp.AtomicWord)
-        !(Map global CoreType)
-        !(Map local Tptp.AtomicWord)
-        !(Map CoreIntrinsicTag Tptp.AtomicWord)
-        !(Map Integer Tptp.AtomicWord)
-        !(Map
-            Text
-            (TypedTptpNameOrigin ref local global))
-
-data RenderState ref local global =
-    RenderState
-        !Natural
-        !Natural
-        !(Map
-            Text
-            (TypedTptpNameOrigin ref local global))
-
-type Render ref local global =
-    StateT
-        (RenderState ref local global)
-        (Either
-            (TypedTptpPreparationError local global))
-
-data RenderedFormula ref = RenderedFormula
-    !Tptp.AtomicWord
-    !(TypedFormulaOccurrence ref)
-    !TextBuilder
-
-data BoundTarget
-    = BoundFofVariable !Tptp.Variable
-    | BoundTh0Variable !Tptp.Variable
-    | AmbientConstant !Tptp.AtomicWord
-
-prepareTypedTptpProblem
-    :: (Ord local, Ord global)
-    => TypedProblem ref local origin global
-    -> Either
-        (TypedTptpPreparationError local global)
-        (PreparedTypedTptpProblem ref local global)
-prepareTypedTptpProblem problem = do
-    names <-
-        allocateNames problem
-    let initialState =
-            RenderState
-                0
-                0
-                (nameEnvironmentOrigins names)
-    (rendered, finalState) <-
-        State.runStateT
-            (renderProblem names problem)
-            initialState
-    let (problemBuilder, conjectureBuilder) =
-            rendered
-        RenderState _nextBinder _nextHypothesis origins =
-            finalState
-    pure
-        (PreparedTypedTptpProblem
-            (typedProblemRoute problem)
-            (TextBuilder.toText problemBuilder)
-            (TextBuilder.toText conjectureBuilder)
-            origins)
-
-allocateNames
-    :: (Ord local, Ord global)
-    => TypedProblem ref local origin global
-    -> Either
-        (TypedTptpPreparationError local global)
-        (NameEnvironment ref local global)
-allocateNames problem = do
-    globalAllocations <-
-        allocateCategory
-            "tg_g"
-            TypedGlobalNameOrigin
-            (Map.keys
-                (typedProblemGlobalTypes
-                    problem))
-    localAllocations <-
-        allocateCategory
-            "tg_l"
-            TypedLocalNameOrigin
-            (Map.keys
-                (typedProblemLocalTypes
-                    problem))
-    intrinsicAllocations <-
-        allocateCategory
-            "tg_i"
-            TypedIntrinsicNameOrigin
-            (Set.toAscList
-                (problemIntrinsics problem))
-    integerAllocations <-
-        allocateCategory
-            "tg_n"
-            TypedIntegerNameOrigin
-            (Set.toAscList
-                (problemIntegers problem))
-    origins <-
-        foldM
-            (\current (target, nameOrigin) ->
-                insertOrigin
-                    (Tptp.atomicWordText target)
-                    nameOrigin
-                    current)
-            Map.empty
-            ( [ (target, nameOrigin)
-              | (_global, target, nameOrigin) <-
-                    globalAllocations
-              ]
-                <> [ (target, nameOrigin)
-                   | (_local, target, nameOrigin) <-
-                        localAllocations
-                   ]
-                <> [ (target, nameOrigin)
-                   | (_intrinsic, target, nameOrigin) <-
-                        intrinsicAllocations
-                   ]
-                <> [ (target, nameOrigin)
-                   | (_integer, target, nameOrigin) <-
-                        integerAllocations
-                   ]
-            )
-    pure
-        (NameEnvironment
-            (Map.fromList
-                [ (global, target)
-                | (global, target, _nameOrigin) <-
-                    globalAllocations
-                ])
-            (typedProblemGlobalTypes problem)
-            (Map.fromList
-                [ (local, target)
-                | (local, target, _nameOrigin) <-
-                    localAllocations
-                ])
-            (Map.fromList
-                [ (intrinsic, target)
-                | (intrinsic, target, _nameOrigin) <-
-                    intrinsicAllocations
-                ])
-            (Map.fromList
-                [ (integer, target)
-                | (integer, target, _nameOrigin) <-
-                    integerAllocations
-                ])
-            origins)
-  where
-    allocateCategory prefix makeOrigin semantics =
-        traverse
-            (\(ordinal, semantic) -> do
-                target <-
-                    generatedAtomicWord
-                        (prefix
-                            <> Text.pack
-                                (show ordinal))
-                pure
-                    ( semantic
-                    , target
-                    , makeOrigin semantic
-                    ))
-            (zip [0 :: Int ..] semantics)
-
-nameEnvironmentOrigins
-    :: NameEnvironment ref local global
-    -> Map
-        Text
-        (TypedTptpNameOrigin ref local global)
-nameEnvironmentOrigins
-        (NameEnvironment
-            _globals
-            _globalTypes
-            _locals
-            _intrinsics
-            _integers
-            origins) =
-    origins
-
-generatedAtomicWord
-    :: Text
-    -> Either
-        (TypedTptpPreparationError local global)
-        Tptp.AtomicWord
-generatedAtomicWord target =
-    maybe
-        (Left
-            (InvalidGeneratedTypedTptpName
-                target))
-        Right
-        (Tptp.atomicWord target)
-
-generatedVariable
-    :: Text
-    -> Either
-        (TypedTptpPreparationError local global)
-        Tptp.Variable
-generatedVariable target =
-    maybe
-        (Left
-            (InvalidGeneratedTypedTptpName
-                target))
-        Right
-        (Tptp.variable target)
-
-insertOrigin
-    :: Text
-    -> TypedTptpNameOrigin ref local global
-    -> Map
-        Text
-        (TypedTptpNameOrigin ref local global)
-    -> Either
-        (TypedTptpPreparationError local global)
-        (Map
-            Text
-            (TypedTptpNameOrigin ref local global))
-insertOrigin target nameOrigin origins =
-    if Map.member target origins
-        then
-            Left
-                (DuplicateGeneratedTypedTptpName
-                    target)
-        else
-            Right
-                (Map.insert
-                    target
-                    nameOrigin
-                    origins)
-
-renderProblem
-    :: (Ord local, Ord global)
-    => NameEnvironment ref local global
-    -> TypedProblem ref local origin global
-    -> Render
-        ref
-        local
-        global
-        (TextBuilder, TextBuilder)
-renderProblem names problem = do
-    hypotheses <-
-        renderHypotheses names problem
-    conjecture <-
-        renderConjecture names problem
-    declarations <-
-        case typedProblemRoute problem of
-            RouteFof ->
-                pure []
-            RouteTh0 ->
-                renderTh0Declarations
-                    names
-                    problem
-    let formulaBuilders =
-            renderFormulaLine
-                (typedProblemRoute problem)
-                "axiom"
-                <$> hypotheses
-        conjectureBuilder =
-            renderFormulaLine
-                (typedProblemRoute problem)
-                "conjecture"
-                conjecture
-        complete =
-            intercalate
-                (char '\n')
-                (declarations
-                    <> formulaBuilders
-                    <> [conjectureBuilder])
-    pure
-        ( complete
-        , conjectureBuilder
-        )
-
-renderHypotheses
-    :: (Ord local, Ord global)
-    => NameEnvironment ref local global
-    -> TypedProblem ref local origin global
-    -> Render
-        ref
-        local
-        global
-        [RenderedFormula ref]
-renderHypotheses names problem = do
-    globalFormulas <-
-        traverse
-            (\fact ->
-                renderOccurrence
-                    names
-                    problem
-                    (TypedGlobalPremiseOccurrence
-                        (typedBackendFactReference
-                            fact))
-                    (weakenClosedSupportedProposition
-                        (typedBackendFactProposition
-                            fact)))
-            (Vector.toList
-                (typedProblemGlobalPremises
-                    problem))
-    localFormulas <-
-        traverse
-            (\premise ->
-                renderOccurrence
-                    names
-                    problem
-                    (TypedLocalPremiseOccurrence
-                        (typedLocalPremiseOrdinal
-                            premise))
-                    (typedLocalPremiseProposition
-                        premise))
-            (Vector.toList
-                (typedProblemLocalPremises
-                    problem))
-    auxiliaryFormulas <-
-        traverse
-            (\auxiliary ->
-                renderOccurrence
-                    names
-                    problem
-                    (TypedAuxiliaryOccurrence
-                        (typedProblemAuxiliaryOrdinal
-                            auxiliary))
-                    (weakenClosedSupportedProposition
-                        (typedProblemAuxiliaryProposition
-                            auxiliary)))
-            (Vector.toList
-                (typedProblemAuxiliaries
-                    problem))
-    pure
-        (globalFormulas
-            <> localFormulas
-            <> auxiliaryFormulas)
-
-renderConjecture
-    :: (Ord local, Ord global)
-    => NameEnvironment ref local global
-    -> TypedProblem ref local origin global
-    -> Render
-        ref
-        local
-        global
-        (RenderedFormula ref)
-renderConjecture names problem =
-    renderOccurrence
-        names
-        problem
-        TypedConjectureOccurrence
-        (typedProblemClaim problem)
-
-renderOccurrence
-    :: (Ord local, Ord global)
-    => NameEnvironment ref local global
-    -> TypedProblem ref local origin global
-    -> TypedFormulaOccurrence ref
-    -> SupportedProposition local global
-    -> Render
-        ref
-        local
-        global
-        (RenderedFormula ref)
-renderOccurrence names problem occurrence proposition = do
-    target <-
-        case occurrence of
-            TypedConjectureOccurrence ->
-                liftEither
-                    (generatedAtomicWord "tg_q0")
-            _ -> do
-                ordinal <-
-                    nextHypothesisOrdinal
-                liftEither
-                    (generatedAtomicWord
-                        ("tg_h"
-                            <> Text.pack
-                                (show ordinal)))
-    registerOrigin
-        (Tptp.atomicWordText target)
-        (TypedFormulaNameOrigin occurrence)
-    bounds <-
-        initialBounds
-            names
-            proposition
-    formula <-
-        case typedProblemRoute problem of
-            RouteFof ->
-                renderFofFormula
-                    names
-                    bounds
-                    (supportedPropositionTerm
-                        proposition)
-            RouteTh0 ->
-                renderTh0Term
-                    names
-                    bounds
-                    (supportedPropositionTerm
-                        proposition)
-    pure
-        (RenderedFormula
-            target
-            occurrence
-            formula)
-
--- Formula and binder ordinals use separate dense namespaces.
-nextHypothesisOrdinal
-    :: Render ref local global Natural
-nextHypothesisOrdinal = do
-    RenderState nextBinder nextHypothesis origins <-
-        State.get
-    State.put
-        (RenderState
-            nextBinder
-            (nextHypothesis + 1)
-            origins)
-    pure nextHypothesis
-
-registerOrigin
-    :: Text
-    -> TypedTptpNameOrigin ref local global
-    -> Render ref local global ()
-registerOrigin target nameOrigin = do
-    RenderState nextBinder nextHypothesis origins <-
-        State.get
-    origins' <-
-        liftEither
-            (insertOrigin
-                target
-                nameOrigin
-                origins)
-    State.put
-        (RenderState
-            nextBinder
-            nextHypothesis
-            origins')
-
-freshBinder
-    :: Render ref local global Tptp.Variable
-freshBinder = do
-    RenderState nextBinder nextHypothesis origins <-
-        State.get
-    let target =
-            "V" <> Text.pack (show nextBinder)
-    variable <-
-        liftEither
-            (generatedVariable target)
-    origins' <-
-        liftEither
-            (insertOrigin
-                target
-                (TypedBinderNameOrigin
-                    nextBinder)
-                origins)
-    State.put
-        (RenderState
-            (nextBinder + 1)
-            nextHypothesis
-            origins')
-    pure variable
-
-liftEither
-    :: Either
-        (TypedTptpPreparationError local global)
-        value
-    -> Render ref local global value
-liftEither =
-    lift
-
-initialBounds
-    :: Ord local
-    => NameEnvironment ref local global
-    -> SupportedProposition local global
-    -> Render ref local global [BoundTarget]
-initialBounds
-        (NameEnvironment
-            _globals
-            _globalTypes
-            localNames
-            _intrinsics
-            _integers
-            _origins)
-        proposition =
-    traverse
-        (\(local, _coreType) ->
-            maybe
-                (lift
-                    (Left
-                        (TypedTptpUnknownLocal
-                            local)))
-                (pure . AmbientConstant)
-                (Map.lookup
-                    local
-                    localNames))
-        (Vector.toList
-            (supportedPropositionSupport
-                proposition))
-
-renderFormulaLine
-    :: TypedProblemRoute
-    -> TextBuilder
-    -> RenderedFormula ref
-    -> TextBuilder
-renderFormulaLine route role
-        (RenderedFormula target _occurrence formula) =
-    dialect
-        <> char '('
-        <> Tptp.buildAtomicWord target
-        <> char ','
-        <> role
-        <> char ','
-        <> formula
-        <> text ")."
-  where
-    dialect =
-        case route of
-            RouteFof ->
-                text "fof"
-            RouteTh0 ->
-                text "thf"
-
-
-renderFofFormula
-    :: (Ord global)
-    => NameEnvironment ref local global
-    -> [BoundTarget]
-    -> CanonicalTerm global
-    -> Render ref local global TextBuilder
-renderFofFormula names bounds = \case
-    CFalsum ->
-        pure (text "$false")
-    CImp premise conclusion -> do
-        premise' <-
-            renderFofFormula names bounds premise
-        conclusion' <-
-            renderFofFormula names bounds conclusion
-        pure
-            (parenthesize
-                (premise'
-                    <> text "=>"
-                    <> conclusion'))
-    CEq TySet left right -> do
-        left' <-
-            renderFofTerm names bounds left
-        right' <-
-            renderFofTerm names bounds right
-        pure
-            (parenthesize
-                (left'
-                    <> char '='
-                    <> right'))
-    CEq TyProp left right -> do
-        left' <-
-            renderFofFormula names bounds left
-        right' <-
-            renderFofFormula names bounds right
-        pure
-            (parenthesize
-                (left'
-                    <> text "<=>"
-                    <> right'))
-    CForall TySet body -> do
-        variable <-
-            freshBinder
-        body' <-
-            renderFofFormula
-                names
-                (BoundFofVariable variable
-                    : bounds)
-                body
-        pure
-            (parenthesize
-                (text "!["
-                    <> Tptp.buildVariable variable
-                    <> text "]:"
-                    <> body'))
-    application ->
-        renderFofApplication
-            names
-            bounds
-            TyProp
-            application
-
-renderFofTerm
-    :: Ord global
-    => NameEnvironment ref local global
-    -> [BoundTarget]
-    -> CanonicalTerm global
-    -> Render ref local global TextBuilder
-renderFofTerm names bounds = \case
-    CBound index ->
-        renderBound index bounds
-    CGlobal global ->
-        Tptp.buildAtomicWord
-            <$> lookupGlobal names global
-    CIntrinsic intrinsic ->
-        Tptp.buildAtomicWord
-            <$> lookupIntrinsic names intrinsic
-    COpaqueInteger integer ->
-        Tptp.buildAtomicWord
-            <$> lookupInteger names integer
-    application ->
-        renderFofApplication
-            names
-            bounds
-            TySet
-            application
-
-renderFofApplication
-    :: Ord global
-    => NameEnvironment ref local global
-    -> [BoundTarget]
-    -> CoreType
-    -> CanonicalTerm global
-    -> Render ref local global TextBuilder
-renderFofApplication names bounds expected application =
-    case applicationHead application of
-        (CGlobal global, arguments) -> do
-            coreType <-
-                maybe
-                    (lift
-                        (Left
-                            (TypedTptpUnknownGlobal
-                                global)))
-                    pure
-                    (Map.lookup
-                        global
-                        (nameEnvironmentGlobalTypes
-                            names))
-            renderHead
-                coreType
-                (lookupGlobal names global)
-                arguments
-        (CIntrinsic intrinsic, arguments) ->
-            renderHead
-                (coreIntrinsicType intrinsic)
-                (lookupIntrinsic names intrinsic)
-                arguments
-        _ ->
-            lift
-                (Left
-                    TypedTptpFofProjectionMismatch)
-  where
-    renderHead coreType targetAction arguments = do
-        unlessFofApplication
-            expected
-            coreType
-            arguments
-        target <-
-            targetAction
-        arguments' <-
-            traverse
-                (renderFofTerm names bounds)
-                arguments
-        pure
-            (applyAtomicWord
-                target
-                arguments')
-
--- Global types are retained in the problem, but names need only the allocated
--- symbols. FOF saturation was already checked by the projection witness.
-nameEnvironmentGlobalTypes
-    :: NameEnvironment ref local global
-    -> Map global CoreType
-nameEnvironmentGlobalTypes
-        (NameEnvironment
-            _globals
-            globalTypes
-            _locals
-            _intrinsics
-            _integers
-            _origins) =
-    globalTypes
-
-unlessFofApplication
-    :: CoreType
-    -> CoreType
-    -> [CanonicalTerm global]
-    -> Render ref local global ()
-unlessFofApplication expected coreType arguments =
-    case consume coreType arguments of
-        Just result
-            | result == expected ->
-                pure ()
-        _ ->
-            lift
-                (Left
-                    TypedTptpFofProjectionMismatch)
-  where
-    consume current = \case
-        [] ->
-            Just current
-        _argument : remaining ->
-            case current of
-                TyArrow TySet result ->
-                    consume result remaining
-                _ ->
-                    Nothing
-
-applyAtomicWord
-    :: Tptp.AtomicWord
-    -> [TextBuilder]
-    -> TextBuilder
-applyAtomicWord target = \case
-    [] ->
-        Tptp.buildAtomicWord target
-    arguments ->
-        Tptp.buildAtomicWord target
-            <> Tptp.buildTuple arguments
-
-renderBound
-    :: Natural
-    -> [BoundTarget]
-    -> Render ref local global TextBuilder
-renderBound index bounds =
-    case contextAt index bounds of
-        Nothing ->
-            lift
-                (Left
-                    (TypedTptpUnboundIndex
-                        index))
-        Just (BoundFofVariable variable) ->
-            pure
-                (Tptp.buildVariable
-                    variable)
-        Just (BoundTh0Variable variable) ->
-            pure
-                (Tptp.buildVariable
-                    variable)
-        Just (AmbientConstant target) ->
-            pure
-                (Tptp.buildAtomicWord
-                    target)
-
-
-renderTh0Term
-    :: Ord global
-    => NameEnvironment ref local global
-    -> [BoundTarget]
-    -> CanonicalTerm global
-    -> Render ref local global TextBuilder
-renderTh0Term names bounds = \case
-    CBound index ->
-        renderBound index bounds
-    CGlobal global ->
-        Tptp.buildAtomicWord
-            <$> lookupGlobal names global
-    CIntrinsic intrinsic ->
-        Tptp.buildAtomicWord
-            <$> lookupIntrinsic names intrinsic
-    COpaqueInteger integer ->
-        Tptp.buildAtomicWord
-            <$> lookupInteger names integer
-    CApp function argument -> do
-        function' <-
-            renderTh0Term names bounds function
-        argument' <-
-            renderTh0Term names bounds argument
-        pure
-            (parenthesize
-                (function'
-                    <> char '@'
-                    <> argument'))
-    CLam binderType body -> do
-        variable <-
-            freshBinder
-        body' <-
-            renderTh0Term
-                names
-                (BoundTh0Variable variable
-                    : bounds)
-                body
-        pure
-            (parenthesize
-                (text "^ ["
-                    <> Tptp.buildVariable variable
-                    <> char ':'
-                    <> renderCoreType binderType
-                    <> text "] : "
-                    <> body'))
-    CFalsum ->
-        pure (text "$false")
-    CImp premise conclusion -> do
-        premise' <-
-            renderTh0Term names bounds premise
-        conclusion' <-
-            renderTh0Term names bounds conclusion
-        pure
-            (parenthesize
-                (premise'
-                    <> text "=>"
-                    <> conclusion'))
-    CEq operandType left right -> do
-        left' <-
-            renderTh0Term names bounds left
-        right' <-
-            renderTh0Term names bounds right
-        pure
-            (parenthesize
-                (left'
-                    <> (case operandType of
-                        TyProp -> text "<=>"
-                        _ -> char '=')
-                    <> right'))
-    CForall binderType body -> do
-        variable <-
-            freshBinder
-        body' <-
-            renderTh0Term
-                names
-                (BoundTh0Variable variable
-                    : bounds)
-                body
-        pure
-            (parenthesize
-                (text "! ["
-                    <> Tptp.buildVariable variable
-                    <> char ':'
-                    <> renderCoreType binderType
-                    <> text "] : "
-                    <> body'))
-
-renderTh0Declarations
-    :: (Ord local, Ord global)
-    => NameEnvironment ref local global
-    -> TypedProblem ref local origin global
-    -> Render ref local global [TextBuilder]
-renderTh0Declarations names problem = do
-    globalDeclarations <-
-        traverse
-            (\(ordinal, (global, coreType)) -> do
-                target <-
-                    lookupGlobal names global
-                label <-
-                    liftEither
-                        (generatedAtomicWord
-                            ("tg_g_type_"
-                                <> Text.pack
-                                    (show ordinal)))
-                pure
-                    (typeDeclaration
-                        label
-                        target
-                        (renderCoreType coreType)))
-            (zip [0 :: Int ..]
-                (Map.toAscList
-                    (typedProblemGlobalTypes
-                        problem)))
-    localDeclarations <-
-        traverse
-            (\(ordinal, (local, coreType)) -> do
-                target <-
-                    lookupLocal names local
-                label <-
-                    liftEither
-                        (generatedAtomicWord
-                            ("tg_l_type_"
-                                <> Text.pack
-                                    (show ordinal)))
-                pure
-                    (typeDeclaration
-                        label
-                        target
-                        (renderCoreType coreType)))
-            (zip [0 :: Int ..]
-                (Map.toAscList
-                    (typedProblemLocalTypes
-                        problem)))
-    intrinsicDeclarations <-
-        traverse
-            (\(ordinal, intrinsic) -> do
-                target <-
-                    lookupIntrinsic names intrinsic
-                label <-
-                    liftEither
-                        (generatedAtomicWord
-                            ("tg_i_type_"
-                                <> Text.pack
-                                    (show ordinal)))
-                pure
-                    (typeDeclaration
-                        label
-                        target
-                        (renderCoreType
-                            (coreIntrinsicType
-                                intrinsic))))
-            (zip [0 :: Int ..]
-                (Set.toAscList
-                    (problemIntrinsics problem)))
-    integerDeclarations <-
-        traverse
-            (\(ordinal, integer) -> do
-                target <-
-                    lookupInteger names integer
-                label <-
-                    liftEither
-                        (generatedAtomicWord
-                            ("tg_n_type_"
-                                <> Text.pack
-                                    (show ordinal)))
-                pure
-                    (typeDeclaration
-                        label
-                        target
-                        (renderCoreType TySet)))
-            (zip [0 :: Int ..]
-                (Set.toAscList
-                    (problemIntegers problem)))
-    pure
-        (globalDeclarations
-            <> localDeclarations
-            <> intrinsicDeclarations
-            <> integerDeclarations)
-
-typeDeclaration
-    :: Tptp.AtomicWord
-    -> Tptp.AtomicWord
-    -> TextBuilder
-    -> TextBuilder
-typeDeclaration label target coreType =
-    text "thf("
-        <> Tptp.buildAtomicWord label
-        <> text ",type,("
-        <> Tptp.buildAtomicWord target
-        <> char ':'
-        <> coreType
-        <> text "))."
-
-renderCoreType :: CoreType -> TextBuilder
-renderCoreType = \case
-    TyProp ->
-        text "$o"
-    TySet ->
-        text "$i"
-    TyArrow argument result ->
-        parenthesize
-            (renderCoreType argument
-                <> char '>'
-                <> renderCoreType result)
-
-parenthesize :: TextBuilder -> TextBuilder
-parenthesize builder =
-    char '(' <> builder <> char ')'
-
-
-lookupGlobal
-    :: Ord global
-    => NameEnvironment ref local global
-    -> global
-    -> Render ref local global Tptp.AtomicWord
-lookupGlobal names global =
-    maybe
-        (lift
-            (Left
-                (TypedTptpUnknownGlobal
-                    global)))
-        pure
-        (lookupGlobalPure names global)
-
-lookupGlobalPure
-    :: Ord global
-    => NameEnvironment ref local global
-    -> global
-    -> Maybe Tptp.AtomicWord
-lookupGlobalPure
-        (NameEnvironment
-            globals
-            _globalTypes
-            _locals
-            _intrinsics
-            _integers
-            _origins) =
-    (`Map.lookup` globals)
-
-lookupLocalPure
-    :: Ord local
-    => NameEnvironment ref local global
-    -> local
-    -> Maybe Tptp.AtomicWord
-lookupLocalPure
-        (NameEnvironment
-            _globals
-            _globalTypes
-            locals
-            _intrinsics
-            _integers
-            _origins) =
-    (`Map.lookup` locals)
-
-lookupLocal
-    :: Ord local
-    => NameEnvironment ref local global
-    -> local
-    -> Render ref local global Tptp.AtomicWord
-lookupLocal names local =
-    maybe
-        (lift
-            (Left
-                (TypedTptpUnknownLocal
-                    local)))
-        pure
-        (lookupLocalPure names local)
-
-lookupIntrinsic
-    :: NameEnvironment ref local global
-    -> CoreIntrinsicTag
-    -> Render ref local global Tptp.AtomicWord
-lookupIntrinsic names intrinsic =
-    maybe
-        (lift
-            (Left
-                TypedTptpFofProjectionMismatch))
-        pure
-        (lookupIntrinsicPure names intrinsic)
-
-lookupIntrinsicPure
-    :: NameEnvironment ref local global
-    -> CoreIntrinsicTag
-    -> Maybe Tptp.AtomicWord
-lookupIntrinsicPure
-        (NameEnvironment
-            _globals
-            _globalTypes
-            _locals
-            intrinsics
-            _integers
-            _origins) =
-    (`Map.lookup` intrinsics)
-
-lookupInteger
-    :: NameEnvironment ref local global
-    -> Integer
-    -> Render ref local global Tptp.AtomicWord
-lookupInteger names integer =
-    maybe
-        (lift
-            (Left
-                TypedTptpFofProjectionMismatch))
-        pure
-        (lookupIntegerPure names integer)
-
-lookupIntegerPure
-    :: NameEnvironment ref local global
-    -> Integer
-    -> Maybe Tptp.AtomicWord
-lookupIntegerPure
-        (NameEnvironment
-            _globals
-            _globalTypes
-            _locals
-            _intrinsics
-            integers
-            _origins) =
-    (`Map.lookup` integers)
-
-problemIntrinsics
-    :: TypedProblem ref local origin global
-    -> Set CoreIntrinsicTag
-problemIntrinsics =
-    foldMap canonicalIntrinsics
-        . problemTerms
-
-problemIntegers
-    :: TypedProblem ref local origin global
-    -> Set Integer
-problemIntegers =
-    foldMap canonicalIntegers
-        . problemTerms
-
-problemTerms
-    :: TypedProblem ref local origin global
-    -> [CanonicalTerm global]
-problemTerms problem =
-    supportedPropositionTerm
-        (typedProblemClaim problem)
-        : (supportedPropositionTerm
-            . typedBackendFactProposition
-            <$> Vector.toList
-                (typedProblemGlobalPremises
-                    problem))
-        <> (supportedPropositionTerm
-            . typedLocalPremiseProposition
-            <$> Vector.toList
-                (typedProblemLocalPremises
-                    problem))
-        <> (supportedPropositionTerm
-            . typedProblemAuxiliaryProposition
-            <$> Vector.toList
-                (typedProblemAuxiliaries
-                    problem))
-
-canonicalIntrinsics
-    :: CanonicalTerm global
-    -> Set CoreIntrinsicTag
-canonicalIntrinsics = \case
-    CBound{} ->
-        mempty
-    CGlobal{} ->
-        mempty
-    CIntrinsic intrinsic ->
-        Set.singleton intrinsic
-    COpaqueInteger{} ->
-        mempty
-    CApp function argument ->
-        canonicalIntrinsics function
-            <> canonicalIntrinsics argument
-    CLam _binderType body ->
-        canonicalIntrinsics body
-    CFalsum ->
-        mempty
-    CImp premise conclusion ->
-        canonicalIntrinsics premise
-            <> canonicalIntrinsics conclusion
-    CEq _operandType left right ->
-        canonicalIntrinsics left
-            <> canonicalIntrinsics right
-    CForall _binderType body ->
-        canonicalIntrinsics body
-
-canonicalIntegers
-    :: CanonicalTerm global
-    -> Set Integer
-canonicalIntegers = \case
-    CBound{} ->
-        mempty
-    CGlobal{} ->
-        mempty
-    CIntrinsic{} ->
-        mempty
-    COpaqueInteger integer ->
-        Set.singleton integer
-    CApp function argument ->
-        canonicalIntegers function
-            <> canonicalIntegers argument
-    CLam _binderType body ->
-        canonicalIntegers body
-    CFalsum ->
-        mempty
-    CImp premise conclusion ->
-        canonicalIntegers premise
-            <> canonicalIntegers conclusion
-    CEq _operandType left right ->
-        canonicalIntegers left
-            <> canonicalIntegers right
-    CForall _binderType body ->
-        canonicalIntegers body
-
-applicationHead
-    :: CanonicalTerm global
-    -> (CanonicalTerm global, [CanonicalTerm global])
-applicationHead =
-    go []
-  where
-    go arguments = \case
-        CApp function argument ->
-            go (argument : arguments) function
-        headTerm ->
-            (headTerm, arguments)
-
-contextAt :: Natural -> [value] -> Maybe value
-contextAt _index [] =
-    Nothing
-contextAt 0 (value : _remaining) =
-    Just value
-contextAt index (_value : remaining) =
-    contextAt (index - 1) remaining