Migrate to `Felix` namespaceHEADhotg

1 files changed, 752 insertions, 0 deletions

diff --git a/source/Felix/Test/Unit/Backend.hs b/source/Felix/Test/Unit/Backend.hs
new file mode 100644
index 0000000..384d21b
--- /dev/null
+++ b/source/Felix/Test/Unit/Backend.hs
@@ -0,0 +1,752 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE OverloadedStrings #-}
+
+module Felix.Test.Unit.Backend (unitTests) where
+
+import Base hiding (Empty)
+import Felix.Checking.Backend.Problem
+import Felix.Checking.Backend.Tptp
+import Felix.Checking.Core
+import Felix.Checking.Foundation qualified as Foundation
+import Felix.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]
+            []
+            FirstOrderLocals
+            ImplicitConstructionJustification
+    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
+            [higherOrderLocal, firstOrderLocal]
+            []
+            FirstOrderLocals
+            ExplicitHigherOrderJustification
+    assertEqual "explicit FOF route" RouteFof
+        (typedProblemRoute explicitFof)
+    assertEqual "explicit FOF references retain only FOF locals" [0]
+        (localPremiseOrdinalValue
+            . typedLocalPremiseOrdinal
+            <$> toList
+                (typedProblemLocalPremises explicitFof))
+
+    explicitTh0 <-
+        planned
+            th0Facts
+            claim
+            [higherOrderLocal, firstOrderLocal]
+            []
+            CompleteLocals
+            ExplicitHigherOrderJustification
+    assertEqual "explicit TH0 route" RouteTh0
+        (typedProblemRoute explicitTh0)
+    assertEqual "explicit TH0 references retain complete locals" [0, 1]
+        (localPremiseOrdinalValue
+            . typedLocalPremiseOrdinal
+            <$> toList
+                (typedProblemLocalPremises explicitTh0))
+
+    localOnly <-
+        planned
+            Vector.empty
+            claim
+            [higherOrderLocal, firstOrderLocal]
+            []
+            CompleteLocals
+            ExplicitHigherOrderJustification
+    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]
+            []
+            CompleteLocals
+            ExplicitHigherOrderJustification 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
+            []
+            []
+            FirstOrderLocals
+            ImplicitConstructionJustification 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]
+            FirstOrderLocals
+            ImplicitConstructionJustification 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 localPolicy higherOrderPolicy =
+        either
+            (assertFailure . show)
+            pure
+            (planTypedProblem
+                testGlobalType
+                selectedFacts
+                claim
+                locals
+                auxiliaries
+                localPolicy
+                higherOrderPolicy)
+
+    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)
+                FirstOrderLocals
+                ImplicitConstructionJustification
+
+    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
+    separationWithLocals <-
+        either
+            (assertFailure . show)
+            pure
+            (plan
+                Vector.empty
+                separationProposition
+                [unrelatedLocal, firstOrderLocal]
+                [Foundation.SeparationCharacteristic])
+    assertEqual "inline separation keeps unrelated HO local out" RouteTh0
+        (typedProblemRoute separationWithLocals)
+    assertEqual "inline separation retains only FOF local" [0]
+        ( localPremiseOrdinalValue
+            . typedLocalPremiseOrdinal
+            <$> toList (typedProblemLocalPremises separationWithLocals)
+        )
+    assertEqual "excluded HO local adds no auxiliary"
+        [Foundation.SeparationCharacteristic]
+        (typedProblemAuxiliaryTag
+            <$> toList (typedProblemAuxiliaries separationWithLocals))
+    localProblem <-
+        either
+            (assertFailure . show)
+            pure
+            (plan
+                Vector.empty
+                firstOrderProposition
+                [unrelatedLocal, separationLocal, firstOrderLocal]
+                [])
+    assertEqual "implicit construction local remains excluded" RouteFof
+        (typedProblemRoute localProblem)
+    assertEqual "unrelated higher-order local remains unselected"
+        [0]
+        ( 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
+            FirstOrderLocals
+            ImplicitConstructionJustification
+    th0Problem <-
+        planned
+            (Vector.singleton th0Fact)
+            claim
+            CompleteLocals
+            ExplicitHigherOrderJustification
+    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(tg_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(tg_h0,axiom,"
+        , "^ [V0:$i]"
+        , "thf(tg_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 localPolicy higherOrderPolicy =
+        either
+            (assertFailure . show)
+            pure
+            (planTypedProblem
+                testGlobalType
+                selectedFacts
+                claim
+                []
+                []
+                localPolicy
+                higherOrderPolicy)
+
+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)