diff options
Diffstat (limited to 'source/Checking/Backend')
| -rw-r--r-- | source/Checking/Backend/Connection.hs | 1088 | ||||
| -rw-r--r-- | source/Checking/Backend/Reconstruction.hs | 253 |
2 files changed, 0 insertions, 1341 deletions
diff --git a/source/Checking/Backend/Connection.hs b/source/Checking/Backend/Connection.hs deleted file mode 100644 index 3a0eb19..0000000 --- a/source/Checking/Backend/Connection.hs +++ /dev/null @@ -1,1088 +0,0 @@ -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE NoImplicitPrelude #-} - --- | Bounded reconstruction for the first quantifier-free Horn slice. -module Checking.Backend.Connection - ( ConnectionLimits - , connectionLimits - , defaultConnectionLimits - , ConnectionLimitError(..) - , ConnectionProblem - , prepareConnectionProblem - , ConnectionUnsupported(..) - , ConnectionChoice - , connectionChoice - , connectionChoicePremiseOrdinal - , connectionChoiceChildren - , ConnectionTrace - , connectionTrace - , connectionTraceRoot - , ConnectionSearchResult(..) - , ConnectionSearchStats - , connectionSearchWork - , connectionSearchDerivedAtomCount - , connectionSearchMaximumCandidateDepth - , ConnectionExhaustion(..) - , searchConnectionProblem - , ReplayedConnection - , replayConnectionTrace - , replayedConnectionDerivation - , replayedConnectionImportUses - , replayedConnectionNodeCount - , replayedConnectionMaximumDepth - , ConnectionReplayFailure(..) - , ConnectionReplayMismatch(..) - ) where - -import Base -import Checking.Backend.Problem -import Checking.Core -import Checking.Kernel.Derivation - -import Control.Monad (foldM, unless, when) -import Data.Map.Strict qualified as Map -import Data.Set qualified as Set -import Data.Vector (Vector) -import Data.Vector qualified as Vector -import Numeric.Natural (Natural) - - -data ConnectionLimits = ConnectionLimits - !Natural - !Natural - !Natural - deriving stock (Show, Eq) - -data ConnectionLimitError - = ConnectionSearchWorkLimitIsZero - | ConnectionTraceNodeLimitIsZero - | ConnectionTraceDepthLimitIsZero - | ConnectionSearchWorkLimitTooLarge !Natural - | ConnectionTraceNodeLimitTooLarge !Natural - | ConnectionTraceDepthLimitTooLarge !Natural - deriving stock (Show, Eq) - -maximumConnectionSearchWork :: Natural -maximumConnectionSearchWork = - 1000000 - -maximumConnectionTraceNodes :: Natural -maximumConnectionTraceNodes = - 100000 - -maximumConnectionTraceDepth :: Natural -maximumConnectionTraceDepth = - 1000 - -connectionLimits - :: Natural - -> Natural - -> Natural - -> Either ConnectionLimitError ConnectionLimits -connectionLimits searchWorkLimit nodeLimit depthLimit - | searchWorkLimit == 0 = - Left ConnectionSearchWorkLimitIsZero - | nodeLimit == 0 = - Left ConnectionTraceNodeLimitIsZero - | depthLimit == 0 = - Left ConnectionTraceDepthLimitIsZero - | searchWorkLimit > maximumConnectionSearchWork = - Left - (ConnectionSearchWorkLimitTooLarge - searchWorkLimit) - | nodeLimit > maximumConnectionTraceNodes = - Left - (ConnectionTraceNodeLimitTooLarge - nodeLimit) - | depthLimit > maximumConnectionTraceDepth = - Left - (ConnectionTraceDepthLimitTooLarge - depthLimit) - | otherwise = - Right - (ConnectionLimits - searchWorkLimit - nodeLimit - depthLimit) - -defaultConnectionLimits :: ConnectionLimits -defaultConnectionLimits = - ConnectionLimits 100000 10000 128 - - -data ConnectionProblem ref origin global = - ConnectionProblem - !(TypedProblem ref Void origin global) - !(Vector (SearchRule global)) - -data ConnectionUnsupported ref - = ConnectionProblemRequiresTh0 - | ConnectionProblemHasLocalPremises - | ConnectionProblemHasFoundationAuxiliaries - | ConnectionClaimIsNotAtomic - | ConnectionPremiseIsNotHorn - !Natural - !ref - deriving stock (Show, Eq) - -prepareConnectionProblem - :: TypedProblem ref Void origin global - -> Either - (ConnectionUnsupported ref) - (ConnectionProblem ref origin global) -prepareConnectionProblem problem = do - unless - (typedProblemRoute problem == RouteFof) - (Left ConnectionProblemRequiresTh0) - unless - (Vector.null - (typedProblemLocalPremises problem)) - (Left ConnectionProblemHasLocalPremises) - unless - (Vector.null - (typedProblemAuxiliaries problem)) - (Left ConnectionProblemHasFoundationAuxiliaries) - unless - (searchAtom - (supportedPropositionTerm - (typedProblemClaim problem))) - (Left ConnectionClaimIsNotAtomic) - rules <- - traverse - preparePremise - (Vector.indexed - (typedProblemGlobalPremises - problem)) - pure (ConnectionProblem problem rules) - where - preparePremise (ordinal, premise) = - maybe - (Left - (ConnectionPremiseIsNotHorn - naturalOrdinal - (typedBackendFactReference - premise))) - Right - (searchRule - naturalOrdinal - (supportedPropositionTerm - (typedBackendFactProposition - premise))) - where - naturalOrdinal = - fromIntegral ordinal - - --- A Horn matrix clause, stored as negative antecedents and one positive head. -data SearchRule global = SearchRule - !Natural - !(Vector (CanonicalTerm global)) - !(CanonicalTerm global) - -searchRule - :: Natural - -> CanonicalTerm global - -> Maybe (SearchRule global) -searchRule ordinal statement = do - (antecedents, consequent) <- - collect [] statement - guard (searchAtom consequent) - pure - (SearchRule - ordinal - (Vector.fromList antecedents) - consequent) - where - collect reversed = \case - CImp premise conclusion -> do - guard (searchAtom premise) - collect - (premise : reversed) - conclusion - consequent -> - pure - ( reverse reversed - , consequent - ) - -searchAtom :: CanonicalTerm global -> Bool -searchAtom = \case - CBound{} -> - False - CGlobal{} -> - True - CIntrinsic{} -> - True - COpaqueInteger{} -> - True - CApp function argument -> - searchAtom function - && searchAtom argument - CLam{} -> - False - CFalsum -> - False - CImp{} -> - False - CEq{} -> - False - CForall{} -> - False - - -data ConnectionChoice = ConnectionChoice - !Natural - !(Vector ConnectionChoice) - deriving stock (Show, Eq) - -connectionChoice - :: Natural - -> [ConnectionChoice] - -> ConnectionChoice -connectionChoice ordinal children = - ConnectionChoice - ordinal - (Vector.fromList children) - -connectionChoicePremiseOrdinal - :: ConnectionChoice - -> Natural -connectionChoicePremiseOrdinal - (ConnectionChoice ordinal _children) = - ordinal - -connectionChoiceChildren - :: ConnectionChoice - -> Vector ConnectionChoice -connectionChoiceChildren - (ConnectionChoice _ordinal children) = - children - -newtype ConnectionTrace = - ConnectionTrace ConnectionChoice - deriving stock (Show, Eq) - -connectionTrace - :: ConnectionChoice - -> ConnectionTrace -connectionTrace = - ConnectionTrace - -connectionTraceRoot - :: ConnectionTrace - -> ConnectionChoice -connectionTraceRoot - (ConnectionTrace root) = - root - -data ConnectionSearchStats = ConnectionSearchStats - !Natural - !Natural - !Natural - deriving stock (Show, Eq) - -connectionSearchWork - :: ConnectionSearchStats - -> Natural -connectionSearchWork - (ConnectionSearchStats - work - _derivedAtoms - _maximumCandidateDepth) = - work - -connectionSearchDerivedAtomCount - :: ConnectionSearchStats - -> Natural -connectionSearchDerivedAtomCount - (ConnectionSearchStats - _work - derivedAtoms - _maximumCandidateDepth) = - derivedAtoms - -connectionSearchMaximumCandidateDepth - :: ConnectionSearchStats - -> Natural -connectionSearchMaximumCandidateDepth - (ConnectionSearchStats - _work - _derivedAtoms - maximumCandidateDepth) = - maximumCandidateDepth - -data ConnectionExhaustion - = ConnectionSearchWorkExhausted !Natural - | ConnectionTraceNodesExhausted !Natural - | ConnectionTraceDepthExhausted !Natural - deriving stock (Show, Eq) - -data ConnectionSearchResult - = ConnectionSearchFound - !ConnectionTrace - !ConnectionSearchStats - | ConnectionSearchUnavailable - !ConnectionSearchStats - | ConnectionSearchExhausted - !ConnectionExhaustion - !ConnectionSearchStats - deriving stock (Show, Eq) - -data SearchDerived = SearchDerived - !ConnectionChoice - !Natural - !Natural - -data SearchState global = SearchState - { searchStateWork :: !Natural - , searchStateDerivedAtomCount :: !Natural - , searchStateMaximumCandidateDepth :: !Natural - , searchStateDerived - :: !(Map (CanonicalTerm global) SearchDerived) - , searchStateRemainingAntecedents - :: !(Map Natural Natural) - , searchStateWaitingRules - :: !(Map - (CanonicalTerm global) - (Map Natural Natural)) - , searchStateReadyRules :: !(Set Natural) - , searchStateStructuralExhaustion - :: !(Maybe ConnectionExhaustion) - } - -searchConnectionProblem - :: Ord global - => ConnectionLimits - -> ConnectionProblem ref origin global - -> ConnectionSearchResult -searchConnectionProblem - limits - (ConnectionProblem problem rules) = - case buildSearchIndex limits rules of - Left (exhaustion, state) -> - ConnectionSearchExhausted - exhaustion - (searchStats state) - Right initial -> - runSearchAgenda - limits - rules - (problemClaimTerm problem) - initial - -emptySearchState :: SearchState global -emptySearchState = - SearchState - { searchStateWork = 0 - , searchStateDerivedAtomCount = 0 - , searchStateMaximumCandidateDepth = 0 - , searchStateDerived = Map.empty - , searchStateRemainingAntecedents = Map.empty - , searchStateWaitingRules = Map.empty - , searchStateReadyRules = Set.empty - , searchStateStructuralExhaustion = Nothing - } - -buildSearchIndex - :: Ord global - => ConnectionLimits - -> Vector (SearchRule global) - -> Either - (ConnectionExhaustion, SearchState global) - (SearchState global) -buildSearchIndex limits = - foldM registerRule emptySearchState - . Vector.toList - where - registerRule state - (SearchRule ordinal antecedents _consequent) = do - charged <- - chargeSearchWork limits state - let antecedentCount = - fromIntegral (Vector.length antecedents) - withRemaining = - charged - { searchStateRemainingAntecedents = - Map.insert - ordinal - antecedentCount - (searchStateRemainingAntecedents - charged) - , searchStateReadyRules = - if antecedentCount == 0 - then - Set.insert - ordinal - (searchStateReadyRules - charged) - else - searchStateReadyRules charged - } - foldM - (registerAntecedent ordinal) - withRemaining - (Vector.toList antecedents) - - registerAntecedent ordinal state antecedent = do - charged <- - chargeSearchWork limits state - pure - charged - { searchStateWaitingRules = - Map.insertWith - (Map.unionWith (+)) - antecedent - (Map.singleton ordinal 1) - (searchStateWaitingRules charged) - } - -runSearchAgenda - :: Ord global - => ConnectionLimits - -> Vector (SearchRule global) - -> CanonicalTerm global - -> SearchState global - -> ConnectionSearchResult -runSearchAgenda limits rules goal state = - case Set.minView (searchStateReadyRules state) of - Nothing -> - case searchStateStructuralExhaustion state of - Nothing -> - ConnectionSearchUnavailable - (searchStats state) - Just exhaustion -> - ConnectionSearchExhausted - exhaustion - (searchStats state) - Just (ordinal, remainingReady) -> - let withoutReady = - state - { searchStateReadyRules = - remainingReady - } - in case chargeSearchWork limits withoutReady of - Left (exhaustion, exhaustedState) -> - ConnectionSearchExhausted - exhaustion - (searchStats exhaustedState) - Right charged -> - considerReadyRule - limits - rules - goal - ordinal - charged - -considerReadyRule - :: Ord global - => ConnectionLimits - -> Vector (SearchRule global) - -> CanonicalTerm global - -> Natural - -> SearchState global - -> ConnectionSearchResult -considerReadyRule limits rules goal ordinal state = - case naturalVectorIndex ordinal rules of - Nothing -> - impossible - "a ready connection rule is outside the prepared rule vector" - Just (SearchRule _ antecedents consequent) - | Map.member consequent - (searchStateDerived state) -> - runSearchAgenda - limits - rules - goal - state - | otherwise -> - case traverse - (`Map.lookup` searchStateDerived state) - antecedents of - Nothing -> - impossible - "a ready connection rule has an unavailable antecedent" - Just antecedentProofs -> - considerCandidate - limits - rules - goal - ordinal - consequent - antecedentProofs - state - -considerCandidate - :: Ord global - => ConnectionLimits - -> Vector (SearchRule global) - -> CanonicalTerm global - -> Natural - -> CanonicalTerm global - -> Vector SearchDerived - -> SearchState global - -> ConnectionSearchResult -considerCandidate - limits - rules - goal - ordinal - consequent - antecedentProofs - state = - case candidateExhaustion limits nodeCount depth of - Just exhaustion -> - runSearchAgenda - limits - rules - goal - stateWithDepth - { searchStateStructuralExhaustion = - rememberExhaustion - exhaustion - (searchStateStructuralExhaustion - stateWithDepth) - } - Nothing -> - let choice = - ConnectionChoice - ordinal - (fmap searchDerivedChoice - antecedentProofs) - derived = - SearchDerived - choice - nodeCount - depth - withDerived = - stateWithDepth - { searchStateDerivedAtomCount = - searchStateDerivedAtomCount - stateWithDepth - + 1 - , searchStateDerived = - Map.insert - consequent - derived - (searchStateDerived - stateWithDepth) - } - in - if consequent == goal - then - ConnectionSearchFound - (connectionTrace choice) - (searchStats withDerived) - else - case activateWaitingRules - limits - consequent - withDerived of - Left (exhaustion, exhaustedState) -> - ConnectionSearchExhausted - exhaustion - (searchStats exhaustedState) - Right activated -> - runSearchAgenda - limits - rules - goal - activated - where - nodeCount = - Vector.foldl' - (\nodeTotal derived -> - saturatingAdd - (connectionTraceNodeLimit limits) - nodeTotal - (searchDerivedNodeCount derived)) - 1 - antecedentProofs - depth = - saturatingSuccessor - (connectionTraceDepthLimit limits) - (Vector.foldl' - (\maximumDepth derived -> - max maximumDepth - (searchDerivedDepth derived)) - 0 - antecedentProofs) - stateWithDepth = - state - { searchStateMaximumCandidateDepth = - max depth - (searchStateMaximumCandidateDepth - state) - } - -activateWaitingRules - :: Ord global - => ConnectionLimits - -> CanonicalTerm global - -> SearchState global - -> Either - (ConnectionExhaustion, SearchState global) - (SearchState global) -activateWaitingRules limits atom state = - foldM - activate - state - (maybe - [] - Map.toAscList - (Map.lookup atom - (searchStateWaitingRules state))) - where - activate current (ordinal, multiplicity) = do - charged <- - chargeSearchWork limits current - let remaining = - fromMaybe - (impossible - "a waiting connection rule has no remaining count") - (Map.lookup - ordinal - (searchStateRemainingAntecedents - charged)) - nextRemaining - | multiplicity <= remaining = - remaining - multiplicity - | otherwise = - impossible - "a waiting connection multiplicity exceeds its rule" - pure - charged - { searchStateRemainingAntecedents = - Map.insert - ordinal - nextRemaining - (searchStateRemainingAntecedents - charged) - , searchStateReadyRules = - if nextRemaining == 0 - then - Set.insert - ordinal - (searchStateReadyRules - charged) - else - searchStateReadyRules charged - } - -chargeSearchWork - :: ConnectionLimits - -> SearchState global - -> Either - (ConnectionExhaustion, SearchState global) - (SearchState global) --- One step registers a rule or antecedent, activates a waiting rule, or --- considers a ready rule. -chargeSearchWork limits state - | searchStateWork state - >= connectionSearchWorkLimit limits = - Left - ( ConnectionSearchWorkExhausted - (connectionSearchWorkLimit limits) - , state - ) - | otherwise = - Right - state - { searchStateWork = - searchStateWork state + 1 - } - -candidateExhaustion - :: ConnectionLimits - -> Natural - -> Natural - -> Maybe ConnectionExhaustion -candidateExhaustion limits nodes depth - | nodes > connectionTraceNodeLimit limits = - Just - (ConnectionTraceNodesExhausted - (connectionTraceNodeLimit limits)) - | depth > connectionTraceDepthLimit limits = - Just - (ConnectionTraceDepthExhausted - (connectionTraceDepthLimit limits)) - | otherwise = - Nothing - -rememberExhaustion - :: ConnectionExhaustion - -> Maybe ConnectionExhaustion - -> Maybe ConnectionExhaustion -rememberExhaustion exhaustion = \case - Nothing -> - Just exhaustion - previous -> - previous - -searchStats - :: SearchState global - -> ConnectionSearchStats -searchStats state = - ConnectionSearchStats - (searchStateWork state) - (searchStateDerivedAtomCount state) - (searchStateMaximumCandidateDepth state) - -searchDerivedChoice :: SearchDerived -> ConnectionChoice -searchDerivedChoice - (SearchDerived choice _nodeCount _depth) = - choice - -searchDerivedNodeCount :: SearchDerived -> Natural -searchDerivedNodeCount - (SearchDerived _choice nodeCount _depth) = - nodeCount - -searchDerivedDepth :: SearchDerived -> Natural -searchDerivedDepth - (SearchDerived _choice _nodeCount depth) = - depth - -connectionSearchWorkLimit :: ConnectionLimits -> Natural -connectionSearchWorkLimit - (ConnectionLimits workLimit _nodeLimit _depthLimit) = - workLimit - -connectionTraceNodeLimit :: ConnectionLimits -> Natural -connectionTraceNodeLimit - (ConnectionLimits _workLimit nodeLimit _depthLimit) = - nodeLimit - -connectionTraceDepthLimit :: ConnectionLimits -> Natural -connectionTraceDepthLimit - (ConnectionLimits _workLimit _nodeLimit depthLimit) = - depthLimit - -saturatingAdd - :: Natural - -> Natural - -> Natural - -> Natural -saturatingAdd limit left right - | left >= ceilingValue = - ceilingValue - | right >= ceilingValue - left = - ceilingValue - | otherwise = - left + right - where - ceilingValue = - limit + 1 - -saturatingSuccessor :: Natural -> Natural -> Natural -saturatingSuccessor limit value - | value >= limit = - limit + 1 - | otherwise = - value + 1 - - --- Replay rebuilds clauses independently from the search representation. -data ReplayClause global = ReplayClause - !Natural - !(Vector (CanonicalTerm global)) - !(CanonicalTerm global) - -replayClause - :: Natural - -> CanonicalTerm global - -> Maybe (ReplayClause global) -replayClause ordinal statement = - finish [] statement - where - finish reversed = \case - CImp premise conclusion - | replayAtom premise -> - finish - (premise : reversed) - conclusion - | otherwise -> - Nothing - consequent - | replayAtom consequent -> - Just - (ReplayClause - ordinal - (Vector.fromList - (reverse reversed)) - consequent) - | otherwise -> - Nothing - -replayAtom :: CanonicalTerm global -> Bool -replayAtom = \case - CGlobal{} -> - True - CIntrinsic{} -> - True - COpaqueInteger{} -> - True - CApp function argument -> - replayAtom function - && replayAtom argument - CBound{} -> - False - CLam{} -> - False - CFalsum -> - False - CImp{} -> - False - CEq{} -> - False - CForall{} -> - False - -data ReplayedConnection global = - ReplayedConnection - !(KernelDerivation global) - !(Set ImportIx) - !Natural - !Natural - -replayedConnectionDerivation - :: ReplayedConnection global - -> KernelDerivation global -replayedConnectionDerivation - (ReplayedConnection - derivation - _imports - _nodes - _maximumDepth) = - derivation - -replayedConnectionImportUses - :: ReplayedConnection global - -> Set ImportIx -replayedConnectionImportUses - (ReplayedConnection - _derivation - imports - _nodes - _maximumDepth) = - imports - -replayedConnectionNodeCount - :: ReplayedConnection global - -> Natural -replayedConnectionNodeCount - (ReplayedConnection - _derivation - _imports - nodes - _maximumDepth) = - nodes - -replayedConnectionMaximumDepth - :: ReplayedConnection global - -> Natural -replayedConnectionMaximumDepth - (ReplayedConnection - _derivation - _imports - _nodes - maximumDepth) = - maximumDepth - -data ConnectionReplayFailure - = ConnectionReplayExhausted !ConnectionExhaustion - | ConnectionReplayRejected !ConnectionReplayMismatch - deriving stock (Show, Eq) - -data ConnectionReplayMismatch - = ConnectionReplayProblemInvariantFailed - | ConnectionReplayChoiceOutOfBounds !Natural - | ConnectionReplayRepeatedChoice !Natural - | ConnectionReplayGoalMismatch !Natural - | ConnectionReplayChildCountMismatch - !Natural - !Natural - !Natural - deriving stock (Show, Eq) - -data ReplayState = ReplayState - !Natural - !Natural - -replayConnectionTrace - :: Eq global - => ConnectionLimits - -> ConnectionProblem ref origin global - -> ConnectionTrace - -> Either - ConnectionReplayFailure - (ReplayedConnection global) -replayConnectionTrace - limits - (ConnectionProblem problem _searchRules) - (ConnectionTrace root) = do - clauses <- - traverse - rebuildClause - (Vector.toList - (Vector.indexed - (typedProblemGlobalPremises - problem))) - (derivation, imports, ReplayState nodes maximumDepth) <- - replayGoal - limits - (Vector.fromList clauses) - Set.empty - 1 - (problemClaimTerm problem) - root - (ReplayState 0 0) - pure - (ReplayedConnection - derivation - imports - nodes - maximumDepth) - where - rebuildClause (ordinal, premise) = - maybe - (Left - (ConnectionReplayRejected - ConnectionReplayProblemInvariantFailed)) - Right - (replayClause - (fromIntegral ordinal) - (supportedPropositionTerm - (typedBackendFactProposition - premise))) - -problemClaimTerm - :: TypedProblem ref Void origin global - -> CanonicalTerm global -problemClaimTerm = - supportedPropositionTerm - . typedProblemClaim - -replayGoal - :: Eq global - => ConnectionLimits - -> Vector (ReplayClause global) - -> Set Natural - -> Natural - -> CanonicalTerm global - -> ConnectionChoice - -> ReplayState - -> Either - ConnectionReplayFailure - ( KernelDerivation global - , Set ImportIx - , ReplayState - ) -replayGoal - limits - clauses - path - depth - goal - (ConnectionChoice ordinal children) - (ReplayState nodes maximumDepth) = do - when - (depth > connectionTraceDepthLimit limits) - (Left - (ConnectionReplayExhausted - (ConnectionTraceDepthExhausted - (connectionTraceDepthLimit limits)))) - when - (nodes >= connectionTraceNodeLimit limits) - (Left - (ConnectionReplayExhausted - (ConnectionTraceNodesExhausted - (connectionTraceNodeLimit limits)))) - when - (ordinal `Set.member` path) - (Left - (ConnectionReplayRejected - (ConnectionReplayRepeatedChoice - ordinal))) - ReplayClause - clauseOrdinal - antecedents - consequent <- - maybe - (Left - (ConnectionReplayRejected - (ConnectionReplayChoiceOutOfBounds - ordinal))) - Right - (naturalVectorIndex - ordinal - clauses) - unless - (clauseOrdinal == ordinal - && consequent == goal) - (Left - (ConnectionReplayRejected - (ConnectionReplayGoalMismatch - ordinal))) - let expectedChildren = - Vector.length antecedents - actualChildren = - Vector.length children - unless - (expectedChildren == actualChildren) - (Left - (ConnectionReplayRejected - (ConnectionReplayChildCountMismatch - ordinal - (fromIntegral expectedChildren) - (fromIntegral actualChildren)))) - (childDerivations, imports, finalState) <- - foldM - replayChild - ( [] - , Set.singleton - (importIx ordinal) - , ReplayState - (nodes + 1) - (max depth maximumDepth) - ) - (Vector.toList - (Vector.zip - antecedents - children)) - pure - ( foldl' - implicationEliminationDerivation - (importedFactDerivation - (importIx ordinal)) - (reverse childDerivations) - , imports - , finalState - ) - where - replayChild - (reversed, imports, current) - (antecedent, child) = do - (derivation, childImports, next) <- - replayGoal - limits - clauses - (Set.insert ordinal path) - (depth + 1) - antecedent - child - current - pure - ( derivation : reversed - , imports <> childImports - , next - ) - -naturalVectorIndex - :: Natural - -> Vector value - -> Maybe value -naturalVectorIndex index values - | index > fromIntegral (maxBound :: Int) = - Nothing - | otherwise = - values Vector.!? fromIntegral index diff --git a/source/Checking/Backend/Reconstruction.hs b/source/Checking/Backend/Reconstruction.hs deleted file mode 100644 index 37ef99f..0000000 --- a/source/Checking/Backend/Reconstruction.hs +++ /dev/null @@ -1,253 +0,0 @@ -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE NoImplicitPrelude #-} - --- | Shadow and authoritative entry point for bounded proof reconstruction. -module Checking.Backend.Reconstruction - ( ReconstructionPolicy - , reconstructionPolicy - , reconstructionPolicyConnectionLimits - , reconstructionPolicyKernelReplayLimits - , defaultReconstructionPolicy - , ReconstructionOutcome(..) - , ReconstructionMismatch(..) - , ReconstructedVampireResult - , reconstructedPreparedTask - , reconstructedAcceptedRun - , reconstructedConnectionTrace - , reconstructedSearchStats - , reconstructedConnectionReplay - , attemptVampireReconstruction - ) where - -import Base -import Checking.Backend.Connection -import Checking.Kernel.Derivation - ( KernelReplayLimits - , defaultKernelReplayLimits - ) -import Provers - - -data ReconstructionPolicy = - ReconstructionPolicy - !ConnectionLimits - !KernelReplayLimits - deriving stock (Show, Eq) - -reconstructionPolicy - :: ConnectionLimits - -> KernelReplayLimits - -> ReconstructionPolicy -reconstructionPolicy = - ReconstructionPolicy - -reconstructionPolicyConnectionLimits - :: ReconstructionPolicy - -> ConnectionLimits -reconstructionPolicyConnectionLimits - (ReconstructionPolicy - connectionLimitsValue - _kernelReplayLimitsValue) = - connectionLimitsValue - -reconstructionPolicyKernelReplayLimits - :: ReconstructionPolicy - -> KernelReplayLimits -reconstructionPolicyKernelReplayLimits - (ReconstructionPolicy - _connectionLimitsValue - kernelReplayLimitsValue) = - kernelReplayLimitsValue - -defaultReconstructionPolicy :: ReconstructionPolicy -defaultReconstructionPolicy = - ReconstructionPolicy - defaultConnectionLimits - defaultKernelReplayLimits - -data ReconstructionOutcome ref origin global - = ReconstructionSucceeded - !(ReconstructedVampireResult - ref - origin - global) - | ReconstructionUnsupported - !(ConnectionUnsupported ref) - | ReconstructionUnavailable - !ConnectionSearchStats - | ReconstructionExhausted - !ConnectionExhaustion - !ConnectionSearchStats - | ReconstructionDefinitiveMismatch - !ReconstructionMismatch - -data ReconstructionMismatch - = ReconstructionAcceptedRequestMismatch - | ReconstructionReplayBudgetMismatch - !ConnectionExhaustion - | ReconstructionReplayRejected - !ConnectionReplayMismatch - deriving stock (Show, Eq) - -data ReconstructedVampireResult ref origin global = - ReconstructedVampireResult - !(PreparedTypedProverTask - ref - Void - origin - global) - !AcceptedVampireRun - !ConnectionTrace - !ConnectionSearchStats - !(ReplayedConnection global) - -reconstructedPreparedTask - :: ReconstructedVampireResult - ref - origin - global - -> PreparedTypedProverTask - ref - Void - origin - global -reconstructedPreparedTask - (ReconstructedVampireResult - prepared - _accepted - _trace - _searchStats - _replayed) = - prepared - -reconstructedAcceptedRun - :: ReconstructedVampireResult - ref - origin - global - -> AcceptedVampireRun -reconstructedAcceptedRun - (ReconstructedVampireResult - _prepared - accepted - _trace - _searchStats - _replayed) = - accepted - -reconstructedConnectionTrace - :: ReconstructedVampireResult - ref - origin - global - -> ConnectionTrace -reconstructedConnectionTrace - (ReconstructedVampireResult - _prepared - _accepted - connectionTraceValue - _searchStats - _replayed) = - connectionTraceValue - -reconstructedSearchStats - :: ReconstructedVampireResult - ref - origin - global - -> ConnectionSearchStats -reconstructedSearchStats - (ReconstructedVampireResult - _prepared - _accepted - _trace - searchStats - _replayed) = - searchStats - -reconstructedConnectionReplay - :: ReconstructedVampireResult - ref - origin - global - -> ReplayedConnection global -reconstructedConnectionReplay - (ReconstructedVampireResult - _prepared - _accepted - _trace - _searchStats - replayed) = - replayed - -attemptVampireReconstruction - :: Ord global - => ReconstructionPolicy - -> PreparedTypedProverTask - ref - Void - origin - global - -> AcceptedVampireRun - -> ReconstructionOutcome ref origin global -attemptVampireReconstruction - policy - prepared - accepted - | acceptedVampireRequest accepted - /= preparedTypedProverRequest prepared = - ReconstructionDefinitiveMismatch - ReconstructionAcceptedRequestMismatch - | otherwise = - case prepareConnectionProblem - (preparedTypedProverLogicalProblem - prepared) of - Left unsupported -> - ReconstructionUnsupported - unsupported - Right problem -> - finish problem - where - limits = - reconstructionPolicyConnectionLimits policy - - finish problem = - case searchConnectionProblem - limits - problem of - ConnectionSearchFound - connectionTraceValue - searchStats -> - case replayConnectionTrace - limits - problem - connectionTraceValue of - Left - (ConnectionReplayExhausted - exhaustion) -> - ReconstructionDefinitiveMismatch - (ReconstructionReplayBudgetMismatch - exhaustion) - Left - (ConnectionReplayRejected - mismatch) -> - ReconstructionDefinitiveMismatch - (ReconstructionReplayRejected - mismatch) - Right replayed -> - ReconstructionSucceeded - (ReconstructedVampireResult - prepared - accepted - connectionTraceValue - searchStats - replayed) - ConnectionSearchUnavailable searchStats -> - ReconstructionUnavailable - searchStats - ConnectionSearchExhausted - exhaustion - searchStats -> - ReconstructionExhausted - exhaustion - searchStats |