Lower relation expressions through ordered pairs

1 files changed, 48 insertions, 0 deletions

diff --git a/source/Test/Unit/Module.hs b/source/Test/Unit/Module.hs
index f7e8fed..e840dba 100644
--- a/source/Test/Unit/Module.hs
+++ b/source/Test/Unit/Module.hs
@@ -88,6 +88,8 @@ unitTests =
             rejectsUnsupportedTypedSource
         , testCase "compiles exact declarations across an import"
             compilesExactDeclarationGraph
+        , testCase "compiles exact relation expressions"
+            compilesExactRelationExpressions
         , testCase "compiles exact ordinary proofs"
             compilesExactOrdinaryProofs
         , testCase "compiles exact separation comprehensions"
@@ -1427,6 +1429,52 @@ compilesExactDeclarationGraph = do
         Identity.TransparentObjectContent{} -> "transparent"
         Identity.IntrinsicObjectContent{} -> "intrinsic"
 
+compilesExactRelationExpressions :: Assertion
+compilesExactRelationExpressions = do
+    positive <-
+        withAcceptedFixtureVampire "felix-exact-relation-expression" \prover ->
+            runNoLoggingT
+                (Api.verifyMeasured
+                    prover
+                    "test/phase5/exact-relation-expression.tex")
+    case positive of
+        Right (result, _measurements) ->
+            assertTypedSuccess "relation expression" result
+        Left err ->
+            assertFailure
+                ("relation expression failed: " <> show err)
+
+    missingPair <-
+        withAcceptedFixtureVampire "felix-exact-relation-expression-missing-pair" \prover ->
+            runNoLoggingT
+                (Api.verifyMeasured
+                    prover
+                    "test/phase5/exact-relation-expression-missing-pair.tex")
+    case missingPair of
+        Left
+            (Api.VerificationTypedModuleError
+                _source
+                (Module.TypedActionFailed
+                    (Module.TypedExactProofFailed
+                        (ExactProof.ExactProofElaborationFailed
+                            (Exact.ExactGlobalNotVisible location key))))
+                prefix) -> do
+            assertEqual "missing ordered-pair provider line"
+                2
+                (locLine location)
+            assertEqual "missing ordered-pair semantic key"
+                (Semantic.SemanticExpressionFunction
+                    (Raw.mixfixPattern Raw.PairSymbol))
+                key
+            assertEqual "missing provider publishes no declaration"
+                0
+                (length (Declaration.pendingModulePrefixBatches prefix))
+        Left err ->
+            assertFailure
+                ("unexpected relation-expression failure: " <> show err)
+        Right{} ->
+            assertFailure "relation expression without ordered pairing was admitted"
+
 compilesExactOrdinaryProofs :: Assertion
 compilesExactOrdinaryProofs =
     Temp.withSystemTempDirectory "felix-exact-proofs" \root -> do