Reject unresolved structure operations before encoding

1 files changed, 69 insertions, 0 deletions

diff --git a/source/Test/Unit/Checking.hs b/source/Test/Unit/Checking.hs
index 7a2d61c..4a11bd9 100644
--- a/source/Test/Unit/Checking.hs
+++ b/source/Test/Unit/Checking.hs
@@ -125,6 +125,41 @@ unitTests = testGroup "Checking"
     , testCase "struct axioms annotate operations from the same structure" do
         text <- encodedTasksText structOperationRewriteBlocks
         assertContains "annotated struct operation in rule" "zf_u0(zf_s1(zf_f0),zf_s0(zf_f0))" text
+    , testCase "structure terms fail before task encoding" do
+        unresolved <-
+            try
+                (check
+                    WithoutDumpPremselTraining
+                    unresolvedStructOperationBlocks)
+                :: IO (Either CheckingError [Task])
+        case unresolved of
+            Left
+                (UnresolvedStructureOperation
+                    actualSymbol
+                    actualLocation
+                    actualMarker) -> do
+                        assertEqual
+                            "structure operation"
+                            fooOp
+                            actualSymbol
+                        assertEqual
+                            "block location"
+                            structureTermErrorLocation
+                            actualLocation
+                        assertEqual
+                            "block marker"
+                            "unresolved_structure_operation"
+                            actualMarker
+            Left err ->
+                assertFailure
+                    ("expected unresolved structure operation, got "
+                        <> show err)
+            Right _ ->
+                assertFailure
+                    "expected unresolved structure operation to fail"
+        expectCheckingError
+            "Nested comprehensions are not supported"
+            nestedStructComprehensionBlocks
     , testCase "exact structure claims introduce carrier labels for continuations" do
         text <- encodedTasksText structClaimIntroducesContextBlocks
         assertContains "claim continuation carrier" "conjecture,zf_u0(zf_f1,zf_s0(zf_f0))" text
@@ -791,6 +826,40 @@ structOperationRewriteBlocks =
     , BlockProof Nowhere Nowhere (Qed (Just Nowhere) (JustificationRef ("foo_op_rule" :| [])))
     ]
 
+unresolvedStructOperationBlocks :: [Block]
+unresolvedStructOperationBlocks =
+    [ fooStructBlock "unresolved_structure_definition" []
+    , BlockAxiom
+        structureTermErrorLocation
+        "unresolved_structure_operation"
+        (Axiom []
+            (TermSymbolStruct fooOp Nothing
+                `eq` TermSymbolStruct fooOp Nothing))
+    ]
+
+nestedStructComprehensionBlocks :: [Block]
+nestedStructComprehensionBlocks =
+    [ fooStructBlock "nested_structure_definition" []
+    , BlockAxiom
+        structureTermErrorLocation
+        "nested_structure_comprehension"
+        (Axiom []
+            (nestedOperation `eq` nestedOperation))
+    ]
+  where
+    nestedOperation =
+        TermSymbolStruct
+            fooOp
+            (Just
+                (TermSep
+                    "x"
+                    emptySet
+                    (toScope Top)))
+
+structureTermErrorLocation :: Location
+structureTermErrorLocation =
+    mkLocation (FileId 50) 7 1
+
 structClaimIntroducesContextBlocks :: [Block]
 structClaimIntroducesContextBlocks =
     [ fooStructBlock "foo_claim_struct" []