Freeze checked HOL terms canonically

1 files changed, 189 insertions, 0 deletions

diff --git a/source/Test/Unit/Core.hs b/source/Test/Unit/Core.hs
new file mode 100644
index 0000000..cb32323
--- /dev/null
+++ b/source/Test/Unit/Core.hs
@@ -0,0 +1,189 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+
+module Test.Unit.Core (unitTests) where
+
+import Base
+import Checking.Core
+
+import Control.DeepSeq (NFData(..), force)
+import Hedgehog
+import Hedgehog.Gen qualified as Gen
+import Hedgehog.Range qualified as Range
+import Test.Tasty
+import Test.Tasty.HUnit hiding (assert)
+import Test.Tasty.Hedgehog (testPropertyNamed)
+
+
+data TestGlobal = TestGlobal
+    deriving (Show, Eq, Ord)
+
+instance NFData TestGlobal where
+    rnf TestGlobal =
+        ()
+
+testGlobalType :: TestGlobal -> Maybe CoreType
+testGlobalType TestGlobal =
+    Just TySet
+
+unitTests :: TestTree
+unitTests =
+    testGroup "Checked core"
+        [ testCase
+            "freezes explicit binder positions"
+            freezesExplicitBinderPositions
+        , testCase
+            "freezes generalized substitution without capture"
+            freezesGeneralizedSubstitution
+        , testCase
+            "rejects ill-typed and open terms"
+            rejectsInvalidTerms
+        , testPropertyNamed
+            "optimized freeze agrees with bounded reference"
+            "prop_freezeAgreesWithReference"
+            prop_freezeAgreesWithReference
+        ]
+
+freezesExplicitBinderPositions :: Assertion
+freezesExplicitBinderPositions = do
+    let x = 0 :: Int
+        y = 1 :: Int
+        freeze body = do
+            checked <-
+                either
+                    (assertFailure . show)
+                    pure
+                    (checkClosedCore
+                        testGlobalType
+                        (coreLambda TySet x
+                            (coreLambda TyProp y body)))
+            either
+                (assertFailure . show)
+                (pure . frozenCoreTerm)
+                (freezeClosed checked)
+    nearest <-
+        freeze (coreLocal y)
+    outer <-
+        freeze (coreLocal x)
+    global <-
+        freeze (coreGlobal TestGlobal)
+    assertEqual
+        "nearest binder"
+        (CLam TySet (CLam TyProp (CBound 0)))
+        nearest
+    assertEqual
+        "outer binder"
+        (CLam TySet (CLam TyProp (CBound 1)))
+        outer
+    assertEqual
+        "global with both vacuous binders"
+        (CLam TySet (CLam TyProp (CGlobal TestGlobal)))
+        global
+
+freezesGeneralizedSubstitution :: Assertion
+freezesGeneralizedSubstitution = do
+    let outer = 0 :: Int
+        inner = 1 :: Int
+        placeholder = 2 :: Int
+        innerTerm =
+            coreLambda TySet inner (coreLocal placeholder)
+        substituted =
+            innerTerm >>= \local ->
+                if local == placeholder
+                    then coreLocal outer
+                    else coreLocal local
+        term =
+            coreLambda TyProp outer substituted
+    checked <-
+        either
+            (assertFailure . show)
+            pure
+            (checkClosedCore testGlobalType term)
+    optimized <-
+        either
+            (assertFailure . show)
+            pure
+            (freezeClosed checked)
+    reference <-
+        either
+            (assertFailure . show)
+            pure
+            (referenceFreezeClosed checked)
+    assertEqual "reference result" reference optimized
+    assertEqual
+        "outer variable remains outside the inner binder"
+        (CLam TyProp (CLam TySet (CBound 1)))
+        (frozenCoreTerm optimized)
+
+rejectsInvalidTerms :: Assertion
+rejectsInvalidTerms = do
+    assertEqual
+        "free local"
+        (Left UnboundCoreLocal)
+        (checkedCoreType
+            <$> checkClosedCore
+                testGlobalType
+                (coreLocal (0 :: Int)))
+    assertEqual
+        "application argument"
+        (Left
+            (ApplicationArgumentTypeMismatch
+                TySet
+                TyProp))
+        (checkedCoreType
+            <$> checkClosedCore
+                testGlobalType
+                (coreApply
+                    (coreIntrinsic FamilyUnion)
+                    coreFalsum))
+    assertEqual
+        "equality operand"
+        (Left
+            (EqualityOperandTypeMismatch
+                TySet
+                TyProp))
+        (checkedCoreType
+            <$> checkClosedCore
+                testGlobalType
+                (coreEquality
+                    TySet
+                    coreFalsum
+                    (coreGlobal TestGlobal)))
+
+prop_freezeAgreesWithReference :: Property
+prop_freezeAgreesWithReference = property do
+    depth <-
+        forAll (Gen.int (Range.linear 1 10))
+    binderTypes <-
+        forAll
+            (Gen.list
+                (Range.singleton depth)
+                (Gen.element
+                    [ TyProp
+                    , TySet
+                    , TySet `TyArrow` TySet
+                    ]))
+    selected <-
+        forAll
+            (Gen.maybe
+                (Gen.int (Range.linear 0 (depth - 1))))
+    let binders =
+            zip [0 :: Int ..] binderTypes
+        body =
+            maybe
+                (coreGlobal TestGlobal)
+                coreLocal
+                selected
+        term =
+            foldr
+                (\(local, binderType) ->
+                    coreLambda binderType local)
+                body
+                binders
+    checked <-
+        evalEither
+            (checkClosedCore testGlobalType term)
+    optimized <-
+        evalEither (force <$> freezeClosed checked)
+    reference <-
+        evalEither (force <$> referenceFreezeClosed checked)
+    optimized === reference