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