Lower exact finite-set notation

1 files changed, 77 insertions, 0 deletions

diff --git a/source/Test/Unit/Declaration.hs b/source/Test/Unit/Declaration.hs
index 14b7f08..6fc3b56 100644
--- a/source/Test/Unit/Declaration.hs
+++ b/source/Test/Unit/Declaration.hs
@@ -60,6 +60,8 @@ unitTests =
             lowersExactSeparationComprehensions
         , testCase "lowers exact replacement telescopes"
             lowersExactReplacementTelescopes
+        , testCase "lowers exact finite sets"
+            lowersExactFiniteSets
         , testCase "lowers exact ordinary declarations"
             lowersExactOrdinaryDeclarations
         , testCase "folds transitive and diamond import evidence"
@@ -1799,6 +1801,81 @@ lowersExactReplacementTelescopes = do
             assertFailure
                 ("replacement driver did not seal: " <> show failure)
 
+lowersExactFiniteSets :: Assertion
+lowersExactFiniteSets = do
+    fixture <- makeNamedFixture "exact-finite-set"
+    let location = mkLocation (FileId 75) 2 1
+        a = Raw.NamedVarAt location "a"
+        b = Raw.NamedVarAt location "b"
+        equality left right =
+            Raw.StmtFormula
+                (Raw.FormulaChain
+                    (Raw.ChainBase
+                        (left :| [])
+                        Raw.Positive
+                        (Raw.Relation Nowhere Raw.EqSymbol [])
+                        (right :| [])))
+        statement =
+            Raw.SymbolicQuantified
+                Nowhere
+                Raw.Universally
+                (a :| [b])
+                Raw.Unbounded
+                Nothing
+                (equality
+                    (Raw.ExprFiniteSet
+                        location
+                        (Raw.ExprVar a :| [Raw.ExprVar b]))
+                    (Raw.ExprVar a))
+        app1 intrinsic argument =
+            Core.CApp (Core.CIntrinsic intrinsic) argument
+        app2 intrinsic first second =
+            Core.CApp (app1 intrinsic first) second
+        insert element rest =
+            app1 Core.FamilyUnion
+                (app2 Core.PairSet
+                    (app2 Core.PairSet element element)
+                    rest)
+        expected =
+            Core.CForall Core.TySet
+                (Core.CForall Core.TySet
+                    (Core.CEq Core.TySet
+                        (insert
+                            (Core.CBound 1)
+                            (insert
+                                (Core.CBound 0)
+                                (Core.CIntrinsic Core.Empty)))
+                        (Core.CBound 1)))
+        action
+            :: Declaration.ModuleDriver Text
+                (Either
+                    Exact.ExactCompileError
+                    Exact.PreparedExactProposition)
+        action =
+            Exact.prepareExactProposition
+                Exact.emptyExactBinderContext
+                statement
+    runDriver fixture action >>= \case
+        Declaration.DriverSucceeded
+                (Right prepared) _interface _prefix _closure ->
+            assertEqual
+                "source-order finite-set core"
+                expected
+                (Core.scopedCoreTerm
+                    (Exact.preparedExactPropositionCore prepared))
+        Declaration.DriverSucceeded
+                (Left failure) _interface _prefix _closure ->
+            assertFailure
+                ("valid finite set failed: "
+                    <> Text.unpack
+                        (Exact.renderExactCompileError failure))
+        Declaration.DriverFailed failure _prefix ->
+            assertFailure
+                ("finite-set driver failed: " <> show failure)
+        Declaration.DriverSealFailed failure _prefix ->
+            assertFailure
+                ("finite-set driver did not seal: " <> show failure)
+
 lowersExactOrdinaryDeclarations :: Assertion
 lowersExactOrdinaryDeclarations = do
     fixture <- makeNamedFixture "exact-lowering"