Migrate to `Felix` namespaceHEADhotg

1 files changed, 0 insertions, 284 deletions

diff --git a/source/Test/Unit/Foundation.hs b/source/Test/Unit/Foundation.hs
deleted file mode 100644
index 17ff526..0000000
--- a/source/Test/Unit/Foundation.hs
+++ /dev/null
@@ -1,284 +0,0 @@
-{-# LANGUAGE NoImplicitPrelude #-}
-
-module Test.Unit.Foundation (unitTests) where
-
-import Base
-import Checking.Core
-import 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"