1 files changed, 96 insertions, 31 deletions

diff --git a/source/Test/Unit/Core.hs b/source/Test/Unit/Core.hs
index fd817c6..e1ba10d 100644
--- a/source/Test/Unit/Core.hs
+++ b/source/Test/Unit/Core.hs
@@ -15,16 +15,20 @@ import Test.Tasty.HUnit hiding (assert)
 import Test.Tasty.Hedgehog (testPropertyNamed)
 
 
-data TestGlobal = TestGlobal
+data TestGlobal
+    = TestGlobal
+    | TestPairGlobal
     deriving (Show, Eq, Ord)
 
 instance NFData TestGlobal where
-    rnf TestGlobal =
+    rnf _global =
         ()
 
 testGlobalType :: TestGlobal -> Maybe CoreType
 testGlobalType TestGlobal =
     Just TySet
+testGlobalType TestPairGlobal =
+    Just (TySet `TyArrow` (TySet `TyArrow` TySet))
 
 unitTests :: TestTree
 unitTests =
@@ -51,6 +55,9 @@ unitTests =
             "specializes the checked separation characteristic"
             specializesCheckedSeparationCharacteristic
         , testCase
+            "specializes the checked replacement characteristic"
+            specializesCheckedReplacementCharacteristic
+        , testCase
             "thaws checked closed terms without changing them"
             thawsCheckedClosedTerms
         , testPropertyNamed
@@ -325,7 +332,11 @@ specializesCheckedSeparationCharacteristic = do
         maybe
             (assertFailure "separation did not form a set definition")
             pure
-            (scopedSetDefinition body)
+            (scopedSetDefinition
+                (Foundation.foundationAxiomFrozen
+                    foundation
+                    Foundation.SeparationCharacteristic)
+                body)
     let generated =
             instantiateCanonical
                 separation
@@ -343,36 +354,90 @@ specializesCheckedSeparationCharacteristic = do
         "local characteristic is the checked rule specialization"
         expected
         generated
+
+specializesCheckedReplacementCharacteristic :: Assertion
+specializesCheckedReplacementCharacteristic = do
+    foundation <-
+        either
+            (assertFailure . show)
+            pure
+            Foundation.checkedFoundation
+    pair <- checked [] (CGlobal TestPairGlobal)
+    domain <- checked [] (CIntrinsic Empty)
+    value <- checked [TySet] (CBound 0)
+    (graph, checkedDomain, function) <-
+        maybe
+            (assertFailure "checked values did not form a replacement graph")
+            pure
+            (scopedReplacementGraph pair domain value)
+    definition <-
+        maybe
+            (assertFailure "replacement graph did not form a definition")
+            pure
+            (scopedCharacteristicDefinition
+                (Foundation.foundationAxiomFrozen
+                    foundation
+                    Foundation.ReplacementCharacteristic)
+                graph
+                (checkedDomain :| [function]))
+    let generated =
+            instantiateCanonical
+                (scopedCoreTerm graph)
+                (scopedCoreTerm definition)
+        expected =
+            betaNormalize
+                (specializeForall (scopedCoreTerm function)
+                (specializeForall (scopedCoreTerm checkedDomain)
+                    (mapCanonicalGlobals absurd
+                        (frozenCoreTerm
+                            (Foundation.foundationAxiomFrozen
+                                foundation
+                                Foundation.ReplacementCharacteristic)))))
+    assertEqual
+        "local graph characteristic is the checked rule specialization"
+        expected
+        generated
   where
-    specializeForall argument = \case
-        CForall _binderType body ->
-            instantiateCanonical argument body
-        _ ->
-            error "the checked separation characteristic lost a binder"
+    checked context term =
+        either
+            (assertFailure . show)
+            pure
+            (checkScopedCanonicalCore testGlobalType context term)
+
+specializeForall
+    :: CanonicalTerm global
+    -> CanonicalTerm global
+    -> CanonicalTerm global
+specializeForall argument = \case
+    CForall _binderType body ->
+        instantiateCanonical argument body
+    _ ->
+        error "the checked characteristic lost a binder"
 
-    betaNormalize = \case
-        CApp function argument ->
-            case betaNormalize function of
-                CLam _binderType body ->
-                    betaNormalize
-                        (instantiateCanonical
-                            (betaNormalize argument)
-                            body)
-                normalizedFunction ->
-                    CApp normalizedFunction (betaNormalize argument)
-        CLam binderType body ->
-            CLam binderType (betaNormalize body)
-        CImp premise conclusion ->
-            CImp
-                (betaNormalize premise)
-                (betaNormalize conclusion)
-        CEq operandType left right ->
-            CEq operandType
-                (betaNormalize left)
-                (betaNormalize right)
-        CForall binderType body ->
-            CForall binderType (betaNormalize body)
-        term -> term
+betaNormalize :: CanonicalTerm global -> CanonicalTerm global
+betaNormalize = \case
+    CApp function argument ->
+        case betaNormalize function of
+            CLam _binderType body ->
+                betaNormalize
+                    (instantiateCanonical
+                        (betaNormalize argument)
+                        body)
+            normalizedFunction ->
+                CApp normalizedFunction (betaNormalize argument)
+    CLam binderType body ->
+        CLam binderType (betaNormalize body)
+    CImp premise conclusion ->
+        CImp
+            (betaNormalize premise)
+            (betaNormalize conclusion)
+    CEq operandType left right ->
+        CEq operandType
+            (betaNormalize left)
+            (betaNormalize right)
+    CForall binderType body ->
+        CForall binderType (betaNormalize body)
+    term -> term
 
 thawsCheckedClosedTerms :: Assertion
 thawsCheckedClosedTerms = do