diff options
Diffstat (limited to 'source/Checking/Declaration.hs')
| -rw-r--r-- | source/Checking/Declaration.hs | 982 |
1 files changed, 915 insertions, 67 deletions
diff --git a/source/Checking/Declaration.hs b/source/Checking/Declaration.hs index 53e3e02..15c8282 100644 --- a/source/Checking/Declaration.hs +++ b/source/Checking/Declaration.hs @@ -17,17 +17,27 @@ module Checking.Declaration , importSealedModuleDriver , nextDeclarationSlotDriver , currentTheoryDriver + , currentFoundationAxiomDriver , resolveVisibleFactAliasDriver , resolveVisibleFactTargetsDriver , resolveVisibleGlobalDriver , resolveVisibleGlobalContentDriver + , ResolvedStructure + , resolvedStructureDescriptor + , resolvedStructurePredicate + , resolvedStructureOperation + , resolvedStructureOperations + , resolveVisibleStructureDriver + , resolveVisibleStructureOperationObjectsDriver , objectAvailableDriver + , objectTypeDriver , runModuleDriver , ValidationLookup , validationLookup , ValidationRun(..) , failModuleDriver , VampireResolver + , vampireBatchResolver , vampireResolver , Declaration , failDeclaration @@ -35,6 +45,7 @@ module Checking.Declaration , addDeclarationProposition , resolveVisibleGlobal , stageSemanticGlobalBinding + , stageSemanticStructureDescriptor , CandidateSpec , candidateSpec , ReservedCandidate @@ -43,6 +54,7 @@ module Checking.Declaration , reservePropositionCandidate , reserveFrozenPropositionCandidateBatch , reserveDefinitionEquationCandidate + , reservePointwiseDefinitionEquationCandidate , reserveDefinitionEquationCandidateBatch , reservedCandidateSlot , reservedCandidateStage @@ -66,7 +78,10 @@ module Checking.Declaration , authorizeDefinitionEquationCandidate , acceptVampireObligation , acceptPreparedVampireObligation + , acceptCurrentCandidateVampire + , prepareCurrentCandidateVampire , authorizeVampireCandidate + , authorizeVampireCandidateBatch , authorizeSourceAxiomCandidate , authorizeOmittedCandidate , authorizeDatatypeCompilationCandidates @@ -110,6 +125,7 @@ import Felix.Cache.Codec (encodeCache) import Felix.Module import Provers qualified import Report.Location +import Syntax.Abstract (StructSymbol) import Control.Exception qualified as Exception import Control.DeepSeq (deepseq) @@ -123,7 +139,7 @@ import Data.ByteString qualified as ByteString import Data.List qualified as List import Data.List.NonEmpty qualified as NonEmpty import Data.Map.Strict qualified as Map -import Data.Maybe (catMaybes) +import Data.Maybe (catMaybes, mapMaybe) import Data.Set qualified as Set import Data.Text qualified as Text import Data.Unique (Unique, newUnique) @@ -205,6 +221,8 @@ data LogicalBuilder = LogicalBuilder :: !(Map SemanticName ImportedAliasBinding) , logicalBuilderGlobals :: !(Map SemanticGlobalKey SemanticGlobalTarget) + , logicalBuilderStructures + :: !(Map SemanticStructurePhrase ResolvedStructure) , logicalBuilderImportedInterfaces :: !(Set SemanticInterfaceId) , logicalBuilderDeltas :: ![DeclarationInterfaceDelta] , logicalBuilderNextDeclaration :: !Natural @@ -212,6 +230,55 @@ data LogicalBuilder = LogicalBuilder , logicalBuilderNextInvocation :: !Natural } +data ResolvedStructureOperation = ResolvedStructureOperation + !ObjectId + !SemanticStructurePhrase + deriving stock (Show, Eq) + +data ResolvedStructure = ResolvedStructure + !SemanticStructureDescriptor + !(Set SemanticStructurePhrase) + !(Map StructSymbol ResolvedStructureOperation) + deriving stock (Show, Eq) + +resolvedStructureDescriptor + :: ResolvedStructure + -> SemanticStructureDescriptor +resolvedStructureDescriptor (ResolvedStructure descriptor _ _) = + descriptor + +resolvedStructurePredicate :: ResolvedStructure -> Maybe ObjectId +resolvedStructurePredicate = + semanticStructureDescriptorPredicate . resolvedStructureDescriptor + +resolvedStructureOperation + :: StructSymbol + -> ResolvedStructure + -> Maybe ObjectId +resolvedStructureOperation symbol (ResolvedStructure _ _ operations) = + operationObject <$> Map.lookup symbol operations + where + operationObject (ResolvedStructureOperation object _origin) = object + +resolvedStructureOperations + :: ResolvedStructure + -> Map StructSymbol ObjectId +resolvedStructureOperations (ResolvedStructure _ _ operations) = + operationObject <$> operations + where + operationObject (ResolvedStructureOperation object _origin) = object + +structureOperationBindings + :: Map SemanticStructurePhrase ResolvedStructure + -> Set (StructSymbol, ObjectId) +structureOperationBindings structures = + Set.fromList + [ (symbol, object) + | structure <- Map.elems structures + , (symbol, object) <- + Map.toAscList (resolvedStructureOperations structure) + ] + data CommittedDeclarationBatch = CommittedDeclarationBatch !ModuleName @@ -370,18 +437,37 @@ forceCommittedBatch newtype VampireResolver = VampireResolver - { resolveVampire + { resolveVampireBatch :: forall local origin. - Provers.PreparedTypedProverTask + NonEmpty + (Provers.PreparedTypedProverTask + SemanticFactOccurrenceFingerprint + local + origin + ObjectId) + -> IO + (NonEmpty + (Either + Provers.ProverProcessError + Provers.ProverAnswer)) + } + +vampireBatchResolver + :: (forall local origin. + NonEmpty + (Provers.PreparedTypedProverTask SemanticFactOccurrenceFingerprint local origin - ObjectId - -> IO + ObjectId) + -> IO + (NonEmpty (Either Provers.ProverProcessError - Provers.ProverAnswer) - } + Provers.ProverAnswer))) + -> VampireResolver +vampireBatchResolver = + VampireResolver vampireResolver :: (forall local origin. @@ -395,8 +481,39 @@ vampireResolver Provers.ProverProcessError Provers.ProverAnswer)) -> VampireResolver -vampireResolver = - VampireResolver +vampireResolver resolve = + vampireBatchResolver (traverse resolve) + +resolveOneVampire + :: VampireResolver + -> Provers.PreparedTypedProverTask + SemanticFactOccurrenceFingerprint + local + origin + ObjectId + -> ExceptT DeclarationError IO + (Either + Provers.ProverProcessError + Provers.ProverAnswer) +resolveOneVampire resolver prepared = do + results@(result :| _) <- + liftIO (resolveVampireBatch resolver (prepared :| [])) + void + (Except.liftEither + (validateVampireResolverResultCount 1 results)) + pure result + +validateVampireResolverResultCount + :: Int + -> NonEmpty value + -> Either DeclarationError [value] +validateVampireResolverResultCount expected results + | expected == actual = + Right (NonEmpty.toList results) + | otherwise = + Left (VampireResolverBatchSizeMismatch expected actual) + where + actual = NonEmpty.length results data DriverState = DriverState !VampireResolver @@ -595,8 +712,11 @@ validateEvidenceInventory -> ImportedModuleEvidence -> Either DeclarationError () validateEvidenceInventory theory closure evidence = - void (foldEvidence Set.empty Map.empty Map.empty evidence) - *> void (foldGlobals Set.empty Map.empty evidence) + do + void (foldEvidence Set.empty Map.empty Map.empty evidence) + (_seen, structures) <- + foldStructures Set.empty Map.empty evidence + void (foldGlobals structures Set.empty Map.empty evidence) where foldEvidence seen facts aliases current | identity `Set.member` seen = @@ -678,19 +798,20 @@ validateEvidenceInventory theory closure evidence = (ImportedAliasCollision name existingOrigin origin) - foldGlobals seen globals current + foldGlobals structures seen globals current | identity `Set.member` seen = Right (seen, globals) | otherwise = do (parentsSeen, parentGlobals) <- foldM (\(seen', globals') parent -> - foldGlobals seen' globals' parent) + foldGlobals structures seen' globals' parent) (seen, globals) parents globals' <- foldM - (insertGlobal current) + (insertGlobal + (structureOperationBindings structures)) parentGlobals [ binding | delta <- semanticInterfaceDeclarations interface @@ -702,13 +823,15 @@ validateEvidenceInventory theory closure evidence = ImportedModuleEvidence interface parents _entries _objects = current identity = semanticInterfaceAssertedId interface - insertGlobal _current globals binding = do + insertGlobal operationBindings globals binding = do let key = semanticGlobalBindingKey binding target = semanticGlobalBindingTarget binding _ <- first (ImportedGlobalTargetInvalid key target) - (validateSemanticGlobalBindingTarget closure binding) + (validateSemanticGlobalBindingTarget + operationBindings + closure binding) case Map.lookup key globals of Nothing -> Right (Map.insert key target globals) Just existing @@ -716,6 +839,30 @@ validateEvidenceInventory theory closure evidence = | otherwise -> Left (ImportedGlobalCollision key existing target) + foldStructures seen structures current + | identity `Set.member` seen = + Right (seen, structures) + | otherwise = do + (parentsSeen, parentStructures) <- + foldM + (\(seen', structures') parent -> + foldStructures seen' structures' parent) + (seen, structures) + parents + structures' <- + foldM + (insertSemanticStructure closure) + parentStructures + [ descriptor + | delta <- semanticInterfaceDeclarations interface + , descriptor <- semanticEnvironmentStructures + (declarationDeltaEnvironment delta) + ] + pure (Set.insert identity parentsSeen, structures') + where + ImportedModuleEvidence interface parents _entries _objects = current + identity = semanticInterfaceAssertedId interface + evidenceInterface :: ImportedModuleEvidence -> SemanticInterface evidenceInterface (ImportedModuleEvidence interface _parents _entries _objects) = @@ -782,6 +929,7 @@ runModuleDriver , logicalBuilderFacts = Map.empty , logicalBuilderAliases = Map.empty , logicalBuilderGlobals = Map.empty + , logicalBuilderStructures = Map.empty , logicalBuilderImportedInterfaces = Set.empty , logicalBuilderDeltas = [] , logicalBuilderNextDeclaration = 0 @@ -848,6 +996,17 @@ currentTheoryDriver = (\(DriverState _resolver builder _prefix _validation) -> logicalBuilderTheory builder)) +currentFoundationAxiomDriver + :: FoundationAxiomTag + -> ModuleDriver failure (FrozenCheckedCore Void) +currentFoundationAxiomDriver tag = + ModuleDriver + (State.gets + (\(DriverState _resolver builder _prefix _validation) -> + foundationAxiomFrozen + (logicalBuilderFoundation builder) + tag)) + resolveVisibleFactAliasDriver :: SemanticName -> ModuleDriver failure @@ -878,8 +1037,12 @@ resolveVisibleGlobalDriver resolveVisibleGlobalDriver key = ModuleDriver do DriverState _resolver builder _prefix _validation <- State.get pure - ( (\(target, content, _dependencies) -> - (target, objectContentType content)) + ( (\(target, _content, _dependencies) -> + ( target + , fromMaybe + (impossible "visible semantic key has no source type") + (semanticGlobalKeyType key) + )) <$> resolveVisibleGlobalContent builder key ) @@ -895,6 +1058,26 @@ resolveVisibleGlobalContentDriver key = ModuleDriver do DriverState _resolver builder _prefix _validation <- State.get pure (resolveVisibleGlobalContent builder key) +resolveVisibleStructureDriver + :: SemanticStructurePhrase + -> ModuleDriver failure (Maybe ResolvedStructure) +resolveVisibleStructureDriver structurePhrase = ModuleDriver do + DriverState _resolver builder _prefix _validation <- State.get + pure (Map.lookup structurePhrase (logicalBuilderStructures builder)) + +resolveVisibleStructureOperationObjectsDriver + :: StructSymbol + -> ModuleDriver failure [ObjectId] +resolveVisibleStructureOperationObjectsDriver symbol = ModuleDriver do + DriverState _resolver builder _prefix _validation <- State.get + pure + ( Set.toAscList + (Set.fromList + (mapMaybe + (resolvedStructureOperation symbol) + (Map.elems (logicalBuilderStructures builder)))) + ) + resolveVisibleGlobalContent :: LogicalBuilder -> SemanticGlobalKey @@ -943,6 +1126,17 @@ objectAvailableDriver identity = identity (logicalBuilderObjectClosure builder)))) +objectTypeDriver + :: ObjectId + -> ModuleDriver failure (Maybe CoreType) +objectTypeDriver identity = + ModuleDriver + (State.gets + (\(DriverState _resolver builder _prefix _validation) -> + lookupCheckedObjectType + identity + (logicalBuilderObjectClosure builder))) + data CandidateSpec = CandidateSpec !CheckedPropositionContent @@ -1023,6 +1217,8 @@ data DeclarationState = DeclarationState :: ![CheckedPropositionContent] , declarationGlobalBindingsReversed :: ![SemanticGlobalBinding] + , declarationStructureDescriptorsReversed + :: ![SemanticStructureDescriptor] , declarationReservations :: !(Map FactSlot ReservedCandidate) , declarationPending :: !(Map FactSlot PendingCandidate) @@ -1084,10 +1280,7 @@ resolveVisibleGlobal key = Declaration do let builder = declarationBuilder state pure do target <- Map.lookup key (logicalBuilderGlobals builder) - coreType <- - lookupCheckedObjectType - (semanticGlobalTargetObject target) - (logicalBuilderObjectClosure builder) + coreType <- semanticGlobalKeyType key pure (target, coreType) stageSemanticGlobalBinding @@ -1116,6 +1309,32 @@ stageSemanticGlobalBinding key target = Declaration do : declarationGlobalBindingsReversed state } +stageSemanticStructureDescriptor + :: SemanticStructureDescriptor + -> Declaration () +stageSemanticStructureDescriptor descriptor = Declaration do + state <- State.get + case declarationValidationSelection state of + DeclarationValidationUnselected -> pure () + _ -> + State.lift + (Except.throwError + DeclarationShapeChangedAfterValidationLookup) + let structurePhrase = semanticStructureDescriptorPhrase descriptor + when + (any + ((== structurePhrase) . semanticStructureDescriptorPhrase) + (declarationStructureDescriptorsReversed state)) + (State.lift + (Except.throwError + (DeclarationStructureAlreadyStaged structurePhrase))) + State.put + state + { declarationStructureDescriptorsReversed = + descriptor + : declarationStructureDescriptorsReversed state + } + reserveCandidate :: CandidateSpec -> Declaration ReservedCandidate @@ -1307,6 +1526,55 @@ reserveDefinitionEquationCandidate identity alias = Declaration do SearchEligible [alias])) +-- | Construct the pointwise presentation of one unary transparent predicate +-- definition. The candidate remains tied to the object's checked content. +reservePointwiseDefinitionEquationCandidate + :: ObjectId + -> SemanticName + -> Declaration ReservedCandidate +reservePointwiseDefinitionEquationCandidate identity alias = Declaration do + unprepared <- State.get + prepared <- + State.lift + (Except.liftEither + (prepareDeclarationClosure unprepared)) + content <- + maybe + (State.lift + (Except.throwError + (DefinitionEquationObjectMissing identity))) + pure + (lookupCheckedObjectContent + identity + (fromMaybe + (impossible "prepared predicate closure is absent") + (declarationObjectClosure prepared))) + body <- + case content of + TransparentObjectContent _theory + (TyArrow TySet TyProp) (CLam TySet predicate) -> + pure predicate + _ -> + State.lift + (Except.throwError + (DefinitionEquationObjectNotPointwisePredicate identity)) + proposition <- + State.lift + (Except.liftEither + (first DeclarationPropositionValidationFailed + (validatePropositionContent + (fromMaybe + (impossible "prepared predicate closure is absent") + (declarationObjectClosure prepared)) + (CForall TySet + (CEq TyProp + (CApp (CGlobal identity) (CBound 0)) + body))))) + State.put prepared + runDeclaration + (reserveCandidate + (candidateSpec proposition SearchEligible [alias])) + -- | Reserve one defining equation and a nonempty generated-fact batch at the -- same declaration stage. No candidate in the batch can cite a sibling. reserveDefinitionEquationCandidateBatch @@ -2016,8 +2284,16 @@ foldImportedEvidence evidence builder | delta <- semanticInterfaceDeclarations interface , alias <- declarationDeltaAliases delta ] + importedStructures <- foldM + (insertSemanticStructure objectClosure) + (logicalBuilderStructures withParents) + [ descriptor + | delta <- semanticInterfaceDeclarations interface + , descriptor <- semanticEnvironmentStructures + (declarationDeltaEnvironment delta) + ] importedGlobals <- foldM - (insertImportedGlobal objectClosure) + (insertImportedGlobal objectClosure importedStructures) (logicalBuilderGlobals withParents) [ binding | delta <- semanticInterfaceDeclarations interface @@ -2029,6 +2305,7 @@ foldImportedEvidence evidence builder { logicalBuilderFacts = importedFacts , logicalBuilderAliases = importedAliases , logicalBuilderGlobals = importedGlobals + , logicalBuilderStructures = importedStructures , logicalBuilderObjectClosure = objectClosure , logicalBuilderImportedInterfaces = Set.insert @@ -2098,13 +2375,15 @@ foldImportedEvidence evidence builder (ImportedAliasCollision name existingOrigin origin) - insertImportedGlobal closure globals binding = do + insertImportedGlobal closure structures globals binding = do let key = semanticGlobalBindingKey binding target = semanticGlobalBindingTarget binding _ <- first (ImportedGlobalTargetInvalid key target) - (validateSemanticGlobalBindingTarget closure binding) + (validateSemanticGlobalBindingTarget + (structureOperationBindings structures) + closure binding) case Map.lookup key globals of Nothing -> pure (Map.insert key target globals) Just existing @@ -2112,6 +2391,109 @@ foldImportedEvidence evidence builder | otherwise -> Left (ImportedGlobalCollision key existing target) +insertSemanticStructure + :: CheckedObjectClosure + -> Map SemanticStructurePhrase ResolvedStructure + -> SemanticStructureDescriptor + -> Either + DeclarationError + (Map SemanticStructurePhrase ResolvedStructure) +insertSemanticStructure closure structures descriptor = do + validateSemanticStructureTargets closure descriptor + let structurePhrase = semanticStructureDescriptorPhrase descriptor + case Map.lookup structurePhrase structures of + Just (ResolvedStructure existing _ _) + | existing == descriptor -> Right structures + | otherwise -> + Left + (ImportedStructureCollision + structurePhrase existing descriptor) + Nothing -> do + parents <- traverse resolveParent + (semanticStructureDescriptorParents descriptor) + inherited <- foldM mergeParentOperations Map.empty parents + complete <- foldM insertOwnOperation inherited + (semanticStructureDescriptorOperations descriptor) + let ancestors = + Set.unions + [ Set.insert + (semanticStructureDescriptorPhrase + (resolvedStructureDescriptor parent)) + parentAncestors + | parent@(ResolvedStructure _ parentAncestors _) <- parents + ] + resolved = ResolvedStructure descriptor ancestors complete + Right (Map.insert structurePhrase resolved structures) + where + resolveParent parentPhrase = + maybe + (Left + (SemanticStructureParentMissing + (semanticStructureDescriptorPhrase descriptor) + parentPhrase)) + Right + (Map.lookup parentPhrase structures) + + mergeParentOperations operations + (ResolvedStructure _descriptor _ancestors parentOperations) = + foldM insertInheritedOperation operations + (Map.toAscList parentOperations) + + insertInheritedOperation operations (symbol, operation) = + insertResolvedOperation symbol operation operations + + insertOwnOperation operations operation = + insertResolvedOperation + (semanticStructureOperationSymbol operation) + (ResolvedStructureOperation + (semanticStructureOperationObject operation) + (semanticStructureDescriptorPhrase descriptor)) + operations + + insertResolvedOperation symbol incoming operations = + case Map.lookup symbol operations of + Nothing -> Right (Map.insert symbol incoming operations) + Just (ResolvedStructureOperation existingObject existingOrigin) -> + case incoming of + ResolvedStructureOperation incomingObject incomingOrigin + | existingObject == incomingObject -> Right operations + | otherwise -> + Left + (SemanticStructureOperationConflict + symbol existingOrigin incomingOrigin) + +validateSemanticStructureTargets + :: CheckedObjectClosure + -> SemanticStructureDescriptor + -> Either DeclarationError () +validateSemanticStructureTargets closure descriptor = do + traverse_ validatePredicate + (semanticStructureDescriptorPredicate descriptor) + traverse_ validateOperation + (semanticStructureDescriptorOperations descriptor) + where + validatePredicate object = + validateObjectType + (SemanticStructurePredicateTargetInvalid + (semanticStructureDescriptorPhrase descriptor)) + object + (TyArrow TySet TyProp) + + validateOperation operation = + validateObjectType + (SemanticStructureOperationTargetInvalid + (semanticStructureDescriptorPhrase descriptor) + (semanticStructureOperationSymbol operation)) + (semanticStructureOperationObject operation) + (TyArrow TySet TySet) + + validateObjectType failure object expected = + case lookupCheckedObjectType object closure of + Nothing -> Left (failure object Nothing expected) + Just actual + | actual == expected -> Right () + | otherwise -> Left (failure object (Just actual) expected) + equivalentAuthorizedFact :: AuthorizedFact -> AuthorizedFact -> Bool equivalentAuthorizedFact (AuthorizedFact leftProposition leftOccurrence @@ -2435,6 +2817,75 @@ acceptPreparedVampireObligation (validatePreparedVampireProblem expected prepared) prepared +-- | Prepare and execute the current closed candidate using exactly the +-- staged premises already consumed by its trusted declaration compiler. +acceptCurrentCandidateVampire :: CandidateProof () +acceptCurrentCandidateVampire = + prepareCurrentCandidateVampire + >>= acceptPreparedVampireObligation + +-- | Prepare the current closed candidate without executing its request. The +-- declaration-owned batch authorizer uses this seam only after all strictly +-- earlier staged premises have been consumed. +prepareCurrentCandidateVampire + :: CandidateProof (PreparedVampireObligation Void ()) +prepareCurrentCandidateVampire = CandidateProof do + initial <- State.get + let builder = candidateProofBuilder initial + closure = candidateProofObjectClosure initial + globalType = (`lookupCheckedObjectType` closure) + target = candidateCheckedProposition + (candidateProofCandidate initial) + premises = reverse (candidateProofPremisesReversed initial) + closed proposition = + embedClosedCore [] + (checkedPropositionTerm proposition) + supportedTarget <- + State.lift + (Except.liftEither + (first + (CurrentCandidateVampirePreparationFailed + . VampireObligationClaimProjectionFailed) + (Backend.projectSupportedProposition + globalType + (Vector.empty :: Vector (Void, CoreType)) + (closed target)))) + locals <- + State.lift + (Except.liftEither + (first CurrentCandidateVampirePreparationFailed + (traverse + (prepareLocal globalType) + (zip [0 :: Natural ..] premises)))) + prepared <- + State.lift + (Except.liftEither + (first CurrentCandidateVampirePreparationFailed + (prepareVampireObligationWith + Provers.DirectTask + builder + closure + supportedTarget + locals + [] + VampireLocalPremises))) + pure prepared + where + prepareLocal globalType (index, CandidatePremise proposition) = do + let ordinal = Backend.localPremiseOrdinal index + supported <- + first + (VampireObligationLocalProjectionFailed ordinal) + (Backend.projectSupportedProposition + globalType + (Vector.empty :: Vector (Void, CoreType)) + (embedClosedCore [] + (checkedPropositionTerm proposition))) + first + (VampireObligationLocalClassificationFailed ordinal) + (Backend.typedLocalPremise + globalType ordinal () supported) + acceptValidatedVampireTask :: (CandidateProofState -> ExceptT DeclarationError IO CandidateProofState) @@ -2447,39 +2898,20 @@ acceptValidatedVampireTask acceptValidatedVampireTask validate prepared = CandidateProof do initial <- State.get validated <- State.lift (validate initial) - let request = Provers.preparedTypedProverRequest prepared - case candidateProofCachedValidation initial of - Nothing -> do - let resolver = - declarationVampireResolver - (candidateProofDeclaration initial) - result <- liftIO (resolveVampire resolver prepared) - accepted <- - case result of - Left err -> - State.lift - (Except.throwError - (VampireProcessFailed err)) - Right answer -> - maybe - (State.lift - (Except.throwError - (VampireObligationRejected answer))) - pure - (Provers.provedVampireRun answer) - unless - (Provers.acceptedVampireRequest accepted == request) - (State.lift - (Except.throwError VampireRequestMismatch)) - Just _validation -> - pure () - let requestId = Provers.preparedVerificationRequestId request - State.put - validated - { candidateProofAcceptedRequestsReversed = - requestId - : candidateProofAcceptedRequestsReversed validated - } + result <- + case candidateProofCachedValidation initial of + Nothing -> do + let resolver = + declarationVampireResolver + (candidateProofDeclaration initial) + Just <$> State.lift (resolveOneVampire resolver prepared) + Just _validation -> + pure Nothing + final <- + State.lift + (acceptVampireBatchMemberResult + prepared result validated) + State.put final -- | Complete one checked source candidate after all of its obligations have -- been accepted in source order. The enclosing proof declaration owns the @@ -2509,6 +2941,333 @@ authorizeVampireCandidate candidate proof = (candidateProofSafety final) final +data PreparedVampireCandidateBatchMember = + PreparedVampireCandidateBatchMember + !Location + !ReservedCandidate + !(Provers.PreparedTypedProverTask + SemanticFactOccurrenceFingerprint + Void + () + ObjectId) + !CandidateProofState + +data ResolvedVampireCandidateBatchMember = + ResolvedVampireCandidateBatchMember + !PreparedVampireCandidateBatchMember + !(Maybe + (Either + Provers.ProverProcessError + Provers.ProverAnswer)) + +-- | Authorize one complete, source-ordered candidate stage whose members are +-- mutually independent and each require exactly one closed Vampire request. +-- Every member is prepared and validated against the same declaration +-- baseline. Results are applied only after the complete live batch returns, +-- so no same-stage sibling can become authority for another member. +authorizeVampireCandidateBatch + :: NonEmpty + ( Location + , ReservedCandidate + , CandidateProof (PreparedVampireObligation Void ()) + ) + -> Declaration () +authorizeVampireCandidateBatch inputs = Declaration do + unprepared <- State.get + baseline <- + State.lift + (Except.liftEither + (prepareDeclarationClosure unprepared)) + let supplied = + [ candidate + | (_location, candidate, _prepare) <- NonEmpty.toList inputs + ] + frontier = declarationAuthorizationFrontier baseline + expected = + List.filter + ((== CandidateStage frontier) . reservedStage) + (Map.elems (declarationReservations baseline)) + traverse_ + (State.lift + . Except.liftEither + . validateReservedCandidate baseline) + supplied + traverse_ + (\candidate -> + when + (Map.member + (reservedCandidateSlot candidate) + (declarationPending baseline)) + (State.lift + (Except.throwError + (CandidateAlreadyAuthorized + (reservedCandidateSlot candidate))))) + supplied + unless (supplied == expected) + (State.lift + (Except.throwError + (VampireCandidateBatchMismatch + (reservedCandidateSlot <$> expected) + (reservedCandidateSlot <$> supplied)))) + prepared <- + State.lift + (traverse + (prepareVampireCandidateBatchMember baseline) + inputs) + State.lift + (validateCachedVampireCandidateBatch + (NonEmpty.toList prepared)) + let live = + [ task + | PreparedVampireCandidateBatchMember + _location _candidate task final <- + NonEmpty.toList prepared + , isNothing (candidateProofCachedValidation final) + ] + liveResults <- + case NonEmpty.nonEmpty live of + Nothing -> pure [] + Just nonempty -> do + let resolver = + declarationVampireResolver baseline + results <- liftIO (resolveVampireBatch resolver nonempty) + State.lift + (Except.liftEither + (validateVampireResolverResultCount + (length live) + results)) + pending <- + State.lift + (completeVampireCandidateBatch + (NonEmpty.toList prepared) + liveResults) + let withPending = + baseline + { declarationPending = + foldl' + (\entries item@(PendingCandidate candidate _ _) -> + Map.insert + (reservedCandidateSlot + candidate) + item + entries) + (declarationPending baseline) + pending + } + State.put (advanceAuthorizationFrontier withPending) + +prepareVampireCandidateBatchMember + :: DeclarationState + -> ( Location + , ReservedCandidate + , CandidateProof (PreparedVampireObligation Void ()) + ) + -> ExceptT DeclarationError IO PreparedVampireCandidateBatchMember +prepareVampireCandidateBatchMember + baseline (location, candidate, prepare) = do + initial <- + Except.liftEither + (initialCandidateProofState baseline candidate) + cached <- selectProofCandidateValidation candidate initial + let selected = + initial{candidateProofCachedValidation = cached} + (obligation, preparedState) <- + State.runStateT + (runCandidateProof + (locateProofObligation location prepare)) + selected + unless (null (acceptedRequestIds preparedState)) + (Except.throwError + (VampireCandidateBatchProofShapeMismatch + (reservedCandidateSlot candidate))) + let PreparedVampireObligation expected task = obligation + validated <- + Except.withExceptT + (ProofObligationFailedAt location) + (validatePreparedVampireProblem + expected task preparedState) + pure + (PreparedVampireCandidateBatchMember + location candidate task validated) + +completeVampireCandidateBatch + :: [PreparedVampireCandidateBatchMember] + -> [Either Provers.ProverProcessError Provers.ProverAnswer] + -> ExceptT DeclarationError IO [PendingCandidate] +completeVampireCandidateBatch members liveResults = do + resolved <- + Except.liftEither + (associateVampireCandidateBatchResults + members liveResults) + -- Integrity dominates ranked proof failure: validate every accepted run + -- before inspecting any ordinary process or prover rejection. + traverse_ validateAcceptedVampireBatchMember resolved + traverse_ rejectOrdinaryVampireBatchMember resolved + traverse completeVampireCandidateBatchMember resolved + +validateCachedVampireCandidateBatch + :: [PreparedVampireCandidateBatchMember] + -> ExceptT DeclarationError IO () +validateCachedVampireCandidateBatch = + traverse_ \member -> + when + (preparedVampireCandidateBatchMemberIsCached member) + (void + (completeVampireCandidateBatchMember + (ResolvedVampireCandidateBatchMember member Nothing))) + +associateVampireCandidateBatchResults + :: [PreparedVampireCandidateBatchMember] + -> [Either Provers.ProverProcessError Provers.ProverAnswer] + -> Either + DeclarationError + [ResolvedVampireCandidateBatchMember] +associateVampireCandidateBatchResults members = + go members + where + go [] [] = Right [] + go [] results = + Left + (VampireResolverBatchSizeMismatch + 0 + (length results)) + go (member : remaining) results + | preparedVampireCandidateBatchMemberIsCached member = + (ResolvedVampireCandidateBatchMember member Nothing :) + <$> go remaining results + | otherwise = + case results of + [] -> + Left (VampireResolverBatchSizeMismatch 1 0) + current : later -> + (ResolvedVampireCandidateBatchMember + member (Just current) :) + <$> go remaining later + +preparedVampireCandidateBatchMemberIsCached + :: PreparedVampireCandidateBatchMember + -> Bool +preparedVampireCandidateBatchMemberIsCached + (PreparedVampireCandidateBatchMember + _location _candidate _task state) = + isJust (candidateProofCachedValidation state) + +validateAcceptedVampireBatchMember + :: ResolvedVampireCandidateBatchMember + -> ExceptT DeclarationError IO () +validateAcceptedVampireBatchMember + (ResolvedVampireCandidateBatchMember + (PreparedVampireCandidateBatchMember + location _candidate task _validated) + result) = + Except.withExceptT + (ProofObligationFailedAt location) + (validateAcceptedVampireResult task result) + +rejectOrdinaryVampireBatchMember + :: ResolvedVampireCandidateBatchMember + -> ExceptT DeclarationError IO () +rejectOrdinaryVampireBatchMember + (ResolvedVampireCandidateBatchMember + (PreparedVampireCandidateBatchMember + location _candidate _task _validated) + result) = + traverse_ + (Except.throwError . ProofObligationFailedAt location) + (result >>= vampireResultFailure) + +completeVampireCandidateBatchMember + :: ResolvedVampireCandidateBatchMember + -> ExceptT DeclarationError IO PendingCandidate +completeVampireCandidateBatchMember + (ResolvedVampireCandidateBatchMember + (PreparedVampireCandidateBatchMember + location candidate task validated) + result) = do + final <- + Except.withExceptT + (ProofObligationFailedAt location) + (applyAcceptedVampireResult task result validated) + completeCandidateWithValidation + candidate + (CheckedSourceProof (acceptedRequestIds final)) + (candidateProofSafety final) + final + +acceptVampireBatchMemberResult + :: Provers.PreparedTypedProverTask + SemanticFactOccurrenceFingerprint + local + origin + ObjectId + -> Maybe (Either Provers.ProverProcessError Provers.ProverAnswer) + -> CandidateProofState + -> ExceptT DeclarationError IO CandidateProofState +acceptVampireBatchMemberResult prepared result validated = do + validateAcceptedVampireResult prepared result + traverse_ Except.throwError (result >>= vampireResultFailure) + applyAcceptedVampireResult prepared result validated + +validateAcceptedVampireResult + :: Provers.PreparedTypedProverTask + SemanticFactOccurrenceFingerprint + local + origin + ObjectId + -> Maybe (Either Provers.ProverProcessError Provers.ProverAnswer) + -> ExceptT DeclarationError IO () +validateAcceptedVampireResult prepared result = do + let request = Provers.preparedTypedProverRequest prepared + traverse_ + (\resolved -> + traverse_ + (\accepted -> + unless + (Provers.acceptedVampireRequest accepted == request) + (Except.throwError VampireRequestMismatch)) + (either (const Nothing) Provers.provedVampireRun resolved)) + result + +vampireResultFailure + :: Either Provers.ProverProcessError Provers.ProverAnswer + -> Maybe DeclarationError +vampireResultFailure = \case + Left failure -> + Just (VampireProcessFailed failure) + Right answer -> + case Provers.provedVampireRun answer of + Nothing -> + Just (VampireObligationRejected answer) + Just _accepted -> + Nothing + +applyAcceptedVampireResult + :: Provers.PreparedTypedProverTask + SemanticFactOccurrenceFingerprint + local + origin + ObjectId + -> Maybe (Either Provers.ProverProcessError Provers.ProverAnswer) + -> CandidateProofState + -> ExceptT DeclarationError IO CandidateProofState +applyAcceptedVampireResult prepared result validated = do + traverse_ + (\resolved -> + case vampireResultFailure resolved of + Just failure -> + Except.throwError failure + Nothing -> + pure ()) + result + let request = Provers.preparedTypedProverRequest prepared + requestId = Provers.preparedVerificationRequestId request + pure + validated + { candidateProofAcceptedRequestsReversed = + requestId + : candidateProofAcceptedRequestsReversed validated + } + selectProofCandidateValidation :: ReservedCandidate -> CandidateProofState @@ -2989,15 +3748,27 @@ matchesDefinitionEquation identity proposition proofState = contentTheory == logicalBuilderTheory (candidateProofBuilder proofState) - && frozenCoreTerm - (checkedPropositionTerm proposition) - == CEq - coreType - (CGlobal identity) - body + && frozenCoreTerm (checkedPropositionTerm proposition) + `elem` definitionEquationTargets identity coreType body _ -> False +definitionEquationTargets + :: ObjectId + -> CoreType + -> CanonicalTerm ObjectId + -> [CanonicalTerm ObjectId] +definitionEquationTargets identity coreType body = + CEq coreType (CGlobal identity) body + : case (coreType, body) of + (TyArrow TySet TyProp, CLam TySet predicate) -> + [ CForall TySet + (CEq TyProp + (CApp (CGlobal identity) (CBound 0)) + predicate) + ] + _ -> [] + validateCandidateVampireProblem :: Provers.PreparedTypedProverTask @@ -3230,6 +4001,7 @@ initialDeclarationState resolver validationRun validationMode builder = , declarationObjectClosure = Nothing , declarationPropositionsReversed = [] , declarationGlobalBindingsReversed = [] + , declarationStructureDescriptorsReversed = [] , declarationReservations = Map.empty , declarationPending = Map.empty , declarationNextFact = logicalBuilderNextFact builder @@ -3284,17 +4056,37 @@ appendDeclaration mode declaration = do semanticGlobalBindingKey (reverse (declarationGlobalBindingsReversed declaration)) + descriptors = + List.sortOn + semanticStructureDescriptorPhrase + (reverse + (declarationStructureDescriptorsReversed declaration)) traverse_ (\binding -> first (DeclarationGlobalTargetInvalid (semanticGlobalBindingKey binding) (semanticGlobalBindingTarget binding)) - (validateSemanticGlobalBindingTarget closure binding)) + (validateSemanticGlobalBindingTarget + (structureOperationBindings + (logicalBuilderStructures builder)) + closure binding)) bindings + traverse_ + (\descriptor -> + let structurePhrase = semanticStructureDescriptorPhrase descriptor + in when + (Map.member structurePhrase + (logicalBuilderStructures builder)) + (Left (BuilderStructureCollision structurePhrase))) + descriptors + structures <- foldM + (insertSemanticStructure closure) + (logicalBuilderStructures builder) + descriptors environment <- first DeclarationEnvironmentFailed - (semanticEnvironmentDelta bindings) + (semanticEnvironmentWithStructures bindings descriptors) delta <- first DeclarationInterfaceFailed (declarationInterfaceDelta @@ -3313,6 +4105,7 @@ appendDeclaration mode declaration = do let builder' = appendBuilderState closure + structures delta next orderedPending @@ -3522,13 +4315,14 @@ validateBuilderCollisions builder delta = do appendBuilderState :: CheckedObjectClosure + -> Map SemanticStructurePhrase ResolvedStructure -> DeclarationInterfaceDelta -> PrefixContextId -> [PendingCandidate] -> LogicalBuilder -> DeclarationState -> LogicalBuilder -appendBuilderState closure delta next pending builder declaration = +appendBuilderState closure structures delta next pending builder declaration = builder { logicalBuilderPrefix = next , logicalBuilderObjectClosure = closure @@ -3560,6 +4354,7 @@ appendBuilderState closure delta next pending builder declaration = (logicalBuilderGlobals builder) (semanticEnvironmentBindings (declarationDeltaEnvironment delta)) + , logicalBuilderStructures = structures , logicalBuilderDeltas = delta : logicalBuilderDeltas builder , logicalBuilderNextDeclaration = @@ -3632,12 +4427,16 @@ data DeclarationError | KernelConstructionDescriptorMismatch | DefinitionEquationObjectMissing !ObjectId | DefinitionEquationObjectNotTransparent !ObjectId + | DefinitionEquationObjectNotPointwisePredicate !ObjectId | DefinitionEquationCandidateMismatch | DatatypeCompilationDescriptorMismatch | ProofObligationFailedAt !Location !DeclarationError | VampireProcessFailed !Provers.ProverProcessError | VampireObligationRejected !Provers.ProverAnswer | VampireProofHasNoAcceptedObligations + | VampireCandidateBatchMismatch ![FactSlot] ![FactSlot] + | VampireCandidateBatchProofShapeMismatch !FactSlot + | VampireResolverBatchSizeMismatch !Int !Int | OmittedProofDidNotRecordUse | VampireRequestMismatch | VampireTargetMismatch @@ -3648,6 +4447,8 @@ data DeclarationError | VampirePremiseCapabilityMismatch !SemanticFactOccurrenceFingerprint | VampireFoundationMismatch !FoundationAxiomTag + | CurrentCandidateVampirePreparationFailed + !(VampireObligationPreparationError Void) | ProofValidationOutsideProofDeclaration | DeclarationValidationOutsideCompiledDeclaration | DeclarationValidationAlreadySelected @@ -3669,6 +4470,18 @@ data DeclarationError !SemanticGlobalKey !SemanticGlobalTarget !SemanticGlobalTargetError + | ImportedStructureCollision + !SemanticStructurePhrase + !SemanticStructureDescriptor + !SemanticStructureDescriptor + | SemanticStructureParentMissing + !SemanticStructurePhrase !SemanticStructurePhrase + | SemanticStructureOperationConflict + !StructSymbol !SemanticStructurePhrase !SemanticStructurePhrase + | SemanticStructurePredicateTargetInvalid + !SemanticStructurePhrase !ObjectId !(Maybe CoreType) !CoreType + | SemanticStructureOperationTargetInvalid + !SemanticStructurePhrase !StructSymbol !ObjectId !(Maybe CoreType) !CoreType | ImportedEvidenceDirectMismatch ![SemanticInterfaceId] ![SemanticInterfaceId] | ImportedEvidenceInterfaceFailed !SemanticInterfaceError @@ -3682,6 +4495,7 @@ data DeclarationError | DeclarationInterfaceFailed !DeclarationInterfaceError | DeclarationEnvironmentFailed !SemanticEnvironmentError | DeclarationGlobalAlreadyStaged !SemanticGlobalKey + | DeclarationStructureAlreadyStaged !SemanticStructurePhrase | DeclarationGlobalTargetInvalid !SemanticGlobalKey !SemanticGlobalTarget @@ -3692,6 +4506,7 @@ data DeclarationError | BuilderAliasCollision !SemanticName | BuilderObjectCollision !ObjectId | BuilderGlobalCollision !SemanticGlobalKey !SemanticGlobalTarget + | BuilderStructureCollision !SemanticStructurePhrase deriving stock (Show, Eq) declarationErrorLocation :: DeclarationError -> Maybe Location @@ -3746,6 +4561,9 @@ renderDeclarationError = \case "definition equation references missing object " <> shown identity DefinitionEquationObjectNotTransparent identity -> "definition equation references non-transparent object " <> shown identity + DefinitionEquationObjectNotPointwisePredicate identity -> + "definition equation object " <> shown identity + <> " is not a unary predicate definition" DefinitionEquationCandidateMismatch -> "definition equation does not match its checked object content" DatatypeCompilationDescriptorMismatch -> @@ -3758,6 +4576,16 @@ renderDeclarationError = \case "Vampire did not accept a declaration obligation" VampireProofHasNoAcceptedObligations -> "Vampire proof contains no accepted obligations" + VampireCandidateBatchMismatch expected actual -> + "Vampire candidate batch does not match the complete authorization " + <> "stage (expected " <> shown expected + <> ", found " <> shown actual <> ")" + VampireCandidateBatchProofShapeMismatch slot -> + "Vampire candidate " <> shown slot + <> " performed execution before its ready batch" + VampireResolverBatchSizeMismatch expected actual -> + "Vampire resolver returned " <> shown actual + <> " results for " <> shown expected <> " requests" OmittedProofDidNotRecordUse -> "omitted proof completion did not record an omission" VampireRequestMismatch -> @@ -3774,6 +4602,8 @@ renderDeclarationError = \case "Vampire request lacks authority for premise " <> shown fingerprint VampireFoundationMismatch tag -> "Vampire request has inconsistent foundation axiom " <> shown tag + CurrentCandidateVampirePreparationFailed failure -> + "the staged Vampire obligation could not be prepared: " <> shown failure ProofValidationOutsideProofDeclaration -> "proof validation requires a proof declaration" DeclarationValidationOutsideCompiledDeclaration -> @@ -3808,6 +4638,20 @@ renderDeclarationError = \case ImportedEvidenceDirectMismatch expected actual -> "imported semantic parents differ: expected " <> shown expected <> ", found " <> shown actual + ImportedStructureCollision structurePhrase _existing _incoming -> + "structure " <> shown structurePhrase <> " has conflicting descriptors" + SemanticStructureParentMissing structurePhrase parent -> + "structure " <> shown structurePhrase <> " has unknown parent " <> shown parent + SemanticStructureOperationConflict symbol firstOrigin secondOrigin -> + "structure operation " <> shown symbol <> " conflicts between " + <> shown firstOrigin <> " and " <> shown secondOrigin + SemanticStructurePredicateTargetInvalid structurePhrase object _actual expected -> + "structure " <> shown structurePhrase <> " has invalid predicate object " + <> shown object <> " (expected " <> shown expected <> ")" + SemanticStructureOperationTargetInvalid structurePhrase symbol object _actual expected -> + "structure " <> shown structurePhrase <> " has invalid operation " + <> shown symbol <> " object " <> shown object + <> " (expected " <> shown expected <> ")" ImportedEvidenceInterfaceFailed{} -> "imported semantic interface failed validation" ImportedEvidenceObjectMissing identity -> @@ -3828,6 +4672,8 @@ renderDeclarationError = \case "declaration environment delta is inconsistent" DeclarationGlobalAlreadyStaged key -> "global " <> shown key <> " was staged more than once" + DeclarationStructureAlreadyStaged structurePhrase -> + "structure " <> shown structurePhrase <> " was staged more than once" DeclarationGlobalTargetInvalid key target _failure -> "global " <> shown key <> " has invalid target " <> shown target ProofDeclarationMustProduceOneFact -> @@ -3840,6 +4686,8 @@ renderDeclarationError = \case "object " <> shown object <> " is already registered" BuilderGlobalCollision key object -> "global " <> shown key <> " is already bound to " <> shown object + BuilderStructureCollision structurePhrase -> + "structure " <> shown structurePhrase <> " is already registered" where shown :: Show value => value -> Text shown = Text.pack . show |