Migrate to `Felix` namespaceHEADhotg

1 files changed, 1281 insertions, 0 deletions

diff --git a/source/Felix/Checking/Backend/Tptp.hs b/source/Felix/Checking/Backend/Tptp.hs
new file mode 100644
index 0000000..a5c0546
--- /dev/null
+++ b/source/Felix/Checking/Backend/Tptp.hs
@@ -0,0 +1,1281 @@
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- | Deterministic task-wide TPTP preparation for checked typed problems.
+module Felix.Checking.Backend.Tptp
+    ( TypedFormulaOccurrence(..)
+    , TypedTptpNameOrigin(..)
+    , PreparedTypedTptpProblem
+    , prepareTypedTptpProblem
+    , preparedTypedTptpRoute
+    , preparedTypedTptpText
+    , preparedTypedTptpTextNewline
+    , preparedTypedTptpConjectureText
+    , preparedTypedTptpNameOrigins
+    , TypedTptpPreparationError(..)
+    ) where
+
+import Base hiding (Empty)
+import Felix.Checking.Backend.Problem
+import Felix.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