Lower exact replacement telescopes

1 files changed, 133 insertions, 0 deletions

diff --git a/source/Test/Unit/Declaration.hs b/source/Test/Unit/Declaration.hs
index c303a53..14b7f08 100644
--- a/source/Test/Unit/Declaration.hs
+++ b/source/Test/Unit/Declaration.hs
@@ -58,6 +58,8 @@ unitTests =
             elaboratesScopedExactPropositions
         , testCase "lowers exact separation comprehensions"
             lowersExactSeparationComprehensions
+        , testCase "lowers exact replacement telescopes"
+            lowersExactReplacementTelescopes
         , testCase "lowers exact ordinary declarations"
             lowersExactOrdinaryDeclarations
         , testCase "folds transitive and diamond import evidence"
@@ -1666,6 +1668,137 @@ lowersExactSeparationComprehensions = do
         Declaration.DriverSealFailed failure _prefix ->
             assertFailure ("separation exact driver did not seal: " <> show failure)
 
+lowersExactReplacementTelescopes :: Assertion
+lowersExactReplacementTelescopes = do
+    fixture <- makeNamedFixture "exact-replacement-telescope"
+    let location = mkLocation (FileId 74) 2 1
+        futureOccurrenceLocation = mkLocation (FileId 74) 7 19
+        a = Raw.NamedVarAt location "A"
+        x = Raw.NamedVarAt location "x"
+        y = Raw.NamedVarAt location "y"
+        futureY = Raw.NamedVarAt futureOccurrenceLocation "y"
+        equality left right =
+            Raw.StmtFormula
+                (Raw.FormulaChain
+                    (Raw.ChainBase
+                        (left :| [])
+                        Raw.Positive
+                        (Raw.Relation Nowhere Raw.EqSymbol [])
+                        (right :| [])))
+        replacement firstDomain =
+            Raw.ExprReplace
+                location
+                (Raw.ExprVar y)
+                ( (x, firstDomain) :|
+                    [(y, Raw.ExprVar x)]
+                )
+                (Just (equality (Raw.ExprVar x) (Raw.ExprVar y)))
+        validStatement =
+            Raw.SymbolicQuantified
+                Nowhere
+                Raw.Universally
+                (a :| [])
+                Raw.Unbounded
+                Nothing
+                (equality
+                    (replacement (Raw.ExprVar a))
+                    (Raw.ExprVar a))
+        invalidStatement =
+            equality
+                (replacement (Raw.ExprVar futureY))
+                (Raw.ExprInteger Nowhere 0)
+        predicateReplacementLocation = mkLocation (FileId 74) 9 3
+        predicateReplacementStatement =
+            equality
+                (Raw.ExprReplacePred
+                    predicateReplacementLocation
+                    y
+                    x
+                    (Raw.ExprInteger Nowhere 0)
+                    (equality (Raw.ExprVar x) (Raw.ExprVar y)))
+                (Raw.ExprInteger Nowhere 0)
+        app1 intrinsic argument =
+            Core.CApp (Core.CIntrinsic intrinsic) argument
+        app2 intrinsic first second =
+            Core.CApp (app1 intrinsic first) second
+        expected =
+            Core.CForall Core.TySet $
+                Core.CEq Core.TySet
+                    (app1 Core.FamilyUnion $
+                        app2 Core.Repl (Core.CBound 0) $
+                            Core.CLam Core.TySet $
+                                app2 Core.Repl
+                                    (app2 Core.Sep
+                                        (Core.CBound 0)
+                                        (Core.CLam Core.TySet $
+                                            Core.CEq Core.TySet
+                                                (Core.CBound 1)
+                                                (Core.CBound 0)))
+                                    (Core.CLam Core.TySet
+                                        (Core.CBound 0)))
+                    (Core.CBound 0)
+        action
+            :: Declaration.ModuleDriver Text
+                ( Either
+                    Exact.ExactCompileError
+                    Exact.PreparedExactProposition
+                , Either
+                    Exact.ExactCompileError
+                    Exact.PreparedExactProposition
+                , Either
+                    Exact.ExactCompileError
+                    Exact.PreparedExactProposition
+                )
+        action = do
+            valid <- Exact.prepareExactProposition
+                Exact.emptyExactBinderContext
+                validStatement
+            invalid <- Exact.prepareExactProposition
+                Exact.emptyExactBinderContext
+                invalidStatement
+            predicateReplacement <- Exact.prepareExactProposition
+                Exact.emptyExactBinderContext
+                predicateReplacementStatement
+            pure (valid, invalid, predicateReplacement)
+    runDriver fixture action >>= \case
+        Declaration.DriverSucceeded
+                ( Right prepared
+                    , Left failure
+                    , Left predicateReplacementFailure
+                    ) _interface _prefix _closure -> do
+            assertEqual
+                "dependent replacement core"
+                expected
+                (Core.scopedCoreTerm
+                    (Exact.preparedExactPropositionCore prepared))
+            assertEqual
+                "future replacement binder location"
+                (Exact.ExactFreeVariable futureOccurrenceLocation futureY)
+                failure
+            assertEqual
+                "predicate replacement remains unsupported at its location"
+                (Exact.ExactUnsupportedDeclarationBody
+                    predicateReplacementLocation)
+                predicateReplacementFailure
+        Declaration.DriverSucceeded
+                (Left validFailure, _, _) _interface _prefix _closure ->
+            assertFailure
+                ("valid replacement failed: "
+                    <> Text.unpack
+                        (Exact.renderExactCompileError validFailure))
+        Declaration.DriverSucceeded
+                (_, Right{}, _) _interface _prefix _closure ->
+            assertFailure "invalid replacement was accepted"
+        Declaration.DriverSucceeded
+                (_, _, Right{}) _interface _prefix _closure ->
+            assertFailure "predicate replacement was accepted"
+        Declaration.DriverFailed failure _prefix ->
+            assertFailure
+                ("replacement driver failed: " <> show failure)
+        Declaration.DriverSealFailed failure _prefix ->
+            assertFailure
+                ("replacement driver did not seal: " <> show failure)
+
 lowersExactOrdinaryDeclarations :: Assertion
 lowersExactOrdinaryDeclarations = do
     fixture <- makeNamedFixture "exact-lowering"