diff options
Diffstat (limited to 'source/Felix/Test/Unit/Kernel.hs')
| -rw-r--r-- | source/Felix/Test/Unit/Kernel.hs | 858 |
1 files changed, 858 insertions, 0 deletions
diff --git a/source/Felix/Test/Unit/Kernel.hs b/source/Felix/Test/Unit/Kernel.hs new file mode 100644 index 0000000..7762a7e --- /dev/null +++ b/source/Felix/Test/Unit/Kernel.hs @@ -0,0 +1,858 @@ +{-# 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 |