{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE PatternSynonyms #-}

module Felix.Test.Unit.Kernel (unitTests) where

import Base hiding (Empty)
import Felix.Checking.Core
import Felix.Checking.Foundation qualified as Foundation
import Felix.Checking.Kernel.Derivation
import Felix.Checking.Kernel.Semantics qualified as Semantics
import Felix.Checking.Kernel.SetLfp qualified as SetLfp
import Felix.Checking.Typed.Inductive qualified as Inductive
import Felix.Report.Location (pattern Nowhere)
import Felix.Syntax.Internal qualified as Internal

import Data.Set qualified as Set
import Data.Vector qualified as Vector
import Test.Tasty
import Test.Tasty.HUnit


data TestGlobal = TestGlobal
    deriving (Show, Eq, Ord)

testGlobalType :: TestGlobal -> CoreType
testGlobalType _global = TySet

unitTests :: TestTree
unitTests =
    testGroup "Kernel replay"
        [ testCase
            "replays equality reflexivity through kernel semantics"
            replaysEqualityReflexivity
        , testCase
            "replays logical scopes and elimination"
            replaysLogicalScopes
        , testCase
            "replays quantifier and equality structure"
            replaysQuantifierAndEqualityStructure
        , testCase
            "records foundation and import leaves"
            recordsAuthorityLeaves
        , testCase
            "checks and replays the exact set fixed-point rules"
            checksSetLfpRules
        , testCase
            "replays direct inductive facts"
            replaysDirectInductiveFacts
        , testCase
            "rejects altered set fixed-point applications"
            rejectsAlteredSetLfpApplications
        , testCase
            "rejects invalid scoped replay"
            rejectsInvalidScopedReplay
        , testCase
            "rejects a caller-supplied target mismatch"
            rejectsTargetMismatch
        ]

replaysEqualityReflexivity :: Assertion
replaysEqualityReflexivity = do
    foundation <-
        expectRight Foundation.checkedFoundation
    operand <-
        expectRight
            (checkCanonicalCore
                absurd
                (CIntrinsic Empty))
    direct <-
        expectRight
            (Semantics.equalityReflexivity
                absurd
                (embedClosedCore [] operand))
    directClosed <-
        maybe
            (assertFailure
                "closed reflexivity result remained scoped")
            pure
            (closeScopedCore direct)
    replayed <-
        expectRight
            (replayKernelDerivation
                foundation
                defaultKernelReplayLimits
                absurd
                Vector.empty
                directClosed
                (equalityReflexivityDerivation operand))
    assertEqual
        "replay agrees with direct semantics"
        directClosed
        (replayedKernelTarget replayed)
    assertEqual
        "one replayed inference"
        1
        (replayedKernelNodeCount replayed)

replaysLogicalScopes :: Assertion
replaysLogicalScopes = do
    foundation <-
        expectRight Foundation.checkedFoundation
    proposition <-
        checkedClosed
            (CEq TySet
                (CIntrinsic Empty)
                (CIntrinsic Empty))
    implication <-
        checkedScoped []
            (CImp
                (frozenCoreTerm proposition)
                (frozenCoreTerm proposition))
    let propositionScoped =
            embedClosedCore [] proposition
        identity =
            implicationIntroductionDerivation
                propositionScoped
                (localHypothesisDerivation
                    (hypothesisIx 0))
        elimination =
            implicationIntroductionDerivation
                propositionScoped
                (implicationIntroductionDerivation
                    implication
                    (implicationEliminationDerivation
                        (localHypothesisDerivation
                            (hypothesisIx 0))
                        (localHypothesisDerivation
                            (hypothesisIx 1))))
        fromFalsum =
            implicationIntroductionDerivation
                falsum
                (falsumEliminationDerivation
                    (localHypothesisDerivation
                        (hypothesisIx 0))
                    propositionScoped)
        falsum =
            unsafeScoped [] CFalsum
    assertReplayTarget
        foundation
        (CImp
            (frozenCoreTerm proposition)
            (frozenCoreTerm proposition))
        identity
    assertReplayTarget
        foundation
        (CImp
            (frozenCoreTerm proposition)
            (CImp
                (scopedCoreTerm implication)
                (frozenCoreTerm proposition)))
        elimination
    assertReplayTarget
        foundation
        (CImp
            CFalsum
            (frozenCoreTerm proposition))
        fromFalsum

replaysQuantifierAndEqualityStructure :: Assertion
replaysQuantifierAndEqualityStructure = do
    foundation <-
        expectRight Foundation.checkedFoundation
    boundSet <-
        checkedScoped [TySet] (CBound 0)
    emptySet <-
        checkedScoped [] (CIntrinsic Empty)
    unionFunction <-
        checkedScoped [] (CIntrinsic FamilyUnion)
    proposition <-
        checkedClosed
            (CEq TySet
                (CIntrinsic Empty)
                (CIntrinsic Empty))
    convertedTarget <-
        checkedScoped []
            (CEq TySet
                (CApp
                    (CLam TySet (CBound 0))
                    (CIntrinsic Empty))
                (CIntrinsic Empty))
    oneReduction <-
        expectRight (conversionPlan 1)
    let boundReflexivity =
            scopedEqualityReflexivityDerivation boundSet
        universalReflexivity =
            forallIntroductionDerivation
                TySet
                boundReflexivity
        specializedReflexivity =
            forallEliminationDerivation
                universalReflexivity
                emptySet
        applicationCongruence =
            equalityCongruenceApplicationDerivation
                (scopedEqualityReflexivityDerivation
                    unionFunction)
                (scopedEqualityReflexivityDerivation
                    emptySet)
        lambdaCongruence =
            equalityCongruenceLambdaDerivation
                TySet
                boundReflexivity
        equalityMp =
            implicationIntroductionDerivation
                (embedClosedCore [] proposition)
                (equalityModusPonensDerivation
                    (scopedEqualityReflexivityDerivation
                        (embedClosedCore []
                            proposition))
                    (localHypothesisDerivation
                        (hypothesisIx 0)))
        conversion =
            convertJudgmentDerivation
                (scopedEqualityReflexivityDerivation
                    emptySet)
                convertedTarget
                oneReduction
    assertReplayTarget
        foundation
        (CForall TySet
            (CEq TySet
                (CBound 0)
                (CBound 0)))
        universalReflexivity
    assertReplayTarget
        foundation
        (CEq TySet
            (CIntrinsic Empty)
            (CIntrinsic Empty))
        specializedReflexivity
    assertReplayTarget
        foundation
        (CEq TySet
            (CApp
                (CIntrinsic FamilyUnion)
                (CIntrinsic Empty))
            (CApp
                (CIntrinsic FamilyUnion)
                (CIntrinsic Empty)))
        applicationCongruence
    assertReplayTarget
        foundation
        (CEq
            (TySet `TyArrow` TySet)
            (CLam TySet (CBound 0))
            (CLam TySet (CBound 0)))
        lambdaCongruence
    assertReplayTarget
        foundation
        (CImp
            (frozenCoreTerm proposition)
            (frozenCoreTerm proposition))
        equalityMp
    assertReplayTarget
        foundation
        (scopedCoreTerm convertedTarget)
        conversion

recordsAuthorityLeaves :: Assertion
recordsAuthorityLeaves = do
    foundation <-
        expectRight Foundation.checkedFoundation
    let foundationTag =
            Foundation.EmptyCharacteristic
        foundationTarget =
            mapFrozenGlobals
                absurd
                (Foundation.foundationAxiomFrozen
                    foundation
                    foundationTag)
    foundationReplay <-
        expectRight
            (replayKernelDerivation
                foundation
                defaultKernelReplayLimits
                absurd
                Vector.empty
                foundationTarget
                (foundationFactDerivation
                    foundationTag))
    assertEqual
        "exact foundation use"
        (Set.singleton foundationTag)
        (replayedKernelFoundationUses
            foundationReplay)
    importedStatement <-
        checkedClosed
            (CEq TySet
                (CIntrinsic Empty)
                (CIntrinsic Empty))
    importedJudgment <-
        expectRight
            (derivationImportJudgment
                importedStatement)
    importedReplay <-
        expectRight
            (replayKernelDerivation
                foundation
                defaultKernelReplayLimits
                absurd
                (Vector.singleton importedJudgment)
                importedStatement
                (importedFactDerivation
                    (importIx 0)))
    assertEqual
        "exact import use"
        (Set.singleton (importIx 0))
        (replayedKernelImportUses importedReplay)

checksSetLfpRules :: Assertion
checksSetLfpRules = do
    foundation <-
        expectRight Foundation.checkedFoundation
    ( domain
        , operator
        , predicate
        , element
        , fixedPoint
        , closedPremise
        , boundedPremise
        , monotonePremise
        , memberPremise
        , closurePremise
        ) <-
            setLfpFixture
    bound <-
        expectRight
            (SetLfp.setLfpBound
                foundation
                absurd
                domain
                operator)
    least <-
        expectRight
            (SetLfp.setLfpLeast
                foundation
                absurd
                domain
                operator
                domain
                closedPremise
                boundedPremise)
    fixed <-
        expectRight
            (SetLfp.setLfpFixed
                foundation
                absurd
                domain
                operator
                monotonePremise)
    inducted <-
        expectRight
            (SetLfp.setLfpInduct
                foundation
                absurd
                domain
                operator
                predicate
                element
                monotonePremise
                memberPremise
                closurePremise)
    expectedSubset <-
        expectRight
            (SetLfp.subsetProposition
                absurd
                fixedPoint
                domain)
    expectedFixed <-
        checkedScoped []
            (CEq TySet
                (scopedCoreTerm fixedPoint)
                (CApp
                    (scopedCoreTerm operator)
                    (scopedCoreTerm fixedPoint)))
    expectedPredicate <-
        checkedScoped []
            (CApp
                (scopedCoreTerm predicate)
                (scopedCoreTerm element))
    assertEqual "bound conclusion" expectedSubset bound
    assertEqual "least conclusion" expectedSubset least
    assertEqual "fixed conclusion" expectedFixed fixed
    assertEqual "induction conclusion" expectedPredicate inducted

    target <-
        maybe
            (assertFailure
                "closed fixed-point bound remained scoped")
            pure
            (closeScopedCore bound)
    replayed <-
        expectRight
            (replayKernelDerivation
                foundation
                defaultKernelReplayLimits
                absurd
                Vector.empty
                target
                (setLfpBoundDerivation
                    domain
                    operator))
    assertEqual
        "exact guarded-rule use"
        (Set.singleton Foundation.SetLfpBound)
        (replayedKernelRuleUses replayed)

replaysDirectInductiveFacts :: Assertion
replaysDirectInductiveFacts = do
    foundation <-
        expectRight Foundation.checkedFoundation
    traverse_
        (replayInductive foundation)
        [ Inductive.DirectInductive
            []
            (Internal.EmptySet Nowhere)
            (Inductive.DirectInductiveClause
                []
                []
                (Internal.EmptySet Nowhere)
                :| [])
        , let x = Internal.NamedVar "x"
          in Inductive.DirectInductive
                []
                (Internal.EmptySet Nowhere)
                ( Inductive.DirectInductiveClause
                    []
                    []
                    (Internal.EmptySet Nowhere)
                :| [ Inductive.DirectInductiveClause
                        [x]
                        [Inductive.DirectRecursiveCondition
                            (Internal.TermVar x)
                            (Inductive.directRecursiveCarrierContext Nowhere)]
                        (Internal.TermVar x)
                   ]
                )
        ]
  where
    replayInductive foundation inductive = do
        prepared <-
            expectRight
                (Inductive.prepareTypedInductive
                    testGlobalType
                    foundation
                    (const Nothing)
                    (Internal.Marker "direct_inductive")
                    inductive)
        imports <-
            traverse
                (expectRight . derivationImportJudgment)
                (Inductive.typedInductiveGuardTargets
                    prepared)
        traverse_
            (\fact -> do
                replayed <-
                    expectRight
                        (replayKernelDerivation
                            foundation
                            defaultKernelReplayLimits
                            (const Nothing)
                            imports
                            (Inductive.typedInductiveFactTarget
                                fact)
                            (Inductive.typedInductiveFactDerivation
                                fact))
                assertEqual
                    "replay target"
                    (Inductive.typedInductiveFactTarget
                        fact)
                    (replayedKernelTarget replayed))
            (Inductive.typedInductiveFacts
                prepared)

rejectsAlteredSetLfpApplications :: Assertion
rejectsAlteredSetLfpApplications = do
    foundation <-
        expectRight Foundation.checkedFoundation
    ( domain
        , operator
        , predicate
        , _element
        , _fixedPoint
        , _closedPremise
        , boundedPremise
        , _monotonePremise
        , _memberPremise
        , _closurePremise
        ) <-
            setLfpFixture
    falsum <-
        checkedScoped [] CFalsum
    assertEqual
        "altered leastness premise"
        (Left
            (SetLfp.SetLfpRulePremiseMismatch
                Foundation.SetLfpLeast
                0))
        (SetLfp.setLfpLeast
            foundation
            absurd
            domain
            operator
            domain
            falsum
            boundedPremise)
    assertEqual
        "operator type mismatch"
        (Left
            (SetLfp.SetLfpRuleArgumentTypeMismatch
                Foundation.SetLfpBound
                1
                (TySet `TyArrow` TySet)
                (TySet `TyArrow` TyProp)))
        (SetLfp.setLfpBound
            foundation
            absurd
            domain
            predicate)
    bound <-
        expectRight
            (SetLfp.setLfpBound
                foundation
                absurd
                domain
                operator)
    wrongTarget <-
        checkedClosed CFalsum
    assertEqual
        "altered replay target"
        (Left KernelReplayTargetMismatch)
        (replayedKernelTarget
            <$> replayKernelDerivation
                foundation
                defaultKernelReplayLimits
                absurd
                Vector.empty
                wrongTarget
                (setLfpBoundDerivation
                    domain
                    operator))
    assertEqual
        "the direct bound remains well formed"
        TyProp
        (scopedCoreType bound)

setLfpFixture
    :: IO
        ( ScopedCheckedCore Void
        , ScopedCheckedCore Void
        , ScopedCheckedCore Void
        , ScopedCheckedCore Void
        , ScopedCheckedCore Void
        , ScopedCheckedCore Void
        , ScopedCheckedCore Void
        , ScopedCheckedCore Void
        , ScopedCheckedCore Void
        , ScopedCheckedCore Void
        )
setLfpFixture = do
    domain <-
        checkedScoped [] (CIntrinsic Empty)
    operator <-
        checkedScoped []
            (CLam TySet (CBound 0))
    predicate <-
        checkedScoped []
            (CLam TySet
                (CEq TySet
                    (CBound 0)
                    (CBound 0)))
    element <-
        checkedScoped [] (CIntrinsic Empty)
    fixedPoint <-
        expectRight
            (SetLfp.setLfpTerm
                absurd
                domain
                operator)
    operatorDomain <-
        checkedScoped []
            (CApp
                (scopedCoreTerm operator)
                (scopedCoreTerm domain))
    closedPremise <-
        expectRight
            (SetLfp.subsetProposition
                absurd
                operatorDomain
                domain)
    boundedPremise <-
        expectRight
            (SetLfp.subsetProposition
                absurd
                domain
                domain)
    monotonePremise <-
        expectRight
            (SetLfp.boundedMonoProposition
                absurd
                domain
                operator)
    memberPremise <-
        expectRight
            (SetLfp.memberProposition
                absurd
                element
                fixedPoint)
    closurePremise <-
        expectRight
            (SetLfp.inductionClosureProposition
                absurd
                domain
                operator
                predicate)
    pure
        ( domain
        , operator
        , predicate
        , element
        , fixedPoint
        , closedPremise
        , boundedPremise
        , monotonePremise
        , memberPremise
        , closurePremise
        )

rejectsInvalidScopedReplay :: Assertion
rejectsInvalidScopedReplay = do
    foundation <-
        expectRight Foundation.checkedFoundation
    proposition <-
        checkedClosed
            (CEq TySet
                (CIntrinsic Empty)
                (CIntrinsic Empty))
    boundSet <-
        checkedScoped [TySet] (CBound 0)
    assertEqual
        "missing local hypothesis"
        (Left
            (KernelReplayHypothesisOutOfBounds
                (hypothesisIx 0)))
        (replayedKernelTarget
            <$> replayKernelDerivation
                foundation
                defaultKernelReplayLimits
                absurd
                Vector.empty
                proposition
                (localHypothesisDerivation
                    (hypothesisIx 0)))
    assertEqual
        "stored term from another lexical context"
        (Left
            (KernelReplayStoredContextMismatch
                []
                [TySet]))
        (replayedKernelTarget
            <$> replayKernelDerivation
                foundation
                defaultKernelReplayLimits
                absurd
                Vector.empty
                proposition
                (scopedEqualityReflexivityDerivation
                    boundSet))
    expanded <-
        checkedScoped []
            (CEq TySet
                (CApp
                    (CLam TySet (CBound 0))
                    (CIntrinsic Empty))
                (CIntrinsic Empty))
    noReductions <-
        expectRight (conversionPlan 0)
    assertEqual
        "conversion budget"
        (Left
            (KernelReplaySemanticsError
                Semantics.KernelConversionBudgetExhausted))
        (replayedKernelTarget
            <$> replayKernelDerivation
                foundation
                defaultKernelReplayLimits
                absurd
                Vector.empty
                (unsafeClosed
                    (scopedCoreTerm expanded))
                (convertJudgmentDerivation
                    (equalityReflexivityDerivation
                        (unsafeClosed
                            (CIntrinsic Empty)))
                    expanded
                    noReductions))
    let checkedAsSet _global =
            Just TySet
        replayedAsProposition _global =
            Just TyProp
    globalTarget <-
        expectRight
            (checkCanonicalCore
                checkedAsSet
                (CEq TySet
                    (CGlobal TestGlobal)
                    (CGlobal TestGlobal)))
    assertEqual
        "stored global types are rechecked"
        (Left
            (KernelReplayStoredTermIllTyped
                (EqualityOperandTypeMismatch
                    TySet
                    TyProp)))
        (replayedKernelTarget
            <$> replayKernelDerivation
                foundation
                defaultKernelReplayLimits
                replayedAsProposition
                Vector.empty
                globalTarget
                (equalityReflexivityDerivation
                    (unsafeGlobalOperand
                        checkedAsSet)))
    oneNode <-
        expectRight (kernelReplayLimits 1 10)
    let propositionScoped =
            embedClosedCore [] proposition
        identityTarget =
            unsafeClosed
                (CImp
                    (frozenCoreTerm proposition)
                    (frozenCoreTerm proposition))
    assertEqual
        "replay node limit"
        (Left
            (KernelReplayNodeLimitExceeded 1))
        (replayedKernelTarget
            <$> replayKernelDerivation
                foundation
                oneNode
                absurd
                Vector.empty
                identityTarget
                (implicationIntroductionDerivation
                    propositionScoped
                    (localHypothesisDerivation
                        (hypothesisIx 0))))

rejectsTargetMismatch :: Assertion
rejectsTargetMismatch = do
    foundation <-
        expectRight Foundation.checkedFoundation
    operand <-
        expectRight
            (checkCanonicalCore
                absurd
                (CIntrinsic Empty))
    wrongTarget <-
        expectRight
            (checkCanonicalCore
                absurd
                (CImp CFalsum CFalsum))
    assertEqual
        "the expected target is comparison input, not evidence"
        (Left KernelReplayTargetMismatch)
        (replayedKernelTarget
            <$> replayKernelDerivation
                foundation
                defaultKernelReplayLimits
                absurd
                Vector.empty
                wrongTarget
                (equalityReflexivityDerivation operand))

assertReplayTarget
    :: Foundation.CheckedFoundation
    -> CanonicalTerm Void
    -> KernelDerivation Void
    -> Assertion
assertReplayTarget foundation expectedTerm derivation = do
    expected <-
        checkedClosed expectedTerm
    replayed <-
        expectRight
            (replayKernelDerivation
                foundation
                defaultKernelReplayLimits
                absurd
                Vector.empty
                expected
                derivation)
    assertEqual
        "replayed exact target"
        expected
        (replayedKernelTarget replayed)

checkedClosed
    :: CanonicalTerm Void
    -> IO (FrozenCheckedCore Void)
checkedClosed =
    expectRight . checkCanonicalCore absurd

checkedScoped
    :: [CoreType]
    -> CanonicalTerm Void
    -> IO (ScopedCheckedCore Void)
checkedScoped context =
    expectRight
        . checkScopedCanonicalCore absurd context

unsafeScoped
    :: [CoreType]
    -> CanonicalTerm Void
    -> ScopedCheckedCore Void
unsafeScoped context term =
    case checkScopedCanonicalCore absurd context term of
        Left coreError ->
            impossible
                ("invalid static kernel fixture: "
                    <> show coreError)
        Right checked ->
            checked

unsafeClosed
    :: CanonicalTerm Void
    -> FrozenCheckedCore Void
unsafeClosed term =
    case checkCanonicalCore absurd term of
        Left coreError ->
            impossible
                ("invalid static closed kernel fixture: "
                    <> show coreError)
        Right checked ->
            checked

unsafeGlobalOperand
    :: (TestGlobal -> Maybe CoreType)
    -> FrozenCheckedCore TestGlobal
unsafeGlobalOperand globalType =
    case checkCanonicalCore
            globalType
            (CGlobal TestGlobal) of
        Left coreError ->
            impossible
                ("invalid static global kernel fixture: "
                    <> show coreError)
        Right checked ->
            checked

expectRight
    :: Show error
    => Either error value
    -> IO value
expectRight =
    either
        (assertFailure . show)
        pure