diff options
Diffstat (limited to 'source/Checking')
| -rw-r--r-- | source/Checking/Backend/Connection.hs | 1088 | ||||
| -rw-r--r-- | source/Checking/Backend/Reconstruction.hs | 253 | ||||
| -rw-r--r-- | source/Checking/Core.hs | 217 | ||||
| -rw-r--r-- | source/Checking/Datatype.hs | 48 | ||||
| -rw-r--r-- | source/Checking/Declaration.hs | 982 | ||||
| -rw-r--r-- | source/Checking/Dependencies.hs | 189 | ||||
| -rw-r--r-- | source/Checking/Exact.hs | 1121 | ||||
| -rw-r--r-- | source/Checking/Exact/Global.hs | 10 | ||||
| -rw-r--r-- | source/Checking/Exact/Inductive.hs | 2 | ||||
| -rw-r--r-- | source/Checking/Exact/Proof.hs | 108 | ||||
| -rw-r--r-- | source/Checking/Facts.hs | 340 | ||||
| -rw-r--r-- | source/Checking/FinalPrelude.hs | 170 | ||||
| -rw-r--r-- | source/Checking/Legacy.hs | 1788 | ||||
| -rw-r--r-- | source/Checking/Legacy/Environment.hs | 279 | ||||
| -rw-r--r-- | source/Checking/Module.hs | 375 | ||||
| -rw-r--r-- | source/Checking/Obligation.hs | 428 | ||||
| -rw-r--r-- | source/Checking/Semantic.hs | 333 | ||||
| -rw-r--r-- | source/Checking/Structure.hs | 150 | ||||
| -rw-r--r-- | source/Checking/Transition.hs | 2584 | ||||
| -rw-r--r-- | source/Checking/Typed/Atomic.hs | 72 | ||||
| -rw-r--r-- | source/Checking/Typed/Reflexivity.hs | 105 |
21 files changed, 2995 insertions, 7647 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 diff --git a/source/Checking/Core.hs b/source/Checking/Core.hs index 6e8d175..4b7478f 100644 --- a/source/Checking/Core.hs +++ b/source/Checking/Core.hs @@ -49,6 +49,8 @@ module Checking.Core , weakenCheckedScopedCore , weakenScopedCore , scopedSetDefinition + , scopedCharacteristicDefinition + , scopedReplacementGraph , implyScopedCore , splitScopedSetEquality , scopedSetInductionHypothesis @@ -697,53 +699,194 @@ weakenScopedCore globalType binderType scoped = (shiftCanonical 1 0 (scopedCoreTerm scoped)) --- | Introduce a fresh set-valued local definition. Separation uses the --- checked characteristic rule so its local premise remains first-order. +-- | Introduce a fresh set-valued local definition. Separation specializes +-- the checked foundation characteristic so its local premise remains +-- first-order. scopedSetDefinition - :: ScopedCheckedCore global + :: Eq global + => FrozenCheckedCore Void + -> ScopedCheckedCore global -> Maybe (ScopedCheckedCore global) scopedSetDefinition - (ScopedCheckedCore context TySet expression) = - Just - (ScopedCheckedCore - (TySet : context) - TyProp - (case expression of - CApp - (CApp (CIntrinsic Sep) bound) - (CLam TySet predicate) -> - separationCharacteristic bound predicate - _ -> - CEq + characteristic + expression@(ScopedCheckedCore context TySet term) = + case term of + CApp + (CApp (CIntrinsic Sep) bound) + predicate@(CLam TySet _body) -> + scopedCharacteristicDefinition + characteristic + expression + ( ScopedCheckedCore context TySet bound + :| [ ScopedCheckedCore + context + (TySet `TyArrow` TyProp) + predicate + ] + ) + _ -> + Just + (ScopedCheckedCore + (TySet : context) + TyProp + (CEq TySet (CBound 0) - (shiftCanonical 1 0 expression))) - where - separationCharacteristic bound predicate = - CForall - TySet - (CEq - TyProp - (member (CBound 0) (CBound 1)) - (andP - (member - (CBound 0) - (shiftCanonical 2 0 bound)) - (shiftCanonical 1 1 predicate))) + (shiftCanonical 1 0 term))) +scopedSetDefinition _characteristic _expression = + Nothing - member element set = - CApp - (CApp (CIntrinsic Member) element) - set +-- | Specialize a checked characteristic and abstract its set-valued target +-- into one fresh nearest binder. Checked substitution and beta reduction +-- preserve the foundation row's proposition type. +scopedCharacteristicDefinition + :: Eq global + => FrozenCheckedCore Void + -> ScopedCheckedCore global + -> NonEmpty (ScopedCheckedCore global) + -> Maybe (ScopedCheckedCore global) +scopedCharacteristicDefinition + (FrozenCheckedCore TyProp frozen) + (ScopedCheckedCore context TySet target) + arguments + | all ((== context) . scopedCoreContext) arguments = do + specialized <- + specialize + (mapCanonicalGlobals absurd frozen) + (toList arguments) + let normalized = betaNormalizeCanonical specialized + (found, abstracted) = abstractTarget 0 normalized + guard found + pure + (ScopedCheckedCore + (TySet : context) + TyProp + abstracted) + where + specialize term [] = + Just term + specialize (CForall binderType body) + (ScopedCheckedCore _ argumentType argument : rest) + | binderType == argumentType = + specialize + (instantiateCanonical argument body) + rest + specialize _term _arguments = + Nothing - andP left right = - notP (CImp left (notP right)) + abstractTarget depth term + | term == shiftCanonical depth 0 target = + (True, CBound (fromIntegral depth)) + | otherwise = + case term of + CBound index + | index < fromIntegral depth -> + (False, CBound index) + | otherwise -> + (False, CBound (index + 1)) + CGlobal global -> + (False, CGlobal global) + CIntrinsic intrinsic -> + (False, CIntrinsic intrinsic) + COpaqueInteger integer -> + (False, COpaqueInteger integer) + CApp function argument -> + combine CApp + (abstractTarget depth function) + (abstractTarget depth argument) + CLam binderType body -> + let (found, abstracted) = + abstractTarget (depth + 1) body + in (found, CLam binderType abstracted) + CFalsum -> + (False, CFalsum) + CImp premise conclusion -> + combine CImp + (abstractTarget depth premise) + (abstractTarget depth conclusion) + CEq operandType left right -> + combine (CEq operandType) + (abstractTarget depth left) + (abstractTarget depth right) + CForall binderType body -> + let (found, abstracted) = + abstractTarget (depth + 1) body + in (found, CForall binderType abstracted) + + combine constructor (leftFound, left) (rightFound, right) = + (leftFound || rightFound, constructor left right) +scopedCharacteristicDefinition _characteristic _target _arguments = + Nothing - notP proposition = - CImp proposition CFalsum -scopedSetDefinition _expression = +-- | Build the replacement graph of one checked set-valued local function. +-- The ordered-pair constructor is an ordinary checked source object. +scopedReplacementGraph + :: ScopedCheckedCore global + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> Maybe + ( ScopedCheckedCore global + , ScopedCheckedCore global + , ScopedCheckedCore global + ) +scopedReplacementGraph + (ScopedCheckedCore context pairType pair) + domain@(ScopedCheckedCore domainContext TySet domainTerm) + (ScopedCheckedCore valueContext TySet value) + | pairType == TySet `TyArrow` (TySet `TyArrow` TySet) + , domainContext == context + , valueContext == TySet : context = + let pairValue = + CApp + (CApp + (shiftCanonical 1 0 pair) + (CBound 0)) + value + function = CLam TySet pairValue + graph = + CApp + (CApp (CIntrinsic Repl) domainTerm) + function + in Just + ( ScopedCheckedCore context TySet graph + , domain + , ScopedCheckedCore + context + (TySet `TyArrow` TySet) + function + ) +scopedReplacementGraph _pair _domain _value = Nothing +betaNormalizeCanonical + :: CanonicalTerm global + -> CanonicalTerm global +betaNormalizeCanonical = \case + CApp function argument -> + case betaNormalizeCanonical function of + CLam _binderType body -> + betaNormalizeCanonical + (instantiateCanonical + (betaNormalizeCanonical argument) + body) + normalizedFunction -> + CApp + normalizedFunction + (betaNormalizeCanonical argument) + CLam binderType body -> + CLam binderType (betaNormalizeCanonical body) + CImp premise conclusion -> + CImp + (betaNormalizeCanonical premise) + (betaNormalizeCanonical conclusion) + CEq operandType left right -> + CEq operandType + (betaNormalizeCanonical left) + (betaNormalizeCanonical right) + CForall binderType body -> + CForall binderType (betaNormalizeCanonical body) + term -> term + -- | Combine two checked propositions under the same lexical context. implyScopedCore :: ScopedCheckedCore global diff --git a/source/Checking/Datatype.hs b/source/Checking/Datatype.hs index d694ec8..a47f93d 100644 --- a/source/Checking/Datatype.hs +++ b/source/Checking/Datatype.hs @@ -13,13 +13,9 @@ module Checking.Datatype , CheckedDatatypePremiseView(..) , checkedDatatypeClauseViews , checkedDatatypeGeneratedFacts - , checkedDatatypeFacts - , checkedDatatypeFactRoles ) where import Base -import Checking.Facts -import Checking.Legacy import Report.Location import Syntax.Internal import Syntax.Lexicon @@ -278,50 +274,6 @@ checkedDatatypeGeneratedFacts checkedDatatypeGeneratedFacts = datatypeFacts -checkedDatatypeFacts - :: Location - -> Marker - -> CheckedDatatype - -> NonEmpty StagedFact -checkedDatatypeFacts location blockMarker checked = - fmap stage (datatypeFacts checked) - where - stage (factMarker, formula) = - stageFact - (factMarker :| []) - (factOrigin location blockMarker) - (prepareSemanticFact formula) - -checkedDatatypeFactRoles - :: CheckedDatatype - -> NonEmpty LegacyDatatypeFactRole -checkedDatatypeFactRoles datatype = - appendList - (LegacyDatatypeIntroduction - <$ checkedDatatypeClauses datatype) - ( replicate - (length - (unorderedPairs - (NonEmpty.toList - (checkedDatatypeClauses datatype)))) - LegacyDatatypeDistinctness - <> [ LegacyDatatypeInjectivity - | clause <- - NonEmpty.toList - (checkedDatatypeClauses datatype) - , not - (null - (checkedDatatypeClauseConstructorArgs - clause)) - ] - <> [ LegacyDatatypeCases - , LegacyDatatypeInduction - ] - ) - where - appendList (first :| rest) trailing = - first :| (rest <> trailing) - datatypeFacts :: CheckedDatatype -> NonEmpty (Marker, Formula) datatypeFacts datatype = appendList 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 diff --git a/source/Checking/Dependencies.hs b/source/Checking/Dependencies.hs deleted file mode 100644 index 392bb04..0000000 --- a/source/Checking/Dependencies.hs +++ /dev/null @@ -1,189 +0,0 @@ -{-# LANGUAGE NoImplicitPrelude #-} - -module Checking.Dependencies - ( DependencyRegistry - , DependencyRegistrationError(..) - , fromRootSymbols - , registerDependencies - , lookupDependencies - , dependencyClosure - , dependencyPath - , DependencyRegistryDelta - , dependencyRegistryExtension - , applyDependencyRegistryDelta - ) where - -import Base -import Syntax.Internal - -import Data.List.NonEmpty qualified as NonEmpty -import Data.Map.Strict qualified as Map -import Data.Set qualified as Set -import Data.Text qualified as Text - - -newtype DependencyRegistry = DependencyRegistry - { dependencyRows :: Map Symbol (Set Symbol) - } - deriving (Show, Eq) - -data DependencyRegistrationError - = DependencyOwnerAlreadyRegistered !Symbol - | SelfDependency !Symbol - | UnknownDependency !Symbol - deriving (Show, Eq) - -fromRootSymbols :: Set Symbol -> DependencyRegistry -fromRootSymbols roots = - DependencyRegistry - (Map.fromSet (const mempty) roots) - -registerDependencies - :: Symbol - -> Set Symbol - -> DependencyRegistry - -> Either DependencyRegistrationError DependencyRegistry -registerDependencies owner dependencies registry - | Map.member owner rows = - Left (DependencyOwnerAlreadyRegistered owner) - | owner `Set.member` dependencies = - Left (SelfDependency owner) - | Just unknown <- Set.lookupMin (dependencies `Set.difference` Map.keysSet rows) = - Left (UnknownDependency unknown) - | otherwise = - Right - (DependencyRegistry - (Map.insert owner dependencies rows)) - where - rows = dependencyRows registry - -lookupDependencies - :: Symbol - -> DependencyRegistry - -> Maybe (Set Symbol) -lookupDependencies symbol = - Map.lookup symbol . dependencyRows - -dependencyClosure - :: DependencyRegistry - -> Set Symbol - -> Either Symbol (Set Symbol) -dependencyClosure registry = - go mempty . Set.toList - where - go seen [] = - Right seen - go seen (symbol:rest) - | symbol `Set.member` seen = - go seen rest - | otherwise = - case lookupDependencies symbol registry of - Nothing -> - Left symbol - Just direct -> - go - (Set.insert symbol seen) - (Set.toList direct <> rest) - -dependencyPath - :: DependencyRegistry - -> Set Symbol - -> Symbol - -> Either Symbol (Maybe (NonEmpty Symbol)) -dependencyPath registry seeds target = - firstPath (Set.toList seeds) - where - firstPath [] = - Right Nothing - firstPath (seed:rest) = do - path <- go mempty seed - case path of - Just _ -> - pure path - Nothing -> - firstPath rest - - go seen symbol - | symbol == target = - Right (Just (NonEmpty.singleton symbol)) - | symbol `Set.member` seen = - Right Nothing - | otherwise = - case lookupDependencies symbol registry of - Nothing -> - Left symbol - Just direct -> - prependFirst - symbol - (Set.toList direct) - (Set.insert symbol seen) - - prependFirst _prefix [] _seen = - Right Nothing - prependFirst prefix (dependency:rest) seen = do - path <- go seen dependency - case path of - Just found -> - Right (Just (NonEmpty.cons prefix found)) - Nothing -> - prependFirst prefix rest seen - - -newtype DependencyRegistryDelta = DependencyRegistryDelta - (Map Symbol (Set Symbol)) - deriving (Show, Eq) - -dependencyRegistryExtension - :: DependencyRegistry - -> DependencyRegistry - -> Either Text DependencyRegistryDelta -dependencyRegistryExtension previous current - | not - (all - (\(symbol, dependencies) -> - Map.lookup symbol currentRows - == Just dependencies) - (Map.toList previousRows)) = - Left "dependency registry changed an imported row" - | otherwise = - Right - (DependencyRegistryDelta - (Map.difference currentRows previousRows)) - where - previousRows = - dependencyRows previous - currentRows = - dependencyRows current - -applyDependencyRegistryDelta - :: DependencyRegistryDelta - -> DependencyRegistry - -> Either Text DependencyRegistry -applyDependencyRegistryDelta - (DependencyRegistryDelta additions) - registry - | not (Set.null duplicateOwners) = - Left "dependency registry imports define the same owner" - | Just owner <- - find - (\(candidate, dependencies) -> - candidate `Set.member` dependencies) - (Map.toList additions) = - Left - ("dependency registry import is self-referential: " - <> Text.pack (show (fst owner))) - | not (Set.null unknownDependencies) = - Left "dependency registry import has an unknown dependency" - | otherwise = - Right - (DependencyRegistry - (Map.union rows additions)) - where - rows = - dependencyRows registry - duplicateOwners = - Map.keysSet rows `Set.intersection` Map.keysSet additions - available = - Map.keysSet rows <> Map.keysSet additions - unknownDependencies = - Set.unions (Map.elems additions) `Set.difference` available diff --git a/source/Checking/Exact.hs b/source/Checking/Exact.hs index 6bb8bd6..6ee258e 100644 --- a/source/Checking/Exact.hs +++ b/source/Checking/Exact.hs @@ -17,9 +17,15 @@ module Checking.Exact , PreparedExactSetExpression , preparedExactSetExpressionCore , prepareExactSetExpression + , PreparedExactLocalFunctionGraph + , preparedExactLocalFunctionGraphCore + , preparedExactLocalFunctionGraphDomain + , preparedExactLocalFunctionGraphMap + , prepareExactLocalFunctionGraph , PreparedExactClaimEnvelope , preparedExactClaimTarget , preparedExactClaimVariables + , preparedExactClaimContext , preparedExactClaimAntecedentCount , prepareExactClaimEnvelope , PreparedExactDeclaration @@ -31,6 +37,9 @@ module Checking.Exact , preparedExactIsDefinition , prepareExactDeclaration , commitPreparedExactBinding + , PreparedExactStructure + , prepareExactStructure + , commitPreparedExactStructure , PreparedExactSourceAxiom , prepareExactSourceAxiom , commitPreparedExactSourceAxiom @@ -49,7 +58,7 @@ import Felix.Cache.Codec import Felix.Module import Report.Location import Syntax.Abstract qualified as Raw -import Syntax.Interface (CanonicalLexicalEntry) +import Syntax.Interface (CanonicalLexicalEntry(..)) import Syntax.Lexicon qualified as Lexicon import Control.Monad.Except (ExceptT) @@ -59,6 +68,7 @@ import Control.Monad (foldM, unless, when) import Control.Monad.State.Strict (StateT) import Control.Monad.State.Strict qualified as State import Data.ByteString (ByteString) +import Data.Bifunctor (first) import Data.List.NonEmpty qualified as NonEmpty import Data.Map.Strict qualified as Map import Data.Maybe (catMaybes) @@ -83,6 +93,12 @@ data ExactBinder = ExactBinder !ExactLocalId !Raw.VarSymbol !CoreType + !(Maybe ExactStructureAnnotation) + +data ExactStructureAnnotation = ExactStructureAnnotation + !SemanticStructurePhrase + !(Maybe ObjectId) + !(Map.Map Raw.StructSymbol ObjectId) -- | The active nearest-first binders of one exact proof scope. newtype ExactBinderContext = ExactBinderContext [ExactBinder] @@ -103,12 +119,12 @@ extendExactBinderContext additions (ExactBinderContext initial) = | any (sameIdentity identity) binders = Left (ExactDuplicateLocalIdentity (locate variable) identity) | otherwise = - Right (ExactBinder identity variable TySet : binders) + Right (ExactBinder identity variable TySet Nothing : binders) - sameVariable variable (ExactBinder _identity existing _coreType) = + sameVariable variable (ExactBinder _identity existing _coreType _structure) = existing == variable - sameIdentity identity (ExactBinder existing _variable _coreType) = + sameIdentity identity (ExactBinder existing _variable _coreType _structure) = existing == identity exactBinderContextSupport @@ -117,7 +133,7 @@ exactBinderContextSupport exactBinderContextSupport (ExactBinderContext binders) = Vector.fromList [ (identity, coreType) - | ExactBinder identity _variable coreType <- binders + | ExactBinder identity _variable coreType _structure <- binders ] exactBinderContextIndex @@ -129,7 +145,7 @@ exactBinderContextIndex variable (ExactBinderContext binders) = where go _index [] = Nothing - go index (ExactBinder _identity candidate _coreType : rest) + go index (ExactBinder _identity candidate _coreType _structure : rest) | candidate == variable = Just index | otherwise = go (index + 1) rest @@ -151,33 +167,70 @@ preparedExactSetExpressionCore preparedExactSetExpressionCore (PreparedExactSetExpression expression) = expression +-- | A checked replacement graph and the two checked arguments used to +-- specialize its foundation characteristic. This is transient proof +-- preparation data, not a declaration or durable object. +data PreparedExactLocalFunctionGraph = PreparedExactLocalFunctionGraph + !(ScopedCheckedCore ObjectId) + !(ScopedCheckedCore ObjectId) + !(ScopedCheckedCore ObjectId) + +preparedExactLocalFunctionGraphCore + :: PreparedExactLocalFunctionGraph + -> ScopedCheckedCore ObjectId +preparedExactLocalFunctionGraphCore + (PreparedExactLocalFunctionGraph graph _domain _function) = + graph + +preparedExactLocalFunctionGraphDomain + :: PreparedExactLocalFunctionGraph + -> ScopedCheckedCore ObjectId +preparedExactLocalFunctionGraphDomain + (PreparedExactLocalFunctionGraph _graph domain _function) = + domain + +preparedExactLocalFunctionGraphMap + :: PreparedExactLocalFunctionGraph + -> ScopedCheckedCore ObjectId +preparedExactLocalFunctionGraphMap + (PreparedExactLocalFunctionGraph _graph _domain function) = + function + -- | One authoritative closed proposition prepared from a top-level claim -- header and conclusion. The remaining fields are transient opening data for -- the proof compiler. data PreparedExactClaimEnvelope = PreparedExactClaimEnvelope !(ScopedCheckedCore ObjectId) ![Raw.VarSymbol] + !ExactBinderContext !Natural preparedExactClaimTarget :: PreparedExactClaimEnvelope -> ScopedCheckedCore ObjectId preparedExactClaimTarget - (PreparedExactClaimEnvelope target _variables _antecedents) = + (PreparedExactClaimEnvelope target _variables _context _antecedents) = target preparedExactClaimVariables :: PreparedExactClaimEnvelope -> [Raw.VarSymbol] preparedExactClaimVariables - (PreparedExactClaimEnvelope _target variables _antecedents) = + (PreparedExactClaimEnvelope _target variables _context _antecedents) = variables +preparedExactClaimContext + :: PreparedExactClaimEnvelope + -> ExactBinderContext +preparedExactClaimContext + (PreparedExactClaimEnvelope _target _variables context _antecedents) = + context + preparedExactClaimAntecedentCount :: PreparedExactClaimEnvelope -> Natural preparedExactClaimAntecedentCount - (PreparedExactClaimEnvelope _target _variables antecedents) = + (PreparedExactClaimEnvelope _target _variables _context antecedents) = antecedents @@ -191,7 +244,7 @@ data PreparedExactDeclaration = PreparedExactDeclaration !Location !ExactDeclarationFamily !SemanticGlobalKey - !ObjectId + !SemanticGlobalTarget !(Maybe AssertedObject) !(Maybe SemanticName) !DeclarationSyntaxId @@ -209,7 +262,7 @@ preparedExactGlobalKey preparedExactObjectId :: PreparedExactDeclaration -> ObjectId preparedExactObjectId (PreparedExactDeclaration _location _family _key target _object _alias _syntax) = - target + semanticGlobalTargetObject target preparedExactObject :: PreparedExactDeclaration @@ -235,11 +288,8 @@ preparedExactGlobalTarget -> SemanticGlobalTarget preparedExactGlobalTarget (PreparedExactDeclaration - _location family _key target _object _alias _syntax) = - case family of - ExactSignature -> GlobalReference target - ExactAbbreviation -> TransparentExpansion target - ExactDefinition -> GlobalReference target + _location _family _key target _object _alias _syntax) = + target preparedDefinitionAlias :: PreparedExactDeclaration @@ -255,6 +305,20 @@ data PreparedExactSourceAxiom = PreparedExactSourceAxiom !(ScopedCheckedCore ObjectId) !DeclarationSyntaxId +data PreparedExactStructureFact = PreparedExactStructureFact + !Location + !(FrozenCheckedCore ObjectId) + !SemanticName + +data PreparedExactStructure = PreparedExactStructure + !Location + ![AssertedObject] + !ObjectId + !SemanticStructureDescriptor + !SemanticName + ![PreparedExactStructureFact] + !DeclarationSyntaxId + data ExactCompileError = ExactUnsupportedDeclaration !Location | ExactUnsupportedDeclarationBody !Location @@ -277,6 +341,28 @@ data ExactCompileError | ExactObjectTypeMismatch !Location !CoreType !CoreType | ExactUnsupportedHeaderAssumption !Location | ExactQuantifiedTermRequiresStatementSubject !Location + | ExactStructureNotVisible !Location !SemanticStructurePhrase + | ExactBaseStructureNotAssertable !Location !SemanticStructurePhrase + | ExactDuplicateStructureAnnotation !Location !Raw.VarSymbol + | ExactStructureOperationNotAvailable !Location !Raw.StructSymbol + | ExactStructureOperationAmbiguous + !Location !Raw.StructSymbol ![ObjectId] + | ExactContextualExpansionNotAvailable + !Location !SemanticGlobalKey + | ExactContextualRequirementConflict + !Location !Raw.StructSymbol !ObjectId !ObjectId + | ExactStructureOccurrenceMismatch !Location + | ExactStructureSelfParent !Location !SemanticStructurePhrase + | ExactStructureDuplicateParent !Location !SemanticStructurePhrase + | ExactStructureAlreadyVisible !Location !SemanticStructurePhrase + | ExactStructureDuplicateOperation !Location !Raw.StructSymbol + | ExactStructureOperationAlreadyInherited !Location !Raw.StructSymbol + | ExactStructureOperationConflict + !Location !Raw.StructSymbol + !SemanticStructurePhrase !SemanticStructurePhrase + | ExactStructureHasNoCarrier !Location !SemanticStructurePhrase + | ExactStructureDescriptorInvalid !Location !SemanticEnvironmentError + | ExactStructureObjectNotVisible !Location !ObjectId deriving stock (Show, Eq) exactCompileErrorLocation :: ExactCompileError -> Location @@ -301,6 +387,23 @@ exactCompileErrorLocation = \case ExactObjectTypeMismatch location _expected _actual -> location ExactUnsupportedHeaderAssumption location -> location ExactQuantifiedTermRequiresStatementSubject location -> location + ExactStructureNotVisible location _phrase -> location + ExactBaseStructureNotAssertable location _phrase -> location + ExactDuplicateStructureAnnotation location _variable -> location + ExactStructureOperationNotAvailable location _symbol -> location + ExactStructureOperationAmbiguous location _symbol _objects -> location + ExactContextualExpansionNotAvailable location _key -> location + ExactContextualRequirementConflict location _symbol _first _second -> location + ExactStructureOccurrenceMismatch location -> location + ExactStructureSelfParent location _phrase -> location + ExactStructureDuplicateParent location _phrase -> location + ExactStructureAlreadyVisible location _phrase -> location + ExactStructureDuplicateOperation location _symbol -> location + ExactStructureOperationAlreadyInherited location _symbol -> location + ExactStructureOperationConflict location _symbol _first _second -> location + ExactStructureHasNoCarrier location _phrase -> location + ExactStructureDescriptorInvalid location _failure -> location + ExactStructureObjectNotVisible location _object -> location renderExactCompileError :: ExactCompileError -> Text renderExactCompileError = \case @@ -348,6 +451,56 @@ renderExactCompileError = \case ExactQuantifiedTermRequiresStatementSubject location -> at location <> "a quantified term must be the sole subject of an exact statement" + ExactStructureNotVisible location structurePhrase -> + at location <> "the structure " <> shown structurePhrase <> " is not visible" + ExactBaseStructureNotAssertable location structurePhrase -> + at location <> "the metadata-only structure " <> shown structurePhrase + <> " cannot be asserted" + ExactDuplicateStructureAnnotation location variable -> + at location <> "the structure binder " <> shown variable + <> " is annotated more than once" + ExactStructureOperationNotAvailable location symbol -> + at location <> "the structure operation " <> shown symbol + <> " is not available in the active structure scope" + ExactStructureOperationAmbiguous location symbol objects -> + at location <> "the structure operation " <> shown symbol + <> " is ambiguous between " <> shown objects + ExactContextualExpansionNotAvailable location key -> + at location <> "the contextual abbreviation " <> shown key + <> " has no compatible active structure" + ExactContextualRequirementConflict location symbol firstObject secondObject -> + at location <> "the contextual abbreviation requires incompatible " + <> shown symbol <> " operations " <> shown firstObject + <> " and " <> shown secondObject + ExactStructureOccurrenceMismatch location -> + at location <> "the structure syntax occurrences do not match the declaration" + ExactStructureSelfParent location structurePhrase -> + at location <> "the structure " <> shown structurePhrase + <> " cannot inherit from itself" + ExactStructureDuplicateParent location structurePhrase -> + at location <> "the parent structure " <> shown structurePhrase + <> " is repeated" + ExactStructureAlreadyVisible location structurePhrase -> + at location <> "the structure " <> shown structurePhrase + <> " is already declared" + ExactStructureDuplicateOperation location symbol -> + at location <> "the structure operation " <> shown symbol + <> " is repeated" + ExactStructureOperationAlreadyInherited location symbol -> + at location <> "the structure operation " <> shown symbol + <> " is already inherited" + ExactStructureOperationConflict location symbol firstOrigin secondOrigin -> + at location <> "the inherited structure operation " <> shown symbol + <> " conflicts between " <> shown firstOrigin + <> " and " <> shown secondOrigin + ExactStructureHasNoCarrier location structurePhrase -> + at location <> "the structure " <> shown structurePhrase + <> " does not inherit the base carrier operation" + ExactStructureDescriptorInvalid location _failure -> + at location <> "the canonical structure descriptor is inconsistent" + ExactStructureObjectNotVisible location identity -> + at location <> "the structure fact mentions unavailable object " + <> shown identity where at location = locationToText location <> ": " shown :: Show value => value -> Text @@ -355,7 +508,11 @@ renderExactCompileError = \case data ElaborationState = ElaborationState { elaborationBinders :: !(Map.Map Raw.VarSymbol Natural) + , elaborationStructures :: !(Map.Map Natural ExactStructureAnnotation) , elaborationGlobals :: !(Map.Map ObjectId CoreType) + , elaborationContextualBinder :: !(Maybe Natural) + , elaborationContextualRequirements + :: !(Map.Map Raw.StructSymbol ObjectId) } type Elaborate failure = @@ -371,6 +528,9 @@ data PreparedHead = PreparedHead data PreparedBody = OpaqueBody | TransparentBody !(CanonicalTerm ObjectId) + | ContextualTransparentBody + !(Map.Map Raw.StructSymbol ObjectId) + !(CanonicalTerm ObjectId) prepareExactProposition :: ExactBinderContext @@ -379,10 +539,7 @@ prepareExactProposition (Either ExactCompileError PreparedExactProposition) prepareExactProposition context statement = Except.runExceptT do - let initialElaboration = - ElaborationState - (binderIndices context) - mempty + let initialElaboration = initialElaborationState context (term, finalElaboration) <- State.runStateT (compileStatement statement) @@ -410,10 +567,7 @@ prepareExactSetExpression (Either ExactCompileError PreparedExactSetExpression) prepareExactSetExpression context expression = Except.runExceptT do - let initialElaboration = - ElaborationState - (binderIndices context) - mempty + let initialElaboration = initialElaborationState context (term, finalElaboration) <- State.runStateT (compileExpressionAsSet expression) @@ -434,6 +588,61 @@ prepareExactSetExpression context expression = (scopedCoreType checked))) pure (PreparedExactSetExpression checked) +prepareExactLocalFunctionGraph + :: Location + -> ExactBinderContext + -> ExactBinderContext + -> Raw.Expr + -> Raw.Expr + -> Declaration.ModuleDriver failure + (Either ExactCompileError PreparedExactLocalFunctionGraph) +prepareExactLocalFunctionGraph + location context argumentContext domainExpression valueExpression = + Except.runExceptT do + domain <- + preparedExactSetExpressionCore + <$> ( Except.lift + (prepareExactSetExpression context domainExpression) + >>= Except.liftEither + ) + value <- + preparedExactSetExpressionCore + <$> ( Except.lift + (prepareExactSetExpression + argumentContext valueExpression) + >>= Except.liftEither + ) + pair <- prepareOrderedPair + case scopedReplacementGraph pair domain value of + Just (graph, checkedDomain, function) -> + pure + (PreparedExactLocalFunctionGraph + graph checkedDomain function) + Nothing -> + impossible + "checked local-function components did not form a replacement graph" + where + prepareOrderedPair = do + let initialElaboration = initialElaborationState context + key = + SemanticExpressionFunction + (Raw.mixfixPattern Raw.PairSymbol) + expected = TySet `TyArrow` (TySet `TyArrow` TySet) + ((term, actual), finalElaboration) <- + State.runStateT + (applyResolvedTyped location key []) + initialElaboration + unless (actual == expected) + (Except.throwError + (ExactObjectTypeMismatch location expected actual)) + either + (Except.throwError . ExactCoreCheckFailed location) + pure + (checkScopedCanonicalCore + (`Map.lookup` elaborationGlobals finalElaboration) + (binderTypes context) + term) + prepareExactClaimEnvelope :: [Raw.Asm] -> Raw.Stmt @@ -463,12 +672,13 @@ prepareExactClaimEnvelope assumptions statement = discover (variables <> [variable]) extended Left failure -> pure (Left failure) - Right (target, antecedentCount) -> + Right (target, antecedentCount, structures) -> pure (Right (PreparedExactClaimEnvelope target variables + (annotateBinderContext structures context) antecedentCount)) prepareExactClaimAttempt @@ -478,13 +688,13 @@ prepareExactClaimAttempt -> Declaration.ModuleDriver failure (Either ExactCompileError - (ScopedCheckedCore ObjectId, Natural)) + ( ScopedCheckedCore ObjectId + , Natural + , Map.Map Natural ExactStructureAnnotation + )) prepareExactClaimAttempt context assumptions statement = Except.runExceptT do - let initialElaboration = - ElaborationState - (binderIndices context) - mempty + let initialElaboration = initialElaborationState context ((antecedents, conclusion), finalElaboration) <- State.runStateT ( do @@ -519,7 +729,11 @@ prepareExactClaimAttempt context assumptions statement = closed = closeClaimBinders implication unless (null (scopedCoreContext closed)) (impossible "exact claim closure retained a binder") - pure (closed, fromIntegral (length antecedents)) + pure + ( closed + , fromIntegral (length antecedents) + , elaborationStructures finalElaboration + ) checkEnvelopeProposition :: ElaborationState @@ -563,16 +777,47 @@ binderIndices :: ExactBinderContext -> Map.Map Raw.VarSymbol Natural binderIndices (ExactBinderContext binders) = Map.fromList [ (variable, fromIntegral index) - | (index, ExactBinder _identity variable _coreType) <- + | (index, ExactBinder _identity variable _coreType _structure) <- + zip [0 :: Int ..] binders + ] + +binderStructures + :: ExactBinderContext + -> Map.Map Natural ExactStructureAnnotation +binderStructures (ExactBinderContext binders) = + Map.fromList + [ (fromIntegral index, structure) + | (index, ExactBinder _identity _variable _coreType (Just structure)) <- zip [0 :: Int ..] binders ] binderTypes :: ExactBinderContext -> [CoreType] binderTypes (ExactBinderContext binders) = [ coreType - | ExactBinder _identity _variable coreType <- binders + | ExactBinder _identity _variable coreType _structure <- binders ] +initialElaborationState :: ExactBinderContext -> ElaborationState +initialElaborationState context = + ElaborationState + (binderIndices context) + (binderStructures context) + mempty + Nothing + mempty + +annotateBinderContext + :: Map.Map Natural ExactStructureAnnotation + -> ExactBinderContext + -> ExactBinderContext +annotateBinderContext structures (ExactBinderContext binders) = + ExactBinderContext + [ ExactBinder identity variable coreType + (Map.lookup (fromIntegral index) structures) + | (index, ExactBinder identity variable coreType _old) <- + zip [0 :: Int ..] binders + ] + compileHeaderAssumption :: Raw.Asm -> Elaborate failure [(Location, CanonicalTerm ObjectId)] @@ -595,7 +840,9 @@ compileHeaderAssumption = \case ] Raw.AsmLetIn variables domain -> do variableTerms <- traverse compileIntroducedVariable variables - domainTerm <- compileExpressionAsSet domain + domainTerm <- + compileExpressionAsSet domain + >>= structureCarrierCast (locate domain) pure [ ( locate variable , CApp @@ -616,9 +863,44 @@ compileHeaderAssumption = \case Raw.AsmLetThe variable _function -> Except.throwError (ExactUnsupportedHeaderAssumption (locate variable)) - Raw.AsmLetStruct variable _structure -> - Except.throwError - (ExactUnsupportedHeaderAssumption (locate variable)) + Raw.AsmLetStruct variable structure -> do + subject <- compileIntroducedVariable variable + annotation <- + resolveStructureAnnotation + (locate variable) + structure + index <- + maybe + (impossible "an introduced structure variable is unbound") + pure + =<< Map.lookup variable <$> State.gets elaborationBinders + existing <- State.gets (Map.lookup index . elaborationStructures) + when + (isJust existing) + (Except.throwError + (ExactDuplicateStructureAnnotation + (locate variable) variable)) + State.modify' \state -> + state + { elaborationStructures = + Map.insert index annotation + (elaborationStructures state) + } + predicate <- + maybe + (impossible "an assertable structure has no predicate") + pure + (structureAnnotationPredicate annotation) + recordExactGlobal + predicate + (TyArrow TySet TyProp) + pure + [ ( locate variable + , CApp + (CGlobal predicate) + subject + ) + ] compileIntroducedVariable :: Raw.VarSymbol @@ -626,6 +908,63 @@ compileIntroducedVariable compileIntroducedVariable variable = compileExpressionAsSet (Raw.ExprVar variable) +resolveStructureAnnotation + :: Location + -> Raw.StructPhrase + -> Elaborate failure ExactStructureAnnotation +resolveStructureAnnotation location rawPhrase = do + let structurePhrase = semanticStructurePhrase rawPhrase + resolved <- + State.lift + (Except.lift + (Declaration.resolveVisibleStructureDriver structurePhrase)) + structure <- + maybe + (Except.throwError + (ExactStructureNotVisible location structurePhrase)) + pure + resolved + predicate <- + maybe + (Except.throwError + (ExactBaseStructureNotAssertable location structurePhrase)) + pure + (Declaration.resolvedStructurePredicate structure) + pure + (ExactStructureAnnotation + structurePhrase + (Just predicate) + (Declaration.resolvedStructureOperations structure)) + +structureAnnotationPredicate :: ExactStructureAnnotation -> Maybe ObjectId +structureAnnotationPredicate + (ExactStructureAnnotation _ predicate _operations) = + predicate + +structureAnnotationOperation + :: Raw.StructSymbol + -> ExactStructureAnnotation + -> Maybe ObjectId +structureAnnotationOperation symbol + (ExactStructureAnnotation _phrase _predicate operations) = + Map.lookup symbol operations + +recordExactGlobal :: ObjectId -> CoreType -> Elaborate failure () +recordExactGlobal identity coreType = do + existing <- State.gets (Map.lookup identity . elaborationGlobals) + case existing of + Nothing -> + State.modify' \state -> + state + { elaborationGlobals = + Map.insert identity coreType + (elaborationGlobals state) + } + Just actual + | actual == coreType -> pure () + | otherwise -> + impossible "one exact global acquired two checked types" + prepareExactSourceAxiom :: Raw.Block -> Declaration.ModuleDriver failure @@ -704,13 +1043,24 @@ prepareExactDeclaration block entries = case rawBody of Nothing -> pure (OpaqueBody, Map.empty) Just buildBody -> do - let initialElaboration = ElaborationState mempty mempty + let initialElaboration = + ElaborationState + mempty mempty mempty Nothing mempty (canonical, finalElaboration) <- State.runStateT buildBody initialElaboration - pure - ( TransparentBody canonical - , elaborationGlobals finalElaboration - ) + let requirements = + elaborationContextualRequirements finalElaboration + body + | Map.null requirements = + TransparentBody canonical + | family == ExactAbbreviation = + ContextualTransparentBody + requirements + (CLam TySet canonical) + | otherwise = + impossible + "a non-abbreviation acquired contextual requirements" + pure (body, elaborationGlobals finalElaboration) let PreparedHead semanticKey _parameters coreType = head' unless (semanticKey == key) (Except.throwError @@ -726,8 +1076,8 @@ prepareExactDeclaration block entries = (generatedObjectSlot 0) content' = OpaqueObjectContent theory seed coreType - pure - (opaqueObjectId theory seed coreType, content') + identity = opaqueObjectId theory seed coreType + pure (GlobalReference identity, content') TransparentBody canonical -> do checked <- either @@ -749,15 +1099,54 @@ prepareExactDeclaration block entries = theory coreType canonical + let identity = + transparentObjectId theory coreType canonical + semanticTarget = + case family of + ExactAbbreviation -> + TransparentExpansion identity + ExactDefinition -> GlobalReference identity + ExactSignature -> + impossible + "a signature acquired a transparent body" + pure (semanticTarget, content') + ContextualTransparentBody requirements canonical -> do + let contextualType = TyArrow TySet coreType + checked <- + either + (Except.throwError + . ExactCoreCheckFailed (locate block)) + pure + (checkCanonicalCore + (`Map.lookup` globals) + canonical) + unless + (frozenCoreType checked == contextualType) + (Except.throwError + (ExactObjectTypeMismatch + (locate block) + contextualType + (frozenCoreType checked))) + let content' = + TransparentObjectContent + theory + contextualType + canonical + identity = + transparentObjectId + theory contextualType canonical pure - ( transparentObjectId theory coreType canonical + ( ContextualTransparentExpansion + identity requirements , content' ) - available <- Except.lift (Declaration.objectAvailableDriver target) + let targetObject = semanticGlobalTargetObject target + available <- + Except.lift (Declaration.objectAvailableDriver targetObject) let alias = definitionAlias block asserted | available = Nothing - | otherwise = Just (assertedObject target content) + | otherwise = Just (assertedObject targetObject content) syntax = declarationSyntaxId (encodePreparedSyntax family head' body alias) @@ -801,6 +1190,367 @@ commitPreparedExactBinding prepared (preparedExactObjectId prepared)) candidate) +prepareExactStructure + :: Raw.Block + -> [CanonicalLexicalEntry] + -> Declaration.ModuleDriver failure + (Either ExactCompileError PreparedExactStructure) +prepareExactStructure block entries = + Except.runExceptT do + (location, marker, structure) <- + case block of + Raw.BlockStruct location _title (Raw.Marker marker) structure -> + pure (location, marker, structure) + _ -> Except.throwError + (ExactUnsupportedDeclaration (locate block)) + validateStructureOccurrences location structure entries + let structurePhrase = + semanticStructurePhrase (Raw.structPhrase structure) + parentPhrases = + semanticStructurePhrase <$> Raw.structParents structure + when + (structurePhrase `elem` parentPhrases) + (Except.throwError + (ExactStructureSelfParent location structurePhrase)) + case firstDuplicate parentPhrases of + Just duplicate -> + Except.throwError + (ExactStructureDuplicateParent location duplicate) + Nothing -> pure () + visible <- Except.lift + (Declaration.resolveVisibleStructureDriver structurePhrase) + when + (isJust visible) + (Except.throwError + (ExactStructureAlreadyVisible location structurePhrase)) + parents <- traverse (resolveParent location) parentPhrases + inherited <- + foldM mergeParentOperations Map.empty + (zip parentPhrases parents) + case firstDuplicate (Raw.structFixes structure) of + Just duplicate -> + Except.throwError + (ExactStructureDuplicateOperation location duplicate) + Nothing -> pure () + traverse_ + (\symbol -> + when + (Map.member symbol inherited) + (Except.throwError + (ExactStructureOperationAlreadyInherited + location symbol))) + (Raw.structFixes structure) + slot <- Except.lift Declaration.nextDeclarationSlotDriver + theory <- Except.lift Declaration.currentTheoryDriver + let operationType = TyArrow TySet TySet + makeOperation index symbol = + let seed = + opaqueDeclarationSeed + (declarationSlotModule slot) + (declarationSlotOrdinal slot) + StructureDeclaration + (generatedObjectSlot index) + content = OpaqueObjectContent theory seed operationType + identity = opaqueObjectId theory seed operationType + in ( symbol + , identity + , assertedObject identity content + ) + ownOperations = + zipWith makeOperation [0 ..] (Raw.structFixes structure) + operationObjects = + [ asserted + | (_symbol, _identity, asserted) <- ownOperations + ] + completeOperations = + Map.union + (Map.fromList + [ (symbol, identity) + | (symbol, identity, _asserted) <- ownOperations + ]) + (fst <$> inherited) + unless + (Map.member Raw.CarrierSymbol completeOperations) + (Except.throwError + (ExactStructureHasNoCarrier location structurePhrase)) + context <- + either Except.throwError pure + (extendExactBinderContext + ((exactLocalId 0, Raw.structLabel structure) :| []) + emptyExactBinderContext) + let provisionalAnnotation = + ExactStructureAnnotation + structurePhrase Nothing completeOperations + structureContext = + annotateBinderContext + (Map.singleton 0 provisionalAnnotation) + context + checkedAssumptions <- + traverse + (\(assumptionMarker, assumption) -> do + prepared <- Except.lift + (prepareExactProposition structureContext assumption) + proposition <- Except.liftEither prepared + pure + ( locate assumption + , assumptionMarker + , preparedExactPropositionCore proposition + )) + (Raw.structAssumes structure) + parentTerms <- + fmap catMaybes + (traverse + (\parent -> + case Declaration.resolvedStructurePredicate parent of + Nothing -> pure Nothing + Just predicate -> + pure + (Just + (CApp + (CGlobal predicate) + (CBound 0)))) + parents) + let assumptionTerms = + [ scopedCoreTerm proposition + | (_assumptionLocation, _assumptionMarker, proposition) <- + checkedAssumptions + ] + predicateBody = + CLam TySet + (logicalConjunction + (parentTerms <> assumptionTerms)) + predicateType = TyArrow TySet TyProp + predicateContent = + TransparentObjectContent theory predicateType predicateBody + predicate = + transparentObjectId theory predicateType predicateBody + predicateAvailable <- + Except.lift (Declaration.objectAvailableDriver predicate) + let predicateObject = + [ assertedObject predicate predicateContent + | not predicateAvailable + ] + ownBindings = + [ semanticStructureOperation symbol identity + | (symbol, identity, _asserted) <- ownOperations + ] + descriptor <- + Except.liftEither + (first + (ExactStructureDescriptorInvalid location) + (semanticStructureDescriptor + structurePhrase + (Just predicate) + parentPhrases + ownBindings)) + let structureApplication = + CApp (CGlobal predicate) (CBound 0) + inheritance = + [ ( location + , semanticName (marker <> "inherit") + , CForall TySet + (CImp structureApplication + (logicalConjunction parentTerms)) + ) + | not (null parentTerms) + ] + projections = + [ ( assumptionLocation + , semanticName assumptionMarker + , CForall TySet + (CImp structureApplication + (scopedCoreTerm proposition)) + ) + | ( assumptionLocation + , Raw.Marker assumptionMarker + , proposition + ) <- checkedAssumptions + ] + generatedTerms = inheritance <> projections + localTypes = + Map.fromList + ((predicate, predicateType) + : [ (identity, operationType) + | (_symbol, identity, _asserted) <- ownOperations + ]) + resolvedTypes <- + resolveStructureGlobalTypes + localTypes + [ term + | (_factLocation, _alias, term) <- generatedTerms + ] + generated <- + traverse + (\(factLocation, alias, term) -> do + frozen <- + either + (Except.throwError + . ExactCoreCheckFailed factLocation) + pure + (checkCanonicalCore + (`Map.lookup` resolvedTypes) + term) + pure + (PreparedExactStructureFact + factLocation frozen alias)) + generatedTerms + environment <- + Except.liftEither + (first + (ExactStructureDescriptorInvalid location) + (semanticEnvironmentWithStructures [] [descriptor])) + let syntax = + declarationSyntaxId + (encodePreparedStructure + environment + predicate + generated) + pure + (PreparedExactStructure + location + (operationObjects <> predicateObject) + predicate + descriptor + (semanticName marker) + generated + syntax) + where + resolveParent location structurePhrase = do + resolved <- Except.lift + (Declaration.resolveVisibleStructureDriver structurePhrase) + maybe + (Except.throwError + (ExactStructureNotVisible location structurePhrase)) + pure + resolved + + mergeParentOperations inherited (parentPhrase, parent) = + foldM + (insertParentOperation parentPhrase) + inherited + (Map.toAscList + (Declaration.resolvedStructureOperations parent)) + + insertParentOperation parentPhrase inherited (symbol, identity) = + case Map.lookup symbol inherited of + Nothing -> + pure + (Map.insert symbol (identity, parentPhrase) inherited) + Just (existing, existingOrigin) + | existing == identity -> pure inherited + | otherwise -> + Except.throwError + (ExactStructureOperationConflict + (locate block) + symbol + existingOrigin + parentPhrase) + + resolveStructureGlobalTypes localTypes terms = do + let dependencies = Set.unions (canonicalTermGlobals <$> terms) + foldM + (\types identity -> + case Map.lookup identity types of + Just{} -> pure types + Nothing -> do + coreType <- Except.lift + (Declaration.objectTypeDriver identity) + case coreType of + Nothing -> + Except.throwError + (ExactStructureObjectNotVisible + (locate block) identity) + Just actual -> + pure (Map.insert identity actual types)) + localTypes + (Set.toAscList dependencies) + +commitPreparedExactStructure + :: PreparedExactStructure + -> Declaration.ModuleDriver failure + ((), Declaration.CommittedDeclarationBatch) +commitPreparedExactStructure + (PreparedExactStructure + _location objects predicate descriptor alias generated syntax) = + Declaration.commitCompiledDeclaration syntax do + traverse_ Declaration.addDeclarationObject objects + Declaration.stageSemanticStructureDescriptor descriptor + definition <- + Declaration.reservePointwiseDefinitionEquationCandidate + predicate alias + generatedCandidates <- + case NonEmpty.nonEmpty generated of + Nothing -> pure [] + Just nonempty -> do + candidates <- + Declaration.reserveFrozenPropositionCandidateBatch + ( fmap + (\(PreparedExactStructureFact + _factLocation target factAlias) -> + (target, SearchEligible, [factAlias])) + nonempty + ) + pure (toList candidates) + Declaration.authorizeCompiledDeclaration do + Declaration.authorizeDefinitionEquationCandidate + predicate definition + case NonEmpty.nonEmpty + (zip generatedCandidates generated) of + Nothing -> pure () + Just ready -> + Declaration.authorizeVampireCandidateBatch + ( fmap + (\(candidate, PreparedExactStructureFact + factLocation _target _factAlias) -> + ( factLocation + , candidate + , do + void + (Declaration.useStagedCandidate + definition) + Declaration.prepareCurrentCandidateVampire + )) + ready + ) + +validateStructureOccurrences + :: Location + -> Raw.StructDefn + -> [CanonicalLexicalEntry] + -> ExceptT ExactCompileError (Declaration.ModuleDriver failure) () +validateStructureOccurrences location structure entries = do + let Raw.LexicalItemSgPl forms structureMarker = + Raw.structPhrase structure + expected = + CanonicalStructureNoun + (Raw.sg forms) + (Raw.pl forms) + structureMarker + : [ CanonicalStructureOperation command + | Raw.StructSymbol command <- Raw.structFixes structure + ] + unless + (entries == expected) + (Except.throwError + (ExactStructureOccurrenceMismatch location)) + +encodePreparedStructure + :: SemanticEnvironmentDelta + -> ObjectId + -> [PreparedExactStructureFact] + -> ByteString +encodePreparedStructure environment predicate generated = + encodeCache do + putCacheTag 0x04 + putSemanticEnvironmentDeltaCache environment + putObjectIdCache predicate + putCacheList + (\(PreparedExactStructureFact _location target alias) -> do + putCanonicalTermCache putObjectIdCache + (frozenCoreTerm target) + putCacheText (semanticNameText alias)) + generated + prepareHead :: Raw.Block -> SemanticGlobalKey @@ -870,32 +1620,32 @@ prepareAbbreviation prepareAbbreviation location key = \case Raw.AbbreviationEq (Raw.SymbolPattern symbol parameters) expression -> do ensureExpressionKey location symbol key - makeTransparentHead + makeContextualTransparentHead location key parameters TySet (compileExpressionAsSet expression) Raw.AbbreviationFun (Raw.Fun _ item parameters) term -> do ensureFunctionPhraseKey location item key - makeTransparentHead + makeContextualTransparentHead location key parameters TySet (compileTermAsSet term) Raw.AbbreviationAdj subject (Raw.Adj _ item arguments) statement -> do ensureAdjectiveKey location item key - makeTransparentHead + makeContextualTransparentHead location key (subject : arguments) TyProp (compileStatement statement) Raw.AbbreviationVerb subject (Raw.Verb _ item arguments) statement -> do ensureVerbKey location item key - makeTransparentHead + makeContextualTransparentHead location key (subject : arguments) TyProp (compileStatement statement) Raw.AbbreviationNoun subject (Raw.Noun _ item arguments) statement -> do ensureNounKey location item key - makeTransparentHead + makeContextualTransparentHead location key (subject : arguments) TyProp (compileStatement statement) Raw.AbbreviationRel left relation parameters right statement -> do ensureRelationKey location relation key - makeTransparentHead + makeContextualTransparentHead location key (parameters <> [left, right]) TyProp (compileStatement statement) @@ -994,6 +1744,32 @@ makeTransparentHead location key parameters resultType body = do pure (foldr (const (CLam TySet)) body' parameters) pure (prepared, close) +makeContextualTransparentHead + :: Location + -> SemanticGlobalKey + -> [Raw.VarSymbol] + -> CoreType + -> Elaborate failure (CanonicalTerm ObjectId) + -> ExceptT + ExactCompileError + (Declaration.ModuleDriver failure) + ( PreparedHead + , Elaborate failure (CanonicalTerm ObjectId) + ) +makeContextualTransparentHead location key parameters resultType body = do + (prepared, binders) <- + prepareParameters location key parameters resultType + let close = do + State.modify' \state -> + state + { elaborationBinders = binders + , elaborationContextualBinder = + Just (fromIntegral (length parameters)) + } + body' <- body + pure (foldr (const (CLam TySet)) body' parameters) + pure (prepared, close) + makePreparedHead :: Location -> SemanticGlobalKey @@ -1105,6 +1881,8 @@ compileExpression = \case location key compiled + Raw.ExprStructOp location symbol maybeArgument -> + compileStructureOperation location symbol maybeArgument Raw.ExprFiniteSet _location elements -> do compiled <- traverse compileExpressionAsSet elements pure @@ -1131,9 +1909,129 @@ compileExpression = \case Raw.ExprReplacePred location _value _variable _bound _predicate -> Except.throwError (ExactUnsupportedDeclarationBody location) - expression -> - Except.throwError - (ExactUnsupportedDeclarationBody (locate expression)) + +compileStructureOperation + :: Location + -> Raw.StructSymbol + -> Maybe Raw.Expr + -> Elaborate failure (CanonicalTerm ObjectId, CoreType) +compileStructureOperation location symbol maybeArgument = do + (argument, object) <- + case maybeArgument of + Just expression -> do + term <- compileExpressionAsSet expression + structures <- State.gets elaborationStructures + case termStructureAnnotation term structures of + Just annotation -> do + object <- + maybe + (Except.throwError + (ExactStructureOperationNotAvailable + location symbol)) + pure + (structureAnnotationOperation + symbol annotation) + pure (term, object) + Nothing -> do + object <- + resolveUniqueStructureOperation location symbol + pure (term, object) + Nothing -> do + structures <- State.gets elaborationStructures + case + [ (CBound index, object) + | (index, structure) <- Map.toAscList structures + , Just object <- + [structureAnnotationOperation symbol structure] + ] of + firstMatch : _ -> pure firstMatch + [] -> do + contextual <- State.gets elaborationContextualBinder + case contextual of + Nothing -> + Except.throwError + (ExactStructureOperationNotAvailable + location symbol) + Just index -> do + object <- + resolveUniqueStructureOperation + location symbol + recordContextualRequirement + location symbol object + pure (CBound index, object) + recordExactGlobal object (TyArrow TySet TySet) + pure (CApp (CGlobal object) argument, TySet) + where + termStructureAnnotation term structures = + case term of + CBound index -> Map.lookup index structures + _ -> Nothing + +resolveUniqueStructureOperation + :: Location + -> Raw.StructSymbol + -> Elaborate failure ObjectId +resolveUniqueStructureOperation location symbol = do + objects <- + State.lift + (Except.lift + (Declaration.resolveVisibleStructureOperationObjectsDriver + symbol)) + case objects of + [] -> + Except.throwError + (ExactStructureOperationNotAvailable location symbol) + [object] -> pure object + _ -> + Except.throwError + (ExactStructureOperationAmbiguous location symbol objects) + +recordContextualRequirement + :: Location + -> Raw.StructSymbol + -> ObjectId + -> Elaborate failure () +recordContextualRequirement location symbol object = do + existing <- + State.gets + (Map.lookup symbol . elaborationContextualRequirements) + case existing of + Nothing -> + State.modify' \state -> + state + { elaborationContextualRequirements = + Map.insert symbol object + (elaborationContextualRequirements state) + } + Just actual + | actual == object -> pure () + | otherwise -> + Except.throwError + (ExactContextualRequirementConflict + location symbol actual object) + +structureCarrierCast + :: Location + -> CanonicalTerm ObjectId + -> Elaborate failure (CanonicalTerm ObjectId) +structureCarrierCast location term = + case term of + CBound index -> do + annotation <- State.gets (Map.lookup index . elaborationStructures) + case annotation of + Nothing -> pure term + Just structure -> do + carrier <- + maybe + (Except.throwError + (ExactStructureOperationNotAvailable + location Raw.CarrierSymbol)) + pure + (structureAnnotationOperation + Raw.CarrierSymbol structure) + recordExactGlobal carrier (TyArrow TySet TySet) + pure (CApp (CGlobal carrier) term) + _ -> pure term compileReplacement :: Raw.Expr @@ -1215,9 +2113,22 @@ compileStatement = \case _location quantifier variables bound suchThat statement -> compileSymbolicQuantified quantifier variables bound suchThat (compileStatement statement) - statement -> - Except.throwError - (ExactUnsupportedDeclarationBody (locate statement)) + Raw.StmtStruct term rawPhrase -> do + subject <- compileTermAsSet term + annotation <- + resolveStructureAnnotation (locate term) rawPhrase + predicate <- + maybe + (impossible "an assertable structure has no predicate") + pure + (structureAnnotationPredicate annotation) + recordExactGlobal + predicate + (TyArrow TySet TyProp) + pure + (CApp + (CGlobal predicate) + subject) compileQuantifiedTermSubject :: Raw.Quantifier @@ -1291,6 +2202,10 @@ compileAtomicRelationTerms left relation right = (Raw.relationSymbolToken symbol) (Raw.relationSymbolParameterArity symbol) compiledParameters <- traverse compileExpressionAsSet parameters + checkedRight <- + if symbol == Raw.ElementSymbol && null parameters + then structureCarrierCast location right + else pure right case fixedSemanticMeaning key of Just FixedEquality | null parameters -> pure (CEq TySet left right) @@ -1304,7 +2219,7 @@ compileAtomicRelationTerms left relation right = (CIntrinsic intrinsic) (coreIntrinsicType intrinsic) ((\term -> (term, TySet)) - <$> (compiledParameters <> [left, right])) + <$> (compiledParameters <> [left, checkedRight])) unless (actual == TyProp) (Except.throwError (ExactFormulaExpectedProposition location actual)) @@ -1316,7 +2231,7 @@ compileAtomicRelationTerms left relation right = (CIntrinsic intrinsic) (coreIntrinsicType intrinsic) ((\term -> (term, TySet)) - <$> (compiledParameters <> [left, right])) + <$> (compiledParameters <> [left, checkedRight])) unless (actual == TyProp) (Except.throwError (ExactFormulaExpectedProposition location actual)) @@ -1326,7 +2241,7 @@ compileAtomicRelationTerms left relation right = applyResolvedTyped location key ((\term -> (term, TySet)) - <$> (compiledParameters <> [left, right])) + <$> (compiledParameters <> [left, checkedRight])) unless (actual == TyProp) (Except.throwError (ExactFormulaExpectedProposition location actual)) @@ -1562,11 +2477,22 @@ withAnonymousSetBinder -> Elaborate failure value withAnonymousSetBinder action = do outer <- State.gets elaborationBinders + outerStructures <- State.gets elaborationStructures + outerContextual <- State.gets elaborationContextualBinder State.modify' \state -> - state{elaborationBinders = (+ 1) <$> outer} + state + { elaborationBinders = (+ 1) <$> outer + , elaborationStructures = + Map.mapKeysMonotonic (+ 1) outerStructures + , elaborationContextualBinder = (+ 1) <$> outerContextual + } result <- action (CBound 0) State.modify' \state -> - state{elaborationBinders = outer} + state + { elaborationBinders = outer + , elaborationStructures = outerStructures + , elaborationContextualBinder = outerContextual + } pure result withSetBinders @@ -1575,6 +2501,8 @@ withSetBinders -> Elaborate failure value withSetBinders variables action = do outer <- State.gets elaborationBinders + outerStructures <- State.gets elaborationStructures + outerContextual <- State.gets elaborationContextualBinder case firstDuplicate (toList variables) of Just duplicate -> Except.throwError @@ -1599,10 +2527,18 @@ withSetBinders variables action = do State.modify' \state -> state { elaborationBinders = introduced <> shifted + , elaborationStructures = + Map.mapKeysMonotonic (+ binderCount) outerStructures + , elaborationContextualBinder = + (+ binderCount) <$> outerContextual } result <- action State.modify' \state -> - state{elaborationBinders = outer} + state + { elaborationBinders = outer + , elaborationStructures = outerStructures + , elaborationContextualBinder = outerContextual + } pure result compileFormula @@ -1930,6 +2866,54 @@ applyResolvedTyped location key arguments = do _ -> impossible "validated transparent expansion has opaque content" + ContextualTransparentExpansion _identity requirements -> + case content of + TransparentObjectContent _theory coreType body -> do + State.modify' \state -> + state + { elaborationGlobals = + Map.union + dependencies + (elaborationGlobals state) + } + contextArgument <- + resolveContextualExpansionArgument + location key requirements + applyExpandedTyped + location body coreType + ((contextArgument, TySet) : arguments) + _ -> + impossible + "validated contextual expansion has opaque content" + +resolveContextualExpansionArgument + :: Location + -> SemanticGlobalKey + -> Map.Map Raw.StructSymbol ObjectId + -> Elaborate failure (CanonicalTerm ObjectId) +resolveContextualExpansionArgument location key requirements = do + contextual <- State.gets elaborationContextualBinder + case contextual of + Just index -> do + traverse_ + (uncurry (recordContextualRequirement location)) + (Map.toAscList requirements) + pure (CBound index) + Nothing -> do + structures <- State.gets elaborationStructures + case + [ CBound index + | (index, structure) <- Map.toAscList structures + , all + (\(symbol, object) -> + structureAnnotationOperation symbol structure + == Just object) + (Map.toAscList requirements) + ] of + firstMatch : _ -> pure firstMatch + [] -> + Except.throwError + (ExactContextualExpansionNotAvailable location key) applyExpandedTyped :: Location @@ -2093,6 +3077,13 @@ encodePreparedSyntax TransparentBody canonical -> do putCacheTag 0x01 putCanonicalTermCache putObjectIdCache canonical + ContextualTransparentBody requirements canonical -> do + putCacheTag 0x02 + putCanonicalCacheMap + (\(Raw.StructSymbol symbol) -> putCacheText symbol) + putObjectIdCache + requirements + putCanonicalTermCache putObjectIdCache canonical putCacheMaybe (putCacheText . semanticNameText) alias diff --git a/source/Checking/Exact/Global.hs b/source/Checking/Exact/Global.hs index 848b600..094255e 100644 --- a/source/Checking/Exact/Global.hs +++ b/source/Checking/Exact/Global.hs @@ -33,6 +33,7 @@ data ExactGlobalResolutionError = ExactGlobalNotVisible !Internal.Symbol | ExactGlobalAmbiguous !Internal.Symbol | ExactGlobalUnsupported !Internal.Symbol + | ExactGlobalContextualUnsupported !Internal.Symbol | ExactGlobalContentInvalid !CoreCheckError deriving stock (Show, Eq) @@ -71,7 +72,7 @@ resolveExactSourceGlobals symbols = throwError (ExactGlobalNotVisible symbol) [match] -> do (source, sourceTypes) <- - liftEither (prepareSourceGlobal match) + liftEither (prepareSourceGlobal symbol match) pure ( Map.insert symbol source resolved , Map.union sourceTypes types @@ -80,14 +81,15 @@ resolveExactSourceGlobals symbols = throwError (ExactGlobalAmbiguous symbol) prepareSourceGlobal - :: ( SemanticGlobalTarget + :: Internal.Symbol + -> ( SemanticGlobalTarget , ObjectContent , Map.Map ObjectId CoreType ) -> Either ExactGlobalResolutionError (Typed.SourceGlobal ObjectId, Map.Map ObjectId CoreType) -prepareSourceGlobal (target, content, dependencies) = do +prepareSourceGlobal symbol (target, content, dependencies) = do body <- case target of GlobalReference _identity -> @@ -103,6 +105,8 @@ prepareSourceGlobal (target, content, dependencies) = do _ -> impossible "validated transparent expansion has opaque content" + ContextualTransparentExpansion _identity _requirements -> + Left (ExactGlobalContextualUnsupported symbol) let identity = semanticGlobalTargetObject target types = Map.insert diff --git a/source/Checking/Exact/Inductive.hs b/source/Checking/Exact/Inductive.hs index c3f281c..e873f0c 100644 --- a/source/Checking/Exact/Inductive.hs +++ b/source/Checking/Exact/Inductive.hs @@ -500,6 +500,8 @@ exactGlobalError location = \case ExactInductiveGlobalAmbiguous location symbol ExactGlobal.ExactGlobalUnsupported symbol -> ExactInductiveUnsupportedSymbol location symbol + ExactGlobal.ExactGlobalContextualUnsupported symbol -> + ExactInductiveUnsupportedSymbol location symbol ExactGlobal.ExactGlobalContentInvalid failure -> ExactInductiveGlobalContentInvalid location failure diff --git a/source/Checking/Exact/Proof.hs b/source/Checking/Exact/Proof.hs index b66ebfe..ad95a62 100644 --- a/source/Checking/Exact/Proof.hs +++ b/source/Checking/Exact/Proof.hs @@ -63,6 +63,8 @@ data ExactProofError | ExactProofExpectedImplicationGoal !Location | ExactProofGoalStatementMismatch !Location | ExactProofContradictionGoalMismatch !Location + | ExactProofLocalFunctionBinderMismatch !Location + | ExactProofLocalFunctionNameConflict !Location | ExactProofUnknownReference !Location !Raw.Marker | ExactProofElaborationFailed !Exact.ExactCompileError | ExactProofObligationPreparationFailed @@ -91,6 +93,8 @@ exactProofErrorLocation = \case ExactProofExpectedImplicationGoal location -> location ExactProofGoalStatementMismatch location -> location ExactProofContradictionGoalMismatch location -> location + ExactProofLocalFunctionBinderMismatch location -> location + ExactProofLocalFunctionNameConflict location -> location ExactProofUnknownReference location _marker -> location ExactProofElaborationFailed failure -> Exact.exactCompileErrorLocation failure @@ -131,6 +135,10 @@ renderExactProofError = \case at location <> "the proof step does not match the current goal" ExactProofContradictionGoalMismatch location -> at location <> "contradiction requires falsum as the current goal" + ExactProofLocalFunctionBinderMismatch location -> + at location <> "the function argument must match its domain binder" + ExactProofLocalFunctionNameConflict location -> + at location <> "the function and argument names must be distinct" ExactProofUnknownReference location marker -> at location <> "the cited fact " <> shown marker <> " is not visible" ExactProofElaborationFailed failure -> @@ -210,6 +218,11 @@ data PreparedProof !(ScopedCheckedCore ObjectId) !(ScopedCheckedCore ObjectId) !PreparedProof + | PreparedDefineFunction + !Exact.ExactLocalId + !(ScopedCheckedCore ObjectId) + !(ScopedCheckedCore ObjectId) + !PreparedProof | PreparedContradiction !PreparedDischarge data PreparedExactProof = PreparedExactProof @@ -277,6 +290,7 @@ prepareExactProof block explicitProof = openEnvelopeVariables targetCore (Exact.preparedExactClaimVariables envelope) + (Exact.preparedExactClaimContext envelope) (locals, bodyGoal, antecedents) <- openEnvelopeAntecedents context @@ -410,20 +424,31 @@ prepareFinalPreludeFoundationClaim foundation block explicitProof = openEnvelopeVariables :: ScopedCheckedCore ObjectId -> [Raw.VarSymbol] + -> Exact.ExactBinderContext -> Prepare failure ( Exact.ExactBinderContext , ScopedCheckedCore ObjectId , [Exact.ExactLocalId] ) -openEnvelopeVariables target variables = +openEnvelopeVariables target variables preparedContext = case NonEmpty.nonEmpty variables of Nothing -> - pure (Exact.emptyExactBinderContext, target, []) - Just nonempty -> - openFixedVariables + pure (preparedContext, target, []) + Just nonempty -> do + (_unannotated, opened, identities) <- + openFixedVariables Exact.emptyExactBinderContext target nonempty + let expected = + reverse + (fst <$> toList + (Exact.exactBinderContextSupport preparedContext)) + unless + (identities == expected) + (impossible + "prepared claim annotations do not match opened binders") + pure (preparedContext, opened, identities) openEnvelopeAntecedents :: Exact.ExactBinderContext @@ -639,12 +664,16 @@ prepareProof fallback context locals inductionAntecedents goal = \case (Exact.extendExactBinderContext ((identity, variable) :| []) context) + separationCharacteristic <- + liftDriver + (Declaration.currentFoundationAxiomDriver + SeparationCharacteristic) definition <- maybe (impossible "an exact set expression did not form a local definition") pure - (scopedSetDefinition body) + (scopedSetDefinition separationCharacteristic body) local <- allocateLocal ExactLocalDefinition context' definition PreparedDefine identity body definition @@ -655,6 +684,65 @@ prepareProof fallback context locals inductionAntecedents goal = \case Nothing (weakenCheckedScopedCore TySet goal) continuation + Raw.DefineFunction + location function argument value bound domain continuation -> do + unless (argument == bound) + (throwProof + (ExactProofLocalFunctionBinderMismatch (locate bound))) + when (function == argument) + (throwProof + (ExactProofLocalFunctionNameConflict (locate function))) + argumentIdentity <- allocateLocalIdentity + argumentContext <- + either + (throwProof . ExactProofElaborationFailed) + pure + (Exact.extendExactBinderContext + ((argumentIdentity, argument) :| []) + context) + graph <- + liftDriver + (Exact.prepareExactLocalFunctionGraph + location context argumentContext domain value) + >>= either + (throwProof . ExactProofElaborationFailed) + pure + functionIdentity <- allocateLocalIdentity + functionContext <- + either + (throwProof . ExactProofElaborationFailed) + pure + (Exact.extendExactBinderContext + ((functionIdentity, function) :| []) + context) + replacementCharacteristic <- + liftDriver + (Declaration.currentFoundationAxiomDriver + ReplacementCharacteristic) + definition <- + maybe + (impossible + "a checked replacement graph did not form a local definition") + pure + (scopedCharacteristicDefinition + replacementCharacteristic + (Exact.preparedExactLocalFunctionGraphCore graph) + ( Exact.preparedExactLocalFunctionGraphDomain graph + :| [Exact.preparedExactLocalFunctionGraphMap graph] + )) + local <- + allocateLocal ExactLocalDefinition functionContext definition + PreparedDefineFunction + functionIdentity + (Exact.preparedExactLocalFunctionGraphCore graph) + definition + <$> prepareProof + fallback + functionContext + (locals <> [local]) + Nothing + (weakenCheckedScopedCore TySet goal) + continuation Raw.Contradiction location justification -> do unless ( scopedCoreType goal == TyProp @@ -978,6 +1066,8 @@ preparedProofFirstOmission = \case <|> preparedProofFirstOmission continuation PreparedDefine _identity _body _definition continuation -> preparedProofFirstOmission continuation + PreparedDefineFunction _identity _graph _definition continuation -> + preparedProofFirstOmission continuation PreparedContradiction{} -> Nothing executePreparedProof @@ -1007,6 +1097,8 @@ executePreparedProof = \case executePreparedProof continuation PreparedDefine _identity _body _definition continuation -> executePreparedProof continuation + PreparedDefineFunction _identity _graph _definition continuation -> + executePreparedProof continuation PreparedContradiction discharge -> executeDischarge discharge @@ -1077,6 +1169,12 @@ putPreparedProof = \case PreparedContradiction discharge -> do putCacheTag 0x0a putPreparedDischarge discharge + PreparedDefineFunction identity graph definition continuation -> do + putCacheTag 0x0b + putCacheNatural (Exact.exactLocalIdValue identity) + putScopedTerm graph + putScopedProposition definition + putPreparedProof continuation putPreparedDischarge :: PreparedDischarge -> CachePut putPreparedDischarge diff --git a/source/Checking/Facts.hs b/source/Checking/Facts.hs deleted file mode 100644 index b365e1e..0000000 --- a/source/Checking/Facts.hs +++ /dev/null @@ -1,340 +0,0 @@ -{-# LANGUAGE NoImplicitPrelude #-} - -module Checking.Facts - ( PreparedSemanticFact - , prepareSemanticFact - , preparedSemanticStatement - , preparedSemanticDependencies - , FactOrigin - , factOrigin - , factOriginLocation - , factOriginBlock - , StagedFact - , stageFact - , stagedFactAliases - , stagedFactOrigin - , stagedFactSemantic - , FactRegistry - , emptyFactRegistry - , registerStagedFacts - , lookupPreparedFact - , lookupFactOrigin - , registeredFacts - , registeredFactsWithOrigins - , factRegistryExtension - , restrictFactRegistry - , partitionFactRegistry - , factRegistryInvariant - ) where - -import Base -import Report.Location -import Syntax.Internal - -import Data.List qualified as List -import Data.List.NonEmpty qualified as NonEmpty -import Data.Map.Strict qualified as Map -import Data.Set qualified as Set - - --- | A checked fact before aliases and diagnostic provenance are attached. --- This is the complete long-lived semantic row. -data PreparedSemanticFact = PreparedSemanticFact - { preparedSemanticStatement :: !Formula - , preparedSemanticDependencies :: !(Set Symbol) - } - deriving (Show, Eq) - -prepareSemanticFact :: Formula -> PreparedSemanticFact -prepareSemanticFact statement = - PreparedSemanticFact - { preparedSemanticStatement = statement - , preparedSemanticDependencies = mentionedSymbols statement - } - -data FactOrigin = FactOrigin - { factOriginLocation :: !Location - , factOriginBlock :: !Marker - } - deriving (Show, Eq) - -factOrigin :: Location -> Marker -> FactOrigin -factOrigin = FactOrigin - --- | Registration data for one semantic fact. -data StagedFact = StagedFact - { stagedFactAliases :: !(NonEmpty Marker) - , stagedFactOrigin :: !FactOrigin - , stagedFactSemantic :: !PreparedSemanticFact - } - deriving (Show, Eq) - -stageFact - :: NonEmpty Marker - -> FactOrigin - -> PreparedSemanticFact - -> StagedFact -stageFact = StagedFact - -newtype FactHandle = FactHandle - { unFactHandle :: Int - } - deriving (Show, Eq, Ord) - -data FactRegistration = FactRegistration - { factRegistrationAliases :: !(NonEmpty Marker) - , factRegistrationOrigin :: !FactOrigin - } - deriving (Show, Eq) - --- | Semantic rows and their registration sidecars share only a private handle. -data FactRegistry = FactRegistry - { factOrder :: ![FactHandle] - , factRows :: !(Map FactHandle PreparedSemanticFact) - , factRegistrations :: !(Map FactHandle FactRegistration) - , factAliases :: !(Map Marker FactHandle) - , nextFactHandle :: !Int - } - deriving (Show, Eq) - -emptyFactRegistry :: FactRegistry -emptyFactRegistry = - FactRegistry - { factOrder = [] - , factRows = mempty - , factRegistrations = mempty - , factAliases = mempty - , nextFactHandle = 0 - } - -registerStagedFacts - :: NonEmpty StagedFact - -> FactRegistry - -> Either Marker FactRegistry -registerStagedFacts staged registry = - case firstDuplicateAlias (Map.keysSet (factAliases registry)) aliases of - Just duplicate -> - Left duplicate - Nothing -> - Right - registry - { factOrder = handles <> factOrder registry - , factRows = - Map.union - (Map.fromList - [ (handle, stagedFactSemantic fact) - | (handle, fact) <- registrations - ]) - (factRows registry) - , factRegistrations = - Map.union - (Map.fromList - [ ( handle - , FactRegistration - { factRegistrationAliases = - stagedFactAliases fact - , factRegistrationOrigin = - stagedFactOrigin fact - } - ) - | (handle, fact) <- registrations - ]) - (factRegistrations registry) - , factAliases = - Map.union - (Map.fromList - [ (alias, handle) - | (handle, fact) <- registrations - , alias <- - NonEmpty.toList (stagedFactAliases fact) - ]) - (factAliases registry) - , nextFactHandle = - nextFactHandle registry + length stagedList - } - where - stagedList = NonEmpty.toList staged - handles = - FactHandle <$> - [ nextFactHandle registry - .. nextFactHandle registry + length stagedList - 1 - ] - registrations = zip handles stagedList - aliases = - concatMap - (NonEmpty.toList . stagedFactAliases) - stagedList - -lookupPreparedFact :: Marker -> FactRegistry -> Maybe PreparedSemanticFact -lookupPreparedFact marker registry = do - handle <- Map.lookup marker (factAliases registry) - Map.lookup handle (factRows registry) - -lookupFactOrigin :: Marker -> FactRegistry -> Maybe FactOrigin -lookupFactOrigin marker registry = do - handle <- Map.lookup marker (factAliases registry) - factRegistrationOrigin - <$> Map.lookup handle (factRegistrations registry) - --- | Facts in checker premise order, paired with their primary aliases. -registeredFacts :: FactRegistry -> [(Marker, PreparedSemanticFact)] -registeredFacts registry = - [ (marker, semantic) - | (marker, semantic, _origin) <- - registeredFactsWithOrigins registry - ] - --- | Facts in checker premise order with their registration provenance. -registeredFactsWithOrigins - :: FactRegistry - -> [(Marker, PreparedSemanticFact, FactOrigin)] -registeredFactsWithOrigins registry = - [ (primaryAlias registration, semantic, factRegistrationOrigin registration) - | handle <- factOrder registry - , Just registration <- [Map.lookup handle (factRegistrations registry)] - , Just semantic <- [Map.lookup handle (factRows registry)] - ] - where - primaryAlias = - NonEmpty.head . factRegistrationAliases - --- | Recover the source-ordered facts appended to one registry. --- --- The first registry must be an unchanged prefix of the second. -factRegistryExtension - :: FactRegistry - -> FactRegistry - -> Either Text [StagedFact] -factRegistryExtension previous current - | nextFactHandle current < nextFactHandle previous = - Left "fact registry handle counter moved backwards" - | Map.restrictKeys - (factRows current) - previousHandles - /= factRows previous = - Left "fact registry changed an existing semantic row" - | Map.restrictKeys - (factRegistrations current) - previousHandles - /= factRegistrations previous = - Left "fact registry changed an existing registration" - | Map.restrictKeys - (factAliases current) - previousAliases - /= factAliases previous = - Left "fact registry changed an existing alias" - | factOrder current - /= extensionHandles <> factOrder previous = - Left "fact registry extension changed premise order" - | otherwise = - traverse staged extensionHandles - where - previousHandles = - Map.keysSet (factRows previous) - previousAliases = - Map.keysSet (factAliases previous) - extensionHandles = - FactHandle <$> - [ nextFactHandle previous - .. nextFactHandle current - 1 - ] - - staged handle = do - semantic <- - maybe - (Left "fact registry extension is missing a semantic row") - Right - (Map.lookup handle (factRows current)) - registration <- - maybe - (Left "fact registry extension is missing a registration") - Right - (Map.lookup handle (factRegistrations current)) - pure - (StagedFact - (factRegistrationAliases registration) - (factRegistrationOrigin registration) - semantic) - -restrictFactRegistry - :: NonEmpty Marker - -> FactRegistry - -> Either Marker FactRegistry -restrictFactRegistry markers registry = do - handles <- traverse resolveHandle markers - pure (registryForHandles (orderedUnique (NonEmpty.toList handles)) registry) - where - resolveHandle marker = - maybe (Left marker) Right (Map.lookup marker (factAliases registry)) - -partitionFactRegistry - :: NonEmpty Marker - -> FactRegistry - -> Either Marker (FactRegistry, FactRegistry) -partitionFactRegistry markers registry = do - selected <- restrictFactRegistry markers registry - let selectedHandles = Set.fromList (factOrder selected) - selectedInRegistryOrder = - List.filter (`Set.member` selectedHandles) (factOrder registry) - unselectedHandles = - List.filter (`Set.notMember` selectedHandles) (factOrder registry) - pure - ( registryForHandles selectedInRegistryOrder registry - , registryForHandles unselectedHandles registry - ) - -factRegistryInvariant :: FactRegistry -> Bool -factRegistryInvariant registry = - length order == Set.size orderSet - && orderSet == Map.keysSet (factRows registry) - && orderSet == Map.keysSet (factRegistrations registry) - && aliasCount == Map.size expectedAliases - && expectedAliases == factAliases registry - && all ((< nextFactHandle registry) . unFactHandle) order - where - order = factOrder registry - orderSet = Set.fromList order - aliasPairs = - [ (alias, handle) - | (handle, registration) <- - Map.toList (factRegistrations registry) - , alias <- - NonEmpty.toList (factRegistrationAliases registration) - ] - aliasCount = length aliasPairs - expectedAliases = Map.fromList aliasPairs - -registryForHandles :: [FactHandle] -> FactRegistry -> FactRegistry -registryForHandles handles registry = - registry - { factOrder = handles - , factRows = Map.restrictKeys (factRows registry) handleSet - , factRegistrations = - Map.restrictKeys (factRegistrations registry) handleSet - , factAliases = - Map.filter (`Set.member` handleSet) (factAliases registry) - } - where - handleSet = Set.fromList handles - -firstDuplicateAlias :: Set Marker -> [Marker] -> Maybe Marker -firstDuplicateAlias existing = - go mempty - where - go _seen [] = - Nothing - go seen (marker:rest) - | marker `Set.member` existing || marker `Set.member` seen = - Just marker - | otherwise = - go (Set.insert marker seen) rest - -orderedUnique :: Ord a => [a] -> [a] -orderedUnique = - reverse . snd . foldl' step (mempty, []) - where - step (seen, acc) value - | value `Set.member` seen = - (seen, acc) - | otherwise = - (Set.insert value seen, value : acc) diff --git a/source/Checking/FinalPrelude.hs b/source/Checking/FinalPrelude.hs index 1e05199..ac2a941 100644 --- a/source/Checking/FinalPrelude.hs +++ b/source/Checking/FinalPrelude.hs @@ -9,12 +9,15 @@ module Checking.FinalPrelude , finalPreludeSemantic , finalPreludePrefix , finalPreludeObjects + , PreludePublicRole(..) + , expectedFinalPreludePublicRoles , FinalPreludeRoleTarget(..) , finalPreludePublicRole , FinalPreludeValidationError(..) , FinalPreludeFailure(..) , FinalPreludeBuildResult(..) , buildFinalPreludeCandidate + , buildParsedFinalPreludeCandidate ) where import Base hiding (Empty) @@ -28,17 +31,19 @@ import Checking.Identity import Checking.Semantic import Checking.Semantic qualified as Semantic import Felix.Module -import Felix.Migration qualified as Migration import Felix.Parse import Felix.Prelude qualified as Prelude import Felix.Source (ImportRef) import Report.Location import Syntax.Abstract qualified as Raw import Syntax.Interface +import Syntax.Lexicon qualified as Lexicon import Control.Monad (unless) +import Data.Bifunctor (first) import Data.List qualified as List import Data.Map.Strict qualified as Map +import Data.Set qualified as Set data FinalPreludeCandidate = FinalPreludeCandidate @@ -47,7 +52,7 @@ data FinalPreludeCandidate = FinalPreludeCandidate !SemanticInterface !Declaration.PendingModulePrefix !CheckedObjectClosure - !(Map.Map Migration.PreludePublicRole FinalPreludeRoleTarget) + !(Map.Map PreludePublicRole FinalPreludeRoleTarget) finalPreludeParsed :: FinalPreludeCandidate @@ -94,9 +99,23 @@ data FinalPreludeRoleTarget | FinalPreludeTheoremRole !TheoremRef deriving stock (Show, Eq, Ord) +-- | Stable public roles exported by the packaged final prelude. +data PreludePublicRole + = PreludeInfinityTheorem + | PreludeOmegaObject + | PreludeOmegaDefiningEquation + | PreludeNaturalsAlias + | PreludeNaturalsInductiveTheorem + | PreludeNaturalsMinimalTheorem + deriving stock (Show, Eq, Ord, Enum, Bounded) + +expectedFinalPreludePublicRoles :: Set PreludePublicRole +expectedFinalPreludePublicRoles = + Set.fromList [minBound .. maxBound] + finalPreludePublicRole :: FinalPreludeCandidate - -> Migration.PreludePublicRole + -> PreludePublicRole -> Maybe FinalPreludeRoleTarget finalPreludePublicRole (FinalPreludeCandidate _parsed _syntax _semantic _prefix _objects @@ -115,7 +134,8 @@ data FinalPreludeValidationError | FinalPreludeFactContentMismatch !Text | FinalPreludeValidationInventoryMismatch !DeclarationSlot | FinalPreludeAuthorityMismatch !DeclarationSlot - | FinalPreludePublicRoleMismatch !Migration.PreludePublicRole + | FinalPreludeBaseStructureMismatch + | FinalPreludePublicRoleMismatch !PreludePublicRole deriving stock (Show, Eq) data FinalPreludeFailure @@ -157,7 +177,9 @@ buildFinalPreludeCandidate foundation resolver = buildParsedFinalPreludeCandidate foundation parsed resolver --- The packaged loader above is the only entry to final-candidate construction. +-- The production acquisition path establishes packaged provenance before +-- passing its already parsed source here. The explicit parsed seam avoids a +-- second load and parse on a cache miss. buildParsedFinalPreludeCandidate :: CheckedFoundation -> Prelude.ReservedParsedPrelude @@ -225,7 +247,7 @@ buildParsedFinalPreludeCandidate foundation parsed resolver = [] compileBlocks _blockIndex [] = - pure () + commitBaseStructure compileBlocks blockIndex (block : remaining) = case block of Raw.BlockClaim{} -> @@ -249,6 +271,39 @@ buildParsedFinalPreludeCandidate foundation parsed resolver = Declaration.failModuleDriver (FinalPreludeUnsupportedBlock (locate block)) + commitBaseStructure = do + slot <- Declaration.nextDeclarationSlotDriver + theory <- Declaration.currentTheoryDriver + let seed = + opaqueDeclarationSeed + (declarationSlotModule slot) + (declarationSlotOrdinal slot) + StructureDeclaration + (generatedObjectSlot 0) + coreType = TyArrow TySet TySet + content = OpaqueObjectContent theory seed coreType + identity = opaqueObjectId theory seed coreType + asserted = assertedObject identity content + structurePhrase = + semanticStructurePhrase Lexicon._Onesorted + operation = + semanticStructureOperation Raw.CarrierSymbol identity + descriptor <- + either + (Declaration.failModuleDriver + . FinalPreludeDeclarationFailed + . Declaration.DeclarationEnvironmentFailed) + pure + (semanticStructureDescriptor + structurePhrase Nothing [] [operation]) + void + (Declaration.commitCompiledDeclaration + (declarationSyntaxId + "felix-final-prelude-base-structure-v1") do + Declaration.addDeclarationObject asserted + Declaration.stageSemanticStructureDescriptor descriptor + Declaration.authorizeCompiledDeclaration (pure ())) + compileBinding blockIndex block = do prepared <- Exact.prepareExactDeclaration @@ -312,10 +367,12 @@ validateFinalPrelude -> CheckedObjectClosure -> Either FinalPreludeValidationError - (Map.Map Migration.PreludePublicRole FinalPreludeRoleTarget) + (Map.Map PreludePublicRole FinalPreludeRoleTarget) validateFinalPrelude foundation parsed semantic prefix objects = do - declarations <- associatePreludeDeclarations parsed prefix - validateConfinedAuthority foundation semantic objects declarations + (declarations, baseStructure) <- + associatePreludeDeclarations parsed prefix + validateConfinedAuthority + foundation semantic objects declarations baseStructure resolveAndValidatePublicRoles foundation objects declarations resolveAndValidatePublicRoles @@ -324,7 +381,7 @@ resolveAndValidatePublicRoles -> [PreludeDeclaration] -> Either FinalPreludeValidationError - (Map.Map Migration.PreludePublicRole FinalPreludeRoleTarget) + (Map.Map PreludePublicRole FinalPreludeRoleTarget) resolveAndValidatePublicRoles foundation objects declarations = do successor <- expectDefinition @@ -403,30 +460,30 @@ resolveAndValidatePublicRoles foundation objects declarations = do minimalOmega let roles = Map.fromList - [ ( Migration.PreludeInfinityTheorem + [ ( PreludeInfinityTheorem , FinalPreludeTheoremRole infinity ) - , ( Migration.PreludeOmegaObject + , ( PreludeOmegaObject , FinalPreludeObjectRole omegaId ) - , ( Migration.PreludeOmegaDefiningEquation + , ( PreludeOmegaDefiningEquation , FinalPreludeTheoremRole omegaEquation ) - , ( Migration.PreludeNaturalsAlias + , ( PreludeNaturalsAlias , FinalPreludeObjectRole omegaId ) - , ( Migration.PreludeNaturalsInductiveTheorem + , ( PreludeNaturalsInductiveTheorem , FinalPreludeTheoremRole naturalsInductive ) - , ( Migration.PreludeNaturalsMinimalTheorem + , ( PreludeNaturalsMinimalTheorem , FinalPreludeTheoremRole naturalsMinimal ) ] unless - (Map.keysSet roles == Migration.expectedFinalPreludePublicRoles) + (Map.keysSet roles == expectedFinalPreludePublicRoles) (Left (FinalPreludePublicRoleMismatch - Migration.PreludeInfinityTheorem)) + PreludeInfinityTheorem)) pure roles validatePackagedPreludeInput @@ -460,12 +517,19 @@ validatePackagedPreludeInput parsed syntax associatePreludeDeclarations :: Prelude.ReservedParsedPrelude -> Declaration.PendingModulePrefix - -> Either FinalPreludeValidationError [PreludeDeclaration] + -> Either + FinalPreludeValidationError + ([PreludeDeclaration], Declaration.CommittedDeclarationBatch) associatePreludeDeclarations parsed prefix = do - unless - (length sourceDeclarations == length batches) - (Left FinalPreludeDeclarationAssociationMismatch) - pure (zipWith PreludeDeclaration sourceDeclarations batches) + case List.splitAt (length sourceDeclarations) batches of + (sourceBatches, [baseStructure]) + | length sourceBatches == length sourceDeclarations -> + pure + ( zipWith PreludeDeclaration + sourceDeclarations sourceBatches + , baseStructure + ) + _ -> Left FinalPreludeDeclarationAssociationMismatch where sourceDeclarations = [ block @@ -483,8 +547,10 @@ validateConfinedAuthority -> SemanticInterface -> CheckedObjectClosure -> [PreludeDeclaration] + -> Declaration.CommittedDeclarationBatch -> Either FinalPreludeValidationError () -validateConfinedAuthority foundation semantic objects declarations = do +validateConfinedAuthority + foundation semantic objects declarations baseStructure = do unless ( semanticInterfaceOwner semantic == preludeModuleName && null (semanticInterfaceDirectInputs semantic) @@ -499,12 +565,68 @@ validateConfinedAuthority foundation semantic objects declarations = do (declarationBatch declaration)) ] traverse_ (validateDeclarationAuthority foundation objects) declarations + validateBaseStructure foundation objects baseStructure where requireTransparent identity = case lookupCheckedObjectContent identity objects of Just TransparentObjectContent{} -> pure () _ -> Left (FinalPreludeUnexpectedObject identity) +validateBaseStructure + :: CheckedFoundation + -> CheckedObjectClosure + -> Declaration.CommittedDeclarationBatch + -> Either FinalPreludeValidationError () +validateBaseStructure foundation objects batch = do + let slot = Declaration.committedBatchSlot batch + delta = Declaration.committedBatchDelta batch + environment = declarationDeltaEnvironment delta + structurePhrase = semanticStructurePhrase Lexicon._Onesorted + expectedSeed = + opaqueDeclarationSeed + (declarationSlotModule slot) + (declarationSlotOrdinal slot) + StructureDeclaration + (generatedObjectSlot 0) + expectedType = TyArrow TySet TySet + expectedObject = opaqueObjectId (theoryId foundation) expectedSeed expectedType + expectedContent = + OpaqueObjectContent + (theoryId foundation) + expectedSeed + expectedType + descriptor <- + case semanticEnvironmentStructures environment of + [single] -> Right single + _ -> Left FinalPreludeBaseStructureMismatch + expectedDescriptor <- + first (const FinalPreludeBaseStructureMismatch) + (semanticStructureDescriptor + structurePhrase + Nothing + [] + [semanticStructureOperation Raw.CarrierSymbol expectedObject]) + unless + ( declarationSlotModule slot == preludeModuleName + && descriptor == expectedDescriptor + && null (semanticEnvironmentBindings environment) + && declarationDeltaObjects delta == [expectedObject] + && null (declarationDeltaFacts delta) + && null (declarationDeltaAliases delta) + && null (declarationDeltaPropositions delta) + && Declaration.committedBatchObjects batch + == [assertedObject expectedObject expectedContent] + && null (Declaration.committedBatchPropositions batch) + && null (Declaration.committedBatchProofValidations batch) + && maybe + False + (null . declarationValidationRecordCertificates) + (Declaration.committedBatchDeclarationValidation batch) + && lookupCheckedObjectContent expectedObject objects + == Just expectedContent + ) + (Left FinalPreludeBaseStructureMismatch) + validateDeclarationAuthority :: CheckedFoundation -> CheckedObjectClosure diff --git a/source/Checking/Legacy.hs b/source/Checking/Legacy.hs deleted file mode 100644 index 7c7bbb4..0000000 --- a/source/Checking/Legacy.hs +++ /dev/null @@ -1,1788 +0,0 @@ -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE NoImplicitPrelude #-} - --- | Disposable H1 vocabulary for the legacy checker. --- --- These values exist only for one checking invocation. They are neither final --- typed identities nor persistent authorization. -module Checking.Legacy - ( LegacyModuleOrdinal - , legacyModuleOrdinal - , legacyModuleOrdinalValue - , LegacyLocalFactOrdinal - , legacyLocalFactOrdinal - , legacyLocalFactOrdinalValue - , LegacyFactRef - , legacyFactRef - , legacyFactModule - , legacyFactLocalOrdinal - , LegacyModuleAssignment - , assignLegacyModuleOrdinals - , assignedLegacyModuleOrdinal - , assignedParsedModule - , LegacyLocalAssumptionOrdinal - , legacyLocalAssumptionOrdinal - , legacyLocalAssumptionOrdinalValue - , LegacyObligationOrdinal - , legacyObligationOrdinal - , legacyObligationOrdinalValue - , SessionLegacyObligationRef - , sessionLegacyObligationRef - , AssumptionKind(..) - , LegacyPreparedProposition - , prepareLegacyProposition - , legacyPreparedFormula - , LegacyDirectAxiomManifestEntry - , SessionLegacyDeclaredAssumptionRef - , LegacySemanticFact - , legacySemanticFact - , legacySemanticProposition - , LegacyTheoremFinalizationRole(..) - , LegacyDefinitionFactRole(..) - , LegacyDatatypeFactRole(..) - , LegacyStructureFactRole(..) - , LegacyInductiveFactRole(..) - , LegacyRuleTag(..) - , LegacyFactProducer(..) - , LegacyRulePredecessor - , legacyRuleFactPredecessor - , legacyRuleObligationPredecessor - , CheckedLegacyRuleApplication - , VampireLoweringAssumption(..) - , mandatoryVampireLoweringAssumptions - , SessionLegacyTrustedVampireUse - , SessionLegacyGapUse - , SessionLegacyRuleUse - , LegacyTrustDependencies - , emptyLegacyTrustDependencies - , legacyTrustedVampireTrust - , legacyGapTrust - , legacyDeclaredAssumptionUses - , legacyTrustedVampireUses - , legacyExplicitGaps - , legacyGapLocations - , trustedLegacyRuleUses - , legacyVampireLoweringUses - , SessionLegacyTrustedVampireEvidence - , SessionLegacyGapEvidence - , LegacyFactAuthorization - , legacyAuthorizationTrustDependencies - , H1LegacyFactAuthorization - , LegacyAdmittedFact - , H1LegacyAdmittedFact - , SymbolOwnerKind(..) - , SymbolOwner(..) - , LegacyCheckingEnvironment - , legacyCheckingEnvironment - , legacyEnvironmentAbbreviations - , legacyEnvironmentPredicateDefinitions - , legacyEnvironmentDependencies - , legacyEnvironmentOwnedSymbols - , legacyEnvironmentOwnedSymbolMarkers - , legacyEnvironmentFrozenSymbols - , legacyEnvironmentStructs - , legacyEnvironmentDefinedMarkers - , LegacyImportedView - , emptyLegacyImportedView - , legacyImportedView - , legacyImportedModuleOrdinals - , legacyImportedCheckingEnvironment - , LegacyModuleStage - , openLegacyModuleStage - , legacyStageModuleOrdinal - , legacyStageSourceAddress - , legacyStageVisibleFacts - , legacyStageLocalFacts - , legacyStageFactRegistry - , legacyStageDirectAxiomManifest - , legacyStageImportedCheckingEnvironment - , lookupLegacyStageFact - , LegacyFactEntry - , legacyFactEntryReference - , legacyFactEntryStagedFact - , legacyFactEntryAdmittedFact - , legacyFactEntryTrustDependencies - , LegacyReservedFact - , legacyReservedFactReference - , legacyReservedStagedFact - , LegacyDeclarationReservation - , reserveLegacyDeclaration - , legacyReservedFacts - , appendEstablishedLegacyDeclaration - , authorizeLegacyDeclaredAssumption - , authorizeLegacyTrustedVampire - , authorizeLegacyGap - , authorizeLegacyRule - , LegacyAdmittedModule - , sealLegacyModuleStage - , legacyAdmittedModuleOrdinal - , legacyAdmittedSourceAddress - , legacyAdmittedDirectImports - , legacyAdmittedVisibleFacts - , legacyAdmittedLocalFacts - , legacyAdmittedFactRegistry - , legacyAdmittedDirectAxiomManifest - , legacyAdmittedTrustDependencies - , legacyAdmittedCheckingEnvironment - , LegacyModuleStageError(..) - ) where - -import Base -import Checking.Facts qualified as Facts -import Checking.Legacy.Environment -import Felix.Parse - ( ParsedModule - , ParsedSourceWorkspace - , parsedModuleAddress - , parsedWorkspaceImportedBeforeImporter - ) -import Felix.Source (ResolvedSourceAddress) -import Provers (AcceptedVampireRun) -import Report.Location -import Syntax.Internal - -import Control.Monad (foldM, unless) -import Data.Bifunctor (first) -import Data.List.NonEmpty qualified as NonEmpty -import Data.Map.Strict qualified as Map -import Data.Set qualified as Set -import Data.Vector (Vector) -import Data.Vector qualified as Vector -import Data.Word (Word32) -import Numeric.Natural (Natural) - - --- | Dense invocation-local module position. -newtype LegacyModuleOrdinal = LegacyModuleOrdinal Word32 - deriving stock (Show, Eq, Ord) - -legacyModuleOrdinal :: Word32 -> LegacyModuleOrdinal -legacyModuleOrdinal = LegacyModuleOrdinal - -legacyModuleOrdinalValue :: LegacyModuleOrdinal -> Word32 -legacyModuleOrdinalValue (LegacyModuleOrdinal ordinal) = - ordinal - - --- | Dense invocation-local fact position within one module. -newtype LegacyLocalFactOrdinal = LegacyLocalFactOrdinal Word32 - deriving stock (Show, Eq, Ord) - -legacyLocalFactOrdinal :: Word32 -> LegacyLocalFactOrdinal -legacyLocalFactOrdinal = LegacyLocalFactOrdinal - -legacyLocalFactOrdinalValue :: LegacyLocalFactOrdinal -> Word32 -legacyLocalFactOrdinalValue (LegacyLocalFactOrdinal ordinal) = - ordinal - - -data LegacyFactRef = LegacyFactRef - !LegacyModuleOrdinal - !LegacyLocalFactOrdinal - deriving stock (Show, Eq, Ord) - -legacyFactRef - :: LegacyModuleOrdinal - -> LegacyLocalFactOrdinal - -> LegacyFactRef -legacyFactRef = LegacyFactRef - -legacyFactModule :: LegacyFactRef -> LegacyModuleOrdinal -legacyFactModule (LegacyFactRef moduleOrdinal _factOrdinal) = - moduleOrdinal - -legacyFactLocalOrdinal :: LegacyFactRef -> LegacyLocalFactOrdinal -legacyFactLocalOrdinal (LegacyFactRef _moduleOrdinal factOrdinal) = - factOrdinal - - --- | One parsed module paired with its dense invocation-local position. -data LegacyModuleAssignment = LegacyModuleAssignment - !LegacyModuleOrdinal - !ParsedModule - -assignedLegacyModuleOrdinal - :: LegacyModuleAssignment - -> LegacyModuleOrdinal -assignedLegacyModuleOrdinal - (LegacyModuleAssignment ordinal _parsedModule) = - ordinal - -assignedParsedModule :: LegacyModuleAssignment -> ParsedModule -assignedParsedModule - (LegacyModuleAssignment _ordinal parsedModule) = - parsedModule - --- | Assign module ordinals in imported-before-importer source order. -assignLegacyModuleOrdinals - :: ParsedSourceWorkspace - -> Either LegacyModuleStageError (NonEmpty LegacyModuleAssignment) -assignLegacyModuleOrdinals workspace - | moduleCountInteger > legacyModuleCapacity = - Left - (LegacyModuleOrdinalSpaceExhausted - (fromIntegral moduleCount)) - | otherwise = - Right - (NonEmpty.zipWith - (\ordinal parsedModule -> - LegacyModuleAssignment - (legacyModuleOrdinal - (fromIntegral ordinal)) - parsedModule) - ((0 :| [1 ..]) :: NonEmpty Integer) - modules) - where - modules = - parsedWorkspaceImportedBeforeImporter workspace - parsedModules = - NonEmpty.toList modules - moduleCount = - length parsedModules - moduleCountInteger = - toInteger moduleCount - legacyModuleCapacity = - toInteger (maxBound :: Word32) + 1 - - -newtype LegacyLocalAssumptionOrdinal = - LegacyLocalAssumptionOrdinal Natural - deriving stock (Show, Eq, Ord) - -legacyLocalAssumptionOrdinal - :: Natural - -> LegacyLocalAssumptionOrdinal -legacyLocalAssumptionOrdinal = LegacyLocalAssumptionOrdinal - -legacyLocalAssumptionOrdinalValue - :: LegacyLocalAssumptionOrdinal - -> Natural -legacyLocalAssumptionOrdinalValue - (LegacyLocalAssumptionOrdinal ordinal) = - ordinal - - --- | Position of one goal among all batches emitted by one declaration. -newtype LegacyObligationOrdinal = LegacyObligationOrdinal Natural - deriving stock (Show, Eq, Ord) - -legacyObligationOrdinal :: Natural -> LegacyObligationOrdinal -legacyObligationOrdinal = LegacyObligationOrdinal - -legacyObligationOrdinalValue :: LegacyObligationOrdinal -> Natural -legacyObligationOrdinalValue (LegacyObligationOrdinal ordinal) = - ordinal - - --- | Session identity assigned after M3a supplies the owning module. -data SessionLegacyObligationRef = SessionLegacyObligationRef - !LegacyModuleOrdinal - !Marker - !LegacyObligationOrdinal - deriving stock (Show, Eq, Ord) - -sessionLegacyObligationRef - :: LegacyModuleOrdinal - -> Marker - -> LegacyObligationOrdinal - -> SessionLegacyObligationRef -sessionLegacyObligationRef = - SessionLegacyObligationRef - - -data AssumptionKind - = DeclaredUserAxiom - | OpaqueAssumption - deriving stock (Show, Eq, Ord) - - --- | Canonical H0 proposition. This makes no typed-core claim. -newtype LegacyPreparedProposition = - LegacyPreparedProposition Formula - deriving stock (Show, Eq, Ord) - -prepareLegacyProposition - :: Facts.PreparedSemanticFact - -> LegacyPreparedProposition -prepareLegacyProposition = - LegacyPreparedProposition . Facts.preparedSemanticStatement - -legacyPreparedFormula :: LegacyPreparedProposition -> Formula -legacyPreparedFormula (LegacyPreparedProposition formula) = - formula - - -data LegacyDirectAxiomManifestEntry = LegacyDirectAxiomManifestEntry - { legacyDirectAssumptionFact :: !LegacyFactRef - , legacyDirectAssumptionKind :: !AssumptionKind - , legacyDirectAssumptionStatement :: !LegacyPreparedProposition - } - deriving stock (Show, Eq, Ord) - - -data SessionLegacyDeclaredAssumptionRef = - SessionLegacyDeclaredAssumptionRef - !LegacyFactRef - !LegacyLocalAssumptionOrdinal - !AssumptionKind - !LegacyPreparedProposition - deriving stock (Show, Eq, Ord) - - -newtype LegacySemanticFact = - LegacySemanticFact LegacyPreparedProposition - deriving stock (Show, Eq, Ord) - -legacySemanticFact :: LegacyPreparedProposition -> LegacySemanticFact -legacySemanticFact = LegacySemanticFact - -legacySemanticProposition - :: LegacySemanticFact - -> LegacyPreparedProposition -legacySemanticProposition (LegacySemanticFact proposition) = - proposition - - -data LegacyTheoremFinalizationRole - = LegacyOrdinaryTheoremFinalization - deriving stock (Show, Eq, Ord) - -data LegacyDefinitionFactRole - = LegacyDefinitionEquation - deriving stock (Show, Eq, Ord) - -data LegacyDatatypeFactRole - = LegacyDatatypeIntroduction - | LegacyDatatypeDistinctness - | LegacyDatatypeInjectivity - | LegacyDatatypeCases - | LegacyDatatypeInduction - deriving stock (Show, Eq, Ord) - -data LegacyStructureFactRole - = LegacyStructureIntroduction - | LegacyStructureInheritance - | LegacyStructureAssumption - deriving stock (Show, Eq, Ord) - -data LegacyInductiveFactRole - = LegacyInductiveIntroduction - | LegacyInductiveDomainSubset - | LegacyInductiveCases - | LegacyInductiveInduction - deriving stock (Show, Eq, Ord) - -data LegacyRuleTag - = LegacyTheoremRule !LegacyTheoremFinalizationRole - | LegacyDefinitionRule !LegacyDefinitionFactRole - | LegacyDatatypeRule !LegacyDatatypeFactRole - | LegacyStructureRule !LegacyStructureFactRole - | LegacyInductiveRule !LegacyInductiveFactRole - deriving stock (Show, Eq, Ord) - --- | Complete authorization choice for every current legacy fact publisher. -data LegacyFactProducer - = LegacyDeclaredAssumptionProducer !AssumptionKind - | LegacyDirectObligationProducer - | LegacyDeclarationRuleProducer !LegacyRuleTag - deriving stock (Show, Eq, Ord) - - -data LegacyRulePredecessor ref - = LegacyRuleFactPredecessor !ref - | LegacyRuleObligationPredecessor !SessionLegacyObligationRef - deriving stock (Show, Eq, Ord) - -legacyRuleFactPredecessor - :: ref - -> LegacyRulePredecessor ref -legacyRuleFactPredecessor = - LegacyRuleFactPredecessor - -legacyRuleObligationPredecessor - :: SessionLegacyObligationRef - -> LegacyRulePredecessor ref -legacyRuleObligationPredecessor = - LegacyRuleObligationPredecessor - -data CheckedLegacyRuleApplication ref trust = - CheckedLegacyRuleApplication - { checkedLegacyRuleTag :: !LegacyRuleTag - , checkedLegacyRuleTarget :: !LegacyPreparedProposition - , checkedLegacyPredecessors - :: !(Vector (LegacyRulePredecessor ref)) - , checkedLegacyTrustSummary :: !trust - } - deriving stock (Show, Eq) - - -data VampireLoweringAssumption - = VampireUsesDoubleNegationElim - | VampireUsesPropositionalExtensionality - deriving stock (Show, Eq, Ord) - -mandatoryVampireLoweringAssumptions - :: Set VampireLoweringAssumption -mandatoryVampireLoweringAssumptions = - Set.fromList - [ VampireUsesDoubleNegationElim - , VampireUsesPropositionalExtensionality - ] - - -newtype SessionLegacyTrustedVampireUse = - SessionLegacyTrustedVampireUse SessionLegacyObligationRef - deriving stock (Show, Eq, Ord) - -data SessionLegacyGapUse = SessionLegacyGapUse - !SessionLegacyObligationRef - !Location - !Marker - deriving stock (Show, Eq, Ord) - -data SessionLegacyRuleUse = SessionLegacyRuleUse - !LegacyFactRef - !LegacyRuleTag - deriving stock (Show, Eq, Ord) - - -data LegacyTrustDependencies = LegacyTrustDependencies - { legacyDeclaredAssumptionUses - :: !(Set SessionLegacyDeclaredAssumptionRef) - , legacyTrustedVampireUses - :: !(Set SessionLegacyTrustedVampireUse) - , legacyExplicitGaps - :: !(Set SessionLegacyGapUse) - , trustedLegacyRuleUses - :: !(Set SessionLegacyRuleUse) - , legacyVampireLoweringUses - :: !(Set VampireLoweringAssumption) - } - deriving stock (Show, Eq) - -emptyLegacyTrustDependencies :: LegacyTrustDependencies -emptyLegacyTrustDependencies = - LegacyTrustDependencies - { legacyDeclaredAssumptionUses = mempty - , legacyTrustedVampireUses = mempty - , legacyExplicitGaps = mempty - , trustedLegacyRuleUses = mempty - , legacyVampireLoweringUses = mempty - } - -legacyTrustedVampireTrust - :: SessionLegacyObligationRef - -> LegacyTrustDependencies - -> LegacyTrustDependencies -legacyTrustedVampireTrust obligation predecessorTrust = - predecessorTrust - <> mempty - { legacyTrustedVampireUses = - Set.singleton - (SessionLegacyTrustedVampireUse obligation) - , legacyVampireLoweringUses = - mandatoryVampireLoweringAssumptions - } - -legacyGapTrust - :: SessionLegacyObligationRef - -> Location - -> Marker - -> LegacyTrustDependencies - -> LegacyTrustDependencies -legacyGapTrust obligation location marker predecessorTrust = - predecessorTrust - <> mempty - { legacyExplicitGaps = - Set.singleton - (SessionLegacyGapUse - obligation - location - marker) - } - -legacyGapLocations - :: LegacyTrustDependencies - -> [Location] -legacyGapLocations trust = - [ location - | SessionLegacyGapUse - _obligation - location - _marker <- - Set.toList (legacyExplicitGaps trust) - ] - -instance Semigroup LegacyTrustDependencies where - left <> right = - LegacyTrustDependencies - { legacyDeclaredAssumptionUses = - legacyDeclaredAssumptionUses left - <> legacyDeclaredAssumptionUses right - , legacyTrustedVampireUses = - legacyTrustedVampireUses left - <> legacyTrustedVampireUses right - , legacyExplicitGaps = - legacyExplicitGaps left - <> legacyExplicitGaps right - , trustedLegacyRuleUses = - trustedLegacyRuleUses left - <> trustedLegacyRuleUses right - , legacyVampireLoweringUses = - legacyVampireLoweringUses left - <> legacyVampireLoweringUses right - } - -instance Monoid LegacyTrustDependencies where - mempty = emptyLegacyTrustDependencies - - -data SessionLegacyTrustedVampireEvidence trust = - SessionLegacyTrustedVampireEvidence - !SessionLegacyObligationRef - !LegacyPreparedProposition - !AcceptedVampireRun - !trust - deriving stock (Eq) - -data SessionLegacyGapEvidence trust = SessionLegacyGapEvidence - !SessionLegacyObligationRef - !LegacyPreparedProposition - !Location - !Marker - !trust - deriving stock (Show, Eq) - - -data LegacyFactAuthorization ref trust - = LegacyDeclaredAssumption !SessionLegacyDeclaredAssumptionRef - | LegacyTrustedVampire - !(SessionLegacyTrustedVampireEvidence trust) - | LegacyGap !(SessionLegacyGapEvidence trust) - | TrustedLegacyDeclarationRule - !(CheckedLegacyRuleApplication ref trust) - deriving stock (Eq) - -type H1LegacyFactAuthorization = - LegacyFactAuthorization LegacyFactRef LegacyTrustDependencies - -legacyAuthorizationTrustDependencies - :: H1LegacyFactAuthorization - -> LegacyTrustDependencies -legacyAuthorizationTrustDependencies = \case - LegacyDeclaredAssumption reference -> - mempty - { legacyDeclaredAssumptionUses = - Set.singleton reference - } - LegacyTrustedVampire - (SessionLegacyTrustedVampireEvidence - _obligation - _proposition - _run - trust) -> - trust - LegacyGap - (SessionLegacyGapEvidence - _obligation - _proposition - _location - _marker - trust) -> - trust - TrustedLegacyDeclarationRule application -> - checkedLegacyTrustSummary application - - -data LegacyAdmittedFact ref trust = LegacyAdmittedFact - !LegacySemanticFact - !(LegacyFactAuthorization ref trust) - deriving stock (Eq) - -type H1LegacyAdmittedFact = - LegacyAdmittedFact LegacyFactRef LegacyTrustDependencies - - --- | One established fact and its invocation-local registration sidecar. -data LegacyFactEntry = LegacyFactEntry - !LegacyFactRef - !Facts.StagedFact - !H1LegacyAdmittedFact - deriving stock (Eq) - -legacyFactEntryReference :: LegacyFactEntry -> LegacyFactRef -legacyFactEntryReference - (LegacyFactEntry reference _staged _admitted) = - reference - -legacyFactEntryStagedFact :: LegacyFactEntry -> Facts.StagedFact -legacyFactEntryStagedFact - (LegacyFactEntry _reference staged _admitted) = - staged - -legacyFactEntryAdmittedFact - :: LegacyFactEntry - -> H1LegacyAdmittedFact -legacyFactEntryAdmittedFact - (LegacyFactEntry _reference _staged admitted) = - admitted - -legacyFactEntryTrustDependencies - :: LegacyFactEntry - -> LegacyTrustDependencies -legacyFactEntryTrustDependencies = - legacyAuthorizationTrustDependencies - . admittedAuthorization - . legacyFactEntryAdmittedFact - where - admittedAuthorization - (LegacyAdmittedFact _semantic authorization) = - authorization - - --- M3b is the only producer of a nonempty imported view. -data LegacyImportedView = LegacyImportedView - !(Vector LegacyModuleOrdinal) - !(Vector LegacyFactEntry) - !(Map Marker LegacyFactRef) - !Facts.FactRegistry - !(Vector LegacyModuleEnvironmentDelta) - !LegacyCheckingEnvironment - -emptyLegacyImportedView - :: LegacyCheckingEnvironment - -> LegacyImportedView -emptyLegacyImportedView foundation = - LegacyImportedView - Vector.empty - Vector.empty - Map.empty - Facts.emptyFactRegistry - Vector.empty - foundation - -legacyImportedModuleOrdinals - :: LegacyImportedView - -> Vector LegacyModuleOrdinal -legacyImportedModuleOrdinals - (LegacyImportedView - moduleOrdinals - _facts - _aliases - _registry - _environmentDeltas - _environment) = - moduleOrdinals - -legacyImportedCheckingEnvironment - :: LegacyImportedView - -> LegacyCheckingEnvironment -legacyImportedCheckingEnvironment - (LegacyImportedView - _moduleOrdinals - _facts - _aliases - _registry - _environmentDeltas - environment) = - environment - - --- | Private builder for one legacy module in the current invocation. -data LegacyModuleStage = LegacyModuleStage - !LegacyModuleOrdinal - !ResolvedSourceAddress - !LegacyImportedView - !(Vector LegacyFactEntry) - !(Map Marker LegacyFactRef) - !Facts.FactRegistry - !(Vector LegacyDirectAxiomManifestEntry) - -openLegacyModuleStage - :: LegacyModuleAssignment - -> LegacyImportedView - -> LegacyModuleStage -openLegacyModuleStage assignment imported = - LegacyModuleStage - (assignedLegacyModuleOrdinal assignment) - (parsedModuleAddress - (assignedParsedModule assignment)) - imported - Vector.empty - Map.empty - importedRegistry - Vector.empty - where - LegacyImportedView - _moduleOrdinals - _importedFacts - _importedAliases - importedRegistry - _environmentDeltas - _environment = - imported - -legacyStageModuleOrdinal - :: LegacyModuleStage - -> LegacyModuleOrdinal -legacyStageModuleOrdinal - (LegacyModuleStage - ordinal - _address - _imported - _localFacts - _localAliases - _registry - _manifest) = - ordinal - -legacyStageSourceAddress - :: LegacyModuleStage - -> ResolvedSourceAddress -legacyStageSourceAddress - (LegacyModuleStage - _ordinal - address - _imported - _localFacts - _localAliases - _registry - _manifest) = - address - -legacyStageVisibleFacts - :: LegacyModuleStage - -> Vector LegacyFactEntry -legacyStageVisibleFacts stage = - importedFacts <> legacyStageLocalFacts stage - where - LegacyModuleStage - _ordinal - _address - (LegacyImportedView - _moduleOrdinals - importedFacts - _importedAliases - _importedRegistry - _environmentDeltas - _environment) - _localFacts - _localAliases - _stageRegistry - _manifest = - stage - -legacyStageLocalFacts - :: LegacyModuleStage - -> Vector LegacyFactEntry -legacyStageLocalFacts - (LegacyModuleStage - _ordinal - _address - _imported - localFacts - _localAliases - _registry - _manifest) = - localFacts - -legacyStageFactRegistry :: LegacyModuleStage -> Facts.FactRegistry -legacyStageFactRegistry - (LegacyModuleStage - _ordinal - _address - _imported - _localFacts - _localAliases - registry - _manifest) = - registry - -legacyStageDirectAxiomManifest - :: LegacyModuleStage - -> Vector LegacyDirectAxiomManifestEntry -legacyStageDirectAxiomManifest - (LegacyModuleStage - _ordinal - _address - _imported - _localFacts - _localAliases - _registry - manifest) = - manifest - -legacyStageImportedCheckingEnvironment - :: LegacyModuleStage - -> LegacyCheckingEnvironment -legacyStageImportedCheckingEnvironment - (LegacyModuleStage - _ordinal - _address - imported - _localFacts - _localAliases - _registry - _manifest) = - legacyImportedCheckingEnvironment imported - -lookupLegacyStageFact - :: Marker - -> LegacyModuleStage - -> Maybe LegacyFactEntry -lookupLegacyStageFact alias stage = do - reference <- Map.lookup alias (visibleAliasBindings stage) - find - ((== reference) . legacyFactEntryReference) - (Vector.toList (legacyStageVisibleFacts stage)) - - -data LegacyReservedFact = LegacyReservedFact - !LegacyFactRef - !Facts.StagedFact - deriving stock (Show, Eq) - -legacyReservedFactReference - :: LegacyReservedFact - -> LegacyFactRef -legacyReservedFactReference - (LegacyReservedFact reference _staged) = - reference - -legacyReservedStagedFact - :: LegacyReservedFact - -> Facts.StagedFact -legacyReservedStagedFact - (LegacyReservedFact _reference staged) = - staged - -data LegacyDeclarationReservation = LegacyDeclarationReservation - !LegacyModuleOrdinal - !(NonEmpty LegacyReservedFact) - deriving stock (Show, Eq) - -legacyReservedFacts - :: LegacyDeclarationReservation - -> NonEmpty LegacyReservedFact -legacyReservedFacts - (LegacyDeclarationReservation _moduleOrdinal facts) = - facts - -reserveLegacyDeclaration - :: NonEmpty Facts.StagedFact - -> LegacyModuleStage - -> Either LegacyModuleStageError LegacyDeclarationReservation -reserveLegacyDeclaration stagedFacts stage - | finalOrdinal > toInteger (maxBound :: Word32) = - Left - (LegacyLocalFactOrdinalSpaceExhausted - (legacyStageModuleOrdinal stage)) - | otherwise = do - void - (foldM - reserveAlias - (visibleAliasBindings stage) - [ ( alias - , legacyReservedFactReference reserved - ) - | reserved <- reservedFactsList - , alias <- - NonEmpty.toList - (Facts.stagedFactAliases - (legacyReservedStagedFact reserved)) - ]) - pure - (LegacyDeclarationReservation - moduleOrdinal - reservedFacts) - where - moduleOrdinal = - legacyStageModuleOrdinal stage - firstOrdinal = - Vector.length (legacyStageLocalFacts stage) - stagedFactsList = - NonEmpty.toList stagedFacts - finalOrdinal = - toInteger firstOrdinal - + toInteger (length stagedFactsList) - - 1 - reservedFacts = - NonEmpty.zipWith - (\ordinal staged -> - LegacyReservedFact - (legacyFactRef - moduleOrdinal - (legacyLocalFactOrdinal - (fromIntegral ordinal))) - staged) - (firstOrdinal :| [firstOrdinal + 1 ..]) - stagedFacts - reservedFactsList = - NonEmpty.toList reservedFacts - - reserveAlias aliases (alias, reference) = - case Map.lookup alias aliases of - Nothing -> - Right (Map.insert alias reference aliases) - Just previous -> - Left - (LegacyAliasAlreadyBound - alias - previous - reference) - -visibleAliasBindings - :: LegacyModuleStage - -> Map Marker LegacyFactRef -visibleAliasBindings - (LegacyModuleStage - _ordinal - _address - (LegacyImportedView - _moduleOrdinals - _facts - importedAliases - _importedRegistry - _environmentDeltas - _environment) - _localFacts - localAliases - _stageRegistry - _manifest) = - Map.union localAliases importedAliases - -appendEstablishedLegacyDeclaration - :: LegacyDeclarationReservation - -> NonEmpty H1LegacyAdmittedFact - -> LegacyModuleStage - -> Either LegacyModuleStageError LegacyModuleStage -appendEstablishedLegacyDeclaration reservation admittedFacts stage = do - expectedReservation <- - reserveLegacyDeclaration - (fmap legacyReservedStagedFact - (legacyReservedFacts reservation)) - stage - unless - (reservation == expectedReservation) - (Left LegacyReservationDoesNotMatchStage) - let reserved = - NonEmpty.toList (legacyReservedFacts reservation) - admitted = - NonEmpty.toList admittedFacts - unless - (length reserved == length admitted) - (Left - (LegacyEstablishedFactCountMismatch - (length reserved) - (length admitted))) - entries <- - traverse - prepareEntry - (zip reserved admitted) - (manifestEntries, _nextAssumptionOrdinal) <- - foldM - prepareManifestEntry - ([], fromIntegral (Vector.length manifest)) - entries - registry' <- - first - LegacyFactRegistryRejectedAlias - (Facts.registerStagedFacts - (fmap legacyReservedStagedFact - (legacyReservedFacts reservation)) - registry) - let localAliases' = - foldl' - insertEntryAliases - localAliases - entries - pure - (LegacyModuleStage - moduleOrdinal - address - imported - (localFacts <> Vector.fromList entries) - localAliases' - registry' - (manifest - <> Vector.fromList (reverse manifestEntries))) - where - LegacyModuleStage - moduleOrdinal - address - imported - localFacts - localAliases - registry - manifest = - stage - - prepareEntry (reservedFact, admitted) = - let reference = - legacyReservedFactReference reservedFact - staged = - legacyReservedStagedFact reservedFact - expected = - prepareLegacyProposition - (Facts.stagedFactSemantic staged) - LegacyAdmittedFact semantic authorization = - admitted - in - do - unless - (legacySemanticProposition semantic == expected) - (Left - (LegacyEstablishedFactStatementMismatch - reference)) - unless - (legacyAuthorizationTarget authorization - == expected) - (Left - (LegacyEstablishedAuthorizationMismatch - reference)) - traverse_ - (validateObligationModule moduleOrdinal) - (legacyAuthorizationObligations authorization) - let availableReferences = - Set.fromList - ( (legacyFactEntryReference - <$> Vector.toList - (legacyStageVisibleFacts stage)) - <> (legacyReservedFactReference - <$> NonEmpty.toList - (legacyReservedFacts - reservation)) - ) - traverse_ - (\predecessor -> - unless - (predecessor - `Set.member` availableReferences) - (Left - (LegacyAuthorizationReferencesUnknownFact - reference - predecessor))) - (legacyAuthorizationFactPredecessors - authorization) - pure - (LegacyFactEntry - reference - staged - admitted) - - prepareManifestEntry - (entries, nextOrdinal) - (LegacyFactEntry - reference - _staged - (LegacyAdmittedFact - semantic - authorization)) = - case authorization of - LegacyDeclaredAssumption - (SessionLegacyDeclaredAssumptionRef - authorizedReference - assumptionOrdinal - kind - proposition) - | authorizedReference == reference - && legacyLocalAssumptionOrdinalValue - assumptionOrdinal - == nextOrdinal - && proposition - == legacySemanticProposition semantic -> - Right - ( LegacyDirectAxiomManifestEntry - reference - kind - proposition - : entries - , nextOrdinal + 1 - ) - | otherwise -> - Left - (LegacyDeclaredAssumptionDoesNotMatch - reference) - _ -> - Right (entries, nextOrdinal) - - insertEntryAliases aliases entry = - foldl' - (\current alias -> - Map.insert - alias - (legacyFactEntryReference entry) - current) - aliases - (NonEmpty.toList - (Facts.stagedFactAliases - (legacyFactEntryStagedFact entry))) - - -authorizeLegacyDeclaredAssumption - :: LegacyModuleStage - -> AssumptionKind - -> LegacyReservedFact - -> H1LegacyAdmittedFact -authorizeLegacyDeclaredAssumption stage kind reserved = - LegacyAdmittedFact - semantic - (LegacyDeclaredAssumption - (SessionLegacyDeclaredAssumptionRef - reference - assumptionOrdinal - kind - proposition)) - where - reference = - legacyReservedFactReference reserved - proposition = - reservedProposition reserved - semantic = - legacySemanticFact proposition - assumptionOrdinal = - legacyLocalAssumptionOrdinal - (fromIntegral - (Vector.length - (legacyStageDirectAxiomManifest stage))) - -authorizeLegacyTrustedVampire - :: SessionLegacyObligationRef - -> AcceptedVampireRun - -> LegacyTrustDependencies - -> LegacyReservedFact - -> H1LegacyAdmittedFact -authorizeLegacyTrustedVampire - obligation - accepted - predecessorTrust - reserved = - LegacyAdmittedFact - semantic - (LegacyTrustedVampire - (SessionLegacyTrustedVampireEvidence - obligation - proposition - accepted - trust)) - where - proposition = - reservedProposition reserved - semantic = - legacySemanticFact proposition - trust = - legacyTrustedVampireTrust - obligation - predecessorTrust - -authorizeLegacyGap - :: SessionLegacyObligationRef - -> Location - -> Marker - -> LegacyTrustDependencies - -> LegacyReservedFact - -> H1LegacyAdmittedFact -authorizeLegacyGap - obligation - location - marker - predecessorTrust - reserved = - LegacyAdmittedFact - semantic - (LegacyGap - (SessionLegacyGapEvidence - obligation - proposition - location - marker - trust)) - where - proposition = - reservedProposition reserved - semantic = - legacySemanticFact proposition - trust = - legacyGapTrust - obligation - location - marker - predecessorTrust - -authorizeLegacyRule - :: LegacyRuleTag - -> Vector (LegacyRulePredecessor LegacyFactRef) - -> LegacyTrustDependencies - -> LegacyReservedFact - -> H1LegacyAdmittedFact -authorizeLegacyRule tag predecessors predecessorTrust reserved = - LegacyAdmittedFact - semantic - (TrustedLegacyDeclarationRule - CheckedLegacyRuleApplication - { checkedLegacyRuleTag = tag - , checkedLegacyRuleTarget = proposition - , checkedLegacyPredecessors = predecessors - , checkedLegacyTrustSummary = trust - }) - where - reference = - legacyReservedFactReference reserved - proposition = - reservedProposition reserved - semantic = - legacySemanticFact proposition - trust = - predecessorTrust - <> mempty - { trustedLegacyRuleUses = - Set.singleton - (SessionLegacyRuleUse reference tag) - } - -reservedProposition - :: LegacyReservedFact - -> LegacyPreparedProposition -reservedProposition = - prepareLegacyProposition - . Facts.stagedFactSemantic - . legacyReservedStagedFact - -legacyAuthorizationTarget - :: H1LegacyFactAuthorization - -> LegacyPreparedProposition -legacyAuthorizationTarget = \case - LegacyDeclaredAssumption - (SessionLegacyDeclaredAssumptionRef - _reference - _ordinal - _kind - proposition) -> - proposition - LegacyTrustedVampire - (SessionLegacyTrustedVampireEvidence - _obligation - proposition - _run - _trust) -> - proposition - LegacyGap - (SessionLegacyGapEvidence - _obligation - proposition - _location - _marker - _trust) -> - proposition - TrustedLegacyDeclarationRule application -> - checkedLegacyRuleTarget application - -legacyAuthorizationObligations - :: H1LegacyFactAuthorization - -> [SessionLegacyObligationRef] -legacyAuthorizationObligations = \case - LegacyDeclaredAssumption{} -> - [] - LegacyTrustedVampire - (SessionLegacyTrustedVampireEvidence - obligation - _proposition - _run - _trust) -> - [obligation] - LegacyGap - (SessionLegacyGapEvidence - obligation - _proposition - _location - _marker - _trust) -> - [obligation] - TrustedLegacyDeclarationRule application -> - [ obligation - | LegacyRuleObligationPredecessor obligation <- - Vector.toList - (checkedLegacyPredecessors application) - ] - -legacyAuthorizationFactPredecessors - :: H1LegacyFactAuthorization - -> [LegacyFactRef] -legacyAuthorizationFactPredecessors = \case - TrustedLegacyDeclarationRule application -> - [ reference - | LegacyRuleFactPredecessor reference <- - Vector.toList - (checkedLegacyPredecessors application) - ] - _ -> - [] - -validateObligationModule - :: LegacyModuleOrdinal - -> SessionLegacyObligationRef - -> Either LegacyModuleStageError () -validateObligationModule - expected - (SessionLegacyObligationRef actual _marker _ordinal) = - unless - (actual == expected) - (Left - (LegacyAuthorizationReferencesAnotherModule - expected - actual)) - - --- | Completed H1 module. Only 'sealLegacyModuleStage' constructs this value. -data LegacyAdmittedModule = LegacyAdmittedModule - { legacyAdmittedModuleOrdinal :: !LegacyModuleOrdinal - , legacyAdmittedSourceAddress :: !ResolvedSourceAddress - , legacyAdmittedDirectImports :: !(Vector LegacyModuleOrdinal) - , legacyAdmittedVisibleFacts :: !(Vector LegacyFactEntry) - , legacyAdmittedLocalFacts :: !(Vector LegacyFactEntry) - , legacyAdmittedAliasBindings :: !(Map Marker LegacyFactRef) - , legacyAdmittedFactRegistry :: !Facts.FactRegistry - , legacyAdmittedDirectAxiomManifest - :: !(Vector LegacyDirectAxiomManifestEntry) - , legacyAdmittedTrustDependencies :: !LegacyTrustDependencies - , legacyAdmittedEnvironmentDeltas - :: !(Vector LegacyModuleEnvironmentDelta) - , legacyAdmittedCheckingEnvironment - :: !LegacyCheckingEnvironment - } - -sealLegacyModuleStage - :: LegacyCheckingEnvironment - -> LegacyModuleStage - -> Either LegacyModuleStageError LegacyAdmittedModule -sealLegacyModuleStage finalEnvironment stage = do - unless - (actualReferences == expectedReferences) - (Left LegacyStageLocalFactOrderMismatch) - expectedVisibleAliases <- - aliasesForEntries - importedAliases - (Vector.toList localFacts) - unless - (Map.union localAliases importedAliases - == expectedVisibleAliases) - (Left LegacyStageAliasMapMismatch) - expectedManifest <- - manifestForEntries localFacts - unless - (manifest == expectedManifest) - (Left LegacyStageDirectAxiomManifestMismatch) - validateStageRegistry visibleFacts registry - localEnvironmentDelta <- - first - LegacyStageEnvironmentMismatch - (legacyCheckingEnvironmentExtension - importedEnvironment - finalEnvironment) - let moduleEnvironmentDelta = - LegacyModuleEnvironmentDelta - moduleOrdinal - address - localEnvironmentDelta - pure - LegacyAdmittedModule - { legacyAdmittedModuleOrdinal = moduleOrdinal - , legacyAdmittedSourceAddress = address - , legacyAdmittedDirectImports = - legacyImportedModuleOrdinals imported - , legacyAdmittedVisibleFacts = visibleFacts - , legacyAdmittedLocalFacts = localFacts - , legacyAdmittedAliasBindings = - Map.union localAliases importedAliases - , legacyAdmittedFactRegistry = registry - , legacyAdmittedDirectAxiomManifest = manifest - , legacyAdmittedTrustDependencies = - foldMap - legacyFactEntryTrustDependencies - visibleFacts - , legacyAdmittedEnvironmentDeltas = - Vector.snoc - importedEnvironmentDeltas - moduleEnvironmentDelta - , legacyAdmittedCheckingEnvironment = - finalEnvironment - } - where - LegacyModuleStage - moduleOrdinal - address - imported@(LegacyImportedView - _directImports - importedFacts - importedAliases - _importedRegistry - importedEnvironmentDeltas - importedEnvironment) - localFacts - localAliases - registry - manifest = - stage - visibleFacts = - importedFacts <> localFacts - actualReferences = - legacyFactEntryReference <$> Vector.toList localFacts - expectedReferences = - [ legacyFactRef - moduleOrdinal - (legacyLocalFactOrdinal - (fromIntegral ordinal)) - | ordinal <- [0 .. Vector.length localFacts - 1] - ] - -legacyImportedView - :: LegacyCheckingEnvironment - -> [LegacyAdmittedModule] - -> Either LegacyModuleStageError LegacyImportedView -legacyImportedView foundation admittedModules = do - imported <- - foldM - importModule - emptyImportedViewBuild - admittedModules - registry <- - registryForEntries - (reverse (importedFactsReversed imported)) - (environmentDeltas, environment) <- - mergeModuleEnvironments foundation admittedModules - pure - (LegacyImportedView - (Vector.fromList - (legacyAdmittedModuleOrdinal <$> admittedModules)) - (Vector.fromList - (reverse (importedFactsReversed imported))) - (fst <$> importedAliasBindings imported) - registry - environmentDeltas - environment) - where - importModule imported admitted = - foldM - importEntry - imported - (Vector.toList - (legacyAdmittedVisibleFacts admitted)) - -data ImportedViewBuild = ImportedViewBuild - !(Map LegacyFactRef LegacyFactEntry) - ![LegacyFactEntry] - !(Map Marker (LegacyFactRef, Facts.FactOrigin)) - -emptyImportedViewBuild :: ImportedViewBuild -emptyImportedViewBuild = - ImportedViewBuild Map.empty [] Map.empty - -importedFactsReversed :: ImportedViewBuild -> [LegacyFactEntry] -importedFactsReversed - (ImportedViewBuild _entriesByReference entries _aliases) = - entries - -importedAliasBindings - :: ImportedViewBuild - -> Map Marker (LegacyFactRef, Facts.FactOrigin) -importedAliasBindings - (ImportedViewBuild _entriesByReference _entries aliases) = - aliases - -data LegacyModuleEnvironmentDelta = LegacyModuleEnvironmentDelta - !LegacyModuleOrdinal - !ResolvedSourceAddress - !LegacyCheckingEnvironmentDelta - deriving stock (Show, Eq) - -data ImportedEnvironmentBuild = ImportedEnvironmentBuild - !(Map LegacyModuleOrdinal LegacyModuleEnvironmentDelta) - ![LegacyModuleEnvironmentDelta] - -mergeModuleEnvironments - :: LegacyCheckingEnvironment - -> [LegacyAdmittedModule] - -> Either - LegacyModuleStageError - ( Vector LegacyModuleEnvironmentDelta - , LegacyCheckingEnvironment - ) -mergeModuleEnvironments foundation admittedModules = do - imported <- - foldM - importModuleEnvironment - (ImportedEnvironmentBuild Map.empty []) - admittedModules - let ImportedEnvironmentBuild _byOrdinal reversedDeltas = - imported - deltas = - reverse reversedDeltas - environment <- - foldM - applyModuleEnvironmentDelta - foundation - deltas - pure (Vector.fromList deltas, environment) - where - importModuleEnvironment imported admitted = - foldM - importEnvironmentDelta - imported - (Vector.toList - (legacyAdmittedEnvironmentDeltas admitted)) - - importEnvironmentDelta - imported@(ImportedEnvironmentBuild - byOrdinal - reversedDeltas) - delta@(LegacyModuleEnvironmentDelta - ordinal - _address - _environmentDelta) = - case Map.lookup ordinal byOrdinal of - Nothing -> - Right - (ImportedEnvironmentBuild - (Map.insert ordinal delta byOrdinal) - (delta : reversedDeltas)) - Just previous - | previous == delta -> - Right imported - | otherwise -> - Left - (LegacyImportedModuleEnvironmentConflict - ordinal) - - applyModuleEnvironmentDelta - environment - (LegacyModuleEnvironmentDelta - _ordinal - address - delta) = - first - (LegacyImportedEnvironmentConflict address) - (applyLegacyCheckingEnvironmentDelta - delta - environment) - -importEntry - :: ImportedViewBuild - -> LegacyFactEntry - -> Either LegacyModuleStageError ImportedViewBuild -importEntry imported entry = - case Map.lookup reference entriesByReference of - Just previous - | previous == entry -> - Right imported - | otherwise -> - Left - (LegacyImportedFactReferenceConflict - reference) - Nothing -> do - aliases' <- - foldM - insertImportedAlias - aliases - (NonEmpty.toList - (Facts.stagedFactAliases staged)) - pure - (ImportedViewBuild - (Map.insert - reference - entry - entriesByReference) - (entry : entries) - aliases') - where - ImportedViewBuild - entriesByReference - entries - aliases = - imported - reference = - legacyFactEntryReference entry - staged = - legacyFactEntryStagedFact entry - origin = - Facts.stagedFactOrigin staged - - insertImportedAlias current alias = - case Map.lookup alias current of - Nothing -> - Right - (Map.insert - alias - (reference, origin) - current) - Just (previousReference, previousOrigin) - | previousReference == reference -> - Right current - | otherwise -> - Left - (LegacyImportedAliasConflict - alias - previousReference - previousOrigin - reference - origin) - -aliasesForEntries - :: Map Marker LegacyFactRef - -> [LegacyFactEntry] - -> Either LegacyModuleStageError (Map Marker LegacyFactRef) -aliasesForEntries = - foldM insertEntry - where - insertEntry aliases entry = - foldM - (insertAlias - (legacyFactEntryReference entry)) - aliases - (NonEmpty.toList - (Facts.stagedFactAliases - (legacyFactEntryStagedFact entry))) - - insertAlias reference aliases alias = - case Map.lookup alias aliases of - Nothing -> - Right (Map.insert alias reference aliases) - Just previous - | previous == reference -> - Right aliases - | otherwise -> - Left - (LegacyAliasAlreadyBound - alias - previous - reference) - -manifestForEntries - :: Vector LegacyFactEntry - -> Either - LegacyModuleStageError - (Vector LegacyDirectAxiomManifestEntry) -manifestForEntries entries = - Vector.fromList . reverse . fst - <$> foldM - step - ([], 0) - (Vector.toList entries) - where - step (manifest, nextOrdinal) entry = - case legacyFactEntryAdmittedFact entry of - LegacyAdmittedFact - semantic - (LegacyDeclaredAssumption - (SessionLegacyDeclaredAssumptionRef - authorizedReference - assumptionOrdinal - kind - proposition)) - | authorizedReference == reference - && legacyLocalAssumptionOrdinalValue - assumptionOrdinal - == nextOrdinal - && proposition - == legacySemanticProposition semantic -> - Right - ( LegacyDirectAxiomManifestEntry - reference - kind - proposition - : manifest - , nextOrdinal + 1 - ) - | otherwise -> - Left - LegacyStageDirectAxiomManifestMismatch - _ -> - Right (manifest, nextOrdinal) - where - reference = - legacyFactEntryReference entry - -validateStageRegistry - :: Vector LegacyFactEntry - -> Facts.FactRegistry - -> Either LegacyModuleStageError () -validateStageRegistry entries registry = do - unless - (Facts.factRegistryInvariant registry) - (Left LegacyStageFactRegistryMismatch) - unless - (length (Facts.registeredFacts registry) - == Vector.length entries) - (Left LegacyStageFactRegistryMismatch) - traverse_ validateEntry entries - where - validateEntry entry = - traverse_ - (validateAlias - (legacyFactEntryStagedFact entry)) - (Facts.stagedFactAliases - (legacyFactEntryStagedFact entry)) - - validateAlias staged alias = do - unless - (Facts.lookupPreparedFact alias registry - == Just (Facts.stagedFactSemantic staged)) - (Left LegacyStageFactRegistryMismatch) - unless - (Facts.lookupFactOrigin alias registry - == Just (Facts.stagedFactOrigin staged)) - (Left LegacyStageFactRegistryMismatch) - -registryForEntries - :: [LegacyFactEntry] - -> Either LegacyModuleStageError Facts.FactRegistry -registryForEntries = \case - [] -> - Right Facts.emptyFactRegistry - firstEntry : remainingEntries -> - first - LegacyFactRegistryRejectedAlias - (Facts.registerStagedFacts - ( legacyFactEntryStagedFact firstEntry - :| (legacyFactEntryStagedFact - <$> remainingEntries) - ) - Facts.emptyFactRegistry) - - -data LegacyModuleStageError - = LegacyModuleOrdinalSpaceExhausted !Natural - | LegacyLocalFactOrdinalSpaceExhausted !LegacyModuleOrdinal - | LegacyAliasAlreadyBound - !Marker - !LegacyFactRef - !LegacyFactRef - | LegacyReservationDoesNotMatchStage - | LegacyEstablishedFactCountMismatch !Int !Int - | LegacyEstablishedFactStatementMismatch !LegacyFactRef - | LegacyEstablishedAuthorizationMismatch !LegacyFactRef - | LegacyAuthorizationReferencesUnknownFact - !LegacyFactRef - !LegacyFactRef - | LegacyAuthorizationReferencesAnotherModule - !LegacyModuleOrdinal - !LegacyModuleOrdinal - | LegacyDeclaredAssumptionDoesNotMatch !LegacyFactRef - | LegacyFactRegistryRejectedAlias !Marker - | LegacyImportedFactReferenceConflict !LegacyFactRef - | LegacyImportedAliasConflict - !Marker - !LegacyFactRef - !Facts.FactOrigin - !LegacyFactRef - !Facts.FactOrigin - | LegacyStageLocalFactOrderMismatch - | LegacyStageAliasMapMismatch - | LegacyStageFactRegistryMismatch - | LegacyStageDirectAxiomManifestMismatch - | LegacyStageEnvironmentMismatch !Text - | LegacyImportedModuleEnvironmentConflict - !LegacyModuleOrdinal - | LegacyImportedEnvironmentConflict - !ResolvedSourceAddress - !Text - deriving stock (Show, Eq) diff --git a/source/Checking/Legacy/Environment.hs b/source/Checking/Legacy/Environment.hs deleted file mode 100644 index 7b94d53..0000000 --- a/source/Checking/Legacy/Environment.hs +++ /dev/null @@ -1,279 +0,0 @@ -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE NoImplicitPrelude #-} - --- | Immutable legacy declaration environment carried by admitted modules. -module Checking.Legacy.Environment - ( SymbolOwnerKind(..) - , SymbolOwner(..) - , LegacyCheckingEnvironment - , legacyCheckingEnvironment - , legacyEnvironmentAbbreviations - , legacyEnvironmentPredicateDefinitions - , legacyEnvironmentDependencies - , legacyEnvironmentOwnedSymbols - , legacyEnvironmentOwnedSymbolMarkers - , legacyEnvironmentFrozenSymbols - , legacyEnvironmentStructs - , legacyEnvironmentDefinedMarkers - , LegacyCheckingEnvironmentDelta - , legacyCheckingEnvironmentExtension - , applyLegacyCheckingEnvironmentDelta - ) where - -import Base -import Checking.Dependencies qualified as Dependencies -import StructGraph qualified -import Syntax.Internal - -import Bound.Scope (Scope) -import Data.HashMap.Strict qualified as HashMap -import Data.HashSet qualified as HashSet - - -data SymbolOwnerKind - = OwnedByBuiltin - | OwnedBySignaturePredicate - | OwnedBySignatureFormula - | OwnedByAbbreviation - | OwnedByPredicateDefinition - | OwnedByFunctionDefinition - | OwnedByOperatorDefinition - | OwnedByDatatypeHead - | OwnedByDatatypeConstructor - | OwnedByInductiveDefinition - | OwnedByStructureDefinition - deriving stock (Show, Eq) - -data SymbolOwner = SymbolOwner - { symbolOwnerKind :: !SymbolOwnerKind - , symbolOwnerMarker :: !Marker - } - deriving stock (Show, Eq) - - -data LegacyCheckingEnvironment = LegacyCheckingEnvironment - { legacyEnvironmentAbbreviations - :: !(HashMap Symbol (Scope Int ExprOf Void)) - , legacyEnvironmentPredicateDefinitions - :: !(HashMap Predicate [Scope Int ExprOf Void]) - , legacyEnvironmentDependencies - :: !Dependencies.DependencyRegistry - , legacyEnvironmentOwnedSymbols - :: !(HashMap Symbol SymbolOwner) - , legacyEnvironmentOwnedSymbolMarkers - :: !(HashSet Marker) - , legacyEnvironmentFrozenSymbols - :: !(HashMap Symbol Marker) - , legacyEnvironmentStructs - :: !StructGraph.StructGraph - , legacyEnvironmentDefinedMarkers - :: !(HashSet Marker) - } - deriving stock (Show, Eq) - -legacyCheckingEnvironment - :: HashMap Symbol (Scope Int ExprOf Void) - -> HashMap Predicate [Scope Int ExprOf Void] - -> Dependencies.DependencyRegistry - -> HashMap Symbol SymbolOwner - -> HashSet Marker - -> HashMap Symbol Marker - -> StructGraph.StructGraph - -> HashSet Marker - -> LegacyCheckingEnvironment -legacyCheckingEnvironment = - LegacyCheckingEnvironment - - -data LegacyCheckingEnvironmentDelta = - LegacyCheckingEnvironmentDelta - !(HashMap Symbol (Scope Int ExprOf Void)) - !(HashMap Predicate [Scope Int ExprOf Void]) - !Dependencies.DependencyRegistryDelta - !(HashMap Symbol SymbolOwner) - !(HashSet Marker) - !(HashMap Symbol Marker) - !StructGraph.StructGraphDelta - !(HashSet Marker) - deriving stock (Show, Eq) - -legacyCheckingEnvironmentExtension - :: LegacyCheckingEnvironment - -> LegacyCheckingEnvironment - -> Either Text LegacyCheckingEnvironmentDelta -legacyCheckingEnvironmentExtension previous current = do - abbreviations <- - hashMapExtension - "abbreviation" - (legacyEnvironmentAbbreviations previous) - (legacyEnvironmentAbbreviations current) - predicateDefinitions <- - hashMapExtension - "predicate definition" - (legacyEnvironmentPredicateDefinitions previous) - (legacyEnvironmentPredicateDefinitions current) - dependencies <- - Dependencies.dependencyRegistryExtension - (legacyEnvironmentDependencies previous) - (legacyEnvironmentDependencies current) - ownedSymbols <- - hashMapExtension - "symbol owner" - (legacyEnvironmentOwnedSymbols previous) - (legacyEnvironmentOwnedSymbols current) - ownedMarkers <- - hashSetExtension - "owned symbol marker" - (legacyEnvironmentOwnedSymbolMarkers previous) - (legacyEnvironmentOwnedSymbolMarkers current) - frozenSymbols <- - hashMapExtension - "frozen symbol" - (legacyEnvironmentFrozenSymbols previous) - (legacyEnvironmentFrozenSymbols current) - structures <- - StructGraph.structGraphExtension - (legacyEnvironmentStructs previous) - (legacyEnvironmentStructs current) - definedMarkers <- - hashSetExtension - "defined marker" - (legacyEnvironmentDefinedMarkers previous) - (legacyEnvironmentDefinedMarkers current) - pure - (LegacyCheckingEnvironmentDelta - abbreviations - predicateDefinitions - dependencies - ownedSymbols - ownedMarkers - frozenSymbols - structures - definedMarkers) - -applyLegacyCheckingEnvironmentDelta - :: LegacyCheckingEnvironmentDelta - -> LegacyCheckingEnvironment - -> Either Text LegacyCheckingEnvironment -applyLegacyCheckingEnvironmentDelta - (LegacyCheckingEnvironmentDelta - abbreviations - predicateDefinitions - dependencies - ownedSymbols - ownedMarkers - frozenSymbols - structures - definedMarkers) - environment = do - abbreviations' <- - disjointHashMapUnion - "abbreviation" - (legacyEnvironmentAbbreviations environment) - abbreviations - predicateDefinitions' <- - disjointHashMapUnion - "predicate definition" - (legacyEnvironmentPredicateDefinitions environment) - predicateDefinitions - dependencies' <- - Dependencies.applyDependencyRegistryDelta - dependencies - (legacyEnvironmentDependencies environment) - ownedSymbols' <- - disjointHashMapUnion - "symbol owner" - (legacyEnvironmentOwnedSymbols environment) - ownedSymbols - ownedMarkers' <- - disjointHashSetUnion - "owned symbol marker" - (legacyEnvironmentOwnedSymbolMarkers environment) - ownedMarkers - structures' <- - StructGraph.applyStructGraphDelta - structures - (legacyEnvironmentStructs environment) - definedMarkers' <- - disjointHashSetUnion - "defined marker" - (legacyEnvironmentDefinedMarkers environment) - definedMarkers - pure - LegacyCheckingEnvironment - { legacyEnvironmentAbbreviations = abbreviations' - , legacyEnvironmentPredicateDefinitions = - predicateDefinitions' - , legacyEnvironmentDependencies = dependencies' - , legacyEnvironmentOwnedSymbols = ownedSymbols' - , legacyEnvironmentOwnedSymbolMarkers = ownedMarkers' - , legacyEnvironmentFrozenSymbols = - HashMap.union - (legacyEnvironmentFrozenSymbols environment) - frozenSymbols - , legacyEnvironmentStructs = structures' - , legacyEnvironmentDefinedMarkers = definedMarkers' - } - -hashMapExtension - :: (Hashable key, Eq value) - => Text - -> HashMap key value - -> HashMap key value - -> Either Text (HashMap key value) -hashMapExtension label previous current - | all - (\(key, value) -> - HashMap.lookup key current == Just value) - (HashMap.toList previous) = - Right (HashMap.difference current previous) - | otherwise = - Left - ("legacy environment changed an imported " - <> label) - -hashSetExtension - :: Hashable value - => Text - -> HashSet value - -> HashSet value - -> Either Text (HashSet value) -hashSetExtension label previous current - | previous `HashSet.isSubsetOf` current = - Right (current `HashSet.difference` previous) - | otherwise = - Left - ("legacy environment removed an imported " - <> label) - -disjointHashMapUnion - :: Hashable key - => Text - -> HashMap key value - -> HashMap key value - -> Either Text (HashMap key value) -disjointHashMapUnion label previous additions - | HashSet.null duplicateKeys = - Right (HashMap.union previous additions) - | otherwise = - Left - ("imported modules define the same " - <> label) - where - duplicateKeys = - HashMap.keysSet previous - `HashSet.intersection` HashMap.keysSet additions - -disjointHashSetUnion - :: Hashable value - => Text - -> HashSet value - -> HashSet value - -> Either Text (HashSet value) -disjointHashSetUnion label previous additions - | HashSet.null (previous `HashSet.intersection` additions) = - Right (previous <> additions) - | otherwise = - Left - ("imported modules define the same " - <> label) diff --git a/source/Checking/Module.hs b/source/Checking/Module.hs index ad2fb27..bb35277 100644 --- a/source/Checking/Module.hs +++ b/source/Checking/Module.hs @@ -10,6 +10,11 @@ module Checking.Module , identifiedModuleOwner , identifiedModuleBinding , identifiedModuleParsed + , TypedSourceDeclaration + , typedSourceDeclarationBlockIndex + , typedSourceDeclarationHead + , typedSourceDeclarationProof + , typedSourceDeclarations , SealedTypedModule , sealedTypedModuleOwner , sealedTypedModuleSyntax @@ -19,9 +24,12 @@ module Checking.Module , renderCachedTypedModuleError , cachedSealedTypedModule , sealedTypedModulePrefix - , MigrationPreludeSession - , migrationPreludeInput - , migrationPreludeModule + , FinalPreludeSession + , ModuleRootAcquisition(..) + , finalPreludeSource + , finalPreludeInput + , finalPreludeModule + , finalPreludeAcquisition , FinalPreludeReadiness , finalPreludeReadiness , BootstrapPreludeFixture @@ -32,7 +40,7 @@ module Checking.Module , BootstrapError(..) , buildBootstrapPreludeFixture , FinalPreludeReadinessError(..) - , buildFinalPreludeSession + , acquireFinalPreludeSession , TypedModuleInput , TypedModuleInputError(..) , renderTypedModuleInputError @@ -118,6 +126,75 @@ identifiedModuleParsed parsed +-- | One source declaration as consumed by the typed module driver. +-- +-- A claim and its immediately following proof occupy one declaration slot. +-- The head block index remains the syntax-occurrence association index. +data TypedSourceDeclaration = TypedSourceDeclaration + !Int + !Raw.Block + !(Maybe Raw.Proof) + +typedSourceDeclarationBlockIndex :: TypedSourceDeclaration -> Int +typedSourceDeclarationBlockIndex + (TypedSourceDeclaration blockIndex _head _proof) = + blockIndex + +typedSourceDeclarationHead :: TypedSourceDeclaration -> Raw.Block +typedSourceDeclarationHead + (TypedSourceDeclaration _blockIndex headBlock _proof) = + headBlock + +typedSourceDeclarationProof + :: TypedSourceDeclaration + -> Maybe Raw.Proof +typedSourceDeclarationProof + (TypedSourceDeclaration _blockIndex _head proof) = + proof + +typedSourceDeclarations + :: IdentifiedParsedModule + -> [TypedSourceDeclaration] +typedSourceDeclarations parsed = + [ declaration + | item <- typedSourceItems (identifiedParsedModuleBlocks parsed) + , Just declaration <- [sourceItemDeclaration item] + ] + +data TypedSourceItem + = TypedSourceDeclarationItem !TypedSourceDeclaration + | TypedUnmatchedSourceProof !Location + +sourceItemDeclaration + :: TypedSourceItem + -> Maybe TypedSourceDeclaration +sourceItemDeclaration = \case + TypedSourceDeclarationItem declaration -> Just declaration + TypedUnmatchedSourceProof{} -> Nothing + +typedSourceItems :: [Raw.Block] -> [TypedSourceItem] +typedSourceItems = go 0 + where + go _blockIndex [] = [] + go blockIndex (block@Raw.BlockClaim{} : remaining) = + case remaining of + Raw.BlockProof _location proof _end : rest -> + TypedSourceDeclarationItem + (TypedSourceDeclaration blockIndex block (Just proof)) + : go (blockIndex + 2) rest + _ -> + TypedSourceDeclarationItem + (TypedSourceDeclaration blockIndex block Nothing) + : go (blockIndex + 1) remaining + go blockIndex (Raw.BlockProof location _proof _end : remaining) = + TypedUnmatchedSourceProof location + : go (blockIndex + 1) remaining + go blockIndex (block : remaining) = + TypedSourceDeclarationItem + (TypedSourceDeclaration blockIndex block Nothing) + : go (blockIndex + 1) remaining + + data SealedTypedModule = SealedTypedModule !ModuleName !ModuleSyntaxInterface @@ -197,55 +274,79 @@ cachedSealedTypedModule propositions = Store.cachedInstallationPropositions installation -data MigrationPreludeSession = MigrationPreludeSession +data ModuleRootAcquisition + = ModuleRootHit + | ModuleRootMiss + deriving stock (Show, Eq) + +data FinalPreludeSession = FinalPreludeSession + !Prelude.ReservedPreludeSourceInput !IdentifiedModuleInput !SealedTypedModule + !ModuleRootAcquisition + +finalPreludeSource + :: FinalPreludeSession + -> Prelude.ReservedPreludeSourceInput +finalPreludeSource + (FinalPreludeSession source _input _module _acquisition) = + source -migrationPreludeInput - :: MigrationPreludeSession +finalPreludeInput + :: FinalPreludeSession -> IdentifiedModuleInput -migrationPreludeInput (MigrationPreludeSession input _module) = +finalPreludeInput (FinalPreludeSession _source input _module _acquisition) = input -migrationPreludeModule - :: MigrationPreludeSession +finalPreludeModule + :: FinalPreludeSession -> SealedTypedModule -migrationPreludeModule (MigrationPreludeSession _input sealed) = +finalPreludeModule (FinalPreludeSession _source _input sealed _acquisition) = sealed +finalPreludeAcquisition + :: FinalPreludeSession + -> ModuleRootAcquisition +finalPreludeAcquisition + (FinalPreludeSession _source _input _sealed acquisition) = + acquisition + newtype FinalPreludeReadiness = FinalPreludeReadiness SealedTypedModule finalPreludeReadiness - :: MigrationPreludeSession + :: FinalPreludeSession -> FinalPreludeReadiness finalPreludeReadiness = - FinalPreludeReadiness . migrationPreludeModule + FinalPreludeReadiness . finalPreludeModule +-- | Test-only empty-prelude fixture. +-- +-- It is exported for focused exact-compiler tests. Production acquisition is +-- exclusively 'acquireFinalPreludeSession'. newtype BootstrapPreludeFixture = BootstrapPreludeFixture - MigrationPreludeSession + FinalPreludeSession bootstrapPreludeInput :: BootstrapPreludeFixture -> IdentifiedModuleInput bootstrapPreludeInput (BootstrapPreludeFixture fixture) = - migrationPreludeInput fixture + finalPreludeInput fixture bootstrapPreludeModule :: BootstrapPreludeFixture -> SealedTypedModule bootstrapPreludeModule (BootstrapPreludeFixture fixture) = - migrationPreludeModule fixture + finalPreludeModule fixture --- | Fixture seam for the empty bootstrap compiler input. +-- | Test-only seam for the empty bootstrap compiler input. bootstrapPreludeReadiness :: BootstrapPreludeFixture -> FinalPreludeReadiness bootstrapPreludeReadiness = FinalPreludeReadiness . bootstrapPreludeModule --- | Fixture seam for exercising a nonempty distinguished prelude before the --- final source prelude is constructed. +-- | Test-only seam for exercising a synthetic distinguished prelude. fixtureFinalPreludeReadinessFromSealed :: SealedTypedModule -> FinalPreludeReadiness @@ -259,7 +360,7 @@ data BootstrapError | BootstrapSealFailed !SemanticInterfaceError deriving stock (Show) --- | Construct the empty distinguished prelude used by compiler fixtures. +-- | Construct the empty distinguished prelude used only by compiler fixtures. buildBootstrapPreludeFixture :: CheckedFoundation -> Declaration.VampireResolver @@ -291,7 +392,8 @@ buildBootstrapPreludeFixture foundation resolver = do () semantic prefix _closure) -> Right (BootstrapPreludeFixture - (MigrationPreludeSession + (FinalPreludeSession + Prelude.emptyBootstrapSourceInput input (SealedTypedModule preludeModuleName @@ -301,7 +403,8 @@ buildBootstrapPreludeFixture foundation resolver = do (Declaration.freshImportedModuleEvidence [] semantic - prefix)))) + prefix)) + ModuleRootMiss)) Right (Declaration.DriverFailed (Declaration.DriverDeclarationFailed err) @@ -321,34 +424,35 @@ data FinalPreludeReadinessError | FinalPreludeReadinessBuildOpenFailed !Declaration.DriverOpenError | FinalPreludeReadinessArtifactKeyFailed !ModuleArtifactKeyError | FinalPreludeReadinessStoreFailed !Store.StoreFailure + | FinalPreludeReadinessCachedModuleFailed !CachedTypedModuleError | FinalPreludeReadinessAcknowledgementMismatch !ModuleArtifactResult !ModuleArtifactResult deriving stock (Show) --- | Build and atomically publish the exact packaged final prelude. +-- | Acquire the exact packaged final prelude through its ordinary module root. -- --- A session is returned only after the ordinary module root transaction has --- acknowledged the exact artifact that was requested. -buildFinalPreludeSession - :: Store.Store +-- Loading and parsing happen once before the root lookup. A hit is validated +-- and materialized through the generic cached-module boundary; a miss reuses +-- that parsed input for confined construction and atomic publication. +acquireFinalPreludeSession + :: Store.StoreMemo + -> Store.Store -> CheckedFoundation -> Declaration.VampireResolver - -> IO (Either FinalPreludeReadinessError MigrationPreludeSession) -buildFinalPreludeSession store foundation resolver = - FinalPrelude.buildFinalPreludeCandidate foundation resolver >>= \case - FinalPrelude.FinalPreludeSourceLoadFailed failure -> + -> IO (Either FinalPreludeReadinessError FinalPreludeSession) +acquireFinalPreludeSession memo store foundation resolver = + Prelude.loadReservedPreludeSourceInput >>= \case + Left failure -> pure (Left (FinalPreludeReadinessSourceLoadFailed failure)) - FinalPrelude.FinalPreludeSourceParseFailed failure -> - pure (Left (FinalPreludeReadinessSourceParseFailed failure)) - FinalPrelude.FinalPreludeBuildFailed failure _prefix -> - pure (Left (FinalPreludeReadinessBuildFailed failure)) - FinalPrelude.FinalPreludeBuildOpenFailed failure -> - pure (Left (FinalPreludeReadinessBuildOpenFailed failure)) - FinalPrelude.FinalPreludeBuilt candidate -> - install candidate + Right source -> + Prelude.parseReservedPreludeSource source >>= \case + Left failure -> + pure (Left (FinalPreludeReadinessSourceParseFailed failure)) + Right parsed -> + acquire source parsed where - install candidate = + acquire source parsed = case moduleArtifactKey preludeModuleName parsedId @@ -357,47 +461,83 @@ buildFinalPreludeSession store foundation resolver = Left failure -> pure (Left (FinalPreludeReadinessArtifactKeyFailed failure)) Right key -> do - let artifact = - moduleArtifactResult - key - (moduleSyntaxAssertedId syntax) - (semanticInterfaceAssertedId semantic) - Store.writeSealedModule - store - prefix - [syntax] - [semantic] - artifact >>= \case + Store.loadCachedModuleInstallation + memo store key (moduleSyntaxAssertedId syntax) >>= \case Left failure -> pure (Left (FinalPreludeReadinessStoreFailed failure)) - Right acknowledged - | acknowledged /= artifact -> - pure - (Left - (FinalPreludeReadinessAcknowledgementMismatch - artifact - acknowledged)) - | otherwise -> + Right (Just installation) -> + pure do + sealed <- first FinalPreludeReadinessCachedModuleFailed + (cachedSealedTypedModule + foundation [] installation) pure - (Right - (MigrationPreludeSession - identified - (SealedTypedModule - preludeModuleName - syntax - semantic - prefix - (Declaration.freshImportedModuleEvidence - [] - semantic - prefix)))) + (FinalPreludeSession + source + identified sealed ModuleRootHit) + Right Nothing -> + build source parsed key where - parsed = FinalPrelude.finalPreludeParsed candidate identified = identifiedReservedPrelude parsed parsedId = identifiedParsedModuleId (identifiedModuleParsed identified) - syntax = FinalPrelude.finalPreludeSyntax candidate - semantic = FinalPrelude.finalPreludeSemantic candidate - prefix = FinalPrelude.finalPreludePrefix candidate + syntax = identifiedParsedModuleSyntaxInterface + (identifiedModuleParsed identified) + + build source parsed key = + FinalPrelude.buildParsedFinalPreludeCandidate + foundation parsed resolver >>= \case + FinalPrelude.FinalPreludeBuildFailed failure _prefix -> + pure (Left (FinalPreludeReadinessBuildFailed failure)) + FinalPrelude.FinalPreludeBuildOpenFailed failure -> + pure (Left (FinalPreludeReadinessBuildOpenFailed failure)) + FinalPrelude.FinalPreludeBuilt candidate -> + publish source key candidate + FinalPrelude.FinalPreludeSourceLoadFailed failure -> + pure (Left (FinalPreludeReadinessSourceLoadFailed failure)) + FinalPrelude.FinalPreludeSourceParseFailed failure -> + pure (Left (FinalPreludeReadinessSourceParseFailed failure)) + + publish source key candidate = do + let parsed = FinalPrelude.finalPreludeParsed candidate + identified = identifiedReservedPrelude parsed + syntax = FinalPrelude.finalPreludeSyntax candidate + semantic = FinalPrelude.finalPreludeSemantic candidate + prefix = FinalPrelude.finalPreludePrefix candidate + artifact = + moduleArtifactResult + key + (moduleSyntaxAssertedId syntax) + (semanticInterfaceAssertedId semantic) + Store.writeSealedModule + store + prefix + [syntax] + [semantic] + artifact >>= \case + Left failure -> + pure (Left (FinalPreludeReadinessStoreFailed failure)) + Right acknowledged + | acknowledged /= artifact -> + pure + (Left + (FinalPreludeReadinessAcknowledgementMismatch + artifact + acknowledged)) + | otherwise -> + pure + (Right + (FinalPreludeSession + source + identified + (SealedTypedModule + preludeModuleName + syntax + semantic + prefix + (Declaration.freshImportedModuleEvidence + [] + semantic + prefix)) + ModuleRootMiss)) data TypedModuleInput = TypedModuleInput @@ -552,10 +692,10 @@ runTypedModule (Declaration.importSealedModuleDriver . sealedTypedModuleEvidence) effectiveDirect - compileBlocks - 0 - (identifiedParsedModuleBlocks - (identifiedModuleParsed identified)) + compileSourceItems + (typedSourceItems + (identifiedParsedModuleBlocks + (identifiedModuleParsed identified))) semanticDirect = semanticInterfaceAssertedId (sealedTypedModuleSemantic prelude) @@ -568,43 +708,45 @@ runTypedModule occurrences = identifiedParsedModuleSyntaxOccurrences (identifiedModuleParsed identified) - compileBlocks _blockIndex [] = + compileSourceItems [] = pure () - compileBlocks blockIndex (block : remaining) = - case block of - Raw.BlockClaim{} -> - case remaining of - Raw.BlockProof _ proof _end : rest -> do - compileClaim block (Just proof) - compileBlocks (blockIndex + 2) rest - _ -> do - compileClaim block Nothing - compileBlocks (blockIndex + 1) remaining - Raw.BlockProof location _proof _end -> + compileSourceItems (item : remaining) = + case item of + TypedUnmatchedSourceProof location -> Declaration.failModuleDriver (TypedUnmatchedProof location) - Raw.BlockSig{} -> do + TypedSourceDeclarationItem declaration -> do + compileDeclaration declaration + compileSourceItems remaining + + compileDeclaration sourceDeclaration = + case block of + Raw.BlockClaim{} -> + compileClaim block explicitProof + Raw.BlockProof{} -> + impossible + "typed declaration association retained a proof head" + Raw.BlockSig{} -> compileSelected block - compileBlocks (blockIndex + 1) remaining - Raw.BlockAbbr{} -> do + Raw.BlockAbbr{} -> compileSelected block - compileBlocks (blockIndex + 1) remaining - Raw.BlockDefn{} -> do + Raw.BlockDefn{} -> compileSelected block - compileBlocks (blockIndex + 1) remaining - Raw.BlockAxiom{} -> do + Raw.BlockAxiom{} -> compileSourceAxiom block - compileBlocks (blockIndex + 1) remaining - Raw.BlockInductive{} -> do + Raw.BlockInductive{} -> compileInductive block - compileBlocks (blockIndex + 1) remaining - Raw.BlockData{} -> do + Raw.BlockData{} -> compileDatatype block - compileBlocks (blockIndex + 1) remaining - _ -> - Declaration.failModuleDriver - (TypedUnsupportedBlock (locate block)) + Raw.BlockStruct{} -> + compileStructure block where + blockIndex = + typedSourceDeclarationBlockIndex sourceDeclaration + block = typedSourceDeclarationHead sourceDeclaration + explicitProof = + typedSourceDeclarationProof sourceDeclaration + compileSelected selected = do prepared <- Exact.prepareExactDeclaration @@ -672,11 +814,28 @@ runTypedModule (ExactDatatype.commitPreparedExactDatatype datatype) - compileClaim selected explicitProof = do + compileStructure selected = do + prepared <- + Exact.prepareExactStructure + selected + [ parsedSyntaxOccurrenceEntry occurrence + | occurrence <- occurrences + , parsedSyntaxOccurrenceBlockIndex occurrence + == blockIndex + ] + case prepared of + Left failure -> + Declaration.failModuleDriver + (TypedExactCompileFailed failure) + Right structure -> + void + (Exact.commitPreparedExactStructure structure) + + compileClaim selected selectedProof = do prepared <- ExactProof.prepareExactProof selected - explicitProof + selectedProof case prepared of Left failure -> Declaration.failModuleDriver 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 diff --git a/source/Checking/Semantic.hs b/source/Checking/Semantic.hs index 3deaa65..7a05f39 100644 --- a/source/Checking/Semantic.hs +++ b/source/Checking/Semantic.hs @@ -35,6 +35,7 @@ module Checking.Semantic , semanticGlobalKeyType , SemanticGlobalTarget(..) , semanticGlobalTargetObject + , semanticGlobalTargetRequirements , SemanticGlobalBinding , semanticGlobalBinding , semanticGlobalBindingKey @@ -44,7 +45,24 @@ module Checking.Semantic , SemanticEnvironmentDelta , emptySemanticEnvironmentDelta , semanticEnvironmentDelta + , semanticEnvironmentWithStructures , semanticEnvironmentBindings + , semanticEnvironmentStructures + , SemanticStructurePhrase + , semanticStructurePhrase + , semanticStructurePhraseSingular + , semanticStructurePhrasePlural + , semanticStructurePhraseMarker + , SemanticStructureOperation + , semanticStructureOperation + , semanticStructureOperationSymbol + , semanticStructureOperationObject + , SemanticStructureDescriptor + , semanticStructureDescriptor + , semanticStructureDescriptorPhrase + , semanticStructureDescriptorPredicate + , semanticStructureDescriptorParents + , semanticStructureDescriptorOperations , SemanticEnvironmentError(..) , DeclarationInterfaceDelta , declarationInterfaceDelta @@ -147,6 +165,7 @@ import Control.DeepSeq (NFData) import Control.Monad (unless, when) import Data.ByteString (ByteString) import Data.List qualified as List +import Data.Map.Strict qualified as Map import Numeric.Natural (Natural) import Data.Set qualified as Set import Data.Text qualified as Text @@ -389,6 +408,9 @@ semanticGlobalKeyFromLexicalEntry = \case data SemanticGlobalTarget = GlobalReference !ObjectId | TransparentExpansion !ObjectId + | ContextualTransparentExpansion + !ObjectId + !(Map.Map StructSymbol ObjectId) deriving stock (Show, Eq, Ord, Generic) deriving anyclass (NFData) @@ -396,6 +418,15 @@ semanticGlobalTargetObject :: SemanticGlobalTarget -> ObjectId semanticGlobalTargetObject = \case GlobalReference identity -> identity TransparentExpansion identity -> identity + ContextualTransparentExpansion identity _requirements -> identity + +semanticGlobalTargetRequirements + :: SemanticGlobalTarget + -> Map.Map StructSymbol ObjectId +semanticGlobalTargetRequirements = \case + GlobalReference{} -> Map.empty + TransparentExpansion{} -> Map.empty + ContextualTransparentExpansion _identity requirements -> requirements data SemanticGlobalBinding = SemanticGlobalBinding !SemanticGlobalKey @@ -428,13 +459,22 @@ data SemanticGlobalTargetError | SemanticGlobalTargetIsIntrinsic !ObjectId | SemanticGlobalTargetTypeMismatch !ObjectId !CoreType !CoreType | SemanticGlobalExpansionNotTransparent !ObjectId + | SemanticGlobalContextualRequirementsEmpty !ObjectId + | SemanticGlobalContextualRequirementMissing !StructSymbol !ObjectId + | SemanticGlobalContextualRequirementIsIntrinsic !StructSymbol !ObjectId + | SemanticGlobalContextualRequirementTypeMismatch + !StructSymbol !ObjectId !CoreType !CoreType + | SemanticGlobalContextualRequirementNotProvided + !StructSymbol !ObjectId + | SemanticGlobalContextualRequirementNotReferenced !StructSymbol !ObjectId deriving stock (Show, Eq) validateSemanticGlobalBindingTarget - :: CheckedObjectClosure + :: Set.Set (StructSymbol, ObjectId) + -> CheckedObjectClosure -> SemanticGlobalBinding -> Either SemanticGlobalTargetError () -validateSemanticGlobalBindingTarget closure binding = do +validateSemanticGlobalBindingTarget operationBindings closure binding = do expected <- maybe (Left (SemanticGlobalKeyHasInconsistentArity key)) @@ -448,35 +488,193 @@ validateSemanticGlobalBindingTarget closure binding = do when (objectIdFamily identity == IntrinsicObject) (Left (SemanticGlobalTargetIsIntrinsic identity)) - let actual = objectContentType content + let targetExpected = + case target of + ContextualTransparentExpansion{} -> + TyArrow TySet expected + _ -> expected + actual = objectContentType content unless - (actual == expected) + (actual == targetExpected) (Left (SemanticGlobalTargetTypeMismatch - identity expected actual)) + identity targetExpected actual)) case target of GlobalReference{} -> pure () TransparentExpansion{} -> - case content of - TransparentObjectContent{} -> pure () - _ -> - Left - (SemanticGlobalExpansionNotTransparent - identity) + validateTransparent content + ContextualTransparentExpansion _ requirements -> do + validateTransparent content + when + (Map.null requirements) + (Left (SemanticGlobalContextualRequirementsEmpty identity)) + traverse_ (validateRequirement content) (Map.toAscList requirements) where key = semanticGlobalBindingKey binding target = semanticGlobalBindingTarget binding identity = semanticGlobalTargetObject target + validateTransparent = \case + TransparentObjectContent{} -> pure () + _ -> Left (SemanticGlobalExpansionNotTransparent identity) + + validateRequirement content (symbol, object) = do + operationContent <- + maybe + (Left + (SemanticGlobalContextualRequirementMissing + symbol object)) + Right + (lookupCheckedObjectContent object closure) + when + (objectIdFamily object == IntrinsicObject) + (Left + (SemanticGlobalContextualRequirementIsIntrinsic + symbol object)) + let expectedOperation = TyArrow TySet TySet + actualOperation = objectContentType operationContent + unless + (actualOperation == expectedOperation) + (Left + (SemanticGlobalContextualRequirementTypeMismatch + symbol object expectedOperation actualOperation)) + unless + ((symbol, object) `Set.member` operationBindings) + (Left + (SemanticGlobalContextualRequirementNotProvided + symbol object)) + case content of + TransparentObjectContent _theory _coreType body -> + unless + (object `Set.member` canonicalTermGlobals body) + (Left + (SemanticGlobalContextualRequirementNotReferenced + symbol object)) + _ -> impossible "a contextual expansion was not transparent" + data SemanticEnvironmentDelta = EmptySemanticEnvironmentDelta | SemanticGlobalBindings ![SemanticGlobalBinding] + | SemanticGlobalBindingsAndStructures + ![SemanticGlobalBinding] + ![SemanticStructureDescriptor] + deriving stock (Show, Eq, Ord, Generic) + deriving anyclass (NFData) + +data SemanticStructurePhrase = SemanticStructurePhrase + !Pattern + !Pattern + !Marker deriving stock (Show, Eq, Ord, Generic) deriving anyclass (NFData) +semanticStructurePhrase :: LexicalItemSgPl -> SemanticStructurePhrase +semanticStructurePhrase (LexicalItemSgPl forms marker) = + SemanticStructurePhrase (sg forms) (pl forms) marker + +semanticStructurePhraseSingular :: SemanticStructurePhrase -> Pattern +semanticStructurePhraseSingular (SemanticStructurePhrase singular _ _) = + singular + +semanticStructurePhrasePlural :: SemanticStructurePhrase -> Pattern +semanticStructurePhrasePlural (SemanticStructurePhrase _ plural _) = + plural + +semanticStructurePhraseMarker :: SemanticStructurePhrase -> Marker +semanticStructurePhraseMarker (SemanticStructurePhrase _ _ marker) = + marker + +data SemanticStructureOperation = SemanticStructureOperation + !StructSymbol + !ObjectId + deriving stock (Show, Eq, Ord, Generic) + deriving anyclass (NFData) + +semanticStructureOperation + :: StructSymbol + -> ObjectId + -> SemanticStructureOperation +semanticStructureOperation = + SemanticStructureOperation + +semanticStructureOperationSymbol + :: SemanticStructureOperation + -> StructSymbol +semanticStructureOperationSymbol (SemanticStructureOperation symbol _) = + symbol + +semanticStructureOperationObject + :: SemanticStructureOperation + -> ObjectId +semanticStructureOperationObject (SemanticStructureOperation _ object) = + object + +data SemanticStructureDescriptor = SemanticStructureDescriptor + !SemanticStructurePhrase + !(Maybe ObjectId) + ![SemanticStructurePhrase] + ![SemanticStructureOperation] + deriving stock (Show, Eq, Ord, Generic) + deriving anyclass (NFData) + +semanticStructureDescriptor + :: SemanticStructurePhrase + -> Maybe ObjectId + -> [SemanticStructurePhrase] + -> [SemanticStructureOperation] + -> Either SemanticEnvironmentError SemanticStructureDescriptor +semanticStructureDescriptor structurePhrase predicate parents operations = do + case firstDuplicate parents of + Just duplicate -> + Left (DuplicateSemanticStructureParent duplicate) + Nothing -> pure () + when + (structurePhrase `elem` parents) + (Left (SelfSemanticStructureParent structurePhrase)) + case firstDuplicate (semanticStructureOperationSymbol <$> operations) of + Just duplicate -> + Left (DuplicateSemanticStructureOperation duplicate) + Nothing -> pure () + pure + (SemanticStructureDescriptor + structurePhrase predicate parents operations) + +semanticStructureDescriptorPhrase + :: SemanticStructureDescriptor + -> SemanticStructurePhrase +semanticStructureDescriptorPhrase + (SemanticStructureDescriptor structurePhrase _ _ _) = + structurePhrase + +semanticStructureDescriptorPredicate + :: SemanticStructureDescriptor + -> Maybe ObjectId +semanticStructureDescriptorPredicate + (SemanticStructureDescriptor _ predicate _ _) = + predicate + +semanticStructureDescriptorParents + :: SemanticStructureDescriptor + -> [SemanticStructurePhrase] +semanticStructureDescriptorParents + (SemanticStructureDescriptor _ _ parents _) = + parents + +semanticStructureDescriptorOperations + :: SemanticStructureDescriptor + -> [SemanticStructureOperation] +semanticStructureDescriptorOperations + (SemanticStructureDescriptor _ _ _ operations) = + operations + data SemanticEnvironmentError = DuplicateSemanticGlobalKey !SemanticGlobalKey | NonCanonicalSemanticGlobalBindingOrder + | DuplicateSemanticStructure !SemanticStructurePhrase + | NonCanonicalSemanticStructureOrder + | DuplicateSemanticStructureParent !SemanticStructurePhrase + | SelfSemanticStructureParent !SemanticStructurePhrase + | DuplicateSemanticStructureOperation !StructSymbol deriving stock (Show, Eq) emptySemanticEnvironmentDelta :: SemanticEnvironmentDelta @@ -486,9 +684,16 @@ emptySemanticEnvironmentDelta = semanticEnvironmentDelta :: [SemanticGlobalBinding] -> Either SemanticEnvironmentError SemanticEnvironmentDelta -semanticEnvironmentDelta [] = +semanticEnvironmentDelta bindings = + semanticEnvironmentWithStructures bindings [] + +semanticEnvironmentWithStructures + :: [SemanticGlobalBinding] + -> [SemanticStructureDescriptor] + -> Either SemanticEnvironmentError SemanticEnvironmentDelta +semanticEnvironmentWithStructures [] [] = Right EmptySemanticEnvironmentDelta -semanticEnvironmentDelta bindings = do +semanticEnvironmentWithStructures bindings structures = do case firstDuplicate (semanticGlobalBindingKey <$> bindings) of Just duplicate -> Left (DuplicateSemanticGlobalKey duplicate) @@ -497,7 +702,19 @@ semanticEnvironmentDelta bindings = do unless (bindings == List.sortOn semanticGlobalBindingKey bindings) (Left NonCanonicalSemanticGlobalBindingOrder) - pure (SemanticGlobalBindings bindings) + case firstDuplicate (semanticStructureDescriptorPhrase <$> structures) of + Just duplicate -> + Left (DuplicateSemanticStructure duplicate) + Nothing -> pure () + unless + ( structures + == List.sortOn semanticStructureDescriptorPhrase structures + ) + (Left NonCanonicalSemanticStructureOrder) + pure + (case structures of + [] -> SemanticGlobalBindings bindings + _ -> SemanticGlobalBindingsAndStructures bindings structures) semanticEnvironmentBindings :: SemanticEnvironmentDelta @@ -505,6 +722,15 @@ semanticEnvironmentBindings semanticEnvironmentBindings = \case EmptySemanticEnvironmentDelta -> [] SemanticGlobalBindings bindings -> bindings + SemanticGlobalBindingsAndStructures bindings _ -> bindings + +semanticEnvironmentStructures + :: SemanticEnvironmentDelta + -> [SemanticStructureDescriptor] +semanticEnvironmentStructures = \case + EmptySemanticEnvironmentDelta -> [] + SemanticGlobalBindings{} -> [] + SemanticGlobalBindingsAndStructures _ structures -> structures data DeclarationInterfaceDelta = DeclarationInterfaceDelta @@ -1079,6 +1305,11 @@ putSemanticEnvironmentDeltaCache EmptySemanticEnvironmentDelta = putSemanticEnvironmentDeltaCache (SemanticGlobalBindings bindings) = do putCacheTag 0x01 putCacheList putSemanticGlobalBindingCache bindings +putSemanticEnvironmentDeltaCache + (SemanticGlobalBindingsAndStructures bindings structures) = do + putCacheTag 0x02 + putCacheList putSemanticGlobalBindingCache bindings + putCacheList putSemanticStructureDescriptorCache structures getSemanticEnvironmentDeltaCache :: CacheGet SemanticEnvironmentDelta @@ -1092,6 +1323,13 @@ getSemanticEnvironmentDeltaCache = (fail . ("invalid semantic environment delta: " <>) . show) pure (semanticEnvironmentDelta bindings) + 0x02 -> do + bindings <- getCacheList getSemanticGlobalBindingCache + structures <- getCacheList getSemanticStructureDescriptorCache + either + (fail . ("invalid semantic environment delta: " <>) . show) + pure + (semanticEnvironmentWithStructures bindings structures) tag -> fail ("unknown semantic environment delta tag " @@ -1168,6 +1406,13 @@ putSemanticGlobalBindingCache (SemanticGlobalBinding key target) = do TransparentExpansion identity -> do putCacheTag 0x01 putObjectIdCache identity + ContextualTransparentExpansion identity requirements -> do + putCacheTag 0x02 + putObjectIdCache identity + putCanonicalCacheMap + (\(StructSymbol symbol) -> putCacheText symbol) + putObjectIdCache + requirements getSemanticGlobalBindingCache :: CacheGet SemanticGlobalBinding getSemanticGlobalBindingCache = @@ -1176,11 +1421,71 @@ getSemanticGlobalBindingCache = <*> (getCacheTag >>= \case 0x00 -> GlobalReference <$> getObjectIdCache 0x01 -> TransparentExpansion <$> getObjectIdCache + 0x02 -> + ContextualTransparentExpansion + <$> getObjectIdCache + <*> getCanonicalCacheMap + (StructSymbol <$> getCacheText) + getObjectIdCache tag -> fail ("unknown semantic global target tag " <> show tag)) +putSemanticStructureDescriptorCache + :: SemanticStructureDescriptor + -> CachePut +putSemanticStructureDescriptorCache + (SemanticStructureDescriptor structurePhrase predicate parents operations) = do + putSemanticStructurePhraseCache structurePhrase + putCacheMaybe putObjectIdCache predicate + putCacheList putSemanticStructurePhraseCache parents + putCacheList putSemanticStructureOperationCache operations + +getSemanticStructureDescriptorCache + :: CacheGet SemanticStructureDescriptor +getSemanticStructureDescriptorCache = do + structurePhrase <- getSemanticStructurePhraseCache + predicate <- getCacheMaybe getObjectIdCache + parents <- getCacheList getSemanticStructurePhraseCache + operations <- getCacheList getSemanticStructureOperationCache + either + (fail . ("invalid semantic structure descriptor: " <>) . show) + pure + (semanticStructureDescriptor structurePhrase predicate parents operations) + +putSemanticStructurePhraseCache + :: SemanticStructurePhrase + -> CachePut +putSemanticStructurePhraseCache + (SemanticStructurePhrase singular plural (Marker marker)) = do + putPatternCache singular + putPatternCache plural + putCacheText marker + +getSemanticStructurePhraseCache + :: CacheGet SemanticStructurePhrase +getSemanticStructurePhraseCache = + SemanticStructurePhrase + <$> getPatternCache + <*> getPatternCache + <*> (Marker <$> getCacheText) + +putSemanticStructureOperationCache + :: SemanticStructureOperation + -> CachePut +putSemanticStructureOperationCache + (SemanticStructureOperation (StructSymbol symbol) object) = do + putCacheText symbol + putObjectIdCache object + +getSemanticStructureOperationCache + :: CacheGet SemanticStructureOperation +getSemanticStructureOperationCache = + SemanticStructureOperation + <$> (StructSymbol <$> getCacheText) + <*> getObjectIdCache + putDeclarationInterfaceDeltaCache :: DeclarationInterfaceDelta -> CachePut diff --git a/source/Checking/Structure.hs b/source/Checking/Structure.hs deleted file mode 100644 index ce4a2ac..0000000 --- a/source/Checking/Structure.hs +++ /dev/null @@ -1,150 +0,0 @@ -{-# LANGUAGE NoImplicitPrelude #-} -{-# LANGUAGE RecordWildCards #-} - -module Checking.Structure - ( CheckedStructDefn - , StructurePreparationError(..) - , prepareCheckedStructDefn - , checkedStructPhrase - , checkedStructAncestors - , checkedStructInternalSymbols - , checkedStructAllSymbols - , checkedStructSymbol - , checkedStructDependencies - , checkedStructSemanticFacts - , checkedStructFacts - , checkedStructFactRoles - , checkedStructMarkers - ) where - -import Base -import Checking.Facts -import Checking.Legacy -import Report.Location -import Syntax.Internal -import Syntax.Lexicon - -import Data.List.NonEmpty qualified as NonEmpty -import Data.Set qualified as Set - - --- | A structure declaration whose formulas have been fully prepared. -data CheckedStructDefn = CheckedStructDefn - { checkedStructPhrase :: !StructPhrase - , checkedStructAncestors :: !(Set StructPhrase) - , checkedStructInternalSymbols :: !(Set StructSymbol) - , checkedStructAllSymbols :: !(Set StructSymbol) - , checkedStructSymbol :: !Symbol - , checkedStructDependencies :: !(Set Symbol) - , checkedStructFacts :: !(NonEmpty StagedFact) - } - deriving (Show, Eq) - -checkedStructSemanticFacts - :: CheckedStructDefn - -> NonEmpty PreparedSemanticFact -checkedStructSemanticFacts = - fmap stagedFactSemantic . checkedStructFacts - -checkedStructMarkers :: CheckedStructDefn -> NonEmpty Marker -checkedStructMarkers = - (>>= stagedFactAliases) . checkedStructFacts - -checkedStructFactRoles - :: CheckedStructDefn - -> NonEmpty LegacyStructureFactRole -checkedStructFactRoles checked = - LegacyStructureIntroduction - :| ( LegacyStructureInheritance - : replicate - (max 0 (factCount - 2)) - LegacyStructureAssumption - ) - where - factCount = - length (checkedStructFacts checked) - -data StructurePreparationError - = SelfReferentialStructure !Symbol - deriving (Show, Eq) - -prepareCheckedStructDefn - :: Location - -> Marker - -> StructDefn - -> Set StructPhrase - -> Set StructSymbol - -> Either StructurePreparationError CheckedStructDefn -prepareCheckedStructDefn location marker StructDefn{..} ancestors inheritedSymbols - | prospectiveSymbol `Set.member` assumptionDependencies = - Left (SelfReferentialStructure prospectiveSymbol) - | otherwise = - Right - CheckedStructDefn - { checkedStructPhrase = structPhrase - , checkedStructAncestors = ancestors - , checkedStructInternalSymbols = structDefnFixes - , checkedStructAllSymbols = structDefnFixes <> inheritedSymbols - , checkedStructSymbol = prospectiveSymbol - , checkedStructDependencies = - parentSymbols <> assumptionDependencies - , checkedStructFacts = stagedFacts - } - where - prospectiveSymbol = - SymbolPredicate (PredicateNounStruct structPhrase) - parentSymbols = - Set.map - (SymbolPredicate . PredicateNounStruct) - structParents - assumptionDependencies = - Set.unions - [ preparedSemanticDependencies (prepareSemanticFact formula) - | (_assumptionMarker, formula) <- structDefnAssumes - ] - isStruct phrase = - TermSymbol - Nowhere - (SymbolPredicate (PredicateNounStruct phrase)) - [TermVar structDefnLabel] - parentPremises - | structParents == Set.singleton _Onesorted = - [] - | otherwise = - isStruct <$> Set.toList structParents - intro = - makeConjunction - (parentPremises <> (snd <$> structDefnAssumes)) - `Implies` isStruct structPhrase - inherit = - isStruct structPhrase - `Implies` makeConjunction - [ isStruct parent - | parent <- Set.toList structParents - ] - generated = - (marker, intro) - :| ( (inheritMarker, inherit) - : [ (assumptionMarker, isStruct structPhrase `Implies` formula) - | (assumptionMarker, formula) <- structDefnAssumes - ] - ) - inheritMarker = - case marker of - Marker text -> - Marker (text <> "inherit") - origin = - factOrigin location marker - semanticFacts = - fmap - (prepareSemanticFact . forallClosure mempty . snd) - generated - stagedFacts = - NonEmpty.zipWith - (\(factMarker, _formula) semantic -> - stageFact - (factMarker :| []) - origin - semantic) - generated - semanticFacts diff --git a/source/Checking/Transition.hs b/source/Checking/Transition.hs deleted file mode 100644 index a2e7054..0000000 --- a/source/Checking/Transition.hs +++ /dev/null @@ -1,2584 +0,0 @@ -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE NoImplicitPrelude #-} - --- | Closed in-memory carrier used while declaration families migrate from the --- disposable legacy checker to checked typed semantics. -module Checking.Transition - ( ModuleName - , moduleName - , moduleNameNamespace - , moduleNameRelativePath - , LocalDeclarationOrdinal - , localDeclarationOrdinalValue - , LocalFactOrdinal - , localFactOrdinalValue - , LocalAssumptionOrdinal - , localAssumptionOrdinalValue - , OpaqueDeclarationRef - , opaqueDeclarationModule - , opaqueDeclarationOrdinal - , Origin - , origin - , CheckedGlobalRef - , checkedGlobalReference - , checkedGlobalType - , FactRef - , factReferenceModule - , factReferenceOrdinal - , TransitionFactRef - , transitionTypedFactReference - , TypedDirectAxiomManifestEntry - , typedDirectAssumptionFact - , typedDirectAssumptionKind - , typedDirectAssumptionStatement - , SessionTypedDeclaredAssumptionRef - , sessionTypedAssumptionFact - , sessionTypedAssumptionOrdinal - , sessionTypedAssumptionKind - , sessionTypedAssumptionStatement - , SessionTypedTrustedVampireUse - , TypedTrustDependencies - , typedDeclaredAssumptionUses - , typedTrustedVampireUses - , typedVampireLoweringUses - , typedFoundationUses - , typedKernelRuleUses - , TransitionDerivationImport - , transitionDerivationImport - , lookupTransitionTypedImport - , AdmittedFact - , admittedFactReference - , admittedFactIsKernelProof - , admittedFactIsReconstructedKernelProof - , admittedFactIsTrustedVampire - , admittedFactTypedTrustDependencies - , TransitionModuleBuilder - , openTransitionModuleBuilder - , transitionBuilderLegacyStage - , transitionBuilderImportedCheckingEnvironment - , transitionBuilderFoundation - , GlobalPremisePolicy(..) - , TransitionTypedProblemError(..) - , planTransitionTypedProblem - , beginTransitionDeclaration - , transitionCurrentDeclarationReference - , commitTransitionOpaqueGlobal - , commitTransitionTransparentGlobal - , commitTransitionKernelFact - , commitTransitionKernelFactWithImports - , commitTransitionTypedVampireFact - , commitTransitionTypedDeclaredAssumption - , transitionBuilderWithLegacyStage - , lookupTransitionGlobal - , lookupTransitionGlobalBody - , TransitionAdmittedModule - , sealTransitionModule - , transitionAdmittedName - , transitionAdmittedLegacyModule - , transitionAdmittedFacts - , transitionAdmittedKernelProofCount - , transitionAdmittedTypedTrustedVampireCount - , TransitionReplayMeasurements(..) - , transitionAdmittedReplayMeasurements - , transitionAdmittedTypedDirectAxiomManifest - , transitionAdmittedTypedTrustDependencies - , transitionAdmittedGlobals - , TransitionModuleError(..) - ) where - -import Base -import Checking.Backend.Connection qualified as BackendConnection -import Checking.Backend.Problem qualified as Backend -import Checking.Backend.Reconstruction qualified as BackendReconstruction -import Checking.Backend.Tptp qualified as BackendTptp -import Checking.Core -import Checking.Facts qualified as Facts -import Checking.Foundation - ( CheckedFoundation - , FoundationAxiomTag - , KernelRuleTag - , foundationAxiomFrozen - ) -import Checking.Kernel.Derivation -import Checking.Legacy -import Felix.Module -import Provers qualified -import Report.Location -import Syntax.Internal - -import Control.Monad (foldM, unless) -import Data.Bifunctor (first) -import Data.Map.Strict qualified as Map -import Data.Sequence qualified as Seq -import Data.Set qualified as Set -import Data.Vector (Vector) -import Data.Vector qualified as Vector -import Numeric.Natural (Natural) - - -data OpaqueDeclarationRef = OpaqueDeclarationRef - !ModuleName - !LocalDeclarationOrdinal - deriving stock (Show, Eq, Ord) - -opaqueDeclarationModule - :: OpaqueDeclarationRef - -> ModuleName -opaqueDeclarationModule - (OpaqueDeclarationRef name _ordinal) = - name - -opaqueDeclarationOrdinal - :: OpaqueDeclarationRef - -> LocalDeclarationOrdinal -opaqueDeclarationOrdinal - (OpaqueDeclarationRef _name ordinal) = - ordinal - -data Origin = Origin - !Location - !(Maybe Text) - !(Maybe Marker) - deriving stock (Show, Eq) - -origin - :: Location - -> Maybe Text - -> Maybe Marker - -> Origin -origin = - Origin - - -data CheckedGlobalRef = CheckedOpaqueGlobal - !OpaqueDeclarationRef - !CoreType - deriving stock (Show, Eq, Ord) - -checkedGlobalReference - :: CheckedGlobalRef - -> OpaqueDeclarationRef -checkedGlobalReference - (CheckedOpaqueGlobal reference _coreType) = - reference - -checkedGlobalType :: CheckedGlobalRef -> CoreType -checkedGlobalType - (CheckedOpaqueGlobal _reference coreType) = - coreType - -newtype LocalAssumptionOrdinal = - LocalAssumptionOrdinal Natural - deriving stock (Show, Eq, Ord) - -localAssumptionOrdinalValue - :: LocalAssumptionOrdinal - -> Natural -localAssumptionOrdinalValue - (LocalAssumptionOrdinal ordinal) = - ordinal - -data FactRef = FactRef - !ModuleName - !LocalFactOrdinal - deriving stock (Show, Eq, Ord) - -factReferenceModule :: FactRef -> ModuleName -factReferenceModule (FactRef name _ordinal) = - name - -factReferenceOrdinal :: FactRef -> LocalFactOrdinal -factReferenceOrdinal (FactRef _name ordinal) = - ordinal - -data TransitionFactRef - = TransitionLegacyFactRef !LegacyFactRef - | TransitionTypedFactRef !FactRef - deriving stock (Show, Eq, Ord) - -transitionTypedFactReference - :: TransitionFactRef - -> Maybe FactRef -transitionTypedFactReference = \case - TransitionLegacyFactRef{} -> - Nothing - TransitionTypedFactRef reference -> - Just reference - -data TypedSemanticFact = TypedSemanticFact - !(FrozenCheckedCore CheckedGlobalRef) - !(Backend.SupportedProposition - Void - CheckedGlobalRef) - !(Backend.FofCapability - (Backend.CheckedFofProjection - Void - CheckedGlobalRef)) - deriving stock (Eq) - -prepareTypedSemanticFact - :: TransitionModuleBuilder - -> FrozenCheckedCore CheckedGlobalRef - -> Either TransitionModuleError TypedSemanticFact -prepareTypedSemanticFact builder supplied = do - statement <- - recheckBuilderFrozenCore builder supplied - prepare statement - where - prepare statement - | frozenCoreType statement /= TyProp = - Left - (TransitionTypedFactIsNotProposition - (frozenCoreType statement)) - | otherwise = do - proposition <- - first TransitionTypedFactSupportError - (Backend.supportedProposition - Vector.empty - (embedClosedCore [] statement)) - capability <- - first TransitionTypedFactClassificationError - (Backend.classifySupportedProposition - (builderGlobalType builder) - proposition) - Right - (TypedSemanticFact - statement - proposition - capability) - -typedSemanticStatement - :: TypedSemanticFact - -> FrozenCheckedCore CheckedGlobalRef -typedSemanticStatement - (TypedSemanticFact - statement - _proposition - _capability) = - statement - -typedSemanticProposition - :: TypedSemanticFact - -> Backend.SupportedProposition - Void - CheckedGlobalRef -typedSemanticProposition - (TypedSemanticFact - _statement - proposition - _capability) = - proposition - -typedSemanticFofCapability - :: TypedSemanticFact - -> Backend.FofCapability - (Backend.CheckedFofProjection - Void - CheckedGlobalRef) -typedSemanticFofCapability - (TypedSemanticFact - _statement - _proposition - capability) = - capability - -data TypedDirectAxiomManifestEntry = - TypedDirectAxiomManifestEntry - !FactRef - !AssumptionKind - !(FrozenCheckedCore CheckedGlobalRef) - deriving stock (Show, Eq, Ord) - -typedDirectAssumptionFact - :: TypedDirectAxiomManifestEntry - -> FactRef -typedDirectAssumptionFact - (TypedDirectAxiomManifestEntry reference _kind _statement) = - reference - -typedDirectAssumptionKind - :: TypedDirectAxiomManifestEntry - -> AssumptionKind -typedDirectAssumptionKind - (TypedDirectAxiomManifestEntry _reference kind _statement) = - kind - -typedDirectAssumptionStatement - :: TypedDirectAxiomManifestEntry - -> FrozenCheckedCore CheckedGlobalRef -typedDirectAssumptionStatement - (TypedDirectAxiomManifestEntry _reference _kind statement) = - statement - -data SessionTypedDeclaredAssumptionRef = - SessionTypedDeclaredAssumptionRef - !FactRef - !LocalAssumptionOrdinal - !AssumptionKind - !(FrozenCheckedCore CheckedGlobalRef) - deriving stock (Show, Eq, Ord) - -sessionTypedAssumptionFact - :: SessionTypedDeclaredAssumptionRef - -> FactRef -sessionTypedAssumptionFact - (SessionTypedDeclaredAssumptionRef - reference - _ordinal - _kind - _statement) = - reference - -sessionTypedAssumptionOrdinal - :: SessionTypedDeclaredAssumptionRef - -> LocalAssumptionOrdinal -sessionTypedAssumptionOrdinal - (SessionTypedDeclaredAssumptionRef - _reference - ordinal - _kind - _statement) = - ordinal - -sessionTypedAssumptionKind - :: SessionTypedDeclaredAssumptionRef - -> AssumptionKind -sessionTypedAssumptionKind - (SessionTypedDeclaredAssumptionRef - _reference - _ordinal - kind - _statement) = - kind - -sessionTypedAssumptionStatement - :: SessionTypedDeclaredAssumptionRef - -> FrozenCheckedCore CheckedGlobalRef -sessionTypedAssumptionStatement - (SessionTypedDeclaredAssumptionRef - _reference - _ordinal - _kind - statement) = - statement - -newtype SessionTypedTrustedVampireUse = - SessionTypedTrustedVampireUse FactRef - deriving stock (Show, Eq, Ord) - -data TypedTrustDependencies = TypedTrustDependencies - { typedDeclaredAssumptionUses - :: !(Set SessionTypedDeclaredAssumptionRef) - , typedTrustedVampireUses - :: !(Set SessionTypedTrustedVampireUse) - , typedVampireLoweringUses - :: !(Set VampireLoweringAssumption) - , typedFoundationUses - :: !(Set FoundationAxiomTag) - , typedKernelRuleUses - :: !(Set KernelRuleTag) - } - deriving stock (Show, Eq) - -instance Semigroup TypedTrustDependencies where - left <> right = - TypedTrustDependencies - { typedDeclaredAssumptionUses = - typedDeclaredAssumptionUses left - <> typedDeclaredAssumptionUses right - , typedTrustedVampireUses = - typedTrustedVampireUses left - <> typedTrustedVampireUses right - , typedVampireLoweringUses = - typedVampireLoweringUses left - <> typedVampireLoweringUses right - , typedFoundationUses = - typedFoundationUses left - <> typedFoundationUses right - , typedKernelRuleUses = - typedKernelRuleUses left - <> typedKernelRuleUses right - } - -instance Monoid TypedTrustDependencies where - mempty = - TypedTrustDependencies - { typedDeclaredAssumptionUses = mempty - , typedTrustedVampireUses = mempty - , typedVampireLoweringUses = mempty - , typedFoundationUses = mempty - , typedKernelRuleUses = mempty - } - -data AuthorizedKernelReplay = - AuthorizedKernelReplay - !(FrozenCheckedCore CheckedGlobalRef) - !(Set FactRef) - !(Set FoundationAxiomTag) - !(Set KernelRuleTag) - !Natural - !Natural - !(Maybe SessionTypedReconstructionProvenance) - deriving stock (Eq) - -data SessionTypedReconstructionProvenance = - SessionTypedReconstructionProvenance - !BackendReconstruction.ReconstructionPolicy - !(BackendTptp.PreparedTypedTptpProblem - TransitionFactRef - Void - CheckedGlobalRef) - !Provers.AcceptedVampireRun - !BackendConnection.ConnectionTrace - !BackendConnection.ConnectionSearchStats - !Natural - !Natural - deriving stock (Eq) - -data SessionTypedReconstructionFallback = - SessionTypedReconstructionFallback - !BackendReconstruction.ReconstructionPolicy - !SessionTypedReconstructionFallbackReason - deriving stock (Eq) - -data SessionTypedReconstructionFallbackReason - = ReconstructionFallbackUnsupported - !(BackendConnection.ConnectionUnsupported - TransitionFactRef) - | ReconstructionFallbackUnavailable - !BackendConnection.ConnectionSearchStats - | ReconstructionFallbackSearchExhausted - !BackendConnection.ConnectionExhaustion - !BackendConnection.ConnectionSearchStats - | ReconstructionFallbackKernelReplayExhausted - !KernelReplayError - deriving stock (Eq) - -data SessionTypedTrustedVampireEvidence = - SessionTypedTrustedVampireEvidence - !FactRef - !(FrozenCheckedCore CheckedGlobalRef) - !(BackendTptp.PreparedTypedTptpProblem - TransitionFactRef - Void - CheckedGlobalRef) - !Provers.AcceptedVampireRun - !TypedTrustDependencies - !SessionTypedReconstructionFallback - deriving stock (Eq) - -data FactAuthorization - = KernelProof - !AuthorizedKernelReplay - !TypedTrustDependencies - | DeclaredAssumption - !SessionTypedDeclaredAssumptionRef - | TrustedVampire - !SessionTypedTrustedVampireEvidence - deriving stock (Eq) - -data TypedAdmittedFact = TypedAdmittedFact - !TypedSemanticFact - !FactAuthorization - deriving stock (Eq) - -commitTransitionKernelFact - :: NonEmpty Marker - -> Origin - -> FrozenCheckedCore CheckedGlobalRef - -> KernelDerivation CheckedGlobalRef - -> TransitionModuleBuilder - -> Either TransitionModuleError TransitionModuleBuilder -commitTransitionKernelFact aliases factOrigin target derivation builder = - commitTransitionKernelFactWithImports - aliases - factOrigin - Vector.empty - target - derivation - builder - -commitTransitionKernelFactWithImports - :: NonEmpty Marker - -> Origin - -> Vector TransitionDerivationImport - -> FrozenCheckedCore CheckedGlobalRef - -> KernelDerivation CheckedGlobalRef - -> TransitionModuleBuilder - -> Either TransitionModuleError TransitionModuleBuilder -commitTransitionKernelFactWithImports - aliases - factOrigin - imports - target - derivation - builder = do - admitted <- - authorizeTransitionKernelFactWithImports - imports - target - derivation - builder - insertTransitionTypedFact - aliases - factOrigin - admitted - builder - -data TransitionDerivationImport = - TransitionDerivationImport - !TransitionFactRef - !(DerivationImportJudgment CheckedGlobalRef) - deriving stock (Eq) - -transitionDerivationImport - :: TransitionFactRef - -> FrozenCheckedCore CheckedGlobalRef - -> Either - TransitionModuleError - TransitionDerivationImport -transitionDerivationImport reference statement = - TransitionDerivationImport reference - <$> first - TransitionDerivationImportError - (derivationImportJudgment statement) - -lookupTransitionTypedImport - :: FrozenCheckedCore CheckedGlobalRef - -> TransitionModuleBuilder - -> Either - TransitionModuleError - (Maybe TransitionDerivationImport) -lookupTransitionTypedImport statement builder = - case Vector.find - ((== Just statement) - . admittedFactStatement - . entryFact) - (builderVisibleFacts builder) of - Nothing -> - Right Nothing - Just - (TransitionFactEntry - fact@(TypedFactRow _reference admitted) - _registration) -> do - unless - (typedAdmittedStatement admitted - == statement) - (Left TransitionKernelTargetMismatch) - Just - <$> transitionDerivationImport - (admittedFactReference fact) - statement - Just (TransitionFactEntry LegacyFactRow{} _registration) -> - Right Nothing - where - entryFact - (TransitionFactEntry fact _registration) = - fact - -authorizeTransitionKernelFactWithImports - :: Vector TransitionDerivationImport - -> FrozenCheckedCore CheckedGlobalRef - -> KernelDerivation CheckedGlobalRef - -> TransitionModuleBuilder - -> Either TransitionModuleError TypedAdmittedFact -authorizeTransitionKernelFactWithImports - imports - target - derivation - builder = do - authorizeTransitionKernelFactWithImportsAndProvenance - defaultKernelReplayLimits - Nothing - imports - target - derivation - builder - -authorizeTransitionKernelFactWithImportsAndProvenance - :: KernelReplayLimits - -> Maybe SessionTypedReconstructionProvenance - -> Vector TransitionDerivationImport - -> FrozenCheckedCore CheckedGlobalRef - -> KernelDerivation CheckedGlobalRef - -> TransitionModuleBuilder - -> Either TransitionModuleError TypedAdmittedFact -authorizeTransitionKernelFactWithImportsAndProvenance - replayLimits - provenance - imports - target - derivation - builder = do - semantic <- - prepareTypedSemanticFact builder target - let checkedTarget = - typedSemanticStatement semantic - replayed <- - first TransitionKernelReplayError - (replayKernelDerivation - (builderFoundation builder) - replayLimits - (builderGlobalType builder) - (derivationImport - <$> imports) - checkedTarget - derivation) - inheritedTrust <- - foldM - (\trust index -> - (trust <>) - <$> authorizeUsedImport - imports - builder - index) - mempty - (Set.toAscList - (replayedKernelImportUses replayed)) - let foundationTrust = - mempty - { typedFoundationUses = - replayedKernelFoundationUses replayed - , typedKernelRuleUses = - replayedKernelRuleUses replayed - } - authorization = - AuthorizedKernelReplay - (replayedKernelTarget replayed) - (Set.fromList - [ reference - | index <- - Set.toAscList - (replayedKernelImportUses replayed) - , Right - (TransitionDerivationImport - (TransitionTypedFactRef reference) - _judgment) <- - [transitionImportAt imports index] - ]) - (replayedKernelFoundationUses replayed) - (replayedKernelRuleUses replayed) - (replayedKernelNodeCount replayed) - (replayedKernelMaximumDepth replayed) - provenance - unless - (typedSemanticStatement semantic - == replayedKernelTarget replayed) - (Left TransitionKernelTargetMismatch) - pure - (TypedAdmittedFact - semantic - (KernelProof - authorization - (inheritedTrust <> foundationTrust))) - -typedAdmittedStatement - :: TypedAdmittedFact - -> FrozenCheckedCore CheckedGlobalRef -typedAdmittedStatement - (TypedAdmittedFact semantic _authorization) = - typedSemanticStatement semantic - -typedAdmittedTrustDependencies - :: TypedAdmittedFact - -> TypedTrustDependencies -typedAdmittedTrustDependencies - (TypedAdmittedFact _semantic authorization) = - factAuthorizationTrust authorization - -data AdmittedFact - = LegacyFactRow - !TransitionFactRef - !H1LegacyAdmittedFact - | TypedFactRow - !TransitionFactRef - !TypedAdmittedFact - deriving stock (Eq) - -admittedFactReference - :: AdmittedFact - -> TransitionFactRef -admittedFactReference = \case - LegacyFactRow reference _admitted -> - reference - TypedFactRow reference _admitted -> - reference - -admittedFactIsKernelProof :: AdmittedFact -> Bool -admittedFactIsKernelProof = \case - LegacyFactRow{} -> - False - TypedFactRow _reference - (TypedAdmittedFact _semantic authorization) -> - case authorization of - KernelProof{} -> - True - DeclaredAssumption{} -> - False - TrustedVampire{} -> - False - -admittedFactIsReconstructedKernelProof :: AdmittedFact -> Bool -admittedFactIsReconstructedKernelProof = \case - LegacyFactRow{} -> - False - TypedFactRow _reference - (TypedAdmittedFact _semantic authorization) -> - case authorization of - KernelProof - (AuthorizedKernelReplay - _target - _imports - _foundation - _rules - _nodes - _depth - (Just _provenance)) - _trust -> - True - KernelProof{} -> - False - DeclaredAssumption{} -> - False - TrustedVampire{} -> - False - -admittedFactIsTrustedVampire :: AdmittedFact -> Bool -admittedFactIsTrustedVampire = \case - LegacyFactRow{} -> - False - TypedFactRow _reference - (TypedAdmittedFact _semantic authorization) -> - case authorization of - KernelProof{} -> - False - DeclaredAssumption{} -> - False - TrustedVampire{} -> - True - -admittedFactTypedTrustDependencies - :: AdmittedFact - -> Maybe TypedTrustDependencies -admittedFactTypedTrustDependencies = \case - LegacyFactRow{} -> - Nothing - TypedFactRow _reference admitted -> - Just (typedAdmittedTrustDependencies admitted) - -admittedFactStatement - :: AdmittedFact - -> Maybe (FrozenCheckedCore CheckedGlobalRef) -admittedFactStatement = \case - LegacyFactRow{} -> - Nothing - TypedFactRow _reference admitted -> - Just (typedAdmittedStatement admitted) - -factAuthorizationTrust - :: FactAuthorization - -> TypedTrustDependencies -factAuthorizationTrust = \case - KernelProof _replay trust -> - trust - DeclaredAssumption reference -> - mempty - { typedDeclaredAssumptionUses = - Set.singleton reference - } - TrustedVampire - (SessionTypedTrustedVampireEvidence - _reference - _target - _prepared - _accepted - trust - _fallback) -> - trust - -derivationImport - :: TransitionDerivationImport - -> DerivationImportJudgment CheckedGlobalRef -derivationImport - (TransitionDerivationImport _reference judgment) = - judgment - -transitionImportAt - :: Vector TransitionDerivationImport - -> ImportIx - -> Either - TransitionModuleError - TransitionDerivationImport -transitionImportAt imports index - | naturalIndex > - fromIntegral (maxBound :: Int) = - Left - (TransitionKernelImportIndexOutOfBounds - index) - | otherwise = - maybe - (Left - (TransitionKernelImportIndexOutOfBounds - index)) - Right - (imports Vector.!? fromIntegral naturalIndex) - where - naturalIndex = - importIxValue index - -authorizeUsedImport - :: Vector TransitionDerivationImport - -> TransitionModuleBuilder - -> ImportIx - -> Either - TransitionModuleError - TypedTrustDependencies -authorizeUsedImport imports builder index = do - TransitionDerivationImport reference judgment <- - transitionImportAt imports index - case reference of - TransitionLegacyFactRef{} -> - Left - (TransitionDependencyNotMigrated - reference) - TransitionTypedFactRef _typedReference -> do - TransitionFactEntry fact _registration <- - maybe - (Left - (TransitionKernelImportNotVisible - reference)) - Right - (lookupBuilderFact reference builder) - case fact of - LegacyFactRow{} -> - Left - (TransitionDependencyNotMigrated - reference) - TypedFactRow rowReference admitted -> do - unless - (rowReference == reference - && typedAdmittedStatement admitted - == derivationImportStatement - judgment) - (Left - (TransitionKernelImportDoesNotMatch - reference)) - pure - (typedAdmittedTrustDependencies - admitted) - -builderVisibleFacts - :: TransitionModuleBuilder - -> Vector TransitionFactEntry -builderVisibleFacts = - Vector.fromList - . toList - . inventoryFactOrder - . builderFactInventory - -lookupBuilderFact - :: TransitionFactRef - -> TransitionModuleBuilder - -> Maybe TransitionFactEntry -lookupBuilderFact reference = - Map.lookup reference - . inventoryFactsByReference - . builderFactInventory - -data TransitionFactRegistration = TransitionFactRegistration - !(NonEmpty Marker) - !Origin - deriving stock (Eq) - -data TransitionFactEntry = TransitionFactEntry - !AdmittedFact - !TransitionFactRegistration - deriving stock (Eq) - -data TransitionFactInventory = TransitionFactInventory - { inventoryFactsByReference - :: !(Map TransitionFactRef TransitionFactEntry) - , inventoryAliases - :: !(Map Marker (TransitionFactRef, Origin)) - , inventoryFactOrder :: !(Seq TransitionFactEntry) - , inventoryFofOrder :: !(Seq TransitionFactRef) - } - -emptyTransitionFactInventory :: TransitionFactInventory -emptyTransitionFactInventory = - TransitionFactInventory - { inventoryFactsByReference = Map.empty - , inventoryAliases = Map.empty - , inventoryFactOrder = Seq.empty - , inventoryFofOrder = Seq.empty - } - -insertTransitionFactEntry - :: TransitionFactEntry - -> TransitionFactInventory - -> Either TransitionModuleError TransitionFactInventory -insertTransitionFactEntry - entry@(TransitionFactEntry - fact - (TransitionFactRegistration - aliases - factOrigin)) - inventory = - case Map.lookup - reference - (inventoryFactsByReference inventory) of - Just previous - | previous == entry -> - Right inventory - | otherwise -> - Left - (TransitionFactReferenceConflict - reference) - Nothing -> do - aliases' <- - insertFactAliases - reference - factOrigin - aliases - (inventoryAliases inventory) - pure - inventory - { inventoryFactsByReference = - Map.insert - reference - entry - (inventoryFactsByReference - inventory) - , inventoryAliases = aliases' - , inventoryFactOrder = - inventoryFactOrder inventory - Seq.|> entry - , inventoryFofOrder = - case typedFofReference fact of - Nothing -> - inventoryFofOrder inventory - Just fofReference -> - inventoryFofOrder inventory - Seq.|> fofReference - } - where - reference = - admittedFactReference fact - - typedFofReference = \case - LegacyFactRow{} -> - Nothing - TypedFactRow rowReference - (TypedAdmittedFact - semantic - _authorization) -> - case typedSemanticFofCapability semantic of - Backend.FofProjectable{} -> - Just rowReference - Backend.RequiresTh0{} -> - Nothing - -data TypedGlobalBinding = TypedGlobalBinding - !Symbol - !CheckedGlobalRef - !Origin - !(Maybe (FrozenCheckedCore CheckedGlobalRef)) - deriving stock (Eq) - -instance Show TypedGlobalBinding where - show - (TypedGlobalBinding - symbol - reference - bindingOrigin - body) = - "TypedGlobalBinding " - <> show symbol - <> " " - <> show reference - <> " " - <> show bindingOrigin - <> if isJust body - then " Transparent" - else " Opaque" - -data TypedModuleEnvironmentDelta = - TypedModuleEnvironmentDelta - !ModuleName - !(Vector TypedGlobalBinding) - deriving stock (Show, Eq) - -data TransitionModuleBuilder = TransitionModuleBuilder - { builderFoundation :: !CheckedFoundation - , builderName :: !ModuleName - , builderLegacyStage :: !LegacyModuleStage - , builderEnvironmentDeltas - :: !(Vector TypedModuleEnvironmentDelta) - , builderGlobals :: !(Map Symbol TypedGlobalBinding) - , builderGlobalDeclarations - :: !(Map OpaqueDeclarationRef TypedGlobalBinding) - , builderLocalGlobalsReversed :: ![TypedGlobalBinding] - , builderFactInventory :: !TransitionFactInventory - , builderLocalFactsReversed :: ![TransitionFactEntry] - , builderTypedDirectAxiomManifestReversed - :: ![TypedDirectAxiomManifestEntry] - , builderNextTypedFact :: !Natural - , builderNextTypedAssumption :: !Natural - , builderNextDeclaration :: !Natural - , builderCurrentDeclaration - :: !(Maybe OpaqueDeclarationRef) - } - -openTransitionModuleBuilder - :: CheckedFoundation - -> LegacyCheckingEnvironment - -> LegacyModuleAssignment - -> [TransitionAdmittedModule] - -> Either TransitionModuleError TransitionModuleBuilder -openTransitionModuleBuilder - checkedFoundationValue - foundation - assignment - directImports = - checkedFoundationValue `seq` do - importedView <- - first TransitionLegacyModuleError - (legacyImportedView - foundation - (transitionAdmittedLegacyModule <$> directImports)) - (environmentDeltas, globals, globalDeclarations) <- - mergeTypedEnvironments directImports - factInventory <- - mergeTransitionFacts directImports - let address = - legacyStageSourceAddress legacyStage - name = - moduleName address - legacyStage = - openLegacyModuleStage assignment importedView - pure - TransitionModuleBuilder - { builderFoundation = - checkedFoundationValue - , builderName = name - , builderLegacyStage = legacyStage - , builderEnvironmentDeltas = - environmentDeltas - , builderGlobals = globals - , builderGlobalDeclarations = - globalDeclarations - , builderLocalGlobalsReversed = [] - , builderFactInventory = factInventory - , builderLocalFactsReversed = [] - , builderTypedDirectAxiomManifestReversed = [] - , builderNextTypedFact = 0 - , builderNextTypedAssumption = 0 - , builderNextDeclaration = 0 - , builderCurrentDeclaration = Nothing - } - -transitionBuilderLegacyStage - :: TransitionModuleBuilder - -> LegacyModuleStage -transitionBuilderLegacyStage - builder = - builderLegacyStage builder - -transitionBuilderImportedCheckingEnvironment - :: TransitionModuleBuilder - -> LegacyCheckingEnvironment -transitionBuilderImportedCheckingEnvironment = - legacyStageImportedCheckingEnvironment - . transitionBuilderLegacyStage - -transitionBuilderFoundation - :: TransitionModuleBuilder - -> CheckedFoundation -transitionBuilderFoundation = - builderFoundation - -builderGlobalType - :: TransitionModuleBuilder - -> CheckedGlobalRef - -> Maybe CoreType -builderGlobalType builder reference = - case Map.lookup - (checkedGlobalReference reference) - (builderGlobalDeclarations builder) of - Just - (TypedGlobalBinding - _symbol - authoritative - _origin - _body) - | checkedGlobalType reference - == checkedGlobalType authoritative -> - Just (checkedGlobalType authoritative) - _ -> - Nothing - -validateBuilderGlobalReference - :: TransitionModuleBuilder - -> CheckedGlobalRef - -> Either TransitionModuleError CoreType -validateBuilderGlobalReference builder reference = - case Map.lookup - (checkedGlobalReference reference) - (builderGlobalDeclarations builder) of - Nothing -> - Left - (TransitionGlobalReferenceNotVisible - reference) - Just - (TypedGlobalBinding - _symbol - authoritative - _origin - _body) - | checkedGlobalType reference - == checkedGlobalType authoritative -> - Right (checkedGlobalType authoritative) - | otherwise -> - Left - (TransitionGlobalReferenceTypeMismatch - reference - (checkedGlobalType authoritative)) - -validateBuilderCanonicalGlobals - :: TransitionModuleBuilder - -> CanonicalTerm CheckedGlobalRef - -> Either TransitionModuleError () -validateBuilderCanonicalGlobals builder = - traverse_ - (void . validateBuilderGlobalReference builder) - . Set.toAscList - . canonicalTermGlobals - -recheckBuilderFrozenCore - :: TransitionModuleBuilder - -> FrozenCheckedCore CheckedGlobalRef - -> Either - TransitionModuleError - (FrozenCheckedCore CheckedGlobalRef) -recheckBuilderFrozenCore builder supplied = do - validateBuilderCanonicalGlobals - builder - (frozenCoreTerm supplied) - first TransitionCoreCheckError - (checkCanonicalCore - (builderGlobalType builder) - (frozenCoreTerm supplied)) - -data GlobalPremisePolicy - = ImplicitFofFacts - | ExplicitFacts !(NonEmpty Marker) - | NoGlobalFacts - deriving stock (Show, Eq) - -planTransitionTypedProblem - :: Ord local - => TransitionModuleBuilder - -> Backend.SupportedProposition - local - CheckedGlobalRef - -> [ Backend.TypedLocalPremise - local - Origin - CheckedGlobalRef - ] - -> [ Backend.TypedFoundationAuxiliaryInput - CheckedGlobalRef - ] - -> GlobalPremisePolicy - -> Backend.LocalPremisePolicy - -> Either - (TransitionTypedProblemError local) - (Backend.TypedProblem - TransitionFactRef - local - Origin - CheckedGlobalRef) -planTransitionTypedProblem - builder - claim - localPremises - auxiliaries - globalPolicy - localPolicy = do - first TransitionTypedProblemGlobalValidationError - (do - validateBuilderCanonicalGlobals - builder - (Backend.supportedPropositionTerm claim) - traverse_ - ( validateBuilderCanonicalGlobals builder - . Backend.supportedPropositionTerm - . Backend.typedLocalPremiseProposition - ) - localPremises) - (selectedFacts, premiseMode) <- - selectTransitionBackendFacts - builder - globalPolicy - first TransitionTypedProblemPlanningError - (Backend.planTypedProblem - (builderGlobalType builder) - selectedFacts - claim - localPremises - auxiliaries - premiseMode - localPolicy) - -selectTransitionBackendFacts - :: TransitionModuleBuilder - -> GlobalPremisePolicy - -> Either - (TransitionTypedProblemError local) - ( Vector - (Backend.TypedBackendFact - TransitionFactRef - CheckedGlobalRef) - , Backend.GlobalPremiseMode - ) -selectTransitionBackendFacts builder policy = do - references <- - case policy of - ImplicitFofFacts -> - Right - (toList - (inventoryFofOrder inventory)) - ExplicitFacts aliases -> - stableUnique - <$> traverse resolveAlias (toList aliases) - NoGlobalFacts -> - Right [] - facts <- - Vector.fromList - <$> traverse resolveFact references - pure - ( facts - , case policy of - ImplicitFofFacts -> - Backend.ImplicitFofPremises - ExplicitFacts{} -> - Backend.ExplicitGlobalPremises - NoGlobalFacts -> - Backend.NoGlobalPremises - ) - where - inventory = - builderFactInventory builder - - resolveAlias alias = - case Map.lookup alias (inventoryAliases inventory) of - Nothing -> - Left - (TransitionTypedProblemUnknownFactAlias - alias) - Just (reference, _origin) -> - Right reference - - resolveFact reference = - case Map.lookup - reference - (inventoryFactsByReference inventory) of - Nothing -> - Left - (TransitionTypedProblemFactReferenceMissing - reference) - Just (TransitionFactEntry LegacyFactRow{} _registration) -> - Left - (TransitionTypedProblemDependencyNotMigrated - reference) - Just - (TransitionFactEntry - (TypedFactRow rowReference - (TypedAdmittedFact - semantic - _authorization)) - _registration) - | rowReference == reference -> - Right - (Backend.typedBackendFact - reference - (typedSemanticProposition semantic) - (typedSemanticFofCapability semantic)) - | otherwise -> - Left - (TransitionTypedProblemFactReferenceMissing - reference) - - stableUnique = - reverse . snd - . foldl' - (\(seen, reversed) reference -> - if reference `Set.member` seen - then (seen, reversed) - else - ( Set.insert reference seen - , reference : reversed - )) - (Set.empty, []) - -data TransitionTypedProblemError local - = TransitionTypedProblemGlobalValidationError - !TransitionModuleError - | TransitionTypedProblemUnknownFactAlias - !Marker - | TransitionTypedProblemDependencyNotMigrated - !TransitionFactRef - | TransitionTypedProblemFactReferenceMissing - !TransitionFactRef - | TransitionTypedProblemPlanningError - !(Backend.TypedProblemError - local - CheckedGlobalRef) - deriving stock (Show, Eq) - -beginTransitionDeclaration - :: TransitionModuleBuilder - -> TransitionModuleBuilder -beginTransitionDeclaration - builder = - builder - { builderNextDeclaration = - nextDeclaration + 1 - , builderCurrentDeclaration = - Just - (OpaqueDeclarationRef - (builderName builder) - (localDeclarationOrdinal - nextDeclaration)) - } - where - nextDeclaration = - builderNextDeclaration builder - -transitionCurrentDeclarationReference - :: TransitionModuleBuilder - -> Maybe OpaqueDeclarationRef -transitionCurrentDeclarationReference - builder = - builderCurrentDeclaration builder - -commitTransitionOpaqueGlobal - :: Symbol - -> CoreType - -> Origin - -> TransitionModuleBuilder - -> Either TransitionModuleError TransitionModuleBuilder -commitTransitionOpaqueGlobal - symbol - coreType - bindingOrigin - builder = - commitTransitionGlobal - symbol - coreType - bindingOrigin - Nothing - builder - -commitTransitionTransparentGlobal - :: Symbol - -> CoreType - -> FrozenCheckedCore CheckedGlobalRef - -> Origin - -> TransitionModuleBuilder - -> Either TransitionModuleError TransitionModuleBuilder -commitTransitionTransparentGlobal - symbol - coreType - body - bindingOrigin - builder = do - checkedBody <- - recheckBuilderFrozenCore builder body - unless - (frozenCoreType checkedBody == coreType) - (Left - (TransitionTransparentGlobalTypeMismatch - symbol - coreType - (frozenCoreType checkedBody))) - commitTransitionGlobal - symbol - coreType - bindingOrigin - (Just checkedBody) - builder - -commitTransitionGlobal - :: Symbol - -> CoreType - -> Origin - -> Maybe (FrozenCheckedCore CheckedGlobalRef) - -> TransitionModuleBuilder - -> Either TransitionModuleError TransitionModuleBuilder -commitTransitionGlobal - symbol - coreType - bindingOrigin - body - builder = - case transitionCurrentDeclarationReference builder of - Nothing -> - Left TransitionDeclarationNotOpen - Just reference -> do - let binding = - TypedGlobalBinding - symbol - (CheckedOpaqueGlobal - reference - coreType) - bindingOrigin - body - case Map.lookup symbol - (builderGlobals builder) of - Just previous -> - Left - (globalSymbolConflict - previous - binding) - Nothing -> - pure () - case Map.lookup reference - (builderGlobalDeclarations builder) of - Just previous -> - Left - (globalReferenceConflict - previous - binding) - Nothing -> - pure () - (globals, declarations) <- - insertVisibleGlobalBinding - ( builderGlobals builder - , builderGlobalDeclarations builder - ) - binding - Right - builder - { builderGlobals = globals - , builderGlobalDeclarations = - declarations - , builderLocalGlobalsReversed = - binding - : builderLocalGlobalsReversed - builder - } - -insertTransitionTypedFact - :: NonEmpty Marker - -> Origin - -> TypedAdmittedFact - -> TransitionModuleBuilder - -> Either TransitionModuleError TransitionModuleBuilder -insertTransitionTypedFact aliases factOrigin admitted builder = do - factReference <- - nextTransitionTypedFactReference builder - let ordinal = - builderNextTypedFact builder - reference = - TransitionTypedFactRef - factReference - registration = - TransitionFactRegistration - aliases - factOrigin - entry = - TransitionFactEntry - (TypedFactRow reference admitted) - registration - inventory' <- - insertTransitionFactEntry - entry - (builderFactInventory builder) - Right - builder - { builderLocalFactsReversed = - entry - : builderLocalFactsReversed - builder - , builderFactInventory = inventory' - , builderNextTypedFact = ordinal + 1 - } - -commitTransitionTypedVampireFact - :: BackendReconstruction.ReconstructionPolicy - -> NonEmpty Marker - -> Origin - -> FrozenCheckedCore CheckedGlobalRef - -> Provers.PreparedTypedProverTask - TransitionFactRef - Void - inputOrigin - CheckedGlobalRef - -> Provers.AcceptedVampireRun - -> TransitionModuleBuilder - -> Either TransitionModuleError TransitionModuleBuilder -commitTransitionTypedVampireFact - reconstructionPolicy - aliases - factOrigin - target - preparedTask - accepted - builder = do - semantic <- - prepareTypedSemanticFact builder target - let checkedTarget = - typedSemanticStatement semantic - let problem = - Provers.preparedTypedProverLogicalProblem - preparedTask - claim = - Backend.typedProblemClaim problem - unless - ( Vector.null - (Backend.supportedPropositionSupport - claim) - && Backend.supportedPropositionTerm claim - == frozenCoreTerm checkedTarget - ) - (Left TransitionTypedVampireTargetMismatch) - unless - (Provers.acceptedVampireRequest accepted - == Provers.preparedTypedProverRequest - preparedTask) - (Left TransitionTypedVampireRequestMismatch) - unless - (Vector.null - (Backend.typedProblemLocalPremises - problem)) - (Left TransitionTypedVampireHasOpenLocalPremises) - traverse_ - validateGlobalType - (Map.toList - (Backend.typedProblemGlobalTypes - problem)) - validatedPremises <- - traverse - validateSelectedFact - (Backend.typedProblemGlobalPremises - problem) - foundationTrust <- - foldM - (\tags auxiliary -> - (tags <>) - <$> validateFoundationAuxiliary - auxiliary) - mempty - (Backend.typedProblemAuxiliaries - problem) - let imports = - fst <$> validatedPremises - premiseTrust = - foldMap snd validatedPremises - case BackendReconstruction.attemptVampireReconstruction - reconstructionPolicy - preparedTask - accepted of - BackendReconstruction.ReconstructionSucceeded - reconstructed -> - commitReconstructed - reconstructionPolicy - semantic - premiseTrust - foundationTrust - imports - checkedTarget - reconstructed - BackendReconstruction.ReconstructionUnsupported - unsupported -> - commitTrusted - semantic - premiseTrust - foundationTrust - (ReconstructionFallbackUnsupported - unsupported) - BackendReconstruction.ReconstructionUnavailable - searchStats -> - commitTrusted - semantic - premiseTrust - foundationTrust - (ReconstructionFallbackUnavailable - searchStats) - BackendReconstruction.ReconstructionExhausted - exhaustion - searchStats -> - commitTrusted - semantic - premiseTrust - foundationTrust - (ReconstructionFallbackSearchExhausted - exhaustion - searchStats) - BackendReconstruction.ReconstructionDefinitiveMismatch - mismatch -> - Left - (TransitionTypedReconstructionMismatch - mismatch) - where - commitReconstructed - policy - semantic - premiseTrust - foundationTrust - imports - checkedTarget - reconstructed = do - let connectionReplay = - BackendReconstruction.reconstructedConnectionReplay - reconstructed - provenance = - SessionTypedReconstructionProvenance - policy - (Provers.preparedTypedProverTptpProblem - (BackendReconstruction.reconstructedPreparedTask - reconstructed)) - (BackendReconstruction.reconstructedAcceptedRun - reconstructed) - (BackendReconstruction.reconstructedConnectionTrace - reconstructed) - (BackendReconstruction.reconstructedSearchStats - reconstructed) - (BackendConnection.replayedConnectionNodeCount - connectionReplay) - (BackendConnection.replayedConnectionMaximumDepth - connectionReplay) - case authorizeTransitionKernelFactWithImportsAndProvenance - (BackendReconstruction.reconstructionPolicyKernelReplayLimits - policy) - (Just provenance) - imports - checkedTarget - (BackendConnection.replayedConnectionDerivation - connectionReplay) - builder of - Left - (TransitionKernelReplayError replayError) - | isKernelReplayExhaustion replayError -> - commitTrusted - semantic - premiseTrust - foundationTrust - (ReconstructionFallbackKernelReplayExhausted - replayError) - Left transitionError -> - Left transitionError - Right admitted -> - insertTransitionTypedFact - aliases - factOrigin - admitted - builder - - commitTrusted - semantic - premiseTrust - foundationTrust - fallbackReason = do - factReference <- - nextTransitionTypedFactReference builder - let trust = - premiseTrust - <> mempty - { typedTrustedVampireUses = - Set.singleton - (SessionTypedTrustedVampireUse - factReference) - , typedVampireLoweringUses = - mandatoryVampireLoweringAssumptions - , typedFoundationUses = - foundationTrust - } - admitted = - TypedAdmittedFact - semantic - (TrustedVampire - (SessionTypedTrustedVampireEvidence - factReference - (typedSemanticStatement semantic) - (Provers.preparedTypedProverTptpProblem - preparedTask) - accepted - trust - (SessionTypedReconstructionFallback - reconstructionPolicy - fallbackReason))) - insertTransitionTypedFact - aliases - factOrigin - admitted - builder - - isKernelReplayExhaustion = \case - KernelReplayNodeLimitExceeded{} -> - True - KernelReplayDepthLimitExceeded{} -> - True - _ -> - False - - validateGlobalType (global, reportedType) = do - authoritativeType <- - validateBuilderGlobalReference - builder - global - unless - (authoritativeType == reportedType) - (Left - (TransitionTypedVampireGlobalTypeMismatch - global - reportedType)) - - validateSelectedFact selected = - case lookupBuilderFact reference builder of - Nothing -> - Left - (TransitionTypedVampireFactNotVisible - reference) - Just - (TransitionFactEntry - LegacyFactRow{} - _registration) -> - Left - (TransitionDependencyNotMigrated - reference) - Just - (TransitionFactEntry - (TypedFactRow - rowReference - admitted) - _registration) -> do - semantic <- - prepareTypedSemanticFact - builder - (typedAdmittedStatement - admitted) - let selectedProposition = - Backend.typedBackendFactProposition - selected - selectedCapability = - Backend.typedBackendFactCapability - selected - unless - ( rowReference == reference - && frozenCoreTerm - (typedSemanticStatement - semantic) - == Backend.supportedPropositionTerm - selectedProposition - && typedSemanticFofCapability - semantic - == selectedCapability - ) - (Left - (TransitionTypedVampireFactMismatch - reference)) - typedImport <- - transitionDerivationImport - reference - (typedSemanticStatement - semantic) - pure - ( typedImport - , typedAdmittedTrustDependencies - admitted - ) - where - reference = - Backend.typedBackendFactReference - selected - - validateFoundationAuxiliary auxiliary = do - let tag = - Backend.typedProblemAuxiliaryTag - auxiliary - actual = - Backend.supportedPropositionTerm - (Backend.typedProblemAuxiliaryProposition - auxiliary) - expected = - frozenCoreTerm - (mapFrozenGlobals - absurd - (foundationAxiomFrozen - (builderFoundation builder) - tag)) - unless - (actual == expected) - (Left - (TransitionTypedVampireFoundationMismatch - tag)) - pure (Set.singleton tag) - -nextTransitionTypedFactReference - :: TransitionModuleBuilder - -> Either TransitionModuleError FactRef -nextTransitionTypedFactReference builder = do - void - (maybe - (Left TransitionDeclarationNotOpen) - Right - (transitionCurrentDeclarationReference builder)) - let ordinal = - builderNextTypedFact builder - pure - (FactRef - (builderName builder) - (localFactOrdinal ordinal)) - -commitTransitionTypedDeclaredAssumption - :: NonEmpty Marker - -> Origin - -> AssumptionKind - -> FrozenCheckedCore CheckedGlobalRef - -> TransitionModuleBuilder - -> Either TransitionModuleError TransitionModuleBuilder -commitTransitionTypedDeclaredAssumption - aliases - factOrigin - kind - statement - builder = do - semantic <- - prepareTypedSemanticFact builder statement - factReference <- - nextTransitionTypedFactReference builder - let checkedStatement = - typedSemanticStatement semantic - assumptionOrdinal = - LocalAssumptionOrdinal - (builderNextTypedAssumption builder) - manifestEntry = - TypedDirectAxiomManifestEntry - factReference - kind - checkedStatement - sessionReference = - SessionTypedDeclaredAssumptionRef - factReference - assumptionOrdinal - kind - checkedStatement - admitted = - TypedAdmittedFact - semantic - (DeclaredAssumption - sessionReference) - builder' <- - insertTransitionTypedFact - aliases - factOrigin - admitted - builder - pure - builder' - { builderTypedDirectAxiomManifestReversed = - manifestEntry - : builderTypedDirectAxiomManifestReversed - builder' - , builderNextTypedAssumption = - builderNextTypedAssumption builder + 1 - } - -transitionBuilderWithLegacyStage - :: LegacyModuleStage - -> TransitionModuleBuilder - -> Either TransitionModuleError TransitionModuleBuilder -transitionBuilderWithLegacyStage newStage builder - | legacyStageSourceAddress newStage - /= legacyStageSourceAddress - (builderLegacyStage builder) = - Left TransitionLegacyStageAddressMismatch - | Vector.take oldCount newFacts /= oldFacts = - Left TransitionLegacyStageIsNotAnExtension - | otherwise = do - (reversedFacts, inventory) <- - foldM - appendLegacyEntry - ( builderLocalFactsReversed builder - , builderFactInventory builder - ) - (Vector.toList - (Vector.drop oldCount newFacts)) - Right - builder - { builderLegacyStage = newStage - , builderLocalFactsReversed = - reversedFacts - , builderFactInventory = inventory - } - where - oldFacts = - legacyStageLocalFacts - (builderLegacyStage builder) - oldCount = - Vector.length oldFacts - newFacts = - legacyStageLocalFacts newStage - - appendLegacyEntry (reversedFacts, inventory) legacyEntry = do - let staged = - legacyFactEntryStagedFact legacyEntry - reference = - TransitionLegacyFactRef - (legacyFactEntryReference - legacyEntry) - factOrigin = - originFromLegacyStagedFact staged - entry = - TransitionFactEntry - (LegacyFactRow - reference - (legacyFactEntryAdmittedFact - legacyEntry)) - (TransitionFactRegistration - (Facts.stagedFactAliases staged) - factOrigin) - inventory' <- - insertTransitionFactEntry - entry - inventory - pure (entry : reversedFacts, inventory') - -lookupTransitionGlobal - :: Symbol - -> TransitionModuleBuilder - -> Maybe CheckedGlobalRef -lookupTransitionGlobal symbol builder = - bindingReference - <$> Map.lookup symbol (builderGlobals builder) - where - bindingReference - (TypedGlobalBinding - _symbol - reference - _origin - _body) = - reference - -lookupTransitionGlobalBody - :: Symbol - -> TransitionModuleBuilder - -> Maybe (FrozenCheckedCore CheckedGlobalRef) -lookupTransitionGlobalBody symbol builder = do - TypedGlobalBinding - _bindingSymbol - _reference - _origin - body <- - Map.lookup symbol (builderGlobals builder) - body - - -data TransitionAdmittedModule = TransitionAdmittedModule - { admittedName :: !ModuleName - , admittedLegacyModule :: !LegacyAdmittedModule - , admittedEnvironmentDeltas - :: !(Vector TypedModuleEnvironmentDelta) - , admittedLocalGlobals :: !(Vector TypedGlobalBinding) - , admittedVisibleFacts :: !(Vector TransitionFactEntry) - , admittedTypedDirectAxiomManifest - :: !(Vector TypedDirectAxiomManifestEntry) - } - -sealTransitionModule - :: LegacyCheckingEnvironment - -> TransitionModuleBuilder - -> Either TransitionModuleError TransitionAdmittedModule -sealTransitionModule finalEnvironment builder = do - legacyAdmitted <- - first TransitionLegacyModuleError - (sealLegacyModuleStage - finalEnvironment - (builderLegacyStage builder)) - let localBindings = - Vector.fromList - (reverse - (builderLocalGlobalsReversed - builder)) - localDelta = - TypedModuleEnvironmentDelta - (builderName builder) - localBindings - localFacts = - Vector.fromList - (reverse - (builderLocalFactsReversed - builder)) - visibleFacts = - builderVisibleFacts builder - typedManifest = - Vector.fromList - (reverse - (builderTypedDirectAxiomManifestReversed - builder)) - actualLegacyReferences = - [ reference - | TransitionFactEntry - (LegacyFactRow - (TransitionLegacyFactRef reference) - _admitted) - _registration <- - Vector.toList localFacts - ] - expectedLegacyReferences = - legacyFactEntryReference - <$> Vector.toList - (legacyAdmittedLocalFacts - legacyAdmitted) - unless - (actualLegacyReferences - == expectedLegacyReferences) - (Left TransitionLegacyFactOrderMismatch) - validateTypedDirectAxiomManifest - localFacts - typedManifest - pure - TransitionAdmittedModule - { admittedName = builderName builder - , admittedLegacyModule = legacyAdmitted - , admittedEnvironmentDeltas = - Vector.snoc - (builderEnvironmentDeltas builder) - localDelta - , admittedLocalGlobals = localBindings - , admittedVisibleFacts = visibleFacts - , admittedTypedDirectAxiomManifest = - typedManifest - } - -transitionAdmittedName - :: TransitionAdmittedModule - -> ModuleName -transitionAdmittedName = - admittedName - -transitionAdmittedLegacyModule - :: TransitionAdmittedModule - -> LegacyAdmittedModule -transitionAdmittedLegacyModule = - admittedLegacyModule - -transitionAdmittedFacts - :: TransitionAdmittedModule - -> Vector AdmittedFact -transitionAdmittedFacts = - fmap entryFact . admittedVisibleFacts - where - entryFact - (TransitionFactEntry fact _registration) = - fact - -transitionAdmittedKernelProofCount - :: TransitionAdmittedModule - -> Int -transitionAdmittedKernelProofCount = - Vector.length - . Vector.filter admittedFactIsKernelProof - . transitionAdmittedFacts - -transitionAdmittedTypedTrustedVampireCount - :: TransitionAdmittedModule - -> Int -transitionAdmittedTypedTrustedVampireCount = - Vector.length - . Vector.filter admittedFactIsTrustedVampire - . transitionAdmittedFacts - --- | Replay work retained by the admitted root module's visible fact closure. -data TransitionReplayMeasurements = - TransitionReplayMeasurements - { transitionKernelReplayCount :: !Int - , transitionKernelReplayNodeCount :: !Natural - , transitionKernelReplayMaximumDepth :: !Natural - , transitionReconstructionCount :: !Int - , transitionReconstructionSearchWork :: !Natural - , transitionReconstructionDerivedAtomCount :: !Natural - , transitionReconstructionMaximumCandidateDepth :: !Natural - , transitionConnectionReplayNodeCount :: !Natural - , transitionConnectionReplayMaximumDepth :: !Natural - } - deriving stock (Show, Eq) - -transitionAdmittedReplayMeasurements - :: TransitionAdmittedModule - -> TransitionReplayMeasurements -transitionAdmittedReplayMeasurements = - Vector.foldl' - combineReplayMeasurements - emptyReplayMeasurements - . transitionAdmittedFacts - -emptyReplayMeasurements :: TransitionReplayMeasurements -emptyReplayMeasurements = - TransitionReplayMeasurements - { transitionKernelReplayCount = 0 - , transitionKernelReplayNodeCount = 0 - , transitionKernelReplayMaximumDepth = 0 - , transitionReconstructionCount = 0 - , transitionReconstructionSearchWork = 0 - , transitionReconstructionDerivedAtomCount = 0 - , transitionReconstructionMaximumCandidateDepth = 0 - , transitionConnectionReplayNodeCount = 0 - , transitionConnectionReplayMaximumDepth = 0 - } - -combineReplayMeasurements - :: TransitionReplayMeasurements - -> AdmittedFact - -> TransitionReplayMeasurements -combineReplayMeasurements measurements = \case - LegacyFactRow{} -> - measurements - TypedFactRow _reference - (TypedAdmittedFact _semantic authorization) -> - case authorization of - KernelProof - (AuthorizedKernelReplay - _target - _imports - _foundation - _rules - nodes - depth - provenance) - _trust -> - combineReconstructionMeasurements - provenance - measurements - { transitionKernelReplayCount = - transitionKernelReplayCount measurements - + 1 - , transitionKernelReplayNodeCount = - transitionKernelReplayNodeCount measurements - + nodes - , transitionKernelReplayMaximumDepth = - max - (transitionKernelReplayMaximumDepth - measurements) - depth - } - DeclaredAssumption{} -> - measurements - TrustedVampire{} -> - measurements - -combineReconstructionMeasurements - :: Maybe SessionTypedReconstructionProvenance - -> TransitionReplayMeasurements - -> TransitionReplayMeasurements -combineReconstructionMeasurements Nothing measurements = - measurements -combineReconstructionMeasurements - (Just - (SessionTypedReconstructionProvenance - _policy - _prepared - _accepted - _trace - searchStats - replayNodes - replayDepth)) - measurements = - measurements - { transitionReconstructionCount = - transitionReconstructionCount measurements - + 1 - , transitionReconstructionSearchWork = - transitionReconstructionSearchWork measurements - + BackendConnection.connectionSearchWork searchStats - , transitionReconstructionDerivedAtomCount = - transitionReconstructionDerivedAtomCount measurements - + BackendConnection.connectionSearchDerivedAtomCount - searchStats - , transitionReconstructionMaximumCandidateDepth = - max - (transitionReconstructionMaximumCandidateDepth - measurements) - (BackendConnection.connectionSearchMaximumCandidateDepth - searchStats) - , transitionConnectionReplayNodeCount = - transitionConnectionReplayNodeCount measurements - + replayNodes - , transitionConnectionReplayMaximumDepth = - max - (transitionConnectionReplayMaximumDepth - measurements) - replayDepth - } - -transitionAdmittedTypedDirectAxiomManifest - :: TransitionAdmittedModule - -> Vector TypedDirectAxiomManifestEntry -transitionAdmittedTypedDirectAxiomManifest = - admittedTypedDirectAxiomManifest - -transitionAdmittedTypedTrustDependencies - :: TransitionAdmittedModule - -> TypedTrustDependencies -transitionAdmittedTypedTrustDependencies = - foldMap - (fromMaybe mempty - . admittedFactTypedTrustDependencies) - . transitionAdmittedFacts - -transitionAdmittedGlobals - :: TransitionAdmittedModule - -> Vector (Symbol, CheckedGlobalRef, Origin) -transitionAdmittedGlobals admitted = - fmap - (\(TypedGlobalBinding - symbol - reference - bindingOrigin - _body) -> - (symbol, reference, bindingOrigin)) - (admittedLocalGlobals admitted) - -validateTypedDirectAxiomManifest - :: Vector TransitionFactEntry - -> Vector TypedDirectAxiomManifestEntry - -> Either TransitionModuleError () -validateTypedDirectAxiomManifest localFacts manifest = - unless - (actual == expected) - (Left TransitionTypedDirectAxiomManifestMismatch) - where - actual = - [ ( reference - , ordinal - , kind - , statement - ) - | TransitionFactEntry - (TypedFactRow - (TransitionTypedFactRef reference) - (TypedAdmittedFact - semantic - (DeclaredAssumption - sessionReference))) - _registration <- - Vector.toList localFacts - , let ordinal = - sessionTypedAssumptionOrdinal - sessionReference - kind = - sessionTypedAssumptionKind - sessionReference - statement = - typedSemanticStatement semantic - , sessionTypedAssumptionFact sessionReference - == reference - , sessionTypedAssumptionStatement sessionReference - == statement - ] - expected = - [ ( typedDirectAssumptionFact entry - , LocalAssumptionOrdinal ordinal - , typedDirectAssumptionKind entry - , typedDirectAssumptionStatement entry - ) - | (ordinal, entry) <- - zip [0 ..] (Vector.toList manifest) - ] - -insertVisibleGlobalBinding - :: ( Map Symbol TypedGlobalBinding - , Map OpaqueDeclarationRef TypedGlobalBinding - ) - -> TypedGlobalBinding - -> Either - TransitionModuleError - ( Map Symbol TypedGlobalBinding - , Map OpaqueDeclarationRef TypedGlobalBinding - ) -insertVisibleGlobalBinding - (globals, declarations) - binding@(TypedGlobalBinding - symbol - reference - _bindingOrigin - _body) = do - globals' <- - case Map.lookup symbol globals of - Nothing -> - Right (Map.insert symbol binding globals) - Just previous@(TypedGlobalBinding - _previousSymbol - _previousReference - _previousOrigin - _previousBody) - | previous == binding -> - Right globals - | otherwise -> - Left - (globalSymbolConflict - previous - binding) - declarations' <- - case Map.lookup declaration declarations of - Nothing -> - Right - (Map.insert - declaration - binding - declarations) - Just previous - | previous == binding -> - Right declarations - | otherwise -> - Left - (globalReferenceConflict - previous - binding) - pure (globals', declarations') - where - declaration = - checkedGlobalReference reference - -globalSymbolConflict - :: TypedGlobalBinding - -> TypedGlobalBinding - -> TransitionModuleError -globalSymbolConflict - (TypedGlobalBinding - previousSymbol - previousReference - previousOrigin - _previousBody) - (TypedGlobalBinding - _incomingSymbol - incomingReference - incomingOrigin - _incomingBody) = - TransitionGlobalConflict - previousSymbol - previousReference - previousOrigin - incomingReference - incomingOrigin - -globalReferenceConflict - :: TypedGlobalBinding - -> TypedGlobalBinding - -> TransitionModuleError -globalReferenceConflict - (TypedGlobalBinding - previousSymbol - previousReference - previousOrigin - _previousBody) - (TypedGlobalBinding - incomingSymbol - incomingReference - incomingOrigin - _incomingBody) = - TransitionGlobalReferenceConflict - (checkedGlobalReference incomingReference) - previousSymbol - (checkedGlobalType previousReference) - previousOrigin - incomingSymbol - (checkedGlobalType incomingReference) - incomingOrigin - - -mergeTypedEnvironments - :: [TransitionAdmittedModule] - -> Either - TransitionModuleError - ( Vector TypedModuleEnvironmentDelta - , Map Symbol TypedGlobalBinding - , Map OpaqueDeclarationRef TypedGlobalBinding - ) -mergeTypedEnvironments directImports = do - (_deltasByModule, reversedDeltas) <- - foldM - importModule - (Map.empty, []) - directImports - (globals, globalDeclarations) <- - foldM - applyDelta - (Map.empty, Map.empty) - (reverse reversedDeltas) - pure - ( Vector.fromList (reverse reversedDeltas) - , globals - , globalDeclarations - ) - where - importModule imported admitted = - foldM - importDelta - imported - (moduleEnvironmentDeltas admitted) - - moduleEnvironmentDeltas - admitted = - toList (admittedEnvironmentDeltas admitted) - - importDelta - current@(byModule, reversedDeltas) - delta@(TypedModuleEnvironmentDelta name _bindings) = - case Map.lookup name byModule of - Nothing -> - Right - ( Map.insert name delta byModule - , delta : reversedDeltas - ) - Just previous - | previous == delta -> - Right current - | otherwise -> - Left - (TransitionImportedModuleConflict - name) - - applyDelta environment - (TypedModuleEnvironmentDelta _name bindings) = - foldM insertVisibleGlobalBinding environment bindings - -mergeTransitionFacts - :: [TransitionAdmittedModule] - -> Either - TransitionModuleError - TransitionFactInventory -mergeTransitionFacts = - foldM importModule emptyTransitionFactInventory - where - importModule inventory admitted = - foldM - (flip insertTransitionFactEntry) - inventory - (Vector.toList - (admittedVisibleFacts admitted)) - -insertFactAliases - :: TransitionFactRef - -> Origin - -> NonEmpty Marker - -> Map Marker (TransitionFactRef, Origin) - -> Either - TransitionModuleError - (Map Marker (TransitionFactRef, Origin)) -insertFactAliases reference factOrigin aliases initial = - foldM insertAlias initial aliases - where - insertAlias current alias = - case Map.lookup alias current of - Nothing -> - Right - (Map.insert - alias - (reference, factOrigin) - current) - Just (previousReference, previousOrigin) - | previousReference == reference -> - Right current - | otherwise -> - Left - (TransitionFactAliasConflict - alias - previousReference - previousOrigin - reference - factOrigin) - -originFromLegacyStagedFact - :: Facts.StagedFact - -> Origin -originFromLegacyStagedFact staged = - Origin - (Facts.factOriginLocation factOrigin) - Nothing - (Just (Facts.factOriginBlock factOrigin)) - where - factOrigin = - Facts.stagedFactOrigin staged - - -data TransitionModuleError - = TransitionLegacyModuleError - !LegacyModuleStageError - | TransitionLegacyStageAddressMismatch - | TransitionLegacyStageIsNotAnExtension - | TransitionLegacyFactOrderMismatch - | TransitionDeclarationNotOpen - | TransitionImportedModuleConflict - !ModuleName - | TransitionGlobalConflict - !Symbol - !CheckedGlobalRef - !Origin - !CheckedGlobalRef - !Origin - | TransitionGlobalReferenceConflict - !OpaqueDeclarationRef - !Symbol - !CoreType - !Origin - !Symbol - !CoreType - !Origin - | TransitionGlobalReferenceNotVisible - !CheckedGlobalRef - | TransitionGlobalReferenceTypeMismatch - !CheckedGlobalRef - !CoreType - | TransitionCoreCheckError - !CoreCheckError - | TransitionTransparentGlobalTypeMismatch - !Symbol - !CoreType - !CoreType - | TransitionTypedFactIsNotProposition - !CoreType - | TransitionTypedFactSupportError - !(Backend.SupportedPropositionError Void) - | TransitionTypedFactClassificationError - !(Backend.BackendClassificationError - CheckedGlobalRef) - | TransitionTypedVampireTargetMismatch - | TransitionTypedVampireRequestMismatch - | TransitionTypedVampireHasOpenLocalPremises - | TransitionTypedVampireGlobalTypeMismatch - !CheckedGlobalRef - !CoreType - | TransitionTypedVampireFactNotVisible - !TransitionFactRef - | TransitionTypedVampireFactMismatch - !TransitionFactRef - | TransitionTypedVampireFoundationMismatch - !FoundationAxiomTag - | TransitionTypedReconstructionMismatch - !BackendReconstruction.ReconstructionMismatch - | TransitionKernelTargetMismatch - | TransitionKernelReplayError - !KernelReplayError - | TransitionDerivationImportError - !DerivationImportError - | TransitionKernelImportIndexOutOfBounds - !ImportIx - | TransitionKernelImportNotVisible - !TransitionFactRef - | TransitionKernelImportDoesNotMatch - !TransitionFactRef - | TransitionDependencyNotMigrated - !TransitionFactRef - | TransitionTypedDirectAxiomManifestMismatch - | TransitionFactReferenceConflict - !TransitionFactRef - | TransitionFactAliasConflict - !Marker - !TransitionFactRef - !Origin - !TransitionFactRef - !Origin - deriving stock (Show, Eq) diff --git a/source/Checking/Typed/Atomic.hs b/source/Checking/Typed/Atomic.hs deleted file mode 100644 index 449928f..0000000 --- a/source/Checking/Typed/Atomic.hs +++ /dev/null @@ -1,72 +0,0 @@ -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE NoImplicitPrelude #-} - --- | Closed applications of checked predicate signatures to ground sets. -module Checking.Typed.Atomic - ( PreparedClosedAtomic - , prepareClosedAtomic - , closedAtomicStatement - , ClosedAtomicError(..) - ) where - -import Base -import Checking.Core -import Checking.Transition -import Checking.Typed.Ground -import Syntax.Internal - -import Data.Bifunctor (first) - - -newtype PreparedClosedAtomic = - PreparedClosedAtomic - (FrozenCheckedCore CheckedGlobalRef) - -closedAtomicStatement - :: PreparedClosedAtomic - -> FrozenCheckedCore CheckedGlobalRef -closedAtomicStatement - (PreparedClosedAtomic statement) = - statement - -data ClosedAtomicError - = ClosedAtomicIllTyped !CoreCheckError - | ClosedAtomicFreezeFailed !FreezeError - deriving stock (Show, Eq) - --- | Return 'Nothing' outside this deliberately small typed family. Once a --- checked predicate global and ground arguments match, formation is total or --- reports its typed-core failure. -prepareClosedAtomic - :: (Symbol -> Maybe CheckedGlobalRef) - -> Formula - -> Maybe - (Either - ClosedAtomicError - PreparedClosedAtomic) -prepareClosedAtomic resolveGlobal = \case - Atomic _location predicate arguments -> do - reference <- - resolveGlobal - (SymbolPredicate predicate) - loweredArguments <- - traverse lowerGroundSetTerm arguments - Just do - checked <- - first ClosedAtomicIllTyped - (checkClosedProposition - (Just . checkedGlobalType) - (foldl' - coreApply - (coreGlobal reference) - loweredArguments)) - statement <- - first ClosedAtomicFreezeFailed - (freezeClosed - (checkedPropositionCore - checked)) - pure - (PreparedClosedAtomic - statement) - _ -> - Nothing diff --git a/source/Checking/Typed/Reflexivity.hs b/source/Checking/Typed/Reflexivity.hs deleted file mode 100644 index f548727..0000000 --- a/source/Checking/Typed/Reflexivity.hs +++ /dev/null @@ -1,105 +0,0 @@ -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE NoImplicitPrelude #-} - --- | Dependency-free typed preparation for closed ground reflexivity. -module Checking.Typed.Reflexivity - ( PreparedGroundReflexivity - , prepareGroundReflexivity - , groundReflexivityTarget - , groundReflexivityDerivation - , GroundReflexivityError(..) - ) where - -import Base hiding (Empty) -import Checking.Core -import Checking.Kernel.Derivation -import Checking.Transition -import Checking.Typed.Ground -import Syntax.Internal - -import Data.Bifunctor (first) - - -data PreparedGroundReflexivity = - PreparedGroundReflexivity - !(FrozenCheckedCore CheckedGlobalRef) - !(KernelDerivation CheckedGlobalRef) - -groundReflexivityTarget - :: PreparedGroundReflexivity - -> FrozenCheckedCore CheckedGlobalRef -groundReflexivityTarget - (PreparedGroundReflexivity target _derivation) = - target - -groundReflexivityDerivation - :: PreparedGroundReflexivity - -> KernelDerivation CheckedGlobalRef -groundReflexivityDerivation - (PreparedGroundReflexivity _target derivation) = - derivation - -data GroundReflexivityError - = GroundReflexivityOperandIllTyped !CoreCheckError - | GroundReflexivityOperandFreezeFailed !FreezeError - | GroundReflexivityTargetIllTyped !CoreCheckError - | GroundReflexivityTargetFreezeFailed !FreezeError - deriving stock (Show, Eq) - --- | Return 'Nothing' when the formula is outside this intentionally small --- typed family. A recognized formula either prepares completely or reports its --- checked-core failure. -prepareGroundReflexivity - :: Formula - -> Maybe - (Either - GroundReflexivityError - PreparedGroundReflexivity) -prepareGroundReflexivity = \case - Equals _location left right -> do - guard (equivalent left right) - leftSyntax <- lowerGroundSetTerm left - Just do - leftFrozen <- - checkAndFreezeOperand leftSyntax - target <- - checkAndFreezeTarget - leftSyntax - leftSyntax - pure - (PreparedGroundReflexivity - target - (equalityReflexivityDerivation - leftFrozen)) - _ -> - Nothing - -checkAndFreezeOperand - :: CoreSyntax CheckedGlobalRef Void - -> Either - GroundReflexivityError - (FrozenCheckedCore CheckedGlobalRef) -checkAndFreezeOperand syntax = do - checked <- - first GroundReflexivityOperandIllTyped - (checkClosedCore - (Just . checkedGlobalType) - syntax) - first GroundReflexivityOperandFreezeFailed - (freezeClosed checked) - -checkAndFreezeTarget - :: CoreSyntax CheckedGlobalRef Void - -> CoreSyntax CheckedGlobalRef Void - -> Either - GroundReflexivityError - (FrozenCheckedCore CheckedGlobalRef) -checkAndFreezeTarget left right = do - checked <- - first GroundReflexivityTargetIllTyped - (checkClosedProposition - (Just . checkedGlobalType) - (coreEquality TySet left right)) - first GroundReflexivityTargetFreezeFailed - (freezeClosed - (checkedPropositionCore checked)) |