Migrate to `Felix` namespaceHEADhotg

1 files changed, 0 insertions, 752 deletions

diff --git a/source/Test/Unit/Backend.hs b/source/Test/Unit/Backend.hs
deleted file mode 100644
index 5243c96..0000000
--- a/source/Test/Unit/Backend.hs
+++ /dev/null
@@ -1,752 +0,0 @@
-{-# 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 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)