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