diff options
Diffstat (limited to 'source/Checking/Identity.hs')
| -rw-r--r-- | source/Checking/Identity.hs | 1023 |
1 files changed, 0 insertions, 1023 deletions
diff --git a/source/Checking/Identity.hs b/source/Checking/Identity.hs deleted file mode 100644 index fe846dc..0000000 --- a/source/Checking/Identity.hs +++ /dev/null @@ -1,1023 +0,0 @@ -{-# LANGUAGE DeriveAnyClass #-} -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE NoImplicitPrelude #-} - --- | Content-addressed identities for checked mathematical content. -module Checking.Identity - ( TheoryId - , theoryId - , theoryIdDigest - , encodeFoundationManifest - , foundationManifestTags - , encodeKernelRuleTag - , ObjectFamily(..) - , ObjectId - , objectId - , objectIdFamily - , objectIdDigest - , encodeObjectId - , OpaqueDeclarationSeed - , opaqueDeclarationSeed - , opaqueDeclarationSeedDigest - , ObjectContent(..) - , objectContentTheory - , objectContentType - , intrinsicObjectId - , transparentObjectId - , opaqueObjectId - , AssertedObject - , assertedObject - , assertedObjectId - , assertedObjectContent - , CheckedObjectClosure - , checkedObjectClosureTheory - , checkedObjectIds - , lookupCheckedObjectType - , lookupCheckedObjectContent - , validateObjectClosure - , extendObjectClosure - , ObjectValidationError(..) - , PropositionId - , propositionIdDigest - , CheckedPropositionContent - , checkedPropositionId - , checkedPropositionTerm - , validatePropositionContent - , validateAssertedPropositionContent - , propositionIdOf - , PropositionValidationError(..) - , TheoremRef - , theoremRef - , theoremRefTheory - , theoremRefProposition - , encodeTheoremRef - , TheoremId - , theoremId - , theoremIdDigest - , putTheoryIdCache - , getTheoryIdCache - , putObjectIdCache - , getObjectIdCache - , putObjectContentCache - , getObjectContentCache - , putPropositionIdCache - , getPropositionIdCache - , putTheoremRefCache - , getTheoremRefCache - ) where - -import Base -import Checking.Core -import Checking.Foundation -import Felix.Cache.Codec -import Felix.Math.Codec -import Felix.Module - -import Control.DeepSeq (NFData) -import Control.Monad.State.Strict -import Data.Bifunctor (first) -import Data.ByteString (ByteString) -import Data.ByteString qualified as ByteString -import Data.List qualified as List -import Data.Map.Strict qualified as Map -import Data.Set qualified as Set -import Data.Word (Word8) - - -newtype TheoryId = - TheoryId MathematicalDigest - deriving stock (Show, Eq, Ord, Generic) - deriving newtype (Hashable, NFData) - -theoryId :: CheckedFoundation -> TheoryId -theoryId foundation = - TheoryId - (codecInvariant - (hashCanonicalFields - "felix-theory" - [encodeFoundationManifest foundation])) - -theoryIdDigest :: TheoryId -> MathematicalDigest -theoryIdDigest (TheoryId digest) = - digest - --- | Canonical ordered intrinsic/rule/axiom manifest. Backend classification is --- intentionally absent. -encodeFoundationManifest :: CheckedFoundation -> ByteString -encodeFoundationManifest foundation = - codecInvariant - (encodeSequence - [ codecInvariant (encodeSequence intrinsicRows) - , codecInvariant (encodeSequence ruleRows) - , codecInvariant (encodeSequence axiomRows) - ]) - where - (intrinsicTags, ruleTags, axiomTags) = - foundationManifestTags - - intrinsicRows = - [ encodeCoreIntrinsicTag tag - <> encodeFrame (encodeCoreType (coreIntrinsicType tag)) - | tag <- intrinsicTags - ] - - ruleRows = - [ encodeKernelRuleTag tag - <> encodeFrame - (codecInvariant - (encodeSequence - (encodeCoreType <$> inputTypes))) - <> encodeFrame (encodeNatural binderCount) - | tag <- ruleTags - , let KernelRuleSignature inputTypes binderCount = - foundationRuleSignature foundation tag - ] - - axiomRows = - [ encodeFoundationAxiomTag tag - <> encodeFrame - (encodeCanonicalTerm - absurd - (frozenCoreTerm - (foundationAxiomFrozen foundation tag))) - | tag <- axiomTags - ] - --- | Exhaustive foundation inventories in their stable encoded-tag order. -foundationManifestTags - :: ( [CoreIntrinsicTag] - , [KernelRuleTag] - , [FoundationAxiomTag] - ) -foundationManifestTags = - ( stableTagOrder - "core intrinsic" - encodeCoreIntrinsicTag - allCoreIntrinsicTags - , stableTagOrder - "kernel rule" - encodeKernelRuleTag - allKernelRuleTags - , stableTagOrder - "foundation axiom" - encodeFoundationAxiomTag - allFoundationAxiomTags - ) - - -data ObjectFamily - = IntrinsicObject - | TransparentObject - | OpaqueObject - deriving stock (Show, Eq, Ord, Enum, Bounded, Generic) - deriving anyclass (NFData) - -data ObjectId = ObjectId - !ObjectFamily - !MathematicalDigest - deriving stock (Show, Eq, Ord, Generic) - deriving anyclass (NFData) - -objectId - :: ObjectFamily - -> MathematicalDigest - -> ObjectId -objectId = - ObjectId - -objectIdFamily :: ObjectId -> ObjectFamily -objectIdFamily (ObjectId family _digest) = - family - -objectIdDigest :: ObjectId -> MathematicalDigest -objectIdDigest (ObjectId _family digest) = - digest - -encodeObjectId :: ObjectId -> ByteString -encodeObjectId (ObjectId family digest) = - ByteString.singleton (objectFamilyTag family) - <> mathematicalDigestBytes digest - - -newtype OpaqueDeclarationSeed = - OpaqueDeclarationSeed MathematicalDigest - deriving stock (Show, Eq, Ord, Generic) - deriving newtype (Hashable, NFData) - -opaqueDeclarationSeed - :: ModuleName - -> LocalDeclarationOrdinal - -> DeclarationFamilyTag - -> GeneratedObjectSlot - -> OpaqueDeclarationSeed -opaqueDeclarationSeed - owner - declarationOrdinal - family - generatedSlot = - OpaqueDeclarationSeed - (codecInvariant - (hashCanonicalFields - "felix-opaque-declaration-v1" - [ encodeModuleName owner - , encodeNatural - (localDeclarationOrdinalValue - declarationOrdinal) - , encodeDeclarationFamilyTag family - , encodeNatural - (generatedObjectSlotValue - generatedSlot) - ])) - -opaqueDeclarationSeedDigest - :: OpaqueDeclarationSeed - -> MathematicalDigest -opaqueDeclarationSeedDigest - (OpaqueDeclarationSeed digest) = - digest - - -data ObjectContent - = IntrinsicObjectContent - !TheoryId - !CoreIntrinsicTag - !CoreType - | TransparentObjectContent - !TheoryId - !CoreType - !(CanonicalTerm ObjectId) - | OpaqueObjectContent - !TheoryId - !OpaqueDeclarationSeed - !CoreType - deriving stock (Show, Eq, Ord, Generic) - deriving anyclass (NFData) - -objectContentTheory :: ObjectContent -> TheoryId -objectContentTheory = \case - IntrinsicObjectContent identity _tag _coreType -> - identity - TransparentObjectContent identity _coreType _body -> - identity - OpaqueObjectContent identity _seed _coreType -> - identity - -objectContentType :: ObjectContent -> CoreType -objectContentType = \case - IntrinsicObjectContent _identity _tag coreType -> - coreType - TransparentObjectContent _identity coreType _body -> - coreType - OpaqueObjectContent _identity _seed coreType -> - coreType - -intrinsicObjectId - :: TheoryId - -> CoreIntrinsicTag - -> CoreType - -> ObjectId -intrinsicObjectId identity tag coreType = - ObjectId - IntrinsicObject - (codecInvariant - (hashCanonicalFields - "felix-intrinsic-object-v1" - [ mathematicalDigestBytes - (theoryIdDigest identity) - , encodeCoreIntrinsicTag tag - , encodeCoreType coreType - ])) - -transparentObjectId - :: TheoryId - -> CoreType - -> CanonicalTerm ObjectId - -> ObjectId -transparentObjectId identity coreType body = - ObjectId - TransparentObject - (codecInvariant - (hashCanonicalFields - "felix-transparent-object-v1" - [ mathematicalDigestBytes - (theoryIdDigest identity) - , encodeCoreType coreType - , encodeCanonicalTerm encodeObjectId body - ])) - -opaqueObjectId - :: TheoryId - -> OpaqueDeclarationSeed - -> CoreType - -> ObjectId -opaqueObjectId identity seed coreType = - ObjectId - OpaqueObject - (codecInvariant - (hashCanonicalFields - "felix-opaque-object-v1" - [ mathematicalDigestBytes - (theoryIdDigest identity) - , mathematicalDigestBytes - (opaqueDeclarationSeedDigest seed) - , encodeCoreType coreType - ])) - - -data AssertedObject = AssertedObject - !ObjectId - !ObjectContent - deriving stock (Show, Eq, Ord, Generic) - deriving anyclass (NFData) - -assertedObject :: ObjectId -> ObjectContent -> AssertedObject -assertedObject = - AssertedObject - -assertedObjectId :: AssertedObject -> ObjectId -assertedObjectId (AssertedObject identity _content) = - identity - -assertedObjectContent :: AssertedObject -> ObjectContent -assertedObjectContent (AssertedObject _identity content) = - content - -data CheckedObject = CheckedObject - !ObjectContent - !CoreType - -data CheckedObjectClosure = CheckedObjectClosure - !TheoryId - !(Map ObjectId CheckedObject) - -checkedObjectClosureTheory :: CheckedObjectClosure -> TheoryId -checkedObjectClosureTheory (CheckedObjectClosure identity _objects) = - identity - -checkedObjectIds :: CheckedObjectClosure -> Set ObjectId -checkedObjectIds (CheckedObjectClosure _identity objects) = - Map.keysSet objects - -lookupCheckedObjectType - :: ObjectId - -> CheckedObjectClosure - -> Maybe CoreType -lookupCheckedObjectType identity - (CheckedObjectClosure _theory objects) = - checkedObjectType - <$> Map.lookup identity objects - -lookupCheckedObjectContent - :: ObjectId - -> CheckedObjectClosure - -> Maybe ObjectContent -lookupCheckedObjectContent identity - (CheckedObjectClosure _theory objects) = - checkedObjectContent - <$> Map.lookup identity objects - -checkedObjectType :: CheckedObject -> CoreType -checkedObjectType (CheckedObject _content coreType) = - coreType - -checkedObjectContent :: CheckedObject -> ObjectContent -checkedObjectContent (CheckedObject content _coreType) = - content - - -data ObjectValidationError - = DuplicateAssertedObjectId !ObjectId - | ObjectContentTheoryMismatch - !ObjectId - !TheoryId - !TheoryId - | ObjectContentFamilyMismatch - !ObjectId - !ObjectFamily - !ObjectFamily - | IntrinsicObjectTypeMismatch - !ObjectId - !CoreIntrinsicTag - !CoreType - !CoreType - | TransparentObjectReferenceMissing - !ObjectId - !ObjectId - | TransparentObjectCycle !(NonEmpty ObjectId) - | TransparentObjectCoreCheckError - !ObjectId - !CoreCheckError - | TransparentObjectTypeMismatch - !ObjectId - !CoreType - !CoreType - | ObjectIdPayloadMismatch - !ObjectId - !ObjectId - deriving stock (Show, Eq) - -data ObjectValidationState = ObjectValidationState - { validationStack :: ![ObjectId] - , validatedObjects :: !(Map ObjectId CheckedObject) - } - -validateObjectClosure - :: TheoryId - -> [AssertedObject] - -> Either ObjectValidationError CheckedObjectClosure -validateObjectClosure expectedTheory asserted = do - inventory <- buildObjectInventory asserted - finalState <- - execStateT - (traverse_ (validateOneObject expectedTheory inventory) - (Map.keys inventory)) - (ObjectValidationState [] Map.empty) - pure - (CheckedObjectClosure - expectedTheory - (validatedObjects finalState)) - --- | Validate one declaration's new objects against an already checked --- closure. The existing closure is returned unchanged for an empty batch. -extendObjectClosure - :: CheckedObjectClosure - -> [AssertedObject] - -> Either ObjectValidationError CheckedObjectClosure -extendObjectClosure closure [] = - Right closure -extendObjectClosure - (CheckedObjectClosure expectedTheory existing) - asserted = do - additions <- buildObjectInventory asserted - traverse_ - (\identity -> - when - (Map.member identity existing) - (Left (DuplicateAssertedObjectId identity))) - (Map.keys additions) - let existingInventory = - checkedObjectContent <$> existing - inventory = - Map.union additions existingInventory - finalState <- - execStateT - (traverse_ - (validateOneObject expectedTheory inventory) - (Map.keys additions)) - (ObjectValidationState [] existing) - pure - (CheckedObjectClosure - expectedTheory - (validatedObjects finalState)) - -buildObjectInventory - :: [AssertedObject] - -> Either ObjectValidationError (Map ObjectId ObjectContent) -buildObjectInventory = - foldM insertOne Map.empty - where - insertOne inventory (AssertedObject identity content) - | Map.member identity inventory = - Left (DuplicateAssertedObjectId identity) - | otherwise = - Right (Map.insert identity content inventory) - -validateOneObject - :: TheoryId - -> Map ObjectId ObjectContent - -> ObjectId - -> StateT - ObjectValidationState - (Either ObjectValidationError) - () -validateOneObject expectedTheory inventory identity = do - alreadyValidated <- - gets (Map.member identity . validatedObjects) - unless alreadyValidated do - stack <- gets validationStack - when (identity `elem` stack) do - lift - (Left - (TransparentObjectCycle - (cyclePath identity stack))) - content <- - case Map.lookup identity inventory of - Nothing -> - impossible - "object validation root is absent from its inventory" - Just found -> - pure found - unless - (objectContentTheory content == expectedTheory) - (lift - (Left - (ObjectContentTheoryMismatch - identity - expectedTheory - (objectContentTheory content)))) - let expectedFamily = - objectContentFamily content - suppliedFamily = - objectIdFamily identity - unless - (suppliedFamily == expectedFamily) - (lift - (Left - (ObjectContentFamilyMismatch - identity - expectedFamily - suppliedFamily))) - modify' - (\validationState -> - validationState - { validationStack = - identity - : validationStack validationState - }) - checked <- case content of - IntrinsicObjectContent - theory - tag - suppliedType -> do - let expectedType = - coreIntrinsicType tag - unless - (suppliedType == expectedType) - (lift - (Left - (IntrinsicObjectTypeMismatch - identity - tag - expectedType - suppliedType))) - verifyObjectId - identity - (intrinsicObjectId - theory - tag - suppliedType) - pure - (CheckedObject content suppliedType) - TransparentObjectContent - theory - suppliedType - body -> do - traverse_ - (validateDependency expectedTheory inventory identity) - (Set.toAscList (canonicalTermGlobals body)) - resolvedObjects <- - gets validatedObjects - checkedBody <- - lift - (first - (TransparentObjectCoreCheckError - identity) - (checkCanonicalCore - (\reference -> - checkedObjectType - <$> Map.lookup - reference - resolvedObjects) - body)) - let inferredType = - frozenCoreType checkedBody - unless - (inferredType == suppliedType) - (lift - (Left - (TransparentObjectTypeMismatch - identity - suppliedType - inferredType))) - verifyObjectId - identity - (transparentObjectId - theory - suppliedType - body) - pure - (CheckedObject content suppliedType) - OpaqueObjectContent - theory - seed - suppliedType -> do - verifyObjectId - identity - (opaqueObjectId - theory - seed - suppliedType) - pure - (CheckedObject content suppliedType) - modify' - (\validationState -> - validationState - { validationStack = - dropCurrent - identity - (validationStack validationState) - , validatedObjects = - Map.insert - identity - checked - (validatedObjects validationState) - }) - where - verifyObjectId supplied computed = - unless - (supplied == computed) - (lift - (Left - (ObjectIdPayloadMismatch - supplied - computed))) - -validateDependency - :: TheoryId - -> Map ObjectId ObjectContent - -> ObjectId - -> ObjectId - -> StateT - ObjectValidationState - (Either ObjectValidationError) - () -validateDependency expectedTheory inventory parent dependency = - case Map.lookup dependency inventory of - Nothing -> - lift - (Left - (TransparentObjectReferenceMissing - parent - dependency)) - Just _ -> - validateOneObject - expectedTheory - inventory - dependency - -cyclePath :: ObjectId -> [ObjectId] -> NonEmpty ObjectId -cyclePath repeated stack = - case break (== repeated) stack of - (between, _repeated : _outer) -> - repeated :| (reverse between <> [repeated]) - _ -> - impossible "repeated object is absent from validation stack" - -dropCurrent :: ObjectId -> [ObjectId] -> [ObjectId] -dropCurrent expected = \case - current : rest - | current == expected -> - rest - _ -> - impossible "object validation stack is inconsistent" - -objectContentFamily :: ObjectContent -> ObjectFamily -objectContentFamily = \case - IntrinsicObjectContent{} -> - IntrinsicObject - TransparentObjectContent{} -> - TransparentObject - OpaqueObjectContent{} -> - OpaqueObject - -newtype PropositionId = - PropositionId MathematicalDigest - deriving stock (Show, Eq, Ord, Generic) - deriving newtype (Hashable, NFData) - -propositionIdDigest :: PropositionId -> MathematicalDigest -propositionIdDigest (PropositionId digest) = - digest - -data CheckedPropositionContent = CheckedPropositionContent - !PropositionId - !(FrozenCheckedCore ObjectId) - deriving stock (Generic) - deriving anyclass (NFData) - -checkedPropositionId - :: CheckedPropositionContent - -> PropositionId -checkedPropositionId - (CheckedPropositionContent identity _term) = - identity - -checkedPropositionTerm - :: CheckedPropositionContent - -> FrozenCheckedCore ObjectId -checkedPropositionTerm - (CheckedPropositionContent _identity term) = - term - -data PropositionValidationError - = PropositionObjectMissing !ObjectId - | PropositionCoreCheckError !CoreCheckError - | PropositionIsNotProp !CoreType - | PropositionIdPayloadMismatch - !PropositionId - !PropositionId - deriving stock (Show, Eq) - -validatePropositionContent - :: CheckedObjectClosure - -> CanonicalTerm ObjectId - -> Either - PropositionValidationError - CheckedPropositionContent -validatePropositionContent closure term = do - traverse_ - (\identity -> - unless - (isJust - (lookupCheckedObjectType identity closure)) - (Left (PropositionObjectMissing identity))) - (Set.toAscList (canonicalTermGlobals term)) - checked <- - first PropositionCoreCheckError - (checkCanonicalCore - (\identity -> - lookupCheckedObjectType identity closure) - term) - unless - (frozenCoreType checked == TyProp) - (Left - (PropositionIsNotProp - (frozenCoreType checked))) - let identity = - propositionIdOf term - pure - (CheckedPropositionContent - identity - checked) - -validateAssertedPropositionContent - :: CheckedObjectClosure - -> PropositionId - -> CanonicalTerm ObjectId - -> Either - PropositionValidationError - CheckedPropositionContent -validateAssertedPropositionContent closure supplied term = do - checked <- - validatePropositionContent closure term - let computed = - checkedPropositionId checked - unless - (supplied == computed) - (Left - (PropositionIdPayloadMismatch - supplied - computed)) - pure checked - -propositionIdOf - :: CanonicalTerm ObjectId - -> PropositionId -propositionIdOf term = - PropositionId - (codecInvariant - (hashCanonicalFields - "felix-proposition-v1" - [encodeCanonicalTerm encodeObjectId term])) - - -data TheoremRef = TheoremRef - !TheoryId - !PropositionId - deriving stock (Show, Eq, Ord, Generic) - deriving anyclass (NFData) - -theoremRef :: TheoryId -> PropositionId -> TheoremRef -theoremRef = - TheoremRef - -theoremRefTheory :: TheoremRef -> TheoryId -theoremRefTheory (TheoremRef identity _proposition) = - identity - -theoremRefProposition :: TheoremRef -> PropositionId -theoremRefProposition (TheoremRef _identity proposition) = - proposition - -encodeTheoremRef :: TheoremRef -> ByteString -encodeTheoremRef (TheoremRef identity proposition) = - encodeFrame - (mathematicalDigestBytes - (theoryIdDigest identity)) - <> encodeFrame - (mathematicalDigestBytes - (propositionIdDigest proposition)) - -newtype TheoremId = - TheoremId MathematicalDigest - deriving stock (Show, Eq, Ord, Generic) - deriving newtype (Hashable, NFData) - -theoremId :: TheoremRef -> TheoremId -theoremId reference = - TheoremId - (codecInvariant - (hashCanonicalFields - "felix-theorem" - [encodeTheoremRef reference])) - -theoremIdDigest :: TheoremId -> MathematicalDigest -theoremIdDigest (TheoremId digest) = - digest - - -putTheoryIdCache :: TheoryId -> CachePut -putTheoryIdCache = - putMathematicalDigestCache . theoryIdDigest - -getTheoryIdCache :: CacheGet TheoryId -getTheoryIdCache = - TheoryId <$> getMathematicalDigestCache - -putObjectIdCache :: ObjectId -> CachePut -putObjectIdCache (ObjectId family digest) = do - putCacheTag (objectFamilyTag family) - putMathematicalDigestCache digest - -getObjectIdCache :: CacheGet ObjectId -getObjectIdCache = do - family <- getCacheTag >>= \case - 0x00 -> - pure IntrinsicObject - 0x01 -> - pure TransparentObject - 0x02 -> - pure OpaqueObject - tag -> - fail ("unknown cache object-family tag " <> show tag) - ObjectId family <$> getMathematicalDigestCache - -putOpaqueDeclarationSeedCache - :: OpaqueDeclarationSeed - -> CachePut -putOpaqueDeclarationSeedCache = - putMathematicalDigestCache - . opaqueDeclarationSeedDigest - -getOpaqueDeclarationSeedCache - :: CacheGet OpaqueDeclarationSeed -getOpaqueDeclarationSeedCache = - OpaqueDeclarationSeed - <$> getMathematicalDigestCache - -putObjectContentCache :: ObjectContent -> CachePut -putObjectContentCache = \case - IntrinsicObjectContent identity tag coreType -> do - putCacheTag 0x00 - putTheoryIdCache identity - putCoreIntrinsicTagCache tag - putCoreTypeCache coreType - TransparentObjectContent identity coreType body -> do - putCacheTag 0x01 - putTheoryIdCache identity - putCoreTypeCache coreType - putCanonicalTermCache putObjectIdCache body - OpaqueObjectContent identity seed coreType -> do - putCacheTag 0x02 - putTheoryIdCache identity - putOpaqueDeclarationSeedCache seed - putCoreTypeCache coreType - -getObjectContentCache :: CacheGet ObjectContent -getObjectContentCache = - getCacheTag >>= \case - 0x00 -> - IntrinsicObjectContent - <$> getTheoryIdCache - <*> getCoreIntrinsicTagCache - <*> getCoreTypeCache - 0x01 -> - TransparentObjectContent - <$> getTheoryIdCache - <*> getCoreTypeCache - <*> getCanonicalTermCache getObjectIdCache - 0x02 -> - OpaqueObjectContent - <$> getTheoryIdCache - <*> getOpaqueDeclarationSeedCache - <*> getCoreTypeCache - tag -> - fail ("unknown cache object-content tag " <> show tag) - -putPropositionIdCache :: PropositionId -> CachePut -putPropositionIdCache = - putMathematicalDigestCache . propositionIdDigest - -getPropositionIdCache :: CacheGet PropositionId -getPropositionIdCache = - PropositionId <$> getMathematicalDigestCache - -putTheoremRefCache :: TheoremRef -> CachePut -putTheoremRefCache (TheoremRef identity proposition) = do - putTheoryIdCache identity - putPropositionIdCache proposition - -getTheoremRefCache :: CacheGet TheoremRef -getTheoremRefCache = - TheoremRef - <$> getTheoryIdCache - <*> getPropositionIdCache - - -objectFamilyTag :: ObjectFamily -> Word8 -objectFamilyTag = \case - IntrinsicObject -> - 0x00 - TransparentObject -> - 0x01 - OpaqueObject -> - 0x02 - -encodeKernelRuleTag :: KernelRuleTag -> ByteString -encodeKernelRuleTag = - ByteString.singleton . \case - SetLfpBound -> - 0x00 - SetLfpLeast -> - 0x01 - SetLfpFixed -> - 0x02 - SetLfpInduct -> - 0x03 - -encodeFoundationAxiomTag :: FoundationAxiomTag -> ByteString -encodeFoundationAxiomTag = - ByteString.singleton . \case - EmptyCharacteristic -> - 0x00 - PairSetCharacteristic -> - 0x01 - FamilyUnionCharacteristic -> - 0x02 - PowerSetCharacteristic -> - 0x03 - SeparationCharacteristic -> - 0x04 - ReplacementCharacteristic -> - 0x05 - SetChooseWitness -> - 0x06 - SetExtensionality -> - 0x07 - SetInduction -> - 0x08 - PropositionalExtensionality -> - 0x09 - DoubleNegationElim -> - 0x0a - UnivOfContains -> - 0x0b - UnivOfTransitive -> - 0x0c - UnivOfFamilyUnionClosed -> - 0x0d - UnivOfPowerSetClosed -> - 0x0e - UnivOfReplacementClosed -> - 0x0f - UnivOfMinimal -> - 0x10 - -allCoreIntrinsicTags :: [CoreIntrinsicTag] -allCoreIntrinsicTags = - [minBound .. maxBound] - -allKernelRuleTags :: [KernelRuleTag] -allKernelRuleTags = - [minBound .. maxBound] - -allFoundationAxiomTags :: [FoundationAxiomTag] -allFoundationAxiomTags = - [minBound .. maxBound] - -stableTagOrder - :: Show tag - => String - -> (tag -> ByteString) - -> [tag] - -> [tag] -stableTagOrder description encodeTag tags - | Set.size encodedTags == length tags = - List.sortOn encodeTag tags - | otherwise = - impossible - ("duplicate stable " - <> description - <> " tag in " - <> show tags) - where - encodedTags = - Set.fromList (encodeTag <$> tags) - -codecInvariant - :: Either MathematicalCodecError value - -> value -codecInvariant = - either - (impossible . ("canonical codec invariant: " <>) . show) - id |