Reuse checked declaration object closures

2 files changed, 91 insertions, 69 deletions

diff --git a/source/Checking/Declaration.hs b/source/Checking/Declaration.hs
index ab7b33c..9b964f8 100644
--- a/source/Checking/Declaration.hs
+++ b/source/Checking/Declaration.hs
@@ -97,7 +97,6 @@ newtype CandidateStage = CandidateStage Natural
 
 data BuilderFactAuthorization = BuilderFactAuthorization
     !BuilderIdentity
-    !PrefixContextId
     !FactSlot
     !FactAuthority
 
@@ -108,7 +107,6 @@ data PendingFactAuthorization = PendingFactAuthorization
     !FactSlot
     !FactAuthority
     !CandidateStage
-    !CandidateStage
 
 data AuthorizedFact = AuthorizedFact
     !CheckedPropositionContent
@@ -121,12 +119,8 @@ data LogicalBuilder = LogicalBuilder
     , logicalBuilderFoundation :: !CheckedFoundation
     , logicalBuilderTheory :: !TheoryId
     , logicalBuilderOwner :: !ModuleName
-    , logicalBuilderDirectInputs :: ![SemanticInterfaceId]
     , logicalBuilderPrefix :: !PrefixContextId
-    , logicalBuilderObjects :: ![AssertedObject]
     , logicalBuilderObjectClosure :: !CheckedObjectClosure
-    , logicalBuilderPropositions
-        :: !(Map PropositionId CheckedPropositionContent)
     , logicalBuilderFacts
         :: !(Map SemanticFactOccurrenceFingerprint AuthorizedFact)
     , logicalBuilderAliases
@@ -373,11 +367,8 @@ runModuleDriver foundation owner direct resolver action = do
                         , logicalBuilderFoundation = foundation
                         , logicalBuilderTheory = theory
                         , logicalBuilderOwner = owner
-                        , logicalBuilderDirectInputs = direct
                         , logicalBuilderPrefix = prefix
-                        , logicalBuilderObjects = []
                         , logicalBuilderObjectClosure = closure
-                        , logicalBuilderPropositions = Map.empty
                         , logicalBuilderFacts = Map.empty
                         , logicalBuilderAliases = Map.empty
                         , logicalBuilderDeltas = []
@@ -486,6 +477,7 @@ data DeclarationState = DeclarationState
     , declarationOwnSlot :: !DeclarationSlot
     , declarationInvocation :: !DeclarationInvocation
     , declarationObjectsReversed :: ![AssertedObject]
+    , declarationObjectClosure :: !(Maybe CheckedObjectClosure)
     , declarationPropositionsReversed
         :: ![CheckedPropositionContent]
     , declarationReservations
@@ -510,14 +502,18 @@ failDeclaration =
     Declaration . State.lift . Except.throwError
 
 addDeclarationObject :: AssertedObject -> Declaration ()
-addDeclarationObject asserted =
-    Declaration
-        (State.modify' \state ->
-            state
-                { declarationObjectsReversed =
-                    asserted
-                        : declarationObjectsReversed state
-                })
+addDeclarationObject asserted = Declaration do
+    state <- State.get
+    when
+        (isJust (declarationObjectClosure state))
+        (State.lift
+            (Except.throwError
+                DeclarationObjectAddedAfterAuthorization))
+    State.put
+        state
+            { declarationObjectsReversed =
+                asserted : declarationObjectsReversed state
+            }
 
 addDeclarationProposition
     :: CheckedPropositionContent
@@ -586,8 +582,8 @@ data CandidatePremise = CandidatePremise
     !CheckedPropositionContent
 
 data CandidateProofState = CandidateProofState
-    { candidateProofBuilder :: !LogicalBuilder
-    , candidateProofDeclaration :: !DeclarationState
+    { candidateProofDeclaration :: !DeclarationState
+    , candidateProofObjectClosure :: !CheckedObjectClosure
     , candidateProofCandidate :: !ReservedCandidate
     , candidateProofPremisesReversed :: ![CandidatePremise]
     , candidateProofPremiseCount :: !Natural
@@ -596,6 +592,10 @@ data CandidateProofState = CandidateProofState
         :: ![PreparedRequestId]
     }
 
+candidateProofBuilder :: CandidateProofState -> LogicalBuilder
+candidateProofBuilder =
+    declarationBuilder . candidateProofDeclaration
+
 newtype CandidateProof value = CandidateProof
     { runCandidateProof
         :: StateT
@@ -880,7 +880,7 @@ freshCompletion candidate direct safety proofState = do
     void
         (first DeclarationPropositionValidationFailed
             (validateAssertedPropositionContent
-                (logicalBuilderObjectClosure builder)
+                (candidateProofObjectClosure proofState)
                 (checkedPropositionId
                     (candidateCheckedProposition candidate))
                 (frozenCoreTerm
@@ -897,8 +897,6 @@ freshCompletion candidate direct safety proofState = do
                 (reservedCandidateSlot candidate)
                 authority
                 (reservedStage candidate)
-                (CandidateStage
-                    (declarationAuthorizationFrontier declaration))
     pure
         (PendingCandidate
             candidate
@@ -911,7 +909,11 @@ authorizeOneCandidate
         -> ExceptT DeclarationError IO PendingCandidate)
     -> Declaration ()
 authorizeOneCandidate candidate complete = Declaration do
-    state <- State.get
+    unprepared <- State.get
+    state <-
+        State.lift
+            (Except.liftEither
+                (prepareDeclarationClosure unprepared))
     State.lift
         (Except.liftEither
             (validateReservedCandidate state candidate))
@@ -975,13 +977,9 @@ initialCandidateProofState
     -> Either DeclarationError CandidateProofState
 initialCandidateProofState declaration candidate = do
     closure <- declarationClosure declaration
-    let builder =
-            (declarationBuilder declaration)
-                { logicalBuilderObjectClosure = closure
-                }
     pure CandidateProofState
-        { candidateProofBuilder = builder
-        , candidateProofDeclaration = declaration
+        { candidateProofDeclaration = declaration
+        , candidateProofObjectClosure = closure
         , candidateProofCandidate = candidate
         , candidateProofPremisesReversed = []
         , candidateProofPremiseCount = 0
@@ -1036,7 +1034,7 @@ useBuilderAuthorizedFact
         state = do
     let builder = candidateProofBuilder state
         BuilderFactAuthorization
-            identity _issuedPrefix slot authority = authorization
+            identity slot authority = authorization
     unless
         ( identity == logicalBuilderIdentity builder
           && slot == semanticFactSlot occurrence
@@ -1063,7 +1061,7 @@ usePendingFact
         declaration = candidateProofDeclaration state
         PendingFactAuthorization
             identity prefix invocation slot authority
-            premiseStageValue frontier = authorization
+            premiseStageValue = authorization
         current = candidateProofCandidate state
     unless
         ( identity == logicalBuilderIdentity builder
@@ -1072,7 +1070,6 @@ usePendingFact
           && slot == reservedCandidateSlot premise
           && authority == validationTarget certificate
           && premiseStageValue == reservedStage premise
-          && frontier <= reservedStage current
         )
         (State.lift
             (Except.throwError PendingFactAuthorizationMismatch))
@@ -1169,7 +1166,7 @@ replayCandidateKernel
 replayCandidateKernel proposition derivation state = do
     imports <- candidateImportJudgments state
     let builder = candidateProofBuilder state
-        closure = logicalBuilderObjectClosure builder
+        closure = candidateProofObjectClosure state
     first KernelCompletionFailed
         (replayKernelDerivation
             (logicalBuilderFoundation builder)
@@ -1219,7 +1216,7 @@ validateKernelConstruction descriptor proposition replayed proofState =
     definingEquation identity =
         case lookupCheckedObjectContent
                 identity
-                (logicalBuilderObjectClosure builder) of
+                (candidateProofObjectClosure proofState) of
             Just
                     (TransparentObjectContent
                         contentTheory coreType body) ->
@@ -1248,7 +1245,7 @@ validatePreparedVampireProblem candidate prepared initial = do
         claim = Backend.typedProblemClaim problem
         target = candidateCheckedProposition candidate
         builder = candidateProofBuilder initial
-        closure = logicalBuilderObjectClosure builder
+        closure = candidateProofObjectClosure initial
     Except.liftEither do
         unless
             ( Vector.null (Backend.supportedPropositionSupport claim)
@@ -1293,8 +1290,7 @@ validatePreparedVampireProblem candidate prepared initial = do
             (failCandidateProof
                 (VampirePremiseMismatch fingerprint))
         let closure =
-                logicalBuilderObjectClosure
-                    (candidateProofBuilder state)
+                candidateProofObjectClosure state
         supported <-
             either
                 (const
@@ -1438,6 +1434,7 @@ initialDeclarationState resolver builder =
             DeclarationInvocation
                 (logicalBuilderNextInvocation builder)
         , declarationObjectsReversed = []
+        , declarationObjectClosure = Nothing
         , declarationPropositionsReversed = []
         , declarationReservations = Map.empty
         , declarationPending = Map.empty
@@ -1499,7 +1496,6 @@ appendDeclaration mode declaration = do
     let builder' =
             appendBuilderState
                 closure
-                propositions
                 delta
                 next
                 orderedPending
@@ -1517,21 +1513,29 @@ appendDeclaration mode declaration = do
                 propositions
                 proofValidations
                 declarationValidation
-    forceCommittedBatch batch `seq` pure (builder', batch)
+    pure (builder', batch)
 
 declarationClosure
     :: DeclarationState
     -> Either DeclarationError CheckedObjectClosure
 declarationClosure declaration =
-    first DeclarationObjectValidationFailed
-        (validateObjectClosure
-            (logicalBuilderTheory
-                (declarationBuilder declaration))
-            ( logicalBuilderObjects
-                (declarationBuilder declaration)
-              <> reverse
-                    (declarationObjectsReversed declaration)
-            ))
+    case declarationObjectClosure declaration of
+        Just closure ->
+            Right closure
+        Nothing ->
+            first DeclarationObjectValidationFailed
+                (extendObjectClosure
+                    (logicalBuilderObjectClosure
+                        (declarationBuilder declaration))
+                    (reverse
+                        (declarationObjectsReversed declaration)))
+
+prepareDeclarationClosure
+    :: DeclarationState
+    -> Either DeclarationError DeclarationState
+prepareDeclarationClosure declaration = do
+    closure <- declarationClosure declaration
+    pure declaration{declarationObjectClosure = Just closure}
 
 validateDeclarationPropositions
     :: CheckedObjectClosure
@@ -1567,7 +1571,7 @@ validatePendingAuthorization declaration
     validateReservedCandidate declaration candidate
     let builder = declarationBuilder declaration
         PendingFactAuthorization
-            identity prefix invocation slot authority stage frontier =
+            identity prefix invocation slot authority stage =
                 authorization
     unless
         ( identity == logicalBuilderIdentity builder
@@ -1576,7 +1580,6 @@ validatePendingAuthorization declaration
           && slot == reservedCandidateSlot candidate
           && authority == validationTarget certificate
           && stage == reservedStage candidate
-          && frontier == stage
         )
         (Left PendingFactAuthorizationMismatch)
 
@@ -1686,33 +1689,19 @@ validateBuilderCollisions builder delta = do
 
 appendBuilderState
     :: CheckedObjectClosure
-    -> [CheckedPropositionContent]
     -> DeclarationInterfaceDelta
     -> PrefixContextId
     -> [PendingCandidate]
     -> LogicalBuilder
     -> DeclarationState
     -> LogicalBuilder
-appendBuilderState closure propositions delta next pending builder declaration =
+appendBuilderState closure delta next pending builder declaration =
     builder
         { logicalBuilderPrefix = next
-        , logicalBuilderObjects =
-            logicalBuilderObjects builder
-                <> reverse
-                    (declarationObjectsReversed declaration)
         , logicalBuilderObjectClosure = closure
-        , logicalBuilderPropositions =
-            foldl'
-                (\entries proposition ->
-                    Map.insert
-                        (checkedPropositionId proposition)
-                        proposition
-                        entries)
-                (logicalBuilderPropositions builder)
-                propositions
         , logicalBuilderFacts =
             foldl'
-                (insertAuthorizedFact builder next)
+                (insertAuthorizedFact builder)
                 (logicalBuilderFacts builder)
                 pending
         , logicalBuilderAliases =
@@ -1736,11 +1725,10 @@ appendBuilderState closure propositions delta next pending builder declaration =
 
 insertAuthorizedFact
     :: LogicalBuilder
-    -> PrefixContextId
     -> Map SemanticFactOccurrenceFingerprint AuthorizedFact
     -> PendingCandidate
     -> Map SemanticFactOccurrenceFingerprint AuthorizedFact
-insertAuthorizedFact builder next entries pending@(PendingCandidate
+insertAuthorizedFact builder entries pending@(PendingCandidate
         candidate certificate _pendingAuthorization) =
     let occurrence = occurrenceFromPending pending
         fingerprint = semanticFactFingerprint occurrence
@@ -1748,7 +1736,6 @@ insertAuthorizedFact builder next entries pending@(PendingCandidate
         authorization =
             BuilderFactAuthorization
                 (logicalBuilderIdentity builder)
-                next
                 (reservedCandidateSlot candidate)
                 authority
     in Map.insert
@@ -1806,6 +1793,7 @@ data DeclarationError
     | VampirePremiseCapabilityMismatch
         !SemanticFactOccurrenceFingerprint
     | VampireFoundationMismatch !FoundationAxiomTag
+    | DeclarationObjectAddedAfterAuthorization
     | DeclarationObjectValidationFailed !ObjectValidationError
     | DeclarationPropositionValidationFailed
         !PropositionValidationError
diff --git a/source/Checking/Identity.hs b/source/Checking/Identity.hs
index fb67172..fd41945 100644
--- a/source/Checking/Identity.hs
+++ b/source/Checking/Identity.hs
@@ -34,6 +34,7 @@ module Checking.Identity
     , lookupCheckedObjectType
     , lookupCheckedObjectContent
     , validateObjectClosure
+    , extendObjectClosure
     , ObjectValidationError(..)
     , PropositionId
     , propositionIdDigest
@@ -434,6 +435,39 @@ validateObjectClosure expectedTheory asserted = do
             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)