diff options
Diffstat (limited to 'source/Checking/Semantic.hs')
| -rw-r--r-- | source/Checking/Semantic.hs | 1759 |
1 files changed, 0 insertions, 1759 deletions
diff --git a/source/Checking/Semantic.hs b/source/Checking/Semantic.hs deleted file mode 100644 index 7a05f39..0000000 --- a/source/Checking/Semantic.hs +++ /dev/null @@ -1,1759 +0,0 @@ -{-# LANGUAGE DeriveAnyClass #-} -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE NoImplicitPrelude #-} - --- | Canonical semantic declaration, prefix, interface, and validation keys. -module Checking.Semantic - ( DeclarationSlot - , declarationSlot - , declarationSlotModule - , declarationSlotOrdinal - , FactSlot - , factSlot - , factSlotModule - , factSlotOrdinal - , SemanticName - , semanticName - , semanticNameText - , FactSearchEligibility(..) - , SemanticFactOccurrence - , semanticFactOccurrence - , semanticFactSlot - , semanticFactProposition - , semanticFactAuthority - , semanticFactSearchEligibility - , semanticFactFingerprint - , SemanticFactOccurrenceFingerprint - , semanticFactOccurrenceFingerprint - , semanticFactFingerprintDigest - , SemanticAlias - , semanticAlias - , semanticAliasName - , semanticAliasTarget - , SemanticGlobalKey(..) - , semanticGlobalKeyFromLexicalEntry - , semanticGlobalKeyType - , SemanticGlobalTarget(..) - , semanticGlobalTargetObject - , semanticGlobalTargetRequirements - , SemanticGlobalBinding - , semanticGlobalBinding - , semanticGlobalBindingKey - , semanticGlobalBindingTarget - , SemanticGlobalTargetError(..) - , validateSemanticGlobalBindingTarget - , SemanticEnvironmentDelta - , emptySemanticEnvironmentDelta - , semanticEnvironmentDelta - , semanticEnvironmentWithStructures - , semanticEnvironmentBindings - , semanticEnvironmentStructures - , SemanticStructurePhrase - , semanticStructurePhrase - , semanticStructurePhraseSingular - , semanticStructurePhrasePlural - , semanticStructurePhraseMarker - , SemanticStructureOperation - , semanticStructureOperation - , semanticStructureOperationSymbol - , semanticStructureOperationObject - , SemanticStructureDescriptor - , semanticStructureDescriptor - , semanticStructureDescriptorPhrase - , semanticStructureDescriptorPredicate - , semanticStructureDescriptorParents - , semanticStructureDescriptorOperations - , SemanticEnvironmentError(..) - , DeclarationInterfaceDelta - , declarationInterfaceDelta - , declarationDeltaSlot - , declarationDeltaFacts - , declarationDeltaAliases - , declarationDeltaObjects - , declarationDeltaPropositions - , declarationDeltaEnvironment - , DeclarationInterfaceError(..) - , SemanticInterfaceId - , semanticInterfaceIdDigest - , SemanticInterface - , semanticInterface - , semanticInterfaceOwner - , semanticInterfaceDirectInputs - , semanticInterfaceDeclarations - , semanticInterfaceAssertedId - , SemanticInterfaceError(..) - , validateSemanticInterface - , renderSemanticInterfaceError - , PrefixContextId - , initialPrefixContextId - , PrefixContextError(..) - , nextPrefixContextId - , prefixContextIdDigest - , ProofSyntaxId - , proofSyntaxId - , DeclarationSyntaxId - , declarationSyntaxId - , ProofValidationKey - , proofValidationKey - , proofValidationKeyDigest - , ProofValidationRecord - , proofValidationRecord - , proofValidationRecordKey - , proofValidationRecordCertificate - , DeclarationValidationKey - , declarationValidationKey - , declarationValidationKeyDigest - , DeclarationValidationRecord - , declarationValidationRecord - , declarationValidationRecordKey - , declarationValidationRecordCertificates - , ModuleArtifactKey - , moduleArtifactKey - , moduleArtifactKeyOwner - , moduleArtifactKeyDirectSemanticInputs - , moduleArtifactKeyTheory - , ModuleArtifactKeyError(..) - , ModuleArtifactId - , moduleArtifactId - , moduleArtifactIdDigest - , ModuleArtifactResult - , moduleArtifactResult - , moduleArtifactResultId - , moduleArtifactResultSyntax - , moduleArtifactResultSemantic - , putModuleArtifactKeyCache - , getModuleArtifactKeyCache - , putModuleArtifactIdCache - , getModuleArtifactIdCache - , putModuleArtifactResultCache - , getModuleArtifactResultCache - , putSemanticFactOccurrenceFingerprintCache - , getSemanticFactOccurrenceFingerprintCache - , putSemanticFactOccurrenceCache - , getSemanticFactOccurrenceCache - , putSemanticEnvironmentDeltaCache - , getSemanticEnvironmentDeltaCache - , putSemanticGlobalKeyCache - , getSemanticGlobalKeyCache - , putDeclarationInterfaceDeltaCache - , getDeclarationInterfaceDeltaCache - , putSemanticInterfaceCache - , getSemanticInterfaceCache - , putSemanticInterfaceIdCache - , getSemanticInterfaceIdCache - , putPrefixContextIdCache - , getPrefixContextIdCache - , putProofValidationRecordCache - , getProofValidationRecordCache - , putDeclarationValidationRecordCache - , getDeclarationValidationRecordCache - ) where - -import Base -import Checking.Authority -import Checking.Core -import Checking.Identity -import Felix.Cache.Codec -import Felix.Math.Codec -import Felix.Module -import Felix.Parsed.Identity -import Felix.Source -import Syntax.Interface -import Syntax.Abstract - -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 - - -data DeclarationSlot = DeclarationSlot - !ModuleName - !LocalDeclarationOrdinal - deriving stock (Show, Eq, Ord) - -declarationSlot - :: ModuleName - -> LocalDeclarationOrdinal - -> DeclarationSlot -declarationSlot = - DeclarationSlot - -declarationSlotModule :: DeclarationSlot -> ModuleName -declarationSlotModule (DeclarationSlot owner _) = - owner - -declarationSlotOrdinal - :: DeclarationSlot - -> LocalDeclarationOrdinal -declarationSlotOrdinal (DeclarationSlot _ ordinal) = - ordinal - -data FactSlot = FactSlot - !ModuleName - !LocalFactOrdinal - deriving stock (Show, Eq, Ord) - -factSlot :: ModuleName -> LocalFactOrdinal -> FactSlot -factSlot = - FactSlot - -factSlotModule :: FactSlot -> ModuleName -factSlotModule (FactSlot owner _) = - owner - -factSlotOrdinal :: FactSlot -> LocalFactOrdinal -factSlotOrdinal (FactSlot _ ordinal) = - ordinal - -newtype SemanticName = - SemanticName Text - deriving stock (Show, Eq, Ord, Generic) - deriving newtype (Hashable, NFData) - -semanticName :: Text -> SemanticName -semanticName = - SemanticName - -semanticNameText :: SemanticName -> Text -semanticNameText (SemanticName name) = - name - -data FactSearchEligibility - = SearchEligible - | SearchIneligible - deriving stock (Show, Eq, Ord, Generic) - deriving anyclass (NFData) - -newtype SemanticFactOccurrenceFingerprint = - SemanticFactOccurrenceFingerprint CacheDigest - deriving stock (Show, Eq, Ord, Generic) - deriving newtype (Hashable, NFData) - -semanticFactOccurrenceFingerprint - :: FactSlot - -> FactAuthority - -> SemanticFactOccurrenceFingerprint -semanticFactOccurrenceFingerprint slot authority = - SemanticFactOccurrenceFingerprint - (hashCacheFields - "felix-semantic-fact-occurrence-v1" - [ encodeCache (putFactSlotCache slot) - , encodeCache (putFactAuthorityCache authority) - ]) - -semanticFactFingerprintDigest - :: SemanticFactOccurrenceFingerprint - -> CacheDigest -semanticFactFingerprintDigest - (SemanticFactOccurrenceFingerprint digest) = - digest - -data SemanticFactOccurrence = SemanticFactOccurrence - !FactSlot - !FactAuthority - !FactSearchEligibility - deriving stock (Show, Eq, Ord, Generic) - -semanticFactOccurrence - :: FactSlot - -> FactAuthority - -> FactSearchEligibility - -> SemanticFactOccurrence -semanticFactOccurrence = - SemanticFactOccurrence - -semanticFactSlot :: SemanticFactOccurrence -> FactSlot -semanticFactSlot - (SemanticFactOccurrence slot _ _) = - slot - -semanticFactProposition - :: SemanticFactOccurrence - -> PropositionId -semanticFactProposition - (SemanticFactOccurrence _ authority _) = - theoremRefProposition - (factAuthorityTheorem authority) - -semanticFactAuthority - :: SemanticFactOccurrence - -> FactAuthority -semanticFactAuthority - (SemanticFactOccurrence _ authority _) = - authority - -semanticFactSearchEligibility - :: SemanticFactOccurrence - -> FactSearchEligibility -semanticFactSearchEligibility - (SemanticFactOccurrence _ _ eligibility) = - eligibility - -semanticFactFingerprint - :: SemanticFactOccurrence - -> SemanticFactOccurrenceFingerprint -semanticFactFingerprint - (SemanticFactOccurrence slot authority _) = - semanticFactOccurrenceFingerprint slot authority - -data SemanticAlias = SemanticAlias - !SemanticName - !SemanticFactOccurrenceFingerprint - deriving stock (Show, Eq, Ord, Generic) - deriving anyclass (NFData) - -semanticAlias - :: SemanticName - -> SemanticFactOccurrenceFingerprint - -> SemanticAlias -semanticAlias = - SemanticAlias - -semanticAliasName :: SemanticAlias -> SemanticName -semanticAliasName (SemanticAlias name _) = - name - -semanticAliasTarget - :: SemanticAlias - -> SemanticFactOccurrenceFingerprint -semanticAliasTarget (SemanticAlias _ target) = - target - - --- | Exact source-level name used to resolve a declared monomorphic object. --- Presentation markers and expression fixity are deliberately absent. -data SemanticGlobalKey - = SemanticLeftAdjective !Pattern - | SemanticRightAdjective !Pattern - | SemanticFunctionPhrase !Pattern !Pattern - | SemanticNoun !Pattern !Pattern - | SemanticVerb !Pattern !Pattern - | SemanticRelation !Token !ParameterArity - | SemanticExpressionFunction !Pattern - | SemanticPrefixPredicate !Text !Natural - deriving stock (Show, Eq, Ord, Generic) - deriving anyclass (NFData) - -semanticGlobalKeyType :: SemanticGlobalKey -> Maybe CoreType -semanticGlobalKeyType = \case - SemanticLeftAdjective pat -> - Just (setArguments (1 + patternArity pat) TyProp) - SemanticRightAdjective pat -> - Just (setArguments (1 + patternArity pat) TyProp) - SemanticFunctionPhrase singular plural - | patternArity singular == patternArity plural -> - Just (setArguments (patternArity singular) TySet) - | otherwise -> Nothing - SemanticNoun singular plural - | patternArity singular == patternArity plural -> - Just (setArguments (1 + patternArity singular) TyProp) - | otherwise -> Nothing - SemanticVerb singular plural - | patternArity singular == patternArity plural -> - Just (setArguments (1 + patternArity singular) TyProp) - | otherwise -> Nothing - SemanticRelation _token arity -> - Just - (setArguments - (2 + parameterArityValue arity) - TyProp) - SemanticExpressionFunction pat -> - Just (setArguments (patternArity pat) TySet) - SemanticPrefixPredicate _command arity -> - Just (setArguments arity TyProp) - where - patternArity :: Pattern -> Natural - patternArity = \case - End -> 0 - HoleCons rest -> 1 + patternArity rest - TokenCons _token rest -> patternArity rest - - setArguments :: Natural -> CoreType -> CoreType - setArguments argumentCount result = - foldr - (const (TyArrow TySet)) - result - [1 .. argumentCount] - -semanticGlobalKeyFromLexicalEntry - :: CanonicalLexicalEntry - -> Maybe SemanticGlobalKey -semanticGlobalKeyFromLexicalEntry = \case - CanonicalLeftAdjective pat _marker -> - Just (SemanticLeftAdjective pat) - CanonicalRightAdjective pat _marker -> - Just (SemanticRightAdjective pat) - CanonicalFunctionPhrase singular plural _marker -> - Just (SemanticFunctionPhrase singular plural) - CanonicalNoun singular plural _marker -> - Just (SemanticNoun singular plural) - CanonicalVerb singular plural _marker -> - Just (SemanticVerb singular plural) - CanonicalRelation token arity _marker -> - Just (SemanticRelation token arity) - CanonicalExpressionFunction pat _marker _fixity -> - Just (SemanticExpressionFunction pat) - CanonicalPrefixPredicate command arity _marker -> - Just (SemanticPrefixPredicate command arity) - CanonicalStructureNoun{} -> - Nothing - CanonicalStructureOperation{} -> - Nothing - -data SemanticGlobalTarget - = GlobalReference !ObjectId - | TransparentExpansion !ObjectId - | ContextualTransparentExpansion - !ObjectId - !(Map.Map StructSymbol ObjectId) - deriving stock (Show, Eq, Ord, Generic) - deriving anyclass (NFData) - -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 - !SemanticGlobalTarget - deriving stock (Show, Eq, Ord, Generic) - deriving anyclass (NFData) - -semanticGlobalBinding - :: SemanticGlobalKey - -> SemanticGlobalTarget - -> SemanticGlobalBinding -semanticGlobalBinding = - SemanticGlobalBinding - -semanticGlobalBindingKey - :: SemanticGlobalBinding - -> SemanticGlobalKey -semanticGlobalBindingKey (SemanticGlobalBinding key _target) = - key - -semanticGlobalBindingTarget - :: SemanticGlobalBinding - -> SemanticGlobalTarget -semanticGlobalBindingTarget (SemanticGlobalBinding _key target) = - target - -data SemanticGlobalTargetError - = SemanticGlobalKeyHasInconsistentArity !SemanticGlobalKey - | SemanticGlobalTargetMissing !ObjectId - | 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 - :: Set.Set (StructSymbol, ObjectId) - -> CheckedObjectClosure - -> SemanticGlobalBinding - -> Either SemanticGlobalTargetError () -validateSemanticGlobalBindingTarget operationBindings closure binding = do - expected <- - maybe - (Left (SemanticGlobalKeyHasInconsistentArity key)) - Right - (semanticGlobalKeyType key) - content <- - maybe - (Left (SemanticGlobalTargetMissing identity)) - Right - (lookupCheckedObjectContent identity closure) - when - (objectIdFamily identity == IntrinsicObject) - (Left (SemanticGlobalTargetIsIntrinsic identity)) - let targetExpected = - case target of - ContextualTransparentExpansion{} -> - TyArrow TySet expected - _ -> expected - actual = objectContentType content - unless - (actual == targetExpected) - (Left - (SemanticGlobalTargetTypeMismatch - identity targetExpected actual)) - case target of - GlobalReference{} -> pure () - TransparentExpansion{} -> - 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 -emptySemanticEnvironmentDelta = - EmptySemanticEnvironmentDelta - -semanticEnvironmentDelta - :: [SemanticGlobalBinding] - -> Either SemanticEnvironmentError SemanticEnvironmentDelta -semanticEnvironmentDelta bindings = - semanticEnvironmentWithStructures bindings [] - -semanticEnvironmentWithStructures - :: [SemanticGlobalBinding] - -> [SemanticStructureDescriptor] - -> Either SemanticEnvironmentError SemanticEnvironmentDelta -semanticEnvironmentWithStructures [] [] = - Right EmptySemanticEnvironmentDelta -semanticEnvironmentWithStructures bindings structures = do - case firstDuplicate (semanticGlobalBindingKey <$> bindings) of - Just duplicate -> - Left (DuplicateSemanticGlobalKey duplicate) - Nothing -> - pure () - unless - (bindings == List.sortOn semanticGlobalBindingKey bindings) - (Left NonCanonicalSemanticGlobalBindingOrder) - 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 - -> [SemanticGlobalBinding] -semanticEnvironmentBindings = \case - EmptySemanticEnvironmentDelta -> [] - SemanticGlobalBindings bindings -> bindings - SemanticGlobalBindingsAndStructures bindings _ -> bindings - -semanticEnvironmentStructures - :: SemanticEnvironmentDelta - -> [SemanticStructureDescriptor] -semanticEnvironmentStructures = \case - EmptySemanticEnvironmentDelta -> [] - SemanticGlobalBindings{} -> [] - SemanticGlobalBindingsAndStructures _ structures -> structures - - -data DeclarationInterfaceDelta = DeclarationInterfaceDelta - !DeclarationSlot - ![SemanticFactOccurrence] - ![SemanticAlias] - ![ObjectId] - ![PropositionId] - !SemanticEnvironmentDelta - deriving stock (Show, Eq, Ord, Generic) - -data DeclarationInterfaceError - = DeclarationFactOwnerMismatch !FactSlot - | DuplicateDeclarationFactSlot !FactSlot - | DuplicateDeclarationFactFingerprint - !SemanticFactOccurrenceFingerprint - | DuplicateDeclarationAlias !SemanticName - | DuplicateDeclarationObject !ObjectId - | DuplicateDeclarationProposition !PropositionId - | DeclarationFactPropositionMissing !PropositionId - deriving stock (Show, Eq) - -declarationInterfaceDelta - :: DeclarationSlot - -> [SemanticFactOccurrence] - -> [SemanticAlias] - -> [ObjectId] - -> [PropositionId] - -> SemanticEnvironmentDelta - -> Either DeclarationInterfaceError DeclarationInterfaceDelta -declarationInterfaceDelta - slot facts aliases objects propositions environment = do - traverse_ validateFact facts - rejectDuplicate - DuplicateDeclarationFactSlot - (semanticFactSlot <$> facts) - rejectDuplicate - DuplicateDeclarationFactFingerprint - (semanticFactFingerprint <$> facts) - rejectDuplicate - DuplicateDeclarationAlias - (semanticAliasName <$> aliases) - rejectDuplicate DuplicateDeclarationObject objects - rejectDuplicate DuplicateDeclarationProposition propositions - pure - (DeclarationInterfaceDelta - slot facts aliases objects propositions environment) - where - owner = declarationSlotModule slot - propositionSet = Set.fromList propositions - - validateFact occurrence = do - unless - (factSlotModule (semanticFactSlot occurrence) == owner) - (Left - (DeclarationFactOwnerMismatch - (semanticFactSlot occurrence))) - let proposition = - semanticFactProposition occurrence - unless - (proposition `Set.member` propositionSet) - (Left (DeclarationFactPropositionMissing proposition)) - -declarationDeltaSlot - :: DeclarationInterfaceDelta - -> DeclarationSlot -declarationDeltaSlot - (DeclarationInterfaceDelta slot _ _ _ _ _) = - slot - -declarationDeltaFacts - :: DeclarationInterfaceDelta - -> [SemanticFactOccurrence] -declarationDeltaFacts - (DeclarationInterfaceDelta _ facts _ _ _ _) = - facts - -declarationDeltaAliases - :: DeclarationInterfaceDelta - -> [SemanticAlias] -declarationDeltaAliases - (DeclarationInterfaceDelta _ _ aliases _ _ _) = - aliases - -declarationDeltaObjects - :: DeclarationInterfaceDelta - -> [ObjectId] -declarationDeltaObjects - (DeclarationInterfaceDelta _ _ _ objects _ _) = - objects - -declarationDeltaPropositions - :: DeclarationInterfaceDelta - -> [PropositionId] -declarationDeltaPropositions - (DeclarationInterfaceDelta _ _ _ _ propositions _) = - propositions - -declarationDeltaEnvironment - :: DeclarationInterfaceDelta - -> SemanticEnvironmentDelta -declarationDeltaEnvironment - (DeclarationInterfaceDelta _ _ _ _ _ environment) = - environment - - -newtype SemanticInterfaceId = - SemanticInterfaceId CacheDigest - deriving stock (Show, Eq, Ord, Generic) - deriving newtype (Hashable, NFData) - -semanticInterfaceIdDigest - :: SemanticInterfaceId - -> CacheDigest -semanticInterfaceIdDigest (SemanticInterfaceId digest) = - digest - -data SemanticInterface = SemanticInterface - !ModuleName - ![SemanticInterfaceId] - ![DeclarationInterfaceDelta] - !SemanticInterfaceId - deriving stock (Show, Eq, Ord) - -data SemanticInterfaceError - = DuplicateDirectSemanticInterface !SemanticInterfaceId - | SemanticDeclarationOwnerMismatch !DeclarationSlot - | NonIncreasingDeclarationSlots - | NonIncreasingFactSlots - | SemanticInterfaceIdMismatch - !SemanticInterfaceId - !SemanticInterfaceId - deriving stock (Show, Eq) - -renderSemanticInterfaceError :: SemanticInterfaceError -> Text -renderSemanticInterfaceError = \case - DuplicateDirectSemanticInterface interface -> - "direct semantic interface occurs more than once: " - <> Text.pack (show interface) - SemanticDeclarationOwnerMismatch slot -> - "declaration belongs to a different module: " - <> Text.pack (show slot) - NonIncreasingDeclarationSlots -> - "declaration slots are not in increasing order" - NonIncreasingFactSlots -> - "fact slots are not in increasing order" - SemanticInterfaceIdMismatch expected actual -> - "semantic interface identity mismatch: expected " - <> Text.pack (show expected) - <> ", found " <> Text.pack (show actual) - -semanticInterface - :: ModuleName - -> [SemanticInterfaceId] - -> [DeclarationInterfaceDelta] - -> Either SemanticInterfaceError SemanticInterface -semanticInterface owner direct declarations = do - validateSemanticInterfaceStructure owner direct declarations - let identity = - computeSemanticInterfaceId owner direct declarations - pure (SemanticInterface owner direct declarations identity) - -validateSemanticInterface - :: ModuleName - -> [SemanticInterfaceId] - -> [DeclarationInterfaceDelta] - -> SemanticInterfaceId - -> Either SemanticInterfaceError SemanticInterface -validateSemanticInterface owner direct declarations asserted = do - validateSemanticInterfaceStructure owner direct declarations - let computed = - computeSemanticInterfaceId - owner direct declarations - unless - (asserted == computed) - (Left - (SemanticInterfaceIdMismatch asserted computed)) - pure - (SemanticInterface - owner direct declarations asserted) - -validateSemanticInterfaceStructure - :: ModuleName - -> [SemanticInterfaceId] - -> [DeclarationInterfaceDelta] - -> Either SemanticInterfaceError () -validateSemanticInterfaceStructure owner direct declarations = do - rejectDuplicate - DuplicateDirectSemanticInterface - direct - traverse_ - (\delta -> - unless - (declarationSlotModule - (declarationDeltaSlot delta) - == owner) - (Left - (SemanticDeclarationOwnerMismatch - (declarationDeltaSlot delta)))) - declarations - unless - (strictlyIncreasing - ( localDeclarationOrdinalValue - . declarationSlotOrdinal - . declarationDeltaSlot - <$> declarations)) - (Left NonIncreasingDeclarationSlots) - unless - (strictlyIncreasing - ( localFactOrdinalValue - . factSlotOrdinal - . semanticFactSlot - <$> concatMap - declarationDeltaFacts - declarations)) - (Left NonIncreasingFactSlots) - -semanticInterfaceOwner :: SemanticInterface -> ModuleName -semanticInterfaceOwner - (SemanticInterface owner _ _ _) = - owner - -semanticInterfaceDirectInputs - :: SemanticInterface - -> [SemanticInterfaceId] -semanticInterfaceDirectInputs - (SemanticInterface _ direct _ _) = - direct - -semanticInterfaceDeclarations - :: SemanticInterface - -> [DeclarationInterfaceDelta] -semanticInterfaceDeclarations - (SemanticInterface _ _ declarations _) = - declarations - -semanticInterfaceAssertedId - :: SemanticInterface - -> SemanticInterfaceId -semanticInterfaceAssertedId - (SemanticInterface _ _ _ asserted) = - asserted - -computeSemanticInterfaceId - :: ModuleName - -> [SemanticInterfaceId] - -> [DeclarationInterfaceDelta] - -> SemanticInterfaceId -computeSemanticInterfaceId owner direct declarations = - SemanticInterfaceId - (hashCacheFields - "felix-semantic-interface-v1" - [ encodeCache (putModuleNameCache owner) - , encodeCache - (putCacheList - putSemanticInterfaceIdCache - direct) - , encodeCache - (putCacheList - putDeclarationInterfaceDeltaCache - declarations) - ]) - - -newtype PrefixContextId = - PrefixContextId CacheDigest - deriving stock (Show, Eq, Ord, Generic) - deriving newtype (Hashable, NFData) - -data PrefixContextError - = DuplicateInitialPrefixSemanticInput !SemanticInterfaceId - deriving stock (Show, Eq) - -initialPrefixContextId - :: TheoryId - -> ModuleName - -> [SemanticInterfaceId] - -> Either PrefixContextError PrefixContextId -initialPrefixContextId theory owner direct = do - rejectDuplicate - DuplicateInitialPrefixSemanticInput - direct - pure - (PrefixContextId - (hashCacheFields - "felix-prefix-initial-v1" - [ encodeCache (putTheoryIdCache theory) - , encodeCache (putModuleNameCache owner) - , encodeCache - (putCacheList - putSemanticInterfaceIdCache - direct) - ])) - -nextPrefixContextId - :: PrefixContextId - -> DeclarationInterfaceDelta - -> PrefixContextId -nextPrefixContextId previous delta = - PrefixContextId - (hashCacheFields - "felix-prefix-step-v1" - [ encodeCache (putPrefixContextIdCache previous) - , encodeCache - (putDeclarationInterfaceDeltaCache delta) - ]) - -prefixContextIdDigest :: PrefixContextId -> CacheDigest -prefixContextIdDigest (PrefixContextId digest) = - digest - - -newtype ProofSyntaxId = - ProofSyntaxId CacheDigest - deriving stock (Show, Eq, Ord, Generic) - deriving newtype (Hashable, NFData) - -proofSyntaxId :: ByteString -> ProofSyntaxId -proofSyntaxId bytes = - ProofSyntaxId - (hashCacheFields "felix-proof-syntax-v1" [bytes]) - -newtype DeclarationSyntaxId = - DeclarationSyntaxId CacheDigest - deriving stock (Show, Eq, Ord, Generic) - deriving newtype (Hashable, NFData) - -declarationSyntaxId :: ByteString -> DeclarationSyntaxId -declarationSyntaxId bytes = - DeclarationSyntaxId - (hashCacheFields "felix-declaration-syntax-v1" [bytes]) - -newtype ProofValidationKey = - ProofValidationKey CacheDigest - deriving stock (Show, Eq, Ord, Generic) - deriving newtype (Hashable, NFData) - -proofValidationKey - :: TheoremId - -> ProofSyntaxId - -> PrefixContextId - -> ProofValidationKey -proofValidationKey theorem (ProofSyntaxId syntax) prefix = - ProofValidationKey - (hashCacheFields - "felix-proof-validation" - [ mathematicalDigestBytes - (theoremIdDigest theorem) - , cacheDigestBytes syntax - , encodeCache (putPrefixContextIdCache prefix) - ]) - -proofValidationKeyDigest - :: ProofValidationKey - -> CacheDigest -proofValidationKeyDigest (ProofValidationKey digest) = - digest - -data ProofValidationRecord = ProofValidationRecord - !ProofValidationKey - !ValidationCertificate - deriving stock (Show, Eq, Ord, Generic) - -proofValidationRecord - :: ProofValidationKey - -> ValidationCertificate - -> ProofValidationRecord -proofValidationRecord = - ProofValidationRecord - -proofValidationRecordKey - :: ProofValidationRecord - -> ProofValidationKey -proofValidationRecordKey - (ProofValidationRecord key _) = - key - -proofValidationRecordCertificate - :: ProofValidationRecord - -> ValidationCertificate -proofValidationRecordCertificate - (ProofValidationRecord _ certificate) = - certificate - -newtype DeclarationValidationKey = - DeclarationValidationKey CacheDigest - deriving stock (Show, Eq, Ord, Generic) - deriving newtype (Hashable, NFData) - -declarationValidationKey - :: DeclarationSyntaxId - -> PrefixContextId - -> [ObjectId] - -> [TheoremId] - -> DeclarationValidationKey -declarationValidationKey - (DeclarationSyntaxId syntax) - prefix objects theorems = - DeclarationValidationKey - (hashCacheFields - "felix-declaration-validation" - [ cacheDigestBytes syntax - , encodeCache (putPrefixContextIdCache prefix) - , encodeCache (putCacheList putObjectIdCache objects) - , encodeCache - (putCacheList - (putMathematicalDigestCache . theoremIdDigest) - theorems) - ]) - -declarationValidationKeyDigest - :: DeclarationValidationKey - -> CacheDigest -declarationValidationKeyDigest - (DeclarationValidationKey digest) = - digest - -data DeclarationValidationRecord = DeclarationValidationRecord - !DeclarationValidationKey - ![ValidationCertificate] - deriving stock (Show, Eq, Ord, Generic) - -declarationValidationRecord - :: DeclarationValidationKey - -> [ValidationCertificate] - -> DeclarationValidationRecord -declarationValidationRecord = - DeclarationValidationRecord - -declarationValidationRecordKey - :: DeclarationValidationRecord - -> DeclarationValidationKey -declarationValidationRecordKey - (DeclarationValidationRecord key _) = - key - -declarationValidationRecordCertificates - :: DeclarationValidationRecord - -> [ValidationCertificate] -declarationValidationRecordCertificates - (DeclarationValidationRecord _ certificates) = - certificates - - -data ModuleArtifactKey = ModuleArtifactKey - !ModuleName - !ParsedModuleId - ![SemanticInterfaceId] - !TheoryId - deriving stock (Show, Eq, Ord) - -data ModuleArtifactKeyError - = DuplicateModuleArtifactSemanticInput - !SemanticInterfaceId - deriving stock (Show, Eq) - -moduleArtifactKey - :: ModuleName - -> ParsedModuleId - -> [SemanticInterfaceId] - -> TheoryId - -> Either ModuleArtifactKeyError ModuleArtifactKey -moduleArtifactKey owner parsed direct theory = do - rejectDuplicate - DuplicateModuleArtifactSemanticInput - direct - pure (ModuleArtifactKey owner parsed direct theory) - -moduleArtifactKeyOwner :: ModuleArtifactKey -> ModuleName -moduleArtifactKeyOwner (ModuleArtifactKey owner _parsed _direct _theory) = - owner - -moduleArtifactKeyDirectSemanticInputs - :: ModuleArtifactKey - -> [SemanticInterfaceId] -moduleArtifactKeyDirectSemanticInputs - (ModuleArtifactKey _owner _parsed direct _theory) = - direct - -moduleArtifactKeyTheory :: ModuleArtifactKey -> TheoryId -moduleArtifactKeyTheory - (ModuleArtifactKey _owner _parsed _direct theory) = - theory - -newtype ModuleArtifactId = - ModuleArtifactId CacheDigest - deriving stock (Show, Eq, Ord, Generic) - deriving newtype (Hashable, NFData) - -moduleArtifactId :: ModuleArtifactKey -> ModuleArtifactId -moduleArtifactId key = - ModuleArtifactId - (hashCacheFields - "felix-module-artifact-v1" - [encodeCache (putModuleArtifactKeyCache key)]) - -moduleArtifactIdDigest :: ModuleArtifactId -> CacheDigest -moduleArtifactIdDigest (ModuleArtifactId digest) = - digest - -data ModuleArtifactResult = ModuleArtifactResult - !ModuleArtifactId - !SyntaxInterfaceId - !SemanticInterfaceId - deriving stock (Show, Eq, Ord, Generic) - deriving anyclass (NFData) - -moduleArtifactResult - :: ModuleArtifactKey - -> SyntaxInterfaceId - -> SemanticInterfaceId - -> ModuleArtifactResult -moduleArtifactResult key = - ModuleArtifactResult (moduleArtifactId key) - -moduleArtifactResultId - :: ModuleArtifactResult - -> ModuleArtifactId -moduleArtifactResultId - (ModuleArtifactResult identity _ _) = - identity - -moduleArtifactResultSyntax - :: ModuleArtifactResult - -> SyntaxInterfaceId -moduleArtifactResultSyntax - (ModuleArtifactResult _ syntax _) = - syntax - -moduleArtifactResultSemantic - :: ModuleArtifactResult - -> SemanticInterfaceId -moduleArtifactResultSemantic - (ModuleArtifactResult _ _ semantic) = - semantic - - -putSemanticFactOccurrenceFingerprintCache - :: SemanticFactOccurrenceFingerprint - -> CachePut -putSemanticFactOccurrenceFingerprintCache - (SemanticFactOccurrenceFingerprint digest) = - putCacheDigest digest - -getSemanticFactOccurrenceFingerprintCache - :: CacheGet SemanticFactOccurrenceFingerprint -getSemanticFactOccurrenceFingerprintCache = - SemanticFactOccurrenceFingerprint <$> getCacheDigest - -putSemanticFactOccurrenceCache - :: SemanticFactOccurrence - -> CachePut -putSemanticFactOccurrenceCache - (SemanticFactOccurrence slot authority eligibility) = do - putFactSlotCache slot - putFactAuthorityCache authority - putEligibility eligibility - -getSemanticFactOccurrenceCache - :: CacheGet SemanticFactOccurrence -getSemanticFactOccurrenceCache = - semanticFactOccurrence - <$> getFactSlotCache - <*> getFactAuthorityCache - <*> getEligibility - -putSemanticEnvironmentDeltaCache - :: SemanticEnvironmentDelta - -> CachePut -putSemanticEnvironmentDeltaCache EmptySemanticEnvironmentDelta = - putCacheTag 0x00 -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 -getSemanticEnvironmentDeltaCache = - getCacheTag >>= \case - 0x00 -> - pure EmptySemanticEnvironmentDelta - 0x01 -> do - bindings <- getCacheList getSemanticGlobalBindingCache - either - (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 " - <> show tag) - -putSemanticGlobalKeyCache :: SemanticGlobalKey -> CachePut -putSemanticGlobalKeyCache = \case - SemanticLeftAdjective pat -> do - putCacheTag 0x00 - putPatternCache pat - SemanticRightAdjective pat -> do - putCacheTag 0x01 - putPatternCache pat - SemanticFunctionPhrase singular plural -> do - putCacheTag 0x02 - putPatternCache singular - putPatternCache plural - SemanticNoun singular plural -> do - putCacheTag 0x03 - putPatternCache singular - putPatternCache plural - SemanticVerb singular plural -> do - putCacheTag 0x04 - putPatternCache singular - putPatternCache plural - SemanticRelation token arity -> do - putCacheTag 0x05 - putTokenCache token - putCacheNatural (parameterArityValue arity) - SemanticExpressionFunction pat -> do - putCacheTag 0x06 - putPatternCache pat - SemanticPrefixPredicate command arity -> do - putCacheTag 0x07 - putCacheText command - putCacheNatural arity - -getSemanticGlobalKeyCache :: CacheGet SemanticGlobalKey -getSemanticGlobalKeyCache = - getCacheTag >>= \case - 0x00 -> SemanticLeftAdjective <$> getPatternCache - 0x01 -> SemanticRightAdjective <$> getPatternCache - 0x02 -> - SemanticFunctionPhrase - <$> getPatternCache - <*> getPatternCache - 0x03 -> - SemanticNoun - <$> getPatternCache - <*> getPatternCache - 0x04 -> - SemanticVerb - <$> getPatternCache - <*> getPatternCache - 0x05 -> - SemanticRelation - <$> getTokenCache - <*> (ParameterArity <$> getCacheNatural) - 0x06 -> SemanticExpressionFunction <$> getPatternCache - 0x07 -> - SemanticPrefixPredicate - <$> getCacheText - <*> getCacheNatural - tag -> - fail ("unknown semantic global key tag " <> show tag) - -putSemanticGlobalBindingCache :: SemanticGlobalBinding -> CachePut -putSemanticGlobalBindingCache (SemanticGlobalBinding key target) = do - putSemanticGlobalKeyCache key - case target of - GlobalReference identity -> do - putCacheTag 0x00 - putObjectIdCache identity - 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 = - SemanticGlobalBinding - <$> getSemanticGlobalKeyCache - <*> (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 -putDeclarationInterfaceDeltaCache - (DeclarationInterfaceDelta - slot facts aliases objects propositions environment) = do - putDeclarationSlotCache slot - putCacheList putSemanticFactOccurrenceCache facts - putCacheList putSemanticAliasCache aliases - putCacheList putObjectIdCache objects - putCacheList putPropositionIdCache propositions - putSemanticEnvironmentDeltaCache environment - -getDeclarationInterfaceDeltaCache - :: CacheGet DeclarationInterfaceDelta -getDeclarationInterfaceDeltaCache = do - slot <- getDeclarationSlotCache - facts <- getCacheList getSemanticFactOccurrenceCache - aliases <- getCacheList getSemanticAliasCache - objects <- getCacheList getObjectIdCache - propositions <- getCacheList getPropositionIdCache - environment <- getSemanticEnvironmentDeltaCache - either - (fail . ("invalid declaration interface delta: " <>) . show) - pure - (declarationInterfaceDelta - slot facts aliases objects propositions environment) - -putSemanticInterfaceCache :: SemanticInterface -> CachePut -putSemanticInterfaceCache - (SemanticInterface owner direct declarations asserted) = do - putModuleNameCache owner - putCacheList putSemanticInterfaceIdCache direct - putCacheList putDeclarationInterfaceDeltaCache declarations - putSemanticInterfaceIdCache asserted - -getSemanticInterfaceCache :: CacheGet SemanticInterface -getSemanticInterfaceCache = do - owner <- getModuleNameCache - direct <- getCacheList getSemanticInterfaceIdCache - declarations <- getCacheList getDeclarationInterfaceDeltaCache - asserted <- getSemanticInterfaceIdCache - either - (fail . ("invalid semantic interface: " <>) . show) - pure - (validateSemanticInterface - owner direct declarations asserted) - -putSemanticInterfaceIdCache :: SemanticInterfaceId -> CachePut -putSemanticInterfaceIdCache (SemanticInterfaceId digest) = - putCacheDigest digest - -getSemanticInterfaceIdCache :: CacheGet SemanticInterfaceId -getSemanticInterfaceIdCache = - SemanticInterfaceId <$> getCacheDigest - -putPrefixContextIdCache :: PrefixContextId -> CachePut -putPrefixContextIdCache (PrefixContextId digest) = - putCacheDigest digest - -getPrefixContextIdCache :: CacheGet PrefixContextId -getPrefixContextIdCache = - PrefixContextId <$> getCacheDigest - -putModuleArtifactKeyCache :: ModuleArtifactKey -> CachePut -putModuleArtifactKeyCache = - putModuleArtifactKeyFields - -getModuleArtifactKeyCache :: CacheGet ModuleArtifactKey -getModuleArtifactKeyCache = do - owner <- getModuleNameCache - parsed <- getParsedModuleIdCache - direct <- getCacheList getSemanticInterfaceIdCache - theory <- getTheoryIdCache - either - (fail . ("invalid module artifact key: " <>) . show) - pure - (moduleArtifactKey owner parsed direct theory) - -putModuleArtifactIdCache :: ModuleArtifactId -> CachePut -putModuleArtifactIdCache (ModuleArtifactId digest) = - putCacheDigest digest - -getModuleArtifactIdCache :: CacheGet ModuleArtifactId -getModuleArtifactIdCache = - ModuleArtifactId <$> getCacheDigest - -putModuleArtifactResultCache - :: ModuleArtifactResult - -> CachePut -putModuleArtifactResultCache - (ModuleArtifactResult identity syntax semantic) = do - putModuleArtifactIdCache identity - putSyntaxInterfaceIdCache syntax - putSemanticInterfaceIdCache semantic - -getModuleArtifactResultCache - :: ModuleArtifactId - -> CacheGet ModuleArtifactResult -getModuleArtifactResultCache expected = do - asserted <- getModuleArtifactIdCache - unless - (asserted == expected) - (fail "module artifact result ID mismatch") - ModuleArtifactResult asserted - <$> getSyntaxInterfaceIdCache - <*> getSemanticInterfaceIdCache - -putProofValidationRecordCache - :: ProofValidationRecord - -> CachePut -putProofValidationRecordCache - (ProofValidationRecord key certificate) = do - putProofValidationKeyCache key - putValidationCertificateCache certificate - -getProofValidationRecordCache - :: CacheGet ProofValidationRecord -getProofValidationRecordCache = - ProofValidationRecord - <$> getProofValidationKeyCache - <*> getValidationCertificateCache - -putDeclarationValidationRecordCache - :: DeclarationValidationRecord - -> CachePut -putDeclarationValidationRecordCache - (DeclarationValidationRecord key certificates) = do - putDeclarationValidationKeyCache key - putCacheList putValidationCertificateCache certificates - -getDeclarationValidationRecordCache - :: CacheGet DeclarationValidationRecord -getDeclarationValidationRecordCache = - DeclarationValidationRecord - <$> getDeclarationValidationKeyCache - <*> getCacheList getValidationCertificateCache - - -putDeclarationSlotCache :: DeclarationSlot -> CachePut -putDeclarationSlotCache (DeclarationSlot owner ordinal) = do - putModuleNameCache owner - putCacheNatural (localDeclarationOrdinalValue ordinal) - -getDeclarationSlotCache :: CacheGet DeclarationSlot -getDeclarationSlotCache = - DeclarationSlot - <$> getModuleNameCache - <*> (localDeclarationOrdinal <$> getCacheNatural) - -putFactSlotCache :: FactSlot -> CachePut -putFactSlotCache (FactSlot owner ordinal) = do - putModuleNameCache owner - putCacheNatural (localFactOrdinalValue ordinal) - -getFactSlotCache :: CacheGet FactSlot -getFactSlotCache = - FactSlot - <$> getModuleNameCache - <*> (localFactOrdinal <$> getCacheNatural) - -putModuleNameCache :: ModuleName -> CachePut -putModuleNameCache owner = do - putMathematicalDigestCache - (sourceNamespaceDigest - (moduleNameNamespace owner)) - putCacheText - (Text.pack - (safeRelativePathFilePath - (moduleNameRelativePath owner))) - -getModuleNameCache :: CacheGet ModuleName -getModuleNameCache = do - namespace <- - sourceNamespaceIdFromDigest - <$> getMathematicalDigestCache - rawPath <- Text.unpack <$> getCacheText - relative <- - either - (fail . ("invalid cache module path: " <>) . show) - pure - (safeRelativePath rawPath) - pure (moduleNameFromParts namespace relative) - -putSemanticAliasCache :: SemanticAlias -> CachePut -putSemanticAliasCache (SemanticAlias name target) = do - putSemanticNameCache name - putSemanticFactOccurrenceFingerprintCache target - -getSemanticAliasCache :: CacheGet SemanticAlias -getSemanticAliasCache = - SemanticAlias - <$> getSemanticNameCache - <*> getSemanticFactOccurrenceFingerprintCache - -putSemanticNameCache :: SemanticName -> CachePut -putSemanticNameCache (SemanticName name) = - putCacheText name - -getSemanticNameCache :: CacheGet SemanticName -getSemanticNameCache = - SemanticName <$> getCacheText - -putEligibility :: FactSearchEligibility -> CachePut -putEligibility = \case - SearchEligible -> putCacheTag 0x00 - SearchIneligible -> putCacheTag 0x01 - -getEligibility :: CacheGet FactSearchEligibility -getEligibility = - getCacheTag >>= \case - 0x00 -> pure SearchEligible - 0x01 -> pure SearchIneligible - tag -> - fail ("unknown fact-search eligibility tag " <> show tag) - -putModuleArtifactKeyFields :: ModuleArtifactKey -> CachePut -putModuleArtifactKeyFields - (ModuleArtifactKey owner parsed direct theory) = do - putModuleNameCache owner - putParsedModuleIdCache parsed - putCacheList putSemanticInterfaceIdCache direct - putTheoryIdCache theory - -putProofValidationKeyCache :: ProofValidationKey -> CachePut -putProofValidationKeyCache (ProofValidationKey digest) = - putCacheDigest digest - -getProofValidationKeyCache :: CacheGet ProofValidationKey -getProofValidationKeyCache = - ProofValidationKey <$> getCacheDigest - -putDeclarationValidationKeyCache - :: DeclarationValidationKey - -> CachePut -putDeclarationValidationKeyCache - (DeclarationValidationKey digest) = - putCacheDigest digest - -getDeclarationValidationKeyCache - :: CacheGet DeclarationValidationKey -getDeclarationValidationKeyCache = - DeclarationValidationKey <$> getCacheDigest - -firstDuplicate :: Ord value => [value] -> Maybe value -firstDuplicate = - go Set.empty - where - go _ [] = - Nothing - go seen (value : rest) - | value `Set.member` seen = - Just value - | otherwise = - go (Set.insert value seen) rest - -rejectDuplicate - :: Ord value - => (value -> error) - -> [value] - -> Either error () -rejectDuplicate makeError values = - maybe - (Right ()) - (Left . makeError) - (firstDuplicate values) - -strictlyIncreasing :: Ord value => [value] -> Bool -strictlyIncreasing values = - and - (zipWith (<) values (drop 1 values)) |