Keep datatype compilation authority inert

2 files changed, 0 insertions, 106 deletions

diff --git a/source/Checking/Authority.hs b/source/Checking/Authority.hs
index aadcddf..1bfcc78 100644
--- a/source/Checking/Authority.hs
+++ b/source/Checking/Authority.hs
@@ -25,9 +25,6 @@ module Checking.Authority
     , KernelConstructionDescriptor(..)
     , DatatypeCompilationDescriptor
     , datatypeCompilationDescriptor
-    , datatypeCompilationCarrier
-    , datatypeCompilationConstructors
-    , datatypeCompilationFacts
     , CompilationDescriptor(..)
     , DirectAuthorization(..)
     , ValidationCertificate
@@ -204,27 +201,6 @@ datatypeCompilationDescriptor
 datatypeCompilationDescriptor =
     DatatypeCompilationDescriptor
 
-datatypeCompilationCarrier
-    :: DatatypeCompilationDescriptor
-    -> ObjectId
-datatypeCompilationCarrier
-        (DatatypeCompilationDescriptor carrier _constructors _facts) =
-    carrier
-
-datatypeCompilationConstructors
-    :: DatatypeCompilationDescriptor
-    -> NonEmpty ObjectId
-datatypeCompilationConstructors
-        (DatatypeCompilationDescriptor _carrier constructors _facts) =
-    constructors
-
-datatypeCompilationFacts
-    :: DatatypeCompilationDescriptor
-    -> [TheoremRef]
-datatypeCompilationFacts
-        (DatatypeCompilationDescriptor _carrier _constructors facts) =
-    facts
-
 data CompilationDescriptor
     = DatatypeCompilation !DatatypeCompilationDescriptor
     deriving stock (Show, Eq, Ord, Generic)
diff --git a/source/Checking/Declaration.hs b/source/Checking/Declaration.hs
index 2c59a96..25e7745 100644
--- a/source/Checking/Declaration.hs
+++ b/source/Checking/Declaration.hs
@@ -31,7 +31,6 @@ module Checking.Declaration
     , authorizeVampireCandidate
     , authorizeSourceAxiomCandidate
     , authorizeOmittedCandidate
-    , authorizeDatatypeCompilation
     , commitProofDeclaration
     , commitCompiledDeclaration
     , CommittedDeclarationBatch
@@ -774,83 +773,6 @@ authorizeVampireCandidate candidate prepared accepted =
             (candidateProofSafety final)
             final
 
--- | Admit exactly the object and theorem inventory emitted by one trusted
--- datatype compilation. Members of the generated batch share one stage and
--- cannot authorize one another.
-authorizeDatatypeCompilation
-    :: DatatypeCompilationDescriptor
-    -> NonEmpty ReservedCandidate
-    -> Declaration ()
-authorizeDatatypeCompilation descriptor candidates = Declaration do
-    state <- State.get
-    traverse_ (validateReservedCandidate state) candidates
-    let orderedCandidates =
-            Map.elems (declarationReservations state)
-        stages = Set.fromList (reservedStage <$> toList candidates)
-    unless
-        ( toList candidates == orderedCandidates
-          && Map.null (declarationPending state)
-        )
-        (State.lift
-            (Left CompilationCandidateInventoryMismatch))
-    unless
-        (stages == Set.singleton
-            (CandidateStage
-                (declarationAuthorizationFrontier state)))
-        (State.lift
-            (Left CompilationCandidatesDoNotShareFrontier))
-    closure <- State.lift (declarationClosure state)
-    let requiredObjects =
-            Set.fromList
-                ( datatypeCompilationCarrier descriptor
-                    : toList
-                        (datatypeCompilationConstructors descriptor)
-                )
-        declaredObjects =
-            Set.fromList
-                (assertedObjectId
-                    <$> declarationObjectsReversed state)
-    unless
-        ( requiredObjects == declaredObjects
-          && requiredObjects
-                `Set.isSubsetOf` checkedObjectIds closure
-        )
-        (State.lift
-            (Left CompilationObjectInventoryMismatch))
-    let builder = declarationBuilder state
-        expectedTheorems =
-            candidateTheoremReference builder
-                <$> orderedCandidates
-    unless
-        (datatypeCompilationFacts descriptor == expectedTheorems)
-        (State.lift
-            (Left CompilationFactInventoryMismatch))
-    pending <-
-        traverse
-            (\candidate -> do
-                initial <- State.lift
-                    (initialCandidateProofState state candidate)
-                completion <- State.lift
-                    (freshCompletion
-                        candidate
-                        (TrustedCompilation
-                            (DatatypeCompilation descriptor))
-                        initialCandidateSafety
-                        initial)
-                pure (candidate, completion))
-            orderedCandidates
-    let pendingMap =
-            foldl'
-                (\entries (candidate, completed) ->
-                    Map.insert
-                        (reservedCandidateSlot candidate)
-                        completed
-                        entries)
-                (declarationPending state)
-                pending
-        state' = state{declarationPending = pendingMap}
-    State.put (advanceAuthorizationFrontier state')
-
 freshCompletion
     :: ReservedCandidate
     -> DirectAuthorization
@@ -1774,10 +1696,6 @@ data DeclarationError
     | VampirePremiseCapabilityMismatch
         !SemanticFactOccurrenceFingerprint
     | VampireFoundationMismatch !FoundationAxiomTag
-    | CompilationCandidateInventoryMismatch
-    | CompilationCandidatesDoNotShareFrontier
-    | CompilationObjectInventoryMismatch
-    | CompilationFactInventoryMismatch
     | DeclarationObjectValidationFailed !ObjectValidationError
     | DeclarationPropositionValidationFailed
         !PropositionValidationError