Retain exact omitted-proof locations

1 files changed, 56 insertions, 0 deletions

diff --git a/source/Test/Unit/Module.hs b/source/Test/Unit/Module.hs
index d5367b9..4a1122e 100644
--- a/source/Test/Unit/Module.hs
+++ b/source/Test/Unit/Module.hs
@@ -72,6 +72,8 @@ unitTests =
             confinesFoundationLeafCompletion
         , testCase "builds the confined final prelude"
             buildsConfinedFinalPrelude
+        , testCase "retains exact omitted-proof locations"
+            retainsExactOmittedProofLocation
         , testCase "coalesces syntax without collapsing semantic imports"
             coalescesSharedDirectSyntax
         , testCase "resets gloss state between modules"
@@ -424,6 +426,60 @@ buildsConfinedFinalPrelude = do
         FinalPrelude.FinalPreludeSourceParseFailed failure ->
             assertFailure ("final prelude did not parse: " <> show failure)
 
+retainsExactOmittedProofLocation :: Assertion
+retainsExactOmittedProofLocation = do
+    foundation <- expectRight Foundation.checkedFoundation
+    source <-
+        expectRight
+            (Prelude.reservedPreludeSourceInput
+                (Text.encodeUtf8
+                    (StrictText.unlines
+                        [ "\\begin{proposition}\\label{omitted_location}"
+                        , "    For all $x$ we have $x = x$."
+                        , "\\end{proposition}"
+                        , "\\begin{proof}"
+                        , "    Omitted."
+                        , "\\end{proof}"
+                        ])))
+    parsed <- expectRight =<< Prelude.parseReservedPreludeSource source
+    let blocks =
+            Parse.identifiedParsedModuleBlocks
+                (Prelude.reservedParsedPreludeModule parsed)
+    claim <- sole "omitted claim"
+        [ block
+        | block@Raw.BlockClaim{} <- blocks
+        ]
+    proof <- sole "omitted proof"
+        [ sourceProof
+        | Raw.BlockProof _location sourceProof _end <- blocks
+        ]
+    outcome <-
+        Declaration.runModuleDriver
+            foundation
+            preludeModuleName
+            []
+            unusedResolver
+            Declaration.FreshValidation do
+                ExactProof.prepareExactProof claim (Just proof)
+                    >>= either Declaration.failModuleDriver pure
+    case outcome of
+        Right (Declaration.DriverSucceeded
+                prepared _semantic prefix _closure) -> do
+            location <-
+                maybe
+                    (assertFailure "prepared omitted proof lost its location")
+                    pure
+                    (ExactProof.preparedExactProofFirstOmission prepared)
+            assertEqual "omitted source line" 5 (locLine location)
+            assertBool "preparation publishes no declaration"
+                (null (Declaration.pendingModulePrefixBatches prefix))
+        Right (Declaration.DriverFailed failure _prefix) ->
+            assertFailure ("omitted preparation failed: " <> show failure)
+        Right (Declaration.DriverSealFailed failure _prefix) ->
+            assertFailure ("omitted preparation did not seal: " <> show failure)
+        Left failure ->
+            assertFailure ("omitted preparation did not open: " <> show failure)
+
 coalescesSharedDirectSyntax :: Assertion
 coalescesSharedDirectSyntax = do
     foundation <- expectRight Foundation.checkedFoundation