summaryrefslogtreecommitdiff
path: root/source/Test/Unit/Core.hs
diff options
context:
space:
mode:
Diffstat (limited to 'source/Test/Unit/Core.hs')
-rw-r--r--source/Test/Unit/Core.hs508
1 files changed, 0 insertions, 508 deletions
diff --git a/source/Test/Unit/Core.hs b/source/Test/Unit/Core.hs
deleted file mode 100644
index e1ba10d..0000000
--- a/source/Test/Unit/Core.hs
+++ /dev/null
@@ -1,508 +0,0 @@
-{-# LANGUAGE NoImplicitPrelude #-}
-
-module Test.Unit.Core (unitTests) where
-
-import Base hiding (Empty)
-import Checking.Core
-import Checking.Foundation qualified as Foundation
-
-import Control.DeepSeq (NFData(..), force)
-import Hedgehog
-import Hedgehog.Gen qualified as Gen
-import Hedgehog.Range qualified as Range
-import Test.Tasty
-import Test.Tasty.HUnit hiding (assert)
-import Test.Tasty.Hedgehog (testPropertyNamed)
-
-
-data TestGlobal
- = TestGlobal
- | TestPairGlobal
- deriving (Show, Eq, Ord)
-
-instance NFData TestGlobal where
- rnf _global =
- ()
-
-testGlobalType :: TestGlobal -> Maybe CoreType
-testGlobalType TestGlobal =
- Just TySet
-testGlobalType TestPairGlobal =
- Just (TySet `TyArrow` (TySet `TyArrow` TySet))
-
-unitTests :: TestTree
-unitTests =
- testGroup "Checked core"
- [ testCase
- "freezes explicit binder positions"
- freezesExplicitBinderPositions
- , testCase
- "freezes generalized substitution without capture"
- freezesGeneralizedSubstitution
- , testCase
- "rejects ill-typed and open terms"
- rejectsInvalidTerms
- , testCase
- "rechecks canonical terms without unchecked construction"
- rechecksCanonicalTerms
- , testCase
- "checks scoped canonical weakening and substitution"
- checksScopedCanonicalOperations
- , testCase
- "builds set-induction hypotheses from the complete property"
- buildsSetInductionHypotheses
- , testCase
- "specializes the checked separation characteristic"
- specializesCheckedSeparationCharacteristic
- , testCase
- "specializes the checked replacement characteristic"
- specializesCheckedReplacementCharacteristic
- , testCase
- "thaws checked closed terms without changing them"
- thawsCheckedClosedTerms
- , testPropertyNamed
- "optimized freeze agrees with bounded reference"
- "prop_freezeAgreesWithReference"
- prop_freezeAgreesWithReference
- ]
-
-freezesExplicitBinderPositions :: Assertion
-freezesExplicitBinderPositions = do
- let x = 0 :: Int
- y = 1 :: Int
- freeze body = do
- checked <-
- either
- (assertFailure . show)
- pure
- (checkClosedCore
- testGlobalType
- (coreLambda TySet x
- (coreLambda TyProp y body)))
- either
- (assertFailure . show)
- (pure . frozenCoreTerm)
- (freezeClosed checked)
- nearest <-
- freeze (coreLocal y)
- outer <-
- freeze (coreLocal x)
- global <-
- freeze (coreGlobal TestGlobal)
- assertEqual
- "nearest binder"
- (CLam TySet (CLam TyProp (CBound 0)))
- nearest
- assertEqual
- "outer binder"
- (CLam TySet (CLam TyProp (CBound 1)))
- outer
- assertEqual
- "global with both vacuous binders"
- (CLam TySet (CLam TyProp (CGlobal TestGlobal)))
- global
-
-freezesGeneralizedSubstitution :: Assertion
-freezesGeneralizedSubstitution = do
- let outer = 0 :: Int
- inner = 1 :: Int
- placeholder = 2 :: Int
- innerTerm =
- coreLambda TySet inner (coreLocal placeholder)
- substituted =
- innerTerm >>= \local ->
- if local == placeholder
- then coreLocal outer
- else coreLocal local
- term =
- coreLambda TyProp outer substituted
- checked <-
- either
- (assertFailure . show)
- pure
- (checkClosedCore testGlobalType term)
- optimized <-
- either
- (assertFailure . show)
- pure
- (freezeClosed checked)
- reference <-
- either
- (assertFailure . show)
- pure
- (referenceFreezeClosed checked)
- assertEqual "reference result" reference optimized
- assertEqual
- "outer variable remains outside the inner binder"
- (CLam TyProp (CLam TySet (CBound 1)))
- (frozenCoreTerm optimized)
-
-rejectsInvalidTerms :: Assertion
-rejectsInvalidTerms = do
- assertEqual
- "free local"
- (Left UnboundCoreLocal)
- (checkedCoreType
- <$> checkClosedCore
- testGlobalType
- (coreLocal (0 :: Int)))
- assertEqual
- "application argument"
- (Left
- (ApplicationArgumentTypeMismatch
- TySet
- TyProp))
- (checkedCoreType
- <$> checkClosedCore
- testGlobalType
- (coreApply
- (coreIntrinsic FamilyUnion)
- coreFalsum))
- assertEqual
- "equality operand"
- (Left
- (EqualityOperandTypeMismatch
- TySet
- TyProp))
- (checkedCoreType
- <$> checkClosedCore
- testGlobalType
- (coreEquality
- TySet
- coreFalsum
- (coreGlobal TestGlobal)))
-
-rechecksCanonicalTerms :: Assertion
-rechecksCanonicalTerms = do
- let term =
- CForall TySet
- (CEq TySet
- (CBound 0)
- (CBound 0))
- assertEqual
- "well-typed canonical proposition"
- (Right (TyProp, term))
- ( (\checked ->
- ( frozenCoreType checked
- , frozenCoreTerm checked
- ))
- <$> checkCanonicalCore testGlobalType term
- )
- assertEqual
- "out-of-scope de Bruijn index"
- (Left (UnboundCoreIndex 1))
- (frozenCoreType
- <$> checkCanonicalCore
- testGlobalType
- (CForall TySet (CBound 1)))
- assertEqual
- "canonical application still checks argument types"
- (Left
- (ApplicationArgumentTypeMismatch
- TySet
- TyProp))
- (frozenCoreType
- <$> checkCanonicalCore
- testGlobalType
- (CApp
- (CIntrinsic FamilyUnion)
- CFalsum))
-
-checksScopedCanonicalOperations :: Assertion
-checksScopedCanonicalOperations = do
- scoped <-
- either
- (assertFailure . show)
- pure
- (checkScopedCanonicalCore
- testGlobalType
- [TySet]
- (CBound 0))
- weakened <-
- either
- (assertFailure . show)
- pure
- (weakenScopedCore
- testGlobalType
- TyProp
- scoped)
- assertEqual
- "nearest binder insertion shifts the prior local"
- ( [TyProp, TySet]
- , TySet
- , CBound 1
- )
- ( scopedCoreContext weakened
- , scopedCoreType weakened
- , scopedCoreTerm weakened
- )
- assertEqual
- "top-level binder substitution removes its index"
- (CEq TySet
- (CIntrinsic Empty)
- (CIntrinsic Empty))
- (instantiateCanonical
- (CIntrinsic Empty
- :: CanonicalTerm TestGlobal)
- (CEq TySet
- (CBound 0)
- (CBound 0)))
- root <-
- either
- (assertFailure . show)
- pure
- (checkScopedCanonicalCore
- testGlobalType
- []
- (CGlobal TestGlobal))
- assertEqual
- "empty scoped context closes"
- (Just
- (TySet, CGlobal TestGlobal))
- ( (\closed ->
- ( frozenCoreType closed
- , frozenCoreTerm closed
- ))
- <$> closeScopedCore root
- )
-
-buildsSetInductionHypotheses :: Assertion
-buildsSetInductionHypotheses = do
- claimProperty <-
- either
- (assertFailure . show)
- pure
- (checkScopedCanonicalCore
- testGlobalType
- [TySet]
- (CImp
- (CEq TySet
- (CBound 0)
- (CIntrinsic Empty))
- (CEq TySet
- (CBound 0)
- (CBound 0))))
- hypothesis <-
- maybe
- (assertFailure "set-induction hypothesis was not constructed")
- pure
- (scopedSetInductionHypothesis 0 claimProperty)
- assertEqual
- "antecedent and goal are both generalized over the member"
- (CForall TySet
- (CImp
- (CApp
- (CApp
- (CIntrinsic Member)
- (CBound 0))
- (CBound 1))
- (CImp
- (CEq TySet
- (CBound 0)
- (CIntrinsic Empty))
- (CEq TySet
- (CBound 0)
- (CBound 0)))))
- (scopedCoreTerm hypothesis)
-
-specializesCheckedSeparationCharacteristic :: Assertion
-specializesCheckedSeparationCharacteristic = do
- foundation <-
- either
- (assertFailure . show)
- pure
- Foundation.checkedFoundation
- let bound = CIntrinsic Empty
- predicate =
- CLam TySet
- (CEq TySet (CBound 0) (CBound 0))
- separation =
- CApp
- (CApp (CIntrinsic Sep) bound)
- predicate
- body <-
- either
- (assertFailure . show)
- pure
- (checkScopedCanonicalCore
- testGlobalType
- []
- separation)
- definition <-
- maybe
- (assertFailure "separation did not form a set definition")
- pure
- (scopedSetDefinition
- (Foundation.foundationAxiomFrozen
- foundation
- Foundation.SeparationCharacteristic)
- body)
- let generated =
- instantiateCanonical
- separation
- (scopedCoreTerm definition)
- expected =
- betaNormalize
- (specializeForall predicate
- (specializeForall bound
- (mapCanonicalGlobals absurd
- (frozenCoreTerm
- (Foundation.foundationAxiomFrozen
- foundation
- Foundation.SeparationCharacteristic)))))
- assertEqual
- "local characteristic is the checked rule specialization"
- expected
- generated
-
-specializesCheckedReplacementCharacteristic :: Assertion
-specializesCheckedReplacementCharacteristic = do
- foundation <-
- either
- (assertFailure . show)
- pure
- Foundation.checkedFoundation
- pair <- checked [] (CGlobal TestPairGlobal)
- domain <- checked [] (CIntrinsic Empty)
- value <- checked [TySet] (CBound 0)
- (graph, checkedDomain, function) <-
- maybe
- (assertFailure "checked values did not form a replacement graph")
- pure
- (scopedReplacementGraph pair domain value)
- definition <-
- maybe
- (assertFailure "replacement graph did not form a definition")
- pure
- (scopedCharacteristicDefinition
- (Foundation.foundationAxiomFrozen
- foundation
- Foundation.ReplacementCharacteristic)
- graph
- (checkedDomain :| [function]))
- let generated =
- instantiateCanonical
- (scopedCoreTerm graph)
- (scopedCoreTerm definition)
- expected =
- betaNormalize
- (specializeForall (scopedCoreTerm function)
- (specializeForall (scopedCoreTerm checkedDomain)
- (mapCanonicalGlobals absurd
- (frozenCoreTerm
- (Foundation.foundationAxiomFrozen
- foundation
- Foundation.ReplacementCharacteristic)))))
- assertEqual
- "local graph characteristic is the checked rule specialization"
- expected
- generated
- where
- checked context term =
- either
- (assertFailure . show)
- pure
- (checkScopedCanonicalCore testGlobalType context term)
-
-specializeForall
- :: CanonicalTerm global
- -> CanonicalTerm global
- -> CanonicalTerm global
-specializeForall argument = \case
- CForall _binderType body ->
- instantiateCanonical argument body
- _ ->
- error "the checked characteristic lost a binder"
-
-betaNormalize :: CanonicalTerm global -> CanonicalTerm global
-betaNormalize = \case
- CApp function argument ->
- case betaNormalize function of
- CLam _binderType body ->
- betaNormalize
- (instantiateCanonical
- (betaNormalize argument)
- body)
- normalizedFunction ->
- CApp normalizedFunction (betaNormalize argument)
- CLam binderType body ->
- CLam binderType (betaNormalize body)
- CImp premise conclusion ->
- CImp
- (betaNormalize premise)
- (betaNormalize conclusion)
- CEq operandType left right ->
- CEq operandType
- (betaNormalize left)
- (betaNormalize right)
- CForall binderType body ->
- CForall binderType (betaNormalize body)
- term -> term
-
-thawsCheckedClosedTerms :: Assertion
-thawsCheckedClosedTerms = do
- let source =
- coreLambda TySet (0 :: Int)
- (coreForall TySet 1
- (coreEquality
- TySet
- (coreLocal 0)
- (coreLocal 1)))
- freeze syntax = do
- checked <-
- either
- (assertFailure . show)
- pure
- (checkClosedCore testGlobalType syntax)
- either
- (assertFailure . show)
- pure
- (freezeClosed checked)
- original <-
- freeze source
- roundTrip <-
- freeze (thawFrozenCore original)
- assertEqual "frozen term" original roundTrip
- assertEqual
- "global inventory"
- mempty
- (frozenCoreGlobals original)
-
-prop_freezeAgreesWithReference :: Property
-prop_freezeAgreesWithReference = property do
- depth <-
- forAll (Gen.int (Range.linear 1 10))
- binderTypes <-
- forAll
- (Gen.list
- (Range.singleton depth)
- (Gen.element
- [ TyProp
- , TySet
- , TySet `TyArrow` TySet
- ]))
- selected <-
- forAll
- (Gen.maybe
- (Gen.int (Range.linear 0 (depth - 1))))
- let binders =
- zip [0 :: Int ..] binderTypes
- body =
- maybe
- (coreGlobal TestGlobal)
- coreLocal
- selected
- term =
- foldr
- (\(local, binderType) ->
- coreLambda binderType local)
- body
- binders
- checked <-
- evalEither
- (checkClosedCore testGlobalType term)
- optimized <-
- evalEither (force <$> freezeClosed checked)
- reference <-
- evalEither (force <$> referenceFreezeClosed checked)
- optimized === reference
generated by cgit v1.2.3 (git 2.39.1) at 2026-08-06 18:44:24 +0000