path: root/source/Test/Unit/Backend.hs

{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE OverloadedStrings #-}

module Test.Unit.Backend (unitTests) where

import Base hiding (Empty)
import Checking.Backend.Problem
import Checking.Backend.Tptp
import Checking.Core
import Checking.Foundation qualified as Foundation
import Provers
import Tptp.UnsortedFirstOrder qualified as Tptp

import Data.Map.Strict qualified as Map
import Data.Text qualified as Text
import Data.Vector (Vector)
import Data.Vector qualified as Vector
import Numeric.Natural (Natural)
import Test.Tasty
import Test.Tasty.HUnit


data TestGlobal
    = FirstOrderPredicate
    | HigherOrderPredicate
    deriving (Show, Eq, Ord)

testGlobalType :: TestGlobal -> Maybe CoreType
testGlobalType = \case
    FirstOrderPredicate ->
        Just (TySet `TyArrow` TyProp)
    HigherOrderPredicate ->
        Just
            ((TySet `TyArrow` TyProp)
                `TyArrow` TyProp)

data TestLocal
    = ObjectLocal
    | PredicateLocal
    deriving (Show, Eq, Ord)

unitTests :: TestTree
unitTests =
    testGroup "Typed backend problem"
        [ testCase
            "projects proposition equality as equivalence"
            classifiesPropositionEquality
        , testCase
            "projects exact ambient support"
            projectsExactAmbientSupport
        , testCase
            "routes implicit, explicit, and local-only problems"
            routesCompleteProblems
        , testCase
            "admits only checked implicit set constructions"
            admitsImplicitSetConstructions
        , testCase
            "renders checked FOF and TH0 problems"
            rendersCheckedProblems
        ]

classifiesPropositionEquality :: Assertion
classifiesPropositionEquality = do
    proposition <-
        checkedProposition
            Vector.empty
            (CEq TyProp CFalsum CFalsum)
    capability <-
        either
            (assertFailure . show)
            pure
            (classifySupportedProposition
                testGlobalType
                proposition)
    case capability of
        FofProjectable{} ->
            pure ()
        RequiresTh0 exclusions ->
            assertFailure
                ("proposition equality was not projected: "
                    <> show exclusions)

projectsExactAmbientSupport :: Assertion
projectsExactAmbientSupport = do
    let term :: CanonicalTerm Void
        term =
            CForall TySet
                (CEq TySet
                    (CBound 1)
                    (CBound 3))
    scoped <-
        either
            (assertFailure . show)
            pure
            (checkScopedCanonicalCore
                (const Nothing)
                [TySet, TySet, TySet]
                term)
    projected <-
        either
            (assertFailure . show)
            pure
            (projectSupportedProposition
                (const Nothing)
                (Vector.fromList
                    [ (0 :: Int, TySet)
                    , (1, TySet)
                    , (2, TySet)
                    ])
                scoped)
    assertEqual
        "unused middle support is removed"
        (Vector.fromList
            [ (0 :: Int, TySet)
            , (2, TySet)
            ])
        (supportedPropositionSupport projected)
    assertEqual
        "indices are remapped below nested binders"
        (CForall TySet
            (CEq TySet
                (CBound 1)
                (CBound 2)))
        (supportedPropositionTerm projected)

routesCompleteProblems :: Assertion
routesCompleteProblems = do
    fofFact <-
        checkedBackendFact
            (0 :: Int)
            firstOrderClaim
    th0Fact <-
        checkedBackendFact
            (1 :: Int)
            higherOrderClaim
    let fofFacts =
            Vector.singleton fofFact
        th0Facts =
            Vector.singleton th0Fact
    claim <-
        checkedProposition
            (Vector.singleton
                (ObjectLocal, TySet))
            (CApp
                (CGlobal FirstOrderPredicate)
                (CBound 0))
    firstOrderLocal <-
        checkedLocalPremise
            0
            "first-order local"
            claim
    higherOrderLocalProposition <-
        checkedProposition
            (Vector.singleton
                (PredicateLocal,
                    TySet `TyArrow` TyProp))
            (CApp
                (CGlobal HigherOrderPredicate)
                (CBound 0))
    higherOrderLocal <-
        checkedLocalPremise
            1
            "higher-order local"
            higherOrderLocalProposition

    implicit <-
        planned
            fofFacts
            claim
            [higherOrderLocal, firstOrderLocal]
            []
            ImplicitPremiseSelection
    assertEqual "implicit route" RouteFof
        (typedProblemRoute implicit)
    assertEqual "implicit FOF globals" [0]
        (typedBackendFactReference
            <$> toList
                (typedProblemGlobalPremises
                    implicit))
    assertEqual "first-order local only" [0]
        (localPremiseOrdinalValue
            . typedLocalPremiseOrdinal
            <$> toList
                (typedProblemLocalPremises
                    implicit))

    explicitFof <-
        planned
            fofFacts
            claim
            [firstOrderLocal]
            []
            ExplicitGlobalPremiseSelection
    assertEqual "explicit FOF route" RouteFof
        (typedProblemRoute explicitFof)

    explicitTh0 <-
        planned
            th0Facts
            claim
            [firstOrderLocal]
            []
            ExplicitGlobalPremiseSelection
    assertEqual "explicit TH0 route" RouteTh0
        (typedProblemRoute explicitTh0)

    localOnly <-
        planned
            Vector.empty
            claim
            [higherOrderLocal, firstOrderLocal]
            []
            LocalOnlyPremiseSelection
    assertEqual "local-only TH0 route" RouteTh0
        (typedProblemRoute localOnly)
    assertEqual "local order restored" [0, 1]
        (localPremiseOrdinalValue
            . typedLocalPremiseOrdinal
            <$> toList
                (typedProblemLocalPremises
                    localOnly))
    assertEqual
        "complete ambient local inventory"
        (Map.fromList
            [ (ObjectLocal, TySet)
            , (PredicateLocal,
                TySet `TyArrow` TyProp)
            ])
        (typedProblemLocalTypes localOnly)

    case planTypedProblem
            testGlobalType
            Vector.empty
            claim
            [firstOrderLocal, firstOrderLocal]
            []
            LocalOnlyPremiseSelection of
        Left
            (TypedProblemDuplicateLocalPremiseOrdinal
                duplicateOrdinal) ->
                    assertEqual
                        "duplicate local ordinal"
                        0
                        (localPremiseOrdinalValue
                            duplicateOrdinal)
        result ->
            assertFailure
                ("expected duplicate local ordinal error, got "
                    <> showProblemResult result)

    higherOrderClaimProposition <-
        checkedProposition
            Vector.empty
            higherOrderClaim
    case planTypedProblem
            testGlobalType
            fofFacts
            higherOrderClaimProposition
            []
            []
            ImplicitPremiseSelection of
        Left
            TypedProblemExplicitHigherOrderJustificationRequired{} ->
                pure ()
        result ->
            assertFailure
                ("expected explicit higher-order error, got "
                    <> showProblemResult result)
    checkedFoundationValue <-
        either
            (assertFailure . show)
            pure
            Foundation.checkedFoundation
    case planTypedProblem
            testGlobalType
            fofFacts
            claim
            []
            [typedFoundationAuxiliaryInput
                checkedFoundationValue
                Foundation.SeparationCharacteristic]
            ImplicitPremiseSelection of
        Left
            TypedProblemExplicitHigherOrderJustificationRequired{} ->
                pure ()
        result ->
            assertFailure
                ("expected implicit higher-order auxiliary error, got "
                    <> showProblemResult result)
    unusedContext <-
        either
            (assertFailure . show)
            pure
            (checkScopedCanonicalCore
                testGlobalType
                [TySet `TyArrow` TyProp]
                firstOrderClaim)
    case supportedProposition
            (Vector.singleton
                (PredicateLocal,
                    TySet `TyArrow` TyProp))
            unusedContext of
        Left (UnusedSupportedLocal PredicateLocal) ->
            pure ()
        Left err ->
            assertFailure
                ("unexpected exact-support error: "
                    <> show err)
        Right _ ->
            assertFailure
                "unused ambient local entered exact support"
  where
    planned selectedFacts claim locals auxiliaries selection =
        either
            (assertFailure . show)
            pure
            (planTypedProblem
                testGlobalType
                selectedFacts
                claim
                locals
                auxiliaries
                selection)

    showProblemResult = \case
        Left err ->
            show err
        Right problem ->
            show (typedProblemRoute problem)

admitsImplicitSetConstructions :: Assertion
admitsImplicitSetConstructions = do
    checkedFoundationValue <-
        either
            (assertFailure . show)
            pure
            Foundation.checkedFoundation
    let separation =
            CApp
                (CApp
                    (CIntrinsic Sep)
                    (CIntrinsic Empty))
                (CLam TySet
                    (CApp
                        (CGlobal HigherOrderPredicate)
                        (CLam TySet CFalsum)))
        separationClaim =
            CEq TySet separation separation
        filteredDomain =
            CApp
                (CApp
                    (CIntrinsic Sep)
                    (CBound 0))
                (CLam TySet
                    (CEq TySet (CBound 0) (CBound 0)))
        innerReplacement =
            CApp
                (CApp (CIntrinsic Repl) filteredDomain)
                (CLam TySet (CBound 0))
        functionalReplacement =
            CApp
                (CIntrinsic FamilyUnion)
                (CApp
                    (CApp
                        (CIntrinsic Repl)
                        (CIntrinsic Empty))
                    (CLam TySet innerReplacement))
        replacementClaim =
            CEq TySet functionalReplacement functionalReplacement
        replacementTags =
            [ Foundation.FamilyUnionCharacteristic
            , Foundation.SeparationCharacteristic
            , Foundation.ReplacementCharacteristic
            ]
        auxiliary tag =
            typedFoundationAuxiliaryInput
                checkedFoundationValue tag
        plan selected claim locals tags =
            planTypedProblem
                testGlobalType
                selected
                claim
                locals
                (auxiliary <$> tags)
                ImplicitPremiseSelection

    separationProposition <-
        checkedProposition Vector.empty separationClaim
    separationProblem <-
        either
            (assertFailure . show)
            pure
            (plan
                Vector.empty
                separationProposition
                []
                [Foundation.SeparationCharacteristic])
    assertEqual "separation implicit route" RouteTh0
        (typedProblemRoute separationProblem)
    assertEqual "separation characteristic only"
        [Foundation.SeparationCharacteristic]
        (typedProblemAuxiliaryTag
            <$> toList (typedProblemAuxiliaries separationProblem))
    assertEqual "separation selects no global premise"
        0
        (Vector.length (typedProblemGlobalPremises separationProblem))

    replacementProposition <-
        checkedProposition Vector.empty replacementClaim
    replacementProblem <-
        either
            (assertFailure . show)
            pure
            (plan
                Vector.empty
                replacementProposition
                []
                replacementTags)
    assertEqual "functional replacement implicit route" RouteTh0
        (typedProblemRoute replacementProblem)
    assertEqual "functional replacement exact helper set"
        replacementTags
        (typedProblemAuxiliaryTag
            <$> toList (typedProblemAuxiliaries replacementProblem))

    firstOrderProposition <-
        checkedProposition Vector.empty firstOrderClaim
    firstOrderLocal <-
        checkedLocalPremise 0 "first-order" firstOrderProposition
    separationLocal <-
        checkedLocalPremise 2 "separation" separationProposition
    unrelatedLocalProposition <-
        checkedProposition
            (Vector.singleton
                (PredicateLocal, TySet `TyArrow` TyProp))
            (CApp
                (CGlobal HigherOrderPredicate)
                (CBound 0))
    unrelatedLocal <-
        checkedLocalPremise 1 "unrelated higher-order" unrelatedLocalProposition
    localProblem <-
        either
            (assertFailure . show)
            pure
            (plan
                Vector.empty
                firstOrderProposition
                [unrelatedLocal, separationLocal, firstOrderLocal]
                [Foundation.SeparationCharacteristic])
    assertEqual "construction local promotes the complete problem" RouteTh0
        (typedProblemRoute localProblem)
    assertEqual "unrelated higher-order local remains unselected"
        [0, 2]
        ( localPremiseOrdinalValue
            . typedLocalPremiseOrdinal
            <$> toList (typedProblemLocalPremises localProblem)
        )

    higherOrderFact <- checkedBackendFact (1 :: Int) higherOrderClaim
    expectImplicitHigherOrderRejection
        "implicit higher-order global remains forbidden"
        (plan
            (Vector.singleton higherOrderFact)
            separationProposition
            []
            [Foundation.SeparationCharacteristic])

    ordinaryHigherOrder <-
        checkedProposition Vector.empty
            (CEq TySet
                (CApp
                    (CIntrinsic SetChoose)
                    (CLam TySet CFalsum))
                (CIntrinsic Empty))
    expectImplicitHigherOrderRejection
        "ordinary implicit higher-order target remains forbidden"
        (plan Vector.empty ordinaryHigherOrder [] [])
    mixedHigherOrder <-
        checkedProposition Vector.empty
            (CImp
                separationClaim
                (supportedPropositionTerm ordinaryHigherOrder))
    expectImplicitHigherOrderRejection
        "construction does not admit another higher-order intrinsic"
        (plan
            Vector.empty
            mixedHigherOrder
            []
            [Foundation.SeparationCharacteristic])

    expectImplicitHigherOrderRejection
        "auxiliary tag alone grants no construction permission"
        (plan
            Vector.empty
            firstOrderProposition
            []
            [Foundation.SeparationCharacteristic])
  where
    expectImplicitHigherOrderRejection label = \case
        Left TypedProblemExplicitHigherOrderJustificationRequired{} ->
            pure ()
        Left err ->
            assertFailure (label <> ": unexpected error " <> show err)
        Right problem ->
            assertFailure
                (label <> ": unexpectedly routed "
                    <> show (typedProblemRoute problem))

rendersCheckedProblems :: Assertion
rendersCheckedProblems = do
    fofFact <-
        checkedBackendFact
            (0 :: Int)
            firstOrderClaim
    th0Fact <-
        checkedBackendFact
            (1 :: Int)
            higherOrderClaim
    claim <-
        checkedProposition
            (Vector.singleton
                (ObjectLocal, TySet))
            (CApp
                (CGlobal FirstOrderPredicate)
                (CBound 0))
    fofProblem <-
        planned
            (Vector.singleton fofFact)
            claim
            ImplicitPremiseSelection
    th0Problem <-
        planned
            (Vector.singleton th0Fact)
            claim
            ExplicitGlobalPremiseSelection
    preparedFof <-
        either
            (assertFailure . show)
            pure
            (prepareTypedTptpProblem
                fofProblem)
    preparedTh0 <-
        either
            (assertFailure . show)
            pure
            (prepareTypedTptpProblem
                th0Problem)
    proverTask <-
        either
            (assertFailure . show)
            pure
            (prepareTypedProverTask
                DirectTask
                th0Problem)
    assertEqual "FOF route" RouteFof
        (preparedTypedTptpRoute preparedFof)
    assertBool "FOF formulas"
        ("fof(zf_h0,axiom,"
            `Text.isInfixOf`
                preparedTypedTptpText
                    preparedFof)
    assertBool "FOF has no TH0 declarations"
        (not
            ("thf("
                `Text.isInfixOf`
                    preparedTypedTptpText
                        preparedFof))
    assertEqual "TH0 route" RouteTh0
        (preparedTypedTptpRoute preparedTh0)
    assertEqual "TH0 request dialect"
        VerificationTh0
        (preparedVerificationDialect
            (preparedTypedProverRequest
                proverTask))
    assertEqual "request preserves exact prepared text"
        (preparedTypedTptpText preparedTh0)
        (preparedVerificationText
            (preparedTypedProverRequest
                proverTask))
    for_
        [ "thf(zf_h0,axiom,"
        , "^ [V0:$i]"
        , "thf(zf_q0,conjecture,"
        ]
        \fragment ->
            assertBool
                ("TH0 contains " <> Text.unpack fragment)
                (fragment
                    `Text.isInfixOf`
                        preparedTypedTptpText
                            preparedTh0)
    for_
        (Map.keys
            (preparedTypedTptpNameOrigins
                preparedTh0))
        \target ->
            assertBool
                ("valid generated name " <> Text.unpack target)
                (if "V" `Text.isPrefixOf` target
                    then Tptp.isProperVariable target
                    else Tptp.isProperAtomicWord target)
  where
    planned selectedFacts claim selection =
        either
            (assertFailure . show)
            pure
            (planTypedProblem
                testGlobalType
                selectedFacts
                claim
                []
                []
                selection)

firstOrderClaim :: CanonicalTerm TestGlobal
firstOrderClaim =
    CApp
        (CGlobal FirstOrderPredicate)
        (CIntrinsic Empty)

higherOrderClaim :: CanonicalTerm TestGlobal
higherOrderClaim =
    CApp
        (CGlobal HigherOrderPredicate)
        (CLam TySet
            (CApp
                (CGlobal FirstOrderPredicate)
                (CBound 0)))

checkedProposition
    :: Vector (TestLocal, CoreType)
    -> CanonicalTerm TestGlobal
    -> IO
        (SupportedProposition
            TestLocal
            TestGlobal)
checkedProposition support term = do
    checked <-
        either
            (assertFailure . show)
            pure
            (checkScopedCanonicalCore
                testGlobalType
                (snd <$> Vector.toList support)
                term)
    either
        (assertFailure . show)
        pure
        (supportedProposition support checked)

checkedClosedProposition
    :: CanonicalTerm TestGlobal
    -> IO
        (SupportedProposition
            Void
            TestGlobal)
checkedClosedProposition term = do
    checked <-
        either
            (assertFailure . show)
            pure
            (checkScopedCanonicalCore
                testGlobalType
                []
                term)
    either
        (assertFailure . show)
        pure
        (supportedProposition
            Vector.empty
            checked)

checkedBackendFact
    :: ref
    -> CanonicalTerm TestGlobal
    -> IO (TypedBackendFact ref TestGlobal)
checkedBackendFact reference term = do
    proposition <-
        checkedClosedProposition term
    capability <-
        either
            (assertFailure . show)
            pure
            (classifySupportedProposition
                testGlobalType
                proposition)
    pure
        (typedBackendFact
            reference
            proposition
            capability)

checkedLocalPremise
    :: Natural
    -> Text
    -> SupportedProposition TestLocal TestGlobal
    -> IO
        (TypedLocalPremise
            TestLocal
            Text
            TestGlobal)
checkedLocalPremise ordinal premiseOrigin proposition =
    either
        (assertFailure . show)
        pure
        (typedLocalPremise
            testGlobalType
            (localPremiseOrdinal ordinal)
            premiseOrigin
            proposition)