{-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE NoImplicitPrelude #-} -- | Canonical semantic declaration, prefix, interface, and validation keys. module Felix.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 Felix.Checking.Authority import Felix.Checking.Core import Felix.Checking.Identity import Felix.Cache.Codec import Felix.Math.Codec import Felix.Module import Felix.Parsed.Identity import Felix.Source import Felix.Syntax.Interface import Felix.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))