diff options
Diffstat (limited to 'source/Test/Unit/Backend.hs')
| -rw-r--r-- | source/Test/Unit/Backend.hs | 752 |
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) |