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