Add owned Vampire request handles

1 files changed, 98 insertions, 44 deletions

diff --git a/source/Checking/Declaration.hs b/source/Checking/Declaration.hs
index 15c8282..3919630 100644
--- a/source/Checking/Declaration.hs
+++ b/source/Checking/Declaration.hs
@@ -38,6 +38,7 @@ module Checking.Declaration
     , failModuleDriver
     , VampireResolver
     , vampireBatchResolver
+    , vampireBatchResolverWithPreparationObserver
     , vampireResolver
     , Declaration
     , failDeclaration
@@ -436,7 +437,7 @@ forceCommittedBatch
                 (declarationValidationRecordCertificates record)
 
 
-newtype VampireResolver = VampireResolver
+data VampireResolver = VampireResolver
     { resolveVampireBatch
         :: forall local origin.
             NonEmpty
@@ -450,6 +451,7 @@ newtype VampireResolver = VampireResolver
                     (Either
                         Provers.ProverProcessError
                         Provers.ProverAnswer))
+    , observeVampirePreparationNanoseconds :: !(Word64 -> IO ())
     }
 
 vampireBatchResolver
@@ -466,7 +468,25 @@ vampireBatchResolver
                     Provers.ProverProcessError
                     Provers.ProverAnswer)))
     -> VampireResolver
-vampireBatchResolver =
+vampireBatchResolver resolve =
+    vampireBatchResolverWithPreparationObserver resolve (const (pure ()))
+
+vampireBatchResolverWithPreparationObserver
+    :: (forall local origin.
+        NonEmpty
+            (Provers.PreparedTypedProverTask
+                SemanticFactOccurrenceFingerprint
+                local
+                origin
+                ObjectId)
+        -> IO
+            (NonEmpty
+                (Either
+                    Provers.ProverProcessError
+                    Provers.ProverAnswer)))
+    -> (Word64 -> IO ())
+    -> VampireResolver
+vampireBatchResolverWithPreparationObserver =
     VampireResolver
 
 vampireResolver
@@ -1985,27 +2005,30 @@ prepareScopedVampireObligationForMode
 prepareScopedVampireObligationForMode
         taskMode claimSupport claim scopedLocals auxiliaryTags selection =
     ModuleDriver do
-        DriverState _resolver builder _prefix _validation <- State.get
+        DriverState resolver builder _prefix _validation <- State.get
         let closure = logicalBuilderObjectClosure builder
             globalType = (`lookupCheckedObjectType` closure)
-        pure do
-            supportedClaim <-
-                first VampireObligationClaimProjectionFailed
-                    (Backend.projectSupportedProposition
-                        globalType
-                        claimSupport
-                        claim)
-            locals <- traverse
-                (prepareLocal globalType)
-                scopedLocals
-            prepareVampireObligationWith
-                taskMode
-                builder
-                closure
-                supportedClaim
-                locals
-                auxiliaryTags
-                selection
+            preparation = do
+                supportedClaim <-
+                    first VampireObligationClaimProjectionFailed
+                        (Backend.projectSupportedProposition
+                            globalType
+                            claimSupport
+                            claim)
+                locals <- traverse
+                    (prepareLocal globalType)
+                    scopedLocals
+                prepareVampireObligationWith
+                    taskMode
+                    builder
+                    closure
+                    supportedClaim
+                    locals
+                    auxiliaryTags
+                    selection
+        State.lift
+            (Except.liftIO
+                (measureVampirePreparation resolver preparation))
   where
     prepareLocal globalType
             (ScopedVampirePremise
@@ -2098,6 +2121,32 @@ prepareVampireObligationWith
                 problem)
     pure (PreparedVampireObligation problem task)
 
+measureVampirePreparation
+    :: VampireResolver
+    -> Either
+        (VampireObligationPreparationError local)
+        (PreparedVampireObligation local origin)
+    -> IO
+        (Either
+            (VampireObligationPreparationError local)
+            (PreparedVampireObligation local origin))
+measureVampirePreparation resolver preparation = do
+    started <- getMonotonicTimeNSec
+    prepared <- Exception.evaluate (forcePrepared preparation)
+    finished <- getMonotonicTimeNSec
+    observeVampirePreparationNanoseconds resolver (finished - started)
+    pure prepared
+  where
+    forcePrepared result =
+        case result of
+            Left err -> err `seq` result
+            Right prepared@(PreparedVampireObligation _ task) ->
+                let request = Provers.preparedTypedProverRequest task
+                in Provers.preparedVerificationByteCount request `seq`
+                    Provers.preparedVerificationRequestId request `seq`
+                    prepared `seq`
+                    result
+
 selectVampireFacts
     :: (ObjectId -> Maybe CoreType)
     -> LogicalBuilder
@@ -2840,35 +2889,39 @@ prepareCurrentCandidateVampire = CandidateProof do
         closed proposition =
             embedClosedCore []
                 (checkedPropositionTerm proposition)
-    supportedTarget <-
-        State.lift
-            (Except.liftEither
-                (first
-                    (CurrentCandidateVampirePreparationFailed
-                        . VampireObligationClaimProjectionFailed)
+        resolver =
+            declarationVampireResolver
+                (candidateProofDeclaration initial)
+        preparation = do
+            supportedTarget <-
+                first
+                    VampireObligationClaimProjectionFailed
                     (Backend.projectSupportedProposition
                         globalType
                         (Vector.empty :: Vector (Void, CoreType))
-                        (closed target))))
-    locals <-
+                        (closed target))
+            locals <-
+                traverse
+                    (prepareLocal globalType)
+                    (zip [0 :: Natural ..] premises)
+            prepareVampireObligationWith
+                Provers.DirectTask
+                builder
+                closure
+                supportedTarget
+                locals
+                []
+                VampireLocalPremises
+    preparedResult <-
         State.lift
-            (Except.liftEither
-                (first CurrentCandidateVampirePreparationFailed
-                    (traverse
-                        (prepareLocal globalType)
-                        (zip [0 :: Natural ..] premises))))
+            (liftIO
+                (measureVampirePreparation resolver preparation))
     prepared <-
         State.lift
             (Except.liftEither
-                (first CurrentCandidateVampirePreparationFailed
-                    (prepareVampireObligationWith
-                        Provers.DirectTask
-                        builder
-                        closure
-                        supportedTarget
-                        locals
-                        []
-                        VampireLocalPremises)))
+                (first
+                    CurrentCandidateVampirePreparationFailed
+                    preparedResult))
     pure prepared
   where
     prepareLocal globalType (index, CandidatePremise proposition) = do
@@ -3223,7 +3276,8 @@ validateAcceptedVampireResult prepared result = do
             traverse_
                 (\accepted ->
                     unless
-                        (Provers.acceptedVampireRequest accepted == request)
+                        (Provers.acceptedVampireRequestId accepted
+                            == Provers.preparedVerificationRequestId request)
                         (Except.throwError VampireRequestMismatch))
                 (either (const Nothing) Provers.provedVampireRun resolved))
         result