Migrate to `Felix` namespaceHEADhotg

1 files changed, 0 insertions, 1281 deletions

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