summaryrefslogtreecommitdiff
path: root/source/Test/Unit/Kernel.hs
diff options
context:
space:
mode:
Diffstat (limited to 'source/Test/Unit/Kernel.hs')
-rw-r--r--source/Test/Unit/Kernel.hs858
1 files changed, 0 insertions, 858 deletions
diff --git a/source/Test/Unit/Kernel.hs b/source/Test/Unit/Kernel.hs
deleted file mode 100644
index d01a194..0000000
--- a/source/Test/Unit/Kernel.hs
+++ /dev/null
@@ -1,858 +0,0 @@
-{-# LANGUAGE NoImplicitPrelude #-}
-{-# LANGUAGE PatternSynonyms #-}
-
-module Test.Unit.Kernel (unitTests) where
-
-import Base hiding (Empty)
-import Checking.Core
-import Checking.Foundation qualified as Foundation
-import Checking.Kernel.Derivation
-import Checking.Kernel.Semantics qualified as Semantics
-import Checking.Kernel.SetLfp qualified as SetLfp
-import Checking.Typed.Inductive qualified as Inductive
-import Report.Location (pattern Nowhere)
-import 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
generated by cgit v1.2.3 (git 2.39.1) at 2026-08-06 19:48:38 +0000