diff options
Diffstat (limited to 'source/Checking/Obligation.hs')
| -rw-r--r-- | source/Checking/Obligation.hs | 428 |
1 files changed, 0 insertions, 428 deletions
diff --git a/source/Checking/Obligation.hs b/source/Checking/Obligation.hs deleted file mode 100644 index 22309b7..0000000 --- a/source/Checking/Obligation.hs +++ /dev/null @@ -1,428 +0,0 @@ -{-# LANGUAGE NoImplicitPrelude #-} - --- | Strict, invocation-local proof obligations emitted by the legacy checker. -module Checking.Obligation - ( ObligationPremiseOrigin(..) - , PreparedPremise - , preparedPremise - , preparedPremiseHypothesis - , preparedPremiseOrigin - , PreparedObligation - , preparedObligationOrdinal - , preparedObligationProverTask - , preparedObligationTask - , ObligationMethod(..) - , preparedObligationMethod - , preparedObligationSelectedPremises - , PreparedObligationBatch - , preparedBatchMarker - , preparedBatchLocation - , preparedBatchPremises - , preparedBatchObligations - , prepareObligationBatch - , prepareOmittedObligationBatch - , ResolvedObligation - , resolvedObligationPrepared - , resolvedObligationVampireRun - , resolvedObligationGapLocation - , ResolvedObligationBatch - , resolvedBatchPrepared - , resolvedBatchObligations - , resolveObligationWithVampire - , resolveObligationAsGap - , resolveObligationBatch - , ObligationResolutionError(..) - ) where - -import Base -import Checking.Facts qualified as Facts -import Checking.Legacy -import Provers -import Report.Location -import Syntax.Internal - -import Control.Monad (unless) -import Data.Vector (Vector) -import Data.Vector qualified as Vector - - -data ObligationPremiseOrigin - = RegisteredFactPremise !Facts.FactOrigin - | RegisteredLegacyFactPremise - !LegacyFactRef - !Facts.FactOrigin - !LegacyTrustDependencies - | LocalHypothesisPremise !Location !Marker - deriving (Show, Eq) - -data PreparedPremise = PreparedPremise - !Hypothesis - !ObligationPremiseOrigin - deriving (Show, Eq) - -preparedPremise - :: Hypothesis - -> ObligationPremiseOrigin - -> PreparedPremise -preparedPremise = PreparedPremise - -preparedPremiseHypothesis :: PreparedPremise -> Hypothesis -preparedPremiseHypothesis - (PreparedPremise hypothesis _origin) = - hypothesis - -preparedPremiseOrigin - :: PreparedPremise - -> ObligationPremiseOrigin -preparedPremiseOrigin - (PreparedPremise _hypothesis origin) = - origin - - -data ObligationMethod - = ProveWithVampire - | RecordExplicitGap !Location - deriving (Show, Eq) - -data PreparedObligation = PreparedObligation - !LegacyObligationOrdinal - !PreparedProverTask - !ObligationMethod - !(Vector PreparedPremise) - -preparedObligationOrdinal - :: PreparedObligation - -> LegacyObligationOrdinal -preparedObligationOrdinal - (PreparedObligation ordinal _proverTask _method _premises) = - ordinal - -preparedObligationProverTask - :: PreparedObligation - -> PreparedProverTask -preparedObligationProverTask - (PreparedObligation _ordinal proverTask _method _premises) = - proverTask - -preparedObligationMethod :: PreparedObligation -> ObligationMethod -preparedObligationMethod - (PreparedObligation _ordinal _proverTask method _premises) = - method - -preparedObligationSelectedPremises - :: PreparedObligation - -> Vector PreparedPremise -preparedObligationSelectedPremises - (PreparedObligation _ordinal _proverTask _method premises) = - premises - -preparedObligationTask :: PreparedObligation -> Task -preparedObligationTask = - preparedProverLogicalTask . preparedObligationProverTask - - -data PreparedObligationBatch = PreparedObligationBatch - !Marker - !Location - !(Vector PreparedPremise) - !(Vector PreparedObligation) - -preparedBatchMarker :: PreparedObligationBatch -> Marker -preparedBatchMarker - (PreparedObligationBatch marker _location _premises _obligations) = - marker - -preparedBatchLocation :: PreparedObligationBatch -> Location -preparedBatchLocation - (PreparedObligationBatch _marker location _premises _obligations) = - location - -preparedBatchPremises - :: PreparedObligationBatch - -> Vector PreparedPremise -preparedBatchPremises - (PreparedObligationBatch _marker _location premises _obligations) = - premises - -preparedBatchObligations - :: PreparedObligationBatch - -> Vector PreparedObligation -preparedBatchObligations - (PreparedObligationBatch _marker _location _premises obligations) = - obligations - - -prepareObligationBatch - :: (Task -> Task) - -> LegacyObligationOrdinal - -> [PreparedPremise] - -> Directness - -> Marker - -> Location - -> [Formula] - -> (PreparedObligationBatch, LegacyObligationOrdinal) -prepareObligationBatch - prepareTask - firstOrdinal - premises - directness - marker - location - goals = - prepareObligationBatchWith - ProveWithVampire - prepareTask - firstOrdinal - premises - directness - marker - location - goals - -prepareOmittedObligationBatch - :: (Task -> Task) - -> LegacyObligationOrdinal - -> [PreparedPremise] - -> Directness - -> Marker - -> Location - -> [Formula] - -> (PreparedObligationBatch, LegacyObligationOrdinal) -prepareOmittedObligationBatch - prepareTask - firstOrdinal - premises - directness - marker - location - goals = - prepareObligationBatchWith - (RecordExplicitGap location) - prepareTask - firstOrdinal - premises - directness - marker - location - goals - -prepareObligationBatchWith - :: ObligationMethod - -> (Task -> Task) - -> LegacyObligationOrdinal - -> [PreparedPremise] - -> Directness - -> Marker - -> Location - -> [Formula] - -> (PreparedObligationBatch, LegacyObligationOrdinal) -prepareObligationBatchWith - method - prepareTask - firstOrdinal - premises - directness - marker - location - goals = - let (obligations, nextOrdinal) = - prepareGoals firstOrdinal goals - in - ( PreparedObligationBatch - marker - location - (Vector.fromList premises) - (Vector.fromList obligations) - , nextOrdinal - ) - where - hypotheses = - preparedPremiseHypothesis <$> premises - - prepareGoals ordinal = \case - [] -> - ([], ordinal) - goal : remainingGoals -> - let task = - prepareTask - (Task - directness - hypotheses - marker - location - goal) - proverTask = prepareProverTask task - obligation = - PreparedObligation - ordinal - proverTask - method - (selectedPremises - (taskHypotheses task) - premises) - nextOrdinal = - legacyObligationOrdinal - (legacyObligationOrdinalValue ordinal + 1) - (remaining, finalOrdinal) = - prepareGoals nextOrdinal remainingGoals - in - proverTask `seq` - ( obligation : remaining - , finalOrdinal - ) - --- Task preparation may only select existing premises. Resolution checks this --- inventory before it can authorize a fact. -selectedPremises - :: [Hypothesis] - -> [PreparedPremise] - -> Vector PreparedPremise -selectedPremises hypotheses premises = - Vector.fromList (go hypotheses premises) - where - go [] _available = - [] - go (hypothesis : remaining) available = - case takeMatching hypothesis available of - Nothing -> - [] - Just (premise, available') -> - premise : go remaining available' - - takeMatching _hypothesis [] = - Nothing - takeMatching hypothesis (premise : remaining) - | preparedPremiseHypothesis premise == hypothesis = - Just (premise, remaining) - | otherwise = do - (found, remaining') <- - takeMatching hypothesis remaining - pure (found, premise : remaining') - - -data ResolvedObligation = ResolvedObligation - !PreparedObligation - !(Either Location AcceptedVampireRun) - -resolvedObligationPrepared - :: ResolvedObligation - -> PreparedObligation -resolvedObligationPrepared - (ResolvedObligation prepared _evidence) = - prepared - -resolvedObligationVampireRun - :: ResolvedObligation - -> Maybe AcceptedVampireRun -resolvedObligationVampireRun - (ResolvedObligation _prepared evidence) = - either (const Nothing) Just evidence - -resolvedObligationGapLocation - :: ResolvedObligation - -> Maybe Location -resolvedObligationGapLocation - (ResolvedObligation _prepared evidence) = - either Just (const Nothing) evidence - -data ResolvedObligationBatch = ResolvedObligationBatch - !PreparedObligationBatch - !(Vector ResolvedObligation) - -resolvedBatchPrepared - :: ResolvedObligationBatch - -> PreparedObligationBatch -resolvedBatchPrepared - (ResolvedObligationBatch prepared _resolved) = - prepared - -resolvedBatchObligations - :: ResolvedObligationBatch - -> Vector ResolvedObligation -resolvedBatchObligations - (ResolvedObligationBatch _prepared resolved) = - resolved - -data ObligationResolutionError - = VampireEvidenceForGap - | GapEvidenceForVampire - | VampireRequestMismatch - | ResolvedBatchLengthMismatch !Int !Int - | ResolvedBatchObligationMismatch !LegacyObligationOrdinal - deriving (Show, Eq) - -resolveObligationWithVampire - :: PreparedObligation - -> AcceptedVampireRun - -> Either ObligationResolutionError ResolvedObligation -resolveObligationWithVampire prepared accepted = - case preparedObligationMethod prepared of - RecordExplicitGap{} -> - Left VampireEvidenceForGap - ProveWithVampire - | acceptedVampireRequest accepted - == preparedProverRequest - (preparedObligationProverTask prepared) -> - Right - (ResolvedObligation - prepared - (Right accepted)) - | otherwise -> - Left VampireRequestMismatch - -resolveObligationAsGap - :: PreparedObligation - -> Either ObligationResolutionError ResolvedObligation -resolveObligationAsGap prepared = - case preparedObligationMethod prepared of - ProveWithVampire -> - Left GapEvidenceForVampire - RecordExplicitGap location -> - Right - (ResolvedObligation - prepared - (Left location)) - -resolveObligationBatch - :: PreparedObligationBatch - -> Vector ResolvedObligation - -> Either ObligationResolutionError ResolvedObligationBatch -resolveObligationBatch prepared resolved - | Vector.length expected /= Vector.length resolved = - Left - (ResolvedBatchLengthMismatch - (Vector.length expected) - (Vector.length resolved)) - | otherwise = do - Vector.zipWithM_ - validate - expected - resolved - pure (ResolvedObligationBatch prepared resolved) - where - expected = - preparedBatchObligations prepared - - validate expectedObligation actual = - unless - (samePreparedObligation - expectedObligation - (resolvedObligationPrepared actual)) - (Left - (ResolvedBatchObligationMismatch - (preparedObligationOrdinal - expectedObligation))) - - samePreparedObligation left right = - preparedObligationOrdinal left - == preparedObligationOrdinal right - && preparedObligationMethod left - == preparedObligationMethod right - && preparedObligationTask left - == preparedObligationTask right - && preparedProverRequest - (preparedObligationProverTask left) - == preparedProverRequest - (preparedObligationProverTask right) - && preparedObligationSelectedPremises left - == preparedObligationSelectedPremises right |