Migrate to `Felix` namespaceHEADhotg

1 files changed, 284 insertions, 0 deletions

diff --git a/source/Felix/Test/Unit/Foundation.hs b/source/Felix/Test/Unit/Foundation.hs
new file mode 100644
index 0000000..18ead04
--- /dev/null
+++ b/source/Felix/Test/Unit/Foundation.hs
@@ -0,0 +1,284 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+
+module Felix.Test.Unit.Foundation (unitTests) where
+
+import Base
+import Felix.Checking.Core
+import Felix.Checking.Foundation
+
+import Data.List qualified as List
+import Data.Set qualified as Set
+import Test.Tasty
+import Test.Tasty.HUnit
+
+
+unitTests :: TestTree
+unitTests =
+    testGroup "Foundation manifest"
+        [ testCase
+            "accepts the exact compiled foundation"
+            acceptsCompiledFoundation
+        , testCase
+            "rejects incomplete and altered manifests"
+            rejectsManifestMutations
+        , testCase
+            "classifies the exact UnivOf schemas"
+            classifiesUnivOfSchemas
+        , testCase
+            "selects only intrinsic characteristic dependencies"
+            selectsOnlyIntrinsicCharacteristicDependencies
+        ]
+
+acceptsCompiledFoundation :: Assertion
+acceptsCompiledFoundation = do
+    foundation <-
+        either
+            (assertFailure . show)
+            pure
+            checkedFoundation
+    assertEqual
+        "intrinsic coverage"
+        [minBound .. maxBound]
+        (fst <$> compiledFoundationIntrinsicRows)
+    assertEqual
+        "guarded-rule coverage"
+        [minBound .. maxBound]
+        [ tag
+        | FoundationRuleInput tag _signature <-
+            compiledFoundationRuleRows
+        ]
+    for_ [minBound .. maxBound] \tag ->
+        assertEqual
+            ("closed proposition type for " <> show tag)
+            TyProp
+            (frozenCoreType
+                (foundationAxiomFrozen foundation tag))
+
+selectsOnlyIntrinsicCharacteristicDependencies :: Assertion
+selectsOnlyIntrinsicCharacteristicDependencies = do
+    let separation =
+            CApp
+                (CApp (CIntrinsic Sep) (CBound 0))
+                (CLam TySet CFalsum)
+        underUniverse =
+            CApp (CIntrinsic UnivOf) separation
+    assertEqual
+        "separation is found recursively without a universe bundle"
+        (Set.singleton SeparationCharacteristic)
+        (foundationAxiomDependencies underUniverse)
+
+rejectsManifestMutations :: Assertion
+rejectsManifestMutations = do
+    let withoutMinimal =
+            List.filter
+                (\case
+                    FoundationAxiomInput
+                        UnivOfMinimal
+                        _syntax
+                        _backendClass ->
+                            False
+                    _ ->
+                        True)
+                compiledFoundationAxiomRows
+        wrongUnivType =
+            [ if tag == UnivOf
+                then (tag, TySet)
+                else row
+            | row@(tag, _coreType) <-
+                compiledFoundationIntrinsicRows
+            ]
+        duplicatedEmpty =
+            case findAxiomInput EmptyCharacteristic of
+                Just row ->
+                    row : compiledFoundationAxiomRows
+                Nothing ->
+                    impossible
+                        "compiled manifest omitted EmptyCharacteristic"
+        alteredEmpty =
+            replaceAxiomInput
+                EmptyCharacteristic
+                (FoundationAxiomInput
+                    EmptyCharacteristic
+                    (coreOpaqueInteger 0)
+                    FoundationFofProjectable)
+        alteredExtensionality =
+            replaceAxiomInput
+                SetExtensionality
+                (FoundationAxiomInput
+                    SetExtensionality
+                    coreFalsum
+                    FoundationFofProjectable)
+        misclassifiedEmpty =
+            case findAxiomInput EmptyCharacteristic of
+                Just
+                    (FoundationAxiomInput
+                        tag
+                        syntax
+                        _backendClass) ->
+                            replaceAxiomInput
+                                tag
+                                (FoundationAxiomInput
+                                    tag
+                                    syntax
+                                    (FoundationRequiresTh0
+                                        (HigherOrderLambda :| [])))
+                Nothing ->
+                    impossible
+                        "compiled manifest omitted EmptyCharacteristic"
+        withoutLeast =
+            [ row
+            | row@(FoundationRuleInput tag _signature) <-
+                compiledFoundationRuleRows
+            , tag /= SetLfpLeast
+            ]
+        alteredInductSignature =
+            [ if tag == SetLfpInduct
+                then
+                    FoundationRuleInput
+                        tag
+                        (KernelRuleSignature [TySet] 0)
+                else row
+            | row@(FoundationRuleInput tag _signature) <-
+                compiledFoundationRuleRows
+            ]
+    assertAuditContains
+        (== MissingFoundationAxiom UnivOfMinimal)
+        (auditFoundationManifest
+            compiledFoundationIntrinsicRows
+            compiledFoundationRuleRows
+            withoutMinimal)
+    assertAuditContains
+        (== FoundationIntrinsicTypeMismatch
+                UnivOf
+                (TySet `TyArrow` TySet)
+                TySet)
+        (auditFoundationManifest
+            wrongUnivType
+            compiledFoundationRuleRows
+            compiledFoundationAxiomRows)
+    assertAuditContains
+        (== MissingFoundationRule SetLfpLeast)
+        (auditFoundationManifest
+            compiledFoundationIntrinsicRows
+            withoutLeast
+            compiledFoundationAxiomRows)
+    assertAuditContains
+        (\case
+            FoundationRuleSignatureMismatch
+                SetLfpInduct
+                _expected
+                (KernelRuleSignature [TySet] 0) ->
+                    True
+            _ ->
+                False)
+        (auditFoundationManifest
+            compiledFoundationIntrinsicRows
+            alteredInductSignature
+            compiledFoundationAxiomRows)
+    assertAuditContains
+        (== DuplicateFoundationAxiom EmptyCharacteristic)
+        (auditFoundationManifest
+            compiledFoundationIntrinsicRows
+            compiledFoundationRuleRows
+            duplicatedEmpty)
+    assertAuditContains
+        (\case
+            FoundationAxiomIllTyped
+                EmptyCharacteristic
+                (ExpectedCoreType TyProp TySet) ->
+                    True
+            _ ->
+                False)
+        (auditFoundationManifest
+            compiledFoundationIntrinsicRows
+            compiledFoundationRuleRows
+            alteredEmpty)
+    assertAuditContains
+        (== FoundationAxiomStatementMismatch
+                SetExtensionality)
+        (auditFoundationManifest
+            compiledFoundationIntrinsicRows
+            compiledFoundationRuleRows
+            alteredExtensionality)
+    assertAuditContains
+        (== FoundationAxiomBackendClassMismatch
+                EmptyCharacteristic
+                (FoundationRequiresTh0
+                    (HigherOrderLambda :| []))
+                FoundationFofProjectable)
+        (auditFoundationManifest
+            compiledFoundationIntrinsicRows
+            compiledFoundationRuleRows
+            misclassifiedEmpty)
+
+classifiesUnivOfSchemas :: Assertion
+classifiesUnivOfSchemas = do
+    foundation <-
+        either
+            (assertFailure . show)
+            pure
+            checkedFoundation
+    for_
+        [ UnivOfContains
+        , UnivOfTransitive
+        , UnivOfFamilyUnionClosed
+        , UnivOfPowerSetClosed
+        ]
+        \tag ->
+            assertEqual
+                (show tag)
+                FoundationFofProjectable
+                (foundationAxiomBackendClass foundation tag)
+    for_
+        [ UnivOfReplacementClosed
+        , UnivOfMinimal
+        ]
+        \tag ->
+            case foundationAxiomBackendClass foundation tag of
+                FoundationRequiresTh0 exclusions ->
+                    assertBool
+                        (show tag <> " has a structural exclusion")
+                        (not (null exclusions))
+                FoundationFofProjectable ->
+                    assertFailure
+                        (show tag <> " was classified as FOF")
+
+findAxiomInput
+    :: FoundationAxiomTag
+    -> Maybe FoundationAxiomInput
+findAxiomInput wanted =
+    List.find
+        (\case
+            FoundationAxiomInput tag _syntax _backendClass ->
+                tag == wanted)
+        compiledFoundationAxiomRows
+
+replaceAxiomInput
+    :: FoundationAxiomTag
+    -> FoundationAxiomInput
+    -> [FoundationAxiomInput]
+replaceAxiomInput wanted replacement =
+    fmap
+        (\row ->
+            case row of
+                FoundationAxiomInput tag _syntax _backendClass
+                    | tag == wanted ->
+                        replacement
+                _ ->
+                    row)
+        compiledFoundationAxiomRows
+
+assertAuditContains
+    :: (FoundationManifestError -> Bool)
+    -> Either
+        (NonEmpty FoundationManifestError)
+        FoundationManifestAudit
+    -> Assertion
+assertAuditContains predicate = \case
+    Left errors ->
+        assertBool
+            ("expected error not found in " <> show errors)
+            (any predicate errors)
+    Right _audit ->
+        assertFailure
+            "expected foundation-manifest audit to fail"