{-# 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"