diff options
Diffstat (limited to 'source/Test/Unit/Backend.hs')
| -rw-r--r-- | source/Test/Unit/Backend.hs | 219 |
1 files changed, 194 insertions, 25 deletions
diff --git a/source/Test/Unit/Backend.hs b/source/Test/Unit/Backend.hs index 11c36b8..81a911a 100644 --- a/source/Test/Unit/Backend.hs +++ b/source/Test/Unit/Backend.hs @@ -52,6 +52,9 @@ unitTests = "routes implicit, explicit, and local-only problems" routesCompleteProblems , testCase + "admits only checked implicit set constructions" + admitsImplicitSetConstructions + , testCase "renders checked FOF and TH0 problems" rendersCheckedProblems ] @@ -166,8 +169,7 @@ routesCompleteProblems = do claim [higherOrderLocal, firstOrderLocal] [] - ImplicitFofPremises - FirstOrderLocals + ImplicitPremiseSelection assertEqual "implicit route" RouteFof (typedProblemRoute implicit) assertEqual "implicit FOF globals" [0] @@ -188,8 +190,7 @@ routesCompleteProblems = do claim [firstOrderLocal] [] - ExplicitGlobalPremises - FirstOrderLocals + ExplicitGlobalPremiseSelection assertEqual "explicit FOF route" RouteFof (typedProblemRoute explicitFof) @@ -199,8 +200,7 @@ routesCompleteProblems = do claim [firstOrderLocal] [] - ExplicitGlobalPremises - FirstOrderLocals + ExplicitGlobalPremiseSelection assertEqual "explicit TH0 route" RouteTh0 (typedProblemRoute explicitTh0) @@ -210,8 +210,7 @@ routesCompleteProblems = do claim [higherOrderLocal, firstOrderLocal] [] - NoGlobalPremises - AllLocals + LocalOnlyPremiseSelection assertEqual "local-only TH0 route" RouteTh0 (typedProblemRoute localOnly) assertEqual "local order restored" [0, 1] @@ -235,8 +234,7 @@ routesCompleteProblems = do claim [firstOrderLocal, firstOrderLocal] [] - NoGlobalPremises - AllLocals of + LocalOnlyPremiseSelection of Left (TypedProblemDuplicateLocalPremiseOrdinal duplicateOrdinal) -> @@ -260,8 +258,7 @@ routesCompleteProblems = do higherOrderClaimProposition [] [] - ImplicitFofPremises - FirstOrderLocals of + ImplicitPremiseSelection of Left TypedProblemExplicitHigherOrderJustificationRequired{} -> pure () @@ -282,8 +279,7 @@ routesCompleteProblems = do [typedFoundationAuxiliaryInput checkedFoundationValue Foundation.SeparationCharacteristic] - ImplicitFofPremises - FirstOrderLocals of + ImplicitPremiseSelection of Left TypedProblemExplicitHigherOrderJustificationRequired{} -> pure () @@ -314,8 +310,7 @@ routesCompleteProblems = do assertFailure "unused ambient local entered exact support" where - planned selectedFacts claim locals auxiliaries - globalPolicy localPolicy = + planned selectedFacts claim locals auxiliaries selection = either (assertFailure . show) pure @@ -325,8 +320,7 @@ routesCompleteProblems = do claim locals auxiliaries - globalPolicy - localPolicy) + selection) showProblemResult = \case Left err -> @@ -334,6 +328,184 @@ routesCompleteProblems = do 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) + ImplicitPremiseSelection + + 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 + localProblem <- + either + (assertFailure . show) + pure + (plan + Vector.empty + firstOrderProposition + [unrelatedLocal, separationLocal, firstOrderLocal] + [Foundation.SeparationCharacteristic]) + assertEqual "construction local promotes the complete problem" RouteTh0 + (typedProblemRoute localProblem) + assertEqual "unrelated higher-order local remains unselected" + [0, 2] + ( 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 <- @@ -355,14 +527,12 @@ rendersCheckedProblems = do planned (Vector.singleton fofFact) claim - ImplicitFofPremises - FirstOrderLocals + ImplicitPremiseSelection th0Problem <- planned (Vector.singleton th0Fact) claim - ExplicitGlobalPremises - FirstOrderLocals + ExplicitGlobalPremiseSelection preparedFof <- either (assertFailure . show) @@ -430,7 +600,7 @@ rendersCheckedProblems = do then Tptp.isProperVariable target else Tptp.isProperAtomicWord target) where - planned selectedFacts claim globalPolicy localPolicy = + planned selectedFacts claim selection = either (assertFailure . show) pure @@ -440,8 +610,7 @@ rendersCheckedProblems = do claim [] [] - globalPolicy - localPolicy) + selection) firstOrderClaim :: CanonicalTerm TestGlobal firstOrderClaim = |