path: root/source/Checking/Semantic.hs

{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE NoImplicitPrelude #-}

-- | Canonical semantic declaration, prefix, interface, and validation keys.
module Checking.Semantic
    ( DeclarationSlot
    , declarationSlot
    , declarationSlotModule
    , declarationSlotOrdinal
    , FactSlot
    , factSlot
    , factSlotModule
    , factSlotOrdinal
    , SemanticName
    , semanticName
    , semanticNameText
    , FactSearchEligibility(..)
    , SemanticFactOccurrence
    , semanticFactOccurrence
    , semanticFactSlot
    , semanticFactProposition
    , semanticFactAuthority
    , semanticFactSearchEligibility
    , semanticFactFingerprint
    , SemanticFactOccurrenceFingerprint
    , semanticFactOccurrenceFingerprint
    , semanticFactFingerprintDigest
    , SemanticAlias
    , semanticAlias
    , semanticAliasName
    , semanticAliasTarget
    , SemanticGlobalKey(..)
    , semanticGlobalKeyFromLexicalEntry
    , semanticGlobalKeyType
    , SemanticGlobalTarget(..)
    , semanticGlobalTargetObject
    , semanticGlobalTargetRequirements
    , SemanticGlobalBinding
    , semanticGlobalBinding
    , semanticGlobalBindingKey
    , semanticGlobalBindingTarget
    , SemanticGlobalTargetError(..)
    , validateSemanticGlobalBindingTarget
    , SemanticEnvironmentDelta
    , emptySemanticEnvironmentDelta
    , semanticEnvironmentDelta
    , semanticEnvironmentWithStructures
    , semanticEnvironmentBindings
    , semanticEnvironmentStructures
    , SemanticStructurePhrase
    , semanticStructurePhrase
    , semanticStructurePhraseSingular
    , semanticStructurePhrasePlural
    , semanticStructurePhraseMarker
    , SemanticStructureOperation
    , semanticStructureOperation
    , semanticStructureOperationSymbol
    , semanticStructureOperationObject
    , SemanticStructureDescriptor
    , semanticStructureDescriptor
    , semanticStructureDescriptorPhrase
    , semanticStructureDescriptorPredicate
    , semanticStructureDescriptorParents
    , semanticStructureDescriptorOperations
    , SemanticEnvironmentError(..)
    , DeclarationInterfaceDelta
    , declarationInterfaceDelta
    , declarationDeltaSlot
    , declarationDeltaFacts
    , declarationDeltaAliases
    , declarationDeltaObjects
    , declarationDeltaPropositions
    , declarationDeltaEnvironment
    , DeclarationInterfaceError(..)
    , SemanticInterfaceId
    , semanticInterfaceIdDigest
    , SemanticInterface
    , semanticInterface
    , semanticInterfaceOwner
    , semanticInterfaceDirectInputs
    , semanticInterfaceDeclarations
    , semanticInterfaceAssertedId
    , SemanticInterfaceError(..)
    , validateSemanticInterface
    , renderSemanticInterfaceError
    , PrefixContextId
    , initialPrefixContextId
    , PrefixContextError(..)
    , nextPrefixContextId
    , prefixContextIdDigest
    , ProofSyntaxId
    , proofSyntaxId
    , DeclarationSyntaxId
    , declarationSyntaxId
    , ProofValidationKey
    , proofValidationKey
    , proofValidationKeyDigest
    , ProofValidationRecord
    , proofValidationRecord
    , proofValidationRecordKey
    , proofValidationRecordCertificate
    , DeclarationValidationKey
    , declarationValidationKey
    , declarationValidationKeyDigest
    , DeclarationValidationRecord
    , declarationValidationRecord
    , declarationValidationRecordKey
    , declarationValidationRecordCertificates
    , ModuleArtifactKey
    , moduleArtifactKey
    , moduleArtifactKeyOwner
    , moduleArtifactKeyDirectSemanticInputs
    , moduleArtifactKeyTheory
    , ModuleArtifactKeyError(..)
    , ModuleArtifactId
    , moduleArtifactId
    , moduleArtifactIdDigest
    , ModuleArtifactResult
    , moduleArtifactResult
    , moduleArtifactResultId
    , moduleArtifactResultSyntax
    , moduleArtifactResultSemantic
    , putModuleArtifactKeyCache
    , getModuleArtifactKeyCache
    , putModuleArtifactIdCache
    , getModuleArtifactIdCache
    , putModuleArtifactResultCache
    , getModuleArtifactResultCache
    , putSemanticFactOccurrenceFingerprintCache
    , getSemanticFactOccurrenceFingerprintCache
    , putSemanticFactOccurrenceCache
    , getSemanticFactOccurrenceCache
    , putSemanticEnvironmentDeltaCache
    , getSemanticEnvironmentDeltaCache
    , putSemanticGlobalKeyCache
    , getSemanticGlobalKeyCache
    , putDeclarationInterfaceDeltaCache
    , getDeclarationInterfaceDeltaCache
    , putSemanticInterfaceCache
    , getSemanticInterfaceCache
    , putSemanticInterfaceIdCache
    , getSemanticInterfaceIdCache
    , putPrefixContextIdCache
    , getPrefixContextIdCache
    , putProofValidationRecordCache
    , getProofValidationRecordCache
    , putDeclarationValidationRecordCache
    , getDeclarationValidationRecordCache
    ) where

import Base
import Checking.Authority
import Checking.Core
import Checking.Identity
import Felix.Cache.Codec
import Felix.Math.Codec
import Felix.Module
import Felix.Parsed.Identity
import Felix.Source
import Syntax.Interface
import Syntax.Abstract

import Control.DeepSeq (NFData)
import Control.Monad (unless, when)
import Data.ByteString (ByteString)
import Data.List qualified as List
import Data.Map.Strict qualified as Map
import Numeric.Natural (Natural)
import Data.Set qualified as Set
import Data.Text qualified as Text


data DeclarationSlot = DeclarationSlot
    !ModuleName
    !LocalDeclarationOrdinal
    deriving stock (Show, Eq, Ord)

declarationSlot
    :: ModuleName
    -> LocalDeclarationOrdinal
    -> DeclarationSlot
declarationSlot =
    DeclarationSlot

declarationSlotModule :: DeclarationSlot -> ModuleName
declarationSlotModule (DeclarationSlot owner _) =
    owner

declarationSlotOrdinal
    :: DeclarationSlot
    -> LocalDeclarationOrdinal
declarationSlotOrdinal (DeclarationSlot _ ordinal) =
    ordinal

data FactSlot = FactSlot
    !ModuleName
    !LocalFactOrdinal
    deriving stock (Show, Eq, Ord)

factSlot :: ModuleName -> LocalFactOrdinal -> FactSlot
factSlot =
    FactSlot

factSlotModule :: FactSlot -> ModuleName
factSlotModule (FactSlot owner _) =
    owner

factSlotOrdinal :: FactSlot -> LocalFactOrdinal
factSlotOrdinal (FactSlot _ ordinal) =
    ordinal

newtype SemanticName =
    SemanticName Text
    deriving stock (Show, Eq, Ord, Generic)
    deriving newtype (Hashable, NFData)

semanticName :: Text -> SemanticName
semanticName =
    SemanticName

semanticNameText :: SemanticName -> Text
semanticNameText (SemanticName name) =
    name

data FactSearchEligibility
    = SearchEligible
    | SearchIneligible
    deriving stock (Show, Eq, Ord, Generic)
    deriving anyclass (NFData)

newtype SemanticFactOccurrenceFingerprint =
    SemanticFactOccurrenceFingerprint CacheDigest
    deriving stock (Show, Eq, Ord, Generic)
    deriving newtype (Hashable, NFData)

semanticFactOccurrenceFingerprint
    :: FactSlot
    -> FactAuthority
    -> SemanticFactOccurrenceFingerprint
semanticFactOccurrenceFingerprint slot authority =
    SemanticFactOccurrenceFingerprint
        (hashCacheFields
            "felix-semantic-fact-occurrence-v1"
            [ encodeCache (putFactSlotCache slot)
            , encodeCache (putFactAuthorityCache authority)
            ])

semanticFactFingerprintDigest
    :: SemanticFactOccurrenceFingerprint
    -> CacheDigest
semanticFactFingerprintDigest
        (SemanticFactOccurrenceFingerprint digest) =
    digest

data SemanticFactOccurrence = SemanticFactOccurrence
    !FactSlot
    !FactAuthority
    !FactSearchEligibility
    deriving stock (Show, Eq, Ord, Generic)

semanticFactOccurrence
    :: FactSlot
    -> FactAuthority
    -> FactSearchEligibility
    -> SemanticFactOccurrence
semanticFactOccurrence =
    SemanticFactOccurrence

semanticFactSlot :: SemanticFactOccurrence -> FactSlot
semanticFactSlot
        (SemanticFactOccurrence slot _ _) =
    slot

semanticFactProposition
    :: SemanticFactOccurrence
    -> PropositionId
semanticFactProposition
        (SemanticFactOccurrence _ authority _) =
    theoremRefProposition
        (factAuthorityTheorem authority)

semanticFactAuthority
    :: SemanticFactOccurrence
    -> FactAuthority
semanticFactAuthority
        (SemanticFactOccurrence _ authority _) =
    authority

semanticFactSearchEligibility
    :: SemanticFactOccurrence
    -> FactSearchEligibility
semanticFactSearchEligibility
        (SemanticFactOccurrence _ _ eligibility) =
    eligibility

semanticFactFingerprint
    :: SemanticFactOccurrence
    -> SemanticFactOccurrenceFingerprint
semanticFactFingerprint
        (SemanticFactOccurrence slot authority _) =
    semanticFactOccurrenceFingerprint slot authority

data SemanticAlias = SemanticAlias
    !SemanticName
    !SemanticFactOccurrenceFingerprint
    deriving stock (Show, Eq, Ord, Generic)
    deriving anyclass (NFData)

semanticAlias
    :: SemanticName
    -> SemanticFactOccurrenceFingerprint
    -> SemanticAlias
semanticAlias =
    SemanticAlias

semanticAliasName :: SemanticAlias -> SemanticName
semanticAliasName (SemanticAlias name _) =
    name

semanticAliasTarget
    :: SemanticAlias
    -> SemanticFactOccurrenceFingerprint
semanticAliasTarget (SemanticAlias _ target) =
    target


-- | Exact source-level name used to resolve a declared monomorphic object.
-- Presentation markers and expression fixity are deliberately absent.
data SemanticGlobalKey
    = SemanticLeftAdjective !Pattern
    | SemanticRightAdjective !Pattern
    | SemanticFunctionPhrase !Pattern !Pattern
    | SemanticNoun !Pattern !Pattern
    | SemanticVerb !Pattern !Pattern
    | SemanticRelation !Token !ParameterArity
    | SemanticExpressionFunction !Pattern
    | SemanticPrefixPredicate !Text !Natural
    deriving stock (Show, Eq, Ord, Generic)
    deriving anyclass (NFData)

semanticGlobalKeyType :: SemanticGlobalKey -> Maybe CoreType
semanticGlobalKeyType = \case
    SemanticLeftAdjective pat ->
        Just (setArguments (1 + patternArity pat) TyProp)
    SemanticRightAdjective pat ->
        Just (setArguments (1 + patternArity pat) TyProp)
    SemanticFunctionPhrase singular plural
        | patternArity singular == patternArity plural ->
            Just (setArguments (patternArity singular) TySet)
        | otherwise -> Nothing
    SemanticNoun singular plural
        | patternArity singular == patternArity plural ->
            Just (setArguments (1 + patternArity singular) TyProp)
        | otherwise -> Nothing
    SemanticVerb singular plural
        | patternArity singular == patternArity plural ->
            Just (setArguments (1 + patternArity singular) TyProp)
        | otherwise -> Nothing
    SemanticRelation _token arity ->
        Just
            (setArguments
                (2 + parameterArityValue arity)
                TyProp)
    SemanticExpressionFunction pat ->
        Just (setArguments (patternArity pat) TySet)
    SemanticPrefixPredicate _command arity ->
        Just (setArguments arity TyProp)
  where
    patternArity :: Pattern -> Natural
    patternArity = \case
        End -> 0
        HoleCons rest -> 1 + patternArity rest
        TokenCons _token rest -> patternArity rest

    setArguments :: Natural -> CoreType -> CoreType
    setArguments argumentCount result =
        foldr
            (const (TyArrow TySet))
            result
            [1 .. argumentCount]

semanticGlobalKeyFromLexicalEntry
    :: CanonicalLexicalEntry
    -> Maybe SemanticGlobalKey
semanticGlobalKeyFromLexicalEntry = \case
    CanonicalLeftAdjective pat _marker ->
        Just (SemanticLeftAdjective pat)
    CanonicalRightAdjective pat _marker ->
        Just (SemanticRightAdjective pat)
    CanonicalFunctionPhrase singular plural _marker ->
        Just (SemanticFunctionPhrase singular plural)
    CanonicalNoun singular plural _marker ->
        Just (SemanticNoun singular plural)
    CanonicalVerb singular plural _marker ->
        Just (SemanticVerb singular plural)
    CanonicalRelation token arity _marker ->
        Just (SemanticRelation token arity)
    CanonicalExpressionFunction pat _marker _fixity ->
        Just (SemanticExpressionFunction pat)
    CanonicalPrefixPredicate command arity _marker ->
        Just (SemanticPrefixPredicate command arity)
    CanonicalStructureNoun{} ->
        Nothing
    CanonicalStructureOperation{} ->
        Nothing

data SemanticGlobalTarget
    = GlobalReference !ObjectId
    | TransparentExpansion !ObjectId
    | ContextualTransparentExpansion
        !ObjectId
        !(Map.Map StructSymbol ObjectId)
    deriving stock (Show, Eq, Ord, Generic)
    deriving anyclass (NFData)

semanticGlobalTargetObject :: SemanticGlobalTarget -> ObjectId
semanticGlobalTargetObject = \case
    GlobalReference identity -> identity
    TransparentExpansion identity -> identity
    ContextualTransparentExpansion identity _requirements -> identity

semanticGlobalTargetRequirements
    :: SemanticGlobalTarget
    -> Map.Map StructSymbol ObjectId
semanticGlobalTargetRequirements = \case
    GlobalReference{} -> Map.empty
    TransparentExpansion{} -> Map.empty
    ContextualTransparentExpansion _identity requirements -> requirements

data SemanticGlobalBinding = SemanticGlobalBinding
    !SemanticGlobalKey
    !SemanticGlobalTarget
    deriving stock (Show, Eq, Ord, Generic)
    deriving anyclass (NFData)

semanticGlobalBinding
    :: SemanticGlobalKey
    -> SemanticGlobalTarget
    -> SemanticGlobalBinding
semanticGlobalBinding =
    SemanticGlobalBinding

semanticGlobalBindingKey
    :: SemanticGlobalBinding
    -> SemanticGlobalKey
semanticGlobalBindingKey (SemanticGlobalBinding key _target) =
    key

semanticGlobalBindingTarget
    :: SemanticGlobalBinding
    -> SemanticGlobalTarget
semanticGlobalBindingTarget (SemanticGlobalBinding _key target) =
    target

data SemanticGlobalTargetError
    = SemanticGlobalKeyHasInconsistentArity !SemanticGlobalKey
    | SemanticGlobalTargetMissing !ObjectId
    | SemanticGlobalTargetIsIntrinsic !ObjectId
    | SemanticGlobalTargetTypeMismatch !ObjectId !CoreType !CoreType
    | SemanticGlobalExpansionNotTransparent !ObjectId
    | SemanticGlobalContextualRequirementsEmpty !ObjectId
    | SemanticGlobalContextualRequirementMissing !StructSymbol !ObjectId
    | SemanticGlobalContextualRequirementIsIntrinsic !StructSymbol !ObjectId
    | SemanticGlobalContextualRequirementTypeMismatch
        !StructSymbol !ObjectId !CoreType !CoreType
    | SemanticGlobalContextualRequirementNotProvided
        !StructSymbol !ObjectId
    | SemanticGlobalContextualRequirementNotReferenced !StructSymbol !ObjectId
    deriving stock (Show, Eq)

validateSemanticGlobalBindingTarget
    :: Set.Set (StructSymbol, ObjectId)
    -> CheckedObjectClosure
    -> SemanticGlobalBinding
    -> Either SemanticGlobalTargetError ()
validateSemanticGlobalBindingTarget operationBindings closure binding = do
    expected <-
        maybe
            (Left (SemanticGlobalKeyHasInconsistentArity key))
            Right
            (semanticGlobalKeyType key)
    content <-
        maybe
            (Left (SemanticGlobalTargetMissing identity))
            Right
            (lookupCheckedObjectContent identity closure)
    when
        (objectIdFamily identity == IntrinsicObject)
        (Left (SemanticGlobalTargetIsIntrinsic identity))
    let targetExpected =
            case target of
                ContextualTransparentExpansion{} ->
                    TyArrow TySet expected
                _ -> expected
        actual = objectContentType content
    unless
        (actual == targetExpected)
        (Left
            (SemanticGlobalTargetTypeMismatch
                identity targetExpected actual))
    case target of
        GlobalReference{} -> pure ()
        TransparentExpansion{} ->
            validateTransparent content
        ContextualTransparentExpansion _ requirements -> do
            validateTransparent content
            when
                (Map.null requirements)
                (Left (SemanticGlobalContextualRequirementsEmpty identity))
            traverse_ (validateRequirement content) (Map.toAscList requirements)
  where
    key = semanticGlobalBindingKey binding
    target = semanticGlobalBindingTarget binding
    identity = semanticGlobalTargetObject target

    validateTransparent = \case
        TransparentObjectContent{} -> pure ()
        _ -> Left (SemanticGlobalExpansionNotTransparent identity)

    validateRequirement content (symbol, object) = do
        operationContent <-
            maybe
                (Left
                    (SemanticGlobalContextualRequirementMissing
                        symbol object))
                Right
                (lookupCheckedObjectContent object closure)
        when
            (objectIdFamily object == IntrinsicObject)
            (Left
                (SemanticGlobalContextualRequirementIsIntrinsic
                    symbol object))
        let expectedOperation = TyArrow TySet TySet
            actualOperation = objectContentType operationContent
        unless
            (actualOperation == expectedOperation)
            (Left
                (SemanticGlobalContextualRequirementTypeMismatch
                    symbol object expectedOperation actualOperation))
        unless
            ((symbol, object) `Set.member` operationBindings)
            (Left
                (SemanticGlobalContextualRequirementNotProvided
                    symbol object))
        case content of
            TransparentObjectContent _theory _coreType body ->
                unless
                    (object `Set.member` canonicalTermGlobals body)
                    (Left
                        (SemanticGlobalContextualRequirementNotReferenced
                            symbol object))
            _ -> impossible "a contextual expansion was not transparent"

data SemanticEnvironmentDelta
    = EmptySemanticEnvironmentDelta
    | SemanticGlobalBindings ![SemanticGlobalBinding]
    | SemanticGlobalBindingsAndStructures
        ![SemanticGlobalBinding]
        ![SemanticStructureDescriptor]
    deriving stock (Show, Eq, Ord, Generic)
    deriving anyclass (NFData)

data SemanticStructurePhrase = SemanticStructurePhrase
    !Pattern
    !Pattern
    !Marker
    deriving stock (Show, Eq, Ord, Generic)
    deriving anyclass (NFData)

semanticStructurePhrase :: LexicalItemSgPl -> SemanticStructurePhrase
semanticStructurePhrase (LexicalItemSgPl forms marker) =
    SemanticStructurePhrase (sg forms) (pl forms) marker

semanticStructurePhraseSingular :: SemanticStructurePhrase -> Pattern
semanticStructurePhraseSingular (SemanticStructurePhrase singular _ _) =
    singular

semanticStructurePhrasePlural :: SemanticStructurePhrase -> Pattern
semanticStructurePhrasePlural (SemanticStructurePhrase _ plural _) =
    plural

semanticStructurePhraseMarker :: SemanticStructurePhrase -> Marker
semanticStructurePhraseMarker (SemanticStructurePhrase _ _ marker) =
    marker

data SemanticStructureOperation = SemanticStructureOperation
    !StructSymbol
    !ObjectId
    deriving stock (Show, Eq, Ord, Generic)
    deriving anyclass (NFData)

semanticStructureOperation
    :: StructSymbol
    -> ObjectId
    -> SemanticStructureOperation
semanticStructureOperation =
    SemanticStructureOperation

semanticStructureOperationSymbol
    :: SemanticStructureOperation
    -> StructSymbol
semanticStructureOperationSymbol (SemanticStructureOperation symbol _) =
    symbol

semanticStructureOperationObject
    :: SemanticStructureOperation
    -> ObjectId
semanticStructureOperationObject (SemanticStructureOperation _ object) =
    object

data SemanticStructureDescriptor = SemanticStructureDescriptor
    !SemanticStructurePhrase
    !(Maybe ObjectId)
    ![SemanticStructurePhrase]
    ![SemanticStructureOperation]
    deriving stock (Show, Eq, Ord, Generic)
    deriving anyclass (NFData)

semanticStructureDescriptor
    :: SemanticStructurePhrase
    -> Maybe ObjectId
    -> [SemanticStructurePhrase]
    -> [SemanticStructureOperation]
    -> Either SemanticEnvironmentError SemanticStructureDescriptor
semanticStructureDescriptor structurePhrase predicate parents operations = do
    case firstDuplicate parents of
        Just duplicate ->
            Left (DuplicateSemanticStructureParent duplicate)
        Nothing -> pure ()
    when
        (structurePhrase `elem` parents)
        (Left (SelfSemanticStructureParent structurePhrase))
    case firstDuplicate (semanticStructureOperationSymbol <$> operations) of
        Just duplicate ->
            Left (DuplicateSemanticStructureOperation duplicate)
        Nothing -> pure ()
    pure
        (SemanticStructureDescriptor
            structurePhrase predicate parents operations)

semanticStructureDescriptorPhrase
    :: SemanticStructureDescriptor
    -> SemanticStructurePhrase
semanticStructureDescriptorPhrase
        (SemanticStructureDescriptor structurePhrase _ _ _) =
    structurePhrase

semanticStructureDescriptorPredicate
    :: SemanticStructureDescriptor
    -> Maybe ObjectId
semanticStructureDescriptorPredicate
        (SemanticStructureDescriptor _ predicate _ _) =
    predicate

semanticStructureDescriptorParents
    :: SemanticStructureDescriptor
    -> [SemanticStructurePhrase]
semanticStructureDescriptorParents
        (SemanticStructureDescriptor _ _ parents _) =
    parents

semanticStructureDescriptorOperations
    :: SemanticStructureDescriptor
    -> [SemanticStructureOperation]
semanticStructureDescriptorOperations
        (SemanticStructureDescriptor _ _ _ operations) =
    operations

data SemanticEnvironmentError
    = DuplicateSemanticGlobalKey !SemanticGlobalKey
    | NonCanonicalSemanticGlobalBindingOrder
    | DuplicateSemanticStructure !SemanticStructurePhrase
    | NonCanonicalSemanticStructureOrder
    | DuplicateSemanticStructureParent !SemanticStructurePhrase
    | SelfSemanticStructureParent !SemanticStructurePhrase
    | DuplicateSemanticStructureOperation !StructSymbol
    deriving stock (Show, Eq)

emptySemanticEnvironmentDelta :: SemanticEnvironmentDelta
emptySemanticEnvironmentDelta =
    EmptySemanticEnvironmentDelta

semanticEnvironmentDelta
    :: [SemanticGlobalBinding]
    -> Either SemanticEnvironmentError SemanticEnvironmentDelta
semanticEnvironmentDelta bindings =
    semanticEnvironmentWithStructures bindings []

semanticEnvironmentWithStructures
    :: [SemanticGlobalBinding]
    -> [SemanticStructureDescriptor]
    -> Either SemanticEnvironmentError SemanticEnvironmentDelta
semanticEnvironmentWithStructures [] [] =
    Right EmptySemanticEnvironmentDelta
semanticEnvironmentWithStructures bindings structures = do
    case firstDuplicate (semanticGlobalBindingKey <$> bindings) of
        Just duplicate ->
            Left (DuplicateSemanticGlobalKey duplicate)
        Nothing ->
            pure ()
    unless
        (bindings == List.sortOn semanticGlobalBindingKey bindings)
        (Left NonCanonicalSemanticGlobalBindingOrder)
    case firstDuplicate (semanticStructureDescriptorPhrase <$> structures) of
        Just duplicate ->
            Left (DuplicateSemanticStructure duplicate)
        Nothing -> pure ()
    unless
        ( structures
            == List.sortOn semanticStructureDescriptorPhrase structures
        )
        (Left NonCanonicalSemanticStructureOrder)
    pure
        (case structures of
            [] -> SemanticGlobalBindings bindings
            _ -> SemanticGlobalBindingsAndStructures bindings structures)

semanticEnvironmentBindings
    :: SemanticEnvironmentDelta
    -> [SemanticGlobalBinding]
semanticEnvironmentBindings = \case
    EmptySemanticEnvironmentDelta -> []
    SemanticGlobalBindings bindings -> bindings
    SemanticGlobalBindingsAndStructures bindings _ -> bindings

semanticEnvironmentStructures
    :: SemanticEnvironmentDelta
    -> [SemanticStructureDescriptor]
semanticEnvironmentStructures = \case
    EmptySemanticEnvironmentDelta -> []
    SemanticGlobalBindings{} -> []
    SemanticGlobalBindingsAndStructures _ structures -> structures


data DeclarationInterfaceDelta = DeclarationInterfaceDelta
    !DeclarationSlot
    ![SemanticFactOccurrence]
    ![SemanticAlias]
    ![ObjectId]
    ![PropositionId]
    !SemanticEnvironmentDelta
    deriving stock (Show, Eq, Ord, Generic)

data DeclarationInterfaceError
    = DeclarationFactOwnerMismatch !FactSlot
    | DuplicateDeclarationFactSlot !FactSlot
    | DuplicateDeclarationFactFingerprint
        !SemanticFactOccurrenceFingerprint
    | DuplicateDeclarationAlias !SemanticName
    | DuplicateDeclarationObject !ObjectId
    | DuplicateDeclarationProposition !PropositionId
    | DeclarationFactPropositionMissing !PropositionId
    deriving stock (Show, Eq)

declarationInterfaceDelta
    :: DeclarationSlot
    -> [SemanticFactOccurrence]
    -> [SemanticAlias]
    -> [ObjectId]
    -> [PropositionId]
    -> SemanticEnvironmentDelta
    -> Either DeclarationInterfaceError DeclarationInterfaceDelta
declarationInterfaceDelta
        slot facts aliases objects propositions environment = do
    traverse_ validateFact facts
    rejectDuplicate
        DuplicateDeclarationFactSlot
        (semanticFactSlot <$> facts)
    rejectDuplicate
        DuplicateDeclarationFactFingerprint
        (semanticFactFingerprint <$> facts)
    rejectDuplicate
        DuplicateDeclarationAlias
        (semanticAliasName <$> aliases)
    rejectDuplicate DuplicateDeclarationObject objects
    rejectDuplicate DuplicateDeclarationProposition propositions
    pure
        (DeclarationInterfaceDelta
            slot facts aliases objects propositions environment)
  where
    owner = declarationSlotModule slot
    propositionSet = Set.fromList propositions

    validateFact occurrence = do
        unless
            (factSlotModule (semanticFactSlot occurrence) == owner)
            (Left
                (DeclarationFactOwnerMismatch
                    (semanticFactSlot occurrence)))
        let proposition =
                semanticFactProposition occurrence
        unless
            (proposition `Set.member` propositionSet)
            (Left (DeclarationFactPropositionMissing proposition))

declarationDeltaSlot
    :: DeclarationInterfaceDelta
    -> DeclarationSlot
declarationDeltaSlot
        (DeclarationInterfaceDelta slot _ _ _ _ _) =
    slot

declarationDeltaFacts
    :: DeclarationInterfaceDelta
    -> [SemanticFactOccurrence]
declarationDeltaFacts
        (DeclarationInterfaceDelta _ facts _ _ _ _) =
    facts

declarationDeltaAliases
    :: DeclarationInterfaceDelta
    -> [SemanticAlias]
declarationDeltaAliases
        (DeclarationInterfaceDelta _ _ aliases _ _ _) =
    aliases

declarationDeltaObjects
    :: DeclarationInterfaceDelta
    -> [ObjectId]
declarationDeltaObjects
        (DeclarationInterfaceDelta _ _ _ objects _ _) =
    objects

declarationDeltaPropositions
    :: DeclarationInterfaceDelta
    -> [PropositionId]
declarationDeltaPropositions
        (DeclarationInterfaceDelta _ _ _ _ propositions _) =
    propositions

declarationDeltaEnvironment
    :: DeclarationInterfaceDelta
    -> SemanticEnvironmentDelta
declarationDeltaEnvironment
        (DeclarationInterfaceDelta _ _ _ _ _ environment) =
    environment


newtype SemanticInterfaceId =
    SemanticInterfaceId CacheDigest
    deriving stock (Show, Eq, Ord, Generic)
    deriving newtype (Hashable, NFData)

semanticInterfaceIdDigest
    :: SemanticInterfaceId
    -> CacheDigest
semanticInterfaceIdDigest (SemanticInterfaceId digest) =
    digest

data SemanticInterface = SemanticInterface
    !ModuleName
    ![SemanticInterfaceId]
    ![DeclarationInterfaceDelta]
    !SemanticInterfaceId
    deriving stock (Show, Eq, Ord)

data SemanticInterfaceError
    = DuplicateDirectSemanticInterface !SemanticInterfaceId
    | SemanticDeclarationOwnerMismatch !DeclarationSlot
    | NonIncreasingDeclarationSlots
    | NonIncreasingFactSlots
    | SemanticInterfaceIdMismatch
        !SemanticInterfaceId
        !SemanticInterfaceId
    deriving stock (Show, Eq)

renderSemanticInterfaceError :: SemanticInterfaceError -> Text
renderSemanticInterfaceError = \case
    DuplicateDirectSemanticInterface interface ->
        "direct semantic interface occurs more than once: "
            <> Text.pack (show interface)
    SemanticDeclarationOwnerMismatch slot ->
        "declaration belongs to a different module: "
            <> Text.pack (show slot)
    NonIncreasingDeclarationSlots ->
        "declaration slots are not in increasing order"
    NonIncreasingFactSlots ->
        "fact slots are not in increasing order"
    SemanticInterfaceIdMismatch expected actual ->
        "semantic interface identity mismatch: expected "
            <> Text.pack (show expected)
            <> ", found " <> Text.pack (show actual)

semanticInterface
    :: ModuleName
    -> [SemanticInterfaceId]
    -> [DeclarationInterfaceDelta]
    -> Either SemanticInterfaceError SemanticInterface
semanticInterface owner direct declarations = do
    validateSemanticInterfaceStructure owner direct declarations
    let identity =
            computeSemanticInterfaceId owner direct declarations
    pure (SemanticInterface owner direct declarations identity)

validateSemanticInterface
    :: ModuleName
    -> [SemanticInterfaceId]
    -> [DeclarationInterfaceDelta]
    -> SemanticInterfaceId
    -> Either SemanticInterfaceError SemanticInterface
validateSemanticInterface owner direct declarations asserted = do
    validateSemanticInterfaceStructure owner direct declarations
    let computed =
            computeSemanticInterfaceId
                owner direct declarations
    unless
        (asserted == computed)
        (Left
            (SemanticInterfaceIdMismatch asserted computed))
    pure
        (SemanticInterface
            owner direct declarations asserted)

validateSemanticInterfaceStructure
    :: ModuleName
    -> [SemanticInterfaceId]
    -> [DeclarationInterfaceDelta]
    -> Either SemanticInterfaceError ()
validateSemanticInterfaceStructure owner direct declarations = do
    rejectDuplicate
        DuplicateDirectSemanticInterface
        direct
    traverse_
        (\delta ->
            unless
                (declarationSlotModule
                    (declarationDeltaSlot delta)
                    == owner)
                (Left
                    (SemanticDeclarationOwnerMismatch
                        (declarationDeltaSlot delta))))
        declarations
    unless
        (strictlyIncreasing
            ( localDeclarationOrdinalValue
                . declarationSlotOrdinal
                . declarationDeltaSlot
                <$> declarations))
        (Left NonIncreasingDeclarationSlots)
    unless
        (strictlyIncreasing
            ( localFactOrdinalValue
                . factSlotOrdinal
                . semanticFactSlot
                <$> concatMap
                    declarationDeltaFacts
                    declarations))
        (Left NonIncreasingFactSlots)

semanticInterfaceOwner :: SemanticInterface -> ModuleName
semanticInterfaceOwner
        (SemanticInterface owner _ _ _) =
    owner

semanticInterfaceDirectInputs
    :: SemanticInterface
    -> [SemanticInterfaceId]
semanticInterfaceDirectInputs
        (SemanticInterface _ direct _ _) =
    direct

semanticInterfaceDeclarations
    :: SemanticInterface
    -> [DeclarationInterfaceDelta]
semanticInterfaceDeclarations
        (SemanticInterface _ _ declarations _) =
    declarations

semanticInterfaceAssertedId
    :: SemanticInterface
    -> SemanticInterfaceId
semanticInterfaceAssertedId
        (SemanticInterface _ _ _ asserted) =
    asserted

computeSemanticInterfaceId
    :: ModuleName
    -> [SemanticInterfaceId]
    -> [DeclarationInterfaceDelta]
    -> SemanticInterfaceId
computeSemanticInterfaceId owner direct declarations =
    SemanticInterfaceId
        (hashCacheFields
            "felix-semantic-interface-v1"
            [ encodeCache (putModuleNameCache owner)
            , encodeCache
                (putCacheList
                    putSemanticInterfaceIdCache
                    direct)
            , encodeCache
                (putCacheList
                    putDeclarationInterfaceDeltaCache
                    declarations)
            ])


newtype PrefixContextId =
    PrefixContextId CacheDigest
    deriving stock (Show, Eq, Ord, Generic)
    deriving newtype (Hashable, NFData)

data PrefixContextError
    = DuplicateInitialPrefixSemanticInput !SemanticInterfaceId
    deriving stock (Show, Eq)

initialPrefixContextId
    :: TheoryId
    -> ModuleName
    -> [SemanticInterfaceId]
    -> Either PrefixContextError PrefixContextId
initialPrefixContextId theory owner direct = do
    rejectDuplicate
        DuplicateInitialPrefixSemanticInput
        direct
    pure
        (PrefixContextId
            (hashCacheFields
                "felix-prefix-initial-v1"
                [ encodeCache (putTheoryIdCache theory)
                , encodeCache (putModuleNameCache owner)
                , encodeCache
                    (putCacheList
                        putSemanticInterfaceIdCache
                        direct)
                ]))

nextPrefixContextId
    :: PrefixContextId
    -> DeclarationInterfaceDelta
    -> PrefixContextId
nextPrefixContextId previous delta =
    PrefixContextId
        (hashCacheFields
            "felix-prefix-step-v1"
            [ encodeCache (putPrefixContextIdCache previous)
            , encodeCache
                (putDeclarationInterfaceDeltaCache delta)
            ])

prefixContextIdDigest :: PrefixContextId -> CacheDigest
prefixContextIdDigest (PrefixContextId digest) =
    digest


newtype ProofSyntaxId =
    ProofSyntaxId CacheDigest
    deriving stock (Show, Eq, Ord, Generic)
    deriving newtype (Hashable, NFData)

proofSyntaxId :: ByteString -> ProofSyntaxId
proofSyntaxId bytes =
    ProofSyntaxId
        (hashCacheFields "felix-proof-syntax-v1" [bytes])

newtype DeclarationSyntaxId =
    DeclarationSyntaxId CacheDigest
    deriving stock (Show, Eq, Ord, Generic)
    deriving newtype (Hashable, NFData)

declarationSyntaxId :: ByteString -> DeclarationSyntaxId
declarationSyntaxId bytes =
    DeclarationSyntaxId
        (hashCacheFields "felix-declaration-syntax-v1" [bytes])

newtype ProofValidationKey =
    ProofValidationKey CacheDigest
    deriving stock (Show, Eq, Ord, Generic)
    deriving newtype (Hashable, NFData)

proofValidationKey
    :: TheoremId
    -> ProofSyntaxId
    -> PrefixContextId
    -> ProofValidationKey
proofValidationKey theorem (ProofSyntaxId syntax) prefix =
    ProofValidationKey
        (hashCacheFields
            "felix-proof-validation"
            [ mathematicalDigestBytes
                (theoremIdDigest theorem)
            , cacheDigestBytes syntax
            , encodeCache (putPrefixContextIdCache prefix)
            ])

proofValidationKeyDigest
    :: ProofValidationKey
    -> CacheDigest
proofValidationKeyDigest (ProofValidationKey digest) =
    digest

data ProofValidationRecord = ProofValidationRecord
    !ProofValidationKey
    !ValidationCertificate
    deriving stock (Show, Eq, Ord, Generic)

proofValidationRecord
    :: ProofValidationKey
    -> ValidationCertificate
    -> ProofValidationRecord
proofValidationRecord =
    ProofValidationRecord

proofValidationRecordKey
    :: ProofValidationRecord
    -> ProofValidationKey
proofValidationRecordKey
        (ProofValidationRecord key _) =
    key

proofValidationRecordCertificate
    :: ProofValidationRecord
    -> ValidationCertificate
proofValidationRecordCertificate
        (ProofValidationRecord _ certificate) =
    certificate

newtype DeclarationValidationKey =
    DeclarationValidationKey CacheDigest
    deriving stock (Show, Eq, Ord, Generic)
    deriving newtype (Hashable, NFData)

declarationValidationKey
    :: DeclarationSyntaxId
    -> PrefixContextId
    -> [ObjectId]
    -> [TheoremId]
    -> DeclarationValidationKey
declarationValidationKey
        (DeclarationSyntaxId syntax)
        prefix objects theorems =
    DeclarationValidationKey
        (hashCacheFields
            "felix-declaration-validation"
            [ cacheDigestBytes syntax
            , encodeCache (putPrefixContextIdCache prefix)
            , encodeCache (putCacheList putObjectIdCache objects)
            , encodeCache
                (putCacheList
                    (putMathematicalDigestCache . theoremIdDigest)
                    theorems)
            ])

declarationValidationKeyDigest
    :: DeclarationValidationKey
    -> CacheDigest
declarationValidationKeyDigest
        (DeclarationValidationKey digest) =
    digest

data DeclarationValidationRecord = DeclarationValidationRecord
    !DeclarationValidationKey
    ![ValidationCertificate]
    deriving stock (Show, Eq, Ord, Generic)

declarationValidationRecord
    :: DeclarationValidationKey
    -> [ValidationCertificate]
    -> DeclarationValidationRecord
declarationValidationRecord =
    DeclarationValidationRecord

declarationValidationRecordKey
    :: DeclarationValidationRecord
    -> DeclarationValidationKey
declarationValidationRecordKey
        (DeclarationValidationRecord key _) =
    key

declarationValidationRecordCertificates
    :: DeclarationValidationRecord
    -> [ValidationCertificate]
declarationValidationRecordCertificates
        (DeclarationValidationRecord _ certificates) =
    certificates


data ModuleArtifactKey = ModuleArtifactKey
    !ModuleName
    !ParsedModuleId
    ![SemanticInterfaceId]
    !TheoryId
    deriving stock (Show, Eq, Ord)

data ModuleArtifactKeyError
    = DuplicateModuleArtifactSemanticInput
        !SemanticInterfaceId
    deriving stock (Show, Eq)

moduleArtifactKey
    :: ModuleName
    -> ParsedModuleId
    -> [SemanticInterfaceId]
    -> TheoryId
    -> Either ModuleArtifactKeyError ModuleArtifactKey
moduleArtifactKey owner parsed direct theory = do
    rejectDuplicate
        DuplicateModuleArtifactSemanticInput
        direct
    pure (ModuleArtifactKey owner parsed direct theory)

moduleArtifactKeyOwner :: ModuleArtifactKey -> ModuleName
moduleArtifactKeyOwner (ModuleArtifactKey owner _parsed _direct _theory) =
    owner

moduleArtifactKeyDirectSemanticInputs
    :: ModuleArtifactKey
    -> [SemanticInterfaceId]
moduleArtifactKeyDirectSemanticInputs
        (ModuleArtifactKey _owner _parsed direct _theory) =
    direct

moduleArtifactKeyTheory :: ModuleArtifactKey -> TheoryId
moduleArtifactKeyTheory
        (ModuleArtifactKey _owner _parsed _direct theory) =
    theory

newtype ModuleArtifactId =
    ModuleArtifactId CacheDigest
    deriving stock (Show, Eq, Ord, Generic)
    deriving newtype (Hashable, NFData)

moduleArtifactId :: ModuleArtifactKey -> ModuleArtifactId
moduleArtifactId key =
    ModuleArtifactId
        (hashCacheFields
            "felix-module-artifact-v1"
            [encodeCache (putModuleArtifactKeyCache key)])

moduleArtifactIdDigest :: ModuleArtifactId -> CacheDigest
moduleArtifactIdDigest (ModuleArtifactId digest) =
    digest

data ModuleArtifactResult = ModuleArtifactResult
    !ModuleArtifactId
    !SyntaxInterfaceId
    !SemanticInterfaceId
    deriving stock (Show, Eq, Ord, Generic)
    deriving anyclass (NFData)

moduleArtifactResult
    :: ModuleArtifactKey
    -> SyntaxInterfaceId
    -> SemanticInterfaceId
    -> ModuleArtifactResult
moduleArtifactResult key =
    ModuleArtifactResult (moduleArtifactId key)

moduleArtifactResultId
    :: ModuleArtifactResult
    -> ModuleArtifactId
moduleArtifactResultId
        (ModuleArtifactResult identity _ _) =
    identity

moduleArtifactResultSyntax
    :: ModuleArtifactResult
    -> SyntaxInterfaceId
moduleArtifactResultSyntax
        (ModuleArtifactResult _ syntax _) =
    syntax

moduleArtifactResultSemantic
    :: ModuleArtifactResult
    -> SemanticInterfaceId
moduleArtifactResultSemantic
        (ModuleArtifactResult _ _ semantic) =
    semantic


putSemanticFactOccurrenceFingerprintCache
    :: SemanticFactOccurrenceFingerprint
    -> CachePut
putSemanticFactOccurrenceFingerprintCache
        (SemanticFactOccurrenceFingerprint digest) =
    putCacheDigest digest

getSemanticFactOccurrenceFingerprintCache
    :: CacheGet SemanticFactOccurrenceFingerprint
getSemanticFactOccurrenceFingerprintCache =
    SemanticFactOccurrenceFingerprint <$> getCacheDigest

putSemanticFactOccurrenceCache
    :: SemanticFactOccurrence
    -> CachePut
putSemanticFactOccurrenceCache
        (SemanticFactOccurrence slot authority eligibility) = do
    putFactSlotCache slot
    putFactAuthorityCache authority
    putEligibility eligibility

getSemanticFactOccurrenceCache
    :: CacheGet SemanticFactOccurrence
getSemanticFactOccurrenceCache =
    semanticFactOccurrence
        <$> getFactSlotCache
        <*> getFactAuthorityCache
        <*> getEligibility

putSemanticEnvironmentDeltaCache
    :: SemanticEnvironmentDelta
    -> CachePut
putSemanticEnvironmentDeltaCache EmptySemanticEnvironmentDelta =
    putCacheTag 0x00
putSemanticEnvironmentDeltaCache (SemanticGlobalBindings bindings) = do
    putCacheTag 0x01
    putCacheList putSemanticGlobalBindingCache bindings
putSemanticEnvironmentDeltaCache
        (SemanticGlobalBindingsAndStructures bindings structures) = do
    putCacheTag 0x02
    putCacheList putSemanticGlobalBindingCache bindings
    putCacheList putSemanticStructureDescriptorCache structures

getSemanticEnvironmentDeltaCache
    :: CacheGet SemanticEnvironmentDelta
getSemanticEnvironmentDeltaCache =
    getCacheTag >>= \case
        0x00 ->
            pure EmptySemanticEnvironmentDelta
        0x01 -> do
            bindings <- getCacheList getSemanticGlobalBindingCache
            either
                (fail . ("invalid semantic environment delta: " <>) . show)
                pure
                (semanticEnvironmentDelta bindings)
        0x02 -> do
            bindings <- getCacheList getSemanticGlobalBindingCache
            structures <- getCacheList getSemanticStructureDescriptorCache
            either
                (fail . ("invalid semantic environment delta: " <>) . show)
                pure
                (semanticEnvironmentWithStructures bindings structures)
        tag ->
            fail
                ("unknown semantic environment delta tag "
                    <> show tag)

putSemanticGlobalKeyCache :: SemanticGlobalKey -> CachePut
putSemanticGlobalKeyCache = \case
    SemanticLeftAdjective pat -> do
        putCacheTag 0x00
        putPatternCache pat
    SemanticRightAdjective pat -> do
        putCacheTag 0x01
        putPatternCache pat
    SemanticFunctionPhrase singular plural -> do
        putCacheTag 0x02
        putPatternCache singular
        putPatternCache plural
    SemanticNoun singular plural -> do
        putCacheTag 0x03
        putPatternCache singular
        putPatternCache plural
    SemanticVerb singular plural -> do
        putCacheTag 0x04
        putPatternCache singular
        putPatternCache plural
    SemanticRelation token arity -> do
        putCacheTag 0x05
        putTokenCache token
        putCacheNatural (parameterArityValue arity)
    SemanticExpressionFunction pat -> do
        putCacheTag 0x06
        putPatternCache pat
    SemanticPrefixPredicate command arity -> do
        putCacheTag 0x07
        putCacheText command
        putCacheNatural arity

getSemanticGlobalKeyCache :: CacheGet SemanticGlobalKey
getSemanticGlobalKeyCache =
    getCacheTag >>= \case
        0x00 -> SemanticLeftAdjective <$> getPatternCache
        0x01 -> SemanticRightAdjective <$> getPatternCache
        0x02 ->
            SemanticFunctionPhrase
                <$> getPatternCache
                <*> getPatternCache
        0x03 ->
            SemanticNoun
                <$> getPatternCache
                <*> getPatternCache
        0x04 ->
            SemanticVerb
                <$> getPatternCache
                <*> getPatternCache
        0x05 ->
            SemanticRelation
                <$> getTokenCache
                <*> (ParameterArity <$> getCacheNatural)
        0x06 -> SemanticExpressionFunction <$> getPatternCache
        0x07 ->
            SemanticPrefixPredicate
                <$> getCacheText
                <*> getCacheNatural
        tag ->
            fail ("unknown semantic global key tag " <> show tag)

putSemanticGlobalBindingCache :: SemanticGlobalBinding -> CachePut
putSemanticGlobalBindingCache (SemanticGlobalBinding key target) = do
    putSemanticGlobalKeyCache key
    case target of
        GlobalReference identity -> do
            putCacheTag 0x00
            putObjectIdCache identity
        TransparentExpansion identity -> do
            putCacheTag 0x01
            putObjectIdCache identity
        ContextualTransparentExpansion identity requirements -> do
            putCacheTag 0x02
            putObjectIdCache identity
            putCanonicalCacheMap
                (\(StructSymbol symbol) -> putCacheText symbol)
                putObjectIdCache
                requirements

getSemanticGlobalBindingCache :: CacheGet SemanticGlobalBinding
getSemanticGlobalBindingCache =
    SemanticGlobalBinding
        <$> getSemanticGlobalKeyCache
        <*> (getCacheTag >>= \case
                0x00 -> GlobalReference <$> getObjectIdCache
                0x01 -> TransparentExpansion <$> getObjectIdCache
                0x02 ->
                    ContextualTransparentExpansion
                        <$> getObjectIdCache
                        <*> getCanonicalCacheMap
                            (StructSymbol <$> getCacheText)
                            getObjectIdCache
                tag ->
                    fail
                        ("unknown semantic global target tag "
                            <> show tag))

putSemanticStructureDescriptorCache
    :: SemanticStructureDescriptor
    -> CachePut
putSemanticStructureDescriptorCache
        (SemanticStructureDescriptor structurePhrase predicate parents operations) = do
    putSemanticStructurePhraseCache structurePhrase
    putCacheMaybe putObjectIdCache predicate
    putCacheList putSemanticStructurePhraseCache parents
    putCacheList putSemanticStructureOperationCache operations

getSemanticStructureDescriptorCache
    :: CacheGet SemanticStructureDescriptor
getSemanticStructureDescriptorCache = do
    structurePhrase <- getSemanticStructurePhraseCache
    predicate <- getCacheMaybe getObjectIdCache
    parents <- getCacheList getSemanticStructurePhraseCache
    operations <- getCacheList getSemanticStructureOperationCache
    either
        (fail . ("invalid semantic structure descriptor: " <>) . show)
        pure
        (semanticStructureDescriptor structurePhrase predicate parents operations)

putSemanticStructurePhraseCache
    :: SemanticStructurePhrase
    -> CachePut
putSemanticStructurePhraseCache
        (SemanticStructurePhrase singular plural (Marker marker)) = do
    putPatternCache singular
    putPatternCache plural
    putCacheText marker

getSemanticStructurePhraseCache
    :: CacheGet SemanticStructurePhrase
getSemanticStructurePhraseCache =
    SemanticStructurePhrase
        <$> getPatternCache
        <*> getPatternCache
        <*> (Marker <$> getCacheText)

putSemanticStructureOperationCache
    :: SemanticStructureOperation
    -> CachePut
putSemanticStructureOperationCache
        (SemanticStructureOperation (StructSymbol symbol) object) = do
    putCacheText symbol
    putObjectIdCache object

getSemanticStructureOperationCache
    :: CacheGet SemanticStructureOperation
getSemanticStructureOperationCache =
    SemanticStructureOperation
        <$> (StructSymbol <$> getCacheText)
        <*> getObjectIdCache

putDeclarationInterfaceDeltaCache
    :: DeclarationInterfaceDelta
    -> CachePut
putDeclarationInterfaceDeltaCache
        (DeclarationInterfaceDelta
            slot facts aliases objects propositions environment) = do
    putDeclarationSlotCache slot
    putCacheList putSemanticFactOccurrenceCache facts
    putCacheList putSemanticAliasCache aliases
    putCacheList putObjectIdCache objects
    putCacheList putPropositionIdCache propositions
    putSemanticEnvironmentDeltaCache environment

getDeclarationInterfaceDeltaCache
    :: CacheGet DeclarationInterfaceDelta
getDeclarationInterfaceDeltaCache = do
    slot <- getDeclarationSlotCache
    facts <- getCacheList getSemanticFactOccurrenceCache
    aliases <- getCacheList getSemanticAliasCache
    objects <- getCacheList getObjectIdCache
    propositions <- getCacheList getPropositionIdCache
    environment <- getSemanticEnvironmentDeltaCache
    either
        (fail . ("invalid declaration interface delta: " <>) . show)
        pure
        (declarationInterfaceDelta
            slot facts aliases objects propositions environment)

putSemanticInterfaceCache :: SemanticInterface -> CachePut
putSemanticInterfaceCache
        (SemanticInterface owner direct declarations asserted) = do
    putModuleNameCache owner
    putCacheList putSemanticInterfaceIdCache direct
    putCacheList putDeclarationInterfaceDeltaCache declarations
    putSemanticInterfaceIdCache asserted

getSemanticInterfaceCache :: CacheGet SemanticInterface
getSemanticInterfaceCache = do
    owner <- getModuleNameCache
    direct <- getCacheList getSemanticInterfaceIdCache
    declarations <- getCacheList getDeclarationInterfaceDeltaCache
    asserted <- getSemanticInterfaceIdCache
    either
        (fail . ("invalid semantic interface: " <>) . show)
        pure
        (validateSemanticInterface
            owner direct declarations asserted)

putSemanticInterfaceIdCache :: SemanticInterfaceId -> CachePut
putSemanticInterfaceIdCache (SemanticInterfaceId digest) =
    putCacheDigest digest

getSemanticInterfaceIdCache :: CacheGet SemanticInterfaceId
getSemanticInterfaceIdCache =
    SemanticInterfaceId <$> getCacheDigest

putPrefixContextIdCache :: PrefixContextId -> CachePut
putPrefixContextIdCache (PrefixContextId digest) =
    putCacheDigest digest

getPrefixContextIdCache :: CacheGet PrefixContextId
getPrefixContextIdCache =
    PrefixContextId <$> getCacheDigest

putModuleArtifactKeyCache :: ModuleArtifactKey -> CachePut
putModuleArtifactKeyCache =
    putModuleArtifactKeyFields

getModuleArtifactKeyCache :: CacheGet ModuleArtifactKey
getModuleArtifactKeyCache = do
    owner <- getModuleNameCache
    parsed <- getParsedModuleIdCache
    direct <- getCacheList getSemanticInterfaceIdCache
    theory <- getTheoryIdCache
    either
        (fail . ("invalid module artifact key: " <>) . show)
        pure
        (moduleArtifactKey owner parsed direct theory)

putModuleArtifactIdCache :: ModuleArtifactId -> CachePut
putModuleArtifactIdCache (ModuleArtifactId digest) =
    putCacheDigest digest

getModuleArtifactIdCache :: CacheGet ModuleArtifactId
getModuleArtifactIdCache =
    ModuleArtifactId <$> getCacheDigest

putModuleArtifactResultCache
    :: ModuleArtifactResult
    -> CachePut
putModuleArtifactResultCache
        (ModuleArtifactResult identity syntax semantic) = do
    putModuleArtifactIdCache identity
    putSyntaxInterfaceIdCache syntax
    putSemanticInterfaceIdCache semantic

getModuleArtifactResultCache
    :: ModuleArtifactId
    -> CacheGet ModuleArtifactResult
getModuleArtifactResultCache expected = do
    asserted <- getModuleArtifactIdCache
    unless
        (asserted == expected)
        (fail "module artifact result ID mismatch")
    ModuleArtifactResult asserted
        <$> getSyntaxInterfaceIdCache
        <*> getSemanticInterfaceIdCache

putProofValidationRecordCache
    :: ProofValidationRecord
    -> CachePut
putProofValidationRecordCache
        (ProofValidationRecord key certificate) = do
    putProofValidationKeyCache key
    putValidationCertificateCache certificate

getProofValidationRecordCache
    :: CacheGet ProofValidationRecord
getProofValidationRecordCache =
    ProofValidationRecord
        <$> getProofValidationKeyCache
        <*> getValidationCertificateCache

putDeclarationValidationRecordCache
    :: DeclarationValidationRecord
    -> CachePut
putDeclarationValidationRecordCache
        (DeclarationValidationRecord key certificates) = do
    putDeclarationValidationKeyCache key
    putCacheList putValidationCertificateCache certificates

getDeclarationValidationRecordCache
    :: CacheGet DeclarationValidationRecord
getDeclarationValidationRecordCache =
    DeclarationValidationRecord
        <$> getDeclarationValidationKeyCache
        <*> getCacheList getValidationCertificateCache


putDeclarationSlotCache :: DeclarationSlot -> CachePut
putDeclarationSlotCache (DeclarationSlot owner ordinal) = do
    putModuleNameCache owner
    putCacheNatural (localDeclarationOrdinalValue ordinal)

getDeclarationSlotCache :: CacheGet DeclarationSlot
getDeclarationSlotCache =
    DeclarationSlot
        <$> getModuleNameCache
        <*> (localDeclarationOrdinal <$> getCacheNatural)

putFactSlotCache :: FactSlot -> CachePut
putFactSlotCache (FactSlot owner ordinal) = do
    putModuleNameCache owner
    putCacheNatural (localFactOrdinalValue ordinal)

getFactSlotCache :: CacheGet FactSlot
getFactSlotCache =
    FactSlot
        <$> getModuleNameCache
        <*> (localFactOrdinal <$> getCacheNatural)

putModuleNameCache :: ModuleName -> CachePut
putModuleNameCache owner = do
    putMathematicalDigestCache
        (sourceNamespaceDigest
            (moduleNameNamespace owner))
    putCacheText
        (Text.pack
            (safeRelativePathFilePath
                (moduleNameRelativePath owner)))

getModuleNameCache :: CacheGet ModuleName
getModuleNameCache = do
    namespace <-
        sourceNamespaceIdFromDigest
            <$> getMathematicalDigestCache
    rawPath <- Text.unpack <$> getCacheText
    relative <-
        either
            (fail . ("invalid cache module path: " <>) . show)
            pure
            (safeRelativePath rawPath)
    pure (moduleNameFromParts namespace relative)

putSemanticAliasCache :: SemanticAlias -> CachePut
putSemanticAliasCache (SemanticAlias name target) = do
    putSemanticNameCache name
    putSemanticFactOccurrenceFingerprintCache target

getSemanticAliasCache :: CacheGet SemanticAlias
getSemanticAliasCache =
    SemanticAlias
        <$> getSemanticNameCache
        <*> getSemanticFactOccurrenceFingerprintCache

putSemanticNameCache :: SemanticName -> CachePut
putSemanticNameCache (SemanticName name) =
    putCacheText name

getSemanticNameCache :: CacheGet SemanticName
getSemanticNameCache =
    SemanticName <$> getCacheText

putEligibility :: FactSearchEligibility -> CachePut
putEligibility = \case
    SearchEligible -> putCacheTag 0x00
    SearchIneligible -> putCacheTag 0x01

getEligibility :: CacheGet FactSearchEligibility
getEligibility =
    getCacheTag >>= \case
        0x00 -> pure SearchEligible
        0x01 -> pure SearchIneligible
        tag ->
            fail ("unknown fact-search eligibility tag " <> show tag)

putModuleArtifactKeyFields :: ModuleArtifactKey -> CachePut
putModuleArtifactKeyFields
        (ModuleArtifactKey owner parsed direct theory) = do
    putModuleNameCache owner
    putParsedModuleIdCache parsed
    putCacheList putSemanticInterfaceIdCache direct
    putTheoryIdCache theory

putProofValidationKeyCache :: ProofValidationKey -> CachePut
putProofValidationKeyCache (ProofValidationKey digest) =
    putCacheDigest digest

getProofValidationKeyCache :: CacheGet ProofValidationKey
getProofValidationKeyCache =
    ProofValidationKey <$> getCacheDigest

putDeclarationValidationKeyCache
    :: DeclarationValidationKey
    -> CachePut
putDeclarationValidationKeyCache
        (DeclarationValidationKey digest) =
    putCacheDigest digest

getDeclarationValidationKeyCache
    :: CacheGet DeclarationValidationKey
getDeclarationValidationKeyCache =
    DeclarationValidationKey <$> getCacheDigest

firstDuplicate :: Ord value => [value] -> Maybe value
firstDuplicate =
    go Set.empty
  where
    go _ [] =
        Nothing
    go seen (value : rest)
        | value `Set.member` seen =
            Just value
        | otherwise =
            go (Set.insert value seen) rest

rejectDuplicate
    :: Ord value
    => (value -> error)
    -> [value]
    -> Either error ()
rejectDuplicate makeError values =
    maybe
        (Right ())
        (Left . makeError)
        (firstDuplicate values)

strictlyIncreasing :: Ord value => [value] -> Bool
strictlyIncreasing values =
    and
        (zipWith (<) values (drop 1 values))