Centralize checked set constructions

1 files changed, 15 insertions, 72 deletions

diff --git a/source/Checking/Declaration.hs b/source/Checking/Declaration.hs
index ee795f0..b114954 100644
--- a/source/Checking/Declaration.hs
+++ b/source/Checking/Declaration.hs
@@ -175,13 +175,9 @@ import Checking.Identity
 import Checking.Kernel.Derivation
 import Checking.Semantic
 import Checking.Materialization qualified as Materialization
+import Checking.SetConstruction
 import Felix.Cache.Codec
-    ( CacheDigest
-    , encodeCache
-    , hashCacheFields
-    , putCanonicalTermCache
-    , putCoreTypeCache
-    )
+    ( encodeCache )
 import Felix.Module
 import Provers qualified
 import Report.Location
@@ -2186,71 +2182,27 @@ prepareNamedSetConstruction
         DeclarationError
         (FrozenCheckedCore ObjectId, KernelConstructionDescriptor)
 prepareNamedSetConstruction foundation closure identity construction = do
-    let expectedContent = namedSetConstructionClosedTerm construction
+    let expectedContent = namedSetConstructionClosedBody construction
     case lookupCheckedObjectContent identity closure of
         Just (TransparentObjectContent _theory coreType body)
             | coreType == frozenCoreType expectedContent
             , body == frozenCoreTerm expectedContent -> pure ()
         _ -> Left KernelConstructionDescriptorMismatch
-    proposition <-
+    derived <-
         maybe
             (Left KernelConstructionDescriptorMismatch)
             Right
-            (namedSetConstructionObjectView
-                (constructionCharacteristic foundation)
+            (namedSetConstructionObjectFact
+                (checkedFoundationSetConstruction foundation)
                 identity
                 construction)
-    descriptorId <-
-        namedSetConstructionDescriptorId foundation construction
     pure
-        ( proposition
-        , CheckedSetConstructionExtensionality identity descriptorId
+        ( namedSetConstructionFactProposition derived
+        , CheckedSetConstructionExtensionality
+            identity
+            (namedSetConstructionFactDescriptor derived)
         )
 
-namedSetConstructionDescriptorId
-    :: CheckedFoundation
-    -> NamedSetConstruction ObjectId
-    -> Either DeclarationError CacheDigest
-namedSetConstructionDescriptorId foundation construction = do
-    selfView <-
-        maybe
-            (Left KernelConstructionDescriptorMismatch)
-            Right
-            (namedSetConstructionClosedSelfView
-                (constructionCharacteristic foundation)
-                construction)
-    let closedTerm = namedSetConstructionClosedTerm construction
-    pure
-        (hashCacheFields
-            "felix-checked-named-set-construction-v1"
-            [ encodeCache do
-                putCoreTypeCache (frozenCoreType closedTerm)
-                putCanonicalTermCache putObjectIdCache
-                    (frozenCoreTerm closedTerm)
-            , encodeCache do
-                putCanonicalTermCache putObjectIdCache
-                    (frozenCoreTerm selfView)
-            ])
-
-constructionCharacteristic
-    :: CheckedFoundation
-    -> CoreIntrinsicTag
-    -> Maybe (FrozenCheckedCore Void)
-constructionCharacteristic foundation = \case
-    FamilyUnion ->
-        Just
-            (foundationAxiomFrozen
-                foundation FamilyUnionCharacteristic)
-    Sep ->
-        Just
-            (foundationAxiomFrozen
-                foundation SeparationCharacteristic)
-    Repl ->
-        Just
-            (foundationAxiomFrozen
-                foundation ReplacementCharacteristic)
-    _ -> Nothing
-
 preparePointwiseDefinitionEquationSpec
     :: CheckedObjectClosure
     -> ObjectId
@@ -3770,25 +3722,16 @@ authorizeNamedSetConstructionCandidate
 authorizeNamedSetConstructionCandidate identity construction candidate =
     authorizeOneCandidate candidate \initial -> do
         let builder = candidateProofBuilder initial
-        expectedDescriptor <-
+        (expected, descriptor) <-
             Except.liftEither
-                (namedSetConstructionDescriptorId
+                (prepareNamedSetConstruction
                     (logicalBuilderFoundation builder)
+                    (candidateProofObjectClosure initial)
+                    identity
                     construction)
-        let descriptor =
-                CheckedSetConstructionExtensionality
-                    identity expectedDescriptor
         when (isNothing (candidateProofCachedValidation initial)) do
-            (expected, preparedDescriptor) <-
-                Except.liftEither
-                    (prepareNamedSetConstruction
-                        (logicalBuilderFoundation builder)
-                        (candidateProofObjectClosure initial)
-                        identity
-                        construction)
             unless
-                ( preparedDescriptor == descriptor
-                  && frozenCoreTerm expected
+                (frozenCoreTerm expected
                         == frozenCoreTerm
                             (checkedPropositionTerm
                                 (candidateCheckedProposition candidate))