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

{-# 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