diff options
Diffstat (limited to 'source/Test/Unit/Backend.hs')
| -rw-r--r-- | source/Test/Unit/Backend.hs | 245 |
1 files changed, 0 insertions, 245 deletions
diff --git a/source/Test/Unit/Backend.hs b/source/Test/Unit/Backend.hs index 0c4ff71..11c36b8 100644 --- a/source/Test/Unit/Backend.hs +++ b/source/Test/Unit/Backend.hs @@ -4,18 +4,14 @@ module Test.Unit.Backend (unitTests) where import Base hiding (Empty) -import Checking.Backend.Connection qualified as Connection import Checking.Backend.Problem import Checking.Backend.Tptp import Checking.Core import Checking.Foundation qualified as Foundation -import Checking.Kernel.Derivation qualified as Derivation import Provers import Tptp.UnsortedFirstOrder qualified as Tptp -import Control.Monad (unless) import Data.Map.Strict qualified as Map -import Data.Set qualified as Set import Data.Text qualified as Text import Data.Vector (Vector) import Data.Vector qualified as Vector @@ -58,9 +54,6 @@ unitTests = , testCase "renders checked FOF and TH0 problems" rendersCheckedProblems - , testCase - "replays bounded Horn connection choices" - replaysHornConnections ] classifiesPropositionEquality :: Assertion @@ -450,216 +443,6 @@ rendersCheckedProblems = do globalPolicy localPolicy) -replaysHornConnections :: Assertion -replaysHornConnections = do - premiseP <- closedFrozen atomP - premisePtoQ <- - closedFrozen - (CImp atomP - (CImp atomP atomQ)) - premiseQtoR <- - closedFrozen (CImp atomQ atomR) - target <- closedFrozen atomR - facts <- - Vector.fromList - <$> sequence - [ checkedBackendFact - (0 :: Int) - atomP - , checkedBackendFact - 1 - (CImp atomP - (CImp atomP atomQ)) - , checkedBackendFact - 2 - (CImp atomQ atomR) - ] - claim <- - checkedClosedProposition atomR - problem <- - either - (assertFailure . show) - pure - (planTypedProblem - testGlobalType - facts - claim - [] - [] - ImplicitFofPremises - FirstOrderLocals) - connectionProblem <- - either - (assertFailure . show) - pure - (Connection.prepareConnectionProblem - problem) - threeNodeLimits <- - either - (assertFailure . show) - pure - (Connection.connectionLimits 100 3 8) - case Connection.searchConnectionProblem - threeNodeLimits - connectionProblem of - Connection.ConnectionSearchExhausted - (Connection.ConnectionTraceNodesExhausted 3) - _stats -> - pure () - result -> - assertFailure - ("expected expanded-node exhaustion, got " - <> show result) - fourNodeLimits <- - either - (assertFailure . show) - pure - (Connection.connectionLimits 100 4 8) - (foundTrace, searchStats) <- - case Connection.searchConnectionProblem - fourNodeLimits - connectionProblem of - Connection.ConnectionSearchFound - found - stats -> - pure (found, stats) - result -> - assertFailure - ("expected a Horn connection, got " - <> show result) - >> fail "unreachable" - assertEqual - "eleven charged search operations" - 11 - (Connection.connectionSearchWork - searchStats) - assertEqual - "three derived atoms" - 3 - (Connection.connectionSearchDerivedAtomCount - searchStats) - assertEqual - "candidate depth" - 3 - (Connection.connectionSearchMaximumCandidateDepth - searchStats) - let root = - Connection.connectionTraceRoot - foundTrace - assertEqual - "claim uses the final rule" - 2 - (Connection.connectionChoicePremiseOrdinal - root) - replayed <- - either - (assertFailure . show) - pure - (Connection.replayConnectionTrace - fourNodeLimits - connectionProblem - foundTrace) - assertEqual - "replay uses every exact premise" - (Set.fromList - [ Derivation.importIx 0 - , Derivation.importIx 1 - , Derivation.importIx 2 - ]) - (Connection.replayedConnectionImportUses - replayed) - assertEqual - "expanded replay nodes" - 4 - (Connection.replayedConnectionNodeCount - replayed) - assertEqual - "replay depth" - 3 - (Connection.replayedConnectionMaximumDepth - replayed) - checkedFoundationValue <- - either - (assertFailure . show) - pure - Foundation.checkedFoundation - imports <- - traverse - (either - (assertFailure . show) - pure - . Derivation.derivationImportJudgment) - [ premiseP - , premisePtoQ - , premiseQtoR - ] - kernelReplay <- - either - (assertFailure . show) - pure - (Derivation.replayKernelDerivation - checkedFoundationValue - Derivation.defaultKernelReplayLimits - testGlobalType - (Vector.fromList imports) - target - (Connection.replayedConnectionDerivation - replayed)) - assertEqual - "connection lifting proves the exact claim" - target - (Derivation.replayedKernelTarget - kernelReplay) - let wrongRoot = - Connection.connectionTrace - (Connection.connectionChoice - 1 - []) - case Connection.replayConnectionTrace - fourNodeLimits - connectionProblem - wrongRoot of - Left - (Connection.ConnectionReplayRejected - (Connection.ConnectionReplayGoalMismatch 1)) -> - pure () - result -> - assertFailure - ("expected changed-choice rejection, got " - <> case result of - Left err -> show err - Right _ -> "successful replay") - case Connection.replayConnectionTrace - threeNodeLimits - connectionProblem - foundTrace of - Left - (Connection.ConnectionReplayExhausted - (Connection.ConnectionTraceNodesExhausted 3)) -> - pure () - result -> - assertFailure - ("expected bounded replay exhaustion, got " - <> case result of - Left err -> show err - Right _ -> "successful replay") - tightWorkLimits <- - either - (assertFailure . show) - pure - (Connection.connectionLimits 10 4 8) - case Connection.searchConnectionProblem - tightWorkLimits - connectionProblem of - Connection.ConnectionSearchExhausted - (Connection.ConnectionSearchWorkExhausted 10) - _stats -> - pure () - result -> - assertFailure - ("expected bounded search exhaustion, got " - <> show result) - firstOrderClaim :: CanonicalTerm TestGlobal firstOrderClaim = CApp @@ -675,18 +458,6 @@ higherOrderClaim = (CGlobal FirstOrderPredicate) (CBound 0))) -atomP, atomQ, atomR :: CanonicalTerm TestGlobal -atomP = - firstOrderClaim -atomQ = - CApp - (CGlobal FirstOrderPredicate) - (COpaqueInteger 1) -atomR = - CApp - (CGlobal FirstOrderPredicate) - (COpaqueInteger 2) - checkedProposition :: Vector (TestLocal, CoreType) -> CanonicalTerm TestGlobal @@ -750,22 +521,6 @@ checkedBackendFact reference term = do proposition capability) -closedFrozen - :: CanonicalTerm TestGlobal - -> IO (FrozenCheckedCore TestGlobal) -closedFrozen term = do - checked <- - either - (assertFailure . show) - pure - (checkCanonicalCore - testGlobalType - term) - unless - (frozenCoreType checked == TyProp) - (assertFailure "fixture is not a proposition") - pure checked - checkedLocalPremise :: Natural -> Text |