Separate epoch cache encoding

1 files changed, 109 insertions, 0 deletions

diff --git a/source/Checking/Identity.hs b/source/Checking/Identity.hs
index d2c48fc..d152f88 100644
--- a/source/Checking/Identity.hs
+++ b/source/Checking/Identity.hs
@@ -50,11 +50,22 @@ module Checking.Identity
     , 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
 
@@ -780,6 +791,104 @@ 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 ->