diff options
Diffstat (limited to 'source/Felix/Checking/Semantic.hs')
| -rw-r--r-- | source/Felix/Checking/Semantic.hs | 1759 |
1 files changed, 1759 insertions, 0 deletions
diff --git a/source/Felix/Checking/Semantic.hs b/source/Felix/Checking/Semantic.hs new file mode 100644 index 0000000..c9442f3 --- /dev/null +++ b/source/Felix/Checking/Semantic.hs @@ -0,0 +1,1759 @@ +{-# 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)) |