Migrate to `Felix` namespaceHEADhotg

1 files changed, 0 insertions, 1759 deletions

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