diff options
Diffstat (limited to 'source/Checking/Backend/Reconstruction.hs')
| -rw-r--r-- | source/Checking/Backend/Reconstruction.hs | 253 |
1 files changed, 0 insertions, 253 deletions
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 |